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