rw [(indep_of_subset_coloops hX).contract_indep_iff, delete_indep_iff, and_comm,
  union_indep_iff_indep_of_subset_coloops hX]
α : 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
no goals