case h
x✝ : ℝ
⊢ ↑(expMapCircle ↑x✝) = ↑(cos ↑x✝) + ↑(sin ↑x✝) * I
θ : Angle
⊢ ↑(expMapCircle θ) = ↑(cos θ) + ↑(sin θ) * I
induction θ using Real.Angle.induction_on
no goals
case h
x✝ : ℝ
⊢ ↑(expMapCircle ↑x✝) = ↑(cos ↑x✝) + ↑(sin ↑x✝) * I
simp [Complex.exp_mul_I]