no goals
α : Type u_1
β : Type ?u.147900
γ : Type ?u.147903
ι : Sort ?u.147906
ι' : Sort ?u.147909
ι₂ : Sort ?u.147912
κ : ι → Sort ?u.147917
κ₁ : ι → Sort ?u.147922
κ₂ : ι → Sort ?u.147927
κ' : ι' → Sort ?u.147932
S : Set (Set α)
⊢ ⋂₀ S = (⋃₀ (compl '' S))ᶜ
rw [← compl_compl (⋂₀ S), compl_sInter]