awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.Separable
g : F[X]
hg : Irreducible g
hgf : (expand F p : (a : F[X]) → F[X]) g = f
N : ℕ
ih :
  ∀ m < N + 1,
    ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
      ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
hn : f.natDegree = N + 1
hg1 : g.natDegree * p = N.succ
hg2 : g.natDegree ≠ 0
⊢ g.natDegree * 1 < g.natDegree * p

Tactic:
Nat.mul_lt_mul_of_pos_left hp.one_lt hg2.bot_lt

Premises used: Nat.Prime.one_lt, Nat.mul_lt_mul_of_pos_left, Ne.bot_lt
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.Separable
g : F[X]
hg : Irreducible g
hgf : (expand F p : (a : F[X]) → F[X]) g = f
N : ℕ
ih :
  ∀ m < N + 1,
    ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
      ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
hn : f.natDegree = N + 1
hg1 : g.natDegree * p = N.succ
hg2 : g.natDegree ≠ 0
⊢ g.natDegree * 1 < g.natDegree * p

Tactic:
exact Nat.mul_lt_mul_of_pos_left hp.one_lt hg2.bot_lt

Premises used: Nat.Prime.one_lt, Nat.mul_lt_mul_of_pos_left, Ne.bot_lt
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.Separable
g : F[X]
hg : Irreducible g
hgf : (expand F p : (a : F[X]) → F[X]) g = f
N : ℕ
ih :
  ∀ m < N + 1,
    ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
      ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
hn : f.natDegree = N + 1
hg1 : g.natDegree * p = N.succ
hg2 : g.natDegree ≠ 0
⊢ g.natDegree < N.succ

Tactic:
have hg3 : g.natDegree < N.succ := by
      rw [← mul_one g.natDegree, ← hg1]
      exact Nat.mul_lt_mul_of_pos_left hp.one_lt hg2.bot_lt
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.Separable
g : F[X]
hg : Irreducible g
hgf : (expand F p : (a : F[X]) → F[X]) g = f
N : ℕ
ih :
  ∀ m < N + 1,
    ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
      ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
hn : f.natDegree = N + 1
hg1 : g.natDegree * p = N.succ
hg2 : g.natDegree ≠ 0
hg3 : g.natDegree < N.succ
h :
  ∀ (n : ℕ) (g : F[X]) (hg4 : g.Separable)
    (hg : Irreducible (M := F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) g : F[X]))
    (hgf : (expand F p : (a : F[X]) → F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) g) = f)
    (hg1 : natDegree.{u} (R := F) ((expand F (p ^ n) : (a : F[X]) → F[X]) g) * p = N.succ)
    (hg2 : natDegree.{u} (R := F) ((expand F (p ^ n) : (a : F[X]) → F[X]) g) ≠ 0)
    (hg3 : natDegree.{u} (R := F) ((expand F (p ^ n) : (a : F[X]) → F[X]) g) < N.succ),
    ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
⊢ ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f

Tactic:
rcases ih _ hg3 hg rfl with ⟨n, g, hg4, rfl⟩

Premises used: rfl
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.Separable
N : ℕ
ih :
  ∀ m < N + 1,
    ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
      ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
hn : f.natDegree = N + 1
n : ℕ
g : F[X]
hg4 : g.Separable
hg : Irreducible (M := F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) g : F[X])
hgf : (expand F p : (a : F[X]) → F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) g) = f
hg1 : natDegree.{u} (R := F) ((expand F (p ^ n) : (a : F[X]) → F[X]) g) * p = N.succ
hg2 : natDegree.{u} (R := F) ((expand F (p ^ n) : (a : F[X]) → F[X]) g) ≠ 0
hg3 : natDegree.{u} (R := F) ((expand F (p ^ n) : (a : F[X]) → F[X]) g) < N.succ
⊢ ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f

Tactic:
⟨n + 1, g, hg4, ?_⟩

Premises used: HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.Separable
N : ℕ
ih :
  ∀ m < N + 1,
    ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
      ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
