rw [← base_restrict_iff] at hB ⊢
α : Type u_1
B X : Set α
f e : α
M : Matroid α
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
α : 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}))