awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Finite.Extension
Goal:
K : Type u_2
inst : Field K
n : ℕ
f : K[X]
hi : Irreducible f
h : f ∣ HPow.hPow (α := K[X]) X (Nat.card K ^ n) - X
hn : n ≠ 0
h_1 : Finite K
p : ℕ
hp : CharP K p
this_1 : Fact (Nat.Prime p)
this : NeZero n
⊢ Splits (R := Extension K p n)
    (Polynomial.map (algebraMap K (Extension K p n)) (HPow.hPow (α := K[X]) X (Nat.card K ^ n) - X))

Tactic:
apply IsSplittingField.splits

Premises used: Polynomial.IsSplittingField.splits
-- Module: Mathlib.FieldTheory.Finite.Extension
Goal:
K : Type u_2
inst : Field K
n : ℕ
f : K[X]
hi : Irreducible f
h : f ∣ HPow.hPow (α := K[X]) X (Nat.card K ^ n) - X
hn : n ≠ 0
h_1 : Finite K
p : ℕ
hp : CharP K p
this_1 : Fact (Nat.Prime p)
this : NeZero n
⊢ Ne (α := (Extension K p n)[X])
    (Polynomial.map (algebraMap K (Extension K p n)) (HPow.hPow (α := K[X]) X (Nat.card K ^ n) - X)) 0

Tactic:
map_ne_zero (X_pow_card_pow_sub_X_ne_zero K hn Finite.one_lt_card)

Premises used: Finite.one_lt_card, FiniteField.X_pow_card_pow_sub_X_ne_zero, Polynomial.map_ne_zero
-- Module: Mathlib.FieldTheory.Finite.Extension
Goal:
K : Type u_2
inst : Field K
n : ℕ
f : K[X]
hi : Irreducible f
h : f ∣ HPow.hPow (α := K[X]) X (Nat.card K ^ n) - X
hn : n ≠ 0
h_1 : Finite K
p : ℕ
hp : CharP K p
this_1 : Fact (Nat.Prime p)
this : NeZero n
⊢ Ne (α := (Extension K p n)[X])
    (Polynomial.map (algebraMap K (Extension K p n)) (HPow.hPow (α := K[X]) X (Nat.card K ^ n) - X)) 0

Tactic:
exact map_ne_zero (X_pow_card_pow_sub_X_ne_zero K hn Finite.one_lt_card)
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
F : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : Field F
inst_3 : Algebra F K
⊢ (HPow.hPow (α := K[X]) X (Fintype.card K) - X).natDegree = Fintype.card K

Tactic:
have h : (X ^ Fintype.card K - X : K[X]).natDegree = Fintype.card K :=
      FiniteField.X_pow_card_sub_X_natDegree_eq K Fintype.one_lt_card
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
F : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : Field F
inst_3 : Algebra F K
h : (HPow.hPow (α := K[X]) X (Fintype.card K) - X).natDegree = Fintype.card K
rw :
  (roots (Polynomial.map (algebraMap F K) (HPow.hPow (α := F[X]) X (Fintype.card K) - X))).card =
    natDegree (Polynomial.map (algebraMap F K) (HPow.hPow (α := F[X]) X (Fintype.card K) - X))
rw₁ :
  (HSub.hSub (α := K[X]) (Polynomial.map (algebraMap F K) (HPow.hPow (α := F[X]) X (Fintype.card K)))
          (Polynomial.map (algebraMap F K : F →+* K) X)).roots.card =
    (HSub.hSub (α := K[X]) (Polynomial.map (algebraMap F K) (HPow.hPow (α := F[X]) X (Fintype.card K)))
        (Polynomial.map (algebraMap F K : F →+* K) X)).natDegree
rw₂ :
  (HPow.hPow (α := K[X]) (Polynomial.map (algebraMap F K : F →+* K) X) (Fintype.card K) -
          Polynomial.map (algebraMap F K : F →+* K) X).roots.card =
    (HPow.hPow (α := K[X]) (Polynomial.map (algebraMap F K : F →+* K) X) (Fintype.card K) -
        Polynomial.map (algebraMap F K : F →+* K) X).natDegree
rw₃ :
  (HPow.hPow (α := K[X]) X (Fintype.card K) - X).roots.card = (HPow.hPow (α := K[X]) X (Fintype.card K) - X).natDegree
