-- Mathlib/Analysis/Convex/Deriv.lean
lemma leftDeriv_le_rightDeriv_of_mem_interior (hfc : ConvexOn ℝ S f) (hxs : x ∈ interior S) :
    derivWithin f (Iio x) x ≤ derivWithin f (Ioi x) x

Proof state:
case intro.intro.intro.refine_2.intro.intro.intro
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
z : ℝ
hzs : z ∈ S
hzx : z < x
⊢ slope f x z ≤ sInf (slope f x '' {y | y ∈ S ∧ x < y})

Tactic:
refine le_csInf ?_ ?_

Result:
case intro.intro.intro.refine_2.intro.intro.intro.refine_1
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
z : ℝ
hzs : z ∈ S
hzx : z < x
⊢ (slope f x '' {y | y ∈ S ∧ x < y}).Nonempty

case intro.intro.intro.refine_2.intro.intro.intro.refine_2
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
z : ℝ
hzs : z ∈ S
hzx : z < x
⊢ ∀ b ∈ slope f x '' {y | y ∈ S ∧ x < y}, slope f x z ≤ b

Proof state:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
⊢ derivWithin f (Iio x) x ≤ derivWithin f (Ioi x) x

Tactic:
have hxs' := hxs

Result:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs hxs' : x ∈ interior S
⊢ derivWithin f (Iio x) x ≤ derivWithin f (Ioi x) x

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

Tactic:
exact ⟨z, habs ⟨haz, hzx.trans hxab.2⟩, hzx⟩

Result:
no goals

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

Tactic:
obtain ⟨z, haz, hzx⟩ := exists_between hxab.1

Result:
case intro.intro.intro.refine_1.intro.intro
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
z : ℝ
haz : a < z
hzx : z < x
⊢ {y | y ∈ S ∧ y < x}.Nonempty

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

Tactic:
rw [image_nonempty]

Result:
case intro.intro.intro.refine_2.intro.intro.intro.refine_1
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
z : ℝ
hzs : z ∈ S
hzx : z < x
⊢ {y | y ∈ S ∧ x < y}.Nonempty

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

Tactic:
refine csSup_le ?_ ?_

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

case intro.intro.intro.refine_2
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
⊢ ∀ b ∈ slope f x '' {y | y ∈ S ∧ y < x}, b ≤ sInf (slope f x '' {y | y ∈ S ∧ x < y})

Proof state:
case intro.intro.intro.refine_1
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
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 intro.intro.intro.refine_1
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
⊢ {y | y ∈ S ∧ y < x}.Nonempty

Proof state:
case intro.intro.intro
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
⊢ derivWithin f (Iio x) x ≤ derivWithin f (Ioi x) x

Tactic:
rw [hfc.rightDeriv_eq_sInf_slope_of_mem_interior hxs,
  hfc.leftDeriv_eq_sSup_slope_of_mem_interior hxs]

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

Proof state:
case intro.intro.intro.refine_2.intro.intro.intro.refine_2
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
z : ℝ
hzs : z ∈ S
hzx : z < x
⊢ ∀ b ∈ slope f x '' {y | y ∈ S ∧ x < y}, slope f x z ≤ b

Tactic:
rintro _ ⟨y, ⟨hys, hxy⟩, rfl⟩

Result:
case intro.intro.intro.refine_2.intro.intro.intro.refine_2.intro.intro.intro
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
z : ℝ
hzs : z ∈ S
hzx : z < x
y : ℝ
hys : y ∈ S
hxy : x < y
⊢ slope f x z ≤ slope f x y

Proof state:
case intro.intro.intro.refine_2.intro.intro.intro.refine_2.intro.intro.intro
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
z : ℝ
hzs : z ∈ S
hzx : z < x
y : ℝ
hys : y ∈ S
hxy : x < y
⊢ slope f x z ≤ slope f x y

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

Result:
no goals

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

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

Result:
no goals

Proof state:
case intro.intro.intro.refine_2
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
⊢ ∀ b ∈ slope f x '' {y | y ∈ S ∧ y < x}, b ≤ sInf (slope f x '' {y | y ∈ S ∧ x < y})

Tactic:
rintro _ ⟨z, ⟨hzs, hzx⟩, rfl⟩

Result:
case intro.intro.intro.refine_2.intro.intro.intro
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
z : ℝ
hzs : z ∈ S
hzx : z < x
⊢ slope f x z ≤ sInf (slope f x '' {y | y ∈ S ∧ x < y})

Proof state:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
hxs' : ∃ l u, x ∈ Ioo l u ∧ Ioo l u ⊆ S
⊢ derivWithin f (Iio x) x ≤ derivWithin f (Ioi x) x

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

Result:
case intro.intro.intro
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
⊢ derivWithin f (Iio x) x ≤ derivWithin f (Ioi x) x

Proof state:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs hxs' : x ∈ interior S
⊢ derivWithin f (Iio x) x ≤ derivWithin f (Ioi x) x

Tactic:
rw [mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset] at hxs'

Result:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
hxs' : ∃ l u, x ∈ Ioo l u ∧ Ioo l u ⊆ S
⊢ derivWithin f (Iio x) x ≤ derivWithin f (Ioi x) x

Proof state:
case intro.intro.intro.refine_2.intro.intro.intro.refine_1
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
z : ℝ
hzs : z ∈ S
hzx : z < x
⊢ {y | y ∈ S ∧ x < y}.Nonempty

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

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