Theorem: Matroid.simple_iff_parallelClasses_eq_discrete (Matroid/Simple.lean)

State before:
α : 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}
Tactic:
rw [simple_iff_parallelClasses_eq_discrete', and_iff_right (by assumption)]
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
⊢ M.Loopless
Tactic:
assumption
State after:
no goals