Theorem: FilterGame.Basis.mem_as_filter_def (FilterGame/Basis.lean)

State before:
α : Type u_1
b : Basis α
s : Set α
⊢ s ∈ as_filter b ↔ ∃ t, t ∈ b ∧ t ⊆ s
Tactic:
exact Iff.rfl
State after:
no goals