α : Type ?u.22098
r : α → α → Prop
ι : Type u
f : ι → Ordinal
⊢ cof (lsub f) ≤ (#ULift ι)
α : Type ?u.22098
r : α → α → Prop
ι : Type u
f : ι → Ordinal
⊢ cof (lsub f) ≤ Cardinal.lift (#ι)
rw [← mk_uLift.{u, v}]
case h.e'_3.h.e'_1
α : Type ?u.22098
r : α → α → Prop
ι : Type u
f : ι → Ordinal
⊢ lsub f = lsub fun i => f i.down
α : Type ?u.22098
r : α → α → Prop
ι : Type u
f : ι → Ordinal
⊢ cof (lsub f) ≤ (#ULift ι)
convert cof_lsub_le.{max u v} fun i : ULift.{v, u} ι => f i.down
no goals
case h.e'_3.h.e'_1
α : Type ?u.22098
r : α → α → Prop
ι : Type u
f : ι → Ordinal
⊢ lsub f = lsub fun i => f i.down
exact
  lsub_eq_of_range_eq.{u, max u v, max u v}
    (Set.ext fun x => ⟨fun ⟨i, hi⟩ => ⟨ULift.up.{v, u} i, hi⟩, fun ⟨i, hi⟩ => ⟨_, hi⟩⟩)