This is only a partial answer, but my understanding is that Lean is really not meant for software verification work. That's very much Coq's alley.

I'm much less certain of this, but I think Lean is better for non-mathematicians trying to learn more about math --- provided, that is, that you're set on playing with a proof assistant. I'm not sure I'd recommend that.