awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ Membership.mem (γ := Set ℝ) {y : ℝ | y ∈ S ∧ x < y} y ∧ slope f x y = slope f x y
have simp : y ∈ S
Tactic: simp only [mem_setOf_eq, hxy, and_true]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ sInf (slope f x '' {y : ℝ | y ∈ S ∧ x < y}) ≤ sInf (slope f y '' {y_1 : ℝ | y_1 ∈ S ∧ y < y_1})
have inr : (slope f y '' {y_1 : ℝ | y_1 ∈ S ∧ y < y_1}).Nonempty
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 ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ sInf (slope f x '' {y : ℝ | y ∈ S ∧ x < y}) ≤ sInf (slope f y '' {y_1 : ℝ | y_1 ∈ S ∧ y < y_1})
have inr₁ : ∀ b ∈ slope f y '' {y_1 : ℝ | y_1 ∈ S ∧ y < y_1}, slope f x y ≤ b
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 ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
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
⊢ (slope f y '' {y_1 : ℝ | y_1 ∈ S ∧ y < y_1}).Nonempty
have hys'₁ : ∃ (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'
Cleared hypotheses: hys'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ (slope f y '' {y_1 : ℝ | y_1 ∈ S ∧ y < y_1}).Nonempty
have 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
Tactic: obtain ⟨a, b, hxab, habs⟩ := hys'
Cleared hypotheses: hys'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ (slope f y '' {y_1 : ℝ | y_1 ∈ S ∧ y < y_1}).Nonempty
have inr : Set.Nonempty (α := ℝ) {y_1 : ℝ | y_1 ∈ S ∧ y < y_1}
Tactic: rw [image_nonempty]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ Set.Nonempty (α := ℝ) {y_1 : ℝ | y_1 ∈ S ∧ y < y_1}
have inr : ∀ (z : ℝ) (hxz : y < z) (hzb : z < b), Set.Nonempty (α := ℝ) {y_1 : ℝ | y_1 ∈ S ∧ y < y_1}
Tactic: obtain ⟨z, hxz, hzb⟩ := exists_between hxab.2
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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 x y ≤ slope f y z
have inr : slope f y x ≤ slope f y z
Tactic: rw [slope_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy : x ≤ y
⊢ LE.le (α := ℝ) ((fun (x : ℝ) ↦ derivWithin f (Iio x) x) x) ((fun (x : ℝ) ↦ derivWithin f (Iio x) x) y)
have 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)
Tactic: rcases eq_or_lt_of_le hxy with rfl | hxy
Cleared hypotheses: y, hys, hxy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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)
⊢ LE.le (α := ℝ) ((fun (x : ℝ) ↦ derivWithin f (Iio x) x) x) ((fun (x : ℝ) ↦ derivWithin f (Iio x) x) y)
have inr : ∀ (hxy : 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
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ LE.le (α := ℝ) ((fun (x : ℝ) ↦ derivWithin f (Iio x) x) x) ((fun (x : ℝ) ↦ derivWithin f (Iio x) x) y)
have inr : sSup (slope f x '' {y : ℝ | y ∈ S ∧ y < x}) ≤ sSup (slope f y '' {y_1 : ℝ | y_1 ∈ S ∧ y_1 < y})
Tactic: simp_rw [hfc.leftDeriv_eq_sSup_slope_of_mem_interior hxs,
    hfc.leftDeriv_eq_sSup_slope_of_mem_interior hys]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ Membership.mem (γ := Set ℝ) {y_1 : ℝ | y_1 ∈ S ∧ y_1 < y} x ∧ slope f y x = slope f x y
have simp : x ∈ S
Tactic: simp only [slope_comm, mem_setOf_eq, hxy, and_true]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ sSup (slope f x '' {y : ℝ | y ∈ S ∧ y < x}) ≤ sSup (slope f y '' {y_1 : ℝ | y_1 ∈ S ∧ y_1 < y})
have inr : (slope f x '' {y : ℝ | y ∈ S ∧ y < x}).Nonempty
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 ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ sSup (slope f x '' {y : ℝ | y ∈ S ∧ y < x}) ≤ sSup (slope f y '' {y_1 : ℝ | y_1 ∈ S ∧ y_1 < y})
have inr₁ : ∀ b ∈ slope f x '' {y : ℝ | y ∈ S ∧ y < x}, b ≤ slope f x 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 ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
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
⊢ (slope f x '' {y : ℝ | y ∈ S ∧ y < x}).Nonempty
have hxs'₁ : ∃ (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'
Cleared hypotheses: hxs'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ (slope f x '' {y : ℝ | y ∈ S ∧ y < x}).Nonempty
have inr : ∀ (a b : ℝ) (hxab : x ∈ Ioo a b) (habs : Ioo a b ⊆ S), (slope f x '' {y : ℝ | y ∈ S ∧ y < x}).Nonempty
Tactic: obtain ⟨a, b, hxab, habs⟩ := hxs'
Cleared hypotheses: hxs'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ (slope f x '' {y : ℝ | y ∈ S ∧ y < x}).Nonempty
have inr : Set.Nonempty (α := ℝ) {y : ℝ | y ∈ S ∧ y < x}
Tactic: rw [image_nonempty]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ Set.Nonempty (α := ℝ) {y : ℝ | y ∈ S ∧ y < x}
have inr : ∀ (z : ℝ) (hxz : a < z) (hzb : z < x), Set.Nonempty (α := ℝ) {y : ℝ | y ∈ S ∧ y < x}
Tactic: obtain ⟨z, hxz, hzb⟩ := exists_between hxab.1
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs hxs' : x ∈ interior S
⊢ derivWithin f (Iio x) x ≤ derivWithin f (Ioi x) x
have hxs'₁ : ∃ (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'
Cleared hypotheses: hxs'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
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
have obtain : ∀ (a b : ℝ) (hxab : x ∈ Ioo a b) (habs : Ioo a b ⊆ S), derivWithin f (Iio x) x ≤ derivWithin f (Ioi x) x
Tactic: obtain ⟨a, b, hxab, habs⟩ := hxs'
Cleared hypotheses: hxs'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ derivWithin f (Iio x) x ≤ derivWithin f (Ioi x) x
have rw : sSup (slope f x '' {y : ℝ | y ∈ S ∧ y < x}) ≤ sInf (slope f x '' {y : ℝ | y ∈ S ∧ x < y})
Tactic: rw [hfc.rightDeriv_eq_sInf_slope_of_mem_interior hxs,
    hfc.leftDeriv_eq_sSup_slope_of_mem_interior hxs]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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})
