E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
F : Type ?u.244965
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
𝕜 : Type u_2
G : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → G
C : ℝ
s : Set E
x y : E
f' g' : E → E →L[𝕜] G
φ : E →L[𝕜] G
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hf' : ∀ (x : E), x ∈ s → fderivWithin 𝕜 f s x = 0
hx : x ∈ s
hy : y ∈ s
bound : ∀ (x : E), x ∈ s → ‖fderivWithin 𝕜 f s x‖ ≤ 0
⊢ f x = f y
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
F : Type ?u.244965
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
𝕜 : Type u_2
G : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → G
C : ℝ
s : Set E
x y : E
f' g' : E → E →L[𝕜] G
φ : E →L[𝕜] G
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hf' : ∀ (x : E), x ∈ s → fderivWithin 𝕜 f s x = 0
hx : x ∈ s
hy : y ∈ s
⊢ f x = f y
have bound : ∀ x ∈ s, ‖fderivWithin 𝕜 f s x‖ ≤ 0 := fun x hx => by
  simp only [hf' x hx, norm_zero, le_rfl]
no goals
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
F : Type ?u.244965
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
𝕜 : Type u_2
G : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → G
C : ℝ
s : Set E
x y : E
f' g' : E → E →L[𝕜] G
φ : E →L[𝕜] G
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hf' : ∀ (x : E), x ∈ s → fderivWithin 𝕜 f s x = 0
hx : x ∈ s
hy : y ∈ s
bound : ∀ (x : E), x ∈ s → ‖fderivWithin 𝕜 f s x‖ ≤ 0
⊢ f x = f y
simpa only [(dist_eq_norm _ _).symm, zero_mul, dist_le_zero, eq_comm] using
  hs.norm_image_sub_le_of_norm_fderivWithin_le hf bound hx hy
no goals
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
F : Type ?u.244965
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
𝕜 : Type u_2
G : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → G
C : ℝ
s : Set E
x✝ y : E
f' g' : E → E →L[𝕜] G
φ : E →L[𝕜] G
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hf' : ∀ (x : E), x ∈ s → fderivWithin 𝕜 f s x = 0
hx✝ : x✝ ∈ s
hy : y ∈ s
x : E
hx : x ∈ s
⊢ ‖fderivWithin 𝕜 f s x‖ ≤ 0
simp only [hf' x hx, norm_zero, le_rfl]