simp only [smul_smul]
case succ.h
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 : ℝ
⊢ deriv
      (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 =
    ∑ i in Finset.range (Nat.succ (Nat.succ n)),
      Nat.choose (Nat.succ n) i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (Nat.succ n - i) (⇑f) x
case succ.h
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 : ℝ
⊢ deriv
      (fun x =>
        ∑ x_1 in Finset.range (Nat.succ n),
          (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (n - x_1) (⇑f) x)
      x =
    ∑ x_1 in Finset.range (Nat.succ (Nat.succ n)),
      (Nat.choose (Nat.succ n) x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (Nat.succ n - x_1) (⇑f) x