have refine_1 : (slope f x '' {y : ℝ | y ∈ S ∧ y < x}).Nonempty
Tactic: refine csSup_le ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ sSup (slope f x '' {y : ℝ | y ∈ S ∧ y < x}) ≤ sInf (slope f x '' {y : ℝ | y ∈ S ∧ x < y})
have refine_2 : ∀ b ∈ slope f x '' {y : ℝ | y ∈ S ∧ y < x}, b ≤ sInf (slope f x '' {y : ℝ | y ∈ S ∧ x < y})
Tactic: refine csSup_le ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ (slope f x '' {y : ℝ | y ∈ S ∧ y < x}).Nonempty
have refine_1 : Set.Nonempty (α := ℝ) {y : ℝ | y ∈ S ∧ y < x}
Tactic: rw [image_nonempty]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ Set.Nonempty (α := ℝ) {y : ℝ | y ∈ S ∧ y < x}
have refine_1 : ∀ (z : ℝ) (haz : a < z) (hzx : z < x), Set.Nonempty (α := ℝ) {y : ℝ | y ∈ S ∧ y < x}
Tactic: obtain ⟨z, haz, hzx⟩ := exists_between hxab.1
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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})
have refine_2 : (slope f x '' {y : ℝ | y ∈ S ∧ x < y}).Nonempty
Tactic: refine le_csInf ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ slope f x z ≤ sInf (slope f x '' {y : ℝ | y ∈ S ∧ x < y})
have refine_2₁ : ∀ b ∈ slope f x '' {y : ℝ | y ∈ S ∧ x < y}, slope f x z ≤ b
Tactic: refine le_csInf ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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 '' {y : ℝ | y ∈ S ∧ x < y}).Nonempty
have refine_2 : Set.Nonempty (α := ℝ) {y : ℝ | y ∈ S ∧ x < y}
Tactic: rw [image_nonempty]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ Set.Nonempty (α := ℝ) {y : ℝ | y ∈ S ∧ x < y}
have refine_2 : ∀ (z : ℝ) (hxz : x < z) (hzb : z < b), Set.Nonempty (α := ℝ) {y : ℝ | y ∈ S ∧ x < y}
Tactic: obtain ⟨z, hxz, hzb⟩ := exists_between hxab.2
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ f' ≤ slope f x y
have apply : ∀ᶠ (c : ℝ) in 𝓝[>] x, slope f x c ≤ slope f x y
Tactic: apply le_of_tendsto <| (hasDerivWithinAt_iff_tendsto_slope' self_notMem_Ioi).mp hf'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] x, slope f x c ≤ slope f x y
have simp_rw : ∀ᶠ (x_1 : ℝ) in 𝓝 x, x_1 ∈ Ioi x → (f x_1 - f x) / (x_1 - x) ≤ (f y - f x) / (y - x)
Tactic: simp_rw [eventually_nhdsWithin_iff, slope_def_field]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ t ∈ Ioi x → (f t - f x) / (t - x) ≤ (f y - f x) / (y - x)
have h : ∀ (ht' : x < t), (f t - f x) / (t - x) ≤ (f y - f x) / (y - x)
Tactic: (ht' : x < t)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝 x, x_1 ∈ Ioi x → (f x_1 - f x) / (x_1 - x) ≤ (f y - f x) / (y - x)
have h : ∀ (t : ℝ) (ht : t < y) (ht' : x < t), (f t - f x) / (t - x) ≤ (f y - f x) / (y - x)
Tactic: filter_upwards [eventually_lt_nhds hxy] with t ht (ht' : x < t)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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)
have h : t ∈ S
Tactic: refine hfc.secant_mono hx (?_ : t ∈ S) hy ht'.ne' hxy.ne' ht.le
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ slope f x y ≤ f'
have apply : ∀ᶠ (c : ℝ) in 𝓝[<] y, slope f x y ≤ slope f y c
Tactic: apply ge_of_tendsto <| (hasDerivWithinAt_iff_tendsto_slope' self_notMem_Iio).mp hf'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ ∀ᶠ (c : ℝ) in 𝓝[<] y, slope f x y ≤ slope f y c
have simp_rw : ∀ᶠ (x_1 : ℝ) in 𝓝 y, x_1 ∈ Iio y → (f x - f y) / (x - y) ≤ (f x_1 - f y) / (x_1 - y)
Tactic: simp_rw [eventually_nhdsWithin_iff, slope_comm f x y, slope_def_field]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ t ∈ Iio y → (f x - f y) / (x - y) ≤ (f t - f y) / (t - y)
have h : ∀ (ht' : t < y), (f x - f y) / (x - y) ≤ (f t - f y) / (t - y)
Tactic: (ht' : t < y)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝 y, x_1 ∈ Iio y → (f x - f y) / (x - y) ≤ (f x_1 - f y) / (x_1 - y)
have h : ∀ (t : ℝ) (ht : x < t) (ht' : t < y), (f x - f y) / (x - y) ≤ (f t - f y) / (t - y)
Tactic: filter_upwards [eventually_gt_nhds hxy] with t ht (ht' : t < y)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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)
have h : t ∈ S
Tactic: refine hfc.secant_mono hy hx (?_ : t ∈ S) hxy.ne ht'.ne ht.le
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x ≤ y
⊢ derivWithin f S x ≤ derivWithin f S y
have inl : ∀ (hy : x ∈ S) (hxy : x ≤ x), derivWithin f S x ≤ derivWithin f S x
Tactic: rcases eq_or_lt_of_le hxy with rfl | hxy'
Cleared hypotheses: y, hy, hxy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ derivWithin f S x ≤ derivWithin f S y
have inr : ∀ (hxy' : x < y), derivWithin f S x ≤ derivWithin f S y
Tactic: rcases eq_or_lt_of_le hxy with rfl | hxy'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ deriv f x ≤ deriv f y
have inl : ∀ (hy : x ∈ S) (hxy : x ≤ x), deriv f x ≤ deriv f x
Tactic: rcases eq_or_lt_of_le hxy with rfl | hxy'
Cleared hypotheses: y, hy, hxy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ deriv f x ≤ deriv f y
have inr : ∀ (hxy' : x < y), deriv f x ≤ deriv f y
Tactic: rcases eq_or_lt_of_le hxy with rfl | hxy'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
⊢ Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ f x ≤ f x_2) x_1} y
have inl : ∀ (hxy : x < y), Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ f x ≤ f x_2) x_1} y
Tactic: rcases lt_trichotomy x y with hxy | h_eq | hyx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
inl : ∀ (hxy : x < y), Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ f x ≤ f x_2) x_1} y
⊢ Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ f x ≤ f x_2) x_1} y
have inr : ∀ (h_eq : x = y), Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ f x ≤ f x_2) x_1} y
Tactic: rcases lt_trichotomy x y with hxy | h_eq | hyx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
inl : ∀ (hxy : x < y), Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ f x ≤ f x_2) x_1} y
inr : ∀ (h_eq : x = y), Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ f x ≤ f x_2) x_1} y
⊢ Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ f x ≤ f x_2) x_1} y
have inr₁ : ∀ (hyx : y < x), Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ f x ≤ f x_2) x_1} y
Tactic: rcases lt_trichotomy x y with hxy | h_eq | hyx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
hxy : x < y
this : 0 ≤ slope f x y
⊢ Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ f x ≤ f x_2) x_1} y
have this₁ : f x ≤ f y ∧ x ≤ y
Tactic: simp only [slope_def_field, div_nonneg_iff, sub_nonneg, tsub_le_iff_right, zero_add,
        not_le.mpr hxy, and_false, or_false] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ f x ≤ f x_2) x_1} y
