case inl
b x y : ℕ
hb : 1 < b
h : b ^ x ≤ y
hy : y ≠ 0
⊢ x ≤ log b y

case inr
b x : ℕ
hb : 1 < b
h : b ^ x ≤ 0
⊢ x ≤ log b 0
b x y : ℕ
hb : 1 < b
h : b ^ x ≤ y
⊢ x ≤ log b y
rcases ne_or_eq y 0 with (hy | rfl)
no goals
case inl
b x y : ℕ
hb : 1 < b
h : b ^ x ≤ y
hy : y ≠ 0
⊢ x ≤ log b y

case inr
b x : ℕ
hb : 1 < b
h : b ^ x ≤ 0
⊢ x ≤ log b 0
exacts [(pow_le_iff_le_log hb hy).1 h, (h.not_lt (pow_pos (zero_lt_one.trans hb) _)).elim]