From fa2309577c7009ea243cffdf990cd6c84f0ad497 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 28 Apr 2023 11:17:47 +0000
Subject: [PATCH] fix(algebra/big_operators): add missing `to_additive`s
 (#18878)

These lemmas were written before `pi.mul_single` existed.
---
 src/algebra/big_operators/basic.lean | 28 ++++++++++++-----------
 src/algebra/big_operators/pi.lean    | 34 +++++++++++++++-------------
 2 files changed, 33 insertions(+), 29 deletions(-)

diff --git a/src/algebra/big_operators/basic.lean b/src/algebra/big_operators/basic.lean
index c84cebf6727e3..85ce482038a50 100644
--- a/src/algebra/big_operators/basic.lean
+++ b/src/algebra/big_operators/basic.lean
@@ -865,15 +865,16 @@ lemma prod_dite_irrel (p : Prop) [decidable p] (s : finset α) (f : p → α →
   (∏ x in s, if h : p then f h x else g h x) = if h : p then ∏ x in s, f h x else ∏ x in s, g h x :=
 by { split_ifs with h; refl }
 
-@[simp] lemma sum_pi_single' {ι M : Type*} [decidable_eq ι] [add_comm_monoid M]
-  (i : ι) (x : M) (s : finset ι) :
-  ∑ j in s, pi.single i x j = if i ∈ s then x else 0 :=
-sum_dite_eq' _ _ _
+@[simp, to_additive]
+lemma prod_pi_mul_single' [decidable_eq α] (a : α) (x : β) (s : finset α) :
+  ∏ a' in s, pi.mul_single a x a' = if a ∈ s then x else 1 :=
+prod_dite_eq' _ _ _
 
-@[simp] lemma sum_pi_single {ι : Type*} {M : ι → Type*}
-  [decidable_eq ι] [Π i, add_comm_monoid (M i)] (i : ι) (f : Π i, M i) (s : finset ι) :
-  ∑ j in s, pi.single j (f j) i = if i ∈ s then f i else 0 :=
-sum_dite_eq _ _ _
+@[simp, to_additive]
+lemma prod_pi_mul_single {β : α → Type*}
+  [decidable_eq α] [Π a, comm_monoid (β a)] (a : α) (f : Π a, β a) (s : finset α) :
+  ∏ a' in s, pi.mul_single a' (f a') a = if a ∈ s then f a else 1 :=
+prod_dite_eq _ _ _
 
 @[to_additive]
 lemma prod_bij_ne_one {s : finset α} {t : finset γ} {f : α → β} {g : γ → β}
@@ -1350,13 +1351,14 @@ begin
     exact λ i hi, if_neg (h i hi) }
 end
 
-lemma sum_erase_lt_of_pos {γ : Type*} [decidable_eq α] [ordered_add_comm_monoid γ]
-  [covariant_class γ γ (+) (<)] {s : finset α} {d : α} (hd : d ∈ s) {f : α → γ} (hdf : 0 < f d) :
-  ∑ (m : α) in s.erase d, f m < ∑ (m : α) in s, f m :=
+@[to_additive]
+lemma prod_erase_lt_of_one_lt {γ : Type*} [decidable_eq α] [ordered_comm_monoid γ]
+  [covariant_class γ γ (*) (<)] {s : finset α} {d : α} (hd : d ∈ s) {f : α → γ} (hdf : 1 < f d) :
+  ∏ (m : α) in s.erase d, f m < ∏ (m : α) in s, f m :=
 begin
   nth_rewrite_rhs 0 ←finset.insert_erase hd,
-  rw finset.sum_insert (finset.not_mem_erase d s),
-  exact lt_add_of_pos_left _ hdf,
+  rw finset.prod_insert (finset.not_mem_erase d s),
+  exact lt_mul_of_one_lt_left' _ hdf,
 end
 
 /-- If a product is 1 and the function is 1 except possibly at one
diff --git a/src/algebra/big_operators/pi.lean b/src/algebra/big_operators/pi.lean
index 4e6021c97864a..ee2f6fc4b94c5 100644
--- a/src/algebra/big_operators/pi.lean
+++ b/src/algebra/big_operators/pi.lean
@@ -56,35 +56,37 @@ lemma prod_mk_prod {α β γ : Type*} [comm_monoid α] [comm_monoid β] (s : fin
 by haveI := classical.dec_eq γ; exact
 finset.induction_on s rfl (by simp [prod.ext_iff] {contextual := tt})
 
-section single
+section mul_single
 variables {I : Type*} [decidable_eq I] {Z : I → Type*}
-variables [Π i, add_comm_monoid (Z i)]
+variables [Π i, comm_monoid (Z i)]
 
--- As we only defined `single` into `add_monoid`, we only prove the `finset.sum` version here.
-lemma finset.univ_sum_single [fintype I] (f : Π i, Z i) :
-  ∑ i, pi.single i (f i) = f :=
+@[to_additive]
+lemma finset.univ_prod_mul_single [fintype I] (f : Π i, Z i) :
+  ∏ i, pi.mul_single i (f i) = f :=
 by { ext a, simp }
 
-lemma add_monoid_hom.functions_ext [finite I] (G : Type*) [add_comm_monoid G]
-  (g h : (Π i, Z i) →+ G) (H : ∀ i x, g (pi.single i x) = h (pi.single i x)) : g = h :=
+@[to_additive]
+lemma monoid_hom.functions_ext [finite I] (G : Type*) [comm_monoid G]
+  (g h : (Π i, Z i) →* G) (H : ∀ i x, g (pi.mul_single i x) = h (pi.mul_single i x)) : g = h :=
 begin
   casesI nonempty_fintype I,
   ext k,
-  rw [← finset.univ_sum_single k, g.map_sum, h.map_sum],
+  rw [← finset.univ_prod_mul_single k, g.map_prod, h.map_prod],
   simp only [H]
 end
 
-/-- This is used as the ext lemma instead of `add_monoid_hom.functions_ext` for reasons explained in
+/-- This is used as the ext lemma instead of `monoid_hom.functions_ext` for reasons explained in
 note [partially-applied ext lemmas]. -/
-@[ext]
-lemma add_monoid_hom.functions_ext' [finite I] (M : Type*) [add_comm_monoid M]
-  (g h : (Π i, Z i) →+ M)
-  (H : ∀ i, g.comp (add_monoid_hom.single Z i) = h.comp (add_monoid_hom.single Z i)) :
+@[ext, to_additive "
+This is used as the ext lemma instead of `add_monoid_hom.functions_ext` for reasons explained in
+note [partially-applied ext lemmas]."]
+lemma monoid_hom.functions_ext' [finite I] (M : Type*) [comm_monoid M]
+  (g h : (Π i, Z i) →* M)
+  (H : ∀ i, g.comp (monoid_hom.single Z i) = h.comp (monoid_hom.single Z i)) :
   g = h :=
-have _ := λ i, add_monoid_hom.congr_fun (H i), -- elab without an expected type
-g.functions_ext M h this
+g.functions_ext M h $ λ i, monoid_hom.congr_fun (H i)
 
-end single
+end mul_single
 
 section ring_hom
 open pi