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?