awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
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
⊢ f.natDegree ∣ Module.finrank K (Extension K p n)
have inr : Splits (R := Extension K p n) (Polynomial.map (algebraMap K (Extension K p n)) f)
Tactic: apply Irreducible.natDegree_dvd_finrank hi
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
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)) f)
have inr : 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: refine Splits.of_dvd ?_ ?_ (map_dvd (algebraMap K (Extension K p n)) h)
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
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
inr :
  Splits (R := Extension K p n)
    (Polynomial.map (algebraMap K (Extension K p n)) (HPow.hPow (α := K[X]) X (Nat.card K ^ n) - X))
⊢ Splits (R := Extension K p n) (Polynomial.map (algebraMap K (Extension K p n)) f)
have inr₁ : 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: refine Splits.of_dvd ?_ ?_ (map_dvd (algebraMap K (Extension K p n)) h)
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (hypothesis)
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
⊢ Splits (Polynomial.map (algebraMap F K) (HPow.hPow (α := F[X]) X (Fintype.card K) - X))
have h : (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
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
⊢ Splits (Polynomial.map (algebraMap F K) (HPow.hPow (α := F[X]) X (Fintype.card K) - X))
have 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))
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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))
⊢ Splits (Polynomial.map (algebraMap F K) (HPow.hPow (α := F[X]) X (Fintype.card K) - X))
have 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
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
⊢ Splits (Polynomial.map (algebraMap F K) (HPow.hPow (α := F[X]) X (Fintype.card K) - X))
have 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
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
⊢ Splits (Polynomial.map (algebraMap F K) (HPow.hPow (α := F[X]) X (Fintype.card K) - X))
have rw₃ : (HPow.hPow (α := K[X]) X (Fintype.card K) - X).roots.card = (HPow.hPow (α := K[X]) X (Fintype.card K) - X).natDegree
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
⊢ Splits (Polynomial.map (algebraMap F K) (HPow.hPow (α := F[X]) X (Fintype.card K) - X))
have rw₄ : (HPow.hPow (α := K[X]) X (Fintype.card K) - X).roots.card = Fintype.card K
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
⊢ Splits (Polynomial.map (algebraMap F K) (HPow.hPow (α := F[X]) X (Fintype.card K) - X))
have rw₅ : Multiset.card.{u_1} (α := K) (val univ) = Fintype.card K
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
⊢ Splits (Polynomial.map (algebraMap F K) (HPow.hPow (α := F[X]) X (Fintype.card K) - X))
have rw₆ : Finset.card.{u_1} (α := K) univ = Fintype.card K
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
⊢ Splits (Polynomial.map (algebraMap F K) (HPow.hPow (α := F[X]) X (Fintype.card K) - X))
have rw₇ : Fintype.card K = Fintype.card K
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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)) ⊤
have 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))
Tactic: trans Algebra.adjoin F ((roots (X ^ Fintype.card K - X : K[X])).toFinset : Set K)
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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))
⊢ Eq (α := Subalgebra F K) (Algebra.adjoin F ((HPow.hPow (α := F[X]) X (Fintype.card K) - X).rootSet K)) ⊤
have trans₁ : Eq (α := Subalgebra F K) (Algebra.adjoin F (↑(HPow.hPow (α := K[X]) X (Fintype.card K) - X).roots.toFinset : Set K)) ⊤
Tactic: trans Algebra.adjoin F ((roots (X ^ Fintype.card K - X : K[X])).toFinset : Set K)
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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 (α := K[X]) X (Fintype.card K) - X).roots.toFinset : Set K)) ⊤
have rw : Eq (α := Subalgebra F K) (Algebra.adjoin F (↑(Multiset.toFinset (val univ)) : Set K)) ⊤
Tactic: rw [FiniteField.roots_X_pow_card_sub_X, val_toFinset, coe_univ, Algebra.adjoin_univ]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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)) ⊤
⊢ Eq (α := Subalgebra F K) (Algebra.adjoin F (↑(HPow.hPow (α := K[X]) X (Fintype.card K) - X).roots.toFinset : Set K)) ⊤
have rw₁ : Eq (α := Subalgebra F K) (Algebra.adjoin F (↑univ : Set K)) ⊤
Tactic: rw [FiniteField.roots_X_pow_card_sub_X, val_toFinset, coe_univ, Algebra.adjoin_univ]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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)) ⊤
⊢ Eq (α := Subalgebra F K) (Algebra.adjoin F (↑(HPow.hPow (α := K[X]) X (Fintype.card K) - X).roots.toFinset : Set K)) ⊤
have rw₂ : Eq.{u_1 + 1} (α := Subalgebra F K) (Algebra.adjoin F Set.univ) ⊤
Tactic: rw [FiniteField.roots_X_pow_card_sub_X, val_toFinset, coe_univ, Algebra.adjoin_univ]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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) ⊤
⊢ Eq (α := Subalgebra F K) (Algebra.adjoin F (↑(HPow.hPow (α := K[X]) X (Fintype.card K) - X).roots.toFinset : Set K)) ⊤
have rw₃ : Eq.{u_1 + 1} (α := Subalgebra F K) ⊤ ⊤
Tactic: rw [FiniteField.roots_X_pow_card_sub_X, val_toFinset, coe_univ, Algebra.adjoin_univ]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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)) ⊤
have 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))
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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))
⊢ Eq (α := Subalgebra F K) (Algebra.adjoin F ((HPow.hPow (α := F[X]) X (Fintype.card K) - X).rootSet K)) ⊤
have trans₁ : Eq (α := Subalgebra F K) (Algebra.adjoin F (↑(HPow.hPow (α := K[X]) X (Fintype.card K) - X).roots.toFinset : Set 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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
K : Type u_1
inst : CommRing K
p q : ℕ
inst_1 : CharP K p
h : p ∣ q
⊢ (HPow.hPow (α := K[X]) X q - X).Separable
have 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
Tactic: use 1, X ^ q - X - 1
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (hypothesis)
Goal:
K : Type u_1
inst : CommRing K
p q : ℕ
inst_1 : CharP K p
h : p ∣ q
⊢ 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
have h₁ : Eq.{u_1 + 1} (α := K[X]) (↑q : K[X]) 0
Tactic: rw [← CharP.cast_eq_zero_iff K[X] p] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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) +
      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
have 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
Tactic: rw [derivative_sub, derivative_X_pow, derivative_X, C_eq_natCast, h]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
⊢ Module.finrank (ZMod p) (GaloisField p n) = n
have haveI : ∀ (this : Fintype (GaloisField p n)), Module.finrank (ZMod p) (GaloisField p n) = n
Tactic: haveI : Fintype (GaloisField p n) := Fintype.ofFinite (GaloisField p n)
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (hypothesis)
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
⊢ Module.finrank (ZMod p) (GaloisField p n) = n
have hp : 1 < p
Tactic: have hp : 1 < p := h_prime.out.one_lt
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (hypothesis)
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
⊢ Module.finrank (ZMod p) (GaloisField p n) = n
have aux : g_poly ≠ 0
Tactic: have aux : g_poly ≠ 0 := FiniteField.X_pow_card_pow_sub_X_ne_zero _ h hp
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (hypothesis)
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
⊢ Module.finrank (ZMod p) (GaloisField p n) = n
have key : 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]))
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (hypothesis)
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
⊢ Module.finrank (ZMod p) (GaloisField p n) = n
have nat_degree_eq : 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
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (hypothesis)
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
⊢ Module.finrank (ZMod p) (GaloisField p n) = n
have key₁ : Fintype.card (↑(g_poly.rootSet (GaloisField p n)) : Type) = p ^ n
Tactic: rw [nat_degree_eq] at key
Cleared hypotheses: key, nat_degree_eq
-- 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
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
⊢ Module.finrank (ZMod p) (GaloisField p n) = n
have key₁ : Fintype.card (GaloisField p n) = p ^ n
Tactic: simp_rw [this, ← Fintype.ofEquiv_card (Equiv.Set.univ _)] at key
Cleared hypotheses: key