rintro ⟨e, he, rfl⟩
α : 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
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})