b : Ordinal
b1 : 1 < b
⊢ sInf {o | 0 < b ^ o} ≤ succ 0
b : Ordinal
b1 : 1 < b
⊢ log b 0 = 0
rw [log_def b1, ← Ordinal.le_zero, pred_le]
case h
b : Ordinal
b1 : 1 < b
⊢ succ 0 ∈ {o | 0 < b ^ o}
b : Ordinal
b1 : 1 < b
⊢ sInf {o | 0 < b ^ o} ≤ succ 0
apply csInf_le'
case h
b : Ordinal
b1 : 1 < b
⊢ 0 < b ^ succ 0
case h
b : Ordinal
b1 : 1 < b
⊢ succ 0 ∈ {o | 0 < b ^ o}
dsimp
case h
b : Ordinal
b1 : 1 < b
⊢ 0 < b
case h
b : Ordinal
b1 : 1 < b
⊢ 0 < b ^ succ 0
rw [succ_zero, opow_one]
no goals
case h
b : Ordinal
b1 : 1 < b
⊢ 0 < b
exact zero_lt_one.trans b1
no goals
b : Ordinal
b1 : ¬1 < b
⊢ log b 0 = 0
simp only [log_of_not_one_lt_left b1]