chore: remove lean4checker from release repos (#13121)

Lean4checker has been merged into this repository and is no longer a
standalone repo.

.claude/CLAUDE.md

@@ -1,4 +1,6 @@
-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
 
@@ -6,13 +8,13 @@ See `doc/dev/testing.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)"
+make -j$(nproc) -C build/release test ARGS="-j$(nproc)"
 
 # Specific test by name (supports regex via ctest -R)
-make -j -C build/release test ARGS='-R grind_ematch --output-on-failure'
+make -j$(nproc) -C build/release test ARGS='-R grind_ematch --output-on-failure'
 
 # Rerun only previously failed tests
-make -j -C build/release test ARGS='--rerun-failed --output-on-failure'
+make -j$(nproc) -C build/release test ARGS='--rerun-failed --output-on-failure'
 
 # Single test from tests/lean/run/ (quick check during development)
 cd tests/lean/run && ./test_single.sh example_test.lean
@@ -41,7 +43,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 +61,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:
 ```

.claude/commands/release.md

@@ -121,6 +121,42 @@ The nightly build system uses branches and tags across two repositories:
 
 When a nightly succeeds with mathlib, all three should point to the same commit. Don't confuse these: branches are in the main lean4 repo, dated tags are in lean4-nightly.
 
+## CI Failures: Investigate Immediately
+
+**CRITICAL: If the checklist reports `❌ CI: X check(s) failing` for any PR, investigate immediately.**
+
+Do NOT:
+- Report it as "CI in progress" or "some checks pending"
+- Wait for the remaining checks to finish before investigating
+- Assume it's a transient failure without checking
+
+DO:
+1. Run `gh pr checks <number> --repo <owner>/<repo>` to see which specific check failed
+2. Run `gh run view <run-id> --repo <owner>/<repo> --log-failed` to see the failure output
+3. Diagnose the failure and report clearly to the user: what failed and why
+4. Propose a fix if one is obvious (e.g., subverso version mismatch, transient elan install error)
+
+The checklist now distinguishes `❌ X check(s) failing, Y still in progress` from `🔄 Y check(s) in progress`.
+Any `❌` in CI status requires immediate investigation — do not move on.
+
+## Waiting for CI or Merges
+
+Use `gh pr checks --watch` to block until a PR's CI checks complete (no polling needed).
+Run these as background bash commands so you get notified when they finish:
+
+```bash
+# Watch CI, then check merge state
+gh pr checks <number> --repo <owner>/<repo> --watch && gh pr view <number> --repo <owner>/<repo> --json state --jq '.state'
+```
+
+For multiple PRs, launch one background command per PR in parallel. When each completes,
+you'll be notified automatically via a task-notification. Do NOT use sleep-based polling
+loops — `--watch` is event-driven and exits as soon as checks finish.
+
+Note: `gh pr checks --watch` exits as soon as ALL checks complete (pass or fail). If some checks
+fail while others are still running, `--watch` will continue until everything settles, then exit
+with a non-zero code. So a background `--watch` finishing = all checks done; check which failed.
+
 ## Error Handling
 
 **CRITICAL**: If something goes wrong or a command fails:

.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
@@ -66,16 +66,10 @@ jobs:
           brew install ccache tree zstd coreutils gmp libuv
         if: runner.os == 'macOS'
       - name: Checkout
-        if: (!endsWith(matrix.os, '-with-cache'))
         uses: actions/checkout@v6
         with:
           # the default is to use a virtual merge commit between the PR and master: just use the PR
           ref: ${{ github.event.pull_request.head.sha }}
-      - name: Namespace Checkout
-        if: endsWith(matrix.os, '-with-cache')
-        uses: namespacelabs/nscloud-checkout-action@v8
-        with:
-          ref: ${{ github.event.pull_request.head.sha }}
       - name: Open Nix shell once
         run: true
         if: runner.os == 'Linux'

.github/workflows/ci.yml

@@ -163,6 +163,34 @@ jobs:
 
           echo "Version validation passed: $TAG_MAJOR.$TAG_MINOR.$TAG_PATCH"
 
+          # Also check stage0/src/CMakeLists.txt — the stage0 compiler stamps .olean
+          # headers with its baked-in version, so a mismatch produces .olean files
+          # with the wrong version in the release tarball.
+          STAGE0_MAJOR=$(grep -E "^set\(LEAN_VERSION_MAJOR " stage0/src/CMakeLists.txt | grep -oE '[0-9]+')
+          STAGE0_MINOR=$(grep -E "^set\(LEAN_VERSION_MINOR " stage0/src/CMakeLists.txt | grep -oE '[0-9]+')
+
+          STAGE0_ERRORS=""
+          if [[ "$STAGE0_MAJOR" != "$TAG_MAJOR" ]]; then
+            STAGE0_ERRORS+="LEAN_VERSION_MAJOR: expected $TAG_MAJOR, found $STAGE0_MAJOR\n"
+          fi
+          if [[ "$STAGE0_MINOR" != "$TAG_MINOR" ]]; then
+            STAGE0_ERRORS+="LEAN_VERSION_MINOR: expected $TAG_MINOR, found $STAGE0_MINOR\n"
+          fi
+
+          if [[ -n "$STAGE0_ERRORS" ]]; then
+            echo "::error::Version mismatch between tag and stage0/src/CMakeLists.txt"
+            echo ""
+            echo "Tag ${{ steps.set-release.outputs.RELEASE_TAG }} expects version $TAG_MAJOR.$TAG_MINOR.$TAG_PATCH"
+            echo "But stage0/src/CMakeLists.txt has mismatched values:"
+            echo -e "$STAGE0_ERRORS"
+            echo ""
+            echo "The stage0 compiler stamps .olean headers with its baked-in version."
+            echo "Run 'make update-stage0' to rebuild stage0 with the correct version, then re-tag."
+            exit 1
+          fi
+
+          echo "stage0 version validation passed: $STAGE0_MAJOR.$STAGE0_MINOR"
+
       # 0: PRs without special label
       # 1: PRs with `merge-ci` label, merge queue checks, master commits
       # 2: nightlies
@@ -275,8 +303,8 @@ jobs:
                 // Always run on large if available, more reliable regarding timeouts
                 "os": large ? "nscloud-ubuntu-22.04-amd64-16x32-with-cache" : "ubuntu-latest",
                 "enabled": level >= 2,
-                // do not fail nightlies on this for now
-                "secondary": level <= 2,
+                // do not fail releases/nightlies on this for now
+                "secondary": true,
                 "test": true,
                 // turn off custom allocator & symbolic functions to make LSAN do its magic
                 "CMAKE_PRESET": "sanitize",

.gitignore

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

CMakeLists.txt

@@ -70,13 +70,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})

script/release_checklist.py

@@ -11,7 +11,7 @@ IMPORTANT: Keep this documentation up-to-date when modifying the script's behavi
 What this script does:
 1. Validates preliminary Lean4 release infrastructure:
    - Checks that the release branch (releases/vX.Y.0) exists
-   - Verifies CMake version settings are correct
+   - Verifies CMake version settings are correct (both src/ and stage0/)
    - Confirms the release tag exists
    - Validates the release page exists on GitHub (created automatically by CI after tag push)
    - Checks the release notes page on lean-lang.org (updated while bumping the `reference-manual` repository)
@@ -326,6 +326,42 @@ def check_cmake_version(repo_url, branch, version_major, version_minor, github_t
     print(f"  ✅ CMake version settings are correct in {cmake_file_path}")
     return True
 
+def check_stage0_version(repo_url, branch, version_major, version_minor, github_token):
+    """Verify that stage0/src/CMakeLists.txt has the same version as src/CMakeLists.txt.
+
+    The stage0 pre-built binaries stamp .olean headers with their baked-in version.
+    If stage0 has a different version (e.g. from a 'begin development cycle' bump),
+    the release tarball will contain .olean files with the wrong version.
+    """
+    stage0_cmake = "stage0/src/CMakeLists.txt"
+    content = get_branch_content(repo_url, branch, stage0_cmake, github_token)
+    if content is None:
+        print(f"  ❌ Could not retrieve {stage0_cmake} from {branch}")
+        return False
+
+    errors = []
+    for line in content.splitlines():
+        stripped = line.strip()
+        if stripped.startswith("set(LEAN_VERSION_MAJOR "):
+            actual = stripped.split()[-1].rstrip(")")
+            if actual != str(version_major):
+                errors.append(f"LEAN_VERSION_MAJOR: expected {version_major}, found {actual}")
+        elif stripped.startswith("set(LEAN_VERSION_MINOR "):
+            actual = stripped.split()[-1].rstrip(")")
+            if actual != str(version_minor):
+                errors.append(f"LEAN_VERSION_MINOR: expected {version_minor}, found {actual}")
+
+    if errors:
+        print(f"  ❌ stage0 version mismatch in {stage0_cmake}:")
+        for error in errors:
+            print(f"     {error}")
+        print(f"     The stage0 compiler stamps .olean headers with its baked-in version.")
+        print(f"     Run `make update-stage0` to rebuild stage0 with the correct version.")
+        return False
+
+    print(f"  ✅ stage0 version matches in {stage0_cmake}")
+    return True
+
 def extract_org_repo_from_url(repo_url):
     """Extract the 'org/repo' part from a GitHub URL."""
     if repo_url.startswith("https://github.com/"):
@@ -441,7 +477,10 @@ def get_pr_ci_status(repo_url, pr_number, github_token):
     conclusions = [run['conclusion'] for run in check_runs if run.get('status') == 'completed']
     in_progress = [run for run in check_runs if run.get('status') in ['queued', 'in_progress']]
 
+    failed = sum(1 for c in conclusions if c in ['failure', 'timed_out', 'action_required'])
     if in_progress:
+        if failed > 0:
+            return "failure", f"{failed} check(s) failing, {len(in_progress)} still in progress"
         return "pending", f"{len(in_progress)} check(s) in progress"
 
     if not conclusions:
@@ -450,7 +489,6 @@ def get_pr_ci_status(repo_url, pr_number, github_token):
     if all(c == 'success' for c in conclusions):
         return "success", f"All {len(conclusions)} checks passed"
 
-    failed = sum(1 for c in conclusions if c in ['failure', 'timed_out', 'action_required'])
     if failed > 0:
         return "failure", f"{failed} check(s) failed"
 
@@ -680,6 +718,9 @@ def main():
         # Check CMake version settings
         if not check_cmake_version(lean_repo_url, branch_name, version_major, version_minor, github_token):
             lean4_success = False
+        # Check that stage0 version matches (stage0 stamps .olean headers with its version)
+        if not check_stage0_version(lean_repo_url, branch_name, version_major, version_minor, github_token):
+            lean4_success = False
 
     # Check for tag and release page
     if not tag_exists(lean_repo_url, toolchain, github_token):
@@ -924,8 +965,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}"
@@ -965,14 +1006,15 @@ def main():
         # Find the actual minor version in CMakeLists.txt
         for line in cmake_lines:
             if line.strip().startswith("set(LEAN_VERSION_MINOR "):
-                actual_minor = int(line.split()[-1].rstrip(")"))
+                m = re.search(r'set\(LEAN_VERSION_MINOR\s+(\d+)', line)
+                actual_minor = int(m.group(1)) if m else 0
                 version_minor_correct = actual_minor >= next_minor
                 break
         else:
             version_minor_correct = False
             
         is_release_correct = any(
-            l.strip().startswith("set(LEAN_VERSION_IS_RELEASE 0)") 
+            re.match(r'set\(LEAN_VERSION_IS_RELEASE\s+0[\s)]', l.strip())
             for l in cmake_lines
         )
         

script/release_repos.yml

@@ -14,13 +14,6 @@ repositories:
     bump-branch: true
     dependencies: []
 
-  - name: lean4checker
-    url: https://github.com/leanprover/lean4checker
-    toolchain-tag: true
-    stable-branch: true
-    branch: master
-    dependencies: []
-
   - name: quote4
     url: https://github.com/leanprover-community/quote4
     toolchain-tag: true

script/release_steps.py

@@ -479,6 +479,25 @@ def execute_release_steps(repo, version, config):
         print(blue("Updating lakefile.toml..."))
         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)
+    elif repo_name == "verso":
+        # verso has nested Lake projects in test-projects/ that each have their own
+        # lake-manifest.json with a subverso pin. After updating the root manifest via
+        # `lake update`, sync the de-modulized subverso rev into all sub-manifests.
+        # The sub-projects use an old toolchain (v4.21.0) that doesn't support module/prelude
+        # syntax, so they need the de-modulized version (tagged no-modules/<root-rev>).
+        # The "SubVerso version consistency" CI check accepts either the root or de-modulized rev.
+        run_command("lake update", cwd=repo_path, stream_output=True)
+        print(blue("Syncing de-modulized subverso rev to test-project sub-manifests..."))
+        sync_script = (
+            'ROOT_REV=$(jq -r \'.packages[] | select(.name == "subverso") | .rev\' lake-manifest.json); '
+            'SUBVERSO_URL=$(jq -r \'.packages[] | select(.name == "subverso") | .url\' lake-manifest.json); '
+            'DEMOD_REV=$(git ls-remote "$SUBVERSO_URL" "refs/tags/no-modules/$ROOT_REV" | awk \'{print $1}\'); '
+            'find test-projects -name lake-manifest.json -print0 | while IFS= read -r -d \'\' f; do '
+            'jq --arg rev "$DEMOD_REV" \'.packages |= map(if .name == "subverso" then .rev = $rev else . end)\' "$f" > /tmp/lm_tmp.json && mv /tmp/lm_tmp.json "$f"; '
+            'done'
+        )
+        run_command(sync_script, cwd=repo_path)
+        print(green("Synced de-modulized subverso rev to all test-project sub-manifests"))
     elif dependencies:
         run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path)
         run_command("lake update", cwd=repo_path, stream_output=True)

src/CMakeLists.txt

@@ -10,9 +10,9 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 30)
+set(LEAN_VERSION_MINOR 29)
 set(LEAN_VERSION_PATCH 0)
-set(LEAN_VERSION_IS_RELEASE 0) # This number is 1 in the release revision, and 0 otherwise.
+set(LEAN_VERSION_IS_RELEASE 1) # 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'")
 set(LEAN_VERSION_STRING "${LEAN_VERSION_MAJOR}.${LEAN_VERSION_MINOR}.${LEAN_VERSION_PATCH}")
 if(LEAN_SPECIAL_VERSION_DESC)

src/Init/Classical.lean

@@ -69,9 +69,11 @@ theorem em (p : Prop) : p ∨ ¬p :=
 theorem exists_true_of_nonempty {α : Sort u} : Nonempty α → ∃ _ : α, True
   | ⟨x⟩ => ⟨x, trivial⟩
 
+@[implicit_reducible]
 noncomputable def inhabited_of_nonempty {α : Sort u} (h : Nonempty α) : Inhabited α :=
   ⟨choice h⟩
 
+@[implicit_reducible]
 noncomputable def inhabited_of_exists {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : Inhabited α :=
   inhabited_of_nonempty (Exists.elim h (fun w _ => ⟨w⟩))
 
@@ -81,6 +83,7 @@ noncomputable scoped instance (priority := low) propDecidable (a : Prop) : Decid
     | Or.inl h => ⟨isTrue h⟩
     | Or.inr h => ⟨isFalse h⟩
 
+@[implicit_reducible]
 noncomputable def decidableInhabited (a : Prop) : Inhabited (Decidable a) where
   default := inferInstance
 
@@ -142,7 +145,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

@@ -49,6 +49,7 @@ instance : Monad Id where
 /--
 The identity monad has a `bind` operator.
 -/
+@[implicit_reducible]
 def hasBind : Bind Id :=
   inferInstance
 
@@ -58,7 +59,7 @@ Runs a computation in the identity monad.
 This function is the identity function. Because its parameter has type `Id α`, it causes
 `do`-notation in its arguments to use the `Monad Id` instance.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline, expose, implicit_reducible]
 protected def run (x : Id α) : α := x
 
 instance [OfNat α n] : OfNat (Id α) n :=
@@ -79,3 +80,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

@@ -258,7 +258,6 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (OptionT m) where
   rw [← bind_pure_comp]
   rfl
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp] theorem run_controlAt [Monad m] [LawfulMonad m] (f : ({β : Type u} → OptionT m β → m (stM m (OptionT m) β)) → m (stM m (OptionT m) α)) :
     OptionT.run (controlAt m f) = f fun x => x.run := by
   simp [controlAt, Option.elimM, Option.elim]
@@ -346,7 +345,6 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (ReaderT ρ m) where
     ReaderT.run (liftWith f) ctx = (f fun x => x.run ctx) :=
   rfl
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp] theorem run_controlAt [Monad m] [LawfulMonad m] (f : ({β : Type u} → ReaderT ρ m β → m (stM m (ReaderT ρ m) β)) → m (stM m (ReaderT ρ m) α)) (ctx : ρ) :
     ReaderT.run (controlAt m f) ctx = f fun x => x.run ctx := by
   simp [controlAt]
@@ -441,13 +439,11 @@ 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
   simp [liftWith, MonadControl.liftWith, Function.comp_def]
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp] theorem run_controlAt [Monad m] [LawfulMonad m] (f : ({β : Type u} → StateT σ m β → m (stM m (StateT σ m) β)) → m (stM m (StateT σ m) α)) (s : σ) :
     StateT.run (controlAt m f) s = f fun x => x.run s := by
   simp [controlAt]

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

