no goals
α : Type ?u.69319
β : Type u_1
γ : Type ?u.69325
ι : Sort u_2
ι' : Sort ?u.69331
ι₂ : Sort ?u.69334
κ : ι → Sort ?u.69339
κ₁ : ι → Sort ?u.69344
κ₂ : ι → Sort ?u.69349
κ' : ι' → Sort ?u.69354
s : ι → Set β
⊢ (⋂ (i : ι), s i) = (⋃ (i : ι), s iᶜ)ᶜ
simp only [compl_iUnion, compl_compl]