no goals
α : Type ?u.168645
r : α → α → Prop
f : Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hc' : c ≠ ℵ₀
hf : ∀ (i : Ordinal), i < ord c → f i < ord c
a : Ordinal
⊢ lift (#Unit) < c
simpa using Cardinal.one_lt_aleph0.trans (lt_of_le_of_ne hc.1 hc'.symm)