⊢ cos (choose exists_cos_eq_zero) = 0
⊢ cos (π / 2) = 0
rw [Real.pi, mul_div_cancel_left _ (two_ne_zero' ℝ)]
no goals
⊢ cos (choose exists_cos_eq_zero) = 0
exact (Classical.choose_spec exists_cos_eq_zero).2