obtain ⟨I,J, hI, hJ, hIJ⟩ := M.exists_basis_subset_basis hXY
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXY : X ⊆ Y
hY : Y ⊆ M.E
⊢ M.ModularPair X Y
case intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J✝ X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I J : Set α
hI : M.Basis I X
hJ : M.Basis J Y
hIJ : I ⊆ J
⊢ M.ModularPair X Y