awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, 0 ≤ f'' x
⊢ ConvexOn ℝ D f
have this : EqOn (deriv f) f' (interior D)
Tactic: have : (interior D).EqOn (deriv f) f' := deriv_eqOn isOpen_interior hf'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, 0 ≤ f'' x
this : EqOn (deriv f) f' (interior D)
⊢ ConvexOn ℝ D f
have refine_1 : DifferentiableOn ℝ (deriv f) (interior D)
Tactic: refine convexOn_of_deriv2_nonneg hD hf (fun x hx ↦ (hf' _ hx).differentiableWithinAt) ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, 0 ≤ f'' x
this : EqOn (deriv f) f' (interior D)
refine_1 : DifferentiableOn ℝ (deriv f) (interior D)
⊢ ConvexOn ℝ D f
have refine_2 : ∀ x ∈ interior D, 0 ≤ deriv^[2] f x
Tactic: refine convexOn_of_deriv2_nonneg hD hf (fun x hx ↦ (hf' _ hx).differentiableWithinAt) ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, 0 ≤ f'' x
this : EqOn (deriv f) f' (interior D)
⊢ DifferentiableOn ℝ (deriv f) (interior D)
have refine_1 : DifferentiableOn ℝ f' (interior D)
Tactic: rw [differentiableOn_congr this]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, 0 ≤ f'' x
this : EqOn (deriv f) f' (interior D)
x : ℝ
hx : x ∈ interior D
⊢ 0 ≤ deriv^[2] f x
have h : deriv^[2] f x = f'' x
Tactic: convert! hf''₀ _ hx using 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, 0 ≤ f'' x
this : EqOn (deriv f) f' (interior D)
x : ℝ
hx : x ∈ interior D
⊢ deriv (deriv f) x = f'' x
have rw : ∀ (y : ℝ) (hy : y ∈ interior D), HasDerivWithinAt (deriv f) (f'' y) (interior D) y
Tactic: rw [deriv_eqOn isOpen_interior (fun y hy ↦ ?_) hx]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, 0 ≤ f'' x
this : EqOn (deriv f) f' (interior D)
x : ℝ
hx : x ∈ interior D
y : ℝ
hy : y ∈ interior D
⊢ deriv f y = f' y
have rw : f' y = f' y
Tactic: rw [this hy]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0
⊢ ConcaveOn ℝ D f
have this : EqOn (deriv f) f' (interior D)
Tactic: have : (interior D).EqOn (deriv f) f' := deriv_eqOn isOpen_interior hf'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0
this : EqOn (deriv f) f' (interior D)
⊢ ConcaveOn ℝ D f
have refine_1 : DifferentiableOn ℝ (deriv f) (interior D)
Tactic: refine concaveOn_of_deriv2_nonpos hD hf (fun x hx ↦ (hf' _ hx).differentiableWithinAt) ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0
this : EqOn (deriv f) f' (interior D)
refine_1 : DifferentiableOn ℝ (deriv f) (interior D)
⊢ ConcaveOn ℝ D f
have refine_2 : ∀ x ∈ interior D, deriv^[2] f x ≤ 0
Tactic: refine concaveOn_of_deriv2_nonpos hD hf (fun x hx ↦ (hf' _ hx).differentiableWithinAt) ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0
this : EqOn (deriv f) f' (interior D)
⊢ DifferentiableOn ℝ (deriv f) (interior D)
have refine_1 : DifferentiableOn ℝ f' (interior D)
Tactic: rw [differentiableOn_congr this]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0
this : EqOn (deriv f) f' (interior D)
x : ℝ
hx : x ∈ interior D
⊢ deriv^[2] f x ≤ 0
have h : deriv^[2] f x = f'' x
Tactic: convert! hf''₀ _ hx using 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0
this : EqOn (deriv f) f' (interior D)
x : ℝ
hx : x ∈ interior D
⊢ deriv (deriv f) x = f'' x
have rw : ∀ (y : ℝ) (hy : y ∈ interior D), HasDerivWithinAt (deriv f) (f'' y) (interior D) y
Tactic: rw [deriv_eqOn isOpen_interior (fun y hy ↦ ?_) hx]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0
this : EqOn (deriv f) f' (interior D)
x : ℝ
hx : x ∈ interior D
y : ℝ
hy : y ∈ interior D
⊢ deriv f y = f' y
have rw : f' y = f' y
Tactic: rw [this hy]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf'' : ∀ x ∈ interior D, 0 < deriv^[2] f x
⊢ ∀ x ∈ interior (interior D), 0 < deriv (deriv f) x
have rwa : ∀ x ∈ interior D, 0 < deriv (deriv f) x
Tactic: rwa [interior_interior]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf'' : ∀ x ∈ interior D, deriv^[2] f x < 0
⊢ ∀ x ∈ interior (interior D), deriv (deriv f) x < 0
have rwa : ∀ x ∈ interior D, deriv (deriv f) x < 0
Tactic: rwa [interior_interior]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hfc : ConcaveOn 𝕜 s f
hx : x ∈ s
⊢ AntitoneOn (slope f x) (s \ {x})
have rw : AntitoneOn ((-slope (-f)) x) (s \ {x})
Tactic: rw [← neg_neg f, slope_neg_fun]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ BddBelow (slope f x '' {y : 𝕜 | y ∈ s ∧ x < y})
have obtain : ∀ (y : 𝕜) (hyx : y < x) (hys : y ∈ s), BddBelow (slope f x '' {y : 𝕜 | y ∈ s ∧ x < y})
Tactic: obtain ⟨y, hyx, hys⟩ : ∃ y, y < x ∧ y ∈ s :=
    Eventually.exists_lt (mem_interior_iff_mem_nhds.mp hxs)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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 : y < x
hys : y ∈ s
⊢ BddBelow (slope f x '' {y : 𝕜 | y ∈ s ∧ x < y})
have refine : ∀ y' ∈ slope f x '' {y : 𝕜 | y ∈ s ∧ x < y},
  ∀ (z : 𝕜) (hz : Membership.mem (γ := Set 𝕜) {y : 𝕜 | y ∈ s ∧ x < y} z) (hz' : slope f x z = y'),
    y' ∈ Ici (slope f x y)
Tactic: refine bddBelow_iff_subset_Ici.mpr ⟨slope f x y, fun y' ⟨z, hz, hz'⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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 : y < x
hys : y ∈ s
y' : 𝕜
h : y' ∈ slope f x '' {y : 𝕜 | y ∈ s ∧ x < y}
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {y : 𝕜 | y ∈ s ∧ x < y} z
hz' : slope f x z = y'
⊢ y' ∈ Ici (slope f x y)
have simp_rw : slope f x y ≤ slope f x z
Tactic: simp_rw [mem_Ici, ← hz']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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 : y < x
hys : y ∈ s
y' : 𝕜
h : y' ∈ slope f x '' {y : 𝕜 | y ∈ s ∧ x < y}
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {y : 𝕜 | y ∈ s ∧ x < y} z
hz' : slope f x z = y'
⊢ slope f x y ≤ slope f x z
have refine_1 : y ∈ s \ {x}
Tactic: refine hfc.slope_mono (interior_subset hxs) ?_ ?_ (hyx.trans hz.2).le
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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 : y < x
hys : y ∈ s
y' : 𝕜
h : y' ∈ slope f x '' {y : 𝕜 | y ∈ s ∧ x < y}
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {y : 𝕜 | y ∈ s ∧ x < y} z
hz' : slope f x z = y'
refine_1 : y ∈ s \ {x}
⊢ slope f x y ≤ slope f x z
have refine_2 : z ∈ s \ {x}
Tactic: refine hfc.slope_mono (interior_subset hxs) ?_ ?_ (hyx.trans hz.2).le
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ BddAbove (slope f x '' {y : 𝕜 | y ∈ s ∧ y < x})
have obtain : ∀ (y : 𝕜) (hyx : x < y) (hys : y ∈ s), BddAbove (slope f x '' {y : 𝕜 | y ∈ s ∧ y < x})
Tactic: obtain ⟨y, hyx, hys⟩ : ∃ y, x < y ∧ y ∈ s :=
    Eventually.exists_gt (mem_interior_iff_mem_nhds.mp hxs)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ BddAbove (slope f x '' {y : 𝕜 | y ∈ s ∧ y < x})
have refine : ∀ 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' ∈ Iic (slope f x y)
Tactic: refine bddAbove_iff_subset_Iic.mpr ⟨slope f x y, fun y' ⟨z, hz, hz'⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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' ∈ Iic (slope f x y)
have simp_rw : slope f x z ≤ slope f x y
Tactic: simp_rw [mem_Iic, ← hz']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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'
⊢ slope f x z ≤ slope f x y
have refine_1 : z ∈ s \ {x}
Tactic: refine hfc.slope_mono (interior_subset hxs) ?_ ?_ (hz.2.trans hyx).le
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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}
⊢ slope f x z ≤ slope f x y
have refine_2 : y ∈ s \ {x}
Tactic: refine hfc.slope_mono (interior_subset hxs) ?_ ?_ (hz.2.trans hyx).le
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
Goal:
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
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
⊢ HasDerivWithinAt f (sInf (slope f x '' {y : ℝ | y ∈ S ∧ x < y})) (Ioi x) x
have 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
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
⊢ HasDerivWithinAt f (sInf (slope f x '' {y : ℝ | y ∈ S ∧ x < y})) (Ioi x) x
have simp_rw : Tendsto (slope f x) (𝓝[Ioi x \ {x}] x) (𝓝 (sInf (slope f x '' {y : ℝ | y ∈ S ∧ x < y})))
Tactic: simp_rw [hasDerivWithinAt_iff_tendsto_slope]
-- 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
⊢ Tendsto (slope f x) (𝓝[Ioi x \ {x}] x) (𝓝 (sInf (slope f x '' {y : ℝ | y ∈ S ∧ x < y})))
have simp : Tendsto (slope f 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
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
⊢ Tendsto (slope f x) (𝓝[>] x) (𝓝 (sInf (slope f x '' {y : ℝ | y ∈ S ∧ x < y})))
have h : 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⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
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 '' {y : ℝ | y ∈ S ∧ x < y})))
have h_Ioo : 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))
-- 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
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})))
have suffices : sInf (slope f x '' Ioo x b) = 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]
-- 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
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})
have apply : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) {y : ℝ | y ∈ S ∧ x < y} y → ∃ x_1 ∈ Ioo x b, x_1 ≤ 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 ?_
-- 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
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
have obtain : ∀ (z : ℝ) (hxz : x < z) (hzy : z < min b y), ∃ x_1 ∈ Ioo x b, x_1 ≤ y
Tactic: obtain ⟨z, hxz, hzy⟩ := exists_between (lt_min hxab.2 hxy)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
Goal:
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
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
⊢ HasDerivWithinAt f (sSup (slope f x '' {y : ℝ | y ∈ S ∧ y < x})) (Iio x) x
have 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
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
⊢ HasDerivWithinAt f (sSup (slope f x '' {y : ℝ | y ∈ S ∧ y < x})) (Iio x) x
have simp_rw : Tendsto (slope f x) (𝓝[Iio x \ {x}] x) (𝓝 (sSup (slope f x '' {y : ℝ | y ∈ S ∧ y < x})))
Tactic: simp_rw [hasDerivWithinAt_iff_tendsto_slope]
-- 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
⊢ Tendsto (slope f x) (𝓝[Iio x \ {x}] x) (𝓝 (sSup (slope f x '' {y : ℝ | y ∈ S ∧ y < x})))
have simp : Tendsto (slope f 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
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
⊢ Tendsto (slope f x) (𝓝[<] x) (𝓝 (sSup (slope f x '' {y : ℝ | y ∈ S ∧ y < x})))
have h : 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⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
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 '' {y : ℝ | y ∈ S ∧ y < x})))
have h_Ioo : 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))
-- 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
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})))
have suffices : sSup (slope f x '' Ioo a 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]
-- 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
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})
have apply : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) {y : ℝ | y ∈ S ∧ y < x} y → ∃ x_1 ∈ Ioo a x, y ≤ x_1
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 ?_
-- 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
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
have obtain : ∀ (z : ℝ) (hyz : max a y < z) (hzx : z < x), ∃ x_1 ∈ Ioo a x, y ≤ x_1
Tactic: obtain ⟨z, hyz, hzx⟩ := exists_between (max_lt hxab.1 hyx)
-- 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 (Ioi x) x) x) ((fun (x : ℝ) ↦ derivWithin f (Ioi x) x) y)
have 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)
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 (Ioi x) x) x) ((fun (x : ℝ) ↦ derivWithin f (Ioi x) x) x)
⊢ LE.le (α := ℝ) ((fun (x : ℝ) ↦ derivWithin f (Ioi x) x) x) ((fun (x : ℝ) ↦ derivWithin f (Ioi x) x) y)
have inr : ∀ (hxy : 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
-- 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 (Ioi x) x) x) ((fun (x : ℝ) ↦ derivWithin f (Ioi x) x) y)
have inr : sInf (slope f x '' {y : ℝ | y ∈ S ∧ x < y}) ≤ sInf (slope f y '' {y_1 : ℝ | y_1 ∈ S ∧ y < y_1})
Tactic: simp_rw [hfc.rightDeriv_eq_sInf_slope_of_mem_interior hxs,
    hfc.rightDeriv_eq_sInf_slope_of_mem_interior hys]