replace hi : i.succ ≤ n := by simpa [Finset.mem_range] using hi
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)
i : ℕ
hi : i ∈ Finset.range n
⊢ (Nat.choose n (i + 1) * Nat.descFactorial k (i + 1)) • x ^ (k - (i + 1)) • iteratedDeriv (n - (i + 1) + 1) (⇑f) x =
    (Nat.choose n (Nat.succ i) * Nat.descFactorial k (i + 1)) • x ^ (k - (i + 1)) • iteratedDeriv (n - i) (⇑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)
i : ℕ
hi : Nat.succ i ≤ n
⊢ (Nat.choose n (i + 1) * Nat.descFactorial k (i + 1)) • x ^ (k - (i + 1)) • iteratedDeriv (n - (i + 1) + 1) (⇑f) x =
    (Nat.choose n (Nat.succ i) * Nat.descFactorial k (i + 1)) • x ^ (k - (i + 1)) • iteratedDeriv (n - i) (⇑f) x