Theorem: Matroid.Point.eq_cl_of_mem (Matroid/Flat.lean)

State before:
α : 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}
Tactic:
rw [← indep_singleton] at he
State after:
α : 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}

State before:
α : 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}
Tactic:
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)
State after:
no goals

State before:
α : 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
⊢ M.er P ≤ M.er {e}
Tactic:
rw [hP.er, he.er, encard_singleton]
State after:
no goals