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