exact ⟨x, by simp [Set.ext_iff, parallel_iff_eq hx.mem_ground]⟩
case refine_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
h : M.Simple
x : α
hx : M.Nonloop x
⊢ ∃ x_1, {f | M.Parallel x f} = {x_1}
no goals