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 : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 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 : StrictConvexOn 𝕜 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 : StrictConvexOn 𝕜 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 : StrictConvexOn 𝕜 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 : StrictConvexOn 𝕜 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 : StrictConvexOn 𝕜 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 : StrictConvexOn 𝕜 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 : StrictConvexOn 𝕜 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)
linarith : x = z → x - y + (y - z) + -(x - z) = 0
⊢ x ≠ z

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
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 (by linarith) ha hb ?_
-- 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
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 : StrictConvexOn 𝕜 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 : StrictConvexOn 𝕜 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 : StrictConvexOn 𝕜 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 : StrictConvexOn 𝕜 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 : StrictConvexOn 𝕜 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 : StrictConvexOn 𝕜 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 : StrictConvexOn 𝕜 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_strict_mono_aux1 hx hz hxy hyz]

Premises used: StrictConvexOn.secant_strict_mono_aux1
-- 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 : 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 : StrictConvexOn 𝕜 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 : StrictConvexOn 𝕜 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 : StrictConvexOn 𝕜 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 : StrictConvexOn 𝕜 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 : StrictConvexOn 𝕜 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_strict_mono_aux1 hx hz hxy hyz]

Premises used: StrictConvexOn.secant_strict_mono_aux1
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy : x < y
inl : ∀ (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 : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa_1 : x ≠ a
hya : y ≠ a
hxy : x < y
hxa : x < a
inl : ∀ (hya : y < a), (f x - f a) / (x - a) < (f y - f a) / (y - a)
inl₁ : ∀ (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 : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa_1 : x ≠ a
hya_1 : y ≠ a
hxy : x < y
hxa : x < a
hya : y < a
⊢ (f a - f x) / (a - x) < (f a - f y) / (a - y)

Tactic:
hf.secant_strict_mono_aux3 hx ha hxy hya

Premises used: StrictConvexOn.secant_strict_mono_aux3
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa_1 : x ≠ a
hya_1 : y ≠ a
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_strict_mono_aux3 hx ha hxy hya using 1

Premises used: StrictConvexOn.secant_strict_mono_aux3
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa_1 : x ≠ a
hya_1 : y ≠ a
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 : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa_1 : x ≠ a
hya_1 : y ≠ a
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 : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa_1 : x ≠ a
hya_1 : y ≠ a
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 : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa_1 : x ≠ a
hya_1 : y ≠ a
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 : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa_1 : x ≠ a
hya_1 : y ≠ a
hxy : x < y
hxa : x < a
hya : a < y
⊢ (f a - f x) / (a - x) < (f y - f a) / (y - a)

Tactic:
hf.slope_strict_mono_adjacent hx hy hxa hya

Premises used: StrictConvexOn.slope_strict_mono_adjacent
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa_1 : x ≠ a
hya_1 : y ≠ a
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_strict_mono_adjacent hx hy hxa hya using 1

Premises used: StrictConvexOn.slope_strict_mono_adjacent
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa_1 : x ≠ a
hya_1 : y ≠ a
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 : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa_1 : x ≠ a
hya_1 : y ≠ a
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 : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa_1 : x ≠ a
hya : y ≠ a
hxy : x < y
hxa : a < x
⊢ (f x - f a) / (x - a) < (f y - f a) / (y - a)

Tactic:
hf.secant_strict_mono_aux2 ha hy hxa hxy

Premises used: StrictConvexOn.secant_strict_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
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa_1 : x ≠ a
hya : y ≠ a
hxy : x < y
hxa : a < x
⊢ (f x - f a) / (x - a) < (f y - f a) / (y - a)

Tactic:
exact hf.secant_strict_mono_aux2 ha hy hxa hxy

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

Tactic:
have key := hf.neg.secant_strict_mono ha hx hy hxa hya hxy
-- Module: Mathlib.Analysis.Convex.Slope
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy : x < y
key : (-f x - -f a) / (x - a) < (-f y - -f a) / (y - a)
⊢ (f y - f a) / (y - a) < (f x - f a) / (x - a)

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 : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
z : 𝕜
hz : z ∈ s ∩ Set.Ioi y
⊢ f y < f z

Tactic:
hf.lt_right_of_left_lt hx hz.1 ?_ hxy'

Premises used: ConvexOn.lt_right_of_left_lt, And.left
-- 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 : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
z : 𝕜
hz : z ∈ s ∩ Set.Ioi y
refine : y ∈ openSegment 𝕜 x z
⊢ f y < f z

Tactic:
refine hf.lt_right_of_left_lt hx hz.1 ?_ hxy'

Premises used: ConvexOn.lt_right_of_left_lt, And.left
-- 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 : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
z : 𝕜
hz : z ∈ s ∩ Set.Ioi y
rw : y ∈ Set.Ioo x z
⊢ y ∈ openSegment 𝕜 x z

Tactic:
rw [openSegment_eq_Ioo (hxy.trans hz.2)]

Premises used: openSegment_eq_Ioo, And.right, LT.lt.trans
-- 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 : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
z : 𝕜
hz : z ∈ s ∩ Set.Ioi y
⊢ y ∈ Set.Ioo x z

Tactic:
⟨hxy, hz.2⟩

Premises used: Set.Mem, setOf, And.right, And.intro, Set.Ioo
-- 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 : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
z : 𝕜
hz : z ∈ s ∩ Set.Ioi y
⊢ y ∈ Set.Ioo x z

Tactic:
exact ⟨hxy, hz.2⟩
-- 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 : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
⊢ ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z

Tactic:
have step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z := by
    intro z hz
    refine hf.lt_right_of_left_lt hx hz.1 ?_ hxy'
    rw [openSegment_eq_Ioo (hxy.trans hz.2)]
    exact ⟨hxy, hz.2⟩
-- 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 : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
inl : ∀ (hu : y ∈ s ∩ Set.Ici y) (huv : y < v), f y < f v
inr : ∀ (hu2 : y < u), f u < f v
⊢ f u < f v

Tactic:
rcases eq_or_lt_of_le hu.2 with (rfl | hu2)

Premises used: eq_or_lt_of_le, And.right, 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
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu : y ∈ s ∩ Set.Ici y
huv : y < v
⊢ f y < f v

Tactic:
step1 ⟨hv.1, huv⟩

Premises used: And.left, And.intro
-- 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 : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu : y ∈ s ∩ Set.Ici y
huv : y < v
⊢ f y < f v

Tactic:
exact step1 ⟨hv.1, huv⟩

Premises used: And.left, And.intro
-- 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 : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
⊢ f u < f v

Tactic:
hf.lt_right_of_left_lt ?_ hv.1 ?_ (step1 ⟨hu.1, hu2⟩)

Premises used: ConvexOn.lt_right_of_left_lt, And.left, And.intro
-- 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 : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
inr : y ∈ s
inr₁ : u ∈ openSegment 𝕜 y v
⊢ f u < f v

Tactic:
refine hf.lt_right_of_left_lt ?_ hv.1 ?_ (step1 ⟨hu.1, hu2⟩)

Premises used: ConvexOn.lt_right_of_left_lt, And.left, And.intro
-- 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 : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
inr : y ∈ segment 𝕜 x u
⊢ y ∈ s

Tactic:
apply hf.1.segment_subset hx hu.1

Premises used: And.left, Convex.segment_subset
-- 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 : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
inr : y ∈ Set.Icc x u
⊢ y ∈ segment 𝕜 x u

Tactic:
rw [segment_eq_Icc (hxy.le.trans hu.2)]

Premises used: LT.lt.le, segment_eq_Icc, And.right, LE.le.trans
-- 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 : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
⊢ y ∈ Set.Icc x u

Tactic:
⟨hxy.le, hu.2⟩

Premises used: Set.Mem, setOf, LT.lt.le, Set.Icc, And.right, And.intro
-- 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 : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
⊢ y ∈ Set.Icc x u

Tactic:
exact ⟨hxy.le, hu.2⟩
-- 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 : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
inr : u ∈ Set.Ioo y v
⊢ u ∈ openSegment 𝕜 y v

Tactic:
rw [openSegment_eq_Ioo (hu2.trans huv)]

Premises used: openSegment_eq_Ioo, LT.lt.trans
-- 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 : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
⊢ u ∈ Set.Ioo y v

Tactic:
⟨hu2, huv⟩

Premises used: Set.Mem, setOf, And.intro, Set.Ioo