refine indep_singleton.2 (toNonloop (by aesop_mat))
case inl.inr.intro
α : Type u_1
M N : Matroid α
e f g : α
X P D : Set α
inst✝ : M.Simple
x : α
hI : autoParam ({x} ⊆ M.E) _auto✝
hne : {x}.encard ≠ ⊤
⊢ M.Indep {x}
no goals