awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxy : x < a * x + b * z
hyz : a * x + b * z < z
key : (f (a * x + b * z) - f x) / (a * x + b * z - x) < (f z - f (a * x + b * z)) / (z - (a * x + b * z))
⊢ (f (a * x + b * z) - f x) * (z - (a * x + b * z)) < (a * x + b * z - x) * (f z - f (a * x + b * z))

Tactic:
field_simp [sub_pos.2 hxy, sub_pos.2 hyz] at key

Premises used: Iff.mpr, sub_pos
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxy : x < a * x + b * z
hyz : a * x + b * z < z
key : (f (a * x + b * z) - f x) * (z - (a * x + b * z)) < (a * x + b * z - x) * (f z - f (a * x + b * z))
apply : (z - x) * f (a * x + b * z) < (z - x) * (a * f x + b * f z)
⊢ f (a * x + b * z) < a * f x + b * f z

Tactic:
apply lt_of_mul_lt_mul_left ?_ (sub_pos.2 hxz).le

Premises used: Iff.mpr, sub_pos, lt_of_mul_lt_mul_left, LT.lt.le
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxy : x < a * x + b * z
hyz : a * x + b * z < z
key : (f (a * x + b * z) - f x) * (z - (a * x + b * z)) < (a * x + b * z - x) * (f z - f (a * x + b * z))
⊢ (z - x) * f (a * x + b * z) < (z - x) * (a * f x + b * f z)

Tactic:
linear_combination key + (- f x * z + x * f z) * hab

Premises used: HMul.hMul, HAdd.hAdd, Neg.neg
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) < (f y - f x) / (y - x)
rw : StrictConvexOn 𝕜 s (-f)
⊢ StrictConcaveOn 𝕜 s f

Tactic:
rw [← neg_strictConvexOn_iff]

Premises used: neg_strictConvexOn_iff
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) < (f y - f x) / (y - x)
⊢ StrictConvexOn 𝕜 s (-f)

Tactic:
strictConvexOn_of_slope_strict_mono_adjacent hs fun hx hz hxy hyz => ?_

Premises used: strictConvexOn_of_slope_strict_mono_adjacent
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) < (f y - f x) / (y - x)
refine :
  ∀ {x y z : 𝕜} (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y) (hyz : y < z),
    ((-f) y - (-f) x) / (y - x) < ((-f) z - (-f) y) / (z - y)
⊢ StrictConvexOn 𝕜 s (-f)

Tactic:
refine strictConvexOn_of_slope_strict_mono_adjacent hs fun hx hz hxy hyz => ?_

Premises used: strictConvexOn_of_slope_strict_mono_adjacent
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) < (f y - f x) / (y - x)
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
simp : (-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:
simp only [Pi.neg_apply]

Premises used: Pi.neg_apply
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) < (f y - f x) / (y - x)
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ (-f y - -f x) / (y - x) < (-f z - -f y) / (z - y)

Tactic:
linear_combination hf hx hz hxy hyz
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
⊢ ConvexOn 𝕜 s f ↔
    Convex 𝕜 s ∧ ∀ ⦃x y z : 𝕜⦄, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)

Tactic:
⟨fun h => ⟨h.1, fun _ _ _ => h.slope_mono_adjacent⟩, fun h =>
    convexOn_of_slope_mono_adjacent h.1 (@fun _ _ _ hx hy => h.2 hx hy)⟩

Premises used: ConvexOn.slope_mono_adjacent, And.right, convexOn_of_slope_mono_adjacent, And.left, And.intro, Iff.intro
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
⊢ ConcaveOn 𝕜 s f ↔
    Convex 𝕜 s ∧ ∀ ⦃x y z : 𝕜⦄, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)

Tactic:
⟨fun h => ⟨h.1, fun _ _ _ => h.slope_anti_adjacent⟩, fun h =>
    concaveOn_of_slope_anti_adjacent h.1 (@fun _ _ _ hx hy => h.2 hx hy)⟩

Premises used: concaveOn_of_slope_anti_adjacent, And.right, And.left, And.intro, Iff.intro, ConcaveOn.slope_anti_adjacent
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
⊢ StrictConvexOn 𝕜 s f ↔
    Convex 𝕜 s ∧ ∀ ⦃x y z : 𝕜⦄, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)

