awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Selmer
Goal:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0
h3 : HPow.hPow (β := ℕ) z 3 = 1
⊢ n % 3 < 3

Tactic:
have : n % 3 < 3 := Nat.mod_lt n zero_lt_three
-- Module: Mathlib.RingTheory.Polynomial.Selmer
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
2 :
  ∀ (this : LT.lt (α := ℕ) 2 3),
    HPow.hPow (β := ℕ) z 2 = 1 ∨ HPow.hPow (β := ℕ) z 2 = z ∨ HPow.hPow (β := ℕ) z 2 = HPow.hPow (β := ℕ) z 2
⊢ z ^ (n % 3) = 1 ∨ z ^ (n % 3) = z ∨ z ^ (n % 3) = HPow.hPow (β := ℕ) z 2

Tactic:
interval_cases n % 3
-- Module: Mathlib.RingTheory.Polynomial.Selmer
Goal:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0
h3 : HPow.hPow (β := ℕ) z 3 = 1
this : LT.lt (α := ℕ) 0 3
⊢ HPow.hPow (β := ℕ) z 0 = 1 ∨ HPow.hPow (β := ℕ) z 0 = z ∨ HPow.hPow (β := ℕ) z 0 = HPow.hPow (β := ℕ) z 2

Tactic:
simp only [pow_zero, pow_one, or_true, true_or]

Premises used: true_or, pow_zero, pow_one, or_true
-- Module: Mathlib.RingTheory.Polynomial.Selmer
Goal:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0
h3 : HPow.hPow (β := ℕ) z 3 = 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:
simp only [pow_zero, pow_one, or_true, true_or]

Premises used: true_or, pow_zero, pow_one, or_true
-- Module: Mathlib.RingTheory.Polynomial.Selmer
Goal:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0
h3 : HPow.hPow (β := ℕ) z 3 = 1
this : LT.lt (α := ℕ) 2 3
⊢ HPow.hPow (β := ℕ) z 2 = 1 ∨ HPow.hPow (β := ℕ) z 2 = z ∨ HPow.hPow (β := ℕ) z 2 = HPow.hPow (β := ℕ) z 2

Tactic:
simp only [pow_zero, pow_one, or_true, true_or]

Premises used: true_or, pow_zero, pow_one, or_true
-- Module: Mathlib.RingTheory.Polynomial.Selmer
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

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]
-- Module: Mathlib.RingTheory.Polynomial.Selmer
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 ≠ 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))
-- Module: Mathlib.RingTheory.Polynomial.Selmer
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
inr₁ : ∀ (key : z ^ n = HPow.hPow (β := ℕ) z 2), False
⊢ False

Tactic:
rcases key with (key | key | key)
-- Module: Mathlib.RingTheory.Polynomial.Selmer
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
rwa₁ rwa₂ rwa₃ 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
⊢ z = 0

Tactic:
rwa [key, right_eq_add] at h1

Premises used: right_eq_add
-- Module: Mathlib.RingTheory.Polynomial.Selmer
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
⊢ False

Tactic:
exact z_ne_zero (by rwa [key, right_eq_add] at h1)
-- Module: Mathlib.RingTheory.Polynomial.Selmer
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
rwa₁ rwa₂ rwa₃ 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
⊢ Eq (α := ℂ) 1 0

Tactic:
rwa [key, left_eq_add] at h1

Premises used: left_eq_add
-- Module: Mathlib.RingTheory.Polynomial.Selmer
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
⊢ False

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

Premises used: one_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Selmer
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
rwa₁ rwa₂ rwa₃ 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
⊢ HPow.hPow (β := ℕ) z 2 = 0

Tactic:
rwa [key, add_self_eq_zero] at h2

Premises used: add_self_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.Selmer
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
⊢ False

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

Premises used: eq_zero_of_pow_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.Selmer
Goal:
n : ℕ
hn1 : n ≠ 1
pos : ∀ (hn0 : n = 0), Irreducible (HPow.hPow (α := ℤ[X]) X n - X - 1)
neg : ∀ (hn0 : ¬n = 0), Irreducible (HPow.hPow (α := ℤ[X]) X n - X - 1)
⊢ Irreducible (HPow.hPow (α := ℤ[X]) X n - X - 1)

Tactic:
by_cases hn0 : n = 0
-- Module: Mathlib.RingTheory.Polynomial.Selmer
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : n = 0
pos : Irreducible (M := ℤ[X]) (-X)
⊢ Irreducible (HPow.hPow (α := ℤ[X]) X n - X - 1)

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

