-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_pi_div_five : cos (π / 5) = (1 + √5) / 4

Proof state:
c : ℝ := cos (π / 5)
⊢ 4 * c ^ 2 - 2 * c - 1 = 0

Tactic:
exact quadratic_root_cos_pi_div_five

Result:
no goals

Proof state:
⊢ cos (π / 5) = (1 + √5) / 4

Tactic:
set c := cos (π / 5)

Result:
c : ℝ := cos (π / 5)
⊢ c = (1 + √5) / 4

Proof state:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 - 2 * √5) / (2 * 4)
⊢ - -2 - 2 * √5 < 0

Tactic:
norm_num [lt_sqrt]

Result:
no goals

Proof state:
c : ℝ := cos (π / 5)
⊢ c = (1 + √5) / 4

Tactic:
have : 4 * (c * c) + (-2) * c + (-1) = 0 := by
  rw [← sq, neg_mul, ← sub_eq_add_neg, ← sub_eq_add_neg]
  exact quadratic_root_cos_pi_div_five

Result:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
⊢ c = (1 + √5) / 4

Proof state:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
⊢ c = (1 + √5) / 4

Tactic:
have hd : discrim 4 (-2) (-1) = (2 * √5) * (2 * √5) := by norm_num [discrim, mul_mul_mul_comm]

Result:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
⊢ c = (1 + √5) / 4

Proof state:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 - 2 * √5) / (2 * 4)
⊢ π / 5 ∈ Icc (-(π / 2)) (π / 2)

Tactic:
constructor <;> linarith [pi_pos.le]

Result:
no goals

Proof state:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
⊢ c = (1 + √5) / 4

Tactic:
rcases (quadratic_eq_zero_iff (by norm_num) hd c).mp this with h | h

Result:
case inl
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 + 2 * √5) / (2 * 4)
⊢ c = (1 + √5) / 4

case inr
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 - 2 * √5) / (2 * 4)
⊢ c = (1 + √5) / 4

Proof state:
case inr
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 - 2 * √5) / (2 * 4)
⊢ (- -2 - 2 * √5) / (2 * 4) < 0

Tactic:
exact div_neg_of_neg_of_pos (by norm_num [lt_sqrt]) (by positivity)

Result:
no goals

Proof state:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
⊢ discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)

Tactic:
norm_num [discrim, mul_mul_mul_comm]

Result:
no goals

Proof state:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 - 2 * √5) / (2 * 4)
⊢ 0 < 2 * 4

Tactic:
positivity

Result:
no goals

Proof state:
case inl
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 + 2 * √5) / (2 * 4)
⊢ (2 + 2 * √5) * 4 = (1 + √5) * (2 * 4)

Tactic:
linarith

Result:
no goals

Proof state:
case inl
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 + 2 * √5) / (2 * 4)
⊢ c = (1 + √5) / 4

Tactic:
field_simp [h]

Result:
case inl
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 + 2 * √5) / (2 * 4)
⊢ (2 + 2 * √5) * 4 = (1 + √5) * (2 * 4)

Proof state:
c : ℝ := cos (π / 5)
⊢ 4 * (c * c) + -2 * c + -1 = 0

Tactic:
rw [← sq, neg_mul, ← sub_eq_add_neg, ← sub_eq_add_neg]

Result:
c : ℝ := cos (π / 5)
⊢ 4 * c ^ 2 - 2 * c - 1 = 0

Proof state:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
⊢ 4 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
case inr
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 - 2 * √5) / (2 * 4)
⊢ ¬0 ≤ c

Tactic:
rw [not_le, h]

Result:
case inr
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 - 2 * √5) / (2 * 4)
⊢ (- -2 - 2 * √5) / (2 * 4) < 0

Proof state:
case inr
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 - 2 * √5) / (2 * 4)
⊢ c = (1 + √5) / 4

Tactic:
absurd (show 0 ≤ c from cos_nonneg_of_mem_Icc <| by constructor <;> linarith [pi_pos.le])

Result:
case inr
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 - 2 * √5) / (2 * 4)
⊢ ¬0 ≤ c