no goals
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
n k : ℕ
f : R[X]
⊢ (↑derivative^[k]) (↑n * f) = ↑n * (↑derivative^[k]) f
induction' k with k ih generalizing f <;> simp [*]