From e452b202d1aaa49d248d1214a3fe46504a87d6cd Mon Sep 17 00:00:00 2001
From: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Wed, 23 Nov 2022 20:18:48 +0100
Subject: [PATCH 1/7] reorg

---
 src/algebra/big_operators/multiset.lean       |   2 +-
 src/algebra/free_monoid/basic.lean            |   2 +-
 src/algebra/graded_monoid.lean                |   2 +-
 .../basic.lean}                               | 138 +--------------
 src/data/list/big_operators/lemmas.lean       | 167 ++++++++++++++++++
 src/data/list/count.lean                      |   2 +-
 src/data/list/join.lean                       |   2 +-
 src/data/list/prime.lean                      |   2 +-
 src/data/list/prod_sigma.lean                 |   2 +-
 src/data/list/zip.lean                        |   2 +-
 10 files changed, 177 insertions(+), 144 deletions(-)
 rename src/data/list/{big_operators.lean => big_operators/basic.lean} (79%)
 create mode 100644 src/data/list/big_operators/lemmas.lean

diff --git a/src/algebra/big_operators/multiset.lean b/src/algebra/big_operators/multiset.lean
index 2c97988ba2a7d..8aadedfeb1d41 100644
--- a/src/algebra/big_operators/multiset.lean
+++ b/src/algebra/big_operators/multiset.lean
@@ -3,7 +3,7 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import data.list.big_operators
+import data.list.big_operators.basic
 import data.multiset.basic
 
 /-!
diff --git a/src/algebra/free_monoid/basic.lean b/src/algebra/free_monoid/basic.lean
index d208f9116ffc5..224f4956db049 100644
--- a/src/algebra/free_monoid/basic.lean
+++ b/src/algebra/free_monoid/basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Yury Kudryashov
 -/
-import data.list.big_operators
+import data.list.big_operators.basic
 
 /-!
 # Free monoid over a given alphabet
diff --git a/src/algebra/graded_monoid.lean b/src/algebra/graded_monoid.lean
index b1148140c6b47..9aae3d0e47614 100644
--- a/src/algebra/graded_monoid.lean
+++ b/src/algebra/graded_monoid.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import algebra.group.inj_surj
-import data.list.big_operators
+import data.list.big_operators.basic
 import data.list.range
 import group_theory.group_action.defs
 import group_theory.submonoid.basic
diff --git a/src/data/list/big_operators.lean b/src/data/list/big_operators/basic.lean
similarity index 79%
rename from src/data/list/big_operators.lean
rename to src/data/list/big_operators/basic.lean
index 4cba570c87485..5fc96d9847ebb 100644
--- a/src/data/list/big_operators.lean
+++ b/src/data/list/big_operators/basic.lean
@@ -4,17 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Floris van Doorn, Sébastien Gouëzel, Alex J. Best
 -/
 import data.list.forall2
-import algebra.group.opposite
-import algebra.group_power.basic
-import algebra.group_with_zero.commute
-import algebra.group_with_zero.divisibility
-import algebra.order.with_zero
-import algebra.ring.basic
-import algebra.ring.divisibility
-import algebra.ring.commute
-import data.int.basic
-import data.int.units
-import data.set.basic
 
 /-!
 # Sums and products from lists
@@ -138,7 +127,7 @@ end
 @[simp, to_additive]
 lemma prod_take_mul_prod_drop :
   ∀ (L : list M) (i : ℕ), (L.take i).prod * (L.drop i).prod = L.prod