hn : f.natDegree = N + 1
n : ℕ
g : F[X]
hg4 : g.Separable
hg : Irreducible (M := F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) g : F[X])
hgf : (expand F p : (a : F[X]) → F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) g) = f
hg1 : natDegree.{u} (R := F) ((expand F (p ^ n) : (a : F[X]) → F[X]) g) * p = N.succ
hg2 : natDegree.{u} (R := F) ((expand F (p ^ n) : (a : F[X]) → F[X]) g) ≠ 0
hg3 : natDegree.{u} (R := F) ((expand F (p ^ n) : (a : F[X]) → F[X]) g) < N.succ
h : (expand F (p ^ (n + 1)) : (a : F[X]) → F[X]) g = f
⊢ ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f

Tactic:
refine ⟨n + 1, g, hg4, ?_⟩
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.Separable
N : ℕ
ih :
  ∀ m < N + 1,
    ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
      ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
hn : f.natDegree = N + 1
n : ℕ
g : F[X]
hg4 : g.Separable
hg : Irreducible (M := F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) g : F[X])
hgf : (expand F p : (a : F[X]) → F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) g) = f
hg1 : natDegree.{u} (R := F) ((expand F (p ^ n) : (a : F[X]) → F[X]) g) * p = N.succ
hg2 : natDegree.{u} (R := F) ((expand F (p ^ n) : (a : F[X]) → F[X]) g) ≠ 0
hg3 : natDegree.{u} (R := F) ((expand F (p ^ n) : (a : F[X]) → F[X]) g) < N.succ
h :
  Eq (α := F[X]) ((expand F (p ^ (n + 1)) : (a : F[X]) → F[X]) g : F[X])
    ((expand F p : (a : F[X]) → F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) g) : F[X])
h₁ :
  Eq (α := F[X]) ((expand F (p ^ (n + 1)) : (a : F[X]) → F[X]) g : F[X])
    ((expand F (p * p ^ n) : (a : F[X]) → F[X]) g : F[X])
h₂ h₃ :
  Eq (α := F[X]) ((expand F (p * p ^ n) : (a : F[X]) → F[X]) g : F[X])
    ((expand F (p * p ^ n) : (a : F[X]) → F[X]) g : F[X])
⊢ (expand F (p ^ (n + 1)) : (a : F[X]) → F[X]) g = f

Tactic:
rw [← hgf, expand_expand, pow_succ']

Premises used: Polynomial.expand_expand, pow_succ'
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : Separable.{u} (R := F) ((expand F (p ^ n) : (a : F[X]) → F[X]) f)
rw : ¬n = 0 → IsUnit f
⊢ IsUnit f ∨ n = 0

Tactic:
rw [or_iff_not_imp_right]

Premises used: Classical.or_iff_not_imp_right
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : Separable.{u} (R := F) ((expand F (p ^ n) : (a : F[X]) → F[X]) f)
hn : n ≠ 0
rw :
  HMul.hMul (α := F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) ((derivative : (a : F[X]) → F[X]) f) : F[X])
      ((↑(p ^ n) : F[X]) * HPow.hPow (α := F[X]) X (p ^ n - 1)) =
    0
rw₁ :
  HMul.hMul (α := F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) ((derivative : (a : F[X]) → F[X]) f) : F[X])
      (HPow.hPow (α := F[X]) (↑p : F[X]) n * HPow.hPow (α := F[X]) X (p ^ n - 1)) =
    0
rw₂ :
  HMul.hMul (α := F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) ((derivative : (a : F[X]) → F[X]) f) : F[X])
      (HPow.hPow (α := F[X]) 0 n * HPow.hPow (α := F[X]) X (p ^ n - 1)) =
    0
rw₃ :
  HMul.hMul (α := F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) ((derivative : (a : F[X]) → F[X]) f) : F[X])
      (0 * HPow.hPow (α := F[X]) X (p ^ n - 1)) =
    0
