case inl
b : Ordinal
hb : 1 < b
⊢ 0 < b ^ succ (log b 0)

case inr
b : Ordinal
hb : 1 < b
x : Ordinal
hx : x ≠ 0
⊢ x < b ^ succ (log b x)
b : Ordinal
hb : 1 < b
x : Ordinal
⊢ x < b ^ succ (log b x)
rcases eq_or_ne x 0 with (rfl | hx)
no goals
case inl
b : Ordinal
hb : 1 < b
⊢ 0 < b ^ succ (log b 0)
apply opow_pos _ (zero_lt_one.trans hb)
case inr
b : Ordinal
hb : 1 < b
x : Ordinal
hx : x ≠ 0
⊢ x < b ^ sInf {o | x < b ^ o}
case inr
b : Ordinal
hb : 1 < b
x : Ordinal
hx : x ≠ 0
⊢ x < b ^ succ (log b x)
rw [succ_log_def hb hx]
no goals
case inr
b : Ordinal
hb : 1 < b
x : Ordinal
hx : x ≠ 0
⊢ x < b ^ sInf {o | x < b ^ o}
exact csInf_mem (log_nonempty hb)