no goals
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
x : R
⊢ eval x (↑derivative p) = sum p fun n a => a * ↑n * x ^ (n - 1)
simp_rw [derivative_apply, eval_sum, eval_mul_X_pow, eval_C]