-- Mathlib/Analysis/Convex/Slope.lean
theorem strictConvexOn_of_slope_strict_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)) :
    StrictConvexOn 𝕜 s f :=
  LinearOrder.strictConvexOn_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
⊢ f (a • x + b • z) < a • f x + b • f z

Tactic:
have hxy : x < y := by
  rw [← one_mul x, ← hab, add_mul]
  exact add_lt_add_left ((mul_lt_mul_left hb).2 hxz) _

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
⊢ 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
⊢ 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

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_lt_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 : 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
⊢ (1 - b) * x + b * z - x = b * (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
⊢ f (a • x + b • z) < a • f x + b • f z

Tactic:
have hyz : y < z := by
  rw [← one_mul z, ← hab, add_mul]
  exact add_lt_add_right ((mul_lt_mul_left ha).2 hxz) _

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
⊢ 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 : 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 - y) / (z - x) = a

Tactic:
dsimp [y]

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 - 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 + b * z)) / (z - x) = a

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 + b * z)) / (z - x) = a

Tactic:
simp_rw [div_eq_iff hxz.ne', ← 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 - 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)

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