chore: cleanup of Array docstrings after refactor

This is a second attempt at #5446, first reverting parts of #5403.

.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 occured 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 occurred 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 overriden)
+      # (needs to be after "Checkout" so files don't get overridden)
       - 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,16 +329,17 @@ 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 "nightly-testing-'"${MOST_RECENT_NIGHTLY}"'",' lakefile.lean
+            sed -i 's,require "leanprover-community" / "batteries" @ git ".\+",require "leanprover-community" / "batteries" @ git "lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}",' 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, pushing an empty commit."
+            echo "Branch already exists, merging $BASE and bumping Batteries."
             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 discrepency in universe parameter order between `theorem` and `def` declarations.
+  * [#4408](https://github.com/leanprover/lean4/pull/4408) fixes a discrepancy 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 ouput of `#print axioms` for determinism.
+  * [#4416](https://github.com/leanprover/lean4/pull/4416) sorts the output 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 individal 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 individual 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 explictly unfold the function definition (using `simp`,
+  rewritten to explicitly 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 langauge (e.g. `RBMap`)
+     essential datatypes not provided by the core language (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 availabe in the core langauge.
+* `omega`, our integer linear arithmetic tactic, is now available in the core language.
   * 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 simplied further.
+        not need to be simplified 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` contructor may also take `none`.
+      All three constructors take a `Result`. The `.continue` constructor 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 interpetation of an empty string and allow a string to flow across multiple lines without introducing additional whitespace.
+  These have the interpretation 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 libarary to explicitly give one:
+  you can use `WellFounded.wrap` from the std library to explicitly give one:
   ```diff
   -termination_by' ⟨r, hwf⟩
   +termination_by x => hwf.wrap x

doc/dev/bootstrap.md

@@ -73,7 +73,7 @@ update the archived C source code of the stage 0 compiler in `stage0/src`.
 The github repository will automatically update stage0 on `master` once
 `src/stdlib_flags.h` and `stage0/src/stdlib_flags.h` are out of sync.
 
-If you have write access to the lean4 repository, you can also also manually
+If you have write access to the lean4 repository, you can also manually
 trigger that process, for example to be able to use new features in the compiler itself.
 You can do that on <https://github.com/leanprover/lean4/actions/workflows/update-stage0.yml>
 or using Github CLI with

doc/dev/release_checklist.md

@@ -71,6 +71,12 @@ 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} contructors"
+      throwTacticEx `ctor mvarId "invalid index, inductive datatype has only {ctors.length} constructors"
 
 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/simplications rules.
+use hypotheses such as `a = b` as rewriting/simplifications 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/simplications rules.
+use hypotheses such as `a = b` as rewriting/simplifications 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/tc.lean

@@ -29,7 +29,7 @@ inductive HasType : Expr → Ty → Prop
 
 /-!
 We can easily show that if `e` has type `t₁` and type `t₂`, then `t₁` and `t₂` must be equal
-by using the the `cases` tactic. This tactic creates a new subgoal for every constructor,
+by using the `cases` tactic. This tactic creates a new subgoal for every constructor,
 and automatically discharges unreachable cases. The tactic combinator `tac₁ <;> tac₂` applies
 `tac₂` to each subgoal produced by `tac₁`. Then, the tactic `rfl` is used to close all produced
 goals using reflexivity.
@@ -82,7 +82,7 @@ theorem Expr.typeCheck_correct (h₁ : HasType e ty) (h₂ : e.typeCheck ≠ .un
 /-!
 Now, we prove that if `Expr.typeCheck e` returns `Maybe.unknown`, then forall `ty`, `HasType e ty` does not hold.
 The notation `e.typeCheck` is sugar for `Expr.typeCheck e`. Lean can infer this because we explicitly said that `e` has type `Expr`.
-The proof is by induction on `e` and case analysis. The tactic `rename_i` is used to to rename "inaccessible" variables.
+The proof is by induction on `e` and case analysis. The tactic `rename_i` is used to rename "inaccessible" variables.
 We say a variable is inaccessible if it is introduced by a tactic (e.g., `cases`) or has been shadowed by another variable introduced
 by the user. Note that the tactic `simp [typeCheck]` is applied to all goal generated by the `induction` tactic, and closes
 the cases corresponding to the constructors `Expr.nat` and `Expr.bool`.

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` instnace.
+we need `FromJson` and `ToJson` instance.
 We'll see why the position field is needed later.
 -/
 

doc/expressions.md

@@ -396,7 +396,7 @@ Every expression in Lean has a natural computational interpretation, unless it i
 
 * *β-reduction* : An expression ``(λ x, t) s`` β-reduces to ``t[s/x]``, that is, the result of replacing ``x`` by ``s`` in ``t``.
 * *ζ-reduction* : An expression ``let x := s in t`` ζ-reduces to ``t[s/x]``.
-* *δ-reduction* : If ``c`` is a defined constant with definition ``t``, then ``c`` δ-reduces to to ``t``.
+* *δ-reduction* : If ``c`` is a defined constant with definition ``t``, then ``c`` δ-reduces to ``t``.
 * *ι-reduction* : When a function defined by recursion on an inductive type is applied to an element given by an explicit constructor, the result ι-reduces to the specified function value, as described in [Inductive Types](inductive.md).
 
 The reduction relation is transitive, which is to say, is ``s`` reduces to ``s'`` and ``t`` reduces to ``t'``, then ``s t`` reduces to ``s' t'``, ``λ x, s`` reduces to ``λ x, s'``, and so on. If ``s`` and ``t`` reduce to a common term, they are said to be *definitionally equal*. Definitional equality is defined to be the smallest equivalence relation that satisfies all these properties and also includes α-equivalence and the following two relations:

doc/monads/laws.lean

@@ -171,7 +171,7 @@ of data contained in the container resulting in a new container that has the sam
 
 `u <*> pure y = pure (. y) <*> u`.
 
-This law is is a little more complicated, so don't sweat it too much. It states that the order that
+This law is a little more complicated, so don't sweat it too much. It states that the order that
 you wrap things shouldn't matter. One the left, you apply any applicative `u` over a pure wrapped
 object. On the right, you first wrap a function applying the object as an argument. Note that `(·
 y)` is short hand for: `fun f => f y`. Then you apply this to the first applicative `u`. These

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 comitted
+# copy the README to ensure the `stage0/src/lake` directory is committed
 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 supercedes byCases in Decidable
+-- this supersedes byCases in Decidable
 theorem byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
   Decidable.byCases (dec := propDecidable _) hpq hnpq
 
--- this supercedes byContradiction in Decidable
+-- this supersedes byContradiction in Decidable
 theorem byContradiction {p : Prop} (h : ¬p → False) : p :=
   Decidable.byContradiction (dec := propDecidable _) h
 

src/Init/Core.lean

@@ -1892,7 +1892,8 @@ 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 {α : Sort u} {β : α → Sort v} [∀ a, Subsingleton (β a)] : Subsingleton (∀ a, β a) where
+instance Pi.instSubsingleton {α : Sort u} {β : α → Sort v} [∀ a, Subsingleton (β a)] :
+    Subsingleton (∀ a, β a) where
   allEq f g := funext fun a => Subsingleton.elim (f a) (g a)
 
 /-! # Squash -/
@@ -2055,7 +2056,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 infering the identity using class resoluton.
+is used primarily for inferring the identity using class resolution.
 -/
 class LeftIdentity (op : α → β → β) (o : outParam α) : Prop
 
@@ -2071,7 +2072,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 infering the identity using class resoluton.
+primarily for inferring the identity using class resolution.
 -/
 class RightIdentity (op : α → β → α) (o : outParam β) : Prop
 
@@ -2087,7 +2088,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 infering the identity using class resoluton.
+primarily for inferring the identity using class resolution.
 -/
 class Identity (op : α → α → α) (o : outParam α) extends LeftIdentity op o, RightIdentity op o : Prop
 

src/Init/Data.lean

@@ -33,7 +33,6 @@ 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.lean

@@ -15,3 +15,4 @@ import Init.Data.Array.BasicAux
 import Init.Data.Array.Lemmas
 import Init.Data.Array.TakeDrop
 import Init.Data.Array.Bootstrap
+import Init.Data.Array.GetLit

src/Init/Data/Array/Basic.lean

@@ -13,43 +13,75 @@ import Init.Data.ToString.Basic
 import Init.GetElem
 universe u v w
 
-namespace Array
+/-! ### Array literal syntax -/
+
+syntax "#[" withoutPosition(sepBy(term, ", ")) "]" : term
+
+macro_rules
+  | `(#[ $elems,* ]) => `(List.toArray [ $elems,* ])
+
 variable {α : Type u}
 
+namespace Array
+
+/-! ### Preliminary theorems -/
+
+@[simp] theorem size_set (a : Array α) (i : Fin a.size) (v : α) : (set a i v).size = a.size :=
+  List.length_set ..
+
+@[simp] theorem size_push (a : Array α) (v : α) : (push a v).size = a.size + 1 :=
+  List.length_concat ..
+
+theorem ext (a b : Array α)
+    (h₁ : a.size = b.size)
+    (h₂ : (i : Nat) → (hi₁ : i < a.size) → (hi₂ : i < b.size) → a[i] = b[i])
+    : a = b := by
+  let rec extAux (a b : List α)
+      (h₁ : a.length = b.length)
+      (h₂ : (i : Nat) → (hi₁ : i < a.length) → (hi₂ : i < b.length) → a.get ⟨i, hi₁⟩ = b.get ⟨i, hi₂⟩)
+      : a = b := by
+    induction a generalizing b with
+    | nil =>
+      cases b with
+      | nil       => rfl
+      | cons b bs => rw [List.length_cons] at h₁; injection h₁
+    | cons a as ih =>
+      cases b with
+      | nil => rw [List.length_cons] at h₁; injection h₁
+      | cons b bs =>
+        have hz₁ : 0 < (a::as).length := by rw [List.length_cons]; apply Nat.zero_lt_succ
+        have hz₂ : 0 < (b::bs).length := by rw [List.length_cons]; apply Nat.zero_lt_succ
+        have headEq : a = b := h₂ 0 hz₁ hz₂
+        have h₁' : as.length = bs.length := by rw [List.length_cons, List.length_cons] at h₁; injection h₁
+        have h₂' : (i : Nat) → (hi₁ : i < as.length) → (hi₂ : i < bs.length) → as.get ⟨i, hi₁⟩ = bs.get ⟨i, hi₂⟩ := by
+          intro i hi₁ hi₂
+          have hi₁' : i+1 < (a::as).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
+          have hi₂' : i+1 < (b::bs).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
+          have : (a::as).get ⟨i+1, hi₁'⟩ = (b::bs).get ⟨i+1, hi₂'⟩ := h₂ (i+1) hi₁' hi₂'
+          apply this
+        have tailEq : as = bs := ih bs h₁' h₂'
+        rw [headEq, tailEq]
+  cases a; cases b
+  apply congrArg
+  apply extAux
+  assumption
+  assumption
+
+theorem ext' {as bs : Array α} (h : as.toList = bs.toList) : as = bs := by
+  cases as; cases bs; simp at h; rw [h]
+
+@[simp] theorem toArrayAux_eq (as : List α) (acc : Array α) : (as.toArrayAux acc).toList = acc.toList ++ as := by
+  induction as generalizing acc <;> simp [*, List.toArrayAux, Array.push, List.append_assoc, List.concat_eq_append]
+
+@[simp] theorem toList_toArray (as : List α) : as.toArray.toList = as := rfl
+
+@[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]
+
+@[deprecated toList_toArray (since := "2024-09-09")] abbrev data_toArray := @toList_toArray
+
 @[deprecated Array.toList (since := "2024-09-10")] abbrev Array.data := @Array.toList
 
-@[extern "lean_mk_array"]
-def mkArray {α : Type u} (n : Nat) (v : α) : Array α where
-  toList := List.replicate n v
-
-/--
-`ofFn f` with `f : Fin n → α` returns the list whose ith element is `f i`.
-```
-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)]` -/
-  go (i : Nat) (acc : Array α) : Array α :=
-    if h : i < n then go (i+1) (acc.push (f ⟨i, h⟩)) else acc
-termination_by n - i
-decreasing_by simp_wf; decreasing_trivial_pre_omega
-
-/-- The array `#[0, 1, ..., n - 1]`. -/
-def range (n : Nat) : Array Nat :=
-  n.fold (flip Array.push) (mkEmpty n)
-
-@[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
-  List.length_replicate ..
-
-instance : EmptyCollection (Array α) := ⟨Array.empty⟩
-instance : Inhabited (Array α) where
-  default := Array.empty
-
-@[simp] def isEmpty (a : Array α) : Bool :=
-  a.size = 0
-
-def singleton (v : α) : Array α :=
-  mkArray 1 v
+/-! ### Externs -/
 
 /-- Low-level version of `size` that directly queries the C array object cached size.
     While this is not provable, `usize` always returns the exact size of the array since
@@ -65,29 +97,6 @@ def usize (a : @& Array α) : USize := a.size.toUSize
 def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
   a[i.toNat]
 
-instance : GetElem (Array α) USize α fun xs i => i.toNat < xs.size where
-  getElem xs i h := xs.uget i h
-
-def back [Inhabited α] (a : Array α) : α :=
-  a.get! (a.size - 1)
-
-def get? (a : Array α) (i : Nat) : Option α :=
-  if h : i < a.size then some a[i] else none
-
-def back? (a : Array α) : Option α :=
-  a.get? (a.size - 1)
-
--- auxiliary declaration used in the equation compiler when pattern matching array literals.
-abbrev getLit {α : Type u} {n : Nat} (a : Array α) (i : Nat) (h₁ : a.size = n) (h₂ : i < n) : α :=
-  have := h₁.symm ▸ h₂
-  a[i]
-
-@[simp] theorem size_set (a : Array α) (i : Fin a.size) (v : α) : (set a i v).size = a.size :=
-  List.length_set ..
-
-@[simp] theorem size_push (a : Array α) (v : α) : (push a v).size = a.size + 1 :=
-  List.length_concat ..
-
 /-- Low-level version of `fset` which is as fast as a C array fset.
    `Fin` values are represented as tag pointers in the Lean runtime. Thus,
    `fset` may be slightly slower than `uset`. -/
@@ -95,6 +104,19 @@ abbrev getLit {α : Type u} {n : Nat} (a : Array α) (i : Nat) (h₁ : a.size =
 def uset (a : Array α) (i : USize) (v : α) (h : i.toNat < a.size) : Array α :=
   a.set ⟨i.toNat, h⟩ v
 
+@[extern "lean_array_pop"]
+def pop (a : Array α) : Array α where
+  toList := a.toList.dropLast
+
+@[simp] theorem size_pop (a : Array α) : a.pop.size = a.size - 1 := by
+  match a with
+  | ⟨[]⟩ => rfl
+  | ⟨a::as⟩ => simp [pop, Nat.succ_sub_succ_eq_sub, size]
+
+@[extern "lean_mk_array"]
+def mkArray {α : Type u} (n : Nat) (v : α) : Array α where
+  toList := List.replicate n v
+
 /--
 Swaps two entries in an array.
 
@@ -108,6 +130,10 @@ def swap (a : Array α) (i j : @& Fin a.size) : Array α :=
   let a'  := a.set i v₂
   a'.set (size_set a i v₂ ▸ j) v₁
 
+@[simp] theorem size_swap (a : Array α) (i j : Fin a.size) : (a.swap i j).size = a.size := by
+  show ((a.set i (a.get j)).set (size_set a i _ ▸ j) (a.get i)).size = a.size
+  rw [size_set, size_set]
+
 /--
 Swaps two entries in an array, or returns the array unchanged if either index is out of bounds.
 
@@ -121,6 +147,64 @@ def swap! (a : Array α) (i j : @& Nat) : Array α :=
   else a
   else a
 
+/-! ### GetElem instance for `USize`, backed by `uget` -/
+
+instance : GetElem (Array α) USize α fun xs i => i.toNat < xs.size where
+  getElem xs i h := xs.uget i h
+
+/-! ### Definitions -/
+
+instance : EmptyCollection (Array α) := ⟨Array.empty⟩
+instance : Inhabited (Array α) where
+  default := Array.empty
+
+@[simp] def isEmpty (a : Array α) : Bool :=
+  a.size = 0
+
+@[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)
+
+@[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)
+  else
+    false
+
+instance [BEq α] : BEq (Array α) :=
+  ⟨fun a b => isEqv a b BEq.beq⟩
+
+/--
+`ofFn f` with `f : Fin n → α` returns the list whose ith element is `f i`.
+```
+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
+
+/-- The array `#[0, 1, ..., n - 1]`. -/
+def range (n : Nat) : Array Nat :=
+  n.fold (flip Array.push) (mkEmpty n)
+
+def singleton (v : α) : Array α :=
+  mkArray 1 v
+
+def back [Inhabited α] (a : Array α) : α :=
+  a.get! (a.size - 1)
+
+def get? (a : Array α) (i : Nat) : Option α :=
+  if h : i < a.size then some a[i] else none
+
+def back? (a : Array α) : Option α :=
+  a.get? (a.size - 1)
+
 @[inline] def swapAt (a : Array α) (i : Fin a.size) (v : α) : α × Array α :=
   let e := a.get i
   let a := a.set i v
@@ -134,10 +218,6 @@ def swapAt! (a : Array α) (i : Nat) (v : α) : α × Array α :=
     have : Inhabited α := ⟨v⟩
     panic! ("index " ++ toString i ++ " out of bounds")
 
-@[extern "lean_array_pop"]
-def pop (a : Array α) : Array α where
-  toList := a.toList.dropLast
-
 def shrink (a : Array α) (n : Nat) : Array α :=
   let rec loop
     | 0,   a => a
@@ -306,12 +386,12 @@ 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 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
-  termination_by as.size - i
+  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
   decreasing_by simp_wf; decreasing_trivial_pre_omega
   map 0 (mkEmpty as.size)
 
@@ -375,7 +455,8 @@ 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 loop (j : Nat) : m Bool := do
+    let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+    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
@@ -384,7 +465,6 @@ def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as :
           loop (j+1)
       else
         pure false
-      termination_by stop - j
       decreasing_by simp_wf; decreasing_trivial_pre_omega
     loop start
   if h : stop ≤ as.size then
@@ -466,16 +546,28 @@ def findRev? {α : Type} (as : Array α) (p : α → Bool) : Option α :=
 
 @[inline]
 def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
-  let rec loop (j : Nat) :=
+  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+  loop (j : Nat) :=
     if h : j < as.size then
       if p as[j] then some j else loop (j + 1)
     else none
-    termination_by as.size - j
     decreasing_by simp_wf; decreasing_trivial_pre_omega
   loop 0
 
 def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
-a.findIdx? fun a => a == v
+  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⟩;
+    if a.get idx == v then some idx
+    else indexOfAux a v (i+1)
+  else none
+decreasing_by simp_wf; decreasing_trivial_pre_omega
+
+def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
+  indexOfAux a v 0
 
 @[inline]
 def any (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool :=
@@ -491,13 +583,6 @@ def contains [BEq α] (as : Array α) (a : α) : Bool :=
 def elem [BEq α] (a : α) (as : Array α) : Bool :=
   as.contains a
 
-@[inline] def getEvenElems (as : Array α) : Array α :=
-  (·.2) <| as.foldl (init := (true, Array.empty)) fun (even, r) a =>
-    if even then
-      (false, r.push a)
-    else
-      (true, r)
-
 /-- Convert a `Array α` into an `List α`. This is O(n) in the size of the array.  -/
 -- This function is exported to C, where it is called by `Array.toList`
 -- (the projection) to implement this functionality.
@@ -510,17 +595,6 @@ def toListImpl (as : Array α) : List α :=
 def toListAppend (as : Array α) (l : List α) : List α :=
   as.foldr List.cons l
 
-instance {α : Type u} [Repr α] : Repr (Array α) where
-  reprPrec a _ :=
-    let _ : Std.ToFormat α := ⟨repr⟩
-    if a.size == 0 then
-      "#[]"
-    else
-      Std.Format.bracketFill "#[" (Std.Format.joinSep (toList a) ("," ++ Std.Format.line)) "]"
-
-instance [ToString α] : ToString (Array α) where
-  toString a := "#" ++ toString a.toList
-
 protected def append (as : Array α) (bs : Array α) : Array α :=
   bs.foldl (init := as) fun r v => r.push v
 
@@ -546,44 +620,13 @@ def concatMap (f : α → Array β) (as : Array α) : Array β :=
 def flatten (as : Array (Array α)) : Array α :=
   as.foldl (init := empty) fun r a => r ++ a
 
-end Array
-
-export Array (mkArray)
-
-syntax "#[" withoutPosition(sepBy(term, ", ")) "]" : term
-
-macro_rules
-  | `(#[ $elems,* ]) => `(List.toArray [ $elems,* ])
-
-namespace Array
-
--- TODO(Leo): cleanup
-@[specialize]
-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
-termination_by a.size - i
-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 0
-  else
-    false
-
-instance [BEq α] : BEq (Array α) :=
-  ⟨fun a b => isEqv a b BEq.beq⟩
-
 @[inline]
 def filter (p : α → Bool) (as : Array α) (start := 0) (stop := as.size) : Array α :=
   as.foldl (init := #[]) (start := start) (stop := stop) fun r a =>
     if p a then r.push a else r
 
 @[inline]
-def filterM [Monad m] (p : α → m Bool) (as : Array α) (start := 0) (stop := as.size) : m (Array α) :=
+def filterM {α : Type} [Monad m] (p : α → m Bool) (as : Array α) (start := 0) (stop := as.size) : m (Array α) :=
   as.foldlM (init := #[]) (start := start) (stop := stop) fun r a => do
     if (← p a) then return r.push a else return r
 
@@ -618,93 +661,25 @@ def partition (p : α → Bool) (as : Array α) : Array α × Array α := Id.run
       cs := cs.push a
   return (bs, cs)
 
-theorem ext (a b : Array α)
-    (h₁ : a.size = b.size)
-    (h₂ : (i : Nat) → (hi₁ : i < a.size) → (hi₂ : i < b.size) → a[i] = b[i])
-    : a = b := by
-  let rec extAux (a b : List α)
-      (h₁ : a.length = b.length)
-      (h₂ : (i : Nat) → (hi₁ : i < a.length) → (hi₂ : i < b.length) → a.get ⟨i, hi₁⟩ = b.get ⟨i, hi₂⟩)
-      : a = b := by
-    induction a generalizing b with
-    | nil =>
-      cases b with
-      | nil       => rfl
-      | cons b bs => rw [List.length_cons] at h₁; injection h₁
-    | cons a as ih =>
-      cases b with
-      | nil => rw [List.length_cons] at h₁; injection h₁
-      | cons b bs =>
-        have hz₁ : 0 < (a::as).length := by rw [List.length_cons]; apply Nat.zero_lt_succ
-        have hz₂ : 0 < (b::bs).length := by rw [List.length_cons]; apply Nat.zero_lt_succ
-        have headEq : a = b := h₂ 0 hz₁ hz₂
-        have h₁' : as.length = bs.length := by rw [List.length_cons, List.length_cons] at h₁; injection h₁
-        have h₂' : (i : Nat) → (hi₁ : i < as.length) → (hi₂ : i < bs.length) → as.get ⟨i, hi₁⟩ = bs.get ⟨i, hi₂⟩ := by
-          intro i hi₁ hi₂
-          have hi₁' : i+1 < (a::as).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
-          have hi₂' : i+1 < (b::bs).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
-          have : (a::as).get ⟨i+1, hi₁'⟩ = (b::bs).get ⟨i+1, hi₂'⟩ := h₂ (i+1) hi₁' hi₂'
-          apply this
-        have tailEq : as = bs := ih bs h₁' h₂'
-        rw [headEq, tailEq]
-  cases a; cases b
-  apply congrArg
-  apply extAux
-  assumption
-  assumption
-
-theorem extLit {n : Nat}
-    (a b : Array α)
-    (hsz₁ : a.size = n) (hsz₂ : b.size = n)
-    (h : (i : Nat) → (hi : i < n) → a.getLit i hsz₁ hi = b.getLit i hsz₂ hi) : a = b :=
-  Array.ext a b (hsz₁.trans hsz₂.symm) fun i hi₁ _ => h i (hsz₁ ▸ hi₁)
-
-end Array
-
--- CLEANUP the following code
-namespace Array
-
-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⟩;
-    if a.get idx == v then some idx
-    else indexOfAux a v (i+1)
-  else none
-termination_by a.size - i
-decreasing_by simp_wf; decreasing_trivial_pre_omega
-
-def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
-  indexOfAux a v 0
-
-@[simp] theorem size_swap (a : Array α) (i j : Fin a.size) : (a.swap i j).size = a.size := by
-  show ((a.set i (a.get j)).set (size_set a i _ ▸ j) (a.get i)).size = a.size
-  rw [size_set, size_set]
-
-@[simp] theorem size_pop (a : Array α) : a.pop.size = a.size - 1 := by
-  match a with
-  | ⟨[]⟩ => rfl
-  | ⟨a::as⟩ => simp [pop, Nat.succ_sub_succ_eq_sub, size]
-
-theorem reverse.termination {i j : Nat} (h : i < j) : j - 1 - (i + 1) < j - i := by
-  rw [Nat.sub_sub, Nat.add_comm]
-  exact Nat.lt_of_le_of_lt (Nat.pred_le _) (Nat.sub_succ_lt_self _ _ h)
-
 def reverse (as : Array α) : Array α :=
   if h : as.size ≤ 1 then
     as
   else
     loop as 0 ⟨as.size - 1, Nat.pred_lt (mt (fun h : as.size = 0 => h ▸ by decide) h)⟩
 where
+  termination {i j : Nat} (h : i < j) : j - 1 - (i + 1) < j - i := by
+    rw [Nat.sub_sub, Nat.add_comm]
+    exact Nat.lt_of_le_of_lt (Nat.pred_le _) (Nat.sub_succ_lt_self _ _ h)
   loop (as : Array α) (i : Nat) (j : Fin as.size) :=
     if h : i < j then
-      have := reverse.termination h
+      have := termination h
       let as := as.swap ⟨i, Nat.lt_trans h j.2⟩ j
       have : j-1 < as.size := by rw [size_swap]; exact Nat.lt_of_le_of_lt (Nat.pred_le _) j.2
       loop as (i+1) ⟨j-1, this⟩
     else
       as
-termination_by j - i
 
+@[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
@@ -713,11 +688,11 @@ def popWhile (p : α → Bool) (as : Array α) : Array α :=
       as
   else
     as
-termination_by as.size
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def takeWhile (p : α → Bool) (as : Array α) : Array α :=
-  let rec go (i : Nat) (r : Array α) : Array α :=
+  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+  go (i : Nat) (r : Array α) : Array α :=
     if h : i < as.size then
       let a := as.get ⟨i, h⟩
       if p a then
@@ -726,7 +701,6 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
         r
     else
       r
-    termination_by as.size - i
     decreasing_by simp_wf; decreasing_trivial_pre_omega
   go 0 #[]
 
@@ -734,6 +708,7 @@ 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,6 +719,7 @@ def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
 termination_by a.size - i.val
 decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ i.isLt
 
+-- This is required in `Lean.Data.PersistentHashMap`.
 theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
   induction a, i using Array.feraseIdx.induct with
   | @case1 a i h a' _ ih =>
@@ -767,14 +743,14 @@ 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 loop (as : Array α) (j : Fin as.size) :=
+  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+  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
       loop as ⟨j', by rw [size_swap]; exact j'.2⟩
     else
       as
-    termination_by j.1
     decreasing_by simp_wf; decreasing_trivial_pre_omega
   let j := as.size
   let as := as.push a
@@ -786,41 +762,7 @@ def insertAt! (as : Array α) (i : Nat) (a : α) : Array α :=
     insertAt as ⟨i, Nat.lt_succ_of_le h⟩ a
   else panic! "invalid index"
 
-def toListLitAux (a : Array α) (n : Nat) (hsz : a.size = n) : ∀ (i : Nat), i ≤ a.size → List α → List α
-  | 0,     _,  acc => acc
-  | (i+1), hi, acc => toListLitAux a n hsz i (Nat.le_of_succ_le hi) (a.getLit i hsz (Nat.lt_of_lt_of_eq (Nat.lt_of_lt_of_le (Nat.lt_succ_self i) hi) hsz) :: acc)
-
-def toArrayLit (a : Array α) (n : Nat) (hsz : a.size = n) : Array α :=
-  List.toArray <| toListLitAux a n hsz n (hsz ▸ Nat.le_refl _) []
-
-theorem ext' {as bs : Array α} (h : as.toList = bs.toList) : as = bs := by
-  cases as; cases bs; simp at h; rw [h]
-
-@[simp] theorem toArrayAux_eq (as : List α) (acc : Array α) : (as.toArrayAux acc).toList = acc.toList ++ as := by
-  induction as generalizing acc <;> simp [*, List.toArrayAux, Array.push, List.append_assoc, List.concat_eq_append]
-
-@[simp] theorem toList_toArray (as : List α) : as.toArray.toList = as := by
-  simp [List.toArray, Array.mkEmpty]
-
-@[deprecated toList_toArray (since := "2024-09-09")] abbrev data_toArray := @toList_toArray
-
-@[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]
-
-theorem toArrayLit_eq (as : Array α) (n : Nat) (hsz : as.size = n) : as = toArrayLit as n hsz := by
-  apply ext'
-  simp [toArrayLit, toList_toArray]
-  have hle : n ≤ as.size := hsz ▸ Nat.le_refl _
-  have hge : as.size ≤ n := hsz ▸ Nat.le_refl _
-  have := go n hle
-  rw [List.drop_eq_nil_of_le hge] at this
-  rw [this]
-where
-  getLit_eq (as : Array α) (i : Nat) (h₁ : as.size = n) (h₂ : i < n) : as.getLit i h₁ h₂ = getElem as.toList i ((id (α := as.toList.length = n) h₁) ▸ h₂) :=
-    rfl
-
-  go (i : Nat) (hi : i ≤ as.size) : toListLitAux as n hsz i hi (as.toList.drop i) = as.toList := by
-    induction i <;> simp [getLit_eq, List.get_drop_eq_drop, toListLitAux, List.drop, *]
-
+@[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]
@@ -832,7 +774,6 @@ def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : N
       false
   else
     true
-termination_by as.size - i
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 /-- Return true iff `as` is a prefix of `bs`.
@@ -843,24 +784,8 @@ def isPrefixOf [BEq α] (as bs : Array α) : Bool :=
   else
     false
 
-private def allDiffAuxAux [BEq α] (as : Array α) (a : α) : forall (i : Nat), i < as.size → Bool
-  | 0,   _ => true
-  | i+1, h =>
-    have : i < as.size := Nat.lt_trans (Nat.lt_succ_self _) h;
-    a != as[i] && allDiffAuxAux as a i this
-
-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)
-  else
-    true
-termination_by as.size - i
-decreasing_by simp_wf; decreasing_trivial_pre_omega
-
-def allDiff [BEq α] (as : Array α) : Bool :=
-  allDiffAux as 0
-
-@[specialize] def zipWithAux (f : α → β → γ) (as : Array α) (bs : Array β) (i : Nat) (cs : Array γ) : Array γ :=
+@[semireducible, specialize] -- This is otherwise irreducible because it uses well-founded recursion.
+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
@@ -870,7 +795,6 @@ def allDiff [BEq α] (as : Array α) : Bool :=
       cs
   else
     cs
-termination_by as.size - i
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 @[inline] def zipWith (as : Array α) (bs : Array β) (f : α → β → γ) : Array γ :=
@@ -886,4 +810,48 @@ def split (as : Array α) (p : α → Bool) : Array α × Array α :=
   as.foldl (init := (#[], #[])) fun (as, bs) a =>
     if p a then (as.push a, bs) else (as, bs.push a)
 
+/-! ### Auxiliary functions used in metaprogramming.
+
+We do not intend to provide verification theorems for these functions.
+-/
+
+private def allDiffAuxAux [BEq α] (as : Array α) (a : α) : forall (i : Nat), i < as.size → Bool
+  | 0,   _ => true
+  | i+1, h =>
+    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)
+  else
+    true
+decreasing_by simp_wf; decreasing_trivial_pre_omega
+
+def allDiff [BEq α] (as : Array α) : Bool :=
+  allDiffAux as 0
+
+@[inline] def getEvenElems (as : Array α) : Array α :=
+  (·.2) <| as.foldl (init := (true, Array.empty)) fun (even, r) a =>
+    if even then
+      (false, r.push a)
+    else
+      (true, r)
+
+/-! ### Repr and ToString -/
+
+instance {α : Type u} [Repr α] : Repr (Array α) where
+  reprPrec a _ :=
+    let _ : Std.ToFormat α := ⟨repr⟩
+    if a.size == 0 then
+      "#[]"
+    else
+      Std.Format.bracketFill "#[" (Std.Format.joinSep (toList a) ("," ++ Std.Format.line)) "]"
+
+instance [ToString α] : ToString (Array α) where
+  toString a := "#" ++ toString a.toList
+
 end Array
+
+export Array (mkArray)

src/Init/Data/Array/BasicAux.lean

@@ -34,7 +34,7 @@ private theorem List.of_toArrayAux_eq_toArrayAux {as bs : List α} {cs ds : Arra
 
 @[simp] theorem List.toArray_eq_toArray_eq (as bs : List α) : (as.toArray = bs.toArray) = (as = bs) := by
   apply propext; apply Iff.intro
-  · intro h; simp [toArray] at h; have := of_toArrayAux_eq_toArrayAux h rfl; exact this.1
+  · intro h; simpa [toArray] using h
   · intro h; rw [h]
 
 def Array.mapM' [Monad m] (f : α → m β) (as : Array α) : m { bs : Array β // bs.size = as.size } :=

src/Init/Data/Array/DecidableEq.lean

@@ -5,43 +5,49 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Array.Basic
+import Init.Data.BEq
 import Init.ByCases
 
 namespace Array
 
-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_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 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 α) : 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 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 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 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 isEqv_self [DecidableEq α] (a : Array α) : Array.isEqv a a (fun x y => x = y) = true := by
+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
   simp [isEqv, isEqvAux_self]
 
 instance [DecidableEq α] : DecidableEq (Array α) :=

src/Init/Data/Array/GetLit.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2018 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+
+prelude
+import Init.Data.Array.Basic
+
+namespace Array
+
+/-! ### getLit -/
+
+-- auxiliary declaration used in the equation compiler when pattern matching array literals.
+abbrev getLit {α : Type u} {n : Nat} (a : Array α) (i : Nat) (h₁ : a.size = n) (h₂ : i < n) : α :=
+  have := h₁.symm ▸ h₂
+  a[i]
+
+theorem extLit {n : Nat}
+    (a b : Array α)
+    (hsz₁ : a.size = n) (hsz₂ : b.size = n)
+    (h : (i : Nat) → (hi : i < n) → a.getLit i hsz₁ hi = b.getLit i hsz₂ hi) : a = b :=
+  Array.ext a b (hsz₁.trans hsz₂.symm) fun i hi₁ _ => h i (hsz₁ ▸ hi₁)
+
+def toListLitAux (a : Array α) (n : Nat) (hsz : a.size = n) : ∀ (i : Nat), i ≤ a.size → List α → List α
+  | 0,     _,  acc => acc
+  | (i+1), hi, acc => toListLitAux a n hsz i (Nat.le_of_succ_le hi) (a.getLit i hsz (Nat.lt_of_lt_of_eq (Nat.lt_of_lt_of_le (Nat.lt_succ_self i) hi) hsz) :: acc)
+
+def toArrayLit (a : Array α) (n : Nat) (hsz : a.size = n) : Array α :=
+  List.toArray <| toListLitAux a n hsz n (hsz ▸ Nat.le_refl _) []
+
+theorem toArrayLit_eq (as : Array α) (n : Nat) (hsz : as.size = n) : as = toArrayLit as n hsz := by
+  apply ext'
+  simp [toArrayLit, toList_toArray]
+  have hle : n ≤ as.size := hsz ▸ Nat.le_refl _
+  have hge : as.size ≤ n := hsz ▸ Nat.le_refl _
+  have := go n hle
+  rw [List.drop_eq_nil_of_le hge] at this
+  rw [this]
+where
+  getLit_eq (as : Array α) (i : Nat) (h₁ : as.size = n) (h₂ : i < n) : as.getLit i h₁ h₂ = getElem as.toList i ((id (α := as.toList.length = n) h₁) ▸ h₂) :=
+    rfl
+  go (i : Nat) (hi : i ≤ as.size) : toListLitAux as n hsz i hi (as.toList.drop i) = as.toList := by
+    induction i <;> simp [getLit_eq, List.get_drop_eq_drop, toListLitAux, List.drop, *]
+
+end Array

src/Init/Data/Array/Lemmas.lean

@@ -19,24 +19,9 @@ This file contains some theorems about `Array` and `List` needed for `Init.Data.
 
 namespace Array
 
-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 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]
+@[simp] theorem getElem_mk {xs : List α} {i : Nat} (h : i < xs.length) : (Array.mk xs)[i] = xs[i] := rfl
 
 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
@@ -46,27 +31,7 @@ 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 [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]
+  simp
 
 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]
@@ -84,6 +49,75 @@ 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 size_toArrayAux {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 := rfl
+
+@[deprecated toArray_toList (since := "2024-09-09")]
+abbrev toArray_data := @toArray_toList
+
+@[simp] theorem getElem_toArray {a : List α} {i : Nat} (h : i < a.toArray.size) :
+    a.toArray[i] = a[i]'(by simpa using h) := rfl
+
+@[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
+
+@[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl
+
+@[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 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
@@ -271,6 +305,9 @@ termination_by n - i
 
 /-- # mkArray -/
 
+@[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
+  List.length_replicate ..
+
 @[simp] theorem toList_mkArray (n : Nat) (v : α) : (mkArray n v).toList = List.replicate n v := rfl
 
 @[deprecated toList_mkArray (since := "2024-09-09")]
@@ -342,7 +379,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]; rfl
+  by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg, List.get?_eq_get, eq_comm]
 
 @[deprecated getElem?_eq_toList_get? (since := "2024-09-09")]
 abbrev getElem?_eq_data_get? := @getElem?_eq_toList_get?
@@ -495,7 +532,6 @@ abbrev size_eq_length_data := @size_eq_length_toList
   let rec go (as : Array α) (i j) : (reverse.loop as i j).size = as.size := by
     rw [reverse.loop]
     if h : i < j then
-      have := reverse.termination h
       simp [(go · (i+1) ⟨j-1, ·⟩), h]
     else simp [h]
     termination_by j - i
@@ -527,9 +563,8 @@ set_option linter.deprecated false in
       (H : ∀ k, as.toList.get? k = if i ≤ k ∧ k ≤ j then a.toList.get? k else a.toList.reverse.get? k)
       (k) : (reverse.loop as i ⟨j, hj⟩).toList.get? k = a.toList.reverse.get? k := by
     rw [reverse.loop]; dsimp; split <;> rename_i h₁
-    · have p := reverse.termination h₁
-      match j with | j+1 => ?_
-      simp only [Nat.add_sub_cancel] at p ⊢
+    · match j with | j+1 => ?_
+      simp only [Nat.add_sub_cancel]
       rw [(go · (i+1) j)]
       · rwa [Nat.add_right_comm i]
       · simp [size_swap, h₂]
@@ -608,8 +643,8 @@ theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : A
   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; rfl
-  | cons a l ih => simp [ih]; simp [map_eq_pure_bind, push]
+  | nil => simp
+  | cons a l ih => simp [ih]; simp [map_eq_pure_bind]
 
 @[deprecated mapM_eq_mapM_toList (since := "2024-09-09")]
 abbrev mapM_eq_mapM_data := @mapM_eq_mapM_toList
@@ -1113,5 +1148,4 @@ theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i :=
     · split <;> simp_all
     · split <;> simp_all
 
-
 end Array

src/Init/Data/Array/TakeDrop.lean

@@ -12,6 +12,7 @@ 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 [Array.getElem_eq_toList_getElem] using List.exists_of_set _
+  simpa only [ugetElem_eq_getElem, getElem_eq_toList_getElem, uset, toList_set] using
+    List.exists_of_set _
 
 end Array

src/Init/Data/BitVec.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Init.Data.BitVec.Basic

src/Init/Data/BitVec/Lemmas.lean

@@ -264,6 +264,8 @@ theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) :
 
 @[simp] theorem getLsbD_zero : (0#w).getLsbD i = false := by simp [getLsbD]
 
+@[simp] theorem getElem_zero (h : i < w) : (0#w)[i] = false := by simp [getElem_eq_testBit_toNat]
+
 @[simp] theorem getMsbD_zero : (0#w).getMsbD i = false := by simp [getMsbD]
 
 @[simp] theorem toNat_mod_cancel (x : BitVec n) : x.toNat % (2^n) = x.toNat :=
@@ -312,6 +314,13 @@ theorem getLsbD_ofBool (b : Bool) (i : Nat) : (ofBool b).getLsbD i = ((i = 0) &&
   · simp only [ofBool, ofNat_eq_ofNat, cond_true, getLsbD_ofNat, Bool.and_true]
     by_cases hi : i = 0 <;> simp [hi] <;> omega
 
+@[simp]
+theorem getElem_ofBool {b : Bool} {i : Nat} : (ofBool b)[0] = b := by
+  rcases b with rfl | rfl
+  · simp [ofBool]
+  · simp only [ofBool]
+    by_cases hi : i = 0 <;> simp [hi] <;> omega
+
 /-! ### msb -/
 
 @[simp] theorem msb_zero : (0#w).msb = false := by simp [BitVec.msb, getMsbD]
@@ -635,10 +644,18 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
 @[simp] theorem extractLsb_toNat (hi lo : Nat) (x : BitVec n) :
   (extractLsb hi lo x).toNat = (x.toNat >>> lo) % 2^(hi-lo+1) := rfl
 
+@[simp] theorem getElem_extractLsb' {start len : Nat} {x : BitVec n} {i : Nat} (h : i < len) :
+    (extractLsb' start len x)[i] = x.getLsbD (start+i) := by
+  simp [getElem_eq_testBit_toNat, getLsbD, h]
+
 @[simp] theorem getLsbD_extractLsb' (start len : Nat) (x : BitVec n) (i : Nat) :
     (extractLsb' start len x).getLsbD i = (i < len && x.getLsbD (start+i)) := by
   simp [getLsbD, Nat.lt_succ]
 
+@[simp] theorem getElem_extract {hi lo : Nat} {x : BitVec n} {i : Nat} (h : i < hi - lo + 1) :
+    (extractLsb hi lo x)[i] = getLsbD x (lo+i) := by
+  simp [getElem_eq_testBit_toNat, getLsbD, h]
+
 @[simp] theorem getLsbD_extract (hi lo : Nat) (x : BitVec n) (i : Nat) :
     getLsbD (extractLsb hi lo x) i = (i ≤ (hi-lo) && getLsbD x (lo+i)) := by
   simp [getLsbD, Nat.lt_succ]
@@ -710,6 +727,32 @@ 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
+
+instance : Std.IdempotentOp (α := BitVec n) (· ||| · ) where
+  idempotent _ := BitVec.or_self
+
+@[simp] theorem or_zero {x : BitVec w} : x ||| 0#w = x := by
+  ext i
+  simp
+
+instance : Std.LawfulCommIdentity (α := BitVec n) (· ||| · ) (0#n) where
+  right_id _ := BitVec.or_zero
+
+@[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) :
@@ -751,6 +794,32 @@ 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
+
+instance : Std.IdempotentOp (α := BitVec n) (· &&& · ) where
+  idempotent _ := BitVec.and_self
+
+@[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
+
+instance : Std.LawfulCommIdentity (α := BitVec n) (· &&& · ) (allOnes n) where
+  right_id _ := BitVec.and_allOnes
+
+@[simp] theorem allOnes_and {x : BitVec w} : allOnes w &&& x = x := by
+  ext i
+  simp
+
 /-! ### xor -/
 
 @[simp] theorem toNat_xor (x y : BitVec v) :
@@ -795,6 +864,21 @@ 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
+
+instance : Std.LawfulCommIdentity (α := BitVec n) (· ^^^ · ) (0#n) where
+  right_id _ := BitVec.xor_zero
+
+@[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
@@ -843,6 +927,14 @@ 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
@@ -887,6 +979,14 @@ theorem zero_shiftLeft (n : Nat) : 0#w <<< n = 0#w := by
   cases h₁ : decide (i < m) <;> cases h₂ : decide (n ≤ i) <;> cases h₃ : decide (i < n)
   all_goals { simp_all <;> omega }
 
+@[simp] theorem getElem_shiftLeft {x : BitVec m} {n : Nat} (h : i < m) :
+    (x <<< n)[i] = (!decide (i < n) && getLsbD x (i - n)) := by
+  rw [← testBit_toNat, getElem_eq_testBit_toNat]
+  simp only [toNat_shiftLeft, Nat.testBit_mod_two_pow, Nat.testBit_shiftLeft, ge_iff_le]
+  -- This step could be a case bashing tactic.
+  cases h₁ : decide (i < m) <;> cases h₂ : decide (n ≤ i) <;> cases h₃ : decide (i < n)
+  all_goals { simp_all <;> omega }
+
 theorem shiftLeft_xor_distrib (x y : BitVec w) (n : Nat) :
     (x ^^^ y) <<< n = (x <<< n) ^^^ (y <<< n) := by
   ext i
@@ -932,6 +1032,14 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
     exact Nat.mul_lt_mul_of_pos_right x.isLt (Nat.two_pow_pos _)
   · omega
 
+@[simp] theorem getElem_shiftLeftZeroExtend {x : BitVec m} {n : Nat} (h : i < m + n) :
+    (shiftLeftZeroExtend x n)[i] = ((! decide (i < n)) && getLsbD x (i - n)) := by
+  rw [shiftLeftZeroExtend_eq, getLsbD]
+  simp only [getElem_eq_testBit_toNat, getLsbD_shiftLeft, getLsbD_setWidth]
+  cases h₁ : decide (i < n) <;> cases h₂ : decide (i - n < m + n)
+    <;> simp_all [h]
+    <;> omega
+
 @[simp] theorem getLsbD_shiftLeftZeroExtend (x : BitVec m) (n : Nat) :
     getLsbD (shiftLeftZeroExtend x n) i = ((! decide (i < n)) && getLsbD x (i - n)) := by
   rw [shiftLeftZeroExtend_eq]
@@ -980,6 +1088,11 @@ theorem getLsbD_shiftLeft' {x : BitVec w₁} {y : BitVec w₂} {i : Nat} :
     (x <<< y).getLsbD i = (decide (i < w₁) && !decide (i < y.toNat) && x.getLsbD (i - y.toNat)) := by
   simp [shiftLeft_eq', getLsbD_shiftLeft]
 
+@[simp]
+theorem getElem_shiftLeft' {x : BitVec w₁} {y : BitVec w₂} {i : Nat} (h : i < w₁) :
+    (x <<< y)[i] = (!decide (i < y.toNat) && x.getLsbD (i - y.toNat)) := by
+  simp [shiftLeft_eq', getLsbD_shiftLeft]
+
 /-! ### ushiftRight -/
 
 @[simp, bv_toNat] theorem toNat_ushiftRight (x : BitVec n) (i : Nat) :
@@ -1061,7 +1174,7 @@ theorem sshiftRight_eq_of_msb_true {x : BitVec w} {s : Nat} (h : x.msb = true) :
     · rw [Nat.shiftRight_eq_div_pow]
       apply Nat.lt_of_le_of_lt (Nat.div_le_self _ _) (by omega)
 
-@[simp] theorem getLsbD_sshiftRight (x : BitVec w) (s i : Nat) :
+theorem getLsbD_sshiftRight (x : BitVec w) (s i : Nat) :
     getLsbD (x.sshiftRight s) i =
       (!decide (w ≤ i) && if s + i < w then x.getLsbD (s + i) else x.msb) := by
   rcases hmsb : x.msb with rfl | rfl
@@ -1082,6 +1195,15 @@ theorem sshiftRight_eq_of_msb_true {x : BitVec w} {s : Nat} (h : x.msb = true) :
         Nat.not_lt, decide_eq_true_eq]
       omega
 
+theorem getElem_sshiftRight {x : BitVec w} {s i : Nat} (h : i < w) :
+    (x.sshiftRight s)[i] = (if s + i < w then x.getLsbD (s + i) else x.msb) := by
+  rcases hmsb : x.msb with rfl | rfl
+  · simp only [sshiftRight_eq_of_msb_false hmsb, getElem_ushiftRight, Bool.if_false_right,
+    Bool.iff_and_self, decide_eq_true_eq]
+    intros hlsb
+    apply BitVec.lt_of_getLsbD hlsb
+  · simp [sshiftRight_eq_of_msb_true hmsb]
+
 theorem sshiftRight_xor_distrib (x y : BitVec w) (n : Nat) :
     (x ^^^ y).sshiftRight n = (x.sshiftRight n) ^^^ (y.sshiftRight n) := by
   ext i
@@ -1119,7 +1241,7 @@ theorem sshiftRight_msb_eq_msb {n : Nat} {x : BitVec w} :
 
 @[simp] theorem sshiftRight_zero {x : BitVec w} : x.sshiftRight 0 = x := by
   ext i
-  simp
+  simp [getLsbD_sshiftRight]
 
 theorem sshiftRight_add {x : BitVec w} {m n : Nat} :
     x.sshiftRight (m + n) = (x.sshiftRight m).sshiftRight n := by
@@ -1211,7 +1333,7 @@ theorem signExtend_eq_not_setWidth_not_of_msb_true {x : BitVec w} {v : Nat} (hms
     · apply Nat.le_refl
   · omega
 
-@[simp] theorem getLsbD_signExtend (x  : BitVec w) {v i : Nat} :
+theorem getLsbD_signExtend (x  : BitVec w) {v i : Nat} :
     (x.signExtend v).getLsbD i = (decide (i < v) && if i < w then x.getLsbD i else x.msb) := by
   rcases hmsb : x.msb with rfl | rfl
   · rw [signExtend_eq_not_setWidth_not_of_msb_false hmsb]
@@ -1219,6 +1341,11 @@ theorem signExtend_eq_not_setWidth_not_of_msb_true {x : BitVec w} {v : Nat} (hms
   · rw [signExtend_eq_not_setWidth_not_of_msb_true hmsb]
     by_cases (i < v) <;> by_cases (i < w) <;> simp_all <;> omega
 
+theorem getElem_signExtend {x  : BitVec w} {v i : Nat} (h : i < v) :
+    (x.signExtend v)[i] = if i < w then x.getLsbD i else x.msb := by
+  rw [←getLsbD_eq_getElem, getLsbD_signExtend]
+  simp [h]
+
 /-- Sign extending to a width smaller than the starting width is a truncation. -/
 theorem signExtend_eq_setWidth_of_lt (x : BitVec w) {v : Nat} (hv : v ≤ w):
   x.signExtend v = x.setWidth v := by
@@ -1240,13 +1367,20 @@ theorem append_def (x : BitVec v) (y : BitVec w) :
     (x ++ y).toNat = x.toNat <<< n ||| y.toNat :=
   rfl
 
-@[simp] theorem getLsbD_append {x : BitVec n} {y : BitVec m} :
+theorem getLsbD_append {x : BitVec n} {y : BitVec m} :
     getLsbD (x ++ y) i = bif i < m then getLsbD y i else getLsbD x (i - m) := by
   simp only [append_def, getLsbD_or, getLsbD_shiftLeftZeroExtend, getLsbD_setWidth']
   by_cases h : i < m
   · simp [h]
   · simp [h]; simp_all
 
+theorem getElem_append {x : BitVec n} {y : BitVec m} (h : i < n + m) :
+    (x ++ y)[i] = bif i < m then getLsbD y i else getLsbD x (i - m) := by
+  simp only [append_def, getElem_or, getElem_shiftLeftZeroExtend, getElem_setWidth']
+  by_cases h' : i < m
+  · simp [h']
+  · simp [h']; simp_all
+
 @[simp] theorem getMsbD_append {x : BitVec n} {y : BitVec m} :
     getMsbD (x ++ y) i = bif n ≤ i then getMsbD y (i - n) else getMsbD x i := by
   simp [append_def]
@@ -1290,7 +1424,7 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
 @[simp] theorem cast_append_left (h : w + v = w' + v) (x : BitVec w) (y : BitVec v) :
     cast h (x ++ y) = cast (by omega) x ++ y := by
   ext
-  simp
+  simp [getLsbD_append]
 
 theorem setWidth_append {x : BitVec w} {y : BitVec v} :
     (x ++ y).setWidth k = if h : k ≤ v then y.setWidth k else (x.setWidth (k - v) ++ y).cast (by omega) := by
@@ -1301,9 +1435,9 @@ theorem setWidth_append {x : BitVec w} {y : BitVec v} :
   · have t : i < v := by omega
     simp [t]
   · by_cases t : i < v
-    · simp [t]
+    · simp [t, getLsbD_append]
     · have t' : i - v < k - v := by omega
-      simp [t, t']
+      simp [t, t', getLsbD_append]
 
 @[simp] theorem setWidth_append_of_eq {x : BitVec v} {y : BitVec w} (h : w' = w) : setWidth (v' + w') (x ++ y) = setWidth v' x ++ setWidth w' y := by
   subst h
@@ -1331,19 +1465,19 @@ theorem setWidth_append {x : BitVec w} {y : BitVec v} :
     (x₁ ++ y₁) &&& (x₂ ++ y₂) = (x₁ &&& x₂) ++ (y₁ &&& y₂) := by
   ext i
   simp only [getLsbD_append, cond_eq_if]
-  split <;> simp [*]
+  split <;> simp [getLsbD_append, *]
 
 @[simp] theorem or_append {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} :
     (x₁ ++ y₁) ||| (x₂ ++ y₂) = (x₁ ||| x₂) ++ (y₁ ||| y₂) := by
   ext i
   simp only [getLsbD_append, cond_eq_if]
-  split <;> simp [*]
+  split <;> simp [getLsbD_append, *]
 
 @[simp] theorem xor_append {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} :
     (x₁ ++ y₁) ^^^ (x₂ ++ y₂) = (x₁ ^^^ x₂) ++ (y₁ ^^^ y₂) := by
   ext i
   simp only [getLsbD_append, cond_eq_if]
-  split <;> simp [*]
+  split <;> simp [getLsbD_append, *]
 
 theorem shiftRight_add {w : Nat} (x : BitVec w) (n m : Nat) :
     x >>> (n + m) = (x >>> n) >>> m:= by
@@ -1363,6 +1497,12 @@ theorem getLsbD_rev (x : BitVec w) (i : Fin w) :
   congr 1
   omega
 
+theorem getElem_rev {x : BitVec w} {i : Fin w}:
+    x[i.rev] = x.getMsbD i := by
+  simp [getMsbD]
+  congr 1
+  omega
+
 theorem getMsbD_rev (x : BitVec w) (i : Fin w) :
     x.getMsbD i.rev = x.getLsbD i := by
   simp only [← getLsbD_rev]
@@ -1382,7 +1522,7 @@ theorem toNat_cons' {x : BitVec w} :
     (cons a x).toNat = (a.toNat <<< w) + x.toNat := by
   simp [cons, Nat.shiftLeft_eq, Nat.mul_comm _ (2^w), Nat.mul_add_lt_is_or, x.isLt]
 
-@[simp] theorem getLsbD_cons (b : Bool) {n} (x : BitVec n) (i : Nat) :
+theorem getLsbD_cons (b : Bool) {n} (x : BitVec n) (i : Nat) :
     getLsbD (cons b x) i = if i = n then b else getLsbD x i := by
   simp only [getLsbD, toNat_cons, Nat.testBit_or]
   rw [Nat.testBit_shiftLeft]
@@ -1396,6 +1536,20 @@ theorem toNat_cons' {x : BitVec w} :
     have p2 : i - n ≠ 0 := by omega
     simp [p1, p2, Nat.testBit_bool_to_nat]
 
+theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
+    (cons b x)[i] = if i = n then b else getLsbD x i := by
+  simp only [getElem_eq_testBit_toNat, toNat_cons, Nat.testBit_or, getLsbD]
+  rw [Nat.testBit_shiftLeft]
+  rcases Nat.lt_trichotomy i n with i_lt_n | i_eq_n | n_lt_i
+  · have p1 : ¬(n ≤ i) := by omega
+    have p2 : i ≠ n := by omega
+    simp [p1, p2]
+  · simp [i_eq_n, testBit_toNat]
+    cases b <;> trivial
+  · have p1 : i ≠ n := by omega
+    have p2 : i - n ≠ 0 := by omega
+    simp [p1, p2, Nat.testBit_bool_to_nat]
+
 @[simp] theorem msb_cons : (cons a x).msb = a := by
   simp [cons, msb_cast, msb_append]
 
@@ -1416,15 +1570,19 @@ 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]
 
-theorem eq_msb_cons_setWidth (x : BitVec (w+1)) : x = (cons x.msb (x.setWidth w)) := by
+@[simp] theorem cons_msb_setWidth (x : BitVec (w+1)) : (cons x.msb (x.setWidth w)) = x := by
   ext i
-  simp
+  simp only [getLsbD_cons]
   split <;> rename_i h
   · simp [BitVec.msb, getMsbD, h]
   · by_cases h' : i < 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]
 
@@ -1461,12 +1619,27 @@ theorem getLsbD_concat (x : BitVec w) (b : Bool) (i : Nat) :
   · simp [Nat.mod_eq_of_lt b.toNat_lt]
   · simp [Nat.div_eq_of_lt b.toNat_lt, Nat.testBit_add_one]
 
+theorem getElem_concat (x : BitVec w) (b : Bool) (i : Nat) (h : i < w + 1) :
+    (concat x b)[i] = if i = 0 then b else x.getLsbD (i - 1) := by
+  simp only [concat, getElem_eq_testBit_toNat, getLsbD, toNat_append,
+    toNat_ofBool, Nat.testBit_or, Nat.shiftLeft_eq]
+  cases i
+  · simp [Nat.mod_eq_of_lt b.toNat_lt]
+  · simp [Nat.div_eq_of_lt b.toNat_lt, Nat.testBit_add_one]
+
 @[simp] theorem getLsbD_concat_zero : (concat x b).getLsbD 0 = b := by
   simp [getLsbD_concat]
 
+@[simp] theorem getElem_concat_zero : (concat x b)[0] = b := by
+  simp [getElem_concat]
+
 @[simp] theorem getLsbD_concat_succ : (concat x b).getLsbD (i + 1) = x.getLsbD i := by
   simp [getLsbD_concat]
 
+@[simp] theorem getElem_concat_succ {x : BitVec w} {i : Nat} (h : i < w) :
+    (concat x b)[i + 1] = x[i] := by
+  simp [getElem_concat, h, getLsbD_eq_getElem]
+
 @[simp] theorem not_concat (x : BitVec w) (b : Bool) : ~~~(concat x b) = concat (~~~x) !b := by
   ext i; cases i using Fin.succRecOn <;> simp [*, Nat.succ_lt_succ]
 
@@ -1664,6 +1837,15 @@ 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]
@@ -1748,6 +1930,13 @@ protected theorem umod_lt (x : BitVec n) {y : BitVec n} : 0 < y → x.umod y < y
     (ofBoolListBE bs).getLsbD i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false) := by
   simp [getLsbD_eq_getMsbD]
 
+@[simp] theorem getElem_ofBoolListBE (h : i < bs.length) :
+    (ofBoolListBE bs)[i] = bs[bs.length - 1 - i] := by
+  rw [← getLsbD_eq_getElem, getLsbD_ofBoolListBE]
+  simp only [h, decide_True, List.getD_eq_getElem?_getD, Bool.true_and]
+  rw [List.getElem?_eq_getElem (by omega)]
+  simp
+
 @[simp] theorem getLsb_ofBoolListLE : (ofBoolListLE bs).getLsbD i = bs.getD i false := by
   induction bs generalizing i <;> cases i <;> simp_all [ofBoolListLE]
 
@@ -2113,6 +2302,11 @@ theorem getLsbD_intMax (w : Nat) : (intMax w).getLsbD i = decide (i + 1 < w) :=
 
 /-! ### Non-overflow theorems -/
 
+/-- If `x.toNat * y.toNat < 2^w`, then the multiplication `(x * y)` does not overflow. -/
+theorem toNat_add_of_lt {w} {x y : BitVec w} (h : x.toNat + y.toNat < 2^w) :
+    (x + y).toNat = x.toNat + y.toNat := by
+  rw [BitVec.toNat_add, Nat.mod_eq_of_lt h]
+
 /--
 If `y ≤ x`, then the subtraction `(x - y)` does not overflow.
 Thus, `(x - y).toNat = x.toNat - y.toNat`
@@ -2126,6 +2320,88 @@ 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)]
 
+/--
+If `y > x`, then the subtraction `(x - y)` *does* overflow, and the result is the wraparound.
+Thus, `(x - y).toNat = 2^w - (y.toNat - x.toNat)`.
+-/
+theorem toNat_sub_of_lt {x y : BitVec w} (h : x < y) :
+    (x - y).toNat = 2^w - (y.toNat - x.toNat) := by
+  simp only [toNat_sub]
+  rw [Nat.mod_eq_of_lt (by bv_omega)]
+  bv_omega
+
+/-- If `x.toNat * y.toNat < 2^w`, then the multiplication `(x * y)` does not overflow.
+Thus, `(x * y).toNat = x.toNat * y.toNat`.
+-/
+theorem toNat_mul_of_lt {w} {x y : BitVec w} (h : x.toNat * y.toNat < 2^w) :
+    (x * y).toNat = x.toNat * y.toNat := by
+  rw [BitVec.toNat_mul, Nat.mod_eq_of_lt h]
+
+/-! ### 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 simlar to `Empty.elim`.
+From the empty type `Fin 0`, any desired result `α` can be derived. This is similar 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 heterogenous iterative operation that applies a
+`hIterate` is a heterogeneous 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 heterogenous and must return a value of type `P stop`,
+Because it is heterogeneous 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` satisifies a property `Q stop` by showing that the states
+`hIterate` satisfies 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 definitiions -/
+/-! ### mod definitions -/
 
 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/Attach.lean

@@ -308,6 +308,46 @@ theorem getElem_attach {xs : List α} {i : Nat} (h : i < xs.attach.length) :
     xs.attach.tail = xs.tail.attach.map (fun ⟨x, h⟩ => ⟨x, mem_of_mem_tail h⟩) := by
   cases xs <;> simp
 
+theorem foldl_pmap (l : List α) {P : α → Prop} (f : (a : α) → P a → β)
+  (H : ∀ (a : α), a ∈ l → P a) (g : γ → β → γ) (x : γ) :
+    (l.pmap f H).foldl g x = l.attach.foldl (fun acc a => g acc (f a.1 (H _ a.2))) x := by
+  rw [pmap_eq_map_attach, foldl_map]
+
+theorem foldr_pmap (l : List α) {P : α → Prop} (f : (a : α) → P a → β)
+  (H : ∀ (a : α), a ∈ l → P a) (g : β → γ → γ) (x : γ) :
+    (l.pmap f H).foldr g x = l.attach.foldr (fun a acc => g (f a.1 (H _ a.2)) acc) x := by
+  rw [pmap_eq_map_attach, foldr_map]
+
+/--
+If we fold over `l.attach` with a function that ignores the membership predicate,
+we get the same results as folding over `l` directly.
+
+This is useful when we need to use `attach` to show termination.
+
+Unfortunately this can't be applied by `simp` because of the higher order unification problem,
+and even when rewriting we need to specify the function explicitly.
+-/
+theorem foldl_attach (l : List α) (f : β → α → β) (b : β) :
+    l.attach.foldl (fun acc t => f acc t.1) b = l.foldl f b := by
+  induction l generalizing b with
+  | nil => simp
+  | cons a l ih => rw [foldl_cons, attach_cons, foldl_cons, foldl_map, ih]
+
+/--
+If we fold over `l.attach` with a function that ignores the membership predicate,
+we get the same results as folding over `l` directly.
+
+This is useful when we need to use `attach` to show termination.
+
+Unfortunately this can't be applied by `simp` because of the higher order unification problem,
+and even when rewriting we need to specify the function explicitly.
+-/
+theorem foldr_attach (l : List α) (f : α → β → β) (b : β) :
+    l.attach.foldr (fun t acc => f t.1 acc) b = l.foldr f b := by
+  induction l generalizing b with
+  | nil => simp
+  | cons a l ih => rw [foldr_cons, attach_cons, foldr_cons, foldr_map, ih]
+
 theorem attach_map {l : List α} (f : α → β) :
     (l.map f).attach = l.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem f h⟩) := by
   induction l <;> simp [*]

src/Init/Data/List/Lemmas.lean

@@ -938,6 +938,38 @@ 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 ≠ []),

src/Init/Data/List/Nat/Basic.lean

@@ -119,6 +119,53 @@ theorem minimum?_cons' {a : Nat} {l : List Nat} :
         specialize le b h
         split <;> omega
 
+theorem foldl_min
+    {α : Type _} [Min α] [Std.IdempotentOp (min : α → α → α)] [Std.Associative (min : α → α → α)]
+    {l : List α} {a : α} :
+    l.foldl (init := a) min = min a (l.minimum?.getD a) := by
+  cases l with
+  | nil => simp [Std.IdempotentOp.idempotent]
+  | cons b l =>
+    simp only [minimum?]
+    induction l generalizing a b with
+    | nil => simp
+    | cons c l ih => simp [ih, Std.Associative.assoc]
+
+theorem foldl_min_right {α β : Type _}
+    [Min β] [Std.IdempotentOp (min : β → β → β)] [Std.Associative (min : β → β → β)]
+    {l : List α} {b : β} {f : α → β} :
+    (l.foldl (init := b) fun acc a => min acc (f a)) = min b ((l.map f).minimum?.getD b) := by
+  rw [← foldl_map, foldl_min]
+
+theorem foldl_min_le {l : List Nat} {a : Nat} : l.foldl (init := a) min ≤ a := by
+  induction l generalizing a with
+  | nil => simp
+  | cons c l ih =>
+    simp only [foldl_cons]
+    exact Nat.le_trans ih (Nat.min_le_left _ _)
+
+theorem foldl_min_min_of_le {l : List Nat} {a b : Nat} (h : a ≤ b) :
+    l.foldl (init := a) min ≤ b :=
+  Nat.le_trans (foldl_min_le) h
+
+theorem minimum?_getD_le_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
+    l.minimum?.getD k ≤ a := by
+  cases l with
+  | nil => simp at h
+  | cons b l =>
+    simp [minimum?_cons]
+    simp at h
+    rcases h with (rfl | h)
+    · exact foldl_min_le
+    · induction l generalizing b with
+      | nil => simp_all
+      | cons c l ih =>
+        simp only [foldl_cons]
+        simp at h
+        rcases h with (rfl | h)
+        · exact foldl_min_min_of_le (Nat.min_le_right _ _)
+        · exact ih _ h
+
 /-! ### maximum? -/
 
 -- A specialization of `maximum?_eq_some_iff` to Nat.
@@ -152,4 +199,51 @@ theorem maximum?_cons' {a : Nat} {l : List Nat} :
         specialize le b h
         split <;> omega
 
+theorem foldl_max
+    {α : Type _} [Max α] [Std.IdempotentOp (max : α → α → α)] [Std.Associative (max : α → α → α)]
+    {l : List α} {a : α} :
+    l.foldl (init := a) max = max a (l.maximum?.getD a) := by
+  cases l with
+  | nil => simp [Std.IdempotentOp.idempotent]
+  | cons b l =>
+    simp only [maximum?]
+    induction l generalizing a b with
+    | nil => simp
+    | cons c l ih => simp [ih, Std.Associative.assoc]
+
+theorem foldl_max_right {α β : Type _}
+    [Max β] [Std.IdempotentOp (max : β → β → β)] [Std.Associative (max : β → β → β)]
+    {l : List α} {b : β} {f : α → β} :
+    (l.foldl (init := b) fun acc a => max acc (f a)) = max b ((l.map f).maximum?.getD b) := by
+  rw [← foldl_map, foldl_max]
+
+theorem le_foldl_max {l : List Nat} {a : Nat} : a ≤ l.foldl (init := a) max := by
+  induction l generalizing a with
+  | nil => simp
+  | cons c l ih =>
+    simp only [foldl_cons]
+    exact Nat.le_trans (Nat.le_max_left _ _) ih
+
+theorem le_foldl_max_of_le {l : List Nat} {a b : Nat} (h : a ≤ b) :
+    a ≤ l.foldl (init := b) max :=
+  Nat.le_trans h (le_foldl_max)
+
+theorem le_maximum?_getD_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
+    a ≤ l.maximum?.getD k := by
+  cases l with
+  | nil => simp at h
+  | cons b l =>
+    simp [maximum?_cons]
+    simp at h
+    rcases h with (rfl | h)
+    · exact le_foldl_max
+    · induction l generalizing b with
+      | nil => simp_all
+      | cons c l ih =>
+        simp only [foldl_cons]
+        simp at h
+        rcases h with (rfl | h)
+        · exact le_foldl_max_of_le (Nat.le_max_right b a)
+        · exact ih _ h
+
 end List

src/Init/Data/Nat/Bitwise.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Init.Data.Nat.Bitwise.Basic

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 divison by two.
+An induction principal that works on division 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
-  desireable if trivial `Nat.mod` calculations, namely
+  desirable 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

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Init.Omega
@@ -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 necesssary preliminary results relating order and `*` and `/`,
+It contains the necessary preliminary results relating order and `*` and `/`,
 which should probably be moved to their own file.
 -/
 

src/Init/Data/Repr.lean

@@ -51,6 +51,12 @@ 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"

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 only [getElem!_def, getElem?_def, h]
+  simp [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 only [getElem!_def, getElem?_def, h]
+  simp [getElem!_def, getElem?_def, h]
 
 namespace Fin
 

src/Init/Meta.lean

@@ -7,7 +7,7 @@ Additional goodies for writing macros
 -/
 prelude
 import Init.MetaTypes
-import Init.Data.Array.Basic
+import Init.Data.Array.GetLit
 import Init.Data.Option.BasicAux
 
 namespace Lean
@@ -862,7 +862,7 @@ partial def decodeRawStrLitAux (s : String) (i : String.Pos) (num : Nat) : Strin
 /--
 Takes the string literal lexical syntax parsed by the parser and interprets it as a string.
 This is where escape sequences are processed for example.
-The string `s` is is either a plain string literal or a raw string literal.
+The string `s` is either a plain string literal or a raw string literal.
 
 If it returns `none` then the string literal is ill-formed, which indicates a bug in the parser.
 The function is not required to return `none` if the string literal is ill-formed.

src/Init/Omega.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Init.Omega.Int

src/Init/Omega/Coeffs.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Init.Omega.IntList

src/Init/Omega/Constraint.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Init.Omega.LinearCombo

src/Init/Omega/Int.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Init.Data.Int.DivMod

src/Init/Omega/IntList.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Init.Data.List.Zip

src/Init/Omega/LinearCombo.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Init.Omega.Coeffs

src/Init/Omega/Logic.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Init.PropLemmas

src/Init/Prelude.lean

@@ -754,10 +754,11 @@ infer the proof of `Nonempty α`.
 noncomputable def Classical.ofNonempty {α : Sort u} [Nonempty α] : α :=
   Classical.choice inferInstance
 
-instance (α : Sort u) {β : Sort v} [Nonempty β] : Nonempty (α → β) :=
+instance {α : Sort u} {β : Sort v} [Nonempty β] : Nonempty (α → β) :=
   Nonempty.intro fun _ => Classical.ofNonempty
 
-instance (α : Sort u) {β : α → Sort v} [(a : α) → Nonempty (β a)] : Nonempty ((a : α) → β a) :=
+instance Pi.instNonempty {α : Sort u} {β : α → Sort v} [(a : α) → Nonempty (β a)] :
+    Nonempty ((a : α) → β a) :=
   Nonempty.intro fun _ => Classical.ofNonempty
 
 instance : Inhabited (Sort u) where
@@ -766,7 +767,8 @@ instance : Inhabited (Sort u) where
 instance (α : Sort u) {β : Sort v} [Inhabited β] : Inhabited (α → β) where
   default := fun _ => default
 
-instance (α : Sort u) {β : α → Sort v} [(a : α) → Inhabited (β a)] : Inhabited ((a : α) → β a) where
+instance Pi.instInhabited {α : Sort u} {β : α → Sort v} [(a : α) → Inhabited (β a)] :
+    Inhabited ((a : α) → β a) where
   default := fun _ => default
 
 deriving instance Inhabited for Bool
@@ -1210,7 +1212,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 satisfiying
+    It is implemented as `Int.ediv`, the unique function satisfying
     `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).
@@ -1364,7 +1366,7 @@ class Pow (α : Type u) (β : Type v) where
   /-- `a ^ b` computes `a` to the power of `b`. See `HPow`. -/
   pow : α → β → α
 
-/-- The homogenous version of `Pow` where the exponent is a `Nat`.
+/-- The homogeneous 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.
 
@@ -2065,7 +2067,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 contraints such as `?m + 1 = USize.size`. Recall that
+Lean unifier can solve constraints 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.
@@ -2568,7 +2570,9 @@ structure Array (α : Type u) where
   /--
   Converts a `List α` into an `Array α`.
 
-  At runtime, this constructor is implemented by `List.toArray` and is O(n) in the length of the
+  You can also use the synonym `List.toArray` when dot notation is convenient.
+
+  At runtime, this constructor is implemented by `List.toArrayImpl` and is O(n) in the length of the
   list.
   -/
   mk ::
@@ -2582,6 +2586,9 @@ structure Array (α : Type u) where
 attribute [extern "lean_array_to_list"] Array.toList
 attribute [extern "lean_array_mk"] Array.mk
 
+@[inherit_doc Array.mk, match_pattern]
+abbrev List.toArray (xs : List α) : Array α := .mk xs
+
 /-- Construct a new empty array with initial capacity `c`. -/
 @[extern "lean_mk_empty_array_with_capacity"]
 def Array.mkEmpty {α : Type u} (c : @& Nat) : Array α where
@@ -2709,7 +2716,10 @@ 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`. -/
+/--
+Auxiliary definition for `List.toArray`.
+`List.toArrayAux as r = r ++ as.toArray`
+-/
 @[inline_if_reduce]
 def List.toArrayAux : List α → Array α → Array α
   | nil,       r => r
@@ -2725,7 +2735,7 @@ def List.redLength : List α → Nat
 -- This function is exported to C, where it is called by `Array.mk`
 -- (the constructor) to implement this functionality.
 @[inline, match_pattern, pp_nodot, export lean_list_to_array]
-def List.toArray (as : List α) : Array α :=
+def List.toArrayImpl (as : List α) : Array α :=
   as.toArrayAux (Array.mkEmpty as.redLength)
 
 /-- The typeclass which supplies the `>>=` "bind" function. See `Monad`. -/

src/Init/Tactics.lean

@@ -456,7 +456,7 @@ syntax (name := change) "change " term (location)? : tactic
 
 /--
 * `change a with b` will change occurrences of `a` to `b` in the goal,
-  assuming `a` and `b` are are definitionally equal.
+  assuming `a` and `b` are definitionally equal.
 * `change a with b at h` similarly changes `a` to `b` in the type of hypothesis `h`.
 -/
 syntax (name := changeWith) "change " term " with " term (location)? : tactic
@@ -773,8 +773,9 @@ macro_rules
 macro "refine_lift' " e:term : tactic => `(tactic| focus (refine' no_implicit_lambda% $e; rotate_right))
 /-- Similar to `have`, but using `refine'` -/
 macro "have' " d:haveDecl : tactic => `(tactic| refine_lift' have $d:haveDecl; ?_)
-/-- Similar to `have`, but using `refine'` -/
+set_option linter.missingDocs false in -- OK, because `tactic_alt` causes inheritance of docs
 macro (priority := high) "have'" x:ident " := " p:term : tactic => `(tactic| have' $x:ident : _ := $p)
+attribute [tactic_alt tacticHave'_] «tacticHave'_:=_»
 /-- Similar to `let`, but using `refine'` -/
 macro "let' " d:letDecl : tactic => `(tactic| refine_lift' let $d:letDecl; ?_)
 
@@ -1588,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 accidentaly break this IF
+      We hardcoded `assumption` here to ensure users cannot accidentally break this IF
       they add new `macro_rules` for `get_elem_tactic_trivial`.
 
       TODO: Implement priorities for `macro_rules`.
@@ -1598,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 perfomed, and 'Panic' error message is produced if index is not 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, 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 manuall.
+definition to the user via `decreasing_by`. It is not necessary to use this tactic manually.
 -/
 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` withe `reuse` in `b`.
+to replace a `ctor` with `reuse` in `b`.
 -/
 private def tryS (x : VarId) (c : CtorInfo) (b : FnBody) : M FnBody := do
   let w ← mkFresh

src/Lean/Compiler/LCNF/JoinPoints.lean

@@ -242,7 +242,7 @@ structure ExtendState where
   /--
   A map from join point `FVarId`s to a respective map from free variables
   to `Param`s. The free variables in this map are the once that the context
-  of said join point will be extended by by passing in the respective parameter.
+  of said join point will be extended by passing in the respective parameter.
   -/
   fvarMap : Std.HashMap FVarId (Std.HashMap FVarId Param) := {}
 

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!"unknow declaration '{n}'"
+  | none => Except.error s!"unknown declaration '{n}'"
   | _    => Except.error s!"declaration is not a definition '{n}'"
 
 /--

src/Lean/Data/HashMap.lean

@@ -195,7 +195,7 @@ def insert' (m : HashMap α β) (a : α) (b : β) : HashMap α β × Bool :=
 
 /--
 Similar to `insert`, but returns `some old` if the map already had an entry `α → old`.
-If the result is `some old`, the the resulting map is equal to `m`. -/
+If the result is `some old`, the resulting map is equal to `m`. -/
 def insertIfNew (m : HashMap α β) (a : α) (b : β) : HashMap α β × Option β :=
   match m with
   | ⟨ m, hw ⟩ =>

src/Lean/Data/Json/FromToJson.lean

@@ -28,6 +28,12 @@ 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 notfication"
+    else throw "not a notification"
 
 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 "uknown trace"⟩
+  | _               => throw "unknown 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 auxillary data types produced from nested occurrences.
+  /-- Number of auxiliary 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 workes
+    -- make sure we only add a single component so that scoped works
     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

@@ -170,8 +170,9 @@ private def toBinderViews (stx : Syntax) : TermElabM (Array BinderView) := do
   else
     throwUnsupportedSyntax
 
-private def registerFailedToInferBinderTypeInfo (type : Expr) (ref : Syntax) : TermElabM Unit :=
+private def registerFailedToInferBinderTypeInfo (type : Expr) (ref : Syntax) : TermElabM Unit := do
   registerCustomErrorIfMVar type ref "failed to infer binder type"
+  registerLevelMVarErrorExprInfo type ref m!"failed to infer universe levels in binder type"
 
 def addLocalVarInfo (stx : Syntax) (fvar : Expr) : TermElabM Unit :=
   addTermInfo' (isBinder := true) stx fvar
@@ -639,7 +640,7 @@ open Lean.Elab.Term.Quotation in
   | _ => throwUnsupportedSyntax
 
 /-- If `useLetExpr` is true, then a kernel let-expression `let x : type := val; body` is created.
-   Otherwise, we create a term of the form `(fun (x : type) => body) val`
+   Otherwise, we create a term of the form `letFun val (fun (x : type) => body)`
 
    The default elaboration order is `binders`, `typeStx`, `valStx`, and `body`.
    If `elabBodyFirst == true`, then we use the order `binders`, `typeStx`, `body`, and `valStx`. -/
@@ -650,7 +651,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 synthethic opaque metavariables in `type`.
+    Resolved: we want to avoid synthetic 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.
@@ -670,7 +671,9 @@ def elabLetDeclAux (id : Syntax) (binders : Array Syntax) (typeStx : Syntax) (va
     Recall that TC resolution does **not** produce synthetic opaque metavariables.
     -/
     let type ← withSynthesize (postpone := .partial) <| elabType typeStx
-    registerCustomErrorIfMVar type typeStx "failed to infer 'let' declaration type"
+    let letMsg := if useLetExpr then "let" else "have"
+    registerCustomErrorIfMVar type typeStx m!"failed to infer '{letMsg}' declaration type"
+    registerLevelMVarErrorExprInfo type typeStx m!"failed to infer universe levels in '{letMsg}' declaration type"
     if elabBodyFirst then
       let type ← mkForallFVars fvars type
       let val  ← mkFreshExprMVar type

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 polute the environment with auxliary declarations.
+      -- we don't pollute 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,8 +532,7 @@ 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
-        trace[Elab.snapshotTree]
-          (←Language.ToSnapshotTree.toSnapshotTree snap.new.result.get |>.format)
+        liftCoreM <| Language.ToSnapshotTree.toSnapshotTree snap.new.result.get |>.trace
     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`, `proctected`, `unsafe`, `noncomputable`, doc string)-/
+/-- Elaborate declaration modifiers (i.e., attributes, `partial`, `private`, `protected`, `unsafe`, `noncomputable`, doc string)-/
 def elabModifiers (stx : Syntax) : m Modifiers := do
   let docCommentStx := stx[0]
   let attrsStx      := stx[1]

src/Lean/Elab/DeclUtil.lean

@@ -61,16 +61,17 @@ def expandDeclSig (stx : Syntax) : Syntax × Syntax :=
   (binders, typeSpec[1])
 
 /--
-  Sort the given list of `usedParams` using the following order:
-  - If it is an explicit level `allUserParams`, then use user given order.
-  - Otherwise, use lexicographical.
+Sort the given list of `usedParams` using the following order:
+- If it is an explicit level in `allUserParams`, then use user-given order.
+- All other levels come in lexicographic order after these.
 
-  Remark: `scopeParams` are the universe params introduced using the `universe` command. `allUserParams` contains
-  the universe params introduced using the `universe` command *and* the `.{...}` notation.
+Remark: `scopeParams` are the universe params introduced using the `universe` command. `allUserParams` contains
+the universe params introduced using the `universe` command *and* the `.{...}` notation.
 
-  Remark: this function return an exception if there is an `u` not in `usedParams`, that is in `allUserParams` but not in `scopeParams`.
+Remark: this function return an exception if there is an `u` not in `usedParams`, that is in `allUserParams` but not in `scopeParams`.
 
-  Remark: `explicitParams` are in reverse declaration order. That is, the head is the last declared parameter. -/
+Remark: `scopeParams` and `allUserParams` are in reverse declaration order. That is, the head is the last declared parameter.
+-/
 def sortDeclLevelParams (scopeParams : List Name) (allUserParams : List Name) (usedParams : Array Name) : Except String (List Name) :=
   match allUserParams.find? fun u => !usedParams.contains u && !scopeParams.elem u with
   | some u => throw s!"unused universe parameter '{u}'"

src/Lean/Elab/Deriving/Repr.lean

@@ -59,15 +59,17 @@ where
         let mut ctorArgs := #[]
         let mut rhs : Term := Syntax.mkStrLit (toString ctorInfo.name)
         rhs ← `(Format.text $rhs)
-        -- add `_` for inductive parameters, they are inaccessible
-        for _ in [:indVal.numParams] do
-          ctorArgs := ctorArgs.push (← `(_))
-        for i in [:ctorInfo.numFields] do
-          let x := xs[indVal.numParams + i]!
-          let a := mkIdent (← mkFreshUserName `a)
-          ctorArgs := ctorArgs.push a
-          let localDecl ← x.fvarId!.getDecl
-          if localDecl.binderInfo.isExplicit then
+        for i in [:xs.size] do
+          -- Note: some inductive parameters are explicit if they were promoted from indices,
+          -- so we process all constructor arguments in the same loop.
+          let x := xs[i]!
+          let a ← mkIdent <$> if i < indVal.numParams then pure header.argNames[i]! else mkFreshUserName `a
+          if i < indVal.numParams then
+            -- add `_` for inductive parameters, they are inaccessible
+            ctorArgs := ctorArgs.push (← `(_))
+          else
+            ctorArgs := ctorArgs.push a
+          if (← x.fvarId!.getBinderInfo).isExplicit then
             if (← inferType x).isAppOf indVal.name then
               rhs ← `($rhs ++ Format.line ++ $(mkIdent auxFunName):ident $a:ident max_prec)
             else if (← isType x <||> isProof x) then

src/Lean/Elab/Extra.lean

@@ -18,7 +18,7 @@ private def getMonadForIn (expectedType? : Option Expr) : TermElabM Expr := do
     | some expectedType =>
       match (← isTypeApp? expectedType) with
       | some (m, _) => return m
-      | none => throwError "invalid 'for_in%' notation, expected type is not of of the form `M α`{indentExpr expectedType}"
+      | none => throwError "invalid 'for_in%' notation, expected type is not of the form `M α`{indentExpr expectedType}"
 
 private def throwForInFailure (forInInstance : Expr) : TermElabM Expr :=
   throwError "failed to synthesize instance for 'for_in%' notation{indentExpr forInInstance}"
@@ -375,7 +375,7 @@ private def hasHeterogeneousDefaultInstances (f : Expr) (maxType : Expr) (lhs :
   return false
 
 /--
-  Return `true` if polymorphic function `f` has a homogenous instance of `maxType`.
+  Return `true` if polymorphic function `f` has a homogeneous 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 homogenous instance with `maxType`. See `hasHomogeneousInstance` for additional details.
+          `f` has a homogeneous instance with `maxType`. See `hasHomogeneousInstance` for additional details.
 
-          Remark: We assume `binrel%` elaborator is only used with homogenous predicates.
+          Remark: We assume `binrel%` elaborator is only used with homogeneous 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/InfoTree/Main.lean

@@ -183,7 +183,7 @@ def UserWidgetInfo.format (info : UserWidgetInfo) : Format :=
   f!"UserWidget {info.id}\n{Std.ToFormat.format <| info.props.run' {}}"
 
 def FVarAliasInfo.format (info : FVarAliasInfo) : Format :=
-  f!"FVarAlias {info.userName.eraseMacroScopes}"
+  f!"FVarAlias {info.userName.eraseMacroScopes}: {info.id.name} -> {info.baseId.name}"
 
 def FieldRedeclInfo.format (ctx : ContextInfo) (info : FieldRedeclInfo) : Format :=
   f!"FieldRedecl @ {formatStxRange ctx info.stx}"

src/Lean/Elab/Match.lean

@@ -30,7 +30,7 @@ private def mkUserNameFor (e : Expr) : TermElabM Name := do
 
 
 /--
-   Remark: if the discriminat is `Systax.missing`, we abort the elaboration of the `match`-expression.
+   Remark: if the discriminat is `Syntax.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 mistmatch, alternative {← mkHasTypeButIsExpectedMsg matchType' matchType}"
+                throwError "type mismatch, 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/MutualDef.lean

@@ -98,7 +98,7 @@ private def isMultiConstant? (views : Array DefView) : Option (List Name) :=
   else
     none
 
-private def getPendindMVarErrorMessage (views : Array DefView) : String :=
+private def getPendingMVarErrorMessage (views : Array DefView) : String :=
   match isMultiConstant? views with
   | some ids =>
     let idsStr := ", ".intercalate <| ids.map fun id => s!"`{id}`"
@@ -196,7 +196,7 @@ private def elabHeaders (views : Array DefView)
             if view.type?.isSome then
               let pendingMVarIds ← getMVars type
               discard <| logUnassignedUsingErrorInfos pendingMVarIds <|
-                getPendindMVarErrorMessage views
+                getPendingMVarErrorMessage views
             let newHeader : DefViewElabHeaderData := {
               declName, shortDeclName, type, levelNames, binderIds
               numParams := xs.size
@@ -947,45 +947,6 @@ private def levelMVarToParamHeaders (views : Array DefView) (headers : Array Def
   let newHeaders ← (process).run' 1
   newHeaders.mapM fun header => return { header with type := (← instantiateMVars header.type) }
 
-partial def checkForHiddenUnivLevels (allUserLevelNames : List Name) (preDefs : Array PreDefinition) : TermElabM Unit :=
-  unless (← MonadLog.hasErrors) do
-    -- We do not report this kind of error if the declaration already contains errors
-    let mut sTypes : CollectLevelParams.State := {}
-    let mut sValues : CollectLevelParams.State := {}
-    for preDef in preDefs do
-      sTypes  := collectLevelParams sTypes preDef.type
-      sValues := collectLevelParams sValues preDef.value
-    if sValues.params.all fun u => sTypes.params.contains u || allUserLevelNames.contains u then
-      -- If all universe level occurring in values also occur in types or explicitly provided universes, then everything is fine
-      -- and we just return
-      return ()
-    let checkPreDef (preDef : PreDefinition) : TermElabM Unit :=
-      -- Otherwise, we try to produce an error message containing the expression with the offending universe
-      let rec visitLevel (u : Level) : ReaderT Expr TermElabM Unit := do
-        match u with
-        | .succ u => visitLevel u
-        | .imax u v | .max u v => visitLevel u; visitLevel v
-        | .param n =>
-          unless sTypes.visitedLevel.contains u || allUserLevelNames.contains n do
-            let parent ← withOptions (fun o => pp.universes.set o true) do addMessageContext m!"{indentExpr (← read)}"
-            let body ← withOptions (fun o => pp.letVarTypes.setIfNotSet (pp.funBinderTypes.setIfNotSet o true) true) do addMessageContext m!"{indentExpr preDef.value}"
-            throwError "invalid occurrence of universe level '{u}' at '{preDef.declName}', it does not occur at the declaration type, nor it is explicit universe level provided by the user, occurring at expression{parent}\nat declaration body{body}"
-        | _ => pure ()
-      let rec visit (e : Expr) : ReaderT Expr (MonadCacheT ExprStructEq Unit TermElabM) Unit := do
-        checkCache { val := e : ExprStructEq } fun _ => do
-          match e with
-          | .forallE n d b c | .lam n d b c => visit d e; withLocalDecl n c d fun x => visit (b.instantiate1 x) e
-          | .letE n t v b _  => visit t e; visit v e; withLetDecl n t v fun x => visit (b.instantiate1 x) e
-          | .app ..        => e.withApp fun f args => do visit f e; args.forM fun arg => visit arg e
-          | .mdata _ b     => visit b e
-          | .proj _ _ b    => visit b e
-          | .sort u        => visitLevel u (← read)
-          | .const _ us    => us.forM (visitLevel · (← read))
-          | _              => pure ()
-      visit preDef.value preDef.value |>.run {}
-    for preDef in preDefs do
-      checkPreDef preDef
-
 def elabMutualDef (vars : Array Expr) (sc : Command.Scope) (views : Array DefView) : TermElabM Unit :=
   if isExample views then
     withoutModifyingEnv do
@@ -1021,13 +982,12 @@ where
           let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift
           for preDef in preDefs do
             trace[Elab.definition] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
-          let preDefs ← withLevelNames allUserLevelNames <| levelMVarToParamPreDecls preDefs
+          let preDefs ← withLevelNames allUserLevelNames <| levelMVarToParamTypesPreDecls preDefs
           let preDefs ← instantiateMVarsAtPreDecls preDefs
           let preDefs ← shareCommonPreDefs preDefs
           let preDefs ← fixLevelParams preDefs scopeLevelNames allUserLevelNames
           for preDef in preDefs do
             trace[Elab.definition] "after eraseAuxDiscr, {preDef.declName} : {preDef.type} :=\n{preDef.value}"
-          checkForHiddenUnivLevels allUserLevelNames preDefs
           addPreDefinitions preDefs
           processDeriving headers
       for view in views, header in headers do

src/Lean/Elab/PatternVar.lean

@@ -156,9 +156,11 @@ 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 :=
-  if h : s₁.vars.size = s₂.vars.size then
-    Array.isEqvAux s₁.vars s₂.vars h (.==.) startingAt
+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
   else
     false
 

src/Lean/Elab/PreDefinition/Basic.lean

@@ -39,14 +39,26 @@ structure PreDefinition where
 def PreDefinition.filterAttrs (preDef : PreDefinition) (p : Attribute → Bool) : PreDefinition :=
   { preDef with modifiers := preDef.modifiers.filterAttrs p }
 
+/--
+Applies `Lean.instantiateMVars` to the types of values of each predefinition.
+-/
 def instantiateMVarsAtPreDecls (preDefs : Array PreDefinition) : TermElabM (Array PreDefinition) :=
   preDefs.mapM fun preDef => do
     pure { preDef with type := (← instantiateMVars preDef.type), value := (← instantiateMVars preDef.value) }
 
-def levelMVarToParamPreDecls (preDefs : Array PreDefinition) : TermElabM (Array PreDefinition) :=
+/--
+Applies `Lean.Elab.Term.levelMVarToParam` to the types of each predefinition.
+-/
+def levelMVarToParamTypesPreDecls (preDefs : Array PreDefinition) : TermElabM (Array PreDefinition) :=
   preDefs.mapM fun preDef => do
-    pure { preDef with type := (← levelMVarToParam preDef.type), value := (← levelMVarToParam preDef.value) }
+    pure { preDef with type := (← levelMVarToParam preDef.type) }
 
+/--
+Collects all the level parameters in sorted order from the types and values of each predefinition.
+Throws an "unused universe parameter" error if there is an unused `.{...}` parameter.
+
+See `Lean.collectLevelParams`.
+-/
 private def getLevelParamsPreDecls (preDefs : Array PreDefinition) (scopeLevelNames allUserLevelNames : List Name) : TermElabM (List Name) := do
   let mut s : CollectLevelParams.State := {}
   for preDef in preDefs do

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 altenative{indentExpr eqnType}"
+        let some (_, Expr.fvar fvarId, rhs) ← matchEq? (← inferType y) | throwError "unexpected hypothesis in alternative{indentExpr eqnType}"
         eliminated := eliminated.insert fvarId
         type := type.replaceFVarId fvarId rhs
       else if eliminated.contains y.fvarId! then

src/Lean/Elab/PreDefinition/Main.lean

@@ -53,6 +53,64 @@ private def getMVarsAtPreDef (preDef : PreDefinition) : MetaM (Array MVarId) :=
   let (_, s) ← (collectMVarsAtPreDef preDef).run {}
   pure s.result
 
+/--
+Set any lingering level mvars to `.zero`, for error recovery.
+-/
+private def setLevelMVarsAtPreDef (preDef : PreDefinition) : PreDefinition :=
+  if preDef.value.hasLevelMVar then
+    let value' :=
+      preDef.value.replaceLevel fun l =>
+        match l with
+        | .mvar _ => levelZero
+        | _       => none
+    { preDef with value := value' }
+  else
+    preDef
+
+private partial def ensureNoUnassignedLevelMVarsAtPreDef (preDef : PreDefinition) : TermElabM PreDefinition := do
+  if !preDef.value.hasLevelMVar then
+    return preDef
+  else
+    let pendingLevelMVars := (collectLevelMVars {} (← instantiateMVars preDef.value)).result
+    if (← logUnassignedLevelMVarsUsingErrorInfos pendingLevelMVars) then
+      return setLevelMVarsAtPreDef preDef
+    else if !(← MonadLog.hasErrors) then
+      -- This is a fallback in case we don't have an error info available for the universe level metavariables.
+      -- We try to produce an error message containing an expression with one of the universe level metavariables.
+      let rec visitLevel (u : Level) (e : Expr) : TermElabM Unit := do
+        if u.hasMVar then
+          let e' ← exposeLevelMVars e
+          throwError "\
+            declaration '{preDef.declName}' contains universe level metavariables at the expression\
+            {indentExpr e'}\n\
+            in the declaration body{indentExpr <| ← exposeLevelMVars preDef.value}"
+      let withExpr (e : Expr) (m : ReaderT Expr (MonadCacheT ExprStructEq Unit TermElabM) Unit) :=
+        withReader (fun _ => e) m
+      let rec visit (e : Expr) (head := false) : ReaderT Expr (MonadCacheT ExprStructEq Unit TermElabM) Unit := do
+        if e.hasLevelMVar then
+          checkCache { val := e : ExprStructEq } fun _ => do
+            match e with
+            | .forallE n d b c | .lam n d b c => withExpr e do visit d; withLocalDecl n c d fun x => visit (b.instantiate1 x)
+            | .letE n t v b _ => withExpr e do visit t; visit v; withLetDecl n t v fun x => visit (b.instantiate1 x)
+            | .mdata _ b     => withExpr e do visit b
+            | .proj _ _ b    => withExpr e do visit b
+            | .sort u        => visitLevel u (← read)
+            | .const _ us    => (if head then id else withExpr e) <| us.forM (visitLevel · (← read))
+            | .app ..        => withExpr e do
+                                  if let some (args, n, t, v, b) := e.letFunAppArgs? then
+                                    visit t; visit v; withLocalDeclD n t fun x => visit (b.instantiate1 x); args.forM visit
+                                  else
+                                    e.withApp fun f args => do visit f true; args.forM visit
+            | _              => pure ()
+      try
+        visit preDef.value |>.run preDef.value |>.run {}
+      catch e =>
+        logException e
+        return setLevelMVarsAtPreDef preDef
+      throwAbortCommand
+    else
+      return setLevelMVarsAtPreDef preDef
+
 private def ensureNoUnassignedMVarsAtPreDef (preDef : PreDefinition) : TermElabM PreDefinition := do
   let pendingMVarIds ← getMVarsAtPreDef preDef
   if (← logUnassignedUsingErrorInfos pendingMVarIds) then
@@ -62,7 +120,7 @@ private def ensureNoUnassignedMVarsAtPreDef (preDef : PreDefinition) : TermElabM
     else
       throwAbortCommand
   else
-    return preDef
+    ensureNoUnassignedLevelMVarsAtPreDef preDef
 
 /--
   Letrec declarations produce terms of the form `(fun .. => ..) d` where `d` is a (partial) application of an auxiliary declaration for a letrec declaration.
@@ -104,7 +162,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` shold not have a `decreasing_by` (else log error)
+* A `structural` should not have a `decreasing_by` (else log error)
 
 -/
 def checkTerminationByHints (preDefs : Array PreDefinition) : CoreM Unit := do

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

@@ -269,7 +269,7 @@ def inferBRecOnFTypes (recArgInfos : Array RecArgInfo) (positions : Positions)
   let brecOnType ← inferType brecOn
   -- Skip the indices and major argument
   let packedFTypes ← forallBoundedTelescope brecOnType (some (recArgInfo.indicesPos.size + 1)) fun _ brecOnType =>
-    -- And return the types of of the next arguments
+    -- And return the types of the next arguments
     arrowDomainsN numTypeFormers brecOnType
 
   let mut FTypes := Array.mkArray positions.numIndices (Expr.sort 0)

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 explictly asked to use a certain argument, so throw errors eagerly
+      -- User explicitly 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 auxillary type former of a nested inductive?
+    -- Can this argument be understood as the auxiliary 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 fuction operates on a group as
+One purpose of this abstraction is to make it clear when a function 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 expessions to improve the effectiveness of `elimRecursion`.
+Preprocesses the expressions 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 auxillary data type due to nested recursion
+  If `< indAll.all`, a normal data type, else an auxiliary 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 auxillary ones.
+Name of the recursive data type. Assumes that it is not one of the auxiliary 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 syntatically (it may appear in the `Expr`, so do not just use
+      -- any variable not mentioned syntactically (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 folows:
+  `TerminationHints.rememberExtraParams` and used as follows:
 
   * 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 \
-               intead of cleaning it up with the `clean_wf` tactic. Can be enabled for debugging \
+               instead 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 occurences of Wf.fix to fold on the
+            -- At some point in the past, we looked for occurrences 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 nubmer of measures tried.
+the number 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 optimiziation is to look at each argument of each recursive call
+1. The crucial optimization 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 variabe names in the outermost lambdas.
+Given a predefinition, return the variable 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 meausures we want to try.
+Enumerate all measures 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 expessions to improve the effectiveness of `wfRecursion`.
+Preprocesses the expressions to improve the effectiveness of `wfRecursion`.
 
 * Floats out the RecApp markers.
   Example:

src/Lean/Elab/Quotation.lean

@@ -605,7 +605,7 @@ private partial def hasNoErrorIfUnused : Syntax → Bool
 
 /--
 Given `rhss` the right-hand-sides of a `match`-syntax notation,
-We tag them with with fresh identifiers `alt_idx`. We use them to detect whether an alternative
+We tag them with fresh identifiers `alt_idx`. We use them to detect whether an alternative
 has been used or not.
 The result is a triple `(altIdxMap, ignoreIfUnused, rhssNew)` where
 - `altIdxMap` is a mapping from the `alt_idx` identifiers to right-hand-side indices.

src/Lean/Elab/RecAppSyntax.lean

@@ -29,7 +29,7 @@ def getRecAppSyntax? (e : Expr) : Option Syntax :=
   | _                => none
 
 /--
-Checks if the `MData` is for a recursive applciation.
+Checks if the `MData` is for a recursive application.
 -/
 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, unexpect type{indentExpr resultType}"
+          unless resultType.isForall do throwError "failed to build coercion to parent structure, unexpected 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 `Expection.postpone`.
+  Try to elaborate `stx` that was postponed by an elaboration method using `Exception.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 homogenous default instance for `HSub`.
+  When we did not use a backtracking search here, then the homogeneous 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 synthethic opaque, and can be assigned by `isDefEq`.
+  Motivation: this kind of metavariable are not synthetic opaque, and can be assigned by `isDefEq`.
   Unviverse constraints can also be postponed.
   -/
   | «partial»
@@ -512,7 +512,7 @@ private partial def withSynthesizeLightImp (k : TermElabM α) : TermElabM α :=
   finally
     modify fun s => { s with pendingMVars := s.pendingMVars ++ pendingMVarsSaved }
 
-/-- Similar to `withSynthesize`, but uses `postpone := .true`, does not use use `synthesizeUsingDefault` -/
+/-- Similar to `withSynthesize`, but uses `postpone := .true`, does not use `synthesizeUsingDefault` -/
 @[inline] def withSynthesizeLight [MonadFunctorT TermElabM m] (k : m α) : m α :=
   monadMap (m := TermElabM) (withSynthesizeLightImp ·) k
 

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 mutliple ways to write the primitive (e.g. with TC based notation and without) you
+   If there are multiple 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 emtpy string they will use that binary.\n
+     1. If this is set to something besides the empty 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 ⟨proof, ""⟩
+      return .ok ⟨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 Expr) :
+    (aigSize : Nat) (atomsAssignment : Std.HashMap Nat (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
+    let atomExpr := atomsAssignment.get! bitVecVar |>.snd
     finalMap := finalMap.push (atomExpr, ⟨BitVec.ofNat currentBit value⟩)
   return finalMap
 
@@ -79,18 +79,26 @@ 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 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
+abbrev UnsatProver := ReflectionResult → Std.HashMap Nat (Nat × Expr) →
+    MetaM (Except CounterExample UnsatProver.Result)
 
 /--
 The result of a spurious counter example diagnosis.
@@ -99,20 +107,19 @@ structure Diagnosis where
   uninterpretedSymbols : Std.HashSet Expr := {}
   unusedRelevantHypotheses : Std.HashSet FVarId := {}
 
-abbrev DiagnosisM : Type → Type := ReaderT DiagnosisInput <| StateRefT Diagnosis MetaM
+abbrev DiagnosisM : Type → Type := ReaderT CounterExample <| StateRefT Diagnosis MetaM
 
 namespace DiagnosisM
 
-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 {}
+def run (x : DiagnosisM Unit) (counterExample : CounterExample) : MetaM Diagnosis := do
+  let (_, issues) ← ReaderT.run x counterExample |>.run {}
   return issues
 
 def unusedHyps : DiagnosisM (Std.HashSet FVarId) := do
   return (← read).unusedHypotheses
 
-def atomsAssignment : DiagnosisM (Std.HashMap Nat Expr) := do
-  return (← read).atomsAssignment
+def equations : DiagnosisM (Array (Expr × BVExpr.PackedBitVec)) := do
+  return (← read).equations
 
 def addUninterpretedSymbol (e : Expr) : DiagnosisM Unit :=
   modify fun s => { s with uninterpretedSymbols := s.uninterpretedSymbols.insert e }
@@ -131,7 +138,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 ← atomsAssignment do
+  for (expr, _) in ← equations do
     match_expr expr with
     | BitVec.ofBool x =>
       match x with
@@ -157,9 +164,8 @@ def unusedRelevantHypothesesExplainer (d : Diagnosis) : Option MessageData := do
 def explainers : List (Diagnosis → Option MessageData) :=
   [uninterpretedExplainer, unusedRelevantHypothesesExplainer]
 
-def explainCounterExampleQuality (unusedHypotheses : Std.HashSet FVarId)
-    (atomsAssignment : Std.HashMap Nat Expr) : MetaM MessageData := do
-  let diagnosis ← DiagnosisM.run DiagnosisM.diagnose unusedHypotheses atomsAssignment
+def explainCounterExampleQuality (counterExample : CounterExample) : MetaM MessageData := do
+  let diagnosis ← DiagnosisM.run DiagnosisM.diagnose counterExample
   let folder acc explainer := if let some m := explainer diagnosis then acc.push m else acc
   let explanations := explainers.foldl (init := #[]) folder
 
@@ -172,8 +178,8 @@ def explainCounterExampleQuality (unusedHypotheses : Std.HashSet FVarId)
     return err
 
 def lratBitblaster (cfg : TacticContext) (reflectionResult : ReflectionResult)
-    (atomsAssignment : Std.HashMap Nat Expr) :
-    MetaM UnsatProver.Result := do
+    (atomsAssignment : Std.HashMap Nat (Nat × Expr)) :
+    MetaM (Except CounterExample UnsatProver.Result) := do
   let bvExpr := reflectionResult.bvExpr
   let entry ←
     withTraceNode `bv (fun _ => return "Bitblasting BVLogicalExpr to AIG") do
@@ -201,13 +207,10 @@ def lratBitblaster (cfg : TacticContext) (reflectionResult : ReflectionResult)
   match res with
   | .ok cert =>
     let proof ← cert.toReflectionProof cfg bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true
-    return ⟨proof, cert⟩
+    return .ok ⟨proof, cert⟩
   | .error assignment =>
-    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
+    let equations := reconstructCounterExample map assignment aigSize atomsAssignment
+    return .error { unusedHypotheses := reflectionResult.unusedHypotheses, equations }
 
 
 def reflectBV (g : MVarId) : M ReflectionResult := g.withContext do
@@ -219,51 +222,80 @@ def reflectBV (g : MVarId) : M ReflectionResult := g.withContext do
       sats := sats.push reflected
     else
       unusedHypotheses := unusedHypotheses.insert hyp
-  if sats.size = 0 then
+  if h : 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
-  let sat := sats.foldl (init := SatAtBVLogical.trivial) SatAtBVLogical.and
-  return {
-    bvExpr := sat.bvExpr,
-    proveFalse := sat.proveFalse,
-    unusedHypotheses := unusedHypotheses
-  }
+  else
+    let sat := sats[1:].foldl (init := sats[0]) SatAtBVLogical.and
+    return {
+      bvExpr := sat.bvExpr,
+      proveFalse := sat.proveFalse,
+      unusedHypotheses := unusedHypotheses
+    }
 
 
 def closeWithBVReflection (g : MVarId) (unsatProver : UnsatProver) :
-    MetaM LratCert := M.run do
+    MetaM (Except CounterExample 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, _, ident) => (ident, expr))
+    let atomsPairs := (← getThe State).atoms.toList.map (fun (expr, ⟨width, ident⟩) => (ident, (width, expr)))
     let atomsAssignment := Std.HashMap.ofList atomsPairs
-    let ⟨bvExprUnsat, cert⟩ ← unsatProver reflectionResult atomsAssignment
-    let proveFalse ← reflectionResult.proveFalse bvExprUnsat
-    g.assign proveFalse
-    return cert
+    match ← unsatProver reflectionResult atomsAssignment with
+    | .ok ⟨bvExprUnsat, cert⟩ =>
+      let proveFalse ← reflectionResult.proveFalse bvExprUnsat
+      g.assign proveFalse
+      return .ok cert
+    | .error counterExample => return .error counterExample
 
-def bvUnsat (g : MVarId) (cfg : TacticContext) : MetaM LratCert := M.run do
+def bvUnsat (g : MVarId) (cfg : TacticContext) : MetaM (Except CounterExample 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
 
-def bvDecide (g : MVarId) (cfg : TacticContext) : MetaM Result := do
+/--
+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 ⟨simpTrace, none⟩
-  let lratCert ← bvUnsat g cfg
-  return ⟨simpTrace, some lratCert⟩
+  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
 
 @[builtin_tactic Lean.Parser.Tactic.bvDecide]
 def evalBvTrace : Tactic := fun

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

@@ -61,14 +61,6 @@ 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,10 +141,11 @@ 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 _ cnfPath => do
+  IO.FS.withTempFile fun cnfHandle cnfPath => do
     withTraceNode `sat (fun _ => return "Serializing SAT problem to DIMACS file") do
       -- lazyPure to prevent compiler lifting
-      IO.FS.writeFile cnfPath (← IO.lazyPure (fun _ => cnf.dimacs))
+      cnfHandle.putStr  (← IO.lazyPure (fun _ => cnf.dimacs))
+      cnfHandle.flush
 
     let res ←
       withTraceNode `sat (fun _ => return "Running SAT solver") do

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

@@ -27,18 +27,6 @@ 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
@@ -65,6 +53,7 @@ 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,6 +49,9 @@ 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,6 +90,7 @@ 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), thes are kept as goals.
+-- by `congr` (e.g. dependent instances), these 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/FalseOrByContra.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Lean.Elab.Tactic.Basic

src/Lean/Elab/Tactic/LibrarySearch.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2021-2024 Gabriel Ebner and Lean FRO. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Joe Hendrix, Scott Morrison
+Authors: Gabriel Ebner, Joe Hendrix, Kim Morrison
 -/
 prelude
 import Lean.Meta.Tactic.LibrarySearch

src/Lean/Elab/Tactic/Omega.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Lean.Elab.Tactic.Omega.Frontend
@@ -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 contraints
+* If `x % m` appears, similarly, introduce the same new constraints
   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