diff --git a/Mathlib/Algebra/BigOperators/List/Basic.lean b/Mathlib/Algebra/BigOperators/List/Basic.lean
index a1cd612cea472..217987d88de41 100644
--- a/Mathlib/Algebra/BigOperators/List/Basic.lean
+++ b/Mathlib/Algebra/BigOperators/List/Basic.lean
@@ -9,6 +9,10 @@ import Mathlib.Algebra.Divisibility.Basic
 import Mathlib.Algebra.Ring.Commute
 import Mathlib.Data.Nat.Order.Basic
 import Mathlib.Data.Int.Basic
+import Mathlib.Data.List.Dedup
+import Mathlib.Data.List.ProdSigma
+import Mathlib.Data.List.Range
+import Mathlib.Data.List.Rotate
 
 #align_import data.list.big_operators.basic from "leanprover-community/mathlib"@"6c5f73fd6f6cc83122788a80a27cdd54663609f4"
 
@@ -20,7 +24,7 @@ of elements of a list and `List.alternatingProd`, `List.alternatingSum`, their a
 counterparts. These are defined in [`Algebra.BigOperators.List.Defs`](./Defs).
 -/
 
-variable {ι α M N P M₀ G R : Type*}
+variable {ι α β γ M N P M₀ G R : Type*}
 
 namespace List
 
