no goals
α : Type u_1
β : Type ?u.68398
γ : Type ?u.68401
ι : Sort u_2
ι' : Sort ?u.68407
ι₂ : Sort ?u.68410
κ : ι → Sort u_3
κ₁ : ι → Sort ?u.68420
κ₂ : ι → Sort ?u.68425
κ' : ι' → Sort ?u.68430
s : (i : ι) → κ i → Set α
⊢ (⋂ (i : ι) (j : κ i), s i j)ᶜ = ⋃ (i : ι) (j : κ i), s i jᶜ
simp_rw [compl_iInter]