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 : 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),
    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
⊢ ∀ (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:
simp_rw [mem_rootSet_of_ne aux]

Premises used: Polynomial.mem_rootSet_of_ne
-- 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 : 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 :
  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
⊢ 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:
simp_rw [mem_rootSet_of_ne aux]

Premises used: Polynomial.mem_rootSet_of_ne
-- 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 : 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 :
  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
⊢ 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:
simp_rw [mem_rootSet_of_ne aux]

Premises used: Polynomial.mem_rootSet_of_ne
-- 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 : 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 (γ := 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
⊢ ∀ (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)

Tactic:
simp_rw [mem_rootSet_of_ne aux]

Premises used: Polynomial.mem_rootSet_of_ne
-- 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 : 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
r : ZMod (n_1 + 1)
succ :
  HSub.hSub (β := GaloisField (n_1 + 1) n)
      (HPow.hPow (α := GaloisField (n_1 + 1) n)
        ((algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) r :
          GaloisField (n_1 + 1) n)
        ((n_1 + 1) ^ n))
      ((algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) r :
        GaloisField (n_1 + 1) n) =
    0
⊢ Eq (α := GaloisField (n_1 + 1) n)
    (((aeval
            ((algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n)
              r) :
          (ZMod (n_1 + 1))[X] →ₐ[ZMod (n_1 + 1)] GaloisField (n_1 + 1) n) :
        (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 [map_sub, map_pow, aeval_X]

Premises used: map_sub, map_pow, 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 (↑(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
r : ZMod (n_1 + 1)
succ :
  HSub.hSub (α := GaloisField (n_1 + 1) n) (β := GaloisField (n_1 + 1) n)
      ((algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n)
          (r ^ (n_1 + 1) ^ n) :
        GaloisField (n_1 + 1) n)
      ((algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) r :
        GaloisField (n_1 + 1) n) =
    0
succ₁ :
  HSub.hSub (α := GaloisField (n_1 + 1) n) (β := GaloisField (n_1 + 1) n)
      ((algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) r :
        GaloisField (n_1 + 1) n)
      ((algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) r :
        GaloisField (n_1 + 1) n) =
    0
succ₂ succ₃ : Eq (α := GaloisField (n_1 + 1) n) 0 0
⊢ HSub.hSub (β := GaloisField (n_1 + 1) n)
      (HPow.hPow (α := GaloisField (n_1 + 1) n)
        ((algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) r :
          GaloisField (n_1 + 1) n)
        ((n_1 + 1) ^ n))
      ((algebraMap (ZMod (n_1 + 1)) (GaloisField (n_1 + 1) n) : (a : ZMod (n_1 + 1)) → GaloisField (n_1 + 1) n) r :
        GaloisField (n_1 + 1) n) =
    0

Tactic:
rw [← map_pow, ZMod.pow_card_pow, sub_self]

Premises used: sub_self, map_pow, ZMod.pow_card_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 (↑(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 :
  Membership.mem (γ := Set (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).SplittingField)
    ((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 succ₁ succ₂ succ₃ :
  ∀
    (hx :
      Eq (α := (HPow.hPow (α := (ZMod (n_1 + 1))[X]) X ((n_1 + 1) ^ n) - X).SplittingField)
        ((aeval x : (a : (ZMod (n_1 + 1))[X]) → (X ^ (n_1 + 1) ^ n - X).SplittingField)
          (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
⊢ 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:
rwa [mem_rootSet_of_ne aux] at hx

Premises used: Polynomial.mem_rootSet_of_ne
-- 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 : 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 :
  Eq (α := GaloisField (n_1 + 1) n)
    ((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).coeff 0) :
      GaloisField (n_1 + 1) n)
    (0 : GaloisField (n_1 + 1) n)
⊢ 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:
rw [← coeff_zero_eq_aeval_zero']

Premises used: Polynomial.coeff_zero_eq_aeval_zero'
-- 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 : 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 : 0 = (n_1 + 1) ^ n → False
⊢ Eq (α := GaloisField (n_1 + 1) n)
    ((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).coeff 0) :
      GaloisField (n_1 + 1) n)
    (0 : GaloisField (n_1 + 1) n)

Tactic:
simp only [coeff_X_pow, coeff_X_zero, sub_zero, _root_.map_eq_zero, ite_eq_right_iff,
      one_ne_zero, coeff_sub]

Premises used: sub_zero, Polynomial.coeff_X_pow, map_eq_zero, Polynomial.coeff_X_zero, ite_eq_right_iff, Polynomial.coeff_sub, one_ne_zero
-- 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 : 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
hn : 0 = (n_1 + 1) ^ n
⊢ False

Tactic:
Nat.not_lt_zero 1 (eq_zero_of_pow_eq_zero hn.symm ▸ hp)

Premises used: Eq.rec, Nat.not_lt_zero, eq_zero_of_pow_eq_zero, OfNat.ofNat, Eq.symm
-- 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 : 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
hn : 0 = (n_1 + 1) ^ n
⊢ False

Tactic:
exact Nat.not_lt_zero 1 (eq_zero_of_pow_eq_zero hn.symm ▸ hp)

Premises used: Eq.rec, Nat.not_lt_zero, eq_zero_of_pow_eq_zero, OfNat.ofNat, Eq.symm
-- 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 : 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 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
-- 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:
_