Commit 2023-05-10 05:52 f2c85c3b
View on Github →feat: rewrites, a tactic to suggest rewrites. (#3119)
Unlike the very slow rw_hint long ago proposed (but never merged) for mathlib3, this uses discrimination trees (with keys given by LHS and RHS of lemmas), and looks up all subexpressions of the target expression.
