awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
H : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])
hp : p > 0
this : IsLocalHom (R := F[X]) (S := F[X]) (F := F[X] →ₐ[F] F[X]) (expand F p)
rw : ¬Ne (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])
rw₁ : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])
⊢ ¬f.Separable
have rw₂ : Eq.{u + 1} (α := F[X]) 0 0
Tactic: rw [separable_iff_derivative_ne_zero hf, Classical.not_not, H]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
H : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])
hp : p > 0
this : IsLocalHom (R := F[X]) (S := F[X]) (F := F[X] →ₐ[F] F[X]) (expand F p)
⊢ Irreducible (M := F[X]) ((expand F p : (a : F[X]) → F[X]) (contract p f) : F[X])
have rwa : ∀ (hf : Irreducible (M := F[X]) ((expand F p : (a : F[X]) → F[X]) (contract p f) : F[X]))
  (H : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])) (hp : p > 0)
  (this : IsLocalHom (R := F[X]) (S := F[X]) (F := F[X] →ₐ[F] F[X]) (expand F p)),
  Irreducible (M := F[X]) ((expand F p : (a : F[X]) → F[X]) (contract p f) : F[X])
Tactic: rwa [← expand_contract p H hp.ne'] at hf
Cleared hypotheses: H, hp, this
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : p ≠ 0
⊢ ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
have hp₁ : Nat.Prime p
Tactic: replace hp : p.Prime := (CharP.char_is_prime_or_zero F p).resolve_right hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : Nat.Prime p
⊢ ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
have h : ∀ (N : ℕ)
  (ih :
    ∀ m < N,
      ∀ {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)
  {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = N),
  ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
Tactic: induction hn : f.natDegree using Nat.strong_induction_on generalizing f with | _ N ih
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
N : ℕ
ih :
  ∀ m < N,
    ∀ {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
f : F[X]
hf : Irreducible f
hn : f.natDegree = N
⊢ ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
have h : ∀ (h : f.Separable), ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
Tactic: rcases separable_or p hf with (h | ⟨h1, g, hg, hgf⟩)
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
N : ℕ
ih :
  ∀ m < N,
    ∀ {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
f : F[X]
hf : Irreducible f
hn : f.natDegree = N
h : ∀ (h : f.Separable), ∃ (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
have h₁ : ∀ (h1 : ¬f.Separable) (g : F[X]) (hg : Irreducible g) (hgf : (expand F p : (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 separable_or p hf with (h | ⟨h1, g, hg, hgf⟩)
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
N : ℕ
ih :
  ∀ m < N,
    ∀ {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
f : F[X]
hf : Irreducible f
hn : f.natDegree = N
h : f.Separable
⊢ ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
have h₁ : (expand F (HPow.hPow (β := ℕ) p 0) : (a : F[X]) → F[X]) f = f
Tactic: refine ⟨0, f, h, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
N : ℕ
ih :
  ∀ m < N,
    ∀ {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
f : F[X]
hf : Irreducible f
hn : f.natDegree = N
h : f.Separable
⊢ (expand F (HPow.hPow (β := ℕ) p 0) : (a : F[X]) → F[X]) f = f
have h₁ : (expand F 1 : (a : F[X]) → F[X]) f = f
Tactic: rw [pow_zero, expand_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
N : ℕ
ih :
  ∀ m < N,
    ∀ {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
f : F[X]
hf : Irreducible f
hn : f.natDegree = N
h : f.Separable
h₁ : (expand F 1 : (a : F[X]) → F[X]) f = f
⊢ (expand F (HPow.hPow (β := ℕ) p 0) : (a : F[X]) → F[X]) f = f
have h₂ : f = f
Tactic: rw [pow_zero, expand_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
N : ℕ
ih :
  ∀ m < N,
    ∀ {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
f : F[X]
hf : Irreducible f
hn : f.natDegree = N
h1 : ¬f.Separable
g : F[X]
hg : Irreducible g
hgf : (expand F p : (a : F[X]) → F[X]) g = f
⊢ ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
have h : ∀
  (ih :
    ∀ m < 0,
      ∀ {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 = 0), ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
Tactic: rcases N with - | N
Cleared hypotheses: N, ih, hn
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
N : ℕ
ih :
  ∀ m < N,
    ∀ {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
f : F[X]
hf : Irreducible f
hn : f.natDegree = N
h1 : ¬f.Separable
g : F[X]
hg : Irreducible g
hgf : (expand F p : (a : F[X]) → F[X]) g = f
h :
  ∀
    (ih :
      ∀ m < 0,
        ∀ {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 = 0), ∃ (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
have h₁ : ∀ (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]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
Tactic: rcases N with - | N
Cleared hypotheses: N, ih, hn
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
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
ih :
  ∀ m < 0,
    ∀ {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 = 0
⊢ ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
have hn₁ : f = (C : (a : F) → F[X]) (f.coeff 0)
Tactic: rw [natDegree_eq_zero_iff_degree_le_zero, degree_le_zero_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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
ih :
  ∀ m < 0,
    ∀ {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 = (C : (a : F) → F[X]) (f.coeff 0)
⊢ ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
have h : ∀ (h1 : f.coeff 0 = 0) (g : F[X]) (hg : Irreducible g) (hgf : (expand F p : (a : F[X]) → F[X]) g = f)
  (ih :
    ∀ m < 0,
      ∀ {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 = (C : (a : F) → F[X]) (f.coeff 0)),
  ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
Tactic: rw [hn, separable_C, isUnit_iff_ne_zero, Classical.not_not] at h1
Cleared hypotheses: h1, g, hg, hgf, ih, hn
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : f.coeff 0 = 0
g : F[X]
hg : Irreducible g
hgf : (expand F p : (a : F[X]) → F[X]) g = f
ih :
  ∀ m < 0,
    ∀ {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 = (C : (a : F) → F[X]) (f.coeff 0)
⊢ ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
have hf0 : f ≠ 0
Tactic: have hf0 : f ≠ 0 := hf.ne_zero
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : f.coeff 0 = 0
g : F[X]
hg : Irreducible g
hgf : (expand F p : (a : F[X]) → F[X]) g = f
ih :
  ∀ m < 0,
    ∀ {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 = (C : (a : F) → F[X]) (f.coeff 0)
hf0 : f ≠ 0
⊢ ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
have hn₁ : f = 0
Tactic: rw [h1, C_0] at hn
Cleared hypotheses: hn, hf0
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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
⊢ g.natDegree * p = N.succ
have rwa : natDegree.{u} (R := F) ((expand F p : (a : F[X]) → F[X]) g) = N.succ
Tactic: rwa [← natDegree_expand, hgf]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
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
⊢ ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
have hg1 : g.natDegree * p = N.succ
Tactic: have hg1 : g.natDegree * p = N.succ := by rwa [← natDegree_expand, hgf]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
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
this : g.natDegree = 0
⊢ False
have hg1₁ : 0 = N.succ
Tactic: rw [this, zero_mul] at hg1
Cleared hypotheses: hg1, this
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
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
⊢ ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
have hg2 : g.natDegree ≠ 0
Tactic: have hg2 : g.natDegree ≠ 0 := by
      intro this
      rw [this, zero_mul] at hg1
      cases hg1
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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
have rw : g.natDegree * 1 < g.natDegree * p
Tactic: rw [← mul_one g.natDegree, ← hg1]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
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
⊢ ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
have hg3 : 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
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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
⊢ ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
have 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
Tactic: rcases ih _ hg3 hg rfl with ⟨n, g, hg4, rfl⟩
Cleared hypotheses: g, hg, hgf, hg1, hg2, hg3
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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
have h : (expand F (p ^ (n + 1)) : (a : F[X]) → F[X]) g = f
Tactic: refine ⟨n + 1, g, hg4, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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
⊢ (expand F (p ^ (n + 1)) : (a : F[X]) → F[X]) g = f
have 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])
Tactic: rw [← hgf, expand_expand, pow_succ']
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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])
⊢ (expand F (p ^ (n + 1)) : (a : F[X]) → F[X]) g = f
have 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])
Tactic: rw [← hgf, expand_expand, pow_succ']
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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])
⊢ (expand F (p ^ (n + 1)) : (a : F[X]) → F[X]) g = f
have 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])
Tactic: rw [← hgf, expand_expand, pow_succ']
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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)
⊢ IsUnit f ∨ n = 0
have rw : ¬n = 0 → IsUnit f
Tactic: rw [or_iff_not_imp_right]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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])
have 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
Tactic: rw [derivative_expand, Nat.cast_pow, CharP.cast_eq_zero, zero_pow hn, zero_mul, mul_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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
⊢ Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) f) : F[X]) (0 : F[X])
have 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
Tactic: rw [derivative_expand, Nat.cast_pow, CharP.cast_eq_zero, zero_pow hn, zero_mul, mul_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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
⊢ Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) f) : F[X]) (0 : F[X])
have 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
Tactic: rw [derivative_expand, Nat.cast_pow, CharP.cast_eq_zero, zero_pow hn, zero_mul, mul_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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
⊢ Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) f) : F[X]) (0 : F[X])
have 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
Tactic: rw [derivative_expand, Nat.cast_pow, CharP.cast_eq_zero, zero_pow hn, zero_mul, mul_zero]