feat: simprocs for String and Char <, <=, >, >=

Fixes two output bugs with cloud releases: (1) the fetch as part of an
`extraDep` was not properly isolated in a job, and (2) the release job
would be shown even if the release had already been successfully
fetched.

Also includes some related touchups, including the addition of show all
jobs on `-v` which helps with debugging job counts.

.github/ISSUE_TEMPLATE/bug_report.md

@@ -9,9 +9,15 @@ assignees: ''
 
 ### Prerequisites
 
-* [ ] Put an X between the brackets on this line if you have done all of the following:
-    * Check that your issue is not already [filed](https://github.com/leanprover/lean4/issues).
-    * Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.
+Please put an X between the brackets as you perform the following steps:
+
+* [ ] Check that your issue is not already filed:
+      https://github.com/leanprover/lean4/issues
+* [ ] Reduce the issue to a minimal, self-contained, reproducible test case.
+      Avoid dependencies to Mathlib or Batteries.
+* [ ] Test your test case against the latest nightly release, for example on
+      https://live.lean-lang.org/#project=lean-nightly
+      (You can also use the settings there to switch to “Lean nightly”)
 
 ### Description
 
@@ -33,8 +39,8 @@ assignees: ''
 
 ### Versions
 
-[Output of `#eval Lean.versionString` or of `lean --version` in the folder that the issue occured in]
-[OS version]
+[Output of `#eval Lean.versionString`]
+[OS version, if not using live.lean-lang.org.]
 
 ### Additional Information
 

.github/workflows/check-stage0.yml

@@ -0,0 +1,57 @@
+name: Check for stage0 changes
+
+on:
+  merge_group:
+  pull_request:
+
+jobs:
+  check-stage0-on-queue:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v4
+      with:
+        ref: ${{ github.event.pull_request.head.sha }}
+        filter: blob:none
+        fetch-depth: 0
+
+    - name: Find base commit
+      if: github.event_name == 'pull_request'
+      run: echo "BASE=$(git merge-base origin/${{ github.base_ref }} HEAD)" >> "$GITHUB_ENV"
+
+    - name: Identify stage0 changes
+      run: |
+        git diff "${BASE:-HEAD^}..HEAD" --name-only -- stage0 |
+          grep -v -x -F $'stage0/src/stdlib_flags.h\nstage0/src/lean.mk.in' \
+          > "$RUNNER_TEMP/stage0" || true
+        if test -s "$RUNNER_TEMP/stage0"
+        then
+          echo "CHANGES=yes" >> "$GITHUB_ENV"
+        else
+          echo "CHANGES=no" >> "$GITHUB_ENV"
+        fi
+      shell: bash
+
+    - if: github.event_name == 'pull_request'
+      name: Set label
+      uses: actions/github-script@v7
+      with:
+        script: |
+          const { owner, repo, number: issue_number  } = context.issue;
+          if (process.env.CHANGES == 'yes') {
+            await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['changes-stage0'] }).catch(() => {});
+          } else {
+            await github.rest.issues.removeLabel({ owner, repo, issue_number, name: 'changes-stage0' }).catch(() => {});
+          }
+
+    - if: env.CHANGES == 'yes'
+      name: Report changes
+      run: |
+        echo "Found changes to stage0/, please do not merge using the merge queue." | tee "$GITHUB_STEP_SUMMARY"
+        # shellcheck disable=SC2129
+        echo '```'                  >> "$GITHUB_STEP_SUMMARY"
+        cat  "$RUNNER_TEMP/stage0"  >> "$GITHUB_STEP_SUMMARY"
+        echo '```'                  >> "$GITHUB_STEP_SUMMARY"
+
+    - if: github.event_name == 'merge_group' && env.CHANGES == 'yes'
+      name: Fail when on the merge queue
+      run: exit 1

.github/workflows/ci.yml

@@ -6,7 +6,6 @@ on:
     tags:
       - '*'
   pull_request:
-    types: [opened, synchronize, reopened, labeled]
   merge_group:
   schedule:
     - cron: '0 7 * * *'  # 8AM CET/11PM PT
@@ -41,12 +40,18 @@ jobs:
     steps:
       - name: Run quick CI?
         id: set-quick
-        env:
-          quick: ${{
-            github.event_name == 'pull_request' && !contains( github.event.pull_request.labels.*.name, 'full-ci')
-           }}
+        # We do not use github.event.pull_request.labels.*.name here because
+        # re-running a run does not update that list, and we do want to be able to
+        # rerun the workflow run after settings the `full-ci` label.
         run: |
-          echo "quick=${{env.quick}}" >> "$GITHUB_OUTPUT"
+          if [ "${{ github.event_name }}" == 'pull_request' ]
+          then
+            echo "quick=$(gh api repos/${{ github.repository_owner }}/${{ github.event.repository.name }}/pulls/${{ github.event.pull_request.number }} --jq '.labels | any(.name == "full-ci") | not')" >> "$GITHUB_OUTPUT"
+          else
+            echo "quick=false" >> "$GITHUB_OUTPUT"
+          fi
+        env:
+          GH_TOKEN: ${{ github.token }}
 
       - name: Configure build matrix
         id: set-matrix
@@ -54,7 +59,10 @@ jobs:
         with:
           script: |
             const quick = ${{ steps.set-quick.outputs.quick }};
-            console.log(`quick: ${quick}`)
+            console.log(`quick: ${quick}`);
+            // use large runners outside PRs where available (original repo)
+            // disabled for now as this mostly just speeds up the test suite which is not a bottleneck
+            // let large = ${{ github.event_name != 'pull_request' && github.repository == 'leanprover/lean4' }} ? "-large" : "";
             let matrix = [
               {
                 // portable release build: use channel with older glibc (2.27)
@@ -110,7 +118,7 @@ jobs:
               },*/
               {
                 "name": "macOS",
-                "os": "macos-latest",
+                "os": "macos-13",
                 "release": true,
                 "quick": false,
                 "shell": "bash -euxo pipefail {0}",
@@ -121,7 +129,7 @@ jobs:
               },
               {
                 "name": "macOS aarch64",
-                "os": "macos-latest",
+                "os": "macos-13",
                 "release": true,
                 "quick": false,
                 "cross": true,
@@ -277,18 +285,18 @@ jobs:
         uses: cachix/install-nix-action@v18
         with:
           install_url: https://releases.nixos.org/nix/nix-2.12.0/install
-        if: matrix.os == 'ubuntu-latest' && !matrix.cmultilib
+        if: runner.os == 'Linux' && !matrix.cmultilib
       - name: Install MSYS2
         uses: msys2/setup-msys2@v2
         with:
           msystem: clang64
           # `:p` means prefix with appropriate msystem prefix
           pacboy: "make python cmake:p clang:p ccache:p gmp:p git zip unzip diffutils binutils tree zstd:p tar"
-        if: matrix.os == 'windows-2022'
+        if: runner.os == 'Windows'
       - name: Install Brew Packages
         run: |
           brew install ccache tree zstd coreutils gmp
-        if: matrix.os == 'macos-latest'
+        if: runner.os == 'macOS'
       - name: Setup emsdk
         uses: mymindstorm/setup-emsdk@v12
         with:
@@ -312,13 +320,13 @@ jobs:
         run: |
           # open nix-shell once for initial setup
           true
-        if: matrix.os == 'ubuntu-latest'
+        if: runner.os == 'Linux'
       - name: Set up core dumps
         run: |
           mkdir -p $PWD/coredumps
           # store in current directory, for easy uploading together with binary
           echo $PWD/coredumps/%e.%p.%t | sudo tee /proc/sys/kernel/core_pattern
-        if: matrix.os == 'ubuntu-latest'
+        if: runner.os == 'Linux'
       - name: Build
         run: |
           mkdir build
@@ -423,7 +431,7 @@ jobs:
       - name: CCache stats
         run: ccache -s
       - name: Show stacktrace for coredumps
-        if: ${{ failure() && matrix.os == 'ubuntu-latest' }}
+        if: ${{ failure() && runner.os == 'Linux' }}
         run: |
           for c in coredumps/*; do
             progbin="$(file $c | sed "s/.*execfn: '\([^']*\)'.*/\1/")"
@@ -433,7 +441,7 @@ jobs:
       # shared libs
       #- name: Upload coredumps
       #  uses: actions/upload-artifact@v3
-      #  if: ${{ failure() && matrix.os == 'ubuntu-latest' }}
+      #  if: ${{ failure() && runner.os == 'Linux' }}
       #  with:
       #    name: coredumps-${{ matrix.name }}
       #    path: |

.github/workflows/nix-ci.yml

@@ -6,7 +6,6 @@ on:
     tags:
       - '*'
   pull_request:
-    types: [opened, synchronize, reopened, labeled]
   merge_group:
 
 concurrency:

.github/workflows/pr-release.yml

@@ -126,11 +126,11 @@ jobs:
           if [ "$NIGHTLY_SHA" = "$MERGE_BASE_SHA" ]; then
             echo "The merge base of this PR coincides with the nightly release"
 
-            STD_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover/std4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
+            BATTERIES_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/batteries.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
             MATHLIB_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/mathlib4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
 
-            if [[ -n "$STD_REMOTE_TAGS" ]]; then
-              echo "... and Std has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
+            if [[ -n "$BATTERIES_REMOTE_TAGS" ]]; then
+              echo "... and Batteries has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
               MESSAGE=""
 
               if [[ -n "$MATHLIB_REMOTE_TAGS" ]]; then
@@ -140,8 +140,8 @@ jobs:
                 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."
               fi
             else
-              echo "... but Std does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
-              MESSAGE="- ❗ Std 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\`, Std CI should run now."
+              echo "... but Batteries does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
+              MESSAGE="- ❗ Batteries 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\`, Batteries CI should run now."
             fi
 
           else
@@ -151,7 +151,7 @@ jobs:
 
             git -C lean4.git fetch origin nightly-with-mathlib 
             NIGHTLY_WITH_MATHLIB_SHA="$(git -C lean4.git rev-parse "origin/nightly-with-mathlib")"
-            MESSAGE="- ❗ Std/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\`."
+            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
 
           if [[ -n "$MESSAGE" ]]; then
@@ -223,27 +223,27 @@ jobs:
               description: description,
             });
 
