awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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, deriv f a < (f y - f x) / (y - x)
neg : ∀ (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)

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, deriv f a < (f y - f x) / (y - x)

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

Premises used: StrictMonoOn.exists_deriv_lt_slope_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, deriv f a < (f y - f x) / (y - x)
⊢ ∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x)

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, deriv f a < (f w - f x) / (w - x)

Tactic:
apply StrictMonoOn.exists_deriv_lt_slope_aux _ hxw _ _

Premises used: StrictMonoOn.exists_deriv_lt_slope_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
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)
⊢ ∃ 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

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 : 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)
apply₂ : ∀ w_1 ∈ Ioo w y, deriv f w_1 ≠ 0
⊢ ∃ b ∈ Ioo w y, deriv f b < (f y - f w) / (y - w)

Tactic:
apply StrictMonoOn.exists_deriv_lt_slope_aux _ hwy _ _

Premises used: StrictMonoOn.exists_deriv_lt_slope_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 : deriv f a < (f w - f x) / (w - x)
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 : deriv f a < (f w - f x) / (w - x)
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 : deriv f a < (f w - f x) / (w - x)
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 : deriv f a < (f w - f x) / (w - x)
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 : deriv f a < (f w - f x) / (w - x)
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 : deriv f a < (f w - f x) / (w - x)
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 : deriv f a < (f w - f x) / (w - x)
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 : deriv f a < (f w - f x) / (w - x)
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 : deriv f a < (f w - f x) / (w - x)
hxa : x < a
haw : a < w
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)
⊢ ∃ 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

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 : 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)

Tactic:
⟨a, ⟨hxa, haw.trans hwy⟩, ?_⟩

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 : 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
neg : deriv f a < (f y - f x) / (y - x)
⊢ ∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x)

Tactic:
refine ⟨a, ⟨hxa, haw.trans hwy⟩, ?_⟩
-- 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 : 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
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
⊢ deriv f a < (f y - f x) / (y - x)

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

Premises used: sub_pos, lt_div_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 : 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
apply₁ : 0 ≤ deriv f b
⊢ deriv f a * (y - w) < deriv f b * (y - w)

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

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 : deriv f a * (w - x) < f w - f x
hb : deriv f b * (y - w) < f y - f 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 : deriv f a * (w - x) < f w - f x
hb : deriv f b * (y - w) < f y - f 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 : deriv f a * (w - x) < f w - f x
hb : deriv f b * (y - w) < f y - f 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 : deriv f a * (w - x) < f w - f x
hb : deriv f b * (y - w) < f y - f 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 : deriv f a * (w - x) < f w - f x
hb : deriv f b * (y - w) < f y - f 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 : 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)

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
-- 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 : 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)
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
⊢ deriv f a * (y - x) < f y - f x

Tactic:
linarith
-- Module: Mathlib.Analysis.Convex.Deriv
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
⊢ Icc x z ⊆ D

Tactic:
have hxzD : Icc x z ⊆ D := hD.ordConnected.out hx hz
-- Module: Mathlib.Analysis.Convex.Deriv
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
⊢ Icc x y ⊆ D

Tactic:
have hxyD : Icc x y ⊆ D := (Icc_subset_Icc_right hyz.le).trans hxzD
-- Module: Mathlib.Analysis.Convex.Deriv
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
⊢ 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⟩
-- Module: Mathlib.Analysis.Convex.Deriv
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
⊢ Icc y z ⊆ D

Tactic:
have hyzD : Icc y z ⊆ D := (Icc_subset_Icc_left hxy.le).trans hxzD
-- Module: Mathlib.Analysis.Convex.Deriv
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
⊢ 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⟩
-- Module: Mathlib.Analysis.Convex.Deriv
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 ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a

Tactic:
StrictMonoOn.exists_slope_lt_deriv (hf.mono hxyD) hxy (hf'.mono hxyD')

Premises used: StrictMonoOn.mono, ContinuousOn.mono, StrictMonoOn.exists_slope_lt_deriv
-- Module: Mathlib.Analysis.Convex.Deriv
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
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)
⊢ (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')

Premises used: HSub.hSub, StrictMonoOn.mono, ContinuousOn.mono, StrictMonoOn.exists_slope_lt_deriv, Set.Ioo
-- Module: Mathlib.Analysis.Convex.Deriv
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 ∈ Ioo y z, deriv f b < (f z - f y) / (z - y)

Tactic:
StrictMonoOn.exists_deriv_lt_slope (hf.mono hyzD) hyz (hf'.mono hyzD')

Premises used: StrictMonoOn.mono, ContinuousOn.mono, StrictMonoOn.exists_deriv_lt_slope
-- Module: Mathlib.Analysis.Convex.Deriv
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
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)
⊢ (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')

Premises used: HSub.hSub, StrictMonoOn.mono, ContinuousOn.mono, StrictMonoOn.exists_deriv_lt_slope, Set.Ioo
-- Module: Mathlib.Analysis.Convex.Deriv
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
apply : deriv f a < deriv f b
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)

