no goals
α : Type ?u.35734
r : α → α → Prop
f : Ordinal → Ordinal
c : Ordinal
hc : ℵ₀ < cof c
hf : ∀ (i : Ordinal), i < c → f i < c
a : Ordinal
⊢ Cardinal.lift (#Unit) < cof c
simpa using Cardinal.one_lt_aleph0.trans hc