-- Mathlib/RingTheory/Polynomial/Selmer.lean
theorem X_pow_sub_X_sub_one_irreducible_aux (z : ℂ) : ¬(z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0)

Proof state:
case intro
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
⊢ False

Tactic:
have key : z ^ n = 1 ∨ z ^ n = z ∨ z ^ n = z ^ 2 := by
  rw [← Nat.mod_add_div n 3, pow_add, pow_mul, h3, one_pow, mul_one]
  have : n % 3 < 3 := Nat.mod_lt n zero_lt_three
  interval_cases n % 3 <;>
  simp only [this, pow_zero, pow_one, eq_self_iff_true, or_true, true_or]

Result:
case intro
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
key : z ^ n = 1 ∨ z ^ n = z ∨ z ^ n = z ^ 2
⊢ False

Proof state:
case intro
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
⊢ False

Tactic:
replace h3 : z ^ 3 = 1 := by
  linear_combination (1 - z - z ^ 2 - z ^ n) * h1 + (z ^ n - 2) * h2

Result:
case intro
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
⊢ False

Proof state:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z ^ 2
⊢ z ^ ?m.8597 = 0

Tactic:
rwa [key, add_self_eq_zero] at h2

Result:
no goals

Proof state:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
⊢ z ^ (n % 3) = 1 ∨ z ^ (n % 3) = z ∨ z ^ (n % 3) = z ^ 2

Tactic:
have : n % 3 < 3 := Nat.mod_lt n zero_lt_three

Result:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
this : n % 3 < 3
⊢ z ^ (n % 3) = 1 ∨ z ^ (n % 3) = z ∨ z ^ (n % 3) = z ^ 2

Proof state:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
⊢ z ^ 3 = 1

Tactic:
linear_combination (1 - z - z ^ 2 - z ^ n) * h1 + (z ^ n - 2) * h2

Result:
no goals

Proof state:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
⊢ z ^ n = 1 ∨ z ^ n = z ∨ z ^ n = z ^ 2

Tactic:
rw [← Nat.mod_add_div n 3, pow_add, pow_mul, h3, one_pow, mul_one]

Result:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
⊢ z ^ (n % 3) = 1 ∨ z ^ (n % 3) = z ∨ z ^ (n % 3) = z ^ 2

Proof state:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
this : n % 3 < 3
⊢ z ^ (n % 3) = 1 ∨ z ^ (n % 3) = z ∨ z ^ (n % 3) = z ^ 2

Tactic:
interval_cases n % 3 <;>
simp only [this, pow_zero, pow_one, eq_self_iff_true, or_true, true_or]

Result:
no goals

Proof state:
case intro
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
key : z ^ n = 1 ∨ z ^ n = z ∨ z ^ n = z ^ 2
z_ne_zero : z ≠ 0
⊢ False

Tactic:
rcases key with (key | key | key)

Result:
case intro.inl
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = 1
⊢ False

case intro.inr.inl
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z
⊢ False

case intro.inr.inr
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z ^ 2
⊢ False

Proof state:
case intro.inr.inl
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z
⊢ False

Tactic:
exact one_ne_zero (by rwa [key, self_eq_add_right] at h1)

Result:
no goals

Proof state:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z
⊢ 1 = 0

Tactic:
rwa [key, self_eq_add_right] at h1

Result:
no goals

Proof state:
case intro.inl
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = 1
⊢ False

Tactic:
exact z_ne_zero (by rwa [key, self_eq_add_left] at h1)

Result:
no goals

Proof state:
case intro
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
key : z ^ n = 1 ∨ z ^ n = z ∨ z ^ n = z ^ 2
⊢ False

Tactic:
have z_ne_zero : z ≠ 0 := fun h =>
  zero_ne_one ((zero_pow three_ne_zero).symm.trans (show (0 : ℂ) ^ 3 = 1 from h ▸ h3))

Result:
case intro
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
key : z ^ n = 1 ∨ z ^ n = z ∨ z ^ n = z ^ 2
z_ne_zero : z ≠ 0
⊢ False

Proof state:
n : ℕ
z : ℂ
⊢ ¬(z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0)

Tactic:
rintro ⟨h1, h2⟩

Result:
case intro
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
⊢ False

Proof state:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = 1
⊢ z = 0

Tactic:
rwa [key, self_eq_add_left] at h1

Result:
no goals

Proof state:
case intro.inr.inr
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z ^ 2
⊢ False

Tactic:
exact z_ne_zero (pow_eq_zero (by rwa [key, add_self_eq_zero] at h2))

Result:
no goals