simp only [ModularPair, ModularFamily, mem_singleton_iff, modularBase_pair_iff, indep_iff]
ι : 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 : α
M : Matroid α
X Y : Set α
⊢ M.ModularPair X Y ↔ ∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y
ι : 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 : α
M : Matroid α
X Y : Set α
⊢ (∃ B, M.ModularBase B fun i => bif i then X else Y) ↔
    ∃ I, (∃ B, M.Base B ∧ I ⊆ B) ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y