no goals
α : Type u_1
β : Type ?u.8994
γ : Type ?u.8997
ι : Sort u_2
ι' : Sort ?u.9003
p : ι → Prop
s : ι → Set α
h : IsBasis p s
U : Set α
⊢ U ∈ IsBasis.filter h ↔ ∃ i, p i ∧ s i ⊆ U
simp only [IsBasis.filter, FilterBasis.mem_filter_iff, mem_filterBasis_iff,
  exists_exists_and_eq_and]