awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
apply : ContinuousOn f (Icc w y)
⊢ ∃ b ∈ Ioo w y, (f y - f w) / (y - w) < deriv f b
have apply₁ : StrictMonoOn (deriv f) (Ioo w y)
Tactic: apply StrictMonoOn.exists_slope_lt_deriv_aux _ hwy _ _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
apply : ContinuousOn f (Icc w y)
apply₁ : StrictMonoOn (deriv f) (Ioo w y)
⊢ ∃ b ∈ Ioo w y, (f y - f w) / (y - w) < deriv f b
have apply₂ : ∀ w_1 ∈ Ioo w y, deriv f w_1 ≠ 0
Tactic: apply StrictMonoOn.exists_slope_lt_deriv_aux _ hwy _ _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
z : ℝ
hz : z ∈ Ioo w y
⊢ deriv f z ≠ 0
have rw : deriv f z ≠ deriv f w
Tactic: rw [← hw]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
z : ℝ
hz : z ∈ Ioo w y
⊢ deriv f z ≠ deriv f w
have h : deriv f w < deriv f z
Tactic: apply ne_of_gt
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
⊢ ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a
have neg : ∀ (b : ℝ) (hb : (f y - f w) / (y - w) < deriv f b) (hwb : w < b) (hby : b < y),
  ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a
Tactic: obtain ⟨b, ⟨hwb, hby⟩, hb⟩ : ∃ b ∈ Ioo w y, (f y - f w) / (y - w) < deriv f b := by
      apply StrictMonoOn.exists_slope_lt_deriv_aux _ hwy _ _
      · refine hf.mono (Icc_subset_Icc hxw.le le_rfl)
      · exact hf'_mono.mono (Ioo_subset_Ioo hxw.le le_rfl)
      · intro z hz
        rw [← hw]
        apply ne_of_gt
        exact hf'_mono ⟨hxw, hwy⟩ ⟨hxw.trans hz.1, hz.2⟩ hz.1
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
b : ℝ
hb : (f y - f w) / (y - w) < deriv f b
hwb : w < b
hby : b < y
⊢ ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a
have neg : (f y - f x) / (y - x) < deriv f b
Tactic: refine ⟨b, ⟨hxw.trans hwb, hby⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
b : ℝ
hb : (f y - f w) / (y - w) < deriv f b
hwb : w < b
hby : b < y
⊢ (f y - f x) / (y - x) < deriv f b
have neg : ∀ (ha : f w - f x < deriv f a * (w - x)) (hb : f y - f w < deriv f b * (y - w)), f y - f x < deriv f b * (y - x)
Tactic: simp only [div_lt_iff₀, hxy, hxw, hwy, sub_pos] at ha hb ⊢
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : f w - f x < deriv f a * (w - x)
hb : f y - f w < deriv f b * (y - w)
⊢ deriv f a * (w - x) < deriv f b * (w - x)
have apply : deriv f a < deriv f b
Tactic: apply mul_lt_mul _ le_rfl (sub_pos.2 hxw) _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : f w - f x < deriv f a * (w - x)
hb : f y - f w < deriv f b * (y - w)
apply : deriv f a < deriv f b
⊢ deriv f a * (w - x) < deriv f b * (w - x)
have apply₁ : 0 ≤ deriv f b
Tactic: apply mul_lt_mul _ le_rfl (sub_pos.2 hxw) _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : f w - f x < deriv f a * (w - x)
hb : f y - f w < deriv f b * (y - w)
⊢ 0 ≤ deriv f b
have rw : deriv f w ≤ deriv f b
Tactic: rw [← hw]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : f w - f x < deriv f a * (w - x)
hb : f y - f w < deriv f b * (y - w)
⊢ f y - f x < deriv f b * (y - x)
have this : deriv f a * (w - x) < deriv f b * (w - x)
Tactic: have : deriv f a * (w - x) < deriv f b * (w - x) := by
      apply mul_lt_mul _ le_rfl (sub_pos.2 hxw) _
      · exact hf'_mono ⟨hxa, haw.trans hwy⟩ ⟨hxw.trans hwb, hby⟩ (haw.trans hwb)
      · rw [← hw]
        exact (hf'_mono ⟨hxw, hwy⟩ ⟨hxw.trans hwb, hby⟩ hwb).le
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : f w - f x < deriv f a * (w - x)
hb : f y - f w < deriv f b * (y - w)
this : deriv f a * (w - x) < deriv f b * (w - x)
⊢ f y - f x < deriv f b * (y - x)
have linarith : deriv f b * (y - x) ≤ f y - f x →
  f w - f x - deriv f a * (w - x) + (f y - f w - deriv f b * (y - w)) + (deriv f a * (w - x) - deriv f b * (w - x)) +
      (deriv f b * (y - x) - (f y - f x)) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
h : ∀ w ∈ Ioo x y, deriv f w ≠ 0
⊢ ∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x)
have A : DifferentiableOn ℝ f (Ioo x y)
Tactic: have A : DifferentiableOn ℝ f (Ioo x y) := fun w wmem =>
    (differentiableAt_of_deriv_ne_zero (h w wmem)).differentiableWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
h : ∀ w ∈ Ioo x y, deriv f w ≠ 0
A : DifferentiableOn ℝ f (Ioo x y)
⊢ ∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x)
have obtain : ∀ (a : ℝ) (ha : deriv f a = (f y - f x) / (y - x)) (hxa : x < a) (hay : a < y),
  ∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x)
Tactic: obtain ⟨a, ⟨hxa, hay⟩, ha⟩ : ∃ a ∈ Ioo x y, deriv f a = (f y - f x) / (y - x) :=
    exists_deriv_eq_slope f hxy hf A
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
h : ∀ w ∈ Ioo x y, deriv f w ≠ 0
A : DifferentiableOn ℝ f (Ioo x y)
a : ℝ
ha : deriv f a = (f y - f x) / (y - x)
hxa : x < a
hay : a < y
⊢ ∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x)
have rcases : ∀ (b : ℝ) (hxb : x < b) (hba : b < a), ∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x)
Tactic: rcases nonempty_Ioo.2 hxa with ⟨b, ⟨hxb, hba⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
h : ∀ w ∈ Ioo x y, deriv f w ≠ 0
A : DifferentiableOn ℝ f (Ioo x y)
a : ℝ
ha : deriv f a = (f y - f x) / (y - x)
hxa : x < a
hay : a < y
b : ℝ
hxb : x < b
hba : b < a
⊢ ∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x)
have refine : deriv f b < (f y - f x) / (y - x)
Tactic: refine ⟨b, ⟨hxb, hba.trans hay⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
h : ∀ w ∈ Ioo x y, deriv f w ≠ 0
A : DifferentiableOn ℝ f (Ioo x y)
a : ℝ
ha : deriv f a = (f y - f x) / (y - x)
hxa : x < a
hay : a < y
b : ℝ
hxb : x < b
hba : b < a
⊢ deriv f b < (f y - f x) / (y - x)
have rw : deriv f b < deriv f a
Tactic: rw [← ha]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
⊢ ∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x)
have pos : ∀ (h : ∀ w ∈ Ioo x y, deriv f w ≠ 0), ∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x)
Tactic: by_cases! h : ∀ w ∈ Ioo x y, deriv f w ≠ 0
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
pos : ∀ (h : ∀ w ∈ Ioo x y, deriv f w ≠ 0), ∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x)
⊢ ∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x)
have neg : ∀ (h : ∃ w ∈ Ioo x y, deriv f w = 0), ∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x)
Tactic: by_cases! h : ∀ w ∈ Ioo x y, deriv f w ≠ 0
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
h : ∃ w ∈ Ioo x y, deriv f w = 0
⊢ ∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x)
have neg : ∀ (w : ℝ) (hw : deriv f w = 0) (hxw : x < w) (hwy : w < y), ∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x)
Tactic: rcases h with ⟨w, ⟨hxw, hwy⟩, hw⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
⊢ ∃ a ∈ Ioo x w, deriv f a < (f w - f x) / (w - x)
have apply : ContinuousOn f (Icc x w)
Tactic: apply StrictMonoOn.exists_deriv_lt_slope_aux _ hxw _ _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
apply : ContinuousOn f (Icc x w)
⊢ ∃ a ∈ Ioo x w, deriv f a < (f w - f x) / (w - x)
have apply₁ : StrictMonoOn (deriv f) (Ioo x w)
Tactic: apply StrictMonoOn.exists_deriv_lt_slope_aux _ hxw _ _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
apply : ContinuousOn f (Icc x w)
apply₁ : StrictMonoOn (deriv f) (Ioo x w)
⊢ ∃ a ∈ Ioo x w, deriv f a < (f w - f x) / (w - x)
have apply₂ : ∀ w_1 ∈ Ioo x w, deriv f w_1 ≠ 0
Tactic: apply StrictMonoOn.exists_deriv_lt_slope_aux _ hxw _ _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
⊢ ∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x)
have neg : ∀ (a : ℝ) (ha : deriv f a < (f w - f x) / (w - x)) (hxa : x < a) (haw : a < w),
  ∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x)
