-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem eval_iterate_derivative_rootMultiplicity {p : R[X]} {t : R} :
    (derivative^[p.rootMultiplicity t] p).eval t =
      (p.rootMultiplicity t).factorial • (p /ₘ (X - C t) ^ p.rootMultiplicity t).eval t

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
⊢ eval t ((⇑derivative)^[m] ((X - C t) ^ m * (p /ₘ (X - C t) ^ m))) = m.factorial • eval t (p /ₘ (X - C t) ^ m)

Tactic:
rw [iterate_derivative_mul, eval_finset_sum, sum_eq_single_of_mem _ (mem_range.mpr m.succ_pos)]

Result:
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)^[m - 0] ((X - C t) ^ m) * (⇑derivative)^[0] (p /ₘ (X - C t) ^ m))) =
    m.factorial • eval t (p /ₘ (X - C t) ^ m)

R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
⊢ ∀ b ∈ range m.succ,
    b ≠ 0 → eval t (m.choose b • ((⇑derivative)^[m - b] ((X - C t) ^ m) * (⇑derivative)^[b] (p /ₘ (X - C t) ^ m))) = 0

Proof state:
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)^[m - b] ((X - C t) ^ m) * (⇑derivative)^[b] (p /ₘ (X - C t) ^ 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]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
⊢ eval t ((⇑derivative)^[rootMultiplicity t p] p) =
    (rootMultiplicity t p).factorial • eval t (p /ₘ (X - C t) ^ rootMultiplicity t p)

Tactic:
set m := p.rootMultiplicity t with hm

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
⊢ eval t ((⇑derivative)^[m] p) = m.factorial • eval t (p /ₘ (X - C t) ^ m)

Proof state:
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)^[m - 0] ((X - C t) ^ m) * (⇑derivative)^[0] (p /ₘ (X - C t) ^ m))) =
    m.factorial • eval t (p /ₘ (X - C t) ^ 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]

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
⊢ ↑m.factorial * eval t ((⇑derivative)^[0] (p /ₘ (X - C t) ^ m)) = ↑m.factorial * eval t (p /ₘ (X - C t) ^ m)

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
⊢ ∀ b ∈ range m.succ,
    b ≠ 0 → eval t (m.choose b • ((⇑derivative)^[m - b] ((X - C t) ^ m) * (⇑derivative)^[b] (p /ₘ (X - C t) ^ m))) = 0

Tactic:
intro b hb hb0

Result:
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)^[m - b] ((X - C t) ^ m) * (⇑derivative)^[b] (p /ₘ (X - C t) ^ m))) = 0

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
⊢ ↑m.factorial * eval t ((⇑derivative)^[0] (p /ₘ (X - C t) ^ m)) = ↑m.factorial * eval t (p /ₘ (X - C t) ^ m)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
⊢ eval t ((⇑derivative)^[m] p) = m.factorial • eval t (p /ₘ (X - C t) ^ m)

Tactic:
conv_lhs => rw [← p.pow_mul_divByMonic_rootMultiplicity_eq t, ← hm]

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
⊢ eval t ((⇑derivative)^[m] ((X - C t) ^ m * (p /ₘ (X - C t) ^ m))) = m.factorial • eval t (p /ₘ (X - C t) ^ m)