rw₄ :
  HMul.hMul (α := F[X]) (β := F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) ((derivative : (a : F[X]) → F[X]) f) : F[X])
      (0 : F[X]) =
    0
rw₅ rw₆ : Eq.{u + 1} (α := F[X]) 0 0
⊢ Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) f) : F[X]) (0 : F[X])

Tactic:
rw [derivative_expand, Nat.cast_pow, CharP.cast_eq_zero, zero_pow hn, zero_mul, mul_zero]

Premises used: CharP.cast_eq_zero, Polynomial.derivative_expand, MulZeroClass.zero_mul, MulZeroClass.mul_zero, Nat.cast_pow, zero_pow
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : Separable.{u} (R := F) ((expand F (p ^ n) : (a : F[X]) → F[X]) f)
hn : n ≠ 0
⊢ Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) f) : F[X]) (0 : F[X])

Tactic:
have hf2 : derivative (expand F (p ^ n) f) = 0 := by
    rw [derivative_expand, Nat.cast_pow, CharP.cast_eq_zero, zero_pow hn, zero_mul, mul_zero]
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : Separable.{u} (R := F) ((expand F (p ^ n) : (a : F[X]) → F[X]) f)
hn : n ≠ 0
hf2 : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) f) : F[X]) (0 : F[X])
⊢ ∃ (r : F), IsUnit r ∧ Eq (α := F[X]) ((C : (a : F) → F[X]) r : F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) f : F[X])

Tactic:
rw [separable_def, hf2, isCoprime_zero_right, isUnit_iff] at hf

Premises used: Polynomial.isUnit_iff, Polynomial.separable_def, isCoprime_zero_right
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : Separable.{u} (R := F) ((expand F (p ^ n) : (a : F[X]) → F[X]) f)
hn : n ≠ 0
hf2 : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) f) : F[X]) (0 : F[X])
hf₁ :
  ∃ (r : F), IsUnit r ∧ Eq (α := F[X]) ((C : (a : F) → F[X]) r : F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) f : F[X])
⊢ n ≠ 0

Tactic:
rw [separable_def, hf2, isCoprime_zero_right, isUnit_iff] at hf

Premises used: Polynomial.isUnit_iff, Polynomial.separable_def, isCoprime_zero_right
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : Separable.{u} (R := F) ((expand F (p ^ n) : (a : F[X]) → F[X]) f)
hn : n ≠ 0
hf2 : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) f) : F[X]) (0 : F[X])
hf₁ :
  ∃ (r : F), IsUnit r ∧ Eq (α := F[X]) ((C : (a : F) → F[X]) r : F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) f : F[X])
hn₁ : n ≠ 0
⊢ Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) f) : F[X]) (0 : F[X])

Tactic:
rw [separable_def, hf2, isCoprime_zero_right, isUnit_iff] at hf

Premises used: Polynomial.isUnit_iff, Polynomial.separable_def, isCoprime_zero_right
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf :
  ∃ (r : F), IsUnit r ∧ Eq (α := F[X]) ((C : (a : F) → F[X]) r : F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) f : F[X])
hn : n ≠ 0
hf2 : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) f) : F[X]) (0 : F[X])
rcases :
  ∀ (r : F) (hr : IsUnit r)
    (hrf : Eq (α := F[X]) ((C : (a : F) → F[X]) r : F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) f : F[X])), IsUnit f
⊢ IsUnit f

Tactic:
rcases hf with ⟨r, hr, hrf⟩
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hn : n ≠ 0
hf2 : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) f) : F[X]) (0 : F[X])
r : F
hr : IsUnit r
hrf : Eq (α := F[X]) ((C : (a : F) → F[X]) r : F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) f : F[X])
⊢ f = (C : (a : F) → F[X]) r

Tactic:
rw [eq_comm, expand_eq_C (pow_pos hp _)] at hrf

