b x y : ℝ
hb : 1 < b
hx : 0 < x
⊢ logb b 1 < logb b x ↔ 1 < x
b x y : ℝ
hb : 1 < b
hx : 0 < x
⊢ 0 < logb b x ↔ 1 < x
rw [← @logb_one b]
no goals
b x y : ℝ
hb : 1 < b
hx : 0 < x
⊢ logb b 1 < logb b x ↔ 1 < x
rw [logb_lt_logb_iff hb zero_lt_one hx]