have inl : 0 ≤ slope f x y
Tactic: suffices 0 ≤ slope f x y by
      simp only [slope_def_field, div_nonneg_iff, sub_nonneg, tsub_le_iff_right, zero_add,
        not_le.mpr hxy, and_false, or_false] at this
      exact this.1
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
hyx : y < x
this : slope f x y ≤ 0
⊢ Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ f x ≤ f x_2) x_1} y
have this₁ : f x ≤ f y ∧ y ≤ x
Tactic: simp only [slope_def_field, div_nonpos_iff, sub_nonneg, tsub_le_iff_right, zero_add,
        not_le.mpr hyx, and_false, or_false] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
hyx : y < x
⊢ Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ f x ≤ f x_2) x_1} y
have inr : slope f x y ≤ 0
Tactic: suffices slope f x y ≤ 0 by
      simp only [slope_def_field, div_nonpos_iff, sub_nonneg, tsub_le_iff_right, zero_add,
        not_le.mpr hyx, and_false, or_false] at this
      exact this.1
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
hyx : y < x
⊢ slope f x y ≤ 0
have inr : slope f y x ≤ 0
Tactic: rw [slope_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_rd : derivWithin f (Ioi x) x = 0
⊢ IsMinOn f S x
have refine : derivWithin f (Iio x) x ≤ 0
Tactic: refine hf.isMinOn_of_leftDeriv_nonpos_of_rightDeriv_nonneg hx ?_ hf_rd.symm.le
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x = 0
⊢ IsMinOn f S x
have refine : 0 ≤ derivWithin f (Ioi x) x
Tactic: refine hf.isMinOn_of_leftDeriv_nonpos_of_rightDeriv_nonneg hx hf_ld.le ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
⊢ f' < slope f x y
have obtain : ∀ (u : ℝ) (hxu : x < u) (huy : u < y), f' < slope f x y
Tactic: obtain ⟨u, hxu, huy⟩ := exists_between hxy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
u : ℝ
hxu : x < u
huy : u < y
⊢ f' < slope f x y
have hu : u ∈ S
Tactic: have hu : u ∈ S := hfc.1.ordConnected.out hx hy ⟨hxu.le, huy.le⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
u : ℝ
hxu : x < u
huy : u < y
hu : u ∈ S
⊢ f' < slope f x y
have this : (f u - f x) / (u - x) < (f y - f x) / (y - x)
Tactic: have := hfc.secant_strict_mono hx hu hy hxu.ne' hxy.ne' huy