no goals
α : Type u_1
β : Type ?u.67630
γ : Type ?u.67633
ι : Sort u_2
ι' : Sort ?u.67639
ι₂ : Sort ?u.67642
κ : ι → Sort u_3
κ₁ : ι → Sort ?u.67652
κ₂ : ι → Sort ?u.67657
κ' : ι' → Sort ?u.67662
s : (i : ι) → κ i → Set α
⊢ (⋃ (i : ι) (j : κ i), s i j)ᶜ = ⋂ (i : ι) (j : κ i), s i jᶜ
simp_rw [compl_iUnion]