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

State before:
α : Type u_1
f g : Ultrafilter α
h : ∀ (s : Set α), s ∈ f ↔ s ∈ g
⊢ f = g
Tactic:
exact coe_injective (Filter.ext h)
State after:
no goals