α✝ : Type ?u.21453
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card ↑(derangements (Fin (card α))) = numDerangements (card α)
α✝ : Type ?u.21453
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card ↑(derangements α) = numDerangements (card α)
rw [← card_derangements_invariant (card_fin _)]
no goals
α✝ : Type ?u.21453
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card ↑(derangements (Fin (card α))) = numDerangements (card α)
exact card_derangements_fin_eq_numDerangements