Theorem: Matroid.Indep.parallel'_substitute (Matroid/Parallel.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
h_para : M.Parallel' e f
heI : e ∈ I
⊢ M.Indep (insert f (I \ {e}))
Tactic:
convert (isoOfSwapParallel h_para).image_indep (I := M.E ↓∩ I)
  (by rwa [Subset.image_val_preimage_val_eq hI.subset_ground])
State after:
case h.e'_3
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
h_para : M.Parallel' e f
heI : e ∈ I
⊢ insert f (I \ {e}) = ↑(⇑(isoOfSwapParallel h_para) '' M.E ↓∩ I)

State before:
case h.e'_3
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
h_para : M.Parallel' e f
heI : e ∈ I
⊢ insert f (I \ {e}) = ↑(⇑(isoOfSwapParallel h_para) '' M.E ↓∩ I)
Tactic:
simp only [isoOfSwapParallel_apply_image, Subtype.image_preimage_coe,
  inter_eq_self_of_subset_right hI.subset_ground]
State after:
case h.e'_3
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
h_para : M.Parallel' e f
heI : e ∈ I
⊢ insert f (I \ {e}) = ⇑(Equiv.swap e f) '' I

State before:
case h.e'_3
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
h_para : M.Parallel' e f
heI : e ∈ I
⊢ insert f (I \ {e}) = ⇑(Equiv.swap e f) '' 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 α
hI : M.Indep I
h_para : M.Parallel' e f
heI : e ∈ I
hfI : f ∈ I
⊢ insert f (I \ {e}) = ⇑(Equiv.swap e f) '' I

case neg
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
h_para : M.Parallel' e f
heI : e ∈ I
hfI : f ∉ I
⊢ insert f (I \ {e}) = ⇑(Equiv.swap e f) '' I

State before:
case neg
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
h_para : M.Parallel' e f
heI : e ∈ I
hfI : f ∉ I
⊢ insert f (I \ {e}) = ⇑(Equiv.swap e f) '' I
Tactic:
rw [(Equiv.swap_bijOn_exchange heI hfI).image_eq]
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
h_para : M.Parallel' e f
heI : e ∈ I
⊢ M.Indep ↑(M.E ↓∩ I)
Tactic:
rwa [Subset.image_val_preimage_val_eq hI.subset_ground]
State after:
no goals

State before:
case pos
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
h_para : M.Parallel' e f
heI : e ∈ I
hfI : f ∈ I
⊢ insert f (I \ {e}) = ⇑(Equiv.swap e f) '' I
Tactic:
obtain (rfl : e = f) := h_para.eq_of_indep (hI.subset (pair_subset heI hfI))
State after:
case pos
α : Type u_1
M N : Matroid α
e g : α
I X P D : Set α
hI : M.Indep I
heI : e ∈ I
h_para : M.Parallel' e e
hfI : e ∈ I
⊢ insert e (I \ {e}) = ⇑(Equiv.swap e e) '' I

State before:
case pos
α : Type u_1
M N : Matroid α
e g : α
I X P D : Set α
hI : M.Indep I
heI : e ∈ I
h_para : M.Parallel' e e
hfI : e ∈ I
⊢ insert e (I \ {e}) = ⇑(Equiv.swap e e) '' I
Tactic:
simpa
State after:
no goals