refine ⟨I, J, ?_, ?_, hI, hJ⟩
case intro.refine_2.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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
h : M ／ X ↾ Y = M ↾ Y
J : Set α
hJ : M.Basis J Y
hi : (M ↾ Y).Indep J
⊢ ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y
case intro.refine_2.intro.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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
h : M ／ X ↾ Y = M ↾ Y
J : Set α
hJ : M.Basis J Y
hi : (M ↾ Y).Indep J
⊢ M.Indep (I ∪ J)

case intro.refine_2.intro.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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
h : M ／ X ↾ Y = M ↾ Y
J : Set α
hJ : M.Basis J Y
hi : (M ↾ Y).Indep J
⊢ Disjoint I J