Commit 2025-10-21 12:12 b758e765
View on Github →chore: remove redundant fields from instances (#30734)
This PR removes all occurrences of patterns like mul := (· * ·) in definitions of instances. These patterns are unneccessary, and sometimes they cause the instance to behave inefficiently during unification.
I have no idea why these patterns were there in the first place. Maybe it was a Lean3 thing?
As a result, we get a pretty good speedup: 0.63% less instructions.