checkpoint

This PR fixes universe unification for `for` loops with `mut` variables
whose types span multiple implicit universes. The old approach used
`ensureHasType (mkSort mi.u.succ)` per variable, which generated
constraints like `max (?u+1) (?v+1) =?= ?u+1` that the universe solver
cannot decompose. The new approach uses `getDecLevel`/`isLevelDefEq` on
the decremented level, producing `max ?u ?v =?= ?u` which `solveSelfMax`
handles directly.

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

.github/workflows/build-template.yml

@@ -59,11 +59,11 @@ jobs:
         with:
           msystem: clang64
           # `:` means do not prefix with msystem
-          pacboy: "make: python: cmake clang ccache gmp libuv openssl: git: zip: unzip: diffutils: binutils: tree: zstd tar:"
+          pacboy: "make: python: cmake clang ccache gmp libuv git: zip: unzip: diffutils: binutils: tree: zstd tar:"
         if: runner.os == 'Windows'
       - name: Install Brew Packages
         run: |
-          brew install ccache tree zstd coreutils gmp libuv openssl
+          brew install ccache tree zstd coreutils gmp libuv
         if: runner.os == 'macOS'
       - name: Checkout
         uses: actions/checkout@v6
@@ -92,7 +92,7 @@ jobs:
         run: |
           sudo dpkg --add-architecture i386
           sudo apt-get update
-          sudo apt-get install -y gcc-multilib g++-multilib ccache libuv1-dev:i386 libssl-dev:i386 pkgconf:i386
+          sudo apt-get install -y gcc-multilib g++-multilib ccache libuv1-dev:i386 pkgconf:i386
         if: matrix.cmultilib
       - name: Restore Cache
         id: restore-cache
@@ -131,7 +131,7 @@ jobs:
           [ -d build ] || mkdir build
           cd build
           # arguments passed to `cmake`
-          OPTIONS=(-DLEAN_EXTRA_MAKE_OPTS=-DwarningAsError=true)
+          OPTIONS=(-DWFAIL=ON)
           if [[ -n '${{ matrix.release }}' ]]; then
             # this also enables githash embedding into stage 1 library, which prohibits reusing
             # `.olean`s across commits, so we don't do it in the fast non-release CI

.github/workflows/update-stage0.yml

@@ -77,7 +77,7 @@ jobs:
       # sync options with `Linux Lake` to ensure cache reuse
       run: |
         mkdir -p build
-        cmake --preset release -B build -DLEAN_EXTRA_MAKE_OPTS=-DwarningAsError=true
+        cmake --preset release -B build -DWFAIL=ON
       shell: 'nix develop -c bash -euxo pipefail {0}'
     - if: env.should_update_stage0 == 'yes'
       run: |

.gitignore

@@ -34,3 +34,4 @@ wdErr.txt
 wdIn.txt
 wdOut.txt
 downstream_releases/
+.claude/worktrees/

doc/make/index.md

@@ -9,7 +9,6 @@ Requirements
 - [CMake](http://www.cmake.org)
 - [GMP (GNU multiprecision library)](http://gmplib.org/)
 - [LibUV](https://libuv.org/)
-- [OpenSSL](https://www.openssl.org/)
 
 Platform-Specific Setup
 -----------------------

doc/make/msys2.md

@@ -32,7 +32,7 @@ MSYS2 has a package management system, [pacman][pacman].
 Here are the commands to install all dependencies needed to compile Lean on your machine.
 
 ```bash
-pacman -S make python mingw-w64-clang-x86_64-cmake mingw-w64-clang-x86_64-clang mingw-w64-clang-x86_64-ccache mingw-w64-clang-x86_64-libuv mingw-w64-clang-x86_64-gmp mingw-w64-clang-x86_64-openssl git unzip diffutils binutils
+pacman -S make python mingw-w64-clang-x86_64-cmake mingw-w64-clang-x86_64-clang mingw-w64-clang-x86_64-ccache mingw-w64-clang-x86_64-libuv mingw-w64-clang-x86_64-gmp git unzip diffutils binutils
 ```
 
 You should now be able to run these commands:

doc/make/osx-10.9.md

@@ -32,13 +32,12 @@ following to use `g++`.
 cmake -DCMAKE_CXX_COMPILER=g++ ...
 ```
 
-## Required Packages: CMake, GMP, libuv, OpenSSL, pkgconf
+## Required Packages: CMake, GMP, libuv, pkgconf
 
 ```bash
 brew install cmake
 brew install gmp
 brew install libuv
-brew install openssl
 brew install pkgconf
 ```
 

doc/make/ubuntu.md

@@ -8,5 +8,5 @@ follow the [generic build instructions](index.md).
 ## Basic packages
 
 ```bash
-sudo apt-get install git libgmp-dev libuv1-dev libssl-dev cmake ccache clang pkgconf
+sudo apt-get install git libgmp-dev libuv1-dev cmake ccache clang pkgconf
 ```

flake.nix

@@ -24,7 +24,7 @@
           stdenv = pkgs.overrideCC pkgs.stdenv llvmPackages.clang;
         } ({
           buildInputs = with pkgs; [
-            cmake gmp libuv ccache pkg-config openssl openssl.dev
+            cmake gmp libuv ccache pkg-config
             llvmPackages.bintools  # wrapped lld
             llvmPackages.llvm  # llvm-symbolizer for asan/lsan
             gdb
@@ -34,21 +34,7 @@
           hardeningDisable = [ "all" ];
           # more convenient `ctest` output
           CTEST_OUTPUT_ON_FAILURE = 1;
-        } // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux (let
-          # Build OpenSSL 3 statically using pkgsDist's old-glibc stdenv,
-          # so the resulting static libs don't require newer glibc symbols.
-          opensslForDist = pkgsDist.stdenv.mkDerivation {
-            name = "openssl-static-${pkgs.lib.getVersion pkgs.openssl.name}";
-            inherit (pkgs.openssl) src;
-            nativeBuildInputs = [ pkgsDist.perl ];
-            configurePhase = ''
-            patchShebangs .
-            ./config --prefix=$out no-shared no-tests
-          '';
-            buildPhase = "make -j$NIX_BUILD_CORES";
-            installPhase = "make install_sw";
-          };
-        in {
+        } // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux {
           GMP = (pkgsDist.gmp.override { withStatic = true; }).overrideAttrs (attrs:
             pkgs.lib.optionalAttrs (pkgs.stdenv.system == "aarch64-linux") {
               # would need additional linking setup on Linux aarch64, we don't use it anywhere else either
@@ -67,15 +53,13 @@
             };
             doCheck = false;
           });
-          OPENSSL = opensslForDist;
-          OPENSSL_DEV = opensslForDist;
           GLIBC = pkgsDist.glibc;
           GLIBC_DEV = pkgsDist.glibc.dev;
           GCC_LIB = pkgsDist.gcc.cc.lib;
           ZLIB = pkgsDist.zlib;
           # for CI coredumps
           GDB = pkgsDist.gdb;
-        }));
+        });
     in {
       devShells.${system} = {
         # The default development shell for working on lean itself

script/prepare-llvm-linux.sh

@@ -1,7 +1,7 @@
 #!/usr/bin/env bash
 set -euxo pipefail
 
-# run from root build directory (from inside nix-shell or otherwise defining GLIBC/ZLIB/GMP/OPENSSL) as in
+# run from root build directory (from inside nix-shell or otherwise defining GLIBC/ZLIB/GMP) as in
 # ```
 # eval cmake ../.. $(../../script/prepare-llvm-linux.sh ~/Downloads/lean-llvm-x86_64-linux-gnu.tar.zst)
 # ```
@@ -42,8 +42,6 @@ $CP $GLIBC/lib/*crt* stage1/lib/
 # runtime
 (cd llvm; $CP --parents lib/clang/*/lib/*/{clang_rt.*.o,libclang_rt.builtins*} ../stage1)
 $CP llvm/lib/*/lib{c++,c++abi,unwind}.* $GMP/lib/libgmp.a $LIBUV/lib/libuv.a stage1/lib/
-# bundle OpenSSL static libs
-cp $OPENSSL/lib/libssl.a $OPENSSL/lib/libcrypto.a stage1/lib/
 # LLVM 19 appears to ship the dependencies in 'llvm/lib/<target-triple>/' and 'llvm/include/<target-triple>/'
 # but clang-19 that we use to compile is linked against 'llvm/lib/' and 'llvm/include'
 # https://github.com/llvm/llvm-project/issues/54955
@@ -59,7 +57,6 @@ for f in $GLIBC/lib/{ld,lib{c,dl,m,rt,pthread}}-*; do b=$(basename $f); cp $f st
 OPTIONS=()
 # We build cadical using the custom toolchain on Linux to avoid glibc versioning issues
 echo -n " -DLEAN_STANDALONE=ON -DCADICAL_USE_CUSTOM_CXX=ON"
-echo -n " -DOPENSSL_INCLUDE_DIR=$OPENSSL_DEV/include -DOPENSSL_SSL_LIBRARY=$OPENSSL/lib/libssl.a -DOPENSSL_CRYPTO_LIBRARY=$OPENSSL/lib/libcrypto.a"
 echo -n " -DCMAKE_CXX_COMPILER=$PWD/llvm-host/bin/clang++ -DLEAN_CXX_STDLIB='-Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic'"
 # these should also be used for cadical, so do not use `LEAN_EXTRA_CXX_FLAGS` here
 echo -n " -DCMAKE_CXX_FLAGS='--sysroot $PWD/llvm -idirafter $GLIBC_DEV/include ${EXTRA_FLAGS:-}'"
@@ -77,8 +74,8 @@ fi
 echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang"
 # ld.so is usually included by the libc.so linker script but we discard those. Make sure it is linked to only after `libc.so` like in the original
 # linker script so that no libc symbols are bound to it instead.
-echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--sysroot ROOT -L ROOT/lib -L ROOT/lib/glibc -lc -lc_nonshared -Wl,--as-needed -l:ld.so -Wl,--no-as-needed -lpthread_nonshared -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -lssl -lcrypto -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'"
-# when not using the above flags, link GMP/libuv/OpenSSL dynamically/as usual
-echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-Wl,--as-needed -lgmp -luv -Wl,-Bstatic -lssl -lcrypto -Wl,-Bdynamic -lpthread -ldl -lrt -Wl,--no-as-needed'"
+echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--sysroot ROOT -L ROOT/lib -L ROOT/lib/glibc -lc -lc_nonshared -Wl,--as-needed -l:ld.so -Wl,--no-as-needed -lpthread_nonshared -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'"
+# when not using the above flags, link GMP dynamically/as usual
+echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-Wl,--as-needed -lgmp -luv -lpthread -ldl -lrt -Wl,--no-as-needed'"
 # do not set `LEAN_CC` for tests
 echo -n " -DLEAN_TEST_VARS=''"

script/prepare-llvm-macos.sh

@@ -10,7 +10,6 @@ set -uxo pipefail
 
 GMP=${GMP:-$(brew --prefix)}
 LIBUV=${LIBUV:-$(brew --prefix)}
-OPENSSL=${OPENSSL:-$(brew --prefix openssl@3)}
 
 [[ -d llvm ]] || (mkdir llvm; gtar xf $1 --strip-components 1 --directory llvm)
 [[ -d llvm-host ]] || if [[ "$#" -gt 1 ]]; then
@@ -42,7 +41,6 @@ gcp llvm/lib/libc++.dylib stage1/lib/libc
 # and apparently since Sonoma does not do so implicitly either
 install_name_tool -id /usr/lib/libc++.dylib stage1/lib/libc/libc++.dylib
 echo -n " -DLEAN_STANDALONE=ON"
-echo -n " -DOPENSSL_INCLUDE_DIR=$OPENSSL/include -DOPENSSL_SSL_LIBRARY=$OPENSSL/lib/libssl.a -DOPENSSL_CRYPTO_LIBRARY=$OPENSSL/lib/libcrypto.a"
 # do not change C++ compiler; libc++ etc. being system libraries means there's no danger of conflicts,
 # and the custom clang++ outputs a myriad of warnings when consuming the SDK
 echo -n " -DLEAN_EXTRA_CXX_FLAGS='${EXTRA_FLAGS:-}'"
@@ -50,8 +48,7 @@ if [[ -L llvm-host ]]; then
   echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang"
   gcp $GMP/lib/libgmp.a stage1/lib/
   gcp $LIBUV/lib/libuv.a stage1/lib/
-  gcp $OPENSSL/lib/libssl.a $OPENSSL/lib/libcrypto.a stage1/lib/
-  echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp -luv -lssl -lcrypto'"
+  echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp -luv'"
 else
   echo -n " -DCMAKE_C_COMPILER=$PWD/llvm-host/bin/clang -DLEANC_OPTS='--sysroot $PWD/stage1 -resource-dir $PWD/stage1/lib/clang/15.0.1 ${EXTRA_FLAGS:-}'"
 fi

script/prepare-llvm-mingw.sh

@@ -40,14 +40,14 @@ cp /clang64/lib/{crtbegin,crtend,crt2,dllcrt2}.o stage1/lib/
 # tells the compiler how to dynamically link against `bcrypt.dll` (which is located in the System32 folder).
 # This distinction is relevant specifically for `libicu.a`/`icu.dll` because there we want updates to the time zone database to
 # be delivered to users via Windows Update without having to recompile Lean or Lean programs.
-cp /clang64/lib/lib{m,bcrypt,mingw32,moldname,mingwex,msvcrt,pthread,advapi32,shell32,user32,kernel32,ucrtbase,psapi,iphlpapi,userenv,ws2_32,dbghelp,ole32,icu,crypt32,gdi32}.* /clang64/lib/libgmp.a /clang64/lib/libuv.a /clang64/lib/libssl.a /clang64/lib/libcrypto.a llvm/lib/lib{c++,c++abi,unwind}.a stage1/lib/
+cp /clang64/lib/lib{m,bcrypt,mingw32,moldname,mingwex,msvcrt,pthread,advapi32,shell32,user32,kernel32,ucrtbase,psapi,iphlpapi,userenv,ws2_32,dbghelp,ole32,icu}.* /clang64/lib/libgmp.a /clang64/lib/libuv.a llvm/lib/lib{c++,c++abi,unwind}.a stage1/lib/
 echo -n " -DLEAN_STANDALONE=ON"
 echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang.exe -DCMAKE_C_COMPILER_WORKS=1 -DCMAKE_CXX_COMPILER=$PWD/llvm/bin/clang++.exe -DCMAKE_CXX_COMPILER_WORKS=1 -DLEAN_CXX_STDLIB='-lc++ -lc++abi'"
 echo -n " -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_CXX_COMPILER=clang++"
 echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm -idirafter /clang64/include/'"
 echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang.exe"
-echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--sysroot ROOT -L ROOT/lib -Wl,-Bstatic -lgmp $(pkg-config --static --libs libuv) -lssl -lcrypto -lunwind -Wl,-Bdynamic -lcrypt32 -lgdi32 -fuse-ld=lld'"
-# when not using the above flags, link GMP/libuv/OpenSSL dynamically/as usual. Always link ICU dynamically.
-echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp $(pkg-config --libs libuv) -lssl -lcrypto -lcrypt32 -lgdi32 -lucrtbase'"
+echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--sysroot ROOT -L ROOT/lib -Wl,-Bstatic -lgmp $(pkg-config --static --libs libuv) -lunwind -Wl,-Bdynamic -fuse-ld=lld'"
+# when not using the above flags, link GMP dynamically/as usual. Always link ICU dynamically.
+echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp $(pkg-config --libs libuv) -lucrtbase'"
 # do not set `LEAN_CC` for tests
 echo -n " -DLEAN_TEST_VARS=''"

script/release_repos.yml

@@ -28,6 +28,14 @@ repositories:
     branch: main
     dependencies: []
 
+  - name: leansqlite
+    url: https://github.com/leanprover/leansqlite
+    toolchain-tag: true
+    stable-branch: false
+    branch: main
+    dependencies:
+      - plausible
+
   - name: verso
     url: https://github.com/leanprover/verso
     toolchain-tag: true
@@ -100,7 +108,7 @@ repositories:
     toolchain-tag: true
     stable-branch: false
     branch: main
-    dependencies: [lean4-cli, BibtexQuery, mathlib4]
+    dependencies: [lean4-cli, BibtexQuery, mathlib4, leansqlite]
 
   - name: cslib
     url: https://github.com/leanprover/cslib

script/release_steps.py

@@ -481,11 +481,9 @@ def execute_release_steps(repo, version, config):
         run_command("lake update", cwd=repo_path, stream_output=True)
     elif repo_name == "verso":
         # verso has nested Lake projects in test-projects/ that each have their own
-        # lake-manifest.json with a subverso pin. After updating the root manifest via
-        # `lake update`, sync the de-modulized subverso rev into all sub-manifests.
-        # The sub-projects use an old toolchain (v4.21.0) that doesn't support module/prelude
-        # syntax, so they need the de-modulized version (tagged no-modules/<root-rev>).
-        # The "SubVerso version consistency" CI check accepts either the root or de-modulized rev.
+        # lake-manifest.json with a subverso pin and their own lean-toolchain.
+        # After updating the root manifest via `lake update`, sync the de-modulized
+        # subverso rev into all sub-manifests, and update their lean-toolchain files.
         run_command("lake update", cwd=repo_path, stream_output=True)
         print(blue("Syncing de-modulized subverso rev to test-project sub-manifests..."))
         sync_script = (
@@ -498,6 +496,15 @@ def execute_release_steps(repo, version, config):
         )
         run_command(sync_script, cwd=repo_path)
         print(green("Synced de-modulized subverso rev to all test-project sub-manifests"))
+        # Update all lean-toolchain files in test-projects/ to match the root
+        print(blue("Updating lean-toolchain files in test-projects/..."))
+        find_result = run_command("find test-projects -name lean-toolchain", cwd=repo_path)
+        for tc_path in find_result.stdout.strip().splitlines():
+            if tc_path:
+                tc_file = repo_path / tc_path
+                with open(tc_file, "w") as f:
+                    f.write(f"leanprover/lean4:{version}\n")
+                print(green(f"  Updated {tc_path}"))
     elif dependencies:
         run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path)
         run_command("lake update", cwd=repo_path, stream_output=True)
@@ -659,56 +666,61 @@ def execute_release_steps(repo, version, config):
         # Fetch latest changes to ensure we have the most up-to-date nightly-testing branch
         print(blue("Fetching latest changes from origin..."))
         run_command("git fetch origin", cwd=repo_path)
-        
-        try:
-            print(blue("Merging origin/nightly-testing..."))
-            run_command("git merge origin/nightly-testing", cwd=repo_path)
-            print(green("Merge completed successfully"))
-        except subprocess.CalledProcessError:
-            # Merge failed due to conflicts - check which files are conflicted
-            print(blue("Merge conflicts detected, checking which files are affected..."))
-            
-            # Get conflicted files using git status
-            status_result = run_command("git status --porcelain", cwd=repo_path)
-            conflicted_files = []
-            
-            for line in status_result.stdout.splitlines():
-                if len(line) >= 2 and line[:2] in ['UU', 'AA', 'DD', 'AU', 'UA', 'DU', 'UD']:
-                    # Extract filename (skip the first 3 characters which are status codes)
-                    conflicted_files.append(line[3:])
-            
-            # Filter out allowed files
-            allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
-            problematic_files = []
-            
-            for file in conflicted_files:
-                is_allowed = any(pattern in file for pattern in allowed_patterns)
-                if not is_allowed:
-                    problematic_files.append(file)
-            
-            if problematic_files:
-                # There are conflicts in non-allowed files - fail
-                print(red("❌ Merge failed!"))
-                print(red(f"Merging nightly-testing resulted in conflicts in:"))
-                for file in problematic_files:
-                    print(red(f"  - {file}"))
-                print(red("Please resolve these conflicts manually."))
-                return
-            else:
-                # Only allowed files are conflicted - resolve them automatically
-                print(green(f"✅ Only allowed files conflicted: {', '.join(conflicted_files)}"))
-                print(blue("Resolving conflicts automatically..."))
-                
-                # For lean-toolchain and lake-manifest.json, keep our versions
+
+        # Check if nightly-testing branch exists on origin (use local ref after fetch for exact match)
+        nightly_check = run_command("git show-ref --verify --quiet refs/remotes/origin/nightly-testing", cwd=repo_path, check=False)
+        if nightly_check.returncode != 0:
+            print(yellow("No nightly-testing branch found on origin, skipping merge"))
+        else:
+            try:
+                print(blue("Merging origin/nightly-testing..."))
+                run_command("git merge origin/nightly-testing", cwd=repo_path)
+                print(green("Merge completed successfully"))
+            except subprocess.CalledProcessError:
+                # Merge failed due to conflicts - check which files are conflicted
+                print(blue("Merge conflicts detected, checking which files are affected..."))
+
+                # Get conflicted files using git status
+                status_result = run_command("git status --porcelain", cwd=repo_path)
+                conflicted_files = []
+
+                for line in status_result.stdout.splitlines():
+                    if len(line) >= 2 and line[:2] in ['UU', 'AA', 'DD', 'AU', 'UA', 'DU', 'UD']:
+                        # Extract filename (skip the first 3 characters which are status codes)
+                        conflicted_files.append(line[3:])
+
+                # Filter out allowed files
+                allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
+                problematic_files = []
+
                 for file in conflicted_files:
-                    print(blue(f"Keeping our version of {file}"))
-                    run_command(f"git checkout --ours {file}", cwd=repo_path)
-                
-                # Complete the merge
-                run_command("git add .", cwd=repo_path)
-                run_command("git commit --no-edit", cwd=repo_path)
-                
-                print(green("✅ Merge completed successfully with automatic conflict resolution"))
+                    is_allowed = any(pattern in file for pattern in allowed_patterns)
+                    if not is_allowed:
+                        problematic_files.append(file)
+
+                if problematic_files:
+                    # There are conflicts in non-allowed files - fail
+                    print(red("❌ Merge failed!"))
+                    print(red(f"Merging nightly-testing resulted in conflicts in:"))
+                    for file in problematic_files:
+                        print(red(f"  - {file}"))
+                    print(red("Please resolve these conflicts manually."))
+                    return
+                else:
+                    # Only allowed files are conflicted - resolve them automatically
+                    print(green(f"✅ Only allowed files conflicted: {', '.join(conflicted_files)}"))
+                    print(blue("Resolving conflicts automatically..."))
+
+                    # For lean-toolchain and lake-manifest.json, keep our versions
+                    for file in conflicted_files:
+                        print(blue(f"Keeping our version of {file}"))
+                        run_command(f"git checkout --ours {file}", cwd=repo_path)
+
+                    # Complete the merge
+                    run_command("git add .", cwd=repo_path)
+                    run_command("git commit --no-edit", cwd=repo_path)
+
+                    print(green("✅ Merge completed successfully with automatic conflict resolution"))
 
     # Build and test (skip for Mathlib)
     if repo_name not in ["mathlib4"]:

src/CMakeLists.txt

@@ -116,11 +116,19 @@ option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current ver
 option(USE_LAKE "Use Lake instead of lean.mk for building core libs from language server" ON)
 option(USE_LAKE_CACHE "Use the Lake artifact cache for stage 1 builds (requires USE_LAKE)" OFF)
 
-set(LEAN_EXTRA_MAKE_OPTS "" CACHE STRING "extra options to lean --make")
+set(LEAN_EXTRA_OPTS "" CACHE STRING "extra options to lean (via lake or make)")
+set(LEAN_EXTRA_MAKE_OPTS "" CACHE STRING "extra options to leanmake")
 set(LEANC_CC ${CMAKE_C_COMPILER} CACHE STRING "C compiler to use in `leanc`")
 
 # Temporary, core-only flags. Must be synced with stdlib_flags.h.
-string(APPEND LEAN_EXTRA_MAKE_OPTS " -Dbackward.do.legacy=false")
+string(APPEND LEAN_EXTRA_OPTS " -Dbackward.do.legacy=false")
+
+# option used by the CI to fail on warnings
+option(WFAIL "Fail build if warnings are emitted by Lean" ON)
+if(WFAIL MATCHES "ON")
+  string(APPEND LAKE_EXTRA_ARGS " --wfail")
+  string(APPEND LEAN_EXTRA_MAKE_OPTS " -DwarningAsError=true")
+endif()
 
 if(LAZY_RC MATCHES "ON")
   set(LEAN_LAZY_RC "#define LEAN_LAZY_RC")
@@ -198,7 +206,7 @@ set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/lib/lean")
 
 # OSX default thread stack size is very small. Moreover, in Debug mode, each new stack frame consumes a lot of extra memory.
 if((MULTI_THREAD MATCHES "ON") AND (CMAKE_SYSTEM_NAME MATCHES "Darwin"))
-  string(APPEND LEAN_EXTRA_MAKE_OPTS " -s40000")
+  string(APPEND LEAN_EXTRA_OPTS " -s40000")
 endif()
 
 # We want explicit stack probes in huge Lean stack frames for robust stack overflow detection
@@ -357,28 +365,6 @@ if(NOT LEAN_STANDALONE)
   string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${LIBUV_LDFLAGS}")
 endif()
 
-# OpenSSL
-if(NOT "${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten")
-  find_package(OpenSSL 3 REQUIRED)
-  set(OPENSSL_LIBRARIES ${OPENSSL_SSL_LIBRARY} ${OPENSSL_CRYPTO_LIBRARY})
-  include_directories(${OPENSSL_INCLUDE_DIR})
-  string(JOIN " " OPENSSL_LIBRARIES_STR ${OPENSSL_LIBRARIES})
-  if(NOT LEAN_STANDALONE)
-    string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${OPENSSL_LIBRARIES_STR}")
-  endif()
-endif()
-
-if(CMAKE_SYSTEM_NAME MATCHES "Linux")
-  string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-rpath,\\$$ORIGIN")
-endif()
-
-if(CMAKE_SYSTEM_NAME MATCHES "Windows")
-  string(APPEND LEANSHARED_LINKER_FLAGS " -lcrypt32 -lgdi32")
-  if(NOT LEAN_STANDALONE)
-    string(APPEND LEAN_EXTRA_LINKER_FLAGS " -lcrypt32 -lgdi32")
-  endif()
-endif()
-
 # Windows SDK (for ICU)
 if(CMAKE_SYSTEM_NAME MATCHES "Windows")
   # Pass 'tools' to skip MSVC version check (as MSVC/Visual Studio is not necessarily installed)
@@ -494,17 +480,6 @@ endif()
 string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
 string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
 
-# In standalone (release) builds, OpenSSL must be statically embedded in libleanshared.so.
-# In non-standalone (dev/CI nix) builds, `find_package(OpenSSL)` resolves to shared libs from
-# the nix store. Adding those to libleanshared.so would produce DT_NEEDED entries pointing into
-# the nix store (including transitive libc++.so.1 because nix's libssl is built with libc++).
-# Those paths don't exist in `out/` during `make run-local` tests, breaking them.
-# For non-standalone builds, OpenSSL is instead provided via LEAN_EXTRA_LINKER_FLAGS (leanc.sh)
-# and resolved at runtime from the loading executable.
-if(DEFINED OPENSSL_LIBRARIES_STR AND LEAN_STANDALONE)
-  string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " ${OPENSSL_LIBRARIES_STR}")
-endif()
-
 # in local builds, link executables and not just dynlibs against C++ stdlib as well,
 # which is required for e.g. asan
 if(NOT LEAN_STANDALONE)
@@ -703,6 +678,9 @@ else()
   set(LEAN_PATH_SEPARATOR ":")
 endif()
 
+# inherit genral options for lean.mk.in and stdlib.make.in
+string(APPEND LEAN_EXTRA_MAKE_OPTS " ${LEAN_EXTRA_OPTS}")
+
 # Version
 configure_file("${LEAN_SOURCE_DIR}/version.h.in" "${LEAN_BINARY_DIR}/include/lean/version.h")
 if(STAGE EQUAL 0)
@@ -796,7 +774,7 @@ if(STAGE GREATER 1)
   endif()
 else()
   add_subdirectory(runtime)
-  if("${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten")
+  if(CMAKE_SYSTEM_NAME MATCHES "Emscripten")
     add_dependencies(leanrt libuv)
     add_dependencies(leanrt_initial-exec libuv)
   endif()
@@ -1087,7 +1065,7 @@ string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_CC "${LEANC_CC}")
 string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_INTERNAL_FLAGS "${LEANC_INTERNAL_FLAGS}")
 string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_INTERNAL_LINKER_FLAGS "${LEANC_INTERNAL_LINKER_FLAGS}")
 
