apply mem_insert
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e x y : α
heE : e ∈ M.E
I : Set α
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I (X ∩ M.E)
hfE : e ∈ M.E
h : M.Indep (insert e (insert e I))
⊢ e ∈ insert e I
no goals