rw [uIoo_of_ge hx₀.le] at g'_ne gdiff hf' ⊢
case inr
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (Icc x x₀)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x x₀)) (uIoo x₀ x)
gcont : ContinuousOn g (Icc x x₀)
gdiff : ∀ x_1 ∈ uIoo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ uIoo x₀ x, g' x_1 ≠ 0
hx₀ : x < x₀
⊢ ∃ x',
    ∃ (_ : x' ∈ uIoo x₀ x),
      f x - taylorWithinEval f n (Icc x x₀) x₀ x =
        ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (Icc x x₀) x'
case inr
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (Icc x x₀)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x x₀)) (Ioo x x₀)
gcont : ContinuousOn g (Icc x x₀)
gdiff : ∀ x_1 ∈ Ioo x x₀, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x x₀, g' x_1 ≠ 0
hx₀ : x < x₀
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo x x₀),
      f x - taylorWithinEval f n (Icc x x₀) x₀ x =
        ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (Icc x x₀) x'