chore(Data/List): Do not depend on algebra (#11845)

Remove dependencies on algebra in the `Data.List` folder except for:
* `Data.List.EditDistance`: Actually relies on algebra. Maybe should be moved?
* `Data.List.Card`: Completely unused and redundant.
* `Data.List.Cycle`: Relies on `Fintype`, which shouldn't rely on algebra but it's hard to fix right now. Maybe should be moved?
* `Data.List.Func`: Completely unused and redundant.
* `Data.List.Lex`: That's order theory. Could be moved.
* `Data.List.Prime`. That's algebra. Should definitely be moved.
* `Data.List.Sym`: Relies on `Multiset`, which shouldn't rely on algebra but it's hard to fix right now. Maybe should be moved?
* `Data.List.ToFinsupp`: That's algebra. Should definitely be moved.

As a consequence, move the big operators lemmas that were in there to `Algebra.BigOperators.List.Basic`. For the lemmas that were `Nat`-specific and not about auxiliary definitions, keep a version of them in the original file but stated using `Nat.sum`.

Before
![pre_11845](https://github.com/leanprover-community/mathlib4/assets/14090593/5912261a-7c57-4231-a7d4-aed9ed7c8c79)

After
![post_11845](https://github.com/leanprover-community/mathlib4/assets/14090593/c523c187-2f5a-4d65-ba88-ae489855039e)

Author: YaelDillies

Mathlib/Algebra/BigOperators/List/Basic.lean

@@ -7,6 +7,8 @@ import Mathlib.Algebra.Ring.Commute
 import Mathlib.Data.Int.Basic
 import Mathlib.Data.List.Dedup
 import Mathlib.Data.List.ProdSigma
+import Mathlib.Data.List.Join
+import Mathlib.Data.List.Perm
 import Mathlib.Data.List.Range
 import Mathlib.Data.List.Rotate
 import Mathlib.Data.Nat.Basic
@@ -382,10 +384,26 @@ lemma prod_eq_pow_single [DecidableEq M] (a : M) (h : ∀ a', a' ≠ a → a' 
 #align list.prod_eq_pow_single List.prod_eq_pow_single
 #align list.sum_eq_nsmul_single List.sum_eq_nsmul_single
 
+/-- If elements of a list commute with each other, then their product does not
+depend on the order of elements. -/
+@[to_additive "If elements of a list additively commute with each other, then their sum does not
+depend on the order of elements."]
+lemma Perm.prod_eq' (h : l₁ ~ l₂) (hc : l₁.Pairwise Commute) : l₁.prod = l₂.prod := by
+  refine h.foldl_eq' ?_ _
+  apply Pairwise.forall_of_forall
+  · intro x y h z
+    exact (h z).symm
+  · intros; rfl
+  · apply hc.imp
+    intro a b h z
+    rw [mul_assoc z, mul_assoc z, h]
+#align list.perm.prod_eq' List.Perm.prod_eq'
+#align list.perm.sum_eq' List.Perm.sum_eq'
+
 end Monoid
 
 section CommMonoid
-variable [CommMonoid M] {a : M} {l : List M}
+variable [CommMonoid M] {a : M} {l l₁ l₂ : List M}
 
 @[to_additive (attr := simp)]
 lemma prod_erase [DecidableEq M] (ha : a ∈ l) : a * (l.erase a).prod = l.prod :=
@@ -404,6 +422,14 @@ lemma prod_map_erase [DecidableEq α] (f : α → M) {a} :
 #align list.prod_map_erase List.prod_map_erase
 #align list.sum_map_erase List.sum_map_erase
 
+@[to_additive] lemma Perm.prod_eq (h : Perm l₁ l₂) : prod l₁ = prod l₂ := h.fold_op_eq
+#align list.perm.prod_eq List.Perm.prod_eq
+#align list.perm.sum_eq List.Perm.sum_eq
+
+@[to_additive] lemma prod_reverse (l : List M) : prod l.reverse = prod l := (reverse_perm l).prod_eq
+#align list.prod_reverse List.prod_reverse
+#align list.sum_reverse List.sum_reverse
+
 @[to_additive]
 lemma prod_mul_prod_eq_prod_zipWith_mul_prod_drop :
     ∀ l l' : List M,
@@ -707,4 +733,49 @@ lemma ranges_join (l : List ℕ) : l.ranges.join = range l.sum := by simp [range
 lemma mem_mem_ranges_iff_lt_sum (l : List ℕ) {n : ℕ} :
     (∃ s ∈ l.ranges, n ∈ s) ↔ n < l.sum := by simp [mem_mem_ranges_iff_lt_natSum]
 
+@[simp]
+theorem length_join (L : List (List α)) : length (join L) = sum (map length L) := by
+  induction L <;> [rfl; simp only [*, join, map, sum_cons, length_append]]
+#align list.length_join List.length_join
+
+lemma countP_join (p : α → Bool) : ∀ L : List (List α), countP p L.join = (L.map (countP p)).sum
+  | [] => rfl
+  | a :: l => by rw [join, countP_append, map_cons, sum_cons, countP_join _ l]
+#align list.countp_join List.countP_join
+
+lemma count_join [BEq α] (L : List (List α)) (a : α) : L.join.count a = (L.map (count a)).sum :=
+  countP_join _ _
+#align list.count_join List.count_join
+
+@[simp]
+theorem length_bind (l : List α) (f : α → List β) :
+    length (List.bind l f) = sum (map (length ∘ f) l) := by rw [List.bind, length_join, map_map]
+#align list.length_bind List.length_bind
+
+lemma countP_bind (p : β → Bool) (l : List α) (f : α → List β) :
+    countP p (l.bind f) = sum (map (countP p ∘ f) l) := by rw [List.bind, countP_join, map_map]
+
+lemma count_bind [BEq β] (l : List α) (f : α → List β) (x : β) :
+    count x (l.bind f) = sum (map (count x ∘ f) l) := countP_bind _ _ _
+#align list.count_bind List.count_bind
+
+/-- In a join, taking the first elements up to an index which is the sum of the lengths of the
+first `i` sublists, is the same as taking the join of the first `i` sublists. -/
+lemma take_sum_join (L : List (List α)) (i : ℕ) :
+    L.join.take ((L.map length).take i).sum = (L.take i).join := by simpa using take_sum_join' _ _
+#align list.take_sum_join List.take_sum_join
+
+/-- In a join, dropping all the elements up to an index which is the sum of the lengths of the
+first `i` sublists, is the same as taking the join after dropping the first `i` sublists. -/
+lemma drop_sum_join (L : List (List α)) (i : ℕ) :
+    L.join.drop ((L.map length).take i).sum = (L.drop i).join := by simpa using drop_sum_join' _ _
+#align list.drop_sum_join List.drop_sum_join
+
+/-- In a join of sublists, taking the slice between the indices `A` and `B - 1` gives back the
+original sublist of index `i` if `A` is the sum of the lengths of sublists of index `< i`, and
+`B` is the sum of the lengths of sublists of index `≤ i`. -/
+lemma drop_take_succ_join_eq_get (L : List (List α)) (i : Fin L.length) :
+    (L.join.take ((L.map length).take (i + 1)).sum).drop ((L.map length).take i).sum = get L i := by
+  simpa using drop_take_succ_join_eq_get' _ _
+
 end List

Mathlib/Data/List/DropRight.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yakov Pechersky
 -/
 import Mathlib.Data.List.Infix
-import Mathlib.Data.Nat.Order.Basic
 
 #align_import data.list.rdrop from "leanprover-community/mathlib"@"26f081a2fb920140ed5bc5cc5344e84bcc7cb2b2"
 /-!
@@ -32,6 +31,8 @@ another function that takes a `L : ℕ` and use `L - n`. Under a proof condition
 
 -/
 
+-- Make sure we don't import algebra
+assert_not_exists Monoid
 
 variable {α : Type*} (p : α → Bool) (l : List α) (n : ℕ)
 

Mathlib/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 Mathlib.Algebra.BigOperators.List.Basic
+import Mathlib.Data.List.Basic
 
 #align_import data.list.join from "leanprover-community/mathlib"@"18a5306c091183ac90884daa9373fa3b178e8607"
 
@@ -14,6 +14,8 @@ This file proves basic properties of `List.join`, which concatenates a list of l
 in `Init.Data.List.Basic`.
 -/
 
+-- Make sure we don't import algebra
+assert_not_exists Monoid
 
 variable {α β : Type*}
 
@@ -64,31 +66,31 @@ theorem join_join (l : List (List (List α))) : l.join.join = (l.map join).join
   induction l <;> simp [*]
 #align list.join_join List.join_join
 
-@[simp]
-theorem length_join (L : List (List α)) : length (join L) = sum (map length L) := by
-  induction L <;> [rfl; simp only [*, join, map, sum_cons, length_append]]
-#align list.length_join List.length_join
+/-- See `List.length_join` for the corresponding statement using `List.sum`. -/
+lemma length_join' (L : List (List α)) : length (join L) = Nat.sum (map length L) := by
+  induction L <;> [rfl; simp only [*, join, map, Nat.sum_cons, length_append]]
 
-lemma countP_join (p : α → Bool) : ∀ L : List (List α), countP p L.join = (L.map (countP p)).sum
+/-- See `List.countP_join` for the corresponding statement using `List.sum`. -/
+lemma countP_join' (p : α → Bool) :
+    ∀ L : List (List α), countP p L.join = Nat.sum (L.map (countP p))
   | [] => rfl
-  | a :: l => by rw [join, countP_append, map_cons, sum_cons, countP_join _ l]
-#align list.countp_join List.countP_join
+  | a :: l => by rw [join, countP_append, map_cons, Nat.sum_cons, countP_join' _ l]
 
-lemma count_join [BEq α] (L : List (List α)) (a : α) : L.join.count a = (L.map (count a)).sum :=
-  countP_join _ _
-#align list.count_join List.count_join
+/-- See `List.count_join` for the corresponding statement using `List.sum`. -/
+lemma count_join' [BEq α] (L : List (List α)) (a : α) :
+    L.join.count a = Nat.sum (L.map (count a)) := countP_join' _ _
 
-@[simp]
-theorem length_bind (l : List α) (f : α → List β) :
-    length (List.bind l f) = sum (map (length ∘ f) l) := by rw [List.bind, length_join, map_map]
-#align list.length_bind List.length_bind
+/-- See `List.length_bind` for the corresponding statement using `List.sum`. -/
+lemma length_bind' (l : List α) (f : α → List β) :
+    length (l.bind f) = Nat.sum (map (length ∘ f) l) := by rw [List.bind, length_join', map_map]
 
-lemma countP_bind (p : β → Bool) (l : List α) (f : α → List β) :
-    countP p (l.bind f) = sum (map (countP p ∘ f) l) := by rw [List.bind, countP_join, map_map]
+/-- See `List.countP_bind` for the corresponding statement using `List.sum`. -/
+lemma countP_bind' (p : β → Bool) (l : List α) (f : α → List β) :
+    countP p (l.bind f) = Nat.sum (map (countP p ∘ f) l) := by rw [List.bind, countP_join', map_map]
 
-lemma count_bind [BEq β] (l : List α) (f : α → List β) (x : β) :
-    count x (l.bind f) = sum (map (count x ∘ f) l) := countP_bind _ _ _
-#align list.count_bind List.count_bind
+/-- See `List.count_bind` for the corresponding statement using `List.sum`. -/
+lemma count_bind' [BEq β] (l : List α) (f : α → List β) (x : β) :
+    count x (l.bind f) = Nat.sum (map (count x ∘ f) l) := countP_bind' _ _ _
 
 @[simp]
 theorem bind_eq_nil {l : List α} {f : α → List β} : List.bind l f = [] ↔ ∀ x ∈ l, f x = [] :=
@@ -97,22 +99,24 @@ theorem bind_eq_nil {l : List α} {f : α → List β} : List.bind l f = [] ↔
 #align list.bind_eq_nil List.bind_eq_nil
 
 /-- In a join, taking the first elements up to an index which is the sum of the lengths of the
-first `i` sublists, is the same as taking the join of the first `i` sublists. -/
-theorem take_sum_join (L : List (List α)) (i : ℕ) :
-    L.join.take ((L.map length).take i).sum = (L.take i).join := by
+first `i` sublists, is the same as taking the join of the first `i` sublists.
+
+See `List.take_sum_join` for the corresponding statement using `List.sum`. -/
+theorem take_sum_join' (L : List (List α)) (i : ℕ) :
+    L.join.take (Nat.sum ((L.map length).take i)) = (L.take i).join := by
   induction L generalizing i
   · simp
   · cases i <;> simp [take_append, *]
-#align list.take_sum_join List.take_sum_join
 
 /-- In a join, dropping all the elements up to an index which is the sum of the lengths of the
-first `i` sublists, is the same as taking the join after dropping the first `i` sublists. -/
-theorem drop_sum_join (L : List (List α)) (i : ℕ) :
-    L.join.drop ((L.map length).take i).sum = (L.drop i).join := by
+first `i` sublists, is the same as taking the join after dropping the first `i` sublists.
+
+See `List.drop_sum_join` for the corresponding statement using `List.sum`. -/
+theorem drop_sum_join' (L : List (List α)) (i : ℕ) :
+    L.join.drop (Nat.sum ((L.map length).take i)) = (L.drop i).join := by
   induction L generalizing i
   · simp
   · cases i <;> simp [drop_append, *]
-#align list.drop_sum_join List.drop_sum_join
 
 /-- Taking only the first `i+1` elements in a list, and then dropping the first `i` ones, one is
 left with a list of length `1` made of the `i`-th element of the original list. -/
@@ -145,36 +149,19 @@ theorem drop_take_succ_eq_cons_nthLe (L : List α) {i : ℕ} (hi : i < L.length)
 
 /-- In a join of sublists, taking the slice between the indices `A` and `B - 1` gives back the
 original sublist of index `i` if `A` is the sum of the lengths of sublists of index `< i`, and
-`B` is the sum of the lengths of sublists of index `≤ i`. -/
-theorem drop_take_succ_join_eq_get (L : List (List α)) (i : Fin L.length) :
-    (L.join.take ((L.map length).take (i + 1)).sum).drop ((L.map length).take i).sum =
+`B` is the sum of the lengths of sublists of index `≤ i`.
+
+See `List.drop_take_succ_join_eq_get` for the corresponding statement using `List.sum`. -/
+theorem drop_take_succ_join_eq_get' (L : List (List α)) (i : Fin L.length) :
+    (L.join.take (Nat.sum ((L.map length).take (i + 1)))).drop (Nat.sum ((L.map length).take i)) =
       get L i := by
   have : (L.map length).take i = ((L.take (i + 1)).map length).take i := by
-    simp [map_take, take_take]
-  simp only [this, length_map, take_sum_join, drop_sum_join, drop_take_succ_eq_cons_get,
+    simp [map_take, take_take, Nat.min_eq_left]
+  simp only [this, length_map, take_sum_join', drop_sum_join', drop_take_succ_eq_cons_get,
     join, append_nil]
 
-set_option linter.deprecated false in
-/-- In a join of sublists, taking the slice between the indices `A` and `B - 1` gives back the
-original sublist of index `i` if `A` is the sum of the lengths of sublists of index `< i`, and
-`B` is the sum of the lengths of sublists of index `≤ i`. -/
-@[deprecated drop_take_succ_join_eq_get]
-theorem drop_take_succ_join_eq_nthLe (L : List (List α)) {i : ℕ} (hi : i < L.length) :
-    (L.join.take ((L.map length).take (i + 1)).sum).drop ((L.map length).take i).sum =
-      nthLe L i hi := by
-  have : (L.map length).take i = ((L.take (i + 1)).map length).take i := by
-    simp [map_take, take_take]
-  simp [take_sum_join, this, drop_sum_join, drop_take_succ_eq_cons_nthLe _ hi]
-#align list.drop_take_succ_join_eq_nth_le List.drop_take_succ_join_eq_nthLe
-
-/-- Auxiliary lemma to control elements in a join. -/
-@[deprecated]
-theorem sum_take_map_length_lt1 (L : List (List α)) {i j : ℕ} (hi : i < L.length)
-    (hj : j < (L.get ⟨i, hi⟩).length) :
-    ((L.map length).take i).sum + j < ((L.map length).take (i + 1)).sum := by
-  simp [hi, sum_take_succ, hj]
-#align list.sum_take_map_length_lt1 List.sum_take_map_length_lt1
-
+#noalign list.drop_take_succ_join_eq_nth_le
+#noalign list.sum_take_map_length_lt1
 #noalign list.sum_take_map_length_lt2
 #noalign list.nth_le_join
 
@@ -188,7 +175,7 @@ theorem eq_iff_join_eq (L L' : List (List α)) :
   · have : length (map length L) = length (map length L') := by rw [length_eq]
     simpa using this
   · intro n h₁ h₂
-    rw [← drop_take_succ_join_eq_get, ← drop_take_succ_join_eq_get, join_eq, length_eq]
+    rw [← drop_take_succ_join_eq_get', ← drop_take_succ_join_eq_get', join_eq, length_eq]
 #align list.eq_iff_join_eq List.eq_iff_join_eq
 
 theorem join_drop_length_sub_one {L : List (List α)} (h : L ≠ []) :

Mathlib/Data/List/Perm.lean

@@ -5,12 +5,10 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 import Mathlib.Data.List.Count
 import Mathlib.Data.List.Dedup
-import Mathlib.Data.List.Permutation
-import Mathlib.Data.List.Pairwise
 import Mathlib.Data.List.InsertNth
 import Mathlib.Data.List.Lattice
+import Mathlib.Data.List.Permutation
 import Mathlib.Data.Nat.Factorial.Basic
-import Mathlib.Data.List.Count
 
 #align_import data.list.perm from "leanprover-community/mathlib"@"65a1391a0106c9204fe45bc73a039f056558cb83"
 
@@ -25,6 +23,8 @@ another.
 The notation `~` is used for permutation equivalence.
 -/
 
+-- Make sure we don't import algebra
+assert_not_exists Monoid
 
 open Nat
 
@@ -292,42 +292,6 @@ theorem Perm.fold_op_eq {l₁ l₂ : List α} {a : α} (h : l₁ ~ l₂) : (l₁
 
 end
 
-section CommMonoid
-
-/-- If elements of a list commute with each other, then their product does not
-depend on the order of elements. -/
-@[to_additive
-      "If elements of a list additively commute with each other, then their sum does not
-      depend on the order of elements."]
-theorem Perm.prod_eq' [M : Monoid α] {l₁ l₂ : List α} (h : l₁ ~ l₂) (hc : l₁.Pairwise Commute) :
-    l₁.prod = l₂.prod := by
-  refine h.foldl_eq' ?_ _
-  apply Pairwise.forall_of_forall
-  · intro x y h z
-    exact (h z).symm
-  · intros; rfl
-  · apply hc.imp
-    intro a b h z
-    rw [mul_assoc z, mul_assoc z, h]
-#align list.perm.prod_eq' List.Perm.prod_eq'
-#align list.perm.sum_eq' List.Perm.sum_eq'
-
-variable [CommMonoid α]
-
-@[to_additive]
-theorem Perm.prod_eq {l₁ l₂ : List α} (h : Perm l₁ l₂) : prod l₁ = prod l₂ :=
-  h.fold_op_eq
-#align list.perm.prod_eq List.Perm.prod_eq
-#align list.perm.sum_eq List.Perm.sum_eq
-
-@[to_additive]
-theorem prod_reverse (l : List α) : prod l.reverse = prod l :=
-  (reverse_perm l).prod_eq
-#align list.prod_reverse List.prod_reverse
-#align list.sum_reverse List.sum_reverse
-
-end CommMonoid
-
 #align list.perm_inv_core List.perm_inv_core
 
 #align list.perm.cons_inv List.Perm.cons_inv
@@ -669,12 +633,12 @@ theorem length_permutationsAux :
   refine' permutationsAux.rec (by simp) _
   intro t ts is IH1 IH2
   have IH2 : length (permutationsAux is nil) + 1 = is.length ! := by simpa using IH2
-  simp? [Nat.factorial, Nat.add_succ, mul_comm] at IH1 says
-    simp only [factorial, add_eq, add_zero, mul_comm] at IH1
+  simp? [Nat.factorial, Nat.add_succ, Nat.mul_comm] at IH1 says
+    simp only [factorial, add_eq, Nat.add_zero, Nat.mul_comm] at IH1
   rw [permutationsAux_cons,
     length_foldr_permutationsAux2' _ _ _ _ _ fun l m => (perm_of_mem_permutations m).length_eq,
-    permutations, length, length, IH2, Nat.succ_add, Nat.factorial_succ, mul_comm (_ + 1),
-    ← Nat.succ_eq_add_one, ← IH1, add_comm (_ * _), add_assoc, Nat.mul_succ, mul_comm]
+    permutations, length, length, IH2, Nat.succ_add, Nat.factorial_succ, Nat.mul_comm (_ + 1),
+    ← Nat.succ_eq_add_one, ← IH1, Nat.add_comm (_ * _), Nat.add_assoc, Nat.mul_succ, Nat.mul_comm]
 #align list.length_permutations_aux List.length_permutationsAux
 
 theorem length_permutations (l : List α) : length (permutations l) = (length l)! :=
@@ -800,7 +764,7 @@ theorem nthLe_permutations'Aux (s : List α) (x : α) (n : ℕ)
     (hn : n < length (permutations'Aux x s)) :
     (permutations'Aux x s).nthLe n hn = s.insertNth n x := by
   induction' s with y s IH generalizing n
-  · simp only [length, zero_add, Nat.lt_one_iff] at hn
+  · simp only [length, Nat.zero_add, Nat.lt_one_iff] at hn
     simp [hn]
   · cases n
     · simp [nthLe]
@@ -817,7 +781,7 @@ theorem count_permutations'Aux_self [DecidableEq α] (l : List α) (x : α) :
       simpa [takeWhile, Nat.succ_inj', DecEq_eq] using IH _
     · rw [takeWhile]
       simp only [mem_map, cons.injEq, Ne.symm hx, false_and, and_false, exists_false,
-        not_false_iff, count_eq_zero_of_not_mem, zero_add, hx, decide_False, length_nil]
+        not_false_iff, count_eq_zero_of_not_mem, Nat.zero_add, hx, decide_False, length_nil]
 #align list.count_permutations'_aux_self List.count_permutations'Aux_self
 
 @[simp]
@@ -883,7 +847,7 @@ theorem nodup_permutations'Aux_iff {s : List α} {x : α} : Nodup (permutations'
       rw [nthLe_insertNth_add_succ]
       convert nthLe_insertNth_add_succ s x k m.succ (by simpa using hn) using 2
       · simp [Nat.add_succ, Nat.succ_add]
-      · simp [add_left_comm, add_comm]
+      · simp [Nat.add_left_comm, Nat.add_comm]
       · simpa [Nat.succ_add] using hn
 #align list.nodup_permutations'_aux_iff List.nodup_permutations'Aux_iff