x : ℝ
⊢ cos (π / 2 - π / 3) = cos (π / 6)
x : ℝ
⊢ sin (π / 3) = sqrt 3 / 2
rw [← cos_pi_div_two_sub, ← cos_pi_div_six]
case e_x
x : ℝ
⊢ π / 2 - π / 3 = π / 6
x : ℝ
⊢ cos (π / 2 - π / 3) = cos (π / 6)
congr
no goals
case e_x
x : ℝ
⊢ π / 2 - π / 3 = π / 6
ring