case pos
a b : Ordinal
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b = 0
⊢ a * ω ^ ω ^ b = ω ^ ω ^ b

case neg
a b : Ordinal
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : ¬b = 0
⊢ a * ω ^ ω ^ b = ω ^ ω ^ b
a b : Ordinal
a0 : 0 < a
h : a < ω ^ ω ^ b
⊢ a * ω ^ ω ^ b = ω ^ ω ^ b
by_cases b0 : b = 0
case neg
a b : Ordinal
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : ¬b = 0
⊢ a * ω ^ ω ^ b ≤ ω ^ ω ^ b
case neg
a b : Ordinal
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : ¬b = 0
⊢ a * ω ^ ω ^ b = ω ^ ω ^ b
refine'
  le_antisymm _
    (by simpa only [one_mul] using mul_le_mul_right' (one_le_iff_pos.2 a0) (omega^omega^b))
case neg.intro.intro
a b : Ordinal
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : ¬b = 0
x : Ordinal
xb : x < ω ^ b
ax : a < ω ^ x
⊢ a * ω ^ ω ^ b ≤ ω ^ ω ^ b
case neg
a b : Ordinal
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : ¬b = 0
⊢ a * ω ^ ω ^ b ≤ ω ^ ω ^ b
rcases(lt_opow_of_limit omega_ne_zero (opow_isLimit_left omega_isLimit b0)).1 h with ⟨x, xb, ax⟩
case neg.intro.intro
a b : Ordinal
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : ¬b = 0
x : Ordinal
xb : x < ω ^ b
ax : a < ω ^ x
⊢ ω ^ x * ω ^ ω ^ b ≤ ω ^ ω ^ b
case neg.intro.intro
a b : Ordinal
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : ¬b = 0
x : Ordinal
xb : x < ω ^ b
ax : a < ω ^ x
⊢ a * ω ^ ω ^ b ≤ ω ^ ω ^ b
apply (mul_le_mul_right' (le_of_lt ax) _).trans
no goals
case neg.intro.intro
a b : Ordinal
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : ¬b = 0
x : Ordinal
xb : x < ω ^ b
ax : a < ω ^ x
⊢ ω ^ x * ω ^ ω ^ b ≤ ω ^ ω ^ b
rw [← opow_add, add_omega_opow xb]
case pos
a b : Ordinal
a0 : 0 < a
h : a < ω
b0 : b = 0
⊢ a * ω = ω
case pos
a b : Ordinal
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b = 0
⊢ a * ω ^ ω ^ b = ω ^ ω ^ b
rw [b0, opow_zero, opow_one] at h⊢
no goals
case pos
a b : Ordinal
a0 : 0 < a
h : a < ω
b0 : b = 0
⊢ a * ω = ω
exact mul_omega a0 h
no goals
a b : Ordinal
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : ¬b = 0
⊢ ω ^ ω ^ b ≤ a * ω ^ ω ^ b
simpa only [one_mul] using mul_le_mul_right' (one_le_iff_pos.2 a0) (omega^omega^b)