α : Type ?u.38775
r : α → α → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ cof (blsub o f) ≤ Cardinal.lift (#(Quotient.out o).α)
α : Type ?u.38775
r : α → α → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ cof (blsub o f) ≤ Cardinal.lift (card o)
rw [← mk_ordinal_out o]
no goals
α : Type ?u.38775
r : α → α → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ cof (blsub o f) ≤ Cardinal.lift (#(Quotient.out o).α)
exact cof_lsub_le_lift _