case h
x y : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
⊢ log x ≠ 0

x y : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
h : log x ≠ 0
⊢ log x < x - 1
x y : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
⊢ log x < x - 1
have h : log x ≠ 0
no goals
x y : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
h : log x ≠ 0
⊢ log x < x - 1
linarith [add_one_lt_exp_of_nonzero h, exp_log hx1]
case h
x y : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
⊢ 1 ∈ Ioi 0
case h
x y : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
⊢ log x ≠ 0
rwa [← log_one, log_injOn_pos.ne_iff hx1]
no goals
case h
x y : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
⊢ 1 ∈ Ioi 0
exact mem_Ioi.mpr zero_lt_one