E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.46649
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt f 0 (Ici x) x
this : ∀ (x : ℝ), x ∈ Icc a b → ‖f x - f a‖ ≤ 0 * (x - a)
⊢ ∀ (x : ℝ), x ∈ Icc a b → f x = f a
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.46649
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt f 0 (Ici x) x
⊢ ∀ (x : ℝ), x ∈ Icc a b → f x = f a
have : ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ 0 * (x - a) := fun x hx =>
  norm_image_sub_le_of_norm_deriv_right_le_segment hcont hderiv (fun _ _ => norm_zero.le) x hx
no goals
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.46649
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt f 0 (Ici x) x
this : ∀ (x : ℝ), x ∈ Icc a b → ‖f x - f a‖ ≤ 0 * (x - a)
⊢ ∀ (x : ℝ), x ∈ Icc a b → f x = f a
simpa only [zero_mul, norm_le_zero_iff, sub_eq_zero] using this