awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ interior s
y : 𝕜
hyx : x < y
hys : y ∈ s
y' : 𝕜
h : y' ∈ slope f x '' {y : 𝕜 | y ∈ s ∧ y < x}
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {y : 𝕜 | y ∈ s ∧ y < x} z
hz' : slope f x z = y'
refine_1 : z ∈ s \ {x}
refine_2 : y ∈ s \ {x}
⊢ slope f x z ≤ slope f x y

Tactic:
refine hfc.slope_mono (interior_subset hxs) ?_ ?_ (hz.2.trans hyx).le

Premises used: interior_subset, LT.lt.le, ConvexOn.slope_mono, And.right, LT.lt.trans
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ interior s
y : 𝕜
hyx : x < y
hys : y ∈ s
y' : 𝕜
h : y' ∈ slope f x '' {y : 𝕜 | y ∈ s ∧ y < x}
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {y : 𝕜 | y ∈ s ∧ y < x} z
hz' : slope f x z = y'
⊢ z ∈ s \ {x}

Tactic:
simp [hz.2.ne, hz.1]

Premises used: And.right, And.left, LT.lt.ne
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ interior s
y : 𝕜
hyx : x < y
hys : y ∈ s
y' : 𝕜
h : y' ∈ slope f x '' {y : 𝕜 | y ∈ s ∧ y < x}
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {y : 𝕜 | y ∈ s ∧ y < x} z
hz' : slope f x z = y'
⊢ y ∈ s \ {x}

Tactic:
simp [hys, hyx.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
⊢ x ∈ interior S

Tactic:
have hxs' := hxs
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs hxs' : x ∈ interior S
⊢ ∃ (l : ℝ) (u : ℝ), x ∈ Ioo l u ∧ Ioo l u ⊆ S

Tactic:
rw [mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset] at hxs'

Premises used: mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
hxs' : ∃ (l : ℝ) (u : ℝ), x ∈ Ioo l u ∧ Ioo l u ⊆ S
obtain :
  ∀ (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
⊢ HasDerivWithinAt f (sInf (slope f x '' {y : ℝ | y ∈ S ∧ x < y})) (Ioi x) x

Tactic:
obtain ⟨a, b, hxab, habs⟩ := hxs'
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
simp_rw : Tendsto (slope f x) (𝓝[Ioi x \ {x}] x) (𝓝 (sInf (slope f x '' {y : ℝ | y ∈ S ∧ x < y})))
⊢ HasDerivWithinAt f (sInf (slope f x '' {y : ℝ | y ∈ S ∧ x < y})) (Ioi x) x

Tactic:
simp_rw [hasDerivWithinAt_iff_tendsto_slope]

Premises used: hasDerivWithinAt_iff_tendsto_slope
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
simp : Tendsto (slope f x) (𝓝[>] x) (𝓝 (sInf (slope f x '' {y : ℝ | y ∈ S ∧ x < y})))
⊢ 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]

Premises used: Set.diff_singleton_eq_self, Set.mem_Ioi, lt_self_iff_false, not_false_eq_true
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
⊢ Ioo x b ⊆ {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⟩
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
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

Premises used: And.right
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
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 '' Ioo x b)))

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_mono h))
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
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})
rwa rwa₁ rwa₂ rwa₃ : 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:
rwa [← this]
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
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)))
suffices : 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:
suffices sInf (slope f x '' Ioo x b) = sInf (slope f x '' {y ∈ S | x < y}) by rwa [← this]
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
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)))
apply : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) {y : ℝ | y ∈ S ∧ x < y} y → ∃ x_1 ∈ Ioo x b, x_1 ≤ y
⊢ 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 ?_

Premises used: MonotoneOn.csInf_eq_of_subset_of_forall_exists_le, bddBelow_slope_lt_of_mem_interior, ConvexOn.monotoneOn_slope_gt
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
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
obtain : ∀ (z : ℝ) (hxz : x < z) (hzy : z < min b y), ∃ x_1 ∈ Ioo x b, x_1 ≤ y
⊢ ∃ x_1 ∈ Ioo x b, x_1 ≤ y

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

Premises used: lt_min, exists_between, And.right
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
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 < min b y
⊢ ∃ x_1 ∈ Ioo x b, x_1 ≤ y

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

