F : Type ?u.419112
α : Type u_1
β : Type ?u.419118
γ : Type ?u.419121
ι : Type ?u.419124
κ : Type ?u.419127
ι' : Sort u_2
inst✝ : CompleteLattice α
s : ι' → α
⊢ (⨆ (x : PLift ι'), s (↑Equiv.plift x)) = ⨆ (i : PLift ι'), s i.down
F : Type ?u.419112
α : Type u_1
β : Type ?u.419118
γ : Type ?u.419121
ι : Type ?u.419124
κ : Type ?u.419127
ι' : Sort u_2
inst✝ : CompleteLattice α
s : ι' → α
⊢ (⨆ (i : ι'), s i) = ⨆ (t : Finset (PLift ι')) (i : PLift ι') (_ : i ∈ t), s i.down
rw [← iSup_eq_iSup_finset, ← Equiv.plift.surjective.iSup_comp]
no goals
F : Type ?u.419112
α : Type u_1
β : Type ?u.419118
γ : Type ?u.419121
ι : Type ?u.419124
κ : Type ?u.419127
ι' : Sort u_2
inst✝ : CompleteLattice α
s : ι' → α
⊢ (⨆ (x : PLift ι'), s (↑Equiv.plift x)) = ⨆ (i : PLift ι'), s i.down
rfl