feat: lemmas about sums of lists/arrays/vectors

[datokrat]

This PR provides more lemmas about sums of lists/arrays/vectors, especially sums of Nat or Int lists/arrays/vectors.

This change has been motivated by my experience solving human-eval-lean problems. Sums, minima and maxima are frequently required and the improvements provided in this PR make it easier to verify such programming tasks.

Changes:

• Added lemmas that sum equals foldl/foldr.
• Generalized sum_append_nat and sum_reverse_nat lemmas so that they are polymorphic, requiring only some type class instances about the list elements' type. The polymorphic lemmas aren't simp- or grind-annotated because I fear the instance synthesis overhead. However, the Nat and Int specializations are annotated (see below). Note that as {Array,Vector}.min do not exist, some lemmas can't be stated and were omitted.
• Added List.min_singleton and List.max_singleton lemmas as they were needed for some proofs.
• Nat-related:
  • Moved all {List,Array,Vector}.sum lemmas that are specific for Nat into their own module: Init.Data.List.Nat.Sum, Init.Data.Array.Nat and Int.Data.Vector.Nat.
  • Notably, moved Nat.sum_pos_iff_exists_pos and renamed it to List.sum_pos_iff_exists_pos_nat. This is more consistent and made it possible to add Array and Vector variants of this lemma.
  • Added lemmas proving that l.sum / l.length lies between the minimum and the maximum of a list.
• Added analogous lemmas for Int lists/arrays/vectors to parallel modules: Init.Data.List.Int.Sum, Init.Data.Array.Int and Int.Data.Vector.Int.
• Renamed sum_eq_sum_toList to sum_toList, which better represents the theorem's content.

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-01-12 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-01-13 19:07:37)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-01-28 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-01-29 14:35:34)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-01-30 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-01-30 12:13:56)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase c7a9a4e18c2c1defa4261b852f38f6d67f18eb1c --onto 42a0e9245300da6b3d971fa0033d726bb8e11cc3. You can force reference manual CI using the force-manual-ci label. (2026-02-01 20:44:11)

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-11994 has successfully built against this PR. (2026-01-13 20:25:19) View Log
• 💥 Mathlib branch lean-pr-testing-11994 build failed against this PR. (2026-01-15 14:59:37) View Log
• 💥 Mathlib branch lean-pr-testing-11994 build failed against this PR. (2026-01-15 16:14:10) View Log
• 💥 Mathlib branch lean-pr-testing-11994 build failed against this PR. (2026-01-15 17:49:25) View Log
• ✅ Mathlib branch lean-pr-testing-11994 has successfully built against this PR. (2026-01-16 14:12:15) View Log
• ✅ Mathlib branch lean-pr-testing-11994 has successfully built against this PR. (2026-01-16 15:46:48) View Log
• ✅ Mathlib branch lean-pr-testing-11994 has successfully built against this PR. (2026-01-29 15:40:25) View Log
• ✅ Mathlib branch lean-pr-testing-11994 has successfully built against this PR. (2026-01-30 08:57:52) View Log
• ✅ Mathlib branch lean-pr-testing-11994 has successfully built against this PR. (2026-01-30 13:19:26) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c7a9a4e18c2c1defa4261b852f38f6d67f18eb1c --onto d1514f3cecc4139039962137fcf3a84c9459194a. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-01 20:44:09)

[datokrat]

!radar

[leanprover-radar]

Benchmark results for 75e46e1 against e56351d are in! @datokrat

Warnings (2)

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

• Runner for run build has different system configurations between commits.
• Runner for run other has different system configurations between commits.

Small changes (2✅, 10🟥)

• 🟥 build/module/Init.Data.Array.Lemmas//instructions: +239.0M (+0.3%)
• 🟥 build/module/Init.Data.Array.OfFn//instructions: +119.5M (+5.0%) (reduced significance based on *//lines)
• 🟥 build/module/Init.Data.List.Count//instructions: +68.7M (+1.8%) (reduced significance based on *//lines)
• 🟥 build/module/Init.Data.List.Lemmas//instructions: +657.7M (+1.3%) (reduced significance based on *//lines)
• 🟥 build/module/Init.Data.List.MinMax//instructions: +61.8M (+1.5%)
• 🟥 build/module/Init.Data.List.Nat.Find//instructions: +123.3M (+7.4%) (reduced significance based on *//lines)
• 🟥 build/module/Init.Data.Nat.Div.Lemmas//instructions: +420.3M (+8.1%) (reduced significance based on *//lines)
• 🟥 build/module/Init.Data.Vector.Lemmas//instructions: +405.1M (+0.7%) (reduced significance based on *//lines)
• 🟥 build/module/Init.Data.Vector.OfFn//instructions: +93.3M (+1.4%) (reduced significance based on *//lines)
• ✅ build/module/Lake.CLI//instructions: -16.4M (-2.1%)
• ✅ build/module/Lean.Elab.Tactic.Congr//instructions: -21.1M (-2.0%)
• 🟥 bv_decide_large_aig.lean//instructions: +194.4M (+0.4%)

[kim-em]

I think it would be worthwhile to leave a comment here explaining why you haven't labelled these as simp, grind =, but only done this on the specializations.

In fact, even better would be to benchmark this against Mathlib, with and without annotations on the generic version. I suspect it is actually fine. (Perhaps not even that much work given our new infrastructure?)

[datokrat]

I've annotated sum_append and sum_reverse instead now, I think the benchmark turned out neutral (as long as 0.5% on build//instructions and no other significant changes is natural variability...)

[datokrat]

!bench mathlib

[leanprover-radar]

Benchmark results for leanprover-community/mathlib4-nightly-testing@2975ae5 against leanprover-community/mathlib4-nightly-testing@e0bf30b are in! @datokrat

• 🟥 main exited with code 1

No significant changes detected.

[datokrat]

!bench mathlib

[leanprover-radar]

Benchmark results for leanprover-community/mathlib4-nightly-testing@074ad7a against leanprover-community/mathlib4-nightly-testing@e0bf30b are in! @datokrat

• build//instructions: +93.3G (+0.05%)

No significant changes detected.