awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (hypothesis)
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this_1 : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X
hp : 1 < p
aux : g_poly ≠ 0
nat_degree_eq : g_poly.natDegree = p ^ n
this : Eq (α := Set (GaloisField p n)) (g_poly.rootSet (GaloisField p n)) Set.univ
key : Fintype.card (GaloisField p n) = p ^ n
⊢ Module.finrank (ZMod p) (GaloisField p n) = n
have key₁ : p ^ Module.finrank (ZMod p) (GaloisField p n) = p ^ n
Tactic: rw [@Module.card_eq_pow_finrank (K := ZMod p), ZMod.card] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card (↑(g_poly.rootSet (GaloisField p n)) : Type) = p ^ n
nat_degree_eq : g_poly.natDegree = p ^ n
⊢ Module.finrank (ZMod p) (GaloisField p n) = n
have suffices : Eq (α := Set (GaloisField p n)) (g_poly.rootSet (GaloisField p n)) Set.univ
Tactic: suffices g_poly.rootSet (GaloisField p n) = Set.univ by
    simp_rw [this, ← Fintype.ofEquiv_card (Equiv.Set.univ _)] at key
    -- Porting note: prevents `card_eq_pow_finrank` from using a wrong instance for `Fintype`
    rw [@Module.card_eq_pow_finrank (K := ZMod p), ZMod.card] at key
    exact Nat.pow_right_injective (Nat.Prime.one_lt' p).out key
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card (↑(g_poly.rootSet (GaloisField p n)) : Type) = p ^ n
nat_degree_eq : g_poly.natDegree = p ^ n
⊢ Eq (α := Set (GaloisField p n)) (g_poly.rootSet (GaloisField p n)) Set.univ
have rw : ∀ (x : GaloisField p n), Membership.mem (γ := Set (GaloisField p n)) (g_poly.rootSet (GaloisField p n)) x
Tactic: rw [Set.eq_univ_iff_forall]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card (↑(g_poly.rootSet (GaloisField p n)) : Type) = p ^ n
nat_degree_eq : g_poly.natDegree = p ^ n
⊢ ∀ (x : GaloisField p n), Membership.mem (γ := Set (GaloisField p n)) (g_poly.rootSet (GaloisField p n)) x
have suffices : ∀ (x : GaloisField p n) (hx : Membership.mem (γ := Subalgebra (ZMod p) (GaloisField p n)) ⊤ x),
  Membership.mem (γ := Set (GaloisField p n)) ((HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X).rootSet (GaloisField p n)) x
Tactic: suffices ∀ (x) (hx : x ∈ (⊤ : Subalgebra (ZMod p) (GaloisField p n))),
      x ∈ (X ^ p ^ n - X : (ZMod p)[X]).rootSet (GaloisField p n)
    by simpa
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card (↑(g_poly.rootSet (GaloisField p n)) : Type) = p ^ n
nat_degree_eq : g_poly.natDegree = p ^ n
⊢ ∀ (x : GaloisField p n) (hx : Membership.mem (γ := Subalgebra (ZMod p) (GaloisField p n)) ⊤ x),
    Membership.mem (γ := Set (GaloisField p n)) ((HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X).rootSet (GaloisField p n))
      x
have rw : ∀ (x : GaloisField p n)
  (hx :
    Membership.mem (γ := Subalgebra (ZMod p) (GaloisField p n))
      (Algebra.adjoin (ZMod p)
        ((HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X).rootSet
          (HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X).SplittingField))
      x),
  Membership.mem (γ := Set (GaloisField p n)) ((HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X).rootSet (GaloisField p n)) x
Tactic: rw [← SplittingField.adjoin_rootSet]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card (↑(g_poly.rootSet (GaloisField p n)) : Type) = p ^ n
nat_degree_eq : g_poly.natDegree = p ^ n
⊢ ∀ (x : GaloisField p n)
    (hx :
      Membership.mem (γ := Subalgebra (ZMod p) (GaloisField p n))
        (Algebra.adjoin (ZMod p)
          ((HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X).rootSet
            (HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X).SplittingField))
        x),
    Membership.mem (γ := Set (GaloisField p n)) ((HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X).rootSet (GaloisField p n))
      x
have simp_rw : ∀ (x : GaloisField p n)
  (hx :
    Membership.mem (γ := Subring (GaloisField p n))
      (Subring.closure
        (Set.range (ι := ZMod p) (⇑(algebraMap (ZMod p) (GaloisField p n)) : (a : ZMod p) → GaloisField p n) ∪
          (HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X).rootSet
            (HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X).SplittingField))
      x),
  Membership.mem (γ := Set (GaloisField p n)) ((HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X).rootSet (GaloisField p n)) x
Tactic: simp_rw [Algebra.mem_adjoin_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card (↑(g_poly.rootSet (GaloisField p n)) : Type) = p ^ n
nat_degree_eq : g_poly.natDegree = p ^ n
x : GaloisField p n
hx :
  Membership.mem (γ := Subring (GaloisField p n))
    (Subring.closure
      (Set.range (ι := ZMod p) (⇑(algebraMap (ZMod p) (GaloisField p n)) : (a : ZMod p) → GaloisField p n) ∪
        (HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X).rootSet
          (HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X).SplittingField))
    x
⊢ Membership.mem (γ := Set (GaloisField p n)) ((HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X).rootSet (GaloisField p n)) x
have zero : ∀ [h_prime : Fact (Nat.Prime 0)] (this : Fintype (GaloisField 0 n)),
  let g_poly := HPow.hPow (α := (ZMod 0)[X]) X (HPow.hPow (α := ℕ) 0 n) - X;
  ∀ (hp : LT.lt (α := ℕ) 1 0) (aux : g_poly ≠ 0)
    (key : Fintype.card (↑(g_poly.rootSet (GaloisField 0 n)) : Type) = HPow.hPow (α := ℕ) 0 n)
    (nat_degree_eq : g_poly.natDegree = HPow.hPow (α := ℕ) 0 n) (x : GaloisField 0 n)
    (hx :
      Membership.mem (γ := Subring (GaloisField 0 n))
        (Subring.closure
          (Set.range (ι := ZMod 0) (⇑(algebraMap (ZMod 0) (GaloisField 0 n)) : (a : ZMod 0) → GaloisField 0 n) ∪
            (HPow.hPow (α := (ZMod 0)[X]) X (HPow.hPow (α := ℕ) 0 n) - X).rootSet
              (HPow.hPow (α := (ZMod 0)[X]) X (HPow.hPow (α := ℕ) 0 n) - X).SplittingField))
        x),
    Membership.mem (γ := Set (GaloisField 0 n))
      ((HPow.hPow (α := (ZMod 0)[X]) X (HPow.hPow (α := ℕ) 0 n) - X).rootSet (GaloisField 0 n)) x
Tactic: cases p
Cleared hypotheses: p, h_prime, this, g_poly, hp, aux, key, nat_degree_eq, x, hx
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card (↑(g_poly.rootSet (GaloisField p n)) : Type) = p ^ n
nat_degree_eq : g_poly.natDegree = p ^ n
x : GaloisField p n
hx :
  Membership.mem (γ := Subring (GaloisField p n))
    (Subring.closure
      (Set.range (ι := ZMod p) (⇑(algebraMap (ZMod p) (GaloisField p n)) : (a : ZMod p) → GaloisField p n) ∪
        (HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X).rootSet
          (HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X).SplittingField))
    x
zero :
  ∀ [h_prime : Fact (Nat.Prime 0)] (this : Fintype (GaloisField 0 n)),
    let g_poly := HPow.hPow (α := (ZMod 0)[X]) X (HPow.hPow (α := ℕ) 0 n) - X;
    ∀ (hp : LT.lt (α := ℕ) 1 0) (aux : g_poly ≠ 0)
      (key : Fintype.card (↑(g_poly.rootSet (GaloisField 0 n)) : Type) = HPow.hPow (α := ℕ) 0 n)
      (nat_degree_eq : g_poly.natDegree = HPow.hPow (α := ℕ) 0 n) (x : GaloisField 0 n)
      (hx :
        Membership.mem (γ := Subring (GaloisField 0 n))
          (Subring.closure
            (Set.range (ι := ZMod 0) (⇑(algebraMap (ZMod 0) (GaloisField 0 n)) : (a : ZMod 0) → GaloisField 0 n) ∪
              (HPow.hPow (α := (ZMod 0)[X]) X (HPow.hPow (α := ℕ) 0 n) - X).rootSet
                (HPow.hPow (α := (ZMod 0)[X]) X (HPow.hPow (α := ℕ) 0 n) - X).SplittingField))
          x),
      Membership.mem (γ := Set (GaloisField 0 n))
        ((HPow.hPow (α := (ZMod 0)[X]) X (HPow.hPow (α := ℕ) 0 n) - X).rootSet (GaloisField 0 n)) x
⊢ Membership.mem (γ := Set (GaloisField p n)) ((HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X).rootSet (GaloisField p n)) x
have succ : ∀ (n_1 : ℕ) [h_prime : Fact (Nat.Prime (n_1 + 1))] (this : Fintype (GaloisField (n_1 + 1) n)),
  let g_poly := HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X;
  ∀ (hp : 1 < n_1 + 1) (aux : g_poly ≠ 0)
    (key : Fintype.card (↑(g_poly.rootSet (GaloisField (n_1 + 1) n)) : Type) = (n_1 + 1) ^ n)
    (nat_degree_eq : g_poly.natDegree = (n_1 + 1) ^ n) (x : GaloisField (n_1 + 1) n)
    (hx :
      Membership.mem (γ := Subring (GaloisField (n_1 + 1) n))
        (Subring.closure
          (Set.range (ι := ZMod (n_1 + 1))
              (⇑(algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n)) :
                (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) ∪
            (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet
              (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).SplittingField))
        x),
    Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
      ((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) x
Tactic: cases p
Cleared hypotheses: p, h_prime, this, g_poly, hp, aux, key, nat_degree_eq, x, hx
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
n : ℕ
h : n ≠ 0
n_1 : ℕ
h_prime : Fact (Nat.Prime (n_1 + 1))
this : Fintype (GaloisField (n_1 + 1) n)
g_poly : (ZMod (n_1 + 1))[X] := HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X
hp : 1 < n_1 + 1
aux : HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X ≠ 0
key : Fintype.card (↑(g_poly.rootSet (GaloisField (n_1 + 1) n)) : Type) = (n_1 + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n_1 + 1) ^ n
x : GaloisField (n_1 + 1) n
hx :
  Membership.mem (γ := Subring (GaloisField (n_1 + 1) n))
    (Subring.closure
      (Set.range (ι := ZMod (n_1 + 1))
          (⇑(algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n)) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) ∪
        (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet
          (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).SplittingField))
    x
⊢ Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
    ((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) x
have succ : ∀ (x : GaloisField (n_1 + 1) n)
  (hx :
    Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
      (Set.range (ι := ZMod (n_1 + 1))
          (⇑(algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n)) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) ∪
        (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet
          (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).SplittingField)
      x),
  Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
    ((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) x
Tactic: refine Subring.closure_induction ?_ ?_ ?_ ?_ ?_ ?_ hx
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
n : ℕ
h : n ≠ 0
n_1 : ℕ
h_prime : Fact (Nat.Prime (n_1 + 1))
this : Fintype (GaloisField (n_1 + 1) n)
g_poly : (ZMod (n_1 + 1))[X] := HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X
hp : 1 < n_1 + 1
aux : HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X ≠ 0
key : Fintype.card (↑(g_poly.rootSet (GaloisField (n_1 + 1) n)) : Type) = (n_1 + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n_1 + 1) ^ n
x : GaloisField (n_1 + 1) n
hx :
  Membership.mem (γ := Subring (GaloisField (n_1 + 1) n))
    (Subring.closure
      (Set.range (ι := ZMod (n_1 + 1))
          (⇑(algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n)) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) ∪
        (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet
          (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).SplittingField))
    x
succ :
  ∀ (x : GaloisField (n_1 + 1) n)
    (hx :
      Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
        (Set.range (ι := ZMod (n_1 + 1))
            (⇑(algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n)) :
              (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) ∪
          (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet
            (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).SplittingField)
        x),
    Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
      ((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) x
⊢ Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
    ((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) x
have succ₁ : Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
  ((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) 0
Tactic: refine Subring.closure_induction ?_ ?_ ?_ ?_ ?_ ?_ hx
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
n : ℕ
h : n ≠ 0
n_1 : ℕ
h_prime : Fact (Nat.Prime (n_1 + 1))
this : Fintype (GaloisField (n_1 + 1) n)
g_poly : (ZMod (n_1 + 1))[X] := HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X
hp : 1 < n_1 + 1
aux : HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X ≠ 0
key : Fintype.card (↑(g_poly.rootSet (GaloisField (n_1 + 1) n)) : Type) = (n_1 + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n_1 + 1) ^ n
x : GaloisField (n_1 + 1) n
hx :
  Membership.mem (γ := Subring (GaloisField (n_1 + 1) n))
    (Subring.closure
      (Set.range (ι := ZMod (n_1 + 1))
          (⇑(algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n)) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) ∪
        (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet
          (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).SplittingField))
    x
succ :
  ∀ (x : GaloisField (n_1 + 1) n)
    (hx :
      Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
        (Set.range (ι := ZMod (n_1 + 1))
            (⇑(algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n)) :
              (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) ∪
          (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet
            (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).SplittingField)
        x),
    Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
      ((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) x
succ₁ :
  Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
    ((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) 0
⊢ Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
    ((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) x
have succ₂ : Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
  ((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) 1
Tactic: refine Subring.closure_induction ?_ ?_ ?_ ?_ ?_ ?_ hx
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
n : ℕ
h : n ≠ 0
n_1 : ℕ
h_prime : Fact (Nat.Prime (n_1 + 1))
this : Fintype (GaloisField (n_1 + 1) n)
g_poly : (ZMod (n_1 + 1))[X] := HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X
hp : 1 < n_1 + 1
aux : HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X ≠ 0
key : Fintype.card (↑(g_poly.rootSet (GaloisField (n_1 + 1) n)) : Type) = (n_1 + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n_1 + 1) ^ n
x : GaloisField (n_1 + 1) n
hx :
  Membership.mem (γ := Subring (GaloisField (n_1 + 1) n))
    (Subring.closure
      (Set.range (ι := ZMod (n_1 + 1))
          (⇑(algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n)) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) ∪
        (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet
          (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).SplittingField))
    x
⊢ ∀ (x : GaloisField (n_1 + 1) n)
    (hx :
      Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
        (Set.range (ι := ZMod (n_1 + 1))
            (⇑(algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n)) :
              (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) ∪
          (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet
            (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).SplittingField)
        x),
    Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
      ((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) x
have succ : ∀ (x : GaloisField (n_1 + 1) n)
  (hx :
    Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
      (Set.range (ι := ZMod (n_1 + 1))
          (⇑(algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n)) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) ∪
        (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet
          (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).SplittingField)
      x),
  Eq (α := GaloisField (n_1 + 1) n)
    ((aeval x : (a : (ZMod (n_1 + 1))[X]) → GaloisField (n_1 + 1) n)
      (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X))
    0
Tactic: simp_rw [mem_rootSet_of_ne aux]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
n : ℕ
h : n ≠ 0
n_1 : ℕ
h_prime : Fact (Nat.Prime (n_1 + 1))
this : Fintype (GaloisField (n_1 + 1) n)
g_poly : (ZMod (n_1 + 1))[X] := HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X
hp : 1 < n_1 + 1
aux : HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X ≠ 0
key : Fintype.card (↑(g_poly.rootSet (GaloisField (n_1 + 1) n)) : Type) = (n_1 + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n_1 + 1) ^ n
x : GaloisField (n_1 + 1) n
hx :
  Membership.mem (γ := Subring (GaloisField (n_1 + 1) n))
    (Subring.closure
      (Set.range (ι := ZMod (n_1 + 1))
          (⇑(algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n)) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) ∪
        (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet
          (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).SplittingField))
    x
⊢ Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
    ((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) 0
have succ : Eq (α := GaloisField (n_1 + 1) n)
  ((aeval 0 : (a : (ZMod (n_1 + 1))[X]) → GaloisField (n_1 + 1) n)
    (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X))
  0
Tactic: simp_rw [mem_rootSet_of_ne aux]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
n : ℕ
h : n ≠ 0
n_1 : ℕ
h_prime : Fact (Nat.Prime (n_1 + 1))
this : Fintype (GaloisField (n_1 + 1) n)
g_poly : (ZMod (n_1 + 1))[X] := HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X
hp : 1 < n_1 + 1
aux : HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X ≠ 0
key : Fintype.card (↑(g_poly.rootSet (GaloisField (n_1 + 1) n)) : Type) = (n_1 + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n_1 + 1) ^ n
x : GaloisField (n_1 + 1) n
hx :
  Membership.mem (γ := Subring (GaloisField (n_1 + 1) n))
    (Subring.closure
      (Set.range (ι := ZMod (n_1 + 1))
          (⇑(algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n)) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) ∪
        (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet
          (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).SplittingField))
    x
⊢ Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
    ((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) 1
have succ : Eq (α := GaloisField (n_1 + 1) n)
  ((aeval 1 : (a : (ZMod (n_1 + 1))[X]) → GaloisField (n_1 + 1) n)
    (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X))
  0
Tactic: simp_rw [mem_rootSet_of_ne aux]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
n : ℕ
h : n ≠ 0
n_1 : ℕ
h_prime : Fact (Nat.Prime (n_1 + 1))
this : Fintype (GaloisField (n_1 + 1) n)
g_poly : (ZMod (n_1 + 1))[X] := HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X
hp : 1 < n_1 + 1
aux : HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X ≠ 0
key : Fintype.card (↑(g_poly.rootSet (GaloisField (n_1 + 1) n)) : Type) = (n_1 + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n_1 + 1) ^ n
x : GaloisField (n_1 + 1) n
hx :
  Membership.mem (γ := Subring (GaloisField (n_1 + 1) n))
    (Subring.closure
      (Set.range (ι := ZMod (n_1 + 1))
          (⇑(algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n)) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) ∪
        (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet
          (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).SplittingField))
    x
⊢ ∀ (x : GaloisField (n_1 + 1) n)
    (hx :
      Membership.mem (γ := Subring (GaloisField (n_1 + 1) n))
        (Subring.closure
          (Set.range (ι := ZMod (n_1 + 1))
              (⇑(algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n)) :
                (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) ∪
            (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet
              (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).SplittingField))
        x),
    Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
        ((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) x →
      Membership.mem (γ := Set (GaloisField (n_1 + 1) n))
        ((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) (-x)
have succ : ∀ (x : GaloisField (n_1 + 1) n)
  (hx :
    Membership.mem (γ := Subring (GaloisField (n_1 + 1) n))
      (Subring.closure
        (Set.range (ι := ZMod (n_1 + 1))
            (⇑(algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n)) :
              (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) ∪
          (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet
            (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).SplittingField))
      x),
  Eq (α := GaloisField (n_1 + 1) n)
      ((aeval x : (a : (ZMod (n_1 + 1))[X]) → GaloisField (n_1 + 1) n)
        (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X))
      0 →
    Eq (α := GaloisField (n_1 + 1) n)
      ((aeval (-x) : (a : (ZMod (n_1 + 1))[X]) → GaloisField (n_1 + 1) n)
        (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X))
      0
Tactic: simp_rw [mem_rootSet_of_ne aux]