theorem Complex.norm_sub_one_sq_eq_of_norm_one {z : ℂ} (hz : ‖z‖ = 1) : ‖z - 1‖ ^ 2 = 2 * (1 - z.re)

theorem Complex.norm_sub_one_sq_eqOn_sphere : Set.EqOn (fun (x : ℂ) => ‖x - 1‖ ^ 2) (fun (z : ℂ) => 2 * (1 - z.re)) (Metric.sphere 0 1)