no goals
α : Type u_1
β : Type ?u.147561
γ : Type ?u.147564
ι : Sort ?u.147567
ι' : Sort ?u.147570
ι₂ : Sort ?u.147573
κ : ι → Sort ?u.147578
κ₁ : ι → Sort ?u.147583
κ₂ : ι → Sort ?u.147588
κ' : ι' → Sort ?u.147593
S : Set (Set α)
⊢ ⋃₀ S = (⋂₀ (compl '' S))ᶜ
rw [← compl_compl (⋃₀S), compl_sUnion]