simp only [parallelClasses, Partition.mem_congr_iff, Flat.mem_covByPartition_iff,
  loops_covBy_iff, point_iff_exists_eq_cl_nonloop]
α : Type u_1
M N : Matroid α
e f g : α
I X P✝ D P : Set α
⊢ P ∈ M.parallelClasses ↔ ∃ e, M.Nonloop e ∧ P = M.cl {e} \ M.cl ∅
α : Type u_1
M N : Matroid α
e f g : α
I X P✝ D P : Set α
⊢ (∃ F', (∃ e, M.Nonloop e ∧ F' = M.cl {e}) ∧ F' \ M.cl ∅ = P) ↔ ∃ e, M.Nonloop e ∧ P = M.cl {e} \ M.cl ∅