-      # We next automatically create a Std branch using this toolchain.
-      # Std doesn't itself have a mechanism to report results of CI from this branch back to Lean
-      # Instead this is taken care of by Mathlib CI, which will fail if Std fails.
+      # We next automatically create a Batteries branch using this toolchain.
+      # Batteries doesn't itself have a mechanism to report results of CI from this branch back to Lean
+      # Instead this is taken care of by Mathlib CI, which will fail if Batteries fails.
       - name: Cleanup workspace
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
         run: |
           sudo rm -rf ./*
 
-      # Checkout the Std repository with all branches
-      - name: Checkout Std repository
+      # Checkout the Batteries repository with all branches
+      - name: Checkout Batteries repository
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
         uses: actions/checkout@v3
         with:
-          repository: leanprover/std4
+          repository: leanprover-community/batteries
           token: ${{ secrets.MATHLIB4_BOT }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
 
       - name: Check if tag exists
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        id: check_std_tag
+        id: check_batteries_tag
         run: |
           git config user.name "leanprover-community-mathlib4-bot"
           git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
@@ -251,7 +251,7 @@ jobs:
           if git ls-remote --heads --tags --exit-code origin "nightly-testing-${MOST_RECENT_NIGHTLY}" >/dev/null; then
             BASE="nightly-testing-${MOST_RECENT_NIGHTLY}"
           else
-            echo "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' tag at Std. Falling back to 'nightly-testing'."
+            echo "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' tag at Batteries. Falling back to 'nightly-testing'."
             BASE=nightly-testing
           fi
 
@@ -268,7 +268,7 @@ jobs:
           else
             echo "Branch already exists, pushing an empty commit."
             git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
-            # The Std `nightly-testing` or `nightly-testing-YYYY-MM-DD` branch may have moved since this branch was created, so merge their changes.
+            # The Batteries `nightly-testing` or `nightly-testing-YYYY-MM-DD` branch 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
             git commit --allow-empty -m "Trigger CI for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
@@ -321,7 +321,7 @@ 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 std from git \"https:\/\/github.com\/leanprover\/std4\" @ \".\+\"/require std from git \"https:\/\/github.com\/leanprover\/std4\" @ \"nightly-testing-${MOST_RECENT_NIGHTLY}\"/" lakefile.lean
+            sed -i "s/require batteries from git \"https:\/\/github.com\/leanprover-community\/batteries\" @ \".\+\"/require batteries from git \"https:\/\/github.com\/leanprover-community\/batteries\" @ \"nightly-testing-${MOST_RECENT_NIGHTLY}\"/" lakefile.lean
             git add lakefile.lean
             git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
           else

.github/workflows/restart-on-label.yml

@@ -0,0 +1,31 @@
+name: Restart by label
+on:
+  pull_request_target:
+    types:
+      - unlabeled
+      - labeled
+jobs:
+  restart-on-label:
+    runs-on: ubuntu-latest
+    if: contains(github.event.label.name, 'full-ci')
+    steps:
+    - run: |
+        # Finding latest CI workflow run on current pull request
+        # (unfortunately cannot search by PR number, only base branch,
+        # and that is't even unique given PRs from forks, but the risk
+        # of confusion is low and the danger is mild)
+        run_id=$(gh run list -e pull_request -b "$head_ref" --workflow 'CI' --limit 1 \
+          --limit 1 --json databaseId --jq '.[0].databaseId')
+        echo "Run id: ${run_id}"
+        gh run view "$run_id"
+        echo "Cancelling (just in case)"
+        gh run cancel "$run_id" || echo "(failed)"
+        echo "Waiting for 10s"
+        sleep 10
+        echo "Rerunning"
+        gh run rerun "$run_id"
+      shell: bash
+      env:
+        head_ref: ${{ github.head_ref }}
+        GH_TOKEN: ${{ github.token }}
+        GH_REPO: ${{ github.repository }}

CODEOWNERS

@@ -6,7 +6,6 @@
 
 /.github/ @Kha @semorrison
 /RELEASES.md @semorrison
-/src/Init/IO.lean @joehendrix
 /src/kernel/ @leodemoura
 /src/lake/ @tydeu
 /src/Lean/Compiler/ @leodemoura
@@ -20,7 +19,11 @@
 /src/Lean/PrettyPrinter/Delaborator/ @kmill
 /src/Lean/Server/ @mhuisi
 /src/Lean/Widget/ @Vtec234
-/src/runtime/io.cpp @joehendrix
+/src/Init/Data/ @semorrison
+/src/Init/Data/Array/Lemmas.lean @digama0
+/src/Init/Data/List/Lemmas.lean @digama0
+/src/Init/Data/List/BasicAux.lean @digama0
+/src/Init/Data/Array/Subarray.lean @david-christiansen
 /src/Lean/Elab/Tactic/RCases.lean @digama0
 /src/Init/RCases.lean @digama0
 /src/Lean/Elab/Tactic/Ext.lean @digama0
@@ -39,5 +42,4 @@
 /src/Lean/Elab/Tactic/Guard.lean @digama0
 /src/Init/Guard.lean @digama0
 /src/Lean/Server/CodeActions/ @digama0
-/src/Init/Data/Array/Subarray.lean @david-christiansen
 

README.md

@@ -22,4 +22,4 @@ Please read our [Contribution Guidelines](CONTRIBUTING.md) first.
 
 # Building from Source
 
-See [Building Lean](https://lean-lang.org/lean4/doc/make/index.html).
+See [Building Lean](https://lean-lang.org/lean4/doc/make/index.html) (documentation source: [doc/make/index.md](doc/make/index.md)).

RELEASES.md

@@ -8,7 +8,33 @@ This file contains work-in-progress notes for the upcoming release, as well as p
 Please check the [releases](https://github.com/leanprover/lean4/releases) page for the current status
 of each version.
 
-v4.8.0 (development in progress)
+v4.9.0 (development in progress)
+---------
+
+* Functions defined by well-founded recursion are now marked as
+  `@[irreducible]`, which should prevent expensive and often unfruitful
+  unfolding of such definitions.
+
+  Existing proofs that hold by definitional equality (e.g. `rfl`) can be
+  rewritten to explictly unfold the function definition (using `simp`,
+  `unfold`, `rw`), or the recursive function can be temporariliy made
+  semireducible (using `unseal f in` before the command) or the function
+  definition itself can be marked as `@[semireducible]` to get the previous
+  behavor.
+
+* The `MessageData.ofPPFormat` constructor has been removed.
+  Its functionality has been split into two:
+
+  - for lazy structured messages, please use `MessageData.lazy`;
+  - for embedding `Format` or `FormatWithInfos`, use `MessageData.ofFormatWithInfos`.
+
+  An example migration can be found in [#3929](https://github.com/leanprover/lean4/pull/3929/files#diff-5910592ab7452a0e1b2616c62d22202d2291a9ebb463145f198685aed6299867L109).
+
+* The `MessageData.ofFormat` constructor has been turned into a function.
+  If you need to inspect `MessageData`,
+  you can pattern-match on `MessageData.ofFormatWithInfos`.
+
+v4.8.0
 ---------
 
 * **Executables configured with `supportInterpreter := true` on Windows should now be run via `lake exe` to function properly.**
@@ -79,10 +105,13 @@ v4.8.0 (development in progress)
   Field notation can be disabled on a function-by-function basis using the `@[pp_nodot]` attribute.
 
 * Added options `pp.mvars` (default: true) and `pp.mvars.withType` (default: false).
-  When `pp.mvars` is false, metavariables pretty print as `?_`,
-  and when `pp.mvars.withType` is true, metavariables pretty print with a type ascription.
-  These can be set when using `#guard_msgs` to make tests not rely on the unique ids assigned to anonymous metavariables.
-  [#3798](https://github.com/leanprover/lean4/pull/3798).
+  When `pp.mvars` is false, expression metavariables pretty print as `?_` and universe metavariables pretty print as `_`.
+  When `pp.mvars.withType` is true, expression metavariables pretty print with a type ascription.
+  These can be set when using `#guard_msgs` to make tests not depend on the particular names of metavariables.
+  [#3798](https://github.com/leanprover/lean4/pull/3798) and
+  [#3978](https://github.com/leanprover/lean4/pull/3978).
+
+* Hovers for terms in `match` expressions in the Infoview now reliably show the correct term.
 
 * Added `@[induction_eliminator]` and `@[cases_eliminator]` attributes to be able to define custom eliminators
   for the `induction` and `cases` tactics, replacing the `@[eliminator]` attribute.

doc/BoolExpr.lean

@@ -1,4 +1,4 @@
-open Std
+open Batteries
 open Lean
 
 inductive BoolExpr where

doc/dev/bootstrap.md

@@ -75,14 +75,28 @@ The github repository will automatically update stage0 on `master` once
 
 If you have write access to the lean4 repository, you can also 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/nomeata/lean4/actions/workflows/update-stage0.yml>
+You can do that on <https://github.com/leanprover/lean4/actions/workflows/update-stage0.yml>
 or using Github CLI with
 ```
 gh workflow run update-stage0.yml
 ```
 
-Leaving stage0 updates to the CI automation is preferable, but should you need to do it locally, you can use `make update-stage0-commit` in `build/release` to update `stage0` from `stage1` or `make -C stageN update-stage0-commit` to update from another stage.
-This command will automatically stage the updated files and introduce a commit, so make sure to commit your work before that. Then coordinate with the admins to not squash your PR so that stage 0 updates are preserved as separate commits.
+Leaving stage0 updates to the CI automation is preferable, but should you need
+to do it locally, you can use `make update-stage0-commit` in `build/release` to
+update `stage0` from `stage1` or `make -C stageN update-stage0-commit` to
+update from another stage. This command will automatically stage the updated files
+and introduce a commit,so make sure to commit your work before that.
+
+If you rebased the branch (either onto a newer version of `master`, or fixing
+up some commits prior to the stage0 update, recreate the stage0 update commits.
+The script `script/rebase-stage0.sh` can be used for that.
+
+The CI should prevent PRs with changes to stage0 (besides `stdlib_flags.h`)
+from entering `master` through the (squashing!) merge queue, and label such PRs
+with the `changes-stage0` label. Such PRs should have a cleaned up history,
+with separate stage0 update commits; then coordinate with the admins to merge
+your PR using rebase merge, bypassing the merge queue.
+
 
 ## Further Bootstrapping Complications
 

doc/dev/ffi.md

@@ -53,10 +53,59 @@ In the case of `@[extern]` all *irrelevant* types are removed first; see next se
   Its runtime value is either a pointer to an opaque bignum object or, if the lowest bit of the "pointer" is 1 (`lean_is_scalar`), an encoded unboxed natural number (`lean_box`/`lean_unbox`).
 * A universe `Sort u`, type constructor `... → Sort u`, or proposition `p : Prop` is *irrelevant* and is either statically erased (see above) or represented as a `lean_object *` with the runtime value `lean_box(0)`
 * Any other type is represented by `lean_object *`.
-  Its runtime value is a pointer to an object of a subtype of `lean_object` (see respective declarations in `lean.h`) or the unboxed value `lean_box(cidx)` for the `cidx`th constructor of an inductive type if this constructor does not have any relevant parameters.
+  Its runtime value is a pointer to an object of a subtype of `lean_object` (see the "Inductive types" section below) or the unboxed value `lean_box(cidx)` for the `cidx`th constructor of an inductive type if this constructor does not have any relevant parameters.
 
   Example: the runtime value of `u : Unit` is always `lean_box(0)`.
 
+#### Inductive types
+
+For inductive types which are in the fallback `lean_object *` case above and not trivial constructors, the type is stored as a `lean_ctor_object`, and `lean_is_ctor` will return true. A `lean_ctor_object` stores the constructor index in the header, and the fields are stored in the `m_objs` portion of the object.
+
+The memory order of the fields is derived from the types and order of the fields in the declaration. They are ordered as follows:
+
+* Non-scalar fields stored as `lean_object *`
+* Fields of type `USize`
+* Other scalar fields, in decreasing order by size
+
+Within each group the fields are ordered in declaration order. **Warning**: Trivial wrapper types still count toward a field being treated as non-scalar for this purpose.
+
+* To access fields of the first kind, use `lean_ctor_get(val, i)` to get the `i`th non-scalar field.
+* To access `USize` fields, use `lean_ctor_get_usize(val, n+i)` to get the `i`th usize field and `n` is the total number of fields of the first kind.
+* To access other scalar fields, use `lean_ctor_get_uintN(val, off)` or `lean_ctor_get_usize(val, off)` as appropriate. Here `off` is the byte offset of the field in the structure, starting at `n*sizeof(void*)` where `n` is the number of fields of the first two kinds.
+
+For example, a structure such as
+```lean
+structure S where
+  ptr_1 : Array Nat
+  usize_1 : USize
+  sc64_1 : UInt64
+  ptr_2 : { x : UInt64 // x > 0 } -- wrappers don't count as scalars
+  sc64_2 : Float -- `Float` is 64 bit
+  sc8_1 : Bool
+  sc16_1 : UInt16
+  sc8_2 : UInt8
+  sc64_3 : UInt64
+  usize_2 : USize
+  ptr_3 : Char -- trivial wrapper around `UInt32`
+  sc32_1 : UInt32
+  sc16_2 : UInt16
+```
+would get re-sorted into the following memory order:
+
+* `S.ptr_1` - `lean_ctor_get(val, 0)`
+* `S.ptr_2` - `lean_ctor_get(val, 1)`
+* `S.ptr_3` - `lean_ctor_get(val, 2)`
+* `S.usize_1` - `lean_ctor_get_usize(val, 3)`
+* `S.usize_2` - `lean_ctor_get_usize(val, 4)`
+* `S.sc64_1` - `lean_ctor_get_uint64(val, sizeof(void*)*5)`
+* `S.sc64_2` - `lean_ctor_get_float(val, sizeof(void*)*5 + 8)`
+* `S.sc64_3` - `lean_ctor_get_uint64(val, sizeof(void*)*5 + 16)`
+* `S.sc32_1` - `lean_ctor_get_uint32(val, sizeof(void*)*5 + 24)`
+* `S.sc16_1` - `lean_ctor_get_uint16(val, sizeof(void*)*5 + 28)`
+* `S.sc16_2` - `lean_ctor_get_uint16(val, sizeof(void*)*5 + 30)`
+* `S.sc8_1` - `lean_ctor_get_uint8(val, sizeof(void*)*5 + 32)`
+* `S.sc8_2` - `lean_ctor_get_uint8(val, sizeof(void*)*5 + 33)`
+
 ### Borrowing
 
 By default, all `lean_object *` parameters of an `@[extern]` function are considered *owned*, i.e. the external code is passed a "virtual RC token" and is responsible for passing this token along to another consuming function (exactly once) or freeing it via `lean_dec`.

doc/dev/release_checklist.md

@@ -50,13 +50,13 @@ We'll use `v4.6.0` as the intended release version as a running example.
       - Toolchain bump PR
       - Create and push the tag
       - Merge the tag into `stable`
-    - [Std](https://github.com/leanprover-community/std4)
+    - [Batteries](https://github.com/leanprover-community/batteries)
       - No dependencies
       - Toolchain bump PR
       - Create and push the tag
       - Merge the tag into `stable`
     - [ProofWidgets4](https://github.com/leanprover-community/ProofWidgets4)
-      - Dependencies: `Std`
+      - Dependencies: `Batteries`
       - Note on versions and branches:
         - `ProofWidgets` uses a sequential version tagging scheme, e.g. `v0.0.29`,
           which does not refer to the toolchain being used.
@@ -65,7 +65,7 @@ We'll use `v4.6.0` as the intended release version as a running example.
       - Toolchain bump PR
       - Create and push the tag, following the version convention of the repository
     - [Aesop](https://github.com/leanprover-community/aesop)
-      - Dependencies: `Std`
+      - Dependencies: `Batteries`
       - Toolchain bump PR including updated Lake manifest
       - Create and push the tag
       - Merge the tag into `stable`
@@ -79,7 +79,7 @@ We'll use `v4.6.0` as the intended release version as a running example.
       - Create and push the tag
       - There is no `stable` branch; skip this step
     - [Mathlib](https://github.com/leanprover-community/mathlib4)
-      - Dependencies: `Aesop`, `ProofWidgets4`, `lean4checker`, `Std`, `doc-gen4`, `import-graph`
+      - Dependencies: `Aesop`, `ProofWidgets4`, `lean4checker`, `Batteries`, `doc-gen4`, `import-graph`
       - Toolchain bump PR notes:
         - In addition to updating the `lean-toolchain` and `lakefile.lean`,
           in `.github/workflows/build.yml.in` in the `lean4checker` section update the line
@@ -123,8 +123,8 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
 
 - Decide which nightly release you want to turn into a release candidate.
   We will use `nightly-2024-02-29` in this example.
-- It is essential that Std and Mathlib already have reviewed branches compatible with this nightly.
-  - Check that both Std and Mathlib's `bump/v4.7.0` branch contain `nightly-2024-02-29`
+- It is essential that Batteries and Mathlib already have reviewed branches compatible with this nightly.
+  - Check that both Batteries and Mathlib's `bump/v4.7.0` branch contain `nightly-2024-02-29`
     in their `lean-toolchain`.
   - The steps required to reach that state are beyond the scope of this checklist, but see below!
 - Create the release branch from this nightly tag:
@@ -182,7 +182,7 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
   - We do this for the same list of repositories as for stable releases, see above.
     As above, there are dependencies between these, and so the process above is iterative.
     It greatly helps if you can merge the `bump/v4.7.0` PRs yourself!
-  - For Std/Aesop/Mathlib, which maintain a `nightly-testing` branch, make sure there is a tag
+  - For Batteries/Aesop/Mathlib, which maintain a `nightly-testing` branch, make sure there is a tag
     `nightly-testing-2024-02-29` with date corresponding to the nightly used for the release
     (create it if not), and then on the `nightly-testing` branch `git reset --hard master`, and force push.
 - Make an announcement!
@@ -204,7 +204,7 @@ In particular, updating the downstream repositories is significantly more work
 # Preparing `bump/v4.7.0` branches
 
 While not part of the release process per se,
-this is a brief summary of the work that goes into updating Std/Aesop/Mathlib to new versions.
+this is a brief summary of the work that goes into updating Batteries/Aesop/Mathlib to new versions.
 
 Please read https://leanprover-community.github.io/contribute/tags_and_branches.html
 

doc/examples/Certora2022/ex8.lean

@@ -4,16 +4,16 @@ def ack : Nat → Nat → Nat
   | 0,   y   => y+1
   | x+1, 0   => ack x 1
   | x+1, y+1 => ack x (ack (x+1) y)
-termination_by ack x y => (x, y)
+termination_by x y => (x, y)
 
 def sum (a : Array Int) : Int :=
   let rec go (i : Nat) :=
-     if i < a.size then
+     if _ : i < a.size then
         a[i] + go (i+1)
      else
         0
+  termination_by a.size - i
   go 0
-termination_by go i => a.size - i
 
 set_option pp.proofs true
 #print sum.go

doc/examples/ICERM2022/ctor.lean

@@ -4,43 +4,42 @@ open Lean Meta
 
 def ctor (mvarId : MVarId) (idx : Nat) : MetaM (List MVarId) := do
   /- Set `MetaM` context using `mvarId` -/
-  withMVarContext mvarId do 
+  mvarId.withContext do
     /- Fail if the metavariable is already assigned. -/
-    checkNotAssigned mvarId `ctor
+    mvarId.checkNotAssigned `ctor
     /- Retrieve the target type, instantiateMVars, and use `whnf`. -/
-    let target ← getMVarType' mvarId
+    let target ← mvarId.getType'
     let .const declName us := target.getAppFn
       | throwTacticEx `ctor mvarId "target is not an inductive datatype"
     let .inductInfo { ctors, .. } ← getConstInfo declName
       | throwTacticEx `ctor mvarId "target is not an inductive datatype"
     if idx = 0 then
-      throwTacticEx `ctor mvarId "invalid index, it must be > 0"  
+      throwTacticEx `ctor mvarId "invalid index, it must be > 0"
     else if h : idx - 1 < ctors.length then
-      apply mvarId (.const ctors[idx - 1] us)
+      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} contructors"
 
 open Elab Tactic
 
-elab "ctor" idx:num : tactic => 
+elab "ctor" idx:num : tactic =>
   liftMetaTactic (ctor · idx.getNat)
 
-example (p : Prop) : p := by 
+example (p : Prop) : p := by
   ctor 1 -- Error
 
-example (h : q) : p ∨ q := by 
+example (h : q) : p ∨ q := by
   ctor 0 -- Error
   exact h
 
-example (h : q) : p ∨ q := by 
+example (h : q) : p ∨ q := by
   ctor 3 -- Error
   exact h
 
-example (h : q) : p ∨ q := by 
+example (h : q) : p ∨ q := by
   ctor 2
   exact h
 
-example (h : q) : p ∨ q := by 
+example (h : q) : p ∨ q := by
   ctor 1
-  exact h -- Error 
-
+  exact h -- Error

doc/examples/ICERM2022/meta.lean

@@ -5,15 +5,15 @@ open Lean Meta
 def ex1 (declName : Name) : MetaM Unit := do
   let info ← getConstInfo declName
   IO.println s!"{declName} : {← ppExpr info.type}"
-  if let some val := info.value? then 
+  if let some val := info.value? then
     IO.println s!"{declName} : {← ppExpr val}"
-    
+
 #eval ex1 ``Nat
 
 def ex2 (declName : Name) : MetaM Unit := do
   let info ← getConstInfo declName
   trace[Meta.debug] "{declName} : {info.type}"
-  if let some val := info.value? then 
+  if let some val := info.value? then
     trace[Meta.debug] "{declName} : {val}"
 
 #eval ex2 ``Add.add
@@ -30,9 +30,9 @@ def ex3 (declName : Name) : MetaM Unit := do
       trace[Meta.debug] "{x} : {← inferType x}"
 
 def myMin [LT α] [DecidableRel (α := α) (·<·)] (a b : α) : α :=
-  if a < b then 
+  if a < b then
     a
-  else 
+  else
     b
 
 set_option trace.Meta.debug true in
@@ -40,7 +40,7 @@ set_option trace.Meta.debug true in
 
 def ex4 : MetaM Unit := do
   let nat := mkConst ``Nat
-  withLocalDeclD `a nat fun a => 
+  withLocalDeclD `a nat fun a =>
   withLocalDeclD `b nat fun b => do
     let e ← mkAppM ``HAdd.hAdd #[a, b]
     trace[Meta.debug] "{e} : {← inferType e}"
@@ -66,15 +66,17 @@ open Elab Term
 
 def ex5 : TermElabM Unit := do
   let nat := Lean.mkConst ``Nat
-  withLocalDeclD `a nat fun a => do 
+  withLocalDeclD `a nat fun a => do
   withLocalDeclD `b nat fun b => do
     let ab ← mkAppM ``HAdd.hAdd #[a, b]
-    let stx ← `(fun x => if x < 10 then $(← exprToSyntax ab) + x else x + $(← exprToSyntax a))
+    let abStx ← exprToSyntax ab
+    let aStx ← exprToSyntax a
+    let stx ← `(fun x => if x < 10 then $abStx + x else x + $aStx)
     let e ← elabTerm stx none
     trace[Meta.debug] "{e} : {← inferType e}"
     let e := mkApp e (mkNatLit 5)
     let e ← whnf e
     trace[Meta.debug] "{e}"
-       
+
 set_option trace.Meta.debug true in
 #eval ex5

doc/examples/NFM2022/nfm8.lean

@@ -4,16 +4,16 @@ def ack : Nat → Nat → Nat
   | 0,   y   => y+1
   | x+1, 0   => ack x 1
   | x+1, y+1 => ack x (ack (x+1) y)
-termination_by ack x y => (x, y)
+termination_by x y => (x, y)
 
 def sum (a : Array Int) : Int :=
   let rec go (i : Nat) :=
-     if i < a.size then
+     if _ : i < a.size then
         a[i] + go (i+1)
      else
         0
+  termination_by a.size - i
   go 0
-termination_by go i => a.size - i
 
 set_option pp.proofs true
 #print sum.go

doc/monads/states.lean

@@ -15,7 +15,7 @@ data type containing several important pieces of information. First and foremost
 current player, and it has a random generator.
 -/
 
-open Std (HashMap)
+open Batteries (HashMap)
 abbrev TileIndex := Nat × Nat -- a 2D index
 
 inductive TileState where

nix/bootstrap.nix

@@ -180,7 +180,7 @@ rec {
       update-stage0 =
         let cTree = symlinkJoin { name = "cs"; paths = [ Init.cTree Lean.cTree ]; }; in
         writeShellScriptBin "update-stage0" ''
-          CSRCS=${cTree} CP_C_PARAMS="--dereference --no-preserve=all" ${src + "/script/update-stage0"}
+          CSRCS=${cTree} CP_C_PARAMS="--dereference --no-preserve=all" ${src + "/script/lib/update-stage0"}
         '';
       update-stage0-commit = writeShellScriptBin "update-stage0-commit" ''
         set -euo pipefail

script/issues_summary.sh

@@ -0,0 +1,39 @@
+#!/bin/bash
+
+# https://chat.openai.com/share/7469c7c3-aceb-4d80-aee5-62982e1f1538
+
+# Output CSV Header
+echo '"Issue URL","Title","Days Since Creation","Days Since Last Update","Total Reactions","Assignee","Labels"'
+
+# Get the current date in YYYY-MM-DD format
+today=$(date +%Y-%m-%d)
+
+# Fetch only open issues (excluding PRs and closed issues) from the repository 'leanprover/lean4'
+issues=$(gh api repos/leanprover/lean4/issues --paginate --jq '.[] | select(.pull_request == null and .state == "open") | {url: .html_url, title: .title, created_at: (.created_at | split("T")[0]), updated_at: (.updated_at | split("T")[0]), number: .number, assignee: (.assignee.login // ""), labels: [.labels[].name] | join(",")}')
+
+# Process each JSON object
+echo "$issues" | while IFS= read -r issue; do
+    # Extract fields from JSON
+    url=$(echo "$issue" | jq -r '.url')
+    title=$(echo "$issue" | jq -r '.title')
+    created_at=$(echo "$issue" | jq -r '.created_at')
+    updated_at=$(echo "$issue" | jq -r '.updated_at')
+    issue_number=$(echo "$issue" | jq -r '.number')
+    assignee=$(echo "$issue" | jq -r '.assignee')
+    labels=$(echo "$issue" | jq -r '.labels')
+
+    # Calculate days since creation and update using macOS compatible date calculation
+    days_since_created=$(( ($(date -jf "%Y-%m-%d" "$today" +%s) - $(date -jf "%Y-%m-%d" "$created_at" +%s)) / 86400 ))
+    days_since_updated=$(( ($(date -jf "%Y-%m-%d" "$today" +%s) - $(date -jf "%Y-%m-%d" "$updated_at" +%s)) / 86400 ))
+
+    # Fetch the total number of reactions for each issue
+    reaction_data=$(gh api repos/leanprover/lean4/issues/$issue_number/reactions --paginate --jq 'length' 2>&1)
+    if [[ $reaction_data == *"Not Found"* ]]; then
+        total_reactions="Error fetching reactions"
+    else
+        total_reactions=$reaction_data
+    fi
+
+    # Format output as CSV by escaping quotes and delimiting with commas
+    echo "\"$url\",\"${title//\"/\"\"}\",\"$days_since_created\",\"$days_since_updated\",\"$total_reactions\",\"$assignee\",\"$labels\""
+done

script/lib/README.md

@@ -0,0 +1,2 @@
+This directory contains various scripts that are *not* meant to be called
+directly, but through other scripts or makefiles.

script/lib/rebase-editor.sh

@@ -0,0 +1,19 @@
+#!/usr/bin/env bash
+
+
+# Script internal to `./script/rebase-stage0.sh`
+
+# Determine OS type for sed in-place editing
+SED_CMD=("sed" "-i")
+if [[ "$OSTYPE" == "darwin"* ]]
+then
+    # macOS requires an empty string argument with -i for in-place editing
+    SED_CMD=("sed" "-i" "")
+fi
+
+if [ "$STAGE0_WITH_NIX" = true ]
+then
+  "${SED_CMD[@]}" '/chore: update stage0/ s,.*,x nix run .#update-stage0-commit,' "$1"
+else
+  "${SED_CMD[@]}" '/chore: update stage0/ s,.*,x make -j32 -C build/release update-stage0 \&\& git commit -m "chore: update stage0",' "$1"
+fi

script/rebase-stage0.sh

@@ -0,0 +1,24 @@
+#!/usr/bin/env bash
+
+# This script rebases onto the given branch/commit, and updates
+# all `chore: update stage0` commits along the way.
+
+# Whether to use nix or make to update stage0
+if [ "$1" = "-nix" ]
+then
+   export STAGE0_WITH_NIX=true
+   shift
+fi
+
+# Check if an argument is provided
+if [ "$#" -eq 0 ]; then
+    echo "Usage: $0 [-nix] <options to git rebase -i>"
+    exit 1
+fi
+
+REPO_ROOT=$(git rev-parse --show-toplevel)
+
+# Run git rebase in interactive mode, but automatically edit the todo list
+# using the defined GIT_SEQUENCE_EDITOR command
+GIT_SEQUENCE_EDITOR="$REPO_ROOT/script/lib/rebase-editor.sh" git rebase -i "$@"
+

src/CMakeLists.txt

@@ -9,7 +9,7 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 8)
+set(LEAN_VERSION_MINOR 9)
 set(LEAN_VERSION_PATCH 0)
 set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
@@ -315,6 +315,12 @@ endif()
 string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
 string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
 
+# in local builds, link executables and not just dynlibs against C++ stdlib as well,
+# which is required for e.g. asan
+if(NOT LEAN_STANDALONE)
+  string(APPEND CMAKE_EXE_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
+endif()
+
 # flags for user binaries = flags for toolchain binaries + Lake
 string(APPEND LEANC_STATIC_LINKER_FLAGS " ${TOOLCHAIN_STATIC_LINKER_FLAGS} -lLake")
 
@@ -585,7 +591,7 @@ endif()
 
 if(PREV_STAGE)
   add_custom_target(update-stage0
-    COMMAND bash -c 'CSRCS=${CMAKE_BINARY_DIR}/lib/temp script/update-stage0'
+    COMMAND bash -c 'CSRCS=${CMAKE_BINARY_DIR}/lib/temp script/lib/update-stage0'
     DEPENDS make_stdlib
     WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/..")
 

src/Init.lean

@@ -34,3 +34,4 @@ import Init.BinderPredicates
 import Init.Ext
 import Init.Omega
 import Init.MacroTrace
+import Init.Grind

src/Init/ByCases.lean

@@ -63,3 +63,16 @@ theorem ite_some_none_eq_none [Decidable P] :
 @[simp] theorem ite_some_none_eq_some [Decidable P] :
     (if P then some x else none) = some y ↔ P ∧ x = y := by
   split <;> simp_all
+
+-- This is not marked as `simp` as it is already handled by `dite_eq_right_iff`.
+theorem dite_some_none_eq_none [Decidable P] {x : P → α} :
+    (if h : P then some (x h) else none) = none ↔ ¬P := by
+  simp only [dite_eq_right_iff]
+  rfl
+
+@[simp] theorem dite_some_none_eq_some [Decidable P] {x : P → α} {y : α} :
+    (if h : P then some (x h) else none) = some y ↔ ∃ h : P, x h = y := by
+  by_cases h : P <;> simp only [h, dite_cond_eq_true, dite_cond_eq_false, Option.some.injEq,
+    false_iff, not_exists]
+  case pos => exact ⟨fun h_eq ↦ Exists.intro h h_eq, fun h_exists => h_exists.2⟩
+  case neg => exact fun h_false _ ↦ h_false

src/Init/Classical.lean

@@ -15,6 +15,13 @@ namespace Classical
 noncomputable def indefiniteDescription {α : Sort u} (p : α → Prop) (h : ∃ x, p x) : {x // p x} :=
   choice <| let ⟨x, px⟩ := h; ⟨⟨x, px⟩⟩
 
+/--
+Given that there exists an element satisfying `p`, returns one such element.
+
+This is a straightforward consequence of, and equivalent to, `Classical.choice`.
+
+See also `choose_spec`, which asserts that the returned value has property `p`.
+-/
 noncomputable def choose {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : α :=
   (indefiniteDescription p h).val
 

src/Init/Control/Option.lean

@@ -10,7 +10,7 @@ import Init.Control.Except
 
 universe u v
 
-instance : ToBool (Option α) := ⟨Option.toBool⟩
+instance : ToBool (Option α) := ⟨Option.isSome⟩
 
 def OptionT (m : Type u → Type v) (α : Type u) : Type v :=
   m (Option α)

src/Init/Core.lean

@@ -1114,9 +1114,6 @@ theorem eta (a : {x // p x}) (h : p (val a)) : mk (val a) h = a := by
   cases a
   exact rfl
 
-instance {α : Type u} {p : α → Prop} {a : α} (h : p a) : Inhabited {x // p x} where
-  default := ⟨a, h⟩
-
 instance {α : Type u} {p : α → Prop} [DecidableEq α] : DecidableEq {x : α // p x} :=
   fun ⟨a, h₁⟩ ⟨b, h₂⟩ =>
     if h : a = b then isTrue (by subst h; exact rfl)
@@ -2040,4 +2037,8 @@ class LawfulCommIdentity (op : α → α → α) (o : outParam α) [hc : Commuta
   left_id a := Eq.trans (hc.comm o a) (right_id a)
   right_id a := Eq.trans (hc.comm a o) (left_id a)
 
+instance : Commutative Or := ⟨fun _ _ => propext or_comm⟩
+instance : Commutative And := ⟨fun _ _ => propext and_comm⟩
+instance : Commutative Iff := ⟨fun _ _ => propext iff_comm⟩
+
 end Std

src/Init/Data/Array/Basic.lean

@@ -31,6 +31,7 @@ def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
   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 :=
@@ -43,7 +44,7 @@ instance : EmptyCollection (Array α) := ⟨Array.empty⟩
 instance : Inhabited (Array α) where
   default := Array.empty
 
-def isEmpty (a : Array α) : Bool :=
+@[simp] def isEmpty (a : Array α) : Bool :=
   a.size = 0
 
 def singleton (v : α) : Array α :=
@@ -52,7 +53,7 @@ def singleton (v : α) : Array α :=
 /-- Low-level version of `fget` which is as fast as a C array read.
    `Fin` values are represented as tag pointers in the Lean runtime. Thus,
    `fget` may be slightly slower than `uget`. -/
-@[extern "lean_array_uget"]
+@[extern "lean_array_uget", simp]
 def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
   a[i.toNat]
 
@@ -306,6 +307,7 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
     else
       pure r
   termination_by as.size - i
+  decreasing_by simp_wf; decreasing_trivial_pre_omega
   map 0 (mkEmpty as.size)
 
 @[inline]
@@ -378,6 +380,7 @@ def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as :
       else
         pure false
       termination_by stop - j
+      decreasing_by simp_wf; decreasing_trivial_pre_omega
     loop start
   if h : stop ≤ as.size then
     any stop h
@@ -463,6 +466,7 @@ def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
       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 :=
@@ -557,6 +561,7 @@ def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) (
   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
@@ -661,6 +666,7 @@ def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size)
     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
@@ -703,6 +709,7 @@ def popWhile (p : α → Bool) (as : Array α) : Array α :=
   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 α :=
@@ -715,6 +722,7 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
     else
       r
     termination_by as.size - i
+    decreasing_by simp_wf; decreasing_trivial_pre_omega
   go 0 #[]
 
 /-- Remove the element at a given index from an array without bounds checks, using a `Fin` index.
@@ -725,16 +733,15 @@ 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
     let i' : Fin a'.size := ⟨i.val + 1, by simp [a', h]⟩
-    have : a'.size - i' < a.size - i := by
-      simp [a', Nat.sub_succ_lt_self _ _ i.isLt]
     a'.feraseIdx i'
   else
     a.pop
 termination_by a.size - i.val
+decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ i.isLt
 
 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 =>
+  | @case1 a i h a' _ ih =>
     unfold feraseIdx
     simp [h, a', ih]
   | case2 a i h =>
@@ -763,6 +770,7 @@ def erase [BEq α] (as : Array α) (a : α) : Array α :=
     else
       as
     termination_by j.1
+    decreasing_by simp_wf; decreasing_trivial_pre_omega
   let j := as.size
   let as := as.push a
   loop as ⟨j, size_push .. ▸ j.lt_succ_self⟩
@@ -816,6 +824,7 @@ def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : N
   else
     true
 termination_by as.size - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 /-- Return true iff `as` is a prefix of `bs`.
 That is, `bs = as ++ t` for some `t : List α`.-/
@@ -837,6 +846,7 @@ private def allDiffAux [BEq α] (as : Array α) (i : Nat) : Bool :=
   else
     true
 termination_by as.size - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def allDiff [BEq α] (as : Array α) : Bool :=
   allDiffAux as 0
@@ -852,6 +862,7 @@ def allDiff [BEq α] (as : Array α) : Bool :=
   else
     cs
 termination_by as.size - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 @[inline] def zipWith (as : Array α) (bs : Array β) (f : α → β → γ) : Array γ :=
   zipWithAux f as bs 0 #[]

src/Init/Data/Array/BasicAux.lean

@@ -48,6 +48,7 @@ where
       let b ← f as[i]
       go (i+1) ⟨acc.val.push b, by simp [acc.property]⟩ hlt
   termination_by as.size - i
+  decreasing_by decreasing_trivial_pre_omega
 
 @[inline] private unsafe def mapMonoMImp [Monad m] (as : Array α) (f : α → m α) : m (Array α) :=
   go 0 as

src/Init/Data/Array/DecidableEq.lean

@@ -21,6 +21,8 @@ theorem eq_of_isEqvAux [DecidableEq α] (a b : Array α) (hsz : a.size = b.size)
     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 eq_of_isEqv [DecidableEq α] (a b : Array α) : Array.isEqv a b (fun x y => x = y) → a = b := by
   simp [Array.isEqv]
@@ -37,6 +39,7 @@ theorem isEqvAux_self [DecidableEq α] (a : Array α) (i : Nat) : Array.isEqvAux
   case inl h => simp [h, isEqvAux_self a (i+1)]
   case inr h => simp [h]
 termination_by a.size - i
+decreasing_by decreasing_trivial_pre_omega
 
 theorem isEqv_self [DecidableEq α] (a : Array α) : Array.isEqv a a (fun x y => x = y) = true := by
   simp [isEqv, isEqvAux_self]

src/Init/Data/Array/Lemmas.lean

@@ -5,6 +5,7 @@ Authors: Mario Carneiro
 -/
 prelude
 import Init.Data.Nat.MinMax
+import Init.Data.Nat.Lemmas
 import Init.Data.List.Lemmas
 import Init.Data.Fin.Basic
 import Init.Data.Array.Mem
@@ -20,6 +21,13 @@ namespace Array
 
 attribute [simp] data_toArray uset
 
+@[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
+
+@[simp] theorem toArray_data : (a : Array α) → a.data.toArray = a
+  | ⟨l⟩ => ext' (data_toArray l)
+
+@[simp] theorem data_length {l : Array α} : l.data.length = l.size := rfl
+
 @[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl
 
 @[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]
@@ -130,6 +138,7 @@ where
       simp [aux (i+1), map_eq_pure_bind]; rfl
     · rw [List.drop_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
   termination_by arr.size - i
+  decreasing_by decreasing_trivial_pre_omega
 
 @[simp] theorem map_data (f : α → β) (arr : Array α) : (arr.map f).data = arr.data.map f := by
   rw [map, mapM_eq_foldlM]
@@ -139,7 +148,8 @@ where
   simp [H]
 
 @[simp] theorem size_map (f : α → β) (arr : Array α) : (arr.map f).size = arr.size := by
-  simp [size]
+  simp only [← data_length]
+  simp
 
 @[simp] theorem pop_data (arr : Array α) : arr.pop.data = arr.data.dropLast := rfl
 
@@ -187,7 +197,8 @@ theorem anyM_stop_le_start [Monad m] (p : α → m Bool) (as : Array α) (start
 theorem mem_def (a : α) (as : Array α) : a ∈ as ↔ a ∈ as.data :=
   ⟨fun | .mk h => h, Array.Mem.mk⟩
 
-/-- # get -/
+/-! # get -/
+
 @[simp] theorem get_eq_getElem (a : Array α) (i : Fin _) : a.get i = a[i.1] := rfl
 
 theorem getElem?_lt
@@ -217,7 +228,7 @@ theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default
 @[simp] theorem get!_eq_getElem? [Inhabited α] (a : Array α) (i : Nat) : a.get! i = (a.get? i).getD default := by
   by_cases p : i < a.size <;> simp [getD_get?, get!_eq_getD, p]
 
-/-- # set -/
+/-! # set -/
 
 @[simp] theorem getElem_set_eq (a : Array α) (i : Fin a.size) (v : α) {j : Nat}
       (eq : i.val = j) (p : j < (a.set i v).size) :
@@ -240,7 +251,7 @@ theorem getElem_set (a : Array α) (i : Fin a.size) (v : α) (j : Nat)
     (ne : i.val ≠ j) : (a.set i v)[j]? = a[j]? := by
   by_cases h : j < a.size <;> simp [getElem?_lt, getElem?_ge, Nat.ge_of_not_lt, ne, h]
 
-/- # setD -/
+/-! # setD -/
 
 @[simp] theorem set!_is_setD : @set! = @setD := rfl
 
@@ -266,4 +277,788 @@ theorem getElem?_setD_eq (a : Array α) {i : Nat} (p : i < a.size) (v : α) : (a
   by_cases h : i < a.size <;>
     simp [setD, Nat.not_lt_of_le, h,  getD_get?]
 
+/-! # ofFn -/
+
+@[simp] theorem size_ofFn_go {n} (f : Fin n → α) (i acc) :
+    (ofFn.go f i acc).size = acc.size + (n - i) := by
+  if hin : i < n then
+    unfold ofFn.go
+    have : 1 + (n - (i + 1)) = n - i :=
+      Nat.sub_sub .. ▸ Nat.add_sub_cancel' (Nat.le_sub_of_add_le (Nat.add_comm .. ▸ hin))
+    rw [dif_pos hin, size_ofFn_go f (i+1), size_push, Nat.add_assoc, this]
+  else
+    have : n - i = 0 := Nat.sub_eq_zero_of_le (Nat.le_of_not_lt hin)
+    unfold ofFn.go
+    simp [hin, this]
+termination_by n - i
+
+@[simp] theorem size_ofFn (f : Fin n → α) : (ofFn f).size = n := by simp [ofFn]
+
+theorem getElem_ofFn_go (f : Fin n → α) (i) {acc k}
+    (hki : k < n) (hin : i ≤ n) (hi : i = acc.size)
+    (hacc : ∀ j, ∀ hj : j < acc.size, acc[j] = f ⟨j, Nat.lt_of_lt_of_le hj (hi ▸ hin)⟩) :
+    haveI : acc.size + (n - acc.size) = n := Nat.add_sub_cancel' (hi ▸ hin)
+    (ofFn.go f i acc)[k]'(by simp [*]) = f ⟨k, hki⟩ := by
+  unfold ofFn.go
+  if hin : i < n then
+    have : 1 + (n - (i + 1)) = n - i :=
+      Nat.sub_sub .. ▸ Nat.add_sub_cancel' (Nat.le_sub_of_add_le (Nat.add_comm .. ▸ hin))
+    simp only [dif_pos hin]
+    rw [getElem_ofFn_go f (i+1) _ hin (by simp [*]) (fun j hj => ?hacc)]
+    cases (Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ (by simpa using hj)) with
+    | inl hj => simp [get_push, hj, hacc j hj]
+    | inr hj => simp [get_push, *]
+  else
+    simp [hin, hacc k (Nat.lt_of_lt_of_le hki (Nat.le_of_not_lt (hi ▸ hin)))]
+termination_by n - i
+
+@[simp] theorem getElem_ofFn (f : Fin n → α) (i : Nat) (h) :
+    (ofFn f)[i] = f ⟨i, size_ofFn f ▸ h⟩ :=
+  getElem_ofFn_go _ _ _ (by simp) (by simp) nofun
+
+/-- # mkArray -/
+
+@[simp] theorem mkArray_data (n : Nat) (v : α) : (mkArray n v).data = List.replicate n v := rfl
+
+@[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) :
+    (mkArray n v)[i] = v := by simp [Array.getElem_eq_data_get]
+
+/-- # mem -/
+
+theorem mem_data {a : α} {l : Array α} : a ∈ l.data ↔ a ∈ l := (mem_def _ _).symm
+
+theorem not_mem_nil (a : α) : ¬ a ∈ #[] := nofun
+
+/-- # get lemmas -/
+
+theorem getElem?_mem {l : Array α} {i : Fin l.size} : l[i] ∈ l := by
+  erw [Array.mem_def, getElem_eq_data_get]
+  apply List.get_mem
+
+theorem getElem_fin_eq_data_get (a : Array α) (i : Fin _) : a[i] = a.data.get i := rfl
+
+@[simp] theorem ugetElem_eq_getElem (a : Array α) {i : USize} (h : i.toNat < a.size) :
+  a[i] = a[i.toNat] := rfl
+
+theorem getElem?_eq_getElem (a : Array α) (i : Nat) (h : i < a.size) : a[i]? = a[i] :=
+  getElem?_pos ..
+
+theorem get?_len_le (a : Array α) (i : Nat) (h : a.size ≤ i) : a[i]? = none := by
+  simp [getElem?_neg, h]
+
+theorem getElem_mem_data (a : Array α) (h : i < a.size) : a[i] ∈ a.data := by
+  simp only [getElem_eq_data_get, List.get_mem]
+
+theorem getElem?_eq_data_get? (a : Array α) (i : Nat) : a[i]? = a.data.get? i := by
+  by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg, List.get?_eq_get, eq_comm]; rfl
+
+theorem get?_eq_data_get? (a : Array α) (i : Nat) : a.get? i = a.data.get? i :=
+  getElem?_eq_data_get? ..
+
+theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD default := by
+  simp [get!_eq_getD]
+
+@[simp] theorem back_eq_back? [Inhabited α] (a : Array α) : a.back = a.back?.getD default := by
+  simp [back, back?]
+
+@[simp] theorem back?_push (a : Array α) : (a.push x).back? = some x := by
+  simp [back?, getElem?_eq_data_get?]
+
+theorem back_push [Inhabited α] (a : Array α) : (a.push x).back = x := by simp
+
+theorem get?_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
+    (a.push x)[i]? = some a[i] := by
+  rw [getElem?_pos, get_push_lt]
+
+theorem get?_push_eq (a : Array α) (x : α) : (a.push x)[a.size]? = some x := by
+  rw [getElem?_pos, get_push_eq]
+
+theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x else a[i]? := by
+  match Nat.lt_trichotomy i a.size with
+  | Or.inl g =>
+    have h1 : i < a.size + 1 := by omega
+    have h2 : i ≠ a.size := by omega
+    simp [getElem?, size_push, g, h1, h2, get_push_lt]
+  | Or.inr (Or.inl heq) =>
+    simp [heq, getElem?_pos, get_push_eq]
+  | Or.inr (Or.inr g) =>
+    simp only [getElem?, size_push]
+    have h1 : ¬ (i < a.size) := by omega
+    have h2 : ¬ (i < a.size + 1) := by omega
+    have h3 : i ≠ a.size := by omega
+    simp [h1, h2, h3]
+
+@[simp] theorem get?_size {a : Array α} : a[a.size]? = none := by
+  simp only [getElem?, Nat.lt_irrefl, dite_false]
+
+@[simp] theorem data_set (a : Array α) (i v) : (a.set i v).data = a.data.set i.1 v := rfl
+
+theorem get_set_eq (a : Array α) (i : Fin a.size) (v : α) :
+    (a.set i v)[i.1] = v := by
+  simp only [set, getElem_eq_data_get, List.get_set_eq]
+
+theorem get?_set_eq (a : Array α) (i : Fin a.size) (v : α) :
+    (a.set i v)[i.1]? = v := by simp [getElem?_pos, i.2]
+
+@[simp] theorem get?_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α)
+    (h : i.1 ≠ j) : (a.set i v)[j]? = a[j]? := by
+  by_cases j < a.size <;> simp [getElem?_pos, getElem?_neg, *]
+
+theorem get?_set (a : Array α) (i : Fin a.size) (j : Nat) (v : α) :
+    (a.set i v)[j]? = if i.1 = j then some v else a[j]? := by
+  if h : i.1 = j then subst j; simp [*] else simp [*]
+
+theorem get_set (a : Array α) (i : Fin a.size) (j : Nat) (hj : j < a.size) (v : α) :
+    (a.set i v)[j]'(by simp [*]) = if i = j then v else a[j] := by
+  if h : i.1 = j then subst j; simp [*] else simp [*]
+
+@[simp] theorem get_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α) (hj : j < a.size)
+    (h : i.1 ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
+  simp only [set, getElem_eq_data_get, List.get_set_ne _ h]
+
+theorem getElem_setD (a : Array α) (i : Nat) (v : α) (h : i < (setD a i v).size) :
+  (setD a i v)[i] = v := by
+  simp at h
+  simp only [setD, h, dite_true, get_set, ite_true]
+
+theorem set_set (a : Array α) (i : Fin a.size) (v v' : α) :
+    (a.set i v).set ⟨i, by simp [i.2]⟩ v' = a.set i v' := by simp [set, List.set_set]
+
+private theorem fin_cast_val (e : n = n') (i : Fin n) : e ▸ i = ⟨i.1, e ▸ i.2⟩ := by cases e; rfl
+
+theorem swap_def (a : Array α) (i j : Fin a.size) :
+    a.swap i j = (a.set i (a.get j)).set ⟨j.1, by simp [j.2]⟩ (a.get i) := by
+  simp [swap, fin_cast_val]
+
+theorem data_swap (a : Array α) (i j : Fin a.size) :
+    (a.swap i j).data = (a.data.set i (a.get j)).set j (a.get i) := by simp [swap_def]
+
+theorem get?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)[k]? =
+    if j = k then some a[i.1] else if i = k then some a[j.1] else a[k]? := by
+  simp [swap_def, get?_set, ← getElem_fin_eq_data_get]
+
+@[simp] theorem swapAt_def (a : Array α) (i : Fin a.size) (v : α) :
+    a.swapAt i v = (a[i.1], a.set i v) := rfl
+
+-- @[simp] -- FIXME: gives a weird linter error
+theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
+    a.swapAt! i v = (a[i], a.set ⟨i, h⟩ v) := by simp [swapAt!, h]
+
+@[simp] theorem data_pop (a : Array α) : a.pop.data = a.data.dropLast := by simp [pop]
+
+@[simp] theorem pop_empty : (#[] : Array α).pop = #[] := rfl
+
+@[simp] theorem pop_push (a : Array α) : (a.push x).pop = a := by simp [pop]
+
+@[simp] theorem getElem_pop (a : Array α) (i : Nat) (hi : i < a.pop.size) :
+    a.pop[i] = a[i]'(Nat.lt_of_lt_of_le (a.size_pop ▸ hi) (Nat.sub_le _ _)) :=
+  List.get_dropLast ..
+
+theorem eq_empty_of_size_eq_zero {as : Array α} (h : as.size = 0) : as = #[] := by
+  apply ext
+  · simp [h]
+  · intros; contradiction
+
+theorem eq_push_pop_back_of_size_ne_zero [Inhabited α] {as : Array α} (h : as.size ≠ 0) :
+    as = as.pop.push as.back := by
+  apply ext
+  · simp [Nat.sub_add_cancel (Nat.zero_lt_of_ne_zero h)]
+  · intros i h h'
+    if hlt : i < as.pop.size then
+      rw [get_push_lt (h:=hlt), getElem_pop]
+    else
+      have heq : i = as.pop.size :=
+        Nat.le_antisymm (size_pop .. ▸ Nat.le_pred_of_lt h) (Nat.le_of_not_gt hlt)
+      cases heq; rw [get_push_eq, back, ←size_pop, get!_eq_getD, getD, dif_pos h]; rfl
+
+theorem eq_push_of_size_ne_zero {as : Array α} (h : as.size ≠ 0) :
+    ∃ (bs : Array α) (c : α), as = bs.push c :=
+  let _ : Inhabited α := ⟨as[0]⟩
+  ⟨as.pop, as.back, eq_push_pop_back_of_size_ne_zero h⟩
+
+theorem size_eq_length_data (as : Array α) : as.size = as.data.length := rfl
+
+@[simp] theorem size_swap! (a : Array α) (i j) :
+    (a.swap! i j).size = a.size := by unfold swap!; split <;> (try split) <;> simp [size_swap]
+
+@[simp] theorem size_reverse (a : Array α) : a.reverse.size = a.size := by
+  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
+  simp only [reverse]; split <;> simp [go]
+
+@[simp] theorem size_range {n : Nat} : (range n).size = n := by
+  unfold range
+  induction n with
+  | zero      => simp [Nat.fold]
+  | succ k ih =>
+    rw [Nat.fold, flip]
+    simp only [mkEmpty_eq, size_push] at *
+    omega
+
+@[simp] theorem reverse_data (a : Array α) : a.reverse.data = a.data.reverse := by
+  let rec go (as : Array α) (i j hj)
+      (h : i + j + 1 = a.size) (h₂ : as.size = a.size)
+      (H : ∀ k, as.data.get? k = if i ≤ k ∧ k ≤ j then a.data.get? k else a.data.reverse.get? k)
+      (k) : (reverse.loop as i ⟨j, hj⟩).data.get? k = a.data.reverse.get? k := by
+    rw [reverse.loop]; dsimp; split <;> rename_i h₁
+    · have := reverse.termination h₁
+      match j with | j+1 => ?_
+      simp at *
+      rw [(go · (i+1) j)]
+      · rwa [Nat.add_right_comm i]
+      · simp [size_swap, h₂]
+      · intro k
+        rw [← getElem?_eq_data_get?, get?_swap]
+        simp [getElem?_eq_data_get?, getElem_eq_data_get, ← List.get?_eq_get, H, Nat.le_of_lt h₁]
+        split <;> rename_i h₂
+        · simp [← h₂, Nat.not_le.2 (Nat.lt_succ_self _)]
+          exact (List.get?_reverse' _ _ (Eq.trans (by simp_arith) h)).symm
+        split <;> rename_i h₃
+        · simp [← h₃, Nat.not_le.2 (Nat.lt_succ_self _)]
+          exact (List.get?_reverse' _ _ (Eq.trans (by simp_arith) h)).symm
+        simp only [Nat.succ_le, Nat.lt_iff_le_and_ne.trans (and_iff_left h₃),
+          Nat.lt_succ.symm.trans (Nat.lt_iff_le_and_ne.trans (and_iff_left (Ne.symm h₂)))]
+    · rw [H]; split <;> rename_i h₂
+      · cases Nat.le_antisymm (Nat.not_lt.1 h₁) (Nat.le_trans h₂.1 h₂.2)
+        cases Nat.le_antisymm h₂.1 h₂.2
+        exact (List.get?_reverse' _ _ h).symm
+      · rfl
+    termination_by j - i
+  simp only [reverse]; split
+  · match a with | ⟨[]⟩ | ⟨[_]⟩ => rfl
+  · have := Nat.sub_add_cancel (Nat.le_of_not_le ‹_›)
+    refine List.ext <| go _ _ _ _ (by simp [this]) rfl fun k => ?_
+    split; {rfl}; rename_i h
+    simp [← show k < _ + 1 ↔ _ from Nat.lt_succ (n := a.size - 1), this] at h
+    rw [List.get?_eq_none.2 ‹_›, List.get?_eq_none.2 (a.data.length_reverse ▸ ‹_›)]
+
+/-! ### foldl / foldr -/
+
+-- This proof is the pure version of `Array.SatisfiesM_foldlM`,
+-- reproduced to avoid a dependency on `SatisfiesM`.
+theorem foldl_induction
+    {as : Array α} (motive : Nat → β → Prop) {init : β} (h0 : motive 0 init) {f : β → α → β}
+    (hf : ∀ i : Fin as.size, ∀ b, motive i.1 b → motive (i.1 + 1) (f b as[i])) :
+    motive as.size (as.foldl f init) := by
+  let rec go {i j b} (h₁ : j ≤ as.size) (h₂ : as.size ≤ i + j) (H : motive j b) :
+    (motive as.size) (foldlM.loop (m := Id) f as as.size (Nat.le_refl _) i j b) := by
+    unfold foldlM.loop; split
+    · next hj =>
+      split
+      · cases Nat.not_le_of_gt (by simp [hj]) h₂
+      · exact go hj (by rwa [Nat.succ_add] at h₂) (hf ⟨j, hj⟩ b H)
+    · next hj => exact Nat.le_antisymm h₁ (Nat.ge_of_not_lt hj) ▸ H
+  simpa [foldl, foldlM] using go (Nat.zero_le _) (Nat.le_refl _) h0
+
+-- This proof is the pure version of `Array.SatisfiesM_foldrM`,
+-- reproduced to avoid a dependency on `SatisfiesM`.
+theorem foldr_induction
+    {as : Array α} (motive : Nat → β → Prop) {init : β} (h0 : motive as.size init) {f : α → β → β}
+    (hf : ∀ i : Fin as.size, ∀ b, motive (i.1 + 1) b → motive i.1 (f as[i] b)) :
+    motive 0 (as.foldr f init) := by
+  let rec go {i b} (hi : i ≤ as.size) (H : motive i b) :
+    (motive 0) (foldrM.fold (m := Id) f as 0 i hi b) := by
+    unfold foldrM.fold; simp; split
+    · next hi => exact (hi ▸ H)
+    · next hi =>
+      split; {simp at hi}
+      · next i hi' =>
+        exact go _ (hf ⟨i, hi'⟩ b H)
+  simp [foldr, foldrM]; split; {exact go _ h0}
+  · next h => exact (Nat.eq_zero_of_not_pos h ▸ h0)
+
+/-! ### map -/
+
+@[simp] theorem mem_map {f : α → β} {l : Array α} : b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b := by
+  simp only [mem_def, map_data, List.mem_map]
+
+theorem mapM_eq_mapM_data [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
+    arr.mapM f = return mk (← arr.data.mapM f) := by
+  rw [mapM_eq_foldlM, foldlM_eq_foldlM_data, ← List.foldrM_reverse]
+  conv => rhs; rw [← List.reverse_reverse arr.data]
+  induction arr.data.reverse with
+  | nil => simp; rfl
+  | cons a l ih => simp [ih]; simp [map_eq_pure_bind, push]
+
+theorem mapM_map_eq_foldl (as : Array α) (f : α → β) (i) :
+    mapM.map (m := Id) f as i b = as.foldl (start := i) (fun r a => r.push (f a)) b := by
+  unfold mapM.map
+  split <;> rename_i h
+  · simp only [Id.bind_eq]
+    dsimp [foldl, Id.run, foldlM]
+    rw [mapM_map_eq_foldl, dif_pos (by omega), foldlM.loop, dif_pos h]
+    -- Calling `split` here gives a bad goal.
+    have : size as - i = Nat.succ (size as - i - 1) := by omega
+    rw [this]
+    simp [foldl, foldlM, Id.run, Nat.sub_add_eq]
+  · dsimp [foldl, Id.run, foldlM]
+    rw [dif_pos (by omega), foldlM.loop, dif_neg h]
+    rfl
+termination_by as.size - i
+
+theorem map_eq_foldl (as : Array α) (f : α → β) :
+    as.map f = as.foldl (fun r a => r.push (f a)) #[] :=
+  mapM_map_eq_foldl _ _ _
+
+theorem map_induction (as : Array α) (f : α → β) (motive : Nat → Prop) (h0 : motive 0)
+    (p : Fin as.size → β → Prop) (hs : ∀ i, motive i.1 → p i (f as[i]) ∧ motive (i+1)) :
+    motive as.size ∧
+      ∃ eq : (as.map f).size = as.size, ∀ i h, p ⟨i, h⟩ ((as.map f)[i]) := by
+  have t := foldl_induction (as := as) (β := Array β)
+    (motive := fun i arr => motive i ∧ arr.size = i ∧ ∀ i h2, p i arr[i.1])
+    (init := #[]) (f := fun r a => r.push (f a)) ?_ ?_
+  obtain ⟨m, eq, w⟩ := t
+  · refine ⟨m, by simpa [map_eq_foldl] using eq, ?_⟩
+    intro i h
+    simp [eq] at w
+    specialize w ⟨i, h⟩ h
+    simpa [map_eq_foldl] using w
+  · exact ⟨h0, rfl, nofun⟩
+  · intro i b ⟨m, ⟨eq, w⟩⟩
+    refine ⟨?_, ?_, ?_⟩
+    · exact (hs _ m).2
+    · simp_all
+    · intro j h
+      simp at h ⊢
+      by_cases h' : j < size b
+      · rw [get_push]
+        simp_all
+      · rw [get_push, dif_neg h']
+        simp only [show j = i by omega]
+        exact (hs _ m).1
+
+theorem map_spec (as : Array α) (f : α → β) (p : Fin as.size → β → Prop)
+    (hs : ∀ i, p i (f as[i])) :
+    ∃ eq : (as.map f).size = as.size, ∀ i h, p ⟨i, h⟩ ((as.map f)[i]) := by
+  simpa using map_induction as f (fun _ => True) trivial p (by simp_all)
+
+@[simp] theorem getElem_map (f : α → β) (as : Array α) (i : Nat) (h) :
+    ((as.map f)[i]) = f (as[i]'(size_map .. ▸ h)) := by
+  have := map_spec as f (fun i b => b = f (as[i]))
+  simp only [implies_true, true_implies] at this
+  obtain ⟨eq, w⟩ := this
+  apply w
+  simp_all
+
+/-! ### mapIdx -/
+
+-- This could also be prove from `SatisfiesM_mapIdxM`.
+theorem mapIdx_induction (as : Array α) (f : Fin as.size → α → β)
+    (motive : Nat → Prop) (h0 : motive 0)
+    (p : Fin as.size → β → Prop)
+    (hs : ∀ i, motive i.1 → p i (f i as[i]) ∧ motive (i + 1)) :
+    motive as.size ∧ ∃ eq : (Array.mapIdx as f).size = as.size,
+      ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]) := by
+  let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : ∀ i h h', p ⟨i, h⟩ bs[i]) (hm : motive j) :
+    let arr : Array β := Array.mapIdxM.map (m := Id) as f i j h bs
+    motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i] := by
+    induction i generalizing j bs with simp [mapIdxM.map]
+    | zero =>
+      have := (Nat.zero_add _).symm.trans h
+      exact ⟨this ▸ hm, h₁ ▸ this, fun _ _ => h₂ ..⟩
+    | succ i ih =>
+      apply @ih (bs.push (f ⟨j, by omega⟩ as[j])) (j + 1) (by omega) (by simp; omega)
+      · intro i i_lt h'
+        rw [get_push]
+        split
+        · apply h₂
+        · simp only [size_push] at h'
+          obtain rfl : i = j := by omega
+          apply (hs ⟨i, by omega⟩ hm).1
+      · exact (hs ⟨j, by omega⟩ hm).2
+  simp [mapIdx, mapIdxM]; exact go rfl nofun h0
+
+theorem mapIdx_spec (as : Array α) (f : Fin as.size → α → β)
+    (p : Fin as.size → β → Prop) (hs : ∀ i, p i (f i as[i])) :
+    ∃ eq : (Array.mapIdx as f).size = as.size,
+      ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]) :=
+  (mapIdx_induction _ _ (fun _ => True) trivial p fun _ _ => ⟨hs .., trivial⟩).2
+
+@[simp] theorem size_mapIdx (a : Array α) (f : Fin a.size → α → β) : (a.mapIdx f).size = a.size :=
+  (mapIdx_spec (p := fun _ _ => True) (hs := fun _ => trivial)).1
+
+@[simp] theorem size_zipWithIndex (as : Array α) : as.zipWithIndex.size = as.size :=
+  Array.size_mapIdx _ _
+
+@[simp] theorem getElem_mapIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat)
+    (h : i < (mapIdx a f).size) :
+    haveI : i < a.size := by simp_all
+    (a.mapIdx f)[i] = f ⟨i, this⟩ a[i] :=
+  (mapIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i _
+
+/-! ### modify -/
+
+@[simp] theorem size_modify (a : Array α) (i : Nat) (f : α → α) : (a.modify i f).size = a.size := by
+  unfold modify modifyM Id.run
+  split <;> simp
+
+theorem get_modify {arr : Array α} {x i} (h : i < arr.size) :
+    (arr.modify x f).get ⟨i, by simp [h]⟩ =
+    if x = i then f (arr.get ⟨i, h⟩) else arr.get ⟨i, h⟩ := by
+  simp [modify, modifyM, Id.run]; split
+  · simp [get_set _ _ _ h]; split <;> simp [*]
+  · rw [if_neg (mt (by rintro rfl; exact h) ‹_›)]
+
+/-! ### filter -/
+
+@[simp] theorem filter_data (p : α → Bool) (l : Array α) :
+    (l.filter p).data = l.data.filter p := by
+  dsimp only [filter]
+  rw [foldl_eq_foldl_data]
+  generalize l.data = l
+  suffices ∀ a, (List.foldl (fun r a => if p a = true then push r a else r) a l).data =
+      a.data ++ List.filter p l by
+    simpa using this #[]
+  induction l with simp
+  | cons => split <;> simp [*]
+
+@[simp] theorem filter_filter (q) (l : Array α) :
+    filter p (filter q l) = filter (fun a => p a ∧ q a) l := by
+  apply ext'
+  simp only [filter_data, List.filter_filter]
+
+@[simp] theorem mem_filter : x ∈ filter p as ↔ x ∈ as ∧ p x := by
+  simp only [mem_def, filter_data, List.mem_filter]
+
+theorem mem_of_mem_filter {a : α} {l} (h : a ∈ filter p l) : a ∈ l :=
+  (mem_filter.mp h).1
+
+/-! ### filterMap -/
+
+@[simp] theorem filterMap_data (f : α → Option β) (l : Array α) :
+    (l.filterMap f).data = l.data.filterMap f := by
+  dsimp only [filterMap, filterMapM]
+  rw [foldlM_eq_foldlM_data]
+  generalize l.data = l
+  have this : ∀ a : Array β, (Id.run (List.foldlM (m := Id) ?_ a l)).data =
+    a.data ++ List.filterMap f l := ?_
+  exact this #[]
+  induction l
+  · simp_all [Id.run]
+  · simp_all [Id.run]
+    split <;> simp_all
+
+@[simp] theorem mem_filterMap (f : α → Option β) (l : Array α) {b : β} :
+    b ∈ filterMap f l ↔ ∃ a, a ∈ l ∧ f a = some b := by
+  simp only [mem_def, filterMap_data, List.mem_filterMap]
+
+/-! ### empty -/
+
+theorem size_empty : (#[] : Array α).size = 0 := rfl
+
+theorem empty_data : (#[] : Array α).data = [] := rfl
+
+/-! ### append -/
+
+theorem push_eq_append_singleton (as : Array α) (x) : as.push x = as ++ #[x] := rfl
+
+@[simp] theorem mem_append {a : α} {s t : Array α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t := by
+  simp only [mem_def, append_data, List.mem_append]
+
+theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
+  simp only [size, append_data, List.length_append]
+
+theorem get_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
+    (as ++ bs)[i] = as[i] := by
+  simp only [getElem_eq_data_get]
+  have h' : i < (as.data ++ bs.data).length := by rwa [← data_length, append_data] at h
+  conv => rhs; rw [← List.get_append_left (bs:=bs.data) (h':=h')]
+  apply List.get_of_eq; rw [append_data]
+
+theorem get_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i)
+    (hlt : i - as.size < bs.size := Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h)) :
+    (as ++ bs)[i] = bs[i - as.size] := by
+  simp only [getElem_eq_data_get]
+  have h' : i < (as.data ++ bs.data).length := by rwa [← data_length, append_data] at h
+  conv => rhs; rw [← List.get_append_right (h':=h') (h:=Nat.not_lt_of_ge hle)]
+  apply List.get_of_eq; rw [append_data]
+
+@[simp] theorem append_nil (as : Array α) : as ++ #[] = as := by
+  apply ext'; simp only [append_data, empty_data, List.append_nil]
+
+@[simp] theorem nil_append (as : Array α) : #[] ++ as = as := by
+  apply ext'; simp only [append_data, empty_data, List.nil_append]
+
+theorem append_assoc (as bs cs : Array α) : as ++ bs ++ cs = as ++ (bs ++ cs) := by
+  apply ext'; simp only [append_data, List.append_assoc]
+
+/-! ### extract -/
+
+theorem extract_loop_zero (as bs : Array α) (start : Nat) : extract.loop as 0 start bs = bs := by
+  rw [extract.loop]; split <;> rfl
+
+theorem extract_loop_succ (as bs : Array α) (size start : Nat) (h : start < as.size) :
+    extract.loop as (size+1) start bs = extract.loop as size (start+1) (bs.push as[start]) := by
+  rw [extract.loop, dif_pos h]; rfl
+
+theorem extract_loop_of_ge (as bs : Array α) (size start : Nat) (h : start ≥ as.size) :
+    extract.loop as size start bs = bs := by
+  rw [extract.loop, dif_neg (Nat.not_lt_of_ge h)]
+
+theorem extract_loop_eq_aux (as bs : Array α) (size start : Nat) :
+    extract.loop as size start bs = bs ++ extract.loop as size start #[] := by
+  induction size using Nat.recAux generalizing start bs with
+  | zero => rw [extract_loop_zero, extract_loop_zero, append_nil]
+  | succ size ih =>
+    if h : start < as.size then
+      rw [extract_loop_succ (h:=h), ih (bs.push _), push_eq_append_singleton]
+      rw [extract_loop_succ (h:=h), ih (#[].push _), push_eq_append_singleton, nil_append]
+      rw [append_assoc]
+    else
+      rw [extract_loop_of_ge (h:=Nat.le_of_not_lt h)]
+      rw [extract_loop_of_ge (h:=Nat.le_of_not_lt h)]
+      rw [append_nil]
+
+theorem extract_loop_eq (as bs : Array α) (size start : Nat) (h : start + size ≤ as.size) :
+  extract.loop as size start bs = bs ++ as.extract start (start + size) := by
+  simp [extract]; rw [extract_loop_eq_aux, Nat.min_eq_left h, Nat.add_sub_cancel_left]
+
+theorem size_extract_loop (as bs : Array α) (size start : Nat) :
+    (extract.loop as size start bs).size = bs.size + min size (as.size - start) := by
+  induction size using Nat.recAux generalizing start bs with
+  | zero => rw [extract_loop_zero, Nat.zero_min, Nat.add_zero]
+  | succ size ih =>
+    if h : start < as.size then
+      rw [extract_loop_succ (h:=h), ih, size_push, Nat.add_assoc, ←Nat.add_min_add_left,
+        Nat.sub_succ, Nat.one_add, Nat.one_add, Nat.succ_pred_eq_of_pos (Nat.sub_pos_of_lt h)]
+    else
+      have h := Nat.le_of_not_gt h
+      rw [extract_loop_of_ge (h:=h), Nat.sub_eq_zero_of_le h, Nat.min_zero, Nat.add_zero]
+
+@[simp] theorem size_extract (as : Array α) (start stop : Nat) :
+    (as.extract start stop).size = min stop as.size - start := by
+  simp [extract]; rw [size_extract_loop, size_empty, Nat.zero_add, Nat.sub_min_sub_right,
+    Nat.min_assoc, Nat.min_self]
+
+theorem get_extract_loop_lt_aux (as bs : Array α) (size start : Nat) (hlt : i < bs.size) :
+    i < (extract.loop as size start bs).size := by
+  rw [size_extract_loop]
+  apply Nat.lt_of_lt_of_le hlt
+  exact Nat.le_add_right ..
+
+theorem get_extract_loop_lt (as bs : Array α) (size start : Nat) (hlt : i < bs.size)
+    (h := get_extract_loop_lt_aux as bs size start hlt) :
+    (extract.loop as size start bs)[i] = bs[i] := by
+  apply Eq.trans _ (get_append_left (bs:=extract.loop as size start #[]) hlt)
+  · rw [size_append]; exact Nat.lt_of_lt_of_le hlt (Nat.le_add_right ..)
+  · congr; rw [extract_loop_eq_aux]
+
+theorem get_extract_loop_ge_aux (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size)
+    (h : i < (extract.loop as size start bs).size) : start + i - bs.size < as.size := by
+  have h : i < bs.size + (as.size - start) := by
+      apply Nat.lt_of_lt_of_le h
+      rw [size_extract_loop]
+      apply Nat.add_le_add_left
+      exact Nat.min_le_right ..
+  rw [Nat.add_sub_assoc hge]
+  apply Nat.add_lt_of_lt_sub'
+  exact Nat.sub_lt_left_of_lt_add hge h
+
+theorem get_extract_loop_ge (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size)
+    (h : i < (extract.loop as size start bs).size)
+    (h' := get_extract_loop_ge_aux as bs size start hge h) :
+    (extract.loop as size start bs)[i] = as[start + i - bs.size] := by
+  induction size using Nat.recAux generalizing start bs with
+  | zero =>
+    rw [size_extract_loop, Nat.zero_min, Nat.add_zero] at h
+    omega
+  | succ size ih =>
+    have : start < as.size := by
+      apply Nat.lt_of_le_of_lt (Nat.le_add_right start (i - bs.size))
+      rwa [← Nat.add_sub_assoc hge]
+    have : i < (extract.loop as size (start+1) (bs.push as[start])).size := by
+      rwa [← extract_loop_succ]
+    have heq : (extract.loop as (size+1) start bs)[i] =
+        (extract.loop as size (start+1) (bs.push as[start]))[i] := by
+      congr 1; rw [extract_loop_succ]
+    rw [heq]
+    if hi : bs.size = i then
+      cases hi
+      have h₁ : bs.size < (bs.push as[start]).size := by rw [size_push]; exact Nat.lt_succ_self ..
+      have h₂ : bs.size < (extract.loop as size (start+1) (bs.push as[start])).size := by
+        rw [size_extract_loop]; apply Nat.lt_of_lt_of_le h₁; exact Nat.le_add_right ..
+      have h : (extract.loop as size (start + 1) (push bs as[start]))[bs.size] = as[start] := by
+        rw [get_extract_loop_lt as (bs.push as[start]) size (start+1) h₁ h₂, get_push_eq]
+      rw [h]; congr; rw [Nat.add_sub_cancel]
+    else
+      have hge : bs.size + 1 ≤ i := Nat.lt_of_le_of_ne hge hi
+      rw [ih (bs.push as[start]) (start+1) ((size_push ..).symm ▸ hge)]
+      congr 1; rw [size_push, Nat.add_right_comm, Nat.add_sub_add_right]
+
+theorem get_extract_aux {as : Array α} {start stop : Nat} (h : i < (as.extract start stop).size) :
+    start + i < as.size := by
+  rw [size_extract] at h; apply Nat.add_lt_of_lt_sub'; apply Nat.lt_of_lt_of_le h
+  apply Nat.sub_le_sub_right; apply Nat.min_le_right
+
+@[simp] theorem get_extract {as : Array α} {start stop : Nat}
+    (h : i < (as.extract start stop).size) :
+    (as.extract start stop)[i] = as[start + i]'(get_extract_aux h) :=
+  show (extract.loop as (min stop as.size - start) start #[])[i]
+    = as[start + i]'(get_extract_aux h) by rw [get_extract_loop_ge]; rfl; exact Nat.zero_le _
+
+@[simp] theorem extract_all (as : Array α) : as.extract 0 as.size = as := by
+  apply ext
+  · rw [size_extract, Nat.min_self, Nat.sub_zero]
+  · intros; rw [get_extract]; congr; rw [Nat.zero_add]
+
+theorem extract_empty_of_stop_le_start (as : Array α) {start stop : Nat} (h : stop ≤ start) :
+    as.extract start stop = #[] := by
+  simp [extract]; rw [←Nat.sub_min_sub_right, Nat.sub_eq_zero_of_le h, Nat.zero_min,
+    extract_loop_zero]
+
+theorem extract_empty_of_size_le_start (as : Array α) {start stop : Nat} (h : as.size ≤ start) :
+    as.extract start stop = #[] := by
+  simp [extract]; rw [←Nat.sub_min_sub_right, Nat.sub_eq_zero_of_le h, Nat.min_zero,
+    extract_loop_zero]
+
+@[simp] theorem extract_empty (start stop : Nat) : (#[] : Array α).extract start stop = #[] :=
+  extract_empty_of_size_le_start _ (Nat.zero_le _)
+
+/-! ### any -/
+
+-- Auxiliary for `any_iff_exists`.
+theorem anyM_loop_iff_exists (p : α → Bool) (as : Array α) (start stop) (h : stop ≤ as.size) :
+    anyM.loop (m := Id) p as stop h start = true ↔
+      ∃ i : Fin as.size, start ≤ ↑i ∧ ↑i < stop ∧ p as[i] = true := by
+  unfold anyM.loop
+  split <;> rename_i h₁
+  · dsimp
+    split <;> rename_i h₂
+    · simp only [true_iff]
+      refine ⟨⟨start, by omega⟩, by dsimp; omega, by dsimp; omega, h₂⟩
+    · rw [anyM_loop_iff_exists]
+      constructor
+      · rintro ⟨i, ge, lt, h⟩
+        have : start ≠ i := by rintro rfl; omega
+        exact ⟨i, by omega, lt, h⟩
+      · rintro ⟨i, ge, lt, h⟩
+        have : start ≠ i := by rintro rfl; erw [h] at h₂; simp_all
+        exact ⟨i, by omega, lt, h⟩
+  · simp
+    omega
+termination_by stop - start
+
+-- This could also be proved from `SatisfiesM_anyM_iff_exists` in `Batteries.Data.Array.Init.Monadic`
+theorem any_iff_exists (p : α → Bool) (as : Array α) (start stop) :
+    any as p start stop ↔ ∃ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop ∧ p as[i] := by
+  dsimp [any, anyM, Id.run]
+  split
+  · rw [anyM_loop_iff_exists]; rfl
+  · rw [anyM_loop_iff_exists]
+    constructor
+    · rintro ⟨i, ge, _, h⟩
+      exact ⟨i, by omega, by omega, h⟩
+    · rintro ⟨i, ge, _, h⟩
+      exact ⟨i, by omega, by omega, h⟩
+
+theorem any_eq_true (p : α → Bool) (as : Array α) :
+    any as p ↔ ∃ i : Fin as.size, p as[i] := by simp [any_iff_exists, Fin.isLt]
+
+theorem any_def {p : α → Bool} (as : Array α) : as.any p = as.data.any p := by
+  rw [Bool.eq_iff_iff, any_eq_true, List.any_eq_true]; simp only [List.mem_iff_get]
+  exact ⟨fun ⟨i, h⟩ => ⟨_, ⟨i, rfl⟩, h⟩, fun ⟨_, ⟨i, rfl⟩, h⟩ => ⟨i, h⟩⟩
+
+/-! ### all -/
+
+theorem all_eq_not_any_not (p : α → Bool) (as : Array α) (start stop) :
+    all as p start stop = !(any as (!p ·) start stop) := by
+  dsimp [all, allM]
+  rfl
+
+theorem all_iff_forall (p : α → Bool) (as : Array α) (start stop) :
+    all as p start stop ↔ ∀ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop → p as[i] := by
+  rw [all_eq_not_any_not]
+  suffices ¬(any as (!p ·) start stop = true) ↔
+      ∀ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop → p as[i] by
+    simp_all
+  rw [any_iff_exists]
+  simp
+
+theorem all_eq_true (p : α → Bool) (as : Array α) : all as p ↔ ∀ i : Fin as.size, p as[i] := by
+  simp [all_iff_forall, Fin.isLt]
+
+theorem all_def {p : α → Bool} (as : Array α) : as.all p = as.data.all p := by
+  rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true]; simp only [List.mem_iff_get]
+  constructor
+  · rintro w x ⟨r, rfl⟩
+    rw [← getElem_eq_data_get]
+    apply w
+  · intro w i
+    exact w as[i] ⟨i, (getElem_eq_data_get as i.2).symm⟩
+
+theorem all_eq_true_iff_forall_mem {l : Array α} : l.all p ↔ ∀ x, x ∈ l → p x := by
+  simp only [all_def, List.all_eq_true, mem_def]
+
+/-! ### contains -/
+
+theorem contains_def [DecidableEq α] {a : α} {as : Array α} : as.contains a ↔ a ∈ as := by
+  rw [mem_def, contains, any_def, List.any_eq_true]; simp [and_comm]
+
+instance [DecidableEq α] (a : α) (as : Array α) : Decidable (a ∈ as) :=
+  decidable_of_iff _ contains_def
+
+/-! ### swap -/
+
+open Fin
+
+@[simp] theorem get_swap_right (a : Array α) {i j : Fin a.size} : (a.swap i j)[j.val] = a[i] :=
+  by simp only [swap, fin_cast_val, get_eq_getElem, getElem_set_eq, getElem_fin]
+
+@[simp] theorem get_swap_left (a : Array α) {i j : Fin a.size} : (a.swap i j)[i.val] = a[j] :=
+  if he : ((Array.size_set _ _ _).symm ▸ j).val = i.val then by
+    simp only [←he, fin_cast_val, get_swap_right, getElem_fin]
+  else by
+    apply Eq.trans
+    · apply Array.get_set_ne
+      · simp only [size_set, Fin.isLt]
+      · assumption
+    · simp [get_set_ne]
+
+@[simp] theorem get_swap_of_ne (a : Array α) {i j : Fin a.size} (hp : p < a.size)
+    (hi : p ≠ i) (hj : p ≠ j) : (a.swap i j)[p]'(a.size_swap .. |>.symm ▸ hp) = a[p] := by
+  apply Eq.trans
+  · have : ((a.size_set i (a.get j)).symm ▸ j).val = j.val := by simp only [fin_cast_val]
+    apply Array.get_set_ne
+    · simp only [this]
+      apply Ne.symm
+      · assumption
+  · apply Array.get_set_ne
+    · apply Ne.symm
+      · assumption
+
+theorem get_swap (a : Array α) (i j : Fin a.size) (k : Nat) (hk: k < a.size) :
+    (a.swap i j)[k]'(by simp_all) = if k = i then a[j] else if k = j then a[i]  else a[k] := by
+  split
+  · simp_all only [get_swap_left]
+  · split <;> simp_all
+
+theorem get_swap' (a : Array α) (i j : Fin a.size) (k : Nat) (hk' : k < (a.swap i j).size) :
+    (a.swap i j)[k] = if k = i then a[j] else if k = j then a[i] else a[k]'(by simp_all) := by
+  apply get_swap
+
+@[simp] theorem swap_swap (a : Array α) {i j : Fin a.size} :
+    (a.swap i j).swap ⟨i.1, (a.size_swap ..).symm ▸i.2⟩ ⟨j.1, (a.size_swap ..).symm ▸j.2⟩ = a := by
+  apply ext
+  · simp only [size_swap]
+  · intros
+    simp only [get_swap']
+    split
+    · simp_all
+    · split <;> simp_all
+
+theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i := by
+  apply ext
+  · simp only [size_swap]
+  · intros
+    simp only [get_swap']
+    split
+    · split <;> simp_all
+    · split <;> simp_all
+
+
 end Array

src/Init/Data/Array/Mem.lean

@@ -27,13 +27,20 @@ theorem sizeOf_lt_of_mem [SizeOf α] {as : Array α} (h : a ∈ as) : sizeOf a <
   cases as with | _ as =>
   exact Nat.lt_trans (List.sizeOf_get ..) (by simp_arith)
 
+@[simp] theorem sizeOf_getElem [SizeOf α] (as : Array α) (i : Nat) (h : i < as.size) :
+  sizeOf (as[i]'h) < sizeOf as := sizeOf_get _ _
+
 /-- This tactic, added to the `decreasing_trivial` toolbox, proves that
 `sizeOf arr[i] < sizeOf arr`, which is useful for well founded recursions
 over a nested inductive like `inductive T | mk : Array T → T`. -/
 macro "array_get_dec" : tactic =>
   `(tactic| first
-    | apply sizeOf_get
-    | apply Nat.lt_trans (sizeOf_get ..); simp_arith)
+    -- subsumed by simp
+    -- | with_reducible apply sizeOf_get
+    -- | with_reducible apply sizeOf_getElem
+    | (with_reducible apply Nat.lt_trans (sizeOf_get ..)); simp_arith
+    | (with_reducible apply Nat.lt_trans (sizeOf_getElem ..)); simp_arith
+    )
 
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| array_get_dec)
 
@@ -43,9 +50,10 @@ provided that `a ∈ arr` which is useful for well founded recursions over a nes
 -- NB: This is analogue to tactic `sizeOf_list_dec`
 macro "array_mem_dec" : tactic =>
   `(tactic| first
-    | apply Array.sizeOf_lt_of_mem; assumption; done
-    | apply Nat.lt_trans (Array.sizeOf_lt_of_mem ?h)
-      case' h => assumption
+    | with_reducible apply Array.sizeOf_lt_of_mem; assumption; done
+    | with_reducible
+        apply Nat.lt_trans (Array.sizeOf_lt_of_mem ?h)
+        case' h => assumption
       simp_arith)
 
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| array_mem_dec)

src/Init/Data/Array/QSort.lean

@@ -27,6 +27,7 @@ def qpartition (as : Array α) (lt : α → α → Bool) (lo hi : Nat) : Nat ×
       let as := as.swap! i hi
       (i, as)
     termination_by hi - j
+    decreasing_by all_goals simp_wf; decreasing_trivial_pre_omega
   loop as lo lo
 
 @[inline] partial def qsort (as : Array α) (lt : α → α → Bool) (low := 0) (high := as.size - 1) : Array α :=

src/Init/Data/Array/Subarray.lean

@@ -15,14 +15,14 @@ structure Subarray (α : Type u)  where
   start_le_stop : start ≤ stop
   stop_le_array_size : stop ≤ array.size
 
-@[deprecated Subarray.array]
+@[deprecated Subarray.array (since := "2024-04-13")]
 abbrev Subarray.as (s : Subarray α) : Array α := s.array
 
-@[deprecated Subarray.start_le_stop]
+@[deprecated Subarray.start_le_stop (since := "2024-04-13")]
 theorem Subarray.h₁ (s : Subarray α) : s.start ≤ s.stop := s.start_le_stop
 
-@[deprecated Subarray.stop_le_array_size]
-theorem Subarray.h₂ (s : Subarray α) : s.stop ≤ s.as.size := s.stop_le_array_size
+@[deprecated Subarray.stop_le_array_size (since := "2024-04-13")]
+theorem Subarray.h₂ (s : Subarray α) : s.stop ≤ s.array.size := s.stop_le_array_size
 
 namespace Subarray
 

src/Init/Data/BitVec/Basic.lean

@@ -34,7 +34,8 @@ structure BitVec (w : Nat) where
   O(1), because we use `Fin` as the internal representation of a bitvector. -/
   toFin : Fin (2^w)
 
-@[deprecated] protected abbrev Std.BitVec := _root_.BitVec
+@[deprecated (since := "2024-04-12")]
+protected abbrev Std.BitVec := _root_.BitVec
 
 -- We manually derive the `DecidableEq` instances for `BitVec` because
 -- we want to have builtin support for bit-vector literals, and we
@@ -73,7 +74,7 @@ protected def toNat (a : BitVec n) : Nat := a.toFin.val
 /-- Return the bound in terms of toNat. -/
 theorem isLt (x : BitVec w) : x.toNat < 2^w := x.toFin.isLt
 
-@[deprecated isLt]
+@[deprecated isLt (since := "2024-03-12")]
 theorem toNat_lt (x : BitVec n) : x.toNat < 2^n := x.isLt
 
 /-- Theorem for normalizing the bit vector literal representation. -/

src/Init/Data/BitVec/Bitblast.lean

@@ -159,4 +159,43 @@ theorem add_eq_adc (w : Nat) (x y : BitVec w) : x + y = (adc x y false).snd := b
 theorem allOnes_sub_eq_not (x : BitVec w) : allOnes w - x = ~~~x := by
   rw [← add_not_self x, BitVec.add_comm, add_sub_cancel]
 
+/-! ### Negation -/
+
+theorem bit_not_testBit (x : BitVec w) (i : Fin w) :
+  getLsb (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsb i)))) ()).snd) i.val = !(getLsb x i.val) := by
+  apply iunfoldr_getLsb (fun _ => ()) i (by simp)
+
+theorem bit_not_add_self (x : BitVec w) :
+  ((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsb i)))) ()).snd + x  = -1 := by
+  simp only [add_eq_adc]
+  apply iunfoldr_replace_snd (fun _ => false) (-1) false rfl
+  intro i; simp only [ BitVec.not, adcb, testBit_toNat]
+  rw [iunfoldr_replace_snd (fun _ => ()) (((iunfoldr (fun i c => (c, !(x.getLsb i)))) ()).snd)]
+  <;> simp [bit_not_testBit, negOne_eq_allOnes, getLsb_allOnes]
+
+theorem bit_not_eq_not (x : BitVec w) :
+  ((iunfoldr (fun i c => (c, !(x.getLsb i)))) ()).snd = ~~~ x := by
+  simp [←allOnes_sub_eq_not, BitVec.eq_sub_iff_add_eq.mpr (bit_not_add_self x), ←negOne_eq_allOnes]
+
+theorem bit_neg_eq_neg (x : BitVec w) : -x = (adc (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsb i)))) ()).snd) (BitVec.ofNat w 1) false).snd:= by
+  simp only [← add_eq_adc]
+  rw [iunfoldr_replace_snd ((fun _ => ())) (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsb i)))) ()).snd) _ rfl]
+  · rw [BitVec.eq_sub_iff_add_eq.mpr (bit_not_add_self x), sub_toAdd, BitVec.add_comm _ (-x)]
+    simp [← sub_toAdd, BitVec.sub_add_cancel]
+  · simp [bit_not_testBit x _]
+
+/-! ### Inequalities (le / lt) -/
+
+theorem ult_eq_not_carry (x y : BitVec w) : x.ult y = !carry w x (~~~y) true := by
+  simp only [BitVec.ult, carry, toNat_mod_cancel, toNat_not, toNat_true, ge_iff_le, ← decide_not,
+    Nat.not_le, decide_eq_decide]
+  rw [Nat.mod_eq_of_lt (by omega)]
+  omega
+
+theorem ule_eq_not_ult (x y : BitVec w) : x.ule y = !y.ult x := by
+  simp [BitVec.ule, BitVec.ult, ← decide_not]
+
+theorem ule_eq_carry (x y : BitVec w) : x.ule y = carry w y (~~~x) true := by
+  simp [ule_eq_not_ult, ult_eq_not_carry]
+
 end BitVec

src/Init/Data/BitVec/Folds.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: Joe Hendrix
+Authors: Joe Hendrix, Harun Khan
 -/
 prelude
 import Init.Data.BitVec.Lemmas
@@ -48,6 +48,51 @@ private theorem iunfoldr.eq_test
     intro i
     simp_all [truncate_succ]
 
+theorem iunfoldr_getLsb' {f : Fin w → α → α × Bool} (state : Nat → α)
+    (ind : ∀(i : Fin w), (f i (state i.val)).fst = state (i.val+1)) :
+  (∀ i : Fin w, getLsb (iunfoldr f (state 0)).snd i.val = (f i (state i.val)).snd)
+  ∧ (iunfoldr f (state 0)).fst = state w := by
+  unfold iunfoldr
+  simp
+  apply Fin.hIterate_elim
+        (fun j (p : α × BitVec j) => (hj : j ≤ w) →
+         (∀ i : Fin j,  getLsb p.snd i.val = (f ⟨i.val, Nat.lt_of_lt_of_le i.isLt hj⟩ (state i.val)).snd)
+          ∧ p.fst = state j)
+  case hj => simp
+  case init =>
+    intro
+    apply And.intro
+    · intro i
+      have := Fin.size_pos i
+      contradiction
+    · rfl
+  case step =>
+    intro j ⟨s, v⟩ ih hj
+    apply And.intro
+    case left =>
+      intro i
+      simp only [getLsb_cons]
+      have hj2 : j.val ≤ w := by simp
+      cases (Nat.lt_or_eq_of_le (Nat.lt_succ.mp i.isLt)) with
+      | inl h3 => simp [if_neg, (Nat.ne_of_lt h3)]
+                  exact (ih hj2).1 ⟨i.val, h3⟩
+      | inr h3 => simp [h3, if_pos]
+                  cases (Nat.eq_zero_or_pos j.val) with
+                  | inl hj3 => congr
+                               rw [← (ih hj2).2]
+                  | inr hj3 => congr
+                               exact (ih hj2).2
+    case right =>
+      simp
+      have hj2 : j.val ≤ w := by simp
+      rw [← ind j, ← (ih hj2).2]
+
+
+theorem iunfoldr_getLsb {f : Fin w → α → α × Bool} (state : Nat → α) (i : Fin w)
+    (ind : ∀(i : Fin w), (f i (state i.val)).fst = state (i.val+1)) :
+  getLsb (iunfoldr f (state 0)).snd i.val = (f i (state i.val)).snd := by
+  exact (iunfoldr_getLsb' state ind).1 i
+
 /--
 Correctness theorem for `iunfoldr`.
 -/
@@ -58,4 +103,11 @@ theorem iunfoldr_replace
     iunfoldr f a = (state w, value) := by
   simp [iunfoldr.eq_test state value a init step]
 
+theorem iunfoldr_replace_snd
+  {f : Fin w → α → α × Bool} (state : Nat → α) (value : BitVec w) (a : α)
+    (init : state 0 = a)
+    (step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsb i.val)) :
+    (iunfoldr f a).snd = value := by
+  simp [iunfoldr.eq_test state value a init step]
+
 end BitVec

src/Init/Data/BitVec/Lemmas.lean

@@ -2,6 +2,7 @@
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joe Hendrix, Harun Khan, Alex Keizer, Abdalrhman M Mohamed,
+
 -/
 prelude
 import Init.Data.Bool
@@ -103,7 +104,13 @@ theorem eq_of_getMsb_eq {x y : BitVec w}
     have q := pred ⟨w - 1 - i, q_lt⟩
     simpa [q_lt, Nat.sub_sub_self, r] using q
 
-@[simp] theorem of_length_zero {x : BitVec 0} : x = 0#0 := by ext; simp
+-- This cannot be a `@[simp]` lemma, as it would be tried at every term.
+theorem of_length_zero {x : BitVec 0} : x = 0#0 := by ext; simp
+
+@[simp] theorem toNat_zero_length (x : BitVec 0) : x.toNat = 0 := by simp [of_length_zero]
+@[simp] theorem getLsb_zero_length (x : BitVec 0) : x.getLsb i = false := by simp [of_length_zero]
+@[simp] theorem getMsb_zero_length (x : BitVec 0) : x.getMsb i = false := by simp [of_length_zero]
+@[simp] theorem msb_zero_length (x : BitVec 0) : x.msb = false := by simp [BitVec.msb, of_length_zero]
 
 theorem eq_of_toFin_eq : ∀ {x y : BitVec w}, x.toFin = y.toFin → x = y
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
@@ -139,7 +146,8 @@ theorem getLsb_ofNat (n : Nat) (x : Nat) (i : Nat) :
   getLsb (x#n) i = (i < n && x.testBit i) := by
   simp [getLsb, BitVec.ofNat, Fin.val_ofNat']
 
-@[simp, deprecated toNat_ofNat] theorem toNat_zero (n : Nat) : (0#n).toNat = 0 := by trivial
+@[simp, deprecated toNat_ofNat (since := "2024-02-22")]
+theorem toNat_zero (n : Nat) : (0#n).toNat = 0 := by trivial
 
 @[simp] theorem getLsb_zero : (0#w).getLsb i = false := by simp [getLsb]
 
@@ -238,6 +246,12 @@ theorem eq_of_toInt_eq {i j : BitVec n} : i.toInt = j.toInt → i = j := by
   have _jlt := j.isLt
   split <;> split <;> omega
 
+theorem toInt_inj (x y : BitVec n) : x.toInt = y.toInt ↔ x = y :=
+  Iff.intro eq_of_toInt_eq (congrArg BitVec.toInt)
+
+theorem toInt_ne (x y : BitVec n) : x.toInt ≠ y.toInt ↔ x ≠ y  := by
+  rw [Ne, toInt_inj]
+
 @[simp] theorem toNat_ofInt {n : Nat} (i : Int) :
   (BitVec.ofInt n i).toNat = (i % (2^n : Nat)).toNat := by
   unfold BitVec.ofInt
@@ -336,7 +350,7 @@ theorem nat_eq_toNat (x : BitVec w) (y : Nat)
 @[simp] theorem getMsb_zeroExtend_add {x : BitVec w} (h : k ≤ i) :
     (x.zeroExtend (w + k)).getMsb i = x.getMsb (i - k) := by
   by_cases h : w = 0
-  · subst h; simp
+  · subst h; simp [of_length_zero]
   simp only [getMsb, getLsb_zeroExtend]
   by_cases h₁ : i < w + k <;> by_cases h₂ : i - k < w <;> by_cases h₃ : w + k - 1 - i < w + k
     <;> simp [h₁, h₂, h₃]
@@ -595,6 +609,17 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
     (shiftLeftZeroExtend x i).msb = x.msb := by
   simp [shiftLeftZeroExtend_eq, BitVec.msb]
 
+theorem shiftLeft_shiftLeft {w : Nat} (x : BitVec w) (n m : Nat) :
+    (x <<< n) <<< m = x <<< (n + m) := by
+  ext i
+  simp only [getLsb_shiftLeft, Fin.is_lt, decide_True, Bool.true_and]
+  rw [show i - (n + m) = (i - m - n) by omega]
+  cases h₂ : decide (i < m) <;>
+  cases h₃ : decide (i - m < w) <;>
+  cases h₄ : decide (i - m < n) <;>
+  cases h₅ : decide (i < n + m) <;>
+    simp at * <;> omega
+
 /-! ### ushiftRight -/
 
 @[simp, bv_toNat] theorem toNat_ushiftRight (x : BitVec n) (i : Nat) :
@@ -680,6 +705,11 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
   simp only [getLsb_append, cond_eq_if]
   split <;> simp [*]
 
+theorem shiftRight_shiftRight {w : Nat} (x : BitVec w) (n m : Nat) :
+    (x >>> n) >>> m = x >>> (n + m) := by
+  ext i
+  simp [Nat.add_assoc n m i]
+
 /-! ### rev -/
 
 theorem getLsb_rev (x : BitVec w) (i : Fin w) :
@@ -826,13 +856,18 @@ theorem ofNat_add_ofNat {n} (x y : Nat) : x#n + y#n = (x + y)#n :=
 
 protected theorem add_assoc (x y z : BitVec n) : x + y + z = x + (y + z) := by
   apply eq_of_toNat_eq ; simp [Nat.add_assoc]
+instance : Std.Associative (α := BitVec n) (· + ·) := ⟨BitVec.add_assoc⟩
 
 protected theorem add_comm (x y : BitVec n) : x + y = y + x := by
   simp [add_def, Nat.add_comm]
+instance : Std.Commutative (α := BitVec n) (· + ·) := ⟨BitVec.add_comm⟩
 
 @[simp] protected theorem add_zero (x : BitVec n) : x + 0#n = x := by simp [add_def]
 
 @[simp] protected theorem zero_add (x : BitVec n) : 0#n + x = x := by simp [add_def]
+instance : Std.LawfulIdentity (α := BitVec n) (· + ·) 0#n where
+  left_id := BitVec.zero_add
+  right_id := BitVec.add_zero
 
 theorem truncate_add (x y : BitVec w) (h : i ≤ w) :
     (x + y).truncate i = x.truncate i + y.truncate i := by
@@ -885,10 +920,19 @@ theorem sub_toAdd {n} (x y : BitVec n) : x - y = x + - y := by
 
 theorem add_sub_cancel (x y : BitVec w) : x + y - y = x := by
   apply eq_of_toNat_eq
-  have y_toNat_le := Nat.le_of_lt y.toNat_lt
+  have y_toNat_le := Nat.le_of_lt y.isLt
   rw [toNat_sub, toNat_add, Nat.mod_add_mod, Nat.add_assoc, ← Nat.add_sub_assoc y_toNat_le,
     Nat.add_sub_cancel_left, Nat.add_mod_right, toNat_mod_cancel]
 
+theorem sub_add_cancel (x y : BitVec w) : x - y + y = x := by
+  rw [sub_toAdd, BitVec.add_assoc, BitVec.add_comm _ y,
+      ← BitVec.add_assoc, ← sub_toAdd, add_sub_cancel]
+
+theorem eq_sub_iff_add_eq {x y z : BitVec w} : x = z - y ↔ x + y = z := by
+  apply Iff.intro <;> intro h
+  · simp [h, sub_add_cancel]
+  · simp [←h, add_sub_cancel]
+
 theorem negOne_eq_allOnes : -1#w = allOnes w := by
   apply eq_of_toNat_eq
   if g : w = 0 then
@@ -898,6 +942,13 @@ theorem negOne_eq_allOnes : -1#w = allOnes w := by
     have r : (2^w - 1) < 2^w := by omega
     simp [Nat.mod_eq_of_lt q, Nat.mod_eq_of_lt r]
 
+theorem neg_eq_not_add (x : BitVec w) : -x = ~~~x + 1 := by
+  apply eq_of_toNat_eq
+  simp only [toNat_neg, ofNat_eq_ofNat, toNat_add, toNat_not, toNat_ofNat, Nat.add_mod_mod]
+  congr
+  have hx : x.toNat < 2^w := x.isLt
+  rw [Nat.sub_sub, Nat.add_comm 1 x.toNat, ← Nat.sub_sub, Nat.sub_add_cancel (by omega)]
+
 /-! ### mul -/
 
 theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := by rfl

src/Init/Data/Bool.lean

@@ -74,6 +74,7 @@ Added for confluence with `not_and_self` `and_not_self` on term
 @[simp] theorem eq_false_and_eq_true_self : ∀(b : Bool), (b = false ∧ b = true) ↔ False := by decide
 
 theorem and_comm : ∀ (x y : Bool), (x && y) = (y && x) := by decide
+instance : Std.Commutative (· && ·) := ⟨and_comm⟩
 
 theorem and_left_comm : ∀ (x y z : Bool), (x && (y && z)) = (y && (x && z)) := by decide
 theorem and_right_comm : ∀ (x y z : Bool), ((x && y) && z) = ((x && z) && y) := by decide
@@ -120,6 +121,7 @@ Needed for confluence of term `(a || b) ↔ a` which reduces to `(a || b) = a` v
 @[simp] theorem iff_or_self : ∀(a b : Bool), (b = (a || b)) ↔ (a → b) := by decide
 
 theorem or_comm : ∀ (x y : Bool), (x || y) = (y || x) := by decide
+instance : Std.Commutative (· || ·) := ⟨or_comm⟩
 
 theorem or_left_comm : ∀ (x y z : Bool), (x || (y || z)) = (y || (x || z)) := by decide
 theorem or_right_comm : ∀ (x y z : Bool), ((x || y) || z) = ((x || z) || y) := by decide
@@ -186,12 +188,18 @@ in false_eq and true_eq.
 @[simp] theorem true_beq  : ∀b, (true  == b) =  b := by decide
 @[simp] theorem false_beq : ∀b, (false == b) = !b := by decide
 @[simp] theorem beq_true  : ∀b, (b == true)  =  b := by decide
+instance : Std.LawfulIdentity (· == ·) true where
+  left_id := true_beq
+  right_id := beq_true
 @[simp] theorem beq_false : ∀b, (b == false) = !b := by decide
 
 @[simp] theorem true_bne  : ∀(b : Bool), (true  != b) = !b := by decide
 @[simp] theorem false_bne : ∀(b : Bool), (false != b) =  b := by decide
 @[simp] theorem bne_true  : ∀(b : Bool), (b != true)  = !b := by decide
 @[simp] theorem bne_false : ∀(b : Bool), (b != false) =  b := by decide
+instance : Std.LawfulIdentity (· != ·) false where
+  left_id := false_bne
+  right_id := bne_false
 
 @[simp] theorem not_beq_self : ∀ (x : Bool), ((!x) == x) = false := by decide
 @[simp] theorem beq_not_self : ∀ (x : Bool), (x   == !x) = false := by decide
@@ -214,6 +222,7 @@ due to `beq_iff_eq`.
 @[simp] theorem not_bne_not : ∀ (x y : Bool), ((!x) != (!y)) = (x != y) := by decide
 
 @[simp] theorem bne_assoc : ∀ (x y z : Bool), ((x != y) != z) = (x != (y != z)) := by decide
+instance : Std.Associative (· != ·) := ⟨bne_assoc⟩
 
 @[simp] theorem bne_left_inj  : ∀ (x y z : Bool), (x != y) = (x != z) ↔ y = z := by decide
 @[simp] theorem bne_right_inj : ∀ (x y z : Bool), (x != z) = (y != z) ↔ x = y := by decide
@@ -351,7 +360,8 @@ def toNat (b:Bool) : Nat := cond b 1 0
 theorem toNat_le (c : Bool) : c.toNat ≤ 1 := by
   cases c <;> trivial
 
-@[deprecated toNat_le] abbrev toNat_le_one := toNat_le
+@[deprecated toNat_le (since := "2024-02-23")]
+abbrev toNat_le_one := toNat_le
 
 theorem toNat_lt (b : Bool) : b.toNat < 2 :=
   Nat.lt_succ_of_le (toNat_le _)

src/Init/Data/Fin/Fold.lean

@@ -12,6 +12,7 @@ import Init.Data.Nat.Linear
   loop (x : α) (i : Nat) : α :=
     if h : i < n then loop (f x ⟨i, h⟩) (i+1) else x
   termination_by n - i
+  decreasing_by decreasing_trivial_pre_omega
 
 /-- Folds over `Fin n` from the right: `foldr 3 f x = f 0 (f 1 (f 2 x))`. -/
 @[inline] def foldr (n) (f : Fin n → α → α) (init : α) : α := loop ⟨n, Nat.le_refl n⟩ init where

src/Init/Data/Fin/Iterate.lean

@@ -23,6 +23,7 @@ def hIterateFrom (P : Nat → Sort _) {n} (f : ∀(i : Fin n), P i.val → P (i.
     have p : i = n := (or_iff_left g).mp (Nat.eq_or_lt_of_le ubnd)
     _root_.cast (congrArg P p) a
   termination_by n - i
+  decreasing_by decreasing_trivial_pre_omega
 
 /--
 `hIterate` is a heterogenous iterative operation that applies a

src/Init/Data/Fin/Lemmas.lean

@@ -11,6 +11,9 @@ import Init.ByCases
 import Init.Conv
 import Init.Omega
 
+-- Remove after the next stage0 update
+set_option allowUnsafeReducibility true
+
 namespace Fin
 
 /-- If you actually have an element of `Fin n`, then the `n` is always positive -/
@@ -59,7 +62,8 @@ theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta ..
 @[simp] theorem val_ofNat' (a : Nat) (is_pos : n > 0) :
   (Fin.ofNat' a is_pos).val = a % n := rfl
 
-@[deprecated ofNat'_zero_val] theorem ofNat'_zero_val : (Fin.ofNat' 0 h).val = 0 := Nat.zero_mod _
+@[deprecated ofNat'_zero_val (since := "2024-02-22")]
+theorem ofNat'_zero_val : (Fin.ofNat' 0 h).val = 0 := Nat.zero_mod _
 
 @[simp] theorem mod_val (a b : Fin n) : (a % b).val = a.val % b.val :=
   rfl
@@ -602,6 +606,7 @@ A version of `Fin.succRec` taking `i : Fin n` as the first argument. -/
     @Fin.succRecOn (n + 1) i.succ motive zero succ = succ n i (Fin.succRecOn i zero succ) := by
   cases i; rfl
 
+
 /-- Define `motive i` by induction on `i : Fin (n + 1)` via induction on the underlying `Nat` value.
 This function has two arguments: `zero` handles the base case on `motive 0`,
 and `succ` defines the inductive step using `motive i.castSucc`.
@@ -610,8 +615,12 @@ and `succ` defines the inductive step using `motive i.castSucc`.
 @[elab_as_elim] def induction {motive : Fin (n + 1) → Sort _} (zero : motive 0)
     (succ : ∀ i : Fin n, motive (castSucc i) → motive i.succ) :
     ∀ i : Fin (n + 1), motive i
-  | ⟨0, hi⟩ => by rwa [Fin.mk_zero]
-  | ⟨i+1, hi⟩ => succ ⟨i, Nat.lt_of_succ_lt_succ hi⟩ (induction zero succ ⟨i, Nat.lt_of_succ_lt hi⟩)
+  | ⟨i, hi⟩ => go i hi
+where
+  -- Use a curried function so that this is structurally recursive
+  go : ∀ (i : Nat) (hi : i < n + 1), motive ⟨i, hi⟩
+  | 0, hi => by rwa [Fin.mk_zero]
+  | i+1, hi => succ ⟨i, Nat.lt_of_succ_lt_succ hi⟩ (go i (Nat.lt_of_succ_lt hi))
 
 @[simp] theorem induction_zero {motive : Fin (n + 1) → Sort _} (zero : motive 0)
     (hs : ∀ i : Fin n, motive (castSucc i) → motive i.succ) :
@@ -793,15 +802,20 @@ protected theorem mul_one (k : Fin (n + 1)) : k * 1 = k := by
 
 protected theorem mul_comm (a b : Fin n) : a * b = b * a :=
   ext <| by rw [mul_def, mul_def, Nat.mul_comm]
+instance : Std.Commutative (α := Fin n) (· * ·) := ⟨Fin.mul_comm⟩
 
 protected theorem mul_assoc (a b c : Fin n) : a * b * c = a * (b * c) := by
   apply eq_of_val_eq
   simp only [val_mul]
   rw [← Nat.mod_eq_of_lt a.isLt, ← Nat.mod_eq_of_lt b.isLt, ← Nat.mod_eq_of_lt c.isLt]
   simp only [← Nat.mul_mod, Nat.mul_assoc]
+instance : Std.Associative (α := Fin n) (· * ·) := ⟨Fin.mul_assoc⟩
 
 protected theorem one_mul (k : Fin (n + 1)) : (1 : Fin (n + 1)) * k = k := by
   rw [Fin.mul_comm, Fin.mul_one]
+instance : Std.LawfulIdentity (α := Fin (n + 1)) (· * ·) 1 where
+  left_id := Fin.one_mul
+  right_id := Fin.mul_one
 
 protected theorem mul_zero (k : Fin (n + 1)) : k * 0 = 0 := by simp [ext_iff, mul_def]
 

src/Init/Data/Int/DivModLemmas.lean

@@ -14,6 +14,8 @@ import Init.RCases
 # Lemmas about integer division needed to bootstrap `omega`.
 -/
 
+-- Remove after the next stage0 update
+set_option allowUnsafeReducibility true
 
 open Nat (succ)
 
@@ -142,12 +144,14 @@ theorem eq_one_of_mul_eq_one_left {a b : Int} (H : 0 ≤ b) (H' : a * b = 1) : b
   | ofNat _ => show ofNat _ = _ by simp
   | -[_+1] => show -ofNat _ = _ by simp
 
+unseal Nat.div in
 @[simp] protected theorem div_zero : ∀ a : Int, div a 0 = 0
   | ofNat _ => show ofNat _ = _ by simp
   | -[_+1] => rfl
 
 @[simp] theorem zero_fdiv (b : Int) : fdiv 0 b = 0 := by cases b <;> rfl
 
+unseal Nat.div in
 @[simp] protected theorem fdiv_zero : ∀ a : Int, fdiv a 0 = 0
   | 0      => rfl
   | succ _ => rfl
@@ -178,7 +182,7 @@ theorem fdiv_eq_div {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : fdiv a b = div a
 
 @[simp] theorem mod_zero : ∀ a : Int, mod a 0 = a
   | ofNat _ => congrArg ofNat <| Nat.mod_zero _
-  | -[_+1] => rfl
+  | -[_+1] => congrArg (fun n => -ofNat n) <| Nat.mod_zero _
 
 @[simp] theorem zero_fmod (b : Int) : fmod 0 b = 0 := by cases b <;> rfl
 
@@ -225,7 +229,9 @@ theorem mod_add_div : ∀ a b : Int, mod a b + b * (a.div b) = a
   | ofNat m, -[n+1] => by
     show (m % succ n + -↑(succ n) * -↑(m / succ n) : Int) = m
     rw [Int.neg_mul_neg]; exact congrArg ofNat (Nat.mod_add_div ..)
-  | -[_+1], 0 => rfl
+  | -[m+1], 0 => by
+    show -(↑((succ m) % 0) : Int) + 0 * -↑(succ m / 0) = -↑(succ m)
+    rw [Nat.mod_zero, Int.zero_mul, Int.add_zero]
   | -[m+1], ofNat n => by
     show -(↑((succ m) % n) : Int) + ↑n * -↑(succ m / n) = -↑(succ m)
     rw [Int.mul_neg, ← Int.neg_add]
@@ -763,11 +769,13 @@ theorem ediv_eq_ediv_of_mul_eq_mul {a b c d : Int}
   | (n:Nat) => congrArg ofNat (Nat.div_one _)
   | -[n+1] => by simp [Int.div, neg_ofNat_succ]; rfl
 
+unseal Nat.div in
 @[simp] protected theorem div_neg : ∀ a b : Int, a.div (-b) = -(a.div b)
   | ofNat m, 0 => show ofNat (m / 0) = -↑(m / 0) by rw [Nat.div_zero]; rfl
   | ofNat m, -[n+1] | -[m+1], succ n => (Int.neg_neg _).symm
   | ofNat m, succ n | -[m+1], 0 | -[m+1], -[n+1] => rfl
 
+unseal Nat.div in
 @[simp] protected theorem neg_div : ∀ a b : Int, (-a).div b = -(a.div b)
   | 0, n => by simp [Int.neg_zero]
   | succ m, (n:Nat) | -[m+1], 0 | -[m+1], -[n+1] => rfl
@@ -936,6 +944,7 @@ theorem fdiv_nonneg {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a.fdiv b :
   match a, b, eq_ofNat_of_zero_le Ha, eq_ofNat_of_zero_le Hb with
   | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => ofNat_fdiv .. ▸ ofNat_zero_le _
 
+unseal Nat.div in
 theorem fdiv_nonpos : ∀ {a b : Int}, 0 ≤ a → b ≤ 0 → a.fdiv b ≤ 0
   | 0, 0, _, _ | 0, -[_+1], _, _ | succ _, 0, _, _ | succ _, -[_+1], _, _ => ⟨_⟩
 

src/Init/Data/Int/Lemmas.lean

@@ -137,12 +137,16 @@ protected theorem add_comm : ∀ a b : Int, a + b = b + a
   | ofNat _, -[_+1]  => rfl
   | -[_+1],  ofNat _ => rfl
   | -[_+1],  -[_+1]  => by simp [Nat.add_comm]
+instance : Std.Commutative (α := Int) (· + ·) := ⟨Int.add_comm⟩
 
 @[simp] protected theorem add_zero : ∀ a : Int, a + 0 = a
   | ofNat _ => rfl
   | -[_+1]  => rfl
 
 @[simp] protected theorem zero_add (a : Int) : 0 + a = a := Int.add_comm .. ▸ a.add_zero
+instance : Std.LawfulIdentity (α := Int) (· + ·) 0 where
+  left_id := Int.zero_add
+  right_id := Int.add_zero
 
 theorem ofNat_add_negSucc_of_lt (h : m < n.succ) : ofNat m + -[n+1] = -[n - m+1] :=
   show subNatNat .. = _ by simp [succ_sub (le_of_lt_succ h), subNatNat]
@@ -196,6 +200,7 @@ where
     simp
     rw [Int.add_comm, subNatNat_add_negSucc]
     simp [Nat.add_comm, Nat.add_left_comm, Nat.add_assoc]
+instance : Std.Associative (α := Int) (· + ·) := ⟨Int.add_assoc⟩
 
 protected theorem add_left_comm (a b c : Int) : a + (b + c) = b + (a + c) := by
   rw [← Int.add_assoc, Int.add_comm a, Int.add_assoc]
@@ -351,6 +356,7 @@ protected theorem sub_right_inj (i j k : Int) : (i - k = j - k) ↔ i = j := by
 
 protected theorem mul_comm (a b : Int) : a * b = b * a := by
   cases a <;> cases b <;> simp [Nat.mul_comm]
+instance : Std.Commutative (α := Int) (· * ·) := ⟨Int.mul_comm⟩
 
 theorem ofNat_mul_negOfNat (m n : Nat) : (m : Nat) * negOfNat n = negOfNat (m * n) := by
   cases n <;> rfl
@@ -369,6 +375,7 @@ attribute [local simp] ofNat_mul_negOfNat negOfNat_mul_ofNat
 
 protected theorem mul_assoc (a b c : Int) : a * b * c = a * (b * c) := by
   cases a <;> cases b <;> cases c <;> simp [Nat.mul_assoc]
+instance : Std.Associative (α := Int) (· * ·) := ⟨Int.mul_assoc⟩
 
 protected theorem mul_left_comm (a b c : Int) : a * (b * c) = b * (a * c) := by
   rw [← Int.mul_assoc, ← Int.mul_assoc, Int.mul_comm a]
@@ -458,6 +465,9 @@ protected theorem sub_mul (a b c : Int) : (a - b) * c = a * c - b * c := by
   | -[n+1]  => show -[1 * n +1] = -[n+1] by rw [Nat.one_mul]
 
 @[simp] protected theorem mul_one (a : Int) : a * 1 = a := by rw [Int.mul_comm, Int.one_mul]
+instance : Std.LawfulIdentity (α := Int) (· * ·) 1 where
+  left_id := Int.one_mul
+  right_id := Int.mul_one
 
 protected theorem mul_neg_one (a : Int) : a * -1 = -a := by rw [Int.mul_neg, Int.mul_one]
 

src/Init/Data/Int/Order.lean

@@ -187,6 +187,7 @@ protected theorem min_comm (a b : Int) : min a b = min b a := by
   by_cases h₁ : a ≤ b <;> by_cases h₂ : b ≤ a <;> simp [h₁, h₂]
   · exact Int.le_antisymm h₁ h₂
   · cases not_or_intro h₁ h₂ <| Int.le_total ..
+instance : Std.Commutative (α := Int) min := ⟨Int.min_comm⟩
 
 protected theorem min_le_right (a b : Int) : min a b ≤ b := by rw [Int.min_def]; split <;> simp [*]
 
@@ -206,6 +207,7 @@ protected theorem max_comm (a b : Int) : max a b = max b a := by
   by_cases h₁ : a ≤ b <;> by_cases h₂ : b ≤ a <;> simp [h₁, h₂]
   · exact Int.le_antisymm h₂ h₁
   · cases not_or_intro h₁ h₂ <| Int.le_total ..
+instance : Std.Commutative (α := Int) max := ⟨Int.max_comm⟩
 
 protected theorem le_max_left (a b : Int) : a ≤ max a b := by rw [Int.max_def]; split <;> simp [*]
 

src/Init/Data/List.lean

@@ -9,3 +9,4 @@ import Init.Data.List.BasicAux
 import Init.Data.List.Control
 import Init.Data.List.Lemmas
 import Init.Data.List.Impl
+import Init.Data.List.TakeDrop

src/Init/Data/List/Basic.lean

@@ -127,6 +127,9 @@ instance : Append (List α) := ⟨List.append⟩
   | nil => rfl
   | cons a as ih =>
     simp_all [HAppend.hAppend, Append.append, List.append]
+instance : Std.LawfulIdentity (α := List α) (· ++ ·) [] where
+  left_id := nil_append
+  right_id := append_nil
 
 @[simp] theorem cons_append (a : α) (as bs : List α) : (a::as) ++ bs = a::(as ++ bs) := rfl
 
@@ -136,6 +139,7 @@ theorem append_assoc (as bs cs : List α) : (as ++ bs) ++ cs = as ++ (bs ++ cs)
   induction as with
   | nil => rfl
   | cons a as ih => simp [ih]
+instance : Std.Associative (α := List α) (· ++ ·) := ⟨append_assoc⟩
 
 theorem append_cons (as : List α) (b : α) (bs : List α) : as ++ b :: bs = as ++ [b] ++ bs := by
   induction as with

src/Init/Data/List/BasicAux.lean

@@ -5,6 +5,7 @@ Author: Leonardo de Moura
 -/
 prelude
 import Init.Data.Nat.Linear
+import Init.Ext
 
 universe u
 
@@ -43,6 +44,14 @@ See also `get?` and `get!`.
 def getD (as : List α) (i : Nat) (fallback : α) : α :=
   (as.get? i).getD fallback
 
+@[ext] theorem ext : ∀ {l₁ l₂ : List α}, (∀ n, l₁.get? n = l₂.get? n) → l₁ = l₂
+  | [], [], _ => rfl
+  | a :: l₁, [], h => nomatch h 0
+  | [], a' :: l₂, h => nomatch h 0
+  | a :: l₁, a' :: l₂, h => by
+    have h0 : some a = some a' := h 0
+    injection h0 with aa; simp only [aa, ext fun n => h (n+1)]
+
 /--
 Returns the first element in the list.
 
@@ -148,6 +157,13 @@ def getLastD : (as : List α) → (fallback : α) → α
   | [],   a₀ => a₀
   | a::as, _ => getLast (a::as) (fun h => List.noConfusion h)
 
+/--
+`O(n)`. Rotates the elements of `xs` to the left such that the element at
+`xs[i]` rotates to `xs[(i - n) % l.length]`.
+* `rotateLeft [1, 2, 3, 4, 5] 3 = [4, 5, 1, 2, 3]`
+* `rotateLeft [1, 2, 3, 4, 5] 5 = [1, 2, 3, 4, 5]`
+* `rotateLeft [1, 2, 3, 4, 5] = [2, 3, 4, 5, 1]`
+-/
 def rotateLeft (xs : List α) (n : Nat := 1) : List α :=
   let len := xs.length
   if len ≤ 1 then
@@ -158,6 +174,13 @@ def rotateLeft (xs : List α) (n : Nat := 1) : List α :=
     let e := xs.drop n
     e ++ b
 
+/--
+`O(n)`. Rotates the elements of `xs` to the right such that the element at
+`xs[i]` rotates to `xs[(i + n) % l.length]`.
+* `rotateRight [1, 2, 3, 4, 5] 3 = [3, 4, 5, 1, 2]`
+* `rotateRight [1, 2, 3, 4, 5] 5 = [1, 2, 3, 4, 5]`
+* `rotateRight [1, 2, 3, 4, 5] = [5, 1, 2, 3, 4]`
+-/
 def rotateRight (xs : List α) (n : Nat := 1) : List α :=
   let len := xs.length
   if len ≤ 1 then
@@ -203,9 +226,10 @@ theorem sizeOf_lt_of_mem [SizeOf α] {as : List α} (h : a ∈ as) : sizeOf a <
 over a nested inductive like `inductive T | mk : List T → T`. -/
 macro "sizeOf_list_dec" : tactic =>
   `(tactic| first
-    | apply sizeOf_lt_of_mem; assumption; done
-    | apply Nat.lt_trans (sizeOf_lt_of_mem ?h)
-      case' h => assumption
+    | with_reducible apply sizeOf_lt_of_mem; assumption; done
+    | with_reducible
+        apply Nat.lt_trans (sizeOf_lt_of_mem ?h)
+        case' h => assumption
       simp_arith)
 
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| sizeOf_list_dec)
@@ -288,6 +312,15 @@ def mapMono (as : List α) (f : α → α) : List α :=
 Monadic generalization of `List.partition`.
 
 This uses `Array.toList` and which isn't imported by `Init.Data.List.Basic`.
+```
+def posOrNeg (x : Int) : Except String Bool :=
+  if x > 0 then pure true
+  else if x < 0 then pure false
+  else throw "Zero is not positive or negative"
+
+partitionM posOrNeg [-1, 2, 3] = Except.ok ([2, 3], [-1])
+partitionM posOrNeg [0, 2, 3] = Except.error "Zero is not positive or negative"
+```
 -/
 @[inline] def partitionM [Monad m] (p : α → m Bool) (l : List α) : m (List α × List α) :=
   go l #[] #[]

src/Init/Data/List/TakeDrop.lean

@@ -0,0 +1,360 @@
+/-
+Copyright (c) 2014 Parikshit Khanna. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
+-/
+prelude
+import Init.Data.List.Lemmas
+import Init.Data.Nat.Lemmas
+
+/-!
+# Lemmas about `List.take`, `List.drop`, `List.zip` and `List.zipWith`.
+
+These are in a separate file from most of the list lemmas
+as they required importing more lemmas about natural numbers.
+-/
+
+namespace List
+
+open Nat
+
+/-! ### take -/
+
+abbrev take_succ_cons := @take_cons_succ
+
+@[simp] theorem length_take : ∀ (i : Nat) (l : List α), length (take i l) = min i (length l)
+  | 0, l => by simp [Nat.zero_min]
+  | succ n, [] => by simp [Nat.min_zero]
+  | succ n, _ :: l => by simp [Nat.succ_min_succ, length_take]
+
+theorem length_take_le (n) (l : List α) : length (take n l) ≤ n := by simp [Nat.min_le_left]
+
+theorem length_take_le' (n) (l : List α) : length (take n l) ≤ l.length :=
+  by simp [Nat.min_le_right]
+
+theorem length_take_of_le (h : n ≤ length l) : length (take n l) = n := by simp [Nat.min_eq_left h]
+
+theorem take_all_of_le {n} {l : List α} (h : length l ≤ n) : take n l = l :=
+  take_length_le h
+
+@[simp]
+theorem take_left : ∀ l₁ l₂ : List α, take (length l₁) (l₁ ++ l₂) = l₁
+  | [], _ => rfl
+  | a :: l₁, l₂ => congrArg (cons a) (take_left l₁ l₂)
+
+theorem take_left' {l₁ l₂ : List α} {n} (h : length l₁ = n) : take n (l₁ ++ l₂) = l₁ := by
+  rw [← h]; apply take_left
+
+theorem take_take : ∀ (n m) (l : List α), take n (take m l) = take (min n m) l
+  | n, 0, l => by rw [Nat.min_zero, take_zero, take_nil]
+  | 0, m, l => by rw [Nat.zero_min, take_zero, take_zero]
+  | succ n, succ m, nil => by simp only [take_nil]
+  | succ n, succ m, a :: l => by
+    simp only [take, succ_min_succ, take_take n m l]
+
+theorem take_replicate (a : α) : ∀ n m : Nat, take n (replicate m a) = replicate (min n m) a
+  | n, 0 => by simp [Nat.min_zero]
+  | 0, m => by simp [Nat.zero_min]
+  | succ n, succ m => by simp [succ_min_succ, take_replicate]
+
+theorem map_take (f : α → β) :
+    ∀ (L : List α) (i : Nat), (L.take i).map f = (L.map f).take i
+  | [], i => by simp
+  | _, 0 => by simp
+  | h :: t, n + 1 => by dsimp; rw [map_take f t n]
+
+/-- Taking the first `n` elements in `l₁ ++ l₂` is the same as appending the first `n` elements
+of `l₁` to the first `n - l₁.length` elements of `l₂`. -/
+theorem take_append_eq_append_take {l₁ l₂ : List α} {n : Nat} :
+    take n (l₁ ++ l₂) = take n l₁ ++ take (n - l₁.length) l₂ := by
+  induction l₁ generalizing n
+  · simp
+  · cases n
+    · simp [*]
+    · simp only [cons_append, take_cons_succ, length_cons, succ_eq_add_one, cons.injEq,
+        append_cancel_left_eq, true_and, *]
+      congr 1
+      omega
+
+theorem take_append_of_le_length {l₁ l₂ : List α} {n : Nat} (h : n ≤ l₁.length) :
+    (l₁ ++ l₂).take n = l₁.take n := by
+  simp [take_append_eq_append_take, Nat.sub_eq_zero_of_le h]
+
+/-- Taking the first `l₁.length + i` elements in `l₁ ++ l₂` is the same as appending the first
+`i` elements of `l₂` to `l₁`. -/
+theorem take_append {l₁ l₂ : List α} (i : Nat) :
+    take (l₁.length + i) (l₁ ++ l₂) = l₁ ++ take i l₂ := by
+  rw [take_append_eq_append_take, take_all_of_le (Nat.le_add_right _ _), Nat.add_sub_cancel_left]
+
+/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
+length `> i`. Version designed to rewrite from the big list to the small list. -/
+theorem get_take (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) :
+    get L ⟨i, hi⟩ = get (L.take j) ⟨i, length_take .. ▸ Nat.lt_min.mpr ⟨hj, hi⟩⟩ :=
+  get_of_eq (take_append_drop j L).symm _ ▸ get_append ..
+
+/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
+length `> i`. Version designed to rewrite from the small list to the big list. -/
+theorem get_take' (L : List α) {j i} :
+    get (L.take j) i =
+    get L ⟨i.1, Nat.lt_of_lt_of_le i.2 (length_take_le' _ _)⟩ := by
+  let ⟨i, hi⟩ := i; rw [length_take, Nat.lt_min] at hi; rw [get_take L _ hi.1]
+
+theorem get?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n).get? m = l.get? m := by
+  induction n generalizing l m with
+  | zero =>
+    exact absurd h (Nat.not_lt_of_le m.zero_le)
+  | succ _ hn =>
+    cases l with
+    | nil => simp only [take_nil]
+    | cons hd tl =>
+      cases m
+      · simp only [get?, take]
+      · simpa only using hn (Nat.lt_of_succ_lt_succ h)
+
+theorem get?_take_eq_none {l : List α} {n m : Nat} (h : n ≤ m) :
+    (l.take n).get? m = none :=
+  get?_eq_none.mpr <| Nat.le_trans (length_take_le _ _) h
+
+theorem get?_take_eq_if {l : List α} {n m : Nat} :
+    (l.take n).get? m = if m < n then l.get? m else none := by
+  split
+  · next h => exact get?_take h
+  · next h => exact get?_take_eq_none (Nat.le_of_not_lt h)
+
+@[simp]
+theorem nth_take_of_succ {l : List α} {n : Nat} : (l.take (n + 1)).get? n = l.get? n :=
+  get?_take (Nat.lt_succ_self n)
+
+theorem take_succ {l : List α} {n : Nat} : l.take (n + 1) = l.take n ++ (l.get? n).toList := by
+  induction l generalizing n with
+  | nil =>
+    simp only [Option.toList, get?, take_nil, append_nil]
+  | cons hd tl hl =>
+    cases n
+    · simp only [Option.toList, get?, eq_self_iff_true, take, nil_append]
+    · simp only [hl, cons_append, get?, eq_self_iff_true, take]
+
+@[simp]
+theorem take_eq_nil_iff {l : List α} {k : Nat} : l.take k = [] ↔ l = [] ∨ k = 0 := by
+  cases l <;> cases k <;> simp [Nat.succ_ne_zero]
+
+@[simp]
+theorem take_eq_take :
+    ∀ {l : List α} {m n : Nat}, l.take m = l.take n ↔ min m l.length = min n l.length
+  | [], m, n => by simp [Nat.min_zero]
+  | _ :: xs, 0, 0 => by simp
+  | x :: xs, m + 1, 0 => by simp [Nat.zero_min, succ_min_succ]
+  | x :: xs, 0, n + 1 => by simp [Nat.zero_min, succ_min_succ]
+  | x :: xs, m + 1, n + 1 => by simp [succ_min_succ, take_eq_take]; omega
+
+theorem take_add (l : List α) (m n : Nat) : l.take (m + n) = l.take m ++ (l.drop m).take n := by
+  suffices take (m + n) (take m l ++ drop m l) = take m l ++ take n (drop m l) by
+    rw [take_append_drop] at this
+    assumption
+  rw [take_append_eq_append_take, take_all_of_le, append_right_inj]
+  · simp only [take_eq_take, length_take, length_drop]
+    omega
+  apply Nat.le_trans (m := m)
+  · apply length_take_le
+  · apply Nat.le_add_right
+
+theorem take_eq_nil_of_eq_nil : ∀ {as : List α} {i}, as = [] → as.take i = []
+  | _, _, rfl => take_nil
+
+theorem ne_nil_of_take_ne_nil {as : List α} {i : Nat} (h: as.take i ≠ []) : as ≠ [] :=
+  mt take_eq_nil_of_eq_nil h
+
+theorem dropLast_eq_take (l : List α) : l.dropLast = l.take l.length.pred := by
+  cases l with
+  | nil => simp [dropLast]
+  | cons x l =>
+    induction l generalizing x with
+    | nil => simp [dropLast]
+    | cons hd tl hl => simp [dropLast, hl]
+
+theorem dropLast_take {n : Nat} {l : List α} (h : n < l.length) :
+    (l.take n).dropLast = l.take n.pred := by
+  simp only [dropLast_eq_take, length_take, Nat.le_of_lt h, take_take, pred_le, Nat.min_eq_left]
+
+theorem map_eq_append_split {f : α → β} {l : List α} {s₁ s₂ : List β}
+    (h : map f l = s₁ ++ s₂) : ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = s₁ ∧ map f l₂ = s₂ := by
+  have := h
+  rw [← take_append_drop (length s₁) l] at this ⊢
+  rw [map_append] at this
+  refine ⟨_, _, rfl, append_inj this ?_⟩
+  rw [length_map, length_take, Nat.min_eq_left]
+  rw [← length_map l f, h, length_append]
+  apply Nat.le_add_right
+
+/-! ### drop -/
+
+@[simp]
+theorem drop_eq_nil_iff_le {l : List α} {k : Nat} : l.drop k = [] ↔ l.length ≤ k := by
+  refine' ⟨fun h => _, drop_eq_nil_of_le⟩
+  induction k generalizing l with
+  | zero =>
+    simp only [drop] at h
+    simp [h]
+  | succ k hk =>
+    cases l
+    · simp
+    · simp only [drop] at h
+      simpa [Nat.succ_le_succ_iff] using hk h
+
+theorem drop_length_cons {l : List α} (h : l ≠ []) (a : α) :
+    (a :: l).drop l.length = [l.getLast h] := by
+  induction l generalizing a with
+  | nil =>
+    cases h rfl
+  | cons y l ih =>
+    simp only [drop, length]
+    by_cases h₁ : l = []
+    · simp [h₁]
+    rw [getLast_cons' _ h₁]
+    exact ih h₁ y
+
+/-- Dropping the elements up to `n` in `l₁ ++ l₂` is the same as dropping the elements up to `n`
+in `l₁`, dropping the elements up to `n - l₁.length` in `l₂`, and appending them. -/
+theorem drop_append_eq_append_drop {l₁ l₂ : List α} {n : Nat} :
+    drop n (l₁ ++ l₂) = drop n l₁ ++ drop (n - l₁.length) l₂ := by
+  induction l₁ generalizing n
+  · simp
+  · cases n
+    · simp [*]
+    · simp only [cons_append, drop_succ_cons, length_cons, succ_eq_add_one, append_cancel_left_eq, *]
+      congr 1
+      omega
+
+theorem drop_append_of_le_length {l₁ l₂ : List α} {n : Nat} (h : n ≤ l₁.length) :
+    (l₁ ++ l₂).drop n = l₁.drop n ++ l₂ := by
+  simp [drop_append_eq_append_drop, Nat.sub_eq_zero_of_le h]
+
+
+/-- Dropping the elements up to `l₁.length + i` in `l₁ + l₂` is the same as dropping the elements
+up to `i` in `l₂`. -/
+@[simp]
+theorem drop_append {l₁ l₂ : List α} (i : Nat) : drop (l₁.length + i) (l₁ ++ l₂) = drop i l₂ := by
+  rw [drop_append_eq_append_drop, drop_eq_nil_of_le] <;>
+    simp [Nat.add_sub_cancel_left, Nat.le_add_right]
+
+theorem drop_sizeOf_le [SizeOf α] (l : List α) (n : Nat) : sizeOf (l.drop n) ≤ sizeOf l := by
+  induction l generalizing n with
+  | nil => rw [drop_nil]; apply Nat.le_refl
+  | cons _ _ lih =>
+    induction n with
+    | zero => apply Nat.le_refl
+    | succ n =>
+      exact Trans.trans (lih _) (Nat.le_add_left _ _)
+
+theorem lt_length_drop (L : List α) {i j : Nat} (h : i + j < L.length) : j < (L.drop i).length := by
+  have A : i < L.length := Nat.lt_of_le_of_lt (Nat.le.intro rfl) h
+  rw [(take_append_drop i L).symm] at h
+  simpa only [Nat.le_of_lt A, Nat.min_eq_left, Nat.add_lt_add_iff_left, length_take,
+    length_append] using h
+
+/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
+dropping the first `i` elements. Version designed to rewrite from the big list to the small list. -/
+theorem get_drop (L : List α) {i j : Nat} (h : i + j < L.length) :
+    get L ⟨i + j, h⟩ = get (L.drop i) ⟨j, lt_length_drop L h⟩ := by
+  have : i ≤ L.length := Nat.le_trans (Nat.le_add_right _ _) (Nat.le_of_lt h)
+  rw [get_of_eq (take_append_drop i L).symm ⟨i + j, h⟩, get_append_right'] <;>
+    simp [Nat.min_eq_left this, Nat.add_sub_cancel_left, Nat.le_add_right]
+
+/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
+dropping the first `i` elements. Version designed to rewrite from the small list to the big list. -/
+theorem get_drop' (L : List α) {i j} :
+    get (L.drop i) j = get L ⟨i + j, by
+      rw [Nat.add_comm]
+      exact Nat.add_lt_of_lt_sub (length_drop i L ▸ j.2)⟩ := by
+  rw [get_drop]
+
+@[simp]
+theorem get?_drop (L : List α) (i j : Nat) : get? (L.drop i) j = get? L (i + j) := by
+  ext
+  simp only [get?_eq_some, get_drop', Option.mem_def]
+  constructor <;> intro ⟨h, ha⟩
+  · exact ⟨_, ha⟩
+  · refine ⟨?_, ha⟩
+    rw [length_drop]
+    rw [Nat.add_comm] at h
+    apply Nat.lt_sub_of_add_lt h
+
+@[simp] theorem drop_drop (n : Nat) : ∀ (m) (l : List α), drop n (drop m l) = drop (n + m) l
+  | m, [] => by simp
+  | 0, l => by simp
+  | m + 1, a :: l =>
+    calc
+      drop n (drop (m + 1) (a :: l)) = drop n (drop m l) := rfl
+      _ = drop (n + m) l := drop_drop n m l
+      _ = drop (n + (m + 1)) (a :: l) := rfl
+
+theorem take_drop : ∀ (m n : Nat) (l : List α), take n (drop m l) = drop m (take (m + n) l)
+  | 0, _, _ => by simp
+  | _, _, [] => by simp
+  | _+1, _, _ :: _ => by simpa [Nat.succ_add, take_succ_cons, drop_succ_cons] using take_drop ..
+
+theorem drop_take : ∀ (m n : Nat) (l : List α), drop n (take m l) = take (m - n) (drop n l)
+  | 0, _, _ => by simp
+  | _, 0, _ => by simp
+  | _, _, [] => by simp
+  | m+1, n+1, h :: t => by
+    simp [take_succ_cons, drop_succ_cons, drop_take m n t]
+    congr 1
+    omega
+
+theorem map_drop (f : α → β) :
+    ∀ (L : List α) (i : Nat), (L.drop i).map f = (L.map f).drop i
+  | [], i => by simp
+  | L, 0 => by simp
+  | h :: t, n + 1 => by
+    dsimp
+    rw [map_drop f t]
+
+theorem reverse_take {α} {xs : List α} (n : Nat) (h : n ≤ xs.length) :
+    xs.reverse.take n = (xs.drop (xs.length - n)).reverse := by
+  induction xs generalizing n <;>
+    simp only [reverse_cons, drop, reverse_nil, Nat.zero_sub, length, take_nil]
+  next xs_hd xs_tl xs_ih =>
+  cases Nat.lt_or_eq_of_le h with
+  | inl h' =>
+    have h' := Nat.le_of_succ_le_succ h'
+    rw [take_append_of_le_length, xs_ih _ h']
+    rw [show xs_tl.length + 1 - n = succ (xs_tl.length - n) from _, drop]
+    · rwa [succ_eq_add_one, Nat.sub_add_comm]
+    · rwa [length_reverse]
+  | inr h' =>
+    subst h'
+    rw [length, Nat.sub_self, drop]
+    suffices xs_tl.length + 1 = (xs_tl.reverse ++ [xs_hd]).length by
+      rw [this, take_length, reverse_cons]
+    rw [length_append, length_reverse]
+    rfl
+
+@[simp]
+theorem get_cons_drop : ∀ (l : List α) i, get l i :: drop (i + 1) l = drop i l
+  | _::_, ⟨0, _⟩ => rfl
+  | _::_, ⟨i+1, _⟩ => get_cons_drop _ ⟨i, _⟩
+
+theorem drop_eq_get_cons {n} {l : List α} (h) : drop n l = get l ⟨n, h⟩ :: drop (n + 1) l :=
+  (get_cons_drop _ ⟨n, h⟩).symm
+
+theorem drop_eq_nil_of_eq_nil : ∀ {as : List α} {i}, as = [] → as.drop i = []
+  | _, _, rfl => drop_nil
+
+theorem ne_nil_of_drop_ne_nil {as : List α} {i : Nat} (h: as.drop i ≠ []) : as ≠ [] :=
+  mt drop_eq_nil_of_eq_nil h
+
+/-! ### zipWith -/
+
+@[simp] theorem length_zipWith (f : α → β → γ) (l₁ l₂) :
+    length (zipWith f l₁ l₂) = min (length l₁) (length l₂) := by
+  induction l₁ generalizing l₂ <;> cases l₂ <;>
+    simp_all [succ_min_succ, Nat.zero_min, Nat.min_zero]
+
+/-! ### zip -/
+
+@[simp] theorem length_zip (l₁ : List α) (l₂ : List β) :
+    length (zip l₁ l₂) = min (length l₁) (length l₂) := by
+  simp [zip]
+
+end List

src/Init/Data/Nat/Basic.lean

@@ -137,6 +137,9 @@ instance : LawfulBEq Nat where
 @[simp] protected theorem zero_add : ∀ (n : Nat), 0 + n = n
   | 0   => rfl
   | n+1 => congrArg succ (Nat.zero_add n)
+instance : Std.LawfulIdentity (α := Nat) (· + ·) 0 where
+  left_id := Nat.zero_add
+  right_id := Nat.add_zero
 
 theorem succ_add : ∀ (n m : Nat), (succ n) + m = succ (n + m)
   | _, 0   => rfl
@@ -160,10 +163,12 @@ protected theorem add_comm : ∀ (n m : Nat), n + m = m + n
     have : succ (n + m) = succ (m + n) := by apply congrArg; apply Nat.add_comm
     rw [succ_add m n]
     apply this
+instance : Std.Commutative (α := Nat) (· + ·) := ⟨Nat.add_comm⟩
 
 protected theorem add_assoc : ∀ (n m k : Nat), (n + m) + k = n + (m + k)
   | _, _, 0      => rfl
   | n, m, succ k => congrArg succ (Nat.add_assoc n m k)
+instance : Std.Associative (α := Nat) (· + ·) := ⟨Nat.add_assoc⟩
 
 protected theorem add_left_comm (n m k : Nat) : n + (m + k) = m + (n + k) := by
   rw [← Nat.add_assoc, Nat.add_comm n m, Nat.add_assoc]
@@ -207,12 +212,16 @@ theorem succ_mul (n m : Nat) : (succ n) * m = (n * m) + m := by
 protected theorem mul_comm : ∀ (n m : Nat), n * m = m * n
   | n, 0      => (Nat.zero_mul n).symm ▸ (Nat.mul_zero n).symm ▸ rfl
   | n, succ m => (mul_succ n m).symm ▸ (succ_mul m n).symm ▸ (Nat.mul_comm n m).symm ▸ rfl
+instance : Std.Commutative (α := Nat) (· * ·) := ⟨Nat.mul_comm⟩
 
 @[simp] protected theorem mul_one : ∀ (n : Nat), n * 1 = n :=
   Nat.zero_add
 
 @[simp] protected theorem one_mul (n : Nat) : 1 * n = n :=
   Nat.mul_comm n 1 ▸ Nat.mul_one n
+instance : Std.LawfulIdentity (α := Nat) (· * ·) 1 where
+  left_id := Nat.one_mul
+  right_id := Nat.mul_one
 
 protected theorem left_distrib (n m k : Nat) : n * (m + k) = n * m + n * k := by
   induction n with
@@ -231,6 +240,7 @@ protected theorem add_mul (n m k : Nat) : (n + m) * k = n * k + m * k :=
 protected theorem mul_assoc : ∀ (n m k : Nat), (n * m) * k = n * (m * k)
   | n, m, 0      => rfl
   | n, m, succ k => by simp [mul_succ, Nat.mul_assoc n m k, Nat.left_distrib]
+instance : Std.Associative (α := Nat) (· * ·) := ⟨Nat.mul_assoc⟩
 
 protected theorem mul_left_comm (n m k : Nat) : n * (m * k) = m * (n * k) := by
   rw [← Nat.mul_assoc, Nat.mul_comm n m, Nat.mul_assoc]

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

@@ -50,7 +50,10 @@ noncomputable def div2Induction {motive : Nat → Sort u}
       apply hyp
       exact Nat.div_lt_self n_pos (Nat.le_refl _)
 
-@[simp] theorem zero_and (x : Nat) : 0 &&& x = 0 := by rfl
+@[simp] theorem zero_and (x : Nat) : 0 &&& x = 0 := by
+  simp only [HAnd.hAnd, AndOp.and, land]
+  unfold bitwise
+  simp
 
 @[simp] theorem and_zero (x : Nat) : x &&& 0 = 0 := by
   simp only [HAnd.hAnd, AndOp.and, land]
@@ -188,8 +191,6 @@ theorem lt_pow_two_of_testBit (x : Nat) (p : ∀i, i ≥ n → testBit x i = fal
   have test_false := p _ i_ge_n
   simp only [test_true] at test_false
 
-/-! ### testBit -/
-
 private theorem succ_mod_two : succ x % 2 = 1 - x % 2 := by
   induction x with
   | zero =>
@@ -233,7 +234,7 @@ theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) :
     rw [Nat.sub_eq_zero_iff_le] at i_sub_j_eq
     exact Nat.not_le_of_gt j_lt_i i_sub_j_eq
   | d+1 =>
-    simp [Nat.pow_succ, Nat.mul_comm _ 2,  Nat.mul_add_mod]
+    simp [Nat.pow_succ, Nat.mul_comm _ 2, Nat.mul_add_mod]
 
 @[simp] theorem testBit_mod_two_pow (x j i : Nat) :
     testBit (x % 2^j) i = (decide (i < j) && testBit x i) := by
@@ -257,7 +258,7 @@ theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) :
             exact Nat.lt_add_of_pos_right (Nat.two_pow_pos j)
       simp only [hyp y y_lt_x]
       if i_lt_j : i < j then
-        rw [ Nat.add_comm _ (2^_), testBit_two_pow_add_gt i_lt_j]
+        rw [Nat.add_comm _ (2^_), testBit_two_pow_add_gt i_lt_j]
       else
         simp [i_lt_j]
 
@@ -402,12 +403,12 @@ theorem and_pow_two_identity {x : Nat} (lt : x < 2^n) : x &&& 2^n-1 = x := by
 
 /-! ### lor -/
 
-@[simp] theorem or_zero (x : Nat) : 0 ||| x = x := by
+@[simp] theorem zero_or (x : Nat) : 0 ||| x = x := by
   simp only [HOr.hOr, OrOp.or, lor]
   unfold bitwise
   simp [@eq_comm _ 0]
 
-@[simp] theorem zero_or (x : Nat) : x ||| 0 = x := by
+@[simp] theorem or_zero (x : Nat) : x ||| 0 = x := by
   simp only [HOr.hOr, OrOp.or, lor]
   unfold bitwise
   simp [@eq_comm _ 0]

src/Init/Data/Nat/Div.lean

@@ -82,22 +82,34 @@ decreasing_by apply div_rec_lemma; assumption
 
 @[extern "lean_nat_mod"]
 protected def mod : @& Nat → @& Nat → Nat
-  /- This case is not needed mathematically as the case below is equal to it; however, it makes
-  `0 % n = 0` true definitionally rather than just propositionally.
-  This property is desirable for `Fin n`, as it means `(ofNat 0 : Fin n).val = 0` by definition.
-  Primarily, this is valuable because mathlib in Lean3 assumed this was true definitionally, and so
-  keeping this definitional equality makes mathlib easier to port to mathlib4. -/
+  /-
+  Nat.modCore is defined by well-founded recursion and thus irreducible. Nevertheless it is
+  desireable if trivial `Nat.mod` calculations, namely
+  * `Nat.mod 0 m` for all `m`
+  * `Nat.mod n (m+n)` for concrete literals `n`
+  reduce definitionally.
+  This property is desirable for `Fin n` literals, as it means `(ofNat 0 : Fin n).val = 0` by
+  definition.
+   -/
   | 0, _ => 0
-  | x@(_ + 1), y => Nat.modCore x y
+  | n@(_ + 1), m =>
+    if m ≤ n -- NB: if n < m does not reduce as well as `m ≤ n`!
+    then Nat.modCore n m
+    else n
 
 instance instMod : Mod Nat := ⟨Nat.mod⟩
 
-protected theorem modCore_eq_mod (x y : Nat) : Nat.modCore x y = x % y := by
-  cases x with
-  | zero =>
+protected theorem modCore_eq_mod (n m : Nat) : Nat.modCore n m = n % m := by
+  show Nat.modCore n m = Nat.mod n m
+  match n, m with
+  | 0, _ =>
     rw [Nat.modCore]
     exact if_neg fun ⟨hlt, hle⟩ => Nat.lt_irrefl _ (Nat.lt_of_lt_of_le hlt hle)
-  | succ x => rfl
+  | (_ + 1), _ =>
+    rw [Nat.mod]; dsimp
+    refine iteInduction (fun _ => rfl) (fun h => ?false) -- cannot use `split` this early yet
+    rw [Nat.modCore]
+    exact if_neg fun ⟨_hlt, hle⟩ => h hle
 
 theorem mod_eq (x y : Nat) : x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x := by
   rw [←Nat.modCore_eq_mod, ←Nat.modCore_eq_mod, Nat.modCore]

src/Init/Data/Nat/Gcd.lean

@@ -37,11 +37,11 @@ def gcd (m n : @& Nat) : Nat :=
   termination_by m
   decreasing_by simp_wf; apply mod_lt _ (zero_lt_of_ne_zero _); assumption
 
-@[simp] theorem gcd_zero_left (y : Nat) : gcd 0 y = y :=
-  rfl
+@[simp] theorem gcd_zero_left (y : Nat) : gcd 0 y = y := by
+  rw [gcd]; rfl
 
-theorem gcd_succ (x y : Nat) : gcd (succ x) y = gcd (y % succ x) (succ x) :=
-  rfl
+theorem gcd_succ (x y : Nat) : gcd (succ x) y = gcd (y % succ x) (succ x) := by
+  rw [gcd]; rfl
 
 @[simp] theorem gcd_one_left (n : Nat) : gcd 1 n = 1 := by
   rw [gcd_succ, mod_one]
@@ -54,13 +54,17 @@ theorem gcd_succ (x y : Nat) : gcd (succ x) y = gcd (y % succ x) (succ x) :=
     -- `simp [gcd_succ]` produces an invalid term unless `gcd_succ` is proved with `id rfl` instead
     rw [gcd_succ]
     exact gcd_zero_left _
+instance : Std.LawfulIdentity gcd 0 where
+  left_id := gcd_zero_left
+  right_id := gcd_zero_right
 
 @[simp] theorem gcd_self (n : Nat) : gcd n n = n := by
   cases n <;> simp [gcd_succ]
+instance : Std.IdempotentOp gcd := ⟨gcd_self⟩
 
 theorem gcd_rec (m n : Nat) : gcd m n = gcd (n % m) m :=
   match m with
-  | 0 => by have := (mod_zero n).symm; rwa [gcd_zero_right]
+  | 0 => by have := (mod_zero n).symm; rwa [gcd, gcd_zero_right]
   | _ + 1 => by simp [gcd_succ]
 
 @[elab_as_elim] theorem gcd.induction {P : Nat → Nat → Prop} (m n : Nat)
@@ -97,6 +101,7 @@ theorem gcd_comm (m n : Nat) : gcd m n = gcd n m :=
   Nat.dvd_antisymm
     (dvd_gcd (gcd_dvd_right m n) (gcd_dvd_left m n))
     (dvd_gcd (gcd_dvd_right n m) (gcd_dvd_left n m))
+instance : Std.Commutative gcd := ⟨gcd_comm⟩
 
 theorem gcd_eq_left_iff_dvd : m ∣ n ↔ gcd m n = m :=
   ⟨fun h => by rw [gcd_rec, mod_eq_zero_of_dvd h, gcd_zero_left],

src/Init/Data/Nat/Lcm.lean

@@ -14,6 +14,7 @@ def lcm (m n : Nat) : Nat := m * n / gcd m n
 
 theorem lcm_comm (m n : Nat) : lcm m n = lcm n m := by
   rw [lcm, lcm, Nat.mul_comm n m, gcd_comm n m]
+instance : Std.Commutative lcm := ⟨lcm_comm⟩
 
 @[simp] theorem lcm_zero_left (m : Nat) : lcm 0 m = 0 := by simp [lcm]
 
@@ -22,11 +23,15 @@ theorem lcm_comm (m n : Nat) : lcm m n = lcm n m := by
 @[simp] theorem lcm_one_left (m : Nat) : lcm 1 m = m := by simp [lcm]
 
 @[simp] theorem lcm_one_right (m : Nat) : lcm m 1 = m := by simp [lcm]
+instance : Std.LawfulIdentity lcm 1 where
+  left_id := lcm_one_left
+  right_id := lcm_one_right
 
 @[simp] theorem lcm_self (m : Nat) : lcm m m = m := by
   match eq_zero_or_pos m with
   | .inl h => rw [h, lcm_zero_left]
   | .inr h => simp [lcm, Nat.mul_div_cancel _ h]
+instance : Std.IdempotentOp lcm := ⟨lcm_self⟩
 
 theorem dvd_lcm_left (m n : Nat) : m ∣ lcm m n :=
   ⟨n / gcd m n, by rw [← Nat.mul_div_assoc m (Nat.gcd_dvd_right m n)]; rfl⟩
@@ -54,6 +59,7 @@ Nat.dvd_antisymm
     (Nat.dvd_trans (dvd_lcm_left m n) (dvd_lcm_left (lcm m n) k))
     (lcm_dvd (Nat.dvd_trans (dvd_lcm_right m n) (dvd_lcm_left (lcm m n) k))
       (dvd_lcm_right (lcm m n) k)))
+instance : Std.Associative lcm := ⟨lcm_assoc⟩
 
 theorem lcm_ne_zero (hm : m ≠ 0) (hn : n ≠ 0) : lcm m n ≠ 0 := by
   intro h

src/Init/Data/Nat/Lemmas.lean

@@ -137,14 +137,14 @@ protected theorem sub_le_iff_le_add' {a b c : Nat} : a - b ≤ c ↔ a ≤ b + c
 protected theorem le_sub_iff_add_le {n : Nat} (h : k ≤ m) : n ≤ m - k ↔ n + k ≤ m :=
   ⟨Nat.add_le_of_le_sub h, Nat.le_sub_of_add_le⟩
 
-@[deprecated Nat.le_sub_iff_add_le]
+@[deprecated Nat.le_sub_iff_add_le (since := "2024-02-19")]
 protected theorem add_le_to_le_sub (n : Nat) (h : m ≤ k) : n + m ≤ k ↔ n ≤ k - m :=
   (Nat.le_sub_iff_add_le h).symm
 
 protected theorem add_le_of_le_sub' {n k m : Nat} (h : m ≤ k) : n ≤ k - m → m + n ≤ k :=
   Nat.add_comm .. ▸ Nat.add_le_of_le_sub h
 
-@[deprecated Nat.add_le_of_le_sub']
+@[deprecated Nat.add_le_of_le_sub' (since := "2024-02-19")]
 protected theorem add_le_of_le_sub_left {n k m : Nat} (h : m ≤ k) : n ≤ k - m → m + n ≤ k :=
   Nat.add_le_of_le_sub' h
 
@@ -200,6 +200,7 @@ theorem succ_min_succ (x y) : min (succ x) (succ y) = succ (min x y) := by
   | inr h => rw [Nat.min_eq_right h, Nat.min_eq_right (Nat.succ_le_succ h)]
 
 @[simp] protected theorem min_self (a : Nat) : min a a = a := Nat.min_eq_left (Nat.le_refl _)
+instance : Std.IdempotentOp (α := Nat) min := ⟨Nat.min_self⟩
 
 @[simp] protected theorem zero_min (a) : min 0 a = 0 := Nat.min_eq_left (Nat.zero_le _)
 
@@ -210,6 +211,7 @@ protected theorem min_assoc : ∀ (a b c : Nat), min (min a b) c = min a (min b
   | _, 0, _ => by rw [Nat.zero_min, Nat.min_zero, Nat.zero_min]
   | _, _, 0 => by rw [Nat.min_zero, Nat.min_zero, Nat.min_zero]
   | _+1, _+1, _+1 => by simp only [Nat.succ_min_succ]; exact congrArg succ <| Nat.min_assoc ..
+instance : Std.Associative (α := Nat) min := ⟨Nat.min_assoc⟩
 
 protected theorem sub_sub_eq_min : ∀ (a b : Nat), a - (a - b) = min a b
   | 0, _ => by rw [Nat.zero_sub, Nat.zero_min]
@@ -249,16 +251,21 @@ protected theorem max_lt {a b c : Nat} : max a b < c ↔ a < c ∧ b < c := by
   rw [← Nat.succ_le, ← Nat.succ_max_succ a b]; exact Nat.max_le
 
 @[simp] protected theorem max_self (a : Nat) : max a a = a := Nat.max_eq_right (Nat.le_refl _)
+instance : Std.IdempotentOp (α := Nat) max := ⟨Nat.max_self⟩
 
 @[simp] protected theorem zero_max (a) : max 0 a = a := Nat.max_eq_right (Nat.zero_le _)
 
 @[simp] protected theorem max_zero (a) : max a 0 = a := Nat.max_eq_left (Nat.zero_le _)
+instance : Std.LawfulIdentity (α := Nat) max 0 where
+  left_id := Nat.zero_max
+  right_id := Nat.max_zero
 
 protected theorem max_assoc : ∀ (a b c : Nat), max (max a b) c = max a (max b c)
   | 0, _, _ => by rw [Nat.zero_max, Nat.zero_max]
   | _, 0, _ => by rw [Nat.zero_max, Nat.max_zero]
   | _, _, 0 => by rw [Nat.max_zero, Nat.max_zero]
   | _+1, _+1, _+1 => by simp only [Nat.succ_max_succ]; exact congrArg succ <| Nat.max_assoc ..
+instance : Std.Associative (α := Nat) max := ⟨Nat.max_assoc⟩
 
 protected theorem sub_add_eq_max (a b : Nat) : a - b + b = max a b := by
   match Nat.le_total a b with
@@ -394,11 +401,11 @@ protected theorem mul_min_mul_left (a b c : Nat) : min (a * b) (a * c) = a * min
 
 /-! ### mul -/
 
-@[deprecated Nat.mul_le_mul_left]
+@[deprecated Nat.mul_le_mul_left (since := "2024-02-19")]
 protected theorem mul_le_mul_of_nonneg_left {a b c : Nat} : a ≤ b → c * a ≤ c * b :=
   Nat.mul_le_mul_left c
 
-@[deprecated Nat.mul_le_mul_right]
+@[deprecated Nat.mul_le_mul_right (since := "2024-02-19")]
 protected theorem mul_le_mul_of_nonneg_right {a b c : Nat} : a ≤ b → a * c ≤ b * c :=
   Nat.mul_le_mul_right c
 
@@ -471,6 +478,7 @@ protected theorem mul_lt_mul_of_lt_of_lt {a b c d : Nat} (hac : a < c) (hbd : b
 
 theorem succ_mul_succ (a b) : succ a * succ b = a * b + a + b + 1 := by
   rw [succ_mul, mul_succ]; rfl
+
 theorem mul_le_add_right (m k n : Nat) : k * m ≤ m + n ↔ (k-1) * m ≤ n := by
   match k with
   | 0 =>
@@ -670,6 +678,10 @@ protected theorem pow_lt_pow_iff_right {a n m : Nat} (h : 1 < a) :
 
 /-! ### log2 -/
 
+@[simp]
+theorem log2_zero : Nat.log2 0 = 0 := by
+  simp [Nat.log2]
+
 theorem le_log2 (h : n ≠ 0) : k ≤ n.log2 ↔ 2 ^ k ≤ n := by
   match k with
   | 0 => simp [show 1 ≤ n from Nat.pos_of_ne_zero h]
@@ -690,7 +702,7 @@ theorem log2_self_le (h : n ≠ 0) : 2 ^ n.log2 ≤ n := (le_log2 h).1 (Nat.le_r
 
 theorem lt_log2_self : n < 2 ^ (n.log2 + 1) :=
   match n with
-  | 0 => Nat.zero_lt_two
+  | 0 => by simp
   | n+1 => (log2_lt n.succ_ne_zero).1 (Nat.le_refl _)
 
 /-! ### dvd -/

src/Init/Data/Nat/MinMax.lean

@@ -17,6 +17,7 @@ protected theorem min_comm (a b : Nat) : min a b = min b a := by
   | .inl h => simp [Nat.min_def, h, Nat.le_of_lt, Nat.not_le_of_lt]
   | .inr (.inl h) => simp [Nat.min_def, h]
   | .inr (.inr h) => simp [Nat.min_def, h, Nat.le_of_lt, Nat.not_le_of_lt]
+instance : Std.Commutative (α := Nat) min := ⟨Nat.min_comm⟩
 
 protected theorem min_le_right (a b : Nat) : min a b ≤ b := by
   by_cases (a <= b) <;> simp [Nat.min_def, *]
@@ -47,6 +48,7 @@ protected theorem max_comm (a b : Nat) : max a b = max b a := by
   by_cases h₁ : a ≤ b <;> by_cases h₂ : b ≤ a <;> simp [h₁, h₂]
   · exact Nat.le_antisymm h₂ h₁
   · cases not_or_intro h₁ h₂ <| Nat.le_total ..
+instance : Std.Commutative (α := Nat) max := ⟨Nat.max_comm⟩
 
 protected theorem le_max_left ( a b : Nat) : a ≤ max a b := by
   by_cases (a <= b) <;> simp [Nat.max_def, *]

src/Init/Data/Option/Basic.lean

@@ -18,18 +18,16 @@ def getM [Alternative m] : Option α → m α
   | none     => failure
   | some a   => pure a
 
-@[deprecated getM] def toMonad [Monad m] [Alternative m] : Option α → m α :=
-  getM
-
-@[inline] def toBool : Option α → Bool
-  | some _ => true
-  | none   => false
+@[deprecated getM (since := "2024-04-17")]
+def toMonad [Monad m] [Alternative m] : Option α → m α := getM
 
 /-- Returns `true` on `some x` and `false` on `none`. -/
 @[inline] def isSome : Option α → Bool
   | some _ => true
   | none   => false
 
+@[deprecated isSome, inline] def toBool : Option α → Bool := isSome
+
 /-- Returns `true` on `none` and `false` on `some x`. -/
 @[inline] def isNone : Option α → Bool
   | some _ => false

src/Init/Data/Ord.lean

@@ -182,15 +182,13 @@ instance [Ord α] : Ord (Option α) where
 
 /-- The lexicographic order on pairs. -/
 def lexOrd [Ord α] [Ord β] : Ord (α × β) where
-  compare p1 p2 := match compare p1.1 p2.1 with
-    | .eq => compare p1.2 p2.2
-    | o   => o
+  compare := compareLex (compareOn (·.1)) (compareOn (·.2))
 
 def ltOfOrd [Ord α] : LT α where
-  lt a b := compare a b == Ordering.lt
+  lt a b := compare a b = Ordering.lt
 
 instance [Ord α] : DecidableRel (@LT.lt α ltOfOrd) :=
-  inferInstanceAs (DecidableRel (fun a b => compare a b == Ordering.lt))
+  inferInstanceAs (DecidableRel (fun a b => compare a b = Ordering.lt))
 
 def leOfOrd [Ord α] : LE α where
   le a b := (compare a b).isLE

src/Init/Data/Stream.lean

@@ -94,7 +94,7 @@ instance : Stream (Subarray α) α where
   next? s :=
     if h : s.start < s.stop then
       have : s.start + 1 ≤ s.stop := Nat.succ_le_of_lt h
-      some (s.as.get ⟨s.start, Nat.lt_of_lt_of_le h s.stop_le_array_size⟩,
+      some (s.array.get ⟨s.start, Nat.lt_of_lt_of_le h s.stop_le_array_size⟩,
         { s with start := s.start + 1, start_le_stop := this })
     else
       none

src/Init/Data/String/Basic.lean

@@ -24,23 +24,59 @@ instance : LT String :=
 instance decLt (s₁ s₂ : @& String) : Decidable (s₁ < s₂) :=
   List.hasDecidableLt s₁.data s₂.data
 
+@[reducible] protected def le (a b : String) : Prop := ¬ b < a
+
+instance : LE String :=
+  ⟨String.le⟩
+
+instance decLE (s₁ s₂ : String) : Decidable (s₁ ≤ s₂) :=
+  inferInstanceAs (Decidable (Not _))
+
+/--
+Returns the length of a string in Unicode code points.
+
+Examples:
+* `"".length = 0`
+* `"abc".length = 3`
+* `"L∃∀N".length = 4`
+-/
 @[extern "lean_string_length"]
 def length : (@& String) → Nat
   | ⟨s⟩ => s.length
 
-/-- The internal implementation uses dynamic arrays and will perform destructive updates
-   if the String is not shared. -/
+/--
+Pushes a character onto the end of a string.
+
+The internal implementation uses dynamic arrays and will perform destructive updates
+if the string is not shared.
+
+Example: `"abc".push 'd' = "abcd"`
+-/
 @[extern "lean_string_push"]
 def push : String → Char → String
   | ⟨s⟩, c => ⟨s ++ [c]⟩
 
-/-- The internal implementation uses dynamic arrays and will perform destructive updates
-   if the String is not shared. -/
+/--
+Appends two strings.
+
+The internal implementation uses dynamic arrays and will perform destructive updates
+if the string is not shared.
+
+Example: `"abc".append "def" = "abcdef"`
+-/
 @[extern "lean_string_append"]
 def append : String → (@& String) → String
   | ⟨a⟩, ⟨b⟩ => ⟨a ++ b⟩
 
-/-- O(n) in the runtime, where n is the length of the String -/
+/--
+Converts a string to a list of characters.
+
+Even though the logical model of strings is as a structure that wraps a list of characters,
+this operation takes time and space linear in the length of the string, because the compiler
+uses an optimized representation as dynamic arrays.
+
+Example: `"abc".toList = ['a', 'b', 'c']`
+-/
 def toList (s : String) : List Char :=
   s.data
 
@@ -59,9 +95,17 @@ def utf8GetAux : List Char → Pos → Pos → Char
   | c::cs, i, p => if i = p then c else utf8GetAux cs (i + c) p
 
 /--
-  Return character at position `p`. If `p` is not a valid position
-  returns `(default : Char)`.
-  See `utf8GetAux` for the reference implementation.
+Returns the character at position `p` of a string. If `p` is not a valid position,
+returns `(default : Char)`.
+
+See `utf8GetAux` for the reference implementation.
+
+Examples:
+* `"abc".get ⟨1⟩ = 'b'`
+* `"abc".get ⟨3⟩ = (default : Char) = 'A'`
+
+Positions can also be invalid if a byte index points into the middle of a multi-byte UTF-8
+character. For example,`"L∃∀N".get ⟨2⟩ = (default : Char) = 'A'`.
 -/
 @[extern "lean_string_utf8_get"]
 def get (s : @& String) (p : @& Pos) : Char :=
@@ -72,12 +116,30 @@ def utf8GetAux? : List Char → Pos → Pos → Option Char
   | [],    _, _ => none
   | c::cs, i, p => if i = p then c else utf8GetAux? cs (i + c) p
 
+/--
+Returns the character at position `p`. If `p` is not a valid position, returns `none`.
+
+Examples:
+* `"abc".get? ⟨1⟩ = some 'b'`
+* `"abc".get? ⟨3⟩ = none`
+
+Positions can also be invalid if a byte index points into the middle of a multi-byte UTF-8
+character. For example, `"L∃∀N".get? ⟨2⟩ = none`
+-/
 @[extern "lean_string_utf8_get_opt"]
 def get? : (@& String) → (@& Pos) → Option Char
   | ⟨s⟩, p => utf8GetAux? s 0 p
 
 /--
-  Similar to `get`, but produces a panic error message if `p` is not a valid `String.Pos`.
+Returns the character at position `p` of a string. If `p` is not a valid position,
+returns `(default : Char)` and produces a panic error message.
+
+Examples:
+* `"abc".get! ⟨1⟩ = 'b'`
+* `"abc".get! ⟨3⟩` panics
+
+Positions can also be invalid if a byte index points into the middle of a multi-byte UTF-8 character. For example,
+`"L∃∀N".get! ⟨2⟩` panics.
 -/
 @[extern "lean_string_utf8_get_bang"]
 def get! (s : @& String) (p : @& Pos) : Char :=
@@ -89,13 +151,48 @@ def utf8SetAux (c' : Char) : List Char → Pos → Pos → List Char
   | c::cs, i, p =>
     if i = p then (c'::cs) else c::(utf8SetAux c' cs (i + c) p)
 
+/--
+Replaces the character at a specified position in a string with a new character. If the position
+is invalid, the string is returned unchanged.
+
+If both the replacement character and the replaced character are ASCII characters and the string
+is not shared, destructive updates are used.
+
+Examples:
+* `"abc".set ⟨1⟩ 'B' = "aBc"`
+* `"abc".set ⟨3⟩ 'D' = "abc"`
+* `"L∃∀N".set ⟨4⟩ 'X' = "L∃XN"`
+
+Because `'∃'` is a multi-byte character, the byte index `2` in `L∃∀N` is an invalid position,
+so `"L∃∀N".set ⟨2⟩ 'X' = "L∃∀N"`.
+-/
 @[extern "lean_string_utf8_set"]
 def set : String → (@& Pos) → Char → String
   | ⟨s⟩, i, c => ⟨utf8SetAux c s 0 i⟩
 
+/--
+Replaces the character at position `p` in the string `s` with the result of applying `f` to that character.
+If `p` is an invalid position, the string is returned unchanged.
+
+Examples:
+* `abc.modify ⟨1⟩ Char.toUpper = "aBc"`
+* `abc.modify ⟨3⟩ Char.toUpper = "abc"`
+-/
 def modify (s : String) (i : Pos) (f : Char → Char) : String :=
   s.set i <| f <| s.get i
 
+/--
+Returns the next position in a string after position `p`. If `p` is not a valid position or `p = s.endPos`,
+the result is unspecified.
+
+Examples:
+* `"abc".next ⟨1⟩ = String.Pos.mk 2`
+* `"L∃∀N".next ⟨1⟩ = String.Pos.mk 4`, since `'∃'` is a multi-byte UTF-8 character
+
+Cases where the result is unspecified:
+* `"abc".next ⟨3⟩`, since `3 = s.endPos`
+* `"L∃∀N".next ⟨2⟩`, since `2` points into the middle of a multi-byte UTF-8 character
+-/
 @[extern "lean_string_utf8_next"]
 def next (s : @& String) (p : @& Pos) : Pos :=
   let c := get s p
@@ -594,13 +691,15 @@ def substrEq (s1 : String) (off1 : String.Pos) (s2 : String) (off2 : String.Pos)
   off1.byteIdx + sz ≤ s1.endPos.byteIdx && off2.byteIdx + sz ≤ s2.endPos.byteIdx && loop off1 off2 { byteIdx := off1.byteIdx + sz }
 where
   loop (off1 off2 stop1 : Pos) :=
-    if h : off1.byteIdx < stop1.byteIdx then
+    if _h : off1.byteIdx < stop1.byteIdx then
       let c₁ := s1.get off1
       let c₂ := s2.get off2
-      have := Nat.sub_lt_sub_left h (Nat.add_lt_add_left (one_le_csize c₁) off1.1)
       c₁ == c₂ && loop (off1 + c₁) (off2 + c₂) stop1
     else true
   termination_by stop1.1 - off1.1
+  decreasing_by
+    have := Nat.sub_lt_sub_left _h (Nat.add_lt_add_left (one_le_csize c₁) off1.1)
+    decreasing_tactic
 
 /-- Return true iff `p` is a prefix of `s` -/
 def isPrefixOf (p : String) (s : String) : Bool :=

src/Init/Data/String/Extra.lean

@@ -17,13 +17,69 @@ def toNat! (s : String) : Nat :=
   else
     panic! "Nat expected"
 
+def utf8DecodeChar? (a : ByteArray) (i : Nat) : Option Char := do
+  let c ← a[i]?
+  if c &&& 0x80 == 0 then
+    some ⟨c.toUInt32, .inl (Nat.lt_trans c.1.2 (by decide))⟩
+  else if c &&& 0xe0 == 0xc0 then
+    let c1 ← a[i+1]?
+    guard (c1 &&& 0xc0 == 0x80)
+    let r := ((c &&& 0x1f).toUInt32 <<< 6) ||| (c1 &&& 0x3f).toUInt32
+    guard (0x80 ≤ r)
+    -- TODO: Prove h from the definition of r once we have the necessary lemmas
+    if h : r < 0xd800 then some ⟨r, .inl h⟩ else none
+  else if c &&& 0xf0 == 0xe0 then
+    let c1 ← a[i+1]?
+    let c2 ← a[i+2]?
+    guard (c1 &&& 0xc0 == 0x80 && c2 &&& 0xc0 == 0x80)
+    let r :=
+      ((c &&& 0x0f).toUInt32 <<< 12) |||
+      ((c1 &&& 0x3f).toUInt32 <<< 6) |||
+      (c2 &&& 0x3f).toUInt32
+    guard (0x800 ≤ r)
+    -- TODO: Prove `r < 0x110000` from the definition of r once we have the necessary lemmas
+    if h : r < 0xd800 ∨ 0xdfff < r ∧ r < 0x110000 then some ⟨r, h⟩ else none
+  else if c &&& 0xf8 == 0xf0 then
+    let c1 ← a[i+1]?
+    let c2 ← a[i+2]?
+    let c3 ← a[i+3]?
+    guard (c1 &&& 0xc0 == 0x80 && c2 &&& 0xc0 == 0x80 && c3 &&& 0xc0 == 0x80)
+    let r :=
+      ((c &&& 0x07).toUInt32 <<< 18) |||
+      ((c1 &&& 0x3f).toUInt32 <<< 12) |||
+      ((c2 &&& 0x3f).toUInt32 <<< 6) |||
+      (c3 &&& 0x3f).toUInt32
+    if h : 0x10000 ≤ r ∧ r < 0x110000 then
+      some ⟨r, .inr ⟨Nat.lt_of_lt_of_le (by decide) h.1, h.2⟩⟩
+    else none
+  else
+    none
+
 /-- Returns true if the given byte array consists of valid UTF-8. -/
 @[extern "lean_string_validate_utf8"]
-opaque validateUTF8 (a : @& ByteArray) : Bool
+def validateUTF8 (a : @& ByteArray) : Bool :=
+  (loop 0).isSome
+where
+  loop (i : Nat) : Option Unit := do
+    if i < a.size then
+      let c ← utf8DecodeChar? a i
+      loop (i + csize c)
+    else pure ()
+  termination_by a.size - i
+  decreasing_by exact Nat.sub_lt_sub_left ‹_› (Nat.lt_add_of_pos_right (one_le_csize c))
 
 /-- Converts a [UTF-8](https://en.wikipedia.org/wiki/UTF-8) encoded `ByteArray` string to `String`. -/
 @[extern "lean_string_from_utf8"]
-opaque fromUTF8 (a : @& ByteArray) (h : validateUTF8 a) : String
+def fromUTF8 (a : @& ByteArray) (h : validateUTF8 a) : String :=
+  loop 0 ""
+where
+  loop (i : Nat) (acc : String) : String :=
+    if i < a.size then
+      let c := (utf8DecodeChar? a i).getD default
+      loop (i + csize c) (acc.push c)
+    else acc
+  termination_by a.size - i
+  decreasing_by exact Nat.sub_lt_sub_left ‹_› (Nat.lt_add_of_pos_right (one_le_csize c))
 
 /-- Converts a [UTF-8](https://en.wikipedia.org/wiki/UTF-8) encoded `ByteArray` string to `String`,
 or returns `none` if `a` is not properly UTF-8 encoded. -/
@@ -35,25 +91,58 @@ or panics if `a` is not properly UTF-8 encoded. -/
 @[inline] def fromUTF8! (a : ByteArray) : String :=
   if h : validateUTF8 a then fromUTF8 a h else panic! "invalid UTF-8 string"
 
+def utf8EncodeChar (c : Char) : List UInt8 :=
+  let v := c.val
+  if v ≤ 0x7f then
+    [v.toUInt8]
+  else if v ≤ 0x7ff then
+    [(v >>>  6).toUInt8 &&& 0x1f ||| 0xc0,
+              v.toUInt8 &&& 0x3f ||| 0x80]
+  else if v ≤ 0xffff then
+    [(v >>> 12).toUInt8 &&& 0x0f ||| 0xe0,
+     (v >>>  6).toUInt8 &&& 0x3f ||| 0x80,
+              v.toUInt8 &&& 0x3f ||| 0x80]
+  else
+    [(v >>> 18).toUInt8 &&& 0x07 ||| 0xf0,
+     (v >>> 12).toUInt8 &&& 0x3f ||| 0x80,
+     (v >>>  6).toUInt8 &&& 0x3f ||| 0x80,
+              v.toUInt8 &&& 0x3f ||| 0x80]
+
+@[simp] theorem length_utf8EncodeChar (c : Char) : (utf8EncodeChar c).length = csize c := by
+  simp [csize, utf8EncodeChar, Char.utf8Size]
+  cases Decidable.em (c.val ≤ 0x7f) <;> simp [*]
+  cases Decidable.em (c.val ≤ 0x7ff) <;> simp [*]
+  cases Decidable.em (c.val ≤ 0xffff) <;> simp [*]
+
 /-- Converts the given `String` to a [UTF-8](https://en.wikipedia.org/wiki/UTF-8) encoded byte array. -/
 @[extern "lean_string_to_utf8"]
-opaque toUTF8 (a : @& String) : ByteArray
+def toUTF8 (a : @& String) : ByteArray :=
+  ⟨⟨a.data.bind utf8EncodeChar⟩⟩
+
+@[simp] theorem size_toUTF8 (s : String) : s.toUTF8.size = s.utf8ByteSize := by
+  simp [toUTF8, ByteArray.size, Array.size, utf8ByteSize, List.bind]
+  induction s.data <;> simp [List.map, List.join, utf8ByteSize.go, Nat.add_comm, *]
 
 /-- Accesses a byte in the UTF-8 encoding of the `String`. O(1) -/
 @[extern "lean_string_get_byte_fast"]
-opaque getUtf8Byte (s : @& String) (n : Nat) (h : n < s.utf8ByteSize) : UInt8
+def getUtf8Byte (s : @& String) (n : Nat) (h : n < s.utf8ByteSize) : UInt8 :=
+  (toUTF8 s).get ⟨n, size_toUTF8 _ ▸ h⟩
 
 theorem Iterator.sizeOf_next_lt_of_hasNext (i : String.Iterator) (h : i.hasNext) : sizeOf i.next < sizeOf i := by
   cases i; rename_i s pos; simp [Iterator.next, Iterator.sizeOf_eq]; simp [Iterator.hasNext] at h
   exact Nat.sub_lt_sub_left h (String.lt_next s pos)
 
-macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply String.Iterator.sizeOf_next_lt_of_hasNext; assumption)
+macro_rules
+| `(tactic| decreasing_trivial) =>
+  `(tactic| with_reducible apply String.Iterator.sizeOf_next_lt_of_hasNext; assumption)
 
 theorem Iterator.sizeOf_next_lt_of_atEnd (i : String.Iterator) (h : ¬ i.atEnd = true) : sizeOf i.next < sizeOf i :=
   have h : i.hasNext := decide_eq_true <| Nat.gt_of_not_le <| mt decide_eq_true h
   sizeOf_next_lt_of_hasNext i h
 
-macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply String.Iterator.sizeOf_next_lt_of_atEnd; assumption)
+macro_rules
+| `(tactic| decreasing_trivial) =>
+  `(tactic| with_reducible apply String.Iterator.sizeOf_next_lt_of_atEnd; assumption)
 
 namespace Iterator
 

src/Init/Grind.lean

@@ -0,0 +1,9 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Grind.Norm
+import Init.Grind.Tactics
+import Init.Grind.Lemmas

src/Init/Grind/Lemmas.lean

@@ -0,0 +1,14 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Core
+
+namespace Lean.Grind
+
+theorem intro_with_eq (p p' q : Prop) (he : p = p') (h : p' → q) : p → q :=
+  fun hp => h (he.mp hp)
+
+end Lean.Grind

src/Init/Grind/Norm.lean

@@ -0,0 +1,110 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.SimpLemmas
+import Init.Classical
+import Init.ByCases
+
+namespace Lean.Grind
+/-!
+Normalization theorems for the `grind` tactic.
+
+We are also going to use simproc's in the future.
+-/
+
+-- Not
+attribute [grind_norm] Classical.not_not
+
+-- Ne
+attribute [grind_norm] ne_eq
+
+-- Iff
+@[grind_norm] theorem iff_eq (p q : Prop) : (p ↔ q) = (p = q) := by
+  by_cases p <;> by_cases q <;> simp [*]
+
+-- Eq
+attribute [grind_norm] eq_self heq_eq_eq
+
+-- Prop equality
+@[grind_norm] theorem eq_true_eq (p : Prop) : (p = True) = p := by simp
+@[grind_norm] theorem eq_false_eq (p : Prop) : (p = False) = ¬p := by simp
+@[grind_norm] theorem not_eq_prop (p q : Prop) : (¬(p = q)) = (p = ¬q) := by
+  by_cases p <;> by_cases q <;> simp [*]
+
+-- True
+attribute [grind_norm] not_true
+
+-- False
+attribute [grind_norm] not_false_eq_true
+
+-- Implication as a clause
+@[grind_norm] theorem imp_eq (p q : Prop) : (p → q) = (¬ p ∨ q) := by
+  by_cases p <;> by_cases q <;> simp [*]
+
+-- And
+@[grind_norm↓] theorem not_and (p q : Prop) : (¬(p ∧ q)) = (¬p ∨ ¬q) := by
+  by_cases p <;> by_cases q <;> simp [*]
+attribute [grind_norm] and_true true_and and_false false_and and_assoc
+
+-- Or
+attribute [grind_norm↓] not_or
+attribute [grind_norm] or_true true_or or_false false_or or_assoc
+
+-- ite
+attribute [grind_norm] ite_true ite_false
+@[grind_norm↓] theorem not_ite {_ : Decidable p} (q r : Prop) : (¬ite p q r) = ite p (¬q) (¬r) := by
+  by_cases p <;> simp [*]
+
+-- Forall
+@[grind_norm↓] theorem not_forall (p : α → Prop) : (¬∀ x, p x) = ∃ x, ¬p x := by simp
+attribute [grind_norm] forall_and
+
+-- Exists
+@[grind_norm↓] theorem not_exists (p : α → Prop) : (¬∃ x, p x) = ∀ x, ¬p x := by simp
+attribute [grind_norm] exists_const exists_or
+
+-- Bool cond
+@[grind_norm] theorem cond_eq_ite (c : Bool) (a b : α) : cond c a b = ite c a b := by
+  cases c <;> simp [*]
+
+-- Bool or
+attribute [grind_norm]
+  Bool.or_false Bool.or_true Bool.false_or Bool.true_or Bool.or_eq_true Bool.or_assoc
+
+-- Bool and
+attribute [grind_norm]
+  Bool.and_false Bool.and_true Bool.false_and Bool.true_and Bool.and_eq_true Bool.and_assoc
+
+-- Bool not
+attribute [grind_norm]
+  Bool.not_not
+
+-- beq
+attribute [grind_norm] beq_iff_eq
+
+-- bne
+attribute [grind_norm] bne_iff_ne
+
+-- Bool not eq true/false
+attribute [grind_norm] Bool.not_eq_true Bool.not_eq_false
+
+-- decide
+attribute [grind_norm] decide_eq_true_eq decide_not not_decide_eq_true
+
+-- Nat LE
+attribute [grind_norm] Nat.le_zero_eq
+
+-- Nat/Int LT
+@[grind_norm] theorem Nat.lt_eq (a b : Nat) : (a < b) = (a + 1 ≤ b) := by
+  simp [Nat.lt, LT.lt]
+
+@[grind_norm] theorem Int.lt_eq (a b : Int) : (a < b) = (a + 1 ≤ b) := by
+  simp [Int.lt, LT.lt]
+
+-- GT GE
+attribute [grind_norm] GT.gt GE.ge
+
+end Lean.Grind

src/Init/Grind/Tactics.lean

@@ -0,0 +1,14 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Tactics
+
+namespace Lean.Grind
+/-!
+`grind` tactic and related tactics.
+-/
+
+end Lean.Grind

src/Init/Meta.lean

@@ -1057,6 +1057,7 @@ where
     else
       Syntax.mkCApp (Name.mkStr2 "Array" ("mkArray" ++ toString xs.size)) args
   termination_by xs.size - i
+  decreasing_by decreasing_trivial_pre_omega
 
 instance [Quote α `term] : Quote (Array α) `term where
   quote := quoteArray

src/Init/MetaTypes.lean

@@ -169,6 +169,11 @@ structure Config where
   That is, given a local context containing entry `x : t := e`, the free variable `x` reduces to `e`.
   -/
   zetaDelta         : Bool := false
+  /--
+  When `index` (default : `true`) is `false`, `simp` will only use the root symbol
+  to find candidate `simp` theorems. It approximates Lean 3 `simp` behavior.
+  -/
+  index             : Bool := true
   deriving Inhabited, BEq
 
 -- Configuration object for `simp_all`

src/Init/Notation.lean

@@ -296,7 +296,7 @@ macro_rules | `($x - $y)   => `(binop% HSub.hSub $x $y)
 macro_rules | `($x * $y)   => `(binop% HMul.hMul $x $y)
 macro_rules | `($x / $y)   => `(binop% HDiv.hDiv $x $y)
 macro_rules | `($x % $y)   => `(binop% HMod.hMod $x $y)
--- exponentiation should be considered a right action (#2220)
+-- exponentiation should be considered a right action (#2854)
 macro_rules | `($x ^ $y)   => `(rightact% HPow.hPow $x $y)
 macro_rules | `($x ++ $y)  => `(binop% HAppend.hAppend $x $y)
 macro_rules | `(- $x)      => `(unop% Neg.neg $x)
@@ -492,9 +492,12 @@ The attribute `@[deprecated]` on a declaration indicates that the declaration
 is discouraged for use in new code, and/or should be migrated away from in
 existing code. It may be removed in a future version of the library.
 
-`@[deprecated myBetterDef]` means that `myBetterDef` is the suggested replacement.
+* `@[deprecated myBetterDef]` means that `myBetterDef` is the suggested replacement.
+* `@[deprecated myBetterDef "use myBetterDef instead"]` allows customizing the deprecation message.
+* `@[deprecated (since := "2024-04-21")]` records when the deprecation was first applied.
 -/
-syntax (name := deprecated) "deprecated" (ppSpace ident)? : attr
+syntax (name := deprecated) "deprecated" (ppSpace ident)? (ppSpace str)?
+    (" (" &"since" " := " str ")")? : attr
 
 /--
 The `@[coe]` attribute on a function (which should also appear in a
@@ -684,4 +687,27 @@ syntax (name := checkSimp) "#check_simp " term "~>" term : command
 -/
 syntax (name := checkSimpFailure) "#check_simp " term "!~>" : command
 
+/--
+The `seal foo` command ensures that the definition of `foo` is sealed, meaning it is marked as `[irreducible]`.
+This command is particularly useful in contexts where you want to prevent the reduction of `foo` in proofs.
+
+In terms of functionality, `seal foo` is equivalent to `attribute [local irreducible] foo`.
+This attribute specifies that `foo` should be treated as irreducible only within the local scope,
+which helps in maintaining the desired abstraction level without affecting global settings.
+-/
+syntax "seal " (ppSpace ident)+ : command
+
+/--
+The `unseal foo` command ensures that the definition of `foo` is unsealed, meaning it is marked as `[semireducible]`, the
+default reducibility setting. This command is useful when you need to allow some level of reduction of `foo` in proofs.
+
+Functionally, `unseal foo` is equivalent to `attribute [local semireducible] foo`.
+Applying this attribute makes `foo` semireducible only within the local scope.
+-/
+syntax "unseal " (ppSpace ident)+ : command
+
+macro_rules
+  | `(seal $fs:ident*) => `(attribute [local irreducible] $fs:ident*)
+  | `(unseal $fs:ident*) => `(attribute [local semireducible] $fs:ident*)
+
 end Parser

src/Init/NotationExtra.lean

@@ -87,6 +87,7 @@ macro:35 xs:bracketedExplicitBinders " × " b:term:35  : term => expandBrackedBi
 macro:35 xs:bracketedExplicitBinders " ×' " b:term:35 : term => expandBrackedBinders ``PSigma xs b
 end
 
+namespace Lean
 -- first step of a `calc` block
 syntax calcFirstStep := ppIndent(colGe term (" := " term)?)
 -- enforce indentation of calc steps so we know when to stop parsing them
@@ -136,6 +137,7 @@ syntax (name := calcTactic) "calc" calcSteps : tactic
 @[inherit_doc «calc»]
 macro tk:"calc" steps:calcSteps : conv =>
   `(conv| tactic => calc%$tk $steps)
+end Lean
 
 @[app_unexpander Unit.unit] def unexpandUnit : Lean.PrettyPrinter.Unexpander
   | `($(_)) => `(())
@@ -361,6 +363,7 @@ macro_rules
   | `(letI $_:ident $_* : $_ := $_; $_) => Lean.Macro.throwUnsupported -- handled by elab
 
 
+namespace Lean
 syntax cdotTk := patternIgnore("· " <|> ". ")
 /-- `· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. -/
 syntax (name := cdot) cdotTk tacticSeqIndentGt : tactic
@@ -368,12 +371,11 @@ syntax (name := cdot) cdotTk tacticSeqIndentGt : tactic
 /--
   Similar to `first`, but succeeds only if one the given tactics solves the current goal.
 -/
-syntax (name := solve) "solve" withPosition((ppDedent(ppLine) colGe "| " tacticSeq)+) : tactic
+syntax (name := solveTactic) "solve" withPosition((ppDedent(ppLine) colGe "| " tacticSeq)+) : tactic
 
 macro_rules
   | `(tactic| solve $[| $ts]* ) => `(tactic| focus first $[| ($ts); done]*)
 
-namespace Lean
 /-! # `repeat` and `while` notation -/
 
 inductive Loop where

src/Init/Omega/Coeffs.lean

@@ -68,7 +68,7 @@ abbrev map (f : Int → Int) (xs : Coeffs) : Coeffs := List.map f xs
 /-- Shim for `.enum.find?`. -/
 abbrev findIdx? (f : Int → Bool) (xs : Coeffs) : Option Nat :=
   -- List.findIdx? f xs
-  -- We could avoid `Std.Data.List.Basic` by using the less efficient:
+  -- We could avoid `Batteries.Data.List.Basic` by using the less efficient:
   xs.enum.find? (f ·.2) |>.map (·.1)
 /-- Shim for `IntList.bmod`. -/
 abbrev bmod (x : Coeffs) (m : Nat) : Coeffs := IntList.bmod x m

src/Init/Prelude.lean

@@ -4335,8 +4335,13 @@ def addMacroScope (mainModule : Name) (n : Name) (scp : MacroScope) : Name :=
     Name.mkNum (Name.mkStr (Name.appendCore (Name.mkStr n "_@") mainModule) "_hyg") scp
 
 /--
-Append two names that may have macro scopes. The macro scopes in `b` are always erased.
-If `a` has macro scopes, then they are propagated to the result of `append a b`.
+Appends two names `a` and `b`, propagating macro scopes from `a` or `b`, if any, to the result.
+Panics if both `a` and `b` have macro scopes.
+
+This function is used for the `Append Name` instance.
+
+See also `Lean.Name.appendCore`, which appends names without any consideration for macro scopes.
+Also consider `Lean.Name.eraseMacroScopes` to erase macro scopes before appending, if appropriate.
 -/
 def Name.append (a b : Name) : Name :=
   match a.hasMacroScopes, b.hasMacroScopes with
@@ -4367,7 +4372,7 @@ def defaultMaxRecDepth := 512
 
 /-- The message to display on stack overflow. -/
 def maxRecDepthErrorMessage : String :=
-  "maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)"
+  "maximum recursion depth has been reached\nuse `set_option maxRecDepth <num>` to increase limit\nuse `set_option diagnostics true` to get diagnostic information"
 
 namespace Syntax
 

src/Init/SimpLemmas.lean

@@ -103,18 +103,26 @@ end SimprocHelperLemmas
 
 @[simp] theorem and_true (p : Prop) : (p ∧ True) = p := propext ⟨(·.1), (⟨·, trivial⟩)⟩
 @[simp] theorem true_and (p : Prop) : (True ∧ p) = p := propext ⟨(·.2), (⟨trivial, ·⟩)⟩
+instance : Std.LawfulIdentity And True where
+  left_id := true_and
+  right_id := and_true
 @[simp] theorem and_false (p : Prop) : (p ∧ False) = False := eq_false (·.2)
 @[simp] theorem false_and (p : Prop) : (False ∧ p) = False := eq_false (·.1)
 @[simp] theorem and_self (p : Prop) : (p ∧ p) = p := propext ⟨(·.left), fun h => ⟨h, h⟩⟩
+instance : Std.IdempotentOp And := ⟨and_self⟩
 @[simp] theorem and_not_self : ¬(a ∧ ¬a) | ⟨ha, hn⟩ => absurd ha hn
 @[simp] theorem not_and_self : ¬(¬a ∧ a) := and_not_self ∘ And.symm
 @[simp] theorem and_imp : (a ∧ b → c) ↔ (a → b → c) := ⟨fun h ha hb => h ⟨ha, hb⟩, fun h ⟨ha, hb⟩ => h ha hb⟩
 @[simp] theorem not_and : ¬(a ∧ b) ↔ (a → ¬b) := and_imp
 @[simp] theorem or_self (p : Prop) : (p ∨ p) = p := propext ⟨fun | .inl h | .inr h => h, .inl⟩
+instance : Std.IdempotentOp Or := ⟨or_self⟩
 @[simp] theorem or_true (p : Prop) : (p ∨ True) = True := eq_true (.inr trivial)
 @[simp] theorem true_or (p : Prop) : (True ∨ p) = True := eq_true (.inl trivial)
 @[simp] theorem or_false (p : Prop) : (p ∨ False) = p := propext ⟨fun (.inl h) => h, .inl⟩
 @[simp] theorem false_or (p : Prop) : (False ∨ p) = p := propext ⟨fun (.inr h) => h, .inr⟩
+instance : Std.LawfulIdentity Or False where
+  left_id := false_or
+  right_id := or_false
 @[simp] theorem iff_self (p : Prop) : (p ↔ p) = True := eq_true .rfl
 @[simp] theorem iff_true (p : Prop) : (p ↔ True) = p := propext ⟨(·.2 trivial), fun h => ⟨fun _ => trivial, fun _ => h⟩⟩
 @[simp] theorem true_iff (p : Prop) : (True ↔ p) = p := propext ⟨(·.1 trivial), fun h => ⟨fun _ => h, fun _ => trivial⟩⟩
@@ -140,6 +148,7 @@ theorem and_congr_left (h : c → (a ↔ b)) : a ∧ c ↔ b ∧ c :=
 theorem and_assoc : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) :=
   Iff.intro (fun ⟨⟨ha, hb⟩, hc⟩ => ⟨ha, hb, hc⟩)
             (fun ⟨ha, hb, hc⟩ => ⟨⟨ha, hb⟩, hc⟩)
+instance : Std.Associative And := ⟨fun _ _ _ => propext and_assoc⟩
 
 @[simp] theorem and_self_left  : a ∧ (a ∧ b) ↔ a ∧ b := by rw [←propext and_assoc, and_self]
 @[simp] theorem and_self_right : (a ∧ b) ∧ b ↔ a ∧ b := by rw [ propext and_assoc, and_self]
@@ -167,6 +176,7 @@ theorem Or.imp_right (f : b → c) : a ∨ b → a ∨ c := .imp id f
 theorem or_assoc : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) :=
   Iff.intro (.rec (.imp_right .inl) (.inr ∘ .inr))
             (.rec (.inl ∘ .inl) (.imp_left .inr))
+instance : Std.Associative Or := ⟨fun _ _ _ => propext or_assoc⟩
 
 @[simp] theorem or_self_left  : a ∨ (a ∨ b) ↔ a ∨ b := by rw [←propext or_assoc, or_self]
 @[simp] theorem or_self_right : (a ∨ b) ∨ b ↔ a ∨ b := by rw [ propext or_assoc, or_self]
@@ -187,8 +197,12 @@ theorem or_iff_left_of_imp  (hb : b → a) : (a ∨ b) ↔ a  := Iff.intro (Or.r
 @[simp] theorem Bool.or_false (b : Bool) : (b || false) = b  := by cases b <;> rfl
 @[simp] theorem Bool.or_true (b : Bool) : (b || true) = true := by cases b <;> rfl
 @[simp] theorem Bool.false_or (b : Bool) : (false || b) = b  := by cases b <;> rfl
+instance : Std.LawfulIdentity (· || ·) false where
+  left_id := Bool.false_or
+  right_id := Bool.or_false
 @[simp] theorem Bool.true_or (b : Bool) : (true || b) = true := by cases b <;> rfl
 @[simp] theorem Bool.or_self (b : Bool) : (b || b) = b       := by cases b <;> rfl
+instance : Std.IdempotentOp (· || ·) := ⟨Bool.or_self⟩
 @[simp] theorem Bool.or_eq_true (a b : Bool) : ((a || b) = true) = (a = true ∨ b = true) := by
   cases a <;> cases b <;> decide
 
@@ -196,14 +210,20 @@ theorem or_iff_left_of_imp  (hb : b → a) : (a ∨ b) ↔ a  := Iff.intro (Or.r
 @[simp] theorem Bool.and_true (b : Bool) : (b && true) = b       := by cases b <;> rfl
 @[simp] theorem Bool.false_and (b : Bool) : (false && b) = false := by cases b <;> rfl
 @[simp] theorem Bool.true_and (b : Bool) : (true && b) = b       := by cases b <;> rfl
+instance : Std.LawfulIdentity (· && ·) true where
+  left_id := Bool.true_and
+  right_id := Bool.and_true
 @[simp] theorem Bool.and_self (b : Bool) : (b && b) = b          := by cases b <;> rfl
+instance : Std.IdempotentOp (· && ·) := ⟨Bool.and_self⟩
 @[simp] theorem Bool.and_eq_true (a b : Bool) : ((a && b) = true) = (a = true ∧ b = true) := by
   cases a <;> cases b <;> decide
 
 theorem Bool.and_assoc (a b c : Bool) : (a && b && c) = (a && (b && c)) := by
   cases a <;> cases b <;> cases c <;> decide
+instance : Std.Associative (· && ·) := ⟨Bool.and_assoc⟩
 theorem Bool.or_assoc (a b c : Bool) : (a || b || c) = (a || (b || c)) := by
   cases a <;> cases b <;> cases c <;> decide
+instance : Std.Associative (· || ·) := ⟨Bool.or_assoc⟩
 
 @[simp] theorem Bool.not_not (b : Bool) : (!!b) = b := by cases b <;> rfl
 @[simp] theorem Bool.not_true  : (!true) = false := by decide

src/Init/System/IO.lean

@@ -210,8 +210,44 @@ def sleep (ms : UInt32) : BaseIO Unit :=
 /-- Request cooperative cancellation of the task. The task must explicitly call `IO.checkCanceled` to react to the cancellation. -/
 @[extern "lean_io_cancel"] opaque cancel : @& Task α → BaseIO Unit
 
+/-- The current state of a `Task` in the Lean runtime's task manager. -/
+inductive TaskState
+  /--
+  The `Task` is waiting to be run.
+  It can be waiting for dependencies to complete or
+  sitting in the task manager queue waiting for a thread to run on.
+  -/
+  | waiting
+  /--
+  The `Task` is actively running on a thread or,
+  in the case of a `Promise`, waiting for a call to `IO.Promise.resolve`.
+  -/
+  | running
+  /--
+  The `Task` has finished running and its result is available.
+  Calling `Task.get` or `IO.wait` on the task will not block.
+  -/
+  | finished
+  deriving Inhabited, Repr, DecidableEq, Ord
+
+instance : LT TaskState := ltOfOrd
+instance : LE TaskState := leOfOrd
+instance : Min TaskState := minOfLe
+instance : Max TaskState := maxOfLe
+
+protected def TaskState.toString : TaskState → String
+  | .waiting => "waiting"
+  | .running => "running"
+  | .finished => "finished"
+
+instance : ToString TaskState := ⟨TaskState.toString⟩
+
+/-- Returns current state of the `Task` in the Lean runtime's task manager. -/
+@[extern "lean_io_get_task_state"] opaque getTaskState : @& Task α → BaseIO TaskState
+
 /-- Check if the task has finished execution, at which point calling `Task.get` will return immediately. -/
-@[extern "lean_io_has_finished"] opaque hasFinished : @& Task α → BaseIO Bool
+@[inline] def hasFinished (task : Task α) : BaseIO Bool := do
+  return (← getTaskState task) matches .finished
 
 /-- Wait for the task to finish, then return its result. -/
 @[extern "lean_io_wait"] opaque wait (t : Task α) : BaseIO α :=
@@ -625,7 +661,13 @@ partial def FS.removeDirAll (p : FilePath) : IO Unit := do
 
 namespace Process
 
-/-- Returns the process ID of the current process. -/
+/-- Returns the current working directory of the calling process. -/
+@[extern "lean_io_process_get_current_dir"] opaque getCurrentDir : IO FilePath
+
+/-- Sets the current working directory of the calling process. -/
+@[extern "lean_io_process_set_current_dir"] opaque setCurrentDir (path : @& FilePath) : IO Unit
+
+/-- Returns the process ID of the calling process. -/
 @[extern "lean_io_process_get_pid"] opaque getPID : BaseIO UInt32
 
 inductive Stdio where

src/Init/Tactics.lean

@@ -368,7 +368,7 @@ for new reflexive relations.
 Remark: `rfl` is an extensible tactic. We later add `macro_rules` to try different
 reflexivity theorems (e.g., `Iff.rfl`).
 -/
-macro "rfl" : tactic => `(tactic| fail "The rfl tactic failed. Possible reasons:
+macro "rfl" : tactic => `(tactic| case' _ => fail "The rfl tactic failed. Possible reasons:
 - The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
 - The arguments of the relation are not equal.
 Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.")
@@ -835,7 +835,7 @@ syntax (name := renameI) "rename_i" (ppSpace colGt binderIdent)+ : tactic
 /--
 `repeat tac` repeatedly applies `tac` to the main goal until it fails.
 That is, if `tac` produces multiple subgoals, only subgoals up to the first failure will be visited.
-The `Std` library provides `repeat'` which repeats separately in each subgoal.
+The `Batteries` library provides `repeat'` which repeats separately in each subgoal.
 -/
 syntax "repeat " tacticSeq : tactic
 macro_rules
@@ -1125,11 +1125,14 @@ normalizes `h` with `norm_cast` and tries to use that to close the goal. -/
 macro "assumption_mod_cast" : tactic => `(tactic| norm_cast0 at * <;> assumption)
 
 /--
-The `norm_cast` family of tactics is used to normalize casts inside expressions.
-It is basically a `simp` tactic with a specific set of lemmas to move casts
+The `norm_cast` family of tactics is used to normalize certain coercions (*casts*) in expressions.
+- `norm_cast` normalizes casts in the target.
+- `norm_cast at h` normalizes casts in hypothesis `h`.
+
+The tactic is basically a version of `simp` with a specific set of lemmas to move casts
 upwards in the expression.
 Therefore even in situations where non-terminal `simp` calls are discouraged (because of fragility),
-`norm_cast` is considered safe.
+`norm_cast` is considered to be safe.
 It also has special handling of numerals.
 
 For instance, given an assumption
@@ -1137,22 +1140,22 @@ For instance, given an assumption
 a b : ℤ
 h : ↑a + ↑b < (10 : ℚ)
 ```
-
 writing `norm_cast at h` will turn `h` into
 ```lean
 h : a + b < 10
 ```
 
-There are also variants of `exact`, `apply`, `rw`, and `assumption` that
-work modulo `norm_cast` - in other words, they apply `norm_cast` to make
-them more flexible. They are called `exact_mod_cast`, `apply_mod_cast`,
-`rw_mod_cast`, and `assumption_mod_cast`, respectively.
-Writing `exact_mod_cast h` and `apply_mod_cast h` will normalize casts
-in the goal and `h` before using `exact h` or `apply h`.
-Writing `assumption_mod_cast` will normalize casts in the goal and, for
-every hypothesis `h` in the context, it will try to normalize casts in `h` and use
-`exact h`.
-`rw_mod_cast` acts like the `rw` tactic but it applies `norm_cast` between steps.
+There are also variants of basic tactics that use `norm_cast` to normalize expressions during
+their operation, to make them more flexible about the expressions they accept
+(we say that it is a tactic *modulo* the effects of `norm_cast`):
+- `exact_mod_cast` for `exact` and `apply_mod_cast` for `apply`.
+  Writing `exact_mod_cast h` and `apply_mod_cast h` will normalize casts
+  in the goal and `h` before using `exact h` or `apply h`.
+- `rw_mod_cast` for `rw`. It applies `norm_cast` between rewrites.
+- `assumption_mod_cast` for `assumption`.
+  This is effectively `norm_cast at *; assumption`, but more efficient.
+  It normalizes casts in the goal and, for every hypothesis `h` in the context,
+  it will try to normalize casts in `h` and use `exact h`.
 
 See also `push_cast`, which moves casts inwards rather than lifting them outwards.
 -/
@@ -1160,22 +1163,37 @@ macro "norm_cast" loc:(location)? : tactic =>
   `(tactic| norm_cast0 $[$loc]? <;> try trivial)
 
 /--
-`push_cast` rewrites the goal to move casts inward, toward the leaf nodes.
+`push_cast` rewrites the goal to move certain coercions (*casts*) inward, toward the leaf nodes.
 This uses `norm_cast` lemmas in the forward direction.
 For example, `↑(a + b)` will be written to `↑a + ↑b`.
-It is equivalent to `simp only with push_cast`.
-It can also be used at hypotheses with `push_cast at h`
-and with extra simp lemmas with `push_cast [int.add_zero]`.
+- `push_cast` moves casts inward in the goal.
+- `push_cast at h` moves casts inward in the hypothesis `h`.
+It can be used with extra simp lemmas with, for example, `push_cast [Int.add_zero]`.
 
+Example:
 ```lean
-example (a b : ℕ) (h1 : ((a + b : ℕ) : ℤ) = 10) (h2 : ((a + b + 0 : ℕ) : ℤ) = 10) :
-  ((a + b : ℕ) : ℤ) = 10 :=
-begin
-  push_cast,
-  push_cast at h1,
-  push_cast [int.add_zero] at h2,
-end
+example (a b : Nat)
+    (h1 : ((a + b : Nat) : Int) = 10)
+    (h2 : ((a + b + 0 : Nat) : Int) = 10) :
+    ((a + b : Nat) : Int) = 10 := by
+  /-
+  h1 : ↑(a + b) = 10
+  h2 : ↑(a + b + 0) = 10
+  ⊢ ↑(a + b) = 10
+  -/
+  push_cast
+  /- Now
+  ⊢ ↑a + ↑b = 10
+  -/
+  push_cast at h1
+  push_cast [Int.add_zero] at h2
+  /- Now
+  h1 h2 : ↑a + ↑b = 10
+  -/
+  exact h1
 ```
+
+See also `norm_cast`.
 -/
 syntax (name := pushCast) "push_cast" (config)? (discharger)? (&" only")?
   (" [" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic
@@ -1248,7 +1266,7 @@ Optional arguments passed via a configuration argument as `solve_by_elim (config
   but it is often useful to change to `.reducible`,
   so semireducible definitions will not be unfolded when trying to apply a lemma.
 
-See also the doc-comment for `Std.Tactic.BacktrackConfig` for the options
+See also the doc-comment for `Lean.Meta.Tactic.Backtrack.BacktrackConfig` for the options
 `proc`, `suspend`, and `discharge` which allow further customization of `solve_by_elim`.
 Both `apply_assumption` and `apply_rules` are implemented via these hooks.
 -/
@@ -1407,6 +1425,16 @@ If there are several with the same priority, it is uses the "most recent one". E
 -/
 syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? (ppSpace prio)? : attr
 
+/--
+Theorems tagged with the `grind_norm` attribute are used by the `grind` tactic normalizer/pre-processor.
+-/
+syntax (name := grind_norm) "grind_norm" (Tactic.simpPre <|> Tactic.simpPost)? (ppSpace prio)? : attr
+
+/--
+Simplification procedures tagged with the `grind_norm_proc` attribute are used by the `grind` tactic normalizer/pre-processor.
+-/
+syntax (name := grind_norm_proc) "grind_norm_proc" (Tactic.simpPre <|> Tactic.simpPost)? : attr
+
 
 /-- The possible `norm_cast` kinds: `elim`, `move`, or `squash`. -/
 syntax normCastLabel := &"elim" <|> &"move" <|> &"squash"
@@ -1524,7 +1552,7 @@ macro "get_elem_tactic" : tactic =>
 
 /--
 Searches environment for definitions or theorems that can be substituted in
-for `exact?% to solve the goal.
+for `exact?%` to solve the goal.
  -/
 syntax (name := Lean.Parser.Syntax.exact?) "exact?%" : term
 

src/Init/WFTactics.lean

@@ -25,9 +25,16 @@ syntax "decreasing_trivial" : tactic
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| (simp (config := { arith := true, failIfUnchanged := false })) <;> done)
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| omega)
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| assumption)
-macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.sub_succ_lt_self; assumption) -- a - (i+1) < a - i if i < a
-macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.pred_lt'; assumption) -- i-1 < i if j < i
-macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.pred_lt; assumption)  -- i-1 < i if i ≠ 0
+
+/--
+Variant of `decreasing_trivial` that does not use `omega`, intended to be used in core modules
+before `omega` is available.
+-/
+syntax "decreasing_trivial_pre_omega" : tactic
+macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.sub_succ_lt_self; assumption) -- a - (i+1) < a - i if i < a
+macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.pred_lt'; assumption) -- i-1 < i if j < i
+macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.pred_lt; assumption)  -- i-1 < i if i ≠ 0
+
 
 /-- Constructs a proof of decreasing along a well founded relation, by applying
 lexicographic order lemmas and using `ts` to solve the base case. If it fails,

src/Lean.lean

@@ -37,3 +37,4 @@ import Lean.Log
 import Lean.Linter
 import Lean.SubExpr
 import Lean.LabelAttribute
+import Lean.AddDecl

src/Lean/AddDecl.lean

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.CoreM
+
+namespace Lean
+
+def Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration) : Except KernelException Environment :=
+  addDeclCore env (Core.getMaxHeartbeats opts).toUSize decl
+
+def Environment.addAndCompile (env : Environment) (opts : Options) (decl : Declaration) : Except KernelException Environment := do
+  let env ← addDecl env opts decl
+  compileDecl env opts decl
+
+def addDecl (decl : Declaration) : CoreM Unit := do
+  profileitM Exception "type checking" (← getOptions) do
+    withTraceNode `Kernel (fun _ => return m!"typechecking declaration") do
+      if !(← MonadLog.hasErrors) && decl.hasSorry then
+        logWarning "declaration uses 'sorry'"
+      match (← getEnv).addDecl (← getOptions) decl with
+      | .ok    env => setEnv env
+      | .error ex  => throwKernelException ex
+
+def addAndCompile (decl : Declaration) : CoreM Unit := do
+  addDecl decl
+  compileDecl decl
+
+end Lean

src/Lean/Attributes.lean

@@ -183,7 +183,6 @@ structure ParametricAttribute (α : Type) where
   deriving Inhabited
 
 structure ParametricAttributeImpl (α : Type) extends AttributeImplCore where
-  /-- This is used as the target for go-to-definition queries for simple attributes -/
   getParam : Name → Syntax → AttrM α
   afterSet : Name → α → AttrM Unit := fun _ _ _ => pure ()
   afterImport : Array (Array (Name × α)) → ImportM Unit := fun _ => pure ()

src/Lean/Compiler/ExternAttr.lean

@@ -66,12 +66,13 @@ builtin_initialize externAttr : ParametricAttribute ExternAttrData ←
     descr := "builtin and foreign functions"
     getParam := fun _ stx => syntaxToExternAttrData stx
     afterSet := fun declName _ => do
-      let mut env ← getEnv
-      if env.isProjectionFn declName || env.isConstructor declName then do
-        env ← ofExcept <| addExtern env declName
+      let env ← getEnv
+      if env.isProjectionFn declName || env.isConstructor declName then
+        if let some (.thmInfo ..) := env.find? declName then
+          -- We should not mark theorems as extern
+          return ()
+        let env ← ofExcept <| addExtern env declName
         setEnv env
-      else
-        pure ()
   }
 
 @[export lean_get_extern_attr_data]

src/Lean/Compiler/IR/RC.lean

@@ -9,9 +9,10 @@ import Lean.Compiler.IR.CompilerM
 import Lean.Compiler.IR.LiveVars
 
 namespace Lean.IR.ExplicitRC
-/-! Insert explicit RC instructions. So, it assumes the input code does not contain `inc` nor `dec` instructions.
-   This transformation is applied before lower level optimizations
-   that introduce the instructions `release` and `set`
+/-!
+Insert explicit RC instructions. So, it assumes the input code does not contain `inc` nor `dec` instructions.
+This transformation is applied before lower level optimizations
+that introduce the instructions `release` and `set`
 -/
 
 structure VarInfo where

src/Lean/Compiler/IR/ResetReuse.lean

@@ -9,152 +9,238 @@ import Lean.Compiler.IR.LiveVars
 import Lean.Compiler.IR.Format
 
 namespace Lean.IR.ResetReuse
-/-! Remark: the insertResetReuse transformation is applied before we have
-   inserted `inc/dec` instructions, and performed lower level optimizations
-   that introduce the instructions `release` and `set`. -/
-
-/-! Remark: the functions `S`, `D` and `R` defined here implement the
-  corresponding functions in the paper "Counting Immutable Beans"
-
-  Here are the main differences:
-  - We use the State monad to manage the generation of fresh variable names.
-  - Support for join points, and `uset` and `sset` instructions for unboxed data.
-  - `D` uses the auxiliary function `Dmain`.
-  - `Dmain` returns a pair `(b, found)` to avoid quadratic behavior when checking
-    the last occurrence of the variable `x`.
-  - Because we have join points in the actual implementation, a variable may be live even if it
-    does not occur in a function body. See example at `livevars.lean`.
+/-!
+Remark: the insertResetReuse transformation is applied before we have
+inserted `inc/dec` instructions, and performed lower level optimizations
+that introduce the instructions `release` and `set`.
 -/
 
-private def mayReuse (c₁ c₂ : CtorInfo) : Bool :=
+/-!
+Remark: the functions `S`, `D` and `R` defined here implement the
+corresponding functions in the paper "Counting Immutable Beans"
+
+Here are the main differences:
+- We use the State monad to manage the generation of fresh variable names.
+- Support for join points, and `uset` and `sset` instructions for unboxed data.
+- `D` uses the auxiliary function `Dmain`.
+- `Dmain` returns a pair `(b, found)` to avoid quadratic behavior when checking
+  the last occurrence of the variable `x`.
+- Because we have join points in the actual implementation, a variable may be live even if it
+  does not occur in a function body. See example at `livevars.lean`.
+-/
+
+private def mayReuse (c₁ c₂ : CtorInfo) (relaxedReuse : Bool) : Bool :=
   c₁.size == c₂.size && c₁.usize == c₂.usize && c₁.ssize == c₂.ssize &&
   /- The following condition is a heuristic.
-     We don't want to reuse cells from different types even when they are compatible
+     If `relaxedReuse := false`, then we don't want to reuse cells from
+     different constructors even when they are compatible
      because it produces counterintuitive behavior. -/
-  c₁.name.getPrefix == c₂.name.getPrefix
+  (relaxedReuse || c₁.name.getPrefix == c₂.name.getPrefix)
 
-private partial def S (w : VarId) (c : CtorInfo) : FnBody → FnBody
-  | FnBody.vdecl x t v@(Expr.ctor c' ys) b   =>
-    if mayReuse c c' then
+/--
+Replace `ctor` applications with `reuse` applications if compatible.
+`w` contains the "memory cell" being reused.
+-/
+private partial def S (w : VarId) (c : CtorInfo) (relaxedReuse : Bool) (b : FnBody) : FnBody :=
+  go b
+where
+  go : FnBody → FnBody
+  | .vdecl x t v@(.ctor c' ys) b   =>
+    if mayReuse c c' relaxedReuse then
       let updtCidx := c.cidx != c'.cidx
-      FnBody.vdecl x t (Expr.reuse w c' updtCidx ys) b
+      .vdecl x t (.reuse w c' updtCidx ys) b
     else
-      FnBody.vdecl x t v (S w c b)
-  | FnBody.jdecl j ys v b   =>
-    let v' := S w c v
-    if v == v' then FnBody.jdecl j ys v (S w c b)
-    else FnBody.jdecl j ys v' b
-  | FnBody.case tid x xType alts    => FnBody.case tid x xType <| alts.map fun alt => alt.modifyBody (S w c)
+      .vdecl x t v (go b)
+  | .jdecl j ys v b   =>
+    let v' := go v
+    if v == v' then
+      .jdecl j ys v (go b)
+    else
+      .jdecl j ys v' b
+  | .case tid x xType alts =>
+    .case tid x xType <| alts.map fun alt => alt.modifyBody go
   | b =>
-    if b.isTerminal then b
-    else let
-      (instr, b) := b.split
-      instr.setBody (S w c b)
+    if b.isTerminal then
+      b
+    else
+      let (instr, b) := b.split
+      instr.setBody (go b)
+
+structure Context where
+  lctx      : LocalContext := {}
+  /--
+  Contains all variables in `cases` statements in the current path
+  and variables that are already in `reset` statements when we
+  invoke `R`.
+
+  We use this information to prevent double-reset in code such as
+  ```
+  case x_i : obj of
+  Prod.mk →
+    case x_i : obj of
+    Prod.mk →
+    ...
+  ```
+
+  A variable can already be in a `reset` statement when we
+  invoke `R` because we execute it with and without `relaxedReuse`.
+  -/
+  alreadyFound : PHashSet VarId := {}
+  /--
+  If `relaxedReuse := true`, then allow memory cells from different
+  constructors to be reused. For example, we can reuse a `PSigma.mk`
+  to allocate a `Prod.mk`. To avoid counterintuitive behavior,
+  we first try `relaxedReuse := false`, and then `relaxedReuse := true`.
+  -/
+  relaxedReuse : Bool := false
 
 /-- We use `Context` to track join points in scope. -/
-abbrev M := ReaderT LocalContext (StateT Index Id)
+abbrev M := ReaderT Context (StateT Index Id)
 
 private def mkFresh : M VarId := do
-  let idx ← getModify (fun n => n + 1)
-  pure { idx := idx }
+  let idx ← getModify fun n => n + 1
+  return { idx := idx }
 
+/--
+Helper function for applying `S`. We only introduce a `reset` if we managed
+to replace a `ctor` withe `reuse` in `b`.
+-/
 private def tryS (x : VarId) (c : CtorInfo) (b : FnBody) : M FnBody := do
   let w ← mkFresh
-  let b' := S w c b
-  if b == b' then pure b
-  else pure $ FnBody.vdecl w IRType.object (Expr.reset c.size x) b'
+  let b' := S w c (← read).relaxedReuse b
+  if b == b' then
+    return b
+  else
+    return .vdecl w IRType.object (.reset c.size x) b'
 
 private def Dfinalize (x : VarId) (c : CtorInfo) : FnBody × Bool → M FnBody
-  | (b, true)  => pure b
+  | (b, true)  => return b
   | (b, false) => tryS x c b
 
 private def argsContainsVar (ys : Array Arg) (x : VarId) : Bool :=
   ys.any fun arg => match arg with
-    | Arg.var y => x == y
-    | _         => false
+    | .var y => x == y
+    | _      => false
 
 private def isCtorUsing (b : FnBody) (x : VarId) : Bool :=
   match b with
-  | (FnBody.vdecl _ _ (Expr.ctor _ ys) _) => argsContainsVar ys x
+  | .vdecl _ _ (.ctor _ ys) _ => argsContainsVar ys x
   | _ => false
 
-/-- Given `Dmain b`, the resulting pair `(new_b, flag)` contains the new body `new_b`,
-   and `flag == true` if `x` is live in `b`.
+/--
+Given `Dmain b`, the resulting pair `(new_b, flag)` contains the new body `new_b`,
+and `flag == true` if `x` is live in `b`.
 
-   Note that, in the function `D` defined in the paper, for each `let x := e; F`,
-   `D` checks whether `x` is live in `F` or not. This is great for clarity but it
-   is expensive: `O(n^2)` where `n` is the size of the function body. -/
-private partial def Dmain (x : VarId) (c : CtorInfo) : FnBody → M (FnBody × Bool)
-  | e@(FnBody.case tid y yType alts) => do
-    let ctx ← read
-    if e.hasLiveVar ctx x then do
+Note that, in the function `D` defined in the paper, for each `let x := e; F`,
+`D` checks whether `x` is live in `F` or not. This is great for clarity but it
+is expensive: `O(n^2)` where `n` is the size of the function body. -/
+private partial def Dmain (x : VarId) (c : CtorInfo) (e : FnBody) : M (FnBody × Bool) := do
+  match e with
+  | .case tid y yType alts =>
+    if e.hasLiveVar (← read).lctx x then
       /- If `x` is live in `e`, we recursively process each branch. -/
       let alts ← alts.mapM fun alt => alt.mmodifyBody fun b => Dmain x c b >>= Dfinalize x c
-      pure (FnBody.case tid y yType alts, true)
-    else pure (e, false)
-  | FnBody.jdecl j ys v b   => do
-    let (b, found) ← withReader (fun ctx => ctx.addJP j ys v) (Dmain x c b)
+      return (.case tid y yType alts, true)
+    else
+      return (e, false)
+  | .jdecl j ys v b =>
+    let (b, found) ← withReader (fun ctx => { ctx with lctx := ctx.lctx.addJP j ys v }) (Dmain x c b)
     let (v, _ /- found' -/) ← Dmain x c v
     /- If `found' == true`, then `Dmain b` must also have returned `(b, true)` since
        we assume the IR does not have dead join points. So, if `x` is live in `j` (i.e., `v`),
        then it must also live in `b` since `j` is reachable from `b` with a `jmp`.
        On the other hand, `x` may be live in `b` but dead in `j` (i.e., `v`). -/
-    pure (FnBody.jdecl j ys v b, found)
-  | e => do
-    let ctx ← read
+    return (.jdecl j ys v b, found)
+  | e =>
     if e.isTerminal then
-      pure (e, e.hasLiveVar ctx x)
+      return (e, e.hasLiveVar (← read).lctx x)
     else do
       let (instr, b) := e.split
       if isCtorUsing instr x then
         /- If the scrutinee `x` (the one that is providing memory) is being
            stored in a constructor, then reuse will probably not be able to reuse memory at runtime.
            It may work only if the new cell is consumed, but we ignore this case. -/
-        pure (e, true)
+        return (e, true)
       else
         let (b, found) ← Dmain x c b
         /- Remark: it is fine to use `hasFreeVar` instead of `hasLiveVar`
-           since `instr` is not a `FnBody.jmp` (it is not a terminal) nor it is a `FnBody.jdecl`. -/
+           since `instr` is not a `FnBody.jmp` (it is not a terminal) nor
+           it is a `FnBody.jdecl`. -/
         if found || !instr.hasFreeVar x then
-          pure (instr.setBody b, found)
+          return (instr.setBody b, found)
         else
           let b ← tryS x c b
-          pure (instr.setBody b, true)
+          return (instr.setBody b, true)
 
 private def D (x : VarId) (c : CtorInfo) (b : FnBody) : M FnBody :=
   Dmain x c b >>= Dfinalize x c
 
-partial def R : FnBody → M FnBody
-  | FnBody.case tid x xType alts   => do
+partial def R (e : FnBody) : M FnBody := do
+  match e with
+  | .case tid x xType alts =>
+    let alreadyFound := (← read).alreadyFound.contains x
+    withReader (fun ctx => { ctx with alreadyFound := ctx.alreadyFound.insert x }) do
       let alts ← alts.mapM fun alt => do
         let alt ← alt.mmodifyBody R
         match alt with
-        | Alt.ctor c b =>
-          if c.isScalar then pure alt
-          else Alt.ctor c <$> D x c b
-        | _            => pure alt
-      pure $ FnBody.case tid x xType alts
-  | FnBody.jdecl j ys v b   => do
+        | .ctor c b =>
+          if c.isScalar || alreadyFound then
+            -- If `alreadyFound`, then we don't try to reuse memory cell to avoid
+            -- double reset.
+            return alt
+          else
+            .ctor c <$> D x c b
+        | _ => return alt
+      return .case tid x xType alts
+  | .jdecl j ys v b =>
     let v ← R v
-    let b ← withReader (fun ctx => ctx.addJP j ys v) (R b)
-    pure $ FnBody.jdecl j ys v b
-  | e => do
-    if e.isTerminal then pure e
-    else do
+    let b ← withReader (fun ctx => { ctx with lctx := ctx.lctx.addJP j ys v }) (R b)
+    return .jdecl j ys v b
+  | e =>
+    if e.isTerminal then
+      return e
+    else
       let (instr, b) := e.split
       let b ← R b
-      pure (instr.setBody b)
+      return instr.setBody b
+
+abbrev N := StateT (PHashSet VarId) Id
+
+partial def collectResets (e : FnBody) : N Unit := do
+  match e with
+  | .case _ _ _ alts => alts.forM fun alt => collectResets alt.body
+  | .jdecl _ _ v b => collectResets v; collectResets b
+  | .vdecl _ _ (.reset _ x) b => modify fun s => s.insert x; collectResets b
+  | e => unless e.isTerminal do
+    let (_, b) := e.split
+    collectResets b
 
 end ResetReuse
-
 open ResetReuse
 
-def Decl.insertResetReuse (d : Decl) : Decl :=
+
+def Decl.insertResetReuseCore (d : Decl) (relaxedReuse : Bool) : Decl :=
   match d with
-  | .fdecl (body := b) ..=>
+  | .fdecl (body := b) .. =>
     let nextIndex := d.maxIndex + 1
-    let bNew      := (R b {}).run' nextIndex
+    -- First time we execute `insertResetReuseCore`, `relaxedReuse := false`.
+    let alreadyFound : PHashSet VarId := if relaxedReuse then (collectResets b *> get).run' {} else {}
+    let bNew := R b { relaxedReuse, alreadyFound } |>.run' nextIndex
     d.updateBody! bNew
   | other => other
 
+def Decl.insertResetReuse (d : Decl) : Decl :=
+  /-
+  We execute the reset/reuse algorithm twice. The first time, we only reuse memory cells
+  between identical constructor memory cells. That is, we do not reuse a `PSigma.mk` memory cell
+  when allocating a `Prod.mk` memory cell, even though they have the same layout. Recall
+  that the reset/reuse placement algorithm is a heuristic, and the first pass prevents reuses
+  that are unlikely to be useful at runtime. Then, we run the procedure again,
+  relaxing this restriction. If there are still opportunities for reuse, we will take advantage of them.
+
+  The second pass addresses issue #4089.
+  -/
+  d.insertResetReuseCore (relaxedReuse := false)
+  |>.insertResetReuseCore (relaxedReuse := true)
+
 end Lean.IR

src/Lean/Compiler/InitAttr.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.AddDecl
 import Lean.Elab.InfoTree.Main
 
 namespace Lean

src/Lean/Compiler/Old.lean

@@ -67,9 +67,4 @@ opaque compileDecls (env : Environment) (opt : @& Options) (decls : @& List Name
 def compileDecl (env : Environment) (opt : @& Options) (decl : @& Declaration) : Except KernelException Environment :=
   compileDecls env opt (Compiler.getDeclNamesForCodeGen decl)
 
-
-def addAndCompile (env : Environment) (opt : Options) (decl : Declaration) : Except KernelException Environment := do
-  let env ← addDecl env decl
-  compileDecl env opt decl
-
 end Environment

src/Lean/CoreM.lean

@@ -13,13 +13,27 @@ import Lean.Elab.InfoTree.Types
 import Lean.MonadEnv
 
 namespace Lean
-namespace Core
+register_builtin_option diagnostics : Bool := {
+  defValue := false
+  group    := "diagnostics"
+  descr    := "collect diagnostic information"
+}
+
+register_builtin_option diagnostics.threshold : Nat := {
+  defValue := 20
+  group    := "diagnostics"
+  descr    := "only diagnostic counters above this threshold are reported by the definitional equality"
+}
 
 register_builtin_option maxHeartbeats : Nat := {
   defValue := 200000
   descr := "maximum amount of heartbeats per command. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit"
 }
 
+def useDiagnosticMsg := s!"use `set_option {diagnostics.name} true` to get diagnostic information"
+
+namespace Core
+
 builtin_initialize registerTraceClass `Kernel
 
 def getMaxHeartbeats (opts : Options) : Nat :=
@@ -67,11 +81,10 @@ structure Context where
   maxHeartbeats  : Nat := getMaxHeartbeats options
   currMacroScope : MacroScope := firstFrontendMacroScope
   /--
-  If `catchRuntimeEx = false`, then given `try x catch ex => h ex`,
-  an runtime exception occurring in `x` is not handled by `h`.
-  Recall that runtime exceptions are `maxRecDepth` or `maxHeartbeats`.
+  If `diag := true`, different parts of the system collect diagnostics.
+  Use the `set_option diag true` to set it to true.
   -/
-  catchRuntimeEx : Bool := false
+  diag           : Bool := false
   deriving Nonempty
 
 /-- CoreM is a monad for manipulating the Lean environment.
@@ -104,7 +117,22 @@ instance : MonadOptions CoreM where
   getOptions := return (← read).options
 
 instance : MonadWithOptions CoreM where
-  withOptions f x := withReader (fun ctx => { ctx with options := f ctx.options }) x
+  withOptions f x := do
+    let options := f (← read).options
+    let diag := diagnostics.get options
+    if Kernel.isDiagnosticsEnabled (← getEnv) != diag then
+      modifyEnv fun env => Kernel.enableDiag env diag
+    withReader
+      (fun ctx =>
+        { ctx with
+          options
+          diag
+          maxRecDepth := maxRecDepth.get options })
+      x
+
+-- Helper function for ensuring fields that depend on `options` have the correct value.
+@[inline] private def withConsistentCtx (x : CoreM α) : CoreM α := do
+  withOptions id x
 
 instance : AddMessageContext CoreM where
   addMessageContext := addMessageContextPartial
@@ -192,7 +220,7 @@ def mkFreshUserName (n : Name) : CoreM Name :=
   mkFreshNameImp n
 
 @[inline] def CoreM.run (x : CoreM α) (ctx : Context) (s : State) : EIO Exception (α × State) :=
-  (x ctx).run s
+  ((withConsistentCtx x) ctx).run s
 
 @[inline] def CoreM.run' (x : CoreM α) (ctx : Context) (s : State) : EIO Exception α :=
   Prod.fst <$> x.run ctx s
@@ -206,7 +234,7 @@ def mkFreshUserName (n : Name) : CoreM Name :=
 instance [MetaEval α] : MetaEval (CoreM α) where
   eval env opts x _ := do
     let x : CoreM α := do try x finally printTraces
-    let (a, s) ← x.toIO { maxRecDepth := maxRecDepth.get opts, options := opts, fileName := "<CoreM>", fileMap := default } { env := env }
+    let (a, s) ← (withConsistentCtx x).toIO { fileName := "<CoreM>", fileMap := default, options := opts } { env := env }
     MetaEval.eval s.env opts a (hideUnit := true)
 
 -- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`
@@ -218,8 +246,16 @@ protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m
     -- should never be visible to users!
     throw <| Exception.error .missing "elaboration interrupted"
 
+register_builtin_option debug.moduleNameAtTimeout : Bool := {
+  defValue := true
+  group    := "debug"
+  descr    := "include module name in deterministic timeout error messages.\nRemark: we set this option to false to increase the stability of our test suite"
+}
+
 def throwMaxHeartbeat (moduleName : Name) (optionName : Name) (max : Nat) : CoreM Unit := do
-  let msg := s!"(deterministic) timeout at '{moduleName}', maximum number of heartbeats ({max/1000}) has been reached (use 'set_option {optionName} <num>' to set the limit)"
+  let includeModuleName := debug.moduleNameAtTimeout.get (← getOptions)
+  let atModuleName := if includeModuleName then s!" at `{moduleName}`" else ""
+  let msg := s!"(deterministic) timeout{atModuleName}, maximum number of heartbeats ({max/1000}) has been reached\nuse `set_option {optionName} <num>` to set the limit\n{useDiagnosticMsg}"
   throw <| Exception.error (← getRef) (MessageData.ofFormat (Std.Format.text msg))
 
 def checkMaxHeartbeatsCore (moduleName : String) (optionName : Name) (max : Nat) : CoreM Unit := do
@@ -296,7 +332,8 @@ export Core (CoreM mkFreshUserName checkSystem withCurrHeartbeats)
   We used a similar hack at `Exception.isMaxRecDepth` -/
 def Exception.isMaxHeartbeat (ex : Exception) : Bool :=
   match ex with
-  | Exception.error _ (MessageData.ofFormat (Std.Format.text msg)) => "(deterministic) timeout".isPrefixOf msg
+  | Exception.error _ (MessageData.ofFormatWithInfos ⟨Std.Format.text msg, _⟩) =>
+    "(deterministic) timeout".isPrefixOf msg
   | _ => false
 
 /-- Creates the expression `d → b` -/
@@ -306,15 +343,6 @@ def mkArrow (d b : Expr) : CoreM Expr :=
 /-- Iterated `mkArrow`, creates the expression `a₁ → a₂ → … → aₙ → b`. Also see `arrowDomainsN`. -/
 def mkArrowN (ds : Array Expr) (e : Expr) : CoreM Expr := ds.foldrM mkArrow e
 
-def addDecl (decl : Declaration) : CoreM Unit := do
-  profileitM Exception "type checking" (← getOptions) do
-    withTraceNode `Kernel (fun _ => return m!"typechecking declaration") do
-      if !(← MonadLog.hasErrors) && decl.hasSorry then
-        logWarning "declaration uses 'sorry'"
-      match (← getEnv).addDecl decl with
-      | Except.ok    env => setEnv env
-      | Except.error ex  => throwKernelException ex
-
 private def supportedRecursors :=
   #[``Empty.rec, ``False.rec, ``Eq.ndrec, ``Eq.rec, ``Eq.recOn, ``Eq.casesOn, ``False.casesOn, ``Empty.casesOn, ``And.rec, ``And.casesOn]
 
@@ -368,13 +396,16 @@ def compileDecls (decls : List Name) : CoreM Unit := do
   | Except.error ex =>
     throwKernelException ex
 
-def addAndCompile (decl : Declaration) : CoreM Unit := do
-  addDecl decl;
-  compileDecl decl
+def getDiag (opts : Options) : Bool :=
+  diagnostics.get opts
+
+/-- Return `true` if diagnostic information collection is enabled. -/
+def isDiagnosticsEnabled : CoreM Bool :=
+  return (← read).diag
 
 def ImportM.runCoreM (x : CoreM α) : ImportM α := do
   let ctx ← read
-  let (a, _) ← x.toIO { options := ctx.opts, fileName := "<ImportM>", fileMap := default } { env := ctx.env }
+  let (a, _) ← (withOptions (fun _ => ctx.opts) x).toIO { fileName := "<ImportM>", fileMap := default } { env := ctx.env }
   return a
 
 /-- Return `true` if the exception was generated by one our resource limits. -/
@@ -389,30 +420,36 @@ in these monads, but on `CommandElabM`. See issues #2775 and #2744 as well as `M
   try
     x
   catch ex =>
-    if ex.isRuntime && !(← read).catchRuntimeEx then
-      throw ex
+    if ex.isRuntime then
+      throw ex -- We should use `tryCatchRuntimeEx` for catching runtime exceptions
     else
       h ex
 
+@[inline] protected def Core.tryCatchRuntimeEx (x : CoreM α) (h : Exception → CoreM α) : CoreM α := do
+  try
+    x
+  catch ex =>
+    h ex
+
 instance : MonadExceptOf Exception CoreM where
   throw    := throw
   tryCatch := Core.tryCatch
 
-@[inline] def Core.withCatchingRuntimeEx (flag : Bool) (x : CoreM α) : CoreM α :=
-  withReader (fun ctx => { ctx with catchRuntimeEx := flag }) x
+class MonadRuntimeException (m : Type → Type) where
+  tryCatchRuntimeEx (body : m α) (handler : Exception → m α) : m α
+
+export MonadRuntimeException (tryCatchRuntimeEx)
+
+instance : MonadRuntimeException CoreM where
+  tryCatchRuntimeEx := Core.tryCatchRuntimeEx
+
+@[inline] instance [MonadRuntimeException m] : MonadRuntimeException (ReaderT ρ m) where
+  tryCatchRuntimeEx := fun x c r => tryCatchRuntimeEx (x r) (fun e => (c e) r)
+
+@[inline] instance [MonadRuntimeException m] : MonadRuntimeException (StateRefT' ω σ m) where
+  tryCatchRuntimeEx := fun x c s => tryCatchRuntimeEx (x s) (fun e => c e s)
 
 @[inline] def mapCoreM [MonadControlT CoreM m] [Monad m] (f : forall {α}, CoreM α → CoreM α) {α} (x : m α) : m α :=
   controlAt CoreM fun runInBase => f <| runInBase x
 
-/--
-Execute `x` with `catchRuntimeEx = flag`. That is, given `try x catch ex => h ex`,
-if `x` throws a runtime exception, the handler `h` will be invoked if `flag = true`
-Recall that
--/
-@[inline] def withCatchingRuntimeEx [MonadControlT CoreM m] [Monad m] (x : m α) : m α :=
-  mapCoreM (Core.withCatchingRuntimeEx true) x
-
-@[inline] def withoutCatchingRuntimeEx [MonadControlT CoreM m] [Monad m] (x : m α) : m α :=
-  mapCoreM (Core.withCatchingRuntimeEx false) x
-
 end Lean

src/Lean/Data/HashMap.lean

@@ -92,6 +92,7 @@ def moveEntries [Hashable α] (i : Nat) (source : Array (AssocList α β)) (targ
      moveEntries (i+1) source target
   else target
 termination_by source.size - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapImp α β :=
   let bucketsNew : HashMapBucket α β := ⟨

src/Lean/Data/HashSet.lean

@@ -84,6 +84,7 @@ def moveEntries [Hashable α] (i : Nat) (source : Array (List α)) (target : Has
   else
     target
 termination_by source.size - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def expand [Hashable α] (size : Nat) (buckets : HashSetBucket α) : HashSetImp α :=
   let bucketsNew : HashSetBucket α := ⟨

src/Lean/Data/Parsec.lean

@@ -43,11 +43,19 @@ def fail (msg : String) : Parsec α := fun it =>
   error it msg
 
 @[inline]
-def orElse (p : Parsec α) (q : Unit → Parsec α) : Parsec α := fun it =>
+def tryCatch (p : Parsec α)
+    (csuccess : α → Parsec β)
+    (cerror : Unit → Parsec β)
+    : Parsec β := fun it =>
   match p it with
-  | success rem a => success rem a
-  | error rem err =>
-    if it = rem then q () it else error rem err
+  | .success rem a => csuccess a rem
+  | .error rem err =>
+    -- We assume that it.s never changes as the `Parsec` monad only modifies `it.pos`.
+    if it.pos = rem.pos then cerror () rem else .error rem err
+
+@[inline]
+def orElse (p : Parsec α) (q : Unit → Parsec α) : Parsec α :=
+  tryCatch p pure q
 
 @[inline]
 def attempt (p : Parsec α) : Parsec α := λ it =>
@@ -74,8 +82,7 @@ def eof : Parsec Unit := fun it =>
 
 @[specialize]
 partial def manyCore (p : Parsec α) (acc : Array α) : Parsec $ Array α :=
-  (do manyCore p (acc.push $ ←p))
-  <|> pure acc
+  tryCatch p (manyCore p <| acc.push ·) (fun _ => pure acc)
 
 @[inline]
 def many (p : Parsec α) : Parsec $ Array α := manyCore p #[]
@@ -85,8 +92,7 @@ def many1 (p : Parsec α) : Parsec $ Array α := do manyCore p #[←p]
 
 @[specialize]
 partial def manyCharsCore (p : Parsec Char) (acc : String) : Parsec String :=
-  (do manyCharsCore p (acc.push $ ←p))
-  <|> pure acc
+  tryCatch p (manyCharsCore p <| acc.push ·) (fun _ => pure acc)
 
 @[inline]
 def manyChars (p : Parsec Char) : Parsec String := manyCharsCore p ""

src/Lean/Data/Position.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
 import Lean.Data.Format
+import Lean.Data.Json
 import Lean.ToExpr
 
 namespace Lean
@@ -12,7 +13,7 @@ namespace Lean
 structure Position where
   line   : Nat
   column : Nat
-  deriving Inhabited, DecidableEq, Repr
+  deriving Inhabited, DecidableEq, Repr, ToJson, FromJson
 
 namespace Position
 protected def lt : Position → Position → Bool

src/Lean/Data/RBTree.lean

@@ -100,7 +100,7 @@ def fromArray (l : Array α) (cmp : α → α → Ordering) : RBTree α cmp :=
   RBMap.any t (fun a _ => p a)
 
 def subset (t₁ t₂ : RBTree α cmp) : Bool :=
-  t₁.all fun a => (t₂.find? a).toBool
+  t₁.all fun a => (t₂.find? a).isSome
 
 def seteq (t₁ t₂ : RBTree α cmp) : Bool :=
   subset t₁ t₂ && subset t₂ t₁

src/Lean/Declaration.lean

@@ -135,6 +135,11 @@ structure TheoremVal extends ConstantVal where
   all : List Name := [name]
   deriving Inhabited, BEq
 
+@[export lean_mk_theorem_val]
+def mkTheoremValEx (name : Name) (levelParams : List Name) (type : Expr) (value : Expr) (all : List Name) : TheoremVal := {
+  name, levelParams, type, value, all
+}
+
 /-- Value for an opaque constant declaration `opaque x : t := e` -/
 structure OpaqueVal extends ConstantVal where
   value : Expr

src/Lean/Elab/Binders.lean

@@ -7,6 +7,7 @@ prelude
 import Lean.Elab.Quotation.Precheck
 import Lean.Elab.Term
 import Lean.Elab.BindersUtil
+import Lean.Elab.SyntheticMVars
 import Lean.Elab.PreDefinition.WF.TerminationHint
 
 namespace Lean.Elab.Term
@@ -70,30 +71,34 @@ def kindOfBinderName (binderName : Name) : LocalDeclKind :=
   else
     .default
 
-partial def quoteAutoTactic : Syntax → TermElabM Syntax
-  | stx@(.ident ..) => throwErrorAt stx "invalid auto tactic, identifier is not allowed"
+partial def quoteAutoTactic : Syntax → CoreM Expr
+  | .ident _ _ val preresolved =>
+    return mkApp4 (.const ``Syntax.ident [])
+      (.const ``SourceInfo.none [])
+      (.app (.const ``String.toSubstring []) (mkStrLit (toString val)))
+      (toExpr val)
+      (toExpr preresolved)
   | stx@(.node _ k args) => do
     if stx.isAntiquot then
       throwErrorAt stx "invalid auto tactic, antiquotation is not allowed"
     else
-      let mut quotedArgs ← `(Array.empty)
+      let ty := .const ``Syntax []
+      let mut quotedArgs := mkApp (.const ``Array.empty [.zero]) ty
       for arg in args do
         if k == nullKind && (arg.isAntiquotSuffixSplice || arg.isAntiquotSplice) then
           throwErrorAt arg "invalid auto tactic, antiquotation is not allowed"
         else
           let quotedArg ← quoteAutoTactic arg
-          quotedArgs ← `(Array.push $quotedArgs $quotedArg)
-      `(Syntax.node SourceInfo.none $(quote k) $quotedArgs)
-  | .atom _ val => `(mkAtom $(quote val))
+          quotedArgs := mkApp3 (.const ``Array.push [.zero]) ty quotedArgs quotedArg
+      return mkApp3 (.const ``Syntax.node []) (.const ``SourceInfo.none []) (toExpr k) quotedArgs
+  | .atom _ val => return .app (.const ``mkAtom []) (toExpr val)
   | .missing    => throwError "invalid auto tactic, tactic is missing"
 
 def declareTacticSyntax (tactic : Syntax) : TermElabM Name :=
   withFreshMacroScope do
     let name ← MonadQuotation.addMacroScope `_auto
     let type := Lean.mkConst `Lean.Syntax
-    let tactic ← quoteAutoTactic tactic
-    let value ← elabTerm tactic type
-    let value ← instantiateMVars value
+    let value ← quoteAutoTactic tactic
     trace[Elab.autoParam] value
     let decl := Declaration.defnDecl { name, levelParams := [], type, value, hints := .opaque,
                                        safety := DefinitionSafety.safe }
@@ -642,7 +647,29 @@ def elabLetDeclAux (id : Syntax) (binders : Array Syntax) (typeStx : Syntax) (va
     (expectedType? : Option Expr) (useLetExpr : Bool) (elabBodyFirst : Bool) (usedLetOnly : Bool) : TermElabM Expr := do
   let (type, val, binders) ← elabBindersEx binders fun xs => do
     let (binders, fvars) := xs.unzip
-    let type ← elabType typeStx
+    /-
+    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`.
+    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.
+
+    Here is the analysis for issue #4051.
+    - Given `have x : type := value; body`, we were previously elaborating `value` even
+      if `type` contained postponed elaboration problems.
+    - Moreover, the metavariables in `type` corresponding to postponed elaboration
+      problems cannot be assigned by `isDefEq` since the elaborator is supposed to assign them.
+    - Then, when checking whether type of `value` is definitionally equal to `type`,
+      a very long-time was spent unfolding a bunch of declarations before it failed.
+      In #4051, it was unfolding `Array.swaps` which is defined by well-founded recursion.
+      After the failure, the elaborator inserted a postponed coercion
+      that would be resolved later as soon as the types don't have unassigned metavariables.
+
+    We use `postpone := .partial` to allow type class (TC) resolution problems to be postponed
+    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"
     if elabBodyFirst then
       let type ← mkForallFVars fvars type

src/Lean/Elab/BuiltinCommand.lean

@@ -123,7 +123,7 @@ private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM
   n[1].forArgsM addUnivLevel
 
 @[builtin_command_elab «init_quot»] def elabInitQuot : CommandElab := fun _ => do
-  match (← getEnv).addDecl Declaration.quotDecl with
+  match (← getEnv).addDecl (← getOptions) Declaration.quotDecl with
   | Except.ok env   => setEnv env
   | Except.error ex => throwError (ex.toMessageData (← getOptions))
 

src/Lean/Elab/BuiltinNotation.lean

@@ -98,7 +98,7 @@ open Meta
       show Nat from 0
     ```
     -/
-    let type ← withSynthesize (mayPostpone := true) do
+    let type ← withSynthesize (postpone := .yes) do
       let type ← elabType type
       if let some expectedType := expectedType? then
         -- Recall that a similar approach is used when elaborating applications
@@ -205,7 +205,7 @@ private def elabTParserMacroAux (prec lhsPrec e : Term) : TermElabM Syntax := do
   | _                                        => Macro.throwUnsupported
 
 @[builtin_term_elab «sorry»] def elabSorry : TermElab := fun stx expectedType? => do
-  let stxNew ← `(sorryAx _ false)
+  let stxNew ← `(@sorryAx _ false) -- Remark: we use `@` to ensure `sorryAx` will not consume auot params
   withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
 
 /-- Return syntax `Prod.mk elems[0] (Prod.mk elems[1] ... (Prod.mk elems[elems.size - 2] elems[elems.size - 1])))` -/
@@ -314,11 +314,11 @@ where
 
 @[builtin_term_elab typeAscription] def elabTypeAscription : TermElab
   | `(($e : $type)), _ => do
-    let type ← withSynthesize (mayPostpone := true) <| elabType type
+    let type ← withSynthesize (postpone := .yes) <| elabType type
     let e ← elabTerm e type
     ensureHasType type e
   | `(($e :)), expectedType? => do
-    let e ← withSynthesize (mayPostpone := false) <| elabTerm e none
+    let e ← withSynthesize (postpone := .no) <| elabTerm e none
     ensureHasType expectedType? e
   | _, _ => throwUnsupportedSyntax
 
@@ -388,7 +388,7 @@ private def withLocalIdentFor (stx : Term) (e : Expr) (k : Term → TermElabM Ex
                return (← mkEqRec motive h (← mkEqSymm heq), none)
          let motive ← mkMotive lhs expectedAbst
          if badMotive?.isSome || !(← isTypeCorrect motive) then
-           -- Before failing try tos use `subst`
+           -- Before failing try to use `subst`
            if ← (isSubstCandidate lhs rhs <||> isSubstCandidate rhs lhs) then
              withLocalIdentFor heqStx heq fun heqStx => do
                let h ← instantiateMVars h
@@ -408,7 +408,13 @@ private def withLocalIdentFor (stx : Term) (e : Expr) (k : Term → TermElabM Ex
        | none =>
          let h ← elabTerm hStx none
          let hType ← inferType h
-         let hTypeAbst ← kabstract hType lhs
+         let mut hTypeAbst ← kabstract hType lhs
+         unless hTypeAbst.hasLooseBVars do
+           hTypeAbst ← kabstract hType rhs
+           unless hTypeAbst.hasLooseBVars do
+             throwError "invalid `▸` notation, the equality{indentExpr heq}\nhas type {indentExpr heqType}\nbut neither side of the equality is mentioned in the type{indentExpr hType}"
+           heq ← mkEqSymm heq
+           (lhs, rhs) := (rhs, lhs)
          let motive ← mkMotive lhs hTypeAbst
          unless (← isTypeCorrect motive) do
            throwError "invalid `▸` notation, failed to compute motive for the substitution"

src/Lean/Elab/BuiltinTerm.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Meta.Diagnostics
 import Lean.Elab.Open
 import Lean.Elab.SetOption
 import Lean.Elab.Eval
@@ -313,8 +314,12 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
 
 @[builtin_term_elab «set_option»] def elabSetOption : TermElab := fun stx expectedType? => do
   let options ← Elab.elabSetOption stx[1] stx[3]
-  withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options }) do
-    elabTerm stx[5] expectedType?
+  withOptions (fun _ => options) do
+    try
+      elabTerm stx[5] expectedType?
+    finally
+      if stx[1].getId == `diagnostics then
+        reportDiag
 
 @[builtin_term_elab withAnnotateTerm] def elabWithAnnotateTerm : TermElab := fun stx expectedType? => do
   match stx with

src/Lean/Elab/Calc.lean

@@ -42,7 +42,7 @@ def mkCalcTrans (result resultType step stepType : Expr) : MetaM (Expr × Expr)
     unless (← getCalcRelation? resultType).isSome do
       throwError "invalid 'calc' step, step result is not a relation{indentExpr resultType}"
     return (result, resultType)
-  | _ => throwError "invalid 'calc' step, failed to synthesize `Trans` instance{indentExpr selfType}"
+  | _ => throwError "invalid 'calc' step, failed to synthesize `Trans` instance{indentExpr selfType}\n{useDiagnosticMsg}"
 
 /--
 Adds a type annotation to a hole that occurs immediately at the beginning of the term.
@@ -112,10 +112,12 @@ def elabCalcSteps (steps : TSyntax ``calcSteps) : TermElabM Expr := do
   return result?.get!.1
 
 /-- Elaborator for the `calc` term mode variant. -/
-@[builtin_term_elab «calc»]
+@[builtin_term_elab Lean.calc]
 def elabCalc : TermElab := fun stx expectedType? => do
   let steps : TSyntax ``calcSteps := ⟨stx[1]⟩
   let result ← elabCalcSteps steps
   synthesizeSyntheticMVarsUsingDefault
   let result ← ensureHasType expectedType? result
   return result
+
+end Lean.Elab.Term

src/Lean/Elab/Command.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Gabriel Ebner
 -/
 prelude
+import Lean.Meta.Diagnostics
 import Lean.Elab.Binders
 import Lean.Elab.SyntheticMVars
 import Lean.Elab.SetOption
@@ -127,19 +128,6 @@ def mkMessageAux (ctx : Context) (ref : Syntax) (msgData : MessageData) (severit
   let endPos := ref.getTailPos?.getD pos
   mkMessageCore ctx.fileName ctx.fileMap msgData severity pos endPos
 
-private def mkCoreContext (ctx : Context) (s : State) (heartbeats : Nat) : Core.Context :=
-  let scope        := s.scopes.head!
-  { fileName       := ctx.fileName
-    fileMap        := ctx.fileMap
-    options        := scope.opts
-    currRecDepth   := ctx.currRecDepth
-    maxRecDepth    := s.maxRecDepth
-    ref            := ctx.ref
-    currNamespace  := scope.currNamespace
-    openDecls      := scope.openDecls
-    initHeartbeats := heartbeats
-    currMacroScope := ctx.currMacroScope }
-
 private def addTraceAsMessagesCore (ctx : Context) (log : MessageLog) (traceState : TraceState) : MessageLog := Id.run do
   if traceState.traces.isEmpty then return log
   let mut traces : HashMap (String.Pos × String.Pos) (Array MessageData) := ∅
@@ -165,31 +153,49 @@ private def addTraceAsMessages : CommandElabM Unit := do
       traceState.traces := {}
     }
 
-def liftCoreM (x : CoreM α) : CommandElabM α := do
+private def runCore (x : CoreM α) : CommandElabM α := do
   let s ← get
   let ctx ← read
   let heartbeats ← IO.getNumHeartbeats
-  let Eα := Except Exception α
-  let x : CoreM Eα := try let a ← x; pure <| Except.ok a catch ex => pure <| Except.error ex
-  let x : EIO Exception (Eα × Core.State) := (ReaderT.run x (mkCoreContext ctx s heartbeats)).run { env := s.env, ngen := s.ngen, traceState := s.traceState, messages := {}, infoState.enabled := s.infoState.enabled }
+  let env := Kernel.resetDiag s.env
+  let scope := s.scopes.head!
+  let coreCtx : Core.Context := {
+    fileName       := ctx.fileName
+    fileMap        := ctx.fileMap
+    currRecDepth   := ctx.currRecDepth
+    maxRecDepth    := s.maxRecDepth
+    ref            := ctx.ref
+    currNamespace  := scope.currNamespace
+    openDecls      := scope.openDecls
+    initHeartbeats := heartbeats
+    currMacroScope := ctx.currMacroScope
+    options        := scope.opts
+  }
+  let x : EIO _ _ := x.run coreCtx {
+    env
+    ngen := s.ngen
+    nextMacroScope := s.nextMacroScope
+    infoState.enabled := s.infoState.enabled
+    traceState := s.traceState
+  }
   let (ea, coreS) ← liftM x
   modify fun s => { s with
-    env := coreS.env
-    ngen := coreS.ngen
-    messages := s.messages ++ coreS.messages
+    env               := coreS.env
+    nextMacroScope    := coreS.nextMacroScope
+    ngen              := coreS.ngen
+    infoState.trees   := s.infoState.trees.append coreS.infoState.trees
     traceState.traces := coreS.traceState.traces.map fun t => { t with ref := replaceRef t.ref ctx.ref }
-    infoState.trees := s.infoState.trees.append coreS.infoState.trees
+    messages          := s.messages ++ coreS.messages
   }
-  match ea with
-  | Except.ok a    => pure a
-  | Except.error e => throw e
+  return ea
+
+def liftCoreM (x : CoreM α) : CommandElabM α := do
+  MonadExcept.ofExcept (← runCore (observing x))
 
 private def ioErrorToMessage (ctx : Context) (ref : Syntax) (err : IO.Error) : Message :=
   let ref := getBetterRef ref ctx.macroStack
   mkMessageAux ctx ref (toString err) MessageSeverity.error
 
-@[inline] def liftEIO {α} (x : EIO Exception α) : CommandElabM α := liftM x
-
 @[inline] def liftIO {α} (x : IO α) : CommandElabM α := do
   let ctx ← read
   IO.toEIO (fun (ex : IO.Error) => Exception.error ctx.ref ex.toString) x
@@ -269,7 +275,7 @@ private def elabCommandUsing (s : State) (stx : Syntax) : List (KeyedDeclsAttrib
       (fun _ => do set s; elabCommandUsing s stx elabFns)
 
 /-- Elaborate `x` with `stx` on the macro stack -/
-def withMacroExpansion {α} (beforeStx afterStx : Syntax) (x : CommandElabM α) : CommandElabM α :=
+def withMacroExpansion (beforeStx afterStx : Syntax) (x : CommandElabM α) : CommandElabM α :=
   withInfoContext (mkInfo := pure <| .ofMacroExpansionInfo { stx := beforeStx, output := afterStx, lctx := .empty }) do
     withReader (fun ctx => { ctx with macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack }) x
 
@@ -402,7 +408,6 @@ def printExpr (e : Expr) : MetaM Unit := do
 def liftTermElabM (x : TermElabM α) : CommandElabM α := do
   let ctx ← read
   let s   ← get
-  let heartbeats ← IO.getNumHeartbeats
   -- dbg_trace "heartbeats: {heartbeats}"
   let scope := s.scopes.head!
   -- We execute `x` with an empty message log. Thus, `x` cannot modify/view messages produced by previous commands.
@@ -411,18 +416,9 @@ def liftTermElabM (x : TermElabM α) : CommandElabM α := do
   -- make sure `observing` below also catches runtime exceptions (like we do by default in
   -- `CommandElabM`)
   let _ := MonadAlwaysExcept.except (m := TermElabM)
-  let x : MetaM _      := (observing x).run (mkTermContext ctx s) { levelNames := scope.levelNames }
-  let x : CoreM _      := x.run mkMetaContext {}
-  let x : EIO _ _      := x.run (mkCoreContext ctx s heartbeats) { env := s.env, ngen := s.ngen, nextMacroScope := s.nextMacroScope, infoState.enabled := s.infoState.enabled, traceState := s.traceState }
-  let (((ea, _), _), coreS) ← liftEIO x
-  modify fun s => { s with
-    env               := coreS.env
-    nextMacroScope    := coreS.nextMacroScope
-    ngen              := coreS.ngen
-    infoState.trees   := s.infoState.trees.append coreS.infoState.trees
-    traceState.traces := coreS.traceState.traces.map fun t => { t with ref := replaceRef t.ref ctx.ref }
-    messages          := s.messages ++ coreS.messages
-  }
+  let x : MetaM _ := (observing (try x finally Meta.reportDiag)).run (mkTermContext ctx s) { levelNames := scope.levelNames }
+  let x : CoreM _ := x.run mkMetaContext {}
+  let ((ea, _), _) ← runCore x
   MonadExcept.ofExcept ea
 
 /--