awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Finite.GaloisField
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_1 : 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_1
x y : GaloisField (n_1 + 1) n
hx_1 :
  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 :
  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))
      y →
    x ^ (n_1 + 1) ^ n = x → y ^ (n_1 + 1) ^ n = y → x ^ (n_1 + 1) ^ n + y ^ (n_1 + 1) ^ n = x + y
⊢ ∀
    (hy :
      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))
        y),
    x ^ (n_1 + 1) ^ n = x → y ^ (n_1 + 1) ^ n = y → x ^ (n_1 + 1) ^ n + y ^ (n_1 + 1) ^ n = x + y

Tactic:
_
-- Module: Mathlib.FieldTheory.Finite.GaloisField
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_1 : GaloisField (n_1 + 1) n
hx_1 :
  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_1
x y : GaloisField (n_1 + 1) n
hx_2 :
  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
hy_1 :
  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))
    y
hx : x ^ (n_1 + 1) ^ n = x
hy : y ^ (n_1 + 1) ^ n = y
succ : x + y ^ (n_1 + 1) ^ n = x + y
succ₁ succ₂ : x + y = x + y
⊢ x ^ (n_1 + 1) ^ n + y ^ (n_1 + 1) ^ n = x + y

Tactic:
rw [hx, hy]
-- Module: Mathlib.FieldTheory.Finite.GaloisField
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_1 : 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_1
x : GaloisField (n_1 + 1) n
succ :
  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
⊢ ∀
    (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:
_
-- Module: Mathlib.FieldTheory.Finite.GaloisField
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_1 : GaloisField (n_1 + 1) n
hx_1 :
  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_1
x : GaloisField (n_1 + 1) n
hx_2 :
  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
hx :
  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
succ : ∀ (hx : x ^ (n_1 + 1) ^ n = 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 only [g_poly, sub_eq_zero, aeval_X_pow, aeval_X, map_sub, sub_neg_eq_add] at *

Premises used: map_sub, sub_eq_zero, Polynomial.aeval_X_pow, sub_neg_eq_add, Polynomial.aeval_X
-- Module: Mathlib.FieldTheory.Finite.GaloisField
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
      (↑((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) : Type) =
    (n_1 + 1) ^ n
nat_degree_eq : (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).natDegree = (n_1 + 1) ^ n
x_1 : GaloisField (n_1 + 1) n
hx_1 :
  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_1
x : GaloisField (n_1 + 1) n
hx_2 :
  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
hx : x ^ (n_1 + 1) ^ n = x
succ : -1 * x + x = 0
⊢ (-x) ^ (n_1 + 1) ^ n + x = 0

Tactic:
rw [neg_pow, hx, neg_one_pow_char_pow]

Premises used: neg_one_pow_char_pow, neg_pow
-- Module: Mathlib.FieldTheory.Finite.GaloisField
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
      (↑((HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).rootSet (GaloisField (n_1 + 1) n)) : Type) =
    (n_1 + 1) ^ n
nat_degree_eq : (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).natDegree = (n_1 + 1) ^ n
x_1 : GaloisField (n_1 + 1) n
hx_1 :
  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_1
x : GaloisField (n_1 + 1) n
hx_2 :
  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
hx : x ^ (n_1 + 1) ^ n = x
⊢ -1 * x + x = 0

Tactic:
simp
-- Module: Mathlib.FieldTheory.Finite.GaloisField
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_1 : 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_1
x y : GaloisField (n_1 + 1) n
succ :
  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 →
    ∀
      (hy :
        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))
          y),
      x ^ (n_1 + 1) ^ n = x → y ^ (n_1 + 1) ^ n = y → x ^ (n_1 + 1) ^ n * y ^ (n_1 + 1) ^ n = x * y
⊢ ∀
    (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)
    (hy :
      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))
        y),
    x ^ (n_1 + 1) ^ n = x → y ^ (n_1 + 1) ^ n = y → x ^ (n_1 + 1) ^ n * y ^ (n_1 + 1) ^ n = x * y

Tactic:
_
-- Module: Mathlib.FieldTheory.Finite.GaloisField
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_1 : 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_1
x y : GaloisField (n_1 + 1) n
hx_1 :
  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 :
  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))
      y →
    x ^ (n_1 + 1) ^ n = x → y ^ (n_1 + 1) ^ n = y → x ^ (n_1 + 1) ^ n * y ^ (n_1 + 1) ^ n = x * y
⊢ ∀
    (hy :
      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))
        y),
    x ^ (n_1 + 1) ^ n = x → y ^ (n_1 + 1) ^ n = y → x ^ (n_1 + 1) ^ n * y ^ (n_1 + 1) ^ n = x * y

Tactic:
_
-- Module: Mathlib.FieldTheory.Finite.GaloisField
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_1 : GaloisField (n_1 + 1) n
hx_1 :
  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_1
x y : GaloisField (n_1 + 1) n
hx_2 :
  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
hy_1 :
  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))
    y
hx : x ^ (n_1 + 1) ^ n = x
hy : y ^ (n_1 + 1) ^ n = y
succ : x * y ^ (n_1 + 1) ^ n = x * y
succ₁ succ₂ : x * y = x * y
⊢ x ^ (n_1 + 1) ^ n * y ^ (n_1 + 1) ^ n = x * y

