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