α : Type ?u.67959
r : α → α → Prop
a o : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
⊢ ord (cof (blsub o f)) ≤ o
α : Type ?u.67959
r : α → α → Prop
a o : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
⊢ ord (cof a) ≤ o
rw [← hf.2.2]
no goals
α : Type ?u.67959
r : α → α → Prop
a o : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
⊢ ord (cof (blsub o f)) ≤ o
exact (ord_le_ord.2 (cof_blsub_le f)).trans (ord_card_le o)