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

State before:
α : Type u_1
f g : Filter α
⊢ (∀ (s : Set α), s ∈ f ↔ s ∈ g) → f = g
Tactic:
exact (ext_iff _ _).mpr
State after:
no goals