mathlib

9b797ee3 - feat(library_search): (efficiently) try calling symmetry before searching the library (#2415)

feat(library_search): (efficiently) try calling symmetry before searching the library (#2415) This fixes a gap in `library_search` we've known about for a long time: it misses lemmas stated "the other way round" than what you were looking for. This PR fixes that. I cache the `tactic_state` after calling `symmetry`, so it is only called once, regardless of how much of the library we're searching. When `library_search` was already succeeding, it should still succeed, with the same run time. When it was failing, it will now either succeed (because it found a lemma after calling `symmetry`), or fail (in the same time, if `symmetry` fails, or approximately twice the time, if `symmetry` succeeds). I think this is a reasonable time trade-off for better search results. Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>