I have personally tried Coq and Lean and stuck to Lean as it has much better tooling, documentation and usability while being functionally similar to Coq.
Caveat that I have only used Coq and Lean side by side for about a month before deciding to stick with Lean.
Caveat that I have only used Coq and Lean side by side for about a month before deciding to stick with Lean.