refine ⟨I, hI, ?_⟩
case refine_1.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 : α
M : Matroid α
X : Set α
h : ∀ ⦃F : Set α⦄, M.Flat F → ∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (F ∩ I) F
F : Set α
hF : M.Flat F
I : Set α
hI : M.Indep I
hI' : M.Basis (X ∩ I) X ∧ M.Basis (F ∩ I) F
⊢ ∃ I, M.Indep I ∧ X ⊆ M.cl (X ∩ I) ∧ F ⊆ M.cl (F ∩ I)
case refine_1.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 : α
M : Matroid α
X : Set α
h : ∀ ⦃F : Set α⦄, M.Flat F → ∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (F ∩ I) F
F : Set α
hF : M.Flat F
I : Set α
hI : M.Indep I
hI' : M.Basis (X ∩ I) X ∧ M.Basis (F ∩ I) F
⊢ X ⊆ M.cl (X ∩ I) ∧ F ⊆ M.cl (F ∩ I)