rw [hI.contract_eq_contract_delete, delete_indep_iff, hI.indep.contract_indep_iff,
  and_comm, ← and_assoc, ← disjoint_union_right, diff_union_self,
  union_eq_self_of_subset_right hI.subset, and_comm, disjoint_comm]
α : 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).Indep J ↔ M.Indep (J ∪ I) ∧ Disjoint X J
no goals