Commit 2025-08-03 09:01 bfd0ab2f
View on Github →chore: remove redundant arguments to grind (#27884)
This PR cleans up some grind uses that have redundant arguments.
I observed that on the one hand new lemmas are getting tagged with @[grind], and on the other hand grind is already being used to golf proofs using the same lemmas. Hence this PR.