x : ℝ
⊢ cos (π / 2 - π / 3) ^ 2 = cos (π / 6) ^ 2
x : ℝ
⊢ sin (π / 3) ^ 2 = 3 / 4
rw [← cos_pi_div_two_sub, ← sq_cos_pi_div_six]
case e_a.e_x
x : ℝ
⊢ π / 2 - π / 3 = π / 6
x : ℝ
⊢ cos (π / 2 - π / 3) ^ 2 = cos (π / 6) ^ 2
congr
no goals
case e_a.e_x
x : ℝ
⊢ π / 2 - π / 3 = π / 6
ring