rw [contract_delete_diff, ← contract_inter_ground_eq, ← delete_inter_ground_eq,
  contract_ground, diff_inter_self_eq_diff, diff_inter_diff_right, inter_diff_right_comm]
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
⊢ M ／ C ＼ D ≤m M
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
⊢ M ／ (C ∩ M.E) ＼ (D \ C ∩ M.E) ≤m M