awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : x ∈ S
⊢ Membership.mem (γ := Set ℝ) {y_1 : ℝ | y_1 ∈ S ∧ y_1 < y} x ∧ slope f y x = slope f x y

Tactic:
simp only [slope_comm, mem_setOf_eq, hxy, and_true]

Premises used: and_true, slope_comm, 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
⊢ x ∈ S

Tactic:
interior_subset hxs

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
⊢ x ∈ S

Tactic:
exact interior_subset hxs

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 x '' {y : ℝ | y ∈ S ∧ y < x}).Nonempty
inr₁ : ∀ b ∈ slope f x '' {y : ℝ | y ∈ S ∧ y < x}, b ≤ slope f x y
⊢ sSup (slope f x '' {y : ℝ | y ∈ S ∧ y < x}) ≤ sSup (slope f y '' {y_1 : ℝ | y_1 ∈ S ∧ y_1 < y})

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

Premises used: bddAbove_slope_gt_of_mem_interior, le_csSup_of_le, Exists.intro, csSup_le
-- 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
⊢ x ∈ interior S

Tactic:
have hxs' := hxs
-- 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
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 : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy_1 : x ≤ y
hxy : x < y
hxs' : ∃ (l : ℝ) (u : ℝ), x ∈ Ioo l u ∧ Ioo l u ⊆ S
inr : ∀ (a b : ℝ) (hxab : x ∈ Ioo a b) (habs : Ioo a b ⊆ S), (slope f x '' {y : ℝ | y ∈ S ∧ y < x}).Nonempty
⊢ (slope f x '' {y : ℝ | y ∈ S ∧ y < x}).Nonempty

Tactic:
obtain ⟨a, b, hxab, habs⟩ := hxs'
-- 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 : x ∈ Ioo a b
habs : Ioo a b ⊆ S
inr : Set.Nonempty (α := ℝ) {y : ℝ | y ∈ S ∧ y < x}
⊢ (slope f x '' {y : ℝ | y ∈ S ∧ y < x}).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 : x ∈ Ioo a b
habs : Ioo a b ⊆ S
inr : ∀ (z : ℝ) (hxz : a < z) (hzb : z < x), Set.Nonempty (α := ℝ) {y : ℝ | y ∈ S ∧ y < x}
⊢ Set.Nonempty (α := ℝ) {y : ℝ | y ∈ S ∧ y < x}

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

Premises used: exists_between, And.left
-- 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 : x ∈ Ioo a b
habs : Ioo a b ⊆ S
z : ℝ
hxz : a < z
hzb : z < x
⊢ Set.Nonempty (α := ℝ) {y : ℝ | y ∈ S ∧ y < x}

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

Premises used: Set.Nonempty, And.right, 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 : x ∈ Ioo a b
habs : Ioo a b ⊆ S
z : ℝ
hxz : a < z
hzb : z < x
⊢ Set.Nonempty (α := ℝ) {y : ℝ | y ∈ S ∧ y < x}

Tactic:
exact ⟨z, habs ⟨hxz, hzb.trans hxab.2⟩, hzb⟩
-- 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 : z < x
⊢ slope f x z ≤ slope f x y

Tactic:
slope_mono hfc (interior_subset hxs) ⟨hzs, hyz.ne⟩ ⟨interior_subset hys, hxy.ne'⟩
      (hyz.trans hxy).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 : z < x
⊢ slope f x z ≤ slope f x y

Tactic:
exact slope_mono hfc (interior_subset hxs) ⟨hzs, hyz.ne⟩ ⟨interior_subset hys, hxy.ne'⟩
      (hyz.trans hxy).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 : ℝ → ℝ
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), derivWithin f (Iio x) x ≤ derivWithin f (Ioi x) x
⊢ derivWithin f (Iio x) x ≤ derivWithin f (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
rw : sSup (slope f x '' {y : ℝ | y ∈ S ∧ y < x}) ≤ sInf (slope f x '' {y : ℝ | y ∈ S ∧ x < y})
⊢ 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]

Premises used: ConvexOn.leftDeriv_eq_sSup_slope_of_mem_interior, ConvexOn.rightDeriv_eq_sInf_slope_of_mem_interior
-- 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
⊢ sSup (slope f x '' {y : ℝ | y ∈ S ∧ y < x}) ≤ sInf (slope f x '' {y : ℝ | y ∈ S ∧ x < y})

