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
⊢ ∀ X ⊆ M.E, f '' X = ↑(⇑e '' M.E ↓∩ X)
no goals