Theorem: FilterGame.Basis.mem_as_filter_of_mem (FilterGame/Solutions/Basis.lean)

State before:
α : Type u_1
b : Basis α
s : Set α
h : s ∈ b
⊢ s ∈ as_filter b
Tactic:
rw [Basis.mem_as_filter_def]
State after:
α : Type u_1
b : Basis α
s : Set α
h : s ∈ b
⊢ ∃ t, t ∈ b ∧ t ⊆ s

State before:
α : Type u_1
b : Basis α
s : Set α
h : s ∈ b
⊢ ∃ t, t ∈ b ∧ t ⊆ s
Tactic:
exact ⟨s, h, subset_rfl⟩
State after:
no goals