exact hP.flat.eq_cl_of_basis <| he.basis_of_subset_of_er_le_of_finite (singleton_subset_iff.2 heP)
  (by rw [hP.er, he.er, encard_singleton]) (finite_singleton 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}
no goals