-- Mathlib/Analysis/Convex/Deriv.lean
lemma hasDerivWithinAt_sInf_slope_of_mem_interior (hfc : ConvexOn ℝ S f) (hxs : x ∈ interior S) :
    HasDerivWithinAt f (sInf (slope f x '' {y ∈ S | x < y})) (Ioi 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
h : Ioo x b ⊆ {y | y ∈ S ∧ x < y}
h_Ioo : Tendsto (slope f x) (𝓝[>] x) (𝓝 (sInf (slope f x '' Ioo x b)))
y : ℝ
hyS : y ∈ S
hxy : x < y
z : ℝ
hxz : x < z
hzy : z < b ⊓ y
⊢ ∃ x_1 ∈ Ioo x b, x_1 ≤ y

Tactic:
exact ⟨z, ⟨hxz, hzy.trans_le (min_le_left _ _)⟩, hzy.le.trans (min_le_right _ _)⟩

Result:
no goals

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

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

Tactic:
have hxs' := hxs

Result:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs hxs' : x ∈ interior S
⊢ HasDerivWithinAt f (sInf (slope f x '' {y | y ∈ S ∧ x < y})) (Ioi 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
h : Ioo x b ⊆ {y | y ∈ S ∧ x < y}
h_Ioo : Tendsto (slope f x) (𝓝[>] x) (𝓝 (sInf (slope f x '' Ioo x b)))
⊢ Tendsto (slope f x) (𝓝[>] x) (𝓝 (sInf (slope f x '' {y | y ∈ S ∧ x < y})))

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

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 x b ⊆ {y | y ∈ S ∧ x < y}
⊢ (Ioo x b).Nonempty

Tactic:
simpa using hxab.2

Result:
no goals

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

Tactic:
apply (monotoneOn_slope_gt hfc (habs hxab)).csInf_eq_of_subset_of_forall_exists_le
  (bddBelow_slope_lt_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 x b ⊆ {y | y ∈ S ∧ x < y}
h_Ioo : Tendsto (slope f x) (𝓝[>] x) (𝓝 (sInf (slope f x '' Ioo x b)))
⊢ ∀ y ∈ {y | y ∈ S ∧ x < y}, ∃ x_1 ∈ Ioo x b, x_1 ≤ 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
⊢ HasDerivWithinAt f (sInf (slope f x '' {y | y ∈ S ∧ x < y})) (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
⊢ HasDerivWithinAt f (sInf (slope f x '' {y | y ∈ S ∧ x < y})) (Ioi 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) (𝓝[Ioi x \ {x}] x) (𝓝 (sInf (slope f x '' {y | y ∈ S ∧ x < y})))

Tactic:
simp only [mem_Ioi, 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) (𝓝 (sInf (slope f x '' {y | y ∈ S ∧ x < y})))

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 x b ⊆ {y | y ∈ S ∧ x < y}
h_Ioo : Tendsto (slope f x) (𝓝[>] x) (𝓝 (sInf (slope f x '' Ioo x b)))
y : ℝ
hyS : y ∈ S
hxy : x < y
⊢ ∃ x_1 ∈ Ioo x b, x_1 ≤ y

Tactic:
obtain ⟨z, hxz, hzy⟩ := exists_between (lt_min hxab.2 hxy)

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 x b ⊆ {y | y ∈ S ∧ x < y}
h_Ioo : Tendsto (slope f x) (𝓝[>] x) (𝓝 (sInf (slope f x '' Ioo x b)))
y : ℝ
hyS : y ∈ S
hxy : x < y
z : ℝ
hxz : x < z
hzy : z < b ⊓ y
⊢ ∃ x_1 ∈ Ioo x b, x_1 ≤ y

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

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

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

Proof state:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs hxs' : x ∈ interior S
⊢ HasDerivWithinAt f (sInf (slope f x '' {y | y ∈ S ∧ x < y})) (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
⊢ HasDerivWithinAt f (sInf (slope f x '' {y | y ∈ S ∧ x < y})) (Ioi 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
h : Ioo x b ⊆ {y | y ∈ S ∧ x < y}
⊢ Tendsto (slope f x) (𝓝[>] x) (𝓝 (sInf (slope f x '' {y | y ∈ S ∧ x < y})))

Tactic:
have h_Ioo : Tendsto (slope f x) (𝓝[>] x) (𝓝 (sInf (slope f x '' Ioo x b))) :=
  ((monotoneOn_slope_gt hfc (habs hxab)).mono h).tendsto_nhdsWithin_Ioo_right
    (by simpa using hxab.2) ((bddBelow_slope_lt_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 x b ⊆ {y | y ∈ S ∧ x < y}
h_Ioo : Tendsto (slope f x) (𝓝[>] x) (𝓝 (sInf (slope f x '' Ioo x b)))
⊢ Tendsto (slope f x) (𝓝[>] x) (𝓝 (sInf (slope f x '' {y | y ∈ S ∧ x < y})))

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

Tactic:
rwa [← this]

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 x b ⊆ {y | y ∈ S ∧ x < y}
h_Ioo : Tendsto (slope f x) (𝓝[>] x) (𝓝 (sInf (slope f x '' Ioo x b)))
⊢ ∀ y ∈ {y | y ∈ S ∧ x < y}, ∃ x_1 ∈ Ioo x b, x_1 ≤ y

Tactic:
rintro y ⟨hyS, hxy⟩

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 x b ⊆ {y | y ∈ S ∧ x < y}
h_Ioo : Tendsto (slope f x) (𝓝[>] x) (𝓝 (sInf (slope f x '' Ioo x b)))
y : ℝ
hyS : y ∈ S
hxy : x < y
⊢ ∃ x_1 ∈ Ioo x b, x_1 ≤ y