Premises used: LT.lt.le, min_le_left, LT.lt.trans_le, And.intro, min_le_right, Exists.intro, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
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 < min 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 _ _)⟩
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
hxs' : ∃ (l : ℝ) (u : ℝ), x ∈ Ioo l u ∧ Ioo l u ⊆ S
obtain :
  ∀ (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
⊢ HasDerivWithinAt f (sSup (slope f x '' {y : ℝ | y ∈ S ∧ y < x})) (Iio x) x

Tactic:
obtain ⟨a, b, hxab, habs⟩ := hxs'
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
simp_rw : Tendsto (slope f x) (𝓝[Iio x \ {x}] x) (𝓝 (sSup (slope f x '' {y : ℝ | y ∈ S ∧ y < x})))
⊢ HasDerivWithinAt f (sSup (slope f x '' {y : ℝ | y ∈ S ∧ y < x})) (Iio x) x

Tactic:
simp_rw [hasDerivWithinAt_iff_tendsto_slope]

Premises used: hasDerivWithinAt_iff_tendsto_slope
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
simp : Tendsto (slope f x) (𝓝[<] x) (𝓝 (sSup (slope f x '' {y : ℝ | y ∈ S ∧ y < x})))
⊢ 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]

Premises used: Set.mem_Iio, Set.diff_singleton_eq_self, lt_self_iff_false, not_false_eq_true
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
⊢ Ioo a 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⟩
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
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

Premises used: And.left
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
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 '' Ioo a 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_mono h))
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
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})
rwa rwa₁ rwa₂ rwa₃ : 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:
rwa [← this]
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
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)))
suffices : 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:
suffices sSup (slope f x '' Ioo a x) = sSup (slope f x '' {y ∈ S | y < x}) by rwa [← this]
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
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)))
apply : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) {y : ℝ | y ∈ S ∧ y < x} y → ∃ x_1 ∈ Ioo a x, y ≤ x_1
⊢ 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 ?_

Premises used: ConvexOn.monotoneOn_slope_lt, bddAbove_slope_gt_of_mem_interior, MonotoneOn.csSup_eq_of_subset_of_forall_exists_le
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
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
obtain : ∀ (z : ℝ) (hyz : max a y < z) (hzx : z < x), ∃ x_1 ∈ Ioo a x, y ≤ x_1
⊢ ∃ x_1 ∈ Ioo a x, y ≤ x_1

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

Premises used: exists_between, max_lt, And.left
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
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 : max a y < z
hzx : z < x
⊢ ∃ x_1 ∈ Ioo a x, y ≤ x_1

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

Premises used: le_max_right, LT.lt.le, And.intro, Exists.intro, LE.le.trans, le_max_left, LE.le.trans_lt
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
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 : max 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⟩
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
⊢ DifferentiableWithinAt ℝ f (Ioi x) x

Tactic:
(hfc.hasDerivWithinAt_sInf_slope_of_mem_interior hxs).differentiableWithinAt

Premises used: HasDerivWithinAt.differentiableWithinAt, ConvexOn.hasDerivWithinAt_sInf_slope_of_mem_interior
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
⊢ DifferentiableWithinAt ℝ f (Iio x) x

Tactic:
(hfc.hasDerivWithinAt_sSup_slope_of_mem_interior hxs).differentiableWithinAt

Premises used: HasDerivWithinAt.differentiableWithinAt, ConvexOn.hasDerivWithinAt_sSup_slope_of_mem_interior
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
⊢ HasDerivWithinAt f (derivWithin f (Ioi x) x) (Ioi x) x

Tactic:
(hfc.differentiableWithinAt_Ioi_of_mem_interior hxs).hasDerivWithinAt

Premises used: DifferentiableWithinAt.hasDerivWithinAt, ConvexOn.differentiableWithinAt_Ioi_of_mem_interior
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
⊢ HasDerivWithinAt f (derivWithin f (Iio x) x) (Iio x) x

Tactic:
(hfc.differentiableWithinAt_Iio_of_mem_interior hxs).hasDerivWithinAt

Premises used: ConvexOn.differentiableWithinAt_Iio_of_mem_interior, DifferentiableWithinAt.hasDerivWithinAt
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
⊢ derivWithin f (Ioi x) x = sInf (slope f x '' {y : ℝ | y ∈ S ∧ x < y})

