-- Mathlib/Analysis/Convex/Deriv.lean
lemma monotoneOn_leftDeriv (hfc : ConvexOn ℝ S f) :
    MonotoneOn (fun x ↦ derivWithin f (Iio x) x) (interior S)

Proof state:
case inl
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs hys : x ∈ interior S
hxy : x ≤ x
⊢ (fun x => derivWithin f (Iio x) x) x ≤ (fun x => derivWithin f (Iio x) x) x

Tactic:
rfl

Result:
no goals

Proof state:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
⊢ MonotoneOn (fun x => derivWithin f (Iio x) x) (interior S)

Tactic:
intro x hxs y hys hxy

Result:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy : x ≤ y
⊢ (fun x => derivWithin f (Iio x) x) x ≤ (fun x => derivWithin f (Iio x) x) y

Proof state:
case inr.refine_1.intro.intro.intro.intro.intro
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
z : ℝ
hxz : a < z
hzb : z < x
⊢ {y | y ∈ S ∧ y < x}.Nonempty

Tactic:
exact ⟨z, habs ⟨hxz, hzb.trans hxab.2⟩, hzb⟩

Result:
no goals

Proof state:
case inr.refine_2
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ ∀ b ∈ slope f x '' {y | y ∈ S ∧ y < x}, b ≤ slope f x y

Tactic:
rintro _ ⟨z, ⟨hzs, hyz : z < x⟩, rfl⟩

Result:
case inr.refine_2.intro.intro.intro
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
z : ℝ
hzs : z ∈ S
hyz : z < x
⊢ slope f x z ≤ slope f x y

Proof state:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy : x ≤ y
⊢ (fun x => derivWithin f (Iio x) x) x ≤ (fun x => derivWithin f (Iio x) x) y

Tactic:
rcases eq_or_lt_of_le hxy with rfl | hxy

Result:
case inl
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs hys : x ∈ interior S
hxy : x ≤ x
⊢ (fun x => derivWithin f (Iio x) x) x ≤ (fun x => derivWithin f (Iio x) x) x

case inr
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ (fun x => derivWithin f (Iio x) x) x ≤ (fun x => derivWithin f (Iio x) x) y

Proof state:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ x ∈ S

Tactic:
exact interior_subset hxs

Result:
no goals

Proof state:
case inr.refine_2.intro.intro.intro
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
z : ℝ
hzs : z ∈ S
hyz : z < x
⊢ slope f x z ≤ slope f x y

Tactic:
exact slope_mono hfc (interior_subset hxs) ⟨hzs, hyz.ne⟩ ⟨interior_subset hys, hxy.ne'⟩
  (hyz.trans hxy).le

Result:
no goals

Proof state:
case inr
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ sSup (slope f x '' {y | y ∈ S ∧ y < x}) ≤ sSup (slope f y '' {y_1 | y_1 ∈ S ∧ y_1 < y})

Tactic:
refine le_csSup_of_le (b := slope f x y) (bddAbove_slope_gt_of_mem_interior hfc hys)
  ⟨x, by simp only [slope_comm, mem_setOf_eq, hxy, and_true]; exact interior_subset hxs⟩
  (csSup_le ?_ ?_)

Result:
case inr.refine_1
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ (slope f x '' {y | y ∈ S ∧ y < x}).Nonempty

case inr.refine_2
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ ∀ b ∈ slope f x '' {y | y ∈ S ∧ y < x}, b ≤ slope f x y

Proof state:
case inr
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ (fun x => derivWithin f (Iio x) x) x ≤ (fun x => derivWithin f (Iio x) x) y

Tactic:
simp_rw [hfc.leftDeriv_eq_sSup_slope_of_mem_interior hxs,
  hfc.leftDeriv_eq_sSup_slope_of_mem_interior hys]

Result:
case inr
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ sSup (slope f x '' {y | y ∈ S ∧ y < x}) ≤ sSup (slope f y '' {y_1 | y_1 ∈ S ∧ y_1 < y})

Proof state:
case inr.refine_1.intro.intro.intro
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
⊢ {y | y ∈ S ∧ y < x}.Nonempty

Tactic:
obtain ⟨z, hxz, hzb⟩ := exists_between hxab.1

Result:
case inr.refine_1.intro.intro.intro.intro.intro
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
z : ℝ
hxz : a < z
hzb : z < x
⊢ {y | y ∈ S ∧ y < x}.Nonempty

Proof state:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ x ∈ {y_1 | y_1 ∈ S ∧ y_1 < y} ∧ slope f y x = slope f x y

Tactic:
simp only [slope_comm, mem_setOf_eq, hxy, and_true]

Result:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ x ∈ S

Proof state:
case inr.refine_1
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ (slope f x '' {y | y ∈ S ∧ y < x}).Nonempty

Tactic:
have hxs' := hxs

Result:
case inr.refine_1
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
hxs' : x ∈ interior S
⊢ (slope f x '' {y | y ∈ S ∧ y < x}).Nonempty

Proof state:
case inr.refine_1.intro.intro.intro
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
⊢ (slope f x '' {y | y ∈ S ∧ y < x}).Nonempty

Tactic:
rw [image_nonempty]

Result:
case inr.refine_1.intro.intro.intro
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
⊢ {y | y ∈ S ∧ y < x}.Nonempty

Proof state:
case inr.refine_1
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
hxs' : ∃ l u, x ∈ Ioo l u ∧ Ioo l u ⊆ S
⊢ (slope f x '' {y | y ∈ S ∧ y < x}).Nonempty

Tactic:
obtain ⟨a, b, hxab, habs⟩ := hxs'

Result:
case inr.refine_1.intro.intro.intro
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
⊢ (slope f x '' {y | y ∈ S ∧ y < x}).Nonempty

Proof state:
case inr.refine_1
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
hxs' : x ∈ interior S
⊢ (slope f x '' {y | y ∈ S ∧ y < x}).Nonempty

Tactic:
rw [mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset] at hxs'

Result:
case inr.refine_1
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
hxs' : ∃ l u, x ∈ Ioo l u ∧ Ioo l u ⊆ S
⊢ (slope f x '' {y | y ∈ S ∧ y < x}).Nonempty