Theorem: Matroid.contract_cl_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 α
M : Matroid α
C : Set α
⊢ M ／ M.cl C = M ／ C ＼ (M.cl C \ C)
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis_inter_ground_basis_cl C
State after:
case intro
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J R B X Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C I : Set α
hI : M.Basis I (C ∩ M.E) ∧ M.Basis I (M.cl C)
⊢ M ／ M.cl C = M ／ C ＼ (M.cl C \ C)

State before:
case intro
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J R B X Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C I : Set α
hI : M.Basis I (C ∩ M.E) ∧ M.Basis I (M.cl C)
⊢ M ／ M.cl C = M ／ C ＼ (M.cl C \ C)
Tactic:
rw [hI.2.contract_eq_contract_delete, ← M.contract_inter_ground_eq C,
  hI.1.contract_eq_contract_delete, delete_delete]
State after:
case intro
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J R B X Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C I : Set α
hI : M.Basis I (C ∩ M.E) ∧ M.Basis I (M.cl C)
⊢ M ／ I ＼ (M.cl C \ I) = M ／ I ＼ ((C ∩ M.E) \ I ∪ M.cl C \ C)

State before:
case intro
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J R B X Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C I : Set α
hI : M.Basis I (C ∩ M.E) ∧ M.Basis I (M.cl C)
⊢ M ／ I ＼ (M.cl C \ I) = M ／ I ＼ ((C ∩ M.E) \ I ∪ M.cl C \ C)
Tactic:
convert rfl using 2
State after:
case h.e'_3.h.e'_5
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J R B X Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C I : Set α
hI : M.Basis I (C ∩ M.E) ∧ M.Basis I (M.cl C)
⊢ (C ∩ M.E) \ I ∪ M.cl C \ C = M.cl C \ I

State before:
case h.e'_3.h.e'_5
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J R B X Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C I : Set α
hI : M.Basis I (C ∩ M.E) ∧ M.Basis I (M.cl C)
⊢ (C ∩ M.E) \ I ∪ M.cl C \ C = M.cl C \ I
Tactic:
rw [union_comm, diff_eq (t := I), union_inter_distrib_left, union_inter_distrib_left,
  diff_union_self, union_eq_self_of_subset_left (diff_subset.trans (M.cl_subset_ground _)),
    union_inter_distrib_right, diff_eq, inter_eq_self_of_subset_left (M.cl_subset_ground _),
    ← cl_inter_ground, union_eq_self_of_subset_right (M.subset_cl (C ∩ M.E)),
    inter_union_distrib_left, ← inter_assoc, inter_self, ← inter_union_distrib_left,
    ← compl_inter, ← diff_eq,
    inter_eq_self_of_subset_right (hI.1.subset.trans inter_subset_left)]
State after:
no goals