rw [← indep_singleton] at he
α : 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 : α
hP : M.Point P
he : M.Nonloop e
heP : e ∈ P
⊢ P = M.cl {e}
α : 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 : α
hP : M.Point P
he : M.Indep {e}
heP : e ∈ P
⊢ P = M.cl {e}