x : ℝ
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
⊢ cos (π / 3) = 1 / 2
x : ℝ
⊢ cos (π / 3) = 1 / 2
have h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0 := by
  have : cos (3 * (π / 3)) = cos π := by
    congr 1
    ring
  linarith [cos_pi, cos_three_mul (π / 3)]
case inl
x : ℝ
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : (2 * cos (π / 3) - 1) ^ 2 = 0
⊢ cos (π / 3) = 1 / 2

case inr
x : ℝ
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
⊢ cos (π / 3) = 1 / 2
x : ℝ
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
⊢ cos (π / 3) = 1 / 2
cases' mul_eq_zero.mp h₁ with h h
x : ℝ
this : cos (3 * (π / 3)) = cos π
⊢ (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
x : ℝ
⊢ (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
have : cos (3 * (π / 3)) = cos π := by
  congr 1
  ring
no goals
x : ℝ
this : cos (3 * (π / 3)) = cos π
⊢ (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
linarith [cos_pi, cos_three_mul (π / 3)]
case e_x
x : ℝ
⊢ 3 * (π / 3) = π
x : ℝ
⊢ cos (3 * (π / 3)) = cos π
congr 1
no goals
case e_x
x : ℝ
⊢ 3 * (π / 3) = π
ring
no goals
case inl
x : ℝ
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : (2 * cos (π / 3) - 1) ^ 2 = 0
⊢ cos (π / 3) = 1 / 2
linarith [pow_eq_zero h]
case inr
x : ℝ
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
this : cos π < cos (π / 3)
⊢ cos (π / 3) = 1 / 2
case inr
x : ℝ
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
⊢ cos (π / 3) = 1 / 2
have : cos π < cos (π / 3) := by
  refine' cos_lt_cos_of_nonneg_of_le_pi _ rfl.ge _ <;> linarith [pi_pos]
no goals
case inr
x : ℝ
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
this : cos π < cos (π / 3)
⊢ cos (π / 3) = 1 / 2
linarith [cos_pi]
no goals
x : ℝ
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
⊢ cos π < cos (π / 3)
refine' cos_lt_cos_of_nonneg_of_le_pi _ rfl.ge _ <;> linarith [pi_pos]