awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x ≤ y
hxy' : x < y
⊢ deriv f x ≤ deriv f y

Tactic:
(hfc.deriv_le_slope hx hy hxy' (hfd x hx)).trans (hfc.slope_le_deriv hx hy hxy' (hfd y hy))

Premises used: ConvexOn.slope_le_deriv, ConvexOn.deriv_le_slope, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x ≤ y
hxy' : x < y
⊢ deriv f x ≤ deriv f y

Tactic:
exact (hfc.deriv_le_slope hx hy hxy' (hfd x hx)).trans (hfc.slope_le_deriv hx hy hxy' (hfd y hy))

Premises used: ConvexOn.slope_le_deriv, ConvexOn.deriv_le_slope, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
inl : ∀ (hxy : x < y), Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ f x ≤ f x_2) x_1} y
inr : ∀ (h_eq : x = y), Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ f x ≤ f x_2) x_1} y
inr₁ : ∀ (hyx : y < x), Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ f x ≤ f x_2) x_1} y
⊢ Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ f x ≤ f x_2) x_1} y

Tactic:
rcases lt_trichotomy x y with hxy | h_eq | hyx

Premises used: lt_trichotomy
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
hxy : x < y
this : 0 ≤ slope f x y
⊢ f x ≤ f y ∧ x ≤ y

Tactic:
simp only [slope_def_field, div_nonneg_iff, sub_nonneg, tsub_le_iff_right, zero_add,
        not_le.mpr hxy, and_false, or_false] at this

Premises used: not_le, Iff.mpr, zero_add, tsub_le_iff_right, slope_def_field, div_nonneg_iff, or_false, and_false, sub_nonneg
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
hxy : x < y
this : f x ≤ f y ∧ x ≤ y
⊢ Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ f x ≤ f x_2) x_1} y

Tactic:
this.1

Premises used: Set.Mem, setOf, And.left
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
hxy : x < y
this : f x ≤ f y ∧ x ≤ y
⊢ Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ f x ≤ f x_2) x_1} y

Tactic:
exact this.1

Premises used: And.left
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
hxy : x < y
inl : 0 ≤ slope f x y
⊢ Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ f x ≤ f x_2) x_1} y

Tactic:
suffices 0 ≤ slope f x y by
      simp only [slope_def_field, div_nonneg_iff, sub_nonneg, tsub_le_iff_right, zero_add,
        not_le.mpr hxy, and_false, or_false] at this
      exact this.1
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ 0 ≤ slope f x y

Tactic:
hf_rd.trans <| rightDeriv_le_slope_of_mem_interior hf hx hy hxy

Premises used: ConvexOn.rightDeriv_le_slope_of_mem_interior, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ 0 ≤ slope f x y

Tactic:
exact hf_rd.trans <| rightDeriv_le_slope_of_mem_interior hf hx hy hxy

Premises used: ConvexOn.rightDeriv_le_slope_of_mem_interior, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
h_eq : x = y
⊢ Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ f x ≤ f x_2) x_1} y

Tactic:
simp [h_eq]
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
hyx : y < x
this : slope f x y ≤ 0
⊢ f x ≤ f y ∧ y ≤ x

Tactic:
simp only [slope_def_field, div_nonpos_iff, sub_nonneg, tsub_le_iff_right, zero_add,
        not_le.mpr hyx, and_false, or_false] at this

Premises used: not_le, Iff.mpr, div_nonpos_iff, zero_add, tsub_le_iff_right, slope_def_field, or_false, and_false, sub_nonneg
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
hyx : y < x
this : f x ≤ f y ∧ y ≤ x
⊢ Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ f x ≤ f x_2) x_1} y

Tactic:
this.1

Premises used: Set.Mem, setOf, And.left
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
hyx : y < x
this : f x ≤ f y ∧ y ≤ x
⊢ Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ f x ≤ f x_2) x_1} y

Tactic:
exact this.1

Premises used: And.left
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
hyx : y < x
inr : slope f x y ≤ 0
⊢ Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ f x ≤ f x_2) x_1} y

Tactic:
suffices slope f x y ≤ 0 by
      simp only [slope_def_field, div_nonpos_iff, sub_nonneg, tsub_le_iff_right, zero_add,
        not_le.mpr hyx, and_false, or_false] at this
      exact this.1
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
hyx : y < x
inr : slope f y x ≤ 0
⊢ slope f x y ≤ 0

