awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
hF : ExpChar F q
n : ℕ
zero :
  ∀ [CharZero F], natSepDegree.{u} (F := F) ((expand F (HPow.hPow (α := ℕ) 1 n) : (a : F[X]) → F[X]) f) = f.natSepDegree
⊢ natSepDegree.{u} (F := F) ((expand F (q ^ n) : (a : F[X]) → F[X]) f) = f.natSepDegree
have prime : ∀ (hprime : Nat.Prime q) [CharP F q],
  natSepDegree.{u} (F := F) ((expand F (q ^ n) : (a : F[X]) → F[X]) f) = f.natSepDegree
Tactic: obtain - | hprime := hF
Cleared hypotheses: hF
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
inst : Field F
f : F[X]
q n : ℕ
hprime : Nat.Prime q
hchar : CharP F q
⊢ natSepDegree.{u} (F := F) ((expand F (q ^ n) : (a : F[X]) → F[X]) f) = f.natSepDegree
have this : Fact (Nat.Prime q)
Tactic: haveI := Fact.mk hprime
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
q : ℕ
inst_1 : ExpChar F q
n : ℕ
y : F
⊢ (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])).natSepDegree = 1
have rw : (HSub.hSub (α := F[X]) (β := F[X]) ((expand F (q ^ n) : (a : F[X]) → F[X]) X : F[X])
      ((C : (a : F) → F[X]) y : F[X])).natSepDegree =
  1
Tactic: rw [← expand_X, ← expand_C (q ^ n), ← map_sub, natSepDegree_expand, natSepDegree_X_sub_C]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
q : ℕ
inst_1 : ExpChar F q
n : ℕ
y : F
rw :
  (HSub.hSub (α := F[X]) (β := F[X]) ((expand F (q ^ n) : (a : F[X]) → F[X]) X : F[X])
        ((C : (a : F) → F[X]) y : F[X])).natSepDegree =
    1
⊢ (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])).natSepDegree = 1
have rw₁ : (HSub.hSub (α := F[X]) (β := F[X]) ((expand F (q ^ n) : (a : F[X]) → F[X]) X : F[X])
      ((expand F (q ^ n) : (a : F[X]) → F[X]) ((C : (a : F) → F[X]) y) : F[X])).natSepDegree =
  1
Tactic: rw [← expand_X, ← expand_C (q ^ n), ← map_sub, natSepDegree_expand, natSepDegree_X_sub_C]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
q : ℕ
inst_1 : ExpChar F q
n : ℕ
y : F
rw :
  (HSub.hSub (α := F[X]) (β := F[X]) ((expand F (q ^ n) : (a : F[X]) → F[X]) X : F[X])
        ((C : (a : F) → F[X]) y : F[X])).natSepDegree =
    1
rw₁ :
  (HSub.hSub (α := F[X]) (β := F[X]) ((expand F (q ^ n) : (a : F[X]) → F[X]) X : F[X])
        ((expand F (q ^ n) : (a : F[X]) → F[X]) ((C : (a : F) → F[X]) y) : F[X])).natSepDegree =
    1
⊢ (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])).natSepDegree = 1
have rw₂ : natSepDegree.{u} (F := F)
    ((expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]))) =
  1
Tactic: rw [← expand_X, ← expand_C (q ^ n), ← map_sub, natSepDegree_expand, natSepDegree_X_sub_C]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
q : ℕ
inst_1 : ExpChar F q
n : ℕ
y : F
rw :
  (HSub.hSub (α := F[X]) (β := F[X]) ((expand F (q ^ n) : (a : F[X]) → F[X]) X : F[X])
        ((C : (a : F) → F[X]) y : F[X])).natSepDegree =
    1
rw₁ :
  (HSub.hSub (α := F[X]) (β := F[X]) ((expand F (q ^ n) : (a : F[X]) → F[X]) X : F[X])
        ((expand F (q ^ n) : (a : F[X]) → F[X]) ((C : (a : F) → F[X]) y) : F[X])).natSepDegree =
    1
rw₂ :
  natSepDegree.{u} (F := F)
      ((expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]))) =
    1
