rwa [union_diff_distrib, (sdiff_eq_left (x := J)).2 ]
α : Type u_1
M : Matroid α
B B' I I' J K X Y F : Set α
hXY : Disjoint X Y
hI : M.Basis' I X
hJ : M.Basis' J Y
hFI : F ⊆ I
hF : M.Basis' (I \ F ∪ J) (X ∪ Y)
⊢ M.Basis' ((I ∪ J) \ F) (X ∪ Y)
α : Type u_1
M : Matroid α
B B' I I' J K X Y F : Set α
hXY : Disjoint X Y
hI : M.Basis' I X
hJ : M.Basis' J Y
hFI : F ⊆ I
hF : M.Basis' (I \ F ∪ J) (X ∪ Y)
⊢ Disjoint J F