feat: `∑ x ∈ s, f x` to replace `∑ x in s, f x` in the future

[kmill]

Adds new syntax for sum/product big operators for ∑ x ∈ s, f x. The set s can either be a Finset or a Set with a Fintype instance, in which case it is equivalent to ∑ x ∈ s.toFinset, f x.

Also supports ∑ (x ∈ s) (y ∈ t), f x y for Finset.sum (s ×ˢ t) (fun ⟨x, y⟩ ↦ f x y). Note that these are not dependent products at the moment.

Adds with clauses, so for example ∑ (x ∈ Finset.range 5) (y ∈ Finset.range 5) with x < y, x * y, which inserts a Finset.filter over the domain set.

Supports pattern matching in the variable position. This is by creating an experimental version of extBinder that uses term:max instead of binderIdent.

The new ∑ x ∈ s, f x notation is used in Algebra.BigOperators.Basic for illustration, but the old ∑ x in s, f x still works for backwards compatibility.

Zulip threads here and here

---

[kmill]

@YaelDillies I'm not so sure about this being the sum/prod notation, but I do support having some variant notation that constructs these (dependent) products for the domain.

In #7227 I've been working on a more flexible binder notation to upgrade all notation3 binders to have pattern matching etc. (and you can define your own binders!). Part of it is that ideally sum/prod notation uses it as well for consistency, which that PR succeeds in doing.

Potentially the variant notation could be a new binder type. Just making one up quick for sake of illustration, ∑ join% (x ∈ s) (y ∈ t), f x y could work with this system.

[YaelDillies]

What I really care about is the \sum ... with ..., ... notation. If that makes it easier to get in, would you mind opening a PR with just this change. Then I can copy it in LeanAPAP, check it works there, and subsequently send your PR on the merge queue.

[github-actions[bot]]

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

[fpvandoorn]

This looks very nice from a readability standpoint. Also, the reactions on Zulip are overwhelmingly positive. Am I correct that the current status of the delaboration is only that in is replaced by ∈?

@eric-wieser still had some reservations that he was planning to share (and I do worry a bit about the "can I rewrite the _ ∈ _?"), so please do. Otherwise I'll merge this in a few days.

[YaelDillies]

Yes, we are still the old elaborators here: https://github.com/leanprover-community/mathlib4/pull/6795/files#diff-daef0dcb628557383518bbc8aaabe4b289271a26e17ffd78ab3c1aae7ba1d3b2R201-R215

[eric-wieser]

@eric-wieser still had some reservations that he was planning to share (and I do worry a bit about the "can I rewrite the _ ∈ _?"), so please do. Otherwise I'll merge this in a few days.

I've shared these in the original zulip thread.

[fpvandoorn]

Ah, thanks for the link. I think we should merge this. The notation is a lot nicer, and it shouldn't be too bad for users to adapt to this.

bors d+ bors d=YaelDillies

[mathlib-bors[bot]]

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

[mathlib-bors[bot]]

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

[YaelDillies]

bors merge

[mathlib-bors[bot]]

:-1: Rejected by label

[YaelDillies]

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style