Theorem: Imo1987P1.card_fixed_points (Compfiles/Imo1987P1.lean)

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