rw [hIC.contract_eq_contract_delete, delete_indep_iff, hIC.indep.contract_indep_iff,
  diff_union_inter, and_iff_left hI.indep, ← disjoint_union_right, union_diff_self,
  union_eq_self_of_subset_left inter_subset_right]
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Basis' I (X ∪ C)
hIC : M.Basis' (I ∩ C) C
⊢ (M ／ C).Indep (I \ C)
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Basis' I (X ∪ C)
hIC : M.Basis' (I ∩ C) C
⊢ Disjoint (I \ C) C