apply hB.exchange_base_of_indep hf.2 (hI.indep_restrict_of_subset (insert_subset hf.1
(diff_subset.trans hB.subset_ground)))
α : Type u_1
B X : Set α
f e : α
M : Matroid α
hB : (M ↾ X).Base B
hf : f ∈ X \ B
hI : M.Indep (insert f (B \ {e}))
X_sub : X ⊆ M.E
⊢ (M ↾ X).Base (insert f (B \ {e}))
no goals