awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f_1 f g : F[X]
h_1 : f = 0 ∨ g = 0
hf : f = 0
h : g = 0
rw : Eq.{u + 1} (α := F[X]) ((C : (a : F) → F[X]) 0) 0
rw₁ rw₂ : Eq.{u + 1} (α := F[X]) 0 0
⊢ (C : (a : F) → F[X]) 0 = g

Tactic:
rw [h, map_zero]

Premises used: map_zero
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f_1 f g : F[X]
h_1 : f = 0 ∨ g = 0
hf : f = 0
h : g = 0
⊢ ∃ (x : F), (C : (a : F) → F[X]) x = g

Tactic:
exact ⟨0, by rw [h, map_zero]⟩
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f_1 f g : F[X]
h_1 : f = 0 ∨ g = 0
hf : f = 0
x : F
h : (C : (a : F) → F[X]) x = g
⊢ ∃ (x : F), (C : (a : F) → F[X]) x = g

Tactic:
⟨x, h⟩

Premises used: Exists.intro
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f_1 f g : F[X]
h_1 : f = 0 ∨ g = 0
hf : f = 0
x : F
h : (C : (a : F) → F[X]) x = g
⊢ ∃ (x : F), (C : (a : F) → F[X]) x = g

Tactic:
exact ⟨x, h⟩
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f g : F[X]
h : ¬f * g = 0
neg :
  (∀ (a : AlgebraicClosure F),
      f ≠ 0 ∧
          Eq (α := AlgebraicClosure F) ((aeval a : (a : F[X]) → AlgebraicClosure F) f : AlgebraicClosure F)
            (0 : AlgebraicClosure F) →
        ∀ (b : AlgebraicClosure F),
          g ≠ 0 ∧
              Eq (α := AlgebraicClosure F) ((aeval b : (a : F[X]) → AlgebraicClosure F) g : AlgebraicClosure F)
                (0 : AlgebraicClosure F) →
            a ≠ b) ↔
    f = 0 ∧ g = 0 ∨ IsCoprime f g
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g

Tactic:
simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_mul h, Multiset.toFinset_add,
    Finset.card_union_eq_card_add_card, Finset.disjoint_iff_ne, Multiset.mem_toFinset, mem_aroots]

Premises used: Multiset.toFinset_add, Finset.card_union_eq_card_add_card, Finset.disjoint_iff_ne, Polynomial.natSepDegree_eq_of_isAlgClosed, Polynomial.mem_aroots, Polynomial.aroots_mul, AlgebraicClosure, Multiset.mem_toFinset
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f g : F[X]
h : ¬f * g = 0
⊢ ¬f = 0 ∧ ¬g = 0

Tactic:
rw [mul_eq_zero, not_or] at h

Premises used: mul_eq_zero, not_or
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
⊢ (∀ (a : AlgebraicClosure F),
      f ≠ 0 ∧
          Eq (α := AlgebraicClosure F) ((aeval a : (a : F[X]) → AlgebraicClosure F) f : AlgebraicClosure F)
            (0 : AlgebraicClosure F) →
        ∀ (b : AlgebraicClosure F),
          g ≠ 0 ∧
              Eq (α := AlgebraicClosure F) ((aeval b : (a : F[X]) → AlgebraicClosure F) g : AlgebraicClosure F)
                (0 : AlgebraicClosure F) →
            a ≠ b) ↔
    f = 0 ∧ g = 0 ∨ IsCoprime f g

Tactic:
⟨fun H ↦ .inr (isCoprime_of_irreducible_dvd (not_and.2 fun _ ↦ h.2)
    fun u hu ⟨v, hf⟩ ⟨w, hg⟩ ↦ ?_), ?_⟩

