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