Theorem: Matroid.Point.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 : α
hP : M.Point P
⊢ ∃ e, M.Nonloop e ∧ P = M.cl {e}
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis P
State after:
case intro
α : 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
I : Set α
hI : M.Basis I P
⊢ ∃ e, M.Nonloop e ∧ P = M.cl {e}

State before:
case intro
α : 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
I : Set α
hI : M.Basis I P
⊢ ∃ e, M.Nonloop e ∧ P = M.cl {e}
Tactic:
obtain ⟨e, rfl⟩ := encard_eq_one.1 <| hI.encard.trans hP.er
State after:
case intro.intro
α : 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
e : α
hI : M.Basis {e} P
⊢ ∃ e, M.Nonloop e ∧ P = M.cl {e}

State before:
case intro.intro
α : 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
e : α
hI : M.Basis {e} P
⊢ ∃ e, M.Nonloop e ∧ P = M.cl {e}
Tactic:
obtain rfl := hP.flat.eq_cl_of_basis hI
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 : α
hP : M.Point (M.cl {e})
hI : M.Basis {e} (M.cl {e})
⊢ ∃ e_1, M.Nonloop e_1 ∧ M.cl {e} = M.cl {e_1}

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 : α
hP : M.Point (M.cl {e})
hI : M.Basis {e} (M.cl {e})
⊢ ∃ e_1, M.Nonloop e_1 ∧ M.cl {e} = M.cl {e_1}
Tactic:
exact ⟨e, indep_singleton.1 hI.indep, rfl⟩
State after:
no goals