We need to remove the hard dependency on lsp-mode. Ideally, end-users should be able to choose between both lsp-mode and Eglot. The removal of the hard dependency on lsp-mode allows us to distribute lean4-mode on the Melpa package-archive.