rw [← mul_assoc]
case succ.h
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n i : ℕ
IH : (iteratedDeriv i fun x => x ^ n) = fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)
x : 𝕜
⊢ ↑(Nat.descFactorial n i) * (↑(n - i) * x ^ (n - i - 1)) = ↑(Nat.descFactorial n (Nat.succ i)) * x ^ (n - Nat.succ i)
case succ.h
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n i : ℕ
IH : (iteratedDeriv i fun x => x ^ n) = fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)
x : 𝕜
⊢ ↑(Nat.descFactorial n i) * ↑(n - i) * x ^ (n - i - 1) = ↑(Nat.descFactorial n (Nat.succ i)) * x ^ (n - Nat.succ i)