Tactic:
apply ha.trans (lt_trans _ hb)

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

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

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

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

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

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

Premises used: StrictAntiOn.neg, deriv.neg
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
f : ℝ → ℝ
hf : Differentiable ℝ f
hf'_mono : Monotone (deriv f)
⊢ ConvexOn ℝ univ f

Tactic:
(hf'_mono.monotoneOn _).convexOn_of_deriv convex_univ hf.continuous.continuousOn
    hf.differentiableOn

Premises used: Continuous.continuousOn, MonotoneOn.convexOn_of_deriv, convex_univ, Differentiable.differentiableOn, Monotone.monotoneOn, Differentiable.continuous
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
f : ℝ → ℝ
hf : Differentiable ℝ f
hf'_anti : Antitone (deriv f)
⊢ ConcaveOn ℝ univ f

Tactic:
(hf'_anti.antitoneOn _).concaveOn_of_deriv convex_univ hf.continuous.continuousOn
    hf.differentiableOn

Premises used: AntitoneOn.concaveOn_of_deriv, Continuous.continuousOn, Antitone.antitoneOn, convex_univ, Differentiable.differentiableOn, Differentiable.continuous
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
f : ℝ → ℝ
hf : Continuous f
hf'_mono : StrictMono (deriv f)
⊢ StrictConvexOn ℝ univ f

Tactic:
(hf'_mono.strictMonoOn _).strictConvexOn_of_deriv convex_univ hf.continuousOn

Premises used: Continuous.continuousOn, StrictMonoOn.strictConvexOn_of_deriv, convex_univ, StrictMono.strictMonoOn
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
f : ℝ → ℝ
hf : Continuous f
hf'_anti : StrictAnti (deriv f)
⊢ StrictConcaveOn ℝ univ f

Tactic:
(hf'_anti.strictAntiOn _).strictConcaveOn_of_deriv convex_univ hf.continuousOn

Premises used: Continuous.continuousOn, StrictAntiOn.strictConcaveOn_of_deriv, convex_univ, StrictAnti.strictAntiOn
-- Module: Mathlib.Analysis.Convex.Deriv
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
rwa rwa₁ rwa₂ rwa₃ : DifferentiableOn ℝ (deriv f) (interior D)
⊢ DifferentiableOn ℝ (deriv f) (interior (interior D))

Tactic:
rwa [interior_interior]

Premises used: interior_interior
-- Module: Mathlib.Analysis.Convex.Deriv
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
rwa rwa₁ rwa₂ rwa₃ : ∀ x ∈ interior D, 0 ≤ deriv (deriv f) x
⊢ ∀ x ∈ interior (interior D), 0 ≤ deriv (deriv f) x

Tactic:
rwa [interior_interior]

Premises used: interior_interior
-- Module: Mathlib.Analysis.Convex.Deriv
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
rwa rwa₁ rwa₂ rwa₃ : DifferentiableOn ℝ (deriv f) (interior D)
⊢ DifferentiableOn ℝ (deriv f) (interior (interior D))

Tactic:
rwa [interior_interior]

Premises used: interior_interior
-- Module: Mathlib.Analysis.Convex.Deriv
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
rwa rwa₁ rwa₂ rwa₃ : ∀ x ∈ interior D, deriv (deriv f) x ≤ 0
⊢ ∀ x ∈ interior (interior D), deriv (deriv f) x ≤ 0

Tactic:
rwa [interior_interior]

Premises used: interior_interior
-- Module: Mathlib.Analysis.Convex.Deriv
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
⊢ EqOn (deriv f) f' (interior D)

Tactic:
have : (interior D).EqOn (deriv f) f' := deriv_eqOn isOpen_interior hf'
-- Module: Mathlib.Analysis.Convex.Deriv
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

Tactic:
convexOn_of_deriv2_nonneg hD hf (fun x hx ↦ (hf' _ hx).differentiableWithinAt) ?_ ?_

Premises used: HasDerivWithinAt.differentiableWithinAt, convexOn_of_deriv2_nonneg
-- Module: Mathlib.Analysis.Convex.Deriv
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)
refine_2 : ∀ x ∈ interior D, 0 ≤ deriv^[2] f x
⊢ ConvexOn ℝ D f

Tactic:
refine convexOn_of_deriv2_nonneg hD hf (fun x hx ↦ (hf' _ hx).differentiableWithinAt) ?_ ?_

Premises used: HasDerivWithinAt.differentiableWithinAt, convexOn_of_deriv2_nonneg