Premises used: Iff.mpr, False, _private.0.Polynomial.natSepDegree_mul_eq_iff.match_6, isCoprime_of_irreducible_dvd, And.right, Iff.intro, not_and, Or.inr
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
neg :
  ∀
    (H :
      ∀ (a : AlgebraicClosure F),
        f ≠ 0 ∧
            Eq (α := AlgebraicClosure F) ((aeval a : (a : F[X]) → AlgebraicClosure F) f : AlgebraicClosure F)
              (0 : AlgebraicClosure F) →
          ∀ (b : AlgebraicClosure F),
            g ≠ 0 ∧
                Eq (α := AlgebraicClosure F) ((aeval b : (a : F[X]) → AlgebraicClosure F) g : AlgebraicClosure F)
                  (0 : AlgebraicClosure F) →
              a ≠ b)
    (u : F[X]) (hu : Irreducible u), u ∣ f → u ∣ g → ∀ (v : F[X]) (hf : f = u * v) (w : F[X]) (hg : g = u * w), False
neg₁ :
  f = 0 ∧ g = 0 ∨ IsCoprime f g →
    ∀ (a : AlgebraicClosure F),
      f ≠ 0 ∧
          Eq (α := AlgebraicClosure F) ((aeval a : (a : F[X]) → AlgebraicClosure F) f : AlgebraicClosure F)
            (0 : AlgebraicClosure F) →
        ∀ (b : AlgebraicClosure F),
          g ≠ 0 ∧
              Eq (α := AlgebraicClosure F) ((aeval b : (a : F[X]) → AlgebraicClosure F) g : AlgebraicClosure F)
                (0 : AlgebraicClosure F) →
            a ≠ b
⊢ (∀ (a : AlgebraicClosure F),
      f ≠ 0 ∧
          Eq (α := AlgebraicClosure F) ((aeval a : (a : F[X]) → AlgebraicClosure F) f : AlgebraicClosure F)
            (0 : AlgebraicClosure F) →
        ∀ (b : AlgebraicClosure F),
          g ≠ 0 ∧
              Eq (α := AlgebraicClosure F) ((aeval b : (a : F[X]) → AlgebraicClosure F) g : AlgebraicClosure F)
                (0 : AlgebraicClosure F) →
            a ≠ b) ↔
    f = 0 ∧ g = 0 ∨ IsCoprime f g

Tactic:
refine ⟨fun H ↦ .inr (isCoprime_of_irreducible_dvd (not_and.2 fun _ ↦ h.2)
    fun u hu ⟨v, hf⟩ ⟨w, hg⟩ ↦ ?_), ?_⟩
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
H :
  ∀ (a : AlgebraicClosure F),
    f ≠ 0 ∧
        Eq (α := AlgebraicClosure F) ((aeval a : (a : F[X]) → AlgebraicClosure F) f : AlgebraicClosure F)
          (0 : AlgebraicClosure F) →
      ∀ (b : AlgebraicClosure F),
        g ≠ 0 ∧
            Eq (α := AlgebraicClosure F) ((aeval b : (a : F[X]) → AlgebraicClosure F) g : AlgebraicClosure F)
              (0 : AlgebraicClosure F) →
          a ≠ b
u : F[X]
hu : Irreducible u
h_1 : u ∣ f
h_2 : u ∣ g
v : F[X]
hf : f = u * v
w : F[X]
hg : g = u * w
neg :
  ∀ (x : AlgebraicClosure F)
    (hx :
      Eq (α := AlgebraicClosure F) ((aeval x : (a : F[X]) → AlgebraicClosure F) u : AlgebraicClosure F)
        (0 : AlgebraicClosure F)),
    False
⊢ False

Tactic:
obtain ⟨x, hx⟩ := IsAlgClosed.exists_aeval_eq_zero
      (AlgebraicClosure F) _ (degree_pos_of_irreducible hu).ne'

Premises used: LT.lt.ne', Polynomial.degree_pos_of_irreducible, AlgebraicClosure, IsAlgClosed.exists_aeval_eq_zero
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
H :
  ∀ (a : AlgebraicClosure F),
    f ≠ 0 ∧
        Eq (α := AlgebraicClosure F) ((aeval a : (a : F[X]) → AlgebraicClosure F) f : AlgebraicClosure F)
          (0 : AlgebraicClosure F) →
      ∀ (b : AlgebraicClosure F),
        g ≠ 0 ∧
            Eq (α := AlgebraicClosure F) ((aeval b : (a : F[X]) → AlgebraicClosure F) g : AlgebraicClosure F)
              (0 : AlgebraicClosure F) →
          a ≠ b
