rw [← nsmul_eq_mul, smul_assoc, smul_smul]
case succ.h.refine_1
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
i : ℕ
a✝ : i ∈ Finset.range (Nat.succ n)
⊢ (Nat.choose n i * Nat.descFactorial k i) • (↑(k - i) * x ^ (k - Nat.succ i)) • iteratedDeriv (n - i) (⇑f) x =
    (Nat.choose n i * Nat.descFactorial k (i + 1)) • x ^ (k - (i + 1)) • iteratedDeriv (n - i) (⇑f) x
case succ.h.refine_1
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
i : ℕ
a✝ : i ∈ Finset.range (Nat.succ n)
⊢ (Nat.choose n i * Nat.descFactorial k i * (k - i)) • x ^ (k - Nat.succ i) • iteratedDeriv (n - i) (⇑f) x =
    (Nat.choose n i * Nat.descFactorial k (i + 1)) • x ^ (k - (i + 1)) • iteratedDeriv (n - i) (⇑f) x