style: fix typos in Init/ and Std/ docstrings

src/Init/Classical.lean

@@ -102,7 +102,7 @@ noncomputable def strongIndefiniteDescription {α : Sort u} (p : α → Prop) (h
       ⟨xp.val, fun _ => xp.property⟩)
     (fun hp => ⟨choice h, fun h => absurd h hp⟩)
 
-/-- the Hilbert epsilon Function -/
+/-- The Hilbert epsilon function. -/
 noncomputable def epsilon {α : Sort u} [h : Nonempty α] (p : α → Prop) : α :=
   (strongIndefiniteDescription p h).val
 

src/Init/Control/Basic.lean

@@ -144,7 +144,7 @@ instance : ToBool Bool where
 Converts the result of the monadic action `x` to a `Bool`. If it is `true`, returns it and ignores
 `y`; otherwise, runs `y` and returns its result.
 
-This a monadic counterpart to the short-circuiting `||` operator, usually accessed via the `<||>`
+This is a monadic counterpart to the short-circuiting `||` operator, usually accessed via the `<||>`
 operator.
 -/
 @[macro_inline] def orM {m : Type u → Type v} {β : Type u} [Monad m] [ToBool β] (x y : m β) : m β := do
@@ -161,7 +161,7 @@ recommended_spelling "orM" for "<||>" in [orM, «term_<||>_»]
 Converts the result of the monadic action `x` to a `Bool`. If it is `true`, returns `y`; otherwise,
 returns the original result of `x`.
 
-This a monadic counterpart to the short-circuiting `&&` operator, usually accessed via the `<&&>`
+This is a monadic counterpart to the short-circuiting `&&` operator, usually accessed via the `<&&>`
 operator.
 -/
 @[macro_inline] def andM {m : Type u → Type v} {β : Type u} [Monad m] [ToBool β] (x y : m β) : m β := do

src/Init/Core.lean

@@ -337,7 +337,7 @@ inductive Exists {α : Sort u} (p : α → Prop) : Prop where
 An indication of whether a loop's body terminated early that's used to compile the `for x in xs`
 notation.
 
-A collection's `ForIn` or `ForIn'` instance describe's how to iterate over its elements. The monadic
+A collection's `ForIn` or `ForIn'` instance describes how to iterate over its elements. The monadic
 action that represents the body of the loop returns a `ForInStep α`, where `α` is the local state
 used to implement features such as `let mut`.
 -/
@@ -510,12 +510,12 @@ abbrev SSuperset [HasSSubset α] (a b : α) := SSubset b a
 
 /-- Notation type class for the union operation `∪`. -/
 class Union (α : Type u) where
-  /-- `a ∪ b` is the union of`a` and `b`. -/
+  /-- `a ∪ b` is the union of `a` and `b`. -/
   union : α → α → α
 
 /-- Notation type class for the intersection operation `∩`. -/
 class Inter (α : Type u) where
-  /-- `a ∩ b` is the intersection of`a` and `b`. -/
+  /-- `a ∩ b` is the intersection of `a` and `b`. -/
   inter : α → α → α
 
 /-- Notation type class for the set difference `\`. -/
@@ -538,10 +538,10 @@ infix:50 " ⊇ " => Superset
 /-- Strict superset relation: `a ⊃ b`  -/
 infix:50 " ⊃ " => SSuperset
 
-/-- `a ∪ b` is the union of`a` and `b`. -/
+/-- `a ∪ b` is the union of `a` and `b`. -/
 infixl:65 " ∪ " => Union.union
 
-/-- `a ∩ b` is the intersection of`a` and `b`. -/
+/-- `a ∩ b` is the intersection of `a` and `b`. -/
 infixl:70 " ∩ " => Inter.inter
 
 /--

src/Init/Data/Iterators/PostconditionMonad.lean

@@ -72,7 +72,7 @@ def PostconditionT.liftWithProperty {α : Type w} {m : Type w → Type w'} {P :
   ⟨P, x⟩
 
 /--
-Given a function `f : α → β`, returns a a function `PostconditionT m α → PostconditionT m β`,
+Given a function `f : α → β`, returns a function `PostconditionT m α → PostconditionT m β`,
 turning `PostconditionT m` into a functor.
 
 The postcondition of the `x.map f` states that the return value is the image under `f` of some
@@ -85,7 +85,7 @@ protected def PostconditionT.map {m : Type w → Type w'} [Functor m] {α : Type
     (fun a => ⟨f a.val, _, rfl⟩) <$> x.operation⟩
 
 /--
-Given a function `α → PostconditionT m β`, returns a a function
+Given a function `α → PostconditionT m β`, returns a function
 `PostconditionT m α → PostconditionT m β`, turning `PostconditionT m` into a monad.
 -/
 @[always_inline, inline, expose]

src/Init/Data/LawfulHashable.lean

@@ -11,7 +11,7 @@ public import Init.Core
 public section
 
 /--
-The `BEq α` and `Hashable α` instances on `α` are compatible. This means that that `a == b` implies
+The `BEq α` and `Hashable α` instances on `α` are compatible. This means that `a == b` implies
 `hash a = hash b`.
 
 This is automatic if the `BEq` instance is lawful.

src/Init/Data/List/Control.lean

@@ -50,7 +50,7 @@ Users that want to use `mapM` with `Applicative` should use `mapA` instead.
 Applies the monadic action `f` to every element in the list, left-to-right, and returns the list of
 results.
 
-This implementation is tail recursive. `List.mapM'` is a a non-tail-recursive variant that may be
+This implementation is tail recursive. `List.mapM'` is a non-tail-recursive variant that may be
 more convenient to reason about. `List.forM` is the variant that discards the results and
 `List.mapA` is the variant that works with `Applicative`.
 -/
