Commit 2025-03-11 14:35 7d2195a2
View on Github →perf: delete redundant instances with weak discrimination keys (#22780)
As @eric-wieser pointed out, these are redundant with X.of being reducible now. Their weak keys cause Lean to engage on wild goose instance synthesis paths.