rw₄ : (HPow.hPow (α := K[X]) X (Fintype.card K) - X).roots.card = Fintype.card K
rw₅ : Multiset.card.{u_1} (α := K) (val univ) = Fintype.card K
rw₆ : Finset.card.{u_1} (α := K) univ = Fintype.card K
rw₇ rw₈ : Fintype.card K = Fintype.card K
⊢ Splits (Polynomial.map (algebraMap F K) (HPow.hPow (α := F[X]) X (Fintype.card K) - X))

Tactic:
rw [splits_iff_card_roots, Polynomial.map_sub, Polynomial.map_pow,
      map_X, h, FiniteField.roots_X_pow_card_sub_X K, ← Finset.card_def, Finset.card_univ]

Premises used: Finset.card_univ, FiniteField.roots_X_pow_card_sub_X, Polynomial.map_pow, Polynomial.map_X, Polynomial.splits_iff_card_roots, Polynomial.map_sub, Finset.card_def
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
F : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : Field F
inst_3 : Algebra F K
trans :
  Eq (α := Subalgebra F K) (Algebra.adjoin F ((HPow.hPow (α := F[X]) X (Fintype.card K) - X).rootSet K))
    (Algebra.adjoin F (↑(HPow.hPow (α := K[X]) X (Fintype.card K) - X).roots.toFinset : Set K))
trans₁ :
  Eq (α := Subalgebra F K) (Algebra.adjoin F (↑(HPow.hPow (α := K[X]) X (Fintype.card K) - X).roots.toFinset : Set K)) ⊤
⊢ Eq (α := Subalgebra F K) (Algebra.adjoin F ((HPow.hPow (α := F[X]) X (Fintype.card K) - X).rootSet K)) ⊤

Tactic:
trans Algebra.adjoin F ((roots (X ^ Fintype.card K - X : K[X])).toFinset : Set K)

Premises used: Multiset.toFinset, Polynomial.roots, HSub.hSub, Algebra.adjoin, Fintype.card, SetLike.coe, HPow.hPow, Polynomial.X
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
F : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : Field F
inst_3 : Algebra F K
⊢ Eq (α := Subalgebra F K) (Algebra.adjoin F ((HPow.hPow (α := F[X]) X (Fintype.card K) - X).rootSet K))
    (Algebra.adjoin F (↑(HPow.hPow (α := K[X]) X (Fintype.card K) - X).roots.toFinset : Set K))

Tactic:
simp only [rootSet, aroots, Polynomial.map_pow, map_X, Polynomial.map_sub]

Premises used: Polynomial.rootSet, Polynomial.map_pow, Polynomial.map_X, Polynomial.aroots, Polynomial.map_sub
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
F : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : Field F
inst_3 : Algebra F K
rw : Eq (α := Subalgebra F K) (Algebra.adjoin F (↑(Multiset.toFinset (val univ)) : Set K)) ⊤
rw₁ : Eq (α := Subalgebra F K) (Algebra.adjoin F (↑univ : Set K)) ⊤
rw₂ : Eq.{u_1 + 1} (α := Subalgebra F K) (Algebra.adjoin F Set.univ) ⊤
rw₃ rw₄ : Eq.{u_1 + 1} (α := Subalgebra F K) ⊤ ⊤
⊢ Eq (α := Subalgebra F K) (Algebra.adjoin F (↑(HPow.hPow (α := K[X]) X (Fintype.card K) - X).roots.toFinset : Set K)) ⊤

Tactic:
rw [FiniteField.roots_X_pow_card_sub_X, val_toFinset, coe_univ, Algebra.adjoin_univ]

Premises used: Finset.val_toFinset, Finset.coe_univ, FiniteField.roots_X_pow_card_sub_X, Algebra.adjoin_univ
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
F : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : Field F
inst_3 : Algebra F K
trans :
  Eq (α := Subalgebra F K) (Algebra.adjoin F ((HPow.hPow (α := F[X]) X (Fintype.card K) - X).rootSet K))
    (Algebra.adjoin F (↑(HPow.hPow (α := K[X]) X (Fintype.card K) - X).roots.toFinset : Set K))
trans₁ trans₂ :
  Eq (α := Subalgebra F K) (Algebra.adjoin F (↑(HPow.hPow (α := K[X]) X (Fintype.card K) - X).roots.toFinset : Set K)) ⊤
⊢ Eq (α := Subalgebra F K) (Algebra.adjoin F ((HPow.hPow (α := F[X]) X (Fintype.card K) - X).rootSet K)) ⊤

