no goals
α : Type u
β : Type v
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
inst✝² : DecidableEq β
inst✝¹ : Fintype β
e : Perm α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
⊢ ↑sign (extendDomain e f) = ↑sign e
simp only [Equiv.Perm.extendDomain, sign_subtypeCongr, sign_permCongr, sign_refl, mul_one]