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

---