Tactic:
csSup_le ?_ ?_

Premises used: csSup_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
refine_1 : (slope f x '' {y : ℝ | y ∈ S ∧ y < x}).Nonempty
refine_2 : ∀ b ∈ slope f x '' {y : ℝ | y ∈ S ∧ y < x}, b ≤ sInf (slope f x '' {y : ℝ | y ∈ S ∧ x < y})
⊢ sSup (slope f x '' {y : ℝ | y ∈ S ∧ y < x}) ≤ sInf (slope f x '' {y : ℝ | y ∈ S ∧ x < y})

Tactic:
refine csSup_le ?_ ?_

Premises used: csSup_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
refine_1 : Set.Nonempty (α := ℝ) {y : ℝ | y ∈ S ∧ y < x}
⊢ (slope f x '' {y : ℝ | y ∈ S ∧ y < x}).Nonempty

Tactic:
rw [image_nonempty]

Premises used: Set.image_nonempty
-- 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
refine_1 : ∀ (z : ℝ) (haz : a < z) (hzx : z < x), Set.Nonempty (α := ℝ) {y : ℝ | y ∈ S ∧ y < x}
⊢ Set.Nonempty (α := ℝ) {y : ℝ | y ∈ S ∧ y < x}

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

Premises used: exists_between, 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
z : ℝ
haz : a < z
hzx : z < x
⊢ Set.Nonempty (α := ℝ) {y : ℝ | y ∈ S ∧ y < x}

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

Premises used: Set.Nonempty, And.right, And.intro, Exists.intro, LT.lt.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
z : ℝ
haz : a < z
hzx : z < x
⊢ Set.Nonempty (α := ℝ) {y : ℝ | y ∈ S ∧ y < x}

Tactic:
exact ⟨z, habs ⟨haz, hzx.trans hxab.2⟩, hzx⟩
-- 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
z : ℝ
hzs : z ∈ S
hzx : z < x
⊢ slope f x z ≤ sInf (slope f x '' {y : ℝ | y ∈ S ∧ x < y})

Tactic:
le_csInf ?_ ?_

Premises used: le_csInf
-- 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
z : ℝ
hzs : z ∈ S
hzx : z < x
refine_2 : (slope f x '' {y : ℝ | y ∈ S ∧ x < y}).Nonempty
refine_2₁ : ∀ b ∈ slope f x '' {y : ℝ | y ∈ S ∧ x < y}, slope f x z ≤ b
⊢ slope f x z ≤ sInf (slope f x '' {y : ℝ | y ∈ S ∧ x < y})

Tactic:
refine le_csInf ?_ ?_

Premises used: le_csInf
-- 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
z : ℝ
hzs : z ∈ S
hzx : z < x
refine_2 : Set.Nonempty (α := ℝ) {y : ℝ | y ∈ S ∧ x < y}
⊢ (slope f x '' {y : ℝ | y ∈ S ∧ x < y}).Nonempty

Tactic:
rw [image_nonempty]

Premises used: Set.image_nonempty
-- 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
z : ℝ
hzs : z ∈ S
hzx : z < x
refine_2 : ∀ (z : ℝ) (hxz : x < z) (hzb : z < b), Set.Nonempty (α := ℝ) {y : ℝ | y ∈ S ∧ x < y}
⊢ Set.Nonempty (α := ℝ) {y : ℝ | y ∈ S ∧ x < y}

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

Premises used: 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
z_1 : ℝ
hzs : z_1 ∈ S
hzx : z_1 < x
z : ℝ
hxz : x < z
hzb : z < b
⊢ Set.Nonempty (α := ℝ) {y : ℝ | y ∈ S ∧ x < y}

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 : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
z_1 : ℝ
hzs : z_1 ∈ S
hzx : z_1 < x
z : ℝ
hxz : x < z
hzb : z < b
⊢ Set.Nonempty (α := ℝ) {y : ℝ | y ∈ S ∧ x < y}

Tactic:
exact ⟨z, habs ⟨hxab.1.trans hxz, hzb⟩, hxz⟩
-- 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
z : ℝ
hzs : z ∈ S
hzx : z < x
y : ℝ
hys : y ∈ S
hxy : x < y
⊢ slope f x z ≤ slope f x y