u : F[X]
hu : Irreducible u
h_1 : u ∣ f
h_2 : u ∣ g
v : F[X]
hf : f = u * v
w : F[X]
hg : g = u * w
x : AlgebraicClosure F
hx :
  Eq (α := AlgebraicClosure F) ((aeval x : (a : F[X]) → AlgebraicClosure F) u : AlgebraicClosure F)
    (0 : AlgebraicClosure F)
⊢ Eq (α := AlgebraicClosure F) ((aeval x : (a : F[X]) → AlgebraicClosure F) f : AlgebraicClosure F)
    (0 : AlgebraicClosure F)

Tactic:
simpa only [map_mul, hx, zero_mul] using congr(aeval x $hf)

Premises used: MulZeroClass.zero_mul, map_mul
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
H :
  ∀ (a : AlgebraicClosure F),
    f ≠ 0 ∧
        Eq (α := AlgebraicClosure F) ((aeval a : (a : F[X]) → AlgebraicClosure F) f : AlgebraicClosure F)
          (0 : AlgebraicClosure F) →
      ∀ (b : AlgebraicClosure F),
        g ≠ 0 ∧
            Eq (α := AlgebraicClosure F) ((aeval b : (a : F[X]) → AlgebraicClosure F) g : AlgebraicClosure F)
              (0 : AlgebraicClosure F) →
          a ≠ b
u : F[X]
hu : Irreducible u
h_1 : u ∣ f
h_2 : u ∣ g
v : F[X]
hf : f = u * v
w : F[X]
hg : g = u * w
x : AlgebraicClosure F
hx :
  Eq (α := AlgebraicClosure F) ((aeval x : (a : F[X]) → AlgebraicClosure F) u : AlgebraicClosure F)
    (0 : AlgebraicClosure F)
⊢ Eq (α := AlgebraicClosure F) ((aeval x : (a : F[X]) → AlgebraicClosure F) g : AlgebraicClosure F)
    (0 : AlgebraicClosure F)

Tactic:
simpa only [map_mul, hx, zero_mul] using congr(aeval x $hg)

Premises used: MulZeroClass.zero_mul, map_mul
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
H :
  ∀ (a : AlgebraicClosure F),
    f ≠ 0 ∧
        Eq (α := AlgebraicClosure F) ((aeval a : (a : F[X]) → AlgebraicClosure F) f : AlgebraicClosure F)
          (0 : AlgebraicClosure F) →
      ∀ (b : AlgebraicClosure F),
        g ≠ 0 ∧
            Eq (α := AlgebraicClosure F) ((aeval b : (a : F[X]) → AlgebraicClosure F) g : AlgebraicClosure F)
              (0 : AlgebraicClosure F) →
          a ≠ b
u : F[X]
hu : Irreducible u
h_1 : u ∣ f
h_2 : u ∣ g
v : F[X]
hf : f = u * v
w : F[X]
hg : g = u * w
x : AlgebraicClosure F
hx :
  Eq (α := AlgebraicClosure F) ((aeval x : (a : F[X]) → AlgebraicClosure F) u : AlgebraicClosure F)
    (0 : AlgebraicClosure F)
⊢ False

Tactic:
exact H x ⟨h.1, by simpa only [map_mul, hx, zero_mul] using congr(aeval x $hf)⟩
      x ⟨h.2, by simpa only [map_mul, hx, zero_mul] using congr(aeval x $hg)⟩ rfl

Premises used: And.right, And.left, And.intro, rfl
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
h : ¬Eq.{u + 1} (α := F[X]) 0 0 ∧ ¬Eq.{u + 1} (α := F[X]) 0 0
⊢ ∀ (a : AlgebraicClosure F),
    Ne.{u + 1} (α := F[X]) 0 0 ∧ Eq (α := AlgebraicClosure F) ((aeval a : (a : F[X]) → AlgebraicClosure F) 0) 0 →
      ∀ (b : AlgebraicClosure F),
        Ne.{u + 1} (α := F[X]) 0 0 ∧ Eq (α := AlgebraicClosure F) ((aeval b : (a : F[X]) → AlgebraicClosure F) 0) 0 →
          a ≠ b

