[Merged by Bors] - refactor: use the typeclass SProd to implement overloaded notation · ×ˢ ·

[Komyyy]

Currently, the following notations are changed from · ×ˢ · because Lean 4 can't deal with ambiguous notations.

Definition	Notation
Finset.product	· ×ᶠ ·
LowerSet.prod	· ×ˡˢ ·
UpperSet.prod	· ×ᵘˢ ·

And following notations were still · ×ˢ · but they causes performance issues; even timeouts.

Definition	Notation
Set.prod	· ×ˢ ·
List.product	· ×ˢ ·
Multiset.product	· ×ˢ ·

This PR makes the new typeclass SProd to implement overloaded notation · ×ˢ ·, and revert changed notations.
Also, this PR changes the notation of Filter.prod from · ×ᶠ · to · ×ˢ ·.

---

• depends on: [Merged by Bors] - feat: fbinop% term elaborator to support set product notation #4308

[ChrisHughes24]

I'm very happy with these changes, but they're quite sweeping so I'll let somebody else have an opinion as well.

[kmill]

I'm happy with these changes too. I know I had some reservations on Zulip, but I reviewed all the changes in closer detail and they're all improvements, so I say we go ahead.

Want to put it back at awaiting-review @Komyyy ? Like Chris the changes are quite sweeping and I'd like someone else to look at it (I'm fine with Chris deciding to merge it).

[semorrison]

bors d+

[bors]

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

[Komyyy]

bors r+

[urkud]

Historical remark: I introduced a similar typeclass in leanprover-community/mathlib#11300, then @YaelDillies replaced it with overlapping notations in leanprover-community/mathlib#15717 because it worked better in Lean 3.

[bors]

Merge conflict.

[ChrisHughes24]

bors r+

[kmill]

@urkud To add to the historical remark: one thing that is different now from then is that instances of this SProd class make use of a custom fbinop% elaborator that give us similar benefits to the Lean 3 overlapping notations despite being a class-based design. (I pinged you and Yaël earlier in this thread to show a line that couldn't work with a Lean 3 class, but could work with Lean 3 overlapping notation, and now still works with Lean 4 classes.)

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style