apply le_antisymm
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n) = log b n + 1
case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n) ≤ log b n + 1

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)