⊢ (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])).natSepDegree = 1
have rw₃ : (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X])).natSepDegree = 1
Tactic: rw [← expand_X, ← expand_C (q ^ n), ← map_sub, natSepDegree_expand, natSepDegree_X_sub_C]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
q : ℕ
inst_1 : ExpChar F q
n : ℕ
y : F
rw :
  (HSub.hSub (α := F[X]) (β := F[X]) ((expand F (q ^ n) : (a : F[X]) → F[X]) X : F[X])
        ((C : (a : F) → F[X]) y : F[X])).natSepDegree =
    1
rw₁ :
  (HSub.hSub (α := F[X]) (β := F[X]) ((expand F (q ^ n) : (a : F[X]) → F[X]) X : F[X])
        ((expand F (q ^ n) : (a : F[X]) → F[X]) ((C : (a : F) → F[X]) y) : F[X])).natSepDegree =
    1
rw₂ :
  natSepDegree.{u} (F := F)
      ((expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]))) =
    1
rw₃ : (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X])).natSepDegree = 1
⊢ (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])).natSepDegree = 1
have rw₄ : Eq (α := ℕ) 1 1
Tactic: rw [← expand_X, ← expand_C (q ^ n), ← map_sub, natSepDegree_expand, natSepDegree_X_sub_C]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f g : F[X]
q : ℕ
inst_1 : ExpChar F q
h : IsSeparableContraction q f g
⊢ f.natSepDegree = g.natDegree
have obtain : ∀ (h1 : g.Separable) (m : ℕ) (h2 : (expand F (q ^ m) : (a : F[X]) → F[X]) g = f), f.natSepDegree = g.natDegree
Tactic: obtain ⟨h1, m, h2⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f g : F[X]
q : ℕ
inst_1 : ExpChar F q
h1 : g.Separable
m : ℕ
h2 : (expand F (q ^ m) : (a : F[X]) → F[X]) g = f
⊢ f.natSepDegree = g.natDegree
have rw : natSepDegree.{u} (F := F) ((expand F (q ^ m) : (a : F[X]) → F[X]) g) = g.natDegree
Tactic: rw [← h2, natSepDegree_expand, h1.natSepDegree_eq_natDegree]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f g : F[X]
q : ℕ
inst_1 : ExpChar F q
h1 : g.Separable
m : ℕ
h2 : (expand F (q ^ m) : (a : F[X]) → F[X]) g = f
rw : natSepDegree.{u} (F := F) ((expand F (q ^ m) : (a : F[X]) → F[X]) g) = g.natDegree
⊢ f.natSepDegree = g.natDegree
have rw₁ : g.natSepDegree = g.natDegree
Tactic: rw [← h2, natSepDegree_expand, h1.natSepDegree_eq_natDegree]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f g : F[X]
q : ℕ
inst_1 : ExpChar F q
h1 : g.Separable
m : ℕ
h2 : (expand F (q ^ m) : (a : F[X]) → F[X]) g = f
rw : natSepDegree.{u} (F := F) ((expand F (q ^ m) : (a : F[X]) → F[X]) g) = g.natDegree
rw₁ : g.natSepDegree = g.natDegree
⊢ f.natSepDegree = g.natDegree
have rw₂ : g.natDegree = g.natDegree
Tactic: rw [← h2, natSepDegree_expand, h1.natSepDegree_eq_natDegree]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
h : Irreducible f
⊢ f.natSepDegree ∣ f.natDegree
have obtain : ∀ (q : ℕ), ExpChar F q → f.natSepDegree ∣ f.natDegree
Tactic: obtain ⟨q, _⟩ := ExpChar.exists F
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
inst : Field F
f : F[X]
h : Irreducible f
q : ℕ
h_1 : ExpChar F q
⊢ f.natSepDegree ∣ f.natDegree
have hf : HasSeparableContraction q f
Tactic: have hf := h.hasSeparableContraction q
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
h : Irreducible f
q : ℕ
h_1 : ExpChar F q
hf : HasSeparableContraction q f
⊢ f.natSepDegree ∣ f.natDegree
have rw : hf.degree ∣ f.natDegree
Tactic: rw [hf.natSepDegree_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm : f.Monic
hi : Irreducible f
⊢ f.natSepDegree = 1 ↔
    ∃ (n : ℕ) (y : F),
      f = (expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]))
