diff --git a/lean4-mode/README.md b/lean4-mode/README.md
index e3360e1300..de6a7319ac 100644
--- a/lean4-mode/README.md
+++ b/lean4-mode/README.md
@@ -45,17 +45,17 @@ Set these with e.g. `M-x customize-variable`.
 Key Bindings and Commands
 =========================
 
-| Key                | Function                                                                        |
-|--------------------|---------------------------------------------------------------------------------|
-| <kbd>C-c C-k</kbd> | shows the keystroke needed to input the symbol under the cursor                 |
-| <kbd>C-c C-x</kbd> | execute lean in stand-alone mode (`lean-std-exe`)                               |
-| <kbd>C-c C-n</kbd> | toggle showing next error in dedicated buffer (`lean-toggle-next-error`)        |
-| <kbd>C-c ! n</kbd> | flycheck: go to next error                                                      |
-| <kbd>C-c ! p</kbd> | flycheck: go to previous error                                                  |
-| <kbd>C-c ! l</kbd> | flycheck: show list of errors                                                   |
+| Key                | Function                                                                 |
+|--------------------|--------------------------------------------------------------------------|
+| <kbd>C-c C-k</kbd> | show the keystroke needed to input the symbol under the cursor           |
+| <kbd>C-c C-d</kbd> | recompile & reload imports (`lean-refresh-file-dependencies`)            |
+| <kbd>C-c C-x</kbd> | execute Lean in stand-alone mode (`lean-std-exe`)                        |
+| <kbd>C-c C-n</kbd> | toggle showing next error in dedicated buffer (`lean-toggle-next-error`) |
+| <kbd>C-c ! n</kbd> | flycheck: go to next error                                               |
+| <kbd>C-c ! p</kbd> | flycheck: go to previous error                                           |
+| <kbd>C-c ! l</kbd> | flycheck: show list of errors                                            |
 
 For `lsp-mode` bindings, see https://emacs-lsp.github.io/lsp-mode/page/keybindings/ (not all capabilities are supported currently).
-Of note is `s-l s r` for restarting the server, which can be used to make Lean reload changed imports.
 
 In the default configuration, the Flycheck annotation `FlyC:n/n` indicates the
 number of errors / responses from Lean; clicking on `FlyC` opens the Flycheck menu.
diff --git a/lean4-mode/lean4-mode.el b/lean4-mode/lean4-mode.el
index 2ee3381cce..60473ae508 100644
--- a/lean4-mode/lean4-mode.el
+++ b/lean4-mode/lean4-mode.el
@@ -75,6 +75,20 @@
   (interactive)
   (lean4-execute))
 
+(defun lean4-refresh-file-dependencies ()
+  "Restart the server subprocess for the current file, recompiling & reloading all imports"
+  (interactive)
+  (lsp-notify
+   "textDocument/didClose"
+   `(:textDocument ,(lsp--text-document-identifier)))
+  (lsp-notify
+   "textDocument/didOpen"
+   (list :textDocument
+         (list :uri (lsp--buffer-uri)
+               :languageId (lsp-buffer-language)
+               :version lsp--cur-version
+               :text (lsp--buffer-content)))))
+
 (defun lean4-check-expansion ()
   (interactive)
   (save-excursion
@@ -104,6 +118,7 @@
   (local-set-key lean4-keybinding-leanpkg-configure         #'lean4-leanpkg-configure)
   (local-set-key lean4-keybinding-leanpkg-build             #'lean4-leanpkg-build)
   (local-set-key lean4-keybinding-leanpkg-test              #'lean4-leanpkg-test)
+  (local-set-key lean4-keybinding-refresh-file-dependencies #'lean4-refresh-file-dependencies)
   ;; This only works as a mouse binding due to the event, so it is not abstracted
   ;; to avoid user confusion.
   (local-set-key (kbd "<mouse-3>")                         #'lean4-right-click-show-menu)
diff --git a/lean4-mode/lean4-settings.el b/lean4-mode/lean4-settings.el
index 34b9417554..06ceb5ee67 100644
--- a/lean4-mode/lean4-settings.el
+++ b/lean4-mode/lean4-settings.el
@@ -129,4 +129,7 @@ false (nil)."
 (defcustom lean4-keybinding-leanpkg-test (kbd "C-c C-p C-t")
   "Lean Keybinding for lean4-leanpkg-test"
   :group 'lean4-keybinding :type 'key-sequence)
+(defcustom lean4-keybinding-refresh-file-dependencies (kbd "C-c C-d")
+  "Lean Keybinding for lean4-refresh-file-dependencies"
+  :group 'lean4-keybinding :type 'key-sequence)
 (provide 'lean4-settings)