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

State before:
α : Type u_1
f : Ultrafilter α
g : Filter α
hg : f.as_filter ⊓ g ≠ ⊥
⊢ f.as_filter ≤ g
Tactic:
apply le_of_inf_eq
State after:
case a
α : Type u_1
f : Ultrafilter α
g : Filter α
hg : f.as_filter ⊓ g ≠ ⊥
⊢ f.as_filter ⊓ g = f.as_filter

State before:
case a
α : Type u_1
f : Ultrafilter α
g : Filter α
hg : f.as_filter ⊓ g ≠ ⊥
⊢ f.as_filter ⊓ g = f.as_filter
Tactic:
refine unique ?_ hg
State after:
case a
α : Type u_1
f : Ultrafilter α
g : Filter α
hg : f.as_filter ⊓ g ≠ ⊥
⊢ f.as_filter ⊓ g ≤ f.as_filter

State before:
case a
α : Type u_1
f : Ultrafilter α
g : Filter α
hg : f.as_filter ⊓ g ≠ ⊥
⊢ f.as_filter ⊓ g ≤ f.as_filter
Tactic:
exact inf_le_left
State after:
no goals