case h
x✝ : ℝ
⊢ cos ↑x✝ ^ 2 + sin ↑x✝ ^ 2 = 1
θ : Angle
⊢ cos θ ^ 2 + sin θ ^ 2 = 1
induction θ using Real.Angle.induction_on
no goals
case h
x✝ : ℝ
⊢ cos ↑x✝ ^ 2 + sin ↑x✝ ^ 2 = 1
exact Real.cos_sq_add_sin_sq _