Such a hoogle analogue exists! See moogle.ai.
6 karma · joined December 9, 2023
[citation needed]
I think there are many benefits. Hard to claim that your favourite one is the biggest benefit.
In general, I think it's a bit weird that you are repeatedly (also other HN threads, and sibling comments in this one) making unfounded claims about Lean/mathlib, to the point where you are telling maintainers how their system works. And if they explain that you are misunderstanding the system, you ignore their correction and bring up the next (or the same) unfounded claim.
Disclaimer: I am a Lean/mathlib user.