Yeah, I'm not a fan of the encouragement to use vscode; that said it was pretty easy for me to get neovim set up with Lean tooling, and that's what I use generally.