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

State before:
α : Type u_1
f g : Ultrafilter α
h : f.as_filter ≤ g.as_filter
⊢ f = g
Tactic:
exact coe_injective (g.unique h f.ne_bot)
State after:
no goals