-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem add_omega0_opow (h : a < ω ^ b) : a + ω ^ b = ω ^ b

Proof state:
case H₁
a b : Ordinal.{u}
h : a = 0
⊢ a + ω ^ 0 ≤ ω ^ 0

Tactic:
rw [h, zero_add]

Result:
no goals

Proof state:
case H₂
a b✝ b : Ordinal.{u}
a✝ : a < ω ^ b → a + ω ^ b ≤ ω ^ b
h : a < ω ^ b * ω
⊢ a + ω ^ succ b ≤ ω ^ succ b

Tactic:
rcases (lt_mul_of_limit isLimit_omega0).1 h with ⟨x, xo, ax⟩

Result:
case H₂.intro.intro
a b✝ b : Ordinal.{u}
a✝ : a < ω ^ b → a + ω ^ b ≤ ω ^ b
h : a < ω ^ b * ω
x : Ordinal.{u}
xo : x < ω
ax : a < ω ^ b * x
⊢ a + ω ^ succ b ≤ ω ^ succ b

Proof state:
case H₃.intro.intro
a b✝ b : Ordinal.{u}
l : b.IsLimit
IH : ∀ o' < b, a < ω ^ o' → a + ω ^ o' ≤ ω ^ o'
h : a < ω ^ b
x : Ordinal.{u}
xb : x < b
ax : a < ω ^ x
y : Ordinal.{u}
yb : y < b
⊢ ((fun x => a + x) ∘ fun x => ω ^ x) y ≤ ω ^ b

Tactic:
calc a + ω ^ y ≤ a + ω ^ max x y :=
  add_le_add_left (opow_le_opow_right omega0_pos (le_max_right x y)) _
_ ≤ ω ^ max x y :=
  IH _ (max_lt xb yb) <| ax.trans_le <| opow_le_opow_right omega0_pos <| le_max_left x y
_ ≤ ω ^ b :=
  opow_le_opow_right omega0_pos <| (max_lt xb yb).le

Result:
no goals

Proof state:
case H₂
a b✝ b : Ordinal.{u}
a✝ : a < ω ^ b → a + ω ^ b ≤ ω ^ b
h : a < ω ^ succ b
⊢ a + ω ^ succ b ≤ ω ^ succ b

Tactic:
rw [opow_succ] at h

Result:
case H₂
a b✝ b : Ordinal.{u}
a✝ : a < ω ^ b → a + ω ^ b ≤ ω ^ b
h : a < ω ^ b * ω
⊢ a + ω ^ succ b ≤ ω ^ succ b

Proof state:
case H₃
a b✝ b : Ordinal.{u}
l : b.IsLimit
IH : ∀ o' < b, a < ω ^ o' → a + ω ^ o' ≤ ω ^ o'
h : a < ω ^ b
⊢ a + ω ^ b ≤ ω ^ b

Tactic:
rcases (lt_opow_of_limit omega0_ne_zero l).1 h with ⟨x, xb, ax⟩

Result:
case H₃.intro.intro
a b✝ b : Ordinal.{u}
l : b.IsLimit
IH : ∀ o' < b, a < ω ^ o' → a + ω ^ o' ≤ ω ^ o'
h : a < ω ^ b
x : Ordinal.{u}
xb : x < b
ax : a < ω ^ x
⊢ a + ω ^ b ≤ ω ^ b

Proof state:
case H₃.intro.intro
a b✝ b : Ordinal.{u}
l : b.IsLimit
IH : ∀ o' < b, a < ω ^ o' → a + ω ^ o' ≤ ω ^ o'
h : a < ω ^ b
x : Ordinal.{u}
xb : x < b
ax : a < ω ^ x
⊢ a + ω ^ b ≤ ω ^ b

Tactic:
apply (((isNormal_add_right a).trans <| isNormal_opow one_lt_omega0).limit_le l).2

