rw [loopless_iff_forall_not_loop]
α : 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}
⊢ M.Loopless
α : 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}
⊢ ∀ e ∈ M.E, ¬M.Loop e