Tactic:
(hfc.hasDerivWithinAt_sInf_slope_of_mem_interior hxs).derivWithin (uniqueDiffWithinAt_Ioi x)

Premises used: HasDerivWithinAt.derivWithin, uniqueDiffWithinAt_Ioi, ConvexOn.hasDerivWithinAt_sInf_slope_of_mem_interior
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
⊢ derivWithin f (Iio x) x = sSup (slope f x '' {y : ℝ | y ∈ S ∧ y < x})

Tactic:
(hfc.hasDerivWithinAt_sSup_slope_of_mem_interior hxs).derivWithin (uniqueDiffWithinAt_Iio x)

Premises used: HasDerivWithinAt.derivWithin, uniqueDiffWithinAt_Iio, ConvexOn.hasDerivWithinAt_sSup_slope_of_mem_interior
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy : x ≤ y
inl :
  ∀ (hys : x ∈ interior S) (hxy : x ≤ x),
    LE.le (α := ℝ) ((fun (x : ℝ) ↦ derivWithin f (Ioi x) x) x) ((fun (x : ℝ) ↦ derivWithin f (Ioi x) x) x)
inr :
  ∀ (hxy : x < y),
    LE.le (α := ℝ) ((fun (x : ℝ) ↦ derivWithin f (Ioi x) x) x) ((fun (x : ℝ) ↦ derivWithin f (Ioi x) x) y)
