awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
r : R
hr : IsUnit r
a : ∀ (a : R), Multiset.count a (p.scaleRoots r).roots = Multiset.count a (Multiset.map (fun (x : R) ↦ r * x) p.roots)
⊢ (p.scaleRoots r).roots = Multiset.map (fun (x : R) ↦ r * x) p.roots
have a₁ : ∀ (a : R) (this : Function.Bijective (β := R) fun (x : R) ↦ r * x),
  Multiset.count a (p.scaleRoots r).roots = Multiset.count a (Multiset.map (fun (x : R) ↦ r * x) p.roots)
Tactic: classical
  ext a
  have : Function.Bijective (α := R) (r * ·) := IsUnit.isUnit_iff_mulLeft_bijective.mp hr
  obtain ⟨a, rfl⟩ := this.2 a
  simp [Multiset.count_map_eq_count' _ p.roots this.1 a,
    rootMultiplicity_scaleRoots _ hr.isRegular.left]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
r : R
hr : IsUnit r
a : ∀ (a : R), Multiset.count a (p.scaleRoots r).roots = Multiset.count a (Multiset.map (fun (x : R) ↦ r * x) p.roots)
a₁ :
  ∀ (a : R) (this : Function.Bijective (β := R) fun (x : R) ↦ r * x),
    Multiset.count a (p.scaleRoots r).roots = Multiset.count a (Multiset.map (fun (x : R) ↦ r * x) p.roots)
⊢ (p.scaleRoots r).roots = Multiset.map (fun (x : R) ↦ r * x) p.roots
have a₂ : ∀ (this : Function.Bijective (β := R) fun (x : R) ↦ r * x) (a : R),
  Multiset.count ((fun (x : R) ↦ r * x) a) (p.scaleRoots r).roots =
    Multiset.count (α := R) ((fun (x : R) ↦ r * x) a) (Multiset.map (fun (x : R) ↦ r * x) p.roots)
Tactic: classical
  ext a
  have : Function.Bijective (α := R) (r * ·) := IsUnit.isUnit_iff_mulLeft_bijective.mp hr
  obtain ⟨a, rfl⟩ := this.2 a
  simp [Multiset.count_map_eq_count' _ p.roots this.1 a,
    rootMultiplicity_scaleRoots _ hr.isRegular.left]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (hypothesis)
Goal:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0
⊢ False
have h3 : HPow.hPow (β := ℕ) z 3 = 1
Tactic: replace h3 : z ^ 3 = 1 := by
    linear_combination (1 - z - z ^ 2 - z ^ n) * h1 + (z ^ n - 2) * h2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0
