refine ⟨fun h e he ↦ by rw [cl_singleton_eq], fun h ↦ ?_⟩
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.RkPos
⊢ M.Simple ↔ ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
α : 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