Tactic:
rw [hx, hy]
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
b : Module.Basis (↥(IsNoetherian.finsetBasisIndex (ZMod p) (GaloisField p n))) (ZMod p) (GaloisField p n) :=
  IsNoetherian.finsetBasis (ZMod p) (GaloisField p n)
haveI : ∀ (this : Fintype (GaloisField p n)), Nat.card (GaloisField p n) = p ^ n
⊢ Nat.card (GaloisField p n) = p ^ n

Tactic:
haveI : Fintype (GaloisField p n) := Fintype.ofFinite (GaloisField p n)
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
b : Module.Basis (↥(IsNoetherian.finsetBasisIndex (ZMod p) (GaloisField p n))) (ZMod p) (GaloisField p n) :=
  IsNoetherian.finsetBasis (ZMod p) (GaloisField p n)
this : Fintype (GaloisField p n)
rw : Fintype.card (GaloisField p n) = p ^ n
rw₁ : Fintype.card (ZMod p) ^ Fintype.card ↥(IsNoetherian.finsetBasisIndex (ZMod p) (GaloisField p n)) = p ^ n
rw₂ : Fintype.card (ZMod p) ^ Module.finrank (ZMod p) (GaloisField p n) = p ^ n
rw₃ : p ^ Module.finrank (ZMod p) (GaloisField p n) = p ^ n
rw₄ rw₅ : p ^ n = p ^ n
⊢ Nat.card (GaloisField p n) = p ^ n

Tactic:
rw [Nat.card_eq_fintype_card, Module.card_fintype b, ← Module.finrank_eq_card_basis b,
    ZMod.card, finrank p h]

Premises used: GaloisField.finrank, Module.finrank_eq_card_basis, Module.card_fintype, ZMod.card, Nat.card_eq_fintype_card
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
⊢ 1 < p

Tactic:
have hp : 1 < p := h_prime.out.one_lt
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
hp : 1 < p
⊢ (HPow.hPow (α := (ZMod p)[X]) X (Fintype.card (ZMod p)) - X).roots = val univ

Tactic:
FiniteField.roots_X_pow_card_sub_X (ZMod p)

Premises used: FiniteField.roots_X_pow_card_sub_X, ZMod
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
hp : 1 < p
h : ZMod.commRing p = Field.toCommRing → p = Fintype.card (ZMod p)
⊢ (HPow.hPow (α := (ZMod p)[X]) X p - X).roots = val univ

Tactic:
convert! FiniteField.roots_X_pow_card_sub_X (ZMod p)

Premises used: FiniteField.roots_X_pow_card_sub_X, ZMod
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
hp : 1 < p
e_2 : ZMod.commRing p = Field.toCommRing
⊢ p = Fintype.card (ZMod p)

Tactic:
(ZMod.card p).symm

Premises used: Eq.symm, ZMod.card
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
hp : 1 < p
e_2 : ZMod.commRing p = Field.toCommRing
⊢ p = Fintype.card (ZMod p)

Tactic:
exact (ZMod.card p).symm

Premises used: Eq.symm, ZMod.card
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
hp : 1 < p
⊢ (HPow.hPow (α := (ZMod p)[X]) X p - X).roots = val univ

Tactic:
have h1 : roots (X ^ p - X : (ZMod p)[X]) = Finset.univ.val := by
    convert! FiniteField.roots_X_pow_card_sub_X (ZMod p)
    exact (ZMod.card p).symm
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
hp : 1 < p
h1 : (HPow.hPow (α := (ZMod p)[X]) X p - X).roots = val univ
⊢ (HPow.hPow (α := (ZMod p)[X]) X p - X).natDegree = p

Tactic:
have h2 := FiniteField.X_pow_card_sub_X_natDegree_eq (ZMod p) hp
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
hp : 1 < p
h1 : (HPow.hPow (α := (ZMod p)[X]) X p - X).roots = val univ
h2 : (HPow.hPow (α := (ZMod p)[X]) X p - X).natDegree = p
zero :
  ∀ [h_prime : Fact (Nat.Prime 0)] (hp : LT.lt (α := ℕ) 1 0)
    (h1 : (HPow.hPow (α := (ZMod 0)[X]) (β := ℕ) X 0 - X).roots = val univ)
    (h2 : (HPow.hPow (α := (ZMod 0)[X]) (β := ℕ) X 0 - X).natDegree = 0),
    (HPow.hPow (α := (ZMod 0)[X]) (β := ℕ) X 0 - X).Splits
succ :
  ∀ (n : ℕ) [h_prime : Fact (Nat.Prime (n + 1))] (hp : 1 < n + 1)
    (h1 : (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).roots = val univ)
    (h2 : (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).natDegree = n + 1),
    (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).Splits
⊢ (HPow.hPow (α := (ZMod p)[X]) X p - X).Splits

Tactic:
cases p
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
h_prime : Fact (Nat.Prime 0)
hp : LT.lt (α := ℕ) 1 0
h1 : (HPow.hPow (α := (ZMod 0)[X]) (β := ℕ) X 0 - X).roots = val univ
h2 : (HPow.hPow (α := (ZMod 0)[X]) (β := ℕ) X 0 - X).natDegree = 0
⊢ (HPow.hPow (α := (ZMod 0)[X]) (β := ℕ) X 0 - X).Splits

Tactic:
cases hp