Commit 2025-08-26 23:57 da5290c5
View on Github →chore: golf using grw (#26981)
This PR cleans up some proofs using grw. It also tags a few lemmas with @[gcongr] that were required for the proofs.
chore: golf using grw (#26981)
This PR cleans up some proofs using grw. It also tags a few lemmas with @[gcongr] that were required for the proofs.