feat: Lemmas specialised to piFinset fun _ : Fin n ↦ s (#15329)

Those lemmas are specifically useful for rewriting backwards when the indexing type doesn't matter (and also sometimes useful forwardly).

From LeanAPAP

Author: YaelDillies

Mathlib/Data/Fintype/BigOperators.lean

@@ -112,9 +112,21 @@ namespace Fintype
 @[simp] lemma card_piFinset (s : ∀ i, Finset (α i)) :
     (piFinset s).card = ∏ i, (s i).card := by simp [piFinset, card_map]
 
+/-- This lemma is specifically designed to be used backwards, whence the specialisation to `Fin n`
+as the indexing type doesn't matter in practice. The more general forward direction lemma here is
+`Fintype.card_piFinset`. -/
+lemma card_piFinset_const {α : Type*} (s : Finset α) (n : ℕ) :
+    (piFinset fun _ : Fin n ↦ s).card = s.card ^ n := by simp
+
 @[simp] lemma card_pi [DecidableEq ι] [∀ i, Fintype (α i)] : card (∀ i, α i) = ∏ i, card (α i) :=
   card_piFinset _
 
+/-- This lemma is specifically designed to be used backwards, whence the specialisation to `Fin n`
+as the indexing type doesn't matter in practice. The more general forward direction lemma here is
+`Fintype.card_pi`. -/
+lemma card_pi_const (α : Type*) [Fintype α] (n : ℕ) : card (Fin n → α) = card α ^ n :=
+  card_piFinset_const _ _
+
 @[simp] nonrec lemma card_sigma [Fintype ι] [∀ i, Fintype (α i)] :
     card (Sigma α) = ∑ i, card (α i) := card_sigma _ _
 

Mathlib/Data/Fintype/Pi.lean

@@ -56,6 +56,9 @@ theorem piFinset_empty [Nonempty α] : piFinset (fun _ => ∅ : ∀ i, Finset (
 lemma piFinset_nonempty : (piFinset s).Nonempty ↔ ∀ a, (s a).Nonempty := by
   simp [Finset.Nonempty, Classical.skolem]
 
+lemma _root_.Finset.Nonempty.piFinset_const {ι : Type*} [Fintype ι] [DecidableEq ι] {s : Finset α}
+    (hs : s.Nonempty) : (piFinset fun _ : ι ↦ s).Nonempty := piFinset_nonempty.2 fun _ ↦ hs
+
 @[simp]
 lemma piFinset_of_isEmpty [IsEmpty α] (s : ∀ a, Finset (γ a)) : piFinset s = univ :=
   eq_univ_of_forall fun _ ↦ by simp