rw [taylorWithinEval_self, sub_self, sub_self, abs_zero, zero_pow Nat.succ_pos',
  MulZeroClass.mul_zero, zero_div, norm_zero]
case inl
f : ℝ → ℝ
C x : ℝ
n : ℕ
hab : x ≤ x
hf : ContDiffOn ℝ (↑n + 1) f (Icc x x)
hC : ∀ y ∈ Ioo x x, ‖iteratedDerivWithin (n + 1) f (Icc x x) y‖ ≤ C
⊢ ‖f x - taylorWithinEval f n (Icc x x) x x‖ ≤ C * |x - x| ^ (n + 1) / ↑(n + 1)!
no goals