case h
x : ℂ
⊢ (x ∈ Set.range fun x => exp (↑x * I)) ↔ x ∈ Metric.sphere 0 1
⊢ (Set.range fun x => exp (↑x * I)) = Metric.sphere 0 1
ext x
no goals
case h
x : ℂ
⊢ (x ∈ Set.range fun x => exp (↑x * I)) ↔ x ∈ Metric.sphere 0 1
simp only [mem_sphere_zero_iff_norm, norm_eq_abs, abs_eq_one_iff, Set.mem_range]