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

State before:
α : Type u_1
f g : Ultrafilter α
⊢ f.as_filter ≤ g.as_filter ↔ f = g
Tactic:
apply Iff.intro
State after:
case mp
α : Type u_1
f g : Ultrafilter α
⊢ f.as_filter ≤ g.as_filter → f = g

case mpr
α : Type u_1
f g : Ultrafilter α
⊢ f = g → f.as_filter ≤ g.as_filter

State before:
case mp
α : Type u_1
f g : Ultrafilter α
⊢ f.as_filter ≤ g.as_filter → f = g

case mpr
α : Type u_1
f g : Ultrafilter α
⊢ f = g → f.as_filter ≤ g.as_filter
Tactic:
. exact eq_of_le
State after:
case mpr
α : Type u_1
f g : Ultrafilter α
⊢ f = g → f.as_filter ≤ g.as_filter

State before:
case mpr
α : Type u_1
f g : Ultrafilter α
⊢ f = g → f.as_filter ≤ g.as_filter
Tactic:
. intros h; rw [h]
State after:
no goals

State before:
case mp
α : Type u_1
f g : Ultrafilter α
⊢ f.as_filter ≤ g.as_filter → f = g
Tactic:
exact eq_of_le
State after:
no goals

State before:
case mpr
α : Type u_1
f g : Ultrafilter α
⊢ f = g → f.as_filter ≤ g.as_filter
Tactic:
intros h
State after:
case mpr
α : Type u_1
f g : Ultrafilter α
h : f = g
⊢ f.as_filter ≤ g.as_filter

State before:
case mpr
α : Type u_1
f g : Ultrafilter α
h : f = g
⊢ f.as_filter ≤ g.as_filter
Tactic:
rw [h]
State after:
no goals