case h
x✝ : ℝ
⊢ cos (↑(π / 2) - ↑x✝) = sin ↑x✝
θ : Angle
⊢ cos (↑(π / 2) - θ) = sin θ
induction θ using Real.Angle.induction_on
no goals
case h
x✝ : ℝ
⊢ cos (↑(π / 2) - ↑x✝) = sin ↑x✝
exact Real.cos_pi_div_two_sub _