fix test

Links to the language reference include a version slug, either `latest`
or `v4.X.0`. These are included in hovers, which then get tested. To
avoid test breakages, in the testing framework we normalize all such URL
prefixes back to `REFERENCE`.

CMakeLists.txt

@@ -20,6 +20,9 @@ foreach(var ${vars})
     elseif("${var}" MATCHES "LLVM*|PKG_CONFIG|USE_LAKE|USE_MIMALLOC")
       list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
     endif()
+  elseif("${var}" MATCHES "USE_MIMALLOC")
+    list(APPEND CL_ARGS "-D${var}=${${var}}")
+    list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
   elseif(("${var}" MATCHES "CMAKE_.*") AND NOT ("${var}" MATCHES "CMAKE_BUILD_TYPE") AND NOT ("${var}" MATCHES "CMAKE_HOME_DIRECTORY"))
     list(APPEND PLATFORM_ARGS "-D${var}=${${var}}")
   endif()

CMakePresets.json

@@ -30,6 +30,7 @@
         "LEANC_EXTRA_CC_FLAGS": "-fsanitize=address,undefined",
         "LEAN_EXTRA_LINKER_FLAGS": "-fsanitize=address,undefined -fsanitize-link-c++-runtime",
         "SMALL_ALLOCATOR": "OFF",
+        "USE_MIMALLOC": "OFF",
         "BSYMBOLIC": "OFF",
         "LEAN_TEST_VARS": "MAIN_STACK_SIZE=16000"
       },

doc/dev/release_checklist.md

@@ -42,6 +42,10 @@ We'll use `v4.6.0` as the intended release version as a running example.
   - In order to have the access rights to push to these repositories and merge PRs,
     you will need to be a member of the `lean-release-managers` team at both `leanprover-community` and `leanprover`.
     Contact Kim Morrison (@kim-em) to arrange access.
+  - There is an experimental script that will guide you through the steps for each of the repositories below.
+    The script should be invoked as
+    `script/release_steps.py vx.y.x <repo>` where `<repo>` is a case-insensitive substring of the repo name.
+    For example: `script/release_steps.py v4.6.0 batt` will guide you through the steps for the Batteries repository.
   - For each of the repositories listed below:
     - Make a PR to `master`/`main` changing the toolchain to `v4.6.0`
       - The usual branch name would be `bump_to_v4.6.0`.

script/merge_remote.py

@@ -0,0 +1,165 @@
+#!/usr/bin/env python3
+
+"""
+Merge a tag into a branch on a GitHub repository.
+
+This script checks if a specified tag can be merged cleanly into a branch and performs
+the merge if possible. If the merge cannot be done cleanly, it prints a helpful message.
+
+Usage:
+    python3 merge_remote.py <org/repo> <branch> <tag>
+
+Arguments:
+    org/repo: GitHub repository in the format 'organization/repository'
+    branch: The target branch to merge into
+    tag: The tag to merge from
+
+Example:
+    python3 merge_remote.py leanprover/mathlib4 stable v4.6.0
+
+The script uses the GitHub CLI (`gh`), so make sure it's installed and authenticated.
+"""
+
+import argparse
+import subprocess
+import sys
+import tempfile
+import os
+import shutil
+
+
+def run_command(command, check=True, capture_output=True):
+    """Run a shell command and return the result."""
+    try:
+        result = subprocess.run(
+            command,
+            check=check,
+            shell=True,
+            text=True,
+            capture_output=capture_output
+        )
+        return result
+    except subprocess.CalledProcessError as e:
+        if capture_output:
+            print(f"Command failed: {command}")
+            print(f"Error: {e.stderr}")
+        return e
+
+
+def clone_repo(repo, temp_dir):
+    """Clone the repository to a temporary directory using shallow clone."""
+    print(f"Shallow cloning {repo}...")
+    # Use --depth=1 for shallow clone
+    clone_result = run_command(f"gh repo clone {repo} {temp_dir} -- --depth=1", check=False)
+    if clone_result.returncode != 0:
+        print(f"Failed to clone repository {repo}.")
+        print(f"Error: {clone_result.stderr}")
+        return False
+    return True
+
+
+def check_and_merge(repo, branch, tag, temp_dir):
+    """Check if tag can be merged into branch and perform the merge if possible."""
+    # Change to the temporary directory
+    os.chdir(temp_dir)
+    
+    # Fetch only the specific branch and tag we need
+    print(f"Fetching branch '{branch}' and tag '{tag}'...")
+    fetch_branch = run_command(f"git fetch origin {branch}")
+    if fetch_branch.returncode != 0:
+        print(f"Error: Failed to fetch branch '{branch}'.")
+        return False
+        
+    fetch_tag = run_command(f"git fetch origin tag {tag}")
+    if fetch_tag.returncode != 0:
+        print(f"Error: Failed to fetch tag '{tag}'.")
+        return False
+
+    # Check if branch exists
+    branch_check = run_command(f"git branch -r | grep origin/{branch}")
+    if branch_check.returncode != 0:
+        print(f"Error: Branch '{branch}' does not exist in repository.")
+        return False
+
+    # Check if tag exists
+    tag_check = run_command(f"git tag -l {tag}")
+    if tag_check.returncode != 0 or not tag_check.stdout.strip():
+        print(f"Error: Tag '{tag}' does not exist in repository.")
+        return False
+
+    # Checkout the branch
+    print(f"Checking out branch '{branch}'...")
+    checkout_result = run_command(f"git checkout -b {branch} origin/{branch}")
+    if checkout_result.returncode != 0:
+        return False
+
+    # Try merging the tag in a dry-run to check if it can be merged cleanly
+    print(f"Checking if {tag} can be merged cleanly into {branch}...")
+    merge_check = run_command(f"git merge --no-commit --no-ff {tag}", check=False)
+    
+    if merge_check.returncode != 0:
+        print(f"Cannot merge {tag} cleanly into {branch}.")
+        print("Merge conflicts would occur. Aborting merge.")
+        run_command("git merge --abort")
+        return False
+    
+    # Abort the test merge
+    run_command("git reset --hard HEAD")
+    
+    # Now perform the actual merge and push to remote
+    print(f"Merging {tag} into {branch}...")
+    merge_result = run_command(f"git merge {tag} --no-edit")
+    if merge_result.returncode != 0:
+        print(f"Failed to merge {tag} into {branch}.")
+        return False
+    
+    print(f"Pushing changes to remote...")
+    push_result = run_command(f"git push origin {branch}")
+    if push_result.returncode != 0:
+        print(f"Failed to push changes to remote.")
+        return False
+    
+    print(f"Successfully merged {tag} into {branch} and pushed to remote.")
+    return True
+
+
+def main():
+    parser = argparse.ArgumentParser(
+        description="Merge a tag into a branch on a GitHub repository.",
+        formatter_class=argparse.RawDescriptionHelpFormatter,
+        epilog="""
+Examples:
+  %(prog)s leanprover/mathlib4 stable v4.6.0    Merge tag v4.6.0 into stable branch
+
+The script will:
+1. Clone the repository
+2. Check if the tag and branch exist
+3. Check if the tag can be merged cleanly into the branch
+4. Perform the merge and push to remote if possible
+        """
+    )
+    parser.add_argument("repo", help="GitHub repository in the format 'organization/repository'")
+    parser.add_argument("branch", help="The target branch to merge into")
+    parser.add_argument("tag", help="The tag to merge from")
+    
+    args = parser.parse_args()
+    
+    # Create a temporary directory for the repository
+    temp_dir = tempfile.mkdtemp()
+    try:
+        # Clone the repository
+        if not clone_repo(args.repo, temp_dir):
+            sys.exit(1)
+        
+        # Check if the tag can be merged and perform the merge
+        if not check_and_merge(args.repo, args.branch, args.tag, temp_dir):
+            sys.exit(1)
+        
+    finally:
+        # Clean up the temporary directory
+        print(f"Cleaning up temporary files...")
+        shutil.rmtree(temp_dir)
+
+
+if __name__ == "__main__":
+    main() 

script/release_checklist.py

@@ -8,6 +8,11 @@ import subprocess
 import sys
 import os
 
+def debug(verbose, message):
+    """Print debug message if verbose mode is enabled."""
+    if verbose:
+        print(f"    [DEBUG] {message}")
+
 def parse_repos_config(file_path):
     with open(file_path, "r") as f:
         return yaml.safe_load(f)["repositories"]
@@ -90,7 +95,7 @@ def is_version_gte(version1, version2):
         return False
     return parse_version(version1) >= parse_version(version2)
 
-def is_merged_into_stable(repo_url, tag_name, stable_branch, github_token):
+def is_merged_into_stable(repo_url, tag_name, stable_branch, github_token, verbose=False):
     # First get the commit SHA for the tag
     api_base = repo_url.replace("https://github.com/", "https://api.github.com/repos/")
     headers = {'Authorization': f'token {github_token}'} if github_token else {}
@@ -98,6 +103,7 @@ def is_merged_into_stable(repo_url, tag_name, stable_branch, github_token):
     # Get tag's commit SHA
     tag_response = requests.get(f"{api_base}/git/refs/tags/{tag_name}", headers=headers)
     if tag_response.status_code != 200:
+        debug(verbose, f"Could not fetch tag {tag_name}, status code: {tag_response.status_code}")
         return False
     
     # Handle both single object and array responses
@@ -106,22 +112,48 @@ def is_merged_into_stable(repo_url, tag_name, stable_branch, github_token):
         # Find the exact matching tag in the list
         matching_tags = [tag for tag in tag_data if tag['ref'] == f'refs/tags/{tag_name}']
         if not matching_tags:
+            debug(verbose, f"No matching tag found for {tag_name} in response list")
             return False
         tag_sha = matching_tags[0]['object']['sha']
     else:
         tag_sha = tag_data['object']['sha']
-
+    
+    # Check if the tag is an annotated tag and get the actual commit SHA
+    if tag_data.get('object', {}).get('type') == 'tag' or (
+        isinstance(tag_data, list) and 
+        matching_tags and 
+        matching_tags[0].get('object', {}).get('type') == 'tag'):
+        
+        # Get the commit that this tag points to
+        tag_obj_response = requests.get(f"{api_base}/git/tags/{tag_sha}", headers=headers)
+        if tag_obj_response.status_code == 200:
+            tag_obj = tag_obj_response.json()
+            if 'object' in tag_obj and tag_obj['object']['type'] == 'commit':
+                commit_sha = tag_obj['object']['sha']
+                debug(verbose, f"Tag is annotated. Resolved commit SHA: {commit_sha}")
+                tag_sha = commit_sha  # Use the actual commit SHA
+    
     # Get commits on stable branch containing this SHA
     commits_response = requests.get(
         f"{api_base}/commits?sha={stable_branch}&per_page=100",
         headers=headers
     )
     if commits_response.status_code != 200:
+        debug(verbose, f"Could not fetch commits for branch {stable_branch}, status code: {commits_response.status_code}")
         return False
 
     # Check if any commit in stable's history matches our tag's SHA
     stable_commits = [commit['sha'] for commit in commits_response.json()]
-    return tag_sha in stable_commits
+    
+    is_merged = tag_sha in stable_commits
+    
+    debug(verbose, f"Tag SHA: {tag_sha}")
+    debug(verbose, f"First 5 stable commits: {stable_commits[:5]}")
+    debug(verbose, f"Total stable commits fetched: {len(stable_commits)}")
+    if not is_merged:
+        debug(verbose, f"Tag SHA not found in first {len(stable_commits)} commits of stable branch")
+    
+    return is_merged
 
 def is_release_candidate(version):
     return "-rc" in version
@@ -195,13 +227,15 @@ def pr_exists_with_title(repo_url, title, github_token):
     return None
 
 def main():
+    parser = argparse.ArgumentParser(description="Check release status of Lean4 repositories")
+    parser.add_argument("toolchain", help="The toolchain version to check (e.g., v4.6.0)")
+    parser.add_argument("--verbose", "-v", action="store_true", help="Enable verbose debugging output")
+    args = parser.parse_args()
+
     github_token = get_github_token()
-
-    if len(sys.argv) != 2:
-        print("Usage: python3 release_checklist.py <toolchain>")
-        sys.exit(1)
-
-    toolchain = sys.argv[1]
+    toolchain = args.toolchain
+    verbose = args.verbose
+    
     stripped_toolchain = strip_rc_suffix(toolchain)
     lean_repo_url = "https://github.com/leanprover/lean4"
 
@@ -291,6 +325,7 @@ def main():
                 print(f"  ✅ PR with title '{pr_title}' exists: #{pr_number} ({pr_url})")
             else:
                 print(f"  ❌ PR with title '{pr_title}' does not exist")
+                print(f"     Run `script/release_steps.py {toolchain} {name}` to create it")
             repo_status[name] = False
             continue
         print(f"  ✅ On compatible toolchain (>= {toolchain})")
@@ -303,8 +338,10 @@ def main():
             print(f"  ✅ Tag {toolchain} exists")
 
         if check_stable and not is_release_candidate(toolchain):
-            if not is_merged_into_stable(url, toolchain, "stable", github_token):
+            if not is_merged_into_stable(url, toolchain, "stable", github_token, verbose):
+                org_repo = extract_org_repo_from_url(url)
                 print(f"  ❌ Tag {toolchain} is not merged into stable")
+                print(f"     Run `script/merge_remote.py {org_repo} stable {toolchain}` to merge it")
                 repo_status[name] = False
                 continue
             print(f"  ✅ Tag {toolchain} is merged into stable")

script/release_repos.yml

@@ -85,6 +85,7 @@ repositories:
       - Batteries
       - doc-gen4
       - import-graph
+      - plausible
 
   - name: REPL
     url: https://github.com/leanprover-community/repl

script/release_steps.py

@@ -0,0 +1,145 @@
+#!/usr/bin/env python3
+
+"""
+Generate release steps script for Lean4 repositories.
+
+This script helps automate the release process for Lean4 and its dependent repositories
+by generating step-by-step instructions for updating toolchains, creating tags,
+and managing branches.
+
+Usage:
+    python3 release_steps.py <version> <repo>
+
+Arguments:
+    version: The version to set in the lean-toolchain file (e.g., v4.6.0)
+    repo: A substring of the repository name as specified in release_repos.yml
+
+Example:
+    python3 release_steps.py v4.6.0 mathlib
+    python3 release_steps.py v4.6.0 batt
+
+The script reads repository configurations from release_repos.yml in the same directory.
+Each repository may have specific requirements for:
+- Branch management
+- Toolchain updates
+- Dependency updates
+- Tagging conventions
+- Stable branch handling
+"""
+
+import argparse
+import yaml
+import os
+import sys
+import re
+
+def load_repos_config(file_path):
+    with open(file_path, "r") as f:
+        return yaml.safe_load(f)["repositories"]
+
+def find_repo(repo_substring, config):
+    pattern = re.compile(re.escape(repo_substring), re.IGNORECASE)
+    matching_repos = [r for r in config if pattern.search(r["name"])]
+    if not matching_repos:
+        print(f"Error: No repository matching '{repo_substring}' found in configuration.")
+        sys.exit(1)
+    if len(matching_repos) > 1:
+        print(f"Error: Multiple repositories matching '{repo_substring}' found in configuration: {', '.join(r['name'] for r in matching_repos)}")
+        sys.exit(1)
+    return matching_repos[0]
+
+def generate_script(repo, version, config):
+    repo_config = find_repo(repo, config)
+    repo_name = repo_config['name']
+    repo_url = repo_config['url']
+    # Extract the last component of the URL, removing the .git extension if present
+    repo_dir = repo_url.split('/')[-1].replace('.git', '')
+    default_branch = repo_config.get("branch", "main")
+    dependencies = repo_config.get("dependencies", [])
+    requires_tagging = repo_config.get("toolchain-tag", True)
+    has_stable_branch = repo_config.get("stable-branch", True)
+
+    script_lines = [
+        f"cd {repo_dir}",
+        "git fetch",
+        f"git checkout {default_branch} && git pull",
+        f"git checkout -b bump_to_{version}",
+        f"echo leanprover/lean4:{version} > lean-toolchain",
+    ]
+
+    # Special cases for specific repositories
+    if repo_name == "REPL":
+        script_lines.extend([
+            "lake update",
+            "cd test/Mathlib",
+            f"perl -pi -e 's/rev = \"v\\d+\\.\\d+\\.\\d+(-rc\\d+)?\"/rev = \"{version}\"/g' lakefile.toml",
+            f"echo leanprover/lean4:{version} > lean-toolchain",
+            "lake update",
+            "cd ../..",
+            "./test.sh"
+        ])
+    elif dependencies:
+        script_lines.append('echo "Please update the dependencies in lakefile.{lean,toml}"')
+        script_lines.append("lake update")
+
+    script_lines.append("")
+
+    if re.search(r'rc\d+$', version) and repo_name in ["Batteries", "Mathlib"]:
+        script_lines.extend([
+            "echo 'This repo has nightly-testing infrastructure'",
+            f"git merge bump/{version}",
+            "echo 'Please resolve any conflicts.'",
+            ""
+        ])
+
+    script_lines.extend([
+        f'git commit -am "chore: bump toolchain to {version}"',
+        "gh pr create",
+        "echo 'Please review the PR and merge it.'",
+        ""
+    ])
+
+    # Special cases for specific repositories
+    if repo_name == "ProofWidgets4":
+        script_lines.append(f"echo 'Note: Follow the version convention of the repository for tagging.'")
+    elif requires_tagging:
+        script_lines.append(f"git checkout {default_branch} && git pull")
+        script_lines.append(f'[ "$(cat lean-toolchain)" = "leanprover/lean4:{version}" ] && git tag -a {version} -m \'Release {version}\' && git push origin --tags || echo "Error: lean-toolchain does not contain expected version {version}"')
+
+    if has_stable_branch:
+        script_lines.extend([
+            "git checkout stable && git pull",
+            f"git merge {version} --no-edit",
+            "git push origin stable"
+        ])
+
+    return "\n".join(script_lines)
+
+def main():
+    parser = argparse.ArgumentParser(
+        description="Generate release steps script for Lean4 repositories.",
+        formatter_class=argparse.RawDescriptionHelpFormatter,
+        epilog="""
+Examples:
+  %(prog)s v4.6.0 mathlib    Generate steps for updating Mathlib to v4.6.0
+  %(prog)s v4.6.0 batt       Generate steps for updating Batteries to v4.6.0
+  
+The script will generate shell commands to:
+1. Update the lean-toolchain file
+2. Create appropriate branches and commits
+3. Create pull requests
+4. Create version tags
+5. Update stable branches where applicable"""
+    )
+    parser.add_argument("version", help="The version to set in the lean-toolchain file (e.g., v4.6.0)")
+    parser.add_argument("repo", help="A substring of the repository name as specified in release_repos.yml")
+    args = parser.parse_args()
+
+    config_path = os.path.join(os.path.dirname(__file__), "release_repos.yml")
+    config = load_repos_config(config_path)
+
+    script = generate_script(args.repo, args.version, config)
+    print(script)
+
+if __name__ == "__main__":
+    main()

