refine ⟨fun h ↦ ⟨by infer_instance, Partition.eq_of_rel_iff_rel ?_⟩, fun ⟨_,h⟩ ↦ ?_⟩
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
⊢ M.Simple ↔ M.Loopless ∧ M.parallelClasses = Partition.discrete {e | M.Nonloop e}
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_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x✝ : M.Loopless ∧ M.parallelClasses = Partition.discrete {e | M.Nonloop e}
left✝ : M.Loopless
h : M.parallelClasses = Partition.discrete {e | M.Nonloop e}
⊢ M.Simple