rw [simple_iff_parallelClasses_eq_discrete', and_iff_right (by assumption)]
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
⊢ M.Simple ↔ M.parallelClasses = Partition.discrete {e | M.Nonloop e}
no goals