h3 : HPow.hPow (β := ℕ) z 3 = 1
⊢ z ^ n = 1 ∨ z ^ n = z ∨ z ^ n = HPow.hPow (β := ℕ) z 2
have rw : z ^ (n % 3) = 1 ∨ z ^ (n % 3) = z ∨ z ^ (n % 3) = HPow.hPow (β := ℕ) z 2
Tactic: rw [← Nat.mod_add_div n 3, pow_add, pow_mul, h3, one_pow, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (hypothesis)
Goal:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0
h3 : HPow.hPow (β := ℕ) z 3 = 1
⊢ z ^ (n % 3) = 1 ∨ z ^ (n % 3) = z ∨ z ^ (n % 3) = HPow.hPow (β := ℕ) z 2
have this : n % 3 < 3
Tactic: have : n % 3 < 3 := Nat.mod_lt n zero_lt_three
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0
h3 : HPow.hPow (β := ℕ) z 3 = 1
this : n % 3 < 3
⊢ z ^ (n % 3) = 1 ∨ z ^ (n % 3) = z ∨ z ^ (n % 3) = HPow.hPow (β := ℕ) z 2
have 0 : ∀ (this : LT.lt (α := ℕ) 0 3),
  HPow.hPow (β := ℕ) z 0 = 1 ∨ HPow.hPow (β := ℕ) z 0 = z ∨ HPow.hPow (β := ℕ) z 0 = HPow.hPow (β := ℕ) z 2
Tactic: interval_cases n % 3
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0
h3 : HPow.hPow (β := ℕ) z 3 = 1
this : n % 3 < 3
0 :
  ∀ (this : LT.lt (α := ℕ) 0 3),
    HPow.hPow (β := ℕ) z 0 = 1 ∨ HPow.hPow (β := ℕ) z 0 = z ∨ HPow.hPow (β := ℕ) z 0 = HPow.hPow (β := ℕ) z 2
⊢ z ^ (n % 3) = 1 ∨ z ^ (n % 3) = z ∨ z ^ (n % 3) = HPow.hPow (β := ℕ) z 2
have 1 : ∀ (this : LT.lt (α := ℕ) 1 3),
  HPow.hPow (β := ℕ) z 1 = 1 ∨ HPow.hPow (β := ℕ) z 1 = z ∨ HPow.hPow (β := ℕ) z 1 = HPow.hPow (β := ℕ) z 2
Tactic: interval_cases n % 3
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0
h3 : HPow.hPow (β := ℕ) z 3 = 1
this : n % 3 < 3
0 :
  ∀ (this : LT.lt (α := ℕ) 0 3),
    HPow.hPow (β := ℕ) z 0 = 1 ∨ HPow.hPow (β := ℕ) z 0 = z ∨ HPow.hPow (β := ℕ) z 0 = HPow.hPow (β := ℕ) z 2
1 :
  ∀ (this : LT.lt (α := ℕ) 1 3),
    HPow.hPow (β := ℕ) z 1 = 1 ∨ HPow.hPow (β := ℕ) z 1 = z ∨ HPow.hPow (β := ℕ) z 1 = HPow.hPow (β := ℕ) z 2
⊢ z ^ (n % 3) = 1 ∨ z ^ (n % 3) = z ∨ z ^ (n % 3) = HPow.hPow (β := ℕ) z 2
have 2 : ∀ (this : LT.lt (α := ℕ) 2 3),
  HPow.hPow (β := ℕ) z 2 = 1 ∨ HPow.hPow (β := ℕ) z 2 = z ∨ HPow.hPow (β := ℕ) z 2 = HPow.hPow (β := ℕ) z 2
Tactic: interval_cases n % 3
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (hypothesis)
Goal:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0
h3 : HPow.hPow (β := ℕ) z 3 = 1
⊢ False
have key : z ^ n = 1 ∨ z ^ n = z ∨ z ^ n = HPow.hPow (β := ℕ) z 2
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 [pow_zero, pow_one, or_true, true_or]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (hypothesis)
Goal:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0
h3 : HPow.hPow (β := ℕ) z 3 = 1
key : z ^ n = 1 ∨ z ^ n = z ∨ z ^ n = HPow.hPow (β := ℕ) z 2
⊢ False
have z_ne_zero : z ≠ 0
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))
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0
h3 : HPow.hPow (β := ℕ) z 3 = 1
key : z ^ n = 1 ∨ z ^ n = z ∨ z ^ n = HPow.hPow (β := ℕ) z 2
z_ne_zero : z ≠ 0
⊢ False
have inl : ∀ (key : z ^ n = 1), False
Tactic: rcases key with (key | key | key)
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0
h3 : HPow.hPow (β := ℕ) z 3 = 1
key : z ^ n = 1 ∨ z ^ n = z ∨ z ^ n = HPow.hPow (β := ℕ) z 2
z_ne_zero : z ≠ 0
inl : ∀ (key : z ^ n = 1), False
⊢ False
have inr : ∀ (key : z ^ n = z), False
Tactic: rcases key with (key | key | key)
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0
h3 : HPow.hPow (β := ℕ) z 3 = 1
key : z ^ n = 1 ∨ z ^ n = z ∨ z ^ n = HPow.hPow (β := ℕ) z 2
z_ne_zero : z ≠ 0
inl : ∀ (key : z ^ n = 1), False
inr : ∀ (key : z ^ n = z), False
⊢ False
have inr₁ : ∀ (key : z ^ n = HPow.hPow (β := ℕ) z 2), False
Tactic: rcases key with (key | key | key)
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0
h3 : HPow.hPow (β := ℕ) z 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = 1
⊢ z = 0
have rwa : ∀ (h1 : 1 = z + 1) (h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0) (h3 : HPow.hPow (β := ℕ) z 3 = 1) (z_ne_zero : z ≠ 0)
  (key : z ^ n = 1), z = 0
Tactic: rwa [key, right_eq_add] at h1
Cleared hypotheses: h1, h2, h3, z_ne_zero, key
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0
h3 : HPow.hPow (β := ℕ) z 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = 1
rwa :
  ∀ (h1 : 1 = z + 1) (h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0) (h3 : HPow.hPow (β := ℕ) z 3 = 1) (z_ne_zero : z ≠ 0)
    (key : z ^ n = 1), z = 0
