rw [hf_im' _ (by simp), preimage_image_eq _ Subtype.val_injective]
α : 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)
X : Set ↑M.E
⊢ f '' ↑X = ↑(⇑e '' X)
no goals