awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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)
⊢ Nat.card (GaloisField p n) = p ^ n
have haveI : ∀ (this : Fintype (GaloisField p n)), Nat.card (GaloisField p n) = p ^ n
Tactic: haveI : Fintype (GaloisField p n) := Fintype.ofFinite (GaloisField p n)
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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)
⊢ Nat.card (GaloisField p n) = p ^ n
have rw : Fintype.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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
⊢ Nat.card (GaloisField p n) = p ^ n
have rw₁ : Fintype.card (ZMod p) ^ Fintype.card ↥(IsNoetherian.finsetBasisIndex (ZMod p) (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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
⊢ Nat.card (GaloisField p n) = p ^ n
have rw₂ : Fintype.card (ZMod p) ^ Module.finrank (ZMod p) (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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
⊢ Nat.card (GaloisField p n) = p ^ n
have rw₃ : p ^ Module.finrank (ZMod p) (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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
⊢ Nat.card (GaloisField p n) = p ^ n
have rw₄ : 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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (hypothesis)
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
⊢ (HPow.hPow (α := (ZMod p)[X]) X p - X).Splits
have hp : 1 < p
Tactic: have hp : 1 < p := h_prime.out.one_lt
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
hp : 1 < p
⊢ (HPow.hPow (α := (ZMod p)[X]) X p - X).roots = val univ
have h : ZMod.commRing p = Field.toCommRing → p = Fintype.card (ZMod p)
Tactic: convert! FiniteField.roots_X_pow_card_sub_X (ZMod p)
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (hypothesis)
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
hp : 1 < p
⊢ (HPow.hPow (α := (ZMod p)[X]) X p - X).Splits
have h1 : (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
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (hypothesis)
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).Splits
have h2 : (HPow.hPow (α := (ZMod p)[X]) X p - X).natDegree = p
Tactic: have h2 := FiniteField.X_pow_card_sub_X_natDegree_eq (ZMod p) hp
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
⊢ (HPow.hPow (α := (ZMod p)[X]) X p - X).Splits
have 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
Tactic: cases p
Cleared hypotheses: p, h_prime, hp, h1, h2
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
⊢ (HPow.hPow (α := (ZMod p)[X]) X p - X).Splits
have 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
Tactic: cases p
Cleared hypotheses: p, h_prime, hp, h1, h2
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
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
have succ : (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).roots.card =
  (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).natDegree
Tactic: rw [splits_iff_card_roots, h1, ← Finset.card_def, Finset.card_univ, h2, ZMod.card]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
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
succ :
  (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).roots.card =
    (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).natDegree
⊢ (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).Splits
have succ₁ : Multiset.card (α := ZMod (n + 1)) (val univ) = (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).natDegree
Tactic: rw [splits_iff_card_roots, h1, ← Finset.card_def, Finset.card_univ, h2, ZMod.card]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
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
succ :
  (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).roots.card =
    (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).natDegree
succ₁ : Multiset.card (α := ZMod (n + 1)) (val univ) = (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).natDegree
⊢ (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).Splits
have succ₂ : Finset.card (α := ZMod (n + 1)) univ = (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).natDegree
Tactic: rw [splits_iff_card_roots, h1, ← Finset.card_def, Finset.card_univ, h2, ZMod.card]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
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
succ :
  (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).roots.card =
    (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).natDegree
succ₁ : Multiset.card (α := ZMod (n + 1)) (val univ) = (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).natDegree
succ₂ : Finset.card (α := ZMod (n + 1)) univ = (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).natDegree
⊢ (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).Splits
have succ₃ : Fintype.card (ZMod (n + 1)) = (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).natDegree
Tactic: rw [splits_iff_card_roots, h1, ← Finset.card_def, Finset.card_univ, h2, ZMod.card]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
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
succ :
  (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).roots.card =
    (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).natDegree
succ₁ : Multiset.card (α := ZMod (n + 1)) (val univ) = (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).natDegree
succ₂ : Finset.card (α := ZMod (n + 1)) univ = (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).natDegree
succ₃ : Fintype.card (ZMod (n + 1)) = (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).natDegree
⊢ (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).Splits
have succ₄ : Fintype.card (ZMod (n + 1)) = n + 1
Tactic: rw [splits_iff_card_roots, h1, ← Finset.card_def, Finset.card_univ, h2, ZMod.card]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
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
succ :
  (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).roots.card =
    (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).natDegree
succ₁ : Multiset.card (α := ZMod (n + 1)) (val univ) = (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).natDegree
succ₂ : Finset.card (α := ZMod (n + 1)) univ = (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).natDegree
succ₃ : Fintype.card (ZMod (n + 1)) = (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).natDegree
succ₄ : Fintype.card (ZMod (n + 1)) = n + 1
⊢ (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).Splits
have succ₅ : n + 1 = n + 1
Tactic: rw [splits_iff_card_roots, h1, ← Finset.card_def, Finset.card_univ, h2, ZMod.card]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n_1 p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
⊢ HPow.hPow (α := (ZMod p)[X]) X (HPow.hPow (β := ℕ) p 1) = HPow.hPow (α := (ZMod p)[X]) X (Fintype.card (ZMod p))
have rw : HPow.hPow (α := (ZMod p)[X]) X p = HPow.hPow (α := (ZMod p)[X]) X (Fintype.card (ZMod p))
Tactic: rw [pow_one, ZMod.card p]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n_1 p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
rw : HPow.hPow (α := (ZMod p)[X]) X p = HPow.hPow (α := (ZMod p)[X]) X (Fintype.card (ZMod p))
⊢ HPow.hPow (α := (ZMod p)[X]) X (HPow.hPow (β := ℕ) p 1) = HPow.hPow (α := (ZMod p)[X]) X (Fintype.card (ZMod p))
have rw₁ : HPow.hPow (α := (ZMod p)[X]) X p = HPow.hPow (α := (ZMod p)[X]) X p
Tactic: rw [pow_one, ZMod.card p]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n_1 p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : HPow.hPow (α := (ZMod p)[X]) X (HPow.hPow (β := ℕ) p 1) = HPow.hPow (α := (ZMod p)[X]) X (Fintype.card (ZMod p))
⊢ IsSplittingField (ZMod p) (ZMod p) (HPow.hPow (α := (ZMod p)[X]) X (HPow.hPow (β := ℕ) p 1) - X)
have rw : IsSplittingField (ZMod p) (ZMod p) (HPow.hPow (α := (ZMod p)[X]) X (Fintype.card (ZMod p)) - X)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : Algebra (ZMod p) K
inst_2 : Finite K
⊢ Splits (Polynomial.map (algebraMap (ZMod p) K) (HPow.hPow (α := (ZMod p)[X]) X (Nat.card K) - X))
have haveI : ∀ (this : Fintype K), Splits (Polynomial.map (algebraMap (ZMod p) K) (HPow.hPow (α := (ZMod p)[X]) X (Nat.card K) - X))
Tactic: haveI : Fintype K := Fintype.ofFinite K
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : Algebra (ZMod p) K
inst_2 : Finite K
this : Fintype K
⊢ Splits (Polynomial.map (algebraMap (ZMod p) K) (HPow.hPow (α := (ZMod p)[X]) X (Nat.card K) - X))
have rw : Splits (Polynomial.map (algebraMap (ZMod p) K) (HPow.hPow (α := (ZMod p)[X]) X (Fintype.card K) - X))
Tactic: rw [Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (hypothesis)
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
K : Type u_1
inst : Field K
inst_1 : Algebra (ZMod p) K
h : Nat.card K = p ^ n
⊢ IsSplittingField (ZMod p) K (HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X)
have this : Finite K
Tactic: haveI : Finite K := (Nat.card_pos_iff.mp (h ▸ pow_pos h_prime.1.pos n)).2
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
K : Type u_1
inst : Field K
inst_1 : Algebra (ZMod p) K
h : Nat.card K = p ^ n
this : Finite K
⊢ IsSplittingField (ZMod p) K (HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X)
have haveI : ∀ (this : Fintype K), IsSplittingField (ZMod p) K (HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X)
Tactic: haveI : Fintype K := Fintype.ofFinite K
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
K : Type u_1
inst : Field K
inst_1 : Algebra (ZMod p) K
h : Nat.card K = p ^ n
this_1 : Finite K
this : Fintype K
⊢ IsSplittingField (ZMod p) K (HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X)
have rw : IsSplittingField (ZMod p) K (HPow.hPow (α := (ZMod p)[X]) X (Fintype.card K) - X)
Tactic: rw [← h, Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
K : Type u_1
inst : Field K
⊢ (HPow.hPow (α := K[X]) X (Nat.card K) - X).Splits
have inl : ∀ (val : Fintype K), (HPow.hPow (α := K[X]) X (Nat.card K) - X).Splits
Tactic: cases fintypeOrInfinite K
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
K : Type u_1
inst : Field K
inl : ∀ (val : Fintype K), (HPow.hPow (α := K[X]) X (Nat.card K) - X).Splits
⊢ (HPow.hPow (α := K[X]) X (Nat.card K) - X).Splits
have inr : Infinite K → (HPow.hPow (α := K[X]) X (Nat.card K) - X).Splits
Tactic: cases fintypeOrInfinite K
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (hypothesis)
Goal:
K : Type u_1
inst : Field K
val : Fintype K
⊢ (HPow.hPow (α := K[X]) X (Nat.card K) - X).Splits
have this : Splits (Polynomial.map (algebraMap K K) (HPow.hPow (α := K[X]) X (Fintype.card K) - X))
Tactic: have := (IsSplittingField.splits (L := K) (X ^ (Fintype.card K) - X : K[X]))
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
K : Type u_1
inst : Field K
val : Infinite K
⊢ (HPow.hPow (α := K[X]) X (Nat.card K) - X).Splits
have inr : (-(HPow.hPow (α := K[X]) X (Nat.card K) - X)).Splits
Tactic: rw [← Polynomial.splits_neg_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n_1 p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
K_1 : Type u_1
inst_1 : Field K_1
inst_2 : Algebra (ZMod p) K_1
K : Type u_2
K' : Type u_3
inst_3 : Field K
inst_4 : Field K'
inst_5 : Finite K'
inst_6 : Algebra K K'
⊢ IsGalois K K'
have intro : ∀ (val : Fintype K'), IsGalois K K'
Tactic: cases nonempty_fintype K'
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n_1 p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
K_1 : Type u_1
inst_1 : Field K_1
inst_2 : Algebra (ZMod p) K_1
K : Type u_2
K' : Type u_3
inst_3 : Field K
inst_4 : Field K'
inst_5 : Finite K'
inst_6 : Algebra K K'
val : Fintype K'
⊢ IsGalois K K'
have intro : ∀ (p : ℕ) (hp : CharP K p), IsGalois K K'
Tactic: obtain ⟨p, hp⟩ := CharP.exists K
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (hypothesis)
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n_1 p_2 : ℕ
h_prime : Fact (Nat.Prime p_2)
n : ℕ
K_1 : Type u_1
inst_1 : Field K_1
inst_2 : Algebra (ZMod p_2) K_1
K : Type u_2
K' : Type u_3
inst_3 : Field K
inst_4 : Field K'
inst_5 : Finite K'
inst_6 : Algebra K K'
val : Fintype K'
p : ℕ
hp : CharP K p
this : CharP K p
⊢ IsGalois K K'
have this₁ : CharP K' p
Tactic: haveI : CharP K' p := charP_of_injective_algebraMap' K p
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (hypothesis)
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
x : K'
⊢ (algebraMap K K' : (a : K) → K') ((Algebra.norm K : (a : K') → K) x : K) = x ^ ((Nat.card K' - 1) / (Nat.card K - 1))
have this : Finite K
Tactic: have := Finite.of_injective _ (algebraMap K K').injective
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
x : K'
this : Finite K
⊢ (algebraMap K K' : (a : K) → K') ((Algebra.norm K : (a : K') → K) x : K) = x ^ ((Nat.card K' - 1) / (Nat.card K - 1))
have have : ∀ (this : Fintype K),
  (algebraMap K K' : (a : K) → K') ((Algebra.norm K : (a : K') → K) x : K) = x ^ ((Nat.card K' - 1) / (Nat.card K - 1))
Tactic: have := Fintype.ofFinite K
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
x : K'
this_1 : Finite K
this : Fintype K
⊢ (algebraMap K K' : (a : K) → K') ((Algebra.norm K : (a : K') → K) x : K) = x ^ ((Nat.card K' - 1) / (Nat.card K - 1))
have have : ∀ (this : Fintype K'),
  (algebraMap K K' : (a : K) → K') ((Algebra.norm K : (a : K') → K) x : K) = x ^ ((Nat.card K' - 1) / (Nat.card K - 1))
Tactic: have := Fintype.ofFinite K'
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
x : K'
this_1 : Finite K
this_2 : Fintype K
this : Fintype K'
⊢ (algebraMap K K' : (a : K) → K') ((Algebra.norm K : (a : K') → K) x : K) = x ^ ((Nat.card K' - 1) / (Nat.card K - 1))
have simp_rw : (algebraMap K K' : (a : K) → K') ((Algebra.norm K : (a : K') → K) x : K) =
  x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
Tactic: simp_rw [← Fintype.card_eq_nat_card, Algebra.norm_eq_prod_automorphisms,
    ← (bijective_frobeniusAlgEquivOfAlgebraic_pow K K').prod_comp, AlgEquiv.coe_pow,
    coe_frobeniusAlgEquivOfAlgebraic, pow_iterate, Finset.prod_pow_eq_pow_sum,
    Fin.sum_univ_eq_sum_range, Nat.geomSum_eq Fintype.one_lt_card, ← Module.card_eq_pow_finrank]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
x : K'
this_1 : Finite K
this_2 : Fintype K
this : Fintype K'
simp_rw :
  (algebraMap K K' : (a : K) → K') ((Algebra.norm K : (a : K') → K) x : K) =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
⊢ (algebraMap K K' : (a : K) → K') ((Algebra.norm K : (a : K') → K) x : K) = x ^ ((Nat.card K' - 1) / (Nat.card K - 1))
have simp_rw₁ : ∏ σ : Gal(K'/K), (σ : (a : K') → K') x = x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
Tactic: simp_rw [← Fintype.card_eq_nat_card, Algebra.norm_eq_prod_automorphisms,
    ← (bijective_frobeniusAlgEquivOfAlgebraic_pow K K').prod_comp, AlgEquiv.coe_pow,
    coe_frobeniusAlgEquivOfAlgebraic, pow_iterate, Finset.prod_pow_eq_pow_sum,
    Fin.sum_univ_eq_sum_range, Nat.geomSum_eq Fintype.one_lt_card, ← Module.card_eq_pow_finrank]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
x : K'
this_1 : Finite K
this_2 : Fintype K
this : Fintype K'
simp_rw :
  (algebraMap K K' : (a : K) → K') ((Algebra.norm K : (a : K') → K) x : K) =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₁ : ∏ σ : Gal(K'/K), (σ : (a : K') → K') x = x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
⊢ (algebraMap K K' : (a : K) → K') ((Algebra.norm K : (a : K') → K) x : K) = x ^ ((Nat.card K' - 1) / (Nat.card K - 1))
have simp_rw₂ : ∏ i : Fin (Module.finrank K K'),
    (HPow.hPow (α := Gal(K'/K)) (frobeniusAlgEquivOfAlgebraic K K') (↑i : ℕ) : (a : K') → K') x =
  x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
Tactic: simp_rw [← Fintype.card_eq_nat_card, Algebra.norm_eq_prod_automorphisms,
    ← (bijective_frobeniusAlgEquivOfAlgebraic_pow K K').prod_comp, AlgEquiv.coe_pow,
    coe_frobeniusAlgEquivOfAlgebraic, pow_iterate, Finset.prod_pow_eq_pow_sum,
    Fin.sum_univ_eq_sum_range, Nat.geomSum_eq Fintype.one_lt_card, ← Module.card_eq_pow_finrank]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
x : K'
this_1 : Finite K
this_2 : Fintype K
this : Fintype K'
simp_rw :
  (algebraMap K K' : (a : K) → K') ((Algebra.norm K : (a : K') → K) x : K) =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₁ : ∏ σ : Gal(K'/K), (σ : (a : K') → K') x = x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₂ :
  ∏ i : Fin (Module.finrank K K'),
      (HPow.hPow (α := Gal(K'/K)) (frobeniusAlgEquivOfAlgebraic K K') (↑i : ℕ) : (a : K') → K') x =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
⊢ (algebraMap K K' : (a : K) → K') ((Algebra.norm K : (a : K') → K) x : K) = x ^ ((Nat.card K' - 1) / (Nat.card K - 1))
have simp_rw₃ : ∏ x_1 : Fin (Module.finrank K K'), (⇑(frobeniusAlgEquivOfAlgebraic K K') : (a : K') → K')^[(↑x_1 : ℕ)] x =
  x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
Tactic: simp_rw [← Fintype.card_eq_nat_card, Algebra.norm_eq_prod_automorphisms,
    ← (bijective_frobeniusAlgEquivOfAlgebraic_pow K K').prod_comp, AlgEquiv.coe_pow,
    coe_frobeniusAlgEquivOfAlgebraic, pow_iterate, Finset.prod_pow_eq_pow_sum,
    Fin.sum_univ_eq_sum_range, Nat.geomSum_eq Fintype.one_lt_card, ← Module.card_eq_pow_finrank]