⊢ z = 0
have rwa₁ : ∀ (h1 : z = 0) (h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0) (h3 : HPow.hPow (β := ℕ) z 3 = 1) (z_ne_zero : z ≠ 0)
  (key : z ^ n = 1), z = 0
Tactic: rwa [key, right_eq_add] at h1
Cleared hypotheses: h1, h2, h3, z_ne_zero, key
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0
h3 : HPow.hPow (β := ℕ) z 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z
⊢ Eq (α := ℂ) 1 0
have rwa : ∀ (h1 : z = z + 1) (h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0) (h3 : HPow.hPow (β := ℕ) z 3 = 1) (z_ne_zero : z ≠ 0)
  (key : z ^ n = z), Eq (α := ℂ) 1 0
Tactic: rwa [key, left_eq_add] at h1
Cleared hypotheses: h2, h3, z_ne_zero, key
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0
h3 : HPow.hPow (β := ℕ) z 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z
rwa :
  ∀ (h1 : z = z + 1) (h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0) (h3 : HPow.hPow (β := ℕ) z 3 = 1) (z_ne_zero : z ≠ 0)
    (key : z ^ n = z), Eq (α := ℂ) 1 0
⊢ Eq (α := ℂ) 1 0
have rwa₁ : ∀ (h1 : Eq (α := ℂ) 1 0) (h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0) (h3 : HPow.hPow (β := ℕ) z 3 = 1) (z_ne_zero : z ≠ 0)
  (key : z ^ n = z), Eq (α := ℂ) 1 0
Tactic: rwa [key, left_eq_add] at h1
Cleared hypotheses: h2, h3, z_ne_zero, key
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0
h3 : HPow.hPow (β := ℕ) z 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = HPow.hPow (β := ℕ) z 2
⊢ HPow.hPow (β := ℕ) z 2 = 0
have rwa : ∀ (h2 : HPow.hPow (β := ℕ) z 2 + HPow.hPow (β := ℕ) z 2 = 0) (h3 : HPow.hPow (β := ℕ) z 3 = 1) (z_ne_zero : z ≠ 0)
  (key : z ^ n = HPow.hPow (β := ℕ) z 2), HPow.hPow (β := ℕ) z 2 = 0
Tactic: rwa [key, add_self_eq_zero] at h2
Cleared hypotheses: h3, z_ne_zero, key
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0
h3 : HPow.hPow (β := ℕ) z 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = HPow.hPow (β := ℕ) z 2
rwa :
  ∀ (h2 : HPow.hPow (β := ℕ) z 2 + HPow.hPow (β := ℕ) z 2 = 0) (h3 : HPow.hPow (β := ℕ) z 3 = 1) (z_ne_zero : z ≠ 0)
    (key : z ^ n = HPow.hPow (β := ℕ) z 2), HPow.hPow (β := ℕ) z 2 = 0
⊢ HPow.hPow (β := ℕ) z 2 = 0
have rwa₁ : ∀ (h2 : HPow.hPow (β := ℕ) z 2 = 0) (h3 : HPow.hPow (β := ℕ) z 3 = 1) (z_ne_zero : z ≠ 0)
  (key : z ^ n = HPow.hPow (β := ℕ) z 2), HPow.hPow (β := ℕ) z 2 = 0
