have X_sub := hB.subset_ground
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
f e : α
X : Set α
hB : M.Basis B X
hf : f ∈ X \ B
hI : M.Indep (insert f (B \ {e}))
⊢ M.Basis (insert f (B \ {e})) X
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
f e : α
X : Set α
hB : M.Basis B X
hf : f ∈ X \ B
hI : M.Indep (insert f (B \ {e}))
X_sub : X ⊆ M.E
⊢ M.Basis (insert f (B \ {e})) X