α : Type ?u.29854
r : α → α → Prop
ι : Type u
f : ι → Ordinal
H : (sup fun i => f i) = lsub fun i => f i
⊢ cof (sup f) ≤ Cardinal.lift (#ι)
α : Type ?u.29854
r : α → α → Prop
ι : Type u
f : ι → Ordinal
H : ∀ (i : ι), f i < sup f
⊢ cof (sup f) ≤ Cardinal.lift (#ι)
rw [← sup_eq_lsub_iff_lt_sup.{u, v}] at H
α : Type ?u.29854
r : α → α → Prop
ι : Type u
f : ι → Ordinal
H : (sup fun i => f i) = lsub fun i => f i
⊢ cof (lsub fun i => f i) ≤ Cardinal.lift (#ι)
α : Type ?u.29854
r : α → α → Prop
ι : Type u
f : ι → Ordinal
H : (sup fun i => f i) = lsub fun i => f i
⊢ cof (sup f) ≤ Cardinal.lift (#ι)
rw [H]
no goals
α : Type ?u.29854
r : α → α → Prop
ι : Type u
f : ι → Ordinal
H : (sup fun i => f i) = lsub fun i => f i
⊢ cof (lsub fun i => f i) ≤ Cardinal.lift (#ι)
exact cof_lsub_le_lift f