Theorem: FilterGame.Basis.eq_def (FilterGame/Basis.lean)

State before:
α : Type u_1
b c : Basis α
⊢ b = c ↔ b.sets = c.sets
Tactic:
apply Iff.intro
State after:
case mp
α : Type u_1
b c : Basis α
⊢ b = c → b.sets = c.sets

case mpr
α : Type u_1
b c : Basis α
⊢ b.sets = c.sets → b = c

State before:
case mp
α : Type u_1
b c : Basis α
⊢ b = c → b.sets = c.sets

case mpr
α : Type u_1
b c : Basis α
⊢ b.sets = c.sets → b = c
Tactic:
. intro h; rw [h]
State after:
case mpr
α : Type u_1
b c : Basis α
⊢ b.sets = c.sets → b = c

State before:
case mpr
α : Type u_1
b c : Basis α
⊢ b.sets = c.sets → b = c
Tactic:
. intro h; cases b; cases c; congr
State after:
no goals

State before:
case mp
α : Type u_1
b c : Basis α
⊢ b = c → b.sets = c.sets
Tactic:
intro h
State after:
case mp
α : Type u_1
b c : Basis α
h : b = c
⊢ b.sets = c.sets

State before:
case mp
α : Type u_1
b c : Basis α
h : b = c
⊢ b.sets = c.sets
Tactic:
rw [h]
State after:
no goals

State before:
case mpr
α : Type u_1
b c : Basis α
⊢ b.sets = c.sets → b = c
Tactic:
intro h
State after:
case mpr
α : Type u_1
b c : Basis α
h : b.sets = c.sets
⊢ b = c

State before:
case mpr
α : Type u_1
b c : Basis α
h : b.sets = c.sets
⊢ b = c
Tactic:
cases b
State after:
case mpr.mk
α : Type u_1
c : Basis α
sets✝ : Set (Set α)
sets_nonempty✝ : ∃ s, s ∈ sets✝
inter_mem_sets✝ : ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → ∃ u, u ∈ sets✝ ∧ u ⊆ s ∩ t
h : { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ }.sets = c.sets
⊢ { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ } = c

State before:
case mpr.mk
α : Type u_1
c : Basis α
sets✝ : Set (Set α)
sets_nonempty✝ : ∃ s, s ∈ sets✝
inter_mem_sets✝ : ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → ∃ u, u ∈ sets✝ ∧ u ⊆ s ∩ t
h : { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ }.sets = c.sets
⊢ { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ } = c
Tactic:
cases c
State after:
case mpr.mk.mk
α : Type u_1
sets✝¹ : Set (Set α)
sets_nonempty✝¹ : ∃ s, s ∈ sets✝¹
inter_mem_sets✝¹ : ∀ {s t : Set α}, s ∈ sets✝¹ → t ∈ sets✝¹ → ∃ u, u ∈ sets✝¹ ∧ u ⊆ s ∩ t
sets✝ : Set (Set α)
sets_nonempty✝ : ∃ s, s ∈ sets✝
inter_mem_sets✝ : ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → ∃ u, u ∈ sets✝ ∧ u ⊆ s ∩ t
h :
  { sets := sets✝¹, sets_nonempty := sets_nonempty✝¹, inter_mem_sets := inter_mem_sets✝¹ }.sets =
    { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ }.sets
⊢ { sets := sets✝¹, sets_nonempty := sets_nonempty✝¹, inter_mem_sets := inter_mem_sets✝¹ } =
    { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ }

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