obtain ⟨x, hx⟩ := h _ e hef.nonloop_left rfl
case refine_2
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
inst✝ : M.Loopless
h : ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}
e f : α
hef : M.Parallel e f
⊢ e = f
case refine_2.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
inst✝ : M.Loopless
h : ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}
e f : α
hef : M.Parallel e f
x : α
hx : {f | M.Parallel e f} = {x}
⊢ e = f