rw [← congr_arg Matroid.E h.image_restrict_repFun, restrict_ground_eq]
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
he : M.Nonloop e
⊢ h.repFun e ∈ N.E
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
he : M.Nonloop e
⊢ h.repFun e ∈ ⇑h.repFun '' {e | M.Nonloop e}