no goals
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f : R[X]
⊢ ↑derivative (↑(expand R p) f) = ↑(expand R p) (↑derivative f) * (↑p * X ^ (p - 1))
rw [coe_expand, derivative_eval₂_C, derivative_pow, C_eq_nat_cast, derivative_X, mul_one]