further cleanup

This PR adds documentation to builtin attributes like `@[refl]` or
`@[implemented_by]`.

Closes #8432

---------

Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Co-authored-by: David Thrane Christiansen <david@lean-fro.org>

.github/workflows/ci.yml

@@ -364,7 +364,7 @@ jobs:
         with:
           path: artifacts
       - name: Release
-        uses: softprops/action-gh-release@v2
+        uses: softprops/action-gh-release@da05d552573ad5aba039eaac05058a918a7bf631
         with:
           files: artifacts/*/*
           fail_on_unmatched_files: true
@@ -408,7 +408,7 @@ jobs:
           echo -e "\n*Full commit log*\n" >> diff.md
           git log --oneline "$last_tag"..HEAD | sed 's/^/* /' >> diff.md
       - name: Release Nightly
-        uses: softprops/action-gh-release@v2
+        uses: softprops/action-gh-release@da05d552573ad5aba039eaac05058a918a7bf631
         with:
           body_path: diff.md
           prerelease: true

.github/workflows/pr-release.yml

@@ -48,19 +48,30 @@ jobs:
           git -C lean4.git remote add origin https://github.com/${{ github.repository_owner }}/lean4.git
           git -C lean4.git fetch -n origin master
           git -C lean4.git fetch -n origin "${{ steps.workflow-info.outputs.sourceHeadSha }}"
+          
+          # Create both the original tag and the SHA-suffixed tag
+          SHORT_SHA="${{ steps.workflow-info.outputs.sourceHeadSha }}"
+          SHORT_SHA="${SHORT_SHA:0:7}"
+          
+          # Export the short SHA for use in subsequent steps
+          echo "SHORT_SHA=${SHORT_SHA}" >> "$GITHUB_ENV"
+
           git -C lean4.git tag -f pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} "${{ steps.workflow-info.outputs.sourceHeadSha }}"
+          git -C lean4.git tag -f pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-"${SHORT_SHA}" "${{ steps.workflow-info.outputs.sourceHeadSha }}"
+          
           git -C lean4.git remote add pr-releases https://foo:'${{ secrets.PR_RELEASES_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-pr-releases.git
           git -C lean4.git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}
+          git -C lean4.git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-"${SHORT_SHA}"
       - name: Delete existing release if present
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         run: |
-          # Try to delete any existing release for the current PR.
+          # Try to delete any existing release for the current PR (just the version without the SHA suffix).
           gh release delete --repo ${{ github.repository_owner }}/lean4-pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} -y || true
         env:
           GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
-      - name: Release
+      - name: Release (short format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: softprops/action-gh-release@v2
+        uses: softprops/action-gh-release@da05d552573ad5aba039eaac05058a918a7bf631
         with:
           name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }}
           # There are coredumps files here as well, but all in deeper subdirectories.
@@ -73,7 +84,22 @@ jobs:
           # The token used here must have `workflow` privileges.
           GITHUB_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
 
-      - name: Report release status
+      - name: Release (SHA-suffixed format)
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
+        uses: softprops/action-gh-release@da05d552573ad5aba039eaac05058a918a7bf631
+        with:
+          name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }} (${{ steps.workflow-info.outputs.sourceHeadSha }})
+          # There are coredumps files here as well, but all in deeper subdirectories.
+          files: artifacts/*/*
+          fail_on_unmatched_files: true
+          draft: false
+          tag_name: pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}
+          repository: ${{ github.repository_owner }}/lean4-pr-releases
+        env:
+          # The token used here must have `workflow` privileges.
+          GITHUB_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
+
+      - name: Report release status (short format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         uses: actions/github-script@v7
         with:
@@ -87,6 +113,20 @@ jobs:
               description: "${{ github.repository_owner }}/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}",
             });
 
+      - name: Report release status (SHA-suffixed format)
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
+        uses: actions/github-script@v7
+        with:
+          script: |
+            await github.rest.repos.createCommitStatus({
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              sha: "${{ steps.workflow-info.outputs.sourceHeadSha }}",
+              state: "success",
+              context: "PR toolchain (SHA-suffixed)",
+              description: "${{ github.repository_owner }}/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}",
+            });
+
       - name: Add label
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         uses: actions/github-script@v7
@@ -282,16 +322,18 @@ jobs:
           if [ "$EXISTS" = "0" ]; then
             echo "Branch does not exist, creating it."
             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
+            echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain
             git add lean-toolchain
             git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
           else
-            echo "Branch already exists, pushing an empty commit."
+            echo "Branch already exists, updating lean-toolchain."
             git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
             # The Batteries `nightly-testing` or `nightly-testing-YYYY-MM-DD` branch may have moved since this branch was created, so merge their changes.
             # (This should no longer be possible once `nightly-testing-YYYY-MM-DD` is a tag, but it is still safe to merge.)
             git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories
-            git commit --allow-empty -m "Trigger CI for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
+            echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain
+            git add lean-toolchain
+            git commit -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
           fi
 
       - name: Push changes
@@ -346,21 +388,23 @@ jobs:
           if [ "$EXISTS" = "0" ]; then
             echo "Branch does not exist, creating it."
             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
+            echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain
             git add lean-toolchain
             sed -i 's,require "leanprover-community" / "batteries" @ git ".\+",require "leanprover-community" / "batteries" @ git "lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}",' lakefile.lean
             lake update batteries
             git add lakefile.lean lake-manifest.json
             git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
           else
-            echo "Branch already exists, merging $BASE and bumping Batteries."
+            echo "Branch already exists, updating lean-toolchain and bumping Batteries."
             git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
             # The Mathlib `nightly-testing` branch or `nightly-testing-YYYY-MM-DD` tag may have moved since this branch was created, so merge their changes.
             # (This should no longer be possible once `nightly-testing-YYYY-MM-DD` is a tag, but it is still safe to merge.)
             git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories
+            echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain
+            git add lean-toolchain
             lake update batteries
             git add lake-manifest.json
-            git commit --allow-empty -m "Trigger CI for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
+            git commit -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
           fi
 
       - name: Push changes

doc/dev/release_checklist.md

@@ -50,7 +50,7 @@ We'll use `v4.6.0` as the intended release version as a running example.
     - Re-running `script/release_checklist.py` will then create the tag `v4.6.0` from `master`/`main` and push it (unless `toolchain-tag: false` in the `release_repos.yml` file)
     - `script/release_checklist.py` will then merge the tag `v4.6.0` into the `stable` branch and push it (unless `stable-branch: false` in the `release_repos.yml` file).
   - Special notes on repositories with exceptional requirements:
-    - `doc-gen4` has addition dependencies which we do not update at each toolchain release, although occasionally these break and need to be updated manually.
+    - `doc-gen4` has additional dependencies which we do not update at each toolchain release, although occasionally these break and need to be updated manually.
     - `verso`:
       - The `subverso` dependency is unusual in that it needs to be compatible with _every_ Lean release simultaneously.
         Usually you don't need to do anything.
@@ -94,6 +94,8 @@ We'll use `v4.6.0` as the intended release version as a running example.
 
 This checklist walks you through creating the first release candidate for a version of Lean.
 
+For subsequent release candidates, the process is essentially the same, but we start out with the `releases/v4.7.0` branch already created.
+
 We'll use `v4.7.0-rc1` as the intended release version in this example.
 
 - Decide which nightly release you want to turn into a release candidate.
@@ -112,7 +114,7 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
     git fetch nightly tag nightly-2024-02-29
     git checkout nightly-2024-02-29
     git checkout -b releases/v4.7.0
