In this file, we set up
obviously as a "replacer" tactic,
whose implementation can be modified after the fact.
Then we set the default implementation to be
At present we don't actually take advantage of the replacer mechanism in mathlib.
In the past it had been used by an external category theory library which wanted to incorporate
rewrite_search as part of