rw [removeLoops_eq_restr, restrict_parallel_iff,
  and_iff_left_of_imp (fun h ↦ ⟨h.nonloop_left, h.nonloop_right⟩)]
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
⊢ M.removeLoops.Parallel e f ↔ M.Parallel e f
no goals