Premises used: pow_pos, eq_comm, Polynomial.expand_eq_C
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hn : n ≠ 0
hf2 : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) f) : F[X]) (0 : F[X])
r : F
hr : IsUnit r
hrf : f = (C : (a : F) → F[X]) r
rwa : IsUnit (M := F[X]) ((C : (a : F) → F[X]) r : F[X])
rwa₁ rwa₂ rwa₃ rwa₄ : IsUnit r
⊢ IsUnit f

Tactic:
rwa [hrf, isUnit_C]

Premises used: Polynomial.isUnit_C
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ : ℕ
g₁ : F[X]
hg₁ : g₁.Separable
hgf₁ : (expand F (p ^ n₁) : (a : F[X]) → F[X]) g₁ = f
n₂ : ℕ
g₂ : F[X]
hg₂ : g₂.Separable
hgf₂ : (expand F (p ^ n₂) : (a : F[X]) → F[X]) g₂ = f
revert :
  ∀ (g₁ : F[X]) (hg₁ : g₁.Separable) (hgf₁ : (expand F (p ^ n₁) : (a : F[X]) → F[X]) g₁ = f) (g₂ : F[X])
    (hg₂ : g₂.Separable) (hgf₂ : (expand F (p ^ n₂) : (a : F[X]) → F[X]) g₂ = f), n₁ = n₂ ∧ g₁ = g₂
⊢ n₁ = n₂ ∧ g₁ = g₂

Tactic:
revert g₁ g₂
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ n₂ : ℕ
inr :
  ∀
    (this :
      ∀ {F : Type u} [inst : Field F] (p : ℕ) [HF : CharP F p] {f : F[X]} (hf : Irreducible f) (hp : 0 < p) (n₁ n₂ : ℕ)
        (hn : n₁ ≤ n₂) (g₁ : F[X]) (hg₁ : g₁.Separable) (hgf₁ : (expand F (p ^ n₁) : (a : F[X]) → F[X]) g₁ = f)
        (g₂ : F[X]) (hg₂ : g₂.Separable) (hgf₂ : (expand F (p ^ n₂) : (a : F[X]) → F[X]) g₂ = f), n₁ = n₂ ∧ g₁ = g₂)
    (hn : ¬n₁ ≤ n₂) (g₁ : F[X]) (hg₁ : g₁.Separable) (hgf₁ : (expand F (p ^ n₁) : (a : F[X]) → F[X]) g₁ = f) (g₂ : F[X])
    (hg₂ : g₂.Separable) (hgf₂ : (expand F (p ^ n₂) : (a : F[X]) → F[X]) g₂ = f), n₁ = n₂ ∧ g₁ = g₂
wlog :
  ∀ {F : Type u} [inst : Field F] (p : ℕ) [HF : CharP F p] {f : F[X]} (hf : Irreducible f) (hp : 0 < p) (n₁ n₂ : ℕ)
    (hn : n₁ ≤ n₂) (g₁ : F[X]) (hg₁ : g₁.Separable) (hgf₁ : (expand F (p ^ n₁) : (a : F[X]) → F[X]) g₁ = f) (g₂ : F[X])
    (hg₂ : g₂.Separable) (hgf₂ : (expand F (p ^ n₂) : (a : F[X]) → F[X]) g₂ = f), n₁ = n₂ ∧ g₁ = g₂
⊢ ∀ (g₁ : F[X]) (hg₁ : g₁.Separable) (hgf₁ : (expand F (p ^ n₁) : (a : F[X]) → F[X]) g₁ = f) (g₂ : F[X])
    (hg₂ : g₂.Separable) (hgf₂ : (expand F (p ^ n₂) : (a : F[X]) → F[X]) g₂ = f), n₁ = n₂ ∧ g₁ = g₂

