simp [image_insert_eq]
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
β : Type u_2
hM : M.Simple
f : α → β
hf : InjOn f M.E
x : α
hx : x ∈ M.E
y : α
hy : y ∈ M.E
⊢ {f x, f y} = f '' {x, y}
no goals