case intro
n : ℕ
h : ↑n < ω
⊢ ↑n + ω = ω
a : Ordinal
h : a < ω
⊢ a + ω = ω
rcases lt_omega.1 h with ⟨n, rfl⟩
case intro
n : ℕ
⊢ ↑n + ω = ω
case intro
n : ℕ
h : ↑n < ω
⊢ ↑n + ω = ω
clear h
case intro.zero

⊢ ↑Nat.zero + ω = ω

case intro.succ
n : ℕ
IH : ↑n + ω = ω
⊢ ↑(Nat.succ n) + ω = ω
case intro
n : ℕ
⊢ ↑n + ω = ω
induction' n with n IH
no goals
case intro.zero

⊢ ↑Nat.zero + ω = ω
rw [Nat.cast_zero, zero_add]
no goals
case intro.succ
n : ℕ
IH : ↑n + ω = ω
⊢ ↑(Nat.succ n) + ω = ω
rwa [Nat.cast_succ, add_assoc, one_add_of_omega_le (le_refl _)]