Tactic: rwa [key, add_self_eq_zero] at h2
Cleared hypotheses: h3, z_ne_zero, key
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
hn1 : n ≠ 1
⊢ Irreducible (HPow.hPow (α := ℤ[X]) X n - X - 1)
have pos : ∀ (hn0 : n = 0), Irreducible (HPow.hPow (α := ℤ[X]) X n - X - 1)
Tactic: by_cases hn0 : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
hn1 : n ≠ 1
pos : ∀ (hn0 : n = 0), Irreducible (HPow.hPow (α := ℤ[X]) X n - X - 1)
⊢ Irreducible (HPow.hPow (α := ℤ[X]) X n - X - 1)
have neg : ∀ (hn0 : ¬n = 0), Irreducible (HPow.hPow (α := ℤ[X]) X n - X - 1)
Tactic: by_cases hn0 : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : n = 0
⊢ Irreducible (HPow.hPow (α := ℤ[X]) X n - X - 1)
have pos : Irreducible (M := ℤ[X]) (-X)
Tactic: rw [hn0, pow_zero, sub_sub, add_comm, ← sub_sub, sub_self, zero_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (hypothesis)
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
⊢ Irreducible (HPow.hPow (α := ℤ[X]) X n - X - 1)
have hn : 1 < n
Tactic: have hn : 1 < n := Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hn0, hn1⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
⊢ HPow.hPow (α := ℤ[X]) X n - X - 1 = trinomial 0 1 n (-1) (-1) 1
have simp : HPow.hPow (α := ℤ[X]) X n - X - 1 =
  -1 * HPow.hPow (α := ℤ[X]) (β := ℕ) X 0 + -1 * HPow.hPow (α := ℤ[X]) (β := ℕ) X 1 + 1 * HPow.hPow (α := ℤ[X]) X n
Tactic: simp only [trinomial, C_neg, C_1]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (hypothesis)
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
⊢ Irreducible (HPow.hPow (α := ℤ[X]) X n - X - 1)
have hp : HPow.hPow (α := ℤ[X]) X n - X - 1 = trinomial 0 1 n (-1) (-1) 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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : HPow.hPow (α := ℤ[X]) X n - X - 1 = trinomial 0 1 n (-1) (-1) 1
⊢ Irreducible (HPow.hPow (α := ℤ[X]) X n - X - 1)
have neg : Irreducible (M := ℤ[X]) (trinomial 0 1 n (-1) (-1) 1)
Tactic: rw [hp]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : HPow.hPow (α := ℤ[X]) X n - X - 1 = trinomial 0 1 n (-1) (-1) 1
⊢ Irreducible (M := ℤ[X]) (trinomial 0 1 n (-1) (-1) 1)
have neg : ∀ (z : ℂ),
  ¬(Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (trinomial 0 1 n (↑(-1) : ℤ) (↑(-1) : ℤ) (↑1 : ℤ)) : ℂ) (0 : ℂ) ∧
      Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (mirror (trinomial 0 1 n (↑(-1) : ℤ) (↑(-1) : ℤ) (↑1 : ℤ))) : ℂ) (0 : ℂ))
