awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Finite.Extension
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 = Fintype.card (Extension k p n)
⊢ IsSplittingField k (Extension k p n) (HPow.hPow (α := k[X]) X (Nat.card k ^ n) - X)

Tactic:
convert! FiniteField.isSplittingField_sub (Extension k p n) k

Premises used: FiniteField.isSplittingField_sub, FiniteField.Extension
-- Module: Mathlib.FieldTheory.Finite.Extension
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)
h₁ h₂ : Nat.card k ^ n = Nat.card k ^ n
⊢ Nat.card k ^ n = Fintype.card (Extension k p n)

Tactic:
rw [Fintype.card_eq_nat_card, natCard_extension]

Premises used: FiniteField.natCard_extension, Fintype.card_eq_nat_card
-- Module: Mathlib.FieldTheory.Finite.Extension
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
⊢ IsGalois k (Extension k p n)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.FieldTheory.Finite.Extension
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
⊢ IsCyclic Gal(Extension k p n/k)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.FieldTheory.Finite.Extension
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
⊢ Nat.card Gal(Extension k p n/k) = n

Tactic:
(IsGalois.card_aut_eq_finrank _ _).trans <| finrank_extension k p n

Premises used: IsGalois.card_aut_eq_finrank, Eq.trans, FiniteField.finrank_extension
-- Module: Mathlib.FieldTheory.Finite.Extension
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
⊢ Fintype.card Gal(Extension k p n/k) = n

Tactic:
Fintype.card_eq_nat_card.trans <| natCard_algEquiv_extension k p n

Premises used: FiniteField.natCard_algEquiv_extension, Fintype.card_eq_nat_card, Eq.trans
-- Module: Mathlib.FieldTheory.Finite.Extension
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
x : Extension k p n
⊢ (frob k p n : (a : Extension k p n) → Extension k p n) x = x ^ Nat.card k

Tactic:
simp [frob, ← Nat.card_eq_fintype_card]

Premises used: FiniteField.Extension.frob, Nat.card_eq_fintype_card
-- Module: Mathlib.FieldTheory.Finite.Extension
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
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:
simp
-- Module: Mathlib.FieldTheory.Finite.Extension
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)
succ₆ succ₇ : x ^ Nat.card k ^ (i + 1) = 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)

Tactic:
rw [pow_add, pow_one, AlgEquiv.mul_apply, ih, frob_apply, ← pow_mul, ← Nat.pow_add_one']

Premises used: FiniteField.Extension.frob_apply, pow_add, pow_mul, pow_one, AlgEquiv.mul_apply, Nat.pow_add_one'
-- Module: Mathlib.FieldTheory.Finite.Extension
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
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)
⊢ (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

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']

Premises used: FiniteField.Extension.frob_apply, pow_add, pow_mul, pow_one, AlgEquiv.mul_apply, Nat.pow_add_one'
-- Module: Mathlib.FieldTheory.Finite.Extension
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
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⟩
⊢ ∃ i < n, HPow.hPow (α := Gal(Extension k p n/k)) (frob k p n) i = g

Tactic:
obtain ⟨⟨i, hi⟩, rfl⟩ := (FiniteField.bijective_frobeniusAlgEquivOfAlgebraic_pow k
    (Extension k p n)).2 g

Premises used: And.right, FiniteField.bijective_frobeniusAlgEquivOfAlgebraic_pow, FiniteField.Extension, rfl
-- Module: Mathlib.FieldTheory.Finite.Extension
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)
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)
⊢ 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⟩

Tactic:
ext
-- Module: Mathlib.FieldTheory.Finite.Extension
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)
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:
simp [frob]

Premises used: FiniteField.Extension.frob
-- Module: Mathlib.FieldTheory.Finite.Extension
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)
refine : i < 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:
refine ⟨i, ?_, by ext; simp [frob]⟩
-- Module: Mathlib.FieldTheory.Finite.Extension
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)
rwa rwa₁ rwa₂ rwa₃ : ∀ (hi : i < n), i < n
⊢ i < n

Tactic:
rwa [finrank_extension] at hi

Premises used: FiniteField.finrank_extension
-- Module: Mathlib.FieldTheory.Finite.Extension
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
refine : Nonempty.{u_2 + 1} (l ≃ₐ[k] Extension k p n)
⊢ l ≃ₐ[k] Extension k p n

Tactic:
refine Nonempty.some ?_

Premises used: Nonempty.some
-- Module: Mathlib.FieldTheory.Finite.Extension
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
⊢ Module.Finite k l

