case inl
y : ℝ
h : 0 < y
h' : 1 ≤ y
⊢ 1 - y < exp (-y)

case inr
y : ℝ
h : 0 < y
h' : y < 1
⊢ 1 - y < exp (-y)
y : ℝ
h : 0 < y
⊢ 1 - y < exp (-y)
cases' le_or_lt 1 y with h' h'
case inr
y : ℝ
h : 0 < y
h' : y < 1
⊢ exp y < 1 / (1 - y)

y : ℝ
h : 0 < y
h' : y < 1
⊢ 0 < 1 - y
case inr
y : ℝ
h : 0 < y
h' : y < 1
⊢ 1 - y < exp (-y)
rw [exp_neg, lt_inv _ y.exp_pos, inv_eq_one_div]
no goals
case inl
y : ℝ
h : 0 < y
h' : 1 ≤ y
⊢ 1 - y < exp (-y)
linarith [(-y).exp_pos]
no goals
case inr
y : ℝ
h : 0 < y
h' : y < 1
⊢ exp y < 1 / (1 - y)
exact exp_bound_div_one_sub_of_interval' h h'
no goals
y : ℝ
h : 0 < y
h' : y < 1
⊢ 0 < 1 - y
linarith