no goals
E : Type ?u.415583
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.415679
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'_nonneg : ∀ (x : ℝ), x ∈ interior D → 0 ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
⊢ f x ≤ f y
simpa only [zero_mul, sub_nonneg] using
  hD.mul_sub_le_image_sub_of_le_deriv hf hf' hf'_nonneg x hx y hy hxy