no goals
α : Type u_1
β : Type ?u.147726
γ : Type ?u.147729
ι : Sort ?u.147732
ι' : Sort ?u.147735
ι₂ : Sort ?u.147738
κ : ι → Sort ?u.147743
κ₁ : ι → Sort ?u.147748
κ₂ : ι → Sort ?u.147753
κ' : ι' → Sort ?u.147758
S : Set (Set α)
⊢ (⋂₀ S)ᶜ = ⋃₀ (compl '' S)
rw [sUnion_eq_compl_sInter_compl, compl_compl_image]