simp [Finset.app_mapEquiv_symm]
case mp
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f f' : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : { x // x ∈ Finset.map f' Finset.univ }
h : f' ↑((Finset.mapEquiv Finset.univ f).symm x) = ↑y
⊢ ↑x = f ↑((Finset.mapEquiv Finset.univ f).symm x)
no goals