⊢ ∀ {x y z : ℝ}, x ∈ univ → z ∈ univ → x < y → y < z → (exp y - exp x) / (y - x) < (exp z - exp y) / (z - y)
⊢ StrictConvexOn ℝ univ exp
apply strictConvexOn_of_slope_strict_mono_adjacent convex_univ
x y z : ℝ
hxy : x < y
hyz : y < z
⊢ (exp y - exp x) / (y - x) < (exp z - exp y) / (z - y)
⊢ ∀ {x y z : ℝ}, x ∈ univ → z ∈ univ → x < y → y < z → (exp y - exp x) / (y - x) < (exp z - exp y) / (z - y)
rintro x y z - - hxy hyz
x y z : ℝ
hxy : x < y
hyz : y < z
⊢ (exp y - exp x) / (y - x) < exp y

x y z : ℝ
hxy : x < y
hyz : y < z
⊢ exp y < (exp z - exp y) / (z - y)
x y z : ℝ
hxy : x < y
hyz : y < z
⊢ (exp y - exp x) / (y - x) < (exp z - exp y) / (z - y)
trans exp y
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
⊢ (exp y - exp x) / (y - x) < exp y
x y z : ℝ
hxy : x < y
hyz : y < z
⊢ (exp y - exp x) / (y - x) < exp y
have h1 : 0 < y - x := by linarith
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ (exp y - exp x) / (y - x) < exp y
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
⊢ (exp y - exp x) / (y - x) < exp y
have h2 : x - y < 0 := by linarith
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ exp y - exp x < exp y * (y - x)
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ (exp y - exp x) / (y - x) < exp y
rw [div_lt_iff h1]
no goals
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ exp y - exp x < exp y * (y - x)
calc
  exp y - exp x = exp y - exp y * exp (x - y) := by rw [← exp_add]; ring_nf
  _ = exp y * (1 - exp (x - y)) := by ring
  _ < exp y * -(x - y) := by gcongr; linarith [add_one_lt_exp_of_nonzero h2.ne]
  _ = exp y * (y - x) := by ring
no goals
x y z : ℝ
hxy : x < y
hyz : y < z
⊢ 0 < y - x
linarith
no goals
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
⊢ x - y < 0
linarith
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ exp y - exp x = exp y - exp (y + (x - y))
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ exp y - exp x = exp y - exp y * exp (x - y)
rw [← exp_add]
no goals
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ exp y - exp x = exp y - exp (y + (x - y))
ring_nf
no goals
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ exp y - exp y * exp (x - y) = exp y * (1 - exp (x - y))
ring
case bc
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ 1 - exp (x - y) < -(x - y)
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ exp y * (1 - exp (x - y)) < exp y * -(x - y)
gcongr
no goals
case bc
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ 1 - exp (x - y) < -(x - y)
linarith [add_one_lt_exp_of_nonzero h2.ne]
no goals
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ exp y * -(x - y) = exp y * (y - x)
ring
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ exp y < (exp z - exp y) / (z - y)
x y z : ℝ
hxy : x < y
hyz : y < z
⊢ exp y < (exp z - exp y) / (z - y)
have h1 : 0 < z - y := by linarith
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ exp y * (z - y) < exp z - exp y
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ exp y < (exp z - exp y) / (z - y)
rw [lt_div_iff h1]
no goals
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ exp y * (z - y) < exp z - exp y
calc
  exp y * (z - y) < exp y * (exp (z - y) - 1) := by
    gcongr _ * ?_
    linarith [add_one_lt_exp_of_nonzero h1.ne']
  _ = exp (z - y) * exp y - exp y := by ring
  _ ≤ exp z - exp y := by rw [← exp_add]; ring_nf; rfl
no goals
x y z : ℝ
hxy : x < y
hyz : y < z
⊢ 0 < z - y
linarith
case bc
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ z - y < exp (z - y) - 1
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ exp y * (z - y) < exp y * (exp (z - y) - 1)
gcongr _ * ?_
no goals
case bc
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ z - y < exp (z - y) - 1
linarith [add_one_lt_exp_of_nonzero h1.ne']
no goals
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ exp y * (exp (z - y) - 1) = exp (z - y) * exp y - exp y
ring
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ exp (z - y + y) - exp y ≤ exp z - exp y
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ exp (z - y) * exp y - exp y ≤ exp z - exp y
rw [← exp_add]
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ exp z - exp y ≤ exp z - exp y
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ exp (z - y + y) - exp y ≤ exp z - exp y
ring_nf
no goals
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ exp z - exp y ≤ exp z - exp y
rfl