case h
x✝ : ℝ
⊢ ↑(arg ↑(expMapCircle ↑x✝)) = ↑x✝
θ : Angle
⊢ ↑(arg ↑(expMapCircle θ)) = θ
induction θ using Real.Angle.induction_on
no goals
case h
x✝ : ℝ
⊢ ↑(arg ↑(expMapCircle ↑x✝)) = ↑x✝
rw [Real.Angle.expMapCircle_coe, expMapCircle_apply, exp_mul_I, ← ofReal_cos, ← ofReal_sin, ←
  Real.Angle.cos_coe, ← Real.Angle.sin_coe, arg_cos_add_sin_mul_I_coe_angle]