simp only [Nat.choose_zero_right, Nat.descFactorial_zero, mul_one, Nat.sub_zero, one_smul]
case succ.h.refine_2
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)
⊢ ∑ k_1 in Finset.range n,
        (Nat.choose n (k_1 + 1) * Nat.descFactorial k (k_1 + 1)) •
          x ^ (k - (k_1 + 1)) • iteratedDeriv (n - (k_1 + 1) + 1) (⇑f) x +
      (Nat.choose n 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (n - 0 + 1) (⇑f) x =
    ∑ x_1 in Finset.range n,
        (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
          x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_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.refine_2
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)
⊢ ∑ k_1 in Finset.range n,
        (Nat.choose n (k_1 + 1) * Nat.descFactorial k (k_1 + 1)) •
          x ^ (k - (k_1 + 1)) • iteratedDeriv (n - (k_1 + 1) + 1) (⇑f) x +
      x ^ k • iteratedDeriv (n + 1) (⇑f) x =
    ∑ x_1 in Finset.range n,
        (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
          x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x +
      x ^ k • iteratedDeriv (Nat.succ n) (⇑f) x