rw [contract_eq_contract_iff, delete_ground, diff_inter_diff_right, diff_eq, diff_eq, 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 α
D C : Set α
⊢ M ＼ D ／ C = M ＼ D ／ (C \ D)
no goals