x✝ y x : ℝ
hx : 0 < x
⊢ log x + 1 ≤ x
x✝ y x : ℝ
hx : 0 < x
⊢ log x ≤ x - 1
rw [le_sub_iff_add_le]
case h.e'_4
x✝ y x : ℝ
hx : 0 < x
⊢ x = exp (log x)
x✝ y x : ℝ
hx : 0 < x
⊢ log x + 1 ≤ x
convert add_one_le_exp (log x)
no goals
case h.e'_4
x✝ y x : ℝ
hx : 0 < x
⊢ x = exp (log x)
rw [exp_log hx]