fix merge

src/Init/Data/List/Basic.lean

@@ -1398,8 +1398,17 @@ def unzip : List (α × β) → List α × List β
 
 /-! ## Ranges and enumeration -/
 
+/-- Sum of a list.
+
+`List.sum [a, b, c] = a + (b + (c + 0))` -/
+def sum {α} [Add α] [Zero α] : List α → α :=
+  foldr (· + ·) 0
+
+@[simp] theorem sum_nil [Add α] [Zero α] : ([] : List α).sum = 0 := rfl
+@[simp] theorem sum_cons [Add α] [Zero α] {a : α} {l : List α} : (a::l).sum = a + l.sum := rfl
+
 /-- Sum of a list of natural numbers. -/
--- This is not in the `List` namespace as later `List.sum` will be defined polymorphically.
+-- We intend to subsequently deprecate this in favor of `List.sum`.
 protected def _root_.Nat.sum (l : List Nat) : Nat := l.foldr (·+·) 0
 
 @[simp] theorem _root_.Nat.sum_nil : Nat.sum ([] : List Nat) = 0 := rfl

src/Init/Data/List/Count.lean

@@ -156,7 +156,7 @@ theorem countP_filterMap (p : β → Bool) (f : α → Option β) (l : List α)
   simp (config := { contextual := true }) [Option.getD_eq_iff, Option.isSome_eq_isSome]
 
 @[simp] theorem countP_flatten (l : List (List α)) :
-    countP p l.flatten = Nat.sum (l.map (countP p)) := by
+    countP p l.flatten = (l.map (countP p)).sum := by
   simp only [countP_eq_length_filter, filter_flatten]
   simp [countP_eq_length_filter']
 
@@ -232,7 +232,7 @@ theorem count_singleton (a b : α) : count a [b] = if b == a then 1 else 0 := by
 @[simp] theorem count_append (a : α) : ∀ l₁ l₂, count a (l₁ ++ l₂) = count a l₁ + count a l₂ :=
   countP_append _
 
-theorem count_flatten (a : α) (l : List (List α)) : count a l.flatten = Nat.sum (l.map (count a)) := by
+theorem count_flatten (a : α) (l : List (List α)) : count a l.flatten = (l.map (count a)).sum := by
   simp only [count_eq_countP, countP_flatten, count_eq_countP']
 
 @[deprecated count_flatten (since := "2024-10-14")] abbrev count_join := @count_flatten

src/Init/Data/List/Find.lean

@@ -789,7 +789,7 @@ theorem findIdx?_of_eq_none {xs : List α} {p : α → Bool} (w : xs.findIdx? p
 theorem findIdx?_flatten {l : List (List α)} {p : α → Bool} :
     l.flatten.findIdx? p =
       (l.findIdx? (·.any p)).map
-        fun i => Nat.sum ((l.take i).map List.length) +
+        fun i => ((l.take i).map List.length).sum +
           (l[i]?.map fun xs => xs.findIdx p).getD 0 := by
   induction l with
   | nil => simp

src/Init/Data/List/Lemmas.lean

@@ -2070,8 +2070,7 @@ theorem eq_nil_or_concat : ∀ l : List α, l = [] ∨ ∃ L b, l = concat L b
 
 /-! ### flatten -/
 
-
-@[simp] theorem length_flatten (L : List (List α)) : (flatten L).length = Nat.sum (L.map length) := by
+@[simp] theorem length_flatten (L : List (List α)) : (flatten L).length = (L.map length).sum := by
   induction L with
   | nil => rfl
   | cons =>

src/Init/Data/List/Range.lean

@@ -20,7 +20,6 @@ open Nat
 
 /-! ## Ranges and enumeration -/
 
-
 /-! ### range' -/
 
 theorem range'_succ (s n step) : range' s (n + 1) step = s :: range' (s + step) n step := by