no goals
α : Type u_1
β : Type ?u.135153
γ : Type ?u.135156
ι : Sort u_2
ι' : Sort ?u.135162
ι₂ : Sort ?u.135165
κ : ι → Sort ?u.135170
κ₁ : ι → Sort ?u.135175
κ₂ : ι → Sort ?u.135180
κ' : ι' → Sort ?u.135185
f : ι → Set α
⊢ Set.Nonempty (⋂ (i : ι), f i) ↔ ∃ x, ∀ (i : ι), x ∈ f i
simp [nonempty_iff_ne_empty, iInter_eq_empty_iff]