Premises used: sub_self, add_comm, pow_zero, sub_sub, zero_sub
-- Module: Mathlib.RingTheory.Polynomial.Selmer
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : n = 0
⊢ Irreducible (M := ℤ[X]) (-X)

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

Premises used: Associated.irreducible, Exists.intro, Polynomial.irreducible_X, mul_neg_one, OfNat.ofNat, Polynomial.X, Neg.neg
-- Module: Mathlib.RingTheory.Polynomial.Selmer
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : n = 0
⊢ Irreducible (M := ℤ[X]) (-X)

Tactic:
exact Associated.irreducible ⟨-1, mul_neg_one X⟩ irreducible_X
-- Module: Mathlib.RingTheory.Polynomial.Selmer
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
⊢ 1 < n

Tactic:
have hn : 1 < n := Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hn0, hn1⟩
-- Module: Mathlib.RingTheory.Polynomial.Selmer
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
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
⊢ HPow.hPow (α := ℤ[X]) X n - X - 1 = trinomial 0 1 n (-1) (-1) 1

Tactic:
simp only [trinomial, C_neg, C_1]

Premises used: Polynomial.C_1, Polynomial.trinomial, Polynomial.C_neg
-- Module: Mathlib.RingTheory.Polynomial.Selmer
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
⊢ 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:
ring
-- Module: Mathlib.RingTheory.Polynomial.Selmer
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

Tactic:
have hp : (X ^ n - X - 1 : ℤ[X]) = trinomial 0 1 n (-1) (-1) 1 := by
    simp only [trinomial, C_neg, C_1]; ring
-- Module: Mathlib.RingTheory.Polynomial.Selmer
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
neg : Irreducible (M := ℤ[X]) (trinomial 0 1 n (-1) (-1) 1)
⊢ Irreducible (HPow.hPow (α := ℤ[X]) X n - X - 1)

Tactic:
rw [hp]
-- Module: Mathlib.RingTheory.Polynomial.Selmer
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
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 : ℂ))
⊢ Irreducible (M := ℤ[X]) (trinomial 0 1 n (-1) (-1) 1)

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

Premises used: zero_lt_one, Polynomial.IsUnitTrinomial.irreducible_of_coprime', Exists.intro, OfNat.ofNat, Neg.neg, rfl
-- Module: Mathlib.RingTheory.Polynomial.Selmer
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 : ℂ)
neg : z ^ n = z + 1 ∧ z ^ n + HPow.hPow (β := ℕ) z 2 = 0
⊢ False

Tactic:
apply X_pow_sub_X_sub_one_irreducible_aux (n := n) z

Premises used: Polynomial.X_pow_sub_X_sub_one_irreducible_aux
-- Module: Mathlib.RingTheory.Polynomial.Selmer
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 : ℂ)
⊢ 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

Premises used: Units.ne_zero, zero_lt_one, Polynomial.trinomial_mirror, OfNat.ofNat, Neg.neg
-- Module: Mathlib.RingTheory.Polynomial.Selmer
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 : ℂ)
⊢ -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

Premises used: Polynomial.trinomial, Polynomial.aeval_X_pow, map_neg, Polynomial.aeval_mul, Units.val_neg, map_one, Polynomial.aeval_C, Units.val_one, Polynomial.aeval_add
-- Module: Mathlib.RingTheory.Polynomial.Selmer
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
⊢ 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

Premises used: Polynomial.trinomial, Polynomial.aeval_X_pow, map_neg, Polynomial.aeval_mul, Units.val_neg, map_one, Polynomial.aeval_C, Units.val_one, Polynomial.aeval_add
-- Module: Mathlib.RingTheory.Polynomial.Selmer
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

Tactic:
linear_combination h1
-- Module: Mathlib.RingTheory.Polynomial.Selmer
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

Tactic:
replace h1 : z ^ n = z + 1 := by linear_combination h1
-- Module: Mathlib.RingTheory.Polynomial.Selmer
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
⊢ (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
-- Module: Mathlib.RingTheory.Polynomial.Selmer
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
⊢ 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

Premises used: add_mul, pow_succ, mul_assoc, LT.lt.le, Nat.sub_add_cancel, add_zero, OfNat.ofNat, Neg.neg
-- Module: Mathlib.RingTheory.Polynomial.Selmer
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
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
⊢ z ^ n = z + 1 ∧ z ^ n + HPow.hPow (β := ℕ) z 2 = 0

Tactic:
rw [h1] at h2 ⊢
-- Module: Mathlib.RingTheory.Polynomial.Selmer
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 + 1) + -1 * (z + 1) * z = 0
⊢ z + 1 + HPow.hPow (β := ℕ) z 2 = 0

