[Merged by Bors] - feat(Data/Nat/Choose): Add sum_range_multichoose by metakunt · Pull Request #33656 · leanprover-community/mathlib4

metakunt · 2026-01-06T06:53:06Z

No description provided.

github-actions · 2026-01-06T06:54:17Z

PR summary 15f6691e7a

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ sum_range_multichoose

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

eric-wieser · 2026-01-06T12:27:39Z

Mathlib/Data/Nat/Choose/Sum.lean

+  apply Finset.sum_bij' (fun x _ => x + (k - 1)) (fun x _ => x - (k - 1))
+      (by grind) (by grind) (by grind) (by grind)
+  intro x
+  have _ := choose_symm (k := k - 1) (n := x + (k - 1)) (by lia)
+  grind


I think you could simplify this slightly by adding the Nat version of Int.Icc_eq_finset_map?

I'm afraid I don't understand what you mean by that.

Do you want me to add the Nat version of that https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Int/Interval.html#Int.Icc_eq_finset_map
That would then be Nat.Icc_eq_finset_map?

Yes, exactly! Then you could skip the bij step in this proof

Sooo, after a few hours I've managed to prove both results in a different way.

open Finset Nat in lemma Nat.Icc_eq_finset_map (a b : ℕ) : Icc a b = (Finset.range (b + 1 - a)).map (Nat.castEmbedding.trans <| addLeftEmbedding a) := by ext x simp only [mem_Icc, mem_map, mem_range, Function.Embedding.trans_apply, castEmbedding_apply, cast_id, addLeftEmbedding_apply] constructor · intro h use x - a grind · grind open Nat in lemma sum_range_multichoose (n k : ℕ) (h : k ≠ 0) : ∑ i ∈ Finset.range (n + 1), k.multichoose i = (n + k).choose k := by have h1 : k - 1 + 1 = k := by lia have h2 : n + (k - 1) + 1 = n + k := by lia simp only [← h1 ▸ h2 ▸ (sum_Icc_choose (n + (k - 1)) (k - 1)), multichoose_eq, range_eq_Ico] conv_lhs => rhs; intro x rw [← choose_symm (by grind), Nat.sub_right_comm, Nat.add_sub_cancel_right, add_comm, Nat.add_sub_assoc (by grind)] convert (sum_map (Ico 0 (n + 1)) (addRightEmbedding (k - 1)) (·.choose (k - 1))).symm using 2 rw [map_add_right_Ico, zero_add, add_right_comm, Ico_add_one_right_eq_Icc]

however I'm completely out of my element in trying to find the most "mathlibby" version of the proof.

It appears that I'm doing something wrong and I don't know what. This new version seems more cumbersome to prove as I can't just grind the hyps away. I have to do a lot of targeted rewrites under conv binders, which by itself is really nasty, just to get the embedding version to apply correctly.

Thank you @metakunt for taking the time to investigate this!

I've poked a bit and also don't understand how this would be a simplification.

Overall, I don't think it matters that much anyways. The theorem looks good and is in a reasonable place IMO

I suggest

maintainer merge

I think the Nat.Icc_eq_finset_map lemma is still a good one to have.

I can add it in the next PR. Could you also suggest a file for that? It doesn't fit in Data/Int/Interval and Data/Nat/Interval does not exist.

Nevermind, https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Interval/Finset/Nat.html exists.

Finding the correct theorems/files in Mathlib is truly a work of art.

Indeed putting it in a new PR makes sense!

github-actions · 2026-01-17T12:23:47Z

🚀 Pull request has been placed on the maintainer queue by joneugster.

Mathlib/Data/Nat/Choose/Sum.lean

Co-authored-by: Bhavik Mehta <[email protected]>

metakunt · 2026-01-19T10:12:41Z

@b-mehta I'd have never come up with that golf. That's seriously impressive.
Regarding the pattern simp only [← h1 ▸ h2 ▸ (sum_Icc_choose (n + (k - 1)) (k - 1)), what would you prefer instead so that I can consider this for my future PR's?

ocfnash · 2026-01-21T15:40:13Z

@b-mehta I'd have never come up with that golf. That's seriously impressive. Regarding the pattern simp only [← h1 ▸ h2 ▸ (sum_Icc_choose (n + (k - 1)) (k - 1)), what would you prefer instead so that I can consider this for my future PR's?

I can't speak for Bhavik but I would say:

Try to avoid using ▸: usually, though not always, there is a better option (often just an earlier rw or subst)
Try not to compound too many actions together, fewer characters is not something we value
Study other proofs in Mathlib to learn the sort of style we like

ocfnash · 2026-01-21T15:42:10Z

bors merge

mathlib-bors · 2026-01-21T17:08:23Z

Pull request successfully merged into master.

Build succeeded:

b-mehta · 2026-01-21T20:16:40Z

Oliver is correct, and I'd add that when reading h1 ▸ h2 ▸ (sum_Icc_choose (n + (k - 1)) (k - 1)), it's pretty hard to intuit which statement is actually sent to simp only here. For a local change, I would have suggested making a have statement for this with an explicit type ascription, and giving a proof using rw of h1, h2, sum_Icc_choose (n + (k - 1)) (k - 1) (perhaps this have would have had a clean grind proof too)

…y#33656)

metakunt and others added 2 commits January 6, 2026 07:51

Add sum_range_multichoose

fbd3f3c

Merge branch 'master' into sum_range_multichoose

0de9c6a

github-actions bot added the t-data Data (lists, quotients, numbers, etc) label Jan 6, 2026

eric-wieser reviewed Jan 6, 2026

View reviewed changes

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 17, 2026

leanprover-community deleted a comment from github-actions bot Jan 17, 2026

b-mehta requested changes Jan 19, 2026

View reviewed changes

Mathlib/Data/Nat/Choose/Sum.lean Outdated Show resolved Hide resolved

jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 19, 2026

Update Mathlib/Data/Nat/Choose/Sum.lean

d0fa930

Co-authored-by: Bhavik Mehta <[email protected]>

metakunt removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 19, 2026

eric-wieser requested a review from b-mehta January 19, 2026 18:46

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Jan 21, 2026

mathlib-bors bot pushed a commit that referenced this pull request Jan 21, 2026

feat(Data/Nat/Choose): Add sum_range_multichoose (#33656)

8e016c1

mathlib-bors bot changed the title ~~feat(Data/Nat/Choose): Add sum_range_multichoose~~ [Merged by Bors] - feat(Data/Nat/Choose): Add sum_range_multichoose Jan 21, 2026

mathlib-bors bot closed this Jan 21, 2026

goliath-klein pushed a commit to PrParadoxy/mathlib4 that referenced this pull request Jan 24, 2026

feat(Data/Nat/Choose): Add sum_range_multichoose (leanprover-communit…

b90b375

…y#33656)

metakunt mentioned this pull request Mar 29, 2026

feat(NumberTheory/AKSPrimality): Adds the AKS primality test #34507

Open

Conversation

metakunt commented Jan 6, 2026 • edited by mathlib-bors bot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jan 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 15f6691e7a

Import changes for modified files

Declarations diff

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Jan 17, 2026

Uh oh!

Uh oh!

metakunt commented Jan 19, 2026

Uh oh!

ocfnash commented Jan 21, 2026

Uh oh!

ocfnash commented Jan 21, 2026

Uh oh!

mathlib-bors bot commented Jan 21, 2026

Uh oh!

b-mehta commented Jan 21, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

metakunt commented Jan 6, 2026 •

edited by mathlib-bors bot

Loading

github-actions bot commented Jan 6, 2026 •

edited

Loading