rw [Icc_self, mem_singleton_iff] at hx hx₀
case inl
f : ℝ → ℝ
a x₀ : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
hx₀ : x₀ ∈ Icc a a
x : ℝ
hx : x ∈ Icc a a
⊢ ‖f x - taylorWithinEval f n (Icc a a) x₀ x‖ ≤ 0 * |x - x₀| ^ (n + 1)
case inl
f : ℝ → ℝ
a x₀ : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
hx₀ : x₀ = a
x : ℝ
hx : x = a
⊢ ‖f x - taylorWithinEval f n (Icc a a) x₀ x‖ ≤ 0 * |x - x₀| ^ (n + 1)