exact image_subset f hX.subset_nonloops
case intro
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
hX : (M ↾ X).Simple
f : M.parallelClasses.RepFun
hf : EqOn (⇑f) id X
⊢ ⇑f '' X ⊆ (M ↾ ⇑f '' {e | M.Nonloop e}).E
no goals