no goals
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
n k : ℕ
⊢ (↑derivative^[k]) (X ^ n) = ↑C ↑(Nat.descFactorial n k) * X ^ (n - k)
rw [iterate_derivative_X_pow_eq_nat_cast_mul n k, C_eq_nat_cast]