rintro ⟨e, he, rfl⟩
case mpr
α : Type u_1
M N : Matroid α
e f g : α
I X P✝ D P : Set α
⊢ (∃ e, M.Nonloop e ∧ P = M.cl {e} \ M.cl ∅) → ∃ F', (∃ e, M.Nonloop e ∧ F' = M.cl {e}) ∧ F' \ M.cl ∅ = P
case mpr.intro.intro
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
e : α
he : M.Nonloop e
⊢ ∃ F', (∃ e, M.Nonloop e ∧ F' = M.cl {e}) ∧ F' \ M.cl ∅ = M.cl {e} \ M.cl ∅