have refine_1 : ∀ (h : f.natSepDegree = 1),
  ∃ (n : ℕ) (y : F),
    f = (expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]))
Tactic: refine ⟨fun h ↦ ?_, fun ⟨n, y, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm : f.Monic
hi : Irreducible f
refine_1 :
  ∀ (h : f.natSepDegree = 1),
    ∃ (n : ℕ) (y : F),
      f = (expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]))
⊢ f.natSepDegree = 1 ↔
    ∃ (n : ℕ) (y : F),
      f = (expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]))
have refine_2 : (∃ (n : ℕ) (y : F),
    f = (expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]))) →
  ∀ (n : ℕ) (y : F)
    (h :
      f = (expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]))),
    f.natSepDegree = 1
Tactic: refine ⟨fun h ↦ ?_, fun ⟨n, y, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm : f.Monic
hi : Irreducible f
h : f.natSepDegree = 1
⊢ ∃ (n : ℕ) (y : F),
    f = (expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]))
have refine_1 : ∀ (g : F[X]) (h1 : g.Separable) (n : ℕ) (hm : Monic.{u} (R := F) ((expand F (q ^ n) : (a : F[X]) → F[X]) g))
  (hi : Irreducible (M := F[X]) ((expand F (q ^ n) : (a : F[X]) → F[X]) g : F[X]))
  (h : natSepDegree.{u} (F := F) ((expand F (q ^ n) : (a : F[X]) → F[X]) g) = 1),
  ∃ (n_1 : ℕ) (y : F),
    Eq (α := F[X]) ((expand F (q ^ n) : (a : F[X]) → F[X]) g : F[X])
      ((expand F (q ^ n_1) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X])) :
        F[X])
Tactic: obtain ⟨g, h1, n, rfl⟩ := hi.hasSeparableContraction q
Cleared hypotheses: f, hm, hi, h
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
q : ℕ
inst_1 : ExpChar F q
g : F[X]
h1 : g.Separable
n : ℕ
hm : Monic.{u} (R := F) ((expand F (q ^ n) : (a : F[X]) → F[X]) g)
hi : Irreducible (M := F[X]) ((expand F (q ^ n) : (a : F[X]) → F[X]) g : F[X])
h : natSepDegree.{u} (F := F) ((expand F (q ^ n) : (a : F[X]) → F[X]) g) = 1
⊢ g.natDegree = 1
have rwa : ∀ (h : g.natSepDegree = 1), g.natDegree = 1
Tactic: rwa [natSepDegree_expand _ q, h1.natSepDegree_eq_natDegree] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
q : ℕ
inst_1 : ExpChar F q
g : F[X]
h1 : g.Separable
n : ℕ
hm : Monic.{u} (R := F) ((expand F (q ^ n) : (a : F[X]) → F[X]) g)
hi : Irreducible (M := F[X]) ((expand F (q ^ n) : (a : F[X]) → F[X]) g : F[X])
h : natSepDegree.{u} (F := F) ((expand F (q ^ n) : (a : F[X]) → F[X]) g) = 1
rwa : ∀ (h : g.natSepDegree = 1), g.natDegree = 1
⊢ g.natDegree = 1
have rwa₁ : ∀ (h : g.natDegree = 1), g.natDegree = 1
Tactic: rwa [natSepDegree_expand _ q, h1.natSepDegree_eq_natDegree] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
inst : Field F
q : ℕ
inst_1 : ExpChar F q
g : F[X]
h1 : g.Separable
n : ℕ
hm : Monic.{u} (R := F) ((expand F (q ^ n) : (a : F[X]) → F[X]) g)
hi : Irreducible (M := F[X]) ((expand F (q ^ n) : (a : F[X]) → F[X]) g : F[X])
h : natSepDegree.{u} (F := F) ((expand F (q ^ n) : (a : F[X]) → F[X]) g) = 1
⊢ ∃ (n_1 : ℕ) (y : F),
    Eq (α := F[X]) ((expand F (q ^ n) : (a : F[X]) → F[X]) g : F[X])
      ((expand F (q ^ n_1) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X])) :
        F[X])
