Lean has a good library of formalized mathematics, but lacks code extraction (you cannot generate a program from the proofs it constructs). So it is more suitable and highly used by mathematicians to prove theorems.

Coq has always focused on proving program correctness, so it sees lots of use by computer scientists. It also does code extraction, so after you prove a program correct in Coq you can generate a fast version of that program without the proof overhead.