Tactic: apply IsUnitTrinomial.irreducible_of_coprime' ⟨0, 1, n, zero_lt_one, hn, -1, -1, 1, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : HPow.hPow (α := ℤ[X]) X n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (trinomial 0 1 n (↑(-1) : ℤ) (↑(-1) : ℤ) (↑1 : ℤ)) : ℂ) (0 : ℂ)
h2 : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (mirror (trinomial 0 1 n (↑(-1) : ℤ) (↑(-1) : ℤ) (↑1 : ℤ))) : ℂ) (0 : ℂ)
⊢ False
have neg : z ^ n = z + 1 ∧ z ^ n + HPow.hPow (β := ℕ) z 2 = 0
Tactic: apply X_pow_sub_X_sub_one_irreducible_aux (n := n) z
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (hypothesis)
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : HPow.hPow (α := ℤ[X]) X n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (trinomial 0 1 n (↑(-1) : ℤ) (↑(-1) : ℤ) (↑1 : ℤ)) : ℂ) (0 : ℂ)
h2 : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (mirror (trinomial 0 1 n (↑(-1) : ℤ) (↑(-1) : ℤ) (↑1 : ℤ))) : ℂ) (0 : ℂ)
⊢ z ^ n = z + 1 ∧ z ^ n + HPow.hPow (β := ℕ) z 2 = 0
have h2₁ : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (trinomial 0 (n - 1 + 0) n (↑1 : ℤ) (↑(-1) : ℤ) (↑(-1) : ℤ)) : ℂ) (0 : ℂ)
Tactic: rw [trinomial_mirror zero_lt_one hn (-1 : ℤˣ).ne_zero (1 : ℤˣ).ne_zero] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (hypothesis)
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : HPow.hPow (α := ℤ[X]) X n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (trinomial 0 1 n (↑(-1) : ℤ) (↑(-1) : ℤ) (↑1 : ℤ)) : ℂ) (0 : ℂ)
h2 : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (trinomial 0 (n - 1 + 0) n (↑1 : ℤ) (↑(-1) : ℤ) (↑(-1) : ℤ)) : ℂ) (0 : ℂ)
⊢ z ^ n = z + 1 ∧ z ^ n + HPow.hPow (β := ℕ) z 2 = 0
have h1₁ : -1 * HPow.hPow (β := ℕ) z 0 + -1 * HPow.hPow (β := ℕ) z 1 + 1 * z ^ n = 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
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (hypothesis)
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : HPow.hPow (α := ℤ[X]) X n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (trinomial 0 1 n (↑(-1) : ℤ) (↑(-1) : ℤ) (↑1 : ℤ)) : ℂ) (0 : ℂ)
h2 : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (trinomial 0 (n - 1 + 0) n (↑1 : ℤ) (↑(-1) : ℤ) (↑(-1) : ℤ)) : ℂ) (0 : ℂ)
h1₁ : -1 * HPow.hPow (β := ℕ) z 0 + -1 * HPow.hPow (β := ℕ) z 1 + 1 * z ^ n = 0
⊢ z ^ n = z + 1 ∧ z ^ n + HPow.hPow (β := ℕ) z 2 = 0
have h2₁ : 1 * HPow.hPow (β := ℕ) z 0 + -1 * z ^ (n - 1 + 0) + -1 * z ^ n = 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
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (hypothesis)
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : HPow.hPow (α := ℤ[X]) X n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : -1 * HPow.hPow (β := ℕ) z 0 + -1 * HPow.hPow (β := ℕ) z 1 + 1 * z ^ n = 0
h2 : 1 * HPow.hPow (β := ℕ) z 0 + -1 * z ^ (n - 1 + 0) + -1 * z ^ n = 0
⊢ z ^ n = z + 1 ∧ z ^ n + HPow.hPow (β := ℕ) z 2 = 0
have h1₁ : z ^ n = z + 1
Tactic: replace h1 : z ^ n = z + 1 := by linear_combination h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (hypothesis)
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : HPow.hPow (α := ℤ[X]) X n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h2 : 1 * HPow.hPow (β := ℕ) z 0 + -1 * z ^ (n - 1 + 0) + -1 * z ^ n = 0
h1 : z ^ n = z + 1
⊢ z ^ n = z + 1 ∧ z ^ n + HPow.hPow (β := ℕ) z 2 = 0
have h2₁ : (1 * HPow.hPow (β := ℕ) z 0 + -1 * z ^ (n - 1 + 0) + -1 * z ^ n) * z = 0
Tactic: replace h2 := mul_eq_zero_of_left h2 z
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (hypothesis)
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : HPow.hPow (α := ℤ[X]) X n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : z ^ n = z + 1
h2 : (1 * HPow.hPow (β := ℕ) z 0 + -1 * z ^ (n - 1 + 0) + -1 * z ^ n) * z = 0
⊢ z ^ n = z + 1 ∧ z ^ n + HPow.hPow (β := ℕ) z 2 = 0
have h2₁ : 1 * HPow.hPow (β := ℕ) z 0 * z + -1 * z ^ n + -1 * z ^ n * z = 0
Tactic: rw [add_mul, add_mul, add_zero, mul_assoc (-1 : ℂ), ← pow_succ, Nat.sub_add_cancel hn.le] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : HPow.hPow (α := ℤ[X]) X n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : z ^ n = z + 1
h2 : 1 * HPow.hPow (β := ℕ) z 0 * z + -1 * z ^ n + -1 * z ^ n * z = 0
⊢ z ^ n = z + 1 ∧ z ^ n + HPow.hPow (β := ℕ) z 2 = 0
have neg : ∀ (h2 : 1 * HPow.hPow (β := ℕ) z 0 * z + -1 * (z + 1) + -1 * (z + 1) * z = 0),
  z + 1 = z + 1 ∧ z + 1 + HPow.hPow (β := ℕ) z 2 = 0
