-- Mathlib/RingTheory/Polynomial/Selmer.lean
theorem X_pow_sub_X_sub_one_irreducible (hn1 : n ≠ 1) : Irreducible (X ^ n - X - 1 : ℤ[X])

Proof state:
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
⊢ Irreducible (X ^ n - X - 1)

Tactic:
have hn : 1 < n := Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hn0, hn1⟩

Result:
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
⊢ Irreducible (X ^ n - X - 1)

Proof state:
n : ℕ
hn1 : n ≠ 1
⊢ Irreducible (X ^ n - X - 1)

Tactic:
by_cases hn0 : n = 0

Result:
case pos
n : ℕ
hn1 : n ≠ 1
hn0 : n = 0
⊢ Irreducible (X ^ n - X - 1)

case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
⊢ Irreducible (X ^ n - X - 1)

Proof state:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
⊢ X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1

Tactic:
simp only [trinomial, C_neg, C_1]

Result:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
⊢ X ^ n - X - 1 = -1 * X ^ 0 + -1 * X ^ 1 + 1 * X ^ n

Proof state:
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
⊢ Irreducible (trinomial 0 1 n (-1) (-1) 1)

Tactic:
apply IsUnitTrinomial.irreducible_of_coprime' ⟨0, 1, n, zero_lt_one, hn, -1, -1, 1, rfl⟩

Result:
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
⊢ ∀ (z : ℂ), ¬((aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0 ∧ (aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1).mirror = 0)

Proof state:
case pos
n : ℕ
hn1 : n ≠ 1
hn0 : n = 0
⊢ Irreducible (-X)

Tactic:
exact Associated.irreducible ⟨-1, mul_neg_one X⟩ irreducible_X

Result:
no goals

Proof state:
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : (aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0
h2 : (aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1).mirror = 0
⊢ z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0

Tactic:
rw [trinomial_mirror zero_lt_one hn (-1 : ℤˣ).ne_zero (1 : ℤˣ).ne_zero] at h2

Result:
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : (aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0
h2 : (aeval z) (trinomial 0 (n - 1 + 0) n ↑1 ↑(-1) ↑(-1)) = 0
⊢ z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0

Proof state:
case pos
n : ℕ
hn1 : n ≠ 1
hn0 : n = 0
⊢ Irreducible (X ^ n - X - 1)

Tactic:
rw [hn0, pow_zero, sub_sub, add_comm, ← sub_sub, sub_self, zero_sub]

Result:
case pos
n : ℕ
hn1 : n ≠ 1
hn0 : n = 0
⊢ Irreducible (-X)

Proof state:
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
⊢ ∀ (z : ℂ), ¬((aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0 ∧ (aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1).mirror = 0)

Tactic:
rintro z ⟨h1, h2⟩

Result:
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : (aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0
h2 : (aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1).mirror = 0
⊢ False

Proof state:
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h2 : 1 * z ^ 0 + -1 * z ^ (n - 1 + 0) + -1 * z ^ n = 0
h1 : z ^ n = z + 1
⊢ z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0

Tactic:
replace h2 := mul_eq_zero_of_left h2 z

Result:
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : z ^ n = z + 1
h2 : (1 * z ^ 0 + -1 * z ^ (n - 1 + 0) + -1 * z ^ n) * z = 0
⊢ z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0

Proof state:
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
⊢ Irreducible (X ^ n - X - 1)

Tactic:
rw [hp]

Result:
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
⊢ Irreducible (trinomial 0 1 n (-1) (-1) 1)

Proof state:
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : z ^ n = z + 1
h2 : 1 * z ^ 0 * z + -1 * (z + 1) + -1 * (z + 1) * z = 0
⊢ z + 1 = z + 1 ∧ z + 1 + z ^ 2 = 0

Tactic:
exact ⟨rfl, by linear_combination -h2⟩

Result:
no goals

Proof state:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : -1 * z ^ 0 + -1 * z ^ 1 + 1 * z ^ n = 0
h2 : 1 * z ^ 0 + -1 * z ^ (n - 1 + 0) + -1 * z ^ n = 0
⊢ z ^ n = z + 1

Tactic:
linear_combination h1

Result:
no goals

Proof state:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
⊢ X ^ n - X - 1 = -1 * X ^ 0 + -1 * X ^ 1 + 1 * X ^ n

Tactic:
ring

Result:
no goals

Proof state:
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : (aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0
h2 : (aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1).mirror = 0
⊢ False

Tactic:
apply X_pow_sub_X_sub_one_irreducible_aux (n := n) z

Result:
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : (aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0
h2 : (aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1).mirror = 0
⊢ z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0

Proof state:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : z ^ n = z + 1
h2 : 1 * z ^ 0 * z + -1 * (z + 1) + -1 * (z + 1) * z = 0
⊢ z + 1 + z ^ 2 = 0

Tactic:
linear_combination -h2

Result:
no goals

Proof state:
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : z ^ n = z + 1
h2 : (1 * z ^ 0 + -1 * z ^ (n - 1 + 0) + -1 * z ^ n) * z = 0
⊢ z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0

Tactic:
rw [add_mul, add_mul, add_zero, mul_assoc (-1 : ℂ), ← pow_succ, Nat.sub_add_cancel hn.le] at h2

Result:
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : z ^ n = z + 1
h2 : 1 * z ^ 0 * z + -1 * z ^ n + -1 * z ^ n * z = 0
⊢ z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0

Proof state:
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : z ^ n = z + 1
h2 : 1 * z ^ 0 * z + -1 * z ^ n + -1 * z ^ n * z = 0
⊢ z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0

Tactic:
rw [h1] at h2 ⊢

Result:
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : z ^ n = z + 1
h2 : 1 * z ^ 0 * z + -1 * (z + 1) + -1 * (z + 1) * z = 0
⊢ z + 1 = z + 1 ∧ z + 1 + z ^ 2 = 0

Proof state:
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : -1 * z ^ 0 + -1 * z ^ 1 + 1 * z ^ n = 0
h2 : 1 * z ^ 0 + -1 * z ^ (n - 1 + 0) + -1 * z ^ n = 0
⊢ z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0

Tactic:
replace h1 : z ^ n = z + 1 := by linear_combination h1

Result:
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h2 : 1 * z ^ 0 + -1 * z ^ (n - 1 + 0) + -1 * z ^ n = 0
h1 : z ^ n = z + 1
⊢ z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0

Proof state:
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : (aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0
h2 : (aeval z) (trinomial 0 (n - 1 + 0) n ↑1 ↑(-1) ↑(-1)) = 0
⊢ z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0

Tactic:
simp_rw [trinomial, aeval_add, aeval_mul, aeval_X_pow, aeval_C,
  Units.val_neg, Units.val_one, map_neg, map_one] at h1 h2

Result:
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : -1 * z ^ 0 + -1 * z ^ 1 + 1 * z ^ n = 0
h2 : 1 * z ^ 0 + -1 * z ^ (n - 1 + 0) + -1 * z ^ n = 0
⊢ z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0

Proof state:
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
⊢ Irreducible (X ^ n - X - 1)

Tactic:
have hp : (X ^ n - X - 1 : ℤ[X]) = trinomial 0 1 n (-1) (-1) 1 := by
  simp only [trinomial, C_neg, C_1]; ring

Result:
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
⊢ Irreducible (X ^ n - X - 1)