Tactic:
classical
    trans Algebra.adjoin F ((roots (X ^ Fintype.card K - X : K[X])).toFinset : Set K)
    · simp only [rootSet, aroots, Polynomial.map_pow, map_X, Polynomial.map_sub]
    · rw [FiniteField.roots_X_pow_card_sub_X, val_toFinset, coe_univ, Algebra.adjoin_univ]

Premises used: Finset.val_toFinset, Finset.coe_univ, FiniteField.roots_X_pow_card_sub_X, Polynomial.rootSet, Polynomial.map_pow, Polynomial.map_X, Algebra.adjoin_univ, Polynomial.aroots, Polynomial.map_sub
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
inst : CommRing K
p q : ℕ
inst_1 : CharP K p
h : p ∣ q
h₁ :
  1 * (HPow.hPow (α := K[X]) X q - X) +
      HMul.hMul (β := K[X]) (HPow.hPow (α := K[X]) X q - X - 1)
        ((derivative : (a : K[X]) → K[X]) (HPow.hPow (α := K[X]) X q - X) : K[X]) =
    1
⊢ (HPow.hPow (α := K[X]) X q - X).Separable

Tactic:
use 1, X ^ q - X - 1

Premises used: Polynomial.X
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
inst : CommRing K
p q : ℕ
inst_1 : CharP K p
h : p ∣ q
⊢ Eq.{u_1 + 1} (α := K[X]) (↑q : K[X]) 0

Tactic:
rw [← CharP.cast_eq_zero_iff K[X] p] at h

Premises used: Polynomial, CharP.cast_eq_zero_iff
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
inst : CommRing K
p q : ℕ
inst_1 : CharP K p
h : Eq.{u_1 + 1} (α := K[X]) (↑q : K[X]) 0
h₁ :
  1 * (HPow.hPow (α := K[X]) X q - X) +
      (HPow.hPow (α := K[X]) X q - X - 1) * (0 * HPow.hPow (α := K[X]) X (q - 1) - 1) =
    1
⊢ 1 * (HPow.hPow (α := K[X]) X q - X) +
      HMul.hMul (β := K[X]) (HPow.hPow (α := K[X]) X q - X - 1)
        ((derivative : (a : K[X]) → K[X]) (HPow.hPow (α := K[X]) X q - X) : K[X]) =
    1

Tactic:
rw [derivative_sub, derivative_X_pow, derivative_X, C_eq_natCast, h]

Premises used: Polynomial.derivative_X, Polynomial.C_eq_natCast, Polynomial.derivative_X_pow, Polynomial.derivative_sub
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
inst : CommRing K
p q : ℕ
inst_1 : CharP K p
h : Eq.{u_1 + 1} (α := K[X]) (↑q : K[X]) 0
⊢ 1 * (HPow.hPow (α := K[X]) X q - X) +
      (HPow.hPow (α := K[X]) X q - X - 1) * (0 * HPow.hPow (α := K[X]) X (q - 1) - 1) =
    1

Tactic:
ring
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
haveI : ∀ (this : Fintype (GaloisField p n)), Module.finrank (ZMod p) (GaloisField p n) = n
⊢ Module.finrank (ZMod p) (GaloisField p n) = 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
this : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X
⊢ 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)
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
⊢ g_poly ≠ 0

Tactic:
have aux : g_poly ≠ 0 := FiniteField.X_pow_card_pow_sub_X_ne_zero _ h hp
-- Module: Mathlib.FieldTheory.Finite.GaloisField
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
⊢ Fintype.card (↑(g_poly.rootSet (GaloisField p n)) : Type) = g_poly.natDegree

Tactic:
have key : Fintype.card (g_poly.rootSet (GaloisField p n)) = g_poly.natDegree :=
    card_rootSet_eq_natDegree (galois_poly_separable p _ (dvd_pow (dvd_refl p) h))
      (SplittingField.splits (g_poly : (ZMod p)[X]))
-- Module: Mathlib.FieldTheory.Finite.GaloisField
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) = g_poly.natDegree
⊢ g_poly.natDegree = p ^ n

Tactic:
have nat_degree_eq : g_poly.natDegree = p ^ n :=
    FiniteField.X_pow_card_pow_sub_X_natDegree_eq _ h hp
-- Module: Mathlib.FieldTheory.Finite.GaloisField
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) = g_poly.natDegree
nat_degree_eq : g_poly.natDegree = p ^ n
⊢ Fintype.card (↑(g_poly.rootSet (GaloisField p n)) : Type) = p ^ n

