Theorem: Matroid.contract_cl_eq (Matroid/Minor/Basic.lean)

State before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
⊢ (M ／ C).cl X = M.cl (X ∪ C) \ C
Tactic:
ext e
State after:
case h
α : Type u_1
M✝ M' N : Matroid α
e✝ f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
e : α
⊢ e ∈ (M ／ C).cl X ↔ e ∈ M.cl (X ∪ C) \ C

State before:
case h
α : Type u_1
M✝ M' N : Matroid α
e✝ f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
e : α
⊢ e ∈ (M ／ C).cl X ↔ e ∈ M.cl (X ∪ C) \ C
Tactic:
by_cases heX : e ∈ X
State after:
case pos
α : Type u_1
M✝ M' N : Matroid α
e✝ f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
e : α
heX : e ∈ X
⊢ e ∈ (M ／ C).cl X ↔ e ∈ M.cl (X ∪ C) \ C

case neg
α : Type u_1
M✝ M' N : Matroid α
e✝ f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
e : α
heX : e ∉ X
⊢ e ∈ (M ／ C).cl X ↔ e ∈ M.cl (X ∪ C) \ C

State before:
case neg
α : Type u_1
M✝ M' N : Matroid α
e✝ f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
e : α
heX : e ∉ X
⊢ e ∈ (M ／ C).cl X ↔ e ∈ M.cl (X ∪ C) \ C
Tactic:
suffices h' : e ∈ (M ／ C).cl X \ X ↔ e ∈ M.cl (X ∪ C) \ (X ∪ C) by
  rwa [mem_diff, and_iff_left heX, mem_diff, mem_union, or_iff_right heX, ← mem_diff] at h'
State after:
case neg
α : Type u_1
M✝ M' N : Matroid α
e✝ f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
e : α
heX : e ∉ X
⊢ e ∈ (M ／ C).cl X \ X ↔ e ∈ M.cl (X ∪ C) \ (X ∪ C)

State before:
case neg
α : Type u_1
M✝ M' N : Matroid α
e✝ f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
e : α
heX : e ∉ X
⊢ e ∈ (M ／ C).cl X \ X ↔ e ∈ M.cl (X ∪ C) \ (X ∪ C)
Tactic:
rw [← contract_loop_iff_mem_cl, ← contract_loop_iff_mem_cl, contract_contract, union_comm]
State after:
no goals

State before:
case pos
α : Type u_1
M✝ M' N : Matroid α
e✝ f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
e : α
heX : e ∈ X
⊢ e ∈ (M ／ C).cl X ↔ e ∈ M.cl (X ∪ C) \ C
Tactic:
by_cases he : e ∈ (M ／ C).E
State after:
case pos
α : Type u_1
M✝ M' N : Matroid α
e✝ f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
e : α
heX : e ∈ X
he : e ∈ (M ／ C).E
⊢ e ∈ (M ／ C).cl X ↔ e ∈ M.cl (X ∪ C) \ C

case neg
α : Type u_1
M✝ M' N : Matroid α
e✝ f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
e : α
heX : e ∈ X
he : e ∉ (M ／ C).E
⊢ e ∈ (M ／ C).cl X ↔ e ∈ M.cl (X ∪ C) \ C

State before:
case neg
α : Type u_1
M✝ M' N : Matroid α
e✝ f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
e : α
heX : e ∈ X
he : e ∉ (M ／ C).E
⊢ e ∈ (M ／ C).cl X ↔ e ∈ M.cl (X ∪ C) \ C
Tactic:
refine' iff_of_false (he ∘ fun h ↦ cl_subset_ground _ _ h) (he ∘ fun h ↦ _)
State after:
case neg
α : Type u_1
M✝ M' N : Matroid α
e✝ f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
e : α
heX : e ∈ X
he : e ∉ (M ／ C).E
h : e ∈ M.cl (X ∪ C) \ C
⊢ e ∈ (M ／ C).E

State before:
case neg
α : Type u_1
M✝ M' N : Matroid α
e✝ f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
e : α
heX : e ∈ X
he : e ∉ (M ／ C).E
h : e ∈ M.cl (X ∪ C) \ C
⊢ e ∈ (M ／ C).E
Tactic:
rw [contract_ground]
State after:
case neg
α : Type u_1
M✝ M' N : Matroid α
e✝ f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
e : α
heX : e ∈ X
he : e ∉ (M ／ C).E
h : e ∈ M.cl (X ∪ C) \ C
⊢ e ∈ M.E \ C

State before:
case neg
α : Type u_1
M✝ M' N : Matroid α
e✝ f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
e : α
heX : e ∈ X
he : e ∉ (M ／ C).E
h : e ∈ M.cl (X ∪ C) \ C
⊢ e ∈ M.E \ C
Tactic:
exact ⟨M.cl_subset_ground _ h.1, h.2⟩
State after:
no goals

State before:
case pos
α : Type u_1
M✝ M' N : Matroid α
e✝ f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
e : α
heX : e ∈ X
he : e ∈ (M ／ C).E
⊢ e ∈ (M ／ C).cl X ↔ e ∈ M.cl (X ∪ C) \ C
Tactic:
refine' iff_of_true (mem_cl_of_mem' _ heX) _
State after:
case pos
α : Type u_1
M✝ M' N : Matroid α
e✝ f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
e : α
heX : e ∈ X
he : e ∈ (M ／ C).E
⊢ e ∈ M.cl (X ∪ C) \ C

State before:
case pos
α : Type u_1
M✝ M' N : Matroid α
e✝ f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
e : α
heX : e ∈ X
he : e ∈ (M ／ C).E
⊢ e ∈ M.cl (X ∪ C) \ C
Tactic:
rw [contract_ground] at he
State after:
case pos
α : Type u_1
M✝ M' N : Matroid α
e✝ f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
e : α
heX : e ∈ X
he : e ∈ M.E \ C
⊢ e ∈ M.cl (X ∪ C) \ C

State before:
case pos
α : Type u_1
M✝ M' N : Matroid α
e✝ f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
e : α
heX : e ∈ X
he : e ∈ M.E \ C
⊢ e ∈ M.cl (X ∪ C) \ C
Tactic:
exact ⟨mem_cl_of_mem' _ (Or.inl heX) he.1, he.2⟩
State after:
no goals

State before:
α : Type u_1
M✝ M' N : Matroid α
e✝ f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
e : α
heX : e ∉ X
h' : e ∈ (M ／ C).cl X \ X ↔ e ∈ M.cl (X ∪ C) \ (X ∪ C)
⊢ e ∈ (M ／ C).cl X ↔ e ∈ M.cl (X ∪ C) \ C
Tactic:
rwa [mem_diff, and_iff_left heX, mem_diff, mem_union, or_iff_right heX, ← mem_diff] at h'
State after:
no goals