-- Module: Mathlib.Algebra.Polynomial.FieldDivision
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
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
rw₁₀ :
  m.choose b •
      (HSMul.hSMul (β := R) (m.descFactorial (m - b)) 0 *
        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 •
      (0 *
        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₁₂ : HSMul.hSMul (β := R) (m.choose b) 0 = 0
rw₁₃ rw₁₄ : Eq.{u + 1} (α := R) 0 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

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]

Premises used: Nat.sub_sub_self, Polynomial.eval_C, sub_self, Polynomial.eval_X, Polynomial.eval_pow, Polynomial.iterate_derivative_X_sub_pow, MulZeroClass.zero_mul, Finset.mem_range_succ_iff, smul_zero, Polynomial.eval_mul, Iff.mp, Polynomial.eval_smul, Polynomial.eval_sub, zero_pow