Theorem: Matroid.Loopless.parallel_class_eq_cl (Matroid/Parallel.lean)

State before:
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
h : M.Loopless
e : α
⊢ {f | M.Parallel e f} = M.cl {e}
Tactic:
rw [setOf_parallel_eq_cl_diff_loops, h.cl_empty, diff_empty]
State after:
no goals