From ea22ce39fbdc245cd0d10be2a03e3a26d70262b6 Mon Sep 17 00:00:00 2001
From: Alex J Best <alex.j.best@gmail.com>
Date: Fri, 15 Oct 2021 22:57:51 +0000
Subject: [PATCH] chore(data/list): move lemmas from data.list.basic that
 require algebra.group_power to a new file (#9728)

Hopefully ease the dependencies on anyone importing data.list.basic, if your code broke after this change adding `import data.list.prod_monoid` should fix it.

Lemmas moved:
- `list.prod_repeat`
- `list.sum_repeat`
- `list.prod_le_of_forall_le`
- `list.sum_le_of_forall_le`
---
 src/data/list/basic.lean             | 20 -------------
 src/data/list/prod_monoid.lean       | 42 ++++++++++++++++++++++++++++
 src/data/multiset/basic.lean         |  1 +
 test/lint_unused_haves_suffices.lean |  1 +
 4 files changed, 44 insertions(+), 20 deletions(-)
 create mode 100644 src/data/list/prod_monoid.lean

diff --git a/src/data/list/basic.lean b/src/data/list/basic.lean
index 12fb12ccf4cc0..cbba33bff3e1f 100644
--- a/src/data/list/basic.lean
+++ b/src/data/list/basic.lean
@@ -5,7 +5,6 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 -/
 import control.monad.basic
 import data.nat.basic
-import algebra.group_power.basic
 
 /-!
 # Basic properties of lists
@@ -2402,14 +2401,6 @@ theorem prod_cons : (a::l).prod = a * l.prod :=
 calc (a::l).prod = foldl (*) (a * 1) l : by simp only [list.prod, foldl_cons, one_mul, mul_one]
   ... = _ : foldl_assoc
 
-@[simp, priority 500, to_additive]
-theorem prod_repeat (a : α) (n : ℕ) : (list.repeat a n).prod = a ^ n :=
-begin
-  induction n with n ih,
-  { rw pow_zero, refl },
-  { rw [list.repeat_succ, list.prod_cons, ih, pow_succ] }
-end
-
 @[simp, to_additive]
 theorem prod_append : (l₁ ++ l₂).prod = l₁.prod * l₂.prod :=
 calc (l₁ ++ l₂).prod = foldl (*) (foldl (*) 1 l₁ * 1) l₂ : by simp [list.prod]
@@ -2693,17 +2684,6 @@ begin
     exact lt_of_add_lt_add_left (lt_of_le_of_lt h $ add_lt_add_right (lt_of_not_ge h') _) }
 end
 
-@[to_additive]
-lemma prod_le_of_forall_le [ordered_comm_monoid α] (l : list α) (n : α) (h : ∀ (x ∈ l), x ≤ n) :
-  l.prod ≤ n ^ l.length :=
-begin
-  induction l with y l IH,
-  { simp },
-  { specialize IH (λ x hx, h x (mem_cons_of_mem _ hx)),
-    have hy : y ≤ n := h y (mem_cons_self _ _),
-    simpa [pow_succ] using mul_le_mul' hy IH }
-end
-
 -- Several lemmas about sum/head/tail for `list ℕ`.
 -- These are hard to generalize well, as they rely on the fact that `default ℕ = 0`.
 
diff --git a/src/data/list/prod_monoid.lean b/src/data/list/prod_monoid.lean
new file mode 100644
index 0000000000000..02b859511554d
--- /dev/null
+++ b/src/data/list/prod_monoid.lean
@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2021 Alex J. Best. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alex J. Best
+-/
+import data.list.basic
+import algebra.group_power.basic
+
+/-!
+# Products / sums of lists of terms of a monoid
+
+This file provides basic results about `list.prod` (definition in `data.list.defs`) in a monoid.
+It is in a separate file so that `data.list.basic` does not depend on `algebra.group_power.basic`.
+-/
+
+open nat
+
+namespace list
+
+universes u v
+variables {α : Type u}
+
+@[simp, priority 500, to_additive]
+theorem prod_repeat [monoid α] (a : α) (n : ℕ) : (repeat a n).prod = a ^ n :=
+begin
+  induction n with n ih,
+  { rw pow_zero, refl },
+  { rw [list.repeat_succ, list.prod_cons, ih, pow_succ] }
+end
+
+@[to_additive]
+lemma prod_le_of_forall_le [ordered_comm_monoid α] (l : list α) (n : α) (h : ∀ (x ∈ l), x ≤ n) :
+  l.prod ≤ n ^ l.length :=
+begin
+  induction l with y l IH,
+  { simp },
+  { specialize IH (λ x hx, h x (mem_cons_of_mem _ hx)),
+    have hy : y ≤ n := h y (mem_cons_self _ _),
+    simpa [pow_succ] using mul_le_mul' hy IH }
+end
+
+end list
diff --git a/src/data/multiset/basic.lean b/src/data/multiset/basic.lean
index 77081594965a1..46a82fd0099ae 100644
--- a/src/data/multiset/basic.lean
+++ b/src/data/multiset/basic.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import data.list.perm
+import data.list.prod_monoid
 
 /-!
 # Multisets
diff --git a/test/lint_unused_haves_suffices.lean b/test/lint_unused_haves_suffices.lean
index a54ba47bcc575..c42c49b642e83 100644
--- a/test/lint_unused_haves_suffices.lean
+++ b/test/lint_unused_haves_suffices.lean
@@ -1,5 +1,6 @@
 import tactic.lint
 import data.list.basic
+import algebra.group_power.basic
 open tactic
 
 lemma test_a : true :=