awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
this : Fintype (Extension k p n)
⊢ IsSplittingField k (Extension k p n) (HPow.hPow (α := k[X]) X (Nat.card k ^ n) - X)
have h : Nat.card k ^ n = Fintype.card (Extension k p n)
Tactic: convert! FiniteField.isSplittingField_sub (Extension k p n) k
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
this : Fintype (Extension k p n)
⊢ Nat.card k ^ n = Fintype.card (Extension k p n)
have h : Nat.card k ^ n = Nat.card (Extension k p n)
Tactic: rw [Fintype.card_eq_nat_card, natCard_extension]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
this : Fintype (Extension k p n)
h : Nat.card k ^ n = Nat.card (Extension k p n)
⊢ Nat.card k ^ n = Fintype.card (Extension k p n)
have h₁ : Nat.card k ^ n = Nat.card k ^ n
Tactic: rw [Fintype.card_eq_nat_card, natCard_extension]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
i : ℕ
ih :
  ∀ {x : Extension k p n},
    (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i : (a : Extension k p n) → Extension k p n) x =
      x ^ Nat.card k ^ i
x : Extension k p n
⊢ (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) (i + 1) : (a : Extension k p n) → Extension k p n) x =
    x ^ Nat.card k ^ (i + 1)
have succ : (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i *
        HPow.hPow (α := Gal(Extension k p n/k)) (β := ℕ) (frob k p n) 1 :
      (a : Extension k p n) → Extension k p n)
    x =
  x ^ Nat.card k ^ (i + 1)
Tactic: rw [pow_add, pow_one, AlgEquiv.mul_apply, ih, frob_apply, ← pow_mul, ← Nat.pow_add_one']
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
i : ℕ
ih :
  ∀ {x : Extension k p n},
    (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i : (a : Extension k p n) → Extension k p n) x =
      x ^ Nat.card k ^ i
x : Extension k p n
succ :
  (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i *
          HPow.hPow (α := Gal(Extension k p n/k)) (β := ℕ) (frob k p n) 1 :
        (a : Extension k p n) → Extension k p n)
      x =
    x ^ Nat.card k ^ (i + 1)
⊢ (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) (i + 1) : (a : Extension k p n) → Extension k p n) x =
    x ^ Nat.card k ^ (i + 1)
have succ₁ : (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i * frob k p n : (a : Extension k p n) → Extension k p n) x =
  x ^ Nat.card k ^ (i + 1)
Tactic: rw [pow_add, pow_one, AlgEquiv.mul_apply, ih, frob_apply, ← pow_mul, ← Nat.pow_add_one']
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
i : ℕ
ih :
  ∀ {x : Extension k p n},
    (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i : (a : Extension k p n) → Extension k p n) x =
      x ^ Nat.card k ^ i
x : Extension k p n
succ :
  (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i *
          HPow.hPow (α := Gal(Extension k p n/k)) (β := ℕ) (frob k p n) 1 :
        (a : Extension k p n) → Extension k p n)
      x =
    x ^ Nat.card k ^ (i + 1)
succ₁ :
  (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i * frob k p n : (a : Extension k p n) → Extension k p n) x =
    x ^ Nat.card k ^ (i + 1)
⊢ (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) (i + 1) : (a : Extension k p n) → Extension k p n) x =
    x ^ Nat.card k ^ (i + 1)
have succ₂ : (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i : (a : Extension k p n) → Extension k p n)
    ((frob k p n : (a : Extension k p n) → Extension k p n) x) =
  x ^ Nat.card k ^ (i + 1)
Tactic: rw [pow_add, pow_one, AlgEquiv.mul_apply, ih, frob_apply, ← pow_mul, ← Nat.pow_add_one']
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
i : ℕ
ih :
  ∀ {x : Extension k p n},
    (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i : (a : Extension k p n) → Extension k p n) x =
      x ^ Nat.card k ^ i
x : Extension k p n
succ :
  (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i *
          HPow.hPow (α := Gal(Extension k p n/k)) (β := ℕ) (frob k p n) 1 :
        (a : Extension k p n) → Extension k p n)
      x =
    x ^ Nat.card k ^ (i + 1)
succ₁ :
  (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i * frob k p n : (a : Extension k p n) → Extension k p n) x =
    x ^ Nat.card k ^ (i + 1)
succ₂ :
  (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i : (a : Extension k p n) → Extension k p n)
      ((frob k p n : (a : Extension k p n) → Extension k p n) x) =
    x ^ Nat.card k ^ (i + 1)
⊢ (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) (i + 1) : (a : Extension k p n) → Extension k p n) x =
    x ^ Nat.card k ^ (i + 1)
