no goals
α : Type u_1
β : Type ?u.89932
γ : Type ?u.89935
ι : Sort u_2
κ : ι → Sort ?u.89943
inst✝ : LE α
s t : LowerSet α
a : α
f : ι → LowerSet α
⊢ ↑(compl (⨅ (i : ι), f i)) = ↑(⨅ (i : ι), compl (f i))
simp only [coe_compl, coe_iInf, compl_iInter, UpperSet.coe_iInf]