Yes, it isn’t performant. Lean isn’t a language for writing software, though you technically can; it’s a language for proving math.
Also, part of my confidence comes from both having been a professional programmer for decades, across many languages, and also having programmed in Lean. It’s a great language for math, perhaps the best choice right now. But as a general purpose language it’s incredibly quirky.