simp [card_congr (fixedPointsEquiv α), card_perm, Finset.filter_not, Finset.card_sdiff,
  Finset.filter_eq', Finset.card_univ]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card { σx // σx.2 σx.1 = σx.1 } = card α * (card α - 1)!
no goals