mathlib3

c955537e - fix(library_search): only unfold reducible definitions when matching (#3038)

fix(library_search): only unfold reducible definitions when matching (#3038) By default `library_search` only unfolds `reducible` definitions when attempting to match lemmas against the goal. Previously, it would unfold most definitions, sometimes giving surprising answers, or slow answers. The old behaviour is still available via `library_search!`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>