Result:
case H₃.intro.intro
a b✝ b : Ordinal.{u}
l : b.IsLimit
IH : ∀ o' < b, a < ω ^ o' → a + ω ^ o' ≤ ω ^ o'
h : a < ω ^ b
x : Ordinal.{u}
xb : x < b
ax : a < ω ^ x
⊢ ∀ b_1 < b, ((fun x => a + x) ∘ fun x => ω ^ x) b_1 ≤ ω ^ b

Proof state:
case H₃.intro.intro
a b✝ b : Ordinal.{u}
l : b.IsLimit
IH : ∀ o' < b, a < ω ^ o' → a + ω ^ o' ≤ ω ^ o'
h : a < ω ^ b
x : Ordinal.{u}
xb : x < b
ax : a < ω ^ x
⊢ ∀ b_1 < b, ((fun x => a + x) ∘ fun x => ω ^ x) b_1 ≤ ω ^ b

Tactic:
intro y yb

Result:
case H₃.intro.intro
a b✝ b : Ordinal.{u}
l : b.IsLimit
IH : ∀ o' < b, a < ω ^ o' → a + ω ^ o' ≤ ω ^ o'
h : a < ω ^ b
x : Ordinal.{u}
xb : x < b
ax : a < ω ^ x
y : Ordinal.{u}
yb : y < b
⊢ ((fun x => a + x) ∘ fun x => ω ^ x) y ≤ ω ^ b

Proof state:
a b : Ordinal.{u}
h : a < ω ^ b
⊢ a + ω ^ b = ω ^ b

Tactic:
refine le_antisymm ?_ (le_add_left _ a)

Result:
a b : Ordinal.{u}
h : a < ω ^ b
⊢ a + ω ^ b ≤ ω ^ b

Proof state:
case H₁
a b : Ordinal.{u}
h : a < ω ^ 0
⊢ a + ω ^ 0 ≤ ω ^ 0

Tactic:
rw [opow_zero, ← succ_zero, lt_succ_iff, Ordinal.le_zero] at h

Result:
case H₁
a b : Ordinal.{u}
h : a = 0
⊢ a + ω ^ 0 ≤ ω ^ 0

Proof state:
case H₂.intro.intro
a b✝ b : Ordinal.{u}
a✝ : a < ω ^ b → a + ω ^ b ≤ ω ^ b
h : a < ω ^ b * ω
x : Ordinal.{u}
xo : x < ω
ax : a < ω ^ b * x
⊢ ω ^ b * x + ω ^ succ b ≤ ω ^ succ b

Tactic:
rw [opow_succ, ← mul_add, add_omega0 xo]

Result:
no goals

Proof state:
case H₂.intro.intro
a b✝ b : Ordinal.{u}
a✝ : a < ω ^ b → a + ω ^ b ≤ ω ^ b
h : a < ω ^ b * ω
x : Ordinal.{u}
xo : x < ω
ax : a < ω ^ b * x
⊢ a + ω ^ succ b ≤ ω ^ succ b

Tactic:
apply (add_le_add_right ax.le _).trans

Result:
case H₂.intro.intro
a b✝ b : Ordinal.{u}
a✝ : a < ω ^ b → a + ω ^ b ≤ ω ^ b
h : a < ω ^ b * ω
x : Ordinal.{u}
xo : x < ω
ax : a < ω ^ b * x
⊢ ω ^ b * x + ω ^ succ b ≤ ω ^ succ b

Proof state:
a b : Ordinal.{u}
h : a < ω ^ b
⊢ a + ω ^ b ≤ ω ^ b

Tactic:
induction' b using limitRecOn with b _ b l IH

Result:
case H₁
a b : Ordinal.{u}
h : a < ω ^ 0
⊢ a + ω ^ 0 ≤ ω ^ 0

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

case H₃
a b✝ b : Ordinal.{u}
l : b.IsLimit
IH : ∀ o' < b, a < ω ^ o' → a + ω ^ o' ≤ ω ^ o'
h : a < ω ^ b
⊢ a + ω ^ b ≤ ω ^ b