Tactic:
⟨fun h => ⟨h.1, fun _ _ _ => h.slope_strict_mono_adjacent⟩, fun h =>
    strictConvexOn_of_slope_strict_mono_adjacent h.1 (@fun _ _ _ hx hy => h.2 hx hy)⟩

Premises used: StrictConvexOn.slope_strict_mono_adjacent, strictConvexOn_of_slope_strict_mono_adjacent, And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
⊢ StrictConcaveOn 𝕜 s f ↔
    Convex 𝕜 s ∧ ∀ ⦃x y z : 𝕜⦄, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) < (f y - f x) / (y - x)

Tactic:
⟨fun h => ⟨h.1, fun _ _ _ => h.slope_anti_adjacent⟩, fun h =>
    strictConcaveOn_of_slope_strict_anti_adjacent h.1 (@fun _ _ _ hx hy => h.2 hx hy)⟩

Premises used: StrictConcaveOn.slope_anti_adjacent, And.right, And.left, And.intro, Iff.intro, strictConcaveOn_of_slope_strict_anti_adjacent
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
linarith : y - x ≤ 0 → x - y + (y - x - 0) = 0
⊢ 0 < y - x

Tactic:
linarith
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ 0 < y - x

Tactic:
have hxy' : 0 < y - x := by linarith
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
linarith : z - y ≤ 0 → y - z + (z - y - 0) = 0
⊢ 0 < z - y

Tactic:
linarith
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
⊢ 0 < z - y

Tactic:
have hyz' : 0 < z - y := by linarith
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
linarith : z - x ≤ 0 → x - y + (y - z) + (z - x - 0) = 0
⊢ 0 < z - x

Tactic:
linarith
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
⊢ 0 < z - x

Tactic:
have hxz' : 0 < z - x := by linarith
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
⊢ 0 ≤ (z - y) / (z - x)

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
⊢ 0 ≤ (z - y) / (z - x)

Tactic:
have ha : 0 ≤ (z - y) / (z - x) := by positivity
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
⊢ 0 ≤ (y - x) / (z - x)

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
⊢ 0 ≤ (y - x) / (z - x)

Tactic:
have hb : 0 ≤ (y - x) / (z - x) := by positivity
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
hb : 0 ≤ (y - x) / (z - x)
refine_2 :
  ∀
    (key :
      f (((z - y) / (z - x)) • x + ((y - x) / (z - x)) • z) ≤ ((z - y) / (z - x)) • f x + ((y - x) / (z - x)) • f z),
    (z - x) * f y ≤ (z - y) * f x + (y - x) * f z
refine_1 : (z - y) / (z - x) + (y - x) / (z - x) = 1
⊢ (z - x) * f y ≤ (z - y) * f x + (y - x) * f z

Tactic:
have key := hf.2 hx hz ha hb ?_
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
hb : 0 ≤ (y - x) / (z - x)
key : f ((z - y) / (z - x) * x + (y - x) / (z - x) * z) ≤ (z - y) / (z - x) * f x + (y - x) / (z - x) * f z
⊢ f (z * y * (z - x)⁻¹ - y * x * (z - x)⁻¹) ≤
    z * (z - x)⁻¹ * f x - y * (z - x)⁻¹ * f x + y * (z - x)⁻¹ * f z - x * (z - x)⁻¹ * f z

Tactic:
ring_nf at key
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
hb : 0 ≤ (y - x) / (z - x)
key :
  f (z * y * (z - x)⁻¹ - y * x * (z - x)⁻¹) ≤
    z * (z - x)⁻¹ * f x - y * (z - x)⁻¹ * f x + y * (z - x)⁻¹ * f z - x * (z - x)⁻¹ * f z
⊢ (z - x) * f y ≤ f x * (z - y) + y * f z - x * f z

Tactic:
field_simp at key
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
hb : 0 ≤ (y - x) / (z - x)
key : (z - x) * f y ≤ f x * (z - y) + y * f z - x * f z
⊢ (z - x) * f y ≤ (z - y) * f x + (y - x) * f z

