rwa [← hB.eq_of_subset_indep hI hBI]
case intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B✝ C R : Set α
e f x y : α
S T : Set α
hI : M.Indep I
hIs : M.Spanning I
B : Set α
hB : M.Base B
hBI : B ⊆ I
⊢ M.Base I
no goals