b u v w : Ordinal
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
⊢ log b (b ^ u * v + w) = u
b u v w : Ordinal
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
⊢ log b (b ^ u * v + w) = u
have hne' := (opow_mul_add_pos (zero_lt_one.trans hb).ne' u hv w).ne'
b u v w : Ordinal
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : ¬log b (b ^ u * v + w) = u
⊢ False
b u v w : Ordinal
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
⊢ log b (b ^ u * v + w) = u
by_contra' hne
case inl
b u v w : Ordinal
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : ¬log b (b ^ u * v + w) = u
h : log b (b ^ u * v + w) < u
⊢ False

case inr
b u v w : Ordinal
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : ¬log b (b ^ u * v + w) = u
h : log b (b ^ u * v + w) > u
⊢ False
b u v w : Ordinal
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : ¬log b (b ^ u * v + w) = u
⊢ False
cases' lt_or_gt_of_ne hne with h h
case inl
b u v w : Ordinal
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : ¬log b (b ^ u * v + w) = u
h : b ^ u * v + w < b ^ u
⊢ False
case inl
b u v w : Ordinal
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : ¬log b (b ^ u * v + w) = u
h : log b (b ^ u * v + w) < u
⊢ False
rw [← lt_opow_iff_log_lt hb hne'] at h
no goals
case inl
b u v w : Ordinal
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : ¬log b (b ^ u * v + w) = u
h : b ^ u * v + w < b ^ u
⊢ False
exact h.not_le ((le_mul_left _ (Ordinal.pos_iff_ne_zero.2 hv)).trans (le_add_right _ _))
case inr
b u v w : Ordinal
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : ¬log b (b ^ u * v + w) = u
h : u < log b (b ^ u * v + w)
⊢ False
case inr
b u v w : Ordinal
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : ¬log b (b ^ u * v + w) = u
h : log b (b ^ u * v + w) > u
⊢ False
conv at h => change u < log b (b ^ u * v + w)
case inr
b u v w : Ordinal
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : ¬log b (b ^ u * v + w) = u
h✝ : u < log b (b ^ u * v + w)
h : b ^ succ u ≤ b ^ u * v + w
⊢ False
case inr
b u v w : Ordinal
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : ¬log b (b ^ u * v + w) = u
h : u < log b (b ^ u * v + w)
⊢ False
rw [← succ_le_iff, ← opow_le_iff_le_log hb hne'] at h
no goals
case inr
b u v w : Ordinal
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : ¬log b (b ^ u * v + w) = u
h✝ : u < log b (b ^ u * v + w)
h : b ^ succ u ≤ b ^ u * v + w
⊢ False
exact (not_lt_of_le h) (opow_mul_add_lt_opow_succ hvb hw)