no goals
α : Type u_1
β : Type ?u.61264
γ : Type ?u.61267
ι : Sort u_2
ι' : Sort ?u.61273
l l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
h : HasBasis l p s
x✝ : Set α
⊢ x✝ ∈ l ↔ ∃ i, p i ∧ x✝ ∈ 𝓟 (s i)
simp only [h.mem_iff, mem_principal, exists_prop]