case inl
x : ℝ
h : 0 ≤ x
⊢ x + 1 ≤ exp x

case inr
x : ℝ
h : x < 0
⊢ x + 1 ≤ exp x
x : ℝ
⊢ x + 1 ≤ exp x
cases' le_or_lt 0 x with h h
no goals
case inr
x : ℝ
h : x < 0
⊢ x + 1 ≤ exp x
exact (add_one_lt_exp_of_neg h).le
no goals
case inl
x : ℝ
h : 0 ≤ x
⊢ x + 1 ≤ exp x
exact Real.add_one_le_exp_of_nonneg h