simp only [Icc_self, mem_singleton_iff] at hx hx₀
case inl
f : ℝ → ℝ
a C x x₀ : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
hx : x ∈ Icc a a
hx₀ : x₀ ∈ Icc a a
hC : ∀ y ∈ Ioo a a, ‖iteratedDerivWithin (n + 1) f (Icc a a) y‖ ≤ C
⊢ ‖f x - taylorWithinEval f n (Icc a a) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1) / ↑(n + 1)!
case inl
f : ℝ → ℝ
a C x x₀ : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
hC : ∀ y ∈ Ioo a a, ‖iteratedDerivWithin (n + 1) f (Icc a a) y‖ ≤ C
hx : x = a
hx₀ : x₀ = a
⊢ ‖f x - taylorWithinEval f n (Icc a a) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1) / ↑(n + 1)!