Theorem: Matroid.eq_parallelExtend_iff (Matroid/Constructions/ParallelExtension.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
⊢ M' = M.parallelExtend e f ↔ M'.Parallel e f ∧ M' ＼ f = M
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
⊢ M' = M.parallelExtend e f → M'.Parallel e f ∧ M' ＼ f = M

case mpr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
⊢ M'.Parallel e f ∧ M' ＼ f = M → M' = M.parallelExtend e f

State before:
case mpr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
⊢ M'.Parallel e f ∧ M' ＼ f = M → M' = M.parallelExtend e f
Tactic:
rintro ⟨h, rfl⟩
State after:
case mpr.intro
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I C : Set α
h : M'.Parallel e f
he : (M' ＼ f).Nonloop e
hf : f ∉ (M' ＼ f).E
⊢ M' = (M' ＼ f).parallelExtend e f

State before:
case mpr.intro
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I C : Set α
h : M'.Parallel e f
he : (M' ＼ f).Nonloop e
hf : f ∉ (M' ＼ f).E
⊢ M' = (M' ＼ f).parallelExtend e f
Tactic:
simp only [deleteElem, delete_nonloop_iff, mem_singleton_iff] at he
State after:
case mpr.intro
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
⊢ M' = (M' ＼ f).parallelExtend e f

State before:
case mpr.intro
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
⊢ M' = (M' ＼ f).parallelExtend e f
Tactic:
refine eq_of_indep_iff_indep_forall (by simp [insert_eq_of_mem h.mem_ground_right])
  (fun I hI ↦ ?_)
State after:
case mpr.intro
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I✝ C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
I : Set α
hI : I ⊆ M'.E
⊢ M'.Indep I ↔ ((M' ＼ f).parallelExtend e f).Indep I

State before:
case mpr.intro
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I✝ C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
I : Set α
hI : I ⊆ M'.E
⊢ M'.Indep I ↔ ((M' ＼ f).parallelExtend e f).Indep I
Tactic:
obtain (hfI | hfI) := em' (f ∈ I)
State after:
case mpr.intro.inl
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I✝ C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
I : Set α
hI : I ⊆ M'.E
hfI : f ∉ I
⊢ M'.Indep I ↔ ((M' ＼ f).parallelExtend e f).Indep I

case mpr.intro.inr
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I✝ C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
I : Set α
hI : I ⊆ M'.E
hfI : f ∈ I
⊢ M'.Indep I ↔ ((M' ＼ f).parallelExtend e f).Indep I

State before:
case mpr.intro.inr
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I✝ C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
I : Set α
hI : I ⊆ M'.E
hfI : f ∈ I
⊢ M'.Indep I ↔ ((M' ＼ f).parallelExtend e f).Indep I
Tactic:
suffices M'.Indep I ↔ M'.Indep (insert e (I \ {f})) ∧ e ∉ I by
  simpa [hfI, parallelExtend, Ne.symm he.2, hI.trans (subset_insert _ _)]
State after:
case mpr.intro.inr
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I✝ C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
I : Set α
hI : I ⊆ M'.E
hfI : f ∈ I
⊢ M'.Indep I ↔ M'.Indep (insert e (I \ {f})) ∧ e ∉ I

State before:
case mpr.intro.inr
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I✝ C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
I : Set α
hI : I ⊆ M'.E
hfI : f ∈ I
⊢ M'.Indep I ↔ M'.Indep (insert e (I \ {f})) ∧ e ∉ I
Tactic:
obtain (heI | heI) := em (e ∈ I)
State after:
case mpr.intro.inr.inl
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I✝ C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
I : Set α
hI : I ⊆ M'.E
hfI : f ∈ I
heI : e ∈ I
⊢ M'.Indep I ↔ M'.Indep (insert e (I \ {f})) ∧ e ∉ I

case mpr.intro.inr.inr
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I✝ C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
I : Set α
hI : I ⊆ M'.E
hfI : f ∈ I
heI : e ∉ I
⊢ M'.Indep I ↔ M'.Indep (insert e (I \ {f})) ∧ e ∉ I

State before:
case mpr.intro.inr.inr
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I✝ C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
I : Set α
hI : I ⊆ M'.E
hfI : f ∈ I
heI : e ∉ I
⊢ M'.Indep I ↔ M'.Indep (insert e (I \ {f})) ∧ e ∉ I
Tactic:
simp [heI, h.parallel'.symm.indep_substitute_iff hfI heI]
State after:
no goals

State before:
case mp
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
⊢ M' = M.parallelExtend e f → M'.Parallel e f ∧ M' ＼ f = M
Tactic:
rintro rfl
State after:
case mp
α : Type u_1
inst✝ : DecidableEq α
M : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
⊢ (M.parallelExtend e f).Parallel e f ∧ M.parallelExtend e f ＼ f = M

State before:
case mp
α : Type u_1
inst✝ : DecidableEq α
M : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
⊢ (M.parallelExtend e f).Parallel e f ∧ M.parallelExtend e f ＼ f = M
Tactic:
exact ⟨parallelExtend_parallel he f, parallelExtend_delete_eq e hf⟩
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
⊢ M'.E = ((M' ＼ f).parallelExtend e f).E
Tactic:
simp [insert_eq_of_mem h.mem_ground_right]
State after:
no goals

State before:
case mpr.intro.inl
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I✝ C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
I : Set α
hI : I ⊆ M'.E
hfI : f ∉ I
⊢ M'.Indep I ↔ ((M' ＼ f).parallelExtend e f).Indep I
Tactic:
simp [hfI, parallelExtend, hI.trans (subset_insert _ _)]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I✝ C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
I : Set α
hI : I ⊆ M'.E
hfI : f ∈ I
this : M'.Indep I ↔ M'.Indep (insert e (I \ {f})) ∧ e ∉ I
⊢ M'.Indep I ↔ ((M' ＼ f).parallelExtend e f).Indep I
Tactic:
simpa [hfI, parallelExtend, Ne.symm he.2, hI.trans (subset_insert _ _)]
State after:
no goals

State before:
case mpr.intro.inr.inl
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I✝ C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
I : Set α
hI : I ⊆ M'.E
hfI : f ∈ I
heI : e ∈ I
⊢ M'.Indep I ↔ M'.Indep (insert e (I \ {f})) ∧ e ∉ I
Tactic:
simp [heI, show ¬ M'.Indep I from
  fun hI ↦ he.2 (h.eq_of_indep (hI.subset (pair_subset heI hfI)))]
State after:
no goals