rw [hI.2.contract_eq_contract_delete, ← M.contract_inter_ground_eq C,
  hI.1.contract_eq_contract_delete, delete_delete]
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)
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)