b x : Ordinal
hb : 1 < b
hx : x ≠ 0
t : Ordinal := sInf {o | x < b ^ o}
⊢ succ (log b x) = sInf {o | x < b ^ o}
b x : Ordinal
hb : 1 < b
hx : x ≠ 0
⊢ succ (log b x) = sInf {o | x < b ^ o}
let t := sInf { o | x < (b^o) }
b x : Ordinal
hb : 1 < b
hx : x ≠ 0
t : Ordinal := sInf {o | x < b ^ o}
this : x < b ^ t
⊢ succ (log b x) = sInf {o | x < b ^ o}
b x : Ordinal
hb : 1 < b
hx : x ≠ 0
t : Ordinal := sInf {o | x < b ^ o}
⊢ succ (log b x) = sInf {o | x < b ^ o}
have : x < (b^t) := csInf_mem (log_nonempty hb)
case inl
b x : Ordinal
hb : 1 < b
hx : x ≠ 0
t : Ordinal := sInf {o | x < b ^ o}
this : x < b ^ t
h : t = 0
⊢ succ (log b x) = sInf {o | x < b ^ o}

case inr.inl
b x : Ordinal
hb : 1 < b
hx : x ≠ 0
t : Ordinal := sInf {o | x < b ^ o}
this : x < b ^ t
h : ∃ a, t = succ a
⊢ succ (log b x) = sInf {o | x < b ^ o}

case inr.inr
b x : Ordinal
hb : 1 < b
hx : x ≠ 0
t : Ordinal := sInf {o | x < b ^ o}
this : x < b ^ t
h : IsLimit t
⊢ succ (log b x) = sInf {o | x < b ^ o}
b x : Ordinal
hb : 1 < b
hx : x ≠ 0
t : Ordinal := sInf {o | x < b ^ o}
this : x < b ^ t
⊢ succ (log b x) = sInf {o | x < b ^ o}
rcases zero_or_succ_or_limit t with (h | h | h)
case inl
b x : Ordinal
hb : 1 < b
hx : x ≠ 0
t : Ordinal := sInf {o | x < b ^ o}
this : x < b ^ t
h : t = 0
⊢ x < 1
case inl
b x : Ordinal
hb : 1 < b
hx : x ≠ 0
t : Ordinal := sInf {o | x < b ^ o}
this : x < b ^ t
h : t = 0
⊢ succ (log b x) = sInf {o | x < b ^ o}
refine' ((one_le_iff_ne_zero.2 hx).not_lt _).elim
no goals
case inl
b x : Ordinal
hb : 1 < b
hx : x ≠ 0
t : Ordinal := sInf {o | x < b ^ o}
this : x < b ^ t
h : t = 0
⊢ x < 1
simpa only [h, opow_zero] using this
no goals
case inr.inl
b x : Ordinal
hb : 1 < b
hx : x ≠ 0
t : Ordinal := sInf {o | x < b ^ o}
this : x < b ^ t
h : ∃ a, t = succ a
⊢ succ (log b x) = sInf {o | x < b ^ o}
rw [show log b x = pred t from log_def hb x, succ_pred_iff_is_succ.2 h]
case inr.inr.intro.intro
b x : Ordinal
hb : 1 < b
hx : x ≠ 0
t : Ordinal := sInf {o | x < b ^ o}
this : x < b ^ t
h : IsLimit t
a : Ordinal
h₁ : a < t
h₂ : x < b ^ a
⊢ succ (log b x) = sInf {o | x < b ^ o}
case inr.inr
b x : Ordinal
hb : 1 < b
hx : x ≠ 0
t : Ordinal := sInf {o | x < b ^ o}
this : x < b ^ t
h : IsLimit t
⊢ succ (log b x) = sInf {o | x < b ^ o}
rcases(lt_opow_of_limit (zero_lt_one.trans hb).ne' h).1 this with ⟨a, h₁, h₂⟩
no goals
case inr.inr.intro.intro
b x : Ordinal
hb : 1 < b
hx : x ≠ 0
t : Ordinal := sInf {o | x < b ^ o}
this : x < b ^ t
h : IsLimit t
a : Ordinal
h₁ : a < t
h₂ : x < b ^ a
⊢ succ (log b x) = sInf {o | x < b ^ o}
exact h₁.not_le.elim ((le_csInf_iff'' (log_nonempty hb)).1 le_rfl a h₂)