simp only [Partition.discrete.rel_iff_eq, mem_setOf_eq,
  show M.parallelClasses.Rel = M.Parallel from rfl]
case refine_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Simple
⊢ ∀ (x y : α), M.parallelClasses.Rel x y ↔ (Partition.discrete {e | M.Nonloop e}).Rel x y
case refine_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Simple
⊢ ∀ (x y : α), M.Parallel x y ↔ x = y ∧ M.Nonloop x