feat(tactic/equiv_rw): rewriting along equivalences (#2246)
* feat(tactic): rewriting along equivalences
* header
* minor
* type
* actually, rewriting the goal under functors is easy
* rewriting inside function types
* more
* way better
* improving comments
* fun
* feat(data/equiv): pi_congr
* various
* feat(data/equiv): sigma_congr
* docstrings
* change case for consistency
* tidying up
* minor
* minor
* switching names
* fixes
* add some tracing routines for convenience
* feat(tactic/core): trace_for
* typo
* oops
* oops
* various
* chore(tactic/solve_by_elim): cleanup
* cleanup
* what happened to my commit?
* fix
* fix
* rename to trace_if_enabled
* fixed?
* Tweak comments
* feat(tactic/solve_by_elim): add accept parameter to prune tree search
* when called with empty lemmas, use the same default set as the interactive tactic
* trace_state_if_enabled
* Update src/data/equiv/basic.lean
* implicit arguments
* stop cheating with [] ~ none
* indenting
* yay, working via solve_by_elim
* pretty good
* various
* various
* docstring
* fix docstrings
* more docs
* docs
* feat(data/equiv/functor): bifunctor.map_equiv
* bifunctors
* test rewriting under unique
* rewriting in subtypes
* add documentation, and make the function an explicit argument
* documentation
* fix doc-strings
* typos
* minor
* adding demonstration of transporting semigroup
* Update .vscode/settings.json
* err
* trying to transport through monoid
* err?
* much better
* improve documentation of accept, and add doc-string
* fix duplicated namespace
* improve docs
* try again with documentation
* update
* oops
* rename adapt_equiv
* simplify the equivalence produced, and provide a tactic to access the equivalence
* add max_steps option
* add decl_name to add_tactic_doc
* fix add_tactic_doc
* satisfying linter
* add defaults for cfg arguments
* remove simplify_term, which already existed as expr.simp
* remove duplicate functions that have been PRd separately
* no need for accept
* Update src/tactic/equiv_rw.lean
Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com>
* Update src/tactic/equiv_rw.lean
Co-Authored-By: Gabriel Ebner <gebner@gebner.org>
* replace max_steps with max_depth
* use solve_aux
* add missing simp lemmas about arrow_congr'
* fix failing test, by making sure we don't leave any ≃ goals on the table
* add comment
* comment out trace output
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
