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

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h_para : M.Parallel' e f
he : e ∈ I
hf : f ∉ I
⊢ M.Indep I ↔ M.Indep (insert f (I \ {e}))
Tactic:
refine ⟨fun hI ↦ hI.parallel'_substitute h_para he, fun hI ↦ ?_⟩
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h_para : M.Parallel' e f
he : e ∈ I
hf : f ∉ I
hI : M.Indep (insert f (I \ {e}))
⊢ M.Indep I

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h_para : M.Parallel' e f
he : e ∈ I
hf : f ∉ I
hI : M.Indep (insert f (I \ {e}))
⊢ M.Indep I
Tactic:
convert hI.parallel'_substitute h_para.symm (mem_insert _ _)
State after:
case h.e'_3
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h_para : M.Parallel' e f
he : e ∈ I
hf : f ∉ I
hI : M.Indep (insert f (I \ {e}))
⊢ I = insert e (insert f (I \ {e}) \ {f})

State before:
case h.e'_3
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h_para : M.Parallel' e f
he : e ∈ I
hf : f ∉ I
hI : M.Indep (insert f (I \ {e}))
⊢ I = insert e (insert f (I \ {e}) \ {f})
Tactic:
have hef : e ≠ f := by rintro rfl; exact hf he
State after:
case h.e'_3
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h_para : M.Parallel' e f
he : e ∈ I
hf : f ∉ I
hI : M.Indep (insert f (I \ {e}))
hef : e ≠ f
⊢ I = insert e (insert f (I \ {e}) \ {f})

State before:
case h.e'_3
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h_para : M.Parallel' e f
he : e ∈ I
hf : f ∉ I
hI : M.Indep (insert f (I \ {e}))
hef : e ≠ f
⊢ I = insert e (insert f (I \ {e}) \ {f})
Tactic:
simp [insert_diff_singleton_comm hef, insert_eq_of_mem he, diff_singleton_eq_self hf]
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h_para : M.Parallel' e f
he : e ∈ I
hf : f ∉ I
hI : M.Indep (insert f (I \ {e}))
⊢ e ≠ f
Tactic:
rintro rfl
State after:
α : Type u_1
M N : Matroid α
e g : α
I X P D : Set α
he : e ∈ I
h_para : M.Parallel' e e
hf : e ∉ I
hI : M.Indep (insert e (I \ {e}))
⊢ False

State before:
α : Type u_1
M N : Matroid α
e g : α
I X P D : Set α
he : e ∈ I
h_para : M.Parallel' e e
hf : e ∉ I
hI : M.Indep (insert e (I \ {e}))
⊢ False
Tactic:
exact hf he
State after:
no goals