apply Nat.pow_log_le_self
case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ b ^ b.log n ≤ n

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

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

case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 0 ≤ (↑b).logb ↑n
case neg.a.hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ n ≠ 0

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

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

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