-- Mathlib/Analysis/Convex/Slope.lean
theorem convexOn_of_slope_mono_adjacent (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)) :
    ConvexOn 𝕜 s f :=
  LinearOrder.convexOn_of_lt hs fun x hx z hz hxz a b ha hb hab => by
    let y := a * x + b * z
    have hxy : x < y

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
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
y : 𝕜 := a * x + b * z
⊢ x < y

Tactic:
rw [← one_mul x, ← hab, add_mul]

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
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
y : 𝕜 := a * x + b * z
⊢ a * x + b * x < y

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
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
y : 𝕜 := a * x + b * z
⊢ a * x + b * x < y

Tactic:
exact add_lt_add_left ((mul_lt_mul_left hb).2 hxz) _

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
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
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x)
hxz : 0 < z - x
ha : (z - y) / (z - x) = a
⊢ (y - x) / (z - x) = b

Tactic:
rw [eq_comm, ← sub_eq_iff_eq_add] at hab

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
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 : 1 - b = a
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x)
hxz : 0 < z - x
ha : (z - y) / (z - x) = a
⊢ (y - x) / (z - x) = b

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
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 : 1 - a = b
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x)
hxz : 0 < z - x
⊢ z - (a * x + (1 - a) * z) = a * (z - x)

Tactic:
ring

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
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
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
⊢ f (a • x + b • z) ≤ a • f x + b • f z

Tactic:
have : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x) :=
  (div_le_div_iff₀ (sub_pos.2 hxy) (sub_pos.2 hyz)).1 (hf hx hz hxy hyz)

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
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
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x)
⊢ f (a • x + b • z) ≤ a • f x + b • f z

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
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
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x)
hxz : 0 < z - x
⊢ f (a • x + b • z) ≤ a • f x + b • f z

Tactic:
have ha : (z - y) / (z - x) = a := by
  rw [eq_comm, ← sub_eq_iff_eq_add'] at hab
  dsimp [y]
  simp_rw [div_eq_iff hxz.ne', ← hab]
  ring

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
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
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x)
hxz : 0 < z - x
ha : (z - y) / (z - x) = a
⊢ f (a • x + b • z) ≤ a • f x + b • f z

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
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
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x)
hxz : 0 < z - x
ha : (z - y) / (z - x) = a
hb : (y - x) / (z - x) = b
⊢ f (a • x + b • z) ≤ a • f x + b • f z

Tactic:
rwa [sub_mul, sub_mul, sub_le_iff_le_add', ← add_sub_assoc, le_sub_iff_add_le, ← mul_add,
  sub_add_sub_cancel, ← le_div_iff₀ hxz, add_div, mul_div_assoc, mul_div_assoc, mul_comm (f x),
  mul_comm (f z), ha, hb] at this

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
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
y : 𝕜 := a * x + b * z
hxy : x < y
⊢ y < a * z + b * z

Tactic:
exact add_lt_add_right ((mul_lt_mul_left ha).2 hxz) _

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
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
y : 𝕜 := a * x + b * z
hxy : x < y
⊢ y < z

Tactic:
rw [← one_mul z, ← hab, add_mul]

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
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
y : 𝕜 := a * x + b * z
hxy : x < y
⊢ y < a * z + b * z

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
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
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x)
hxz : 0 < z - x
ha : (z - y) / (z - x) = a
⊢ f (a • x + b • z) ≤ a • f x + b • f z

Tactic:
have hb : (y - x) / (z - x) = b := by
  rw [eq_comm, ← sub_eq_iff_eq_add] at hab
  dsimp [y]
  simp_rw [div_eq_iff hxz.ne', ← hab]
  ring

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
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
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x)
hxz : 0 < z - x
ha : (z - y) / (z - x) = a
hb : (y - x) / (z - x) = b
⊢ f (a • x + b • z) ≤ a • f x + b • f z