no goals
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : DecidableEq β
e : Perm α
f : α ↪ β
inst✝¹ : DecidableEq α
inst✝ : Fintype β
⊢ ↑sign (viaFintypeEmbedding e f) = ↑sign e
simp [Equiv.Perm.viaFintypeEmbedding]