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