x : ℝ
⊢ sqrt 3 = cos (π / 6) * 2
x : ℝ
⊢ cos (π / 6) = sqrt 3 / 2
suffices sqrt 3 = cos (π / 6) * 2 by
  field_simp [(by norm_num : 0 ≠ 2)]
  exact this.symm
x : ℝ
⊢ (cos (π / 6) * 2) ^ 2 = 3

case hx
x : ℝ
⊢ 0 ≤ 3

case hy
x : ℝ
⊢ 0 ≤ cos (π / 6) * 2
x : ℝ
⊢ sqrt 3 = cos (π / 6) * 2
rw [sqrt_eq_iff_sq_eq]
x : ℝ
this : sqrt 3 = cos (π / 6) * 2
⊢ cos (π / 6) * 2 = sqrt 3
x : ℝ
this : sqrt 3 = cos (π / 6) * 2
⊢ cos (π / 6) = sqrt 3 / 2
field_simp [(by norm_num : 0 ≠ 2)]
no goals
x : ℝ
this : sqrt 3 = cos (π / 6) * 2
⊢ cos (π / 6) * 2 = sqrt 3
exact this.symm
no goals
x : ℝ
this : sqrt 3 = cos (π / 6) * 2
⊢ 0 ≠ 2
norm_num
x : ℝ
h1 : 4 * cos (π / 6) ^ 2 = 4 * (3 / 4)
⊢ (cos (π / 6) * 2) ^ 2 = 3
x : ℝ
⊢ (cos (π / 6) * 2) ^ 2 = 3
have h1 := (mul_right_inj' (by norm_num : (4 : ℝ) ≠ 0)).mpr sq_cos_pi_div_six
x : ℝ
h1✝ : 4 * cos (π / 6) ^ 2 = 4 * (3 / 4)
h1 : 4 * cos (π / 6) ^ 2 - 4 * (3 / 4) = 0
⊢ (cos (π / 6) * 2) ^ 2 - 3 = 0
x : ℝ
h1 : 4 * cos (π / 6) ^ 2 = 4 * (3 / 4)
⊢ (cos (π / 6) * 2) ^ 2 = 3
rw [← sub_eq_zero] at h1⊢
case h.e'_2
x : ℝ
h1✝ : 4 * cos (π / 6) ^ 2 = 4 * (3 / 4)
h1 : 4 * cos (π / 6) ^ 2 - 4 * (3 / 4) = 0
⊢ (cos (π / 6) * 2) ^ 2 - 3 = 4 * cos (π / 6) ^ 2 - 4 * (3 / 4)
x : ℝ
h1✝ : 4 * cos (π / 6) ^ 2 = 4 * (3 / 4)
h1 : 4 * cos (π / 6) ^ 2 - 4 * (3 / 4) = 0
⊢ (cos (π / 6) * 2) ^ 2 - 3 = 0
convert h1 using 1
no goals
case h.e'_2
x : ℝ
h1✝ : 4 * cos (π / 6) ^ 2 = 4 * (3 / 4)
h1 : 4 * cos (π / 6) ^ 2 - 4 * (3 / 4) = 0
⊢ (cos (π / 6) * 2) ^ 2 - 3 = 4 * cos (π / 6) ^ 2 - 4 * (3 / 4)
ring
no goals
x : ℝ
⊢ 4 ≠ 0
norm_num
no goals
case hx
x : ℝ
⊢ 0 ≤ 3
norm_num
case hy
x : ℝ
this : 0 < cos (π / 6)
⊢ 0 ≤ cos (π / 6) * 2
case hy
x : ℝ
⊢ 0 ≤ cos (π / 6) * 2
have : 0 < cos (π / 6) := by apply cos_pos_of_mem_Ioo; constructor <;> linarith [pi_pos]
no goals
case hy
x : ℝ
this : 0 < cos (π / 6)
⊢ 0 ≤ cos (π / 6) * 2
linarith
case hx
x : ℝ
⊢ π / 6 ∈ Ioo (-(π / 2)) (π / 2)
x : ℝ
⊢ 0 < cos (π / 6)
apply cos_pos_of_mem_Ioo
no goals
case hx
x : ℝ
⊢ π / 6 ∈ Ioo (-(π / 2)) (π / 2)
constructor <;> linarith [pi_pos]