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