README: Not necessary to (require 'lean4-mode)

Also propagate recent comma-grammar change in README to manuals.

README.org

@@ -30,8 +30,9 @@ Install dependencies:
 Install Lean4-Mode:
 - Clone the [[https://github.com/leanprover-community/lean4-mode][Git repository of Lean4-Mode]].
 - In your [[https://www.gnu.org/software/emacs/manual/html_node/emacs/Init-File.html][Emacs initialization file]], add the path to that local
-  repository to the ~load-path~ list and
-- load Lean4-Mode with =(require 'lean4-mode)=.
+  repository to the ~load-path~ list.
+# Note that (require 'lean4-mode) is not necessary when the user
+# relies on autoloading and uses the default settings.
 
 ** Detailed and Concrete Instructions
 

lean4-mode.info

@@ -72,7 +72,7 @@ Install dependencies:
    • Emacs packages Dash (https://github.com/magnars/dash.el) (which is
      available on GNU-Elpa package-archive), Flycheck
      (https://www.flycheck.org), lsp-mode
-     (https://emacs-lsp.github.io/lsp-mode) and Magit-Section
+     (https://emacs-lsp.github.io/lsp-mode), and Magit-Section
      (https://github.com/magit/magit/blob/main/lisp/magit-section.el)
      (which are available on Melpa package-archive)
 
@@ -81,8 +81,7 @@ Install dependencies:
      (https://github.com/leanprover-community/lean4-mode).
    • In your Emacs initialization file
      (https://www.gnu.org/software/emacs/manual/html_node/emacs/Init-File.html),
-     add the path to that local repository to the ‘load-path’ list and
-   • load Lean4-Mode with ‘(require 'lean4-mode)’.
+     add the path to that local repository to the ‘load-path’ list.
 
 
 File: lean4-mode.info,  Node: Detailed and Concrete Instructions,  Next: Instructions for Source-Based Use-Package,  Prev: Brief and Generic Instructions,  Up: Installation
@@ -249,13 +248,13 @@ Tag Table:
 Node: Top223
 Node: Installation1324
 Node: Brief and Generic Instructions1567
-Node: Detailed and Concrete Instructions2624
-Node: Instructions for Source-Based Use-Package4178
-Node: Native vc (Emacs 30 or later)4899
-Node: Doom-Emacs5752
-Node: Straight6152
-Node: Usage6642
-Node: Key Bindings and Commands7562
+Node: Detailed and Concrete Instructions2565
+Node: Instructions for Source-Based Use-Package4119
+Node: Native vc (Emacs 30 or later)4840
+Node: Doom-Emacs5693
+Node: Straight6093
+Node: Usage6583
+Node: Key Bindings and Commands7503
 
 End Tag Table
 

lean4-mode.texi

@@ -78,7 +78,7 @@ Install dependencies:
 Emacs version 27 or later
 @item
 Emacs packages @uref{https://github.com/magnars/dash.el, Dash} (which is available on GNU-Elpa
-package-archive), @uref{https://www.flycheck.org, Flycheck}, @uref{https://emacs-lsp.github.io/lsp-mode, lsp-mode} and @uref{https://github.com/magit/magit/blob/main/lisp/magit-section.el, Magit-Section} (which are
+package-archive), @uref{https://www.flycheck.org, Flycheck}, @uref{https://emacs-lsp.github.io/lsp-mode, lsp-mode}, and @uref{https://github.com/magit/magit/blob/main/lisp/magit-section.el, Magit-Section} (which are
 available on Melpa package-archive)
 @end itemize
 
@@ -88,9 +88,7 @@ Install Lean4-Mode:
 Clone the @uref{https://github.com/leanprover-community/lean4-mode, Git repository of Lean4-Mode}.
 @item
 In your @uref{https://www.gnu.org/software/emacs/manual/html_node/emacs/Init-File.html, Emacs initialization file}, add the path to that local
-repository to the @code{load-path} list and
-@item
-load Lean4-Mode with @samp{(require 'lean4-mode)}.
+repository to the @code{load-path} list.
 @end itemize
 
 @node Detailed and Concrete Instructions