have h2 : g.natDegree = 1
Tactic: have h2 : g.natDegree = 1 := by
      rwa [natSepDegree_expand _ q, h1.natSepDegree_eq_natDegree] at h
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
q : ℕ
inst_1 : ExpChar F q
g : F[X]
h1 : g.Separable
n : ℕ
hm : Monic.{u} (R := F) ((expand F (q ^ n) : (a : F[X]) → F[X]) g)
hi : Irreducible (M := F[X]) ((expand F (q ^ n) : (a : F[X]) → F[X]) g : F[X])
h : natSepDegree.{u} (F := F) ((expand F (q ^ n) : (a : F[X]) → F[X]) g) = 1
h2 : g.natDegree = 1
⊢ ∃ (n_1 : ℕ) (y : F),
    Eq (α := F[X]) ((expand F (q ^ n) : (a : F[X]) → F[X]) g : F[X])
      ((expand F (q ^ n_1) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X])) :
        F[X])
have refine_1 : ∃ (n_1 : ℕ) (y : F),
  Eq (α := F[X])
    ((expand F (q ^ n) : (a : F[X]) → F[X])
        (HAdd.hAdd (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (g.coeff 0) : F[X])) :
      F[X])
    ((expand F (q ^ n_1) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X])) :
      F[X])
Tactic: rw [((monic_expand_iff <| expChar_pow_pos F q n).mp hm).eq_X_add_C h2]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
q : ℕ
inst_1 : ExpChar F q
g : F[X]
h1 : g.Separable
n : ℕ
hm : Monic.{u} (R := F) ((expand F (q ^ n) : (a : F[X]) → F[X]) g)
hi : Irreducible (M := F[X]) ((expand F (q ^ n) : (a : F[X]) → F[X]) g : F[X])
h : natSepDegree.{u} (F := F) ((expand F (q ^ n) : (a : F[X]) → F[X]) g) = 1
h2 : g.natDegree = 1
⊢ Eq (α := F[X])
    ((expand F (q ^ n) : (a : F[X]) → F[X])
        (HAdd.hAdd (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (g.coeff 0) : F[X])) :
      F[X])
    ((expand F (q ^ n) : (a : F[X]) → F[X])
        (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (-g.coeff 0) : F[X])) :
      F[X])
have rw : Eq (α := F[X])
  ((expand F (q ^ n) : (a : F[X]) → F[X])
      (HAdd.hAdd (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (g.coeff 0) : F[X])) :
    F[X])
  ((expand F (q ^ n) : (a : F[X]) → F[X])
      (HSub.hSub (α := F[X]) (β := F[X]) X (-(C : (a : F) → F[X]) (g.coeff 0) : F[X])) :
    F[X])
Tactic: rw [map_neg, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
q : ℕ
inst_1 : ExpChar F q
g : F[X]
h1 : g.Separable
n : ℕ
hm : Monic.{u} (R := F) ((expand F (q ^ n) : (a : F[X]) → F[X]) g)
hi : Irreducible (M := F[X]) ((expand F (q ^ n) : (a : F[X]) → F[X]) g : F[X])
h : natSepDegree.{u} (F := F) ((expand F (q ^ n) : (a : F[X]) → F[X]) g) = 1
h2 : g.natDegree = 1
rw :
  Eq (α := F[X])
    ((expand F (q ^ n) : (a : F[X]) → F[X])
        (HAdd.hAdd (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (g.coeff 0) : F[X])) :
      F[X])
    ((expand F (q ^ n) : (a : F[X]) → F[X])
        (HSub.hSub (α := F[X]) (β := F[X]) X (-(C : (a : F) → F[X]) (g.coeff 0) : F[X])) :
      F[X])
⊢ Eq (α := F[X])
    ((expand F (q ^ n) : (a : F[X]) → F[X])
        (HAdd.hAdd (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (g.coeff 0) : F[X])) :
      F[X])
    ((expand F (q ^ n) : (a : F[X]) → F[X])
        (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (-g.coeff 0) : F[X])) :
      F[X])
