chore: reordering in Array.Basic

.github/ISSUE_TEMPLATE/bug_report.md

@@ -25,7 +25,7 @@ Please put an X between the brackets as you perform the following steps:
 
 ### Context
 
-[Broader context that the issue occurred in. If there was any prior discussion on [the Lean Zulip](https://leanprover.zulipchat.com), link it here as well.]
+[Broader context that the issue occured in. If there was any prior discussion on [the Lean Zulip](https://leanprover.zulipchat.com), link it here as well.]
 
 ### Steps to Reproduce
 

.github/workflows/ci.yml

@@ -316,7 +316,7 @@ jobs:
           git fetch --depth=1 origin ${{ github.sha }}
           git checkout FETCH_HEAD flake.nix flake.lock
         if: github.event_name == 'pull_request'
-      # (needs to be after "Checkout" so files don't get overridden)
+      # (needs to be after "Checkout" so files don't get overriden)
       - name: Setup emsdk
         uses: mymindstorm/setup-emsdk@v12
         with:

.github/workflows/pr-release.yml

@@ -134,7 +134,7 @@ jobs:
               MESSAGE=""
 
               if [[ -n "$MATHLIB_REMOTE_TAGS" ]]; then
-                echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
+                echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."    
               else
                 echo "... but Mathlib does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
                 MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Mathlib CI should run now."
@@ -149,7 +149,7 @@ jobs:
             echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA"
             git -C lean4.git log -10 origin/master
 
-            git -C lean4.git fetch origin nightly-with-mathlib
+            git -C lean4.git fetch origin nightly-with-mathlib 
             NIGHTLY_WITH_MATHLIB_SHA="$(git -C lean4.git rev-parse "origin/nightly-with-mathlib")"
             MESSAGE="- ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_WITH_MATHLIB_SHA\`."
           fi
@@ -329,17 +329,16 @@ jobs:
             git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE"
             echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}" > lean-toolchain
             git add lean-toolchain
-            sed -i 's,require "leanprover-community" / "batteries" @ git ".\+",require "leanprover-community" / "batteries" @ git "lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}",' lakefile.lean
+            sed -i 's,require "leanprover-community" / "batteries" @ git ".\+",require "leanprover-community" / "batteries" @ git "nightly-testing-'"${MOST_RECENT_NIGHTLY}"'",' lakefile.lean
             lake update batteries
             git add lakefile.lean lake-manifest.json
             git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
           else
-            echo "Branch already exists, merging $BASE and bumping Batteries."
+            echo "Branch already exists, pushing an empty commit."
             git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
             # The Mathlib `nightly-testing` branch or `nightly-testing-YYYY-MM-DD` tag may have moved since this branch was created, so merge their changes.
             # (This should no longer be possible once `nightly-testing-YYYY-MM-DD` is a tag, but it is still safe to merge.)
             git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories
-            lake update batteries
             git commit --allow-empty -m "Trigger CI for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
           fi
 

RELEASES.md

@@ -381,7 +381,7 @@ v4.10.0
 
 * **Commands**
   * [#4370](https://github.com/leanprover/lean4/pull/4370) makes the `variable` command fully elaborate binders during validation, fixing an issue where some errors would be reported only at the next declaration.
-  * [#4408](https://github.com/leanprover/lean4/pull/4408) fixes a discrepancy in universe parameter order between `theorem` and `def` declarations.
+  * [#4408](https://github.com/leanprover/lean4/pull/4408) fixes a discrepency in universe parameter order between `theorem` and `def` declarations.
   * [#4493](https://github.com/leanprover/lean4/pull/4493) and
     [#4482](https://github.com/leanprover/lean4/pull/4482) fix a discrepancy in the elaborators for `theorem`, `def`, and `example`,
     making `Prop`-valued `example`s and other definition commands elaborate like `theorem`s.
@@ -443,7 +443,7 @@ v4.10.0
   * [#4454](https://github.com/leanprover/lean4/pull/4454) adds public `Name.isInternalDetail` function for filtering declarations using naming conventions for internal names.
 
 * **Other fixes or improvements**
-  * [#4416](https://github.com/leanprover/lean4/pull/4416) sorts the output of `#print axioms` for determinism.
+  * [#4416](https://github.com/leanprover/lean4/pull/4416) sorts the ouput of `#print axioms` for determinism.
   * [#4528](https://github.com/leanprover/lean4/pull/4528) fixes error message range for the cdot focusing tactic.
 
 ### Language server, widgets, and IDE extensions
@@ -479,7 +479,7 @@ v4.10.0
   * [#4372](https://github.com/leanprover/lean4/pull/4372) fixes linearity in `HashMap.insert` and `HashMap.erase`, leading to a 40% speedup in a replace-heavy workload.
 * `Option`
   * [#4403](https://github.com/leanprover/lean4/pull/4403) generalizes type of `Option.forM` from `Unit` to `PUnit`.
-  * [#4504](https://github.com/leanprover/lean4/pull/4504) remove simp attribute from `Option.elim` and instead adds it to individual reduction lemmas, making unfolding less aggressive.
+  * [#4504](https://github.com/leanprover/lean4/pull/4504) remove simp attribute from `Option.elim` and instead adds it to individal reduction lemmas, making unfolding less aggressive.
 * `Nat`
   * [#4242](https://github.com/leanprover/lean4/pull/4242) adds missing theorems for `n + 1` and `n - 1` normal forms.
   * [#4486](https://github.com/leanprover/lean4/pull/4486) makes `Nat.min_assoc` be a simp lemma.
@@ -940,7 +940,7 @@ While most changes could be considered to be a breaking change, this section mak
   In particular, tactics embedded in the type will no longer make use of the type of `value` in expressions such as `let x : type := value; body`.
 * Now functions defined by well-founded recursion are marked with `@[irreducible]` by default ([#4061](https://github.com/leanprover/lean4/pull/4061)).
   Existing proofs that hold by definitional equality (e.g. `rfl`) can be
-  rewritten to explicitly unfold the function definition (using `simp`,
+  rewritten to explictly unfold the function definition (using `simp`,
   `unfold`, `rw`), or the recursive function can be temporarily made
   semireducible (using `unseal f in` before the command), or the function
   definition itself can be marked as `@[semireducible]` to get the previous
@@ -1559,7 +1559,7 @@ v4.7.0
      and `BitVec` as we begin making the APIs and simp normal forms for these types
      more complete and consistent.
   4. Laying the groundwork for the Std roadmap, as a library focused on
-     essential datatypes not provided by the core language (e.g. `RBMap`)
+     essential datatypes not provided by the core langauge (e.g. `RBMap`)
      and utilities such as basic IO.
   While we have achieved most of our initial aims in `v4.7.0-rc1`,
   some upstreaming will continue over the coming months.
@@ -1570,7 +1570,7 @@ v4.7.0
   There is now kernel support for these functions.
   [#3376](https://github.com/leanprover/lean4/pull/3376).
 
-* `omega`, our integer linear arithmetic tactic, is now available in the core language.
+* `omega`, our integer linear arithmetic tactic, is now availabe in the core langauge.
   * It is supplemented by a preprocessing tactic `bv_omega` which can solve goals about `BitVec`
     which naturally translate into linear arithmetic problems.
     [#3435](https://github.com/leanprover/lean4/pull/3435).
@@ -1663,11 +1663,11 @@ v4.6.0
       /-
       The `Step` type has three constructors: `.done`, `.visit`, `.continue`.
       * The constructor `.done` instructs `simp` that the result does
-        not need to be simplified further.
+        not need to be simplied further.
       * The constructor `.visit` instructs `simp` to visit the resulting expression.
       * The constructor `.continue` instructs `simp` to try other simplification procedures.
 
-      All three constructors take a `Result`. The `.continue` constructor may also take `none`.
+      All three constructors take a `Result`. The `.continue` contructor may also take `none`.
       `Result` has two fields `expr` (the new expression), and `proof?` (an optional proof).
        If the new expression is definitionally equal to the input one, then `proof?` can be omitted or set to `none`.
       -/
@@ -1879,7 +1879,7 @@ v4.5.0
 ---------
 
 * Modify the lexical syntax of string literals to have string gaps, which are escape sequences of the form `"\" newline whitespace*`.
-  These have the interpretation of an empty string and allow a string to flow across multiple lines without introducing additional whitespace.
+  These have the interpetation of an empty string and allow a string to flow across multiple lines without introducing additional whitespace.
   The following is equivalent to `"this is a string"`.
   ```lean
   "this is \
@@ -1902,7 +1902,7 @@ v4.5.0
 
   If the well-founded relation you want to use is not the one that the
   `WellFoundedRelation` type class would infer for your termination argument,
-  you can use `WellFounded.wrap` from the std library to explicitly give one:
+  you can use `WellFounded.wrap` from the std libarary to explicitly give one:
   ```diff
   -termination_by' ⟨r, hwf⟩
   +termination_by x => hwf.wrap x

doc/dev/release_checklist.md

@@ -71,12 +71,6 @@ We'll use `v4.6.0` as the intended release version as a running example.
       - Toolchain bump PR including updated Lake manifest
       - Create and push the tag
       - There is no `stable` branch; skip this step
-    - [Verso](https://github.com/leanprover/verso)
-      - Dependencies: exist, but they're not part of the release workflow
-      - The `SubVerso` dependency should be compatible with _every_ Lean release simultaneously, rather than following this workflow
-      - Toolchain bump PR including updated Lake manifest
-      - Create and push the tag
-      - There is no `stable` branch; skip this step
     - [import-graph](https://github.com/leanprover-community/import-graph)
       - Toolchain bump PR including updated Lake manifest
       - Create and push the tag

doc/examples/ICERM2022/ctor.lean

@@ -18,7 +18,7 @@ def ctor (mvarId : MVarId) (idx : Nat) : MetaM (List MVarId) := do
     else if h : idx - 1 < ctors.length then
       mvarId.apply (.const ctors[idx - 1] us)
     else
-      throwTacticEx `ctor mvarId "invalid index, inductive datatype has only {ctors.length} constructors"
+      throwTacticEx `ctor mvarId "invalid index, inductive datatype has only {ctors.length} contructors"
 
 open Elab Tactic
 

doc/examples/deBruijn.lean

@@ -149,7 +149,7 @@ We now define the constant folding optimization that traverses a term if replace
 /-!
 The correctness of the `Term.constFold` is proved using induction, case-analysis, and the term simplifier.
 We prove all cases but the one for `plus` using `simp [*]`. This tactic instructs the term simplifier to
-use hypotheses such as `a = b` as rewriting/simplifications rules.
+use hypotheses such as `a = b` as rewriting/simplications rules.
 We use the `split` to break the nested `match` expression in the `plus` case into two cases.
 The local variables `iha` and `ihb` are the induction hypotheses for `a` and `b`.
 The modifier `←` in a term simplifier argument instructs the term simplifier to use the equation as a rewriting rule in

doc/examples/phoas.lean

@@ -225,7 +225,7 @@ We now define the constant folding optimization that traverses a term if replace
 /-!
 The correctness of the `constFold` is proved using induction, case-analysis, and the term simplifier.
 We prove all cases but the one for `plus` using `simp [*]`. This tactic instructs the term simplifier to
-use hypotheses such as `a = b` as rewriting/simplifications rules.
+use hypotheses such as `a = b` as rewriting/simplications rules.
 We use the `split` to break the nested `match` expression in the `plus` case into two cases.
 The local variables `iha` and `ihb` are the induction hypotheses for `a` and `b`.
 The modifier `←` in a term simplifier argument instructs the term simplifier to use the equation as a rewriting rule in

doc/examples/widgets.lean

@@ -93,7 +93,7 @@ Meaning "Remote Procedure Call",this is a Lean function callable from widget cod
 Our method will take in the `name : Name` of a constant in the environment and return its type.
 By convention, we represent the input data as a `structure`.
 Since it will be sent over from JavaScript,
-we need `FromJson` and `ToJson` instance.
+we need `FromJson` and `ToJson` instnace.
 We'll see why the position field is needed later.
 -/
 

script/lib/update-stage0

@@ -17,7 +17,7 @@ for f in $(git ls-files src ':!:src/lake/*' ':!:src/Leanc.lean'); do
 done
 
 # special handling for Lake files due to its nested directory
-# copy the README to ensure the `stage0/src/lake` directory is committed
+# copy the README to ensure the `stage0/src/lake` directory is comitted
 for f in $(git ls-files 'src/lake/Lake/*' src/lake/Lake.lean src/lake/LakeMain.lean src/lake/README.md ':!:src/lakefile.toml'); do
     if [[ $f == *.lean ]]; then
         f=${f#src/lake}

src/Init/Classical.lean

@@ -121,11 +121,11 @@ theorem propComplete (a : Prop) : a = True ∨ a = False :=
   | Or.inl ha => Or.inl (eq_true ha)
   | Or.inr hn => Or.inr (eq_false hn)
 
--- this supersedes byCases in Decidable
+-- this supercedes byCases in Decidable
 theorem byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
   Decidable.byCases (dec := propDecidable _) hpq hnpq
 
--- this supersedes byContradiction in Decidable
+-- this supercedes byContradiction in Decidable
 theorem byContradiction {p : Prop} (h : ¬p → False) : p :=
   Decidable.byContradiction (dec := propDecidable _) h
 

src/Init/Core.lean

@@ -1382,11 +1382,6 @@ gen_injective_theorems% EStateM.Result
 gen_injective_theorems% Lean.Name
 gen_injective_theorems% Lean.Syntax
 
-/-- Replacement for `Array.mk.injEq`; we avoid mentioning the constructor and prefer `List.toArray`. -/
-abbrev List.toArray_inj := @Array.mk.injEq
-
-attribute [deprecated List.toArray_inj (since := "2024-09-09")] Array.mk.injEq
-
 theorem Nat.succ.inj {m n : Nat} : m.succ = n.succ → m = n :=
   fun x => Nat.noConfusion x id
 
@@ -1897,8 +1892,7 @@ theorem funext {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}
   show extfunApp (Quot.mk eqv f) = extfunApp (Quot.mk eqv g)
   exact congrArg extfunApp (Quot.sound h)
 
-instance Pi.instSubsingleton {α : Sort u} {β : α → Sort v} [∀ a, Subsingleton (β a)] :
-    Subsingleton (∀ a, β a) where
+instance {α : Sort u} {β : α → Sort v} [∀ a, Subsingleton (β a)] : Subsingleton (∀ a, β a) where
   allEq f g := funext fun a => Subsingleton.elim (f a) (g a)
 
 /-! # Squash -/
@@ -2061,7 +2055,7 @@ class IdempotentOp (op : α → α → α) : Prop where
 `LeftIdentify op o` indicates `o` is a left identity of `op`.
 
 This class does not require a proof that `o` is an identity, and
-is used primarily for inferring the identity using class resolution.
+is used primarily for infering the identity using class resoluton.
 -/
 class LeftIdentity (op : α → β → β) (o : outParam α) : Prop
 
@@ -2077,7 +2071,7 @@ class LawfulLeftIdentity (op : α → β → β) (o : outParam α) extends LeftI
 `RightIdentify op o` indicates `o` is a right identity `o` of `op`.
 
 This class does not require a proof that `o` is an identity, and is used
-primarily for inferring the identity using class resolution.
+primarily for infering the identity using class resoluton.
 -/
 class RightIdentity (op : α → β → α) (o : outParam β) : Prop
 
@@ -2093,7 +2087,7 @@ class LawfulRightIdentity (op : α → β → α) (o : outParam β) extends Righ
 `Identity op o` indicates `o` is a left and right identity of `op`.
 
 This class does not require a proof that `o` is an identity, and is used
-primarily for inferring the identity using class resolution.
+primarily for infering the identity using class resoluton.
 -/
 class Identity (op : α → α → α) (o : outParam α) extends LeftIdentity op o, RightIdentity op o : Prop
 

src/Init/Data.lean

@@ -33,6 +33,7 @@ import Init.Data.Prod
 import Init.Data.AC
 import Init.Data.Queue
 import Init.Data.Channel
+import Init.Data.Cast
 import Init.Data.Sum
 import Init.Data.BEq
 import Init.Data.Subtype

src/Init/Data/Array/Basic.lean

@@ -162,16 +162,19 @@ instance : Inhabited (Array α) where
 @[simp] def isEmpty (a : Array α) : Bool :=
   a.size = 0
 
+-- TODO(Leo): cleanup
 @[specialize]
-def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) :
-    ∀ (i : Nat) (_ : i ≤ a.size), Bool
-  | 0, _ => true
-  | i+1, h =>
-    p a[i] (b[i]'(hsz ▸ h)) && isEqvAux a b hsz p i (Nat.le_trans (Nat.le_add_right i 1) h)
+def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) (i : Nat) : Bool :=
+  if h : i < a.size then
+     have : i < b.size := hsz ▸ h
+     p a[i] b[i] && isEqvAux a b hsz p (i+1)
+  else
+    true
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 @[inline] def isEqv (a b : Array α) (p : α → α → Bool) : Bool :=
   if h : a.size = b.size then
-    isEqvAux a b h p a.size (Nat.le_refl a.size)
+    isEqvAux a b h p 0
   else
     false
 
@@ -185,10 +188,9 @@ ofFn f = #[f 0, f 1, ... , f(n - 1)]
 ``` -/
 def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
   /-- Auxiliary for `ofFn`. `ofFn.go f i acc = acc ++ #[f i, ..., f(n - 1)]` -/
-  @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
   go (i : Nat) (acc : Array α) : Array α :=
     if h : i < n then go (i+1) (acc.push (f ⟨i, h⟩)) else acc
-  decreasing_by simp_wf; decreasing_trivial_pre_omega
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 /-- The array `#[0, 1, ..., n - 1]`. -/
 def range (n : Nat) : Array Nat :=
@@ -387,12 +389,11 @@ unsafe def mapMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad
 def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) : m (Array β) :=
   -- Note: we cannot use `foldlM` here for the reference implementation because this calls
   -- `bind` and `pure` too many times. (We are not assuming `m` is a `LawfulMonad`)
-  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-    map (i : Nat) (r : Array β) : m (Array β) := do
-      if hlt : i < as.size then
-        map (i+1) (r.push (← f as[i]))
-      else
-        pure r
+  let rec map (i : Nat) (r : Array β) : m (Array β) := do
+    if hlt : i < as.size then
+      map (i+1) (r.push (← f as[i]))
+    else
+      pure r
   decreasing_by simp_wf; decreasing_trivial_pre_omega
   map 0 (mkEmpty as.size)
 
@@ -456,8 +457,7 @@ unsafe def anyMUnsafe {α : Type u} {m : Type → Type w} [Monad m] (p : α →
 @[implemented_by anyMUnsafe]
 def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (start := 0) (stop := as.size) : m Bool :=
   let any (stop : Nat) (h : stop ≤ as.size) :=
-    let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-    loop (j : Nat) : m Bool := do
+    let rec loop (j : Nat) : m Bool := do
       if hlt : j < stop then
         have : j < as.size := Nat.lt_of_lt_of_le hlt h
         if (← p as[j]) then
@@ -547,8 +547,7 @@ def findRev? {α : Type} (as : Array α) (p : α → Bool) : Option α :=
 
 @[inline]
 def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
-  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-  loop (j : Nat) :=
+  let rec loop (j : Nat) :=
     if h : j < as.size then
       if p as[j] then some j else loop (j + 1)
     else none
@@ -558,7 +557,6 @@ def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
 def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
   a.findIdx? fun a => a == v
 
-@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size) :=
   if h : i < a.size then
     let idx : Fin a.size := ⟨i, h⟩;
@@ -680,7 +678,6 @@ where
     else
       as
 
-@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def popWhile (p : α → Bool) (as : Array α) : Array α :=
   if h : as.size > 0 then
     if p (as.get ⟨as.size - 1, Nat.sub_lt h (by decide)⟩) then
@@ -692,8 +689,7 @@ def popWhile (p : α → Bool) (as : Array α) : Array α :=
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def takeWhile (p : α → Bool) (as : Array α) : Array α :=
-  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-  go (i : Nat) (r : Array α) : Array α :=
+  let rec go (i : Nat) (r : Array α) : Array α :=
     if h : i < as.size then
       let a := as.get ⟨i, h⟩
       if p a then
@@ -709,7 +705,6 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
 
   This function takes worst case O(n) time because
   it has to backshift all elements at positions greater than `i`.-/
-@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
   if h : i.val + 1 < a.size then
     let a' := a.swap ⟨i.val + 1, h⟩ i
@@ -744,8 +739,7 @@ def erase [BEq α] (as : Array α) (a : α) : Array α :=
 
 /-- Insert element `a` at position `i`. -/
 @[inline] def insertAt (as : Array α) (i : Fin (as.size + 1)) (a : α) : Array α :=
-  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-  loop (as : Array α) (j : Fin as.size) :=
+  let rec loop (as : Array α) (j : Fin as.size) :=
     if i.1 < j then
       let j' := ⟨j-1, Nat.lt_of_le_of_lt (Nat.pred_le _) j.2⟩
       let as := as.swap j' j
@@ -763,7 +757,6 @@ def insertAt! (as : Array α) (i : Nat) (a : α) : Array α :=
     insertAt as ⟨i, Nat.lt_succ_of_le h⟩ a
   else panic! "invalid index"
 
-@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : Nat) : Bool :=
   if h : i < as.size then
     let a := as[i]
@@ -785,8 +778,7 @@ def isPrefixOf [BEq α] (as bs : Array α) : Bool :=
   else
     false
 
-@[semireducible, specialize] -- This is otherwise irreducible because it uses well-founded recursion.
-def zipWithAux (f : α → β → γ) (as : Array α) (bs : Array β) (i : Nat) (cs : Array γ) : Array γ :=
+@[specialize] def zipWithAux (f : α → β → γ) (as : Array α) (bs : Array β) (i : Nat) (cs : Array γ) : Array γ :=
   if h : i < as.size then
     let a := as[i]
     if h : i < bs.size then
@@ -822,7 +814,6 @@ private def allDiffAuxAux [BEq α] (as : Array α) (a : α) : forall (i : Nat),
     have : i < as.size := Nat.lt_trans (Nat.lt_succ_self _) h;
     a != as[i] && allDiffAuxAux as a i this
 
-@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 private def allDiffAux [BEq α] (as : Array α) (i : Nat) : Bool :=
   if h : i < as.size then
     allDiffAuxAux as as[i] i h && allDiffAux as (i+1)

src/Init/Data/Array/BasicAux.lean

@@ -9,7 +9,7 @@ import Init.Data.Nat.Linear
 import Init.NotationExtra
 
 theorem Array.of_push_eq_push {as bs : Array α} (h : as.push a = bs.push b) : as = bs ∧ a = b := by
-  simp only [push, List.toArray_inj] at h
+  simp only [push, mk.injEq] at h
   have ⟨h₁, h₂⟩ := List.of_concat_eq_concat h
   cases as; cases bs
   simp_all

src/Init/Data/Array/DecidableEq.lean

@@ -5,49 +5,43 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Array.Basic
-import Init.Data.BEq
 import Init.ByCases
 
 namespace Array
 
-theorem rel_of_isEqvAux
-    (r : α → α → Bool) (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size)
-    (heqv : Array.isEqvAux a b hsz r i hi)
-    (j : Nat) (hj : j < i) : r (a[j]'(Nat.lt_of_lt_of_le hj hi)) (b[j]'(Nat.lt_of_lt_of_le hj (hsz ▸ hi))) := by
-  induction i with
-  | zero => contradiction
-  | succ i ih =>
-    simp only [Array.isEqvAux, Bool.and_eq_true, decide_eq_true_eq] at heqv
-    by_cases hj' : j < i
-    next =>
-      exact ih _ heqv.right hj'
-    next =>
-      replace hj' : j = i := Nat.eq_of_le_of_lt_succ (Nat.not_lt.mp hj') hj
-      subst hj'
-      exact heqv.left
+theorem eq_of_isEqvAux [DecidableEq α] (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size) (heqv : Array.isEqvAux a b hsz (fun x y => x = y) i) (j : Nat) (low : i ≤ j) (high : j < a.size) : a[j] = b[j]'(hsz ▸ high) := by
+  by_cases h : i < a.size
+  · unfold Array.isEqvAux at heqv
+    simp [h] at heqv
+    have hind := eq_of_isEqvAux a b hsz (i+1) (Nat.succ_le_of_lt h) heqv.2
+    by_cases heq : i = j
+    · subst heq; exact heqv.1
+    · exact hind j (Nat.succ_le_of_lt (Nat.lt_of_le_of_ne low heq)) high
+  · have heq : i = a.size := Nat.le_antisymm hi (Nat.ge_of_not_lt h)
+    subst heq
+    exact absurd (Nat.lt_of_lt_of_le high low) (Nat.lt_irrefl j)
+termination_by a.size - i
+decreasing_by decreasing_trivial_pre_omega
 
-theorem rel_of_isEqv (r : α → α → Bool) (a b : Array α) :
-    Array.isEqv a b r → ∃ h : a.size = b.size, ∀ (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h ▸ h')) := by
-  simp only [isEqv]
-  split <;> rename_i h
-  · exact fun h' => ⟨h, rel_of_isEqvAux r a b h a.size (Nat.le_refl ..) h'⟩
-  · intro; contradiction
 
-theorem eq_of_isEqv [DecidableEq α] (a b : Array α) (h : Array.isEqv a b (fun x y => x = y)) : a = b := by
-  have ⟨h, h'⟩ := rel_of_isEqv (fun x y => x = y) a b h
-  exact ext _ _ h (fun i lt _ => by simpa using h' i lt)
+theorem eq_of_isEqv [DecidableEq α] (a b : Array α) : Array.isEqv a b (fun x y => x = y) → a = b := by
+  simp [Array.isEqv]
+  split
+  next hsz =>
+   intro h
+   have aux := eq_of_isEqvAux a b hsz 0 (Nat.zero_le ..) h
+   exact ext a b hsz fun i h _ => aux i (Nat.zero_le ..) _
+  next => intro; contradiction
 
-theorem isEqvAux_self (r : α → α → Bool) (hr : ∀ a, r a a) (a : Array α) (i : Nat) (h : i ≤ a.size) :
-    Array.isEqvAux a a rfl r i h = true := by
-  induction i with
-  | zero => simp [Array.isEqvAux]
-  | succ i ih =>
-    simp_all only [isEqvAux, Bool.and_self]
+theorem isEqvAux_self [DecidableEq α] (a : Array α) (i : Nat) : Array.isEqvAux a a rfl (fun x y => x = y) i = true := by
+  unfold Array.isEqvAux
+  split
+  next h => simp [h, isEqvAux_self a (i+1)]
+  next h => simp [h]
+termination_by a.size - i
+decreasing_by decreasing_trivial_pre_omega
 
-theorem isEqv_self_beq [BEq α] [ReflBEq α] (a : Array α) : Array.isEqv a a (· == ·) = true := by
-  simp [isEqv, isEqvAux_self]
-
-theorem isEqv_self [DecidableEq α] (a : Array α) : Array.isEqv a a (· = ·) = true := by
+theorem isEqv_self [DecidableEq α] (a : Array α) : Array.isEqv a a (fun x y => x = y) = true := by
   simp [isEqv, isEqvAux_self]
 
 instance [DecidableEq α] : DecidableEq (Array α) :=

src/Init/Data/Array/Lemmas.lean

@@ -19,14 +19,24 @@ This file contains some theorems about `Array` and `List` needed for `Init.Data.
 
 namespace Array
 
-/-- We avoid mentioning the constructor `Array.mk` directly, preferring `List.toArray`. -/
-@[simp] theorem mk_eq_toArray (as : List α) : Array.mk as = as.toArray := by
-  apply ext'
-  simp
+attribute [simp] uset
 
-@[simp] theorem getElem_toList {a : Array α} {i : Nat} (h : i < a.size) : a.toList[i] = a[i] := rfl
+@[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
 
-@[simp] theorem getElem_mk {xs : List α} {i : Nat} (h : i < xs.length) : (Array.mk xs)[i] = xs[i] := rfl
+@[simp] theorem toArray_toList : (a : Array α) → a.toList.toArray = a
+  | ⟨l⟩ => ext' (toList_toArray l)
+
+@[deprecated toArray_toList (since := "2024-09-09")]
+abbrev toArray_data := @toArray_toList
+
+@[simp] theorem toList_length {l : Array α} : l.toList.length = l.size := rfl
+
+@[deprecated toList_length (since := "2024-09-09")]
+abbrev data_length := @toList_length
+
+@[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl
+
+@[simp] theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size]
 
 theorem getElem_eq_toList_getElem (a : Array α) (h : i < a.size) : a[i] = a.toList[i] := by
   by_cases i < a.size <;> (try simp [*]) <;> rfl
@@ -36,7 +46,27 @@ abbrev getElem_eq_data_getElem := @getElem_eq_toList_getElem
 
 @[deprecated getElem_eq_toList_getElem (since := "2024-06-12")]
 theorem getElem_eq_toList_get (a : Array α) (h : i < a.size) : a[i] = a.toList.get ⟨i, h⟩ := by
-  simp
+  simp [getElem_eq_toList_getElem]
+
+theorem foldrM_push [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) :
+    (arr.push a).foldrM f init = f a init >>= arr.foldrM f := by
+  simp [foldrM_eq_reverse_foldlM_toList, -size_push]
+
+@[simp] theorem foldrM_push' [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) :
+    (arr.push a).foldrM f init (start := arr.size + 1) = f a init >>= arr.foldrM f := by
+  simp [← foldrM_push]
+
+theorem foldr_push (f : α → β → β) (init : β) (arr : Array α) (a : α) :
+    (arr.push a).foldr f init = arr.foldr f (f a init) := foldrM_push ..
+
+@[simp] theorem foldr_push' (f : α → β → β) (init : β) (arr : Array α) (a : α) :
+    (arr.push a).foldr f init (start := arr.size + 1) = arr.foldr f (f a init) := foldrM_push' ..
+
+/-- A more efficient version of `arr.toList.reverse`. -/
+@[inline] def toListRev (arr : Array α) : List α := arr.foldl (fun l t => t :: l) []
+
+@[simp] theorem toListRev_eq (arr : Array α) : arr.toListRev = arr.toList.reverse := by
+  rw [toListRev, foldl_eq_foldl_toList, ← List.foldr_reverse, List.foldr_cons_nil]
 
 theorem get_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
     have : i < (a.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]
@@ -54,78 +84,6 @@ theorem get_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) :
   · simp at h
     simp [get_push_lt, Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.ge_of_not_lt h')]
 
-end Array
-
-namespace List
-
-open Array
-
-/-! ### Lemmas about `List.toArray`. -/
-
-@[simp] theorem toArray_size (as : List α) : as.toArray.size = as.length := by simp [size]
-
-@[simp] theorem toArrayAux_size {a : List α} {b : Array α} :
-    (a.toArrayAux b).size = b.size + a.length := by
-  simp [size]
-
-@[simp] theorem toArray_toList : (a : Array α) → a.toList.toArray = a
-  | ⟨l⟩ => ext' (toList_toArray l)
-
-@[simp] theorem getElem_toArray {a : List α} {i : Nat} (h : i < a.toArray.size) :
-    a.toArray[i] = a[i]'(by simpa using h) := by
-  have h₁ := mk_eq_toArray a
-  have h₂ := getElem_mk (by simpa using h)
-  simpa [h₁] using h₂
-
-@[simp] theorem toArray_concat {as : List α} {x : α} :
-    (as ++ [x]).toArray = as.toArray.push x := by
-  apply ext'
-  simp
-
-end List
-
-namespace Array
-
-attribute [simp] uset
-
-@[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
-
-@[deprecated List.toArray_toList (since := "2024-09-09")]
-abbrev toArray_data := @List.toArray_toList
-@[deprecated List.toArray_toList (since := "2024-09-09")]
-abbrev toArray_toList := @List.toArray_toList
-
-@[simp] theorem toList_length {l : Array α} : l.toList.length = l.size := rfl
-
-@[deprecated toList_length (since := "2024-09-09")]
-abbrev data_length := @toList_length
-
-@[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl
-
-@[simp] theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size]
-
-theorem foldrM_push [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) :
-    (arr.push a).foldrM f init = f a init >>= arr.foldrM f := by
-  simp [foldrM_eq_reverse_foldlM_toList, -size_push]
-
-/-- Variant of `foldrM_push` with the `start := arr.size + 1` rather than `(arr.push a).size`. -/
-@[simp] theorem foldrM_push' [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) :
-    (arr.push a).foldrM f init (start := arr.size + 1) = f a init >>= arr.foldrM f := by
-  simp [← foldrM_push]
-
-theorem foldr_push (f : α → β → β) (init : β) (arr : Array α) (a : α) :
-    (arr.push a).foldr f init = arr.foldr f (f a init) := foldrM_push ..
-
-/-- Variant of `foldr_push` with the `start := arr.size + 1` rather than `(arr.push a).size`. -/
-@[simp] theorem foldr_push' (f : α → β → β) (init : β) (arr : Array α) (a : α) :
-    (arr.push a).foldr f init (start := arr.size + 1) = arr.foldr f (f a init) := foldrM_push' ..
-
-/-- A more efficient version of `arr.toList.reverse`. -/
-@[inline] def toListRev (arr : Array α) : List α := arr.foldl (fun l t => t :: l) []
-
-@[simp] theorem toListRev_eq (arr : Array α) : arr.toListRev = arr.toList.reverse := by
-  rw [toListRev, foldl_eq_foldl_toList, ← List.foldr_reverse, List.foldr_cons_nil]
-
 theorem mapM_eq_foldlM [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
     arr.mapM f = arr.foldlM (fun bs a => bs.push <$> f a) #[] := by
   rw [mapM, aux, foldlM_eq_foldlM_toList]; rfl
@@ -387,7 +345,7 @@ theorem getElem_mem_toList (a : Array α) (h : i < a.size) : a[i] ∈ a.toList :
 abbrev getElem_mem_data := @getElem_mem_toList
 
 theorem getElem?_eq_toList_get? (a : Array α) (i : Nat) : a[i]? = a.toList.get? i := by
-  by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg, List.get?_eq_get, eq_comm]
+  by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg, List.get?_eq_get, eq_comm]; rfl
 
 @[deprecated getElem?_eq_toList_get? (since := "2024-09-09")]
 abbrev getElem?_eq_data_get? := @getElem?_eq_toList_get?
@@ -647,12 +605,12 @@ theorem foldr_induction
   simp only [mem_def, map_toList, List.mem_map]
 
 theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
-    arr.mapM f = return (← arr.toList.mapM f).toArray := by
+    arr.mapM f = return mk (← arr.toList.mapM f) := by
   rw [mapM_eq_foldlM, foldlM_eq_foldlM_toList, ← List.foldrM_reverse]
   conv => rhs; rw [← List.reverse_reverse arr.toList]
   induction arr.toList.reverse with
-  | nil => simp
-  | cons a l ih => simp [ih]; simp [map_eq_pure_bind]
+  | nil => simp; rfl
+  | cons a l ih => simp [ih]; simp [map_eq_pure_bind, push]
 
 @[deprecated mapM_eq_mapM_toList (since := "2024-09-09")]
 abbrev mapM_eq_mapM_data := @mapM_eq_mapM_toList

src/Init/Data/Array/TakeDrop.lean

@@ -12,7 +12,6 @@ namespace Array
 theorem exists_of_uset (self : Array α) (i d h) :
     ∃ l₁ l₂, self.toList = l₁ ++ self[i] :: l₂ ∧ List.length l₁ = i.toNat ∧
       (self.uset i d h).toList = l₁ ++ d :: l₂ := by
-  simpa only [ugetElem_eq_getElem, getElem_eq_toList_getElem, uset, toList_set] using
-    List.exists_of_set _
+  simpa [Array.getElem_eq_toList_getElem] using List.exists_of_set _
 
 end Array

src/Init/Data/BitVec/Lemmas.lean

@@ -710,26 +710,6 @@ theorem or_comm (x y : BitVec w) :
   simp [Bool.or_comm]
 instance : Std.Commutative (fun (x y : BitVec w) => x ||| y) := ⟨BitVec.or_comm⟩
 
-@[simp] theorem or_self {x : BitVec w} : x ||| x = x := by
-  ext i
-  simp
-
-@[simp] theorem or_zero {x : BitVec w} : x ||| 0#w = x := by
-  ext i
-  simp
-
-@[simp] theorem zero_or {x : BitVec w} : 0#w ||| x = x := by
-  ext i
-  simp
-
-@[simp] theorem or_allOnes {x : BitVec w} : x ||| allOnes w = allOnes w := by
-  ext i
-  simp
-
-@[simp] theorem allOnes_or {x : BitVec w} : allOnes w ||| x = allOnes w := by
-  ext i
-  simp
-
 /-! ### and -/
 
 @[simp] theorem toNat_and (x y : BitVec v) :
@@ -771,26 +751,6 @@ theorem and_comm (x y : BitVec w) :
   simp [Bool.and_comm]
 instance : Std.Commutative (fun (x y : BitVec w) => x &&& y) := ⟨BitVec.and_comm⟩
 
-@[simp] theorem and_self {x : BitVec w} : x &&& x = x := by
-  ext i
-  simp
-
-@[simp] theorem and_zero {x : BitVec w} : x &&& 0#w = 0#w := by
-  ext i
-  simp
-
-@[simp] theorem zero_and {x : BitVec w} : 0#w &&& x = 0#w := by
-  ext i
-  simp
-
-@[simp] theorem and_allOnes {x : BitVec w} : x &&& allOnes w = x := by
-  ext i
-  simp
-
-@[simp] theorem allOnes_and {x : BitVec w} : allOnes w &&& x = x := by
-  ext i
-  simp
-
 /-! ### xor -/
 
 @[simp] theorem toNat_xor (x y : BitVec v) :
@@ -835,18 +795,6 @@ theorem xor_comm (x y : BitVec w) :
   simp [Bool.xor_comm]
 instance : Std.Commutative (fun (x y : BitVec w) => x ^^^ y) := ⟨BitVec.xor_comm⟩
 
-@[simp] theorem xor_self {x : BitVec w} : x ^^^ x = 0#w := by
-  ext i
-  simp
-
-@[simp] theorem xor_zero {x : BitVec w} : x ^^^ 0#w = x := by
-  ext i
-  simp
-
-@[simp] theorem zero_xor {x : BitVec w} : 0#w ^^^ x = x := by
-  ext i
-  simp
-
 /-! ### not -/
 
 theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
@@ -895,14 +843,6 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   ext
   simp
 
-@[simp] theorem xor_allOnes {x : BitVec w} : x ^^^ allOnes w = ~~~ x := by
-  ext i
-  simp
-
-@[simp] theorem allOnes_xor {x : BitVec w} : allOnes w ^^^ x = ~~~ x := by
-  ext i
-  simp
-
 /-! ### cast -/
 
 @[simp] theorem not_cast {x : BitVec w} (h : w = w') : ~~~(cast h x) = cast h (~~~x) := by
@@ -1476,7 +1416,7 @@ theorem setWidth_succ (x : BitVec w) :
     have j_lt : j.val < i := Nat.lt_of_le_of_ne (Nat.le_of_succ_le_succ j.isLt) j_eq
     simp [j_eq, j_lt]
 
-@[simp] theorem cons_msb_setWidth (x : BitVec (w+1)) : (cons x.msb (x.setWidth w)) = x := by
+theorem eq_msb_cons_setWidth (x : BitVec (w+1)) : x = (cons x.msb (x.setWidth w)) := by
   ext i
   simp
   split <;> rename_i h
@@ -1485,10 +1425,6 @@ theorem setWidth_succ (x : BitVec w) :
     · simp_all
     · omega
 
-@[deprecated "Use the reverse direction of `cons_msb_setWidth`"]
-theorem eq_msb_cons_setWidth (x : BitVec (w+1)) : x = (cons x.msb (x.setWidth w)) := by
-  simp
-
 @[simp] theorem not_cons (x : BitVec w) (b : Bool) : ~~~(cons b x) = cons (!b) (~~~x) := by
   simp [cons]
 
@@ -1728,15 +1664,6 @@ theorem BitVec.mul_add {x y z : BitVec w} :
   rw [Nat.mul_mod, Nat.mod_mod (y.toNat + z.toNat),
     ← Nat.mul_mod, Nat.mul_add]
 
-theorem mul_succ {x y : BitVec w} : x * (y + 1#w) = x * y + x := by simp [BitVec.mul_add]
-theorem succ_mul {x y : BitVec w} : (x + 1#w) * y = x * y + y := by simp [BitVec.mul_comm, BitVec.mul_add]
-
-theorem mul_two {x : BitVec w} : x * 2#w = x + x := by
-  have : 2#w = 1#w + 1#w := by apply BitVec.eq_of_toNat_eq; simp
-  simp [this, mul_succ]
-
-theorem two_mul {x : BitVec w} : 2#w * x = x + x := by rw [BitVec.mul_comm, mul_two]
-
 @[simp, bv_toNat] theorem toInt_mul (x y : BitVec w) :
   (x * y).toInt = (x.toInt * y.toInt).bmod (2^w) := by
   simp [toInt_eq_toNat_bmod]
@@ -2199,71 +2126,6 @@ theorem toNat_sub_of_le {x y : BitVec n} (h : y ≤ x) :
   · have : 2 ^ n - y.toNat + x.toNat = 2 ^ n + (x.toNat - y.toNat) := by omega
     rw [this, Nat.add_mod_left, Nat.mod_eq_of_lt (by omega)]
 
-/-! ### Decidable quantifiers -/
-
-theorem forall_zero_iff {P : BitVec 0 → Prop} :
-    (∀ v, P v) ↔ P 0#0 := by
-  constructor
-  · intro h
-    apply h
-  · intro h v
-    obtain (rfl : v = 0#0) := (by ext ⟨i, h⟩; simp at h)
-    apply h
-
-theorem forall_cons_iff {P : BitVec (n + 1) → Prop} :
-    (∀ v : BitVec (n + 1), P v) ↔ (∀ (x : Bool) (v : BitVec n), P (v.cons x)) := by
-  constructor
-  · intro h _ _
-    apply h
-  · intro h v
-    have w : v = (v.setWidth n).cons v.msb := by simp
-    rw [w]
-    apply h
-
-instance instDecidableForallBitVecZero (P : BitVec 0 → Prop) :
-    ∀ [Decidable (P 0#0)], Decidable (∀ v, P v)
-  | .isTrue h => .isTrue fun v => by
-    obtain (rfl : v = 0#0) := (by ext ⟨i, h⟩; cases h)
-    exact h
-  | .isFalse h => .isFalse (fun w => h (w _))
-
-instance instDecidableForallBitVecSucc (P : BitVec (n+1) → Prop) [DecidablePred P]
-    [Decidable (∀ (x : Bool) (v : BitVec n), P (v.cons x))] : Decidable (∀ v, P v) :=
-  decidable_of_iff' (∀ x (v : BitVec n), P (v.cons x)) forall_cons_iff
-
-instance instDecidableExistsBitVecZero (P : BitVec 0 → Prop) [Decidable (P 0#0)] :
-    Decidable (∃ v, P v) :=
-  decidable_of_iff (¬ ∀ v, ¬ P v) Classical.not_forall_not
-
-instance instDecidableExistsBitVecSucc (P : BitVec (n+1) → Prop) [DecidablePred P]
-    [Decidable (∀ (x : Bool) (v : BitVec n), ¬ P (v.cons x))] : Decidable (∃ v, P v) :=
-  decidable_of_iff (¬ ∀ v, ¬ P v) Classical.not_forall_not
-
-/--
-For small numerals this isn't necessary (as typeclass search can use the above two instances),
-but for large numerals this provides a shortcut.
-Note, however, that for large numerals the decision procedure may be very slow,
-and you should use `bv_decide` if possible.
--/
-instance instDecidableForallBitVec :
-    ∀ (n : Nat) (P : BitVec n → Prop) [DecidablePred P], Decidable (∀ v, P v)
-  | 0, _, _ => inferInstance
-  | n + 1, _, _ =>
-    have := instDecidableForallBitVec n
-    inferInstance
-
-/--
-For small numerals this isn't necessary (as typeclass search can use the above two instances),
-but for large numerals this provides a shortcut.
-Note, however, that for large numerals the decision procedure may be very slow.
--/
-instance instDecidableExistsBitVec :
-    ∀ (n : Nat) (P : BitVec n → Prop) [DecidablePred P], Decidable (∃ v, P v)
-  | 0, _, _ => inferInstance
-  | n + 1, _, _ =>
-    have := instDecidableExistsBitVec n
-    inferInstance
-
 /-! ### Deprecations -/
 
 set_option linter.missingDocs false

src/Init/Data/Fin/Basic.lean

@@ -14,7 +14,7 @@ instance coeToNat : CoeOut (Fin n) Nat :=
   ⟨fun v => v.val⟩
 
 /--
-From the empty type `Fin 0`, any desired result `α` can be derived. This is similar to `Empty.elim`.
+From the empty type `Fin 0`, any desired result `α` can be derived. This is simlar to `Empty.elim`.
 -/
 def elim0.{u} {α : Sort u} : Fin 0 → α
   | ⟨_, h⟩ => absurd h (not_lt_zero _)

src/Init/Data/Fin/Iterate.lean

@@ -26,7 +26,7 @@ def hIterateFrom (P : Nat → Sort _) {n} (f : ∀(i : Fin n), P i.val → P (i.
   decreasing_by decreasing_trivial_pre_omega
 
 /--
-`hIterate` is a heterogeneous iterative operation that applies a
+`hIterate` is a heterogenous iterative operation that applies a
 index-dependent function `f` to a value `init : P start` a total of
 `stop - start` times to produce a value of type `P stop`.
 
@@ -35,7 +35,7 @@ Concretely, `hIterate start stop f init` is equal to
   init |> f start _ |> f (start+1) _ ... |> f (end-1) _
 ```
 
-Because it is heterogeneous and must return a value of type `P stop`,
+Because it is heterogenous and must return a value of type `P stop`,
 `hIterate` requires proof that `start ≤ stop`.
 
 One can prove properties of `hIterate` using the general theorem
@@ -70,7 +70,7 @@ private theorem hIterateFrom_elim {P : Nat → Sort _}(Q : ∀(i : Nat), P i →
 
 /-
 `hIterate_elim` provides a mechanism for showing that the result of
-`hIterate` satisfies a property `Q stop` by showing that the states
+`hIterate` satisifies a property `Q stop` by showing that the states
 at the intermediate indices `i : start ≤ i < stop` satisfy `Q i`.
 -/
 theorem hIterate_elim {P : Nat → Sort _} (Q : ∀(i : Nat), P i → Prop)

src/Init/Data/Int/DivModLemmas.lean

@@ -194,7 +194,7 @@ theorem fdiv_eq_tdiv {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : fdiv a b = tdiv
 @[simp, norm_cast] theorem ofNat_emod (m n : Nat) : (↑(m % n) : Int) = m % n := rfl
 
 
-/-! ### mod definitions -/
+/-! ### mod definitiions -/
 
 theorem emod_add_ediv : ∀ a b : Int, a % b + b * (a / b) = a
   | ofNat _, ofNat _ => congrArg ofNat <| Nat.mod_add_div ..

src/Init/Data/List/Lemmas.lean

@@ -938,38 +938,6 @@ def foldrRecOn {motive : β → Sort _} : ∀ (l : List α) (op : α → β →
         x (mem_cons_self x l) :=
   rfl
 
-/--
-We can prove that two folds over the same list are related (by some arbitrary relation)
-if we know that the initial elements are related and the folding function, for each element of the list,
-preserves the relation.
--/
-theorem foldl_rel {l : List α} {f g : β → α → β} {a b : β} (r : β → β → Prop)
-    (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f c a) (g c' a)) :
-    r (l.foldl (fun acc a => f acc a) a) (l.foldl (fun acc a => g acc a) b) := by
-  induction l generalizing a b with
-  | nil => simp_all
-  | cons a l ih =>
-    simp only [foldl_cons]
-    apply ih
-    · simp_all
-    · exact fun a m c c' h => h' _ (by simp_all) _ _ h
-
-/--
-We can prove that two folds over the same list are related (by some arbitrary relation)
-if we know that the initial elements are related and the folding function, for each element of the list,
-preserves the relation.
--/
-theorem foldr_rel {l : List α} {f g : α → β → β} {a b : β} (r : β → β → Prop)
-    (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f a c) (g a c')) :
-    r (l.foldr (fun a acc => f a acc) a) (l.foldr (fun a acc => g a acc) b) := by
-  induction l generalizing a b with
-  | nil => simp_all
-  | cons a l ih =>
-    simp only [foldr_cons]
-    apply h'
-    · simp
-    · exact ih h fun a m c c' h => h' _ (by simp_all) _ _ h
-
 /-! ### getLast -/
 
 theorem getLast_eq_getElem : ∀ (l : List α) (h : l ≠ []),
@@ -1314,16 +1282,11 @@ theorem map_eq_iff : map f l = l' ↔ ∀ i : Nat, l'[i]? = l[i]?.map f := by
 theorem map_eq_foldr (f : α → β) (l : List α) : map f l = foldr (fun a bs => f a :: bs) [] l := by
   induction l <;> simp [*]
 
-@[simp] theorem map_set {f : α → β} {l : List α} {i : Nat} {a : α} :
-    (l.set i a).map f = (l.map f).set i (f a) := by
-  induction l generalizing i with
-  | nil => simp
-  | cons b l ih => cases i <;> simp_all
-
-@[deprecated "Use the reverse direction of `map_set`." (since := "2024-09-20")]
-theorem set_map {f : α → β} {l : List α} {n : Nat} {a : α} :
+@[simp] theorem set_map {f : α → β} {l : List α} {n : Nat} {a : α} :
     (map f l).set n (f a) = map f (l.set n a) := by
-  simp
+  induction l generalizing n with
+  | nil => simp
+  | cons b l ih => cases n <;> simp_all
 
 @[simp] theorem head_map (f : α → β) (l : List α) (w) :
     head (map f l) w = f (head l (by simpa using w)) := by

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -36,7 +36,7 @@ private theorem two_mul_sub_one {n : Nat} (n_pos : n > 0) : (2*n - 1) % 2 = 1 :=
 /-! ### Preliminaries -/
 
 /--
-An induction principal that works on division by two.
+An induction principal that works on divison by two.
 -/
 noncomputable def div2Induction {motive : Nat → Sort u}
     (n : Nat) (ind : ∀(n : Nat), (n > 0 → motive (n/2)) → motive n) : motive n := by

src/Init/Data/Nat/Div.lean

@@ -84,7 +84,7 @@ decreasing_by apply div_rec_lemma; assumption
 protected def mod : @& Nat → @& Nat → Nat
   /-
   Nat.modCore is defined by well-founded recursion and thus irreducible. Nevertheless it is
-  desirable if trivial `Nat.mod` calculations, namely
+  desireable if trivial `Nat.mod` calculations, namely
   * `Nat.mod 0 m` for all `m`
   * `Nat.mod n (m+n)` for concrete literals `n`
   reduce definitionally.

src/Init/Data/Nat/Mod.lean

@@ -15,7 +15,7 @@ in particular
 and its corollary
 `Nat.mod_pow_succ : x % b ^ (k + 1) = x % b ^ k + b ^ k * ((x / b ^ k) % b)`.
 
-It contains the necessary preliminary results relating order and `*` and `/`,
+It contains the necesssary preliminary results relating order and `*` and `/`,
 which should probably be moved to their own file.
 -/
 

src/Init/Data/Repr.lean

@@ -51,12 +51,6 @@ instance [Repr α] : Repr (id α) :=
 instance [Repr α] : Repr (Id α) :=
   inferInstanceAs (Repr α)
 
-/-
-This instance allows us to use `Empty` as a type parameter without causing instance synthesis to fail.
--/
-instance : Repr Empty where
-  reprPrec := nofun
-
 instance : Repr Bool where
   reprPrec
     | true, _  => "true"
@@ -163,7 +157,7 @@ protected def _root_.USize.repr (n : @& USize) : String :=
 
 /-- We statically allocate and memoize reprs for small natural numbers. -/
 private def reprArray : Array String := Id.run do
-  List.range 128 |>.map (·.toUSize.repr) |> List.toArray
+  List.range 128 |>.map (·.toUSize.repr) |> Array.mk
 
 private def reprFast (n : Nat) : String :=
   if h : n < 128 then Nat.reprArray.get ⟨n, h⟩ else

src/Init/GetElem.lean

@@ -156,11 +156,11 @@ theorem getElem?_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem d
 theorem getElem!_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     [Inhabited elem] (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] :
     c[i]! = c[i]'h := by
-  simp [getElem!_def, getElem?_def, h]
+  simp only [getElem!_def, getElem?_def, h]
 
 theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     [Inhabited elem] (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]! = default := by
-  simp [getElem!_def, getElem?_def, h]
+  simp only [getElem!_def, getElem?_def, h]
 
 namespace Fin
 

src/Init/Prelude.lean

@@ -757,8 +757,7 @@ noncomputable def Classical.ofNonempty {α : Sort u} [Nonempty α] : α :=
 instance (α : Sort u) {β : Sort v} [Nonempty β] : Nonempty (α → β) :=
   Nonempty.intro fun _ => Classical.ofNonempty
 
-instance Pi.instNonempty (α : Sort u) {β : α → Sort v} [(a : α) → Nonempty (β a)] :
-    Nonempty ((a : α) → β a) :=
+instance (α : Sort u) {β : α → Sort v} [(a : α) → Nonempty (β a)] : Nonempty ((a : α) → β a) :=
   Nonempty.intro fun _ => Classical.ofNonempty
 
 instance : Inhabited (Sort u) where
@@ -767,8 +766,7 @@ instance : Inhabited (Sort u) where
 instance (α : Sort u) {β : Sort v} [Inhabited β] : Inhabited (α → β) where
   default := fun _ => default
 
-instance Pi.instInhabited (α : Sort u) {β : α → Sort v} [(a : α) → Inhabited (β a)] :
-    Inhabited ((a : α) → β a) where
+instance (α : Sort u) {β : α → Sort v} [(a : α) → Inhabited (β a)] : Inhabited ((a : α) → β a) where
   default := fun _ => default
 
 deriving instance Inhabited for Bool
@@ -1212,7 +1210,7 @@ class HDiv (α : Type u) (β : Type v) (γ : outParam (Type w)) where
   * For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
   * For `Nat`, `a / b` rounds downwards.
   * For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
-    It is implemented as `Int.ediv`, the unique function satisfying
+    It is implemented as `Int.ediv`, the unique function satisfiying
     `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
     Other rounding conventions are available using the functions
     `Int.fdiv` (floor rounding) and `Int.div` (truncation rounding).
@@ -1366,7 +1364,7 @@ class Pow (α : Type u) (β : Type v) where
   /-- `a ^ b` computes `a` to the power of `b`. See `HPow`. -/
   pow : α → β → α
 
-/-- The homogeneous version of `Pow` where the exponent is a `Nat`.
+/-- The homogenous version of `Pow` where the exponent is a `Nat`.
 The purpose of this class is that it provides a default `Pow` instance,
 which can be used to specialize the exponent to `Nat` during elaboration.
 
@@ -2067,7 +2065,7 @@ The size of type `USize`, that is, `2^System.Platform.numBits`, which may
 be either `2^32` or `2^64` depending on the platform's architecture.
 
 Remark: we define `USize.size` using `(2^numBits - 1) + 1` to ensure the
-Lean unifier can solve constraints such as `?m + 1 = USize.size`. Recall that
+Lean unifier can solve contraints such as `?m + 1 = USize.size`. Recall that
 `numBits` does not reduce to a numeral in the Lean kernel since it is platform
 specific. Without this trick, the following definition would be rejected by the
 Lean type checker.
@@ -2711,10 +2709,7 @@ def Array.extract (as : Array α) (start stop : Nat) : Array α :=
   let sz' := Nat.sub (min stop as.size) start
   loop sz' start (mkEmpty sz')
 
-/--
-Auxiliary definition for `List.toArray`.
-`List.toArrayAux as r = r ++ as.toArray`
--/
+/-- Auxiliary definition for `List.toArray`. -/
 @[inline_if_reduce]
 def List.toArrayAux : List α → Array α → Array α
   | nil,       r => r

src/Init/Tactics.lean

@@ -1589,7 +1589,7 @@ macro "get_elem_tactic" : tactic =>
       There is a proof embedded in the right-hand-side, and we want it to be just `hi`.
       If `omega` is used to "fill" this proof, we will have a more complex proof term that
       cannot be inferred by unification.
-      We hardcoded `assumption` here to ensure users cannot accidentally break this IF
+      We hardcoded `assumption` here to ensure users cannot accidentaly break this IF
       they add new `macro_rules` for `get_elem_tactic_trivial`.
 
       TODO: Implement priorities for `macro_rules`.
@@ -1599,7 +1599,7 @@ macro "get_elem_tactic" : tactic =>
     | get_elem_tactic_trivial
     | fail "failed to prove index is valid, possible solutions:
   - Use `have`-expressions to prove the index is valid
-  - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid
+  - Use `a[i]!` notation instead, runtime check is perfomed, and 'Panic' error message is produced if index is not valid
   - Use `a[i]?` notation instead, result is an `Option` type
   - Use `a[i]'h` notation instead, where `h` is a proof that index is valid"
    )

src/Init/WFTactics.lean

@@ -20,7 +20,7 @@ macro "simp_wf" : tactic =>
 
 /--
 This tactic is used internally by lean before presenting the proof obligations from a well-founded
-definition to the user via `decreasing_by`. It is not necessary to use this tactic manually.
+definition to the user via `decreasing_by`. It is not necessary to use this tactic manuall.
 -/
 macro "clean_wf" : tactic =>
   `(tactic| simp

src/Lean/Compiler/IR/ResetReuse.lean

@@ -103,7 +103,7 @@ private def mkFresh : M VarId := do
 
 /--
 Helper function for applying `S`. We only introduce a `reset` if we managed
-to replace a `ctor` with `reuse` in `b`.
+to replace a `ctor` withe `reuse` in `b`.
 -/
 private def tryS (x : VarId) (c : CtorInfo) (b : FnBody) : M FnBody := do
   let w ← mkFresh

src/Lean/Compiler/LCNF/Simp/ConstantFold.lean

@@ -180,7 +180,7 @@ let _x.26 := @Array.push _ _x.24 z
 def foldArrayLiteral : Folder := fun args => do
   let #[_, .fvar fvarId] := args | return none
   let some (list, typ, level) ← getPseudoListLiteral fvarId | return none
-  let arr := list.toArray
+  let arr := Array.mk list
   let lit ← mkPseudoArrayLiteral arr typ level
   return some lit
 

src/Lean/Compiler/Old.lean

@@ -35,7 +35,7 @@ def checkIsDefinition (env : Environment) (n : Name) : Except String Unit :=
 match env.find? n with
   | (some (ConstantInfo.defnInfo _))   => Except.ok ()
   | (some (ConstantInfo.opaqueInfo _)) => Except.ok ()
-  | none => Except.error s!"unknown declaration '{n}'"
+  | none => Except.error s!"unknow declaration '{n}'"
   | _    => Except.error s!"declaration is not a definition '{n}'"
 
 /--

src/Lean/Data/Json/FromToJson.lean

@@ -28,12 +28,6 @@ instance : ToJson Json := ⟨id⟩
 instance : FromJson JsonNumber := ⟨Json.getNum?⟩
 instance : ToJson JsonNumber := ⟨Json.num⟩
 
-instance : FromJson Empty where
-  fromJson? j := throw (s!"type Empty has no constructor to match JSON value '{j}'. \
-                           This occurs when deserializing a value for type Empty, \
-                           e.g. at type Option Empty with code for the 'some' constructor.")
-
-instance : ToJson Empty := ⟨nofun⟩
 -- looks like id, but there are coercions happening
 instance : FromJson Bool := ⟨Json.getBool?⟩
 instance : ToJson Bool := ⟨fun b => b⟩

src/Lean/Data/JsonRpc.lean

@@ -266,7 +266,7 @@ instance [FromJson α] : FromJson (Notification α) where
       let params := params?
       let param : α ← fromJson? (toJson params)
       pure $ ⟨method, param⟩
-    else throw "not a notification"
+    else throw "not a notfication"
 
 end Lean.JsonRpc
 

src/Lean/Data/Lsp/InitShutdown.lean

@@ -36,7 +36,7 @@ instance : FromJson Trace := ⟨fun j =>
   | Except.ok "off"      => return Trace.off
   | Except.ok "messages" => return Trace.messages
   | Except.ok "verbose"  => return Trace.verbose
-  | _               => throw "unknown trace"⟩
+  | _               => throw "uknown trace"⟩
 
 instance Trace.hasToJson : ToJson Trace :=
 ⟨fun

src/Lean/Declaration.lean

@@ -239,7 +239,7 @@ structure InductiveVal extends ConstantVal where
   all : List Name
   /-- List of the names of the constructors for this inductive datatype. -/
   ctors : List Name
-  /-- Number of auxiliary data types produced from nested occurrences.
+  /-- Number of auxillary data types produced from nested occurrences.
   An inductive definition `T` is nested when there is a constructor with an argument `x : F T`,
    where `F : Type → Type` is some suitably behaved (ie strictly positive) function (Eg `Array T`, `List T`, `T × T`, ...).  -/
   numNested : Nat

src/Lean/Elab/AuxDef.lean

@@ -24,7 +24,7 @@ def elabAuxDef : CommandElab
     let id := `_aux ++ (← getMainModule) ++ `_ ++ id
     let id := String.intercalate "_" <| id.components.map (·.toString (escape := false))
     let ns ← getCurrNamespace
-    -- make sure we only add a single component so that scoped works
+    -- make sure we only add a single component so that scoped workes
     let id ← mkAuxName (ns.mkStr id) 1
     let id := id.replacePrefix ns Name.anonymous -- TODO: replace with def _root_.id
     elabCommand <|

src/Lean/Elab/Binders.lean

@@ -650,7 +650,7 @@ def elabLetDeclAux (id : Syntax) (binders : Array Syntax) (typeStx : Syntax) (va
     /-
     We use `withSynthesize` to ensure that any postponed elaboration problem
     and nested tactics in `type` are resolved before elaborating `val`.
-    Resolved: we want to avoid synthetic opaque metavariables in `type`.
+    Resolved: we want to avoid synthethic opaque metavariables in `type`.
     Recall that this kind of metavariable is non-assignable, and `isDefEq`
     may waste a lot of time unfolding declarations before failing.
     See issue #4051 for an example.

src/Lean/Elab/BuiltinCommand.lean

@@ -381,7 +381,7 @@ unsafe def elabEvalCoreUnsafe (bang : Bool) (tk term : Syntax): CommandElabM Uni
     -- Evaluate using term using `MetaEval` class.
     let elabMetaEval : CommandElabM Unit := do
       -- Generate an action without executing it. We use `withoutModifyingEnv` to ensure
-      -- we don't pollute the environment with auxliary declarations.
+      -- we don't polute the environment with auxliary declarations.
       -- We have special support for `CommandElabM` to ensure `#eval` can be used to execute commands
       -- that modify `CommandElabM` state not just the `Environment`.
       let act : Sum (CommandElabM Unit) (Environment → Options → IO (String × Except IO.Error Environment)) ←

src/Lean/Elab/Command.lean

@@ -532,7 +532,8 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro
       -- We can assume that the root command snapshot is not involved in parallelism yet, so this
       -- should be true iff the command supports incrementality
       if (← IO.hasFinished snap.new.result) then
-        liftCoreM <| Language.ToSnapshotTree.toSnapshotTree snap.new.result.get |>.trace
+        trace[Elab.snapshotTree]
+          (←Language.ToSnapshotTree.toSnapshotTree snap.new.result.get |>.format)
     modify fun st => { st with
       messages := initMsgs ++ msgs
       infoState := { st.infoState with trees := initInfoTrees ++ st.infoState.trees }

src/Lean/Elab/DeclModifiers.lean

@@ -120,7 +120,7 @@ section Methods
 
 variable [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadInfoTree m] [MonadLiftT IO m]
 
-/-- Elaborate declaration modifiers (i.e., attributes, `partial`, `private`, `protected`, `unsafe`, `noncomputable`, doc string)-/
+/-- Elaborate declaration modifiers (i.e., attributes, `partial`, `private`, `proctected`, `unsafe`, `noncomputable`, doc string)-/
 def elabModifiers (stx : Syntax) : m Modifiers := do
   let docCommentStx := stx[0]
   let attrsStx      := stx[1]

src/Lean/Elab/Extra.lean

@@ -375,7 +375,7 @@ private def hasHeterogeneousDefaultInstances (f : Expr) (maxType : Expr) (lhs :
   return false
 
 /--
-  Return `true` if polymorphic function `f` has a homogeneous instance of `maxType`.
+  Return `true` if polymorphic function `f` has a homogenous instance of `maxType`.
   The coercions to `maxType` only makes sense if such instance exists.
 
   For example, suppose `maxType` is `Int`, and `f` is `HPow.hPow`. Then,
@@ -421,9 +421,9 @@ mutual
       | .binop ref kind f lhs rhs =>
         /-
           We only keep applying coercions to `maxType` if `f` is predicate or
-          `f` has a homogeneous instance with `maxType`. See `hasHomogeneousInstance` for additional details.
+          `f` has a homogenous instance with `maxType`. See `hasHomogeneousInstance` for additional details.
 
-          Remark: We assume `binrel%` elaborator is only used with homogeneous predicates.
+          Remark: We assume `binrel%` elaborator is only used with homogenous predicates.
         -/
         if (← pure isPred <||> hasHomogeneousInstance f maxType) then
           return .binop ref kind f (← go lhs f true false) (← go rhs f false false)

src/Lean/Elab/Match.lean

@@ -30,7 +30,7 @@ private def mkUserNameFor (e : Expr) : TermElabM Name := do
 
 
 /--
-   Remark: if the discriminat is `Syntax.missing`, we abort the elaboration of the `match`-expression.
+   Remark: if the discriminat is `Systax.missing`, we abort the elaboration of the `match`-expression.
    This can happen due to error recovery. Example
    ```
    example : (p ∨ p) → p := fun h => match
@@ -795,7 +795,7 @@ private def elabMatchAltView (discrs : Array Discr) (alt : MatchAltView) (matchT
               let rhs ← elabTermEnsuringType alt.rhs matchType'
               -- We use all approximations to ensure the auxiliary type is defeq to the original one.
               unless (← fullApproxDefEq <| isDefEq matchType' matchType) do
-                throwError "type mismatch, alternative {← mkHasTypeButIsExpectedMsg matchType' matchType}"
+                throwError "type mistmatch, alternative {← mkHasTypeButIsExpectedMsg matchType' matchType}"
               let xs := altLHS.fvarDecls.toArray.map LocalDecl.toExpr ++ eqs
               let rhs ← if xs.isEmpty then pure <| mkSimpleThunk rhs else mkLambdaFVars xs rhs
               trace[Elab.match] "rhs: {rhs}"

src/Lean/Elab/PatternVar.lean

@@ -156,11 +156,9 @@ private def processVar (idStx : Syntax) : M Syntax := do
   modify fun s => { s with vars := s.vars.push idStx, found := s.found.insert id }
   return idStx
 
-private def samePatternsVariables (startingAt : Nat) (s₁ s₂ : State) : Bool := Id.run do
-  if h₁ : s₁.vars.size = s₂.vars.size then
-    for h₂ : i in [startingAt:s₁.vars.size] do
-      if s₁.vars[i] != s₂.vars[i]'(by obtain ⟨_, y⟩ := h₂; simp_all) then return false
-    true
+private def samePatternsVariables (startingAt : Nat) (s₁ s₂ : State) : Bool :=
+  if h : s₁.vars.size = s₂.vars.size then
+    Array.isEqvAux s₁.vars s₂.vars h (.==.) startingAt
   else
     false
 

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -126,7 +126,7 @@ def simpEqnType (eqnType : Expr) : MetaM Expr := do
     for y in ys.reverse do
       trace[Elab.definition] ">> simpEqnType: {← inferType y}, {type}"
       if proofVars.contains y.fvarId! then
-        let some (_, Expr.fvar fvarId, rhs) ← matchEq? (← inferType y) | throwError "unexpected hypothesis in alternative{indentExpr eqnType}"
+        let some (_, Expr.fvar fvarId, rhs) ← matchEq? (← inferType y) | throwError "unexpected hypothesis in altenative{indentExpr eqnType}"
         eliminated := eliminated.insert fvarId
         type := type.replaceFVarId fvarId rhs
       else if eliminated.contains y.fvarId! then

src/Lean/Elab/PreDefinition/Main.lean

@@ -104,7 +104,7 @@ Checks consistency of a clique of TerminationHints:
 
 * If not all have a hint, the hints are ignored (log error)
 * If one has `structural`, check that all have it, (else throw error)
-* A `structural` should not have a `decreasing_by` (else log error)
+* A `structural` shold not have a `decreasing_by` (else log error)
 
 -/
 def checkTerminationByHints (preDefs : Array PreDefinition) : CoreM Unit := do

src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean

@@ -119,7 +119,7 @@ def getRecArgInfos (fnName : Name) (xs : Array Expr) (value : Expr)
     (termArg? : Option TerminationArgument) : MetaM (Array RecArgInfo × MessageData) := do
   lambdaTelescope value fun ys _ => do
     if let .some termArg := termArg? then
-      -- User explicitly asked to use a certain argument, so throw errors eagerly
+      -- User explictly asked to use a certain argument, so throw errors eagerly
       let recArgInfo ← withRef termArg.ref do
         mapError (f := (m!"cannot use specified parameter for structural recursion:{indentD ·}")) do
           getRecArgInfo fnName xs.size (xs ++ ys) (← termArg.structuralArg)
@@ -189,7 +189,7 @@ def argsInGroup (group : IndGroupInst) (xs : Array Expr) (value : Expr)
     if (← group.isDefEq recArgInfo.indGroupInst) then
       return (.some recArgInfo)
 
-    -- Can this argument be understood as the auxiliary type former of a nested inductive?
+    -- Can this argument be understood as the auxillary type former of a nested inductive?
     if nestedTypeFormers.isEmpty then return .none
     lambdaTelescope value fun ys _ => do
       let x := (xs++ys)[recArgInfo.recArgPos]!

src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean

@@ -13,7 +13,7 @@ This module contains the types
 * `IndGroupInst` which extends `IndGroupInfo` with levels and parameters
    to indicate a instantiation of the group.
 
-One purpose of this abstraction is to make it clear when a function operates on a group as
+One purpose of this abstraction is to make it clear when a fuction operates on a group as
 a whole, rather than a specific inductive within the group.
 -/
 

src/Lean/Elab/PreDefinition/Structural/Preprocess.lean

@@ -17,7 +17,7 @@ private def shouldBetaReduce (e : Expr) (recFnNames : Array Name) : Bool :=
     false
 
 /--
-Preprocesses the expressions to improve the effectiveness of `elimRecursion`.
+Preprocesses the expessions to improve the effectiveness of `elimRecursion`.
 
 * Beta reduce terms where the recursive function occurs in the lambda term.
   Example:

src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean

@@ -31,7 +31,7 @@ structure RecArgInfo where
   indGroupInst : IndGroupInst
   /--
   index of the inductive datatype of the argument we are recursing on.
-  If `< indAll.all`, a normal data type, else an auxiliary data type due to nested recursion
+  If `< indAll.all`, a normal data type, else an auxillary data type due to nested recursion
   -/
   indIdx       : Nat
 deriving Inhabited
@@ -52,7 +52,7 @@ def RecArgInfo.pickIndicesMajor (info : RecArgInfo) (xs : Array Expr) : (Array E
   return (indexMajorArgs, otherArgs)
 
 /--
-Name of the recursive data type. Assumes that it is not one of the auxiliary ones.
+Name of the recursive data type. Assumes that it is not one of the auxillary ones.
 -/
 def RecArgInfo.indName! (info : RecArgInfo) : Name :=
   info.indGroupInst.all[info.indIdx]!

src/Lean/Elab/PreDefinition/TerminationArgument.lean

@@ -112,7 +112,7 @@ def TerminationArgument.delab (arity : Nat) (extraParams : Nat) (termArg : Termi
       let stxBody ← Delaborator.delab
       let hole : TSyntax `Lean.Parser.Term.hole ← `(hole|_)
 
-      -- any variable not mentioned syntactically (it may appear in the `Expr`, so do not just use
+      -- any variable not mentioned syntatically (it may appear in the `Expr`, so do not just use
       -- `e.bindingBody!.hasLooseBVar`) should be delaborated as a hole.
       let vars  : TSyntaxArray [`ident, `Lean.Parser.Term.hole] :=
         Array.map (fun (i : Ident) => if stxBody.raw.hasIdent i.getId then i else hole) vars

src/Lean/Elab/PreDefinition/TerminationHint.lean

@@ -45,7 +45,7 @@ structure TerminationHints where
   decreasingBy?  : Option DecreasingBy
   /--
   Here we record the number of parameters past the `:`. It is set by
-  `TerminationHints.rememberExtraParams` and used as follows:
+  `TerminationHints.rememberExtraParams` and used as folows:
 
   * When we guess the termination argument in `GuessLex` and want to print it in surface-syntax
     compatible form.

src/Lean/Elab/PreDefinition/WF/Basic.lean

@@ -12,7 +12,7 @@ namespace Lean.Elab.WF
 register_builtin_option debug.rawDecreasingByGoal : Bool := {
   defValue := false
   descr    := "Shows the raw `decreasing_by` goal including internal implementation detail \
-               instead of cleaning it up with the `clean_wf` tactic. Can be enabled for debugging \
+               intead of cleaning it up with the `clean_wf` tactic. Can be enabled for debugging \
                purposes. Please report an issue if you have to use this option for other reasons."
 }
 

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -66,7 +66,7 @@ private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
           else if let some mvarIds ← splitTarget? mvarId then
             mvarIds.forM go
           else
-            -- At some point in the past, we looked for occurrences of Wf.fix to fold on the
+            -- At some point in the past, we looked for occurences of Wf.fix to fold on the
             -- LHS (introduced in 096e4eb), but it seems that code path was never used,
             -- so #3133 removed it again (and can be recovered from there if this was premature).
             throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}"

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

@@ -29,7 +29,7 @@ if given, or the default `decreasing_tactic`.
 
 For mutual recursion, a single measure is not just one parameter, but one from each recursive
 function. Enumerating these can lead to a combinatoric explosion, so we bound
-the number of measures tried.
+the nubmer of measures tried.
 
 In addition to measures derived from `sizeOf xᵢ`, it also considers measures
 that assign an order to the functions themselves. This way we can support mutual
@@ -42,7 +42,7 @@ guessed lexicographic order.
 
 The following optimizations are applied to make this feasible:
 
-1. The crucial optimization is to look at each argument of each recursive call
+1. The crucial optimiziation is to look at each argument of each recursive call
    _once_, try to prove `<` and (if that fails `≤`), and then look at that table to
    pick a suitable measure.
 
@@ -80,7 +80,7 @@ register_builtin_option showInferredTerminationBy : Bool := {
 
 
 /--
-Given a predefinition, return the variable names in the outermost lambdas.
+Given a predefinition, return the variabe names in the outermost lambdas.
 Includes the “fixed prefix”.
 
 The length of the returned array is also used to determine the arity
@@ -550,7 +550,7 @@ where
         failure
 
 /--
-Enumerate all measures we want to try.
+Enumerate all meausures we want to try.
 
 All arguments (resp. combinations thereof) and
 possible orderings of functions (if more than one)

src/Lean/Elab/PreDefinition/WF/Preprocess.lean

@@ -17,7 +17,7 @@ private def shouldBetaReduce (e : Expr) (recFnNames : Array Name) : Bool :=
     false
 
 /--
-Preprocesses the expressions to improve the effectiveness of `wfRecursion`.
+Preprocesses the expessions to improve the effectiveness of `wfRecursion`.
 
 * Floats out the RecApp markers.
   Example:

src/Lean/Elab/RecAppSyntax.lean

@@ -29,7 +29,7 @@ def getRecAppSyntax? (e : Expr) : Option Syntax :=
   | _                => none
 
 /--
-Checks if the `MData` is for a recursive application.
+Checks if the `MData` is for a recursive applciation.
 -/
 def MData.isRecApp (d : MData) : Bool :=
   d.contains recAppKey

src/Lean/Elab/Structure.lean

@@ -772,7 +772,7 @@ private partial def mkCoercionToCopiedParent (levelParams : List Name) (params :
           let some fieldInfo := getFieldInfo? env parentStructName fieldName | unreachable!
           if fieldInfo.subobject?.isNone then throwError "failed to build coercion to parent structure"
           let resultType ← whnfD (← inferType result)
-          unless resultType.isForall do throwError "failed to build coercion to parent structure, unexpected type{indentExpr resultType}"
+          unless resultType.isForall do throwError "failed to build coercion to parent structure, unexpect type{indentExpr resultType}"
           let fieldVal ← copyFields resultType.bindingDomain!
           result := mkApp result fieldVal
       return result

src/Lean/Elab/SyntheticMVars.lean

@@ -21,7 +21,7 @@ private def resumeElabTerm (stx : Syntax) (expectedType? : Option Expr) (errToSo
     elabTerm stx expectedType? false
 
 /--
-  Try to elaborate `stx` that was postponed by an elaboration method using `Exception.postpone`.
+  Try to elaborate `stx` that was postponed by an elaboration method using `Expection.postpone`.
   It returns `true` if it succeeded, and `false` otherwise.
   It is used to implement `synthesizeSyntheticMVars`. -/
 private def resumePostponed (savedContext : SavedContext) (stx : Syntax) (mvarId : MVarId) (postponeOnError : Bool) : TermElabM Bool :=
@@ -86,7 +86,7 @@ private def synthesizePendingInstMVar (instMVar : MVarId) (extraErrorMsg? : Opti
   example (a : Int) (b c : Nat) : a = ↑b - ↑c := sorry
   ```
   We have two pending coercions for the `↑` and `HSub ?m.220 ?m.221 ?m.222`.
-  When we did not use a backtracking search here, then the homogeneous default instance for `HSub`.
+  When we did not use a backtracking search here, then the homogenous default instance for `HSub`.
   ```
   instance [Sub α] : HSub α α α where
   ```
@@ -306,7 +306,7 @@ inductive PostponeBehavior where
   | no
   /--
   Synthectic metavariables associated with type class resolution can be postponed.
-  Motivation: this kind of metavariable are not synthetic opaque, and can be assigned by `isDefEq`.
+  Motivation: this kind of metavariable are not synthethic opaque, and can be assigned by `isDefEq`.
   Unviverse constraints can also be postponed.
   -/
   | «partial»

src/Lean/Elab/Tactic/BVDecide.lean

@@ -71,7 +71,7 @@ For the second kind more steps are involved:
 3. Verify that algorithm in `Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas`.
 4. Integrate it with either the expression or predicate bitblaster and use the proof above to verify it.
 5. Add simplification lemmas for the primitive to `bv_normalize` in `Std.Tactic.BVDecide.Normalize`.
-   If there are multiple ways to write the primitive (e.g. with TC based notation and without) you
+   If there are mutliple ways to write the primitive (e.g. with TC based notation and without) you
    should normalize for one notation here.
 6. Add the reflection code to `Lean.Elab.Tactic.BVDecide.Frontend.BVDecide`
 7. Add a test!

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

@@ -24,7 +24,7 @@ register_builtin_option sat.solver : String := {
   defValue := ""
   descr :=
     "Name of the SAT solver used by Lean.Elab.Tactic.BVDecide tactics.\n
-     1. If this is set to something besides the empty string they will use that binary.\n
+     1. If this is set to something besides the emtpy string they will use that binary.\n
      2. If this is set to the empty string they will check if there is a cadical binary next to the\
         executing program. Usually that program is going to be `lean` itself and we do ship a\
         `cadical` next to it.\n

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

@@ -44,7 +44,7 @@ def bvCheck (g : MVarId) (cfg : TacticContext) : MetaM Unit := do
   let unsatProver : UnsatProver := fun reflectionResult _ => do
     withTraceNode `sat (fun _ => return "Preparing LRAT reflection term") do
       let proof ← lratChecker cfg reflectionResult.bvExpr
-      return .ok ⟨proof, ""⟩
+      return ⟨proof, ""⟩
   let _ ← closeWithBVReflection g unsatProver
   return ()
 

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

@@ -35,7 +35,7 @@ Reconstruct bit by bit which value expression must have had which `BitVec` value
 expression - pair values.
 -/
 def reconstructCounterExample (var2Cnf : Std.HashMap BVBit Nat) (assignment : Array (Bool × Nat))
-    (aigSize : Nat) (atomsAssignment : Std.HashMap Nat (Nat × Expr)) :
+    (aigSize : Nat) (atomsAssignment : Std.HashMap Nat Expr) :
     Array (Expr × BVExpr.PackedBitVec) := Id.run do
   let mut sparseMap : Std.HashMap Nat (RBMap Nat Bool Ord.compare) := {}
   for (bitVar, cnfVar) in var2Cnf.toArray do
@@ -70,7 +70,7 @@ def reconstructCounterExample (var2Cnf : Std.HashMap BVBit Nat) (assignment : Ar
       if bitValue then
         value := value ||| (1 <<< currentBit)
       currentBit := currentBit + 1
-    let atomExpr := atomsAssignment.get! bitVecVar |>.snd
+    let atomExpr := atomsAssignment.get! bitVecVar
     finalMap := finalMap.push (atomExpr, ⟨BitVec.ofNat currentBit value⟩)
   return finalMap
 
@@ -79,26 +79,18 @@ structure ReflectionResult where
   proveFalse : Expr → M Expr
   unusedHypotheses : Std.HashSet FVarId
 
-/--
-A counter example generated from the bitblaster.
--/
-structure CounterExample where
-  /--
-  The set of unused but potentially relevant hypotheses. Useful for diagnosing spurious counter
-  examples.
-  -/
-  unusedHypotheses : Std.HashSet FVarId
-  /--
-  The actual counter example as a list of equations denoted as `expr = value` pairs.
-  -/
-  equations : Array (Expr × BVExpr.PackedBitVec)
-
 structure UnsatProver.Result where
   proof : Expr
   lratCert : LratCert
 
-abbrev UnsatProver := ReflectionResult → Std.HashMap Nat (Nat × Expr) →
-    MetaM (Except CounterExample UnsatProver.Result)
+abbrev UnsatProver := ReflectionResult → Std.HashMap Nat Expr → MetaM UnsatProver.Result
+
+/--
+Contains values that will be used to diagnose spurious counter examples.
+-/
+structure DiagnosisInput where
+  unusedHypotheses : Std.HashSet FVarId
+  atomsAssignment : Std.HashMap Nat Expr
 
 /--
 The result of a spurious counter example diagnosis.
@@ -107,19 +99,20 @@ structure Diagnosis where
   uninterpretedSymbols : Std.HashSet Expr := {}
   unusedRelevantHypotheses : Std.HashSet FVarId := {}
 
-abbrev DiagnosisM : Type → Type := ReaderT CounterExample <| StateRefT Diagnosis MetaM
+abbrev DiagnosisM : Type → Type := ReaderT DiagnosisInput <| StateRefT Diagnosis MetaM
 
 namespace DiagnosisM
 
-def run (x : DiagnosisM Unit) (counterExample : CounterExample) : MetaM Diagnosis := do
-  let (_, issues) ← ReaderT.run x counterExample |>.run {}
+def run (x : DiagnosisM Unit) (unusedHypotheses : Std.HashSet FVarId)
+    (atomsAssignment : Std.HashMap Nat Expr) : MetaM Diagnosis := do
+  let (_, issues) ← ReaderT.run x { unusedHypotheses, atomsAssignment } |>.run {}
   return issues
 
 def unusedHyps : DiagnosisM (Std.HashSet FVarId) := do
   return (← read).unusedHypotheses
 
-def equations : DiagnosisM (Array (Expr × BVExpr.PackedBitVec)) := do
-  return (← read).equations
+def atomsAssignment : DiagnosisM (Std.HashMap Nat Expr) := do
+  return (← read).atomsAssignment
 
 def addUninterpretedSymbol (e : Expr) : DiagnosisM Unit :=
   modify fun s => { s with uninterpretedSymbols := s.uninterpretedSymbols.insert e }
@@ -138,7 +131,7 @@ Diagnose spurious counter examples, currently this checks:
 - Whether all hypotheses which contain any variable that was bitblasted were included
 -/
 def diagnose : DiagnosisM Unit := do
-  for (expr, _) in ← equations do
+  for (_, expr) in ← atomsAssignment do
     match_expr expr with
     | BitVec.ofBool x =>
       match x with
@@ -164,8 +157,9 @@ def unusedRelevantHypothesesExplainer (d : Diagnosis) : Option MessageData := do
 def explainers : List (Diagnosis → Option MessageData) :=
   [uninterpretedExplainer, unusedRelevantHypothesesExplainer]
 
-def explainCounterExampleQuality (counterExample : CounterExample) : MetaM MessageData := do
-  let diagnosis ← DiagnosisM.run DiagnosisM.diagnose counterExample
+def explainCounterExampleQuality (unusedHypotheses : Std.HashSet FVarId)
+    (atomsAssignment : Std.HashMap Nat Expr) : MetaM MessageData := do
+  let diagnosis ← DiagnosisM.run DiagnosisM.diagnose unusedHypotheses atomsAssignment
   let folder acc explainer := if let some m := explainer diagnosis then acc.push m else acc
   let explanations := explainers.foldl (init := #[]) folder
 
@@ -178,8 +172,8 @@ def explainCounterExampleQuality (counterExample : CounterExample) : MetaM Messa
     return err
 
 def lratBitblaster (cfg : TacticContext) (reflectionResult : ReflectionResult)
-    (atomsAssignment : Std.HashMap Nat (Nat × Expr)) :
-    MetaM (Except CounterExample UnsatProver.Result) := do
+    (atomsAssignment : Std.HashMap Nat Expr) :
+    MetaM UnsatProver.Result := do
   let bvExpr := reflectionResult.bvExpr
   let entry ←
     withTraceNode `bv (fun _ => return "Bitblasting BVLogicalExpr to AIG") do
@@ -207,10 +201,13 @@ def lratBitblaster (cfg : TacticContext) (reflectionResult : ReflectionResult)
   match res with
   | .ok cert =>
     let proof ← cert.toReflectionProof cfg bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true
-    return .ok ⟨proof, cert⟩
+    return ⟨proof, cert⟩
   | .error assignment =>
-    let equations := reconstructCounterExample map assignment aigSize atomsAssignment
-    return .error { unusedHypotheses := reflectionResult.unusedHypotheses, equations }
+    let reconstructed := reconstructCounterExample map assignment aigSize atomsAssignment
+    let mut error ← explainCounterExampleQuality reflectionResult.unusedHypotheses atomsAssignment
+    for (var, value) in reconstructed do
+      error := error ++ m!"{var} = {value.bv}\n"
+    throwError error
 
 
 def reflectBV (g : MVarId) : M ReflectionResult := g.withContext do
@@ -222,80 +219,51 @@ def reflectBV (g : MVarId) : M ReflectionResult := g.withContext do
       sats := sats.push reflected
     else
       unusedHypotheses := unusedHypotheses.insert hyp
-  if h : sats.size = 0 then
+  if sats.size = 0 then
     let mut error := "None of the hypotheses are in the supported BitVec fragment.\n"
     error := error ++ "There are two potential fixes for this:\n"
     error := error ++ "1. If you are using custom BitVec constructs simplify them to built-in ones.\n"
     error := error ++ "2. If your problem is using only built-in ones it might currently be out of reach.\n"
     error := error ++ "   Consider expressing it in terms of different operations that are better supported."
     throwError error
-  else
-    let sat := sats[1:].foldl (init := sats[0]) SatAtBVLogical.and
-    return {
-      bvExpr := sat.bvExpr,
-      proveFalse := sat.proveFalse,
-      unusedHypotheses := unusedHypotheses
-    }
+  let sat := sats.foldl (init := SatAtBVLogical.trivial) SatAtBVLogical.and
+  return {
+    bvExpr := sat.bvExpr,
+    proveFalse := sat.proveFalse,
+    unusedHypotheses := unusedHypotheses
+  }
 
 
 def closeWithBVReflection (g : MVarId) (unsatProver : UnsatProver) :
-    MetaM (Except CounterExample LratCert) := M.run do
+    MetaM LratCert := M.run do
   g.withContext do
     let reflectionResult ←
       withTraceNode `bv (fun _ => return "Reflecting goal into BVLogicalExpr") do
         reflectBV g
     trace[Meta.Tactic.bv] "Reflected bv logical expression: {reflectionResult.bvExpr}"
 
-    let atomsPairs := (← getThe State).atoms.toList.map (fun (expr, ⟨width, ident⟩) => (ident, (width, expr)))
+    let atomsPairs := (← getThe State).atoms.toList.map (fun (expr, _, ident) => (ident, expr))
     let atomsAssignment := Std.HashMap.ofList atomsPairs
-    match ← unsatProver reflectionResult atomsAssignment with
-    | .ok ⟨bvExprUnsat, cert⟩ =>
-      let proveFalse ← reflectionResult.proveFalse bvExprUnsat
-      g.assign proveFalse
-      return .ok cert
-    | .error counterExample => return .error counterExample
+    let ⟨bvExprUnsat, cert⟩ ← unsatProver reflectionResult atomsAssignment
+    let proveFalse ← reflectionResult.proveFalse bvExprUnsat
+    g.assign proveFalse
+    return cert
 
-def bvUnsat (g : MVarId) (cfg : TacticContext) : MetaM (Except CounterExample LratCert) := M.run do
+def bvUnsat (g : MVarId) (cfg : TacticContext) : MetaM LratCert := M.run do
   let unsatProver : UnsatProver := fun reflectionResult atomsAssignment => do
     withTraceNode `bv (fun _ => return "Preparing LRAT reflection term") do
       lratBitblaster cfg reflectionResult atomsAssignment
   closeWithBVReflection g unsatProver
 
-/--
-The result of calling `bv_decide`.
--/
 structure Result where
-  /--
-  Trace of the `simp` used in `bv_decide`'s normalization procedure.
-  -/
   simpTrace : Simp.Stats
-  /--
-  If the normalization step was not enough to solve the goal this contains the LRAT proof
-  certificate.
-  -/
   lratCert : Option LratCert
 
-/--
-Try to close `g` using a bitblaster. Return either a `CounterExample` if one is found or a `Result`
-if `g` is proven.
--/
-def bvDecide' (g : MVarId) (cfg : TacticContext) : MetaM (Except CounterExample Result) := do
-  let ⟨g?, simpTrace⟩ ← Normalize.bvNormalize g
-  let some g := g? | return .ok ⟨simpTrace, none⟩
-  match ← bvUnsat g cfg with
-  | .ok lratCert => return .ok ⟨simpTrace, some lratCert⟩
-  | .error counterExample => return .error counterExample
-
-/--
-Call `bvDecide'` and throw a pretty error if a counter example ends up being produced.
--/
 def bvDecide (g : MVarId) (cfg : TacticContext) : MetaM Result := do
-  match ← bvDecide' g cfg with
-  | .ok result => return result
-  | .error counterExample =>
-    let error ← explainCounterExampleQuality counterExample
-    let folder := fun error (var, value) => error ++ m!"{var} = {value.bv}\n"
-    throwError counterExample.equations.foldl (init := error) folder
+  let ⟨g?, simpTrace⟩ ← Normalize.bvNormalize g
+  let some g := g? | return ⟨simpTrace, none⟩
+  let lratCert ← bvUnsat g cfg
+  return ⟨simpTrace, some lratCert⟩
 
 @[builtin_tactic Lean.Parser.Tactic.bvDecide]
 def evalBvTrace : Tactic := fun

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

@@ -61,6 +61,14 @@ partial def of (h : Expr) : M (Option SatAtBVLogical) := do
     return some ⟨bvLogical.bvExpr, proof, bvLogical.expr⟩
   | _ => return none
 
+/--
+The trivially true `BVLogicalExpr`.
+-/
+def trivial : SatAtBVLogical where
+  bvExpr := .const true
+  expr := toExpr (.const true : BVLogicalExpr)
+  satAtAtoms := return mkApp (mkConst ``BVLogicalExpr.sat_true) (← M.atomsAssignment)
+
 /--
 Logical conjunction of two `ReifiedBVLogical`.
 -/

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

@@ -141,11 +141,10 @@ This will obtain an `LratCert` if the formula is UNSAT and throw errors otherwis
 def runExternal (cnf : CNF Nat) (solver : System.FilePath) (lratPath : System.FilePath)
     (trimProofs : Bool) (timeout : Nat) (binaryProofs : Bool)
     : MetaM (Except (Array (Bool × Nat)) LratCert) := do
-  IO.FS.withTempFile fun cnfHandle cnfPath => do
+  IO.FS.withTempFile fun _ cnfPath => do
     withTraceNode `sat (fun _ => return "Serializing SAT problem to DIMACS file") do
       -- lazyPure to prevent compiler lifting
-      cnfHandle.putStr  (← IO.lazyPure (fun _ => cnf.dimacs))
-      cnfHandle.flush
+      IO.FS.writeFile cnfPath (← IO.lazyPure (fun _ => cnf.dimacs))
 
     let res ←
       withTraceNode `sat (fun _ => return "Running SAT solver") do

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

@@ -27,6 +27,18 @@ namespace Frontend.Normalize
 open Lean.Meta
 open Std.Tactic.BVDecide.Normalize
 
+/--
+The bitblaster for multiplication introduces symbolic branches over the right hand side.
+If we have an expression of the form `c * x` where `c` is constant we should change it to `x * c`
+such that these symbolic branches get constant folded by the AIG framework.
+-/
+builtin_simproc [bv_normalize] mulConst ((_ : BitVec _) * (_ : BitVec _)) := fun e => do
+  let_expr HMul.hMul _ _ _ _ lhs rhs := e | return .continue
+  let some ⟨width, _⟩ ← Lean.Meta.getBitVecValue? lhs | return .continue
+  let new ← mkAppM ``HMul.hMul #[rhs, lhs]
+  let proof := mkApp3 (mkConst ``BitVec.mul_comm) (toExpr width) lhs rhs
+  return .done { expr := new, proof? := some proof }
+
 builtin_simproc [bv_normalize] eqToBEq (((_ : Bool) = (_ : Bool))) := fun e => do
   let_expr Eq _ lhs rhs := e | return .continue
   match_expr rhs with
@@ -53,7 +65,6 @@ def bvNormalize (g : MVarId) : MetaM Result := do
     let sevalSimprocs ← Simp.getSEvalSimprocs
 
     let simpCtx : Simp.Context := {
-      config := { failIfUnchanged := false, zetaDelta := true }
       simpTheorems := #[bvThms, sevalThms]
       congrTheorems := (← getSimpCongrTheorems)
     }

src/Lean/Elab/Tactic/Basic.lean

@@ -49,9 +49,6 @@ instance : Monad TacticM :=
   let i := inferInstanceAs (Monad TacticM);
   { pure := i.pure, bind := i.bind }
 
-instance : Inhabited (TacticM α) where
-  default := fun _ _ => default
-
 def getGoals : TacticM (List MVarId) :=
   return (← get).goals
 

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -90,7 +90,6 @@ where
         withAlwaysResolvedPromise fun finished => do
           withAlwaysResolvedPromise fun inner => do
             snap.new.resolve <| .mk {
-              desc := tac.getKind.toString
               diagnostics := .empty
               stx := tac
               inner? := some { range?, task := inner.result }

src/Lean/Elab/Tactic/Conv/Congr.lean

@@ -77,7 +77,7 @@ def congr (mvarId : MVarId) (addImplicitArgs := false) (nameSubgoals := true) :
 
 -- mvarIds is the list of goals produced by congr. We only want to change the one at position `i`
 -- so this closes all other equality goals with `rfl.`. There are non-equality goals produced
--- by `congr` (e.g. dependent instances), these are kept as goals.
+-- by `congr` (e.g. dependent instances), thes are kept as goals.
 private def selectIdx (tacticName : String) (mvarIds : List (Option MVarId)) (i : Int) :
   TacticM Unit := do
   if i >= 0 then

src/Lean/Elab/Tactic/Omega.lean

@@ -39,7 +39,7 @@ The `omega` tactic pre-processes the hypotheses in the following ways:
 * If `x / m` appears, for some `x : Int` and literal `m : Nat`,
   replace `x / m` with a new variable `α` and add the constraints
   `0 ≤ - m * α + x ≤ m - 1`.
-* If `x % m` appears, similarly, introduce the same new constraints
+* If `x % m` appears, similarly, introduce the same new contraints
   but replace `x % m` with `- m * α + x`.
 * Split conjunctions, existentials, and subtypes.
 * Record, for each appearance of `(a - b : Int)` with `a b : Nat`, the disjunction

src/Lean/Elab/Tactic/Omega/Core.lean

@@ -49,7 +49,7 @@ inductive Justification : Constraint → Coeffs → Type
   | combo {s t x y} (a : Int) (j : Justification s x) (b : Int) (k : Justification t y) :
     Justification (Constraint.combo a s b t) (Coeffs.combo a x b y)
   /--
-  The justification for the constraint constructed using "balanced mod" while
+  The justification for the constraing constructed using "balanced mod" while
   eliminating an equality.
   -/
   | bmod (m : Nat) (r : Int) (i : Nat) {x} (j : Justification (.exact r) x) :

src/Lean/Elab/Tactic/Omega/Frontend.lean

@@ -322,7 +322,7 @@ where
 end
 namespace MetaProblem
 
-/-- The trivial `MetaProblem`, with no facts to process and a trivial `Problem`. -/
+/-- The trivial `MetaProblem`, with no facts to processs and a trivial `Problem`. -/
 def trivial : MetaProblem where
   problem := {}
 

src/Lean/Elab/Term.lean

@@ -1045,7 +1045,7 @@ def exceptionToSorry (ex : Exception) (expectedType? : Option Expr) : TermElabM
   logException ex
   pure syntheticSorry
 
-/-- If `mayPostpone == true`, throw `Exception.postpone`. -/
+/-- If `mayPostpone == true`, throw `Expection.postpone`. -/
 def tryPostpone : TermElabM Unit := do
   if (← read).mayPostpone then
     throwPostpone

src/Lean/Environment.lean

@@ -718,7 +718,7 @@ def writeModule (env : Environment) (fname : System.FilePath) : IO Unit := do
   saveModuleData fname env.mainModule (← mkModuleData env)
 
 /--
-Construct a mapping from persistent extension name to extension index at the array of persistent extensions.
+Construct a mapping from persistent extension name to entension index at the array of persistent extensions.
 We only consider extensions starting with index `>= startingAt`.
 -/
 def mkExtNameMap (startingAt : Nat) : IO (Std.HashMap Name Nat) := do

src/Lean/Expr.lean

@@ -1628,7 +1628,7 @@ def nat? (e : Expr) : Option Nat := do
 /--
 Checks if an expression is an "integer numeral in normal form",
 i.e. of type `Nat` or `Int`, and either a natural number numeral in normal form (as specified by `nat?`),
-or the negation of a positive natural number numeral in normal form,
+or the negation of a positive natural number numberal in normal form,
 and if so returns the integer.
 -/
 def int? (e : Expr) : Option Int :=

src/Lean/Language/Basic.lean

@@ -205,19 +205,20 @@ abbrev SnapshotTree.element : SnapshotTree → Snapshot
 abbrev SnapshotTree.children : SnapshotTree → Array (SnapshotTask SnapshotTree)
   | mk _ children => children
 
-/-- Produces trace of given snapshot tree, synchronously waiting on all children. -/
-partial def SnapshotTree.trace (s : SnapshotTree) : CoreM Unit :=
-  go none s
+/-- Produces debug tree format of given snapshot tree, synchronously waiting on all children. -/
+partial def SnapshotTree.format [Monad m] [MonadFileMap m] [MonadLiftT IO m] :
+    SnapshotTree → m Format :=
+  go none
 where go range? s := do
   let file ← getFileMap
-  let mut desc := f!"{s.element.desc}"
+  let mut desc := f!"• {s.element.desc}"
   if let some range := range? then
     desc := desc ++ f!"{file.toPosition range.start}-{file.toPosition range.stop} "
   desc := desc ++ .prefixJoin "\n• " (← s.element.diagnostics.msgLog.toList.mapM (·.toString))
   if let some t := s.element.infoTree? then
-    trace[Elab.info] (← t.format)
-  withTraceNode `Elab.snapshotTree (fun _ => pure desc) do
-    s.children.toList.forM fun c => go c.range? c.get
+    desc := desc ++ f!"\n{← t.format}"
+  desc := desc ++ .prefixJoin "\n" (← s.children.toList.mapM fun c => go c.range? c.get)
+  return .nestD desc
 
 /--
   Helper class for projecting a heterogeneous hierarchy of snapshot classes to a homogeneous

src/Lean/Meta/ArgsPacker.lean

@@ -27,9 +27,9 @@ r'[p] = match p with | inl (x,y) => r1[x,y] | inr (x,y) => r2[x,y]
 The `ArgsPacker` data structure (defined in `Lean.Meta.ArgsPacker.Basic` for fewer module
 dependencies) contains necessary information to pack and unpack reliably. Care is taken that the
 code is not confused even if the user intentionally uses a `PSigma` or `PSum` type, e.g. as the
-ast parameter. Additionally, “good” variable names are stored here.
+ast parameter. Additionaly, “good” variable names are stored here.
 
-It is used in the translation of a possibly mutual, possibly n-ary recursive function to a single
+It is used in the transation of a possibly mutual, possibly n-ary recursive function to a single
 unary function, which can then be made non-recursive using `WellFounded.fix`.  Additional users are
 the `GuessLex` and `FunInd` modules, which also have to deal with this encoding.
 
@@ -550,7 +550,7 @@ brings `m1 : a → b → s` and `m2 : c → d → s` into scope. The continuatio
 
 where `m : a ⊗' b ⊕' c ⊗' d → s` is the uncurried form of `m1` and `m2`.
 
-The variable names `m1` and `m2` are taken from the parameter name in `t`, with numbers added
+The variable names `m1` and `m2` are taken from the paramter name in `t`, with numbers added
 unless `numFuns = 1`
 -/
 def curryParam {α} (argsPacker : ArgsPacker) (value : Expr) (type : Expr)

src/Lean/Meta/ArgsPacker/Basic.lean

@@ -24,7 +24,7 @@ structure ArgsPacker where
   /--
   Variable names to use when unpacking a packed argument.
 
-  Crucially, the size of this array also indicates the number of functions to pack, and
+  Crucialy, the size of this arry also indicates the number of functions to pack, and
   the length of each array the arity.
   -/
   varNamess : Array (Array Name)

src/Lean/Meta/Basic.lean

@@ -72,7 +72,7 @@ structure Config where
   constApprox        : Bool := false
   /--
     When the following flag is set,
-    `isDefEq` throws the exception `Exception.isDefEqStuck`
+    `isDefEq` throws the exception `Exeption.isDefEqStuck`
     whenever it encounters a constraint `?m ... =?= t` where
     `?m` is read only.
     This feature is useful for type class resolution where
@@ -1549,7 +1549,7 @@ def withLCtx (lctx : LocalContext) (localInsts : LocalInstances) : n α → n α
   mapMetaM <| withLocalContextImp lctx localInsts
 
 /--
-Runs `k` in a local environment with the `fvarIds` erased.
+Runs `k` in a local envrionment with the `fvarIds` erased.
 -/
 def withErasedFVars [MonadLCtx n] [MonadLiftT MetaM n] (fvarIds : Array FVarId) (k : n α) : n α := do
   let lctx ← getLCtx
@@ -1819,7 +1819,7 @@ partial def processPostponed (mayPostpone : Bool := true) (exceptionOnFailure :=
               return true
             else if numPostponed' < numPostponed then
               loop
-            -- If we cannot postpone anymore, `Config.univApprox := true`, but we haven't tried universe approximations yet,
+            -- If we cannot pospone anymore, `Config.univApprox := true`, but we haven't tried universe approximations yet,
             -- then try approximations before failing.
             else if !mayPostpone && (← getConfig).univApprox && !(← read).univApprox then
               withReader (fun ctx => { ctx with univApprox := true }) loop

src/Lean/Meta/CompletionName.lean

@@ -15,7 +15,7 @@ insert into Lean code.
 The `exact?` tactic is an example of a tactic that benefits from this
 functionality.  `exact?` finds lemmas in the environment to use to
 prove a theorem, but it needs to avoid inserting references to theorems
-with unstable names such as auxiliary lemmas that could change with
+with unstable names such as auxillary lemmas that could change with
 minor unintentional modifications to definitions.
 
 It uses a blacklist environment extension to enable names in an

src/Lean/Meta/Constructions/BRecOn.lean

@@ -139,7 +139,7 @@ private def mkBelowFromRec (recName : Name) (ibelow reflexive : Bool) (nParams :
     val := mkAppN val indices
     val := mkApp val major
 
-    -- All parameters of `.rec` besides the `minors` become parameters of `.below`
+    -- All paramaters of `.rec` besides the `minors` become parameters of `.below`
     let below_params := params ++ motives ++ indices ++ #[major]
     let type ← mkForallFVars below_params (.sort rlvl)
     val ← mkLambdaFVars below_params val
@@ -330,7 +330,7 @@ private def mkBRecOnFromRec (recName : Name) (ind reflexive : Bool) (nParams : N
       -- project out first component
       val ← mkPProdFst val
 
-      -- All parameters of `.rec` besides the `minors` become parameters of `.bRecOn`, and the `fs`
+      -- All paramaters of `.rec` besides the `minors` become parameters of `.bRecOn`, and the `fs`
       let below_params := params ++ motives ++ indices ++ #[major] ++ fs
       let type ← mkForallFVars below_params (mkAppN motives[idx]! (indices ++ #[major]))
       val ← mkLambdaFVars below_params val

src/Lean/Meta/Eqns.lean

@@ -32,7 +32,7 @@ These options affect the generation of equational theorems in a significant way.
 value at definition time, not realization time, should matter.
 
 This is implemented by
- * eagerly realizing the equations when they are set to a non-default value
+ * eagerly realizing the equations when they are set to a non-default vaule
  * when realizing them lazily, reset the options to their default
 -/
 def eqnAffectingOptions : Array (Lean.Option Bool) := #[backward.eqns.nonrecursive, backward.eqns.deepRecursiveSplit]

src/Lean/Meta/ExprDefEq.lean

@@ -92,7 +92,7 @@ where
                 continue
             trace[Meta.isDefEq.eta.struct] "{a} =?= {b} @ [{j}], {proj} =?= {args[i]!}"
             unless (← isDefEq proj args[i]!) do
-              trace[Meta.isDefEq.eta.struct] "failed, unexpected arg #{i}, projection{indentExpr proj}\nis not defeq to{indentExpr args[i]!}"
+              trace[Meta.isDefEq.eta.struct] "failed, unexpect arg #{i}, projection{indentExpr proj}\nis not defeq to{indentExpr args[i]!}"
               return false
           return true
       else
@@ -1879,7 +1879,7 @@ inductive DeltaStepResult where
 
 /--
 Perform one step of lazy delta reduction. This function decides whether to perform delta-reduction on `t`, `s`, or both.
-It is currently used to solve constraints of the form `(f a).i =?= (g a).i` where `i` is a numeral at `isDefEqProjDelta`.
+It is currently used to solve contraints of the form `(f a).i =?= (g a).i` where `i` is a numeral at `isDefEqProjDelta`.
 It is also a simpler version of `isDefEqDelta`. In the future, we may decide to combine these two functions like we do
 in the kernel.
 -/
@@ -1919,7 +1919,7 @@ where
     | .undef => return .cont t s
 
 /--
-Helper function for solving constraints of the form `t.i =?= s.i`.
+Helper function for solving contraints of the form `t.i =?= s.i`.
 -/
 private partial def isDefEqProjDelta (t s : Expr) (i : Nat) : MetaM Bool := do
   let t ← whnfCore t

src/Lean/Meta/Injective.lean

@@ -41,7 +41,7 @@ def elimOptParam (type : Expr) : CoreM Expr := do
   inductive Tmₛ.{u} :  Tyₛ.{u} -> Type (u+1)
   | app : Tmₛ (.SPi T A) -> (arg : T) -> Tmₛ (A arg)```
   ```
-  When looking for fixed arguments in `Tmₛ.app`, if we only consider occurrences in the term `Tmₛ (A arg)`,
+  When looking for fixed arguments in `Tmₛ.app`, if we only consider occurences in the term `Tmₛ (A arg)`,
   `T` is considered non-fixed despite the fact that `A : T -> Tyₛ`.
   This leads to an ill-typed injectivity theorem signature:
   ```lean

src/Lean/Meta/Instances.lean

@@ -113,34 +113,8 @@ For example:
     (because A B are out-params and are only filled in once we synthesize 2)
 
 (The type of `inst` must not contain mvars.)
-
-Remark: `projInfo?` is `some` if the instance is a projection.
-We need this information because of the heuristic we use to annotate binder
-information in projections. See PR #5376 and issue #5333. Before PR
-#5376, given a class `C` at
-```
-class A (n : Nat) where
-
-instance [A n] : A n.succ where
-
-class B [A 20050] where
-
-class C [A 20000] extends B where
-```
-we would get the following instance
-```
-C.toB [inst : A 20000] [self : @C inst] : @B ...
-```
-After the PR, we have
-```
-C.toB {inst : A 20000} [self : @C inst] : @B ...
-```
-Note the attribute `inst` is now just a regular implicit argument.
-To ensure `computeSynthOrder` works as expected, we should take
-this change into account while processing field `self`.
-This field is the one at position `projInfo?.numParams`.
 -/
-private partial def computeSynthOrder (inst : Expr) (projInfo? : Option ProjectionFunctionInfo) : MetaM (Array Nat) :=
+private partial def computeSynthOrder (inst : Expr) : MetaM (Array Nat) :=
   withReducible do
   let instTy ← inferType inst
 
@@ -177,8 +151,7 @@ private partial def computeSynthOrder (inst : Expr) (projInfo? : Option Projecti
   let tyOutParams ← getSemiOutParamPositionsOf ty
   let tyArgs := ty.getAppArgs
   for tyArg in tyArgs, i in [:tyArgs.size] do
-    unless tyOutParams.contains i do
-      assignMVarsIn tyArg
+    unless tyOutParams.contains i do assignMVarsIn tyArg
 
   -- Now we successively try to find the next ready subgoal, where all
   -- non-out-params are mvar-free.
@@ -186,13 +159,7 @@ private partial def computeSynthOrder (inst : Expr) (projInfo? : Option Projecti
   let mut toSynth := List.range argMVars.size |>.filter (argBIs[·]! == .instImplicit) |>.toArray
   while !toSynth.isEmpty do
     let next? ← toSynth.findM? fun i => do
-      let argTy ← instantiateMVars (← inferType argMVars[i]!)
-      if let some projInfo := projInfo? then
-        if projInfo.numParams == i then
-          -- See comment regarding `projInfo?` at the beginning of this function
-          assignMVarsIn argTy
-          return true
-      forallTelescopeReducing argTy fun _ argTy => do
+      forallTelescopeReducing (← instantiateMVars (← inferType argMVars[i]!)) fun _ argTy => do
       let argTy ← whnf argTy
       let argOutParams ← getSemiOutParamPositionsOf argTy
       let argTyArgs := argTy.getAppArgs
@@ -228,8 +195,7 @@ def addInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) : Meta
   let c ← mkConstWithLevelParams declName
   let keys ← mkInstanceKey c
   addGlobalInstance declName attrKind
-  let projInfo? ← getProjectionFnInfo? declName
-  let synthOrder ← computeSynthOrder c projInfo?
+  let synthOrder ← computeSynthOrder c
   instanceExtension.add { keys, val := c, priority := prio, globalName? := declName, attrKind, synthOrder } attrKind
 
 builtin_initialize

src/Lean/Meta/Iterator.lean

@@ -9,7 +9,7 @@ import Lean.Meta.Basic
 namespace Lean.Meta
 
 /--
-Provides an interface for iterating over values that are bundled with the `Meta` state
+Provides an iterface for iterating over values that are bundled with the `Meta` state
 they are valid in.
 -/
 protected structure Iterator (α : Type) where

src/Lean/Meta/LazyDiscrTree.lean

@@ -839,7 +839,7 @@ private def addConstImportData
     pure tree
 
 /--
-Contains the pre discrimination tree and any errors occurring during initialization of
+Contains the pre discrimination tree and any errors occuring during initialization of
 the library search tree.
 -/
 private structure InitResults (α : Type) where

src/Lean/Meta/Match/MatcherApp/Transform.lean

@@ -109,7 +109,7 @@ def addArg? (matcherApp : MatcherApp) (e : Expr) : MetaM (Option MatcherApp) :=
   refined, and not a type with a value.
 
   This is used in in `Lean.Elab.PreDefinition.WF.GuessFix` when constructing the context of recursive
-  calls to refine the functions' parameter, which may mention `major`.
+  calls to refine the functions' paramter, which may mention `major`.
   See there for how to use this function.
 -/
 def refineThrough (matcherApp : MatcherApp) (e : Expr) : MetaM (Array Expr) :=
@@ -379,12 +379,12 @@ The given `MatcherApp` must not use a splitter in `matcherName`.
 The resulting expression *will* use the splitter corresponding to `matcherName` (this is necessary
 for the construction).
 
-Internally, this needs to reduce the matcher in a given branch; this is done using
+Interally, this needs to reduce the matcher in a given branch; this is done using
 `Split.simpMatchTarget`.
 -/
 def inferMatchType (matcherApp : MatcherApp) : MetaM MatcherApp := do
   -- In matcherApp.motive, replace the (dummy) matcher body with a type
-  -- derived from the inferred types of the alternatives
+  -- derived from the inferred types of the alterantives
   let nExtra := matcherApp.remaining.size
   matcherApp.transform (useSplitter := true)
     (onMotive := fun motiveArgs body => do

src/Lean/Meta/Offset.lean

@@ -7,6 +7,7 @@ prelude
 import Lean.Data.LBool
 import Lean.Meta.InferType
 import Lean.Meta.NatInstTesters
+import Lean.Meta.NatInstTesters
 import Lean.Util.SafeExponentiation
 
 namespace Lean.Meta

src/Lean/Meta/PProdN.lean

@@ -8,7 +8,7 @@ prelude
 import Lean.Meta.InferType
 
 /-!
-This module provides functions to pack and unpack values using nested `PProd` or `And`,
+This module provides functios to pack and unpack values using nested `PProd` or `And`,
 as used in the `.below` construction, in the `.brecOn` construction for mutual recursion and
 and the `mutual_induct` construction.
 

src/Lean/Meta/SynthInstance.lean

@@ -442,7 +442,7 @@ private def hasUnusedArguments : Expr → Bool
 
 /--
   If the type of the metavariable `mvar` has unused argument, return a pair `(α, transformer)`
-  where `α` is a new type without the unused arguments and the `transformer` is a function for converting a
+  where `α` is a new type without the unused arguments and the `transformer` is a function for coverting a
   solution with type `α` into a value that can be assigned to `mvar`.
   Example: suppose `mvar` has type `(a : A) → (b : B a) → (c : C a) → D a c`, the result is the pair
   ```
@@ -752,7 +752,7 @@ private def applyCachedAbstractResult? (type : Expr) (abstResult? : Option Abstr
   let some abstResult := abstResult? | return none
   if abstResult.numMVars == 0 && abstResult.paramNames.isEmpty then
     /-
-    Result does not introduce new metavariables, thus we don't need to perform (again)
+    Result does not instroduce new metavariables, thus we don't need to perform (again)
     the `check` at `applyAbstractResult?`.
     This is an optimization.
     -/

src/Lean/Meta/Tactic/Cases.lean

@@ -327,7 +327,7 @@ def _root_.Lean.MVarId.byCasesDec (mvarId : MVarId) (p : Expr) (dec : Expr) (hNa
   let (fvarId, mvarId) ← mvarId.intro1
   let #[s₁, s₂] ← mvarId.cases fvarId #[{ varNames := [hName] }, { varNames := [hName] }] |
     throwError "'byCasesDec' tactic failed, unexpected number of subgoals"
-  -- We flip `s₁` and `s₂` because `isFalse` is the first constructor.
+  -- We flip `s₁` and `s₂` because `isFalse` is the first contructor.
   return ((← toByCasesSubgoal s₂), (← toByCasesSubgoal s₁))
 
 builtin_initialize registerTraceClass `Meta.Tactic.cases

src/Lean/Meta/Tactic/FunInd.lean

@@ -125,7 +125,7 @@ For a non-mutual, unary function `foo` (or else for the `_unary` function), we
    hypothesis is now itself a `match` statement (cf. `Lean.Meta.MatcherApp.inferMatchType`)
 
    The termination proof of `foo` may have abstracted over some proofs; these proofs must be
-   transferred, so auxiliary lemmas are unfolded if needed.
+   transferred, so auxillary lemmas are unfolded if needed.
 
 7. After this construction, the MVars introduced by `buildInductionCase` are turned into parameters.
 
@@ -150,7 +150,7 @@ foo.mutual_induct : {motive1 : a → b → Prop} {motive2 : c → Prop} →
 where all the `PSum`/`PSigma` encoding has been resolved. This theorem is attached to the
 name of the first function in the mutual group, like the `._unary` definition.
 
-Finally, in `deriveUnpackedInduction`, for each of the functions in the mutual group, a simple
+Finally, in `deriveUnpackedInduction`, for each of the funtions in the mutual group, a simple
 projection yields the final `foo.induct` theorem:
 ```
 foo.induct : {motive1 : a → b → Prop} {motive2 : c → Prop} →
@@ -246,11 +246,11 @@ re-assembling we have to be supple (mainly around `PProd.fst`/`PProd.snd`). As w
 the term we check if it has type `motive xs..`. If it has, then know we have just found and
 rewritten a recursive call, and this type nicely provides us the arguments `xs`. So at this point
 we store the rewritten expression as a new induction hypothesis (using `M.tell`) and rewrite to
-`f xs..`, which now again has the same type as the original term, and the further re-assembly should
+`f xs..`, which now again has the same type as the original term, and the furthe re-assembly should
 work. Half this logic is in the `isRecCall` parameter.
 
 If this process fails we’ll get weird type errors (caught later on). We'll see if we need to
-improve the errors, for example by passing down a flag whether we expect the same type (and no
+imporve the errors, for example by passing down a flag whether we expect the same type (and no
 occurrences of `newIH`), or whether we are in “supple mode”, and catch it earlier if the rewriting
 fails.
 -/
@@ -270,7 +270,7 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
     if let some matcherApp ← matchMatcherApp? e (alsoCasesOn := true) then
       if matcherApp.remaining.size == 1 && matcherApp.remaining[0]!.isFVarOf oldIH then
         -- We do different things to the matcher when folding recursive calls and when
-        -- collecting inductive hypotheses. Therefore we do it separately,
+        -- collecting inductive hypotheses. Therfore we do it separately,
         -- droppin got `MetaM` in between, and using `M.eval`/`M.exec` as appropriate
         -- We could try to do it in one pass by breaking up the `matcherApp.transform`
         -- abstraction.
@@ -288,8 +288,8 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
               let eTypeAbst ← kabstract eTypeAbst discr
               return eTypeAbst.instantiate1 motiveArg
 
-            -- Will later be overridden with a type that’s itself a match
-            -- statement and the inferred alt types
+            -- Will later be overriden with a type that’s itself a match
+            -- statement and the infered alt types
             let dummyGoal := mkConst ``True []
             mkArrow eTypeAbst dummyGoal)
           (onAlt := fun altType alt => do
@@ -403,7 +403,7 @@ def assertIHs (vals : Array Expr) (mvarid : MVarId) : MetaM MVarId := do
 
 /--
 Goal cleanup:
-Substitutes equations (with `substVar`) to remove superfluous variables, and clears unused
+Substitutes equations (with `substVar`) to remove superfluous varialbes, and clears unused
 let bindings.
 
 Substitutes from the outside in so that the inner-bound variable name wins, but does a first pass
@@ -631,7 +631,7 @@ variables), so after this operations, terms that still mention these meta variab
 be used anymore.
 
 We are not using `mkLambdaFVars` on mvars directly, nor `abstractMVars`, as these at the moment
-do not handle delayed assignments correctly.
+do not handle delayed assignemnts correctly.
 -/
 def abstractIndependentMVars (mvars : Array MVarId) (index : Nat) (e : Expr) : MetaM Expr := do
   trace[Meta.FunInd] "abstractIndependentMVars, to revert after {index}, original mvars: {mvars}"
@@ -840,7 +840,7 @@ def unpackMutualInduction (eqnInfo : WF.EqnInfo) (unaryInductName : Name) : Meta
         return value
 
   unless ← isTypeCorrect value do
-    logError m!"failed to unpack induction principle:{indentExpr value}"
+    logError m!"failed to unpack induction priciple:{indentExpr value}"
     check value
   let type ← inferType value
   let type ← elimOptParam type
@@ -924,7 +924,7 @@ def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit
       let group : Structural.IndGroupInst := { Structural.IndGroupInfo.ofInductiveVal indInfo with
         levels := indLevels, params := brecOnArgs }
 
-      -- We also need to know the number of indices of each type former, including the auxiliary
+      -- We also need to know the number of indices of each type former, including the auxillary
       -- type formers that do not have IndInfo. We can read it off the motives types of the recursor.
       let numTargetss ← do
         let aux := mkAppN (.const recInfo.name (0 :: group.levels)) group.params
@@ -984,7 +984,7 @@ def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit
           let packedMotives ← positions.mapMwith PProdN.packLambdas brecMotiveTypes brecMotives
           trace[Meta.FunInd] m!"packedMotives: {packedMotives}"
 
-          -- Now we can calculate the expected types of the minor arguments
+          -- Now we can calcualte the expected types of the minor arguments
           let minorTypes ← inferArgumentTypesN recInfo.numMotives <|
             mkAppN (group.brecOn true lvl 0) (packedMotives ++ brecOnTargets)
           trace[Meta.FunInd] m!"minorTypes: {minorTypes}"

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

@@ -78,7 +78,7 @@ def _root_.Lean.MVarId.byContra? (mvarId : MVarId) : MetaM (Option MVarId) := mv
 
 /--
 Clear auxiliary decls used to encode recursive declarations.
-`grind` eliminates them to ensure they are not accidentally used by its proof automation.
+`grind` eliminates them to ensure they are not accidentaly used by its proof automation.
 -/
 def _root_.Lean.MVarId.clearAuxDecls (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
   mvarId.checkNotAssigned `grind.clear_aux_decls

src/Lean/Meta/Tactic/LibrarySearch.lean

@@ -102,7 +102,7 @@ def droppedKeys : List (List LazyDiscrTree.Key) := [[.star], [.const `Eq 3, .sta
 /--
 The maximum number of constants an individual task may perform.
 
-The value was picked because it roughly corresponded to 50ms of work on the
+The value was picked because it roughly correponded to 50ms of work on the
 machine this was developed on.  Smaller numbers did not seem to improve
 performance when importing Std and larger numbers (<10k) seemed to degrade
 initialization performance.

src/Lean/Meta/Tactic/Refl.lean

@@ -12,9 +12,6 @@ namespace Lean.Meta
 
 /--
 Close given goal using `Eq.refl`.
-
-See `Lean.MVarId.applyRfl` for the variant that also consults `@[refl]` lemmas, and which
-backs the `rfl` tactic.
 -/
 def _root_.Lean.MVarId.refl (mvarId : MVarId) : MetaM Unit := do
   mvarId.withContext do

src/Lean/Meta/Tactic/Rewrites.lean

@@ -102,7 +102,7 @@ private builtin_initialize ext : EnvExtension ExtState ←
 /--
 The maximum number of constants an individual task may perform.
 
-The value was picked because it roughly corresponded to 50ms of work on the
+The value was picked because it roughly correponded to 50ms of work on the
 machine this was developed on.  Smaller numbers did not seem to improve
 performance when importing Std and larger numbers (<10k) seemed to degrade
 initialization performance.

src/Lean/Meta/Tactic/Rfl.lean

@@ -50,59 +50,33 @@ open Elab Tactic
 
 /-- `MetaM` version of the `rfl` tactic.
 
-This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive
-relation, that is, equality or another relation which has a reflexive lemma tagged with the
-attribute [refl].
+This tactic applies to a goal whose target has the form `x ~ x`,
+where `~` is a reflexive relation other than `=`,
+that is, a relation which has a reflexive lemma tagged with the attribute @[refl].
 -/
-def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext do
-  -- NB: uses whnfR, we do not want to unfold the relation itself
-  let t ← whnfR <|← instantiateMVars <|← goal.getType
-  if t.getAppNumArgs < 2 then
-    throwError "rfl can only be used on binary relations, not{indentExpr (← goal.getType)}"
-
-  -- Special case HEq here as it has a different argument order.
-  if t.isAppOfArity ``HEq 4 then
-    let gs ← goal.applyConst ``HEq.refl
-    unless gs.isEmpty do
-      throwError MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
-        goalsToMessageData gs}"
-    return
-
-  let rel := t.appFn!.appFn!
-  let lhs := t.appFn!.appArg!
-  let rhs := t.appArg!
-
-  let success ← approxDefEq <| isDefEqGuarded lhs rhs
-  unless success do
-    let explanation := MessageData.ofLazyM (es := #[lhs, rhs]) do
-      let (lhs, rhs) ← addPPExplicitToExposeDiff lhs rhs
-      return m!"The lhs{indentExpr lhs}\nis not definitionally equal to rhs{indentExpr rhs}"
-    throwTacticEx `apply_rfl goal explanation
-
-  if rel.isAppOfArity `Eq 1 then
-    -- The common case is equality: just use `Eq.refl`
-    let us := rel.appFn!.constLevels!
-    let α :=  rel.appArg!
-    goal.assign (mkApp2 (mkConst ``Eq.refl us) α lhs)
+def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := do
+  let .app (.app rel _) _ ← whnfR <|← instantiateMVars <|← goal.getType
+    | throwError "reflexivity lemmas only apply to binary relations, not{
+        indentExpr (← goal.getType)}"
+  if let .app (.const ``Eq [_]) _ := rel then
+    throwError "MVarId.applyRfl does not solve `=` goals. Use `MVarId.refl` instead."
   else
-    -- Else search through `@refl` keyed by the relation
     let s ← saveState
     let mut ex? := none
     for lem in ← (reflExt.getState (← getEnv)).getMatch rel reflExt.config do
       try
         let gs ← goal.apply (← mkConstWithFreshMVarLevels lem)
         if gs.isEmpty then return () else
-          throwError MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
+          logError <| MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
             goalsToMessageData gs}"
       catch e =>
-        unless ex?.isSome do
-          ex? := some (← saveState, e) -- stash the first failure of `apply`
+        ex? := ex? <|> (some (← saveState, e)) -- stash the first failure of `apply`
       s.restore
     if let some (sErr, e) := ex? then
       sErr.restore
       throw e
     else
-      throwError "rfl failed, no @[refl] lemma registered for relation{indentExpr rel}"
+      throwError "rfl failed, no lemma with @[refl] applies"
 
 /-- Helper theorem for `Lean.MVarId.liftReflToEq`. -/
 private theorem rel_of_eq_and_refl {α : Sort _} {R : α → α → Prop}