Kevin might not care, but I care more about building the foundation for future proofs and human understanding than I do about this particular result.

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.