-- Mathlib/Analysis/Convex/Deriv.lean
lemma hasDerivWithinAt_sSup_slope_of_mem_interior (hfc : ConvexOn ℝ S f) (hxs : x ∈ interior S) :
    HasDerivWithinAt f (sSup (slope f x '' {y ∈ S | y < x})) (Iio x) x

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
⊢ Tendsto (slope f x) (𝓝[<] x) (𝓝 (sSup (slope f x '' {y | y ∈ S ∧ y < x})))

Tactic:
have h : Ioo a x ⊆ {y | y ∈ S ∧ y < x} := fun z hz ↦ ⟨habs ⟨hz.1, hz.2.trans hxab.2⟩, hz.2⟩

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
h : Ioo a x ⊆ {y | y ∈ S ∧ y < x}
⊢ Tendsto (slope f x) (𝓝[<] x) (𝓝 (sSup (slope f x '' {y | y ∈ S ∧ y < x})))

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
h : Ioo a x ⊆ {y | y ∈ S ∧ y < x}
h_Ioo : Tendsto (slope f x) (𝓝[<] x) (𝓝 (sSup (slope f x '' Ioo a x)))
y : ℝ
hyS : y ∈ S
hyx : y < x
z : ℝ
hyz : a ⊔ y < z
hzx : z < x
⊢ ∃ x_1 ∈ Ioo a x, y ≤ x_1

Tactic:
exact ⟨z, ⟨(le_max_left _ _).trans_lt hyz, hzx⟩, (le_max_right _ _).trans hyz.le⟩

Result:
no goals

Proof state:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
h : Ioo a x ⊆ {y | y ∈ S ∧ y < x}
h_Ioo : Tendsto (slope f x) (𝓝[<] x) (𝓝 (sSup (slope f x '' Ioo a x)))
⊢ ∀ y ∈ {y | y ∈ S ∧ y < x}, ∃ x_1 ∈ Ioo a x, y ≤ x_1

Tactic:
rintro y ⟨hyS, hyx⟩

Result:
case 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
h : Ioo a x ⊆ {y | y ∈ S ∧ y < x}
h_Ioo : Tendsto (slope f x) (𝓝[<] x) (𝓝 (sSup (slope f x '' Ioo a x)))
y : ℝ
hyS : y ∈ S
hyx : y < x
⊢ ∃ x_1 ∈ Ioo a x, y ≤ x_1

Proof state:
case 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
h : Ioo a x ⊆ {y | y ∈ S ∧ y < x}
h_Ioo : Tendsto (slope f x) (𝓝[<] x) (𝓝 (sSup (slope f x '' Ioo a x)))
y : ℝ
hyS : y ∈ S
hyx : y < x
⊢ ∃ x_1 ∈ Ioo a x, y ≤ x_1

Tactic:
obtain ⟨z, hyz, hzx⟩ := exists_between (max_lt hxab.1 hyx)

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
h : Ioo a x ⊆ {y | y ∈ S ∧ y < x}
h_Ioo : Tendsto (slope f x) (𝓝[<] x) (𝓝 (sSup (slope f x '' Ioo a x)))
y : ℝ
hyS : y ∈ S
hyx : y < x
z : ℝ
hyz : a ⊔ y < z
hzx : z < x
⊢ ∃ x_1 ∈ Ioo a x, y ≤ x_1

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
h : Ioo a x ⊆ {y | y ∈ S ∧ y < x}
h_Ioo : Tendsto (slope f x) (𝓝[<] x) (𝓝 (sSup (slope f x '' Ioo a x)))
⊢ Tendsto (slope f x) (𝓝[<] x) (𝓝 (sSup (slope f x '' {y | y ∈ S ∧ y < x})))

Tactic:
suffices sSup (slope f x '' Ioo a x) = sSup (slope f x '' {y ∈ S | y < x}) by rwa [← this]

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
h : Ioo a x ⊆ {y | y ∈ S ∧ y < x}
h_Ioo : Tendsto (slope f x) (𝓝[<] x) (𝓝 (sSup (slope f x '' Ioo a x)))
⊢ sSup (slope f x '' Ioo a x) = sSup (slope f x '' {y | y ∈ S ∧ y < x})

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
h : Ioo a x ⊆ {y | y ∈ S ∧ y < x}
⊢ Tendsto (slope f x) (𝓝[<] x) (𝓝 (sSup (slope f x '' {y | y ∈ S ∧ y < x})))

