no goals
α : Type u_1
β : Type ?u.129049
γ : Type ?u.129052
ι : Sort u_2
ι' : Sort ?u.129058
ι₂ : Sort ?u.129061
κ : ι → Sort ?u.129066
κ₁ : ι → Sort ?u.129071
κ₂ : ι → Sort ?u.129076
κ' : ι' → Sort ?u.129081
f : ι → Set α
⊢ (⋂ (i : ι), f i) = ∅ ↔ ∀ (x : α), ∃ i, ¬x ∈ f i
simp [Set.eq_empty_iff_forall_not_mem]