Tactic:
(h.1 rfl).elim

Premises used: False.elim, And.left, rfl
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
h : ¬Eq.{u + 1} (α := F[X]) 0 0 ∧ ¬Eq.{u + 1} (α := F[X]) 0 0
⊢ ∀ (a : AlgebraicClosure F),
    Ne.{u + 1} (α := F[X]) 0 0 ∧ Eq (α := AlgebraicClosure F) ((aeval a : (a : F[X]) → AlgebraicClosure F) 0) 0 →
      ∀ (b : AlgebraicClosure F),
        Ne.{u + 1} (α := F[X]) 0 0 ∧ Eq (α := AlgebraicClosure F) ((aeval b : (a : F[X]) → AlgebraicClosure F) 0) 0 →
          a ≠ b

Tactic:
exact (h.1 rfl).elim

Premises used: False.elim, And.left, rfl
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
hc : IsCoprime f g
x : AlgebraicClosure F
hf :
  f ≠ 0 ∧
    Eq (α := AlgebraicClosure F) ((aeval x : (a : F[X]) → AlgebraicClosure F) f : AlgebraicClosure F)
      (0 : AlgebraicClosure F)
hg :
  g ≠ 0 ∧
    Eq (α := AlgebraicClosure F) ((aeval x : (a : F[X]) → AlgebraicClosure F) g : AlgebraicClosure F)
      (0 : AlgebraicClosure F)
neg : ∀ (u v : F[X]) (hfg : u * f + v * g = 1), False
⊢ False

Tactic:
obtain ⟨u, v, hfg⟩ := hc
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
x : AlgebraicClosure F
hf :
  f ≠ 0 ∧
    Eq (α := AlgebraicClosure F) ((aeval x : (a : F[X]) → AlgebraicClosure F) f : AlgebraicClosure F)
      (0 : AlgebraicClosure F)
hg :
  g ≠ 0 ∧
    Eq (α := AlgebraicClosure F) ((aeval x : (a : F[X]) → AlgebraicClosure F) g : AlgebraicClosure F)
      (0 : AlgebraicClosure F)
u v : F[X]
hfg : u * f + v * g = 1
⊢ False

Tactic:
simpa only [map_add, map_mul, map_one, hf.2, hg.2, mul_zero, add_zero,
    zero_ne_one] using congr(aeval x $hfg)

Premises used: zero_ne_one, map_add, MulZeroClass.mul_zero, map_mul, And.right, map_one, add_zero
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f g : F[X]
hc : IsCoprime f g
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree

Tactic:
(natSepDegree_mul_eq_iff f g).2 (.inr hc)

Premises used: Iff.mpr, Polynomial.natSepDegree_mul_eq_iff, Or.inr
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f g : F[X]
h1 : f ∣ g
h2 : g ≠ 0
simp_rw :
  Finset.card (α := AlgebraicClosure F) (Multiset.toFinset (f.aroots (AlgebraicClosure F))) ≤
    Finset.card (α := AlgebraicClosure F) (Multiset.toFinset (g.aroots (AlgebraicClosure F)))
⊢ f.natSepDegree ≤ g.natSepDegree

Tactic:
simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F)]

Premises used: Polynomial.natSepDegree_eq_of_isAlgClosed, AlgebraicClosure
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f g : F[X]
h1 : f ∣ g
h2 : g ≠ 0
⊢ Finset.card (α := AlgebraicClosure F) (Multiset.toFinset (f.aroots (AlgebraicClosure F))) ≤
    Finset.card (α := AlgebraicClosure F) (Multiset.toFinset (g.aroots (AlgebraicClosure F)))

Tactic:
Finset.card_le_card <| Multiset.toFinset_subset.mpr <|
    Multiset.Le.subset <| roots.le_of_dvd (map_ne_zero h2) <| map_dvd _ h1

