case inl
h : 0 ≤ 0
⊢ 1 - 0 ≤ exp (-0)

case inr
y : ℝ
h✝ : 0 ≤ y
h : 0 < y
⊢ 1 - y ≤ exp (-y)
y : ℝ
h : 0 ≤ y
⊢ 1 - y ≤ exp (-y)
rcases eq_or_lt_of_le h with (rfl | h)
no goals
case inl
h : 0 ≤ 0
⊢ 1 - 0 ≤ exp (-0)
simp
no goals
case inr
y : ℝ
h✝ : 0 ≤ y
h : 0 < y
⊢ 1 - y ≤ exp (-y)
exact (one_sub_lt_exp_minus_of_pos h).le