Commit 2025-03-31 05:22 a3041c41

chore(*): replace @[simp, nolint simpNF] with @[simp high] for specialized lemmas (#23261) These are specialized lemmas and should therefore apply faster than the more general lemmas introduced later (which need to look for typeclass instances). If we raise their simp priority, we can remove the simpNF annotation. On the other hand, simp? output will look more ugly... Since simp now prefers lemmas declared lower down in the hierarchy, it looks like we can get in a bit of shaking! From the "specialized high priority simp lemma" library note:

It sometimes happens that a `@[simp]` lemma declared early in the library can be proved by `simp`
using later, more general simp lemmas. In that case, the following reasons might be arguments for
the early lemma to be tagged `@[simp high]` (rather than `@[simp, nolint simpNF]` or
un``@[simp]``ed):
1. There is a significant portion of the library which needs the early lemma to be available via
  `simp` and which doesn't have access to the more general lemmas.
2. The more general lemmas have more complicated typeclass assumptions, causing rewrites with them
  to be slower.