Tactic:
slope_mono hfc (interior_subset hxs) ⟨hzs, hzx.ne⟩ ⟨hys, hxy.ne'⟩ (hzx.trans hxy).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 : ℝ → ℝ
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

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 : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
apply : ∀ᶠ (c : ℝ) in 𝓝[>] x, slope f x c ≤ slope f x y
⊢ f' ≤ slope f x y

Tactic:
apply le_of_tendsto <| (hasDerivWithinAt_iff_tendsto_slope' self_notMem_Ioi).mp hf'

Premises used: le_of_tendsto, Iff.mp, Set.self_notMem_Ioi, hasDerivWithinAt_iff_tendsto_slope'
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
simp_rw : ∀ᶠ (x_1 : ℝ) in 𝓝 x, x_1 ∈ Ioi x → (f x_1 - f x) / (x_1 - x) ≤ (f y - f x) / (y - x)
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] x, slope f x c ≤ slope f x y

Tactic:
simp_rw [eventually_nhdsWithin_iff, slope_def_field]

Premises used: slope_def_field, eventually_nhdsWithin_iff
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
t : ℝ
ht : t < y
h : ∀ (ht' : x < t), (f t - f x) / (t - x) ≤ (f y - f x) / (y - x)
⊢ t ∈ Ioi x → (f t - f x) / (t - x) ≤ (f y - f x) / (y - x)

Tactic:
(ht' : x < t)
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
h : ∀ (t : ℝ) (ht : t < y) (ht' : x < t), (f t - f x) / (t - x) ≤ (f y - f x) / (y - x)
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝 x, x_1 ∈ Ioi x → (f x_1 - f x) / (x_1 - x) ≤ (f y - f x) / (y - x)

Tactic:
filter_upwards [eventually_lt_nhds hxy] with t ht (ht' : x < t)

Premises used: eventually_lt_nhds
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
t : ℝ
ht : t < y
ht' : x < t
⊢ (f t - f x) / (t - x) ≤ (f y - f x) / (y - x)

Tactic:
hfc.secant_mono hx (?_ : t ∈ S) hy ht'.ne' hxy.ne' ht.le

Premises used: LT.lt.le, ConvexOn.secant_mono, LT.lt.ne'
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
t : ℝ
ht : t < y
ht' : x < t
h : t ∈ S
⊢ (f t - f x) / (t - x) ≤ (f y - f x) / (y - x)

Tactic:
refine hfc.secant_mono hx (?_ : t ∈ S) hy ht'.ne' hxy.ne' ht.le

Premises used: LT.lt.le, ConvexOn.secant_mono, LT.lt.ne'
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
t : ℝ
ht : t < y
ht' : x < t
⊢ t ∈ S

Tactic:
hfc.1.ordConnected.out hx hy ⟨ht'.le, ht.le⟩

Premises used: Set.OrdConnected.out, LT.lt.le, And.left, And.intro, Convex.ordConnected
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
t : ℝ
ht : t < y
ht' : x < t
⊢ t ∈ S

Tactic:
exact hfc.1.ordConnected.out hx hy ⟨ht'.le, ht.le⟩

Premises used: Set.OrdConnected.out, LT.lt.le, And.left, And.intro, Convex.ordConnected
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : DifferentiableWithinAt ℝ f (Ioi x) x
⊢ derivWithin f (Ioi x) x ≤ slope f x y

Tactic:
le_slope_of_hasDerivWithinAt_Ioi hfc hx hy hxy hfd.hasDerivWithinAt

Premises used: DifferentiableWithinAt.hasDerivWithinAt, ConvexOn.le_slope_of_hasDerivWithinAt_Ioi
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
y : ℝ
hxs : x ∈ interior S
hys : y ∈ S
hxy : x < y
⊢ derivWithin f (Ioi x) x ≤ slope f x y

Tactic:
rightDeriv_le_slope hfc (interior_subset hxs) hys hxy
    (differentiableWithinAt_Ioi_of_mem_interior hfc hxs)

Premises used: interior_subset, ConvexOn.differentiableWithinAt_Ioi_of_mem_interior, ConvexOn.rightDeriv_le_slope
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' S x
⊢ f' ≤ slope f x y

Tactic:
hfc.le_slope_of_hasDerivWithinAt_Ioi hx hy hxy <|
    hf'.mono_of_mem_nhdsWithin <| hfc.1.ordConnected.mem_nhdsGT hx hy hxy

Premises used: Set.OrdConnected.mem_nhdsGT, ConvexOn.le_slope_of_hasDerivWithinAt_Ioi, HasDerivWithinAt.mono_of_mem_nhdsWithin, And.left, Convex.ordConnected
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : DifferentiableWithinAt ℝ f S x
⊢ derivWithin f S x ≤ slope f x y

Tactic:
le_slope_of_hasDerivWithinAt hfc hx hy hxy hfd.hasDerivWithinAt

Premises used: DifferentiableWithinAt.hasDerivWithinAt, ConvexOn.le_slope_of_hasDerivWithinAt
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
ha : HasDerivAt f f' x
⊢ f' ≤ slope f x y

Tactic:
hfc.le_slope_of_hasDerivWithinAt_Ioi hx hy hxy ha.hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, ConvexOn.le_slope_of_hasDerivWithinAt_Ioi
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : DifferentiableAt ℝ f x
⊢ deriv f x ≤ slope f x y

Tactic:
le_slope_of_hasDerivAt hfc hx hy hxy hfd.hasDerivAt

Premises used: ConvexOn.le_slope_of_hasDerivAt, DifferentiableAt.hasDerivAt
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
apply : ∀ᶠ (c : ℝ) in 𝓝[<] y, slope f x y ≤ slope f y c
⊢ slope f x y ≤ f'

Tactic:
apply ge_of_tendsto <| (hasDerivWithinAt_iff_tendsto_slope' self_notMem_Iio).mp hf'

Premises used: Set.self_notMem_Iio, ge_of_tendsto, Iff.mp, hasDerivWithinAt_iff_tendsto_slope'
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
simp_rw : ∀ᶠ (x_1 : ℝ) in 𝓝 y, x_1 ∈ Iio y → (f x - f y) / (x - y) ≤ (f x_1 - f y) / (x_1 - y)
⊢ ∀ᶠ (c : ℝ) in 𝓝[<] y, slope f x y ≤ slope f y c

Tactic:
simp_rw [eventually_nhdsWithin_iff, slope_comm f x y, slope_def_field]

Premises used: slope_comm, slope_def_field, eventually_nhdsWithin_iff
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
t : ℝ
ht : x < t
h : ∀ (ht' : t < y), (f x - f y) / (x - y) ≤ (f t - f y) / (t - y)
⊢ t ∈ Iio y → (f x - f y) / (x - y) ≤ (f t - f y) / (t - y)

Tactic:
(ht' : t < y)
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
h : ∀ (t : ℝ) (ht : x < t) (ht' : t < y), (f x - f y) / (x - y) ≤ (f t - f y) / (t - y)
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝 y, x_1 ∈ Iio y → (f x - f y) / (x - y) ≤ (f x_1 - f y) / (x_1 - y)

Tactic:
filter_upwards [eventually_gt_nhds hxy] with t ht (ht' : t < y)

Premises used: eventually_gt_nhds
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
t : ℝ
ht : x < t
ht' : t < y
⊢ (f x - f y) / (x - y) ≤ (f t - f y) / (t - y)

Tactic:
hfc.secant_mono hy hx (?_ : t ∈ S) hxy.ne ht'.ne ht.le

Premises used: LT.lt.le, ConvexOn.secant_mono, LT.lt.ne
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
t : ℝ
ht : x < t
ht' : t < y
h : t ∈ S
⊢ (f x - f y) / (x - y) ≤ (f t - f y) / (t - y)

Tactic:
refine hfc.secant_mono hy hx (?_ : t ∈ S) hxy.ne ht'.ne ht.le

Premises used: LT.lt.le, ConvexOn.secant_mono, LT.lt.ne
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
t : ℝ
ht : x < t
ht' : t < y
⊢ t ∈ S

Tactic:
hfc.1.ordConnected.out hx hy ⟨ht.le, ht'.le⟩

Premises used: Set.OrdConnected.out, LT.lt.le, And.left, And.intro, Convex.ordConnected
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
t : ℝ
ht : x < t
ht' : t < y
⊢ t ∈ S

Tactic:
exact hfc.1.ordConnected.out hx hy ⟨ht.le, ht'.le⟩

Premises used: Set.OrdConnected.out, LT.lt.le, And.left, And.intro, Convex.ordConnected
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : DifferentiableWithinAt ℝ f (Iio y) y
⊢ slope f x y ≤ derivWithin f (Iio y) y

Tactic:
hfc.slope_le_of_hasDerivWithinAt_Iio hx hy hxy hfd.hasDerivWithinAt

Premises used: DifferentiableWithinAt.hasDerivWithinAt, ConvexOn.slope_le_of_hasDerivWithinAt_Iio
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y : ℝ
hfc : ConvexOn ℝ S f
hys : x ∈ S
hxs : y ∈ interior S
hxy : x < y
⊢ slope f x y ≤ derivWithin f (Iio y) y

Tactic:
slope_le_leftDeriv hfc hys (interior_subset hxs) hxy
    (differentiableWithinAt_Iio_of_mem_interior hfc hxs)

Premises used: ConvexOn.differentiableWithinAt_Iio_of_mem_interior, interior_subset, ConvexOn.slope_le_leftDeriv
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' S y
⊢ slope f x y ≤ f'

Tactic:
hfc.slope_le_of_hasDerivWithinAt_Iio hx hy hxy <|
    hf'.mono_of_mem_nhdsWithin <| hfc.1.ordConnected.mem_nhdsLT hx hy hxy

Premises used: Set.OrdConnected.mem_nhdsLT, HasDerivWithinAt.mono_of_mem_nhdsWithin, And.left, Convex.ordConnected, ConvexOn.slope_le_of_hasDerivWithinAt_Iio
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : DifferentiableWithinAt ℝ f S y
⊢ slope f x y ≤ derivWithin f S y

Tactic:
hfc.slope_le_of_hasDerivWithinAt hx hy hxy hfd.hasDerivWithinAt

Premises used: DifferentiableWithinAt.hasDerivWithinAt, ConvexOn.slope_le_of_hasDerivWithinAt
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivAt f f' y
⊢ slope f x y ≤ f'

Tactic:
hfc.slope_le_of_hasDerivWithinAt_Iio hx hy hxy hf'.hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, ConvexOn.slope_le_of_hasDerivWithinAt_Iio
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : DifferentiableAt ℝ f y
⊢ slope f x y ≤ deriv f y

Tactic:
hfc.slope_le_of_hasDerivAt hx hy hxy hfd.hasDerivAt

Premises used: DifferentiableAt.hasDerivAt, ConvexOn.slope_le_of_hasDerivAt
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x ≤ y
inl : ∀ (hy : x ∈ S) (hxy : x ≤ x), derivWithin f S x ≤ derivWithin f S x
inr : ∀ (hxy' : x < y), derivWithin f S x ≤ derivWithin f S y
⊢ derivWithin f S x ≤ derivWithin f S 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
hfd : DifferentiableOn ℝ f S
x : ℝ
hx hy : x ∈ S
hxy : x ≤ x
⊢ derivWithin f S x ≤ derivWithin f S x

Tactic:
rfl
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x ≤ y
hxy' : x < y
⊢ derivWithin f S x ≤ derivWithin f S y

Tactic:
(hfc.derivWithin_le_slope hx hy hxy' (hfd x hx)).trans
    (hfc.slope_le_derivWithin hx hy hxy' (hfd y hy))

Premises used: ConvexOn.derivWithin_le_slope, ConvexOn.slope_le_derivWithin, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x ≤ y
hxy' : x < y
⊢ derivWithin f S x ≤ derivWithin f S y

Tactic:
exact (hfc.derivWithin_le_slope hx hy hxy' (hfd x hx)).trans
    (hfc.slope_le_derivWithin hx hy hxy' (hfd y hy))

Premises used: ConvexOn.derivWithin_le_slope, ConvexOn.slope_le_derivWithin, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x ≤ y
inl : ∀ (hy : x ∈ S) (hxy : x ≤ x), deriv f x ≤ deriv f x
inr : ∀ (hxy' : x < y), deriv f x ≤ deriv f y
⊢ deriv f x ≤ deriv f 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
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
x : ℝ
hx hy : x ∈ S
hxy : x ≤ x
⊢ deriv f x ≤ deriv f x

Tactic:
rfl