have hg' : ∀ y : ℝ, y ∈ uIoo x₀ x → -(↑n + 1) * (x - y) ^ n ≠ 0 := fun y hy =>
  mul_ne_zero (neg_ne_zero.mpr (Nat.cast_add_one_ne_zero n)) (xy_ne y hy)
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
⊢ ∃ x',
    ∃ (_ : x' ∈ uIoo x₀ x),
      f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
        iteratedDerivWithin (n + 1) f (uIcc x₀ x) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
⊢ ∃ x',
    ∃ (_ : x' ∈ uIoo x₀ x),
      f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
        iteratedDerivWithin (n + 1) f (uIcc x₀ x) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!