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