fix: delete empty .out.expected files instead of leaving them empty

The lint.sh check flags empty .out.expected files. Delete them entirely
since these tests no longer produce expected output.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

.claude/CLAUDE.md

@@ -1,30 +1,28 @@
-To build Lean you should use `make -j -C build/release`.
+(In the following, use `sysctl -n hw.logicalcpu` instead of `nproc` on macOS)
+
+To build Lean you should use `make -j$(nproc) -C build/release`.
 
 ## Running Tests
 
-See `doc/dev/testing.md` for full documentation. Quick reference:
+See `tests/README.md` for full documentation. Quick reference:
 
 ```bash
 # Full test suite (use after builds to verify correctness)
-make -j -C build/release test ARGS="-j$(nproc)"
+CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
+make -C build/release -j "$(nproc)" test
 
 # Specific test by name (supports regex via ctest -R)
-make -j -C build/release test ARGS='-R grind_ematch --output-on-failure'
+CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
+make -C build/release -j "$(nproc)" test ARGS='-R grind_ematch'
 
 # Rerun only previously failed tests
-make -j -C build/release test ARGS='--rerun-failed --output-on-failure'
+CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
+make -C build/release -j "$(nproc)" test ARGS='--rerun-failed'
 
-# Single test from tests/lean/run/ (quick check during development)
-cd tests/lean/run && ./test_single.sh example_test.lean
-
-# ctest directly (from stage1 build dir)
-cd build/release/stage1 && ctest -j$(nproc) --output-on-failure --timeout 300
+# Single test from tests/foo/bar/ (quick check during development)
+cd tests/foo/bar && ./run_test example_test.lean
 ```
 
-The full test suite includes `tests/lean/`, `tests/lean/run/`, `tests/lean/interactive/`,
-`tests/compiler/`, `tests/pkg/`, Lake tests, and more. Using `make test` or `ctest` runs
-all of them; `test_single.sh` in `tests/lean/run/` only covers that one directory.
-
 ## New features
 
 When asked to implement new features:
@@ -32,8 +30,6 @@ When asked to implement new features:
 * write comprehensive tests first (expecting that these will initially fail)
 * and then iterate on the implementation until the tests pass.
 
-All new tests should go in `tests/lean/run/`. These tests don't have expected output; we just check there are no errors. You should use `#guard_msgs` to check for specific messages.
-
 ## Success Criteria
 
 *Never* report success on a task unless you have verified both a clean build without errors, and that the relevant tests pass.
@@ -41,7 +37,7 @@ All new tests should go in `tests/lean/run/`. These tests don't have expected ou
 ## Build System Safety
 
 **NEVER manually delete build directories** (build/, stage0/, stage1/, etc.) even when builds fail.
-- ONLY use the project's documented build command: `make -j -C build/release`
+- ONLY use the project's documented build command: `make -j$(nproc) -C build/release`
 - If a build is broken, ask the user before attempting any manual cleanup
 
 ## LSP and IDE Diagnostics
@@ -59,7 +55,7 @@ Follow the commit convention in `doc/dev/commit_convention.md`.
 **Title format:** `<type>: <subject>` where type is one of: `feat`, `fix`, `doc`, `style`, `refactor`, `test`, `chore`, `perf`.
 Subject should use imperative present tense ("add" not "added"), no capitalization, no trailing period.
 
-**Body format:** The first paragraph must start with "This PR". This paragraph is automatically incorporated into release notes. Use imperative present tense. Include motivation and contrast with previous behavior when relevant.
+**Body format:** The first paragraph must start with "This PR". This paragraph is automatically incorporated into release notes. Use imperative present tense. Include motivation and contrast with previous behavior when relevant. Do NOT use markdown headings (`## Summary`, `## Test plan`, etc.) in PR bodies.
 
 Example:
 ```
@@ -84,6 +80,27 @@ leading quantifiers are stripped when creating a pattern.
 
 If you're unsure which label applies, it's fine to omit the label and let reviewers add it.
 
+## Module System for `src/` Files
+
+Files in `src/Lean/`, `src/Std/`, and `src/lake/Lake/` must have both `module` and `prelude` (CI enforces `^prelude$` on its own line). With `prelude`, nothing is auto-imported — you must explicitly import `Init.*` modules for standard library features. Check existing files in the same directory for the pattern, e.g.:
+
+```lean
+module
+
+prelude
+import Init.While  -- needed for while/repeat
+import Init.Data.String.TakeDrop  -- needed for String.startsWith
+public import Lean.Compiler.NameMangling  -- public if types are used in public signatures
+```
+
+Files outside these directories (e.g. `tests/`, `script/`) use just `module`.
+
 ## CI Log Retrieval
 
 When CI jobs fail, investigate immediately - don't wait for other jobs to complete. Individual job logs are often available even while other jobs are still running. Try `gh run view <run-id> --log` or `gh run view <run-id> --log-failed`, or use `gh run view <run-id> --job=<job-id>` to target the specific failed job. Sleeping is fine when asked to monitor CI and no failures exist yet, but once any job fails, investigate that failure immediately.
+
+## Copyright Headers
+
+New files require a copyright header. To get the year right, always run `date +%Y` rather than relying on memory. The copyright holder should be the author or their current employer — check other recent files by the same author in the repository to determine the correct entity (e.g., "Lean FRO, LLC", "Amazon.com, Inc. or its affiliates").
+
+Test files (in `tests/`) do not need copyright headers.

.claude/commands/release.md

@@ -103,6 +103,15 @@ Every time you run `release_checklist.py`, you MUST:
 This summary should be provided EVERY time you run the checklist, not just after creating new PRs.
 The user needs to see the complete picture of what's waiting for review.
 
+## Checking PR Status When Asked
+
+When the user asks for "status" or you need to report on PRs between checklist runs:
+- **ALWAYS check actual PR state** using `gh pr view <number> --repo <repo> --json state,mergedAt`
+- Do NOT rely on cached CI results or previous checklist output
+- The user may have merged PRs since your last check
+- Report which PRs are MERGED, which are OPEN with CI status, and which are still pending
+- After discovering merged PRs, rerun `release_checklist.py` to advance the release process
+
 ## Nightly Infrastructure
 
 The nightly build system uses branches and tags across two repositories:

.claude/settings.json

@@ -0,0 +1,13 @@
+{
+  "extraKnownMarketplaces": {
+    "leanprover": {
+      "source": {
+        "source": "github",
+        "repo": "leanprover/skills"
+      }
+    }
+  },
+  "enabledPlugins": {
+    "lean@leanprover": true
+  }
+}

.claude/skills/zulip-extract/SKILL.md

@@ -0,0 +1,17 @@
+---
+name: zulip-extract
+description: Extract Zulip thread HTML dumps into readable plain text. Use when the user provides a Zulip HTML file or asks to parse/read/convert/summarize a Zulip thread.
+---
+
+# Zulip Thread Extractor
+
+Run the bundled script to convert a Zulip HTML page dump into plain text.
+
+## Usage
+```bash
+python3 .claude/skills/zulip-extract/zulip_thread_extract.py input.html output.txt
+```
+
+The script has zero dependencies beyond Python 3 stdlib.
+It extracts sender, timestamp, message content (with code blocks,
+links, quotes, mentions), and reactions.

.claude/skills/zulip-extract/zulip_thread_extract.py

@@ -0,0 +1,313 @@
+#!/usr/bin/env python3
+"""
+Convert a Zulip HTML page dump to plain text (the visible message thread).
+
+Zero external dependencies — uses only the Python standard library.
+
+Usage:
+    python3 zulip_thread_extract.py input.html [output.txt]
+"""
+
+import sys
+import re
+from html.parser import HTMLParser
+from html import unescape
+
+
+# ---------------------------------------------------------------------------
+# Minimal DOM built from stdlib HTMLParser
+# ---------------------------------------------------------------------------
+
+class Node:
+    """A lightweight DOM node."""
+    __slots__ = ('tag', 'attrs', 'children', 'parent', 'text')
+
+    def __init__(self, tag='', attrs=None):
+        self.tag = tag
+        self.attrs = dict(attrs) if attrs else {}
+        self.children = []
+        self.parent = None
+        self.text = ''  # for text nodes only (tag == '')
+
+    @property
+    def cls(self):
+        return self.attrs.get('class', '')
+
+    def has_class(self, c):
+        return c in self.cls.split()
+
+    def find_all(self, tag=None, class_=None):
+        """Depth-first search for matching descendants."""
+        for child in self.children:
+            if child.tag == '':
+                continue
+            match = True
+            if tag and child.tag != tag:
+                match = False
+            if class_ and not child.has_class(class_):
+                match = False
+            if match:
+                yield child
+            yield from child.find_all(tag, class_)
+
+    def find(self, tag=None, class_=None):
+        return next(self.find_all(tag, class_), None)
+
+    def get_text(self):
+        if self.tag == '':
+            return self.text
+        return ''.join(c.get_text() for c in self.children)
+
+
+class DOMBuilder(HTMLParser):
+    """Build a minimal DOM tree from HTML."""
+
+    VOID_ELEMENTS = frozenset([
+        'area', 'base', 'br', 'col', 'embed', 'hr', 'img', 'input',
+        'link', 'meta', 'param', 'source', 'track', 'wbr',
+    ])
+
+    def __init__(self):
+        super().__init__()
+        self.root = Node('root')
+        self._cur = self.root
+
+    def handle_starttag(self, tag, attrs):
+        node = Node(tag, attrs)
+        node.parent = self._cur
+        self._cur.children.append(node)
+        if tag not in self.VOID_ELEMENTS:
+            self._cur = node
+
+    def handle_endtag(self, tag):
+        # Walk up to find the matching open tag (tolerates misnesting)
+        n = self._cur
+        while n and n.tag != tag and n.parent:
+            n = n.parent
+        if n and n.parent:
+            self._cur = n.parent
+
+    def handle_data(self, data):
+        t = Node()
+        t.text = data
+        t.parent = self._cur
+        self._cur.children.append(t)
+
+    def handle_entityref(self, name):
+        self.handle_data(unescape(f'&{name};'))
+
+    def handle_charref(self, name):
+        self.handle_data(unescape(f'&#{name};'))
+
+
+def parse_html(path):
+    with open(path, 'r', encoding='utf-8') as f:
+        html = f.read()
+    builder = DOMBuilder()
+    builder.feed(html)
+    return builder.root
+
+
+# ---------------------------------------------------------------------------
+# Content extraction
+# ---------------------------------------------------------------------------
+
+SKIP_CLASSES = {
+    'message_controls', 'message_length_controller',
+    'code-buttons-container', 'copy_codeblock', 'code_external_link',
+    'message_edit_notice', 'edit-notifications',
+}
+
+def should_skip(node):
+    return bool(SKIP_CLASSES & set(node.cls.split()))
+
+
+def extract_content(node):
+    """Recursively convert a message_content node into readable text."""
+    parts = []
+    for child in node.children:
+        # Text node
+        if child.tag == '':
+            parts.append(child.text)
+            continue
+
+        if should_skip(child):
+            continue
+
+        cls_set = set(child.cls.split())
+
+        # Code block wrappers  (div.codehilite / div.zulip-code-block)
+        if child.tag == 'div' and ({'codehilite', 'zulip-code-block'} & cls_set):
+            code = child.find('code')
+            lang = child.attrs.get('data-code-language', '')
+            text = code.get_text() if code else child.get_text()
+            parts.append(f'\n```{lang}\n{text}```\n')
+            continue
+
+        # <pre> (bare code blocks without wrapper div)
+        if child.tag == 'pre':
+            code = child.find('code')
+            text = code.get_text() if code else child.get_text()
+            parts.append(f'\n```\n{text}```\n')
+            continue
+
+        # Inline <code>
+        if child.tag == 'code':
+            parts.append(f'`{child.get_text()}`')
+            continue
+
+        # Paragraph
+        if child.tag == 'p':
+            inner = extract_content(child)
+            parts.append(f'\n{inner}\n')
+            continue
+
+        # Line break
+        if child.tag == 'br':
+            parts.append('\n')
+            continue
+
+        # Links
+        if child.tag == 'a':
+            href = child.attrs.get('href', '')
+            text = child.get_text().strip()
+            if href and not href.startswith('#') and text:
+                parts.append(f'[{text}]({href})')
+            else:
+                parts.append(text)
+            continue
+
+        # Block quotes
+        if child.tag == 'blockquote':
+            bq = extract_content(child).strip()
+            parts.append('\n' + '\n'.join(f'> {l}' for l in bq.split('\n')) + '\n')
+            continue
+
+        # Lists
+        if child.tag in ('ul', 'ol'):
+            for i, li in enumerate(c for c in child.children if c.tag == 'li'):
+                pfx = f'{i+1}.' if child.tag == 'ol' else '-'
+                parts.append(f'\n{pfx} {extract_content(li).strip()}')
+            parts.append('\n')
+            continue
+
+        # User mentions
+        if 'user-mention' in cls_set:
+            parts.append(f'@{child.get_text().strip().lstrip("@")}')
+            continue
+
+        # Emoji
+        if 'emoji' in cls_set:
+            alt = child.attrs.get('alt', '') or child.attrs.get('title', '')
+            if alt:
+                parts.append(alt)
+            continue
+
+        # Recurse into everything else
+        parts.append(extract_content(child))
+
+    return ''.join(parts)
+
+
+# ---------------------------------------------------------------------------
+# Thread extraction
+# ---------------------------------------------------------------------------
+
+def extract_thread(html_path, output_path=None):
+    root = parse_html(html_path)
+
+    # Find the message list
+    msg_list = root.find('div', class_='message-list')
+    if not msg_list:
+        print("ERROR: Could not find message list.", file=sys.stderr)
+        sys.exit(1)
+
+    # Topic header
+    header = msg_list.find('div', class_='message_header')
+    stream_name = topic_name = date_str = ''
+    if header:
+        el = header.find('span', class_='message-header-stream-name')
+        if el: stream_name = el.get_text().strip()
+        el = header.find('span', class_='stream-topic-inner')
+        if el: topic_name = el.get_text().strip()
+        el = header.find('span', class_='recipient_row_date')
+        if el:
+            tr = el.find('span', class_='timerender-content')
+            if tr:
+                date_str = tr.attrs.get('data-tippy-content', '') or tr.get_text().strip()
+
+    # Messages
+    messages = []
+    for row in msg_list.find_all('div', class_='message_row'):
+        if not row.has_class('messagebox-includes-sender'):
+            continue
+
+        msg = {}
+
+        sn = row.find('span', class_='sender_name_text')
+        if sn:
+            un = sn.find('span', class_='user-name')
+            msg['sender'] = (un or sn).get_text().strip()
+
+        tm = row.find('a', class_='message-time')
+        if tm:
+            msg['time'] = tm.get_text().strip()
+
+        cd = row.find('div', class_='message_content')
+        if cd:
+            text = extract_content(cd)
+            text = re.sub(r'\n{3,}', '\n\n', text).strip()
+            msg['content'] = text
+
+        # Reactions
+        reactions = []
+        for rx in row.find_all('div', class_='message_reaction'):
+            em = rx.find('div', class_='emoji_alt_code')
+            if em:
+                reactions.append(em.get_text().strip())
+            else:
+                img = rx.find(tag='img')
+                if img:
+                    reactions.append(img.attrs.get('alt', ''))
+            cnt = rx.find('span', class_='message_reaction_count')
+            if cnt and reactions:
+                c = cnt.get_text().strip()
+                if c and c != '1':
+                    reactions[-1] += f' x{c}'
+        if reactions:
+            msg['reactions'] = reactions
+
+        if msg.get('content') or msg.get('sender'):
+            messages.append(msg)
+
+    # Format
+    lines = [
+        '=' * 70,
+        f'# {stream_name} > {topic_name}',
+    ]
+    if date_str:
+        lines.append(f'# Started: {date_str}')
+    lines += [f'# Messages: {len(messages)}', '=' * 70, '']
+
+    for msg in messages:
+        lines.append(f'--- {msg.get("sender","?")}  [{msg.get("time","")}] ---')
+        lines.append(msg.get('content', ''))
+        if msg.get('reactions'):
+            lines.append(f'  Reactions: {", ".join(msg["reactions"])}')
+        lines.append('')
+
+    result = '\n'.join(lines)
+    if output_path:
+        with open(output_path, 'w', encoding='utf-8') as f:
+            f.write(result)
+        print(f"Written {len(messages)} messages to {output_path}")
+    else:
+        print(result)
+
+
+if __name__ == '__main__':
+    if len(sys.argv) < 2:
+        print(f"Usage: {sys.argv[0]} input.html [output.txt]")
+        sys.exit(1)
+    extract_thread(sys.argv[1], sys.argv[2] if len(sys.argv) > 2 else None)
+

.github/workflows/build-template.yml

@@ -49,7 +49,7 @@ jobs:
       LSAN_OPTIONS: max_leaks=10
       # somehow MinGW clang64 (or cmake?) defaults to `g++` even though it doesn't exist
       CXX: c++
-      MACOSX_DEPLOYMENT_TARGET: 10.15
+      MACOSX_DEPLOYMENT_TARGET: 11.0
     steps:
       - name: Install Nix
         uses: DeterminateSystems/nix-installer-action@main
@@ -85,7 +85,7 @@ jobs:
       - name: CI Merge Checkout
         run: |
           git fetch --depth=1 origin ${{ github.sha }}
-          git checkout FETCH_HEAD flake.nix flake.lock script/prepare-* tests/lean/run/importStructure.lean
+          git checkout FETCH_HEAD flake.nix flake.lock script/prepare-* tests/elab/importStructure.lean
         if: github.event_name == 'pull_request'
       # (needs to be after "Checkout" so files don't get overridden)
       - name: Setup emsdk
@@ -235,7 +235,7 @@ jobs:
         # prefix `if` above with `always` so it's run even if tests failed
         if: always() && steps.test.conclusion != 'skipped'
       - name: Check Test Binary
-        run: ${{ matrix.binary-check }} tests/compiler/534.lean.out
+        run: ${{ matrix.binary-check }} tests/compile/534.lean.out
         if: (!matrix.cross) && steps.test.conclusion != 'skipped'
       - name: Build Stage 2
         run: |
@@ -246,13 +246,7 @@ jobs:
           make -C build -j$NPROC check-stage3
         if: matrix.check-stage3
       - name: Test Speedcenter Benchmarks
-        run: |
-          # Necessary for some timing metrics but does not work on Namespace runners
-          # and we just want to test that the benchmarks run at all here
-          #echo -1 | sudo tee /proc/sys/kernel/perf_event_paranoid
-          export BUILD=$PWD/build PATH=$PWD/build/stage1/bin:$PATH
-          cd tests/bench
-          nix shell .#temci -c temci exec --config speedcenter.yaml --included_blocks fast --runs 1
+        run: nix shell github:Kha/lakeprof -c make -C build -j$NPROC bench
         if: matrix.test-speedcenter
       - name: Check rebootstrap
         run: |

.gitignore

@@ -18,6 +18,7 @@ compile_commands.json
 *.idea
 tasks.json
 settings.json
+!.claude/settings.json
 .gdb_history
 .vscode/*
 script/__pycache__

CMakeLists.txt

@@ -1,4 +1,8 @@
-cmake_minimum_required(VERSION 3.11)
+cmake_minimum_required(VERSION 3.21)
+
+if(NOT CMAKE_GENERATOR MATCHES "Makefiles")
+  message(FATAL_ERROR "Only makefile generators are supported")
+endif()
 
 option(USE_MIMALLOC "use mimalloc" ON)
 
@@ -70,13 +74,7 @@ if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
       BUILD_IN_SOURCE ON
       INSTALL_COMMAND ""
     )
-    set(
-      CADICAL
-      ${CMAKE_BINARY_DIR}/cadical/cadical${CMAKE_EXECUTABLE_SUFFIX}
-      CACHE FILEPATH
-      "path to cadical binary"
-      FORCE
-    )
+    set(CADICAL ${CMAKE_BINARY_DIR}/cadical/cadical${CMAKE_EXECUTABLE_SUFFIX})
     list(APPEND EXTRA_DEPENDS cadical)
   endif()
   list(APPEND CL_ARGS -DCADICAL=${CADICAL})
@@ -153,6 +151,7 @@ ExternalProject_Add(
   INSTALL_COMMAND ""
   DEPENDS stage2
   EXCLUDE_FROM_ALL ON
+  STEP_TARGETS configure
 )
 
 # targets forwarded to appropriate stages
@@ -163,6 +162,25 @@ add_custom_target(update-stage0-commit COMMAND $(MAKE) -C stage1 update-stage0-c
 
 add_custom_target(test COMMAND $(MAKE) -C stage1 test DEPENDS stage1)
 
+add_custom_target(
+  bench
+  COMMAND $(MAKE) -C stage2
+  COMMAND $(MAKE) -C stage2 -j1 bench
+  DEPENDS stage2
+)
+add_custom_target(
+  bench-part1
+  COMMAND $(MAKE) -C stage2
+  COMMAND $(MAKE) -C stage2 -j1 bench-part1
+  DEPENDS stage2
+)
+add_custom_target(
+  bench-part2
+  COMMAND $(MAKE) -C stage2
+  COMMAND $(MAKE) -C stage2 -j1 bench-part2
+  DEPENDS stage2
+)
+
 add_custom_target(clean-stdlib COMMAND $(MAKE) -C stage1 clean-stdlib DEPENDS stage1)
 
 install(CODE "execute_process(COMMAND make -C stage1 install)")

doc/dev/release_checklist.md

@@ -65,7 +65,14 @@ We'll use `v4.6.0` as the intended release version as a running example.
       - The `lakefile.toml` should always refer to dependencies via their `main` or `master` branch,
         not a toolchain tag
         (with the exception of `ProofWidgets4`, which *must* use a sequential version tag).
+      - **Important:** After creating and pushing the ProofWidgets4 tag (see above),
+        the mathlib4 lakefile must be updated to reference the new tag (e.g. `v0.0.87`).
+        The `release_steps.py` script handles this automatically by looking up the latest
+        ProofWidgets4 tag compatible with the target toolchain.
       - Push the PR branch to the main Mathlib repository rather than a fork, or CI may not work reliably
+      - The "Verify Transient and Automated Commits" CI check on toolchain bump PRs can be ignored —
+        it often fails on automated commits (`x:` prefixed) from the nightly-testing history that can't be
+        reproduced in CI. This does not block merging.
     - `repl`:
       There are two copies of `lean-toolchain`/`lakefile.lean`:
       in the root, and in `test/Mathlib/`. Edit both, and run `lake update` in both directories.
@@ -146,6 +153,9 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
     * The repository does not need any changes to move to the new version.
     * Note that sometimes there are *unreviewed* but necessary changes on the `nightly-testing` branch of the repository.
       If so, you will need to merge these into the `bump_to_v4.7.0-rc1` branch manually.
+    * The `nightly-testing` branch may also contain temporary fix scripts (e.g. `fix_backward_defeq.py`,
+      `fix_deprecations.py`) that were used to adapt to breaking changes during the nightly cycle.
+      These should be reviewed and removed if no longer needed, as they can interfere with CI checks.
   - For each of the repositories listed in `script/release_repos.yml`,
     - Run `script/release_steps.py v4.7.0-rc1 <repo>` (e.g. replacing `<repo>` with `batteries`), which will walk you through the following steps:
       - Create a new branch off `master`/`main` (as specified in the `branch` field), called `bump_to_v4.7.0-rc1`.

doc/dev/testing.md

@@ -1,5 +1,9 @@
 # Test Suite
 
+**Warning:** This document is partially outdated.
+It describes the old test suite, which is currently in the process of being replaced.
+The new test suite's documentation can be found at [`tests/README.md`](../../tests/README.md).
+
 After [building Lean](../make/index.md) you can run all the tests using
 ```
 cd build/release

doc/std/grove/lean-toolchain

@@ -1 +1 @@
-lean4
+../../../build/release/stage1

lean-toolchain

@@ -1 +1 @@
-lean4
+build/release/stage1

lean.code-workspace

