diff --git a/README.org b/README.org
index b9f420b..ac66c63 100644
--- a/README.org
+++ b/README.org
@@ -13,8 +13,8 @@ The Lean4-Mode source code is developed at [[https://github.com/leanprover-commu
 tracked there too.  Further discussions and question-answering takes
 place in the [[https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs][#Emacs channel]] of Lean's Zulip chat.
 
-For legacy version 3 of Lean, use the archived [[https://github.com/leanprover/lean3-mode][Lean3-Mode]] (formerly
-known as /Lean-Mode/).
+For legacy version 3 of Lean, use the archived [[https://github.com/leanprover/lean3-mode][Lean3-Mode]] (also known
+as /Lean-Mode/).
 
 * Installation
 
@@ -191,3 +191,12 @@ use it.  If you want to customize this behavior, e.g. if you'd like to
 use Emacs' built-in Flymake package instead of Flycheck while keeping
 later installed, then customize the ~lsp-diagnostics-provider~ user
 option accordingly.
+
+* Common Pitfalls
+
+Lean4-Mode only supports version 4 of Lean.  For editing Lean version
+3, use [[https://github.com/leanprover/lean3-mode][Lean3-Mode]], which is also known as Lean-Mode due to historical
+reasons.  In principle, it is fine to have both Lean3-Mode and
+Lean4-Mode installed at the same time.  But note that Lean3-Mode uses
+the prefix =lean-= for its symbols.  E.g. you should not use
+=lean-=-prefixed commands in a buffer with Lean4-Mode as major mode.
diff --git a/lean4-mode.info b/lean4-mode.info
index a46a9b8..41a8f4c 100644
--- a/lean4-mode.info
+++ b/lean4-mode.info
@@ -24,14 +24,14 @@ place in the #Emacs channel
 Lean's Zulip chat.
 
    For legacy version 3 of Lean, use the archived Lean3-Mode
-(https://github.com/leanprover/lean3-mode) (formerly known as
-_Lean-Mode_).
+(https://github.com/leanprover/lean3-mode) (also known as _Lean-Mode_).
 
 * Menu:
 
 * Installation::
 * Usage::
 * Configuration::
+* Common Pitfalls::
 
 -- The Detailed Node Listing --
 
@@ -266,7 +266,7 @@ Key         Description            Command
 ‘C-c ! p’   Go to previous error   ‘flycheck-previous-error’
 
 
-File: lean4-mode.info,  Node: Configuration,  Prev: Usage,  Up: Top
+File: lean4-mode.info,  Node: Configuration,  Next: Common Pitfalls,  Prev: Usage,  Up: Top
 
 3 Configuration
 ***************
@@ -299,23 +299,38 @@ Emacs' built-in Flymake package instead of Flycheck while keeping later
 installed, then customize the ‘lsp-diagnostics-provider’ user option
 accordingly.
 
+
+File: lean4-mode.info,  Node: Common Pitfalls,  Prev: Configuration,  Up: Top
+
+4 Common Pitfalls
+*****************
+
+Lean4-Mode only supports version 4 of Lean.  For editing Lean version 3,
+use Lean3-Mode (https://github.com/leanprover/lean3-mode), which is also
+known as Lean-Mode due to historical reasons.  In principle, it is fine
+to have both Lean3-Mode and Lean4-Mode installed at the same time.  But
+note that Lean3-Mode uses the prefix ‘lean-’ for its symbols.  E.g.  you
+should not use ‘lean-’-prefixed commands in a buffer with Lean4-Mode as
+major mode.
+
 
 
 Tag Table:
 Node: Top223
-Node: Installation1476
-Node: Brief and Generic Instructions1719
-Node: Detailed and Concrete Instructions2668
-Node: Instructions for Source-Based Use-Package4325
-Node: Native vc (Emacs 30 or later)5046
-Node: Doom-Emacs5954
-Node: Straight6380
-Node: Usage6880
-Node: lsp-mode8326
-Node: Flycheck8611
-Node: Configuration9221
-Node: lsp-mode (1)9387
-Node: Flycheck (1)9656
+Node: Installation1492
+Node: Brief and Generic Instructions1735
+Node: Detailed and Concrete Instructions2684
+Node: Instructions for Source-Based Use-Package4341
+Node: Native vc (Emacs 30 or later)5062
+Node: Doom-Emacs5970
+Node: Straight6396
+Node: Usage6896
+Node: lsp-mode8342
+Node: Flycheck8627
+Node: Configuration9237
+Node: lsp-mode (1)9427
+Node: Flycheck (1)9696
+Node: Common Pitfalls10181
 
 End Tag Table
 
diff --git a/lean4-mode.texi b/lean4-mode.texi
index c4f92c7..fd205bf 100644
--- a/lean4-mode.texi
+++ b/lean4-mode.texi
@@ -30,8 +30,8 @@ The Lean4-Mode source code is developed at @uref{https://github.com/leanprover-c
 tracked there too.  Further discussions and question-answering takes
 place in the @uref{https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs, #Emacs channel} of Lean's Zulip chat.
 
-For legacy version 3 of Lean, use the archived @uref{https://github.com/leanprover/lean3-mode, Lean3-Mode} (formerly
-known as @emph{Lean-Mode}).
+For legacy version 3 of Lean, use the archived @uref{https://github.com/leanprover/lean3-mode, Lean3-Mode} (also known
+as @emph{Lean-Mode}).
 
 @end ifnottex
 
@@ -39,6 +39,7 @@ known as @emph{Lean-Mode}).
 * Installation::
 * Usage::
 * Configuration::
+* Common Pitfalls::
 
 @detailmenu
 --- The Detailed Node Listing ---
@@ -306,4 +307,14 @@ use Emacs' built-in Flymake package instead of Flycheck while keeping
 later installed, then customize the @code{lsp-diagnostics-provider} user
 option accordingly.
 
+@node Common Pitfalls
+@chapter Common Pitfalls
+
+Lean4-Mode only supports version 4 of Lean.  For editing Lean version
+3, use @uref{https://github.com/leanprover/lean3-mode, Lean3-Mode}, which is also known as Lean-Mode due to historical
+reasons.  In principle, it is fine to have both Lean3-Mode and
+Lean4-Mode installed at the same time.  But note that Lean3-Mode uses
+the prefix @samp{lean-} for its symbols.  E.g. you should not use
+@samp{lean-}-prefixed commands in a buffer with Lean4-Mode as major mode.
+
 @bye