chore: fix spelling mistakes (#8324)

Co-authored-by: euprunin <[email protected]>

Author: euprunin

doc/dev/release_checklist.md

@@ -69,7 +69,7 @@ We'll use `v4.6.0` as the intended release version as a running example.
     - `repl`:
       There are two copies of `lean-toolchain`/`lakefile.lean`:
       in the root, and in `test/Mathlib/`. Edit both, and run `lake update` in both directories.
-- An awkward situtation that sometimes occurs (e.g. with Verso) is that the `master`/`main` branch has already been moved
+- An awkward situation that sometimes occurs (e.g. with Verso) is that the `master`/`main` branch has already been moved
   to a nightly toolchain that comes *after* the stable toolchain we are
   targeting. In this case it is necessary to create a branch `releases/v4.6.0` from the last commit which was on
   an earlier toolchain, move that branch to the stable toolchain, and create the toolchain tag from that branch.

src/Init/Core.lean

@@ -944,7 +944,7 @@ theorem eqRec_heq {α : Sort u} {φ : α → Sort v} {a a' : α} : (h : a = a')
   | rfl, p => HEq.refl p
 
 /--
-Heterogenous equality with an `Eq.rec` application on the left is equivalent to a heterogenous
+Heterogeneous equality with an `Eq.rec` application on the left is equivalent to a heterogeneous
 equality on the original term.
 -/
 theorem eqRec_heq_iff {α : Sort u} {a : α} {motive : (b : α) → a = b → Sort v}
@@ -953,7 +953,7 @@ theorem eqRec_heq_iff {α : Sort u} {a : α} {motive : (b : α) → a = b → So
   h.rec (fun _ => ⟨id, id⟩) c
 
 /--
-Heterogenous equality with an `Eq.rec` application on the right is equivalent to a heterogenous
+Heterogeneous equality with an `Eq.rec` application on the right is equivalent to a heterogeneous
 equality on the original term.
 -/
 theorem heq_eqRec_iff {α : Sort u} {a : α} {motive : (b : α) → a = b → Sort v}

src/Init/Data/BitVec/Folds.lean

@@ -23,7 +23,7 @@ the final bitvector.
 It produces a sequence of state values `[s_0, s_1 .. s_w]` and a bitvector `v` where `f i s_i =
 (s_{i+1}, b_i)` and `b_i` is bit `i`th least-significant bit in `v` (e.g., `getLsb v i = b_i`).
 
-The theorem `iunfoldr_replace` allows uses of `BitVec.iunfoldr` to be replaced wiht declarative
+The theorem `iunfoldr_replace` allows uses of `BitVec.iunfoldr` to be replaced with declarative
 specifications that are easier to reason about.
 -/
 def iunfoldr (f : Fin w → α → α × Bool) (s : α) : α × BitVec w :=

src/Init/Data/Option/Coe.lean

@@ -11,7 +11,7 @@ import Init.Coe
 /-!
 In this file, we define the coercion `α → Option α`.
 
-The use of this coercion is **banned** in `Init` and `Std` (but allowed everwhere else). For this
+The use of this coercion is **banned** in `Init` and `Std` (but allowed everywhere else). For this
 reason, we define it in this file, which must not be imported anywhere in `Init` or `Std` (this
 is enforced by the test `importStructure.lean`).
 -/

src/Init/Prelude.lean

@@ -1818,7 +1818,7 @@ theorem Nat.succ_pos (n : Nat) : LT.lt 0 (succ n) :=
 
 set_option bootstrap.genMatcherCode false in
 /--
-The predecessor of a natural number is one less than it. The precedessor of `0` is defined to be
+The predecessor of a natural number is one less than it. The predecessor of `0` is defined to be
 `0`.
 
 This definition is overridden in the compiler with an efficient implementation. This definition is
@@ -1958,7 +1958,7 @@ instance instSubNat : Sub Nat where
   sub := Nat.sub
 
 /--
-Gets the word size of the curent platform. The word size may be 64 or 32 bits.
+Gets the word size of the current platform. The word size may be 64 or 32 bits.
 
 This function is opaque because there is no guarantee at compile time that the target will have the
 same word size as the host. It also helps avoid having type checking be architecture-dependent.
@@ -3409,7 +3409,7 @@ instance {ε : Type u} {α : Type v} [Inhabited ε] : Inhabited (Except ε α) w
 Exception monads provide the ability to throw errors and handle errors.
 
 In this class, `ε` is a `semiOutParam`, which means that it can influence the choice of instance.
-`MonadExcept ε` provides the same operations, but requires that `ε` be inferrable from `m`.
+`MonadExcept ε` provides the same operations, but requires that `ε` be inferable from `m`.
 
 `tryCatchThe`, which takes an explicit exception type, is used to desugar `try ... catch ...` steps
 inside `do`-blocks when the handlers have type annotations.
@@ -3589,7 +3589,7 @@ be read, but not written. A `MonadWithReader ρ` instance additionally allows th
 overridden for a sub-computation.
 
 In this class, `ρ` is a `semiOutParam`, which means that it can influence the choice of instance.
-`MonadReader ρ` provides the same operations, but requires that `ρ` be inferrable from `m`.
+`MonadReader ρ` provides the same operations, but requires that `ρ` be inferable from `m`.
 -/
 -- Note: This class can be seen as a simplification of the more "principled" definition
 -- ```
@@ -3641,7 +3641,7 @@ instance {ρ : Type u} {m : Type u → Type v} [Monad m] : MonadReaderOf ρ (Rea
 A reader monad that additionally allows the value to be locally overridden.
 
 In this class, `ρ` is a `semiOutParam`, which means that it can influence the choice of instance.
-`MonadWithReader ρ` provides the same operations, but requires that `ρ` be inferrable from `m`.
+`MonadWithReader ρ` provides the same operations, but requires that `ρ` be inferable from `m`.
 -/
 class MonadWithReaderOf (ρ : semiOutParam (Type u)) (m : Type u → Type v) where
   /--
@@ -3698,7 +3698,7 @@ Instances may implement these operations by passing state values around, by usin
 reference cell (e.g. `ST.Ref σ`), or in other ways.
 
 In this class, `σ` is a `semiOutParam`, which means that it can influence the choice of instance.
-`MonadState σ` provides the same operations, but requires that `σ` be inferrable from `m`.
+`MonadState σ` provides the same operations, but requires that `σ` be inferable from `m`.
 
 The mutable state of a state monad is visible between multiple `do`-blocks or functions, unlike
 [local mutable state](lean-manual://section/do-notation-let-mut) in `do`-notation.

src/Init/System/IO.lean

@@ -728,7 +728,7 @@ Use `IO.getStderr` to get the current standard error stream.
 /--
 Iterates an `IO` action. Starting with an initial state, the action is applied repeatedly until it
 returns a final value in `Sum.inr`. Each time it returns `Sum.inl`, the returned value is treated as
-a new sate.
+a new state.
 -/
 @[specialize] partial def iterate (a : α) (f : α → IO (Sum α β)) : IO β := do
   let v ← f a

src/Lean/Elab/Command.lean

@@ -236,7 +236,7 @@ private def runCore (x : CoreM α) : CommandElabM α := do
     nextMacroScope           := coreS.nextMacroScope
     ngen                     := coreS.ngen
     infoState.trees          := s.infoState.trees.append coreS.infoState.trees
-    -- we assume substitution of `assingment` has already happened, but for lazy assignments we only
+    -- we assume substitution of `assignment` has already happened, but for lazy assignments we only
     -- do it at the very end
     infoState.lazyAssignment := coreS.infoState.lazyAssignment
     traceState.traces        := coreS.traceState.traces.map fun t => { t with ref := replaceRef t.ref ctx.ref }

src/Lean/Elab/MutualDef.lean

@@ -1085,7 +1085,7 @@ where
       -- that depends only on a part of the ref
       addDeclarationRangesForBuiltin declId.declName view.modifiers.stx view.ref
   elabSync headers isRflLike := do
-    -- If the reflexivity holds publically as well (we're still inside `withExporting` here), export
+    -- If the reflexivity holds publicly as well (we're still inside `withExporting` here), export
     -- the body even if it is a theorem so that it is recognized as a rfl theorem even without
     -- `import all`.
     let rflPublic ← pure isRflLike <&&> pure (← getEnv).header.isModule <&&>

src/Lean/Elab/StructInst.lean

@@ -1217,7 +1217,7 @@ private def expandNonAtomicExplicitSources (stx : Syntax) : TermElabM (Option Sy
 where
   /--
   If the source is a local, we can use it.
-  *However*, we need to watch out that the local doesn't have implicit arguemnts,
+  *However*, we need to watch out that the local doesn't have implicit arguments,
   since that could cause multiple evaluation.
   For simplicity, we just check that the fvar isn't a forall.
   -/

src/Lean/Elab/Structure.lean

@@ -855,7 +855,7 @@ private def registerFailedToInferDefaultValue (fieldName : Name) (e : Expr) (ref
 Goes through all the natural mvars appearing in `e`, assigning any whose type is one of the inherited parents.
 
 Rationale 1: Structures can only extend a parent once.
-There should be no other occurences of a parent except for the parent itself.
+There should be no other occurrences of a parent except for the parent itself.
 
 Rationale 2: Consider the following code in the test `lean/run/balg.lean`:
 ```lean