feat(data/finsupp/basic): Version of finsupp.prod_add_index with we…

…aker premises (#11353)

A simpler proof of `finsupp.prod_add_index : (f + g).prod h = f.prod h * g.prod h` with weaker premises.

Specifically, this only requires:
* `[add_zero_class M]` rather than `[add_comm_monoid M]`
* `h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1` rather than `h_zero : ∀a, h a 0 = 1`.  
* `h_add : ∀ (a ∈ f.support ∪ g.support) b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂` rather than `h_add : ∀ a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂` (thanks to Anne Baanen for spotting this weakening).

The original version has been retained and re-named to `finsupp.prod_add_index'`, since in some places this is more convenient to use.  (There was already a lemma called `prod_add_index'` which appears not to have been used anywhere.  This has been renamed to `prod_hom_add_index`.)

Discussed in this Zulip thread:
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Variant.20of.20finsupp.2Eprod_add_index.3F

src/algebra/big_operators/finsupp.lean

@@ -35,7 +35,7 @@ open_locale classical
 
 theorem finsupp.sum_sum_index' : (∑ x in s, f x).sum t = ∑ x in s, (f x).sum t :=
 finset.induction_on s rfl $ λ a s has ih,
-by simp_rw [finset.sum_insert has, finsupp.sum_add_index h0 h1, ih]
+by simp_rw [finset.sum_insert has, finsupp.sum_add_index' h0 h1, ih]
 
 end
 

src/data/finsupp/basic.lean

@@ -1211,37 +1211,55 @@ lemma prod_inv [has_zero M] [comm_group G] {f : α →₀ M}
   f.sum (λa b, h₁ a b - h₂ a b) = f.sum h₁ - f.sum h₂ :=
 finset.sum_sub_distrib
 
-@[to_additive]
-lemma prod_add_index [add_comm_monoid M] [comm_monoid N] {f g : α →₀ M}
+/-- Taking the product under `h` is an additive-to-multiplicative homomorphism of finsupps,
+if `h` is an additive-to-multiplicative homomorphism on the support.
+This is a more general version of `finsupp.prod_add_index'`; the latter has simpler hypotheses. -/
+@[to_additive "Taking the product under `h` is an additive homomorphism of finsupps,
+if `h` is an additive homomorphism on the support.
+This is a more general version of `finsupp.sum_add_index'`; the latter has simpler hypotheses."]
+lemma prod_add_index [add_zero_class M] [comm_monoid N] {f g : α →₀ M}
+  {h : α → M → N} (h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1)
+  (h_add : ∀ (a ∈ f.support ∪ g.support) b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) :
+  (f + g).prod h = f.prod h * g.prod h :=
+begin
+  rw [finsupp.prod_of_support_subset f (subset_union_left _ g.support) h h_zero,
+      finsupp.prod_of_support_subset g (subset_union_right f.support _) h h_zero,
+      ←finset.prod_mul_distrib,
+      finsupp.prod_of_support_subset (f + g) finsupp.support_add h h_zero],
+  exact finset.prod_congr rfl (λ x hx, (by apply h_add x hx)),
+end
+
+/-- Taking the product under `h` is an additive-to-multiplicative homomorphism of finsupps,
+if `h` is an additive-to-multiplicative homomorphism.
+This is a more specialized version of `finsupp.prod_add_index` with simpler hypotheses. -/
+@[to_additive "Taking the product under `h` is an additive homomorphism of finsupps,
+if `h` is an additive homomorphism.
+This is a more specific version of `finsupp.sum_add_index` with simpler hypotheses."]
+lemma prod_add_index' [add_zero_class M] [comm_monoid N] {f g : α →₀ M}
   {h : α → M → N} (h_zero : ∀a, h a 0 = 1) (h_add : ∀a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) :
   (f + g).prod h = f.prod h * g.prod h :=
-have hf : f.prod h = ∏ a in f.support ∪ g.support, h a (f a),
-  from f.prod_of_support_subset (subset_union_left _ _) _ $ λ a ha, h_zero a,
-have hg : g.prod h = ∏ a in f.support ∪ g.support, h a (g a),
-  from g.prod_of_support_subset (subset_union_right _ _) _ $ λ a ha, h_zero a,
-have hfg : (f + g).prod h = ∏ a in f.support ∪ g.support, h a ((f + g) a),
-  from (f + g).prod_of_support_subset support_add _ $ λ a ha, h_zero a,
-by simp only [*, add_apply, prod_mul_distrib]
+prod_add_index (λ a ha, h_zero a) (λ a ha, h_add a)
 
 @[simp]
-lemma sum_add_index' [add_comm_monoid M] [add_comm_monoid N] {f g : α →₀ M} (h : α → M →+ N) :
+lemma sum_hom_add_index [add_zero_class M] [add_comm_monoid N] {f g : α →₀ M} (h : α → M →+ N) :
   (f + g).sum (λ x, h x) = f.sum (λ x, h x) + g.sum (λ x, h x) :=
-sum_add_index (λ a, (h a).map_zero) (λ a, (h a).map_add)
+sum_add_index' (λ a, (h a).map_zero) (λ a, (h a).map_add)
 
 @[simp]
-lemma prod_add_index' [add_comm_monoid M] [comm_monoid N] {f g : α →₀ M}
+lemma prod_hom_add_index [add_zero_class M] [comm_monoid N] {f g : α →₀ M}
   (h : α → multiplicative M →* N) :
   (f + g).prod (λ a b, h a (multiplicative.of_add b)) =
     f.prod (λ a b, h a (multiplicative.of_add b)) * g.prod (λ a b, h a (multiplicative.of_add b)) :=
-prod_add_index (λ a, (h a).map_one) (λ a, (h a).map_mul)
+prod_add_index' (λ a, (h a).map_one) (λ a, (h a).map_mul)
+
 
 /-- The canonical isomorphism between families of additive monoid homomorphisms `α → (M →+ N)`
 and monoid homomorphisms `(α →₀ M) →+ N`. -/
-def lift_add_hom [add_comm_monoid M] [add_comm_monoid N] : (α → M →+ N) ≃+ ((α →₀ M) →+ N) :=
+def lift_add_hom [add_zero_class M] [add_comm_monoid N] : (α → M →+ N) ≃+ ((α →₀ M) →+ N) :=
 { to_fun := λ F,
   { to_fun := λ f, f.sum (λ x, F x),
     map_zero' := finset.sum_empty,
-    map_add' := λ _ _, sum_add_index (λ x, (F x).map_zero) (λ x, (F x).map_add) },
+    map_add' := λ _ _, sum_add_index' (λ x, (F x).map_zero) (λ x, (F x).map_add) },
   inv_fun := λ F x, F.comp $ single_add_hom x,
   left_inv := λ F, by { ext, simp },
   right_inv := λ F, by { ext, simp },
@@ -1305,7 +1323,7 @@ lemma prod_finset_sum_index [add_comm_monoid M] [comm_monoid N]
   {h : α → M → N} (h_zero : ∀a, h a 0 = 1) (h_add : ∀a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) :
   ∏ i in s, (g i).prod h = (∑ i in s, g i).prod h :=
 finset.induction_on s rfl $ λ a s has ih,
-by rw [prod_insert has, ih, sum_insert has, prod_add_index h_zero h_add]
+by rw [prod_insert has, ih, sum_insert has, prod_add_index' h_zero h_add]
 
 @[to_additive]
 lemma prod_sum_index
@@ -1321,7 +1339,7 @@ lemma multiset_sum_sum_index
   (h₀ : ∀a, h a 0 = 0) (h₁ : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) :
   (f.sum.sum h) = (f.map $ λg:α →₀ M, g.sum h).sum :=
 multiset.induction_on f rfl $ assume a s ih,
-by rw [multiset.sum_cons, multiset.map_cons, multiset.sum_cons, sum_add_index h₀ h₁, ih]
+by rw [multiset.sum_cons, multiset.map_cons, multiset.sum_cons, sum_add_index' h₀ h₁, ih]
 
 lemma support_sum_eq_bUnion {α : Type*} {ι : Type*} {M : Type*} [add_comm_monoid M]
   {g : ι → α →₀ M} (s : finset ι) (h : ∀ i₁ i₂, i₁ ≠ i₂ → disjoint (g i₁).support (g i₂).support) :
@@ -1560,7 +1578,7 @@ lemma map_domain_congr {f g : α → β} (h : ∀x∈v.support, f x = g x) :
 finset.sum_congr rfl $ λ _ H, by simp only [h _ H]
 
 lemma map_domain_add {f : α → β} : map_domain f (v₁ + v₂) = map_domain f v₁ + map_domain f v₂ :=
-sum_add_index (λ _, single_zero) (λ _ _ _, single_add)
+sum_add_index' (λ _, single_zero) (λ _ _ _, single_add)
 
 @[simp] lemma map_domain_equiv_apply {f : α ≃ β} (x : α →₀ M) (a : β) :
   map_domain f x a = x (f.symm a) :=
@@ -1709,9 +1727,9 @@ lemma sum_update_add [add_comm_monoid α] [add_comm_monoid β]
   (hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂) :
   (f.update i a).sum g + g i (f i) = f.sum g + g i a :=
 begin
-  rw [update_eq_erase_add_single, sum_add_index hg hgg],
+  rw [update_eq_erase_add_single, sum_add_index' hg hgg],
   conv_rhs { rw ← finsupp.update_self f i },
-  rw [update_eq_erase_add_single, sum_add_index hg hgg, add_assoc, add_assoc],
+  rw [update_eq_erase_add_single, sum_add_index' hg hgg, add_assoc, add_assoc],
   congr' 1,
   rw [add_comm, sum_single_index (hg _), sum_single_index (hg _)],
 end
@@ -2141,7 +2159,7 @@ begin
   rw [finsupp.curry],
   transitivity,
   { exact sum_sum_index (assume a, sum_zero_index)
-      (assume a b₀ b₁, sum_add_index (assume a, hg₀ _ _) (assume c d₀ d₁, hg₁ _ _ _ _)) },
+      (assume a b₀ b₁, sum_add_index' (assume a, hg₀ _ _) (assume c d₀ d₁, hg₁ _ _ _ _)) },
   congr, funext p c,
   transitivity,
   { exact sum_single_index sum_zero_index },

src/data/finsupp/multiset.lean

@@ -31,7 +31,7 @@ def to_multiset : (α →₀ ℕ) ≃+ multiset α :=
         mem_support_iff, multiset.count_nsmul, finset.sum_ite_eq, ite_not, ite_eq_right_iff],
       exact eq.symm },
   right_inv := λ s, by simp only [sum, coe_mk, multiset.to_finset_sum_count_nsmul_eq],
-  map_add' := λ f g, sum_add_index (λ a, zero_nsmul _) (λ a, add_nsmul _) }
+  map_add' := λ f g, sum_add_index' (λ a, zero_nsmul _) (λ a, add_nsmul _) }
 
 lemma to_multiset_zero : (0 : α →₀ ℕ).to_multiset = 0 := rfl
 
@@ -77,11 +77,9 @@ begin
   refine f.induction _ _,
   { rw [to_multiset_zero, multiset.prod_zero, finsupp.prod_zero_index] },
   { assume a n f _ _ ih,
-    rw [to_multiset_add, multiset.prod_add, ih, to_multiset_single, finsupp.prod_add_index,
-      finsupp.prod_single_index, multiset.prod_nsmul, multiset.prod_singleton],
-    { exact pow_zero a },
-    { exact pow_zero },
-    { exact pow_add } }
+    rw [to_multiset_add, multiset.prod_add, ih, to_multiset_single, multiset.prod_nsmul,
+      finsupp.prod_add_index' pow_zero pow_add, finsupp.prod_single_index, multiset.prod_singleton],
+    { exact pow_zero a } }
 end
 
 @[simp] lemma to_finset_to_multiset [decidable_eq α] (f : α →₀ ℕ) :

src/data/mv_polynomial/variables.lean

@@ -597,7 +597,7 @@ finset.sup_le $ assume n hn,
   begin
     simp only [finset.mem_bUnion, finset.mem_singleton] at this,
     rcases this with ⟨a₁, h₁, a₂, h₂, rfl⟩,
-    rw [finsupp.sum_add_index],
+    rw [finsupp.sum_add_index'],
     { exact add_le_add (finset.le_sup h₁) (finset.le_sup h₂) },
     { assume a, refl },
     { assume a b₁ b₂, refl }

src/data/nat/factorization.lean

@@ -225,7 +225,7 @@ begin
     set K := n.factorization - d.factorization with hK,
     use K.prod pow,
     rw [←factorization_prod_pow_eq_self hn, ←factorization_prod_pow_eq_self hd,
-        ←finsupp.prod_add_index pow_zero pow_add, hK, add_tsub_cancel_of_le hdn] },
+        ←finsupp.prod_add_index' pow_zero pow_add, hK, add_tsub_cancel_of_le hdn] },
   { rintro ⟨c, rfl⟩, rw factorization_mul hd (right_ne_zero_of_mul hn), simp },
 end
 

src/data/polynomial/basic.lean

@@ -547,7 +547,7 @@ lemma sum_add_index {S : Type*} [add_comm_monoid S] (p q : R[X])
 begin
   rcases p, rcases q,
   simp only [add_to_finsupp, sum, support, coeff, pi.add_apply, coe_add],
-  exact finsupp.sum_add_index hf h_add,
+  exact finsupp.sum_add_index' hf h_add,
 end
 
 lemma sum_add' {S : Type*} [add_comm_monoid S] (p : R[X]) (f g : ℕ → R → S) :