case inl
x : ℝ
hx : x ≠ 0
h : x < 0
⊢ x + 1 < exp x

case inr
x : ℝ
hx : x ≠ 0
h : x > 0
⊢ x + 1 < exp x
x : ℝ
hx : x ≠ 0
⊢ x + 1 < exp x
cases' lt_or_gt_of_ne hx with h h
no goals
case inr
x : ℝ
hx : x ≠ 0
h : x > 0
⊢ x + 1 < exp x
exact add_one_lt_exp_of_pos h
no goals
case inl
x : ℝ
hx : x ≠ 0
h : x < 0
⊢ x + 1 < exp x
exact add_one_lt_exp_of_neg h