mathlib
601d5b13 - feat(tactic/simp_rw): add `simp_rw` tactic, a mix of `simp` and `rw` (#1900)

Commit
6 years ago
feat(tactic/simp_rw): add `simp_rw` tactic, a mix of `simp` and `rw` (#1900) * add `simp_rw` tactic that is a mix of `simp` and `rw` * Style fixes * Module documentation for the file `tactic/simp_rw.lean` * Apply suggestions to improve documentation of `simp_rw` * Documentation and tests for `simp_rw [...] at ...` Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Author
Committer
Parents
Loading