case inl
b o : Ordinal
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
h : o % b ^ log b o = 0
⊢ log b (o % b ^ log b o) < log b o

case inr
b o : Ordinal
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ log b (o % b ^ log b o) < log b o
b o : Ordinal
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
⊢ log b (o % b ^ log b o) < log b o
cases' eq_or_ne (o % (b^log b o)) 0 with h h
case inl
b o : Ordinal
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
h : o % b ^ log b o = 0
⊢ 0 < log b o
case inl
b o : Ordinal
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
h : o % b ^ log b o = 0
⊢ log b (o % b ^ log b o) < log b o
rw [h, log_zero_right]
no goals
case inl
b o : Ordinal
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
h : o % b ^ log b o = 0
⊢ 0 < log b o
apply log_pos hb ho hbo
case inr
b o : Ordinal
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ sInf {o_1 | o % b ^ log b o < b ^ o_1} ≤ log b o
case inr
b o : Ordinal
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ log b (o % b ^ log b o) < log b o
rw [← succ_le_iff, succ_log_def hb h]
case inr.h
b o : Ordinal
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ log b o ∈ {o_1 | o % b ^ log b o < b ^ o_1}
case inr
b o : Ordinal
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ sInf {o_1 | o % b ^ log b o < b ^ o_1} ≤ log b o
apply csInf_le'
case inr.h.h
b o : Ordinal
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ b ^ log b o ≠ 0
case inr.h
b o : Ordinal
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ log b o ∈ {o_1 | o % b ^ log b o < b ^ o_1}
apply mod_lt
case inr.h.h
b o : Ordinal
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ 0 < b ^ log b o
case inr.h.h
b o : Ordinal
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ b ^ log b o ≠ 0
rw [← Ordinal.pos_iff_ne_zero]
no goals
case inr.h.h
b o : Ordinal
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ 0 < b ^ log b o
exact opow_pos _ (zero_lt_one.trans hb)