@@ -107,7 +107,7 @@ Applies the monadic action `f` to the corresponding elements of two lists, left-
 at the end of the shorter list. `zipWithM f as bs` is equivalent to `mapM id (zipWith f as bs)`
 for lawful `Monad` instances.
 
-This implementation is tail recursive. `List.zipWithM'` is a a non-tail-recursive variant that may
+This implementation is tail recursive. `List.zipWithM'` is a non-tail-recursive variant that may
 be more convenient to reason about.
 -/
 @[inline, expose]

src/Init/Data/Order/Ord.lean

@@ -46,7 +46,7 @@ theorem ne_of_cmp_ne_eq {α : Type u} {cmp : α → α → Ordering} [Std.ReflCm
 
 end ReflCmp
 
-/-- A typeclasses for ordered types for which `compare a a = .eq` for all `a`. -/
+/-- A typeclass for ordered types for which `compare a a = .eq` for all `a`. -/
 abbrev ReflOrd (α : Type u) [Ord α] := ReflCmp (compare : α → α → Ordering)
 
 @[simp]

src/Init/Data/Slice/Notation.lean

@@ -40,7 +40,7 @@ class Rcc.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type
 This typeclass indicates how to obtain slices of elements of {lit}`α` over ranges in the index type
 {lit}`β`, the ranges being left-closed right-open.
 
-The type of resulting the slices is {lit}`γ`.
+The type of the resulting slices is {lit}`γ`.
 -/
 class Rco.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
   /--

src/Init/Data/String/Pattern/String.lean

@@ -119,7 +119,7 @@ instance (s : Slice) : Std.Iterator (ForwardSliceSearcher s) Id (SearchStep s) w
       -- **Invariant 1:** we have already covered everything up until `stackPos - needlePos` (exclusive),
       -- with matches and rejections.
       -- **Invariant 2:** `stackPos - needlePos` is a valid position
-      -- **Invariant 3:** the range from from `stackPos - needlePos` to `stackPos` (exclusive) is a
+      -- **Invariant 3:** the range from `stackPos - needlePos` to `stackPos` (exclusive) is a
       -- prefix of the pattern.
       if h₁ : stackPos < s.rawEndPos then
         let stackByte := s.getUTF8Byte stackPos h₁

src/Init/Data/String/Slice.lean

@@ -20,7 +20,7 @@ functionality for searching for various kinds of pattern matches in slices to it
 provide subslices according to matches etc. The key design principles behind this module are:
 - Instead of providing one function per kind of pattern the API is generic over various kinds of
   patterns. Thus it only provides e.g. one kind of function for looking for the position of the
-  first occurence of a pattern. Currently the supported patterns are:
+  first occurrence of a pattern. Currently the supported patterns are:
   - {name}`Char`
   - {lean}`Char → Bool`
   - {name}`String` and {name}`String.Slice` (partially: doing non trivial searches backwards is not

src/Init/Notation.lean

@@ -523,7 +523,7 @@ macro_rules
   | `(bif $c then $t else $e) => `(cond $c $t $e)
 
 /--
-Haskell-like pipe operator `<|`. `f <| x` means the same as the same as `f x`,
+Haskell-like pipe operator `<|`. `f <| x` means the same as `f x`,
 except that it parses `x` with lower precedence, which means that `f <| g <| x`
 is interpreted as `f (g x)` rather than `(f g) x`.
 -/
@@ -557,7 +557,7 @@ macro_rules
   | `($a |> $f)        => `($f $a)
 
 /--
-Alternative syntax for `<|`. `f $ x` means the same as the same as `f x`,
+Alternative syntax for `<|`. `f $ x` means the same as `f x`,
 except that it parses `x` with lower precedence, which means that `f $ g $ x`
 is interpreted as `f (g x)` rather than `(f g) x`.
 -/

src/Init/NotationExtra.lean

@@ -120,7 +120,7 @@ calc
   _ = z := pyz
 ```
 It is also possible to write the *first* relation as `<lhs>\n  _ = <rhs> :=
-<proof>`. This is useful for aligning relation symbols, especially on longer:
+<proof>`. This is useful for aligning relation symbols, especially on longer
 identifiers:
 ```
 calc abc

src/Init/Prelude.lean

@@ -907,7 +907,7 @@ instance [Inhabited α] : Inhabited (ULift α) where
 Lifts a type or proposition to a higher universe level.
 
 `PULift α` wraps a value of type `α`. It is a generalization of
-`PLift` that allows lifting values who's type may live in `Sort s`.
+`PLift` that allows lifting values whose type may live in `Sort s`.
 It also subsumes `PLift`.
 -/
 -- The universe variable `r` is written first so that `ULift.{r} α` can be used
@@ -3525,7 +3525,7 @@ instance : DecidableEq String.Pos.Raw :=
 /--
 A region or slice of some underlying string.
 
-A substring contains an string together with the start and end byte positions of a region of
+A substring contains a string together with the start and end byte positions of a region of
 interest. Actually extracting a substring requires copying and memory allocation, while many
 substrings of the same underlying string may exist with very little overhead, and they are more
 convenient than tracking the bounds by hand.

src/Init/System/FilePath.lean

@@ -150,7 +150,7 @@ def parent (p : FilePath) : Option FilePath :=
 /--
 Extracts the last element of a path if it is a file or directory name.
 
-Returns `none ` if the last entry is a special name (such as `.` or `..`) or if the path is the root
+Returns `none` if the last entry is a special name (such as `.` or `..`) or if the path is the root
 directory.
 -/
 def fileName (p : FilePath) : Option String :=

src/Init/System/IO.lean

@@ -561,7 +561,7 @@ Waits for the task to finish, then returns its result.
   return t.get
 
 /--
-Waits until any of the tasks in the list has finished, then return its result.
+Waits until any of the tasks in the list has finished, then returns its result.
 -/
 @[extern "lean_io_wait_any"] opaque waitAny (tasks : @& List (Task α))
     (h : tasks.length > 0 := by exact Nat.zero_lt_succ _) : BaseIO α :=
@@ -679,7 +679,7 @@ File handles wrap the underlying operating system's file descriptors. There is n
 to close a file: when the last reference to a file handle is dropped, the file is closed
 automatically.
 
-Handles have an associated read/write cursor that determines the where reads and writes occur in the
+Handles have an associated read/write cursor that determines where reads and writes occur in the
 file.
 -/
 opaque FS.Handle : Type := Unit
@@ -790,15 +790,15 @@ An exception is thrown if the file cannot be opened.
 /--
 Acquires an exclusive or shared lock on the handle. Blocks to wait for the lock if necessary.
 
-Acquiring a exclusive lock while already possessing a shared lock will **not** reliably succeed: it
+Acquiring an exclusive lock while already possessing a shared lock will **not** reliably succeed: it
 works on Unix-like systems but not on Windows.
 -/
 @[extern "lean_io_prim_handle_lock"] opaque lock (h : @& Handle) (exclusive := true) : IO Unit
 /--
 Tries to acquire an exclusive or shared lock on the handle and returns `true` if successful. Will
 not block if the lock cannot be acquired, but instead returns `false`.
 
-Acquiring a exclusive lock while already possessing a shared lock will **not** reliably succeed: it
+Acquiring an exclusive lock while already possessing a shared lock will **not** reliably succeed: it
 works on Unix-like systems but not on Windows.
 -/
 @[extern "lean_io_prim_handle_try_lock"] opaque tryLock (h : @& Handle) (exclusive := true) : IO Bool
@@ -1350,7 +1350,7 @@ def withTempFile [Monad m] [MonadFinally m] [MonadLiftT IO m] (f : Handle → Fi
     removeFile path
 
 /--
-Creates a temporary directory in the most secure manner possible, providing a its path to an `IO`
+Creates a temporary directory in the most secure manner possible, providing its path to an `IO`
 action. Afterwards, all files in the temporary directory are recursively deleted, regardless of how
 or when they were created.
 
@@ -1480,7 +1480,7 @@ possible to close the child's standard input before the process terminates, whic
 @[extern "lean_io_process_spawn"] opaque spawn (args : SpawnArgs) : IO (Child args.toStdioConfig)
 
 /--
-Blocks until the child process has exited and return its exit code.
+Blocks until the child process has exited and returns its exit code.
 -/
 @[extern "lean_io_process_child_wait"] opaque Child.wait {cfg : @& StdioConfig} : @& Child cfg → IO UInt32
 
@@ -1586,7 +1586,7 @@ end Process
 /--
 POSIX-style file permissions.
 
-The `FileRight` structure describes these permissions for a file's owner, members of it's designated
+The `FileRight` structure describes these permissions for a file's owner, members of its designated
 group, and all others.
 -/
 structure AccessRight where
@@ -1863,7 +1863,7 @@ unsafe def Runtime.markPersistent (a : α) : BaseIO α := return a
 
 set_option linter.unusedVariables false in
 /--
-Discards the passed owned reference. This leads to `a` any any object reachable from it never being
+Discards the passed owned reference. This leads to `a` and any object reachable from it never being
 freed. This can be a useful optimization for eliding deallocation time of big object graphs that are
 kept alive close to the end of the process anyway (in which case calling `Runtime.markPersistent`
 would be similarly costly to deallocation). It is still considered a safe operation as it cannot

src/Init/WF.lean

@@ -463,7 +463,7 @@ variable {motive : α → Sort v}
 variable (h : α → Nat)
 variable (F : (x : α) → ((y : α) → InvImage (· < ·) h y x → motive y) → motive x)
 
-/-- Helper gadget that prevents reduction of `Nat.eager n` unless `n` evalutes to a ground term. -/
+/-- Helper gadget that prevents reduction of `Nat.eager n` unless `n` evaluates to a ground term. -/
 def Nat.eager (n : Nat) : Nat :=
   if Nat.beq n n = true then n else n
 
@@ -474,8 +474,8 @@ A well-founded fixpoint operator specialized for `Nat`-valued measures. Given a
 its higher order function argument `F` to invoke its argument only on values `y` that are smaller
 than `x` with regard to `h`.
 
-In contrast to to `WellFounded.fix`, this fixpoint operator reduces on closed terms. (More precisely:
-when `h x` evalutes to a ground value)
+In contrast to `WellFounded.fix`, this fixpoint operator reduces on closed terms. (More precisely:
+when `h x` evaluates to a ground value)
 
 -/
 def Nat.fix : (x : α) → motive x :=

src/Std/Data/ExtHashMap/Basic.lean

@@ -107,7 +107,7 @@ def containsThenInsertIfNew [EquivBEq α] [LawfulHashable α]
   ⟨replaced, ⟨r⟩⟩
 
 /--
-Checks whether a key is present in a map, returning the associate value, and inserts a value for
+Checks whether a key is present in a map, returning the associated value, and inserts a value for
 the key if it was not found.
 
 If the returned value is `some v`, then the returned map is unaltered. If it is `none`, then the

src/Std/Data/HashMap/Basic.lean

@@ -108,7 +108,7 @@ instance : LawfulSingleton (α × β) (HashMap α β) := ⟨fun _ => rfl⟩
   ⟨replaced, ⟨r⟩⟩
 
 /--
-Checks whether a key is present in a map, returning the associate value, and inserts a value for
+Checks whether a key is present in a map, returning the associated value, and inserts a value for
 the key if it was not found.
 
 If the returned value is `some v`, then the returned map is unaltered. If it is `none`, then the

src/Std/Do/SPred/DerivedLaws.lean

@@ -220,7 +220,7 @@ Decomposing assertions in postconditions into conjunctions of simpler predicates
 chance that automation will be able to prove the entailment of the postcondition and the next precondition.
 -/
 class IsAnd (P : SPred σs) (Q₁ Q₂ : outParam (SPred σs)) where
-  /-- A proof the the decomposition is logically equivalent to the original predicate. -/
+  /-- A proof that the decomposition is logically equivalent to the original predicate. -/
   to_and : P ⊣⊢ₛ Q₁ ∧ Q₂
 instance (σs) (Q₁ Q₂ : SPred σs) : IsAnd (σs:=σs) spred(Q₁ ∧ Q₂) Q₁ Q₂ where to_and := .rfl
 instance (σs) : IsAnd (σs:=σs) ⌜p ∧ q⌝ ⌜p⌝ ⌜q⌝ where to_and := pure_and.symm

src/Std/Internal/Async/Basic.lean

@@ -22,13 +22,13 @@ namespace Async
 This module provides a layered approach to asynchronous programming, combining monadic types,
 type classes, and concrete task types that work together in a cohesive system.
 
-- **Monadic Types**: These types provide a good way to to chain and manipulate context. These
+- **Monadic Types**: These types provide a good way to chain and manipulate context. These
   can contain a `Task`, enabling manipulation of both asynchronous and synchronous code.
 - **Concrete Task Types**: Concrete units of work that can be executed within these contexts.
 
 ## Monadic Types
 
-These types provide a good way to to chain and manipulate context. These can contain a `Task`,
+These types provide a good way to chain and manipulate context. These can contain a `Task`,
 enabling manipulation of both asynchronous and synchronous code.
 
 - `BaseAsync`: A monadic type for infallible asynchronous computations
@@ -548,7 +548,7 @@ def concurrentlyAll (xs : Array (BaseAsync α)) (prio := Task.Priority.default)
 
 /--
 Runs all computations concurrently and returns the result of the first one to finish.
-All other results are lost, and the tasks are not cancelled, so they'll continue their executing
+All other results are lost, and the tasks are not cancelled, so they'll continue their execution
 until the end.
 -/
 @[inline, specialize]
@@ -829,7 +829,7 @@ def concurrentlyAll (xs : Array (EAsync ε α)) (prio := Task.Priority.default)
 
 /--
 Runs all computations concurrently and returns the result of the first one to finish.
-All other results are lost, and the tasks are not cancelled, so they'll continue their executing
+All other results are lost, and the tasks are not cancelled, so they'll continue their execution
 until the end.
 -/
 @[inline, specialize]
@@ -969,7 +969,7 @@ def concurrentlyAll (xs : Array (Async α)) (prio := Task.Priority.default) : As
 
 /--
 Runs all computations concurrently and returns the result of the first one to finish.
-All other results are lost, and the tasks are not cancelled, so they'll continue their executing
+All other results are lost, and the tasks are not cancelled, so they'll continue their execution
 until the end.
 -/
 @[inline, specialize]

src/Std/Sync/Broadcast.lean

@@ -540,7 +540,7 @@ def recv [Inhabited α] (ch : Broadcast.Receiver α) : BaseIO (Task (Option α))
 open Internal.IO.Async in
 
 /--
-Creates a `Selector` that resolves once the broadcast channel `ch` has data available and provides that that data.
+Creates a `Selector` that resolves once the broadcast channel `ch` has data available and provides that data.
 -/
 @[inline]
 def recvSelector [Inhabited α] (ch : Broadcast.Receiver α) : Selector (Option α) :=

src/Std/Sync/Channel.lean

@@ -734,7 +734,7 @@ def recv (ch : CloseableChannel α) : BaseIO (Task (Option α)) :=
 
 open Internal.IO.Async in
 /--
-Creates a `Selector` that resolves once `ch` has data available and provides that that data.
+Creates a `Selector` that resolves once `ch` has data available and provides that data.
 In particular if `ch` is closed while waiting on this `Selector` and no data is available already
 this will resolve to `none`.
 -/

src/Std/Sync/Notify.lean

@@ -43,7 +43,7 @@ def Notify.Consumer.resolve (c : Consumer α) (x : α) : BaseIO Bool := do
     waiter.race lose win
 
 /--
-The central state structure for an a `Notify`.
+The central state structure for a `Notify`.
 -/
 structure Notify.State where
 

src/Std/Tactic/BVDecide/Syntax.lean

@@ -83,7 +83,7 @@ structure BVDecideConfig where
   -/
   maxSteps : Nat := Lean.Meta.Simp.defaultMaxSteps
   /--
-  Short-circuit multiplication as a abstraction-style optimization that triggers
+  Short-circuit multiplication as an abstraction-style optimization that triggers
   if matching multiplications are not needed to proof a goal.
   -/
   shortCircuit : Bool := false