no goals
α : Type u_1
β : Type ?u.12014
γ : Type ?u.12017
ι : Sort u_2
ι' : Sort ?u.12023
l l' : Filter α
p : ι → Prop
s : ι → Set α
t✝ : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
h : IsBasis p s
t : Set α
⊢ t ∈ IsBasis.filter h ↔ ∃ i, p i ∧ s i ⊆ t
simp only [h.mem_filter_iff, exists_prop]