leanprover · alok · Jan 2, 2026 · Jan 2, 2026 · Jan 2, 2026 · Jan 2, 2026
diff --git a/Manual/BasicTypes/Char.lean b/Manual/BasicTypes/Char.lean
@@ -53,7 +53,7 @@ tag := "char-syntax"
 %%%
 
 Character literals consist of a single character or an escape sequence enclosed in single quotes (`'`, Unicode `'APOSTROPHE' (U+0027)`).
-Between these single quotes, the character literal may contain character other that `'`, including newlines, which are included literally (with the caveat that all newlines in a Lean source file are interpreted as `'\n'`, regardless of file encoding and platform).
+Between these single quotes, the character literal may contain any character other than `'`, including newlines, which are included literally (with the caveat that all newlines in a Lean source file are interpreted as `'\n'`, regardless of file encoding and platform).
 Special characters may be escaped with a backslash, so `'\''` is a character literal that contains a single quote.
 The following forms of escape sequences are accepted:
 

diff --git a/Manual/BasicTypes/Float.lean b/Manual/BasicTypes/Float.lean
@@ -23,7 +23,7 @@ set_option pp.rawOnError true
 tag := "Float"
 %%%
 
-Floating-point numbers are a an approximation of the real numbers that are efficiently implemented in computer hardware.
+Floating-point numbers are an approximation of the real numbers that are efficiently implemented in computer hardware.
 Computations that use floating-point numbers are very efficient; however, the nature of the way that they approximate the real numbers is complex, with many corner cases.
 The IEEE 754 standard, which defines the floating-point format that is used on modern computers, allows hardware designers to make certain choices, and real systems differ in these small details.
 For example, there are many distinct bit representations of `NaN`, the indicator that a result is undefined, and some platforms differ with respect to _which_ `NaN` is returned from adding two `NaN`s.

diff --git a/Manual/BasicTypes/Int.lean b/Manual/BasicTypes/Int.lean
@@ -183,7 +183,7 @@ All evaluate to 0.
 
 ## Bitwise Operators
 
-Bitwise operators on {name}`Int` can be understood as bitwise operators on an infinite stream of bits that are the twos-complement representation of integers.
+Bitwise operators on {name}`Int` can be understood as bitwise operators on an infinite stream of bits that are the two's-complement representation of integers.
 
 {docstring Int.not}
 

diff --git a/Manual/BasicTypes/UInt.lean b/Manual/BasicTypes/UInt.lean
@@ -29,7 +29,7 @@ In compiled code, they are represented efficiently: the compiler has special sup
 Fixed-width integers may be unsigned or signed.
 Furthermore, they are available in five sizes: 8, 16, 32, and 64 bits, along with the current architecture's word size.
 In their logical models, the unsigned integers are structures that wrap a {name}`BitVec` of the appropriate width.
-Signed integers wrap the corresponding unsigned integers, and use a twos-complement representation.
+Signed integers wrap the corresponding unsigned integers, and use a two's-complement representation.
 
 ## Unsigned
 
@@ -108,7 +108,7 @@ theorem Permissions.decode_encode (p : Permissions) : p = .decode (p.encode) :=
 :::
 
 Literals that overflow their types' precision are interpreted modulus the precision.
-Signed types, are interpreted according to the underlying twos-complement representation.
+Signed types, are interpreted according to the underlying two's-complement representation.
 
 :::example "Overflowing Fixed-Width Literals"
 The following statements are all true:

diff --git a/Manual/BuildTools/Lake/CLI.lean b/Manual/BuildTools/Lake/CLI.lean
@@ -956,13 +956,13 @@ They are likely change in future versions of Lake based on user feedback.
 Packages that use Reservoir cloud build archives should enable the {tomlField Lake.PackageConfig}`platformIndependent` setting.
 
 ```lakeHelp "pack"
-Pack build artifacts into a archive for distribution
+Pack build artifacts into an archive for distribution
 
 USAGE:
   lake pack [<file.tgz>]
 
 Packs the root package's `buildDir` into a gzip tar archive using `tar`.
-If a path for the archive is not specified, creates a archive in the package's
+If a path for the archive is not specified, creates an archive in the package's
 Lake directory (`.lake`) named according to its `buildArchive` setting.
 
 Does NOT build any artifacts. It just packs the existing ones.
@@ -1160,7 +1160,7 @@ If {lakeOpt}`--scope` is set, Lake will use the specified scope verbatim.
 
 Artifacts are uploaded to the artifact endpoint with a file name derived from their Lake content hash (and prefixed by the repository or scope).
 The mappings file is uploaded to the revision endpoint with a file name derived from the package's current Git revision (and prefixed by the full scope).
-As such, the command will warn if the the work tree currently has changes.
+As such, the command will warn if the work tree currently has changes.
 ::::
 
 

diff --git a/Manual/Classes/DerivingHandlers.lean b/Manual/Classes/DerivingHandlers.lean
@@ -51,7 +51,7 @@ private def checkDerivable (expected : Array Name) : CommandElabM Unit := do
     unless missing.isEmpty do
       logError
         m!"These classes were expected but not present. Check whether the text needs updating, then \
-           then remove them from the call."
+           remove them from the call."
 
 end
 

diff --git a/Manual/Grind/Algebra.lean b/Manual/Grind/Algebra.lean
@@ -216,7 +216,7 @@ tag := "NoNatZeroDivisors"
 
 The class `NoNatZeroDivisors` is used to control coefficient growth.
 For example, the polynomial `2 * x * y + 4 * z = 0` is simplified to `x * y + 2 * z = 0`.
-It also used when processing disequalities.
+It is also used when processing disequalities.
 
 :::example "Using `NoNatZeroDivisors`"
 ```lean -show

diff --git a/Manual/Grind/CaseAnalysis.lean b/Manual/Grind/CaseAnalysis.lean
@@ -23,7 +23,7 @@ tag := "grind-split"
 %%%
 
 In addition to congruence closure and constraint propagation, {tactic}`grind` performs case analysis.
-During case analysis, {tactic}`grind` considers each possible way that a term could have been built, or each possbile value of a particular term, in a manner similar to the {tactic}`cases` and {tactic}`split` tactics.
+During case analysis, {tactic}`grind` considers each possible way that a term could have been built, or each possible value of a particular term, in a manner similar to the {tactic}`cases` and {tactic}`split` tactics.
 This case analysis is not exhaustive: {tactic}`grind` only recursively splits cases up to a configured depth limit, and configuration options and annotations control which terms are candidates for splitting.
 
 

