chore: update comments in kernel/declaration.h

This file has comments that recall the data type definitions in Lean.
Most of them were still using lean3 syntax, and at least one of them was
out of date (one field missing), so I updated them.

I took the liberty to shorten the comments from the original file, or
omit them if they don’t add much over the field names.

.github/workflows/ci.yml

@@ -9,6 +9,17 @@ on:
   merge_group:
   schedule:
     - cron: '0 7 * * *'  # 8AM CET/11PM PT
+  # for manual re-release of a nightly
+  workflow_dispatch:
+    inputs:
+      action:
+        description: 'Action'
+        required: true
+        default: 'release nightly'
+        type: choice
+        options:
+        - release nightly
+
 
 concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}-${{ github.event_name }}
@@ -43,9 +54,9 @@ jobs:
       - name: Checkout
         uses: actions/checkout@v3
         # don't schedule nightlies on forks
-        if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4'
+        if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4' || inputs.action == 'release nightly'
       - name: Set Nightly
-        if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4'
+        if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4' || inputs.action == 'release nightly'
         id: set-nightly
         run: |
           if [[ -n '${{ secrets.PUSH_NIGHTLY_TOKEN }}' ]]; then
@@ -470,6 +481,11 @@ jobs:
           prerelease: ${{ !startsWith(github.ref, 'refs/tags/v') || contains(github.ref, '-rc') }}
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+      - name: Update release.lean-lang.org
+        run: |
+          gh workflow -R leanprover/release-index run update-index.yml
+        env:
+          GITHUB_TOKEN: ${{ secrets.RELEASE_INDEX_TOKEN }}
 
   # This job creates nightly releases during the cron job.
   # It is responsible for creating the tag, and automatically generating a changelog.
@@ -512,3 +528,8 @@ jobs:
           repository: ${{ github.repository_owner }}/lean4-nightly
         env:
           GITHUB_TOKEN: ${{ secrets.PUSH_NIGHTLY_TOKEN }}
+      - name: Update release.lean-lang.org
+        run: |
+          gh workflow -R leanprover/release-index run update-index.yml
+        env:
+          GITHUB_TOKEN: ${{ secrets.RELEASE_INDEX_TOKEN }}

.github/workflows/pr-release.yml

@@ -328,7 +328,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 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
+            sed -i 's,require "leanprover-community" / "batteries" @ ".\+",require "leanprover-community" / "batteries" @ "git#nightly-testing-'"${MOST_RECENT_NIGHTLY}"'",' lakefile.lean
             lake update batteries
             git add lakefile.lean lake-manifest.json
             git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"

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

@@ -20,10 +20,12 @@ jobs:
         gh run view "$run_id"
         echo "Cancelling (just in case)"
         gh run cancel "$run_id" || echo "(failed)"
-        echo "Waiting for 10s"
-        sleep 10
+        echo "Waiting for 30s"
+        sleep 30
+        gh run view "$run_id"
         echo "Rerunning"
         gh run rerun "$run_id"
+        gh run view "$run_id"
       shell: bash
       env:
         head_ref: ${{ github.head_ref }}

RELEASES.md

@@ -8,13 +8,326 @@ 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.10.0
+v4.11.0
 ----------
 Development in progress.
 
+v4.10.0
+----------
+Release candidate, release notes will be copied from branch `releases/v4.10.0` once completed.
+
 v4.9.0
 ---------- 