Tactic:
linear_combination -h2
-- Module: Mathlib.RingTheory.Polynomial.Selmer
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 + 1) + -1 * (z + 1) * z = 0
⊢ z + 1 = z + 1 ∧ z + 1 + HPow.hPow (β := ℕ) z 2 = 0

Tactic:
exact ⟨rfl, by linear_combination -h2⟩
-- Module: Mathlib.RingTheory.Polynomial.Selmer
Goal:
n : ℕ
hn1 : n ≠ 1
pos : ∀ (hn0 : n = 0), Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
neg : ∀ (hn0 : ¬n = 0), Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
⊢ Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)

Tactic:
by_cases hn0 : n = 0
-- Module: Mathlib.RingTheory.Polynomial.Selmer
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : n = 0
pos : Irreducible (M := ℚ[X]) (-X)
⊢ Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)

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

Premises used: sub_self, add_comm, pow_zero, sub_sub, zero_sub
-- Module: Mathlib.RingTheory.Polynomial.Selmer
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : n = 0
⊢ Irreducible (M := ℚ[X]) (-X)

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

Premises used: Associated.irreducible, Exists.intro, Polynomial.irreducible_X, mul_neg_one, OfNat.ofNat, Polynomial.X, Neg.neg
-- Module: Mathlib.RingTheory.Polynomial.Selmer
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : n = 0
⊢ Irreducible (M := ℚ[X]) (-X)

Tactic:
exact Associated.irreducible ⟨-1, mul_neg_one X⟩ irreducible_X
-- Module: Mathlib.RingTheory.Polynomial.Selmer
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
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
⊢ HPow.hPow (α := ℤ[X]) X n - X - 1 = trinomial 0 1 n (-1) (-1) 1

Tactic:
simp only [trinomial, C_neg, C_1]

Premises used: Polynomial.C_1, Polynomial.trinomial, Polynomial.C_neg
-- Module: Mathlib.RingTheory.Polynomial.Selmer
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
⊢ 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:
ring
-- Module: Mathlib.RingTheory.Polynomial.Selmer
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
⊢ 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
-- Module: Mathlib.RingTheory.Polynomial.Selmer
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : HPow.hPow (α := ℤ[X]) X n - X - 1 = trinomial 0 1 n (-1) (-1) 1
⊢ 1 < n

Tactic:
have hn : 1 < n := Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hn0, hn1⟩
-- Module: Mathlib.RingTheory.Polynomial.Selmer
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)
neg₁ : (HPow.hPow (α := ℤ[X]) X n - X - 1).IsPrimitive
⊢ 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)
-- Module: Mathlib.RingTheory.Polynomial.Selmer
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)
neg₂ :
  ∀ (h : Irreducible (map (Int.castRingHom ℚ) X ^ n - map (Int.castRingHom ℚ) X - map (Int.castRingHom ℚ) 1)),
    Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
neg₃ :
  ∀ (h : Irreducible (map (Int.castRingHom ℚ) X ^ n - map (Int.castRingHom ℚ) X - 1)),
    Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
neg₄ neg₅ neg₆ neg₇ :
  ∀ (h : Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)), Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 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

Premises used: Polynomial.map_one, Polynomial.map_pow, Polynomial.map_X, Polynomial.map_sub
-- Module: Mathlib.RingTheory.Polynomial.Selmer
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
⊢ (HPow.hPow (α := ℤ[X]) X n - X - 1).IsPrimitive

Tactic:
hp.symm ▸ (trinomial_monic zero_lt_one hn).isPrimitive

Premises used: Eq.rec, Polynomial.trinomial_monic, zero_lt_one, Polynomial.Monic.isPrimitive, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.Selmer
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
⊢ (HPow.hPow (α := ℤ[X]) X n - X - 1).IsPrimitive

Tactic:
exact hp.symm ▸ (trinomial_monic zero_lt_one hn).isPrimitive
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F : Type u_1
inst : CommSemiring F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
⊢ IsSeparableContraction q f hf.contraction

Tactic:
Classical.choose_spec hf

Premises used: Classical.choose_spec, Polynomial.HasSeparableContraction.contraction
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F : Type u_1
inst : CommSemiring F
q : ℕ
f g : F[X]
hf : IsSeparableContraction q f g
obtain :
  ∀ (m : ℕ) (hf : IsSeparableContraction q ((expand F (q ^ m) : (a : F[X]) → F[X]) g) g),
    ∃ (m_1 : ℕ), g.natDegree * q ^ m_1 = natDegree.{u_1} (R := F) ((expand F (q ^ m) : (a : F[X]) → F[X]) g)
