x : ℝ
h1 : cos (π / 6) ^ 2 = 1 / 2 + 1 / 2 / 2
⊢ cos (π / 6) ^ 2 = 3 / 4
x : ℝ
⊢ cos (π / 6) ^ 2 = 3 / 4
have h1 : cos (π / 6) ^ 2 = 1 / 2 + 1 / 2 / 2 := by
  convert cos_sq (π / 6) using 3
  have h2 : 2 * (π / 6) = π / 3 := by linarith
  rw [h2, cos_pi_div_three]
x : ℝ
h1✝ : cos (π / 6) ^ 2 = 1 / 2 + 1 / 2 / 2
h1 : cos (π / 6) ^ 2 - (1 / 2 + 1 / 2 / 2) = 0
⊢ cos (π / 6) ^ 2 - 3 / 4 = 0
x : ℝ
h1 : cos (π / 6) ^ 2 = 1 / 2 + 1 / 2 / 2
⊢ cos (π / 6) ^ 2 = 3 / 4
rw [← sub_eq_zero] at h1⊢
case h.e'_2
x : ℝ
h1✝ : cos (π / 6) ^ 2 = 1 / 2 + 1 / 2 / 2
h1 : cos (π / 6) ^ 2 - (1 / 2 + 1 / 2 / 2) = 0
⊢ cos (π / 6) ^ 2 - 3 / 4 = cos (π / 6) ^ 2 - (1 / 2 + 1 / 2 / 2)
x : ℝ
h1✝ : cos (π / 6) ^ 2 = 1 / 2 + 1 / 2 / 2
h1 : cos (π / 6) ^ 2 - (1 / 2 + 1 / 2 / 2) = 0
⊢ cos (π / 6) ^ 2 - 3 / 4 = 0
convert h1 using 1
no goals
case h.e'_2
x : ℝ
h1✝ : cos (π / 6) ^ 2 = 1 / 2 + 1 / 2 / 2
h1 : cos (π / 6) ^ 2 - (1 / 2 + 1 / 2 / 2) = 0
⊢ cos (π / 6) ^ 2 - 3 / 4 = cos (π / 6) ^ 2 - (1 / 2 + 1 / 2 / 2)
ring
case h.e'_3.h.e'_6.h.e'_5
x : ℝ
⊢ 1 / 2 = cos (2 * (π / 6))
x : ℝ
⊢ cos (π / 6) ^ 2 = 1 / 2 + 1 / 2 / 2
convert cos_sq (π / 6) using 3
case h.e'_3.h.e'_6.h.e'_5
x : ℝ
h2 : 2 * (π / 6) = π / 3
⊢ 1 / 2 = cos (2 * (π / 6))
case h.e'_3.h.e'_6.h.e'_5
x : ℝ
⊢ 1 / 2 = cos (2 * (π / 6))
have h2 : 2 * (π / 6) = π / 3 := by linarith
no goals
case h.e'_3.h.e'_6.h.e'_5
x : ℝ
h2 : 2 * (π / 6) = π / 3
⊢ 1 / 2 = cos (2 * (π / 6))
rw [h2, cos_pi_div_three]
no goals
x : ℝ
⊢ 2 * (π / 6) = π / 3
linarith