exact Nonloop.mem_ground <| f.apply_mem hx
case intro.intro.intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x✝ y : α
f : M.parallelClasses.RepFun
x : α
hx : x ∈ {e | M.Nonloop e}
⊢ f x ∈ M.E
no goals