feat(Tactic): erw tries rw first and warns if that succeeds

[Vierkantor]

This PR adds a macro rule to the erw tactic that first tries rw at reducible transparency, and displays a "Try this:" if that succeeded. This should help us get rid of uselessly slow erws.

This is a relatively simple implementation that does not verify if erw and rw would have resulted in the same exact rewrite. So it is possible that erw and rw both succeed but rewrite different occurrences, and there would be a suggestion to replace erw with rw in that case. I think the complication of running both at the same time and checking the goal state afterwards doesn't weigh up to accepting that this happens and adding an explanation to the warning generated by erw.

I import the erw extension in Tactic.Common: it might be nice to migrate this up even earlier in the import hierarchy but Mathlib.Tactic.TryThis is a somewhat heavy import to put in Mathlib.Tactic.Core.

Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Fixing.20the.20.60erw.60.20hell.20around.20concrete.20categories

---

• depends on: [Merged by Bors] - chore: clean up after #17615 #17617
• depends on: [Merged by Bors] - chore(*): replace erw with rw where possible #17703

[github-actions]

PR summary af3c28c713

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.Common	244	246	+2 (+0.82%)
Mathlib.CategoryTheory.Shift.Basic	445	447	+2 (+0.45%)
Mathlib.CategoryTheory.Limits.Shapes.Reflexive	556	558	+2 (+0.36%)
Mathlib.Topology.Order.ScottTopology	671	673	+2 (+0.30%)

Import changes for all files

Files	Import difference
There are 4319 files with changed transitive imports taking up over 182543 characters: this is too many to display!
You can run scripts/import_trans_difference.sh all locally to see the whole output.

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[grunweg]

Thanks for this PR! I'm (perhaps needlessly so) worries about the performance effects of this change. Can you benchmark this/is the speedcenter up and working already?
Or is the idea that this will reduce slow erw's over time, and hence be worth it even if it's a small slow-down?

[Vierkantor]

Thanks for this PR! I'm (perhaps needlessly so) worries about the performance effects of this change. Can you benchmark this/is the speedcenter up and working already? Or is the idea that this will reduce slow erw's over time, and hence be worth it even if it's a small slow-down?

Unfortunately the speedcenter was still down yesterday, and I don't see any movement in the zulip thread. I agree that this will make Mathlib a bit slower, but the extra cost of doing a rw in addition to erw should make that cost somewhat marginal. And removing erws definitely makes up for that. And even if it weren't about speed, then simply cleaning up erws that don't need to be erw is nice for code clarity.

[grunweg]

Two nits about outdated comments - otherwise the erw -> rw replacements look good to me. The macro looks plausible to me, but I'm not an expert on them - that's a low-confidence approval of that part.

[Vierkantor]

Two nits about outdated comments

Nicely spotted, thanks!

[kim-em]

Lets split this into separate PRs for changing proofs and for the macro.

[kim-em]

I would prefer a solution where we only run the extra check in CI, like we do for says.

[Vierkantor]

Lets split this into separate PRs for changing proofs and for the macro.

See #17703 for only the changed proofs.

[grunweg]

I'm curious about the overall balance of this PR, thus let me bench it.

[grunweg]

!bench

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - chore: clean up after #17615 #17617
• [Merged by Bors] - chore(*): replace erw with rw where possible #17703
  By Dependent Issues (🤖). Happy coding!

[leanprover-bot]

Here are the benchmark results for commit edc1e5c.
There were significant changes against commit 626e646:

  Benchmark                                                  Metric         Change
  ================================================================================
- ~Mathlib.Algebra.Module.LocalizedModule                    instructions     8.2%
- ~Mathlib.CategoryTheory.Adjunction.Lifting.Right           instructions    46.6%
- ~Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing       instructions    15.4%
- ~Mathlib.RepresentationTheory.GroupCohomology.Resolution   instructions     8.1%

[grunweg]

The previous PR was performance-neutral - so the benchmark should mostly represent the effect of this PR. Overall, there is a slowdown of 200*10⁹ instruction (about 0.1-0.2% of all of mathlib).

[Vierkantor]

I'll hold off on merging this PR then, running it manually every so often until the number of erws is more manageable.