no goals
α : Type u_1
β : Type ?u.87716
γ : Type ?u.87719
ι : Sort ?u.87722
κ : ι → Sort ?u.87727
inst✝ : LE α
s t : LowerSet α
a : α
S : Set (LowerSet α)
⊢ ↑(compl (sSup S)) = ↑(⨆ (s : LowerSet α) (_ : s ∈ S), compl s)
simp only [coe_compl, coe_sSup, compl_iUnion₂, UpperSet.coe_iSup₂]