case h
x✝ : ℝ
⊢ expMapCircle (-↑x✝) = (expMapCircle ↑x✝)⁻¹
θ : Angle
⊢ expMapCircle (-θ) = (expMapCircle θ)⁻¹
induction θ using Real.Angle.induction_on
no goals
case h
x✝ : ℝ
⊢ expMapCircle (-↑x✝) = (expMapCircle ↑x✝)⁻¹
simp_rw [← Real.Angle.coe_neg, Real.Angle.expMapCircle_coe, _root_.expMapCircle_neg]