have rw₁ : Eq (α := F[X])
  ((expand F (q ^ n) : (a : F[X]) → F[X])
      (HAdd.hAdd (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (g.coeff 0) : F[X])) :
    F[X])
  ((expand F (q ^ n) : (a : F[X]) → F[X])
      (HAdd.hAdd (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (g.coeff 0) : F[X])) :
    F[X])
Tactic: rw [map_neg, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm : f.Monic
hi : Irreducible f
h_1 :
  ∃ (n : ℕ) (y : F),
    f = (expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]))
n : ℕ
y : F
h : f = (expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]))
⊢ f.natSepDegree = 1
have refine_2 : natSepDegree.{u} (F := F)
    ((expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]))) =
  1
Tactic: rw [h, natSepDegree_expand _ q, natSepDegree_X_sub_C]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm : f.Monic
hi : Irreducible f
h_1 :
  ∃ (n : ℕ) (y : F),
    f = (expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]))
n : ℕ
y : F
h : f = (expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]))
refine_2 :
  natSepDegree.{u} (F := F)
      ((expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]))) =
    1
⊢ f.natSepDegree = 1
have refine_2₁ : (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X])).natSepDegree = 1
Tactic: rw [h, natSepDegree_expand _ q, natSepDegree_X_sub_C]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm : f.Monic
hi : Irreducible f
h_1 :
  ∃ (n : ℕ) (y : F),
    f = (expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]))
n : ℕ
y : F
h : f = (expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]))
refine_2 :
  natSepDegree.{u} (F := F)
      ((expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]))) =
    1
refine_2₁ : (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X])).natSepDegree = 1
⊢ f.natSepDegree = 1
have refine_2₂ : Eq (α := ℕ) 1 1
Tactic: rw [h, natSepDegree_expand _ q, natSepDegree_X_sub_C]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm : f.Monic
hi : Irreducible f
⊢ f.natSepDegree = 1 ↔
    ∃ (n : ℕ) (y : F), f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
have simp_rw : (∃ (n : ℕ) (y : F),
    f = (expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]))) ↔
  ∃ (n : ℕ) (y : F), f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
Tactic: simp_rw [hi.natSepDegree_eq_one_iff_of_monic' q hm, map_sub, expand_X, expand_C]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm : f.Monic
hi : Irreducible f
simp_rw :
  (∃ (n : ℕ) (y : F),
      f =
        (expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]))) ↔
    ∃ (n : ℕ) (y : F), f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
⊢ f.natSepDegree = 1 ↔
    ∃ (n : ℕ) (y : F), f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
have simp_rw₁ : (∃ (n : ℕ) (y : F),
    f =
      HSub.hSub (α := F[X]) (β := F[X]) ((expand F (q ^ n) : (a : F[X]) → F[X]) X : F[X])
        ((expand F (q ^ n) : (a : F[X]) → F[X]) ((C : (a : F) → F[X]) y) : F[X])) ↔
  ∃ (n : ℕ) (y : F), f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
Tactic: simp_rw [hi.natSepDegree_eq_one_iff_of_monic' q hm, map_sub, expand_X, expand_C]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm : f.Monic
hi : Irreducible f
simp_rw :
  (∃ (n : ℕ) (y : F),
      f =
        (expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]))) ↔
    ∃ (n : ℕ) (y : F), f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
simp_rw₁ :
  (∃ (n : ℕ) (y : F),
      f =
        HSub.hSub (α := F[X]) (β := F[X]) ((expand F (q ^ n) : (a : F[X]) → F[X]) X : F[X])
          ((expand F (q ^ n) : (a : F[X]) → F[X]) ((C : (a : F) → F[X]) y) : F[X])) ↔
    ∃ (n : ℕ) (y : F), f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
