simp_rw [mem_parallelClasses_iff_eq_cl_diff_loops, setOf_parallel_eq_cl_diff_loops]
α : Type u_1
M N : Matroid α
e f g : α
I X P✝ D P : Set α
⊢ P ∈ M.parallelClasses ↔ ∃ e, M.Nonloop e ∧ P = {f | M.Parallel e f}
no goals