simpa [insert_eq_of_mem heB] using hB.indep
case refine'_1
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hB : M.Base B
heB : e ∈ B
⊢ M.Indep (insert e (B \ {e})) ∧ e ∉ B \ {e}
no goals