refine hF.basis_inter_ground.basis_subset diff_subset
  (subset_inter (union_subset_union hI.subset hJ.subset)
  (union_subset hI.indep.subset_ground hJ.indep.subset_ground))
α : 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
hFIJ : F ⊆ I ∪ J
hF : M.Basis' ((I ∪ J) \ F) (X ∪ Y)
⊢ M.Basis ((I ∪ J) \ F) (I ∪ J)
no goals