⊢ f.natSepDegree = 1 ↔
    ∃ (n : ℕ) (y : F), f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
have simp_rw₂ : (∃ (n : ℕ) (y : F),
    f =
      HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n))
        ((expand F (q ^ n) : (a : F[X]) → F[X]) ((C : (a : F) → F[X]) y) : F[X])) ↔
  ∃ (n : ℕ) (y : F), f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
Tactic: simp_rw [hi.natSepDegree_eq_one_iff_of_monic' q hm, map_sub, expand_X, expand_C]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
inst : Field F
f : F[X]
hm : f.Monic
hs : f.Splits
h : f.natSepDegree = 1
⊢ ∃ (m : ℕ) (y : F), m ≠ 0 ∧ f = HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]) ^ m
have h1 : f =
  Multiset.prod
    (Multiset.map (fun (x : F) ↦ HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X])) f.roots)
Tactic: have h1 := hs.eq_prod_roots_of_monic hm
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
inst : Field F
f : F[X]
hm : f.Monic
hs : f.Splits
h : f.natSepDegree = 1
h1 :
  f =
    Multiset.prod
      (Multiset.map (fun (x : F) ↦ HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X])) f.roots)
⊢ ∃ (m : ℕ) (y : F), m ≠ 0 ∧ f = HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]) ^ m
have h2 : (f.aroots F).toFinset.card = f.natSepDegree
Tactic: have h2 := (natSepDegree_eq_of_splits f (hs.map <| .id F)).symm
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
inst : Field F
f : F[X]
hm : f.Monic
hs : f.Splits
h : f.natSepDegree = 1
h1 :
  f =
    Multiset.prod
      (Multiset.map (fun (x : F) ↦ HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X])) f.roots)
h2 : (f.aroots F).toFinset.card = f.natSepDegree
⊢ ∃ (m : ℕ) (y : F), m ≠ 0 ∧ f = HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]) ^ m
have h2₁ : f.roots.card ≠ 0 ∧ ∃ (a : F), f.roots = HSMul.hSMul (β := Multiset F) f.roots.card {a}
Tactic: rw [h, aroots_def, Algebra.algebraMap_self, map_id, Multiset.toFinset_card_eq_one_iff] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
hm : f.Monic
hs : f.Splits
h : f.natSepDegree = 1
h1 :
  f =
    Multiset.prod
      (Multiset.map (fun (x : F) ↦ HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X])) f.roots)
h2 : f.roots.card ≠ 0 ∧ ∃ (a : F), f.roots = HSMul.hSMul (β := Multiset F) f.roots.card {a}
⊢ ∃ (m : ℕ) (y : F), m ≠ 0 ∧ f = HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]) ^ m
have obtain : ∀ (h2 : f.roots.card ≠ 0) (y : F) (h3 : f.roots = HSMul.hSMul (β := Multiset F) f.roots.card {y}),
  ∃ (m : ℕ) (y : F), m ≠ 0 ∧ f = HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]) ^ m
Tactic: obtain ⟨h2, y, h3⟩ := h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
hm : f.Monic
hs : f.Splits
h : f.natSepDegree = 1
h1 :
  f =
    Multiset.prod
      (Multiset.map (fun (x : F) ↦ HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X])) f.roots)
h2 : f.roots.card ≠ 0
y : F
h3 : f.roots = HSMul.hSMul (β := Multiset F) f.roots.card {y}
⊢ f = HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]) ^ f.roots.card
have rwa : ∀
  (h1 :
    f =
      Multiset.prod
        (Multiset.map (fun (x : F) ↦ HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X]))
          (HSMul.hSMul (β := Multiset F) f.roots.card {y})))
  (h3 : f.roots = HSMul.hSMul (β := Multiset F) f.roots.card {y}),
  f = HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]) ^ f.roots.card
Tactic: rwa [h3, Multiset.map_nsmul, Multiset.map_singleton, Multiset.prod_nsmul,
    Multiset.prod_singleton] at h1
Cleared hypotheses: h1, h3