o : Ordinal
h : o < ω
n : ℕ
e : o = ↑n
⊢ succ o < ω
o : Ordinal
h : o < ω
⊢ succ o < ω
let ⟨n, e⟩ := lt_omega.1 h
o : Ordinal
h : o < ω
n : ℕ
e : o = ↑n
⊢ succ ↑n < ω
o : Ordinal
h : o < ω
n : ℕ
e : o = ↑n
⊢ succ o < ω
rw [e]
no goals
o : Ordinal
h : o < ω
n : ℕ
e : o = ↑n
⊢ succ ↑n < ω
exact nat_lt_omega (n + 1)