@@ -2,21 +2,9 @@
 	"folders": [
 		{
 			"path": "."
-		},
-		{
-			"path": "src"
-		},
-		{
-			"path": "tests"
-		},
-		{
-			"path": "script"
 		}
 	],
 	"settings": {
-		// Open terminal at root, not current workspace folder
-		// (there is not way to directly refer to the root folder included as `.` above)
-		"terminal.integrated.cwd": "${workspaceFolder:src}/..",
 		"files.insertFinalNewline": true,
 		"files.trimTrailingWhitespace": true,
 		"cmake.buildDirectory": "${workspaceFolder}/build/release",

releases_drafts/environment.md

@@ -1,6 +0,0 @@
-**Breaking Changes**
-
-* The functions `Lean.Environment.importModules` and `Lean.Environment.finalizeImport` have been extended with a new parameter `loadExts : Bool := false` that enables environment extension state loading.
-  Their previous behavior corresponds to setting the flag to `true` but is only safe to do in combination with `enableInitializersExecution`; see also the `importModules` docstring.
-  The new default value `false` ensures the functions can be used correctly multiple times within the same process when environment extension access is not needed.
-  The wrapper function `Lean.Environment.withImportModules` now always calls `importModules` with `loadExts := false` as it is incompatible with extension loading.

releases_drafts/module-system.md

@@ -1,54 +0,0 @@
-This release introduces the Lean module system, which allows files to
-control the visibility of their contents for other files. In previous
-releases, this feature was available as a preview when the option
-`experimental.module` was set to `true`; it is now a fully supported
-feature of Lean.
-
-# Benefits
-
-Because modules reduce the amount of information exposed to other
-code, they speed up rebuilds because irrelevant changes can be
-ignored, they make it possible to be deliberate about API evolution by
-hiding details that may change from clients, they help proofs be
-checked faster by avoiding accidentally unfolding definitions, and
-they lead to smaller executable files through improved dead code
-elimination.
-
-# Visibility
-
-A source file is a module if it begins with the `module` keyword.  By
-default, declarations in a module are private; the `public` modifier
-exports them. Proofs of theorems and bodies of definitions are private
-by default even when their signatures are public; the bodies of
-definitions can be made public by adding the `@[expose]`
-attribute. Theorems and opaque constants never expose their bodies.
-
-`public section` and `@[expose] section` change the default visibility
-of declarations in the section.
-
-# Imports
-
-Modules may only import other modules. By default, `import` adds the
-public information of the imported module to the private scope of the
-current module. Adding the `public` modifier to an import places the
-imported modules's public information in the public scope of the
-current module, exposing it in turn to the current module's clients.
-
-Within a package, `import all` can be used to import another module's
-private scope into the current module; this can be used to separate
-lemmas or tests from definition modules without exposing details to
-downstream clients.
-
-# Meta Code
-
-Code used in metaprograms must be marked `meta`. This ensures that the
-code is compiled and available for execution when it is needed during
-elaboration. Meta code may only reference other meta code. A whole
-module can be made available in the meta phase using `meta import`;
-this allows code to be shared across phases by importing the module in
-each phase. Code that is reachable from public metaprograms must be
-imported via `public meta import`, while local metaprograms can use
-plain `meta import` for their dependencies.
-
-
-The module system is described in detail in [the Lean language reference](https://lean-reference-manual-review.netlify.app/find/?domain=Verso.Genre.Manual.section&name=files).

script/PROFILER_README.md

@@ -0,0 +1,178 @@
+# Lean Profiler
+
+Profile Lean programs with demangled names using
+[samply](https://github.com/mstange/samply) and
+[Firefox Profiler](https://profiler.firefox.com).
+
+Python 3, no external dependencies.
+
+## Quick start
+
+```bash
+# One command: record, symbolicate, demangle, and open in Firefox Profiler
+script/lean_profile.sh ./my_lean_binary [args...]
+
+# See all options
+script/lean_profile.sh --help
+```
+
+Requirements: `samply` (`cargo install samply`), `python3`.
+
+## Reading demangled names
+
+The demangler transforms low-level C symbol names into readable Lean names
+and annotates them with compact modifiers.
+
+### Basic names
+
+| Raw symbol | Demangled |
+|---|---|
+| `l_Lean_Meta_Sym_main` | `Lean.Meta.Sym.main` |
+| `lp_std_List_map` | `List.map (std)` |
+| `_init_l_Foo_bar` | `[init] Foo.bar` |
+| `initialize_Init_Data` | `[module_init] Init.Data` |
+| `_lean_main` | `[lean] main` |
+
+### Modifier flags `[...]`
+
+Compiler-generated suffixes are folded into a bracket annotation after the
+name. These indicate *how* the function was derived from the original source
+definition.
+
+| Flag | Meaning | Compiler suffix |
+|---|---|---|
+| `arity`↓ | Reduced-arity specialization | `_redArg` |
+| `boxed` | Boxed calling-convention wrapper | `_boxed` |
+| `impl` | Implementation detail | `_impl` |
+| λ | Lambda-lifted closure | `_lam_N`, `_lambda_N`, `_elam_N` |
+| `jp` | Join point | `_jp_N` |
+| `closed` | Extracted closed subterm | `_closed_N` |
+| `private` | Private (module-scoped) definition | `_private.Module.0.` prefix |
+
+Examples:
+
+```
+Lean.Meta.Simp.simpLambda [boxed, λ]     -- boxed wrapper of a lambda-lifted closure
+Lean.Meta.foo [arity↓, private]           -- reduced-arity version of a private def
+```
+
+Multiple flags are comma-separated. Order reflects how they were collected
+(innermost suffix first).
+
+### Specializations `spec at ...`
+
+When the compiler specializes a function at a particular call site, the
+demangled name shows `spec at <context>` after the base name and its flags.
+The context names the function whose body triggered the specialization, and
+may carry its own modifier flags:
+
+```
+<base-name> [<base-flags>] spec at <context>[<context-flags>]
+```
+
+Examples:
+
+```
+-- foo specialized at call site in bar
+Lean.Meta.foo spec at Lean.Meta.bar
+
+-- foo (with a lambda closure) specialized at bar (with reduced arity and a lambda)
+Lean.Meta.foo [λ] spec at Lean.Meta.bar[λ, arity↓]
+
+-- chained specialization: foo specialized at bar, then at baz
+Lean.Meta.foo spec at Lean.Meta.bar spec at Lean.Meta.baz[arity↓]
+```
+
+Context flags use the same symbols as base flags. When a context has no
+flags, the brackets are omitted.
+
+### Other annotations
+
+| Pattern | Meaning |
+|---|---|
+| `<apply/N>` | Lean runtime apply function (N arguments) |
+| `.cold.N` suffix | LLVM cold-path clone (infrequently executed) |
+| `(pkg)` suffix | Function from package `pkg` |
+
+## Tools
+
+### `script/lean_profile.sh` -- Full profiling pipeline
+
+Records a profile, symbolicates it via samply's API, demangles Lean names,
+and opens the result in Firefox Profiler. This is the recommended workflow.
+
+```bash
+script/lean_profile.sh ./build/release/stage1/bin/lean src/Lean/Elab/Term.lean
+```
+
+Environment variables:
+
+| Variable | Default | Description |
+|---|---|---|
+| `SAMPLY_RATE` | 1000 | Sampling rate in Hz |
+| `SAMPLY_PORT` | 3756 | Port for samply symbolication server |
+| `SERVE_PORT` | 3757 | Port for serving the demangled profile |
+| `PROFILE_KEEP` | 0 | Set to 1 to keep the temp directory |
+
+### `script/profiler/lean_demangle.py` -- Name demangler
+
+Demangles individual symbol names. Works as a stdin filter (like `c++filt`)
+or with arguments.
+
+```bash
+echo "l_Lean_Meta_Sym_main" | python3 script/profiler/lean_demangle.py
+# Lean.Meta.Sym.main
+
+python3 script/profiler/lean_demangle.py --raw l_foo___redArg
+# foo._redArg  (exact name, no postprocessing)
+```
+
+As a Python module:
+
+```python
+from lean_demangle import demangle_lean_name, demangle_lean_name_raw
+
+demangle_lean_name("l_foo___redArg")       # "foo [arity↓]"
+demangle_lean_name_raw("l_foo___redArg")   # "foo._redArg"
+```
+
+### `script/profiler/symbolicate_profile.py` -- Profile symbolicator
+
+Calls samply's symbolication API to resolve raw addresses into symbol names,
+then demangles them. Used internally by `lean_profile.sh`.
+
+### `script/profiler/serve_profile.py` -- Profile server
+
+Serves a profile JSON file to Firefox Profiler without re-symbolication
+(which would overwrite demangled names). Used internally by `lean_profile.sh`.
+
+### `script/profiler/lean_demangle_profile.py` -- Standalone profile rewriter
+
+Demangles names in an already-symbolicated profile file (if you have one
+from another source).
+
+```bash
+python3 script/profiler/lean_demangle_profile.py profile.json.gz -o demangled.json.gz
+```
+
+## Tests
+
+```bash
+cd script/profiler && python3 -m unittest test_demangle -v
+```
+
+## How it works
+
+The demangler is a faithful port of Lean 4's `Name.demangleAux` from
+`src/Lean/Compiler/NameMangling.lean`. It reverses the encoding used by
+`Name.mangle` / `Name.mangleAux` which turns hierarchical Lean names into
+valid C identifiers:
+
+- `_` separates name components (`Lean.Meta` -> `Lean_Meta`)
+- `__` encodes a literal underscore in a component name
+- `_xHH`, `_uHHHH`, `_UHHHHHHHH` encode special characters
+- `_N_` encodes numeric name components
+- `_00` is a disambiguation prefix for ambiguous patterns
+
+After demangling, a postprocessing pass folds compiler-generated suffixes
+into human-readable annotations (see [Reading demangled names](#reading-demangled-names)).

script/benchReelabRss.lean

@@ -83,7 +83,7 @@ def main (args : List String) : IO Unit := do
       lastRSS? := some rss
 
     let avgRSSDelta := totalRSSDelta / (n - 2)
-    IO.println s!"avg-reelab-rss-delta: {avgRSSDelta}"
+    IO.println s!"measurement: avg-reelab-rss-delta {avgRSSDelta*1024} b"
 
     let _ ← Ipc.collectDiagnostics requestNo uri versionNo
     (← Ipc.stdin).writeLspMessage (Message.notification "exit" none)

script/benchReelabWatchdogRss.lean

@@ -82,7 +82,7 @@ def main (args : List String) : IO Unit := do
       lastRSS? := some rss
 
     let avgRSSDelta := totalRSSDelta / (n - 2)
-    IO.println s!"avg-reelab-rss-delta: {avgRSSDelta}"
+    IO.println s!"measurement: avg-reelab-rss-delta {avgRSSDelta*1024} b"
 
     let _ ← Ipc.collectDiagnostics requestNo uri versionNo
     Ipc.shutdown requestNo

script/fmt

@@ -9,5 +9,5 @@ find -regex '.*/CMakeLists\.txt\(\.in\)?\|.*\.cmake\(\.in\)?' \
   ! -path "./stage0/*" \
   -exec \
     uvx gersemi --in-place --line-length 120 --indent 2 \
-    --definitions src/cmake/Modules/ src/CMakeLists.txt \
+    --definitions src/cmake/Modules/ src/CMakeLists.txt tests/CMakeLists.txt \
     -- {} +

script/lean-toolchain

@@ -1 +1 @@
-lean4
+../build/release/stage1

script/lean_profile.sh

@@ -0,0 +1,133 @@
+#!/bin/bash
+# Profile a Lean binary with demangled names.
+#
+# Usage:
+#   script/lean_profile.sh ./my_lean_binary [args...]
+#
+# Records a profile with samply, symbolicates via samply's API,
+# demangles Lean symbol names, and opens the result in Firefox Profiler.
+#
+# Requirements: samply (cargo install samply), python3
+#
+# Options (via environment variables):
+#   SAMPLY_RATE    — sampling rate in Hz (default: 1000)
+#   SAMPLY_PORT    — port for samply symbolication server (default: 3756)
+#   SERVE_PORT     — port for serving the demangled profile (default: 3757)
+#   PROFILE_KEEP   — set to 1 to keep the raw profile after demangling
+
+set -euo pipefail
+
+SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)"
+PROFILER_DIR="$SCRIPT_DIR/profiler"
+SYMBOLICATE="$PROFILER_DIR/symbolicate_profile.py"
+SERVE_PROFILE="$PROFILER_DIR/serve_profile.py"
+
+usage() {
+    cat >&2 <<EOF
+Usage: $0 [options] <lean-binary> [args...]
+
+Profile a Lean binary and view the results in Firefox Profiler
+with demangled Lean names.
+
+Requirements:
+  samply    cargo install samply
+  python3   (included with macOS / most Linux distros)
+
+Environment variables:
+  SAMPLY_RATE    sampling rate in Hz (default: 1000)
+  SAMPLY_PORT    port for samply symbolication server (default: 3756)
+  SERVE_PORT     port for serving the demangled profile (default: 3757)
+  PROFILE_KEEP   set to 1 to keep the temp directory after profiling
+
+Reading demangled names:
+  Compiler suffixes are shown as modifier flags after the name:
+    [arity↓]   reduced-arity specialization     (_redArg)
+    [boxed]    boxed calling-convention wrapper  (_boxed)
+    [λ]        lambda-lifted closure             (_lam_N, _lambda_N, _elam_N)
+    [jp]       join point                        (_jp_N)
+    [closed]   extracted closed subterm          (_closed_N)
+    [private]  private (module-scoped) def       (_private.Module.0. prefix)
+    [impl]     implementation detail             (_impl)
+
+  Specializations appear after the flags:
+    Lean.Meta.foo [λ] spec at Lean.Meta.bar[λ, arity↓]
+      = foo (with lambda closure), specialized at bar (lambda, reduced arity)
+
+  Multiple "spec at" entries indicate chained specializations.
+  See script/PROFILER_README.md for full documentation.
+EOF
+    exit "${1:-0}"
+}
+
+if [ $# -eq 0 ]; then
+    usage 1
+fi
+
+case "${1:-}" in
+    -h|--help) usage 0 ;;
+esac
+
+if ! command -v samply &>/dev/null; then
+    echo "error: samply not found. Install with: cargo install samply" >&2
+    exit 1
+fi
+
+RATE="${SAMPLY_RATE:-1000}"
+PORT="${SAMPLY_PORT:-3756}"
+SERVE="${SERVE_PORT:-3757}"
+TMPDIR=$(mktemp -d /tmp/lean-profile-XXXXXX)
+TMPFILE="$TMPDIR/profile.json.gz"
+DEMANGLED="$TMPDIR/profile-demangled.json.gz"
+SAMPLY_LOG="$TMPDIR/samply.log"
+SAMPLY_PID=""
+
+cleanup() {
+    if [ -n "$SAMPLY_PID" ]; then
+        kill "$SAMPLY_PID" 2>/dev/null || true
+        wait "$SAMPLY_PID" 2>/dev/null || true
+    fi
+    # Safety net: kill anything still on the symbolication port
+    lsof -ti :"$PORT" 2>/dev/null | xargs kill 2>/dev/null || true
+    [ "${PROFILE_KEEP:-0}" = "1" ] || rm -rf "$TMPDIR"
+}
+trap cleanup EXIT
+
+# Step 1: Record
+echo "Recording profile (rate=${RATE} Hz)..." >&2
+samply record --save-only -o "$TMPFILE" -r "$RATE" "$@"
+
+# Step 2: Start samply server for symbolication
+echo "Starting symbolication server..." >&2
+samply load --no-open -P "$PORT" "$TMPFILE" > "$SAMPLY_LOG" 2>&1 &
+SAMPLY_PID=$!
+
+# Wait for server to be ready
+for i in $(seq 1 30); do
+    if grep -q "Local server listening" "$SAMPLY_LOG" 2>/dev/null; then
+        break
+    fi
+    sleep 0.2
+done
+
+# Extract the token from samply's output
+TOKEN=$(grep -oE '[a-z0-9]{30,}' "$SAMPLY_LOG" | head -1)
+
+if [ -z "$TOKEN" ]; then
+    echo "error: could not get samply server token" >&2
+    exit 1
+fi
+
+SERVER_URL="http://127.0.0.1:${PORT}/${TOKEN}"
+
+# Step 3: Symbolicate + demangle
+echo "Symbolicating and demangling..." >&2
+python3 "$SYMBOLICATE" --server "$SERVER_URL" "$TMPFILE" -o "$DEMANGLED"
+
+# Step 4: Kill symbolication server
+kill "$SAMPLY_PID" 2>/dev/null || true
+wait "$SAMPLY_PID" 2>/dev/null || true
+SAMPLY_PID=""
+
+# Step 5: Serve the demangled profile directly (without samply's re-symbolication)
+echo "Opening in Firefox Profiler..." >&2
+python3 "$SERVE_PROFILE" "$DEMANGLED" -P "$SERVE"

script/lib/update-stage0

@@ -1,7 +1,7 @@
 #!/usr/bin/env bash
 set -euo pipefail
 
-rm -r stage0 || true
+rm -rf stage0 || true
 # don't copy untracked files
 # `:!` is git glob flavor for exclude patterns
 for f in $(git ls-files src ':!:src/lake/*' ':!:src/Leanc.lean'); do

script/profiler/lean_demangle.py

@@ -0,0 +1,779 @@
+#!/usr/bin/env python3
+"""
+Lean name demangler.
+
+Demangles C symbol names produced by the Lean 4 compiler back into
+readable Lean hierarchical names.
+
+Usage as a filter (like c++filt):
+    echo "l_Lean_Meta_Sym_main" | python lean_demangle.py
+
+Usage as a module:
+    from lean_demangle import demangle_lean_name
+    print(demangle_lean_name("l_Lean_Meta_Sym_main"))
+"""
+
+import sys
+
+
+# ---------------------------------------------------------------------------
+# String.mangle / unmangle
+# ---------------------------------------------------------------------------
+
+def _is_ascii_alnum(ch):
+    """Check if ch is an ASCII letter or digit (matching Lean's isAlpha/isDigit)."""
+    return ('a' <= ch <= 'z') or ('A' <= ch <= 'Z') or ('0' <= ch <= '9')
+
+
+def mangle_string(s):
+    """Port of Lean's String.mangle: escape a single string for C identifiers."""
+    result = []
+    for ch in s:
+        if _is_ascii_alnum(ch):
+            result.append(ch)
+        elif ch == '_':
+            result.append('__')
+        else:
+            code = ord(ch)
+            if code < 0x100:
+                result.append('_x' + format(code, '02x'))
+            elif code < 0x10000:
+                result.append('_u' + format(code, '04x'))
+            else:
+                result.append('_U' + format(code, '08x'))
+    return ''.join(result)
+
+
+def _parse_hex(s, pos, n):
+    """Parse n lowercase hex digits at pos. Returns (new_pos, value) or None."""
+    if pos + n > len(s):
+        return None
+    val = 0
+    for i in range(n):
+        c = s[pos + i]
+        if '0' <= c <= '9':
+            val = (val << 4) | (ord(c) - ord('0'))
+        elif 'a' <= c <= 'f':
+            val = (val << 4) | (ord(c) - ord('a') + 10)
+        else:
+            return None
+    return (pos + n, val)
+
+
+# ---------------------------------------------------------------------------
+# Name mangling (for round-trip verification)
+# ---------------------------------------------------------------------------
+
+def _check_disambiguation(m):
+    """Port of Lean's checkDisambiguation: does mangled string m need a '00' prefix?"""
+    pos = 0
+    while pos < len(m):
+        ch = m[pos]
+        if ch == '_':
+            pos += 1
+            continue
+        if ch == 'x':
+            return _parse_hex(m, pos + 1, 2) is not None
+        if ch == 'u':
+            return _parse_hex(m, pos + 1, 4) is not None
+        if ch == 'U':
+            return _parse_hex(m, pos + 1, 8) is not None
+        if '0' <= ch <= '9':
+            return True
+        return False
+    # all underscores or empty
+    return True
+
+
+def _need_disambiguation(prev_component, mangled_next):
+    """Port of Lean's needDisambiguation."""
+    # Check if previous component (as a string) ends with '_'
+    prev_ends_underscore = (isinstance(prev_component, str) and
+                            len(prev_component) > 0 and
+                            prev_component[-1] == '_')
+    return prev_ends_underscore or _check_disambiguation(mangled_next)
+
+
+def mangle_name(components, prefix="l_"):
+    """
+    Mangle a list of name components (str or int) into a C symbol.
+    Port of Lean's Name.mangle.
+    """
+    if not components:
+        return prefix
+
+    parts = []
+    prev = None
+    for i, comp in enumerate(components):
+        if isinstance(comp, int):
+            if i == 0:
+                parts.append(str(comp) + '_')
+            else:
+                parts.append('_' + str(comp) + '_')
+        else:
+            m = mangle_string(comp)
+            if i == 0:
+                if _check_disambiguation(m):
+                    parts.append('00' + m)
+                else:
+                    parts.append(m)
+            else:
+                if _need_disambiguation(prev, m):
+                    parts.append('_00' + m)
+                else:
+                    parts.append('_' + m)
+        prev = comp
+
+    return prefix + ''.join(parts)
+
+
+# ---------------------------------------------------------------------------
+# Name demangling
+# ---------------------------------------------------------------------------
+
+def demangle_body(s):
+    """
+    Demangle a string produced by Name.mangleAux (without prefix).
+    Returns a list of components (str or int).
+
+    This is a faithful port of Lean's Name.demangleAux from NameMangling.lean.
+    """
+    components = []
+    length = len(s)
+
+    def emit(comp):
+        components.append(comp)
+
+    def decode_num(pos, n):
+        """Parse remaining digits, emit numeric component, continue."""
+        while pos < length:
+            ch = s[pos]
+            if '0' <= ch <= '9':
+                n = n * 10 + (ord(ch) - ord('0'))
+                pos += 1
+            else:
+                # Expect '_' (trailing underscore of numeric encoding)
+                pos += 1  # skip '_'
+                emit(n)
+                if pos >= length:
+                    return pos
+                # Skip separator '_' and go to name_start
+                pos += 1
+                return name_start(pos)
+        # End of string
+        emit(n)
+        return pos
+
+    def name_start(pos):
+        """Start parsing a new name component."""
+        if pos >= length:
+            return pos
+        ch = s[pos]
+        pos += 1
+        if '0' <= ch <= '9':
+            # Check for '00' disambiguation
+            if ch == '0' and pos < length and s[pos] == '0':
+                pos += 1
+                return demangle_main(pos, "", 0)
+            else:
+                return decode_num(pos, ord(ch) - ord('0'))
+        elif ch == '_':
+            return demangle_main(pos, "", 1)
+        else:
+            return demangle_main(pos, ch, 0)
+
+    def demangle_main(pos, acc, ucount):
+        """Main demangling loop."""
+        while pos < length:
+            ch = s[pos]
+            pos += 1
+
+            if ch == '_':
+                ucount += 1
+                continue
+
+            if ucount % 2 == 0:
+                # Even underscores: literal underscores in component name
+                acc += '_' * (ucount // 2) + ch
+                ucount = 0
+                continue
+
+            # Odd ucount: separator or escape
+            if '0' <= ch <= '9':
+                # End current str component, start number
+                emit(acc + '_' * (ucount // 2))
+                if ch == '0' and pos < length and s[pos] == '0':
+                    pos += 1
+                    return demangle_main(pos, "", 0)
+                else:
+                    return decode_num(pos, ord(ch) - ord('0'))
+
+            # Try hex escapes
+            if ch == 'x':
+                result = _parse_hex(s, pos, 2)
+                if result is not None:
+                    new_pos, val = result
+                    acc += '_' * (ucount // 2) + chr(val)
+                    pos = new_pos
+                    ucount = 0
+                    continue
+
+            if ch == 'u':
+                result = _parse_hex(s, pos, 4)
+                if result is not None:
+                    new_pos, val = result
+                    acc += '_' * (ucount // 2) + chr(val)
+                    pos = new_pos
+                    ucount = 0
+                    continue
+
+            if ch == 'U':
+                result = _parse_hex(s, pos, 8)
+                if result is not None:
+                    new_pos, val = result
+                    acc += '_' * (ucount // 2) + chr(val)
+                    pos = new_pos
+                    ucount = 0
+                    continue
+
+            # Name separator
+            emit(acc)
+            acc = '_' * (ucount // 2) + ch
+            ucount = 0
+
+        # End of string
+        acc += '_' * (ucount // 2)
+        if acc:
+            emit(acc)
+        return pos
+
+    name_start(0)
+    return components
+
+
+# ---------------------------------------------------------------------------
+# Prefix handling for lp_ (package prefix)
+# ---------------------------------------------------------------------------
+
+def _is_valid_string_mangle(s):
+    """Check if s is a valid output of String.mangle (no trailing bare _)."""
+    pos = 0
+    length = len(s)
+    while pos < length:
+        ch = s[pos]
+        if _is_ascii_alnum(ch):
+            pos += 1
+        elif ch == '_':
+            if pos + 1 >= length:
+                return False  # trailing bare _
+            nch = s[pos + 1]
+            if nch == '_':
+                pos += 2
+            elif nch == 'x' and _parse_hex(s, pos + 2, 2) is not None:
+                pos = _parse_hex(s, pos + 2, 2)[0]
+            elif nch == 'u' and _parse_hex(s, pos + 2, 4) is not None:
+                pos = _parse_hex(s, pos + 2, 4)[0]
+            elif nch == 'U' and _parse_hex(s, pos + 2, 8) is not None:
+                pos = _parse_hex(s, pos + 2, 8)[0]
+            else:
+                return False
+        else:
+            return False
+    return True
+
+
+def _skip_string_mangle(s, pos):
+    """
+    Skip past a String.mangle output in s starting at pos.
+    Returns the position after the mangled string (where we expect the separator '_').
+    This is a greedy scan.
+    """
+    length = len(s)
+    while pos < length:
+        ch = s[pos]
+        if _is_ascii_alnum(ch):
+            pos += 1
+        elif ch == '_':
+            if pos + 1 < length:
+                nch = s[pos + 1]
+                if nch == '_':
+                    pos += 2
+                elif nch == 'x' and _parse_hex(s, pos + 2, 2) is not None:
+                    pos = _parse_hex(s, pos + 2, 2)[0]
+                elif nch == 'u' and _parse_hex(s, pos + 2, 4) is not None:
+                    pos = _parse_hex(s, pos + 2, 4)[0]
+                elif nch == 'U' and _parse_hex(s, pos + 2, 8) is not None:
+                    pos = _parse_hex(s, pos + 2, 8)[0]
+                else:
+                    return pos  # bare '_': separator
+            else:
+                return pos
+        else:
+            return pos
+    return pos
+
+
+def _find_lp_body(s):
+    """
+    Given s = everything after 'lp_' in a symbol, find where the declaration
+    body (Name.mangleAux output) starts.
+    Returns the start index of the body within s, or None.
+
+    Strategy: try all candidate split points where the package part is a valid
+    String.mangle output and the body round-trips. Prefer the longest valid
+    package name (most specific match).
+    """
+    length = len(s)
+
+    # Collect candidate split positions: every '_' that could be the separator
+    candidates = []
+    pos = 0
+    while pos < length:
+        if s[pos] == '_':
+            candidates.append(pos)
+        pos += 1
+
+    # Try each candidate; collect all valid splits
+    valid_splits = []
+    for split_pos in candidates:
+        pkg_part = s[:split_pos]
+        if not pkg_part:
+            continue
+        if not _is_valid_string_mangle(pkg_part):
+            continue
+        body = s[split_pos + 1:]
+        if not body:
+            continue
+        components = demangle_body(body)
+        if not components:
+            continue
+        remangled = mangle_name(components, prefix="")
+        if remangled == body:
+            first = components[0]
+            # Score: prefer first component starting with uppercase
+            has_upper = isinstance(first, str) and first and first[0].isupper()
+            valid_splits.append((split_pos, has_upper))
+
+    if valid_splits:
+        # Among splits where first decl component starts uppercase, pick longest pkg.
+        # Otherwise pick shortest pkg.
+        upper_splits = [s for s in valid_splits if s[1]]
+        if upper_splits:
+            best = max(upper_splits, key=lambda x: x[0])
+        else:
+            best = min(valid_splits, key=lambda x: x[0])
+        return best[0] + 1
+
+    # Fallback: greedy String.mangle scan
+    greedy_pos = _skip_string_mangle(s, 0)
+    if greedy_pos < length and s[greedy_pos] == '_':
+        return greedy_pos + 1
+
+    return None
+
+
+# ---------------------------------------------------------------------------
+# Format name components for display
+# ---------------------------------------------------------------------------
+
+def format_name(components):
+    """Format a list of name components as a dot-separated string."""
+    return '.'.join(str(c) for c in components)
+
+
+# ---------------------------------------------------------------------------
+# Human-friendly postprocessing
+# ---------------------------------------------------------------------------
+
+# Compiler-generated suffix components — exact match
+_SUFFIX_FLAGS_EXACT = {
+    '_redArg':  'arity\u2193',
+    '_boxed':   'boxed',
+    '_impl':    'impl',
+}
+
+# Compiler-generated suffix prefixes — match with optional _N index
+# e.g., _lam, _lam_0, _lam_3, _lambda_0, _closed_2
+_SUFFIX_FLAGS_PREFIX = {
+    '_lam':     '\u03bb',
+    '_lambda':  '\u03bb',
+    '_elam':    '\u03bb',
+    '_jp':      'jp',
+    '_closed':  'closed',
+}
+
+
+def _match_suffix(component):
+    """
+    Check if a string component is a compiler-generated suffix.
+    Returns the flag label or None.
+
+    Handles both exact matches (_redArg, _boxed) and indexed suffixes
+    (_lam_0, _lambda_2, _closed_0) produced by appendIndexAfter.
+    """
+    if not isinstance(component, str):
+        return None
+    if component in _SUFFIX_FLAGS_EXACT:
+        return _SUFFIX_FLAGS_EXACT[component]
+    if component in _SUFFIX_FLAGS_PREFIX:
+        return _SUFFIX_FLAGS_PREFIX[component]
+    # Check for indexed suffix: prefix + _N
+    for prefix, label in _SUFFIX_FLAGS_PREFIX.items():
+        if component.startswith(prefix + '_'):
+            rest = component[len(prefix) + 1:]
+            if rest.isdigit():
+                return label
+    return None
+
+
+def _strip_private(components):
+    """Strip _private.Module.0. prefix. Returns (stripped_parts, is_private)."""
+    if (len(components) >= 3 and isinstance(components[0], str) and
+            components[0] == '_private'):
+        for i in range(1, len(components)):
+            if components[i] == 0:
+                if i + 1 < len(components):
+                    return components[i + 1:], True
+                break
+    return components, False
+
+
+def _strip_spec_suffixes(components):
+    """Strip trailing spec_N components (from appendIndexAfter)."""
+    parts = list(components)
+    while parts and isinstance(parts[-1], str) and parts[-1].startswith('spec_'):
+        rest = parts[-1][5:]
+        if rest.isdigit():
+            parts.pop()
+        else:
+            break
+    return parts
+
+
+def _is_spec_index(component):
+    """Check if a component is a spec_N index (from appendIndexAfter)."""
+    return (isinstance(component, str) and
+            component.startswith('spec_') and component[5:].isdigit())
+
+
+def _parse_spec_entries(rest):
+    """Parse _at_..._spec pairs into separate spec context entries.
+
+    Given components starting from the first _at_, returns:
+    - entries: list of component lists, one per _at_..._spec block
+    - remaining: components after the last _spec N (trailing suffixes)
+    """
+    entries = []
+    current_ctx = None
+    remaining = []
+    skip_next = False
+
+    for p in rest:
+        if skip_next:
+            skip_next = False
+            continue
+        if isinstance(p, str) and p == '_at_':
+            if current_ctx is not None:
+                entries.append(current_ctx)
+            current_ctx = []
+            continue
+        if isinstance(p, str) and p == '_spec':
+            if current_ctx is not None:
+                entries.append(current_ctx)
+                current_ctx = None
+            skip_next = True
+            continue
+        if isinstance(p, str) and p.startswith('_spec'):
+            if current_ctx is not None:
+                entries.append(current_ctx)
+                current_ctx = None
+            continue
+        if current_ctx is not None:
+            current_ctx.append(p)
+        else:
+            remaining.append(p)
+
+    if current_ctx is not None:
+        entries.append(current_ctx)
+
+    return entries, remaining
+
+
+def _process_spec_context(components):
+    """Process a spec context into a clean name and its flags.
+
+    Returns (name_parts, flags) where name_parts are the cleaned components
+    and flags is a deduplicated list of flag labels from compiler suffixes.
+    """
+    parts = list(components)
+    parts, _ = _strip_private(parts)
+
+    name_parts = []
+    ctx_flags = []
+    seen = set()
+
+    for p in parts:
+        flag = _match_suffix(p)
+        if flag is not None:
+            if flag not in seen:
+                ctx_flags.append(flag)
+                seen.add(flag)
+        elif _is_spec_index(p):
+            pass
+        else:
+            name_parts.append(p)
+
+    return name_parts, ctx_flags
+
+
+def postprocess_name(components):
+    """
+    Transform raw demangled components into a human-friendly display string.
+
+    Applies:
+    - Private name cleanup: _private.Module.0.Name.foo -> Name.foo [private]
+    - Hygienic name cleanup: strips _@.module._hygCtx._hyg.N
+    - Suffix folding: _redArg, _boxed, _lam_0, etc. -> [flags]
+    - Specialization: f._at_.g._spec.N -> f spec at g
+      Shown after base [flags], with context flags: spec at g[ctx_flags]
+    """
+    if not components:
+        return ""
+
+    parts = list(components)
+    flags = []
+    spec_entries = []
+
+    # --- Strip _private prefix ---
+    parts, is_private = _strip_private(parts)
+
+    # --- Strip hygienic suffixes: everything from _@ onward ---
+    at_idx = None
+    for i, p in enumerate(parts):
+        if isinstance(p, str) and p.startswith('_@'):
+            at_idx = i
+            break
+    if at_idx is not None:
+        parts = parts[:at_idx]
+
+    # --- Handle specialization: _at_ ... _spec N ---
+    at_positions = [i for i, p in enumerate(parts)
+                    if isinstance(p, str) and p == '_at_']
+    if at_positions:
+        first_at = at_positions[0]
+        base = parts[:first_at]
+        rest = parts[first_at:]
+
+        entries, remaining = _parse_spec_entries(rest)
+        for ctx_components in entries:
+            ctx_name, ctx_flags = _process_spec_context(ctx_components)
+            if ctx_name or ctx_flags:
+                spec_entries.append((ctx_name, ctx_flags))
+
+        parts = base + remaining
+
+    # --- Collect suffix flags from the end ---
+    while parts:
+        last = parts[-1]
+        flag = _match_suffix(last)
+        if flag is not None:
+            flags.append(flag)
+            parts.pop()
+        elif isinstance(last, int) and len(parts) >= 2:
+            prev_flag = _match_suffix(parts[-2])
+            if prev_flag is not None:
+                flags.append(prev_flag)
+                parts.pop()  # remove the number
+                parts.pop()  # remove the suffix
+            else:
+                break
+        else:
+            break
+
+    if is_private:
+        flags.append('private')
+
+    # --- Format result ---
+    name = '.'.join(str(c) for c in parts) if parts else '?'
+    result = name
+    if flags:
+        flag_str = ', '.join(flags)
+        result += f' [{flag_str}]'
+
+    for ctx_name, ctx_flags in spec_entries:
+        ctx_str = '.'.join(str(c) for c in ctx_name) if ctx_name else '?'
+        if ctx_flags:
+            ctx_flag_str = ', '.join(ctx_flags)
+            result += f' spec at {ctx_str}[{ctx_flag_str}]'
+        else:
+            result += f' spec at {ctx_str}'
+
+    return result
+
+
+# ---------------------------------------------------------------------------
+# Main demangling entry point
+# ---------------------------------------------------------------------------
+
+def demangle_lean_name_raw(mangled):
+    """
+    Demangle a Lean C symbol, preserving all internal name components.
+
+    Returns the exact demangled name with all compiler-generated suffixes
+    intact. Use demangle_lean_name() for human-friendly output.
+    """
+    try:
+        return _demangle_lean_name_inner(mangled, human_friendly=False)
+    except Exception:
+        return mangled
+
+
+def demangle_lean_name(mangled):
+    """
+    Demangle a C symbol name produced by the Lean 4 compiler.
+
+    Returns a human-friendly demangled name with compiler suffixes folded
+    into readable flags. Use demangle_lean_name_raw() to preserve all
+    internal components.
+    """
+    try:
+        return _demangle_lean_name_inner(mangled, human_friendly=True)
+    except Exception:
+        return mangled
+
+
+def _demangle_lean_name_inner(mangled, human_friendly=True):
+    """Inner demangle that may raise on malformed input."""
+
+    if mangled == "_lean_main":
+        return "[lean] main"
+
+    # Handle lean_ runtime functions
+    if human_friendly and mangled.startswith("lean_apply_"):
+        rest = mangled[11:]
+        if rest.isdigit():
+            return f"<apply/{rest}>"
+
+    # Strip .cold.N suffix (LLVM linker cold function clones)
+    cold_suffix = ""
+    core = mangled
+    dot_pos = core.find('.cold.')
+    if dot_pos >= 0:
+        cold_suffix = " " + core[dot_pos:]
+        core = core[:dot_pos]
+    elif core.endswith('.cold'):
+        cold_suffix = " .cold"
+        core = core[:-5]
+
+    result = _demangle_core(core, human_friendly)
+    if result is None:
+        return mangled
+    return result + cold_suffix
+
+
+def _demangle_core(mangled, human_friendly=True):
+    """Demangle a symbol without .cold suffix. Returns None if not a Lean name."""
+
+    fmt = postprocess_name if human_friendly else format_name
+
+    # _init_ prefix
+    if mangled.startswith("_init_"):
+        rest = mangled[6:]
+        body, pkg_display = _strip_lean_prefix(rest)
+        if body is None:
+            return None
+        components = demangle_body(body)
+        if not components:
+            return None
+        name = fmt(components)
+        if pkg_display:
+            return f"[init] {name} ({pkg_display})"
+        return f"[init] {name}"
+
+    # initialize_ prefix (module init functions)
+    if mangled.startswith("initialize_"):
+        rest = mangled[11:]
+        # With package: initialize_lp_{pkg}_{body} or initialize_l_{body}
+        body, pkg_display = _strip_lean_prefix(rest)
+        if body is not None:
+            components = demangle_body(body)
+            if components:
+                name = fmt(components)
+                if pkg_display:
+                    return f"[module_init] {name} ({pkg_display})"
+                return f"[module_init] {name}"
+        # Without package: initialize_{Name.mangleAux(moduleName)}
+        if rest:
+            components = demangle_body(rest)
+            if components:
+                return f"[module_init] {fmt(components)}"
+        return None
+
+    # l_ or lp_ prefix
+    body, pkg_display = _strip_lean_prefix(mangled)
+    if body is None:
+        return None
+    components = demangle_body(body)
+    if not components:
+        return None
+    name = fmt(components)
+    if pkg_display:
+        return f"{name} ({pkg_display})"
+    return name
+
+
+def _strip_lean_prefix(s):
+    """
+    Strip the l_ or lp_ prefix from a mangled symbol.
+    Returns (body, pkg_display) where body is the Name.mangleAux output
+    and pkg_display is None or a string describing the package.
+    Returns (None, None) if the string doesn't have a recognized prefix.
+    """
+    if s.startswith("l_"):
+        return (s[2:], None)
+
+    if s.startswith("lp_"):
+        after_lp = s[3:]
+        body_start = _find_lp_body(after_lp)
+        if body_start is not None:
+            pkg_mangled = after_lp[:body_start - 1]
+            # Unmangle the package name
+            pkg_components = demangle_body(pkg_mangled)
+            if pkg_components and len(pkg_components) == 1 and isinstance(pkg_components[0], str):
+                pkg_display = pkg_components[0]
+            else:
+                pkg_display = pkg_mangled
+            return (after_lp[body_start:], pkg_display)
+        # Fallback: treat everything after lp_ as body
+        return (after_lp, "?")
+
+    return (None, None)
+
+
+# ---------------------------------------------------------------------------
+# CLI
+# ---------------------------------------------------------------------------
+
+def main():
+    """Filter stdin or arguments, demangling Lean names."""
+    import argparse
+    parser = argparse.ArgumentParser(
+        description="Demangle Lean 4 C symbol names (like c++filt for Lean)")
+    parser.add_argument('names', nargs='*',
+                        help='Names to demangle (reads stdin if none given)')
+    parser.add_argument('--raw', action='store_true',
+                        help='Output exact demangled names without postprocessing')
+    args = parser.parse_args()
+
+    demangle = demangle_lean_name_raw if args.raw else demangle_lean_name
+
+    if args.names:
+        for name in args.names:
+            print(demangle(name))
+    else:
+        for line in sys.stdin:
+            print(demangle(line.rstrip('\n')))
+
+
+if __name__ == '__main__':
+    main()

script/profiler/lean_demangle_profile.py

@@ -0,0 +1,117 @@
+#!/usr/bin/env python3
+"""
+Lean name demangler for samply / Firefox Profiler profiles.
+
+Reads a profile JSON (plain or gzipped), demangles Lean function names
+in the string table, and writes the result back.
+
+Usage:
+    python lean_demangle_profile.py profile.json -o profile-demangled.json
+    python lean_demangle_profile.py profile.json.gz -o profile-demangled.json.gz
+"""
+
+import argparse
+import gzip
+import json
+import sys
+
+from lean_demangle import demangle_lean_name
+
+
+def _demangle_string_array(string_array):
+    """Demangle Lean names in a string array in-place. Returns count."""
+    count = 0
+    for i, s in enumerate(string_array):
+        if not isinstance(s, str):
+            continue
+        demangled = demangle_lean_name(s)
+        if demangled != s:
+            string_array[i] = demangled
+            count += 1
+    return count
+
+
+def rewrite_profile(profile):
+    """
+    Demangle Lean names in a Firefox Profiler profile dict (in-place).
+
+    Handles two profile formats:
+    - Newer: shared.stringArray (single shared string table)
+    - Older/samply: per-thread stringArray (each thread has its own)
+    """
+    count = 0
+
+    # Shared string table (newer Firefox Profiler format)
+    shared = profile.get("shared")
+    if shared is not None:
+        sa = shared.get("stringArray")
+        if sa is not None:
+            count += _demangle_string_array(sa)
+
+    # Per-thread string tables (samply format)
+    for thread in profile.get("threads", []):
+        sa = thread.get("stringArray")
+        if sa is not None:
+            count += _demangle_string_array(sa)
+
+    return count
+
+
+def process_profile_file(input_path, output_path):
+    """Read a profile, demangle names, write it back."""
+    is_gzip = input_path.endswith('.gz')
+
+    if is_gzip:
+        with gzip.open(input_path, 'rt', encoding='utf-8') as f:
+            profile = json.load(f)
+    else:
+        with open(input_path, 'r', encoding='utf-8') as f:
+            profile = json.load(f)
+
+    count = rewrite_profile(profile)
+
+    out_gzip = output_path.endswith('.gz') if output_path else is_gzip
+
+    if output_path:
+        if out_gzip:
+            with gzip.open(output_path, 'wt', encoding='utf-8') as f:
+                json.dump(profile, f, ensure_ascii=False)
+        else:
+            with open(output_path, 'w', encoding='utf-8') as f:
+                json.dump(profile, f, ensure_ascii=False)
+    else:
+        json.dump(profile, sys.stdout, ensure_ascii=False)
+        sys.stdout.write('\n')
+
+    return count
+
+
+def main():
+    parser = argparse.ArgumentParser(
+        description="Demangle Lean names in samply/Firefox Profiler profiles")
+    parser.add_argument('input', help='Input profile (JSON or .json.gz)')
+    parser.add_argument('-o', '--output',
+                        help='Output path (default: stdout for JSON, '
+                             'or input with -demangled suffix)')
+    args = parser.parse_args()
+
+    output = args.output
+    if output is None and not sys.stdout.isatty():
+        output = None  # write to stdout
+    elif output is None:
+        # Generate output filename
+        inp = args.input
+        if inp.endswith('.json.gz'):
+            output = inp[:-8] + '-demangled.json.gz'
+        elif inp.endswith('.json'):
+            output = inp[:-5] + '-demangled.json'
+        else:
+            output = inp + '-demangled'
+
+    count = process_profile_file(args.input, output)
+    if output:
+        print(f"Demangled {count} names, wrote {output}", file=sys.stderr)
+
+
+if __name__ == '__main__':
+    main()

script/profiler/serve_profile.py

@@ -0,0 +1,94 @@
+#!/usr/bin/env python3
+"""
+Serve a Firefox Profiler JSON file and open it in the browser.
+
+Unlike `samply load`, this does NOT provide a symbolication API,
+so Firefox Profiler will use the names already in the profile as-is.
+"""
+
+import argparse
+import gzip
+import http.server
+import io
+import sys
+import threading
+import webbrowser
+import urllib.parse
+
+
+class ProfileHandler(http.server.BaseHTTPRequestHandler):
+    """Serve the profile JSON and handle CORS for Firefox Profiler."""
+
+    profile_data = None  # set by main()
+
+    def do_GET(self):
+        if self.path == "/profile.json":
+            self.send_response(200)
+            self.send_header("Content-Type", "application/json")
+            self.send_header("Content-Encoding", "gzip")
+            self.send_header("Access-Control-Allow-Origin", "*")
+            self.end_headers()
+            self.wfile.write(self.profile_data)
+        else:
+            self.send_response(404)
+            self.end_headers()
+
+    def do_OPTIONS(self):
+        # CORS preflight
+        self.send_response(200)
+        self.send_header("Access-Control-Allow-Origin", "*")
+        self.send_header("Access-Control-Allow-Methods", "GET")
+        self.send_header("Access-Control-Allow-Headers", "Content-Type")
+        self.end_headers()
+
+    def log_message(self, format, *args):
+        pass  # suppress request logs
+
+
+def main():
+    parser = argparse.ArgumentParser(
+        description="Serve a profile JSON for Firefox Profiler")
+    parser.add_argument("profile", help="Profile file (.json or .json.gz)")
+    parser.add_argument("-P", "--port", type=int, default=3457,
+                        help="Port to serve on (default: 3457)")
+    parser.add_argument("-n", "--no-open", action="store_true",
+                        help="Do not open the browser")
+    args = parser.parse_args()
+
+    # Read the profile data (keep it gzipped for efficient serving)
+    if args.profile.endswith(".gz"):
+        with open(args.profile, "rb") as f:
+            ProfileHandler.profile_data = f.read()
+    else:
+        with open(args.profile, "rb") as f:
+            raw = f.read()
+        buf = io.BytesIO()
+        with gzip.GzipFile(fileobj=buf, mode="wb") as gz:
+            gz.write(raw)
+        ProfileHandler.profile_data = buf.getvalue()
+
+    http.server.HTTPServer.allow_reuse_address = True
+    server = http.server.HTTPServer(("127.0.0.1", args.port), ProfileHandler)
+    profile_url = f"http://127.0.0.1:{args.port}/profile.json"
+    encoded = urllib.parse.quote(profile_url, safe="")
+    viewer_url = f"https://profiler.firefox.com/from-url/{encoded}"
+
+    if not args.no_open:
+        # Open browser after a short delay to let server start
+        def open_browser():
+            webbrowser.open(viewer_url)
+        threading.Timer(0.5, open_browser).start()
+
+    print(f"Serving profile at {profile_url}", file=sys.stderr)
+    print(f"Firefox Profiler: {viewer_url}", file=sys.stderr)
+    print("Press Ctrl+C to stop.", file=sys.stderr)
+
+    try:
+        server.serve_forever()
+    except KeyboardInterrupt:
+        print("\nStopped.", file=sys.stderr)
+        server.server_close()
+
+
+if __name__ == "__main__":
+    main()

script/profiler/symbolicate_profile.py

@@ -0,0 +1,198 @@
+#!/usr/bin/env python3
+"""
+Symbolicate a raw samply profile using samply's symbolication API,
+then demangle Lean names.
+
+Usage:
+    python symbolicate_profile.py --server http://127.0.0.1:3000/TOKEN \
+        raw-profile.json.gz -o symbolicated-demangled.json.gz
+"""
+
+import argparse
+import gzip
+import json
+import sys
+import urllib.request
+
+from lean_demangle import demangle_lean_name
+
+
+def symbolicate_and_demangle(profile, server_url):
+    """
+    Symbolicate a raw samply profile via the symbolication API,
+    then demangle Lean names. Modifies the profile in-place.
+    Returns the number of names resolved.
+    """
+    libs = profile.get("libs", [])
+    memory_map = [[lib["debugName"], lib["breakpadId"]] for lib in libs]
+
+    count = 0
+    for thread in profile.get("threads", []):
+        count += _process_thread(thread, libs, memory_map, server_url)
+
+    return count
+
+
+def _process_thread(thread, libs, memory_map, server_url):
+    """Symbolicate and demangle one thread. Returns count of resolved names."""
+    sa = thread.get("stringArray")
+    ft = thread.get("frameTable")
+    func_t = thread.get("funcTable")
+    rt = thread.get("resourceTable")
+
+    if not all([sa, ft, func_t, rt]):
+        return 0
+
+    # Build mapping: func_index -> (lib_index, address)
+    # A function may be referenced by multiple frames; pick any address.
+    func_info = {}  # func_idx -> (lib_idx, address)
+    for i in range(ft.get("length", 0)):
+        addr = ft["address"][i]
+        func_idx = ft["func"][i]
+        if func_idx in func_info:
+            continue
+        res_idx = func_t["resource"][func_idx]
+        if res_idx < 0 or res_idx >= rt.get("length", 0):
+            continue
+        lib_idx = rt["lib"][res_idx]
+        if lib_idx < 0 or lib_idx >= len(libs):
+            continue
+        func_info[func_idx] = (lib_idx, addr)
+
+    if not func_info:
+        return 0
+
+    # Batch symbolication: group by lib, send all addresses at once
+    frames_to_symbolicate = []
+    func_order = []  # track which func each frame corresponds to
+    for func_idx, (lib_idx, addr) in func_info.items():
+        frames_to_symbolicate.append([lib_idx, addr])
+        func_order.append(func_idx)
+
+    # Call the symbolication API
+    symbols = _call_symbolication_api(
+        server_url, memory_map, frames_to_symbolicate)
+
+    if not symbols:
+        return 0
+
+    # Update stringArray with demangled names
+    count = 0
+    for func_idx, symbol_name in zip(func_order, symbols):
+        if symbol_name is None:
+            continue
+        demangled = demangle_lean_name(symbol_name)
+        name_idx = func_t["name"][func_idx]
+        if name_idx < len(sa):
+            sa[name_idx] = demangled
+            count += 1
+
+    return count
+
+
+def _call_symbolication_api(server_url, memory_map, frames):
+    """
+    Call the Firefox Profiler symbolication API v5.
+    frames: list of [lib_index, address]
+    Returns: list of symbol names (or None for unresolved frames).
+    """
+    url = server_url.rstrip("/") + "/symbolicate/v5"
+
+    # Send all frames as one "stack" in one job
+    req_body = json.dumps({
+        "memoryMap": memory_map,
+        "stacks": [frames],
+    }).encode()
+
+    req = urllib.request.Request(
+        url,
+        data=req_body,
+        headers={"Content-Type": "application/json"},
+    )
+
+    try:
+        with urllib.request.urlopen(req, timeout=60) as resp:
+            result = json.loads(resp.read())
+    except Exception as e:
+        print(f"Symbolication API error: {e}", file=sys.stderr)
+        return None
+
+    if "error" in result:
+        print(f"Symbolication API error: {result['error']}", file=sys.stderr)
+        return None
+
+    # Extract symbol names from result
+    results = result.get("results", [])
+    if not results:
+        return None
+
+    stacks = results[0].get("stacks", [[]])
+    if not stacks:
+        return None
+
+    symbols = []
+    for frame_result in stacks[0]:
+        if isinstance(frame_result, dict):
+            symbols.append(frame_result.get("function"))
+        elif isinstance(frame_result, str):
+            symbols.append(frame_result)
+        else:
+            symbols.append(None)
+
+    return symbols
+
+
+def process_file(input_path, output_path, server_url):
+    """Read a raw profile, symbolicate + demangle, write it back."""
+    is_gzip = input_path.endswith('.gz')
+
+    if is_gzip:
+        with gzip.open(input_path, 'rt', encoding='utf-8') as f:
+            profile = json.load(f)
+    else:
+        with open(input_path, 'r', encoding='utf-8') as f:
+            profile = json.load(f)
+
+    count = symbolicate_and_demangle(profile, server_url)
+
+    out_gzip = output_path.endswith('.gz') if output_path else is_gzip
+    if output_path:
+        if out_gzip:
+            with gzip.open(output_path, 'wt', encoding='utf-8') as f:
+                json.dump(profile, f, ensure_ascii=False)
+        else:
+            with open(output_path, 'w', encoding='utf-8') as f:
+                json.dump(profile, f, ensure_ascii=False)
+    else:
+        json.dump(profile, sys.stdout, ensure_ascii=False)
+        sys.stdout.write('\n')
+
+    return count
+
+
+def main():
+    parser = argparse.ArgumentParser(
+        description="Symbolicate a raw samply profile and demangle Lean names")
+    parser.add_argument('input', help='Raw profile (JSON or .json.gz)')
+    parser.add_argument('-o', '--output', help='Output path')
+    parser.add_argument('--server', required=True,
+                        help='Samply server URL (e.g., http://127.0.0.1:3000/TOKEN)')
+    args = parser.parse_args()
+
+    output = args.output
+    if output is None:
+        inp = args.input
+        if inp.endswith('.json.gz'):
+            output = inp[:-8] + '-demangled.json.gz'
+        elif inp.endswith('.json'):
+            output = inp[:-5] + '-demangled.json'
+        else:
+            output = inp + '-demangled'
+
+    count = process_file(args.input, output, args.server)
+    print(f"Symbolicated and demangled {count} names, wrote {output}",
+          file=sys.stderr)
+
+
+if __name__ == '__main__':
+    main()

script/profiler/test_demangle.py

@@ -0,0 +1,670 @@
+#!/usr/bin/env python3
+"""Tests for the Lean name demangler."""
+
+import unittest
+import json
+import gzip
+import tempfile
+import os
+
+from lean_demangle import (
+    mangle_string, mangle_name, demangle_body, format_name,
+    demangle_lean_name, demangle_lean_name_raw, postprocess_name,
+    _parse_hex, _check_disambiguation,
+)
+
+
+class TestStringMangle(unittest.TestCase):
+    """Test String.mangle (character-level escaping)."""
+
+    def test_alphanumeric(self):
+        self.assertEqual(mangle_string("hello"), "hello")
+        self.assertEqual(mangle_string("abc123"), "abc123")
+
+    def test_underscore(self):
+        self.assertEqual(mangle_string("a_b"), "a__b")
+        self.assertEqual(mangle_string("_"), "__")
+        self.assertEqual(mangle_string("__"), "____")
+
+    def test_special_chars(self):
+        self.assertEqual(mangle_string("."), "_x2e")
+        self.assertEqual(mangle_string("a.b"), "a_x2eb")
+
+    def test_unicode(self):
+        self.assertEqual(mangle_string("\u03bb"), "_u03bb")
+        self.assertEqual(mangle_string("\U0001d55c"), "_U0001d55c")
+
+    def test_empty(self):
+        self.assertEqual(mangle_string(""), "")
+
+
+class TestNameMangle(unittest.TestCase):
+    """Test Name.mangle (hierarchical name mangling)."""
+
+    def test_simple(self):
+        self.assertEqual(mangle_name(["Lean", "Meta", "Sym", "main"]),
+                         "l_Lean_Meta_Sym_main")
+
+    def test_single_component(self):
+        self.assertEqual(mangle_name(["main"]), "l_main")
+
+    def test_numeric_component(self):
+        self.assertEqual(
+            mangle_name(["_private", "Lean", "Meta", "Basic", 0,
+                         "Lean", "Meta", "withMVarContextImp"]),
+            "l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp")
+
+    def test_component_with_underscore(self):
+        self.assertEqual(mangle_name(["a_b"]), "l_a__b")
+        self.assertEqual(mangle_name(["a_b", "c"]), "l_a__b_c")
+
+    def test_disambiguation_digit_start(self):
+        self.assertEqual(mangle_name(["0foo"]), "l_000foo")
+
+    def test_disambiguation_escape_start(self):
+        self.assertEqual(mangle_name(["a", "x27"]), "l_a_00x27")
+
+    def test_numeric_root(self):
+        self.assertEqual(mangle_name([42]), "l_42_")
+        self.assertEqual(mangle_name([42, "foo"]), "l_42__foo")
+
+    def test_component_ending_with_underscore(self):
+        self.assertEqual(mangle_name(["a_", "b"]), "l_a___00b")
+
+    def test_custom_prefix(self):
+        self.assertEqual(mangle_name(["foo"], prefix="lp_pkg_"),
+                         "lp_pkg_foo")
+
+
+class TestDemangleBody(unittest.TestCase):
+    """Test demangle_body (the core Name.demangleAux algorithm)."""
+
+    def test_simple(self):
+        self.assertEqual(demangle_body("Lean_Meta_Sym_main"),
+                         ["Lean", "Meta", "Sym", "main"])
+
+    def test_single(self):
+        self.assertEqual(demangle_body("main"), ["main"])
+
+    def test_empty(self):
+        self.assertEqual(demangle_body(""), [])
+
+    def test_underscore_in_component(self):
+        self.assertEqual(demangle_body("a__b"), ["a_b"])
+        self.assertEqual(demangle_body("a__b_c"), ["a_b", "c"])
+
+    def test_numeric_component(self):
+        self.assertEqual(demangle_body("foo_42__bar"), ["foo", 42, "bar"])
+
+    def test_numeric_root(self):
+        self.assertEqual(demangle_body("42_"), [42])
+
+    def test_numeric_at_end(self):
+        self.assertEqual(demangle_body("foo_42_"), ["foo", 42])
+
+    def test_disambiguation_00(self):
+        self.assertEqual(demangle_body("a_00x27"), ["a", "x27"])
+
+    def test_disambiguation_00_at_root(self):
+        self.assertEqual(demangle_body("000foo"), ["0foo"])
+
+    def test_hex_escape_x(self):
+        self.assertEqual(demangle_body("a_x2eb"), ["a.b"])
+
+    def test_hex_escape_u(self):
+        self.assertEqual(demangle_body("_u03bb"), ["\u03bb"])
+
+    def test_hex_escape_U(self):
+        self.assertEqual(demangle_body("_U0001d55c"), ["\U0001d55c"])
+
+    def test_private_name(self):
+        body = "__private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp"
+        self.assertEqual(demangle_body(body),
+                         ["_private", "Lean", "Meta", "Basic", 0,
+                          "Lean", "Meta", "withMVarContextImp"])
+
+    def test_boxed_suffix(self):
+        body = "foo___boxed"
+        self.assertEqual(demangle_body(body), ["foo", "_boxed"])
+
+    def test_redArg_suffix(self):
+        body = "foo_bar___redArg"
+        self.assertEqual(demangle_body(body), ["foo", "bar", "_redArg"])
+
+    def test_component_ending_underscore_disambiguation(self):
+        self.assertEqual(demangle_body("a___00b"), ["a_", "b"])
+
+
+class TestRoundTrip(unittest.TestCase):
+    """Test that mangle(demangle(x)) == x for various names."""
+
+    def _check_roundtrip(self, components):
+        mangled = mangle_name(components, prefix="")
+        demangled = demangle_body(mangled)
+        self.assertEqual(demangled, components,
+                         f"Round-trip failed: {components} -> '{mangled}' -> {demangled}")
+        mangled_with_prefix = mangle_name(components, prefix="l_")
+        self.assertTrue(mangled_with_prefix.startswith("l_"))
+        body = mangled_with_prefix[2:]
+        demangled2 = demangle_body(body)
+        self.assertEqual(demangled2, components)
+
+    def test_simple_names(self):
+        self._check_roundtrip(["Lean", "Meta", "main"])
+        self._check_roundtrip(["a"])
+        self._check_roundtrip(["Foo", "Bar", "baz"])
+
+    def test_numeric(self):
+        self._check_roundtrip(["foo", 0, "bar"])
+        self._check_roundtrip([42])
+        self._check_roundtrip(["a", 1, "b", 2, "c"])
+
+    def test_underscores(self):
+        self._check_roundtrip(["_private"])
+        self._check_roundtrip(["a_b", "c_d"])
+        self._check_roundtrip(["_at_", "_spec"])
+
+    def test_private_name(self):
+        self._check_roundtrip(["_private", "Lean", "Meta", "Basic", 0,
+                                "Lean", "Meta", "withMVarContextImp"])
+
+    def test_boxed(self):
+        self._check_roundtrip(["Lean", "Meta", "foo", "_boxed"])
+
+    def test_redArg(self):
+        self._check_roundtrip(["Lean", "Meta", "foo", "_redArg"])
+
+    def test_specialization(self):
+        self._check_roundtrip(["List", "map", "_at_", "Foo", "bar", "_spec", 3])
+
+    def test_lambda(self):
+        self._check_roundtrip(["Foo", "bar", "_lambda", 0])
+        self._check_roundtrip(["Foo", "bar", "_lambda", 2])
+
+    def test_closed(self):
+        self._check_roundtrip(["myConst", "_closed", 0])
+
+    def test_special_chars(self):
+        self._check_roundtrip(["a.b"])
+        self._check_roundtrip(["\u03bb"])
+        self._check_roundtrip(["a", "b\u2192c"])
+
+    def test_disambiguation_cases(self):
+        self._check_roundtrip(["a", "x27"])
+        self._check_roundtrip(["0foo"])
+        self._check_roundtrip(["a_", "b"])
+
+    def test_complex_real_names(self):
+        """Names modeled after real Lean compiler output."""
+        self._check_roundtrip(
+            ["Lean", "MVarId", "withContext", "_at_",
+             "_private", "Lean", "Meta", "Sym", 0,
+             "Lean", "Meta", "Sym", "BackwardRule", "apply",
+             "_spec", 2, "_redArg", "_lambda", 0, "_boxed"])
+
+
+class TestDemangleRaw(unittest.TestCase):
+    """Test demangle_lean_name_raw (exact demangling, no postprocessing)."""
+
+    def test_l_prefix(self):
+        self.assertEqual(
+            demangle_lean_name_raw("l_Lean_Meta_Sym_main"),
+            "Lean.Meta.Sym.main")
+
+    def test_l_prefix_private(self):
+        result = demangle_lean_name_raw(
+            "l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp")
+        self.assertEqual(result,
+                         "_private.Lean.Meta.Basic.0.Lean.Meta.withMVarContextImp")
+
+    def test_l_prefix_boxed(self):
+        result = demangle_lean_name_raw("l_foo___boxed")
+        self.assertEqual(result, "foo._boxed")
+
+    def test_l_prefix_redArg(self):
+        result = demangle_lean_name_raw(
+            "l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp___redArg")
+        self.assertEqual(
+            result,
+            "_private.Lean.Meta.Basic.0.Lean.Meta.withMVarContextImp._redArg")
+
+    def test_lean_main(self):
+        self.assertEqual(demangle_lean_name_raw("_lean_main"), "[lean] main")
+
+    def test_non_lean_names(self):
+        self.assertEqual(demangle_lean_name_raw("printf"), "printf")
+        self.assertEqual(demangle_lean_name_raw("malloc"), "malloc")
+        self.assertEqual(demangle_lean_name_raw("lean_apply_5"), "lean_apply_5")
+        self.assertEqual(demangle_lean_name_raw(""), "")
+
+    def test_init_prefix(self):
+        result = demangle_lean_name_raw("_init_l_Lean_Meta_foo")
+        self.assertEqual(result, "[init] Lean.Meta.foo")
+
+    def test_lp_prefix_simple(self):
+        mangled = mangle_name(["Lean", "Meta", "foo"], prefix="lp_std_")
+        self.assertEqual(mangled, "lp_std_Lean_Meta_foo")
+        result = demangle_lean_name_raw(mangled)
+        self.assertEqual(result, "Lean.Meta.foo (std)")
+
+    def test_lp_prefix_underscore_pkg(self):
+        pkg_mangled = mangle_string("my_pkg")
+        self.assertEqual(pkg_mangled, "my__pkg")
+        mangled = mangle_name(["Lean", "Meta", "foo"],
+                              prefix=f"lp_{pkg_mangled}_")
+        self.assertEqual(mangled, "lp_my__pkg_Lean_Meta_foo")
+        result = demangle_lean_name_raw(mangled)
+        self.assertEqual(result, "Lean.Meta.foo (my_pkg)")
+
+    def test_lp_prefix_private_decl(self):
+        mangled = mangle_name(
+            ["_private", "X", 0, "Y", "foo"], prefix="lp_pkg_")
+        self.assertEqual(mangled, "lp_pkg___private_X_0__Y_foo")
+        result = demangle_lean_name_raw(mangled)
+        self.assertEqual(result, "_private.X.0.Y.foo (pkg)")
+
+    def test_complex_specialization(self):
+        components = [
+            "Lean", "MVarId", "withContext", "_at_",
+            "_private", "Lean", "Meta", "Sym", 0,
+            "Lean", "Meta", "Sym", "BackwardRule", "apply",
+            "_spec", 2, "_redArg", "_lambda", 0, "_boxed"
+        ]
+        mangled = mangle_name(components)
+        result = demangle_lean_name_raw(mangled)
+        expected = format_name(components)
+        self.assertEqual(result, expected)
+
+    def test_cold_suffix(self):
+        result = demangle_lean_name_raw("l_Lean_Meta_foo___redArg.cold.1")
+        self.assertEqual(result, "Lean.Meta.foo._redArg .cold.1")
+
+    def test_cold_suffix_plain(self):
+        result = demangle_lean_name_raw("l_Lean_Meta_foo.cold")
+        self.assertEqual(result, "Lean.Meta.foo .cold")
+
+    def test_initialize_no_pkg(self):
+        result = demangle_lean_name_raw("initialize_Init_Control_Basic")
+        self.assertEqual(result, "[module_init] Init.Control.Basic")
+
+    def test_initialize_with_l_prefix(self):
+        result = demangle_lean_name_raw("initialize_l_Lean_Meta_foo")
+        self.assertEqual(result, "[module_init] Lean.Meta.foo")
+
+    def test_never_crashes(self):
+        """Demangling should never raise, just return the original."""
+        weird_inputs = [
+            "", "l_", "lp_", "lp_x", "_init_", "initialize_",
+            "l_____", "lp____", "l_00", "l_0",
+            "some random string", "l_ space",
+        ]
+        for inp in weird_inputs:
+            result = demangle_lean_name_raw(inp)
+            self.assertIsInstance(result, str)
+
+
+class TestPostprocess(unittest.TestCase):
+    """Test postprocess_name (human-friendly suffix folding, etc.)."""
+
+    def test_no_change(self):
+        self.assertEqual(postprocess_name(["Lean", "Meta", "main"]),
+                         "Lean.Meta.main")
+
+    def test_boxed(self):
+        self.assertEqual(postprocess_name(["foo", "_boxed"]),
+                         "foo [boxed]")
+
+    def test_redArg(self):
+        self.assertEqual(postprocess_name(["foo", "bar", "_redArg"]),
+                         "foo.bar [arity\u2193]")
+
+    def test_lambda_separate(self):
+        # _lam as separate component + numeric index
+        self.assertEqual(postprocess_name(["foo", "_lam", 0]),
+                         "foo [\u03bb]")
+
+    def test_lambda_indexed(self):
+        # _lam_0 as single string (appendIndexAfter)
+        self.assertEqual(postprocess_name(["foo", "_lam_0"]),
+                         "foo [\u03bb]")
+        self.assertEqual(postprocess_name(["foo", "_lambda_2"]),
+                         "foo [\u03bb]")
+
+    def test_lambda_boxed(self):
+        # _lam_0 followed by _boxed
+        self.assertEqual(
+            postprocess_name(["Lean", "Meta", "Simp", "simpLambda",
+                              "_lam_0", "_boxed"]),
+            "Lean.Meta.Simp.simpLambda [boxed, \u03bb]")
+
+    def test_closed(self):
+        self.assertEqual(postprocess_name(["myConst", "_closed", 3]),
+                         "myConst [closed]")
+
+    def test_closed_indexed(self):
+        self.assertEqual(postprocess_name(["myConst", "_closed_0"]),
+                         "myConst [closed]")
+
+    def test_multiple_suffixes(self):
+        self.assertEqual(postprocess_name(["foo", "_redArg", "_boxed"]),
+                         "foo [boxed, arity\u2193]")
+
+    def test_redArg_lam(self):
+        # _redArg followed by _lam_0 (issue #4)
+        self.assertEqual(
+            postprocess_name(["Lean", "profileitIOUnsafe",
+                              "_redArg", "_lam_0"]),
+            "Lean.profileitIOUnsafe [\u03bb, arity\u2193]")
+
+    def test_private_name(self):
+        self.assertEqual(
+            postprocess_name(["_private", "Lean", "Meta", "Basic", 0,
+                              "Lean", "Meta", "withMVarContextImp"]),
+            "Lean.Meta.withMVarContextImp [private]")
+
+    def test_private_with_suffix(self):
+        self.assertEqual(
+            postprocess_name(["_private", "Lean", "Meta", "Basic", 0,
+                              "Lean", "Meta", "foo", "_redArg"]),
+            "Lean.Meta.foo [arity\u2193, private]")
+
+    def test_hygienic_strip(self):
+        self.assertEqual(
+            postprocess_name(["Lean", "Meta", "foo", "_@", "Lean", "Meta",
+                              "_hyg", 42]),
+            "Lean.Meta.foo")
+
+    def test_specialization(self):
+        self.assertEqual(
+            postprocess_name(["List", "map", "_at_", "Foo", "bar",
+                              "_spec", 3]),
+            "List.map spec at Foo.bar")
+
+    def test_specialization_with_suffix(self):
+        # Base suffix _boxed appears in [flags] before spec at
+        self.assertEqual(
+            postprocess_name(["Lean", "MVarId", "withContext", "_at_",
+                              "Foo", "bar", "_spec", 2, "_boxed"]),
+            "Lean.MVarId.withContext [boxed] spec at Foo.bar")
+
+    def test_spec_context_with_flags(self):
+        # Compiler suffixes in spec context become context flags
+        self.assertEqual(
+            postprocess_name(["Lean", "Meta", "foo", "_at_",
+                              "Lean", "Meta", "bar", "_elam_1", "_redArg",
+                              "_spec", 2]),
+            "Lean.Meta.foo spec at Lean.Meta.bar[\u03bb, arity\u2193]")
+
+    def test_spec_context_flags_dedup(self):
+        # Duplicate flag labels are deduplicated
+        self.assertEqual(
+            postprocess_name(["f", "_at_",
+                              "g", "_lam_0", "_elam_1", "_redArg",
+                              "_spec", 1]),
+            "f spec at g[\u03bb, arity\u2193]")
+
+    def test_multiple_at(self):
+        # Multiple _at_ entries become separate spec at clauses
+        self.assertEqual(
+            postprocess_name(["f", "_at_", "g", "_spec", 1,
+                              "_at_", "h", "_spec", 2]),
+            "f spec at g spec at h")
+
+    def test_multiple_at_with_flags(self):
+        # Multiple spec at with flags on base and contexts
+        self.assertEqual(
+            postprocess_name(["f", "_at_", "g", "_redArg", "_spec", 1,
+                              "_at_", "h", "_lam_0", "_spec", 2,
+                              "_boxed"]),
+            "f [boxed] spec at g[arity\u2193] spec at h[\u03bb]")
+
+    def test_base_flags_before_spec(self):
+        # Base trailing suffixes appear in [flags] before spec at
+        self.assertEqual(
+            postprocess_name(["f", "_at_", "g", "_spec", 1, "_lam_0"]),
+            "f [\u03bb] spec at g")
+
+    def test_spec_context_strip_spec_suffixes(self):
+        # spec_0 in context should be stripped
+        self.assertEqual(
+            postprocess_name(["Lean", "Meta", "transformWithCache", "visit",
+                              "_at_",
+                              "_private", "Lean", "Meta", "Transform", 0,
+                              "Lean", "Meta", "transform",
+                              "Lean", "Meta", "Sym", "unfoldReducible",
+                              "spec_0", "spec_0",
+                              "_spec", 1]),
+            "Lean.Meta.transformWithCache.visit "
+            "spec at Lean.Meta.transform.Lean.Meta.Sym.unfoldReducible")
+
+    def test_spec_context_strip_private(self):
+        # _private in spec context should be stripped
+        self.assertEqual(
+            postprocess_name(["Array", "mapMUnsafe", "map", "_at_",
+                              "_private", "Lean", "Meta", "Transform", 0,
+                              "Lean", "Meta", "transformWithCache", "visit",
+                              "_spec", 1]),
+            "Array.mapMUnsafe.map "
+            "spec at Lean.Meta.transformWithCache.visit")
+
+    def test_empty(self):
+        self.assertEqual(postprocess_name([]), "")
+
+
+class TestDemangleHumanFriendly(unittest.TestCase):
+    """Test demangle_lean_name (human-friendly output)."""
+
+    def test_simple(self):
+        self.assertEqual(demangle_lean_name("l_Lean_Meta_main"),
+                         "Lean.Meta.main")
+
+    def test_boxed(self):
+        self.assertEqual(demangle_lean_name("l_foo___boxed"),
+                         "foo [boxed]")
+
+    def test_redArg(self):
+        self.assertEqual(demangle_lean_name("l_foo___redArg"),
+                         "foo [arity\u2193]")
+
+    def test_private(self):
+        self.assertEqual(
+            demangle_lean_name(
+                "l___private_Lean_Meta_Basic_0__Lean_Meta_foo"),
+            "Lean.Meta.foo [private]")
+
+    def test_private_with_redArg(self):
+        self.assertEqual(
+            demangle_lean_name(
+                "l___private_Lean_Meta_Basic_0__Lean_Meta_foo___redArg"),
+            "Lean.Meta.foo [arity\u2193, private]")
+
+    def test_cold_with_suffix(self):
+        self.assertEqual(
+            demangle_lean_name("l_Lean_Meta_foo___redArg.cold.1"),
+            "Lean.Meta.foo [arity\u2193] .cold.1")
+
+    def test_lean_apply(self):
+        self.assertEqual(demangle_lean_name("lean_apply_5"), "<apply/5>")
+        self.assertEqual(demangle_lean_name("lean_apply_12"), "<apply/12>")
+
+    def test_lean_apply_raw_unchanged(self):
+        self.assertEqual(demangle_lean_name_raw("lean_apply_5"),
+                         "lean_apply_5")
+
+    def test_init_private(self):
+        self.assertEqual(
+            demangle_lean_name(
+                "_init_l___private_X_0__Y_foo"),
+            "[init] Y.foo [private]")
+
+    def test_complex_specialization(self):
+        components = [
+            "Lean", "MVarId", "withContext", "_at_",
+            "_private", "Lean", "Meta", "Sym", 0,
+            "Lean", "Meta", "Sym", "BackwardRule", "apply",
+            "_spec", 2, "_redArg", "_lambda", 0, "_boxed"
+        ]
+        mangled = mangle_name(components)
+        result = demangle_lean_name(mangled)
+        # Base: Lean.MVarId.withContext with trailing _redArg, _lambda 0, _boxed
+        # Spec context: Lean.Meta.Sym.BackwardRule.apply (private stripped)
+        self.assertEqual(
+            result,
+            "Lean.MVarId.withContext [boxed, \u03bb, arity\u2193] "
+            "spec at Lean.Meta.Sym.BackwardRule.apply")
+
+    def test_non_lean_unchanged(self):
+        self.assertEqual(demangle_lean_name("printf"), "printf")
+        self.assertEqual(demangle_lean_name("malloc"), "malloc")
+        self.assertEqual(demangle_lean_name(""), "")
+
+
+class TestDemangleProfile(unittest.TestCase):
+    """Test the profile rewriter."""
+
+    def _make_profile_shared(self, strings):
+        """Create a profile with shared.stringArray (newer format)."""
+        return {
+            "meta": {"version": 28},
+            "libs": [],
+            "shared": {
+                "stringArray": list(strings),
+            },
+            "threads": [{
+                "name": "main",
+                "pid": "1",
+                "tid": 1,
+                "funcTable": {
+                    "name": list(range(len(strings))),
+                    "isJS": [False] * len(strings),
+                    "relevantForJS": [False] * len(strings),
+                    "resource": [-1] * len(strings),
+                    "fileName": [None] * len(strings),
+                    "lineNumber": [None] * len(strings),
+                    "columnNumber": [None] * len(strings),
+                    "length": len(strings),
+                },
+                "frameTable": {"length": 0},
+                "stackTable": {"length": 0},
+                "samples": {"length": 0},
+                "markers": {"length": 0},
+                "resourceTable": {"length": 0},
+                "nativeSymbols": {"length": 0},
+            }],
+            "pages": [],
+            "counters": [],
+        }
+
+    def _make_profile_per_thread(self, strings):
+        """Create a profile with per-thread stringArray (samply format)."""
+        return {
+            "meta": {"version": 28},
+            "libs": [],
+            "threads": [{
+                "name": "main",
+                "pid": "1",
+                "tid": 1,
+                "stringArray": list(strings),
+                "funcTable": {
+                    "name": list(range(len(strings))),
+                    "isJS": [False] * len(strings),
+                    "relevantForJS": [False] * len(strings),
+                    "resource": [-1] * len(strings),
+                    "fileName": [None] * len(strings),
+                    "lineNumber": [None] * len(strings),
+                    "columnNumber": [None] * len(strings),
+                    "length": len(strings),
+                },
+                "frameTable": {"length": 0},
+                "stackTable": {"length": 0},
+                "samples": {"length": 0},
+                "markers": {"length": 0},
+                "resourceTable": {"length": 0},
+                "nativeSymbols": {"length": 0},
+            }],
+            "pages": [],
+            "counters": [],
+        }
+
+    def test_profile_rewrite_shared(self):
+        from lean_demangle_profile import rewrite_profile
+        strings = [
+            "l_Lean_Meta_Sym_main",
+            "printf",
+            "lean_apply_5",
+            "l___private_Lean_Meta_Basic_0__Lean_Meta_foo",
+        ]
+        profile = self._make_profile_shared(strings)
+        rewrite_profile(profile)
+        sa = profile["shared"]["stringArray"]
+        self.assertEqual(sa[0], "Lean.Meta.Sym.main")
+        self.assertEqual(sa[1], "printf")
+        self.assertEqual(sa[2], "<apply/5>")
+        self.assertEqual(sa[3], "Lean.Meta.foo [private]")
+
+    def test_profile_rewrite_per_thread(self):
+        from lean_demangle_profile import rewrite_profile
+        strings = [
+            "l_Lean_Meta_Sym_main",
+            "printf",
+            "lean_apply_5",
+            "l___private_Lean_Meta_Basic_0__Lean_Meta_foo",
+        ]
+        profile = self._make_profile_per_thread(strings)
+        count = rewrite_profile(profile)
+        sa = profile["threads"][0]["stringArray"]
+        self.assertEqual(sa[0], "Lean.Meta.Sym.main")
+        self.assertEqual(sa[1], "printf")
+        self.assertEqual(sa[2], "<apply/5>")
+        self.assertEqual(sa[3], "Lean.Meta.foo [private]")
+        self.assertEqual(count, 3)
+
+    def test_profile_json_roundtrip(self):
+        from lean_demangle_profile import process_profile_file
+        strings = ["l_Lean_Meta_main", "malloc"]
+        profile = self._make_profile_shared(strings)
+
+        with tempfile.NamedTemporaryFile(mode='w', suffix='.json',
+                                         delete=False) as f:
+            json.dump(profile, f)
+            inpath = f.name
+
+        outpath = inpath.replace('.json', '-demangled.json')
+        try:
+            process_profile_file(inpath, outpath)
+            with open(outpath) as f:
+                result = json.load(f)
+            self.assertEqual(result["shared"]["stringArray"][0],
+                             "Lean.Meta.main")
+            self.assertEqual(result["shared"]["stringArray"][1], "malloc")
+        finally:
+            os.unlink(inpath)
+            if os.path.exists(outpath):
+                os.unlink(outpath)
+
+    def test_profile_gzip_roundtrip(self):
+        from lean_demangle_profile import process_profile_file
+        strings = ["l_Lean_Meta_main", "malloc"]
+        profile = self._make_profile_shared(strings)
+
+        with tempfile.NamedTemporaryFile(suffix='.json.gz',
+                                         delete=False) as f:
+            with gzip.open(f, 'wt') as gz:
+                json.dump(profile, gz)
+            inpath = f.name
+
+        outpath = inpath.replace('.json.gz', '-demangled.json.gz')
+        try:
+            process_profile_file(inpath, outpath)
+            with gzip.open(outpath, 'rt') as f:
+                result = json.load(f)
+            self.assertEqual(result["shared"]["stringArray"][0],
+                             "Lean.Meta.main")
+        finally:
+            os.unlink(inpath)
+            if os.path.exists(outpath):
+                os.unlink(outpath)
+
+
+if __name__ == '__main__':
+    unittest.main()

script/release_checklist.py

@@ -836,6 +836,14 @@ def main():
             continue
         print(f"  ✅ On compatible toolchain (>= {toolchain})")
 
+        # For reference-manual, check that the release notes title is correct BEFORE tagging.
+        # This catches the case where the toolchain bump PR was merged without updating
+        # the release notes title (e.g., still showing "-rc1" for a stable release).
+        if name == "reference-manual":
+            if not check_reference_manual_release_title(url, toolchain, branch, github_token):
+                repo_status[name] = False
+                continue
+
         # Special handling for ProofWidgets4
         if name == "ProofWidgets4":
             if not check_proofwidgets4_release(url, toolchain, github_token):
@@ -916,8 +924,8 @@ def main():
             
             print(f"  ✅ Bump branch {bump_branch} exists")
             
-            # For batteries and mathlib4, update the lean-toolchain to the latest nightly
-            if branch_created and name in ["batteries", "mathlib4"]:
+            # Update the lean-toolchain to the latest nightly for newly created bump branches
+            if branch_created:
                 latest_nightly = get_latest_nightly_tag(github_token)
                 if latest_nightly:
                     nightly_toolchain = f"leanprover/lean4:{latest_nightly}"

script/release_repos.yml

@@ -65,13 +65,6 @@ repositories:
     branch: master
     dependencies: [lean4-unicode-basic]
 
-  - name: doc-gen4
-    url: https://github.com/leanprover/doc-gen4
-    toolchain-tag: true
-    stable-branch: false
-    branch: main
-    dependencies: [lean4-cli, BibtexQuery]
-
   - name: reference-manual
     url: https://github.com/leanprover/reference-manual
     toolchain-tag: true
@@ -84,8 +77,7 @@ repositories:
     toolchain-tag: false
     stable-branch: false
     branch: main
-    dependencies:
-      - batteries
+    dependencies: []
 
   - name: aesop
     url: https://github.com/leanprover-community/aesop
@@ -107,10 +99,16 @@ repositories:
       - lean4checker
       - batteries
       - lean4-cli
-      - doc-gen4
       - import-graph
       - plausible
 
+  - name: doc-gen4
+    url: https://github.com/leanprover/doc-gen4
+    toolchain-tag: true
+    stable-branch: false
+    branch: main
+    dependencies: [lean4-cli, BibtexQuery, mathlib4]
+
   - name: cslib
     url: https://github.com/leanprover/cslib
     toolchain-tag: true

script/release_steps.py

@@ -24,6 +24,7 @@ What this script does:
    - Safety checks for repositories using bump branches
    - Custom build and test procedures
    - lean-fro.org: runs scripts/update.sh to regenerate site content
+   - mathlib4: updates ProofWidgets4 pin (v0.0.X sequential tags, not v4.X.Y)
 
 6. Commits the changes with message "chore: bump toolchain to {version}"
 
@@ -59,6 +60,8 @@ import re
 import subprocess
 import shutil
 import json
+import requests
+import base64
 from pathlib import Path
 
 # Color functions for terminal output
@@ -115,6 +118,60 @@ def find_repo(repo_name, config):
         sys.exit(1)
     return matching_repos[0]
 
+def get_github_token():
+    try:
+        result = subprocess.run(['gh', 'auth', 'token'], capture_output=True, text=True)
+        if result.returncode == 0:
+            return result.stdout.strip()
+    except FileNotFoundError:
+        pass
+    return None
+
+def find_proofwidgets_tag(version):
+    """Find the latest ProofWidgets4 tag that uses the given toolchain version.
+
+    ProofWidgets4 uses sequential version tags (v0.0.X) rather than toolchain-based tags.
+    This function finds the most recent tag whose lean-toolchain matches the target version
+    exactly, checking the 20 most recent tags.
+    """
+    github_token = get_github_token()
+    api_base = "https://api.github.com/repos/leanprover-community/ProofWidgets4"
+    headers = {'Authorization': f'token {github_token}'} if github_token else {}
+
+    response = requests.get(f"{api_base}/git/matching-refs/tags/v0.0.", headers=headers, timeout=30)
+    if response.status_code != 200:
+        return None
+
+    tags = response.json()
+    tag_names = []
+    for tag in tags:
+        ref = tag['ref']
+        if ref.startswith('refs/tags/v0.0.'):
+            tag_name = ref.replace('refs/tags/', '')
+            try:
+                version_num = int(tag_name.split('.')[-1])
+                tag_names.append((version_num, tag_name))
+            except (ValueError, IndexError):
+                continue
+
+    if not tag_names:
+        return None
+
+    # Sort by version number (descending) and check recent tags
+    tag_names.sort(reverse=True)
+    target = f"leanprover/lean4:{version}"
+    for _, tag_name in tag_names[:20]:
+        # Fetch lean-toolchain for this tag
+        api_url = f"{api_base}/contents/lean-toolchain?ref={tag_name}"
+        resp = requests.get(api_url, headers=headers, timeout=30)
+        if resp.status_code != 200:
+            continue
+        content = base64.b64decode(resp.json().get("content", "").replace("\n", "")).decode('utf-8').strip()
+        if content == target:
+            return tag_name
+
+    return None
+
 def setup_downstream_releases_dir():
     """Create the downstream_releases directory if it doesn't exist."""
     downstream_dir = Path("downstream_releases")
@@ -426,6 +483,62 @@ def execute_release_steps(repo, version, config):
         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)
 
+    # For reference-manual, update the release notes title to match the target version.
+    # e.g., for a stable release, change "Lean 4.28.0-rc1 (date)" to "Lean 4.28.0 (date)"
+    # e.g., for rc2, change "Lean 4.28.0-rc1 (date)" to "Lean 4.28.0-rc2 (date)"
+    if repo_name == "reference-manual":
+        base_version = version.lstrip('v').split('-')[0]  # "4.28.0"
+        file_name = f"v{base_version.replace('.', '_')}.lean"
+        release_notes_file = repo_path / "Manual" / "Releases" / file_name
+
+        if release_notes_file.exists():
+            is_rc = "-rc" in version
+            if is_rc:
+                # For RC releases, update to the exact RC version
+                display_version = version.lstrip('v')  # "4.28.0-rc2"
+            else:
+                # For stable releases, strip any RC suffix
+                display_version = base_version  # "4.28.0"
+
+            print(blue(f"Updating release notes title in {file_name}..."))
+            content = release_notes_file.read_text()
+            # Match the #doc line title: "Lean X.Y.Z-rcN (date)" or "Lean X.Y.Z (date)"
+            new_content = re.sub(
+                r'(#doc\s+\(Manual\)\s+"Lean\s+)\d+\.\d+\.\d+(-rc\d+)?(\s+\([^)]*\)"\s*=>)',
+                rf'\g<1>{display_version}\3',
+                content
+            )
+            if new_content != content:
+                release_notes_file.write_text(new_content)
+                print(green(f"Updated release notes title to Lean {display_version}"))
+            else:
+                print(green("Release notes title already correct"))
+        else:
+            print(yellow(f"Release notes file {file_name} not found, skipping title update"))
+
+    # For mathlib4, update ProofWidgets4 pin (it uses sequential v0.0.X tags, not v4.X.Y)
+    if repo_name == "mathlib4":
+        print(blue("Checking ProofWidgets4 version pin..."))
+        pw_tag = find_proofwidgets_tag(version)
+        if pw_tag:
+            print(blue(f"Updating ProofWidgets4 pin to {pw_tag}..."))
+            for lakefile in repo_path.glob("lakefile.*"):
+                content = lakefile.read_text()
+                # Only update the ProofWidgets4 dependency line, not other v0.0.X pins
+                new_content = re.sub(
+                    r'(require\s+"leanprover-community"\s*/\s*"proofwidgets"\s*@\s*git\s+"v)0\.0\.\d+(")',
+                    rf'\g<1>{pw_tag.removeprefix("v")}\2',
+                    content
+                )
+                if new_content != content:
+                    lakefile.write_text(new_content)
+                    print(green(f"Updated ProofWidgets4 pin in {lakefile.name}"))
+            run_command("lake update proofwidgets", cwd=repo_path, stream_output=True)
+            print(green(f"Updated ProofWidgets4 to {pw_tag}"))
+        else:
+            print(yellow(f"Could not find a ProofWidgets4 tag for toolchain {version}"))
+            print(yellow("You may need to update the ProofWidgets4 pin manually"))
+
     # Commit changes (only if there are changes)
     print(blue("Checking for changes to commit..."))
     try:

src/CMakeLists.txt

@@ -1,6 +1,4 @@
-cmake_minimum_required(VERSION 3.10)
-cmake_policy(SET CMP0054 NEW)
-cmake_policy(SET CMP0110 NEW)
+cmake_minimum_required(VERSION 3.21)
 if(NOT CMAKE_GENERATOR MATCHES "Unix Makefiles")
   message(FATAL_ERROR "The only supported CMake generator at the moment is 'Unix Makefiles'")
 endif()
@@ -10,7 +8,7 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 29)
+set(LEAN_VERSION_MINOR 30)
 set(LEAN_VERSION_PATCH 0)
 set(LEAN_VERSION_IS_RELEASE 0) # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")

src/Init/Classical.lean

@@ -142,7 +142,7 @@ is classically true but not constructively. -/
 
 /-- Transfer decidability of `¬ p` to decidability of `p`. -/
 -- This can not be an instance as it would be tried everywhere.
-@[instance_reducible]
+@[implicit_reducible]
 def decidable_of_decidable_not (p : Prop) [h : Decidable (¬ p)] : Decidable p :=
   match h with
   | isFalse h => isTrue (Classical.not_not.mp h)

src/Init/Control/Do.lean

@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+module
+
+prelude
+public import Init.Control.Except
+public import Init.Control.Option
+
+public section
+
+/-!
+This module provides specialized wrappers around `ExceptT` to support the `do` elaborator.
+
+Specifically, the types here are used to tunnel early `return`, `break` and `continue` through
+non-algebraic higher-order effect combinators such as `tryCatch`.
+-/
+
+/-- A wrapper around `ExceptT` signifying early return. -/
+@[expose]
+abbrev EarlyReturnT (ρ m α) := ExceptT ρ m α
+
+/-- Exit a computation by returning a value `r : ρ` early. -/
+@[always_inline, inline, expose]
+abbrev EarlyReturnT.return {ρ m α} [Monad m] (r : ρ) : EarlyReturnT ρ m α :=
+  throw r
+
+/-- A specialization of `Except.casesOn`. -/
+@[always_inline, inline, expose]
+abbrev EarlyReturn.runK {ρ α : Type u} {β : Type v} (x : Except ρ α) (ret : ρ → β) (pure : α → β) : β :=
+  x.casesOn ret pure
+
+/-- A wrapper around `OptionT` signifying `break` in a loop. -/
+@[expose]
+abbrev BreakT := OptionT
+
+/-- Exit a loop body via `break`. -/
+@[always_inline, inline, expose]
+abbrev BreakT.break {m : Type w → Type x} [Monad m] : BreakT m α := failure
+
+/-- A specialization of `Option.casesOn`. -/
+@[always_inline, inline, expose]
+abbrev Break.runK {α : Type u} {β : Type v} (x : Option α) (breakK : Unit → β) (successK : α → β) : β :=
+  -- Note: The matcher below is used in the elaborator targeting `forIn` loops.
+  -- If you change the order of match arms here, you may need to adjust the elaborator.
+  match x with
+  | some a => successK a
+  | none => breakK ()
+
+/-- A wrapper around `OptionT` signifying `continue` in a loop. -/
+@[expose]
+abbrev ContinueT := OptionT
+
+/-- Exit a loop body via `continue`. -/
+@[always_inline, inline, expose]
+abbrev ContinueT.continue {m : Type w → Type x} [Monad m] : ContinueT m α := failure
+
+/-- A specialization of `Option.casesOn`. -/
+@[always_inline, inline, expose]
+abbrev Continue.runK {α : Type u} {β : Type v} (x : Option α) (continueK : Unit → β) (successK : α → β) : β :=
+  x.casesOn continueK (fun a _ => successK a) ()

src/Init/Control/Id.lean

@@ -79,3 +79,11 @@ instance : LawfulMonadAttach Id where
     exact x.run.2
 
 end Id
+
+/-- Turn a collection with a pure `ForIn` instance into an array. -/
+def ForIn.toArray {α : Type u} [inst : ForIn Id ρ α] (xs : ρ) : Array α :=
+  ForIn.forIn xs Array.empty (fun a acc => pure (.yield (acc.push a))) |> Id.run
+
+/-- Turn a collection with a pure `ForIn` instance into a list. -/
+def ForIn.toList {α : Type u} [ForIn Id ρ α] (xs : ρ) : List α :=
+  ForIn.toArray xs |>.toList

src/Init/Control/Lawful/Instances.lean

@@ -30,6 +30,8 @@ namespace ExceptT
   simp [run] at h
   assumption
 
+@[simp] theorem stM_eq [Monad m] : stM m (ExceptT ε m) α = Except ε α := rfl
+
 @[simp, grind =] theorem run_mk (x : m (Except ε α)) : run (mk x : ExceptT ε m α) = x := rfl
 
 @[simp, grind =] theorem run_pure [Monad m] (x : α) : run (pure x : ExceptT ε m α) = pure (Except.ok x) := rfl
@@ -118,7 +120,7 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (ExceptT ε m) where
 
 @[simp] theorem run_controlAt [Monad m] [LawfulMonad m] (f : ({β : Type u} → ExceptT ε m β → m (stM m (ExceptT ε m) β)) → m (stM m (ExceptT ε m) α)) :
     ExceptT.run (controlAt m f) = f fun x => x.run := by
-  simp [controlAt, run_bind, bind_map_left]
+  simp [controlAt, run_bind]
 
 @[simp] theorem run_control [Monad m] [LawfulMonad m] (f : ({β : Type u} → ExceptT ε m β → m (stM m (ExceptT ε m) β)) → m (stM m (ExceptT ε m) α)) :
     ExceptT.run (control f) = f fun x => x.run := run_controlAt f
@@ -437,7 +439,6 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (StateT σ m) where
 @[simp] theorem run_restoreM [Monad m] [LawfulMonad m] (x : stM m (StateT σ m) α) (s : σ) :
     StateT.run (restoreM x) s = pure x := by
   simp [restoreM, MonadControl.restoreM]
-  rfl
 
 @[simp] theorem run_liftWith [Monad m] [LawfulMonad m] (f : ({β : Type u} → StateT σ m β → m (stM m (StateT σ m) β)) → m α) (s : σ) :
     StateT.run (liftWith f) s = ((·, s) <$> f fun x => x.run s) := by

src/Init/Control/Lawful/MonadAttach/Instances.lean

@@ -15,7 +15,8 @@ public import Init.Ext
 public instance [Monad m] [LawfulMonad m] [MonadAttach m] [WeaklyLawfulMonadAttach m] :
     WeaklyLawfulMonadAttach (ReaderT ρ m) where
   map_attach := by
-    simp only [Functor.map, MonadAttach.attach, Functor.map_map, WeaklyLawfulMonadAttach.map_attach]
+    simp only [Functor.map, MonadAttach.attach, Functor.map_map, WeaklyLawfulMonadAttach.map_attach,
+      MonadAttach.CanReturn]
     intros; rfl
 
 public instance [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m] :
@@ -30,7 +31,7 @@ public instance [Monad m] [LawfulMonad m] [MonadAttach m] [WeaklyLawfulMonadAtta
   map_attach := by
     intro α x
     simp only [Functor.map, StateT, funext_iff, StateT.map, bind_pure_comp, MonadAttach.attach,
-      Functor.map_map]
+      Functor.map_map, MonadAttach.CanReturn]
     exact fun s => WeaklyLawfulMonadAttach.map_attach
 
 public instance [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m] :
@@ -45,7 +46,7 @@ public instance [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m]
 public instance [Monad m] [LawfulMonad m] [MonadAttach m] [WeaklyLawfulMonadAttach m] :
     WeaklyLawfulMonadAttach (ExceptT ε m) where
   map_attach {α} x := by
-    simp only [Functor.map, MonadAttach.attach, ExceptT.map]
+    simp only [Functor.map, MonadAttach.attach, ExceptT.map, MonadAttach.CanReturn]
     simp
     conv => rhs; rw [← WeaklyLawfulMonadAttach.map_attach (m := m) (x := x)]
     simp only [map_eq_pure_bind]
@@ -83,6 +84,6 @@ attribute [local instance] MonadAttach.trivial
 
 public instance [Monad m] [LawfulMonad m] :
     WeaklyLawfulMonadAttach m where
-  map_attach := by simp [MonadAttach.attach]
+  map_attach := by simp [MonadAttach.attach, MonadAttach.CanReturn]
 
 end

src/Init/Control/MonadAttach.lean

@@ -70,7 +70,7 @@ information to the return value, except a trivial proof of {name}`True`.
 This instance is used whenever no more useful {name}`MonadAttach` instance can be implemented.
 It always has a {name}`WeaklyLawfulMonadAttach`, but usually no {name}`LawfulMonadAttach` instance.
 -/
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 public protected def MonadAttach.trivial {m : Type u → Type v} [Monad m] : MonadAttach m where
   CanReturn _ _ := True
   attach x := (⟨·, .intro⟩) <$> x

src/Init/Core.lean

@@ -1339,10 +1339,10 @@ transitive and contains `r`. `TransGen r a z` if and only if there exists a sequ
 -/
 inductive Relation.TransGen {α : Sort u} (r : α → α → Prop) : α → α → Prop
   /-- If `r a b`, then `TransGen r a b`. This is the base case of the transitive closure. -/
-  | single {a b} : r a b → TransGen r a b
+  | single {a b : α} : r a b → TransGen r a b
   /-- If `TransGen r a b` and `r b c`, then `TransGen r a c`.
   This is the inductive case of the transitive closure. -/
-  | tail {a b c} : TransGen r a b → r b c → TransGen r a c
+  | tail {a b c : α} : TransGen r a b → r b c → TransGen r a c
 
 /-- The transitive closure is transitive. -/
 theorem Relation.TransGen.trans {α : Sort u} {r : α → α → Prop} {a b c} :
@@ -2313,6 +2313,13 @@ instance Pi.instSubsingleton {α : Sort u} {β : α → Sort v} [∀ a, Subsingl
 
 /-! # Squash -/
 
+theorem equivalence_true (α : Sort u) : Equivalence fun _ _ : α => True :=
+  ⟨fun _ => trivial, fun _ => trivial, fun _ _ => trivial⟩
+
+/-- Always-true relation as a `Setoid`. -/
+protected def Setoid.trivial (α : Sort u) : Setoid α :=
+  ⟨_, equivalence_true α⟩
+
 /--
 The quotient of `α` by the universal relation. The elements of `Squash α` are those of `α`, but all
 of them are equal and cannot be distinguished.
@@ -2326,8 +2333,11 @@ and its representation in compiled code is identical to that of `α`.
 
 Consequently, `Squash.lift` may extract an `α` value into any subsingleton type `β`, while
 `Nonempty.rec` can only do the same when `β` is a proposition.
+
+`Squash` is defined in terms of `Quotient`, so `Squash` can be used when a `Quotient` argument is
+expected.
 -/
-def Squash (α : Sort u) := Quot (fun (_ _ : α) => True)
+def Squash (α : Sort u) := Quotient (Setoid.trivial α)
 
 /--
 Places a value into its squash type, in which it cannot be distinguished from any other.
@@ -2583,3 +2593,11 @@ class Trichotomous (r : α → α → Prop) : Prop where
   trichotomous (a b : α) : ¬ r a b → ¬ r b a → a = b
 
 end Std
+
+@[simp] theorem flip_flip {α : Sort u} {β : Sort v} {φ : Sort w} {f : α → β → φ} :
+    flip (flip f) = f := by
+  apply funext
+  intro a
+  apply funext
+  intro b
+  rw [flip, flip]

src/Init/Data/Array/Basic.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
+public import Init.Control.Do
 public import Init.GetElem
 public import Init.Data.List.ToArrayImpl
 import all Init.Data.List.ToArrayImpl
@@ -170,6 +171,15 @@ This avoids overhead due to unboxing a `Nat` used as an index.
 def uget (xs : @& Array α) (i : USize) (h : i.toNat < xs.size) : α :=
   xs[i.toNat]
 
+/--
+Version of `Array.uget` that does not increment the reference count of its result.
+
+This is only intended for direct use by the compiler.
+-/
+@[extern "lean_array_uget_borrowed"]
+unsafe opaque ugetBorrowed (xs : @& Array α) (i : USize) (h : i.toNat < xs.size) : α :=
+  xs.uget i h
+
 /--
 Low-level modification operator which is as fast as a C array write. The modification is performed
 in-place when the reference to the array is unique.

src/Init/Data/Array/Bootstrap.lean

@@ -52,7 +52,9 @@ theorem foldrM_eq_reverse_foldlM_toList.aux [Monad m]
   unfold foldrM.fold
   match i with
   | 0 => simp
-  | i+1 => rw [← List.take_concat_get h]; simp [← aux]
+  | i+1 =>
+    set_option backward.isDefEq.respectTransparency false in
+    rw [← List.take_concat_get h]; simp [← aux]
 
 theorem foldrM_eq_reverse_foldlM_toList [Monad m] {f : α → β → m β} {init : β} {xs : Array α} :
     xs.foldrM f init = xs.toList.reverse.foldlM (fun x y => f y x) init := by

src/Init/Data/Array/Count.lean

@@ -117,11 +117,13 @@ grind_pattern Std.Internal.Array.not_of_countP_eq_zero_of_mem => xs.countP p, x
 theorem countP_replicate {a : α} {n : Nat} : countP p (replicate n a) = if p a then n else 0 := by
   simp [← List.toArray_replicate, List.countP_replicate]
 
+set_option backward.isDefEq.respectTransparency false in
 theorem boole_getElem_le_countP {xs : Array α} {i : Nat} (h : i < xs.size) :
     (if p xs[i] then 1 else 0) ≤ xs.countP p := by
   rcases xs with ⟨xs⟩
   simp [List.boole_getElem_le_countP]
 
+set_option backward.isDefEq.respectTransparency false in
 @[grind =]
 theorem countP_set {xs : Array α} {i : Nat} {a : α} (h : i < xs.size) :
     (xs.set i a).countP p = xs.countP p - (if p xs[i] then 1 else 0) + (if p a then 1 else 0) := by

src/Init/Data/Array/DecidableEq.lean

@@ -76,7 +76,7 @@ theorem isEqv_eq_decide (xs ys : Array α) (r) :
     simpa [isEqv_iff_rel] using h'
 
 @[simp, grind =] theorem isEqv_toList [BEq α] (xs ys : Array α) : (xs.toList.isEqv ys.toList r) = (xs.isEqv ys r) := by
-  simp [isEqv_eq_decide, List.isEqv_eq_decide, Array.size]
+  simp [isEqv_eq_decide, List.isEqv_eq_decide, Array.size]; rfl
 
 theorem eq_of_isEqv [DecidableEq α] (xs ys : Array α) (h : Array.isEqv xs ys (fun x y => x = y)) : xs = ys := by
   have ⟨h, h'⟩ := rel_of_isEqv h
@@ -87,6 +87,7 @@ private theorem isEqvAux_self (r : α → α → Bool) (hr : ∀ a, r a a) (xs :
   induction i with
   | zero => simp [Array.isEqvAux]
   | succ i ih =>
+    set_option backward.isDefEq.respectTransparency false in
     simp_all only [isEqvAux, Bool.and_self]
 
 theorem isEqv_self_beq [BEq α] [ReflBEq α] (xs : Array α) : Array.isEqv xs xs (· == ·) = true := by
@@ -153,7 +154,7 @@ theorem beq_eq_decide [BEq α] (xs ys : Array α) :
   simp [BEq.beq, isEqv_eq_decide]
 
 @[simp, grind =] theorem beq_toList [BEq α] (xs ys : Array α) : (xs.toList == ys.toList) = (xs == ys) := by
-  simp [beq_eq_decide, List.beq_eq_decide, Array.size]
+  simp [beq_eq_decide, List.beq_eq_decide, Array.size]; rfl
 
 end Array
 

src/Init/Data/Array/Erase.lean

@@ -329,7 +329,7 @@ theorem eraseIdx_eq_take_drop_succ {xs : Array α} {i : Nat} (h) :
   rcases xs with ⟨xs⟩
   simp only [List.size_toArray] at h
   simp only [List.eraseIdx_toArray, List.eraseIdx_eq_take_drop_succ, take_eq_extract,
-    List.extract_toArray, List.extract_eq_drop_take, Nat.sub_zero, List.drop_zero, drop_eq_extract,
+    List.extract_toArray, List.extract_eq_take_drop, Nat.sub_zero, List.drop_zero, drop_eq_extract,
     List.size_toArray, List.append_toArray, mk.injEq, List.append_cancel_left_eq]
   rw [List.take_of_length_le]
   simp

src/Init/Data/Array/Find.lean

@@ -83,6 +83,10 @@ theorem findSome?_eq_some_iff {f : α → Option β} {xs : Array α} {b : β} :
   · rintro ⟨xs, a, ys, h₀, h₁, h₂⟩
     exact ⟨xs.toList, a, ys.toList, by simpa using congrArg toList h₀, h₁, by simpa⟩
 
+theorem isSome_findSome? {xs : Array α} {f : α → Option β} :
+    (xs.findSome? f).isSome = xs.any (f · |>.isSome) := by
+  simp [← findSome?_toList, List.isSome_findSome?]
+
 @[simp, grind =] theorem findSome?_guard {xs : Array α} : findSome? (Option.guard p) xs = find? p xs := by
   cases xs; simp
 
@@ -197,6 +201,10 @@ theorem find?_eq_some_iff_append {xs : Array α} :
     exact ⟨as.toList, ⟨l, by simpa using congrArg Array.toList h'⟩,
       by simpa using h⟩
 
+theorem isSome_find? {xs : Array α} {f : α → Bool} :
+    (xs.find? f).isSome = xs.any (f ·) := by
+  simp [← find?_toList, List.isSome_find?]
+
 theorem find?_push {xs : Array α} : (xs.push a).find? p = (xs.find? p).or (if p a then some a else none) := by
   cases xs; simp
 
@@ -425,6 +433,7 @@ theorem lt_findIdx_of_not {p : α → Bool} {xs : Array α} {i : Nat} (h : i < x
   simp only [Nat.not_lt] at f
   exact absurd (@findIdx_getElem _ p xs (Nat.lt_of_le_of_lt f h)) (h2 (xs.findIdx p) f)
 
+set_option backward.isDefEq.respectTransparency false in
 /-- `xs.findIdx p = i` iff `p xs[i]` and `¬ p xs [j]` for all `j < i`. -/
 theorem findIdx_eq {p : α → Bool} {xs : Array α} {i : Nat} (h : i < xs.size) :
     xs.findIdx p = i ↔ p xs[i] ∧ ∀ j (hji : j < i), p (xs[j]'(Nat.lt_trans hji h)) = false := by
@@ -613,12 +622,12 @@ theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : Array α} {p q : α → Bo
 /-! ### findFinIdx? -/
 
 @[grind =]
-theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := by simp
+theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := by simp; rfl
 
 @[grind =]
 theorem findFinIdx?_singleton {a : α} {p : α → Bool} :
     #[a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by
-  simp
+  simp; rfl
 
 -- We can't mark this as a `@[congr]` lemma since the head of the RHS is not `findFinIdx?`.
 theorem findFinIdx?_congr {p : α → Bool} {xs ys : Array α} (w : xs = ys) :
@@ -792,7 +801,7 @@ theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : Array α} {a : α} :
     xs.idxOf? a = (xs.finIdxOf? a).map (·.val) := by
   simp [idxOf?, finIdxOf?]
 
-@[grind =] theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by simp
+@[grind =] theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by simp; rfl
 
 @[simp, grind =] theorem finIdxOf?_eq_none_iff [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     xs.finIdxOf? a = none ↔ a ∉ xs := by

src/Init/Data/Array/Lemmas.lean

@@ -72,6 +72,9 @@ theorem toArray_eq : List.toArray as = xs ↔ as = xs.toList := by
 
 /-! ### size -/
 
+theorem size_singleton {x : α} : #[x].size = 1 := by
+  simp
+
 theorem eq_empty_of_size_eq_zero (h : xs.size = 0) : xs = #[] := by
   cases xs
   simp_all
@@ -170,6 +173,7 @@ theorem getD_getElem? {xs : Array α} {i : Nat} {d : α} :
 
 @[simp] theorem getElem?_empty {i : Nat} : (#[] : Array α)[i]? = none := rfl
 
+set_option backward.isDefEq.respectTransparency false in
 theorem getElem_push_lt {xs : Array α} {x : α} {i : Nat} (h : i < xs.size) :
     have : i < (xs.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]
     (xs.push x)[i] = xs[i] := by
@@ -3482,6 +3486,21 @@ theorem foldl_eq_foldr_reverse {xs : Array α} {f : β → α → β} {b} :
 theorem foldr_eq_foldl_reverse {xs : Array α} {f : α → β → β} {b} :
     xs.foldr f b = xs.reverse.foldl (fun x y => f y x) b := by simp
 
+theorem foldl_eq_apply_foldr {xs : Array α} {f : α → α → α}
+    [Std.Associative f] [Std.LawfulRightIdentity f init] :
+    xs.foldl f x = f x (xs.foldr f init) := by
+  simp [← foldl_toList, ← foldr_toList, List.foldl_eq_apply_foldr]
+
+theorem foldr_eq_apply_foldl {xs : Array α} {f : α → α → α}
+    [Std.Associative f] [Std.LawfulLeftIdentity f init] :
+    xs.foldr f x = f (xs.foldl f init) x := by
+  simp [← foldl_toList, ← foldr_toList, List.foldr_eq_apply_foldl]
+
+theorem foldr_eq_foldl {xs : Array α} {f : α → α → α}
+    [Std.Associative f] [Std.LawfulIdentity f init] :
+    xs.foldr f init = xs.foldl f init := by
+  simp [foldl_eq_apply_foldr, Std.LawfulLeftIdentity.left_id]
+
 @[simp] theorem foldr_push_eq_append {as : Array α} {bs : Array β} {f : α → β} (w : start = as.size) :
     as.foldr (fun a xs => Array.push xs (f a)) bs start 0 = bs ++ (as.map f).reverse := by
   subst w
@@ -3974,6 +3993,7 @@ theorem all_filterMap {xs : Array α} {f : α → Option β} {p : β → Bool} :
   · simp only [Id.run_pure]
     rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))]
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp, grind =] theorem toList_modify {xs : Array α} {f : α → α} {i : Nat} :
     (xs.modify i f).toList = xs.toList.modify i f := by
   apply List.ext_getElem
@@ -4146,7 +4166,7 @@ variable [LawfulBEq α]
     (xs.replace a b)[i]? = if xs[i]? == some a then if a ∈ xs.take i then some a else some b else xs[i]? := by
   rcases xs with ⟨xs⟩
   simp only [List.replace_toArray, List.getElem?_toArray, List.getElem?_replace, take_eq_extract,
-    List.extract_toArray, List.extract_eq_drop_take, Nat.sub_zero, List.drop_zero, List.mem_toArray]
+    List.extract_toArray, List.extract_eq_take_drop, Nat.sub_zero, List.drop_zero, List.mem_toArray]
 
 theorem getElem?_replace_of_ne {xs : Array α} {i : Nat} (h : xs[i]? ≠ some a) :
     (xs.replace a b)[i]? = xs[i]? := by
@@ -4259,6 +4279,7 @@ private theorem getElem_ofFn_go {f : Fin n → α} {acc i k} (h : i ≤ n) (w₁
     · simp
       omega
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp] theorem getElem_ofFn {f : Fin n → α} {i : Nat} (h : i < (ofFn f).size) :
     (ofFn f)[i] = f ⟨i, size_ofFn (f := f) ▸ h⟩ := by
   unfold ofFn
@@ -4332,16 +4353,33 @@ def sum_eq_sum_toList := @sum_toList
 
 @[simp, grind =]
 theorem sum_append [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
-    [Std.LeftIdentity (α := α) (· + ·) 0] [Std.LawfulLeftIdentity (α := α) (· + ·) 0]
+    [Std.LawfulLeftIdentity (α := α) (· + ·) 0]
     {as₁ as₂ : Array α} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
   simp [← sum_toList, List.sum_append]
 
+@[simp, grind =]
+theorem sum_singleton [Add α] [Zero α] [Std.LawfulRightIdentity (· + ·) (0 : α)] {x : α} :
+    #[x].sum = x := by
+  simp [Array.sum_eq_foldr, Std.LawfulRightIdentity.right_id x]
+
+@[simp, grind =]
+theorem sum_push [Add α] [Zero α] [Std.Associative (α := α) (· + ·)]
+    [Std.LawfulIdentity (· + ·) (0 : α)] {xs : Array α} {x : α} :
+    (xs.push x).sum = xs.sum + x := by
+  simp [Array.sum_eq_foldr, Std.LawfulRightIdentity.right_id, Std.LawfulLeftIdentity.left_id,
+    ← Array.foldr_assoc]
+
 @[simp, grind =]
 theorem sum_reverse [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
     [Std.Commutative (α := α) (· + ·)]
     [Std.LawfulLeftIdentity (α := α) (· + ·) 0] (xs : Array α) : xs.reverse.sum = xs.sum := by
   simp [← sum_toList, List.sum_reverse]
 
+theorem sum_eq_foldl [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
+    [Std.LawfulIdentity (· + ·) (0 : α)] {xs : Array α} :
+    xs.sum = xs.foldl (init := 0) (· + ·) := by
+  simp [← sum_toList, List.sum_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) :
@@ -4490,11 +4528,13 @@ theorem getElem?_push_eq {xs : Array α} {x : α} : (xs.push x)[xs.size]? = some
   cases xs
   simp
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp, grind =] theorem finIdxOf?_toList [BEq α] {a : α} {xs : Array α} :
     xs.toList.finIdxOf? a = (xs.finIdxOf? a).map (Fin.cast (by simp)) := by
   cases xs
   simp
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp, grind =] theorem findFinIdx?_toList {p : α → Bool} {xs : Array α} :
     xs.toList.findFinIdx? p = (xs.findFinIdx? p).map (Fin.cast (by simp)) := by
   cases xs
@@ -4619,6 +4659,7 @@ namespace List
     as.toArray.unzip = Prod.map List.toArray List.toArray as.unzip := by
   ext1 <;> simp
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp, grind =] theorem firstM_toArray [Alternative m] {as : List α} {f : α → m β} :
     as.toArray.firstM f = as.firstM f := by
   unfold Array.firstM

src/Init/Data/Array/MinMax.lean

@@ -89,7 +89,7 @@ public theorem _root_.List.min_toArray [Min α] {l : List α} {h} :
     · rename_i x xs
       simp only [List.getElem_toArray, List.getElem_cons_zero, List.size_toArray, List.length_cons]
       rw [List.toArray_cons, foldl_eq_foldl_extract]
-      rw [← Array.foldl_toList, Array.toList_extract, List.extract_eq_drop_take]
+      rw [← Array.foldl_toList, Array.toList_extract, List.extract_eq_take_drop]
       simp [List.min]
 
 public theorem _root_.List.min_eq_min_toArray [Min α] {l : List α} {h} :
@@ -129,7 +129,7 @@ public theorem _root_.List.max_toArray [Max α] {l : List α} {h} :
     · rename_i x xs
       simp only [List.getElem_toArray, List.getElem_cons_zero, List.size_toArray, List.length_cons]
       rw [List.toArray_cons, foldl_eq_foldl_extract]
-      rw [← Array.foldl_toList, Array.toList_extract, List.extract_eq_drop_take]
+      rw [← Array.foldl_toList, Array.toList_extract, List.extract_eq_take_drop]
       simp [List.max]
 
 public theorem _root_.List.max_eq_max_toArray [Max α] {l : List α} {h} :

src/Init/Data/Array/Perm.lean

@@ -126,6 +126,14 @@ theorem swap_perm {xs : Array α} {i j : Nat} (h₁ : i < xs.size) (h₂ : j < x
   simp only [swap, perm_iff_toList_perm, toList_set]
   apply set_set_perm
 
+theorem Perm.pairwise_iff {R : α → α → Prop} (S : ∀ {x y}, R x y → R y x) {xs ys : Array α}
+    : ∀ _p : xs.Perm ys, xs.toList.Pairwise R ↔ ys.toList.Pairwise R := by
+  simpa only [perm_iff_toList_perm] using List.Perm.pairwise_iff S
+
+theorem Perm.pairwise {R : α → α → Prop} {xs ys : Array α} (hp : xs ~ ys)
+    (hR : xs.toList.Pairwise R) (hsymm : ∀ {x y}, R x y → R y x) :
+    ys.toList.Pairwise R := (hp.pairwise_iff hsymm).mp hR
+
 namespace Perm
 
 set_option linter.indexVariables false in
@@ -135,7 +143,7 @@ theorem extract {xs ys : Array α} (h : xs ~ ys) {lo hi : Nat}
   rcases xs with ⟨xs⟩
   rcases ys with ⟨ys⟩
   simp_all only [perm_iff_toList_perm, List.getElem?_toArray, List.extract_toArray,
-    List.extract_eq_drop_take]
+    List.extract_eq_take_drop]
   apply List.Perm.take_of_getElem? (w := fun i h => by simpa using whi (lo + i) (by omega))
   apply List.Perm.drop_of_getElem? (w := wlo)
   exact h

src/Init/Data/Array/Subarray.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Init.Data.Array.Basic
-public import Init.Data.Slice.Basic
+public import Init.Data.Slice.Operations
 
 public section
 
@@ -76,15 +76,17 @@ def Subarray.stop_le_array_size (xs : Subarray α) : xs.stop ≤ xs.array.size :
 
 namespace Subarray
 
-/--
-Computes the size of the subarray.
--/
-def size (s : Subarray α) : Nat :=
-  s.stop - s.start
+instance : SliceSize (Internal.SubarrayData α) where
+  size s := s.internalRepresentation.stop - s.internalRepresentation.start
+
+@[grind =, suggest_for Subarray.size]
+public theorem size_eq {xs : Subarray α} :
+    xs.size = xs.stop - xs.start := by
+  simp [Std.Slice.size, SliceSize.size, start, stop]
 
 theorem size_le_array_size {s : Subarray α} : s.size ≤ s.array.size := by
   let ⟨{array, start, stop, start_le_stop, stop_le_array_size}⟩ := s
-  simp only [size, ge_iff_le]
+  simp only [ge_iff_le, size_eq]
   apply Nat.le_trans (Nat.sub_le stop start)
   assumption
 

src/Init/Data/BitVec/Bitblast.lean

@@ -2192,6 +2192,7 @@ def uppcRec {w} (x : BitVec w) (s : Nat) (hs : s < w) : Bool :=
   | 0 => x.msb
   | i + 1 =>  x[w - 1 - i] || uppcRec x i (by omega)
 
+set_option backward.isDefEq.respectTransparency false in
 /-- The unsigned parallel prefix of `x` at `s` is `true` if and only if x interpreted
   as a natural number is greater or equal than `2 ^ (w - 1 - (s - 1))`. -/
 @[simp]

src/Init/Data/BitVec/Lemmas.lean

@@ -2581,6 +2581,19 @@ theorem msb_signExtend {x : BitVec w} :
   · simp [h, BitVec.msb, getMsbD_signExtend, show v - w = 0 by omega]
   · simp [h, BitVec.msb, getMsbD_signExtend, show ¬ (v - w = 0) by omega]
 
+/-- Sign-extending to `w + n` bits, extracting bits `[w - 1 + n..n]`, and setting width
+back to `w` is equivalent to arithmetic right shift by `n`, since both sides discard the `n`
+least significant bits and replicate the sign bit into the upper bits. -/
+@[simp]
+theorem signExtend_extractLsb_setWidth {x : BitVec w} {n : Nat} :
+    ((x.signExtend (w + n)).extractLsb (w - 1 + n) n).setWidth w = x.sshiftRight n := by
+  ext i hi
+  simp only [getElem_sshiftRight, getElem_setWidth, getLsbD_extract,
+    Nat.add_sub_cancel, show i ≤ w - 1 by omega, decide_true, getLsbD_signExtend,
+    Bool.true_and]
+  by_cases hni : n + i < w
+  <;> (simp [hni]; omega)
+
 /-- Sign extending to a width smaller than the starting width is a truncation. -/
 theorem signExtend_eq_setWidth_of_le (x : BitVec w) {v : Nat} (hv : v ≤ w) :
   x.signExtend v = x.setWidth v := by

src/Init/Data/Bool.lean

@@ -636,7 +636,7 @@ def boolPredToPred : Coe (α → Bool) (α  → Prop) where
 This should not be turned on globally as an instance because it degrades performance in Mathlib,
 but may be used locally.
 -/
-@[expose, instance_reducible] def boolRelToRel : Coe (α → α → Bool) (α → α → Prop) where
+@[expose, implicit_reducible] def boolRelToRel : Coe (α → α → Bool) (α → α → Prop) where
   coe r := fun a b => Eq (r a b) true
 
 /-! ### subtypes -/

src/Init/Data/ByteArray/Lemmas.lean

@@ -111,13 +111,13 @@ theorem getElem_eq_getElem_data {a : ByteArray} {i : Nat} {h : i < a.size} :
 theorem getElem_append_left {i : Nat} {a b : ByteArray} {h : i < (a ++ b).size}
     (hlt : i < a.size) : (a ++ b)[i] = a[i] := by
   simp only [getElem_eq_getElem_data, data_append]
-  rw [Array.getElem_append_left (by simpa)]
+  rw [Array.getElem_append_left (by simpa)]; rfl
 
 theorem getElem_append_right {i : Nat} {a b : ByteArray} {h : i < (a ++ b).size}
     (hle : a.size ≤ i) : (a ++ b)[i] = b[i - a.size]'(by simp_all; omega) := by
   simp only [getElem_eq_getElem_data, data_append]
   rw [Array.getElem_append_right (by simpa)]
-  simp
+  simp; rfl
 
 @[simp]
 theorem _root_.List.getElem_toByteArray {l : List UInt8} {i : Nat} {h : i < l.toByteArray.size} :
@@ -223,7 +223,7 @@ theorem getElem_extract_aux {xs : ByteArray} {start stop : Nat} (h : i < (xs.ext
 
 theorem getElem_extract {i : Nat} {b : ByteArray} {start stop : Nat}
     (h) : (b.extract start stop)[i]'h = b[start + i]'(getElem_extract_aux h) := by
-  simp [getElem_eq_getElem_data]
+  simp [getElem_eq_getElem_data]; rfl
 
 theorem extract_eq_extract_left {a : ByteArray} {i i' j : Nat} :
     a.extract i j = a.extract i' j ↔ min j a.size - i = min j a.size - i' := by
@@ -236,25 +236,25 @@ theorem extract_add_one {a : ByteArray} {i : Nat} (ha : i + 1 ≤ a.size) :
     omega
   · rename_i j hj hj'
     obtain rfl : j = 0 := by simpa using hj'
-    simp [ByteArray.getElem_eq_getElem_data]
+    simp [ByteArray.getElem_eq_getElem_data]; rfl
 
 theorem extract_add_two {a : ByteArray} {i : Nat} (ha : i + 2 ≤ a.size) :
     a.extract i (i + 2) = [a[i], a[i + 1]].toByteArray := by
   rw [extract_eq_extract_append_extract (i + 1) (by simp) (by omega),
     extract_add_one (by omega), extract_add_one (by omega)]
-  simp [← List.toByteArray_append]
+  simp [← List.toByteArray_append]; rfl
 
 theorem extract_add_three {a : ByteArray} {i : Nat} (ha : i + 3 ≤ a.size) :
     a.extract i (i + 3) = [a[i], a[i + 1], a[i + 2]].toByteArray := by
   rw [extract_eq_extract_append_extract (i + 1) (by simp) (by omega),
     extract_add_one (by omega), extract_add_two (by omega)]
-  simp [← List.toByteArray_append]
+  simp [← List.toByteArray_append]; rfl
 
 theorem extract_add_four {a : ByteArray} {i : Nat} (ha : i + 4 ≤ a.size) :
     a.extract i (i + 4) = [a[i], a[i + 1], a[i + 2], a[i + 3]].toByteArray := by
   rw [extract_eq_extract_append_extract (i + 1) (by simp) (by omega),
     extract_add_one (by omega), extract_add_three (by omega)]
-  simp [← List.toByteArray_append]
+  simp [← List.toByteArray_append]; rfl
 
 theorem append_assoc {a b c : ByteArray} : a ++ b ++ c = a ++ (b ++ c) := by
   ext1

src/Init/Data/Char/Lemmas.lean

@@ -50,7 +50,7 @@ instance ltTrans : Trans (· < · : Char → Char → Prop) (· < ·) (· < ·)
   trans := Char.lt_trans
 
 -- This instance is useful while setting up instances for `String`.
-@[instance_reducible]
+@[implicit_reducible]
 def notLTTrans : Trans (¬ · < · : Char → Char → Prop) (¬ · < ·) (¬ · < ·) where
   trans h₁ h₂ := by simpa using Char.le_trans (by simpa using h₂) (by simpa using h₁)
 

src/Init/Data/Fin/Fold.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: François G. Dorais
 -/
 module
-
 prelude
 public import Init.Control.Lawful.Basic
 public import Init.Ext
@@ -13,7 +12,7 @@ import Init.Data.Nat.Lemmas
 import Init.Omega
 import Init.TacticsExtra
 import Init.WFTactics
-
+import Init.Hints
 public section
 
 namespace Fin

src/Init/Data/Fin/Iterate.lean

@@ -4,14 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joe Hendrix
 -/
 module
-
 prelude
 public import Init.Data.Fin.Basic
 import Init.PropLemmas
 import Init.WFTactics
-
+import Init.Hints
 public section
-
 namespace Fin
 
 /--
@@ -71,7 +69,7 @@ private theorem hIterateFrom_elim {P : Nat → Sort _}(Q : ∀(i : Nat), P i →
     have g : ¬ (i < n) := by simp at p; simp [p]
     have r : Q n (_root_.cast (congrArg P p) s) :=
       @Eq.rec Nat i (fun k eq => Q k (_root_.cast (congrArg P eq) s)) init n p
-    simp only [g, r, dite_false]
+    simp only [g, dite_false]; exact r
   | succ j inv =>
     unfold hIterateFrom
     have d : Nat.succ i + j = n := by simp [Nat.succ_add]; exact p

src/Init/Data/Fin/Lemmas.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Leonardo de Moura
 -/
 module
-
 prelude
 public import Init.Ext
 public import Init.Data.Nat.Div.Basic
@@ -15,7 +14,7 @@ import Init.Data.Nat.Lemmas
 import Init.Data.Nat.Linear
 import Init.Omega
 import Init.TacticsExtra
-
+import Init.Hints
 @[expose] public section
 
 open Std
@@ -124,7 +123,7 @@ For example, for `x : Fin k` and `n : Nat`,
 it causes `x < n` to be elaborated as `x < ↑n` rather than `↑x < n`,
 silently introducing wraparound arithmetic.
 -/
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 def instNatCast (n : Nat) [NeZero n] : NatCast (Fin n) where
   natCast a := Fin.ofNat n a
 
@@ -146,7 +145,7 @@ This is not a global instance, but may be activated locally via `open Fin.IntCas
 
 See the doc-string for `Fin.NatCast.instNatCast` for more details.
 -/
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 def instIntCast (n : Nat) [NeZero n] : IntCast (Fin n) where
   intCast := Fin.intCast
 
@@ -998,7 +997,7 @@ For the induction:
 
 @[simp, grind =] theorem reverseInduction_last {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ} :
     (reverseInduction zero succ (Fin.last n) : motive (Fin.last n)) = zero := by
-  rw [reverseInduction, reverseInduction.go]; simp
+  rw [reverseInduction, reverseInduction.go]; simp; rfl
 
 private theorem reverseInduction_castSucc_aux {n : Nat} {motive : Fin (n + 1) → Sort _} {succ}
     (i : Fin n) (j : Nat) (h) (h2 : i.1 < j) (zero : motive ⟨j, h⟩) :
@@ -1009,9 +1008,9 @@ private theorem reverseInduction_castSucc_aux {n : Nat} {motive : Fin (n + 1)
   | succ j ih =>
     rw [reverseInduction.go, dif_neg (by exact Nat.ne_of_lt h2)]
     by_cases hij : i = j
-    · subst hij; simp [reverseInduction.go]
-    dsimp only
-    rw [ih _ _ (by omega), eq_comm, reverseInduction.go, dif_neg (by change i.1 + 1 ≠ _; omega)]
+    · subst hij; simp [reverseInduction.go]; rfl
+    · dsimp only
+      rw [ih _ _ (by omega), eq_comm, reverseInduction.go, dif_neg (by change i.1 + 1 ≠ _; omega)]
 
 @[simp, grind =] theorem reverseInduction_castSucc {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ}
     (i : Fin n) : reverseInduction (motive := motive) zero succ (castSucc i) =

src/Init/Data/Hashable.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.String.PosRaw
+import Init.Data.Array.Basic
 public import Init.Data.UInt.Basic
 
 public section
@@ -15,9 +15,6 @@ universe u
 instance : Hashable Nat where
   hash n := UInt64.ofNat n
 
-instance : Hashable String.Pos.Raw where
-  hash p := UInt64.ofNat p.byteIdx
-
 instance [Hashable α] [Hashable β] : Hashable (α × β) where
   hash | (a, b) => mixHash (hash a) (hash b)
 

src/Init/Data/Iterators/Basic.lean

@@ -315,7 +315,7 @@ of another state. Having this proof bundled up with the step is important for te
 See `IterM.Step` and `Iter.Step` for the concrete choice of the plausibility predicate.
 -/
 @[expose]
-def PlausibleIterStep (IsPlausibleStep : IterStep α β → Prop) := Subtype IsPlausibleStep
+abbrev PlausibleIterStep (IsPlausibleStep : IterStep α β → Prop) := Subtype IsPlausibleStep
 
 /--
 Match pattern for the `yield` case. See also `IterStep.yield`.
@@ -379,6 +379,8 @@ class Iterator (α : Type w) (m : Type w → Type w') (β : outParam (Type w)) w
   -/
   step : (it : IterM (α := α) m β) → m (Shrink <| PlausibleIterStep <| IsPlausibleStep it)
 
+attribute [reducible] Iterator.IsPlausibleStep
+
 section Monadic
 
 /-- The constructor has been renamed. -/
@@ -424,7 +426,6 @@ theorem IterM.toIter_mk {α β} {it : α} :
 Asserts that certain step is plausibly the successor of a given iterator. What "plausible" means
 is up to the `Iterator` instance but it should be strong enough to allow termination proofs.
 -/
-@[expose]
 abbrev IterM.IsPlausibleStep {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] :
     IterM (α := α) m β → IterStep (IterM (α := α) m β) β → Prop :=
   Iterator.IsPlausibleStep (α := α) (m := m)
@@ -493,7 +494,7 @@ Asserts that certain step is plausibly the successor of a given iterator. What "
 is up to the `Iterator` instance but it should be strong enough to allow termination proofs.
 -/
 @[expose]
-def Iter.IsPlausibleStep {α : Type w} {β : Type w} [Iterator α Id β]
+abbrev Iter.IsPlausibleStep {α : Type w} {β : Type w} [Iterator α Id β]
     (it : Iter (α := α) β) (step : IterStep (Iter (α := α) β) β) : Prop :=
   it.toIterM.IsPlausibleStep (step.mapIterator Iter.toIterM)
 
@@ -549,7 +550,7 @@ The type of the step object returned by `Iter.step`, containing an `IterStep`
 and a proof that this is a plausible step for the given iterator.
 -/
 @[expose]
-def Iter.Step {α : Type w} {β : Type w} [Iterator α Id β] (it : Iter (α := α) β) :=
+abbrev Iter.Step {α : Type w} {β : Type w} [Iterator α Id β] (it : Iter (α := α) β) :=
   PlausibleIterStep (Iter.IsPlausibleStep it)
 
 /--

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

@@ -765,6 +765,7 @@ theorem Iter.anyM_eq_anyM_mapM_pure {α β : Type} {m : Type → Type w'} [Itera
   rw [forIn_eq_match_step, IterM.forIn_eq_match_step, bind_assoc, step_mapM]
   cases it.step using PlausibleIterStep.casesOn
   · rename_i out _
+    simp only
     simp only [bind_assoc, pure_bind, map_eq_pure_bind, Shrink.inflate_deflate,
       liftM, monadLift]
     have {x : m Bool} : x = MonadAttach.attach (pure out) >>= (fun _ => x) := by
@@ -777,7 +778,7 @@ theorem Iter.anyM_eq_anyM_mapM_pure {α β : Type} {m : Type → Type w'} [Itera
     apply bind_congr; intro px
     split
     · simp
-    · simp [ihy ‹_›]
+    · simp [ihy ‹_›, monadLift]
   · simp [ihs ‹_›]
   · simp
 

src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean

@@ -232,6 +232,7 @@ public theorem Iter.toArray_flatMapM {α α₂ β γ : Type w} {m : Type w → T
     (it₁.flatMapM f).toArray = Array.flatten <$> (it₁.mapM fun b => do (← f b).toArray).toArray := by
   simp [flatMapM, toArray_flatMapAfterM]
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem Iter.toList_flatMapAfter {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
     [Finite α Id] [Finite α₂ Id]
     {f : β → Iter (α := α₂) γ} {it₁ : Iter (α := α) β} {it₂ : Option (Iter (α := α₂) γ)} :
@@ -242,6 +243,7 @@ public theorem Iter.toList_flatMapAfter {α α₂ β γ : Type w} [Iterator α I
   simp only [flatMapAfter, Iter.toList, toIterM_toIter, IterM.toList_flatMapAfter]
   cases it₂ <;> simp [map, IterM.toList_map_eq_toList_mapM, - IterM.toList_map]
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem Iter.toArray_flatMapAfter {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
     [Finite α Id] [Finite α₂ Id]
     {f : β → Iter (α := α₂) γ} {it₁ : Iter (α := α) β} {it₂ : Option (Iter (α := α₂) γ)} :

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

@@ -182,11 +182,12 @@ theorem IterM.step_filterMap [Monad m] [LawfulMonad m] {f : β → Option β'} :
       pure <| .deflate <| .skip (it'.filterMap f) (.skip h)
     | .done h =>
       pure <| .deflate <| .done (.done h)) := by
-  simp only [IterM.filterMap, step_filterMapWithPostcondition, pure]
+  simp only [IterM.filterMap]
+  simp only [step_filterMapWithPostcondition, PostconditionT.operation_pure]
   apply bind_congr
   intro step
   split
-  · simp only [PostconditionT.pure, PlausibleIterStep.skip, PlausibleIterStep.yield, pure_bind]
+  · simp only [PlausibleIterStep.skip, PlausibleIterStep.yield, pure_bind]
     split <;> split <;> simp_all
   · simp
   · simp
@@ -361,8 +362,8 @@ theorem IterM.toList_map_eq_toList_mapM {α β γ : Type w}
       bind_map_left]
     conv => rhs; rhs; ext a; rw [← pure_bind (x := a.val) (f := fun _ => _ <$> _)]
     simp only [← bind_assoc, bind_pure_comp, WeaklyLawfulMonadAttach.map_attach]
-    simp [ihy ‹_›]
-  · simp [ihs ‹_›]
+    simpa using ihy ‹_›
+  · simpa using ihs ‹_›
   · simp
 
 theorem IterM.toList_map_eq_toList_filterMapM {α β γ : Type w} {m : Type w → Type w'}
@@ -373,6 +374,7 @@ theorem IterM.toList_map_eq_toList_filterMapM {α β γ : Type w} {m : Type w
   simp [toList_map_eq_toList_mapM, toList_mapM_eq_toList_filterMapM]
   congr <;> simp
 
+set_option backward.whnf.reducibleClassField false in
 /--
 Variant of `toList_filterMapWithPostcondition_filterMapWithPostcondition` that is intended to be
 used with the `apply` tactic. Because neither the LHS nor the RHS determine all implicit parameters,
@@ -600,6 +602,7 @@ theorem IterM.toList_map_mapM {α β γ δ : Type w}
     toList_filterMapM_mapM]
   congr <;> simp
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem IterM.toList_filterMapWithPostcondition {α β γ : Type w} {m : Type w → Type w'}
     [Monad m] [LawfulMonad m]
@@ -623,6 +626,7 @@ theorem IterM.toList_filterMapWithPostcondition {α β γ : Type w} {m : Type w
   · simp [ihs ‹_›, heq]
   · simp [heq]
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem IterM.toList_mapWithPostcondition {α β γ : Type w} {m : Type w → Type w'}
     [Monad m] [LawfulMonad m] [Iterator α Id β] [Finite α Id]
@@ -643,6 +647,7 @@ theorem IterM.toList_mapWithPostcondition {α β γ : Type w} {m : Type w → Ty
   · simp [ihs ‹_›, heq]
   · simp [heq]
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem IterM.toList_filterMapM {α β γ : Type w} {m : Type w → Type w'}
     [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m]
@@ -652,6 +657,7 @@ theorem IterM.toList_filterMapM {α β γ : Type w} {m : Type w → Type w'}
   simp [toList_filterMapM_eq_toList_filterMapWithPostcondition, toList_filterMapWithPostcondition,
     PostconditionT.attachLift, PostconditionT.run_eq_map, WeaklyLawfulMonadAttach.map_attach]
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem IterM.toList_mapM {α β γ : Type w} {m : Type w → Type w'}
     [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m]
@@ -1297,6 +1303,7 @@ theorem IterM.forIn_filterMap
   rw [filterMap, forIn_filterMapWithPostcondition]
   simp [PostconditionT.run_eq_map]
 
+set_option backward.isDefEq.respectTransparency false in
 theorem IterM.forIn_mapWithPostcondition
     [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
     [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o]

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

@@ -36,7 +36,7 @@ theorem IterM.step_flattenAfter {α α₂ β : Type w} {m : Type w → Type w'}
   cases it₂
   all_goals
   · apply bind_congr; intro step
-    cases step.inflate using PlausibleIterStep.casesOn <;> simp [IterM.flattenAfter]
+    cases step.inflate using PlausibleIterStep.casesOn <;> simp [IterM.flattenAfter] <;> rfl
 
 namespace Iterators.Types
 

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

@@ -29,7 +29,7 @@ theorem IterM.step_uLift [Iterator α m β] [Monad n] {it : IterM (α := α) m
       | .done h => return .deflate (.done ⟨_, h, rfl⟩)) := by
   simp only [IterM.step, Iterator.step, IterM.uLift]
   apply bind_congr; intro step
-  split <;> simp [Types.ULiftIterator.Monadic.modifyStep, *]
+  split <;> simp [Types.ULiftIterator.Monadic.modifyStep, *] <;> rfl
 
 @[simp]
 theorem IterM.toList_uLift [Iterator α m β] [Monad m] [Monad n] {it : IterM (α := α) m β}

src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean

@@ -42,7 +42,7 @@ theorem Iter.step_uLift [Iterator α Id β] {it : Iter (α := α) β} :
 theorem Iter.toList_uLift [Iterator α Id β] {it : Iter (α := α) β}
     [Finite α Id] :
     it.uLift.toList = it.toList.map ULift.up := by
-  simp only [monadLift, uLift_eq_toIter_uLift_toIterM, IterM.toList_toIter]
+  simp only [uLift_eq_toIter_uLift_toIterM, IterM.toList_toIter]
   rw [IterM.toList_uLift]
   simp [monadLift, Iter.toList_eq_toList_toIterM]
 
@@ -63,7 +63,7 @@ theorem Iter.toArray_uLift [Iterator α Id β] {it : Iter (α := α) β}
 theorem Iter.length_uLift [Iterator α Id β] {it : Iter (α := α) β}
     [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] :
     it.uLift.length = it.length := by
-  simp only [monadLift, uLift_eq_toIter_uLift_toIterM, length_eq_length_toIterM, toIterM_toIter]
+  simp only [uLift_eq_toIter_uLift_toIterM, length_eq_length_toIterM, toIterM_toIter]
   rw [IterM.length_uLift]
   simp [monadLift]
 

src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean

@@ -58,8 +58,7 @@ theorem Iter.forIn_eq {α β : Type w} [Iterator α Id β] [Finite α Id]
     forIn' ita b f = forIn' itb b' g := by
   subst_eqs
   simp only [← funext_iff] at h
-  rw [← h]
-  rfl
+  rw [← h]; rfl
 
 @[congr] theorem Iter.forIn_congr {α β : Type w} {m : Type w → Type w'} [Monad m]
     [Iterator α Id β] [Finite α Id] [IteratorLoop α Id m]
@@ -276,8 +275,7 @@ theorem Iter.forIn'_eq_forIn'_toList {α β : Type w} [Iterator α Id β]
     {f : (out : β) → _ → γ → m (ForInStep γ)} :
     letI : ForIn' m (Iter (α := α) β) β _ := Iter.instForIn'
     ForIn'.forIn' it init f = ForIn'.forIn' it.toList init (fun out h acc => f out (Iter.mem_toList_iff_isPlausibleIndirectOutput.mp h) acc) := by
-  simp only [forIn'_toList]
-  congr
+  simp only [forIn'_toList]; rfl
 
 theorem Iter.forIn'_eq_forIn'_toArray {α β : Type w} [Iterator α Id β]
     [Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m]
@@ -287,8 +285,7 @@ theorem Iter.forIn'_eq_forIn'_toArray {α β : Type w} [Iterator α Id β]
     {f : (out : β) → _ → γ → m (ForInStep γ)} :
     letI : ForIn' m (Iter (α := α) β) β _ := Iter.instForIn'
     ForIn'.forIn' it init f = ForIn'.forIn' it.toArray init (fun out h acc => f out (Iter.mem_toArray_iff_isPlausibleIndirectOutput.mp h) acc) := by
-  simp only [forIn'_toArray]
-  congr
+  simp only [forIn'_toArray]; rfl
 
 theorem Iter.forIn_toList {α β : Type w} [Iterator α Id β]
     [Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m]
@@ -398,7 +395,7 @@ theorem Iter.fold_eq_fold_toIterM {α β : Type w} {γ : Type w} [Iterator α Id
     [Finite α Id] [IteratorLoop α Id Id]
     {f : γ → β → γ} {init : γ} {it : Iter (α := α) β} :
     it.fold (init := init) f = (it.toIterM.fold (init := init) f).run := by
-  rw [fold_eq_foldM, foldM_eq_foldM_toIterM, IterM.fold_eq_foldM]
+  rw [fold_eq_foldM, foldM_eq_foldM_toIterM, IterM.fold_eq_foldM]; rfl
 
 @[simp]
 theorem Iter.forIn_pure_yield_eq_fold {α β : Type w} {γ : Type x} [Iterator α Id β]

src/Init/Data/Iterators/Producers/Monadic/List.lean

@@ -70,7 +70,7 @@ private def ListIterator.instFinitenessRelation [Pure m] :
   subrelation {it it'} h := by
     simp_wf
     obtain ⟨step, h, h'⟩ := h
-    cases step <;> simp_all [IterStep.successor, IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+    cases step <;> simp_all [IterStep.successor, IterM.IsPlausibleStep, Iterator.IsPlausibleStep, instIterator]
 
 instance ListIterator.instFinite [Pure m] : Finite (ListIterator α) m :=
   by exact Finite.of_finitenessRelation ListIterator.instFinitenessRelation

src/Init/Data/Iterators/ToIterator.lean

@@ -32,14 +32,14 @@ def ToIterator.iter [ToIterator γ Id α β] (x : γ) : Iter (α := α) β :=
   ToIterator.iterM x |>.toIter
 
 /-- Creates a monadic `ToIterator` instance. -/
-@[always_inline, inline, expose]
+@[always_inline, inline, expose, instance_reducible]
 def ToIterator.ofM (α : Type w)
     (iterM : γ → IterM (α := α) m β) :
     ToIterator γ m α β where
   iterMInternal x := iterM x
 
 /-- Creates a pure `ToIterator` instance. -/
-@[always_inline, inline, expose]
+@[always_inline, inline, expose, instance_reducible]
 def ToIterator.of (α : Type w)
     (iter : γ → Iter (α := α) β) :
     ToIterator γ Id α β where

src/Init/Data/List.lean

@@ -35,3 +35,5 @@ public import Init.Data.List.OfFn
 public import Init.Data.List.FinRange
 public import Init.Data.List.Lex
 public import Init.Data.List.Range
+public import Init.Data.List.Scan
+public import Init.Data.List.ControlImpl

src/Init/Data/List/Basic.lean

@@ -955,9 +955,13 @@ Examples:
 abbrev extract (l : List α) (start : Nat := 0) (stop : Nat := l.length) : List α :=
   (l.drop start).take (stop - start)
 
-@[simp] theorem extract_eq_drop_take {l : List α} {start stop : Nat} :
+@[simp] theorem extract_eq_take_drop {l : List α} {start stop : Nat} :
     l.extract start stop = (l.drop start).take (stop - start) := rfl
 
+set_option linter.missingDocs false in
+@[deprecated extract_eq_take_drop (since := "2026-02-06")]
+def extract_eq_drop_take := @extract_eq_take_drop
+
 /-! ### takeWhile -/
 
 /--
@@ -2182,7 +2186,7 @@ Examples:
 * `List.intercalate sep [a, b] = a ++ sep ++ b`
 * `List.intercalate sep [a, b, c] = a ++ sep ++ b ++ sep ++ c`
 -/
-def intercalate (sep : List α) (xs : List (List α)) : List α :=
+noncomputable def intercalate (sep : List α) (xs : List (List α)) : List α :=
   (intersperse sep xs).flatten
 
 /-! ### eraseDupsBy -/

src/Init/Data/List/Control.lean

@@ -219,9 +219,9 @@ def filterMapM {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f
 Applies a monadic function that returns a list to each element of a list, from left to right, and
 concatenates the resulting lists.
 -/
-@[inline, expose]
-def flatMapM {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (List β)) (as : List α) : m (List β) :=
-  let rec @[specialize] loop
+@[expose]
+noncomputable def flatMapM {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (List β)) (as : List α) : m (List β) :=
+  let rec loop
     | [],     bs => pure bs.reverse.flatten
     | a :: as, bs => do
       let bs' ← f a

src/Init/Data/List/ControlImpl.lean

@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.List.Control
+public import Init.Data.List.Impl
+
+public section
+
+namespace List
+
+/--
+Applies a monadic function that returns a list to each element of a list, from left to right, and
+concatenates the resulting lists.
+-/
+@[inline, expose]
+def flatMapMTR {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (List β)) (as : List α) : m (List β) :=
+  let rec @[specialize] loop
+    | [],     bs => pure bs.reverse.flatten
+    | a :: as, bs => do
+      let bs' ← f a
+      loop as (bs' :: bs)
+  loop as []
+
+@[csimp] theorem flatMapM_eq_flatMapMTR : @flatMapM = @flatMapMTR := by
+  funext m _ α β f l
+  simp only [flatMapM, flatMapMTR]
+  generalize [] = m
+  fun_induction flatMapM.loop <;> simp_all [flatMapMTR.loop]
+
+end List

src/Init/Data/List/Count.lean

@@ -132,7 +132,9 @@ theorem boole_getElem_le_countP {p : α → Bool} {l : List α} {i : Nat} (h : i
   | nil => simp at h
   | cons x l ih =>
     cases i with
-    | zero => simp [countP_cons]
+    | zero =>
+      set_option backward.isDefEq.respectTransparency false in
+      simp [countP_cons]
     | succ i =>
       simp only [length_cons, add_one_lt_add_one_iff] at h
       simp only [getElem_cons_succ, countP_cons]
@@ -263,7 +265,9 @@ theorem count_eq_length_filter {a : α} {l : List α} : count a l = (filter (·
 theorem count_tail : ∀ {l : List α} {a : α},
       l.tail.count a = l.count a - if l.head? == some a then 1 else 0
   | [], a => by simp
-  | _ :: _, a => by simp [count_cons]
+  | _ :: _, a => by
+    set_option backward.isDefEq.respectTransparency false in
+    simp [count_cons]
 
 theorem count_le_length {a : α} {l : List α} : count a l ≤ l.length := countP_le_length
 

src/Init/Data/List/Find.lean

@@ -97,6 +97,12 @@ theorem findSome?_eq_some_iff {f : α → Option β} {l : List α} {b : β} :
           obtain ⟨⟨rfl, rfl⟩, rfl⟩ := h₁
           exact ⟨l₁, a, l₂, rfl, h₂, fun a' w => h₃ a' (mem_cons_of_mem p w)⟩
 
+theorem isSome_findSome? {xs : List α} {f : α → Option β} :
+    (xs.findSome? f).isSome = xs.any (f · |>.isSome) := by
+  rw [Bool.eq_iff_iff]
+  simp only [Option.isSome_iff_ne_none, ne_eq, findSome?_eq_none_iff, Classical.not_forall]
+  simp [← Option.isSome_iff_ne_none]
+
 @[simp, grind =] theorem findSome?_guard {l : List α} : findSome? (Option.guard p) l = find? p l := by
   induction l with
   | nil => simp
@@ -270,6 +276,11 @@ theorem find?_eq_some_iff_append :
           cases h₁
           simp
 
+theorem isSome_find? {xs : List α} {f : α → Bool} :
+    (xs.find? f).isSome = xs.any (f ·) := by
+  rw [Bool.eq_iff_iff]
+  simp [Option.isSome_iff_ne_none, ne_eq, find?_eq_none, Classical.not_forall]
+
 @[simp]
 theorem find?_cons_eq_some : (a :: xs).find? p = some b ↔ (p a ∧ a = b) ∨ (!p a ∧ xs.find? p = some b) := by
   rw [find?_cons]
@@ -654,6 +665,7 @@ theorem lt_findIdx_of_not {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs
   simp only [Nat.not_lt] at f
   exact absurd (@findIdx_getElem _ p xs (Nat.lt_of_le_of_lt f h)) (h2 (xs.findIdx p) f)
 
+set_option backward.isDefEq.respectTransparency false in
 /-- `xs.findIdx p = i` iff `p xs[i]` and `¬ p xs [j]` for all `j < i`. -/
 theorem findIdx_eq {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs.length) :
     xs.findIdx p = i ↔ p xs[i] ∧ ∀ j (hji : j < i), p (xs[j]'(Nat.lt_trans hji h)) = false := by
@@ -1038,7 +1050,7 @@ theorem findFinIdx?_append {xs ys : List α} {p : α → Bool} :
 
 @[simp, grind =] theorem findFinIdx?_singleton {a : α} {p : α → Bool} :
     [a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by
-  simp [findFinIdx?_cons, findFinIdx?_nil]
+  simp [findFinIdx?_cons, findFinIdx?_nil]; rfl
 
 @[simp, grind =] theorem findFinIdx?_eq_none_iff {l : List α} {p : α → Bool} :
     l.findFinIdx? p = none ↔ ∀ x ∈ l, ¬ p x := by
@@ -1080,6 +1092,7 @@ theorem isNone_findFinIdx? {l : List α} {p : α → Bool} :
   induction l with
   | nil => simp
   | cons a l ih =>
+    set_option backward.isDefEq.respectTransparency false in
     simp [hf, findFinIdx?_cons]
     split <;> simp [ih, Function.comp_def]
 

src/Init/Data/List/Lemmas.lean

@@ -1838,6 +1838,11 @@ theorem sum_append [Add α] [Zero α] [Std.LawfulLeftIdentity (α := α) (· +
     [Std.Associative (α := α) (· + ·)] {l₁ l₂ : List α} : (l₁ ++ l₂).sum = l₁.sum + l₂.sum := by
   induction l₁ generalizing l₂ <;> simp_all [Std.Associative.assoc, Std.LawfulLeftIdentity.left_id]
 
+@[simp, grind =]
+theorem sum_singleton [Add α] [Zero α] [Std.LawfulRightIdentity (· + ·) (0 : α)] {x : α} :
+    [x].sum = x := by
+  simp [List.sum_eq_foldr, Std.LawfulRightIdentity.right_id x]
+
 @[simp, grind =]
 theorem sum_reverse [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
     [Std.Commutative (α := α) (· + ·)]
@@ -2727,6 +2732,31 @@ theorem foldr_assoc {op : α → α → α} [ha : Std.Associative op] :
     simp only [foldr_cons, ha.assoc]
     rw [foldr_assoc]
 
+theorem foldl_eq_apply_foldr {xs : List α} {f : α → α → α}
+    [Std.Associative f] [Std.LawfulRightIdentity f init] :
+    xs.foldl f x = f x (xs.foldr f init) := by
+  induction xs generalizing x
+  · simp [Std.LawfulRightIdentity.right_id]
+  · simp [foldl_assoc, *]
+
+theorem foldr_eq_apply_foldl {xs : List α} {f : α → α → α}
+    [Std.Associative f] [Std.LawfulLeftIdentity f init] :
+    xs.foldr f x = f (xs.foldl f init) x := by
+  have : Std.Associative (fun x y => f y x) := ⟨by simp [Std.Associative.assoc]⟩
+  have : Std.RightIdentity (fun x y => f y x) init := ⟨⟩
+  have : Std.LawfulRightIdentity (fun x y => f y x) init := ⟨by simp [Std.LawfulLeftIdentity.left_id]⟩
+  rw [← List.reverse_reverse (as := xs), foldr_reverse, foldl_eq_apply_foldr, foldl_reverse]
+
+theorem foldr_eq_foldl {xs : List α} {f : α → α → α}
+    [Std.Associative f] [Std.LawfulIdentity f init] :
+    xs.foldr f init = xs.foldl f init := by
+  simp [foldl_eq_apply_foldr, Std.LawfulLeftIdentity.left_id]
+
+theorem sum_eq_foldl [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
+    [Std.LawfulIdentity (· + ·) (0 : α)] {xs : List α} :
+    xs.sum = xs.foldl (init := 0) (· + ·) := by
+  simp [sum_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
@@ -3648,6 +3678,40 @@ theorem eraseDups_append [BEq α] [LawfulBEq α] {as bs : List α} :
     simp [removeAll_cons]
 termination_by as.length
 
+/-- Loop invariant for `eraseDupsBy.loop`: membership in the result equals
+membership in the remaining list or the accumulator. -/
+private theorem mem_eraseDupsBy_loop [BEq α] [LawfulBEq α] {a : α} {l acc : List α} :
+    a ∈ eraseDupsBy.loop (· == ·) l acc ↔ a ∈ l ∨ a ∈ acc := by
+  induction l generalizing acc with
+  | nil => simp [eraseDupsBy.loop]
+  | cons x xs ih =>
+    unfold eraseDupsBy.loop; split
+    · next h =>
+      rw [ih]; simp only [mem_cons]
+      apply Iff.intro (fun
+        | .inl hxs => Or.inl (Or.inr hxs)
+        | .inr hacc => Or.inr hacc) (fun
+        | .inl (.inl rfl) =>
+            have ⟨y, hy, heq⟩ := any_eq_true.mp h
+            .inr (LawfulBEq.eq_of_beq heq ▸ hy)
+        | .inl (.inr hxs) => .inl hxs
+        | .inr hacc => .inr hacc)
+    · rw [ih]; simp only [mem_cons]
+      apply Iff.intro (fun
+        | .inl hxs => Or.inl (Or.inr hxs)
+        | .inr (.inl rfl) => Or.inl (Or.inl rfl)
+        | .inr (.inr hacc) => Or.inr hacc) (fun
+        | .inl (.inl rfl) => Or.inr (Or.inl rfl)
+        | .inl (.inr hxs) => .inl hxs
+        | .inr hacc => Or.inr (Or.inr hacc))
+
+/-- Membership is preserved by `eraseDups`: an element is in the deduplicated list
+iff it was in the original list. -/
+@[simp]
+theorem mem_eraseDups [BEq α] [LawfulBEq α] {a : α} {l : List α} :
+    a ∈ l.eraseDups ↔ a ∈ l := by
+  simp only [eraseDups, eraseDupsBy, mem_eraseDupsBy_loop, not_mem_nil, or_false]
+
 /-! ### Legacy lemmas about `get`, `get?`, and `get!`.
 
 Hopefully these should not be needed, in favour of lemmas about `xs[i]`, `xs[i]?`, and `xs[i]!`,
@@ -3679,11 +3743,13 @@ theorem get_of_eq {l l' : List α} (h : l = l') (i : Fin l.length) :
 theorem getElem!_nil [Inhabited α] {n : Nat} : ([] : List α)[n]! = default := rfl
 
 theorem getElem!_cons_zero [Inhabited α] {l : List α} : (a::l)[0]! = a := by
-  rw [getElem!_pos] <;> simp
+  rw [getElem!_pos]; rfl; simp
 
 theorem getElem!_cons_succ [Inhabited α] {l : List α} : (a::l)[i+1]! = l[i]! := by
   by_cases h : i < l.length
-  · rw [getElem!_pos, getElem!_pos] <;> simp_all [Nat.succ_lt_succ_iff]
+  · rw [getElem!_pos, getElem!_pos]
+    · rfl
+    · simp; apply Nat.succ_lt_succ; assumption
   · rw [getElem!_neg, getElem!_neg] <;> simp_all [Nat.succ_lt_succ_iff]
 
 theorem getElem!_of_getElem? [Inhabited α] : ∀ {l : List α} {i : Nat}, l[i]? = some a → l[i]! = a

src/Init/Data/List/MinMax.lean

@@ -180,6 +180,21 @@ theorem min_singleton [Min α] {x : α} :
     [x].min (cons_ne_nil _ _) = x := by
   (rfl)
 
+theorem min_cons_cons [Min α] {a b : α} {l : List α} :
+    (a :: b :: l).min (by simp) = (min a b :: l).min (by simp) :=
+  (rfl)
+
+theorem min_cons [Min α] [Std.Associative (α := α) Min.min] {a : α} {l : List α} {h} :
+    (a :: l).min h = l.min?.elim a (min a ·) :=
+  match l with
+  | nil => by simp
+  | cons hd tl =>
+      Option.some.inj ((min?_cons' (x := a) (xs := hd :: tl)).symm.trans min?_cons)
+
+@[simp]
+theorem min_cons_cons_nil [Min α] {a b : α} : [a, b].min (by simp) = min a b := by
+  simp [min_cons_cons]
+
 theorem min?_eq_some_min [Min α] : {l : List α} → (hl : l ≠ []) →
     l.min? = some (l.min hl)
   | a::as, _ => by simp [List.min, List.min?_cons']
@@ -388,6 +403,21 @@ theorem max_singleton [Max α] {x : α} :
     [x].max (cons_ne_nil _ _) = x := by
   (rfl)
 
+theorem max_cons_cons [Max α] {a b : α} {l : List α} :
+    (a :: b :: l).max (by simp) = (max a b :: l).max (by simp) :=
+  (rfl)
+
+theorem max_cons [Max α] [Std.Associative (α := α) Max.max] {a : α} {l : List α} {h} :
+    (a :: l).max h = l.max?.elim a (max a ·) :=
+  match l with
+  | nil => by simp
+  | cons hd tl =>
+      Option.some.inj ((max?_cons' (x := a) (xs := hd :: tl)).symm.trans max?_cons)
+
+@[simp]
+theorem max_cons_cons_nil [Max α] {a b : α} : [a, b].max (by simp) = max a b := by
+  simp [max_cons_cons]
+
 theorem max?_eq_some_max [Max α] : {l : List α} → (hl : l ≠ []) →
     l.max? = some (l.max hl)
   | a::as, _ => by simp [List.max, List.max?_cons']

src/Init/Data/List/MinMaxIdx.lean

@@ -358,11 +358,19 @@ private theorem combineMinIdxOn_lt [LE β] [DecidableLE β]
   simp only [combineMinIdxOn]
   split <;> (simp; omega)
 
+private theorem combineMinIdxOn_lt' [LE β] [DecidableLE β]
+    (f : α → β) {xs ys : List α} (zs : List α) {i j : Nat} (hi : i < xs.length) (hj : j < ys.length)
+    (h : zs = xs ++ ys) :
+    combineMinIdxOn f i j hi hj < zs.length := by
+  simp only [combineMinIdxOn, h]
+  split <;> (simp; omega)
+
 private theorem combineMinIdxOn_assoc [LE β] [DecidableLE β] [IsLinearPreorder β]
     {xs ys zs : List α} {i j k : Nat} {f : α → β} (hi : i < xs.length) (hj : j < ys.length)
-    (hk : k < zs.length) :
+    (hk : k < zs.length) (h) :
     combineMinIdxOn f (combineMinIdxOn f i j _ _) k
-      (combineMinIdxOn_lt f hi hj) hk = combineMinIdxOn f i (combineMinIdxOn f j k _ _) hi (combineMinIdxOn_lt f hj hk) := by
+      (combineMinIdxOn_lt' f xys hi hj h) hk = combineMinIdxOn f i (combineMinIdxOn f j k _ _) hi (combineMinIdxOn_lt f hj hk) := by
+  cases h
   open scoped Classical.Order in
   simp only [combineMinIdxOn]
   split
@@ -412,7 +420,8 @@ private theorem minIdxOn_append_aux [LE β] [DecidableLE β]
     | z :: zs =>
       simp +singlePass only [cons_append]
       simp only [minIdxOn_cons_aux (xs := z :: zs ++ ys) (by simp), ih (by simp),
-        minIdxOn_cons_aux (xs := z :: zs) (by simp), combineMinIdxOn_assoc]
+        minIdxOn_cons_aux (xs := z :: zs) (by simp)]
+      rw [combineMinIdxOn_assoc (h := by simp)]
 
 protected theorem minIdxOn_append [LE β] [DecidableLE β] [IsLinearPreorder β]
     {xs ys : List α} {f : α → β} (hxs : xs ≠ []) (hys : ys ≠ []) :

src/Init/Data/List/MinMaxOn.lean

@@ -99,6 +99,15 @@ protected theorem minOn_cons
   | [] => simp
   | y :: xs => simp [foldl_assoc]
 
+protected theorem minOn_cons_cons [LE β] [DecidableLE β] {a b : α} {l : List α} {f : α → β} :
+    (a :: b :: l).minOn f (by simp) = (minOn f a b :: l).minOn f (by simp) :=
+  (rfl)
+
+@[simp]
+protected theorem minOn_cons_cons_nil [LE β] [DecidableLE β] {a b : α} {f : α → β} :
+    [a, b].minOn f (by simp) = minOn f a b := by
+  simp [List.minOn_cons_cons]
+
 @[simp]
 protected theorem minOn_id [Min α] [LE α] [DecidableLE α] [LawfulOrderLeftLeaningMin α]
     {xs : List α} (h : xs ≠ []) :
@@ -242,6 +251,26 @@ protected theorem min_map
     rw [foldl_hom]
     simp [min_apply]
 
+protected theorem minOn_eq_min [Min α] [LE α] [DecidableLE α] [LawfulOrderLeftLeaningMin α]
+    [LE β] [DecidableLE β] {f : α → β} {l : List α} {h}
+    (hf : ∀ a b, f a ≤ f b ↔ a ≤ b) : l.minOn f h = l.min h := by
+  generalize hlen : l.length = n
+  induction n generalizing l with
+  | zero => simp_all
+  | succ n ih =>
+    match n, l, hlen with
+    | 0, [_], _ => simp
+    | 1, [b, c], _ => simp [_root_.minOn_eq_min (hf b c)]
+    | n + 2, b :: c :: tl, _ =>
+      simp [min_cons_cons, List.minOn_cons_cons, _root_.minOn_eq_min (hf b c)]
+      rw [ih (by exact Nat.succ.inj ‹_›)]
+
+protected theorem min_map_eq_min [Min α] [LE α] [DecidableLE α] [LawfulOrderLeftLeaningMin α]
+    [Min β] [LE β] [DecidableLE β] [IsLinearPreorder β] [LawfulOrderLeftLeaningMin β]
+    {f : α → β} (hf : ∀ a b, f a ≤ f b ↔ a ≤ b) {l : List α} {h : l ≠ []} :
+    (l.map f).min (by simpa) = f (l.min h) := by
+  rw [List.min_map h, List.minOn_eq_min hf]
+
 @[simp]
 protected theorem minOn_replicate [LE β] [DecidableLE β] [IsLinearPreorder β]
     {n : Nat} {a : α} {f : α → β} (h : replicate n a ≠ []) :
@@ -271,6 +300,17 @@ protected theorem maxOn_cons
   letI : LE β := (inferInstanceAs (LE β)).opposite
   exact List.minOn_cons (f := f)
 
+protected theorem maxOn_cons_cons [LE β] [DecidableLE β] {a b : α} {l : List α} {f : α → β} :
+    (a :: b :: l).maxOn f (by simp) = (maxOn f a b :: l).maxOn f (by simp) := by
+  simp only [List.maxOn_eq_minOn, maxOn_eq_minOn]
+  letI : LE β := (inferInstanceAs (LE β)).opposite
+  exact List.minOn_cons_cons
+
+@[simp]
+protected theorem maxOn_cons_cons_nil [LE β] [DecidableLE β] {a b : α} {f : α → β} :
+    [a, b].maxOn f (by simp) = maxOn f a b := by
+  simp [List.maxOn_cons_cons]
+
 protected theorem min_eq_max {min : Min α} {xs : List α} {h} :
     xs.min h = (letI := min.oppositeMax; xs.max h) := by
   simp only [List.min, List.max]
@@ -394,6 +434,26 @@ protected theorem max_map
   letI : Min β := (inferInstanceAs (Max β)).oppositeMin
   simpa [List.max_eq_min] using List.min_map (f := f) h
 
+protected theorem maxOn_eq_max [Max α] [LE α] [DecidableLE α] [LawfulOrderLeftLeaningMax α]
+    [LE β] [DecidableLE β] {f : α → β} {l : List α} {h}
+    (hf : ∀ a b, f a ≤ f b ↔ a ≤ b) : l.maxOn f h = l.max h := by
+  generalize hlen : l.length = n
+  induction n generalizing l with
+  | zero => simp_all
+  | succ n ih =>
+    match n, l, hlen with
+    | 0, [_], _ => simp
+    | 1, [b, c], _ => simp [_root_.maxOn_eq_max (hf c b)]
+    | n + 2, b :: c :: tl, _ =>
+      simp [max_cons_cons, List.maxOn_cons_cons, _root_.maxOn_eq_max (hf c b)]
+      rw [ih (by exact Nat.succ.inj ‹_›)]
+
+protected theorem max_map_eq_max [Max α] [LE α] [DecidableLE α] [LawfulOrderLeftLeaningMax α]
+    [Max β] [LE β] [DecidableLE β] [IsLinearPreorder β] [LawfulOrderLeftLeaningMax β]
+    {f : α → β} (hf : ∀ a b, f a ≤ f b ↔ a ≤ b) {l : List α} {h : l ≠ []} :
+    (l.map f).max (by simpa) = f (l.max h) := by
+  rw [List.max_map h, List.maxOn_eq_max hf]
+
 @[simp]
 protected theorem maxOn_replicate [LE β] [DecidableLE β] [IsLinearPreorder β]
     {n : Nat} {a : α} {f : α → β} (h : replicate n a ≠ []) :

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

@@ -25,6 +25,7 @@ namespace List
 
 open Nat
 
+set_option backward.isDefEq.respectTransparency false in
 @[grind =]
 theorem countP_set {p : α → Bool} {l : List α} {i : Nat} {a : α} (h : i < l.length) :
     (l.set i a).countP p = l.countP p - (if p l[i] then 1 else 0) + (if p a then 1 else 0) := by

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

@@ -53,10 +53,12 @@ theorem sublist_eq_map_getElem {l l' : List α} (h : l' <+ l) : ∃ is : List (F
   | cons _ _ IH =>
     let ⟨is, IH⟩ := IH
     refine ⟨is.map (·.succ), ?_⟩
+    set_option backward.isDefEq.respectTransparency false in
     simpa [Function.comp_def, pairwise_map]
   | cons₂ _ _ IH =>
     rcases IH with ⟨is,IH⟩
     refine ⟨⟨0, by simp [Nat.zero_lt_succ]⟩ :: is.map (·.succ), ?_⟩
+    set_option backward.isDefEq.respectTransparency false in
     simp [Function.comp_def, pairwise_map, IH, ← get_eq_getElem, get_cons_zero, get_cons_succ']
 
 set_option linter.listVariables false in

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

@@ -387,6 +387,22 @@ theorem drop_take : ∀ {i j : Nat} {l : List α}, drop i (take j l) = take (j -
   rw [drop_take]
   simp
 
+set_option doc.verso true in
+/--
+This lemma will be renamed to {lit}`List.extract_eq_drop_take` as soon as the current deprecated
+lemma {name}`List.extract_eq_drop_take` has been removed.
+-/
+theorem extract_eq_drop_take' {l : List α} {start stop : Nat} :
+    l.extract start stop = (l.take stop).drop start := by
+  simp only [take_drop]
+  by_cases start ≤ stop
+  · rw [add_sub_of_le ‹_›]
+  · have h₁ : stop - start = 0 := by omega
+    have h₂ : min stop l.length ≤ stop := by omega
+    simp only [Nat.add_zero, List.drop_take_self, List.nil_eq, List.drop_eq_nil_iff,
+      List.length_take, ge_iff_le, h₁]
+    omega
+
 @[simp]
 theorem drop_eq_drop_iff :
     ∀ {l : List α} {i j : Nat}, l.drop i = l.drop j ↔ min i l.length = min j l.length

src/Init/Data/List/OfFn.lean

@@ -98,7 +98,8 @@ theorem ofFn_add {n m} {f : Fin (n + m) → α} :
     ofFn f = (ofFn fun i => f (i.castLE (Nat.le_add_right n m))) ++ (ofFn fun i => f (i.natAdd n)) := by
   induction m with
   | zero => simp
-  | succ m ih => simp [-ofFn_succ, ofFn_succ_last, ih]
+  | succ m ih =>
+    simp [-ofFn_succ, ofFn_succ_last, ih]
 
 @[simp]
 theorem ofFn_eq_nil_iff {f : Fin n → α} : ofFn f = [] ↔ n = 0 := by
@@ -154,8 +155,8 @@ theorem ofFnM_add {n m} [Monad m] [LawfulMonad m] {f : Fin (n + k) → m α} :
       pure (as ++ bs)) := by
   induction k with
   | zero => simp
-  | succ k ih => simp [ofFnM_succ_last, ih]
-
+  | succ k ih =>
+    simp [ofFnM_succ_last, ih]
 
 end List
 

src/Init/Data/List/Scan.lean

@@ -0,0 +1,10 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Init.Data.List.Scan.Basic
+public import Init.Data.List.Scan.Lemmas

src/Init/Data/List/Scan/Basic.lean

@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, Chad Sharp
+-/
+module
+
+prelude
+public import Init.Data.List.Basic
+public import Init.Control.Id
+
+public section
+
+namespace List
+
+/-- Tail-recursive helper function for `scanlM` and `scanrM` -/
+@[inline]
+private def scanAuxM [Monad m] (f : β → α → m β) (init : β) (l : List α) : m (List β) :=
+  go l init []
+where
+  /-- Auxiliary for `scanAuxM` -/
+  @[specialize] go : List α → β → List β → m (List β)
+    | [], last, acc => pure <| last :: acc
+    | x :: xs, last, acc => do go xs (← f last x) (last :: acc)
+
+/--
+Folds a monadic function over a list from the left, accumulating partial results starting with
+`init`. The accumulated values are combined with the each element of the list in order, using `f`.
+-/
+@[inline]
+def scanlM [Monad m] (f : β → α → m β) (init : β) (l : List α) : m (List β) :=
+  List.reverse <$> scanAuxM f init l
+
+/--
+Folds a monadic function over a list from the right, accumulating partial results starting with
+`init`. The accumulated values are combined with the each element of the list in order, using `f`.
+-/
+@[inline]
+def scanrM [Monad m] (f : α → β → m β) (init : β) (xs : List α) : m (List β) :=
+  scanAuxM (flip f) init xs.reverse
+
+/--
+Fold a function `f` over the list from the left, returning the list of partial results.
+```
+scanl (+) 0 [1, 2, 3] = [0, 1, 3, 6]
+```
+-/
+@[inline]
+def scanl (f : β → α → β) (init : β) (as : List α) : List β :=
+  Id.run <| as.scanlM (pure <| f · ·) init
+
+/--
+Fold a function `f` over the list from the right, returning the list of partial results.
+```
+scanr (+) 0 [1, 2, 3] = [6, 5, 3, 0]
+```
+-/
+@[inline]
+def scanr (f : α → β → β) (init : β) (as : List α) : List β :=
+  Id.run <| as.scanrM (pure <| f · ·) init
+
+end List

src/Init/Data/List/Scan/Lemmas.lean

@@ -0,0 +1,339 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro, Chad Sharp
+-/
+module
+
+prelude
+public import Init.Data.List.Scan.Basic
+public import Init.Data.List.Lemmas
+import all Init.Data.List.Scan.Basic
+import Init.Data.List.TakeDrop
+import Init.Data.Option.Lemmas
+import Init.Data.Nat.Lemmas
+
+public section
+
+/-!
+# List scan
+
+Prove basic results about `List.scanl`, `List.scanr`, `List.scanlM` and `List.scanrM`.
+-/
+
+namespace List
+
+/-! ### `List.scanlM` and `List.scanrM` -/
+
+@[local simp]
+private theorem scanAuxM.go_eq_append_map [Monad m] [LawfulMonad m] {f : α → β → m α} :
+    go f xs last acc = (· ++ acc) <$> scanAuxM f last xs := by
+  unfold scanAuxM
+  induction xs generalizing last acc with
+  | nil => simp [scanAuxM.go]
+  | cons _ _ ih => simp [scanAuxM.go, ih (acc := last :: acc), ih (acc := [last])]
+
+private theorem scanAuxM_nil [Monad m] {f : α → β → m α} :
+    scanAuxM f init [] = return [init] := rfl
+
+private theorem scanAuxM_cons [Monad m] [LawfulMonad m] {f : α → β → m α} :
+    scanAuxM f init (x :: xs) = return (← scanAuxM f (← f init x) xs) ++ [init] := by
+  rw [scanAuxM, scanAuxM.go]
+  simp
+
+@[simp, grind =]
+theorem scanlM_nil [Monad m] [LawfulMonad m] {f : α → β → m α} :
+    scanlM f init [] = return [init] := by
+  simp [scanlM, scanAuxM_nil]
+
+@[simp, grind =]
+theorem scanlM_cons [Monad m] [LawfulMonad m] {f : α → β → m α} :
+    scanlM f init (x :: xs) = return init :: (← scanlM f (← f init x) xs) := by
+  simp [scanlM, scanAuxM_cons]
+
+@[simp, grind =]
+theorem scanrM_concat [Monad m] [LawfulMonad m] {f : α → β → m β} :
+    scanrM f init (xs ++ [x]) = return (← scanrM f (← f x init) xs) ++ [init] := by
+  simp [scanrM, flip, scanAuxM_cons]
+
+@[simp, grind =]
+theorem scanrM_nil [Monad m] {f : α → β → m β} :
+    scanrM f init [] = return [init] :=
+  (rfl)
+
+theorem scanlM_eq_scanrM_reverse [Monad m] {f : β → α → m β} :
+    scanlM f init as = reverse <$> (scanrM (flip f) init as.reverse) := by
+  simp only [scanrM, reverse_reverse]
+  rfl
+
+theorem scanrM_eq_scanlM_reverse [Monad m] [LawfulMonad m] {f : α → β → m β} :
+    scanrM f init as = reverse <$> (scanlM (flip f) init as.reverse) := by
+  simp only [scanlM_eq_scanrM_reverse, reverse_reverse, id_map', Functor.map_map]
+  rfl
+
+@[simp, grind =]
+theorem scanrM_reverse [Monad m] [LawfulMonad m] {f : α → β → m β} :
+    scanrM f init as.reverse = reverse <$> (scanlM (flip f) init as) := by
+  simp [scanrM_eq_scanlM_reverse (as := as.reverse)]
+
+@[simp, grind =]
+theorem scanlM_reverse [Monad m] {f : β → α → m β} :
+    scanlM f init as.reverse = reverse <$> (scanrM (flip f) init as) := by
+  simp [scanlM_eq_scanrM_reverse (as := as.reverse)]
+
+theorem scanlM_pure [Monad m] [LawfulMonad m] {f: β → α → β} {as : List α} :
+    as.scanlM (m := m) (pure <| f · ·) init = pure (as.scanl f init) := by
+  induction as generalizing init with simp_all [scanlM_cons, scanl]
+
+theorem scanrM_pure [Monad m] [LawfulMonad m] {f : α → β → β} {as : List α} :
+    as.scanrM (m := m) (pure <| f · · ) init = pure (as.scanr f init) := by
+  simp only [scanrM_eq_scanlM_reverse]
+  unfold flip
+  simp only [scanlM_pure, map_pure, scanr,  scanrM_eq_scanlM_reverse]
+  rfl
+
+theorem idRun_scanlM {f : β → α → Id β} {as : List α} :
+    (as.scanlM f init).run = as.scanl (f · · |>.run) init :=
+  scanlM_pure
+
+theorem idRun_scanrM {f : α → β → Id β} {as : List α} :
+    (as.scanrM f init).run = as.scanr (f · · |>.run) init :=
+  scanrM_pure
+
+@[simp, grind =]
+theorem scanlM_map [Monad m] [LawfulMonad m]
+    {f : α₁ → α₂} {g: β → α₂ → m β} {as : List α₁} :
+    (as.map f).scanlM g init = as.scanlM (g · <| f ·) init := by
+  induction as generalizing g init with simp [*]
+
+@[simp, grind =]
+theorem scanrM_map [Monad m] [LawfulMonad m]
+    {f : α₁ → α₂} {g: α₂ → β → m β} {as : List α₁} :
+    (as.map f).scanrM g init = as.scanrM (fun a b => g (f a) b) init := by
+  simp only [← map_reverse, scanlM_map, scanrM_eq_scanlM_reverse]
+  rfl
+
+/-! ### `List.scanl` and `List.scanr` -/
+
+@[simp]
+theorem length_scanl {f : β → α → β} : (scanl f init as).length = as.length + 1 := by
+  induction as generalizing init <;> simp_all [scanl, pure, bind, Id.run]
+
+grind_pattern length_scanl => scanl f init as
+
+@[simp, grind =]
+theorem scanl_nil {f : β → α → β} : scanl f init [] = [init] := by simp [scanl]
+
+@[simp, grind =]
+theorem scanl_cons {f : β → α → β} : scanl f b (a :: l) = b :: scanl f (f b a) l := by
+  simp [scanl]
+
+theorem scanl_singleton {f : β → α → β} : scanl f b [a] = [b, f b a] := by simp
+
+@[simp]
+theorem scanl_ne_nil {f : β → α → β} : scanl f b l ≠ [] := by
+  cases l <;> simp
+
+@[simp]
+theorem scanl_iff_nil {f : β → α → β} (c : β) : scanl f b l = [c] ↔ c = b ∧ l = [] := by
+  cases l
+  · simp [eq_comm]
+  · simp
+
+@[simp, grind =]
+theorem getElem_scanl {f : α → β → α} (h : i < (scanl f a l).length) :
+    (scanl f a l)[i] = foldl f a (l.take i) := by
+  induction l generalizing a i
+  · simp
+  · cases i <;> simp [*]
+
+@[grind =]
+theorem getElem?_scanl {f : α → β → α} :
+    (scanl f a l)[i]? = if i ≤ l.length then some (foldl f a (l.take i)) else none := by
+  split
+  · rw [getElem?_pos _ _ (by simpa using Nat.lt_add_one_iff.mpr ‹_›), getElem_scanl]
+  · rw [getElem?_neg]
+    simpa only [length_scanl, Nat.lt_add_one_iff]
+
+@[grind _=_]
+theorem take_scanl {f : β → α → β} (init : β) (as : List α) (i : Nat) :
+    (scanl f init as).take (i + 1) = scanl f init (as.take i) := by
+  induction as generalizing init i
+  · simp
+  · cases i
+    · simp
+    · simp [*]
+
+theorem getElem?_scanl_zero {f : β → α → β} : (scanl f b l)[0]? = some b := by
+  simp
+
+theorem getElem_scanl_zero {f : β → α → β} : (scanl f b l)[0] = b := by
+  simp
+
+@[simp]
+theorem head_scanl {f : β → α → β} (h : scanl f b l ≠ []) : (scanl f b l).head h = b := by
+  simp [head_eq_getElem]
+
+@[simp]
+theorem head?_scanl {f : β → α → β} : (scanl f b l).head? = some b := by
+  simp [head?_eq_getElem?]
+
+theorem getLast_scanl {f : β → α → β} (h : scanl f b l ≠ []) :
+    (scanl f b l).getLast h = foldl f b l := by
+  simp [getLast_eq_getElem]
+
+theorem getLast?_scanl {f : β → α → β} : (scanl f b l).getLast? = some (foldl f b l) := by
+  simp [getLast?_eq_getElem?]
+
+@[grind =]
+theorem tail_scanl {f : β → α → β} (h : 0 < l.length) :
+    (scanl f b l).tail = scanl f (f b (l.head (ne_nil_of_length_pos h))) l.tail := by
+  induction l
+  · simp at h
+  · simp
+
+theorem getElem?_succ_scanl {f : β → α → β} :
+    (scanl f b l)[i + 1]? = (scanl f b l)[i]?.bind fun x => l[i]?.map fun y => f x y := by
+  simp only [getElem?_scanl, take_add_one]
+  split
+  · have : i < l.length := Nat.add_one_le_iff.mp ‹_›
+    have : i ≤ l.length := Nat.le_of_lt ‹_›
+    simp [*, - take_append_getElem]
+  · split
+    · apply Eq.symm
+      simpa using Nat.lt_add_one_iff.mp (Nat.not_le.mp ‹_›)
+    · simp
+
+theorem getElem_succ_scanl {f : β → α → β} (h : i + 1 < (scanl f b l).length) :
+    (scanl f b l)[i + 1] = f ((l.scanl f b)[i]'(Nat.lt_trans (Nat.lt_add_one _) h)) (l[i]'(by simpa using h)) := by
+  simp only [length_scanl, Nat.add_lt_add_iff_right] at h
+  simp [take_add_one, *, - take_append_getElem]
+
+@[grind =]
+theorem scanl_append {f : β → α → β} {l₁ l₂ : List α} :
+    scanl f b (l₁ ++ l₂) = scanl f b l₁ ++ (scanl f (foldl f b l₁) l₂).tail := by
+  induction l₁ generalizing b
+  case nil => cases l₂ <;> simp
+  case cons head tail ih => simp [ih]
+
+@[grind =]
+theorem scanl_map {f : β → γ → β} {g : α → γ} {as : List α} :
+    scanl f init (as.map g) = scanl (fun acc x => f acc (g x)) init as := by
+  induction as generalizing init with simp [*]
+
+theorem scanl_eq_scanr_reverse {f : β → α → β} :
+    scanl f init as = reverse (scanr (flip f) init as.reverse) := by
+  simp only [scanl, scanr, Id.run, scanrM_reverse, Functor.map, reverse_reverse]
+  rfl
+
+theorem scanr_eq_scanl_reverse  {f : α → β → β} :
+    scanr f init as = reverse (scanl (flip f) init as.reverse) := by
+  simp only [scanl_eq_scanr_reverse, reverse_reverse]
+  rfl
+
+@[simp, grind =]
+theorem scanl_reverse {f : β → α → β} {as : List α} :
+    scanl f init as.reverse = reverse (scanr (flip f) init as) := by
+  simp [scanr_eq_scanl_reverse]
+
+@[simp, grind =]
+theorem scanr_reverse {f : α → β → β} {as : List α} :
+    scanr f init as.reverse = reverse (scanl (flip f) init as) := by
+  simp [scanl_eq_scanr_reverse]
+
+@[simp, grind =]
+theorem scanr_nil {f : α → β → β} : scanr f init [] = [init] := by simp [scanr]
+
+@[simp, grind =]
+theorem scanr_cons {f : α → β → β} :
+    scanr f b (a :: l) = foldr f b (a :: l) :: scanr f b l := by
+  simp [scanr_eq_scanl_reverse, reverse_cons, scanl_append, flip, - scanl_reverse]
+
+@[simp]
+theorem scanr_ne_nil {f : α → β → β} : scanr f b l ≠ [] := by
+  simp [scanr_eq_scanl_reverse, - scanl_reverse]
+
+theorem scanr_singleton {f : α → β → β} : scanr f b [a] = [f a b, b] := by
+  simp
+
+@[simp]
+theorem length_scanr {f : α → β → β} {as : List α} :
+    length (scanr f init as) = as.length + 1 := by
+  simp [scanr_eq_scanl_reverse, - scanl_reverse]
+
+grind_pattern length_scanr => scanr f init as
+
+@[simp]
+theorem scanr_iff_nil {f : α → β → β} (c : β) : scanr f b l = [c] ↔ c = b ∧ l = [] := by
+  simp [scanr_eq_scanl_reverse, - scanl_reverse]
+
+@[grind =]
+theorem scanr_append {f : α → β → β} (l₁ l₂ : List α) :
+    scanr f b (l₁ ++ l₂) = (scanr f (foldr f b l₂) l₁) ++ (scanr f b l₂).tail := by
+  induction l₁ <;> induction l₂ <;> simp [*]
+
+@[simp]
+theorem head_scanr {f : α → β → β} (h : scanr f b l ≠ []) :
+    (scanr f b l).head h = foldr f b l := by
+  simp [scanr_eq_scanl_reverse, - scanl_reverse, getLast_scanl, flip]
+
+@[grind =]
+theorem getLast_scanr {f : α → β → β} (h : scanr f b l ≠ []) :
+    (scanr f b l).getLast h = b := by
+  simp [scanr_eq_scanl_reverse, - scanl_reverse]
+
+theorem getLast?_scanr {f : α → β → β} : (scanr f b l).getLast? = some b := by
+  simp [scanr_eq_scanl_reverse, - scanl_reverse]
+
+@[grind =]
+theorem tail_scanr {f : α → β → β} (h : 0 < l.length) :
+    (scanr f b l).tail = scanr f b l.tail := by
+  induction l with simp_all
+
+@[grind _=_]
+theorem drop_scanr {f : α → β → β} (h : i ≤ l.length) :
+    (scanr f b l).drop i = scanr f b (l.drop i) := by
+  induction i generalizing l
+  · simp
+  · rename_i i ih
+    rw [drop_add_one_eq_tail_drop (i := i), drop_add_one_eq_tail_drop (i := i), ih]
+    · rw [tail_scanr]
+      simpa [length_drop, Nat.lt_sub_iff_add_lt]
+    · exact Nat.le_of_lt (Nat.add_one_le_iff.mp ‹_›)
+
+@[simp, grind =]
+theorem getElem_scanr {f : α → β → β} (h : i < (scanr f b l).length) :
+    (scanr f b l)[i] = foldr f b (l.drop i) := by
+  induction l generalizing b i
+  · simp
+  · cases i <;> simp [*]
+
+@[grind =]
+theorem getElem?_scanr {f : α → β → β} :
+    (scanr f b l)[i]? = if i < l.length + 1 then some (foldr f b (l.drop i)) else none := by
+  split
+  · rw [getElem?_pos _ _ (by simpa), getElem_scanr]
+  · rename_i h
+    simpa [getElem?_neg, length_scanr] using h
+
+@[simp]
+theorem head?_scanr {f : α → β → β} : (scanr f b l).head? = some (foldr f b l) := by
+  simp [head?_eq_getElem?]
+
+theorem getElem_scanr_zero {f : α → β → β} : (scanr f b l)[0] = foldr f b l := by
+  simp
+
+theorem getElem?_scanr_zero {f : α → β → β} : (scanr f b l)[0]? = some (foldr f b l) := by
+  simp
+
+theorem getElem?_scanr_of_lt {f : α → β → β} (h : i < l.length + 1) :
+    (scanr f b l)[i]? = some (foldr f b (l.drop i)) := by
+  simp [h]
+
+@[grind =]
+theorem scanr_map {f : α → β → β} {g : γ → α} (b : β) (l : List γ) :
+    scanr f b (l.map g) = scanr (fun x acc => f (g x) acc) b l := by
+  suffices ∀ l, foldr f b (l.map g) = foldr (fun x acc => f (g x) acc) b l from by
+    induction l generalizing b with simp [*]
+  intro l
+  induction l with simp [*]

src/Init/Data/List/Sort/Basic.lean

@@ -64,6 +64,7 @@ def MergeSort.Internal.splitInTwo (l : { l : List α // l.length = n }) :
 
 open MergeSort.Internal in
 set_option linter.unusedVariables false in
+set_option backward.isDefEq.respectTransparency false in
 /--
 A stable merge sort.
 

src/Init/Data/List/Sort/Impl.lean

@@ -182,14 +182,14 @@ private theorem mergeSortTR_run_eq_mergeSort : {n : Nat} → (l : { l : List α
     simp only [mergeSortTR.run, mergeSortTR.run, mergeSort]
     rw [merge_eq_mergeTR]
     rw [mergeSortTR_run_eq_mergeSort, mergeSortTR_run_eq_mergeSort]
+    rfl
 
 -- We don't make this a `@[csimp]` lemma because `mergeSort_eq_mergeSortTR₂` is faster.
 theorem mergeSort_eq_mergeSortTR : @mergeSort = @mergeSortTR := by
   funext
   rw [mergeSortTR, mergeSortTR_run_eq_mergeSort]
 
--- This mutual block is unfortunately quite slow to elaborate.
-set_option maxHeartbeats 400000 in
+set_option backward.isDefEq.respectTransparency false in
 mutual
 private theorem mergeSortTR₂_run_eq_mergeSort : {n : Nat} → (l : { l : List α // l.length = n }) → mergeSortTR₂.run le l = mergeSort l.1 le
   | 0, ⟨[], _⟩

src/Init/Data/List/TakeDrop.lean

@@ -268,7 +268,7 @@ theorem drop_eq_extract {l : List α} {k : Nat} :
     | 0 => simp
     | _ + 1 =>
       simp only [List.drop_succ_cons, List.length_cons, ih]
-      simp only [List.extract_eq_drop_take, List.drop_succ_cons, Nat.succ_sub_succ]
+      simp only [List.extract_eq_take_drop, List.drop_succ_cons, Nat.succ_sub_succ]
 
 /-! ### takeWhile and dropWhile -/
 

src/Init/Data/List/ToArray.lean

@@ -280,6 +280,7 @@ theorem findRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : Lis
     simp only [forIn_cons, find?]
     by_cases f a <;> simp_all
 
+set_option backward.isDefEq.respectTransparency false in
 private theorem findFinIdx?_loop_toArray (w : l' = l.drop j) :
     Array.findFinIdx?.loop p l.toArray j = List.findFinIdx?.go p l l' j h := by
   unfold findFinIdx?.loop
@@ -316,6 +317,7 @@ termination_by l.length - j
   rw [Array.findIdx?_eq_map_findFinIdx?_val, findIdx?_eq_map_findFinIdx?_val]
   simp [Array.size]
 
+set_option backward.isDefEq.respectTransparency false in
 private theorem idxAuxOf_toArray [BEq α] (a : α) (l : List α) (j : Nat) (w : l' = l.drop j) (h) :
     l.toArray.idxOfAux a j = findFinIdx?.go (fun x => x == a) l l' j h := by
   unfold idxOfAux
@@ -361,6 +363,7 @@ termination_by l.length - j
     as.toArray.idxOf a = as.idxOf a := by
   rw [Array.idxOf, findIdx_toArray, idxOf]
 
+set_option backward.isDefEq.respectTransparency false in
 theorem isPrefixOfAux_toArray_succ [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : Nat) :
     Array.isPrefixOfAux l₁.toArray l₂.toArray hle (i + 1) =
       Array.isPrefixOfAux l₁.tail.toArray l₂.tail.toArray (by simp; omega) i := by
@@ -616,13 +619,13 @@ decreasing_by
 @[simp, grind =] theorem eraseP_toArray {as : List α} {p : α → Bool} :
     as.toArray.eraseP p = (as.eraseP p).toArray := by
   rw [Array.eraseP, List.eraseP_eq_eraseIdx, findFinIdx?_toArray]
-  split <;> simp [*, findIdx?_eq_map_findFinIdx?_val]
+  split <;> simp [*, findIdx?_eq_map_findFinIdx?_val] <;> rfl
 
 @[simp, grind =] theorem erase_toArray [BEq α] {as : List α} {a : α} :
     as.toArray.erase a = (as.erase a).toArray := by
   rw [Array.erase, finIdxOf?_toArray, List.erase_eq_eraseIdx]
   rw [idxOf?_eq_map_finIdxOf?_val]
-  split <;> simp_all
+  split <;> simp_all <;> rfl
 
 private theorem insertIdx_loop_toArray (i : Nat) (l : List α) (j : Nat) (hj : j < l.toArray.size) (h : i ≤ j) :
     insertIdx.loop i l.toArray ⟨j, hj⟩ = (l.take i ++ l[j] :: (l.take j).drop i ++ l.drop (j + 1)).toArray := by
@@ -639,7 +642,7 @@ private theorem insertIdx_loop_toArray (i : Nat) (l : List α) (j : Nat) (hj : j
       getElem_set_self, take_set_of_le (j := j - 1) (by omega),
       take_set_of_le (j := j - 1) (by omega), take_eq_append_getElem_of_pos (by omega) hj,
       drop_append_of_le_length (by simp; omega)]
-    simp only [append_assoc, cons_append, nil_append, append_cancel_right_eq]
+    simp only [append_assoc, cons_append, nil_append]
     cases i with
     | zero => simp
     | succ i => rw [take_set_of_le (by omega)]

src/Init/Data/List/ToArrayImpl.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Prelude
+import Init.Data.List.Basic
 
 public section
 

src/Init/Data/Nat.lean

@@ -26,3 +26,4 @@ public import Init.Data.Nat.Compare
 public import Init.Data.Nat.Simproc
 public import Init.Data.Nat.Fold
 public import Init.Data.Nat.Order
+public import Init.Data.Nat.ToString

src/Init/Data/Nat/Fold.lean

@@ -434,7 +434,8 @@ theorem dfoldRev_add
         (dfoldRev m (α := fun i h => α (n + i)) (fun i h => f (n + i) (by omega)) init) := by
   induction m with
   | zero => simp; rfl
-  | succ m ih => simp [← Nat.add_assoc, ih]
+  | succ m ih =>
+    simp [← Nat.add_assoc, ih]
 
 end Nat
 

src/Init/Data/Nat/ToString.lean

@@ -0,0 +1,197 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Marcus Rossel, Paul Reichert
+-/
+module
+
+prelude
+public import Init.Data.Repr
+public import Init.Data.Char.Basic
+public import Init.Data.ToString.Basic
+public import Init.Data.String.Basic
+import Init.NotationExtra
+import all Init.Data.Repr
+import Init.Omega
+import Init.RCases
+import Init.Data.Nat.Lemmas
+import Init.Data.Nat.Bitwise
+import Init.Data.Nat.Simproc
+import Init.WFTactics
+import Init.Data.Char.Lemmas
+
+public section
+
+-- todo: lemmas about `ToString Nat` and `ToString Int`
+
+namespace Nat
+
+variable {b : Nat}
+
+
+@[simp]
+theorem isDigit_digitChar : n.digitChar.isDigit = decide (n < 10) :=
+  match n with
+  | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 => by simp [digitChar]
+  | _ + 10 => by
+    simp only [digitChar, ↓reduceIte, Nat.reduceEqDiff]
+    (repeat' split) <;> simp
+
+private theorem isDigit_of_mem_toDigitsCore
+    (hc : c ∈ cs → c.isDigit) (hb₁ : 0 < b) (hb₂ : b ≤ 10) (h : c ∈ toDigitsCore b fuel n cs) :
+    c.isDigit := by
+  induction fuel generalizing n cs with rw [toDigitsCore] at h
+  | zero => exact hc h
+  | succ _ ih =>
+    split at h
+    case' isFalse => apply ih (fun h => ?_) h
+    all_goals
+      cases h with
+      | head      => simp [Nat.lt_of_lt_of_le (mod_lt _ hb₁) hb₂]
+      | tail _ hm => exact hc hm
+
+theorem isDigit_of_mem_toDigits (hb₁ : 0 < b) (hb₂ : b ≤ 10) (hc : c ∈ toDigits b n) : c.isDigit :=
+  isDigit_of_mem_toDigitsCore (fun _ => by contradiction) hb₁ hb₂ hc
+
+private theorem toDigitsCore_of_lt_base (hb : n < b) (hf : n < fuel) :
+    toDigitsCore b fuel n cs = n.digitChar :: cs := by
+  unfold toDigitsCore
+  split <;> simp_all [mod_eq_of_lt]
+
+theorem toDigits_of_lt_base (h : n < b) : toDigits b n = [n.digitChar] :=
+  toDigitsCore_of_lt_base h (lt_succ_self _)
+
+@[simp, grind =]
+theorem toDigits_zero : (b : Nat) → toDigits b 0 = ['0']
+  | 0     => rfl
+  | _ + 1 => toDigits_of_lt_base (zero_lt_succ _)
+
+private theorem toDigitsCore_append :
+    toDigitsCore b fuel n cs₁ ++ cs₂ = toDigitsCore b fuel n (cs₁ ++ cs₂) := by
+  induction fuel generalizing n cs₁ with simp only [toDigitsCore]
+  | succ => split <;> simp_all
+
+private theorem toDigitsCore_eq_toDigitsCore_nil_append :
+    toDigitsCore b fuel n cs₁ = toDigitsCore b fuel n [] ++ cs₁ := by
+  simp [toDigitsCore_append]
+
+private theorem toDigitsCore_eq_of_lt_fuel (hb : 1 < b) (h₁ : n < fuel₁) (h₂ : n < fuel₂) :
+    toDigitsCore b fuel₁ n cs = toDigitsCore b fuel₂ n cs := by
+  cases fuel₁ <;> cases fuel₂ <;> try contradiction
+  simp only [toDigitsCore, Nat.div_eq_zero_iff]
+  split
+  · simp
+  · have := Nat.div_lt_self (by omega : 0 < n) hb
+    exact toDigitsCore_eq_of_lt_fuel hb (by omega) (by omega)
+
+private theorem toDigitsCore_toDigitsCore
+    (hb : 1 < b) (hn : 0 < n) (hd : d < b) (hf : b * n + d < fuel) (hnf : n < nf) (hdf : d < df) :
+    toDigitsCore b nf n (toDigitsCore b df d cs) = toDigitsCore b fuel (b * n + d) cs := by
+  cases fuel with
+  | zero => contradiction
+  | succ fuel =>
+    rw [toDigitsCore]
+    split
+    case isTrue h =>
+      have : b ≤ b * n + d := Nat.le_trans (Nat.le_mul_of_pos_right _ hn) (le_add_right _ _)
+      cases Nat.div_eq_zero_iff.mp h <;> omega
+    case isFalse =>
+      have h : (b * n + d) / b = n := by
+        rw [mul_add_div (by omega), Nat.div_eq_zero_iff.mpr (.inr hd), Nat.add_zero]
+      have := (Nat.lt_mul_iff_one_lt_left hn).mpr hb
+      simp only [toDigitsCore_of_lt_base hd hdf, mul_add_mod_self_left, mod_eq_of_lt hd, h]
+      apply toDigitsCore_eq_of_lt_fuel hb hnf (by omega)
+
+theorem toDigits_append_toDigits (hb : 1 < b) (hn : 0 < n) (hd : d < b) :
+    (toDigits b n) ++ (toDigits b d) = toDigits b (b * n + d) := by
+  rw [toDigits, toDigitsCore_append]
+  exact toDigitsCore_toDigitsCore hb hn hd (lt_succ_self _) (lt_succ_self _) (lt_succ_self _)
+
+theorem toDigits_of_base_le (hb : 1 < b) (h : b ≤ n) :
+    toDigits b n = toDigits b (n / b) ++ [digitChar (n % b)] := by
+  have := Nat.div_add_mod n b
+  rw (occs := [1]) [← Nat.div_add_mod n b,
+    ← toDigits_append_toDigits (by omega) (Nat.div_pos_iff.mpr (by omega)) (Nat.mod_lt n (by omega))]
+  rw [toDigits_of_lt_base (n := n % b) (Nat.mod_lt n (by omega))]
+
+theorem toDigits_eq_if (hb : 1 < b) :
+    toDigits b n = if n < b then [digitChar n] else toDigits b (n / b) ++ [digitChar (n % b)] := by
+  split
+  · rw [toDigits_of_lt_base ‹_›]
+  · rw [toDigits_of_base_le hb (by omega)]
+
+theorem length_toDigits_pos {b n : Nat} :
+    0 < (Nat.toDigits b n).length := by
+  simp [toDigits]
+  rw [toDigitsCore]
+  split
+  · simp
+  · rw [toDigitsCore_eq_toDigitsCore_nil_append]
+    simp
+
+theorem length_toDigits_le_iff {n k : Nat} (hb : 1 < b) (h : 0 < k) :
+    (Nat.toDigits b n).length ≤ k ↔ n < b ^ k := by
+  match k with
+  | 0 => contradiction
+  | k + 1 =>
+    induction k generalizing n
+    · rw [toDigits_eq_if hb]
+      split <;> simp [*, length_toDigits_pos, ← Nat.pos_iff_ne_zero, - List.length_eq_zero_iff]
+    · rename_i ih
+      rw [toDigits_eq_if hb]
+      split
+      · rename_i hlt
+        simp [Nat.pow_add]
+        refine Nat.lt_of_lt_of_le hlt ?_
+        apply Nat.le_mul_of_pos_left
+        apply Nat.mul_pos
+        · apply Nat.pow_pos
+          omega
+        · omega
+      · simp [ih (n := n / b) (by omega), Nat.div_lt_iff_lt_mul (k := b) (by omega), Nat.pow_add]
+
+theorem repr_eq_ofList_toDigits {n : Nat} :
+    n.repr = .ofList (toDigits 10 n) :=
+  (rfl)
+
+theorem toString_eq_ofList_toDigits {n : Nat} :
+    toString n = .ofList (toDigits 10 n) :=
+  (rfl)
+
+@[simp, grind norm]
+theorem toString_eq_repr {n : Nat} :
+    toString n = n.repr :=
+  (rfl)
+
+@[simp, grind norm]
+theorem reprPrec_eq_repr {n i : Nat} :
+    reprPrec n i = n.repr :=
+  (rfl)
+
+@[simp, grind norm]
+theorem repr_eq_repr {n : Nat} :
+    repr n = n.repr :=
+  (rfl)
+
+theorem repr_of_lt {n : Nat} (h : n < 10) :
+    n.repr = .singleton (digitChar n) := by
+  rw [repr_eq_ofList_toDigits, toDigits_of_lt_base h, String.singleton_eq_ofList]
+
+theorem repr_of_ge {n : Nat} (h : 10 ≤ n) :
+    n.repr = (n / 10).repr ++ .singleton (digitChar (n % 10)) := by
+  simp [repr_eq_ofList_toDigits, toDigits_of_base_le (by omega) h, String.singleton_eq_ofList,
+    String.ofList_append]
+
+theorem repr_eq_repr_append_repr {n : Nat} (h : 10 ≤ n) :
+    n.repr = (n / 10).repr ++ (n % 10).repr := by
+  rw [repr_of_ge h, repr_of_lt (n := n % 10) (by omega)]
+
+theorem length_repr_pos {n : Nat} :
+    0 < n.repr.length := by
+  simpa [repr_eq_ofList_toDigits] using length_toDigits_pos
+
+theorem length_repr_le_iff {n k : Nat} (h : 0 < k) :
+    n.repr.length ≤ k ↔ n < 10 ^ k := by
+  simpa [repr_eq_ofList_toDigits] using length_toDigits_le_iff (by omega) h
+
+end Nat

src/Init/Data/Ord/Basic.lean

@@ -619,7 +619,7 @@ protected theorem compare_nil_right_eq_eq {α} [Ord α] {xs : List α} :
 end List
 
 /-- The lexicographic order on pairs. -/
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 def lexOrd [Ord α] [Ord β] : Ord (α × β) where
   compare := compareLex (compareOn (·.1)) (compareOn (·.2))
 
@@ -627,14 +627,14 @@ def lexOrd [Ord α] [Ord β] : Ord (α × β) where
 Constructs an `BEq` instance from an `Ord` instance that asserts that the result of `compare` is
 `Ordering.eq`.
 -/
-@[expose, instance_reducible] def beqOfOrd [Ord α] : BEq α where
+@[expose, implicit_reducible] def beqOfOrd [Ord α] : BEq α where
   beq a b := (compare a b).isEq
 
 /--
 Constructs an `LT` instance from an `Ord` instance that asserts that the result of `compare` is
 `Ordering.lt`.
 -/
-@[expose, instance_reducible] def ltOfOrd [Ord α] : LT α where
+@[expose, implicit_reducible] def ltOfOrd [Ord α] : LT α where
   lt a b := compare a b = Ordering.lt
 
 @[inline]
@@ -645,7 +645,7 @@ instance [Ord α] : DecidableRel (@LT.lt α ltOfOrd) := fun a b =>
 Constructs an `LE` instance from an `Ord` instance that asserts that the result of `compare`
 satisfies `Ordering.isLE`.
 -/
-@[expose, instance_reducible] def leOfOrd [Ord α] : LE α where
+@[expose, implicit_reducible] def leOfOrd [Ord α] : LE α where
   le a b := (compare a b).isLE
 
 @[inline]
@@ -677,7 +677,7 @@ Inverts the order of an `Ord` instance.
 The result is an `Ord α` instance that returns `Ordering.lt` when `ord` would return `Ordering.gt`
 and that returns `Ordering.gt` when `ord` would return `Ordering.lt`.
 -/
-@[expose, instance_reducible] protected def opposite (ord : Ord α) : Ord α where
+@[expose, implicit_reducible] protected def opposite (ord : Ord α) : Ord α where
   compare x y := ord.compare y x
 
 /--
@@ -688,7 +688,7 @@ In particular, `ord.on f` compares `x` and `y` by comparing `f x` and `f y` acco
 The function `compareOn` can be used to perform this comparison without constructing an intermediate
 `Ord` instance.
 -/
-@[expose, instance_reducible] protected def on (_ : Ord β) (f : α → β) : Ord α where
+@[expose, implicit_reducible] protected def on (_ : Ord β) (f : α → β) : Ord α where
   compare := compareOn f
 
 /--
@@ -707,7 +707,7 @@ The function `compareLex` can be used to perform this comparison without constru
 intermediate `Ord` instance. `Ordering.then` can be used to lexicographically combine the results of
 comparisons.
 -/
-@[expose, instance_reducible] protected def lex' (ord₁ ord₂ : Ord α) : Ord α where
+@[expose, implicit_reducible] protected def lex' (ord₁ ord₂ : Ord α) : Ord α where
   compare := compareLex ord₁.compare ord₂.compare
 
 end Ord

src/Init/Data/Order/Factories.lean

@@ -23,7 +23,7 @@ preferring `a` over `b` when in doubt.
 
 Has a `LawfulOrderLeftLeaningMin α` instance.
 -/
-@[inline, instance_reducible]
+@[inline, implicit_reducible]
 public def _root_.Min.leftLeaningOfLE (α : Type u) [LE α] [DecidableLE α] : Min α where
   min a b := if a ≤ b then a else b
 
@@ -33,7 +33,7 @@ preferring `a` over `b` when in doubt.
 
 Has a `LawfulOrderLeftLeaningMax α` instance.
 -/
-@[inline, instance_reducible]
+@[inline, implicit_reducible]
 public def _root_.Max.leftLeaningOfLE (α : Type u) [LE α] [DecidableLE α] : Max α where
   max a b := if b ≤ a then a else b
 

src/Init/Data/Order/FactoriesExtra.lean

@@ -19,7 +19,7 @@ Creates an `LE α` instance from an `Ord α` instance.
 `OrientedOrd α` must be satisfied so that the resulting `LE α` instance faithfully represents
 the `Ord α` instance.
 -/
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def _root_.LE.ofOrd (α : Type u) [Ord α] : LE α where
   le a b := (compare a b).isLE
 
@@ -39,7 +39,7 @@ Creates an `LT α` instance from an `Ord α` instance.
 `OrientedOrd α` must be satisfied so that the resulting `LT α` instance faithfully represents
 the `Ord α` instance.
 -/
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def _root_.LT.ofOrd (α : Type u) [Ord α] :
     LT α where
   lt a b := compare a b = .lt
@@ -104,7 +104,7 @@ public def _root_.DecidableLT.ofOrd (α : Type u) [LE α] [LT α] [Ord α] [Lawf
 
 /--
 Creates a `BEq α` instance from an `Ord α` instance. -/
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def _root_.BEq.ofOrd (α : Type u) [Ord α] :
     BEq α where
   beq a b := compare a b = .eq

src/Init/Data/Order/MinMaxOn.lean

@@ -124,6 +124,21 @@ public theorem min_apply [LE β] [DecidableLE β] [Min β] [LawfulOrderLeftLeani
   rw [min_eq_if, minOn]
   split <;> rfl
 
+public theorem minOn_eq_if [LE β] [DecidableLE β] {f : α → β} {a b : α} :
+    minOn f a b = if f a ≤ f b then a else b :=
+  (rfl)
+
+public theorem minOn_eq_min [Min α] [LE α] [DecidableLE α] [LawfulOrderLeftLeaningMin α] [LE β]
+    [DecidableLE β] {f : α → β} {a b : α} (hf : f a ≤ f b ↔ a ≤ b) :
+    minOn f a b = min a b := by
+  simp [minOn_eq_if, min_eq_if, hf]
+
+public theorem min_apply_eq_min [LE α] [DecidableLE α] [Min α] [LawfulOrderLeftLeaningMin α]
+    [Min β] [LE β] [DecidableLE β] [LawfulOrderLeftLeaningMin β]
+    (f : α → β) {a b : α} (hf : f a ≤ f b ↔ a ≤ b) :
+    min (f a) (f b) = f (min a b) := by
+  rw [min_apply, minOn_eq_min hf]
+
 /-! ## `maxOn` Lemmas -/
 
 public theorem maxOn_eq_minOn [le : LE β] [DecidableLE β] {f : α → β} {x y : α} :
@@ -195,3 +210,18 @@ public theorem max_apply [LE β] [DecidableLE β] [Max β] [LawfulOrderLeftLeani
 public theorem apply_maxOn [LE β] [DecidableLE β] [Max β] [LawfulOrderLeftLeaningMax β]
     {f : α → β} {x y : α} : f (maxOn f x y) = max (f x) (f y) :=
   max_apply.symm
+
+public theorem maxOn_eq_if [LE β] [DecidableLE β] {f : α → β} {a b : α} :
+    maxOn f a b = if f b ≤ f a then a else b := by
+  simp only [maxOn_eq_minOn, minOn_eq_if, LE.le_opposite_iff]
+
+public theorem maxOn_eq_max [Max α] [LE α] [DecidableLE α] [LawfulOrderLeftLeaningMax α] [LE β]
+    [DecidableLE β] {f : α → β} {a b : α} (hf : f b ≤ f a ↔ b ≤ a) :
+    maxOn f a b = max a b := by
+  simp [maxOn_eq_if, max_eq_if, hf]
+
+public theorem max_apply_eq_max [LE α] [DecidableLE α] [Max α] [LawfulOrderLeftLeaningMax α]
+    [Max β] [LE β] [DecidableLE β] [LawfulOrderLeftLeaningMax β]
+    (f : α → β) {a b : α} (hf : f b ≤ f a ↔ b ≤ a) :
+    max (f a) (f b) = f (max a b) := by
+  rw [max_apply, maxOn_eq_max hf]

src/Init/Data/Order/Opposite.lean

@@ -52,7 +52,7 @@ def max' [LE α] [DecidableLE α] (a b : α) : α :=
 Without the `open scoped` command, Lean would not find the required {lit}`DecidableLE α`
 instance for the opposite order.
 -/
-@[instance_reducible] def LE.opposite (le : LE α) : LE α where
+@[implicit_reducible] def LE.opposite (le : LE α) : LE α where
   le a b := b ≤ a
 
 theorem LE.opposite_def {le : LE α} :
@@ -262,15 +262,18 @@ scoped instance (priority := low) instLawfulOrderOrdOpposite {il : LE α} {io :
     haveI := il.opposite
     haveI := io.opposite
     LawfulOrderOrd α :=
-      @LawfulOrderOrd.mk α io.opposite il.opposite
-        (by intros a b
-            simp +instances only [LE.opposite, Ord.opposite]
-            try simp [compare, LE.le]
-            apply isLE_compare)
-        (by intros a b
-            simp +instances only [LE.opposite, Ord.opposite]
-            try simp [compare, LE.le]
-            apply isGE_compare)
+  letI i := il.opposite
+  letI j := io.opposite
+  { isLE_compare a b := by
+      unfold LE.opposite Ord.opposite
+      simp only [compare, LE.le]
+      letI := il; letI := io
+      apply isLE_compare
+    isGE_compare a b := by
+      unfold LE.opposite Ord.opposite
+      simp only [compare, LE.le]
+      letI := il; letI := io
+      apply isGE_compare }
 
 scoped instance (priority := low) instLawfulOrderLTOpposite {il : LE α} {it : LT α}
     [LawfulOrderLT α] :

src/Init/Data/Order/PackageFactories.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Init.Data.Order.LemmasExtra  -- shake: keep (instance inlined by `haveI`)
 public import Init.Data.Order.FactoriesExtra
+public import Init.Data.Order.Factories -- shake: keep (autoparam filling `Min.leftLeaningOfLE`)
 import Init.Data.Bool
 import Init.Data.Order.Lemmas
 
@@ -46,7 +47,7 @@ public instance instLawfulOrderBEqOfDecidableLE {α : Type u} [LE α] [Decidable
   beq_iff_le_and_ge := by simp [BEq.beq]
 
 /-- If `LT` can be characterized in terms of a decidable `LE`, then `LT` is decidable either. -/
-@[expose]
+@[expose, instance_reducible]
 public def decidableLTOfLE {α : Type u} [LE α] {_ : LT α} [DecidableLE α] [LawfulOrderLT α] :
     DecidableLT α :=
   fun a b =>
@@ -91,10 +92,11 @@ public structure Packages.PreorderOfLEArgs (α : Type u) where
       have := lt_iff
       DecidableLT α := by
     extract_lets
-    haveI := @_root_.Std.LawfulOrderLT.mk (lt_iff := by assumption) ..
     first
     | infer_instance
+    | (haveI := @_root_.Std.LawfulOrderLT.mk (lt_iff := by assumption) ..; infer_instance)
     | exact _root_.Std.FactoryInstances.decidableLTOfLE
+    | (haveI := @_root_.Std.LawfulOrderLT.mk (lt_iff := by assumption) ..; exact _root_.Std.FactoryInstances.decidableLTOfLE)
     | fail "Failed to automatically derive that `LT` is decidable. \
             Please ensure that a `DecidableLT` instance can be synthesized or \
             manually provide the field `decidableLT`."
@@ -169,7 +171,7 @@ automatically. If it fails, it is necessary to provide some of the fields manual
 * Other proof obligations, namely `le_refl` and `le_trans`, can be omitted if `Refl` and `Trans`
   instances can be synthesized.
 -/
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 public def PreorderPackage.ofLE (α : Type u)
     (args : Packages.PreorderOfLEArgs α := by exact {}) : PreorderPackage α where
   toLE := args.le
@@ -254,7 +256,7 @@ automatically. If it fails, it is necessary to provide some of the fields manual
 * Other proof obligations, namely `le_refl`, `le_trans` and `le_antisymm`, can be omitted if `Refl`,
   `Trans` and `Antisymm` instances can be synthesized.
 -/
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 public def PartialOrderPackage.ofLE (α : Type u)
     (args : Packages.PartialOrderOfLEArgs α := by exact {}) : PartialOrderPackage α where
   toPreorderPackage := .ofLE α args.toPreorderOfLEArgs
@@ -383,7 +385,7 @@ automatically. If it fails, it is necessary to provide some of the fields manual
 * Other proof obligations, namely `le_total` and `le_trans`, can be omitted if `Total` and `Trans`
   instances can be synthesized.
 -/
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 public def LinearPreorderPackage.ofLE (α : Type u)
     (args : Packages.LinearPreorderOfLEArgs α := by exact {}) : LinearPreorderPackage α where
   toPreorderPackage := .ofLE α args.toPreorderOfLEArgs
@@ -485,7 +487,7 @@ automatically. If it fails, it is necessary to provide some of the fields manual
 * Other proof obligations, namely `le_total`, `le_trans` and `le_antisymm`, can be omitted if
   `Total`, `Trans` and `Antisymm` instances can be synthesized.
 -/
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 public def LinearOrderPackage.ofLE (α : Type u)
     (args : Packages.LinearOrderOfLEArgs α := by exact {}) : LinearOrderPackage α where
   toLinearPreorderPackage := .ofLE α args.toLinearPreorderOfLEArgs
@@ -645,7 +647,7 @@ automatically. If it fails, it is necessary to provide some of the fields manual
 * Other proof obligations, for example `transOrd`, can be omitted if a matching instance can be
   synthesized.
 -/
-@[expose]
+@[expose, instance_reducible]
 public def LinearPreorderPackage.ofOrd (α : Type u)
     (args : Packages.LinearPreorderOfOrdArgs α := by exact {}) : LinearPreorderPackage α :=
   letI := args.ord
@@ -791,9 +793,10 @@ automatically. If it fails, it is necessary to provide some of the fields manual
 * Other proof obligations, such as `transOrd`, can be omitted if matching instances can be
   synthesized.
 -/
-@[expose]
+@[expose, instance_reducible]
 public def LinearOrderPackage.ofOrd (α : Type u)
     (args : Packages.LinearOrderOfOrdArgs α := by exact {}) : LinearOrderPackage α :=
+  -- set_option backward.isDefEq.respectTransparency false in
   letI := LinearPreorderPackage.ofOrd α args.toLinearPreorderOfOrdArgs
   haveI : LawfulEqOrd α := ⟨args.eq_of_compare _ _⟩
   letI : Min α := args.min

src/Init/Data/Range/Polymorphic/Internal/SignedBitVec.lean

@@ -6,16 +6,16 @@ Authors: Paul Reichert
 module
 
 prelude
-import Init.Data.BitVec.Bootstrap
-import Init.Data.BitVec.Lemmas
-import Init.Data.Int.DivMod.Lemmas
-import Init.Data.Int.Pow
-import Init.Data.Nat.Div.Lemmas
-import Init.Data.Nat.Lemmas
-import Init.Data.Nat.Mod
-import Init.Data.Option.Lemmas
-import Init.Data.Range.Polymorphic.BitVec
-import Init.Omega
+public import Init.Data.BitVec.Bootstrap
+public import Init.Data.BitVec.Lemmas
+public import Init.Data.Int.DivMod.Lemmas
+public import Init.Data.Int.Pow
+public import Init.Data.Nat.Div.Lemmas
+public import Init.Data.Nat.Lemmas
+public import Init.Data.Nat.Mod
+public import Init.Data.Option.Lemmas
+public import Init.Data.Range.Polymorphic.BitVec
+public import Init.Omega
 
 /-!
 # Ranges on signed bit vectors

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

@@ -486,7 +486,7 @@ public theorem Rxc.Iterator.toList_eq_toList_rxoIterator [LE α] [DecidableLE α
   · simp only [UpwardEnumerable.le_iff, UpwardEnumerable.lt_iff, *]
     split <;> rename_i h
     · rw [ihy]; rotate_left
-      · simp [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+      · simp [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep, instIteratorIteratorIdOfUpwardEnumerableOfDecidableLE, -- TODO
           Iterator.Monadic.step, Iter.toIterM, *]; rfl
       · simpa [UpwardEnumerable.lt_iff, UpwardEnumerable.le_iff, UpwardEnumerable.lt_succ_iff] using h
     · simpa [UpwardEnumerable.lt_iff, UpwardEnumerable.le_iff, UpwardEnumerable.lt_succ_iff] using h
@@ -535,6 +535,14 @@ public theorem Rxc.Iterator.pairwise_toList_upwardEnumerableLt [LE α] [Decidabl
   · apply ihy (out := a)
     simp_all [Rxc.Iterator.isPlausibleStep_iff, Rxc.Iterator.step]
 
+theorem Rxc.Iterator.nodup_toList [LE α] [DecidableLE α]
+    [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α]
+    [PRange.LawfulUpwardEnumerableLE α]
+    {it : Iter (α := Rxc.Iterator α) α} :
+    it.toList.Nodup := by
+  apply (Rxc.Iterator.pairwise_toList_upwardEnumerableLt it).imp
+  apply PRange.UpwardEnumerable.ne_of_lt
+
 public theorem Rxo.Iterator.pairwise_toList_upwardEnumerableLt [LT α] [DecidableLT α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
     [Rxo.IsAlwaysFinite α]
@@ -558,6 +566,14 @@ public theorem Rxo.Iterator.pairwise_toList_upwardEnumerableLt [LT α] [Decidabl
   · apply ihy (out := a)
     simp_all [Rxo.Iterator.isPlausibleStep_iff, Rxo.Iterator.step]
 
+theorem Rxo.Iterator.nodup_toList [LT α] [DecidableLT α]
+    [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α]
+    [PRange.LawfulUpwardEnumerableLT α]
+    {it : Iter (α := Rxo.Iterator α) α} :
+    it.toList.Nodup := by
+  apply (Rxo.Iterator.pairwise_toList_upwardEnumerableLt it).imp
+  apply PRange.UpwardEnumerable.ne_of_lt
+
 public theorem Rxi.Iterator.pairwise_toList_upwardEnumerableLt
     [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     [Rxi.IsAlwaysFinite α]
@@ -581,6 +597,13 @@ public theorem Rxi.Iterator.pairwise_toList_upwardEnumerableLt
   · apply ihy (out := a)
     simp_all [Rxi.Iterator.isPlausibleStep_iff, Rxi.Iterator.step]
 
+theorem Rxi.Iterator.nodup_toList
+    [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α]
+    {it : Iter (α := Rxi.Iterator α) α} :
+    it.toList.Nodup := by
+  apply (Rxi.Iterator.pairwise_toList_upwardEnumerableLt it).imp
+  apply PRange.UpwardEnumerable.ne_of_lt
+
 namespace Rcc
 
 variable {r : Rcc α}
@@ -658,6 +681,13 @@ public theorem pairwise_toList_upwardEnumerableLt [LE α] [DecidableLE α]
   rw [Internal.toList_eq_toList_iter]
   apply Rxc.Iterator.pairwise_toList_upwardEnumerableLt
 
+public theorem nodup_toList [LE α] [DecidableLE α]
+    [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α]
+    [PRange.LawfulUpwardEnumerableLE α]
+    {a b : α} :
+    (a...=b).toList.Nodup := by
+  simpa [Internal.toList_eq_toList_iter] using Std.Rxc.Iterator.nodup_toList
+
 public theorem pairwise_toList_ne [LE α] [DecidableLE α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
     [Rxc.IsAlwaysFinite α] :
@@ -913,6 +943,13 @@ public theorem pairwise_toList_upwardEnumerableLt [LE α] [LT α] [DecidableLT
   rw [Internal.toList_eq_toList_iter]
   apply Rxo.Iterator.pairwise_toList_upwardEnumerableLt
 
+public theorem nodup_toList [LT α] [DecidableLT α]
+    [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α]
+    [PRange.LawfulUpwardEnumerableLT α]
+    {a b : α} :
+    (a...b).toList.Nodup := by
+  simpa [Internal.toList_eq_toList_iter] using Std.Rxo.Iterator.nodup_toList
+
 public theorem pairwise_toList_ne [LE α] [LT α] [DecidableLT α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
     [Rxo.IsAlwaysFinite α] :
@@ -1124,6 +1161,11 @@ public theorem pairwise_toList_upwardEnumerableLt [LE α]
   rw [Internal.toList_eq_toList_iter]
   apply Rxi.Iterator.pairwise_toList_upwardEnumerableLt
 
+public theorem nodup_toList
+    [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α]
+    {a : α} : (a...*).toList.Nodup := by
+  simpa [Internal.toList_eq_toList_iter] using Std.Rxi.Iterator.nodup_toList
+
 public theorem pairwise_toList_ne [LE α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => a ≠ b) :=
@@ -1363,6 +1405,13 @@ public theorem pairwise_toList_upwardEnumerableLt [LE α] [DecidableLE α]
   rw [Internal.toList_eq_toList_iter]
   apply Rxc.Iterator.pairwise_toList_upwardEnumerableLt
 
+public theorem nodup_toList [LE α] [DecidableLE α]
+    [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α]
+    [PRange.LawfulUpwardEnumerableLE α]
+    {a b : α} :
+    (a<...=b).toList.Nodup := by
+  simpa [Internal.toList_eq_toList_iter] using Std.Rxc.Iterator.nodup_toList
+
 public theorem pairwise_toList_ne [LE α] [DecidableLE α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
     [Rxc.IsAlwaysFinite α] :
@@ -1588,6 +1637,13 @@ public theorem pairwise_toList_upwardEnumerableLt [LT α] [DecidableLT α]
   rw [Internal.toList_eq_toList_iter]
   apply Rxo.Iterator.pairwise_toList_upwardEnumerableLt
 
+public theorem nodup_toList [LT α] [DecidableLT α]
+    [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α]
+    [PRange.LawfulUpwardEnumerableLT α]
+    {a b : α} :
+    (a<...b).toList.Nodup := by
+  simpa [Internal.toList_eq_toList_iter] using Std.Rxo.Iterator.nodup_toList
+
 public theorem pairwise_toList_ne [LT α] [DecidableLT α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
     [Rxo.IsAlwaysFinite α] :
@@ -1823,6 +1879,11 @@ public theorem pairwise_toList_upwardEnumerableLt
   rw [Internal.toList_eq_toList_iter]
   apply Rxi.Iterator.pairwise_toList_upwardEnumerableLt
 
+public theorem nodup_toList
+    [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α]
+    {a : α} : (a<...*).toList.Nodup := by
+  simpa [Internal.toList_eq_toList_iter] using Std.Rxi.Iterator.nodup_toList
+
 public theorem pairwise_toList_ne
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => a ≠ b) :=
@@ -2072,6 +2133,13 @@ public theorem pairwise_toList_upwardEnumerableLt [LE α] [DecidableLE α] [Leas
     r.toList.Pairwise (fun a b => UpwardEnumerable.LT a b) := by
   simp [toList_eq_toList_rcc, Rcc.pairwise_toList_upwardEnumerableLt]
 
+public theorem nodup_toList [LE α] [DecidableLE α] [Least? α]
+    [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α]
+    [PRange.LawfulUpwardEnumerableLE α]
+    {a : α} :
+    (*...=a).toList.Nodup := by
+  simpa [Internal.toList_eq_toList_iter] using Std.Rxc.Iterator.nodup_toList
+
 public theorem pairwise_toList_ne [LE α] [DecidableLE α] [Least? α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
     [LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] :
@@ -2395,6 +2463,13 @@ public theorem pairwise_toList_upwardEnumerableLt [LT α] [DecidableLT α] [Leas
     · exact Roo.pairwise_toList_upwardEnumerableLt
   · simp
 
+public theorem nodup_toList [LT α] [DecidableLT α] [Least? α]
+    [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α]
+    [PRange.LawfulUpwardEnumerableLT α]
+    {a : α} :
+    (*...a).toList.Nodup := by
+  simpa [Internal.toList_eq_toList_iter] using Std.Rxo.Iterator.nodup_toList
+
 public theorem pairwise_toList_ne [LT α] [DecidableLT α] [Least? α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
     [LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] :
@@ -2688,6 +2763,11 @@ public theorem pairwise_toList_upwardEnumerableLt [Least? α]
   · simp
   · exact Rci.pairwise_toList_upwardEnumerableLt
 
+public theorem nodup_toList [Least? α]
+    [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] :
+    (*...* : Std.Rii α).toList.Nodup := by
+  simpa [Internal.toList_eq_toList_iter] using Std.Rxi.Iterator.nodup_toList
+
 public theorem pairwise_toList_ne [Least? α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     [LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] :