Tactic:
rw [nat_degree_eq] at key
-- Module: Mathlib.FieldTheory.Finite.GaloisField
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) = g_poly.natDegree
nat_degree_eq : g_poly.natDegree = p ^ n
key₁ : Fintype.card (↑(g_poly.rootSet (GaloisField p n)) : Type) = p ^ n
⊢ g_poly.natDegree = p ^ n

Tactic:
rw [nat_degree_eq] at key
-- Module: Mathlib.FieldTheory.Finite.GaloisField
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
key : Fintype.card (↑(g_poly.rootSet (GaloisField p n)) : Type) = p ^ n
nat_degree_eq : g_poly.natDegree = p ^ n
this : Eq (α := Set (GaloisField p n)) (g_poly.rootSet (GaloisField p n)) Set.univ
⊢ Fintype.card (GaloisField p n) = p ^ n

Tactic:
simp_rw [this, ← Fintype.ofEquiv_card (Equiv.Set.univ _)] at key

Premises used: Fintype.ofEquiv_card, Equiv.Set.univ
-- Module: Mathlib.FieldTheory.Finite.GaloisField
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
⊢ p ^ Module.finrank (ZMod p) (GaloisField p n) = p ^ n

Tactic:
rw [@Module.card_eq_pow_finrank (K := ZMod p), ZMod.card] at key

Premises used: Module.card_eq_pow_finrank, ZMod.card
-- Module: Mathlib.FieldTheory.Finite.GaloisField
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 : p ^ Module.finrank (ZMod p) (GaloisField p n) = p ^ n
⊢ Module.finrank (ZMod p) (GaloisField p n) = n

Tactic:
Nat.pow_right_injective (Nat.Prime.one_lt' p).out key

Premises used: Nat.pow_right_injective, Fact.out
-- Module: Mathlib.FieldTheory.Finite.GaloisField
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 : p ^ Module.finrank (ZMod p) (GaloisField p n) = p ^ n
⊢ Module.finrank (ZMod p) (GaloisField p n) = n

Tactic:
exact Nat.pow_right_injective (Nat.Prime.one_lt' p).out key

Premises used: Nat.pow_right_injective, Fact.out
-- Module: Mathlib.FieldTheory.Finite.GaloisField
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
suffices : Eq (α := Set (GaloisField p n)) (g_poly.rootSet (GaloisField p n)) Set.univ
⊢ Module.finrank (ZMod p) (GaloisField p n) = n

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
-- Module: Mathlib.FieldTheory.Finite.GaloisField
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
rw : ∀ (x : GaloisField p n), Membership.mem (γ := Set (GaloisField p n)) (g_poly.rootSet (GaloisField p n)) x
⊢ Eq (α := Set (GaloisField p n)) (g_poly.rootSet (GaloisField p n)) Set.univ

Tactic:
rw [Set.eq_univ_iff_forall]

Premises used: Set.eq_univ_iff_forall
-- Module: Mathlib.FieldTheory.Finite.GaloisField
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
key : Fintype.card (↑(g_poly.rootSet (GaloisField p n)) : Type) = p ^ n
nat_degree_eq : g_poly.natDegree = p ^ n
this :
  ∀ (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
⊢ ∀ (x : GaloisField p n), Membership.mem (γ := Set (GaloisField p n)) (g_poly.rootSet (GaloisField p n)) x

Tactic:
simpa
-- Module: Mathlib.FieldTheory.Finite.GaloisField
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
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
⊢ ∀ (x : GaloisField p n), Membership.mem (γ := Set (GaloisField p n)) (g_poly.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
-- Module: Mathlib.FieldTheory.Finite.GaloisField
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
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
⊢ ∀ (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:
rw [← SplittingField.adjoin_rootSet]

Premises used: Polynomial.SplittingField.adjoin_rootSet
-- Module: Mathlib.FieldTheory.Finite.GaloisField
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
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
⊢ ∀ (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:
simp_rw [Algebra.mem_adjoin_iff]

Premises used: Algebra.mem_adjoin_iff
-- Module: Mathlib.FieldTheory.Finite.GaloisField
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
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
⊢ Membership.mem (γ := Set (GaloisField p n)) ((HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X).rootSet (GaloisField p n)) x

Tactic:
cases p
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
n : ℕ
h : n ≠ 0
h_prime : Fact (Nat.Prime 0)
this : Fintype (GaloisField 0 n)
g_poly : (ZMod 0)[X] := 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 hp
-- 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
⊢ 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:
Subring.closure_induction ?_ ?_ ?_ ?_ ?_ ?_ hx

Premises used: Subring.closure_induction