Commit 2025-07-15 22:37 3a074087
View on Github →chore: import rw?? into Mathlib.Tactic.Common (#27164)
This PR makes rw?? available to use in most places inside of mathlib.
This also caught the problem that "all" was turned into a token accidentally.