case H₁
a b c : Ordinal
⊢ a + 0 ≤ a ♯ 0

case H₂
a b c : Ordinal
⊢ ∀ (o : Ordinal), a + o ≤ a ♯ o → a + succ o ≤ a ♯ succ o

case H₃
a b c : Ordinal
⊢ ∀ (o : Ordinal), IsLimit o → (∀ (o' : Ordinal), o' < o → a + o' ≤ a ♯ o') → a + o ≤ a ♯ o
a b c : Ordinal
⊢ a + b ≤ a ♯ b
apply b.limitRecOn
no goals
case H₁
a b c : Ordinal
⊢ a + 0 ≤ a ♯ 0
simp
case H₂
a b c✝ c : Ordinal
h : a + c ≤ a ♯ c
⊢ a + succ c ≤ a ♯ succ c
case H₂
a b c : Ordinal
⊢ ∀ (o : Ordinal), a + o ≤ a ♯ o → a + succ o ≤ a ♯ succ o
intro c h
no goals
case H₂
a b c✝ c : Ordinal
h : a + c ≤ a ♯ c
⊢ a + succ c ≤ a ♯ succ c
rwa [add_succ, nadd_succ, succ_le_succ_iff]
case H₃
a b c✝ c : Ordinal
hc : IsLimit c
H : ∀ (o' : Ordinal), o' < c → a + o' ≤ a ♯ o'
⊢ a + c ≤ a ♯ c
case H₃
a b c : Ordinal
⊢ ∀ (o : Ordinal), IsLimit o → (∀ (o' : Ordinal), o' < o → a + o' ≤ a ♯ o') → a + o ≤ a ♯ o
intro c hc H
case H₃
a b c✝ c : Ordinal
hc : IsLimit c
H : ∀ (o' : Ordinal), o' < c → a + o' ≤ a ♯ o'
⊢ ∀ (i : Ordinal), i < c → a + i < a ♯ c
case H₃
a b c✝ c : Ordinal
hc : IsLimit c
H : ∀ (o' : Ordinal), o' < c → a + o' ≤ a ♯ o'
⊢ a + c ≤ a ♯ c
simp_rw [← IsNormal.blsub_eq.{u, u} (add_isNormal a) hc, blsub_le_iff]
no goals
case H₃
a b c✝ c : Ordinal
hc : IsLimit c
H : ∀ (o' : Ordinal), o' < c → a + o' ≤ a ♯ o'
⊢ ∀ (i : Ordinal), i < c → a + i < a ♯ c
exact fun i hi => (H i hi).trans_lt (nadd_lt_nadd_left hi a)