rw [Parallel, parallelClasses, Partition.rel_congr,
  Partition.setOf_rel_eq_partOf, (M.cl_flat ∅).partOf_covByPartition_eq,
  cl_insert_cl_eq_cl_insert, insert_emptyc_eq]
case pos
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
M : Matroid α
e : α
he : M.Nonloop e
⊢ {f | M.Parallel e f} = M.cl {e} \ M.cl ∅
no goals