rw [simple_iff_loopless_eq_of_parallel_forall, and_iff_right hl]
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
hl : M.Loopless
⊢ M.Simple
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
hl : M.Loopless
⊢ ∀ (e f : α), M.Parallel e f → e = f