obviously tactic #
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
Implementation note #
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