-- Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean
theorem strictConvexOn_exp : StrictConvexOn ℝ univ exp

Proof state:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ rexp y - rexp x = rexp y - rexp (y + (x - y))

Tactic:
ring_nf

Result:
no goals

Proof state:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ rexp z - rexp y ≤ rexp z - rexp y

Tactic:
rfl

Result:
no goals

Proof state:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ rexp y - rexp y * rexp (x - y) = rexp y * (1 - rexp (x - y))

Tactic:
ring

Result:
no goals

Proof state:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ rexp y * -(x - y) = rexp y * (y - x)

Tactic:
ring

Result:
no goals

Proof state:
x y z : ℝ
hxy : x < y
hyz : y < z
⊢ (rexp y - rexp x) / (y - x) < rexp y

Tactic:
have h1 : 0 < y - x := by linarith

Result:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
⊢ (rexp y - rexp x) / (y - x) < rexp y

Proof state:
⊢ ∀ {x y z : ℝ}, x ∈ univ → z ∈ univ → x < y → y < z → (rexp y - rexp x) / (y - x) < (rexp z - rexp y) / (z - y)

Tactic:
rintro x y z - - hxy hyz

Result:
x y z : ℝ
hxy : x < y
hyz : y < z
⊢ (rexp y - rexp x) / (y - x) < (rexp z - rexp y) / (z - y)

Proof state:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ rexp (z - y + y) - rexp y ≤ rexp z - rexp y

Tactic:
ring_nf

Result:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ rexp z - rexp y ≤ rexp z - rexp y

Proof state:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ rexp y - rexp x = rexp y - rexp y * rexp (x - y)

Tactic:
rw [← exp_add]

Result:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ rexp y - rexp x = rexp y - rexp (y + (x - y))

Proof state:
x y z : ℝ
hxy : x < y
hyz : y < z
⊢ rexp y < (rexp z - rexp y) / (z - y)

Tactic:
have h1 : 0 < z - y := by linarith

Result:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ rexp y < (rexp z - rexp y) / (z - y)

Proof state:
x y z : ℝ
hxy : x < y
hyz : y < z
⊢ (rexp y - rexp x) / (y - x) < (rexp z - rexp y) / (z - y)

Tactic:
trans exp y

Result:
x y z : ℝ
hxy : x < y
hyz : y < z
⊢ (rexp y - rexp x) / (y - x) < rexp y

x y z : ℝ
hxy : x < y
hyz : y < z
⊢ rexp y < (rexp z - rexp y) / (z - y)

Proof state:
case bc
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ z - y < rexp (z - y) - 1

Tactic:
linarith [add_one_lt_exp h1.ne']

Result:
no goals

Proof state:
x y z : ℝ
hxy : x < y
hyz : y < z
⊢ 0 < z - y

Tactic:
linarith

Result:
no goals

Proof state:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ rexp y * (z - y) < rexp z - rexp y

Tactic:
calc
  exp y * (z - y) < exp y * (exp (z - y) - 1) := by
    gcongr _ * ?_
    linarith [add_one_lt_exp h1.ne']
  _ = exp (z - y) * exp y - exp y := by ring
  _ ≤ exp z - exp y := by rw [← exp_add]; ring_nf; rfl

Result:
no goals

Proof state:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ rexp (z - y) * rexp y - rexp y ≤ rexp z - rexp y

Tactic:
rw [← exp_add]

Result:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ rexp (z - y + y) - rexp y ≤ rexp z - rexp y

Proof state:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
⊢ x - y < 0

Tactic:
linarith

Result:
no goals

Proof state:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ rexp y * (z - y) < rexp y * (rexp (z - y) - 1)

Tactic:
gcongr _ * ?_

Result:
case bc
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ z - y < rexp (z - y) - 1

Proof state:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ rexp y - rexp x < rexp y * (y - x)

Tactic:
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 h2.ne]
  _ = exp y * (y - x) := by ring

Result:
no goals

Proof state:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ rexp y < (rexp z - rexp y) / (z - y)

Tactic:
rw [lt_div_iff₀ h1]

Result:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ rexp y * (z - y) < rexp z - rexp y

Proof state:
⊢ StrictConvexOn ℝ univ rexp

Tactic:
apply strictConvexOn_of_slope_strict_mono_adjacent convex_univ

Result:
⊢ ∀ {x y z : ℝ}, x ∈ univ → z ∈ univ → x < y → y < z → (rexp y - rexp x) / (y - x) < (rexp z - rexp y) / (z - y)

Proof state:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ (rexp y - rexp x) / (y - x) < rexp y

Tactic:
rw [div_lt_iff₀ h1]

Result:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ rexp y - rexp x < rexp y * (y - x)

Proof state:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ rexp y * (rexp (z - y) - 1) = rexp (z - y) * rexp y - rexp y

Tactic:
ring

Result:
no goals

Proof state:
x y z : ℝ
hxy : x < y
hyz : y < z
⊢ 0 < y - x

Tactic:
linarith

Result:
no goals

Proof state:
case bc
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ 1 - rexp (x - y) < -(x - y)

Tactic:
linarith [add_one_lt_exp h2.ne]

Result:
no goals

Proof state:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
⊢ (rexp y - rexp x) / (y - x) < rexp y

Tactic:
have h2 : x - y < 0 := by linarith

Result:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ (rexp y - rexp x) / (y - x) < rexp y

Proof state:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ rexp y * (1 - rexp (x - y)) < rexp y * -(x - y)

Tactic:
gcongr

Result:
case bc
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ 1 - rexp (x - y) < -(x - y)