Theorem: FilterGame.Filter.eq_def (FilterGame/Solutions/Filter.lean)

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

case mpr
α : Type u_1
f g : Filter α
⊢ f.sets = g.sets → f = g

State before:
case mp
α : Type u_1
f g : Filter α
⊢ f = g → f.sets = g.sets

case mpr
α : Type u_1
f g : Filter α
⊢ f.sets = g.sets → f = g
Tactic:
. intro h; rw [h]
State after:
case mpr
α : Type u_1
f g : Filter α
⊢ f.sets = g.sets → f = g

State before:
case mpr
α : Type u_1
f g : Filter α
⊢ f.sets = g.sets → f = g
Tactic:
. intro h; cases f; cases g; congr
State after:
no goals

State before:
case mp
α : Type u_1
f g : Filter α
⊢ f = g → f.sets = g.sets
Tactic:
intro h
State after:
case mp
α : Type u_1
f g : Filter α
h : f = g
⊢ f.sets = g.sets

State before:
case mp
α : Type u_1
f g : Filter α
h : f = g
⊢ f.sets = g.sets
Tactic:
rw [h]
State after:
no goals

State before:
case mpr
α : Type u_1
f g : Filter α
⊢ f.sets = g.sets → f = g
Tactic:
intro h
State after:
case mpr
α : Type u_1
f g : Filter α
h : f.sets = g.sets
⊢ f = g

State before:
case mpr
α : Type u_1
f g : Filter α
h : f.sets = g.sets
⊢ f = g
Tactic:
cases f
State after:
case mpr.mk
α : Type u_1
g : Filter α
sets✝ : Set (Set α)
univ_mem_sets✝ : Set.univ ∈ sets✝
superset_mem_sets✝ : ∀ {s t : Set α}, s ∈ sets✝ → s ⊆ t → t ∈ sets✝
inter_mem_sets✝ : ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → s ∩ t ∈ sets✝
h :
  { sets := sets✝, univ_mem_sets := univ_mem_sets✝, superset_mem_sets := superset_mem_sets✝,
        inter_mem_sets := inter_mem_sets✝ }.sets =
    g.sets
⊢ { sets := sets✝, univ_mem_sets := univ_mem_sets✝, superset_mem_sets := superset_mem_sets✝,
      inter_mem_sets := inter_mem_sets✝ } =
    g

State before:
case mpr.mk
α : Type u_1
g : Filter α
sets✝ : Set (Set α)
univ_mem_sets✝ : Set.univ ∈ sets✝
superset_mem_sets✝ : ∀ {s t : Set α}, s ∈ sets✝ → s ⊆ t → t ∈ sets✝
inter_mem_sets✝ : ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → s ∩ t ∈ sets✝
h :
  { sets := sets✝, univ_mem_sets := univ_mem_sets✝, superset_mem_sets := superset_mem_sets✝,
        inter_mem_sets := inter_mem_sets✝ }.sets =
    g.sets
⊢ { sets := sets✝, univ_mem_sets := univ_mem_sets✝, superset_mem_sets := superset_mem_sets✝,
      inter_mem_sets := inter_mem_sets✝ } =
    g
Tactic:
cases g
State after:
case mpr.mk.mk
α : Type u_1
sets✝¹ : Set (Set α)
univ_mem_sets✝¹ : Set.univ ∈ sets✝¹
superset_mem_sets✝¹ : ∀ {s t : Set α}, s ∈ sets✝¹ → s ⊆ t → t ∈ sets✝¹
inter_mem_sets✝¹ : ∀ {s t : Set α}, s ∈ sets✝¹ → t ∈ sets✝¹ → s ∩ t ∈ sets✝¹
sets✝ : Set (Set α)
univ_mem_sets✝ : Set.univ ∈ sets✝
superset_mem_sets✝ : ∀ {s t : Set α}, s ∈ sets✝ → s ⊆ t → t ∈ sets✝
inter_mem_sets✝ : ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → s ∩ t ∈ sets✝
h :
  { sets := sets✝¹, univ_mem_sets := univ_mem_sets✝¹, superset_mem_sets := superset_mem_sets✝¹,
        inter_mem_sets := inter_mem_sets✝¹ }.sets =
    { sets := sets✝, univ_mem_sets := univ_mem_sets✝, superset_mem_sets := superset_mem_sets✝,
        inter_mem_sets := inter_mem_sets✝ }.sets
⊢ { sets := sets✝¹, univ_mem_sets := univ_mem_sets✝¹, superset_mem_sets := superset_mem_sets✝¹,
      inter_mem_sets := inter_mem_sets✝¹ } =
    { sets := sets✝, univ_mem_sets := univ_mem_sets✝, superset_mem_sets := superset_mem_sets✝,
      inter_mem_sets := inter_mem_sets✝ }

State before:
case mpr.mk.mk
α : Type u_1
sets✝¹ : Set (Set α)
univ_mem_sets✝¹ : Set.univ ∈ sets✝¹
superset_mem_sets✝¹ : ∀ {s t : Set α}, s ∈ sets✝¹ → s ⊆ t → t ∈ sets✝¹
inter_mem_sets✝¹ : ∀ {s t : Set α}, s ∈ sets✝¹ → t ∈ sets✝¹ → s ∩ t ∈ sets✝¹
sets✝ : Set (Set α)
univ_mem_sets✝ : Set.univ ∈ sets✝
superset_mem_sets✝ : ∀ {s t : Set α}, s ∈ sets✝ → s ⊆ t → t ∈ sets✝
inter_mem_sets✝ : ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → s ∩ t ∈ sets✝
h :
  { sets := sets✝¹, univ_mem_sets := univ_mem_sets✝¹, superset_mem_sets := superset_mem_sets✝¹,
        inter_mem_sets := inter_mem_sets✝¹ }.sets =
    { sets := sets✝, univ_mem_sets := univ_mem_sets✝, superset_mem_sets := superset_mem_sets✝,
        inter_mem_sets := inter_mem_sets✝ }.sets
⊢ { sets := sets✝¹, univ_mem_sets := univ_mem_sets✝¹, superset_mem_sets := superset_mem_sets✝¹,
      inter_mem_sets := inter_mem_sets✝¹ } =
    { sets := sets✝, univ_mem_sets := univ_mem_sets✝, superset_mem_sets := superset_mem_sets✝,
      inter_mem_sets := inter_mem_sets✝ }
Tactic:
congr
State after:
no goals