awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
⊢ eval t
      (m.choose 0 •
        ((⇑derivative : (a : R[X]) → R[X])^[m - 0]
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m) *
          (⇑derivative : (a : R[X]) → R[X])^[0]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    m ! • eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m)
have rw : (↑m ! : R) *
    eval t
      ((⇑derivative : (a : R[X]) → R[X])^[0]
        (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m)) =
  (↑m ! : R) * eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m)
Tactic: rw [m.choose_zero_right, one_smul, eval_mul, m.sub_zero, iterate_derivative_X_sub_pow_self,
      eval_natCast, nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
b : ℕ
hb : b ∈ range m.succ
hb0 : b ≠ 0
⊢ eval t
      (m.choose b •
        ((⇑derivative : (a : R[X]) → R[X])^[m - b]
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m) *
          (⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
have rw : eval t
    (m.choose b •
      (m.descFactorial (m - b) • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ (m - (m - b)) *
        (⇑derivative : (a : R[X]) → R[X])^[b]
          (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
  0
Tactic: rw [iterate_derivative_X_sub_pow, eval_smul, eval_mul, eval_smul, eval_pow,
      Nat.sub_sub_self (mem_range_succ_iff.mp hb), eval_sub, eval_X, eval_C, sub_self,
      zero_pow hb0, smul_zero, zero_mul, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
b : ℕ
hb : b ∈ range m.succ
hb0 : b ≠ 0
rw :
  eval t
      (m.choose b •
        (m.descFactorial (m - b) • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ (m - (m - b)) *
          (⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
⊢ eval t
      (m.choose b •
        ((⇑derivative : (a : R[X]) → R[X])^[m - b]
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m) *
          (⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
have rw₁ : m.choose b •
    eval t
      (m.descFactorial (m - b) • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ (m - (m - b)) *
        (⇑derivative : (a : R[X]) → R[X])^[b]
          (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m)) =
  0
Tactic: rw [iterate_derivative_X_sub_pow, eval_smul, eval_mul, eval_smul, eval_pow,
      Nat.sub_sub_self (mem_range_succ_iff.mp hb), eval_sub, eval_X, eval_C, sub_self,
      zero_pow hb0, smul_zero, zero_mul, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
b : ℕ
hb : b ∈ range m.succ
hb0 : b ≠ 0
rw :
  eval t
      (m.choose b •
        (m.descFactorial (m - b) • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ (m - (m - b)) *
          (⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
rw₁ :
  m.choose b •
      eval t
        (m.descFactorial (m - b) • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ (m - (m - b)) *
          (⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m)) =
    0
⊢ eval t
      (m.choose b •
        ((⇑derivative : (a : R[X]) → R[X])^[m - b]
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m) *
          (⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
have rw₂ : m.choose b •
    (eval t
        (m.descFactorial (m - b) •
          HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ (m - (m - b))) *
      eval t
        ((⇑derivative : (a : R[X]) → R[X])^[b]
          (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
  0
Tactic: rw [iterate_derivative_X_sub_pow, eval_smul, eval_mul, eval_smul, eval_pow,
      Nat.sub_sub_self (mem_range_succ_iff.mp hb), eval_sub, eval_X, eval_C, sub_self,
      zero_pow hb0, smul_zero, zero_mul, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
b : ℕ
hb : b ∈ range m.succ
hb0 : b ≠ 0
rw :
  eval t
      (m.choose b •
        (m.descFactorial (m - b) • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ (m - (m - b)) *
          (⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
rw₁ :
  m.choose b •
      eval t
        (m.descFactorial (m - b) • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ (m - (m - b)) *
          (⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m)) =
    0
rw₂ :
  m.choose b •
      (eval t
          (m.descFactorial (m - b) •
            HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ (m - (m - b))) *
        eval t
          ((⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
⊢ eval t
      (m.choose b •
        ((⇑derivative : (a : R[X]) → R[X])^[m - b]
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m) *
          (⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
have rw₃ : m.choose b •
    (m.descFactorial (m - b) •
        eval t (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ (m - (m - b))) *
      eval t
        ((⇑derivative : (a : R[X]) → R[X])^[b]
          (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
  0
Tactic: rw [iterate_derivative_X_sub_pow, eval_smul, eval_mul, eval_smul, eval_pow,
      Nat.sub_sub_self (mem_range_succ_iff.mp hb), eval_sub, eval_X, eval_C, sub_self,
      zero_pow hb0, smul_zero, zero_mul, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
b : ℕ
hb : b ∈ range m.succ
hb0 : b ≠ 0
rw :
  eval t
      (m.choose b •
        (m.descFactorial (m - b) • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ (m - (m - b)) *
          (⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
rw₁ :
  m.choose b •
      eval t
        (m.descFactorial (m - b) • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ (m - (m - b)) *
          (⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m)) =
    0
rw₂ :
  m.choose b •
      (eval t
          (m.descFactorial (m - b) •
            HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ (m - (m - b))) *
        eval t
          ((⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
rw₃ :
  m.choose b •
      (m.descFactorial (m - b) •
          eval t (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ (m - (m - b))) *
        eval t
          ((⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
⊢ eval t
      (m.choose b •
        ((⇑derivative : (a : R[X]) → R[X])^[m - b]
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m) *
          (⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
have rw₄ : m.choose b •
    (m.descFactorial (m - b) •
        eval t (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) ^ (m - (m - b)) *
      eval t
        ((⇑derivative : (a : R[X]) → R[X])^[b]
          (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
  0
Tactic: rw [iterate_derivative_X_sub_pow, eval_smul, eval_mul, eval_smul, eval_pow,
      Nat.sub_sub_self (mem_range_succ_iff.mp hb), eval_sub, eval_X, eval_C, sub_self,
      zero_pow hb0, smul_zero, zero_mul, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
b : ℕ
hb : b ∈ range m.succ
hb0 : b ≠ 0
rw :
  eval t
      (m.choose b •
        (m.descFactorial (m - b) • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ (m - (m - b)) *
          (⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
rw₁ :
  m.choose b •
      eval t
        (m.descFactorial (m - b) • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ (m - (m - b)) *
          (⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m)) =
    0
rw₂ :
  m.choose b •
      (eval t
          (m.descFactorial (m - b) •
            HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ (m - (m - b))) *
        eval t
          ((⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
rw₃ :
  m.choose b •
      (m.descFactorial (m - b) •
          eval t (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ (m - (m - b))) *
        eval t
          ((⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
rw₄ :
  m.choose b •
      (m.descFactorial (m - b) •
          eval t (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) ^ (m - (m - b)) *
        eval t
          ((⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
⊢ eval t
      (m.choose b •
        ((⇑derivative : (a : R[X]) → R[X])^[m - b]
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m) *
          (⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
have rw₅ : m.choose b •
    (m.descFactorial (m - b) • eval t (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) ^ b *
      eval t
        ((⇑derivative : (a : R[X]) → R[X])^[b]
          (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
  0
Tactic: rw [iterate_derivative_X_sub_pow, eval_smul, eval_mul, eval_smul, eval_pow,
      Nat.sub_sub_self (mem_range_succ_iff.mp hb), eval_sub, eval_X, eval_C, sub_self,
      zero_pow hb0, smul_zero, zero_mul, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
b : ℕ
hb : b ∈ range m.succ
hb0 : b ≠ 0
rw :
  eval t
      (m.choose b •
        (m.descFactorial (m - b) • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ (m - (m - b)) *
          (⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
rw₁ :
  m.choose b •
      eval t
        (m.descFactorial (m - b) • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ (m - (m - b)) *
          (⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m)) =
    0
rw₂ :
  m.choose b •
      (eval t
          (m.descFactorial (m - b) •
            HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ (m - (m - b))) *
        eval t
          ((⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
rw₃ :
  m.choose b •
      (m.descFactorial (m - b) •
          eval t (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ (m - (m - b))) *
        eval t
          ((⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
rw₄ :
  m.choose b •
      (m.descFactorial (m - b) •
          eval t (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) ^ (m - (m - b)) *
        eval t
          ((⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
rw₅ :
  m.choose b •
      (m.descFactorial (m - b) • eval t (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) ^ b *
        eval t
          ((⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
⊢ eval t
      (m.choose b •
        ((⇑derivative : (a : R[X]) → R[X])^[m - b]
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m) *
          (⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
have rw₆ : m.choose b •
    (m.descFactorial (m - b) • (eval t X - eval t ((C : (a : R) → R[X]) t)) ^ b *
      eval t
        ((⇑derivative : (a : R[X]) → R[X])^[b]
          (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
  0
Tactic: rw [iterate_derivative_X_sub_pow, eval_smul, eval_mul, eval_smul, eval_pow,
      Nat.sub_sub_self (mem_range_succ_iff.mp hb), eval_sub, eval_X, eval_C, sub_self,
      zero_pow hb0, smul_zero, zero_mul, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
b : ℕ
hb : b ∈ range m.succ
hb0 : b ≠ 0
rw :
  eval t
      (m.choose b •
        (m.descFactorial (m - b) • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ (m - (m - b)) *
          (⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
rw₁ :
  m.choose b •
      eval t
        (m.descFactorial (m - b) • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ (m - (m - b)) *
          (⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m)) =
    0
rw₂ :
  m.choose b •
      (eval t
          (m.descFactorial (m - b) •
            HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ (m - (m - b))) *
        eval t
          ((⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
rw₃ :
  m.choose b •
      (m.descFactorial (m - b) •
          eval t (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ (m - (m - b))) *
        eval t
          ((⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
rw₄ :
  m.choose b •
      (m.descFactorial (m - b) •
          eval t (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) ^ (m - (m - b)) *
        eval t
          ((⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
rw₅ :
  m.choose b •
      (m.descFactorial (m - b) • eval t (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) ^ b *
        eval t
          ((⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
rw₆ :
  m.choose b •
      (m.descFactorial (m - b) • (eval t X - eval t ((C : (a : R) → R[X]) t)) ^ b *
        eval t
          ((⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
⊢ eval t
      (m.choose b •
        ((⇑derivative : (a : R[X]) → R[X])^[m - b]
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m) *
          (⇑derivative : (a : R[X]) → R[X])^[b]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    0
have rw₇ : m.choose b •
    (m.descFactorial (m - b) • (t - eval t ((C : (a : R) → R[X]) t)) ^ b *
      eval t
        ((⇑derivative : (a : R[X]) → R[X])^[b]
          (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
  0
Tactic: rw [iterate_derivative_X_sub_pow, eval_smul, eval_mul, eval_smul, eval_pow,
      Nat.sub_sub_self (mem_range_succ_iff.mp hb), eval_sub, eval_X, eval_C, sub_self,
      zero_pow hb0, smul_zero, zero_mul, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hroot : ∀ m ≤ n, ((⇑derivative : (a : R[X]) → R[X])^[m] p).IsRoot t
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑n ! : R)
⊢ n < rootMultiplicity t p
have by_contra! : ∀ (h' : rootMultiplicity t p ≤ n), False
Tactic: by_contra! h'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hroot : ∀ m ≤ n, ((⇑derivative : (a : R[X]) → R[X])^[m] p).IsRoot t
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑n ! : R)
h' : rootMultiplicity t p ≤ n
⊢ False
have hroot₁ : ((⇑derivative : (a : R[X]) → R[X])^[rootMultiplicity t p] p).IsRoot t
Tactic: replace hroot := hroot _ h'
Cleared hypotheses: hroot
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑n ! : R)
h' : rootMultiplicity t p ≤ n
hroot : ((⇑derivative : (a : R[X]) → R[X])^[rootMultiplicity t p] p).IsRoot t
⊢ False
have hroot₁ : (rootMultiplicity t p)! •
    eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p) =
  0
Tactic: simp only [IsRoot, eval_iterate_derivative_rootMultiplicity] at hroot
Cleared hypotheses: hroot
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑n ! : R)
h' : rootMultiplicity t p ≤ n
hroot :
  (rootMultiplicity t p)! •
      eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p) =
    0
⊢ False
have obtain : ∀ (q : R) (hq : (↑n ! : R) = (↑(rootMultiplicity t p)! : R) * q), False
Tactic: obtain ⟨q, hq⟩ : ((rootMultiplicity t p)! : R) ∣ n ! := by gcongr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑n ! : R)
h' : rootMultiplicity t p ≤ n
hroot :
  (rootMultiplicity t p)! •
      eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p) =
    0
q : R
hq : (↑n ! : R) = (↑(rootMultiplicity t p)! : R) * q
⊢ False
have hnzd₁ : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑(rootMultiplicity t p)! : R) ∧
  Membership.mem (γ := Submonoid R) (nonZeroDivisors R) q
Tactic: rw [hq, mul_mem_nonZeroDivisors] at hnzd
Cleared hypotheses: hnzd, hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
h' : rootMultiplicity t p ≤ n
hroot :
  (rootMultiplicity t p)! •
      eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p) =
    0
q : R
hnzd :
  Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑(rootMultiplicity t p)! : R) ∧
    Membership.mem (γ := Submonoid R) (nonZeroDivisors R) q
hq : (↑n ! : R) = (↑(rootMultiplicity t p)! : R) * q
⊢ False
have rw : ∀ (hroot : eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p) = 0)
  (q : R)
  (hnzd :
    Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑(rootMultiplicity t p)! : R) ∧
      Membership.mem (γ := Submonoid R) (nonZeroDivisors R) q)
  (hq : (↑n ! : R) = (↑(rootMultiplicity t p)! : R) * q), False
Tactic: rw [nsmul_eq_mul, mul_left_mem_nonZeroDivisors_eq_zero_iff hnzd.1] at hroot
Cleared hypotheses: hroot, q, hnzd, hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hroot : ∀ m ≤ n, ((⇑derivative : (a : R[X]) → R[X])^[m] p).IsRoot t
hnzd : ∀ m ≤ n, m ≠ 0 → Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
⊢ n < rootMultiplicity t p
have apply : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑n ! : R)
Tactic: apply lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors h hroot
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
h : p ≠ 0
hnzd : ∀ m ≤ 0, m ≠ 0 → Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
⊢ Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑0! : R)
have zero : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) 1
Tactic: simp only [Nat.factorial_zero, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
h : p ≠ 0
n : ℕ
ih :
  ∀ (hnzd : ∀ m ≤ n, m ≠ 0 → Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)),
    Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑n ! : R)
hnzd : ∀ m ≤ n + 1, m ≠ 0 → Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
⊢ Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑(n + 1)! : R)
have succ : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑(n + 1) : R) ∧
  Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑n ! : R)
Tactic: rw [Nat.factorial_succ, Nat.cast_mul, mul_mem_nonZeroDivisors]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hnzd : ∀ m ≤ n, m ≠ 0 → Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
⊢ Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑n ! : R)
have zero : ∀ (hnzd : ∀ m ≤ 0, m ≠ 0 → Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)),
  Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑0! : R)
Tactic: induction n with
  | zero =>
    simp only [Nat.factorial_zero, Nat.cast_one]
    exact Submonoid.one_mem _
  | succ n ih =>
    rw [Nat.factorial_succ, Nat.cast_mul, mul_mem_nonZeroDivisors]
    exact ⟨hnzd _ le_rfl n.succ_ne_zero, ih fun m h ↦ hnzd m (h.trans n.le_succ)⟩
Cleared hypotheses: n, hnzd