x y : ℝ
hx : 0 < x
h : x < y
⊢ log x < log y
x y : ℝ
hx : 0 < x
⊢ x < y → log x < log y
intro h
no goals
x y : ℝ
hx : 0 < x
h : x < y
⊢ log x < log y
rwa [← exp_lt_exp, exp_log hx, exp_log (lt_trans hx h)]