E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.39172
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ‖f' x‖ ≤ C
x : ℝ
hx : x ∈ Ico a b
⊢ HasDerivWithinAt (fun x => f x) (f' x) (Ici x) x
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.39172
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ‖f' x‖ ≤ C
⊢ ∀ (x : ℝ), x ∈ Icc a b → ‖f x - f a‖ ≤ C * (x - a)
refine'
  norm_image_sub_le_of_norm_deriv_right_le_segment (fun x hx => (hf x hx).continuousWithinAt)
    (fun x hx => _) bound
no goals
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.39172
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ‖f' x‖ ≤ C
x : ℝ
hx : x ∈ Ico a b
⊢ HasDerivWithinAt (fun x => f x) (f' x) (Ici x) x
exact (hf x <| Ico_subset_Icc_self hx).nhdsWithin (Icc_mem_nhdsWithin_Ici hx)