Premises used: Iff.mpr, Polynomial.map_dvd, Finset.card_le_card, Polynomial.roots.le_of_dvd, Multiset.toFinset_subset, Polynomial.map_ne_zero, Multiset.Le.subset
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f g : F[X]
h1 : f ∣ g
h2 : g ≠ 0
⊢ Finset.card (α := AlgebraicClosure F) (Multiset.toFinset (f.aroots (AlgebraicClosure F))) ≤
    Finset.card (α := AlgebraicClosure F) (Multiset.toFinset (g.aroots (AlgebraicClosure F)))

Tactic:
exact Finset.card_le_card <| Multiset.toFinset_subset.mpr <|
    Multiset.Le.subset <| roots.le_of_dvd (map_ne_zero h2) <| map_dvd _ h1

Premises used: Iff.mpr, Polynomial.map_dvd, Finset.card_le_card, Polynomial.roots.le_of_dvd, Multiset.toFinset_subset, Polynomial.map_ne_zero, Multiset.Le.subset
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f g : F[X]
h1 : f ∣ g
h2 : g ≠ 0
simp_rw :
  Finset.card (α := AlgebraicClosure F) (Multiset.toFinset (f.aroots (AlgebraicClosure F))) ≤
    Finset.card (α := AlgebraicClosure F) (Multiset.toFinset (g.aroots (AlgebraicClosure F)))
⊢ f.natSepDegree ≤ g.natSepDegree

Tactic:
classical
  simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F)]
  exact Finset.card_le_card <| Multiset.toFinset_subset.mpr <|
    Multiset.Le.subset <| roots.le_of_dvd (map_ne_zero h2) <| map_dvd _ h1

