feat: ∑ hi : i ∈ s, f i hi syntax for big operators

[YaelDillies]

Define new notation for Finset.sum/Finset.prod. The main changes are

• ∑ hi : i ∈ s, f i hi as notation for ∑ i : s, f i.1 i.2
• ∑ hi : i ∈ s with p i, f i hi as notation for ∑ i : s.filter p, f i.1 (mem_filter.1 i.2).1
• ∑ i ∈ s with hpi : p i, f i hpi as notation for ∑ i : s.filter p, f i.1 (mem_filter.1 i.2).2
• ∑ hi : i ∈ s with hpi : p i, f i hi hpi as notation for ∑ i : s.filter p, f i.1 (mem_filter.1 i.2).1 (mem_filter.1 i.2).2

---

• depends on: [Merged by Bors] - feat: ∑ x ∈ s, f x to replace ∑ x in s, f x in the future #6795

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - feat: ∑ x ∈ s, f x to replace ∑ x in s, f x in the future #6795
  By Dependent Issues (🤖). Happy coding!

[eric-wieser]

I am very much not a fan of ∑ hi : i ∈ s, f i hi syntax, as it means something completely different from ∑ᶠ hi : i ∈ s, f i hi or ⨅ hi : i ∈ s, f i hi, which don't quantify over i at all.

[YaelDillies]

I am aware of this potential confusion, but consider the number of people wondering how to get access to hi : i ∈ s inside the sum. Zulip is full of such questions. I believe it's easier to explain a posteriori why ∑ᶠ hi : i ∈ s, f i hi means something different than why we can't do the same thing as for if i ∈ s then a else b.

Or maybe you would be happier with ∑ (hi : i ∈ s), f i hi?

[eric-wieser]

∑ i (hi : i ∈ s), f i hi (allowing type info on the i) would be ok with me, as this is similar enough to the behavior of binders in iInf, even if it doesn't actually generate nested sums.

[YaelDillies]

But iInf binders would rather be \iInf (hi : i \in s), ...?