Tactic:
rw [slope_comm]

Premises used: slope_comm
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
hyx : y < x
⊢ slope f y x ≤ 0

Tactic:
(slope_le_leftDeriv_of_mem_interior hf hy hx hyx).trans hf_ld

Premises used: LE.le.trans, ConvexOn.slope_le_leftDeriv_of_mem_interior
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
hyx : y < x
⊢ slope f y x ≤ 0

Tactic:
exact (slope_le_leftDeriv_of_mem_interior hf hy hx hyx).trans hf_ld

Premises used: LE.le.trans, ConvexOn.slope_le_leftDeriv_of_mem_interior
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_rd : derivWithin f (Ioi x) x = 0
⊢ IsMinOn f S x

Tactic:
hf.isMinOn_of_leftDeriv_nonpos_of_rightDeriv_nonneg hx ?_ hf_rd.symm.le

Premises used: Eq.le, ConvexOn.isMinOn_of_leftDeriv_nonpos_of_rightDeriv_nonneg, Eq.symm
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_rd : derivWithin f (Ioi x) x = 0
refine : derivWithin f (Iio x) x ≤ 0
⊢ IsMinOn f S x

Tactic:
refine hf.isMinOn_of_leftDeriv_nonpos_of_rightDeriv_nonneg hx ?_ hf_rd.symm.le

Premises used: Eq.le, ConvexOn.isMinOn_of_leftDeriv_nonpos_of_rightDeriv_nonneg, Eq.symm
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_rd : derivWithin f (Ioi x) x = 0
⊢ derivWithin f (Iio x) x ≤ 0

Tactic:
(hf.leftDeriv_le_rightDeriv_of_mem_interior hx).trans_eq hf_rd

Premises used: ConvexOn.leftDeriv_le_rightDeriv_of_mem_interior, LE.le.trans_eq
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_rd : derivWithin f (Ioi x) x = 0
⊢ derivWithin f (Iio x) x ≤ 0

Tactic:
exact (hf.leftDeriv_le_rightDeriv_of_mem_interior hx).trans_eq hf_rd

Premises used: ConvexOn.leftDeriv_le_rightDeriv_of_mem_interior, LE.le.trans_eq
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x = 0
⊢ IsMinOn f S x

Tactic:
hf.isMinOn_of_leftDeriv_nonpos_of_rightDeriv_nonneg hx hf_ld.le ?_

Premises used: Eq.le, ConvexOn.isMinOn_of_leftDeriv_nonpos_of_rightDeriv_nonneg
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x = 0
refine : 0 ≤ derivWithin f (Ioi x) x
⊢ IsMinOn f S x

Tactic:
refine hf.isMinOn_of_leftDeriv_nonpos_of_rightDeriv_nonneg hx hf_ld.le ?_

Premises used: Eq.le, ConvexOn.isMinOn_of_leftDeriv_nonpos_of_rightDeriv_nonneg
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x = 0
⊢ 0 ≤ derivWithin f (Ioi x) x

Tactic:
hf_ld.symm.le.trans (hf.leftDeriv_le_rightDeriv_of_mem_interior hx)

Premises used: ConvexOn.leftDeriv_le_rightDeriv_of_mem_interior, Eq.le, LE.le.trans, Eq.symm
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x = 0
⊢ 0 ≤ derivWithin f (Ioi x) x

Tactic:
exact hf_ld.symm.le.trans (hf.leftDeriv_le_rightDeriv_of_mem_interior hx)

Premises used: ConvexOn.leftDeriv_le_rightDeriv_of_mem_interior, Eq.le, LE.le.trans, Eq.symm
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
obtain : ∀ (u : ℝ) (hxu : x < u) (huy : u < y), f' < slope f x y
⊢ f' < slope f x y

Tactic:
obtain ⟨u, hxu, huy⟩ := exists_between hxy

Premises used: exists_between
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
u : ℝ
hxu : x < u
huy : u < y
⊢ u ∈ S

Tactic:
have hu : u ∈ S := hfc.1.ordConnected.out hx hy ⟨hxu.le, huy.le⟩
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
u : ℝ
hxu : x < u
huy : u < y
hu : u ∈ S
⊢ (f u - f x) / (u - x) < (f y - f x) / (y - x)