Tactic:
linear_combination key
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
hb : 0 ≤ (y - x) / (z - x)
⊢ (z - y) / (z - x) + (y - x) / (z - x) = 1

Tactic:
field
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
linarith : z - x ≤ 0 → x - y + (y - z) + (z - x - 0) = 0
⊢ 0 < z - x

Tactic:
linarith
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
⊢ 0 < z - x

Tactic:
have hxz' : 0 < z - x := by linarith
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hxz' : 0 < z - x
field_simp : (f y - f x) * (z - x) ≤ (y - x) * (f z - f x)
⊢ (f y - f x) / (y - x) ≤ (f z - f x) / (z - x)

Tactic:
field_simp
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hxz' : 0 < z - x
linarith :
  (y - x) * (f z - f x) < (f y - f x) * (z - x) →
    (y - x) * (f z - f x) - (f y - f x) * (z - x) + ((z - x) * f y - ((z - y) * f x + (y - x) * f z)) = 0
⊢ (f y - f x) * (z - x) ≤ (y - x) * (f z - f x)

Tactic:
linarith only [hf.secant_mono_aux1 hx hz hxy hyz]

Premises used: ConvexOn.secant_mono_aux1
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
linarith : z - y ≤ 0 → y - z + (z - y - 0) = 0
⊢ 0 < z - y

Tactic:
linarith
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ 0 < z - y

Tactic:
have hyz' : 0 < z - y := by linarith
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hyz' : 0 < z - y
linarith : z - x ≤ 0 → x - y + (y - z) + (z - x - 0) = 0
⊢ 0 < z - x

Tactic:
linarith
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hyz' : 0 < z - y
⊢ 0 < z - x

Tactic:
have hxz' : 0 < z - x := by linarith
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hyz' : 0 < z - y
hxz' : 0 < z - x
field_simp : (f z - f x) * (z - y) ≤ (z - x) * (f z - f y)
⊢ (f z - f x) / (z - x) ≤ (f z - f y) / (z - y)

Tactic:
field_simp
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hyz' : 0 < z - y
hxz' : 0 < z - x
linarith :
  (z - x) * (f z - f y) < (f z - f x) * (z - y) →
    (z - x) * (f z - f y) - (f z - f x) * (z - y) + ((z - x) * f y - ((z - y) * f x + (y - x) * f z)) = 0
⊢ (f z - f x) * (z - y) ≤ (z - x) * (f z - f y)

Tactic:
linarith only [hf.secant_mono_aux1 hx hz hxy hyz]

Premises used: ConvexOn.secant_mono_aux1
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy : x ≤ y
inl : ∀ (hy : x ∈ s) (hya : x ≠ a) (hxy : x ≤ x), (f x - f a) / (x - a) ≤ (f x - f a) / (x - a)
inr : ∀ (hxy : x < y), (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)
⊢ (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)

Tactic:
rcases eq_or_lt_of_le hxy with (rfl | hxy)

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x : 𝕜
ha : a ∈ s
hx : x ∈ s
hxa : x ≠ a
hy : x ∈ s
hya : x ≠ a
hxy : x ≤ x
⊢ (f x - f a) / (x - a) ≤ (f x - f a) / (x - a)

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy_1 : x ≤ y
hxy : x < y
inr : ∀ (hxa : x < a), (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)
inr₁ : ∀ (hxa : a < x), (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)
⊢ (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)

Tactic:
rcases lt_or_gt_of_ne hxa with hxa | hxa

Premises used: lt_or_gt_of_ne
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa_1 : x ≠ a
hya : y ≠ a
hxy_1 : x ≤ y
hxy : x < y
hxa : x < a
inr : ∀ (hya : y < a), (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)
inr₁ : ∀ (hya : a < y), (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)
⊢ (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)

Tactic:
rcases lt_or_gt_of_ne hya with hya | hya

Premises used: lt_or_gt_of_ne
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa_1 : x ≠ a
hya_1 : y ≠ a
hxy_1 : x ≤ y
hxy : x < y
hxa : x < a
hya : y < a
⊢ (f a - f x) / (a - x) ≤ (f a - f y) / (a - y)

Tactic:
hf.secant_mono_aux3 hx ha hxy hya