@@ -288,6 +292,68 @@ theorem _root_.Commute.list_prod_left (l : List M) (y : M) (h : ∀ x ∈ l, Com
 #align commute.list_prod_left Commute.list_prod_left
 #align add_commute.list_sum_left AddCommute.list_sum_left
 
+@[to_additive] lemma prod_range_succ (f : ℕ → M) (n : ℕ) :
+    ((range n.succ).map f).prod = ((range n).map f).prod * f n := by
+  rw [range_succ, map_append, map_singleton, prod_append, prod_cons, prod_nil, mul_one]
+#align list.prod_range_succ List.prod_range_succ
+#align list.sum_range_succ List.sum_range_succ
+
+/-- A variant of `prod_range_succ` which pulls off the first term in the product rather than the
+last. -/
+@[to_additive
+"A variant of `sum_range_succ` which pulls off the first term in the sum rather than the last."]
+lemma prod_range_succ' (f : ℕ → M) (n : ℕ) :
+    ((range n.succ).map f).prod = f 0 * ((range n).map fun i ↦ f i.succ).prod :=
+  Nat.recOn n (show 1 * f 0 = f 0 * 1 by rw [one_mul, mul_one]) fun _ hd => by
+    rw [List.prod_range_succ, hd, mul_assoc, ← List.prod_range_succ]
+#align list.prod_range_succ' List.prod_range_succ'
+#align list.sum_range_succ' List.sum_range_succ'
+
+/-- 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 `AddMonoid`"]
+lemma prod_eq_one (hl : ∀ x ∈ l, x = 1) : l.prod = 1 := by
+  induction' l with i l hil
+  · rfl
+  rw [List.prod_cons, hil fun x hx ↦ hl _ (mem_cons_of_mem i hx), hl _ (mem_cons_self i l), one_mul]
+#align list.prod_eq_one List.prod_eq_one
+#align list.sum_eq_zero List.sum_eq_zero
+
+@[to_additive] lemma exists_mem_ne_one_of_prod_ne_one (h : l.prod ≠ 1) :
+    ∃ x ∈ l, x ≠ (1 : M) := by simpa only [not_forall, exists_prop] using mt prod_eq_one h
+#align list.exists_mem_ne_one_of_prod_ne_one List.exists_mem_ne_one_of_prod_ne_one
+#align list.exists_mem_ne_zero_of_sum_ne_zero List.exists_mem_ne_zero_of_sum_ne_zero
+
+@[to_additive]
+lemma prod_erase_of_comm [DecidableEq M] (ha : a ∈ l) (comm : ∀ x ∈ l, ∀ y ∈ l, x * y = y * x) :
+    a * (l.erase a).prod = l.prod := by
+  induction' l with b l ih; simp only [not_mem_nil] at ha
+  obtain rfl | ⟨ne, h⟩ := Decidable.List.eq_or_ne_mem_of_mem ha
+  simp only [erase_cons_head, prod_cons]
+  rw [List.erase, beq_false_of_ne ne.symm, List.prod_cons, List.prod_cons, ← mul_assoc,
+    comm a ha b (l.mem_cons_self b), mul_assoc,
+    ih h fun x hx y hy ↦ comm _ (List.mem_cons_of_mem b hx) _ (List.mem_cons_of_mem b hy)]
+
+@[to_additive]
+lemma prod_map_eq_pow_single [DecidableEq α] {l : List α} (a : α) (f : α → M)
+    (hf : ∀ a', a' ≠ a → a' ∈ l → f a' = 1) : (l.map f).prod = f a ^ l.count a := by
+  induction' l with a' as h generalizing a
+  · rw [map_nil, prod_nil, count_nil, _root_.pow_zero]
+  · specialize h a fun a' ha' hfa' => hf a' ha' (mem_cons_of_mem _ hfa')
+    rw [List.map_cons, List.prod_cons, count_cons, h]
+    split_ifs with ha'
+    · rw [ha', _root_.pow_succ']
+    · rw [hf a' (Ne.symm ha') (List.mem_cons_self a' as), one_mul, add_zero]
+#align list.prod_map_eq_pow_single List.prod_map_eq_pow_single
+#align list.sum_map_eq_nsmul_single List.sum_map_eq_nsmul_single
+
+@[to_additive]
+lemma prod_eq_pow_single [DecidableEq M] (a : M) (h : ∀ a', a' ≠ a → a' ∈ l → a' = 1) :
+    l.prod = a ^ l.count a :=
+  _root_.trans (by rw [map_id]) (prod_map_eq_pow_single a id h)
+#align list.prod_eq_pow_single List.prod_eq_pow_single
+#align list.sum_eq_nsmul_single List.sum_eq_nsmul_single
+
 @[to_additive sum_le_sum]
 theorem Forall₂.prod_le_prod' [Preorder M] [CovariantClass M M (Function.swap (· * ·)) (· ≤ ·)]
     [CovariantClass M M (· * ·) (· ≤ ·)] {l₁ l₂ : List M} (h : Forall₂ (· ≤ ·) l₁ l₂) :
@@ -402,6 +468,53 @@ theorem one_le_prod_of_one_le [Preorder M] [CovariantClass M M (· * ·) (· ≤
 
 end Monoid
 
+section CommMonoid
+variable [CommMonoid M] {a : M} {l : List M}
+
+@[to_additive (attr := simp)]
+lemma prod_erase [DecidableEq M] (ha : a ∈ l) : a * (l.erase a).prod = l.prod :=
+  prod_erase_of_comm ha fun x _ y _ ↦ mul_comm x y
+#align list.prod_erase List.prod_erase
+#align list.sum_erase List.sum_erase
+
+@[to_additive (attr := simp)]
+lemma prod_map_erase [DecidableEq α] (f : α → M) {a} :
+    ∀ {l : List α}, a ∈ l → f a * ((l.erase a).map f).prod = (l.map f).prod
+  | b :: l, h => by
+    obtain rfl | ⟨ne, h⟩ := Decidable.List.eq_or_ne_mem_of_mem h
+    · simp only [map, erase_cons_head, prod_cons]
+    · simp only [map, erase_cons_tail _ (not_beq_of_ne ne.symm), prod_cons, prod_map_erase _ h,
+        mul_left_comm (f a) (f b)]
+#align list.prod_map_erase List.prod_map_erase
+#align list.sum_map_erase List.sum_map_erase
+
+@[to_additive]
+lemma prod_mul_prod_eq_prod_zipWith_mul_prod_drop :
+    ∀ l l' : List M,
+      l.prod * l'.prod =
+        (zipWith (· * ·) l l').prod * (l.drop l'.length).prod * (l'.drop l.length).prod
+  | [], ys => by simp [Nat.zero_le]
+  | xs, [] => by simp [Nat.zero_le]
+  | x :: xs, y :: ys => by
+    simp only [drop, length, zipWith_cons_cons, prod_cons]
+    conv =>
+      lhs; rw [mul_assoc]; right; rw [mul_comm, mul_assoc]; right
+      rw [mul_comm, prod_mul_prod_eq_prod_zipWith_mul_prod_drop xs ys]
+    simp only [Nat.add_eq, add_zero]
+    ac_rfl
+#align list.prod_mul_prod_eq_prod_zip_with_mul_prod_drop List.prod_mul_prod_eq_prod_zipWith_mul_prod_drop
+#align list.sum_add_sum_eq_sum_zip_with_add_sum_drop List.sum_add_sum_eq_sum_zipWith_add_sum_drop
+
+@[to_additive]
+lemma prod_mul_prod_eq_prod_zipWith_of_length_eq (l l' : List M) (h : l.length = l'.length) :
+    l.prod * l'.prod = (zipWith (· * ·) l l').prod := by
+  apply (prod_mul_prod_eq_prod_zipWith_mul_prod_drop l l').trans
+  rw [← h, drop_length, h, drop_length, prod_nil, mul_one, mul_one]
+#align list.prod_mul_prod_eq_prod_zip_with_of_length_eq List.prod_mul_prod_eq_prod_zipWith_of_length_eq
+#align list.sum_add_sum_eq_sum_zip_with_of_length_eq List.sum_add_sum_eq_sum_zipWith_of_length_eq
+
+end CommMonoid
+
 section MonoidWithZero
 
 variable [MonoidWithZero M₀]
@@ -472,6 +585,16 @@ theorem prod_range_div' (n : ℕ) (f : ℕ → G) :
   · exact (div_self' (f 0)).symm
   · rw [range_succ, map_append, map_singleton, prod_append, prod_singleton, h, div_mul_div_cancel']
 
+lemma prod_rotate_eq_one_of_prod_eq_one :
+    ∀ {l : List G} (_ : l.prod = 1) (n : ℕ), (l.rotate n).prod = 1
+  | [], _, _ => by simp
+  | a :: l, hl, n => by
+    have : n % List.length (a :: l) ≤ List.length (a :: l) := le_of_lt (Nat.mod_lt _ (by simp))
+    rw [← List.take_append_drop (n % List.length (a :: l)) (a :: l)] at hl;
+      rw [← rotate_mod, rotate_eq_drop_append_take this, List.prod_append, mul_eq_one_iff_inv_eq, ←
+        one_mul (List.prod _)⁻¹, ← hl, List.prod_append, mul_assoc, mul_inv_self, mul_one]
+#align list.prod_rotate_eq_one_of_prod_eq_one List.prod_rotate_eq_one_of_prod_eq_one
+
 end Group
 
 section CommGroup
@@ -508,6 +631,16 @@ theorem prod_set' (L : List G) (n : ℕ) (a : G) :
 
 end CommGroup
 
+@[simp]
+theorem sum_zipWith_distrib_left [Semiring γ] (f : α → β → γ) (n : γ) (l : List α) (l' : List β) :
+    (l.zipWith (fun x y => n * f x y) l').sum = n * (l.zipWith f l').sum := by
+  induction' l with hd tl hl generalizing f n l'
+  · simp
+  · cases' l' with hd' tl'
+    · simp
+    · simp [hl, mul_add]
+#align list.sum_zip_with_distrib_left List.sum_zipWith_distrib_left
+
 @[to_additive]
 theorem eq_of_prod_take_eq [LeftCancelMonoid M] {L L' : List M} (h : L.length = L'.length)
     (h' : ∀ i ≤ L.length, (L.take i).prod = (L'.take i).prod) : L = L' := by
@@ -564,23 +697,6 @@ theorem all_one_of_le_one_le_of_prod_eq_one [OrderedCommMonoid M] {l : List M}
 #align list.all_one_of_le_one_le_of_prod_eq_one List.all_one_of_le_one_le_of_prod_eq_one
 #align list.all_zero_of_le_zero_le_of_sum_eq_zero List.all_zero_of_le_zero_le_of_sum_eq_zero
 
-/-- 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 `AddMonoid`"]
-theorem prod_eq_one [Monoid M] {l : List M} (hl : ∀ x ∈ l, x = (1 : M)) : l.prod = 1 := by
-  induction' l with i l hil
-  · rfl
-  rw [List.prod_cons, hil fun x hx => hl _ (mem_cons_of_mem i hx), hl _ (mem_cons_self i l),
-    one_mul]
-#align list.prod_eq_one List.prod_eq_one
-#align list.sum_eq_zero List.sum_eq_zero
-
-@[to_additive]
-theorem 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, exists_prop] using mt prod_eq_one h
-#align list.exists_mem_ne_one_of_prod_ne_one List.exists_mem_ne_one_of_prod_ne_one
-#align list.exists_mem_ne_zero_of_sum_ne_zero List.exists_mem_ne_zero_of_sum_ne_zero
-
 -- TODO: develop theory of tropical rings
 theorem sum_le_foldr_max [AddMonoid M] [AddMonoid N] [LinearOrder N] (f : M → N) (h0 : f 0 ≤ 0)
     (hadd : ∀ x y, f (x + y) ≤ max (f x) (f y)) (l : List M) : f l.sum ≤ (l.map f).foldr max 0 := by
@@ -590,35 +706,6 @@ theorem sum_le_foldr_max [AddMonoid M] [AddMonoid N] [LinearOrder N] (f : M →
   exact (hadd _ _).trans (max_le_max le_rfl IH)
 #align list.sum_le_foldr_max List.sum_le_foldr_max
 
-@[to_additive]
-theorem prod_erase_of_comm [DecidableEq M] [Monoid M] {a} {l : List M} (ha : a ∈ l)
-    (comm : ∀ x ∈ l, ∀ y ∈ l, x * y = y * x) :
-    a * (l.erase a).prod = l.prod := by
-  induction' l with b l ih; simp only [not_mem_nil] at ha
-  obtain rfl | ⟨ne, h⟩ := Decidable.List.eq_or_ne_mem_of_mem ha
-  simp only [erase_cons_head, prod_cons]
-  rw [List.erase, beq_false_of_ne ne.symm, List.prod_cons, List.prod_cons, ← mul_assoc,
-    comm a ha b (l.mem_cons_self b), mul_assoc,
-    ih h fun x hx y hy ↦ comm _ (List.mem_cons_of_mem b hx) _ (List.mem_cons_of_mem b hy)]
-
-@[to_additive (attr := simp)]
-theorem prod_erase [DecidableEq M] [CommMonoid M] {a} {l : List M} (ha : a ∈ l) :
-    a * (l.erase a).prod = l.prod :=
-  prod_erase_of_comm ha fun x _ y _ ↦ mul_comm x y
-#align list.prod_erase List.prod_erase
-#align list.sum_erase List.sum_erase
-
-@[to_additive (attr := simp)]
-theorem prod_map_erase [DecidableEq ι] [CommMonoid M] (f : ι → M) {a} :
-    ∀ {l : List ι}, a ∈ l → f a * ((l.erase a).map f).prod = (l.map f).prod
-  | b :: l, h => by
-    obtain rfl | ⟨ne, h⟩ := Decidable.List.eq_or_ne_mem_of_mem h
-    · simp only [map, erase_cons_head, prod_cons]
-    · simp only [map, erase_cons_tail _ (not_beq_of_ne ne.symm), prod_cons, prod_map_erase _ h,
-        mul_left_comm (f a) (f b)]
-#align list.prod_map_erase List.prod_map_erase
-#align list.sum_map_erase List.sum_map_erase
-
 theorem sum_const_nat (m n : ℕ) : sum (replicate m n) = m * n :=
   sum_replicate m n
 #align list.sum_const_nat List.sum_const_nat
@@ -733,6 +820,38 @@ lemma prod_int_mod (l : List ℤ) (n : ℤ) : l.prod % n = (l.map (· % n)).prod
   induction l <;> simp [Int.mul_emod, *]
 #align list.prod_int_mod List.prod_int_mod
 
+variable [DecidableEq α]
+
+/-- Summing the count of `x` over a list filtered by some `p` is just `countP` applied to `p` -/
+theorem sum_map_count_dedup_filter_eq_countP (p : α → Bool) (l : List α) :
+    ((l.dedup.filter p).map fun x => l.count x).sum = l.countP p := by
+  induction' l with a as h
+  · simp
+  · simp_rw [List.countP_cons, List.count_cons, List.sum_map_add]
+    congr 1
+    · refine' _root_.trans _ h
+      by_cases ha : a ∈ as
+      · simp [dedup_cons_of_mem ha]
+      · simp only [dedup_cons_of_not_mem ha, List.filter]
+        match p a with
+        | true => simp only [List.map_cons, List.sum_cons, List.count_eq_zero.2 ha, zero_add]
+        | false => simp only
+    · by_cases hp : p a
+      · refine' _root_.trans (sum_map_eq_nsmul_single a _ fun _ h _ => by simp [h]) _
+        simp [hp, count_dedup]
+      · refine' _root_.trans (List.sum_eq_zero fun n hn => _) (by simp [hp])
+        obtain ⟨a', ha'⟩ := List.mem_map.1 hn
+        split_ifs at ha' with ha
+        · simp only [ha, mem_filter, mem_dedup, find?, mem_cons, true_or, hp,
+            and_false, false_and] at ha'
+        · exact ha'.2.symm
+#align list.sum_map_count_dedup_filter_eq_countp List.sum_map_count_dedup_filter_eq_countP
+
+theorem sum_map_count_dedup_eq_length (l : List α) :
+    (l.dedup.map fun x => l.count x).sum = l.length := by
+  simpa using sum_map_count_dedup_filter_eq_countP (fun _ => True) l
+#align list.sum_map_count_dedup_eq_length List.sum_map_count_dedup_eq_length
+
 end List
 
 section MonoidHom
@@ -758,3 +877,20 @@ protected theorem map_list_prod (f : M →* N) (l : List M) : f l.prod = (l.map
 end MonoidHom
 
 end MonoidHom
+
+@[simp] lemma Nat.sum_eq_listSum (l : List ℕ) : Nat.sum l = l.sum :=
+  (List.foldl_eq_foldr Nat.add_comm Nat.add_assoc _ _).symm
+
+namespace List
+
+lemma length_sigma {σ : α → Type*} (l₁ : List α) (l₂ : ∀ a, List (σ a)) :
+    length (l₁.sigma l₂) = (l₁.map fun a ↦ length (l₂ a)).sum := by simp [length_sigma']
+#align list.length_sigma List.length_sigma
+
+lemma ranges_join (l : List ℕ) : l.ranges.join = range l.sum := by simp [ranges_join']
+
+/-- Any entry of any member of `l.ranges` is strictly smaller than `l.sum`. -/
+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]
+
+end List
diff --git a/Mathlib/Data/List/Count.lean b/Mathlib/Data/List/Count.lean
index 2b7a573a32cd2..7f6d30c09b8fa 100644
--- a/Mathlib/Data/List/Count.lean
+++ b/Mathlib/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 Mathlib.Algebra.BigOperators.List.Basic
+import Mathlib.Data.List.Basic
 
 #align_import data.list.count from "leanprover-community/mathlib"@"65a1391a0106c9204fe45bc73a039f056558cb83"
 
@@ -15,12 +15,13 @@ elements of a list satisfying a predicate and equal to a given element respectiv
 definitions can be found in `Std.Data.List.Basic`.
 -/
 
-set_option autoImplicit true
-
+assert_not_exists Set.range
+assert_not_exists GroupWithZero
+assert_not_exists Ring
 
 open Nat
 
-variable {l : List α}
+variable {α : Type*} {l : List α}
 
 namespace List
 
@@ -44,11 +45,6 @@ variable (p q : α → Bool)
 
 #align list.countp_append List.countP_append
 
-theorem countP_join : ∀ 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
-
 #align list.countp_pos List.countP_pos
 
 #align list.countp_eq_zero List.countP_eq_zero
@@ -92,7 +88,7 @@ variable [DecidableEq α]
 
 @[deprecated] theorem count_cons' (a b : α) (l : List α) :
     count a (b :: l) = count a l + if a = b then 1 else 0 := by
-  simp only [count, beq_iff_eq, countP_cons, add_right_inj]
+  simp only [count, beq_iff_eq, countP_cons, Nat.add_right_inj]
   simp only [eq_comm]
 #align list.count_cons' List.count_cons'
 
@@ -116,10 +112,6 @@ variable [DecidableEq α]
 
 #align list.count_append List.count_append
 
-theorem count_join (l : List (List α)) (a : α) : l.join.count a = (l.map (count a)).sum :=
-  countP_join _ _
-#align list.count_join List.count_join
-
 #align list.count_concat List.count_concat
 
 #align list.count_pos List.count_pos_iff_mem
@@ -148,10 +140,6 @@ theorem count_join (l : List (List α)) (a : α) : l.join.count a = (l.map (coun
 
 #align list.count_filter List.count_filter
 
-theorem count_bind {α β} [DecidableEq β] (l : List α) (f : α → List β) (x : β) :
-    count x (l.bind f) = sum (map (count x ∘ f) l) := by rw [List.bind, count_join, map_map]
-#align list.count_bind List.count_bind
-
 @[simp]
 lemma count_attach (a : {x // x ∈ l}) : l.attach.count a = l.count ↑a :=
   Eq.trans (countP_congr fun _ _ => by simp [Subtype.ext_iff]) <| countP_attach _ _
@@ -171,26 +159,6 @@ theorem count_map_of_injective {α β} [DecidableEq α] [DecidableEq β] (l : Li
 
 #align list.count_erase_of_ne List.count_erase_of_ne
 
-@[to_additive]
-theorem prod_map_eq_pow_single [Monoid β] (a : α) (f : α → β)
-    (hf : ∀ a', a' ≠ a → a' ∈ l → f a' = 1) : (l.map f).prod = f a ^ l.count a := by
-  induction' l with a' as h generalizing a
-  · rw [map_nil, prod_nil, count_nil, _root_.pow_zero]
-  · specialize h a fun a' ha' hfa' => hf a' ha' (mem_cons_of_mem _ hfa')
-    rw [List.map_cons, List.prod_cons, count_cons, h]
-    split_ifs with ha'
-    · rw [ha', _root_.pow_succ']
-    · rw [hf a' (Ne.symm ha') (List.mem_cons_self a' as), one_mul, add_zero]
-#align list.prod_map_eq_pow_single List.prod_map_eq_pow_single
-#align list.sum_map_eq_nsmul_single List.sum_map_eq_nsmul_single
-
-@[to_additive]
-theorem prod_eq_pow_single [Monoid α] (a : α)
-    (h : ∀ a', a' ≠ a → a' ∈ l → a' = 1) : l.prod = a ^ l.count a :=
-  _root_.trans (by rw [map_id]) (prod_map_eq_pow_single a id h)
-#align list.prod_eq_pow_single List.prod_eq_pow_single
-#align list.sum_eq_nsmul_single List.sum_eq_nsmul_single
-
 end Count
 
 end List
diff --git a/Mathlib/Data/List/Dedup.lean b/Mathlib/Data/List/Dedup.lean
index 396faee1fb8f2..26af9e520f372 100644
--- a/Mathlib/Data/List/Dedup.lean
+++ b/Mathlib/Data/List/Dedup.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Mathlib.Data.List.Nodup
-import Mathlib.Data.List.Count
 
 #align_import data.list.dedup from "leanprover-community/mathlib"@"d9e96a3e3e0894e93e10aff5244f4c96655bac1c"
 
@@ -96,9 +95,10 @@ theorem dedup_eq_cons (l : List α) (a : α) (l' : List α) :
     l.dedup = a :: l' ↔ a ∈ l ∧ a ∉ l' ∧ l.dedup.tail = l' := by
   refine' ⟨fun h => _, fun h => _⟩
   · refine' ⟨mem_dedup.1 (h.symm ▸ mem_cons_self _ _), fun ha => _, by rw [h, tail_cons]⟩
+    have := count_pos_iff_mem.2 ha
     have : count a l.dedup ≤ 1 := nodup_iff_count_le_one.1 (nodup_dedup l) a
-    rw [h, count_cons_self, add_le_iff_nonpos_left] at this
-    exact not_le_of_lt (count_pos_iff_mem.2 ha) this
+    rw [h, count_cons_self] at this
+    omega
   · have := @List.cons_head!_tail α ⟨a⟩ _ (ne_nil_of_mem (mem_dedup.2 h.1))
     have hal : a ∈ l.dedup := mem_dedup.2 h.1
     rw [← this, mem_cons, or_iff_not_imp_right] at hal
@@ -144,34 +144,4 @@ theorem count_dedup (l : List α) (a : α) : l.dedup.count a = if a ∈ l then 1
   simp_rw [count_eq_of_nodup <| nodup_dedup l, mem_dedup]
 #align list.count_dedup List.count_dedup
 
-/-- Summing the count of `x` over a list filtered by some `p` is just `countP` applied to `p` -/
-theorem sum_map_count_dedup_filter_eq_countP (p : α → Bool) (l : List α) :
-    ((l.dedup.filter p).map fun x => l.count x).sum = l.countP p := by
-  induction' l with a as h
-  · simp
-  · simp_rw [List.countP_cons, List.count_cons, List.sum_map_add]
-    congr 1
-    · refine' _root_.trans _ h
-      by_cases ha : a ∈ as
-      · simp [dedup_cons_of_mem ha]
-      · simp only [dedup_cons_of_not_mem ha, List.filter]
-        match p a with
-        | true => simp only [List.map_cons, List.sum_cons, List.count_eq_zero.2 ha, zero_add]
-        | false => simp only
-    · by_cases hp : p a
-      · refine' _root_.trans (sum_map_eq_nsmul_single a _ fun _ h _ => by simp [h]) _
-        simp [hp, count_dedup]
-      · refine' _root_.trans (List.sum_eq_zero fun n hn => _) (by simp [hp])
-        obtain ⟨a', ha'⟩ := List.mem_map.1 hn
-        split_ifs at ha' with ha
-        · simp only [ha, mem_filter, mem_dedup, find?, mem_cons, true_or, hp,
-            and_false, false_and] at ha'
-        · exact ha'.2.symm
-#align list.sum_map_count_dedup_filter_eq_countp List.sum_map_count_dedup_filter_eq_countP
-
-theorem sum_map_count_dedup_eq_length (l : List α) :
-    (l.dedup.map fun x => l.count x).sum = l.length := by
-  simpa using sum_map_count_dedup_filter_eq_countP (fun _ => True) l
-#align list.sum_map_count_dedup_eq_length List.sum_map_count_dedup_eq_length
-
 end List
diff --git a/Mathlib/Data/List/Join.lean b/Mathlib/Data/List/Join.lean
index 0b933771d372b..d5391a5e29dc7 100644
--- a/Mathlib/Data/List/Join.lean
+++ b/Mathlib/Data/List/Join.lean
@@ -69,11 +69,27 @@ theorem length_join (L : List (List α)) : length (join L) = sum (map length L)
   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
+
 @[simp]
 theorem bind_eq_nil {l : List α} {f : α → List β} : List.bind l f = [] ↔ ∀ x ∈ l, f x = [] :=
   join_eq_nil.trans <| by
diff --git a/Mathlib/Data/List/Perm.lean b/Mathlib/Data/List/Perm.lean
index 38d9789a844a5..2e81ee7f752f9 100644
--- a/Mathlib/Data/List/Perm.lean
+++ b/Mathlib/Data/List/Perm.lean
@@ -9,6 +9,7 @@ import Mathlib.Data.List.Pairwise
 import Mathlib.Data.List.InsertNth
 import Mathlib.Data.List.Lattice
 import Mathlib.Data.Nat.Factorial.Basic
+import Mathlib.Data.List.Count
 
 #align_import data.list.perm from "leanprover-community/mathlib"@"65a1391a0106c9204fe45bc73a039f056558cb83"
 
diff --git a/Mathlib/Data/List/ProdSigma.lean b/Mathlib/Data/List/ProdSigma.lean
index c6ca5612baa8f..02ac2c7810995 100644
--- a/Mathlib/Data/List/ProdSigma.lean
+++ b/Mathlib/Data/List/ProdSigma.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 Mathlib.Algebra.BigOperators.List.Basic
+import Mathlib.Data.List.Basic
 import Mathlib.Data.Sigma.Basic
 
 #align_import data.list.prod_sigma from "leanprover-community/mathlib"@"dd71334db81d0bd444af1ee339a29298bef40734"
@@ -51,9 +51,9 @@ theorem mem_product {l₁ : List α} {l₂ : List β} {a : α} {b : β} :
 theorem length_product (l₁ : List α) (l₂ : List β) :
     length (l₁ ×ˢ l₂) = length l₁ * length l₂ := by
   induction' l₁ with x l₁ IH
-  · exact (zero_mul _).symm
-  · simp only [length, product_cons, length_append, IH, right_distrib, one_mul, length_map,
-      add_comm]
+  · exact (Nat.zero_mul _).symm
+  · simp only [length, product_cons, length_append, IH, Nat.add_mul, Nat.one_mul, length_map,
+      Nat.add_comm]
 #align list.length_product List.length_product
 
 /-! ### sigma -/
@@ -85,11 +85,11 @@ theorem mem_sigma {l₁ : List α} {l₂ : ∀ a, List (σ a)} {a : α} {b : σ
     exists_eq_left, heq_iff_eq, exists_eq_right]
 #align list.mem_sigma List.mem_sigma
 
-theorem length_sigma (l₁ : List α) (l₂ : ∀ a, List (σ a)) :
-    length (l₁.sigma l₂) = (l₁.map fun a => length (l₂ a)).sum := by
+/-- See `List.length_sigma` for the corresponding statement using `List.sum`. -/
+theorem length_sigma' (l₁ : List α) (l₂ : ∀ a, List (σ a)) :
+    length (l₁.sigma l₂) = Nat.sum (l₁.map fun a ↦ length (l₂ a)) := by
   induction' l₁ with x l₁ IH
   · rfl
-  · simp only [map, sigma_cons, length_append, length_map, IH, sum_cons]
-#align list.length_sigma List.length_sigma
+  · simp only [map, sigma_cons, length_append, length_map, IH, Nat.sum_cons]
 
 end List
diff --git a/Mathlib/Data/List/Range.lean b/Mathlib/Data/List/Range.lean
index 3d01edbe5762f..879eb3cd0fe58 100644
--- a/Mathlib/Data/List/Range.lean
+++ b/Mathlib/Data/List/Range.lean
@@ -165,24 +165,6 @@ theorem pairwise_lt_finRange (n : ℕ) : Pairwise (· < ·) (finRange n) :=
 theorem pairwise_le_finRange (n : ℕ) : Pairwise (· ≤ ·) (finRange n) :=
   (List.pairwise_le_range n).pmap (by simp) (by simp)
 
-@[to_additive]
-theorem prod_range_succ {α : Type u} [Monoid α] (f : ℕ → α) (n : ℕ) :
-    ((range n.succ).map f).prod = ((range n).map f).prod * f n := by
-  rw [range_succ, map_append, map_singleton, prod_append, prod_cons, prod_nil, mul_one]
-#align list.prod_range_succ List.prod_range_succ
-#align list.sum_range_succ List.sum_range_succ
-
-/-- A variant of `prod_range_succ` which pulls off the first
-  term in the product rather than the last.-/
-@[to_additive
-  "A variant of `sum_range_succ` which pulls off the first term in the sum rather than the last."]
-theorem prod_range_succ' {α : Type u} [Monoid α] (f : ℕ → α) (n : ℕ) :
-    ((range n.succ).map f).prod = f 0 * ((range n).map fun i => f (succ i)).prod :=
-  Nat.recOn n (show 1 * f 0 = f 0 * 1 by rw [one_mul, mul_one]) fun _ hd => by
-    rw [List.prod_range_succ, hd, mul_assoc, ← List.prod_range_succ]
-#align list.prod_range_succ' List.prod_range_succ'
-#align list.sum_range_succ' List.sum_range_succ'
-
 #align list.enum_from_map_fst List.enumFrom_map_fst
 #align list.enum_map_fst List.enum_map_fst
 
@@ -259,7 +241,7 @@ theorem ranges_disjoint (l : List ℕ) :
       rw [mem_map]
       rintro ⟨v, _, rfl⟩
       rw [mem_range] at hu
-      exact lt_iff_not_le.mp hu le_self_add
+      omega
     · rw [pairwise_map]
       apply Pairwise.imp _ hl
       intro u v
@@ -279,26 +261,20 @@ theorem ranges_length (l : List ℕ) :
     intro s _
     simp only [Function.comp_apply, length_map]
 
-theorem ranges_join (l : List ℕ) :
-    l.ranges.join = range l.sum := by
-  induction l with
-  | nil => exact rfl
-  | cons a l hl =>
-    simp only [sum_cons, join]
-    rw [← map_join, hl]
-    rw [range_add]
+/-- See `List.ranges_join` for the version about `List.sum`. -/
+lemma ranges_join' : ∀ l : List ℕ, l.ranges.join = range (Nat.sum l)
+  | [] => rfl
+  | a :: l => by simp only [sum_cons, join, ← map_join, ranges_join', range_add]
 
-/-- Any entry of any member of `l.ranges` is strictly smaller than `l.sum` -/
-theorem mem_mem_ranges_iff_lt_sum (l : List ℕ) {n : ℕ} :
-    (∃ s ∈ List.ranges l,  n ∈ s) ↔ n < l.sum := by
-  rw [← mem_range, ← ranges_join, mem_join]
+/-- Any entry of any member of `l.ranges` is strictly smaller than `Nat.sum l`.
+See `List.mem_mem_ranges_iff_lt_sum` for the version about `List.sum`. -/
+lemma mem_mem_ranges_iff_lt_natSum (l : List ℕ) {n : ℕ} :
+    (∃ s ∈ l.ranges, n ∈ s) ↔ n < Nat.sum l := by
+  rw [← mem_range, ← ranges_join', mem_join]
 
  /-- The members of `l.ranges` have no duplicate -/
-theorem ranges_nodup {l s : List ℕ} (hs : s ∈ ranges l) :
-    s.Nodup := by
-  refine (List.pairwise_join.mp ?_).1 s hs
-  rw [ranges_join]
-  exact nodup_range (sum l)
+theorem ranges_nodup {l s : List ℕ} (hs : s ∈ ranges l) : s.Nodup :=
+  (List.pairwise_join.mp $ by rw [ranges_join']; exact nodup_range _).1 s hs
 
 end Ranges
 
diff --git a/Mathlib/Data/List/Rotate.lean b/Mathlib/Data/List/Rotate.lean
index 2324abf115dfe..7d370938f2050 100644
--- a/Mathlib/Data/List/Rotate.lean
+++ b/Mathlib/Data/List/Rotate.lean
@@ -5,6 +5,7 @@ Authors: Chris Hughes, Yakov Pechersky
 -/
 import Mathlib.Data.List.Nodup
 import Mathlib.Data.List.Zip
+import Mathlib.Data.Nat.Defs
 
 #align_import data.list.rotate from "leanprover-community/mathlib"@"f694c7dead66f5d4c80f446c796a5aad14707f0e"
 
@@ -78,7 +79,7 @@ theorem rotate'_rotate' : ∀ (l : List α) (n m : ℕ), (l.rotate' n).rotate' m
   | a :: l, 0, m => by simp
   | [], n, m => by simp
   | a :: l, n + 1, m => by
-    rw [rotate'_cons_succ, rotate'_rotate' _ n, add_right_comm, ← rotate'_cons_succ]
+    rw [rotate'_cons_succ, rotate'_rotate' _ n, Nat.add_right_comm, ← rotate'_cons_succ]
 #align list.rotate'_rotate' List.rotate'_rotate'
 
 @[simp]
@@ -170,16 +171,6 @@ theorem rotate_length_mul (l : List α) (n : ℕ) : l.rotate (l.length * n) = l
   rw [rotate_eq_rotate', rotate'_length_mul]
 #align list.rotate_length_mul List.rotate_length_mul
 
-theorem prod_rotate_eq_one_of_prod_eq_one [Group α] :
-    ∀ {l : List α} (_ : l.prod = 1) (n : ℕ), (l.rotate n).prod = 1
-  | [], _, _ => by simp
-  | a :: l, hl, n => by
-    have : n % List.length (a :: l) ≤ List.length (a :: l) := le_of_lt (Nat.mod_lt _ (by simp))
-    rw [← List.take_append_drop (n % List.length (a :: l)) (a :: l)] at hl;
-      rw [← rotate_mod, rotate_eq_drop_append_take this, List.prod_append, mul_eq_one_iff_inv_eq, ←
-        one_mul (List.prod _)⁻¹, ← hl, List.prod_append, mul_assoc, mul_inv_self, mul_one]
-#align list.prod_rotate_eq_one_of_prod_eq_one List.prod_rotate_eq_one_of_prod_eq_one
-
 theorem rotate_perm (l : List α) (n : ℕ) : l.rotate n ~ l := by
   rw [rotate_eq_rotate']
   induction' n with n hn generalizing l
@@ -235,22 +226,22 @@ theorem get?_rotate {l : List α} {n m : ℕ} (hml : m < l.length) :
     (l.rotate n).get? m = l.get? ((m + n) % l.length) := by
   rw [rotate_eq_drop_append_take_mod]
   rcases lt_or_le m (l.drop (n % l.length)).length with hm | hm
-  · rw [get?_append hm, get?_drop, add_comm m, ← mod_add_mod]
-    rw [length_drop, lt_tsub_iff_left] at hm
-    rw [mod_eq_of_lt hm]
+  · rw [get?_append hm, get?_drop, ← add_mod_mod]
+    rw [length_drop, Nat.lt_sub_iff_add_lt] at hm
+    rw [mod_eq_of_lt hm, Nat.add_comm]
   · have hlt : n % length l < length l := mod_lt _ (m.zero_le.trans_lt hml)
     rw [get?_append_right hm, get?_take, length_drop]
     · congr 1
       rw [length_drop] at hm
-      have hm' := tsub_le_iff_left.1 hm
+      have hm' := Nat.sub_le_iff_le_add'.1 hm
       have : n % length l + m - length l < length l := by
-        rw [tsub_lt_iff_left hm']
+        rw [Nat.sub_lt_iff_lt_add' hm']
         exact Nat.add_lt_add hlt hml
-      conv_rhs => rw [add_comm m, ← mod_add_mod, mod_eq_sub_mod hm', mod_eq_of_lt this]
-      rw [← add_right_inj l.length, ← add_tsub_assoc_of_le (α := ℕ), add_tsub_tsub_cancel (α := ℕ),
-        add_tsub_cancel_of_le (α := ℕ), add_comm]
+      conv_rhs => rw [Nat.add_comm m, ← mod_add_mod, mod_eq_sub_mod hm', mod_eq_of_lt this]
+      rw [← Nat.add_right_inj, ← Nat.add_sub_assoc, Nat.add_sub_sub_cancel, Nat.add_sub_cancel',
+        Nat.add_comm]
       exacts [hm', hlt.le, hm]
-    · rwa [tsub_lt_iff_left hm, length_drop, tsub_add_cancel_of_le hlt.le]
+    · rwa [Nat.sub_lt_iff_lt_add hm, length_drop, Nat.sub_add_cancel hlt.le]
 #align list.nth_rotate List.get?_rotate
 
 -- Porting note (#10756): new lemma
@@ -261,7 +252,7 @@ theorem get_rotate (l : List α) (n : ℕ) (k : Fin (l.rotate n).length) :
   exact k.2.trans_eq (length_rotate _ _)
 
 theorem head?_rotate {l : List α} {n : ℕ} (h : n < l.length) : head? (l.rotate n) = l.get? n := by
-  rw [← get?_zero, get?_rotate (n.zero_le.trans_lt h), zero_add, Nat.mod_eq_of_lt h]
+  rw [← get?_zero, get?_rotate (n.zero_le.trans_lt h), Nat.zero_add, Nat.mod_eq_of_lt h]
 #align list.head'_rotate List.head?_rotate
 
 -- Porting note: moved down from its original location below `get_rotate` so that the
@@ -291,7 +282,7 @@ theorem get_eq_get_rotate (l : List α) (n : ℕ) (k : Fin l.length) :
   rw [get_rotate]
   refine congr_arg l.get (Fin.eq_of_val_eq ?_)
   simp only [mod_add_mod]
-  rw [← add_mod_mod, add_right_comm, tsub_add_cancel_of_le (α := ℕ), add_mod_left, mod_eq_of_lt]
+  rw [← add_mod_mod, Nat.add_right_comm, Nat.sub_add_cancel, add_mod_left, mod_eq_of_lt]
   exacts [k.2, (mod_lt _ (k.1.zero_le.trans_lt k.2)).le]
 
 set_option linter.deprecated false in
@@ -340,7 +331,7 @@ theorem rotate_eq_iff {l l' : List α} {n : ℕ} :
   · rw [eq_nil_of_length_eq_zero hl.symm, rotate_nil]
   · rcases (Nat.zero_le (n % l'.length)).eq_or_lt with hn | hn
     · simp [← hn]
-    · rw [mod_eq_of_lt (tsub_lt_self hl hn), tsub_add_cancel_of_le (α := ℕ), mod_self, rotate_zero]
+    · rw [mod_eq_of_lt (Nat.sub_lt hl hn), Nat.sub_add_cancel, mod_self, rotate_zero]
       exact (Nat.mod_lt _ hl).le
 #align list.rotate_eq_iff List.rotate_eq_iff
 
@@ -376,9 +367,9 @@ theorem rotate_reverse (l : List α) (n : ℕ) :
   · simp_all! [k, length_reverse, ← rotate_rotate]
   · cases' l with x l
     · simp
-    · rw [Nat.mod_eq_of_lt, tsub_add_cancel_of_le (α := ℕ), rotate_length]
-      · exact tsub_le_self
-      · exact tsub_lt_self (by simp) (by simp_all! [k])
+    · rw [Nat.mod_eq_of_lt, Nat.sub_add_cancel, rotate_length]
+      · exact Nat.sub_le _ _
+      · exact Nat.sub_lt (by simp) (by simp_all! [k])
 #align list.rotate_reverse List.rotate_reverse
 
 theorem map_rotate {β : Type*} (f : α → β) (l : List α) (n : ℕ) :
@@ -401,7 +392,7 @@ theorem Nodup.rotate_eq_self_iff {l : List α} (hl : l.Nodup) {n : ℕ} :
     rw [nodup_iff_nthLe_inj] at hl
     refine' hl _ _ (mod_lt _ hl') hl' _
     rw [← nthLe_rotate' _ n]
-    simp_rw [h, tsub_add_cancel_of_le (mod_lt _ hl').le, mod_self]
+    simp_rw [h, Nat.sub_add_cancel (mod_lt _ hl').le, mod_self]
   · rintro (h | h)
     · rw [← rotate_mod, h]
       exact rotate_zero l
@@ -415,7 +406,7 @@ theorem Nodup.rotate_congr {l : List α} (hl : l.Nodup) (hn : l ≠ []) (i j : 
   have hj : j % l.length < l.length := mod_lt _ (length_pos_of_ne_nil hn)
   refine' (nodup_iff_nthLe_inj.mp hl) _ _ hi hj _
   rw [← nthLe_rotate' l i, ← nthLe_rotate' l j]
-  simp [tsub_add_cancel_of_le, hi.le, hj.le, h]
+  simp [Nat.sub_add_cancel, hi.le, hj.le, h]
 #align list.nodup.rotate_congr List.Nodup.rotate_congr
 
 section IsRotated
@@ -444,7 +435,7 @@ theorem IsRotated.symm (h : l ~r l') : l' ~r l := by
   cases' l with hd tl
   · exists 0
   · use (hd :: tl).length * n - n
-    rw [rotate_rotate, add_tsub_cancel_of_le (α := ℕ), rotate_length_mul]
+    rw [rotate_rotate, Nat.add_sub_cancel', rotate_length_mul]
     exact Nat.le_mul_of_pos_left _ (by simp)
 #align list.is_rotated.symm List.IsRotated.symm
 
@@ -673,7 +664,7 @@ theorem cyclicPermutations_rotate (l : List α) (k : ℕ) :
     · simp
     · rw [length_cyclicPermutations_of_ne_nil] <;> simp
   refine' ext_nthLe this fun n hn hn' => _
-  rw [nthLe_rotate, nthLe_cyclicPermutations, rotate_rotate, ← rotate_mod, add_comm]
+  rw [nthLe_rotate, nthLe_cyclicPermutations, rotate_rotate, ← rotate_mod, Nat.add_comm]
   cases l <;> simp
 #align list.cyclic_permutations_rotate List.cyclicPermutations_rotate
 
@@ -695,7 +686,7 @@ theorem isRotated_cyclicPermutations_iff {l l' : List α} :
   refine' ⟨k % l.length, _⟩
   have hk' : k % l.length < l.length := mod_lt _ (length_pos_of_ne_nil hl)
   rw [← nthLe_cyclicPermutations _ _ (hk'.trans_le hl'.ge), ← nthLe_rotate' _ k]
-  simp [hk, hl', tsub_add_cancel_of_le hk'.le]
+  simp [hk, hl', Nat.sub_add_cancel hk'.le]
 #align list.is_rotated_cyclic_permutations_iff List.isRotated_cyclicPermutations_iff
 
 section Decidable
diff --git a/Mathlib/Data/List/Zip.lean b/Mathlib/Data/List/Zip.lean
index 1ba8ac5345f52..31c03bd69e896 100644
--- a/Mathlib/Data/List/Zip.lean
+++ b/Mathlib/Data/List/Zip.lean
@@ -3,8 +3,8 @@ 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 Mathlib.Algebra.BigOperators.List.Basic
-import Mathlib.Algebra.Order.Monoid.MinMax
+import Mathlib.Data.List.Forall2
+import Mathlib.Order.MinMax
 
 #align_import data.list.zip from "leanprover-community/mathlib"@"134625f523e737f650a6ea7f0c82a6177e45e622"
 
@@ -349,16 +349,6 @@ theorem map_uncurry_zip_eq_zipWith (f : α → β → γ) (l : List α) (l' : Li
     · simp [hl]
 #align list.map_uncurry_zip_eq_zip_with List.map_uncurry_zip_eq_zipWith
 
-@[simp]
-theorem sum_zipWith_distrib_left {γ : Type*} [Semiring γ] (f : α → β → γ) (n : γ) (l : List α)
-    (l' : List β) : (l.zipWith (fun x y => n * f x y) l').sum = n * (l.zipWith f l').sum := by
-  induction' l with hd tl hl generalizing f n l'
-  · simp
-  · cases' l' with hd' tl'
-    · simp
-    · simp [hl, mul_add]
-#align list.sum_zip_with_distrib_left List.sum_zipWith_distrib_left
-
 section Distrib
 
 /-! ### Operations that can be applied before or after a `zip_with` -/
@@ -377,42 +367,10 @@ theorem zipWith_distrib_reverse (h : l.length = l'.length) :
   · simp
   · cases' l' with hd' tl'
     · simp
-    · simp only [add_left_inj, length] at h
+    · simp only [Nat.add_left_inj, length] at h
       have : tl.reverse.length = tl'.reverse.length := by simp [h]
       simp [hl _ h, zipWith_append _ _ _ _ _ this]
 #align list.zip_with_distrib_reverse List.zipWith_distrib_reverse
 
 end Distrib
-
-section CommMonoid
-
-variable [CommMonoid α]
-
-@[to_additive]
-theorem prod_mul_prod_eq_prod_zipWith_mul_prod_drop :
-    ∀ L L' : List α,
-      L.prod * L'.prod =
-        (zipWith (· * ·) L L').prod * (L.drop L'.length).prod * (L'.drop L.length).prod
-  | [], ys => by simp [Nat.zero_le]
-  | xs, [] => by simp [Nat.zero_le]
-  | x :: xs, y :: ys => by
-    simp only [drop, length, zipWith_cons_cons, prod_cons]
-    conv =>
-      lhs; rw [mul_assoc]; right; rw [mul_comm, mul_assoc]; right
-      rw [mul_comm, prod_mul_prod_eq_prod_zipWith_mul_prod_drop xs ys]
-    simp only [add_eq, add_zero]
-    ac_rfl
-#align list.prod_mul_prod_eq_prod_zip_with_mul_prod_drop List.prod_mul_prod_eq_prod_zipWith_mul_prod_drop
-#align list.sum_add_sum_eq_sum_zip_with_add_sum_drop List.sum_add_sum_eq_sum_zipWith_add_sum_drop
-
-@[to_additive]
-theorem prod_mul_prod_eq_prod_zipWith_of_length_eq (L L' : List α) (h : L.length = L'.length) :
-    L.prod * L'.prod = (zipWith (· * ·) L L').prod := by
-  apply (prod_mul_prod_eq_prod_zipWith_mul_prod_drop L L').trans
-  rw [← h, drop_length, h, drop_length, prod_nil, mul_one, mul_one]
-#align list.prod_mul_prod_eq_prod_zip_with_of_length_eq List.prod_mul_prod_eq_prod_zipWith_of_length_eq
-#align list.sum_add_sum_eq_sum_zip_with_of_length_eq List.sum_add_sum_eq_sum_zipWith_of_length_eq
-
-end CommMonoid
-
 end List