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]
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
⊢ 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]) (β := F[X]) ((expand F (p ^ n) : (a : F[X]) → F[X]) ((derivative : (a : F[X]) → F[X]) f) : F[X])
    (0 : F[X]) =
  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
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
⊢ 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₅ : Eq.{u + 1} (α := F[X]) 0 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 (hypothesis)
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
⊢ IsUnit f
have 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])
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
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])
⊢ IsUnit f
have 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])
Tactic: rw [separable_def, hf2, isCoprime_zero_right, isUnit_iff] at hf
Cleared hypotheses: hf, hn, hf2
-- 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 :
  ∃ (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])
⊢ IsUnit f
have 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
Tactic: rcases hf with ⟨r, hr, hrf⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
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])
⊢ IsUnit f
have hrf₁ : f = (C : (a : F) → F[X]) r
Tactic: rw [eq_comm, expand_eq_C (pow_pos hp _)] at hrf
Cleared hypotheses: hrf
-- 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
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
⊢ IsUnit f
have rwa : IsUnit (M := F[X]) ((C : (a : F) → F[X]) r : F[X])
Tactic: rwa [hrf, isUnit_C]
-- 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 : 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
⊢ n₁ = n₂ ∧ g₁ = g₂
have 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₂
Tactic: revert g₁ g₂
Cleared hypotheses: g₁, hg₁, hgf₁, g₂, hg₂, hgf₂
-- 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 : 0 < p
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₂
have 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₂
Tactic: wlog hn : n₁ ≤ n₂
-- 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 : 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₂
⊢ ∀ (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₂
have 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₂
Tactic: wlog hn : n₁ ≤ n₂
Cleared hypotheses: HF, f, hf, hp, n₁, n₂
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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
⊢ n₁ = n₂ ∧ g₁ = g₂
have 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₂
Tactic: rw [le_iff_exists_add] at hn
Cleared hypotheses: hn, g₁, hg₁, hgf₁, g₂, hg₂, hgf₂
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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
⊢ n₁ = n₂ ∧ g₁ = g₂
have rcases : ∀ (k : ℕ) (hgf₂ : (expand F (p ^ (n₁ + k)) : (a : F[X]) → F[X]) g₂ = f), n₁ = n₁ + k ∧ g₁ = g₂
Tactic: rcases hn with ⟨k, rfl⟩
Cleared hypotheses: n₂, hn, hgf₂
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
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
⊢ n₁ = n₁ + k ∧ g₁ = g₂
have hgf₃ : (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₂
Cleared hypotheses: hgf₂
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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₁
⊢ n₁ = n₁ + k ∧ g₁ = g₂
have 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₂
Tactic: subst hgf₂
Cleared hypotheses: g₁, hg₁, hgf₁, hgf₂
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
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
⊢ n₁ = n₁ + k ∧ (expand F (p ^ k) : (a : F[X]) → F[X]) g₂ = g₂
have 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])
Tactic: subst hgf₁
Cleared hypotheses: f, hf, hgf₁
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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])
⊢ n₁ = n₁ + k ∧ (expand F (p ^ k) : (a : F[X]) → F[X]) g₂ = g₂
have inl : ∀ (h : IsUnit 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)
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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₂
⊢ n₁ = n₁ + k ∧ (expand F (p ^ k) : (a : F[X]) → F[X]) g₂ = g₂
have 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₂
Tactic: rcases isUnit_or_eq_zero_of_separable_expand p k hp hg₁ with (h | rfl)
Cleared hypotheses: k, hg₁, hf
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
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₂
⊢ n₁ = n₁ + k ∧ (expand F (p ^ k) : (a : F[X]) → F[X]) g₂ = g₂
have h₁ : ∃ (r : F), IsUnit r ∧ (C : (a : F) → F[X]) r = g₂
Tactic: rw [isUnit_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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₂
⊢ n₁ = n₁ + k ∧ (expand F (p ^ k) : (a : F[X]) → F[X]) g₂ = g₂
have 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])
Tactic: rcases h with ⟨r, hr, rfl⟩
Cleared hypotheses: g₂, hg₂, hg₁, hf, h
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
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])
⊢ 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])
have hf₁ : Irreducible (M := F[X]) ((C : (a : F) → F[X]) r : F[X])
Tactic: simp_rw [expand_C] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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₁ + 0 ∧ (expand F (HPow.hPow (β := ℕ) p 0) : (a : F[X]) → F[X]) g₂ = g₂
have inr : n₁ = n₁ ∧ g₂ = g₂
Tactic: rw [add_zero, pow_zero, expand_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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₁ ∧ g₂ = g₂
have inr : n₁ = n₁
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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₁
⊢ n₁ = n₁ ∧ g₂ = g₂
have inr₁ : g₂ = g₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
p n : ℕ
a : F
inst_1 : CharP F p
hn : ¬p ∣ n
ha : a ≠ 0
⊢ Ne.{u + 1} (α := F) (↑n : F) 0
have rwa : ∀ (hn : ¬Eq.{u + 1} (α := F) (↑n : F) 0) (ha : a ≠ 0), Ne.{u + 1} (α := F) (↑n : F) 0
Tactic: rwa [← CharP.cast_eq_zero_iff F p n] at hn
Cleared hypotheses: hn, ha
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
n : ℕ
x : F
hn : 0 < n
hx : x ≠ 0
⊢ (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) x : F[X])).Separable ↔
    Ne.{u + 1} (α := F) (↑n : F) 0
