nth_rw 1 [← diff_union_of_subset hI.subset]
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : M.Basis I X
⊢ M ／ X = M ／ I ＼ (X \ I)
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : M.Basis I X
⊢ M ／ (X \ I ∪ I) = M ／ I ＼ (X \ I)