Theorem: Matroid.removeLoops_parallel_iff (Matroid/Parallel.lean)

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