feat(data/finsupp/basic): add finsupp.prod_congr and sum_congr (#10568)

These are the counterparts for `finsupp` of a simpler form of `finset.prod_congr`

Author: stuart-presnell

src/data/finsupp/basic.lean

@@ -770,6 +770,11 @@ lemma _root_.submonoid.finsupp_prod_mem (S : submonoid N) (f : α →₀ M) (g :
   (h : ∀ c, f c ≠ 0 → g c (f c) ∈ S) : f.prod g ∈ S :=
 S.prod_mem $ λ i hi, h _ (finsupp.mem_support_iff.mp hi)
 
+@[to_additive]
+lemma prod_congr {f : α →₀ M} {g1 g2 : α → M → N}
+  (h : ∀ x ∈ f.support, g1 x (f x) = g2 x (f x)) : f.prod g1 = f.prod g2 :=
+finset.prod_congr rfl h
+
 end sum_prod
 
 /-!
@@ -1438,7 +1443,7 @@ begin
   refine ((sum_sum_index _ _).trans _).symm,
   { intros, exact single_zero },
   { intros, exact single_add },
-  refine sum_congr rfl (λ _ _, sum_single_index _),
+  refine sum_congr (λ _ _, sum_single_index _),
   { exact single_zero }
 end
 
@@ -1497,7 +1502,7 @@ finset.subset.trans support_sum $
 lemma prod_map_domain_index [comm_monoid N] {f : α → β} {s : α →₀ M}
   {h : β → M → N} (h_zero : ∀b, h b 0 = 1) (h_add : ∀b m₁ m₂, h b (m₁ + m₂) = h b m₁ * h b m₂) :
   (map_domain f s).prod h = s.prod (λa m, h (f a) m) :=
-(prod_sum_index h_zero h_add).trans $ prod_congr rfl $ λ _ _, prod_single_index (h_zero _)
+(prod_sum_index h_zero h_add).trans $ prod_congr $ λ _ _, prod_single_index (h_zero _)
 
 /--
 A version of `sum_map_domain_index` that takes a bundled `add_monoid_hom`,