Theorem: Matroid.parallel'_iff_parallel (Matroid/Parallel.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
⊢ M.Parallel' e f ↔ M.Parallel e f
Tactic:
rw [parallel'_iff_loops_or_parallel, or_iff_right (fun h ↦ M.not_loop e h.1)]
State after:
no goals