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

State before:
α : Type u_1
f g : Filter α
s : Set α
⊢ s ∈ f ⊓ g ↔ ∃ a, a ∈ f ∧ ∃ b, b ∈ g ∧ s = a ∩ b
Tactic:
exact Iff.rfl
State after:
no goals