feat: card (ι →₀ α) = card α ^ card ι (#17807)

From PFR

Author: YaelDillies

Mathlib/Data/Finsupp/Fintype.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen, Alex J. Best
 -/
 import Mathlib.Data.Finsupp.Defs
-import Mathlib.Data.Fintype.Basic
+import Mathlib.Data.Fintype.BigOperators
 
 /-!
 
@@ -14,17 +14,19 @@ Some lemmas on the combination of `Finsupp`, `Fintype` and `Infinite`.
 
 -/
 
+variable {ι α : Type*} [DecidableEq ι] [Fintype ι] [Zero α] [Fintype α]
 
-noncomputable instance Finsupp.fintype {ι π : Sort _} [DecidableEq ι] [Zero π] [Fintype ι]
-    [Fintype π] : Fintype (ι →₀ π) :=
+noncomputable instance Finsupp.fintype : Fintype (ι →₀ α) :=
   Fintype.ofEquiv _ Finsupp.equivFunOnFinite.symm
 
-instance Finsupp.infinite_of_left {ι π : Sort _} [Nontrivial π] [Zero π] [Infinite ι] :
-    Infinite (ι →₀ π) :=
-  let ⟨_, hm⟩ := exists_ne (0 : π)
+instance Finsupp.infinite_of_left [Nontrivial α] [Infinite ι] : Infinite (ι →₀ α) :=
+  let ⟨_, hm⟩ := exists_ne (0 : α)
   Infinite.of_injective _ <| Finsupp.single_left_injective hm
 
-instance Finsupp.infinite_of_right {ι π : Sort _} [Infinite π] [Zero π] [Nonempty ι] :
-    Infinite (ι →₀ π) :=
+instance Finsupp.infinite_of_right [Infinite α] [Nonempty ι] : Infinite (ι →₀ α) :=
   Infinite.of_injective (fun i => Finsupp.single (Classical.arbitrary ι) i)
     (Finsupp.single_injective (Classical.arbitrary ι))
+
+variable (ι α) in
+@[simp] lemma Fintype.card_finsupp : card (ι →₀ α) = card α ^ card ι := by
+  simp [card_congr Finsupp.equivFunOnFinite]