case inl
h1 : 0 ≤ 0
h2 : 0 < 1
⊢ exp 0 ≤ 1 / (1 - 0)

case inr
x : ℝ
h1✝ : 0 ≤ x
h2 : x < 1
h1 : 0 < x
⊢ exp x ≤ 1 / (1 - x)
x : ℝ
h1 : 0 ≤ x
h2 : x < 1
⊢ exp x ≤ 1 / (1 - x)
rcases eq_or_lt_of_le h1 with (rfl | h1)
no goals
case inl
h1 : 0 ≤ 0
h2 : 0 < 1
⊢ exp 0 ≤ 1 / (1 - 0)
simp
no goals
case inr
x : ℝ
h1✝ : 0 ≤ x
h2 : x < 1
h1 : 0 < x
⊢ exp x ≤ 1 / (1 - x)
exact (exp_bound_div_one_sub_of_interval' h1 h2).le