rw [← restrict_compl, restrict_cl_eq', sdiff_sdiff_self, bot_eq_empty, union_empty,
  diff_eq, inter_comm M.E, ← inter_assoc X, ← diff_eq, cl_inter_ground,
  ← inter_assoc, ← diff_eq, inter_eq_left]
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X✝ Y Z K D✝ D₁ D₂ R : Set α
M : Matroid α
D X : Set α
⊢ (M ＼ D).cl X = M.cl (X \ D) \ D
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X✝ Y Z K D✝ D₁ D₂ R : Set α
M : Matroid α
D X : Set α
⊢ M.cl (X \ D) \ D ⊆ M.E