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. Cave

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.