no goals
E : Type ?u.418135
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.418231
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ (x : ℝ), x ∈ interior D → deriv f x < 0
x : ℝ
hx : x ∈ D
y : ℝ
⊢ y ∈ D → x < y → f y < f x
simpa only [zero_mul, sub_lt_zero] using
  hD.image_sub_lt_mul_sub_of_deriv_lt hf
    (fun z hz => (differentiableAt_of_deriv_ne_zero (hf' z hz).ne).differentiableWithinAt) hf' x
    hx y