Remove unmaintained "Even Better TOML" dependency

Description

Please remove the "Even Better TOML" dependency or make it optional, to improve the supply chain security of the vscode-lean4 extension.

Context

See https://github.com/tamasfe/taplo/issues/715. The extension seems to be in a state where we cannot expect it to be maintained in a secure manner. Indeed, the extension was last updated 12/20/2024. From the thread I linked to, it is likely that any future updates are likely to come from people other than the author.

In #706 it was also noted that the extension is absolutely huge. Thus the attack surface of the extension is also large.

A gigantic attack surface with no maintainers is a terrible combination.

Lean 4 itself is foundational in the supply chain security of several projects that intend to be critical infrastructure for other tools (e.g. security, privacy, cryptography components), and the VS Code extension is the primary recommended interface to Lean 4. Thus it is critical that the Lean 4 VS Code extension also have a good supply chain security story.

In #706 it was suggested that the code completion (etc.) support for lakefiles is critical. IMO it is not so critical to justify complicating the security story for the project.

No file or test is named in the issue. Start by locating the Even Better TOML dependency and the lakefile code-completion entry points in the vscode-lean4 extension, then review #706 and the linked taplo issue. Done means the dependency is removed or made optional while the required extension functionality still builds and works.