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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ ∑ k ∈ range (card α + 1), k * p α k = card α * (card α - 1)!
Tactic:
have A : ∀ (k) (σ : fiber α k), card (fixedPoints (↑σ : Perm α)) = k := fun k σ => σ.2
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
A : ∀ (k : ℕ) (σ : ↑(fiber α k)), card ↑(fixedPoints ⇑↑σ) = k
⊢ ∑ k ∈ range (card α + 1), k * p α k = card α * (card α - 1)!

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