case inl
b : Ordinal
hbo : 0 < b
⊢ log b 0 = 0

case inr
b o : Ordinal
hbo : o < b
ho : o ≠ 0
⊢ log b o = 0
b o : Ordinal
hbo : o < b
⊢ log b o = 0
rcases eq_or_ne o 0 with (rfl | ho)
case inr.inl
b o : Ordinal
hbo : o < b
ho : o ≠ 0
hb : b ≤ 1
⊢ log b o = 0

case inr.inr
b o : Ordinal
hbo : o < b
ho : o ≠ 0
hb : 1 < b
⊢ log b o = 0
case inr
b o : Ordinal
hbo : o < b
ho : o ≠ 0
⊢ log b o = 0
cases' le_or_lt b 1 with hb hb
no goals
case inl
b : Ordinal
hbo : 0 < b
⊢ log b 0 = 0
exact log_zero_right b
case inr.inl.inl
o : Ordinal
ho : o ≠ 0
hbo : o < 0
hb : 0 ≤ 1
⊢ log 0 o = 0

case inr.inl.inr
o : Ordinal
ho : o ≠ 0
hbo : o < 1
hb : 1 ≤ 1
⊢ log 1 o = 0
case inr.inl
b o : Ordinal
hbo : o < b
ho : o ≠ 0
hb : b ≤ 1
⊢ log b o = 0
rcases le_one_iff.1 hb with (rfl | rfl)
no goals
case inr.inl.inl
o : Ordinal
ho : o ≠ 0
hbo : o < 0
hb : 0 ≤ 1
⊢ log 0 o = 0
exact log_zero_left o
no goals
case inr.inl.inr
o : Ordinal
ho : o ≠ 0
hbo : o < 1
hb : 1 ≤ 1
⊢ log 1 o = 0
exact log_one_left o
no goals
case inr.inr
b o : Ordinal
hbo : o < b
ho : o ≠ 0
hb : 1 < b
⊢ log b o = 0
rwa [← Ordinal.le_zero, ← lt_succ_iff, succ_zero, ← lt_opow_iff_log_lt hb ho, opow_one]