Tactic:
have := hfc.secant_strict_mono hx hu hy hxu.ne' hxy.ne' huy
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
u : ℝ
hxu : x < u
huy : u < y
hu : u ∈ S
this : (f u - f x) / (u - x) < (f y - f x) / (y - x)
⊢ slope f x u < slope f x y

Tactic:
simp only [← slope_def_field] at this

Premises used: slope_def_field
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
u : ℝ
hxu : x < u
huy : u < y
hu : u ∈ S
this : slope f x u < slope f x y
⊢ f' < slope f x y

Tactic:
(hfc.convexOn.le_slope_of_hasDerivWithinAt_Ioi hx hu hxu hf').trans_lt this

Premises used: ConvexOn.le_slope_of_hasDerivWithinAt_Ioi, StrictConvexOn.convexOn, LE.le.trans_lt
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
u : ℝ
hxu : x < u
huy : u < y
hu : u ∈ S
this : slope f x u < slope f x y
⊢ f' < slope f x y

Tactic:
exact (hfc.convexOn.le_slope_of_hasDerivWithinAt_Ioi hx hu hxu hf').trans_lt this

Premises used: ConvexOn.le_slope_of_hasDerivWithinAt_Ioi, StrictConvexOn.convexOn, LE.le.trans_lt
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : DifferentiableWithinAt ℝ f (Ioi x) x
⊢ derivWithin f (Ioi x) x < slope f x y

Tactic:
hfc.lt_slope_of_hasDerivWithinAt_Ioi hx hy hxy hfd.hasDerivWithinAt

Premises used: DifferentiableWithinAt.hasDerivWithinAt, StrictConvexOn.lt_slope_of_hasDerivWithinAt_Ioi
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' S x
⊢ f' < slope f x y

Tactic:
hfc.lt_slope_of_hasDerivWithinAt_Ioi hx hy hxy <|
    hf'.mono_of_mem_nhdsWithin <| hfc.1.ordConnected.mem_nhdsGT hx hy hxy

Premises used: Set.OrdConnected.mem_nhdsGT, HasDerivWithinAt.mono_of_mem_nhdsWithin, And.left, StrictConvexOn.lt_slope_of_hasDerivWithinAt_Ioi, Convex.ordConnected
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : DifferentiableWithinAt ℝ f S x
⊢ derivWithin f S x < slope f x y

Tactic:
hfc.lt_slope_of_hasDerivWithinAt hx hy hxy hfd.hasDerivWithinAt

Premises used: DifferentiableWithinAt.hasDerivWithinAt, StrictConvexOn.lt_slope_of_hasDerivWithinAt
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivAt f f' x
⊢ f' < slope f x y

Tactic:
hfc.lt_slope_of_hasDerivWithinAt_Ioi hx hy hxy hf'.hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, StrictConvexOn.lt_slope_of_hasDerivWithinAt_Ioi
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : DifferentiableAt ℝ f x
⊢ deriv f x < slope f x y

Tactic:
hfc.lt_slope_of_hasDerivAt hx hy hxy hfd.hasDerivAt

Premises used: DifferentiableAt.hasDerivAt, StrictConvexOn.lt_slope_of_hasDerivAt
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
obtain : ∀ (u : ℝ) (hxu : x < u) (huy : u < y), slope f x y < f'
⊢ slope f x y < f'

Tactic:
obtain ⟨u, hxu, huy⟩ := exists_between hxy

Premises used: exists_between
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
u : ℝ
hxu : x < u
huy : u < y
⊢ u ∈ S

Tactic:
have hu : u ∈ S := hfc.1.ordConnected.out hx hy ⟨hxu.le, huy.le⟩
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
u : ℝ
hxu : x < u
huy : u < y
hu : u ∈ S
⊢ (f x - f y) / (x - y) < (f u - f y) / (u - y)

Tactic:
have := hfc.secant_strict_mono hy hx hu hxy.ne huy.ne hxu
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
u : ℝ
hxu : x < u
huy : u < y
hu : u ∈ S
this : (f x - f y) / (x - y) < (f u - f y) / (u - y)
⊢ slope f x y < slope f u y

Tactic:
simp_rw [← slope_def_field, slope_comm _ y] at this

Premises used: slope_comm, slope_def_field
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
u : ℝ
hxu : x < u
huy : u < y
hu : u ∈ S
this : slope f x y < slope f u y
⊢ slope f x y < f'

Tactic:
this.trans_le <| hfc.convexOn.slope_le_of_hasDerivWithinAt_Iio hu hy huy hf'

Premises used: LT.lt.trans_le, StrictConvexOn.convexOn, ConvexOn.slope_le_of_hasDerivWithinAt_Iio
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
u : ℝ
hxu : x < u
huy : u < y
hu : u ∈ S
this : slope f x y < slope f u y
⊢ slope f x y < f'

Tactic:
exact this.trans_le <| hfc.convexOn.slope_le_of_hasDerivWithinAt_Iio hu hy huy hf'

Premises used: LT.lt.trans_le, StrictConvexOn.convexOn, ConvexOn.slope_le_of_hasDerivWithinAt_Iio
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : DifferentiableWithinAt ℝ f (Iio y) y
⊢ slope f x y < derivWithin f (Iio y) y

Tactic:
hfc.slope_lt_of_hasDerivWithinAt_Iio hx hy hxy hfd.hasDerivWithinAt

Premises used: DifferentiableWithinAt.hasDerivWithinAt, StrictConvexOn.slope_lt_of_hasDerivWithinAt_Iio
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' S y
⊢ slope f x y < f'

Tactic:
hfc.slope_lt_of_hasDerivWithinAt_Iio hx hy hxy <|
    hf'.mono_of_mem_nhdsWithin <| hfc.1.ordConnected.mem_nhdsLT hx hy hxy

Premises used: Set.OrdConnected.mem_nhdsLT, StrictConvexOn.slope_lt_of_hasDerivWithinAt_Iio, HasDerivWithinAt.mono_of_mem_nhdsWithin, And.left, Convex.ordConnected
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : DifferentiableWithinAt ℝ f S y
⊢ slope f x y < derivWithin f S y

Tactic:
hfc.slope_lt_of_hasDerivWithinAt hx hy hxy hfd.hasDerivWithinAt

Premises used: DifferentiableWithinAt.hasDerivWithinAt, StrictConvexOn.slope_lt_of_hasDerivWithinAt
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivAt f f' y
⊢ slope f x y < f'

Tactic:
hfc.slope_lt_of_hasDerivWithinAt_Iio hx hy hxy hf'.hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, StrictConvexOn.slope_lt_of_hasDerivWithinAt_Iio
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : DifferentiableAt ℝ f y
⊢ slope f x y < deriv f y

Tactic:
hfc.slope_lt_of_hasDerivAt hx hy hxy hfd.hasDerivAt

Premises used: DifferentiableAt.hasDerivAt, StrictConvexOn.slope_lt_of_hasDerivAt
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : StrictConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ derivWithin f S x < derivWithin f S y

Tactic:
(hfc.derivWithin_lt_slope hx hy hxy (hfd x hx)).trans
    (hfc.slope_lt_derivWithin hx hy hxy (hfd y hy))

Premises used: StrictConvexOn.slope_lt_derivWithin, LT.lt.trans, StrictConvexOn.derivWithin_lt_slope
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : StrictConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ derivWithin f S x < derivWithin f S y

Tactic:
exact (hfc.derivWithin_lt_slope hx hy hxy (hfd x hx)).trans
    (hfc.slope_lt_derivWithin hx hy hxy (hfd y hy))

Premises used: StrictConvexOn.slope_lt_derivWithin, LT.lt.trans, StrictConvexOn.derivWithin_lt_slope
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : StrictConvexOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ deriv f x < deriv f y

Tactic:
(hfc.deriv_lt_slope hx hy hxy (hfd x hx)).trans (hfc.slope_lt_deriv hx hy hxy (hfd y hy))

Premises used: StrictConvexOn.deriv_lt_slope, StrictConvexOn.slope_lt_deriv, LT.lt.trans
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : StrictConvexOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ deriv f x < deriv f y

Tactic:
exact (hfc.deriv_lt_slope hx hy hxy (hfd x hx)).trans (hfc.slope_lt_deriv hx hy hxy (hfd y hy))

Premises used: StrictConvexOn.deriv_lt_slope, StrictConvexOn.slope_lt_deriv, LT.lt.trans
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
⊢ slope f x y ≤ f'

Tactic:
simpa only [Pi.neg_def, slope_neg, neg_neg] using
    neg_le_neg (hfc.neg.le_slope_of_hasDerivWithinAt_Ioi hx hy hxy hf'.neg)

Premises used: neg_neg, ConvexOn.le_slope_of_hasDerivWithinAt_Ioi, HasDerivWithinAt.neg, slope_neg, ConcaveOn.neg, neg_le_neg, Pi.neg_def
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y : ℝ
hfc : ConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : DifferentiableWithinAt ℝ f (Ioi x) x
⊢ slope f x y ≤ derivWithin f (Ioi x) x

Tactic:
hfc.slope_le_of_hasDerivWithinAt_Ioi hx hy hxy hfd.hasDerivWithinAt

Premises used: DifferentiableWithinAt.hasDerivWithinAt, ConcaveOn.slope_le_of_hasDerivWithinAt_Ioi
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : HasDerivWithinAt f f' S x
⊢ slope f x y ≤ f'

Tactic:
hfc.slope_le_of_hasDerivWithinAt_Ioi hx hy hxy <|
    hfd.mono_of_mem_nhdsWithin <| hfc.1.ordConnected.mem_nhdsGT hx hy hxy

Premises used: Set.OrdConnected.mem_nhdsGT, ConcaveOn.slope_le_of_hasDerivWithinAt_Ioi, HasDerivWithinAt.mono_of_mem_nhdsWithin, And.left, Convex.ordConnected
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y : ℝ
hfc : ConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : DifferentiableWithinAt ℝ f S x
⊢ slope f x y ≤ derivWithin f S x

Tactic:
hfc.slope_le_of_hasDerivWithinAt hx hy hxy hfd.hasDerivWithinAt

Premises used: DifferentiableWithinAt.hasDerivWithinAt, ConcaveOn.slope_le_of_hasDerivWithinAt
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivAt f f' x
⊢ slope f x y ≤ f'

Tactic:
hfc.slope_le_of_hasDerivWithinAt_Ioi hx hy hxy hf'.hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, ConcaveOn.slope_le_of_hasDerivWithinAt_Ioi
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y : ℝ
hfc : ConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : DifferentiableAt ℝ f x
⊢ slope f x y ≤ deriv f x

Tactic:
hfc.slope_le_of_hasDerivAt hx hy hxy hfd.hasDerivAt

Premises used: ConcaveOn.slope_le_of_hasDerivAt, DifferentiableAt.hasDerivAt
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
⊢ f' ≤ slope f x y

Tactic:
simpa only [neg_neg, Pi.neg_def, slope_neg] using
    neg_le_neg (hfc.neg.slope_le_of_hasDerivWithinAt_Iio hx hy hxy hf'.neg)

Premises used: neg_neg, HasDerivWithinAt.neg, slope_neg, ConcaveOn.neg, neg_le_neg, ConvexOn.slope_le_of_hasDerivWithinAt_Iio, Pi.neg_def
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y : ℝ
hfc : ConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : DifferentiableWithinAt ℝ f (Iio y) y
⊢ derivWithin f (Iio y) y ≤ slope f x y

Tactic:
hfc.le_slope_of_hasDerivWithinAt_Iio hx hy hxy hfd.hasDerivWithinAt

Premises used: DifferentiableWithinAt.hasDerivWithinAt, ConcaveOn.le_slope_of_hasDerivWithinAt_Iio
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' S y
⊢ f' ≤ slope f x y

Tactic:
hfc.le_slope_of_hasDerivWithinAt_Iio hx hy hxy <|
    hf'.mono_of_mem_nhdsWithin <| hfc.1.ordConnected.mem_nhdsLT hx hy hxy

Premises used: Set.OrdConnected.mem_nhdsLT, HasDerivWithinAt.mono_of_mem_nhdsWithin, ConcaveOn.le_slope_of_hasDerivWithinAt_Iio, And.left, Convex.ordConnected
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y : ℝ
hfc : ConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : DifferentiableWithinAt ℝ f S y
⊢ derivWithin f S y ≤ slope f x y

Tactic:
hfc.le_slope_of_hasDerivWithinAt hx hy hxy hfd.hasDerivWithinAt

Premises used: DifferentiableWithinAt.hasDerivWithinAt, ConcaveOn.le_slope_of_hasDerivWithinAt
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivAt f f' y
⊢ f' ≤ slope f x y

Tactic:
hfc.le_slope_of_hasDerivWithinAt_Iio hx hy hxy hf'.hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, ConcaveOn.le_slope_of_hasDerivWithinAt_Iio