[GOAL]
z : ℂ
⊢ z ∈ circle ↔ ↑normSq z = 1
[PROOFSTEP]
simp [Complex.abs]
[GOAL]
z : { x // x ∈ circle }
⊢ ↑normSq ↑z = 1
[PROOFSTEP]
simp [normSq_eq_abs]
[GOAL]
z : { x // x ∈ circle }
⊢ ↑z⁻¹ = ↑(starRingEnd ℂ) ↑z
[PROOFSTEP]
rw [coe_inv_circle, inv_def, normSq_eq_of_mem_circle, inv_one, ofReal_one, mul_one]
[GOAL]
z : ℂ
hz : z ≠ 0
⊢ ↑Complex.abs (↑(starRingEnd ℂ) z / z) = 1
[PROOFSTEP]
rw [map_div₀, abs_conj, div_self]
[GOAL]
z : ℂ
hz : z ≠ 0
⊢ ↑Complex.abs z ≠ 0
[PROOFSTEP]
exact Complex.abs.ne_zero hz
[GOAL]
t : ℝ
⊢ exp (↑t * I) ∈ circle
[PROOFSTEP]
simp [exp_mul_I, abs_cos_add_sin_mul_I]
[GOAL]
⊢ ↑(↑expMapCircle 0) = ↑1
[PROOFSTEP]
rw [expMapCircle_apply, ofReal_zero, zero_mul, exp_zero, Submonoid.coe_one]
[GOAL]
x y : ℝ
⊢ ↑(↑expMapCircle (x + y)) = ↑(↑expMapCircle x * ↑expMapCircle y)
[PROOFSTEP]
simp only [expMapCircle_apply, Submonoid.coe_mul, ofReal_add, add_mul, Complex.exp_add]