-toml_escape("${LEAN_EXTRA_MAKE_OPTS}" LEAN_EXTRA_OPTS_TOML)
+toml_escape("${LEAN_EXTRA_OPTS}" LEAN_EXTRA_OPTS_TOML)
 
 if(CMAKE_BUILD_TYPE MATCHES "Debug|Release|RelWithDebInfo|MinSizeRel")
   set(CMAKE_BUILD_TYPE_TOML "${CMAKE_BUILD_TYPE}")

src/Init/Data/Array/Basic.lean

@@ -1085,6 +1085,17 @@ Examples:
 def sum {α} [Add α] [Zero α] : Array α → α :=
   foldr (· + ·) 0
 
+/--
+Computes the product of the elements of an array.
+
+Examples:
+ * `#[a, b, c].prod = a * (b * (c * 1))`
+ * `#[1, 2, 5].prod = 10`
+-/
+@[inline, expose]
+def prod {α} [Mul α] [One α] : Array α → α :=
+  foldr (· * ·) 1
+
 /--
 Counts the number of elements in the array `as` that satisfy the Boolean predicate `p`.
 

src/Init/Data/Array/Int.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.List.Int.Sum
+public import Init.Data.List.Int.Prod
 public import Init.Data.Array.MinMax
 import Init.Data.Int.Lemmas
 
