Theorem: Matroid.point_iff_exists_eq_cl_nonloop (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 : α
⊢ (∃ e, M.Nonloop e ∧ P = M.cl {e}) → M.Point P
Tactic:
rintro ⟨e, he, rfl⟩
State after:
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 : α
he : M.Nonloop e
⊢ M.Point (M.cl {e})

State before:
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 : α
he : M.Nonloop e
⊢ M.Point (M.cl {e})
Tactic:
exact he.cl_point
State after:
no goals