Theorem: FilterGame.Filter.ext_iff (FilterGame/Solutions/Filter.lean)

State before:
α : Type u_1
f g : Filter α
⊢ f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g
Tactic:
simp only [eq_def, mem_def, Set.ext_iff]
State after:
no goals