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

State before:
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
M : Matroid α
e : α
⊢ M.cl {e} = {f | M.Parallel e f} ∪ M.cl ∅
Tactic:
rw [setOf_parallel_eq_cl_diff_loops, diff_union_self,
  union_eq_self_of_subset_right (M.cl_mono (empty_subset _))]
State after:
no goals