⊢ ∃ (m : ℕ), g.natDegree * q ^ m = f.natDegree

Tactic:
obtain ⟨m, rfl⟩ := hf.2

Premises used: And.right, rfl
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F : Type u_1
inst : CommSemiring F
q : ℕ
g : F[X]
m : ℕ
hf : IsSeparableContraction q ((expand F (q ^ m) : (a : F[X]) → F[X]) g) g
h : g.natDegree * q ^ m = natDegree.{u_1} (R := F) ((expand F (q ^ m) : (a : F[X]) → F[X]) g)
⊢ ∃ (m_1 : ℕ), g.natDegree * q ^ m_1 = natDegree.{u_1} (R := F) ((expand F (q ^ m) : (a : F[X]) → F[X]) g)

Tactic:
use m
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F : Type u_1
inst : CommSemiring F
q : ℕ
g : F[X]
m : ℕ
hf : IsSeparableContraction q ((expand F (q ^ m) : (a : F[X]) → F[X]) g) g
h h₁ : g.natDegree * q ^ m = g.natDegree * q ^ m
⊢ g.natDegree * q ^ m = natDegree.{u_1} (R := F) ((expand F (q ^ m) : (a : F[X]) → F[X]) g)

Tactic:
rw [natDegree_expand]

Premises used: Polynomial.natDegree_expand
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F : Type u_1
inst : CommSemiring F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
⊢ ∃ (m : ℕ), hf.degree * q ^ m = f.natDegree

Tactic:
(Classical.choose_spec hf).dvd_degree'

Premises used: Classical.choose_spec, Polynomial.HasSeparableContraction.degree, Polynomial.HasSeparableContraction.contraction, Polynomial.IsSeparableContraction.dvd_degree'
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F : Type u_1
inst : CommSemiring F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
⊢ hf.degree ∣ f.natDegree

Tactic:
let ⟨a, ha⟩ := hf.dvd_degree'
  Dvd.intro (q ^ a) ha

Premises used: Dvd.dvd, Dvd.intro, Polynomial.HasSeparableContraction.dvd_degree', _private.0.Polynomial.HasSeparableContraction.dvd_degree.match_1, HPow.hPow, Polynomial.HasSeparableContraction.degree, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F : Type u_1
inst : CommSemiring F
f : F[X]
hf : HasSeparableContraction 1 f
let : ∀ (a : ℕ) (ha : hf.degree * HPow.hPow (α := ℕ) 1 a = f.natDegree), hf.degree = f.natDegree
⊢ hf.degree = f.natDegree

Tactic:
let ⟨a, ha⟩ := hf.dvd_degree'
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F : Type u_1
inst : Field F
q : ℕ
hF : ExpChar F q
f : F[X]
irred : Irreducible f
zero : ∀ [CharZero F], HasSeparableContraction 1 f
prime : Nat.Prime q → ∀ [CharP F q], HasSeparableContraction q f
⊢ HasSeparableContraction q f

Tactic:
cases hF
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F : Type u_1
inst : Field F
f : F[X]
irred : Irreducible f
inst_1 : CharZero F
rw : (expand F 1 : (a : F[X]) → F[X]) f = f
rw₁ rw₂ : f = f
⊢ (expand F (HPow.hPow (α := ℕ) (β := ℕ) 1 0) : (a : F[X]) → F[X]) f = f

Tactic:
rw [pow_zero, expand_one]

Premises used: Polynomial.expand_one, pow_zero
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F : Type u_1
inst : Field F
f : F[X]
irred : Irreducible f
inst_1 : CharZero F
⊢ HasSeparableContraction 1 f

Tactic:
exact ⟨f, irred.separable, ⟨0, by rw [pow_zero, expand_one]⟩⟩
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F : Type u_1
inst : Field F
q : ℕ
f : F[X]
irred : Irreducible f
hprime : Nat.Prime q
hchar : CharP F q
prime :
  ∀ (n : ℕ) (g : F[X]) (hgs : g.Separable) (hge : (expand F (q ^ n) : (a : F[X]) → F[X]) g = f),
    HasSeparableContraction q f
⊢ HasSeparableContraction q f

Tactic:
rcases exists_separable_of_irreducible q irred ‹q.Prime›.ne_zero with ⟨n, g, hgs, hge⟩

Premises used: Nat.Prime.ne_zero, Polynomial.exists_separable_of_irreducible