exact ⟨e, indep_singleton.1 hI.indep, rfl⟩
case intro.intro
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ L H H₁ H₂ H' B C K : Set α
e✝ f e : α
hP : M.Point (M.cl {e})
hI : M.Basis {e} (M.cl {e})
⊢ ∃ e_1, M.Nonloop e_1 ∧ M.cl {e} = M.cl {e_1}
no goals