have hl : M.Loopless := by
  rw [loopless_iff_forall_not_loop]
  intro e _ hel
  obtain ⟨f, hf⟩ := M.exists_nonloop
  obtain (rfl : e = f) := (h f hf).subset (hel.mem_cl _)
  exact hf.not_loop hel
α : 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.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
⊢ M.Simple