feat: lemmas about sums of lists/arrays/vectors

src/Init/Data/Array.lean

@@ -30,3 +30,5 @@ public import Init.Data.Array.Erase
 public import Init.Data.Array.Zip
 public import Init.Data.Array.InsertIdx
 public import Init.Data.Array.Extract
+public import Init.Data.Array.Nat
+public import Init.Data.Array.Int

src/Init/Data/Array/Find.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.List.Nat.Find
+import Init.Data.List.Nat.Sum
 import all Init.Data.Array.Basic
 public import Init.Data.Array.Range
 
@@ -114,7 +115,7 @@ theorem getElem_zero_flatten.proof {xss : Array (Array α)} (h : 0 < xss.flatten
   simp only [List.findSome?_toArray, List.findSome?_map, Function.comp_def, List.getElem?_toArray,
     List.findSome?_isSome_iff, isSome_getElem?]
   simp only [flatten_toArray_map_toArray, List.size_toArray, List.length_flatten,
-    Nat.sum_pos_iff_exists_pos, List.mem_map] at h
+    List.sum_pos_iff_exists_pos_nat, List.mem_map] at h
   obtain ⟨_, ⟨xs, m, rfl⟩, h⟩ := h
   exact ⟨xs, m, by simpa using h⟩
 

src/Init/Data/Array/Int.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison, Sebastian Graf, Paul Reichert
+-/
+module
+
+prelude
+public import Init.Data.List.Int.Sum
+public import Init.Data.Array.Lemmas
+public import Init.Data.Int.DivMod.Bootstrap
+import Init.Data.Int.DivMod.Lemmas
+import Init.Data.List.MinMax
+
+public section
+
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
+namespace Array
+
+@[simp] theorem sum_replicate_int {n : Nat} {a : Int} : (replicate n a).sum = n * a := by
+  rw [← List.toArray_replicate, List.sum_toArray]
+  simp
+
+@[simp, grind =]
+theorem sum_append_int {as₁ as₂ : Array Int} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
+  simp [sum_append]
+
+@[simp, grind =]
+theorem sum_reverse_int (xs : Array Int) : xs.reverse.sum = xs.sum := by
+  simp [sum_reverse]
+
+theorem sum_eq_foldl_int {xs : Array Int} : xs.sum = xs.foldl (init := 0) (· + ·) := by
+  simp only [foldl_eq_foldr_reverse, Int.add_comm, ← sum_eq_foldr, sum_reverse_int]
+
+end Array

src/Init/Data/Array/Lemmas.lean

