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