diff --git a/Manual/Grind/EMatching.lean b/Manual/Grind/EMatching.lean
@@ -748,7 +748,7 @@ h₄: [p (#2 + 2), q #1]
 axiom p : Nat → Nat
 axiom q : Nat → Nat
 ```
-In this example, pattern generation fails because the theorem's conclusion doesn't mention the the argument `y`.
+In this example, pattern generation fails because the theorem's conclusion doesn't mention the argument `y`.
 ```lean (name := h5) +error
 @[grind? ←] theorem h₅ (w : p x = q y) : p (x + 2) = 7 := sorry
 ```

diff --git a/Manual/Grind/ExtendedExamples/IfElseNorm.lean b/Manual/Grind/ExtendedExamples/IfElseNorm.lean
@@ -418,7 +418,7 @@ theorem normalize_spec
   fun_induction normalize with grind
 ```
 
-(The fact that we can do this relies on the fact that all the lemmas for both {name}`HashMap` and for {name}`TreeMap` that {tactic}`grind` needs have already be annotated in the standard library.)
+(The fact that we can do this relies on the fact that all the lemmas for both {name}`HashMap` and for {name}`TreeMap` that {tactic}`grind` needs have already been annotated in the standard library.)
 
 If you'd like to play around with this code,
 you can find the whole file [here](https://github.com/leanprover/lean4/blob/master/tests/lean/run/grind_ite.lean),

diff --git a/Manual/Language/InductiveTypes.lean b/Manual/Language/InductiveTypes.lean
@@ -160,7 +160,7 @@ Solo.solo : Solo
 inductive Yes : Prop where
   | intro
 ```
-Unlike {lean}`One`, the new inductive type {lean}`Yes` is specified to be in the {lean}`Prop` universe.
+Unlike {lean}`Solo`, the new inductive type {lean}`Yes` is specified to be in the {lean}`Prop` universe.
 ```lean (name := YesTy)
 #check Yes
 ```

diff --git a/Manual/Language/InductiveTypes/LogicalModel.lean b/Manual/Language/InductiveTypes/LogicalModel.lean
@@ -368,7 +368,7 @@ tag := "recursor-elaboration-helpers"
 %%%
 
 In addition to the type constructor, constructors, and recursors that Lean's core type theory prescribes for inductive types, Lean constructs a number of useful helpers.
-First, the equation compiler (which translates recursive functions with pattern matching in to applications of recursors) makes use of these additional constructs:
+First, the equation compiler (which translates recursive functions with pattern matching into applications of recursors) makes use of these additional constructs:
  * `recOn` is a version of the recursor in which the major premise is prior to the minor premise for each constructor.
  * `casesOn` is a version of the recursor in which the major premise is prior to the minor premise for each constructor, and recursive arguments do not yield induction hypotheses. It expresses case analysis rather than primitive recursion.
  * `below` computes a type that, for some motive, expresses that _all_ inhabitants of the inductive type that are subtrees of the major premise satisfy the motive. It transforms a motive for induction or primitive recursion into a motive for strong recursion or strong induction.

diff --git a/Manual/Monads/API.lean b/Manual/Monads/API.lean
@@ -22,7 +22,7 @@ set_option linter.unusedVariables false
 
 #doc (Manual) "API Reference" =>
 
-In addition to the general functions described here, there are some functions that are conventionally defined as part of the API of in the namespace of each collection type:
+In addition to the general functions described here, there are some functions that are conventionally defined as part of the API in the namespace of each collection type:
  * `mapM` maps a monadic function.
  * `forM` maps a monadic function, throwing away the result.
  * `filterM` filters using a monadic predicate, returning the values that satisfy it.
@@ -100,7 +100,7 @@ The {name}`discard` function is especially useful when using an action that retu
 # Re-Ordered Operations
 
 Sometimes, it can be convenient to partially apply a function to its second argument.
-These functions reverse the order of arguments, making it this easier.
+These functions reverse the order of arguments, making this easier.
 
 {docstring Functor.mapRev}
 

diff --git a/Manual/Namespaces.lean b/Manual/Namespaces.lean
@@ -203,7 +203,7 @@ Without an identifier, {keywordOf Lean.Parser.Command.end}`end` closes the most
 end
 ```
 
-With an identifier, it closes the most recently opened section section or namespace.
+With an identifier, it closes the most recently opened section or namespace.
 If it is a section, the identifier must be a suffix of the concatenated names of the sections opened since the most recent {keywordOf Lean.Parser.Command.namespace}`namespace` command.
 If it is a namespace, then the identifier must be a suffix of the current namespace's extensions since the most recent {keywordOf Lean.Parser.Command.section}`section` that is still open; afterwards, the current namespace will have had this suffix removed.
 ```grammar

diff --git a/Manual/Releases/v4_10_0.lean b/Manual/Releases/v4_10_0.lean
@@ -166,7 +166,7 @@ file := "v4.10.0"
   * [#4499](https://github.com/leanprover/lean4/pull/4499) introduces `Std`, a library situated between `Init` and `Lean`, providing functionality not in the prelude both to Lean's implementation and to external users.
 * **Other fixes or improvements**
   * [#3056](https://github.com/leanprover/lean4/pull/3056) standardizes on using `(· == a)` over `(a == ·)`.
-  * [#4502](https://github.com/leanprover/lean4/pull/4502) fixes errors reported by running the library through the the Batteries linters.
+  * [#4502](https://github.com/leanprover/lean4/pull/4502) fixes errors reported by running the library through the Batteries linters.
 
 ### Lean internals
 

diff --git a/Manual/Releases/v4_15_0.lean b/Manual/Releases/v4_15_0.lean
@@ -489,7 +489,7 @@ make proving inequalities about `USize.size` easier.
 
 - [#6205](https://github.com/leanprover/lean4/pull/6205) upstreams some UInt theorems from Batteries and adds more
 `toNat`-related theorems. It also adds the missing `UInt8` and `UInt16`
-to/from `USize` conversions so that the the interface is uniform across
+to/from `USize` conversions so that the interface is uniform across
 the UInt types.
 
 - [#6207](https://github.com/leanprover/lean4/pull/6207) ensures the `Fin.foldl` and `Fin.foldr` are semireducible.

diff --git a/Manual/Releases/v4_16_0.lean b/Manual/Releases/v4_16_0.lean
@@ -548,7 +548,7 @@ none) using the necessary flags.
 * [#6289](https://github.com/leanprover/lean4/pull/6289) adapts Lake modules to use `prelude` and includes them in the
 `check-prelude` CI.
 
-* [#6291](https://github.com/leanprover/lean4/pull/6291) ensures the the log error position is properly preserved when
+* [#6291](https://github.com/leanprover/lean4/pull/6291) ensures the log error position is properly preserved when
 prepending stray log entries to the job log. It also adds comparison
 support for `Log.Pos`.
 

diff --git a/Manual/Releases/v4_17_0.lean b/Manual/Releases/v4_17_0.lean
@@ -461,7 +461,7 @@ theorem:
   ```lean
   theorem inv_eq {a b : α} (w : a * b = 1) : inv a = b
   ```
-  and we want to instantiate the theorem whenever we are tying to prove
+  and we want to instantiate the theorem whenever we are trying to prove
 `inv t = s` for some terms `t` and `s`
 The attribute `[grind ←]` is not applicable in this case because, by
 default, `=` is not eligible for E-matching. The new attribute `[grind

diff --git a/Manual/Releases/v4_20_0.lean b/Manual/Releases/v4_20_0.lean
@@ -1095,7 +1095,7 @@ Other notable library developments in this release include:
   no longer incorporate their module's source trace.
 
 * [#7909](https://github.com/leanprover/lean4/pull/7909) adds Lake support for building modules given their source file
-  path. This is made use of in both the CLI and the sever.
+  path. This is made use of in both the CLI and the server.
 
 * [#7963](https://github.com/leanprover/lean4/pull/7963) adds helper functions to convert between `Lake.EStateT` and
   `EStateM`.

diff --git a/Manual/Releases/v4_21_0.lean b/Manual/Releases/v4_21_0.lean
@@ -304,7 +304,7 @@ _Other Highlights_
 * [#8301](https://github.com/leanprover/lean4/pull/8301) unfolds functions in the unfolding induction principle properly
   when they use `bif` (a.k.a. `Bool.cond`).
 
-* [#8302](https://github.com/leanprover/lean4/pull/8302) lets `cases` fail gracefully when the motive has an complex
+* [#8302](https://github.com/leanprover/lean4/pull/8302) lets `cases` fail gracefully when the motive has a complex
   argument whose type is dependent type on the targets. While the
   `induction` tactic can handle this well, `cases` does not. This change
   at least gracefully degrades to not instantiating that motive parameter.
@@ -600,7 +600,7 @@ _Other Highlights_
   `BitVec.one_eq_zero_iff`
 
 * [#8206](https://github.com/leanprover/lean4/pull/8206) shows that negating a bitvector created from a natural number
-  equals creating a bitvector from the the negative of that number (as an
+  equals creating a bitvector from the negative of that number (as an
   integer).
 
 * [#8216](https://github.com/leanprover/lean4/pull/8216) completes adding `@[grind]` annotations for `Option` lemmas, and
@@ -770,7 +770,7 @@ _Other Highlights_
 
 * [#8620](https://github.com/leanprover/lean4/pull/8620) removes the `NatCast (Fin n)` global instance (both the direct
   instance, and the indirect one via `Lean.Grind.Semiring`), as that
-  instance causes causes `x < n` (for `x : Fin k`, `n : Nat`) to be
+  instance causes `x < n` (for `x : Fin k`, `n : Nat`) to be
   elaborated as `x < ↑n` rather than `↑x < n`, which is undesirable. Note
   however that in Mathlib this happens anyway!
 
@@ -928,7 +928,7 @@ _Other Highlights_
   name would not be caught and cause loading to fail.
 
 * [#8529](https://github.com/leanprover/lean4/pull/8529) changes `lake lean` and `lake setup-file` to precompile the
-  imports of non-workspace files using the the import's whole library.
+  imports of non-workspace files using the import's whole library.
   This ensures that additional link objects are linked and available
   during elaboration.
 

diff --git a/Manual/Releases/v4_22_0.lean b/Manual/Releases/v4_22_0.lean
@@ -403,7 +403,7 @@ When false, the warning is not logged.
   linarith modules in grind.
 
 * [#8694](https://github.com/leanprover/lean4/pull/8694) implements special support for `One.one` in linarith when the
-  structure is a ordered ring. It also fixes bugs during initialization.
+  structure is an ordered ring. It also fixes bugs during initialization.
 
 * [#8697](https://github.com/leanprover/lean4/pull/8697) implements support for inequalities in the `grind` linear
   arithmetic procedure and simplifies its design. Some examples that can
@@ -1068,7 +1068,7 @@ When false, the warning is not logged.
 
 * [#8620](https://github.com/leanprover/lean4/pull/8620) removes the `NatCast (Fin n)` global instance (both the direct
   instance, and the indirect one via `Lean.Grind.Semiring`), as that
-  instance causes causes `x < n` (for `x : Fin k`, `n : Nat`) to be
+  instance causes `x < n` (for `x : Fin k`, `n : Nat`) to be
   elaborated as `x < ↑n` rather than `↑x < n`, which is undesirable. Note
   however that in Mathlib this happens anyway!
 

diff --git a/Manual/Releases/v4_23_0.lean b/Manual/Releases/v4_23_0.lean
@@ -586,7 +586,7 @@ In terms of user experience, noteworthy new features are:
 
 * [#9670](https://github.com/leanprover/lean4/pull/9670) add constructors `.intCast k` and `.natCast k` to
   `CommRing.Expr`. We need them because terms such as `Nat.cast (R := α)
-  1` and `(1 : α)` are not definitionally equal. This is pervaise in
+  1` and `(1 : α)` are not definitionally equal. This is pervasive in
   Mathlib for the numerals `0` and `1`.
 
 * [#9671](https://github.com/leanprover/lean4/pull/9671) fixes support for `SMul.smul` in `grind ring`. `SMul.smul`

diff --git a/Manual/Releases/v4_27_0.lean b/Manual/Releases/v4_27_0.lean
@@ -35,7 +35,7 @@ For this release, 372 changes landed. In addition to the 118 feature additions a
   `MatcherInfo`, and using that during matcher calculation.
 
 * [#11200](https://github.com/leanprover/lean4/pull/11200) changes how sparse case expressions represent the
-  none-of-the-above information. Instead of of many `x.ctorIdx ≠ i`
+  none-of-the-above information. Instead of many `x.ctorIdx ≠ i`
   hypotheses, it introduces a single `Nat.hasNotBit mask x.ctorIdx`
   hypothesis which compresses that information into a bitmask. This avoids
   a quadratic overhead during splitter generation, where all n assumptions
@@ -155,7 +155,7 @@ For this release, 372 changes landed. In addition to the 118 feature additions a
 * [#11453](https://github.com/leanprover/lean4/pull/11453) fixes undefined behavior where `delete` (instead of `delete[]`)
   is called on an object allocated with `new[]`.
 
-* [#11456](https://github.com/leanprover/lean4/pull/11456) refines several error error messages, mostly involving invalid
+* [#11456](https://github.com/leanprover/lean4/pull/11456) refines several error messages, mostly involving invalid
   use of field notation, generalized field notation, and numeric
   projection. Provides a new error explanation for field notation.
 
@@ -182,7 +182,7 @@ For this release, 372 changes landed. In addition to the 118 feature additions a
   those using `aesop`) being affected by the current recursion depth or
   heartbeat limit.
 
-* [#11492](https://github.com/leanprover/lean4/pull/11492) uses the the helper functions withImplicitBinderInfos and
+* [#11492](https://github.com/leanprover/lean4/pull/11492) uses the helper functions withImplicitBinderInfos and
   mkArrowN in more places.
 
 * [#11493](https://github.com/leanprover/lean4/pull/11493) makes `Match.MatchEqs` a leaf module, to be less restricted in

diff --git a/Manual/Releases/v4_8_0.lean b/Manual/Releases/v4_8_0.lean
@@ -379,7 +379,7 @@ file := "v4.8.0"
 
 * **TOML Lake configurations**. [#3298](https://github.com/leanprover/lean4/pull/3298), [#4104](https://github.com/leanprover/lean4/pull/4104).
 
-  Lake packages can now use TOML as a alternative configuration file format instead of Lean. If the default `lakefile.lean` is missing, Lake will also look for a `lakefile.toml`. The TOML version of the configuration supports a restricted set of the Lake configuration options, only including those which can easily mapped to a TOML data structure. The TOML syntax itself fully compiles with the TOML v1.0.0 specification.
+  Lake packages can now use TOML as an alternative configuration file format instead of Lean. If the default `lakefile.lean` is missing, Lake will also look for a `lakefile.toml`. The TOML version of the configuration supports a restricted set of the Lake configuration options, only including those which can easily mapped to a TOML data structure. The TOML syntax itself fully compiles with the TOML v1.0.0 specification.
 
   As part of the introduction of this new feature, we have been helping maintainers of some major packages within the ecosystem switch to this format. For example, the following is Aesop's new `lakefile.toml`: