awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'_mono : MonotoneOn (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 : deriv f a = (f y - f x) / (y - x)
hxa : x < a
hay : a < y
b : ℝ
hb : deriv f b = (f z - f y) / (z - y)
hyb : y < b
hbz : b < z
⊢ deriv f a ≤ deriv f b

Tactic:
exact hf'_mono (hxyD' ⟨hxa, hay⟩) (hyzD' ⟨hyb, hbz⟩) (hay.trans hyb).le

Premises used: LT.lt.le, And.intro, LT.lt.trans
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
h_anti : AntitoneOn (deriv f) (interior D)
⊢ MonotoneOn (deriv (-f)) (interior D)

Tactic:
simpa only [← deriv.neg] using h_anti.neg

Premises used: AntitoneOn.neg, deriv.neg
-- Module: Mathlib.Analysis.Convex.Deriv
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
⊢ 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
-- Module: Mathlib.Analysis.Convex.Deriv
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)

Tactic:
exists_deriv_eq_slope f hxy hf A

Premises used: exists_deriv_eq_slope
-- Module: Mathlib.Analysis.Convex.Deriv
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)
obtain :
  ∀ (a : ℝ) (ha : deriv f a = (f y - f x) / (y - x)) (hxa : x < a) (hay : a < y),
    ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a
⊢ ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a

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

Premises used: HSub.hSub, exists_deriv_eq_slope, Set.Ioo
-- Module: Mathlib.Analysis.Convex.Deriv
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
rcases : ∀ (b : ℝ) (hab : a < b) (hby : b < y), ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a
⊢ ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a

Tactic:
rcases nonempty_Ioo.2 hay with ⟨b, ⟨hab, hby⟩⟩

Premises used: Iff.mpr, Set.nonempty_Ioo
-- Module: Mathlib.Analysis.Convex.Deriv
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 : ℝ
hab : a < b
hby : b < y
⊢ ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a

Tactic:
⟨b, ⟨hxa.trans hab, hby⟩, ?_⟩

Premises used: And.intro, Exists.intro, LT.lt.trans
-- Module: Mathlib.Analysis.Convex.Deriv
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 : ℝ
hab : a < b
hby : b < y
refine : (f y - f x) / (y - x) < deriv f b
⊢ ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a

Tactic:
refine ⟨b, ⟨hxa.trans hab, hby⟩, ?_⟩
-- Module: Mathlib.Analysis.Convex.Deriv
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 : ℝ
hab : a < b
hby : b < y
rw : deriv f a < deriv f b
⊢ (f y - f x) / (y - x) < deriv f b

Tactic:
rw [← ha]
-- Module: Mathlib.Analysis.Convex.Deriv
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 : ℝ
hab : a < b
hby : b < y
⊢ deriv f a < deriv f b

Tactic:
hf'_mono ⟨hxa, hay⟩ ⟨hxa.trans hab, hby⟩ hab

Premises used: And.intro, LT.lt.trans
-- Module: Mathlib.Analysis.Convex.Deriv
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 : ℝ
hab : a < b
hby : b < y
⊢ deriv f a < deriv f b

Tactic:
exact hf'_mono ⟨hxa, hay⟩ ⟨hxa.trans hab, hby⟩ hab

Premises used: And.intro, LT.lt.trans
-- Module: Mathlib.Analysis.Convex.Deriv
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, (f y - f x) / (y - x) < deriv f a
neg : ∀ (h : ∃ w ∈ Ioo x y, deriv f w = 0), ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a
⊢ ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a

Tactic:
by_cases! h : ∀ w ∈ Ioo x y, deriv f w ≠ 0

Premises used: Set.Ioo
-- Module: Mathlib.Analysis.Convex.Deriv
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, (f y - f x) / (y - x) < deriv f a

Tactic:
apply StrictMonoOn.exists_slope_lt_deriv_aux hf hxy hf'_mono h

Premises used: StrictMonoOn.exists_slope_lt_deriv_aux
-- Module: Mathlib.Analysis.Convex.Deriv
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
neg : ∀ (w : ℝ) (hw : deriv f w = 0) (hxw : x < w) (hwy : w < y), ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a
⊢ ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a

Tactic:
rcases h with ⟨w, ⟨hxw, hwy⟩, hw⟩
-- Module: Mathlib.Analysis.Convex.Deriv
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)
apply₂ : ∀ w_1 ∈ Ioo x w, deriv f w_1 ≠ 0
⊢ ∃ a ∈ Ioo x w, (f w - f x) / (w - x) < deriv f a

Tactic:
apply StrictMonoOn.exists_slope_lt_deriv_aux _ hxw _ _

Premises used: StrictMonoOn.exists_slope_lt_deriv_aux
-- Module: Mathlib.Analysis.Convex.Deriv
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
⊢ ContinuousOn f (Icc x w)

Tactic:
hf.mono (Icc_subset_Icc le_rfl hwy.le)

Premises used: le_rfl, LT.lt.le, Set.Icc_subset_Icc, ContinuousOn.mono
-- Module: Mathlib.Analysis.Convex.Deriv
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
⊢ ContinuousOn f (Icc x w)

Tactic:
exact hf.mono (Icc_subset_Icc le_rfl hwy.le)

Premises used: le_rfl, LT.lt.le, Set.Icc_subset_Icc, ContinuousOn.mono
-- Module: Mathlib.Analysis.Convex.Deriv
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
⊢ StrictMonoOn (deriv f) (Ioo x w)

Tactic:
hf'_mono.mono (Ioo_subset_Ioo le_rfl hwy.le)

Premises used: le_rfl, StrictMonoOn.mono, LT.lt.le, Set.Ioo_subset_Ioo
-- Module: Mathlib.Analysis.Convex.Deriv
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
⊢ StrictMonoOn (deriv f) (Ioo x w)

Tactic:
exact hf'_mono.mono (Ioo_subset_Ioo le_rfl hwy.le)

Premises used: le_rfl, StrictMonoOn.mono, LT.lt.le, Set.Ioo_subset_Ioo
-- Module: Mathlib.Analysis.Convex.Deriv
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
z : ℝ
hz : z ∈ Ioo x w
rw : deriv f z ≠ deriv f w
⊢ deriv f z ≠ 0

Tactic:
rw [← hw]
-- Module: Mathlib.Analysis.Convex.Deriv
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
z : ℝ
hz : z ∈ Ioo x w
h : deriv f z < deriv f w
⊢ deriv f z ≠ deriv f w

Tactic:
apply ne_of_lt

Premises used: ne_of_lt
-- Module: Mathlib.Analysis.Convex.Deriv
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
z : ℝ
hz : z ∈ Ioo x w
⊢ deriv f z < deriv f w

Tactic:
hf'_mono ⟨hz.1, hz.2.trans hwy⟩ ⟨hxw, hwy⟩ hz.2

Premises used: And.right, And.left, And.intro, LT.lt.trans
-- Module: Mathlib.Analysis.Convex.Deriv
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
z : ℝ
hz : z ∈ Ioo x w
⊢ deriv f z < deriv f w

Tactic:
exact hf'_mono ⟨hz.1, hz.2.trans hwy⟩ ⟨hxw, hwy⟩ hz.2

Premises used: And.right, And.left, And.intro, LT.lt.trans
-- Module: Mathlib.Analysis.Convex.Deriv
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
neg :
  ∀ (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
⊢ ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a

Tactic:
obtain ⟨a, ⟨hxa, haw⟩, ha⟩ : ∃ a ∈ Ioo x w, (f w - f x) / (w - x) < deriv f a := by
      apply StrictMonoOn.exists_slope_lt_deriv_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

Premises used: HSub.hSub, Set.Ioo
-- Module: Mathlib.Analysis.Convex.Deriv
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)
apply₂ : ∀ w_1 ∈ Ioo w y, deriv f w_1 ≠ 0
⊢ ∃ b ∈ Ioo w y, (f y - f w) / (y - w) < deriv f b

Tactic:
apply StrictMonoOn.exists_slope_lt_deriv_aux _ hwy _ _

Premises used: StrictMonoOn.exists_slope_lt_deriv_aux
-- Module: Mathlib.Analysis.Convex.Deriv
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
⊢ ContinuousOn f (Icc w y)

Tactic:
hf.mono (Icc_subset_Icc hxw.le le_rfl)

Premises used: le_rfl, LT.lt.le, Set.Icc_subset_Icc, ContinuousOn.mono
-- Module: Mathlib.Analysis.Convex.Deriv
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
⊢ ContinuousOn f (Icc w y)

Tactic:
refine hf.mono (Icc_subset_Icc hxw.le le_rfl)

Premises used: le_rfl, LT.lt.le, Set.Icc_subset_Icc, ContinuousOn.mono
-- Module: Mathlib.Analysis.Convex.Deriv
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
⊢ StrictMonoOn (deriv f) (Ioo w y)

Tactic:
hf'_mono.mono (Ioo_subset_Ioo hxw.le le_rfl)

Premises used: le_rfl, StrictMonoOn.mono, LT.lt.le, Set.Ioo_subset_Ioo
-- Module: Mathlib.Analysis.Convex.Deriv
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
⊢ StrictMonoOn (deriv f) (Ioo w y)

Tactic:
exact hf'_mono.mono (Ioo_subset_Ioo hxw.le le_rfl)

Premises used: le_rfl, StrictMonoOn.mono, LT.lt.le, Set.Ioo_subset_Ioo
-- Module: Mathlib.Analysis.Convex.Deriv
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
rw : deriv f z ≠ deriv f w
⊢ deriv f z ≠ 0

Tactic:
rw [← hw]
-- Module: Mathlib.Analysis.Convex.Deriv
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
h : deriv f w < deriv f z
⊢ deriv f z ≠ deriv f w

Tactic:
apply ne_of_gt

Premises used: ne_of_gt
-- Module: Mathlib.Analysis.Convex.Deriv
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 w < deriv f z

Tactic:
hf'_mono ⟨hxw, hwy⟩ ⟨hxw.trans hz.1, hz.2⟩ hz.1

Premises used: And.right, And.left, And.intro, LT.lt.trans
-- Module: Mathlib.Analysis.Convex.Deriv
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 w < deriv f z

Tactic:
exact hf'_mono ⟨hxw, hwy⟩ ⟨hxw.trans hz.1, hz.2⟩ hz.1

Premises used: And.right, And.left, And.intro, LT.lt.trans
-- Module: Mathlib.Analysis.Convex.Deriv
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
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
⊢ ∃ 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

Premises used: HSub.hSub, Set.Ioo
-- Module: Mathlib.Analysis.Convex.Deriv
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

Tactic:
⟨b, ⟨hxw.trans hwb, hby⟩, ?_⟩

Premises used: And.intro, Exists.intro, LT.lt.trans
-- Module: Mathlib.Analysis.Convex.Deriv
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
neg : (f y - f x) / (y - x) < deriv f b
⊢ ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a

Tactic:
refine ⟨b, ⟨hxw.trans hwb, hby⟩, ?_⟩
-- Module: Mathlib.Analysis.Convex.Deriv
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
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)
⊢ (f y - f x) / (y - x) < deriv f b

Tactic:
simp only [div_lt_iff₀, hxy, hxw, hwy, sub_pos] at ha hb ⊢

Premises used: sub_pos, div_lt_iff₀
-- Module: Mathlib.Analysis.Convex.Deriv
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
apply₁ : 0 ≤ deriv f b
⊢ deriv f a * (w - x) < deriv f b * (w - x)

Tactic:
apply mul_lt_mul _ le_rfl (sub_pos.2 hxw) _

Premises used: Iff.mpr, sub_pos, le_rfl, mul_lt_mul
-- Module: Mathlib.Analysis.Convex.Deriv
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 < deriv f b

Tactic:
hf'_mono ⟨hxa, haw.trans hwy⟩ ⟨hxw.trans hwb, hby⟩ (haw.trans hwb)

Premises used: And.intro, LT.lt.trans
-- Module: Mathlib.Analysis.Convex.Deriv
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 < deriv f b

Tactic:
exact hf'_mono ⟨hxa, haw.trans hwy⟩ ⟨hxw.trans hwb, hby⟩ (haw.trans hwb)

Premises used: And.intro, LT.lt.trans
-- Module: Mathlib.Analysis.Convex.Deriv
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)
rw : deriv f w ≤ deriv f b
⊢ 0 ≤ deriv f b

Tactic:
rw [← hw]
-- Module: Mathlib.Analysis.Convex.Deriv
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 w ≤ deriv f b

Tactic:
(hf'_mono ⟨hxw, hwy⟩ ⟨hxw.trans hwb, hby⟩ hwb).le

Premises used: LT.lt.le, And.intro, LT.lt.trans
-- Module: Mathlib.Analysis.Convex.Deriv
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 w ≤ deriv f b

Tactic:
exact (hf'_mono ⟨hxw, hwy⟩ ⟨hxw.trans hwb, hby⟩ hwb).le

Premises used: LT.lt.le, And.intro, LT.lt.trans
-- Module: Mathlib.Analysis.Convex.Deriv
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)

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
-- Module: Mathlib.Analysis.Convex.Deriv
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)
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
⊢ f y - f x < deriv f b * (y - x)

Tactic:
linarith
-- Module: Mathlib.Analysis.Convex.Deriv
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)
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)
⊢ ∃ 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

Premises used: HSub.hSub, exists_deriv_eq_slope, Set.Ioo
-- Module: Mathlib.Analysis.Convex.Deriv
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
rcases : ∀ (b : ℝ) (hxb : x < b) (hba : b < a), ∃ 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)

Tactic:
rcases nonempty_Ioo.2 hxa with ⟨b, ⟨hxb, hba⟩⟩

Premises used: Iff.mpr, Set.nonempty_Ioo
-- Module: Mathlib.Analysis.Convex.Deriv
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)

Tactic:
⟨b, ⟨hxb, hba.trans hay⟩, ?_⟩

Premises used: And.intro, Exists.intro, LT.lt.trans
-- Module: Mathlib.Analysis.Convex.Deriv
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
refine : deriv f b < (f y - f x) / (y - x)
⊢ ∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x)

Tactic:
refine ⟨b, ⟨hxb, hba.trans hay⟩, ?_⟩
-- Module: Mathlib.Analysis.Convex.Deriv
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
rw : deriv f b < deriv f a
⊢ deriv f b < (f y - f x) / (y - x)

Tactic:
rw [← ha]
-- Module: Mathlib.Analysis.Convex.Deriv
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 < deriv f a

Tactic:
hf'_mono ⟨hxb, hba.trans hay⟩ ⟨hxa, hay⟩ hba

Premises used: And.intro, LT.lt.trans
-- Module: Mathlib.Analysis.Convex.Deriv
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 < deriv f a

Tactic:
exact hf'_mono ⟨hxb, hba.trans hay⟩ ⟨hxa, hay⟩ hba

Premises used: And.intro, LT.lt.trans