Theorem: FilterGame.Filter.inter_mem_inf (FilterGame/Solutions/Semilattice.lean)

State before:
α : Type u_1
f g : Filter α
s t : Set α
hs : s ∈ f
ht : t ∈ g
⊢ s ∩ t ∈ f ⊓ g
Tactic:
exact ⟨s, hs, t, ht, rfl⟩
State after:
no goals