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

State before:
α : Type u_1
f g : Ultrafilter α
⊢ f.as_filter = g.as_filter ↔ f = g
Tactic:
exact coe_injective.eq_iff
State after:
no goals