diff --git a/lean4-mode/README.md b/lean4-mode/README.md
index 95251d5413..0b3bfceaa5 100644
--- a/lean4-mode/README.md
+++ b/lean4-mode/README.md
@@ -21,6 +21,25 @@ To use `lean4-mode` in Emacs, add the following to your `init.el`:
 
 (require 'lean4-mode)
 ```
+Alternatively if you are a fan of `use-package` and `straight.el` you
+can use:
+```
+(use-package lean4-mode
+  :straight (lean4-mode :type git :host github :repo "leanprover/lean4"
+             :files ("lean4-mode/lean4*.el"))
+  ;; to defer loading the package until required
+  :commands (lean4-mode))
+```
+If you are working on the `lean4` repository already and don't want to
+have two separate checkouts you can use:
+```
+(use-package lean4-mode
+  :straight (lean4-mode :local-repo "/path/to/your/lean4"
+             :files ("lean4-mode/lean4*.el"))
+  ;; to defer loading the package until required
+  :commands (lean4-mode))
+```
+
 
 Trying It Out
 =============