Tactic:
have h_Ioo : Tendsto (slope f x) (𝓝[<] x) (𝓝 (sSup (slope f x '' Ioo a x))) :=
  ((monotoneOn_slope_lt hfc (habs hxab)).mono h).tendsto_nhdsWithin_Ioo_left
    (by simpa using hxab.1) ((bddAbove_slope_gt_of_mem_interior hfc hxs).mono (image_subset _ h))

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
h : Ioo a x ⊆ {y | y ∈ S ∧ y < x}
h_Ioo : Tendsto (slope f x) (𝓝[<] x) (𝓝 (sSup (slope f x '' Ioo a x)))
⊢ Tendsto (slope f x) (𝓝[<] x) (𝓝 (sSup (slope f x '' {y | y ∈ S ∧ y < x})))

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
h : Ioo a x ⊆ {y | y ∈ S ∧ y < x}
h_Ioo : Tendsto (slope f x) (𝓝[<] x) (𝓝 (sSup (slope f x '' Ioo a x)))
⊢ sSup (slope f x '' Ioo a x) = sSup (slope f x '' {y | y ∈ S ∧ y < x})

Tactic:
apply (monotoneOn_slope_lt hfc (habs hxab)).csSup_eq_of_subset_of_forall_exists_le
  (bddAbove_slope_gt_of_mem_interior hfc hxs) h ?_

Result:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
h : Ioo a x ⊆ {y | y ∈ S ∧ y < x}
h_Ioo : Tendsto (slope f x) (𝓝[<] x) (𝓝 (sSup (slope f x '' Ioo a x)))
⊢ ∀ y ∈ {y | y ∈ S ∧ y < x}, ∃ x_1 ∈ Ioo a x, y ≤ x_1

Proof state:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
⊢ HasDerivWithinAt f (sSup (slope f x '' {y | y ∈ S ∧ y < x})) (Iio x) x

Tactic:
have hxs' := hxs

Result:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs hxs' : x ∈ interior S
⊢ HasDerivWithinAt f (sSup (slope f x '' {y | y ∈ S ∧ y < x})) (Iio x) x

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
⊢ Tendsto (slope f x) (𝓝[Iio x \ {x}] x) (𝓝 (sSup (slope f x '' {y | y ∈ S ∧ y < x})))

Tactic:
simp only [mem_Iio, lt_self_iff_false, not_false_eq_true, diff_singleton_eq_self]

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
⊢ Tendsto (slope f x) (𝓝[<] x) (𝓝 (sSup (slope f x '' {y | y ∈ S ∧ y < x})))

Proof state:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
h : Ioo a x ⊆ {y | y ∈ S ∧ y < x}
h_Ioo : Tendsto (slope f x) (𝓝[<] x) (𝓝 (sSup (slope f x '' Ioo a x)))
this : sSup (slope f x '' Ioo a x) = sSup (slope f x '' {y | y ∈ S ∧ y < x})
⊢ Tendsto (slope f x) (𝓝[<] x) (𝓝 (sSup (slope f x '' {y | y ∈ S ∧ y < x})))

Tactic:
rwa [← this]

Result:
no goals

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
⊢ HasDerivWithinAt f (sSup (slope f x '' {y | y ∈ S ∧ y < x})) (Iio 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
⊢ HasDerivWithinAt f (sSup (slope f x '' {y | y ∈ S ∧ y < x})) (Iio x) x

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

Tactic:
simpa using hxab.1

Result:
no goals

Proof state:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs hxs' : x ∈ interior S
⊢ HasDerivWithinAt f (sSup (slope f x '' {y | y ∈ S ∧ y < x})) (Iio 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
⊢ HasDerivWithinAt f (sSup (slope f x '' {y | y ∈ S ∧ y < x})) (Iio x) x

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
⊢ HasDerivWithinAt f (sSup (slope f x '' {y | y ∈ S ∧ y < x})) (Iio x) x

Tactic:
simp_rw [hasDerivWithinAt_iff_tendsto_slope]

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
⊢ Tendsto (slope f x) (𝓝[Iio x \ {x}] x) (𝓝 (sSup (slope f x '' {y | y ∈ S ∧ y < x})))