I've found the VS Code plugin for Microsoft's Lean Theorem prover to be quite nice as far as IDE support goes.

https://leanprover.github.io/about/ https://github.com/leanprover/vscode-lean