rw [contract_restrict_eq_restrict_contract _ _ _ disjoint_sdiff_right]
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C R : Set α
hCR : C ⊆ R
⊢ (M ↾ R) ／ C = M ／ C ↾ R \ C
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C R : Set α
hCR : C ⊆ R
⊢ (M ↾ R) ／ C = (M ↾ (R \ C ∪ C)) ／ C