Premises used: Iff.mpr, Polynomial.map_dvd, Finset.card_le_card, Polynomial.roots.le_of_dvd, Polynomial.natSepDegree_eq_of_isAlgClosed, Multiset.toFinset_subset, Polynomial.map_ne_zero, AlgebraicClosure, Multiset.Le.subset
-- Module: Mathlib.FieldTheory.SeparableDegree
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
prime :
  ∀ (hprime : Nat.Prime q) [CharP F q],
    natSepDegree.{u} (F := F) ((expand F (q ^ 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

Tactic:
obtain - | hprime := hF
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
n : ℕ
inst_1 : CharZero F
⊢ natSepDegree.{u} (F := F) ((expand F (HPow.hPow (α := ℕ) 1 n) : (a : F[X]) → F[X]) f) = f.natSepDegree

Tactic:
simp only [one_pow, expand_one]

Premises used: one_pow, Polynomial.expand_one
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
q n : ℕ
hprime : Nat.Prime q
hchar : CharP F q
⊢ Fact (Nat.Prime q)

Tactic:
haveI := Fact.mk hprime
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
q n : ℕ
hprime : Nat.Prime q
hchar : CharP F q
this : Fact (Nat.Prime q)
⊢ natSepDegree.{u} (F := F) ((expand F (q ^ n) : (a : F[X]) → F[X]) f) = f.natSepDegree

Tactic:
simpa only [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_def, map_expand,
    Fintype.card_coe] using Fintype.card_eq.2
      ⟨(f.map (algebraMap F (AlgebraicClosure F))).rootsExpandPowEquivRoots q n⟩

Premises used: Iff.mpr, Algebra.algebraMap, Polynomial.map_expand, Fintype.card_eq, Nonempty.intro, Polynomial.natSepDegree_eq_of_isAlgClosed, Polynomial.map, Polynomial.rootsExpandPowEquivRoots, AlgebraicClosure, Polynomial.aroots_def, Fintype.card_coe
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
q n : ℕ
hprime : Nat.Prime q
hchar : CharP F q
this : Fact (Nat.Prime q)
⊢ natSepDegree.{u} (F := F) ((expand F (q ^ n) : (a : F[X]) → F[X]) f) = f.natSepDegree

Tactic:
classical
  simpa only [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_def, map_expand,
    Fintype.card_coe] using Fintype.card_eq.2
      ⟨(f.map (algebraMap F (AlgebraicClosure F))).rootsExpandPowEquivRoots q n⟩

Premises used: Polynomial.map_expand, Polynomial.natSepDegree_eq_of_isAlgClosed, AlgebraicClosure, Polynomial.aroots_def, Fintype.card_coe
-- Module: Mathlib.FieldTheory.SeparableDegree
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
rw₄ rw₅ : Eq (α := ℕ) 1 1
⊢ (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((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]

Premises used: map_sub, Polynomial.expand_C, Polynomial.expand_X, Polynomial.natSepDegree_expand, HPow.hPow, Polynomial.natSepDegree_X_sub_C
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f g : F[X]
q : ℕ
inst_1 : ExpChar F q
h : IsSeparableContraction q f g
obtain : ∀ (h1 : g.Separable) (m : ℕ) (h2 : (expand F (q ^ m) : (a : F[X]) → F[X]) g = f), f.natSepDegree = g.natDegree
⊢ f.natSepDegree = g.natDegree

Tactic:
obtain ⟨h1, m, h2⟩ := h
-- Module: Mathlib.FieldTheory.SeparableDegree
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
rw₂ rw₃ : g.natDegree = g.natDegree
⊢ f.natSepDegree = g.natDegree

Tactic:
rw [← h2, natSepDegree_expand, h1.natSepDegree_eq_natDegree]

Premises used: Polynomial.Separable.natSepDegree_eq_natDegree, Polynomial.natSepDegree_expand
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hf : HasSeparableContraction q f
⊢ f.natSepDegree = hf.degree

Tactic:
hf.isSeparableContraction.natSepDegree_eq

Premises used: Polynomial.HasSeparableContraction.isSeparableContraction, Polynomial.IsSeparableContraction.natSepDegree_eq, Polynomial.HasSeparableContraction.degree
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
h : Irreducible f
obtain : ∀ (q : ℕ), ExpChar F q → f.natSepDegree ∣ f.natDegree
⊢ f.natSepDegree ∣ f.natDegree

Tactic:
obtain ⟨q, _⟩ := ExpChar.exists F

Premises used: ExpChar.exists
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
h : Irreducible f
q : ℕ
h_1 : ExpChar F q
⊢ HasSeparableContraction q f

Tactic:
have hf := h.hasSeparableContraction q
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
h : Irreducible f
q : ℕ
h_1 : ExpChar F q
hf : HasSeparableContraction q f
rw : hf.degree ∣ f.natDegree
⊢ f.natSepDegree ∣ f.natDegree

Tactic:
rw [hf.natSepDegree_eq]

Premises used: Polynomial.HasSeparableContraction.natSepDegree_eq
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
h : Irreducible f
q : ℕ
h_1 : ExpChar F q
hf : HasSeparableContraction q f
⊢ hf.degree ∣ f.natDegree

Tactic:
hf.dvd_degree

Premises used: Polynomial.HasSeparableContraction.dvd_degree
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
h : Irreducible f
q : ℕ
h_1 : ExpChar F q
hf : HasSeparableContraction q f
⊢ hf.degree ∣ f.natDegree

Tactic:
exact hf.dvd_degree

Premises used: Polynomial.HasSeparableContraction.dvd_degree
-- 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
⊢ 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:
⟨fun h ↦ ?_, fun ⟨n, y, h⟩ ↦ ?_⟩

Premises used: _private.0.Irreducible.natSepDegree_eq_one_iff_of_monic'.match_1, Polynomial.natSepDegree, Iff.intro, OfNat.ofNat, Eq
-- 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
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]))
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
⊢ 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⟩ ↦ ?_⟩
-- 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
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])
⊢ ∃ (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:
obtain ⟨g, h1, n, rfl⟩ := hi.hasSeparableContraction q

Premises used: Irreducible.hasSeparableContraction, rfl
-- 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
rwa : ∀ (h : g.natSepDegree = 1), g.natDegree = 1
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (h : g.natDegree = 1), g.natDegree = 1
⊢ g.natDegree = 1

Tactic:
rwa [natSepDegree_expand _ q, h1.natSepDegree_eq_natDegree] at h

Premises used: Polynomial.Separable.natSepDegree_eq_natDegree, Polynomial.natSepDegree_expand
-- 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
⊢ g.natDegree = 1

Tactic:
have h2 : g.natDegree = 1 := by
      rwa [natSepDegree_expand _ q, h1.natSepDegree_eq_natDegree] at h