case inl
x : Ordinal
hx : x ≠ 0
⊢ 0 ^ log 0 x ≤ x

case inr
b x : Ordinal
hx : x ≠ 0
b0 : b ≠ 0
⊢ b ^ log b x ≤ x
b x : Ordinal
hx : x ≠ 0
⊢ b ^ log b x ≤ x
rcases eq_or_ne b 0 with (rfl | b0)
case inr.inl
b x : Ordinal
hx : x ≠ 0
b0 : b ≠ 0
hb : 1 < b
⊢ b ^ log b x ≤ x

case inr.inr
x : Ordinal
hx : x ≠ 0
b0 : 1 ≠ 0
⊢ 1 ^ log 1 x ≤ x
case inr
b x : Ordinal
hx : x ≠ 0
b0 : b ≠ 0
⊢ b ^ log b x ≤ x
rcases lt_or_eq_of_le (one_le_iff_ne_zero.2 b0) with (hb | rfl)
case inl
x : Ordinal
hx : x ≠ 0
⊢ 1 - log 0 x ≤ x
case inl
x : Ordinal
hx : x ≠ 0
⊢ 0 ^ log 0 x ≤ x
rw [zero_opow']
no goals
case inl
x : Ordinal
hx : x ≠ 0
⊢ 1 - log 0 x ≤ x
refine' (sub_le_self _ _).trans (one_le_iff_ne_zero.2 hx)
case inr.inl
b x : Ordinal
hx : x ≠ 0
b0 : b ≠ 0
hb : 1 < b
h : x < b ^ log b x
⊢ succ (log b x) ≤ log b x
case inr.inl
b x : Ordinal
hx : x ≠ 0
b0 : b ≠ 0
hb : 1 < b
⊢ b ^ log b x ≤ x
refine' le_of_not_lt fun h => (lt_succ (log b x)).not_le _
case inr.inl
b x : Ordinal
hx : x ≠ 0
b0 : b ≠ 0
hb : 1 < b
h : x < b ^ log b x
this : sInf {o | x < b ^ o} ≤ log b x
⊢ succ (log b x) ≤ log b x
case inr.inl
b x : Ordinal
hx : x ≠ 0
b0 : b ≠ 0
hb : 1 < b
h : x < b ^ log b x
⊢ succ (log b x) ≤ log b x
have := @csInf_le' _ _ { o | x < (b^o) } _ h
no goals
case inr.inl
b x : Ordinal
hx : x ≠ 0
b0 : b ≠ 0
hb : 1 < b
h : x < b ^ log b x
this : sInf {o | x < b ^ o} ≤ log b x
⊢ succ (log b x) ≤ log b x
rwa [← succ_log_def hb hx] at this
no goals
case inr.inr
x : Ordinal
hx : x ≠ 0
b0 : 1 ≠ 0
⊢ 1 ^ log 1 x ≤ x
rwa [one_opow, one_le_iff_ne_zero]