Tactic: obtain ⟨a, ⟨hxa, haw⟩, ha⟩ : ∃ a ∈ Ioo x w, deriv f a < (f w - f x) / (w - x) := by
      apply StrictMonoOn.exists_deriv_lt_slope_aux _ hxw _ _
      · exact hf.mono (Icc_subset_Icc le_rfl hwy.le)
      · exact hf'_mono.mono (Ioo_subset_Ioo le_rfl hwy.le)
      · intro z hz
        rw [← hw]
        apply ne_of_lt
        exact hf'_mono ⟨hz.1, hz.2.trans hwy⟩ ⟨hxw, hwy⟩ hz.2
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : deriv f a < (f w - f x) / (w - x)
hxa : x < a
haw : a < w
⊢ ∃ b ∈ Ioo w y, deriv f b < (f y - f w) / (y - w)
have apply : ContinuousOn f (Icc w y)
Tactic: apply StrictMonoOn.exists_deriv_lt_slope_aux _ hwy _ _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : deriv f a < (f w - f x) / (w - x)
hxa : x < a
haw : a < w
apply : ContinuousOn f (Icc w y)
⊢ ∃ b ∈ Ioo w y, deriv f b < (f y - f w) / (y - w)
have apply₁ : StrictMonoOn (deriv f) (Ioo w y)
Tactic: apply StrictMonoOn.exists_deriv_lt_slope_aux _ hwy _ _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : deriv f a < (f w - f x) / (w - x)
hxa : x < a
haw : a < w
apply : ContinuousOn f (Icc w y)
apply₁ : StrictMonoOn (deriv f) (Ioo w y)
⊢ ∃ b ∈ Ioo w y, deriv f b < (f y - f w) / (y - w)
have apply₂ : ∀ w_1 ∈ Ioo w y, deriv f w_1 ≠ 0
Tactic: apply StrictMonoOn.exists_deriv_lt_slope_aux _ hwy _ _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : deriv f a < (f w - f x) / (w - x)
hxa : x < a
haw : a < w
z : ℝ
hz : z ∈ Ioo w y
⊢ deriv f z ≠ 0
have rw : deriv f z ≠ deriv f w
Tactic: rw [← hw]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : deriv f a < (f w - f x) / (w - x)
hxa : x < a
haw : a < w
z : ℝ
hz : z ∈ Ioo w y
⊢ deriv f z ≠ deriv f w
have h : deriv f w < deriv f z
Tactic: apply ne_of_gt
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : deriv f a < (f w - f x) / (w - x)
hxa : x < a
haw : a < w
⊢ ∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x)
have neg : ∀ (b : ℝ) (hb : deriv f b < (f y - f w) / (y - w)) (hwb : w < b) (hby : b < y),
  ∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x)
