You can search for any object declared in Mathlib and Lean, including theorems, functions, types, syntax, tactics, and metaprogramming functions.
The neural network sees the name, type, file location, and comment of a declaration. Your search terms should match these as closely as possible.
You can find README.md and the code I used in the Files tab. Thank you!