awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.SeparableDegree
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
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])
⊢ ∃ (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:
rw [((monic_expand_iff <| expChar_pow_pos F q n).mp hm).eq_X_add_C h2]

Premises used: Polynomial.Monic.eq_X_add_C, Polynomial.monic_expand_iff, expChar_pow_pos, Iff.mp
-- Module: Mathlib.FieldTheory.SeparableDegree
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])
rw₁ 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])
⊢ 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]

Premises used: map_neg, sub_neg_eq_add
-- Module: Mathlib.FieldTheory.SeparableDegree
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])
          (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:
exact ⟨n, -(g.coeff 0), by rw [map_neg, sub_neg_eq_add]⟩
-- Module: Mathlib.FieldTheory.SeparableDegree
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
refine_2₂ refine_2₃ : Eq (α := ℕ) 1 1
⊢ f.natSepDegree = 1

Tactic:
rw [h, natSepDegree_expand _ q, natSepDegree_X_sub_C]

Premises used: Polynomial.natSepDegree_expand, Polynomial.natSepDegree_X_sub_C
-- Module: Mathlib.FieldTheory.SeparableDegree
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])
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])
⊢ 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])

Tactic:
simp_rw [hi.natSepDegree_eq_one_iff_of_monic' q hm, map_sub, expand_X, expand_C]

Premises used: Irreducible.natSepDegree_eq_one_iff_of_monic', map_sub, Polynomial.expand_C, Polynomial.expand_X
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
hm : f.Monic
hs : f.Splits
h : f.natSepDegree = 1
⊢ 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
-- Module: Mathlib.FieldTheory.SeparableDegree
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)
⊢ (f.aroots F).toFinset.card = f.natSepDegree

Tactic:
have h2 := (natSepDegree_eq_of_splits f (hs.map <| .id F)).symm
-- Module: Mathlib.FieldTheory.SeparableDegree
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
⊢ 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

Premises used: Algebra.algebraMap_self, Polynomial.map_id, Multiset.toFinset_card_eq_one_iff, Polynomial.aroots_def
-- Module: Mathlib.FieldTheory.SeparableDegree
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}
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
⊢ ∃ (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
-- Module: Mathlib.FieldTheory.SeparableDegree
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
rwa₄ rwa₅ rwa₆ 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
⊢ 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

Premises used: Multiset.map_singleton, Multiset.prod_singleton, Multiset.prod_nsmul, Multiset.map_nsmul
-- Module: Mathlib.FieldTheory.SeparableDegree
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}
⊢ ∃ (m : ℕ) (y : F), m ≠ 0 ∧ f = HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]) ^ m

Tactic:
exact ⟨_, y, h2, by rwa [h3, Multiset.map_nsmul, Multiset.map_singleton, Multiset.prod_nsmul,
    Multiset.prod_singleton] at h1⟩
-- Module: Mathlib.FieldTheory.SeparableDegree
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
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
⊢ ∃ (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⟩

Premises used: Algebra.algebraMap_self, Polynomial.map_id, Multiset.toFinset_card_eq_one_iff, Polynomial.aroots_def
-- Module: Mathlib.FieldTheory.SeparableDegree
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
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])
⊢ ∃ (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

Premises used: Iff.mp, Polynomial.Monic.natSepDegree_eq_one_iff_of_irreducible
-- Module: Mathlib.FieldTheory.SeparableDegree
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])
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])
⊢ ∃ (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])

Tactic:
simp_rw [one_pow, pow_one] at hf ⊢

Premises used: one_pow, pow_one
-- Module: Mathlib.FieldTheory.SeparableDegree
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]) (β := 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:
⟨0, y, .inl rfl, hf⟩

Premises used: And.intro, Exists.intro, Or.inl, OfNat.ofNat, rfl
-- Module: Mathlib.FieldTheory.SeparableDegree
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]) (β := 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:
exact ⟨0, y, .inl rfl, hf⟩
-- Module: Mathlib.FieldTheory.SeparableDegree
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])

Tactic:
⟨n, y, (em _).imp id fun hn ⟨z, hy⟩ ↦ ?_, hf⟩

Premises used: False, em, id, And.intro, Exists.intro, _private.0.Polynomial.Monic.eq_X_pow_char_pow_sub_C_of_natSepDegree_eq_one_of_irreducible.match_1, Or.imp
-- Module: Mathlib.FieldTheory.SeparableDegree
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
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
⊢ ∃ (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:
refine ⟨n, y, (em _).imp id fun hn ⟨z, hy⟩ ↦ ?_, hf⟩
-- Module: Mathlib.FieldTheory.SeparableDegree
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
⊢ ExpChar.{u} F[X] q

Tactic:
haveI := expChar_of_injective_ringHom (R := F) C_injective q
-- Module: Mathlib.FieldTheory.SeparableDegree
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
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
⊢ False

Tactic:
rw [hf, ← Nat.succ_pred hn, pow_succ, pow_mul, ← hy, frobenius_def, map_pow,
      ← sub_pow_expChar] at hi

Premises used: pow_succ, map_pow, pow_mul, Nat.succ_pred, frobenius_def, sub_pow_expChar
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm : f.Monic
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
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:
not_irreducible_pow hq.ne_one hi

Premises used: not_irreducible_pow, Nat.Prime.ne_one
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm : f.Monic
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
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:
exact not_irreducible_pow hq.ne_one hi

Premises used: not_irreducible_pow, Nat.Prime.ne_one
-- Module: Mathlib.FieldTheory.SeparableDegree
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])
⊢ ExpChar F q

Tactic:
cases id ‹ExpChar F q› with
  | zero =>
    simp_rw [one_pow, pow_one] at hf ⊢
    exact ⟨0, y, .inl rfl, hf⟩
  | prime hq =>
    refine ⟨n, y, (em _).imp id fun hn ⟨z, hy⟩ ↦ ?_, hf⟩
    haveI := expChar_of_injective_ringHom (R := F) C_injective q
    rw [hf, ← Nat.succ_pred hn, pow_succ, pow_mul, ← hy, frobenius_def, map_pow,
      ← sub_pow_expChar] at hi
    exact not_irreducible_pow hq.ne_one hi

Premises used: one_pow, pow_succ, id, map_pow, pow_mul, frobenius_def, pow_one, sub_pow_expChar
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
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
⊢ ∃ (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)

Premises used: Polynomial.not_isUnit_of_natDegree_pos, Polynomial.exists_monic_irreducible_factor, Polynomial.natSepDegree_ne_zero_iff, Nat.pos_of_ne_zero, Iff.mp
-- Module: Mathlib.FieldTheory.SeparableDegree
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
⊢ 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'
-- Module: Mathlib.FieldTheory.SeparableDegree
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
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
⊢ ∃ (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

Premises used: Polynomial.Monic.eq_X_pow_char_pow_sub_C_of_natSepDegree_eq_one_of_irreducible
-- Module: Mathlib.FieldTheory.SeparableDegree
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])
⊢ FiniteMultiplicity p f

Tactic:
have hF := finiteMultiplicity_of_degree_pos_of_monic (degree_pos_of_irreducible hI) hM hm.ne_zero
-- Module: Mathlib.FieldTheory.SeparableDegree
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
⊢ multiplicity p f ≠ 0

Tactic:
have hne := (multiplicity_pos_of_dvd hf).ne'