[Merged by Bors] - feat: add Finset lemmas

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

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⟩