src/Init/Data/Array/Lemmas.lean

@@ -3893,7 +3893,7 @@ theorem all_map {xs : Array α} {p : β → Bool} : (xs.map f).all p = xs.all (p
 
 /-- Variant of `all_filter` with a side condition for the `stop` argument. -/
 @[simp] theorem all_filter' {xs : Array α} {p q : α → Bool} (w : stop = (xs.filter p).size) :
-    (xs.filter p).all q 0 stop = xs.all fun a => p a → q a := by
+    (xs.filter p).all q 0 stop = xs.all fun a => !(p a) || q a := by
   subst w
   rcases xs with ⟨xs⟩
   rw [List.filter_toArray]
@@ -3904,7 +3904,7 @@ theorem any_filter {xs : Array α} {p q : α → Bool} :
   simp
 
 theorem all_filter {xs : Array α} {p q : α → Bool} :
-    (xs.filter p).all q 0 = xs.all fun a => p a → q a := by
+    (xs.filter p).all q 0 = xs.all fun a => !(p a) || q a := by
   simp
 
 /-- Variant of `any_filterMap` with a side condition for the `stop` argument. -/

src/Init/Data/BitVec/Bitblast.lean

@@ -1752,4 +1752,9 @@ theorem extractLsb'_mul {w len} {x y : BitVec w} (hlen : len ≤ w) :
     (x * y).extractLsb' 0 len = (x.extractLsb' 0 len) * (y.extractLsb' 0 len) := by
   simp [← setWidth_eq_extractLsb' hlen, setWidth_mul _ _ hlen]
 
+/-- Adding bitvectors that are zero in complementary positions equals concatenation. -/
+theorem append_add_append_eq_append {v w : Nat} {x : BitVec v} {y : BitVec w} :
+    (x ++ 0#w) + (0#v ++ y) = x ++ y := by
+  rw [add_eq_or_of_and_eq_zero] <;> ext i <;> simp
+
 end BitVec

src/Init/Data/BitVec/Lemmas.lean

@@ -3339,6 +3339,14 @@ theorem sub_toAdd {n} (x y : BitVec n) : x - y = x + - y := by
   simp only [toNat_sub, toNat_add, toNat_neg, Nat.add_mod_mod]
   rw [Nat.add_comm]
 
+theorem add_left_neg (x : BitVec w) : -x + x = 0#w := by
+  apply toInt_inj.mp
+  simp [toInt_neg, Int.add_left_neg]
+
+theorem add_right_neg (x : BitVec w) : x + -x = 0#w := by
+  rw [BitVec.add_comm]
+  exact add_left_neg x
+
 @[simp] theorem neg_zero (n:Nat) : -BitVec.ofNat n 0 = BitVec.ofNat n 0 := by apply eq_of_toNat_eq ; simp
 
 theorem add_sub_cancel (x y : BitVec w) : x + y - y = x := by

src/Init/Data/Int/Linear.lean

@@ -1796,6 +1796,29 @@ theorem of_not_dvd (a b : Int) : a != 0 → ¬ (a ∣ b) → b % a > 0 := by
   simp [h₁] at h₂
   assumption
 
+def le_of_le_cert (p q : Poly) (k : Nat) : Bool :=
+  q == p.addConst (- k)
+
+theorem le_of_le (ctx : Context) (p q : Poly) (k : Nat)
+    : le_of_le_cert p q k → p.denote' ctx ≤ 0 → q.denote' ctx ≤ 0 := by
+  simp [le_of_le_cert]; intro; subst q; simp
+  intro h
+  simp [Lean.Omega.Int.add_le_zero_iff_le_neg']
+  exact Int.le_trans h (Int.ofNat_zero_le _)
+
+def not_le_of_le_cert (p q : Poly) (k : Nat) : Bool :=
+  q == (p.mul (-1)).addConst (1 + k)
+
+theorem not_le_of_le (ctx : Context) (p q : Poly) (k : Nat)
+    : not_le_of_le_cert p q k → p.denote' ctx ≤ 0 → ¬ q.denote' ctx ≤ 0 := by
+  simp [not_le_of_le_cert]; intro; subst q
+  intro h
+  apply Int.pos_of_neg_neg
+  apply Int.lt_of_add_one_le
+  simp [Int.neg_add, Int.neg_sub]
+  rw [← Int.add_assoc, ← Int.add_assoc, Int.add_neg_cancel_right, Lean.Omega.Int.add_le_zero_iff_le_neg']
+  simp; exact Int.le_trans h (Int.ofNat_zero_le _)
+
 end Int.Linear
 
 theorem Int.not_le_eq (a b : Int) : (¬a ≤ b) = (b + 1 ≤ a) := by

src/Init/Data/List/Lemmas.lean

@@ -3361,7 +3361,7 @@ theorem all_eq_not_any_not {l : List α} {p : α → Bool} : l.all p = !l.any (!
     split <;> simp_all
 
 @[simp] theorem all_filter {l : List α} {p q : α → Bool} :
-    (filter p l).all q = l.all fun a => p a → q a := by
+    (filter p l).all q = l.all fun a => !(p a) || q a := by
   induction l with
   | nil => rfl
   | cons h t ih =>

src/Init/Data/Nat/Basic.lean

@@ -777,31 +777,34 @@ protected theorem pow_succ (n m : Nat) : n^(succ m) = n^m * n :=
 protected theorem pow_add_one (n m : Nat) : n^(m + 1) = n^m * n :=
   rfl
 
-protected theorem pow_zero (n : Nat) : n^0 = 1 := rfl
+@[simp] protected theorem pow_zero (n : Nat) : n^0 = 1 := rfl
 
-theorem pow_le_pow_left {n m : Nat} (h : n ≤ m) : ∀ (i : Nat), n^i ≤ m^i
+@[simp] protected theorem pow_one (a : Nat) : a ^ 1 = a := by
+  simp [Nat.pow_succ]
+
+protected theorem pow_le_pow_left {n m : Nat} (h : n ≤ m) : ∀ (i : Nat), n^i ≤ m^i
   | 0      => Nat.le_refl _
-  | succ i => Nat.mul_le_mul (pow_le_pow_left h i) h
+  | succ i => Nat.mul_le_mul (Nat.pow_le_pow_left h i) h
 
-theorem pow_le_pow_right {n : Nat} (hx : n > 0) {i : Nat} : ∀ {j}, i ≤ j → n^i ≤ n^j
+protected theorem pow_le_pow_right {n : Nat} (hx : n > 0) {i : Nat} : ∀ {j}, i ≤ j → n^i ≤ n^j
   | 0,      h =>
     have : i = 0 := eq_zero_of_le_zero h
     this.symm ▸ Nat.le_refl _
   | succ j, h =>
     match le_or_eq_of_le_succ h with
     | Or.inl h => show n^i ≤ n^j * n from
-      have : n^i * 1 ≤ n^j * n := Nat.mul_le_mul (pow_le_pow_right hx h) hx
+      have : n^i * 1 ≤ n^j * n := Nat.mul_le_mul (Nat.pow_le_pow_right hx h) hx
       Nat.mul_one (n^i) ▸ this
     | Or.inr h =>
       h.symm ▸ Nat.le_refl _
 
 set_option linter.missingDocs false in
 @[deprecated Nat.pow_le_pow_left (since := "2025-02-17")]
-abbrev pow_le_pow_of_le_left := @pow_le_pow_left
+abbrev pow_le_pow_of_le_left := @Nat.pow_le_pow_left
 
 set_option linter.missingDocs false in
 @[deprecated Nat.pow_le_pow_right (since := "2025-02-17")]
-abbrev pow_le_pow_of_le_right := @pow_le_pow_right
+abbrev pow_le_pow_of_le_right := @Nat.pow_le_pow_right
 
 protected theorem pow_pos (h : 0 < a) : 0 < a^n :=
   match n with
@@ -822,6 +825,33 @@ protected theorem two_pow_pos (w : Nat) : 0 < 2^w := Nat.pow_pos (by decide)
 instance {n m : Nat} [NeZero n] : NeZero (n^m) :=
   ⟨Nat.ne_zero_iff_zero_lt.mpr (Nat.pow_pos (pos_of_neZero _))⟩
 
+protected theorem mul_pow (a b n : Nat) : (a * b) ^ n = a ^ n * b ^ n := by
+  induction n with
+  | zero => simp [Nat.pow_zero]
+  | succ n ih =>
+    rw [Nat.pow_succ, ih, Nat.pow_succ, Nat.pow_succ, ← Nat.mul_assoc, ← Nat.mul_assoc]
+    congr 1
+    rw [Nat.mul_assoc, Nat.mul_assoc, Nat.mul_comm _ a]
+
+protected theorem pow_lt_pow_left {a b n : Nat} (hab : a < b) (h : n ≠ 0) : a ^ n < b ^ n := by
+  cases n with
+  | zero => simp at h
+  | succ n =>
+    clear h
+    induction n with
+    | zero => simpa
+    | succ n ih =>
+      rw [Nat.pow_succ a, Nat.pow_succ b]
+      exact Nat.lt_of_le_of_lt (Nat.mul_le_mul_left _ (Nat.le_of_lt hab))
+        (Nat.mul_lt_mul_of_pos_right ih (Nat.lt_of_le_of_lt (Nat.zero_le _) hab))
+
+protected theorem pow_left_inj {a b n : Nat} (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b := by
+  refine ⟨fun h => ?_, (· ▸ rfl)⟩
+  match Nat.lt_trichotomy a b with
+  | Or.inl hab => exact False.elim (absurd h (ne_of_lt (Nat.pow_lt_pow_left hab hn)))
+  | Or.inr (Or.inl hab) => exact hab
+  | Or.inr (Or.inr hab) => exact False.elim (absurd h (Nat.ne_of_lt' (Nat.pow_lt_pow_left hab hn)))
+
 /-! # min/max -/
 
 /--
@@ -1170,9 +1200,15 @@ protected theorem mul_sub_right_distrib (n m k : Nat) : (n - m) * k = n * k - m
   | zero => simp
   | succ m ih => rw [Nat.sub_succ, Nat.pred_mul, ih, succ_mul, Nat.sub_sub]; done
 
+protected theorem sub_mul (n m k : Nat) : (n - m) * k = n * k - m * k :=
+  Nat.mul_sub_right_distrib n m k
+
 protected theorem mul_sub_left_distrib (n m k : Nat) : n * (m - k) = n * m - n * k := by
   rw [Nat.mul_comm, Nat.mul_sub_right_distrib, Nat.mul_comm m n, Nat.mul_comm n k]
 
+protected theorem mul_sub (n m k : Nat) : n * (m - k) = n * m - n * k :=
+  Nat.mul_sub_left_distrib n m k
+
 /-! # Helper normalization theorems -/
 
 theorem not_le_eq (a b : Nat) : (¬ (a ≤ b)) = (b + 1 ≤ a) :=

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

@@ -501,7 +501,7 @@ theorem and_lt_two_pow (x : Nat) {y n : Nat} (right : y < 2^n) : (x &&& y) < 2^n
   have yf : testBit y i = false := by
           apply Nat.testBit_lt_two_pow
           apply Nat.lt_of_lt_of_le right
-          exact pow_le_pow_right Nat.zero_lt_two i_ge_n
+          exact Nat.pow_le_pow_right Nat.zero_lt_two i_ge_n
   simp [testBit_and, yf]
 
 @[simp] theorem and_two_pow_sub_one_eq_mod (x n : Nat) : x &&& 2^n - 1 = x % 2^n := by

src/Init/Data/Nat/Dvd.lean

@@ -21,6 +21,12 @@ protected theorem dvd_trans {a b c : Nat} (h₁ : a ∣ b) (h₂ : b ∣ c) : a
   | ⟨d, (h₃ : b = a * d)⟩, ⟨e, (h₄ : c = b * e)⟩ =>
     ⟨d * e, show c = a * (d * e) by simp[h₃,h₄, Nat.mul_assoc]⟩
 
+protected theorem dvd_mul_left_of_dvd {a b : Nat} (h : a ∣ b) (c : Nat) : a ∣ c * b :=
+  Nat.dvd_trans h (Nat.dvd_mul_left _ _)
+
+protected theorem dvd_mul_right_of_dvd {a b : Nat} (h : a ∣ b) (c : Nat) : a ∣ b * c :=
+  Nat.dvd_trans h (Nat.dvd_mul_right _ _)
+
 protected theorem eq_zero_of_zero_dvd {a : Nat} (h : 0 ∣ a) : a = 0 :=
   let ⟨c, H'⟩ := h; H'.trans c.zero_mul
 
@@ -106,8 +112,26 @@ protected theorem dvd_of_mul_dvd_mul_left
 protected theorem dvd_of_mul_dvd_mul_right (kpos : 0 < k) (H : m * k ∣ n * k) : m ∣ n := by
   rw [Nat.mul_comm m k, Nat.mul_comm n k] at H; exact Nat.dvd_of_mul_dvd_mul_left kpos H
 
-theorem dvd_sub {k m n : Nat} (H : n ≤ m) (h₁ : k ∣ m) (h₂ : k ∣ n) : k ∣ m - n :=
-  (Nat.dvd_add_iff_left h₂).2 <| by rwa [Nat.sub_add_cancel H]
+theorem dvd_sub {k m n : Nat} (h₁ : k ∣ m) (h₂ : k ∣ n) : k ∣ m - n :=
+  if H : n ≤ m then
+    (Nat.dvd_add_iff_left h₂).2 <| by rwa [Nat.sub_add_cancel H]
+  else
+    Nat.sub_eq_zero_of_le (Nat.le_of_not_le H) ▸ Nat.dvd_zero k
+
+theorem dvd_sub_iff_right {m n k : Nat} (hkn : k ≤ n) (h : m ∣ n) : m ∣ n - k ↔ m ∣ k := by
+  refine ⟨?_, dvd_sub h⟩
+  let ⟨x, hx⟩ := h
+  cases hx
+  intro hy
+  let ⟨y, hy⟩ := hy
+  have hk : k = m * (x - y) := by
+    rw [Nat.sub_eq_iff_eq_add hkn] at hy
+    rw [Nat.mul_sub, hy, Nat.add_comm, Nat.add_sub_cancel]
+  exact hk ▸ Nat.dvd_mul_right _ _
+
+theorem dvd_sub_iff_left {m n k : Nat} (hkn : k ≤ n) (h : m ∣ k) : m ∣ n - k ↔ m ∣ n := by
+  rw (occs := [2]) [← Nat.sub_add_cancel hkn]
+  exact Nat.dvd_add_iff_left h
 
 protected theorem mul_dvd_mul {a b c d : Nat} : a ∣ b → c ∣ d → a * c ∣ b * d
   | ⟨e, he⟩, ⟨f, hf⟩ =>

src/Init/Data/Nat/Gcd.lean

@@ -106,11 +106,11 @@ theorem gcd_comm (m n : Nat) : gcd m n = gcd n m :=
     (dvd_gcd (gcd_dvd_right n m) (gcd_dvd_left n m))
 instance : Std.Commutative gcd := ⟨gcd_comm⟩
 
-theorem gcd_eq_left_iff_dvd : m ∣ n ↔ gcd m n = m :=
-  ⟨fun h => by rw [gcd_rec, mod_eq_zero_of_dvd h, gcd_zero_left],
-   fun h => h ▸ gcd_dvd_right m n⟩
+theorem gcd_eq_left_iff_dvd : gcd m n = m ↔ m ∣ n :=
+  ⟨fun h => h ▸ gcd_dvd_right m n,
+   fun h => by rw [gcd_rec, mod_eq_zero_of_dvd h, gcd_zero_left]⟩
 
-theorem gcd_eq_right_iff_dvd : m ∣ n ↔ gcd n m = m := by
+theorem gcd_eq_right_iff_dvd : gcd n m = m ↔ m ∣ n := by
   rw [gcd_comm]; exact gcd_eq_left_iff_dvd
 
 theorem gcd_assoc (m n k : Nat) : gcd (gcd m n) k = gcd m (gcd n k) :=
@@ -174,12 +174,20 @@ theorem gcd_dvd_gcd_of_dvd_left {m k : Nat} (n : Nat) (H : m ∣ k) : gcd m n
 theorem gcd_dvd_gcd_of_dvd_right {m k : Nat} (n : Nat) (H : m ∣ k) : gcd n m ∣ gcd n k :=
   dvd_gcd (gcd_dvd_left n m) (Nat.dvd_trans (gcd_dvd_right n m) H)
 
-theorem gcd_dvd_gcd_mul_left (m n k : Nat) : gcd m n ∣ gcd (k * m) n :=
+theorem gcd_dvd_gcd_mul_left_left (m n k : Nat) : gcd m n ∣ gcd (k * m) n :=
   gcd_dvd_gcd_of_dvd_left _ (Nat.dvd_mul_left _ _)
 
-theorem gcd_dvd_gcd_mul_right (m n k : Nat) : gcd m n ∣ gcd (m * k) n :=
+@[deprecated gcd_dvd_gcd_mul_left_left (since := "2025-04-01")]
+theorem gcd_dvd_gcd_mul_left (m n k : Nat) : gcd m n ∣ gcd (k * m) n :=
+  gcd_dvd_gcd_mul_left_left m n k
+
+theorem gcd_dvd_gcd_mul_right_left (m n k : Nat) : gcd m n ∣ gcd (m * k) n :=
   gcd_dvd_gcd_of_dvd_left _ (Nat.dvd_mul_right _ _)
 
+@[deprecated gcd_dvd_gcd_mul_right_left (since := "2025-04-01")]
+theorem gcd_dvd_gcd_mul_right (m n k : Nat) : gcd m n ∣ gcd (m * k) n :=
+  gcd_dvd_gcd_mul_right_left m n k
+
 theorem gcd_dvd_gcd_mul_left_right (m n k : Nat) : gcd m n ∣ gcd m (k * n) :=
   gcd_dvd_gcd_of_dvd_right _ (Nat.dvd_mul_left _ _)
 
@@ -192,6 +200,16 @@ theorem gcd_eq_left {m n : Nat} (H : m ∣ n) : gcd m n = m :=
 theorem gcd_eq_right {m n : Nat} (H : n ∣ m) : gcd m n = n := by
   rw [gcd_comm, gcd_eq_left H]
 
+theorem gcd_right_eq_iff {m n n' : Nat} : gcd m n = gcd m n' ↔ ∀ k, k ∣ m → (k ∣ n ↔ k ∣ n') := by
+  refine ⟨fun h k hkm => ⟨fun hkn => ?_, fun hkn' => ?_⟩, fun h => Nat.dvd_antisymm ?_ ?_⟩
+  · exact Nat.dvd_trans (h ▸ dvd_gcd hkm hkn) (Nat.gcd_dvd_right m n')
+  · exact Nat.dvd_trans (h ▸ dvd_gcd hkm hkn') (Nat.gcd_dvd_right m n)
+  · exact dvd_gcd_iff.2 ⟨gcd_dvd_left _ _, (h _ (gcd_dvd_left _ _)).1 (gcd_dvd_right _ _)⟩
+  · exact dvd_gcd_iff.2 ⟨gcd_dvd_left _ _, (h _ (gcd_dvd_left _ _)).2 (gcd_dvd_right _ _)⟩
+
+theorem gcd_left_eq_iff {m m' n : Nat} : gcd m n = gcd m' n ↔ ∀ k, k ∣ n → (k ∣ m ↔ k ∣ m') := by
+  rw [gcd_comm m n, gcd_comm m' n, gcd_right_eq_iff]
+
 @[simp] theorem gcd_mul_left_left (m n : Nat) : gcd (m * n) n = n :=
   Nat.dvd_antisymm (gcd_dvd_right _ _) (dvd_gcd (Nat.dvd_mul_left _ _) (Nat.dvd_refl _))
 
@@ -216,10 +234,123 @@ theorem gcd_eq_right {m n : Nat} (H : n ∣ m) : gcd m n = n := by
 @[simp] theorem gcd_gcd_self_left_left (m n : Nat) : gcd (gcd m n) m = gcd m n := by
   rw [gcd_comm m n, gcd_gcd_self_left_right]
 
-theorem gcd_add_mul_self (m n k : Nat) : gcd m (n + k * m) = gcd m n := by
+@[simp] theorem gcd_add_mul_right_right (m n k : Nat) : gcd m (n + k * m) = gcd m n := by
   simp [gcd_rec m (n + k * m), gcd_rec m n]
 
-theorem gcd_eq_zero_iff {i j : Nat} : gcd i j = 0 ↔ i = 0 ∧ j = 0 :=
+@[deprecated gcd_add_mul_right_right (since := "2025-03-31")]
+theorem gcd_add_mul_self (m n k : Nat) : gcd m (n + k * m) = gcd m n :=
+  gcd_add_mul_right_right _ _ _
+
+@[simp] theorem gcd_add_mul_left_right (m n k : Nat) : gcd m (n + m * k) = gcd m n := by
+  rw [Nat.mul_comm, gcd_add_mul_right_right]
+
+@[simp] theorem gcd_mul_right_add_right (m n k : Nat) : gcd m (k * m + n) = gcd m n := by
+  rw [Nat.add_comm, gcd_add_mul_right_right]
+
+@[simp] theorem gcd_mul_left_add_right (m n k : Nat) : gcd m (m * k + n) = gcd m n := by
+  rw [Nat.add_comm, gcd_add_mul_left_right]
+
+@[simp] theorem gcd_add_mul_right_left (m n k : Nat) : gcd (n + k * m) m = gcd n m := by
+  rw [gcd_comm, gcd_add_mul_right_right, gcd_comm]
+
+@[simp] theorem gcd_add_mul_left_left (m n k : Nat) : gcd (n + m * k) m = gcd n m := by
+  rw [Nat.mul_comm, gcd_add_mul_right_left]
+
+@[simp] theorem gcd_mul_right_add_left (m n k : Nat) : gcd (k * m + n) m = gcd n m := by
+  rw [Nat.add_comm, gcd_add_mul_right_left]
+
+@[simp] theorem gcd_mul_left_add_left (m n k : Nat) : gcd (m * k + n) m = gcd n m := by
+  rw [Nat.add_comm, gcd_add_mul_left_left]
+
+@[simp] theorem gcd_add_self_right (m n : Nat) : gcd m (n + m) = gcd m n := by
+  simpa using gcd_add_mul_right_right _ _ 1
+
+@[simp] theorem gcd_self_add_right (m n : Nat) : gcd m (m + n) = gcd m n := by
+  simpa using gcd_mul_right_add_right _ _ 1
+
+@[simp] theorem gcd_add_self_left (m n : Nat) : gcd (n + m) m = gcd n m := by
+  simpa using gcd_add_mul_right_left _ _ 1
+
+@[simp] theorem gcd_self_add_left (m n : Nat) : gcd (m + n) m = gcd n m := by
+  simpa using gcd_mul_right_add_left _ _ 1
+
+@[simp] theorem gcd_add_left_left_of_dvd {m k : Nat} (n : Nat) :
+    m ∣ k → gcd (k + n) m = gcd n m := by
+  rintro ⟨l, rfl⟩; exact gcd_mul_left_add_left m n l
+
+@[simp] theorem gcd_add_right_left_of_dvd {m k : Nat} (n : Nat) :
+    m ∣ k → gcd (n + k) m = gcd n m := by
+  rintro ⟨l, rfl⟩; exact gcd_add_mul_left_left m n l
+
+@[simp] theorem gcd_add_left_right_of_dvd {n k : Nat} (m : Nat) :
+    n ∣ k → gcd n (k + m) = gcd n m := by
+  rintro ⟨l, rfl⟩; exact gcd_mul_left_add_right n m l
+
+@[simp] theorem gcd_add_right_right_of_dvd {n k : Nat} (m : Nat) :
+    n ∣ k → gcd n (m + k) = gcd n m := by
+  rintro ⟨l, rfl⟩; exact gcd_add_mul_left_right n m l
+
+@[simp] theorem gcd_sub_mul_right_right {m n k : Nat} (h : k * m ≤ n) :
+    gcd m (n - k * m) = gcd m n := by
+  rw [← gcd_add_mul_right_right m (n - k * m) k, Nat.sub_add_cancel h]
+
+@[simp] theorem gcd_sub_mul_left_right {m n k : Nat} (h : m * k ≤ n) :
+    gcd m (n - m * k) = gcd m n := by
+  rw [← gcd_add_mul_left_right m (n - m * k) k, Nat.sub_add_cancel h]
+
+@[simp] theorem gcd_mul_right_sub_right {m n k : Nat} (h : n ≤ k * m) :
+    gcd m (k * m - n) = gcd m n :=
+  gcd_right_eq_iff.2 fun _ hl => dvd_sub_iff_right h (Nat.dvd_mul_left_of_dvd hl _)
+
+@[simp] theorem gcd_mul_left_sub_right {m n k : Nat} (h : n ≤ m * k) :
+    gcd m (m * k - n) = gcd m n := by
+  rw [Nat.mul_comm, gcd_mul_right_sub_right (Nat.mul_comm _ _ ▸ h)]
+
+@[simp] theorem gcd_sub_mul_right_left {m n k : Nat} (h : k * m ≤ n) :
+    gcd (n - k * m) m = gcd n m := by
+  rw [gcd_comm, gcd_sub_mul_right_right h, gcd_comm]
+
+@[simp] theorem gcd_sub_mul_left_left {m n k : Nat} (h : m * k ≤ n) :
+    gcd (n - m * k) m = gcd n m := by
+  rw [Nat.mul_comm, gcd_sub_mul_right_left (Nat.mul_comm _ _ ▸ h)]
+
+@[simp] theorem gcd_mul_right_sub_left {m n k : Nat} (h : n ≤ k * m) :
+    gcd (k * m - n) m = gcd n m := by
+  rw [gcd_comm, gcd_mul_right_sub_right h, gcd_comm]
+
+@[simp] theorem gcd_mul_left_sub_left {m n k : Nat} (h : n ≤ m * k) :
+    gcd (m * k - n) m = gcd n m := by
+  rw [Nat.mul_comm, gcd_mul_right_sub_left (Nat.mul_comm _ _ ▸ h)]
+
+@[simp] theorem gcd_sub_self_right {m n : Nat} (h : m ≤ n) : gcd m (n - m) = gcd m n := by
+  simpa using gcd_sub_mul_right_right (k := 1) (by simpa using h)
+
+@[simp] theorem gcd_self_sub_right {m n : Nat} (h : n ≤ m) : gcd m (m - n) = gcd m n := by
+  simpa using gcd_mul_right_sub_right (k := 1) (by simpa using h)
+
+@[simp] theorem gcd_sub_self_left {m n : Nat} (h : m ≤ n) : gcd (n - m) m = gcd n m := by
+  simpa using gcd_sub_mul_right_left (k := 1) (by simpa using h)
+
+@[simp] theorem gcd_self_sub_left {m n : Nat} (h : n ≤ m) : gcd (m - n) m = gcd n m := by
+  simpa using gcd_mul_right_sub_left (k := 1) (by simpa using h)
+
+@[simp] theorem gcd_sub_left_left_of_dvd {n k : Nat} (m : Nat) (h : n ≤ k) :
+    m ∣ k → gcd (k - n) m = gcd n m := by
+  rintro ⟨l, rfl⟩; exact gcd_mul_left_sub_left h
+
+@[simp] theorem gcd_sub_right_left_of_dvd {n k : Nat} (m : Nat) (h : k ≤ n) :
+    m ∣ k → gcd (n - k) m = gcd n m := by
+  rintro ⟨l, rfl⟩; exact gcd_sub_mul_left_left h
+
+@[simp] theorem gcd_sub_left_right_of_dvd {m k : Nat} (n : Nat) (h : m ≤ k) :
+    n ∣ k → gcd n (k - m) = gcd n m := by
+  rintro ⟨l, rfl⟩; exact gcd_mul_left_sub_right h
+
+@[simp] theorem gcd_sub_right_right_of_dvd {m k : Nat} (n : Nat) (h : k ≤ m) :
+    n ∣ k → gcd n (m - k) = gcd n m := by
+  rintro ⟨l, rfl⟩; exact gcd_sub_mul_left_right h
+
+@[simp] theorem gcd_eq_zero_iff {i j : Nat} : gcd i j = 0 ↔ i = 0 ∧ j = 0 :=
   ⟨fun h => ⟨eq_zero_of_gcd_eq_zero_left h, eq_zero_of_gcd_eq_zero_right h⟩,
    fun h => by simp [h]⟩
 
@@ -237,7 +368,7 @@ theorem gcd_eq_iff {a b : Nat} :
     · exact Nat.dvd_gcd ha hb
 
 /-- Represent a divisor of `m * n` as a product of a divisor of `m` and a divisor of `n`. -/
-def prod_dvd_and_dvd_of_dvd_prod {k m n : Nat} (H : k ∣ m * n) :
+def dvdProdDvdOfDvdProd {k m n : Nat} (h : k ∣ m * n) :
     {d : {m' // m' ∣ m} × {n' // n' ∣ n} // k = d.1.val * d.2.val} :=
   if h0 : gcd k m = 0 then
     ⟨⟨⟨0, eq_zero_of_gcd_eq_zero_right h0 ▸ Nat.dvd_refl 0⟩,
@@ -248,15 +379,90 @@ def prod_dvd_and_dvd_of_dvd_prod {k m n : Nat} (H : k ∣ m * n) :
     refine ⟨⟨⟨gcd k m, gcd_dvd_right k m⟩, ⟨k / gcd k m, ?_⟩⟩, hd.symm⟩
     apply Nat.dvd_of_mul_dvd_mul_left (Nat.pos_of_ne_zero h0)
     rw [hd, ← gcd_mul_right]
-    exact Nat.dvd_gcd (Nat.dvd_mul_right _ _) H
+    exact Nat.dvd_gcd (Nat.dvd_mul_right _ _) h
+
+@[inherit_doc dvdProdDvdOfDvdProd, deprecated dvdProdDvdOfDvdProd (since := "2025-04-01")]
+def prod_dvd_and_dvd_of_dvd_prod {k m n : Nat} (H : k ∣ m * n) :
+    {d : {m' // m' ∣ m} × {n' // n' ∣ n} // k = d.1.val * d.2.val} :=
+  dvdProdDvdOfDvdProd H
+
+protected theorem dvd_mul {k m n : Nat} : k ∣ m * n ↔ ∃ k₁ k₂, k₁ ∣ m ∧ k₂ ∣ n ∧ k₁ * k₂ = k := by
+  refine ⟨fun h => ?_, ?_⟩
+  · obtain ⟨⟨⟨k₁, hk₁⟩, ⟨k₂, hk₂⟩⟩, rfl⟩ := dvdProdDvdOfDvdProd h
+    exact ⟨k₁, k₂, hk₁, hk₂, rfl⟩
+  · rintro ⟨k₁, k₂, hk₁, hk₂, rfl⟩
+    exact Nat.mul_dvd_mul hk₁ hk₂
 
 theorem gcd_mul_dvd_mul_gcd (k m n : Nat) : gcd k (m * n) ∣ gcd k m * gcd k n := by
   let ⟨⟨⟨m', hm'⟩, ⟨n', hn'⟩⟩, (h : gcd k (m * n) = m' * n')⟩ :=
-    prod_dvd_and_dvd_of_dvd_prod <| gcd_dvd_right k (m * n)
+    dvdProdDvdOfDvdProd <| gcd_dvd_right k (m * n)
   rw [h]
   have h' : m' * n' ∣ k := h ▸ gcd_dvd_left ..
   exact Nat.mul_dvd_mul
     (dvd_gcd (Nat.dvd_trans (Nat.dvd_mul_right m' n') h') hm')
     (dvd_gcd (Nat.dvd_trans (Nat.dvd_mul_left n' m') h') hn')
 
+theorem dvd_gcd_mul_iff_dvd_mul {k n m : Nat} : k ∣ gcd k n * m ↔ k ∣ n * m := by
+  refine ⟨(Nat.dvd_trans · <| Nat.mul_dvd_mul_right (k.gcd_dvd_right n) m), fun ⟨y, hy⟩ ↦ ?_⟩
+  rw [← gcd_mul_right, hy, gcd_mul_left]
+  exact Nat.dvd_mul_right k (gcd m y)
+
+theorem dvd_mul_gcd_iff_dvd_mul {k n m : Nat} : k ∣ n * gcd k m ↔ k ∣ n * m := by
+  rw [Nat.mul_comm, dvd_gcd_mul_iff_dvd_mul, Nat.mul_comm]
+
+theorem dvd_gcd_mul_gcd_iff_dvd_mul {k n m : Nat} : k ∣ gcd k n * gcd k m ↔ k ∣ n * m := by
+  rw [dvd_gcd_mul_iff_dvd_mul, dvd_mul_gcd_iff_dvd_mul]
+
+theorem gcd_eq_one_iff {m n : Nat} : gcd m n = 1 ↔ ∀ c, c ∣ m → c ∣ n → c = 1 := by
+  simp [gcd_eq_iff]
+
+theorem gcd_mul_right_right_of_gcd_eq_one {n m k : Nat} : gcd n m = 1 → gcd n (m * k) = gcd n k := by
+  rw [gcd_right_eq_iff, gcd_eq_one_iff]
+  refine fun h l hl₁ => ⟨?_, fun a => Nat.dvd_mul_left_of_dvd a m⟩
+  rw [Nat.dvd_mul]
+  rintro ⟨k₁, k₂, hk₁, hk₂, rfl⟩
+  obtain rfl : k₁ = 1 := h _ (Nat.dvd_trans (Nat.dvd_mul_right k₁ k₂) hl₁) hk₁
+  simpa
+
+theorem gcd_mul_left_right_of_gcd_eq_one {n m k : Nat} (h : gcd n m = 1) :
+    gcd n (k * m) = gcd n k := by
+  rw [Nat.mul_comm, gcd_mul_right_right_of_gcd_eq_one h]
+
+theorem gcd_mul_right_left_of_gcd_eq_one {n m k : Nat} (h : gcd n m = 1) :
+    gcd (n * k) m = gcd k m := by
+  rw [gcd_comm, gcd_mul_right_right_of_gcd_eq_one (gcd_comm _ _ ▸ h), gcd_comm]
+
+theorem gcd_mul_left_left_of_gcd_eq_one {n m k : Nat} (h : gcd n m = 1) :
+    gcd (k * n) m = gcd k m := by
+  rw [Nat.mul_comm, gcd_mul_right_left_of_gcd_eq_one h]
+
+theorem gcd_pow_left_of_gcd_eq_one {k n m : Nat} (h : gcd n m = 1) : gcd (n ^ k) m = 1 := by
+  induction k with
+  | zero => simp [Nat.pow_zero]
+  | succ k ih => rw [Nat.pow_succ, gcd_mul_left_left_of_gcd_eq_one h, ih]
+
+theorem gcd_pow_right_of_gcd_eq_one {k n m : Nat} (h : gcd n m = 1) : gcd n (m ^ k) = 1 := by
+  rw [gcd_comm, gcd_pow_left_of_gcd_eq_one (gcd_comm _ _ ▸ h)]
+
+theorem pow_gcd_pow_of_gcd_eq_one {k l n m : Nat} (h : gcd n m = 1) : gcd (n ^ k) (m ^ l) = 1 :=
+  gcd_pow_left_of_gcd_eq_one (gcd_pow_right_of_gcd_eq_one h)
+
+theorem gcd_div_gcd_div_gcd_of_pos_left {n m : Nat} (h : 0 < n) :
+    gcd (n / gcd n m) (m / gcd n m) = 1 := by
+  rw [gcd_div (gcd_dvd_left _ _) (gcd_dvd_right _ _), Nat.div_self (gcd_pos_of_pos_left _ h)]
+
+theorem gcd_div_gcd_div_gcd_of_pos_right {n m : Nat} (h : 0 < m) :
+    gcd (n / gcd n m) (m / gcd n m) = 1 := by
+  rw [gcd_div (gcd_dvd_left _ _) (gcd_dvd_right _ _), Nat.div_self (gcd_pos_of_pos_right _ h)]
+
+theorem pow_gcd_pow {k n m : Nat} : gcd (n ^ k) (m ^ k) = (gcd n m) ^ k := by
+  refine (Nat.eq_zero_or_pos n).elim (by rintro rfl; cases k <;> simp [Nat.pow_zero]) (fun hn => ?_)
+  conv => lhs; rw [← Nat.div_mul_cancel (gcd_dvd_left n m)]
+  conv => lhs; arg 2; rw [← Nat.div_mul_cancel (gcd_dvd_right n m)]
+  rw [Nat.mul_pow, Nat.mul_pow, gcd_mul_right, pow_gcd_pow_of_gcd_eq_one, Nat.one_mul]
+  exact gcd_div_gcd_div_gcd_of_pos_left hn
+
+theorem pow_dvd_pow_iff {a b n : Nat} (h : n ≠ 0) : a ^ n ∣ b ^ n ↔ a ∣ b := by
+  rw [← gcd_eq_left_iff_dvd, ← gcd_eq_left_iff_dvd, pow_gcd_pow, Nat.pow_left_inj h]
+
 end Nat

src/Init/Data/Nat/Lemmas.lean

@@ -626,9 +626,6 @@ protected theorem zero_pow {n : Nat} (H : 0 < n) : 0 ^ n = 0 := by
   | zero => rfl
   | succ _ ih => rw [Nat.pow_succ, Nat.mul_one, ih]
 
-@[simp] protected theorem pow_one (a : Nat) : a ^ 1 = a := by
-  rw [Nat.pow_succ, Nat.pow_zero, Nat.one_mul]
-
 protected theorem pow_two (a : Nat) : a ^ 2 = a * a := by rw [Nat.pow_succ, Nat.pow_one]
 
 protected theorem pow_add (a m n : Nat) : a ^ (m + n) = a ^ m * a ^ n := by
@@ -650,11 +647,6 @@ protected theorem pow_mul' (a m n : Nat) : a ^ (m * n) = (a ^ n) ^ m := by
 protected theorem pow_right_comm (a m n : Nat) : (a ^ m) ^ n = (a ^ n) ^ m := by
   rw [← Nat.pow_mul, Nat.pow_mul']
 
-protected theorem mul_pow (a b n : Nat) : (a * b) ^ n = a ^ n * b ^ n := by
-  induction n with
-  | zero => rw [Nat.pow_zero, Nat.pow_zero, Nat.pow_zero, Nat.mul_one]
-  | succ _ ih => rw [Nat.pow_succ, Nat.pow_succ, Nat.pow_succ, Nat.mul_mul_mul_comm, ih]
-
 protected theorem one_lt_two_pow (h : n ≠ 0) : 1 < 2 ^ n :=
   match n, h with
   | n+1, _ => by

src/Init/Data/SInt/Lemmas.lean

@@ -2393,6 +2393,17 @@ instance : Std.LawfulIdentity (α := ISize) (· + ·) 0 where
 @[simp] protected theorem Int64.sub_self (a : Int64) : a - a = 0 := Int64.toBitVec_inj.1 (BitVec.sub_self _)
 @[simp] protected theorem ISize.sub_self (a : ISize) : a - a = 0 := ISize.toBitVec_inj.1 (BitVec.sub_self _)
 
+protected theorem Int8.add_left_neg (a : Int8) : -a + a = 0 := Int8.toBitVec_inj.1 (BitVec.add_left_neg _)
+protected theorem Int8.add_right_neg (a : Int8) : a + -a = 0 := Int8.toBitVec_inj.1 (BitVec.add_right_neg _)
+protected theorem Int16.add_left_neg (a : Int16) : -a + a = 0 := Int16.toBitVec_inj.1 (BitVec.add_left_neg _)
+protected theorem Int16.add_right_neg (a : Int16) : a + -a = 0 := Int16.toBitVec_inj.1 (BitVec.add_right_neg _)
+protected theorem Int32.add_left_neg (a : Int32) : -a + a = 0 := Int32.toBitVec_inj.1 (BitVec.add_left_neg _)
+protected theorem Int32.add_right_neg (a : Int32) : a + -a = 0 := Int32.toBitVec_inj.1 (BitVec.add_right_neg _)
+protected theorem Int64.add_left_neg (a : Int64) : -a + a = 0 := Int64.toBitVec_inj.1 (BitVec.add_left_neg _)
+protected theorem Int64.add_right_neg (a : Int64) : a + -a = 0 := Int64.toBitVec_inj.1 (BitVec.add_right_neg _)
+protected theorem ISize.add_left_neg (a : ISize) : -a + a = 0 := ISize.toBitVec_inj.1 (BitVec.add_left_neg _)
+protected theorem ISize.add_right_neg (a : ISize) : a + -a = 0 := ISize.toBitVec_inj.1 (BitVec.add_right_neg _)
+
 @[simp] protected theorem Int8.sub_add_cancel (a b : Int8) : a - b + b = a :=
   Int8.toBitVec_inj.1 (BitVec.sub_add_cancel _ _)
 @[simp] protected theorem Int16.sub_add_cancel (a b : Int16) : a - b + b = a :=

src/Init/Data/UInt/Lemmas.lean

@@ -2376,6 +2376,17 @@ instance : Std.LawfulIdentity (α := USize) (· + ·) 0 where
 @[simp] protected theorem UInt64.sub_self (a : UInt64) : a - a = 0 := UInt64.toBitVec_inj.1 (BitVec.sub_self _)
 @[simp] protected theorem USize.sub_self (a : USize) : a - a = 0 := USize.toBitVec_inj.1 (BitVec.sub_self _)
 
+protected theorem UInt8.add_left_neg (a : UInt8) : -a + a = 0 := UInt8.toBitVec_inj.1 (BitVec.add_left_neg _)
+protected theorem UInt8.add_right_neg (a : UInt8) : a + -a = 0 := UInt8.toBitVec_inj.1 (BitVec.add_right_neg _)
+protected theorem UInt16.add_left_neg (a : UInt16) : -a + a = 0 := UInt16.toBitVec_inj.1 (BitVec.add_left_neg _)
+protected theorem UInt16.add_right_neg (a : UInt16) : a + -a = 0 := UInt16.toBitVec_inj.1 (BitVec.add_right_neg _)
+protected theorem UInt32.add_left_neg (a : UInt32) : -a + a = 0 := UInt32.toBitVec_inj.1 (BitVec.add_left_neg _)
+protected theorem UInt32.add_right_neg (a : UInt32) : a + -a = 0 := UInt32.toBitVec_inj.1 (BitVec.add_right_neg _)
+protected theorem UInt64.add_left_neg (a : UInt64) : -a + a = 0 := UInt64.toBitVec_inj.1 (BitVec.add_left_neg _)
+protected theorem UInt64.add_right_neg (a : UInt64) : a + -a = 0 := UInt64.toBitVec_inj.1 (BitVec.add_right_neg _)
+protected theorem USize.add_left_neg (a : USize) : -a + a = 0 := USize.toBitVec_inj.1 (BitVec.add_left_neg _)
+protected theorem USize.add_right_neg (a : USize) : a + -a = 0 := USize.toBitVec_inj.1 (BitVec.add_right_neg _)
+
 @[simp] protected theorem UInt8.neg_zero : -(0 : UInt8) = 0 := rfl
 @[simp] protected theorem UInt16.neg_zero : -(0 : UInt16) = 0 := rfl
 @[simp] protected theorem UInt32.neg_zero : -(0 : UInt32) = 0 := rfl

src/Init/Data/Vector/Lemmas.lean

@@ -2783,7 +2783,7 @@ theorem any_eq_not_all_not {xs : Vector α n} {p : α → Bool} : xs.any p = !xs
   simp
 
 @[simp] theorem all_filter {xs : Vector α n} {p q : α → Bool} :
-    (xs.filter p).all q = xs.all fun a => p a → q a := by
+    (xs.filter p).all q = xs.all fun a => !(p a) || q a := by
   rcases xs with ⟨xs, rfl⟩
   simp
 

src/Init/Data/Zero.lean

@@ -15,3 +15,13 @@ instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) w
 
 instance (priority := 200) Zero.ofOfNat0 {α} [OfNat α (nat_lit 0)] : Zero α where
   zero := 0
+
+/-!
+Instances converting between `One α` and `OfNat α (nat_lit 1)`.
+-/
+
+instance (priority := 300) One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
+  ofNat := ‹One α›.1
+
+instance (priority := 200) One.ofOfNat1 {α} [OfNat α (nat_lit 1)] : One α where
+  one := 1

src/Init/Grind.lean

@@ -12,3 +12,4 @@ import Init.Grind.Propagator
 import Init.Grind.Util
 import Init.Grind.Offset
 import Init.Grind.PP
+import Init.Grind.CommRing

src/Init/Grind/CommRing.lean

@@ -0,0 +1,11 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Grind.CommRing.Basic
+import Init.Grind.CommRing.Int
+import Init.Grind.CommRing.UInt
+import Init.Grind.CommRing.SInt
+import Init.Grind.CommRing.BitVec

src/Init/Grind/CommRing/Basic.lean

@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.Zero
+
+/-!
+# A monolithic commutative ring typeclass for internal use in `grind`.
+-/
+
+namespace Lean.Grind
+
+class CommRing (α : Type u) extends Add α, Zero α, Mul α, One α, Neg α where
+  add_assoc : ∀ a b c : α, a + b + c = a + (b + c)
+  add_comm : ∀ a b : α, a + b = b + a
+  add_zero : ∀ a : α, a + 0 = a
+  neg_add_cancel : ∀ a : α, -a + a = 0
+  mul_assoc : ∀ a b c : α, a * b * c = a * (b * c)
+  mul_comm : ∀ a b : α, a * b = b * a
+  mul_one : ∀ a : α, a * 1 = a
+  left_distrib : ∀ a b c : α, a * (b + c) = a * b + a * c
+  zero_mul : ∀ a : α, 0 * a = 0
+
+namespace CommRing
+
+variable {α : Type u} [CommRing α]
+
+theorem zero_add (a : α) : 0 + a = a := by
+  rw [add_comm, add_zero]
+
+theorem add_neg_cancel (a : α) : a + -a = 0 := by
+  rw [add_comm, neg_add_cancel]
+
+theorem one_mul (a : α) : 1 * a = a := by
+  rw [mul_comm, mul_one]
+
+theorem right_distrib (a b c : α) : (a + b) * c = a * c + b * c := by
+  rw [mul_comm, left_distrib, mul_comm c, mul_comm c]
+
+theorem mul_zero (a : α) : a * 0 = 0 := by
+  rw [mul_comm, zero_mul]
+
+end CommRing
+
+end Lean.Grind

src/Init/Grind/CommRing/BitVec.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Grind.CommRing.Basic
+import Init.Data.BitVec.Lemmas
+
+namespace Lean.Grind
+
+instance : CommRing (BitVec w) where
+  add_assoc := BitVec.add_assoc
+  add_comm := BitVec.add_comm
+  add_zero := BitVec.add_zero
+  neg_add_cancel := BitVec.add_left_neg
+  mul_assoc := BitVec.mul_assoc
+  mul_comm := BitVec.mul_comm
+  mul_one := BitVec.mul_one
+  left_distrib _ _ _ := BitVec.mul_add
+  zero_mul _ := BitVec.zero_mul
+
+end Lean.Grind

src/Init/Grind/CommRing/Int.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Grind.CommRing.Basic
+import Init.Data.Int.Lemmas
+
+namespace Lean.Grind
+
+instance : CommRing Int where
+  add_assoc := Int.add_assoc
+  add_comm := Int.add_comm
+  add_zero := Int.add_zero
+  neg_add_cancel := Int.add_left_neg
+  mul_assoc := Int.mul_assoc
+  mul_comm := Int.mul_comm
+  mul_one := Int.mul_one
+  left_distrib := Int.mul_add
+  zero_mul := Int.zero_mul
+
+end Lean.Grind

src/Init/Grind/CommRing/SInt.lean

@@ -0,0 +1,67 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Grind.CommRing.Basic
+import Init.Data.SInt.Lemmas
+
+namespace Lean.Grind
+
+instance : CommRing Int8 where
+  add_assoc := Int8.add_assoc
+  add_comm := Int8.add_comm
+  add_zero := Int8.add_zero
+  neg_add_cancel := Int8.add_left_neg
+  mul_assoc := Int8.mul_assoc
+  mul_comm := Int8.mul_comm
+  mul_one := Int8.mul_one
+  left_distrib _ _ _ := Int8.mul_add
+  zero_mul _ := Int8.zero_mul
+
+instance : CommRing Int16 where
+  add_assoc := Int16.add_assoc
+  add_comm := Int16.add_comm
+  add_zero := Int16.add_zero
+  neg_add_cancel := Int16.add_left_neg
+  mul_assoc := Int16.mul_assoc
+  mul_comm := Int16.mul_comm
+  mul_one := Int16.mul_one
+  left_distrib _ _ _ := Int16.mul_add
+  zero_mul _ := Int16.zero_mul
+
+instance : CommRing Int32 where
+  add_assoc := Int32.add_assoc
+  add_comm := Int32.add_comm
+  add_zero := Int32.add_zero
+  neg_add_cancel := Int32.add_left_neg
+  mul_assoc := Int32.mul_assoc
+  mul_comm := Int32.mul_comm
+  mul_one := Int32.mul_one
+  left_distrib _ _ _ := Int32.mul_add
+  zero_mul _ := Int32.zero_mul
+
+instance : CommRing Int64 where
+  add_assoc := Int64.add_assoc
+  add_comm := Int64.add_comm
+  add_zero := Int64.add_zero
+  neg_add_cancel := Int64.add_left_neg
+  mul_assoc := Int64.mul_assoc
+  mul_comm := Int64.mul_comm
+  mul_one := Int64.mul_one
+  left_distrib _ _ _ := Int64.mul_add
+  zero_mul _ := Int64.zero_mul
+
+instance : CommRing ISize where
+  add_assoc := ISize.add_assoc
+  add_comm := ISize.add_comm
+  add_zero := ISize.add_zero
+  neg_add_cancel := ISize.add_left_neg
+  mul_assoc := ISize.mul_assoc
+  mul_comm := ISize.mul_comm
+  mul_one := ISize.mul_one
+  left_distrib _ _ _ := ISize.mul_add
+  zero_mul _ := ISize.zero_mul
+
+end Lean.Grind

src/Init/Grind/CommRing/UInt.lean

@@ -0,0 +1,67 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Grind.CommRing.Basic
+import Init.Data.UInt.Lemmas
+
+namespace Lean.Grind
+
+instance : CommRing UInt8 where
+  add_assoc := UInt8.add_assoc
+  add_comm := UInt8.add_comm
+  add_zero := UInt8.add_zero
+  neg_add_cancel := UInt8.add_left_neg
+  mul_assoc := UInt8.mul_assoc
+  mul_comm := UInt8.mul_comm
+  mul_one := UInt8.mul_one
+  left_distrib _ _ _ := UInt8.mul_add
+  zero_mul _ := UInt8.zero_mul
+
+instance : CommRing UInt16 where
+  add_assoc := UInt16.add_assoc
+  add_comm := UInt16.add_comm
+  add_zero := UInt16.add_zero
+  neg_add_cancel := UInt16.add_left_neg
+  mul_assoc := UInt16.mul_assoc
+  mul_comm := UInt16.mul_comm
+  mul_one := UInt16.mul_one
+  left_distrib _ _ _ := UInt16.mul_add
+  zero_mul _ := UInt16.zero_mul
+
+instance : CommRing UInt32 where
+  add_assoc := UInt32.add_assoc
+  add_comm := UInt32.add_comm
+  add_zero := UInt32.add_zero
+  neg_add_cancel := UInt32.add_left_neg
+  mul_assoc := UInt32.mul_assoc
+  mul_comm := UInt32.mul_comm
+  mul_one := UInt32.mul_one
+  left_distrib _ _ _ := UInt32.mul_add
+  zero_mul _ := UInt32.zero_mul
+
+instance : CommRing UInt64 where
+  add_assoc := UInt64.add_assoc
+  add_comm := UInt64.add_comm
+  add_zero := UInt64.add_zero
+  neg_add_cancel := UInt64.add_left_neg
+  mul_assoc := UInt64.mul_assoc
+  mul_comm := UInt64.mul_comm
+  mul_one := UInt64.mul_one
+  left_distrib _ _ _ := UInt64.mul_add
+  zero_mul _ := UInt64.zero_mul
+
+instance : CommRing USize where
+  add_assoc := USize.add_assoc
+  add_comm := USize.add_comm
+  add_zero := USize.add_zero
+  neg_add_cancel := USize.add_left_neg
+  mul_assoc := USize.mul_assoc
+  mul_comm := USize.mul_comm
+  mul_one := USize.mul_one
+  left_distrib _ _ _ := USize.mul_add
+  zero_mul _ := USize.zero_mul
+
+end Lean.Grind

src/Init/Grind/Lemmas.lean

@@ -77,6 +77,14 @@ theorem eq_congr' {α : Sort u} {a₁ b₁ a₂ b₂ : α} (h₁ : a₁ = b₂)
 theorem ne_of_ne_of_eq_left {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b ≠ c) : a ≠ c := by simp [*]
 theorem ne_of_ne_of_eq_right {α : Sort u} {a b c : α} (h₁ : a = c) (h₂ : b ≠ c) : b ≠ a := by simp [*]
 
+/-! BEq -/
+
+theorem beq_eq_true_of_eq {α : Type u} {_ : BEq α} {_ : LawfulBEq α} {a b : α} (h : a = b) : (a == b) = true := by
+  simp[*]
+
+theorem beq_eq_false_of_diseq {α : Type u} {_ : BEq α} {_ : LawfulBEq α} {a b : α} (h : ¬ a = b) : (a == b) = false := by
+  simp[*]
+
 /-! Bool.and -/
 
 theorem Bool.and_eq_of_eq_true_left {a b : Bool} (h : a = true) : (a && b) = b := by simp [h]
@@ -105,6 +113,9 @@ theorem Bool.not_eq_of_eq_false {a : Bool} (h : a = false) : (!a) = true := by s
 theorem Bool.eq_false_of_not_eq_true {a : Bool} (h : (!a) = true) : a = false := by simp_all
 theorem Bool.eq_true_of_not_eq_false {a : Bool} (h : (!a) = false) : a = true := by simp_all
 
+theorem Bool.eq_false_of_not_eq_true' {a : Bool} (h : ¬ a = true) : a = false := by simp_all
+theorem Bool.eq_true_of_not_eq_false' {a : Bool} (h : ¬ a = false) : a = true := by simp_all
+
 theorem Bool.false_of_not_eq_self {a : Bool} (h : (!a) = a) : False := by
   by_cases a <;> simp_all
 

src/Init/Grind/Norm.lean

@@ -120,7 +120,7 @@ init_grind_norm
   -- Bool not
   Bool.not_not
   -- beq
-  beq_iff_eq beq_eq_decide_eq
+  beq_iff_eq beq_eq_decide_eq beq_self_eq_true
   -- bne
   bne_iff_ne bne_eq_decide_not_eq
   -- Bool not eq true/false

src/Init/Grind/Util.lean

@@ -78,6 +78,19 @@ def offsetUnexpander : PrettyPrinter.Unexpander := fun stx => do
   | `($_ $lhs:term $rhs:term) => `($lhs + $rhs)
   | _ => throw ()
 
+/-
+Remark: `↑a` is notation for `Nat.cast a`. `Nat.cast` is an abbreviation
+for `NatCast.natCast`. We added it because users wanted to use dot-notation (e.g., `a.cast`).
+`grind` expands all reducible definitions. Thus, a `grind` failure state contains
+many `NatCast.natCast` applications which is too verbose. We add the following
+unexpander to cope with this issue.
+-/
+@[app_unexpander NatCast.natCast]
+def natCastUnexpander : PrettyPrinter.Unexpander := fun stx => do
+  match stx with
+  | `($_ $a:term) => `(↑$a)
+  | _ => throw ()
+
 /--
 A marker to indicate that a proposition has already been normalized and should not
 be processed again.

src/Init/Prelude.lean

@@ -1415,6 +1415,11 @@ class Zero (α : Type u) where
   /-- The zero element of the type. -/
   zero : α
 
+/-- A type with a "one" element. -/
+class One (α : Type u) where
+  /-- The "one" element of the type. -/
+  one : α
+
 /-- The homogeneous version of `HAdd`: `a + b : α` where `a b : α`. -/
 class Add (α : Type u) where
   /-- `a + b` computes the sum of `a` and `b`. See `HAdd`. -/

src/Lean/Compiler/IR/Basic.lean

@@ -180,7 +180,7 @@ structure CtorInfo where
   size : Nat
   usize : Nat
   ssize : Nat
-  deriving Repr
+  deriving Inhabited, Repr
 
 def CtorInfo.beq : CtorInfo → CtorInfo → Bool
   | ⟨n₁, cidx₁, size₁, usize₁, ssize₁⟩, ⟨n₂, cidx₂, size₂, usize₂, ssize₂⟩ =>
@@ -223,6 +223,7 @@ inductive Expr where
   | lit (v : LitVal)
   /-- Return `1 : uint8` Iff `RC(x) > 1` -/
   | isShared (x : VarId)
+  deriving Inhabited
 
 @[export lean_ir_mk_ctor_expr]  def mkCtorExpr (n : Name) (cidx : Nat) (size : Nat) (usize : Nat) (ssize : Nat) (ys : Array Arg) : Expr :=
   Expr.ctor ⟨n, cidx, size, usize, ssize⟩ ys

src/Lean/Compiler/IR/CtorLayout.lean

@@ -15,6 +15,7 @@ inductive CtorFieldInfo where
   | object (i : Nat)
   | usize  (i : Nat)
   | scalar (sz : Nat) (offset : Nat) (type : IRType)
+  deriving Inhabited
 
 namespace CtorFieldInfo
 

src/Lean/Compiler/LCNF/AuxDeclCache.lean

@@ -10,10 +10,7 @@ import Lean.Compiler.LCNF.Internalize
 
 namespace Lean.Compiler.LCNF
 
-abbrev AuxDeclCache := PHashMap Decl Name
-
-builtin_initialize auxDeclCacheExt : EnvExtension AuxDeclCache ←
-  registerEnvExtension (pure {}) (asyncMode := .sync)  -- compilation is non-parallel anyway
+builtin_initialize auxDeclCacheExt : CacheExtension Decl Name ← CacheExtension.register
 
 inductive CacheAuxDeclResult where
   | new
@@ -22,11 +19,11 @@ inductive CacheAuxDeclResult where
 def cacheAuxDecl (decl : Decl) : CompilerM CacheAuxDeclResult := do
   let key := { decl with name := .anonymous }
   let key ← normalizeFVarIds key
-  match auxDeclCacheExt.getState (← getEnv) |>.find? key with
+  match (← auxDeclCacheExt.find? key) with
   | some declName =>
     return .alreadyCached declName
   | none =>
-    modifyEnv fun env => auxDeclCacheExt.modifyState env fun s => s.insert key decl.name
+    auxDeclCacheExt.insert key decl.name
     return .new
 
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/BaseTypes.lean

@@ -14,21 +14,15 @@ State for the environment extension used to save the LCNF base phase type for de
 that do not have code associated with them.
 Example: constructors, inductive types, foreign functions.
 -/
-structure BaseTypeExtState where
-  /-- The LCNF type for the `base` phase. -/
-  base : PHashMap Name Expr := {}
-  deriving Inhabited
-
-builtin_initialize baseTypeExt : EnvExtension BaseTypeExtState ←
-  registerEnvExtension (pure {}) (asyncMode := .sync)  -- compilation is non-parallel anyway
+builtin_initialize baseTypeExt : CacheExtension Name Expr ← CacheExtension.register
 
 def getOtherDeclBaseType (declName : Name) (us : List Level) : CoreM Expr := do
   let info ← getConstInfo declName
-  let type ← match baseTypeExt.getState (← getEnv) |>.base.find? declName with
+  let type ← match (← baseTypeExt.find? declName) with
     | some type => pure type
     | none =>
       let type ← Meta.MetaM.run' <| toLCNFType info.type
-      modifyEnv fun env => baseTypeExt.modifyState env fun s => { s with base := s.base.insert declName type }
+      baseTypeExt.insert declName type
       pure type
   return type.instantiateLevelParamsNoCache info.levelParams us
 

src/Lean/Compiler/LCNF/CompilerM.lean

@@ -483,4 +483,26 @@ def getConfig : CompilerM ConfigOptions :=
 def CompilerM.run (x : CompilerM α) (s : State := {}) (phase : Phase := .base) : CoreM α := do
   x { phase, config := toConfigOptions (← getOptions) } |>.run' s
 
+/-- Environment extension for local caching of key-value pairs, not persisted in .olean files. -/
+structure CacheExtension (α β : Type) [BEq α] [Hashable α] extends EnvExtension (List α × PHashMap α β)
+deriving Inhabited
+
+namespace CacheExtension
+
+def register [BEq α] [Hashable α] [Inhabited β] :
+    IO (CacheExtension α β) :=
+  CacheExtension.mk <$> registerEnvExtension (pure ([], {})) (asyncMode := .sync)  -- compilation is non-parallel anyway
+    (replay? := some fun oldState newState _ s =>
+      let newEntries := newState.1.take (newState.1.length - oldState.1.length)
+      newEntries.foldl (init := s) fun s e =>
+        (e :: s.1, s.2.insert e (newState.2.find! e)))
+
+def insert [BEq α] [Hashable α] [Inhabited β] (ext : CacheExtension α β) (a : α) (b : β) : CoreM Unit := do
+  modifyEnv (ext.modifyState · fun ⟨as, m⟩ => (a :: as, m.insert a b))
+
+def find? [BEq α] [Hashable α] [Inhabited β] (ext : CacheExtension α β) (a : α) : CoreM (Option β) := do
+  return ext.toEnvExtension.getState (← getEnv) |>.2.find? a
+
+end CacheExtension
+
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/ElimDeadBranches.lean

@@ -249,6 +249,7 @@ builtin_initialize functionSummariesExt : SimplePersistentEnvExtension (Name ×
     addEntryFn := fun s ⟨e, n⟩ => s.insert e n
     toArrayFn := fun s => s.toArray.qsort decLt
     asyncMode := .sync  -- compilation is non-parallel anyway
+    replay? := some <| SimplePersistentEnvExtension.replayOfFilter (!·.contains ·.1) (fun s ⟨e, n⟩ => s.insert e n)
   }
 
 /--

src/Lean/Compiler/LCNF/MonoTypes.lean

@@ -111,20 +111,14 @@ State for the environment extension used to save the LCNF mono phase type for de
 that do not have code associated with them.
 Example: constructors, inductive types, foreign functions.
 -/
-structure MonoTypeExtState where
-  /-- The LCNF type for the `mono` phase. -/
-  mono : PHashMap Name Expr := {}
-  deriving Inhabited
-
-builtin_initialize monoTypeExt : EnvExtension MonoTypeExtState ←
-  registerEnvExtension (pure {}) (asyncMode := .sync)  -- compilation is non-parallel anyway
+builtin_initialize monoTypeExt : CacheExtension Name Expr ← CacheExtension.register
 
 def getOtherDeclMonoType (declName : Name) : CoreM Expr := do
-  match monoTypeExt.getState (← getEnv) |>.mono.find? declName with
+  match (← monoTypeExt.find? declName) with
   | some type => return type
   | none =>
     let type ← toMonoType (← getOtherDeclBaseType declName [])
-    modifyEnv fun env => monoTypeExt.modifyState env fun s => { s with mono := s.mono.insert declName type }
+    monoTypeExt.insert declName type
     return type
 
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/Passes.lean

@@ -94,7 +94,6 @@ builtin_initialize passManagerExt : PersistentEnvExtension Name (Name × PassMan
     addImportedFn := fun ns => return ([], ← ImportM.runCoreM <| runImportedDecls ns)
     addEntryFn := fun (installerDeclNames, _) (installerDeclName, managerNew) => (installerDeclName :: installerDeclNames, managerNew)
     exportEntriesFn := fun s => s.1.reverse.toArray
-    asyncMode := .sync
   }
 
 def getPassManager : CoreM PassManager :=

src/Lean/Compiler/LCNF/PhaseExt.lean

@@ -21,22 +21,21 @@ private abbrev findAtSorted? (decls : Array Decl) (declName : Name) : Option Dec
   let tmpDecl := { tmpDecl with name := declName }
   decls.binSearch tmpDecl declLt
 
-abbrev DeclExt := PersistentEnvExtension Decl Decl DeclExtState
+abbrev DeclExt := SimplePersistentEnvExtension Decl DeclExtState
 
 def mkDeclExt (name : Name := by exact decl_name%) : IO DeclExt := do
-  registerPersistentEnvExtension {
+  registerSimplePersistentEnvExtension {
     name            := name
-    mkInitial       := return {}
-    addImportedFn   := fun _ => return {}
+    addImportedFn   := fun _ => {}
     addEntryFn      := fun decls decl => decls.insert decl.name decl
-    exportEntriesFn := fun s =>
-      let decls := s.foldl (init := #[]) fun decls _ decl => decls.push decl
-      sortDecls decls
+    toArrayFn       := (sortDecls ·.toArray)
     asyncMode       := .sync  -- compilation is non-parallel anyway
+    replay?         := some <| SimplePersistentEnvExtension.replayOfFilter
+      (fun s d => !s.contains d.name) (fun decls decl => decls.insert decl.name decl)
   }
 
-builtin_initialize baseExt : PersistentEnvExtension Decl Decl DeclExtState ← mkDeclExt
-builtin_initialize monoExt : PersistentEnvExtension Decl Decl DeclExtState ← mkDeclExt
+builtin_initialize baseExt : DeclExt ← mkDeclExt
+builtin_initialize monoExt : DeclExt ← mkDeclExt
 
 def getDeclCore? (env : Environment) (ext : DeclExt) (declName : Name) : Option Decl :=
   match env.getModuleIdxFor? declName with

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

@@ -397,7 +397,7 @@ structure FolderOleanEntry where
 structure FolderEntry extends FolderOleanEntry where
   folder : Folder
 
-builtin_initialize folderExt : PersistentEnvExtension FolderOleanEntry FolderEntry (List FolderOleanEntry × SMap Name Folder) ←
+builtin_initialize folderExt : PersistentEnvExtension FolderOleanEntry FolderEntry (List FolderEntry × SMap Name Folder) ←
   registerPersistentEnvExtension {
     mkInitial := return ([], builtinFolders)
     addImportedFn := fun entriesArray => do
@@ -408,9 +408,12 @@ builtin_initialize folderExt : PersistentEnvExtension FolderOleanEntry FolderEnt
           let folder ← IO.ofExcept <| getFolderCore ctx.env ctx.opts folderDeclName
           folders := folders.insert declName folder
       return ([], folders.switch)
-    addEntryFn := fun (entries, map) entry => (entry.toFolderOleanEntry :: entries, map.insert entry.declName entry.folder)
-    exportEntriesFn := fun (entries, _) => entries.reverse.toArray
+    addEntryFn := fun (entries, map) entry => (entry :: entries, map.insert entry.declName entry.folder)
+    exportEntriesFn := fun (entries, _) => entries.reverse.toArray.map (·.toFolderOleanEntry)
     asyncMode := .sync
+    replay? := some fun oldState newState _ s =>
+      let newEntries := newState.1.take (newState.1.length - oldState.1.length)
+      (newEntries ++ s.1, newEntries.foldl (init := s.2) fun s e => s.insert e.declName (newState.2.find! e.declName))
   }
 
 def registerFolder (declName : Name) (folderDeclName : Name) : CoreM Unit := do

src/Lean/Compiler/LCNF/SpecInfo.lean

@@ -86,6 +86,8 @@ builtin_initialize specExtension : SimplePersistentEnvExtension SpecEntry SpecSt
     addImportedFn := fun _ => {}
     toArrayFn     := fun s => sortEntries s.toArray
     asyncMode     := .sync
+    replay?       := some <| SimplePersistentEnvExtension.replayOfFilter
+      (!·.specInfo.contains ·.declName) SpecState.addEntry
   }
 
 /--

src/Lean/Compiler/LCNF/Specialize.lean

@@ -33,6 +33,8 @@ builtin_initialize specCacheExt : SimplePersistentEnvExtension CacheEntry Cache
     addEntryFn    := addEntry
     addImportedFn := fun es => (mkStateFromImportedEntries addEntry {} es).switch
     asyncMode     := .sync
+    replay?       := some <| SimplePersistentEnvExtension.replayOfFilter
+      (!·.contains ·.key) addEntry
   }
 
 def cacheSpec (key : Expr) (declName : Name) : CoreM Unit :=

src/Lean/Environment.lean

@@ -1045,10 +1045,10 @@ end ConstantInfo
 
 /--
 Async access mode for environment extensions used in `EnvironmentExtension.get/set/modifyState`.
-Depending on their specific uses, extensions may opt out of the strict `sync` access mode in order
-to avoid blocking parallel elaboration and/or to optimize accesses. The access mode is set at
-environment extension registration time but can be overriden at `EnvironmentExtension.getState` in
-order to weaken it for specific accesses.
+When modified in concurrent contexts, extensions may need to switch to a different mode than the
+default `mainOnly`, which will panic in such cases. The access mode is set at environment extension
+registration time but can be overriden when calling the mentioned functions in order to weaken it
+for specific accesses.
 
 In all modes, the state stored into the `.olean` file for persistent environment extensions is the
 result of `getState` called on the main environment branch at the end of the file, i.e. it
@@ -1056,15 +1056,15 @@ encompasses all modifications for all modes but `local`.
 -/
 inductive EnvExtension.AsyncMode where
   /--
-  Default access mode, writing and reading the extension state to/from the full `checked`
+  Safest access mode, writes and reads the extension state to/from the full `checked`
   environment. This mode ensures the observed state is identical independently of whether or how
   parallel elaboration is used but `getState` will block on all prior environment branches by
   waiting for `checked`. `setState` and `modifyState` do not block.
 
-  While a safe default, any extension that reasonably could be used in parallel elaboration contexts
-  should opt for a weaker mode to avoid blocking unless there is no way to access the correct state
-  without waiting for all prior environment branches, in which case its data management should be
-  restructured if at all possible.
+  While a safe fallback for when `mainOnly` is not sufficient, any extension that reasonably could
+  be used in parallel elaboration contexts should opt for a weaker mode to avoid blocking unless
+  there is no way to access the correct state without waiting for all prior environment branches, in
+  which case its data management should be restructured if at all possible.
   -/
   | sync
   /--
@@ -1077,9 +1077,10 @@ inductive EnvExtension.AsyncMode where
   -/
   | local
   /--
-  Like `local` but panics when trying to modify the state on anything but the main environment
-  branch. For extensions that fulfill this requirement, all modes functionally coincide but this
-  is the safest and most efficient choice in that case, preventing accidental misuse.
+  Default access mode. Like `local` but panics when trying to modify the state on anything but the
+  main environment branch. For extensions that fulfill this requirement, all modes functionally
+  coincide with `local` but this is the safest and most efficient choice in that case, preventing
+  accidental misuse.
 
   This mode is suitable for extensions that are modified only at the command elaboration level
   before any environment forks in the command, and in particular for extensions that are modified

src/Lean/Meta/Tactic/Grind.lean

@@ -72,5 +72,6 @@ builtin_initialize registerTraceClass `grind.debug.matchCond.lambda
 builtin_initialize registerTraceClass `grind.debug.matchCond.proveFalse
 builtin_initialize registerTraceClass `grind.debug.mbtc
 builtin_initialize registerTraceClass `grind.debug.ematch
+builtin_initialize registerTraceClass `grind.debug.proveEq
 
 end Lean

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

@@ -111,35 +111,39 @@ private partial def introNext (goal : Goal) (generation : Nat) : GrindM IntroRes
         let tag ← mvarId.getTag
         let qBase := target.bindingBody!
         let fvarId ← mkFreshFVarId
+        let fvar := mkFVar fvarId
         let r ← preprocessHypothesis p
         let lctx := (← getLCtx).mkLocalDecl fvarId (← mkCleanName target.bindingName! r.expr) r.expr target.bindingInfo!
+        let mut localInsts ← getLocalInstances
+        if let some className ← isClass? r.expr then
+          localInsts := localInsts.push { className, fvar }
         match r.proof? with
         | some he =>
           if target.isArrow then
             let q := qBase
             let u ← getLevel q
-            let mvarNew ← mkFreshExprMVarAt lctx (← getLocalInstances) q .syntheticOpaque tag
+            let mvarNew ← mkFreshExprMVarAt lctx localInsts q .syntheticOpaque tag
             let mvarIdNew := mvarNew.mvarId!
             mvarIdNew.withContext do
-              let h ← mkLambdaFVars #[mkFVar fvarId] mvarNew
+              let h ← mkLambdaFVars #[fvar] mvarNew
               let hNew := mkAppN (mkConst ``Lean.Grind.intro_with_eq [u]) #[p, r.expr, q, he, h]
               mvarId.assign hNew
               return .newHyp fvarId { (← get) with mvarId := mvarIdNew }
           else
             let q := mkLambda target.bindingName! target.bindingInfo! p qBase
-            let q' := qBase.instantiate1 (mkApp4 (mkConst ``Eq.mpr_prop) p r.expr he (mkFVar fvarId))
+            let q' := qBase.instantiate1 (mkApp4 (mkConst ``Eq.mpr_prop) p r.expr he fvar)
             let u ← getLevel q'
-            let mvarNew ← mkFreshExprMVarAt lctx (← getLocalInstances) q' .syntheticOpaque tag
+            let mvarNew ← mkFreshExprMVarAt lctx localInsts q' .syntheticOpaque tag
             let mvarIdNew := mvarNew.mvarId!
             mvarIdNew.withContext do
-              let h ← mkLambdaFVars #[mkFVar fvarId] mvarNew
+              let h ← mkLambdaFVars #[fvar] mvarNew
               let hNew := mkAppN (mkConst ``Lean.Grind.intro_with_eq' [u]) #[p, r.expr, q, he, h]
               mvarId.assign hNew
               return .newHyp fvarId { (← get) with mvarId := mvarIdNew }
         | none =>
           -- `p` and `p'` are definitionally equal
           let q := if target.isArrow then qBase else qBase.instantiate1 (mkFVar fvarId)
-          let mvarNew ← mkFreshExprMVarAt lctx (← getLocalInstances) q .syntheticOpaque tag
+          let mvarNew ← mkFreshExprMVarAt lctx localInsts q .syntheticOpaque tag
           let mvarIdNew := mvarNew.mvarId!
           mvarIdNew.withContext do
             let h ← mkLambdaFVars #[mkFVar fvarId] mvarNew

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

@@ -119,15 +119,25 @@ builtin_grind_propagator propagateNotDown ↓Not := fun e => do
   else if (← isEqv e a) then
     closeGoal <| mkApp2 (mkConst ``Grind.false_of_not_eq_self) a (← mkEqProof e a)
 
+def propagateBoolDiseq (a : Expr) : GoalM Unit := do
+  if let some h ← mkDiseqProof? a (← getBoolFalseExpr) then
+    pushEqBoolTrue a <| mkApp2 (mkConst ``Grind.Bool.eq_true_of_not_eq_false') a h
+  if let some h ← mkDiseqProof? a (← getBoolTrueExpr) then
+    pushEqBoolFalse a <| mkApp2 (mkConst ``Grind.Bool.eq_false_of_not_eq_true') a h
+
 /-- Propagates `Eq` upwards -/
 builtin_grind_propagator propagateEqUp ↑Eq := fun e => do
-  let_expr Eq _ a b := e | return ()
+  let_expr Eq α a b := e | return ()
   if (← isEqTrue a) then
     pushEq e b <| mkApp3 (mkConst ``Grind.eq_eq_of_eq_true_left) a b (← mkEqTrueProof a)
   else if (← isEqTrue b) then
     pushEq e a <| mkApp3 (mkConst ``Grind.eq_eq_of_eq_true_right) a b (← mkEqTrueProof b)
   else if (← isEqv a b) then
     pushEqTrue e <| mkEqTrueCore e (← mkEqProof a b)
+  if α.isConstOf ``Bool then
+    if (← isEqFalse e) then
+      propagateBoolDiseq a
+      propagateBoolDiseq b
   let aRoot ← getRootENode a
   let bRoot ← getRootENode b
   if aRoot.ctor && bRoot.ctor && aRoot.self.getAppFn != bRoot.self.getAppFn then
@@ -146,6 +156,9 @@ builtin_grind_propagator propagateEqDown ↓Eq := fun e => do
     pushEq a b <| mkOfEqTrueCore e (← mkEqTrueProof e)
   else if (← isEqFalse e) then
     let_expr Eq α lhs rhs := e | return ()
+    if α.isConstOf ``Bool then
+      propagateBoolDiseq lhs
+      propagateBoolDiseq rhs
     propagateCutsatDiseq lhs rhs
     let thms ← getExtTheorems α
     if !thms.isEmpty then
@@ -159,6 +172,25 @@ builtin_grind_propagator propagateEqDown ↓Eq := fun e => do
       for thm in (← getExtTheorems α) do
         instantiateExtTheorem thm e
 
+builtin_grind_propagator propagateBEqUp ↑BEq.beq := fun e => do
+  /-
+  `grind` uses the normalization rule `Bool.beq_eq_decide_eq`, but it is only applicable if
+  the type implements the instances `BEq`, `LawfulBEq`, **and** `DecidableEq α`.
+  However, we may be in a context where only `BEq` and `LawfulBEq` are available.
+  Thus, we have added this propagator as a backup.
+  -/
+  let_expr f@BEq.beq α binst a b := e | return ()
+  if (← isEqv a b) then
+    let u := f.constLevels!
+    let lawfulBEq := mkApp2 (mkConst ``LawfulBEq u) α binst
+    let .some linst ← trySynthInstance lawfulBEq | return ()
+    pushEqBoolTrue e <| mkApp6 (mkConst ``Grind.beq_eq_true_of_eq u) α binst linst a b (← mkEqProof a b)
+  else if let some h ← mkDiseqProof? a b then
+    let u := f.constLevels!
+    let lawfulBEq := mkApp2 (mkConst ``LawfulBEq u) α binst
+    let .some linst ← trySynthInstance lawfulBEq | return ()
+    pushEqBoolFalse e <| mkApp6 (mkConst ``Grind.beq_eq_false_of_diseq u) α binst linst a b h
+
 /-- Propagates `EqMatch` downwards -/
 builtin_grind_propagator propagateEqMatchDown ↓Grind.EqMatch := fun e => do
   if (← isEqTrue e) then

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

@@ -22,15 +22,23 @@ private def withoutModifyingState (x : GoalM α) : GoalM α := do
     set saved
 
 /--
-If `e` has not been internalized yet, simplify it, and internalize the result.
+If `e` has not been internalized yet, instantiate metavariables, unfold reducible, canonicalize,
+and internalize the result.
+
+This is an auxliary function used at `proveEq?` and `proveHEq?`.
 -/
-private def preprocessAndInternalize (e : Expr) (gen : Nat := 0) : GoalM Simp.Result := do
+private def ensureInternalized (e : Expr) : GoalM Expr := do
   if (← alreadyInternalized e) then
-    return { expr := e }
+    return e
   else
-    let r ← preprocess e
-    internalize r.expr gen
-    return r
+    /-
+    It is important to expand reducible declarations. Otherwise, we cannot prove
+    `¬ a = []` and `b ≠ []` by congruence closure even when `a` and `b` are in the same
+    equivalence class.
+    -/
+    let e ← shareCommon (← canon (← unfoldReducible (← instantiateMVars e)))
+    internalize e 0
+    return e
 
 /--
 Try to construct a proof that `lhs = rhs` using the information in the
@@ -42,24 +50,26 @@ This function mainly relies on congruence closure, and constraint
 propagation. It will not perform case analysis.
 -/
 def proveEq? (lhs rhs : Expr) : GoalM (Option Expr) := do
+  trace[grind.debug.proveEq] "({lhs}) = ({rhs})"
   if (← alreadyInternalized lhs <&&> alreadyInternalized rhs) then
     if (← isEqv lhs rhs) then
       return some (← mkEqProof lhs rhs)
     else
       return none
   else withoutModifyingState do
-    let lhs ← preprocessAndInternalize lhs
-    let rhs ← preprocessAndInternalize rhs
+    /-
+    We used to apply the `grind` normalizer, but it created unexpected failures.
+    Here is an example, suppose we are trying to prove `i < (a :: l).length` is equal to `0 < (a :: l).length`
+    when `i` and `0`  are in the same equivalence class. This should hold by applying congruence closure.
+    However, if we apply the normalizer, we obtain `i+1 ≤ (a :: l).length` and `1 ≤ (a :: l).length`, and
+    the equality cannot be detected by congruence closure anymore.
+    -/
+    let lhs ← ensureInternalized lhs
+    let rhs ← ensureInternalized rhs
     processNewFacts
-    unless (← isEqv lhs.expr rhs.expr) do return none
-    unless (← hasSameType lhs.expr rhs.expr) do return none
-    let h ← mkEqProof lhs.expr rhs.expr
-    let h ← match lhs.proof?, rhs.proof? with
-      | none,    none    => pure h
-      | none,    some h₂ => mkEqTrans h (← mkEqSymm h₂)
-      | some h₁, none    => mkEqTrans h₁ h
-      | some h₁, some h₂ => mkEqTrans (← mkEqTrans h₁ h) (← mkEqSymm h₂)
-    return some h
+    unless (← isEqv lhs rhs) do return none
+    unless (← hasSameType lhs rhs) do return none
+    mkEqProof lhs rhs
 
 /-- Similiar to `proveEq?`, but for heterogeneous equality. -/
 def proveHEq? (lhs rhs : Expr) : GoalM (Option Expr) := do
@@ -69,16 +79,11 @@ def proveHEq? (lhs rhs : Expr) : GoalM (Option Expr) := do
     else
       return none
   else withoutModifyingState do
-    let lhs ← preprocessAndInternalize lhs
-    let rhs ← preprocessAndInternalize rhs
+    -- See comment at `proveEq?`
+    let lhs ← ensureInternalized lhs
+    let rhs ← ensureInternalized rhs
     processNewFacts
-    unless (← isEqv lhs.expr rhs.expr) do return none
-    let h ← mkHEqProof lhs.expr rhs.expr
-    let h ← match lhs.proof?, rhs.proof? with
-      | none,    none    => pure h
-      | none,    some h₂ => mkHEqTrans h (← mkHEqSymm h₂)
-      | some h₁, none    => mkHEqTrans h₁ h
-      | some h₁, some h₂ => mkHEqTrans (← mkHEqTrans h₁ h) (← mkHEqSymm h₂)
-    return some h
+    unless (← isEqv lhs rhs) do return none
+    mkHEqProof lhs rhs
 
 end Lean.Meta.Grind

src/Std/Sync.lean

@@ -4,5 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 prelude
+import Std.Sync.Basic
 import Std.Sync.Channel
 import Std.Sync.Mutex
+import Std.Sync.RecursiveMutex
+import Std.Sync.Barrier

src/Std/Sync/Barrier.lean

@@ -0,0 +1,60 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Std.Sync.Mutex
+
+namespace Std
+
+/-
+This file heavily inspired by:
+https://github.com/rust-lang/rust/blob/b8ae372/library/std/src/sync/barrier.rs
+-/
+
+private structure BarrierState where
+  count : Nat
+  generationId : Nat
+
+/--
+A `Barrier` will block `n - 1` threads which call `Barrier.wait` and then wake up all threads at
+once when the `n`-th thread calls `Barrier.wait`.
+-/
+structure Barrier where private mk ::
+  private lock : Mutex BarrierState
+  private cvar : Condvar
+  numThreads : Nat
+
+/--
+Creates a new barrier that can block a given number of threads.
+-/
+def Barrier.new (numThreads : Nat) : BaseIO Barrier := do
+  return {
+    lock := ← Mutex.new { count := 0, generationId := 0 },
+    cvar := ← Condvar.new,
+    numThreads := numThreads
+  }
+
+/--
+Blocks the current thread until all threads have rendezvoused here.
+
+Barriers are re-usable after all threads have rendezvoused once, and can be used continuously.
+
+A single (arbitrary) thread will receive `true` when returning from this function, and all other
+threads will receive `false`.
+-/
+def Barrier.wait (barrier : Barrier) : BaseIO Bool := do
+  barrier.lock.atomically do
+    let localGen := (← get).generationId
+    modify fun s => { s with count := s.count + 1 }
+    if (← get).count < barrier.numThreads then
+      barrier.cvar.waitUntil barrier.lock.mutex do
+        return (← get).generationId != localGen
+      return false
+    else
+      modify fun s => { count := 0, generationId := s.generationId + 1 }
+      barrier.cvar.notifyAll
+      return true
+
+end Std

src/Std/Sync/Basic.lean

@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Ebner
+-/
+prelude
+import Init.System.IO
+import Init.Control.StateRef
+
+namespace Std
+
+/--
+`AtomicT α m` is the monad that can be atomically executed inside mutual exclusion primitives like
+`Mutex α` with outside monad `m`.
+The action has access to the state `α` of the mutex (via `get` and `set`).
+-/
+abbrev AtomicT := StateRefT' IO.RealWorld
+
+end Std

src/Std/Sync/Mutex.lean

@@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner
 -/
 prelude
-import Init.System.IO
-import Init.Control.StateRef
+import Std.Sync.Basic
 
 namespace Std
 
@@ -29,6 +28,7 @@ Locks a `BaseMutex`.  Waits until no other thread has locked the mutex.
 
 The current thread must not have already locked the mutex.
 Reentrant locking is undefined behavior (inherited from the C++ implementation).
+If this is unavoidable in your code, consider using `BaseRecursiveMutex`.
 -/
 @[extern "lean_io_basemutex_lock"]
 opaque BaseMutex.lock (mutex : @& BaseMutex) : BaseIO Unit
@@ -41,6 +41,7 @@ This function does not block.
 
 The current thread must not have already locked the mutex.
 Reentrant locking is undefined behavior (inherited from the C++ implementation).
+If this is unavoidable in your code, consider using `BaseRecursiveMutex`.
 -/
 @[extern "lean_io_basemutex_try_lock"]
 opaque BaseMutex.tryLock (mutex : @& BaseMutex) : BaseIO Bool
@@ -50,6 +51,7 @@ Unlocks a `BaseMutex`.
 
 The current thread must have already locked the mutex.
 Unlocking an unlocked mutex is undefined behavior (inherited from the C++ implementation).
+If this is unavoidable in your code, consider using `BaseRecursiveMutex`.
 -/
 @[extern "lean_io_basemutex_unlock"]
 opaque BaseMutex.unlock (mutex : @& BaseMutex) : BaseIO Unit
@@ -106,14 +108,13 @@ def Condvar.waitUntil [Monad m] [MonadLift BaseIO m]
 /--
 Mutual exclusion primitive (lock) guarding shared state of type `α`.
 
-The type `Mutex α` is similar to `IO.Ref α`,
-except that concurrent accesses are guarded by a mutex
+The type `Mutex α` is similar to `IO.Ref α`, except that concurrent accesses are guarded by a mutex
 instead of atomic pointer operations and busy-waiting.
 -/
 structure Mutex (α : Type) where private mk ::
   private ref : IO.Ref α
   mutex : BaseMutex
-  deriving Nonempty
+deriving Nonempty
 
 instance : CoeOut (Mutex α) BaseMutex where coe := Mutex.mutex
 
@@ -122,13 +123,11 @@ def Mutex.new (a : α) : BaseIO (Mutex α) :=
   return { ref := ← IO.mkRef a, mutex := ← BaseMutex.new }
 
 /--
-`AtomicT α m` is the monad that can be atomically executed inside a `Mutex α`,
-with outside monad `m`.
-The action has access to the state `α` of the mutex (via `get` and `set`).
--/
-abbrev AtomicT := StateRefT' IO.RealWorld
+`mutex.atomically k` runs `k` with access to the mutex's state while locking the mutex.
 
-/-- `mutex.atomically k` runs `k` with access to the mutex's state while locking the mutex. -/
+Calling `mutex.atomically` while already holding the underlying `BaseMutex` in the same thread
+is undefined behavior. If this is unavoidable in your code, consider using `RecursiveMutex`.
+-/
 def Mutex.atomically [Monad m] [MonadLiftT BaseIO m] [MonadFinally m]
     (mutex : Mutex α) (k : AtomicT α m β) : m β := do
   try
@@ -141,7 +140,9 @@ def Mutex.atomically [Monad m] [MonadLiftT BaseIO m] [MonadFinally m]
 `mutex.tryAtomically k` tries to lock `mutex` and runs `k` on it if it succeeds. On success the
 return value of `k` is returned as `some`, on failure `none` is returned.
 
-This function does not block on the `mutex`.
+This function does not block on the `mutex`. Additionally calling `mutex.tryAtomically` while
+already holding the underlying `BaseMutex` in the same thread is undefined behavior. If this is
+unavoidable in your code, consider using `RecursiveMutex`.
 -/
 def Mutex.tryAtomically [Monad m] [MonadLiftT BaseIO m] [MonadFinally m]
     (mutex : Mutex α) (k : AtomicT α m β) : m (Option β) := do
@@ -154,9 +155,11 @@ def Mutex.tryAtomically [Monad m] [MonadLiftT BaseIO m] [MonadFinally m]
     return none
 
 /--
-`mutex.atomicallyOnce condvar pred k` runs `k`,
-waiting on `condvar` until `pred` returns true.
+`mutex.atomicallyOnce condvar pred k` runs `k`, waiting on `condvar` until `pred` returns true.
 Both `k` and `pred` have access to the mutex's state.
+
+Calling `mutex.atomicallyOnce` while already holding the underlying `BaseMutex` in the same thread
+is undefined behavior. If this is unavoidable in your code, consider using `RecursiveMutex`.
 -/
 def Mutex.atomicallyOnce [Monad m] [MonadLiftT BaseIO m] [MonadFinally m]
     (mutex : Mutex α) (condvar : Condvar)

src/Std/Sync/RecursiveMutex.lean

@@ -0,0 +1,102 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Std.Sync.Basic
+
+namespace Std
+
+private opaque RecursiveMutexImpl : NonemptyType.{0}
+
+/--
+Recursive (or reentrant) exclusion primitive.
+
+If you want to guard shared state, use `RecursiveMutex α` instead.
+-/
+def BaseRecursiveMutex : Type := RecursiveMutexImpl.type
+
+instance : Nonempty BaseRecursiveMutex := RecursiveMutexImpl.property
+
+/-- Creates a new `BaseRecursiveMutex`. -/
+@[extern "lean_io_baserecmutex_new"]
+opaque BaseRecursiveMutex.new : BaseIO BaseRecursiveMutex
+
+/--
+Locks a `RecursiveBaseMutex`. Waits until no other thread has locked the mutex.
+If the current thread already holds the mutex this function doesn't block.
+-/
+@[extern "lean_io_baserecmutex_lock"]
+opaque BaseRecursiveMutex.lock (mutex : @& BaseRecursiveMutex) : BaseIO Unit
+
+/--
+Attempts to lock a `RecursiveBaseMutex`. If the mutex is not available return `false`, otherwise
+lock it and return `true`.
+
+This function does not block. Furthermore the same thread may acquire the lock multiple times
+through this function.
+-/
+@[extern "lean_io_baserecmutex_try_lock"]
+opaque BaseRecursiveMutex.tryLock (mutex : @& BaseRecursiveMutex) : BaseIO Bool
+
+/--
+Unlocks a `RecursiveBaseMutex`. The owning thread must make as many `unlock` calls as `lock` and
+`tryLock` calls in order to fully relinquish ownership of the mutex.
+
+The current thread must have already locked the mutex at least once.
+Unlocking an unlocked mutex is undefined behavior (inherited from the C++ implementation).
+-/
+@[extern "lean_io_baserecmutex_unlock"]
+opaque BaseRecursiveMutex.unlock (mutex : @& BaseRecursiveMutex) : BaseIO Unit
+
+/--
+Recursive (or reentrant) mutual exclusion primitive (lock) guarding shared state of type `α`.
+
+The type `RecursiveMutex α` is similar to `IO.Ref α`, except that concurrent accesses are guarded
+by a mutex instead of atomic pointer operations and busy-waiting. Additionally locking a
+`RecursiveMutex` multiple times from the same thread does not block, unlike `Mutex`.
+-/
+structure RecursiveMutex (α : Type) where private mk ::
+  private ref : IO.Ref α
+  mutex : BaseRecursiveMutex
+deriving Nonempty
+
+instance : CoeOut (RecursiveMutex α) BaseRecursiveMutex where coe := RecursiveMutex.mutex
+
+/-- Creates a new recursive mutex. -/
+def RecursiveMutex.new (a : α) : BaseIO (RecursiveMutex α) :=
+  return { ref := ← IO.mkRef a, mutex := ← BaseRecursiveMutex.new }
+
+/--
+`mutex.atomically k` runs `k` with access to the mutex's state while locking the mutex.
+
+Calling `mutex.atomically` while already holding the underlying `BaseRecursiveMutex` in the same
+thread does not block.
+-/
+def RecursiveMutex.atomically [Monad m] [MonadLiftT BaseIO m] [MonadFinally m]
+    (mutex : RecursiveMutex α) (k : AtomicT α m β) : m β := do
+  try
+    mutex.mutex.lock
+    k mutex.ref
+  finally
+    mutex.mutex.unlock
+
+/--
+`mutex.tryAtomically k` tries to lock `mutex` and runs `k` on it if it succeeds. On success the
+return value of `k` is returned as `some`, on failure `none` is returned.
+
+This function does not block on the `mutex`. Additionally `mutex.tryAtomically`, while already
+holding the underlying `BaseRecursiveMutex` in the same thread, does not block.
+-/
+def RecursiveMutex.tryAtomically [Monad m] [MonadLiftT BaseIO m] [MonadFinally m]
+    (mutex : RecursiveMutex α) (k : AtomicT α m β) : m (Option β) := do
+  if ← mutex.mutex.tryLock then
+    try
+      k mutex.ref
+    finally
+      mutex.mutex.unlock
+  else
+    return none
+
+end Std

src/lake/examples/ffi/lib/lakefile.lean

@@ -50,4 +50,3 @@ target libleanffi_shared pkg : Dynlib := do
 
 lean_lib FFI.Shared where
   moreLinkLibs := #[libleanffi_shared]
-  moreLinkArgs := #["-lstdc++"]

src/runtime/mutex.cpp

@@ -2,7 +2,7 @@
 Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
-Authors: Gabriel Ebner
+Authors: Gabriel Ebner, Henrik Böving
 */
 #include <lean/lean.h>
 #include "runtime/mutex.h"
@@ -72,9 +72,39 @@ extern "C" LEAN_EXPORT obj_res lean_io_condvar_notify_all(b_obj_arg condvar, obj
     return io_result_mk_ok(box(0));
 }
 
+static lean_external_class * g_baserecmutex_external_class = nullptr;
+static void baserecmutex_finalizer(void * h) {
+    delete static_cast<recursive_mutex *>(h);
+}
+static void baserecmutex_foreach(void *, b_obj_arg) {}
+
+static recursive_mutex * baserecmutex_get(lean_object * mtx) {
+    return static_cast<recursive_mutex *>(lean_get_external_data(mtx));
+}
+
+extern "C" LEAN_EXPORT obj_res lean_io_baserecmutex_new(obj_arg) {
+    return io_result_mk_ok(lean_alloc_external(g_baserecmutex_external_class, new recursive_mutex));
+}
+
+extern "C" LEAN_EXPORT obj_res lean_io_baserecmutex_lock(b_obj_arg mtx, obj_arg) {
+    baserecmutex_get(mtx)->lock();
+    return io_result_mk_ok(box(0));
+}
+
+extern "C" LEAN_EXPORT obj_res lean_io_baserecmutex_try_lock(b_obj_arg mtx, obj_arg) {
+    bool success = baserecmutex_get(mtx)->try_lock();
+    return io_result_mk_ok(box(success));
+}
+
+extern "C" LEAN_EXPORT obj_res lean_io_baserecmutex_unlock(b_obj_arg mtx, obj_arg) {
+    baserecmutex_get(mtx)->unlock();
+    return io_result_mk_ok(box(0));
+}
+
 void initialize_mutex() {
     g_basemutex_external_class = lean_register_external_class(basemutex_finalizer, basemutex_foreach);
     g_condvar_external_class = lean_register_external_class(condvar_finalizer, condvar_foreach);
+    g_baserecmutex_external_class = lean_register_external_class(baserecmutex_finalizer, baserecmutex_foreach);
 }
 
 void finalize_mutex() {

tests/common.sh

@@ -48,9 +48,13 @@ function exec_capture_raw {
 function exec_capture {
     # backtraces are system-specific, strip them
     # mvar suffixes like in `?m.123` are deterministic but prone to change on minor changes, so strip them
-    LEAN_BACKTRACE=0 "$@" 2>&1 | perl -pe 's/(\?(\w|_\w+))\.[0-9]+/\1/g' > "$f.produced.out"
+    # similarly, links to the language reference may have URL components depending on the toolchain, so normalize those
+    LEAN_BACKTRACE=0 "$@" 2>&1 \
+      | perl -pe 's/(\?(\w|_\w+))\.[0-9]+/\1/g' \
+      | perl -pe 's/https:\/\/lean-lang\.org\/doc\/reference\/(v?[0-9.]+(-rc[0-9]+)?|latest)/REFERENCE/g'  > "$f.produced.out"
 }
 
+
 # Remark: `${var+x}` is a parameter expansion which evaluates to nothing if `var` is unset, and substitutes the string `x` otherwise.
 function check_ret {
     [ -n "${expected_ret+x}" ] || expected_ret=0

tests/lean/1018unknowMVarIssue.lean.expected.out

@@ -60,8 +60,8 @@ a : α
         • Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
           • α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
         • a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • FVarAlias a: _uniq.592 -> _uniq.319
-        • FVarAlias α: _uniq.591 -> _uniq.317
+        • FVarAlias a: _uniq.596 -> _uniq.323
+        • FVarAlias α: _uniq.595 -> _uniq.321
         • ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
         • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
         • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
@@ -75,8 +75,8 @@ a : α
         • Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
           • n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
         • a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • FVarAlias a: _uniq.623 -> _uniq.319
-        • FVarAlias n: _uniq.622 -> _uniq.317
+        • FVarAlias a: _uniq.627 -> _uniq.323
+        • FVarAlias n: _uniq.626 -> _uniq.321
         • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
           • [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
           • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩

tests/lean/1870.lean

@@ -1,23 +0,0 @@
-class One (α : Type u) where
-  one : α
-
-instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
-  ofNat := ‹One α›.1
-
-instance One.ofOfNat1 {α} [OfNat α (nat_lit 1)] : One α where
-  one := 1
-
-set_option pp.mvars false in
-theorem ex1 : (@OfNat.ofNat Nat 0 Zero.toOfNat0) = @OfNat.ofNat Nat 1 One.toOfNat1 := by
-  refine congrArg _ (congrArg _ ?_)
-  rfl
-
-example : (@OfNat.ofNat Nat 0 Zero.toOfNat0) = @OfNat.ofNat Nat 1 One.toOfNat1 := by
-  apply congrArg
-  apply congrArg
-  apply rfl
-
-theorem ex2 : (@OfNat.ofNat Nat 0 Zero.toOfNat0) = @OfNat.ofNat Nat 1 One.toOfNat1 := by
-  apply congrArg
-  apply congrArg
-  apply rfl

tests/lean/1870.lean.expected.out

@@ -1,16 +0,0 @@
-1870.lean:12:2-12:35: error: type mismatch
-  congrArg ?_ (congrArg ?_ ?_)
-has type
-  ?_ (?_ ?_) = ?_ (?_ ?_) : Prop
-but is expected to have type
-  OfNat.ofNat 0 = OfNat.ofNat 1 : Prop
-1870.lean:16:2-16:16: error: tactic 'apply' failed, failed to unify
-  ?f ?a₁ = ?f ?a₂
-with
-  OfNat.ofNat 0 = OfNat.ofNat 1
-⊢ OfNat.ofNat 0 = OfNat.ofNat 1
-1870.lean:21:2-21:16: error: tactic 'apply' failed, failed to unify
-  ?f ?a₁ = ?f ?a₂
-with
-  OfNat.ofNat 0 = OfNat.ofNat 1
-⊢ OfNat.ofNat 0 = OfNat.ofNat 1

tests/lean/948.lean

@@ -1,9 +1,6 @@
 class Trait (X : Type) where
   R : Type
 
-class One (R : Type) where
-  one : R
-
 attribute [reducible] Trait.R
 
 def add_one {X} [Trait X] [One (Trait.R X)] [HAdd X (Trait.R X) X] (x : X) : X := x + (One.one : (Trait.R X))

tests/lean/diamond7.lean

@@ -4,12 +4,6 @@ class Semigroup (α : Type u) extends Mul α where
 class CommSemigroup (α : Type u) extends Semigroup α where
   mul_comm (a b : α) : a * b = b * a
 
-class One (α : Type u) where
-  one : α
-
-instance [One α] : OfNat α (nat_lit 1) where
-  ofNat := One.one
-
 class Monoid (α : Type u) extends Semigroup α, One α where
   one_mul (a : α) : 1 * a = a
   mul_one (a : α) : a * 1 = a

tests/lean/diamond8.lean

@@ -1,6 +1,3 @@
-class One (M : Type u) where one : M
-instance {M} [One M] : OfNat M (nat_lit 1) := ⟨One.one⟩
-
 class Monoid (M : Type u) extends Mul M, One M where
   mul_one (m : M) : m * 1 = m
 

tests/lean/infoFromFailure.lean

@@ -1,18 +0,0 @@
-
-
-def A.foo {α : Type} [Add α] (a : α) : α × α :=
-(a, a + a)
-
-def B.foo {α : Type} (a : α) : α × α :=
-(a, a)
-
-open A
-open B
-
-set_option trace.Meta.synthInstance true
--- `foo` is overloaded, the case `A.foo` is discarded because we don't have an instance `[Add String]`.
--- However, we still want to see the trace since we used trace.Meta.synthInstance
-#check foo "hello"
-
-theorem ex : foo true = (true, true) :=
-rfl

tests/lean/infoFromFailure.lean.expected.out

@@ -1,9 +0,0 @@
-B.foo "hello" : String × String
-[Meta.synthInstance] ❌️ Add String
-  [Meta.synthInstance] no instances for Add String
-    [Meta.synthInstance.instances] #[]
-  [Meta.synthInstance] result <not-available>
-[Meta.synthInstance] ❌️ Add Bool
-  [Meta.synthInstance] no instances for Add Bool
-    [Meta.synthInstance.instances] #[]
-  [Meta.synthInstance] result <not-available>

tests/lean/interactive/completionPrefixIssue.lean.expected.out

@@ -7,7 +7,7 @@
    {"params":
     {"textDocument": {"uri": "file:///completionPrefixIssue.lean"},
      "position": {"line": 1, "character": 64}},
-    "id": {"fvar": {"id": "_uniq.29"}},
+    "id": {"fvar": {"id": "_uniq.32"}},
     "cPos": 0}},
   {"label": "veryLongDefinitionNameVeryLongDefinitionName",
    "kind": 21,

tests/lean/interactive/hover.lean.expected.out

@@ -20,7 +20,7 @@
  {"start": {"line": 12, "character": 4}, "end": {"line": 12, "character": 12}},
  "contents":
  {"value":
-  "```lean\nNat.zero : Nat\n```\n***\nZero, the smallest natural number.\n\nUsing `Nat.zero` explicitly should usually be avoided in favor of the literal `0`, which is the\n[simp normal form](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
+  "```lean\nNat.zero : Nat\n```\n***\nZero, the smallest natural number.\n\nUsing `Nat.zero` explicitly should usually be avoided in favor of the literal `0`, which is the\n[simp normal form](REFERENCE/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hover.lean"},
  "position": {"line": 21, "character": 2}}
@@ -521,7 +521,7 @@
  {"start": {"line": 257, "character": 4}, "end": {"line": 257, "character": 9}},
  "contents":
  {"value":
-  "```lean\nNat.zero : ℕ\n```\n***\nZero, the smallest natural number.\n\nUsing `Nat.zero` explicitly should usually be avoided in favor of the literal `0`, which is the\n[simp normal form](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
+  "```lean\nNat.zero : ℕ\n```\n***\nZero, the smallest natural number.\n\nUsing `Nat.zero` explicitly should usually be avoided in favor of the literal `0`, which is the\n[simp normal form](REFERENCE/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hover.lean"},
  "position": {"line": 257, "character": 15}}
@@ -530,7 +530,7 @@
   "end": {"line": 257, "character": 18}},
  "contents":
  {"value":
-  "```lean\nNat.zero : ℕ\n```\n***\nZero, the smallest natural number.\n\nUsing `Nat.zero` explicitly should usually be avoided in favor of the literal `0`, which is the\n[simp normal form](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
+  "```lean\nNat.zero : ℕ\n```\n***\nZero, the smallest natural number.\n\nUsing `Nat.zero` explicitly should usually be avoided in favor of the literal `0`, which is the\n[simp normal form](REFERENCE/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hover.lean"},
  "position": {"line": 260, "character": 6}}
@@ -538,7 +538,7 @@
  {"start": {"line": 260, "character": 4}, "end": {"line": 260, "character": 9}},
  "contents":
  {"value":
-  "```lean\nNat.succ (n : ℕ) : ℕ\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
+  "```lean\nNat.succ (n : ℕ) : ℕ\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](REFERENCE/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hover.lean"},
  "position": {"line": 260, "character": 17}}
@@ -547,7 +547,7 @@
   "end": {"line": 260, "character": 20}},
  "contents":
  {"value":
-  "```lean\nNat.succ (n : ℕ) : ℕ\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
+  "```lean\nNat.succ (n : ℕ) : ℕ\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](REFERENCE/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hover.lean"},
  "position": {"line": 263, "character": 27}}
@@ -565,7 +565,7 @@
   "end": {"line": 263, "character": 36}},
  "contents":
  {"value":
-  "```lean\nNat.zero : ℕ\n```\n***\nZero, the smallest natural number.\n\nUsing `Nat.zero` explicitly should usually be avoided in favor of the literal `0`, which is the\n[simp normal form](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
+  "```lean\nNat.zero : ℕ\n```\n***\nZero, the smallest natural number.\n\nUsing `Nat.zero` explicitly should usually be avoided in favor of the literal `0`, which is the\n[simp normal form](REFERENCE/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hover.lean"},
  "position": {"line": 269, "character": 2}}

tests/lean/interactive/hoverDot.lean.expected.out

@@ -20,7 +20,7 @@
  {"start": {"line": 12, "character": 14}, "end": {"line": 12, "character": 18}},
  "contents":
  {"value":
-  "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
+  "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](REFERENCE/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hoverDot.lean"},
  "position": {"line": 16, "character": 11}}
@@ -34,7 +34,7 @@
  {"start": {"line": 16, "character": 14}, "end": {"line": 16, "character": 18}},
  "contents":
  {"value":
-  "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
+  "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](REFERENCE/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hoverDot.lean"},
  "position": {"line": 19, "character": 13}}
@@ -48,7 +48,7 @@
  {"start": {"line": 19, "character": 16}, "end": {"line": 19, "character": 20}},
  "contents":
  {"value":
-  "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
+  "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](REFERENCE/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hoverDot.lean"},
  "position": {"line": 22, "character": 14}}
@@ -62,5 +62,5 @@
  {"start": {"line": 22, "character": 17}, "end": {"line": 22, "character": 21}},
  "contents":
  {"value":
-  "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
+  "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](REFERENCE/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
   "kind": "markdown"}}

tests/lean/run/1711.lean

@@ -1,9 +1,3 @@
-class One (α : Type u) where
-  one : α
-
-instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
-  ofNat := ‹One α›.1
-
 class MulOneClass (M : Type u) extends One M, Mul M where
   one_mul : ∀ a : M, 1 * a = a
   mul_one : ∀ a : M, a * 1 = a

tests/lean/run/1870.lean

@@ -0,0 +1,40 @@
+set_option pp.mvars false
+
+/--
+error: type mismatch
+  congrArg ?_ (congrArg ?_ ?_)
+has type
+  ?_ (?_ ?_) = ?_ (?_ ?_) : Prop
+but is expected to have type
+  OfNat.ofNat 0 = OfNat.ofNat 1 : Prop
+-/
+#guard_msgs in
+theorem ex1 : (@OfNat.ofNat Nat 0 Zero.toOfNat0) = @OfNat.ofNat Nat 1 One.toOfNat1 := by
+  refine congrArg _ (congrArg _ ?_)
+  rfl
+
+/--
+error: tactic 'apply' failed, failed to unify
+  ?_ ?_ = ?_ ?_
+with
+  OfNat.ofNat 0 = OfNat.ofNat 1
+⊢ OfNat.ofNat 0 = OfNat.ofNat 1
+-/
+#guard_msgs in
+example : (@OfNat.ofNat Nat 0 Zero.toOfNat0) = @OfNat.ofNat Nat 1 One.toOfNat1 := by
+  apply congrArg
+  apply congrArg
+  apply rfl
+
+/--
+error: tactic 'apply' failed, failed to unify
+  ?_ ?_ = ?_ ?_
+with
+  OfNat.ofNat 0 = OfNat.ofNat 1
+⊢ OfNat.ofNat 0 = OfNat.ofNat 1
+-/
+#guard_msgs in
+theorem ex2 : (@OfNat.ofNat Nat 0 Zero.toOfNat0) = @OfNat.ofNat Nat 1 One.toOfNat1 := by
+  apply congrArg
+  apply congrArg
+  apply rfl

tests/lean/run/1907.lean

@@ -1,9 +1,3 @@
-class One (α : Type u) where
-  one : α
-
-instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
-  ofNat := ‹One α›.1
-
 class MulOneClass (M : Type u) extends One M, Mul M
 
 class FunLike (F : Sort _) (α : outParam (Sort _)) (β : outParam <| α → Sort _) where

tests/lean/run/1907orig.lean

@@ -1,9 +1,3 @@
-class One (α : Type u) where
-  one : α
-
-instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
-  ofNat := ‹One α›.1
-
 class MulOneClass (M : Type u) extends One M, Mul M
 
 class FunLike (F : Sort _) (α : outParam (Sort _)) (β : outParam <| α → Sort _) where

tests/lean/run/1951.lean

@@ -1,7 +1,5 @@
 class FunLike (F : Type _) (A : outParam (Type _)) (B : outParam (A → Type _)) where toFun : F → ∀ a, B a
 instance [FunLike F A B] : CoeFun F fun _ => ∀ a, B a where coe := FunLike.toFun
-class One (M) where one : M
-instance [One M] : OfNat M (nat_lit 1) where ofNat := One.one
 class OneHomClass (F) (A B : outParam _) [One A] [One B] extends FunLike F A fun _ => B where
   map_one (f : F) : f 1 = 1
 class MulHomClass (F) (A B : outParam _) [Mul A] [Mul B] extends FunLike F A fun _ => B

tests/lean/run/2461.lean

@@ -1,8 +1,5 @@
 section algebra_hierarchy_classes_to_comm_ring
 
-class One (α : Type) where
-  one : α
-
 class Semiring (α : Type) extends Add α, Mul α, Zero α, One α
 
 class CommSemiring (R : Type) extends Semiring R

tests/lean/run/2736.lean

@@ -1,15 +1,5 @@
 set_option autoImplicit true
 
-section Mathlib.Init.ZeroOne
-
-class One (α : Type) where
-  one : α
-
-instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
-  ofNat := ‹One α›.1
-
-end Mathlib.Init.ZeroOne
-
 section Mathlib.Algebra.Group.Defs
 
 class MulOneClass (M : Type) extends One M, Mul M where

tests/lean/run/3150.lean

@@ -1,6 +1,3 @@
-class One (α : Type) where
-  one : α
-
 variable (R A : Type) [One R] [One A]
 
 class OneHom where

tests/lean/run/3807.lean

@@ -87,18 +87,6 @@ class PartialOrder (α : Type u) extends Preorder α where
 
 end Mathlib.Init.Order.Defs
 
-section Mathlib.Init.ZeroOne
-
-set_option autoImplicit true
-
-class One (α : Type u) where
-  one : α
-
-instance (priority := 300) One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
-  ofNat := ‹One α›.1
-
-end Mathlib.Init.ZeroOne
-
 section Mathlib.Init.Function
 
 universe u₁ u₂

tests/lean/run/KyleAlg.lean

@@ -14,13 +14,7 @@ class Inv (α : Type u) where
 
 postfix:max "⁻¹" => Inv.inv
 
-class One (α : Type u) where
-    one : α
 export One (one)
-
-instance [One α] : OfNat α (nat_lit 1) where
-    ofNat := one
-
 export Zero (zero)
 
 class MulComm (α : Type u) [Mul α] : Prop where

tests/lean/run/KyleAlgAbbrev.lean

@@ -14,13 +14,6 @@ class Inv (α : Type u) where
 
 postfix:max "⁻¹" => Inv.inv
 
-class One (α : Type u) where
-    one : α
-export One (one)
-
-instance [One α] : OfNat α (nat_lit 1) where
-    ofNat := one
-
 export Zero (zero)
 
 instance [Zero α] : OfNat α (nat_lit 0) where

tests/lean/run/alg.lean

@@ -14,12 +14,6 @@ class CommSemigroup (α : Type u) extends Semigroup α where
 instance [CommSemigroup α] : MulComm α where
   mul_comm := CommSemigroup.mul_comm
 
-class One (α : Type u) where
-  one : α
-
-instance [One α] : OfNat α (nat_lit 1) where
-  ofNat := One.one
-
 class Monoid (α : Type u) extends Semigroup α, One α where
   one_mul (a : α) : 1 * a = a
   mul_one (a : α) : a * 1 = a

tests/lean/run/binop_binrel_perf_issue.lean

@@ -22,18 +22,6 @@ end Set
 
 end Mathlib.Init.Set
 
-section Mathlib.Init.ZeroOne
-
-set_option autoImplicit true
-
-class One (α : Type u) where
-  one : α
-
-instance (priority := 300) One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
-  ofNat := ‹One α›.1
-
-end Mathlib.Init.ZeroOne
-
 section Mathlib.Init.Function
 
 universe u₁ u₂

tests/lean/run/grind_bool_diseq.lean

@@ -0,0 +1,25 @@
+set_option grind.warning false
+
+example (f : Bool → Nat) : (x = y ↔ q) → ¬ q → y = false → f x = 0 → f true = 0 := by
+  grind (splits := 0)
+
+example (f : Bool → Nat) : (x = false ↔ q) → ¬ q → f x = 0 → f true = 0 := by
+  grind (splits := 0)
+
+example (f : Bool → Nat) : (y = x ↔ q) → ¬ q → y = false → f x = 0 → f true = 0 := by
+  grind (splits := 0)
+
+example (f : Bool → Nat) : (x = true ↔ q) → ¬ q → f x = 0 → f false = 0 := by
+  grind (splits := 0)
+
+example (f : Bool → Nat) : (true = x ↔ q) → ¬ q → f x = 0 → f false = 0 := by
+  grind (splits := 0)
+
+example (f : Bool → Nat) : (false = x ↔ q) → ¬ q → f x = 0 → f true = 0 := by
+  grind (splits := 0)
+
+example (f : Bool → Nat) : (x = false ↔ q) → ¬ q → f x = 0 → f true = 0 := by
+  grind (splits := 0)
+
+example (f : Bool → Nat) : (y = x ↔ q) → ¬ q → y = true → f x = 0 → f false = 0 := by
+  grind (splits := 0)

tests/lean/run/grind_canon_insts.lean

@@ -18,12 +18,6 @@ class CommSemigroup (α : Type u) extends Semigroup α where
 instance [CommSemigroup α] : MulComm α where
   mul_comm := CommSemigroup.mul_comm
 
-class One (α : Type u) where
-  one : α
-
-instance [One α] : OfNat α (nat_lit 1) where
-  ofNat := One.one
-
 class Monoid (α : Type u) extends Semigroup α, One α where
   one_mul (a : α) : 1 * a = a
   mul_one (a : α) : a * 1 = a
@@ -59,11 +53,11 @@ def fallback : Fallback := do
 set_option trace.Meta.debug true
 
 /--
-info: [Meta.debug] [NatCast.natCast a * (NatCast.natCast b * NatCast.natCast c),
-     NatCast.natCast b * NatCast.natCast c,
-     NatCast.natCast d * (NatCast.natCast b * NatCast.natCast c),
-     -1 * (NatCast.natCast a * (NatCast.natCast b * NatCast.natCast c)),
-     -1 * (NatCast.natCast d * (NatCast.natCast b * NatCast.natCast c)),
+info: [Meta.debug] [↑a * (↑b * ↑c),
+     ↑b * ↑c,
+     ↑d * (↑b * ↑c),
+     -1 * (↑a * (↑b * ↑c)),
+     -1 * (↑d * (↑b * ↑c)),
      a * (b * c),
      b * c,
      d * (b * c)]

tests/lean/run/grind_eq.lean

@@ -72,7 +72,7 @@ info: [grind.assert] x1 = appV a_2 b
 [grind.assert] ¬HEq x2 x4
 [grind.ematch.instance] appV_assoc: HEq (appV a_2 (appV b c)) (appV (appV a_2 b) c)
 [grind.assert] HEq (appV a_2 (appV b c)) (appV (appV a_2 b) c)
-[grind.assert] -1 * NatCast.natCast a ≤ 0
+[grind.assert] -1 * ↑a ≤ 0
 -/
 #guard_msgs (info) in
 example : x1 = appV a b → x2 = appV x1 c → x3 = appV b c → x4 = appV a x3 → HEq x2 x4 := by

tests/lean/run/grind_list_issue.lean

@@ -0,0 +1,9 @@
+reset_grind_attrs%
+open List Nat
+
+attribute [grind] List.filter_nil List.filter_cons
+attribute [grind] List.any_nil List.any_cons
+
+@[simp] theorem any_filter {l : List α} {p q : α → Bool} :
+    (filter p l).any q = l.any fun a => p a && q a := by
+  induction l <;> grind

tests/lean/run/grind_offset.lean

@@ -51,7 +51,7 @@ info: [grind.assert] f (c + 2) = a
 [grind.assert] ¬a = g (g (f c))
 [grind.ematch.instance] f.eq_2: f (c + 1).succ = g (f (c + 1))
 [grind.assert] f (c + 2) = g (f (c + 1))
-[grind.assert] -1 * NatCast.natCast c ≤ 0
+[grind.assert] -1 * ↑c ≤ 0
 [grind.ematch.instance] f.eq_2: f c.succ = g (f c)
 [grind.assert] f (c + 1) = g (f c)
 -/
@@ -77,8 +77,8 @@ info: [grind.assert] foo (c + 1) = a
 [grind.assert] ¬a = g (foo b)
 [grind.ematch.instance] foo.eq_3: foo b.succ.succ = g (foo b)
 [grind.assert] foo (b + 2) = g (foo b)
-[grind.assert] -1 * NatCast.natCast b ≤ 0
-[grind.assert] -1 * NatCast.natCast c ≤ 0
+[grind.assert] -1 * ↑b ≤ 0
+[grind.assert] -1 * ↑c ≤ 0
 -/
 #guard_msgs (info) in
 example : foo (c + 1) = a → c = b + 1 → a = g (foo b) := by

tests/lean/run/grind_proveEqIssue.lean

@@ -0,0 +1,11 @@
+reset_grind_attrs%
+open List Nat
+
+attribute [grind] List.getElem_cons_zero
+
+theorem getElem_cons {l : List α} (w : i < (a :: l).length) :
+    (a :: l)[i] =
+      if h : i = 0 then a else l[i-1]'(match i, h with | i+1, _ => succ_lt_succ_iff.mp w) := by
+  split
+  · grind
+  · sorry

tests/lean/run/grind_regression.lean

@@ -640,9 +640,6 @@ end
 
 section
 
-class One (α) where one : α
-instance [One α] : OfNat α 1 where ofNat := One.one
-
 class Inv (α) where inv : α → α
 postfix:max "⁻¹" => Inv.inv
 

tests/lean/run/grind_shelf.lean

@@ -1,9 +1,3 @@
-class One (α : Type u) where
-  one : α
-
-instance (priority := 300) One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
-  ofNat := ‹One α›.1
-
 class Shelf (α : Type u) where
   act : α → α → α
   self_distrib : ∀ {x y z : α}, act x (act y z) = act (act x y) (act x z)

tests/lean/run/grind_t1.lean

@@ -1,4 +1,5 @@
 set_option grind.warning false
+
 example (a b : List Nat) : a = [] → b = [2] → a = b → False := by
   grind
 
@@ -396,3 +397,26 @@ example [Decidable p] : false = a → ¬p → decide p = a := by
 
 example (a : Nat) (p q r : Prop) (h₁ : if _ : a < 1 then p else q) (h₂ : r) : (if a < 1 then p else q) ↔ r := by
   grind (splits := 0)
+
+example [BEq α] [LawfulBEq α] (a b : α) : a == b → a = b := by
+  grind
+
+example [BEq α] [LawfulBEq α] {a : α} : (a::as).replace a b = b::as := by
+  grind [List.replace]
+
+example [BEq α] [LawfulBEq α] {a : α} : (a::as).replace a b = b::as := by
+  grind [List.replace_cons]
+
+def foo [BEq α] (a b : α) :=
+  match a == b with
+  | true => 1
+  | false => 0
+
+example [BEq α] [LawfulBEq α] (a b : α) : a = b → foo a b = 1 := by
+  grind (splits := 0) [foo]
+
+example [BEq α] [LawfulBEq α] (a b : α) : a ≠ b → foo a b = 0 := by
+  grind [foo]
+
+example [BEq α] [LawfulBEq α] (a b : α) : a ≠ b → foo a b = 0 := by
+  grind (splits := 0) [foo]

tests/lean/run/infoFromFailure.lean

@@ -0,0 +1,43 @@
+
+
+def A.foo {α : Type} [Add α] (a : α) : α × α :=
+(a, a + a)
+
+def B.foo {α : Type} (a : α) : α × α :=
+(a, a)
+
+open A
+open B
+
+set_option trace.Meta.synthInstance true
+
+/--
+info: B.foo "hello" : String × String
+---
+info: [Meta.synthInstance] ❌️ Add String
+  [Meta.synthInstance] new goal Add String
+    [Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toAdd]
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.CommRing.toAdd to Add String
+    [Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
+    [Meta.synthInstance] no instances for Lean.Grind.CommRing String
+      [Meta.synthInstance.instances] #[]
+  [Meta.synthInstance] result <not-available>
+-/
+#guard_msgs in
+-- `foo` is overloaded, the case `A.foo` is discarded because we don't have an instance `[Add String]`.
+-- However, we still want to see the trace since we used trace.Meta.synthInstance
+#check foo "hello"
+
+/--
+info: [Meta.synthInstance] ❌️ Add Bool
+  [Meta.synthInstance] new goal Add Bool
+    [Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toAdd]
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.CommRing.toAdd to Add Bool
+    [Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
+    [Meta.synthInstance] no instances for Lean.Grind.CommRing Bool
+      [Meta.synthInstance.instances] #[]
+  [Meta.synthInstance] result <not-available>
+-/
+#guard_msgs in
+theorem ex : foo true = (true, true) :=
+rfl

tests/lean/run/linearCategory_perf_issue.lean

@@ -1,15 +1,5 @@
 universe u v w v₁ v₂ v₃ u₁ u₂ u₃
 
-section Mathlib.Algebra.Group.ZeroOne
-
-class One (α : Type u) where
-  one : α
-
-instance (priority := 300) One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
-  ofNat := ‹One α›.1
-
-end Mathlib.Algebra.Group.ZeroOne
-
 section Mathlib.Algebra.Group.Defs
 
 class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where

tests/lean/run/mathlibetaissue.lean

@@ -42,15 +42,6 @@ class RatCast (K : Type u) where
 
 end Std.Classes.RatCast
 
-section Mathlib.Init.ZeroOne
-
-class One (α : Type u) where
-  one : α
-instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
-  ofNat := ‹One α›.1
-
-end Mathlib.Init.ZeroOne
-
 section Mathlib.Algebra.Group.Defs
 
 class Inv (α : Type u) where

tests/lean/run/matrix.lean

@@ -1,14 +1,3 @@
-/-
-Helper classes for Lean 3 users
--/
-class One (α : Type u) where
-  one : α
-
-instance [OfNat α (nat_lit 1)] : One α where
-  one := 1
-
-instance [One α] : OfNat α (nat_lit 1) where
-  ofNat := One.one
 
 /- Simple Matrix -/
 

tests/lean/run/ofNatNormNum.lean

@@ -6,12 +6,6 @@ export OfNatSound (ofNat_add)
 theorem ex1 {α : Type u} [Add α] [(n : Nat) → OfNat α n] [OfNatSound α] : (10000000 : α) + 10000000 = 20000000 :=
   ofNat_add ..
 
-class One (α : Type u) where
-  one : α
-
-instance [One α] : OfNat α (nat_lit 1) where
-  ofNat := One.one
-
 -- Some example structure
 class S (α : Type u) extends Add α, Mul α, Zero α, One α where
   add_assoc (a b c : α)    : a + b + c = a + (b + c)

tests/lean/run/proofAsSorry.lean

@@ -1,10 +1,11 @@
 set_option debug.proofAsSorry true
+set_option pp.mvars false
 
 /--
 error: type mismatch
   rfl
 has type
-  ?m.156 = ?m.156 : Prop
+  ?_ = ?_ : Prop
 but is expected to have type
   2 + 2 = 5 : Prop
 -/

tests/lean/run/regressions3210.lean

@@ -5,14 +5,6 @@ example : ¬1 % 2 = 0 := by
 
 universe u
 
-class One (α : Type u) where
-  one : α
-
-instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
-  ofNat := ‹One α›.1
-instance One.ofOfNat1 {α} [OfNat α (nat_lit 1)] : One α where
-  one := 1
-
 example : Not
   (@Eq.{1} Nat
     (@HMod.hMod.{0, 0, 0} Nat Nat Nat (@instHMod.{0} Nat Nat.instMod)

tests/lean/run/structWithAlgTCSynth.lean

@@ -85,16 +85,6 @@ end Quotient
 
 end Mathlib.Data.Quot
 
-section Mathlib.Init.ZeroOne
-
-class One (α : Type u) where
-  one : α
-
-instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
-  ofNat := ‹One α›.1
-
-section Mathlib.Init.ZeroOne
-
 section Mathlib.Logic.Function.Basic
 
 namespace Function

tests/lean/run/sync_barrier.lean

@@ -0,0 +1,32 @@
+import Std.Sync.Barrier
+
+def consBarrier (b : Std.Barrier) (list : IO.Ref (List Nat)) : IO Bool := do
+  for _ in [0:1000] do
+    list.modify fun l => 1 :: l
+  let isLeader ← b.wait
+  for _ in [0:1000] do
+    list.modify fun l => 2 :: l
+  return isLeader
+
+def barrier : IO Unit := do
+  let b ← Std.Barrier.new 2
+  let ref ← IO.mkRef []
+  go b ref
+  -- reuse barrier
+  go b ref
+where
+  go (b : Std.Barrier) (ref : IO.Ref (List Nat)) : IO Unit := do
+    let t1 ← IO.asTask (prio := .dedicated) (consBarrier b ref)
+    let t2 ← IO.asTask (prio := .dedicated) (consBarrier b ref)
+    let leaderT1 ← IO.ofExcept t1.get
+    let leaderT2 ← IO.ofExcept t2.get
+    if leaderT1 == leaderT2 then
+      let err := s!"Exactly one should be leader but t1 leader? {leaderT1} t2 leader? {leaderT2}"
+      throw <| .userError err
+    let list ← ref.get
+    if list.take 2000 |>.any (· != 2) then
+      throw <| .userError "List head should have only 2's but doesn't"
+    if list.drop 2000 |>.take 2000 |>.any (· != 1) then
+      throw <| .userError "List tail should have only 1's but doesn't"
+
+#eval barrier

tests/lean/run/sync_recursive_mutex.lean

@@ -0,0 +1,70 @@
+import Std.Sync.RecursiveMutex
+
+def countIt (mutex : Std.RecursiveMutex Nat) : IO Unit := do
+  for _ in [0:1000] do
+    mutex.atomically do
+      modify fun s => s + 1
+
+def atomically : IO Unit := do
+  let mutex ← Std.RecursiveMutex.new 0
+  let t1 ← IO.asTask (prio := .dedicated) (countIt mutex)
+  let t2 ← IO.asTask (prio := .dedicated) (countIt mutex)
+  let t3 ← IO.asTask (prio := .dedicated) (countIt mutex)
+  let t4 ← IO.asTask (prio := .dedicated) (countIt mutex)
+  IO.ofExcept t1.get
+  IO.ofExcept t2.get
+  IO.ofExcept t3.get
+  IO.ofExcept t4.get
+  mutex.atomically do
+    let val ← get
+    if val != 4000 then
+      throw <| .userError s!"Should be 4000 but was {val}"
+
+def holdIt (mutex : Std.RecursiveMutex Nat) (ref : IO.Ref Nat) : IO Unit := do
+  mutex.atomically do
+    ref.set 1
+    modify fun s => s + 1
+    while (← ref.get) == 1 do
+      IO.sleep 1
+
+def tryIt (mutex : Std.RecursiveMutex Nat) (ref : IO.Ref Nat) : IO Unit := do
+  while (← ref.get) == 0 do
+    IO.sleep 1
+  let success ← mutex.tryAtomically (modify fun s => s + 1)
+  if success.isSome then throw <| .userError s!"lock succeeded but shouldn't"
+  ref.set 2
+  mutex.atomically (modify fun s => s + 1)
+  let success ← mutex.tryAtomically (modify fun s => s + 1)
+  if success.isNone then throw <| .userError s!"lock didn't succeed but should"
+
+
+def tryAtomically : IO Unit := do
+  let mutex ← Std.RecursiveMutex.new 0
+  let ref ← IO.mkRef 0
+  let t1 ← IO.asTask (prio := .dedicated) (holdIt mutex ref)
+  let t2 ← IO.asTask (prio := .dedicated) (tryIt mutex ref)
+  IO.ofExcept t1.get
+  IO.ofExcept t2.get
+  mutex.atomically do
+    let val ← get
+    if val != 3 then
+      throw <| .userError s!"Should be 3 but was {val}"
+
+def recursive : IO Unit := do
+  let mutex ← Std.RecursiveMutex.new 0
+  mutex.atomically do
+    mutex.atomically do
+      modify fun s => s + 1
+
+  mutex.atomically do
+    discard <| mutex.tryAtomically do
+      modify fun s => s + 1
+
+  mutex.atomically do
+    let val ← get
+    if val != 2 then
+      throw <| .userError s!"Should be 2 but was {val}"
+
+#eval atomically
+#eval tryAtomically
+#eval recursive