α : Type ?u.30174
r : α → α → Prop
ι : Type u
f : ι → Ordinal
H : ∀ (i : ι), f i < sup f
⊢ cof (sup f) ≤ Cardinal.lift (#ι)
α : Type ?u.30174
r : α → α → Prop
ι : Type u
f : ι → Ordinal
H : ∀ (i : ι), f i < sup f
⊢ cof (sup f) ≤ (#ι)
rw [← (#ι).lift_id]
no goals
α : Type ?u.30174
r : α → α → Prop
ι : Type u
f : ι → Ordinal
H : ∀ (i : ι), f i < sup f
⊢ cof (sup f) ≤ Cardinal.lift (#ι)
exact cof_sup_le_lift H