@@ -74,4 +75,17 @@ theorem sum_div_length_le_max_of_max?_eq_some_int {xs : Array Int} (h : xs.max?
   simpa [List.max?_toArray, List.sum_toArray] using
     List.sum_div_length_le_max_of_max?_eq_some_int (by simpa using h)
 
+@[simp] theorem prod_replicate_int {n : Nat} {a : Int} : (replicate n a).prod = a ^ n := by
+  rw [← List.toArray_replicate, List.prod_toArray]
+  simp
+
+theorem prod_append_int {as₁ as₂ : Array Int} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
+  simp [prod_append]
+
+theorem prod_reverse_int (xs : Array Int) : xs.reverse.prod = xs.prod := by
+  simp [prod_reverse]
+
+theorem prod_eq_foldl_int {xs : Array Int} : xs.prod = xs.foldl (init := 1) (· * ·) := by
+  simp only [foldl_eq_foldr_reverse, Int.mul_comm, ← prod_eq_foldr, prod_reverse_int]
+
 end Array

src/Init/Data/Array/Lemmas.lean

@@ -4380,6 +4380,47 @@ theorem sum_eq_foldl [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
     xs.sum = xs.foldl (init := 0) (· + ·) := by
   simp [← sum_toList, List.sum_eq_foldl]
 
+/-! ### prod -/
+
+@[simp, grind =] theorem prod_empty [Mul α] [One α] : (#[] : Array α).prod = 1 := rfl
+theorem prod_eq_foldr [Mul α] [One α] {xs : Array α} :
+    xs.prod = xs.foldr (init := 1) (· * ·) :=
+  rfl
+
+@[simp, grind =]
+theorem prod_toList [Mul α] [One α] {as : Array α} : as.toList.prod = as.prod := by
+  cases as
+  simp [Array.prod, List.prod]
+
+@[simp, grind =]
+theorem prod_append [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
+    [Std.LawfulLeftIdentity (α := α) (· * ·) 1]
+    {as₁ as₂ : Array α} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
+  simp [← prod_toList, List.prod_append]
+
+@[simp, grind =]
+theorem prod_singleton [Mul α] [One α] [Std.LawfulRightIdentity (· * ·) (1 : α)] {x : α} :
+    #[x].prod = x := by
+  simp [Array.prod_eq_foldr, Std.LawfulRightIdentity.right_id x]
+
+@[simp, grind =]
+theorem prod_push [Mul α] [One α] [Std.Associative (α := α) (· * ·)]
+    [Std.LawfulIdentity (· * ·) (1 : α)] {xs : Array α} {x : α} :
+    (xs.push x).prod = xs.prod * x := by
+  simp [Array.prod_eq_foldr, Std.LawfulRightIdentity.right_id, Std.LawfulLeftIdentity.left_id,
+    ← Array.foldr_assoc]
+
+@[simp, grind =]
+theorem prod_reverse [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
+    [Std.Commutative (α := α) (· * ·)]
+    [Std.LawfulLeftIdentity (α := α) (· * ·) 1] (xs : Array α) : xs.reverse.prod = xs.prod := by
+  simp [← prod_toList, List.prod_reverse]
+
+theorem prod_eq_foldl [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
+    [Std.LawfulIdentity (· * ·) (1 : α)] {xs : Array α} :
+    xs.prod = xs.foldl (init := 1) (· * ·) := by
+  simp [← prod_toList, List.prod_eq_foldl]
+
 theorem foldl_toList_eq_flatMap {l : List α} {acc : Array β}
     {F : Array β → α → Array β} {G : α → List β}
     (H : ∀ acc a, (F acc a).toList = acc.toList ++ G a) :

src/Init/Data/Array/Nat.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Init.Data.Array.MinMax
 import Init.Data.List.Nat.Sum
+import Init.Data.List.Nat.Prod
 import Init.Data.Array.Lemmas
 
 public section
@@ -81,4 +82,24 @@ theorem sum_div_length_le_max_of_max?_eq_some_nat {xs : Array Nat} (h : xs.max?
   simpa [List.max?_toArray, List.sum_toArray] using
     List.sum_div_length_le_max_of_max?_eq_some_nat (by simpa using h)
 
+protected theorem prod_pos_iff_forall_pos_nat {xs : Array Nat} : 0 < xs.prod ↔ ∀ x ∈ xs, 0 < x := by
+  simp [← prod_toList, List.prod_pos_iff_forall_pos_nat]
+
+protected theorem prod_eq_zero_iff_exists_zero_nat {xs : Array Nat} :
+    xs.prod = 0 ↔ ∃ x ∈ xs, x = 0 := by
+  simp [← prod_toList, List.prod_eq_zero_iff_exists_zero_nat]
+
+@[simp] theorem prod_replicate_nat {n : Nat} {a : Nat} : (replicate n a).prod = a ^ n := by
+  rw [← List.toArray_replicate, List.prod_toArray]
+  simp
+
+theorem prod_append_nat {as₁ as₂ : Array Nat} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
+  simp [prod_append]
+
+theorem prod_reverse_nat (xs : Array Nat) : xs.reverse.prod = xs.prod := by
+  simp [prod_reverse]
+
+theorem prod_eq_foldl_nat {xs : Array Nat} : xs.prod = xs.foldl (init := 1) (· * ·) := by
+  simp only [foldl_eq_foldr_reverse, Nat.mul_comm, ← prod_eq_foldr, prod_reverse_nat]
+
 end Array

src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean

@@ -271,7 +271,7 @@ private def optionPelim' {α : Type u_1} (t : Option α) {β :  Sort u_2}
 
 /--
 Inserts an `Option` case distinction after the first computation of a call to `MonadAttach.pbind`.
-This lemma is useful for simplifying the second computation, which often involes `match` expressions
+This lemma is useful for simplifying the second computation, which often involves `match` expressions
 that use `pbind`'s proof term.
 -/
 private theorem pbind_eq_pbind_if_isSome [Monad m] [MonadAttach m] (x : m (Option α)) (f : (_ : _) → _ → m β) :

src/Init/Data/List/Basic.lean

@@ -2056,6 +2056,20 @@ def sum {α} [Add α] [Zero α] : List α → α :=
 @[simp, grind =] theorem sum_cons [Add α] [Zero α] {a : α} {l : List α} : (a::l).sum = a + l.sum := rfl
 theorem sum_eq_foldr [Add α] [Zero α] {l : List α} : l.sum = l.foldr (· + ·) 0 := rfl
 
+/--
+Computes the product of the elements of a list.
+
+Examples:
+ * `[a, b, c].prod = a * (b * (c * 1))`
+ * `[1, 2, 5].prod = 10`
+-/
+def prod {α} [Mul α] [One α] : List α → α :=
+  foldr (· * ·) 1
+
+@[simp, grind =] theorem prod_nil [Mul α] [One α] : ([] : List α).prod = 1 := rfl
+@[simp, grind =] theorem prod_cons [Mul α] [One α] {a : α} {l : List α} : (a::l).prod = a * l.prod := rfl
+theorem prod_eq_foldr [Mul α] [One α] {l : List α} : l.prod = l.foldr (· * ·) 1 := rfl
+
 /-! ### range -/
 
 /--

src/Init/Data/List/Int.lean

@@ -7,3 +7,4 @@ module
 
 prelude
 public import Init.Data.List.Int.Sum
+public import Init.Data.List.Int.Prod

src/Init/Data/List/Int/Prod.lean

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+import Init.Data.List.Lemmas
+import Init.Data.Int.Lemmas
+public import Init.Data.Int.Pow
+public import Init.Data.List.Basic
+
+public section
+
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
+namespace List
+
+@[simp]
+theorem prod_replicate_int {n : Nat} {a : Int} : (replicate n a).prod = a ^ n := by
+  induction n <;> simp_all [replicate_succ, Int.pow_succ, Int.mul_comm]
+
+theorem prod_append_int {l₁ l₂ : List Int} : (l₁ ++ l₂).prod = l₁.prod * l₂.prod := by
+  simp [prod_append]
+
+theorem prod_reverse_int (xs : List Int) : xs.reverse.prod = xs.prod := by
+  simp [prod_reverse]
+
+end List

src/Init/Data/List/Lemmas.lean

@@ -1878,6 +1878,24 @@ theorem sum_reverse [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
     simp_all [sum_append, Std.Commutative.comm (α := α) _ 0,
       Std.LawfulLeftIdentity.left_id, Std.Commutative.comm]
 
+@[simp, grind =]
+theorem prod_append [Mul α] [One α] [Std.LawfulLeftIdentity (α := α) (· * ·) 1]
+    [Std.Associative (α := α) (· * ·)] {l₁ l₂ : List α} : (l₁ ++ l₂).prod = l₁.prod * l₂.prod := by
+  induction l₁ generalizing l₂ <;> simp_all [Std.Associative.assoc, Std.LawfulLeftIdentity.left_id]
+
+@[simp, grind =]
+theorem prod_singleton [Mul α] [One α] [Std.LawfulRightIdentity (· * ·) (1 : α)] {x : α} :
+    [x].prod = x := by
+  simp [List.prod_eq_foldr, Std.LawfulRightIdentity.right_id x]
+
+@[simp, grind =]
+theorem prod_reverse [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
+    [Std.Commutative (α := α) (· * ·)]
+    [Std.LawfulLeftIdentity (α := α) (· * ·) 1] (xs : List α) : xs.reverse.prod = xs.prod := by
+  induction xs <;>
+    simp_all [prod_append, Std.Commutative.comm (α := α) _ 1,
+      Std.LawfulLeftIdentity.left_id, Std.Commutative.comm]
+
 /-! ### concat
 
 Note that `concat_eq_append` is a `@[simp]` lemma, so `concat` should usually not appear in goals.
@@ -2784,6 +2802,11 @@ theorem sum_eq_foldl [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
     xs.sum = xs.foldl (init := 0) (· + ·) := by
   simp [sum_eq_foldr, foldl_eq_apply_foldr, Std.LawfulLeftIdentity.left_id]
 
+theorem prod_eq_foldl [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
+    [Std.LawfulIdentity (· * ·) (1 : α)] {xs : List α} :
+    xs.prod = xs.foldl (init := 1) (· * ·) := by
+  simp [prod_eq_foldr, foldl_eq_apply_foldr, Std.LawfulLeftIdentity.left_id]
+
 -- The argument `f : α₁ → α₂` is intentionally explicit, as it is sometimes not found by unification.
 theorem foldl_hom (f : α₁ → α₂) {g₁ : α₁ → β → α₁} {g₂ : α₂ → β → α₂} {l : List β} {init : α₁}
     (H : ∀ x y, g₂ (f x) y = f (g₁ x y)) : l.foldl g₂ (f init) = f (l.foldl g₁ init) := by

src/Init/Data/List/Nat.lean

@@ -13,6 +13,7 @@ public import Init.Data.List.Nat.Sublist
 public import Init.Data.List.Nat.TakeDrop
 public import Init.Data.List.Nat.Count
 public import Init.Data.List.Nat.Sum
+public import Init.Data.List.Nat.Prod
 public import Init.Data.List.Nat.Erase
 public import Init.Data.List.Nat.Find
 public import Init.Data.List.Nat.BEq

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

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+import Init.Data.List.Lemmas
+public import Init.BinderPredicates
+public import Init.NotationExtra
+import Init.Data.Nat.Lemmas
+
+public section
+
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
+namespace List
+
+protected theorem prod_eq_zero_iff_exists_zero_nat {l : List Nat} : l.prod = 0 ↔ ∃ x ∈ l, x = 0 := by
+  induction l with
+  | nil => simp
+  | cons x xs ih =>
+    simp [Nat.mul_eq_zero, ih, eq_comm (a := (0 : Nat))]
+
+protected theorem prod_pos_iff_forall_pos_nat {l : List Nat} : 0 < l.prod ↔ ∀ x ∈ l, 0 < x := by
+  induction l with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [prod_cons, mem_cons, forall_eq_or_imp, ← ih]
+    constructor
+    · intro h
+      exact ⟨Nat.pos_of_mul_pos_right h, Nat.pos_of_mul_pos_left h⟩
+    · exact fun ⟨hx, hxs⟩ => Nat.mul_pos hx hxs
+
+@[simp]
+theorem prod_replicate_nat {n : Nat} {a : Nat} : (replicate n a).prod = a ^ n := by
+  induction n <;> simp_all [replicate_succ, Nat.pow_succ, Nat.mul_comm]
+
+theorem prod_append_nat {l₁ l₂ : List Nat} : (l₁ ++ l₂).prod = l₁.prod * l₂.prod := by
+  simp [prod_append]
+
+theorem prod_reverse_nat (xs : List Nat) : xs.reverse.prod = xs.prod := by
+  simp [prod_reverse]
+
+theorem prod_eq_foldl_nat {xs : List Nat} : xs.prod = xs.foldl (init := 1) (· * ·) := by
+  simp only [foldl_eq_foldr_reverse, Nat.mul_comm, ← prod_eq_foldr, prod_reverse_nat]
+
+end List

src/Init/Data/List/Perm.lean

@@ -606,6 +606,13 @@ theorem sum_nat {l₁ l₂ : List Nat} (h : l₁ ~ l₂) : l₁.sum = l₂.sum :
   | swap => simpa [List.sum_cons] using Nat.add_left_comm ..
   | trans _ _ ih₁ ih₂ => simp [ih₁, ih₂]
 
+theorem prod_nat {l₁ l₂ : List Nat} (h : l₁ ~ l₂) : l₁.prod = l₂.prod := by
+  induction h with
+  | nil => simp
+  | cons _ _ ih => simp [ih]
+  | swap => simpa [List.prod_cons] using Nat.mul_left_comm ..
+  | trans _ _ ih₁ ih₂ => simp [ih₁, ih₂]
+
 theorem all_eq {l₁ l₂ : List α} {f : α → Bool} (hp : l₁.Perm l₂) : l₁.all f = l₂.all f := by
   rw [Bool.eq_iff_iff]; simp [hp.mem_iff]
 
@@ -615,6 +622,9 @@ theorem any_eq {l₁ l₂ : List α} {f : α → Bool} (hp : l₁.Perm l₂) : l
 grind_pattern Perm.sum_nat => l₁ ~ l₂, l₁.sum
 grind_pattern Perm.sum_nat => l₁ ~ l₂, l₂.sum
 
+grind_pattern Perm.prod_nat => l₁ ~ l₂, l₁.prod
+grind_pattern Perm.prod_nat => l₁ ~ l₂, l₂.prod
+
 end Perm
 
 end List

src/Init/Data/List/ToArray.lean

@@ -213,6 +213,9 @@ theorem forM_toArray [Monad m] (l : List α) (f : α → m PUnit) :
 @[simp, grind =] theorem sum_toArray [Add α] [Zero α] (l : List α) : l.toArray.sum = l.sum := by
   simp [Array.sum, List.sum]
 
+@[simp, grind =] theorem prod_toArray [Mul α] [One α] (l : List α) : l.toArray.prod = l.prod := by
+  simp [Array.prod, List.prod]
+
 @[simp, grind =] theorem append_toArray (l₁ l₂ : List α) :
     l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
   apply ext'

src/Init/Data/Nat/Gcd.lean

@@ -60,7 +60,7 @@ theorem gcd_def (x y : Nat) : gcd x y = if x = 0 then y else gcd (y % x) x := by
   cases n with
   | zero => simp
   | succ n =>
-    -- `simp [gcd_succ]` produces an invalid term unless `gcd_succ` is proved with `id rfl` instead
+    -- `simp [gcd_succ]` produces an invalid term unless `gcd_succ` is proved with `(rfl)` instead
     rw [gcd_succ]
     exact gcd_zero_left _
 instance : Std.LawfulIdentity gcd 0 where

src/Init/Data/Range/Polymorphic/NatLemmas.lean

@@ -1718,7 +1718,7 @@ theorem toArray_roc_append_toArray_roc {l m n : Nat} (h : l ≤ m) (h' : m ≤ n
 @[simp]
 theorem getElem_toArray_roc {m n i : Nat} (_h : i < (m<...=n).toArray.size) :
     (m<...=n).toArray[i]'_h = m + 1 + i := by
-simp [toArray_roc_eq_toArray_rco]
+  simp [toArray_roc_eq_toArray_rco]
 
 theorem getElem?_toArray_roc {m n i : Nat} :
     (m<...=n).toArray[i]? = if i < n - m then some (m + 1 + i) else none := by

src/Init/Data/String/Decode.lean

@@ -363,7 +363,7 @@ theorem toBitVec_eq_of_parseFirstByte_eq_threeMore {b : UInt8} (h : parseFirstBy
 public def isInvalidContinuationByte (b : UInt8) : Bool :=
   b &&& 0xc0 != 0x80
 
-theorem isInvalidContinutationByte_eq_false_iff {b : UInt8} :
+theorem isInvalidContinuationByte_eq_false_iff {b : UInt8} :
     isInvalidContinuationByte b = false ↔ b &&& 0xc0 = 0x80 := by
   simp [isInvalidContinuationByte]
 

src/Init/Data/String/Lemmas/Iterate.lean

@@ -31,7 +31,7 @@ namespace Slice
 /--
 A list of all positions starting at {name}`p`.
 
-This function is not meant to be used in actual progams. Actual programs should use
+This function is not meant to be used in actual programs. Actual programs should use
 {name}`Slice.positionsFrom` or {name}`Slice.positions`.
 -/
 protected def Model.positionsFrom {s : Slice} (p : s.Pos) : List { p : s.Pos // p ≠ s.endPos } :=
@@ -206,7 +206,7 @@ end Slice
 /--
 A list of all positions starting at {name}`p`.
 
-This function is not meant to be used in actual progams. Actual programs should use
+This function is not meant to be used in actual programs. Actual programs should use
 {name}`Slice.positionsFrom` or {name}`Slice.positions`.
 -/
 protected def Model.positionsFrom {s : String} (p : s.Pos) : List { p : s.Pos // p ≠ s.endPos } :=

src/Init/Data/String/Subslice.lean

@@ -23,7 +23,7 @@ Given a {name}`Slice` {name}`s`, the type {lean}`s.Subslice` is the type of half
 in {name}`s` delineated by a valid position on both sides.
 
 This type is useful to track regions of interest within some larger slice that is also of interest.
-In contrast, {name}`Slice` is used to track regions of interest whithin some larger string that is
+In contrast, {name}`Slice` is used to track regions of interest within some larger string that is
 not or no longer relevant.
 
 Equality on {name}`Subslice` is somewhat better behaved than on {name}`Slice`, but note that there

src/Init/Data/Vector/Basic.lean

@@ -506,6 +506,16 @@ Examples:
 @[inline, expose] def sum [Add α] [Zero α] (xs : Vector α n) : α :=
   xs.toArray.sum
 
+/--
+Computes the product of the elements of a vector.
+
+Examples:
+ * `#v[a, b, c].prod = a * (b * (c * 1))`
+ * `#v[1, 2, 5].prod = 10`
+-/
+@[inline, expose] def prod [Mul α] [One α] (xs : Vector α n) : α :=
+  xs.toArray.prod
+
 /--
 Pad a vector on the left with a given element.
 

src/Init/Data/Vector/Int.lean

@@ -30,4 +30,16 @@ theorem sum_reverse_int (xs : Vector Int n) : xs.reverse.sum = xs.sum := by
 theorem sum_eq_foldl_int {xs : Vector Int n} : xs.sum = xs.foldl (b := 0) (· + ·) := by
   simp only [foldl_eq_foldr_reverse, Int.add_comm, ← sum_eq_foldr, sum_reverse_int]
 
+@[simp] theorem prod_replicate_int {n : Nat} {a : Int} : (replicate n a).prod = a ^ n := by
+  simp [← prod_toArray, Array.prod_replicate_int]
+
+theorem prod_append_int {as₁ as₂ : Vector Int n} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
+  simp [← prod_toArray]
+
+theorem prod_reverse_int (xs : Vector Int n) : xs.reverse.prod = xs.prod := by
+  simp [prod_reverse]
+
+theorem prod_eq_foldl_int {xs : Vector Int n} : xs.prod = xs.foldl (b := 1) (· * ·) := by
+  simp only [foldl_eq_foldr_reverse, Int.mul_comm, ← prod_eq_foldr, prod_reverse_int]
+
 end Vector

src/Init/Data/Vector/Lemmas.lean

@@ -278,6 +278,12 @@ theorem toArray_mk {xs : Array α} (h : xs.size = n) : (Vector.mk xs h).toArray
 @[simp, grind =] theorem sum_toArray [Add α] [Zero α] {xs : Vector α n} :
     xs.toArray.sum = xs.sum := rfl
 
+@[simp] theorem prod_mk [Mul α] [One α] {xs : Array α} (h : xs.size = n) :
+    (Vector.mk xs h).prod = xs.prod := rfl
+
+@[simp, grind =] theorem prod_toArray [Mul α] [One α] {xs : Vector α n} :
+    xs.toArray.prod = xs.prod := rfl
+
 @[simp] theorem eq_mk : xs = Vector.mk as h ↔ xs.toArray = as := by
   cases xs
   simp
@@ -551,6 +557,10 @@ theorem toArray_toList {xs : Vector α n} : xs.toList.toArray = xs.toArray := rf
     xs.toList.sum = xs.sum := by
   rw [← toList_toArray, Array.sum_toList, sum_toArray]
 
+@[simp, grind =] theorem prod_toList [Mul α] [One α] {xs : Vector α n} :
+    xs.toList.prod = xs.prod := by
+  rw [← toList_toArray, Array.prod_toList, prod_toArray]
+
 @[simp] theorem getElem_toList {xs : Vector α n} {i : Nat} (h : i < xs.toList.length) :
     xs.toList[i] = xs[i]'(by simpa using h) := by
   cases xs
@@ -3134,3 +3144,39 @@ theorem sum_eq_foldl [Zero α] [Add α]
     {xs : Vector α n} :
     xs.sum = xs.foldl (b := 0) (· + ·) := by
   simp [← sum_toList, List.sum_eq_foldl]
+
+/-! ### prod -/
+
+@[simp, grind =] theorem prod_empty [Mul α] [One α] : (#v[] : Vector α 0).prod = 1 := rfl
+theorem prod_eq_foldr [Mul α] [One α] {xs : Vector α n} :
+    xs.prod = xs.foldr (b := 1) (· * ·) :=
+  rfl
+
+@[simp, grind =]
+theorem prod_append [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
+    [Std.LeftIdentity (α := α) (· * ·) 1] [Std.LawfulLeftIdentity (α := α) (· * ·) 1]
+    {as₁ as₂ : Vector α n} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
+  simp [← prod_toList, List.prod_append]
+
+@[simp, grind =]
+theorem prod_singleton [Mul α] [One α] [Std.LawfulRightIdentity (· * ·) (1 : α)] {x : α} :
+    #v[x].prod = x := by
+  simp [← prod_toList, Std.LawfulRightIdentity.right_id x]
+
+@[simp, grind =]
+theorem prod_push [Mul α] [One α] [Std.Associative (α := α) (· * ·)]
+    [Std.LawfulIdentity (· * ·) (1 : α)] {xs : Vector α n} {x : α} :
+    (xs.push x).prod = xs.prod * x := by
+  simp [← prod_toArray]
+
+@[simp, grind =]
+theorem prod_reverse [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
+    [Std.Commutative (α := α) (· * ·)]
+    [Std.LawfulLeftIdentity (α := α) (· * ·) 1] (xs : Vector α n) : xs.reverse.prod = xs.prod := by
+  simp [← prod_toList, List.prod_reverse]
+
+theorem prod_eq_foldl [One α] [Mul α]
+    [Std.Associative (α := α) (· * ·)] [Std.LawfulIdentity (· * ·) (1 : α)]
+    {xs : Vector α n} :
+    xs.prod = xs.foldl (b := 1) (· * ·) := by
+  simp [← prod_toList, List.prod_eq_foldl]

src/Init/Data/Vector/Nat.lean

@@ -37,4 +37,23 @@ theorem sum_reverse_nat (xs : Vector Nat n) : xs.reverse.sum = xs.sum := by
 theorem sum_eq_foldl_nat {xs : Vector Nat n} : xs.sum = xs.foldl (b := 0) (· + ·) := by
   simp only [foldl_eq_foldr_reverse, Nat.add_comm, ← sum_eq_foldr, sum_reverse_nat]
 
+protected theorem prod_pos_iff_forall_pos_nat {xs : Vector Nat n} : 0 < xs.prod ↔ ∀ x ∈ xs, 0 < x := by
+  simp [← prod_toArray, Array.prod_pos_iff_forall_pos_nat]
+
+protected theorem prod_eq_zero_iff_exists_zero_nat {xs : Vector Nat n} :
+    xs.prod = 0 ↔ ∃ x ∈ xs, x = 0 := by
+  simp [← prod_toArray, Array.prod_eq_zero_iff_exists_zero_nat]
+
+@[simp] theorem prod_replicate_nat {n : Nat} {a : Nat} : (replicate n a).prod = a ^ n := by
+  simp [← prod_toArray, Array.prod_replicate_nat]
+
+theorem prod_append_nat {as₁ as₂ : Vector Nat n} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
+  simp [← prod_toArray]
+
+theorem prod_reverse_nat (xs : Vector Nat n) : xs.reverse.prod = xs.prod := by
+  simp [prod_reverse]
+
+theorem prod_eq_foldl_nat {xs : Vector Nat n} : xs.prod = xs.foldl (b := 1) (· * ·) := by
+  simp only [foldl_eq_foldr_reverse, Nat.mul_comm, ← prod_eq_foldr, prod_reverse_nat]
+
 end Vector

src/Init/Grind/Ring/Basic.lean

@@ -564,6 +564,28 @@ end Ring
 
 end IsCharP
 
+/--
+`PowIdentity α p` states that `x ^ p = x` holds for all elements of `α`.
+
+The primary source of instances is Fermat's little theorem: for a finite field with `q` elements,
+`x ^ q = x` for every `x`. For `Fin p` or `ZMod p` with prime `p`, this gives `x ^ p = x`.
+
+The `grind` ring solver uses this typeclass to add the relation `x ^ p - x = 0` to the
+Groebner basis, which allows it to reduce high-degree polynomials. Mathlib can provide
+instances for general finite fields via `FiniteField.pow_card`.
+-/
+class PowIdentity (α : Type u) [CommSemiring α] (p : outParam Nat) : Prop where
+  /-- Every element satisfies `x ^ p = x`. -/
+  pow_eq (x : α) : x ^ p = x
+
+namespace PowIdentity
+
+variable [CommSemiring α] [PowIdentity α p]
+
+theorem pow (x : α) : x ^ p = x := pow_eq x
+
+end PowIdentity
+
 open AddCommGroup
 
 theorem no_int_zero_divisors {α : Type u} [IntModule α] [NoNatZeroDivisors α] {k : Int} {a : α}

src/Init/Grind/Ring/Envelope.lean

@@ -193,7 +193,7 @@ theorem mul_assoc (a b c : Q α) : mul (mul a b) c = mul a (mul b c) := by
   simp [Semiring.left_distrib, Semiring.right_distrib]; refine ⟨0, ?_⟩; ac_rfl
 
 theorem mul_one (a : Q α) : mul a (natCast 1) = a := by
-obtain ⟨⟨_, _⟩⟩ := a; simp
+  obtain ⟨⟨_, _⟩⟩ := a; simp
 
 theorem one_mul (a : Q α) : mul (natCast 1) a = a := by
   obtain ⟨⟨_, _⟩⟩ := a; simp

src/Init/GrindInstances/Ring/Fin.lean

@@ -156,6 +156,12 @@ instance [i : NeZero n] : ToInt.Pow (Fin n) (.co 0 n) where
       rw [pow_succ, ToInt.Mul.toInt_mul, ih, ← ToInt.wrap_toInt,
         ← IntInterval.wrap_mul (by simp), Int.pow_succ, ToInt.wrap_toInt]
 
+instance : PowIdentity (Fin 2) 2 where
+  pow_eq x := by
+    match x with
+    | ⟨0, _⟩ => rfl
+    | ⟨1, _⟩ => rfl
+
 end Fin
 
 end Lean.Grind

src/Init/Prelude.lean

@@ -145,7 +145,7 @@ Examples:
 The constant function that ignores its argument.
 
 If `a : α`, then `Function.const β a : β → α` is the “constant function with value `a`”. For all
-arguments `b : β`, `Function.const β a b = a`.
+arguments `b : β`, `Function.const β a b = a`. It is often written directly as `fun _ => a`.
 
 Examples:
  * `Function.const Bool 10 true = 10`
@@ -3754,7 +3754,7 @@ class Functor (f : Type u → Type v) : Type (max (u+1) v) where
   /--
   Mapping a constant function.
 
-  Given `a : α` and `v : f α`, `mapConst a v` is equivalent to `Function.const _ a <$> v`. For some
+  Given `a : α` and `v : f β`, `mapConst a v` is equivalent to `(fun _ => a) <$> v`. For some
   functors, this can be implemented more efficiently; for all other functors, the default
   implementation may be used.
   -/

src/Init/System/IO.lean

@@ -1880,3 +1880,12 @@ lead to undefined behavior.
 -/
 @[extern "lean_runtime_forget"]
 def Runtime.forget (a : α) : BaseIO Unit := return
+
+set_option linter.unusedVariables false in
+/--
+Ensures `a` remains at least alive until the call site by holding a reference to `a`. This can be useful
+for unsafe code (such as an FFI) that relies on a Lean object not being freed until after some point
+in the program. At runtime, this will be a no-op as the C compiler will optimize away this call.
+-/
+@[extern "lean_runtime_hold"]
+def Runtime.hold (a : @& α) : BaseIO Unit := return

src/Lean/AddDecl.lean

@@ -9,6 +9,7 @@ prelude
 public import Lean.Meta.Sorry
 public import Lean.Util.CollectAxioms
 public import Lean.OriginalConstKind
+import Lean.Compiler.MetaAttr
 import all Lean.OriginalConstKind  -- for accessing `privateConstKindsExt`
 
 public section
@@ -208,8 +209,12 @@ where
       catch _ => pure ()
 
 
-def addAndCompile (decl : Declaration) (logCompileErrors : Bool := true) : CoreM Unit := do
+def addAndCompile (decl : Declaration) (logCompileErrors : Bool := true)
+    (markMeta : Bool := false) : CoreM Unit := do
   addDecl decl
+  if markMeta then
+    for n in decl.getNames do
+      modifyEnv (Lean.markMeta · n)
   compileDecl decl (logErrors := logCompileErrors)
 
 end Lean

src/Lean/Compiler/LCNF/InferBorrow.lean

@@ -67,7 +67,7 @@ structure ParamMap where
   The set of fvars that were already annotated as borrowed before arriving at this pass. We try to
   preserve the annotations here if possible.
   -/
-  annoatedBorrows : Std.HashSet FVarId := {}
+  annotatedBorrows : Std.HashSet FVarId := {}
 
 namespace ParamMap
 
@@ -95,7 +95,7 @@ where
         modify fun m =>
           { m with
             map := m.map.insert (.decl decl.name) (initParamsIfNotExported exported decl.params),
-            annoatedBorrows := decl.params.foldl (init := m.annoatedBorrows) fun acc p =>
+            annotatedBorrows := decl.params.foldl (init := m.annotatedBorrows) fun acc p =>
               if p.borrow then acc.insert p.fvarId else acc
           }
         goCode decl.name code
@@ -116,7 +116,7 @@ where
       modify fun m =>
         { m with
           map := m.map.insert (.jp declName decl.fvarId) (initParams decl.params),
-          annoatedBorrows := decl.params.foldl (init := m.annoatedBorrows) fun acc p =>
+          annotatedBorrows := decl.params.foldl (init := m.annotatedBorrows) fun acc p =>
             if p.borrow then acc.insert p.fvarId else acc
         }
       goCode declName decl.value
@@ -286,7 +286,7 @@ where
 
   ownFVar (fvarId : FVarId) (reason : OwnReason) : InferM Unit := do
     unless (← get).owned.contains fvarId do
-      if !reason.isForced && (← get).paramMap.annoatedBorrows.contains fvarId then
+      if !reason.isForced && (← get).paramMap.annotatedBorrows.contains fvarId then
         trace[Compiler.inferBorrow] "user annotation blocked owning {← PP.run <| PP.ppFVar fvarId}: {← reason.toString}"
       else
         trace[Compiler.inferBorrow] "own {← PP.run <| PP.ppFVar fvarId}: {← reason.toString}"

src/Lean/Compiler/LCNF/PassManager.lean

@@ -121,7 +121,7 @@ def mkPerDeclaration (name : Name) (phase : Phase)
   occurrence := occurrence
   phase := phase
   name := name
-  run := fun xs => xs.mapM run
+  run := fun xs => xs.mapM fun decl => do checkSystem "LCNF compiler"; run decl
 
 end Pass
 

src/Lean/Compiler/LCNF/ResetReuse.lean

@@ -28,7 +28,7 @@ inserts addition instructions to attempt to reuse the memory right away instead
 allocator.
 
 For this the paper defines three functions:
-- `R` (called `Decl.insertResetReuse` here) which looks for candidates that might be elligible for
+- `R` (called `Decl.insertResetReuse` here) which looks for candidates that might be eligible for
   reuse. For these variables it invokes `D`.
 - `D` which looks for code regions in which the target variable is dead (i.e. no longer read from),
   it then invokes `S`. If `S` succeeds it inserts a `reset` instruction to match the `reuse`

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

@@ -217,6 +217,8 @@ Simplify `code`
 -/
 partial def simp (code : Code .pure) : SimpM (Code .pure) := withIncRecDepth do
   incVisited
+  if (← get).visited % 128 == 0 then
+    checkSystem "LCNF simp"
   match code with
   | .let decl k =>
     let baseDecl := decl

src/Lean/Compiler/LCNF/SimpCase.lean

@@ -24,7 +24,7 @@ In particular we perform:
 - folding of the most common cases arm into the default arm if possible
 
 Note: Currently the simplifier still contains almost equivalent simplifications to the ones shown
-here. We know that this causes unforseen behavior and do plan on changing it eventually.
+here. We know that this causes unforeseen behavior and do plan on changing it eventually.
 -/
 
 -- TODO: the following functions are duplicated from simp and should be deleted in simp once we

src/Lean/Compiler/LCNF/ToDecl.lean

@@ -171,7 +171,7 @@ def toDecl (declName : Name) : CompilerM (Decl .pure) := do
     if compiler.ignoreBorrowAnnotation.get (← getOptions) then
       decl := { decl with params := ← decl.params.mapM (·.updateBorrow false) }
     if isExport env decl.name && decl.params.any (·.borrow) then
-      throwError m!" Declaration {decl.name} is marked as `export` but some of its parameters have borrow annotations.\n Consider using `set_option compiler.ignoreBorrowAnnotation true in` to supress the borrow annotations in its type.\n If the declaration is part of an `export`/`extern` pair make sure to also supress the annotations at the `extern` declaration."
+      throwError m!" Declaration {decl.name} is marked as `export` but some of its parameters have borrow annotations.\n Consider using `set_option compiler.ignoreBorrowAnnotation true in` to suppress the borrow annotations in its type.\n If the declaration is part of an `export`/`extern` pair make sure to also suppress the annotations at the `extern` declaration."
     return decl
 
 end Lean.Compiler.LCNF

src/Lean/CoreM.lean

@@ -20,6 +20,8 @@ register_builtin_option diagnostics : Bool := {
   descr    := "collect diagnostic information"
 }
 
+builtin_initialize registerTraceClass `diagnostics
+
 register_builtin_option diagnostics.threshold : Nat := {
   defValue := 20
   descr    := "only diagnostic counters above this threshold are reported by the definitional equality"
@@ -444,10 +446,6 @@ Note that the value of `ctx.initHeartbeats` is ignored and replaced with `IO.get
 @[inline] def CoreM.toIO' (x : CoreM α) (ctx : Context) (s : State) : IO α :=
   (·.1) <$> x.toIO ctx s
 
-/-- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`. -/
-protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m α :=
-  controlAt CoreM fun runInBase => withIncRecDepth (runInBase x)
-
 /--
 Throws an internal interrupt exception if cancellation has been requested. The exception is not
 caught by `try catch` but is intended to be caught by `Command.withLoggingExceptions` at the top
@@ -462,6 +460,12 @@ heartbeat tracking (e.g. `SynthInstance`).
     if (← tk.isSet) then
       throwInterruptException
 
+/-- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`.
+Also checks for cancellation, so that recursive elaboration functions
+(inferType, whnf, isDefEq, …) respond promptly to interrupt requests. -/
+protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m α :=
+  controlAt CoreM fun runInBase => do checkInterrupted; withIncRecDepth (runInBase x)
+
 register_builtin_option debug.moduleNameAtTimeout : Bool := {
   defValue := true
   descr    := "include module name in deterministic timeout error messages.\nRemark: we set this option to false to increase the stability of our test suite"

src/Lean/Elab/BuiltinDo/For.lean

@@ -111,8 +111,14 @@ open Lean.Meta
     for x in loopMutVars do
       let defn ← getLocalDeclFromUserName x.getId
       Term.addTermInfo' x defn.toExpr
-      -- ForIn forces all mut vars into the same universe: that of the do block result type.
-      discard <| Term.ensureHasType (mkSort (mi.u.succ)) defn.type
+      -- ForIn forces the mut tuple into the universe mi.u: that of the do block result type.
+      -- If we don't do this, then we are stuck on solving constraints such as
+      --   `max ?u.46 ?u.47 =?= max (max ?u.22 ?u.46) ?u.47`
+      -- It's important we do this as a separate isLevelDefEq check on the decremented level because
+      -- otherwise (`ensureHasType (mkSort mi.u.succ)`) we are stuck on constraints like
+      --   `max (?u+1) (?v+1) =?= ?u+1`
+      let u ← getDecLevel defn.type
+      discard <| isLevelDefEq u mi.u
       defs := defs.push defn.toExpr
     if info.returnsEarly && loopMutVars.isEmpty then
       defs := defs.push (mkConst ``Unit.unit)

src/Lean/Elab/Deriving/Basic.lean

@@ -233,27 +233,41 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) (isNoncomputable
         finally
           Core.setMessageLog (msgLog ++ (← Core.getMessageLog))
   let env ← getEnv
-  let hints := ReducibilityHints.regular (getMaxHeight env result.value + 1)
-  let decl ← mkDefinitionValInferringUnsafe instName result.levelParams.toList result.type result.value hints
-  -- Pre-check: if the instance value depends on noncomputable definitions and the user didn't write
-  -- `noncomputable`, give an actionable error with a `Try this:` suggestion.
-  unless isNoncomputable || (← read).isNoncomputableSection || (← isProp result.type) do
-    let noncompRef? := preNormValue.foldConsts none fun n acc =>
-      acc <|> if Lean.isNoncomputable (asyncMode := .local) env n then some n else none
-    if let some noncompRef := noncompRef? then
-      if let some cmdRef := cmdRef? then
-        if let some origText := cmdRef.reprint then
-          let newText := (origText.replace "deriving instance " "deriving noncomputable instance ").trimAscii
-          logInfoAt cmdRef m!"Try this: {newText}"
-      throwError "failed to derive instance because it depends on \
-        `{.ofConstName noncompRef}`, which is noncomputable"
-  if isNoncomputable || (← read).isNoncomputableSection then
-    addDecl <| Declaration.defnDecl decl
-    modifyEnv (addNoncomputable · instName)
+  let isPropType ← isProp result.type
+  if isPropType then
+    let decl ← mkThmOrUnsafeDef {
+      name := instName, levelParams := result.levelParams.toList,
+      type := result.type, value := result.value
+    }
+    addDecl decl
   else
-    addAndCompile <| Declaration.defnDecl decl
+    let hints := ReducibilityHints.regular (getMaxHeight env result.value + 1)
+    let decl ← mkDefinitionValInferringUnsafe instName result.levelParams.toList result.type result.value hints
+    -- Pre-check: if the instance value depends on noncomputable definitions and the user didn't write
+    -- `noncomputable`, give an actionable error with a `Try this:` suggestion.
+    unless isNoncomputable || (← read).isNoncomputableSection do
+      let noncompRef? := preNormValue.foldConsts none fun n acc =>
+        acc <|> if Lean.isNoncomputable (asyncMode := .local) env n then some n else none
+      if let some noncompRef := noncompRef? then
+        if let some cmdRef := cmdRef? then
+          if let some origText := cmdRef.reprint then
+            let newText := (origText.replace "deriving instance " "deriving noncomputable instance ").trimAscii
+            logInfoAt cmdRef m!"Try this: {newText}"
+        throwError "failed to derive instance because it depends on \
+          `{.ofConstName noncompRef}`, which is noncomputable"
+    if isNoncomputable || (← read).isNoncomputableSection then
+      addDecl <| Declaration.defnDecl decl
+      modifyEnv (addNoncomputable · instName)
+    else
+      addAndCompile <| Declaration.defnDecl decl
   trace[Elab.Deriving] "Derived instance `{.ofConstName instName}`"
-  registerInstance instName AttributeKind.global (eval_prio default)
+  -- For Prop-typed instances (theorems), skip `implicit_reducible` since reducibility hints are
+  -- irrelevant for theorems. This matches the behavior of the handwritten `instance` command
+  -- (see `MutualDef.lean`).
+  if isPropType then
+    addInstance instName AttributeKind.global (eval_prio default)
+  else
+    registerInstance instName AttributeKind.global (eval_prio default)
   addDeclarationRangesFromSyntax instName (← getRef)
 
 end Term

src/Lean/Elab/Deriving/DecEq.lean

@@ -111,7 +111,7 @@ def mkMatchNew (ctx : Context) (header : Header) (indVal : InductiveVal) : TermE
   let x1 := mkIdent header.targetNames[0]!
   let x2 := mkIdent header.targetNames[1]!
   let ctorIdxName := mkCtorIdxName indVal.name
-  -- NB: the getMatcherInfo? assumes all mathcers are called `match_`
+  -- NB: the getMatcherInfo? assumes all matchers are called `match_`
   let casesOnSameCtorName ← mkFreshUserName (indVal.name ++ `match_on_same_ctor)
   mkCasesOnSameCtor casesOnSameCtorName indVal.name
   let alts ← Array.ofFnM (n := indVal.numCtors) fun ⟨ctorIdx, _⟩ => do

src/Lean/Elab/Import.lean

@@ -28,7 +28,9 @@ def HeaderSyntax.isModule (header : HeaderSyntax) : Bool :=
 def HeaderSyntax.imports (stx : HeaderSyntax) (includeInit : Bool := true) : Array Import :=
   match stx with
   | `(Parser.Module.header| $[module%$moduleTk]? $[prelude%$preludeTk]? $importsStx*) =>
-    let imports := if preludeTk.isNone && includeInit then #[{ module := `Init : Import }] else #[]
+    let imports := if preludeTk.isNone && includeInit then
+        #[{ module := `Init : Import }, { module := `Init, isMeta := true : Import }]
+      else #[]
     imports ++ importsStx.map fun
       | `(Parser.Module.import| $[public%$publicTk]? $[meta%$metaTk]? import $[all%$allTk]? $n) =>
         { module := n.getId, importAll := allTk.isSome

src/Lean/Elab/ParseImportsFast.lean

@@ -233,7 +233,7 @@ def setImportAll : Parser := fun _ s =>
 
 def main : Parser :=
   keywordCore "module" (setIsModule false) (setIsModule true) >>
-  keywordCore "prelude" (fun _ s => s.pushImport `Init) skip >>
+  keywordCore "prelude" (fun _ s => (s.pushImport `Init).pushImport { module := `Init, isMeta := true }) skip >>
   manyImports (atomic (keywordCore "public" skip setExported >>
     keywordCore "meta" skip setMeta >>
     keyword "import") >>

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

@@ -36,7 +36,7 @@ def mkContext (lratPath : System.FilePath) (cfg : BVDecideConfig) : TermElabM Ta
   TacticContext.new lratPath cfg
 
 /--
-Prepare an `Expr` that proves `bvExpr.unsat` using native evalution.
+Prepare an `Expr` that proves `bvExpr.unsat` using native evaluation.
 -/
 def lratChecker (ctx : TacticContext) (reflectionResult : ReflectionResult) : MetaM Expr := do
   let cert ← LratCert.ofFile ctx.lratPath ctx.config.trimProofs

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

@@ -357,6 +357,7 @@ def reflectBV (g : MVarId) : M ReflectionResult := g.withContext do
   let mut sats := #[]
   let mut unusedHypotheses := {}
   for hyp in hyps do
+    checkSystem "bv_decide"
     if let (some reflected, lemmas) ← (SatAtBVLogical.of (mkFVar hyp)).run then
       sats := (sats ++ lemmas).push reflected
     else

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

@@ -33,6 +33,7 @@ where
   Reify `x`, returns `none` if the reification procedure failed.
   -/
   go (origExpr : Expr) : LemmaM (Option ReifiedBVExpr) := do
+    checkSystem "bv_decide"
     match_expr origExpr with
     | BitVec.ofNat _ _ => goBvLit origExpr
     | HAnd.hAnd _ _ _ _ lhsExpr rhsExpr =>
@@ -340,6 +341,7 @@ where
   Reify `t`, returns `none` if the reification procedure failed.
   -/
   go (origExpr : Expr) : LemmaM (Option ReifiedBVLogical) := do
+    checkSystem "bv_decide"
     match_expr origExpr with
     | Bool.true => ReifiedBVLogical.mkBoolConst true
     | Bool.false => ReifiedBVLogical.mkBoolConst false

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

@@ -159,6 +159,7 @@ Repeatedly run a list of `Pass` until they either close the goal or an iteration
 the goal anymore.
 -/
 partial def fixpointPipeline (passes : List Pass) (goal : MVarId) : PreProcessM (Option MVarId) := do
+  checkSystem "bv_decide"
   let mut newGoal := goal
   for pass in passes do
     if let some nextGoal ← pass.run newGoal then

src/Lean/Linter.lean

@@ -18,3 +18,4 @@ public import Lean.Linter.List
 public import Lean.Linter.Sets
 public import Lean.Linter.UnusedSimpArgs
 public import Lean.Linter.Coe
+public import Lean.Linter.GlobalAttributeIn

src/Lean/Linter/GlobalAttributeIn.lean

@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+-/
+module
+
+prelude
+public import Lean.Elab.Command
+public import Lean.Linter.Basic
+
+
+namespace Lean.Linter
+open Elab.Command
+
+private structure TopDownSkipQuot where
+  stx : Syntax
+
+def topDownSkipQuot (stx : Syntax) : TopDownSkipQuot := ⟨stx⟩
+
+partial instance [Monad m] : ForIn m TopDownSkipQuot Syntax where
+  forIn := fun ⟨stx⟩ init f => do
+    let rec @[specialize] loop stx b [Inhabited (type_of% b)] := do
+      if stx.isQuot then return ForInStep.yield b
+      match (← f stx b) with
+      | ForInStep.yield b' =>
+        let mut b := b'
+        if let Syntax.node _ _ args := stx then
+          for arg in args do
+            match (← loop arg b) with
+            | ForInStep.yield b' => b := b'
+            | ForInStep.done b'  => return ForInStep.done b'
+        return ForInStep.yield b
+      | ForInStep.done b => return ForInStep.done b
+    match (← @loop stx init ⟨init⟩) with
+    | ForInStep.yield b => return b
+    | ForInStep.done b  => return b
+
+def getGlobalAttributesIn? : Syntax → Option (Ident × Array (TSyntax `attr))
+  | `(attribute [$x,*] $id in $_) =>
+    let xs := x.getElems.filterMap fun a => match a.raw with
+      | `(Parser.Command.eraseAttr| -$_) => none
+      | `(Parser.Term.attrInstance| local $_attr:attr) => none
+      | `(Parser.Term.attrInstance| scoped $_attr:attr) => none
+      | `(attr| $a) => some a
+    (id, xs)
+  | _ => default
+
+def globalAttributeIn : Linter where run := withSetOptionIn fun stx => do
+  for s in topDownSkipQuot stx do
+    if let some (id, nonScopedNorLocal) := getGlobalAttributesIn? s then
+      for attr in nonScopedNorLocal do
+        logErrorAt attr
+          m!"Despite the `in`, the attribute {attr} is added globally to {id}\n\
+          please remove the `in` or make this a `local {attr}`"
+
+builtin_initialize addLinter globalAttributeIn
+
+end Lean.Linter

src/Lean/Meta/ExprDefEq.lean

@@ -48,6 +48,16 @@ register_builtin_option backward.isDefEq.respectTransparency : Bool := {
   when checking whether implicit arguments are definitionally equal"
 }
 
+/--
+Controls the transparency used to check whether the type of metavariable matches the type of the
+term being assigned to it.
+-/
+register_builtin_option backward.isDefEq.respectTransparency.types : Bool := {
+  defValue := false -- TODO: replace with `true` after we fix stage0
+  descr    := "if true, do not bump transparency to `.default` \
+  when checking whether the type of a metavariable matches the type of the term being assigned to it."
+}
+
 /--
 Controls whether *all* implicit arguments (not just instance-implicit `[..]`) get their
 transparency bumped to `TransparencyMode.instances` during `isDefEq`.
@@ -335,10 +345,10 @@ private def isDefEqArgsFirstPass
 
 /--
 Ensure `MetaM` configuration is strong enough for checking definitional equality of
-instances. For example, we must be able to unfold instances, `beta := true`, `proj := .yesWithDelta`
-are essential.
+implicit arguments (e.g., instances) and types.
+For example, we must be able to unfold instances, `beta := true`, `proj := .yesWithDelta` are essential.
 -/
-@[inline] def withInstanceConfig (x : MetaM α) : MetaM α :=
+@[inline] def withImplicitConfig (x : MetaM α) : MetaM α :=
   withAtLeastTransparency .instances do
     let cfg ← getConfig
     if cfg.beta && cfg.iota && cfg.zeta && cfg.zetaHave && cfg.zetaDelta && cfg.proj == .yesWithDelta then
@@ -382,7 +392,7 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta
       -- Bump to `.instances` so that `[implicit_reducible]` definitions (instances, `Nat.add`,
       -- `Array.size`, etc.) are unfolded. The user doesn't choose implicit arguments directly,
       -- so Lean should try harder than the caller's transparency to make them match.
-      unless (← withInstanceConfig <| Meta.isExprDefEqAux a₁ a₂) do return false
+      unless (← withImplicitConfig <| Meta.isExprDefEqAux a₁ a₂) do return false
     else if respectTransparency then
       unless (← Meta.isExprDefEqAux a₁ a₂) do return false
     else
@@ -392,7 +402,7 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta
     let a₁   := args₁[i]!
     let a₂   := args₂[i]!
     if respectTransparency && (implicitBump || finfo.paramInfo[i]!.isInstance) then
-      unless (← withInstanceConfig <| Meta.isExprDefEqAux a₁ a₂) do return false
+      unless (← withImplicitConfig <| Meta.isExprDefEqAux a₁ a₂) do return false
     else if !respectTransparency && finfo.paramInfo[i]!.isInstance then
       -- Old behavior
       unless (← withInferTypeConfig <| Meta.isExprDefEqAux a₁ a₂) do return false
@@ -454,6 +464,19 @@ private partial def isDefEqBindingAux (lctx : LocalContext) (fvars : Array Expr)
   let lctx ← getLCtx
   isDefEqBindingAux lctx #[] a b #[]
 
+/--
+Returns `true` if both `backward.isDefEq.respectTransparency` and `backward.isDefEq.respectTransparency.types` is true.
+
+The option `backward.isDefEq.respectTransparency.types` is newer than ``backward.isDefEq.respectTransparency`,
+and is used to enable the transparency bump when checking metavariable assignments.
+
+If `backward.isDefEq.respectTransparency` is `false`, then we automatically disable
+`backward.isDefEq.respectTransparency.types` too.
+-/
+abbrev respectTransparencyAtTypes : CoreM Bool := do
+  let opts ← getOptions
+  return backward.isDefEq.respectTransparency.types.get opts && backward.isDefEq.respectTransparency.get opts
+
 private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
   withTraceNodeBefore `Meta.isDefEq.assign.checkTypes (fun _ => return m!"({mvar} : {← inferType mvar}) := ({v} : {← inferType v})") do
     if !mvar.isMVar then
@@ -462,14 +485,24 @@ private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
     else
       -- must check whether types are definitionally equal or not, before assigning and returning true
       let mvarType ← inferType mvar
-      -- **TODO**: avoid transparency bump. Let's fix other issues first
-      withInferTypeConfig do
-        let vType ← inferType v
-        if (← Meta.isExprDefEqAux mvarType vType) then
-          mvar.mvarId!.assign v
-          pure true
-        else
-          pure false
+      let vType ← inferType v
+      if (← respectTransparencyAtTypes) then
+        withImplicitConfig do
+          if (← Meta.isExprDefEqAux mvarType vType) then
+            mvar.mvarId!.assign v
+            return true
+          else
+            if (← isDiagnosticsEnabled) then withInferTypeConfig do
+              if (← Meta.isExprDefEqAux mvarType vType) then
+                trace[diagnostics] "failure when assigning metavariable with type{indentExpr mvarType}\nwhich is not definitionally equal to{indentExpr vType}\nwhen using `.instances` transparency, but it is with `.default`.\nWorkaround: `set_option backward.isDefEq.respectTransparency.types false`"
+            return false
+      else
+        withInferTypeConfig do
+          if (← Meta.isExprDefEqAux mvarType vType) then
+            mvar.mvarId!.assign v
+            return true
+          else
+            return false
 
 /--
 Auxiliary method for solving constraints of the form `?m xs := v`.
@@ -2062,7 +2095,7 @@ private def isDefEqProj : Expr → Expr → MetaM Bool
        for instance-implicit parameters. -/
     let fromClass := isClass (← getEnv) m
     let isDefEqStructArgs (x : MetaM Bool) : MetaM Bool :=
-      if fromClass then withInstanceConfig x else x
+      if fromClass then withImplicitConfig x else x
     if (← read).inTypeClassResolution then
       -- See comment at `inTypeClassResolution`
       pure (i == j && m == n) <&&> isDefEqStructArgs (Meta.isExprDefEqAux t s)

src/Lean/Meta/Match/Match.lean

@@ -33,12 +33,12 @@ The high-level overview of moves are
   * If there is an alternative, solve its constraints
   * Else use `contradiction` to prove completeness of the match
 * Process “independent prefixes” of patterns. These are patterns that can be processed without
-  affecting the aother alternatives, and without side effects in the sense of updating the `mvarId`.
+  affecting the other alternatives, and without side effects in the sense of updating the `mvarId`.
   These are
   - variable patterns; substitute
   - inaccessible patterns; add equality constraints
   - as-patterns: substitute value and equality
-  After thes have been processed, we use `.inaccessible x` where `x` is the variable being matched
+  After these have been processed, we use `.inaccessible x` where `x` is the variable being matched
   to mark them as “done”.
 * If all patterns start with “done”, drop the first variable
 * The first alt has only “done” patterns, drop remaining alts (they're overlapped)
@@ -1108,6 +1108,9 @@ def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) (isSplitte
       -- matcher bodies should always be exported, if not private anyway
       withExporting do
         addDecl decl
+      -- if `matcher` is not private, we mark it as `implicit_reducible` too
+      unless isPrivateName name do
+        setReducibilityStatus name .implicitReducible
       unless isSplitter do
         modifyEnv fun env => matcherExt.modifyState env fun s => s.insert key name
         addMatcherInfo name mi

src/Lean/Meta/Match/Rewrite.lean

@@ -17,7 +17,7 @@ namespace Lean.Meta
 
 /--
 Tries to rewrite the `ite`, `dite` or `cond` expression `e` with the hypothesis `hc`.
-If it fails, it returns a rewrite with `proof? := none` and unchaged expression.
+If it fails, it returns a rewrite with `proof? := none` and unchanged expression.
 -/
 def rwIfWith (hc : Expr) (e : Expr) : MetaM Simp.Result := do
   match_expr e with

src/Lean/Meta/Native.lean

@@ -22,9 +22,9 @@ of that computation as an axiom towards the logic.
 -/
 
 public inductive NativeEqTrueResult where
-  /-- The given expression `e` evalutes to true. `prf` is a proof of `e = true`. -/
+  /-- The given expression `e` evaluates to true. `prf` is a proof of `e = true`. -/
   | success (prf : Expr)
-  /-- The given expression `e` evalutes to false. -/
+  /-- The given expression `e` evaluates to false. -/
   | notTrue
 
 /--

src/Lean/Meta/SameCtorUtils.lean

@@ -14,7 +14,7 @@ This module contains utilities for dealing with equalities between constructor a
 in particular about which fields must be the same a-priori for the equality to type check.
 
 Users include (or will include) the injectivity theorems, the per-constructor no-confusion
-construction and deriving type classes lik `BEq`, `DecidableEq` or `Ord`.
+construction and deriving type classes like `BEq`, `DecidableEq` or `Ord`.
 -/
 
 namespace Lean.Meta

src/Lean/Meta/SizeOf.lean

@@ -149,17 +149,15 @@ partial def mkSizeOfFn (recName : Name) (declName : Name): MetaM Unit := do
           trace[Meta.sizeOf] "declName: {declName}"
           trace[Meta.sizeOf] "type: {sizeOfType}"
           trace[Meta.sizeOf] "val: {sizeOfValue}"
-          -- We expose the `sizeOf` functions so that the `spec` theorems can be publicly `defeq`
-          withExporting do
-            addDecl <| Declaration.defnDecl {
-              name        := declName
-              levelParams := levelParams
-              type        := sizeOfType
-              value       := sizeOfValue
-              safety      := DefinitionSafety.safe
-              hints       := ReducibilityHints.abbrev
-            }
-            enableRealizationsForConst declName
+          addDecl <| Declaration.defnDecl {
+            name        := declName
+            levelParams := levelParams
+            type        := sizeOfType
+            value       := sizeOfValue
+            safety      := DefinitionSafety.safe
+            hints       := ReducibilityHints.abbrev
+          }
+          enableRealizationsForConst declName
 
 /--
   Create `sizeOf` functions for all inductive datatypes in the mutual inductive declaration containing `typeName`
@@ -469,7 +467,6 @@ private def mkSizeOfSpecTheorem (indInfo : InductiveVal) (sizeOfFns : Array Name
         type        := thmType
         value       := thmValue
       }
-      inferDefEqAttr thmName
       simpAttr.add thmName default .global
       grindAttr.add thmName grindAttrStx .global
 

src/Lean/Meta/Sym.lean

@@ -25,6 +25,7 @@ public import Lean.Meta.Sym.Simp
 public import Lean.Meta.Sym.Util
 public import Lean.Meta.Sym.Eta
 public import Lean.Meta.Sym.Canon
+public import Lean.Meta.Sym.Arith
 public import Lean.Meta.Sym.Grind
 public import Lean.Meta.Sym.SynthInstance
 

src/Lean/Meta/Sym/AbstractS.lean

@@ -97,4 +97,16 @@ public def mkLambdaFVarsS (xs : Array Expr) (e : Expr) : SymM Expr := do
     let type ← abstractFVarsRange decl.type i xs
     mkLambdaS decl.userName decl.binderInfo type b
 
+/--
+Similar to `mkForallFVars`, but uses the more efficient `abstractFVars` and `abstractFVarsRange`,
+and makes the same assumption made by these functions.
+-/
+public def mkForallFVarsS (xs : Array Expr) (e : Expr) : SymM Expr := do
+  let b ← abstractFVars e xs
+  xs.size.foldRevM (init := b) fun i _ b => do
+    let x := xs[i]
+    let decl ← x.fvarId!.getDecl
+    let type ← abstractFVarsRange decl.type i xs
+    mkForallS decl.userName decl.binderInfo type b
+
 end Lean.Meta.Sym

src/Lean/Meta/Sym/AlphaShareBuilder.lean

@@ -189,4 +189,48 @@ def mkAppS₄ (f a₁ a₂ a₃ a₄ : Expr) : m Expr := do
 def mkAppS₅ (f a₁ a₂ a₃ a₄ a₅ : Expr) : m Expr := do
   mkAppS (← mkAppS₄ f a₁ a₂ a₃ a₄) a₅
 
+def mkAppS₆ (f a₁ a₂ a₃ a₄ a₅ a₆ : Expr) : m Expr := do
+  mkAppS (← mkAppS₅ f a₁ a₂ a₃ a₄ a₅) a₆
+
+def mkAppS₇ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ : Expr) : m Expr := do
+  mkAppS (← mkAppS₆ f a₁ a₂ a₃ a₄ a₅ a₆) a₇
+
+def mkAppS₈ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ : Expr) : m Expr := do
+  mkAppS (← mkAppS₇ f a₁ a₂ a₃ a₄ a₅ a₆ a₇) a₈
+
+def mkAppS₉ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ : Expr) : m Expr := do
+  mkAppS (← mkAppS₈ f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈) a₉
+
+def mkAppS₁₀ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ a₁₀ : Expr) : m Expr := do
+  mkAppS (← mkAppS₉ f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉) a₁₀
+
+def mkAppS₁₁ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ a₁₀ a₁₁ : Expr) : m Expr := do
+  mkAppS (← mkAppS₁₀ f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ a₁₀) a₁₁
+
+/-- `mkAppRangeS f i j #[a₀, ..., aᵢ, ..., aⱼ, ...]` ==> `f aᵢ ... aⱼ₋₁` with max sharing. -/
+partial def mkAppRangeS (f : Expr) (beginIdx endIdx : Nat) (args : Array Expr) : m Expr :=
+  go endIdx f beginIdx
+where
+  go (endIdx : Nat) (b : Expr) (i : Nat) : m Expr := do
+    if endIdx ≤ i then return b
+    else go endIdx (← mkAppS b args[i]!) (i + 1)
+
+/-- `mkAppNS f #[a₀, ..., aₙ]` constructs `f a₀ ... aₙ` with max sharing. -/
+def mkAppNS (f : Expr) (args : Array Expr) : m Expr :=
+  mkAppRangeS f 0 args.size args
+
+/-- `mkAppRevRangeS f b e revArgs` ==> `mkAppRev f (revArgs.extract b e)` with max sharing. -/
+partial def mkAppRevRangeS (f : Expr) (beginIdx endIdx : Nat) (revArgs : Array Expr) : m Expr :=
+  go revArgs beginIdx f endIdx
+where
+  go (revArgs : Array Expr) (start : Nat) (b : Expr) (i : Nat) : m Expr := do
+    if i ≤ start then return b
+    else
+      let i := i - 1
+      go revArgs start (← mkAppS b revArgs[i]!) i
+
+/-- Same as `mkAppS f args` but reversing `args`, with max sharing. -/
+def mkAppRevS (f : Expr) (revArgs : Array Expr) : m Expr :=
+  mkAppRevRangeS f 0 revArgs.size revArgs
+
 end Lean.Meta.Sym.Internal

src/Lean/Meta/Sym/Arith.lean

@@ -0,0 +1,20 @@
+/-
+Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Sym.Arith.Types
+public import Lean.Meta.Sym.Arith.EvalNum
+public import Lean.Meta.Sym.Arith.Classify
+public import Lean.Meta.Sym.Arith.MonadCanon
+public import Lean.Meta.Sym.Arith.MonadRing
+public import Lean.Meta.Sym.Arith.MonadSemiring
+public import Lean.Meta.Sym.Arith.MonadVar
+public import Lean.Meta.Sym.Arith.Functions
+public import Lean.Meta.Sym.Arith.Reify
+public import Lean.Meta.Sym.Arith.DenoteExpr
+public import Lean.Meta.Sym.Arith.ToExpr
+public import Lean.Meta.Sym.Arith.VarRename
+public import Lean.Meta.Sym.Arith.Poly

src/Lean/Meta/Sym/Arith/Classify.lean

@@ -0,0 +1,165 @@
+/-
+Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Sym.Arith.EvalNum
+import Lean.Meta.Sym.SynthInstance
+import Lean.Meta.Sym.Canon
+import Lean.Meta.DecLevel
+import Init.Grind.Ring
+public section
+
+namespace Lean.Meta.Sym.Arith
+
+/-!
+# Algebraic structure classification
+
+Detects the strongest algebraic structure available for a type and caches
+the classification in `Arith.State.typeClassify`. The detection order is:
+
+1. `Grind.CommRing` (includes `Field` check)
+2. `Grind.Ring` (non-commutative)
+3. `Grind.CommSemiring` (via `OfSemiring.Q` envelope)
+4. `Grind.Semiring` (non-commutative)
+
+Results (including failures) are cached in a single `PHashMap ExprPtr ClassifyResult`
+to avoid repeated synthesis attempts.
+-/
+
+private def getIsCharInst? (u : Level) (type : Expr) (semiringInst : Expr) : SymM (Option (Expr × Nat)) := do
+  withNewMCtxDepth do
+    let n ← mkFreshExprMVar (mkConst ``Nat)
+    let charType := mkApp3 (mkConst ``Grind.IsCharP [u]) type semiringInst n
+    let some charInst ← Sym.synthInstance? charType | return none
+    let n ← instantiateMVars n
+    let some n ← evalNat? n | return none
+    return some (charInst, n)
+
+private def getNoZeroDivInst? (u : Level) (type : Expr) : SymM (Option Expr) := do
+  let natModuleType := mkApp (mkConst ``Grind.NatModule [u]) type
+  let some natModuleInst ← Sym.synthInstance? natModuleType | return none
+  let noZeroDivType := mkApp2 (mkConst ``Grind.NoNatZeroDivisors [u]) type natModuleInst
+  Sym.synthInstance? noZeroDivType
+
+private def getPowIdentityInst? (u : Level) (type : Expr) : SymM (Option (Expr × Expr × Nat)) := do withNewMCtxDepth do
+  -- We use a fresh metavar for `CommSemiring` (unlike `getIsCharInst?` which pins the semiring)
+  -- because `PowIdentity` instances may be declared against a canonical `CommSemiring` instance
+  -- that is not definitionally equal to `CommRing.toCommSemiring`. The synthesized `csInst` is
+  -- stored and used in proof terms to ensure type-correctness.
+  let csInst ← mkFreshExprMVar (mkApp (mkConst ``Grind.CommSemiring [u]) type)
+  let p ← mkFreshExprMVar (mkConst ``Nat)
+  let powIdentityType := mkApp3 (mkConst ``Grind.PowIdentity [u]) type csInst p
+  let some inst ← synthInstance? powIdentityType | return none
+  let csInst ← instantiateMVars csInst
+  let p ← instantiateMVars p
+  let some pVal ← evalNat? p | return none
+  return some (inst, csInst, pVal)
+
+private def mkAddRightCancelInst? (u : Level) (type : Expr) : SymM (Option Expr) := do
+  let add := mkApp (mkConst ``Add [u]) type
+  let some addInst ← synthInstance? add | return none
+  let addRightCancel := mkApp2 (mkConst ``Grind.AddRightCancel [u]) type addInst
+  synthInstance? addRightCancel
+
+/-- Try to classify `type` as a `CommRing`. Returns the ring id on success. -/
+private def tryCommRing? (type : Expr) : SymM (Option Nat) := do
+  let u ← getDecLevel type
+  let commRing := mkApp (mkConst ``Grind.CommRing [u]) type
+  let some commRingInst ← Sym.synthInstance? commRing | return none
+  let ringInst := mkApp2 (mkConst ``Grind.CommRing.toRing [u]) type commRingInst
+  let semiringInst := mkApp2 (mkConst ``Grind.Ring.toSemiring [u]) type ringInst
+  let commSemiringInst := mkApp2 (mkConst ``Grind.CommRing.toCommSemiring [u]) type semiringInst
+  let charInst? ← getIsCharInst? u type semiringInst
+  let noZeroDivInst? ← getNoZeroDivInst? u type
+  let fieldInst? ← Sym.synthInstance? <| mkApp (mkConst ``Grind.Field [u]) type
+  let powIdentityInst? ← getPowIdentityInst? u type
+  let semiringId? := none
+  let id := (← getArithState).rings.size
+  let ring : CommRing := {
+    id, semiringId?, type, u, semiringInst, ringInst, commSemiringInst,
+    commRingInst, charInst?, noZeroDivInst?, fieldInst?, powIdentityInst?
+  }
+  modifyArithState fun s => { s with rings := s.rings.push ring }
+  return some id
+
+/-- Try to classify `type` as a non-commutative `Ring`. -/
+private def tryNonCommRing? (type : Expr) : SymM (Option Nat) := do
+  let u ← getDecLevel type
+  let ring := mkApp (mkConst ``Grind.Ring [u]) type
+  let some ringInst ← Sym.synthInstance? ring | return none
+  let semiringInst := mkApp2 (mkConst ``Grind.Ring.toSemiring [u]) type ringInst
+  let charInst? ← getIsCharInst? u type semiringInst
+  let id := (← getArithState).ncRings.size
+  let ring : Ring := {
+    id, type, u, semiringInst, ringInst, charInst?
+  }
+  modifyArithState fun s => { s with ncRings := s.ncRings.push ring }
+  return some id
+
+/-- Helper function for `tryCommSemiring? -/
+private def tryCacheAndCommRing? (type : Expr) : SymM (Option Nat) := do
+  if let some result := (← getArithState).typeClassify.find? { expr := type } then
+    let .commRing id := result | return none
+    return id
+  let id? ← tryCommRing? type
+  let result := match id? with
+    | none => .none
+    | some id => .commRing id
+  modifyArithState fun s => { s with typeClassify := s.typeClassify.insert { expr := type } result }
+  return id?
+
+/-- Try to classify `type` as a `CommSemiring`. Creates the `OfSemiring.Q` envelope ring. -/
+private def tryCommSemiring? (type : Expr) : SymM (Option Nat) := do
+  let u ← getDecLevel type
+  let commSemiring := mkApp (mkConst ``Grind.CommSemiring [u]) type
+  let some commSemiringInst ← Sym.synthInstance? commSemiring | return none
+  let semiringInst := mkApp2 (mkConst ``Grind.CommSemiring.toSemiring [u]) type commSemiringInst
+  let addRightCancelInst? ← mkAddRightCancelInst? u type
+  let q ← shareCommon (← Sym.canon (mkApp2 (mkConst ``Grind.Ring.OfSemiring.Q [u]) type semiringInst))
+  -- The envelope `Q` type must be classifiable as a CommRing.
+  let some ringId ← tryCacheAndCommRing? q
+    | reportIssue! "unexpected failure initializing ring{indentExpr q}"; return none
+  let id := (← getArithState).semirings.size
+  let semiring : CommSemiring := {
+    id, type, ringId, u, semiringInst, commSemiringInst, addRightCancelInst?
+  }
+  modifyArithState fun s => { s with semirings := s.semirings.push semiring }
+  -- Link the envelope ring back to this semiring
+  modifyArithState fun s =>
+    let rings := s.rings.modify ringId fun r => { r with semiringId? := some id }
+    { s with rings }
+  return some id
+
+/-- Try to classify `type` as a non-commutative `Semiring`. -/
+private def tryNonCommSemiring? (type : Expr) : SymM (Option Nat) := do
+  let u ← getDecLevel type
+  let semiring := mkApp (mkConst ``Grind.Semiring [u]) type
+  let some semiringInst ← Sym.synthInstance? semiring | return none
+  let id := (← getArithState).ncSemirings.size
+  let semiring : Semiring := { id, type, u, semiringInst }
+  modifyArithState fun s => { s with ncSemirings := s.ncSemirings.push semiring }
+  return some id
+
+/--
+Classify the algebraic structure of `type`, trying the strongest first:
+CommRing > Ring > CommSemiring > Semiring.
+Results are cached in `Arith.State.typeClassify`.
+-/
+def classify? (type : Expr) : SymM ClassifyResult := do
+  if let some result := (← getArithState).typeClassify.find? { expr := type } then
+    return result
+  let result ← go
+  modifyArithState fun s => { s with typeClassify := s.typeClassify.insert { expr := type } result }
+  return result
+where
+  go : SymM ClassifyResult := do
+    if let some id ← tryCommRing? type then return .commRing id
+    if let some id ← tryNonCommRing? type then return .nonCommRing id
+    if let some id ← tryCommSemiring? type then return .commSemiring id
+    if let some id ← tryNonCommSemiring? type then return .nonCommSemiring id
+    return .none
+
+end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/DenoteExpr.lean

@@ -0,0 +1,93 @@
+/-
+Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Sym.Arith.Functions
+public import Lean.Meta.Sym.Arith.MonadVar
+public section
+namespace Lean.Meta.Sym.Arith
+
+/-!
+# Denotation of reified expressions
+
+Converts reified `RingExpr`, `Poly`, `Mon`, `Power` back into Lean `Expr`s using
+the ring's cached operator functions and variable array.
+-/
+
+variable [Monad m] [MonadError m] [MonadLiftT MetaM m] [MonadCanon m] [MonadRing m]
+
+/-- Convert an integer to a numeral expression in the ring. Negative values use `getNegFn`. -/
+def denoteNum (k : Int) : m Expr := do
+  let ring ← getRing
+  let n := mkRawNatLit k.natAbs
+  let ofNatInst ← if let some inst ← MonadCanon.synthInstance? (mkApp2 (mkConst ``OfNat [ring.u]) ring.type n) then
+    pure inst
+  else
+    pure <| mkApp3 (mkConst ``Grind.Semiring.ofNat [ring.u]) ring.type ring.semiringInst n
+  let e := mkApp3 (mkConst ``OfNat.ofNat [ring.u]) ring.type n ofNatInst
+  if k < 0 then
+    return mkApp (← getNegFn) e
+  else
+    return e
+
+/-- Denote a `Power` (variable raised to a power). -/
+def denotePower [MonadGetVar m] (pw : Power) : m Expr := do
+  let x ← getVar pw.x
+  if pw.k == 1 then
+    return x
+  else
+    return mkApp2 (← getPowFn) x (toExpr pw.k)
+
+/-- Denote a `Mon` (product of powers). -/
+def denoteMon [MonadGetVar m] (mn : Mon) : m Expr := do
+  match mn with
+  | .unit => denoteNum 1
+  | .mult pw mn => go mn (← denotePower pw)
+where
+  go (mn : Mon) (acc : Expr) : m Expr := do
+    match mn with
+    | .unit => return acc
+    | .mult pw mn => go mn (mkApp2 (← getMulFn) acc (← denotePower pw))
+
+/-- Denote a `Poly` (sum of coefficient × monomial terms). -/
+def denotePoly [MonadGetVar m] (p : Poly) : m Expr := do
+  match p with
+  | .num k => denoteNum k
+  | .add k mn p => go p (← denoteTerm k mn)
+where
+  denoteTerm (k : Int) (mn : Mon) : m Expr := do
+    if k == 1 then
+      denoteMon mn
+    else
+      return mkApp2 (← getMulFn) (← denoteNum k) (← denoteMon mn)
+
+  go (p : Poly) (acc : Expr) : m Expr := do
+    match p with
+    | .num 0 => return acc
+    | .num k => return mkApp2 (← getAddFn) acc (← denoteNum k)
+    | .add k mn p => go p (mkApp2 (← getAddFn) acc (← denoteTerm k mn))
+
+/-- Denote a `RingExpr` using a variable lookup function. -/
+@[specialize]
+private def denoteRingExprCore (getVarExpr : Nat → Expr) (e : RingExpr) : m Expr := do
+  go e
+where
+  go : RingExpr → m Expr
+  | .num k => denoteNum k
+  | .natCast k => return mkApp (← getNatCastFn) (mkNatLit k)
+  | .intCast k => return mkApp (← getIntCastFn) (mkIntLit k)
+  | .var x => return getVarExpr x
+  | .add a b => return mkApp2 (← getAddFn) (← go a) (← go b)
+  | .sub a b => return mkApp2 (← getSubFn) (← go a) (← go b)
+  | .mul a b => return mkApp2 (← getMulFn) (← go a) (← go b)
+  | .pow a k => return mkApp2 (← getPowFn) (← go a) (toExpr k)
+  | .neg a => return mkApp (← getNegFn) (← go a)
+
+/-- Denote a `RingExpr` using an explicit variable array. -/
+def denoteRingExpr (vars : Array Expr) (e : RingExpr) : m Expr := do
+  denoteRingExprCore (fun x => vars[x]!) e
+
+end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/EvalNum.lean

@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Sym.Arith.Types
+import Lean.Meta.Sym.LitValues
+import Lean.Meta.IntInstTesters
+import Lean.Meta.NatInstTesters
+public section
+
+namespace Lean.Meta.Sym.Arith
+
+/-!
+Functions for evaluating simple `Nat` and `Int` expressions that appear in type classes
+(e.g., `ToInt` and `IsCharP`). Using `whnf` for this purpose is too expensive and can
+exhaust the stack. We considered `evalExpr` as an alternative, but it introduces
+considerable overhead. We may use `evalExpr` as a fallback in the future.
+-/
+
+def checkExp (k : Nat) : OptionT SymM Unit := do
+  let exp ← getExpThreshold
+  if k > exp then
+    reportIssue! "exponent {k} exceeds threshold for exponentiation `(exp := {exp})`"
+    failure
+
+/-
+**Note**: It is safe to use (the more efficient) structural instance tests here because
+`Sym.Canon` has already run.
+-/
+open Structural in
+mutual
+private partial def evalNatCore (e : Expr) : OptionT SymM Nat := do
+  match_expr e with
+  | Nat.zero => return 0
+  | Nat.succ a => return (← evalNatCore a) + 1
+  | Int.toNat a => return (← evalIntCore a).toNat
+  | Int.natAbs a => return (← evalIntCore a).natAbs
+  | HAdd.hAdd _ _ _ inst a b => guard (← isInstHAddNat inst); return (← evalNatCore a) + (← evalNatCore b)
+  | HMul.hMul _ _ _ inst a b => guard (← isInstHMulNat inst); return (← evalNatCore a) * (← evalNatCore b)
+  | HSub.hSub _ _ _ inst a b => guard (← isInstHSubNat inst); return (← evalNatCore a) - (← evalNatCore b)
+  | HDiv.hDiv _ _ _ inst a b => guard (← isInstHDivNat inst); return (← evalNatCore a) / (← evalNatCore b)
+  | HMod.hMod _ _ _ inst a b => guard (← isInstHModNat inst); return (← evalNatCore a) % (← evalNatCore b)
+  | OfNat.ofNat _ _ _ =>
+    let some n := Sym.getNatValue? e |>.run | failure
+    return n
+  | HPow.hPow _ _ _ inst a k =>
+    guard (← isInstHPowNat inst)
+    let k ← evalNatCore k
+    checkExp k
+    let a ← evalNatCore a
+    return a ^ k
+  | _ => failure
+
+private partial def evalIntCore (e : Expr) : OptionT SymM Int := do
+  match_expr e with
+  | Neg.neg _ i a => guard (← isInstNegInt i); return - (← evalIntCore a)
+  | HAdd.hAdd _ _ _ i a b => guard (← isInstHAddInt i); return (← evalIntCore a) + (← evalIntCore b)
+  | HSub.hSub _ _ _ i a b => guard (← isInstHSubInt i); return (← evalIntCore a) - (← evalIntCore b)
+  | HMul.hMul _ _ _ i a b => guard (← isInstHMulInt i); return (← evalIntCore a) * (← evalIntCore b)
+  | HDiv.hDiv _ _ _ i a b => guard (← isInstHDivInt i); return (← evalIntCore a) / (← evalIntCore b)
+  | HMod.hMod _ _ _ i a b => guard (← isInstHModInt i); return (← evalIntCore a) % (← evalIntCore b)
+  | HPow.hPow _ _ _ i a k =>
+    guard (← isInstHPowInt i)
+    let a ← evalIntCore a
+    let k ← evalNatCore k
+    checkExp k
+    return a ^ k
+  | OfNat.ofNat _ _ _ =>
+    let some n := Sym.getIntValue? e |>.run | failure
+    return n
+  | NatCast.natCast _ i a =>
+    let_expr instNatCastInt ← i | failure
+    return (← evalNatCore a)
+  | Nat.cast _ i a =>
+    let_expr instNatCastInt ← i | failure
+    return (← evalNatCore a)
+  | _ => failure
+
+end
+
+def evalNat? (e : Expr) : SymM (Option Nat) :=
+  evalNatCore e |>.run
+
+def evalInt? (e : Expr) : SymM (Option Int) :=
+  evalIntCore e |>.run
+
+end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/Functions.lean

@@ -1,52 +1,62 @@
 /-
-Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
+public import Lean.Meta.Sym.Arith.MonadRing
+public import Lean.Meta.Sym.Arith.MonadSemiring
 public section
-namespace Lean.Meta.Grind.Arith.CommRing
+namespace Lean.Meta.Sym.Arith
+
+/-!
+# Cached function expressions for arithmetic operators
+
+Synthesizes and caches the canonical Lean expressions for arithmetic operators
+(`+`, `*`, `-`, `^`, `intCast`, `natCast`, etc.). These cached expressions are used
+during reification to validate instances via pointer equality (`isSameExpr`).
+
+Each getter checks the cache field first. On a miss, it synthesizes the instance,
+verifies it against the expected instance from the ring structure using `isDefEqI`,
+canonicalizes the result via `canonExpr`, and stores it.
+-/
+
 variable [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m]
 
-section
-variable [MonadRing m]
+private def checkInst (declName : Name) (inst inst' : Expr) : MetaM Unit := do
+  unless (← withReducibleAndInstances <| isDefEq inst inst') do
+    throwError "error while initializing arithmetic operators:\ninstance for `{declName}` {indentExpr inst}\nis not definitionally equal to the expected one {indentExpr inst'}\nwhen only reducible definitions and instances are reduced"
 
-def checkInst (declName : Name) (inst inst' : Expr) : MetaM Unit := do
-  unless (← isDefEqI inst inst') do
-    throwError "error while initializing `grind ring` operators:\ninstance for `{declName}` {indentExpr inst}\nis not definitionally equal to the expected one {indentExpr inst'}\nwhen only reducible definitions and instances are reduced"
-
-def mkUnaryFn (type : Expr) (u : Level) (instDeclName : Name) (declName : Name) (expectedInst : Expr) : m Expr := do
+private def mkUnaryFn (type : Expr) (u : Level) (instDeclName : Name) (declName : Name) (expectedInst : Expr) : m Expr := do
   let inst ← MonadCanon.synthInstance <| mkApp (mkConst instDeclName [u]) type
   checkInst declName inst expectedInst
   canonExpr <| mkApp2 (mkConst declName [u]) type inst
 
-def mkBinHomoFn (type : Expr) (u : Level) (instDeclName : Name) (declName : Name) (expectedInst : Expr) : m Expr := do
+private def mkBinHomoFn (type : Expr) (u : Level) (instDeclName : Name) (declName : Name) (expectedInst : Expr) : m Expr := do
   let inst ← MonadCanon.synthInstance <| mkApp3 (mkConst instDeclName [u, u, u]) type type type
   checkInst declName inst expectedInst
   canonExpr <| mkApp4 (mkConst declName [u, u, u]) type type type inst
 
-def mkPowFn (u : Level) (type : Expr) (semiringInst : Expr) : m Expr := do
+private def mkPowFn (u : Level) (type : Expr) (semiringInst : Expr) : m Expr := do
   let inst ← MonadCanon.synthInstance <| mkApp3 (mkConst ``HPow [u, 0, u]) type Nat.mkType type
   let inst' := mkApp2 (mkConst ``Grind.Semiring.npow [u]) type semiringInst
   checkInst ``HPow.hPow inst inst'
   canonExpr <| mkApp4 (mkConst ``HPow.hPow [u, 0, u]) type Nat.mkType type inst
 
-def mkNatCastFn (u : Level) (type : Expr) (semiringInst : Expr) : m Expr := do
+private def mkNatCastFn (u : Level) (type : Expr) (semiringInst : Expr) : m Expr := do
   let inst' := mkApp2 (mkConst ``Grind.Semiring.natCast [u]) type semiringInst
   let instType := mkApp (mkConst ``NatCast [u]) type
-  -- Note that `Semiring.natCast` is not registered as a global instance
-  -- (to avoid introducing unwanted coercions)
-  -- so merely having a `Semiring α` instance
-  -- does not guarantee that an `NatCast α` will be available.
-  -- When both are present we verify that they are defeq,
-  -- and otherwise fall back to the field of the `Semiring α` instance that we already have.
+  -- Note: `Semiring.natCast` is not a global instance, so `NatCast α` may not be available.
+  -- When present, verify defeq; otherwise fall back to the semiring field.
   let inst ← match (← MonadCanon.synthInstance? instType) with
   | none => pure inst'
   | some inst => checkInst ``NatCast.natCast inst inst'; pure inst
   canonExpr <| mkApp2 (mkConst ``NatCast.natCast [u]) type inst
 
+section RingFns
+variable [MonadRing m]
+
 def getAddFn : m Expr := do
   let ring ← getRing
   if let some addFn := ring.addFn? then return addFn
@@ -55,14 +65,6 @@ def getAddFn : m Expr := do
   modifyRing fun s => { s with addFn? := some addFn }
   return addFn
 
-def getSubFn : m Expr := do
-  let ring ← getRing
-  if let some subFn := ring.subFn? then return subFn
-  let expectedInst := mkApp2 (mkConst ``instHSub [ring.u]) ring.type <| mkApp2 (mkConst ``Grind.Ring.toSub [ring.u]) ring.type ring.ringInst
-  let subFn ← mkBinHomoFn ring.type ring.u ``HSub ``HSub.hSub expectedInst
-  modifyRing fun s => { s with subFn? := some subFn }
-  return subFn
-
 def getMulFn : m Expr := do
   let ring ← getRing
   if let some mulFn := ring.mulFn? then return mulFn
@@ -71,6 +73,14 @@ def getMulFn : m Expr := do
   modifyRing fun s => { s with mulFn? := some mulFn }
   return mulFn
 
+def getSubFn : m Expr := do
+  let ring ← getRing
+  if let some subFn := ring.subFn? then return subFn
+  let expectedInst := mkApp2 (mkConst ``instHSub [ring.u]) ring.type <| mkApp2 (mkConst ``Grind.Ring.toSub [ring.u]) ring.type ring.ringInst
+  let subFn ← mkBinHomoFn ring.type ring.u ``HSub ``HSub.hSub expectedInst
+  modifyRing fun s => { s with subFn? := some subFn }
+  return subFn
+
 def getNegFn : m Expr := do
   let ring ← getRing
   if let some negFn := ring.negFn? then return negFn
@@ -91,12 +101,7 @@ def getIntCastFn : m Expr := do
   if let some intCastFn := ring.intCastFn? then return intCastFn
   let inst' := mkApp2 (mkConst ``Grind.Ring.intCast [ring.u]) ring.type ring.ringInst
   let instType := mkApp (mkConst ``IntCast [ring.u]) ring.type
-  -- Note that `Ring.intCast` is not registered as a global instance
-  -- (to avoid introducing unwanted coercions)
-  -- so merely having a `Ring α` instance
-  -- does not guarantee that an `IntCast α` will be available.
-  -- When both are present we verify that they are defeq,
-  -- and otherwise fall back to the field of the `Ring α` instance that we already have.
+  -- Note: `Ring.intCast` is not a global instance. Same pattern as `mkNatCastFn`.
   let inst ← match (← MonadCanon.synthInstance? instType) with
     | none => pure inst'
     | some inst => checkInst ``Int.cast inst inst'; pure inst
@@ -111,32 +116,56 @@ def getNatCastFn : m Expr := do
   modifyRing fun s => { s with natCastFn? := some natCastFn }
   return natCastFn
 
-private def mkOne (u : Level) (type : Expr) (semiringInst : Expr) : m Expr := do
-  let n := mkRawNatLit 1
-  let ofNatInst := mkApp3 (mkConst ``Grind.Semiring.ofNat [u]) type semiringInst n
-  canonExpr <| mkApp3 (mkConst ``OfNat.ofNat [u]) type n ofNatInst
+end RingFns
 
-def getOne [MonadLiftT GoalM m] : m Expr := do
-  let ring ← getRing
-  if let some one := ring.one? then return one
-  let one ← mkOne ring.u ring.type ring.semiringInst
-  modifyRing fun s => { s with one? := some one }
-  internalize one 0
-  return one
-end
-
-section
+section CommRingFns
 variable [MonadCommRing m]
 
 def getInvFn : m Expr := do
   let ring ← getCommRing
   let some fieldInst := ring.fieldInst?
-    | throwError "`grind` internal error, type is not a field{indentExpr ring.type}"
+    | throwError "internal error: type is not a field{indentExpr ring.type}"
   if let some invFn := ring.invFn? then return invFn
   let expectedInst := mkApp2 (mkConst ``Grind.Field.toInv [ring.u]) ring.type fieldInst
   let invFn ← mkUnaryFn ring.type ring.u ``Inv ``Inv.inv expectedInst
   modifyCommRing fun s => { s with invFn? := some invFn }
   return invFn
-end
 
-end Lean.Meta.Grind.Arith.CommRing
+end CommRingFns
+
+section SemiringFns
+variable [MonadSemiring m]
+
+def getAddFn' : m Expr := do
+  let sr ← getSemiring
+  if let some addFn := sr.addFn? then return addFn
+  let expectedInst := mkApp2 (mkConst ``instHAdd [sr.u]) sr.type <| mkApp2 (mkConst ``Grind.Semiring.toAdd [sr.u]) sr.type sr.semiringInst
+  let addFn ← mkBinHomoFn sr.type sr.u ``HAdd ``HAdd.hAdd expectedInst
+  modifySemiring fun s => { s with addFn? := some addFn }
+  return addFn
+
+def getMulFn' : m Expr := do
+  let sr ← getSemiring
+  if let some mulFn := sr.mulFn? then return mulFn
+  let expectedInst := mkApp2 (mkConst ``instHMul [sr.u]) sr.type <| mkApp2 (mkConst ``Grind.Semiring.toMul [sr.u]) sr.type sr.semiringInst
+  let mulFn ← mkBinHomoFn sr.type sr.u ``HMul ``HMul.hMul expectedInst
+  modifySemiring fun s => { s with mulFn? := some mulFn }
+  return mulFn
+
+def getPowFn' : m Expr := do
+  let sr ← getSemiring
+  if let some powFn := sr.powFn? then return powFn
+  let powFn ← mkPowFn sr.u sr.type sr.semiringInst
+  modifySemiring fun s => { s with powFn? := some powFn }
+  return powFn
+
+def getNatCastFn' : m Expr := do
+  let sr ← getSemiring
+  if let some natCastFn := sr.natCastFn? then return natCastFn
+  let natCastFn ← mkNatCastFn sr.u sr.type sr.semiringInst
+  modifySemiring fun s => { s with natCastFn? := some natCastFn }
+  return natCastFn
+
+end SemiringFns
+
+end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/MonadCanon.lean

@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Sym.Arith.Types
+public import Lean.Meta.Sym.Canon
+public import Lean.Meta.Sym.SynthInstance
+public section
+namespace Lean.Meta.Sym.Arith
+
+class MonadCanon (m : Type → Type) where
+  /--
+  Canonicalize an expression (types, instances, support arguments).
+  In `SymM`, this is `Sym.canon`. In `PP.M` (diagnostics), this is the identity.
+  -/
+  canonExpr : Expr → m Expr
+  /--
+  Synthesize an instance, returning `none` on failure.
+  In `SymM`, this is `Sym.synthInstance?`. In `PP.M`, this is `Meta.synthInstance?`.
+  -/
+  synthInstance? : Expr → m (Option Expr)
+
+export MonadCanon (canonExpr)
+
+@[always_inline]
+instance (m n) [MonadLift m n] [MonadCanon m] : MonadCanon n where
+  canonExpr e := liftM (canonExpr e : m Expr)
+  synthInstance? e := liftM (MonadCanon.synthInstance? e : m (Option Expr))
+
+def MonadCanon.synthInstance [Monad m] [MonadError m] [MonadCanon m] (type : Expr) : m Expr := do
+  let some inst ← synthInstance? type
+    | throwError "failed to find instance{indentExpr type}"
+  return inst
+
+instance : MonadCanon SymM where
+  canonExpr := canon
+  synthInstance? := Sym.synthInstance?
+
+end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/MonadRing.lean

@@ -1,13 +1,13 @@
 /-
-Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadCanon
+public import Lean.Meta.Sym.Arith.MonadCanon
 public section
-namespace Lean.Meta.Grind.Arith.CommRing
+namespace Lean.Meta.Sym.Arith
 
 class MonadRing (m : Type → Type) where
   getRing : m Ring
@@ -36,4 +36,4 @@ instance (m) [Monad m] [MonadCommRing m] : MonadRing m where
   getRing := return (← getCommRing).toRing
   modifyRing f := modifyCommRing fun s => { s with toRing := f s.toRing }
 
-end Lean.Meta.Grind.Arith.CommRing
+end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/MonadSemiring.lean

@@ -1,13 +1,13 @@
 /-
-Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadCanon
+public import Lean.Meta.Sym.Arith.MonadCanon
 public section
-namespace Lean.Meta.Grind.Arith.CommRing
+namespace Lean.Meta.Sym.Arith
 
 class MonadSemiring (m : Type → Type) where
   getSemiring : m Semiring
@@ -36,4 +36,4 @@ instance (m) [Monad m] [MonadCommSemiring m] : MonadSemiring m where
   getSemiring := return (← getCommSemiring).toSemiring
   modifySemiring f := modifyCommSemiring fun s => { s with toSemiring := f s.toSemiring }
 
-end Lean.Meta.Grind.Arith.CommRing
+end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/MonadVar.lean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Sym.Arith.Types
+public section
+namespace Lean.Meta.Sym.Arith
+
+/-- Read a variable's Lean expression by index. Used by `DenoteExpr` and diagnostics (PP). -/
+class MonadGetVar (m : Type → Type) where
+  getVar : Var → m Expr
+
+export MonadGetVar (getVar)
+
+@[always_inline]
+instance (m n) [MonadLift m n] [MonadGetVar m] : MonadGetVar n where
+  getVar x := liftM (getVar x : m Expr)
+
+/-- Create or lookup a variable for a Lean expression. Used by reification. -/
+class MonadMkVar (m : Type → Type) where
+  mkVar : Expr → (gen : Nat) → m Var
+
+export MonadMkVar (mkVar)
+
+@[always_inline]
+instance (m n) [MonadLift m n] [MonadMkVar m] : MonadMkVar n where
+  mkVar e gen := liftM (mkVar e gen : m Var)
+
+end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/Reify.lean

@@ -1,16 +1,36 @@
 /-
-Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommRingM
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommSemiringM
+public import Lean.Meta.Sym.Arith.Functions
+public import Lean.Meta.Sym.Arith.MonadVar
+public import Lean.Meta.Sym.LitValues
 public section
-namespace Lean.Meta.Grind.Arith.CommRing
+namespace Lean.Meta.Sym.Arith
+open Sym.Arith (MonadCanon)
 
-variable [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m]
+/-!
+# Reification of arithmetic expressions
+
+Converts Lean expressions into `CommRing.Expr` (ring) or `CommSemiring.Expr`
+(semiring) for reflection-based normalization.
+
+Instance validation uses pointer equality (`isSameExpr`) against cached function
+expressions from `Functions.lean`.
+
+## Differences from grind's `Reify.lean`
+
+- Uses `MonadMkVar` for variable creation instead of grind's `internalize` + `mkVarCore`
+- Uses `Sym.getNatValue?`/`Sym.getIntValue?` (pure) instead of `MetaM` versions
+- No `MonadSetTermId` — term-to-ring-id tracking is grind-specific
+-/
+
+section RingReify
+
+variable [MonadLiftT SymM m] [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] [MonadMkVar m]
 
 def isAddInst (inst : Expr) : m Bool :=
   return isSameExpr (← getAddFn).appArg! inst
@@ -27,29 +47,22 @@ def isIntCastInst (inst : Expr) : m Bool :=
 def isNatCastInst (inst : Expr) : m Bool :=
   return isSameExpr (← getNatCastFn).appArg! inst
 
-private def reportAppIssue (e : Expr) : GoalM Unit := do
+private def reportRingAppIssue [MonadLiftT SymM m] (e : Expr) : m Unit := do
   reportIssue! "ring term with unexpected instance{indentExpr e}"
 
-variable [MonadLiftT GoalM m] [MonadSetTermId m]
-
 /--
-Converts a Lean expression `e` in the `CommRing` into a `CommRing.Expr` object.
+Converts a Lean expression `e` into a `RingExpr`.
 
-If `skipVar` is `true`, then the result is `none` if `e` is not an interpreted `CommRing` term.
-We use `skipVar := false` when processing inequalities, and `skipVar := true` for equalities and disequalities
+If `skipVar` is `true`, returns `none` if `e` is not an interpreted ring term
+(used for equalities/disequalities). If `false`, treats non-interpreted terms
+as variables (used for inequalities).
 -/
-partial def reifyCore? (e : Expr) (skipVar : Bool) (gen : Nat) : m (Option RingExpr) := do
-  let mkVar (e : Expr) : m Var := do
-    if (← alreadyInternalized e) then
-      mkVarCore e
-    else
-      internalize e gen
-      mkVarCore e
+partial def reifyRing? (e : Expr) (skipVar : Bool := true) (gen : Nat) : m (Option RingExpr) := do
   let toVar (e : Expr) : m RingExpr := do
-    return .var (← mkVar e)
+    return .var (← mkVar e gen)
   let asVar (e : Expr) : m RingExpr := do
-    reportAppIssue e
-    return .var (← mkVar e)
+    reportRingAppIssue e
+    return .var (← mkVar e gen)
   let rec go (e : Expr) : m RingExpr := do
     match_expr e with
     | HAdd.hAdd _ _ _ i a b =>
@@ -59,27 +72,33 @@ partial def reifyCore? (e : Expr) (skipVar : Bool) (gen : Nat) : m (Option RingE
     | HSub.hSub _ _ _ i a b =>
       if (← isSubInst i) then return .sub (← go a) (← go b) else asVar e
     | HPow.hPow _ _ _ i a b =>
-      let some k ← getNatValue? b | toVar e
+      let some k := Sym.getNatValue? b |>.run | toVar e
       if (← isPowInst i) then return .pow (← go a) k else asVar e
     | Neg.neg _ i a =>
       if (← isNegInst i) then return .neg (← go a) else asVar e
     | IntCast.intCast _ i a =>
       if (← isIntCastInst i) then
-        let some k ← getIntValue? a | toVar e
+        let some k := Sym.getIntValue? a |>.run | toVar e
         return .intCast k
       else
         asVar e
     | NatCast.natCast _ i a =>
       if (← isNatCastInst i) then
-        let some k ← getNatValue? a | toVar e
+        let some k := Sym.getNatValue? a |>.run | toVar e
         return .natCast k
       else
         asVar e
     | OfNat.ofNat _ n _ =>
-      let some k ← getNatValue? n | toVar e
+      /-
+      **Note**: We extract `n` directly as a raw nat literal. The grind version uses `MetaM`'s
+      `getNatValue?` which handles multiple encodings (raw literals, nested `OfNat`, etc.).
+      In `SymM`, we assume terms have been canonicalized by `Sym.canon` before reification,
+      so `OfNat.ofNat _ n _` always has a raw nat literal at position 1.
+      -/
+      let .lit (.natVal k) := n | toVar e
       return .num k
     | BitVec.ofNat _ n =>
-      let some k ← getNatValue? n | toVar e
+      let .lit (.natVal k) := n | toVar e
       return .num k
     | _ => toVar e
   let toTopVar (e : Expr) : m (Option RingExpr) := do
@@ -88,7 +107,7 @@ partial def reifyCore? (e : Expr) (skipVar : Bool) (gen : Nat) : m (Option RingE
     else
       return some (← toVar e)
   let asTopVar (e : Expr) : m (Option RingExpr) := do
-    reportAppIssue e
+    reportRingAppIssue e
     toTopVar e
   match_expr e with
   | HAdd.hAdd _ _ _ i a b =>
@@ -98,54 +117,46 @@ partial def reifyCore? (e : Expr) (skipVar : Bool) (gen : Nat) : m (Option RingE
   | HSub.hSub _ _ _ i a b =>
     if (← isSubInst i) then return some (.sub (← go a) (← go b)) else asTopVar e
   | HPow.hPow _ _ _ i a b =>
-    let some k ← getNatValue? b | asTopVar e
+    let some k := Sym.getNatValue? b |>.run | asTopVar e
     if (← isPowInst i) then return some (.pow (← go a) k) else asTopVar e
   | Neg.neg _ i a =>
     if (← isNegInst i) then return some (.neg (← go a)) else asTopVar e
   | IntCast.intCast _ i a =>
     if (← isIntCastInst i) then
-      let some k ← getIntValue? a | toTopVar e
+      let some k := Sym.getIntValue? a |>.run | toTopVar e
       return some (.intCast k)
     else
       asTopVar e
   | NatCast.natCast _ i a =>
     if (← isNatCastInst i) then
-      let some k ← getNatValue? a | toTopVar e
+      let some k := Sym.getNatValue? a |>.run | toTopVar e
       return some (.natCast k)
     else
       asTopVar e
   | OfNat.ofNat _ n _ =>
-    let some k ← getNatValue? n | asTopVar e
+    let .lit (.natVal k) := n | asTopVar e
     return some (.num k)
   | _ => toTopVar e
 
-/-- Reify ring expression. -/
-def reify? (e : Expr) (skipVar := true) (gen : Nat := 0) : RingM (Option RingExpr) := do
-  reifyCore? e skipVar gen
+end RingReify
 
-/-- Reify non-commutative ring expression. -/
-def ncreify? (e : Expr) (skipVar := true) (gen : Nat := 0) : NonCommRingM (Option RingExpr) := do
-  reifyCore? e skipVar gen
+section SemiringReify
 
-private def reportSAppIssue (e : Expr) : GoalM Unit := do
+variable [MonadLiftT SymM m] [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadSemiring m] [MonadMkVar m]
+
+private def reportSemiringAppIssue [MonadLiftT SymM m] (e : Expr) : m Unit := do
   reportIssue! "semiring term with unexpected instance{indentExpr e}"
 
-section
-variable [MonadLiftT GoalM m] [MonadError m] [Monad m] [MonadCanon m] [MonadSemiring m] [MonadSetTermId m]
-
 /--
-Similar to `reify?` but for `CommSemiring`
+Converts a Lean expression `e` into a `SemiringExpr`.
+Only recognizes `add`, `mul`, `pow`, `natCast`, and numerals (no `sub`, `neg`, `intCast`).
 -/
-partial def sreifyCore? (e : Expr) : m (Option SemiringExpr) := do
-  let mkVar (e : Expr) : m Var := do
-    unless (← alreadyInternalized e) do
-      internalize e 0
-    mkSVarCore e
+partial def reifySemiring? (e : Expr) (gen : Nat) : m (Option SemiringExpr) := do
   let toVar (e : Expr) : m SemiringExpr := do
-    return .var (← mkVar e)
+    return .var (← mkVar e gen)
   let asVar (e : Expr) : m SemiringExpr := do
-    reportSAppIssue e
-    return .var (← mkVar e)
+    reportSemiringAppIssue e
+    return .var (← mkVar e gen)
   let rec go (e : Expr) : m SemiringExpr := do
     match_expr e with
     | HAdd.hAdd _ _ _ i a b =>
@@ -153,22 +164,22 @@ partial def sreifyCore? (e : Expr) : m (Option SemiringExpr) := do
     | HMul.hMul _ _ _ i a b =>
       if isSameExpr (← getMulFn').appArg! i then return .mul (← go a) (← go b) else asVar e
     | HPow.hPow _ _ _ i a b =>
-      let some k ← getNatValue? b | toVar e
+      let some k := Sym.getNatValue? b |>.run | toVar e
       if isSameExpr (← getPowFn').appArg! i then return .pow (← go a) k else asVar e
     | NatCast.natCast _ i a =>
       if isSameExpr (← getNatCastFn').appArg! i then
-        let some k ← getNatValue? a | toVar e
+        let some k := Sym.getNatValue? a |>.run | toVar e
         return .num k
       else
         asVar e
     | OfNat.ofNat _ n _ =>
-      let some k ← getNatValue? n | toVar e
+      let .lit (.natVal k) := n | toVar e
       return .num k
     | _ => toVar e
   let toTopVar (e : Expr) : m (Option SemiringExpr) := do
     return some (← toVar e)
   let asTopVar (e : Expr) : m (Option SemiringExpr) := do
-    reportSAppIssue e
+    reportSemiringAppIssue e
     toTopVar e
   match_expr e with
   | HAdd.hAdd _ _ _ i a b =>
@@ -176,27 +187,19 @@ partial def sreifyCore? (e : Expr) : m (Option SemiringExpr) := do
   | HMul.hMul _ _ _ i a b =>
     if isSameExpr (← getMulFn').appArg! i then return some (.mul (← go a) (← go b)) else asTopVar e
   | HPow.hPow _ _ _ i a b =>
-    let some k ← getNatValue? b | return none
+    let some k := Sym.getNatValue? b |>.run | return none
     if isSameExpr (← getPowFn').appArg! i then return some (.pow (← go a) k) else asTopVar e
   | NatCast.natCast _ i a =>
     if isSameExpr (← getNatCastFn').appArg! i then
-      let some k ← getNatValue? a | toTopVar e
+      let some k := Sym.getNatValue? a |>.run | toTopVar e
       return some (.num k)
     else
       asTopVar e
   | OfNat.ofNat _ n _ =>
-    let some k ← getNatValue? n | asTopVar e
+    let .lit (.natVal k) := n | asTopVar e
     return some (.num k)
   | _ => toTopVar e
 
-end
+end SemiringReify
 
-/-- Reify semiring expression. -/
-def sreify? (e : Expr) : SemiringM (Option SemiringExpr) := do
-  sreifyCore? e
-
-/-- Reify non-commutative semiring expression. -/
-def ncsreify? (e : Expr) : NonCommSemiringM (Option SemiringExpr) := do
-  sreifyCore? e
-
-end  Lean.Meta.Grind.Arith.CommRing
+end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/ToExpr.lean

@@ -8,7 +8,7 @@ prelude
 public import Init.Grind.Ring.CommSemiringAdapter
 public import Lean.ToExpr
 public section
-namespace Lean.Meta.Grind.Arith.CommRing
+namespace Lean.Meta.Sym.Arith
 open Grind.CommRing
 /-!
 `ToExpr` instances for `CommRing.Poly` types.
@@ -57,4 +57,4 @@ instance : ToExpr CommRing.Expr where
   toExpr := ofRingExpr
   toTypeExpr := mkConst ``CommRing.Expr
 
-end Lean.Meta.Grind.Arith.CommRing
+end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/Types.lean

@@ -0,0 +1,160 @@
+/-
+Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Init.Grind.Ring.CommSemiringAdapter
+public import Lean.Meta.Sym.SymM
+public section
+
+namespace Lean.Meta.Sym.Arith
+export Lean.Grind.CommRing (Var Power Mon Poly)
+abbrev RingExpr := Grind.CommRing.Expr
+/-
+**Note**: recall that we use ring expressions to represent semiring expressions,
+and ignore non-applicable constructors.
+-/
+abbrev SemiringExpr := Grind.CommRing.Expr
+
+/-- Classification state for a type with a `Semiring` instance. -/
+structure Semiring where
+  id             : Nat
+  type           : Expr
+  /-- Cached `getDecLevel type` -/
+  u              : Level
+  /-- `Semiring` instance for `type` -/
+  semiringInst   : Expr
+  addFn?         : Option Expr := none
+  mulFn?         : Option Expr := none
+  powFn?         : Option Expr := none
+  natCastFn?     : Option Expr := none
+  deriving Inhabited
+
+/-- Classification state for a type with a `Ring` instance. -/
+structure Ring where
+  id             : Nat
+  type           : Expr
+  /-- Cached `getDecLevel type` -/
+  u              : Level
+  /-- `Ring` instance for `type` -/
+  ringInst       : Expr
+  /-- `Semiring` instance for `type` -/
+  semiringInst   : Expr
+  /-- `IsCharP` instance for `type` if available. -/
+  charInst?      : Option (Expr × Nat)
+  addFn?         : Option Expr := none
+  mulFn?         : Option Expr := none
+  subFn?         : Option Expr := none
+  negFn?         : Option Expr := none
+  powFn?         : Option Expr := none
+  intCastFn?     : Option Expr := none
+  natCastFn?     : Option Expr := none
+  one?           : Option Expr := none
+  deriving Inhabited
+
+/-- Classification state for a type with a `CommRing` instance. -/
+structure CommRing extends Ring where
+  /-- Inverse function if `fieldInst?` is `some inst` -/
+  invFn?             : Option Expr := none
+  /--
+  If this is a `OfSemiring.Q α` ring, this field contains the
+  `semiringId` for `α`.
+  -/
+  semiringId?        : Option Nat
+  /-- `CommSemiring` instance for `type` -/
+  commSemiringInst   : Expr
+  /-- `CommRing` instance for `type` -/
+  commRingInst       : Expr
+  /-- `NoNatZeroDivisors` instance for `type` if available. -/
+  noZeroDivInst?     : Option Expr
+  /-- `Field` instance for `type` if available. -/
+  fieldInst?         : Option Expr
+  /-- `PowIdentity` instance, the synthesized `CommSemiring` instance, and exponent `p` if available. -/
+  powIdentityInst? : Option (Expr × Expr × Nat) := none
+  deriving Inhabited
+
+/--
+Classification state for a type with a `CommSemiring` instance.
+Recall that `CommSemiring` types are normalized using the `OfSemiring.Q` envelope.
+-/
+structure CommSemiring extends Semiring where
+  /-- Id of the envelope ring `OfSemiring.Q type` -/
+  ringId              : Nat
+  /-- `CommSemiring` instance for `type` -/
+  commSemiringInst    : Expr
+  /-- `AddRightCancel` instance for `type` if available. -/
+  addRightCancelInst? : Option Expr := none
+  toQFn?              : Option Expr := none
+  deriving Inhabited
+
+/-- Result of classifying a type's algebraic structure. -/
+inductive ClassifyResult where
+  | commRing (id : Nat)
+  | nonCommRing (id : Nat)
+  | commSemiring (id : Nat)
+  | nonCommSemiring (id : Nat)
+  | /-- No algebraic structure found. -/ none
+  deriving Inhabited
+
+def ClassifyResult.toOption : ClassifyResult → Option Nat
+ | .commRing id | .nonCommRing id
+ | .commSemiring id | .nonCommSemiring id => some id
+ | .none => .none
+
+/-- Arith type classification state, stored as a `SymExtension`. -/
+structure State where
+  /-- Exponent threshold for `HPow` evaluation. -/
+  exp            : Nat := 8
+  /-- Commutative rings. -/
+  rings          : Array CommRing := {}
+  /-- Commutative semirings. -/
+  semirings      : Array CommSemiring := {}
+  /-- Non-commutative rings. -/
+  ncRings        : Array Ring := {}
+  /-- Non-commutative semirings. -/
+  ncSemirings    : Array Semiring := {}
+  /-- Mapping from types to their classification result. Caches failures as `.none`. -/
+  typeClassify   : PHashMap ExprPtr ClassifyResult := {}
+  deriving Inhabited
+
+builtin_initialize arithExt : SymExtension State ← registerSymExtension (return {})
+
+def getArithState : SymM State :=
+  arithExt.getState
+
+@[inline] def modifyArithState (f : State → State) : SymM Unit :=
+  arithExt.modifyState f
+
+/-- Get the exponent threshold. -/
+def getExpThreshold : SymM Nat :=
+  return (← getArithState).exp
+
+/-- Set the exponent threshold. -/
+def setExpThreshold (exp : Nat) : SymM Unit :=
+  modifyArithState fun s => { s with exp }
+
+/-- Run `k` with a temporary exponent threshold. -/
+def withExpThreshold (exp : Nat) (k : SymM α) : SymM α := do
+  let oldExp := (← getArithState).exp
+  setExpThreshold exp
+  try k finally setExpThreshold oldExp
+
+def getCommRingOfId (id : Nat) : SymM CommRing := do
+  let s ← getArithState
+  return s.rings[id]!
+
+def getNonCommRingOfId (id : Nat) : SymM Ring := do
+  let s ← getArithState
+  return s.ncRings[id]!
+
+def getCommSemiringOfId (id : Nat) : SymM CommSemiring := do
+  let s ← getArithState
+  return s.semirings[id]!
+
+def getNonCommSemiringOfId (id : Nat) : SymM Semiring := do
+  let s ← getArithState
+  return s.ncSemirings[id]!
+
+end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Canon.lean

@@ -24,10 +24,19 @@ builtin_initialize registerTraceClass `sym.debug.canon
 
 Canonicalizes expressions by normalizing types and instances. At the top level, it traverses
 applications, foralls, lambdas, and let-bindings, classifying each argument as a type, instance,
-implicit, or value using `shouldCanon`. Values are recursively visited but not normalized.
-Types and instances receive targeted reductions.
+implicit, or value using `shouldCanon`. Targeted reductions (projection, match/ite/cond, Nat
+arithmetic) are applied to all positions; instances are re-synthesized.
 
-## Reductions (applied only in type positions)
+**Note about types:** `grind` is not built for reasoning about types that are not propositions.
+We assume that definitionally equal types will be structurally identical after we apply the
+canonicalizer. We also erase most of the subsingleton markers occurring inside types.
+
+## Reductions
+
+It also normalizes expressions using the following reductions. We can view it as a cheap/custom `dsimp`.
+We used to reduce only terms inside types, but it restricted important normalizations that were important
+when, for example, a term had a forward dependency. That is, the term is not directly in a type, but
+there is a type that depends on it.
 
 - **Eta**: `fun x => f x` → `f`
 - **Projection**: `⟨a, b⟩.1` → `a` (structure projections, not class projections)
@@ -35,11 +44,30 @@ Types and instances receive targeted reductions.
 - **Nat arithmetic**: ground evaluation (`2 + 1` → `3`) and offset normalization
   (`n.succ + 1` → `n + 2`)
 
+**Note**: Eta is applied only if the lambda is occurring inside of a type. For lambdas occurring
+in non type positions, we want to leverage the support in `grind` for lambda-expressions.
+
 ## Instance canonicalization
 
 Instances are re-synthesized via `synthInstance`. The instance type is first normalized
 using the type-level reductions above, so that `OfNat (Fin (2+1)) 0` and `OfNat (Fin 3) 0`
-produce the same canonical instance.
+produce the same canonical instance. Two special cases:
+
+- **`Decidable` instances** (`Grind.nestedDecidable`): the proposition is recursively
+  canonicalized, then the `Decidable` instance is re-synthesized. If resynthesis fails,
+  the original instance is kept (users often provide these via `haveI`).
+  A `checkDefEqInst` guard is required because structurally different `Decidable` instances
+  are not necessarily definitionally equal.
+
+- **Propositional instances** (`Grind.nestedProof`): the proposition is recursively
+  canonicalized, then the proof is re-synthesized. If resynthesis fails, the original
+  proof is kept. No definitional-equality check is needed thanks to proof irrelevance.
+
+In both cases, resynthesis failure is silent — the original instance or proof is kept.
+Ideally we would report an issue when resynthesis fails inside a type (where structural
+agreement matters most), but in practice users provide non-synthesizable instances via `haveI`,
+and these instances propagate into types through forward dependencies. Reporting failures
+for such instances produces noise that obscures real issues.
 
 ## Two caches
 
@@ -213,7 +241,7 @@ def checkDefEqInst (e : Expr) (inst : Expr) : SymM Expr := do
     return e
   return inst
 
-/-- Canonicalize `e`. Applies targeted reductions in type positions; recursively visits value positions. -/
+/-- Canonicalize `e`. Applies targeted reductions and re-synthesizes instances. -/
 partial def canon (e : Expr) : CanonM Expr := do
   match e with
   | .forallE ..    => withCaching e <| canonForall #[] e
@@ -246,23 +274,91 @@ where
     else
       withReader (fun ctx => { ctx with insideType := true }) <| canon e
 
-  canonInst (e : Expr) : CanonM Expr := do
-    if let some inst := (← get).canon.cacheInsts.get? e then
-      checkDefEqInst e inst
+  /--
+  Canonicalize `e : type` where `e` is an instance by trying to resynthesize `type`.
+  If `report` is `true`, we report an issue when the instance cannot be resynthesized.
+  -/
+  canonInstCore (e : Expr) (type : Expr) (report := true) : CanonM Expr := do
+    let some inst ← Sym.synthInstance? type |
+      if report then
+        reportIssue! "failed to canonicalize instance{indentExpr e}\nfailed to synthesize{indentExpr type}"
+      return e
+    checkDefEqInst e inst
+
+  /--
+  Canonicalize an instance by trying to resynthesize it without caching.
+  Recall that we have special support for `Decidable` and propositional instances.
+  -/
+  canonInst' (e : Expr) (report := true) : CanonM Expr := do
+    /-
+    We normalize the type to make sure `OfNat (Fin (2+1)) 1` and `OfNat (Fin 3) 1` will produce
+    the same instances.
+    -/
+    let type ← inferType e
+    let type' ← canonInsideType' type
+    canonInstCore e type' report
+
+  /-- `withCaching` + `canonInst'` -/
+  canonInst (e : Expr) (report := true) : CanonM Expr := withCaching e do
+    canonInst' e report
+
+  /--
+  Canonicalize a proposition that is also a term instance.
+  Given a term `e` of the form `@Grind.nestedProof prop h`, where `g` is the constant `Grind.nestedProof`,
+  we canonicalize it as follows:
+  1- We recursively canonicalize the proposition `prop`.
+  2- Try to resynthesize the instance, but keep the original one in case of failure since users often
+  provide them using `haveI`.
+  -/
+  canonInstProp (g : Expr) (prop : Expr) (h : Expr) (e : Expr) : CanonM Expr := withCaching e do
+    let prop' ← canon prop
+    if (← read).insideType then
+      /- We suppress reporting here because `haveI`-provided instances propagate into types
+         through forward dependencies, and reporting them produces noise. See module doc. -/
+      canonInstCore h prop' (report := false)
     else
       /-
-      We normalize the type to make sure `OfNat (Fin (2+1)) 1` and `OfNat (Fin 3) 1` will produce
-      the same instances.
+      **Note**: We try to resynthesize the proposition, but if it fails we keep the current one.
+      This may happen because propositional instances are often provided manually using `haveI`.
       -/
-      let type ← inferType e
-      let type' ← canonInsideType' type
-      let some inst ← Sym.synthInstance? type' |
-        reportIssue! "failed to canonicalize instance{indentExpr e}\nfailed to synthesize{indentExpr type'}"
-        return e
-      let inst ← checkDefEqInst e inst
-      -- Remark: we cache result using the type **before** canonicalization.
-      modify fun s => { s with canon.cacheInsts := s.canon.cacheInsts.insert e inst }
-      return inst
+      let h' := (← Sym.synthInstance? prop').getD h
+      /- **Note**: We don't need to check whether `h` and `h'` are definitionally equal because of proof irrelevance. -/
+      return if isSameExpr prop prop' && isSameExpr h h' then e else mkApp2 g prop' h'
+
+  /--
+  Canonicalize a decidable instance without checking the cache.
+  Given a term `e` of the form `@Grind.nestedDecidable prop inst`, where `g` is the constant `Grind.nestedDecidable`,
+  we canonicalize it as follows:
+  1- We recursively canonicalize the proposition `prop`.
+  2- Try to resynthesize the instance, but keep the original one in case of failure since users often
+  provide them using `haveI`.
+  -/
+  canonInstDec' (g : Expr) (prop : Expr) (inst : Expr) (e : Expr) : CanonM Expr := do
+    let prop' ← canon prop
+    let type := mkApp (mkConst ``Decidable) prop'
+    if (← read).insideType then
+      /- See comment in `canonInstProp` for why we suppress reporting here. -/
+      canonInstCore inst type (report := false)
+    else
+      /-
+      **Note**: We try to resynthesize the instance, but if it fails we keep the current one.
+      We use `checkDefEqInst` here because two structurally different decidable instances are not necessarily
+      definitionally equal.
+      This may happen because propositional instances are often provided manually using `haveI`.
+      -/
+      let inst' := (← Sym.synthInstance? type).getD inst
+      let inst' ← checkDefEqInst inst inst'
+      return if isSameExpr prop prop' && isSameExpr inst inst' then e else mkApp2 g prop' inst'
+
+  /-- `withCaching` + `canonInstDec'` -/
+  canonInstDec (g : Expr) (prop : Expr) (h : Expr) (e : Expr) : CanonM Expr := withCaching e do
+    canonInstDec' g prop h e
+
+  /-- `canonInstDec` variant for normalizing `if-then-else` expressions. -/
+  canonInstDecCore (e : Expr) : CanonM Expr := do
+    match_expr e with
+    | g@Grind.nestedDecidable prop inst => canonInstDec g prop inst e
+    | _  => canonInst e (report := false)
 
   canonLambda (e : Expr) : CanonM Expr := do
     if (← read).insideType then
@@ -295,60 +391,56 @@ where
       mkLetFVars (generalizeNondepLet := false) fvars (← canon (e.instantiateRev fvars))
 
   canonAppDefault (e : Expr) : CanonM Expr := e.withApp fun f args => do
-    if f.isConstOf ``Grind.nestedProof && args.size == 2 then
-      let prop := args[0]!
-      let prop' ← canon prop
-      let e' := if isSameExpr prop prop' then e else mkAppN f (args.set! 0 prop')
-      return e'
-    else if f.isConstOf ``Grind.nestedDecidable && args.size == 2 then
-      let prop := args[0]!
-      let prop' ← canon prop
-      let e' := if isSameExpr prop prop' then e else mkAppN f (args.set! 0 prop')
-      return e'
+    if args.size == 2 then
+      if f.isConstOf ``Grind.nestedProof then
+        /- **Note**: We don't have special treatment if `e` inside a type. -/
+        let prop := args[0]!
+        let prop' ← canon prop
+        let e' := if isSameExpr prop prop' then e else mkApp2 f prop' args[1]!
+        return e'
+      else if f.isConstOf ``Grind.nestedDecidable then
+        return (← canonInstDec' f args[0]! args[1]! e)
+    let mut modified := false
+    let args ← if f.isConstOf ``OfNat.ofNat then
+      let some args ← normOfNatArgs? args | pure args
+      modified := true
+      pure args
     else
-      let mut modified := false
-      let args ← if f.isConstOf ``OfNat.ofNat then
-        let some args ← normOfNatArgs? args | pure args
+      pure args
+    let mut f := f
+    let f' ← canon f
+    unless isSameExpr f f' do
+      f := f'
+      modified := true
+    let pinfos := (← getFunInfo f).paramInfo
+    let mut args := args.toVector
+    for h : i in *...args.size do
+      let arg := args[i]
+      trace[sym.debug.canon] "[{repr (← shouldCanon pinfos i arg)}]: {arg} : {← inferType arg}"
+      let arg' ← match (← shouldCanon pinfos i arg) with
+        | .canonType =>
+          /-
+          The type may have nested propositions and terms that may need to be canonicalized too.
+          So, we must recurse over it. See issue #10232
+          -/
+          canonInsideType' arg
+        | .canonImplicit => canon arg
+        | .visit => canon arg
+        | .canonInst =>
+          match_expr arg with
+          | g@Grind.nestedDecidable prop h => canonInstDec g prop h arg
+          | g@Grind.nestedProof prop h => canonInstProp g prop h arg
+          | _ => canonInst arg
+      unless isSameExpr arg arg' do
+        args := args.set i arg'
         modified := true
-        pure args
-      else
-        pure args
-      let mut f := f
-      let f' ← canon f
-      unless isSameExpr f f' do
-        f := f'
-        modified := true
-      let pinfos := (← getFunInfo f).paramInfo
-      let mut args := args.toVector
-      for h : i in *...args.size do
-        let arg := args[i]
-        trace[sym.debug.canon] "[{repr (← shouldCanon pinfos i arg)}]: {arg} : {← inferType arg}"
-        let arg' ← match (← shouldCanon pinfos i arg) with
-          | .canonType =>
-            /-
-            The type may have nested propositions and terms that may need to be canonicalized too.
-            So, we must recurse over it. See issue #10232
-            -/
-            canonInsideType' arg
-          | .canonImplicit => canon arg
-          | .visit => canon arg
-          | .canonInst =>
-            if arg.isAppOfArity ``Grind.nestedDecidable 2 then
-              let prop := arg.appFn!.appArg!
-              let prop' ← canon prop
-              if isSameExpr prop prop' then pure arg else pure (mkApp2 arg.appFn!.appFn! prop' arg.appArg!)
-            else
-              canonInst arg
-        unless isSameExpr arg arg' do
-          args := args.set i arg'
-          modified := true
-      return if modified then mkAppN f args.toArray else e
+    return if modified then mkAppN f args.toArray else e
 
   canonIte (f : Expr) (α c inst a b : Expr) : CanonM Expr := do
     let c ← canon c
     if isTrueCond c then canon a
     else if isFalseCond c then canon b
-    else return mkApp5 f (← canonInsideType α) c (← canonInst inst) (← canon a) (← canon b)
+    else return mkApp5 f (← canonInsideType α) c (← canonInstDecCore inst) (← canon a) (← canon b)
 
   canonCond (f : Expr) (α c a b : Expr) : CanonM Expr := do
     let c ← canon c
@@ -389,30 +481,24 @@ where
         return e
 
   canonApp (e : Expr) : CanonM Expr := do
-    if (← read).insideType then
-      match_expr e with
-      | f@ite α c i a b => canonIte f α c i a b
-      | f@cond α c a b => canonCond f α c a b
-      -- Remark: We currently don't normalize dependent-if-then-else occurring in types.
-      | _ =>
-        let f := e.getAppFn
-        let .const declName _ := f | canonAppAndPost e
-        if (← isMatcher declName) then
-          canonMatch e
-        else
-          canonAppAndPost e
-    else
-      canonAppDefault e
+    match_expr e with
+    | f@ite α c i a b => canonIte f α c i a b
+    | f@cond α c a b => canonCond f α c a b
+    -- Remark: We currently don't normalize dependent-if-then-else occurring in types.
+    | _ =>
+      let f := e.getAppFn
+      let .const declName _ := f | canonAppAndPost e
+      if (← isMatcher declName) then
+        canonMatch e
+      else
+        canonAppAndPost e
 
   canonProj (e : Expr) : CanonM Expr := do
     let e := e.updateProj! (← canon e.projExpr!)
-    if (← read).insideType then
-      return (← reduceProj? e).getD e
-    else
-      return e
+    return (← reduceProj? e).getD e
 
 /--
-Returns `true` if `shouldCannon pinfos i arg` is not `.visit`.
+Returns `true` if `shouldCanon pinfos i arg` is not `.visit`.
 This is a helper function used to implement mbtc.
 -/
 public def isSupport (pinfos : Array ParamInfo) (i : Nat) (arg : Expr) : MetaM Bool := do
@@ -423,8 +509,8 @@ end Canon
 
 /--
 Canonicalize `e` by normalizing types, instances, and support arguments.
-Types receive targeted reductions (eta, projection, match/ite, Nat arithmetic).
-Instances are re-synthesized. Values are traversed but not reduced.
+Applies targeted reductions (projection, match/ite/cond, Nat arithmetic) in all positions;
+eta reduction is applied only inside types. Instances are re-synthesized.
 Runs at reducible transparency.
 -/
 public def canon (e : Expr) : SymM Expr := do profileitM Exception "sym canon" (← getOptions) do

src/Lean/Meta/Sym/InstantiateS.lean

@@ -86,22 +86,8 @@ It assumes the input is maximally shared, and ensures the output is too.
 public def instantiateS  (e : Expr) (subst : Array Expr) : SymM Expr :=
   liftBuilderM <| instantiateS' e subst
 
-/-- `mkAppRevRangeS f b e args == mkAppRev f (revArgs.extract b e)` -/
-def mkAppRevRangeS (f : Expr) (beginIdx endIdx : Nat) (revArgs : Array Expr) : AlphaShareBuilderM Expr :=
-  loop revArgs beginIdx f endIdx
-where
-  loop (revArgs : Array Expr) (start : Nat) (b : Expr) (i : Nat) : AlphaShareBuilderM Expr := do
-  if i ≤ start then
-    return b
-  else
-    let i := i - 1
-    loop revArgs start (← mkAppS b revArgs[i]!) i
-
-/--
-Beta-reduces `f` applied to reversed arguments `revArgs`, ensuring maximally shared terms.
-`betaRevS f #[a₃, a₂, a₁]` computes the beta-normal form of `f a₁ a₂ a₃`.
--/
-partial def betaRevS (f : Expr) (revArgs : Array Expr) : AlphaShareBuilderM Expr :=
+/-- Internal variant of `betaRevS` that runs in `AlphaShareBuilderM`. -/
+private partial def betaRevS' (f : Expr) (revArgs : Array Expr) : AlphaShareBuilderM Expr :=
   if revArgs.size == 0 then
     return f
   else
@@ -173,7 +159,7 @@ where
     | .bvar bidx =>
       let f' ← visitBVar f bidx offset
       if modified || !isSameExpr f f' then
-        betaRevS f' argsRev
+        betaRevS' f' argsRev
       else
         return e
     | _ => unreachable!
@@ -215,4 +201,18 @@ public def instantiateRevBetaS (e : Expr) (subst : Array Expr) : SymM Expr := do
   if !e.hasLooseBVars || subst.isEmpty then return e
   else liftBuilderM <| instantiateRevBetaS' e subst
 
+/--
+Beta-reduces `f` applied to reversed arguments `revArgs`, ensuring maximally shared terms.
+`betaRevS f #[a₃, a₂, a₁]` computes the beta-normal form of `f a₁ a₂ a₃`.
+-/
+public def betaRevS (f : Expr) (revArgs : Array Expr) : SymM Expr :=
+  liftBuilderM <| betaRevS' f revArgs
+
+/--
+Apply the given arguments to `f`, beta-reducing if `f` is a lambda expression,
+ensuring maximally shared terms. See `betaRevS` for details.
+-/
+public def betaS (f : Expr) (args : Array Expr) : SymM Expr :=
+  betaRevS f args.reverse
+
 end Lean.Meta.Sym

src/Lean/Meta/Sym/SymM.lean

@@ -152,8 +152,6 @@ structure Canon.State where
   cache       : Std.HashMap Expr Expr := {}
   /-- Cache for type-level canonicalization (reductions applied). -/
   cacheInType : Std.HashMap Expr Expr := {}
-  /-- Cache mapping instances to their canonical synthesized instances. -/
-  cacheInsts  : Std.HashMap Expr Expr := {}
 
 /-- Mutable state for the symbolic computation framework. -/
 structure State where

src/Lean/Meta/Tactic/Cbv/ControlFlow.lean

@@ -44,7 +44,7 @@ def isCbvNoncomputable (p : Name) : CoreM Bool := do
   return evalLemmas.isNone && Lean.isNoncomputable (← getEnv) p
 
 /--
-Attemps to synthesize `Decidable p` instance and guards against picking up a `noncomputable` instance
+Attempts to synthesize `Decidable p` instance and guards against picking up a `noncomputable` instance
 -/
 def trySynthComputableInstance (p : Expr) : SymM <| Option Expr := do
   let .some inst' ← trySynthInstance (mkApp (mkConst ``Decidable) p) | return .none
@@ -112,7 +112,7 @@ builtin_cbv_simproc ↓ simpIteCbv (@ite _ _ _ _ _) := fun e => do
       else if (← isFalseExpr c') then
         return .step b (mkApp (e.replaceFn ``ite_cond_eq_false) h) (contextDependent := cd)
       else
-        -- If we got stuck with simplifying `p` then let's try evaluating the original isntance
+        -- If we got stuck with simplifying `p` then let's try evaluating the original instance
         simpAndMatchIteDecidable f α c inst a b do
           -- If we get stuck here, maybe the problem is that we need to look at `Decidable c'`
           let inst' := mkApp4 (mkConst ``decidable_of_decidable_of_eq) c c' inst h
@@ -317,7 +317,7 @@ public def reduceRecMatcher : Simproc := fun e => do
   else
     return .rfl
 
-builtin_cbv_simproc ↓ simpDecidableRec (@Decidable.rec _ _ _ _ _) := 
+builtin_cbv_simproc ↓ simpDecidableRec (@Decidable.rec _ _ _ _ _) :=
   (simpInterlaced · #[false,false,false,false,true]) >> reduceRecMatcher
 
 def tryMatchEquations (appFn : Name) : Simproc := fun e => do

src/Lean/Meta/Tactic/Cbv/Main.lean

@@ -272,7 +272,7 @@ def handleProj : Simproc := fun e => do
         let reduced ← Sym.share reduced
         return .step reduced (← Sym.mkEqRefl reduced)
       | .none =>
-       -- If we failed to reduce it, we turn to a last resort; we try use heterogenous congruence lemma that we then try to turn into an equality.
+       -- If we failed to reduce it, we turn to a last resort; we try use heterogeneous congruence lemma that we then try to turn into an equality.
         unless (← isDefEq struct e') do
           -- If we rewrote the projection body using something that holds up to propositional equality, then there is nothing we can do.
           -- TODO: Check if there is a need to report this to a user, or shall we fail silently.
@@ -283,6 +283,7 @@ def handleProj : Simproc := fun e => do
         let newProof ← mkEqOfHEq newProof (check := false)
         return .step (← Lean.Expr.updateProjS! e e') newProof
 
+open Sym.Internal in
 /--
 For an application whose head is neither a constant nor a lambda (e.g. a projection
 like `p.1 x`), simplify the function head and lift the proof via `congrArg`.

src/Lean/Meta/Tactic/Cbv/Util.lean

@@ -24,9 +24,6 @@ namespace Lean.Meta.Tactic.Cbv
 
 open Lean.Meta.Sym.Simp
 
-public def mkAppNS (f : Expr) (args : Array Expr) : Sym.SymM Expr := do
-  args.foldlM Sym.Internal.mkAppS f
-
 abbrev isNatValue (e : Expr) : Bool := (Sym.getNatValue? e).isSome
 abbrev isStringValue (e : Expr) : Bool := (Sym.getStringValue? e).isSome
 abbrev isIntValue (e : Expr) : Bool := (Sym.getIntValue? e).isSome

src/Lean/Meta/Tactic/Grind/Arith/CommRing.lean

@@ -5,28 +5,19 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Internalize
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.SemiringM
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommRingM
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommSemiringM
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.EqCnstr
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Inv
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.PP
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadCanon
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadSemiring
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Action
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Power
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Denote
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 builtin_initialize registerTraceClass `grind.ring

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Denote.lean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
+public import Lean.Meta.Sym.Arith.DenoteExpr
+
+namespace Lean.Meta.Grind.Arith.CommRing
+open Sym.Arith
+/-!
+Helper functions for converting reified terms back into their denotations.
+-/
+
+variable [Monad M] [MonadGetVar M] [MonadError M] [MonadLiftT MetaM M] [MonadCanon M] [MonadRing M]
+
+def mkEq (a b : Expr) : M Expr := do
+  let r ← getRing
+  return mkApp3 (mkConst ``Eq [r.u.succ]) r.type a b
+
+public def EqCnstr.denoteExpr (c : EqCnstr) : M Expr := do
+  mkEq (← denotePoly c.p) (← denoteNum 0)
+
+public def PolyDerivation.denoteExpr (d : PolyDerivation) : M Expr := do
+  denotePoly d.p
+
+public def DiseqCnstr.denoteExpr (c : DiseqCnstr) : M Expr := do
+  return mkNot (← mkEq (← c.d.denoteExpr) (← denoteNum 0))
+
+end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean

@@ -1,99 +0,0 @@
-/-
-Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
-public section
-namespace Lean.Meta.Grind.Arith.CommRing
-/-!
-Helper functions for converting reified terms back into their denotations.
--/
-
-variable [Monad M] [MonadError M] [MonadLiftT MetaM M] [MonadCanon M] [MonadRing M]
-
-def denoteNum (k : Int) : M Expr := do
-  let ring ← getRing
-  let n := mkRawNatLit k.natAbs
-  let ofNatInst ← if let some inst ← synthInstance? (mkApp2 (mkConst ``OfNat [ring.u]) ring.type n) then
-    pure inst
-  else
-    pure <| mkApp3 (mkConst ``Grind.Semiring.ofNat [ring.u]) ring.type ring.semiringInst n
-  let n := mkApp3 (mkConst ``OfNat.ofNat [ring.u]) ring.type n ofNatInst
-  if k < 0 then
-    return mkApp (← getNegFn) n
-  else
-    return n
-
-def _root_.Lean.Grind.CommRing.Power.denoteExpr (pw : Power) : M Expr := do
-  let x := (← getRing).vars[pw.x]!
-  if pw.k == 1 then
-    return x
-  else
-    return mkApp2 (← getPowFn) x (toExpr pw.k)
-
-def _root_.Lean.Grind.CommRing.Mon.denoteExpr (m : Mon) : M Expr := do
-  match m with
-  | .unit => denoteNum 1
-  | .mult pw m => go m (← pw.denoteExpr)
-where
-  go (m : Mon) (acc : Expr) : M Expr := do
-    match m with
-    | .unit => return acc
-    | .mult pw m => go m (mkApp2 (← getMulFn) acc (← pw.denoteExpr))
-
-def _root_.Lean.Grind.CommRing.Poly.denoteExpr (p : Poly) : M Expr := do
-  match p with
-  | .num k => denoteNum k
-  | .add k m p => go p (← denoteTerm k m)
-where
-  denoteTerm (k : Int) (m : Mon) : M Expr := do
-    if k == 1 then
-      m.denoteExpr
-    else
-      return mkApp2 (← getMulFn) (← denoteNum k) (← m.denoteExpr)
-
-  go (p : Poly) (acc : Expr) : M Expr := do
-    match p with
-    | .num 0 => return acc
-    | .num k => return mkApp2 (← getAddFn) acc (← denoteNum k)
-    | .add k m p => go p (mkApp2 (← getAddFn) acc (← denoteTerm k m))
-
-@[specialize]
-private def denoteExprCore (getVar : Nat → Expr) (e : RingExpr) : M Expr := do
-  go e
-where
-  go : RingExpr → M Expr
-  | .num k => denoteNum k
-  | .natCast k => return mkApp (← getNatCastFn) (mkNatLit k)
-  | .intCast k => return mkApp (← getIntCastFn) (mkIntLit k)
-  | .var x => return getVar x
-  | .add a b => return mkApp2 (← getAddFn) (← go a) (← go b)
-  | .sub a b => return mkApp2 (← getSubFn) (← go a) (← go b)
-  | .mul a b => return mkApp2 (← getMulFn) (← go a) (← go b)
-  | .pow a k => return mkApp2 (← getPowFn) (← go a) (toExpr k)
-  | .neg a => return mkApp (← getNegFn) (← go a)
-
-def _root_.Lean.Grind.CommRing.Expr.denoteExpr (e : RingExpr) : M Expr := do
-  let ring ← getRing
-  denoteExprCore (fun x => ring.vars[x]!) e
-
-def _root_.Lean.Grind.CommRing.Expr.denoteExpr' (vars : Array Expr) (e : RingExpr) : M Expr := do
-  denoteExprCore (fun x => vars[x]!) e
-
-private def mkEq (a b : Expr) : M Expr := do
-  let r ← getRing
-  return mkApp3 (mkConst ``Eq [r.u.succ]) r.type a b
-
-def EqCnstr.denoteExpr (c : EqCnstr) : M Expr := do
-  mkEq (← c.p.denoteExpr) (← denoteNum 0)
-
-def PolyDerivation.denoteExpr (d : PolyDerivation) : M Expr := do
-  d.p.denoteExpr
-
-def DiseqCnstr.denoteExpr (c : DiseqCnstr) : M Expr := do
-  return mkNot (← mkEq (← c.d.denoteExpr) (← denoteNum 0))
-
-end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean

@@ -9,9 +9,7 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 import Lean.Meta.Tactic.Grind.Diseq
 import Lean.Meta.Tactic.Grind.Arith.Util
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
-import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Inv
-import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
 import Lean.Meta.Tactic.Grind.Arith.CommRing.SafePoly
 public section
 namespace Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean

@@ -6,12 +6,16 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
+import Lean.Meta.Sym.Arith.Reify
+import Lean.Meta.Sym.Arith.DenoteExpr
+import Lean.Meta.Tactic.Grind.Arith.CommRing.SemiringM
+import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommRingM
+import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommSemiringM
 import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.Arith.Util
-import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
-import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
+open Sym Arith
 
 /-- If `e` is a function application supported by the `CommRing` module, return its type. -/
 private def getType? (e : Expr) : Option Expr :=
@@ -80,8 +84,8 @@ private def processInv (e inst a : Expr) : RingM Unit := do
   unless (← isInvInst inst) do return ()
   let ring ← getCommRing
   let some fieldInst := ring.fieldInst? | return ()
-  if (← getCommRing).invSet.contains a then return ()
-  modifyCommRing fun s => { s with invSet := s.invSet.insert a }
+  if (← getCommRingEntry).invSet.contains a then return ()
+  modifyCommRingEntry fun s => { s with invSet := s.invSet.insert a }
   if let some k ← toInt? a then
     if k == 0 then
       /-
@@ -112,6 +116,26 @@ private def processInv (e inst a : Expr) : RingM Unit := do
       return ()
   pushNewFact <| mkApp3 (mkConst ``Grind.CommRing.inv_split [ring.u]) ring.type fieldInst a
 
+/--
+For each new variable `x` in a ring with `PowIdentity α p`,
+push the equation `x ^ p = x` as a new fact into grind.
+-/
+private def processPowIdentityVars : RingM Unit := do
+  let ring ← getCommRing
+  let some (powIdentityInst, csInst, p) := ring.powIdentityInst? | return ()
+  let ringEntry ← getCommRingEntry
+  let startIdx := ringEntry.powIdentityVarCount
+  let vars := ringEntry.vars
+  if startIdx >= vars.size then return ()
+  for i in [startIdx:vars.size] do
+    let x := vars[i]!
+    trace_goal[grind.ring] "PowIdentity: pushing x^{p} = x for {x}"
+    -- Construct proof: @PowIdentity.pow_eq α csInst p powIdentityInst x
+    let proof := mkApp5 (mkConst ``Grind.PowIdentity.pow_eq [ring.u])
+      ring.type csInst (mkNatLit p) powIdentityInst x
+    pushNewFact proof
+  modifyCommRingEntry fun s => { s with powIdentityVarCount := vars.size }
+
 /-- Returns `true` if `e` is a term `a⁻¹`. -/
 private def internalizeInv (e : Expr) : GoalM Bool := do
   match_expr e with
@@ -129,32 +153,34 @@ def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
   if (← internalizeInv e) then return ()
   let some type := getType? e | return ()
   if isForbiddenParent parent? then return ()
+  let gen ← getGeneration e
   if let some ringId ← getCommRingId? type then RingM.run ringId do
-    let some re ← reify? e | return ()
+    let some re ← reifyRing? e (gen := gen) | return ()
     trace_goal[grind.ring.internalize] "[{ringId}]: {e}"
     setTermRingId e
     ringExt.markTerm e
-    modifyCommRing fun s => { s with
+    modifyCommRingEntry fun s => { s with
       denote := s.denote.insert { expr := e } re
       denoteEntries := s.denoteEntries.push (e, re)
     }
+    processPowIdentityVars
   else if let some semiringId ← getCommSemiringId? type then SemiringM.run semiringId do
-    let some re ← sreify? e | return ()
+    let some re ← reifySemiring? e (gen := gen) | return ()
     trace_goal[grind.ring.internalize] "semiring [{semiringId}]: {e}"
     setTermSemiringId e
     ringExt.markTerm e
-    modifySemiring fun s => { s with denote := s.denote.insert { expr := e } re }
+    modifyCommSemiringEntry fun s => { s with denote := s.denote.insert { expr := e } re }
   else if let some ncRingId ← getNonCommRingId? type then NonCommRingM.run ncRingId do
-    let some re ← ncreify? e | return ()
+    let some re ← reifyRing? e (gen := gen) | return ()
     trace_goal[grind.ring.internalize] "(non-comm) ring [{ncRingId}]: {e}"
     setTermNonCommRingId e
     ringExt.markTerm e
-    modifyRing fun s => { s with denote := s.denote.insert { expr := e } re }
+    modifyRingEntry fun s => { s with denote := s.denote.insert { expr := e } re }
   else if let some ncSemiringId ← getNonCommSemiringId? type then NonCommSemiringM.run ncSemiringId do
-    let some re ← ncsreify? e | return ()
+    let some re ← reifySemiring? e (gen := gen) | return ()
     trace_goal[grind.ring.internalize] "(non-comm) semiring [{ncSemiringId}]: {e}"
     setTermNonCommSemiringId e
     ringExt.markTerm e
-    modifySemiring fun s => { s with denote := s.denote.insert { expr := e } re }
+    modifySemiringEntry fun s => { s with denote := s.denote.insert { expr := e } re }
 
 end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Inv.lean

@@ -6,10 +6,10 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
-import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
+import Lean.Meta.Sym.Arith.Poly
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-
+/-
 private def checkVars : RingM Unit := do
   let s ← getRing
   let mut num := 0
@@ -42,11 +42,14 @@ private def checkDiseqs : RingM Unit := do
   for c in (← getCommRing).diseqs do
     checkPoly c.d.p
 
+-/
+
 private def checkRingInvs : RingM Unit := do
-  checkVars
-  checkBasis
-  checkQueue
-  checkDiseqs
+  -- checkVars
+  -- checkBasis
+  -- checkQueue
+  -- checkDiseqs
+  return ()
 
 def checkInvariants : GoalM Unit := do
   if (← isDebugEnabled) then

src/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadCanon.lean

@@ -1,37 +0,0 @@
-/-
-Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
-public section
-namespace Lean.Meta.Grind.Arith.CommRing
-
-class MonadCanon (m : Type → Type) where
-  /--
-  Helper function for removing dependency on `GoalM`.
-  In `RingM` and `SemiringM`, this is just `sharedCommon (← canon e)`
-  When printing counterexamples, we are at `MetaM`, and this is just the identity function.
-  -/
-  canonExpr : Expr → m Expr
-  /--
-  Helper function for removing dependency on `GoalM`. During search we
-  want to track the instances synthesized by `grind`, and this is `Grind.synthInstance`.
-  -/
-  synthInstance? : Expr → m (Option Expr)
-
-export MonadCanon (canonExpr)
-
-@[always_inline]
-instance (m n) [MonadLift m n] [MonadCanon m] : MonadCanon n where
-  canonExpr e := liftM (canonExpr e : m Expr)
-  synthInstance? e := liftM (MonadCanon.synthInstance? e : m (Option Expr))
-
-def MonadCanon.synthInstance [Monad m] [MonadError m] [MonadCanon m] (type : Expr) : m Expr := do
-  let some inst ← synthInstance? type
-    | throwError "`grind` failed to find instance{indentExpr type}"
-  return inst
-
-end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/NonCommRingM.lean

@@ -8,31 +8,31 @@ prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
+open Sym.Arith
 
 structure NonCommRingM.Context where
   ringId : Nat
+  symRingId : Nat
 
 /-- We don't want to keep carrying the `RingId` around. -/
 abbrev NonCommRingM := ReaderT NonCommRingM.Context GoalM
 
-abbrev NonCommRingM.run (ringId : Nat) (x : NonCommRingM α) : GoalM α :=
-  x { ringId }
-
-instance : MonadCanon NonCommRingM where
-  canonExpr e := do shareCommon (← canon e)
-  synthInstance? e := Grind.synthInstance? e
+abbrev NonCommRingM.run (ringId : Nat) (x : NonCommRingM α) : GoalM α := do
+  let s ← get'
+  let symRingId := s.ncRings[ringId]!.symId
+  x { ringId, symRingId }
 
 protected def NonCommRingM.getRing : NonCommRingM Ring := do
-  let s ← get'
-  let ringId := (← read).ringId
+  let s ← getArithState
+  let ringId := (← read).symRingId
   if h : ringId < s.ncRings.size then
     return s.ncRings[ringId]
   else
     throwError "`grind` internal error, invalid ringId"
 
 protected def NonCommRingM.modifyRing (f : Ring → Ring) : NonCommRingM Unit := do
-  let ringId := (← read).ringId
-  modify' fun s => { s with ncRings := s.ncRings.modify ringId f }
+  let ringId := (← read).symRingId
+  modifyArithState fun s => { s with ncRings := s.ncRings.modify ringId f }
 
 instance : MonadRing NonCommRingM where
   getRing := NonCommRingM.getRing
@@ -49,7 +49,37 @@ def setTermNonCommRingId (e : Expr) : NonCommRingM Unit := do
     return ()
   modify' fun s => { s with exprToNCRingId := s.exprToNCRingId.insert { expr := e } ringId }
 
-instance : MonadSetTermId NonCommRingM where
-  setTermId e := setTermNonCommRingId e
+def getRingEntry : NonCommRingM RingEntry := do
+  let s ← get'
+  let ringId := (← read).ringId
+  if h : ringId < s.ncRings.size then
+    return s.ncRings[ringId]
+  else
+    throwError "`grind` internal error, invalid ringId"
+
+def modifyRingEntry (f : RingEntry → RingEntry) : NonCommRingM Unit := do
+  let ringId := (← read).ringId
+  modify' fun s => { s with ncRings := s.ncRings.modify ringId f }
+
+def mkNonCommVar (e : Expr) (gen : Nat) : NonCommRingM Var := do
+  unless (← alreadyInternalized e) do
+    internalize e gen
+  let s ← getRingEntry
+  if let some var := s.varMap.find? { expr := e } then
+    return var
+  let var : Var := s.vars.size
+  modifyRingEntry fun s => { s with
+    vars       := s.vars.push e
+    varMap     := s.varMap.insert { expr := e } var
+  }
+  setTermNonCommRingId e
+  ringExt.markTerm e
+  return var
+
+instance : MonadMkVar NonCommRingM where
+  mkVar := mkNonCommVar
+
+instance : MonadGetVar NonCommRingM where
+  getVar x := return (← getRingEntry).vars[x]!
 
 end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/NonCommSemiringM.lean

@@ -8,20 +8,36 @@ prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.SemiringM
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
+open Sym.Arith
 
 structure NonCommSemiringM.Context where
   semiringId : Nat
+  symSemiringId : Nat
 
 abbrev NonCommSemiringM := ReaderT NonCommSemiringM.Context GoalM
 
-abbrev NonCommSemiringM.run (semiringId : Nat) (x : NonCommSemiringM α) : GoalM α :=
-  x { semiringId }
-
-instance : MonadCanon NonCommSemiringM where
-  canonExpr e := do shareCommon (← canon e)
-  synthInstance? e := Grind.synthInstance? e
+abbrev NonCommSemiringM.run (semiringId : Nat) (x : NonCommSemiringM α) : GoalM α := do
+  let s ← get'
+  let symSemiringId := s.ncSemirings[semiringId]!.symId
+  x { semiringId, symSemiringId }
 
 protected def NonCommSemiringM.getSemiring : NonCommSemiringM Semiring := do
+  let s ← getArithState
+  let semiringId := (← read).symSemiringId
+  if h : semiringId < s.ncSemirings.size then
+    return s.ncSemirings[semiringId]
+  else
+    throwError "`grind` internal error, invalid semiringId"
+
+protected def NonCommSemiringM.modifySemiring (f : Semiring → Semiring) : NonCommSemiringM Unit := do
+  let semiringId := (← read).symSemiringId
+  modifyArithState fun s => { s with ncSemirings := s.ncSemirings.modify semiringId f }
+
+instance : MonadSemiring NonCommSemiringM where
+  getSemiring := NonCommSemiringM.getSemiring
+  modifySemiring := NonCommSemiringM.modifySemiring
+
+def getSemiringEntry : NonCommSemiringM SemiringEntry := do
   let s ← get'
   let semiringId := (← read).semiringId
   if h : semiringId < s.ncSemirings.size then
@@ -29,14 +45,10 @@ protected def NonCommSemiringM.getSemiring : NonCommSemiringM Semiring := do
   else
     throwError "`grind` internal error, invalid semiringId"
 
-protected def NonCommSemiringM.modifySemiring (f : Semiring → Semiring) : NonCommSemiringM Unit := do
+def modifySemiringEntry (f : SemiringEntry → SemiringEntry) : NonCommSemiringM Unit := do
   let semiringId := (← read).semiringId
   modify' fun s => { s with ncSemirings := s.ncSemirings.modify semiringId f }
 
-instance : MonadSemiring NonCommSemiringM where
-  getSemiring := NonCommSemiringM.getSemiring
-  modifySemiring := NonCommSemiringM.modifySemiring
-
 def getTermNonCommSemiringId? (e : Expr) : GoalM (Option Nat) := do
     return (← get').exprToNCSemiringId.find? { expr := e }
 
@@ -48,7 +60,25 @@ def setTermNonCommSemiringId (e : Expr) : NonCommSemiringM Unit := do
     return ()
   modify' fun s => { s with exprToNCSemiringId := s.exprToNCSemiringId.insert { expr := e } semiringId }
 
-instance : MonadSetTermId NonCommSemiringM where
-  setTermId e := setTermNonCommSemiringId e
+def mkNonCommSVar (e : Expr) (gen : Nat) : NonCommSemiringM Var := do
+  unless (← alreadyInternalized e) do
+    internalize e gen
+  let s ← getSemiringEntry
+  if let some var := s.varMap.find? { expr := e } then
+    return var
+  let var : Var := s.vars.size
+  modifySemiringEntry fun s => { s with
+    vars       := s.vars.push e
+    varMap     := s.varMap.insert { expr := e } var
+  }
+  setTermNonCommSemiringId e
+  ringExt.markTerm e
+  return var
+
+instance : MonadMkVar NonCommSemiringM where
+  mkVar := mkNonCommSVar
+
+instance : MonadGetVar NonCommSemiringM where
+  getVar x := return (← getSemiringEntry).vars[x]!
 
 end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/PP.lean

@@ -6,20 +6,26 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
-import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Denote
+import Lean.Meta.Sym.Arith.DenoteExpr
 import Init.Omega
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
+open Sym.Arith
 
-private abbrev M := StateT CommRing MetaM
+private abbrev M := StateT (CommRing × CommRingEntry) MetaM
 
 private instance : MonadCanon M where
   canonExpr e := return e
   synthInstance? e := Meta.synthInstance? e none
 
 private instance : MonadCommRing M where
-  getCommRing := get
-  modifyCommRing := modify
+  getCommRing := return (← get).1
+  modifyCommRing f := modify fun (r, e) => (f r, e)
+
+private instance : MonadGetVar M where
+  getVar x := return (← get).2.vars[x]!
 
 private def toOption (cls : Name) (header : Thunk MessageData) (msgs : Array MessageData) : Option MessageData :=
   if msgs.isEmpty then
@@ -30,15 +36,18 @@ private def toOption (cls : Name) (header : Thunk MessageData) (msgs : Array Mes
 private def push (msgs : Array MessageData) (msg? : Option MessageData) : Array MessageData :=
   if let some msg := msg? then msgs.push msg else msgs
 
+private def getCommRingEntry : M CommRingEntry :=
+  return (← get).2
+
 private def ppBasis? : M (Option MessageData) := do
   let mut basis := #[]
-  for c in (← getCommRing).basis do
+  for c in (← getCommRingEntry).basis do
     basis := basis.push (toTraceElem (← c.denoteExpr))
   return toOption `basis "Basis" basis
 
 private def ppDiseqs? : M (Option MessageData) := do
   let mut diseqs := #[]
-  for d in (← getCommRing).diseqs do
+  for d in (← getCommRingEntry).diseqs do
     diseqs := diseqs.push (toTraceElem (← d.denoteExpr))
   return toOption `diseqs "Disequalities" diseqs
 
@@ -50,9 +59,12 @@ private def ppRing? : M (Option MessageData) := do
 
 def pp? (goal : Goal) : MetaM (Option MessageData) := do
   let mut msgs := #[]
-  for ring in (← ringExt.getStateCore goal).rings do
-    let some msg ← ppRing? |>.run' ring | pure ()
-    msgs := msgs.push msg
+  for ringEntry in (← ringExt.getStateCore goal).rings do
+    -- let ring ← getCommRingOfId ringEntry.symId
+    -- let some msg ← ppRing? |>.run' (_, ringEntry) | pure ()
+    -- msgs := msgs.push msg
+    -- TODO: fix
+    pure ()
   if msgs.isEmpty then
     return none
   else if h : msgs.size = 1 then

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean

@@ -8,16 +8,19 @@ prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommRingM
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommSemiringM
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Denote
 import Lean.Data.RArray
 import Lean.Meta.Tactic.Grind.Diseq
 import Lean.Meta.Tactic.Grind.ProofUtil
-import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
-import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
-import Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename
+import Lean.Meta.Sym.Arith.DenoteExpr
+import Lean.Meta.Sym.Arith.ToExpr
+import Lean.Meta.Sym.Arith.VarRename
 import Init.Data.Nat.Order
 import Init.Data.Order.Lemmas
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
+open Sym.Arith
+
 /--
 Returns a context of type `RArray α` containing the variables `vars` where
 `α` is the type of the ring.
@@ -55,7 +58,7 @@ private def throwNoNatZeroDivisors : RingM α := do
 
 private def getPolyConst (p : Poly) : RingM Int := do
   let .num k := p
-    | throwError "`grind` internal error, constant polynomial expected {indentExpr (← p.denoteExpr)}"
+    | throwError "`grind` internal error, constant polynomial expected {indentExpr (← denotePoly p)}"
   return k
 
 structure ProofM.State where
@@ -133,6 +136,9 @@ private def getSemiringIdOf : RingM Nat := do
 private def getSemiringOf : RingM CommSemiring := do
   SemiringM.run (← getSemiringIdOf) do getCommSemiring
 
+private def getSemiringEntryOf : RingM CommSemiringEntry := do
+  SemiringM.run (← getSemiringIdOf) do getCommSemiringEntry
+
 private def mkSemiringPrefix (declName : Name) : ProofM Expr := do
   let sctx ← getSContext
   let semiring ← getSemiringOf
@@ -141,7 +147,7 @@ private def mkSemiringPrefix (declName : Name) : ProofM Expr := do
 private def mkSemiringAddRightCancelPrefix (declName : Name) : ProofM Expr := do
   let sctx ← getSContext
   let semiring ← getSemiringOf
-  let some addRightCancelInst ← SemiringM.run (← getSemiringIdOf) do getAddRightCancelInst?
+  let some addRightCancelInst ← SemiringM.run (← getSemiringIdOf) do return (← getCommSemiring).addRightCancelInst?
     | throwError "`grind` internal error, `AddRightCancel` instance is not available"
   return mkApp4 (mkConst declName [semiring.u]) semiring.type semiring.semiringInst addRightCancelInst sctx
 
@@ -239,7 +245,7 @@ private def mkContext (h : Expr) : ProofM Expr := do
     collectMapVars (← get).exprDecls (·.collectVars) <| {}
   let vars'        := usedVars.toArray
   let varRename    := mkVarRename vars'
-  let vars         := (← getRing).vars
+  let vars         := (← getCommRingEntry).vars
   let vars         := vars'.map fun x => vars[x]!
   let h := mkLetOfMap (← get).polyDecls h `p (mkConst ``Grind.CommRing.Poly) fun p => toExpr <| p.renameVars varRename
   let h := mkLetOfMap (← get).monDecls h `m (mkConst ``Grind.CommRing.Mon) fun m => toExpr <| m.renameVars varRename
@@ -256,11 +262,12 @@ private def mkContext (h : Expr) : ProofM Expr := do
 private def mkSemiringContext (h : Expr) : ProofM Expr := do
   let some sctx := (← read).sctx? | return h
   let some semiringId := (← getCommRing).semiringId? | return h
-  let semiring ← getSemiringOf
+  let semiring      ← getSemiringOf
+  let semiringEntry ← getSemiringEntryOf
   let usedVars     := collectMapVars (← get).sexprDecls (·.collectVars) {}
   let vars'        := usedVars.toArray
   let varRename    := mkVarRename vars'
-  let vars         := vars'.map fun x => semiring.vars[x]!
+  let vars         := vars'.map fun x => semiringEntry.vars[x]!
   let h := mkLetOfMap (← get).sexprDecls h `s (mkConst ``Grind.CommRing.Expr) fun s => toExpr <| s.renameVars varRename
   let h := h.abstract #[sctx]
   if h.hasLooseBVars then
@@ -325,7 +332,7 @@ def setSemiringDiseqUnsat (a b : Expr) (sa sb : SemiringExpr) : SemiringM Unit :
   let usedVars     := sa.collectVars >> sb.collectVars <| {}
   let vars'        := usedVars.toArray
   let varRename    := mkVarRename vars'
-  let vars         := (← getSemiring).vars
+  let vars         := (← getCommSemiringEntry).vars
   let vars         := vars'.map fun x => vars[x]!
   let sa           := sa.renameVars varRename
   let sb           := sb.renameVars varRename
@@ -340,11 +347,12 @@ terms s.t. `ra.toPoly_nc == rb.toPoly_nc`, close the goal.
 -/
 def setNonCommRingDiseqUnsat (a b : Expr) (ra rb : RingExpr) : NonCommRingM Unit := do
   let ring ← getRing
+  let ringEntry ← getRingEntry
   let hne ← mkDiseqProof a b
   let usedVars     := ra.collectVars >> rb.collectVars <| {}
   let vars'        := usedVars.toArray
   let varRename    := mkVarRename vars'
-  let vars         := ring.vars
+  let vars         := ringEntry.vars
   let vars         := vars'.map fun x => vars[x]!
   let ra           := ra.renameVars varRename
   let rb           := rb.renameVars varRename
@@ -362,11 +370,12 @@ terms s.t. `sa.toPolyS_nc == sb.toPolyS_nc`, close the goal.
 -/
 def setNonCommSemiringDiseqUnsat (a b : Expr) (sa sb : SemiringExpr) : NonCommSemiringM Unit := do
   let semiring ← getSemiring
+  let semiringEntry ← getSemiringEntry
   let hne ← mkDiseqProof a b
   let usedVars     := sa.collectVars >> sb.collectVars <| {}
   let vars'        := usedVars.toArray
   let varRename    := mkVarRename vars'
-  let vars         := semiring.vars
+  let vars         := semiringEntry.vars
   let vars         := vars'.map fun x => vars[x]!
   let sa           := sa.renameVars varRename
   let sb           := sb.renameVars varRename
@@ -395,7 +404,8 @@ private def norm (vars : PArray Expr) (lhs rhs lhs' rhs' : RingExpr) : NormResul
 
 def mkLeIffProof (leInst ltInst isPreorderInst orderedRingInst : Expr) (lhs rhs lhs' rhs' : RingExpr) : RingM Expr := do
   let ring ← getCommRing
-  let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
+  let ringEntry ← getCommRingEntry
+  let { lhs, rhs, lhs', rhs', vars } := norm ringEntry.vars lhs rhs lhs' rhs'
   let ctx ← toContextExpr vars
   let h := mkApp6 (mkConst ``Grind.CommRing.le_norm_expr [ring.u]) ring.type ring.commRingInst leInst ltInst isPreorderInst orderedRingInst
   let h := mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
@@ -407,7 +417,8 @@ def mkLeIffProof (leInst ltInst isPreorderInst orderedRingInst : Expr) (lhs rhs
 
 def mkLtIffProof (leInst ltInst lawfulOrdLtInst isPreorderInst orderedRingInst : Expr) (lhs rhs lhs' rhs' : RingExpr) : RingM Expr := do
   let ring ← getCommRing
-  let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
+  let ringEntry ← getCommRingEntry
+  let { lhs, rhs, lhs', rhs', vars } := norm ringEntry.vars lhs rhs lhs' rhs'
   let ctx ← toContextExpr vars
   let h := mkApp7 (mkConst ``Grind.CommRing.lt_norm_expr [ring.u]) ring.type ring.commRingInst leInst ltInst lawfulOrdLtInst isPreorderInst orderedRingInst
   let h := mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
@@ -419,7 +430,8 @@ def mkLtIffProof (leInst ltInst lawfulOrdLtInst isPreorderInst orderedRingInst :
 
 def mkEqIffProof (lhs rhs lhs' rhs' : RingExpr) : RingM Expr := do
   let ring ← getCommRing
-  let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
+  let ringEntry ← getCommRingEntry
+  let { lhs, rhs, lhs', rhs', vars } := norm ringEntry.vars lhs rhs lhs' rhs'
   let ctx ← toContextExpr vars
   let h := mkApp2 (mkConst ``Grind.CommRing.eq_norm_expr [ring.u]) ring.type ring.commRingInst
   let h := mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
@@ -434,7 +446,8 @@ Given `e` and `e'` s.t. `e.toPoly == e'.toPoly`, returns a proof that `e.denote
 -/
 def mkTermEqProof (e e' : RingExpr) : RingM Expr := do
   let ring ← getCommRing
-  let { lhs, lhs', vars, .. } := norm ring.vars e (.num 0) e' (.num 0)
+  let ringEntry ← getCommRingEntry
+  let { lhs, lhs', vars, .. } := norm ringEntry.vars e (.num 0) e' (.num 0)
   let ctx ← toContextExpr vars
   let h := mkApp2 (mkConst ``Grind.CommRing.Expr.eq_of_toPoly_eq [ring.u]) ring.type ring.commRingInst
   let h := mkApp4 h ctx (toExpr lhs) (toExpr lhs') eagerReflBoolTrue
@@ -444,7 +457,8 @@ def mkTermEqProof (e e' : RingExpr) : RingM Expr := do
 
 def mkNonCommLeIffProof (leInst ltInst isPreorderInst orderedRingInst : Expr) (lhs rhs lhs' rhs' : RingExpr) : NonCommRingM Expr := do
   let ring ← getRing
-  let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
+  let ringEntry ← getRingEntry
+  let { lhs, rhs, lhs', rhs', vars } := norm ringEntry.vars lhs rhs lhs' rhs'
   let ctx ← toContextExpr vars
   let h := mkApp6 (mkConst ``Grind.CommRing.le_norm_expr_nc [ring.u]) ring.type ring.ringInst leInst ltInst isPreorderInst orderedRingInst
   let h := mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
@@ -456,7 +470,8 @@ def mkNonCommLeIffProof (leInst ltInst isPreorderInst orderedRingInst : Expr) (l
 
 def mkNonCommLtIffProof (leInst ltInst lawfulOrdLtInst isPreorderInst orderedRingInst : Expr) (lhs rhs lhs' rhs' : RingExpr) : NonCommRingM Expr := do
   let ring ← getRing
-  let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
+  let ringEntry ← getRingEntry
+  let { lhs, rhs, lhs', rhs', vars } := norm ringEntry.vars lhs rhs lhs' rhs'
   let ctx ← toContextExpr vars
   let h := mkApp7 (mkConst ``Grind.CommRing.lt_norm_expr_nc [ring.u]) ring.type ring.ringInst leInst ltInst lawfulOrdLtInst isPreorderInst orderedRingInst
   let h := mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
@@ -468,7 +483,8 @@ def mkNonCommLtIffProof (leInst ltInst lawfulOrdLtInst isPreorderInst orderedRin
 
 def mkNonCommEqIffProof (lhs rhs lhs' rhs' : RingExpr) : NonCommRingM Expr := do
   let ring ← getRing
-  let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
+  let ringEntry ← getRingEntry
+  let { lhs, rhs, lhs', rhs', vars } := norm ringEntry.vars lhs rhs lhs' rhs'
   let ctx ← toContextExpr vars
   let h := mkApp2 (mkConst ``Grind.CommRing.eq_norm_expr_nc [ring.u]) ring.type ring.ringInst
   let h := mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
@@ -483,7 +499,8 @@ Given `e` and `e'` s.t. `e.toPoly_nc == e'.toPoly_nc`, returns a proof that `e.d
 -/
 def mkNonCommTermEqProof (e e' : RingExpr) : NonCommRingM Expr := do
   let ring ← getRing
-  let { lhs, lhs', vars, .. } := norm ring.vars e (.num 0) e' (.num 0)
+  let ringEntry ← getRingEntry
+  let { lhs, lhs', vars, .. } := norm ringEntry.vars e (.num 0) e' (.num 0)
   let ctx ← toContextExpr vars
   let h := mkApp2 (mkConst ``Grind.CommRing.Expr.eq_of_toPoly_nc_eq [ring.u]) ring.type ring.ringInst
   let h := mkApp4 h ctx (toExpr lhs) (toExpr lhs') eagerReflBoolTrue