no goals
α : Type u_1
β : Type ?u.131162
γ : Type ?u.131165
ι : Sort u_2
ι' : Sort ?u.131171
ι₂ : Sort ?u.131174
κ : ι → Sort u_3
κ₁ : ι → Sort ?u.131184
κ₂ : ι → Sort ?u.131189
κ' : ι' → Sort ?u.131194
s : (i : ι) → κ i → Set α
⊢ (⋂ (i : ι) (j : κ i), s i j) = ∅ ↔ ∀ (a : α), ∃ i j, ¬a ∈ s i j
simp only [eq_empty_iff_forall_not_mem, mem_iInter, not_forall]