Tactic:
have : Module.Finite k l := Module.finite_of_finrank_pos <| h ▸ NeZero.pos n
-- Module: Mathlib.FieldTheory.Finite.Extension
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
⊢ Finite l

Tactic:
have : Finite l := Module.finite_of_finite k
-- Module: Mathlib.FieldTheory.Finite.Extension
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
have : ∀ (this : Fintype l), Nonempty.{u_2 + 1} (l ≃ₐ[k] Extension k p n)
⊢ Nonempty.{u_2 + 1} (l ≃ₐ[k] Extension k p n)

Tactic:
have : Fintype l := .ofFinite _
-- Module: Mathlib.FieldTheory.Finite.Extension
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
rw : IsSplittingField k l (HPow.hPow (α := k[X]) X (Fintype.card l) - X)
rw₁ : Fintype l
⊢ IsSplittingField k l (HPow.hPow (α := k[X]) X (Nat.card k ^ n) - X)

Tactic:
rw [← h, ← Module.natCard_eq_pow_finrank, ← Fintype.card_eq_nat_card]

Premises used: Module.natCard_eq_pow_finrank, Fintype.card_eq_nat_card
-- Module: Mathlib.FieldTheory.Finite.Extension
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 (Fintype.card l) - X)

Tactic:
FiniteField.isSplittingField_sub l k

Premises used: FiniteField.isSplittingField_sub
-- Module: Mathlib.FieldTheory.Finite.Extension
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)

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
-- Module: Mathlib.FieldTheory.Finite.Extension
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)

Tactic:
⟨(IsSplittingField.algEquiv _ (X ^ (Nat.card k ^ n) - X)).trans ?_⟩

Premises used: HSub.hSub, Nat.card, Nonempty.intro, Polynomial.IsSplittingField.algEquiv, AlgEquiv.trans, HPow.hPow, Polynomial.X
-- Module: Mathlib.FieldTheory.Finite.Extension
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)
refine : (HPow.hPow (α := k[X]) X (Nat.card k ^ n) - X).SplittingField ≃ₐ[k] Extension k p n
⊢ Nonempty.{u_2 + 1} (l ≃ₐ[k] Extension k p n)

Tactic:
refine ⟨(IsSplittingField.algEquiv _ (X ^ (Nat.card k ^ n) - X)).trans ?_⟩
-- Module: Mathlib.FieldTheory.Finite.Extension
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)
⊢ (HPow.hPow (α := k[X]) X (Nat.card k ^ n) - X).SplittingField ≃ₐ[k] Extension k p n

Tactic:
exact (IsSplittingField.algEquiv _ (X ^ (Nat.card k ^ n) - X)).symm

Premises used: AlgEquiv.symm, HSub.hSub, Nat.card, Polynomial.IsSplittingField.algEquiv, HPow.hPow, Polynomial.X
-- Module: Mathlib.FieldTheory.Finite.Extension
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
⊢ NeZero n

Tactic:
have : NeZero n := NeZero.of_pos Module.finrank_pos
-- Module: Mathlib.FieldTheory.Finite.Extension
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
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 ⋯)) (g.trans (algEquivExtension k p n l ⋯))),
      ∃ (i : ℕ), ∀ (x : l), (g : (a : l) → l) x = x ^ Nat.card k ^ i
⊢ ∃ (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))

Premises used: FiniteField.algEquivExtension, AlgEquiv.symm, AlgEquiv.trans, FiniteField.Extension.exists_frob_pow_eq, rfl
-- Module: Mathlib.FieldTheory.Finite.Extension
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

Tactic:
⟨i, fun x ↦ ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.FieldTheory.Finite.Extension
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 ⋯))
refine : ∀ (x : l), (g : (a : l) → l) x = x ^ Nat.card k ^ i
⊢ ∃ (i : ℕ), ∀ (x : l), (g : (a : l) → l) x = x ^ Nat.card k ^ i

Tactic:
refine ⟨i, fun x ↦ ?_⟩
-- Module: Mathlib.FieldTheory.Finite.Extension
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 ⋯))
x : l
⊢ (g : (a : l) → l) x = x ^ Nat.card k ^ i

Tactic:
simpa using (AlgEquiv.congr_arg (f := (algEquivExtension k p n l rfl).symm) <|
    AlgEquiv.congr_fun hi (algEquivExtension k p n l rfl x)).symm

