Theorem: Matroid.parallelExtend_cl_eq_of_mem (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
X : Set α
heX : e ∈ M.cl X
⊢ (M.parallelExtend e f).cl X = insert f (M.cl X)
Tactic:
nth_rw 2 [← M.parallelExtend_delete_eq e hf]
State after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
X : Set α
heX : e ∈ M.cl X
⊢ (M.parallelExtend e f).cl X = insert f ((M.parallelExtend e f ＼ f).cl X)

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
X : Set α
heX : e ∈ M.cl X
⊢ (M.parallelExtend e f).cl X = insert f ((M.parallelExtend e f ＼ f).cl X)
Tactic:
simp only [deleteElem, delete_cl_eq, insert_diff_singleton]
State after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
X : Set α
heX : e ∈ M.cl X
⊢ (M.parallelExtend e f).cl X = insert f ((M.parallelExtend e f).cl (X \ {f}))

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
X : Set α
heX : e ∈ M.cl X
⊢ (M.parallelExtend e f).cl X = insert f ((M.parallelExtend e f).cl (X \ {f}))
Tactic:
rw [← M.parallelExtend_delete_eq e hf, deleteElem, delete_cl_eq, mem_diff,
  (parallelExtend_parallel he f).mem_cl_iff_mem_cl] at heX
State after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
X : Set α
heX : f ∈ (M.parallelExtend e f).cl (X \ {f}) ∧ e ∉ {f}
⊢ (M.parallelExtend e f).cl X = insert f ((M.parallelExtend e f).cl (X \ {f}))

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
X : Set α
heX : f ∈ (M.parallelExtend e f).cl (X \ {f}) ∧ e ∉ {f}
⊢ (M.parallelExtend e f).cl X = insert f ((M.parallelExtend e f).cl (X \ {f}))
Tactic:
rw [cl_diff_singleton_eq_cl heX.1, eq_comm, insert_eq_self]
State after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
X : Set α
heX : f ∈ (M.parallelExtend e f).cl (X \ {f}) ∧ e ∉ {f}
⊢ f ∈ (M.parallelExtend e f).cl X

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
X : Set α
heX : f ∈ (M.parallelExtend e f).cl (X \ {f}) ∧ e ∉ {f}
⊢ f ∈ (M.parallelExtend e f).cl X
Tactic:
exact mem_of_mem_of_subset heX.1 (cl_subset_cl _ diff_subset)
State after:
no goals