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]
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}
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
⊢ f = HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]) ^ f.roots.card
have rwa₁ : ∀
  (h1 :
    f =
      (HSMul.hSMul (β := Multiset F[X]) f.roots.card
          (Multiset.map (fun (x : F) ↦ HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X])) {y})).prod)
  (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
-- 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}
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
rwa₁ :
  ∀
    (h1 :
      f =
        (HSMul.hSMul (β := Multiset F[X]) f.roots.card
            (Multiset.map (fun (x : F) ↦ HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X]))
              {y})).prod)
    (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
⊢ f = HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]) ^ f.roots.card
have rwa₂ : ∀
  (h1 :
    f =
      (HSMul.hSMul (β := Multiset F[X]) f.roots.card
          {HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X])}).prod)
  (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
-- 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}
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
rwa₁ :
  ∀
    (h1 :
      f =
        (HSMul.hSMul (β := Multiset F[X]) f.roots.card
            (Multiset.map (fun (x : F) ↦ HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X]))
              {y})).prod)
    (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
rwa₂ :
  ∀
    (h1 :
      f =
        (HSMul.hSMul (β := Multiset F[X]) f.roots.card
            {HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X])}).prod)
    (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
⊢ f = HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]) ^ f.roots.card
have rwa₃ : ∀
  (h1 :
    f =
      HPow.hPow (α := F[X]) (Multiset.prod {HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X])})
        f.roots.card)
  (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
-- 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}
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
rwa₁ :
  ∀
    (h1 :
      f =
        (HSMul.hSMul (β := Multiset F[X]) f.roots.card
            (Multiset.map (fun (x : F) ↦ HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X]))
              {y})).prod)
    (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
rwa₂ :
  ∀
    (h1 :
      f =
        (HSMul.hSMul (β := Multiset F[X]) f.roots.card
            {HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X])}).prod)
    (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
rwa₃ :
  ∀
    (h1 :
      f =
        HPow.hPow (α := F[X]) (Multiset.prod {HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X])})
          f.roots.card)
    (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
⊢ f = HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]) ^ f.roots.card
have rwa₄ : ∀ (h1 : f = HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]) ^ f.roots.card)
  (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
-- 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
⊢ ∃ (m : ℕ) (y : F), m ≠ 0 ∧ f = HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]) ^ m
have 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)),
  ∃ (m : ℕ) (y : F), m ≠ 0 ∧ f = HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]) ^ m
Tactic: classical
  have h1 := hs.eq_prod_roots_of_monic hm
  have h2 := (natSepDegree_eq_of_splits f (hs.map <| .id F)).symm
  rw [h, aroots_def, Algebra.algebraMap_self, map_id, Multiset.toFinset_card_eq_one_iff] at h2
  obtain ⟨h2, y, h3⟩ := h2
  exact ⟨_, y, h2, by rwa [h3, Multiset.map_nsmul, Multiset.map_singleton, Multiset.prod_nsmul,
    Multiset.prod_singleton] at h1⟩
-- 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
have have₁ 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)),
    ∃ (m : ℕ) (y : F), m ≠ 0 ∧ f = HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]) ^ m
⊢ ∃ (m : ℕ) (y : F), m ≠ 0 ∧ f = HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]) ^ m
have 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))
  (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
Tactic: classical
  have h1 := hs.eq_prod_roots_of_monic hm
  have h2 := (natSepDegree_eq_of_splits f (hs.map <| .id F)).symm
  rw [h, aroots_def, Algebra.algebraMap_self, map_id, Multiset.toFinset_card_eq_one_iff] at h2
  obtain ⟨h2, y, h3⟩ := h2
  exact ⟨_, y, h2, by rwa [h3, Multiset.map_nsmul, Multiset.map_singleton, Multiset.prod_nsmul,
    Multiset.prod_singleton] at h1⟩
-- 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
have have₁ 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)),
    ∃ (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))
    (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
⊢ ∃ (m : ℕ) (y : F), m ≠ 0 ∧ f = HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]) ^ m
have 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))
  (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
Tactic: classical
  have h1 := hs.eq_prod_roots_of_monic hm
  have h2 := (natSepDegree_eq_of_splits f (hs.map <| .id F)).symm
  rw [h, aroots_def, Algebra.algebraMap_self, map_id, Multiset.toFinset_card_eq_one_iff] at h2
  obtain ⟨h2, y, h3⟩ := h2
  exact ⟨_, y, h2, by rwa [h3, Multiset.map_nsmul, Multiset.map_singleton, Multiset.prod_nsmul,
    Multiset.prod_singleton] at h1⟩
-- 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
have have₁ 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)),
    ∃ (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))
    (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₄ :
  ∀
    (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
⊢ ∃ (m : ℕ) (y : F), m ≠ 0 ∧ f = HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]) ^ m
have 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))
  (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: classical
  have h1 := hs.eq_prod_roots_of_monic hm
  have h2 := (natSepDegree_eq_of_splits f (hs.map <| .id F)).symm
  rw [h, aroots_def, Algebra.algebraMap_self, map_id, Multiset.toFinset_card_eq_one_iff] at h2
  obtain ⟨h2, y, h3⟩ := h2
  exact ⟨_, y, h2, by rwa [h3, Multiset.map_nsmul, Multiset.map_singleton, Multiset.prod_nsmul,
    Multiset.prod_singleton] at h1⟩
-- 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),
    (n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F q)) ∧
      f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
