Theorem: Matroid.contract_eq_delete_of_subset_coloops (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 α
hX : X ⊆ M✶.cl ∅
⊢ M ／ X = M ＼ X
Tactic:
refine' eq_of_indep_iff_indep_forall rfl fun I _ ↦ _
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K C C₁ C₂ : Set α
hX : X ⊆ M✶.cl ∅
I : Set α
x✝ : I ⊆ (M ／ X).E
⊢ (M ／ X).Indep I ↔ (M ＼ X).Indep I

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K C C₁ C₂ : Set α
hX : X ⊆ M✶.cl ∅
I : Set α
x✝ : I ⊆ (M ／ X).E
⊢ (M ／ X).Indep I ↔ (M ＼ X).Indep I
Tactic:
rw [(indep_of_subset_coloops hX).contract_indep_iff, delete_indep_iff, and_comm,
  union_indep_iff_indep_of_subset_coloops hX]
State after:
no goals