現状ではVSCodeに限って言えば（Emacs等他はどうかは知らない）Nixの例えばdevshellなどが上手くVSCodeと上手く噛み合ってくれるかはかなり微妙で多分出来ておらず，おとなしくelanを入れるか，どうしてもクリーンな環境を保っておきたいならdevcontainerとかを使うのが良いと思う（Mathlib4のものを参照）

https://github.com/leanprover-community/mathlib4/tree/master/.devcontainer