Theorem: Matroid.parallelExtend_cl_eq_of_not_mem_not_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
hfX : f ∉ X
⊢ (M.parallelExtend e f).cl X = 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
hfX : f ∉ X
⊢ (M.parallelExtend e f).cl X = (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
hfX : f ∉ X
⊢ (M.parallelExtend e f).cl X = (M.parallelExtend e f ＼ f).cl X
Tactic:
have hfX' : f ∉ (M.parallelExtend e f).cl (X \ {f}) := by
  rw [← M.parallelExtend_delete_eq e hf, deleteElem, delete_cl_eq, mem_diff,
    (parallelExtend_parallel he f).mem_cl_iff_mem_cl] at heX
  simpa [(show e ≠ f by rintro rfl; exact hf he.mem_ground)] using 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 : e ∉ M.cl X
hfX : f ∉ X
hfX' : f ∉ (M.parallelExtend e f).cl (X \ {f})
⊢ (M.parallelExtend e f).cl X = (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
hfX : f ∉ X
hfX' : f ∉ (M.parallelExtend e f).cl (X \ {f})
⊢ (M.parallelExtend e f).cl X = (M.parallelExtend e f ＼ f).cl X
Tactic:
simp only [deleteElem, delete_cl_eq, diff_singleton_eq_self hfX']
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
hfX : f ∉ X
hfX' : f ∉ (M.parallelExtend e f).cl (X \ {f})
⊢ (M.parallelExtend e f).cl X = (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
hfX : f ∉ X
hfX' : f ∉ (M.parallelExtend e f).cl (X \ {f})
⊢ (M.parallelExtend e f).cl X = (M.parallelExtend e f).cl (X \ {f})
Tactic:
rw [diff_singleton_eq_self hfX]
State after:
no goals

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
hfX : f ∉ X
⊢ 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})
hfX : f ∉ X
⊢ 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})
hfX : f ∉ X
⊢ f ∉ (M.parallelExtend e f).cl (X \ {f})
Tactic:
simpa [(show e ≠ f by rintro rfl; exact hf he.mem_ground)] using heX
State after:
no goals

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})
hfX : f ∉ X
⊢ e ≠ f
Tactic:
rintro rfl
State after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e x : α
I C : Set α
he : M.Nonloop e
X : Set α
hf : e ∉ M.E
heX : ¬(e ∈ (M.parallelExtend e e).cl (X \ {e}) ∧ e ∉ {e})
hfX : e ∉ X
⊢ False

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