simp only [Nat.choose_succ_succ]
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) • iteratedDeriv (n - x_1 + 1) (⇑f) x +
      ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) •
          (↑(k - x_1) * x ^ (k - Nat.succ x_1)) • iteratedDeriv (n - x_1) (⇑f) x =
    ∑ k_1 in Finset.range (Nat.succ n),
        (Nat.choose (Nat.succ n) (k_1 + 1) * Nat.descFactorial k (k_1 + 1)) •
          x ^ (k - (k_1 + 1)) • iteratedDeriv (Nat.succ n - (k_1 + 1)) (⇑f) x +
      (Nat.choose (Nat.succ n) 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (Nat.succ n - 0) (⇑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) • iteratedDeriv (n - x_1 + 1) (⇑f) x +
      ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) •
          (↑(k - x_1) * x ^ (k - Nat.succ x_1)) • iteratedDeriv (n - x_1) (⇑f) x =
    ∑ x_1 in Finset.range (Nat.succ n),
        ((Nat.choose n x_1 + Nat.choose n (Nat.succ x_1)) * Nat.descFactorial k (x_1 + 1)) •
          x ^ (k - (x_1 + 1)) • iteratedDeriv (Nat.succ n - (x_1 + 1)) (⇑f) x +
      (Nat.choose (Nat.succ n) 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (Nat.succ n - 0) (⇑f) x