have obtain : ∀ (n : ℕ) (y : F) (hf : f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])),
  ∃ (n : ℕ) (y : F),
    (n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F q)) ∧
      f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
Tactic: obtain ⟨n, y, hf⟩ := (hm.natSepDegree_eq_one_iff_of_irreducible q hi).1 h
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
hm : f.Monic
hi : Irreducible f
h : f.natSepDegree = 1
n : ℕ
y : F
inst_1 : CharZero F
inst_2 : ExpChar F 1
hf : f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (HPow.hPow (α := ℕ) 1 n)) ((C : (a : F) → F[X]) y : F[X])
⊢ ∃ (n : ℕ) (y : F),
    (n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F 1)) ∧
      f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (HPow.hPow (α := ℕ) 1 n)) ((C : (a : F) → F[X]) y : F[X])
have zero : ∀ (hf : f = HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X])),
  ∃ (n : ℕ) (y : F),
    (n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F 1)) ∧
      f = HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X])
Tactic: simp_rw [one_pow, pow_one] at hf ⊢
Cleared hypotheses: hf
-- 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
hf : f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
hq : Nat.Prime q
hchar : CharP F q
⊢ ∃ (n : ℕ) (y : F),
    (n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F q)) ∧
      f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
have prime : ∀ (hn : ¬n = 0),
  Membership.mem (γ := Subring F) (RingHom.range (R := F) (frobenius F q)) y →
    ∀ (z : F) (hy : ((frobenius F q : F →+* F) : (a : F) → F) z = y), False
Tactic: refine ⟨n, y, (em _).imp id fun hn ⟨z, hy⟩ ↦ ?_, hf⟩
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
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
hf : f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
hq : Nat.Prime q
hchar : CharP F q
hn : ¬n = 0
h_1 : Membership.mem (γ := Subring F) (RingHom.range (R := F) (frobenius F q)) y
z : F
hy : ((frobenius F q : F →+* F) : (a : F) → F) z = y
⊢ False
have this : ExpChar.{u} F[X] q
Tactic: haveI := expChar_of_injective_ringHom (R := F) C_injective q
-- 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
hf : f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
hq : Nat.Prime q
hchar : CharP F q
hn : ¬n = 0
h_1 : Membership.mem (γ := Subring F) (RingHom.range (R := F) (frobenius F q)) y
z : F
hy : ((frobenius F q : F →+* F) : (a : F) → F) z = y
this : ExpChar.{u} F[X] q
⊢ False
have prime : ∀ (hf : f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])) (hq : Nat.Prime q)
  [CharP F q] (hn : ¬n = 0),
  Membership.mem (γ := Subring F) (RingHom.range (R := F) (frobenius F q)) y →
    ∀ (z : F)
      (hi :
        Irreducible (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n.pred)) ((C : (a : F) → F[X]) z : F[X]) ^ q))
      (hy : ((frobenius F q : F →+* F) : (a : F) → F) z = y) (this : ExpChar.{u} F[X] q), False
Tactic: rw [hf, ← Nat.succ_pred hn, pow_succ, pow_mul, ← hy, frobenius_def, map_pow,
      ← sub_pow_expChar] at hi
