feat(data/nat/choose/multinomial): add multinomial theorem

[pimotte]

Proof by induction on the number of summands. finset.sym is used to sum over. It means we have access to the finset tooling to rewrite it, and it's one of the more direct ways of expressing it.

Co-authored-by: Junyan Xu [email protected]

---

• [ ] depends on: #16859
• [x] depends on: #16170 [multinomial defintions and basic lemma's]
• [x] depends on: #16316 [basic sym lemma's to support definition]
• [x] depends on: #16486

[pimotte]

Due to changes in #16316 this will need some changes and likely another PR dependency

[pimotte]

@kmill If you're up for it, maybe you could take a look at this one too? 😇

Couple remarks/questions:

• Is is a good practice to work with named projections instead of .1, .2? If yes, I'm happy to replace those.
• I guess there is some stuff that could be extracted out of the main proof, but I don't think the main blocks are great candidates for that and I don't really know how else to approach it.
• In making this compatible with the modified sym lemma's I changed some parts in the last bit of the main proof, so those are not as golfed as the parts by @alreadydone that I didn't touch:P

[alreadydone]

• I think using .1 and .2 for iff.mp/prod.fst and iff.mpr/prod.snd is intuitive and accepted practice.

• I've done the lemma extraction at my fork. I also switched some argument from explicit to implicit. Feel free to merge if you think they're good. I switched to a proof using finset.sum_bij' so the extracted lemmas are now about left/right inverse (which are stronger) instead of injectivity/surjectivity.

[alreadydone]

If @pimotte no longer has time for this PR, can I take over? Let's start by merging my fork, if there's no objection.

[pimotte]

If @pimotte no longer has time for this PR, can I take over? Let's start by merging my fork, if there's no objection.

Yeah, I'm currently otherwise occupied, feel free to take over:)

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib#16859~~
• ~~leanprover-community/mathlib#16170~~
• ~~leanprover-community/mathlib#16316~~
• ~~leanprover-community/mathlib#16486~~ By Dependent Issues (🤖). Happy coding!

[riccardobrasca]

bors d+

[bors[bot]]

:v: pimotte can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[pimotte]

bors r+

[bors[bot]]

This PR was included in a batch that was canceled, it will be automatically retried

[bors[bot]]

Build failed (retrying...):

• Run tests

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests