simpa [A, ← Fin.sum_univ_eq_sum_range, -card_ofFinset, Finset.card_univ, card_fixed_points,
  mul_comm] using card_congr (fixedPointsEquiv' α)
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
A : ∀ (k : ℕ) (σ : ↑(fiber α k)), card ↑(fixedPoints ⇑↑σ) = k
⊢ ∑ k ∈ range (card α + 1), k * p α k = card α * (card α - 1)!
no goals