no goals
α : Type ?u.39723
r : α → α → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
c : Ordinal
ho : Cardinal.lift (card o) < cof c
hf : ∀ (i : Ordinal) (hi : i < o), f i hi < c
h : blsub o f = c
⊢ cof c ≤ Cardinal.lift (card o)
simpa [← iSup_ord, hf, h] using cof_blsub_le_lift.{u, v} f