refine ⟨Partition.RepFun.mk f (fun a ha ↦ f.apply_of_not_mem (by simpa))
  (fun a ha ↦ by simpa [mem_setOf_eq, parallelClasses_rel_eq] using f.rel_apply (by simpa))
  (fun a b hab ↦ f.apply_eq_apply (by simpa)), ?_⟩
α : Type u_1
M✝ N : Matroid α
e f✝ g : α
I X P D : Set α
M : Matroid α
f : M.removeLoops.parallelClasses.RepFun := ⋯.some
⊢ M.simplification.IsSimplification M
α : Type u_1
M✝ N : Matroid α
e f✝ g : α
I X P D : Set α
M : Matroid α
f : M.removeLoops.parallelClasses.RepFun := ⋯.some
⊢ M.simplification =
    M ↾
      ⇑{ toFun := ⇑f, apply_eq_self_of_not_mem := ⋯, rel_apply_of_mem := ⋯, apply_eq_of_rel := ⋯ } '' {e | M.Nonloop e}