have hf_im' : ∀ X ⊆ M.E, f '' X = e '' (M.E ↓∩ X) := by
  simp [← Subtype.forall_set_subtype, preimage_image_eq _ Subtype.val_injective,
    image_image, show ∀ x : M.E, f x = e x from fun x ↦ by simp [f, x.2]]
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : Nonempty (α → β)
f : α → β := fun x => if hx : x ∈ M.E then ↑(e ⟨x, hx⟩) else Classical.arbitrary (α → β) x
⊢ ∃ f, ∃ (hf : InjOn f M.E), N = M.map f hf
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : Nonempty (α → β)
f : α → β := fun x => if hx : x ∈ M.E then ↑(e ⟨x, hx⟩) else Classical.arbitrary (α → β) x
hf_im' : ∀ X ⊆ M.E, f '' X = ↑(⇑e '' M.E ↓∩ X)
⊢ ∃ f, ∃ (hf : InjOn f M.E), N = M.map f hf