no goals
α : Type u_1
β : Type ?u.90446
γ : Type ?u.90449
ι : Sort u_2
κ : ι → Sort u_3
inst✝ : LE α
s t : LowerSet α
a : α
f : (i : ι) → κ i → LowerSet α
⊢ compl (⨆ (i : ι) (j : κ i), f i j) = ⨆ (i : ι) (j : κ i), compl (f i j)
simp_rw [LowerSet.compl_iSup]