simp [f, hx, hy, Subtype.val_inj]
α : 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)
hf_im : ∀ (X : Set ↑M.E), f '' ↑X = ↑(⇑e '' X)
x✝¹ : α
hx : x✝¹ ∈ M.E
x✝ : α
hy : x✝ ∈ M.E
⊢ f x✝¹ = f x✝ → x✝¹ = x✝
no goals