rw [simple_iff_loopless_eq_of_parallel_forall, and_iff_right (by assumption)]
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}
⊢ M.Simple
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 : α), M.Parallel e f → e = f