-| [] i := by simp [@zero_le' ℕ]
+| [] i := by simp [nat.zero_le]
 | L 0 := by simp
 | (h :: t) (n+1) := by { dsimp, rw [prod_cons, prod_cons, mul_assoc, prod_take_mul_prod_drop] }
 
@@ -172,7 +161,7 @@ lemma prod_update_nth : ∀ (L : list M) (n : ℕ) (a : M),
     (L.take n).prod * (if n < L.length then a else 1) * (L.drop (n + 1)).prod
 | (x :: xs) 0     a := by simp [update_nth]
 | (x :: xs) (i+1) a := by simp [update_nth, prod_update_nth xs i a, mul_assoc]
-| []      _     _ := by simp [update_nth, (nat.zero_le _).not_lt, @zero_le' ℕ]
+| []      _     _ := by simp [update_nth, (nat.zero_le _).not_lt, nat.zero_le]
 
 open mul_opposite
 
@@ -210,21 +199,6 @@ lemma _root_.commute.list_prod_left (l : list M) (y : M) (h : ∀ (x ∈ l), com
   commute l.prod y  :=
 (commute.list_prod_right _ _ $ λ x hx, (h _ hx).symm).symm
 
-lemma _root_.commute.list_sum_right [non_unital_non_assoc_semiring R] (a : R) (l : list R)
-  (h : ∀ b ∈ l, commute a b) :
-  commute a l.sum :=
-begin
-  induction l with x xs ih,
-  { exact commute.zero_right _, },
-  { rw sum_cons,
-    exact (h _ $ mem_cons_self _ _).add_right (ih $ λ j hj, h _ $ mem_cons_of_mem _ hj) }
-end
-
-lemma _root_.commute.list_sum_left [non_unital_non_assoc_semiring R] (b : R) (l : list R)
-  (h : ∀ a ∈ l, commute a b) :
-  commute l.sum b :=
-(commute.list_sum_right _ _ $ λ x hx, (h _ hx).symm).symm
-
 @[to_additive sum_le_sum] lemma forall₂.prod_le_prod' [preorder M]
   [covariant_class M M (function.swap (*)) (≤)] [covariant_class M M (*) (≤)]
   {l₁ l₂ : list M} (h : forall₂ (≤) l₁ l₂) : l₁.prod ≤ l₂.prod :=
@@ -293,13 +267,6 @@ lemma prod_le_pow_card [preorder M]
   l.prod ≤ n ^ l.length :=
 by simpa only [map_id'', map_const, prod_repeat] using prod_le_prod' h
 
-@[to_additive card_nsmul_le_sum]
-lemma pow_card_le_prod [preorder M]
-  [covariant_class M M (function.swap (*)) (≤)] [covariant_class M M (*) (≤)]
-  (l : list M) (n : M) (h : ∀ (x ∈ l), n ≤ x) :
-  n ^ l.length ≤ l.prod :=
-@prod_le_pow_card Mᵒᵈ _ _ _ _ l n h
-
 @[to_additive exists_lt_of_sum_lt] lemma exists_lt_of_prod_lt' [linear_order M]
   [covariant_class M M (function.swap (*)) (≤)] [covariant_class M M (*) (≤)] {l : list ι}
   (f g : ι → M) (h : (l.map f).prod < (l.map g).prod) :
@@ -461,39 +428,6 @@ lemma all_one_of_le_one_le_of_prod_eq_one [ordered_comm_monoid M]
   x = 1 :=
 le_antisymm (hl₂ ▸ single_le_prod hl₁ _ hx) (hl₁ x hx)
 
-@[to_additive] lemma prod_eq_one_iff [canonically_ordered_monoid M] (l : list M) :
-  l.prod = 1 ↔ ∀ x ∈ l, x = (1 : M) :=
-⟨all_one_of_le_one_le_of_prod_eq_one (λ _ _, one_le _),
-  λ h, by rw [eq_repeat.2 ⟨rfl, h⟩, prod_repeat, one_pow]⟩
-
-/-- Slightly more general version of `list.prod_eq_one_iff` for a non-ordered `monoid` -/
-@[to_additive "Slightly more general version of `list.sum_eq_zero_iff`
-  for a non-ordered `add_monoid`"]
-lemma prod_eq_one [monoid M] {l : list M} (hl : ∀ (x ∈ l), x = (1 : M)) : l.prod = 1 :=
-trans (prod_eq_pow_card l 1 hl) (one_pow l.length)
-
-@[to_additive]
-lemma exists_mem_ne_one_of_prod_ne_one [monoid M] {l : list M} (h : l.prod ≠ 1) :
-  ∃ (x ∈ l), x ≠ (1 : M) :=
-by simpa only [not_forall] using mt prod_eq_one h
-
-/-- If a product of integers is `-1`, then at least one factor must be `-1`. -/
-lemma neg_one_mem_of_prod_eq_neg_one {l : list ℤ} (h : l.prod = -1) : (-1 : ℤ) ∈ l :=
-begin
-  obtain ⟨x, h₁, h₂⟩ := exists_mem_ne_one_of_prod_ne_one (ne_of_eq_of_ne h dec_trivial),
-  exact or.resolve_left (int.is_unit_iff.mp (prod_is_unit_iff.mp
-         (h.symm ▸ is_unit.neg is_unit_one : is_unit l.prod) x h₁)) h₂ ▸ h₁,
-end
-
-/-- If all elements in a list are bounded below by `1`, then the length of the list is bounded
-by the sum of the elements. -/
-lemma length_le_sum_of_one_le (L : list ℕ) (h : ∀ i ∈ L, 1 ≤ i) : L.length ≤ L.sum :=
-begin
-  induction L with j L IH h, { simp },
-  rw [sum_cons, length, add_comm],
-  exact add_le_add (h _ (set.mem_insert _ _)) (IH (λ i hi, h i (set.mem_union_right _ hi)))
-end
-
 -- TODO: develop theory of tropical rings
 lemma sum_le_foldr_max [add_monoid M] [add_monoid N] [linear_order N] (f : M → N)
   (h0 : f 0 ≤ 0) (hadd : ∀ x y, f (x + y) ≤ max (f x) (f y)) (l : list M) :
@@ -526,21 +460,9 @@ lemma prod_map_erase [decidable_eq ι] [comm_monoid M] (f : ι → M) {a} :
         mul_left_comm (f a) (f b)], }
   end
 
-lemma dvd_prod [comm_monoid M] {a} {l : list M} (ha : a ∈ l) : a ∣ l.prod :=
-let ⟨s, t, h⟩ := mem_split ha in
-by { rw [h, prod_append, prod_cons, mul_left_comm], exact dvd_mul_right _ _ }
-
 @[simp] lemma sum_const_nat (m n : ℕ) : sum (list.repeat m n) = m * n :=
 by induction n; [refl, simp only [*, repeat_succ, sum_cons, nat.mul_succ, add_comm]]
 
-lemma dvd_sum [semiring R] {a} {l : list R} (h : ∀ x ∈ l, a ∣ x) : a ∣ l.sum :=
-begin
-  induction l with x l ih,
-  { exact dvd_zero _ },
-  { rw [list.sum_cons],
-    exact dvd_add (h _ (mem_cons_self _ _)) (ih (λ x hx, h x (mem_cons_of_mem _ hx))) }
-end
-
 /-- The product of a list of positive natural numbers is positive,
 and likewise for any nontrivial ordered semiring. -/
 lemma prod_pos [strict_ordered_semiring R] (l : list R) (h : ∀ a ∈ l, (0 : R) < a) : 0 < l.prod :=
@@ -596,54 +518,10 @@ by rw [alternating_prod_cons_cons', alternating_prod_cons' b l, mul_inv, inv_inv
   alternating_prod (a :: l) = a / alternating_prod l :=
 by rw [div_eq_mul_inv, alternating_prod_cons']
 
-@[to_additive]
-lemma alternating_prod_append : ∀ l₁ l₂ : list α,
-  alternating_prod (l₁ ++ l₂) = alternating_prod l₁ * alternating_prod l₂ ^ (-1 : ℤ) ^ length l₁
-| [] l₂ := by simp
-| (a :: l₁) l₂ := by simp_rw [cons_append, alternating_prod_cons, alternating_prod_append,
-  length_cons, pow_succ, neg_mul, one_mul, zpow_neg, ←div_eq_mul_inv, div_div]
-
-@[to_additive]
-lemma alternating_prod_reverse :
-  ∀ l : list α, alternating_prod (reverse l) = alternating_prod l ^ (-1 : ℤ) ^ (length l + 1)
-| [] := by simp only [alternating_prod_nil, one_zpow, reverse_nil]
-| (a :: l) :=
-begin
-  simp_rw [reverse_cons, alternating_prod_append, alternating_prod_reverse,
-    alternating_prod_singleton, alternating_prod_cons, length_reverse, length, pow_succ, neg_mul,
-    one_mul, zpow_neg, inv_inv],
-  rw [mul_comm, ←div_eq_mul_inv, div_zpow],
-end
-
 end alternating
 
-lemma sum_map_mul_left [non_unital_non_assoc_semiring R] (L : list ι) (f : ι → R) (r : R) :
-  (L.map (λ b, r * f b)).sum = r * (L.map f).sum :=
-sum_map_hom L f $ add_monoid_hom.mul_left r
-
-lemma sum_map_mul_right [non_unital_non_assoc_semiring R] (L : list ι) (f : ι → R) (r : R) :
-  (L.map (λ b, f b * r)).sum = (L.map f).sum * r :=
-sum_map_hom L f $ add_monoid_hom.mul_right r
-
 end list
 
-namespace mul_opposite
-
-open list
-variables [monoid M]
-
-lemma op_list_prod : ∀ (l : list M), op (l.prod) = (l.map op).reverse.prod
-| [] := rfl
-| (x :: xs) := by rw [list.prod_cons, list.map_cons, list.reverse_cons', list.prod_concat, op_mul,
-                      op_list_prod]
-
-lemma _root_.mul_opposite.unop_list_prod (l : list Mᵐᵒᵖ) :
-  (l.prod).unop = (l.map unop).reverse.prod :=
-by rw [← op_inj, op_unop, mul_opposite.op_list_prod, map_reverse, map_map, reverse_reverse,
-  op_comp_unop, map_id]
-
-end mul_opposite
-
 section monoid_hom
 
 variables [monoid M] [monoid N]
@@ -653,11 +531,6 @@ lemma map_list_prod {F : Type*} [monoid_hom_class F M N] (f : F)
   (l : list M) : f l.prod = (l.map f).prod :=
 (l.prod_hom f).symm
 
-/-- A morphism into the opposite monoid acts on the product by acting on the reversed elements. -/
-lemma unop_map_list_prod {F : Type*} [monoid_hom_class F M Nᵐᵒᵖ] (f : F) (l : list M) :
-  (f l.prod).unop = (l.map (mul_opposite.unop ∘ f)).reverse.prod :=
-by rw [map_list_prod f l, mul_opposite.unop_list_prod, list.map_map]
-
 namespace monoid_hom
 
 /-- Deprecated, use `_root_.map_list_prod` instead. -/
@@ -666,13 +539,6 @@ protected lemma map_list_prod (f : M →* N) (l : list M) :
   f l.prod = (l.map f).prod :=
 map_list_prod f l
 
-/-- A morphism into the opposite monoid acts on the product by acting on the reversed elements.
-
-Deprecated, use `_root_.unop_map_list_prod` instead. -/
-protected lemma unop_map_list_prod (f : M →* Nᵐᵒᵖ) (l : list M) :
-  (f l.prod).unop = (l.map (mul_opposite.unop ∘ f)).reverse.prod :=
-unop_map_list_prod f l
-
 end monoid_hom
 
 end monoid_hom
diff --git a/src/data/list/big_operators/lemmas.lean b/src/data/list/big_operators/lemmas.lean
new file mode 100644
index 0000000000000..308b2cbb4f043
--- /dev/null
+++ b/src/data/list/big_operators/lemmas.lean
@@ -0,0 +1,167 @@
+/-
+Copyright (c) 2017 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Floris van Doorn, Sébastien Gouëzel, Alex J. Best
+-/
+import data.list.big_operators.basic
+import algebra.group.opposite
+import algebra.group_power.basic
+import algebra.group_with_zero.commute
+import algebra.group_with_zero.divisibility
+import algebra.order.with_zero
+import algebra.ring.basic
+import algebra.ring.divisibility
+import algebra.ring.commute
+import data.int.units
+import data.set.basic
+
+/-! # Lemmas about `list.sum` and `list.prod` requiring extra algebra imports -/
+
+open mul_opposite list
+
+variables {ι α M N P M₀ G R : Type*}
+
+namespace commute
+
+lemma list_sum_right [non_unital_non_assoc_semiring R] (a : R) (l : list R)
+  (h : ∀ b ∈ l, commute a b) :
+  commute a l.sum :=
+begin
+  induction l with x xs ih,
+  { exact commute.zero_right _, },
+  { rw list.sum_cons,
+    exact (h _ $ mem_cons_self _ _).add_right (ih $ λ j hj, h _ $ mem_cons_of_mem _ hj) }
+end
+
+lemma list_sum_left [non_unital_non_assoc_semiring R] (b : R) (l : list R)
+  (h : ∀ a ∈ l, commute a b) :
+  commute l.sum b :=
+(commute.list_sum_right _ _ $ λ x hx, (h _ hx).symm).symm
+
+end commute
+
+namespace list
+
+@[to_additive card_nsmul_le_sum]
+lemma pow_card_le_prod [monoid M] [preorder M]
+  [covariant_class M M (function.swap (*)) (≤)] [covariant_class M M (*) (≤)]
+  (l : list M) (n : M) (h : ∀ (x ∈ l), n ≤ x) :
+  n ^ l.length ≤ l.prod :=
+@prod_le_pow_card Mᵒᵈ _ _ _ _ l n h
+
+@[to_additive] lemma prod_eq_one_iff [canonically_ordered_monoid M] (l : list M) :
+  l.prod = 1 ↔ ∀ x ∈ l, x = (1 : M) :=
+⟨all_one_of_le_one_le_of_prod_eq_one (λ _ _, one_le _),
+  λ h, by rw [eq_repeat.2 ⟨rfl, h⟩, prod_repeat, one_pow]⟩
+
+/-- Slightly more general version of `list.prod_eq_one_iff` for a non-ordered `monoid` -/
+@[to_additive "Slightly more general version of `list.sum_eq_zero_iff`
+  for a non-ordered `add_monoid`"]
+lemma prod_eq_one [monoid M] {l : list M} (hl : ∀ (x ∈ l), x = (1 : M)) : l.prod = 1 :=
+trans (prod_eq_pow_card l 1 hl) (one_pow l.length)
+
+@[to_additive]
+lemma exists_mem_ne_one_of_prod_ne_one [monoid M] {l : list M} (h : l.prod ≠ 1) :
+  ∃ (x ∈ l), x ≠ (1 : M) :=
+by simpa only [not_forall] using mt prod_eq_one h
+
+/-- If a product of integers is `-1`, then at least one factor must be `-1`. -/
+lemma neg_one_mem_of_prod_eq_neg_one {l : list ℤ} (h : l.prod = -1) : (-1 : ℤ) ∈ l :=
+begin
+  obtain ⟨x, h₁, h₂⟩ := exists_mem_ne_one_of_prod_ne_one (ne_of_eq_of_ne h dec_trivial),
+  exact or.resolve_left (int.is_unit_iff.mp (prod_is_unit_iff.mp
+         (h.symm ▸ is_unit.neg is_unit_one : is_unit l.prod) x h₁)) h₂ ▸ h₁,
+end
+
+/-- If all elements in a list are bounded below by `1`, then the length of the list is bounded
+by the sum of the elements. -/
+lemma length_le_sum_of_one_le (L : list ℕ) (h : ∀ i ∈ L, 1 ≤ i) : L.length ≤ L.sum :=
+begin
+  induction L with j L IH h, { simp },
+  rw [sum_cons, length, add_comm],
+  exact add_le_add (h _ (set.mem_insert _ _)) (IH (λ i hi, h i (set.mem_union_right _ hi)))
+end
+
+lemma dvd_prod [comm_monoid M] {a} {l : list M} (ha : a ∈ l) : a ∣ l.prod :=
+let ⟨s, t, h⟩ := mem_split ha in
+by { rw [h, prod_append, prod_cons, mul_left_comm], exact dvd_mul_right _ _ }
+
+lemma dvd_sum [semiring R] {a} {l : list R} (h : ∀ x ∈ l, a ∣ x) : a ∣ l.sum :=
+begin
+  induction l with x l ih,
+  { exact dvd_zero _ },
+  { rw [list.sum_cons],
+    exact dvd_add (h _ (mem_cons_self _ _)) (ih (λ x hx, h x (mem_cons_of_mem _ hx))) }
+end
+
+section alternating
+variables [comm_group α]
+
+@[to_additive]
+lemma alternating_prod_append : ∀ l₁ l₂ : list α,
+  alternating_prod (l₁ ++ l₂) = alternating_prod l₁ * alternating_prod l₂ ^ (-1 : ℤ) ^ length l₁
+| [] l₂ := by simp
+| (a :: l₁) l₂ := by simp_rw [cons_append, alternating_prod_cons, alternating_prod_append,
+  length_cons, pow_succ, neg_mul, one_mul, zpow_neg, ←div_eq_mul_inv, div_div]
+
+@[to_additive]
+lemma alternating_prod_reverse :
+  ∀ l : list α, alternating_prod (reverse l) = alternating_prod l ^ (-1 : ℤ) ^ (length l + 1)
+| [] := by simp only [alternating_prod_nil, one_zpow, reverse_nil]
+| (a :: l) :=
+begin
+  simp_rw [reverse_cons, alternating_prod_append, alternating_prod_reverse,
+    alternating_prod_singleton, alternating_prod_cons, length_reverse, length, pow_succ, neg_mul,
+    one_mul, zpow_neg, inv_inv],
+  rw [mul_comm, ←div_eq_mul_inv, div_zpow],
+end
+
+end alternating
+
+lemma sum_map_mul_left [non_unital_non_assoc_semiring R] (L : list ι) (f : ι → R) (r : R) :
+  (L.map (λ b, r * f b)).sum = r * (L.map f).sum :=
+sum_map_hom L f $ add_monoid_hom.mul_left r
+
+lemma sum_map_mul_right [non_unital_non_assoc_semiring R] (L : list ι) (f : ι → R) (r : R) :
+  (L.map (λ b, f b * r)).sum = (L.map f).sum * r :=
+sum_map_hom L f $ add_monoid_hom.mul_right r
+
+end list
+
+namespace mul_opposite
+
+open list
+variables [monoid M]
+
+lemma op_list_prod : ∀ (l : list M), op (l.prod) = (l.map op).reverse.prod
+| [] := rfl
+| (x :: xs) := by rw [list.prod_cons, list.map_cons, list.reverse_cons', list.prod_concat, op_mul,
+                      op_list_prod]
+
+lemma _root_.mul_opposite.unop_list_prod (l : list Mᵐᵒᵖ) :
+  (l.prod).unop = (l.map unop).reverse.prod :=
+by rw [← op_inj, op_unop, mul_opposite.op_list_prod, map_reverse, map_map, reverse_reverse,
+  op_comp_unop, map_id]
+
+end mul_opposite
+
+section monoid_hom
+
+variables [monoid M] [monoid N]
+
+/-- A morphism into the opposite monoid acts on the product by acting on the reversed elements. -/
+lemma unop_map_list_prod {F : Type*} [monoid_hom_class F M Nᵐᵒᵖ] (f : F) (l : list M) :
+  (f l.prod).unop = (l.map (mul_opposite.unop ∘ f)).reverse.prod :=
+by rw [map_list_prod f l, mul_opposite.unop_list_prod, list.map_map]
+
+namespace monoid_hom
+
+/-- A morphism into the opposite monoid acts on the product by acting on the reversed elements.
+
+Deprecated, use `_root_.unop_map_list_prod` instead. -/
+protected lemma unop_map_list_prod (f : M →* Nᵐᵒᵖ) (l : list M) :
+  (f l.prod).unop = (l.map (mul_opposite.unop ∘ f)).reverse.prod :=
+unop_map_list_prod f l
+
+end monoid_hom
+end monoid_hom
diff --git a/src/data/list/count.lean b/src/data/list/count.lean
index 39a5f34592339..1f77bc6d461d4 100644
--- a/src/data/list/count.lean
+++ b/src/data/list/count.lean
@@ -3,7 +3,7 @@ Copyright (c) 2014 Parikshit Khanna. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
 -/
-import data.list.big_operators
+import data.list.big_operators.basic
 
 /-!
 # Counting in lists
diff --git a/src/data/list/join.lean b/src/data/list/join.lean
index b23683f3ee382..590b5102b8cda 100644
--- a/src/data/list/join.lean
+++ b/src/data/list/join.lean
@@ -3,7 +3,7 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Floris van Doorn, Mario Carneiro, Martin Dvorak
 -/
-import data.list.big_operators
+import data.list.big_operators.basic
 
 /-!
 # Join of a list of lists
diff --git a/src/data/list/prime.lean b/src/data/list/prime.lean
index 9fa1305b4c410..cd1c3e6558c8d 100644
--- a/src/data/list/prime.lean
+++ b/src/data/list/prime.lean
@@ -5,7 +5,7 @@ Authors: Johannes Hölzl, Jens Wagemaker, Anne Baanen
 -/
 
 import algebra.associated
-import data.list.big_operators
+import data.list.big_operators.basic
 import data.list.perm
 
 /-!
diff --git a/src/data/list/prod_sigma.lean b/src/data/list/prod_sigma.lean
index db8d50049aacb..c720d8312cb34 100644
--- a/src/data/list/prod_sigma.lean
+++ b/src/data/list/prod_sigma.lean
@@ -3,7 +3,7 @@ Copyright (c) 2015 Leonardo de Moura. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
-import data.list.big_operators
+import data.list.big_operators.basic
 
 /-!
 # Lists in product and sigma types
diff --git a/src/data/list/zip.lean b/src/data/list/zip.lean
index 3a8da95981ad3..0c22cd095866a 100644
--- a/src/data/list/zip.lean
+++ b/src/data/list/zip.lean
@@ -3,7 +3,7 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Kenny Lau
 -/
-import data.list.big_operators
+import data.list.big_operators.basic
 import algebra.order.monoid.min_max
 
 /-!

From fd67f9599d283ea35ab17640a8c5b4112b262c1e Mon Sep 17 00:00:00 2001
From: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Wed, 23 Nov 2022 20:23:32 +0100
Subject: [PATCH 2/7] data.list.zip

---
 src/data/list/zip.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/data/list/zip.lean b/src/data/list/zip.lean
index 0c22cd095866a..1ff6b66c0f097 100644
--- a/src/data/list/zip.lean
+++ b/src/data/list/zip.lean
@@ -396,8 +396,8 @@ variables [comm_monoid α]
 @[to_additive]
 lemma prod_mul_prod_eq_prod_zip_with_mul_prod_drop : ∀ (L L' : list α), L.prod * L'.prod =
   (zip_with (*) L L').prod * (L.drop L'.length).prod * (L'.drop L.length).prod
-| [] ys := by simp [@zero_le' ℕ]
-| xs [] := by simp [@zero_le' ℕ]
+| [] ys := by simp [nat.zero_le]
+| xs [] := by simp [nat.zero_le]
 | (x :: xs) (y :: ys) := begin
   simp only [drop, length, zip_with_cons_cons, prod_cons],
   rw [mul_assoc x, mul_comm xs.prod, mul_assoc y, mul_comm ys.prod,

From b12502823480567b5b875c46b90f6b57d19e0a34 Mon Sep 17 00:00:00 2001
From: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Wed, 23 Nov 2022 20:30:50 +0100
Subject: [PATCH 3/7] control.fold

---
 src/control/fold.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/control/fold.lean b/src/control/fold.lean
index f00281fcffdeb..ad8ee814af62e 100644
--- a/src/control/fold.lean
+++ b/src/control/fold.lean
@@ -3,8 +3,8 @@ Copyright (c) 2018 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Sean Leather
 -/
+import algebra.group.opposite
 import algebra.free_monoid.basic
-import algebra.opposites
 import control.traversable.instances
 import control.traversable.lemmas
 import category_theory.endomorphism

From 9172e99cfe20eddf7e8fb649ff1477beb6f3bc7a Mon Sep 17 00:00:00 2001
From: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Wed, 23 Nov 2022 22:00:50 +0100
Subject: [PATCH 4/7] move lemma back

---
 src/data/list/big_operators/basic.lean  | 10 ++++++++++
 src/data/list/big_operators/lemmas.lean |  6 ------
 2 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/src/data/list/big_operators/basic.lean b/src/data/list/big_operators/basic.lean
index 5fc96d9847ebb..d4cc396063a60 100644
--- a/src/data/list/big_operators/basic.lean
+++ b/src/data/list/big_operators/basic.lean
@@ -428,6 +428,16 @@ lemma all_one_of_le_one_le_of_prod_eq_one [ordered_comm_monoid M]
   x = 1 :=
 le_antisymm (hl₂ ▸ single_le_prod hl₁ _ hx) (hl₁ x hx)
 
+/-- Slightly more general version of `list.prod_eq_one_iff` for a non-ordered `monoid` -/
+@[to_additive "Slightly more general version of `list.sum_eq_zero_iff`
+  for a non-ordered `add_monoid`"]
+lemma prod_eq_one [monoid M] {l : list M} (hl : ∀ (x ∈ l), x = (1 : M)) : l.prod = 1 :=
+begin
+  induction l with i l hil,
+  { refl },
+  rw [list.prod_cons, hil (λ x hx, hl _ (mem_cons_of_mem i hx)), hl _ (mem_cons_self i l), one_mul]
+end
+
 -- TODO: develop theory of tropical rings
 lemma sum_le_foldr_max [add_monoid M] [add_monoid N] [linear_order N] (f : M → N)
   (h0 : f 0 ≤ 0) (hadd : ∀ x y, f (x + y) ≤ max (f x) (f y)) (l : list M) :
diff --git a/src/data/list/big_operators/lemmas.lean b/src/data/list/big_operators/lemmas.lean
index 308b2cbb4f043..a161e575e7216 100644
--- a/src/data/list/big_operators/lemmas.lean
+++ b/src/data/list/big_operators/lemmas.lean
@@ -54,12 +54,6 @@ lemma pow_card_le_prod [monoid M] [preorder M]
 ⟨all_one_of_le_one_le_of_prod_eq_one (λ _ _, one_le _),
   λ h, by rw [eq_repeat.2 ⟨rfl, h⟩, prod_repeat, one_pow]⟩
 
-/-- Slightly more general version of `list.prod_eq_one_iff` for a non-ordered `monoid` -/
-@[to_additive "Slightly more general version of `list.sum_eq_zero_iff`
-  for a non-ordered `add_monoid`"]
-lemma prod_eq_one [monoid M] {l : list M} (hl : ∀ (x ∈ l), x = (1 : M)) : l.prod = 1 :=
-trans (prod_eq_pow_card l 1 hl) (one_pow l.length)
-
 @[to_additive]
 lemma exists_mem_ne_one_of_prod_ne_one [monoid M] {l : list M} (h : l.prod ≠ 1) :
   ∃ (x ∈ l), x ≠ (1 : M) :=

From aed9e52b5cefe44e8f29da65925525d591ab038d Mon Sep 17 00:00:00 2001
From: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Wed, 23 Nov 2022 22:02:16 +0100
Subject: [PATCH 5/7] move another lemma

---
 src/data/list/big_operators/basic.lean  | 5 +++++
 src/data/list/big_operators/lemmas.lean | 5 -----
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/data/list/big_operators/basic.lean b/src/data/list/big_operators/basic.lean
index d4cc396063a60..ac866d2ce39f3 100644
--- a/src/data/list/big_operators/basic.lean
+++ b/src/data/list/big_operators/basic.lean
@@ -438,6 +438,11 @@ begin
   rw [list.prod_cons, hil (λ x hx, hl _ (mem_cons_of_mem i hx)), hl _ (mem_cons_self i l), one_mul]
 end
 
+@[to_additive]
+lemma exists_mem_ne_one_of_prod_ne_one [monoid M] {l : list M} (h : l.prod ≠ 1) :
+  ∃ (x ∈ l), x ≠ (1 : M) :=
+by simpa only [not_forall] using mt prod_eq_one h
+
 -- TODO: develop theory of tropical rings
 lemma sum_le_foldr_max [add_monoid M] [add_monoid N] [linear_order N] (f : M → N)
   (h0 : f 0 ≤ 0) (hadd : ∀ x y, f (x + y) ≤ max (f x) (f y)) (l : list M) :
diff --git a/src/data/list/big_operators/lemmas.lean b/src/data/list/big_operators/lemmas.lean
index a161e575e7216..e42d4982a4244 100644
--- a/src/data/list/big_operators/lemmas.lean
+++ b/src/data/list/big_operators/lemmas.lean
@@ -54,11 +54,6 @@ lemma pow_card_le_prod [monoid M] [preorder M]
 ⟨all_one_of_le_one_le_of_prod_eq_one (λ _ _, one_le _),
   λ h, by rw [eq_repeat.2 ⟨rfl, h⟩, prod_repeat, one_pow]⟩
 
-@[to_additive]
-lemma exists_mem_ne_one_of_prod_ne_one [monoid M] {l : list M} (h : l.prod ≠ 1) :
-  ∃ (x ∈ l), x ≠ (1 : M) :=
-by simpa only [not_forall] using mt prod_eq_one h
-
 /-- If a product of integers is `-1`, then at least one factor must be `-1`. -/
 lemma neg_one_mem_of_prod_eq_neg_one {l : list ℤ} (h : l.prod = -1) : (-1 : ℤ) ∈ l :=
 begin

From 645df31c2bddf1a43b88fcba75422ec0e2438278 Mon Sep 17 00:00:00 2001
From: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Wed, 23 Nov 2022 22:04:49 +0100
Subject: [PATCH 6/7] data.multiset.basic

---
 src/data/multiset/basic.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/data/multiset/basic.lean b/src/data/multiset/basic.lean
index 20c91d032a450..48c7804f68a1b 100644
--- a/src/data/multiset/basic.lean
+++ b/src/data/multiset/basic.lean
@@ -3,6 +3,7 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
+import data.list.big_operators.lemmas
 import data.list.lemmas
 import data.list.perm
 

From 3fdd6cb2895ba8dd40ee49f9e3dc4fd29daee49c Mon Sep 17 00:00:00 2001
From: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Wed, 23 Nov 2022 22:08:22 +0100
Subject: [PATCH 7/7] algebra.big_operators.multiset

---
 src/algebra/big_operators/multiset.lean | 2 +-
 src/data/multiset/basic.lean            | 1 -
 2 files changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/algebra/big_operators/multiset.lean b/src/algebra/big_operators/multiset.lean
index 8aadedfeb1d41..d5016bdf975b0 100644
--- a/src/algebra/big_operators/multiset.lean
+++ b/src/algebra/big_operators/multiset.lean
@@ -3,7 +3,7 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import data.list.big_operators.basic
+import data.list.big_operators.lemmas
 import data.multiset.basic
 
 /-!
diff --git a/src/data/multiset/basic.lean b/src/data/multiset/basic.lean
index 48c7804f68a1b..20c91d032a450 100644
--- a/src/data/multiset/basic.lean
+++ b/src/data/multiset/basic.lean
@@ -3,7 +3,6 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import data.list.big_operators.lemmas
 import data.list.lemmas
 import data.list.perm