@@ -2500,10 +2500,6 @@ theorem flatMap_replicate {f : α → Array β} : (replicate n a).flatMap f = (r
   rw [← List.toArray_replicate, List.isEmpty_toArray]
   simp
 
-@[simp] theorem sum_replicate_nat {n : Nat} {a : Nat} : (replicate n a).sum = n * a := by
-  rw [← List.toArray_replicate, List.sum_toArray]
-  simp
-
 /-! ### Preliminaries about `swap` needed for `reverse`. -/
 
 @[grind =]
@@ -4277,19 +4273,29 @@ theorem getElem?_range {n : Nat} {i : Nat} : (Array.range n)[i]? = if i < n then
 /-! ### sum -/
 
 @[simp, grind =] theorem sum_empty [Add α] [Zero α] : (#[] : Array α).sum = 0 := rfl
+theorem sum_eq_foldr [Add α] [Zero α] {xs : Array α} :
+    xs.sum = xs.foldr (init := 0) (· + ·) :=
+  rfl
 
 -- Without further algebraic hypotheses, there's no useful `sum_push` lemma.
 
 @[simp, grind =]
-theorem sum_eq_sum_toList [Add α] [Zero α] {as : Array α} : as.toList.sum = as.sum := by
+theorem sum_toList [Add α] [Zero α] {as : Array α} : as.toList.sum = as.sum := by
   cases as
   simp [Array.sum, List.sum]
 
-@[simp, grind =]
-theorem sum_append_nat {as₁ as₂ : Array Nat} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
-  cases as₁
-  cases as₂
-  simp [List.sum_append_nat]
+@[deprecated sum_toList (since := "2026-01-14")]
+def sum_eq_sum_toList := @sum_toList
+
+theorem sum_append [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
+    [Std.LeftIdentity (α := α) (· + ·) 0] [Std.LawfulLeftIdentity (α := α) (· + ·) 0]
+    {as₁ as₂ : Array α} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
+  simp [← sum_toList, List.sum_append]
+
+theorem sum_reverse [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
+    [Std.Commutative (α := α) (· + ·)]
+    [Std.LawfulLeftIdentity (α := α) (· + ·) 0] (xs : Array α) : xs.reverse.sum = xs.sum := by
+  simp [← sum_toList, List.sum_reverse]
 
 theorem foldl_toList_eq_flatMap {l : List α} {acc : Array β}
     {F : Array β → α → Array β} {G : α → List β}

src/Init/Data/Array/Nat.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison, Sebastian Graf, Paul Reichert
+-/
+module
+
+prelude
+public import Init.Data.Array.Lemmas
+import Init.Data.List.Nat.Sum
+
+public section
+
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
+namespace Array
+
+protected theorem sum_pos_iff_exists_pos_nat {xs : Array Nat} : 0 < xs.sum ↔ ∃ x ∈ xs, 0 < x := by
+  simp [← sum_toList, List.sum_pos_iff_exists_pos_nat]
+
+protected theorem sum_eq_zero_iff_forall_eq_nat {xs : Array Nat} :
+    xs.sum = 0 ↔ ∀ x ∈ xs, x = 0 := by
+  simp [← sum_toList, List.sum_eq_zero_iff_forall_eq_nat]
+
+@[simp] theorem sum_replicate_nat {n : Nat} {a : Nat} : (replicate n a).sum = n * a := by
+  rw [← List.toArray_replicate, List.sum_toArray]
+  simp
+
+@[simp, grind =]
+theorem sum_append_nat {as₁ as₂ : Array Nat} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
+  simp [sum_append]
+
+@[simp, grind =]
+theorem sum_reverse_nat (xs : Array Nat) : xs.reverse.sum = xs.sum := by
+  simp [sum_reverse]
+
+theorem sum_eq_foldl_nat {xs : Array Nat} : xs.sum = xs.foldl (init := 0) (· + ·) := by
+  simp only [foldl_eq_foldr_reverse, Nat.add_comm, ← sum_eq_foldr, sum_reverse_nat]
+
+end Array

src/Init/Data/Int/Order.lean

@@ -1447,4 +1447,10 @@ instance : LawfulOrderLT Int where
   lt_iff := by
     simp [← Int.not_le, Decidable.imp_iff_not_or, Std.Total.total]
 
+instance : LawfulOrderInf Int where
+  le_min_iff _ _ _ := Int.le_min
+
+instance : LawfulOrderSup Int where
+  max_le_iff _ _ _ := Int.max_le
+
 end Int

src/Init/Data/List.lean

@@ -18,6 +18,7 @@ public import Init.Data.List.Lemmas
 public import Init.Data.List.MinMax
 public import Init.Data.List.Monadic
 public import Init.Data.List.Nat
+public import Init.Data.List.Int
 public import Init.Data.List.Notation
 public import Init.Data.List.Pairwise
 public import Init.Data.List.Sublist

src/Init/Data/List/Basic.lean

@@ -2017,6 +2017,7 @@ def sum {α} [Add α] [Zero α] : List α → α :=
 
 @[simp, grind =] theorem sum_nil [Add α] [Zero α] : ([] : List α).sum = 0 := rfl
 @[simp, grind =] theorem sum_cons [Add α] [Zero α] {a : α} {l : List α} : (a::l).sum = a + l.sum := rfl
+theorem sum_eq_foldr [Add α] [Zero α] {l : List α} : l.sum = l.foldr (· + ·) 0 := rfl
 
 /-! ### range -/
 

src/Init/Data/List/Int.lean

@@ -0,0 +1,9 @@
+/-
+Copyright (c) 2026 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Init.Data.List.Int.Sum

src/Init/Data/List/Int/Sum.lean

@@ -0,0 +1,109 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison, Sebastian Graf, Paul Reichert
+-/
+module
+
+prelude
+public import Init.Data.Int.DivMod.Bootstrap
+import Init.Data.Int.DivMod.Lemmas
+import Init.Data.List.MinMax
+
+public section
+
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
+namespace List
+
+@[simp]
+theorem sum_replicate_int {n : Nat} {a : Int} : (replicate n a).sum = n * a := by
+  induction n <;> simp_all [replicate_succ, Int.add_mul, Int.add_comm]
+
+@[simp, grind =]
+theorem sum_append_int {l₁ l₂ : List Int} : (l₁ ++ l₂).sum = l₁.sum + l₂.sum := by
+  simp [sum_append]
+
+@[simp, grind =]
+theorem sum_reverse_int (xs : List Int) : xs.reverse.sum = xs.sum := by
+  simp [sum_reverse]
+
+theorem min_mul_length_le_sum_int {xs : List Int} (h : xs ≠ []) :
+    xs.min h * xs.length ≤ xs.sum := by
+  induction xs
+  · contradiction
+  · rename_i x xs ih
+    cases xs
+    · simp_all [List.min_singleton]
+    · simp only [ne_eq, reduceCtorEq, not_false_eq_true, min_eq_get_min?,
+      List.min?_cons (α := Int), Option.get_some, length_cons, Int.natCast_add, Int.cast_ofNat_Int,
+      forall_const] at ih ⊢
+      rw [Int.mul_add, Int.mul_one, Int.add_comm]
+      apply Int.add_le_add
+      · apply Int.min_le_left
+      · refine Int.le_trans ?_ ih
+        rw [Int.mul_le_mul_right (by omega)]
+        apply Int.min_le_right
+
+theorem mul_length_le_sum_of_min?_eq_some_int {xs : List Int} (h : xs.min? = some x) :
+    x * xs.length ≤ xs.sum := by
+  cases xs
+  · simp_all
+  · simp only [min?_eq_some_min (cons_ne_nil _ _), Option.some.injEq] at h
+    simpa [← h] using min_mul_length_le_sum_int _
+
+theorem min_le_sum_div_length_int {xs : List Int} (h : xs ≠ []) :
+    xs.min h ≤ xs.sum / xs.length := by
+  have := min_mul_length_le_sum_int h
+  rwa [Int.le_ediv_iff_mul_le]
+  simp [List.length_pos_iff, h]
+
+theorem le_sum_div_length_of_min?_eq_some_int {xs : List Int} (h : xs.min? = some x) :
+    x ≤ xs.sum / xs.length := by
+  cases xs
+  · simp_all
+  · simp only [min?_eq_some_min (cons_ne_nil _ _), Option.some.injEq] at h
+    simpa [← h] using min_le_sum_div_length_int _
+
+theorem sum_le_max_mul_length_int {xs : List Int} (h : xs ≠ []) :
+    xs.sum ≤ xs.max h * xs.length := by
+  induction xs
+  · contradiction
+  · rename_i x xs ih
+    cases xs
+    · simp_all [List.max_singleton]
+    · simp only [ne_eq, reduceCtorEq, not_false_eq_true, max_eq_get_max?,
+      List.max?_cons (α := Int), Option.get_some, length_cons, Int.natCast_add, Int.cast_ofNat_Int,
+      forall_const] at ih ⊢
+      rw [Int.mul_add, Int.mul_one, Int.add_comm]
+      apply Int.add_le_add
+      · apply Int.le_max_left
+      · refine Int.le_trans ih ?_
+        rw [Int.mul_le_mul_right (by omega)]
+        apply Int.le_max_right
+
+theorem sum_le_max_mul_length_of_max?_eq_some_int {xs : List Int} (h : xs.max? = some x) :
+    xs.sum ≤ x * xs.length := by
+  cases xs
+  · simp_all
+  · simp only [max?_eq_some_max (cons_ne_nil _ _), Option.some.injEq] at h
+    simpa [← h] using sum_le_max_mul_length_int _
+
+theorem sum_div_length_le_max_int {xs : List Int} (h : xs ≠ []) :
+    xs.sum / xs.length ≤ xs.max h := by
+  have := sum_le_max_mul_length_int h
+  rw [Int.ediv_le_iff_le_mul]
+  · refine Int.lt_of_le_of_lt this ?_
+    apply Int.lt_add_of_pos_right
+    simp [← Nat.ne_zero_iff_zero_lt, h]
+  · simp [List.length_pos_iff, h]
+
+theorem sum_div_length_le_max_of_max?_eq_some_int {xs : List Int} (h : xs.max? = some x) :
+    xs.sum / xs.length ≤ x := by
+  cases xs
+  · simp_all
+  · simp only [max?_eq_some_max (cons_ne_nil _ _), Option.some.injEq] at h
+    simpa [← h] using sum_div_length_le_max_int _
+
+end List

src/Init/Data/List/Lemmas.lean

@@ -1826,13 +1826,16 @@ theorem append_eq_map_iff {f : α → β} :
     L₁ ++ L₂ = map f l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂ := by
   rw [eq_comm, map_eq_append_iff]
 
-@[simp, grind =]
-theorem sum_append_nat {l₁ l₂ : List Nat} : (l₁ ++ l₂).sum = l₁.sum + l₂.sum := by
-  induction l₁ generalizing l₂ <;> simp_all [Nat.add_assoc]
+theorem sum_append [Add α] [Zero α] [Std.LawfulLeftIdentity (α := α) (· + ·) 0]
+    [Std.Associative (α := α) (· + ·)] {l₁ l₂ : List α} : (l₁ ++ l₂).sum = l₁.sum + l₂.sum := by
+  induction l₁ generalizing l₂ <;> simp_all [Std.Associative.assoc, Std.LawfulLeftIdentity.left_id]
 
-@[simp, grind =]
-theorem sum_reverse_nat (xs : List Nat) : xs.reverse.sum = xs.sum := by
-  induction xs <;> simp_all [Nat.add_comm]
+theorem sum_reverse [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
+    [Std.Commutative (α := α) (· + ·)]
+    [Std.LawfulLeftIdentity (α := α) (· + ·) 0] (xs : List α) : xs.reverse.sum = xs.sum := by
+  induction xs <;>
+    simp_all [sum_append, Std.Commutative.comm (α := α) _ 0,
+      Std.LawfulLeftIdentity.left_id, Std.Commutative.comm]
 
 /-! ### concat
 
@@ -2363,9 +2366,6 @@ theorem replicateRecOn {α : Type _} {p : List α → Prop} (l : List α)
     exact hi _ _ _ _ h hn (replicateRecOn (b :: l') h0 hr hi)
 termination_by l.length
 
-@[simp] theorem sum_replicate_nat {n : Nat} {a : Nat} : (replicate n a).sum = n * a := by
-  induction n <;> simp_all [replicate_succ, Nat.add_mul, Nat.add_comm]
-
 /-! ### reverse -/
 
 @[simp, grind =] theorem length_reverse {as : List α} : (as.reverse).length = as.length := by

src/Init/Data/List/MinMax.lean

@@ -168,6 +168,10 @@ theorem min_eq_get_min? [Min α] : (l : List α) → (hl : l ≠ []) →
     l.min hl = l.min?.get (isSome_min?_of_ne_nil hl)
   | a::as, _ => by simp [List.min, List.min?_cons']
 
+theorem min_singleton [Min α] {x : α} :
+    [x].min (cons_ne_nil _ _) = x := by
+  simp [List.min]
+
 theorem min_eq_head {α : Type u} [Min α] {l : List α} (hl : l ≠ [])
     (h : l.Pairwise (fun a b => min a b = a)) : l.min hl = l.head hl := by
   apply Option.some.inj
@@ -182,6 +186,7 @@ theorem min_le_of_mem [Min α] [LE α] [Std.IsLinearOrder α] [Std.LawfulOrderMi
     l.min (ne_nil_of_mem ha) ≤ a :=
   (min?_eq_some_iff.mp (min?_eq_some_min (List.ne_nil_of_mem ha))).right a ha
 
+@[grind =]
 protected theorem le_min_iff [Min α] [LE α] [LawfulOrderInf α]
     {l : List α} (hl : l ≠ []) : ∀ {x}, x ≤ l.min hl ↔ ∀ b, b ∈ l → x ≤ b :=
   le_min?_iff (min?_eq_some_min hl)
@@ -354,6 +359,10 @@ theorem max_eq_get_max? [Max α] : (l : List α) → (hl : l ≠ []) →
     l.max hl = l.max?.get (isSome_max?_of_ne_nil hl)
   | a::as, _ => by simp [List.max, List.max?_cons']
 
+theorem max_singleton [Max α] {x : α} :
+    [x].max (cons_ne_nil _ _) = x := by
+  simp [List.max]
+
 theorem max_eq_head {α : Type u} [Max α] {l : List α} (hl : l ≠ [])
     (h : l.Pairwise (fun a b => max a b = a)) : l.max hl = l.head hl := by
   apply Option.some.inj
@@ -363,6 +372,7 @@ theorem max_eq_head {α : Type u} [Max α] {l : List α} (hl : l ≠ [])
 theorem max_mem [Max α] [MaxEqOr α] {l : List α} (hl : l ≠ []) : l.max hl ∈ l :=
   max?_mem (max?_eq_some_max hl)
 
+@[grind =]
 protected theorem max_le_iff [Max α] [LE α] [LawfulOrderSup α]
     {l : List α} (hl : l ≠ []) : ∀ {x}, l.max hl ≤ x ↔ ∀ b, b ∈ l → b ≤ x :=
   max?_le_iff (max?_eq_some_max hl)

src/Init/Data/List/Nat.lean

@@ -12,6 +12,7 @@ public import Init.Data.List.Nat.Range
 public import Init.Data.List.Nat.Sublist
 public import Init.Data.List.Nat.TakeDrop
 public import Init.Data.List.Nat.Count
+public import Init.Data.List.Nat.Sum
 public import Init.Data.List.Nat.Erase
 public import Init.Data.List.Nat.Find
 public import Init.Data.List.Nat.BEq

src/Init/Data/List/Nat/Find.lean

@@ -13,13 +13,6 @@ public section
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
-protected theorem Nat.sum_pos_iff_exists_pos {l : List Nat} : 0 < l.sum ↔ ∃ x ∈ l, 0 < x := by
-  induction l with
-  | nil => simp
-  | cons x xs ih =>
-    simp [← ih]
-    omega
-
 namespace List
 
 open Nat