have refine : ∀ (h : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) x : F[X])).Separable)
  (hn' : Eq.{u + 1} (α := F) (↑n : F) 0), False
Tactic: refine ⟨fun h hn' ↦ ?_, fun h => separable_X_pow_sub_C x h hx⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
n : ℕ
⊢ (HPow.hPow (α := F[X]) X n - 1).Separable ↔ Ne.{u + 1} (α := F) (↑n : F) 0
have inl : ∀ (hz : n = 0), (HPow.hPow (α := F[X]) X n - 1).Separable ↔ Ne.{u + 1} (α := F) (↑n : F) 0
Tactic: rcases (Nat.eq_zero_or_pos n) with (hz | hpos)
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
n : ℕ
inl : ∀ (hz : n = 0), (HPow.hPow (α := F[X]) X n - 1).Separable ↔ Ne.{u + 1} (α := F) (↑n : F) 0
⊢ (HPow.hPow (α := F[X]) X n - 1).Separable ↔ Ne.{u + 1} (α := F) (↑n : F) 0
have inr : ∀ (hpos : n > 0), (HPow.hPow (α := F[X]) X n - 1).Separable ↔ Ne.{u + 1} (α := F) (↑n : F) 0
Tactic: rcases (Nat.eq_zero_or_pos n) with (hz | hpos)
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
p : F[X]
hsep : p.Separable
hsplit : Splits (map (algebraMap F K) p)
⊢ Fintype.card.{v} (↑(p.rootSet K) : Type v) = p.natDegree
have simp_rw : #(p.aroots K).toFinset = p.natDegree
Tactic: simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
p : F[X]
hsep : p.Separable
hsplit : Splits (map (algebraMap F K) p)
⊢ #(p.aroots K).toFinset = p.natDegree
have rw : (roots (map (algebraMap F K) p)).card = p.natDegree
Tactic: rw [Multiset.toFinset_card_of_nodup (nodup_roots hsep.map), ← hsplit.natDegree_eq_card_roots,
    natDegree_map]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
p : F[X]
hsep : p.Separable
hsplit : Splits (map (algebraMap F K) p)
rw : (roots (map (algebraMap F K) p)).card = p.natDegree
⊢ #(p.aroots K).toFinset = p.natDegree
have rw₁ : natDegree (map (algebraMap F K) p) = p.natDegree
Tactic: rw [Multiset.toFinset_card_of_nodup (nodup_roots hsep.map), ← hsplit.natDegree_eq_card_roots,
    natDegree_map]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
p : F[X]
hsep : p.Separable
hsplit : Splits (map (algebraMap F K) p)
rw : (roots (map (algebraMap F K) p)).card = p.natDegree
rw₁ : natDegree (map (algebraMap F K) p) = p.natDegree
⊢ #(p.aroots K).toFinset = p.natDegree
have rw₂ : p.natDegree = p.natDegree
Tactic: rw [Multiset.toFinset_card_of_nodup (nodup_roots hsep.map), ← hsplit.natDegree_eq_card_roots,
    natDegree_map]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
p : F[X]
hsep : p.Separable
hsplit : Splits (map (algebraMap F K) p)
⊢ Fintype.card.{v} (↑(p.rootSet K) : Type v) = p.natDegree
have simp_rw : Fintype.card.{v} (↑(↑(p.aroots K).toFinset : Set K) : Type v) = p.natDegree
Tactic: classical
  simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]
  rw [Multiset.toFinset_card_of_nodup (nodup_roots hsep.map), ← hsplit.natDegree_eq_card_roots,
    natDegree_map]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
