by_cases hn : n = 0
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
⊢ b.log n = ⌊(↑b).logb ↑n⌋₊
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : n = 0
⊢ b.log n = ⌊(↑b).logb ↑n⌋₊

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
⊢ b.log n = ⌊(↑b).logb ↑n⌋₊