simp only [mem_parallelClasses_iff, forall_exists_index, and_imp, encard_eq_one]
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
⊢ M.Simple ↔ ∀ P ∈ M.parallelClasses, P.encard = 1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
⊢ M.Simple ↔ ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}