no goals
α : Type u_1
β : Type ?u.140766
γ : Type ?u.140769
ι : Sort ?u.140772
ι' : Sort ?u.140775
ι₂ : Sort ?u.140778
κ : ι → Sort ?u.140783
κ₁ : ι → Sort ?u.140788
κ₂ : ι → Sort ?u.140793
κ' : ι' → Sort ?u.140798
c : Set (Set α)
⊢ Set.Nonempty (⋂₀ c) ↔ ∃ a, ∀ (b : Set α), b ∈ c → a ∈ b
simp [nonempty_iff_ne_empty, sInter_eq_empty_iff]