Theorem: Matroid.Parallel'.eq_mapEquiv_swap (Matroid/Parallel.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
⊢ M.mapEquiv (Equiv.swap e f) = M
Tactic:
have hrw := Equiv.swap_image_eq_self
    (show e ∈ M.E ↔ f ∈ M.E by simp [h.mem_ground_left, h.mem_ground_right])
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
⊢ M.mapEquiv (Equiv.swap e f) = M

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
⊢ M.mapEquiv (Equiv.swap e f) = M
Tactic:
simp only [eq_iff_indep_iff_indep_forall, mapEquiv_ground_eq, hrw, mapEquiv_indep_iff,
  Equiv.symm_swap, true_and]
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
⊢ ∀ I ⊆ M.E, M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
⊢ ∀ I ⊆ M.E, M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I
Tactic:
rintro I -
State after:
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
⊢ M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I

State before:
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
⊢ M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I
Tactic:
by_cases heI : e ∈ I
State after:
case pos
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
heI : e ∈ I
⊢ M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I

case neg
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
heI : e ∉ I
⊢ M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I

State before:
case neg
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
heI : e ∉ I
⊢ M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I
Tactic:
by_cases hfI : f ∈ I
State after:
case pos
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
heI : e ∉ I
hfI : f ∈ I
⊢ M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I

case neg
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
heI : e ∉ I
hfI : f ∉ I
⊢ M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I

State before:
case neg
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
heI : e ∉ I
hfI : f ∉ I
⊢ M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I
Tactic:
rw [Equiv.swap_image_eq_self (by simp [hfI, heI])]
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
⊢ e ∈ M.E ↔ f ∈ M.E
Tactic:
simp [h.mem_ground_left, h.mem_ground_right]
State after:
no goals

State before:
case pos
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
heI : e ∈ I
⊢ M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I
Tactic:
by_cases hfI : f ∈ I
State after:
case pos
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
heI : e ∈ I
hfI : f ∈ I
⊢ M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I

case neg
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
heI : e ∈ I
hfI : f ∉ I
⊢ M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I

State before:
case neg
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
heI : e ∈ I
hfI : f ∉ I
⊢ M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I
Tactic:
rw [Equiv.swap_image_eq_exchange heI hfI, ← h.indep_substitute_iff heI hfI]
State after:
no goals

State before:
case pos
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
heI : e ∈ I
hfI : f ∈ I
⊢ M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I
Tactic:
rw [Equiv.swap_image_eq_self (by simp [heI, hfI])]
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
heI : e ∈ I
hfI : f ∈ I
⊢ e ∈ I ↔ f ∈ I
Tactic:
simp [heI, hfI]
State after:
no goals

State before:
case pos
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
heI : e ∉ I
hfI : f ∈ I
⊢ M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I
Tactic:
rw [Equiv.swap_comm, Equiv.swap_image_eq_exchange hfI heI,
  ← h.symm.indep_substitute_iff hfI heI]
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
heI : e ∉ I
hfI : f ∉ I
⊢ e ∈ I ↔ f ∈ I
Tactic:
simp [hfI, heI]
State after:
no goals