-- 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
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
rw₈ :
  m.choose b •
      (m.descFactorial (m - b) • (t - 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) • HPow.hPow (α := R) 0 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]