case h
θ₂ : Angle
x✝ : ℝ
⊢ expMapCircle (↑x✝ + θ₂) = expMapCircle ↑x✝ * expMapCircle θ₂
θ₁ θ₂ : Angle
⊢ expMapCircle (θ₁ + θ₂) = expMapCircle θ₁ * expMapCircle θ₂
induction θ₁ using Real.Angle.induction_on
case h.h
x✝¹ x✝ : ℝ
⊢ expMapCircle (↑x✝¹ + ↑x✝) = expMapCircle ↑x✝¹ * expMapCircle ↑x✝
case h
θ₂ : Angle
x✝ : ℝ
⊢ expMapCircle (↑x✝ + θ₂) = expMapCircle ↑x✝ * expMapCircle θ₂
induction θ₂ using Real.Angle.induction_on
no goals
case h.h
x✝¹ x✝ : ℝ
⊢ expMapCircle (↑x✝¹ + ↑x✝) = expMapCircle ↑x✝¹ * expMapCircle ↑x✝
exact _root_.expMapCircle_add _ _