chore: typos (#4026)

src/Init/Notation.lean

@@ -296,7 +296,7 @@ macro_rules | `($x - $y)   => `(binop% HSub.hSub $x $y)
 macro_rules | `($x * $y)   => `(binop% HMul.hMul $x $y)
 macro_rules | `($x / $y)   => `(binop% HDiv.hDiv $x $y)
 macro_rules | `($x % $y)   => `(binop% HMod.hMod $x $y)
--- exponentiation should be considered a right action (#2220)
+-- exponentiation should be considered a right action (#2854)
 macro_rules | `($x ^ $y)   => `(rightact% HPow.hPow $x $y)
 macro_rules | `($x ++ $y)  => `(binop% HAppend.hAppend $x $y)
 macro_rules | `(- $x)      => `(unop% Neg.neg $x)

src/Lean/Elab/Extra.lean

@@ -96,7 +96,7 @@ Here are brief descriptions of each of the operator types:
 - `rightact% f a b` elaborates `f a b` as a right action (the `b` operand "acts upon" the `a` operand).
   Only `a` participates in the protocol since `b` can have an unrelated type.
   This is used by `HPow` since, for example, there are both `Real -> Nat -> Real` and `Real -> Real -> Real`
-  exponentiation functions, and we prefer the former in the case of `x ^ 2`, but `binop%` would choose the latter. (#2220)
+  exponentiation functions, and we prefer the former in the case of `x ^ 2`, but `binop%` would choose the latter. (#2854)
 - There are also `binrel%` and `binrel_no_prop%` (see the docstring for `elabBinRelCore`).
 
 The elaborator works as follows:
@@ -449,7 +449,7 @@ def elabOp : TermElab := fun stx expectedType? => do
 
   - `binrel% R x y` elaborates `R x y` using the `binop%/...` expression trees in both `x` and `y`.
     It is similar to how `binop% R x y` elaborates but with a significant difference:
-    it does not use the expected type when computing the types of the operads.
+    it does not use the expected type when computing the types of the operands.
   - `binrel_no_prop% R x y` elaborates `R x y` like `binrel% R x y`, but if the resulting type for `x` and `y`
     is `Prop` they are coerced to `Bool`.
     This is used for relations such as `==` which do not support `Prop`, but we still want

src/Lean/Meta/Basic.lean

@@ -517,15 +517,15 @@ def appendOptMessageData (m : MessageData) (header : String) (m? : Option Messag
 
 def reportDiag : MetaM Unit := do
   if (← isDiagnosticsEnabled) then
-    let threshould := diag.threshold.get (← getOptions)
-    let unfold? := mkMessageBodyFor? (← get).diag.unfoldCounter threshould
-    let heu?    := mkMessageBodyFor? (← get).diag.heuristicCounter threshould
-    let inst?   := mkMessageBodyFor? (← get).diag.instanceCounter threshould
+    let threshold := diag.threshold.get (← getOptions)
+    let unfold? := mkMessageBodyFor? (← get).diag.unfoldCounter threshold
+    let heu?    := mkMessageBodyFor? (← get).diag.heuristicCounter threshold
+    let inst?   := mkMessageBodyFor? (← get).diag.instanceCounter threshold
     if unfold?.isSome || heu?.isSome || inst?.isSome then
       let m := appendOptMessageData MessageData.nil "unfolded declarations:" unfold?
       let m := appendOptMessageData m "used instances:" inst?
       let m := appendOptMessageData m "`isDefEq` heuristic:" heu?
-      let m := m ++ "\nuse `set_option diag.threshould <num>` to control threshold for reporting counters"
+      let m := m ++ "\nuse `set_option diag.threshold <num>` to control threshold for reporting counters"
       logInfo m
 
 def getLocalInstances : MetaM LocalInstances :=

src/Lean/Meta/ExprDefEq.lean

@@ -2013,7 +2013,7 @@ partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecD
     we only want to unify negation (and not all other field operations as well).
     Unifying the field instances slowed down unification: https://github.com/leanprover/lean4/issues/1986
 
-    Note that ew use `proj := .yesWithDeltaI` to ensure `whnfAtMostI` is used to reduce the projection structure.
+    Note that we use `proj := .yesWithDeltaI` to ensure `whnfAtMostI` is used to reduce the projection structure.
     We added this refinement to address a performance issue in code such as
     ```
     let val : Test := bar c1 key

src/Lean/Meta/WHNF.lean

@@ -344,7 +344,7 @@ inductive ProjReductionKind where
   | yesWithDelta
   /--
   Projections `s.i` are reduced at `whnfCore`, and `whnfAtMostI` is used at `s` during the process.
-  Recall that `whnfAtMostII` is like `whnf` but uses transparency at most `instances`.
+  Recall that `whnfAtMostI` is like `whnf` but uses transparency at most `instances`.
   This option is stronger than `yes`, but weaker than `yesWithDelta`.
   We use this option to ensure we reduce projections to prevent expensive defeq checks when unifying TC operations.
   When unifying e.g. `(@Field.toNeg α inst1).1 =?= (@Field.toNeg α inst2).1`,

tests/lean/hpow.lean

@@ -1,7 +1,7 @@
 import Lean.Data.Rat
 
 /-!
-Test the `rightact%` elaborator for `HPow.hPow`, added to address #2220
+Test the `rightact%` elaborator for `HPow.hPow`, added to address #2854
 -/
 
 open Lean

tests/lean/run/diagRec.lean

@@ -14,7 +14,7 @@ info: unfolded declarations:
   Or.rec ↦ 144
   PProd.fst ↦ 126
   Acc.rec ↦ 108
-use `set_option diag.threshould <num>` to control threshold for reporting counters
+use `set_option diag.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
 set_option diag true in