a b : Ordinal
h : a < ω ^ b
⊢ a + ω ^ b ≤ ω ^ b
a b : Ordinal
h : a < ω ^ b
⊢ a + ω ^ b = ω ^ b
refine' le_antisymm _ (le_add_left _ _)
case H₁
a b : Ordinal
h✝ : a < ω ^ b
h : a < ω ^ 0
⊢ a + ω ^ 0 ≤ ω ^ 0

case H₂
a b✝ : Ordinal
h✝ : a < ω ^ b✝
b : Ordinal
a✝ : a < ω ^ b → a + ω ^ b ≤ ω ^ b
h : a < ω ^ succ b
⊢ a + ω ^ succ b ≤ ω ^ succ b

case H₃
a b✝ : Ordinal
h✝ : a < ω ^ b✝
b : Ordinal
l : IsLimit b
IH : ∀ (o' : Ordinal), o' < b → a < ω ^ o' → a + ω ^ o' ≤ ω ^ o'
h : a < ω ^ b
⊢ a + ω ^ b ≤ ω ^ b
a b : Ordinal
h : a < ω ^ b
⊢ a + ω ^ b ≤ ω ^ b
induction' b using limitRecOn with b _ b l IH
case H₁
a b : Ordinal
h✝ : a < ω ^ b
h : a = 0
⊢ a + ω ^ 0 ≤ ω ^ 0
case H₁
a b : Ordinal
h✝ : a < ω ^ b
h : a < ω ^ 0
⊢ a + ω ^ 0 ≤ ω ^ 0
rw [opow_zero, ← succ_zero, lt_succ_iff, Ordinal.le_zero] at h
no goals
case H₁
a b : Ordinal
h✝ : a < ω ^ b
h : a = 0
⊢ a + ω ^ 0 ≤ ω ^ 0
rw [h, zero_add]
case H₂
a b✝ : Ordinal
h✝ : a < ω ^ b✝
b : Ordinal
a✝ : a < ω ^ b → a + ω ^ b ≤ ω ^ b
h : a < ω ^ b * ω
⊢ a + ω ^ succ b ≤ ω ^ succ b
case H₂
a b✝ : Ordinal
h✝ : a < ω ^ b✝
b : Ordinal
a✝ : a < ω ^ b → a + ω ^ b ≤ ω ^ b
h : a < ω ^ succ b
⊢ a + ω ^ succ b ≤ ω ^ succ b
rw [opow_succ] at h
case H₂.intro.intro
a b✝ : Ordinal
h✝ : a < ω ^ b✝
b : Ordinal
a✝ : a < ω ^ b → a + ω ^ b ≤ ω ^ b
h : a < ω ^ b * ω
x : Ordinal
xo : x < ω
ax : a < ω ^ b * x
⊢ a + ω ^ succ b ≤ ω ^ succ b
case H₂
a b✝ : Ordinal
h✝ : a < ω ^ b✝
b : Ordinal
a✝ : a < ω ^ b → a + ω ^ b ≤ ω ^ b
h : a < ω ^ b * ω
⊢ a + ω ^ succ b ≤ ω ^ succ b
rcases(lt_mul_of_limit omega_isLimit).1 h with ⟨x, xo, ax⟩
case H₂.intro.intro
a b✝ : Ordinal
h✝ : a < ω ^ b✝
b : Ordinal
a✝ : a < ω ^ b → a + ω ^ b ≤ ω ^ b
h : a < ω ^ b * ω
x : Ordinal
xo : x < ω
ax : a < ω ^ b * x
⊢ ω ^ b * x + ω ^ succ b ≤ ω ^ succ b
case H₂.intro.intro
a b✝ : Ordinal
h✝ : a < ω ^ b✝
b : Ordinal
a✝ : a < ω ^ b → a + ω ^ b ≤ ω ^ b
h : a < ω ^ b * ω
x : Ordinal
xo : x < ω
ax : a < ω ^ b * x
⊢ a + ω ^ succ b ≤ ω ^ succ b
refine' le_trans (add_le_add_right (le_of_lt ax) _) _
no goals
case H₂.intro.intro
a b✝ : Ordinal
h✝ : a < ω ^ b✝
b : Ordinal
a✝ : a < ω ^ b → a + ω ^ b ≤ ω ^ b
h : a < ω ^ b * ω
x : Ordinal
xo : x < ω
ax : a < ω ^ b * x
⊢ ω ^ b * x + ω ^ succ b ≤ ω ^ succ b
rw [opow_succ, ← mul_add, add_omega xo]
case H₃.intro.intro
a b✝ : Ordinal
h✝ : a < ω ^ b✝
b : Ordinal
l : IsLimit b
IH : ∀ (o' : Ordinal), o' < b → a < ω ^ o' → a + ω ^ o' ≤ ω ^ o'
h : a < ω ^ b
x : Ordinal
xb : x < b
ax : a < ω ^ x
⊢ a + ω ^ b ≤ ω ^ b
case H₃
a b✝ : Ordinal
h✝ : a < ω ^ b✝
b : Ordinal
l : IsLimit b
IH : ∀ (o' : Ordinal), o' < b → a < ω ^ o' → a + ω ^ o' ≤ ω ^ o'
h : a < ω ^ b
⊢ a + ω ^ b ≤ ω ^ b
rcases(lt_opow_of_limit omega_ne_zero l).1 h with ⟨x, xb, ax⟩
no goals
case H₃.intro.intro
a b✝ : Ordinal
h✝ : a < ω ^ b✝
b : Ordinal
l : IsLimit b
IH : ∀ (o' : Ordinal), o' < b → a < ω ^ o' → a + ω ^ o' ≤ ω ^ o'
h : a < ω ^ b
x : Ordinal
xb : x < b
ax : a < ω ^ x
⊢ a + ω ^ b ≤ ω ^ b
exact
  (((add_isNormal a).trans (opow_isNormal one_lt_omega)).limit_le l).2 fun y yb =>
    (add_le_add_left (opow_le_opow_right omega_pos (le_max_right _ _)) _).trans
      (le_trans
        (IH _ (max_lt xb yb) (ax.trans_le <| opow_le_opow_right omega_pos (le_max_left _ _)))
        (opow_le_opow_right omega_pos <| le_of_lt <| max_lt xb yb))