Tactic:
wlog hn : n₁ ≤ n₂
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ n₂ : ℕ
this :
  ∀ {F : Type u} [inst : Field F] (p : ℕ) [HF : CharP F p] {f : F[X]} (hf : Irreducible f) (hp : 0 < p) (n₁ n₂ : ℕ)
    (hn : n₁ ≤ n₂) (g₁ : F[X]) (hg₁ : g₁.Separable) (hgf₁ : (expand F (p ^ n₁) : (a : F[X]) → F[X]) g₁ = f) (g₂ : F[X])
    (hg₂ : g₂.Separable) (hgf₂ : (expand F (p ^ n₂) : (a : F[X]) → F[X]) g₂ = f), n₁ = n₂ ∧ g₁ = g₂
hn : ¬n₁ ≤ n₂
g₁ : F[X]
hg₁ : g₁.Separable
Hg₁ : (expand F (p ^ n₁) : (a : F[X]) → F[X]) g₁ = f
g₂ : F[X]
hg₂ : g₂.Separable
Hg₂ : (expand F (p ^ n₂) : (a : F[X]) → F[X]) g₂ = f
⊢ n₁ = n₂ ∧ g₁ = g₂

Tactic:
simpa only [eq_comm] using this p hf hp n₂ n₁ (le_of_not_ge hn) g₂ hg₂ Hg₂ g₁ hg₁ Hg₁

Premises used: le_of_not_ge, eq_comm
-- Module: Mathlib.FieldTheory.Separable
Goal:
F_1 : Type u
inst : Field F_1
p_1 : ℕ
F : Type u
inst_1 : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ n₂ : ℕ
hn : n₁ ≤ n₂
g₁ : F[X]
hg₁ : g₁.Separable
hgf₁ : (expand F (p ^ n₁) : (a : F[X]) → F[X]) g₁ = f
g₂ : F[X]
hg₂ : g₂.Separable
hgf₂ : (expand F (p ^ n₂) : (a : F[X]) → F[X]) g₂ = f
rw :
  ∀ (hn : ∃ (c : ℕ), n₂ = n₁ + c) (g₁ : F[X]) (hg₁ : g₁.Separable)
    (hgf₁ : (expand F (p ^ n₁) : (a : F[X]) → F[X]) g₁ = f) (g₂ : F[X]) (hg₂ : g₂.Separable)
    (hgf₂ : (expand F (p ^ n₂) : (a : F[X]) → F[X]) g₂ = f), n₁ = n₂ ∧ g₁ = g₂
⊢ n₁ = n₂ ∧ g₁ = g₂

Tactic:
rw [le_iff_exists_add] at hn

Premises used: le_iff_exists_add
-- Module: Mathlib.FieldTheory.Separable
Goal:
F_1 : Type u
inst : Field F_1
p_1 : ℕ
F : Type u
inst_1 : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ n₂ : ℕ
hn : ∃ (c : ℕ), n₂ = n₁ + c
g₁ : F[X]
hg₁ : g₁.Separable
hgf₁ : (expand F (p ^ n₁) : (a : F[X]) → F[X]) g₁ = f
g₂ : F[X]
hg₂ : g₂.Separable
hgf₂ : (expand F (p ^ n₂) : (a : F[X]) → F[X]) g₂ = f
rcases : ∀ (k : ℕ) (hgf₂ : (expand F (p ^ (n₁ + k)) : (a : F[X]) → F[X]) g₂ = f), n₁ = n₁ + k ∧ g₁ = g₂
⊢ n₁ = n₂ ∧ g₁ = g₂

Tactic:
rcases hn with ⟨k, rfl⟩

Premises used: rfl
-- Module: Mathlib.FieldTheory.Separable
Goal:
F_1 : Type u
inst : Field F_1
p_1 : ℕ
F : Type u
inst_1 : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ : ℕ
g₁ : F[X]
hg₁ : g₁.Separable
hgf₁ : (expand F (p ^ n₁) : (a : F[X]) → F[X]) g₁ = f
g₂ : F[X]
hg₂ : g₂.Separable
k : ℕ
hgf₂ : (expand F (p ^ (n₁ + k)) : (a : F[X]) → F[X]) g₂ = f
⊢ (expand F (p ^ k) : (a : F[X]) → F[X]) g₂ = g₁

