rw [hx₀, hx, taylorWithinEval_self, sub_self, MulZeroClass.zero_mul, norm_zero]
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)
no goals