Cleared hypotheses: hi, hf, hq, hchar, hn, h_1, z, hy, this
-- 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
h : f.natSepDegree = 1
⊢ ∃ (m : ℕ) (n : ℕ) (y : F),
    m ≠ 0 ∧
      (n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F q)) ∧
        f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ m
have obtain : ∀ (p : F[X]) (hM : p.Monic) (hI : Irreducible p) (hf : p ∣ f),
  ∃ (m : ℕ) (n : ℕ) (y : F),
    m ≠ 0 ∧
      (n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F q)) ∧
        f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ m
Tactic: obtain ⟨p, hM, hI, hf⟩ := exists_monic_irreducible_factor _ <| not_isUnit_of_natDegree_pos _
    <| Nat.pos_of_ne_zero <| (natSepDegree_ne_zero_iff _).1 (h.symm ▸ Nat.one_ne_zero)
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf : p ∣ f
⊢ ∃ (m : ℕ) (n : ℕ) (y : F),
    m ≠ 0 ∧
      (n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F q)) ∧
        f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ m
have hD : p.natSepDegree = 1
Tactic: have hD := (h ▸ natSepDegree_le_of_dvd p f hf hm.ne_zero).antisymm <|
    Nat.pos_of_ne_zero <| (natSepDegree_ne_zero_iff _).2 hI.natDegree_pos.ne'
-- 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
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf : p ∣ f
hD : p.natSepDegree = 1
⊢ ∃ (m : ℕ) (n : ℕ) (y : F),
    m ≠ 0 ∧
      (n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F q)) ∧
        f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ m
have obtain : ∀ (n : ℕ) (y : F) (H : n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F q))
  (hp : p = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])),
  ∃ (m : ℕ) (n : ℕ) (y : F),
    m ≠ 0 ∧
      (n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F q)) ∧
        f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ m
Tactic: obtain ⟨n, y, H, hp⟩ := hM.eq_X_pow_char_pow_sub_C_of_natSepDegree_eq_one_of_irreducible q hI hD
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H : n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F q)
hp : p = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
⊢ ∃ (m : ℕ) (n : ℕ) (y : F),
    m ≠ 0 ∧
      (n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F q)) ∧
        f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ m
have hF : FiniteMultiplicity p f
Tactic: have hF := finiteMultiplicity_of_degree_pos_of_monic (degree_pos_of_irreducible hI) hM hm.ne_zero
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H : n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F q)
hp : p = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
hF : FiniteMultiplicity p f
⊢ ∃ (m : ℕ) (n : ℕ) (y : F),
    m ≠ 0 ∧
      (n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F q)) ∧
        f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ m
have hne : multiplicity p f ≠ 0
Tactic: have hne := (multiplicity_pos_of_dvd hf).ne'
-- 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
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H : n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F q)
hp : p = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
hF : FiniteMultiplicity p f
hne : multiplicity p f ≠ 0
⊢ ∃ (m : ℕ) (n : ℕ) (y : F),
    m ≠ 0 ∧
      (n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F q)) ∧
        f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ m
have refine : f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ multiplicity p f
Tactic: refine ⟨_, n, y, hne, 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
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H : n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F q)
hp : p = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
hF : FiniteMultiplicity p f
hne : multiplicity p f ≠ 0
⊢ f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ multiplicity p f
have obtain : ∀ (c : F[X]) (hf : f = p ^ multiplicity p f * c) (H : ¬p ∣ c),
  f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ multiplicity p f
Tactic: obtain ⟨c, hf, H⟩ := hF.exists_eq_pow_mul_and_not_dvd
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf_1 : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H_1 : n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F q)
hp : p = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
hF : FiniteMultiplicity p f
hne : multiplicity p f ≠ 0
c : F[X]
hf : f = p ^ multiplicity p f * c
H : ¬p ∣ c
⊢ f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ multiplicity p f
have h₁ : c.natDegree = 0
Tactic: rw [hf, natSepDegree_mul_of_isCoprime _ c <| IsCoprime.pow_left <|
    (hI.isCoprime_or_dvd c).resolve_right H, natSepDegree_pow_of_ne_zero _ hne, hD,
    add_eq_left, natSepDegree_eq_zero_iff] at h
Cleared hypotheses: h, hf, H