Tactic:
rw [← hgf₁, pow_add, expand_mul, expand_inj (pow_pos hp n₁)] at hgf₂

Premises used: pow_pos, pow_add, Polynomial.expand_inj, Polynomial.expand_mul
-- Module: Mathlib.FieldTheory.Separable
Goal:
F_1 : Type u
inst : Field F_1
p_1 : ℕ
F : Type u
inst_1 : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ : ℕ
g₁ : F[X]
hg₁ : g₁.Separable
hgf₁ : (expand F (p ^ n₁) : (a : F[X]) → F[X]) g₁ = f
g₂ : F[X]
hg₂ : g₂.Separable
k : ℕ
hgf₂ : (expand F (p ^ k) : (a : F[X]) → F[X]) g₂ = g₁
subst :
  ∀ (hg₁ : Separable.{u} (R := F) ((expand F (p ^ k) : (a : F[X]) → F[X]) g₂))
    (hgf₁ : (expand F (p ^ n₁) : (a : F[X]) → F[X]) ((expand F (p ^ k) : (a : F[X]) → F[X]) g₂) = f),
    n₁ = n₁ + k ∧ (expand F (p ^ k) : (a : F[X]) → F[X]) g₂ = g₂
⊢ n₁ = n₁ + k ∧ g₁ = g₂

Tactic:
subst hgf₂
-- Module: Mathlib.FieldTheory.Separable
Goal:
F_1 : Type u
inst : Field F_1
p_1 : ℕ
F : Type u
inst_1 : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : g₂.Separable
k : ℕ
hg₁ : Separable.{u} (R := F) ((expand F (p ^ k) : (a : F[X]) → F[X]) g₂)
hgf₁ : (expand F (p ^ n₁) : (a : F[X]) → F[X]) ((expand F (p ^ k) : (a : F[X]) → F[X]) g₂) = f
⊢ Irreducible (M := F[X]) ((expand F (p ^ n₁) : (a : F[X]) → F[X]) ((expand F (p ^ k) : (a : F[X]) → F[X]) g₂) : F[X])

Tactic:
subst hgf₁
-- Module: Mathlib.FieldTheory.Separable
Goal:
F_1 : Type u
inst : Field F_1
p_1 : ℕ
F : Type u
inst_1 : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : g₂.Separable
k : ℕ
hg₁ : Separable.{u} (R := F) ((expand F (p ^ k) : (a : F[X]) → F[X]) g₂)
hf :
  Irreducible (M := F[X]) ((expand F (p ^ n₁) : (a : F[X]) → F[X]) ((expand F (p ^ k) : (a : F[X]) → F[X]) g₂) : F[X])
inl : ∀ (h : IsUnit g₂), n₁ = n₁ + k ∧ (expand F (p ^ k) : (a : F[X]) → F[X]) g₂ = g₂
inr :
  ∀ (hg₁ : Separable.{u} (R := F) ((expand F (HPow.hPow (β := ℕ) p 0) : (a : F[X]) → F[X]) g₂))
    (hf :
      Irreducible (M := F[X])
        ((expand F (p ^ n₁) : (a : F[X]) → F[X]) ((expand F (HPow.hPow (β := ℕ) p 0) : (a : F[X]) → F[X]) g₂) : F[X])),
    n₁ = n₁ + 0 ∧ (expand F (HPow.hPow (β := ℕ) p 0) : (a : F[X]) → F[X]) g₂ = g₂
⊢ n₁ = n₁ + k ∧ (expand F (p ^ k) : (a : F[X]) → F[X]) g₂ = g₂

Tactic:
rcases isUnit_or_eq_zero_of_separable_expand p k hp hg₁ with (h | rfl)

