rw [delete_eq_delete_iff, contract_ground, diff_eq, diff_eq, ← inter_inter_distrib_right,
  inter_assoc]
α : 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 ／ C ＼ (D \ C)
no goals