There is a tactic (in Lean) called library_search. I'm not sure it's as smart as you'd like? But it is useful. https://leanprover-community.github.io/mathlib_d

There is a tactic (in Lean) called library_search. I'm not sure it's as smart as you'd like? But it is useful. https://leanprover-community.github.io/mathlib_docs/tactics.html#library_search https://leanprover-community.github.io/mathlib_docs/tactics....