have succ₃ : HPow.hPow (α := Extension k p n) ((frob k p n : (a : Extension k p n) → Extension k p n) x : Extension k p n)
    (Nat.card k ^ i) =
  x ^ Nat.card k ^ (i + 1)
Tactic: rw [pow_add, pow_one, AlgEquiv.mul_apply, ih, frob_apply, ← pow_mul, ← Nat.pow_add_one']
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
i : ℕ
ih :
  ∀ {x : Extension k p n},
    (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i : (a : Extension k p n) → Extension k p n) x =
      x ^ Nat.card k ^ i
x : Extension k p n
succ :
  (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i *
          HPow.hPow (α := Gal(Extension k p n/k)) (β := ℕ) (frob k p n) 1 :
        (a : Extension k p n) → Extension k p n)
      x =
    x ^ Nat.card k ^ (i + 1)
succ₁ :
  (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i * frob k p n : (a : Extension k p n) → Extension k p n) x =
    x ^ Nat.card k ^ (i + 1)
succ₂ :
  (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i : (a : Extension k p n) → Extension k p n)
      ((frob k p n : (a : Extension k p n) → Extension k p n) x) =
    x ^ Nat.card k ^ (i + 1)
succ₃ :
  HPow.hPow (α := Extension k p n) ((frob k p n : (a : Extension k p n) → Extension k p n) x : Extension k p n)
      (Nat.card k ^ i) =
    x ^ Nat.card k ^ (i + 1)
⊢ (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) (i + 1) : (a : Extension k p n) → Extension k p n) x =
    x ^ Nat.card k ^ (i + 1)
have succ₄ : (x ^ Nat.card k) ^ Nat.card k ^ i = x ^ Nat.card k ^ (i + 1)
Tactic: rw [pow_add, pow_one, AlgEquiv.mul_apply, ih, frob_apply, ← pow_mul, ← Nat.pow_add_one']
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
i : ℕ
ih :
  ∀ {x : Extension k p n},
    (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i : (a : Extension k p n) → Extension k p n) x =
      x ^ Nat.card k ^ i
x : Extension k p n
succ :
  (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i *
          HPow.hPow (α := Gal(Extension k p n/k)) (β := ℕ) (frob k p n) 1 :
        (a : Extension k p n) → Extension k p n)
      x =
    x ^ Nat.card k ^ (i + 1)
succ₁ :
  (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i * frob k p n : (a : Extension k p n) → Extension k p n) x =
    x ^ Nat.card k ^ (i + 1)
succ₂ :
  (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i : (a : Extension k p n) → Extension k p n)
      ((frob k p n : (a : Extension k p n) → Extension k p n) x) =
    x ^ Nat.card k ^ (i + 1)
succ₃ :
  HPow.hPow (α := Extension k p n) ((frob k p n : (a : Extension k p n) → Extension k p n) x : Extension k p n)
      (Nat.card k ^ i) =
    x ^ Nat.card k ^ (i + 1)
succ₄ : (x ^ Nat.card k) ^ Nat.card k ^ i = x ^ Nat.card k ^ (i + 1)
⊢ (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) (i + 1) : (a : Extension k p n) → Extension k p n) x =
    x ^ Nat.card k ^ (i + 1)
have succ₅ : x ^ (Nat.card k * Nat.card k ^ i) = x ^ Nat.card k ^ (i + 1)
Tactic: rw [pow_add, pow_one, AlgEquiv.mul_apply, ih, frob_apply, ← pow_mul, ← Nat.pow_add_one']
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
i : ℕ
ih :
  ∀ {x : Extension k p n},
    (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i : (a : Extension k p n) → Extension k p n) x =
      x ^ Nat.card k ^ i
x : Extension k p n
succ :
  (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i *
          HPow.hPow (α := Gal(Extension k p n/k)) (β := ℕ) (frob k p n) 1 :
        (a : Extension k p n) → Extension k p n)
      x =
    x ^ Nat.card k ^ (i + 1)
succ₁ :
  (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i * frob k p n : (a : Extension k p n) → Extension k p n) x =
    x ^ Nat.card k ^ (i + 1)
succ₂ :
  (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i : (a : Extension k p n) → Extension k p n)
      ((frob k p n : (a : Extension k p n) → Extension k p n) x) =
    x ^ Nat.card k ^ (i + 1)
succ₃ :
  HPow.hPow (α := Extension k p n) ((frob k p n : (a : Extension k p n) → Extension k p n) x : Extension k p n)
      (Nat.card k ^ i) =
    x ^ Nat.card k ^ (i + 1)
succ₄ : (x ^ Nat.card k) ^ Nat.card k ^ i = x ^ Nat.card k ^ (i + 1)
succ₅ : x ^ (Nat.card k * Nat.card k ^ i) = x ^ Nat.card k ^ (i + 1)
⊢ (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) (i + 1) : (a : Extension k p n) → Extension k p n) x =
    x ^ Nat.card k ^ (i + 1)