@@ -72,11 +72,11 @@ public instance [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m]
 
 public instance [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] :
     WeaklyLawfulMonadAttach (StateRefT' ω σ m) :=
-  inferInstanceAs (WeaklyLawfulMonadAttach (ReaderT _ _))
+  inferInstanceAs (WeaklyLawfulMonadAttach (ReaderT (ST.Ref ω σ) m))
 
 public instance [Monad m] [MonadAttach m] [LawfulMonad m] [LawfulMonadAttach m] :
     LawfulMonadAttach (StateRefT' ω σ m) :=
-  inferInstanceAs (LawfulMonadAttach (ReaderT _ _))
+  inferInstanceAs (LawfulMonadAttach (ReaderT (ST.Ref ω σ) m))
 
 section
 

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

@@ -103,11 +103,11 @@ namespace StateRefT'
 instance {ω σ : Type} {m : Type → Type} [Monad m] : LawfulMonadLift m (StateRefT' ω σ m) where
   monadLift_pure _ := by
     simp only [MonadLift.monadLift, pure]
-    unfold StateRefT'.lift ReaderT.pure
+    unfold StateRefT'.lift instMonad._aux_5 ReaderT.pure
     simp only
   monadLift_bind _ _ := by
     simp only [MonadLift.monadLift, bind]
-    unfold StateRefT'.lift ReaderT.bind
+    unfold StateRefT'.lift instMonad._aux_13 ReaderT.bind
     simp only
 
 end StateRefT'

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/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
@@ -93,7 +94,7 @@ theorem ext' {xs ys : Array α} (h : xs.toList = ys.toList) : xs = ys := by
 
 @[simp, grind =] theorem getElem?_toList {xs : Array α} {i : Nat} : xs.toList[i]? = xs[i]? := by
   simp only [getElem?_def, getElem_toList]
-  simp only [Array.size]; rfl
+  simp only [Array.size]
 
 /-- `a ∈ as` is a predicate which asserts that `a` is in the array `as`. -/
 -- NB: This is defined as a structure rather than a plain def so that a lemma
@@ -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/Find.lean

@@ -723,7 +723,6 @@ theorem findFinIdx?_eq_bind_find?_finIdxOf? [BEq α] [LawfulBEq α] {xs : Array
     xs.findFinIdx? p = (xs.find? p).bind (xs.finIdxOf? ·) := by
   cases xs
   simp [List.findFinIdx?_eq_bind_find?_finIdxOf?]
-  rfl
 
 theorem findIdx_eq_getD_bind_find?_idxOf? [BEq α] [LawfulBEq α] {xs : Array α} {p : α → Bool} :
     xs.findIdx p = ((xs.find? p).bind (xs.idxOf? ·)).getD xs.size := by

src/Init/Data/Array/Lemmas.lean

@@ -896,7 +896,7 @@ theorem all_push {xs : Array α} {a : α} {p : α → Bool} :
 @[simp] theorem getElem_set_ne {xs : Array α} {i : Nat} (h' : i < xs.size) {v : α} {j : Nat}
     (pj : j < xs.size) (h : i ≠ j) :
     (xs.set i v)[j]'(by simp [*]) = xs[j] := by
-  simp only [set, ← getElem_toList, List.getElem_set_ne h]; rfl
+  simp only [set, ← getElem_toList, List.getElem_set_ne h]
 
 @[simp] theorem getElem?_set_ne {xs : Array α} {i : Nat} (h : i < xs.size) {v : α} {j : Nat}
     (ne : i ≠ j) : (xs.set i v)[j]? = xs[j]? := by
@@ -2855,7 +2855,7 @@ theorem getElem?_extract {xs : Array α} {start stop : Nat} :
   · simp only [length_toList, size_extract, List.length_take, List.length_drop]
     omega
   · intro n h₁ h₂
-    simp; rfl
+    simp
 
 @[simp] theorem extract_size {xs : Array α} : xs.extract 0 xs.size = xs := by
   apply ext

src/Init/Data/Array/MapIdx.lean

@@ -72,7 +72,6 @@ theorem mapFinIdx_spec {xs : Array α} {f : (i : Nat) → α → (h : i < xs.siz
   simp only [getElem?_def, size_mapFinIdx, getElem_mapFinIdx]
   split <;> simp_all
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp, grind =] theorem toList_mapFinIdx {xs : Array α} {f : (i : Nat) → α → (h : i < xs.size) → β} :
     (xs.mapFinIdx f).toList = xs.toList.mapFinIdx (fun i a h => f i a (by simpa)) := by
   apply List.ext_getElem <;> simp
@@ -106,7 +105,6 @@ theorem mapIdx_spec {f : Nat → α → β} {xs : Array α}
       xs[i]?.map (f i) := by
   simp [getElem?_def, size_mapIdx, getElem_mapIdx]
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp, grind =] theorem toList_mapIdx {f : Nat → α → β} {xs : Array α} :
     (xs.mapIdx f).toList = xs.toList.mapIdx (fun i a => f i a) := by
   apply List.ext_getElem <;> simp

src/Init/Data/Array/OfFn.lean

@@ -41,7 +41,6 @@ theorem ofFn_succ {f : Fin (n+1) → α} :
     intro h₃
     simp only [show i = n by omega]
 
-set_option backward.isDefEq.respectTransparency false in
 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
@@ -108,7 +107,6 @@ theorem ofFnM_succ {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} :
       pure (as.push a)) := by
   simp [ofFnM, Fin.foldlM_succ_last]
 
-set_option backward.isDefEq.respectTransparency false in
 theorem ofFnM_add {n m} [Monad m] [LawfulMonad m] {f : Fin (n + k) → m α} :
     ofFnM f = (do
       let as ← ofFnM fun i : Fin n => f (i.castLE (Nat.le_add_right n k))

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/Lemmas.lean

@@ -1198,7 +1198,7 @@ let x' = x.extractLsb' 7 5  =   _ _ 9 8 7
       (decide (0 < len) &&
       (decide (start + len ≤ w) &&
       x.getMsbD (w - (start + len)))) := by
-  simp [BitVec.msb, getMsbD_extractLsb']; rfl
+  simp [BitVec.msb, getMsbD_extractLsb']
 
 @[simp, grind =] theorem getElem_extract {hi lo : Nat} {x : BitVec n} {i : Nat} (h : i < hi - lo + 1) :
     (extractLsb hi lo x)[i] = getLsbD x (lo+i) := by
@@ -1234,7 +1234,7 @@ let x' = x.extractLsb' 7 5  =   _ _ 9 8 7
 
 @[simp, grind =] theorem msb_extractLsb {hi lo : Nat} {x : BitVec w} :
     (extractLsb hi lo x).msb = (decide (max hi lo < w) && x.getMsbD (w - 1 - max hi lo)) := by
-  simp [BitVec.msb]; rfl
+  simp [BitVec.msb]
 
 theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h : len > 0) :
     x.extractLsb' start len = (x.extractLsb (len - 1 + start) start).cast (by omega) := by
@@ -2784,9 +2784,8 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
 @[simp] theorem append_zero_width (x : BitVec w) (y : BitVec 0) : x ++ y = x := by
   ext i ih
   rw [getElem_append] -- Why does this not work with `simp [getElem_append]`?
-  simp; rfl
+  simp
 
-set_option backward.isDefEq.respectTransparency false in
 @[grind =]
 theorem toInt_append {x : BitVec n} {y : BitVec m} :
     (x ++ y).toInt = if n == 0 then y.toInt else (2 ^ m) * x.toInt + y.toNat := by
@@ -5292,7 +5291,6 @@ theorem and_one_eq_setWidth_ofBool_getLsbD {x : BitVec w} :
 theorem replicate_zero {x : BitVec w} : x.replicate 0 = 0#0 := by
   simp [replicate]
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp, grind =]
 theorem replicate_one {w : Nat} {x : BitVec w} :
     (x.replicate 1) = x.cast (by rw [Nat.mul_one]) := by
@@ -5344,7 +5342,6 @@ theorem append_assoc {x₁ : BitVec w₁} {x₂ : BitVec w₂} {x₃ : BitVec w
 theorem append_assoc' {x₁ : BitVec w₁} {x₂ : BitVec w₂} {x₃ : BitVec w₃} :
     (x₁ ++ (x₂ ++ x₃)) = ((x₁ ++ x₂) ++ x₃).cast (by omega) := by simp [append_assoc]
 
-set_option backward.isDefEq.respectTransparency false in
 theorem replicate_append_self {x : BitVec w} :
     x ++ x.replicate n = (x.replicate n ++ x).cast (by omega) := by
   induction n with

src/Init/Data/Bool.lean

@@ -629,6 +629,7 @@ export Bool (cond_eq_if cond_eq_ite xor and or not)
 This should not be turned on globally as an instance because it degrades performance in Mathlib,
 but may be used locally.
 -/
+@[implicit_reducible]
 def boolPredToPred : Coe (α → Bool) (α  → Prop) where
   coe r := fun a => Eq (r a) true
 
@@ -636,7 +637,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/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₁)
 
@@ -62,7 +62,7 @@ instance ltTrichotomous : Std.Trichotomous (· < · : Char → Char → Prop) wh
   trichotomous _ _ h₁ h₂ := Char.le_antisymm (by simpa using h₂) (by simpa using h₁)
 
 @[deprecated ltTrichotomous (since := "2025-10-27")]
-def notLTAntisymm : Std.Antisymm (¬ · < · : Char → Char → Prop) where
+theorem notLTAntisymm : Std.Antisymm (¬ · < · : Char → Char → Prop) where
   antisymm := Char.ltTrichotomous.trichotomous
 
 instance ltAsymm : Std.Asymm (· < · : Char → Char → Prop) where
@@ -73,7 +73,7 @@ instance leTotal : Std.Total (· ≤ · : Char → Char → Prop) where
 
 -- This instance is useful while setting up instances for `String`.
 @[deprecated ltAsymm (since := "2025-08-01")]
-def notLTTotal : Std.Total (¬ · < · : Char → Char → Prop) where
+theorem notLTTotal : Std.Total (¬ · < · : Char → Char → Prop) where
   total := fun x y => by simpa using Char.le_total y x
 
 @[simp] theorem ofNat_toNat (c : Char) : Char.ofNat c.toNat = c := by

src/Init/Data/Fin/Fold.lean

@@ -164,7 +164,7 @@ theorem foldlM_add [Monad m] [LawfulMonad m] (f : α → Fin (n + k) → m α) :
     simp
   | succ k ih =>
     funext x
-    simp [foldlM_succ_last, ← Nat.add_assoc, ih]; rfl
+    simp [foldlM_succ_last, ← Nat.add_assoc, ih]
 
 /-! ### foldrM -/
 
@@ -222,7 +222,7 @@ theorem foldrM_add [Monad m] [LawfulMonad m] (f : Fin (n + k) → α → m α) :
     simp
   | succ k ih =>
     funext x
-    simp [foldrM_succ_last, ← Nat.add_assoc, ih]; rfl
+    simp [foldrM_succ_last, ← Nat.add_assoc, ih]
 
 /-! ### foldl -/
 
@@ -268,7 +268,7 @@ theorem foldl_add (f : α → Fin (n + m) → α) (x) :
         (foldl n (fun x i => f x (i.castLE (Nat.le_add_right n m))) x):= by
   induction m with
   | zero => simp
-  | succ m ih => simp [foldl_succ_last, ih, ← Nat.add_assoc]; rfl
+  | succ m ih => simp [foldl_succ_last, ih, ← Nat.add_assoc]
 
 theorem foldl_eq_foldlM (f : α → Fin n → α) (x) :
     foldl n f x = (foldlM (m := Id) n (pure <| f · ·) x).run := by
@@ -321,7 +321,7 @@ theorem foldr_add (f : Fin (n + m) → α → α) (x) :
         (foldr m (fun i => f (i.natAdd n)) x) := by
   induction m generalizing x with
   | zero => simp
-  | succ m ih => simp [foldr_succ_last, ih, ← Nat.add_assoc]; rfl
+  | succ m ih => simp [foldr_succ_last, ih, ← Nat.add_assoc]
 
 theorem foldr_eq_foldrM (f : Fin n → α → α) (x) :
     foldr n f x = (foldrM (m := Id) n (pure <| f · ·) x).run := by

src/Init/Data/Fin/Iterate.lean

@@ -69,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

@@ -123,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
 
@@ -145,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
 

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/Combinators/Monadic/FilterMap.lean

@@ -168,6 +168,13 @@ instance Map.instIterator {α β γ : Type w} {m : Type w → Type w'} {n : Type
     Iterator (Map α m n lift f) n γ :=
   inferInstanceAs <| Iterator (FilterMap α m n lift _) n γ
 
+theorem Map.instIterator_eq_filterMapInstIterator {α β γ : Type w} {m : Type w → Type w'}
+    {n : Type w → Type w''} [Monad n]
+    [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n γ} :
+    Map.instIterator (α := α) (β := β) (γ := γ) (m := m) (n := n) (lift := lift) (f := f) =
+      FilterMap.instIterator :=
+  rfl
+
 private def FilterMap.instFinitenessRelation {α β γ : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α}
     {f : β → PostconditionT n (Option γ)} [Finite α m] :

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

@@ -362,8 +362,7 @@ def Flatten.instProductivenessRelation [Monad m] [Iterator α m (IterM (α := α
     case innerDone =>
       apply Flatten.productiveRel_of_right₂
 
-@[no_expose]
-public def Flatten.instProductive [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
+public theorem Flatten.instProductive [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
     [Finite α m] [Productive α₂ m] : Productive (Flatten α α₂ β m) m :=
   .of_productivenessRelation instProductivenessRelation
 

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

@@ -35,7 +35,7 @@ A `ForIn'` instance for iterators. Its generic membership relation is not easy t
 so this is not marked as `instance`. This way, more convenient instances can be built on top of it
 or future library improvements will make it more comfortable.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose, implicit_reducible]
 def Iter.instForIn' {α : Type w} {β : Type w} {n : Type x → Type x'} [Monad n]
     [Iterator α Id β] [IteratorLoop α Id n] :
     ForIn' n (Iter (α := α) β) β ⟨fun it out => it.IsPlausibleIndirectOutput out⟩ where
@@ -53,7 +53,7 @@ instance (α : Type w) (β : Type w) (n : Type x → Type x') [Monad n]
 /--
 An implementation of `for h : ... in ... do ...` notation for partial iterators.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose, implicit_reducible]
 def Iter.Partial.instForIn' {α : Type w} {β : Type w} {n : Type x → Type x'} [Monad n]
     [Iterator α Id β] [IteratorLoop α Id n] :
     ForIn' n (Iter.Partial (α := α) β) β ⟨fun it out => it.it.IsPlausibleIndirectOutput out⟩ where
@@ -71,7 +71,7 @@ instance (α : Type w) (β : Type w) (n : Type x → Type x') [Monad n]
 A `ForIn'` instance for iterators that is guaranteed to terminate after finitely many steps.
 It is not marked as an instance because the membership predicate is difficult to work with.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose, implicit_reducible]
 def Iter.Total.instForIn' {α : Type w} {β : Type w} {n : Type x → Type x'} [Monad n]
     [Iterator α Id β] [IteratorLoop α Id n] [Finite α Id] :
     ForIn' n (Iter.Total (α := α) β) β ⟨fun it out => it.it.IsPlausibleIndirectOutput out⟩ where

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

@@ -159,7 +159,7 @@ This is the default implementation of the `IteratorLoop` class.
 It simply iterates through the iterator using `IterM.step`. For certain iterators, more efficient
 implementations are possible and should be used instead.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline, expose, implicit_reducible]
 def IteratorLoop.defaultImplementation {α : Type w} {m : Type w → Type w'} {n : Type x → Type x'}
     [Monad n] [Iterator α m β] :
     IteratorLoop α m n where
@@ -211,7 +211,7 @@ theorem IteratorLoop.wellFounded_of_productive {α β : Type w} {m : Type w →
 /--
 This `ForIn'`-style loop construct traverses a finite iterator using an `IteratorLoop` instance.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose, implicit_reducible]
 def IteratorLoop.finiteForIn' {m : Type w → Type w'} {n : Type x → Type x'}
     {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoop α m n] [Monad n]
     (lift : ∀ γ δ, (γ → n δ) → m γ → n δ) :
@@ -224,7 +224,7 @@ A `ForIn'` instance for iterators. Its generic membership relation is not easy t
 so this is not marked as `instance`. This way, more convenient instances can be built on top of it
 or future library improvements will make it more comfortable.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose, implicit_reducible]
 def IterM.instForIn' {m : Type w → Type w'} {n : Type w → Type w''}
     {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoop α m n] [Monad n]
     [MonadLiftT m n] :
@@ -239,7 +239,7 @@ instance IterM.instForInOfIteratorLoop {m : Type w → Type w'} {n : Type w →
   instForInOfForIn'
 
 /-- Internal implementation detail of the iterator library. -/
-@[always_inline, inline]
+@[always_inline, inline, expose, implicit_reducible]
 def IterM.Partial.instForIn' {m : Type w → Type w'} {n : Type w → Type w''}
     {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] [Monad n] :
     ForIn' n (IterM.Partial (α := α) m β) β ⟨fun it out => it.it.IsPlausibleIndirectOutput out⟩ where
@@ -247,7 +247,7 @@ def IterM.Partial.instForIn' {m : Type w → Type w'} {n : Type w → Type w''}
     haveI := @IterM.instForIn'; forIn' it.it init f
 
 /-- Internal implementation detail of the iterator library. -/
-@[always_inline, inline]
+@[always_inline, inline, expose, implicit_reducible]
 def IterM.Total.instForIn' {m : Type w → Type w'} {n : Type w → Type w''}
     {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] [Monad n]
     [Finite α m] :

src/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.lean

@@ -70,7 +70,7 @@ theorem LawfulMonadLiftFunction.lift_seqRight [LawfulMonad m] [LawfulMonad n]
 abbrev idToMonad [Monad m] ⦃α : Type u⦄ (x : Id α) : m α :=
     pure x.run
 
-def LawfulMonadLiftFunction.idToMonad [Monad m] [LawfulMonad m] :
+theorem LawfulMonadLiftFunction.idToMonad [LawfulMonad m] :
     LawfulMonadLiftFunction (m := Id) (n := m) idToMonad where
   lift_pure := by simp [Internal.idToMonad]
   lift_bind := by simp [Internal.idToMonad]
@@ -95,7 +95,7 @@ instance [LawfulMonadLiftBindFunction (n := n) (fun _ _ f x => lift x >>= f)] [L
     simpa using LawfulMonadLiftBindFunction.liftBind_bind (n := n)
       (liftBind := fun _ _ f x => lift x >>= f) (β := β) (γ := γ) (δ := γ) pure x g
 
-def LawfulMonadLiftBindFunction.id [Monad m] [LawfulMonad m] :
+theorem LawfulMonadLiftBindFunction.id [LawfulMonad m] :
     LawfulMonadLiftBindFunction (m := Id) (n := m) (fun _ _ f x => f x.run) where
   liftBind_pure := by simp
   liftBind_bind := by simp

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

@@ -750,7 +750,6 @@ theorem Iter.anyM_filterMapM {α β β' : Type w} {m : Type w → Type w'}
   simp only [filterMapM_eq_toIter_filterMapM_toIterM, IterM.anyM_filterMapM]
   rfl
 
-set_option backward.isDefEq.respectTransparency false in
 -- There is hope to generalize the following theorem as soon there is a `Shrink` type.
 /--
 This lemma expresses `Iter.anyM` in terms of `IterM.anyM`.
@@ -766,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
@@ -778,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/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,
@@ -700,18 +702,16 @@ theorem IterM.toList_map {α β β' : Type w} {m : Type w → Type w'} [Monad m]
     (it : IterM (α := α) m β) :
     (it.map f).toList = (fun x => x.map f) <$> it.toList := by
   rw [← List.filterMap_eq_map, ← toList_filterMap]
-  let t := type_of% (it.map f)
-  let t' := type_of% (it.filterMap (some ∘ f))
+  simp only [map, mapWithPostcondition, InternalCombinators.map, filterMap,
+    filterMapWithPostcondition, InternalCombinators.filterMap]
+  unfold Map
   congr
-  · simp [Map]
-  · simp [Map.instIterator, inferInstanceAs]
+  · simp
+  · rw [Map.instIterator_eq_filterMapInstIterator]
     congr
     simp
-  · simp only [map, mapWithPostcondition, InternalCombinators.map, Function.comp_apply, filterMap,
-    filterMapWithPostcondition, InternalCombinators.filterMap]
-    congr
-    · simp [Map]
-    · simp
+  · simp
+  · simp
 
 @[simp]
 theorem IterM.toList_filter {α : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m]

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

@@ -26,7 +26,6 @@ theorem Iter.uLift_eq_toIter_uLift_toIterM {it : Iter (α := α) β} :
     it.uLift = (it.toIterM.uLift Id).toIter :=
   rfl
 
-set_option backward.isDefEq.respectTransparency false in
 theorem Iter.step_uLift [Iterator α Id β] {it : Iter (α := α) β} :
     it.uLift.step = match it.step with
       | .yield it' out h => .yield it'.uLift (.up out) ⟨_, h, rfl⟩
@@ -39,12 +38,11 @@ theorem Iter.step_uLift [Iterator α Id β] {it : Iter (α := α) β} :
     PlausibleIterStep.done, pure_bind]
   cases it.toIterM.step.run.inflate using PlausibleIterStep.casesOn <;> simp
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 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]
 
@@ -61,12 +59,11 @@ theorem Iter.toArray_uLift [Iterator α Id β] {it : Iter (α := α) β}
   rw [← toArray_toList, ← toArray_toList, toList_uLift]
   simp [-toArray_toList]
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 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

@@ -32,7 +32,7 @@ theorem Iter.forIn'_eq {α β : Type w} [Iterator α Id β] [Finite α Id]
       IterM.DefaultConsumers.forIn' (n := m) (fun _ _ f x => f x.run) γ (fun _ _ _ => True)
         it.toIterM init _ (fun _ => id)
           (fun out h acc => return ⟨← f out (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc, trivial⟩) := by
-  simp +instances only [instForIn', ForIn'.forIn', IteratorLoop.finiteForIn']
+  simp +instances only [ForIn'.forIn']
   have : ∀ a b c, f a b c = (Subtype.val <$> (⟨·, trivial⟩) <$> f a b c) := by simp
   simp +singlePass only [this]
   rw [hl.lawful (fun _ _ f x => f x.run) (wf := IteratorLoop.wellFounded_of_finite)]
@@ -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]
@@ -82,7 +81,7 @@ theorem Iter.forIn'_eq_forIn'_toIterM {α β : Type w} [Iterator α Id β]
       letI : ForIn' m (IterM (α := α) Id β) β _ := IterM.instForIn'
       ForIn'.forIn' it.toIterM init
         (fun out h acc => f out (isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc) := by
-  simp +instances [ForIn'.forIn', Iter.instForIn', IterM.instForIn', monadLift]
+  simp +instances [ForIn'.forIn', monadLift]
 
 theorem Iter.forIn_eq_forIn_toIterM {α β : Type w} [Iterator α Id β]
     [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad 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]; rfl
+  rw [fold_eq_foldM, foldM_eq_foldM_toIterM, IterM.fold_eq_foldM]
 
 @[simp]
 theorem Iter.forIn_pure_yield_eq_fold {α β : Type w} {γ : Type x} [Iterator α Id β]

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

@@ -109,7 +109,7 @@ theorem IterM.forIn'_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m
     letI : ForIn' n (IterM (α := α) m β) β _ := IterM.instForIn'
     ForIn'.forIn' (α := β) (m := n) it init f = IterM.DefaultConsumers.forIn' (n := n)
         (fun _ _ f x => monadLift x >>= f) γ (fun _ _ _ => True) it init _ (fun _ => id) (return ⟨← f · · ·, trivial⟩) := by
-  simp +instances only [instForIn', ForIn'.forIn', IteratorLoop.finiteForIn']
+  simp +instances only [ForIn'.forIn']
   have : f = (Subtype.val <$> (⟨·, trivial⟩) <$> f · · ·) := by simp
   rw [this, hl.lawful (fun _ _ f x => monadLift x >>= f) (wf := IteratorLoop.wellFounded_of_finite)]
   simp +instances [IteratorLoop.defaultImplementation]

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

@@ -23,7 +23,6 @@ open Std Std.Iterators
 
 variable {β : Type w}
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem List.step_iter_nil :
     (([] : List β).iter).step = ⟨.done, rfl⟩ := by
@@ -32,7 +31,7 @@ theorem List.step_iter_nil :
 @[simp]
 theorem List.step_iter_cons {x : β} {xs : List β} :
     ((x :: xs).iter).step = ⟨.yield xs.iter x, rfl⟩ := by
-  simp [List.iter, List.iterM, IterM.toIter, Iter.step_eq]; rfl
+  simp [List.iter, List.iterM, IterM.toIter, Iter.step_eq]
 
 @[simp, grind =]
 theorem List.toArray_iter {l : List β} :

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

@@ -31,7 +31,7 @@ theorem List.step_iterM_nil :
 @[simp]
 theorem List.step_iterM_cons {x : β} {xs : List β} :
     ((x :: xs).iterM m).step = pure (.deflate ⟨.yield (xs.iterM m) x, rfl⟩) := by
-  simp only [List.iterM, IterM.step, Iterator.step]; rfl
+  simp only [List.iterM, IterM.step, Iterator.step]
 
 theorem List.step_iterM {l : List β} :
     (l.iterM m).step = match l with

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, implicit_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, implicit_reducible]
 def ToIterator.of (α : Type w)
     (iter : γ → Iter (α := α) β) :
     ToIterator γ Id α β where

src/Init/Data/List/Lemmas.lean

@@ -236,7 +236,6 @@ theorem getElem?_eq_some_iff {l : List α} : l[i]? = some a ↔ ∃ h : i < l.le
     · match i, h with
       | i + 1, h => simp [getElem?_eq_some_iff, Nat.succ_lt_succ_iff]
 
-@[grind →]
 theorem getElem_of_getElem? {l : List α} : l[i]? = some a → ∃ h : i < l.length, l[i] = a :=
   getElem?_eq_some_iff.mp
 
@@ -3525,7 +3524,7 @@ theorem getElem?_insert_succ {l : List α} {a : α} {i : Nat} :
   · split
     · rfl
     · have h' : i - 1 < l.length := Nat.lt_of_le_of_lt (Nat.pred_le _) h
-      simp [h']; rfl
+      simp [h']
 
 theorem head?_insert {l : List α} {a : α} :
     (l.insert a).head? = some (if h : a ∈ l then l.head (ne_nil_of_mem h) else a) := by

src/Init/Data/List/MapIdx.lean

@@ -350,7 +350,6 @@ theorem getElem?_mapIdx_go : ∀ {l : List α} {acc : Array β} {i : Nat},
   | [], acc, i => by
     simp only [mapIdx.go, getElem?_def, Array.length_toList,
       ← Array.getElem_toList, length_nil, Nat.not_lt_zero, ↓reduceDIte, Option.map_none]
-    rfl
   | a :: l, acc, i => by
     rw [mapIdx.go, getElem?_mapIdx_go]
     simp only [Array.size_push]

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
@@ -410,10 +418,10 @@ private theorem minIdxOn_append_aux [LE β] [DecidableLE β]
     match xs with
     | [] => simp [minIdxOn_cons_aux (xs := ys) ‹_›]
     | z :: zs =>
-      set_option backward.isDefEq.respectTransparency false in
       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 ≠ []) :
@@ -473,13 +481,13 @@ protected theorem maxIdxOn_nil_eq_iff_false [LE β] [DecidableLE β] {f : α →
 @[simp]
 protected theorem maxIdxOn_singleton [LE β] [DecidableLE β] {x : α} {f : α → β} :
     [x].maxIdxOn f (of_decide_eq_false rfl) = 0 :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.minIdxOn_singleton
 
 @[simp]
 protected theorem maxIdxOn_lt_length [LE β] [DecidableLE β] {f : α → β} {xs : List α}
     (h : xs ≠ []) : xs.maxIdxOn f h < xs.length :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.minIdxOn_lt_length h
 
 protected theorem maxIdxOn_le_of_apply_getElem_le_apply_maxOn [LE β] [DecidableLE β] [IsLinearPreorder β]
@@ -487,7 +495,7 @@ protected theorem maxIdxOn_le_of_apply_getElem_le_apply_maxOn [LE β] [Decidable
     {k : Nat} (hi : k < xs.length) (hle : f (xs.maxOn f h) ≤ f xs[k]) :
     xs.maxIdxOn f h ≤ k := by
   simp only [List.maxIdxOn_eq_minIdxOn, List.maxOn_eq_minOn] at hle ⊢
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   exact List.minIdxOn_le_of_apply_getElem_le_apply_minOn h hi (by simpa [LE.le_opposite_iff] using hle)
 
 protected theorem apply_maxOn_lt_apply_getElem_of_lt_maxIdxOn [LE β] [DecidableLE β] [LT β] [IsLinearPreorder β]
@@ -505,7 +513,7 @@ protected theorem getElem_maxIdxOn [LE β] [DecidableLE β] [IsLinearPreorder β
     {f : α → β} {xs : List α} (h : xs ≠ []) :
     xs[xs.maxIdxOn f h] = xs.maxOn f h := by
   simp only [List.maxIdxOn_eq_minIdxOn, List.maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   exact List.getElem_minIdxOn h
 
 protected theorem le_maxIdxOn_of_apply_getElem_lt_apply_getElem [LE β] [DecidableLE β] [LT β]
@@ -554,14 +562,14 @@ protected theorem maxIdxOn_cons
       else if f (xs.maxOn f h) ≤ f x then 0
       else (xs.maxIdxOn f h) + 1 := by
   simp only [List.maxIdxOn_eq_minIdxOn, List.maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa [LE.le_opposite_iff] using List.minIdxOn_cons (f := f)
 
 protected theorem maxIdxOn_eq_zero_iff [LE β] [DecidableLE β] [IsLinearPreorder β]
     {xs : List α} {f : α → β} (h : xs ≠ []) :
     xs.maxIdxOn f h = 0 ↔ ∀ x ∈ xs, f x ≤ f (xs.head h) := by
   simp only [List.maxIdxOn_eq_minIdxOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa [LE.le_opposite_iff] using List.minIdxOn_eq_zero_iff h (f := f)
 
 protected theorem maxIdxOn_append [LE β] [DecidableLE β] [IsLinearPreorder β]
@@ -572,26 +580,26 @@ protected theorem maxIdxOn_append [LE β] [DecidableLE β] [IsLinearPreorder β]
       else
         xs.length + ys.maxIdxOn f hys := by
   simp only [List.maxIdxOn_eq_minIdxOn, List.maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa [LE.le_opposite_iff] using List.minIdxOn_append hxs hys (f := f)
 
 protected theorem left_le_maxIdxOn_append [LE β] [DecidableLE β] [IsLinearPreorder β]
     {xs ys : List α} {f : α → β} (h : xs ≠ []) :
     xs.maxIdxOn f h ≤ (xs ++ ys).maxIdxOn f (by simp [h]) :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.left_le_minIdxOn_append h
 
 protected theorem maxIdxOn_take_le [LE β] [DecidableLE β] [IsLinearPreorder β]
     {xs : List α} {f : α → β} {i : Nat} (h : xs.take i ≠ []) :
     (xs.take i).maxIdxOn f h ≤ xs.maxIdxOn f (List.ne_nil_of_take_ne_nil h) :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.minIdxOn_take_le h
 
 @[simp]
 protected theorem maxIdxOn_replicate [LE β] [DecidableLE β] [Refl (α := β) (· ≤ ·)]
     {n : Nat} {a : α} {f : α → β} (h : replicate n a ≠ []) :
     (replicate n a).maxIdxOn f h = 0 :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.minIdxOn_replicate h
 
 @[simp]

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 ≠ []) :
@@ -268,9 +297,20 @@ protected theorem maxOn_cons
     (x :: xs).maxOn f (by exact of_decide_eq_false rfl) =
       if h : xs = [] then x else maxOn f x (xs.maxOn f h) := by
   simp only [maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstance : 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]
@@ -294,51 +334,51 @@ protected theorem maxOn_id [Max α] [LE α] [DecidableLE α] [LawfulOrderLeftLea
     {xs : List α} (h : xs ≠ []) :
     xs.maxOn id h = xs.max h := by
   simp only [List.maxOn_eq_minOn]
-  letI : LE α := (inferInstanceAs (LE α)).opposite
-  letI : Min α := (inferInstanceAs (Max α)).oppositeMin
+  letI : LE α := (inferInstance : LE α).opposite
+  letI : Min α := (inferInstance : Max α).oppositeMin
   simpa only [List.max_eq_min] using List.minOn_id h
 
 @[simp]
 protected theorem maxOn_mem [LE β] [DecidableLE β] {xs : List α}
     {f : α → β} {h : xs ≠ []} : xs.maxOn f h ∈ xs :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.minOn_mem (f := f)
 
 protected theorem le_apply_maxOn_of_mem [LE β] [DecidableLE β] [IsLinearPreorder β]
     {xs : List α} {f : α → β} {y : α} (hx : y ∈ xs) :
     f y ≤ f (xs.maxOn f (List.ne_nil_of_mem hx)) := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa [LE.le_opposite_iff] using List.apply_minOn_le_of_mem (f := f) hx
 
 protected theorem apply_maxOn_le_iff [LE β] [DecidableLE β] [IsLinearPreorder β] {xs : List α}
     {f : α → β} (h : xs ≠ []) {b : β} :
     f (xs.maxOn f h) ≤ b ↔ ∀ x ∈ xs, f x ≤ b := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa [LE.le_opposite_iff] using List.le_apply_minOn_iff (f := f) h
 
 protected theorem le_apply_maxOn_iff [LE β] [DecidableLE β] [IsLinearPreorder β] {xs : List α}
     {f : α → β} (h : xs ≠ []) {b : β} :
     b ≤ f (xs.maxOn f h) ↔ ∃ x ∈ xs, b ≤ f x := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa [LE.le_opposite_iff] using List.apply_minOn_le_iff (f := f) h
 
 protected theorem apply_maxOn_lt_iff
      [LE β] [DecidableLE β] [LT β] [IsLinearPreorder β] [LawfulOrderLT β]
     {xs : List α} {f : α → β} (h : xs ≠ []) {b : β} :
     f (xs.maxOn f h) < b ↔ ∀ x ∈ xs, f x < b := by
-  letI : LE β := (inferInstanceAs (LE β)).opposite
-  letI : LT β := (inferInstanceAs (LT β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
+  letI : LT β := (inferInstance : LT β).opposite
   simpa [LT.lt_opposite_iff] using List.lt_apply_minOn_iff (f := f) h
 
 protected theorem lt_apply_maxOn_iff
      [LE β] [DecidableLE β] [LT β] [IsLinearPreorder β] [LawfulOrderLT β]
     {xs : List α} {f : α → β} (h : xs ≠ []) {b : β} :
     b < f (xs.maxOn f h) ↔ ∃ x ∈ xs, b < f x := by
-  letI : LE β := (inferInstanceAs (LE β)).opposite
-  letI : LT β := (inferInstanceAs (LT β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
+  letI : LT β := (inferInstance : LT β).opposite
   simpa [LT.lt_opposite_iff] using List.apply_minOn_lt_iff (f := f) h
 
 protected theorem apply_maxOn_le_apply_maxOn_of_subset [LE β] [DecidableLE β]
@@ -346,14 +386,14 @@ protected theorem apply_maxOn_le_apply_maxOn_of_subset [LE β] [DecidableLE β]
     haveI : xs ≠ [] := by intro h; rw [h] at hxs; simp_all [subset_nil]
     f (ys.maxOn f hys) ≤ f (xs.maxOn f this) := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa [LE.le_opposite_iff] using List.apply_minOn_le_apply_minOn_of_subset (f := f) hxs hys
 
 protected theorem apply_maxOn_take_le [LE β] [DecidableLE β] [IsLinearPreorder β]
     {xs : List α} {f : α → β} {i : Nat} (h : xs.take i ≠ []) :
     f ((xs.take i).maxOn f h) ≤ f (xs.maxOn f (List.ne_nil_of_take_ne_nil h)) := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa [LE.le_opposite_iff] using List.le_apply_minOn_take (f := f) h
 
 protected theorem le_apply_maxOn_append_left [LE β] [DecidableLE β] [IsLinearPreorder β]
@@ -361,7 +401,7 @@ protected theorem le_apply_maxOn_append_left [LE β] [DecidableLE β] [IsLinearP
     f (xs.maxOn f h) ≤
       f ((xs ++ ys).maxOn f (append_ne_nil_of_left_ne_nil h ys)) := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa [LE.le_opposite_iff] using List.apply_minOn_append_le_left (f := f) h
 
 protected theorem le_apply_maxOn_append_right [LE β] [DecidableLE β] [IsLinearPreorder β]
@@ -369,7 +409,7 @@ protected theorem le_apply_maxOn_append_right [LE β] [DecidableLE β] [IsLinear
     f (ys.maxOn f h) ≤
       f ((xs ++ ys).maxOn f (append_ne_nil_of_right_ne_nil xs h)) := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa [LE.le_opposite_iff] using List.apply_minOn_append_le_right (f := f) h
 
 @[simp]
@@ -377,28 +417,48 @@ protected theorem maxOn_append [LE β] [DecidableLE β] [IsLinearPreorder β] {x
     {f : α → β} (hxs : xs ≠ []) (hys : ys ≠ []) :
     (xs ++ ys).maxOn f (by simp [hxs]) = maxOn f (xs.maxOn f hxs) (ys.maxOn f hys) := by
   simp only [List.maxOn_eq_minOn, maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa [LE.le_opposite_iff] using List.minOn_append (f := f) hxs hys
 
 protected theorem maxOn_eq_head [LE β] [DecidableLE β] [IsLinearPreorder β] {xs : List α}
     {f : α → β} (h : xs ≠ []) (h' : ∀ x ∈ xs, f x ≤ f (xs.head h)) :
     xs.maxOn f h = xs.head h := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa [LE.le_opposite_iff] using List.minOn_eq_head (f := f) h (by simpa [LE.le_opposite_iff] using h')
 
 protected theorem max_map
     [LE β] [DecidableLE β] [Max β] [IsLinearPreorder β] [LawfulOrderLeftLeaningMax β] {xs : List α}
     {f : α → β} (h : xs ≠ []) : (xs.map f).max (by simpa) = f (xs.maxOn f h) := by
-  letI : LE β := (inferInstanceAs (LE β)).opposite
-  letI : Min β := (inferInstanceAs (Max β)).oppositeMin
+  letI : LE β := (inferInstance : LE β).opposite
+  letI : Min β := (inferInstance : 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 ≠ []) :
     (replicate n a).maxOn f h = a :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.minOn_replicate (f := f) h
 
 /-! # minOn? -/
@@ -519,7 +579,7 @@ protected theorem maxOn?_nil [LE β] [DecidableLE β] {f : α → β} :
 protected theorem maxOn?_cons_eq_some_maxOn
     [LE β] [DecidableLE β] {f : α → β} {x : α} {xs : List α} :
     (x :: xs).maxOn? f = some ((x :: xs).maxOn f (fun h => nomatch h)) :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.minOn?_cons_eq_some_minOn
 
 protected theorem maxOn?_cons
@@ -528,7 +588,7 @@ protected theorem maxOn?_cons
   have : maxOn f x = (letI : LE β := LE.opposite inferInstance; minOn f x) := by
     ext; simp only [maxOn_eq_minOn]
   simp only [List.maxOn?_eq_minOn?, this]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   exact List.minOn?_cons
 
 @[simp]
@@ -539,8 +599,8 @@ protected theorem maxOn?_singleton [LE β] [DecidableLE β] {x : α} {f : α →
 @[simp]
 protected theorem maxOn?_id [Max α] [LE α] [DecidableLE α] [LawfulOrderLeftLeaningMax α]
     {xs : List α} : xs.maxOn? id = xs.max? := by
-  letI : LE α := (inferInstanceAs (LE α)).opposite
-  letI : Min α := (inferInstanceAs (Max α)).oppositeMin
+  letI : LE α := (inferInstance : LE α).opposite
+  letI : Min α := (inferInstance : Max α).oppositeMin
   simpa only [List.maxOn?_eq_minOn?, List.max?_eq_min?] using List.minOn?_id (α := α)
 
 protected theorem maxOn?_eq_if
@@ -550,7 +610,7 @@ protected theorem maxOn?_eq_if
       some (xs.maxOn f h)
     else
       none :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.minOn?_eq_if
 
 @[simp]
@@ -560,55 +620,55 @@ protected theorem isSome_maxOn?_iff [LE β] [DecidableLE β] {f : α → β} {xs
 
 protected theorem maxOn_eq_get_maxOn? [LE β] [DecidableLE β] {f : α → β} {xs : List α}
     (h : xs ≠ []) : xs.maxOn f h = (xs.maxOn? f).get (List.isSome_maxOn?_iff.mpr h) :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.minOn_eq_get_minOn? (f := f) h
 
 protected theorem maxOn?_eq_some_maxOn [LE β] [DecidableLE β] {f : α → β} {xs : List α}
     (h : xs ≠ []) : xs.maxOn? f = some (xs.maxOn f h) :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.minOn?_eq_some_minOn (f := f) h
 
 @[simp]
 protected theorem get_maxOn? [LE β] [DecidableLE β] {f : α → β} {xs : List α}
     (h : xs ≠ []) : (xs.maxOn? f).get (List.isSome_maxOn?_iff.mpr h) = xs.maxOn f h :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.get_minOn? (f := f) h
 
 protected theorem maxOn_eq_of_maxOn?_eq_some
     [LE β] [DecidableLE β] {f : α → β} {xs : List α} {x : α} (h : xs.maxOn? f = some x) :
     xs.maxOn f (List.isSome_maxOn?_iff.mp (Option.isSome_of_eq_some h)) = x :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.minOn_eq_of_minOn?_eq_some (f := f) h
 
 protected theorem isSome_maxOn?_of_mem
     [LE β] [DecidableLE β] {f : α → β} {xs : List α} {x : α} (h : x ∈ xs) :
     (xs.maxOn? f).isSome :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.isSome_minOn?_of_mem (f := f) h
 
 protected theorem le_apply_get_maxOn?_of_mem
     [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β} {xs : List α} {x : α} (h : x ∈ xs) :
     f x ≤ f ((xs.maxOn? f).get (List.isSome_maxOn?_of_mem h)) := by
   simp only [List.maxOn?_eq_minOn?]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa [LE.le_opposite_iff] using List.apply_get_minOn?_le_of_mem (f := f) h
 
 protected theorem maxOn?_mem [LE β] [DecidableLE β] {xs : List α}
     {f : α → β} (h : xs.maxOn? f = some a) : a ∈ xs :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.minOn?_mem (f := f) h
 
 protected theorem maxOn?_replicate [LE β] [DecidableLE β] [IsLinearPreorder β]
     {n : Nat} {a : α} {f : α → β} :
     (replicate n a).maxOn? f = if n = 0 then none else some a :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.minOn?_replicate
 
 @[simp]
 protected theorem maxOn?_replicate_of_pos [LE β] [DecidableLE β] [IsLinearPreorder β]
     {n : Nat} {a : α} {f : α → β} (h : 0 < n) :
     (replicate n a).maxOn? f = some a :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.minOn?_replicate_of_pos (f := f) h
 
 @[simp]
@@ -618,7 +678,7 @@ protected theorem maxOn?_append [LE β] [DecidableLE β] [IsLinearPreorder β]
   have : maxOn f = (letI : LE β := LE.opposite inferInstance; minOn f) := by
     ext; simp only [maxOn_eq_minOn]
   simp only [List.maxOn?_eq_minOn?, this]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   exact List.minOn?_append xs ys f
 
 end List

src/Init/Data/List/OfFn.lean

@@ -99,7 +99,6 @@ theorem ofFn_add {n m} {f : Fin (n + m) → α} :
   induction m with
   | zero => simp
   | succ m ih =>
-    set_option backward.isDefEq.respectTransparency false in
     simp [-ofFn_succ, ofFn_succ_last, ih]
 
 @[simp]
@@ -157,7 +156,6 @@ theorem ofFnM_add {n m} [Monad m] [LawfulMonad m] {f : Fin (n + k) → m α} :
   induction k with
   | zero => simp
   | succ k ih =>
-    set_option backward.isDefEq.respectTransparency false in
     simp [ofFnM_succ_last, ih]
 
 end List

src/Init/Data/List/ToArray.lean

@@ -589,7 +589,7 @@ theorem flatMap_toArray_cons {β} (f : α → Array β) (a : α) (as : List α)
 @[simp, grind =] theorem swap_toArray (l : List α) (i j : Nat) {hi hj}:
     l.toArray.swap i j hi hj = ((l.set i l[j]).set j l[i]).toArray := by
   apply ext'
-  simp; rfl
+  simp
 
 @[simp, grind =] theorem eraseIdx_toArray (l : List α) (i : Nat) (h : i < l.toArray.size) :
     l.toArray.eraseIdx i h = (l.eraseIdx i).toArray := by
@@ -644,8 +644,8 @@ private theorem insertIdx_loop_toArray (i : Nat) (l : List α) (j : Nat) (hj : j
       drop_append_of_le_length (by simp; omega)]
     simp only [append_assoc, cons_append, nil_append]
     cases i with
-    | zero => simp; rfl
-    | succ i => rw [take_set_of_le (by omega)]; rfl
+    | zero => simp
+    | succ i => rw [take_set_of_le (by omega)]
   · simp only [Nat.not_lt] at h'
     have : i = j := by omega
     subst this

src/Init/Data/Nat/Basic.lean

@@ -478,7 +478,7 @@ instance : Std.Trichotomous (. < . : Nat → Nat → Prop) where
 
 set_option linter.missingDocs false in
 @[deprecated Nat.instTrichotomousLt (since := "2025-10-27")]
-def Nat.instAntisymmNotLt : Std.Antisymm (¬ . < . : Nat → Nat → Prop) where
+theorem Nat.instAntisymmNotLt : Std.Antisymm (¬ . < . : Nat → Nat → Prop) where
   antisymm := Nat.instTrichotomousLt.trichotomous
 
 protected theorem add_le_add_left {n m : Nat} (h : n ≤ m) (k : Nat) : k + n ≤ k + m :=

src/Init/Data/Nat/Fold.lean

@@ -400,7 +400,6 @@ theorem dfold_add
   induction m with
   | zero => simp; rfl
   | succ m ih =>
-    set_option backward.isDefEq.respectTransparency false in
     simp [dfold_congr (Nat.add_assoc n m 1).symm, ih]
 
 @[simp] theorem dfoldRev_zero
@@ -436,7 +435,6 @@ theorem dfoldRev_add
   induction m with
   | zero => simp; rfl
   | succ m ih =>
-    set_option backward.isDefEq.respectTransparency false in
     simp [← Nat.add_assoc, ih]
 
 end Nat

src/Init/Data/Option/Attach.lean

@@ -444,7 +444,6 @@ instance : MonadAttach Option where
   CanReturn x a := x = some a
   attach x := x.attach
 
-set_option backward.isDefEq.respectTransparency false in
 public instance : LawfulMonadAttach Option where
   map_attach {α} x := by simp [MonadAttach.attach]
   canReturn_map_imp {α P x a} := by
@@ -456,7 +455,6 @@ end Option
 
 namespace OptionT
 
-set_option backward.isDefEq.respectTransparency false in
 public instance [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] :
     WeaklyLawfulMonadAttach (OptionT m) where
   map_attach {α} x := by

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
 
@@ -147,7 +147,7 @@ public theorem LawfulOrderMin.of_min_le {α : Type u} [Min α] [LE α]
 This lemma characterizes in terms of `LE α` when a `Max α` instance "behaves like a supremum
 operator".
 -/
-public def LawfulOrderSup.of_le {α : Type u} [Max α] [LE α]
+public theorem LawfulOrderSup.of_le {α : Type u} [Max α] [LE α]
     (max_le_iff : ∀ a b c : α, max a b ≤ c ↔ a ≤ c ∧ b ≤ c) : LawfulOrderSup α where
   max_le_iff := max_le_iff
 
@@ -159,7 +159,7 @@ instances.
 
 The produced instance entails `LawfulOrderSup α` and `MaxEqOr α`.
 -/
-public def LawfulOrderMax.of_max_le_iff {α : Type u} [Max α] [LE α]
+public theorem LawfulOrderMax.of_max_le_iff {α : Type u} [Max α] [LE α]
     (max_le_iff : ∀ a b c : α, max a b ≤ c ↔ a ≤ c ∧ b ≤ c := by exact LawfulOrderInf.le_min_iff)
     (max_eq_or : ∀ a b : α, max a b = a ∨ max a b = b := by exact MaxEqOr.max_eq_or) :
     LawfulOrderMax α where
@@ -196,7 +196,7 @@ Creates a *total* `LE α` instance from an `LT α` instance.
 
 This only makes sense for asymmetric `LT α` instances (see `Std.Asymm`).
 -/
-@[inline]
+@[inline, implicit_reducible, expose]
 public def _root_.LE.ofLT (α : Type u) [LT α] : LE α where
   le a b := ¬ b < a
 
@@ -208,7 +208,7 @@ public instance LawfulOrderLT.of_lt {α : Type u} [LT α] [i : Asymm (α := α)
     haveI := LE.ofLT α
     LawfulOrderLT α :=
   letI := LE.ofLT α
-  { lt_iff a b := by simp +instances [LE.ofLT, LE.le]; apply Asymm.asymm }
+  { lt_iff a b := by simp +instances [LE.le]; apply Asymm.asymm }
 
 /--
 If an `LT α` instance is asymmetric and its negation is transitive, then `LE.ofLT α` represents a
@@ -253,7 +253,7 @@ public theorem LawfulOrderInf.of_lt {α : Type u} [Min α] [LT α]
   letI := LE.ofLT α
   { le_min_iff a b c := by
       open Classical in
-      simp +instances only [LE.ofLT, LE.le]
+      simp +instances only [LE.le]
       simp [← not_or, Decidable.not_iff_not]
       simpa [Decidable.imp_iff_not_or] using min_lt_iff a b c }
 
@@ -276,14 +276,14 @@ public theorem LawfulOrderMin.of_lt {α : Type u} [Min α] [LT α]
 This lemma characterizes in terms of `LT α` when a `Max α` instance
 "behaves like an supremum operator" with respect to `LE.ofLT α`.
 -/
-public def LawfulOrderSup.of_lt {α : Type u} [Max α] [LT α]
+public theorem LawfulOrderSup.of_lt {α : Type u} [Max α] [LT α]
     (lt_max_iff : ∀ a b c : α, c < max a b ↔ c < a ∨ c < b) :
     haveI := LE.ofLT α
     LawfulOrderSup α :=
   letI := LE.ofLT α
   { max_le_iff a b c := by
       open Classical in
-      simp +instances only [LE.ofLT, LE.le]
+      simp +instances only [LE.le]
       simp [← not_or, Decidable.not_iff_not]
       simpa [Decidable.imp_iff_not_or] using lt_max_iff a b c }
 
@@ -293,7 +293,7 @@ Derives a `LawfulOrderMax α` instance for `LE.ofLT` from two properties involvi
 
 The produced instance entails `LawfulOrderSup α` and `MaxEqOr α`.
 -/
-public def LawfulOrderMax.of_lt {α : Type u} [Max α] [LT α]
+public theorem LawfulOrderMax.of_lt {α : Type u} [Max α] [LT α]
     (lt_max_iff : ∀ a b c : α, c < max a b ↔ c < a ∨ c < b)
     (max_eq_or : ∀ a b : α, max a b = a ∨ max a b = b) :
     haveI := LE.ofLT α

src/Init/Data/Order/FactoriesExtra.lean

@@ -19,14 +19,14 @@ 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
 
 /--
 Creates an `DecidableLE α` instance using a well-behaved `Ord α` instance.
 -/
-@[inline, expose]
+@[inline, expose, implicit_reducible]
 public def _root_.DecidableLE.ofOrd (α : Type u) [LE α] [Ord α] [LawfulOrderOrd α] :
     DecidableLE α :=
   fun a b => match h : (compare a b).isLE with
@@ -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
@@ -93,7 +93,7 @@ grind_pattern compare_ne_eq => compare a b, Ordering.eq where
 /--
 Creates a `DecidableLT α` instance using a well-behaved `Ord α` instance.
 -/
-@[inline, expose]
+@[inline, expose, implicit_reducible]
 public def _root_.DecidableLT.ofOrd (α : Type u) [LE α] [LT α] [Ord α] [LawfulOrderOrd α]
     [LawfulOrderLT α] :
     DecidableLT α :=
@@ -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

@@ -39,8 +39,8 @@ public theorem minOn_id [Min α] [LE α] [DecidableLE α] [LawfulOrderLeftLeanin
 
 public theorem maxOn_id [Max α] [LE α] [DecidableLE α] [LawfulOrderLeftLeaningMax α] {x y : α} :
     maxOn id x y = max x y := by
-  letI : LE α := (inferInstanceAs (LE α)).opposite
-  letI : Min α := (inferInstanceAs (Max α)).oppositeMin
+  letI : LE α := (inferInstance : LE α).opposite
+  letI : Min α := (inferInstance : Max α).oppositeMin
   simp [maxOn, minOn_id, Max.min_oppositeMin, this]
 
 public theorem minOn_eq_or [LE β] [DecidableLE β] {f : α → β} {x y : α} :
@@ -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 : α} :
@@ -153,32 +168,32 @@ public theorem maxOn_eq_right_of_lt
     [LE β] [DecidableLE β] [LT β] [Total (α := β) (· ≤ ·)] [LawfulOrderLT β]
     {f : α → β} {x y : α} (h : f x < f y) :
     maxOn f x y = y :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
-  letI : LT β := (inferInstanceAs (LT β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
+  letI : LT β := (inferInstance : LT β).opposite
   minOn_eq_right_of_lt (h := by simpa [LT.lt_opposite_iff] using h) ..
 
 public theorem left_le_apply_maxOn [le : LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β}
     {x y : α} : f x ≤ f (maxOn f x y) := by
   rw [maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa only [LE.le_opposite_iff] using apply_minOn_le_left (f := f) ..
 
 public theorem right_le_apply_maxOn [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β}
     {x y : α} : f y ≤ f (maxOn f x y) := by
   rw [maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa only [LE.le_opposite_iff] using apply_minOn_le_right (f := f)
 
 public theorem apply_maxOn_le_iff [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β}
     {x y : α} {b : β} :
     f (maxOn f x y) ≤ b ↔ f x ≤ b ∧ f y ≤ b := by
   rw [maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa only [LE.le_opposite_iff] using le_apply_minOn_iff (f := f)
 
 public theorem maxOn_assoc [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β}
     {x y z : α} : maxOn f (maxOn f x y) z = maxOn f x (maxOn f y z) :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   minOn_assoc (f := f)
 
 public instance [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β} :
@@ -188,10 +203,25 @@ public instance [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β} :
 
 public theorem max_apply [LE β] [DecidableLE β] [Max β] [LawfulOrderLeftLeaningMax β]
     {f : α → β} {x y : α} : max (f x) (f y) = f (maxOn f x y) := by
-  letI : LE β := (inferInstanceAs (LE β)).opposite
-  letI : Min β := (inferInstanceAs (Max β)).oppositeMin
+  letI : LE β := (inferInstance : LE β).opposite
+  letI : Min β := (inferInstance : Max β).oppositeMin
   simpa [Max.min_oppositeMin] using min_apply (f := f)
 
 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

@@ -44,7 +44,7 @@ def min' [LE α] [DecidableLE α] (a b : α) : α :=
 
 open scoped Std.OppositeOrderInstances in
 def max' [LE α] [DecidableLE α] (a b : α) : α :=
-  letI : LE α := (inferInstanceAs (LE α)).opposite
+  letI : LE α := (inferInstance : LE α).opposite
   -- `DecidableLE` for the opposite order is derived automatically via `OppositeOrderInstances`
   min' a b
 ```
@@ -52,7 +52,8 @@ 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 α} :
@@ -89,6 +90,7 @@ example [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] {x y : α}
 Without the `open scoped` command, Lean would not find the {lit}`LawfulOrderLT α`
 and {lit}`IsLinearOrder α` instances for the opposite order that are required by {name}`not_le`.
 -/
+@[implicit_reducible]
 def LT.opposite (lt : LT α) : LT α where
   lt a b := b < a
 
@@ -125,6 +127,7 @@ example [LE α] [DecidableLE α] [Min α] [Std.LawfulOrderLeftLeaningMin α] {a
 Without the `open scoped` command, Lean would not find the {lit}`LawfulOrderLeftLeaningMax α`
 instance for the opposite order that is required by {name}`max_eq_if`.
 -/
+@[implicit_reducible]
 def Min.oppositeMax (min : Min α) : Max α where
   max a b := Min.min a b
 
@@ -161,6 +164,7 @@ example [LE α] [DecidableLE α] [Max α] [Std.LawfulOrderLeftLeaningMax α] {a
 Without the `open scoped` command, Lean would not find the {lit}`LawfulOrderLeftLeaningMin α`
 instance for the opposite order that is required by {name}`min_eq_if`.
 -/
+@[implicit_reducible]
 def Max.oppositeMin (max : Max α) : Min α where
   min a b := Max.max a b
 
@@ -262,15 +266,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]
+@[inline, expose, implicit_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]
+@[inline, 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]
+@[inline, 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]
+@[inline, 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]
+@[inline, 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]
+@[inline, expose, implicit_reducible]
 public def LinearPreorderPackage.ofOrd (α : Type u)
     (args : Packages.LinearPreorderOfOrdArgs α := by exact {}) : LinearPreorderPackage α :=
   letI := args.ord
@@ -791,10 +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]
+@[inline, expose, implicit_reducible]
 public def LinearOrderPackage.ofOrd (α : Type u)
     (args : Packages.LinearOrderOfOrdArgs α := by exact {}) : LinearOrderPackage α :=
-  set_option backward.isDefEq.respectTransparency false in
+  -- 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

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

@@ -102,7 +102,7 @@ theorem Iterator.Monadic.isPlausibleStep_iff [UpwardEnumerable α] [LE α] [Deci
 theorem Iterator.Monadic.step_eq_step [UpwardEnumerable α] [LE α] [DecidableLE α]
     {it : IterM (α := Rxc.Iterator α) Id α} :
     Std.Iterator.step it = pure (.deflate ⟨Iterator.Monadic.step it, isPlausibleStep_iff.mpr rfl⟩) := by
-  simp [Std.Iterator.step]; rfl
+  simp [Std.Iterator.step]
 
 theorem Iterator.isPlausibleStep_iff [UpwardEnumerable α] [LE α] [DecidableLE α]
     {it : Iter (α := Rxc.Iterator α) α} {step} :
@@ -184,7 +184,7 @@ theorem Iterator.Monadic.isPlausibleSuccessorOf_iff
   · rintro ⟨a, h, hP, h'⟩
     refine ⟨.yield it' a, rfl, ?_⟩
     simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, step, h, hP, ↓reduceIte,
-      IterStep.yield.injEq, and_true]
+      IterStep.yield.injEq, and_true, instIteratorIteratorIdOfUpwardEnumerableOfDecidableLE] -- TODO
     simp [h'.1, ← h'.2]
 
 theorem Iterator.isPlausibleSuccessorOf_iff
@@ -244,10 +244,10 @@ private def Iterator.instFinitenessRelation [UpwardEnumerable α] [LE α] [Decid
       intro bound
       constructor
       intro it' ⟨step, hs₁, hs₂⟩
-      simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, Monadic.step] at hs₂
+      simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, Monadic.step, instIteratorIteratorIdOfUpwardEnumerableOfDecidableLE] at hs₂ -- TODO
       simp [hs₂, IterStep.successor] at hs₁
     simp only [IterM.IsPlausibleSuccessorOf, IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
-      Monadic.step, exists_eq_right] at hnone ⊢
+      Monadic.step, exists_eq_right, instIteratorIteratorIdOfUpwardEnumerableOfDecidableLE] at hnone ⊢ -- TODO
     match it with
     | ⟨⟨none, _⟩⟩ => apply hnone
     | ⟨⟨some init, bound⟩⟩ =>
@@ -293,7 +293,7 @@ private def Iterator.instProductivenessRelation [UpwardEnumerable α] [LE α] [D
   subrelation {it it'} h := by
     exfalso
     simp only [IterM.IsPlausibleSkipSuccessorOf, IterM.IsPlausibleStep,
-      Iterator.IsPlausibleStep, Monadic.step] at h
+      Iterator.IsPlausibleStep, Monadic.step, instIteratorIteratorIdOfUpwardEnumerableOfDecidableLE] at h
     split at h
     · cases h
     · split at h
@@ -535,7 +535,6 @@ private theorem Iterator.instIteratorLoop.loop_eq_wf [UpwardEnumerable α] [LE
     · rw [WellFounded.fix_eq]
       simp_all
 
-set_option backward.isDefEq.respectTransparency false in
 private theorem Iterator.instIteratorLoop.loopWf_eq [UpwardEnumerable α] [LE α] [DecidableLE α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
     {n : Type u → Type w} [Monad n] [LawfulMonad n] (γ : Type u)
@@ -581,24 +580,29 @@ private theorem Iterator.instIteratorLoop.loopWf_eq [UpwardEnumerable α] [LE α
           · simp
         · simp
     · rw [IterM.DefaultConsumers.forIn'_eq_match_step Pl wf]
-      simp [IterM.step_eq, Monadic.step, instLawfulMonadLiftFunction.liftBind_pure, *]
+      simp only [IterM.step_eq, instLawfulMonadLiftFunction.liftBind_pure, Shrink.inflate_deflate, *]
+      -- Unfolding `Monadic.step` earlier would make some defeq checks fail on reducible transparency:
+      -- `Iterator.IsPlausibleStep` is reducible and it reduces to `Monadic.step`, but `Monadic.step`
+      -- is semireducible, and `simp` isn't able to unfold `Monadic.step` inside `Iterator.IsPlausibleStep`,
+      -- since that one only appears in the type of a constant -- I think?
+      simp [Monadic.step]
   · simp
 termination_by IteratorLoop.WithWF.mk ⟨⟨some next, upperBound⟩⟩ acc (hwf := wf)
 decreasing_by
   simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *]
 
-set_option backward.isDefEq.respectTransparency false in
 instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α] [LE α] [DecidableLE α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
     {n : Type u → Type w} [Monad n] [LawfulMonad n] :
     LawfulIteratorLoop (Rxc.Iterator α) Id n where
   lawful := by
     intro lift instLawfulMonadLiftFunction γ it init Pl wf f
-    simp +instances only [IteratorLoop.defaultImplementation, IteratorLoop.forIn,
-      IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
+    simp +instances only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
     rw [IterM.DefaultConsumers.forIn'.wf]
     split; rotate_left
-    · simp [IterM.step_eq, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure (liftBind := lift)]
+    · simp only [IterM.step_eq,
+      Internal.LawfulMonadLiftBindFunction.liftBind_pure (liftBind := lift), Shrink.inflate_deflate]
+      simp [Monadic.step]
     rename_i next _
     rw [instIteratorLoop.loop_eq_wf Pl wf, instIteratorLoop.loopWf_eq (lift := lift)]
     simp only [IterM.step_mk, Monadic.step_eq_step, Monadic.step,
@@ -680,7 +684,7 @@ theorem Iterator.Monadic.isPlausibleStep_iff [UpwardEnumerable α] [LT α] [Deci
 theorem Iterator.Monadic.step_eq_step [UpwardEnumerable α] [LT α] [DecidableLT α]
     {it : IterM (α := Rxo.Iterator α) Id α} :
     Std.Iterator.step it = pure (.deflate ⟨Iterator.Monadic.step it, isPlausibleStep_iff.mpr rfl⟩) := by
-  simp [Std.Iterator.step]; rfl
+  simp [Std.Iterator.step]
 
 theorem Iterator.isPlausibleStep_iff [UpwardEnumerable α] [LT α] [DecidableLT α]
     {it : Iter (α := Rxo.Iterator α) α} {step} :
@@ -762,7 +766,7 @@ theorem Iterator.Monadic.isPlausibleSuccessorOf_iff
   · rintro ⟨a, h, hP, h'⟩
     refine ⟨.yield it' a, rfl, ?_⟩
     simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, step, h, hP, ↓reduceIte,
-      IterStep.yield.injEq, and_true]
+      IterStep.yield.injEq, and_true, instIteratorIteratorIdOfUpwardEnumerableOfDecidableLT] -- TODO
     simp [h'.1, ← h'.2]
 
 theorem Iterator.isPlausibleSuccessorOf_iff
@@ -822,10 +826,10 @@ private def Iterator.instFinitenessRelation [UpwardEnumerable α] [LT α] [Decid
       intro bound
       constructor
       intro it' ⟨step, hs₁, hs₂⟩
-      simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, Monadic.step] at hs₂
+      simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, Monadic.step, instIteratorIteratorIdOfUpwardEnumerableOfDecidableLT] at hs₂ -- TODO
       simp [hs₂, IterStep.successor] at hs₁
     simp only [IterM.IsPlausibleSuccessorOf, IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
-      Monadic.step, exists_eq_right] at hnone ⊢
+      Monadic.step, exists_eq_right, instIteratorIteratorIdOfUpwardEnumerableOfDecidableLT] at hnone ⊢ -- TODO
     match it with
     | ⟨⟨none, _⟩⟩ => apply hnone
     | ⟨⟨some init, bound⟩⟩ =>
@@ -871,7 +875,7 @@ private def Iterator.instProductivenessRelation [UpwardEnumerable α] [LT α] [D
   subrelation {it it'} h := by
     exfalso
     simp only [IterM.IsPlausibleSkipSuccessorOf, IterM.IsPlausibleStep,
-      Iterator.IsPlausibleStep, Monadic.step] at h
+      Iterator.IsPlausibleStep, Monadic.step, instIteratorIteratorIdOfUpwardEnumerableOfDecidableLT] at h -- TODO
     split at h
     · cases h
     · split at h
@@ -1168,8 +1172,7 @@ instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α] [LT α] [Decidabl
     LawfulIteratorLoop (Rxo.Iterator α) Id n where
   lawful := by
     intro lift instLawfulMonadLiftFunction γ it init Pl wf f
-    simp +instances only [IteratorLoop.defaultImplementation, IteratorLoop.forIn,
-      IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
+    simp +instances only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
     rw [IterM.DefaultConsumers.forIn'.wf]
     split; rotate_left
     · simp [IterM.step_eq, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure (liftBind := lift)]
@@ -1244,7 +1247,7 @@ theorem Iterator.Monadic.isPlausibleStep_iff [UpwardEnumerable α]
 theorem Iterator.Monadic.step_eq_step [UpwardEnumerable α]
     {it : IterM (α := Rxi.Iterator α) Id α} :
     it.step = pure (.deflate ⟨Iterator.Monadic.step it, isPlausibleStep_iff.mpr rfl⟩) := by
-  simp [IterM.step, Std.Iterator.step]; rfl
+  simp [IterM.step, Std.Iterator.step]
 
 theorem Iterator.isPlausibleStep_iff [UpwardEnumerable α]
     {it : Iter (α := Rxi.Iterator α) α} {step} :
@@ -1310,7 +1313,7 @@ theorem Iterator.Monadic.isPlausibleSuccessorOf_iff
   · rintro ⟨a, h, h'⟩
     refine ⟨.yield it' a, rfl, ?_⟩
     simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, step, h,
-      IterStep.yield.injEq, and_true]
+      IterStep.yield.injEq, and_true, instIteratorIteratorIdOfUpwardEnumerable] -- TODO
     simp [h']
 
 theorem Iterator.isPlausibleSuccessorOf_iff
@@ -1345,10 +1348,10 @@ private def Iterator.instFinitenessRelation [UpwardEnumerable α]
         ⟨⟨none⟩⟩ := by
       constructor
       intro it' ⟨step, hs₁, hs₂⟩
-      simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, Monadic.step] at hs₂
+      simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, Monadic.step, instIteratorIteratorIdOfUpwardEnumerable] at hs₂ -- TODO
       simp [hs₂, IterStep.successor] at hs₁
     simp only [IterM.IsPlausibleSuccessorOf, IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
-      Monadic.step, exists_eq_right] at hnone ⊢
+      Monadic.step, exists_eq_right, instIteratorIteratorIdOfUpwardEnumerable] at hnone ⊢ -- TODO
     match it with
     | ⟨⟨none⟩⟩ => apply hnone
     | ⟨⟨some init⟩⟩ =>
@@ -1387,7 +1390,7 @@ private def Iterator.instProductivenessRelation [UpwardEnumerable α]
   subrelation {it it'} h := by
     exfalso
     simp only [IterM.IsPlausibleSkipSuccessorOf, IterM.IsPlausibleStep,
-      Iterator.IsPlausibleStep, Monadic.step] at h
+      Iterator.IsPlausibleStep, Monadic.step, instIteratorIteratorIdOfUpwardEnumerable] at h -- TODO
     split at h <;> cases h
 
 @[no_expose]
@@ -1634,8 +1637,7 @@ instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α]
     LawfulIteratorLoop (Rxi.Iterator α) Id n where
   lawful := by
     intro lift instLawfulMonadLiftFunction γ it init Pl wf f
-    simp +instances only [IteratorLoop.defaultImplementation, IteratorLoop.forIn,
-      IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
+    simp +instances only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
     rw [IterM.DefaultConsumers.forIn'.wf]
     split; rotate_left
     · simp [Monadic.step_eq_step, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure]

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

@@ -10,7 +10,6 @@ prelude
 public import Init.Data.Range.Polymorphic.Instances
 public import Init.Data.SInt
 import all Init.Data.SInt.Basic
-
 import all Init.Data.Range.Polymorphic.Internal.SignedBitVec
 import Init.ByCases
 import Init.Data.Int.LemmasAux
@@ -246,9 +245,10 @@ instance : HasModel Int8 (BitVec 8) where
   decode x := .ofBitVec x
   encode_decode := by simp
   decode_encode := by simp
-  le_iff_encode_le := by simp +instances [Int8.le_iff_toBitVec_sle, BitVec.Signed.instLE]
-  lt_iff_encode_lt := by simp +instances [Int8.lt_iff_toBitVec_slt, BitVec.Signed.instLT]
+  le_iff_encode_le := by simp [LE.le, Int8.le]
+  lt_iff_encode_lt := by simp [LT.lt, Int8.lt]
 
+set_option backward.whnf.reducibleClassField false in
 theorem instUpwardEnumerable_eq :
     instUpwardEnumerable = HasModel.instUpwardEnumerable := by
   apply UpwardEnumerable.ext
@@ -259,6 +259,7 @@ theorem instUpwardEnumerable_eq :
     simp +instances [HasModel.succMany?_eq, instUpwardEnumerable, HasModel.encode, HasModel.decode,
       ← toInt_toBitVec, toBitVec_maxValueSealed_eq_intMaxSealed, ofIntLE_eq_ofInt]
 
+
 instance : LawfulUpwardEnumerable Int8 := by
   simp +instances only [instUpwardEnumerable_eq]
   infer_instance
@@ -340,9 +341,10 @@ instance : HasModel Int16 (BitVec 16) where
   decode x := .ofBitVec x
   encode_decode := by simp
   decode_encode := by simp
-  le_iff_encode_le := by simp +instances [Int16.le_iff_toBitVec_sle, BitVec.Signed.instLE]
-  lt_iff_encode_lt := by simp +instances [Int16.lt_iff_toBitVec_slt, BitVec.Signed.instLT]
+  le_iff_encode_le := by simp [LE.le, Int16.le]
+  lt_iff_encode_lt := by simp [LT.lt, Int16.lt]
 
+set_option backward.whnf.reducibleClassField false in
 theorem instUpwardEnumerable_eq :
     instUpwardEnumerable = HasModel.instUpwardEnumerable := by
   apply UpwardEnumerable.ext
@@ -350,15 +352,16 @@ theorem instUpwardEnumerable_eq :
     apply HasModel.succ?_eq_of_technicalCondition
     simp [HasModel.encode, succ?, ← Int16.toBitVec_inj, toBitVec_minValueSealed_eq_intMinSealed]
   · ext
-    simp +instances [HasModel.succMany?_eq, instUpwardEnumerable, HasModel.encode, HasModel.decode,
+    simp only [HasModel.succMany?_eq]
+    simp [UpwardEnumerable.succMany?, HasModel.encode, HasModel.decode,
       ← toInt_toBitVec, toBitVec_maxValueSealed_eq_intMaxSealed, ofIntLE_eq_ofInt]
 
 instance : LawfulUpwardEnumerable Int16 := by
-  simp +instances only [instUpwardEnumerable_eq]
+  rw [instUpwardEnumerable_eq]
   infer_instance
 
 instance : LawfulUpwardEnumerableLE Int16 := by
-  simp +instances only [instUpwardEnumerable_eq]
+  rw [instUpwardEnumerable_eq]
   infer_instance
 
 public instance instRxcHasSize : Rxc.HasSize Int16 where
@@ -370,7 +373,7 @@ theorem instRxcHasSize_eq :
     ← toInt_toBitVec, HasModel.toNat_toInt_add_one_sub_toInt (Nat.zero_lt_succ _)]
 
 public instance instRxcLawfulHasSize : Rxc.LawfulHasSize Int16 := by
-  simp +instances only [instUpwardEnumerable_eq, instRxcHasSize_eq]
+  rw [instUpwardEnumerable_eq, instRxcHasSize_eq]
   infer_instance
 public instance : Rxc.IsAlwaysFinite Int16 := by exact inferInstance
 
@@ -387,7 +390,7 @@ theorem instRxiHasSize_eq :
     HasModel.encode, HasModel.toNat_two_pow_sub_one_sub_toInt (show 16 > 0 by omega)]
 
 public instance instRxiLawfulHasSize : Rxi.LawfulHasSize Int16 := by
-  simp +instances only [instUpwardEnumerable_eq, instRxiHasSize_eq]
+  rw [instUpwardEnumerable_eq, instRxiHasSize_eq]
   infer_instance
 public instance instRxiIsAlwaysFinite : Rxi.IsAlwaysFinite Int16 := by exact inferInstance
 
@@ -434,9 +437,10 @@ instance : HasModel Int32 (BitVec 32) where
   decode x := .ofBitVec x
   encode_decode := by simp
   decode_encode := by simp
-  le_iff_encode_le := by simp +instances [Int32.le_iff_toBitVec_sle, BitVec.Signed.instLE]
-  lt_iff_encode_lt := by simp +instances [Int32.lt_iff_toBitVec_slt, BitVec.Signed.instLT]
+  le_iff_encode_le := by simp [LE.le, Int32.le]
+  lt_iff_encode_lt := by simp [LT.lt, Int32.lt]
 
+set_option backward.whnf.reducibleClassField false in
 theorem instUpwardEnumerable_eq :
     instUpwardEnumerable = HasModel.instUpwardEnumerable := by
   apply UpwardEnumerable.ext
@@ -444,15 +448,16 @@ theorem instUpwardEnumerable_eq :
     apply HasModel.succ?_eq_of_technicalCondition
     simp [HasModel.encode, succ?, ← Int32.toBitVec_inj, toBitVec_minValueSealed_eq_intMinSealed]
   · ext
-    simp +instances [HasModel.succMany?_eq, instUpwardEnumerable, HasModel.encode, HasModel.decode,
+    simp only [HasModel.succMany?_eq]
+    simp [UpwardEnumerable.succMany?, HasModel.encode, HasModel.decode,
       ← toInt_toBitVec, toBitVec_maxValueSealed_eq_intMaxSealed, ofIntLE_eq_ofInt]
 
 instance : LawfulUpwardEnumerable Int32 := by
-  simp +instances only [instUpwardEnumerable_eq]
+  rw [instUpwardEnumerable_eq]
   infer_instance
 
 instance : LawfulUpwardEnumerableLE Int32 := by
-  simp +instances only [instUpwardEnumerable_eq]
+  rw [instUpwardEnumerable_eq]
   infer_instance
 
 public instance instRxcHasSize : Rxc.HasSize Int32 where
@@ -464,7 +469,7 @@ theorem instRxcHasSize_eq :
     ← toInt_toBitVec, HasModel.toNat_toInt_add_one_sub_toInt (Nat.zero_lt_succ _)]
 
 public instance instRxcLawfulHasSize : Rxc.LawfulHasSize Int32 := by
-  simp +instances only [instUpwardEnumerable_eq, instRxcHasSize_eq]
+  rw [instUpwardEnumerable_eq, instRxcHasSize_eq]
   infer_instance
 public instance : Rxc.IsAlwaysFinite Int32 := by exact inferInstance
 
@@ -481,7 +486,7 @@ theorem instRxiHasSize_eq :
     HasModel.encode, HasModel.toNat_two_pow_sub_one_sub_toInt (show 32 > 0 by omega)]
 
 public instance instRxiLawfulHasSize : Rxi.LawfulHasSize Int32 := by
-  simp +instances only [instUpwardEnumerable_eq, instRxiHasSize_eq]
+  rw [instUpwardEnumerable_eq, instRxiHasSize_eq]
   infer_instance
 public instance instRxiIsAlwaysFinite : Rxi.IsAlwaysFinite Int32 := by exact inferInstance
 
@@ -528,9 +533,10 @@ instance : HasModel Int64 (BitVec 64) where
   decode x := .ofBitVec x
   encode_decode := by simp
   decode_encode := by simp
-  le_iff_encode_le := by simp +instances [Int64.le_iff_toBitVec_sle, BitVec.Signed.instLE]
-  lt_iff_encode_lt := by simp +instances [Int64.lt_iff_toBitVec_slt, BitVec.Signed.instLT]
+  le_iff_encode_le := by simp [LE.le, Int64.le]
+  lt_iff_encode_lt := by simp [LT.lt, Int64.lt]
 
+set_option backward.whnf.reducibleClassField false in
 theorem instUpwardEnumerable_eq :
     instUpwardEnumerable = HasModel.instUpwardEnumerable := by
   apply UpwardEnumerable.ext
@@ -538,15 +544,16 @@ theorem instUpwardEnumerable_eq :
     apply HasModel.succ?_eq_of_technicalCondition
     simp [HasModel.encode, succ?, ← Int64.toBitVec_inj, toBitVec_minValueSealed_eq_intMinSealed]
   · ext
-    simp +instances [HasModel.succMany?_eq, instUpwardEnumerable, HasModel.encode, HasModel.decode,
+    simp only [HasModel.succMany?_eq]
+    simp [UpwardEnumerable.succMany?, HasModel.encode, HasModel.decode,
       ← toInt_toBitVec, toBitVec_maxValueSealed_eq_intMaxSealed, ofIntLE_eq_ofInt]
 
 instance : LawfulUpwardEnumerable Int64 := by
-  simp +instances only [instUpwardEnumerable_eq]
+  rw [instUpwardEnumerable_eq]
   infer_instance
 
 instance : LawfulUpwardEnumerableLE Int64 := by
-  simp +instances only [instUpwardEnumerable_eq]
+  rw [instUpwardEnumerable_eq]
   infer_instance
 
 public instance instRxcHasSize : Rxc.HasSize Int64 where
@@ -558,7 +565,7 @@ theorem instRxcHasSize_eq :
     ← toInt_toBitVec, HasModel.toNat_toInt_add_one_sub_toInt (Nat.zero_lt_succ _)]
 
 public instance instRxcLawfulHasSize : Rxc.LawfulHasSize Int64 := by
-  simp +instances only [instUpwardEnumerable_eq, instRxcHasSize_eq]
+  rw [instUpwardEnumerable_eq, instRxcHasSize_eq]
   infer_instance
 public instance : Rxc.IsAlwaysFinite Int64 := by exact inferInstance
 
@@ -575,7 +582,7 @@ theorem instRxiHasSize_eq :
     HasModel.encode, HasModel.toNat_two_pow_sub_one_sub_toInt (show 64 > 0 by omega)]
 
 public instance instRxiLawfulHasSize : Rxi.LawfulHasSize Int64 := by
-  simp +instances only [instUpwardEnumerable_eq, instRxiHasSize_eq]
+  rw [instUpwardEnumerable_eq, instRxiHasSize_eq]
   infer_instance
 public instance instRxiIsAlwaysFinite : Rxi.IsAlwaysFinite Int64 := by exact inferInstance
 
@@ -627,9 +634,10 @@ instance : HasModel ISize (BitVec System.Platform.numBits) where
   decode x := .ofBitVec x
   encode_decode := by simp
   decode_encode := by simp
-  le_iff_encode_le := by simp +instances [ISize.le_iff_toBitVec_sle, BitVec.Signed.instLE]
-  lt_iff_encode_lt := by simp +instances [ISize.lt_iff_toBitVec_slt, BitVec.Signed.instLT]
+  le_iff_encode_le := by simp [LE.le, ISize.le]
+  lt_iff_encode_lt := by simp [LT.lt, ISize.lt]
 
+set_option backward.whnf.reducibleClassField false in
 theorem instUpwardEnumerable_eq :
     instUpwardEnumerable = HasModel.instUpwardEnumerable := by
   apply UpwardEnumerable.ext
@@ -637,15 +645,16 @@ theorem instUpwardEnumerable_eq :
     apply HasModel.succ?_eq_of_technicalCondition
     simp [HasModel.encode, succ?, ← ISize.toBitVec_inj, toBitVec_minValueSealed_eq_intMinSealed]
   · ext
-    simp +instances [HasModel.succMany?_eq, instUpwardEnumerable, HasModel.encode, HasModel.decode,
+    simp only [HasModel.succMany?_eq]
+    simp [UpwardEnumerable.succMany?, HasModel.encode, HasModel.decode,
       ← toInt_toBitVec, toBitVec_maxValueSealed_eq_intMaxSealed, ofIntLE_eq_ofInt]
 
 instance : LawfulUpwardEnumerable ISize := by
-  simp +instances only [instUpwardEnumerable_eq]
+  rw [instUpwardEnumerable_eq]
   infer_instance
 
 instance : LawfulUpwardEnumerableLE ISize := by
-  simp +instances only [instUpwardEnumerable_eq]
+  rw [instUpwardEnumerable_eq]
   infer_instance
 
 public instance instRxcHasSize : Rxc.HasSize ISize where
@@ -657,7 +666,7 @@ theorem instRxcHasSize_eq :
     ← toInt_toBitVec, HasModel.toNat_toInt_add_one_sub_toInt System.Platform.numBits_pos]
 
 public instance instRxcLawfulHasSize : Rxc.LawfulHasSize ISize := by
-  simp +instances only [instUpwardEnumerable_eq, instRxcHasSize_eq]
+  rw [instUpwardEnumerable_eq, instRxcHasSize_eq]
   infer_instance
 public instance : Rxc.IsAlwaysFinite ISize := by exact inferInstance
 
@@ -674,7 +683,7 @@ theorem instRxiHasSize_eq :
     HasModel.encode, HasModel.toNat_two_pow_sub_one_sub_toInt System.Platform.numBits_pos]
 
 public instance instRxiLawfulHasSize : Rxi.LawfulHasSize ISize := by
-  simp +instances only [instUpwardEnumerable_eq, instRxiHasSize_eq]
+  rw [instUpwardEnumerable_eq, instRxiHasSize_eq]
   infer_instance
 public instance instRxiIsAlwaysFinite : Rxi.IsAlwaysFinite ISize := by exact inferInstance
 

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

@@ -438,6 +438,7 @@ protected theorem UpwardEnumerable.le_iff {α : Type u} [LE α] [UpwardEnumerabl
     [LawfulUpwardEnumerableLE α] {a b : α} : a ≤ b ↔ UpwardEnumerable.LE a b :=
   LawfulUpwardEnumerableLE.le_iff a b
 
+@[expose, implicit_reducible]
 def UpwardEnumerable.instLETransOfLawfulUpwardEnumerableLE {α : Type u} [LE α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] :
     Trans (α := α) (· ≤ ·) (· ≤ ·) (· ≤ ·) where
@@ -502,12 +503,13 @@ protected theorem UpwardEnumerable.lt_succ_iff {α : Type u} [UpwardEnumerable
       ← succMany?_eq_some_iff_succMany] at hn
     exact ⟨n, hn⟩
 
+@[expose, implicit_reducible]
 def UpwardEnumerable.instLTTransOfLawfulUpwardEnumerableLT {α : Type u} [LT α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] :
     Trans (α := α) (· < ·) (· < ·) (· < ·) where
   trans := by simpa [UpwardEnumerable.lt_iff] using @UpwardEnumerable.lt_trans
 
-def UpwardEnumerable.instLawfulOrderLTOfLawfulUpwardEnumerableLT {α : Type u} [LT α] [LE α]
+theorem UpwardEnumerable.instLawfulOrderLTOfLawfulUpwardEnumerableLT {α : Type u} [LT α] [LE α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
     [LawfulUpwardEnumerableLE α] :
     LawfulOrderLT α where

src/Init/Data/SInt/Basic.lean

@@ -409,7 +409,7 @@ Examples:
  * `(if (5 : Int8) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : Int8) < 7) by decide`
 -/
-@[extern "lean_int8_dec_lt", instance_reducible]
+@[extern "lean_int8_dec_lt", implicit_reducible]
 def Int8.decLt (a b : Int8) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
 
@@ -425,7 +425,7 @@ Examples:
  * `(if (15 : Int8) ≤ 5 then "yes" else "no") = "no"`
  * `show (7 : Int8) ≤ 7 by decide`
 -/
-@[extern "lean_int8_dec_le", instance_reducible]
+@[extern "lean_int8_dec_le", implicit_reducible]
 def Int8.decLe (a b : Int8) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
@@ -778,7 +778,7 @@ Examples:
  * `(if (5 : Int16) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : Int16) < 7) by decide`
 -/
-@[extern "lean_int16_dec_lt", instance_reducible]
+@[extern "lean_int16_dec_lt", implicit_reducible]
 def Int16.decLt (a b : Int16) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
 
@@ -794,7 +794,7 @@ Examples:
  * `(if (15 : Int16) ≤ 5 then "yes" else "no") = "no"`
  * `show (7 : Int16) ≤ 7 by decide`
 -/
-@[extern "lean_int16_dec_le", instance_reducible]
+@[extern "lean_int16_dec_le", implicit_reducible]
 def Int16.decLe (a b : Int16) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
@@ -1163,7 +1163,7 @@ Examples:
  * `(if (5 : Int32) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : Int32) < 7) by decide`
 -/
-@[extern "lean_int32_dec_lt", instance_reducible]
+@[extern "lean_int32_dec_lt", implicit_reducible]
 def Int32.decLt (a b : Int32) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
 
@@ -1179,7 +1179,7 @@ Examples:
  * `(if (15 : Int32) ≤ 5 then "yes" else "no") = "no"`
  * `show (7 : Int32) ≤ 7 by decide`
 -/
-@[extern "lean_int32_dec_le", instance_reducible]
+@[extern "lean_int32_dec_le", implicit_reducible]
 def Int32.decLe (a b : Int32) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
@@ -1568,7 +1568,7 @@ Examples:
  * `(if (5 : Int64) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : Int64) < 7) by decide`
 -/
-@[extern "lean_int64_dec_lt", instance_reducible]
+@[extern "lean_int64_dec_lt", implicit_reducible]
 def Int64.decLt (a b : Int64) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
 /--
@@ -1583,7 +1583,7 @@ Examples:
  * `(if (15 : Int64) ≤ 5 then "yes" else "no") = "no"`
  * `show (7 : Int64) ≤ 7 by decide`
 -/
-@[extern "lean_int64_dec_le", instance_reducible]
+@[extern "lean_int64_dec_le", implicit_reducible]
 def Int64.decLe (a b : Int64) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
@@ -1958,7 +1958,7 @@ Examples:
  * `(if (5 : ISize) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : ISize) < 7) by decide`
 -/
-@[extern "lean_isize_dec_lt", instance_reducible]
+@[extern "lean_isize_dec_lt", implicit_reducible]
 def ISize.decLt (a b : ISize) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
 
@@ -1974,7 +1974,7 @@ Examples:
  * `(if (15 : ISize) ≤ 5 then "yes" else "no") = "no"`
  * `show (7 : ISize) ≤ 7 by decide`
 -/
-@[extern "lean_isize_dec_le", instance_reducible]
+@[extern "lean_isize_dec_le", implicit_reducible]
 def ISize.decLe (a b : ISize) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 

src/Init/Data/Slice/Array/Iterator.lean

@@ -43,7 +43,7 @@ private def SubarrayIterator.instFinitelessRelation : FinitenessRelation (Subarr
   Rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.xs.stop - it.internalState.xs.start)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by
-    simp [IterM.IsPlausibleSuccessorOf, IterM.IsPlausibleStep, Iterator.IsPlausibleStep, step] at h
+    simp [IterM.IsPlausibleSuccessorOf, IterM.IsPlausibleStep, Iterator.IsPlausibleStep, step, instIteratorSubarrayIteratorId] at h -- TODO
     split at h
     · cases h
       simp only [InvImage, Subarray.stop, Subarray.start, WellFoundedRelation.rel, InvImage, sizeOf_nat]
@@ -55,16 +55,13 @@ instance SubarrayIterator.instFinite : Finite (SubarrayIterator α) Id :=
 
 instance [Monad m] : IteratorLoop (SubarrayIterator α) Id m := .defaultImplementation
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 def Subarray.instToIterator :=
   ToIterator.of (γ := Slice (Internal.SubarrayData α)) (β := α) (SubarrayIterator α) (⟨⟨·⟩⟩)
 attribute [instance] Subarray.instToIterator
 
 universe v w
 
-instance : SliceSize (Internal.SubarrayData α) where
-  size s := s.internalRepresentation.stop - s.internalRepresentation.start
-
 instance {α : Type u} {m : Type v → Type w} [Monad m] : ForIn m (Subarray α) α :=
   inferInstance
 
@@ -76,45 +73,6 @@ explicitly provide the wrapper function `Subarray.foldlM` for `Slice.foldlM`, pr
 specific docstring.
 -/
 
-/--
-Folds a monadic operation from left to right over the elements in a subarray.
-An accumulator of type `β` is constructed by starting with `init` and monadically combining each
-element of the subarray with the current accumulator value in turn. The monad in question may permit
-early termination or repetition.
-Examples:
-```lean example
-#eval #["red", "green", "blue"].toSubarray.foldlM (init := "") fun acc x => do
-  let l ← Option.guard (· ≠ 0) x.length
-  return s!"{acc}({l}){x} "
-```
-```output
-some "(3)red (5)green (4)blue "
-```
-```lean example
-#eval #["red", "green", "blue"].toSubarray.foldlM (init := 0) fun acc x => do
-  let l ← Option.guard (· ≠ 5) x.length
-  return s!"{acc}({l}){x} "
-```
-```output
-none
-```
--/
-@[inline]
-def Subarray.foldlM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (as : Subarray α) : m β :=
-  Slice.foldlM f (init := init) as
-
-/--
-Folds an operation from left to right over the elements in a subarray.
-An accumulator of type `β` is constructed by starting with `init` and combining each
-element of the subarray with the current accumulator value in turn.
-Examples:
- * `#["red", "green", "blue"].toSubarray.foldl (· + ·.length) 0 = 12`
- * `#["red", "green", "blue"].toSubarray.popFront.foldl (· + ·.length) 0 = 9`
--/
-@[inline]
-def Subarray.foldl {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : Subarray α) : β :=
-  Slice.foldl f (init := init) as
-
 /--
 The implementation of `ForIn.forIn` for `Subarray`, which allows it to be used with `for` loops in
 `do`-notation.
@@ -126,16 +84,12 @@ def Subarray.forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
 /--
 Allocates a new array that contains the contents of the subarray.
 -/
-@[coe]
-def Subarray.toArray (s : Subarray α) : Array α :=
+@[expose, coe]
+def Subarray.copy (s : Subarray α) : Array α :=
   Slice.toArray s
 
 instance instCoeSubarrayArray : Coe (Subarray α) (Array α) :=
-  ⟨Subarray.toArray⟩
-
-@[inherit_doc Subarray.toArray]
-def Subarray.copy (s : Subarray α) : Array α :=
-  Slice.toArray s
+  ⟨Subarray.copy⟩
 
 @[simp]
 theorem Subarray.copy_eq_toArray {s : Subarray α} :
@@ -149,7 +103,7 @@ theorem Subarray.sliceToArray_eq_toArray {s : Subarray α} :
 
 namespace Array
 
-@[inherit_doc Subarray.toArray]
+@[inherit_doc Subarray.copy]
 def ofSubarray (s : Subarray α) : Array α :=
   Slice.toArray s
 

src/Init/Data/Slice/Array/Lemmas.lean

@@ -36,11 +36,11 @@ theorem step_eq {it : Iter (α := SubarrayIterator α) α} :
         ⟨.yield ⟨⟨it.1.xs.array, it.1.xs.start + 1, it.1.xs.stop, by omega, by assumption⟩⟩
             (it.1.xs.array[it.1.xs.start]'(by omega)),
           (by
-            simp_all [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+            simp_all [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep, instIteratorSubarrayIteratorId, -- TODO
               SubarrayIterator.step, Iter.toIterM])⟩
       else
         ⟨.done, (by
-            simpa [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+            simpa [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep, instIteratorSubarrayIteratorId, -- TODO
               SubarrayIterator.step] using h)⟩ := by
   simp only [Iter.step, IterM.Step.toPure, Iter.toIter_toIterM, IterStep.mapIterator, IterM.step,
     Iterator.step, SubarrayIterator.step, Id.run_pure, Shrink.inflate_deflate]
@@ -67,7 +67,6 @@ theorem val_step_eq {it : Iter (α := SubarrayIterator α) α} :
   simp only [step_eq]
   split <;> simp
 
-set_option backward.isDefEq.respectTransparency false in
 theorem toList_eq {α : Type u} {it : Iter (α := SubarrayIterator α) α} :
     it.toList =
       (it.internalState.xs.array.toList.take it.internalState.xs.stop).drop it.internalState.xs.start := by
@@ -84,7 +83,7 @@ theorem toList_eq {α : Type u} {it : Iter (α := SubarrayIterator α) α} :
         simp [it.internalState.xs.stop_le_array_size]
         exact h
       · simp [Subarray.array, Subarray.stop]
-    · simp only [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+    · simp only [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep, instIteratorSubarrayIteratorId, -- TODO
       IterStep.mapIterator_yield, SubarrayIterator.step]
       rw [dif_pos]; rotate_left; exact h
       rfl
@@ -106,13 +105,11 @@ theorem Internal.iter_eq {α : Type u} {s : Subarray α} :
     Internal.iter s = ⟨⟨s⟩⟩ :=
   rfl
 
-set_option backward.isDefEq.respectTransparency false in
 theorem Internal.toList_iter {α : Type u} {s : Subarray α} :
     (Internal.iter s).toList =
       (s.array.toList.take s.stop).drop s.start := by
   simp [SubarrayIterator.toList_eq, Internal.iter_eq_toIteratorIter, ToIterator.iter_eq]
 
-set_option backward.isDefEq.respectTransparency false in
 public instance : LawfulSliceSize (Internal.SubarrayData α) where
   lawful s := by
     simp [SliceSize.size, ToIterator.iter_eq,
@@ -121,7 +118,7 @@ public instance : LawfulSliceSize (Internal.SubarrayData α) where
 
 public theorem toArray_eq_sliceToArray {α : Type u} {s : Subarray α} :
     s.toArray = Slice.toArray s := by
-  simp [Subarray.toArray]
+  simp [Std.Slice.toArray]
 
 @[simp]
 public theorem forIn_toList {α : Type u} {s : Subarray α}
@@ -156,11 +153,11 @@ public theorem sliceFoldl_eq_foldl {α : Type u} {s : Subarray α} {f : β →
 public theorem foldlM_toList {m} [Monad m] {α : Type u} {s : Subarray α} {f}
     [LawfulMonad m] :
     s.toList.foldlM (init := init) f = s.foldlM (m := m) (init := init) f := by
-  simp [Std.Slice.foldlM_toList, sliceFoldlM_eq_foldlM]
+  simp [Std.Slice.foldlM_toList]
 
 public theorem foldl_toList {α : Type u} {s : Subarray α} {f} :
     s.toList.foldl (init := init) f = s.foldl (init := init) f := by
-  simp [Std.Slice.foldl_toList, sliceFoldl_eq_foldl]
+  simp [Std.Slice.foldl_toList]
 
 end Subarray
 
@@ -218,6 +215,7 @@ public theorem Array.stop_toSubarray {xs : Array α} {lo hi : Nat} :
     (xs.toSubarray lo hi).stop = min hi xs.size := by
   simp [toSubarray_eq_min, Subarray.stop]
 
+set_option backward.whnf.reducibleClassField false in
 public theorem Subarray.toList_eq {xs : Subarray α} :
     xs.toList = (xs.array.extract xs.start xs.stop).toList := by
   let aslice := xs
@@ -227,13 +225,13 @@ public theorem Subarray.toList_eq {xs : Subarray α} :
   change aslice.toList = _
   have : aslice.toList = lslice.toList := by
     rw [ListSlice.toList_eq]
-    simp +instances only [aslice, lslice, Std.Slice.toList, Internal.toList_iter]
+    simp only [aslice, lslice, Std.Slice.toList, Internal.toList_iter]
     apply List.ext_getElem
     · have : stop - start ≤ array.size - start := by omega
       simp [Subarray.start, Subarray.stop, *, Subarray.array]
     · intros
       simp [Subarray.array, Subarray.start, Subarray.stop]
-  simp +instances [this, ListSlice.toList_eq, lslice]
+  simp [this, ListSlice.toList_eq, lslice]
 
 -- TODO: The current `List.extract_eq_drop_take` should be called `List.extract_eq_take_drop`
 private theorem Std.Internal.List.extract_eq_drop_take' {l : List α} {start stop : Nat} :
@@ -251,21 +249,16 @@ public theorem Subarray.toList_eq_drop_take {xs : Subarray α} :
     xs.toList = (xs.array.toList.take xs.stop).drop xs.start := by
   rw [Subarray.toList_eq, Array.toList_extract, Std.Internal.List.extract_eq_drop_take']
 
-@[grind =]
-public theorem Subarray.size_eq {xs : Subarray α} :
-    xs.size = xs.stop - xs.start := by
-  simp [Subarray.size]
-
 @[simp, grind =]
 public theorem Subarray.size_drop {xs : Subarray α} :
     (xs.drop i).size = xs.size - i := by
-  simp only [size, stop, drop, start]
+  simp only [size_eq, stop, drop, start]
   omega
 
 @[simp, grind =]
 public theorem Subarray.size_take {xs : Subarray α} :
     (xs.take i).size = min i xs.size := by
-  simp only [size, stop, take, start]
+  simp only [size_eq, stop, take, start]
   omega
 
 public theorem Subarray.sliceSize_eq_size {xs : Subarray α} :
@@ -273,12 +266,12 @@ public theorem Subarray.sliceSize_eq_size {xs : Subarray α} :
   rfl
 
 public theorem Subarray.getElem_eq_getElem_array {xs : Subarray α} {h : i < xs.size} :
-    xs[i] = xs.array[xs.start + i]'(by simp only [size] at h; have := xs.stop_le_array_size; omega) := by
+    xs[i] = xs.array[xs.start + i]'(by simp only [size_eq] at h; have := xs.stop_le_array_size; omega) := by
   rfl
 
 public theorem Subarray.getElem_toList {xs : Subarray α} {h : i < xs.toList.length} :
     xs.toList[i]'h = xs[i]'(by simpa using h) := by
-  simp [getElem_eq_getElem_array, toList_eq_drop_take]; rfl
+  simp [getElem_eq_getElem_array, toList_eq_drop_take]
 
 public theorem Subarray.getElem_eq_getElem_toList {xs : Subarray α} {h : i < xs.size} :
     xs[i]'h = xs.toList[i]'(by simpa using h) := by
@@ -297,24 +290,24 @@ public theorem Subarray.toList_take {xs : Subarray α} :
 @[simp, grind =]
 public theorem Subarray.toArray_toList {xs : Subarray α} :
     xs.toList.toArray = xs.toArray := by
-  simp [Std.Slice.toList, Subarray.toArray, Std.Slice.toArray]
+  simp [Std.Slice.toList, Std.Slice.toArray, Std.Slice.toArray]
 
 @[simp, grind =]
 public theorem Subarray.toList_toArray {xs : Subarray α} :
     xs.toArray.toList = xs.toList := by
-  simp [Std.Slice.toList, Subarray.toArray, Std.Slice.toArray]
+  simp [Std.Slice.toList, Std.Slice.toArray, Std.Slice.toArray]
 
 @[simp, grind =]
 public theorem Subarray.length_toList {xs : Subarray α} :
     xs.toList.length = xs.size := by
   have : xs.start ≤ xs.stop := xs.internalRepresentation.start_le_stop
   have : xs.stop ≤ xs.array.size := xs.internalRepresentation.stop_le_array_size
-  simp [Subarray.toList_eq, Subarray.size]; omega
+  simp [Subarray.toList_eq, Subarray.size_eq]; omega
 
 @[simp, grind =]
 public theorem Subarray.size_toArray {xs : Subarray α} :
     xs.toArray.size = xs.size := by
-  simp [← Subarray.toArray_toList, Subarray.size, Slice.size, SliceSize.size, start, stop]
+  simp [← Subarray.toArray_toList, Subarray.size_eq, start, stop]
 
 namespace Array
 
@@ -708,7 +701,7 @@ public theorem toList_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
     Array.start_toSubarray, Array.stop_toSubarray, Array.toList_extract, List.take_drop,
     List.take_take]
   rw [Nat.add_sub_cancel' (by omega)]
-  simp [Subarray.size, ← Array.length_toList, ← List.take_eq_take_min, Nat.add_comm xs.start]
+  simp [Subarray.size_eq, ← Array.length_toList, ← List.take_eq_take_min, Nat.add_comm xs.start]
 
 @[simp, grind =]
 public theorem toArray_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
@@ -718,7 +711,7 @@ public theorem toArray_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
 @[simp, grind =]
 public theorem size_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
     xs[lo...hi].size = min hi xs.size - lo := by
-  simp [← Subarray.length_toList]
+  simp [← length_toList, - length_toList_eq_size]
 
 public theorem mkSlice_rcc_eq_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
     xs[lo...=hi] = xs[lo...(hi + 1)] := by
@@ -738,7 +731,7 @@ public theorem toArray_mkSlice_rcc {xs : Subarray α} {lo hi : Nat} :
 @[simp, grind =]
 public theorem size_mkSlice_rcc {xs : Subarray α} {lo hi : Nat} :
     xs[lo...=hi].size = min (hi + 1) xs.size - lo := by
-  simp [← Subarray.length_toList]
+  simp [← length_toList, - length_toList_eq_size]
 
 public theorem mkSlice_rci_eq_mkSlice_rco {xs : Subarray α} {lo : Nat} :
     xs[lo...*] = xs[lo...xs.size] := by
@@ -758,7 +751,7 @@ public theorem toArray_mkSlice_rci {xs : Subarray α} {lo : Nat} :
 @[simp, grind =]
 public theorem size_mkSlice_rci {xs : Subarray α} {lo : Nat} :
     xs[lo...*].size = xs.size - lo := by
-  simp [← Subarray.length_toList]
+  simp [← length_toList, - length_toList_eq_size]
 
 public theorem mkSlice_roc_eq_mkSlice_roo {xs : Subarray α} {lo hi : Nat} :
     xs[lo<...=hi] = xs[lo<...(hi + 1)] := by
@@ -787,7 +780,7 @@ public theorem toArray_mkSlice_roo {xs : Subarray α} {lo hi : Nat} :
 @[simp, grind =]
 public theorem size_mkSlice_roo {xs : Subarray α} {lo hi : Nat} :
     xs[lo<...hi].size = min hi xs.size - (lo + 1) := by
-  simp [← Subarray.length_toList]
+  simp [← length_toList, - length_toList_eq_size]
 
 public theorem mkSlice_roc_eq_mkSlice_rcc {xs : Subarray α} {lo hi : Nat} :
     xs[lo<...=hi] = xs[(lo + 1)...=hi] := by
@@ -806,7 +799,7 @@ public theorem toArray_mkSlice_roc {xs : Subarray α} {lo hi : Nat} :
 @[simp, grind =]
 public theorem size_mkSlice_roc {xs : Subarray α} {lo hi : Nat} :
     xs[lo<...=hi].size = min (hi + 1) xs.size - (lo + 1) := by
-  simp [← Subarray.length_toList]
+  simp [← length_toList, - length_toList_eq_size]
 
 public theorem mkSlice_roi_eq_mkSlice_rci {xs : Subarray α} {lo : Nat} :
     xs[lo<...*] = xs[(lo + 1)...*] := by
@@ -830,7 +823,7 @@ public theorem toArray_mkSlice_roi {xs : Subarray α} {lo : Nat} :
 @[simp, grind =]
 public theorem size_mkSlice_roi {xs : Subarray α} {lo : Nat} :
     xs[lo<...*].size = xs.size - (lo + 1) := by
-  simp [← Subarray.length_toList]
+  simp [← length_toList, - length_toList_eq_size]
 
 public theorem mkSlice_ric_eq_mkSlice_rio {xs : Subarray α} {hi : Nat} :
     xs[*...=hi] = xs[*...(hi + 1)] := by
@@ -859,7 +852,7 @@ public theorem toArray_mkSlice_rio {xs : Subarray α} {hi : Nat} :
 @[simp, grind =]
 public theorem size_mkSlice_rio {xs : Subarray α} {hi : Nat} :
     xs[*...hi].size = min hi xs.size := by
-  simp [← Subarray.length_toList]
+  simp [← length_toList, - length_toList_eq_size]
 
 public theorem mkSlice_ric_eq_mkSlice_rcc {xs : Subarray α} {hi : Nat} :
     xs[*...=hi] = xs[0...=hi] := by
@@ -880,7 +873,7 @@ public theorem toArray_mkSlice_ric {xs : Subarray α} {hi : Nat} :
 @[simp, grind =]
 public theorem size_mkSlice_ric {xs : Subarray α} {hi : Nat} :
     xs[*...=hi].size = min (hi + 1) xs.size := by
-  simp [← Subarray.length_toList]
+  simp [← length_toList, - length_toList_eq_size]
 
 @[simp, grind =, grind =]
 public theorem mkSlice_rii {xs : Subarray α} :

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

@@ -21,7 +21,7 @@ open Std Std.Slice Std.PRange
 /--
 Internal representation of `ListSlice`, which is an abbreviation for `Slice ListSliceData`.
 -/
-public class Std.Slice.Internal.ListSliceData (α : Type u) where
+public structure Std.Slice.Internal.ListSliceData (α : Type u) where
   /-- The relevant suffix of the underlying list. -/
   list : List α
   /-- The maximum length of the slice, starting at the beginning of `list`. -/

src/Init/Data/Slice/List/Iterator.lean

@@ -22,7 +22,7 @@ open Std Slice PRange Iterators
 
 variable {α : Type u}
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 def ListSlice.instToIterator :=
   ToIterator.of (γ := Slice (Internal.ListSliceData α)) _ (fun s => match s.internalRepresentation.stop with
       | some n => s.internalRepresentation.list.iter.take n

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

@@ -70,6 +70,7 @@ end ListSlice
 
 namespace List
 
+set_option backward.whnf.reducibleClassField false in
 @[simp, grind =]
 public theorem toList_mkSlice_rco {xs : List α} {lo hi : Nat} :
     xs[lo...hi].toList = (xs.take hi).drop lo := by
@@ -110,6 +111,7 @@ public theorem size_mkSlice_rcc {xs : List α} {lo hi : Nat} :
     xs[lo...=hi].size = min (hi + 1) xs.length - lo := by
   simp [← length_toList_eq_size]
 
+set_option backward.whnf.reducibleClassField false in
 @[simp, grind =]
 public theorem toList_mkSlice_rci {xs : List α} {lo : Nat} :
     xs[lo...*].toList = xs.drop lo := by
@@ -288,6 +290,7 @@ section ListSubslices
 
 namespace ListSlice
 
+set_option backward.whnf.reducibleClassField false in
 @[simp, grind =]
 public theorem toList_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} :
     xs[lo...hi].toList = (xs.toList.take hi).drop lo := by
@@ -326,6 +329,7 @@ public theorem size_mkSlice_rcc {xs : ListSlice α} {lo hi : Nat} :
     xs[lo...=hi].size = min (hi + 1) xs.size - lo := by
   simp [← length_toList_eq_size]
 
+set_option backward.whnf.reducibleClassField false in
 @[simp, grind =]
 public theorem toList_mkSlice_rci {xs : ListSlice α} {lo : Nat} :
     xs[lo...*].toList = xs.toList.drop lo := by

src/Init/Data/Slice/Operations.lean

@@ -51,12 +51,12 @@ Returns the number of elements with distinct indices in the given slice.
 
 Example: `#[1, 1, 1][0...2].size = 2`.
 -/
-@[always_inline, inline]
+@[expose, always_inline, inline, suggest_for Subarray.size]
 def size (s : Slice γ) [SliceSize γ] :=
   SliceSize.size s
 
 /-- Allocates a new array that contains the elements of the slice. -/
-@[always_inline, inline]
+@[always_inline, inline, suggest_for Subarray.toArray]
 def toArray [ToIterator (Slice γ) Id α β] [Iterator α Id β]
     (s : Slice γ) : Array β :=
   Internal.iter s |>.toArray
@@ -103,7 +103,7 @@ some "(3)red (5)green (4)blue "
 none
 ```
 -/
-@[always_inline, inline]
+@[always_inline, inline, suggest_for Subarray.foldlM]
 def foldlM {γ : Type u} {β : Type v}
     {δ : Type w} {m : Type w → Type w'} [Monad m] (f : δ → β → m δ) (init : δ)
     [ToIterator (Slice γ) Id α β] [Iterator α Id β]
@@ -119,7 +119,7 @@ Examples for the special case of subarrays:
  * `#["red", "green", "blue"].toSubarray.foldl (· + ·.length) 0 = 12`
  * `#["red", "green", "blue"].toSubarray.popFront.foldl (· + ·.length) 0 = 9`
 -/
-@[always_inline, inline]
+@[always_inline, inline, suggest_for Subarray.foldl]
 def foldl {γ : Type u} {β : Type v}
     {δ : Type w} (f : δ → β → δ) (init : δ)
     [ToIterator (Slice γ) Id α β] [Iterator α Id β]

src/Init/Data/String.lean

@@ -30,3 +30,4 @@ public import Init.Data.String.FindPos
 public import Init.Data.String.Subslice
 public import Init.Data.String.Iter
 public import Init.Data.String.Iterate
+public import Init.Data.String.Hashable

src/Init/Data/String/Hashable.lean

@@ -0,0 +1,20 @@
+/-
+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.Hashable
+public import Init.Data.String.Defs
+
+public section
+
+namespace String
+
+deriving instance Hashable for String.Pos.Raw
+deriving instance Hashable for String.Pos
+deriving instance Hashable for String.Slice.Pos
+
+end String

src/Init/Data/String/Lemmas/Pattern/Basic.lean

@@ -296,7 +296,6 @@ class LawfulToForwardSearcherModel {ρ : Type} (pat : ρ) [ForwardPatternModel p
     [∀ s, Std.Iterators.Finite (σ s) Id] : Prop where
   isValidSearchFrom_toList (s) : IsValidSearchFrom pat s.startPos (ToForwardSearcher.toSearcher pat s).toList
 
-set_option backward.isDefEq.respectTransparency false in
 theorem LawfulToForwardSearcherModel.defaultImplementation {pat : ρ} [ForwardPattern pat] [StrictForwardPattern pat]
     [ForwardPatternModel pat] [LawfulForwardPatternModel pat] :
     letI : ToForwardSearcher pat (ToForwardSearcher.DefaultForwardSearcher pat) := .defaultImplementation

src/Init/Data/String/Lemmas/Pattern/Split.lean

@@ -197,7 +197,6 @@ theorem IsValidSearchFrom.splitFromSteps_eq_extend_split {ρ : Type} (pat : ρ)
     · exact h' p hp₁ hp
     · exact rej _ (Std.not_lt.1 hp) hp₂
 
-set_option backward.isDefEq.respectTransparency false in
 theorem SplitIterator.toList_eq_splitFromSteps {ρ : Type} {pat : ρ} {σ : Slice → Type}
     [ToForwardSearcher pat σ]
     [∀ s, Std.Iterator (σ s) Id (SearchStep s)] [∀ s, Std.Iterators.Finite (σ s) Id] {s : Slice}

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

@@ -296,6 +296,12 @@ theorem Pos.Splits.next {s : String} {p : s.Pos}
   obtain ⟨rfl, rfl, rfl⟩ := by simpa using h.eq (splits_next_right p hp)
   exact splits_next p hp
 
+/-- You might want to invoke `Pos.Splits.exists_eq_append_singleton` to be able to apply this. -/
+theorem Pos.Splits.of_next {s : String} {p : s.Pos} {hp}
+    (h : (p.next hp).Splits (t₁ ++ singleton c) t₂) : p.Splits t₁ (singleton c ++ t₂) := by
+  obtain ⟨⟨rfl, rfl⟩, rfl⟩ := by simpa using h.eq (splits_next p hp)
+  exact splits_next_right p hp
+
 /-- You might want to invoke `Slice.Pos.Splits.exists_eq_singleton_append` to be able to apply this. -/
 theorem Slice.Pos.Splits.next {s : Slice} {p : s.Pos}
     (h : p.Splits t₁ (singleton c ++ t₂)) : (p.next h.ne_endPos_of_singleton).Splits (t₁ ++ singleton c) t₂ := by
@@ -303,6 +309,12 @@ theorem Slice.Pos.Splits.next {s : Slice} {p : s.Pos}
   obtain ⟨rfl, rfl, rfl⟩ := by simpa using h.eq (splits_next_right p hp)
   exact splits_next p hp
 
+/-- You might want to invoke `Slice.Pos.Splits.exists_eq_append_singleton` to be able to apply this. -/
+theorem Slice.Pos.Splits.of_next {s : Slice} {p : s.Pos} {hp}
+    (h : (p.next hp).Splits (t₁ ++ singleton c) t₂) : p.Splits t₁ (singleton c ++ t₂) := by
+  obtain ⟨⟨rfl, rfl⟩, rfl⟩ := by simpa using h.eq (splits_next p hp)
+  exact splits_next_right p hp
+
 /-- You might want to invoke `Pos.Splits.exists_eq_singleton_append_of_ne_startPos` to be able to apply this. -/
 theorem Pos.Splits.prev {s : String} {p : s.Pos}
     (h : p.Splits (t₁ ++ singleton c) t₂) : (p.prev h.ne_startPos_of_singleton).Splits t₁ (singleton c ++ t₂) := by
@@ -310,6 +322,12 @@ theorem Pos.Splits.prev {s : String} {p : s.Pos}
   obtain ⟨⟨rfl, rfl⟩, rfl⟩ := by simpa using h.eq (splits_prev_right p hp)
   exact splits_prev p hp
 
+/-- You might want to invoke `Pos.Splits.exists_eq_append_singleton_of_ne_startPos` to be able to apply this. -/
+theorem Pos.Splits.of_prev {s : String} {p : s.Pos} {hp}
+    (h : (p.prev hp).Splits t₁ (singleton c ++ t₂)) : p.Splits (t₁ ++ singleton c) t₂ := by
+  obtain ⟨rfl, rfl, rfl⟩ := by simpa using h.eq (splits_prev p hp)
+  exact splits_prev_right p hp
+
 /-- You might want to invoke `Slice.Pos.Splits.exists_eq_singleton_append_of_ne_startPos` to be able to apply this. -/
 theorem Slice.Pos.Splits.prev {s : Slice} {p : s.Pos}
     (h : p.Splits (t₁ ++ singleton c) t₂) : (p.prev h.ne_startPos_of_singleton).Splits t₁ (singleton c ++ t₂) := by
@@ -317,6 +335,12 @@ theorem Slice.Pos.Splits.prev {s : Slice} {p : s.Pos}
   obtain ⟨⟨rfl, rfl⟩, rfl⟩ := by simpa using h.eq (splits_prev_right p hp)
   exact splits_prev p hp
 
+/-- You might want to invoke `Slice.Pos.Splits.exists_eq_append_singleton_of_ne_startPos` to be able to apply this. -/
+theorem Slice.Pos.Splits.of_prev {s : Slice} {p : s.Pos} {hp}
+    (h : (p.prev hp).Splits t₁ (singleton c ++ t₂)) : p.Splits (t₁ ++ singleton c) t₂ := by
+  obtain ⟨rfl, rfl, rfl⟩ := by simpa using h.eq (splits_prev p hp)
+  exact splits_prev_right p hp
+
 theorem Slice.sliceTo_copy_eq_iff_exists_splits {s : Slice} {p : s.Pos} {t₁ : String} :
     (s.sliceTo p).copy = t₁ ↔ ∃ t₂, p.Splits t₁ t₂ := by
   refine ⟨?_, ?_⟩

src/Init/Data/String/OrderInstances.lean

@@ -9,7 +9,9 @@ prelude
 public import Init.Data.String.Defs
 public import Init.Grind.ToInt
 public import Init.Data.Order.Classes
+import Init.Data.Order.PackageFactories
 import Init.Omega
+public import Init.Data.Order.PackageFactories
 
 public section
 
@@ -46,14 +48,14 @@ instance : Lean.Grind.ToInt.LE String.Pos.Raw (.ci 0) where
 instance : Lean.Grind.ToInt.LT String.Pos.Raw (.ci 0) where
   lt_iff := by simp [Pos.Raw.lt_iff]
 
-instance : Std.LawfulOrderLT String.Pos.Raw where
-  lt_iff := by order
+instance : Std.Total (α := String.Pos.Raw) (· ≤ ·) := ⟨fun _ _ => by order⟩
+instance : Trans (α := String.Pos.Raw) (· ≤ ·) (· ≤ ·) (· ≤ ·) := ⟨fun _ _ => by order⟩
+instance : Std.Antisymm (α := String.Pos.Raw) (· ≤ ·) := ⟨fun _ _ => by order⟩
 
-instance : Std.IsLinearOrder String.Pos.Raw where
-  le_refl := by order
-  le_trans := by order
-  le_antisymm := by order
-  le_total := by order
+instance : Std.LawfulOrderBEq String.Pos.Raw := ⟨fun _ _ => by order⟩
+instance : Std.LawfulOrderLT String.Pos.Raw := ⟨fun _ _ => by order⟩
+
+instance : Std.LinearOrderPackage String.Pos.Raw := .ofLE _
 
 end Pos.Raw
 
@@ -73,14 +75,14 @@ instance {s : String} : Lean.Grind.ToInt.LE s.Pos (.co 0 (s.utf8ByteSize + 1)) w
 instance {s : String} : Lean.Grind.ToInt.LT s.Pos (.co 0 (s.utf8ByteSize + 1)) where
   lt_iff := by simp [Pos.lt_iff, Pos.Raw.lt_iff]
 
-instance {s : String} : Std.LawfulOrderLT s.Pos where
-  lt_iff := by order
+instance {s : String} : Std.Total (α := s.Pos) (· ≤ ·) := ⟨fun _ _ => by order⟩
+instance {s : String} : Trans (α := s.Pos) (· ≤ ·) (· ≤ ·) (· ≤ ·) := ⟨fun _ _ => by order⟩
+instance {s : String} : Std.Antisymm (α := s.Pos) (· ≤ ·) := ⟨fun _ _ => by order⟩
 
-instance {s : String} : Std.IsLinearOrder s.Pos where
-  le_refl := by order
-  le_trans := by order
-  le_antisymm := by order
-  le_total := by order
+instance {s : String} : Std.LawfulOrderBEq s.Pos := ⟨fun _ _ => by order⟩
+instance {s : String} : Std.LawfulOrderLT s.Pos := ⟨fun _ _ => by order⟩
+
+instance {s : String} : Std.LinearOrderPackage s.Pos := .ofLE _
 
 end Pos
 
@@ -100,14 +102,14 @@ instance {s : Slice} : Lean.Grind.ToInt.LE s.Pos (.co 0 (s.utf8ByteSize + 1)) wh
 instance {s : Slice} : Lean.Grind.ToInt.LT s.Pos (.co 0 (s.utf8ByteSize + 1)) where
   lt_iff := by simp [Pos.lt_iff, Pos.Raw.lt_iff]
 
-instance {s : Slice} : Std.LawfulOrderLT s.Pos where
-  lt_iff := by order
+instance {s : Slice} : Std.Total (α := s.Pos) (· ≤ ·) := ⟨fun _ _ => by order⟩
+instance {s : Slice} : Trans (α := s.Pos) (· ≤ ·) (· ≤ ·) (· ≤ ·) := ⟨fun _ _ => by order⟩
+instance {s : Slice} : Std.Antisymm (α := s.Pos) (· ≤ ·) := ⟨fun _ _ => by order⟩
 
-instance {s : Slice} : Std.IsLinearOrder s.Pos where
-  le_refl := by order
-  le_trans := by order
-  le_antisymm := by order
-  le_total := by order
+instance {s : Slice} : Std.LawfulOrderBEq s.Pos := ⟨fun _ _ => by order⟩
+instance {s : Slice} : Std.LawfulOrderLT s.Pos := ⟨fun _ _ => by order⟩
+
+instance {s : Slice} : Std.LinearOrderPackage s.Pos := .ofLE _
 
 end Slice.Pos
 

src/Init/Data/String/Pattern/Basic.lean

@@ -245,7 +245,7 @@ the given {name}`ForwardPattern` instance.
 It is sometimes possible to give a more efficient implementation; see {name}`ToForwardSearcher`
 for more details.
 -/
-@[inline]
+@[inline, implicit_reducible]
 def defaultImplementation [ForwardPattern pat] :
     ToForwardSearcher pat (DefaultForwardSearcher pat) where
   toSearcher := DefaultForwardSearcher.iter pat
@@ -450,7 +450,7 @@ the given {name}`BackwardPattern` instance.
 It is sometimes possible to give a more efficient implementation; see {name}`ToBackwardSearcher`
 for more details.
 -/
-@[inline]
+@[inline, implicit_reducible]
 def defaultImplementation [BackwardPattern pat] :
     ToBackwardSearcher pat (DefaultBackwardSearcher pat) where
   toSearcher := DefaultBackwardSearcher.iter pat

src/Init/Data/String/Pattern/String.lean

@@ -241,7 +241,7 @@ private def finitenessRelation :
     all_goals try
       cases h
       revert h'
-      simp only [Std.IterM.IsPlausibleStep, Std.Iterator.IsPlausibleStep]
+      simp only [Std.IterM.IsPlausibleStep, Std.Iterator.IsPlausibleStep, instIteratorIdSearchStep] -- TODO
       match it.internalState with
       | .emptyBefore pos =>
         rintro (⟨h, h'⟩|h') <;> simp [h', ForwardSliceSearcher.toOption, Option.lt, Prod.lex_def]

src/Init/Data/String/PosRaw.lean

@@ -57,9 +57,6 @@ instance (p₁ p₂ : String.Pos.Raw) : Decidable (p₁ ≤ p₂) :=
 instance (p₁ p₂ : String.Pos.Raw) : Decidable (p₁ < p₂) :=
   inferInstanceAs (Decidable (p₁.byteIdx < p₂.byteIdx))
 
-instance : Min String.Pos.Raw := minOfLe
-instance : Max String.Pos.Raw := maxOfLe
-
 @[simp]
 theorem Pos.Raw.byteIdx_sub_char {p : Pos.Raw} {c : Char} : (p - c).byteIdx = p.byteIdx - c.utf8Size := rfl
 

src/Init/Data/String/Slice.lean

@@ -176,7 +176,7 @@ private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
     match step with
     | .yield it'' out | .skip it'' =>
       obtain rfl : it' = it'' := by simpa using h.symm
-      simp only [Std.IterM.IsPlausibleStep, Std.Iterator.IsPlausibleStep] at h'
+      simp only [Std.IterM.IsPlausibleStep, Std.Iterator.IsPlausibleStep, instIteratorIdSubslice] at h' -- TODO
       revert h'
       match it, it' with
       | ⟨.operating _ searcher⟩, ⟨.operating _ searcher'⟩ => simp [SplitIterator.toOption, Option.lt]
@@ -287,7 +287,7 @@ private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
     match step with
     | .yield it'' out | .skip it'' =>
       obtain rfl : it' = it'' := by simpa using h.symm
-      simp only [Std.IterM.IsPlausibleStep, Std.Iterator.IsPlausibleStep] at h'
+      simp only [Std.IterM.IsPlausibleStep, Std.Iterator.IsPlausibleStep, instIteratorId] at h' -- TODO
       revert h'
       match it, it' with
       | ⟨.operating _ searcher⟩, ⟨.operating _ searcher'⟩ => simp [SplitInclusiveIterator.toOption, Option.lt]
@@ -627,7 +627,7 @@ private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
     match step with
     | .yield it'' out | .skip it'' =>
       obtain rfl : it' = it'' := by simpa using h.symm
-      simp only [Std.IterM.IsPlausibleStep, Std.Iterator.IsPlausibleStep] at h'
+      simp only [Std.IterM.IsPlausibleStep, Std.Iterator.IsPlausibleStep, instIteratorOfPure] at h' -- TODO
       revert h'
       match it, it' with
       | ⟨.operating _ searcher⟩, ⟨.operating _ searcher'⟩ => simp [RevSplitIterator.toOption, Option.lt]

src/Init/Data/UInt/Basic.lean

@@ -372,7 +372,7 @@ Examples:
  * `(if (5 : UInt16) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : UInt16) < 7) by decide`
 -/
-@[extern "lean_uint16_dec_lt", instance_reducible]
+@[extern "lean_uint16_dec_lt", implicit_reducible]
 def UInt16.decLt (a b : UInt16) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
 
@@ -389,7 +389,7 @@ Examples:
  * `(if (5 : UInt16) ≤ 15 then "yes" else "no") = "yes"`
  * `show (7 : UInt16) ≤ 7 by decide`
 -/
-@[extern "lean_uint16_dec_le", instance_reducible]
+@[extern "lean_uint16_dec_le", implicit_reducible]
 def UInt16.decLe (a b : UInt16) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
 
@@ -736,7 +736,7 @@ Examples:
  * `(if (5 : UInt64) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : UInt64) < 7) by decide`
 -/
-@[extern "lean_uint64_dec_lt", instance_reducible]
+@[extern "lean_uint64_dec_lt", implicit_reducible]
 def UInt64.decLt (a b : UInt64) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
 
@@ -752,7 +752,7 @@ Examples:
  * `(if (5 : UInt64) ≤ 15 then "yes" else "no") = "yes"`
  * `show (7 : UInt64) ≤ 7 by decide`
 -/
-@[extern "lean_uint64_dec_le", instance_reducible]
+@[extern "lean_uint64_dec_le", implicit_reducible]
 def UInt64.decLe (a b : UInt64) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
 

src/Init/Data/UInt/BasicAux.lean

@@ -399,7 +399,7 @@ Examples:
  * `(if (5 : USize) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : USize) < 7) by decide`
 -/
-@[extern "lean_usize_dec_lt", instance_reducible]
+@[extern "lean_usize_dec_lt", implicit_reducible]
 def USize.decLt (a b : USize) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
 
@@ -415,7 +415,7 @@ Examples:
  * `(if (5 : USize) ≤ 15 then "yes" else "no") = "yes"`
  * `show (7 : USize) ≤ 7 by decide`
 -/
-@[extern "lean_usize_dec_le", instance_reducible]
+@[extern "lean_usize_dec_le", implicit_reducible]
 def USize.decLe (a b : USize) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
 

src/Init/Data/Vector/Algebra.lean

@@ -75,7 +75,7 @@ def mul [Mul α] (xs ys : Vector α n) : Vector α n :=
 Pointwise multiplication of vectors.
 This is not a global instance as in some applications different multiplications may be relevant.
 -/
-@[instance_reducible]
+@[implicit_reducible]
 def instMul [Mul α] : Mul (Vector α n) := ⟨mul⟩
 
 section mul

src/Init/Data/Vector/Extract.lean

@@ -132,7 +132,6 @@ theorem extract_append {xs : Vector α n} {ys : Vector α m} {i j : Nat} :
   rcases ys with ⟨ys, rfl⟩
   simp
 
-set_option backward.isDefEq.respectTransparency false in
 theorem extract_append_left {xs : Vector α n} {ys : Vector α m} :
     (xs ++ ys).extract 0 n = (xs.extract 0 n).cast (by omega) := by
   ext i h
@@ -179,7 +178,7 @@ theorem mem_extract_iff_getElem {xs : Vector α n} {a : α} {i j : Nat} :
 theorem set_eq_push_extract_append_extract {xs : Vector α n} {i : Nat} (h : i < n) {a : α} :
     xs.set i a = ((xs.extract 0 i).push a ++ (xs.extract (i + 1) n)).cast (by omega) := by
   rcases xs with ⟨as, rfl⟩
-  simp [Array.set_eq_push_extract_append_extract]; rfl
+  simp [Array.set_eq_push_extract_append_extract]
 
 theorem extract_reverse {xs : Vector α n} {i j : Nat} :
     xs.reverse.extract i j = (xs.extract (n - j) (n - i)).reverse.cast (by omega) := by

src/Init/Data/Vector/Lemmas.lean

@@ -528,7 +528,7 @@ theorem toList_zip {as : Vector α n} {bs : Vector β n} :
 @[simp] theorem getElem_toList {xs : Vector α n} {i : Nat} (h : i < xs.toList.length) :
     xs.toList[i] = xs[i]'(by simpa using h) := by
   cases xs
-  simp; rfl
+  simp
 
 @[simp] theorem getElem?_toList {xs : Vector α n} {i : Nat} :
     xs.toList[i]? = xs[i]? := by
@@ -828,7 +828,6 @@ grind_pattern Vector.getElem?_eq_none => xs[i]? where
 theorem getElem?_eq_some_iff {xs : Vector α n} : xs[i]? = some b ↔ ∃ h : i < n, xs[i] = b :=
   _root_.getElem?_eq_some_iff
 
-@[grind →]
 theorem getElem_of_getElem? {xs : Vector α n} : xs[i]? = some a → ∃ h : i < n, xs[i] = a :=
   getElem?_eq_some_iff.mp
 

src/Init/Data/Vector/OfFn.lean

@@ -119,7 +119,6 @@ theorem ofFnM_succ {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} :
       pure (as.push a)) := by
   simp [ofFnM, ofFnM_go_succ]
 
-set_option backward.isDefEq.respectTransparency false in
 theorem ofFnM_add {n m} [Monad m] [LawfulMonad m] {f : Fin (n + k) → m α} :
     ofFnM f = (do
       let as ← ofFnM (fun i => f (i.castLE (Nat.le_add_right n k)))

src/Init/Dynamic.lean

@@ -47,6 +47,7 @@ Creates a `TypeName` instance.
 For safety, it is required that the constant `typeName` is definitionally equal
 to `α`.
 -/
+@[implicit_reducible]
 unsafe def TypeName.mk (α : Type u) (typeName : Name) : TypeName α :=
   ⟨unsafeCast typeName⟩
 

src/Init/Grind/Module/Basic.lean

@@ -60,7 +60,7 @@ class NatModule (M : Type u) extends AddCommMonoid M where
   /-- Scalar multiplication by a successor. -/
   add_one_nsmul : ∀ n : Nat, ∀ a : M, (n + 1) • a = n • a + a
 
-attribute [instance_reducible] NatModule.nsmul
+attribute [implicit_reducible] NatModule.nsmul
 attribute [instance 100] NatModule.toAddCommMonoid NatModule.nsmul
 
 /--
@@ -83,7 +83,7 @@ class IntModule (M : Type u) extends AddCommGroup M where
   /-- Scalar multiplication by natural numbers is consistent with scalar multiplication by integers. -/
   zsmul_natCast_eq_nsmul : ∀ n : Nat, ∀ a : M, (n : Int) • a = n • a
 
-attribute [instance_reducible] IntModule.zsmul
+attribute [implicit_reducible] IntModule.zsmul
 attribute [instance 100] IntModule.toAddCommGroup IntModule.zsmul
 
 namespace IntModule
@@ -266,6 +266,7 @@ export NoNatZeroDivisors (no_nat_zero_divisors)
 namespace NoNatZeroDivisors
 
 /-- Alternative constructor for `NoNatZeroDivisors` when we have an `IntModule`. -/
+@[implicit_reducible]
 def mk' {α} [IntModule α]
     (eq_zero_of_mul_eq_zero : ∀ (k : Nat) (a : α), k ≠ 0 → k • a = 0 → a = 0) :
     NoNatZeroDivisors α where

src/Init/Grind/Module/Envelope.lean

@@ -204,7 +204,7 @@ theorem zsmul_natCast_eq_nsmul (n : Nat) (a : Q α) : zsmul (n : Int) a = nsmul
   induction a using Q.ind with | _ a
   rcases a with ⟨a₁, a₂⟩; simp; omega
 
-@[instance_reducible]
+@[implicit_reducible]
 def ofNatModule : IntModule (Q α) := {
   nsmul := ⟨nsmul⟩,
   zsmul := ⟨zsmul⟩,

src/Init/Grind/Ring/Basic.lean

@@ -94,7 +94,7 @@ class Semiring (α : Type u) extends Add α, Mul α where
   -/
   nsmul_eq_natCast_mul : ∀ n : Nat, ∀ a : α, n • a = Nat.cast n * a := by intros; rfl
 
-attribute [instance_reducible] Semiring.npow Semiring.ofNat Semiring.natCast
+attribute [implicit_reducible] Semiring.npow Semiring.ofNat Semiring.natCast
 
 /--
 A ring, i.e. a type equipped with addition, negation, multiplication, and a map from the integers,
@@ -120,7 +120,7 @@ class Ring (α : Type u) extends Semiring α, Neg α, Sub α where
   /-- The canonical map from the integers is consistent with negation. -/
   intCast_neg : ∀ i : Int, Int.cast (R := α) (-i) = -Int.cast i := by intros; rfl
 
-attribute [instance_reducible] Ring.intCast Ring.zsmul
+attribute [implicit_reducible] Ring.intCast Ring.zsmul
 
 /--
 A commutative semiring, i.e. a semiring with commutative multiplication.
@@ -184,7 +184,7 @@ theorem natCast_succ (n : Nat) : ((n + 1 : Nat) : α) = ((n : α) + 1) := by
 
 theorem ofNat_mul (a b : Nat) : OfNat.ofNat (α := α) (a * b) = OfNat.ofNat a * OfNat.ofNat b := by
   induction b with
-  | zero => simp [Nat.mul_zero, mul_zero]; rfl
+  | zero => simp [Nat.mul_zero, mul_zero]
   | succ a ih => rw [Nat.mul_succ, ofNat_add, ih, ofNat_add, left_distrib, mul_one]
 
 theorem natCast_mul (a b : Nat) : ((a * b : Nat) : α) = ((a : α) * (b : α)) := by
@@ -501,6 +501,7 @@ private theorem mk'_aux {x y : Nat} (p : Nat) (h : y ≤ x) :
       omega
 
 /-- Alternative constructor when `α` is a `Ring`. -/
+@[implicit_reducible]
 def mk' (p : Nat) (α : Type u) [Ring α]
     (ofNat_eq_zero_iff : ∀ (x : Nat), OfNat.ofNat (α := α) x = 0 ↔ x % p = 0) : IsCharP α p where
   ofNat_ext_iff {x y} := by

src/Init/Grind/Ring/CommSolver.lean

@@ -21,6 +21,7 @@ import Init.Data.Int.LemmasAux
 import Init.Data.Nat.Linear
 import Init.Grind.Ordered.Order
 import Init.Omega
+import Init.WFTactics
 
 @[expose] public section
 

src/Init/Grind/Ring/Envelope.lean

@@ -245,7 +245,7 @@ theorem neg_zsmul (i : Int) (a : Q α) : zsmul (-i) a = neg (zsmul i a) := by
     · have : i = 0 := by omega
       simp [this]
 
-@[instance_reducible]
+@[implicit_reducible]
 def ofSemiring : Ring (Q α) := {
   nsmul := ⟨nsmul⟩
   zsmul := ⟨zsmul⟩
@@ -330,7 +330,7 @@ theorem toQ_inj [AddRightCancel α] {a b : α} : toQ a = toQ b → a = b := by
   obtain ⟨k, h₁⟩ := h₁
   exact AddRightCancel.add_right_cancel a b k h₁
 
-instance [Semiring α] [AddRightCancel α] [NoNatZeroDivisors α] : NoNatZeroDivisors (OfSemiring.Q α) where
+instance (priority := high) [Semiring α] [AddRightCancel α] [NoNatZeroDivisors α] : NoNatZeroDivisors (OfSemiring.Q α) where
   no_nat_zero_divisors := by
     intro k a b h₁ h₂
     replace h₂ : mul (natCast k) a = mul (natCast k) b := h₂
@@ -346,7 +346,7 @@ instance [Semiring α] [AddRightCancel α] [NoNatZeroDivisors α] : NoNatZeroDiv
     replace h₂ := NoNatZeroDivisors.no_nat_zero_divisors k (a₁ + b₂) (a₂ + b₁) h₁ h₂
     apply Quot.sound; simp [r]; exists 0; simp [h₂]
 
-instance {p} [Semiring α] [AddRightCancel α] [IsCharP α p] : IsCharP (OfSemiring.Q α) p where
+instance (priority := high) {p} [Semiring α] [AddRightCancel α] [IsCharP α p] : IsCharP (OfSemiring.Q α) p where
   ofNat_ext_iff := by
     intro x y
     constructor
@@ -366,7 +366,7 @@ instance {p} [Semiring α] [AddRightCancel α] [IsCharP α p] : IsCharP (OfSemir
       apply Quot.sound
       exists 0; simp [← Semiring.ofNat_eq_natCast, this]
 
-instance [LE α] [IsPreorder α] [OrderedAdd α] : LE (OfSemiring.Q α) where
+instance (priority := high) [LE α] [IsPreorder α] [OrderedAdd α] : LE (OfSemiring.Q α) where
   le a b := Q.liftOn₂ a b (fun (a, b) (c, d) => a + d ≤ b + c)
     (by intro (a₁, b₁) (a₂, b₂) (a₃, b₃) (a₄, b₄)
         simp; intro k₁ h₁ k₂ h₂
@@ -382,14 +382,14 @@ instance [LE α] [IsPreorder α] [OrderedAdd α] : LE (OfSemiring.Q α) where
         rw [this]; clear this
         rw [← OrderedAdd.add_le_left_iff])
 
-instance [LE α] [IsPreorder α] [OrderedAdd α] : LT (OfSemiring.Q α) where
+instance (priority := high) [LE α] [IsPreorder α] [OrderedAdd α] : LT (OfSemiring.Q α) where
   lt a b := a ≤ b ∧ ¬b ≤ a
 
 @[local simp] theorem mk_le_mk [LE α] [IsPreorder α] [OrderedAdd α] {a₁ a₂ b₁ b₂ : α}  :
     Q.mk (a₁, a₂) ≤ Q.mk (b₁, b₂) ↔ a₁ + b₂ ≤ a₂ + b₁ := by
   rfl
 
-instance [LE α] [IsPreorder α] [OrderedAdd α] : IsPreorder (OfSemiring.Q α) where
+instance (priority := high) [LE α] [IsPreorder α] [OrderedAdd α] : IsPreorder (OfSemiring.Q α) where
   le_refl a := by
     obtain ⟨⟨a₁, a₂⟩⟩ := a
     change Q.mk _ ≤ Q.mk _
@@ -424,7 +424,7 @@ theorem toQ_le [LE α] [IsPreorder α] [OrderedAdd α] {a b : α} : toQ a ≤ to
 theorem toQ_lt [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [OrderedAdd α] {a b : α} : toQ a < toQ b ↔ a < b := by
   simp [lt_iff_le_and_not_ge]
 
-instance [LE α] [IsPreorder α] [OrderedAdd α] : OrderedAdd (OfSemiring.Q α) where
+instance (priority := high) [LE α] [IsPreorder α] [OrderedAdd α] : OrderedAdd (OfSemiring.Q α) where
   add_le_left_iff := by
     intro a b c
     obtain ⟨⟨a₁, a₂⟩⟩ := a
@@ -438,7 +438,7 @@ instance [LE α] [IsPreorder α] [OrderedAdd α] : OrderedAdd (OfSemiring.Q α)
     rw [← OrderedAdd.add_le_left_iff]
 
 -- This perhaps works in more generality than `ExistsAddOfLT`?
-instance [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [OrderedRing α] [ExistsAddOfLT α] : OrderedRing (OfSemiring.Q α) where
+instance (priority := high) [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [OrderedRing α] [ExistsAddOfLT α] : OrderedRing (OfSemiring.Q α) where
   zero_lt_one := by
     rw [← toQ_ofNat, ← toQ_ofNat, toQ_lt]
     exact OrderedRing.zero_lt_one
@@ -506,12 +506,21 @@ theorem mul_comm (a b : OfSemiring.Q α) : OfSemiring.mul a b = OfSemiring.mul b
   obtain ⟨⟨b₁, b₂⟩⟩ := b
   apply Quot.sound; refine ⟨0, ?_⟩; simp; ac_rfl
 
-@[instance_reducible]
+@[implicit_reducible]
 def ofCommSemiring : CommRing (OfSemiring.Q α) :=
   { OfSemiring.ofSemiring with
     mul_comm := mul_comm }
 
-attribute [instance] ofCommSemiring
+attribute [instance high] ofCommSemiring
+instance (priority := high) [CommRing (OfSemiring.Q α)] : Add (OfSemiring.Q α) := by infer_instance
+instance (priority := high) [CommRing (OfSemiring.Q α)] : Sub (OfSemiring.Q α) := by infer_instance
+instance (priority := high) [CommRing (OfSemiring.Q α)] : Mul (OfSemiring.Q α) := by infer_instance
+instance (priority := high) [CommRing (OfSemiring.Q α)] : Neg (OfSemiring.Q α) := by infer_instance
+instance (priority := high) [CommRing (OfSemiring.Q α)] : OfNat (OfSemiring.Q α) n := by infer_instance
+attribute [local instance] Semiring.natCast Ring.intCast
+instance (priority := high) [CommRing (OfSemiring.Q α)] : NatCast (OfSemiring.Q α) := by infer_instance
+instance (priority := high) [CommRing (OfSemiring.Q α)] : IntCast (OfSemiring.Q α) := by infer_instance
+instance (priority := high) [CommRing (OfSemiring.Q α)] : HPow (OfSemiring.Q α) Nat (OfSemiring.Q α) := by infer_instance
 
 /-
 Remark: `↑a` is notation for `OfSemiring.toQ a`.

src/Init/Grind/Ring/Field.lean

@@ -38,7 +38,7 @@ class Field (α : Type u) extends CommRing α, Inv α, Div α where
   /-- Raising to a negative power is the inverse of raising to the positive power. -/
   zpow_neg : ∀ (a : α) (n : Int), a ^ (-n) = (a ^ n)⁻¹
 
-attribute [instance_reducible] Field.zpow
+attribute [implicit_reducible] Field.zpow
 attribute [instance 100] Field.toInv Field.toDiv Field.zpow
 
 namespace Field
@@ -223,6 +223,7 @@ theorem natCast_div_of_dvd {x y : Nat} (h : y ∣ x) (w : (y : α) ≠ 0) :
       mul_inv_cancel w, Semiring.mul_one]
 
 -- This is expensive as an instance. Let's see what breaks without it.
+@[implicit_reducible]
 def noNatZeroDivisors.ofIsCharPZero [IsCharP α 0] : NoNatZeroDivisors α := NoNatZeroDivisors.mk' <| by
   intro a b h w
   have := IsCharP.natCast_eq_zero_iff (α := α) 0 a

src/Init/Grind/Ring/ToInt.lean

@@ -15,6 +15,7 @@ public section
 namespace Lean.Grind
 
 /-- A `ToInt` instance on a semiring preserves powers if it preserves numerals and multiplication. -/
+@[implicit_reducible]
 def ToInt.pow_of_semiring [Semiring α] [ToInt α I] [ToInt.OfNat α I] [ToInt.Mul α I]
     (h₁ : I.isFinite) : ToInt.Pow α I where
   toInt_pow x n := by