chore: fix spelling mistakes (#8711)

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

Author: euprunin

src/Init/Grind/Tactics.lean

@@ -55,7 +55,7 @@ and stores `c` in `x`, `b` in `a`, and the proof that `c = some b` in `h`.
 -/
 def genPattern {α : Sort u} (_h : Prop) (x : α) (_val : α) : α := x
 
-/-- Similar to `genPattern` but for the heterogenous case -/
+/-- Similar to `genPattern` but for the heterogeneous case -/
 def genHEqPattern {α β : Sort u} (_h : Prop) (x : α) (_val : β) : α := x
 end Lean.Grind
 

src/Lean/Elab/Tactic/Induction.lean

@@ -243,10 +243,10 @@ def setMotiveArg (mvarId : MVarId) (motiveArg : MVarId) (targets : Array FVarId)
       if (← isTypeCorrect absType') then
         absType := absType'
       else
-        trace[Elab.induction] "Not abstracing goal over {complexArg}, resulting term is not type correct:{indentExpr absType'} }"
+        trace[Elab.induction] "Not abstracting goal over {complexArg}, resulting term is not type correct:{indentExpr absType'} }"
         absType := .lam (← mkFreshUserName `x) complexArgType absType .default
     else
-      trace[Elab.induction] "Not abstracing goal over {complexArg}, its type {complexArgType} does not match the expected {exptComplexArgType}"
+      trace[Elab.induction] "Not abstracting goal over {complexArg}, its type {complexArgType} does not match the expected {exptComplexArgType}"
       absType := .lam (← mkFreshUserName `x) exptComplexArgType absType .default
 
   let motive ← mkLambdaFVars (targets.map mkFVar) absType

src/Lean/EnvExtension.lean

@@ -151,7 +151,7 @@ def insert (ext : MapDeclarationExtension α) (env : Environment) (declName : Na
   have : Inhabited Environment := ⟨env⟩
   assert! env.getModuleIdxFor? declName |>.isNone -- See comment at `MapDeclarationExtension`
   if !env.asyncMayContain declName then
-    panic! s!"MapDeclarationExtension.insert: cannot insert {declName} into {ext.name}, it is not contined in {env.asyncPrefix?}"
+    panic! s!"MapDeclarationExtension.insert: cannot insert {declName} into {ext.name}, it is not contained in {env.asyncPrefix?}"
   else
     ext.addEntry env (declName, val)
 

src/Lean/Environment.lean

@@ -1859,7 +1859,7 @@ partial def importModulesCore
     ImportStateM Unit := go imports (importAll := true) (isExported := isModule)
 /-
 When the module system is disabled for the root, we import all transitively referenced modules and
-ignore any module sytem annotations on the way.
+ignore any module system annotations on the way.
 
 When the module system is enabled for the root, each module may need to be imported at one of the
 following levels:

src/Lean/Linter/Basic.lean

@@ -37,7 +37,7 @@ This structure contains all the data required to do so, the `Options` set on the
 or by the `set_option` command, and the `LinterSets` that have been declared.
 
 A single structure holding this data is useful since we want `getLinterValue` to be a pure
-function: determinining the `LinterSets` would otherwise require a `MonadEnv` instance.
+function: determining the `LinterSets` would otherwise require a `MonadEnv` instance.
 -/
 structure LinterOptions where
   toOptions : Options

src/Lean/Meta/Constructions/NoConfusionLinear.lean

@@ -10,7 +10,7 @@ import Lean.Meta.CompletionName
 
 /-!
 This module produces a construction for the `noConfusionType` that is linear in size in the number of
-constructors of the inductive type. This is in contrast to the previous construction (definde in
+constructors of the inductive type. This is in contrast to the previous construction (defined in
 `no_confusion.cpp`), that is quadratic in size due to nested `.brecOn` applications.
 
 We still use the old construction when processing the prelude, for the few inductives that we need

src/Lean/Meta/Tactic/FunInd.lean

@@ -1506,7 +1506,7 @@ where doRealize inductName := do
 
 /--
 Given an expression `fun x y z => body`, returns a bit mask of the functinon's arity length
-that has `true` whenver that parameter of the function appears as a scrutinee of a `match` in
+that has `true` whenever that parameter of the function appears as a scrutinee of a `match` in
 tail position. These are the parameters that are likely useful as targets of the motive
 of the functional cases theorem. All others become parameters or may be dropped.
 

src/Lean/Meta/Tactic/Grind/EMatch.lean

@@ -407,7 +407,7 @@ private def applyAssignment (mvars : Array Expr) : OptionT (StateT Choice M) Uni
         theorem getElem_reverse {xs : Array α} {i : Nat} (hi : i < xs.reverse.size) :
           (xs.reverse)[i] = xs[xs.size - 1 - i]'(by simp at hi; omega)
         ```
-        The pattern for this theorem is `xs.reverese[i]`. Note that `hi` occurs there as an implicit argument.
+        The pattern for this theorem is `xs.reverse[i]`. Note that `hi` occurs there as an implicit argument.
         The term `xs[j]` in our goal e-matches the pattern because we have the equality `xs.reverse = xs`.
         However, the implicit proof at `xs[j]` has type `j < xs.size` instead of `j < xs.reverse.size`.
         -/

src/Lean/Setup.lean

@@ -15,7 +15,7 @@ Data types used by Lean module headers and the `--setup` CLI.
 
 namespace Lean
 
-/- Abstract sturcture of an `import` statement. -/
+/- Abstract structure of an `import` statement. -/
 structure Import where
   module     : Name
   /-- `import all`; whether to import and expose all data saved by the module. -/

src/Std/Data/Iterators.lean

@@ -67,7 +67,7 @@ steps are called productive. This behavior is encoded in the `Std.Iterators.Prod
 ## Stability
 
 The API for the usage of iterators provided in this module can be considered stable, as well as
-the API for the verification of programms using iterators, unless explicitly stated otherwise.
+the API for the verification of programs using iterators, unless explicitly stated otherwise.
 
 Contrarily, the API for implementation of new iterators, including the design of the `Iterator`
 typeclass, is still experimental and will change in the future. It is already planned that there