assumption
α : 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.Loopless
no goals