feat: ∑ x ∈ s, f x to replace ∑ x in s, f x in the future (#6795)

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](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.E2.88.91.20x.20.E2.88.88.20s.2C.20f.20x.20instead.20of.20.E2.88.91.20x.20in.20s.2C.20f.20x/near/387352818) and [here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Destruction.20and.20big.20operators/near/387366894)



Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>