simp_rw [← mem_def, Basis.mem_as_filter_def, mem_as_basis_def]
case h
α : Type u_1
f : Filter α
x : Set α
⊢ x ∈ (Basis.as_filter (as_basis f)).sets ↔ x ∈ f.sets
case h
α : Type u_1
f : Filter α
x : Set α
⊢ (∃ t, t ∈ f ∧ t ⊆ x) ↔ x ∈ f