This PR goes through the diff of #17615, which automatically replaced `erw` with `rw`) to clean up as follows:
 * delete obsolote comments
 * merge adjacent `rw` calls
 * restore old code that broke at some point but now works again

This is an automatically generated PR, replacing 259 `erw` calls with `rw` for free. I'm working on a follow-up that manually deals with the context around these `erw`s: deleting now-useless comments about `erw` and merging adjacent `rw` calls into one. Keeping the automatically generated changes apart from the manual ones should help with reviewing.

# How to reproduce this PR

Check out the branch `erw-to-rw-setup`. Run the command
```bash
lake build | grep '^info:' | awk -F ":" '{ print "-i ‘.bak’ -e "$3"s/erw/rw/ "$2; }' | xargs -L 1 sed
```
and `git diff` should show you exactly the same modifications as in this PR.

# Technical details

In `Mathlib.Tactic.Core` I added the following rule to `erw`:
```lean
import Mathlib.Tactic.TryThis

/-- if we call `erw`, first try running regular `rw` and warn if that succeds. -/
macro_rules 
  | `(tactic| erw $s $(loc)?) =>
    `(tactic| try_this rw $(.none)? $s $(loc)?)
```
This makes `erw` display a "Try this:" message if `rw` would have succeeded as well. Beware that this does not mean that the file compiles just as well after doing the replacement, since a `rw` could succeed by rewriting a different term, so subsequent tactics fail. This is important for running the script!

With that edit in place, it's possible to run the script. This will parse the `lake build` output, looking for the lines produced by the macro rule, and replace `erw` with `rw` on the lines that it indicates. Note that it assumes there is at most one `erw` on one line; that was true at least when I ran the script.

This is an automatically generated PR, replacing 259 `erw` calls with `rw` for free. I'm working on a follow-up that manually deals with the context around these `erw`s: deleting now-useless comments about `erw` and merging adjacent `rw` calls into one. Keeping the automatically generated changes apart from the manual ones should help with reviewing.

# How to reproduce this PR

Check out the branch `erw-to-rw-setup`. Run the command
```bash
lake build | grep '^info:' | awk -F ":" '{ print "-i ‘.bak’ -e "$3"s/erw/rw/ "$2; }' | xargs -L 1 sed
```
and `git diff` should show you exactly the same modifications as in this PR.

# Technical details

In `Mathlib.Tactic.Core` I added the following rule to `erw`:
```lean
import Mathlib.Tactic.TryThis

/-- if we call `erw`, first try running regular `rw` and warn if that succeds. -/
macro_rules 
  | `(tactic| erw $s $(loc)?) =>
    `(tactic| try_this rw $(.none)? $s $(loc)?)
```
This makes `erw` display a "Try this:" message if `rw` would have succeeded as well. Beware that this does not mean that the file compiles just as well after doing the replacement, since a `rw` could succeed by rewriting a different term, so subsequent tactics fail. This is important for running the script!

With that edit in place, it's possible to run the script. This will parse the `lake build` output, looking for the lines produced by the macro rule, and replace `erw` with `rw` on the lines that it indicates. Note that it assumes there is at most one `erw` on one line; that was true at least when I ran the script.

This PR goes through the diff of #17615, which automatically replaced `erw` with `rw`) to clean up as follows:
 * delete obsolote comments
 * merge adjacent `rw` calls
 * restore old code that broke at some point but now works again

This PR goes through the diff of #17615, which automatically replaced `erw` with `rw`, to clean up as follows:
 * delete obsolote comments
 * merge adjacent `rw` calls
 * restore old code that was commented out when it broke at some point but now works again



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>