rw [setOf_parallel_eq_cl_diff_loops, diff_union_self,
  union_eq_self_of_subset_right (M.cl_mono (empty_subset _))]
α : 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 ∅
no goals