Tactic: obtain ⟨b, ⟨hwb, hby⟩, hb⟩ : ∃ b ∈ Ioo w y, deriv f b < (f y - f w) / (y - w) := by
      apply StrictMonoOn.exists_deriv_lt_slope_aux _ hwy _ _
      · refine hf.mono (Icc_subset_Icc hxw.le le_rfl)
      · exact hf'_mono.mono (Ioo_subset_Ioo hxw.le le_rfl)
      · intro z hz
        rw [← hw]
        apply ne_of_gt
        exact hf'_mono ⟨hxw, hwy⟩ ⟨hxw.trans hz.1, hz.2⟩ hz.1
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : deriv f a < (f w - f x) / (w - x)
hxa : x < a
haw : a < w
b : ℝ
hb : deriv f b < (f y - f w) / (y - w)
hwb : w < b
hby : b < y
⊢ ∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x)
have neg : deriv f a < (f y - f x) / (y - x)
Tactic: refine ⟨a, ⟨hxa, haw.trans hwy⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : deriv f a < (f w - f x) / (w - x)
hxa : x < a
haw : a < w
b : ℝ
hb : deriv f b < (f y - f w) / (y - w)
hwb : w < b
hby : b < y
⊢ deriv f a < (f y - f x) / (y - x)
have neg : ∀ (ha : deriv f a * (w - x) < f w - f x) (hb : deriv f b * (y - w) < f y - f w), deriv f a * (y - x) < f y - f x
Tactic: simp only [lt_div_iff₀, hxy, hxw, hwy, sub_pos] at ha hb ⊢
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : deriv f a * (w - x) < f w - f x
hb : deriv f b * (y - w) < f y - f w
⊢ deriv f a * (y - w) < deriv f b * (y - w)
have apply : deriv f a < deriv f b
Tactic: apply mul_lt_mul _ le_rfl (sub_pos.2 hwy) _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : deriv f a * (w - x) < f w - f x
hb : deriv f b * (y - w) < f y - f w
apply : deriv f a < deriv f b
⊢ deriv f a * (y - w) < deriv f b * (y - w)
have apply₁ : 0 ≤ deriv f b
Tactic: apply mul_lt_mul _ le_rfl (sub_pos.2 hwy) _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : deriv f a * (w - x) < f w - f x
hb : deriv f b * (y - w) < f y - f w
⊢ 0 ≤ deriv f b
have rw : deriv f w ≤ deriv f b
Tactic: rw [← hw]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : deriv f a * (w - x) < f w - f x
hb : deriv f b * (y - w) < f y - f w
⊢ deriv f a * (y - x) < f y - f x
have this : deriv f a * (y - w) < deriv f b * (y - w)
Tactic: have : deriv f a * (y - w) < deriv f b * (y - w) := by
      apply mul_lt_mul _ le_rfl (sub_pos.2 hwy) _
      · exact hf'_mono ⟨hxa, haw.trans hwy⟩ ⟨hxw.trans hwb, hby⟩ (haw.trans hwb)
      · rw [← hw]
        exact (hf'_mono ⟨hxw, hwy⟩ ⟨hxw.trans hwb, hby⟩ hwb).le
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : deriv f a * (w - x) < f w - f x
hb : deriv f b * (y - w) < f y - f w
this : deriv f a * (y - w) < deriv f b * (y - w)
⊢ deriv f a * (y - x) < f y - f x
have linarith : f y - f x ≤ deriv f a * (y - x) →
  deriv f a * (w - x) - (f w - f x) + (deriv f b * (y - w) - (f y - f w)) +
        (deriv f a * (y - w) - deriv f b * (y - w)) +
      (f y - f x - deriv f a * (y - x)) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : StrictMonoOn (deriv f) (interior D)
x y z : ℝ
hx : x ∈ D
hz : z ∈ D
hxy : x < y
hyz : y < z
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)
have hxzD : Icc x z ⊆ D
Tactic: have hxzD : Icc x z ⊆ D := hD.ordConnected.out hx hz
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : StrictMonoOn (deriv f) (interior D)
x y z : ℝ
hx : x ∈ D
hz : z ∈ D
hxy : x < y
hyz : y < z
hxzD : Icc x z ⊆ D
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)
have hxyD : Icc x y ⊆ D
Tactic: have hxyD : Icc x y ⊆ D := (Icc_subset_Icc_right hyz.le).trans hxzD
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : StrictMonoOn (deriv f) (interior D)
x y z : ℝ
hx : x ∈ D
hz : z ∈ D
hxy : x < y
hyz : y < z
hxzD : Icc x z ⊆ D
hxyD : Icc x y ⊆ D
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)
have hxyD' : Ioo x y ⊆ interior D
Tactic: have hxyD' : Ioo x y ⊆ interior D :=
      subset_sUnion_of_mem ⟨isOpen_Ioo, Ioo_subset_Icc_self.trans hxyD⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : StrictMonoOn (deriv f) (interior D)