Premises used: Polynomial.isUnit_or_eq_zero_of_separable_expand, rfl
-- Module: Mathlib.FieldTheory.Separable
Goal:
F_1 : Type u
inst : Field F_1
p_1 : ℕ
F : Type u
inst_1 : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : g₂.Separable
k : ℕ
hg₁ : Separable.{u} (R := F) ((expand F (p ^ k) : (a : F[X]) → F[X]) g₂)
hf :
  Irreducible (M := F[X]) ((expand F (p ^ n₁) : (a : F[X]) → F[X]) ((expand F (p ^ k) : (a : F[X]) → F[X]) g₂) : F[X])
h : IsUnit g₂
⊢ ∃ (r : F), IsUnit r ∧ (C : (a : F) → F[X]) r = g₂

Tactic:
rw [isUnit_iff] at h

Premises used: Polynomial.isUnit_iff
-- Module: Mathlib.FieldTheory.Separable
Goal:
F_1 : Type u
inst : Field F_1
p_1 : ℕ
F : Type u
inst_1 : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : g₂.Separable
k : ℕ
hg₁ : Separable.{u} (R := F) ((expand F (p ^ k) : (a : F[X]) → F[X]) g₂)
hf :
  Irreducible (M := F[X]) ((expand F (p ^ n₁) : (a : F[X]) → F[X]) ((expand F (p ^ k) : (a : F[X]) → F[X]) g₂) : F[X])
h : ∃ (r : F), IsUnit r ∧ (C : (a : F) → F[X]) r = g₂
inl :
  ∀ (r : F) (hr : IsUnit r) (hg₂ : Separable.{u} (R := F) ((C : (a : F) → F[X]) r))
    (hg₁ : Separable.{u} (R := F) ((expand F (p ^ k) : (a : F[X]) → F[X]) ((C : (a : F) → F[X]) r)))
    (hf :
      Irreducible (M := F[X])
        ((expand F (p ^ n₁) : (a : F[X]) → F[X]) ((expand F (p ^ k) : (a : F[X]) → F[X]) ((C : (a : F) → F[X]) r)) :
          F[X])),
    n₁ = n₁ + k ∧
      Eq (α := F[X]) ((expand F (p ^ k) : (a : F[X]) → F[X]) ((C : (a : F) → F[X]) r) : F[X])
        ((C : (a : F) → F[X]) r : F[X])
⊢ n₁ = n₁ + k ∧ (expand F (p ^ k) : (a : F[X]) → F[X]) g₂ = g₂

Tactic:
rcases h with ⟨r, hr, rfl⟩

Premises used: rfl
-- Module: Mathlib.FieldTheory.Separable
Goal:
F_1 : Type u
inst : Field F_1
p_1 : ℕ
F : Type u
inst_1 : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ k : ℕ
r : F
hr : IsUnit r
hg₂ : Separable.{u} (R := F) ((C : (a : F) → F[X]) r)
hg₁ : Separable.{u} (R := F) ((expand F (p ^ k) : (a : F[X]) → F[X]) ((C : (a : F) → F[X]) r))
hf :
  Irreducible (M := F[X])
    ((expand F (p ^ n₁) : (a : F[X]) → F[X]) ((expand F (p ^ k) : (a : F[X]) → F[X]) ((C : (a : F) → F[X]) r)) : F[X])
⊢ Irreducible (M := F[X]) ((C : (a : F) → F[X]) r : F[X])

Tactic:
simp_rw [expand_C] at hf

Premises used: Polynomial.expand_C
-- Module: Mathlib.FieldTheory.Separable
Goal:
F_1 : Type u
inst : Field F_1
p_1 : ℕ
F : Type u
inst_1 : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ k : ℕ
r : F
hr : IsUnit r
hg₂ : Separable.{u} (R := F) ((C : (a : F) → F[X]) r)
hg₁ : Separable.{u} (R := F) ((expand F (p ^ k) : (a : F[X]) → F[X]) ((C : (a : F) → F[X]) r))
hf : Irreducible (M := F[X]) ((C : (a : F) → F[X]) r : F[X])
⊢ n₁ = n₁ + k ∧
    Eq (α := F[X]) ((expand F (p ^ k) : (a : F[X]) → F[X]) ((C : (a : F) → F[X]) r) : F[X])
      ((C : (a : F) → F[X]) r : F[X])

