rw [simple_iff_loopless_eq_of_parallel_forall]
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
f : M.parallelClasses.RepFun
⊢ (M ↾ ⇑f '' {e | M.Nonloop e}).Simple
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
f : M.parallelClasses.RepFun
⊢ (M ↾ ⇑f '' {e | M.Nonloop e}).Loopless ∧ ∀ (e f_1 : α), (M ↾ ⇑f '' {e | M.Nonloop e}).Parallel e f_1 → e = f_1