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