chore: fix spelling errors (#13274)

This PR fixed typos:

```
pip install codespell --upgrade
codespell --summary --ignore-words-list enew,forin,fro,happend,hge,ihs,iterm,spred --skip stage0 --check-filenames
codespell --summary --ignore-words-list enew,forin,fro,happend,hge,ihs,iterm,spred --skip stage0 --check-filenames --regex '[A-Z][a-z]*'
codespell --summary --ignore-words-list enew,forin,fro,happend,hge,ihs,iterm,spred --skip stage0 --check-filenames --regex "\b[a-z']*"
```

src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean

@@ -271,7 +271,7 @@ private def optionPelim' {α : Type u_1} (t : Option α) {β :  Sort u_2}
 
 /--
 Inserts an `Option` case distinction after the first computation of a call to `MonadAttach.pbind`.
-This lemma is useful for simplifying the second computation, which often involes `match` expressions
+This lemma is useful for simplifying the second computation, which often involves `match` expressions
 that use `pbind`'s proof term.
 -/
 private theorem pbind_eq_pbind_if_isSome [Monad m] [MonadAttach m] (x : m (Option α)) (f : (_ : _) → _ → m β) :

src/Init/Data/String/Lemmas/Iterate.lean

@@ -31,7 +31,7 @@ namespace Slice
 /--
 A list of all positions starting at {name}`p`.
 
-This function is not meant to be used in actual progams. Actual programs should use
+This function is not meant to be used in actual programs. Actual programs should use
 {name}`Slice.positionsFrom` or {name}`Slice.positions`.
 -/
 protected def Model.positionsFrom {s : Slice} (p : s.Pos) : List { p : s.Pos // p ≠ s.endPos } :=
@@ -206,7 +206,7 @@ end Slice
 /--
 A list of all positions starting at {name}`p`.
 
-This function is not meant to be used in actual progams. Actual programs should use
+This function is not meant to be used in actual programs. Actual programs should use
 {name}`Slice.positionsFrom` or {name}`Slice.positions`.
 -/
 protected def Model.positionsFrom {s : String} (p : s.Pos) : List { p : s.Pos // p ≠ s.endPos } :=

src/Init/Data/String/Subslice.lean

@@ -23,7 +23,7 @@ Given a {name}`Slice` {name}`s`, the type {lean}`s.Subslice` is the type of half
 in {name}`s` delineated by a valid position on both sides.
 
 This type is useful to track regions of interest within some larger slice that is also of interest.
-In contrast, {name}`Slice` is used to track regions of interest whithin some larger string that is
+In contrast, {name}`Slice` is used to track regions of interest within some larger string that is
 not or no longer relevant.
 
 Equality on {name}`Subslice` is somewhat better behaved than on {name}`Slice`, but note that there

src/Lean/Compiler/LCNF/ResetReuse.lean

@@ -28,7 +28,7 @@ inserts addition instructions to attempt to reuse the memory right away instead
 allocator.
 
 For this the paper defines three functions:
-- `R` (called `Decl.insertResetReuse` here) which looks for candidates that might be elligible for
+- `R` (called `Decl.insertResetReuse` here) which looks for candidates that might be eligible for
   reuse. For these variables it invokes `D`.
 - `D` which looks for code regions in which the target variable is dead (i.e. no longer read from),
   it then invokes `S`. If `S` succeeds it inserts a `reset` instruction to match the `reuse`

src/Lean/Compiler/LCNF/SimpCase.lean

@@ -24,7 +24,7 @@ In particular we perform:
 - folding of the most common cases arm into the default arm if possible
 
 Note: Currently the simplifier still contains almost equivalent simplifications to the ones shown
-here. We know that this causes unforseen behavior and do plan on changing it eventually.
+here. We know that this causes unforeseen behavior and do plan on changing it eventually.
 -/
 
 -- TODO: the following functions are duplicated from simp and should be deleted in simp once we

src/Lean/Compiler/LCNF/ToDecl.lean

@@ -171,7 +171,7 @@ def toDecl (declName : Name) : CompilerM (Decl .pure) := do
     if compiler.ignoreBorrowAnnotation.get (← getOptions) then
       decl := { decl with params := ← decl.params.mapM (·.updateBorrow false) }
     if isExport env decl.name && decl.params.any (·.borrow) then
-      throwError m!" Declaration {decl.name} is marked as `export` but some of its parameters have borrow annotations.\n Consider using `set_option compiler.ignoreBorrowAnnotation true in` to supress the borrow annotations in its type.\n If the declaration is part of an `export`/`extern` pair make sure to also supress the annotations at the `extern` declaration."
+      throwError m!" Declaration {decl.name} is marked as `export` but some of its parameters have borrow annotations.\n Consider using `set_option compiler.ignoreBorrowAnnotation true in` to suppress the borrow annotations in its type.\n If the declaration is part of an `export`/`extern` pair make sure to also suppress the annotations at the `extern` declaration."
     return decl
 
 end Lean.Compiler.LCNF

src/Lean/Elab/Deriving/DecEq.lean

@@ -111,7 +111,7 @@ def mkMatchNew (ctx : Context) (header : Header) (indVal : InductiveVal) : TermE
   let x1 := mkIdent header.targetNames[0]!
   let x2 := mkIdent header.targetNames[1]!
   let ctorIdxName := mkCtorIdxName indVal.name
-  -- NB: the getMatcherInfo? assumes all mathcers are called `match_`
+  -- NB: the getMatcherInfo? assumes all matchers are called `match_`
   let casesOnSameCtorName ← mkFreshUserName (indVal.name ++ `match_on_same_ctor)
   mkCasesOnSameCtor casesOnSameCtorName indVal.name
   let alts ← Array.ofFnM (n := indVal.numCtors) fun ⟨ctorIdx, _⟩ => do

src/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean

@@ -36,7 +36,7 @@ def mkContext (lratPath : System.FilePath) (cfg : BVDecideConfig) : TermElabM Ta
   TacticContext.new lratPath cfg
 
 /--
-Prepare an `Expr` that proves `bvExpr.unsat` using native evalution.
+Prepare an `Expr` that proves `bvExpr.unsat` using native evaluation.
 -/
 def lratChecker (ctx : TacticContext) (reflectionResult : ReflectionResult) : MetaM Expr := do
   let cert ← LratCert.ofFile ctx.lratPath ctx.config.trimProofs

src/Lean/Meta/Match/Match.lean

@@ -33,12 +33,12 @@ The high-level overview of moves are
   * If there is an alternative, solve its constraints
   * Else use `contradiction` to prove completeness of the match
 * Process “independent prefixes” of patterns. These are patterns that can be processed without
-  affecting the aother alternatives, and without side effects in the sense of updating the `mvarId`.
+  affecting the other alternatives, and without side effects in the sense of updating the `mvarId`.
   These are
   - variable patterns; substitute
   - inaccessible patterns; add equality constraints
   - as-patterns: substitute value and equality
-  After thes have been processed, we use `.inaccessible x` where `x` is the variable being matched
+  After these have been processed, we use `.inaccessible x` where `x` is the variable being matched
   to mark them as “done”.
 * If all patterns start with “done”, drop the first variable
 * The first alt has only “done” patterns, drop remaining alts (they're overlapped)

src/Lean/Meta/Match/Rewrite.lean

@@ -17,7 +17,7 @@ namespace Lean.Meta
 
 /--
 Tries to rewrite the `ite`, `dite` or `cond` expression `e` with the hypothesis `hc`.
-If it fails, it returns a rewrite with `proof? := none` and unchaged expression.
+If it fails, it returns a rewrite with `proof? := none` and unchanged expression.
 -/
 def rwIfWith (hc : Expr) (e : Expr) : MetaM Simp.Result := do
   match_expr e with

src/Lean/Meta/Native.lean

@@ -22,9 +22,9 @@ of that computation as an axiom towards the logic.
 -/
 
 public inductive NativeEqTrueResult where
-  /-- The given expression `e` evalutes to true. `prf` is a proof of `e = true`. -/
+  /-- The given expression `e` evaluates to true. `prf` is a proof of `e = true`. -/
   | success (prf : Expr)
-  /-- The given expression `e` evalutes to false. -/
+  /-- The given expression `e` evaluates to false. -/
   | notTrue
 
 /--

src/Lean/Meta/SameCtorUtils.lean

@@ -14,7 +14,7 @@ This module contains utilities for dealing with equalities between constructor a
 in particular about which fields must be the same a-priori for the equality to type check.
 
 Users include (or will include) the injectivity theorems, the per-constructor no-confusion
-construction and deriving type classes lik `BEq`, `DecidableEq` or `Ord`.
+construction and deriving type classes like `BEq`, `DecidableEq` or `Ord`.
 -/
 
 namespace Lean.Meta

src/Lean/Meta/Sym/AbstractS.lean

@@ -97,4 +97,16 @@ public def mkLambdaFVarsS (xs : Array Expr) (e : Expr) : SymM Expr := do
     let type ← abstractFVarsRange decl.type i xs
     mkLambdaS decl.userName decl.binderInfo type b
 
+/--
+Similar to `mkForallFVars`, but uses the more efficient `abstractFVars` and `abstractFVarsRange`,
+and makes the same assumption made by these functions.
+-/
+public def mkForallFVarsS (xs : Array Expr) (e : Expr) : SymM Expr := do
+  let b ← abstractFVars e xs
+  xs.size.foldRevM (init := b) fun i _ b => do
+    let x := xs[i]
+    let decl ← x.fvarId!.getDecl
+    let type ← abstractFVarsRange decl.type i xs
+    mkForallS decl.userName decl.binderInfo type b
+
 end Lean.Meta.Sym

src/Lean/Meta/Sym/AlphaShareBuilder.lean

@@ -189,4 +189,48 @@ def mkAppS₄ (f a₁ a₂ a₃ a₄ : Expr) : m Expr := do
 def mkAppS₅ (f a₁ a₂ a₃ a₄ a₅ : Expr) : m Expr := do
   mkAppS (← mkAppS₄ f a₁ a₂ a₃ a₄) a₅
 
+def mkAppS₆ (f a₁ a₂ a₃ a₄ a₅ a₆ : Expr) : m Expr := do
+  mkAppS (← mkAppS₅ f a₁ a₂ a₃ a₄ a₅) a₆
+
+def mkAppS₇ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ : Expr) : m Expr := do
+  mkAppS (← mkAppS₆ f a₁ a₂ a₃ a₄ a₅ a₆) a₇
+
+def mkAppS₈ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ : Expr) : m Expr := do
+  mkAppS (← mkAppS₇ f a₁ a₂ a₃ a₄ a₅ a₆ a₇) a₈
+
+def mkAppS₉ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ : Expr) : m Expr := do
+  mkAppS (← mkAppS₈ f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈) a₉
+
+def mkAppS₁₀ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ a₁₀ : Expr) : m Expr := do
+  mkAppS (← mkAppS₉ f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉) a₁₀
+
+def mkAppS₁₁ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ a₁₀ a₁₁ : Expr) : m Expr := do
+  mkAppS (← mkAppS₁₀ f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ a₁₀) a₁₁
+
+/-- `mkAppRangeS f i j #[a₀, ..., aᵢ, ..., aⱼ, ...]` ==> `f aᵢ ... aⱼ₋₁` with max sharing. -/
+partial def mkAppRangeS (f : Expr) (beginIdx endIdx : Nat) (args : Array Expr) : m Expr :=
+  go endIdx f beginIdx
+where
+  go (endIdx : Nat) (b : Expr) (i : Nat) : m Expr := do
+    if endIdx ≤ i then return b
+    else go endIdx (← mkAppS b args[i]!) (i + 1)
+
+/-- `mkAppNS f #[a₀, ..., aₙ]` constructs `f a₀ ... aₙ` with max sharing. -/
+def mkAppNS (f : Expr) (args : Array Expr) : m Expr :=
+  mkAppRangeS f 0 args.size args
+
+/-- `mkAppRevRangeS f b e revArgs` ==> `mkAppRev f (revArgs.extract b e)` with max sharing. -/
+partial def mkAppRevRangeS (f : Expr) (beginIdx endIdx : Nat) (revArgs : Array Expr) : m Expr :=
+  go revArgs beginIdx f endIdx
+where
+  go (revArgs : Array Expr) (start : Nat) (b : Expr) (i : Nat) : m Expr := do
+    if i ≤ start then return b
+    else
+      let i := i - 1
+      go revArgs start (← mkAppS b revArgs[i]!) i
+
+/-- Same as `mkAppS f args` but reversing `args`, with max sharing. -/
+def mkAppRevS (f : Expr) (revArgs : Array Expr) : m Expr :=
+  mkAppRevRangeS f 0 revArgs.size revArgs
+
 end Lean.Meta.Sym.Internal

src/Lean/Meta/Sym/Canon.lean

@@ -24,14 +24,19 @@ builtin_initialize registerTraceClass `sym.debug.canon
 
 Canonicalizes expressions by normalizing types and instances. At the top level, it traverses
 applications, foralls, lambdas, and let-bindings, classifying each argument as a type, instance,
-implicit, or value using `shouldCanon`. Values are recursively visited but not normalized.
-Types and instances receive targeted reductions.
+implicit, or value using `shouldCanon`. Targeted reductions (projection, match/ite/cond, Nat
+arithmetic) are applied to all positions; instances are re-synthesized.
 
 **Note about types:** `grind` is not built for reasoning about types that are not propositions.
 We assume that definitionally equal types will be structurally identical after we apply the
 canonicalizer. We also erase most of the subsingleton markers occurring inside types.
 
-## Reductions (applied only in type positions)
+## Reductions
+
+It also normalizes expressions using the following reductions. We can view it as a cheap/custom `dsimp`.
+We used to reduce only terms inside types, but it restricted important normalizations that were important
+when, for example, a term had a forward dependency. That is, the term is not directly in a type, but
+there is a type that depends on it.
 
 - **Eta**: `fun x => f x` → `f`
 - **Projection**: `⟨a, b⟩.1` → `a` (structure projections, not class projections)
@@ -39,6 +44,9 @@ canonicalizer. We also erase most of the subsingleton markers occurring inside t
 - **Nat arithmetic**: ground evaluation (`2 + 1` → `3`) and offset normalization
   (`n.succ + 1` → `n + 2`)
 
+**Note**: Eta is applied only if the lambda is occurring inside of a type. For lambdas occurring
+in non type positions, we want to leverage the support in `grind` for lambda-expressions.
+
 ## Instance canonicalization
 
 Instances are re-synthesized via `synthInstance`. The instance type is first normalized
@@ -55,7 +63,11 @@ produce the same canonical instance. Two special cases:
   canonicalized, then the proof is re-synthesized. If resynthesis fails, the original
   proof is kept. No definitional-equality check is needed thanks to proof irrelevance.
 
-Inside types, both cases are strict: resynthesis failure is reported as an issue.
+In both cases, resynthesis failure is silent — the original instance or proof is kept.
+Ideally we would report an issue when resynthesis fails inside a type (where structural
+agreement matters most), but in practice users provide non-synthesizable instances via `haveI`,
+and these instances propagate into types through forward dependencies. Reporting failures
+for such instances produces noise that obscures real issues.
 
 ## Two caches
 
@@ -229,7 +241,7 @@ def checkDefEqInst (e : Expr) (inst : Expr) : SymM Expr := do
     return e
   return inst
 
-/-- Canonicalize `e`. Applies targeted reductions in type positions; recursively visits value positions. -/
+/-- Canonicalize `e`. Applies targeted reductions and re-synthesizes instances. -/
 partial def canon (e : Expr) : CanonM Expr := do
   match e with
   | .forallE ..    => withCaching e <| canonForall #[] e
@@ -264,11 +276,12 @@ where
 
   /--
   Canonicalize `e : type` where `e` is an instance by trying to resynthesize `type`.
-  We report an issue if the instance cannot be resynthesized.
+  If `report` is `true`, we report an issue when the instance cannot be resynthesized.
   -/
-  canonInstCore (e : Expr) (type : Expr) : CanonM Expr := do
+  canonInstCore (e : Expr) (type : Expr) (report := true) : CanonM Expr := do
     let some inst ← Sym.synthInstance? type |
-      reportIssue! "failed to canonicalize instance{indentExpr e}\nfailed to synthesize{indentExpr type}"
+      if report then
+        reportIssue! "failed to canonicalize instance{indentExpr e}\nfailed to synthesize{indentExpr type}"
       return e
     checkDefEqInst e inst
 
@@ -276,18 +289,18 @@ where
   Canonicalize an instance by trying to resynthesize it without caching.
   Recall that we have special support for `Decidable` and propositional instances.
   -/
-  canonInst' (e : Expr) : CanonM Expr := do
+  canonInst' (e : Expr) (report := true) : CanonM Expr := do
     /-
     We normalize the type to make sure `OfNat (Fin (2+1)) 1` and `OfNat (Fin 3) 1` will produce
     the same instances.
     -/
     let type ← inferType e
     let type' ← canonInsideType' type
-    canonInstCore e type'
+    canonInstCore e type' report
 
   /-- `withCaching` + `canonInst'` -/
-  canonInst (e : Expr) : CanonM Expr := withCaching e do
-    canonInst' e
+  canonInst (e : Expr) (report := true) : CanonM Expr := withCaching e do
+    canonInst' e report
 
   /--
   Canonicalize a proposition that is also a term instance.
@@ -300,7 +313,9 @@ where
   canonInstProp (g : Expr) (prop : Expr) (h : Expr) (e : Expr) : CanonM Expr := withCaching e do
     let prop' ← canon prop
     if (← read).insideType then
-      canonInstCore h prop'
+      /- We suppress reporting here because `haveI`-provided instances propagate into types
+         through forward dependencies, and reporting them produces noise. See module doc. -/
+      canonInstCore h prop' (report := false)
     else
       /-
       **Note**: We try to resynthesize the proposition, but if it fails we keep the current one.
@@ -322,7 +337,8 @@ where
     let prop' ← canon prop
     let type := mkApp (mkConst ``Decidable) prop'
     if (← read).insideType then
-      canonInstCore inst type
+      /- See comment in `canonInstProp` for why we suppress reporting here. -/
+      canonInstCore inst type (report := false)
     else
       /-
       **Note**: We try to resynthesize the instance, but if it fails we keep the current one.
@@ -338,6 +354,12 @@ where
   canonInstDec (g : Expr) (prop : Expr) (h : Expr) (e : Expr) : CanonM Expr := withCaching e do
     canonInstDec' g prop h e
 
+  /-- `canonInstDec` variant for normalizing `if-then-else` expressions. -/
+  canonInstDecCore (e : Expr) : CanonM Expr := do
+    match_expr e with
+    | g@Grind.nestedDecidable prop inst => canonInstDec g prop inst e
+    | _  => canonInst e (report := false)
+
   canonLambda (e : Expr) : CanonM Expr := do
     if (← read).insideType then
       canonLambdaLoop #[] (etaReduce e)
@@ -418,7 +440,7 @@ where
     let c ← canon c
     if isTrueCond c then canon a
     else if isFalseCond c then canon b
-    else return mkApp5 f (← canonInsideType α) c (← canonInst inst) (← canon a) (← canon b)
+    else return mkApp5 f (← canonInsideType α) c (← canonInstDecCore inst) (← canon a) (← canon b)
 
   canonCond (f : Expr) (α c a b : Expr) : CanonM Expr := do
     let c ← canon c
@@ -459,27 +481,21 @@ where
         return e
 
   canonApp (e : Expr) : CanonM Expr := do
-    if (← read).insideType then
-      match_expr e with
-      | f@ite α c i a b => canonIte f α c i a b
-      | f@cond α c a b => canonCond f α c a b
-      -- Remark: We currently don't normalize dependent-if-then-else occurring in types.
-      | _ =>
-        let f := e.getAppFn
-        let .const declName _ := f | canonAppAndPost e
-        if (← isMatcher declName) then
-          canonMatch e
-        else
-          canonAppAndPost e
-    else
-      canonAppDefault e
+    match_expr e with
+    | f@ite α c i a b => canonIte f α c i a b
+    | f@cond α c a b => canonCond f α c a b
+    -- Remark: We currently don't normalize dependent-if-then-else occurring in types.
+    | _ =>
+      let f := e.getAppFn
+      let .const declName _ := f | canonAppAndPost e
+      if (← isMatcher declName) then
+        canonMatch e
+      else
+        canonAppAndPost e
 
   canonProj (e : Expr) : CanonM Expr := do
     let e := e.updateProj! (← canon e.projExpr!)
-    if (← read).insideType then
-      return (← reduceProj? e).getD e
-    else
-      return e
+    return (← reduceProj? e).getD e
 
 /--
 Returns `true` if `shouldCanon pinfos i arg` is not `.visit`.
@@ -493,8 +509,8 @@ end Canon
 
 /--
 Canonicalize `e` by normalizing types, instances, and support arguments.
-Types receive targeted reductions (eta, projection, match/ite, Nat arithmetic).
-Instances are re-synthesized. Values are traversed but not reduced.
+Applies targeted reductions (projection, match/ite/cond, Nat arithmetic) in all positions;
+eta reduction is applied only inside types. Instances are re-synthesized.
 Runs at reducible transparency.
 -/
 public def canon (e : Expr) : SymM Expr := do profileitM Exception "sym canon" (← getOptions) do

src/Lean/Meta/Sym/InstantiateS.lean

@@ -86,22 +86,8 @@ It assumes the input is maximally shared, and ensures the output is too.
 public def instantiateS  (e : Expr) (subst : Array Expr) : SymM Expr :=
   liftBuilderM <| instantiateS' e subst
 
-/-- `mkAppRevRangeS f b e args == mkAppRev f (revArgs.extract b e)` -/
-def mkAppRevRangeS (f : Expr) (beginIdx endIdx : Nat) (revArgs : Array Expr) : AlphaShareBuilderM Expr :=
-  loop revArgs beginIdx f endIdx
-where
-  loop (revArgs : Array Expr) (start : Nat) (b : Expr) (i : Nat) : AlphaShareBuilderM Expr := do
-  if i ≤ start then
-    return b
-  else
-    let i := i - 1
-    loop revArgs start (← mkAppS b revArgs[i]!) i
-
-/--
-Beta-reduces `f` applied to reversed arguments `revArgs`, ensuring maximally shared terms.
-`betaRevS f #[a₃, a₂, a₁]` computes the beta-normal form of `f a₁ a₂ a₃`.
--/
-partial def betaRevS (f : Expr) (revArgs : Array Expr) : AlphaShareBuilderM Expr :=
+/-- Internal variant of `betaRevS` that runs in `AlphaShareBuilderM`. -/
+private partial def betaRevS' (f : Expr) (revArgs : Array Expr) : AlphaShareBuilderM Expr :=
   if revArgs.size == 0 then
     return f
   else
@@ -173,7 +159,7 @@ where
     | .bvar bidx =>
       let f' ← visitBVar f bidx offset
       if modified || !isSameExpr f f' then
-        betaRevS f' argsRev
+        betaRevS' f' argsRev
       else
         return e
     | _ => unreachable!
@@ -215,4 +201,18 @@ public def instantiateRevBetaS (e : Expr) (subst : Array Expr) : SymM Expr := do
   if !e.hasLooseBVars || subst.isEmpty then return e
   else liftBuilderM <| instantiateRevBetaS' e subst
 
+/--
+Beta-reduces `f` applied to reversed arguments `revArgs`, ensuring maximally shared terms.
+`betaRevS f #[a₃, a₂, a₁]` computes the beta-normal form of `f a₁ a₂ a₃`.
+-/
+public def betaRevS (f : Expr) (revArgs : Array Expr) : SymM Expr :=
+  liftBuilderM <| betaRevS' f revArgs
+
+/--
+Apply the given arguments to `f`, beta-reducing if `f` is a lambda expression,
+ensuring maximally shared terms. See `betaRevS` for details.
+-/
+public def betaS (f : Expr) (args : Array Expr) : SymM Expr :=
+  betaRevS f args.reverse
+
 end Lean.Meta.Sym

src/Lean/Meta/Tactic/Cbv/ControlFlow.lean

@@ -44,7 +44,7 @@ def isCbvNoncomputable (p : Name) : CoreM Bool := do
   return evalLemmas.isNone && Lean.isNoncomputable (← getEnv) p
 
 /--
-Attemps to synthesize `Decidable p` instance and guards against picking up a `noncomputable` instance
+Attempts to synthesize `Decidable p` instance and guards against picking up a `noncomputable` instance
 -/
 def trySynthComputableInstance (p : Expr) : SymM <| Option Expr := do
   let .some inst' ← trySynthInstance (mkApp (mkConst ``Decidable) p) | return .none
@@ -112,7 +112,7 @@ builtin_cbv_simproc ↓ simpIteCbv (@ite _ _ _ _ _) := fun e => do
       else if (← isFalseExpr c') then
         return .step b (mkApp (e.replaceFn ``ite_cond_eq_false) h) (contextDependent := cd)
       else
-        -- If we got stuck with simplifying `p` then let's try evaluating the original isntance
+        -- If we got stuck with simplifying `p` then let's try evaluating the original instance
         simpAndMatchIteDecidable f α c inst a b do
           -- If we get stuck here, maybe the problem is that we need to look at `Decidable c'`
           let inst' := mkApp4 (mkConst ``decidable_of_decidable_of_eq) c c' inst h
@@ -317,7 +317,7 @@ public def reduceRecMatcher : Simproc := fun e => do
   else
     return .rfl
 
-builtin_cbv_simproc ↓ simpDecidableRec (@Decidable.rec _ _ _ _ _) := 
+builtin_cbv_simproc ↓ simpDecidableRec (@Decidable.rec _ _ _ _ _) :=
   (simpInterlaced · #[false,false,false,false,true]) >> reduceRecMatcher
 
 def tryMatchEquations (appFn : Name) : Simproc := fun e => do

src/Lean/Meta/Tactic/Cbv/Main.lean

@@ -272,7 +272,7 @@ def handleProj : Simproc := fun e => do
         let reduced ← Sym.share reduced
         return .step reduced (← Sym.mkEqRefl reduced)
       | .none =>
-       -- If we failed to reduce it, we turn to a last resort; we try use heterogenous congruence lemma that we then try to turn into an equality.
+       -- If we failed to reduce it, we turn to a last resort; we try use heterogeneous congruence lemma that we then try to turn into an equality.
         unless (← isDefEq struct e') do
           -- If we rewrote the projection body using something that holds up to propositional equality, then there is nothing we can do.
           -- TODO: Check if there is a need to report this to a user, or shall we fail silently.
@@ -283,6 +283,7 @@ def handleProj : Simproc := fun e => do
         let newProof ← mkEqOfHEq newProof (check := false)
         return .step (← Lean.Expr.updateProjS! e e') newProof
 
+open Sym.Internal in
 /--
 For an application whose head is neither a constant nor a lambda (e.g. a projection
 like `p.1 x`), simplify the function head and lift the proof via `congrArg`.

src/Lean/Meta/Tactic/Cbv/Util.lean

@@ -24,9 +24,6 @@ namespace Lean.Meta.Tactic.Cbv
 
 open Lean.Meta.Sym.Simp
 
-public def mkAppNS (f : Expr) (args : Array Expr) : Sym.SymM Expr := do
-  args.foldlM Sym.Internal.mkAppS f
-
 abbrev isNatValue (e : Expr) : Bool := (Sym.getNatValue? e).isSome
 abbrev isStringValue (e : Expr) : Bool := (Sym.getStringValue? e).isSome
 abbrev isIntValue (e : Expr) : Bool := (Sym.getIntValue? e).isSome

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

@@ -172,7 +172,7 @@ private partial def addEqStep (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit
       trueEqFalse := true
     else
       let hasHEq := isHEq || lhsRoot.heqProofs || rhsRoot.heqProofs
-      -- **Note**: We only have to check the types if there are heterogenous equalities.
+      -- **Note**: We only have to check the types if there are heterogeneous equalities.
       if (← pure !hasHEq <||> hasSameType lhsRoot.self rhsRoot.self) then
         valueInconsistency := true
   if    (lhsRoot.interpreted && !rhsRoot.interpreted)

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

@@ -1973,7 +1973,7 @@ def SolverExtension.markTerm (ext : SolverExtension σ) (e : Expr) : GoalM Unit
     | .next id' e' sTerms' =>
       if id == id' then
         -- Skip if `e` and `e'` have different types (e.g., they were merged via `HEq` from `cast`).
-        -- This can happen when we have heterogenous equalities in an equivalence class containing types such as `Fin n` and `Fin m`
+        -- This can happen when we have heterogeneous equalities in an equivalence class containing types such as `Fin n` and `Fin m`
         if (← pure !root.heqProofs <||> hasSameType e e') then
           (← solverExtensionsRef.get)[id]!.newEq e e'
         return sTerms
@@ -2056,7 +2056,7 @@ where
     | .nil => return ()
     | .eq solverId lhs rhs rest =>
       -- Skip if `lhs` and `rhs` have different types (e.g., they were merged via `HEq` from `cast`).
-      -- This can happen when we have heterogenous equalities in an equivalence class containing types such as `Fin n` and `Fin m`
+      -- This can happen when we have heterogeneous equalities in an equivalence class containing types such as `Fin n` and `Fin m`
       let root ← getRootENode lhs
       if (← pure !root.heqProofs <||> hasSameType lhs rhs) then
         (← solverExtensionsRef.get)[solverId]!.newEq lhs rhs

src/Lean/Server/FileWorker/WidgetRequests.lean

@@ -192,7 +192,7 @@ private def matchEndPos (query : String) (startPos : String.Pos.Raw) : String.Po
   startPos + query
 
 @[specialize]
-private def hightlightStringMatches? (query text : String) (matchPositions : Array String.Pos.Raw)
+private def highlightStringMatches? (query text : String) (matchPositions : Array String.Pos.Raw)
     (highlight : α) (offset : String.Pos.Raw := ⟨0⟩) (mapIdx : Nat → Nat := id) :
     Option (TaggedText α) := Id.run do
   if query.isEmpty || text.isEmpty || matchPositions.isEmpty then
@@ -245,7 +245,7 @@ private def advanceTaggedTextHighlightState (text : String) (highlighted : α) :
   let query := (← get).query
   let p := (← get).p
   let ms := (← get).ms
-  let highlighted? := hightlightStringMatches? query text ms highlighted (offset := p)
+  let highlighted? := highlightStringMatches? query text ms highlighted (offset := p)
     (mapIdx := fun i => ms.size - i - 1)
   updateState text highlighted?.isSome
   return highlighted?.getD (.text text)

src/Std/Tactic/BVDecide/Syntax.lean

@@ -53,7 +53,7 @@ structure BVDecideConfig where
   /--
   Split hypotheses of the form `h : (x && y) = true` into `h1 : x = true` and `h2 : y = true`.
   This has synergy potential with embedded constraint substitution. Because embedded constraint
-  subsitution is the only use case for this feature it is automatically disabled whenever embedded
+  substitution is the only use case for this feature it is automatically disabled whenever embedded
   constraint substitution is disabled.
   -/
   andFlattening : Bool := true

src/kernel/declaration.h

@@ -226,7 +226,7 @@ public:
     bool is_unsafe() const;
     /** \brief Only definitions have values for the purpose of reduction and
         type checking. Theorems used to be like that; now they are treated like
-        opaque declations. */
+        opaque declarations. */
     bool has_value() const { return is_definition(); }
 
     axiom_val const & to_axiom_val() const { lean_assert(is_axiom()); return static_cast<axiom_val const &>(cnstr_get_ref(raw(), 0)); }

src/lake/Lake/Build/Common.lean

@@ -271,7 +271,7 @@ Returns `true` if the saved trace exists and its hash matches `inputHash`.
 
 If up-to-date, replays the saved log from the trace and sets the current
 build action to `replay`. Otherwise, if the log is empty and trace is synthetic,
-or if the trace is not up-to-date, the build action will be set ot `fetch`.
+or if the trace is not up-to-date, the build action will be set to `fetch`.
 -/
 public def SavedTrace.replayOrFetchIfUpToDate (inputHash : Hash) (self : SavedTrace) : JobM Bool := do
   if let .ok data := self then

src/lake/Lake/Build/Trace.lean

@@ -151,7 +151,7 @@ public def ofDecimal? (s : String) : Option Hash :=
 @[inline] public def ofString? (s : String) : Option Hash :=
   ofHex? s
 
-/-- Laod a hash from a `.hash` file. -/
+/-- Load a hash from a `.hash` file. -/
 public def load? (hashFile : FilePath) : BaseIO (Option Hash) :=
   ofString? <$> IO.FS.readFile hashFile |>.catchExceptions fun _ => pure none
 

src/lake/Lake/CLI/Help.lean

@@ -356,9 +356,9 @@ USAGE:
 
 COMMANDS:
   get [<mappings>]      download build outputs into the local Lake cache
-  put <mappings>        upload build ouptuts to a remote cache
+  put <mappings>        upload build outputs to a remote cache
   add <mappings>        add input-to-output mappings to the Lake cache
-  clean                 removes ALL froms the local Lake cache
+  clean                 removes ALL from the local Lake cache
   services              print configured remote cache services
 
 STAGING COMMANDS:
@@ -415,7 +415,7 @@ will search the repository's entire history (or as far as Git will allow).
 
 By default, Lake will download both the input-to-output mappings and the
 output artifacts for a package. By using `--mappings-onlys`, Lake will only
-download the mappings abd delay downloading artifacts until they are needed.
+download the mappings and delay downloading artifacts until they are needed.
 
 If a download for an artifact fails or the download process for a whole
 package fails, Lake will report this and continue on to the next. Once done,
@@ -469,7 +469,7 @@ OPTIONS:
   --scope=<remote-scope>          the prefix of artifacts within the service
   --repo=<github-repo>            for Reservoir, a GitHub repository scope
 
-Reads a list of input-to-output mapppings from the provided file and adds
+Reads a list of input-to-output mappings from the provided file and adds
 them to the local Lake cache. If `--service` is provided, the output artifacts
 can then be fetched lazily from that service during a Lake build. The service
 must either be `reservoir` or  be configured through the Lake system

src/lake/Lake/Config/Env.lean

@@ -58,7 +58,7 @@ public structure Env where
   If `none`, no suitable system directory for the cache exists.
   -/
   lakeSystemCache? : Option Cache := none
-  /-- The path to the sytem Lake configuration (i.e., `LAKE_CONFIG`). -/
+  /-- The path to the system Lake configuration (i.e., `LAKE_CONFIG`). -/
   lakeConfig? : Option FilePath
   /-- The authentication key for cache uploads (i.e., `LAKE_CACHE_KEY`). -/
   cacheKey? : Option String

src/lake/Lake/Load/Resolve.lean

@@ -220,7 +220,7 @@ private structure ToolchainCandidate where
   fixed : Bool := false
 
 private structure ToolchainState where
-  /-- The name of depedency which provided the current candidate toolchain. -/
+  /-- The name of dependency which provided the current candidate toolchain. -/
   src : Name
   /-- The current candidate toolchain version (if any). -/
   tc? : Option ToolchainVer

tests/README.md

@@ -203,7 +203,7 @@ Inside a test directory, they receive no arguments.
 
 A test succeeds iff the `run_test.sh` script exits with exit code 0.
 A benchmark additionally must produce a measurements file:
-Inside a test pile, `run_bench.sh` is expected to produce a `<testfile>.measurments.jsonl` file.
+Inside a test pile, `run_bench.sh` is expected to produce a `<testfile>.measurements.jsonl` file.
 Inside a test directory, `run_bench.sh` is expected to produce a `measurements.jsonl` file.
 
 ## The `elab*` test pile

tests/bench/mvcgen/sym/lib/VCGen.lean

@@ -219,7 +219,7 @@ lemma for the backward rule.
 
 It is unnecessary to use the `bind` rule in full generality. It is much more efficient to specialize
 it for the particular monad, postshape and `WP` instance. In doing so we can also unfold many
-`Std.Do` abbrevations, such as `Assertion ps` and `PostCond α ps`.
+`Std.Do` abbreviations, such as `Assertion ps` and `PostCond α ps`.
 We do that by doing `unfoldReducible` on the forall telescope. The type for `StateM Nat` and one
 excess state arg `s` becomes
 ```

tests/compile_bench/iterators.lean

@@ -10,7 +10,7 @@ The benchmark is run in three settings.
 * The time taken to interpret the script, including running `main`, is measured in
   `iterators (interpreted)`.
 * The time taken to interpret the script, without running `main`, is measured in
-  `interators (elab)`.
+  `iterators (elab)`.
 -/
 
 /- definitions -/

tests/elab/10984.lean

@@ -66,7 +66,7 @@ Example of `@` from Floris van Doorn at https://github.com/leanprover/lean4/issu
 example {α : Type} (f : ∀ {α}, List α → List α) : f (@.nil α) = .nil := sorry
 
 /-!
-Example of `@` plus universe levels adapated from https://github.com/leanprover/lean4/issues/10984
+Example of `@` plus universe levels adapted from https://github.com/leanprover/lean4/issues/10984
 -/
 example {α : Type u} (f : ∀ {α}, List α → List α) : f (@.nil.{u} α) = .nil := sorry
 

tests/elab/casesOnSameCtor.lean

@@ -109,7 +109,7 @@ info: theorem Vec.decEqVec.eq_def.{u_1} : ∀ {α : Type u_1} {a : Nat} [inst :
 #print sig decEqVec.eq_def
 
 
--- Incidentially, normal match syntax is able to produce an equivalent matcher
+-- Incidentally, normal match syntax is able to produce an equivalent matcher
 -- (with different implementation):
 -- (see #10195 for problems with equation generation)
 

tests/elab/cbv_classical.lean

@@ -4,7 +4,7 @@ when re-synthesizing instances.
 
 When `cbv` encounters `decide P`, it simplifies the proposition `P`. If `P`
 unfolds (e.g. `IsEven 2` → `∃ k, 2 * k = 2`), `simpDecideCbv` tries to
-synthetize `Decidable` instance for the *unfolded* form. With `open Classical`,
+synthesize `Decidable` instance for the *unfolded* form. With `open Classical`,
 this was picking up `Classical.propDecidable` (which uses `choice`), replacing
 the original computable instance with one that cannot be evaluated.
 

tests/elab/grind_11124.lean

@@ -136,9 +136,9 @@ h_10 : ¬(w_2 ∈ s₁.entries.kunion s₂.entries → decide (w_1.fst = w_2.fst
 w_3 : Sigma β
 h_12 : ¬(w_3 ∈ s₁.entries.kunion s₂.entries → decide (w_2.fst = w_3.fst) = false)
 h_13 : (fun s => decide (w_1.fst = s.fst)) = fun s => decide (x = s.fst)
-left_4 : ⟨x, cast ⋯ w_1.snd⟩ ∈ ⟨x, w⟩ :: s₂.entries.kunion s₁.entries
-right_4 : ⟨x, cast ⋯ w_1.snd⟩ = ⟨x, w⟩ ∨ ⟨x, cast ⋯ w_1.snd⟩ ∈ s₂.entries.kunion s₁.entries
-h_15 : (fun s => decide (w_2.fst = s.fst)) = fun s => decide (x = s.fst)
+h_14 : (fun s => decide (w_2.fst = s.fst)) = fun s => decide (x = s.fst)
+left_4 : ⟨x, w⟩ ∈ w_1 :: s₂.entries.kunion s₁.entries
+right_4 : ⟨x, w⟩ = w_1 ∨ ⟨x, w⟩ ∈ s₂.entries.kunion s₁.entries
 ⊢ False
 -/
 #guard_msgs in

tests/elab/grind_9856.lean

@@ -1,7 +1,7 @@
 module
 inductive T (a:Type) where
-  | constuctor1: T a
-  | constuctor2: T a
+  | constructor1: T a
+  | constructor2: T a
 
 instance : LE (T a) where
   le := sorry

tests/elab/grind_lia_regression.lean

@@ -0,0 +1,5 @@
+-- MWE for lia regression generated by the new canonicalizer
+
+example (n : Nat) (i : Fin (n + 1 + 1)) (h : n + 1 + 1 ≤ ↑i + ↑i + 1) :
+    ↑i + ↑i + 1 - (n + 1 + 1) < n + 1 + 1 := by
+  lia

tests/elab/issue11665.lean

@@ -10,4 +10,4 @@ def test1 : (n : Nat) → T n → Unit
    | _, _ => ()
 
 def eqns := @test1.match_1.eq_1 -- used to fail
-def congreqns := @test1.match_1.congr_eq_1 -- used to faile
+def congreqns := @test1.match_1.congr_eq_1 -- used to fail

tests/elab/lcnf_export_borrow_error.lean

@@ -4,8 +4,8 @@ module
 
 /--
 error:  Declaration bar is marked as `export` but some of its parameters have borrow annotations.
- Consider using `set_option compiler.ignoreBorrowAnnotation true in` to supress the borrow annotations in its type.
- If the declaration is part of an `export`/`extern` pair make sure to also supress the annotations at the `extern` declaration.
+ Consider using `set_option compiler.ignoreBorrowAnnotation true in` to suppress the borrow annotations in its type.
+ If the declaration is part of an `export`/`extern` pair make sure to also suppress the annotations at the `extern` declaration.
 -/
 #guard_msgs in
 @[export foo]

tests/elab/match1.lean

@@ -158,7 +158,7 @@ partial def natToBin' : (n : Nat) → List Bool
 
 -- This used to be bad until we used sparse matchers,
 -- which meant that the `0` pattern does not cause the remaining
--- to have `n = .succ _`, whic breaks dependent pattern matching
+-- to have `n = .succ _`, which breaks dependent pattern matching
 partial def natToBinBad (n : Nat) : List Bool :=
 match n, parity n with
 | 0, _             => []

tests/elab/newdo.lean

@@ -486,7 +486,7 @@ example (cache : Std.HashMap (Nat × Nat) Bool) : Bool := Id.run do
 
 -- Extracted from MathlibTest.random.lean. The problem here is that the `match` elaborator used to
 -- destructure the `(x, y)` pattern into `x` and `y` caused defaulting of `count` to `Nat`.
--- Nowadays, the `match` elaborator does not trigger global defaulting (in constrast to the term
+-- Nowadays, the `match` elaborator does not trigger global defaulting (in contrast to the term
 -- `match` elaborator), fixing this test case.
 example : IO Bool := do
   let mut count := 0

tests/elab/simple_ground_extraction.lean

@@ -1,4 +1,4 @@
-/-! This test asserts that the compiler is able to succesfully extract certain terms as statically
+/-! This test asserts that the compiler is able to successfully extract certain terms as statically
   initializable values. -/
 
 

tests/elab/sparseCasesOn.lean

@@ -32,7 +32,7 @@ run_meta
     Lean.logInfo m!"{name}"
 
 
-/- Check that the compiler is producin good code -/
+/- Check that the compiler is producing good code -/
 
 set_option trace.Compiler.saveBase true
 

tests/elab_bench/cbv_aes.lean

@@ -316,7 +316,7 @@ def AES256KBR : KBR :=
 def KeySchedule : Type := List (BitVec WordSize)
 
 -- Declare KeySchedule to be an instance HAppend
--- so we can apply `++` to KeySchedules propertly
+-- so we can apply `++` to KeySchedules properly
 instance : HAppend KeySchedule KeySchedule KeySchedule where
   hAppend := List.append
 

tests/elab_fail/10488.lean

@@ -41,7 +41,7 @@ def foo {A B} (_: A) (_: B) : Unit := ()
 #check (11.12succ)
 
 
--- This example (adapted from structInst4.lean) exercises the difference betwee
+-- This example (adapted from structInst4.lean) exercises the difference between
 -- term parsing and LVal parsing; the latter fails if we allow `2.snd` to parse
 -- as a scientificLit followed by an error token, so this test captures
 -- that we have to throw the error token right away, positioned before, rather

tests/lake/tests/module/test.sh

@@ -20,7 +20,7 @@ public def foo : String := "bar"
 EOF
 
 # Test cross-package `import all`
-# previosuly prevented by default
+# previously prevented by default
 # test_err 'cannot `import all` the module' build ErrorTest.CrossPackageImportAll
 # currently allowed
 test_run build ErrorTest.CrossPackageImportAll