case inl
x y : ℝ
hx : 0 ≤ 0
⊢ 0 + 1 ≤ exp 0

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