obtain ⟨f, hf⟩ := M.exists_nonloop
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
e : α
a✝ : e ∈ M.E
hel : M.Loop e
⊢ False
case intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
e : α
a✝ : e ∈ M.E
hel : M.Loop e
f : α
hf : M.Nonloop f
⊢ False