⊢ LE.le (α := ℝ) ((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

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs hys : x ∈ interior S
hxy : x ≤ x
⊢ LE.le (α := ℝ) ((fun (x : ℝ) ↦ derivWithin f (Ioi x) x) x) ((fun (x : ℝ) ↦ derivWithin f (Ioi x) x) x)

Tactic:
rfl
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy_1 : x ≤ y
hxy : x < y
inr : sInf (slope f x '' {y : ℝ | y ∈ S ∧ x < y}) ≤ sInf (slope f y '' {y_1 : ℝ | y_1 ∈ S ∧ y < y_1})
⊢ LE.le (α := ℝ) ((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]

Premises used: ConvexOn.rightDeriv_eq_sInf_slope_of_mem_interior
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy_1 : x ≤ y
hxy : x < y
simp : y ∈ S
⊢ Membership.mem (γ := Set ℝ) {y : ℝ | y ∈ S ∧ x < y} y ∧ slope f x y = slope f x y

Tactic:
simp only [mem_setOf_eq, hxy, and_true]

Premises used: and_true, Set.mem_setOf_eq
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy_1 : x ≤ y
hxy : x < y
⊢ y ∈ S

Tactic:
interior_subset hys

Premises used: interior_subset
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy_1 : x ≤ y
hxy : x < y
⊢ y ∈ S

Tactic:
exact interior_subset hys

Premises used: interior_subset
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy_1 : x ≤ y
hxy : x < y
inr : (slope f y '' {y_1 : ℝ | y_1 ∈ S ∧ y < y_1}).Nonempty
inr₁ : ∀ b ∈ slope f y '' {y_1 : ℝ | y_1 ∈ S ∧ y < y_1}, slope f x y ≤ b
⊢ 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 ?_ ?_)

Premises used: le_csInf, csInf_le_of_le, bddBelow_slope_lt_of_mem_interior, Exists.intro
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy_1 : x ≤ y
hxy : x < y
⊢ y ∈ interior S

Tactic:
have hys' := hys
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy_1 : x ≤ y
hxy : x < y
hys' : y ∈ interior S
⊢ ∃ (l : ℝ) (u : ℝ), y ∈ Ioo l u ∧ Ioo l u ⊆ S

Tactic:
rw [mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset] at hys'

Premises used: mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy_1 : x ≤ y
hxy : x < y
hys' : ∃ (l : ℝ) (u : ℝ), y ∈ Ioo l u ∧ Ioo l u ⊆ S
inr : ∀ (a b : ℝ) (hxab : y ∈ Ioo a b) (habs : Ioo a b ⊆ S), (slope f y '' {y_1 : ℝ | y_1 ∈ S ∧ y < y_1}).Nonempty
⊢ (slope f y '' {y_1 : ℝ | y_1 ∈ S ∧ y < y_1}).Nonempty

Tactic:
obtain ⟨a, b, hxab, habs⟩ := hys'
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy_1 : x ≤ y
hxy : x < y
a b : ℝ
hxab : y ∈ Ioo a b
habs : Ioo a b ⊆ S
inr : Set.Nonempty (α := ℝ) {y_1 : ℝ | y_1 ∈ S ∧ y < y_1}
⊢ (slope f y '' {y_1 : ℝ | y_1 ∈ S ∧ y < y_1}).Nonempty

Tactic:
rw [image_nonempty]

Premises used: Set.image_nonempty
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy_1 : x ≤ y
hxy : x < y
a b : ℝ
hxab : y ∈ Ioo a b
habs : Ioo a b ⊆ S
inr : ∀ (z : ℝ) (hxz : y < z) (hzb : z < b), Set.Nonempty (α := ℝ) {y_1 : ℝ | y_1 ∈ S ∧ y < y_1}
⊢ Set.Nonempty (α := ℝ) {y_1 : ℝ | y_1 ∈ S ∧ y < y_1}

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

Premises used: exists_between, And.right
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy_1 : x ≤ y
hxy : x < y
a b : ℝ
hxab : y ∈ Ioo a b
habs : Ioo a b ⊆ S
z : ℝ
hxz : y < z
hzb : z < b
⊢ Set.Nonempty (α := ℝ) {y_1 : ℝ | y_1 ∈ S ∧ y < y_1}

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

Premises used: Set.Nonempty, And.left, And.intro, Exists.intro, LT.lt.trans
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy_1 : x ≤ y
hxy : x < y
a b : ℝ
hxab : y ∈ Ioo a b
habs : Ioo a b ⊆ S
z : ℝ
hxz : y < z
hzb : z < b
⊢ Set.Nonempty (α := ℝ) {y_1 : ℝ | y_1 ∈ S ∧ y < y_1}

Tactic:
exact ⟨z, habs ⟨hxab.1.trans hxz, hzb⟩, hxz⟩
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy_1 : x ≤ y
hxy : x < y
z : ℝ
hzs : z ∈ S
hyz : y < z
inr : slope f y x ≤ slope f y z
⊢ slope f x y ≤ slope f y z

Tactic:
rw [slope_comm]

Premises used: slope_comm
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy_1 : x ≤ y
hxy : x < y
z : ℝ
hzs : z ∈ S
hyz : y < z
⊢ slope f y x ≤ slope f y z

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

Premises used: interior_subset, LT.lt.le, ConvexOn.slope_mono, LT.lt.ne', And.intro, LT.lt.trans, LT.lt.ne
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy_1 : 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

Premises used: interior_subset, LT.lt.le, ConvexOn.slope_mono, LT.lt.ne', And.intro, LT.lt.trans, LT.lt.ne
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy : x ≤ y
inl :
  ∀ (hys : x ∈ interior S) (hxy : x ≤ x),
    LE.le (α := ℝ) ((fun (x : ℝ) ↦ derivWithin f (Iio x) x) x) ((fun (x : ℝ) ↦ derivWithin f (Iio x) x) x)
inr :
  ∀ (hxy : x < y),
    LE.le (α := ℝ) ((fun (x : ℝ) ↦ derivWithin f (Iio x) x) x) ((fun (x : ℝ) ↦ derivWithin f (Iio x) x) y)
⊢ LE.le (α := ℝ) ((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

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs hys : x ∈ interior S
hxy : x ≤ x
⊢ LE.le (α := ℝ) ((fun (x : ℝ) ↦ derivWithin f (Iio x) x) x) ((fun (x : ℝ) ↦ derivWithin f (Iio x) x) x)

Tactic:
rfl
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy_1 : x ≤ y
hxy : x < y
inr : sSup (slope f x '' {y : ℝ | y ∈ S ∧ y < x}) ≤ sSup (slope f y '' {y_1 : ℝ | y_1 ∈ S ∧ y_1 < y})
⊢ LE.le (α := ℝ) ((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]

Premises used: ConvexOn.leftDeriv_eq_sSup_slope_of_mem_interior