rcases eq_or_ne x₀ x with (rfl | hx')
f g g' : ℝ → ℝ
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 g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'
case inl
f g g' : ℝ → ℝ
x₀ a b : ℝ
n : ℕ
hab : 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 g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
hx : x₀ ∈ Icc a b
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x₀ ∧
        (f x₀ - taylorWithinEval f n (Icc a b) x₀ x₀) * g' x' =
          ((x₀ - x') ^ n / ↑n ! * (g x₀ - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'

case inr
f g g' : ℝ → ℝ
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 g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
hx' : x₀ ≠ x
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'