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