b x y : ℝ
hb : 1 < b
h : 0 < x
⊢ logb b x < logb ?m.12315 1 ↔ x < 1

b x y : ℝ
hb : 1 < b
h : 0 < x
⊢ ℝ
b x y : ℝ
hb : 1 < b
h : 0 < x
⊢ logb b x < 0 ↔ x < 1
rw [← logb_one]
no goals
b x y : ℝ
hb : 1 < b
h : 0 < x
⊢ logb b x < logb ?m.12315 1 ↔ x < 1

b x y : ℝ
hb : 1 < b
h : 0 < x
⊢ ℝ
exact logb_lt_logb_iff hb h zero_lt_one