-    git push --set-upstream origin releases/v4.18.0
+    git push --set-upstream origin releases/v4.7.0
     ```
 - In `src/CMakeLists.txt`,
   - verify that you see `set(LEAN_VERSION_MINOR 7)` (for whichever `7` is appropriate); this should already have been updated when the development cycle began.

script/release_checklist.py

@@ -53,6 +53,23 @@ def tag_exists(repo_url, tag_name, github_token):
     matching_tags = response.json()
     return any(tag["ref"] == f"refs/tags/{tag_name}" for tag in matching_tags)
 
+def commit_hash_for_tag(repo_url, tag_name, github_token):
+    # Use /git/matching-refs/tags/ to get all matching tags
+    api_url = repo_url.replace("https://github.com/", "https://api.github.com/repos/") + f"/git/matching-refs/tags/{tag_name}"
+    headers = {'Authorization': f'token {github_token}'} if github_token else {}
+    response = requests.get(api_url, headers=headers)
+
+    if response.status_code != 200:
+        return False
+
+    # Check if any of the returned refs exactly match our tag
+    matching_tags = response.json()
+    matching_commits = [tag["object"]["sha"] for tag in matching_tags if tag["ref"] == f"refs/tags/{tag_name}"]
+    if len(matching_commits) != 1:
+        return None
+    else:
+        return matching_commits[0]
+
 def release_page_exists(repo_url, tag_name, github_token):
     api_url = repo_url.replace("https://github.com/", "https://api.github.com/repos/") + f"/releases/tags/{tag_name}"
     headers = {'Authorization': f'token {github_token}'} if github_token else {}
@@ -286,6 +303,14 @@ def main():
         lean4_success = False
     else:
         print(f"  ✅ Tag {toolchain} exists")
+        commit_hash = commit_hash_for_tag(lean_repo_url, toolchain, github_token)
+        SHORT_HASH_LENGTH = 7 # Lake abbreviates the Lean commit to 7 characters.
+        if commit_hash is None:
+            print(f"  ❌ Could not resolve tag {toolchain} to a commit.")
+            lean4_success = False
+        elif commit_hash[0] == '0' and commit_hash[:SHORT_HASH_LENGTH].isnumeric():
+            print(f"  ❌ Short commit hash {commit_hash[:SHORT_HASH_LENGTH]} is numeric and starts with 0, causing issues for version parsing. Try regenerating the last commit to get a new hash.")
+            lean4_success = False
 
     if not release_page_exists(lean_repo_url, toolchain, github_token):
         print(f"  ❌ Release page for {toolchain} does not exist")

script/release_steps.py

@@ -94,6 +94,7 @@ def generate_script(repo, version, config):
             "echo 'This repo has nightly-testing infrastructure'",
             f"git merge origin/bump/{version.split('-rc')[0]}",
             "echo 'Please resolve any conflicts.'",
+            "grep nightly-testing lakefile.* && echo 'Please ensure the lakefile does not include nightly-testing versions.'",
             ""
         ])
     if re.search(r'rc\d+$', version) and repo_name in ["verso", "reference-manual"]:

src/CMakeLists.txt

@@ -10,7 +10,7 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 21)
+set(LEAN_VERSION_MINOR 22)
 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'")

src/Init/Data/Array/Find.lean

@@ -59,10 +59,10 @@ theorem findSome?_eq_some_iff {f : α → Option β} {xs : Array α} {b : β} :
   · rintro ⟨xs, a, ys, h₀, h₁, h₂⟩
     exact ⟨xs.toList, a, ys.toList, by simpa using congrArg toList h₀, h₁, by simpa⟩
 
-@[simp] theorem findSome?_guard {xs : Array α} : findSome? (Option.guard fun x => p x) xs = find? p xs := by
+@[simp] theorem findSome?_guard {xs : Array α} : findSome? (Option.guard p) xs = find? p xs := by
   cases xs; simp
 
-theorem find?_eq_findSome?_guard {xs : Array α} : find? p xs = findSome? (Option.guard fun x => p x) xs :=
+theorem find?_eq_findSome?_guard {xs : Array α} : find? p xs = findSome? (Option.guard p) xs :=
   findSome?_guard.symm
 
 @[simp] theorem getElem?_zero_filterMap {f : α → Option β} {xs : Array α} : (xs.filterMap f)[0]? = xs.findSome? f := by
@@ -231,7 +231,7 @@ theorem get_find?_mem {xs : Array α} (h) : (xs.find? p).get h ∈ xs := by
   simp
 
 @[simp] theorem find?_flatten {xss : Array (Array α)} {p : α → Bool} :
-    xss.flatten.find? p = xss.findSome? (·.find? p) := by
+    xss.flatten.find? p = xss.findSome? (find? p) := by
   cases xss using array₂_induction
   simp [List.findSome?_map, Function.comp_def]
 
@@ -743,13 +743,15 @@ theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by sim
   simp [List.finIdxOf?_eq_some_iff]
 
 @[simp]
-theorem isSome_finIdxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
-    (xs.finIdxOf? a).isSome ↔ a ∈ xs := by
+theorem isSome_finIdxOf? [BEq α] [PartialEquivBEq α] {xs : Array α} {a : α} :
+    (xs.finIdxOf? a).isSome = xs.contains a := by
   rcases xs with ⟨xs⟩
   simp [Array.size]
 
-theorem isNone_finIdxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
-    (xs.finIdxOf? a).isNone = ¬ a ∈ xs := by
-  simp
+@[simp]
+theorem isNone_finIdxOf? [BEq α] [PartialEquivBEq α] {xs : Array α} {a : α} :
+    (xs.finIdxOf? a).isNone = !xs.contains a := by
+  rcases xs with ⟨xs⟩
+  simp [Array.size]
 
 end Array

src/Init/Data/Array/Lemmas.lean

@@ -133,7 +133,6 @@ grind_pattern Array.getElem?_eq_none => xs.size ≤ i, xs[i]?
 theorem getElem?_eq_some_iff {xs : Array α} : xs[i]? = some b ↔ ∃ h : i < xs.size, xs[i] = b :=
   _root_.getElem?_eq_some_iff
 
-@[grind →]
 theorem getElem_of_getElem? {xs : Array α} : xs[i]? = some a → ∃ h : i < xs.size, xs[i] = a :=
   getElem?_eq_some_iff.mp
 
@@ -3622,8 +3621,8 @@ We can prove that two folds over the same array are related (by some arbitrary r
 if we know that the initial elements are related and the folding function, for each element of the array,
 preserves the relation.
 -/
-theorem foldl_rel {xs : Array α} {f g : β → α → β} {a b : β} {r : β → β → Prop}
-    (h : r a b) (h' : ∀ (a : α), a ∈ xs → ∀ (c c' : β), r c c' → r (f c a) (g c' a)) :
+theorem foldl_rel {xs : Array α} {f : β → α → β} {g : γ → α → γ} {a : β} {b : γ} {r : β → γ → Prop}
+    (h : r a b) (h' : ∀ (a : α), a ∈ xs → ∀ (c : β) (c' : γ), r c c' → r (f c a) (g c' a)) :
     r (xs.foldl (fun acc a => f acc a) a) (xs.foldl (fun acc a => g acc a) b) := by
   rcases xs with ⟨xs⟩
   simpa using List.foldl_rel h (by simpa using h')
@@ -3633,8 +3632,8 @@ We can prove that two folds over the same array are related (by some arbitrary r
 if we know that the initial elements are related and the folding function, for each element of the array,
 preserves the relation.
 -/
-theorem foldr_rel {xs : Array α} {f g : α → β → β} {a b : β} {r : β → β → Prop}
-    (h : r a b) (h' : ∀ (a : α), a ∈ xs → ∀ (c c' : β), r c c' → r (f a c) (g a c')) :
+theorem foldr_rel {xs : Array α} {f : α → β → β} {g : α → γ → γ} {a : β} {b : γ} {r : β → γ → Prop}
+    (h : r a b) (h' : ∀ (a : α), a ∈ xs → ∀ (c : β) (c' : γ), r c c' → r (f a c) (g a c')) :
     r (xs.foldr (fun a acc => f a acc) a) (xs.foldr (fun a acc => g a acc) b) := by
   rcases xs with ⟨xs⟩
   simpa using List.foldr_rel h (by simpa using h')

src/Init/Data/BitVec/Lemmas.lean

@@ -319,6 +319,7 @@ theorem ofFin_ofNat (n : Nat) :
 @[simp] theorem ofFin_neg {x : Fin (2 ^ w)} : ofFin (-x) = -(ofFin x) := by
   rfl
 
+open Fin.NatCast in
 @[simp, norm_cast] theorem ofFin_natCast (n : Nat) : ofFin (n : Fin (2^w)) = (n : BitVec w) := by
   rfl
 
@@ -337,6 +338,7 @@ theorem toFin_zero : toFin (0 : BitVec w) = 0 := rfl
 theorem toFin_one  : toFin (1 : BitVec w) = 1 := by
   rw [toFin_inj]; simp only [ofNat_eq_ofNat, ofFin_ofNat]
 
+open Fin.NatCast in
 @[simp, norm_cast] theorem toFin_natCast (n : Nat) : toFin (n : BitVec w) = (n : Fin (2^w)) := by
   rfl
 
@@ -880,6 +882,19 @@ theorem slt_eq_sle_and_ne {x y : BitVec w} : x.slt y = (x.sle y && x != y) := by
   apply Bool.eq_iff_iff.2
   simp [BitVec.slt, BitVec.sle, Int.lt_iff_le_and_ne, BitVec.toInt_inj]
 
+/-- For all bitvectors `x, y`, either `x` is signed less than `y`,
+or is equal to `y`, or is signed greater than `y`. -/
+theorem slt_trichotomy (x y : BitVec w) : x.slt y ∨ x = y ∨ y.slt x := by
+  simpa [slt_iff_toInt_lt, ← toInt_inj]
+    using Int.lt_trichotomy x.toInt y.toInt
+
+/-- For all bitvectors `x, y`, either `x` is unsigned less than `y`,
+or is equal to `y`, or is unsigned greater than `y`. -/
+theorem lt_trichotomy (x y : BitVec w) :
+    x < y ∨ x = y ∨ y < x := by
+  simpa [← ult_iff_lt, ult_eq_decide, decide_eq_true_eq, ← toNat_inj]
+    using Nat.lt_trichotomy x.toNat y.toNat
+
 /-! ### setWidth, zeroExtend and truncate -/
 
 @[simp]

src/Init/Data/Fin/Fold.lean

@@ -183,10 +183,7 @@ theorem foldrM_loop [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x
   | zero =>
     rw [foldrM_loop_zero, foldrM_loop_succ, pure_bind]
     conv => rhs; rw [←bind_pure (f 0 x)]
-    congr
-    try  -- TODO: block can be deleted after bootstrapping
-      funext
-      simp [foldrM_loop_zero]
+    rfl
   | succ i ih =>
     rw [foldrM_loop_succ, foldrM_loop_succ, bind_assoc]
     congr; funext; exact ih ..

src/Init/Data/Fin/Lemmas.lean

@@ -102,9 +102,30 @@ theorem dite_val {n : Nat} {c : Prop} [Decidable c] {x y : Fin n} :
     (if c then x else y).val = if c then x.val else y.val := by
   by_cases c <;> simp [*]
 
-instance (n : Nat) [NeZero n] : NatCast (Fin n) where
+namespace NatCast
+
+/--
+This is not a global instance, but may be activated locally via `open Fin.NatCast in ...`.
+
+This is not an instance because the `binop%` elaborator assumes that
+there are no non-trivial coercion loops,
+but this introduces a coercion from `Nat` to `Fin n` and back.
+
+Non-trivial loops lead to undesirable and counterintuitive elaboration behavior.
+For example, for `x : Fin k` and `n : Nat`,
+it causes `x < n` to be elaborated as `x < ↑n` rather than `↑x < n`,
+silently introducing wraparound arithmetic.
+
+Note: as of 2025-06-03, Mathlib has such a coercion for `Fin n` anyway!
+-/
+@[expose]
+def instNatCast (n : Nat) [NeZero n] : NatCast (Fin n) where
   natCast a := Fin.ofNat n a
 
+attribute [scoped instance] instNatCast
+
+end NatCast
+
 @[expose]
 def intCast [NeZero n] (a : Int) : Fin n :=
   if 0 ≤ a then
@@ -112,9 +133,22 @@ def intCast [NeZero n] (a : Int) : Fin n :=
   else
     - Fin.ofNat n a.natAbs
 
-instance (n : Nat) [NeZero n] : IntCast (Fin n) where
+namespace IntCast
+
+/--
+This is not a global instance, but may be activated locally via `open Fin.IntCast in ...`.
+
+See the doc-string for `Fin.NatCast.instNatCast` for more details.
+-/
+@[expose]
+def instIntCast (n : Nat) [NeZero n] : IntCast (Fin n) where
   intCast := Fin.intCast
 
+attribute [scoped instance] instIntCast
+
+end IntCast
+
+open IntCast in
 theorem intCast_def {n : Nat} [NeZero n] (x : Int) :
     (x : Fin n) = if 0 ≤ x then Fin.ofNat n x.natAbs else -Fin.ofNat n x.natAbs := rfl
 
@@ -1045,6 +1079,17 @@ theorem val_neg {n : Nat} [NeZero n] (x : Fin n) :
     have := Fin.val_ne_zero_iff.mpr h
     omega
 
+protected theorem sub_eq_add_neg {n : Nat} (x y : Fin n) : x - y = x + -y := by
+  by_cases h : n = 0
+  · subst h
+    apply elim0 x
+  · replace h : NeZero n := ⟨h⟩
+    ext
+    rw [Fin.coe_sub, Fin.val_add, val_neg]
+    split
+    · simp_all
+    · simp [Nat.add_comm]
+
 /-! ### mul -/
 
 theorem ofNat_mul [NeZero n] (x : Nat) (y : Fin n) :

src/Init/Data/Int/DivMod/Lemmas.lean

@@ -203,6 +203,9 @@ theorem tdiv_eq_ediv_of_nonneg : ∀ {a b : Int}, 0 ≤ a → a.tdiv b = a / b
   | succ _, succ _, _ => rfl
   | succ _, -[_+1], _ => rfl
 
+@[simp] theorem natCast_tdiv_eq_ediv {a : Nat} {b : Int} : (a : Int).tdiv b = a / b :=
+    tdiv_eq_ediv_of_nonneg (by simp)
+
 theorem tdiv_eq_ediv {a b : Int} :
     a.tdiv b = a / b + if 0 ≤ a ∨ b ∣ a then 0 else sign b := by
   simp only [dvd_iff_emod_eq_zero]

src/Init/Data/List/Basic.lean

@@ -1624,8 +1624,8 @@ def find? (p : α → Bool) : List α → Option α
     | true  => some a
     | false => find? p as
 
-@[simp] theorem find?_nil : ([] : List α).find? p = none := rfl
-theorem find?_cons : (a::as).find? p = match p a with | true => some a | false => as.find? p :=
+@[simp, grind =] theorem find?_nil : ([] : List α).find? p = none := rfl
+@[grind =]theorem find?_cons : (a::as).find? p = match p a with | true => some a | false => as.find? p :=
   rfl
 
 /-! ### findSome? -/

src/Init/Data/List/Find.lean

@@ -45,7 +45,7 @@ theorem exists_of_findSome?_eq_some {l : List α} {f : α → Option β} (w : l.
     simp_all only [findSome?_cons, mem_cons, exists_eq_or_imp]
     split at w <;> simp_all
 
-@[simp] theorem findSome?_eq_none_iff : findSome? p l = none ↔ ∀ x ∈ l, p x = none := by
+@[simp, grind =] theorem findSome?_eq_none_iff : findSome? p l = none ↔ ∀ x ∈ l, p x = none := by
   induction l <;> simp [findSome?_cons]; split <;> simp [*]
 
 @[simp] theorem findSome?_isSome_iff {f : α → Option β} {l : List α} :
@@ -91,7 +91,7 @@ theorem findSome?_eq_some_iff {f : α → Option β} {l : List α} {b : β} :
           obtain ⟨⟨rfl, rfl⟩, rfl⟩ := h₁
           exact ⟨l₁, a, l₂, rfl, h₂, fun a' w => h₃ a' (mem_cons_of_mem p w)⟩
 
-@[simp] theorem findSome?_guard {l : List α} : findSome? (Option.guard fun x => p x) l = find? p l := by
+@[simp, grind =] theorem findSome?_guard {l : List α} : findSome? (Option.guard p) l = find? p l := by
   induction l with
   | nil => simp
   | cons x xs ih =>
@@ -103,32 +103,33 @@ theorem findSome?_eq_some_iff {f : α → Option β} {l : List α} {b : β} :
     · simp only [Option.guard_eq_none_iff] at h
       simp [ih, h]
 
-theorem find?_eq_findSome?_guard {l : List α} : find? p l = findSome? (Option.guard fun x => p x) l :=
+theorem find?_eq_findSome?_guard {l : List α} : find? p l = findSome? (Option.guard p) l :=
   findSome?_guard.symm
 
-@[simp] theorem head?_filterMap {f : α → Option β} {l : List α} : (l.filterMap f).head? = l.findSome? f := by
+@[simp, grind =] theorem head?_filterMap {f : α → Option β} {l : List α} : (l.filterMap f).head? = l.findSome? f := by
   induction l with
   | nil => simp
   | cons x xs ih =>
     simp only [filterMap_cons, findSome?_cons]
     split <;> simp [*]
 
-@[simp] theorem head_filterMap {f : α → Option β} {l : List α} (h) :
+@[simp, grind =] theorem head_filterMap {f : α → Option β} {l : List α} (h) :
     (l.filterMap f).head h = (l.findSome? f).get (by simp_all [Option.isSome_iff_ne_none]) := by
   simp [head_eq_iff_head?_eq_some]
 
-@[simp] theorem getLast?_filterMap {f : α → Option β} {l : List α} : (l.filterMap f).getLast? = l.reverse.findSome? f := by
+@[simp, grind =] theorem getLast?_filterMap {f : α → Option β} {l : List α} : (l.filterMap f).getLast? = l.reverse.findSome? f := by
   rw [getLast?_eq_head?_reverse]
   simp [← filterMap_reverse]
 
-@[simp] theorem getLast_filterMap {f : α → Option β} {l : List α} (h) :
+@[simp, grind =] theorem getLast_filterMap {f : α → Option β} {l : List α} (h) :
     (l.filterMap f).getLast h = (l.reverse.findSome? f).get (by simp_all [Option.isSome_iff_ne_none]) := by
   simp [getLast_eq_iff_getLast?_eq_some]
 
-@[simp] theorem map_findSome? {f : α → Option β} {g : β → γ} {l : List α} :
+@[simp, grind _=_] theorem map_findSome? {f : α → Option β} {g : β → γ} {l : List α} :
     (l.findSome? f).map g = l.findSome? (Option.map g ∘ f) := by
   induction l <;> simp [findSome?_cons]; split <;> simp [*]
 
+@[grind _=_]
 theorem findSome?_map {f : β → γ} {l : List β} : findSome? p (l.map f) = l.findSome? (p ∘ f) := by
   induction l with
   | nil => simp
@@ -136,15 +137,18 @@ theorem findSome?_map {f : β → γ} {l : List β} : findSome? p (l.map f) = l.
     simp only [map_cons, findSome?]
     split <;> simp_all
 
+@[grind =]
 theorem head_flatten {L : List (List α)} (h : ∃ l, l ∈ L ∧ l ≠ []) :
-    (flatten L).head (by simpa using h) = (L.findSome? fun l => l.head?).get (by simpa using h) := by
+    (flatten L).head (by simpa using h) = (L.findSome? head?).get (by simpa using h) := by
   simp [head_eq_iff_head?_eq_some, head?_flatten]
 
+@[grind =]
 theorem getLast_flatten {L : List (List α)} (h : ∃ l, l ∈ L ∧ l ≠ []) :
     (flatten L).getLast (by simpa using h) =
-      (L.reverse.findSome? fun l => l.getLast?).get (by simpa using h) := by
+      (L.reverse.findSome? getLast?).get (by simpa using h) := by
   simp [getLast_eq_iff_getLast?_eq_some, getLast?_flatten]
 
+@[grind =]
 theorem findSome?_replicate : findSome? f (replicate n a) = if n = 0 then none else f a := by
   cases n with
   | zero => simp
@@ -174,6 +178,9 @@ theorem Sublist.findSome?_isSome {l₁ l₂ : List α} (h : l₁ <+ l₂) :
     · simp_all
     · exact ih
 
+grind_pattern Sublist.findSome?_isSome => l₁ <+ l₂, l₁.findSome? f
+grind_pattern Sublist.findSome?_isSome => l₁ <+ l₂, l₂.findSome? f
+
 theorem Sublist.findSome?_eq_none {l₁ l₂ : List α} (h : l₁ <+ l₂) :
     l₂.findSome? f = none → l₁.findSome? f = none := by
   simp only [List.findSome?_eq_none_iff, Bool.not_eq_true]
@@ -185,16 +192,30 @@ theorem IsPrefix.findSome?_eq_some {l₁ l₂ : List α} {f : α → Option β}
   obtain ⟨t, rfl⟩ := h
   simp +contextual [findSome?_append]
 
+grind_pattern IsPrefix.findSome?_eq_some => l₁ <+: l₂, l₁.findSome? f, some b
+grind_pattern IsPrefix.findSome?_eq_some => l₁ <+: l₂, l₂.findSome? f, some b
+
 theorem IsPrefix.findSome?_eq_none {l₁ l₂ : List α} {f : α → Option β} (h : l₁ <+: l₂) :
     List.findSome? f l₂ = none → List.findSome? f l₁ = none :=
   h.sublist.findSome?_eq_none
+
+grind_pattern IsPrefix.findSome?_eq_none => l₁ <+: l₂, l₂.findSome? f
+grind_pattern IsPrefix.findSome?_eq_none => l₁ <+: l₂, l₁.findSome? f
+
 theorem IsSuffix.findSome?_eq_none {l₁ l₂ : List α} {f : α → Option β} (h : l₁ <:+ l₂) :
     List.findSome? f l₂ = none → List.findSome? f l₁ = none :=
   h.sublist.findSome?_eq_none
+
+grind_pattern IsSuffix.findSome?_eq_none => l₁ <+: l₂, l₂.findSome? f
+grind_pattern IsSuffix.findSome?_eq_none => l₁ <+: l₂, l₁.findSome? f
+
 theorem IsInfix.findSome?_eq_none {l₁ l₂ : List α} {f : α → Option β} (h : l₁ <:+: l₂) :
     List.findSome? f l₂ = none → List.findSome? f l₁ = none :=
   h.sublist.findSome?_eq_none
 
+grind_pattern IsInfix.findSome?_eq_none => l₁ <+: l₂, l₂.findSome? f
+grind_pattern IsInfix.findSome?_eq_none => l₁ <+: l₂, l₁.findSome? f
+
 /-! ### find? -/
 
 @[simp] theorem find?_cons_of_pos {l} (h : p a) : find? p (a :: l) = some a := by
@@ -203,7 +224,7 @@ theorem IsInfix.findSome?_eq_none {l₁ l₂ : List α} {f : α → Option β} (
 @[simp] theorem find?_cons_of_neg {l} (h : ¬p a) : find? p (a :: l) = find? p l := by
   simp [find?, h]
 
-@[simp] theorem find?_eq_none : find? p l = none ↔ ∀ x ∈ l, ¬ p x := by
+@[simp, grind =] theorem find?_eq_none : find? p l = none ↔ ∀ x ∈ l, ¬ p x := by
   induction l <;> simp [find?_cons]; split <;> simp [*]
 
 theorem find?_eq_some_iff_append :
@@ -255,18 +276,21 @@ theorem find?_cons_eq_some : (a :: xs).find? p = some b ↔ (p a ∧ a = b) ∨
     simp only [find?_cons, mem_cons, exists_eq_or_imp]
     split <;> simp_all
 
+@[grind →]
 theorem find?_some : ∀ {l}, find? p l = some a → p a
   | b :: l, H => by
     by_cases h : p b <;> simp [find?, h] at H
     · exact H ▸ h
     · exact find?_some H
 
+@[grind →]
 theorem mem_of_find?_eq_some : ∀ {l}, find? p l = some a → a ∈ l
   | b :: l, H => by
     by_cases h : p b <;> simp [find?, h] at H
     · exact H ▸ .head _
     · exact .tail _ (mem_of_find?_eq_some H)
 
+@[grind]
 theorem get_find?_mem {xs : List α} {p : α → Bool} (h) : (xs.find? p).get h ∈ xs := by
   induction xs with
   | nil => simp at h
@@ -278,7 +302,7 @@ theorem get_find?_mem {xs : List α} {p : α → Bool} (h) : (xs.find? p).get h
       right
       apply ih
 
-@[simp] theorem find?_filter {xs : List α} {p : α → Bool} {q : α → Bool} :
+@[simp, grind =] theorem find?_filter {xs : List α} {p : α → Bool} {q : α → Bool} :
     (xs.filter p).find? q = xs.find? (fun a => p a ∧ q a) := by
   induction xs with
   | nil => simp
@@ -288,22 +312,22 @@ theorem get_find?_mem {xs : List α} {p : α → Bool} (h) : (xs.find? p).get h
     · simp only [find?_cons]
       split <;> simp_all
 
-@[simp] theorem head?_filter {p : α → Bool} {l : List α} : (l.filter p).head? = l.find? p := by
+@[simp, grind =] theorem head?_filter {p : α → Bool} {l : List α} : (l.filter p).head? = l.find? p := by
   rw [← filterMap_eq_filter, head?_filterMap, findSome?_guard]
 
-@[simp] theorem head_filter {p : α → Bool} {l : List α} (h) :
+@[simp, grind =] theorem head_filter {p : α → Bool} {l : List α} (h) :
     (l.filter p).head h = (l.find? p).get (by simp_all [Option.isSome_iff_ne_none]) := by
   simp [head_eq_iff_head?_eq_some]
 
-@[simp] theorem getLast?_filter {p : α → Bool} {l : List α} : (l.filter p).getLast? = l.reverse.find? p := by
+@[simp, grind =] theorem getLast?_filter {p : α → Bool} {l : List α} : (l.filter p).getLast? = l.reverse.find? p := by
   rw [getLast?_eq_head?_reverse]
   simp [← filter_reverse]
 
-@[simp] theorem getLast_filter {p : α → Bool} {l : List α} (h) :
+@[simp, grind =] theorem getLast_filter {p : α → Bool} {l : List α} (h) :
     (l.filter p).getLast h = (l.reverse.find? p).get (by simp_all [Option.isSome_iff_ne_none]) := by
   simp [getLast_eq_iff_getLast?_eq_some]
 
-@[simp] theorem find?_filterMap {xs : List α} {f : α → Option β} {p : β → Bool} :
+@[simp, grind =] theorem find?_filterMap {xs : List α} {f : α → Option β} {p : β → Bool} :
     (xs.filterMap f).find? p = (xs.find? (fun a => (f a).any p)).bind f := by
   induction xs with
   | nil => simp
@@ -313,15 +337,15 @@ theorem get_find?_mem {xs : List α} {p : α → Bool} (h) : (xs.find? p).get h
     · simp only [find?_cons]
       split <;> simp_all
 
-@[simp] theorem find?_map {f : β → α} {l : List β} : find? p (l.map f) = (l.find? (p ∘ f)).map f := by
+@[simp, grind =] theorem find?_map {f : β → α} {l : List β} : find? p (l.map f) = (l.find? (p ∘ f)).map f := by
   induction l with
   | nil => simp
   | cons x xs ih =>
     simp only [map_cons, find?]
     by_cases h : p (f x) <;> simp [h, ih]
 
-@[simp] theorem find?_flatten {xss : List (List α)} {p : α → Bool} :
-    xss.flatten.find? p = xss.findSome? (·.find? p) := by
+@[simp, grind _=_] theorem find?_flatten {xss : List (List α)} {p : α → Bool} :
+    xss.flatten.find? p = xss.findSome? (find? p) := by
   induction xss with
   | nil => simp
   | cons _ _ ih =>
@@ -378,7 +402,7 @@ theorem find?_flatten_eq_some_iff {xs : List (List α)} {p : α → Bool} {a :
 @[deprecated find?_flatten_eq_some_iff (since := "2025-02-03")]
 abbrev find?_flatten_eq_some := @find?_flatten_eq_some_iff
 
-@[simp] theorem find?_flatMap {xs : List α} {f : α → List β} {p : β → Bool} :
+@[simp, grind =] theorem find?_flatMap {xs : List α} {f : α → List β} {p : β → Bool} :
     (xs.flatMap f).find? p = xs.findSome? (fun x => (f x).find? p) := by
   simp [flatMap_def, findSome?_map]; rfl
 
@@ -386,6 +410,7 @@ theorem find?_flatMap_eq_none_iff {xs : List α} {f : α → List β} {p : β
     (xs.flatMap f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y := by
   simp
 
+@[grind =]
 theorem find?_replicate : find? p (replicate n a) = if n = 0 then none else if p a then some a else none := by
   cases n
   · simp
@@ -430,6 +455,9 @@ theorem Sublist.find?_isSome {l₁ l₂ : List α} (h : l₁ <+ l₂) : (l₁.fi
     · simp
     · simpa using ih
 
+grind_pattern Sublist.find?_isSome => l₁ <+ l₂, l₁.find? p
+grind_pattern Sublist.find?_isSome => l₁ <+ l₂, l₂.find? p
+
 theorem Sublist.find?_eq_none {l₁ l₂ : List α} (h : l₁ <+ l₂) : l₂.find? p = none → l₁.find? p = none := by
   simp only [List.find?_eq_none, Bool.not_eq_true]
   exact fun w x m => w x (Sublist.mem m h)
@@ -440,16 +468,31 @@ theorem IsPrefix.find?_eq_some {l₁ l₂ : List α} {p : α → Bool} (h : l₁
   obtain ⟨t, rfl⟩ := h
   simp +contextual [find?_append]
 
+grind_pattern IsPrefix.find?_eq_some => l₁ <+: l₂, l₁.find? p, some b
+grind_pattern IsPrefix.find?_eq_some => l₁ <+: l₂, l₂.find? p, some b
+
 theorem IsPrefix.find?_eq_none {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂) :
     List.find? p l₂ = none → List.find? p l₁ = none :=
   h.sublist.find?_eq_none
+
+grind_pattern Sublist.find?_eq_none => l₁ <+ l₂, l₂.find? p
+grind_pattern Sublist.find?_eq_none => l₁ <+ l₂, l₁.find? p
+
 theorem IsSuffix.find?_eq_none {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <:+ l₂) :
     List.find? p l₂ = none → List.find? p l₁ = none :=
   h.sublist.find?_eq_none
+
+grind_pattern IsPrefix.find?_eq_none => l₁ <+: l₂, l₂.find? p
+grind_pattern IsPrefix.find?_eq_none => l₁ <+: l₂, l₁.find? p
+
 theorem IsInfix.find?_eq_none {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <:+: l₂) :
     List.find? p l₂ = none → List.find? p l₁ = none :=
   h.sublist.find?_eq_none
 
+grind_pattern IsSuffix.find?_eq_none => l₁ <:+ l₂, l₂.find? p
+grind_pattern IsSuffix.find?_eq_none => l₁ <:+ l₂, l₁.find? p
+
+@[grind =]
 theorem find?_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : List α}
     (H : ∀ (a : α), a ∈ xs → P a) {p : β → Bool} :
     (xs.pmap f H).find? p = (xs.attach.find? (fun ⟨a, m⟩ => p (f a (H a m)))).map fun ⟨a, m⟩ => f a (H a m) := by
@@ -482,9 +525,9 @@ private theorem findIdx?_go_eq {p : α → Bool} {xs : List α} {i : Nat} :
       ext
       simp only [Nat.add_comm i, Function.comp_apply, Nat.add_assoc]
 
-@[simp] theorem findIdx?_nil : ([] : List α).findIdx? p = none := rfl
+@[simp, grind =] theorem findIdx?_nil : ([] : List α).findIdx? p = none := rfl
 
-theorem findIdx?_cons :
+@[grind =] theorem findIdx?_cons :
     (x :: xs).findIdx? p = if p x then some 0 else (xs.findIdx? p).map fun i => i + 1 := by
   simp [findIdx?, findIdx?_go_eq]
 
@@ -493,6 +536,7 @@ theorem findIdx?_cons :
 
 /-! ### findIdx -/
 
+@[grind =]
 theorem findIdx_cons {p : α → Bool} {b : α} {l : List α} :
     (b :: l).findIdx p = bif p b then 0 else (l.findIdx p) + 1 := by
   cases H : p b with
@@ -511,6 +555,7 @@ where
 @[simp] theorem findIdx_singleton {a : α} {p : α → Bool} : [a].findIdx p = if p a then 0 else 1 := by
   simp [findIdx_cons, findIdx_nil]
 
+@[grind →]
 theorem findIdx_of_getElem?_eq_some {xs : List α} (w : xs[xs.findIdx p]? = some y) : p y := by
   induction xs with
   | nil => simp_all
@@ -520,6 +565,8 @@ theorem findIdx_getElem {xs : List α} {w : xs.findIdx p < xs.length} :
     p xs[xs.findIdx p] :=
   xs.findIdx_of_getElem?_eq_some (getElem?_eq_getElem w)
 
+grind_pattern findIdx_getElem => xs[xs.findIdx p]
+
 theorem findIdx_lt_length_of_exists {xs : List α} (h : ∃ x ∈ xs, p x) :
     xs.findIdx p < xs.length := by
   induction xs with
@@ -1097,17 +1144,18 @@ theorem finIdxOf?_cons [BEq α] {a : α} {xs : List α} :
   simp only [finIdxOf?, findFinIdx?_eq_some_iff, beq_iff_eq]
 
 @[simp]
-theorem isSome_finIdxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} :
-    (l.finIdxOf? a).isSome ↔ a ∈ l := by
+theorem isSome_finIdxOf? [BEq α] [PartialEquivBEq α] {l : List α} {a : α} :
+    (l.finIdxOf? a).isSome = l.contains a := by
   induction l with
   | nil => simp
   | cons x xs ih =>
     simp only [finIdxOf?_cons]
-    split <;> simp_all [@eq_comm _ x a]
+    split <;> simp_all [BEq.comm]
 
-theorem isNone_finIdxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} :
-    (l.finIdxOf? a).isNone = ¬ a ∈ l := by
-  simp
+@[simp]
+theorem isNone_finIdxOf? [BEq α] [PartialEquivBEq α] {l : List α} {a : α} :
+    (l.finIdxOf? a).isNone = !l.contains a := by
+  rw [← isSome_finIdxOf?, Option.not_isSome]
 
 /-! ### idxOf?
 

src/Init/Data/List/Lemmas.lean

@@ -2778,8 +2778,8 @@ We can prove that two folds over the same list are related (by some arbitrary re
 if we know that the initial elements are related and the folding function, for each element of the list,
 preserves the relation.
 -/
-theorem foldl_rel {l : List α} {f g : β → α → β} {a b : β} {r : β → β → Prop}
-    (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f c a) (g c' a)) :
+theorem foldl_rel {l : List α} {f : β → α → β} {g : γ → α → γ} {a : β} {b : γ} {r : β → γ → Prop}
+    (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c : β) (c' : γ), r c c' → r (f c a) (g c' a)) :
     r (l.foldl (fun acc a => f acc a) a) (l.foldl (fun acc a => g acc a) b) := by
   induction l generalizing a b with
   | nil => simp_all
@@ -2794,8 +2794,8 @@ We can prove that two folds over the same list are related (by some arbitrary re
 if we know that the initial elements are related and the folding function, for each element of the list,
 preserves the relation.
 -/
-theorem foldr_rel {l : List α} {f g : α → β → β} {a b : β} {r : β → β → Prop}
-    (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f a c) (g a c')) :
+theorem foldr_rel {l : List α} {f : α → β → β} {g : α → γ → γ} {a : β} {b : γ} {r : β → γ → Prop}
+    (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c : β) (c' : γ), r c c' → r (f a c) (g a c')) :
     r (l.foldr (fun a acc => f a acc) a) (l.foldr (fun a acc => g a acc) b) := by
   induction l generalizing a b with
   | nil => simp_all

src/Init/Data/Range/Basic.lean

@@ -85,4 +85,4 @@ theorem Membership.get_elem_helper {i n : Nat} {r : Std.Range} (h₁ : i ∈ r)
     i < n := h₂ ▸ h₁.2.1
 
 macro_rules
-  | `(tactic| get_elem_tactic_trivial) => `(tactic| apply Membership.get_elem_helper; assumption; rfl)
+  | `(tactic| get_elem_tactic_extensible) => `(tactic| apply Membership.get_elem_helper; assumption; rfl)

src/Init/Data/Vector/Find.lean

@@ -72,11 +72,11 @@ theorem findSome?_eq_some_iff {f : α → Option β} {xs : Vector α n} {b : β}
   · rintro ⟨k₁, k₂, h, ys, a, zs, w, h₁, h₂⟩
     exact ⟨ys.toArray, a, zs.toArray, by simp [w], h₁, by simpa using h₂⟩
 
-@[simp] theorem findSome?_guard {xs : Vector α n} : findSome? (Option.guard fun x => p x) xs = find? p xs := by
+@[simp] theorem findSome?_guard {xs : Vector α n} : findSome? (Option.guard p) xs = find? p xs := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
-theorem find?_eq_findSome?_guard {xs : Vector α n} : find? p xs = findSome? (Option.guard fun x => p x) xs :=
+theorem find?_eq_findSome?_guard {xs : Vector α n} : find? p xs = findSome? (Option.guard p) xs :=
   findSome?_guard.symm
 
 @[simp] theorem map_findSome? {f : α → Option β} {g : β → γ} {xs : Vector α n} :
@@ -209,7 +209,7 @@ theorem get_find?_mem {xs : Vector α n} (h) : (xs.find? p).get h ∈ xs := by
   simp
 
 @[simp] theorem find?_flatten {xs : Vector (Vector α m) n} {p : α → Bool} :
-    xs.flatten.find? p = xs.findSome? (·.find? p) := by
+    xs.flatten.find? p = xs.findSome? (find? p) := by
   cases xs using vector₂_induction
   simp [Array.findSome?_map, Function.comp_def]
 

src/Init/Data/Vector/Lemmas.lean

@@ -2538,23 +2538,23 @@ theorem foldr_hom (f : β₁ → β₂) {g₁ : α → β₁ → β₁} {g₂ :
   rw [Array.foldr_hom _ H]
 
 /--
-We can prove that two folds over the same array are related (by some arbitrary relation)
-if we know that the initial elements are related and the folding function, for each element of the array,
-preserves the relation.
+We can prove that two folds over the same vector are related (by some arbitrary relation)
+if we know that the initial elements are related and the folding function, for each element of the
+vector, preserves the relation.
 -/
-theorem foldl_rel {xs : Vector α n} {f g : β → α → β} {a b : β} {r : β → β → Prop}
-    (h : r a b) (h' : ∀ (a : α), a ∈ xs → ∀ (c c' : β), r c c' → r (f c a) (g c' a)) :
+theorem foldl_rel {xs : Vector α n} {f : β → α → β} {g : γ → α → γ} {a : β} {b : γ} {r : β → γ → Prop}
+    (h : r a b) (h' : ∀ (a : α), a ∈ xs → ∀ (c : β) (c' : γ), r c c' → r (f c a) (g c' a)) :
     r (xs.foldl (fun acc a => f acc a) a) (xs.foldl (fun acc a => g acc a) b) := by
   rcases xs with ⟨xs, rfl⟩
   simpa using Array.foldl_rel h (by simpa using h')
 
 /--
-We can prove that two folds over the same array are related (by some arbitrary relation)
-if we know that the initial elements are related and the folding function, for each element of the array,
-preserves the relation.
+We can prove that two folds over the same vector are related (by some arbitrary relation)
+if we know that the initial elements are related and the folding function, for each element of the
+vector, preserves the relation.
 -/
-theorem foldr_rel {xs : Vector α n} {f g : α → β → β} {a b : β} {r : β → β → Prop}
-    (h : r a b) (h' : ∀ (a : α), a ∈ xs → ∀ (c c' : β), r c c' → r (f a c) (g a c')) :
+theorem foldr_rel {xs : Vector α n} {f : α → β → β} {g : α → γ → γ} {a : β} {b : γ} {r : β → γ → Prop}
+    (h : r a b) (h' : ∀ (a : α), a ∈ xs → ∀ (c : β) (c' : γ), r c c' → r (f a c) (g a c')) :
     r (xs.foldr (fun a acc => f a acc) a) (xs.foldr (fun a acc => g a acc) b) := by
   rcases xs with ⟨xs, rfl⟩
   simpa using Array.foldr_rel h (by simpa using h')

src/Init/GetElem.lean

@@ -47,7 +47,7 @@ proof in the context using `have`, because `get_elem_tactic` tries
 
 The proof side-condition `valid xs i` is automatically dispatched by the
 `get_elem_tactic` tactic; this tactic can be extended by adding more clauses to
-`get_elem_tactic_trivial` using `macro_rules`.
+`get_elem_tactic_extensible` 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
@@ -193,7 +193,7 @@ instance (priority := low) [GetElem coll idx elem valid] [∀ xs i, Decidable (v
   simp only [getElem?_def] at h ⊢
   split <;> simp_all
 
-@[simp, grind =] theorem getElem?_eq_none_iff [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+@[simp] theorem getElem?_eq_none_iff [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     (c : cont) (i : idx) [Decidable (dom c i)] : c[i]? = none ↔ ¬dom c i := by
   simp only [getElem?_def]
   split <;> simp_all
@@ -238,8 +238,6 @@ theorem getElem_of_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx
     {c : cont} {i : idx} [Decidable (dom c i)] (h : c[i]? = some e) : Exists fun h : dom c i => c[i] = e :=
   getElem?_eq_some_iff.mp h
 
-grind_pattern getElem_of_getElem? => c[i]?, some e
-
 @[simp] theorem some_getElem_eq_getElem?_iff [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     {c : cont} {i : idx} [Decidable (dom c i)] (h : dom c i):
     (some c[i] = c[i]?) ↔ True := by
@@ -283,7 +281,7 @@ instance [GetElem? cont Nat elem dom] [h : LawfulGetElem cont Nat elem dom] :
 @[simp, grind =] theorem getElem!_fin [GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) [Inhabited Elem] : a[i]! = a[i.1]! := rfl
 
 macro_rules
-  | `(tactic| get_elem_tactic_trivial) => `(tactic| (with_reducible apply Fin.val_lt_of_le); get_elem_tactic_trivial; done)
+  | `(tactic| get_elem_tactic_extensible) => `(tactic| (with_reducible apply Fin.val_lt_of_le); get_elem_tactic_extensible; done)
 
 end Fin
 

src/Init/Grind.lean

@@ -18,4 +18,5 @@ import Init.Grind.CommRing
 import Init.Grind.Module
 import Init.Grind.Ordered
 import Init.Grind.Ext
+import Init.Grind.ToInt
 import Init.Data.Int.OfNat -- This may not have otherwise been imported, breaking `grind` proofs.

src/Init/Grind/CommRing/Basic.lean

@@ -71,7 +71,9 @@ class CommRing (α : Type u) extends Ring α, CommSemiring α
 attribute [instance 100] Semiring.toAdd Semiring.toMul Semiring.toHPow Ring.toNeg Ring.toSub
 
 -- This is a low-priority instance, to avoid conflicts with existing `OfNat`, `NatCast`, and `IntCast` instances.
-attribute [instance 100] Semiring.ofNat Semiring.natCast Ring.intCast
+attribute [instance 100] Semiring.ofNat
+
+attribute [local instance] Semiring.natCast Ring.intCast
 
 namespace Semiring
 
@@ -118,7 +120,6 @@ theorem pow_add (a : α) (k₁ k₂ : Nat) : a ^ (k₁ + k₂) = a^k₁ * a^k₂
 instance : NatModule α where
   hMul a x := a * x
   add_zero := by simp [add_zero]
-  zero_add := by simp [zero_add]
   add_assoc := by simp [add_assoc]
   add_comm := by simp [add_comm]
   zero_hmul := by simp [natCast_zero, zero_mul]
@@ -271,7 +272,6 @@ theorem intCast_pow (x : Int) (k : Nat) : ((x ^ k : Int) : α) = (x : α) ^ k :=
 instance : IntModule α where
   hMul a x := a * x
   add_zero := by simp [add_zero]
-  zero_add := by simp [zero_add]
   add_assoc := by simp [add_assoc]
   add_comm := by simp [add_comm]
   zero_hmul := by simp [intCast_zero, zero_mul]

src/Init/Grind/CommRing/BitVec.lean

@@ -34,4 +34,9 @@ instance : CommRing (BitVec w) where
 instance : IsCharP (BitVec w) (2 ^ w) where
   ofNat_eq_zero_iff {x} := by simp [BitVec.ofInt, BitVec.toNat_eq]
 
+-- Verify we can derive the instances showing how `toInt` interacts with operations:
+example : ToInt.Add (BitVec w) (some 0) (some (2^w)) := inferInstance
+example : ToInt.Neg (BitVec w) (some 0) (some (2^w)) := inferInstance
+example : ToInt.Sub (BitVec w) (some 0) (some (2^w)) := inferInstance
+
 end Lean.Grind

src/Init/Grind/CommRing/Fin.lean

@@ -14,22 +14,6 @@ namespace Lean.Grind
 
 namespace Fin
 
-instance (n : Nat) [NeZero n] : NatCast (Fin n) where
-  natCast a := Fin.ofNat n a
-
-@[expose]
-def intCast [NeZero n] (a : Int) : Fin n :=
-  if 0 ≤ a then
-    Fin.ofNat n a.natAbs
-  else
-    - Fin.ofNat n a.natAbs
-
-instance (n : Nat) [NeZero n] : IntCast (Fin n) where
-  intCast := Fin.intCast
-
-theorem intCast_def {n : Nat} [NeZero n] (x : Int) :
-    (x : Fin n) = if 0 ≤ x then Fin.ofNat n x.natAbs else -Fin.ofNat n x.natAbs := rfl
-
 -- TODO: we should replace this at runtime with either repeated squaring,
 -- or a GMP accelerated function.
 @[expose]
@@ -78,18 +62,22 @@ theorem sub_eq_add_neg [NeZero n] (a b : Fin n) : a - b = a + -b := by
   cases a; cases b; simp [Fin.neg_def, Fin.sub_def, Fin.add_def, Nat.add_comm]
 
 private theorem neg_neg [NeZero n] (a : Fin n) : - - a = a := by
-  cases a; simp [Fin.neg_def, Fin.sub_def];
+  cases a; simp [Fin.neg_def, Fin.sub_def]
   next a h => cases a; simp; next a =>
    rw [Nat.self_sub_mod n (a+1)]
    have : NeZero (n - (a + 1)) := ⟨by omega⟩
    rw [Nat.self_sub_mod, Nat.sub_sub_eq_min, Nat.min_eq_right (Nat.le_of_lt h)]
 
+open Fin.NatCast Fin.IntCast in
 theorem intCast_neg [NeZero n] (i : Int) : Int.cast (R := Fin n) (-i) = - Int.cast (R := Fin n) i := by
-  simp [Int.cast, IntCast.intCast, Fin.intCast]; split <;> split <;> try omega
+  simp [Int.cast, IntCast.intCast, Fin.intCast]
+  split <;> split <;> try omega
   next h₁ h₂ => simp [Int.le_antisymm h₁ h₂, Fin.neg_def]
   next => simp [Fin.neg_neg]
 
 instance (n : Nat) [NeZero n] : CommRing (Fin n) where
+  natCast := Fin.NatCast.instNatCast n
+  intCast := Fin.IntCast.instIntCast n
   add_assoc := Fin.add_assoc
   add_comm := Fin.add_comm
   add_zero := Fin.add_zero
@@ -112,6 +100,9 @@ instance (n : Nat) [NeZero n] : IsCharP (Fin n) n where
     simp only [Nat.zero_mod]
     simp only [Fin.mk.injEq]
 
+example [NeZero n] : ToInt.Neg (Fin n) (some 0) (some n) := inferInstance
+example [NeZero n] : ToInt.Sub (Fin n) (some 0) (some n) := inferInstance
+
 end Fin
 
 end Lean.Grind

src/Init/Grind/CommRing/Poly.lean

@@ -11,10 +11,14 @@ import Init.Data.Hashable
 import all Init.Data.Ord
 import Init.Data.RArray
 import Init.Grind.CommRing.Basic
+import Init.Grind.Ordered.Ring
 
 namespace Lean.Grind
 namespace CommRing
 
+-- These are no longer global instances, so we need to turn them on here.
+attribute [local instance] Semiring.natCast Ring.intCast
+
 abbrev Var := Nat
 
 inductive Expr where
@@ -32,13 +36,13 @@ abbrev Context (α : Type u) := RArray α
 def Var.denote {α} (ctx : Context α) (v : Var) : α :=
   ctx.get v
 
-def denoteInt {α} [CommRing α] (k : Int) : α :=
+def denoteInt {α} [Ring α] (k : Int) : α :=
   bif k < 0 then
     - OfNat.ofNat (α := α) k.natAbs
   else
     OfNat.ofNat (α := α) k.natAbs
 
-def Expr.denote {α} [CommRing α] (ctx : Context α) : Expr → α
+def Expr.denote {α} [Ring α] (ctx : Context α) : Expr → α
   | .add a b  => denote ctx a + denote ctx b
   | .sub a b  => denote ctx a - denote ctx b
   | .mul a b  => denote ctx a * denote ctx b
@@ -1136,5 +1140,90 @@ theorem imp_keqC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) [NoNatZe
 
 end Stepwise
 
+/-! IntModule interface -/
+
+def Mon.denoteAsIntModule [CommRing α] (ctx : Context α) (m : Mon) : α :=
+  match m with
+  | .unit => One.one
+  | .mult pw m => go m (pw.denote ctx)
+where
+  go (m : Mon) (acc : α) : α :=
+    match m with
+    | .unit => acc
+    | .mult pw m => go m (acc * pw.denote ctx)
+
+def Poly.denoteAsIntModule [CommRing α] (ctx : Context α) (p : Poly) : α :=
+  match p with
+  | .num k => Int.cast k * One.one
+  | .add k m p => Int.cast k * m.denoteAsIntModule ctx + denoteAsIntModule ctx p
+
+theorem Mon.denoteAsIntModule_go_eq_denote {α} [CommRing α] (ctx : Context α) (m : Mon) (acc : α)
+    : denoteAsIntModule.go ctx m acc = acc * m.denote ctx := by
+  induction m generalizing acc <;> simp [*, denoteAsIntModule.go, denote, mul_one, One.one, *, mul_assoc]
+
+theorem Mon.denoteAsIntModule_eq_denote {α} [CommRing α] (ctx : Context α) (m : Mon)
+    : m.denoteAsIntModule ctx = m.denote ctx := by
+  cases m <;> simp [denoteAsIntModule, denote, denoteAsIntModule_go_eq_denote]; rfl
+
+theorem Poly.denoteAsIntModule_eq_denote {α} [CommRing α] (ctx : Context α) (p : Poly) : p.denoteAsIntModule ctx = p.denote ctx := by
+  induction p <;> simp [*, denoteAsIntModule, denote, mul_one, One.one, Mon.denoteAsIntModule_eq_denote]
+
+open Stepwise
+
+theorem eq_norm {α} [CommRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+    : core_cert lhs rhs p → lhs.denote ctx = rhs.denote ctx → p.denoteAsIntModule ctx = 0 := by
+  rw [Poly.denoteAsIntModule_eq_denote]; apply core
+
+theorem diseq_norm {α} [CommRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+    : core_cert lhs rhs p → lhs.denote ctx ≠ rhs.denote ctx → p.denoteAsIntModule ctx ≠ 0 := by
+  simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h; subst p; simp [Expr.denote_toPoly, Expr.denote]
+  intro h; rw [sub_eq_zero_iff] at h; contradiction
+
+open IntModule.IsOrdered
+
+theorem le_norm {α} [CommRing α] [Preorder α] [Ring.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+    : core_cert lhs rhs p → lhs.denote ctx ≤ rhs.denote ctx → p.denoteAsIntModule ctx ≤ 0 := by
+  simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h; subst p; simp [Expr.denote_toPoly, Expr.denote]
+  replace h := add_le_left h ((-1) * rhs.denote ctx)
+  rw [neg_mul, ← sub_eq_add_neg, one_mul, ← sub_eq_add_neg, sub_self] at h
+  assumption
+
+theorem lt_norm {α} [CommRing α] [Preorder α] [Ring.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+    : core_cert lhs rhs p → lhs.denote ctx < rhs.denote ctx → p.denoteAsIntModule ctx < 0 := by
+  simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h; subst p; simp [Expr.denote_toPoly, Expr.denote]
+  replace h := add_lt_left h ((-1) * rhs.denote ctx)
+  rw [neg_mul, ← sub_eq_add_neg, one_mul, ← sub_eq_add_neg, sub_self] at h
+  assumption
+
+theorem not_le_norm {α} [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+    : core_cert rhs lhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → p.denoteAsIntModule ctx < 0 := by
+  simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]
+  replace h₁ := LinearOrder.lt_of_not_le h₁
+  replace h₁ := add_lt_left h₁ (-lhs.denote ctx)
+  simp [← sub_eq_add_neg, sub_self] at h₁
+  assumption
+
+theorem not_lt_norm {α} [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+    : core_cert rhs lhs p → ¬ lhs.denote ctx < rhs.denote ctx → p.denoteAsIntModule ctx ≤ 0 := by
+  simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]
+  replace h₁ := LinearOrder.le_of_not_lt h₁
+  replace h₁ := add_le_left h₁ (-lhs.denote ctx)
+  simp [← sub_eq_add_neg, sub_self] at h₁
+  assumption
+
+theorem not_le_norm' {α} [CommRing α] [Preorder α] [Ring.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+    : core_cert lhs rhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → ¬ p.denoteAsIntModule ctx ≤ 0 := by
+  simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]; intro h
+  replace h := add_le_right (rhs.denote ctx) h
+  rw [sub_eq_add_neg, add_left_comm, ← sub_eq_add_neg, sub_self] at h; simp [add_zero] at h
+  contradiction
+
+theorem not_lt_norm' {α} [CommRing α] [Preorder α] [Ring.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+    : core_cert lhs rhs p → ¬ lhs.denote ctx < rhs.denote ctx → ¬ p.denoteAsIntModule ctx < 0 := by
+  simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]; intro h
+  replace h := add_lt_right (rhs.denote ctx) h
+  rw [sub_eq_add_neg, add_left_comm, ← sub_eq_add_neg, sub_self] at h; simp [add_zero] at h
+  contradiction
+
 end CommRing
 end Lean.Grind

src/Init/Grind/CommRing/SInt.lean

@@ -45,6 +45,11 @@ instance : IsCharP Int8 (2 ^ 8) where
     simp [Int8.ofInt_eq_iff_bmod_eq_toInt,
       ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right]
 
+-- Verify we can derive the instances showing how `toInt` interacts with operations:
+example : ToInt.Add Int8 (some (-(2^7))) (some (2^7)) := inferInstance
+example : ToInt.Neg Int8 (some (-(2^7))) (some (2^7)) := inferInstance
+example : ToInt.Sub Int8 (some (-(2^7))) (some (2^7)) := inferInstance
+
 instance : NatCast Int16 where
   natCast x := Int16.ofNat x
 
@@ -76,6 +81,11 @@ instance : IsCharP Int16 (2 ^ 16) where
     simp [Int16.ofInt_eq_iff_bmod_eq_toInt,
       ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right]
 
+-- Verify we can derive the instances showing how `toInt` interacts with operations:
+example : ToInt.Add Int16 (some (-(2^15))) (some (2^15)) := inferInstance
+example : ToInt.Neg Int16 (some (-(2^15))) (some (2^15)) := inferInstance
+example : ToInt.Sub Int16 (some (-(2^15))) (some (2^15)) := inferInstance
+
 instance : NatCast Int32 where
   natCast x := Int32.ofNat x
 
@@ -107,6 +117,11 @@ instance : IsCharP Int32 (2 ^ 32) where
     simp [Int32.ofInt_eq_iff_bmod_eq_toInt,
       ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right]
 
+-- Verify we can derive the instances showing how `toInt` interacts with operations:
+example : ToInt.Add Int32 (some (-(2^31))) (some (2^31)) := inferInstance
+example : ToInt.Neg Int32 (some (-(2^31))) (some (2^31)) := inferInstance
+example : ToInt.Sub Int32 (some (-(2^31))) (some (2^31)) := inferInstance
+
 instance : NatCast Int64 where
   natCast x := Int64.ofNat x
 
@@ -138,6 +153,11 @@ instance : IsCharP Int64 (2 ^ 64) where
     simp [Int64.ofInt_eq_iff_bmod_eq_toInt,
       ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right]
 
+-- Verify we can derive the instances showing how `toInt` interacts with operations:
+example : ToInt.Add Int64 (some (-(2^63))) (some (2^63)) := inferInstance
+example : ToInt.Neg Int64 (some (-(2^63))) (some (2^63)) := inferInstance
+example : ToInt.Sub Int64 (some (-(2^63))) (some (2^63)) := inferInstance
+
 instance : NatCast ISize where
   natCast x := ISize.ofNat x
 
@@ -171,4 +191,9 @@ instance : IsCharP ISize (2 ^ numBits) where
     simp [ISize.ofInt_eq_iff_bmod_eq_toInt,
       ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right]
 
+-- Verify we can derive the instances showing how `toInt` interacts with operations:
+example : ToInt.Add ISize (some (-(2^(numBits-1)))) (some (2^(numBits-1))) := inferInstance
+example : ToInt.Neg ISize (some (-(2^(numBits-1)))) (some (2^(numBits-1))) := inferInstance
+example : ToInt.Sub ISize (some (-(2^(numBits-1)))) (some (2^(numBits-1))) := inferInstance
+
 end Lean.Grind

src/Init/Grind/CommRing/UInt.lean

@@ -149,6 +149,11 @@ instance : IsCharP UInt8 256 where
     have : OfNat.ofNat x = UInt8.ofNat x := rfl
     simp [this, UInt8.ofNat_eq_iff_mod_eq_toNat]
 
+-- Verify we can derive the instances showing how `toInt` interacts with operations:
+example : ToInt.Add UInt8 (some 0) (some (2^8)) := inferInstance
+example : ToInt.Neg UInt8 (some 0) (some (2^8)) := inferInstance
+example : ToInt.Sub UInt8 (some 0) (some (2^8)) := inferInstance
+
 instance : CommRing UInt16 where
   add_assoc := UInt16.add_assoc
   add_comm := UInt16.add_comm
@@ -174,6 +179,11 @@ instance : IsCharP UInt16 65536 where
     have : OfNat.ofNat x = UInt16.ofNat x := rfl
     simp [this, UInt16.ofNat_eq_iff_mod_eq_toNat]
 
+-- Verify we can derive the instances showing how `toInt` interacts with operations:
+example : ToInt.Add UInt16 (some 0) (some (2^16)) := inferInstance
+example : ToInt.Neg UInt16 (some 0) (some (2^16)) := inferInstance
+example : ToInt.Sub UInt16 (some 0) (some (2^16)) := inferInstance
+
 instance : CommRing UInt32 where
   add_assoc := UInt32.add_assoc
   add_comm := UInt32.add_comm
@@ -199,6 +209,11 @@ instance : IsCharP UInt32 4294967296 where
     have : OfNat.ofNat x = UInt32.ofNat x := rfl
     simp [this, UInt32.ofNat_eq_iff_mod_eq_toNat]
 
+-- Verify we can derive the instances showing how `toInt` interacts with operations:
+example : ToInt.Add UInt32 (some 0) (some (2^32)) := inferInstance
+example : ToInt.Neg UInt32 (some 0) (some (2^32)) := inferInstance
+example : ToInt.Sub UInt32 (some 0) (some (2^32)) := inferInstance
+
 instance : CommRing UInt64 where
   add_assoc := UInt64.add_assoc
   add_comm := UInt64.add_comm
@@ -224,6 +239,11 @@ instance : IsCharP UInt64 18446744073709551616 where
     have : OfNat.ofNat x = UInt64.ofNat x := rfl
     simp [this, UInt64.ofNat_eq_iff_mod_eq_toNat]
 
+-- Verify we can derive the instances showing how `toInt` interacts with operations:
+example : ToInt.Add UInt64 (some 0) (some (2^64)) := inferInstance
+example : ToInt.Neg UInt64 (some 0) (some (2^64)) := inferInstance
+example : ToInt.Sub UInt64 (some 0) (some (2^64)) := inferInstance
+
 instance : CommRing USize where
   add_assoc := USize.add_assoc
   add_comm := USize.add_comm
@@ -251,4 +271,9 @@ instance : IsCharP USize (2 ^ numBits) where
     have : OfNat.ofNat x = USize.ofNat x := rfl
     simp [this, USize.ofNat_eq_iff_mod_eq_toNat]
 
+-- Verify we can derive the instances showing how `toInt` interacts with operations:
+example : ToInt.Add USize (some 0) (some (2^numBits)) := inferInstance
+example : ToInt.Neg USize (some 0) (some (2^numBits)) := inferInstance
+example : ToInt.Sub USize (some 0) (some (2^numBits)) := inferInstance
+
 end Lean.Grind

src/Init/Grind/Module/Basic.lean

@@ -7,12 +7,12 @@ module
 
 prelude
 import Init.Data.Int.Order
+import Init.Grind.ToInt
 
 namespace Lean.Grind
 
 class NatModule (M : Type u) extends Zero M, Add M, HMul Nat M M where
   add_zero : ∀ a : M, a + 0 = a
-  zero_add : ∀ a : M, 0 + a = a
   add_comm : ∀ a b : M, a + b = b + a
   add_assoc : ∀ a b c : M, a + b + c = a + (b + c)
   zero_hmul : ∀ a : M, 0 * a = 0
@@ -26,7 +26,6 @@ attribute [instance 100] NatModule.toZero NatModule.toAdd NatModule.toHMul
 
 class IntModule (M : Type u) extends Zero M, Add M, Neg M, Sub M, HMul Int M M where
   add_zero : ∀ a : M, a + 0 = a
-  zero_add : ∀ a : M, 0 + a = a
   add_comm : ∀ a b : M, a + b = b + a
   add_assoc : ∀ a b c : M, a + b + c = a + (b + c)
   zero_hmul : ∀ a : M, (0 : Int) * a = 0
@@ -52,9 +51,15 @@ instance toNatModule (M : Type u) [i : IntModule M] : NatModule M :=
 
 variable {M : Type u} [IntModule M]
 
+theorem zero_add (a : M) : 0 + a = a := by
+  rw [add_comm, add_zero]
+
 theorem add_neg_cancel (a : M) : a + -a = 0 := by
   rw [add_comm, neg_add_cancel]
 
+theorem add_left_comm (a b c : M) : a + (b + c) = b + (a + c) := by
+  rw [← add_assoc, ← add_assoc, add_comm a]
+
 theorem add_left_inj {a b : M} (c : M) : a + c = b + c ↔ a = b :=
   ⟨fun h => by simpa [add_assoc, add_neg_cancel, add_zero] using (congrArg (· + -c) h),
    fun g => congrArg (· + c) g⟩
@@ -111,4 +116,17 @@ class NoNatZeroDivisors (α : Type u) [Zero α] [HMul Nat α α] where
 
 export NoNatZeroDivisors (no_nat_zero_divisors)
 
+instance [ToInt α (some lo) (some hi)] [IntModule α] [ToInt.Zero α (some lo) (some hi)] [ToInt.Add α (some lo) (some hi)] : ToInt.Neg α (some lo) (some hi) where
+  toInt_neg x := by
+    have := (ToInt.Add.toInt_add (-x) x).symm
+    rw [IntModule.neg_add_cancel, ToInt.Zero.toInt_zero] at this
+    rw [ToInt.wrap_eq_wrap_iff] at this
+    simp at this
+    rw [← ToInt.wrap_toInt]
+    rw [ToInt.wrap_eq_wrap_iff]
+    simpa
+
+instance [ToInt α (some lo) (some hi)] [IntModule α] [ToInt.Add α (some lo) (some hi)] [ToInt.Neg α (some lo) (some hi)] : ToInt.Sub α (some lo) (some hi) :=
+  ToInt.Sub.of_sub_eq_add_neg IntModule.sub_eq_add_neg
+
 end Lean.Grind

src/Init/Grind/Ordered.lean

@@ -11,3 +11,4 @@ import Init.Grind.Ordered.Module
 import Init.Grind.Ordered.Ring
 import Init.Grind.Ordered.Field
 import Init.Grind.Ordered.Int
+import Init.Grind.Ordered.Linarith

src/Init/Grind/Ordered/Linarith.lean

@@ -0,0 +1,502 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+import Init.Grind.Ordered.Module
+import Init.Grind.Ordered.Ring
+import all Init.Data.Ord
+import all Init.Data.AC
+import Init.Data.RArray
+
+/-!
+Support for the linear arithmetic module for `IntModule` in `grind`
+-/
+
+namespace Lean.Grind.Linarith
+abbrev Var := Nat
+open IntModule
+
+attribute [local simp] add_zero zero_add zero_hmul hmul_zero one_hmul
+
+inductive Expr where
+  | zero
+  | var  (i : Var)
+  | add  (a b : Expr)
+  | sub  (a b : Expr)
+  | neg  (a : Expr)
+  | mul  (k : Int) (a : Expr)
+  deriving Inhabited, BEq
+
+abbrev Context (α : Type u) := RArray α
+
+def Var.denote {α} (ctx : Context α) (v : Var) : α :=
+  ctx.get v
+
+def Expr.denote {α} [IntModule α] (ctx : Context α) : Expr → α
+  | zero      => 0
+  | .var v    => v.denote ctx
+  | .add a b  => denote ctx a + denote ctx b
+  | .sub a b  => denote ctx a - denote ctx b
+  | .mul k a  => k * denote ctx a
+  | .neg a    => -denote ctx a
+
+inductive Poly where
+  | nil
+  | add (k : Int) (v : Var) (p : Poly)
+  deriving BEq
+
+def Poly.denote {α} [IntModule α] (ctx : Context α) (p : Poly) : α :=
+  match p with
+  | .nil => 0
+  | .add k v p => k * v.denote ctx + denote ctx p
+
+/--
+Similar to `Poly.denote`, but produces a denotation better for normalization.
+-/
+def Poly.denote' {α} [IntModule α] (ctx : Context α) (p : Poly) : α :=
+  match p with
+  | .nil => 0
+  | .add 1 v p => go (v.denote ctx) p
+  | .add k v p => go (k * v.denote ctx) p
+where
+  go (r : α)  (p : Poly) : α :=
+    match p with
+    | .nil => r
+    | .add 1 v p => go (r + v.denote ctx) p
+    | .add k v p => go (r + k * v.denote ctx) p
+
+-- Helper instance for `ac_rfl`
+local instance {α} [IntModule α] : Std.Associative (· + · : α → α → α) where
+  assoc := IntModule.add_assoc
+-- Helper instance for `ac_rfl`
+local instance {α} [IntModule α] : Std.Commutative (· + · : α → α → α) where
+  comm := IntModule.add_comm
+
+theorem Poly.denote'_go_eq_denote {α} [IntModule α] (ctx : Context α) (p : Poly) (r : α) : denote'.go ctx r p = p.denote ctx + r := by
+  induction r, p using denote'.go.induct ctx <;> simp [denote'.go, denote]
+  next ih => rw [ih]; ac_rfl
+  next ih => rw [ih]; ac_rfl
+
+theorem Poly.denote'_eq_denote {α} [IntModule α] (ctx : Context α) (p : Poly) : p.denote' ctx = p.denote ctx := by
+  unfold denote' <;> split <;> simp [denote, denote'_go_eq_denote] <;> ac_rfl
+
+def Poly.insert (k : Int) (v : Var) (p : Poly) : Poly :=
+  match p with
+  | .nil => .add k v .nil
+  | .add k' v' p =>
+    bif Nat.blt v' v then
+      .add k v <| .add k' v' p
+    else bif Nat.beq v v' then
+      if Int.add k k' == 0 then
+        p
+      else
+        .add (Int.add k k') v' p
+    else
+      .add k' v' (insert k v p)
+
+/-- Normalizes the given polynomial by fusing monomial and constants. -/
+def Poly.norm (p : Poly) : Poly :=
+  match p with
+  | .nil => .nil
+  | .add k v p => (norm p).insert k v
+
+def Poly.append (p₁ p₂ : Poly) : Poly :=
+  match p₁ with
+  | .nil => p₂
+  | .add k x p₁ => .add k x (append p₁ p₂)
+
+def Poly.combine' (fuel : Nat) (p₁ p₂ : Poly) : Poly :=
+  match fuel with
+  | 0 => p₁.append p₂
+  | fuel + 1 => match p₁, p₂ with
+    | .nil, p₂ => p₂
+    | p₁, .nil => p₁
+    | .add a₁ x₁ p₁, .add a₂ x₂ p₂ =>
+      bif Nat.beq x₁ x₂ then
+        let a := a₁ + a₂
+        bif a == 0 then
+          combine' fuel p₁ p₂
+        else
+          .add a x₁ (combine' fuel p₁ p₂)
+      else bif Nat.blt x₂ x₁ then
+        .add a₁ x₁ (combine' fuel p₁ (.add a₂ x₂ p₂))
+      else
+        .add a₂ x₂ (combine' fuel (.add a₁ x₁ p₁) p₂)
+
+def Poly.combine (p₁ p₂ : Poly) : Poly :=
+  combine' 100000000 p₁ p₂
+
+/-- Converts the given expression into a polynomial. -/
+def Expr.toPoly' (e : Expr) : Poly :=
+  go 1 e .nil
+where
+  go (coeff : Int) : Expr → (Poly → Poly)
+    | .zero     => id
+    | .var v    => (.add coeff v ·)
+    | .add a b  => go coeff a ∘ go coeff b
+    | .sub a b  => go coeff a ∘ go (-coeff) b
+    | .mul k a  => bif k == 0 then id else go (Int.mul coeff k) a
+    | .neg a    => go (-coeff) a
+
+/-- Converts the given expression into a polynomial, and then normalizes it. -/
+def Expr.norm (e : Expr) : Poly :=
+  e.toPoly'.norm
+
+/--
+`p.mul k` multiplies all coefficients and constant of the polynomial `p` by `k`.
+-/
+def Poly.mul' (p : Poly) (k : Int) : Poly :=
+  match p with
+  | .nil => .nil
+  | .add k' v p => .add (k*k') v (mul' p k)
+
+def Poly.mul (p : Poly) (k : Int) : Poly :=
+  if k == 0 then
+    .nil
+  else
+    p.mul' k
+
+@[simp] theorem Poly.denote_mul {α} [IntModule α] (ctx : Context α) (p : Poly) (k : Int) : (p.mul k).denote ctx = k * p.denote ctx := by
+  simp [mul]
+  split
+  next => simp [*, denote]
+  next =>
+    induction p <;> simp [mul', denote, *]
+    rw [mul_hmul, hmul_add]
+
+theorem Poly.denote_insert {α} [IntModule α] (ctx : Context α) (k : Int) (v : Var) (p : Poly) :
+    (p.insert k v).denote ctx = p.denote ctx + k * v.denote ctx := by
+  fun_induction p.insert k v <;> simp [denote]
+  next => ac_rfl
+  next h₁ h₂ h₃ =>
+    simp at h₃; simp at h₂; subst h₂
+    rw [add_comm, ← add_assoc, ← add_hmul, h₃, zero_hmul, zero_add]
+  next h _ => simp at h; subst h; rw [add_hmul]; ac_rfl
+  next ih => rw [ih]; ac_rfl
+
+attribute [local simp] Poly.denote_insert
+
+theorem Poly.denote_norm {α} [IntModule α] (ctx : Context α) (p : Poly) : p.norm.denote ctx = p.denote ctx := by
+  induction p <;> simp [denote, norm, add_comm, *]
+
+attribute [local simp] Poly.denote_norm
+
+theorem Poly.denote_append {α} [IntModule α] (ctx : Context α) (p₁ p₂ : Poly) : (p₁.append p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := by
+  induction p₁ <;> simp [append, denote, *]; ac_rfl
+
+attribute [local simp] Poly.denote_append
+
+theorem Poly.denote_combine' {α} [IntModule α] (ctx : Context α) (fuel : Nat) (p₁ p₂ : Poly) : (p₁.combine' fuel p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := by
+  fun_induction p₁.combine' fuel p₂ <;>
+    simp_all +zetaDelta [denote, ← Int.add_mul]
+  next h _ =>
+    rw [Int.add_comm] at h
+    rw [add_left_comm, add_assoc, ← add_assoc, ← add_hmul, h, zero_hmul, zero_add]
+  next => rw [add_hmul]; ac_rfl
+  all_goals ac_rfl
+
+theorem Poly.denote_combine {α} [IntModule α] (ctx : Context α) (p₁ p₂ : Poly) : (p₁.combine p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := by
+  simp [combine, denote_combine']
+
+attribute [local simp] Poly.denote_combine
+
+theorem Expr.denote_toPoly'_go {α} [IntModule α] {k p} (ctx : Context α) (e : Expr)
+    : (toPoly'.go k e p).denote ctx = k * e.denote ctx + p.denote ctx := by
+  induction k, e using Expr.toPoly'.go.induct generalizing p <;> simp [toPoly'.go, denote, Poly.denote, *, hmul_add]
+  next => ac_rfl
+  next => rw [sub_eq_add_neg, neg_hmul, hmul_add, hmul_neg]; ac_rfl
+  next h => simp at h; subst h; simp
+  next ih => simp at ih; rw [ih, mul_hmul]
+  next => rw [hmul_neg, neg_hmul]
+
+theorem Expr.denote_norm {α} [IntModule α] (ctx : Context α) (e : Expr) : e.norm.denote ctx = e.denote ctx := by
+  simp [norm, toPoly', Expr.denote_toPoly'_go, Poly.denote]
+
+attribute [local simp] Expr.denote_norm
+
+instance : LawfulBEq Poly where
+  eq_of_beq {a} := by
+    induction a <;> intro b <;> cases b <;> simp_all! [BEq.beq]
+    next ih =>
+      intro _ _ h
+      exact ih h
+  rfl := by
+    intro a
+    induction a <;> simp! [BEq.beq]
+    assumption
+
+attribute [local simp] Poly.denote'_eq_denote
+
+def Poly.leadCoeff (p : Poly) : Int :=
+  match p with
+  | .add a _ _ => a
+  | _ => 1
+
+open IntModule.IsOrdered
+
+/-!
+Helper theorems for conflict resolution during model construction.
+-/
+
+private theorem le_add_le {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] {a b : α}
+    (h₁ : a ≤ 0) (h₂ : b ≤ 0) : a + b ≤ 0 := by
+  replace h₁ := add_le_left h₁ b; simp at h₁
+  exact Preorder.le_trans h₁ h₂
+
+private theorem le_add_lt {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] {a b : α}
+    (h₁ : a ≤ 0) (h₂ : b < 0) : a + b < 0 := by
+  replace h₁ := add_le_left h₁ b; simp at h₁
+  exact Preorder.lt_of_le_of_lt h₁ h₂
+
+private theorem lt_add_lt {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] {a b : α}
+    (h₁ : a < 0) (h₂ : b < 0) : a + b < 0 := by
+  replace h₁ := add_lt_left h₁ b; simp at h₁
+  exact Preorder.lt_trans h₁ h₂
+
+private theorem coe_natAbs_nonneg (a : Int) : (a.natAbs : Int) ≥ 0 := by
+  exact Int.natCast_nonneg a.natAbs
+
+def le_le_combine_cert (p₁ p₂ p₃ : Poly) : Bool :=
+  let a₁ := p₁.leadCoeff.natAbs
+  let a₂ := p₂.leadCoeff.natAbs
+  p₃ == (p₁.mul a₂ |>.combine (p₂.mul a₁))
+
+theorem le_le_combine {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ p₂ p₃ : Poly)
+    : le_le_combine_cert p₁ p₂ p₃ → p₁.denote' ctx ≤ 0 → p₂.denote' ctx ≤ 0 → p₃.denote' ctx ≤ 0 := by
+  simp [le_le_combine_cert]; intro _ h₁ h₂; subst p₃; simp
+  replace h₁ := hmul_nonpos (coe_natAbs_nonneg p₂.leadCoeff) h₁
+  replace h₂ := hmul_nonpos (coe_natAbs_nonneg p₁.leadCoeff) h₂
+  exact le_add_le h₁ h₂
+
+def le_lt_combine_cert (p₁ p₂ p₃ : Poly) : Bool :=
+  let a₁ := p₁.leadCoeff.natAbs
+  let a₂ := p₂.leadCoeff.natAbs
+  a₁ > (0 : Int) && p₃ == (p₁.mul a₂ |>.combine (p₂.mul a₁))
+
+theorem le_lt_combine {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ p₂ p₃ : Poly)
+    : le_lt_combine_cert p₁ p₂ p₃ → p₁.denote' ctx ≤ 0 → p₂.denote' ctx < 0 → p₃.denote' ctx < 0 := by
+  simp [-Int.natAbs_pos, -Int.ofNat_pos, le_lt_combine_cert]; intro hp _ h₁ h₂; subst p₃; simp
+  replace h₁ := hmul_nonpos (coe_natAbs_nonneg p₂.leadCoeff) h₁
+  replace h₂ := hmul_neg (↑p₁.leadCoeff.natAbs) h₂ |>.mp hp
+  exact le_add_lt h₁ h₂
+
+theorem le_eq_combine {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ p₂ p₃ : Poly)
+    : le_le_combine_cert p₁ p₂ p₃ → p₁.denote' ctx ≤ 0 → p₂.denote' ctx = 0 → p₃.denote' ctx ≤ 0 := by
+  simp [le_le_combine_cert]; intro _ h₁ h₂; subst p₃; simp [h₂]
+  replace h₁ := hmul_nonpos (coe_natAbs_nonneg p₂.leadCoeff) h₁
+  assumption
+
+def lt_lt_combine_cert (p₁ p₂ p₃ : Poly) : Bool :=
+  let a₁ := p₁.leadCoeff.natAbs
+  let a₂ := p₂.leadCoeff.natAbs
+  a₂ > (0 : Int) && a₁ > (0 : Int) && p₃ == (p₁.mul a₂ |>.combine (p₂.mul a₁))
+
+theorem lt_lt_combine {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ p₂ p₃ : Poly)
+    : lt_lt_combine_cert p₁ p₂ p₃ → p₁.denote' ctx < 0 → p₂.denote' ctx < 0 → p₃.denote' ctx < 0 := by
+  simp [-Int.natAbs_pos, -Int.ofNat_pos, lt_lt_combine_cert]; intro hp₁ hp₂ _ h₁ h₂; subst p₃; simp
+  replace h₁ := hmul_neg (↑p₂.leadCoeff.natAbs) h₁ |>.mp hp₁
+  replace h₂ := hmul_neg (↑p₁.leadCoeff.natAbs) h₂ |>.mp hp₂
+  exact lt_add_lt h₁ h₂
+
+def lt_eq_combine_cert (p₁ p₂ p₃ : Poly) : Bool :=
+  let a₁ := p₁.leadCoeff.natAbs
+  let a₂ := p₂.leadCoeff.natAbs
+  a₂ > (0 : Int) && p₃ == (p₁.mul a₂ |>.combine (p₂.mul a₁))
+
+theorem lt_eq_combine {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ p₂ p₃ : Poly)
+    : lt_eq_combine_cert p₁ p₂ p₃ → p₁.denote' ctx < 0 → p₂.denote' ctx = 0 → p₃.denote' ctx < 0 := by
+  simp [-Int.natAbs_pos, -Int.ofNat_pos, lt_eq_combine_cert]; intro hp₁ _ h₁ h₂; subst p₃; simp [h₂]
+  replace h₁ := hmul_neg (↑p₂.leadCoeff.natAbs) h₁ |>.mp hp₁
+  assumption
+
+theorem eq_eq_combine {α} [IntModule α] (ctx : Context α) (p₁ p₂ p₃ : Poly)
+    : le_le_combine_cert p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx = 0 → p₃.denote' ctx = 0 := by
+  simp [le_le_combine_cert]; intro _ h₁ h₂; subst p₃; simp [h₁, h₂]
+
+def diseq_split_cert (p₁ p₂ : Poly) : Bool :=
+  p₂ == p₁.mul (-1)
+
+-- We need `LinearOrder` to use `trichotomy`
+theorem diseq_split {α} [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ p₂ : Poly)
+    : diseq_split_cert p₁ p₂ → p₁.denote' ctx ≠ 0 → p₁.denote' ctx < 0 ∨ p₂.denote' ctx < 0 := by
+  simp [diseq_split_cert]; intro _ h₁; subst p₂; simp
+  cases LinearOrder.trichotomy (p₁.denote ctx) 0
+  next h => exact Or.inl h
+  next h =>
+    apply Or.inr
+    simp [h₁] at h
+    rw [← neg_pos_iff, neg_hmul, neg_neg, one_hmul]; assumption
+
+theorem diseq_split_resolve {α} [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ p₂ : Poly)
+    : diseq_split_cert p₁ p₂ → p₁.denote' ctx ≠ 0 → ¬p₁.denote' ctx < 0 → p₂.denote' ctx < 0 := by
+  intro h₁ h₂ h₃
+  exact (diseq_split ctx p₁ p₂ h₁ h₂).resolve_left h₃
+
+def eq_diseq_combine_cert (p₁ p₂ p₃ : Poly) : Bool :=
+  let a₁ := p₁.leadCoeff.natAbs
+  let a₂ := p₂.leadCoeff.natAbs
+  a₁ ≠ 0 && p₃ == (p₁.mul a₂ |>.combine (p₂.mul a₁))
+
+theorem eq_diseq_combine {α} [IntModule α] [NoNatZeroDivisors α] (ctx : Context α) (p₁ p₂ p₃ : Poly)
+    : eq_diseq_combine_cert p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx ≠ 0 → p₃.denote' ctx ≠ 0 := by
+  simp [- Int.natAbs_eq_zero, -Int.natCast_eq_zero, eq_diseq_combine_cert]; intro hne _ h₁ h₂; subst p₃
+  simp [h₁, h₂]; intro h
+  have := no_nat_zero_divisors (p₁.leadCoeff.natAbs) (p₂.denote ctx) hne h
+  contradiction
+
+def eq_diseq_combine_cert' (p₁ p₂ p₃ : Poly) (k : Int) : Bool :=
+  p₃ == (p₁.mul k |>.combine p₂)
+
+/-
+Special case of `eq_diseq_combine` where leading coefficient `c₁` of `p₁` is `-k*c₂`, where
+`c₂` is the leading coefficient of `p₂`.
+-/
+theorem eq_diseq_combine' {α} [IntModule α] (ctx : Context α) (p₁ p₂ p₃ : Poly) (k : Int)
+    : eq_diseq_combine_cert' p₁ p₂ p₃ k → p₁.denote' ctx = 0 → p₂.denote' ctx ≠ 0 → p₃.denote' ctx ≠ 0 := by
+  simp [eq_diseq_combine_cert']; intro _ h₁ h₂; subst p₃
+  simp [h₁, h₂]
+
+/-!
+Helper theorems for internalizing facts into the linear arithmetic procedure
+-/
+
+def norm_cert (lhs rhs : Expr) (p : Poly) :=
+  p == (lhs.sub rhs).norm
+
+theorem eq_norm {α} [IntModule α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+    : norm_cert lhs rhs p → lhs.denote ctx = rhs.denote ctx → p.denote' ctx = 0 := by
+  simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote, h₁, sub_self]
+
+theorem le_of_eq {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+    : norm_cert lhs rhs p → lhs.denote ctx = rhs.denote ctx → p.denote' ctx ≤ 0 := by
+  simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote, h₁, sub_self]
+  apply Preorder.le_refl
+
+theorem diseq_norm {α} [IntModule α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+    : norm_cert lhs rhs p → lhs.denote ctx ≠ rhs.denote ctx → p.denote' ctx ≠ 0 := by
+  simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote, h₁, sub_self]
+  intro h
+  replace h := congrArg (rhs.denote ctx + ·) h; simp [sub_eq_add_neg] at h
+  rw [add_left_comm, ← sub_eq_add_neg, sub_self, add_zero] at h
+  contradiction
+
+theorem le_norm {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+    : norm_cert lhs rhs p → lhs.denote ctx ≤ rhs.denote ctx → p.denote' ctx ≤ 0 := by
+  simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote, h₁, sub_self]
+  replace h₁ := add_le_left h₁ (-rhs.denote ctx)
+  simp [← sub_eq_add_neg, sub_self] at h₁
+  assumption
+
+theorem lt_norm {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+    : norm_cert lhs rhs p → lhs.denote ctx < rhs.denote ctx → p.denote' ctx < 0 := by
+  simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote, h₁, sub_self]
+  replace h₁ := add_lt_left h₁ (-rhs.denote ctx)
+  simp [← sub_eq_add_neg, sub_self] at h₁
+  assumption
+
+theorem not_le_norm {α} [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+    : norm_cert rhs lhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → p.denote' ctx < 0 := by
+  simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote, h₁, sub_self]
+  replace h₁ := LinearOrder.lt_of_not_le h₁
+  replace h₁ := add_lt_left h₁ (-lhs.denote ctx)
+  simp [← sub_eq_add_neg, sub_self] at h₁
+  assumption
+
+theorem not_lt_norm {α} [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+    : norm_cert rhs lhs p → ¬ lhs.denote ctx < rhs.denote ctx → p.denote' ctx ≤ 0 := by
+  simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote, h₁, sub_self]
+  replace h₁ := LinearOrder.le_of_not_lt h₁
+  replace h₁ := add_le_left h₁ (-lhs.denote ctx)
+  simp [← sub_eq_add_neg, sub_self] at h₁
+  assumption
+
+-- If the module does not have a linear order, we can still put the expressions in polynomial forms
+
+theorem not_le_norm' {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+    : norm_cert lhs rhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → ¬ p.denote' ctx ≤ 0 := by
+  simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote, h₁, sub_self]; intro h
+  replace h := add_le_right (rhs.denote ctx) h
+  rw [sub_eq_add_neg, add_left_comm, ← sub_eq_add_neg, sub_self] at h; simp at h
+  contradiction
+
+theorem not_lt_norm' {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+    : norm_cert lhs rhs p → ¬ lhs.denote ctx < rhs.denote ctx → ¬ p.denote' ctx < 0 := by
+  simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote, h₁, sub_self]; intro h
+  replace h := add_lt_right (rhs.denote ctx) h
+  rw [sub_eq_add_neg, add_left_comm, ← sub_eq_add_neg, sub_self] at h; simp at h
+  contradiction
+
+/-!
+Equality detection
+-/
+def eq_of_le_ge_cert (p₁ p₂ : Poly) : Bool :=
+  p₂ == p₁.mul (-1)
+
+theorem eq_of_le_ge {α} [IntModule α] [PartialOrder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ : Poly) (p₂ : Poly)
+    : eq_of_le_ge_cert p₁ p₂ → p₁.denote' ctx ≤ 0 → p₂.denote' ctx ≤ 0 → p₁.denote' ctx = 0 := by
+  simp [eq_of_le_ge_cert]
+  intro; subst p₂; simp
+  intro h₁ h₂
+  replace h₂ := add_le_left h₂ (p₁.denote ctx)
+  rw [add_comm, neg_hmul, one_hmul, ← sub_eq_add_neg, sub_self, zero_add] at h₂
+  exact PartialOrder.le_antisymm h₁ h₂
+
+/-!
+Helper theorems for closing the goal
+-/
+
+theorem diseq_unsat {α} [IntModule α] (ctx : Context α) : (Poly.nil).denote ctx ≠ 0 → False := by
+  simp [Poly.denote]
+
+theorem lt_unsat {α} [IntModule α] [Preorder α] (ctx : Context α) : (Poly.nil).denote ctx < 0 → False := by
+  simp [Poly.denote]; intro h
+  have := Preorder.lt_iff_le_not_le.mp h
+  simp at this
+
+def zero_lt_one_cert (p : Poly) : Bool :=
+  p == .add (-1) 0 .nil
+
+theorem zero_lt_one {α} [Ring α] [Preorder α] [Ring.IsOrdered α] (ctx : Context α) (p : Poly)
+    : zero_lt_one_cert p → (0 : Var).denote ctx = One.one → p.denote' ctx < 0 := by
+  simp [zero_lt_one_cert]; intro _ h; subst p; simp [Poly.denote, h, One.one, neg_hmul]
+  rw [neg_lt_iff, neg_zero]; apply Ring.IsOrdered.zero_lt_one
+
+/-!
+Coefficient normalization
+-/
+
+def coeff_cert (p₁ p₂ : Poly) (k : Nat) :=
+  k > 0 && p₁ == p₂.mul k
+
+theorem eq_coeff {α} [IntModule α] [NoNatZeroDivisors α] (ctx : Context α) (p₁ p₂ : Poly) (k : Nat)
+    : coeff_cert p₁ p₂ k → p₁.denote' ctx = 0 → p₂.denote' ctx = 0 := by
+  simp [coeff_cert]; intro h _; subst p₁; simp
+  exact no_nat_zero_divisors k (p₂.denote ctx) (Nat.ne_zero_of_lt h)
+
+theorem le_coeff {α} [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ p₂ : Poly) (k : Nat)
+    : coeff_cert p₁ p₂ k → p₁.denote' ctx ≤ 0 → p₂.denote' ctx ≤ 0 := by
+  simp [coeff_cert]; intro h _; subst p₁; simp
+  have : ↑k > (0 : Int) := Int.natCast_pos.mpr h
+  intro h₁; apply Classical.byContradiction
+  intro h₂; replace h₂ := LinearOrder.lt_of_not_le h₂
+  replace h₂ := IsOrdered.hmul_pos (↑k) h₂ |>.mp this
+  exact Preorder.lt_irrefl 0 (Preorder.lt_of_lt_of_le h₂ h₁)
+
+theorem lt_coeff {α} [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ p₂ : Poly) (k : Nat)
+    : coeff_cert p₁ p₂ k → p₁.denote' ctx < 0 → p₂.denote' ctx < 0 := by
+  simp [coeff_cert]; intro h _; subst p₁; simp
+  have : ↑k > (0 : Int) := Int.natCast_pos.mpr h
+  intro h₁; apply Classical.byContradiction
+  intro h₂; replace h₂ := LinearOrder.le_of_not_lt h₂
+  replace h₂ := IsOrdered.hmul_nonneg (Int.le_of_lt this) h₂
+  exact Preorder.lt_irrefl 0 (Preorder.lt_of_le_of_lt h₂ h₁)
+
+theorem diseq_neg {α} [IntModule α] (ctx : Context α) (p p' : Poly) : p' == p.mul (-1) → p.denote' ctx ≠ 0 → p'.denote' ctx ≠ 0 := by
+  simp; intro _ _; subst p'; simp [neg_hmul]
+  intro h; replace h := congrArg (- ·) h; simp [neg_neg, neg_zero] at h
+  contradiction
+
+end Lean.Grind.Linarith

src/Init/Grind/Ordered/Order.lean

@@ -91,6 +91,19 @@ theorem trichotomy (a b : α) : a < b ∨ a = b ∨ b < a := by
     | inl h => right; right; exact h
     | inr h => right; left; exact h.symm
 
+theorem le_of_not_lt {α} [LinearOrder α] {a b : α} (h : ¬ a < b) : b ≤ a := by
+  cases LinearOrder.trichotomy a b
+  next => contradiction
+  next h => apply PartialOrder.le_iff_lt_or_eq.mpr; cases h <;> simp [*]
+
+theorem lt_of_not_le {α} [LinearOrder α] {a b : α} (h : ¬ a ≤ b) : b < a := by
+  cases LinearOrder.trichotomy a b
+  next h₁ h₂ => have := Preorder.lt_iff_le_not_le.mp h₂; simp [h] at this
+  next h =>
+    cases h
+    next h => subst a; exact False.elim <| h (Preorder.le_refl b)
+    next => assumption
+
 end LinearOrder
 
 end Lean.Grind

src/Init/Grind/Tactics.lean

@@ -55,7 +55,7 @@ and stores `c` in `x`, `b` in `a`, and the proof that `c = some b` in `h`.
 -/
 def genPattern {α : Sort u} (_h : Prop) (x : α) (_val : α) : α := x
 
-/-- Similar to `genPattern` but for the heterogenous case -/
+/-- Similar to `genPattern` but for the heterogeneous case -/
 def genHEqPattern {α β : Sort u} (_h : Prop) (x : α) (_val : β) : α := x
 end Lean.Grind
 
@@ -175,7 +175,7 @@ structure Config where
   -/
   zeta := true
   /--
-  When `true` (default: `false`), uses procedure for handling equalities over commutative rings.
+  When `true` (default: `true`), uses procedure for handling equalities over commutative rings.
   -/
   ring := true
   ringSteps := 10000
@@ -184,6 +184,11 @@ structure Config where
   proof terms, instead of a single-step Nullstellensatz certificate
   -/
   ringNull := false
+  /--
+  When `true` (default: `true`), uses procedure for handling linear arithmetic for `IntModule`, and
+  `CommRing`.
+  -/
+  linarith := true
   deriving Inhabited, BEq
 
 end Lean.Grind

src/Init/Grind/ToInt.lean

@@ -0,0 +1,513 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+
+import Init.Data.Int.DivMod.Basic
+import Init.Data.Int.Lemmas
+import Init.Data.Int.Order
+import Init.Data.Fin.Lemmas
+import Init.Data.UInt.Lemmas
+import Init.Data.SInt.Lemmas
+
+/-!
+# Typeclasses for types that can be embedded into an interval of `Int`.
+
+The typeclass `ToInt α lo? hi?` carries the data of a function `ToInt.toInt : α → Int`
+which is injective, lands between the (optional) lower and upper bounds `lo?` and `hi?`.
+
+The function `ToInt.wrap` is the identity if either bound is `none`,
+and otherwise wraps the integers into the interval `[lo, hi)`.
+
+The typeclass `ToInt.Add α lo? hi?` then asserts that `toInt (x + y) = wrap lo? hi? (toInt x + toInt y)`.
+There are many variants for other operations.
+
+These typeclasses are used solely in the `grind` tactic to lift linear inequalities into `Int`.
+-/
+
+namespace Lean.Grind
+
+class ToInt (α : Type u) (lo? hi? : outParam (Option Int)) where
+  toInt : α → Int
+  toInt_inj : ∀ x y, toInt x = toInt y → x = y
+  le_toInt : lo? = some lo → lo ≤ toInt x
+  toInt_lt : hi? = some hi → toInt x < hi
+
+@[simp]
+def ToInt.wrap (lo? hi? : Option Int) (x : Int) : Int :=
+  match lo?, hi? with
+  | some lo, some hi => (x - lo) % (hi - lo) + lo
+  | _, _ => x
+
+class ToInt.Zero (α : Type u) [Zero α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where
+  toInt_zero : toInt (0 : α) = wrap lo? hi? 0
+
+class ToInt.Add (α : Type u) [Add α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where
+  toInt_add : ∀ x y : α, toInt (x + y) = wrap lo? hi? (toInt x + toInt y)
+
+class ToInt.Neg (α : Type u) [Neg α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where
+  toInt_neg : ∀ x : α, toInt (-x) = wrap lo? hi? (-toInt x)
+
+class ToInt.Sub (α : Type u) [Sub α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where
+  toInt_sub : ∀ x y : α, toInt (x - y) = wrap lo? hi? (toInt x - toInt y)
+
+class ToInt.Mod (α : Type u) [Mod α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where
+  /-- One might expect a `wrap` on the right hand side,
+  but in practice this stronger statement is usually true. -/
+  toInt_mod : ∀ x y : α, toInt (x % y) = toInt x % toInt y
+
+class ToInt.LE (α : Type u) [LE α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where
+  le_iff : ∀ x y : α, x ≤ y ↔ toInt x ≤ toInt y
+
+class ToInt.LT (α : Type u) [LT α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where
+  lt_iff : ∀ x y : α, x < y ↔ toInt x < toInt y
+
+/-! ## Helper theorems -/
+
+theorem ToInt.wrap_add (lo? hi? : Option Int) (x y : Int) :
+    ToInt.wrap lo? hi? (x + y) = ToInt.wrap lo? hi? (ToInt.wrap lo? hi? x + ToInt.wrap lo? hi? y) := by
+  simp only [wrap]
+  split <;> rename_i lo hi
+  · dsimp
+    rw [Int.add_left_inj, Int.emod_eq_emod_iff_emod_sub_eq_zero, Int.emod_def (x - lo), Int.emod_def (y - lo)]
+    have : (x + y - lo -
+        (x - lo - (hi - lo) * ((x - lo) / (hi - lo)) + lo +
+          (y - lo - (hi - lo) * ((y - lo) / (hi - lo)) + lo) - lo)) =
+        (hi - lo) * ((x - lo) / (hi - lo) + (y - lo) / (hi - lo)) := by
+      simp only [Int.mul_add]
+      omega
+    rw [this]
+    exact Int.mul_emod_right ..
+  · simp
+
+@[simp]
+theorem ToInt.wrap_toInt (lo? hi? : Option Int) [ToInt α lo? hi?] (x : α) :
+    ToInt.wrap lo? hi? (ToInt.toInt x) = ToInt.toInt x := by
+  simp only [wrap]
+  split
+  · have := ToInt.le_toInt (x := x) rfl
+    have := ToInt.toInt_lt (x := x) rfl
+    rw [Int.emod_eq_of_lt (by omega) (by omega)]
+    omega
+  · rfl
+
+theorem ToInt.wrap_eq_bmod {i : Int} (h : 0 ≤ i) :
+    ToInt.wrap (some (-i)) (some i) x = x.bmod ((2 * i).toNat) := by
+  match i, h with
+  | (i : Nat), _ =>
+    have : (2 * (i : Int)).toNat = 2 * i := by omega
+    rw [this]
+    simp [Int.bmod_eq_emod, ← Int.two_mul]
+    have : (2 * (i : Int) + 1) / 2 = i := by omega
+    rw [this]
+    by_cases h : i = 0
+    · simp [h]
+    split
+    · rw [← Int.sub_eq_add_neg, Int.sub_eq_iff_eq_add, Nat.two_mul, Int.natCast_add,
+        ← Int.sub_sub, Int.sub_add_cancel]
+      rw [Int.emod_eq_iff (by omega)]
+      refine ⟨?_, ?_, ?_⟩
+      · omega
+      · have := Int.emod_lt x (b := 2 * (i : Int)) (by omega)
+        omega
+      · rw [Int.emod_def]
+        have : x - 2 * ↑i * (x / (2 * ↑i)) - ↑i - (x + ↑i) = (2 * (i : Int)) * (- (x / (2 * i)) - 1) := by
+          simp only [Int.mul_sub, Int.mul_neg]
+          omega
+        rw [this]
+        exact Int.dvd_mul_right ..
+    · rw [← Int.sub_eq_add_neg, Int.sub_eq_iff_eq_add, Int.natCast_zero, Int.sub_zero]
+      rw [Int.emod_eq_iff (by omega)]
+      refine ⟨?_, ?_, ?_⟩
+      · have := Int.emod_nonneg x (b := 2 * (i : Int)) (by omega)
+        omega
+      · omega
+      · rw [Int.emod_def]
+        have : x - 2 * ↑i * (x / (2 * ↑i)) + ↑i - (x + ↑i) = (2 * (i : Int)) * (- (x / (2 * i))) := by
+          simp only [Int.mul_neg]
+          omega
+        rw [this]
+        exact Int.dvd_mul_right ..
+
+theorem ToInt.wrap_eq_wrap_iff :
+    ToInt.wrap (some lo) (some hi) x = ToInt.wrap (some lo) (some hi) y ↔ (x - y) % (hi - lo) = 0 := by
+  simp only [wrap]
+  rw [Int.add_left_inj]
+  rw [Int.emod_eq_emod_iff_emod_sub_eq_zero]
+  have : x - lo - (y - lo)  = x - y := by omega
+  rw [this]
+
+/-- Construct a `ToInt.Sub` instance from a `ToInt.Add` and `ToInt.Neg` instance and
+a `sub_eq_add_neg` assumption. -/
+def ToInt.Sub.of_sub_eq_add_neg {α : Type u} [_root_.Add α] [_root_.Neg α] [_root_.Sub α]
+    (sub_eq_add_neg : ∀ x y : α, x - y = x + -y)
+    {lo? hi? : Option Int} [ToInt α lo? hi?] [Add α lo? hi?] [Neg α lo? hi?] : ToInt.Sub α lo? hi? where
+  toInt_sub x y := by
+    rw [sub_eq_add_neg, ToInt.Add.toInt_add, ToInt.Neg.toInt_neg, Int.sub_eq_add_neg]
+    conv => rhs; rw [ToInt.wrap_add, ToInt.wrap_toInt]
+
+/-! ## Instances for concrete types-/
+
+instance : ToInt Int none none where
+  toInt := id
+  toInt_inj := by simp
+  le_toInt := by simp
+  toInt_lt := by simp
+
+@[simp] theorem toInt_int (x : Int) : ToInt.toInt x = x := rfl
+
+instance : ToInt.Add Int none none where
+  toInt_add := by simp
+
+instance : ToInt.Neg Int none none where
+  toInt_neg x := by simp
+
+instance : ToInt.Sub Int none none where
+  toInt_sub x y := by simp
+
+instance : ToInt.Mod Int none none where
+  toInt_mod x y := by simp
+
+instance : ToInt.LE Int none none where
+  le_iff x y := by simp
+
+instance : ToInt.LT Int none none where
+  lt_iff x y := by simp
+
+instance : ToInt Nat (some 0) none where
+  toInt := Nat.cast
+  toInt_inj x y := Int.ofNat_inj.mp
+  le_toInt {lo x} w := by simp at w; subst w; exact Int.natCast_nonneg x
+  toInt_lt := by simp
+
+@[simp] theorem toInt_nat (x : Nat) : ToInt.toInt x = (x : Int) := rfl
+
+instance : ToInt.Add Nat (some 0) none where
+  toInt_add := by simp
+
+instance : ToInt.Mod Nat (some 0) none where
+  toInt_mod x y := by simp
+
+instance : ToInt.LE Nat (some 0) none where
+  le_iff x y := by simp
+
+instance : ToInt.LT Nat (some 0) none where
+  lt_iff x y := by simp
+
+-- Mathlib will add a `ToInt ℕ+ (some 1) none` instance.
+
+instance : ToInt (Fin n) (some 0) (some n) where
+  toInt x := x.val
+  toInt_inj x y w := Fin.eq_of_val_eq (Int.ofNat_inj.mp w)
+  le_toInt {lo x} w := by simp only [Option.some.injEq] at w; subst w; exact Int.natCast_nonneg x
+  toInt_lt {hi x} w := by simp only [Option.some.injEq] at w; subst w; exact Int.ofNat_lt.mpr x.isLt
+
+@[simp] theorem toInt_fin (x : Fin n) : ToInt.toInt x = (x.val : Int) := rfl
+
+instance : ToInt.Add (Fin n) (some 0) (some n) where
+  toInt_add x y := by rfl
+
+instance [NeZero n] : ToInt.Zero (Fin n) (some 0) (some n) where
+  toInt_zero := by rfl
+
+-- The `ToInt.Neg` and `ToInt.Sub` instances are generated automatically from the `IntModule (Fin n)` instance.
+
+instance : ToInt.Mod (Fin n) (some 0) (some n) where
+  toInt_mod x y := by
+    simp only [toInt_fin, Fin.mod_val, Int.natCast_emod]
+
+instance : ToInt.LE (Fin n) (some 0) (some n) where
+  le_iff x y := by simpa using Fin.le_def
+
+instance : ToInt.LT (Fin n) (some 0) (some n) where
+  lt_iff x y := by simpa using Fin.lt_def
+
+instance : ToInt UInt8 (some 0) (some (2^8)) where
+  toInt x := (x.toNat : Int)
+  toInt_inj x y w := UInt8.toNat_inj.mp (Int.ofNat_inj.mp w)
+  le_toInt {lo x} w := by simp at w; subst w; exact Int.natCast_nonneg x.toNat
+  toInt_lt {hi x} w := by simp at w; subst w; exact Int.lt_toNat.mp (UInt8.toNat_lt x)
+
+@[simp] theorem toInt_uint8 (x : UInt8) : ToInt.toInt x = (x.toNat : Int) := rfl
+
+instance : ToInt.Add UInt8 (some 0) (some (2^8)) where
+  toInt_add x y := by simp
+
+instance : ToInt.Zero UInt8 (some 0) (some (2^8)) where
+  toInt_zero := by simp
+
+instance : ToInt.Mod UInt8 (some 0) (some (2^8)) where
+  toInt_mod x y := by simp
+
+instance : ToInt.LE UInt8 (some 0) (some (2^8)) where
+  le_iff x y := by simpa using UInt8.le_iff_toBitVec_le
+
+instance : ToInt.LT UInt8 (some 0) (some (2^8)) where
+  lt_iff x y := by simpa using UInt8.lt_iff_toBitVec_lt
+
+instance : ToInt UInt16 (some 0) (some (2^16)) where
+  toInt x := (x.toNat : Int)
+  toInt_inj x y w := UInt16.toNat_inj.mp (Int.ofNat_inj.mp w)
+  le_toInt {lo x} w := by simp at w; subst w; exact Int.natCast_nonneg x.toNat
+  toInt_lt {hi x} w := by simp at w; subst w; exact Int.lt_toNat.mp (UInt16.toNat_lt x)
+
+@[simp] theorem toInt_uint16 (x : UInt16) : ToInt.toInt x = (x.toNat : Int) := rfl
+
+instance : ToInt.Add UInt16 (some 0) (some (2^16)) where
+  toInt_add x y := by simp
+
+instance : ToInt.Zero UInt16 (some 0) (some (2^16)) where
+  toInt_zero := by simp
+
+instance : ToInt.Mod UInt16 (some 0) (some (2^16)) where
+  toInt_mod x y := by simp
+
+instance : ToInt.LE UInt16 (some 0) (some (2^16)) where
+  le_iff x y := by simpa using UInt16.le_iff_toBitVec_le
+
+instance : ToInt.LT UInt16 (some 0) (some (2^16)) where
+  lt_iff x y := by simpa using UInt16.lt_iff_toBitVec_lt
+
+instance : ToInt UInt32 (some 0) (some (2^32)) where
+  toInt x := (x.toNat : Int)
+  toInt_inj x y w := UInt32.toNat_inj.mp (Int.ofNat_inj.mp w)
+  le_toInt {lo x} w := by simp at w; subst w; exact Int.natCast_nonneg x.toNat
+  toInt_lt {hi x} w := by simp at w; subst w; exact Int.lt_toNat.mp (UInt32.toNat_lt x)
+
+@[simp] theorem toInt_uint32 (x : UInt32) : ToInt.toInt x = (x.toNat : Int) := rfl
+
+instance : ToInt.Add UInt32 (some 0) (some (2^32)) where
+  toInt_add x y := by simp
+
+instance : ToInt.Zero UInt32 (some 0) (some (2^32)) where
+  toInt_zero := by simp
+
+instance : ToInt.Mod UInt32 (some 0) (some (2^32)) where
+  toInt_mod x y := by simp
+
+instance : ToInt.LE UInt32 (some 0) (some (2^32)) where
+  le_iff x y := by simpa using UInt32.le_iff_toBitVec_le
+
+instance : ToInt.LT UInt32 (some 0) (some (2^32)) where
+  lt_iff x y := by simpa using UInt32.lt_iff_toBitVec_lt
+
+instance : ToInt UInt64 (some 0) (some (2^64)) where
+  toInt x := (x.toNat : Int)
+  toInt_inj x y w := UInt64.toNat_inj.mp (Int.ofNat_inj.mp w)
+  le_toInt {lo x} w := by simp at w; subst w; exact Int.natCast_nonneg x.toNat
+  toInt_lt {hi x} w := by simp at w; subst w; exact Int.lt_toNat.mp (UInt64.toNat_lt x)
+
+@[simp] theorem toInt_uint64 (x : UInt64) : ToInt.toInt x = (x.toNat : Int) := rfl
+
+instance : ToInt.Add UInt64 (some 0) (some (2^64)) where
+  toInt_add x y := by simp
+
+instance : ToInt.Zero UInt64 (some 0) (some (2^64)) where
+  toInt_zero := by simp
+
+instance : ToInt.Mod UInt64 (some 0) (some (2^64)) where
+  toInt_mod x y := by simp
+
+instance : ToInt.LE UInt64 (some 0) (some (2^64)) where
+  le_iff x y := by simpa using UInt64.le_iff_toBitVec_le
+
+instance : ToInt.LT UInt64 (some 0) (some (2^64)) where
+  lt_iff x y := by simpa using UInt64.lt_iff_toBitVec_lt
+
+instance : ToInt USize (some 0) (some (2^System.Platform.numBits)) where
+  toInt x := (x.toNat : Int)
+  toInt_inj x y w := USize.toNat_inj.mp (Int.ofNat_inj.mp w)
+  le_toInt {lo x} w := by simp at w; subst w; exact Int.natCast_nonneg x.toNat
+  toInt_lt {hi x} w := by
+    simp at w; subst w
+    rw [show (2 : Int) ^ System.Platform.numBits = (2 ^ System.Platform.numBits : Nat) by simp,
+      Int.ofNat_lt]
+    exact USize.toNat_lt_two_pow_numBits x
+
+@[simp] theorem toInt_usize (x : USize) : ToInt.toInt x = (x.toNat : Int) := rfl
+
+instance : ToInt.Add USize (some 0) (some (2^System.Platform.numBits)) where
+  toInt_add x y := by simp
+
+instance : ToInt.Zero USize (some 0) (some (2^System.Platform.numBits)) where
+  toInt_zero := by simp
+
+instance : ToInt.Mod USize (some 0) (some (2^System.Platform.numBits)) where
+  toInt_mod x y := by simp
+
+instance : ToInt.LE USize (some 0) (some (2^System.Platform.numBits)) where
+  le_iff x y := by simpa using USize.le_iff_toBitVec_le
+
+instance : ToInt.LT USize (some 0) (some (2^System.Platform.numBits)) where
+  lt_iff x y := by simpa using USize.lt_iff_toBitVec_lt
+
+instance : ToInt Int8 (some (-2^7)) (some (2^7)) where
+  toInt x := x.toInt
+  toInt_inj x y w := Int8.toInt_inj.mp w
+  le_toInt {lo x} w := by simp at w; subst w; exact Int8.le_toInt x
+  toInt_lt {hi x} w := by simp at w; subst w; exact Int8.toInt_lt x
+
+@[simp] theorem toInt_int8 (x : Int8) : ToInt.toInt x = (x.toInt : Int) := rfl
+
+instance : ToInt.Add Int8 (some (-2^7)) (some (2^7)) where
+  toInt_add x y := by
+    simp [Int.bmod_eq_emod]
+    split <;> · simp; omega
+
+instance : ToInt.Zero Int8 (some (-2^7)) (some (2^7)) where
+  toInt_zero := by
+    --  simp -- FIXME: succeeds, but generates a `(kernel) application type mismatch` error!
+    change (0 : Int8).toInt = _
+    rw [Int8.toInt_zero]
+    decide
+
+-- Note that we can not define `ToInt.Mod` instances for `Int8`,
+-- because the condition does not hold unless `0 ≤ x.toInt ∨ y.toInt ∣ x.toInt ∨ y = 0`.
+
+instance : ToInt.LE Int8 (some (-2^7)) (some (2^7)) where
+  le_iff x y := by simpa using Int8.le_iff_toInt_le
+
+instance : ToInt.LT Int8 (some (-2^7)) (some (2^7)) where
+  lt_iff x y := by simpa using Int8.lt_iff_toInt_lt
+
+instance : ToInt Int16 (some (-2^15)) (some (2^15)) where
+  toInt x := x.toInt
+  toInt_inj x y w := Int16.toInt_inj.mp w
+  le_toInt {lo x} w := by simp at w; subst w; exact Int16.le_toInt x
+  toInt_lt {hi x} w := by simp at w; subst w; exact Int16.toInt_lt x
+
+@[simp] theorem toInt_int16 (x : Int16) : ToInt.toInt x = (x.toInt : Int) := rfl
+
+instance : ToInt.Add Int16 (some (-2^15)) (some (2^15)) where
+  toInt_add x y := by
+    simp [Int.bmod_eq_emod]
+    split <;> · simp; omega
+
+instance : ToInt.Zero Int16 (some (-2^15)) (some (2^15)) where
+  toInt_zero := by
+    -- simp -- FIXME: succeeds, but generates a `(kernel) application type mismatch` error!
+    change (0 : Int16).toInt = _
+    rw [Int16.toInt_zero]
+    decide
+
+instance : ToInt.LE Int16 (some (-2^15)) (some (2^15)) where
+  le_iff x y := by simpa using Int16.le_iff_toInt_le
+
+instance : ToInt.LT Int16 (some (-2^15)) (some (2^15)) where
+  lt_iff x y := by simpa using Int16.lt_iff_toInt_lt
+
+instance : ToInt Int32 (some (-2^31)) (some (2^31)) where
+  toInt x := x.toInt
+  toInt_inj x y w := Int32.toInt_inj.mp w
+  le_toInt {lo x} w := by simp at w; subst w; exact Int32.le_toInt x
+  toInt_lt {hi x} w := by simp at w; subst w; exact Int32.toInt_lt x
+
+@[simp] theorem toInt_int32 (x : Int32) : ToInt.toInt x = (x.toInt : Int) := rfl
+
+instance : ToInt.Add Int32 (some (-2^31)) (some (2^31)) where
+  toInt_add x y := by
+    simp [Int.bmod_eq_emod]
+    split <;> · simp; omega
+
+instance : ToInt.Zero Int32 (some (-2^31)) (some (2^31)) where
+  toInt_zero := by
+    -- simp -- FIXME: succeeds, but generates a `(kernel) application type mismatch` error!
+    change (0 : Int32).toInt = _
+    rw [Int32.toInt_zero]
+    decide
+
+instance : ToInt.LE Int32 (some (-2^31)) (some (2^31)) where
+  le_iff x y := by simpa using Int32.le_iff_toInt_le
+
+instance : ToInt.LT Int32 (some (-2^31)) (some (2^31)) where
+  lt_iff x y := by simpa using Int32.lt_iff_toInt_lt
+
+instance : ToInt Int64 (some (-2^63)) (some (2^63)) where
+  toInt x := x.toInt
+  toInt_inj x y w := Int64.toInt_inj.mp w
+  le_toInt {lo x} w := by simp at w; subst w; exact Int64.le_toInt x
+  toInt_lt {hi x} w := by simp at w; subst w; exact Int64.toInt_lt x
+
+@[simp] theorem toInt_int64 (x : Int64) : ToInt.toInt x = (x.toInt : Int) := rfl
+
+instance : ToInt.Add Int64 (some (-2^63)) (some (2^63)) where
+  toInt_add x y := by
+    simp [Int.bmod_eq_emod]
+    split <;> · simp; omega
+
+instance : ToInt.Zero Int64 (some (-2^63)) (some (2^63)) where
+  toInt_zero := by
+    -- simp -- FIXME: succeeds, but generates a `(kernel) application type mismatch` error!
+    change (0 : Int64).toInt = _
+    rw [Int64.toInt_zero]
+    decide
+
+instance : ToInt.LE Int64 (some (-2^63)) (some (2^63)) where
+  le_iff x y := by simpa using Int64.le_iff_toInt_le
+
+instance : ToInt.LT Int64 (some (-2^63)) (some (2^63)) where
+  lt_iff x y := by simpa using Int64.lt_iff_toInt_lt
+
+instance : ToInt (BitVec v) (some 0) (some (2^v)) where
+  toInt x := (x.toNat : Int)
+  toInt_inj x y w :=
+    BitVec.eq_of_toNat_eq (Int.ofNat_inj.mp w)
+  le_toInt {lo x} w := by simp at w; subst w; exact Int.natCast_nonneg x.toNat
+  toInt_lt {hi x} w := by
+    simp at w; subst w;
+    simpa using Int.ofNat_lt.mpr (BitVec.isLt x)
+
+@[simp] theorem toInt_bitVec (x : BitVec v) : ToInt.toInt x = (x.toNat : Int) := rfl
+
+instance : ToInt.Add (BitVec v) (some 0) (some (2^v)) where
+  toInt_add x y := by simp
+
+instance : ToInt.Zero (BitVec v) (some 0) (some (2^v)) where
+  toInt_zero := by simp
+
+instance : ToInt.Mod (BitVec v) (some 0) (some (2^v)) where
+  toInt_mod x y := by simp
+
+instance : ToInt.LE (BitVec v) (some 0) (some (2^v)) where
+  le_iff x y := by simpa using BitVec.le_def
+
+instance : ToInt.LT (BitVec v) (some 0) (some (2^v)) where
+  lt_iff x y := by simpa using BitVec.lt_def
+
+instance : ToInt ISize (some (-2^(System.Platform.numBits-1))) (some (2^(System.Platform.numBits-1))) where
+  toInt x := x.toInt
+  toInt_inj x y w := ISize.toInt_inj.mp w
+  le_toInt {lo x} w := by simp at w; subst w; exact ISize.two_pow_numBits_le_toInt x
+  toInt_lt {hi x} w := by simp at w; subst w; exact ISize.toInt_lt_two_pow_numBits x
+
+@[simp] theorem toInt_isize (x : ISize) : ToInt.toInt x = x.toInt := rfl
+
+instance : ToInt.Add ISize (some (-2^(System.Platform.numBits-1))) (some (2^(System.Platform.numBits-1))) where
+  toInt_add x y := by
+    rw [toInt_isize, ISize.toInt_add, ToInt.wrap_eq_bmod (Int.pow_nonneg (by decide))]
+    have p₁ : (2 : Int) * 2 ^ (System.Platform.numBits - 1) = 2 ^ System.Platform.numBits := by
+      have := System.Platform.numBits_pos
+      have : System.Platform.numBits - 1 + 1 = System.Platform.numBits := by omega
+      simp [← Int.pow_succ', this]
+    have p₂ : ((2 : Int) ^ System.Platform.numBits).toNat = 2 ^ System.Platform.numBits := by
+      rw [Int.toNat_pow_of_nonneg (by decide)]
+      simp
+    simp [p₁, p₂]
+
+instance : ToInt.Zero ISize (some (-2^(System.Platform.numBits-1))) (some (2^(System.Platform.numBits-1))) where
+  toInt_zero := by
+    rw [toInt_isize]
+    rw [ISize.toInt_zero, ToInt.wrap_eq_bmod (Int.pow_nonneg (by decide))]
+    simp
+
+instance instToIntLEISize : ToInt.LE ISize (some (-2^(System.Platform.numBits-1))) (some (2^(System.Platform.numBits-1))) where
+  le_iff x y := by simpa using ISize.le_iff_toInt_le
+
+instance instToIntLTISize : ToInt.LT ISize (some (-2^(System.Platform.numBits-1))) (some (2^(System.Platform.numBits-1))) where
+  lt_iff x y := by simpa using ISize.lt_iff_toInt_lt
+
+end Lean.Grind

src/Init/System/IO.lean

@@ -149,7 +149,7 @@ Because the resulting value is treated as a side-effect-free term, the compiler
 duplicate, or delete calls to this function. The side effect may even be hoisted into a constant,
 causing the side effect to occur at initialization time, even if it would otherwise never be called.
 -/
-@[inline] unsafe def unsafeBaseIO (fn : BaseIO α) : α :=
+@[noinline] unsafe def unsafeBaseIO (fn : BaseIO α) : α :=
   match fn.run () with
   | EStateM.Result.ok a _ => a
 
@@ -567,7 +567,7 @@ def addHeartbeats (count : Nat) : BaseIO Unit := do
 /--
 Whether a file should be opened for reading, writing, creation and writing, or appending.
 
-A the operating system level, this translates to the mode of a file handle (i.e., a set of `open`
+At the operating system level, this translates to the mode of a file handle (i.e., a set of `open`
 flags and an `fdopen` mode).
 
 None of the modes represented by this datatype translate line endings (i.e. `O_BINARY` on Windows).

src/Init/Tactics.lean

@@ -1917,30 +1917,35 @@ syntax "‹" withoutPosition(term) "›" : term
 macro_rules | `(‹$type›) => `((by assumption : $type))
 
 /--
-`get_elem_tactic_trivial` is an extensible tactic automatically called
+`get_elem_tactic_extensible` is an extensible tactic automatically called
 by the notation `arr[i]` to prove any side conditions that arise when
 constructing the term (e.g. the index is in bounds of the array).
-The default behavior is to just try `trivial` (which handles the case
-where `i < arr.size` is in the context) and `simp +arith` and `omega`
+The default behavior is to try `simp +arith` and `omega`
 (for doing linear arithmetic in the index).
+
+(Note that the core tactic `get_elem_tactic` has already tried
+`done` and `assumption` before the extensible tactic is called.)
 -/
+syntax "get_elem_tactic_extensible" : tactic
+
+/-- `get_elem_tactic_trivial` has been deprecated in favour of `get_elem_tactic_extensible`. -/
 syntax "get_elem_tactic_trivial" : tactic
 
-macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| omega)
-macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| simp +arith; done)
-macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| trivial)
+macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| omega)
+macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| simp +arith; done)
+macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| trivial)
 
 /--
 `get_elem_tactic` is the tactic automatically called by the notation `arr[i]`
 to prove any side conditions that arise when constructing the term
 (e.g. the index is in bounds of the array). It just delegates to
-`get_elem_tactic_trivial` and gives a diagnostic error message otherwise;
-users are encouraged to extend `get_elem_tactic_trivial` instead of this tactic.
+`get_elem_tactic_extensible` and gives a diagnostic error message otherwise;
+users are encouraged to extend `get_elem_tactic_extensible` instead of this tactic.
 -/
 macro "get_elem_tactic" : tactic =>
   `(tactic| first
       /-
-      Recall that `macro_rules` (namely, for `get_elem_tactic_trivial`) are tried in reverse order.
+      Recall that `macro_rules` (namely, for `get_elem_tactic_extensible`) are tried in reverse order.
       We first, however, try `done`, since the necessary proof may already have been
       found during unification, in which case there is no goal to solve (see #6999).
       If a goal is present, we want `assumption` to be tried first.
@@ -1953,15 +1958,15 @@ macro "get_elem_tactic" : tactic =>
       If `omega` is used to "fill" this proof, we will have a more complex proof term that
       cannot be inferred by unification.
       We hardcoded `assumption` here to ensure users cannot accidentally break this IF
-      they add new `macro_rules` for `get_elem_tactic_trivial`.
+      they add new `macro_rules` for `get_elem_tactic_extensible`.
 
       TODO: Implement priorities for `macro_rules`.
-      TODO: Ensure we have **high-priority** macro_rules for `get_elem_tactic_trivial` which are
+      TODO: Ensure we have **high-priority** macro_rules for `get_elem_tactic_extensible` which are
             just `done` and `assumption`.
       -/
     | done
     | assumption
-    | get_elem_tactic_trivial
+    | get_elem_tactic_extensible
     | fail "failed to prove index is valid, possible solutions:
   - Use `have`-expressions to prove the index is valid
   - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid

src/Lean.lean

@@ -41,3 +41,4 @@ import Lean.PrivateName
 import Lean.PremiseSelection
 import Lean.Namespace
 import Lean.EnvExtension
+import Lean.DefEqAttrib

src/Lean/AddDecl.lean

@@ -64,13 +64,6 @@ Checks whether the declaration was originally declared as a theorem; see also
 def wasOriginallyTheorem (env : Environment) (declName : Name) : Bool :=
   getOriginalConstKind? env declName |>.map (· matches .thm) |>.getD false
 
--- HACK: remove together with MutualDef HACK when `[dsimp]` is introduced
-private def isSimpleRflProof (proof : Expr) : Bool :=
-  if let .lam _ _ proof _ := proof then
-    isSimpleRflProof proof
-  else
-    proof.isAppOfArity ``rfl 2
-
 private def looksLikeRelevantTheoremProofType (type : Expr) : Bool :=
   if let .forallE _ _ type _ := type then
     looksLikeRelevantTheoremProofType type
@@ -90,9 +83,6 @@ def addDecl (decl : Declaration) : CoreM Unit := do
   let (name, info, kind) ← match decl with
     | .thmDecl thm =>
       let exportProof := !(← getEnv).header.isModule ||
-        -- We should preserve rfl theorems but also we should not override a decision to hide by the
-        -- MutualDef elaborator via `withoutExporting`
-        (← getEnv).isExporting && isSimpleRflProof thm.value ||
         -- TODO: this is horrible...
         looksLikeRelevantTheoremProofType thm.type
       if !exportProof then

src/Lean/Attributes.lean

@@ -135,7 +135,9 @@ structure TagAttribute where
   deriving Inhabited
 
 def registerTagAttribute (name : Name) (descr : String)
-    (validate : Name → AttrM Unit := fun _ => pure ()) (ref : Name := by exact decl_name%) (applicationTime := AttributeApplicationTime.afterTypeChecking) : IO TagAttribute := do
+    (validate : Name → AttrM Unit := fun _ => pure ()) (ref : Name := by exact decl_name%)
+    (applicationTime := AttributeApplicationTime.afterTypeChecking)
+    (asyncMode : EnvExtension.AsyncMode := .mainOnly) : IO TagAttribute := do
   let ext : PersistentEnvExtension Name Name NameSet ← registerPersistentEnvExtension {
     name            := ref
     mkInitial       := pure {}
@@ -145,6 +147,12 @@ def registerTagAttribute (name : Name) (descr : String)
       let r : Array Name := es.fold (fun a e => a.push e) #[]
       r.qsort Name.quickLt
     statsFn         := fun s => "tag attribute" ++ Format.line ++ "number of local entries: " ++ format s.size
+    asyncMode       := asyncMode
+    replay?         := some fun _ newState newConsts s =>
+      newConsts.foldl (init := s) fun s c =>
+        if newState.contains c then
+          s.insert c
+        else s
   }
   let attrImpl : AttributeImpl := {
     ref, name, descr, applicationTime
@@ -153,7 +161,9 @@ def registerTagAttribute (name : Name) (descr : String)
       unless kind == AttributeKind.global do throwError "invalid attribute '{name}', must be global"
       let env ← getEnv
       unless (env.getModuleIdxFor? decl).isNone do
-        throwError "invalid attribute '{name}', declaration is in an imported module"
+        throwError "invalid attribute '{name}', declaration {.ofConstName decl} is in an imported module"
+      unless env.asyncMayContain decl do
+        throwError "invalid attribute '{name}', declaration {.ofConstName decl} is not from the present async context {env.asyncPrefix?}"
       validate decl
       modifyEnv fun env => ext.addEntry env decl
   }
@@ -162,10 +172,27 @@ def registerTagAttribute (name : Name) (descr : String)
 
 namespace TagAttribute
 
+/-- Sets the attribute (without running `validate`) -/
+def setTag  [Monad m] [MonadError m] [MonadEnv m] (attr : TagAttribute) (decl : Name) : m Unit := do
+  let env ← getEnv
+  unless (env.getModuleIdxFor? decl).isNone do
+    throwError "invalid attribute '{attr.attr.name}', declaration {.ofConstName decl} is in an imported module"
+  unless env.asyncMayContain decl do
+    throwError "invalid attribute '{attr.attr.name}', declaration {.ofConstName decl} is not from the present async context {env.asyncPrefix?}"
+  modifyEnv fun env => attr.ext.addEntry env decl
+
 def hasTag (attr : TagAttribute) (env : Environment) (decl : Name) : Bool :=
   match env.getModuleIdxFor? decl with
   | some modIdx => (attr.ext.getModuleEntries env modIdx).binSearchContains decl Name.quickLt
-  | none        => (attr.ext.getState env).contains decl
+  | none        =>
+    if attr.ext.toEnvExtension.asyncMode matches .async then
+      -- It seems that the env extension API doesn't quite allow querying attributes in a way
+      -- that works for realizable constants, but without waiting on proofs to finish.
+      -- Until then, we use the following overapproximation, to be refined later:
+      (attr.ext.findStateAsync env decl).contains decl ||
+      (attr.ext.getState env (asyncMode := .local)).contains decl
+    else
+      (attr.ext.getState env).contains decl
 
 end TagAttribute
 

src/Lean/BuiltinDocAttr.lean

@@ -15,7 +15,15 @@ def declareBuiltinDocStringAndRanges (declName : Name) : AttrM Unit := do
   if let some declRanges ← findDeclarationRanges? declName then
     declareBuiltin (declName ++ `declRange) (mkAppN (mkConst ``addBuiltinDeclarationRanges) #[toExpr declName, toExpr declRanges])
 
-builtin_initialize
+/--
+Makes the documentation and location of a declaration available as a builtin.
+
+This allows the documentation of core Lean features to be visible without importing the file they
+are defined in. This is only useful during bootstrapping and should not be used outside of
+the Lean source code.
+-/
+@[builtin_init, builtin_doc]
+private def initFn :=
   registerBuiltinAttribute {
     name  := `builtin_doc
     descr := "make the docs and location of this declaration available as a builtin"

src/Lean/Class.lean

@@ -159,7 +159,12 @@ def addClass (env : Environment) (clsName : Name) : Except MessageData Environme
   let outParams ← checkOutParam 0 #[] #[] decl.type
   return classExtension.addEntry env { name := clsName, outParams }
 
-builtin_initialize
+/--
+Registers an inductive type or structure as a type class. Using `class` or `class inductive` is
+generally preferred over using `@[class] structure` or `@[class] inductive` directly.
+-/
+@[builtin_init, builtin_doc]
+private def init :=
   registerBuiltinAttribute {
     name  := `class
     descr := "type class"

src/Lean/Compiler/CSimpAttr.lean

@@ -48,7 +48,22 @@ def add (declName : Name) (kind : AttributeKind) : CoreM Unit := do
   else
     throwError "invalid 'csimp' theorem, only constant replacement theorems (e.g., `@f = @g`) are currently supported."
 
-builtin_initialize
+/--
+Tags compiler simplification theorems, which allow one value to be replaced by another equal value
+in compiled code. This is typically used to replace a slow function whose definition is convenient
+in proofs with a faster equivalent or to make noncomputable functions computable. In particular,
+many operations on lists and arrays are replaced by tail-recursive equivalents.
+
+A compiler simplification theorem cannot take any parameters and must prove a statement `@f = @g`
+where `f` and `g` may be arbitrary constants. In functions defined after the theorem tagged
+`@[csimp]`, any occurrence of `f` is replaced with `g` in compiled code, but not in the type
+theory. In this sense, `@[csimp]` is a safer alternative to `@[implemented_by]`.
+
+However it is still possible to register unsound `@[csimp]` lemmas by using `unsafe` or unsound
+axioms (like `sorryAx`).
+-/
+@[builtin_init, builtin_doc]
+private def initFn :=
   registerBuiltinAttribute {
     name  := `csimp
     descr := "simplification theorem for the compiler"

src/Lean/Compiler/ExportAttr.lean

@@ -17,6 +17,36 @@ private def isValidCppName : Name → Bool
   | .str p s          => isValidCppId s && isValidCppName p
   | _                 => false
 
+/--
+Exports a function under the provided unmangled symbol name. This can be used to refer to Lean
+functions from other programming languages like C.
+
+Example:
+```
+@[export lean_color_from_map]
+def colorValue (properties : @& Std.HashMap String String) : UInt32 :=
+  match properties["color"]? with
+  | some "red" => 0xff0000
+  | some "green" => 0x00ff00
+  | some "blue" => 0x0000ff
+  | _ => -1
+```
+C code:
+```c
+#include <lean/lean.h>
+
+uint32_t lean_color_from_map(b_lean_obj_arg properties);
+
+void fill_rectangle_from_map(b_lean_obj_arg properties) {
+    uint32_t color = lean_color_from_map(properties);
+    // ...
+}
+```
+
+The opposite of this is `@[extern]`, which allows Lean functions to refer to functions from other
+programming languages.
+-/
+@[builtin_doc]
 builtin_initialize exportAttr : ParametricAttribute Name ←
   registerParametricAttribute {
     name := `export,

src/Lean/Compiler/IR/UnboxResult.lean

@@ -9,6 +9,12 @@ import Lean.Compiler.IR.Basic
 
 namespace Lean.IR.UnboxResult
 
+/--
+Tags types that the compiler should unbox if they occur in result values.
+
+This attribute currently has no effect.
+-/
+@[builtin_doc]
 builtin_initialize unboxAttr : TagAttribute ←
   registerTagAttribute `unbox "compiler tries to unbox result values if their types are tagged with `[unbox]`" fun declName => do
     let cinfo ← getConstInfo declName;
@@ -19,6 +25,6 @@ builtin_initialize unboxAttr : TagAttribute ←
     | _ => throwError "constant must be an inductive type"
 
 def hasUnboxAttr (env : Environment) (n : Name) : Bool :=
-unboxAttr.hasTag env n
+  unboxAttr.hasTag env n
 
 end Lean.IR.UnboxResult

src/Lean/Compiler/ImplementedByAttr.lean

@@ -11,6 +11,37 @@ import Lean.Elab.InfoTree
 
 namespace Lean.Compiler
 
+/--
+Instructs the compiler to use a different function as the implementation of a function. With the
+exception of tactics that call native code such as `native_decide`, the kernel and type checking
+are unaffected. When this attribute is used on a function, the function is not compiled and all
+compiler-related attributes (e.g. `noncomputable`, `@[inline]`) are ignored. Calls to this
+function are replaced by calls to its implementation.
+
+The most common use cases of `@[implemented_by]` are to provide an efficient unsafe implementation
+and to make an unsafe function accessible in safe code through an opaque function:
+
+```
+unsafe def testEqImpl (as bs : Array Nat) : Bool :=
+  ptrEq as bs || as == bs
+
+@[implemented_by testEqImpl]
+def testEq (as bs : Array Nat) : Bool :=
+  as == bs
+
+unsafe def printAddrImpl {α : Type u} (x : α) : IO Unit :=
+  IO.println s!"Address: {ptrAddrUnsafe x}"
+
+@[implemented_by printAddrImpl]
+opaque printAddr {α : Type u} (x : α) : IO Unit
+```
+
+The provided implementation is not checked to be equivalent to the original definition. This makes
+it possible to prove `False` with `native_decide` using incorrect implementations. For a safer
+variant of this attribute that however doesn't work for unsafe implementations, see `@[csimp]`,
+which requires a proof that the two functions are equal.
+-/
+@[builtin_doc]
 builtin_initialize implementedByAttr : ParametricAttribute Name ← registerParametricAttribute {
   name := `implemented_by
   descr := "name of the Lean (probably unsafe) function that implements opaque constant"

src/Lean/Compiler/InitAttr.lean

@@ -96,7 +96,28 @@ private opaque registerInitAttrInner (attrName : Name) (runAfterImport : Bool) (
 def registerInitAttr (attrName : Name) (runAfterImport : Bool) (ref : Name := by exact decl_name%) : IO (ParametricAttribute Name) :=
   registerInitAttrInner attrName runAfterImport ref
 
+/--
+Registers an initialization procedure. Initialization procedures are run in files that import the
+file they are defined in.
+
+This attribute comes in two kinds: Without arguments, the tagged declaration should have type
+`IO Unit` and are simply run during initialization. With a declaration name as a argument, the
+tagged declaration should be an opaque constant and the provided declaration name an action in `IO`
+that returns a value of the type of the tagged declaration. Such initialization procedures store
+the resulting value and make it accessible through the tagged declaration.
+
+The `initialize` command should usually be preferred over using this attribute directly.
+-/
+@[builtin_doc]
 builtin_initialize regularInitAttr : ParametricAttribute Name ← registerInitAttr `init true
+
+/--
+Registers a builtin initialization procedure.
+
+This attribute is used internally to define builtin initialization procedures for bootstrapping and
+should not be used otherwise.
+-/
+@[builtin_doc]
 builtin_initialize builtinInitAttr : ParametricAttribute Name ← registerInitAttr `builtin_init false
 
 def getInitFnNameForCore? (env : Environment) (attr : ParametricAttribute Name) (fn : Name) : Option Name :=

src/Lean/Compiler/InlineAttrs.lean

@@ -14,7 +14,7 @@ inductive InlineAttributeKind where
   deriving Inhabited, BEq, Hashable
 
 /--
-  This is an approximate test for testing whether `declName` can be annotated with the `[macro_inline]` attribute or not.
+This is an approximate test for testing whether `declName` can be annotated with the `[macro_inline]` attribute or not.
 -/
 private def isValidMacroInline (declName : Name) : CoreM Bool := do
   let .defnInfo info ← getConstInfo declName
@@ -32,6 +32,27 @@ private def isValidMacroInline (declName : Name) : CoreM Bool := do
     return false
   return true
 
+/--
+Changes the inlining behavior. This attribute comes in several variants:
+- `@[inline]`: marks the definition to be inlined when it is appropriate.
+- `@[inline_if_reduce]`: marks the definition to be inlined if an application of it after inlining
+  and applying reduction isn't a `match` expression. This attribute can be used for inlining
+  structurally recursive functions.
+- `@[noinline]`: marks the definition to never be inlined.
+- `@[always_inline]`: marks the definition to always be inlined.
+- `@[macro_inline]`: marks the definition to always be inlined at the beginning of compilation.
+  This makes it possible to define functions that evaluate some of their parameters lazily.
+  Example:
+  ```
+  @[macro_inline]
+  def test (x y : Nat) : Nat :=
+    if x = 42 then x else y
+
+  #eval test 42 (2^1000000000000) -- doesn't compute 2^1000000000000
+  ```
+  Only non-recursive functions may be marked `@[macro_inline]`.
+-/
+@[builtin_doc]
 builtin_initialize inlineAttrs : EnumAttributes InlineAttributeKind ←
   registerEnumAttributes
     [(`inline, "mark definition to be inlined", .inline),

src/Lean/Compiler/LCNF/MonoTypes.lean

@@ -46,6 +46,8 @@ def hasTrivialStructure? (declName : Name) : CoreM (Option TrivialStructureInfo)
   let .inductInfo info ← getConstInfo declName | return none
   if info.isUnsafe || info.isRec then return none
   let [ctorName] := info.ctors | return none
+  let ctorType ← getOtherDeclBaseType ctorName []
+  if ctorType.isErased then return none
   let mask ← getRelevantCtorFields ctorName
   let mut result := none
   for h : i in [:mask.size] do
@@ -86,11 +88,7 @@ partial def toMonoType (type : Expr) : CoreM Expr := do
 where
   visitApp (f : Expr) (args : Array Expr) : CoreM Expr := do
     match f with
-    | .const ``lcErased _ =>
-      if args.all (·.isErased) then
-        return erasedExpr
-      else
-        return anyExpr
+    | .const ``lcErased _ => return erasedExpr
     | .const ``lcAny _ => return anyExpr
     | .const ``Decidable _ => return mkConst ``Bool
     | .const declName us =>
@@ -100,6 +98,7 @@ where
       else
         let mut result := mkConst declName
         let mut type ← getOtherDeclBaseType declName us
+        if type.isErased then return erasedExpr
         for arg in args do
           let .forallE _ d b _ := type.headBeta | unreachable!
           let arg := arg.headBeta

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

@@ -311,7 +311,7 @@ def Folder.mulShift [Literal α] [BEq α] (shiftLeft : Name) (pow2 : α → α)
 -- TODO: add option for controlling the limit
 def natPowThreshold := 256
 
-def foldNatPow (args : Array Arg): FolderM (Option LetValue) := do
+def foldNatPow (args : Array Arg) : FolderM (Option LetValue) := do
   let #[.fvar fvarId₁, .fvar fvarId₂] := args | return none
   let some value₁ ← getNatLit fvarId₁ | return none
   let some value₂ ← getNatLit fvarId₂ | return none
@@ -323,12 +323,12 @@ def foldNatPow (args : Array Arg): FolderM (Option LetValue) := do
 /--
 Folder for ofNat operations on fixed-sized integer types.
 -/
-def Folder.ofNat (f : Nat → LitValue) (args : Array Arg): FolderM (Option LetValue) := do
+def Folder.ofNat (f : Nat → LitValue) (args : Array Arg) : FolderM (Option LetValue) := do
   let #[.fvar fvarId] := args | return none
   let some value ← getNatLit fvarId | return none
   return some (.lit (f value))
 
-def Folder.toNat (args : Array Arg): FolderM (Option LetValue) := do
+def Folder.toNat (args : Array Arg) : FolderM (Option LetValue) := do
   let #[.fvar fvarId] := args | return none
   let some (.lit lit) ← findLetValue? fvarId | return none
   match lit with

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

@@ -227,7 +227,14 @@ partial def simp (code : Code) : SimpM Code := withIncRecDepth do
     if let some value ← simpValue? decl.value then
       markSimplified
       decl ← decl.updateValue value
-    if let some decls ← ConstantFold.foldConstants decl then
+    -- This `decl.value != .erased` check is required because `.return` takes
+    -- and `FVarId` rather than `Arg`, and the substitution will end up
+    -- creating a new erased let decl in that case.
+    if decl.type.isErased && decl.value != .erased then
+      modifySubst fun s => s.insert decl.fvarId (.const ``lcErased [])
+      eraseLetDecl decl
+      simp k
+    else if let some decls ← ConstantFold.foldConstants decl then
       markSimplified
       let k ← simp k
       attachCodeDecls decls k
@@ -314,7 +321,6 @@ partial def simp (code : Code) : SimpM Code := withIncRecDepth do
     else
       withNormFVarResult (← normFVar c.discr) fun discr => do
         let resultType ← normExpr c.resultType
-        markUsedFVar discr
         let alts ← c.alts.mapMonoM fun alt => do
           match alt with
           | .alt ctorName ps k =>
@@ -328,8 +334,14 @@ partial def simp (code : Code) : SimpM Code := withIncRecDepth do
                 return alt.updateCode (← simp k)
           | .default k => return alt.updateCode (← simp k)
         let alts ← addDefaultAlt alts
-        if alts.size == 1 && alts[0]! matches .default .. then
-          return alts[0]!.getCode
-        else
-          return code.updateCases! resultType discr alts
+        if let #[alt] := alts then
+          match alt with
+          | .default k => return k
+          | .alt _ params k =>
+            if !(← params.anyM (isUsed ·.fvarId)) then
+              params.forM (eraseParam ·)
+              markSimplified
+              return k
+        markUsedFVar discr
+        return code.updateCases! resultType discr alts
 end

src/Lean/Compiler/LCNF/ToMono.lean

@@ -31,26 +31,38 @@ def checkFVarUse (fvarId : FVarId) : ToMonoM Unit := do
   if let some declName := (← get).noncomputableVars.get? fvarId then
     throwError f!"failed to compile definition, consider marking it as 'noncomputable' because it depends on '{declName}', which is 'noncomputable'"
 
-def argToMono (arg : Arg) : ToMonoM Arg := do
+def checkFVarUseDeferred (resultFVar fvarId : FVarId) : ToMonoM Unit := do
+  if let some declName := (← get).noncomputableVars.get? fvarId then
+    modify fun s => { s with noncomputableVars := s.noncomputableVars.insert resultFVar declName }
+
+@[inline]
+def argToMonoBase (check : FVarId → ToMonoM Unit) (arg : Arg) : ToMonoM Arg := do
   match arg with
   | .erased | .type .. => return .erased
   | .fvar fvarId =>
     if (← get).typeParams.contains fvarId then
       return .erased
     else
-      checkFVarUse fvarId
+      check fvarId
       return arg
 
-def ctorAppToMono (ctorInfo : ConstructorVal) (args : Array Arg) : ToMonoM LetValue := do
-  let argsNew : Array Arg ← args[:ctorInfo.numParams].toArray.mapM fun arg => do
+def argToMono (arg : Arg) : ToMonoM Arg := argToMonoBase checkFVarUse arg
+
+def argToMonoDeferredCheck (resultFVar : FVarId) (arg : Arg) : ToMonoM Arg :=
+  argToMonoBase (checkFVarUseDeferred resultFVar) arg
+
+def ctorAppToMono (resultFVar : FVarId) (ctorInfo : ConstructorVal) (args : Array Arg)
+    : ToMonoM LetValue := do
+  let argsNewParams : Array Arg ← args[:ctorInfo.numParams].toArray.mapM fun arg => do
     -- We only preserve constructor parameters that are types
     match arg with
     | .type type => return .type (← toMonoType type)
     | .fvar .. | .erased => return .erased
-  let argsNew := argsNew ++ (← args[ctorInfo.numParams:].toArray.mapM argToMono)
+  let argsNewFields ← args[ctorInfo.numParams:].toArray.mapM (argToMonoDeferredCheck resultFVar)
+  let argsNew := argsNewParams ++ argsNewFields
   return .const ctorInfo.name [] argsNew
 
-partial def LetValue.toMono (e : LetValue) (fvarId : FVarId) : ToMonoM LetValue := do
+partial def LetValue.toMono (e : LetValue) (resultFVar : FVarId) : ToMonoM LetValue := do
   match e with
   | .erased | .lit .. => return e
   | .const declName _ args =>
@@ -63,28 +75,28 @@ partial def LetValue.toMono (e : LetValue) (fvarId : FVarId) : ToMonoM LetValue
       -- and Bool have the same runtime representation.
       return args[1]!.toLetValue
     else if let some e' ← isTrivialConstructorApp? declName args then
-      e'.toMono fvarId
+      e'.toMono resultFVar
     else if let some (.ctorInfo ctorInfo) := (← getEnv).find? declName then
-      ctorAppToMono ctorInfo args
+      ctorAppToMono resultFVar ctorInfo args
     else
       let env ← getEnv
       if isNoncomputable env declName && !(isExtern env declName) then
-        modify fun s => { s with noncomputableVars := s.noncomputableVars.insert fvarId declName }
-      return .const declName [] (← args.mapM argToMono)
+        modify fun s => { s with noncomputableVars := s.noncomputableVars.insert resultFVar declName }
+      return .const declName [] (← args.mapM (argToMonoDeferredCheck resultFVar))
   | .fvar fvarId args =>
     if (← get).typeParams.contains fvarId then
       return .erased
     else
-      checkFVarUse fvarId
-      return .fvar fvarId (← args.mapM argToMono)
-  | .proj structName fieldIdx fvarId =>
-    if (← get).typeParams.contains fvarId then
+      checkFVarUseDeferred resultFVar fvarId
+      return .fvar fvarId (← args.mapM (argToMonoDeferredCheck resultFVar))
+  | .proj structName fieldIdx baseFVar =>
+    if (← get).typeParams.contains baseFVar then
       return .erased
     else
-      checkFVarUse fvarId
+      checkFVarUseDeferred resultFVar baseFVar
       if let some info ← hasTrivialStructure? structName then
         if info.fieldIdx == fieldIdx then
-          return .fvar fvarId #[]
+          return .fvar baseFVar #[]
         else
           return .erased
       else

src/Lean/Compiler/NeverExtractAttr.lean

@@ -9,6 +9,18 @@ import Lean.Attributes
 
 namespace Lean
 
+/--
+Instructs the compiler that function applications using the tagged declaration should not be
+extracted when they are closed terms, and that common subexpression elimination should not be
+performed.
+
+Ordinarily, the Lean compiler identifies closed terms (without free variables) and extracts them
+to top-level definitions. This optimization can prevent unnecessary recomputation of values.
+
+Preventing the extraction of closed terms is useful for declarations that have implicit effects
+that should be repeated.
+-/
+@[builtin_doc]
 builtin_initialize neverExtractAttr : TagAttribute ←
   registerTagAttribute `never_extract "instruct the compiler that function applications using the tagged declaration should not be extracted when they are closed terms, nor common subexpression should be performed. This is useful for declarations that have implicit effects."
 

src/Lean/Compiler/NoncomputableAttr.lean

@@ -15,7 +15,7 @@ def addNoncomputable (env : Environment) (declName : Name) : Environment :=
   noncomputableExt.tag env declName
 
 /--
-  Return true iff the user has declared the given declaration as `noncomputable`.
+Returns `true` when the given declaration is tagged `noncomputable`.
 -/
 @[export lean_is_noncomputable]
 def isNoncomputable (env : Environment) (declName : Name) : Bool :=

src/Lean/Compiler/Specialize.lean

@@ -13,6 +13,10 @@ inductive SpecializeAttributeKind where
   | specialize | nospecialize
   deriving Inhabited, BEq
 
+/--
+Marks a definition to never be specialized during code generation.
+-/
+@[builtin_doc]
 builtin_initialize nospecializeAttr : TagAttribute ←
   registerTagAttribute `nospecialize "mark definition to never be specialized"
 
@@ -40,6 +44,20 @@ private def elabSpecArgs (declName : Name) (args : Array Syntax) : MetaM (Array
           throwErrorAt arg "invalid specialization argument name `{argName}`, `{declName}` does have an argument with this name"
     return result.qsort (·<·)
 
+/--
+Marks a definition to always be specialized during code generation.
+
+Specialization is an optimization in the code generator for generating variants of a function that
+are specialized to specific parameter values. This is in particular useful for functions that take
+other functions as parameters: Usually when passing functions as parameters, a closure needs to be
+allocated that will then be called. Using `@[specialize]` prevents both of these operations by
+using the provided function directly in the specialization of the inner function.
+
+`@[specialize]` can take additional arguments for the parameter names or indices (starting at 1) of
+the parameters that should be specialized. By default, instance and function parameters are
+specialized.
+-/
+@[builtin_doc]
 builtin_initialize specializeAttr : ParametricAttribute (Array Nat) ←
   registerParametricAttribute {
     name := `specialize

src/Lean/Data/Lsp/Capabilities.lean

@@ -9,6 +9,7 @@ import Lean.Data.JsonRpc
 import Lean.Data.Lsp.TextSync
 import Lean.Data.Lsp.LanguageFeatures
 import Lean.Data.Lsp.CodeActions
+import Lean.Data.Lsp.Extra
 
 /-! Minimal LSP servers/clients do not have to implement a lot
 of functionality. Most useful additional behavior is instead
@@ -82,6 +83,10 @@ def ClientCapabilities.silentDiagnosticSupport (c : ClientCapabilities) : Bool :
     | return false
   return silentDiagnosticSupport
 
+structure LeanServerCapabilities where
+  moduleHierarchyProvider? : Option ModuleHierarchyOptions
+  deriving FromJson, ToJson
+
 -- TODO largely unimplemented
 structure ServerCapabilities where
   textDocumentSync?         : Option TextDocumentSyncOptions := none
@@ -101,6 +106,7 @@ structure ServerCapabilities where
   codeActionProvider?       : Option CodeActionOptions       := none
   inlayHintProvider?        : Option InlayHintOptions        := none
   signatureHelpProvider?    : Option SignatureHelpOptions    := none
+  experimental?             : Option LeanServerCapabilities  := none
   deriving ToJson, FromJson
 
 end Lsp

src/Lean/Data/Lsp/Extra.lean

@@ -121,6 +121,62 @@ structure PlainTermGoal where
   range : Range
   deriving FromJson, ToJson
 
+structure ModuleHierarchyOptions where
+  deriving FromJson, ToJson
+
+structure LeanModule where
+  name  : String
+  uri   : DocumentUri
+  data? : Option Json := none
+  deriving FromJson, ToJson
+
+/--
+`$/lean/prepareModuleHierarchy` client->server request.
+
+Response type: `Option LeanModule`
+-/
+structure LeanPrepareModuleHierarchyParams where
+  textDocument : TextDocumentIdentifier
+  deriving FromJson, ToJson
+
+inductive LeanImportMetaKind where
+  /-- `meta` flag was not set on this import. -/
+  | nonMeta
+  /-- `meta` flag was set on this import. -/
+  | «meta»
+  /-- This import is imported twice; once with `meta`, once without. -/
+  | full
+  deriving Inhabited, FromJson, ToJson
+
+structure LeanImportKind where
+  isPrivate : Bool
+  isAll     : Bool
+  metaKind  : LeanImportMetaKind
+  deriving FromJson, ToJson
+
+structure LeanImport where
+  module : LeanModule
+  kind   : LeanImportKind
+  deriving FromJson, ToJson
+
+/--
+`$/lean/moduleHierarchy/imports` client->server request.
+
+Response type: `Array LeanImport`
+-/
+structure LeanModuleHierarchyImportsParams where
+  module : LeanModule
+  deriving FromJson, ToJson
+
+/--
+`$/lean/moduleHierarchy/importedBy` client->server request.
+
+Response type: `Array LeanImport`
+-/
+structure LeanModuleHierarchyImportedByParams where
+  module : LeanModule
+  deriving FromJson, ToJson
+
 /-- `$/lean/rpc/connect` client->server request.
 
 Starts an RPC session at the given file's worker, replying with the new session ID.

src/Lean/Data/Lsp/Internal.lean

@@ -21,6 +21,32 @@ namespace Lean.Lsp
 /-! Most reference-related types have custom FromJson/ToJson implementations to
 reduce the size of the resulting JSON. -/
 
+/-- Information about a single import statement. -/
+structure ImportInfo where
+  /-- Name of the module that is imported. -/
+  module    : String
+  /-- Whether the module is being imported via `private import`. -/
+  isPrivate : Bool
+  /-- Whether the module is being imported via `import all`. -/
+  isAll     : Bool
+  /-- Whether the module is being imported via `meta import`. -/
+  isMeta    : Bool
+  deriving Inhabited
+
+instance : ToJson ImportInfo where
+  toJson info := Json.arr #[info.module, info.isPrivate, info.isAll, info.isMeta]
+
+instance : FromJson ImportInfo where
+  fromJson?
+    | .arr #[moduleJson, isPrivateJson, isAllJson, isMetaJson] => do
+      return {
+        module    := ← fromJson? moduleJson
+        isPrivate := ← fromJson? isPrivateJson
+        isAll     := ← fromJson? isAllJson
+        isMeta    := ← fromJson? isMetaJson
+      }
+    | _ => .error "Expected array, got other JSON type"
+
 /--
 Identifier of a reference.
 -/
@@ -173,15 +199,26 @@ instance : FromJson ModuleRefs where
     node.foldM (init := ∅) fun m k v =>
       return m.insert (← RefIdent.fromJson? (← Json.parse k)) (← fromJson? v)
 
+/--
+Used in the `$/lean/ileanHeaderInfo` watchdog <- worker notifications.
+Contains the direct imports of the file managed by a worker.
+-/
+structure LeanILeanHeaderInfoParams where
+  /-- Version of the file these imports are from. -/
+  version       : Nat
+  /-- Direct imports of this file. -/
+  directImports : Array ImportInfo
+  deriving FromJson, ToJson
+
 /--
 Used in the `$/lean/ileanInfoUpdate` and `$/lean/ileanInfoFinal` watchdog <- worker notifications.
 Contains the definitions and references of the file managed by a worker.
 -/
 structure LeanIleanInfoParams where
   /-- Version of the file these references are from. -/
-  version    : Nat
+  version        : Nat
   /-- All references for the file. -/
-  references : ModuleRefs
+  references     : ModuleRefs
   deriving FromJson, ToJson
 
 /--

src/Lean/Declaration.lean

@@ -482,7 +482,7 @@ def value! (info : ConstantInfo) (allowOpaque := false) : Expr :=
   | .defnInfo {value, ..}   => value
   | .thmInfo  {value, ..}   => value
   | .opaqueInfo {value, ..} => if allowOpaque then value else panic! "declaration with value expected"
-  | _                       => panic! "declaration with value expected"
+  | _                       => panic! s!"declaration with value expected, but {info.name} has none"
 
 def hints : ConstantInfo → ReducibilityHints
   | .defnInfo {hints, ..} => hints

src/Lean/DefEqAttrib.lean

@@ -0,0 +1,109 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+prelude
+
+import Lean.PrettyPrinter
+
+namespace Lean
+open Meta
+
+/--
+There are defeq theorems that only hold at transparency `.all`, but also others that hold
+(from the kernel's point of view) but where the defeq checker here will run out of cycles.
+
+So we try the more careful first.
+-/
+private def isDefEqCareful (e1 e2 : Expr) : MetaM Bool := do
+  withOptions (smartUnfolding.set · false) <| do
+    withDefault (isDefEq e1 e2) <||> withTransparency .all (isDefEq e1 e2)
+
+def validateDefEqAttr (declName : Name) : AttrM Unit := do
+  let info ← getConstVal declName
+  MetaM.run' do
+    withTransparency .all do -- we want to look through defs in `info.type` all the way to `Eq`
+      forallTelescopeReducing info.type fun _ type => do
+        let type ← whnf type
+        -- NB: The warning wording should work both for explicit uses of `@[defeq]` as well as the implicit `:= rfl`.
+        let some (_, lhs, rhs) := type.eq? |
+          throwError m!"Not a definitional equality: the conclusion should be an equality, but is{inlineExpr type}"
+        let ok ← isDefEqCareful lhs rhs
+        unless ok do
+          let explanation := MessageData.ofLazyM (es := #[lhs, rhs]) do
+            let (lhs, rhs) ← addPPExplicitToExposeDiff lhs rhs
+            let mut msg := m!"Not a definitional equality: the left-hand side{indentExpr lhs}\nis \
+              not definitionally equal to the right-hand side{indentExpr rhs}"
+            if (← getEnv).isExporting then
+              let okPrivately ← withoutExporting <| isDefEqCareful lhs rhs
+              if okPrivately then
+                msg := msg ++ .note m!"This theorem is exported from the current module. \
+                  This requires that all definitions that need to be unfolded to prove this \
+                  theorem must be exposed."
+            pure msg
+          throwError explanation
+
+/--
+Marks the theorem as a definitional equality.
+
+The theorem must be an equality that holds by `rfl`. This allows `dsimp` to use this theorem
+when rewriting.
+
+A theorem with with a definition that is (syntactically) `:= rfl` is implicitly marked `@[defeq]`.
+To avoid this behavior, write `:= (rfl)` instead.
+
+The attribute should be given before a `@[simp]` attribute to have effect.
+
+When using the module system, an exported theorem can only be `@[defeq]` if all definitions that
+need to be unfolded to prove the theorem are exported and exposed.
+-/
+@[builtin_doc]
+builtin_initialize defeqAttr : TagAttribute ←
+  registerTagAttribute `defeq "mark theorem as a definitional equality, to be used by `dsimp`"
+    (validate := validateDefEqAttr) (applicationTime := .afterTypeChecking)
+    (asyncMode := .async)
+
+private partial def isRflProofCore (type : Expr) (proof : Expr) : CoreM Bool := do
+  match type with
+  | .forallE _ _ type _ =>
+    if let .lam _ _ proof _ := proof then
+      isRflProofCore type proof
+    else
+      return false
+  | _ =>
+    if type.isAppOfArity ``Eq 3 then
+      if proof.isAppOfArity ``Eq.refl 2 || proof.isAppOfArity ``rfl 2 then
+        return true
+      else if proof.isAppOfArity ``Eq.symm 4 then
+        -- `Eq.symm` of rfl proof is a rfl proof
+        isRflProofCore type proof.appArg! -- small hack: we don't need to set the exact type
+      else if proof.getAppFn.isConst then
+        -- The application of a `defeq` theorem is a `rfl` proof
+        return defeqAttr.hasTag (← getEnv) proof.getAppFn.constName!
+      else
+        return false
+    else
+      return false
+
+/--
+For automatically generated theorems (equational theorems etc.), we want to set the `defeq` attribute
+if the proof is `rfl`, essentially reproducing the behavior before the introduction of the `defeq`
+attribute. This function infers the `defeq` attribute based on the declaration value.
+-/
+def inferDefEqAttr (declName : Name) : MetaM Unit := do
+  withoutExporting do
+    let info ← getConstInfo declName
+    let isRfl ←
+      if let some value := info.value? then
+        isRflProofCore info.type value
+      else
+        pure false
+    if isRfl then
+      try
+        withExporting (isExporting := !isPrivateName declName) do
+          validateDefEqAttr declName -- sanity-check: would we have accepted `@[defeq]` on this?
+      catch e =>
+        logError m!"Theorem {declName} has a `rfl`-proof and was thus inferred to be `@[defeq]`, \
+          but validating that attribute failed:{indentD e.toMessageData}"
+      defeqAttr.setTag declName

src/Lean/Elab/App.lean

@@ -18,6 +18,11 @@ import Lean.Elab.RecAppSyntax
 namespace Lean.Elab.Term
 open Meta
 
+/--
+Instructs the elaborator to elaborate applications of the given declaration without an expected
+type. This may prevent the elaborator from incorrectly inferring implicit arguments.
+-/
+@[builtin_doc]
 builtin_initialize elabWithoutExpectedTypeAttr : TagAttribute ←
   registerTagAttribute `elab_without_expected_type "mark that applications of the given declaration should be elaborated without the expected type"
 
@@ -800,7 +805,7 @@ def getElabElimExprInfo (elimExpr : Expr) : MetaM ElabElimInfo := do
         throwError "unexpected number of arguments at motive type{indentExpr motiveType}"
       unless motiveResultType.isSort do
         throwError "motive result type must be a sort{indentExpr motiveType}"
-    let some motivePos ← pure (xs.idxOf? motive) |
+    let some motivePos := xs.idxOf? motive |
       throwError "unexpected eliminator type{indentExpr elimType}"
     /-
     Compute transitive closure of fvars appearing in arguments to the motive.
@@ -830,11 +835,67 @@ def getElabElimExprInfo (elimExpr : Expr) : MetaM ElabElimInfo := do
           majorsPos := majorsPos.push i
     trace[Elab.app.elab_as_elim] "motivePos: {motivePos}"
     trace[Elab.app.elab_as_elim] "majorsPos: {majorsPos}"
-    return { elimExpr, elimType,  motivePos, majorsPos }
+    return { elimExpr, elimType, motivePos, majorsPos }
 
 def getElabElimInfo (elimName : Name) : MetaM ElabElimInfo := do
   getElabElimExprInfo (← mkConstWithFreshMVarLevels elimName)
 
+
+/--
+Instructs the elaborator that applications of this function should be elaborated like an eliminator.
+
+An eliminator is a function that returns an application of a "motive" which is a parameter of the
+form `_ → ... → Sort _`, i.e. a function that takes in a certain amount of arguments (referred to
+as major premises) and returns a type in some universe. The `rec` and `casesOn` functions of
+inductive types are automatically treated as eliminators, for other functions this attribute needs
+to be used.
+
+Eliminator elaboration can be compared to the `induction` tactic: The expected type is used as the
+return value of the motive, with occurrences of the major premises replaced with the arguments.
+When more arguments are specified than necessary, the remaining arguments are reverted into the
+expected type.
+
+Examples:
+```lean example
+@[elab_as_elim]
+def evenOddRecOn {motive : Nat → Sort u}
+    (even : ∀ n, motive (n * 2)) (odd : ∀ n, motive (n * 2 + 1))
+    (n : Nat) : motive n := ...
+
+-- simple usage
+example (a : Nat) : (a * a) % 2 = a % 2 :=
+  evenOddRec _ _ a
+  /-
+  1. basic motive is `fun n => (a + 2) % 2 = a % 2`
+  2. major premise `a` substituted: `fun n => (n + 2) % 2 = n % 2`
+  3. now elaborate the other parameters as usual:
+    "even" (first hole): expected type `∀ n, ((n * 2) * (n * 2)) % 2 = (n * 2) % 2`,
+    "odd" (second hole): expected type `∀ n, ((n * 2 + 1) * (n * 2 + 1)) % 2 = (n * 2 + 1) % 2`
+  -/
+
+-- complex substitution
+example (a : Nat) (f : Nat → Nat) : (f a + 1) % 2 ≠ f a :=
+  evenOddRec _ _ (f a)
+  /-
+  Similar to before, except `f a` is substituted: `motive := fun n => (n + 1) % 2 ≠ n`.
+  Now the first hole has expected type `∀ n, (n * 2 + 1) % 2 ≠ n * 2`.
+  Now the second hole has expected type `∀ n, (n * 2 + 1 + 1) % 2 ≠ n * 2 + 1`.
+  -/
+
+-- more parameters
+example (a : Nat) (h : a % 2 = 1) : (a + 1) % 2 = 0 :=
+  evenOddRec _ _ a h
+  /-
+  Before substitution, `a % 2 = 1` is reverted: `motive := fun n => a % 2 = 0 → (a + 1) % 2 = 0`.
+  Substitution: `motive := fun n => n % 2 = 1 → (n + 1) % 2 = 0`
+  Now the first hole has expected type `∀ n, n * 2 % 2 = 1 → (n * 2) % 2 = 0`.
+  Now the second hole has expected type `∀ n, (n * 2 + 1) % 2 = 1 → (n * 2 + 1) % 2 = 0`.
+  -/
+```
+
+See also `@[induction_eliminator]` and `@[cases_eliminator]` for registering default eliminators.
+-/
+@[builtin_doc]
 builtin_initialize elabAsElim : TagAttribute ←
   registerTagAttribute `elab_as_elim
     "instructs elaborator that the arguments of the function application should be elaborated as were an eliminator"

src/Lean/Elab/Command.lean

@@ -416,13 +416,19 @@ instance : MonadQuotation CommandElabM where
   getMainModule       := Command.getMainModule
   withFreshMacroScope := Command.withFreshMacroScope
 
-unsafe def mkCommandElabAttributeUnsafe (ref : Name) : IO (KeyedDeclsAttribute CommandElab) :=
-  mkElabAttribute CommandElab `builtin_command_elab `command_elab `Lean.Parser.Command `Lean.Elab.Command.CommandElab "command" ref
+/--
+Registers a command elaborator for the given syntax node kind.
 
-@[implemented_by mkCommandElabAttributeUnsafe]
-opaque mkCommandElabAttribute (ref : Name) : IO (KeyedDeclsAttribute CommandElab)
+A command elaborator should have type `Lean.Elab.Command.CommandElab` (which is
+`Lean.Syntax → Lean.Elab.Term.CommandElabM Unit`), i.e. should take syntax of the given syntax
+node kind as a parameter and perform an action.
 
-builtin_initialize commandElabAttribute : KeyedDeclsAttribute CommandElab ← mkCommandElabAttribute decl_name%
+The `elab_rules` and `elab` commands should usually be preferred over using this attribute
+directly.
+-/
+@[builtin_doc]
+unsafe builtin_initialize commandElabAttribute : KeyedDeclsAttribute CommandElab ←
+  mkElabAttribute CommandElab `builtin_command_elab `command_elab `Lean.Parser.Command `Lean.Elab.Command.CommandElab "command"
 
 private def mkInfoTree (elaborator : Name) (stx : Syntax) (trees : PersistentArray InfoTree) : CommandElabM InfoTree := do
   let ctx ← read

src/Lean/Elab/ComputedFields.lean

@@ -33,6 +33,28 @@ This file implements the computed fields feature by simulating it via
 namespace Lean.Elab.ComputedFields
 open Meta
 
+/--
+Marks a function as a computed field of an inductive.
+
+Computed fields are specified in the with-block of an inductive type declaration. They can be used
+to allow certain values to be computed only once at the time of construction and then later be
+accessed immediately.
+
+Example:
+```
+inductive NatList where
+  | nil
+  | cons : Nat → NatList → NatList
+with
+  @[computed_field] sum : NatList → Nat
+  | .nil => 0
+  | .cons x l => x + l.sum
+  @[computed_field] length : NatList → Nat
+  | .nil => 0
+  | .cons _ l => l.length + 1 
+```
+-/
+@[builtin_doc]
 builtin_initialize computedFieldAttr : TagAttribute ←
   registerTagAttribute `computed_field "Marks a function as a computed field of an inductive" fun _ => do
     unless (← getOptions).getBool `elaboratingComputedFields do

src/Lean/Elab/DeclModifiers.lean

@@ -28,7 +28,7 @@ def checkNotAlreadyDeclared {m} [Monad m] [MonadEnv m] [MonadError m] [MonadInfo
     match privateToUserName? declName with
     | none          => throwError "'{.ofConstName declName true}' has already been declared"
     | some declName => throwError "private declaration '{.ofConstName declName true}' has already been declared"
-  if isReservedName env declName then
+  if isReservedName env (privateToUserName declName) || isReservedName env (mkPrivateName (← getEnv) declName) then
     throwError "'{declName}' is a reserved name"
   if env.contains (mkPrivateName env declName) then
     addInfo (mkPrivateName env declName)
@@ -84,10 +84,14 @@ def Modifiers.isNonrec : Modifiers → Bool
   | { recKind := .nonrec, .. } => true
   | _                          => false
 
-/-- Adds attribute `attr` in `modifiers` -/
+/-- Adds attribute `attr` in `modifiers`, at the end -/
 def Modifiers.addAttr (modifiers : Modifiers) (attr : Attribute) : Modifiers :=
   { modifiers with attrs := modifiers.attrs.push attr }
 
+/-- Adds attribute `attr` in `modifiers`, at the beginning -/
+def Modifiers.addFirstAttr (modifiers : Modifiers) (attr : Attribute) : Modifiers :=
+  { modifiers with attrs := #[attr] ++ modifiers.attrs }
+
 /-- Filters attributes using `p` -/
 def Modifiers.filterAttrs (modifiers : Modifiers) (p : Attribute → Bool) : Modifiers :=
   { modifiers with attrs := modifiers.attrs.filter p }
@@ -128,7 +132,13 @@ def elabModifiers (stx : TSyntax ``Parser.Command.declModifiers) : m Modifiers :
   let docCommentStx := stx.raw[0]
   let attrsStx      := stx.raw[1]
   let visibilityStx := stx.raw[2]
-  let noncompStx    := stx.raw[3]
+  let isNoncomputable :=
+    if stx.raw[3].isNone then
+      false
+    else if stx.raw[3][0].getKind == ``Parser.Command.meta then
+      false  -- TODO: handle `meta` declarations
+    else
+      true
   let unsafeStx     := stx.raw[4]
   let recKind       :=
     if stx.raw[5].isNone then
@@ -151,7 +161,7 @@ def elabModifiers (stx : TSyntax ``Parser.Command.declModifiers) : m Modifiers :
   return {
     stx, docString?, visibility, recKind, attrs,
     isUnsafe        := !unsafeStx.isNone
-    isNoncomputable := !noncompStx.isNone
+    isNoncomputable
   }
 
 /--

src/Lean/Elab/Declaration.lean

@@ -335,9 +335,11 @@ def elabMutual : CommandElab := fun stx => do
         $[unsafe%$unsafe?]? def initFn : IO $type := with_decl_name% $(mkIdent fullId) do $doSeq
         $defStx:command))
     else
-      let `(Parser.Command.declModifiersT| $[$doc?:docComment]? ) := declModifiers
+      let `(Parser.Command.declModifiersT| $[$doc?:docComment]? $[@[$attrs?,*]]? $(_)? $[unsafe%$unsafe?]?) := declModifiers
         | throwErrorAt declModifiers "invalid initialization command, unexpected modifiers"
-      elabCommand (← `($[$doc?:docComment]? @[$attrId:ident] def initFn : IO Unit := do $doSeq))
+      let attrs := (attrs?.map (·.getElems)).getD #[]
+      let attrs := attrs.push (← `(Lean.Parser.Term.attrInstance| $attrId:ident))
+      elabCommand (← `($[$doc?:docComment]? @[$[$attrs],*] $[unsafe%$unsafe?]? def initFn : IO Unit := do $doSeq))
   | _ => throwUnsupportedSyntax
 
 builtin_initialize

src/Lean/Elab/DefView.lean

@@ -127,6 +127,11 @@ structure DefView where
 def DefView.isInstance (view : DefView) : Bool :=
   view.modifiers.attrs.any fun attr => attr.name == `instance
 
+/-- Prepends the `defeq` attribute, removing existing ones if there are any -/
+def DefView.markDefEq (view : DefView) : DefView :=
+  { view with modifiers :=
+      view.modifiers.filterAttrs (·.name != `defeq) |>.addFirstAttr { name := `defeq } }
+
 namespace Command
 open Meta
 

src/Lean/Elab/Do.lean

@@ -221,7 +221,7 @@ inductive Code where
   /-- Recall that an if-then-else may declare a variable using `optIdent` for the branches `thenBranch` and `elseBranch`. We store the variable name at `var?`. -/
   | ite          (ref : Syntax) (h? : Option Var) (optIdent : Syntax) (cond : Syntax) (thenBranch : Code) (elseBranch : Code)
   | match        (ref : Syntax) (gen : Syntax) (discrs : Syntax) (optMotive : Syntax) (alts : Array (Alt Code))
-  | matchExpr    (ref : Syntax) (meta : Bool) (discr : Syntax) (alts : Array (AltExpr Code)) (elseBranch : Code)
+  | matchExpr    (ref : Syntax) («meta» : Bool) (discr : Syntax) (alts : Array (AltExpr Code)) (elseBranch : Code)
   | jmp          (ref : Syntax) (jpName : Name) (args : Array Syntax)
   deriving Inhabited
 
@@ -268,8 +268,8 @@ partial def CodeBlocl.toMessageData (codeBlock : CodeBlock) : MessageData :=
     | .match _ _ ds _ alts   =>
       m!"match {ds} with"
       ++ alts.foldl (init := m!"") fun acc alt => acc ++ m!"\n| {alt.patterns} => {loop alt.rhs}"
-    | .matchExpr _ meta d alts elseCode =>
-      let r := m!"match_expr {if meta then "" else "(meta := false)"} {d} with"
+    | .matchExpr _ «meta» d alts elseCode =>
+      let r := m!"match_expr {if «meta» then "" else "(meta := false)"} {d} with"
       let r := r ++ alts.foldl (init := m!"") fun acc alt =>
             let acc := acc ++ m!"\n| {if let some var := alt.var? then m!"{var}@" else ""}"
             let acc := acc ++ m!"{alt.funName}"
@@ -341,10 +341,10 @@ partial def convertTerminalActionIntoJmp (code : Code) (jp : Name) (xs : Array V
       return Code.jmp ref jp jmpArgs
     | .match ref g ds t alts =>
       return .match ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← loop alt.rhs) })
-    | .matchExpr ref meta d alts e => do
+    | .matchExpr ref «meta» d alts e => do
       let alts ← alts.mapM fun alt => do pure { alt with rhs := (← loop alt.rhs) }
       let e ← loop e
-      return .matchExpr ref meta d alts e
+      return .matchExpr ref «meta» d alts e
     | c => return c
   loop code
 
@@ -430,10 +430,10 @@ partial def pullExitPointsAux (rs : VarSet) (c : Code) : StateRefT (Array JPDecl
   | .match ref g ds t alts =>
     let alts ← alts.mapM fun alt => do pure { alt with rhs := (← pullExitPointsAux (eraseVars rs alt.vars) alt.rhs) }
     return .match ref g ds t alts
-  | .matchExpr ref meta d alts e =>
+  | .matchExpr ref «meta» d alts e =>
     let alts ← alts.mapM fun alt => do pure { alt with rhs := (← pullExitPointsAux (eraseVars rs alt.vars) alt.rhs) }
     let e ← pullExitPointsAux rs e
-    return .matchExpr ref meta d alts e
+    return .matchExpr ref «meta» d alts e
 
 /--
 Auxiliary operation for adding new variables to the collection of updated variables in a CodeBlock.
@@ -502,14 +502,14 @@ partial def extendUpdatedVarsAux (c : Code) (ws : VarSet) : TermElabM Code :=
         pullExitPoints c
       else
         return .match ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← update alt.rhs) })
-    | .matchExpr ref meta d alts e =>
+    | .matchExpr ref «meta» d alts e =>
       if alts.any fun alt => alt.vars.any fun x => ws.contains x.getId then
         -- If a pattern variable is shadowing a variable in ws, we `pullExitPoints`
         pullExitPoints c
       else
         let alts ← alts.mapM fun alt => do pure { alt with rhs := (← update alt.rhs) }
         let e ← update e
-        return .matchExpr ref meta d alts e
+        return .matchExpr ref «meta» d alts e
     | .ite ref none o c t e => return .ite ref none o c (← update t) (← update e)
     | .ite ref (some h) o cond t e =>
       if ws.contains h.getId then
@@ -623,7 +623,7 @@ def mkMatch (ref : Syntax) (genParam : Syntax) (discrs : Syntax) (optMotive : Sy
     return { ref := alt.ref, vars := alt.vars, patterns := alt.patterns, rhs := rhs.code : Alt Code }
   return { code := .match ref genParam discrs optMotive alts, uvars := ws }
 
-def mkMatchExpr (ref : Syntax) (meta : Bool) (discr : Syntax) (alts : Array (AltExpr CodeBlock)) (elseBranch : CodeBlock) : TermElabM CodeBlock := do
+def mkMatchExpr (ref : Syntax) («meta» : Bool) (discr : Syntax) (alts : Array (AltExpr CodeBlock)) (elseBranch : CodeBlock) : TermElabM CodeBlock := do
   -- nary version of homogenize
   let ws := alts.foldl (union · ·.rhs.uvars) {}
   let ws := union ws elseBranch.uvars
@@ -631,7 +631,7 @@ def mkMatchExpr (ref : Syntax) (meta : Bool) (discr : Syntax) (alts : Array (Alt
     let rhs ← extendUpdatedVars alt.rhs ws
     return { alt with rhs := rhs.code : AltExpr Code }
   let elseBranch ← extendUpdatedVars elseBranch ws
-  return { code := .matchExpr ref meta discr alts elseBranch.code, uvars := ws }
+  return { code := .matchExpr ref «meta» discr alts elseBranch.code, uvars := ws }
 
 /-- Return a code block that executes `terminal` and then `k` with the value produced by `terminal`.
    This method assumes `terminal` is a terminal -/
@@ -1148,7 +1148,7 @@ where
         termAlts := termAlts.push termAlt
       let termMatchAlts := mkNode ``Parser.Term.matchAlts #[mkNullNode termAlts]
       return mkNode ``Parser.Term.«match» #[mkAtomFrom ref "match", genParam, optMotive, discrs, mkAtomFrom ref "with", termMatchAlts]
-    | .matchExpr ref meta d alts elseBranch => withFreshMacroScope do
+    | .matchExpr ref «meta» d alts elseBranch => withFreshMacroScope do
       let d' ← `(discr)
       let mut termAlts := #[]
       for alt in alts do
@@ -1160,7 +1160,7 @@ where
       let elseBranch := mkNode ``Parser.Term.matchExprElseAlt #[mkAtomFrom ref "|", mkHole ref, mkAtomFrom ref "=>", (← toTerm elseBranch)]
       let termMatchExprAlts := mkNode ``Parser.Term.matchExprAlts #[mkNullNode termAlts, elseBranch]
       let body := mkNode ``Parser.Term.matchExpr #[mkAtomFrom ref "match_expr", d', mkAtomFrom ref "with", termMatchExprAlts]
-      if meta then
+      if «meta» then
         `(Bind.bind (instantiateMVarsIfMVarApp $d) fun discr => $body)
       else
         `(let discr := $d; $body)
@@ -1625,7 +1625,7 @@ mutual
   /-- Generate `CodeBlock` for `doMatchExpr; doElems` -/
   partial def doMatchExprToCode (doMatchExpr : Syntax) (doElems: List Syntax) : M CodeBlock := do
     let ref       := doMatchExpr
-    let meta      := doMatchExpr[1].isNone
+    let «meta»    := doMatchExpr[1].isNone
     let discr     := doMatchExpr[2]
     let alts      := doMatchExpr[4][0].getArgs -- Array of `doMatchExprAlt`
     let alts ← alts.mapM fun alt => do
@@ -1637,7 +1637,7 @@ mutual
       let rhs ← doSeqToCode (getDoSeqElems rhs)
       pure { ref, var?, funName, pvars, rhs }
     let elseBranch ← doSeqToCode (getDoSeqElems doMatchExpr[4][1][3])
-    let matchCode ← mkMatchExpr ref meta discr alts elseBranch
+    let matchCode ← mkMatchExpr ref «meta» discr alts elseBranch
     concatWith matchCode doElems
 
   /--

src/Lean/Elab/Frontend.lean

@@ -200,7 +200,12 @@ def runFrontend
   if let some ileanFileName := ileanFileName? then
     let trees := snaps.getAll.flatMap (match ·.infoTree? with | some t => #[t] | _ => #[])
     let references := Lean.Server.findModuleRefs inputCtx.fileMap trees (localVars := false)
-    let ilean := { module := mainModuleName, references := ← references.toLspModuleRefs : Lean.Server.Ilean }
+    let ilean := {
+      module        := mainModuleName
+      directImports := Server.collectImports ⟨snap.stx⟩
+      references    := ← references.toLspModuleRefs
+      : Lean.Server.Ilean
+    }
     IO.FS.writeFile ileanFileName $ Json.compress $ toJson ilean
 
   if let some out := trace.profiler.output.get? opts then

src/Lean/Elab/Import.lean

@@ -18,12 +18,14 @@ def HeaderSyntax.startPos (header : HeaderSyntax) : String.Pos :=
 def HeaderSyntax.isModule (header : HeaderSyntax) : Bool :=
   !header.raw[0].isNone
 
-def HeaderSyntax.imports : HeaderSyntax → Array Import
+def HeaderSyntax.imports (stx : HeaderSyntax) (includeInit : Bool := true) : Array Import :=
+  match stx with
   | `(Parser.Module.header| $[module%$moduleTk]? $[prelude%$preludeTk]? $importsStx*) =>
-    let imports := if preludeTk.isNone then #[{ module := `Init : Import }] else #[]
+    let imports := if preludeTk.isNone && includeInit then #[{ module := `Init : Import }] else #[]
     imports ++ importsStx.map fun
-      | `(Parser.Module.import| $[private%$privateTk]? import $[all%$allTk]? $n) =>
-        { module := n.getId, importAll := allTk.isSome, isExported := privateTk.isNone }
+      | `(Parser.Module.import| $[private%$privateTk]? $[meta%$metaTk]? import $[all%$allTk]? $n) =>
+        { module := n.getId, importAll := allTk.isSome, isExported := privateTk.isNone
+          isMeta := metaTk.isSome }
       | _ => unreachable!
   | _ => unreachable!
 

src/Lean/Elab/InheritDoc.lean

@@ -9,7 +9,13 @@ import Lean.DocString.Extension
 
 namespace Lean
 
-builtin_initialize
+/--
+Uses documentation from a specified declaration.
+
+`@[inherit_doc decl]` is used to inherit the documentation from the declaration `decl`.
+-/
+@[builtin_init, builtin_doc]
+private def init :=
   registerBuiltinAttribute {
     name := `inherit_doc
     descr := "inherit documentation from a specified declaration"

src/Lean/Elab/MutualDef.lean

@@ -24,6 +24,16 @@ open Language
 
 builtin_initialize
   registerTraceClass `Meta.instantiateMVars
+
+-- TODO: this documentation is not shown
+/--
+Makes the bodies of definitions available to importing modules.
+
+This only has an effect if both the module the definition is defined in and the importing module
+have the module system enabled.
+-/
+@[builtin_init, builtin_doc]
+private def init :=
   registerBuiltinAttribute {
     name := `expose
     descr := "(module system) Make bodies of definitions available to importing modules."
@@ -31,6 +41,16 @@ builtin_initialize
       -- Attribute will be filtered out by `MutualDef`
       throwError "Invalid attribute 'expose', must be used when declaring `def`"
   }
+
+/--
+Negates a previous `@[expose]` attribute. This is useful for declaring definitions that shouldn't.
+be exposed in a section tagged `@[expose]`
+
+This only has an effect if both the module the definition is defined in and the importing module
+have the module system enabled.
+-/
+@[builtin_init, builtin_doc]
+private def init2 :=
   registerBuiltinAttribute {
     name := `no_expose
     descr := "(module system) Negate previous `[expose]` attribute."
@@ -1072,34 +1092,20 @@ where
     withExporting (isExporting := !expandedDeclIds.all (isPrivateName ·.declName)) do
     let headers ← elabHeaders views expandedDeclIds bodyPromises tacPromises
     let headers ← levelMVarToParamHeaders views headers
-    -- If the decl looks like a `rfl` theorem, we elaborate is synchronously as we need to wait for
-    -- the type before we can decide whether the theorem body should be exported and then waiting
-    -- for the body as well should not add any significant overhead.
-    let isRflLike := headers.all (·.value matches `(declVal| := rfl))
-    -- elaborate body in parallel when all stars align
     if let (#[view], #[declId]) := (views, expandedDeclIds) then
-      if Elab.async.get (← getOptions) && view.kind.isTheorem && !isRflLike &&
+      if Elab.async.get (← getOptions) && view.kind.isTheorem &&
           !deprecated.oldSectionVars.get (← getOptions) &&
           -- holes in theorem types is not a fatal error, but it does make parallelism impossible
           !headers[0]!.type.hasMVar then
         elabAsync headers[0]! view declId
-      else elabSync headers isRflLike
-    else elabSync headers isRflLike
+      else elabSync headers
+    else elabSync headers
     for view in views, declId in expandedDeclIds do
       -- NOTE: this should be the full `ref`, and thus needs to be done after any snapshotting
       -- that depends only on a part of the ref
       addDeclarationRangesForBuiltin declId.declName view.modifiers.stx view.ref
-  elabSync headers isRflLike := do
-    -- If the reflexivity holds publicly as well (we're still inside `withExporting` here), export
-    -- the body even if it is a theorem so that it is recognized as a rfl theorem even without
-    -- `import all`.
-    let rflPublic ← pure isRflLike <&&> pure (← getEnv).header.isModule <&&>
-      forallTelescopeReducing headers[0]!.type fun _ type => do
-        let some (_, lhs, rhs) := type.eq? | pure false
-        try
-          isDefEq lhs rhs
-        catch _ => pure false
-    finishElab (isExporting := rflPublic) headers
+  elabSync headers := do
+    finishElab headers
     processDeriving headers
   elabAsync header view declId := do
     let env ← getEnv
@@ -1147,7 +1153,7 @@ where
         (cancelTk? := cancelTk) fun _ => do profileitM Exception "elaboration" (← getOptions) do
       setEnv async.asyncEnv
       try
-        finishElab (isExporting := false) #[header]
+        finishElab #[header]
       finally
         reportDiag
         -- must introduce node to fill `infoHole` with multiple info trees
@@ -1279,6 +1285,8 @@ def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do
     if ds.size > 1 && modifiers.isNonrec then
       throwErrorAt d "invalid use of 'nonrec' modifier in 'mutual' block"
     let mut view ← mkDefView modifiers d[1]
+    if view.kind != .example && view.value matches `(declVal| := rfl) then
+      view := view.markDefEq
     let fullHeaderRef := mkNullNode #[d[0], view.headerRef]
     if let some snap := snap? then
       view := { view with headerSnap? := some {

src/Lean/Elab/MutualInductive.lean

@@ -171,8 +171,15 @@ structure InductiveElabDescr where
   deriving Inhabited
 
 /--
-Environment extension to register inductive type elaborator commands.
+Registers an inductive type elaborator for the given syntax node kind.
+
+Commands registered using this attribute are allowed to be used together in mutual blocks with
+other inductive type commands. This attribute is mostly used internally for `inductive` and
+`structure`.
+
+An inductive type elaborator should have type `Lean.Elab.Command.InductiveElabDescr`.
 -/
+@[builtin_doc]
 builtin_initialize inductiveElabAttr : KeyedDeclsAttribute InductiveElabDescr ←
   unsafe KeyedDeclsAttribute.init {
     builtinName := `builtin_inductive_elab,

src/Lean/Elab/ParseImportsFast.lean

@@ -15,6 +15,7 @@ structure State where
   error?        : Option String := none
   isModule      : Bool := false
   -- per-import fields to be consumed by `moduleIdent`
+  isMeta        : Bool := false
   isExported    : Bool := false
   importAll     : Bool := false
   deriving Inhabited
@@ -147,7 +148,7 @@ def State.pushImport (i : Import) (s : State) : State :=
 
 partial def moduleIdent : Parser := fun input s =>
   let finalize (module : Name) : Parser := fun input s =>
-    whitespace input (s.pushImport { module, importAll := s.importAll, isExported := s.isExported })
+    whitespace input (s.pushImport { module, isMeta := s.isMeta, importAll := s.importAll, isExported := s.isExported })
   let rec parse (module : Name) (s : State) :=
     let i := s.pos
     if h : input.atEnd i then
@@ -188,42 +189,39 @@ partial def moduleIdent : Parser := fun input s =>
   let s := p input s
   match s.error? with
   | none => many p input s
-  | some _ => { pos, error? := none, imports := s.imports.shrink size }
+  | some _ => { s with pos, error? := none, imports := s.imports.shrink size }
+
+def setIsMeta (isMeta : Bool) : Parser := fun _ s =>
+  { s with isMeta }
 
 def setIsExported (isExported : Bool) : Parser := fun _ s =>
-  { s with isExported := isExported }
+  { s with isExported }
 
 def setImportAll (importAll : Bool) : Parser := fun _ s =>
   { s with importAll }
 
 def main : Parser :=
-  keywordCore "module" (fun _ s => { s with isModule := true }) (fun _ s => s) >>
+  keywordCore "module" (fun _ s => s) (fun _ s => { s with isModule := true }) >>
   keywordCore "prelude" (fun _ s => s.pushImport `Init) (fun _ s => s) >>
   many (keywordCore "private" (setIsExported true) (setIsExported false) >>
+    keywordCore "meta" (setIsMeta true) (setIsMeta false) >>
     keyword "import" >>
     keywordCore "all" (setImportAll false) (setImportAll true) >>
     moduleIdent)
 
 end ParseImports
 
-deriving instance ToJson for Import
-
-structure ParseImportsResult where
-  imports  : Array Import
-  isModule : Bool
-  deriving ToJson
-
 /--
 Simpler and faster version of `parseImports`. We use it to implement Lake.
 -/
-def parseImports' (input : String) (fileName : String) : IO ParseImportsResult := do
+def parseImports' (input : String) (fileName : String) : IO ModuleHeader := do
   let s := ParseImports.main input (ParseImports.whitespace input {})
   match s.error? with
   | none => return { s with }
   | some err => throw <| IO.userError s!"{fileName}: {err}"
 
 structure PrintImportResult where
-  result?  : Option ParseImportsResult := none
+  result?  : Option ModuleHeader := none
   errors   : Array String := #[]
   deriving ToJson
 

src/Lean/Elab/PreDefinition/EqUnfold.lean

@@ -9,6 +9,7 @@ import Lean.Meta.Tactic.Util
 import Lean.Meta.Tactic.Rfl
 import Lean.Meta.Tactic.Intro
 import Lean.Meta.Tactic.Apply
+import Lean.DefEqAttrib
 
 namespace Lean.Meta
 
@@ -23,8 +24,9 @@ This is not extensible, and always builds on the unfold theorem (`f.eq_def`).
 -/
 def getConstUnfoldEqnFor? (declName : Name) : MetaM (Option Name) := do
   if (← getUnfoldEqnFor? (nonRec := true) declName).isNone then
+    trace[ReservedNameAction] "getConstUnfoldEqnFor? {declName} failed, no unfold theorem available"
     return none
-  let name := .str declName eqUnfoldThmSuffix
+  let name := mkEqLikeNameFor (← getEnv) declName eqUnfoldThmSuffix
   realizeConst declName name do
     -- we have to call `getUnfoldEqnFor?` again to make `unfoldEqnName` available in this context
     let some unfoldEqnName ← getUnfoldEqnFor? (nonRec := true) declName | unreachable!
@@ -52,15 +54,18 @@ def getConstUnfoldEqnFor? (declName : Name) : MetaM (Option Name) := do
       name, type, value
       levelParams := info.levelParams
     }
+    inferDefEqAttr name
   return some name
 
 
 builtin_initialize
   registerReservedNameAction fun name => do
     let .str p s := name | return false
-    unless (← getEnv).isSafeDefinition p do return false
     if s == eqUnfoldThmSuffix then
-      return (← MetaM.run' <| getConstUnfoldEqnFor? p).isSome
+      let env := (← getEnv).setExporting false
+      for p in [p, privateToUserName p] do
+        if env.isSafeDefinition p then
+          return (← MetaM.run' <| getConstUnfoldEqnFor? p).isSome
     return false
 
 end Lean.Meta

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -12,6 +12,7 @@ import Lean.Meta.Tactic.Split
 import Lean.Meta.Tactic.Apply
 import Lean.Meta.Tactic.Refl
 import Lean.Meta.Match.MatchEqs
+import Lean.DefEqAttrib
 
 namespace Lean.Elab.Eqns
 open Meta
@@ -401,6 +402,7 @@ This is currently used for non-recursive functions, well-founded recursion and p
 but not for structural recursion.
 -/
 def mkEqns (declName : Name) (declNames : Array Name) (tryRefl := true): MetaM (Array Name) := do
+  trace[Elab.definition.eqns] "mkEqns: {declName}"
   let info ← getConstInfoDefn declName
   let us := info.levelParams.map mkLevelParam
   withOptions (tactic.hygienic.set · false) do
@@ -414,7 +416,7 @@ def mkEqns (declName : Name) (declNames : Array Name) (tryRefl := true): MetaM (
   for h : i in [: eqnTypes.size] do
     let type := eqnTypes[i]
     trace[Elab.definition.eqns] "eqnType[{i}]: {eqnTypes[i]}"
-    let name := mkEqnThmName declName (i+1)
+    let name := mkEqLikeNameFor (← getEnv) declName s!"{eqnThmSuffixBasePrefix}{i+1}"
     thmNames := thmNames.push name
     -- determinism: `type` should be independent of the environment changes since `baseName` was
     -- added
@@ -428,6 +430,7 @@ where
       name, type, value
       levelParams := info.levelParams
     }
+    inferDefEqAttr name
 
 /--
   Auxiliary method for `mkUnfoldEq`. The structure is based on `mkEqnTypes`.

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

@@ -18,11 +18,10 @@ open Eqns
 /--
 Simple, coarse-grained equation theorem for nonrecursive definitions.
 -/
-private def mkSimpleEqThm (declName : Name) (suffix := Name.mkSimple unfoldThmSuffix) : MetaM (Option Name) := do
+private def mkSimpleEqThm (declName : Name) : MetaM (Option Name) := do
   if let some (.defnInfo info) := (← getEnv).find? declName then
-    let name := declName ++ suffix
-    -- determinism: `name` and `info` are dependent only on `declName`, not any later env
-    -- modifications
+    let name := mkEqLikeNameFor (← getEnv) declName eqn1ThmSuffix
+    trace[Elab.definition.eqns] "mkSimpleEqnThm: {name}"
     realizeConst declName name (doRealize name info)
     return some name
   else
@@ -37,6 +36,7 @@ where
         name, type, value
         levelParams := info.levelParams
       }
+      inferDefEqAttr name
 
 def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
   if (← isRecursiveDefinition declName) then

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

@@ -72,7 +72,7 @@ private def rwFixEq (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
 
 /-- Generate the "unfold" lemma for `declName`. -/
 def mkUnfoldEq (declName : Name) (info : EqnInfo) : MetaM Name := do
-  let name := Name.str declName unfoldThmSuffix
+  let name := mkEqLikeNameFor (← getEnv) declName unfoldThmSuffix
   realizeConst declName name (doRealize name)
   return name
 where
@@ -104,7 +104,7 @@ where
       }
 
 def getUnfoldFor? (declName : Name) : MetaM (Option Name) := do
-  let name := Name.str declName unfoldThmSuffix
+  let name := mkEqLikeNameFor (← getEnv) declName unfoldThmSuffix
   let env ← getEnv
   if env.contains name then return name
   let some info := eqnInfoExt.find? env declName | return none

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

@@ -26,40 +26,51 @@ structure EqnInfo extends EqnInfoCore where
   deriving Inhabited
 
 private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
-  trace[Elab.definition.structural.eqns] "proving: {type}"
-  withNewMCtxDepth do
-    let main ← mkFreshExprSyntheticOpaqueMVar type
-    let (_, mvarId) ← main.mvarId!.intros
-    unless (← tryURefl mvarId) do -- catch easy cases
-      go (← deltaLHS mvarId)
-    instantiateMVars main
+  withTraceNode `Elab.definition.structural.eqns (return m!"{exceptEmoji ·} proving:{indentExpr type}") do
+    withNewMCtxDepth do
+      let main ← mkFreshExprSyntheticOpaqueMVar type
+      let (_, mvarId) ← main.mvarId!.intros
+      unless (← tryURefl mvarId) do -- catch easy cases
+        go (← deltaLHS mvarId)
+      instantiateMVars main
 where
   go (mvarId : MVarId) : MetaM Unit := do
-    trace[Elab.definition.structural.eqns] "step\n{MessageData.ofGoal mvarId}"
-    if (← tryURefl mvarId) then
-      return ()
-    else if (← tryContradiction mvarId) then
-      return ()
-    else if let some mvarId ← whnfReducibleLHS? mvarId then
-      go mvarId
-    else if let some mvarId ← simpMatch? mvarId then
-      go mvarId
-    else if let some mvarId ← simpIf? mvarId then
-      go mvarId
-    else
-      let ctx ← Simp.mkContext
-      match (← simpTargetStar mvarId ctx (simprocs := {})).1 with
-      | TacticResultCNM.closed => return ()
-      | TacticResultCNM.modified mvarId => go mvarId
-      | TacticResultCNM.noChange =>
-        if let some mvarId ← deltaRHS? mvarId declName then
+    withTraceNode `Elab.definition.structural.eqns (return m!"{exceptEmoji ·} step:\n{MessageData.ofGoal mvarId}") do
+      if (← tryURefl mvarId) then
+        trace[Elab.definition.structural.eqns] "tryURefl succeeded"
+        return ()
+      else if (← tryContradiction mvarId) then
+        trace[Elab.definition.structural.eqns] "tryContadiction succeeded"
+        return ()
+      else if let some mvarId ← whnfReducibleLHS? mvarId then
+        trace[Elab.definition.structural.eqns] "whnfReducibleLHS succeeded"
+        go mvarId
+      else if let some mvarId ← simpMatch? mvarId then
+        trace[Elab.definition.structural.eqns] "simpMatch? succeeded"
+        go mvarId
+      else if let some mvarId ← simpIf? mvarId then
+        trace[Elab.definition.structural.eqns] "simpIf? succeeded"
+        go mvarId
+      else
+        let ctx ← Simp.mkContext
+        match (← simpTargetStar mvarId ctx (simprocs := {})).1 with
+        | TacticResultCNM.closed =>
+          trace[Elab.definition.structural.eqns] "simpTargetStar closed the goal"
+        | TacticResultCNM.modified mvarId =>
+          trace[Elab.definition.structural.eqns] "simpTargetStar modified the goal"
           go mvarId
-        else if let some mvarIds ← casesOnStuckLHS? mvarId then
-          mvarIds.forM go
-        else if let some mvarIds ← splitTarget? mvarId then
-          mvarIds.forM go
-        else
-          throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}"
+        | TacticResultCNM.noChange =>
+          if let some mvarId ← deltaRHS? mvarId declName then
+            trace[Elab.definition.structural.eqns] "deltaRHS? succeeded"
+            go mvarId
+          else if let some mvarIds ← casesOnStuckLHS? mvarId then
+            trace[Elab.definition.structural.eqns] "casesOnStuckLHS? succeeded"
+            mvarIds.forM go
+          else if let some mvarIds ← splitTarget? mvarId then
+            trace[Elab.definition.structural.eqns] "splitTarget? succeeded"
+            mvarIds.forM go
+          else
+            throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}"
 
 def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
   withOptions (tactic.hygienic.set · false) do
@@ -68,12 +79,11 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
     let target ← mkEq (mkAppN (Lean.mkConst info.declName us) xs) body
     let goal ← mkFreshExprSyntheticOpaqueMVar target
     mkEqnTypes info.declNames goal.mvarId!
-  let baseName := info.declName
   let mut thmNames := #[]
   for h : i in [: eqnTypes.size] do
     let type := eqnTypes[i]
-    trace[Elab.definition.structural.eqns] "eqnType {i}: {type}"
-    let name := mkEqnThmName baseName (i+1)
+    trace[Elab.definition.structural.eqns] "eqnType {i+1}: {type}"
+    let name := mkEqLikeNameFor (← getEnv) info.declName s!"{eqnThmSuffixBasePrefix}{i+1}"
     thmNames := thmNames.push name
     -- determinism: `type` should be independent of the environment changes since `baseName` was
     -- added
@@ -87,6 +97,7 @@ where
       name, type, value
       levelParams := info.levelParams
     }
+    inferDefEqAttr name
 
 builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension
 
@@ -104,7 +115,7 @@ def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
 
 /-- Generate the "unfold" lemma for `declName`. -/
 def mkUnfoldEq (declName : Name) (info : EqnInfo) : MetaM Name := do
-  let name := Name.str declName unfoldThmSuffix
+  let name := mkEqLikeNameFor (← getEnv) info.declName unfoldThmSuffix
   realizeConst info.declNames[0]! name (doRealize name)
   return name
 where
@@ -120,6 +131,7 @@ where
         name, type, value
         levelParams := info.levelParams
       }
+      inferDefEqAttr name
 
 def getUnfoldFor? (declName : Name) : MetaM (Option Name) := do
   if let some info := eqnInfoExt.find? (← getEnv) declName then

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

@@ -51,4 +51,32 @@ def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
 builtin_initialize
   registerGetEqnsFn getEqnsFor?
 
+
+/--
+This is a hack to fix fallout from #8519, where a non-exposed wfrec definition `foo`
+in a module would cause `foo.eq_def` to be defined eagerly and privately,
+but it should still be visible from non-mudule files.
+
+So we create a unfold equation generator that aliases an existing private `eq_def` to
+wherever the current module expects it.
+-/
+def copyPrivateUnfoldTheorem : GetUnfoldEqnFn := fun declName => do
+  withTraceNode `ReservedNameAction (pure m!"{exceptOptionEmoji ·} copyPrivateUnfoldTheorem running for {declName}") do
+  let name := mkEqLikeNameFor (← getEnv) declName unfoldThmSuffix
+  if let some mod ← findModuleOf? declName then
+    let unfoldName' := mkPrivateNameCore mod (.str declName unfoldThmSuffix)
+    if let some (.thmInfo info) := (← getEnv).find? unfoldName' then
+      realizeConst declName name do
+        addDecl <| Declaration.thmDecl {
+          name,
+          type := info.type,
+          value := .const unfoldName' (info.levelParams.map mkLevelParam),
+          levelParams := info.levelParams
+        }
+      return name
+  return none
+
+builtin_initialize
+  registerGetUnfoldEqnFn copyPrivateUnfoldTheorem
+
 end Lean.Elab.WF

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

@@ -74,6 +74,7 @@ def wfRecursion (preDefs : Array PreDefinition) (termMeasure?s : Array (Option T
   let unaryPreDef ← Mutual.cleanPreDef (cacheProofs := false) unaryPreDef
   let preDefs ← preDefs.mapM (Mutual.cleanPreDef (cacheProofs := false) ·)
   registerEqnsInfo preDefs preDefNonRec.declName fixedParamPerms argsPacker
+  markAsRecursive unaryPreDef.declName
   unless (← isProp unaryPreDef.type) do
     WF.mkUnfoldEq unaryPreDef preDefNonRec.declName wfPreprocessProof
   for preDef in preDefs do

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

@@ -73,8 +73,7 @@ private partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Un
         throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}"
 
 def mkUnfoldEq (preDef : PreDefinition) (unaryPreDefName : Name) (wfPreprocessProof : Simp.Result) : MetaM Unit := do
-  let baseName := preDef.declName
-  let name := Name.str baseName unfoldThmSuffix
+  let name := mkEqLikeNameFor (← getEnv) preDef.declName unfoldThmSuffix
   prependError m!"Cannot derive {name}" do
   withOptions (tactic.hygienic.set · false) do
     lambdaTelescope preDef.value fun xs body => do
@@ -97,6 +96,7 @@ def mkUnfoldEq (preDef : PreDefinition) (unaryPreDefName : Name) (wfPreprocessPr
         name, type, value
         levelParams := preDef.levelParams
       }
+      inferDefEqAttr name
       trace[Elab.definition.wf] "mkUnfoldEq defined {.ofConstName name}"
 
 /--
@@ -106,9 +106,8 @@ theorem of `foo._unary` or `foo._binary`.
 It should just be a specialization of that one, due to defeq.
 -/
 def mkBinaryUnfoldEq (preDef : PreDefinition) (unaryPreDefName : Name) : MetaM Unit := do
-  let baseName := preDef.declName
-  let name := Name.str baseName unfoldThmSuffix
-  let unaryEqName := Name.str unaryPreDefName unfoldThmSuffix
+  let name := mkEqLikeNameFor (← getEnv) preDef.declName unfoldThmSuffix
+  let unaryEqName:= mkEqLikeNameFor (← getEnv) unaryPreDefName unfoldThmSuffix
   prependError m!"Cannot derive {name} from {unaryEqName}" do
   withOptions (tactic.hygienic.set · false) do
     lambdaTelescope preDef.value fun xs body => do
@@ -129,6 +128,7 @@ def mkBinaryUnfoldEq (preDef : PreDefinition) (unaryPreDefName : Name) : MetaM U
         name, type, value
         levelParams := preDef.levelParams
       }
+      inferDefEqAttr name
       trace[Elab.definition.wf] "mkBinaryUnfoldEq defined {.ofConstName name}"
 
 builtin_initialize

src/Lean/Elab/Print.lean

@@ -23,47 +23,60 @@ private def levelParamsToMessageData (levelParams : List Name) : MessageData :=
     return m ++ "}"
 
 private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (safety : DefinitionSafety) (sig : Bool := true) : CommandElabM MessageData := do
-  let m : MessageData :=
-    match (← getReducibilityStatus id) with
-    | ReducibilityStatus.irreducible => "@[irreducible] "
-    | ReducibilityStatus.reducible => "@[reducible] "
-    | ReducibilityStatus.semireducible => ""
-  let m :=
-    m ++
-    match safety with
-    | DefinitionSafety.unsafe  => "unsafe "
-    | DefinitionSafety.partial => "partial "
-    | DefinitionSafety.safe    => ""
-  let m := if isProtected (← getEnv) id then m ++ "protected " else m
-  let (m, id) := match privateToUserName? id with
-    | some id => (m ++ "private ", id)
-    | none    => (m, id)
+  let mut attrs := #[]
+  match (← getReducibilityStatus id) with
+  | ReducibilityStatus.irreducible =>   attrs := attrs.push m!"irreducible"
+  | ReducibilityStatus.reducible =>     attrs := attrs.push m!"reducible"
+  | ReducibilityStatus.semireducible => pure ()
+
+  if defeqAttr.hasTag (← getEnv) id then
+    attrs := attrs.push m!"defeq"
+
+  let mut m : MessageData := m!""
+  unless attrs.isEmpty do
+    m := m ++ "@[" ++ MessageData.joinSep attrs.toList ", " ++ "] "
+
+  match safety with
+  | DefinitionSafety.unsafe  => m := m ++ "unsafe "
+  | DefinitionSafety.partial => m := m ++ "partial "
+  | DefinitionSafety.safe    => pure ()
+
+  if isProtected (← getEnv) id then
+    m := m ++ "protected "
+
+  let id' ← match privateToUserName? id with
+    | some id' =>
+      m := m ++ "private "
+      pure id'
+    | none =>
+      pure id
+
   if sig then
-    return m!"{m}{kind} {id}{levelParamsToMessageData levelParams} : {type}"
+    return m!"{m}{kind} {id'}{levelParamsToMessageData levelParams} : {type}"
   else
     return m!"{m}{kind}"
 
-private def mkHeader' (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (isUnsafe : Bool) (sig : Bool := true) : CommandElabM MessageData :=
-  mkHeader kind id levelParams type (if isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe) (sig := sig)
-
 private def mkOmittedMsg : Option Expr → MessageData
   | none   => "<not imported>"
   | some e => e
 
-private def printDefLike (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (value? : Option Expr) (safety := DefinitionSafety.safe) : CommandElabM Unit := do
-  let m ← mkHeader kind id levelParams type safety
-  let m := m ++ " :=" ++ Format.line ++ mkOmittedMsg value?
-  logInfo m
+private def printAxiomLike (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (safety : DefinitionSafety) : CommandElabM Unit := do
+  logInfo (← mkHeader kind id levelParams type safety)
 
-private def printAxiomLike (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (isUnsafe := false) : CommandElabM Unit := do
-  logInfo (← mkHeader' kind id levelParams type isUnsafe)
+private def printDefLike (sigOnly : Bool) (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (value? : Option Expr) (safety := DefinitionSafety.safe) : CommandElabM Unit := do
+  if sigOnly then
+    printAxiomLike kind id levelParams type safety
+  else
+    let m ← mkHeader kind id levelParams type safety
+    let m := m ++ " :=" ++ Format.line ++ mkOmittedMsg value?
+    logInfo m
 
 private def printQuot (id : Name) (levelParams : List Name) (type : Expr) : CommandElabM Unit := do
-  printAxiomLike "Quotient primitive" id levelParams type
+  printAxiomLike "Quotient primitive" id levelParams type (safety := DefinitionSafety.safe)
 
 private def printInduct (id : Name) (levelParams : List Name) (numParams : Nat) (type : Expr)
     (ctors : List Name) (isUnsafe : Bool) : CommandElabM Unit := do
-  let mut m ← mkHeader' "inductive" id levelParams type isUnsafe
+  let mut m ← mkHeader "inductive" id levelParams type (if isUnsafe then .unsafe else .safe)
   m := m ++ Format.line ++ "number of parameters: " ++ toString numParams
   m := m ++ Format.line ++ "constructors:"
   for ctor in ctors do
@@ -89,7 +102,7 @@ private partial def printStructure (id : Name) (levelParams : List Name) (numPar
     (isUnsafe : Bool) : CommandElabM Unit := do
   let env ← getEnv
   let kind := if isClass env id then "class" else "structure"
-  let header ← mkHeader' kind id levelParams type isUnsafe (sig := false)
+  let header ← mkHeader kind id levelParams type (if isUnsafe then .unsafe else .safe) (sig := false)
   let levels := levelParams.map Level.param
   liftTermElabM <| forallTelescope (← getConstInfo id).type fun params _ =>
     let s := Expr.const id levels
@@ -158,20 +171,20 @@ private partial def printStructure (id : Name) (levelParams : List Name) (numPar
       withOptions (fun opts => opts.set pp.proofs.name false) do
         logInfo m
 
-private def printIdCore (id : Name) : CommandElabM Unit := do
+private def printIdCore (sigOnly : Bool) (id : Name) : CommandElabM Unit := do
   let env ← getEnv
   match env.find? id with
   | ConstantInfo.axiomInfo { levelParams := us, type := t, isUnsafe := u, .. } =>
     match getOriginalConstKind? env id with
-    | some .defn => printDefLike "def" id us t none (if u then .unsafe else .safe)
-    | some .thm => printDefLike "theorem" id us t none (if u then .unsafe else .safe)
-    | _  => printAxiomLike "axiom" id us t u
-  | ConstantInfo.defnInfo  { levelParams := us, type := t, value := v, safety := s, .. } => printDefLike "def" id us t v s
-  | ConstantInfo.thmInfo  { levelParams := us, type := t, value := v, .. } => printDefLike "theorem" id us t v
-  | ConstantInfo.opaqueInfo  { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "opaque" id us t u
+    | some .defn => printDefLike sigOnly "def" id us t none (if u then .unsafe else .safe)
+    | some .thm => printDefLike sigOnly "theorem" id us t none (if u then .unsafe else .safe)
+    | _  => printAxiomLike "axiom" id us t (if u then .unsafe else .safe)
+  | ConstantInfo.defnInfo  { levelParams := us, type := t, value := v, safety := s, .. } => printDefLike sigOnly "def" id us t v s
+  | ConstantInfo.thmInfo  { levelParams := us, type := t, value := v, .. } => printDefLike sigOnly "theorem" id us t v
+  | ConstantInfo.opaqueInfo  { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "opaque" id us t (if u then .unsafe else .safe)
   | ConstantInfo.quotInfo  { levelParams := us, type := t, .. } => printQuot id us t
-  | ConstantInfo.ctorInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constructor" id us t u
-  | ConstantInfo.recInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "recursor" id us t u
+  | ConstantInfo.ctorInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constructor" id us t (if u then .unsafe else .safe)
+  | ConstantInfo.recInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "recursor" id us t (if u then .unsafe else .safe)
   | ConstantInfo.inductInfo { levelParams := us, numParams, type := t, ctors, isUnsafe := u, .. } =>
     if isStructure env id then
       printStructure id us numParams t ctors[0]! u
@@ -182,13 +195,23 @@ private def printIdCore (id : Name) : CommandElabM Unit := do
 private def printId (id : Syntax) : CommandElabM Unit := do
   addCompletionInfo <| CompletionInfo.id id id.getId (danglingDot := false) {} none
   let cs ← liftCoreM <| realizeGlobalConstWithInfos id
-  cs.forM printIdCore
+  cs.forM (printIdCore (sigOnly := false) ·)
 
 @[builtin_command_elab «print»] def elabPrint : CommandElab
   | `(#print%$tk $id:ident) => withRef tk <| printId id
   | `(#print%$tk $s:str)    => logInfoAt tk s.getString
   | _                       => throwError "invalid #print command"
 
+private def printIdSig (id : Syntax) : CommandElabM Unit := do
+  addCompletionInfo <| CompletionInfo.id id id.getId (danglingDot := false) {} none
+  let cs ← liftCoreM <| realizeGlobalConstWithInfos id
+  cs.forM (printIdCore (sigOnly := true) ·)
+
+@[builtin_command_elab «printSig»] def elabPrintSig : CommandElab := fun stx =>
+  withRef stx[0] do
+    let id := stx[2]
+    printIdSig id
+
 private def printAxiomsOf (constName : Name) : CommandElabM Unit := do
   let axioms ← collectAxioms constName
   if axioms.isEmpty then

src/Lean/Elab/Quotation/Precheck.lean

@@ -36,19 +36,23 @@ register_builtin_option quotPrecheck.allowSectionVars : Bool := {
   descr    := "Allow occurrences of section variables in checked quotations, it is useful when declaring local notation."
 }
 
-unsafe def mkPrecheckAttribute : IO (KeyedDeclsAttribute Precheck) :=
+/--
+Registers a double backtick syntax quotation pre-check.
+
+`@[quot_precheck k]` registers a declaration of type `Lean.Elab.Term.Quotation.Precheck` for the
+syntax node kind `k`. It should implement eager name analysis on the passed syntax by throwing an
+exception on unbound identifiers, and calling `precheck` recursively on nested terms, potentially
+with an extended local context (`withNewLocal`). Macros without registered precheck hook are
+unfolded, and identifier-less syntax is ultimately assumed to be well-formed.
+-/
+@[builtin_doc]
+unsafe builtin_initialize precheckAttribute : KeyedDeclsAttribute Precheck ←
   KeyedDeclsAttribute.init {
     builtinName := `builtin_quot_precheck,
     name := `quot_precheck,
-    descr    := "Register a double backtick syntax quotation pre-check.
-
-[quot_precheck k] registers a declaration of type `Lean.Elab.Term.Quotation.Precheck` for the `SyntaxNodeKind` `k`.
-It should implement eager name analysis on the passed syntax by throwing an exception on unbound identifiers,
-and calling `precheck` recursively on nested terms, potentially with an extended local context (`withNewLocal`).
-Macros without registered precheck hook are unfolded, and identifier-less syntax is ultimately assumed to be well-formed.",
+    descr    := "Register a double backtick syntax quotation pre-check.",
     valueTypeName := ``Precheck
-  } `Lean.Elab.Term.Quotation.precheckAttribute
-@[builtin_init mkPrecheckAttribute] opaque precheckAttribute : KeyedDeclsAttribute Precheck
+  }
 
 partial def precheck : Precheck := fun stx => do
   if let p::_ := precheckAttribute.getValues (← getEnv) stx.getKind then

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

@@ -355,6 +355,9 @@ builtin_initialize
 builtin_initialize
   registerReservedNameAction fun name => do
     let .str p s := name | return false
+    unless s == enumToBitVecSuffix ||
+           s == eqIffEnumToBitVecEqSuffix ||
+           s == enumToBitVecLeSuffix do return false
     if ← isEnumType p then
       if s == enumToBitVecSuffix then
         discard <| MetaM.run' (getEnumToBitVecFor p)

src/Lean/Elab/Tactic/Basic.lean

@@ -127,10 +127,19 @@ def withRestoreOrSaveFull (reusableResult? : Option (α × SavedState))
 protected def getCurrMacroScope : TacticM MacroScope := do pure (← readThe Core.Context).currMacroScope
 protected def getMainModule     : TacticM Name       := do pure (← getEnv).mainModule
 
-unsafe def mkTacticAttribute : IO (KeyedDeclsAttribute Tactic) :=
-  mkElabAttribute Tactic `builtin_tactic `tactic `Lean.Parser.Tactic `Lean.Elab.Tactic.Tactic "tactic" `Lean.Elab.Tactic.tacticElabAttribute
+/--
+Registers a tactic elaborator for the given syntax node kind.
 
-@[builtin_init mkTacticAttribute] opaque tacticElabAttribute : KeyedDeclsAttribute Tactic
+A tactic elaborator should have type `Lean.Elab.Tactic.Tactic` (which is
+`Lean.Syntax → Lean.Elab.Tactic.TacticM Unit`), i.e. should take syntax of the given syntax
+node kind as a parameter and alter the tactic state.
+
+The `elab_rules` and `elab` commands should usually be preferred over using this attribute
+directly.
+-/
+@[builtin_doc]
+unsafe builtin_initialize tacticElabAttribute : KeyedDeclsAttribute Tactic ←
+  mkElabAttribute Tactic `builtin_tactic `tactic `Lean.Parser.Tactic `Lean.Elab.Tactic.Tactic "tactic"
 
 def mkTacticInfo (mctxBefore : MetavarContext) (goalsBefore : List MVarId) (stx : Syntax) : TacticM Info :=
   return Info.ofTacticInfo {

src/Lean/Elab/Tactic/Grind.lean

@@ -144,6 +144,7 @@ def grind
     let result ← Grind.main mvar'.mvarId! params fallback
     if result.hasFailed then
       throwError "`grind` failed\n{← result.toMessageData}"
+    trace[grind.debug.proof] "{← instantiateMVars mvar'}"
     -- `grind` proofs are often big
     let e ← if (← isProp type) then
       mkAuxTheorem type (← instantiateMVarsProfiling mvar') (zetaDelta := true)
@@ -181,7 +182,7 @@ def evalGrindCore
   let only := only.isSome
   let params := if let some params := params then params.getElems else #[]
   if Grind.grind.warning.get (← getOptions) then
-    logWarningAt ref "The `grind` tactic is experimental and still under development. Avoid using it in production projects."
+    logWarningAt ref "The `grind` tactic is new and its behaviour may change in the future. This project has used `set_option grind.warning true` to discourage its use."
   withMainContext do
     let result ← grind (← getMainGoal) config only params fallback
     replaceMainGoal []

src/Lean/Elab/Tactic/Induction.lean

@@ -243,10 +243,10 @@ def setMotiveArg (mvarId : MVarId) (motiveArg : MVarId) (targets : Array FVarId)
       if (← isTypeCorrect absType') then
         absType := absType'
       else
-        trace[Elab.induction] "Not abstracing goal over {complexArg}, resulting term is not type correct:{indentExpr absType'} }"
+        trace[Elab.induction] "Not abstracting goal over {complexArg}, resulting term is not type correct:{indentExpr absType'} }"
         absType := .lam (← mkFreshUserName `x) complexArgType absType .default
     else
-      trace[Elab.induction] "Not abstracing goal over {complexArg}, its type {complexArgType} does not match the expected {exptComplexArgType}"
+      trace[Elab.induction] "Not abstracting goal over {complexArg}, its type {complexArgType} does not match the expected {exptComplexArgType}"
       absType := .lam (← mkFreshUserName `x) exptComplexArgType absType .default
 
   let motive ← mkLambdaFVars (targets.map mkFVar) absType

src/Lean/Elab/Tactic/Monotonicity.lean

@@ -29,7 +29,15 @@ builtin_initialize monotoneExt :
     initial := {}
   }
 
-builtin_initialize registerBuiltinAttribute {
+/--
+Registers a monotonicity theorem for `partial_fixpoint`.
+
+Monotonicity theorems should have `Lean.Order.monotone ...` as a conclusion. They are used in the
+`monotonicity` tactic (scoped in the `Lean.Order` namespace) to automatically prove monotonicity
+for functions defined using `partial_fixpoint`.
+-/
+@[builtin_init, builtin_doc]
+private def init := registerBuiltinAttribute {
   name := `partial_fixpoint_monotone
   descr := "monotonicity theorem"
   add := fun decl _ kind => MetaM.run' do

src/Lean/Elab/Term.lean

@@ -177,7 +177,7 @@ structure State where
   Backtrackable state for the `TermElabM` monad.
 -/
 structure SavedState where
-  meta   : Meta.SavedState
+  «meta» : Meta.SavedState
   «elab» : State
   deriving Nonempty
 
@@ -200,7 +200,7 @@ structure State where
 -/
 structure Snapshot where
   core   : Core.State
-  meta   : Meta.State
+  «meta» : Meta.State
   term   : Term.State
   tactic : Tactic.State
   stx    : Syntax
@@ -352,7 +352,7 @@ instance : Inhabited (TermElabM α) where
   default := throw default
 
 protected def saveState : TermElabM SavedState :=
-  return { meta := (← Meta.saveState), «elab» := (← get) }
+  return { «meta» := (← Meta.saveState), «elab» := (← get) }
 
 def SavedState.restore (s : SavedState) (restoreInfo : Bool := false) : TermElabM Unit := do
   let traceState ← getTraceState -- We never backtrack trace message
@@ -387,10 +387,10 @@ def withRestoreOrSaveFull (reusableResult? : Option (α × SavedState))
       snap.new.resolve old.val.get
 
   let reusableResult? := reusableResult?.map (fun (val, state) => (val, state.meta))
-  let (a, meta) ← withReader ({ · with tacSnap? }) do
+  let (a, «meta») ← withReader ({ · with tacSnap? }) do
     controlAt MetaM fun runInBase => do
       Meta.withRestoreOrSaveFull reusableResult? <| runInBase act
-  return (a, { meta, «elab» := (← get) })
+  return (a, { «meta», «elab» := (← get) })
 
 instance : MonadBacktrack SavedState TermElabM where
   saveState      := Term.saveState
@@ -577,6 +577,17 @@ unsafe def mkTermElabAttributeUnsafe (ref : Name) : IO (KeyedDeclsAttribute Term
 @[implemented_by mkTermElabAttributeUnsafe]
 opaque mkTermElabAttribute (ref : Name) : IO (KeyedDeclsAttribute TermElab)
 
+/--
+Registers a term elaborator for the given syntax node kind.
+
+A term elaborator should have type `Lean.Elab.Term.TermElab` (which is
+`Lean.Syntax → Option Lean.Expr → Lean.Elab.Term.TermElabM Lean.Expr`), i.e. should take syntax of
+the given syntax node kind and an optional expected type as parameters and produce an expression.
+
+The `elab_rules` and `elab` commands should usually be preferred over using this attribute
+directly.
+-/
+@[builtin_doc]
 builtin_initialize termElabAttribute : KeyedDeclsAttribute TermElab ← mkTermElabAttribute decl_name%
 
 /--
@@ -956,7 +967,7 @@ private def applyAttributesCore
         let runAttr := do
           -- not truly an elaborator, but a sensible target for go-to-definition
           let elaborator := attrImpl.ref
-          if (← getInfoState).enabled && (← getEnv).contains elaborator then
+          if (← getInfoState).enabled then
             withInfoContext (mkInfo := return .ofCommandInfo { elaborator, stx := attr.stx }) do
               try runAttr
               finally if attr.stx[0].isIdent || attr.stx[0].isAtom then
@@ -2072,6 +2083,13 @@ builtin_initialize
   registerTraceClass `Elab.debug
   registerTraceClass `Elab.reuse
 
+/--
+Marks an elaborator (tactic or command, currently) as supporting incremental elaboration.
+
+For unmarked elaborators, the corresponding snapshot bundle field in the elaboration context is
+unset so as to prevent accidental, incorrect reuse.
+-/
+@[builtin_doc]
 builtin_initialize incrementalAttr : TagAttribute ←
   registerTagAttribute `incremental "Marks an elaborator (tactic or command, currently) as \
 supporting incremental elaboration. For unmarked elaborators, the corresponding snapshot bundle \
@@ -2082,7 +2100,8 @@ builtin_initialize builtinIncrementalElabs : IO.Ref NameSet ← IO.mkRef {}
 def addBuiltinIncrementalElab (decl : Name) : IO Unit := do
   builtinIncrementalElabs.modify fun s => s.insert decl
 
-builtin_initialize
+@[builtin_init, inherit_doc incrementalAttr, builtin_doc]
+private def init :=
   registerBuiltinAttribute {
     name            := `builtin_incremental
     descr           := s!"(builtin) {incrementalAttr.attr.descr}"

src/Lean/Elab/Util.lean

@@ -123,6 +123,17 @@ unsafe def mkMacroAttributeUnsafe (ref : Name) : IO (KeyedDeclsAttribute Macro)
 @[implemented_by mkMacroAttributeUnsafe]
 opaque mkMacroAttribute (ref : Name) : IO (KeyedDeclsAttribute Macro)
 
+/--
+Registers a macro expander for a given syntax node kind.
+
+A macro expander should have type `Lean.Macro` (which is `Lean.Syntax → Lean.MacroM Lean.Syntax`),
+i.e. should take syntax of the given syntax node kind as a parameter and produce different syntax
+in the same syntax category.
+
+The `macro_rules` and `macro` commands should usually be preferred over using this attribute
+directly.
+-/
+@[builtin_doc]
 builtin_initialize macroAttribute : KeyedDeclsAttribute Macro ← mkMacroAttribute decl_name%
 
 /--

src/Lean/EnvExtension.lean

@@ -150,8 +150,10 @@ namespace MapDeclarationExtension
 def insert (ext : MapDeclarationExtension α) (env : Environment) (declName : Name) (val : α) : Environment :=
   have : Inhabited Environment := ⟨env⟩
   assert! env.getModuleIdxFor? declName |>.isNone -- See comment at `MapDeclarationExtension`
-  assert! env.asyncMayContain declName
-  ext.addEntry env (declName, val)
+  if !env.asyncMayContain declName then
+    panic! s!"MapDeclarationExtension.insert: cannot insert {declName} into {ext.name}, it is not contained in {env.asyncPrefix?}"
+  else
+    ext.addEntry env (declName, val)
 
 def find? [Inhabited α] (ext : MapDeclarationExtension α) (env : Environment) (declName : Name)
     (includeServer := false) : Option α :=

src/Lean/Environment.lean

@@ -1859,7 +1859,7 @@ partial def importModulesCore
     ImportStateM Unit := go imports (importAll := true) (isExported := isModule)
 /-
 When the module system is disabled for the root, we import all transitively referenced modules and
-ignore any module sytem annotations on the way.
+ignore any module system annotations on the way.
 
 When the module system is enabled for the root, each module may need to be imported at one of the
 following levels:

src/Lean/Linter/Basic.lean

@@ -37,7 +37,7 @@ This structure contains all the data required to do so, the `Options` set on the
 or by the `set_option` command, and the `LinterSets` that have been declared.
 
 A single structure holding this data is useful since we want `getLinterValue` to be a pure
-function: determinining the `LinterSets` would otherwise require a `MonadEnv` instance.
+function: determining the `LinterSets` would otherwise require a `MonadEnv` instance.
 -/
 structure LinterOptions where
   toOptions : Options

src/Lean/Meta/Basic.lean

@@ -427,7 +427,7 @@ structure State where
 -/
 structure SavedState where
   core        : Core.SavedState
-  meta        : State
+  «meta»      : State
   deriving Nonempty
 
 register_builtin_option maxSynthPendingDepth : Nat := {
@@ -555,7 +555,7 @@ instance : AddMessageContext MetaM where
   addMessageContext := addMessageContextFull
 
 protected def saveState : MetaM SavedState :=
-  return { core := (← Core.saveState), meta := (← get) }
+  return { core := (← Core.saveState), «meta» := (← get) }
 
 /-- Restore backtrackable parts of the state. -/
 def SavedState.restore (b : SavedState) : MetaM Unit := do
@@ -570,7 +570,7 @@ def withRestoreOrSaveFull (reusableResult? : Option (α × SavedState)) (act : M
   let reusableResult? := reusableResult?.map (fun (val, state) => (val, state.core))
   let (a, core) ← controlAt CoreM fun runInBase => do
     Core.withRestoreOrSaveFull reusableResult? <| runInBase act
-  return (a, { core, meta := (← get) })
+  return (a, { core, «meta» := (← get) })
 
 instance : MonadBacktrack SavedState MetaM where
   saveState      := Meta.saveState

src/Lean/Meta/Coe.lean

@@ -10,12 +10,20 @@ import Lean.Meta.AppBuilder
 
 namespace Lean.Meta
 
+/--
+Tags declarations to be unfolded during coercion elaboration.
+
+This is mostly used to hide coercion implementation details and show the coerced result instead of
+an application of auxiliary definitions (e.g. `CoeT.coe`, `Coe.coe`). This attribute only works on
+reducible functions and instance projections.
+-/
+@[builtin_doc]
 builtin_initialize coeDeclAttr : TagAttribute ←
   registerTagAttribute `coe_decl "auxiliary definition used to implement coercion (unfolded during elaboration)"
 
 /--
-  Return true iff `declName` is one of the auxiliary definitions/projections
-  used to implement coercions.
+Return true iff `declName` is one of the auxiliary definitions/projections used to implement
+coercions.
 -/
 def isCoeDecl (env : Environment) (declName : Name) : Bool :=
   coeDeclAttr.hasTag env declName

src/Lean/Meta/Constructions/NoConfusionLinear.lean

@@ -10,7 +10,7 @@ import Lean.Meta.CompletionName
 
 /-!
 This module produces a construction for the `noConfusionType` that is linear in size in the number of
-constructors of the inductive type. This is in contrast to the previous construction (definde in
+constructors of the inductive type. This is in contrast to the previous construction (defined in
 `no_confusion.cpp`), that is quadratic in size due to nested `.brecOn` applications.
 
 We still use the old construction when processing the prelude, for the few inductives that we need

src/Lean/Meta/Eqns.lean

@@ -9,6 +9,7 @@ import Lean.AddDecl
 import Lean.Meta.Basic
 import Lean.Meta.AppBuilder
 import Lean.Meta.Match.MatcherInfo
+import Lean.DefEqAttrib
 
 namespace Lean.Meta
 
@@ -62,9 +63,6 @@ def eqnThmSuffixBasePrefix := eqnThmSuffixBase ++ "_"
 def eqn1ThmSuffix := eqnThmSuffixBasePrefix ++ "1"
 example : eqn1ThmSuffix = "eq_1" := rfl
 
-def mkEqnThmName (declName : Name) (idx : Nat) : Name :=
-  Name.str declName eqnThmSuffixBase |>.appendIndexAfter idx
-
 /-- Returns `true` if `s` is of the form `eq_<idx>` -/
 def isEqnReservedNameSuffix (s : String) : Bool :=
   eqnThmSuffixBasePrefix.isPrefixOf s && (s.drop 3).isNat
@@ -72,6 +70,28 @@ def isEqnReservedNameSuffix (s : String) : Bool :=
 def unfoldThmSuffix := "eq_def"
 def eqUnfoldThmSuffix := "eq_unfold"
 
+def isEqnLikeSuffix (s : String) : Bool :=
+  s == unfoldThmSuffix || s == eqUnfoldThmSuffix || isEqnReservedNameSuffix s
+
+/--
+The equational theorem for a definition can be private even if the definition itself is not.
+So un-private the name here when looking for a declaration
+-/
+def declFromEqLikeName (env : Environment) (name : Name) : Option (Name × String) := Id.run do
+  if let .str p s := name then
+    if isEqnLikeSuffix s then
+      for p in [p, privateToUserName p] do
+        -- Remark: `f.match_<idx>.eq_<idx>` are handled separately in `Lean.Meta.Match.MatchEqs`.
+        if (env.setExporting false).isSafeDefinition p && !isMatcherCore env p then
+          return some (p, s)
+  return none
+
+def mkEqLikeNameFor (env : Environment) (declName : Name) (suffix : String) : Name :=
+  let isExposed := !env.header.isModule || ((env.setExporting true).find? declName).elim false (·.hasValue)
+  let name := .str declName suffix
+  let name := if isExposed then name else mkPrivateName env name
+  name
+
 /--
 Throw an error if names for equation theorems for `declName` are not available.
 -/
@@ -85,16 +105,14 @@ def ensureEqnReservedNamesAvailable (declName : Name) : CoreM Unit := do
 /--
 Ensures that `f.eq_def`, `f.unfold` and `f.eq_<idx>` are reserved names if `f` is a safe definition.
 -/
-builtin_initialize registerReservedNamePredicate fun env n =>
-  match n with
-  | .str p s =>
-    (isEqnReservedNameSuffix s || s == unfoldThmSuffix || s == eqUnfoldThmSuffix)
-    -- Make equation theorems accessible even when body should not be visible for compatibility.
-    -- TODO: Make them private instead.
-    && (env.setExporting false).isSafeDefinition p
-    -- Remark: `f.match_<idx>.eq_<idx>` are handled separately in `Lean.Meta.Match.MatchEqs`.
-    && !isMatcherCore env p
-  | _ => false
+builtin_initialize registerReservedNamePredicate fun env n => Id.run do
+  if let some (declName, suffix) := declFromEqLikeName env n then
+    -- The reserved name predicate has to be precise, as `resolveExact`
+    -- will believe it. So make sure that `n` is exactly the name we expect,
+    -- including the privat prefix.
+    n == mkEqLikeNameFor env declName suffix
+  else
+    false
 
 def GetEqnsFn := Name → MetaM (Option (Array Name))
 
@@ -137,21 +155,21 @@ private def shouldGenerateEqnThms (declName : Name) : MetaM Bool := do
   else
     return false
 
+/-- A mapping from equational theorem to the declaration it was derived from.  -/
 structure EqnsExtState where
-  map    : PHashMap Name (Array Name) := {}
-  mapInv : PHashMap Name Name := {} -- TODO: delete?
+  mapInv : PHashMap Name Name := {}
   deriving Inhabited
 
-/- We generate the equations on demand. -/
+/-- A mapping from equational theorem to the declaration it was derived from.  -/
 builtin_initialize eqnsExt : EnvExtension EqnsExtState ←
   registerEnvExtension (pure {}) (asyncMode := .local)
 
 /--
 Simple equation theorem for nonrecursive definitions.
 -/
-private def mkSimpleEqThm (declName : Name) (suffix := Name.mkSimple unfoldThmSuffix) : MetaM (Option Name) := do
+private def mkSimpleEqThm (declName : Name) : MetaM (Option Name) := do
   if let some (.defnInfo info) := (← getEnv).find? declName then
-    let name := declName ++ suffix
+    let name := mkEqLikeNameFor (← getEnv) declName unfoldThmSuffix
     realizeConst declName name (doRealize name info)
     return some name
   else
@@ -165,6 +183,7 @@ where doRealize name info := do
       name, type, value
       levelParams := info.levelParams
     }
+    inferDefEqAttr name -- should always succeed
 
 /--
 Returns `some declName` if `thmName` is an equational theorem for `declName`.
@@ -183,7 +202,6 @@ Stores in the `eqnsExt` environment extension that `eqThms` are the equational t
 -/
 private def registerEqnThms (declName : Name) (eqThms : Array Name) : CoreM Unit := do
   modifyEnv fun env => eqnsExt.modifyState env fun s => { s with
-    map := s.map.insert declName eqThms
     mapInv := eqThms.foldl (init := s.mapInv) fun mapInv eqThm => mapInv.insert eqThm declName
   }
 
@@ -192,23 +210,21 @@ Equation theorems are generated on demand, check whether they were generated in
 -/
 private partial def alreadyGenerated? (declName : Name) : MetaM (Option (Array Name)) := do
   let env ← getEnv
-  let eq1 := Name.str declName eqn1ThmSuffix
+  let eq1 := mkEqLikeNameFor env declName eqn1ThmSuffix
   if env.contains eq1 then
     let rec loop (idx : Nat) (eqs : Array Name) : MetaM (Array Name) := do
-      let nextEq := mkEqnThmName declName idx
-      if env.contains nextEq then
+      let nextEq := mkEqLikeNameFor env declName s!"{eqnThmSuffixBasePrefix}{idx+1}"
+      if env.containsOnBranch nextEq then
         loop (idx+1) (eqs.push nextEq)
       else
         return eqs
-    let eqs ← loop 2 #[eq1]
+    let eqs ← loop 1 #[eq1]
     registerEqnThms declName eqs
     return some eqs
   else
     return none
 
 private def getEqnsFor?Core (declName : Name) : MetaM (Option (Array Name)) := withLCtx {} {} do
-  if let some eqs := eqnsExt.getState (← getEnv) |>.map.find? declName then
-    return some eqs
   if !(← shouldGenerateEqnThms declName) then
     return none
   if let some eqs ← alreadyGenerated? declName then
@@ -223,7 +239,7 @@ private def getEqnsFor?Core (declName : Name) : MetaM (Option (Array Name)) := w
 Returns equation theorems for the given declaration.
 -/
 def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := withLCtx {} {} do
-  -- This is the entry point for lazy equaion generation. Ignore the current value
+  -- This is the entry point for lazy equation generation. Ignore the current value
   -- of the options, and revert to the default.
   withOptions (eqnAffectingOptions.foldl fun os o => o.set os o.defValue) do
     getEqnsFor?Core declName
@@ -234,6 +250,7 @@ If any equation theorem affecting option is not the default value, create the eq
 def generateEagerEqns (declName : Name) : MetaM Unit := do
   let opts ← getOptions
   if eqnAffectingOptions.any fun o => o.get opts != o.defValue then
+    trace[Elab.definition.eqns] "generating eager equations for {declName}"
     let _ ← getEqnsFor?Core declName
 
 def GetUnfoldEqnFn := Name → MetaM (Option Name)
@@ -276,28 +293,35 @@ By default, we do not create unfold theorems for nonrecursive definitions.
 You can use `nonRec := true` to override this behavior.
 -/
 def getUnfoldEqnFor? (declName : Name) (nonRec := false) : MetaM (Option Name) := withLCtx {} {} do
-  let env ← getEnv
-  let unfoldName := Name.str declName unfoldThmSuffix
-  if env.contains unfoldName then
-    return some unfoldName
-  if (← shouldGenerateEqnThms declName) then
-    for f in (← getUnfoldEqnFnsRef.get) do
-      if let some r ← f declName then
-        unless r == unfoldName do
-          throwError "invalid unfold theorem name `{r}` has been generated expected `{unfoldName}`"
-        return some r
-    if nonRec then
-      return (← mkSimpleEqThm declName)
-   return none
+  let unfoldName := mkEqLikeNameFor (← getEnv) declName unfoldThmSuffix
+  let r? ← withoutExporting do
+    let env := (← getEnv)
+
+    if env.contains unfoldName then
+      return some unfoldName
+    if (← shouldGenerateEqnThms declName) then
+      if (← isRecursiveDefinition declName) then
+        for f in (← getUnfoldEqnFnsRef.get) do
+          if let some r ← f declName then
+            return some r
+      else
+        if nonRec then
+          return (← mkSimpleEqThm declName)
+    return none
+  if let some r := r? then
+    unless r == unfoldName do
+      throwError "invalid unfold theorem name `{r}` has been generated expected `{unfoldName}`"
+  return r?
 
 builtin_initialize
   registerReservedNameAction fun name => do
-    let .str p s := name | return false
-    unless (← getEnv).isSafeDefinition p && !isMatcherCore (← getEnv) p do return false
-    if isEqnReservedNameSuffix s then
-      return (← MetaM.run' <| getEqnsFor? p).isSome
-    if s == unfoldThmSuffix then
-      return (← MetaM.run' <| getUnfoldEqnFor? p (nonRec := true)).isSome
-    return false
+    withTraceNode `ReservedNameAction (pure m!"{exceptBoolEmoji ·} Lean.Meta.Eqns reserved name action for {name}") do
+      if let some (declName, suffix) := declFromEqLikeName (← getEnv) name then
+        if name == mkEqLikeNameFor (← getEnv) declName suffix then
+          if isEqnReservedNameSuffix suffix then
+            return (← MetaM.run' <| getEqnsFor? declName).isSome
+          if suffix == unfoldThmSuffix then
+            return (← MetaM.run' <| getUnfoldEqnFor? declName (nonRec := true)).isSome
+      return false
 
 end Lean.Meta

src/Lean/Meta/Instances.lean

@@ -232,7 +232,18 @@ def addInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) : Meta
   let synthOrder ← computeSynthOrder c projInfo?
   instanceExtension.add { keys, val := c, priority := prio, globalName? := declName, attrKind, synthOrder } attrKind
 
-builtin_initialize
+/--
+Registers type class instances.
+
+The `instance` command, which expands to `@[instance] def`, is usually preferred over using this
+attribute directly. However it might sometimes still be necessary to use this attribute directly,
+in particular for `opaque` instances.
+
+To assign priorities to instances, `@[instance prio]` can be used (where `prio` is a priority).
+This corresponds to the `instance (priority := prio)` notation.
+-/
+@[builtin_init, builtin_doc]
+private def init :=
   registerBuiltinAttribute {
     name  := `instance
     descr := "type class instance"

src/Lean/Meta/LazyDiscrTree.lean

@@ -794,9 +794,9 @@ private def ImportData.new : BaseIO ImportData := do
 structure Cache where
   ngen : NameGenerator
   core : Lean.Core.Cache
-  meta : Lean.Meta.Cache
+  «meta» : Lean.Meta.Cache
 
-def Cache.empty (ngen : NameGenerator) : Cache := { ngen := ngen, core := {}, meta := {} }
+def Cache.empty (ngen : NameGenerator) : Cache := { ngen := ngen, core := {}, «meta» := {} }
 
 def blacklistInsertion (env : Environment) (declName : Name) : Bool :=
   !allowCompletion env declName
@@ -816,7 +816,7 @@ private def addConstImportData
     (name : Name) (constInfo : ConstantInfo) : BaseIO (PreDiscrTree α) := do
   if constInfo.isUnsafe then return tree
   if blacklistInsertion env name then return tree
-  let { ngen, core := core_cache, meta := meta_cache } ← cacheRef.get
+  let { ngen, core := core_cache, «meta» := meta_cache } ← cacheRef.get
   let mstate : Meta.State := { cache := meta_cache }
   cacheRef.set (Cache.empty ngen)
   let ctx : Meta.Context := { config := { transparency := .reducible } }
@@ -824,7 +824,7 @@ private def addConstImportData
   let cstate : Core.State := {env, cache := core_cache, ngen}
   match ←(cm.run cctx cstate).toBaseIO with
   | .ok ((a, ms), cs) =>
-    cacheRef.set { ngen := cs.ngen, core := cs.cache, meta := ms.cache }
+    cacheRef.set { ngen := cs.ngen, core := cs.cache, «meta» := ms.cache }
     pure <| a.foldl (fun t e => t.push e.key e.entry) tree
   | .error e =>
     let i : ImportFailure := {

src/Lean/Meta/Match/MatchEqs.lean

@@ -762,7 +762,7 @@ where go baseName splitterName := withConfig (fun c => { c with etaStruct := .no
     let mut altArgMasks := #[] -- masks produced by `forallAltTelescope`
     for i in [:alts.size] do
       let altNumParams := matchInfo.altNumParams[i]!
-      let thmName := mkEqnThmName baseName idx
+      let thmName := Name.str baseName eqnThmSuffixBase |>.appendIndexAfter idx
       eqnNames := eqnNames.push thmName
       let (notAlt, splitterAltType, splitterAltNumParam, argMask) ←
           forallAltTelescope (← inferType alts[i]!) altNumParams numDiscrEqs

src/Lean/Meta/Match/MatchPatternAttr.lean

@@ -8,6 +8,25 @@ import Lean.Attributes
 
 namespace Lean
 
+/--
+Instructs the pattern matcher to unfold occurrences of this definition.
+
+By default, only constructors and literals can be used for pattern matching. Using
+`@[match_pattern]` allows using other definitions, as long as they eventually reduce to
+constructors and literals.
+
+Example:
+```
+@[match_pattern]
+def yellowString : String := "yellow"
+
+def isYellow (color : String) : Bool :=
+  match color with
+  | yellowString => true
+  | _ => false
+```
+-/
+@[builtin_doc]
 builtin_initialize matchPatternAttr : TagAttribute ←
   registerTagAttribute `match_pattern "mark that a definition can be used in a pattern (remark: the dependent pattern matching compiler will unfold the definition)"
 

src/Lean/Meta/SizeOf.lean

@@ -8,6 +8,7 @@ import Init.Data.List.BasicAux
 import Lean.AddDecl
 import Lean.Meta.AppBuilder
 import Lean.Meta.Instances
+import Lean.DefEqAttrib
 
 namespace Lean.Meta
 
@@ -148,14 +149,16 @@ partial def mkSizeOfFn (recName : Name) (declName : Name): MetaM Unit := do
           trace[Meta.sizeOf] "declName: {declName}"
           trace[Meta.sizeOf] "type: {sizeOfType}"
           trace[Meta.sizeOf] "val: {sizeOfValue}"
-          addDecl <| Declaration.defnDecl {
-            name        := declName
-            levelParams := levelParams
-            type        := sizeOfType
-            value       := sizeOfValue
-            safety      := DefinitionSafety.safe
-            hints       := ReducibilityHints.abbrev
-          }
+          -- We expose the `sizeOf` functions so that the `spec` theorems can be publicly `defeq`
+          withExporting do
+            addDecl <| Declaration.defnDecl {
+              name        := declName
+              levelParams := levelParams
+              type        := sizeOfType
+              value       := sizeOfValue
+              safety      := DefinitionSafety.safe
+              hints       := ReducibilityHints.abbrev
+            }
 
 /--
   Create `sizeOf` functions for all inductive datatypes in the mutual inductive declaration containing `typeName`
@@ -457,6 +460,7 @@ private def mkSizeOfSpecTheorem (indInfo : InductiveVal) (sizeOfFns : Array Name
         type        := thmType
         value       := thmValue
       }
+      inferDefEqAttr thmName
       simpAttr.add thmName default AttributeKind.global
 
 private def mkSizeOfSpecTheorems (indTypeNames : Array Name) (sizeOfFns : Array Name) (recMap : NameMap Name) : MetaM Unit := do
@@ -500,14 +504,16 @@ def mkSizeOfInstances (typeName : Name) : MetaM Unit := do
                   let instDeclType ← mkForallFVars (xs ++ localInsts) sizeOfIndType
                   let instDeclValue ← mkLambdaFVars (xs ++ localInsts) sizeOfMk
                   trace[Meta.sizeOf] ">> {instDeclName} : {instDeclType}"
-                  addDecl <| Declaration.defnDecl {
-                    name        := instDeclName
-                    levelParams := indInfo.levelParams
-                    type        := instDeclType
-                    value       := instDeclValue
-                    safety      := .safe
-                    hints       := .abbrev
-                  }
+                  -- We expose the `sizeOf` instance so that the `spec` theorems can be publicly `defeq`
+                  withExporting do
+                    addDecl <| Declaration.defnDecl {
+                      name        := instDeclName
+                      levelParams := indInfo.levelParams
+                      type        := instDeclType
+                      value       := instDeclValue
+                      safety      := .safe
+                      hints       := .abbrev
+                    }
                   addInstance instDeclName AttributeKind.global (eval_prio default)
         if genSizeOfSpec.get (← getOptions) then
           mkSizeOfSpecTheorems indInfo.all.toArray fns recMap

src/Lean/Meta/Tactic/AuxLemma.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.AddDecl
 import Lean.Meta.Basic
+import Lean.DefEqAttrib
 
 namespace Lean.Meta
 
@@ -27,7 +28,8 @@ builtin_initialize auxLemmasExt : EnvExtension AuxLemmas ←
   This method is useful for tactics (e.g., `simp`) that may perform preprocessing steps to lemmas provided by
   users. For example, `simp` preprocessor may convert a lemma into multiple ones.
 -/
-def mkAuxLemma (levelParams : List Name) (type : Expr) (value : Expr) (kind? : Option Name := none) (cache := true) : MetaM Name := do
+def mkAuxLemma (levelParams : List Name) (type : Expr) (value : Expr) (kind? : Option Name := none)
+    (cache := true) (inferRfl := false) : MetaM Name := do
   let env ← getEnv
   let s := auxLemmasExt.getState env
   let mkNewAuxLemma := do
@@ -47,6 +49,8 @@ def mkAuxLemma (levelParams : List Name) (type : Expr) (value : Expr) (kind? : O
           levelParams, type, value
         }
     addDecl decl
+    if inferRfl then
+      inferDefEqAttr auxName
     modifyEnv fun env => auxLemmasExt.modifyState env fun ⟨lemmas⟩ => ⟨lemmas.insert type (auxName, levelParams)⟩
     return auxName
   if cache then