p : F[X]
hsep : p.Separable
hsplit : Splits (map (algebraMap F K) p)
simp_rw : Fintype.card.{v} (↑(↑(p.aroots K).toFinset : Set K) : Type v) = p.natDegree
⊢ Fintype.card.{v} (↑(p.rootSet K) : Type v) = p.natDegree
have simp_rw₁ : Fintype.card.{v} ↥(p.aroots K).toFinset = p.natDegree
Tactic: classical
  simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]
  rw [Multiset.toFinset_card_of_nodup (nodup_roots hsep.map), ← hsplit.natDegree_eq_card_roots,
    natDegree_map]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
p : F[X]
hsep : p.Separable
hsplit : Splits (map (algebraMap F K) p)
simp_rw : Fintype.card.{v} (↑(↑(p.aroots K).toFinset : Set K) : Type v) = p.natDegree
simp_rw₁ : Fintype.card.{v} ↥(p.aroots K).toFinset = p.natDegree
⊢ Fintype.card.{v} (↑(p.rootSet K) : Type v) = p.natDegree
have simp_rw₂ : #(p.aroots K).toFinset = p.natDegree
Tactic: classical
  simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]
  rw [Multiset.toFinset_card_of_nodup (nodup_roots hsep.map), ← hsplit.natDegree_eq_card_roots,
    natDegree_map]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
hf : f ≠ 0
h : f.Splits
⊢ f.roots.Nodup ↔ f.Separable
have refine : ∀ (hnsep : ¬f.Separable), ¬f.roots.Nodup
Tactic: refine ⟨(fun hnsep ↦ ?_).mtr, nodup_roots⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
Goal:
F : Type u
inst : Field F
f : F[X]
hf : f ≠ 0
h : f.Splits
hnsep : ¬f.Separable
⊢ ¬f.roots.Nodup
have hnsep₁ : ¬(@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ f ((derivative : (a : F[X]) → F[X]) f)).degree = 0
Tactic: rw [Separable, ← gcd_isUnit_iff, isUnit_iff_degree_eq_zero] at hnsep
Cleared hypotheses: hnsep
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
hf : f ≠ 0
h : f.Splits
hnsep : ¬(@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ f ((derivative : (a : F[X]) → F[X]) f)).degree = 0
⊢ ¬f.roots.Nodup
have obtain : ∀ (x : F)
  (hx : eval x (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ f ((derivative : (a : F[X]) → F[X]) f)) = 0),
  ¬f.roots.Nodup
Tactic: obtain ⟨x, hx⟩ := Splits.exists_eval_eq_zero (Splits.of_dvd h hf (gcd_dvd_left f _)) hnsep
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
hf : f ≠ 0
h : f.Splits
hnsep : ¬(@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ f ((derivative : (a : F[X]) → F[X]) f)).degree = 0
x : F
hx : eval x (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ f ((derivative : (a : F[X]) → F[X]) f)) = 0
⊢ ¬f.roots.Nodup
have simp_rw : ∃ (x : F), 1 < Multiset.count x f.roots
Tactic: simp_rw [Multiset.nodup_iff_count_le_one, not_forall, not_le]