awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ConcaveOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
have this : ((-f) y - (-f) x) / (y - x) ≤ ((-f) z - (-f) y) / (z - y)
Tactic: have := ConvexOn.slope_mono_adjacent hf.neg hx hz hxy hyz
-- 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 y) / (z - y)
have hxz : x < z
Tactic: have hxz := hxy.trans hyz
-- 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
hxz : x < z
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)
have hxz' : x ≠ z
Tactic: have hxz' := hxz.ne
-- 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
hxz : x < z
hxz' : x ≠ z
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)
have hxy₁ : 0 < y - x
Tactic: rw [← sub_pos] at hxy hxz hyz
Cleared hypotheses: hxy, hyz, hxz, hxz'
-- 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
hxz : x < z
hxz' : x ≠ z
hxy₁ : 0 < y - x
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)
have hyz₁ : 0 < z - y
Tactic: rw [← sub_pos] at hxy hxz hyz
Cleared hypotheses: hxy, hyz, hxz, hxz'
-- 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
hxz : x < z
hxz' : x ≠ z
hxy₁ : 0 < y - x
hyz₁ : 0 < z - y
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)
have hxz₁ : 0 < z - x
Tactic: rw [← sub_pos] at hxy hxz hyz
Cleared hypotheses: hxy, hyz, hxz, hxz'
-- 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 : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
hxz' : x ≠ z
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)
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 : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
hxz' : x ≠ z
ha : 0 < (z - y) / (z - x)
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)
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 (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 : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
hxz' : x ≠ z
ha : 0 < (z - y) / (z - x)
hb : 0 < (y - x) / (z - x)
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)
have key : f (((z - y) / (z - x)) • x + ((y - x) / (z - x)) • z) < ((z - y) / (z - x)) • f x + ((y - x) / (z - x)) • f z
Tactic: have key := hf.2 hx hz hxz' ha hb (by field)
-- 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 : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
hxz' : x ≠ z
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 y - f x) / (y - x) < (f z - f y) / (z - y)
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 (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 : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
hxz' : x ≠ z
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
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)
have field_simp : ∀ (key : (z - x) * f y < f x * (z - y) + y * f z - x * f z), (z - y) * (f y - f x) < (y - x) * (f z - f y)
Tactic: field_simp at key ⊢
Cleared hypotheses: key
-- 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 : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
hxz' : x ≠ z
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 - y) * (f y - f x) < (y - x) * (f z - f y)
have linarith : (y - x) * (f z - f y) ≤ (z - y) * (f y - f x) →
  (z - x) * f y - (f x * (z - y) + y * f z - x * f z) + ((y - x) * (f z - f y) - (z - y) * (f y - f x)) = 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 : StrictConcaveOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ (f z - f y) / (z - y) < (f y - f x) / (y - x)
have this : ((-f) y - (-f) x) / (y - x) < ((-f) z - (-f) y) / (z - y)
Tactic: have := StrictConvexOn.slope_strict_mono_adjacent hf.neg 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 : 𝕜 → 𝕜
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
⊢ f (a • x + b • z) ≤ a • f x + b • f z
have simp : f (a * x + b * z) ≤ a * f x + b * f z
Tactic: simp only [smul_eq_mul]
-- 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 : 𝕜 → 𝕜
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
⊢ f (a * x + b * z) ≤ a * f x + b * f z
have hxy : x < a * x + b * z
Tactic: have hxy : x < a * x + b * z := by linear_combination b * hxz - x * hab
-- 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 : 𝕜 → 𝕜
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
⊢ f (a * x + b * z) ≤ a * f x + b * f z
have hyz : a * x + b * z < z
Tactic: have hyz : a * x + b * z < z := by linear_combination a * hxz + z * hab
-- 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 : 𝕜 → 𝕜
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
⊢ f (a * x + b * z) ≤ a * f x + b * f z
have 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))
Tactic: have key := hf hx hz hxy hyz
-- 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 : 𝕜 → 𝕜
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) ≤ a * f x + b * f z
have 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))
Tactic: field_simp [sub_pos.2 hxy, sub_pos.2 hyz] at key
Cleared hypotheses: key
-- 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 : 𝕜 → 𝕜
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))
⊢ f (a * x + b * z) ≤ a * f x + b * f z
have apply : (z - x) * f (a * x + b * z) ≤ (z - x) * (a * f x + b * f z)
Tactic: apply le_of_mul_le_mul_left ?_ (sub_pos.2 hxz)
-- 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 : 𝕜 → 𝕜
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)
⊢ ConcaveOn 𝕜 s f
have rw : ConvexOn 𝕜 s (-f)
Tactic: rw [← neg_convexOn_iff]
-- 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 : 𝕜 → 𝕜
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)
⊢ ConvexOn 𝕜 s (-f)
have 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)
Tactic: refine convexOn_of_slope_mono_adjacent hs fun 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 : 𝕜 → 𝕜
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)
have simp : (-f y - -f x) / (y - x) ≤ (-f z - -f y) / (z - y)
Tactic: simp only [Pi.neg_apply]
-- 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 : 𝕜 → 𝕜
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
⊢ f (a • x + b • z) < a • f x + b • f z
have simp : f (a * x + b * z) < a * f x + b * f z
Tactic: simp only [smul_eq_mul]
-- 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 : 𝕜 → 𝕜
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
⊢ f (a * x + b * z) < a * f x + b * f z
have hxy : x < a * x + b * z
Tactic: have hxy : x < a * x + b * z := by linear_combination b * hxz - x * hab
-- 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 : 𝕜 → 𝕜
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
⊢ f (a * x + b * z) < a * f x + b * f z
have hyz : a * x + b * z < z
Tactic: have hyz : a * x + b * z < z := by linear_combination a * hxz + z * hab
-- 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 : 𝕜 → 𝕜
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
⊢ f (a * x + b * z) < a * f x + b * f z
have 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))
Tactic: have key := hf hx hz hxy hyz
-- 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 : 𝕜 → 𝕜
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) < a * f x + b * f z
have 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))
Tactic: field_simp [sub_pos.2 hxy, sub_pos.2 hyz] at key
Cleared hypotheses: key
-- 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 : 𝕜 → 𝕜
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))
⊢ f (a * x + b * z) < a * f x + b * f z
have apply : (z - x) * f (a * x + b * z) < (z - x) * (a * f x + b * f z)
Tactic: apply lt_of_mul_lt_mul_left ?_ (sub_pos.2 hxz).le
-- 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 : 𝕜 → 𝕜
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)
⊢ StrictConcaveOn 𝕜 s f
have rw : StrictConvexOn 𝕜 s (-f)
Tactic: rw [← neg_strictConvexOn_iff]
-- 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 : 𝕜 → 𝕜
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)
have 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)
Tactic: refine strictConvexOn_of_slope_strict_mono_adjacent hs fun 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 : 𝕜 → 𝕜
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)
have simp : (-f y - -f x) / (y - x) < (-f z - -f y) / (z - y)
Tactic: simp only [Pi.neg_apply]
-- 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 < 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 : ConvexOn 𝕜 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 : 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
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
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 : 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
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
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 : 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
⊢ (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 : 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)
⊢ (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 : 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 - 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 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 : 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
⊢ (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 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 : 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
⊢ (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 : 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 ≤ (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 : ConvexOn 𝕜 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 : 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
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
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 : 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) / (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