refine ⟨fun ⟨B, hB, hB'⟩ ↦ ⟨B, indep_iff.1 hB.indep, ?_⟩,
  fun ⟨I, ⟨B, hB, hIB⟩, hIX, hIY⟩ ↦ ⟨B, hB, ?_⟩ ⟩
ι : 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
case refine_1
ι : 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 α
x✝ : ∃ B, M.ModularBase B fun i => bif i then X else Y
B : Set α
hB : M.Base B
hB' : ∀ (i : Bool), M.Basis ((fun i => bif i then X else Y) i ∩ B) ((fun i => bif i then X else Y) i)
⊢ M.Basis (X ∩ B) X ∧ M.Basis (Y ∩ B) Y

case refine_2
ι : 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 α
x✝ : ∃ I, (∃ B, M.Base B ∧ I ⊆ B) ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y
I B : Set α
hB : M.Base B
hIB : I ⊆ B
hIX : M.Basis (X ∩ I) X
hIY : M.Basis (Y ∩ I) Y
⊢ ∀ (i : Bool), M.Basis ((fun i => bif i then X else Y) i ∩ B) ((fun i => bif i then X else Y) i)