awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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
⊢ (f y - f x) * (z - x) ≤ (y - x) * (f z - f x)
have 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
Tactic: linarith only [hf.secant_mono_aux1 hx hz hxy hyz]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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
have linarith : z - y ≤ 0 → y - z + (z - y - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (hypothesis)
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
⊢ (f z - f x) / (z - x) ≤ (f z - f y) / (z - y)
have hyz' : 0 < z - y
Tactic: have hyz' : 0 < z - y := by linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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
have linarith : z - x ≤ 0 → x - y + (y - z) + (z - x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (hypothesis)
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
⊢ (f z - f x) / (z - x) ≤ (f z - f y) / (z - y)
have hxz' : 0 < z - x
Tactic: have hxz' : 0 < z - x := by linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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
⊢ (f z - f x) / (z - x) ≤ (f z - f y) / (z - y)
have field_simp : (f z - f x) * (z - y) ≤ (z - x) * (f z - f y)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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
⊢ (f z - f x) * (z - y) ≤ (z - x) * (f z - f y)
have 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
Tactic: linarith only [hf.secant_mono_aux1 hx hz hxy hyz]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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
⊢ (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)
have inl : ∀ (hy : x ∈ s) (hya : x ≠ a) (hxy : x ≤ x), (f x - f a) / (x - a) ≤ (f x - f a) / (x - a)
Tactic: rcases eq_or_lt_of_le hxy with (rfl | hxy)
Cleared hypotheses: y, hy, hya, hxy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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)
⊢ (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)
have inr : ∀ (hxy : x < y), (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)
Tactic: rcases eq_or_lt_of_le hxy with (rfl | hxy)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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
⊢ (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)
have inr : ∀ (hxa : x < a), (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)
Tactic: rcases lt_or_gt_of_ne hxa with hxa | hxa
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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)
⊢ (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)
have inr₁ : ∀ (hxa : a < x), (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)
Tactic: rcases lt_or_gt_of_ne hxa with hxa | hxa
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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
⊢ (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)
have inr : ∀ (hya : 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
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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)
⊢ (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)
have inr₁ : ∀ (hya : a < y), (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)
Tactic: rcases lt_or_gt_of_ne hya with hya | hya
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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 y - f a) / (y - a)
have h : (f x - f a) / (x - a) = (f a - f x) / (a - x)
Tactic: convert! hf.secant_mono_aux3 hx ha hxy hya using 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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 y - f a) / (y - a)
have h₁ : (f y - f a) / (y - a) = (f a - f y) / (a - y)
Tactic: convert! hf.secant_mono_aux3 hx ha hxy hya using 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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)
have h : -(f x - f a) / -(x - a) = (f a - f x) / (a - x)
Tactic: rw [← neg_div_neg_eq]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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)
have h : -(f y - f a) / -(y - a) = (f a - f y) / (a - y)
Tactic: rw [← neg_div_neg_eq]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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 y - f a) / (y - a)
have h : (f x - f a) / (x - a) = (f a - f x) / (a - x)
Tactic: convert! hf.slope_mono_adjacent hx hy hxa hya using 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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)
have h : -(f x - f a) / -(x - a) = (f a - f x) / (a - x)
Tactic: rw [← neg_div_neg_eq]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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
have linarith : y - x ≤ 0 → x - y + (y - x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (hypothesis)
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
⊢ (z - x) * f y < (z - y) * f x + (y - x) * f z
have hxy' : 0 < y - x
Tactic: have hxy' : 0 < y - x := by linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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
have linarith : z - y ≤ 0 → y - z + (z - y - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (hypothesis)
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
⊢ (z - x) * f y < (z - y) * f x + (y - x) * f z
have hyz' : 0 < z - y
Tactic: have hyz' : 0 < z - y := by linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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
have linarith : z - x ≤ 0 → x - y + (y - z) + (z - x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (hypothesis)
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
⊢ (z - x) * f y < (z - y) * f x + (y - x) * f z
have hxz' : 0 < z - x
Tactic: have hxz' : 0 < z - x := by linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (hypothesis)
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
⊢ (z - x) * f y < (z - y) * f x + (y - x) * f z
have ha : 0 < (z - y) / (z - x)
Tactic: have ha : 0 < (z - y) / (z - x) := by positivity
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (hypothesis)
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)
⊢ (z - x) * f y < (z - y) * f x + (y - x) * f z
have hb : 0 < (y - x) / (z - x)
Tactic: have hb : 0 < (y - x) / (z - x) := by positivity
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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)
⊢ x ≠ z
have linarith : x = z → x - y + (y - z) + -(x - z) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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 - x) * f y < (z - y) * f x + (y - x) * f z
have 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
Tactic: have key := hf.2 hx hz (by linarith) ha hb ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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
⊢ (z - x) * f y < (z - y) * f x + (y - x) * f z
have refine_1 : (z - y) / (z - x) + (y - x) / (z - x) = 1
Tactic: have key := hf.2 hx hz (by linarith) ha hb ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (hypothesis)
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
⊢ (z - x) * f y < (z - y) * f x + (y - x) * f z
have 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
Tactic: ring_nf at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (hypothesis)
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 < (z - y) * f x + (y - x) * f z
have key₁ : (z - x) * f y < f x * (z - y) + y * f z - x * f z
Tactic: field_simp at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (hypothesis)
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
⊢ (f y - f x) / (y - x) < (f z - f x) / (z - x)
have hxy' : 0 < y - x
Tactic: have hxy' : 0 < y - x := by linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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
have linarith : z - x ≤ 0 → x - y + (y - z) + (z - x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (hypothesis)
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
⊢ (f y - f x) / (y - x) < (f z - f x) / (z - x)
have hxz' : 0 < z - x
Tactic: have hxz' : 0 < z - x := by linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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
⊢ (f y - f x) / (y - x) < (f z - f x) / (z - x)
have field_simp : (f y - f x) * (z - x) < (y - x) * (f z - f x)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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
⊢ (f y - f x) * (z - x) < (y - x) * (f z - f x)
have 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
Tactic: linarith only [hf.secant_strict_mono_aux1 hx hz hxy hyz]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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
have linarith : z - y ≤ 0 → y - z + (z - y - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (hypothesis)
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
⊢ (f z - f x) / (z - x) < (f z - f y) / (z - y)
have hyz' : 0 < z - y
Tactic: have hyz' : 0 < z - y := by linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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
have linarith : z - x ≤ 0 → x - y + (y - z) + (z - x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (hypothesis)
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
⊢ (f z - f x) / (z - x) < (f z - f y) / (z - y)
have hxz' : 0 < z - x
Tactic: have hxz' : 0 < z - x := by linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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
⊢ (f z - f x) / (z - x) < (f z - f y) / (z - y)
have field_simp : (f z - f x) * (z - y) < (z - x) * (f z - f y)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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
⊢ (f z - f x) * (z - y) < (z - x) * (f z - f y)
have 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
Tactic: linarith only [hf.secant_strict_mono_aux1 hx hz hxy hyz]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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
⊢ (f x - f a) / (x - a) < (f y - f a) / (y - a)
have inl : ∀ (hxa : x < a), (f x - f a) / (x - a) < (f y - f a) / (y - a)
Tactic: rcases lt_or_gt_of_ne hxa with hxa | hxa
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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)
⊢ (f x - f a) / (x - a) < (f y - f a) / (y - a)
have inr : ∀ (hxa : a < x), (f x - f a) / (x - a) < (f y - f a) / (y - a)
Tactic: rcases lt_or_gt_of_ne hxa with hxa | hxa
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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
⊢ (f x - f a) / (x - a) < (f y - f a) / (y - a)
have inl : ∀ (hya : 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
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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)
⊢ (f x - f a) / (x - a) < (f y - f a) / (y - a)
have inl₁ : ∀ (hya : a < y), (f x - f a) / (x - a) < (f y - f a) / (y - a)
Tactic: rcases lt_or_gt_of_ne hya with hya | hya
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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 y - f a) / (y - a)
have h : (f x - f a) / (x - a) = (f a - f x) / (a - x)
Tactic: convert! hf.secant_strict_mono_aux3 hx ha hxy hya using 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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 y - f a) / (y - a)
have h₁ : (f y - f a) / (y - a) = (f a - f y) / (a - y)
Tactic: convert! hf.secant_strict_mono_aux3 hx ha hxy hya using 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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)
have h : -(f x - f a) / -(x - a) = (f a - f x) / (a - x)
Tactic: rw [← neg_div_neg_eq]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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)
have h : -(f y - f a) / -(y - a) = (f a - f y) / (a - y)
Tactic: rw [← neg_div_neg_eq]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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 y - f a) / (y - a)
have h : (f x - f a) / (x - a) = (f a - f x) / (a - x)
Tactic: convert! hf.slope_strict_mono_adjacent hx hy hxa hya using 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.Slope (goal)
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)
have h : -(f x - f a) / -(x - a) = (f a - f x) / (a - x)
Tactic: rw [← neg_div_neg_eq]