no goals
α : Type u_1
β : Type ?u.84048
γ : Type ?u.84051
ι : Sort u_2
κ : ι → Sort ?u.84059
inst✝ : LE α
s t : UpperSet α
a : α
f : ι → UpperSet α
⊢ ↑(compl (⨆ (i : ι), f i)) = ↑(⨆ (i : ι), compl (f i))
simp only [coe_compl, coe_iSup, compl_iInter, LowerSet.coe_iSup]