-- Mathlib/Analysis/Calculus/Taylor.lean
theorem hasDerivWithinAt_taylorWithinEval {f : ℝ → E} {x y : ℝ} {n : ℕ} {s s' : Set ℝ}
    (hs_unique : UniqueDiffOn ℝ s) (hs' : s' ∈ 𝓝[s] y)
    (hy : y ∈ s') (h : s' ⊆ s) (hf : ContDiffOn ℝ n f s)
    (hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin n f s) s y) :
    HasDerivWithinAt (fun t => taylorWithinEval f n s t x)
      (((n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f s y) s' y

Proof state:
case succ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
s s' : Set ℝ
hs_unique : UniqueDiffOn ℝ s
hs' : s' ∈ 𝓝[s] y
hy : y ∈ s'
h : s' ⊆ s
hs'_unique : UniqueDiffWithinAt ℝ s' y
k : ℕ
hk :
  ContDiffOn ℝ (↑k) f s →
    DifferentiableWithinAt ℝ (iteratedDerivWithin k f s) s y →
      HasDerivWithinAt (fun t => taylorWithinEval f k s t x)
        (((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y) s' y
hf : ContDiffOn ℝ (↑(k + 1)) f s
hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y
⊢ HasDerivWithinAt
    (fun t =>
      taylorWithinEval f k s t x + (((↑k + 1) * ↑k !)⁻¹ * (x - t) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s t)
    (((↑(k + 0).succ !)⁻¹ * (x - y) ^ (k + 0).succ) • iteratedDerivWithin ((k + 0).succ + 0).succ f s y) s' y

Tactic:
simp only [add_zero, Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one]

Result:
case succ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
s s' : Set ℝ
hs_unique : UniqueDiffOn ℝ s
hs' : s' ∈ 𝓝[s] y
hy : y ∈ s'
h : s' ⊆ s
hs'_unique : UniqueDiffWithinAt ℝ s' y
k : ℕ
hk :
  ContDiffOn ℝ (↑k) f s →
    DifferentiableWithinAt ℝ (iteratedDerivWithin k f s) s y →
      HasDerivWithinAt (fun t => taylorWithinEval f k s t x)
        (((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y) s' y
hf : ContDiffOn ℝ (↑(k + 1)) f s
hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y
⊢ HasDerivWithinAt
    (fun t =>
      taylorWithinEval f k s t x + (((↑k + 1) * ↑k !)⁻¹ * (x - t) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s t)
    ((((↑k + 1) * ↑k !)⁻¹ * (x - y) ^ k.succ) • iteratedDerivWithin k.succ.succ f s y) s' y

Proof state:
case succ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
s s' : Set ℝ
hs_unique : UniqueDiffOn ℝ s
hs' : s' ∈ 𝓝[s] y
hy : y ∈ s'
h : s' ⊆ s
hs'_unique : UniqueDiffWithinAt ℝ s' y
k : ℕ
hf : ContDiffOn ℝ (↑(k + 1)) f s
hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y
coe_lt_succ : ↑k < ↑k.succ
hdiff : DifferentiableOn ℝ (iteratedDerivWithin k f s) s'
hk :
  HasDerivWithinAt (fun t => taylorWithinEval f k s t x) (((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y)
    s' y
⊢ HasDerivWithinAt
    (fun t =>
      taylorWithinEval f k s t x + (((↑k + 1) * ↑k !)⁻¹ * (x - t) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s t)
    ((((↑k + 1) * ↑k !)⁻¹ * (x - y) ^ k.succ) • iteratedDerivWithin k.succ.succ f s y) s' y

Tactic:
convert hk.add (hasDerivWithinAt_taylor_coeff_within hs'_unique
  (nhdsWithin_mono _ h self_mem_nhdsWithin) hf') using 1

Result:
case h.e'_9
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
s s' : Set ℝ
hs_unique : UniqueDiffOn ℝ s
hs' : s' ∈ 𝓝[s] y
hy : y ∈ s'
h : s' ⊆ s
hs'_unique : UniqueDiffWithinAt ℝ s' y
k : ℕ
hf : ContDiffOn ℝ (↑(k + 1)) f s
hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y
coe_lt_succ : ↑k < ↑k.succ
hdiff : DifferentiableOn ℝ (iteratedDerivWithin k f s) s'
hk :
  HasDerivWithinAt (fun t => taylorWithinEval f k s t x) (((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y)
    s' y
⊢ (((↑k + 1) * ↑k !)⁻¹ * (x - y) ^ k.succ) • iteratedDerivWithin k.succ.succ f s y =
    ((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y +
      ((((↑k + 1) * ↑k !)⁻¹ * (x - y) ^ (k + 1)) • iteratedDerivWithin (k + 2) f s y -
        ((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y)