Premises used: ConvexOn.secant_mono_aux3
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa_1 : x ≠ a
hya_1 : y ≠ a
hxy_1 : x ≤ y
hxy : x < y
hxa : x < a
hya : y < a
h : (f x - f a) / (x - a) = (f a - f x) / (a - x)
h₁ : (f y - f a) / (y - a) = (f a - f y) / (a - y)
⊢ (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)

Tactic:
convert! hf.secant_mono_aux3 hx ha hxy hya using 1

Premises used: ConvexOn.secant_mono_aux3
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa_1 : x ≠ a
hya_1 : y ≠ a
hxy_1 : x ≤ y
hxy : x < y
hxa : x < a
hya : y < a
h : -(f x - f a) / -(x - a) = (f a - f x) / (a - x)
⊢ (f x - f a) / (x - a) = (f a - f x) / (a - x)

Tactic:
rw [← neg_div_neg_eq]

Premises used: neg_div_neg_eq
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa_1 : x ≠ a
hya_1 : y ≠ a
hxy_1 : x ≤ y
hxy : x < y
hxa : x < a
hya : y < a
h : -(f y - f a) / -(y - a) = (f a - f y) / (a - y)
⊢ (f y - f a) / (y - a) = (f a - f y) / (a - y)

Tactic:
rw [← neg_div_neg_eq]

Premises used: neg_div_neg_eq
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa_1 : x ≠ a
hya_1 : y ≠ a
hxy_1 : x ≤ y
hxy : x < y
hxa : x < a
hya : y < a
⊢ -(f x - f a) / -(x - a) = (f a - f x) / (a - x)

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa_1 : x ≠ a
hya_1 : y ≠ a
hxy_1 : x ≤ y
hxy : x < y
hxa : x < a
hya : y < a
⊢ -(f y - f a) / -(y - a) = (f a - f y) / (a - y)

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa_1 : x ≠ a
hya_1 : y ≠ a
hxy_1 : x ≤ y
hxy : x < y
hxa : x < a
hya : a < y
⊢ (f a - f x) / (a - x) ≤ (f y - f a) / (y - a)

Tactic:
hf.slope_mono_adjacent hx hy hxa hya

Premises used: ConvexOn.slope_mono_adjacent
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa_1 : x ≠ a
hya_1 : y ≠ a
hxy_1 : x ≤ y
hxy : x < y
hxa : x < a
hya : a < y
h : (f x - f a) / (x - a) = (f a - f x) / (a - x)
⊢ (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)

Tactic:
convert! hf.slope_mono_adjacent hx hy hxa hya using 1

Premises used: ConvexOn.slope_mono_adjacent
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa_1 : x ≠ a
hya_1 : y ≠ a
hxy_1 : x ≤ y
hxy : x < y
hxa : x < a
hya : a < y
h : -(f x - f a) / -(x - a) = (f a - f x) / (a - x)
⊢ (f x - f a) / (x - a) = (f a - f x) / (a - x)

Tactic:
rw [← neg_div_neg_eq]

Premises used: neg_div_neg_eq
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa_1 : x ≠ a
hya_1 : y ≠ a
hxy_1 : x ≤ y
hxy : x < y
hxa : x < a
hya : a < y
⊢ -(f x - f a) / -(x - a) = (f a - f x) / (a - x)

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa_1 : x ≠ a
hya : y ≠ a
hxy_1 : x ≤ y
hxy : x < y
hxa : a < x
⊢ (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)

Tactic:
hf.secant_mono_aux2 ha hy hxa hxy

Premises used: ConvexOn.secant_mono_aux2
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa_1 : x ≠ a
hya : y ≠ a
hxy_1 : x ≤ y
hxy : x < y
hxa : a < x
⊢ (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)

Tactic:
exact hf.secant_mono_aux2 ha hy hxa hxy

Premises used: ConvexOn.secant_mono_aux2
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
linarith : y - x ≤ 0 → x - y + (y - x - 0) = 0
⊢ 0 < y - x

Tactic:
linarith
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ 0 < y - x

Tactic:
have hxy' : 0 < y - x := by linarith
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
linarith : z - y ≤ 0 → y - z + (z - y - 0) = 0
⊢ 0 < z - y

Tactic:
linarith