Theorem: Matroid.Basis.contract_eq_contract_delete (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 α
hI : M.Basis I X
⊢ M ／ X = M ／ I ＼ (X \ I)
Tactic:
nth_rw 1 [← diff_union_of_subset hI.subset]
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : M.Basis I X
⊢ M ／ (X \ I ∪ I) = M ／ I ＼ (X \ I)

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : M.Basis I X
⊢ M ／ (X \ I ∪ I) = M ／ I ＼ (X \ I)
Tactic:
rw [union_comm, ← contract_contract]
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : M.Basis I X
⊢ M ／ I ／ (X \ I) = M ／ I ＼ (X \ I)

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : M.Basis I X
⊢ M ／ I ／ (X \ I) = M ／ I ＼ (X \ I)
Tactic:
refine' contract_eq_delete_of_subset_loops fun e he ↦ _
State after:
α : Type u_1
M M' N : Matroid α
e✝ f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : M.Basis I X
e : α
he : e ∈ X \ I
⊢ e ∈ (M ／ I).cl ∅

State before:
α : Type u_1
M M' N : Matroid α
e✝ f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : M.Basis I X
e : α
he : e ∈ X \ I
⊢ e ∈ (M ／ I).cl ∅
Tactic:
rw [← loop_iff_mem_cl_empty, ← singleton_dep, hI.indep.contract_dep_iff,
  disjoint_singleton_left, and_iff_right he.2, singleton_union,
  ← hI.indep.mem_cl_iff_of_not_mem he.2]
State after:
α : Type u_1
M M' N : Matroid α
e✝ f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : M.Basis I X
e : α
he : e ∈ X \ I
⊢ e ∈ M.cl I

State before:
α : Type u_1
M M' N : Matroid α
e✝ f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : M.Basis I X
e : α
he : e ∈ X \ I
⊢ e ∈ M.cl I
Tactic:
exact hI.subset_cl he.1
State after:
no goals