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