-- Mathlib/Analysis/Convex/Slope.lean
theorem ConvexOn.slope_mono_adjacent (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 y) / (z - y)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
⊢ f y / (y - x) + f y / (z - y) ≤ f x / (y - x) + f z / (z - y)

Tactic:
have key :=
  hf.2 hx hz (show 0 ≤ a by apply div_nonneg <;> linarith)
    (show 0 ≤ b by apply div_nonneg <;> linarith)
    (show a + b = 1 by field_simp [a, b])

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
key : f (a • x + b • z) ≤ a • f x + b • f z
⊢ f y / (y - x) + f y / (z - y) ≤ f x / (y - x) + f z / (z - y)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
key : (z - x) * f y ≤ (z - x) * (a • f x + b • f z)
⊢ f y / (y - x) + f y / (z - y) ≤ f x / (y - x) + f z / (z - y)

Tactic:
field_simp [a, b, mul_comm (z - x) _] at key ⊢

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
key : f y * (z - x) ≤ (z - y) * f x + (y - x) * f z
⊢ (f y * (z - y) + f y * (y - x)) / ((y - x) * (z - y)) ≤ (f x * (z - y) + f z * (y - x)) / ((y - x) * (z - y))

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
⊢ f y / (y - x) + f y / (z - y) ≤ f x / (y - x) + f z / (z - y)

Tactic:
set b := (y - x) / (z - x)

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
⊢ f y / (y - x) + f y / (z - y) ≤ f x / (y - x) + f z / (z - y)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
this : f y / (y - x) + f y / (z - y) ≤ f x / (y - x) + f z / (z - y)
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)

Tactic:
ring_nf at this ⊢

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
this : f y * (y - x)⁻¹ + f y * (-y + z)⁻¹ ≤ (y - x)⁻¹ * f x + (-y + z)⁻¹ * f z
⊢ f y * (y - x)⁻¹ - (y - x)⁻¹ * f x ≤ -(f y * (-y + z)⁻¹) + (-y + z)⁻¹ * f z

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)

Tactic:
suffices f y / (y - x) + f y / (z - y) ≤ f x / (y - x) + f z / (z - y) by
  ring_nf at this ⊢
  linarith

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
⊢ f y / (y - x) + f y / (z - y) ≤ f x / (y - x) + f z / (z - y)