Premises used: FiniteField.algEquivExtension, Eq.symm, DFunLike.coe, rfl, AlgEquiv.congr_fun, AlgEquiv.congr_arg
-- 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
inl : ∀ (h : f ∣ HPow.hPow (α := K[X]) X (HPow.hPow (β := ℕ) (Nat.card K) 0) - X), f.natDegree ∣ 0
inr : ∀ (hn : n ≠ 0), f.natDegree ∣ n
⊢ f.natDegree ∣ n

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.FieldTheory.Finite.Extension
Goal:
K : Type u_2
inst : Field K
f : K[X]
hi : Irreducible f
h : f ∣ HPow.hPow (α := K[X]) X (HPow.hPow (β := ℕ) (Nat.card K) 0) - X
⊢ f.natDegree ∣ 0

Tactic:
simp
-- 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
inr : Finite K → f.natDegree ∣ n
inr₁ : Infinite K → f.natDegree ∣ n
⊢ f.natDegree ∣ n

Tactic:
cases finite_or_infinite K

Premises used: finite_or_infinite
-- 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 : Infinite K
⊢ 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

Premises used: neg_sub, Nat.card_eq_zero_of_infinite, pow_zero, dvd_neg, zero_pow
-- 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 : Infinite K
h₁ : f ∣ HSub.hSub (α := K[X]) X 1
⊢ n ≠ 0

Tactic:
rw [Nat.card_eq_zero_of_infinite, zero_pow hn, pow_zero, ← dvd_neg, neg_sub] at h

Premises used: neg_sub, Nat.card_eq_zero_of_infinite, pow_zero, dvd_neg, zero_pow
-- 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 : Infinite K
h₁ : f ∣ HSub.hSub (α := K[X]) X 1
hn₁ : n ≠ 0
⊢ Infinite K

Tactic:
rw [Nat.card_eq_zero_of_infinite, zero_pow hn, pow_zero, ← dvd_neg, neg_sub] at h

Premises used: neg_sub, Nat.card_eq_zero_of_infinite, pow_zero, dvd_neg, zero_pow
-- Module: Mathlib.FieldTheory.Finite.Extension
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
inr : 1 ∣ n
⊢ f.natDegree ∣ n

Tactic:
rw [((Splits.X_sub_C 1).of_dvd (X_sub_C_ne_zero 1) h).natDegree_eq_one_of_irreducible hi]

Premises used: Polynomial.Splits.natDegree_eq_one_of_irreducible, Polynomial.Splits.X_sub_C, Polynomial.Splits.of_dvd, Polynomial.X_sub_C_ne_zero, OfNat.ofNat
-- Module: Mathlib.FieldTheory.Finite.Extension
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
⊢ 1 ∣ n

Tactic:
one_dvd n

Premises used: one_dvd
-- Module: Mathlib.FieldTheory.Finite.Extension
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
⊢ 1 ∣ n

Tactic:
exact one_dvd n

Premises used: one_dvd
-- 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
inr : ∀ (p : ℕ) (hp : CharP K p), f.natDegree ∣ n
⊢ f.natDegree ∣ n

Tactic:
let ⟨p, hp⟩ := CharP.exists K
-- 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
⊢ Fact (Nat.Prime p)

Tactic:
have : Fact (Nat.Prime p) := ⟨CharP.char_is_prime K p⟩
-- 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 : Fact (Nat.Prime p)
⊢ NeZero n

Tactic:
have : NeZero n := ⟨hn⟩
-- 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
inr : f.natDegree ∣ Module.finrank K (Extension K p n)
⊢ f.natDegree ∣ n

Tactic:
rw [← finrank_extension K p n]

Premises used: FiniteField.finrank_extension
-- 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
inr : Splits (R := Extension K p n) (Polynomial.map (algebraMap K (Extension K p n)) f)
⊢ f.natDegree ∣ Module.finrank K (Extension K p n)

Tactic:
apply Irreducible.natDegree_dvd_finrank hi

Premises used: Polynomial.Irreducible.natDegree_dvd_finrank
-- 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)) f)

Tactic:
Splits.of_dvd ?_ ?_ (map_dvd (algebraMap K (Extension K p n)) h)

Premises used: Algebra.algebraMap, Polynomial.map_dvd, Polynomial.Splits.of_dvd, FiniteField.Extension
-- 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
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))
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
⊢ Splits (R := Extension K p n) (Polynomial.map (algebraMap K (Extension K p n)) f)

Tactic:
refine Splits.of_dvd ?_ ?_ (map_dvd (algebraMap K (Extension K p n)) h)

Premises used: Algebra.algebraMap, Polynomial.map_dvd, Polynomial.Splits.of_dvd, FiniteField.Extension