no goals
α : Type ?u.40577
r : α → α → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
c : Ordinal
ho : card o < cof c
hf : ∀ (i : Ordinal) (hi : i < o), f i hi < c
⊢ Cardinal.lift (card o) < cof c
rwa [o.card.lift_id]