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

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 : y ∈ Ioo a b
habs : Ioo a b ⊆ S
⊢ {y_1 | y_1 ∈ S ∧ y < y_1}.Nonempty

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

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 : y ∈ Ioo a b
habs : Ioo a b ⊆ S
z : ℝ
hxz : y < z
hzb : z < b
⊢ {y_1 | y_1 ∈ S ∧ y < y_1}.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
⊢ (slope f y '' {y_1 | y_1 ∈ S ∧ y < y_1}).Nonempty

Tactic:
have hys' := hys

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
hys' : y ∈ interior S
⊢ (slope f y '' {y_1 | y_1 ∈ S ∧ y < y_1}).Nonempty

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 : y ∈ Ioo a b
habs : Ioo a b ⊆ S
z : ℝ
hxz : y < z
hzb : z < b
⊢ {y_1 | y_1 ∈ S ∧ y < y_1}.Nonempty

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

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 : y < z
⊢ slope f x y ≤ slope f y z

Tactic:
rw [slope_comm]

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 : y < z
⊢ slope f y x ≤ slope f y z

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 : y < z
⊢ slope f y x ≤ slope f y z

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

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 y '' {y_1 | y_1 ∈ S ∧ y < y_1}, slope f x y ≤ b

Tactic:
rintro _ ⟨z, ⟨hzs, hyz : y < z⟩, 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 : y < z
⊢ slope f x y ≤ slope f y z

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
⊢ sInf (slope f x '' {y | y ∈ S ∧ x < y}) ≤ sInf (slope f y '' {y_1 | y_1 ∈ S ∧ y < y_1})

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

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 y '' {y_1 | y_1 ∈ S ∧ y < y_1}).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 y '' {y_1 | y_1 ∈ S ∧ y < y_1}, slope f x y ≤ b

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
hys' : ∃ l u, y ∈ Ioo l u ∧ Ioo l u ⊆ S
⊢ (slope f y '' {y_1 | y_1 ∈ S ∧ y < y_1}).Nonempty

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

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 : y ∈ Ioo a b
habs : Ioo a b ⊆ S
⊢ (slope f y '' {y_1 | y_1 ∈ S ∧ y < y_1}).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
⊢ y ∈ S

Tactic:
exact interior_subset hys

Result:
no goals

Proof state:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
⊢ MonotoneOn (fun x => derivWithin f (Ioi 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 (Ioi x) x) x ≤ (fun x => derivWithin f (Ioi x) x) y

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
hys' : y ∈ interior S
⊢ (slope f y '' {y_1 | y_1 ∈ S ∧ y < y_1}).Nonempty

Tactic:
rw [mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset] at hys'

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
hys' : ∃ l u, y ∈ Ioo l u ∧ Ioo l u ⊆ S
⊢ (slope f y '' {y_1 | y_1 ∈ S ∧ y < y_1}).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 : y ∈ Ioo a b
habs : Ioo a b ⊆ S
⊢ (slope f y '' {y_1 | y_1 ∈ S ∧ y < y_1}).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 : y ∈ Ioo a b
habs : Ioo a b ⊆ S
⊢ {y_1 | y_1 ∈ S ∧ y < y_1}.Nonempty

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

Tactic:
rfl

Result:
no goals

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 (Ioi x) x) x ≤ (fun x => derivWithin f (Ioi 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 (Ioi x) x) x ≤ (fun x => derivWithin f (Ioi 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 (Ioi x) x) x ≤ (fun x => derivWithin f (Ioi x) 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 (Ioi x) x) x ≤ (fun x => derivWithin f (Ioi x) x) y

Tactic:
simp_rw [hfc.rightDeriv_eq_sInf_slope_of_mem_interior hxs,
  hfc.rightDeriv_eq_sInf_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
⊢ sInf (slope f x '' {y | y ∈ S ∧ x < y}) ≤ sInf (slope f y '' {y_1 | y_1 ∈ S ∧ y < y_1})

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
⊢ y ∈ {y | y ∈ S ∧ x < y} ∧ slope f x y = slope f x y

Tactic:
simp only [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
⊢ y ∈ S