-Release candidate, release notes will be copied from branch `releases/v4.9.0` once completed.
+
+### Language features, tactics, and metaprograms
+
+* **Definition transparency**
+  * [#4053](https://github.com/leanprover/lean4/pull/4053) adds the `seal` and `unseal` commands, which make definitions locally be irreducible or semireducible.
+  * [#4061](https://github.com/leanprover/lean4/pull/4061) marks functions defined by well-founded recursion with `@[irreducible]` by default,
+    which should prevent the expensive and often unfruitful unfolding of such definitions (see breaking changes below).
+* **Incrementality**
+  * [#3940](https://github.com/leanprover/lean4/pull/3940) extends incremental elaboration into various steps inside of declarations:
+    definition headers, bodies, and tactics.
+    ![Recording 2024-05-10](https://github.com/leanprover/lean4/assets/109126/c9d67b6f-c131-4bc3-a0de-7d63eaf1bfc9).
+  * [250994](https://github.com/leanprover/lean4/commit/250994166ce036ab8644e459129f51ea79c1c2d2)
+    and [67338b](https://github.com/leanprover/lean4/commit/67338bac2333fa39a8656e8f90574784e4c23d3d)
+    add `@[incremental]` attribute to mark an elaborator as supporting incremental elaboration.
+  * [#4259](https://github.com/leanprover/lean4/pull/4259) improves resilience by ensuring incremental commands and tactics are reached only in supported ways.
+  * [#4268](https://github.com/leanprover/lean4/pull/4268) adds special handling for `:= by` so that stray tokens in tactic blocks do not inhibit incrementality.
+  * [#4308](https://github.com/leanprover/lean4/pull/4308) adds incremental `have` tactic.
+  * [#4340](https://github.com/leanprover/lean4/pull/4340) fixes incorrect info tree reuse.
+  * [#4364](https://github.com/leanprover/lean4/pull/4364) adds incrementality for careful command macros such as `set_option in theorem`, `theorem foo.bar`, and `lemma`.
+  * [#4395](https://github.com/leanprover/lean4/pull/4395) adds conservative fix for whitespace handling to avoid incremental reuse leading to goals in front of the text cursor being shown.
+  * [#4407](https://github.com/leanprover/lean4/pull/4407) fixes non-incremental commands in macros blocking further incremental reporting.
+  * [#4436](https://github.com/leanprover/lean4/pull/4436) fixes incremental reporting when there are nested tactics in terms.
+* **Functional induction**
+  * [#4135](https://github.com/leanprover/lean4/pull/4135) ensures that the names used for functional induction are reserved.
+  * [#4327](https://github.com/leanprover/lean4/pull/4327) adds support for structural recursion on reflexive types.
+    For example,
+    ```lean4
+    inductive Many (α : Type u) where
+      | none : Many α
+      | more : α → (Unit → Many α) → Many α
+
+    def Many.map {α β : Type u} (f : α → β) : Many α → Many β
+      | .none => .none
+      | .more x xs => .more (f x) (fun _ => (xs ()).map f)
+
+    #check Many.map.induct
+    /-
+    Many.map.induct {α β : Type u} (f : α → β) (motive : Many α → Prop)
+      (case1 : motive Many.none)
+      (case2 : ∀ (x : α) (xs : Unit → Many α), motive (xs ()) → motive (Many.more x xs)) :
+      ∀ (a : Many α), motive a
+    -/
+    ```
+* [#3903](https://github.com/leanprover/lean4/pull/3903) makes the Lean frontend normalize all line endings to LF before processing.
+  This lets Lean be insensitive to CRLF vs LF line endings, improving the cross-platform experience and making Lake hashes be faithful to what Lean processes.
+* [#4130](https://github.com/leanprover/lean4/pull/4130) makes the tactic framework be able to recover from runtime errors (for example, deterministic timeouts or maximum recursion depth errors).
+* `split` tactic
+  * [#4211](https://github.com/leanprover/lean4/pull/4211) fixes `split at h` when `h` has forward dependencies.
+  * [#4349](https://github.com/leanprover/lean4/pull/4349) allows `split` for `if`-expressions to work on non-propositional goals.
+* `apply` tactic
+  * [#3929](https://github.com/leanprover/lean4/pull/3929) makes error message for `apply` show implicit arguments in unification errors as needed.
+    Modifies `MessageData` type (see breaking changes below).
+* `cases` tactic
+  * [#4224](https://github.com/leanprover/lean4/pull/4224) adds support for unification of offsets such as `x + 20000 = 20001` in `cases` tactic.
+* `omega` tactic
+  * [#4073](https://github.com/leanprover/lean4/pull/4073) lets `omega` fall back to using classical `Decidable` instances when setting up contradiction proofs.
+  * [#4141](https://github.com/leanprover/lean4/pull/4141) and [#4184](https://github.com/leanprover/lean4/pull/4184) fix bugs.
+  * [#4264](https://github.com/leanprover/lean4/pull/4264) improves `omega` error message if no facts found in local context.
+  * [#4358](https://github.com/leanprover/lean4/pull/4358) improves expression matching in `omega` by using `match_expr`.
+* `simp` tactic
+  * [#4176](https://github.com/leanprover/lean4/pull/4176) makes names of erased lemmas clickable.
+  * [#4208](https://github.com/leanprover/lean4/pull/4208) adds a pretty printer for discrimination tree keys.
+  * [#4202](https://github.com/leanprover/lean4/pull/4202) adds `Simp.Config.index` configuration option,
+    which controls whether to use the full discrimination tree when selecting candidate simp lemmas.
+    When `index := false`, only the head function is taken into account, like in Lean 3.
+    This feature can help users diagnose tricky simp failures or issues in code from libraries
+    developed using Lean 3 and then ported to Lean 4.
+    
+    In the following example, it will report that `foo` is a problematic theorem.
+    ```lean
+    opaque f : Nat → Nat → Nat
+
+    @[simp] theorem foo : f x (x, y).2 = y := by sorry
+
+    example : f a b ≤ b := by
+      set_option diagnostics true in
+      simp (config := { index := false })
+    /-
+    [simp] theorems with bad keys
+      foo, key: f _ (@Prod.mk ℕ ℕ _ _).2
+    -/
+    ```
+    With the information above, users can annotate theorems such as `foo` using `no_index` for problematic subterms. Example:
+    ```lean
+    opaque f : Nat → Nat → Nat
+
+    @[simp] theorem foo : f x (no_index (x, y).2) = y := by sorry
+    
+    example : f a b ≤ b := by
+      simp -- `foo` is still applied with `index := true`
+    ```
+  * [#4274](https://github.com/leanprover/lean4/pull/4274) prevents internal `match` equational theorems from appearing in simp trace.
+  * [#4177](https://github.com/leanprover/lean4/pull/4177) and [#4359](https://github.com/leanprover/lean4/pull/4359) make `simp` continue even if a simp lemma does not elaborate, if the tactic state is in recovery mode.
+  * [#4341](https://github.com/leanprover/lean4/pull/4341) fixes panic when applying `@[simp]` to malformed theorem syntax.
+  * [#4345](https://github.com/leanprover/lean4/pull/4345) fixes `simp` so that it does not use the forward version of a user-specified backward theorem.
+  * [#4352](https://github.com/leanprover/lean4/pull/4352) adds missing `dsimp` simplifications for fixed parameters of generated congruence theorems.
+  * [#4362](https://github.com/leanprover/lean4/pull/4362) improves trace messages for `simp` so that constants are hoverable.
+* **Elaboration**
+  * [#4046](https://github.com/leanprover/lean4/pull/4046) makes subst notation (`he ▸ h`) try rewriting in both directions even when there is no expected type available.
+  * [#3328](https://github.com/leanprover/lean4/pull/3328) adds support for identifiers in autoparams (for example, `rfl` in `(h : x = y := by exact rfl)`).
+  * [#4096](https://github.com/leanprover/lean4/pull/4096) changes how the type in `let` and `have` is elaborated, requiring that any tactics in the type be evaluated before proceeding, improving performance.
+  * [#4215](https://github.com/leanprover/lean4/pull/4215) ensures the expression tree elaborator commits to the computed "max type" for the entire arithmetic expression.
+  * [#4267](https://github.com/leanprover/lean4/pull/4267) cases signature elaboration errors to show even if there are parse errors in the body.
+  * [#4368](https://github.com/leanprover/lean4/pull/4368) improves error messages when numeric literals fail to synthesize an `OfNat` instance,
+    including special messages warning when the expected type of the numeral can be a proposition.
+* **Metaprogramming**
+  * [#4167](https://github.com/leanprover/lean4/pull/4167) adds `Lean.MVarId.revertAll` to revert all free variables.
+  * [#4169](https://github.com/leanprover/lean4/pull/4169) adds `Lean.MVarId.ensureNoMVar` to ensure the goal's target contains no expression metavariables.
+  * [#4180](https://github.com/leanprover/lean4/pull/4180) adds `cleanupAnnotations` parameter to `forallTelescope` methods.
+  * [#4307](https://github.com/leanprover/lean4/pull/4307) adds support for parser aliases in syntax quotations.
+* Work toward implementing `grind` tactic
+  * [0a515e](https://github.com/leanprover/lean4/commit/0a515e2ec939519dafb4b99daa81d6bf3c411404)
+    and [#4164](https://github.com/leanprover/lean4/pull/4164)
+    add `grind_norm` and `grind_norm_proc` attributes and `@[grind_norm]` theorems.
+  * [#4170](https://github.com/leanprover/lean4/pull/4170), [#4221](https://github.com/leanprover/lean4/pull/4221),
+    and [#4249](https://github.com/leanprover/lean4/pull/4249) create `grind` preprocessor and core module.
+  * [#4235](https://github.com/leanprover/lean4/pull/4235) and [d6709e](https://github.com/leanprover/lean4/commit/d6709eb1576c5d40fc80462637dc041f970e4d9f)
+    add special `cases` tactic to `grind` along with `@[grind_cases]` attribute to mark types that this `cases` tactic should automatically apply to.
+  * [#4243](https://github.com/leanprover/lean4/pull/4243) adds special `injection?` tactic to `grind`.
+* **Other fixes or improvements**
+  * [#4065](https://github.com/leanprover/lean4/pull/4065) fixes a bug in the `Nat.reduceLeDiff` simproc.
+  * [#3969](https://github.com/leanprover/lean4/pull/3969) makes deprecation warnings activate even for generalized field notation ("dot notation").
+  * [#4132](https://github.com/leanprover/lean4/pull/4132) fixes the `sorry` term so that it does not activate the implicit lambda feature
+  * [9803c5](https://github.com/leanprover/lean4/commit/9803c5dd63dc993628287d5f998525e74af03839)
+    and [47c8e3](https://github.com/leanprover/lean4/commit/47c8e340d65b01f4d9f011686e3dda0d4bb30a20)
+    move `cdot` and `calc` parsers to `Lean` namespace.
+  * [#4252](https://github.com/leanprover/lean4/pull/4252) fixes the `case` tactic so that it is usable in macros by having it erase macro scopes from the tag.
+  * [26b671](https://github.com/leanprover/lean4/commit/26b67184222e75529e1b166db050aaebee323d2d)
+    and [cc33c3](https://github.com/leanprover/lean4/commit/cc33c39cb022d8a3166b1e89677c78835ead1fc7)
+    extract `haveId` syntax.
+  * [#4335](https://github.com/leanprover/lean4/pull/4335) fixes bugs in partial `calc` tactic when there is mdata or metavariables.
+  * [#4329](https://github.com/leanprover/lean4/pull/4329) makes `termination_by?` report unused each unused parameter as `_`.
+* **Docs:** [#4238](https://github.com/leanprover/lean4/pull/4238), [#4294](https://github.com/leanprover/lean4/pull/4294),
+  [#4338](https://github.com/leanprover/lean4/pull/4338).
+
+### Language server, widgets, and IDE extensions
+* [#4066](https://github.com/leanprover/lean4/pull/4066) fixes features like "Find References" when browsing core Lean sources.
+* [#4254](https://github.com/leanprover/lean4/pull/4254) allows embedding user widgets in structured messages.
+  Companion PR is [vscode-lean4#449](https://github.com/leanprover/vscode-lean4/pull/449).
+* [#4445](https://github.com/leanprover/lean4/pull/4445) makes watchdog more resilient against badly behaving clients.
+
+### Library
+* [#4059](https://github.com/leanprover/lean4/pull/4059) upstreams many `List` and `Array` operations and theorems from Batteries.
+* [#4055](https://github.com/leanprover/lean4/pull/4055) removes the unused `Inhabited` instance for `Subtype`.
+* [#3967](https://github.com/leanprover/lean4/pull/3967) adds dates in existing `@[deprecated]` attributes.
+* [#4231](https://github.com/leanprover/lean4/pull/4231) adds boilerplate `Char`, `UInt`, and `Fin` theorems.
+* [#4205](https://github.com/leanprover/lean4/pull/4205) fixes the `MonadStore` type classes to use `semiOutParam`.
+* [#4350](https://github.com/leanprover/lean4/pull/4350) renames `IsLawfulSingleton` to `LawfulSingleton`.
+* `Nat`
+  * [#4094](https://github.com/leanprover/lean4/pull/4094) swaps `Nat.zero_or` and `Nat.or_zero`.
+  * [#4098](https://github.com/leanprover/lean4/pull/4098) and [#4145](https://github.com/leanprover/lean4/pull/4145)
+    change the definition of `Nat.mod` so that `n % (m + n)` reduces when `n` is literal without relying on well-founded recursion,
+    which becomes irreducible by default in [#4061](https://github.com/leanprover/lean4/pull/4061).
+  * [#4188](https://github.com/leanprover/lean4/pull/4188) redefines `Nat.testBit` to be more performant.
+  * Theorems: [#4199](https://github.com/leanprover/lean4/pull/4199).
+* `Array`
+  * [#4074](https://github.com/leanprover/lean4/pull/4074) improves the functional induction principle `Array.feraseIdx.induct`.
+* `List`
+  * [#4172](https://github.com/leanprover/lean4/pull/4172) removes `@[simp]` from `List.length_pos`.
+* `Option`
+  * [#4037](https://github.com/leanprover/lean4/pull/4037) adds theorems to simplify `Option`-valued dependent if-then-else.
+  * [#4314](https://github.com/leanprover/lean4/pull/4314) removes `@[simp]` from `Option.bind_eq_some`.
+* `BitVec`
+  * Theorems: [#3920](https://github.com/leanprover/lean4/pull/3920), [#4095](https://github.com/leanprover/lean4/pull/4095),
+    [#4075](https://github.com/leanprover/lean4/pull/4075), [#4148](https://github.com/leanprover/lean4/pull/4148),
+    [#4165](https://github.com/leanprover/lean4/pull/4165), [#4178](https://github.com/leanprover/lean4/pull/4178),
+    [#4200](https://github.com/leanprover/lean4/pull/4200), [#4201](https://github.com/leanprover/lean4/pull/4201),
+    [#4298](https://github.com/leanprover/lean4/pull/4298), [#4299](https://github.com/leanprover/lean4/pull/4299),
+    [#4257](https://github.com/leanprover/lean4/pull/4257), [#4179](https://github.com/leanprover/lean4/pull/4179),
+    [#4321](https://github.com/leanprover/lean4/pull/4321), [#4187](https://github.com/leanprover/lean4/pull/4187).
+  * [#4193](https://github.com/leanprover/lean4/pull/4193) adds simprocs for reducing `x >>> i` and `x <<< i` where `i` is a bitvector literal.
+  * [#4194](https://github.com/leanprover/lean4/pull/4194) adds simprocs for reducing `(x <<< i) <<< j` and `(x >>> i) >>> j` where `i` and `j` are natural number literals.
+  * [#4229](https://github.com/leanprover/lean4/pull/4229) redefines `rotateLeft`/`rotateRight` to use modulo reduction of shift offset.
+  * [0d3051](https://github.com/leanprover/lean4/commit/0d30517dca094a07bcb462252f718e713b93ffba) makes `<num>#<term>` bitvector literal notation global.
+* `Char`/`String`
+  * [#4143](https://github.com/leanprover/lean4/pull/4143) modifies `String.substrEq` to avoid linter warnings in downstream code.
+  * [#4233](https://github.com/leanprover/lean4/pull/4233) adds simprocs for `Char` and `String` inequalities.
+  * [#4348](https://github.com/leanprover/lean4/pull/4348) upstreams Mathlib lemmas.
+  * [#4354](https://github.com/leanprover/lean4/pull/4354) upstreams basic `String` lemmas.
+* `HashMap`
+  * [#4248](https://github.com/leanprover/lean4/pull/4248) fixes implicitness of typeclass arguments in `HashMap.ofList`.
+* `IO`
+  * [#4036](https://github.com/leanprover/lean4/pull/4036) adds `IO.Process.getCurrentDir` and `IO.Process.setCurrentDir` for adjusting the current process's working directory.
+* **Cleanup:** [#4077](https://github.com/leanprover/lean4/pull/4077), [#4189](https://github.com/leanprover/lean4/pull/4189),
+  [#4304](https://github.com/leanprover/lean4/pull/4304).
+* **Docs:** [#4001](https://github.com/leanprover/lean4/pull/4001), [#4166](https://github.com/leanprover/lean4/pull/4166),
+  [#4332](https://github.com/leanprover/lean4/pull/4332).
+
+### Lean internals
+* **Defeq and WHNF algorithms**
+  * [#4029](https://github.com/leanprover/lean4/pull/4029) remove unnecessary `checkpointDefEq`
+  * [#4206](https://github.com/leanprover/lean4/pull/4206) fixes `isReadOnlyOrSyntheticOpaque` to respect metavariable depth.
+  * [#4217](https://github.com/leanprover/lean4/pull/4217) fixes missing occurs check for delayed assignments.
+* **Definition transparency**
+  * [#4052](https://github.com/leanprover/lean4/pull/4052) adds validation to application of `@[reducible]`/`@[semireducible]`/`@[irreducible]` attributes (with `local`/`scoped` modifiers as well).
+    Setting `set_option allowUnsafeReductibility true` turns this validation off.
+* **Inductive types**
+  * [#3591](https://github.com/leanprover/lean4/pull/3591) fixes a bug where indices could be incorrectly promoted to parameters.
+  * [#3398](https://github.com/leanprover/lean4/pull/3398) fixes a bug in the injectivity theorem generator.
+  * [#4342](https://github.com/leanprover/lean4/pull/4342) fixes elaboration of mutual inductives with instance parameters.
+* **Diagnostics and profiling**
+  * [#3986](https://github.com/leanprover/lean4/pull/3986) adds option `trace.profiler.useHeartbeats` to switch `trace.profiler.threshold` to being in terms of heartbeats instead of milliseconds.
+  * [#4082](https://github.com/leanprover/lean4/pull/4082) makes `set_option diagnostics true` report kernel diagnostic information.
+* **Typeclass resolution**
+  * [#4119](https://github.com/leanprover/lean4/pull/4119) fixes multiple issues with TC caching interacting with `synthPendingDepth`, adds `maxSynthPendingDepth` option with default value `1`.
+  * [#4210](https://github.com/leanprover/lean4/pull/4210) ensures local instance cache does not contain multiple copies of the same instance.
+  * [#4216](https://github.com/leanprover/lean4/pull/4216) fix handling of metavariables, to avoid needing to set the option `backward.synthInstance.canonInstances` to `false`.
+* **Other fixes or improvements**
+  * [#4080](https://github.com/leanprover/lean4/pull/4080) fixes propagation of state for `Lean.Elab.Command.liftCoreM` and `Lean.Elab.Command.liftTermElabM`.
+  * [#3944](https://github.com/leanprover/lean4/pull/3944) makes the `Repr` deriving handler be consistent between `structure` and `inductive` for how types and proofs are erased.
+  * [#4113](https://github.com/leanprover/lean4/pull/4113) propagates `maxHeartbeats` to kernel to control "(kernel) deterministic timeout" error.
+  * [#4125](https://github.com/leanprover/lean4/pull/4125) reverts [#3970](https://github.com/leanprover/lean4/pull/3970) (monadic generalization of `FindExpr`).
+  * [#4128](https://github.com/leanprover/lean4/pull/4128) catches stack overflow in auto-bound implicits feature.
+  * [#4129](https://github.com/leanprover/lean4/pull/4129) adds `tryCatchRuntimeEx` combinator to replace `catchRuntimeEx` reader state.
+  * [#4155](https://github.com/leanprover/lean4/pull/4155) simplifies the expression canonicalizer.
+  * [#4151](https://github.com/leanprover/lean4/pull/4151) and [#4369](https://github.com/leanprover/lean4/pull/4369)
+    add many missing trace classes.
+  * [#4185](https://github.com/leanprover/lean4/pull/4185) makes congruence theorem generators clean up type annotations of argument types.
+  * [#4192](https://github.com/leanprover/lean4/pull/4192) fixes restoration of infotrees when auto-bound implicit feature is activated,
+    fixing a pretty printing error in hovers and strengthening the unused variable linter.
+  * [dfb496](https://github.com/leanprover/lean4/commit/dfb496a27123c3864571aec72f6278e2dad1cecf) fixes `declareBuiltin` to allow it to be called multiple times per declaration.
+  * Cleanup: [#4112](https://github.com/leanprover/lean4/pull/4112), [#4126](https://github.com/leanprover/lean4/pull/4126), [#4091](https://github.com/leanprover/lean4/pull/4091), [#4139](https://github.com/leanprover/lean4/pull/4139), [#4153](https://github.com/leanprover/lean4/pull/4153).
+  * Tests: [030406](https://github.com/leanprover/lean4/commit/03040618b8f9b35b7b757858483e57340900cdc4), [#4133](https://github.com/leanprover/lean4/pull/4133).
+
+### Compiler, runtime, and FFI
+* [#4100](https://github.com/leanprover/lean4/pull/4100) improves reset/reuse algorithm; it now runs a second pass relaxing the constraint that reused memory cells must only be for the exact same constructor.
+* [#2903](https://github.com/leanprover/lean4/pull/2903) fixes segfault in old compiler from mishandling `noConfusion` applications.
+* [#4311](https://github.com/leanprover/lean4/pull/4311) fixes bug in constant folding.
+* [#3915](https://github.com/leanprover/lean4/pull/3915) documents the runtime memory layout for inductive types.
+
+### Lake
+* [#4057](https://github.com/leanprover/lean4/pull/4057) adds support for docstrings on `require` commands.
+* [#4088](https://github.com/leanprover/lean4/pull/4088) improves hovers for `family_def` and `library_data` commands.
+* [#4147](https://github.com/leanprover/lean4/pull/4147) adds default `README.md` to package templates
+* [#4261](https://github.com/leanprover/lean4/pull/4261) extends `lake test` help page, adds help page for `lake check-test`,
+  adds `lake lint` and tag `@[lint_driver]`, adds support for specifying test and lint drivers from dependencies,
+  adds `testDriverArgs` and `lintDriverArgs` options, adds support for library test drivers,
+  makes `lake check-test` and `lake check-lint` only load the package without dependencies.
+* [#4270](https://github.com/leanprover/lean4/pull/4270) adds `lake pack` and `lake unpack` for packing and unpacking Lake build artifacts from an archive.
+* [#4083](https://github.com/leanprover/lean4/pull/4083)
+  Switches the manifest format to use `major.minor.patch` semantic
+  versions. Major version increments indicate breaking changes (e.g., new
+  required fields and semantic changes to existing fields). Minor version
+  increments (after `0.x`) indicate backwards-compatible extensions (e.g.,
+  adding optional fields, removing fields). This change is backwards
+  compatible. Lake will still successfully read old manifests with numeric
+  versions. It will treat the numeric version `N` as semantic version
+  `0.N.0`. Lake will also accept manifest versions with `-` suffixes
+  (e.g., `x.y.z-foo`) and then ignore the suffix.
+* [#4273](https://github.com/leanprover/lean4/pull/4273) adds a lift from `JobM` to `FetchM` for backwards compatibility reasons.
+* [#4351](https://github.com/leanprover/lean4/pull/4351) fixes `LogIO`-to-`CliM`-lifting performance issues.
+* [#4343](https://github.com/leanprover/lean4/pull/4343) make Lake store the dependency trace for a build in
+  the cached build long and then verifies that it matches the trace of the current build before replaying the log.
+* [#4402](https://github.com/leanprover/lean4/pull/4402) moves the cached log into the trace file (no more `.log.json`).
+  This means logs are no longer cached on fatal errors and this ensures that an out-of-date log is not associated with an up-to-date trace.
+  Separately, `.hash` file generation was changed to be more reliable as well.
+  The `.hash` files are deleted as part of the build and always regenerate with `--rehash`.
+* **Other fixes or improvements**
+  * [#4056](https://github.com/leanprover/lean4/pull/4056) cleans up tests
+  * [#4244](https://github.com/leanprover/lean4/pull/4244) fixes `noRelease` test when Lean repo is tagged
+  * [#4346](https://github.com/leanprover/lean4/pull/4346) improves `tests/serve`
+  * [#4356](https://github.com/leanprover/lean4/pull/4356) adds build log path to the warning for a missing or invalid build log.
+
+### DevOps
+* [#3984](https://github.com/leanprover/lean4/pull/3984) adds a script (`script/rebase-stage0.sh`) for `git rebase -i` that automatically updates each stage0.
+* [#4108](https://github.com/leanprover/lean4/pull/4108) finishes renamings from transition to Std to Batteries.
+* [#4109](https://github.com/leanprover/lean4/pull/4109) adjusts the Github bug template to mention testing using [live.lean-lang.org](https://live.lean-lang.org).
+* [#4136](https://github.com/leanprover/lean4/pull/4136) makes CI rerun only when `full-ci` label is added or removed.
+* [#4175](https://github.com/leanprover/lean4/pull/4175) and [72b345](https://github.com/leanprover/lean4/commit/72b345c621a9a06d3a5a656da2b793a5eea5f168)
+  switch to using `#guard_msgs` to run tests as much as possible.
+* [#3125](https://github.com/leanprover/lean4/pull/3125) explains the Lean4 `pygments` lexer.
+* [#4247](https://github.com/leanprover/lean4/pull/4247) sets up a procedure for preparing release notes.
+* [#4032](https://github.com/leanprover/lean4/pull/4032) modernizes build instructions and workflows.
+* [#4255](https://github.com/leanprover/lean4/pull/4255) moves some expensive checks from merge queue to releases.
+* [#4265](https://github.com/leanprover/lean4/pull/4265) adds aarch64 macOS as native compilation target for CI.
+* [f05a82](https://github.com/leanprover/lean4/commit/f05a82799a01569edeb5e2594cd7d56282320f9e) restores macOS aarch64 install suffix in CI
+* [#4317](https://github.com/leanprover/lean4/pull/4317) updates build instructions for macOS.
+* [#4333](https://github.com/leanprover/lean4/pull/4333) adjusts workflow to update Batteries in manifest when creating `lean-pr-testing-NNNN` Mathlib branches.
+* [#4355](https://github.com/leanprover/lean4/pull/4355) simplifies `lean4checker` step of release checklist.
+* [#4361](https://github.com/leanprover/lean4/pull/4361) adds installing elan to `pr-release` CI step.
+
+### Breaking changes
+While most changes could be considered to be a breaking change, this section makes special note of API changes.
+
+* `Nat.zero_or` and `Nat.or_zero` have been swapped ([#4094](https://github.com/leanprover/lean4/pull/4094)).
+* `IsLawfulSingleton` is now `LawfulSingleton` ([#4350](https://github.com/leanprover/lean4/pull/4350)).
+* `BitVec.rotateLeft` and `BitVec.rotateRight` now take the shift modulo the bitwidth ([#4229](https://github.com/leanprover/lean4/pull/4229)).
+* These are no longer simp lemmas:
+  `List.length_pos` ([#4172](https://github.com/leanprover/lean4/pull/4172)),
+  `Option.bind_eq_some` ([#4314](https://github.com/leanprover/lean4/pull/4314)).
+* Types in `let` and `have` (both the expressions and tactics) may fail to elaborate due to new restrictions on what sorts of elaboration problems may be postponed ([#4096](https://github.com/leanprover/lean4/pull/4096)).
+  In particular, tactics embedded in the type will no longer make use of the type of `value` in expressions such as `let x : type := value; body`.
+* Now functions defined by well-founded recursion are marked with `@[irreducible]` by default ([#4061](https://github.com/leanprover/lean4/pull/4061)).
+  Existing proofs that hold by definitional equality (e.g. `rfl`) can be
+  rewritten to explictly unfold the function definition (using `simp`,
+  `unfold`, `rw`), or the recursive function can be temporarily made
+  semireducible (using `unseal f in` before the command), or the function
+  definition itself can be marked as `@[semireducible]` to get the previous
+  behavior.
+* Due to [#3929](https://github.com/leanprover/lean4/pull/3929):
+  * 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
 ---------

doc/dev/release_checklist.md

@@ -13,13 +13,11 @@ We'll use `v4.6.0` as the intended release version as a running example.
   - `set(LEAN_VERSION_MINOR 6)` (for whichever `6` is appropriate)
   - `set(LEAN_VERSION_IS_RELEASE 1)`
   - (both of these should already be in place from the release candidates)
-- It is possible that the `v4.6.0` section of `RELEASES.md` is out of sync between
-  `releases/v4.6.0` and `master`. This should be reconciled:
-  - Run `git diff master RELEASES.md`.
-  - You should expect to see additons on `master` in the `v4.7.0-rc1` section; ignore these.
-    (i.e. the new release notes for the upcoming release candidate).
-  - Reconcile discrepancies in the `v4.6.0` section,
-    usually via copy and paste and a commit to `releases/v4.6.0`.
+- In `RELEASES.md`, verify that the `v4.6.0` section has been completed during the release candidate cycle.
+  It should be in bullet point form, with a point for every significant PR,
+  and may have a paragraph describing each major new language feature.
+  It should have a "breaking changes" section calling out changes that are specifically likely
+  to cause problems for downstream users.
 - `git tag v4.6.0`
 - `git push $REMOTE v4.6.0`, where `$REMOTE` is the upstream Lean repository (e.g., `origin`, `upstream`)
 - Now wait, while CI runs.
@@ -189,8 +187,12 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
   Please also make sure that whoever is handling social media knows the release is out.
 - Begin the next development cycle (i.e. for `v4.8.0`) on the Lean repository, by making a PR that:
   - Updates `src/CMakeLists.txt` to say `set(LEAN_VERSION_MINOR 8)`
-  - Removes `(in development)` from the section heading in `RELEASES.md` for `v4.7.0`,
-    and creates a new `v4.8.0 (in development)` section heading.
+  - In `RELEASES.md`, update the `v4.7.0` section to say:
+    "Release candidate, release notes will be copied from branch `releases/v4.7.0` once completed."
+    Make sure that whoever is preparing the release notes during this cycle knows that it is their job to do so!
+  - In `RELEASES.md`, update the `v4.8.0` section to say:
+    "Development in progress".
+  - In `RELEASES.md`, verify that the old section `v4.6.0` has the full releases notes from the `releases/v4.6.0` branch.
 
 ## Time estimates:
 Slightly longer than the corresponding steps for a stable release.

nix/bootstrap.nix

@@ -125,8 +125,10 @@ rec {
       leanshared = runCommand "leanshared" { buildInputs = [ stdenv.cc ]; libName = "libleanshared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
         mkdir $out
         LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc -shared ${lib.optionalString stdenv.isLinux "-Wl,-Bsymbolic"} \
-          ${if stdenv.isDarwin then "-Wl,-force_load,${Init.staticLib}/libInit.a -Wl,-force_load,${Lean.staticLib}/libStd.a -Wl,-force_load,${Lean.staticLib}/libLean.a -Wl,-force_load,${leancpp}/lib/lean/libleancpp.a ${leancpp}/lib/libleanrt_initial-exec.a -lc++"
-            else "-Wl,--whole-archive -lInit -lStd -lLean -lleancpp ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive -lstdc++"} -lm ${stdlibLinkFlags} \
+          ${if stdenv.isDarwin
+            then "-Wl,-force_load,${Init.staticLib}/libInit.a -Wl,-force_load,${Std.staticLib}/libStd.a -Wl,-force_load,${Lean.staticLib}/libLean.a -Wl,-force_load,${leancpp}/lib/lean/libleancpp.a ${leancpp}/lib/libleanrt_initial-exec.a -lc++"
+            else "-Wl,--whole-archive -lInit -lStd -lLean -lleancpp ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive -lstdc++"} \
+          -lm ${stdlibLinkFlags} \
           $(${llvmPackages.libllvm.dev}/bin/llvm-config --ldflags --libs) \
           -o $out/$libName
       '';

nix/buildLeanPackage.nix

@@ -224,7 +224,8 @@ with builtins; let
   allLinkFlags = lib.foldr (shared: acc: acc ++ [ "-L${shared}" "-l${shared.linkName or shared.name}" ]) linkFlags allNativeSharedLibs;
 
   objects   = mapAttrs (_: m: m.obj) mods';
-  staticLib = runCommand "${name}-lib" { buildInputs = [ stdenv.cc.bintools.bintools ]; } ''
+  bintools = if stdenv.isDarwin then darwin.cctools else stdenv.cc.bintools.bintools;
+  staticLib = runCommand "${name}-lib" { buildInputs = [ bintools ]; } ''
     mkdir -p $out
     ar Trcs $out/lib${libName}.a ${lib.concatStringsSep " " (map (drv: "${drv}/${drv.oPath}") (attrValues objects))};
   '';

src/CMakeLists.txt

@@ -9,7 +9,7 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 10)
+set(LEAN_VERSION_MINOR 11)
 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'")
@@ -300,11 +300,11 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
     cmake_path(GET ZLIB_LIBRARY PARENT_PATH ZLIB_LIBRARY_PARENT_PATH)
     string(APPEND LEANSHARED_LINKER_FLAGS " -L ${ZLIB_LIBRARY_PARENT_PATH}")
   endif()
-  string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " -lleancpp -lInit -lLean -lleanrt")
+  string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " -lleancpp -lInit -lStd -lLean -lleanrt")
 elseif(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
-  string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " -lleancpp -lInit -lLean -lnodefs.js -lleanrt")
+  string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " -lleancpp -lInit -lStd -lLean -lnodefs.js -lleanrt")
 else()
-  string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " -Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lleanrt -Wl,--end-group")
+  string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " -Wl,--start-group -lleancpp -lLean -Wl,--end-group -lStd -Wl,--start-group -lInit -lleanrt -Wl,--end-group")
 endif()
 
 set(LEAN_CXX_STDLIB "-lstdc++" CACHE STRING "C++ stdlib linker flags")
@@ -313,7 +313,7 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
   set(LEAN_CXX_STDLIB "-lc++")
 endif()
 
-string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " ${LEAN_CXX_STDLIB} -lStd")
+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,
@@ -510,13 +510,13 @@ file(RELATIVE_PATH LIB ${LEAN_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib)
 
 # set up libInit_shared only on Windows; see also stdlib.make.in
 if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
-  set(INIT_SHARED_LINKER_FLAGS "-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libInit.a.export ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a -Wl,--no-whole-archive -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libInit_shared.dll.a")
+  set(INIT_SHARED_LINKER_FLAGS "-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libInit.a.export ${CMAKE_BINARY_DIR}/lib/temp/libStd.a.export ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a -Wl,--no-whole-archive -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libInit_shared.dll.a")
 endif()
 
 if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
   set(LEANSHARED_LINKER_FLAGS "-Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libStd.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
 elseif(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
-  set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libStd.a.export ${CMAKE_BINARY_DIR}/lib/temp/libLean.a.export -lleancpp -Wl,--no-whole-archive -lInit_shared -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a")
+  set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libLean.a.export -lleancpp -Wl,--no-whole-archive -lInit_shared -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a")
 else()
   set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit -lStd -lLean -lleancpp -Wl,--no-whole-archive ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
 endif()

src/Init/Control/Lawful/Instances.lean

@@ -188,7 +188,7 @@ theorem ext {x y : StateT σ m α} (h : ∀ s, x.run s = y.run s) : x = y :=
 
 @[simp] theorem run_lift {α σ : Type u} [Monad m] (x : m α) (s : σ) : (StateT.lift x : StateT σ m α).run s = x >>= fun a => pure (a, s) := rfl
 
-@[simp] theorem run_bind_lift {α σ : Type u} [Monad m] [LawfulMonad m] (x : m α) (f : α → StateT σ m β) (s : σ) : (StateT.lift x >>= f).run s = x >>= fun a => (f a).run s := by
+theorem run_bind_lift {α σ : Type u} [Monad m] [LawfulMonad m] (x : m α) (f : α → StateT σ m β) (s : σ) : (StateT.lift x >>= f).run s = x >>= fun a => (f a).run s := by
   simp [StateT.lift, StateT.run, bind, StateT.bind]
 
 @[simp] theorem run_monadLift {α σ : Type u} [Monad m] [MonadLiftT n m] (x : n α) (s : σ) : (monadLift x : StateT σ m α).run s = (monadLift x : m α) >>= fun a => pure (a, s) := rfl

src/Init/Data/Array.lean

@@ -10,5 +10,6 @@ import Init.Data.Array.BinSearch
 import Init.Data.Array.InsertionSort
 import Init.Data.Array.DecidableEq
 import Init.Data.Array.Mem
+import Init.Data.Array.Attach
 import Init.Data.Array.BasicAux
 import Init.Data.Array.Lemmas

src/Init/Data/Array/Attach.lean

@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2021 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner, Mario Carneiro
+-/
+prelude
+import Init.Data.Array.Mem
+import Init.Data.List.Attach
+
+namespace Array
+
+/--
+Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of
+`Array {x // P x}` is the same as the input `Array α`.
+-/
+@[inline] private unsafe def attachWithImpl
+    (xs : Array α) (P : α → Prop) (_ : ∀ x ∈ xs, P x) : Array {x // P x} := unsafeCast xs
+
+/-- `O(1)`. "Attach" a proof `P x` that holds for all the elements of `xs` to produce a new array
+  with the same elements but in the type `{x // P x}`. -/
+@[implemented_by attachWithImpl] def attachWith
+    (xs : Array α) (P : α → Prop) (H : ∀ x ∈ xs, P x) : Array {x // P x} :=
+  ⟨xs.data.attachWith P fun x h => H x (Array.Mem.mk h)⟩
+
+/-- `O(1)`. "Attach" the proof that the elements of `xs` are in `xs` to produce a new array
+  with the same elements but in the type `{x // x ∈ xs}`. -/
+@[inline] def attach (xs : Array α) : Array {x // x ∈ xs} := xs.attachWith _ fun _ => id
+
+end Array

src/Init/Data/Array/Basic.lean

@@ -60,8 +60,6 @@ def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
 instance : GetElem (Array α) USize α fun xs i => i.toNat < xs.size where
   getElem xs i h := xs.uget i h
 
-instance : LawfulGetElem (Array α) USize α fun xs i => i.toNat < xs.size where
-
 def back [Inhabited α] (a : Array α) : α :=
   a.get! (a.size - 1)
 

src/Init/Data/Array/Lemmas.lean

@@ -220,7 +220,7 @@ theorem getElem?_len_le (a : Array α) {i : Nat} (h : a.size ≤ i) : a[i]? = no
 theorem getD_get? (a : Array α) (i : Nat) (d : α) :
   Option.getD a[i]? d = if p : i < a.size then a[i]'p else d := by
   if h : i < a.size then
-    simp [setD, h, getElem?]
+    simp [setD, h, getElem?_def]
   else
     have p : i ≥ a.size := Nat.le_of_not_gt h
     simp [setD, getElem?_len_le _ p, h]
@@ -383,18 +383,18 @@ theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x el
   | 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]
+    simp [getElem?_def, 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]
+    simp only [getElem?_def, 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 only [getElem?_def, 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
 

src/Init/Data/Array/Mem.lean

@@ -23,7 +23,7 @@ theorem sizeOf_lt_of_mem [SizeOf α] {as : Array α} (h : a ∈ as) : sizeOf a <
   cases as with | _ as =>
   exact Nat.lt_trans (List.sizeOf_lt_of_mem h.val) (by simp_arith)
 
-@[simp] theorem sizeOf_get [SizeOf α] (as : Array α) (i : Fin as.size) : sizeOf (as.get i) < sizeOf as := by
+theorem sizeOf_get [SizeOf α] (as : Array α) (i : Fin as.size) : sizeOf (as.get i) < sizeOf as := by
   cases as with | _ as =>
   exact Nat.lt_trans (List.sizeOf_get ..) (by simp_arith)
 

src/Init/Data/Array/Subarray.lean

@@ -47,8 +47,6 @@ def get (s : Subarray α) (i : Fin s.size) : α :=
 instance : GetElem (Subarray α) Nat α fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
-instance : LawfulGetElem (Subarray α) Nat α fun xs i => i < xs.size where
-
 @[inline] def getD (s : Subarray α) (i : Nat) (v₀ : α) : α :=
   if h : i < s.size then s.get ⟨i, h⟩ else v₀
 

src/Init/Data/Array/TakeDrop.lean

@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+prelude
+import Init.Data.Array.Lemmas
+import Init.Data.List.TakeDrop
+
+namespace Array
+
+theorem exists_of_uset (self : Array α) (i d h) :
+    ∃ l₁ l₂, self.data = l₁ ++ self[i] :: l₂ ∧ List.length l₁ = i.toNat ∧
+      (self.uset i d h).data = l₁ ++ d :: l₂ := by
+  simpa [Array.getElem_eq_data_getElem] using List.exists_of_set _
+
+end Array

src/Init/Data/BEq.lean

@@ -0,0 +1,60 @@
+/-
+Copyright (c) 2022 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, Markus Himmel
+-/
+prelude
+import Init.Data.Bool
+
+set_option linter.missingDocs true
+
+/-- `PartialEquivBEq α` says that the `BEq` implementation is a
+partial equivalence relation, that is:
+* it is symmetric: `a == b → b == a`
+* it is transitive: `a == b → b == c → a == c`.
+-/
+class PartialEquivBEq (α) [BEq α] : Prop where
+  /-- Symmetry for `BEq`. If `a == b` then `b == a`. -/
+  symm : (a : α) == b → b == a
+  /-- Transitivity for `BEq`. If `a == b` and `b == c` then `a == c`. -/
+  trans : (a : α) == b → b == c → a == c
+
+/-- `ReflBEq α` says that the `BEq` implementation is reflexive. -/
+class ReflBEq (α) [BEq α] : Prop where
+  /-- Reflexivity for `BEq`. -/
+  refl : (a : α) == a
+
+/-- `EquivBEq` says that the `BEq` implementation is an equivalence relation. -/
+class EquivBEq (α) [BEq α] extends PartialEquivBEq α, ReflBEq α : Prop
+
+@[simp]
+theorem BEq.refl [BEq α] [ReflBEq α] {a : α} : a == a :=
+  ReflBEq.refl
+
+theorem beq_of_eq [BEq α] [ReflBEq α] {a b : α} : a = b → a == b
+  | rfl => BEq.refl
+
+theorem BEq.symm [BEq α] [PartialEquivBEq α] {a b : α} : a == b → b == a :=
+  PartialEquivBEq.symm
+
+theorem BEq.comm [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = (b == a) :=
+  Bool.eq_iff_iff.2 ⟨BEq.symm, BEq.symm⟩
+
+theorem BEq.symm_false [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = false → (b == a) = false :=
+  BEq.comm (α := α) ▸ id
+
+theorem BEq.trans [BEq α] [PartialEquivBEq α] {a b c : α} : a == b → b == c → a == c :=
+  PartialEquivBEq.trans
+
+theorem BEq.neq_of_neq_of_beq [BEq α] [PartialEquivBEq α] {a b c : α} :
+    (a == b) = false → b == c → (a == c) = false :=
+  fun h₁ h₂ => Bool.eq_false_iff.2 fun h₃ => Bool.eq_false_iff.1 h₁ (BEq.trans h₃ (BEq.symm h₂))
+
+theorem BEq.neq_of_beq_of_neq [BEq α] [PartialEquivBEq α] {a b c : α} :
+    a == b → (b == c) = false → (a == c) = false :=
+  fun h₁ h₂ => Bool.eq_false_iff.2 fun h₃ => Bool.eq_false_iff.1 h₂ (BEq.trans (BEq.symm h₁) h₃)
+
+instance (priority := low) [BEq α] [LawfulBEq α] : EquivBEq α where
+  refl := LawfulBEq.rfl
+  symm h := (beq_iff_eq _ _).2 <| Eq.symm <| (beq_iff_eq _ _).1 h
+  trans hab hbc := (beq_iff_eq _ _).2 <| ((beq_iff_eq _ _).1 hab).trans <| (beq_iff_eq _ _).1 hbc

src/Init/Data/BitVec/Bitblast.lean

@@ -159,6 +159,21 @@ 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]
 
+/-- Addition of bitvectors is the same as bitwise or, if bitwise and is zero. -/
+theorem add_eq_or_of_and_eq_zero {w : Nat} (x y : BitVec w)
+    (h : x &&& y = 0#w) : x + y = x ||| y := by
+  rw [add_eq_adc, adc, iunfoldr_replace (fun _ => false) (x ||| y)]
+  · rfl
+  · simp only [adcb, atLeastTwo, Bool.and_false, Bool.or_false, bne_false, getLsb_or,
+    Prod.mk.injEq, and_eq_false_imp]
+    intros i
+    replace h : (x &&& y).getLsb i = (0#w).getLsb i := by rw [h]
+    simp only [getLsb_and, getLsb_zero, and_eq_false_imp] at h
+    constructor
+    · intros hx
+      simp_all [hx]
+    · by_cases hx : x.getLsb i <;> simp_all [hx]
+
 /-! ### Negation -/
 
 theorem bit_not_testBit (x : BitVec w) (i : Fin w) :
@@ -235,4 +250,80 @@ theorem sle_eq_carry (x y : BitVec w) :
     x.sle y = !((x.msb == y.msb).xor (carry w y (~~~x) true)) := by
   rw [sle_eq_not_slt, slt_eq_not_carry, beq_comm]
 
+/-! ### mul recurrence for bitblasting -/
+
+/--
+A recurrence that describes multiplication as repeated addition.
+Is useful for bitblasting multiplication.
+-/
+def mulRec (l r : BitVec w) (s : Nat) : BitVec w :=
+  let cur := if r.getLsb s then (l <<< s) else 0
+  match s with
+  | 0 => cur
+  | s + 1 => mulRec l r s + cur
+
+theorem mulRec_zero_eq (l r : BitVec w) :
+    mulRec l r 0 = if r.getLsb 0 then l else 0 := by
+  simp [mulRec]
+
+theorem mulRec_succ_eq (l r : BitVec w) (s : Nat) :
+    mulRec l r (s + 1) = mulRec l r s + if r.getLsb (s + 1) then (l <<< (s + 1)) else 0 := rfl
+
+/--
+Recurrence lemma: truncating to `i+1` bits and then zero extending to `w`
+equals truncating upto `i` bits `[0..i-1]`, and then adding the `i`th bit of `x`.
+-/
+theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow (x : BitVec w) (i : Nat) :
+    zeroExtend w (x.truncate (i + 1)) =
+      zeroExtend w (x.truncate i) + (x &&& twoPow w i) := by
+  rw [add_eq_or_of_and_eq_zero]
+  · ext k
+    simp only [getLsb_zeroExtend, Fin.is_lt, decide_True, Bool.true_and, getLsb_or, getLsb_and]
+    by_cases hik : i = k
+    · subst hik
+      simp
+    · simp only [getLsb_twoPow, hik, decide_False, Bool.and_false, Bool.or_false]
+      by_cases hik' : k < (i + 1)
+      · have hik'' : k < i := by omega
+        simp [hik', hik'']
+      · have hik'' : ¬ (k < i) := by omega
+        simp [hik', hik'']
+  · ext k
+    simp
+    omega
+
+/--
+Recurrence lemma: multiplying `l` with the first `s` bits of `r` is the
+same as truncating `r` to `s` bits, then zero extending to the original length,
+and performing the multplication. -/
+theorem mulRec_eq_mul_signExtend_truncate (l r : BitVec w) (s : Nat) :
+    mulRec l r s = l * ((r.truncate (s + 1)).zeroExtend w) := by
+  induction s
+  case zero =>
+    simp only [mulRec_zero_eq, ofNat_eq_ofNat, Nat.reduceAdd]
+    by_cases r.getLsb 0
+    case pos hr =>
+      simp only [hr, ↓reduceIte, truncate, zeroExtend_one_eq_ofBool_getLsb_zero,
+        hr, ofBool_true, ofNat_eq_ofNat]
+      rw [zeroExtend_ofNat_one_eq_ofNat_one_of_lt (by omega)]
+      simp
+    case neg hr =>
+      simp [hr, zeroExtend_one_eq_ofBool_getLsb_zero]
+  case succ s' hs =>
+    rw [mulRec_succ_eq, hs]
+    have heq :
+      (if r.getLsb (s' + 1) = true then l <<< (s' + 1) else 0) =
+        (l * (r &&& (BitVec.twoPow w (s' + 1)))) := by
+      simp only [ofNat_eq_ofNat, and_twoPow_eq]
+      by_cases hr : r.getLsb (s' + 1) <;> simp [hr]
+    rw [heq, ← BitVec.mul_add, ← zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow]
+
+theorem getLsb_mul (x y : BitVec w) (i : Nat) :
+    (x * y).getLsb i = (mulRec x y w).getLsb i := by
+  simp only [mulRec_eq_mul_signExtend_truncate]
+  rw [truncate, ← truncate_eq_zeroExtend, ← truncate_eq_zeroExtend,
+    truncate_truncate_of_le]
+  · simp
+  · omega
+
 end BitVec

src/Init/Data/BitVec/Lemmas.lean

@@ -110,8 +110,8 @@ theorem eq_of_getMsb_eq {x y : BitVec w}
 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]
+theorem getLsb_zero_length (x : BitVec 0) : x.getLsb i = false := by simp
+theorem getMsb_zero_length (x : BitVec 0) : x.getMsb i = false := by simp
 @[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
@@ -163,6 +163,13 @@ theorem toNat_zero (n : Nat) : (0#n).toNat = 0 := by trivial
 private theorem lt_two_pow_of_le {x m n : Nat} (lt : x < 2 ^ m) (le : m ≤ n) : x < 2 ^ n :=
   Nat.lt_of_lt_of_le lt (Nat.pow_le_pow_of_le_right (by trivial : 0 < 2) le)
 
+@[simp]
+theorem getLsb_ofBool (b : Bool) (i : Nat) : (BitVec.ofBool b).getLsb i = ((i = 0) && b) := by
+  rcases b with rfl | rfl
+  · simp [ofBool]
+  · simp only [ofBool, ofNat_eq_ofNat, cond_true, getLsb_ofNat, Bool.and_true]
+    by_cases hi : i = 0 <;> simp [hi] <;> omega
+
 /-! ### msb -/
 
 @[simp] theorem msb_zero : (0#w).msb = false := by simp [BitVec.msb, getMsb]
@@ -286,6 +293,9 @@ theorem toInt_ofNat {n : Nat} (x : Nat) :
 
 /-! ### zeroExtend and truncate -/
 
+theorem truncate_eq_zeroExtend {v : Nat} {x : BitVec w} :
+  truncate v x = zeroExtend v x := rfl
+
 @[simp, bv_toNat] theorem toNat_zeroExtend' {m n : Nat} (p : m ≤ n) (x : BitVec m) :
     (zeroExtend' p x).toNat = x.toNat := by
   unfold zeroExtend'
@@ -319,7 +329,7 @@ theorem zeroExtend'_eq {x : BitVec w} (h : w ≤ v) : x.zeroExtend' h = x.zeroEx
   apply eq_of_toNat_eq
   simp [toNat_zeroExtend]
 
-@[simp] theorem truncate_eq (x : BitVec n) : truncate n x = x := zeroExtend_eq x
+theorem truncate_eq (x : BitVec n) : truncate n x = x := zeroExtend_eq x
 
 @[simp] theorem ofNat_toNat (m : Nat) (x : BitVec n) : BitVec.ofNat m x.toNat = truncate m x := by
   apply eq_of_toNat_eq
@@ -373,7 +383,7 @@ theorem nat_eq_toNat (x : BitVec w) (y : Nat)
   all_goals (first | apply getLsb_ge | apply Eq.symm; apply getLsb_ge)
     <;> omega
 
-@[simp] theorem getLsb_truncate (m : Nat) (x : BitVec n) (i : Nat) :
+theorem getLsb_truncate (m : Nat) (x : BitVec n) (i : Nat) :
     getLsb (truncate m x) i = (decide (i < m) && getLsb x i) :=
   getLsb_zeroExtend m x i
 
@@ -392,6 +402,12 @@ theorem msb_truncate (x : BitVec w) : (x.truncate (k + 1)).msb = x.getLsb k := b
     (x.truncate l).truncate k = x.truncate k :=
   zeroExtend_zeroExtend_of_le x h
 
+/--Truncating by the bitwidth has no effect. -/
+@[simp]
+theorem truncate_eq_self {x : BitVec w} : x.truncate w = x := by
+  ext i
+  simp [getLsb_zeroExtend]
+
 @[simp] theorem truncate_cast {h : w = v} : (cast h x).truncate k = x.truncate k := by
   apply eq_of_getLsb_eq
   simp
@@ -404,6 +420,22 @@ theorem msb_zeroExtend (x : BitVec w) : (x.zeroExtend v).msb = (decide (0 < v) &
 theorem msb_zeroExtend' (x : BitVec w) (h : w ≤ v) : (x.zeroExtend' h).msb = (decide (0 < v) && x.getLsb (v - 1)) := by
   rw [zeroExtend'_eq, msb_zeroExtend]
 
+/-- zero extending a bitvector to width 1 equals the boolean of the lsb. -/
+theorem zeroExtend_one_eq_ofBool_getLsb_zero (x : BitVec w) :
+    x.zeroExtend 1 = BitVec.ofBool (x.getLsb 0) := by
+  ext i
+  simp [getLsb_zeroExtend, Fin.fin_one_eq_zero i]
+
+/-- Zero extending `1#v` to `1#w` equals `1#w` when `v > 0`. -/
+theorem zeroExtend_ofNat_one_eq_ofNat_one_of_lt {v w : Nat} (hv : 0 < v) :
+    (BitVec.ofNat v 1).zeroExtend w = BitVec.ofNat w 1 := by
+  ext ⟨i, hilt⟩
+  simp only [getLsb_zeroExtend, hilt, decide_True, getLsb_ofNat, Bool.true_and,
+    Bool.and_iff_right_iff_imp, decide_eq_true_eq]
+  intros hi₁
+  have hv := Nat.testBit_one_eq_true_iff_self_eq_zero.mp hi₁
+  omega
+
 /-! ## extractLsb -/
 
 @[simp]
@@ -576,7 +608,7 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   ext
   simp_all [lt_of_getLsb]
 
-@[simp] theorem xor_cast {x y : BitVec w} (h : w = w') : cast h x &&& cast h y = cast h (x &&& y) := by
+@[simp] theorem xor_cast {x y : BitVec w} (h : w = w') : cast h x ^^^ cast h y = cast h (x ^^^ y) := by
   ext
   simp_all [lt_of_getLsb]
 
@@ -589,6 +621,11 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
 @[simp] theorem toFin_shiftLeft {n : Nat} (x : BitVec w) :
     BitVec.toFin (x <<< n) = Fin.ofNat' (x.toNat <<< n) (Nat.two_pow_pos w) := rfl
 
+@[simp]
+theorem shiftLeft_zero_eq (x : BitVec w) : x <<< 0 = x := by
+  apply eq_of_toNat_eq
+  simp
+
 @[simp] theorem getLsb_shiftLeft (x : BitVec m) (n) :
     getLsb (x <<< n) i = (decide (i < m) && !decide (i < n) && getLsb x (i - n)) := by
   rw [← testBit_toNat, getLsb]
@@ -1043,8 +1080,16 @@ theorem ofInt_add {n} (x y : Int) : BitVec.ofInt n (x + y) =
 
 theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toNat) := by rfl
 
-@[simp, bv_toNat] theorem toNat_sub {n} (x y : BitVec n) :
-  (x - y).toNat = (((2^n - y.toNat) + x.toNat) % 2^n) := rfl
+@[simp] theorem toNat_sub {n} (x y : BitVec n) :
+    (x - y).toNat = (((2^n - y.toNat) + x.toNat) % 2^n) := rfl
+
+-- We prefer this lemma to `toNat_sub` for the `bv_toNat` simp set.
+-- For reasons we don't yet understand, unfolding via `toNat_sub` sometimes
+-- results in `omega` generating proof terms that are very slow in the kernel.
+@[bv_toNat] theorem toNat_sub' {n} (x y : BitVec n) :
+    (x - y).toNat = ((x.toNat + (2^n - y.toNat)) % 2^n) := by
+  rw [toNat_sub, Nat.add_comm]
+
 @[simp] theorem toFin_sub (x y : BitVec n) : (x - y).toFin = toFin x - toFin y := rfl
 
 @[simp] theorem ofFin_sub (x : Fin (2^n)) (y : BitVec n) : .ofFin x - y = .ofFin (x - y.toFin) :=
@@ -1136,6 +1181,18 @@ instance : Std.Associative (fun (x y : BitVec w) => x * y) := ⟨BitVec.mul_asso
 instance : Std.LawfulCommIdentity (fun (x y : BitVec w) => x * y) (1#w) where
   right_id := BitVec.mul_one
 
+@[simp]
+theorem BitVec.mul_zero {x : BitVec w} : x * 0#w = 0#w := by
+  apply eq_of_toNat_eq
+  simp [toNat_mul]
+
+theorem BitVec.mul_add {x y z : BitVec w} :
+    x * (y + z) = x * y + x * z := by
+  apply eq_of_toNat_eq
+  simp only [toNat_mul, toNat_add, Nat.add_mod_mod, Nat.mod_add_mod]
+  rw [Nat.mul_mod, Nat.mod_mod (y.toNat + z.toNat),
+    ← Nat.mul_mod, Nat.mul_add]
+
 @[simp, bv_toNat] theorem toInt_mul (x y : BitVec w) :
   (x * y).toInt = (x.toInt * y.toInt).bmod (2^w) := by
   simp [toInt_eq_toNat_bmod]
@@ -1414,4 +1471,37 @@ theorem mul_twoPow_eq_shiftLeft (x : BitVec w) (i : Nat) :
       apply Nat.pow_dvd_pow 2 (by omega)
     simp [Nat.mul_mod, hpow]
 
+/- ### zeroExtend, truncate, and bitwise operations -/
+
+/--
+When the `(i+1)`th bit of `x` is false,
+keeping the lower `(i + 1)` bits of `x` equals keeping the lower `i` bits.
+-/
+theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsb_false
+  {x : BitVec w} {i : Nat} (hx : x.getLsb i = false) :
+    zeroExtend w (x.truncate (i + 1)) =
+      zeroExtend w (x.truncate i) := by
+  ext k
+  simp only [getLsb_zeroExtend, Fin.is_lt, decide_True, Bool.true_and, getLsb_or, getLsb_and]
+  by_cases hik : i = k
+  · subst hik
+    simp [hx]
+  · by_cases hik' : k < i + 1 <;> simp [hik'] <;> omega
+
+/--
+When the `(i+1)`th bit of `x` is true,
+keeping the lower `(i + 1)` bits of `x` equalsk eeping the lower `i` bits
+and then performing bitwise-or with `twoPow i = (1 << i)`,
+-/
+theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsb_true
+    {x : BitVec w} {i : Nat} (hx : x.getLsb i = true) :
+    zeroExtend w (x.truncate (i + 1)) =
+      zeroExtend w (x.truncate i) ||| (twoPow w i) := by
+  ext k
+  simp only [getLsb_zeroExtend, Fin.is_lt, decide_True, Bool.true_and, getLsb_or, getLsb_and]
+  by_cases hik : i = k
+  · subst hik
+    simp [hx]
+  · by_cases hik' : k < i + 1 <;> simp [hik, hik'] <;> omega
+
 end BitVec

src/Init/Data/Bool.lean

@@ -52,8 +52,8 @@ theorem eq_iff_iff {a b : Bool} : a = b ↔ (a ↔ b) := by cases b <;> simp
 
 @[simp] theorem decide_eq_true  {b : Bool} [Decidable (b = true)]  : decide (b = true)  =  b := by cases b <;> simp
 @[simp] theorem decide_eq_false {b : Bool} [Decidable (b = false)] : decide (b = false) = !b := by cases b <;> simp
-@[simp] theorem decide_true_eq  {b : Bool} [Decidable (true = b)]  : decide (true  = b) =  b := by cases b <;> simp
-@[simp] theorem decide_false_eq {b : Bool} [Decidable (false = b)] : decide (false = b) = !b := by cases b <;> simp
+theorem decide_true_eq  {b : Bool} [Decidable (true = b)]  : decide (true  = b) =  b := by cases b <;> simp
+theorem decide_false_eq {b : Bool} [Decidable (false = b)] : decide (false = b) = !b := by cases b <;> simp
 
 /-! ### and -/
 
@@ -163,7 +163,7 @@ Consider the term: `¬((b && c) = true)`:
 -/
 @[simp] theorem and_eq_false_imp : ∀ (x y : Bool), (x && y) = false ↔ (x = true → y = false) := by decide
 
-@[simp] theorem or_eq_true_iff : ∀ (x y : Bool), (x || y) = true ↔ x = true ∨ y = true := by decide
+theorem or_eq_true_iff : ∀ (x y : Bool), (x || y) = true ↔ x = true ∨ y = true := by simp
 
 @[simp] theorem or_eq_false_iff : ∀ (x y : Bool), (x || y) = false ↔ x = false ∧ y = false := by decide
 
@@ -187,11 +187,9 @@ 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
@@ -353,7 +351,7 @@ theorem and_or_inj_left_iff :
 /-! ## toNat -/
 
 /-- convert a `Bool` to a `Nat`, `false -> 0`, `true -> 1` -/
-def toNat (b:Bool) : Nat := cond b 1 0
+def toNat (b : Bool) : Nat := cond b 1 0
 
 @[simp] theorem toNat_false : false.toNat = 0 := rfl
 
@@ -496,6 +494,16 @@ protected theorem cond_false {α : Type u} {a b : α} : cond false a b = b := co
 @[simp] theorem cond_true_same  : ∀(c b : Bool), cond c c b = (c || b) := by decide
 @[simp] theorem cond_false_same : ∀(c b : Bool), cond c b c = (c && b) := by decide
 
+theorem cond_pos {b : Bool} {a a' : α} (h : b = true) : (bif b then a else a') = a := by
+  rw [h, cond_true]
+
+theorem cond_neg {b : Bool} {a a' : α} (h : b = false) : (bif b then a else a') = a' := by
+  rw [h, cond_false]
+
+theorem apply_cond (f : α → β) {b : Bool} {a a' : α} :
+    f (bif b then a else a') = bif b then f a else f a' := by
+  cases b <;> simp
+
 /-# decidability -/
 
 protected theorem decide_coe (b : Bool) [Decidable (b = true)] : decide (b = true) = b := decide_eq_true

src/Init/Data/ByteArray/Basic.lean

@@ -52,13 +52,9 @@ def get : (a : @& ByteArray) → (@& Fin a.size) → UInt8
 instance : GetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
-instance : LawfulGetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
-
 instance : GetElem ByteArray USize UInt8 fun xs i => i.val < xs.size where
   getElem xs i h := xs.uget i h
 
-instance : LawfulGetElem ByteArray USize UInt8 fun xs i => i.val < xs.size where
-
 @[extern "lean_byte_array_set"]
 def set! : ByteArray → (@& Nat) → UInt8 → ByteArray
   | ⟨bs⟩, i, b => ⟨bs.set! i b⟩
@@ -96,20 +92,24 @@ protected def append (a : ByteArray) (b : ByteArray) : ByteArray :=
 
 instance : Append ByteArray := ⟨ByteArray.append⟩
 
-partial def toList (bs : ByteArray) : List UInt8 :=
+def toList (bs : ByteArray) : List UInt8 :=
   let rec loop (i : Nat) (r : List UInt8) :=
     if i < bs.size then
       loop (i+1) (bs.get! i :: r)
     else
       r.reverse
+    termination_by bs.size - i
+    decreasing_by decreasing_trivial_pre_omega
   loop 0 []
 
-@[inline] partial def findIdx? (a : ByteArray) (p : UInt8 → Bool) (start := 0) : Option Nat :=
+@[inline] def findIdx? (a : ByteArray) (p : UInt8 → Bool) (start := 0) : Option Nat :=
   let rec @[specialize] loop (i : Nat) :=
     if i < a.size then
       if p (a.get! i) then some i else loop (i+1)
     else
       none
+    termination_by a.size - i
+    decreasing_by decreasing_trivial_pre_omega
   loop start
 
 /--

src/Init/Data/Char/Lemmas.lean

@@ -31,10 +31,10 @@ theorem utf8Size_eq (c : Char) : c.utf8Size = 1 ∨ c.utf8Size = 2 ∨ c.utf8Siz
   rw [Char.ofNat, dif_pos]
   rfl
 
-@[ext] theorem Char.ext : {a b : Char} → a.val = b.val → a = b
+@[ext] theorem ext : {a b : Char} → a.val = b.val → a = b
   | ⟨_,_⟩, ⟨_,_⟩, rfl => rfl
 
-theorem Char.ext_iff {x y : Char} : x = y ↔ x.val = y.val := ⟨congrArg _, Char.ext⟩
+theorem ext_iff {x y : Char} : x = y ↔ x.val = y.val := ⟨congrArg _, Char.ext⟩
 
 end Char
 

src/Init/Data/Fin/Bitwise.lean

@@ -0,0 +1,15 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+prelude
+import Init.Data.Nat.Bitwise
+import Init.Data.Fin.Basic
+
+namespace Fin
+
+@[simp] theorem and_val (a b : Fin n) : (a &&& b).val = a.val &&& b.val :=
+  Nat.mod_eq_of_lt (Nat.lt_of_le_of_lt Nat.and_le_left a.isLt)
+
+end Fin

src/Init/Data/Fin/Lemmas.lean

@@ -786,6 +786,9 @@ theorem coe_sub_iff_le {a b : Fin n} : (↑(a - b) : Nat) = a - b ↔ b ≤ a :=
     rw [Nat.mod_eq_of_lt]
     all_goals omega
 
+theorem sub_val_of_le {a b : Fin n} : b ≤ a → (a - b).val = a.val - b.val :=
+  coe_sub_iff_le.2
+
 theorem coe_sub_iff_lt {a b : Fin n} : (↑(a - b) : Nat) = n + a - b ↔ a < b := by
   rw [sub_def, lt_def]
   dsimp only

src/Init/Data/FloatArray/Basic.lean

@@ -58,13 +58,9 @@ def get? (ds : FloatArray) (i : Nat) : Option Float :=
 instance : GetElem FloatArray Nat Float fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
-instance : LawfulGetElem FloatArray Nat Float fun xs i => i < xs.size where
-
 instance : GetElem FloatArray USize Float fun xs i => i.val < xs.size where
   getElem xs i h := xs.uget i h
 
-instance : LawfulGetElem FloatArray USize Float fun xs i => i.val < xs.size where
-
 @[extern "lean_float_array_uset"]
 def uset : (a : FloatArray) → (i : USize) → Float → i.toNat < a.size → FloatArray
   | ⟨ds⟩, i, v, h => ⟨ds.uset i v h⟩

src/Init/Data/Hashable.lean

@@ -62,3 +62,16 @@ instance (P : Prop) : Hashable P where
 /-- An opaque (low-level) hash operation used to implement hashing for pointers. -/
 @[always_inline, inline] def hash64 (u : UInt64) : UInt64 :=
   mixHash u 11
+
+/-- `LawfulHashable α` says that the `BEq α` and `Hashable α` instances on `α` are compatible, i.e.,
+that `a == b` implies `hash a = hash b`. This is automatic if the `BEq` instance is lawful.
+-/
+class LawfulHashable (α : Type u) [BEq α] [Hashable α] where
+  /-- If `a == b`, then `hash a = hash b`. -/
+  hash_eq (a b : α) : a == b → hash a = hash b
+
+theorem hash_eq [BEq α] [Hashable α] [LawfulHashable α] {a b : α} : a == b → hash a = hash b :=
+  LawfulHashable.hash_eq a b
+
+instance (priority := low) [BEq α] [Hashable α] [LawfulBEq α] : LawfulHashable α where
+  hash_eq _ _ h := eq_of_beq h ▸ rfl

src/Init/Data/List.lean

@@ -8,6 +8,7 @@ import Init.Data.List.Basic
 import Init.Data.List.BasicAux
 import Init.Data.List.Control
 import Init.Data.List.Lemmas
+import Init.Data.List.Attach
 import Init.Data.List.Impl
 import Init.Data.List.TakeDrop
 import Init.Data.List.Notation

src/Init/Data/List/Attach.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2023 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+prelude
+import Init.Data.List.Lemmas
+
+namespace List
+
+/-- `O(n)`. Partial map. If `f : Π a, P a → β` is a partial function defined on
+  `a : α` satisfying `P`, then `pmap f l h` is essentially the same as `map f l`
+  but is defined only when all members of `l` satisfy `P`, using the proof
+  to apply `f`. -/
+@[simp] def pmap {P : α → Prop} (f : ∀ a, P a → β) : ∀ l : List α, (H : ∀ a ∈ l, P a) → List β
+  | [], _ => []
+  | a :: l, H => f a (forall_mem_cons.1 H).1 :: pmap f l (forall_mem_cons.1 H).2
+
+/--
+Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of
+`List {x // P x}` is the same as the input `List α`.
+(Someday, the compiler might do this optimization automatically, but until then...)
+-/
+@[inline] private unsafe def attachWithImpl
+    (l : List α) (P : α → Prop) (_ : ∀ x ∈ l, P x) : List {x // P x} := unsafeCast l
+
+/-- `O(1)`. "Attach" a proof `P x` that holds for all the elements of `l` to produce a new list
+  with the same elements but in the type `{x // P x}`. -/
+@[implemented_by attachWithImpl] def attachWith
+    (l : List α) (P : α → Prop) (H : ∀ x ∈ l, P x) : List {x // P x} := pmap Subtype.mk l H
+
+/-- `O(1)`. "Attach" the proof that the elements of `l` are in `l` to produce a new list
+  with the same elements but in the type `{x // x ∈ l}`. -/
+@[inline] def attach (l : List α) : List {x // x ∈ l} := attachWith l _ fun _ => id
+
+/-- Implementation of `pmap` using the zero-copy version of `attach`. -/
+@[inline] private def pmapImpl {P : α → Prop} (f : ∀ a, P a → β) (l : List α) (H : ∀ a ∈ l, P a) :
+    List β := (l.attachWith _ H).map fun ⟨x, h'⟩ => f x h'
+
+@[csimp] private theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by
+  funext α β p f L h'
+  let rec go : ∀ L' (hL' : ∀ ⦃x⦄, x ∈ L' → p x),
+      pmap f L' hL' = map (fun ⟨x, hx⟩ => f x hx) (pmap Subtype.mk L' hL')
+  | nil, hL' => rfl
+  | cons _ L', hL' => congrArg _ <| go L' fun _ hx => hL' (.tail _ hx)
+  exact go L h'

src/Init/Data/List/Basic.lean

@@ -88,7 +88,7 @@ namespace List
 
 /-! ### concat -/
 
-@[simp] theorem length_concat (as : List α) (a : α) : (concat as a).length = as.length + 1 := by
+@[simp high] theorem length_concat (as : List α) (a : α) : (concat as a).length = as.length + 1 := by
   induction as with
   | nil => rfl
   | cons _ xs ih => simp [concat, ih]
@@ -817,6 +817,8 @@ def dropLast {α} : List α → List α
 @[simp] theorem dropLast_cons₂ :
     (x::y::zs).dropLast = x :: (y::zs).dropLast := rfl
 
+-- Later this can be proved by `simp` via `[List.length_dropLast, List.length_cons, Nat.add_sub_cancel]`,
+-- but we need this while bootstrapping `Array`.
 @[simp] theorem length_dropLast_cons (a : α) (as : List α) : (a :: as).dropLast.length = as.length := by
   match as with
   | []       => rfl

src/Init/Data/List/Lemmas.lean

@@ -126,6 +126,14 @@ theorem length_pos {l : List α} : 0 < length l ↔ l ≠ [] :=
 theorem length_eq_one {l : List α} : length l = 1 ↔ ∃ a, l = [a] :=
   ⟨fun h => match l, h with | [_], _ => ⟨_, rfl⟩, fun ⟨_, h⟩ => by simp [h]⟩
 
+/-! ### `isEmpty` -/
+
+theorem isEmpty_iff {l : List α} : l.isEmpty ↔ l = [] := by
+  cases l <;> simp
+
+theorem isEmpty_iff_length_eq_zero {l : List α} : l.isEmpty ↔ l.length = 0 := by
+  rw [isEmpty_iff, length_eq_zero]
+
 /-! ### L[i] and L[i]? -/
 
 @[simp] theorem get_cons_zero : get (a::l) (0 : Fin (l.length + 1)) = a := rfl
@@ -154,27 +162,12 @@ theorem get?_eq_none : l.get? n = none ↔ length l ≤ n :=
   ⟨fun e => Nat.ge_of_not_lt (fun h' => by cases e ▸ get?_eq_some.2 ⟨h', rfl⟩), get?_len_le⟩
 
 @[simp] theorem get?_eq_getElem? (l : List α) (i : Nat) : l.get? i = l[i]? := by
-  simp only [getElem?]; split
+  simp only [getElem?, decidableGetElem?]; split
   · exact (get?_eq_get ‹_›)
   · exact (get?_eq_none.2 <| Nat.not_lt.1 ‹_›)
 
 @[simp] theorem get_eq_getElem (l : List α) (i : Fin l.length) : l.get i = l[i.1]'i.2 := rfl
 
-@[simp] theorem getElem?_nil {n : Nat} : ([] : List α)[n]? = none := rfl
-
-@[simp] theorem getElem?_cons_zero {l : List α} : (a::l)[0]? = some a := by
-  simp only [← get?_eq_getElem?]
-  rfl
-
-@[simp] theorem getElem?_cons_succ {l : List α} : (a::l)[n+1]? = l[n]? := by
-  simp only [← get?_eq_getElem?]
-  rfl
-
-theorem getElem?_len_le : ∀ {l : List α} {n}, length l ≤ n → l[n]? = none
-  | [], _, _ => rfl
-  | _ :: l, _+1, h => by
-    rw [getElem?_cons_succ, getElem?_len_le (l := l) <| Nat.le_of_succ_le_succ h]
-
 @[simp] theorem getElem?_eq_getElem {l : List α} {n} (h : n < l.length) : l[n]? = some l[n] := by
   simp only [← get?_eq_getElem?, get?_eq_get, h, get_eq_getElem]
 
@@ -186,6 +179,19 @@ theorem getElem?_eq_some {l : List α} : l[n]? = some a ↔ ∃ h : n < l.length
 
 theorem getElem?_eq_none (h : length l ≤ n) : l[n]? = none := getElem?_eq_none_iff.mpr h
 
+@[simp] theorem getElem?_nil {n : Nat} : ([] : List α)[n]? = none := rfl
+
+theorem getElem?_cons_zero {l : List α} : (a::l)[0]? = some a := by simp
+
+@[simp] theorem getElem?_cons_succ {l : List α} : (a::l)[n+1]? = l[n]? := by
+  simp only [← get?_eq_getElem?]
+  rfl
+
+theorem getElem?_len_le : ∀ {l : List α} {n}, length l ≤ n → l[n]? = none
+  | [], _, _ => rfl
+  | _ :: l, _+1, h => by
+    rw [getElem?_cons_succ, getElem?_len_le (l := l) <| Nat.le_of_succ_le_succ h]
+
 @[simp] theorem getElem!_nil [Inhabited α] {n : Nat} : ([] : List α)[n]! = default := rfl
 
 @[simp] theorem getElem!_cons_zero [Inhabited α] {l : List α} : (a::l)[0]! = a := by
@@ -812,9 +818,8 @@ theorem map_eq_foldr (f : α → β) (l : List α) : map f l = foldr (fun a bs =
 @[simp] theorem tail?_map (f : α → β) (l : List α) : tail? (map f l) = (tail? l).map (map f) := by
   cases l <;> rfl
 
-@[simp] theorem tailD_map (f : α → β) (l : List α) (l' : List α) :
-    tailD (map f l) (map f l') = map f (tailD l l') := by
-  cases l <;> rfl
+theorem tailD_map (f : α → β) (l : List α) (l' : List α) :
+    tailD (map f l) (map f l') = map f (tailD l l') := by simp
 
 @[simp] theorem getLast_map (f : α → β) (l : List α) (h) :
     getLast (map f l) h = f (getLast l (by simpa using h)) := by
@@ -1035,6 +1040,10 @@ theorem getElem_append_right' {l₁ l₂ : List α} {n : Nat} (h₁ : l₁.lengt
       l₂[n - l₁.length]'(by rw [length_append] at h₂; exact Nat.sub_lt_left_of_lt_add h₁ h₂) :=
   Option.some.inj <| by rw [← getElem?_eq_getElem, ← getElem?_eq_getElem, getElem?_append_right h₁]
 
+theorem getElem_append_right'' (l₁ : List α) {l₂ : List α} {n : Nat} (hn : n < l₂.length) :
+    l₂[n] = (l₁ ++ l₂)[n + l₁.length]'(by simpa [Nat.add_comm] using Nat.add_lt_add_left hn _) := by
+  rw [getElem_append_right] <;> simp [*, le_add_left]
+
 @[deprecated (since := "2024-06-12")]
 theorem get_append_right_aux {l₁ l₂ : List α} {n : Nat}
   (h₁ : l₁.length ≤ n) (h₂ : n < (l₁ ++ l₂).length) : n - l₁.length < l₂.length := by
@@ -1282,6 +1291,14 @@ theorem map_eq_bind {α β} (f : α → β) (l : List α) : map f l = l.bind fun
   simp only [← map_singleton]
   rw [← bind_singleton' l, map_bind, bind_singleton']
 
+theorem bind_eq_foldl (f : α → List β) (l : List α) :
+    l.bind f = l.foldl (fun acc a => acc ++ f a) [] := by
+  suffices ∀ l', l' ++ l.bind f = l.foldl (fun acc a => acc ++ f a) l' by simpa using this []
+  intro l'
+  induction l generalizing l'
+  · simp
+  · next ih => rw [bind_cons, ← append_assoc, ih, foldl_cons]
+
 /-! ### replicate -/
 
 @[simp] theorem replicate_one : replicate 1 a = [a] := rfl
@@ -1518,8 +1535,7 @@ theorem reverseAux_eq (as bs : List α) : reverseAux as bs = reverse as ++ bs :=
 
 /-! ### elem / contains -/
 
-@[simp] theorem elem_cons_self [BEq α] [LawfulBEq α] {a : α} : (a::as).elem a = true := by
-  simp [elem_cons]
+theorem elem_cons_self [BEq α] [LawfulBEq α] {a : α} : (a::as).elem a = true := by simp
 
 @[simp] theorem contains_cons [BEq α] :
     (a :: as : List α).contains x = (x == a || as.contains x) := by
@@ -1529,6 +1545,10 @@ theorem reverseAux_eq (as bs : List α) : reverseAux as bs = reverse as ++ bs :=
 theorem contains_eq_any_beq [BEq α] (l : List α) (a : α) : l.contains a = l.any (a == ·) := by
   induction l with simp | cons b l => cases b == a <;> simp [*]
 
+theorem contains_iff_exists_mem_beq [BEq α] (l : List α) (a : α) :
+    l.contains a ↔ ∃ a' ∈ l, a == a' := by
+  induction l <;> simp_all
+
 /-! ## Sublists -/
 
 /-! ### take and drop
@@ -1920,15 +1940,14 @@ end replace
 section insert
 variable [BEq α] [LawfulBEq α]
 
-@[simp] theorem insert_nil (a : α) : [].insert a = [a] := by
-  simp [List.insert]
-
 @[simp] theorem insert_of_mem {l : List α} (h : a ∈ l) : l.insert a = l := by
   simp [List.insert, h]
 
 @[simp] theorem insert_of_not_mem {l : List α} (h : a ∉ l) : l.insert a = a :: l := by
   simp [List.insert, h]
 
+theorem insert_nil (a : α) : [].insert a = [a] := by simp
+
 @[simp] theorem mem_insert_iff {l : List α} : a ∈ l.insert b ↔ a = b ∨ a ∈ l := by
   if h : b ∈ l then
     rw [insert_of_mem h]

src/Init/Data/List/TakeDrop.lean

@@ -272,6 +272,15 @@ theorem set_eq_take_append_cons_drop {l : List α} {n : Nat} {a : α} :
   · rw [set_eq_of_length_le]
     omega
 
+theorem exists_of_set {n : Nat} {a' : α} {l : List α} (h : n < l.length) :
+    ∃ l₁ l₂, l = l₁ ++ l[n] :: l₂ ∧ l₁.length = n ∧ l.set n a' = l₁ ++ a' :: l₂ := by
+  refine ⟨l.take n, l.drop (n + 1), ⟨by simp, ⟨length_take_of_le (Nat.le_of_lt h), ?_⟩⟩⟩
+  simp [set_eq_take_append_cons_drop, h]
+
+theorem drop_set_of_lt (a : α) {n m : Nat} (l : List α)
+    (hnm : n < m) : drop m (l.set n a) = l.drop m :=
+  ext_getElem? fun k => by simpa only [getElem?_drop] using getElem?_set_ne (by omega)
+
 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

src/Init/Data/Nat/Basic.lean

@@ -124,13 +124,8 @@ instance : LawfulBEq Nat where
   eq_of_beq h := Nat.eq_of_beq_eq_true h
   rfl := by simp [BEq.beq]
 
-@[simp] theorem beq_eq_true_eq (a b : Nat) : ((a == b) = true) = (a = b) := propext <| Iff.intro eq_of_beq (fun h => by subst h; apply LawfulBEq.rfl)
-@[simp] theorem not_beq_eq_true_eq (a b : Nat) : ((!(a == b)) = true) = ¬(a = b) :=
-  propext <| Iff.intro
-    (fun h₁ h₂ => by subst h₂; rw [LawfulBEq.rfl] at h₁; contradiction)
-    (fun h =>
-      have : ¬ ((a == b) = true) := fun h' => absurd (eq_of_beq h') h
-      by simp [this])
+theorem beq_eq_true_eq (a b : Nat) : ((a == b) = true) = (a = b) := by simp
+theorem not_beq_eq_true_eq (a b : Nat) : ((!(a == b)) = true) = ¬(a = b) := by simp
 
 /-! # Nat.add theorems -/
 
@@ -355,7 +350,7 @@ protected theorem pos_of_ne_zero {n : Nat} : n ≠ 0 → 0 < n := (eq_zero_or_po
 
 theorem lt.base (n : Nat) : n < succ n := Nat.le_refl (succ n)
 
-@[simp] theorem lt_succ_self (n : Nat) : n < succ n := lt.base n
+theorem lt_succ_self (n : Nat) : n < succ n := lt.base n
 
 @[simp] protected theorem lt_add_one (n : Nat) : n < n + 1 := lt.base n
 
@@ -705,8 +700,7 @@ protected theorem one_ne_zero : 1 ≠ (0 : Nat) :=
 protected theorem zero_ne_one : 0 ≠ (1 : Nat) :=
   fun h => Nat.noConfusion h
 
-@[simp] theorem succ_ne_zero (n : Nat) : succ n ≠ 0 :=
-  fun h => Nat.noConfusion h
+theorem succ_ne_zero (n : Nat) : succ n ≠ 0 := by simp
 
 /-! # mul + order -/
 
@@ -814,8 +808,11 @@ theorem sub_one_lt_of_lt {n m : Nat} (h : m < n) : n - 1 < n :=
 
 /-! # pred theorems -/
 
-@[simp] protected theorem pred_zero : pred 0 = 0 := rfl
-@[simp] protected theorem pred_succ (n : Nat) : pred n.succ = n := rfl
+protected theorem pred_zero : pred 0 = 0 := rfl
+protected theorem pred_succ (n : Nat) : pred n.succ = n := rfl
+
+@[simp] protected theorem zero_sub_one : 0 - 1 = 0 := rfl
+@[simp] protected theorem add_one_sub_one (n : Nat) : n + 1 - 1 = n := rfl
 
 theorem succ_pred {a : Nat} (h : a ≠ 0) : a.pred.succ = a := by
   induction a with

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

@@ -86,7 +86,7 @@ noncomputable def div2Induction {motive : Nat → Sort u}
 @[simp] theorem testBit_zero (x : Nat) : testBit x 0 = decide (x % 2 = 1) := by
   cases mod_two_eq_zero_or_one x with | _ p => simp [testBit, p]
 
-@[simp] theorem testBit_succ (x i : Nat) : testBit x (succ i) = testBit (x/2) i := by
+theorem testBit_succ (x i : Nat) : testBit x (succ i) = testBit (x/2) i := by
   unfold testBit
   simp [shiftRight_succ_inside]
 
@@ -504,3 +504,27 @@ theorem mul_add_lt_is_or {b : Nat} (b_lt : b < 2^i) (a : Nat) : 2^i * a + b = 2^
 
 @[simp] theorem testBit_shiftRight (x : Nat) : testBit (x >>> i) j = testBit x (i+j) := by
   simp [testBit, ←shiftRight_add]
+
+/-! ### le -/
+
+theorem le_of_testBit {n m : Nat} (h : ∀ i, n.testBit i = true → m.testBit i = true) : n ≤ m := by
+  induction n using div2Induction generalizing m
+  next n ih =>
+  have : n / 2 ≤ m / 2 := by
+    rcases n with (_|n)
+    · simp
+    · exact ih (Nat.succ_pos _) fun i => by simpa using h (i + 1)
+  rw [← div_add_mod n 2, ← div_add_mod m 2]
+  cases hn : n.testBit 0
+  · have hn2 : n % 2 = 0 := by simp at hn; omega
+    rw [hn2]
+    omega
+  · have hn2 : n % 2 = 1 := by simpa using hn
+    have hm2 : m % 2 = 1 := by simpa using h _ hn
+    omega
+
+theorem and_le_left {n m : Nat} : n &&& m ≤ n :=
+  le_of_testBit (by simpa using fun i x _ => x)
+
+theorem and_le_right {n m : Nat} : n &&& m ≤ m :=
+  le_of_testBit (by simp)

src/Init/Data/Nat/Lemmas.lean

@@ -115,8 +115,6 @@ protected theorem add_sub_cancel_right (n m : Nat) : (n + m) - m = n := Nat.add_
 
 theorem succ_sub_one (n) : succ n - 1 = n := rfl
 
-protected theorem add_one_sub_one (n : Nat) : (n + 1) - 1 = n := rfl
-
 protected theorem one_add_sub_one (n : Nat) : (1 + n) - 1 = n := Nat.add_sub_cancel_left 1 _
 
 protected theorem sub_sub_self {n m : Nat} (h : m ≤ n) : n - (n - m) = m :=

src/Init/Data/Option/Basic.lean

@@ -26,7 +26,7 @@ def toMonad [Monad m] [Alternative m] : Option α → m α := getM
   | some _ => true
   | none   => false
 
-@[deprecated isSome, inline] def toBool : Option α → Bool := isSome
+@[deprecated isSome (since := "2024-04-17"), inline] def toBool : Option α → Bool := isSome
 
 /-- Returns `true` on `none` and `false` on `some x`. -/
 @[inline] def isNone : Option α → Bool
@@ -80,7 +80,9 @@ theorem map_id : (Option.map id : Option α → Option α) = id :=
   | none   => false
 
 /--
-Implementation of `OrElse`'s `<|>` syntax for `Option`.
+Implementation of `OrElse`'s `<|>` syntax for `Option`. If the first argument is `some a`, returns
+`some a`, otherwise evaluates and returns the second argument. See also `or` for a version that is
+strict in the second argument.
 -/
 @[always_inline, macro_inline] protected def orElse : Option α → (Unit → Option α) → Option α
   | some a, _ => some a
@@ -89,6 +91,12 @@ Implementation of `OrElse`'s `<|>` syntax for `Option`.
 instance : OrElse (Option α) where
   orElse := Option.orElse
 
+/-- If the first argument is `some a`, returns `some a`, otherwise returns the second argument.
+This is similar to `<|>`/`orElse`, but it is strict in the second argument. -/
+@[always_inline, macro_inline] def or : Option α → Option α → Option α
+  | some a, _ => some a
+  | none,   b => b
+
 @[inline] protected def lt (r : α → α → Prop) : Option α → Option α → Prop
   | none, some _     => True
   | some x,   some y => r x y

src/Init/Data/Option/Lemmas.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 prelude
+import Init.Data.Option.BasicAux
 import Init.Data.Option.Instances
 import Init.Classical
 import Init.Ext
@@ -41,6 +42,21 @@ theorem getD_of_ne_none {x : Option α} (hx : x ≠ none) (y : α) : some (x.get
 theorem getD_eq_iff {o : Option α} {a b} : o.getD a = b ↔ (o = some b ∨ o = none ∧ a = b) := by
   cases o <;> simp
 
+@[simp] theorem get!_none [Inhabited α] : (none : Option α).get! = default := rfl
+
+@[simp] theorem get!_some [Inhabited α] {a : α} : (some a).get! = a := rfl
+
+theorem get_eq_get! [Inhabited α] : (o : Option α) → {h : o.isSome} → o.get h = o.get!
+  | some _, _ => rfl
+
+theorem get_eq_getD {fallback : α} : (o : Option α) → {h : o.isSome} → o.get h = o.getD fallback
+  | some _, _ => rfl
+
+theorem some_get! [Inhabited α] : (o : Option α) → o.isSome → some (o.get!) = o
+  | some _, _ => rfl
+
+theorem get!_eq_getD_default [Inhabited α] (o : Option α) : o.get! = o.getD default := rfl
+
 theorem mem_unique {o : Option α} {a b : α} (ha : a ∈ o) (hb : b ∈ o) : a = b :=
   some.inj <| ha ▸ hb
 
@@ -145,6 +161,12 @@ theorem map_eq_some : f <$> x = some b ↔ ∃ a, x = some a ∧ f a = b := map_
 @[simp] theorem map_eq_none' : x.map f = none ↔ x = none := by
   cases x <;> simp only [map_none', map_some', eq_self_iff_true]
 
+theorem isSome_map {x : Option α} : (f <$> x).isSome = x.isSome := by
+  cases x <;> simp
+
+@[simp] theorem isSome_map' {x : Option α} : (x.map f).isSome = x.isSome := by
+  cases x <;> simp
+
 theorem map_eq_none : f <$> x = none ↔ x = none := map_eq_none'
 
 theorem map_eq_bind {x : Option α} : x.map f = x.bind (some ∘ f) := by
@@ -236,3 +258,46 @@ end
 @[simp] theorem toList_some (a : α) : (a : Option α).toList = [a] := rfl
 
 @[simp] theorem toList_none (α : Type _) : (none : Option α).toList = [] := rfl
+
+@[simp] theorem or_some : (some a).or o = some a := rfl
+@[simp] theorem none_or : none.or o = o := rfl
+
+theorem or_eq_bif : or o o' = bif o.isSome then o else o' := by
+  cases o <;> rfl
+
+@[simp] theorem isSome_or : (or o o').isSome = (o.isSome || o'.isSome) := by
+  cases o <;> rfl
+
+@[simp] theorem isNone_or : (or o o').isNone = (o.isNone && o'.isNone) := by
+  cases o <;> rfl
+
+@[simp] theorem or_eq_none : or o o' = none ↔ o = none ∧ o' = none := by
+  cases o <;> simp
+
+theorem or_eq_some : or o o' = some a ↔ o = some a ∨ (o = none ∧ o' = some a) := by
+  cases o <;> simp
+
+theorem or_assoc : or (or o₁ o₂) o₃ = or o₁ (or o₂ o₃) := by
+  cases o₁ <;> cases o₂ <;> rfl
+instance : Std.Associative (or (α := α)) := ⟨@or_assoc _⟩
+
+@[simp]
+theorem or_none : or o none = o := by
+  cases o <;> rfl
+instance : Std.LawfulIdentity (or (α := α)) none where
+  left_id := @none_or _
+  right_id := @or_none _
+
+@[simp]
+theorem or_self : or o o = o := by
+  cases o <;> rfl
+instance : Std.IdempotentOp (or (α := α)) := ⟨@or_self _⟩
+
+theorem or_eq_orElse : or o o' = o.orElse (fun _ => o') := by
+  cases o <;> rfl
+
+theorem map_or : f <$> or o o' = (f <$> o).or (f <$> o') := by
+  cases o <;> rfl
+
+theorem map_or' : (or o o').map f = (o.map f).or (o'.map f) := by
+  cases o <;> rfl

src/Init/Data/UInt.lean

@@ -7,3 +7,4 @@ prelude
 import Init.Data.UInt.Basic
 import Init.Data.UInt.Log2
 import Init.Data.UInt.Lemmas
+import Init.Data.UInt.Bitwise

src/Init/Data/UInt/Bitwise.lean

@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+prelude
+import Init.Data.UInt.Basic
+import Init.Data.Fin.Bitwise
+
+set_option hygiene false in
+macro "declare_bitwise_uint_theorems" typeName:ident : command =>
+`(
+namespace $typeName
+
+@[simp] protected theorem and_toNat (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := Fin.and_val ..
+
+end $typeName
+)
+
+declare_bitwise_uint_theorems UInt8
+declare_bitwise_uint_theorems UInt16
+declare_bitwise_uint_theorems UInt32
+declare_bitwise_uint_theorems UInt64
+declare_bitwise_uint_theorems USize

src/Init/Data/UInt/Lemmas.lean

@@ -26,6 +26,8 @@ theorem add_def (a b : $typeName) : a + b = ⟨a.val + b.val⟩ := rfl
   | ⟨_, _⟩ => rfl
 theorem val_eq_of_lt {a : Nat} : a < size → ((ofNat a).val : Nat) = a :=
   Nat.mod_eq_of_lt
+theorem toNat_ofNat_of_lt {n : Nat} (h : n < size) : (ofNat n).toNat = n := by
+  rw [toNat, val_eq_of_lt h]
 
 theorem le_def {a b : $typeName} : a ≤ b ↔ a.1 ≤ b.1 := .rfl
 theorem lt_def {a b : $typeName} : a < b ↔ a.1 < b.1 := .rfl
@@ -48,6 +50,7 @@ protected theorem ne_of_lt {a b : $typeName} (h : a < b) : a ≠ b := ne_of_val_
 @[simp] protected theorem zero_toNat : (0 : $typeName).toNat = 0 := Nat.zero_mod _
 @[simp] protected theorem mod_toNat (a b : $typeName) : (a % b).toNat = a.toNat % b.toNat := Fin.mod_val ..
 @[simp] protected theorem div_toNat (a b : $typeName) : (a / b).toNat = a.toNat / b.toNat := Fin.div_val ..
+@[simp] protected theorem sub_toNat_of_le (a b : $typeName) : b ≤ a → (a - b).toNat = a.toNat - b.toNat := Fin.sub_val_of_le
 @[simp] protected theorem modn_toNat (a : $typeName) (b : Nat) : (a.modn b).toNat = a.toNat % b := Fin.modn_val ..
 protected theorem modn_lt {m : Nat} : ∀ (u : $typeName), m > 0 → toNat (u % m) < m
   | ⟨u⟩, h => Fin.modn_lt u h
@@ -55,6 +58,8 @@ open $typeName (modn_lt) in
 protected theorem mod_lt (a b : $typeName) (h : 0 < b) : a % b < b := modn_lt _ (by simp [lt_def] at h; exact h)
 protected theorem toNat.inj : ∀ {a b : $typeName}, a.toNat = b.toNat → a = b
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
+protected theorem toNat_lt_size (a : $typeName) : a.toNat < size := a.1.2
+@[simp] protected theorem ofNat_one : ofNat 1 = 1 := rfl
 
 end $typeName
 )

src/Init/GetElem.lean

@@ -7,22 +7,57 @@ prelude
 import Init.Util
 
 @[never_extract]
-private def outOfBounds [Inhabited α] : α :=
+def outOfBounds [Inhabited α] : α :=
   panic! "index out of bounds"
 
-/--
-The class `GetElem coll idx elem valid` implements the `xs[i]` notation.
-Given `xs[i]` with `xs : coll` and `i : idx`, Lean looks for an instance of
-`GetElem coll idx elem valid` and uses this to infer the type of return
-value `elem` and side conditions `valid` required to ensure `xs[i]` yields
-a valid value of type `elem`.
+theorem outOfBounds_eq_default [Inhabited α] : (outOfBounds : α) = default := rfl
+
+/--
+The classes `GetElem` and `GetElem?` implement lookup notation,
+specifically `xs[i]`, `xs[i]?`, `xs[i]!`, and `xs[i]'p`.
+
+Both classes are indexed by types `coll`, `idx`, and `elem` which are
+the collection, the index, and the element types.
+A single collection may support lookups with multiple index
+types. The relation `valid` determines when the index is guaranteed to be
+valid; lookups of valid indices are guaranteed not to fail.
+
+For example, an instance for arrays looks like
+`GetElem (Array α) Nat α (fun xs i => i < xs.size)`. In other words, given an
+array `xs` and a natural number `i`, `xs[i]` will return an `α` when `valid xs i`
+holds, which is true when `i` is less than the size of the array. `Array`
+additionally supports indexing with `USize` instead of `Nat`.
+In either case, because the bounds are checked at compile time,
+no runtime check is required.
+
+Given `xs[i]` with `xs : coll` and `i : idx`, Lean looks for an instance of
+`GetElem coll idx elem valid` and uses this to infer the type of the return
+value `elem` and side condition `valid` required to ensure `xs[i]` yields
+a valid value of type `elem`. The tactic `get_elem_tactic` is
+invoked to prove validity automatically. The `xs[i]'p` notation uses the
+proof `p` to satisfy the validity condition.
+If the proof `p` is long, it is often easier to place the
+proof in the context using `have`, because `get_elem_tactic` tries
+`assumption`.
 
-For example, the instance for arrays looks like
-`GetElem (Array α) Nat α (fun xs i => i < xs.size)`.
 
 The proof side-condition `valid xs i` is automatically dispatched by the
-`get_elem_tactic` tactic, which can be extended by adding more clauses to
-`get_elem_tactic_trivial`.
+`get_elem_tactic` tactic; this tactic can be extended by adding more clauses to
+`get_elem_tactic_trivial` using `macro_rules`.
+
+`xs[i]?` and `xs[i]!` do not impose a proof obligation; the former returns
+an `Option elem`, with `none` signalling that the value isn't present, and
+the latter returns `elem` but panics if the value isn't there, returning
+`default : elem` based on the `Inhabited elem` instance.
+These are provided by the `GetElem?` class, for which there is a default instance
+generated from a `GetElem` class as long as `valid xs i` is always decidable.
+
+Important instances include:
+  * `arr[i] : α` where `arr : Array α` and `i : Nat` or `i : USize`: does array
+    indexing with no runtime bounds check and a proof side goal `i < arr.size`.
+  * `l[i] : α` where `l : List α` and `i : Nat`: index into a list, with proof
+    side goal `i < l.length`.
+
 -/
 class GetElem (coll : Type u) (idx : Type v) (elem : outParam (Type w))
               (valid : outParam (coll → idx → Prop)) where
@@ -30,33 +65,10 @@ class GetElem (coll : Type u) (idx : Type v) (elem : outParam (Type w))
   The syntax `arr[i]` gets the `i`'th element of the collection `arr`. If there
   are proof side conditions to the application, they will be automatically
   inferred by the `get_elem_tactic` tactic.
-
-  The actual behavior of this class is type-dependent, but here are some
-  important implementations:
-  * `arr[i] : α` where `arr : Array α` and `i : Nat` or `i : USize`: does array
-    indexing with no bounds check and a proof side goal `i < arr.size`.
-  * `l[i] : α` where `l : List α` and `i : Nat`: index into a list, with proof
-    side goal `i < l.length`.
-  * `stx[i] : Syntax` where `stx : Syntax` and `i : Nat`: get a syntax argument,
-    no side goal (returns `.missing` out of range)
-
-  There are other variations on this syntax:
-  * `arr[i]!` is syntax for `getElem! arr i` which should panic and return
-    `default : α` if the index is not valid.
-  * `arr[i]?` is syntax for `getElem?` which should return `none` if the index
-    is not valid.
-  * `arr[i]'h` is syntax for `getElem arr i h` with `h` an explicit proof the
-    index is valid.
   -/
   getElem (xs : coll) (i : idx) (h : valid xs i) : elem
 
-  getElem? (xs : coll) (i : idx) [Decidable (valid xs i)] : Option elem :=
-    if h : _ then some (getElem xs i h) else none
-
-  getElem! [Inhabited elem] (xs : coll) (i : idx) [Decidable (valid xs i)] : elem :=
-    match getElem? xs i with | some e => e | none => outOfBounds
-
-export GetElem (getElem getElem! getElem?)
+export GetElem (getElem)
 
 @[inherit_doc getElem]
 syntax:max term noWs "[" withoutPosition(term) "]" : term
@@ -66,6 +78,30 @@ macro_rules | `($x[$i]) => `(getElem $x $i (by get_elem_tactic))
 syntax term noWs "[" withoutPosition(term) "]'" term:max : term
 macro_rules | `($x[$i]'$h) => `(getElem $x $i $h)
 
+/-- Helper function for implementation of `GetElem?.getElem?`. -/
+abbrev decidableGetElem? [GetElem coll idx elem valid] (xs : coll) (i : idx) [Decidable (valid xs i)] :
+    Option elem :=
+  if h : valid xs i then some xs[i] else none
+
+@[inherit_doc GetElem]
+class GetElem? (coll : Type u) (idx : Type v) (elem : outParam (Type w))
+    (valid : outParam (coll → idx → Prop)) extends GetElem coll idx elem valid where
+  /--
+  The syntax `arr[i]?` gets the `i`'th element of the collection `arr`,
+  if it is present (and wraps it in `some`), and otherwise returns `none`.
+  -/
+  getElem? : coll → idx → Option elem
+
+  /--
+  The syntax `arr[i]!` gets the `i`'th element of the collection `arr`,
+  if it is present, and otherwise panics at runtime and returns the `default` term
+  from `Inhabited elem`.
+  -/
+  getElem! [Inhabited elem] (xs : coll) (i : idx) : elem :=
+    match getElem? xs i with | some e => e | none => outOfBounds
+
+export GetElem? (getElem? getElem!)
+
 /--
 The syntax `arr[i]?` gets the `i`'th element of the collection `arr` or
 returns `none` if `i` is out of bounds.
@@ -78,32 +114,51 @@ panics `i` is out of bounds.
 -/
 macro:max x:term noWs "[" i:term "]" noWs "!" : term => `(getElem! $x $i)
 
+instance (priority := low) [GetElem coll idx elem valid] [∀ xs i, Decidable (valid xs i)] :
+    GetElem? coll idx elem valid where
+  getElem? xs i := decidableGetElem? xs i
+
+theorem getElem_congr_coll [GetElem coll idx elem valid] {c d : coll} {i : idx} {h : valid c i}
+    (h' : c = d) : c[i] = d[i]'(h' ▸ h) := by
+  cases h'; rfl
+
+theorem getElem_congr [GetElem coll idx elem valid] {c : coll} {i j : idx} {h : valid c i}
+    (h' : i = j) : c[i] = c[j]'(h' ▸ h) := by
+  cases h'; rfl
+
 class LawfulGetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w))
-   (dom : outParam (cont → idx → Prop)) [ge : GetElem cont idx elem dom] : Prop where
+   (dom : outParam (cont → idx → Prop)) [ge : GetElem? cont idx elem dom] : Prop where
 
   getElem?_def (c : cont) (i : idx) [Decidable (dom c i)] :
-    c[i]? = if h : dom c i then some (c[i]'h) else none := by intros; eq_refl
-  getElem!_def [Inhabited elem] (c : cont) (i : idx) [Decidable (dom c i)] :
-    c[i]! = match c[i]? with | some e => e | none => default := by intros; eq_refl
+      c[i]? = if h : dom c i then some (c[i]'h) else none := by
+    intros
+    try simp only [getElem?] <;> congr
+  getElem!_def [Inhabited elem] (c : cont) (i : idx) :
+      c[i]! = match c[i]? with | some e => e | none => default := by
+    intros
+    simp only [getElem!, getElem?, outOfBounds_eq_default]
 
 export LawfulGetElem (getElem?_def getElem!_def)
 
-theorem getElem?_pos [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
+instance (priority := low) [GetElem coll idx elem valid] [∀ xs i, Decidable (valid xs i)] :
+    LawfulGetElem coll idx elem valid where
+
+theorem getElem?_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] : c[i]? = some (c[i]'h) := by
   rw [getElem?_def]
   exact dif_pos h
 
-theorem getElem?_neg [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
+theorem getElem?_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]? = none := by
   rw [getElem?_def]
   exact dif_neg h
 
-theorem getElem!_pos [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
+theorem getElem!_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     [Inhabited elem] (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] :
     c[i]! = c[i]'h := by
   simp only [getElem!_def, getElem?_def, h]
 
-theorem getElem!_neg [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
+theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     [Inhabited elem] (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]! = default := by
   simp only [getElem!_def, getElem?_def, h]
 
@@ -111,22 +166,23 @@ namespace Fin
 
 instance instGetElemFinVal [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun xs i => dom xs i where
   getElem xs i h := getElem xs i.1 h
+
+instance instGetElem?FinVal [GetElem? cont Nat elem dom] : GetElem? cont (Fin n) elem fun xs i => dom xs i where
   getElem? xs i := getElem? xs i.val
   getElem! xs i := getElem! xs i.val
 
-instance [GetElem cont Nat elem dom] [h : LawfulGetElem cont Nat elem dom] :
+instance [GetElem? cont Nat elem dom] [h : LawfulGetElem cont Nat elem dom] :
       LawfulGetElem cont (Fin n) elem fun xs i => dom xs i where
-
   getElem?_def _c _i _d := h.getElem?_def ..
-  getElem!_def _c _i _d := h.getElem!_def ..
+  getElem!_def _c _i := h.getElem!_def ..
 
-@[simp] theorem getElem_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) :
+@[simp] theorem getElem_fin [GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) :
     a[i] = a[i.1] := rfl
 
-@[simp] theorem getElem?_fin [h : GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n)
+@[simp] theorem getElem?_fin [h : GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n)
     [Decidable (Dom a i)] : a[i]? = a[i.1]? := by rfl
 
-@[simp] theorem getElem!_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n)
+@[simp] theorem getElem!_fin [GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n)
     [Decidable (Dom a i)] [Inhabited Elem] : a[i]! = a[i.1]! := rfl
 
 macro_rules
@@ -139,17 +195,15 @@ namespace List
 instance : GetElem (List α) Nat α fun as i => i < as.length where
   getElem as i h := as.get ⟨i, h⟩
 
-instance : LawfulGetElem (List α) Nat α fun as i => i < as.length where
-
 @[simp] theorem getElem_cons_zero (a : α) (as : List α) (h : 0 < (a :: as).length) : getElem (a :: as) 0 h = a := by
   rfl
 
-@[deprecated (since := "2024-6-12")] abbrev cons_getElem_zero := @getElem_cons_zero
+@[deprecated (since := "2024-06-12")] abbrev cons_getElem_zero := @getElem_cons_zero
 
 @[simp] theorem getElem_cons_succ (a : α) (as : List α) (i : Nat) (h : i + 1 < (a :: as).length) : getElem (a :: as) (i+1) h = getElem as i (Nat.lt_of_succ_lt_succ h) := by
   rfl
 
-@[deprecated (since := "2024-6-12")] abbrev cons_getElem_succ := @getElem_cons_succ
+@[deprecated (since := "2024-06-12")] abbrev cons_getElem_succ := @getElem_cons_succ
 
 theorem get_drop_eq_drop (as : List α) (i : Nat) (h : i < as.length) : as[i] :: as.drop (i+1) = as.drop i :=
   match as, i with
@@ -163,8 +217,6 @@ namespace Array
 instance : GetElem (Array α) Nat α fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
-instance : LawfulGetElem (Array α) Nat α fun xs i => i < xs.size where
-
 end Array
 
 namespace Lean.Syntax
@@ -172,6 +224,4 @@ namespace Lean.Syntax
 instance : GetElem Syntax Nat Syntax fun _ _ => True where
   getElem stx i _ := stx.getArg i
 
-instance : LawfulGetElem Syntax Nat Syntax fun _ _ => True where
-
 end Lean.Syntax

src/Init/MetaTypes.lean

@@ -218,6 +218,14 @@ structure Config where
   to find candidate `simp` theorems. It approximates Lean 3 `simp` behavior.
   -/
   index             : Bool := true
+  /--
+  When `true` (default: `false`), `simp` will **not** create a proof for a rewriting rule associated
+  with an `rfl`-theorem.
+  Rewriting rules are provided by users by annotating theorems with the attribute `@[simp]`.
+  If the proof of the theorem is just `rfl` (reflexivity), and `implicitDefEqProofs := true`, `simp`
+  will **not** create a proof term which is an application of the annotated theorem.
+  -/
+  implicitDefEqProofs : Bool := false
   deriving Inhabited, BEq
 
 -- Configuration object for `simp_all`

src/Init/PropLemmas.lean

@@ -368,9 +368,6 @@ else isTrue fun h2 => absurd h2 h
 
 theorem decide_eq_true_iff (p : Prop) [Decidable p] : (decide p = true) ↔ p := by simp
 
-@[simp] theorem decide_eq_false_iff_not (p : Prop) {_ : Decidable p} : (decide p = false) ↔ ¬p :=
-  ⟨of_decide_eq_false, decide_eq_false⟩
-
 @[simp] theorem decide_eq_decide {p q : Prop} {_ : Decidable p} {_ : Decidable q} :
     decide p = decide q ↔ (p ↔ q) :=
   ⟨fun h => by rw [← decide_eq_true_iff p, h, decide_eq_true_iff], fun h => by simp [h]⟩

src/Init/SimpLemmas.lean

@@ -228,25 +228,22 @@ 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
 @[simp] theorem Bool.not_false : (!false) = true := by decide
-@[simp] theorem Bool.not_beq_true  (b : Bool) : (!(b == true)) = (b == false) := by cases b <;> rfl
-@[simp] theorem Bool.not_beq_false (b : Bool) : (!(b == false)) = (b == true) := by cases b <;> rfl
+@[simp] theorem beq_true  (b : Bool) : (b == true)  =  b := by cases b <;> rfl
+@[simp] theorem beq_false (b : Bool) : (b == false) = !b := by cases b <;> rfl
 @[simp] theorem Bool.not_eq_true'  (b : Bool) : ((!b) = true) = (b = false) := by cases b <;> simp
 @[simp] theorem Bool.not_eq_false' (b : Bool) : ((!b) = false) = (b = true) := by cases b <;> simp
 
-@[simp] theorem Bool.beq_to_eq (a b : Bool) :
-  (a == b) = (a = b) := by cases a <;> cases b <;> decide
-@[simp] theorem Bool.not_beq_to_not_eq (a b : Bool) :
-  (!(a == b)) = ¬(a = b) := by cases a <;> cases b <;> decide
-
 @[simp] theorem Bool.not_eq_true (b : Bool) : (¬(b = true)) = (b = false) := by cases b <;> decide
 @[simp] theorem Bool.not_eq_false (b : Bool) : (¬(b = false)) = (b = true) := by cases b <;> decide
 
 @[simp] theorem decide_eq_true_eq [Decidable p] : (decide p = true) = p :=
   propext <| Iff.intro of_decide_eq_true decide_eq_true
+@[simp] theorem decide_eq_false_iff_not {_ : Decidable p} : (decide p = false) ↔ ¬p :=
+  ⟨of_decide_eq_false, decide_eq_false⟩
+
 @[simp] theorem decide_not [g : Decidable p] [h : Decidable (Not p)] : decide (Not p) = !(decide p) := by
   cases g <;> (rename_i gp; simp [gp]; rfl)
-@[simp] theorem not_decide_eq_true [h : Decidable p] : ((!decide p) = true) = ¬ p := by
-  cases h <;> (rename_i hp; simp [decide, hp])
+@[simp] theorem not_decide_eq_true [h : Decidable p] : ((!decide p) = true) = ¬ p := by simp
 
 @[simp] theorem heq_eq_eq (a b : α) : HEq a b = (a = b) := propext <| Iff.intro eq_of_heq heq_of_eq
 
@@ -254,10 +251,10 @@ instance : Std.Associative (· || ·) := ⟨Bool.or_assoc⟩
 @[simp] theorem cond_false (a b : α) : cond false a b = b := rfl
 
 @[simp] theorem beq_self_eq_true [BEq α] [LawfulBEq α] (a : α) : (a == a) = true := LawfulBEq.rfl
-@[simp] theorem beq_self_eq_true' [DecidableEq α] (a : α) : (a == a) = true := by simp [BEq.beq]
+theorem beq_self_eq_true' [DecidableEq α] (a : α) : (a == a) = true := by simp
 
 @[simp] theorem bne_self_eq_false [BEq α] [LawfulBEq α] (a : α) : (a != a) = false := by simp [bne]
-@[simp] theorem bne_self_eq_false' [DecidableEq α] (a : α) : (a != a) = false := by simp [bne]
+theorem bne_self_eq_false' [DecidableEq α] (a : α) : (a != a) = false := by simp
 
 @[simp] theorem decide_False : decide False = false := rfl
 @[simp] theorem decide_True  : decide True  = true := rfl
@@ -283,7 +280,10 @@ These will both normalize to `a = b` with the first via `bne_eq_false_iff_eq`.
   rw [bne, ← beq_iff_eq a b]
   cases a == b <;> decide
 
-/-# Nat -/
+theorem Bool.beq_to_eq (a b : Bool) : (a == b) = (a = b) := by simp
+theorem Bool.not_beq_to_not_eq (a b : Bool) : (!(a == b)) = ¬(a = b) := by simp
+
+/- # Nat -/
 
 @[simp] theorem Nat.le_zero_eq (a : Nat) : (a ≤ 0) = (a = 0) :=
   propext ⟨fun h => Nat.le_antisymm h (Nat.zero_le ..), fun h => by rw [h]; decide⟩

src/Init/System/IO.lean

@@ -814,6 +814,10 @@ def set (tk : CancelToken) : BaseIO Unit :=
 def isSet (tk : CancelToken) : BaseIO Bool :=
   tk.ref.get
 
+-- separate definition as otherwise no unboxed version is generated
+@[export lean_io_cancel_token_is_set]
+private def isSetExport := @isSet
+
 end CancelToken
 
 namespace FS

src/Init/WF.lean

@@ -288,7 +288,7 @@ instance [ha : WellFoundedRelation α] [hb : WellFoundedRelation β] : WellFound
   lex ha hb
 
 -- relational product is a Subrelation of the Lex
-def RProdSubLex (a : α × β) (b : α × β) (h : RProd ra rb a b) : Prod.Lex ra rb a b := by
+theorem RProdSubLex (a : α × β) (b : α × β) (h : RProd ra rb a b) : Prod.Lex ra rb a b := by
   cases h with
   | intro h₁ h₂ => exact Prod.Lex.left _ _ h₁
 
@@ -320,7 +320,7 @@ section
 variable {α : Sort u} {β : α → Sort v}
 variable {r  : α → α → Prop} {s : ∀ (a : α), β a → β a → Prop}
 
-def lexAccessible {a} (aca : Acc r a) (acb : (a : α) → WellFounded (s a)) (b : β a) : Acc (Lex r s) ⟨a, b⟩ := by
+theorem lexAccessible {a} (aca : Acc r a) (acb : (a : α) → WellFounded (s a)) (b : β a) : Acc (Lex r s) ⟨a, b⟩ := by
   induction aca with
   | intro xa _ iha =>
     induction (WellFounded.apply (acb xa) b) with

src/Lean/AddDecl.lean

@@ -8,11 +8,22 @@ import Lean.CoreM
 
 namespace Lean
 
-def Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration) : Except KernelException Environment :=
-  addDeclCore env (Core.getMaxHeartbeats opts).toUSize decl
+register_builtin_option debug.skipKernelTC : Bool := {
+  defValue := false
+  group    := "debug"
+  descr    := "skip kernel type checker. WARNING: setting this option to true may compromise soundness because your proofs will not be checked by the Lean kernel"
+}
 
-def Environment.addAndCompile (env : Environment) (opts : Options) (decl : Declaration) : Except KernelException Environment := do
-  let env ← addDecl env opts decl
+def Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration)
+    (cancelTk? : Option IO.CancelToken := none) : Except KernelException Environment :=
+  if debug.skipKernelTC.get opts then
+    addDeclWithoutChecking env decl
+  else
+    addDeclCore env (Core.getMaxHeartbeats opts).toUSize decl cancelTk?
+
+def Environment.addAndCompile (env : Environment) (opts : Options) (decl : Declaration)
+    (cancelTk? : Option IO.CancelToken := none) : Except KernelException Environment := do
+  let env ← addDecl env opts decl cancelTk?
   compileDecl env opts decl
 
 def addDecl (decl : Declaration) : CoreM Unit := do
@@ -20,7 +31,7 @@ def addDecl (decl : Declaration) : CoreM Unit := 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
+      match (← getEnv).addDecl (← getOptions) decl (← read).cancelTk? with
       | .ok    env => setEnv env
       | .error ex  => throwKernelException ex
 

src/Lean/CoreM.lean

@@ -211,12 +211,12 @@ instance : MonadTrace CoreM where
 
 structure SavedState extends State where
   /-- Number of heartbeats passed inside `withRestoreOrSaveFull`, not used otherwise. -/
-  passedHearbeats : Nat
+  passedHeartbeats : Nat
 deriving Nonempty
 
 def saveState : CoreM SavedState := do
   let s ← get
-  return { toState := s, passedHearbeats := 0 }
+  return { toState := s, passedHeartbeats := 0 }
 
 /--
 Incremental reuse primitive: if `reusableResult?` is `none`, runs `act` and returns its result
@@ -236,14 +236,14 @@ itself after calling `act` as well as by reuse-handling code such as the one sup
     (act : CoreM α) : CoreM (α × SavedState) := do
   if let some (val, state) := reusableResult? then
     set state.toState
-    IO.addHeartbeats state.passedHearbeats.toUInt64
+    IO.addHeartbeats state.passedHeartbeats.toUInt64
     return (val, state)
 
   let startHeartbeats ← IO.getNumHeartbeats
   let a ← act
   let s ← get
   let stopHeartbeats ← IO.getNumHeartbeats
-  return (a, { toState := s, passedHearbeats := stopHeartbeats - startHeartbeats })
+  return (a, { toState := s, passedHeartbeats := stopHeartbeats - startHeartbeats })
 
 /-- Restore backtrackable parts of the state. -/
 def SavedState.restore (b : SavedState) : CoreM Unit :=
@@ -472,23 +472,30 @@ def Exception.isInterrupt : Exception → Bool
 
 /--
 Custom `try-catch` for all monads based on `CoreM`. We usually don't want to catch "runtime
-exceptions" these monads, but on `CommandElabM`. See issues #2775 and #2744 as well as
-`MonadAlwaysExcept`. Also, we never want to catch interrupt exceptions inside the elaborator.
+exceptions" these monads, but on `CommandElabM` or, in specific cases, using `tryCatchRuntimeEx`.
+See issues #2775 and #2744 as well as `MonadAlwaysExcept`. Also, we never want to catch interrupt
+exceptions inside the elaborator.
 -/
 @[inline] protected def Core.tryCatch (x : CoreM α) (h : Exception → CoreM α) : CoreM α := do
   try
     x
   catch ex =>
     if ex.isInterrupt || ex.isRuntime then
-
-      throw ex -- We should use `tryCatchRuntimeEx` for catching runtime exceptions
+      throw ex
     else
       h ex
 
+/--
+A variant of `tryCatch` that also catches runtime exception (see also `tryCatch` documentation).
+Like `tryCatch`, this function does not catch interrupt exceptions, which are not considered runtime
+exceptions.
+-/
 @[inline] protected def Core.tryCatchRuntimeEx (x : CoreM α) (h : Exception → CoreM α) : CoreM α := do
   try
     x
   catch ex =>
+    if ex.isInterrupt then
+      throw ex
     h ex
 
 instance : MonadExceptOf Exception CoreM where
@@ -512,4 +519,16 @@ instance : MonadRuntimeException CoreM where
 @[inline] def mapCoreM [MonadControlT CoreM m] [Monad m] (f : forall {α}, CoreM α → CoreM α) {α} (x : m α) : m α :=
   controlAt CoreM fun runInBase => f <| runInBase x
 
+/--
+Returns `true` if the given message kind has not been reported in the message log,
+and then mark it as reported. Otherwise, returns `false`.
+We use this API to ensure we don't report the same kind of warning multiple times.
+-/
+def reportMessageKind (kind : Name) : CoreM Bool := do
+  if (← get).messages.reportedKinds.contains kind then
+    return false
+  else
+    modify fun s => { s with messages.reportedKinds := s.messages.reportedKinds.insert kind }
+    return true
+
 end Lean

src/Lean/Data/HashMap.lean

@@ -223,8 +223,6 @@ def insertIfNew (m : HashMap α β) (a : α) (b : β) : HashMap α β × Option
 instance : GetElem (HashMap α β) α (Option β) fun _ _ => True where
   getElem m k _ := m.find? k
 
-instance : LawfulGetElem (HashMap α β) α (Option β) fun _ _ => True where
-
 @[inline] def contains (m : HashMap α β) (a : α) : Bool :=
   match m with
   | ⟨ m, _ ⟩ => m.contains a

src/Lean/Data/PersistentArray.lean

@@ -72,8 +72,6 @@ def get! [Inhabited α] (t : PersistentArray α) (i : Nat) : α :=
 instance [Inhabited α] : GetElem (PersistentArray α) Nat α fun as i => i < as.size where
   getElem xs i _ := xs.get! i
 
-instance [Inhabited α] : LawfulGetElem (PersistentArray α) Nat α fun as i => i < as.size where
-
 partial def setAux : PersistentArrayNode α → USize → USize → α → PersistentArrayNode α
   | node cs, i, shift, a =>
     let j     := div2Shift i shift

src/Lean/Data/PersistentHashMap.lean

@@ -161,8 +161,6 @@ def find? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → Op
 instance {_ : BEq α} {_ : Hashable α} : GetElem (PersistentHashMap α β) α (Option β) fun _ _ => True where
   getElem m i _ := m.find? i
 
-instance {_ : BEq α} {_ : Hashable α} : LawfulGetElem (PersistentHashMap α β) α (Option β) fun _ _ => True where
-
 @[inline] def findD {_ : BEq α} {_ : Hashable α} (m : PersistentHashMap α β) (a : α) (b₀ : β) : β :=
   (m.find? a).getD b₀
 

src/Lean/Elab/App.lean

@@ -1424,8 +1424,27 @@ private def getSuccesses (candidates : Array (TermElabResult Expr)) : TermElabM
           return false
       return true
     | _ => return false
-  if r₂.size == 0 then return r₁ else return r₂
-
+  if r₂.size == 0 then
+    return r₁
+  if r₂.size == 1 then
+    return r₂
+  /-
+  If there are still more than one solution, discard solutions that have pending metavariables.
+  We added this extra filter to address regressions introduced after fixing
+  `isDefEqStuckEx` behavior at `ExprDefEq.lean`.
+  -/
+  let r₂ ← candidates.filterM fun
+    | .ok _ s => do
+      try
+        s.restore
+        synthesizeSyntheticMVars (postpone := .no)
+        return true
+      catch _ =>
+        return false
+    | _ => return false
+  if r₂.size == 0 then
+    return r₁
+  return r₂
 /--
   Throw an error message that describes why each possible interpretation for the overloaded notation and symbols did not work.
   We use a nested error message to aggregate the exceptions produced by each failure.

src/Lean/Elab/Binders.lean

@@ -8,7 +8,7 @@ import Lean.Elab.Quotation.Precheck
 import Lean.Elab.Term
 import Lean.Elab.BindersUtil
 import Lean.Elab.SyntheticMVars
-import Lean.Elab.PreDefinition.WF.TerminationHint
+import Lean.Elab.PreDefinition.TerminationHint
 
 namespace Lean.Elab.Term
 open Meta

src/Lean/Elab/BuiltinNotation.lean

@@ -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) -- Remark: we use `@` to ensure `sorryAx` will not consume auot params
+  let stxNew ← `(@sorryAx _ false) -- Remark: we use `@` to ensure `sorryAx` will not consume auto 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])))` -/

src/Lean/Elab/BuiltinTerm.lean

@@ -157,9 +157,19 @@ private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr :=
   registerSyntheticMVar ref mvarId <| SyntheticMVarKind.tactic tacticCode (← saveContext)
   return mvar
 
+register_builtin_option debug.byAsSorry : Bool := {
+  defValue := false
+  group    := "debug"
+  descr    := "replace `by ..` blocks with `sorry` IF the expected type is a proposition"
+}
+
 @[builtin_term_elab byTactic] def elabByTactic : TermElab := fun stx expectedType? => do
   match expectedType? with
-  | some expectedType => mkTacticMVar expectedType stx
+  | some expectedType =>
+    if ← pure (debug.byAsSorry.get (← getOptions)) <&&> isProp expectedType then
+      mkSorry expectedType false
+    else
+      mkTacticMVar expectedType stx
   | none =>
     tryPostpone
     throwError ("invalid 'by' tactic, expected type has not been provided")

src/Lean/Elab/Command.lean

@@ -81,7 +81,10 @@ Remark: see comment at TermElabM
 @[always_inline]
 instance : Monad CommandElabM := let i := inferInstanceAs (Monad CommandElabM); { pure := i.pure, bind := i.bind }
 
-/-- Like `Core.tryCatch` but do catch runtime exceptions. -/
+/--
+Like `Core.tryCatchRuntimeEx`; runtime errors are generally used to abort term elaboration, so we do
+want to catch and process them at the command level.
+-/
 @[inline] protected def tryCatch (x : CommandElabM α) (h : Exception → CommandElabM α) :
     CommandElabM α := do
   try

src/Lean/Elab/ComputedFields.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner
 -/
 prelude
-import Lean.Meta.Constructions
+import Lean.Meta.Constructions.CasesOn
 import Lean.Compiler.ImplementedByAttr
 import Lean.Elab.PreDefinition.WF.Eqns
 

src/Lean/Elab/LetRec.lean

@@ -22,7 +22,7 @@ structure LetRecDeclView where
   type          : Expr
   mvar          : Expr -- auxiliary metavariable used to lift the 'let rec'
   valStx        : Syntax
-  termination   : WF.TerminationHints
+  termination   : TerminationHints
 
 structure LetRecView where
   decls     : Array LetRecDeclView
@@ -30,20 +30,24 @@ structure LetRecView where
 
 /-  group ("let " >> nonReservedSymbol "rec ") >> sepBy1 (group (optional «attributes» >> letDecl)) ", " >> "; " >> termParser -/
 private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
-  let decls ← letRec[1][0].getSepArgs.mapM fun (attrDeclStx : Syntax) => do
+  let mut decls : Array LetRecDeclView := #[]
+  for attrDeclStx in letRec[1][0].getSepArgs do
     let docStr? ← expandOptDocComment? attrDeclStx[0]
     let attrOptStx := attrDeclStx[1]
     let attrs ← if attrOptStx.isNone then pure #[] else elabDeclAttrs attrOptStx[0]
     let decl := attrDeclStx[2][0]
     if decl.isOfKind `Lean.Parser.Term.letPatDecl then
       throwErrorAt decl "patterns are not allowed in 'let rec' expressions"
-    else if decl.isOfKind `Lean.Parser.Term.letIdDecl || decl.isOfKind `Lean.Parser.Term.letEqnsDecl then
+    else if decl.isOfKind ``Lean.Parser.Term.letIdDecl || decl.isOfKind ``Lean.Parser.Term.letEqnsDecl then
       let declId := decl[0]
       unless declId.isIdent do
         throwErrorAt declId "'let rec' expressions must be named"
       let shortDeclName := declId.getId
       let currDeclName? ← getDeclName?
       let declName := currDeclName?.getD Name.anonymous ++ shortDeclName
+      if decls.any fun decl => decl.declName == declName then
+        withRef declId do
+          throwError "'{declName}' has already been declared"
       checkNotAlreadyDeclared declName
       applyAttributesAt declName attrs AttributeApplicationTime.beforeElaboration
       addDocString' declName docStr?
@@ -61,9 +65,11 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
         pure decl[4]
       else
         liftMacroM <| expandMatchAltsIntoMatch decl decl[3]
-      let termination ← WF.elabTerminationHints ⟨attrDeclStx[3]⟩
-      pure { ref := declId, attrs, shortDeclName, declName, binderIds, type, mvar, valStx,
-             termination : LetRecDeclView }
+      let termination ← elabTerminationHints ⟨attrDeclStx[3]⟩
+      decls := decls.push {
+        ref := declId, attrs, shortDeclName, declName,
+        binderIds, type, mvar, valStx, termination
+      }
     else
       throwUnsupportedSyntax
   return { decls, body := letRec[3] }

src/Lean/Elab/MutualDef.lean

@@ -14,7 +14,7 @@ import Lean.Elab.Match
 import Lean.Elab.DefView
 import Lean.Elab.Deriving.Basic
 import Lean.Elab.PreDefinition.Main
-import Lean.Elab.PreDefinition.WF.TerminationHint
+import Lean.Elab.PreDefinition.TerminationHint
 import Lean.Elab.DeclarationRange
 
 namespace Lean.Elab
@@ -167,7 +167,7 @@ private def elabHeaders (views : Array DefView)
         else
           reuseBody := false
 
-      let mut (newHeader, newState) ← withRestoreOrSaveFull reusableResult? do
+      let mut (newHeader, newState) ← withRestoreOrSaveFull reusableResult? none do
         withRef view.headerRef do
         addDeclarationRanges declName view.ref  -- NOTE: this should be the full `ref`
         applyAttributesAt declName view.modifiers.attrs .beforeElaboration
@@ -320,11 +320,11 @@ private def declValToTerm (declVal : Syntax) : MacroM Syntax := withRef declVal
     Macro.throwErrorAt declVal "unexpected declaration body"
 
 /-- Elaborates the termination hints in a `declVal` syntax. -/
-private def declValToTerminationHint (declVal : Syntax) : TermElabM WF.TerminationHints :=
+private def declValToTerminationHint (declVal : Syntax) : TermElabM TerminationHints :=
   if declVal.isOfKind ``Parser.Command.declValSimple then
-    WF.elabTerminationHints ⟨declVal[2]⟩
+    elabTerminationHints ⟨declVal[2]⟩
   else if declVal.isOfKind ``Parser.Command.declValEqns then
-    WF.elabTerminationHints ⟨declVal[0][1]⟩
+    elabTerminationHints ⟨declVal[0][1]⟩
   else
     return .none
 
@@ -337,14 +337,9 @@ private def elabFunValues (headers : Array DefViewElabHeader) : TermElabM (Array
         -- elaboration
         if let some old := old.val.get then
           snap.new.resolve <| some old
-          -- also make sure to reuse tactic snapshots if present so that body reuse does not lead to
-          -- missed tactic reuse on further changes
-          if let some tacSnap := header.tacSnap? then
-            if let some oldTacSnap := tacSnap.old? then
-              tacSnap.new.resolve oldTacSnap.val.get
           reusableResult? := some (old.value, old.state)
 
-    let (val, state) ← withRestoreOrSaveFull reusableResult? do
+    let (val, state) ← withRestoreOrSaveFull reusableResult? header.tacSnap? do
       withDeclName header.declName <| withLevelNames header.levelNames do
       let valStx ← liftMacroM <| declValToTerm header.value
       forallBoundedTelescope header.type header.numParams fun xs type => do
@@ -846,10 +841,7 @@ private def levelMVarToParamHeaders (views : Array DefView) (headers : Array Def
   let rec process : StateRefT Nat TermElabM (Array DefViewElabHeader) := do
     let mut newHeaders := #[]
     for view in views, header in headers do
-      -- Remark: we should consider using `pure view.kind.isTheorem <||> isProp header.type`, and
-      -- also handle definitions. We used the following approach because it is less disruptive to Mathlib.
-      -- Moreover, the type of most definitions are not propositions anyway.
-      if ← pure view.kind.isTheorem <||> (pure view.kind.isExample <&&> isProp header.type) then
+      if ← pure view.kind.isTheorem <||> isProp header.type then
         newHeaders ←
           withLevelNames header.levelNames do
             return newHeaders.push { header with type := (← levelMVarToParam header.type), levelNames := (← getLevelNames) }

src/Lean/Elab/PreDefinition/Basic.lean

@@ -10,7 +10,7 @@ import Lean.Meta.AbstractNestedProofs
 import Lean.Meta.ForEachExpr
 import Lean.Elab.RecAppSyntax
 import Lean.Elab.DefView
-import Lean.Elab.PreDefinition.WF.TerminationHint
+import Lean.Elab.PreDefinition.TerminationHint
 
 namespace Lean.Elab
 open Meta
@@ -29,7 +29,7 @@ structure PreDefinition where
   declName    : Name
   type        : Expr
   value       : Expr
-  termination : WF.TerminationHints
+  termination : TerminationHints
   deriving Inhabited
 
 def PreDefinition.filterAttrs (preDef : PreDefinition) (p : Attribute → Bool) : PreDefinition :=

src/Lean/Elab/PreDefinition/Main.lean

@@ -95,6 +95,64 @@ def ensureFunIndReservedNamesAvailable (preDefs : Array PreDefinition) : MetaM U
     withRef preDef.ref <| ensureReservedNameAvailable preDef.declName "induct"
   withRef preDefs[0]!.ref <| ensureReservedNameAvailable preDefs[0]!.declName "mutual_induct"
 
+
+/--
+Checks consistency of a clique of TerminationHints:
+
+* If not all have a hint, the hints are ignored (log error)
+* If one has `structural`, check that all have it, (else throw error)
+* A `structural` shold not have a `decreasing_by` (else log error)
+
+-/
+def checkTerminationByHints (preDefs : Array PreDefinition) : CoreM Unit := do
+  let some preDefWith := preDefs.find? (·.termination.terminationBy?.isSome) | return
+  let preDefsWithout := preDefs.filter (·.termination.terminationBy?.isNone)
+  let structural :=
+    preDefWith.termination.terminationBy? matches some {structural := true, ..}
+  for preDef in preDefs do
+    if let .some termBy := preDef.termination.terminationBy? then
+      if !preDefsWithout.isEmpty then
+        let m := MessageData.andList (preDefsWithout.toList.map (m!"{·.declName}"))
+        let doOrDoes := if preDefsWithout.size = 1 then "does" else "do"
+        logErrorAt termBy.ref (m!"Incomplete set of `termination_by` annotations:\n"++
+          m!"This function is mutually with {m}, which {doOrDoes} not have " ++
+          m!"a `termination_by` clause.\n" ++
+          m!"The present clause is ignored.")
+
+      if structural && ! termBy.structural then
+        throwErrorAt termBy.ref (m!"Invalid `termination_by`; this function is mutually " ++
+          m!"recursive with {preDefWith.declName}, which is marked as `termination_by " ++
+          m!"structural` so this one also needs to be marked `structural`.")
+      if ! structural && termBy.structural then
+        throwErrorAt termBy.ref (m!"Invalid `termination_by`; this function is mutually " ++
+          m!"recursive with {preDefWith.declName}, which is not marked as `structural` " ++
+          m!"so this one cannot be `structural` either.")
+      if termBy.structural then
+        if let .some decr := preDef.termination.decreasingBy? then
+          logErrorAt decr.ref (m!"Invalid `decreasing_by`; this function is marked as " ++
+            m!"structurally recursive, so no explicit termination proof is needed.")
+
+/--
+Elaborates the `TerminationHint` in the clique to `TerminationArguments`
+-/
+def elabTerminationByHints (preDefs : Array PreDefinition) : TermElabM (Option TerminationArguments) := do
+  let tas ← preDefs.mapM fun preDef => do
+    let arity ← lambdaTelescope preDef.value fun xs _ => pure xs.size
+    let hints := preDef.termination
+    hints.terminationBy?.mapM
+      (TerminationArgument.elab preDef.declName preDef.type arity hints.extraParams ·)
+  return tas.sequenceMap id -- only return something if every function has a hint
+
+def shouldUseStructural (preDefs : Array PreDefinition) : Bool :=
+  preDefs.any fun preDef =>
+    preDef.termination.terminationBy? matches some {structural := true, ..}
+
+def shouldUseWF (preDefs : Array PreDefinition) : Bool :=
+  preDefs.any fun preDef =>
+    preDef.termination.terminationBy? matches some {structural := false, ..} ||
+    preDef.termination.decreasingBy?.isSome
+
+
 def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLCtx {} {} do
   for preDef in preDefs do
     trace[Elab.definition.body] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
@@ -128,14 +186,17 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
     else
       ensureFunIndReservedNamesAvailable preDefs
       try
-        let hasHints := preDefs.any fun preDef => preDef.termination.isNotNone
-        if hasHints then
-          wfRecursion preDefs
+        checkTerminationByHints preDefs
+        let termArgs ← elabTerminationByHints preDefs
+        if shouldUseStructural preDefs then
+          structuralRecursion preDefs termArgs
+        else if shouldUseWF preDefs then
+          wfRecursion preDefs termArgs
         else
           withRef (preDefs[0]!.ref) <| mapError
             (orelseMergeErrors
-              (structuralRecursion preDefs)
-              (wfRecursion preDefs))
+              (structuralRecursion preDefs termArgs)
+              (wfRecursion preDefs termArgs))
             (fun msg =>
               let preDefMsgs := preDefs.toList.map (MessageData.ofExpr $ mkConst ·.declName)
               m!"fail to show termination for{indentD (MessageData.joinSep preDefMsgs Format.line)}\nwith errors\n{msg}")

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

@@ -153,9 +153,9 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo)
           trace[Elab.definition.structural] "below before matcherApp.addArg: {below} : {← inferType below}"
           if let some matcherApp ← matcherApp.addArg? below then
             let altsNew ← (Array.zip matcherApp.alts matcherApp.altNumParams).mapM fun (alt, numParams) =>
-              lambdaTelescope alt fun xs altBody => do
+              lambdaBoundedTelescope alt numParams fun xs altBody => do
                 trace[Elab.definition.structural] "altNumParams: {numParams}, xs: {xs}"
-                unless xs.size >= numParams do
+                unless xs.size = numParams do
                   throwError "unexpected matcher application alternative{indentExpr alt}\nat application{indentExpr e}"
                 let belowForAlt := xs[numParams - 1]!
                 mkLambdaFVars xs (← loop belowForAlt altBody)

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

@@ -19,7 +19,8 @@ open Eqns
 namespace Structural
 
 structure EqnInfo extends EqnInfoCore where
-  recArgPos   : Nat
+  recArgPos : Nat
+  declNames : Array Name
   deriving Inhabited
 
 private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
@@ -80,9 +81,9 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
 
 builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension
 
-def registerEqnsInfo (preDef : PreDefinition) (recArgPos : Nat) : CoreM Unit := do
+def registerEqnsInfo (preDef : PreDefinition) (declNames : Array Name) (recArgPos : Nat) : CoreM Unit := do
   ensureEqnReservedNamesAvailable preDef.declName
-  modifyEnv fun env => eqnInfoExt.insert env preDef.declName { preDef with recArgPos }
+  modifyEnv fun env => eqnInfoExt.insert env preDef.declName { preDef with recArgPos, declNames }
 
 def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
   if let some info := eqnInfoExt.find? (← getEnv) declName then

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

@@ -35,12 +35,61 @@ private def hasBadParamDep? (ys : Array Expr) (indParams : Array Expr) : MetaM (
         return some (p, y)
   return none
 
-private def throwStructuralFailed : MetaM α :=
-  throwError "structural recursion cannot be used"
-
-private def orelse' (x y : M α) : M α := do
-  let saveState ← get
-  orelseMergeErrors x (do set saveState; y)
+/--
+Pass to `k` the `RecArgInfo` for the `i`th parameter in the parameter list `xs`. This performs
+various sanity checks on the argument (is it even an inductive type etc).
+Also wraps all errors in a common “argument cannot be used” header
+-/
+def withRecArgInfo (numFixed : Nat) (xs : Array Expr) (i : Nat) (k : RecArgInfo → M α) : M α := do
+  mapError
+    (f := fun msg => m!"argument #{i+1} cannot be used for structural recursion{indentD msg}") do
+  if h : i < xs.size then
+    if i < numFixed then
+      throwError "it is unchanged in the recursive calls"
+    let x := xs[i]
+    let localDecl ← getFVarLocalDecl x
+    if localDecl.isLet then
+      throwError "it is a let-binding"
+    let xType ← whnfD localDecl.type
+    matchConstInduct xType.getAppFn (fun _ => throwError "its type is not an inductive") fun indInfo us => do
+    if !(← hasConst (mkBRecOnName indInfo.name)) then
+      throwError "its type does not have a recursor"
+    else if indInfo.isReflexive && !(← hasConst (mkBInductionOnName indInfo.name)) && !(← isInductivePredicate indInfo.name) then
+      throwError "its type is a reflexive inductive, but {mkBInductionOnName indInfo.name} does not exist and it is not an inductive predicate"
+    else
+      let indArgs    := xType.getAppArgs
+      let indParams  := indArgs.extract 0 indInfo.numParams
+      let indIndices := indArgs.extract indInfo.numParams indArgs.size
+      if !indIndices.all Expr.isFVar then
+        throwError "its type is an inductive family and indices are not variables{indentExpr xType}"
+      else if !indIndices.allDiff then
+        throwError " its type is an inductive family and indices are not pairwise distinct{indentExpr xType}"
+      else
+        let indexMinPos := getIndexMinPos xs indIndices
+        let numFixed    := if indexMinPos < numFixed then indexMinPos else numFixed
+        let fixedParams := xs.extract 0 numFixed
+        let ys          := xs.extract numFixed xs.size
+        match (← hasBadIndexDep? ys indIndices) with
+        | some (index, y) =>
+          throwError "its type is an inductive family{indentExpr xType}\nand index{indentExpr index}\ndepends on the non index{indentExpr y}"
+        | none =>
+          match (← hasBadParamDep? ys indParams) with
+          | some (indParam, y) =>
+            throwError "its type is an inductive datatype{indentExpr xType}\nand parameter{indentExpr indParam}\ndepends on{indentExpr y}"
+          | none =>
+            let indicesPos := indIndices.map fun index => match ys.indexOf? index with | some i => i.val | none => unreachable!
+            k { fixedParams := fixedParams
+                ys          := ys
+                pos         := i - fixedParams.size
+                indicesPos  := indicesPos
+                indName     := indInfo.name
+                indLevels   := us
+                indParams   := indParams
+                indIndices  := indIndices
+                reflexive   := indInfo.isReflexive
+                indPred     := ←isInductivePredicate indInfo.name }
+    else
+      throwError "the index #{i+1} exceeds {xs.size}, the number of parameters"
 
 /--
   Try to find an argument that is structurally smaller in every recursive application.
@@ -49,16 +98,10 @@ private def orelse' (x y : M α) : M α := do
   We give preference for arguments that are *not* indices of inductive types of other arguments.
   See issue #837 for an example where we can show termination using the index of an inductive family, but
   we don't get the desired definitional equalities.
-
-  We perform two passes. In the first-pass, we only consider arguments that are not indices.
-  In the second pass, we consider them.
-
-  TODO: explore whether there are better solutions, and whether there are other ways to break the heuristic used
-  for creating the smart unfolding auxiliary definition.
 -/
 partial def findRecArg (numFixed : Nat) (xs : Array Expr) (k : RecArgInfo → M α) : M α := do
   /- Collect arguments that are indices. See comment above. -/
-  let indicesRef : IO.Ref FVarIdSet ← IO.mkRef {}
+  let indicesRef : IO.Ref (Array Nat) ← IO.mkRef {}
   for x in xs do
     let xType ← inferType x
     /- Traverse all sub-expressions in the type of `x` -/
@@ -68,75 +111,22 @@ partial def findRecArg (numFixed : Nat) (xs : Array Expr) (k : RecArgInfo → M
         if info.numIndices > 0 && info.numParams + info.numIndices == e.getAppNumArgs then
           for arg in e.getAppArgs[info.numParams:] do
             forEachExpr arg fun e => do
-              if e.isFVar && xs.any (· == e) then
-                indicesRef.modify fun indices => indices.insert e.fvarId!
+              if let .some idx := xs.getIdx? e then
+                indicesRef.modify fun indices => indices.push idx
   let indices ← indicesRef.get
-  /- We perform two passes. See comment above. -/
-  let rec go (i : Nat) (firstPass : Bool) : M α := do
-    if h : i < xs.size then
-      let x := xs.get ⟨i, h⟩
-      trace[Elab.definition.structural] "findRecArg x: {x}, firstPass: {firstPass}"
-      let localDecl ← getFVarLocalDecl x
-      if localDecl.isLet then
-        throwStructuralFailed
-      else if firstPass == indices.contains localDecl.fvarId then
-        go (i+1) firstPass
-      else
-        let xType ← whnfD localDecl.type
-        matchConstInduct xType.getAppFn (fun _ => go (i+1) firstPass) fun indInfo us => do
-        if !(← hasConst (mkBRecOnName indInfo.name)) then
-          go (i+1) firstPass
-        else if indInfo.isReflexive && !(← hasConst (mkBInductionOnName indInfo.name)) && !(← isInductivePredicate indInfo.name) then
-          go (i+1) firstPass
-        else
-          let indArgs    := xType.getAppArgs
-          let indParams  := indArgs.extract 0 indInfo.numParams
-          let indIndices := indArgs.extract indInfo.numParams indArgs.size
-          if !indIndices.all Expr.isFVar then
-            orelse'
-              (throwError "argument #{i+1} was not used because its type is an inductive family and indices are not variables{indentExpr xType}")
-              (go (i+1) firstPass)
-          else if !indIndices.allDiff then
-            orelse'
-              (throwError "argument #{i+1} was not used because its type is an inductive family and indices are not pairwise distinct{indentExpr xType}")
-              (go (i+1) firstPass)
-          else
-            let indexMinPos := getIndexMinPos xs indIndices
-            let numFixed    := if indexMinPos < numFixed then indexMinPos else numFixed
-            let fixedParams := xs.extract 0 numFixed
-            let ys          := xs.extract numFixed xs.size
-            match (← hasBadIndexDep? ys indIndices) with
-            | some (index, y) =>
-              orelse'
-                (throwError "argument #{i+1} was not used because its type is an inductive family{indentExpr xType}\nand index{indentExpr index}\ndepends on the non index{indentExpr y}")
-                (go (i+1) firstPass)
-            | none =>
-              match (← hasBadParamDep? ys indParams) with
-              | some (indParam, y) =>
-                orelse'
-                  (throwError "argument #{i+1} was not used because its type is an inductive datatype{indentExpr xType}\nand parameter{indentExpr indParam}\ndepends on{indentExpr y}")
-                  (go (i+1) firstPass)
-              | none =>
-                let indicesPos := indIndices.map fun index => match ys.indexOf? index with | some i => i.val | none => unreachable!
-                orelse'
-                  (mapError
-                    (k { fixedParams := fixedParams
-                         ys          := ys
-                         pos         := i - fixedParams.size
-                         indicesPos  := indicesPos
-                         indName     := indInfo.name
-                         indLevels   := us
-                         indParams   := indParams
-                         indIndices  := indIndices
-                         reflexive := indInfo.isReflexive
-                         indPred := ←isInductivePredicate indInfo.name })
-                    (fun msg => m!"argument #{i+1} was not used for structural recursion{indentD msg}"))
-                  (go (i+1) firstPass)
-    else if firstPass then
-      go (i := numFixed) (firstPass := false)
-    else
-      throwStructuralFailed
-
-  go (i := numFixed) (firstPass := true)
+  let nonIndices := (Array.range xs.size).filter (fun i => !(indices.contains i))
+  let mut errors : Array MessageData := Array.mkArray xs.size m!""
+  let saveState ← get -- backtrack the state for each argument
+  for i in id (nonIndices ++ indices) do
+    let x := xs[i]!
+    trace[Elab.definition.structural] "findRecArg x: {x}"
+    try
+      set saveState
+      return (← withRecArgInfo numFixed xs i k)
+    catch e => errors := errors.set! i e.toMessageData
+  throwError
+    errors.foldl
+      (init := m!"structural recursion cannot be used:")
+      (f := (· ++ Format.line ++ Format.line ++ .))
 
 end Lean.Elab.Structural

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

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Elab.PreDefinition.TerminationArgument
 import Lean.Elab.PreDefinition.Structural.Basic
 import Lean.Elab.PreDefinition.Structural.FindRecArg
 import Lean.Elab.PreDefinition.Structural.Preprocess
@@ -11,6 +12,7 @@ import Lean.Elab.PreDefinition.Structural.BRecOn
 import Lean.Elab.PreDefinition.Structural.IndPred
 import Lean.Elab.PreDefinition.Structural.Eqns
 import Lean.Elab.PreDefinition.Structural.SmartUnfolding
+import Lean.Meta.Tactic.TryThis
 
 namespace Lean.Elab
 namespace Structural
@@ -57,7 +59,7 @@ private def getFixedPrefix (declName : Name) (xs : Array Expr) (value : Expr) :
       return true
   numFixedRef.get
 
-private def elimRecursion (preDef : PreDefinition) : M (Nat × PreDefinition) := do
+private def elimRecursion (preDef : PreDefinition) (termArg? : Option TerminationArgument) : M (Nat × PreDefinition) := do
   trace[Elab.definition.structural] "{preDef.declName} := {preDef.value}"
   withoutModifyingEnv do lambdaTelescope preDef.value fun xs value => do
     addAsAxiom preDef
@@ -65,8 +67,7 @@ private def elimRecursion (preDef : PreDefinition) : M (Nat × PreDefinition) :=
     trace[Elab.definition.structural] "{preDef.declName} {xs} :=\n{value}"
     let numFixed ← getFixedPrefix preDef.declName xs value
     trace[Elab.definition.structural] "numFixed: {numFixed}"
-    findRecArg numFixed xs fun recArgInfo => do
-      -- when (recArgInfo.indName == `Nat) throwStructuralFailed -- HACK to skip Nat argument
+    let go := fun recArgInfo => do
       let valueNew ← if recArgInfo.indPred then
         mkIndPredBRecOn preDef.declName recArgInfo value
       else
@@ -77,12 +78,28 @@ private def elimRecursion (preDef : PreDefinition) : M (Nat × PreDefinition) :=
       let valueNew ← ensureNoRecFn preDef.declName valueNew
       let recArgPos := recArgInfo.fixedParams.size + recArgInfo.pos
       return (recArgPos, { preDef with value := valueNew })
+    -- Use termination_by annotation to find argument to recurse on, or just try all
+    match termArg? with
+    | .some termArg =>
+        assert! termArg.structural
+        withRecArgInfo numFixed xs (← termArg.structuralArg) go
+    | .none => findRecArg numFixed xs go
 
-def structuralRecursion (preDefs : Array PreDefinition) : TermElabM Unit :=
+def reportTermArg (preDef : PreDefinition) (recArgPos : Nat) : MetaM Unit := do
+  if let some ref := preDef.termination.terminationBy?? then
+    let fn ← lambdaTelescope preDef.value fun xs _ => mkLambdaFVars xs xs[recArgPos]!
+    let termArg : TerminationArgument := {ref := .missing, structural := true, fn}
+    let arity ← lambdaTelescope preDef.value fun xs _ => pure xs.size
+    let stx ← termArg.delab arity (extraParams := preDef.termination.extraParams)
+    Tactic.TryThis.addSuggestion ref stx
+
+def structuralRecursion (preDefs : Array PreDefinition) (termArgs? : Option TerminationArguments) : TermElabM Unit :=
   if preDefs.size != 1 then
     throwError "structural recursion does not handle mutually recursive functions"
   else do
-    let ((recArgPos, preDefNonRec), state) ← run <| elimRecursion preDefs[0]!
+    let termArg? := termArgs?.map (·[0]!)
+    let ((recArgPos, preDefNonRec), state) ← run <| elimRecursion preDefs[0]! termArg?
+    reportTermArg preDefNonRec recArgPos
     let preDefNonRec ← eraseRecAppSyntax preDefNonRec
     let mut preDef ← eraseRecAppSyntax preDefs[0]!
     state.addMatchers.forM liftM
@@ -99,7 +116,7 @@ def structuralRecursion (preDefs : Array PreDefinition) : TermElabM Unit :=
         for theorems and definitions that are propositions.
         See issue #2327
         -/
-        registerEqnsInfo preDef recArgPos
+        registerEqnsInfo preDef (preDefs.map (·.declName)) recArgPos
     addSmartUnfoldingDef preDef recArgPos
     markAsRecursive preDef.declName
     applyAttributesOf #[preDefNonRec] AttributeApplicationTime.afterCompilation

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

@@ -47,17 +47,13 @@ where
         else
           let mut altsNew := #[]
           for alt in matcherApp.alts, numParams in matcherApp.altNumParams do
-            let altNew ← lambdaTelescope alt fun xs altBody => do
-              unless xs.size >= numParams do
+            let altNew ← lambdaBoundedTelescope alt numParams fun xs altBody => do
+              unless xs.size = numParams do
                 throwError "unexpected matcher application alternative{indentExpr alt}\nat application{indentExpr e}"
               let altBody ← visit altBody
               let containsSUnfoldMatch := Option.isSome <| altBody.find? fun e => smartUnfoldingMatch? e |>.isSome
-              if !containsSUnfoldMatch then
-                let altBody ← mkLambdaFVars xs[numParams:xs.size] altBody
-                let altBody := markSmartUnfoldingMatchAlt altBody
-                mkLambdaFVars xs[0:numParams] altBody
-              else
-                mkLambdaFVars xs altBody
+              let altBody := if !containsSUnfoldMatch then markSmartUnfoldingMatchAlt altBody else altBody
+              mkLambdaFVars xs altBody
             altsNew := altsNew.push altNew
           return markSmartUnfoldingMatch { matcherApp with alts := altsNew }.toExpr
       | _ => processApp e

src/Lean/Elab/PreDefinition/TerminationArgument.lean

@@ -9,17 +9,19 @@ import Lean.Parser.Term
 import Lean.Elab.Term
 import Lean.Elab.Binders
 import Lean.Elab.SyntheticMVars
-import Lean.Elab.PreDefinition.WF.TerminationHint
+import Lean.Elab.PreDefinition.TerminationHint
 import Lean.PrettyPrinter.Delaborator
 
 /-!
-This module contains the data type `TerminationArgument`, the elaborated form of a `TerminationBy`
-clause, the `TerminationArguments` type for a clique and the elaboration functions.
+This module contains
+* the data type `TerminationArgument`, the elaborated form of a `TerminationBy` clause,
+* the `TerminationArguments` type for a clique, and
+* elaboration and deelaboration functions.
 -/
 
 set_option autoImplicit false
 
-namespace Lean.Elab.WF
+namespace Lean.Elab
 
 open Lean Meta Elab Term
 
@@ -29,11 +31,12 @@ Elaborated form for a `termination_by` clause.
 The `fn` has the same (value) arity as the recursive functions (stored in
 `arity`), and maps its arguments (including fixed prefix, in unpacked form) to
 the termination argument.
+
+If `structural := Bool`, then the `fn` is a lambda picking out exactly one argument.
 -/
 structure TerminationArgument where
   ref : Syntax
-  arity : Nat
-  extraParams : Nat
+  structural : Bool
   fn : Expr
 deriving Inhabited
 
@@ -44,9 +47,6 @@ abbrev TerminationArguments := Array TerminationArgument
 Elaborates a `TerminationBy` to an `TerminationArgument`.
 
 * `type` is the full type of the original recursive function, including fixed prefix.
-* `arity` is the value arity of the recursive function; the termination argument cannot take more.
-* `extraParams` is the the number of parameters the function has after the colon; together with
-  `arity` indicates how many parameters of the function are before the colon and thus in scope.
 * `hint : TerminationBy` is the syntactic `TerminationBy`.
 -/
 def TerminationArgument.elab (funName : Name) (type : Expr) (arity extraParams : Nat)
@@ -69,22 +69,43 @@ def TerminationArgument.elab (funName : Name) (type : Expr) (arity extraParams :
       elabFunBinders hint.vars (some type') fun xs type' => do
         -- Elaborate the body in this local environment
         let body ← Lean.Elab.Term.withSynthesize <| elabTermEnsuringType hint.body none
+
+        -- Structural recursion: The body has to be a single parameter, whose index we return
+        if hint.structural then unless (ys ++ xs).contains body do
+          let params := MessageData.andList ((ys ++ xs).toList.map (m!"'{·}'"))
+          throwErrorAt hint.ref m!"The termination argument of a structurally recursive " ++
+            m!"function must be one of the parameters {params}, but{indentExpr body}\nisn't " ++
+            m!"one of these."
+
         -- Now abstract also over the remaining extra parameters
         forallBoundedTelescope type'.get! (extraParams - hint.vars.size) fun zs _ => do
           mkLambdaFVars (ys ++ xs ++ zs) body
-  -- logInfo m!"elabTermValue: {r}"
   check r
-  pure { ref := hint.ref, arity, extraParams, fn := r}
+  pure { ref := hint.ref, structural := hint.structural, fn := r}
   where
     parameters : Nat → MessageData
     | 1 => "one parameter"
     | n => m!"{n} parameters"
 
-open PrettyPrinter Delaborator SubExpr Parser.Termination Parser.Term in
-def TerminationArgument.delab (termArg : TerminationArgument) : MetaM (TSyntax ``terminationBy) := do
+def TerminationArgument.structuralArg (termArg : TerminationArgument) : MetaM Nat := do
+  assert! termArg.structural
   lambdaTelescope termArg.fn fun ys e => do
-    let e ← mkLambdaFVars ys[termArg.arity - termArg.extraParams:] e -- undo overshooting by lambdaTelescope
-    pure (← delabCore e (delab := go termArg.extraParams #[])).1
+    let .some idx := ys.indexOf? e
+      | panic! "TerminationArgument.structuralArg: body not one of the parameters"
+    return idx
+
+
+open PrettyPrinter Delaborator SubExpr Parser.Termination Parser.Term in
+/--
+Delaborates a `TerminationArgument` back to a `TerminationHint`, e.g. for `termination_by?`.
+
+This needs extra information:
+* `arity` is the value arity of the recursive function
+* `extraParams` indicates how many of the functions arguments are bound “after the colon”.
+-/
+def TerminationArgument.delab (arity : Nat) (extraParams : Nat) (termArg : TerminationArgument) : MetaM (TSyntax ``terminationBy) := do
+  lambdaBoundedTelescope termArg.fn (arity - extraParams) fun _ys e => do
+    pure (← delabCore e (delab := go extraParams #[])).1
   where
     go : Nat → TSyntaxArray `ident → DelabM (TSyntax ``terminationBy)
     | 0, vars => do
@@ -98,11 +119,19 @@ def TerminationArgument.delab (termArg : TerminationArgument) : MetaM (TSyntax `
       -- drop trailing underscores
       let mut vars := vars
       while ! vars.isEmpty && vars.back.raw.isOfKind ``hole do vars := vars.pop
-      if vars.isEmpty then
-        `(terminationBy|termination_by $stxBody)
+      if termArg.structural then
+        if vars.isEmpty then
+          `(terminationBy|termination_by structural $stxBody)
+        else
+          `(terminationBy|termination_by structural $vars* => $stxBody)
       else
-        `(terminationBy|termination_by $vars* => $stxBody)
+        if vars.isEmpty then
+          `(terminationBy|termination_by $stxBody)
+        else
+          `(terminationBy|termination_by $vars* => $stxBody)
     | i+1, vars => do
       let e ← getExpr
       unless e.isLambda do return ← go 0 vars -- should not happen
       withBindingBodyUnusedName fun n => go i (vars.push ⟨n⟩)
+
+end Lean.Elab

src/Lean/Elab/PreDefinition/TerminationHint.lean

@@ -8,22 +8,23 @@ import Lean.Parser.Term
 
 set_option autoImplicit false
 
-namespace Lean.Elab.WF
+namespace Lean.Elab
 
 /-! # Support for `termination_by` notation -/
 
 /-- A single `termination_by` clause -/
 structure TerminationBy where
-  ref       : Syntax
-  vars      : TSyntaxArray [`ident, ``Lean.Parser.Term.hole]
-  body      : Term
+  ref          : Syntax
+  structural : Bool
+  vars         : TSyntaxArray [`ident, ``Lean.Parser.Term.hole]
+  body         : Term
   /--
   If `synthetic := true`, then this `termination_by` clause was
   generated by `GuessLex`, and `vars` refers to *all* parameters
   of the function, not just the “extra parameters”.
   Cf. Lean.Elab.WF.unpackUnary
   -/
-  synthetic : Bool := false
+  synthetic    : Bool := false
   deriving Inhabited
 
 /-- A single `decreasing_by` clause -/
@@ -32,7 +33,8 @@ structure DecreasingBy where
   tactic    : TSyntax ``Lean.Parser.Tactic.tacticSeq
   deriving Inhabited
 
-/-- The termination annotations for a single function.
+/--
+The termination annotations for a single function.
 For `decreasing_by`, we store the whole `decreasing_by tacticSeq` expression, as this
 is what `Term.runTactic` expects.
  -/
@@ -41,7 +43,8 @@ structure TerminationHints where
   terminationBy?? : Option Syntax
   terminationBy? : Option TerminationBy
   decreasingBy?  : Option DecreasingBy
-  /-- Here we record the number of parameters past the `:`. It is set by
+  /--
+  Here we record the number of parameters past the `:`. It is set by
   `TerminationHints.rememberExtraParams` and used as folows:
 
   * When we guess the termination argument in `GuessLex` and want to print it in surface-syntax
@@ -55,7 +58,7 @@ structure TerminationHints where
 def TerminationHints.none : TerminationHints := ⟨.missing, .none, .none, .none, 0⟩
 
 /-- Logs warnings when the `TerminationHints` are present.  -/
-def TerminationHints.ensureNone (hints : TerminationHints) (reason : String): CoreM Unit := do
+def TerminationHints.ensureNone (hints : TerminationHints) (reason : String) : CoreM Unit := do
   match hints.terminationBy??, hints.terminationBy?, hints.decreasingBy? with
   | .none, .none, .none => pure ()
   | .none, .none, .some dec_by =>
@@ -114,10 +117,12 @@ def elabTerminationHints {m} [Monad m] [MonadError m] (stx : TSyntax ``suffix) :
       | _ => pure none
       else pure none
     let terminationBy? : Option TerminationBy ← if let some t := t? then match t with
-      | `(terminationBy|termination_by => $_body) =>
+      | `(terminationBy|termination_by $[structural%$s]? => $_body) =>
         throwErrorAt t "no extra parameters bounds, please omit the `=>`"
-      | `(terminationBy|termination_by $vars* => $body) => pure (some {ref := t, vars, body})
-      | `(terminationBy|termination_by $body:term) => pure (some {ref := t, vars := #[], body})
+      | `(terminationBy|termination_by $[structural%$s]? $vars* => $body) =>
+        pure (some {ref := t, structural := s.isSome, vars, body})
+      | `(terminationBy|termination_by $[structural%$s]? $body:term) =>
+        pure (some {ref := t, structural := s.isSome, vars := #[], body})
       | `(terminationBy?|termination_by?) => pure none
       | _ => throwErrorAt t "unexpected `termination_by` syntax"
       else pure none
@@ -127,4 +132,4 @@ def elabTerminationHints {m} [Monad m] [MonadError m] (stx : TSyntax ``suffix) :
     return { ref := stx, terminationBy??, terminationBy?, decreasingBy?, extraParams := 0 }
   | _ => throwErrorAt stx s!"Unexpected Termination.suffix syntax: {stx} of kind {stx.raw.getKind}"
 
-end Lean.Elab.WF
+end Lean.Elab

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

@@ -81,8 +81,8 @@ where
       | some matcherApp =>
         if let some matcherApp ← matcherApp.addArg? F then
           let altsNew ← (Array.zip matcherApp.alts matcherApp.altNumParams).mapM fun (alt, numParams) =>
-            lambdaTelescope alt fun xs altBody => do
-              unless xs.size >= numParams do
+            lambdaBoundedTelescope alt numParams fun xs altBody => do
+              unless xs.size = numParams do
                 throwError "unexpected matcher application alternative{indentExpr alt}\nat application{indentExpr e}"
               let FAlt := xs[numParams - 1]!
               mkLambdaFVars xs (← loop FAlt altBody)
@@ -103,12 +103,11 @@ private partial def processSumCasesOn (x F val : Expr) (k : (x : Expr) → (F :
       let type ← mkArrow (FDecl.type.replaceFVar x xs[0]!) type
       return (← mkLambdaFVars xs type, ← getLevel type)
     let mkMinorNew (ctorName : Name) (minor : Expr) : TermElabM Expr :=
-      lambdaTelescope minor fun xs body => do
+      lambdaBoundedTelescope minor 1 fun xs body => do
         let xNew := xs[0]!
-        let valNew ← mkLambdaFVars xs[1:] body
         let FTypeNew := FDecl.type.replaceFVar x (← mkAppOptM ctorName #[α, β, xNew])
         withLocalDeclD FDecl.userName FTypeNew fun FNew => do
-          mkLambdaFVars #[xNew, FNew] (← processSumCasesOn xNew FNew valNew k)
+          mkLambdaFVars #[xNew, FNew] (← processSumCasesOn xNew FNew body k)
     let minorLeft ← mkMinorNew ``PSum.inl args[4]!
     let minorRight ← mkMinorNew ``PSum.inr args[5]!
     let result := mkAppN (mkConst ``PSum.casesOn [u, (← getLevel α), (← getLevel β)]) #[α, β, motiveNew, x, minorLeft, minorRight, F]

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

@@ -14,7 +14,7 @@ import Lean.Elab.Quotation
 import Lean.Elab.RecAppSyntax
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Structural.Basic
-import Lean.Elab.PreDefinition.WF.TerminationArgument
+import Lean.Elab.PreDefinition.TerminationArgument
 import Lean.Data.Array
 
 
@@ -128,10 +128,10 @@ structure Measure extends TerminationArgument where
   natFn : Expr
 deriving Inhabited
 
-/-- String desription of this measure -/
+/-- String description of this measure -/
 def Measure.toString (measure : Measure) : MetaM String := do
-  lambdaTelescope measure.fn fun xs e => do
-    let e ← mkLambdaFVars xs[measure.arity:] e -- undo overshooting
+  lambdaTelescope measure.fn fun _xs e => do
+    -- This is a bit slopping if `measure.fn` takes more parameters than the `PreDefinition`
     return (← ppExpr e).pretty
 
 /--
@@ -187,8 +187,7 @@ def simpleMeasures (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)
             if  ← mayOmitSizeOf is_mutual xs[fixedPrefixSize:] x
             then mkLambdaFVars xs x
             else pure natFn
-          let extraParams := preDef.termination.extraParams
-          ret := ret.push { ref := .missing, fn, natFn, arity := xs.size, extraParams }
+          ret := ret.push { ref := .missing, structural := false, fn, natFn }
         return ret
 
 /-- Internal monad used by `withRecApps` -/
@@ -257,8 +256,7 @@ where
           matcherApp.discrs.forM (loop param)
           (Array.zip matcherApp.alts (Array.zip matcherApp.altNumParams altParams)).forM
             fun (alt, altNumParam, altParam) =>
-              lambdaTelescope altParam fun xs altParam => do
-                -- TODO: Use boundedLambdaTelescope
+              lambdaBoundedTelescope altParam altNumParam fun xs altParam => do
                 unless altNumParam = xs.size do
                   throwError "unexpected `casesOn` application alternative{indentExpr alt}\nat application{indentExpr e}"
                 let altBody := alt.beta xs
@@ -343,9 +341,8 @@ call site.
 def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat)
     (argsPacker : ArgsPacker) : MetaM (Array RecCallWithContext) := withoutModifyingState do
   addAsAxiom unaryPreDef
-  lambdaTelescope unaryPreDef.value fun xs body => do
+  lambdaBoundedTelescope unaryPreDef.value (fixedPrefixSize + 1) fun xs body => do
     unless xs.size == fixedPrefixSize + 1 do
-      -- Maybe cleaner to have lambdaBoundedTelescope?
       throwError "Unexpected number of lambdas in unary pre-definition"
     let ys := xs[:fixedPrefixSize]
     let param := xs[fixedPrefixSize]!
@@ -370,8 +367,7 @@ def isNatCmp (e : Expr) : Option (Expr × Expr) :=
 def complexMeasures (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)
     (userVarNamess : Array (Array Name)) (recCalls : Array RecCallWithContext) :
     MetaM (Array (Array Measure)) := do
-  preDefs.mapIdxM fun funIdx preDef => do
-    let arity ← lambdaTelescope preDef.value fun xs _ => pure xs.size
+  preDefs.mapIdxM fun funIdx _preDef => do
     let mut measures := #[]
     for rc in recCalls do
       -- Only look at calls from the current function
@@ -398,8 +394,7 @@ def complexMeasures (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)
               let fn ← mkLambdaFVars rc.params body
               -- Avoid duplicates
               unless ← measures.anyM (isDefEq ·.fn fn) do
-                let extraParams := preDef.termination.extraParams
-                measures := measures.push { ref := .missing, fn, natFn := fn, arity, extraParams }
+                measures := measures.push { ref := .missing, structural := false,  fn, natFn := fn }
         return measures
     return measures
 
@@ -751,18 +746,20 @@ def toTerminationArguments (preDefs : Array PreDefinition) (fixedPrefixSize : Na
           | .args taIdxs => measures[taIdxs[funIdx]!]!.fn.beta xs
           | .func funIdx' => mkNatLit <| if funIdx' == funIdx then 1 else 0
         let fn ← mkLambdaFVars xs (← mkProdElem args)
-        let extraParams := preDef.termination.extraParams
-        return { ref := .missing, arity := xs.size, extraParams, fn}
+        return { ref := .missing, structural := false, fn}
 
 /--
 Shows the inferred termination argument to the user, and implements `termination_by?`
 -/
 def reportTermArgs (preDefs : Array PreDefinition) (termArgs : TerminationArguments) : MetaM Unit := do
   for preDef in preDefs, termArg in termArgs do
+    let stx := do
+      let arity ← lambdaTelescope preDef.value fun xs _ => pure xs.size
+      termArg.delab arity (extraParams := preDef.termination.extraParams)
     if showInferredTerminationBy.get (← getOptions) then
-      logInfoAt preDef.ref m!"Inferred termination argument:\n{← termArg.delab}"
+      logInfoAt preDef.ref m!"Inferred termination argument:\n{← stx}"
     if let some ref := preDef.termination.terminationBy?? then
-      Tactic.TryThis.addSuggestion ref (← termArg.delab)
+      Tactic.TryThis.addSuggestion ref (← stx)
 
 end GuessLex
 open GuessLex

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

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Elab.PreDefinition.Basic
-import Lean.Elab.PreDefinition.WF.TerminationArgument
+import Lean.Elab.PreDefinition.TerminationArgument
 import Lean.Elab.PreDefinition.WF.PackMutual
 import Lean.Elab.PreDefinition.WF.Preprocess
 import Lean.Elab.PreDefinition.WF.Rel
@@ -86,7 +86,7 @@ def varyingVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Ar
     let xs : Array Expr := xs[fixedPrefixSize:]
     xs.mapM (·.fvarId!.getUserName)
 
-def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
+def wfRecursion (preDefs : Array PreDefinition) (termArgs? : Option TerminationArguments) : TermElabM Unit := do
   let preDefs ← preDefs.mapM fun preDef =>
     return { preDef with value := (← preprocess preDef.value) }
   let (fixedPrefixSize, argsPacker, unaryPreDef) ← withoutModifyingEnv do
@@ -100,21 +100,9 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
     return (fixedPrefixSize, argsPacker, ← packMutual fixedPrefixSize argsPacker preDefsDIte)
 
   let wf : TerminationArguments ← do
-    let (preDefsWith, preDefsWithout) := preDefs.partition (·.termination.terminationBy?.isSome)
-    if preDefsWith.isEmpty then
-      -- No termination_by anywhere, so guess one
-      guessLex preDefs unaryPreDef fixedPrefixSize argsPacker
-    else if preDefsWithout.isEmpty then
-      preDefsWith.mapIdxM fun funIdx predef => do
-        let arity := fixedPrefixSize + argsPacker.varNamess[funIdx]!.size
-        let hints := predef.termination
-        TerminationArgument.elab predef.declName predef.type arity hints.extraParams hints.terminationBy?.get!
-    else
-      -- Some have, some do not, so report errors
-      preDefsWithout.forM fun preDef => do
-        logErrorAt preDef.ref (m!"Missing `termination_by`; this function is mutually " ++
-          m!"recursive with {preDefsWith[0]!.declName}, which has a `termination_by` clause.")
-      return
+    if let some tas := termArgs? then pure tas else
+    -- No termination_by here, so use GuessLex to infer one
+    guessLex preDefs unaryPreDef fixedPrefixSize argsPacker
 
   let preDefNonRec ← forallBoundedTelescope unaryPreDef.type fixedPrefixSize fun prefixArgs type => do
     let type ← whnfForall type

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

@@ -9,7 +9,7 @@ import Lean.Meta.Tactic.Cases
 import Lean.Meta.Tactic.Rename
 import Lean.Elab.SyntheticMVars
 import Lean.Elab.PreDefinition.Basic
-import Lean.Elab.PreDefinition.WF.TerminationArgument
+import Lean.Elab.PreDefinition.TerminationArgument
 import Lean.Meta.ArgsPacker
 
 namespace Lean.Elab.WF

src/Lean/Elab/Tactic/Basic.lean

@@ -96,14 +96,15 @@ def SavedState.restore (b : SavedState) (restoreInfo := false) : TacticM Unit :=
   b.term.restore restoreInfo
   set b.tactic
 
-@[specialize, inherit_doc Core.withRestoreOrSaveFull]
-def withRestoreOrSaveFull (reusableResult? : Option (α × SavedState)) (act : TacticM α) :
+@[specialize, inherit_doc Term.withRestoreOrSaveFull]
+def withRestoreOrSaveFull (reusableResult? : Option (α × SavedState))
+    (tacSnap? : Option (Language.SnapshotBundle Tactic.TacticParsedSnapshot)) (act : TacticM α) :
     TacticM (α × SavedState) := do
   if let some (_, state) := reusableResult? then
     set state.tactic
   let reusableResult? := reusableResult?.map (fun (val, state) => (val, state.term))
   let (a, term) ← controlAt TermElabM fun runInBase => do
-    Term.withRestoreOrSaveFull reusableResult? <| runInBase act
+    Term.withRestoreOrSaveFull reusableResult? tacSnap? <| runInBase act
   return (a, { term, tactic := (← get) })
 
 protected def getCurrMacroScope : TacticM MacroScope := do pure (← readThe Core.Context).currMacroScope

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -90,11 +90,10 @@ where
               {
                 range? := stxs |>.getRange?
                 task := next.result }]
-            let (_, state) ← withRestoreOrSaveFull reusableResult? do
-              -- set up nested reuse; `evalTactic` will check for `isIncrementalElab`
-              withTheReader Term.Context ({ · with
-                  tacSnap? := some { old? := oldInner?, new := inner } }) do
-                evalTactic tac
+            let (_, state) ← withRestoreOrSaveFull reusableResult?
+                -- set up nested reuse; `evalTactic` will check for `isIncrementalElab`
+                (tacSnap? := some { old? := oldInner?, new := inner }) do
+              evalTactic tac
             finished.resolve { state? := state }
 
         withTheReader Term.Context ({ · with tacSnap? := some {

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

@@ -578,9 +578,14 @@ where
         names := names.push "(masked)"
     return names
 
+  -- We sort the constraints; otherwise the order is dependent on details of the hashing
+  -- and this can cause test suite output churn
   prettyConstraints (names : Array String) (constraints : HashMap Coeffs Fact) : String :=
     constraints.toList
+      |>.toArray
+      |>.qsort (·.1 < ·.1)
       |>.map (fun ⟨coeffs, ⟨_, cst, _⟩⟩ => "  " ++ prettyConstraint (prettyCoeffs names coeffs) cst)
+      |>.toList
       |> "\n".intercalate
 
   prettyConstraint (e : String) : Constraint → String

src/Lean/Elab/Tactic/Simp.lean

@@ -347,7 +347,7 @@ def mkSimpOnly (stx : Syntax) (usedSimps : Simp.UsedSimps) : MetaM Syntax := do
       if env.contains declName
          && (inv || !simpOnlyBuiltins.contains declName)
          && !Match.isMatchEqnTheorem env declName then
-        let decl : Term ← `($(mkIdent (← unresolveNameGlobal declName)):ident)
+        let decl : Term ← `($(mkIdent (← unresolveNameGlobalAvoidingLocals declName)):ident)
         let arg ← match post, inv with
           | true,  true  => `(Parser.Tactic.simpLemma| ← $decl:term)
           | true,  false => `(Parser.Tactic.simpLemma| $decl:term)

src/Lean/Elab/Term.lean

@@ -12,7 +12,7 @@ import Lean.Linter.Deprecated
 import Lean.Elab.Config
 import Lean.Elab.Level
 import Lean.Elab.DeclModifiers
-import Lean.Elab.PreDefinition.WF.TerminationHint
+import Lean.Elab.PreDefinition.TerminationHint
 import Lean.Language.Basic
 
 namespace Lean.Elab
@@ -108,7 +108,7 @@ structure LetRecToLift where
   type           : Expr
   val            : Expr
   mvarId         : MVarId
-  termination    : WF.TerminationHints
+  termination    : TerminationHints
   deriving Inhabited
 
 /--
@@ -327,14 +327,33 @@ def SavedState.restore (s : SavedState) (restoreInfo : Bool := false) : TermElab
   unless restoreInfo do
     setInfoState infoState
 
-@[specialize, inherit_doc Core.withRestoreOrSaveFull]
-def withRestoreOrSaveFull (reusableResult? : Option (α × SavedState)) (act : TermElabM α) :
+/--
+Like `Meta.withRestoreOrSaveFull` for `TermElabM`, but also takes a `tacSnap?` that
+* when running `act`, is set as `Context.tacSnap?`
+* otherwise (i.e. on restore) is used to update the new snapshot promise to the old task's
+  value.
+This extra restore step is necessary because while `reusableResult?` can be used to replay any
+effects on `State`, `Context.tacSnap?` is not part of it but changed via an `IO` side effect, so
+it needs to be replayed separately.
+
+We use an explicit parameter instead of accessing `Context.tacSnap?` directly because this prevents
+`withRestoreOrSaveFull` and `withReader` from being used in the wrong order.
+-/
+@[specialize]
+def withRestoreOrSaveFull (reusableResult? : Option (α × SavedState))
+    (tacSnap? : Option (Language.SnapshotBundle Tactic.TacticParsedSnapshot)) (act : TermElabM α) :
     TermElabM (α × SavedState) := do
   if let some (_, state) := reusableResult? then
     set state.elab
+    if let some snap := tacSnap? then
+      let some old := snap.old?
+        | throwError "withRestoreOrSaveFull: expected old snapshot in `tacSnap?`"
+      snap.new.resolve old.val.get
+
   let reusableResult? := reusableResult?.map (fun (val, state) => (val, state.meta))
-  let (a, meta) ← controlAt MetaM fun runInBase => do
-    Meta.withRestoreOrSaveFull reusableResult? <| runInBase act
+  let (a, meta) ← withReader ({ · with tacSnap? }) do
+    controlAt MetaM fun runInBase => do
+      Meta.withRestoreOrSaveFull reusableResult? <| runInBase act
   return (a, { meta, «elab» := (← get) })
 
 instance : MonadBacktrack SavedState TermElabM where

src/Lean/Environment.lean

@@ -244,9 +244,21 @@ inductive KernelException where
 
 namespace Environment
 
-/-- Type check given declaration and add it to the environment -/
+/--
+Type check given declaration and add it to the environment
+-/
 @[extern "lean_add_decl"]
-opaque addDeclCore (env : Environment) (maxHeartbeats : USize) (decl : @& Declaration) : Except KernelException Environment
+opaque addDeclCore (env : Environment) (maxHeartbeats : USize) (decl : @& Declaration)
+  (cancelTk? : @& Option IO.CancelToken) : Except KernelException Environment
+
+/--
+Add declaration to kernel without type checking it.
+**WARNING** This function is meant for temporarily working around kernel performance issues.
+It compromises soundness because, for example, a buggy tactic may produce an invalid proof,
+and the kernel will not catch it if the new option is set to true.
+-/
+@[extern "lean_add_decl_without_checking"]
+opaque addDeclWithoutChecking (env : Environment) (decl : @& Declaration) : Except KernelException Environment
 
 end Environment
 

src/Lean/Message.lean

@@ -256,6 +256,15 @@ def ofList : List MessageData → MessageData
 def ofArray (msgs : Array MessageData) : MessageData :=
   ofList msgs.toList
 
+/-- Puts `MessageData` into a comma-separated list with `"and"` at the back (no Oxford comma).
+Best used on non-empty lists; returns `"– none –"` for an empty list.  -/
+def andList (xs : List MessageData) : MessageData :=
+  match xs with
+  | [] => "– none –"
+  | [x] => x
+  | _ => joinSep xs.dropLast ", " ++ " and " ++ xs.getLast!
+
+
 instance : Coe (List MessageData) MessageData := ⟨ofList⟩
 instance : Coe (List Expr) MessageData := ⟨fun es => ofList <| es.map ofExpr⟩
 
@@ -350,13 +359,20 @@ structure MessageLog where
   hadErrors : Bool := false
   /-- The list of messages not already reported, in insertion order. -/
   unreported : PersistentArray Message := {}
+  /--
+  Set of message kinds that have been added to the log.
+  For example, we have the kind `unsafe.exponentiation.warning` for warning messages associated with
+  the configuration option `exponentiation.threshold`.
+  We don't produce a warning if the kind is already in the following set.
+  -/
+  reportedKinds : NameSet := {}
   deriving Inhabited
 
 namespace MessageLog
 def empty : MessageLog := {}
 
 @[deprecated "renamed to `unreported`; direct access should in general be avoided in favor of \
-using `MessageLog.toList/toArray`"]
+using `MessageLog.toList/toArray`" (since := "2024-05-22")]
 def msgs : MessageLog → PersistentArray Message := unreported
 
 def hasUnreported (log : MessageLog) : Bool :=
@@ -403,7 +419,7 @@ def indentExpr (e : Expr) : MessageData :=
   indentD e
 
 class AddMessageContext (m : Type → Type) where
-  /-- 
+  /--
   Without context, a `MessageData` object may be be missing information
   (e.g. hover info) for pretty printing, or may print an error. Hence,
   `addMessageContext` should be called on all constructed `MessageData`

src/Lean/Meta/Basic.lean

@@ -664,10 +664,6 @@ Return `none` if `mvarId` has no declaration in the current metavariable context
 def _root_.Lean.MVarId.findDecl? (mvarId : MVarId) : MetaM (Option MetavarDecl) :=
   return (← getMCtx).findDecl? mvarId
 
-@[deprecated MVarId.findDecl? (since := "2022-07-15")]
-def findMVarDecl? (mvarId : MVarId) : MetaM (Option MetavarDecl) :=
-  mvarId.findDecl?
-
 /--
 Return `mvarId` declaration in the current metavariable context.
 Throw an exception if `mvarId` is not declared in the current metavariable context.
@@ -677,20 +673,12 @@ def _root_.Lean.MVarId.getDecl (mvarId : MVarId) : MetaM MetavarDecl := do
   | some d => pure d
   | none   => throwError "unknown metavariable '?{mvarId.name}'"
 
-@[deprecated MVarId.getDecl (since := "2022-07-15")]
-def getMVarDecl (mvarId : MVarId) : MetaM MetavarDecl := do
-  mvarId.getDecl
-
 /--
 Return `mvarId` kind. Throw an exception if `mvarId` is not declared in the current metavariable context.
 -/
 def _root_.Lean.MVarId.getKind (mvarId : MVarId) : MetaM MetavarKind :=
   return (← mvarId.getDecl).kind
 
-@[deprecated MVarId.getKind (since := "2022-07-15")]
-def getMVarDeclKind (mvarId : MVarId) : MetaM MetavarKind :=
-  mvarId.getKind
-
 /-- Return `true` if `e` is a synthetic (or synthetic opaque) metavariable -/
 def isSyntheticMVar (e : Expr) : MetaM Bool := do
   if e.isMVar then
@@ -704,19 +692,11 @@ Set `mvarId` kind in the current metavariable context.
 def _root_.Lean.MVarId.setKind (mvarId : MVarId) (kind : MetavarKind) : MetaM Unit :=
   modifyMCtx fun mctx => mctx.setMVarKind mvarId kind
 
-@[deprecated MVarId.setKind (since := "2022-07-15")]
-def setMVarKind (mvarId : MVarId) (kind : MetavarKind) : MetaM Unit :=
-  mvarId.setKind kind
-
 /-- Update the type of the given metavariable. This function assumes the new type is
    definitionally equal to the current one -/
 def _root_.Lean.MVarId.setType (mvarId : MVarId) (type : Expr) : MetaM Unit := do
   modifyMCtx fun mctx => mctx.setMVarType mvarId type
 
-@[deprecated MVarId.setType (since := "2022-07-15")]
-def setMVarType (mvarId : MVarId) (type : Expr) : MetaM Unit := do
-  mvarId.setType type
-
 /--
 Return true if the given metavariable is "read-only".
 That is, its `depth` is different from the current metavariable context depth.
@@ -724,10 +704,6 @@ That is, its `depth` is different from the current metavariable context depth.
 def _root_.Lean.MVarId.isReadOnly (mvarId : MVarId) : MetaM Bool := do
   return (← mvarId.getDecl).depth != (← getMCtx).depth
 
-@[deprecated MVarId.isReadOnly (since := "2022-07-15")]
-def isReadOnlyExprMVar (mvarId : MVarId) : MetaM Bool := do
-  mvarId.isReadOnly
-
 /--
 Returns true if `mvarId.isReadOnly` returns true or if `mvarId` is a synthetic opaque metavariable.
 
@@ -742,10 +718,6 @@ def _root_.Lean.MVarId.isReadOnlyOrSyntheticOpaque (mvarId : MVarId) : MetaM Boo
     | MetavarKind.syntheticOpaque => return !(← getConfig).assignSyntheticOpaque
     | _ => return false
 
-@[deprecated MVarId.isReadOnlyOrSyntheticOpaque (since := "2022-07-15")]
-def isReadOnlyOrSyntheticOpaqueExprMVar (mvarId : MVarId) : MetaM Bool := do
-  mvarId.isReadOnlyOrSyntheticOpaque
-
 /--
 Return the level of the given universe level metavariable.
 -/
@@ -754,10 +726,6 @@ def _root_.Lean.LMVarId.getLevel (mvarId : LMVarId) : MetaM Nat := do
   | some depth => return depth
   | _          => throwError "unknown universe metavariable '?{mvarId.name}'"
 
-@[deprecated LMVarId.getLevel (since := "2022-07-15")]
-def getLevelMVarDepth (mvarId : LMVarId) : MetaM Nat :=
-  mvarId.getLevel
-
 /--
 Return true if the given universe metavariable is "read-only".
 That is, its `depth` is different from the current metavariable context depth.
@@ -765,40 +733,24 @@ That is, its `depth` is different from the current metavariable context depth.
 def _root_.Lean.LMVarId.isReadOnly (mvarId : LMVarId) : MetaM Bool :=
   return (← mvarId.getLevel) < (← getMCtx).levelAssignDepth
 
-@[deprecated LMVarId.isReadOnly (since := "2022-07-15")]
-def isReadOnlyLevelMVar (mvarId : LMVarId) : MetaM Bool := do
-  mvarId.isReadOnly
-
 /--
 Set the user-facing name for the given metavariable.
 -/
 def _root_.Lean.MVarId.setUserName (mvarId : MVarId) (newUserName : Name) : MetaM Unit :=
   modifyMCtx fun mctx => mctx.setMVarUserName mvarId newUserName
 
-@[deprecated MVarId.setUserName (since := "2022-07-15")]
-def setMVarUserName (mvarId : MVarId) (userNameNew : Name) : MetaM Unit :=
-  mvarId.setUserName userNameNew
-
 /--
 Throw an exception saying `fvarId` is not declared in the current local context.
 -/
 def _root_.Lean.FVarId.throwUnknown (fvarId : FVarId) : CoreM α :=
   throwError "unknown free variable '{mkFVar fvarId}'"
 
-@[deprecated FVarId.throwUnknown (since := "2022-07-15")]
-def throwUnknownFVar (fvarId : FVarId) : MetaM α :=
-  fvarId.throwUnknown
-
 /--
 Return `some decl` if `fvarId` is declared in the current local context.
 -/
 def _root_.Lean.FVarId.findDecl? (fvarId : FVarId) : MetaM (Option LocalDecl) :=
   return (← getLCtx).find? fvarId
 
-@[deprecated FVarId.findDecl? (since := "2022-07-15")]
-def findLocalDecl? (fvarId : FVarId) : MetaM (Option LocalDecl) :=
-  fvarId.findDecl?
-
 /--
   Return the local declaration for the given free variable.
   Throw an exception if local declaration is not in the current local context.
@@ -808,10 +760,6 @@ def _root_.Lean.FVarId.getDecl (fvarId : FVarId) : MetaM LocalDecl := do
   | some d => return d
   | none   => fvarId.throwUnknown
 
-@[deprecated FVarId.getDecl (since := "2022-07-15")]
-def getLocalDecl (fvarId : FVarId) : MetaM LocalDecl := do
-  fvarId.getDecl
-
 /-- Return the type of the given free variable. -/
 def _root_.Lean.FVarId.getType (fvarId : FVarId) : MetaM Expr :=
   return (← fvarId.getDecl).type
@@ -886,10 +834,6 @@ contain a metavariable `?m` s.t. local context of `?m` contains a free variable
 def _root_.Lean.Expr.abstractRangeM (e : Expr) (n : Nat) (xs : Array Expr) : MetaM Expr :=
   liftMkBindingM <| MetavarContext.abstractRange e n xs
 
-@[deprecated Expr.abstractRangeM (since := "2022-07-15")]
-def abstractRange (e : Expr) (n : Nat) (xs : Array Expr) : MetaM Expr :=
-  e.abstractRangeM n xs
-
 /--
 Replace free (or meta) variables `xs` with loose bound variables.
 Similar to `Expr.abstract`, but handles metavariables correctly.
@@ -897,10 +841,6 @@ Similar to `Expr.abstract`, but handles metavariables correctly.
 def _root_.Lean.Expr.abstractM (e : Expr) (xs : Array Expr) : MetaM Expr :=
   e.abstractRangeM xs.size xs
 
-@[deprecated Expr.abstractM (since := "2022-07-15")]
-def abstract (e : Expr) (xs : Array Expr) : MetaM Expr :=
-  e.abstractM xs
-
 /--
 Collect forward dependencies for the free variables in `toRevert`.
 Recall that when reverting free variables `xs`, we must also revert their forward dependencies.
@@ -1261,30 +1201,31 @@ private def forallBoundedTelescopeImp (type : Expr) (maxFVars? : Option Nat) (k
 def forallBoundedTelescope (type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → n α) (cleanupAnnotations := false) : n α :=
   map2MetaM (fun k => forallBoundedTelescopeImp type maxFVars? k cleanupAnnotations) k
 
-private partial def lambdaTelescopeImp (e : Expr) (consumeLet : Bool) (k : Array Expr → Expr → MetaM α) (cleanupAnnotations := false) : MetaM α := do
-  process consumeLet (← getLCtx) #[] 0 e
+private partial def lambdaTelescopeImp (e : Expr) (consumeLet : Bool) (maxFVars? : Option Nat)
+    (k : Array Expr → Expr → MetaM α) (cleanupAnnotations := false) : MetaM α := do
+  process consumeLet (← getLCtx) #[] e
 where
-  process (consumeLet : Bool) (lctx : LocalContext) (fvars : Array Expr) (j : Nat) (e : Expr) : MetaM α := do
-    match consumeLet, e with
-    | _, .lam n d b bi =>
-      let d := d.instantiateRevRange j fvars.size fvars
+  process (consumeLet : Bool) (lctx : LocalContext) (fvars : Array Expr) (e : Expr) : MetaM α := do
+    match fvarsSizeLtMaxFVars fvars maxFVars?, consumeLet, e with
+    | true, _, .lam n d b bi =>
+      let d := d.instantiateRevRange 0 fvars.size fvars
       let d := if cleanupAnnotations then d.cleanupAnnotations else d
       let fvarId ← mkFreshFVarId
       let lctx := lctx.mkLocalDecl fvarId n d bi
       let fvar := mkFVar fvarId
-      process consumeLet lctx (fvars.push fvar) j b
-    | true, .letE n t v b _ => do
-      let t := t.instantiateRevRange j fvars.size fvars
+      process consumeLet lctx (fvars.push fvar) b
+    | true, true, .letE n t v b _ => do
+      let t := t.instantiateRevRange 0 fvars.size fvars
       let t := if cleanupAnnotations then t.cleanupAnnotations else t
-      let v := v.instantiateRevRange j fvars.size fvars
+      let v := v.instantiateRevRange 0 fvars.size fvars
       let fvarId ← mkFreshFVarId
       let lctx := lctx.mkLetDecl fvarId n t v
       let fvar := mkFVar fvarId
-      process true lctx (fvars.push fvar) j b
-    | _, e =>
-      let e := e.instantiateRevRange j fvars.size fvars
+      process true lctx (fvars.push fvar) b
+    | _, _, e =>
+      let e := e.instantiateRevRange 0 fvars.size fvars
       withReader (fun ctx => { ctx with lctx := lctx }) do
-        withNewLocalInstancesImp fvars j do
+        withNewLocalInstancesImp fvars 0 do
           k fvars e
 
 /--
@@ -1293,7 +1234,7 @@ Similar to `lambdaTelescope` but for lambda and let expressions.
 If `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope.
 -/
 def lambdaLetTelescope (e : Expr) (k : Array Expr → Expr → n α) (cleanupAnnotations := false) : n α :=
-  map2MetaM (fun k => lambdaTelescopeImp e true k (cleanupAnnotations := cleanupAnnotations)) k
+  map2MetaM (fun k => lambdaTelescopeImp e true .none k (cleanupAnnotations := cleanupAnnotations)) k
 
 /--
   Given `e` of the form `fun ..xs => A`, execute `k xs A`.
@@ -1303,7 +1244,18 @@ def lambdaLetTelescope (e : Expr) (k : Array Expr → Expr → n α) (cleanupAnn
   If `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope.
 -/
 def lambdaTelescope (e : Expr) (k : Array Expr → Expr → n α) (cleanupAnnotations := false) : n α :=
-  map2MetaM (fun k => lambdaTelescopeImp e false k (cleanupAnnotations := cleanupAnnotations)) k
+  map2MetaM (fun k => lambdaTelescopeImp e false none k (cleanupAnnotations := cleanupAnnotations)) k
+
+/--
+  Given `e` of the form `fun ..xs ..ys => A`, execute `k xs (fun ..ys => A)` where
+  `xs.size ≤ maxFVars`.
+  This combinator will declare local declarations, create free variables for them,
+  execute `k` with updated local context, and make sure the cache is restored after executing `k`.
+
+  If `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope.
+-/
+def lambdaBoundedTelescope (e : Expr) (maxFVars : Nat) (k : Array Expr → Expr → n α) (cleanupAnnotations := false) : n α :=
+  map2MetaM (fun k => lambdaTelescopeImp e false (.some maxFVars) k (cleanupAnnotations := cleanupAnnotations)) k
 
 /-- Return the parameter names for the given global declaration. -/
 def getParamNames (declName : Name) : MetaM (Array Name) := do
@@ -1551,10 +1503,6 @@ private def withMVarContextImp (mvarId : MVarId) (x : MetaM α) : MetaM α := do
 def _root_.Lean.MVarId.withContext (mvarId : MVarId) : n α → n α :=
   mapMetaM <| withMVarContextImp mvarId
 
-@[deprecated MVarId.withContext (since := "2022-07-15")]
-def withMVarContext (mvarId : MVarId) : n α → n α :=
-  mvarId.withContext
-
 private def withMCtxImp (mctx : MetavarContext) (x : MetaM α) : MetaM α := do
   let mctx' ← getMCtx
   setMCtx mctx

src/Lean/Meta/Constructions.lean

@@ -4,183 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.AuxRecursor
-import Lean.AddDecl
-import Lean.Meta.AppBuilder
-import Lean.Meta.CompletionName
+import Lean.Meta.Constructions.CasesOn
+import Lean.Meta.Constructions.NoConfusion
 import Lean.Meta.Constructions.RecOn
-
-namespace Lean
-
-@[extern "lean_mk_cases_on"] opaque mkCasesOnImp (env : Environment) (declName : @& Name) : Except KernelException Declaration
-@[extern "lean_mk_no_confusion_type"] opaque mkNoConfusionTypeCoreImp (env : Environment) (declName : @& Name) : Except KernelException Declaration
-@[extern "lean_mk_no_confusion"] opaque mkNoConfusionCoreImp (env : Environment) (declName : @& Name) : Except KernelException Declaration
-@[extern "lean_mk_below"] opaque mkBelowImp (env : Environment) (declName : @& Name) (ibelow : Bool) : Except KernelException Declaration
-@[extern "lean_mk_brec_on"] opaque mkBRecOnImp (env : Environment) (declName : @& Name) (ind : Bool) : Except KernelException Declaration
-
-open Meta
-
-def mkCasesOn (declName : Name) : MetaM Unit := do
-  let name := mkCasesOnName declName
-  let decl ← ofExceptKernelException (mkCasesOnImp (← getEnv) declName)
-  addDecl decl
-  setReducibleAttribute name
-  modifyEnv fun env => markAuxRecursor env name
-  modifyEnv fun env => addProtected env name
-
-private def mkBelowOrIBelow (declName : Name) (ibelow : Bool) : MetaM Unit := do
-  let .inductInfo indVal ← getConstInfo declName | return
-  unless indVal.isRec do return
-  if ← isPropFormerType indVal.type then return
-
-  let decl ← ofExceptKernelException (mkBelowImp (← getEnv) declName ibelow)
-  let name := decl.definitionVal!.name
-  addDecl decl
-  setReducibleAttribute name
-  modifyEnv fun env => addToCompletionBlackList env name
-  modifyEnv fun env => addProtected env name
-
-def mkBelow (declName : Name) : MetaM Unit := mkBelowOrIBelow declName true
-def mkIBelow (declName : Name) : MetaM Unit := mkBelowOrIBelow declName false
-
-private def mkBRecOrBInductionOn (declName : Name) (ind : Bool) : MetaM Unit := do
-  let .inductInfo indVal ← getConstInfo declName | return
-  unless indVal.isRec do return
-  if ← isPropFormerType indVal.type then return
-  let .recInfo recInfo ← getConstInfo (mkRecName declName) | return
-  unless recInfo.numMotives = indVal.all.length do
-    /-
-    The mutual declaration containing `declName` contains nested inductive datatypes.
-    We don't support this kind of declaration here yet. We probably never will :)
-    To support it, we will need to generate an auxiliary `below` for each nested inductive
-    type since their default `below` is not good here. For example, at
-    ```
-    inductive Term
-    | var : String -> Term
-    | app : String -> List Term -> Term
-    ```
-    The `List.below` is not useful since it will not allow us to recurse over the nested terms.
-    We need to generate another one using the auxiliary recursor `Term.rec_1` for `List Term`.
-    -/
-    return
-
-  let decl ← ofExceptKernelException (mkBRecOnImp (← getEnv) declName ind)
-  let name := decl.definitionVal!.name
-  addDecl decl
-  setReducibleAttribute name
-  modifyEnv fun env => markAuxRecursor env name
-  modifyEnv fun env => addProtected env name
-
-def mkBRecOn (declName : Name) : MetaM Unit := mkBRecOrBInductionOn declName false
-def mkBInductionOn (declName : Name) : MetaM Unit := mkBRecOrBInductionOn declName true
-
-def mkNoConfusionCore (declName : Name) : MetaM Unit := do
-  -- Do not do anything unless can_elim_to_type. TODO: Extract to util
-  let .inductInfo indVal ← getConstInfo declName | return
-  let recInfo ← getConstInfo (mkRecName declName)
-  unless recInfo.levelParams.length > indVal.levelParams.length do return
-
-  let name := Name.mkStr declName "noConfusionType"
-  let decl ← ofExceptKernelException (mkNoConfusionTypeCoreImp (← getEnv) declName)
-  addDecl decl
-  setReducibleAttribute name
-  modifyEnv fun env => addToCompletionBlackList env name
-  modifyEnv fun env => addProtected env name
-
-  let name := Name.mkStr declName "noConfusion"
-  let decl ← ofExceptKernelException (mkNoConfusionCoreImp (← getEnv) declName)
-  addDecl decl
-  setReducibleAttribute name
-  modifyEnv fun env => markNoConfusion env name
-  modifyEnv fun env => addProtected env name
-
-def mkNoConfusionEnum (enumName : Name) : MetaM Unit := do
-  if (← getEnv).contains ``noConfusionEnum then
-    mkToCtorIdx
-    mkNoConfusionType
-    mkNoConfusion
-  else
-    -- `noConfusionEnum` was not defined yet, so we use `mkNoConfusionCore`
-    mkNoConfusionCore enumName
-where
-
-  mkToCtorIdx : MetaM Unit := do
-    let ConstantInfo.inductInfo info ← getConstInfo enumName | unreachable!
-    let us := info.levelParams.map mkLevelParam
-    let numCtors := info.ctors.length
-    let declName := Name.mkStr enumName "toCtorIdx"
-    let enumType := mkConst enumName us
-    let natType  := mkConst ``Nat
-    let declType ← mkArrow enumType natType
-    let mut minors := #[]
-    for i in [:numCtors] do
-      minors := minors.push <| mkNatLit i
-    withLocalDeclD `x enumType fun x => do
-      let motive ← mkLambdaFVars #[x] natType
-      let declValue ← mkLambdaFVars #[x] <| mkAppN (mkApp2 (mkConst (mkCasesOnName enumName) (levelOne::us)) motive x) minors
-      addAndCompile <| Declaration.defnDecl {
-        name        := declName
-        levelParams := info.levelParams
-        type        := declType
-        value       := declValue
-        safety      := DefinitionSafety.safe
-        hints       := ReducibilityHints.abbrev
-      }
-      setReducibleAttribute declName
-
-  mkNoConfusionType : MetaM Unit := do
-    let ConstantInfo.inductInfo info ← getConstInfo enumName | unreachable!
-    let us := info.levelParams.map mkLevelParam
-    let v ← mkFreshUserName `v
-    let enumType := mkConst enumName us
-    let sortV := mkSort (mkLevelParam v)
-    let toCtorIdx := mkConst (Name.mkStr enumName "toCtorIdx") us
-    withLocalDeclD `P sortV fun P =>
-    withLocalDeclD `x enumType fun x =>
-    withLocalDeclD `y enumType fun y => do
-      let declType  ← mkForallFVars #[P, x, y] sortV
-      let declValue ← mkLambdaFVars #[P, x, y] (← mkAppM ``noConfusionTypeEnum #[toCtorIdx, P, x, y])
-      let declName  := Name.mkStr enumName "noConfusionType"
-      addAndCompile <| Declaration.defnDecl {
-        name        := declName
-        levelParams := v :: info.levelParams
-        type        := declType
-        value       := declValue
-        safety      := DefinitionSafety.safe
-        hints       := ReducibilityHints.abbrev
-      }
-      setReducibleAttribute declName
-
-  mkNoConfusion : MetaM Unit := do
-    let ConstantInfo.inductInfo info ← getConstInfo enumName | unreachable!
-    let us := info.levelParams.map mkLevelParam
-    let v ← mkFreshUserName `v
-    let enumType := mkConst enumName us
-    let sortV := mkSort (mkLevelParam v)
-    let toCtorIdx := mkConst (Name.mkStr enumName "toCtorIdx") us
-    let noConfusionType := mkConst (Name.mkStr enumName "noConfusionType") (mkLevelParam v :: us)
-    withLocalDecl `P BinderInfo.implicit sortV fun P =>
-    withLocalDecl `x BinderInfo.implicit enumType fun x =>
-    withLocalDecl `y BinderInfo.implicit enumType fun y => do
-    withLocalDeclD `h (← mkEq x y) fun h => do
-      let declType  ← mkForallFVars #[P, x, y, h] (mkApp3 noConfusionType P x y)
-      let declValue ← mkLambdaFVars #[P, x, y, h] (← mkAppOptM ``noConfusionEnum #[none, none, none, toCtorIdx, P, x, y, h])
-      let declName  := Name.mkStr enumName "noConfusion"
-      addAndCompile <| Declaration.defnDecl {
-        name        := declName
-        levelParams := v :: info.levelParams
-        type        := declType
-        value       := declValue
-        safety      := DefinitionSafety.safe
-        hints       := ReducibilityHints.abbrev
-      }
-      setReducibleAttribute declName
-      modifyEnv fun env => markNoConfusion env declName
-
-def mkNoConfusion (declName : Name) : MetaM Unit := do
-  if (← isEnumType declName) then
-    mkNoConfusionEnum declName
-  else
-    mkNoConfusionCore declName
-
-end Lean
+import Lean.Meta.Constructions.BRecOn

src/Lean/Meta/Constructions/BRecOn.lean

@@ -0,0 +1,393 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Joachim Breitner
+-/
+prelude
+import Lean.Meta.InferType
+import Lean.AuxRecursor
+import Lean.AddDecl
+import Lean.Meta.CompletionName
+
+namespace Lean
+open Meta
+
+section PProd
+
+/--!
+Helpers to construct types and values of `PProd` and project out of them, set up to use `And`
+instead of `PProd` if the universes allow. Maybe be extracted into a Utils module when useful
+elsewhere.
+-/
+
+private def mkPUnit : Level → Expr
+  | .zero => .const ``True []
+  | lvl   => .const ``PUnit [lvl]
+
+private def mkPProd (e1 e2 : Expr) : MetaM Expr := do
+  let lvl1 ← getLevel e1
+  let lvl2 ← getLevel e2
+  if lvl1 matches .zero && lvl2 matches .zero then
+    return mkApp2 (.const `And []) e1 e2
+  else
+    return mkApp2 (.const ``PProd [lvl1, lvl2]) e1 e2
+
+private def mkNProd (lvl : Level) (es : Array Expr) : MetaM Expr :=
+  es.foldrM (init := mkPUnit lvl) mkPProd
+
+private def mkPUnitMk : Level → Expr
+  | .zero => .const ``True.intro []
+  | lvl   => .const ``PUnit.unit [lvl]
+
+private def mkPProdMk (e1 e2 : Expr) : MetaM Expr := do
+  let t1 ← inferType e1
+  let t2 ← inferType e2
+  let lvl1 ← getLevel t1
+  let lvl2 ← getLevel t2
+  if lvl1 matches .zero && lvl2 matches .zero then
+    return mkApp4 (.const ``And.intro []) t1 t2 e1 e2
+  else
+    return mkApp4 (.const ``PProd.mk [lvl1, lvl2]) t1 t2 e1 e2
+
+private def mkNProdMk (lvl : Level) (es : Array Expr) : MetaM Expr :=
+  es.foldrM (init := mkPUnitMk lvl) mkPProdMk
+
+/-- `PProd.fst` or `And.left` (as projections) -/
+private def mkPProdFst (e : Expr) : MetaM Expr := do
+  let t ← whnf (← inferType e)
+  match_expr t with
+  | PProd _ _ => return .proj ``PProd 0 e
+  | And _ _ =>   return .proj ``And 0 e
+  | _ => throwError "Cannot project .1 out of{indentExpr e}\nof type{indentExpr t}"
+
+/-- `PProd.snd` or `And.right` (as projections) -/
+private def mkPProdSnd (e : Expr) : MetaM Expr := do
+  let t ← whnf (← inferType e)
+  match_expr t with
+  | PProd _ _ => return .proj ``PProd 1 e
+  | And _ _ =>   return .proj ``And 1 e
+  | _ => throwError "Cannot project .2 out of{indentExpr e}\nof type{indentExpr t}"
+
+end PProd
+
+/--
+If `minorType` is the type of a minor premies of a recursor, such as
+```
+  (cons : (head : α) → (tail : List α) → (tail_hs : motive tail) → motive (head :: tail))
+```
+of `List.rec`, constructs the corresponding argument to `List.rec` in the construction
+of `.below` definition; in this case
+```
+fun head tail tail_ih =>
+  PProd (PProd (motive tail) tail_ih) PUnit
+```
+of type
+```
+α → List α → Sort (max 1 u_1) → Sort (max 1 u_1)
+```
+The parameter `typeFormers` are the `motive`s.
+-/
+private def buildBelowMinorPremise (rlvl : Level) (typeFormers : Array Expr) (minorType : Expr) : MetaM Expr :=
+  forallTelescope minorType fun minor_args _ => do go #[] minor_args.toList
+where
+  ibelow := rlvl matches .zero
+  go (prods : Array Expr) : List Expr → MetaM Expr
+  | [] => mkNProd rlvl prods
+  | arg::args => do
+    let argType ← inferType arg
+    forallTelescope argType fun arg_args arg_type => do
+      if typeFormers.contains arg_type.getAppFn then
+        let name ← arg.fvarId!.getUserName
+        let type' ← forallTelescope argType fun args _ => mkForallFVars args (.sort rlvl)
+        withLocalDeclD name type' fun arg' => do
+          let snd ← mkForallFVars arg_args (mkAppN arg' arg_args)
+          let e' ← mkPProd argType snd
+          mkLambdaFVars #[arg'] (← go (prods.push e') args)
+      else
+        mkLambdaFVars #[arg] (← go prods args)
+
+/--
+Constructs the `.below` or `.ibelow` definition for a inductive predicate.
+
+For example for the `List` type, it constructs,
+```
+@[reducible] protected def List.below.{u_1, u} : {α : Type u} →
+  {motive : List α → Sort u_1} → List α → Sort (max 1 u_1) :=
+fun {α} {motive} t =>
+  List.rec PUnit (fun head tail tail_ih => PProd (PProd (motive tail) tail_ih) PUnit) t
+```
+and
+```
+@[reducible] protected def List.ibelow.{u} : {α : Type u} →
+  {motive : List α → Prop} → List α → Prop :=
+fun {α} {motive} t =>
+  List.rec True (fun head tail tail_ih => (motive tail ∧ tail_ih) ∧ True) t
+```
+-/
+private def mkBelowOrIBelow (indName : Name) (ibelow : Bool) : MetaM Unit := do
+  let .inductInfo indVal ← getConstInfo indName | return
+  unless indVal.isRec do return
+  if ← isPropFormerType indVal.type then return
+
+  let recName := mkRecName indName
+  -- The construction follows the type of `ind.rec`
+  let .recInfo recVal ← getConstInfo recName
+    | throwError "{recName} not a .recInfo"
+  let lvl::lvls := recVal.levelParams.map (Level.param ·)
+    | throwError "recursor {recName} has no levelParams"
+  let lvlParam := recVal.levelParams.head!
+  -- universe parameter names of ibelow/below
+  let blvls :=
+    -- For ibelow we instantiate the first universe parameter of `.rec` to `.zero`
+    if ibelow then recVal.levelParams.tail!
+              else recVal.levelParams
+  let .some ilvl ← typeFormerTypeLevel indVal.type
+    | throwError "type {indVal.type} of inductive {indVal.name} not a type former?"
+
+  -- universe level of the resultant type
+  let rlvl : Level :=
+    if ibelow then
+      0
+    else if indVal.isReflexive then
+      if let .max 1 ilvl' := ilvl then
+        mkLevelMax' (.succ lvl) ilvl'
+      else
+        mkLevelMax' (.succ lvl) ilvl
+    else
+      mkLevelMax' 1 lvl
+
+  let refType :=
+    if ibelow then
+      recVal.type.instantiateLevelParams [lvlParam] [0]
+    else if indVal.isReflexive then
+      recVal.type.instantiateLevelParams [lvlParam] [lvl.succ]
+    else
+      recVal.type
+
+  let decl ← forallTelescope refType fun refArgs _ => do
+    assert! refArgs.size == indVal.numParams + recVal.numMotives + recVal.numMinors + indVal.numIndices + 1
+    let params      : Array Expr := refArgs[:indVal.numParams]
+    let typeFormers : Array Expr := refArgs[indVal.numParams:indVal.numParams + recVal.numMotives]
+    let minors      : Array Expr := refArgs[indVal.numParams + recVal.numMotives:indVal.numParams + recVal.numMotives + recVal.numMinors]
+    let remaining   : Array Expr := refArgs[indVal.numParams + recVal.numMotives + recVal.numMinors:]
+
+    let mut val := .const recName (rlvl.succ :: lvls)
+    -- add parameters
+    val := mkAppN val params
+    -- add type formers
+    for typeFormer in typeFormers do
+      let arg ← forallTelescope (← inferType typeFormer) fun targs _ =>
+        mkLambdaFVars targs (.sort rlvl)
+      val := .app val arg
+    -- add minor premises
+    for minor in minors do
+      let arg ← buildBelowMinorPremise rlvl typeFormers (← inferType minor)
+      val := .app val arg
+    -- add indices and major premise
+    val := mkAppN val remaining
+
+    -- All paramaters of `.rec` besides the `minors` become parameters of `.below`
+    let below_params := params ++ typeFormers ++ remaining
+    let type ← mkForallFVars below_params (.sort rlvl)
+    val ← mkLambdaFVars below_params val
+
+    let name := if ibelow then mkIBelowName indName else mkBelowName indName
+    mkDefinitionValInferrringUnsafe name blvls type val .abbrev
+
+  addDecl (.defnDecl decl)
+  setReducibleAttribute decl.name
+  modifyEnv fun env => markAuxRecursor env decl.name
+  modifyEnv fun env => addProtected env decl.name
+
+def mkBelow (declName : Name) : MetaM Unit := mkBelowOrIBelow declName true
+def mkIBelow (declName : Name) : MetaM Unit := mkBelowOrIBelow declName false
+
+/--
+If `minorType` is the type of a minor premies of a recursor, such as
+```
+  (cons : (head : α) → (tail : List α) → (tail_hs : motive tail) → motive (head :: tail))
+```
+of `List.rec`, constructs the corresponding argument to `List.rec` in the construction
+of `.brecOn` definition; in this case
+```
+fun head tail tail_ih =>
+  ⟨F_1 (head :: tail) ⟨tail_ih, PUnit.unit⟩, ⟨tail_ih, PUnit.unit⟩⟩
+```
+of type
+```
+(head : α) → (tail : List α) →
+  PProd (motive tail) (List.below tail) →
+  PProd (motive (head :: tail)) (PProd (PProd (motive tail) (List.below tail)) PUnit)
+```
+The parameter `typeFormers` are the `motive`s.
+-/
+private def buildBRecOnMinorPremise (rlvl : Level) (typeFormers : Array Expr)
+    (belows : Array Expr) (fs : Array Expr) (minorType : Expr) : MetaM Expr :=
+  forallTelescope minorType fun minor_args minor_type => do
+    let rec go (prods : Array Expr) : List Expr → MetaM Expr
+      | [] => minor_type.withApp fun minor_type_fn minor_type_args => do
+          let b ← mkNProdMk rlvl prods
+          let .some ⟨idx, _⟩ := typeFormers.indexOf? minor_type_fn
+            | throwError m!"Did not find {minor_type} in {typeFormers}"
+          mkPProdMk (mkAppN fs[idx]! (minor_type_args.push b)) b
+      | arg::args => do
+        let argType ← inferType arg
+        forallTelescope argType fun arg_args arg_type => do
+          arg_type.withApp fun arg_type_fn arg_type_args => do
+            if let .some idx := typeFormers.indexOf? arg_type_fn then
+              let name ← arg.fvarId!.getUserName
+              let type' ← mkForallFVars arg_args
+                (← mkPProd arg_type (mkAppN belows[idx]! arg_type_args) )
+              withLocalDeclD name type' fun arg' => do
+                if arg_args.isEmpty then
+                  mkLambdaFVars #[arg'] (← go (prods.push arg') args)
+                else
+                  let r := mkAppN arg' arg_args
+                  let r₁ ← mkLambdaFVars arg_args (← mkPProdFst r)
+                  let r₂ ← mkLambdaFVars arg_args (← mkPProdSnd r)
+                  let r ← mkPProdMk r₁ r₂
+                  mkLambdaFVars #[arg'] (← go (prods.push r) args)
+            else
+              mkLambdaFVars #[arg] (← go prods args)
+    go #[] minor_args.toList
+
+/--
+Constructs the `.brecon` or `.binductionon` definition for a inductive predicate.
+
+For example for the `List` type, it constructs,
+```
+@[reducible] protected def List.brecOn.{u_1, u} : {α : Type u} → {motive : List α → Sort u_1} →
+  (t : List α) → ((t : List α) → List.below t → motive t) → motive t :=
+fun {α} {motive} t (F_1 : (t : List α) → List.below t → motive t) => (
+  @List.rec α (fun t => PProd (motive t) (@List.below α motive t))
+    ⟨F_1 [] PUnit.unit, PUnit.unit⟩
+    (fun head tail tail_ih => ⟨F_1 (head :: tail) ⟨tail_ih, PUnit.unit⟩, ⟨tail_ih, PUnit.unit⟩⟩)
+    t
+  ).1
+```
+and
+```
+@[reducible] protected def List.binductionOn.{u} : ∀ {α : Type u} {motive : List α → Prop}
+  (t : List α), (∀ (t : List α), List.ibelow t → motive t) → motive t :=
+fun {α} {motive} t F_1 => (
+  @List.rec α (fun t => And (motive t) (@List.ibelow α motive t))
+    ⟨F_1 [] True.intro, True.intro⟩
+    (fun head tail tail_ih => ⟨F_1 (head :: tail) ⟨tail_ih, True.intro⟩, ⟨tail_ih, True.intro⟩⟩)
+    t
+  ).1
+```
+-/
+def mkBRecOnOrBInductionOn (indName : Name) (ind : Bool) : MetaM Unit := do
+  let .inductInfo indVal ← getConstInfo indName | return
+  unless indVal.isRec do return
+  if ← isPropFormerType indVal.type then return
+  let recName := mkRecName indName
+  let .recInfo recVal ← getConstInfo recName | return
+  unless recVal.numMotives = indVal.all.length do
+    /-
+    The mutual declaration containing `declName` contains nested inductive datatypes.
+    We don't support this kind of declaration here yet. We probably never will :)
+    To support it, we will need to generate an auxiliary `below` for each nested inductive
+    type since their default `below` is not good here. For example, at
+    ```
+    inductive Term
+    | var : String -> Term
+    | app : String -> List Term -> Term
+    ```
+    The `List.below` is not useful since it will not allow us to recurse over the nested terms.
+    We need to generate another one using the auxiliary recursor `Term.rec_1` for `List Term`.
+    -/
+    return
+
+  let lvl::lvls := recVal.levelParams.map (Level.param ·)
+    | throwError "recursor {recName} has no levelParams"
+  let lvlParam := recVal.levelParams.head!
+  -- universe parameter names of brecOn/binductionOn
+  let blps := if ind then recVal.levelParams.tail!  else recVal.levelParams
+  -- universe arguments of below/ibelow
+  let blvls := if ind then lvls else lvl::lvls
+
+  let .some ⟨idx, _⟩ := indVal.all.toArray.indexOf? indName
+    | throwError m!"Did not find {indName} in {indVal.all}"
+
+  let .some ilvl ← typeFormerTypeLevel indVal.type
+    | throwError "type {indVal.type} of inductive {indVal.name} not a type former?"
+  -- universe level of the resultant type
+  let rlvl : Level :=
+    if ind then
+      0
+    else if indVal.isReflexive then
+      if let .max 1 ilvl' := ilvl then
+        mkLevelMax' (.succ lvl) ilvl'
+      else
+        mkLevelMax' (.succ lvl) ilvl
+    else
+      mkLevelMax' 1 lvl
+
+  let refType :=
+    if ind then
+      recVal.type.instantiateLevelParams [lvlParam] [0]
+    else if indVal.isReflexive then
+      recVal.type.instantiateLevelParams [lvlParam] [lvl.succ]
+    else
+      recVal.type
+
+  let decl ← forallTelescope refType fun refArgs _ => do
+    assert! refArgs.size == indVal.numParams + recVal.numMotives + recVal.numMinors + indVal.numIndices + 1
+    let params      : Array Expr := refArgs[:indVal.numParams]
+    let typeFormers : Array Expr := refArgs[indVal.numParams:indVal.numParams + recVal.numMotives]
+    let minors      : Array Expr := refArgs[indVal.numParams + recVal.numMotives:indVal.numParams + recVal.numMotives + recVal.numMinors]
+    let remaining   : Array Expr := refArgs[indVal.numParams + recVal.numMotives + recVal.numMinors:]
+
+    -- One `below` for each type former (same parameters)
+    let belows := indVal.all.toArray.map fun n =>
+      let belowName := if ind then mkIBelowName n else mkBelowName n
+      mkAppN (.const belowName blvls) (params ++ typeFormers)
+
+    -- create types of functionals (one for each type former)
+    --   (F_1 : (t : List α) → (f : List.below t) → motive t)
+    -- and bring parameters of that type into scope
+    let mut fDecls : Array (Name × (Array Expr -> MetaM Expr)) := #[]
+    for typeFormer in typeFormers, below in belows, i in [:typeFormers.size] do
+      let fType ← forallTelescope (← inferType typeFormer) fun targs _ => do
+        withLocalDeclD `f (mkAppN below targs) fun f =>
+          mkForallFVars (targs.push f) (mkAppN typeFormer targs)
+      let fName := .mkSimple s!"F_{i + 1}"
+      fDecls := fDecls.push (fName, fun _ => pure fType)
+    withLocalDeclsD fDecls fun fs => do
+      let mut val := .const recName (rlvl :: lvls)
+      -- add parameters
+      val := mkAppN val params
+      -- add type formers
+      for typeFormer in typeFormers, below in belows do
+        -- example: (motive := fun t => PProd (motive t) (@List.below α motive t))
+        let arg ← forallTelescope (← inferType typeFormer) fun targs _ => do
+          let cType := mkAppN typeFormer targs
+          let belowType := mkAppN below targs
+          let arg ← mkPProd cType belowType
+          mkLambdaFVars targs arg
+        val := .app val arg
+      -- add minor premises
+      for minor in minors do
+        let arg ← buildBRecOnMinorPremise rlvl typeFormers belows fs (← inferType minor)
+        val := .app val arg
+      -- add indices and major premise
+      val := mkAppN val remaining
+      -- project out first component
+      val ← mkPProdFst val
+
+      -- All paramaters of `.rec` besides the `minors` become parameters of `.bRecOn`, and the `fs`
+      let below_params := params ++ typeFormers ++ remaining ++ fs
+      let type ← mkForallFVars below_params (mkAppN typeFormers[idx]! remaining)
+      val ← mkLambdaFVars below_params val
+
+      let name := if ind then mkBInductionOnName indName else mkBRecOnName indName
+      mkDefinitionValInferrringUnsafe name blps type val .abbrev
+
+  addDecl (.defnDecl decl)
+  setReducibleAttribute decl.name
+  modifyEnv fun env => markAuxRecursor env decl.name
+  modifyEnv fun env => addProtected env decl.name
+
+def mkBRecOn (declName : Name) : MetaM Unit := mkBRecOnOrBInductionOn declName false
+def mkBInductionOn (declName : Name) : MetaM Unit := mkBRecOnOrBInductionOn declName true

src/Lean/Meta/Constructions/CasesOn.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.AddDecl
+import Lean.Meta.Basic
+
+namespace Lean
+
+@[extern "lean_mk_cases_on"] opaque mkCasesOnImp (env : Environment) (declName : @& Name) : Except KernelException Declaration
+
+open Meta
+
+def mkCasesOn (declName : Name) : MetaM Unit := do
+  let name := mkCasesOnName declName
+  let decl ← ofExceptKernelException (mkCasesOnImp (← getEnv) declName)
+  addDecl decl
+  setReducibleAttribute name
+  modifyEnv fun env => markAuxRecursor env name
+
+end Lean

src/Lean/Meta/Constructions/NoConfusion.lean

@@ -0,0 +1,126 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.AddDecl
+import Lean.Meta.AppBuilder
+import Lean.Meta.CompletionName
+
+namespace Lean
+
+@[extern "lean_mk_no_confusion_type"] opaque mkNoConfusionTypeCoreImp (env : Environment) (declName : @& Name) : Except KernelException Declaration
+@[extern "lean_mk_no_confusion"] opaque mkNoConfusionCoreImp (env : Environment) (declName : @& Name) : Except KernelException Declaration
+
+open Meta
+
+def mkNoConfusionCore (declName : Name) : MetaM Unit := do
+  -- Do not do anything unless can_elim_to_type. TODO: Extract to util
+  let .inductInfo indVal ← getConstInfo declName | return
+  let recInfo ← getConstInfo (mkRecName declName)
+  unless recInfo.levelParams.length > indVal.levelParams.length do return
+
+  let name := Name.mkStr declName "noConfusionType"
+  let decl ← ofExceptKernelException (mkNoConfusionTypeCoreImp (← getEnv) declName)
+  addDecl decl
+  setReducibleAttribute name
+  modifyEnv fun env => addToCompletionBlackList env name
+  modifyEnv fun env => addProtected env name
+
+  let name := Name.mkStr declName "noConfusion"
+  let decl ← ofExceptKernelException (mkNoConfusionCoreImp (← getEnv) declName)
+  addDecl decl
+  setReducibleAttribute name
+  modifyEnv fun env => markNoConfusion env name
+  modifyEnv fun env => addProtected env name
+
+def mkNoConfusionEnum (enumName : Name) : MetaM Unit := do
+  if (← getEnv).contains ``noConfusionEnum then
+    mkToCtorIdx
+    mkNoConfusionType
+    mkNoConfusion
+  else
+    -- `noConfusionEnum` was not defined yet, so we use `mkNoConfusionCore`
+    mkNoConfusionCore enumName
+where
+  mkToCtorIdx : MetaM Unit := do
+    let ConstantInfo.inductInfo info ← getConstInfo enumName | unreachable!
+    let us := info.levelParams.map mkLevelParam
+    let numCtors := info.ctors.length
+    let declName := Name.mkStr enumName "toCtorIdx"
+    let enumType := mkConst enumName us
+    let natType  := mkConst ``Nat
+    let declType ← mkArrow enumType natType
+    let mut minors := #[]
+    for i in [:numCtors] do
+      minors := minors.push <| mkNatLit i
+    withLocalDeclD `x enumType fun x => do
+      let motive ← mkLambdaFVars #[x] natType
+      let declValue ← mkLambdaFVars #[x] <| mkAppN (mkApp2 (mkConst (mkCasesOnName enumName) (levelOne::us)) motive x) minors
+      addAndCompile <| Declaration.defnDecl {
+        name        := declName
+        levelParams := info.levelParams
+        type        := declType
+        value       := declValue
+        safety      := DefinitionSafety.safe
+        hints       := ReducibilityHints.abbrev
+      }
+      setReducibleAttribute declName
+
+  mkNoConfusionType : MetaM Unit := do
+    let ConstantInfo.inductInfo info ← getConstInfo enumName | unreachable!
+    let us := info.levelParams.map mkLevelParam
+    let v ← mkFreshUserName `v
+    let enumType := mkConst enumName us
+    let sortV := mkSort (mkLevelParam v)
+    let toCtorIdx := mkConst (Name.mkStr enumName "toCtorIdx") us
+    withLocalDeclD `P sortV fun P =>
+    withLocalDeclD `x enumType fun x =>
+    withLocalDeclD `y enumType fun y => do
+      let declType  ← mkForallFVars #[P, x, y] sortV
+      let declValue ← mkLambdaFVars #[P, x, y] (← mkAppM ``noConfusionTypeEnum #[toCtorIdx, P, x, y])
+      let declName  := Name.mkStr enumName "noConfusionType"
+      addAndCompile <| Declaration.defnDecl {
+        name        := declName
+        levelParams := v :: info.levelParams
+        type        := declType
+        value       := declValue
+        safety      := DefinitionSafety.safe
+        hints       := ReducibilityHints.abbrev
+      }
+      setReducibleAttribute declName
+
+  mkNoConfusion : MetaM Unit := do
+    let ConstantInfo.inductInfo info ← getConstInfo enumName | unreachable!
+    let us := info.levelParams.map mkLevelParam
+    let v ← mkFreshUserName `v
+    let enumType := mkConst enumName us
+    let sortV := mkSort (mkLevelParam v)
+    let toCtorIdx := mkConst (Name.mkStr enumName "toCtorIdx") us
+    let noConfusionType := mkConst (Name.mkStr enumName "noConfusionType") (mkLevelParam v :: us)
+    withLocalDecl `P BinderInfo.implicit sortV fun P =>
+    withLocalDecl `x BinderInfo.implicit enumType fun x =>
+    withLocalDecl `y BinderInfo.implicit enumType fun y => do
+    withLocalDeclD `h (← mkEq x y) fun h => do
+      let declType  ← mkForallFVars #[P, x, y, h] (mkApp3 noConfusionType P x y)
+      let declValue ← mkLambdaFVars #[P, x, y, h] (← mkAppOptM ``noConfusionEnum #[none, none, none, toCtorIdx, P, x, y, h])
+      let declName  := Name.mkStr enumName "noConfusion"
+      addAndCompile <| Declaration.defnDecl {
+        name        := declName
+        levelParams := v :: info.levelParams
+        type        := declType
+        value       := declValue
+        safety      := DefinitionSafety.safe
+        hints       := ReducibilityHints.abbrev
+      }
+      setReducibleAttribute declName
+      modifyEnv fun env => markNoConfusion env declName
+
+def mkNoConfusion (declName : Name) : MetaM Unit := do
+  if (← isEnumType declName) then
+    mkNoConfusionEnum declName
+  else
+    mkNoConfusionCore declName
+
+end Lean

src/Lean/Meta/Diagnostics.lean

@@ -69,6 +69,9 @@ def mkDiagSynthPendingFailure (failures : PHashMap Expr MessageData) : MetaM Dia
       data := data.push m!"{if data.isEmpty then "  " else "\n"}{msg}"
     return { data }
 
+/--
+We use below that this returns `m` unchanged if `s.isEmpty`
+-/
 def appendSection (m : MessageData) (cls : Name) (header : String) (s : DiagSummary) (resultSummary := true) : MessageData :=
   if s.isEmpty then
     m
@@ -86,17 +89,17 @@ def reportDiag : MetaM Unit := do
     let inst ← mkDiagSummaryForUsedInstances
     let synthPending ← mkDiagSynthPendingFailure (← get).diag.synthPendingFailures
     let unfoldKernel ← mkDiagSummary (Kernel.getDiagnostics (← getEnv)).unfoldCounter
-    unless unfoldDefault.isEmpty && unfoldInstance.isEmpty && unfoldReducible.isEmpty && heu.isEmpty && inst.isEmpty && synthPending.isEmpty do
-      let m := MessageData.nil
-      let m := appendSection m `reduction "unfolded declarations" unfoldDefault
-      let m := appendSection m `reduction "unfolded instances" unfoldInstance
-      let m := appendSection m `reduction "unfolded reducible declarations" unfoldReducible
-      let m := appendSection m `type_class "used instances" inst
-      let m := appendSection m `type_class
-                 s!"max synth pending failures (maxSynthPendingDepth: {maxSynthPendingDepth.get (← getOptions)}), use `set_option maxSynthPendingDepth <limit>`"
-                 synthPending (resultSummary := false)
-      let m := appendSection m `def_eq "heuristic for solving `f a =?= f b`" heu
-      let m := appendSection m `kernel "unfolded declarations" unfoldKernel
+    let m := MessageData.nil
+    let m := appendSection m `reduction "unfolded declarations" unfoldDefault
+    let m := appendSection m `reduction "unfolded instances" unfoldInstance
+    let m := appendSection m `reduction "unfolded reducible declarations" unfoldReducible
+    let m := appendSection m `type_class "used instances" inst
+    let m := appendSection m `type_class
+              s!"max synth pending failures (maxSynthPendingDepth: {maxSynthPendingDepth.get (← getOptions)}), use `set_option maxSynthPendingDepth <limit>`"
+              synthPending (resultSummary := false)
+    let m := appendSection m `def_eq "heuristic for solving `f a =?= f b`" heu
+    let m := appendSection m `kernel "unfolded declarations" unfoldKernel
+    unless m matches .nil do
       let m := m ++ "use `set_option diagnostics.threshold <num>` to control threshold for reporting counters"
       logInfo m
 

src/Lean/Meta/ExprDefEq.lean

@@ -1815,6 +1815,32 @@ end
       let e ← instantiateMVars e
       successK e
     else
+      if (← read).config.isDefEqStuckEx then
+        /-
+        When `isDefEqStuckEx := true` and `mvar` was created in a previous level,
+        we should throw an exception. See issue #2736 for a situation where this can happen.
+        This can happen when we have type classes such as
+        ```
+        class RightDistribClass (R : Type) [Mul R] [Add R] : Prop where
+          right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c
+        ```
+        and a theorem
+        ```
+        theorem add_one_mul [Add α] [MulOneClass α] [RightDistribClass α] (a b : α)
+                : (a + 1) * b = a * b + b
+        ```
+        and then we try to elaborate
+        ```
+        #check (add_one_mul)
+        ```
+        When we try to synthesize `@RightDistribClass ?α (MulOneClass.toMul ?moInst) ?addInst`
+        we get stuck at the term `(MulOneClass.toMul ?moInst)`, and we should abort
+        type class resolution, which sets `isDefEqStuckEx := true`, because `?moInst : MulOneClass ?α`
+        was **not** created by the type class resolution procedure.
+        -/
+        let mvarDecl ← mvarId.getDecl
+        if mvarDecl.depth < (← getMCtx).depth then
+          Meta.throwIsDefEqStuck
       failK
   | none   => failK
 

src/Lean/Meta/IndPredBelow.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Dany Fabian
 -/
 prelude
-import Lean.Meta.Constructions
+import Lean.Meta.Constructions.CasesOn
 import Lean.Meta.Match.Match
 
 namespace Lean.Meta.IndPredBelow
@@ -434,7 +434,7 @@ partial def mkBelowMatcher
   withExistingLocalDecls (lhss.foldl (init := []) fun s v => s ++ v.fvarDecls) do
     for lhs in lhss do
       trace[Meta.IndPredBelow.match] "{lhs.patterns.map (·.toMessageData)}"
-  let res ← Match.mkMatcher { matcherName, matchType, discrInfos := mkArray (mkMatcherInput.numDiscrs + 1) {}, lhss }
+  let res ← Match.mkMatcher (exceptionIfContainsSorry := true) { matcherName, matchType, discrInfos := mkArray (mkMatcherInput.numDiscrs + 1) {}, lhss }
   res.addMatcher
   -- if a wrong index is picked, the resulting matcher can be type-incorrect.
   -- we check here, so that errors can propagate higher up the call stack.

src/Lean/Meta/Match/Match.lean

@@ -830,8 +830,12 @@ Each `AltLHS` has a list of local declarations and a list of patterns.
 The number of patterns must be the same in each `AltLHS`.
 The generated matcher has the structure described at `MatcherInfo`. The motive argument is of the form
 `(motive : (a_1 : A_1) -> (a_2 : A_2[a_1]) -> ... -> (a_n : A_n[a_1, a_2, ... a_{n-1}]) -> Sort v)`
-where `v` is a universe parameter or 0 if `B[a_1, ..., a_n]` is a proposition. -/
-def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := withCleanLCtxFor input do
+where `v` is a universe parameter or 0 if `B[a_1, ..., a_n]` is a proposition.
+
+If `exceptionIfContainsSorry := true`, then `mkMatcher` throws an exception if the auxiliary
+declarations contains a `sorry`. We use this argument to workaround a bug at `IndPredBelow.mkBelowMatcher`.
+-/
+def mkMatcher (input : MkMatcherInput) (exceptionIfContainsSorry := false) : MetaM MatcherResult := withCleanLCtxFor input do
   let ⟨matcherName, matchType, discrInfos, lhss⟩ := input
   let numDiscrs := discrInfos.size
   let numEqs := getNumEqsFromDiscrInfos discrInfos
@@ -844,6 +848,11 @@ def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := withCleanLCtxFor
   let uElim ← getLevel matchTypeBody
   let uElimGen ← if uElim == levelZero then pure levelZero else mkFreshLevelMVar
   let mkMatcher (type val : Expr) (minors : Array (Expr × Nat)) (s : State) : MetaM MatcherResult := do
+    let val ← instantiateMVars val
+    let type ← instantiateMVars type
+    if exceptionIfContainsSorry then
+      if type.hasSorry || val.hasSorry then
+        throwError "failed to create auxiliary match declaration `{matcherName}`, it contains `sorry`"
     trace[Meta.Match.debug] "matcher value: {val}\ntype: {type}"
     trace[Meta.Match.debug] "minors num params: {minors.map (·.2)}"
     /- The option `bootstrap.gen_matcher_code` is a helper hack. It is useful, for example,
@@ -857,7 +866,6 @@ def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := withCleanLCtxFor
        | negSucc n => succ n
        ```
        which is defined **before** `Int.decLt` -/
-
     let (matcher, addMatcher) ← mkMatcherAuxDefinition matcherName type val
     trace[Meta.Match.debug] "matcher levels: {matcher.getAppFn.constLevels!}, uElim: {uElimGen}"
     let uElimPos? ← getUElimPos? matcher.getAppFn.constLevels! uElimGen

src/Lean/Meta/Offset.lean

@@ -7,6 +7,8 @@ prelude
 import Lean.Data.LBool
 import Lean.Meta.InferType
 import Lean.Meta.NatInstTesters
+import Lean.Meta.NatInstTesters
+import Lean.Util.SafeExponentiation
 
 namespace Lean.Meta
 
@@ -29,6 +31,10 @@ partial def evalNat (e : Expr) : OptionT MetaM Nat := do
   | .mvar ..             => visit e
   | _                    => failure
 where
+  evalPow (b n : Expr) : OptionT MetaM Nat := do
+    let n ← evalNat n
+    guard (← checkExponent n)
+    return (← evalNat b) ^ n
   visit e := do
     match_expr e with
     | OfNat.ofNat _ n i => guard (← isInstOfNatNat i); evalNat n
@@ -48,10 +54,10 @@ where
     | Nat.mod a b => return (← evalNat a) % (← evalNat b)
     | Mod.mod _ i a b => guard (← isInstModNat i); return (← evalNat a) % (← evalNat b)
     | HMod.hMod _ _ _ i a b => guard (← isInstHModNat i); return (← evalNat a) % (← evalNat b)
-    | Nat.pow a b => return (← evalNat a) ^ (← evalNat b)
-    | NatPow.pow _ i a b => guard (← isInstNatPowNat i); return (← evalNat a) ^ (← evalNat b)
-    | Pow.pow _ _ i a b => guard (← isInstPowNat i); return (← evalNat a) ^ (← evalNat b)
-    | HPow.hPow _ _ _ i a b => guard (← isInstHPowNat i); return (← evalNat a) ^ (← evalNat b)
+    | Nat.pow a b => evalPow a b
+    | NatPow.pow _ i a b => guard (← isInstNatPowNat i); evalPow a b
+    | Pow.pow _ _ i a b => guard (← isInstPowNat i); evalPow a b
+    | HPow.hPow _ _ _ i a b => guard (← isInstHPowNat i); evalPow a b
     | _ => failure
 
 /--

src/Lean/Meta/Tactic/Apply.lean

@@ -29,18 +29,73 @@ private def throwApplyError {α} (mvarId : MVarId) (eType : Expr) (targetType :
     return m!"{indentExpr eType}\nwith{indentExpr targetType}"
   throwTacticEx `apply mvarId m!"failed to unify{explanation}"
 
-def synthAppInstances (tacticName : Name) (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Array BinderInfo)
-    (synthAssignedInstances : Bool) (allowSynthFailures : Bool) : MetaM Unit :=
-  newMVars.size.forM fun i => do
-    if binderInfos[i]!.isInstImplicit then
-      let mvar := newMVars[i]!
+def synthAppInstances (tacticName : Name) (mvarId : MVarId) (mvarsNew : Array Expr) (binderInfos : Array BinderInfo)
+    (synthAssignedInstances : Bool) (allowSynthFailures : Bool) : MetaM Unit := do
+  let mut todo := #[]
+  -- Collect metavariables to synthesize
+  for mvar in mvarsNew, binderInfo in binderInfos do
+    if binderInfo.isInstImplicit then
       if synthAssignedInstances || !(← mvar.mvarId!.isAssigned) then
-        let mvarType ← inferType mvar
-        try
-          let mvarVal  ← synthInstance mvarType
-          unless (← isDefEq mvar mvarVal) do
+        todo := todo.push mvar
+  while !todo.isEmpty do
+    todo ← step todo
+where
+  /--
+  Try to synthesize instances for the metavariables `mvars`.
+  Returns metavariables that still need to be synthesized.
+  We can view the resulting array as the set of metavariables that we should try again.
+  This is needed when applying or rewriting with functions with complex instances.
+  For example, consider `rw [@map_smul]` where `map_smul` is
+  ```
+  map_smul {F : Type u_1} {M : Type u_2} {N : Type u_3} {φ : M → N}
+           {X : Type u_4} {Y : Type u_5}
+           [SMul M X] [SMul N Y] [FunLike F X Y] [MulActionSemiHomClass F φ X Y]
+           (f : F) (c : M) (x : X) : DFunLike.coe f (c • x) = φ c • DFunLike.coe f x
+  ```
+  and `MulActionSemiHomClass` is defined as
+  ```
+  class MulActionSemiHomClass (F : Type _)
+     {M N : outParam (Type _)} (φ : outParam (M → N))
+     (X Y : outParam (Type _)) [SMul M X] [SMul N Y] [FunLike F X Y] : Prop where
+  ```
+  The left-hand-side of the equation does not bind `N`. Thus, `SMul N Y` cannot
+  be synthesized until we synthesize `MulActionSemiHomClass F φ X Y`. Note that
+  `N` is an output parameter for `MulActionSemiHomClass`.
+  -/
+  step (mvars : Array Expr) : MetaM (Array Expr) := do
+    -- `ex?` stores the exception for this first synthesis failure in this step.
+    let mut ex? := none
+    -- `true` if we managed to synthesize an instance after we hit a failure.
+    -- That is, there is a chance we may succeed if we try again.
+    let mut progressAfterEx := false
+    -- Metavariables that we failed to synthesize.
+    let mut postponed := #[]
+    for mvar in mvars do
+      let mvarType ← inferType mvar
+      let mvarVal? ← try
+        let mvarVal ← synthInstance mvarType
+        unless postponed.isEmpty do
+          progressAfterEx := true
+        pure (some mvarVal)
+      catch ex =>
+        ex? := some ex
+        postponed := postponed.push mvar
+        pure none
+      if let some mvarVal := mvarVal? then
+        unless (← isDefEq mvar mvarVal) do
+          -- There is no point in trying again for this kind of failure
+          unless allowSynthFailures do
             throwTacticEx tacticName mvarId "failed to assign synthesized instance"
-        catch e => unless allowSynthFailures do throw e
+    if let some ex := ex? then
+      if progressAfterEx then
+        return postponed
+      else
+        -- There is no point in running `step` again. We should give up (`allowSynthFailures`),
+        -- or throw the first exception we found in this `step`.
+        if allowSynthFailures then return #[] else throw ex
+    else
+      -- Done. We successfully synthesized all metavariables.
+      return #[]
 
 def appendParentTag (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Array BinderInfo) : MetaM Unit := do
   let parentTag ← mvarId.getTag
@@ -161,10 +216,6 @@ def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig :=
     result.forM (·.headBetaType)
     return result
 
-@[deprecated MVarId.apply (since := "2022-07-15")]
-def apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig := {}) : MetaM (List MVarId) :=
-  mvarId.apply e cfg
-
 /-- Short-hand for applying a constant to the goal. -/
 def _root_.Lean.MVarId.applyConst (mvar : MVarId) (c : Name) (cfg : ApplyConfig := {}) : MetaM (List MVarId) := do
   mvar.apply (← mkConstWithFreshMVarLevels c) cfg

src/Lean/Meta/Tactic/Assert.lean

@@ -24,10 +24,6 @@ def _root_.Lean.MVarId.assert (mvarId : MVarId) (name : Name) (type : Expr) (val
     mvarId.assign (mkApp newMVar val)
     return newMVar.mvarId!
 
-@[deprecated MVarId.assert (since := "2022-07-15")]
-def assert (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) : MetaM MVarId :=
-  mvarId.assert name type val
-
 /-- Add the hypothesis `h : t`, given `v : t`, and return the new `FVarId`. -/
 def _root_.Lean.MVarId.note (g : MVarId) (h : Name) (v : Expr) (t? : Option Expr := .none) :
     MetaM (FVarId × MVarId) := do
@@ -46,10 +42,6 @@ def _root_.Lean.MVarId.define (mvarId : MVarId) (name : Name) (type : Expr) (val
     mvarId.assign newMVar
     return newMVar.mvarId!
 
-@[deprecated MVarId.define (since := "2022-07-15")]
-def define (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) : MetaM MVarId := do
-  mvarId.define name type val
-
 /--
   Convert the given goal `Ctx |- target` into `Ctx |- (hName : type) -> hName = val -> target`.
   It assumes `val` has type `type` -/
@@ -66,10 +58,6 @@ def _root_.Lean.MVarId.assertExt (mvarId : MVarId) (name : Name) (type : Expr) (
     mvarId.assign (mkApp2 newMVar val rflPrf)
     return newMVar.mvarId!
 
-@[deprecated MVarId.assertExt (since := "2022-07-15")]
-def assertExt (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) (hName : Name := `h) : MetaM MVarId := do
-  mvarId.assertExt name type val hName
-
 structure AssertAfterResult where
   fvarId : FVarId
   mvarId : MVarId
@@ -90,10 +78,6 @@ def _root_.Lean.MVarId.assertAfter (mvarId : MVarId) (fvarId : FVarId) (userName
     subst := subst.insert f (mkFVar fNew)
   return { fvarId := fvarIdNew, mvarId, subst }
 
-@[deprecated MVarId.assertAfter (since := "2022-07-15")]
-def assertAfter (mvarId : MVarId) (fvarId : FVarId) (userName : Name) (type : Expr) (val : Expr) : MetaM AssertAfterResult := do
-  mvarId.assertAfter fvarId userName type val
-
 structure Hypothesis where
   userName : Name
   type     : Expr
@@ -116,11 +100,6 @@ def _root_.Lean.MVarId.assertHypotheses (mvarId : MVarId) (hs : Array Hypothesis
     mvarId.assign val
     mvarNew.mvarId!.introNP hs.size
 
-@[deprecated MVarId.assertHypotheses (since := "2022-07-15")]
-def assertHypotheses (mvarId : MVarId) (hs : Array Hypothesis) : MetaM (Array FVarId × MVarId) := do
-  mvarId.assertHypotheses hs
-
-
 /--
 Replace hypothesis `hyp` in goal `g` with `proof : typeNew`.
 The new hypothesis is given the same user name as the original,

src/Lean/Meta/Tactic/Assumption.lean

@@ -26,17 +26,9 @@ def _root_.Lean.MVarId.assumptionCore (mvarId : MVarId) : MetaM Bool :=
     | none => return false
     | some fvarId => mvarId.assign (mkFVar fvarId); return true
 
-@[deprecated MVarId.assumptionCore (since := "2022-07-15")]
-def assumptionCore (mvarId : MVarId) : MetaM Bool :=
-  mvarId.assumptionCore
-
 /-- Close goal `mvarId` using an assumption. Throw error message if failed. -/
 def _root_.Lean.MVarId.assumption (mvarId : MVarId) : MetaM Unit :=
   unless (← mvarId.assumptionCore) do
     throwTacticEx `assumption mvarId
 
-@[deprecated MVarId.assumption (since := "2022-07-15")]
-def assumption (mvarId : MVarId) : MetaM Unit :=
-  mvarId.assumption
-
 end Lean.Meta

src/Lean/Meta/Tactic/Cases.lean

@@ -269,10 +269,6 @@ Apply `casesOn` using the free variable `majorFVarId` as the major premise (aka
 def _root_.Lean.MVarId.cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array AltVarNames := #[]) (useNatCasesAuxOn : Bool := false) : MetaM (Array CasesSubgoal) :=
   Cases.cases mvarId majorFVarId givenNames (useNatCasesAuxOn := useNatCasesAuxOn)
 
-@[deprecated MVarId.cases (since := "2022-07-15")]
-def cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array AltVarNames := #[]) : MetaM (Array CasesSubgoal) :=
-  Cases.cases mvarId majorFVarId givenNames
-
 /--
 Keep applying `cases` on any hypothesis that satisfies `p`.
 -/

src/Lean/Meta/Tactic/Cleanup.lean

@@ -72,8 +72,4 @@ where
 abbrev _root_.Lean.MVarId.cleanup (mvarId : MVarId) (toPreserve : Array FVarId := #[]) (indirectProps : Bool := true) : MetaM MVarId := do
   cleanupCore mvarId toPreserve indirectProps
 
-@[deprecated MVarId.cleanup (since := "2022-07-15")]
-abbrev cleanup (mvarId : MVarId) : MetaM MVarId := do
-  mvarId.cleanup
-
 end Lean.Meta

src/Lean/Meta/Tactic/Clear.lean

@@ -35,10 +35,6 @@ def _root_.Lean.MVarId.clear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId
     pure newMVar.mvarId!
 
 
-@[deprecated MVarId.clear (since := "2022-07-15")]
-def clear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId :=
-  mvarId.clear fvarId
-
 /--
 Try to erase the given free variable from the goal `mvarId`. It is no-op if the free variable
 cannot be erased due to forward dependencies.
@@ -46,18 +42,10 @@ cannot be erased due to forward dependencies.
 def _root_.Lean.MVarId.tryClear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId :=
   mvarId.clear fvarId <|> pure mvarId
 
-@[deprecated MVarId.tryClear (since := "2022-07-15")]
-def tryClear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId :=
-  mvarId.tryClear fvarId
-
 /--
 Try to erase the given free variables from the goal `mvarId`.
 -/
 def _root_.Lean.MVarId.tryClearMany (mvarId : MVarId) (fvarIds : Array FVarId) : MetaM MVarId := do
   fvarIds.foldrM (init := mvarId) fun fvarId mvarId => mvarId.tryClear fvarId
 
-@[deprecated MVarId.tryClearMany (since := "2022-07-15")]
-def tryClearMany (mvarId : MVarId) (fvarIds : Array FVarId) : MetaM MVarId := do
-  mvarId.tryClearMany fvarIds
-
 end Lean.Meta

src/Lean/Meta/Tactic/Constructor.lean

@@ -28,10 +28,6 @@ def _root_.Lean.MVarId.constructor (mvarId : MVarId) (cfg : ApplyConfig := {}) :
             pure ()
         throwTacticEx `constructor mvarId "no applicable constructor found"
 
-@[deprecated MVarId.constructor (since := "2022-07-15")]
-def constructor (mvarId : MVarId) (cfg : ApplyConfig := {}) : MetaM (List MVarId) := do
-  mvarId.constructor cfg
-
 def _root_.Lean.MVarId.existsIntro (mvarId : MVarId) (w : Expr) : MetaM MVarId := do
   mvarId.withContext do
     mvarId.checkNotAssigned `exists
@@ -50,8 +46,4 @@ def _root_.Lean.MVarId.existsIntro (mvarId : MVarId) (w : Expr) : MetaM MVarId :
           | throwTacticEx `exists mvarId "unexpected number of subgoals"
         pure mvarId
 
-@[deprecated MVarId.existsIntro (since := "2022-07-15")]
-def existsIntro (mvarId : MVarId) (w : Expr) : MetaM MVarId := do
-  mvarId.existsIntro w
-
 end Lean.Meta

src/Lean/Meta/Tactic/Contradiction.lean

@@ -226,10 +226,6 @@ def _root_.Lean.MVarId.contradiction (mvarId : MVarId) (config : Contradiction.C
   unless (← mvarId.contradictionCore config) do
     throwTacticEx `contradiction mvarId
 
-@[deprecated MVarId.contradiction (since := "2022-07-15")]
-def contradiction (mvarId : MVarId) (config : Contradiction.Config := {}) : MetaM Unit :=
-  mvarId.contradiction config
-
 builtin_initialize registerTraceClass `Meta.Tactic.contradiction
 
 end Lean.Meta

src/Lean/Meta/Tactic/Delta.lean

@@ -32,10 +32,6 @@ def _root_.Lean.MVarId.deltaTarget (mvarId : MVarId) (p : Name → Bool) : MetaM
     mvarId.checkNotAssigned `delta
     mvarId.change (← deltaExpand (← mvarId.getType) p) (checkDefEq := false)
 
-@[deprecated MVarId.deltaTarget (since := "2022-07-15")]
-def deltaTarget (mvarId : MVarId) (p : Name → Bool) : MetaM MVarId :=
-  mvarId.deltaTarget p
-
 /--
 Delta expand declarations that satisfy `p` at `fvarId` type.
 -/
@@ -44,8 +40,4 @@ def _root_.Lean.MVarId.deltaLocalDecl (mvarId : MVarId) (fvarId : FVarId) (p : N
     mvarId.checkNotAssigned `delta
     mvarId.changeLocalDecl fvarId (← deltaExpand (← mvarId.getType) p) (checkDefEq := false)
 
-@[deprecated MVarId.deltaLocalDecl (since := "2022-07-15")]
-def deltaLocalDecl (mvarId : MVarId) (fvarId : FVarId) (p : Name → Bool) : MetaM MVarId :=
-  mvarId.deltaLocalDecl fvarId p
-
 end Lean.Meta

src/Lean/Meta/Tactic/Generalize.lean

@@ -125,11 +125,6 @@ def _root_.Lean.MVarId.generalize (mvarId : MVarId) (args : Array GeneralizeArg)
     (transparency := TransparencyMode.instances) : MetaM (Array FVarId × MVarId) :=
   generalizeCore mvarId args transparency
 
-@[inherit_doc generalizeCore, deprecated MVarId.generalize (since := "2022-07-15")]
-def generalize (mvarId : MVarId) (args : Array GeneralizeArg)
-    (transparency := TransparencyMode.instances) : MetaM (Array FVarId × MVarId) :=
-  generalizeCore mvarId args transparency
-
 /--
 Extension of `generalize` to support generalizing within specified hypotheses.
 The `hyps` array contains the list of hypotheses within which to look for occurrences

src/Lean/Meta/Tactic/Induction.lean

@@ -229,10 +229,6 @@ def _root_.Lean.MVarId.induction (mvarId : MVarId) (majorFVarId : FVarId) (recur
         let recursor ← mkRecursorAppPrefix mvarId `induction majorFVarId recursorInfo indices
         finalize mvarId givenNames recursorInfo reverted major indices baseSubst recursor
 
-@[deprecated MVarId.induction (since := "2022-07-15")]
-def induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (givenNames : Array AltVarNames := #[]) : MetaM (Array InductionSubgoal) :=
-  mvarId.induction majorFVarId recursorName givenNames
-
 builtin_initialize registerTraceClass `Meta.Tactic.induction
 
 end Lean.Meta

src/Lean/Meta/Tactic/Intro.lean

@@ -132,10 +132,6 @@ Introduce `n` binders in the goal `mvarId`.
 abbrev _root_.Lean.MVarId.introN (mvarId : MVarId) (n : Nat) (givenNames : List Name := []) (useNamesForExplicitOnly := false) : MetaM (Array FVarId × MVarId) :=
   introNCore mvarId n givenNames (useNamesForExplicitOnly := useNamesForExplicitOnly) (preserveBinderNames := false)
 
-@[deprecated MVarId.introN (since := "2022-07-15")]
-abbrev introN (mvarId : MVarId) (n : Nat) (givenNames : List Name := []) (useNamesForExplicitOnly := false) : MetaM (Array FVarId × MVarId) :=
-  mvarId.introN n givenNames useNamesForExplicitOnly
-
 /--
 Introduce `n` binders in the goal `mvarId`. The new hypotheses are named using the binder names.
 The suffix `P` stands for "preserving`.
@@ -143,10 +139,6 @@ The suffix `P` stands for "preserving`.
 abbrev _root_.Lean.MVarId.introNP (mvarId : MVarId) (n : Nat) : MetaM (Array FVarId × MVarId) :=
   introNCore mvarId n [] (useNamesForExplicitOnly := false) (preserveBinderNames := true)
 
-@[deprecated MVarId.introNP (since := "2022-07-15")]
-abbrev introNP (mvarId : MVarId) (n : Nat) : MetaM (Array FVarId × MVarId) :=
-  mvarId.introNP n
-
 /--
 Introduce one binder using `name` as the the new hypothesis name.
 -/
@@ -154,10 +146,6 @@ def _root_.Lean.MVarId.intro (mvarId : MVarId) (name : Name) : MetaM (FVarId ×
   let (fvarIds, mvarId) ← mvarId.introN 1 [name]
   return (fvarIds[0]!, mvarId)
 
-@[deprecated MVarId.intro (since := "2022-07-15")]
-def intro (mvarId : MVarId) (name : Name) : MetaM (FVarId × MVarId) := do
-  mvarId.intro name
-
 def intro1Core (mvarId : MVarId) (preserveBinderNames : Bool) : MetaM (FVarId × MVarId) := do
   let (fvarIds, mvarId) ← introNCore mvarId 1 [] (useNamesForExplicitOnly := false) preserveBinderNames
   return (fvarIds[0]!, mvarId)
@@ -169,10 +157,6 @@ does not start with a forall, lambda or let. -/
 abbrev _root_.Lean.MVarId.intro1 (mvarId : MVarId) : MetaM (FVarId × MVarId) :=
   intro1Core mvarId false
 
-@[deprecated MVarId.intro1 (since := "2022-07-15")]
-abbrev intro1 (mvarId : MVarId) : MetaM (FVarId × MVarId) :=
-  mvarId.intro1
-
 /-- Introduce one object from the goal `mvarid`, preserving the name used in the binder.
 Returns a pair made of the newly introduced variable and the new goal.
 This will fail if there is nothing to introduce, ie when the goal
@@ -180,10 +164,6 @@ does not start with a forall, lambda or let. -/
 abbrev _root_.Lean.MVarId.intro1P (mvarId : MVarId) : MetaM (FVarId × MVarId) :=
   intro1Core mvarId true
 
-@[deprecated MVarId.intro1P (since := "2022-07-15")]
-abbrev intro1P (mvarId : MVarId) : MetaM (FVarId × MVarId) :=
-  mvarId.intro1P
-
 private partial def getIntrosSize : Expr → Nat
   | .forallE _ _ b _ => getIntrosSize b + 1
   | .letE _ _ _ b _  => getIntrosSize b + 1
@@ -206,8 +186,4 @@ def _root_.Lean.MVarId.intros (mvarId : MVarId) : MetaM (Array FVarId × MVarId)
   else
     mvarId.introN n
 
-@[deprecated MVarId.intros (since := "2022-07-15")]
-def intros (mvarId : MVarId) : MetaM (Array FVarId × MVarId) := do
-  mvarId.intros
-
 end Lean.Meta