Tactic:
absurd (isUnit_C.2 hr) hf.1

Premises used: Iff.mpr, Irreducible.not_isUnit, Polynomial.isUnit_C, absurd
-- Module: Mathlib.FieldTheory.Separable
Goal:
F_1 : Type u
inst : Field F_1
p_1 : ℕ
F : Type u
inst_1 : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ k : ℕ
r : F
hr : IsUnit r
hg₂ : Separable.{u} (R := F) ((C : (a : F) → F[X]) r)
hg₁ : Separable.{u} (R := F) ((expand F (p ^ k) : (a : F[X]) → F[X]) ((C : (a : F) → F[X]) r))
hf : Irreducible (M := F[X]) ((C : (a : F) → F[X]) r : F[X])
⊢ n₁ = n₁ + k ∧
    Eq (α := F[X]) ((expand F (p ^ k) : (a : F[X]) → F[X]) ((C : (a : F) → F[X]) r) : F[X])
      ((C : (a : F) → F[X]) r : F[X])

Tactic:
exact absurd (isUnit_C.2 hr) hf.1

Premises used: Iff.mpr, Irreducible.not_isUnit, Polynomial.isUnit_C, absurd
-- Module: Mathlib.FieldTheory.Separable
Goal:
F_1 : Type u
inst : Field F_1
p_1 : ℕ
F : Type u
inst_1 : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : g₂.Separable
hg₁ : Separable.{u} (R := F) ((expand F (HPow.hPow (β := ℕ) p 0) : (a : F[X]) → F[X]) g₂)
hf :
  Irreducible (M := F[X])
    ((expand F (p ^ n₁) : (a : F[X]) → F[X]) ((expand F (HPow.hPow (β := ℕ) p 0) : (a : F[X]) → F[X]) g₂) : F[X])
inr : n₁ = n₁ ∧ g₂ = g₂
⊢ n₁ = n₁ + 0 ∧ (expand F (HPow.hPow (β := ℕ) p 0) : (a : F[X]) → F[X]) g₂ = g₂

Tactic:
rw [add_zero, pow_zero, expand_one]

Premises used: Polynomial.expand_one, pow_zero, add_zero
-- Module: Mathlib.FieldTheory.Separable
Goal:
F_1 : Type u
inst : Field F_1
p_1 : ℕ
F : Type u
inst_1 : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : g₂.Separable
hg₁ : Separable.{u} (R := F) ((expand F (HPow.hPow (β := ℕ) p 0) : (a : F[X]) → F[X]) g₂)
hf :
  Irreducible (M := F[X])
    ((expand F (p ^ n₁) : (a : F[X]) → F[X]) ((expand F (HPow.hPow (β := ℕ) p 0) : (a : F[X]) → F[X]) g₂) : F[X])
inr : n₁ = n₁
inr₁ : g₂ = g₂
⊢ n₁ = n₁ ∧ g₂ = g₂

Tactic:
constructor
-- Module: Mathlib.FieldTheory.Separable
Goal:
F_1 : Type u
inst : Field F_1
p_1 : ℕ
F : Type u
inst_1 : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : g₂.Separable
hg₁ : Separable.{u} (R := F) ((expand F (HPow.hPow (β := ℕ) p 0) : (a : F[X]) → F[X]) g₂)
hf :
  Irreducible (M := F[X])
    ((expand F (p ^ n₁) : (a : F[X]) → F[X]) ((expand F (HPow.hPow (β := ℕ) p 0) : (a : F[X]) → F[X]) g₂) : F[X])
⊢ n₁ = n₁

Tactic:
rfl