rintro h P x hx rfl
case refine_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
⊢ M.Simple → ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}
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}