substs hx₀ hx
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)!
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)!