no goals
α : Type u_1
β : Type ?u.88567
γ : Type ?u.88570
ι : Sort ?u.88573
κ : ι → Sort ?u.88578
inst✝ : LE α
s t : LowerSet α
a : α
S : Set (LowerSet α)
⊢ ↑(compl (sInf S)) = ↑(⨅ (s : LowerSet α) (_ : s ∈ S), compl s)
simp only [coe_compl, coe_sInf, compl_iInter₂, UpperSet.coe_iInf₂]