rw [restrict_eq_self_iff, f.coeFun_eq_id_of_eq_discrete M.parallelClasses_eq_discrete, image_id,
  Loopless.ground_eq]
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
h' : M.Simple
f : M.parallelClasses.RepFun
⊢ M ↾ ⇑f '' {e | M.Nonloop e} = M
no goals