-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem quadratic_root_cos_pi_div_five :
    letI c := cos (π / 5)
    4 * c ^ 2 - 2 * c - 1 = 0

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

Tactic:
set s := sin θ

Result:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
⊢ 4 * c ^ 2 - 2 * c - 1 = 0

Proof state:
θ : ℝ := π / 5
hθ : θ = π / 5
⊢ 4 * cos θ ^ 2 - 2 * cos θ - 1 = 0

Tactic:
set c := cos θ

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

Proof state:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ s * (2 * c * c) + s * (2 * c ^ 2 - 1) = s * (4 * c ^ 2 - 1)

Tactic:
linarith

Result:
no goals

Proof state:
case e_x
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ π * 5 - 2 * π = 2 * π + π

Tactic:
linarith

Result:
no goals

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

Tactic:
set θ := π / 5 with hθ

Result:
θ : ℝ := π / 5
hθ : θ = π / 5
⊢ 4 * cos θ ^ 2 - 2 * cos θ - 1 = 0

Proof state:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ 2 * s * c = sin (2 * θ)

Tactic:
rw [sin_two_mul]

Result:
no goals

Proof state:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
n : ℤ
hn : ↑n * π = π / 5
⊢ False

Tactic:
replace hn : n * 5 = 1 := by field_simp [mul_comm _ π, mul_assoc] at hn; norm_cast at hn

Result:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
n : ℤ
hn : n * 5 = 1
⊢ False

Proof state:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
⊢ s ≠ 0

Tactic:
rw [ne_eq, sin_eq_zero_iff, hθ]

Result:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
⊢ ¬∃ n, ↑n * π = π / 5

Proof state:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
n : ℤ
hn : n * 5 = 1
⊢ False

Tactic:
omega

Result:
no goals

Proof state:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
⊢ 4 * c ^ 2 - 2 * c - 1 = 0

Tactic:
suffices 2 * c = 4 * c ^ 2 - 1 by simp [this]

Result:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
⊢ 2 * c = 4 * c ^ 2 - 1

Proof state:
case e_x
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ π - 2 * θ = 2 * θ + θ

Tactic:
field_simp [hθ]

Result:
case e_x
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ π * 5 - 2 * π = 2 * π + π

Proof state:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ s * (2 * c) = s * (4 * c ^ 2 - 1)

Tactic:
calc s * (2 * c) = 2 * s * c := by rw [← mul_assoc, mul_comm 2]
               _ = sin (2 * θ) := by rw [sin_two_mul]
               _ = sin (π - 2 * θ) := by rw [sin_pi_sub]
               _ = sin (2 * θ + θ) := by congr; field_simp [hθ]; linarith
               _ = sin (2 * θ) * c + cos (2 * θ) * s := sin_add (2 * θ) θ
               _ = 2 * s * c * c + cos (2 * θ) * s := by rw [sin_two_mul]
               _ = 2 * s * c * c + (2 * c ^ 2 - 1) * s := by rw [cos_two_mul]
               _ = s * (2 * c * c) + s * (2 * c ^ 2 - 1) := by linarith
               _ = s * (4 * c ^ 2 - 1) := by linarith

Result:
no goals

Proof state:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
⊢ 2 * c = 4 * c ^ 2 - 1

Tactic:
have hs : s ≠ 0 := by
  rw [ne_eq, sin_eq_zero_iff, hθ]
  push_neg
  intro n hn
  replace hn : n * 5 = 1 := by field_simp [mul_comm _ π, mul_assoc] at hn; norm_cast at hn
  omega

Result:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ 2 * c = 4 * c ^ 2 - 1

Proof state:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
this : 2 * c = 4 * c ^ 2 - 1
⊢ 4 * c ^ 2 - 2 * c - 1 = 0

Tactic:
simp [this]

Result:
no goals

Proof state:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
n : ℤ
hn : ↑n * π = π / 5
⊢ n * 5 = 1

Tactic:
field_simp [mul_comm _ π, mul_assoc] at hn

Result:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
n : ℤ
hn : ↑n * 5 = 1
⊢ n * 5 = 1

Proof state:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ sin (2 * θ) * c + cos (2 * θ) * s = 2 * s * c * c + cos (2 * θ) * s

Tactic:
rw [sin_two_mul]

Result:
no goals

Proof state:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ s * (2 * c) = 2 * s * c

Tactic:
rw [← mul_assoc, mul_comm 2]

Result:
no goals

Proof state:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
⊢ ¬∃ n, ↑n * π = π / 5

Tactic:
push_neg

Result:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
⊢ ∀ (n : ℤ), ↑n * π ≠ π / 5

Proof state:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ sin (2 * θ) = sin (π - 2 * θ)

Tactic:
rw [sin_pi_sub]

Result:
no goals

Proof state:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ 2 * s * c * c + (2 * c ^ 2 - 1) * s = s * (2 * c * c) + s * (2 * c ^ 2 - 1)

Tactic:
linarith

Result:
no goals

Proof state:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ sin (π - 2 * θ) = sin (2 * θ + θ)

Tactic:
congr

Result:
case e_x
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ π - 2 * θ = 2 * θ + θ

Proof state:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ 2 * s * c * c + cos (2 * θ) * s = 2 * s * c * c + (2 * c ^ 2 - 1) * s

Tactic:
rw [cos_two_mul]

Result:
no goals

Proof state:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ 2 * c = 4 * c ^ 2 - 1

Tactic:
suffices s * (2 * c) = s * (4 * c ^ 2 - 1) from mul_left_cancel₀ hs this

Result:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ s * (2 * c) = s * (4 * c ^ 2 - 1)

Proof state:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
n : ℤ
hn : ↑n * 5 = 1
⊢ n * 5 = 1

Tactic:
norm_cast at hn

Result:
no goals

Proof state:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
⊢ ∀ (n : ℤ), ↑n * π ≠ π / 5

Tactic:
intro n hn

Result:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
n : ℤ
hn : ↑n * π = π / 5
⊢ False