[sadfev]

I think CoqIDE is great and ProofGeneral (Emacs) is something all Coq experts use.

I have the opposite experience with Lean 4, the VSCode integration is horrid and documentation is awful.

The only good sources are papers for Lean4.

Granted I can go back to Lean3 but why would I?

[outlace]

But Lean4 is in alpha stage and there are no official stable releases yet, of course it's not well-documented nor polished yet. Lean3 works perfectly well and has everything you need.