chore(Algebra/BigOperators/List): Use Std lemmas (#11725)

* Make `Algebra.BigOperators.List.Basic`, `Data.List.Chain` not depend on `Data.Nat.Order.Basic` by using `Nat`-specific Std lemmas rather than general mathlib ones. I leave the `Data.Nat.Basic` import since `Algebra.BigOperators.List.Basic` is algebra territory.
* Make `Algebra.BigOperators.List.Basic` not depend on `Algebra.Divisibility.Basic`. I'm not too sure about that one since they already are algebra. My motivation is that they involve ring-like objects while big operators are about group-like objects, but this is in some sense a second order refactor.
* As a consequence, move the divisibility and `MonoidWithZero` lemmas from `Algebra.BigOperators.List.Basic` to `Algebra.BigOperators.List.Lemmas`.
* Move the content of `Algebra.BigOperators.List.Defs` to `Algebra.BigOperators.List.Basic` since no file imported the former without the latter and their imports are becoming very close after this PR.
* Make `Data.List.Count`, `Data.List.Dedup`, `Data.List.ProdSigma`, `Data.List.Zip` not depend on `Algebra.BigOperators.List.Basic`.
* As a consequence, move the big operators lemmas that were in there to `Algebra.BigOperators.List.Basic`. For the lemmas that were `Nat` -specific, keep a version of them stated using `Nat.sum`.
* To help with this, add `Nat.sum_eq_listSum (l : List Nat) : Nat.sum l = l.sum`.

Archive/Examples/IfNormalization/Result.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
 import Archive.Examples.IfNormalization.Statement
+import Mathlib.Algebra.Order.Monoid.Canonical.Defs
+import Mathlib.Algebra.Order.Monoid.MinMax
 import Mathlib.Data.List.AList
 import Mathlib.Tactic.Recall
 

Archive/Examples/IfNormalization/WithoutAesop.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Scott Morrison
 -/
 import Archive.Examples.IfNormalization.Statement
+import Mathlib.Algebra.Order.Monoid.Canonical.Defs
+import Mathlib.Algebra.Order.Monoid.MinMax
 import Mathlib.Data.List.AList
 
 /-!

Mathlib.lean

@@ -29,7 +29,6 @@ import Mathlib.Algebra.BigOperators.Finprod
 import Mathlib.Algebra.BigOperators.Finsupp
 import Mathlib.Algebra.BigOperators.Intervals
 import Mathlib.Algebra.BigOperators.List.Basic
-import Mathlib.Algebra.BigOperators.List.Defs
 import Mathlib.Algebra.BigOperators.List.Lemmas
 import Mathlib.Algebra.BigOperators.Module
 import Mathlib.Algebra.BigOperators.Multiset.Basic

Mathlib/Algebra/BigOperators/List/Basic.lean

@@ -3,16 +3,13 @@ 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 Mathlib.Algebra.BigOperators.List.Defs
-import Mathlib.Data.List.Forall2
-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
+import Mathlib.Data.Nat.Basic
 
 #align_import data.list.big_operators.basic from "leanprover-community/mathlib"@"6c5f73fd6f6cc83122788a80a27cdd54663609f4"
 
@@ -21,12 +18,45 @@ import Mathlib.Data.List.Rotate
 
 This file provides basic results about `List.prod`, `List.sum`, which calculate the product and sum
 of elements of a list and `List.alternatingProd`, `List.alternatingSum`, their alternating
-counterparts. These are defined in [`Algebra.BigOperators.List.Defs`](./Defs).
+counterparts.
 -/
 
+-- Make sure we haven't imported `Data.Nat.Order.Basic`
+assert_not_exists OrderedSub
+
+-- TODO
+-- assert_not_exists Ring
+
 variable {ι α β γ M N P M₀ G R : Type*}
 
 namespace List
+section Defs
+
+/-- Product of a list.
+
+`List.prod [a, b, c] = ((1 * a) * b) * c` -/
+@[to_additive "Sum of a list.\n\n`List.sum [a, b, c] = ((0 + a) + b) + c`"]
+def prod {α} [Mul α] [One α] : List α → α :=
+  foldl (· * ·) 1
+#align list.prod List.prod
+#align list.sum List.sum
+
+/-- The alternating sum of a list. -/
+def alternatingSum {G : Type*} [Zero G] [Add G] [Neg G] : List G → G
+  | [] => 0
+  | g :: [] => g
+  | g :: h :: t => g + -h + alternatingSum t
+#align list.alternating_sum List.alternatingSum
+
+/-- The alternating product of a list. -/
+@[to_additive existing]
+def alternatingProd {G : Type*} [One G] [Mul G] [Inv G] : List G → G
+  | [] => 1
+  | g :: [] => g
+  | g :: h :: t => g * h⁻¹ * alternatingProd t
+#align list.alternating_prod List.alternatingProd
+
+end Defs
 
 section MulOneClass
 
@@ -248,7 +278,8 @@ theorem prod_set :
       (L.set n a).prod =
         ((L.take n).prod * if n < L.length then a else 1) * (L.drop (n + 1)).prod
   | x :: xs, 0, a => by simp [set]
-  | x :: xs, i + 1, a => by simp [set, prod_set xs i a, mul_assoc, Nat.succ_eq_add_one]
+  | x :: xs, i + 1, a => by
+    simp [set, prod_set xs i a, mul_assoc, Nat.succ_eq_add_one, Nat.add_lt_add_iff_right]
   | [], _, _ => by simp [set, (Nat.zero_le _).not_lt, Nat.zero_le]
 #align list.prod_update_nth List.prod_set
 #align list.sum_update_nth List.sum_set
@@ -309,10 +340,7 @@ lemma prod_range_succ' (f : ℕ → M) (n : ℕ) :
 #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
+@[to_additive] 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]
@@ -403,37 +431,15 @@ lemma prod_mul_prod_eq_prod_zipWith_of_length_eq (l l' : List M) (h : l.length =
 
 end CommMonoid
 
-section MonoidWithZero
-
-variable [MonoidWithZero M₀]
-
-/-- If zero is an element of a list `L`, then `List.prod L = 0`. If the domain is a nontrivial
-monoid with zero with no divisors, then this implication becomes an `iff`, see
-`List.prod_eq_zero_iff`. -/
-theorem prod_eq_zero {L : List M₀} (h : (0 : M₀) ∈ L) : L.prod = 0 := by
-  induction' L with a L ihL
-  · exact absurd h (not_mem_nil _)
-  · rw [prod_cons]
-    cases' mem_cons.1 h with ha hL
-    exacts [mul_eq_zero_of_left ha.symm _, mul_eq_zero_of_right _ (ihL hL)]
-#align list.prod_eq_zero List.prod_eq_zero
-
-/-- Product of elements of a list `L` equals zero if and only if `0 ∈ L`. See also
-`List.prod_eq_zero` for an implication that needs weaker typeclass assumptions. -/
-@[simp]
-theorem prod_eq_zero_iff [Nontrivial M₀] [NoZeroDivisors M₀] {L : List M₀} :
-    L.prod = 0 ↔ (0 : M₀) ∈ L := by
-  induction' L with a L ihL
-  · simp
-  · rw [prod_cons, mul_eq_zero, ihL, mem_cons, eq_comm]
-#align list.prod_eq_zero_iff List.prod_eq_zero_iff
-
-theorem prod_ne_zero [Nontrivial M₀] [NoZeroDivisors M₀] {L : List M₀} (hL : (0 : M₀) ∉ L) :
-    L.prod ≠ 0 :=
-  mt prod_eq_zero_iff.1 hL
-#align list.prod_ne_zero List.prod_ne_zero
-
-end MonoidWithZero
+@[to_additive]
+lemma 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
+  refine ext_get h fun i h₁ h₂ => ?_
+  have : (L.take (i + 1)).prod = (L'.take (i + 1)).prod := h' _ (Nat.succ_le_of_lt h₁)
+  rw [prod_take_succ L i h₁, prod_take_succ L' i h₂, h' i (le_of_lt h₁)] at this
+  convert mul_left_cancel this
+#align list.eq_of_prod_take_eq List.eq_of_prod_take_eq
+#align list.eq_of_sum_take_eq List.eq_of_sum_take_eq
 
 section Group
 
@@ -529,16 +535,6 @@ theorem sum_zipWith_distrib_left [Semiring γ] (f : α → β → γ) (n : γ) (
     · 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
-  refine ext_get h fun i h₁ h₂ => ?_
-  have : (L.take (i + 1)).prod = (L'.take (i + 1)).prod := h' _ (Nat.succ_le_of_lt h₁)
-  rw [prod_take_succ L i h₁, prod_take_succ L' i h₂, h' i (le_of_lt h₁)] at this
-  convert mul_left_cancel this
-#align list.eq_of_prod_take_eq List.eq_of_prod_take_eq
-#align list.eq_of_sum_take_eq List.eq_of_sum_take_eq
-
 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
@@ -561,7 +557,7 @@ theorem headI_le_sum (L : List ℕ) : L.headI ≤ L.sum :=
 
 /-- This relies on `default ℕ = 0`. -/
 theorem tail_sum (L : List ℕ) : L.tail.sum = L.sum - L.headI := by
-  rw [← headI_add_tail_sum L, add_comm, @add_tsub_cancel_right]
+  rw [← headI_add_tail_sum L, add_comm, Nat.add_sub_cancel_right]
 #align list.tail_sum List.tail_sum
 
 section Alternating
@@ -619,11 +615,15 @@ theorem alternatingProd_cons (a : α) (l : List α) :
 end Alternating
 
 lemma sum_nat_mod (l : List ℕ) (n : ℕ) : l.sum % n = (l.map (· % n)).sum % n := by
-  induction l <;> simp [Nat.add_mod, *]
+  induction' l with a l ih
+  · simp only [Nat.zero_mod, map_nil]
+  · simpa only [map_cons, sum_cons, Nat.mod_add_mod, Nat.add_mod_mod] using congr((a + $ih) % n)
 #align list.sum_nat_mod List.sum_nat_mod
 
 lemma prod_nat_mod (l : List ℕ) (n : ℕ) : l.prod % n = (l.map (· % n)).prod % n := by
-  induction l <;> simp [Nat.mul_mod, *]
+  induction' l with a l ih
+  · simp only [Nat.zero_mod, map_nil]
+  · simpa only [prod_cons, map_cons, Nat.mod_mul_mod, Nat.mul_mod_mod] using congr((a * $ih) % n)
 #align list.prod_nat_mod List.prod_nat_mod
 
 lemma sum_int_mod (l : List ℤ) (n : ℤ) : l.sum % n = (l.map (· % n)).sum % n := by

Mathlib/Algebra/BigOperators/List/Lemmas.lean

@@ -8,7 +8,6 @@ import Mathlib.Algebra.Group.Opposite
 import Mathlib.Algebra.GroupPower.Basic
 import Mathlib.Algebra.GroupWithZero.Commute
 import Mathlib.Algebra.GroupWithZero.Divisibility
-import Mathlib.Algebra.Order.Monoid.OrderDual
 import Mathlib.Algebra.Ring.Basic
 import Mathlib.Algebra.Ring.Commute
 import Mathlib.Algebra.Ring.Divisibility.Basic
@@ -58,7 +57,7 @@ by the sum of the elements. -/
 theorem length_le_sum_of_one_le (L : List ℕ) (h : ∀ i ∈ L, 1 ≤ i) : L.length ≤ L.sum := by
   induction' L with j L IH h; · simp
   rw [sum_cons, length, add_comm]
-  exact add_le_add (h _ (mem_cons_self _ _)) (IH fun i hi => h i (mem_cons.2 (Or.inr hi)))
+  exact Nat.add_le_add (h _ (mem_cons_self _ _)) (IH fun i hi => h i (mem_cons.2 (Or.inr hi)))
 #align list.length_le_sum_of_one_le List.length_le_sum_of_one_le
 
 theorem dvd_prod [CommMonoid M] {a} {l : List M} (ha : a ∈ l) : a ∣ l.prod := by
@@ -67,6 +66,37 @@ theorem dvd_prod [CommMonoid M] {a} {l : List M} (ha : a ∈ l) : a ∣ l.prod :
   exact dvd_mul_right _ _
 #align list.dvd_prod List.dvd_prod
 
+section MonoidWithZero
+variable [MonoidWithZero M₀]
+
+/-- If zero is an element of a list `L`, then `List.prod L = 0`. If the domain is a nontrivial
+monoid with zero with no divisors, then this implication becomes an `iff`, see
+`List.prod_eq_zero_iff`. -/
+lemma prod_eq_zero {L : List M₀} (h : (0 : M₀) ∈ L) : L.prod = 0 := by
+  induction' L with a L ihL
+  · exact absurd h (not_mem_nil _)
+  · rw [prod_cons]
+    cases' mem_cons.1 h with ha hL
+    exacts [mul_eq_zero_of_left ha.symm _, mul_eq_zero_of_right _ (ihL hL)]
+#align list.prod_eq_zero List.prod_eq_zero
+
+/-- Product of elements of a list `L` equals zero if and only if `0 ∈ L`. See also
+`List.prod_eq_zero` for an implication that needs weaker typeclass assumptions. -/
+@[simp]
+lemma prod_eq_zero_iff [Nontrivial M₀] [NoZeroDivisors M₀] {L : List M₀} :
+    L.prod = 0 ↔ (0 : M₀) ∈ L := by
+  induction' L with a L ihL
+  · simp
+  · rw [prod_cons, mul_eq_zero, ihL, mem_cons, eq_comm]
+#align list.prod_eq_zero_iff List.prod_eq_zero_iff
+
+lemma prod_ne_zero [Nontrivial M₀] [NoZeroDivisors M₀] {L : List M₀} (hL : (0 : M₀) ∉ L) :
+    L.prod ≠ 0 :=
+  mt prod_eq_zero_iff.1 hL
+#align list.prod_ne_zero List.prod_ne_zero
+
+end MonoidWithZero
+
 theorem dvd_sum [NonUnitalSemiring R] {a} {l : List R} (h : ∀ x ∈ l, a ∣ x) : a ∣ l.sum := by
   induction' l with x l ih
   · exact dvd_zero _

Mathlib/Algebra/BigOperators/Multiset/Basic.lean

@@ -3,9 +3,10 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
+import Mathlib.Algebra.BigOperators.List.Basic
+import Mathlib.Algebra.Divisibility.Basic
 import Mathlib.Algebra.Group.Hom.Basic
 import Mathlib.Algebra.GroupPower.Hom
-import Mathlib.Algebra.BigOperators.List.Basic
 import Mathlib.Data.Multiset.Basic
 
 #align_import algebra.big_operators.multiset.basic from "leanprover-community/mathlib"@"6c5f73fd6f6cc83122788a80a27cdd54663609f4"

Mathlib/Algebra/FreeMonoid/Basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Yury Kudryashov
 -/
 import Mathlib.Algebra.BigOperators.List.Basic
+import Mathlib.Algebra.Group.Units
 import Mathlib.GroupTheory.GroupAction.Defs
 
 #align_import algebra.free_monoid.basic from "leanprover-community/mathlib"@"657df4339ae6ceada048c8a2980fb10e393143ec"

Mathlib/Algebra/Order/BigOperators/Group/List.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yakov Pechersky
 -/
 import Mathlib.Algebra.BigOperators.List.Basic
+import Mathlib.Algebra.Order.Monoid.Canonical.Defs
 import Mathlib.Algebra.Order.Monoid.OrderDual
 
 /-!

Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean

@@ -3,11 +3,11 @@ Copyright (c) 2019 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
-import Mathlib.Algebra.BigOperators.List.Basic
 import Mathlib.Algebra.BigOperators.Multiset.Basic
 import Mathlib.Algebra.Order.BigOperators.Group.List
-import Mathlib.Algebra.Order.Monoid.OrderDual
 import Mathlib.Algebra.Order.Group.Abs
+import Mathlib.Data.List.MinMax
+import Mathlib.Data.Multiset.Fold
 
 /-!
 # Big operators on a multiset in ordered groups
@@ -177,6 +177,12 @@ variable [CanonicallyOrderedCommMonoid α] {m : Multiset α} {a : α}
 
 end CanonicallyOrderedCommMonoid
 
+lemma max_le_of_forall_le {α : Type*} [LinearOrder α] [OrderBot α] (l : Multiset α)
+    (n : α) (h : ∀ x ∈ l, x ≤ n) : l.fold max ⊥ ≤ n := by
+  induction l using Quotient.inductionOn
+  simpa using List.max_le_of_forall_le _ _ h
+#align multiset.max_le_of_forall_le Multiset.max_le_of_forall_le
+
 lemma abs_sum_le_sum_abs [LinearOrderedAddCommGroup α] {s : Multiset α} :
     |s.sum| ≤ (s.map abs).sum :=
   le_sum_of_subadditive _ abs_zero abs_add s

Mathlib/Data/Finset/Basic.lean

@@ -2984,13 +2984,13 @@ theorem mem_range_le {n x : ℕ} (hx : x ∈ range n) : x ≤ n :=
 #align finset.mem_range_le Finset.mem_range_le
 
 theorem mem_range_sub_ne_zero {n x : ℕ} (hx : x ∈ range n) : n - x ≠ 0 :=
-  _root_.ne_of_gt <| tsub_pos_of_lt <| mem_range.1 hx
+  _root_.ne_of_gt <| Nat.sub_pos_of_lt <| mem_range.1 hx
 #align finset.mem_range_sub_ne_zero Finset.mem_range_sub_ne_zero
 
 @[simp, aesop safe apply (rule_sets := [finsetNonempty])]
 theorem nonempty_range_iff : (range n).Nonempty ↔ n ≠ 0 :=
-  ⟨fun ⟨k, hk⟩ => ((_root_.zero_le k).trans_lt <| mem_range.1 hk).ne',
-   fun h => ⟨0, mem_range.2 <| pos_iff_ne_zero.2 h⟩⟩
+  ⟨fun ⟨k, hk⟩ => (k.zero_le.trans_lt <| mem_range.1 hk).ne',
+   fun h => ⟨0, mem_range.2 <| Nat.pos_iff_ne_zero.2 h⟩⟩
 #align finset.nonempty_range_iff Finset.nonempty_range_iff
 
 @[simp]
@@ -3012,7 +3012,7 @@ theorem range_filter_eq {n m : ℕ} : (range n).filter (· = m) = if m < n then
 
 lemma range_nontrivial {n : ℕ} (hn : 1 < n) : (Finset.range n).Nontrivial := by
   rw [Finset.Nontrivial, Finset.coe_range]
-  exact ⟨0, zero_lt_one.trans hn, 1, hn, zero_ne_one⟩
+  exact ⟨0, Nat.zero_lt_one.trans hn, 1, hn, zero_ne_one⟩
 
 end Range