Tactic: rw [h1] at h2 ⊢
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
hn1 : n ≠ 1
⊢ Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
have pos : ∀ (hn0 : n = 0), Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
Tactic: by_cases hn0 : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
hn1 : n ≠ 1
pos : ∀ (hn0 : n = 0), Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
⊢ Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
have neg : ∀ (hn0 : ¬n = 0), Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
Tactic: by_cases hn0 : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : n = 0
⊢ Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
have pos : Irreducible (M := ℚ[X]) (-X)
Tactic: rw [hn0, pow_zero, sub_sub, add_comm, ← sub_sub, sub_self, zero_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
⊢ HPow.hPow (α := ℤ[X]) X n - X - 1 = trinomial 0 1 n (-1) (-1) 1
have simp : HPow.hPow (α := ℤ[X]) X n - X - 1 =
  -1 * HPow.hPow (α := ℤ[X]) (β := ℕ) X 0 + -1 * HPow.hPow (α := ℤ[X]) (β := ℕ) X 1 + 1 * HPow.hPow (α := ℤ[X]) X n
Tactic: simp only [trinomial, C_neg, C_1]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (hypothesis)
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
⊢ Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
have hp : HPow.hPow (α := ℤ[X]) X n - X - 1 = trinomial 0 1 n (-1) (-1) 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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (hypothesis)
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : HPow.hPow (α := ℤ[X]) X n - X - 1 = trinomial 0 1 n (-1) (-1) 1
⊢ Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
have hn : 1 < n
Tactic: have hn : 1 < n := Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hn0, hn1⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : HPow.hPow (α := ℤ[X]) X n - X - 1 = trinomial 0 1 n (-1) (-1) 1
hn : 1 < n
⊢ Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
have neg : ∀ (h : Irreducible (map (Int.castRingHom ℚ) (HPow.hPow (α := ℤ[X]) X n - X - 1))),
  Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
Tactic: have h := (IsPrimitive.Int.irreducible_iff_irreducible_map_cast ?_).mp
    (X_pow_sub_X_sub_one_irreducible hn1)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : HPow.hPow (α := ℤ[X]) X n - X - 1 = trinomial 0 1 n (-1) (-1) 1
hn : 1 < n
neg :
  ∀ (h : Irreducible (map (Int.castRingHom ℚ) (HPow.hPow (α := ℤ[X]) X n - X - 1))),
    Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
⊢ Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
have neg₁ : (HPow.hPow (α := ℤ[X]) X n - X - 1).IsPrimitive
Tactic: have h := (IsPrimitive.Int.irreducible_iff_irreducible_map_cast ?_).mp
    (X_pow_sub_X_sub_one_irreducible hn1)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : HPow.hPow (α := ℤ[X]) X n - X - 1 = trinomial 0 1 n (-1) (-1) 1
hn : 1 < n
h : Irreducible (map (Int.castRingHom ℚ) (HPow.hPow (α := ℤ[X]) X n - X - 1))
⊢ Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
have neg : ∀ (h : Irreducible (map (Int.castRingHom ℚ) (HPow.hPow (α := ℤ[X]) X n - X) - map (Int.castRingHom ℚ) 1)),
  Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
Tactic: rwa [Polynomial.map_sub, Polynomial.map_sub, Polynomial.map_pow, Polynomial.map_one,
      Polynomial.map_X] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : HPow.hPow (α := ℤ[X]) X n - X - 1 = trinomial 0 1 n (-1) (-1) 1
hn : 1 < n
h : Irreducible (map (Int.castRingHom ℚ) (HPow.hPow (α := ℤ[X]) X n - X - 1))
neg :
  ∀ (h : Irreducible (map (Int.castRingHom ℚ) (HPow.hPow (α := ℤ[X]) X n - X) - map (Int.castRingHom ℚ) 1)),
    Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
⊢ Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
have neg₁ : ∀
  (h :
    Irreducible
      (map (Int.castRingHom ℚ) (HPow.hPow (α := ℤ[X]) X n) - map (Int.castRingHom ℚ) X - map (Int.castRingHom ℚ) 1)),
  Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
Tactic: rwa [Polynomial.map_sub, Polynomial.map_sub, Polynomial.map_pow, Polynomial.map_one,
      Polynomial.map_X] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : HPow.hPow (α := ℤ[X]) X n - X - 1 = trinomial 0 1 n (-1) (-1) 1
hn : 1 < n
h : Irreducible (map (Int.castRingHom ℚ) (HPow.hPow (α := ℤ[X]) X n - X - 1))
neg :
  ∀ (h : Irreducible (map (Int.castRingHom ℚ) (HPow.hPow (α := ℤ[X]) X n - X) - map (Int.castRingHom ℚ) 1)),
    Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
neg₁ :
  ∀
    (h :
      Irreducible
        (map (Int.castRingHom ℚ) (HPow.hPow (α := ℤ[X]) X n) - map (Int.castRingHom ℚ) X - map (Int.castRingHom ℚ) 1)),
    Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
⊢ Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
have neg₂ : ∀ (h : Irreducible (map (Int.castRingHom ℚ) X ^ n - map (Int.castRingHom ℚ) X - map (Int.castRingHom ℚ) 1)),
  Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
Tactic: rwa [Polynomial.map_sub, Polynomial.map_sub, Polynomial.map_pow, Polynomial.map_one,
      Polynomial.map_X] at h
Cleared hypotheses: h