α : Type ?u.30918
r : α → α → Prop
ι : Type u
f : ι → Cardinal
c : Cardinal
hι : Cardinal.lift (#ι) < cof (ord c)
hf : ∀ (i : ι), f i < c
⊢ (⨆ (i : ι), ord (f i)) < ord c
α : Type ?u.30918
r : α → α → Prop
ι : Type u
f : ι → Cardinal
c : Cardinal
hι : Cardinal.lift (#ι) < cof (ord c)
hf : ∀ (i : ι), f i < c
⊢ iSup f < c
rw [← ord_lt_ord, iSup_ord (Cardinal.bddAbove_range.{u, v} _)]
α : Type ?u.30918
r : α → α → Prop
ι : Type u
f : ι → Cardinal
c : Cardinal
hι : Cardinal.lift (#ι) < cof (ord c)
hf : ∀ (i : ι), f i < c
i : ι
⊢ ord (f i) < ord c
α : Type ?u.30918
r : α → α → Prop
ι : Type u
f : ι → Cardinal
c : Cardinal
hι : Cardinal.lift (#ι) < cof (ord c)
hf : ∀ (i : ι), f i < c
⊢ (⨆ (i : ι), ord (f i)) < ord c
refine' sup_lt_ord_lift hι fun i => _
α : Type ?u.30918
r : α → α → Prop
ι : Type u
f : ι → Cardinal
c : Cardinal
hι : Cardinal.lift (#ι) < cof (ord c)
hf : ∀ (i : ι), f i < c
i : ι
⊢ f i < c
α : Type ?u.30918
r : α → α → Prop
ι : Type u
f : ι → Cardinal
c : Cardinal
hι : Cardinal.lift (#ι) < cof (ord c)
hf : ∀ (i : ι), f i < c
i : ι
⊢ ord (f i) < ord c
rw [ord_lt_ord]
no goals
α : Type ?u.30918
r : α → α → Prop
ι : Type u
f : ι → Cardinal
c : Cardinal
hι : Cardinal.lift (#ι) < cof (ord c)
hf : ∀ (i : ι), f i < c
i : ι
⊢ f i < c
apply hf