priority of instSMulOfMul

Stream: lean4

[Kevin Buzzard]

What is the logic for why docs#instSMulOfMul has priority less than 1000 (it's 910 in core)?

In Mathlib PR #34077 I made a copy of the instance with priority 1100 and it gives a 290G instruction speedup in mathlib; one file gets substantially slower but that's because that file has a declaration which is borked because of lean4#12102 ; the hack #34088 which works around this issue, in tandem with #34077, gives a saving in mathlib of 463.2G (see here ).

My argument for making the priority > 1000 in mathlib is "this instance is essentially always the right one when it applies, and is essentially always quick to fail when it isn't". Does this also apply to core and other applications? I am unclear about what the counterargument is, but presumably the instance is at 910 for a reason.

I write more about my thoughts here.

[Bryan Gin-ge Chen]

Looks like the instance was added in this commit with a priority of 910. Maybe @Kim Morrison remembers why?