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

State before:
α : Type u_1
f : Ultrafilter α
g : Filter α
h : g ≤ f.as_filter
hg : g ≠ ⊥
⊢ g = f.as_filter
Tactic:
apply le_antisymm h
State after:
α : Type u_1
f : Ultrafilter α
g : Filter α
h : g ≤ f.as_filter
hg : g ≠ ⊥
⊢ f.as_filter ≤ g

State before:
α : Type u_1
f : Ultrafilter α
g : Filter α
h : g ≤ f.as_filter
hg : g ≠ ⊥
⊢ f.as_filter ≤ g
Tactic:
exact f.le_of_le hg h
State after:
no goals