no goals
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.44608
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b C : ℝ
hf : DifferentiableOn ℝ f (Icc 0 1)
bound : ∀ (x : ℝ), x ∈ Ico 0 1 → ‖derivWithin f (Icc 0 1) x‖ ≤ C
⊢ ‖f 1 - f 0‖ ≤ C
simpa only [sub_zero, mul_one] using
  norm_image_sub_le_of_norm_deriv_le_segment hf bound 1 (right_mem_Icc.2 zero_le_one)