This file sets up a tactic called
which is subsequently used throughout the category theory library
auto_param to discharge easy proof obligations when building structures.
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