x y z : ℝ
hx : x ∈ D
hz : z ∈ D
hxy : x < y
hyz : y < z
hxzD : Icc x z ⊆ D
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)
have hyzD : Icc y z ⊆ D
Tactic: have hyzD : Icc y z ⊆ D := (Icc_subset_Icc_left hxy.le).trans hxzD
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : StrictMonoOn (deriv f) (interior D)
x y z : ℝ
hx : x ∈ D
hz : z ∈ D
hxy : x < y
hyz : y < z
hxzD : Icc x z ⊆ D
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
hyzD : Icc y z ⊆ D
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)
have hyzD' : Ioo y z ⊆ interior D
Tactic: have hyzD' : Ioo y z ⊆ interior D :=
      subset_sUnion_of_mem ⟨isOpen_Ioo, Ioo_subset_Icc_self.trans hyzD⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : StrictMonoOn (deriv f) (interior D)
x y z : ℝ
hx : x ∈ D
hz : z ∈ D
hxy : x < y
hyz : y < z
hxzD : Icc x z ⊆ D
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
hyzD : Icc y z ⊆ D
hyzD' : Ioo y z ⊆ interior D
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)
have obtain : ∀ (a : ℝ) (ha : (f y - f x) / (y - x) < deriv f a) (hxa : x < a) (hay : a < y),
  (f y - f x) / (y - x) < (f z - f y) / (z - y)
Tactic: obtain ⟨a, ⟨hxa, hay⟩, ha⟩ : ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a :=
      StrictMonoOn.exists_slope_lt_deriv (hf.mono hxyD) hxy (hf'.mono hxyD')
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : StrictMonoOn (deriv f) (interior D)
x y z : ℝ
hx : x ∈ D
hz : z ∈ D
hxy : x < y
hyz : y < z
hxzD : Icc x z ⊆ D
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
hyzD : Icc y z ⊆ D
hyzD' : Ioo y z ⊆ interior D
a : ℝ
ha : (f y - f x) / (y - x) < deriv f a
hxa : x < a
hay : a < y
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)
have obtain : ∀ (b : ℝ) (hb : deriv f b < (f z - f y) / (z - y)) (hyb : y < b) (hbz : b < z),
  (f y - f x) / (y - x) < (f z - f y) / (z - y)
Tactic: obtain ⟨b, ⟨hyb, hbz⟩, hb⟩ : ∃ b ∈ Ioo y z, deriv f b < (f z - f y) / (z - y) :=
      StrictMonoOn.exists_deriv_lt_slope (hf.mono hyzD) hyz (hf'.mono hyzD')
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : StrictMonoOn (deriv f) (interior D)
x y z : ℝ
hx : x ∈ D
hz : z ∈ D
hxy : x < y
hyz : y < z
hxzD : Icc x z ⊆ D
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
hyzD : Icc y z ⊆ D
hyzD' : Ioo y z ⊆ interior D
a : ℝ
ha : (f y - f x) / (y - x) < deriv f a
hxa : x < a
hay : a < y
b : ℝ
hb : deriv f b < (f z - f y) / (z - y)
hyb : y < b
hbz : b < z
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)
have apply : deriv f a < deriv f b
Tactic: apply ha.trans (lt_trans _ hb)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'' : DifferentiableOn ℝ (deriv f) (interior D)
hf''_nonneg : ∀ 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' : DifferentiableOn ℝ f (interior D)
hf'' : DifferentiableOn ℝ (deriv f) (interior D)
hf''_nonpos : ∀ 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]