From 254bd02458ba51a439de1bc9ae07091f7e0b32bd Mon Sep 17 00:00:00 2001
From: mariainesdff <mariainesdff@gmail.com>
Date: Tue, 14 Oct 2025 13:20:16 +0200
Subject: [PATCH] feat: add Finset lemmas

---
 Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean | 6 ++++++
 Mathlib/Data/Finsupp/Defs.lean                       | 4 ++++
 2 files changed, 10 insertions(+)

diff --git a/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean b/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
index b6ca8b1733ac87..0d4d190659aba6 100644
--- a/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
+++ b/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@@ -837,6 +837,12 @@ lemma prod_dvd_prod_of_dvd (f g : ι → M) (h : ∀ i ∈ s, f i ∣ g i) :
     ∏ i ∈ s, f i ∣ ∏ i ∈ s, g i :=
   Multiset.prod_dvd_prod_of_dvd _ _ h
 
+@[to_additive]
+theorem prod_map_equiv (e : ι ≃ κ) : (s.map e).prod (f ∘ e.symm) = s.prod f := by simp
+
+@[to_additive]
+theorem prod_comp_equiv {f : κ → M} (e : ι ≃ κ) : s.prod (f ∘ e) = (s.map e).prod f := by simp
+
 end CommMonoid
 
 section CancelCommMonoid
diff --git a/Mathlib/Data/Finsupp/Defs.lean b/Mathlib/Data/Finsupp/Defs.lean
index fb70965ea111d1..95333ed9a0bab8 100644
--- a/Mathlib/Data/Finsupp/Defs.lean
+++ b/Mathlib/Data/Finsupp/Defs.lean
@@ -265,6 +265,10 @@ theorem ofSupportFinite_coe {f : α → M} {hf : (Function.support f).Finite} :
     (ofSupportFinite f hf : α → M) = f :=
   rfl
 
+theorem ofSupportFinite_support {f : α → M} (hf : f.support.Finite) :
+    (ofSupportFinite f hf).support = hf.toFinset := by
+  ext; simp [ofSupportFinite_coe]
+
 instance instCanLift : CanLift (α → M) (α →₀ M) (⇑) fun f => (Function.support f).Finite where
   prf f hf := ⟨ofSupportFinite f hf, rfl⟩