have : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b) :=
  by
  refine'
    (hf.differentiable_on_iterated_deriv_within _ (uniqueDiffOn_Icc hab)).mono Ioo_subset_Icc_self
  rw [← Nat.cast_add_one, Nat.cast_lt]
  exact Nat.lt_succ_self _
case inr
f : ℝ → ℝ
a b C x x₀ : ℝ
n : ℕ
hab✝ : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hC : ∀ y ∈ Ioo a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
hab : a < b
⊢ ‖f x - taylorWithinEval f n (Icc a b) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1) / ↑(n + 1)!
case inr
f : ℝ → ℝ
a b C x x₀ : ℝ
n : ℕ
hab✝ : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hC : ∀ y ∈ Ioo a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
hab : a < b
this : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
⊢ ‖f x - taylorWithinEval f n (Icc a b) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1) / ↑(n + 1)!