Comment by wyager

I believe Lean supports a signature search mechanism. E.g. Haskell has Hoogle, Lean has Loogle. So in many ways it's actually easier to search for "library" code than in most languages, because the type tells you everything you need to know and you don't need to care about the implementation.