α : Type ?u.28987
r : α → α → Prop
ι : Type u
f : ι → Ordinal
hι : Cardinal.lift (#ι) < cof (lsub f)
hf : ∀ (i : ι), f i < lsub f
⊢ False
α : Type ?u.28987
r : α → α → Prop
ι : Type u
f : ι → Ordinal
c : Ordinal
hι : Cardinal.lift (#ι) < cof c
hf : ∀ (i : ι), f i < c
h : lsub f = c
⊢ False
subst h
no goals
α : Type ?u.28987
r : α → α → Prop
ι : Type u
f : ι → Ordinal
hι : Cardinal.lift (#ι) < cof (lsub f)
hf : ∀ (i : ι), f i < lsub f
⊢ False
exact (cof_lsub_le_lift.{u, v} f).not_lt hι