case inl
a b : Ordinal
hb : b < ω
c0 : 0 < 0
ha : a < ω ^ 0
⊢ a * b < ω ^ 0

case inr.inl.intro
a b : Ordinal
hb : b < ω
c : Ordinal
c0 : 0 < succ c
ha : a < ω ^ succ c
⊢ a * b < ω ^ succ c

case inr.inr
a b c : Ordinal
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsLimit c
⊢ a * b < ω ^ c
a b c : Ordinal
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
⊢ a * b < ω ^ c
rcases zero_or_succ_or_limit c with (rfl | ⟨c, rfl⟩ | l)
no goals
case inl
a b : Ordinal
hb : b < ω
c0 : 0 < 0
ha : a < ω ^ 0
⊢ a * b < ω ^ 0
exact (lt_irrefl _).elim c0
case inr.inl.intro
a b : Ordinal
hb : b < ω
c : Ordinal
c0 : 0 < succ c
ha : a < ω ^ c * ω
⊢ a * b < ω ^ succ c
case inr.inl.intro
a b : Ordinal
hb : b < ω
c : Ordinal
c0 : 0 < succ c
ha : a < ω ^ succ c
⊢ a * b < ω ^ succ c
rw [opow_succ] at ha
case inr.inl.intro.intro.intro
a b : Ordinal
hb : b < ω
c : Ordinal
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal
hn : n < ω
an : a < (fun x x_1 => x * x_1) (ω ^ c) n
⊢ a * b < ω ^ succ c
case inr.inl.intro
a b : Ordinal
hb : b < ω
c : Ordinal
c0 : 0 < succ c
ha : a < ω ^ c * ω
⊢ a * b < ω ^ succ c
rcases((mul_isNormal <| opow_pos _ omega_pos).limit_lt omega_isLimit).1 ha with ⟨n, hn, an⟩
case inr.inl.intro.intro.intro
a b : Ordinal
hb : b < ω
c : Ordinal
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal
hn : n < ω
an : a < (fun x x_1 => x * x_1) (ω ^ c) n
⊢ (fun x x_1 => x * x_1) (ω ^ c) n * b < ω ^ succ c
case inr.inl.intro.intro.intro
a b : Ordinal
hb : b < ω
c : Ordinal
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal
hn : n < ω
an : a < (fun x x_1 => x * x_1) (ω ^ c) n
⊢ a * b < ω ^ succ c
apply (mul_le_mul_right' (le_of_lt an) _).trans_lt
case inr.inl.intro.intro.intro
a b : Ordinal
hb : b < ω
c : Ordinal
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal
hn : n < ω
an : a < (fun x x_1 => x * x_1) (ω ^ c) n
⊢ n * b < ω
case inr.inl.intro.intro.intro
a b : Ordinal
hb : b < ω
c : Ordinal
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal
hn : n < ω
an : a < (fun x x_1 => x * x_1) (ω ^ c) n
⊢ (fun x x_1 => x * x_1) (ω ^ c) n * b < ω ^ succ c
rw [opow_succ, mul_assoc, mul_lt_mul_iff_left (opow_pos _ omega_pos)]
no goals
case inr.inl.intro.intro.intro
a b : Ordinal
hb : b < ω
c : Ordinal
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal
hn : n < ω
an : a < (fun x x_1 => x * x_1) (ω ^ c) n
⊢ n * b < ω
exact principal_mul_omega hn hb
case inr.inr.intro.intro
a b c : Ordinal
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsLimit c
x : Ordinal
hx : x < c
ax : a < (fun x x_1 => x ^ x_1) ω x
⊢ a * b < ω ^ c
case inr.inr
a b c : Ordinal
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsLimit c
⊢ a * b < ω ^ c
rcases((opow_isNormal one_lt_omega).limit_lt l).1 ha with ⟨x, hx, ax⟩
case inr.inr.intro.intro
a b c : Ordinal
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsLimit c
x : Ordinal
hx : x < c
ax : a < (fun x x_1 => x ^ x_1) ω x
⊢ (fun x x_1 => x ^ x_1) ω x * ω < ω ^ c
case inr.inr.intro.intro
a b c : Ordinal
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsLimit c
x : Ordinal
hx : x < c
ax : a < (fun x x_1 => x ^ x_1) ω x
⊢ a * b < ω ^ c
refine' (mul_le_mul' (le_of_lt ax) (le_of_lt hb)).trans_lt _
case inr.inr.intro.intro
a b c : Ordinal
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsLimit c
x : Ordinal
hx : x < c
ax : a < (fun x x_1 => x ^ x_1) ω x
⊢ succ x < c
case inr.inr.intro.intro
a b c : Ordinal
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsLimit c
x : Ordinal
hx : x < c
ax : a < (fun x x_1 => x ^ x_1) ω x
⊢ (fun x x_1 => x ^ x_1) ω x * ω < ω ^ c
rw [← opow_succ, opow_lt_opow_iff_right one_lt_omega]
no goals
case inr.inr.intro.intro
a b c : Ordinal
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsLimit c
x : Ordinal
hx : x < c
ax : a < (fun x x_1 => x ^ x_1) ω x
⊢ succ x < c
exact l.2 _ hx