no goals
α : Type u_1
β : Type ?u.20912
γ : Type ?u.20915
ι : Sort u_2
ι' : Sort ?u.20921
l l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
hl : HasBasis l p s
⊢ (∀ {i : ι}, p i → Set.Nonempty (s i)) ↔ ¬∃ i, p i ∧ s i = ∅
simp only [not_exists, not_and, nonempty_iff_ne_empty]