Lean compiles its code to C, so it's pretty good on that end of the spectrum, though it does have a bit of a runtime, so it's certainly not at the very end of spectrum where Rust/C/C++ are (never used Go, so idk). With some optimization my personal experience is that it's not that bad to get it within a factor of 2-5 of half-decent rust speed. My personal mental model of it is like a more-to-my-tastes wildly-faster python but without an ecosystem.
As for library support, yeah it's definitely not a mature ecosystem. But since it compiles to C, the FFI is great, so you can just ask an LLM to write bindings to your favorite rust/C/C++ library and they do just fine. I recently wanted (apache) arrow bindings for lean, and LLMs knocked out perfectly sufficient bindings just fine.
As for library support, yeah it's definitely not a mature ecosystem. But since it compiles to C, the FFI is great, so you can just ask an LLM to write bindings to your favorite rust/C/C++ library and they do just fine. I recently wanted (apache) arrow bindings for lean, and LLMs knocked out perfectly sufficient bindings just fine.