rw [contract_delete_comm _ hCD, ← insert_eq_of_mem heD, ← singleton_union, ← delete_delete]
case refine_1.intro.intro.intro.intro.intro.intro.intro.inr
α : 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 : C ⊆ M.E
hD : D ⊆ M.E
hCD : Disjoint C D
e : α
heD : e ∈ D
h : M ／ C ＼ D <m M
⊢ M ／ C ＼ D ≤m M ＼ e
case refine_1.intro.intro.intro.intro.intro.intro.intro.inr
α : 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 : C ⊆ M.E
hD : D ⊆ M.E
hCD : Disjoint C D
e : α
heD : e ∈ D
h : M ／ C ＼ D <m M
⊢ M ＼ {e} ＼ D ／ C ≤m M ＼ e