have gcont : ContinuousOn (fun t : ℝ => (x - t) ^ (n + 1)) (Icc a b) := by
  refine' Continuous.continuousOn _; continuity
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      f x - taylorWithinEval f n (Icc a b) x₀ x =
        iteratedDerivWithin (n + 1) f (Icc a b) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc a b)
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      f x - taylorWithinEval f n (Icc a b) x₀ x =
        iteratedDerivWithin (n + 1) f (Icc a b) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!