have succ₆ : x ^ Nat.card k ^ (i + 1) = x ^ Nat.card k ^ (i + 1)
Tactic: rw [pow_add, pow_one, AlgEquiv.mul_apply, ih, frob_apply, ← pow_mul, ← Nat.pow_add_one']
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
i : ℕ
x : Extension k p n
⊢ (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i : (a : Extension k p n) → Extension k p n) x =
    x ^ Nat.card k ^ i
have zero : ∀ {x : Extension k p n},
  (HPow.hPow (α := Gal(Extension k p n/k)) (β := ℕ) (frob k p n) 0 : (a : Extension k p n) → Extension k p n) x =
    x ^ HPow.hPow (β := ℕ) (Nat.card k) 0
Tactic: induction i generalizing x with
  | zero => simp
  | succ i ih =>
      rw [pow_add, pow_one, AlgEquiv.mul_apply, ih, frob_apply, ← pow_mul, ← Nat.pow_add_one']
Cleared hypotheses: i, x
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
i : ℕ
x : Extension k p n
zero :
  ∀ {x : Extension k p n},
    (HPow.hPow (α := Gal(Extension k p n/k)) (β := ℕ) (frob k p n) 0 : (a : Extension k p n) → Extension k p n) x =
      x ^ HPow.hPow (β := ℕ) (Nat.card k) 0
⊢ (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i : (a : Extension k p n) → Extension k p n) x =
    x ^ Nat.card k ^ i
have succ : ∀ (i : ℕ)
  (ih :
    ∀ {x : Extension k p n},
      (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i : (a : Extension k p n) → Extension k p n) x =
        x ^ Nat.card k ^ i)
  {x : Extension k p n},
  (HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) (i + 1) : (a : Extension k p n) → Extension k p n) x =
    x ^ Nat.card k ^ (i + 1)
Tactic: induction i generalizing x with
  | zero => simp
  | succ i ih =>
      rw [pow_add, pow_one, AlgEquiv.mul_apply, ih, frob_apply, ← pow_mul, ← Nat.pow_add_one']
Cleared hypotheses: i, x
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
g : Gal(Extension k p n/k)
this : Fintype k := Fintype.ofFinite k
⊢ ∃ i < n, HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i = g
have obtain : ∀ (i : ℕ) (hi : i < Module.finrank k (Extension k p n)),
  ∃ i_1 < n,
    HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i_1 =
      (fun (n_1 : Fin (Module.finrank k (Extension k p n))) ↦
          HPow.hPow (α := Gal(Extension k p n/k)) (frobeniusAlgEquivOfAlgebraic k (Extension k p n)) (↑n_1 : ℕ))
        ⟨i, hi⟩
Tactic: obtain ⟨⟨i, hi⟩, rfl⟩ := (FiniteField.bijective_frobeniusAlgEquivOfAlgebraic_pow k
    (Extension k p n)).2 g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
this : Fintype k := Fintype.ofFinite k
i : ℕ
hi : i < Module.finrank k (Extension k p n)
⊢ HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i =
    (fun (n_1 : Fin (Module.finrank k (Extension k p n))) ↦
        HPow.hPow (α := Gal(Extension k p n/k)) (frobeniusAlgEquivOfAlgebraic k (Extension k p n)) (↑n_1 : ℕ))
      ⟨i, hi⟩
have h : ∀ (a : Extension k p n),
  Eq (α := Extension k p n)
    ((HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i : (a : Extension k p n) → Extension k p n) a :
      Extension k p n)
    (((fun (n_1 : Fin (Module.finrank k (Extension k p n))) ↦
              HPow.hPow (α := Gal(Extension k p n/k)) (frobeniusAlgEquivOfAlgebraic k (Extension k p n)) (↑n_1 : ℕ))
            ⟨i, hi⟩ :
          (a : Extension k p n) → Extension k p n)
        a :
      Extension k p n)
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
this : Fintype k := Fintype.ofFinite k
i : ℕ
hi : i < Module.finrank k (Extension k p n)
⊢ ∃ i_1 < n,
    HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i_1 =
      (fun (n_1 : Fin (Module.finrank k (Extension k p n))) ↦
          HPow.hPow (α := Gal(Extension k p n/k)) (frobeniusAlgEquivOfAlgebraic k (Extension k p n)) (↑n_1 : ℕ))
        ⟨i, hi⟩
have refine : i < n
Tactic: refine ⟨i, ?_, by ext; simp [frob]⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
this : Fintype k := Fintype.ofFinite k
i : ℕ
hi : i < Module.finrank k (Extension k p n)
⊢ i < n
have rwa : ∀ (hi : i < n), i < n
Tactic: rwa [finrank_extension] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
l : Type u_2
inst_5 : Field l
inst_6 : Algebra k l
h : Module.finrank k l = n
⊢ l ≃ₐ[k] Extension k p n
have refine : Nonempty.{u_2 + 1} (l ≃ₐ[k] Extension k p n)
Tactic: refine Nonempty.some ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (hypothesis)
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
l : Type u_2
inst_5 : Field l
inst_6 : Algebra k l
h : Module.finrank k l = n
⊢ Nonempty.{u_2 + 1} (l ≃ₐ[k] Extension k p n)
have this : Module.Finite k l
Tactic: have : Module.Finite k l := Module.finite_of_finrank_pos <| h ▸ NeZero.pos n
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (hypothesis)
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
l : Type u_2
inst_5 : Field l
inst_6 : Algebra k l
h : Module.finrank k l = n
this : Module.Finite k l
⊢ Nonempty.{u_2 + 1} (l ≃ₐ[k] Extension k p n)
have this₁ : Finite l
Tactic: have : Finite l := Module.finite_of_finite k
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
l : Type u_2
inst_5 : Field l
inst_6 : Algebra k l
h : Module.finrank k l = n
this_1 : Module.Finite k l
this : Finite l
⊢ Nonempty.{u_2 + 1} (l ≃ₐ[k] Extension k p n)
have have : ∀ (this : Fintype l), Nonempty.{u_2 + 1} (l ≃ₐ[k] Extension k p n)
Tactic: have : Fintype l := .ofFinite _
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
l : Type u_2
inst_5 : Field l
inst_6 : Algebra k l
h : Module.finrank k l = n
this_1 : Module.Finite k l
this_2 : Finite l
this : Fintype l
⊢ IsSplittingField k l (HPow.hPow (α := k[X]) X (Nat.card k ^ n) - X)
have rw : IsSplittingField k l (HPow.hPow (α := k[X]) X (Fintype.card l) - X)
Tactic: rw [← h, ← Module.natCard_eq_pow_finrank, ← Fintype.card_eq_nat_card]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (hypothesis)
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
l : Type u_2
inst_5 : Field l
inst_6 : Algebra k l
h : Module.finrank k l = n
this_1 : Module.Finite k l
this_2 : Finite l
this : Fintype l
⊢ Nonempty.{u_2 + 1} (l ≃ₐ[k] Extension k p n)
have this₁ : IsSplittingField k l (HPow.hPow (α := k[X]) X (Nat.card k ^ n) - X)
Tactic: have : IsSplittingField k l (X ^ Nat.card k ^ n - X) := by
    rw [← h, ← Module.natCard_eq_pow_finrank, ← Fintype.card_eq_nat_card]
    exact FiniteField.isSplittingField_sub l k
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
l : Type u_2
inst_5 : Field l
inst_6 : Algebra k l
h : Module.finrank k l = n
this_1 : Module.Finite k l
this_2 : Finite l
this_3 : Fintype l
this : IsSplittingField k l (HPow.hPow (α := k[X]) X (Nat.card k ^ n) - X)
⊢ Nonempty.{u_2 + 1} (l ≃ₐ[k] Extension k p n)
have refine : (HPow.hPow (α := k[X]) X (Nat.card k ^ n) - X).SplittingField ≃ₐ[k] Extension k p n
Tactic: refine ⟨(IsSplittingField.algEquiv _ (X ^ (Nat.card k ^ n) - X)).trans ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (hypothesis)
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
l : Type u_2
inst_4 : Field l
inst_5 : Algebra k l
inst_6 : Finite l
g : Gal(l/k)
n : ℕ := Module.finrank k l
⊢ ∃ (i : ℕ), ∀ (x : l), (g : (a : l) → l) x = x ^ Nat.card k ^ i
have this : NeZero n
Tactic: have : NeZero n := NeZero.of_pos Module.finrank_pos
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
l : Type u_2
inst_4 : Field l
inst_5 : Algebra k l
inst_6 : Finite l
g : Gal(l/k)
n : ℕ := Module.finrank k l
this : NeZero n
⊢ ∃ (i : ℕ), ∀ (x : l), (g : (a : l) → l) x = x ^ Nat.card k ^ i
have obtain : ∀ i < n,
  ∀
    (hi :
      HPow.hPow (α := Gal(Extension k p n/k)) (Extension.frob k p n) i =
        AlgEquiv.trans (AlgEquiv.symm (algEquivExtension k p n l sorry)) (g.trans (algEquivExtension k p n l sorry))),
    ∃ (i : ℕ), ∀ (x : l), (g : (a : l) → l) x = x ^ Nat.card k ^ i
Tactic: obtain ⟨i, _, hi⟩ := Extension.exists_frob_pow_eq k p n <|
    (algEquivExtension k p n l rfl).symm.trans (g.trans (algEquivExtension k p n l rfl))
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
l : Type u_2
inst_4 : Field l
inst_5 : Algebra k l
inst_6 : Finite l
g : Gal(l/k)
n : ℕ := Module.finrank k l
this : NeZero n
i : ℕ
left : i < n
hi :
  HPow.hPow (α := Gal(Extension k p n/k)) (Extension.frob k p n) i =
    AlgEquiv.trans (AlgEquiv.symm (algEquivExtension k p n l ⋯)) (g.trans (algEquivExtension k p n l ⋯))
⊢ ∃ (i : ℕ), ∀ (x : l), (g : (a : l) → l) x = x ^ Nat.card k ^ i
have refine : ∀ (x : l), (g : (a : l) → l) x = x ^ Nat.card k ^ i
Tactic: refine ⟨i, fun x ↦ ?_⟩
-- 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
⊢ f.natDegree ∣ n
have inl : ∀ (h : f ∣ HPow.hPow (α := K[X]) X (HPow.hPow (β := ℕ) (Nat.card K) 0) - X), f.natDegree ∣ 0
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: 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
inl : ∀ (h : f ∣ HPow.hPow (α := K[X]) X (HPow.hPow (β := ℕ) (Nat.card K) 0) - X), f.natDegree ∣ 0
⊢ f.natDegree ∣ n
have inr : ∀ (hn : n ≠ 0), f.natDegree ∣ n
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- 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
⊢ f.natDegree ∣ n
have inr : Finite K → f.natDegree ∣ n
Tactic: cases finite_or_infinite K
-- 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
inr : Finite K → f.natDegree ∣ n
⊢ f.natDegree ∣ n
have inr₁ : Infinite K → f.natDegree ∣ n
Tactic: cases finite_or_infinite K
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (hypothesis)
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 : Infinite K
⊢ f.natDegree ∣ n
have h₁ : f ∣ HSub.hSub (α := K[X]) X 1
Tactic: rw [Nat.card_eq_zero_of_infinite, zero_pow hn, pow_zero, ← dvd_neg, neg_sub] at h
Cleared hypotheses: h, hn, h_1
-- 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 ∣ HSub.hSub (α := K[X]) X 1
hn : n ≠ 0
h_1 : Infinite K
⊢ f.natDegree ∣ n
have inr : 1 ∣ n
Tactic: rw [((Splits.X_sub_C 1).of_dvd (X_sub_C_ne_zero 1) h).natDegree_eq_one_of_irreducible 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
⊢ f.natDegree ∣ n
have inr : ∀ (p : ℕ) (hp : CharP K p), f.natDegree ∣ n
Tactic: let ⟨p, hp⟩ := CharP.exists K
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (hypothesis)
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
⊢ f.natDegree ∣ n
have this : Fact (Nat.Prime p)
Tactic: have : Fact (Nat.Prime p) := ⟨CharP.char_is_prime K p⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (hypothesis)
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 : Fact (Nat.Prime p)
⊢ f.natDegree ∣ n
have this₁ : NeZero n
Tactic: have : NeZero n := ⟨hn⟩
-- 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 ∣ n
have inr : f.natDegree ∣ Module.finrank K (Extension K p n)
Tactic: rw [← finrank_extension K p n]