no goals
α : Type u_1
β : Type ?u.131860
γ : Type ?u.131863
ι : Sort ?u.131866
ι' : Sort ?u.131869
ι₂ : Sort ?u.131872
κ : ι → Sort ?u.131877
κ₁ : ι → Sort ?u.131882
κ₂ : ι → Sort ?u.131887
κ' : ι' → Sort ?u.131892
c : Set (Set α)
⊢ ⋂₀ c = ∅ ↔ ∀ (a : α), ∃ b, b ∈ c ∧ ¬a ∈ b
simp [Set.eq_empty_iff_forall_not_mem]