no goals
α : Type u_1
β : Type ?u.15898
γ : Type ?u.15901
ι : Sort ?u.15904
ι' : Sort ?u.15907
l l' : Filter α
p : ι → Prop
s✝ : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
s : Set (Set α)
⊢ FilterBasis.filter (FilterBasis.ofSets s) = generate s
rw [← (FilterBasis.ofSets s).generate, FilterBasis.ofSets_sets, ← generate_eq_generate_inter]