rw [← (hD.coindep_contract_of_disjoint hCD.symm).cl_compl, delete_ground]
case intro.intro.intro.intro.intro
α : Type u_1
M M' : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
C D : Set α
hC : M.Indep C
hD : M.Coindep D
hCD : Disjoint C D
h : M ／ C ＼ D ≤m M
⊢ (M ／ C).cl (M ／ C ＼ D).E = (M ／ C).E
no goals