x✝ y✝ x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ log y < log x
x y : ℝ
⊢ StrictAntiOn log (Iio 0)
rintro x (hx : x < 0) y (hy : y < 0) hxy
x✝ y✝ x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ log (abs y) < log (abs x)
x✝ y✝ x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ log y < log x
rw [← log_abs y, ← log_abs x]
x✝ y✝ x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ abs y < abs x
x✝ y✝ x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ log (abs y) < log (abs x)
refine' log_lt_log (abs_pos.2 hy.ne) _
no goals
x✝ y✝ x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ abs y < abs x
rwa [abs_of_neg hy, abs_of_neg hx, neg_lt_neg_iff]