feat: some missing Array grind annotations

.claude/CLAUDE.md

@@ -1,34 +1,14 @@
-To build Lean you should use `make -j -C build/release`.
-
-To run a test you should use `cd tests/lean/run && ./test_single.sh example_test.lean`.
-
-## New features
-
 When asked to implement new features:
 * begin by reviewing existing relevant code and tests
 * write comprehensive tests first (expecting that these will initially fail)
 * and then iterate on the implementation until the tests pass.
 
-All new tests should go in `tests/lean/run/`. These tests don't have expected output; we just check there are no errors. You should use `#guard_msgs` to check for specific messages.
+To build Lean you should use `make -j$(nproc) -C build/release`.
 
-## Success Criteria
+To run a test you should use `cd tests/lean/run && ./test_single.sh example_test.lean`.
 
-*Never* report success on a task unless you have verified both a clean build without errors, and that the relevant tests pass.
+*Never* report success on a task unless you have verified both a clean build without errors, and that the relevant tests pass. You have to keep working until you have verified both of these.
 
-## Build System Safety
+All new tests should go in `tests/lean/run/`. Note that these tests don't have expected output, and just run on a success or failure basis. So you should use `#guard_msgs` to check for specific messages.
 
-**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`
-- If a build is broken, ask the user before attempting any manual cleanup
-
-## LSP and IDE Diagnostics
-
-After rebuilding, LSP diagnostics may be stale until the user interacts with files. Trust command-line test results over IDE diagnostics.
-
-## Update prompting when the user is frustrated
-
-If the user expresses frustration with you, stop and ask them to help update this `.claude/CLAUDE.md` file with missing guidance.
-
-## Creating pull requests.
-
-All PRs must have a first paragraph starting with "This PR". This paragraph is automatically incorporated into release notes. Read `lean4/doc/dev/commit_convention.md` when making PRs.
+If you are not following best practices specific to this repository and the user expresses frustration, stop and ask them to help update this `.claude/CLAUDE.md` file with the missing guidance.

.github/workflows/build-template.yml

@@ -213,7 +213,7 @@ jobs:
           else
             ${{ matrix.tar || 'tar' }} cf - $dir | zstd -T0 --no-progress -o pack/$dir.tar.zst
           fi
-      - uses: actions/upload-artifact@v5
+      - uses: actions/upload-artifact@v4
         if: matrix.release
         with:
           name: build-${{ matrix.name }}

.github/workflows/ci.yml

@@ -106,54 +106,9 @@ jobs:
           TAG_NAME="${GITHUB_REF##*/}"
           echo "RELEASE_TAG=$TAG_NAME" >> "$GITHUB_OUTPUT"
 
-      - name: Validate CMakeLists.txt version matches tag
-        if: steps.set-release.outputs.RELEASE_TAG != ''
-        run: |
-          echo "Validating CMakeLists.txt version matches tag ${{ steps.set-release.outputs.RELEASE_TAG }}"
-
-          # Extract version values from CMakeLists.txt
-          CMAKE_MAJOR=$(grep -E "^set\(LEAN_VERSION_MAJOR " src/CMakeLists.txt | grep -oE '[0-9]+')
-          CMAKE_MINOR=$(grep -E "^set\(LEAN_VERSION_MINOR " src/CMakeLists.txt | grep -oE '[0-9]+')
-          CMAKE_PATCH=$(grep -E "^set\(LEAN_VERSION_PATCH " src/CMakeLists.txt | grep -oE '[0-9]+')
-          CMAKE_IS_RELEASE=$(grep -E "^set\(LEAN_VERSION_IS_RELEASE " src/CMakeLists.txt | grep -oE '[0-9]+')
-
-          # Expected values from tag parsing
-          TAG_MAJOR="${{ steps.set-release.outputs.LEAN_VERSION_MAJOR }}"
-          TAG_MINOR="${{ steps.set-release.outputs.LEAN_VERSION_MINOR }}"
-          TAG_PATCH="${{ steps.set-release.outputs.LEAN_VERSION_PATCH }}"
-
-          ERRORS=""
-
-          if [[ "$CMAKE_MAJOR" != "$TAG_MAJOR" ]]; then
-            ERRORS+="LEAN_VERSION_MAJOR: expected $TAG_MAJOR, found $CMAKE_MAJOR\n"
-          fi
-          if [[ "$CMAKE_MINOR" != "$TAG_MINOR" ]]; then
-            ERRORS+="LEAN_VERSION_MINOR: expected $TAG_MINOR, found $CMAKE_MINOR\n"
-          fi
-          if [[ "$CMAKE_PATCH" != "$TAG_PATCH" ]]; then
-            ERRORS+="LEAN_VERSION_PATCH: expected $TAG_PATCH, found $CMAKE_PATCH\n"
-          fi
-          if [[ "$CMAKE_IS_RELEASE" != "1" ]]; then
-            ERRORS+="LEAN_VERSION_IS_RELEASE: expected 1, found $CMAKE_IS_RELEASE\n"
-          fi
-
-          if [[ -n "$ERRORS" ]]; then
-            echo "::error::Version mismatch between tag and src/CMakeLists.txt"
-            echo ""
-            echo "Tag ${{ steps.set-release.outputs.RELEASE_TAG }} expects version $TAG_MAJOR.$TAG_MINOR.$TAG_PATCH"
-            echo "But src/CMakeLists.txt has mismatched values:"
-            echo -e "$ERRORS"
-            echo ""
-            echo "Fix src/CMakeLists.txt, delete the tag, and re-tag."
-            exit 1
-          fi
-
-          echo "Version validation passed: $TAG_MAJOR.$TAG_MINOR.$TAG_PATCH"
-
       # 0: PRs without special label
       # 1: PRs with `merge-ci` label, merge queue checks, master commits
-      # 2: nightlies
-      # 3: PRs with `release-ci` label, full releases
+      # 2: PRs with `release-ci` label, releases (incl. nightlies)
       - name: Set check level
         id: set-level
         # We do not use github.event.pull_request.labels.*.name here because
@@ -163,16 +118,14 @@ jobs:
           check_level=0
           fast=false
 
-          if [[ -n "${{ steps.set-release.outputs.RELEASE_TAG }}" || -n "${{ steps.set-release-custom.outputs.RELEASE_TAG }}" ]]; then
-            check_level=3
-          elif [[ -n "${{ steps.set-nightly.outputs.nightly }}" ]]; then
+          if [[ -n "${{ steps.set-nightly.outputs.nightly }}" || -n "${{ steps.set-release.outputs.RELEASE_TAG }}" || -n "${{ steps.set-release-custom.outputs.RELEASE_TAG }}" ]]; then
             check_level=2
           elif [[ "${{ github.event_name }}" != "pull_request" ]]; then
             check_level=1
           else
             labels="$(gh api repos/${{ github.repository_owner }}/${{ github.event.repository.name }}/pulls/${{ github.event.pull_request.number }} --jq '.labels')"
             if echo "$labels" | grep -q "release-ci"; then
-              check_level=3
+              check_level=2
             elif echo "$labels" | grep -q "merge-ci"; then
               check_level=1
             fi
@@ -257,22 +210,17 @@ jobs:
                 "test": true,
                 "CMAKE_PRESET": "reldebug",
               },
-              {
+              // TODO: suddenly started failing in CI
+              /*{
                 "name": "Linux fsanitize",
-                // Always run on large if available, more reliable regarding timeouts
-                "os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
+                "os": "ubuntu-latest",
                 "enabled": level >= 2,
-                // do not fail nightlies on this for now
-                "secondary": level <= 2,
                 "test": true,
                 // turn off custom allocator & symbolic functions to make LSAN do its magic
                 "CMAKE_PRESET": "sanitize",
-                // `StackOverflow*` correctly triggers ubsan
-                // `reverse-ffi` fails to link in sanitizers
-                // `interactive` and `async_select_channel` fail nondeterministically, would need to
-                // be investigated.
-                "CTEST_OPTIONS": "-E 'StackOverflow|reverse-ffi|interactive|async_select_channel'"
-              },
+                // exclude seriously slow/problematic tests (laketests crash)
+                "CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
+              },*/
               {
                 "name": "macOS",
                 "os": "macos-15-intel",
@@ -304,7 +252,7 @@ jobs:
               },
               {
                 "name": "Windows",
-                "os": large && (fast || level >= 2) ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
+                "os": large && (fast || level == 2) ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
                 "release": true,
                 "enabled": level >= 2,
                 "test": true,
@@ -427,11 +375,11 @@ jobs:
     runs-on: ubuntu-latest
     needs: build
     steps:
-      - uses: actions/download-artifact@v6
+      - uses: actions/download-artifact@v5
         with:
           path: artifacts
       - name: Release
-        uses: softprops/action-gh-release@6da8fa9354ddfdc4aeace5fc48d7f679b5214090
+        uses: softprops/action-gh-release@6cbd405e2c4e67a21c47fa9e383d020e4e28b836
         with:
           files: artifacts/*/*
           fail_on_unmatched_files: true
@@ -459,7 +407,7 @@ jobs:
           # Doesn't seem to be working when additionally fetching from lean4-nightly
           #filter: tree:0
           token: ${{ secrets.PUSH_NIGHTLY_TOKEN }}
-      - uses: actions/download-artifact@v6
+      - uses: actions/download-artifact@v5
         with:
           path: artifacts
       - name: Prepare Nightly Release
@@ -477,7 +425,7 @@ jobs:
           echo -e "\n*Full commit log*\n" >> diff.md
           git log --oneline "$last_tag"..HEAD | sed 's/^/* /' >> diff.md
       - name: Release Nightly
-        uses: softprops/action-gh-release@6da8fa9354ddfdc4aeace5fc48d7f679b5214090
+        uses: softprops/action-gh-release@6cbd405e2c4e67a21c47fa9e383d020e4e28b836
         with:
           body_path: diff.md
           prerelease: true

.github/workflows/pr-release.yml

@@ -71,7 +71,7 @@ jobs:
           GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
       - name: Release (short format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: softprops/action-gh-release@6da8fa9354ddfdc4aeace5fc48d7f679b5214090
+        uses: softprops/action-gh-release@6cbd405e2c4e67a21c47fa9e383d020e4e28b836
         with:
           name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }}
           # There are coredumps files here as well, but all in deeper subdirectories.
@@ -86,7 +86,7 @@ jobs:
 
       - name: Release (SHA-suffixed format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: softprops/action-gh-release@6da8fa9354ddfdc4aeace5fc48d7f679b5214090
+        uses: softprops/action-gh-release@6cbd405e2c4e67a21c47fa9e383d020e4e28b836
         with:
           name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }} (${{ steps.workflow-info.outputs.sourceHeadSha }})
           # There are coredumps files here as well, but all in deeper subdirectories.

CMakePresets.json

@@ -41,7 +41,7 @@
         "SMALL_ALLOCATOR": "OFF",
         "USE_MIMALLOC": "OFF",
         "BSYMBOLIC": "OFF",
-        "LEAN_TEST_VARS": "MAIN_STACK_SIZE=16000 LSAN_OPTIONS=max_leaks=10"
+        "LEAN_TEST_VARS": "MAIN_STACK_SIZE=16000"
       },
       "generator": "Unix Makefiles",
       "binaryDir": "${sourceDir}/build/sanitize"

doc/dev/bootstrap.md

@@ -72,9 +72,6 @@ update the archived C source code of the stage 0 compiler in `stage0/src`.
 
 The github repository will automatically update stage0 on `master` once
 `src/stdlib_flags.h` and `stage0/src/stdlib_flags.h` are out of sync.
-To trigger this, modify `stage0/src/stdlib_flags.h` (e.g., by adding or changing
-a comment). When `update-stage0` runs, it will overwrite `stage0/src/stdlib_flags.h`
-with the contents of `src/stdlib_flags.h`, bringing them back in sync.
 
 NOTE: A full rebuild of stage 1 will only be triggered when the *committed* contents of `stage0/` are changed.
 Thus if you change files in it manually instead of through `update-stage0-commit` (see below) or fetching updates from git, you either need to commit those changes first or run `make -C build/release clean-stdlib`.

doc/dev/ffi.md

@@ -129,7 +129,8 @@ For all other modules imported by `lean`, the initializer is run without `builti
 Thus `[init]` functions are run iff their module is imported, regardless of whether they have native code available or not, while `[builtin_init]` functions are only run for native executable or plugins, regardless of whether their module is imported or not.
 `lean` uses built-in initializers for e.g. registering basic parsers that should be available even without importing their module (which is necessary for bootstrapping).
 
-The initializer for module `A.B` in a package `foo` is called `initialize_foo_A_B`. For modules in the Lean core (e.g., `Init.Prelude`), the initializer is called `initialize_Init_Prelude`. Module initializers will automatically initialize any imported modules. They are also idempotent (when run with the same `builtin` flag), but not thread-safe.
+The initializer for module `A.B` is called `initialize_A_B` and will automatically initialize any imported modules.
+Module initializers are idempotent (when run with the same `builtin` flag), but not thread-safe.
 
 **Important for process-related functionality**: If your application needs to use process-related functions from libuv, such as `Std.Internal.IO.Process.getProcessTitle` and `Std.Internal.IO.Process.setProcessTitle`, you must call `lean_setup_args(argc, argv)` (which returns a potentially modified `argv` that must be used in place of the original) **before** calling `lean_initialize()` or `lean_initialize_runtime_module()`. This sets up process handling capabilities correctly, which is essential for certain system-level operations that Lean's runtime may depend on.
 

releases_drafts/module-system.md

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

script/AnalyzeGrindAnnotations.lean

@@ -0,0 +1,132 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean
+
+namespace Lean.Meta.Grind.Analyzer
+
+
+/-!
+A simple E-matching annotation analyzer.
+For each theorem annotated as an E-matching candidate, it creates an artificial goal, executes `grind` and shows the
+number of instances created.
+For a theorem of the form `params -> type`, the artificial goal is of the form `params -> type -> False`.
+-/
+
+/--
+`grind` configuration for the analyzer. We disable case-splits and lookahead,
+increase the number of generations, and limit the number of instances generated.
+-/
+def config : Grind.Config := {
+  splits       := 0
+  lookahead    := false
+  mbtc         := false
+  ematch       := 20
+  instances    := 100
+  gen          := 10
+}
+
+structure Config where
+  /-- Minimum number of instantiations to trigger summary report -/
+  min : Nat := 10
+  /-- Minimum number of instantiations to trigger detailed report -/
+  detailed : Nat := 50
+
+def mkParams : MetaM Params := do
+  let params ← Grind.mkParams config
+  let ematch ← getEMatchTheorems
+  let casesTypes ← Grind.getCasesTypes
+  return { params with ematch, casesTypes }
+
+/-- Returns the total number of generated instances.  -/
+private def sum (cs : PHashMap Origin Nat) : Nat := Id.run do
+  let mut r := 0
+  for (_, c) in cs do
+    r := r + c
+  return r
+
+private def thmsToMessageData (thms : PHashMap Origin Nat) : MetaM MessageData := do
+  let data := thms.toArray.filterMap fun (origin, c) =>
+    match origin with
+    | .decl declName => some (declName, c)
+    | _ => none
+  let data := data.qsort fun (d₁, c₁) (d₂, c₂) => if c₁ == c₂ then Name.lt d₁ d₂ else c₁ > c₂
+  let data ← data.mapM fun (declName, counter) =>
+    return .trace { cls := `thm } m!"{.ofConst (← mkConstWithLevelParams declName)} ↦ {counter}" #[]
+  return .trace { cls := `thm } "instances" data
+
+/--
+Analyzes theorem `declName`. That is, creates the artificial goal based on `declName` type,
+and invokes `grind` on it.
+-/
+def analyzeEMatchTheorem (declName : Name) (c : Config) : MetaM Unit := do
+  let info ← getConstInfo declName
+  let mvarId ← forallTelescope info.type fun _ type => do
+    withLocalDeclD `h type fun _ => do
+      return (← mkFreshExprMVar (mkConst ``False)).mvarId!
+  let result ← Grind.main mvarId (← mkParams) (pure ())
+  let thms := result.counters.thm
+  let s := sum thms
+  if s > c.min then
+    IO.println s!"{declName} : {s}"
+  if s > c.detailed then
+    logInfo m!"{declName}\n{← thmsToMessageData thms}"
+
+-- Not sure why this is failing: `down_pure` perhaps has an unnecessary universe parameter?
+run_meta analyzeEMatchTheorem ``Std.Do.SPred.down_pure {}
+
+/-- Analyzes all theorems in the standard library marked as E-matching theorems. -/
+def analyzeEMatchTheorems (c : Config := {}) : MetaM Unit := do
+  let origins := (← getEMatchTheorems).getOrigins
+  let decls := origins.filterMap fun | .decl declName => some declName | _ => none
+  for declName in decls.mergeSort Name.lt do
+    try
+      analyzeEMatchTheorem declName c
+    catch e =>
+      logError m!"{declName} failed with {e.toMessageData}"
+  logInfo m!"Finished analyzing {decls.length} theorems"
+
+/-- Macro for analyzing E-match theorems with unlimited heartbeats -/
+macro "#analyzeEMatchTheorems" : command => `(
+  set_option maxHeartbeats 0 in
+  run_meta analyzeEMatchTheorems
+)
+
+#analyzeEMatchTheorems
+
+-- -- We can analyze specific theorems using commands such as
+set_option trace.grind.ematch.instance true
+
+-- 1. grind immediately sees `(#[] : Array α) = ([] : List α).toArray` but probably this should be hidden.
+-- 2. `Vector.toArray_empty` keys on `Array.mk []` rather than `#v[].toArray`
+-- I guess we could add `(#[].extract _ _).extract _ _` as a stop pattern.
+run_meta analyzeEMatchTheorem ``Array.extract_empty {}
+
+-- Neither `Option.bind_some` nor `Option.bind_fun_some` fire, because the terms appear inside
+-- lambdas. So we get crazy things like:
+-- `fun x => ((some x).bind some).bind fun x => (some x).bind fun x => (some x).bind some`
+-- We could consider replacing `filterMap_some` with
+-- `filterMap g (filterMap f xs) = filterMap (f >=> g) xs`
+-- to avoid the lambda that `grind` struggles with, but this would require more API around the fish.
+run_meta analyzeEMatchTheorem ``Array.filterMap_some {}
+
+-- Not entirely certain what is wrong here, but certainly
+-- `eq_empty_of_append_eq_empty` is firing too often.
+-- Ideally we could instantiate this is we fine `xs ++ ys` in the same equivalence class,
+-- note just as soon as we see `xs ++ ys`.
+-- I've tried removing this in https://github.com/leanprover/lean4/pull/10162
+run_meta analyzeEMatchTheorem ``Array.range'_succ {}
+
+-- Perhaps the same story here.
+run_meta analyzeEMatchTheorem ``Array.range_succ {}
+
+-- `zip_map_left` and `zip_map_right` are bad grind lemmas,
+-- checking if they can be removed in https://github.com/leanprover/lean4/pull/10163
+run_meta analyzeEMatchTheorem ``Array.zip_map {}
+
+-- It seems crazy to me that as soon as we have `0 >>> n = 0`, we instantiate based on the
+-- pattern `0 >>> n >>> m` by substituting `0` into `0 >>> n` to produce the `0 >>> n >>> n`.
+-- I don't think any forbidden subterms can help us here. I don't know what to do. :-(
+run_meta analyzeEMatchTheorem ``Int.zero_shiftRight {}

script/Shake.lean

@@ -300,7 +300,7 @@ def parseHeaderFromString (text path : String) :
     throw <| .userError "parse errors in file"
   -- the insertion point for `add` is the first newline after the imports
   let insertion := header.raw.getTailPos?.getD parserState.pos
-  let insertion := text.findAux (· == '\n') text.rawEndPos insertion + '\n'
+  let insertion := text.findAux (· == '\n') text.endPos insertion + '\n'
   pure (path, inputCtx, header, insertion)
 
 /-- Parse a source file to extract the location of the import lines, for edits and error messages.
@@ -593,16 +593,16 @@ def main (args : List String) : IO UInt32 := do
     for stx in imports do
       let mod := decodeImport stx
       if remove.contains mod || seen.contains mod then
-        out := out ++ String.Pos.Raw.extract text pos stx.raw.getPos?.get!
+        out := out ++ text.extract pos stx.raw.getPos?.get!
         -- We use the end position of the syntax, but include whitespace up to the first newline
         pos := text.findAux (· == '\n') text.rawEndPos stx.raw.getTailPos?.get! + '\n'
       seen := seen.insert mod
-    out := out ++ String.Pos.Raw.extract text pos insertion
+    out := out ++ text.extract pos insertion
     for mod in add do
       if !seen.contains mod then
         seen := seen.insert mod
         out := out ++ s!"{mod}\n"
-    out := out ++ String.Pos.Raw.extract text insertion text.rawEndPos
+    out := out ++ text.extract insertion text.rawEndPos
 
     IO.FS.writeFile path out
     count := count + 1

script/apply.lean

@@ -60,7 +60,7 @@ if (arity == fixed + {n}) \{
   for j in [n:max + 1] do
     let fs := mkFsArgs (j - n)
     let sep := if j = n then "" else ", "
-    emit s!"    case {j}: \{ obj* r = FN{j}(f)({fs}{sep}{args}); lean_free_object(f); return r; }\n"
+    emit s!"    case {j}: \{ obj* r = FN{j}(f)({fs}{sep}{args}); lean_free_small_object(f); return r; }\n"
   emit "    }
   }
   switch (arity) {\n"
@@ -162,7 +162,7 @@ static obj* fix_args(obj* f, unsigned n, obj*const* as) {
       for (unsigned i = 0; i < fixed; i++, source++, target++) {
           *target = *source;
       }
-      lean_free_object(f);
+      lean_free_small_object(f);
     }
     for (unsigned i = 0; i < n; i++, as++, target++) {
         *target = *as;

script/bench.sh

@@ -0,0 +1,96 @@
+#!/usr/bin/env bash
+set -euxo pipefail
+
+cmake --preset release 1>&2
+
+# We benchmark against stage2/bin to test new optimizations.
+timeout -s KILL 1h time make -C build/release -j$(nproc) stage3 1>&2
+export PATH=$PWD/build/release/stage2/bin:$PATH
+
+# The extra opts used to be passed to the Makefile during benchmarking only but with Lake it is
+# easier to configure them statically.
+cmake -B build/release/stage3 -S src -DLEAN_EXTRA_LAKEFILE_TOML='weakLeanArgs=["-Dprofiler=true", "-Dprofiler.threshold=9999999", "--stats"]' 1>&2
+
+(
+cd tests/bench
+timeout -s KILL 1h time temci exec --config speedcenter.yaml --in speedcenter.exec.velcom.yaml 1>&2
+temci report run_output.yaml --reporter codespeed2
+)
+
+if [ -d .git ]; then
+    DIR="$(git rev-parse @)"
+    BASE_URL="https://speed.lean-lang.org/lean4-out/$DIR"
+    {
+        cat <<'EOF'
+<!DOCTYPE html>
+<html>
+<head>
+  <meta charset="UTF-8">
+  <title>Lakeprof Report</title>
+</head>
+<h1>Lakeprof Report</h1>
+<button type="button" id="btn_fetch">View build trace in Perfetto</button>
+<script type="text/javascript">
+const ORIGIN = 'https://ui.perfetto.dev';
+
+const btnFetch = document.getElementById('btn_fetch');
+
+async function fetchAndOpen(traceUrl) {
+  const resp = await fetch(traceUrl);
+  // Error checking is left as an exercise to the reader.
+  const blob = await resp.blob();
+  const arrayBuffer = await blob.arrayBuffer();
+  openTrace(arrayBuffer, traceUrl);
+}
+
+function openTrace(arrayBuffer, traceUrl) {
+  const win = window.open(ORIGIN);
+  if (!win) {
+    btnFetch.style.background = '#f3ca63';
+  	btnFetch.onclick = () => openTrace(arrayBuffer);
+    btnFetch.innerText = 'Popups blocked, click here to open the trace file';
+    return;
+  }
+
+  const timer = setInterval(() => win.postMessage('PING', ORIGIN), 50);
+
+  const onMessageHandler = (evt) => {
+    if (evt.data !== 'PONG') return;
+
+    // We got a PONG, the UI is ready.
+    window.clearInterval(timer);
+    window.removeEventListener('message', onMessageHandler);
+
+    const reopenUrl = new URL(location.href);
+    reopenUrl.hash = `#reopen=${traceUrl}`;
+    win.postMessage({
+      perfetto: {
+        buffer: arrayBuffer,
+        title: 'Lake Build Trace',
+        url: reopenUrl.toString(),
+    }}, ORIGIN);
+  };
+
+  window.addEventListener('message', onMessageHandler);
+}
+
+// This is triggered when following the link from the Perfetto UI's sidebar.
+if (location.hash.startsWith('#reopen=')) {
+ const traceUrl = location.hash.substr(8);
+ fetchAndOpen(traceUrl);
+}
+EOF
+        cat <<EOF
+btnFetch.onclick = () => fetchAndOpen("$BASE_URL/lakeprof.trace_event");
+</script>
+EOF
+        echo "<pre><code>"
+        (cd src; lakeprof report -prc)
+        echo "</code></pre>"
+        echo "</body></html>"
+    } | tee index.html
+
+    curl -T index.html $BASE_URL/index.html
+    curl -T src/lakeprof.log $BASE_URL/lakeprof.log
+    curl -T src/lakeprof.trace_event $BASE_URL/lakeprof.trace_event
+fi

script/benchReelabRss.lean

@@ -10,16 +10,6 @@ Tests language server memory use by repeatedly re-elaborate a given file.
 NOTE: only works on Linux for now.
 -/
 
-def determineRSS (pid : UInt32) : IO Nat := do
-  let status ← IO.FS.readFile s!"/proc/{pid}/smaps_rollup"
-  let some rssLine := status.splitOn "\n" |>.find? (·.startsWith "Rss:")
-    | throw <| IO.userError "No RSS in proc status"
-  let rssLine := rssLine.dropPrefix "Rss:"
-  let rssLine := rssLine.dropWhile Char.isWhitespace
-  let some rssInKB := rssLine.takeWhile Char.isDigit |>.toNat?
-    | throw <| IO.userError "Cannot parse RSS"
-  return rssInKB
-
 def main (args : List String) : IO Unit := do
   let leanCmd :: file :: iters :: args := args | panic! "usage: script <lean> <file> <#iterations> <server-args>..."
   let file ← IO.FS.realPath file
@@ -44,14 +34,11 @@ def main (args : List String) : IO Unit := do
     let text ← IO.FS.readFile file
     let (_, headerEndPos, _) ← Elab.parseImports text
     let headerEndPos := FileMap.ofString text |>.leanPosToLspPos headerEndPos
-    let n := iters.toNat!
-    let mut lastRSS? : Option Nat := none
-    let mut totalRSSDelta : Int := 0
     let mut requestNo : Nat := 1
     let mut versionNo : Nat := 1
     Ipc.writeNotification ⟨"textDocument/didOpen", {
       textDocument := { uri := uri, languageId := "lean", version := 1, text := text } : DidOpenTextDocumentParams }⟩
-    for i in [0:n] do
+    for i in [0:iters.toNat!] do
       if i > 0 then
         versionNo := versionNo + 1
         let params : DidChangeTextDocumentParams := {
@@ -74,16 +61,9 @@ def main (args : List String) : IO Unit := do
           IO.eprintln diag.message
       requestNo := requestNo + 1
 
-      let rss ← determineRSS (← read).pid
-      -- The first `didChange` usually results in a significantly higher RSS increase than
-      -- the others, so we ignore it.
-      if i > 1 then
-        if let some lastRSS := lastRSS? then
-          totalRSSDelta := totalRSSDelta + ((rss : Int) - (lastRSS : Int))
-      lastRSS? := some rss
-
-    let avgRSSDelta := totalRSSDelta / (n - 2)
-    IO.println s!"avg-reelab-rss-delta: {avgRSSDelta}"
+      let status ← IO.FS.readFile s!"/proc/{(← read).pid}/status"
+      for line in status.splitOn "\n" |>.filter (·.startsWith "RssAnon") do
+        IO.eprintln line
 
     let _ ← Ipc.collectDiagnostics requestNo uri versionNo
     (← Ipc.stdin).writeLspMessage (Message.notification "exit" none)

script/benchReelabWatchdogRss.lean

@@ -1,89 +0,0 @@
-import Lean.Data.Lsp
-import Lean.Elab.Import
-open Lean
-open Lean.Lsp
-open Lean.JsonRpc
-
-/-!
-Tests watchdog memory use by repeatedly re-elaborate a given file.
-
-NOTE: only works on Linux for now.
--/
-
-def determineRSS (pid : UInt32) : IO Nat := do
-  let status ← IO.FS.readFile s!"/proc/{pid}/smaps_rollup"
-  let some rssLine := status.splitOn "\n" |>.find? (·.startsWith "Rss:")
-    | throw <| IO.userError "No RSS in proc status"
-  let rssLine := rssLine.dropPrefix "Rss:"
-  let rssLine := rssLine.dropWhile Char.isWhitespace
-  let some rssInKB := rssLine.takeWhile Char.isDigit |>.toNat?
-    | throw <| IO.userError "Cannot parse RSS"
-  return rssInKB
-
-def main (args : List String) : IO Unit := do
-  let leanCmd :: file :: iters :: args := args | panic! "usage: script <lean> <file> <#iterations> <server-args>..."
-  let file ← IO.FS.realPath file
-  let uri := s!"file://{file}"
-  Ipc.runWith leanCmd (#["--server", "-DstderrAsMessages=false"] ++ args ++ #[uri]) do
-    let capabilities := {
-      textDocument? := some {
-        completion? := some {
-          completionItem? := some {
-            insertReplaceSupport? := true
-          }
-        }
-      }
-    }
-    Ipc.writeRequest ⟨0, "initialize", { capabilities : InitializeParams }⟩
-    discard <| Ipc.readResponseAs 0 InitializeResult
-    Ipc.writeNotification ⟨"initialized", InitializedParams.mk⟩
-
-    let text ← IO.FS.readFile file
-    let (_, headerEndPos, _) ← Elab.parseImports text
-    let headerEndPos := FileMap.ofString text |>.leanPosToLspPos headerEndPos
-    let n := iters.toNat!
-    let mut lastRSS? : Option Nat := none
-    let mut totalRSSDelta : Int := 0
-    let mut requestNo : Nat := 1
-    let mut versionNo : Nat := 1
-    Ipc.writeNotification ⟨"textDocument/didOpen", {
-      textDocument := { uri := uri, languageId := "lean", version := 1, text := text } : DidOpenTextDocumentParams }⟩
-    for i in [0:iters.toNat!] do
-      if i > 0 then
-        versionNo := versionNo + 1
-        let params : DidChangeTextDocumentParams := {
-          textDocument := {
-            uri      := uri
-            version? := versionNo
-          }
-          contentChanges := #[TextDocumentContentChangeEvent.rangeChange {
-            start := headerEndPos
-            «end» := headerEndPos
-          } " "]
-        }
-        let params := toJson params
-        Ipc.writeNotification ⟨"textDocument/didChange", params⟩
-        requestNo := requestNo + 1
-
-      let diags ← Ipc.collectDiagnostics requestNo uri versionNo
-      if let some diags := diags then
-        for diag in diags.param.diagnostics do
-          IO.eprintln diag.message
-      requestNo := requestNo + 1
-
-      Ipc.waitForILeans requestNo uri versionNo
-
-      let rss ← determineRSS (← read).pid
-      -- The first `didChange` usually results in a significantly higher RSS increase than
-      -- the others, so we ignore it.
-      if i > 1 then
-        if let some lastRSS := lastRSS? then
-          totalRSSDelta := totalRSSDelta + ((rss : Int) - (lastRSS : Int))
-      lastRSS? := some rss
-
-    let avgRSSDelta := totalRSSDelta / (n - 2)
-    IO.println s!"avg-reelab-rss-delta: {avgRSSDelta}"
-
-    let _ ← Ipc.collectDiagnostics requestNo uri versionNo
-    Ipc.shutdown requestNo
-    discard <| Ipc.waitForExit

script/prepare-llvm-linux.sh

@@ -58,11 +58,7 @@ OPTIONS=()
 # We build cadical using the custom toolchain on Linux to avoid glibc versioning issues
 echo -n " -DLEAN_STANDALONE=ON -DCADICAL_USE_CUSTOM_CXX=ON"
 echo -n " -DCMAKE_CXX_COMPILER=$PWD/llvm-host/bin/clang++ -DLEAN_CXX_STDLIB='-Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic'"
-# these should also be used for cadical, so do not use `LEAN_EXTRA_CXX_FLAGS` here
-echo -n " -DCMAKE_CXX_FLAGS='--sysroot $PWD/llvm -idirafter $GLIBC_DEV/include ${EXTRA_FLAGS:-}'"
-# the above does not include linker flags which will be added below based on context, so skip the
-# generic check by cmake
-echo -n " -DCMAKE_C_COMPILER_WORKS=1 -DCMAKE_CXX_COMPILER_WORKS=1"
+echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm -idirafter $GLIBC_DEV/include ${EXTRA_FLAGS:-}'"
 # use target compiler directly when not cross-compiling
 if [[ -L llvm-host ]]; then
   echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang"

script/release_checklist.py

@@ -31,8 +31,6 @@ What this script does:
    - Ensures tags are merged into stable branches (for non-RC releases)
    - Verifies bump branches exist and are configured correctly
    - Special handling for ProofWidgets4 release tags
-   - For mathlib4: runs verify_version_tags.py to validate the release tag
-     (checks git/GitHub consistency, toolchain, elan, cache, and build)
 
 3. Optionally automates missing steps (when not in --dry-run mode):
    - Creates missing release tags using push_repo_release_tag.py
@@ -501,57 +499,6 @@ def check_proofwidgets4_release(repo_url, target_toolchain, github_token):
     print(f"     You will need to create and push a tag v0.0.{next_version}")
     return False
 
-def run_mathlib_verify_version_tags(toolchain, verbose=False):
-    """Run mathlib4's verify_version_tags.py script to validate the release tag.
-
-    This clones mathlib4 to a temp directory and runs the verification script.
-    Returns True if verification passes, False otherwise.
-    """
-    import tempfile
-
-    print(f"  ... Running mathlib4 verify_version_tags.py {toolchain}")
-
-    with tempfile.TemporaryDirectory() as tmpdir:
-        # Clone mathlib4 (shallow clone is sufficient for running the script)
-        clone_result = subprocess.run(
-            ['git', 'clone', '--depth', '1', 'https://github.com/leanprover-community/mathlib4.git', tmpdir],
-            capture_output=True,
-            text=True
-        )
-        if clone_result.returncode != 0:
-            print(f"  ❌ Failed to clone mathlib4: {clone_result.stderr.strip()[:200]}")
-            return False
-
-        # Run the verification script
-        script_path = os.path.join(tmpdir, 'scripts', 'verify_version_tags.py')
-        if not os.path.exists(script_path):
-            print(f"  ❌ verify_version_tags.py not found in mathlib4 (expected at scripts/verify_version_tags.py)")
-            return False
-
-        # Run from the mathlib4 directory so git operations work
-        result = subprocess.run(
-            ['python3', script_path, toolchain],
-            cwd=tmpdir,
-            capture_output=True,
-            text=True,
-            timeout=900  # 15 minutes timeout for cache download etc.
-        )
-
-        # Print output with indentation
-        if result.stdout:
-            for line in result.stdout.strip().split('\n'):
-                print(f"     {line}")
-        if result.stderr:
-            for line in result.stderr.strip().split('\n'):
-                print(f"     {line}")
-
-        if result.returncode != 0:
-            print(f"  ❌ mathlib4 verify_version_tags.py failed")
-            return False
-
-        print(f"  ✅ mathlib4 verify_version_tags.py passed")
-        return True
-
 def main():
     parser = argparse.ArgumentParser(description="Check release status of Lean4 repositories")
     parser.add_argument("toolchain", help="The toolchain version to check (e.g., v4.6.0)")
@@ -816,12 +763,6 @@ def main():
                 repo_status[name] = False
                 continue
 
-        # For mathlib4, run verify_version_tags.py to validate the release tag
-        if name == "mathlib4":
-            if not run_mathlib_verify_version_tags(toolchain, verbose):
-                repo_status[name] = False
-                continue
-
         repo_status[name] = success
 
     # Final check for lean4 master branch

src/CMakeLists.txt

@@ -10,7 +10,7 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 27)
+set(LEAN_VERSION_MINOR 26)
 set(LEAN_VERSION_PATCH 0)
 set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
@@ -42,7 +42,7 @@ if(LLD_PATH)
 endif()
 
 set(LEAN_EXTRA_LINKER_FLAGS ${LEAN_EXTRA_LINKER_FLAGS_DEFAULT} CACHE STRING "Additional flags used by the linker")
-set(LEAN_EXTRA_CXX_FLAGS "" CACHE STRING "Additional flags used by the C++ compiler. Unlike `CMAKE_CXX_FLAGS`, these will not be used to build e.g. cadical.")
+set(LEAN_EXTRA_CXX_FLAGS "" CACHE STRING "Additional flags used by the C++ compiler")
 set(LEAN_TEST_VARS "LEAN_CC=${CMAKE_C_COMPILER}" CACHE STRING "Additional environment variables used when running tests")
 
 if (NOT CMAKE_BUILD_TYPE)
@@ -191,7 +191,7 @@ endif()
 set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_SOURCE_DIR}/cmake/Modules")
 
 # Initialize CXXFLAGS.
-set(CMAKE_CXX_FLAGS                "${CMAKE_CXX_FLAGS} ${LEAN_EXTRA_CXX_FLAGS} -DLEAN_BUILD_TYPE=\"${CMAKE_BUILD_TYPE}\" -DLEAN_EXPORTING")
+set(CMAKE_CXX_FLAGS                "${LEAN_EXTRA_CXX_FLAGS} -DLEAN_BUILD_TYPE=\"${CMAKE_BUILD_TYPE}\" -DLEAN_EXPORTING")
 set(CMAKE_CXX_FLAGS_DEBUG          "-DLEAN_DEBUG")
 set(CMAKE_CXX_FLAGS_MINSIZEREL     "-DNDEBUG")
 set(CMAKE_CXX_FLAGS_RELEASE        "-DNDEBUG")

src/Init/Classical.lean

@@ -205,5 +205,3 @@ export Classical (imp_iff_right_iff imp_and_neg_imp_iff and_or_imp not_imp)
 
 /-- Show that an element extracted from `P : ∃ a, p a` using `P.choose` satisfies `p`. -/
 theorem Exists.choose_spec {p : α → Prop} (P : ∃ a, p a) : p P.choose := Classical.choose_spec P
-
-grind_pattern Exists.choose_spec => P.choose

src/Init/Control/Basic.lean

@@ -25,7 +25,7 @@ instances are provided for the same type.
 instance (priority := 500) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α where
   forIn x b f := forIn' x b fun a _ => f a
 
-@[simp] theorem forIn'_eq_forIn [d : Membership α ρ] [ForIn' m ρ α d] {β} (x : ρ) (b : β)
+@[simp] theorem forIn'_eq_forIn [d : Membership α ρ] [ForIn' m ρ α d] {β} [Monad m] (x : ρ) (b : β)
     (f : (a : α) → a ∈ x → β → m (ForInStep β)) (g : (a : α) → β → m (ForInStep β))
     (h : ∀ a m b, f a m b = g a b) :
     forIn' x b f = forIn x b g := by
@@ -40,7 +40,7 @@ instance (priority := 500) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α
   simp [h]
   rfl
 
-@[wf_preprocess] theorem forIn_eq_forIn' [d : Membership α ρ] [ForIn' m ρ α d] {β}
+@[wf_preprocess] theorem forIn_eq_forIn' [d : Membership α ρ] [ForIn' m ρ α d] {β} [Monad m]
     (x : ρ) (b : β) (f : (a : α) → β → m (ForInStep β)) :
     forIn x b f = forIn' x b (fun x h => binderNameHint x f <| binderNameHint h () <| f x) := by
   rfl
@@ -403,7 +403,7 @@ class ForM (m : Type u → Type v) (γ : Type w₁) (α : outParam (Type w₂))
   /--
   Runs the monadic action `f` on each element of the collection `coll`.
   -/
-  forM (coll : γ) (f : α → m PUnit) : m PUnit
+  forM [Monad m] (coll : γ) (f : α → m PUnit) : m PUnit
 
 export ForM (forM)
 

src/Init/Control/Except.lean

@@ -148,23 +148,6 @@ This is the inverse of `ExceptT.mk`.
 @[always_inline, inline, expose]
 def ExceptT.run {ε : Type u} {m : Type u → Type v} {α : Type u} (x : ExceptT ε m α) : m (Except ε α) := x
 
-/--
-Use a monadic action that may throw an exception by providing explicit success and failure
-continuations.
--/
-@[always_inline, inline, expose]
-def ExceptT.runK [Monad m] (x : ExceptT ε m α) (ok : α → m β) (error : ε → m β) : m β :=
-  x.run >>= (·.casesOn error ok)
-
-/--
-Returns the value of a computation, forgetting whether it was an exception or a success.
-
-This corresponds to early return.
--/
-@[always_inline, inline, expose]
-def ExceptT.runCatch [Monad m] (x : ExceptT α m α) : m α :=
-  x.runK pure pure
-
 namespace ExceptT
 
 variable {ε : Type u} {m : Type u → Type v} [Monad m]

src/Init/Core.lean

@@ -377,7 +377,7 @@ class ForIn (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v))
   More information about the translation of `for` loops into `ForIn.forIn` is available in [the Lean
   reference manual](lean-manual://section/monad-iteration-syntax).
   -/
-  forIn {β} (xs : ρ) (b : β) (f : α → β → m (ForInStep β)) : m β
+  forIn {β} [Monad m] (xs : ρ) (b : β) (f : α → β → m (ForInStep β)) : m β
 
 export ForIn (forIn)
 
@@ -405,7 +405,7 @@ class ForIn' (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v)
   More information about the translation of `for` loops into `ForIn'.forIn'` is available in [the
   Lean reference manual](lean-manual://section/monad-iteration-syntax).
   -/
-  forIn' {β} (x : ρ) (b : β) (f : (a : α) → a ∈ x → β → m (ForInStep β)) : m β
+  forIn' {β} [Monad m] (x : ρ) (b : β) (f : (a : α) → a ∈ x → β → m (ForInStep β)) : m β
 
 export ForIn' (forIn')
 
@@ -1590,7 +1590,7 @@ gen_injective_theorems% PSum
 gen_injective_theorems% Sigma
 gen_injective_theorems% String
 gen_injective_theorems% String.Pos.Raw
-gen_injective_theorems% Substring.Raw
+gen_injective_theorems% Substring
 gen_injective_theorems% Subtype
 gen_injective_theorems% Sum
 gen_injective_theorems% Task
@@ -2507,7 +2507,8 @@ class Antisymm (r : α → α → Prop) : Prop where
   /-- An antisymmetric relation `r` satisfies `r a b → r b a → a = b`. -/
   antisymm (a b : α) : r a b → r b a → a = b
 
-/-- `Asymm r` means that the binary relation `r` is asymmetric, that is, `r a b → ¬ r b a`. -/
+/-- `Asymm r` means that the binary relation `r` is asymmetric, that is,
+`r a b → ¬ r b a`. -/
 class Asymm (r : α → α → Prop) : Prop where
   /-- An asymmetric relation satisfies `r a b → ¬ r b a`. -/
   asymm : ∀ a b, r a b → ¬r b a
@@ -2517,19 +2518,16 @@ class Symm (r : α → α → Prop) : Prop where
   /-- A symmetric relation satisfies `r a b → r b a`. -/
   symm : ∀ a b, r a b → r b a
 
-/-- `Total X r` means that the binary relation `r` on `X` is total, that is, `r a b` or `r b a`. -/
+/-- `Total X r` means that the binary relation `r` on `X` is total, that is, that for any
+`x y : X` we have `r x y` or `r y x`. -/
 class Total (r : α → α → Prop) : Prop where
-  /-- A total relation satisfies `r a b` or `r b a`. -/
+  /-- A total relation satisfies `r a b ∨ r b a`. -/
   total : ∀ a b, r a b ∨ r b a
 
-/-- `Irrefl r` means the binary relation `r` is irreflexive, that is, `r x x` never holds. -/
+/-- `Irrefl r` means the binary relation `r` is irreflexive, that is, `r x x` never
+holds. -/
 class Irrefl (r : α → α → Prop) : Prop where
   /-- An irreflexive relation satisfies `¬ r a a`. -/
   irrefl : ∀ a, ¬r a a
 
-/-- `Trichotomous r` says that `r` is trichotomous, that is, `¬ r a b → ¬ r b a → a = b`. -/
-class Trichotomous (r : α → α → Prop) : Prop where
-  /-- An trichotomous relation `r` satisfies `¬ r a b → ¬ r b a → a = b`. -/
-  trichotomous (a b : α) : ¬ r a b → ¬ r b a → a = b
-
 end Std

src/Init/Data/Array/Basic.lean

@@ -242,7 +242,7 @@ Examples:
 * `#["red", "green", "blue", "brown"].swapIfInBounds 0 4 = #["red", "green", "blue", "brown"]`
 * `#["red", "green", "blue", "brown"].swapIfInBounds 9 2 = #["red", "green", "blue", "brown"]`
 -/
-@[extern "lean_array_swap", expose]
+@[extern "lean_array_swap", grind]
 def swapIfInBounds (xs : Array α) (i j : @& Nat) : Array α :=
   if h₁ : i < xs.size then
   if h₂ : j < xs.size then swap xs i j
@@ -570,7 +570,7 @@ protected def forIn' {α : Type u} {β : Type v} {m : Type v → Type w} [Monad
       | ForInStep.yield b => loop i (Nat.le_of_lt h') b
   loop as.size (Nat.le_refl _) b
 
-instance [Monad m] : ForIn' m (Array α) α inferInstance where
+instance : ForIn' m (Array α) α inferInstance where
   forIn' := Array.forIn'
 
 -- No separate `ForIn` instance is required because it can be derived from `ForIn'`.
@@ -1001,7 +1001,7 @@ unless `start < stop`. By default, the entire array is used.
 protected def forM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Array α) (start := 0) (stop := as.size) : m PUnit :=
   as.foldlM (fun _ => f) ⟨⟩ start stop
 
-instance [Monad m] : ForM m (Array α) α where
+instance : ForM m (Array α) α where
   forM xs f := Array.forM f xs
 
 -- We simplify `Array.forM` to `forM`.
@@ -1295,7 +1295,7 @@ decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 
 /--
-Returns the index of the first element equal to `a`, or `none` if no element is equal
+Returns the index of the first element equal to `a`, or the size of the array if no element is equal
 to `a`. The index is returned as a `Fin`, which guarantees that it is in bounds.
 
 Examples:

src/Init/Data/Array/Bootstrap.lean

@@ -100,15 +100,9 @@ abbrev push_toList := @toList_push
 @[simp, grind =] theorem empty_append {xs : Array α} : #[] ++ xs = xs := by
   apply ext'; simp only [toList_append, List.nil_append]
 
-@[simp] theorem append_assoc {xs ys zs : Array α} : xs ++ ys ++ zs = xs ++ (ys ++ zs) := by
+@[simp, grind _=_] theorem append_assoc {xs ys zs : Array α} : xs ++ ys ++ zs = xs ++ (ys ++ zs) := by
   apply ext'; simp only [toList_append, List.append_assoc]
 
-grind_pattern append_assoc => (xs ++ ys) ++ zs where
-  xs =/= #[]; ys =/= #[]; zs =/= #[]
-
-grind_pattern append_assoc => xs ++ (ys ++ zs) where
-  xs =/= #[]; ys =/= #[]; zs =/= #[]
-
 @[simp] theorem appendList_eq_append {xs : Array α} {l : List α} : xs.appendList l = xs ++ l := rfl
 
 @[simp, grind =] theorem toList_appendList {xs : Array α} {l : List α} :
@@ -116,4 +110,6 @@ grind_pattern append_assoc => xs ++ (ys ++ zs) where
   rw [← appendList_eq_append]; unfold Array.appendList
   induction l generalizing xs <;> simp [*]
 
+
+
 end Array

src/Init/Data/Array/DecidableEq.lean

@@ -89,41 +89,11 @@ theorem isEqv_self_beq [BEq α] [ReflBEq α] (xs : Array α) : Array.isEqv xs xs
 theorem isEqv_self [DecidableEq α] (xs : Array α) : Array.isEqv xs xs (· = ·) = true := by
   simp [isEqv, isEqvAux_self]
 
-def instDecidableEqImpl [DecidableEq α] : DecidableEq (Array α) := fun xs ys =>
-  match h:isEqv xs ys (fun a b => a = b) with
-  | true  => isTrue (eq_of_isEqv xs ys h)
-  | false => isFalse (by subst ·; rw [isEqv_self] at h; contradiction)
-
-instance instDecidableEq [DecidableEq α] : DecidableEq (Array α) := fun xs ys =>
-  match xs with
-  | ⟨[]⟩ =>
-    match ys with
-    | ⟨[]⟩ => isTrue rfl
-    | ⟨_ :: _⟩ => isFalse (Array.noConfusion · (List.noConfusion ·))
-  | ⟨a :: as⟩ =>
-    match ys with
-    | ⟨[]⟩ => isFalse (Array.noConfusion · (List.noConfusion ·))
-    | ⟨b :: bs⟩ => instDecidableEqImpl ⟨a :: as⟩ ⟨b :: bs⟩
-
-@[csimp]
-theorem instDecidableEq_csimp : @instDecidableEq = @instDecidableEqImpl :=
-  Subsingleton.allEq _ _
-  
-/--
-Equality with `#[]` is decidable even if the underlying type does not have decidable equality.
--/
-instance instDecidableEqEmp (xs : Array α) : Decidable (xs = #[]) :=
-  match xs with
-  | ⟨[]⟩ => isTrue rfl
-  | ⟨_ :: _⟩ => isFalse (Array.noConfusion · (List.noConfusion ·))
-
-/--
-Equality with `#[]` is decidable even if the underlying type does not have decidable equality.
--/
-instance instDecidableEmpEq (ys : Array α) : Decidable (#[] = ys) :=
-  match ys with
-  | ⟨[]⟩ => isTrue rfl
-  | ⟨_ :: _⟩ => isFalse (Array.noConfusion · (List.noConfusion ·))
+instance [DecidableEq α] : DecidableEq (Array α) :=
+  fun xs ys =>
+    match h:isEqv xs ys (fun a b => a = b) with
+    | true  => isTrue (eq_of_isEqv xs ys h)
+    | false => isFalse fun h' => by subst h'; rw [isEqv_self] at h; contradiction
 
 theorem beq_eq_decide [BEq α] (xs ys : Array α) :
     (xs == ys) = if h : xs.size = ys.size then

src/Init/Data/Array/Extract.lean

@@ -200,7 +200,7 @@ theorem getElem?_extract_of_succ {as : Array α} {j : Nat} :
   simp [getElem?_extract]
   omega
 
-@[simp] theorem extract_extract {as : Array α} {i j k l : Nat} :
+@[simp, grind =] theorem extract_extract {as : Array α} {i j k l : Nat} :
     (as.extract i j).extract k l = as.extract (i + k) (min (i + l) j) := by
   ext m h₁ h₂
   · simp
@@ -208,9 +208,6 @@ theorem getElem?_extract_of_succ {as : Array α} {j : Nat} :
   · simp only [size_extract] at h₁ h₂
     simp [Nat.add_assoc]
 
-grind_pattern extract_extract => (as.extract i j).extract k l where
-  as =/= #[]
-
 theorem extract_eq_empty_of_eq_empty {as : Array α} {i j : Nat} (h : as = #[]) :
     as.extract i j = #[] := by
   simp [h]
@@ -409,6 +406,8 @@ theorem popWhile_append {xs ys : Array α} :
   rcases ys with ⟨ys⟩
   simp only [List.append_toArray, List.popWhile_toArray, List.reverse_append, List.dropWhile_append,
     List.isEmpty_iff, List.isEmpty_toArray, List.isEmpty_reverse]
+  -- Why do these not fire with `simp`?
+  rw [List.popWhile_toArray, List.isEmpty_toArray, List.isEmpty_reverse]
   split
   · rfl
   · simp

src/Init/Data/Array/Lemmas.lean

@@ -1628,15 +1628,12 @@ theorem filterMap_eq_filter {p : α → Bool} (w : stop = as.size) :
   cases as
   simp
 
+@[grind =]
 theorem filterMap_filterMap {f : α → Option β} {g : β → Option γ} {xs : Array α} :
     filterMap g (filterMap f xs) = filterMap (fun x => (f x).bind g) xs := by
   cases xs
   simp [List.filterMap_filterMap]
 
-grind_pattern filterMap_filterMap => filterMap g (filterMap f xs) where
-  f =/= some
-  g =/= some
-
 @[grind =]
 theorem map_filterMap {f : α → Option β} {g : β → γ} {xs : Array α} :
     map g (filterMap f xs) = filterMap (fun x => (f x).map g) xs := by
@@ -2231,8 +2228,8 @@ theorem push_eq_flatten_iff {xss : Array (Array α)} {ys : Array α} {y : α} :
 --           zs = cs ++ ds.flatten := by sorry
 
 
-/-- Two arrays of arrays are equal iff their flattens coincide, as well as the sizes of the
-arrays. -/
+/-- Two arrays of subarrays are equal iff their flattens coincide, as well as the sizes of the
+subarrays. -/
 theorem eq_iff_flatten_eq {xss₁ xss₂ : Array (Array α)} :
     xss₁ = xss₂ ↔ xss₁.flatten = xss₂.flatten ∧ map size xss₁ = map size xss₂ := by
   cases xss₁ using array₂_induction with
@@ -3328,16 +3325,6 @@ theorem foldr_filterMap {f : α → Option β} {g : β → γ → γ} {xs : Arra
     (xs.filterMap f).foldr g init = xs.foldr (fun x y => match f x with | some b => g b y | none => y) init := by
   simp [foldr_filterMap']
 
-theorem foldl_flatMap {f : α → Array β} {g : γ → β → γ} {xs : Array α} {init : γ} :
-    (xs.flatMap f).foldl g init = xs.foldl (fun acc x => (f x).foldl g acc) init := by
-  rcases xs with ⟨l⟩
-  simp [List.foldl_flatMap]
-
-theorem foldr_flatMap {f : α → Array β} {g : β → γ → γ} {xs : Array α} {init : γ} :
-    (xs.flatMap f).foldr g init = xs.foldr (fun x acc => (f x).foldr g acc) init := by
-  rcases xs with ⟨l⟩
-  simp [List.foldr_flatMap]
-
 theorem foldl_map_hom' {g : α → β} {f : α → α → α} {f' : β → β → β} {a : α} {xs : Array α}
     {stop : Nat} (h : ∀ x y, f' (g x) (g y) = g (f x y)) (w : stop = xs.size) :
     (xs.map g).foldl f' (g a) 0 stop = g (xs.foldl f a) := by
@@ -3555,6 +3542,11 @@ theorem mem_of_back? {xs : Array α} {a : α} (h : xs.back? = some a) : a ∈ xs
   rcases ys with ⟨ys⟩
   simp only [List.append_toArray, List.back_toArray, List.getLast_append, List.isEmpty_iff,
     List.isEmpty_toArray]
+  split
+  · rw [dif_pos]
+    simpa only [List.isEmpty_toArray]
+  · rw [dif_neg]
+    simpa only [List.isEmpty_toArray]
 
 theorem back_append_right {xs ys : Array α} (h : 0 < ys.size) :
     (xs ++ ys).back (by simp; omega) = ys.back h := by
@@ -3966,29 +3958,28 @@ theorem getElem_modify_of_ne {xs : Array α} {i : Nat} (h : i ≠ j)
 
 /-! ### swap -/
 
-@[grind =]
-theorem getElem_swap {xs : Array α} {i j : Nat} (hi hj) {k : Nat} (hk : k < (xs.swap i j hi hj).size) :
-    (xs.swap i j hi hj)[k] = if k = i then xs[j] else if k = j then xs[i] else xs[k]'(by simp_all) := by
-  simp only [swap_def, getElem_set, eq_comm (a := k)]
-  split <;> split <;> simp_all
-
 @[simp] theorem getElem_swap_right {xs : Array α} {i j : Nat} {hi hj} :
     (xs.swap i j hi hj)[j]'(by simpa using hj) = xs[i] := by
-  simp +contextual [getElem_swap]
+  simp [swap_def]
 
 @[simp] theorem getElem_swap_left {xs : Array α} {i j : Nat} {hi hj} :
     (xs.swap i j hi hj)[i]'(by simpa using hi) = xs[j] := by
-  simp [getElem_swap]
+  simp +contextual [swap_def, getElem_set]
 
-@[simp] theorem getElem_swap_of_ne {xs : Array α} {i j : Nat} {hi hj}
-    {h : k < (xs.swap i j hi hj).size} (hi' : k ≠ i) (hj' : k ≠ j) :
-    (xs.swap i j hi hj)[k] = xs[k]'(by simp_all) := by
-  simp [getElem_swap, hi', hj']
+@[simp] theorem getElem_swap_of_ne {xs : Array α} {i j : Nat} {hi hj} (hp : k < xs.size)
+    (hi' : k ≠ i) (hj' : k ≠ j) : (xs.swap i j hi hj)[k]'(xs.size_swap .. |>.symm ▸ hp) = xs[k] := by
+  simp [swap_def, getElem_set, hi'.symm, hj'.symm]
 
-@[deprecated getElem_swap (since := "2025-10-10")]
 theorem getElem_swap' {xs : Array α} {i j : Nat} {hi hj} {k : Nat} (hk : k < xs.size) :
-    (xs.swap i j hi hj)[k]'(by simp_all) = if k = i then xs[j] else if k = j then xs[i] else xs[k] :=
-  getElem_swap _ _ _
+    (xs.swap i j hi hj)[k]'(by simp_all) = if k = i then xs[j] else if k = j then xs[i] else xs[k] := by
+  split
+  · simp_all only [getElem_swap_left]
+  · split <;> simp_all
+
+@[grind =]
+theorem getElem_swap {xs : Array α} {i j : Nat} (hi hj) {k : Nat} (hk : k < (xs.swap i j hi hj).size) :
+    (xs.swap i j hi hj)[k] = if k = i then xs[j] else if k = j then xs[i] else xs[k]'(by simp_all) := by
+  apply getElem_swap'
 
 @[simp] theorem swap_swap {xs : Array α} {i j : Nat} (hi hj) :
     (xs.swap i j hi hj).swap i j ((xs.size_swap ..).symm ▸ hi) ((xs.size_swap ..).symm ▸ hj) = xs := by
@@ -4009,66 +4000,8 @@ theorem swap_comm {xs : Array α} {i j : Nat} (hi hj) : xs.swap i j hi hj = xs.s
     · split <;> simp_all
     · split <;> simp_all
 
-/-! ### swapIfInBounds -/
-
-@[grind =] theorem swapIfInBounds_def {xs : Array α} {i j : Nat} :
-    xs.swapIfInBounds i j = if h₁ : i < xs.size then
-  if h₂ : j < xs.size then swap xs i j else xs else xs := rfl
-
 @[simp, grind =] theorem size_swapIfInBounds {xs : Array α} {i j : Nat} :
-    (xs.swapIfInBounds i j).size = xs.size := by
-  unfold swapIfInBounds; split <;> (try split) <;> simp [size_swap]
-
-@[grind =] theorem getElem_swapIfInBounds {xs : Array α} {i j k : Nat}
-    (hk : k < (xs.swapIfInBounds i j).size) :
-    (xs.swapIfInBounds i j)[k] =
-    if h₁ : k = i ∧ j < xs.size then xs[j]'h₁.2 else if h₂ : k = j ∧ i < xs.size then xs[i]'h₂.2
-    else xs[k]'(by simp_all) := by
-  rw [size_swapIfInBounds] at hk
-  unfold swapIfInBounds
-  split <;> rename_i hi
-  · split <;> rename_i hj
-    · simp only [hi, hj, and_true]
-      exact getElem_swap _ _ _
-    · simp only [hi, hj, and_true, and_false, dite_false]
-      split <;> simp_all
-  · simp only [hi, and_false, dite_false]
-    split <;> simp_all
-
-@[simp]
-theorem getElem_swapIfInBounds_of_size_le_left {xs : Array α} {i j k : Nat} (hi : xs.size ≤ i)
-    (hk : k < (xs.swapIfInBounds i j).size) :
-    (xs.swapIfInBounds i j)[k] = xs[k]'(Nat.lt_of_lt_of_eq hk size_swapIfInBounds) := by
-  have h₁ : k ≠ i := Nat.ne_of_lt <| Nat.lt_of_lt_of_le hk <|
-    Nat.le_trans (Nat.le_of_eq (size_swapIfInBounds)) hi
-  have h₂ : ¬ (i < xs.size) := Nat.not_lt_of_le hi
-  simp [getElem_swapIfInBounds, h₁, h₂]
-
-@[simp]
-theorem getElem_swapIfInBounds_of_size_le_right {xs : Array α} {i j k : Nat} (hj : xs.size ≤ j)
-    (hk : k < (xs.swapIfInBounds i j).size) :
-    (xs.swapIfInBounds i j)[k] = xs[k]'(Nat.lt_of_lt_of_eq hk size_swapIfInBounds) := by
-  have h₁ : ¬ (j < xs.size) := Nat.not_lt_of_le hj
-  have h₂ : k ≠ j := Nat.ne_of_lt <| Nat.lt_of_lt_of_le hk <|
-    Nat.le_trans (Nat.le_of_eq (size_swapIfInBounds)) hj
-  simp [getElem_swapIfInBounds, h₁, h₂]
-
-@[simp]
-theorem getElem_swapIfInBounds_left {xs : Array α} {i j : Nat} (hj : j < xs.size)
-    (hi : i < (xs.swapIfInBounds i j).size) : (xs.swapIfInBounds i j)[i] = xs[j] := by
-  simp [getElem_swapIfInBounds, hj]
-
-@[simp]
-theorem getElem_swapIfInBounds_right {xs : Array α} {i j : Nat} (hi : i < xs.size)
-    (hj : j < (xs.swapIfInBounds i j).size) :
-    (xs.swapIfInBounds i j)[j] = xs[i] := by
-  simp +contextual [getElem_swapIfInBounds, hi]
-
-@[simp]
-theorem getElem_swapIfInBounds_of_ne_of_ne {xs : Array α} {i j k : Nat} (hi : k ≠ i) (hj : k ≠ j)
-    (hk : k < (xs.swapIfInBounds i j).size) :
-    (xs.swapIfInBounds i j)[k] = xs[k]'(Nat.lt_of_lt_of_eq hk size_swapIfInBounds) := by
-  simp [getElem_swapIfInBounds, hi, hj]
+    (xs.swapIfInBounds i j).size = xs.size := by unfold swapIfInBounds; split <;> (try split) <;> simp [size_swap]
 
 /-! ### swapAt -/
 
@@ -4330,10 +4263,6 @@ theorem size_uset {xs : Array α} {v : α} {i : USize} (h : i.toNat < xs.size) :
 theorem getElem!_eq_getD [Inhabited α] {xs : Array α} {i} : xs[i]! = xs.getD i default := by
   rfl
 
-theorem getElem_eq_getD {xs : Array α} {i} {h : i < xs.size} (fallback : α) :
-    xs[i]'h = xs.getD i fallback := by
-  rw [getD_eq_getD_getElem?, getElem_eq_getElem?_get, Option.get_eq_getD]
-
 /-! # mem -/
 
 @[deprecated mem_toList_iff (since := "2025-05-26")]

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

@@ -75,11 +75,11 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs
     Nat.add_min_add_left, Nat.add_lt_add_iff_left, Std.Rco.forIn'_eq_forIn'_toList]
   conv =>
     lhs; congr; congr
-    rw [cons_lex_cons.forIn'_congr_aux Std.Rco.toList_eq_if_roo rfl (fun _ _ _ => rfl)]
+    rw [cons_lex_cons.forIn'_congr_aux Std.Rco.toList_eq_if rfl (fun _ _ _ => rfl)]
     simp only [bind_pure_comp, map_pure]
     rw [cons_lex_cons.forIn'_congr_aux (if_pos (by omega)) rfl (fun _ _ _ => rfl)]
-  simp only [Std.toList_roo_eq_toList_rco_of_isSome_succ? (lo := 0) (h := rfl),
-    Std.PRange.UpwardEnumerable.succ?, Nat.add_comm 1, Std.PRange.Nat.toList_rco_succ_succ,
+  simp only [Std.toList_Roo_eq_toList_Rco_of_isSome_succ? (lo := 0) (h := rfl),
+    Std.PRange.UpwardEnumerable.succ?, Nat.add_comm 1, Std.PRange.Nat.toList_Rco_succ_succ,
     Option.get_some, List.forIn'_cons, List.size_toArray, List.length_cons, List.length_nil,
     Nat.lt_add_one, getElem_append_left, List.getElem_toArray, List.getElem_cons_zero]
   cases lt a b
@@ -151,7 +151,7 @@ protected theorem lt_of_le_of_lt [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrd
 @[deprecated Array.lt_of_le_of_lt (since := "2025-08-01")]
 protected theorem lt_of_le_of_lt' [LT α]
     [i₁ : Std.Asymm (· < · : α → α → Prop)]
-    [i₂ : Std.Trichotomous (· < · : α → α → Prop)]
+    [i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
     [i₃ : Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)]
     {xs ys zs : Array α} (h₁ : xs ≤ ys) (h₂ : ys < zs) : xs < zs :=
   letI := LE.ofLT α
@@ -165,7 +165,7 @@ protected theorem le_trans [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α]
 @[deprecated Array.le_trans (since := "2025-08-01")]
 protected theorem le_trans' [LT α]
     [i₁ : Std.Asymm (· < · : α → α → Prop)]
-    [i₂ : Std.Trichotomous (· < · : α → α → Prop)]
+    [i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
     [i₃ : Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)]
     {xs ys zs : Array α} (h₁ : xs ≤ ys) (h₂ : ys ≤ zs) : xs ≤ zs :=
   letI := LE.ofLT α
@@ -196,7 +196,7 @@ protected theorem le_of_lt [LT α]
 
 protected theorem le_iff_lt_or_eq [LT α]
     [Std.Irrefl (· < · : α → α → Prop)]
-    [Std.Trichotomous (· < · : α → α → Prop)]
+    [Std.Antisymm (¬ · < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     {xs ys : Array α} : xs ≤ ys ↔ xs < ys ∨ xs = ys := by
   simpa using List.le_iff_lt_or_eq (l₁ := xs.toList) (l₂ := ys.toList)
@@ -285,7 +285,7 @@ protected theorem lt_iff_exists [LT α] {xs ys : Array α} :
 
 protected theorem le_iff_exists [LT α]
     [Std.Asymm (· < · : α → α → Prop)]
-    [Std.Trichotomous (· < · : α → α → Prop)] {xs ys : Array α} :
+    [Std.Antisymm (¬ · < · : α → α → Prop)] {xs ys : Array α} :
     xs ≤ ys ↔
       (xs = ys.take xs.size) ∨
         (∃ (i : Nat) (h₁ : i < xs.size) (h₂ : i < ys.size),
@@ -304,7 +304,7 @@ theorem append_left_lt [LT α] {xs ys zs : Array α} (h : ys < zs) :
 
 theorem append_left_le [LT α]
     [Std.Asymm (· < · : α → α → Prop)]
-    [Std.Trichotomous (· < · : α → α → Prop)]
+    [Std.Antisymm (¬ · < · : α → α → Prop)]
     {xs ys zs : Array α} (h : ys ≤ zs) :
     xs ++ ys ≤ xs ++ zs := by
   cases xs
@@ -327,9 +327,9 @@ protected theorem map_lt [LT α] [LT β]
 
 protected theorem map_le [LT α] [LT β]
     [Std.Asymm (· < · : α → α → Prop)]
-    [Std.Trichotomous (· < · : α → α → Prop)]
+    [Std.Antisymm (¬ · < · : α → α → Prop)]
     [Std.Asymm (· < · : β → β → Prop)]
-    [Std.Trichotomous (· < · : β → β → Prop)]
+    [Std.Antisymm (¬ · < · : β → β → Prop)]
     {xs ys : Array α} {f : α → β} (w : ∀ x y, x < y → f x < f y) (h : xs ≤ ys) :
     map f xs ≤ map f ys := by
   cases xs

src/Init/Data/BitVec/Lemmas.lean

@@ -1056,7 +1056,7 @@ theorem toInt_setWidth' {m n : Nat} (p : m ≤ n) {x : BitVec m} :
 @[simp, grind =] theorem toFin_setWidth' {m n : Nat} (p : m ≤ n) (x : BitVec m) :
     (setWidth' p x).toFin = x.toFin.castLE (Nat.pow_le_pow_right (by omega) (by omega)) := by
   ext
-  rw [setWidth'_eq, toFin_setWidth, Fin.val_ofNat, Fin.val_castLE, val_toFin,
+  rw [setWidth'_eq, toFin_setWidth, Fin.val_ofNat, Fin.coe_castLE, val_toFin,
     Nat.mod_eq_of_lt (by apply BitVec.toNat_lt_twoPow_of_le p)]
 
 theorem toNat_setWidth_of_le {w w' : Nat} {b : BitVec w} (h : w ≤ w') : (b.setWidth w').toNat = b.toNat := by

src/Init/Data/ByteArray/Basic.lean

@@ -132,11 +132,6 @@ Copies the bytes with indices {name}`b` (inclusive) to {name}`e` (exclusive) to
 def extract (a : ByteArray) (b e : Nat) : ByteArray :=
   a.copySlice b empty 0 (e - b)
 
-/--
-Appends two byte arrays using fast array primitives instead of converting them into lists and back.
-
-In compiled code, this function replaces calls to {name}`ByteArray.append`.
--/
 @[inline]
 protected def fastAppend (a : ByteArray) (b : ByteArray) : ByteArray :=
   -- we assume that `append`s may be repeated, so use asymptotic growing; use `copySlice` directly to customize
@@ -248,7 +243,7 @@ protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteAr
       | ForInStep.yield b => loop i (Nat.le_of_lt h') b
   loop as.size (Nat.le_refl _) b
 
-instance [Monad m] : ForIn m ByteArray UInt8 where
+instance : ForIn m ByteArray UInt8 where
   forIn := ByteArray.forIn
 
 /--

src/Init/Data/Char/Lemmas.lean

@@ -55,12 +55,8 @@ instance leAntisymm : Std.Antisymm (· ≤ · : Char → Char → Prop) where
   antisymm _ _ := Char.le_antisymm
 
 -- This instance is useful while setting up instances for `String`.
-instance ltTrichotomous : Std.Trichotomous (· < · : Char → Char → Prop) where
-  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
-  antisymm := Char.ltTrichotomous.trichotomous
+  antisymm _ _ h₁ h₂ := Char.le_antisymm (by simpa using h₂) (by simpa using h₁)
 
 instance ltAsymm : Std.Asymm (· < · : Char → Char → Prop) where
   asymm _ _ := Char.lt_asymm

src/Init/Data/Dyadic/Basic.lean

@@ -440,11 +440,11 @@ theorem toDyadic_mkRat (a : Int) (b : Nat) (prec : Int) :
   cases prec
   · simp only [Rat.toDyadic, Int.ofNat_eq_natCast, Int.toNat_natCast, Int.toNat_neg_natCast,
       shiftLeft_zero, Int.natCast_mul]
-    rw [Int.mul_comm d, ← Int.ediv_ediv_of_nonneg (by simp), ← Int.shiftLeft_mul,
+    rw [Int.mul_comm d, ← Int.ediv_ediv (by simp), ← Int.shiftLeft_mul,
       Int.mul_ediv_cancel _ (by simpa using hm)]
   · simp only [Rat.toDyadic, Int.natCast_shiftLeft, Int.negSucc_eq, ← Int.natCast_add_one,
       Int.toNat_neg_natCast, Int.shiftLeft_zero, Int.neg_neg, Int.toNat_natCast, Int.natCast_mul]
-    rw [Int.mul_comm d, ← Int.mul_shiftLeft, ← Int.ediv_ediv_of_nonneg (by simp),
+    rw [Int.mul_comm d, ← Int.mul_shiftLeft, ← Int.ediv_ediv (by simp),
       Int.mul_ediv_cancel _ (by simpa using hm)]
 
 theorem toDyadic_eq_ofIntWithPrec (x : Rat) (prec : Int) :
@@ -472,7 +472,7 @@ theorem toRat_toDyadic (x : Rat) (prec : Int) :
       Rat.den_ofNat, Nat.one_pow, Nat.mul_one]
     split
     · simp_all
-    · rw [Int.ediv_ediv_of_nonneg (Int.natCast_nonneg _)]
+    · rw [Int.ediv_ediv (Int.natCast_nonneg _)]
       congr 1
       rw [Int.natCast_ediv, Int.mul_ediv_cancel']
       rw [Int.natCast_dvd_natCast]
@@ -495,7 +495,7 @@ theorem toRat_toDyadic (x : Rat) (prec : Int) :
     simp only [this, Int.mul_one]
     split
     · simp_all
-    · rw [Int.ediv_ediv_of_nonneg (Int.natCast_nonneg _)]
+    · rw [Int.ediv_ediv (Int.natCast_nonneg _)]
       congr 1
       rw [Int.natCast_ediv, Int.mul_ediv_cancel']
       · simp

src/Init/Data/Fin/Basic.lean

@@ -246,11 +246,6 @@ instance neg (n : Nat) : Neg (Fin n) :=
 
 theorem neg_def (a : Fin n) : -a = ⟨(n - a) % n, Nat.mod_lt _ a.pos⟩ := rfl
 
--- Later we give another version called `Fin.val_neg` that splits on `a = 0`.
-protected theorem val_neg' (a : Fin n) : ((-a : Fin n) : Nat) = (n - a) % n :=
-  rfl
-
-@[deprecated Fin.val_neg' (since := "2025-11-21")]
 protected theorem coe_neg (a : Fin n) : ((-a : Fin n) : Nat) = (n - a) % n :=
   rfl
 

src/Init/Data/Fin/Lemmas.lean

@@ -16,25 +16,17 @@ open Std
 
 namespace Fin
 
-@[simp, grind =] theorem ofNat_zero (n : Nat) [NeZero n] : Fin.ofNat n 0 = 0 := rfl
+@[simp] theorem ofNat_zero (n : Nat) [NeZero n] : Fin.ofNat n 0 = 0 := rfl
 
 @[deprecated ofNat_zero (since := "2025-05-28")] abbrev ofNat'_zero := @ofNat_zero
 
 theorem mod_def (a m : Fin n) : a % m = Fin.mk (a.val % m.val) (Nat.lt_of_le_of_lt (Nat.mod_le _ _) a.2) :=
   rfl
 
-theorem val_mod (a m : Fin n) : (a % m).val = a.val % m.val := rfl
-
 theorem mul_def (a b : Fin n) : a * b = Fin.mk ((a.val * b.val) % n) (Nat.mod_lt _ a.pos) := rfl
 
-theorem val_mul (a b : Fin n) : (a * b).val = (a.val * b.val) % n := rfl
-
 theorem sub_def (a b : Fin n) : a - b = Fin.mk (((n - b.val) + a.val) % n) (Nat.mod_lt _ a.pos) := rfl
 
-@[grind =]
-theorem val_sub (a b : Fin n) : (a - b).val = ((n - b.val) + a.val) % n := rfl
-
-@[grind →]
 theorem pos' : ∀ [Nonempty (Fin n)], 0 < n | ⟨i⟩ => i.pos
 
 @[simp] theorem is_lt (a : Fin n) : (a : Nat) < n := a.2
@@ -46,8 +38,7 @@ theorem pos_iff_nonempty {n : Nat} : 0 < n ↔ Nonempty (Fin n) :=
 
 @[simp] protected theorem eta (a : Fin n) (h : a < n) : (⟨a, h⟩ : Fin n) = a := rfl
 
-@[ext, grind ext]
-protected theorem ext {a b : Fin n} (h : (a : Nat) = b) : a = b := eq_of_val_eq h
+@[ext] protected theorem ext {a b : Fin n} (h : (a : Nat) = b) : a = b := eq_of_val_eq h
 
 theorem val_ne_iff {a b : Fin n} : a.1 ≠ b.1 ↔ a ≠ b := not_congr val_inj
 
@@ -78,7 +69,7 @@ theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta ..
 
 @[deprecated val_ofNat (since := "2025-05-28")] abbrev val_ofNat' := @val_ofNat
 
-@[simp, grind =] theorem ofNat_self {n : Nat} [NeZero n] : Fin.ofNat n n = 0 := by
+@[simp] theorem ofNat_self {n : Nat} [NeZero n] : Fin.ofNat n n = 0 := by
   ext
   simp
   congr
@@ -98,7 +89,7 @@ theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta ..
 @[simp] theorem div_val (a b : Fin n) : (a / b).val = a.val / b.val :=
   rfl
 
-@[simp, grind =] theorem modn_val (a : Fin n) (b : Nat) : (a.modn b).val = a.val % b :=
+@[simp] theorem modn_val (a : Fin n) (b : Nat) : (a.modn b).val = a.val % b :=
   rfl
 
 @[simp] theorem val_eq_zero (a : Fin 1) : a.val = 0 :=
@@ -268,9 +259,7 @@ instance : LawfulOrderLT (Fin n) where
   lt_iff := by
     simp [← Fin.not_le, Decidable.imp_iff_not_or, Std.Total.total]
 
-@[simp] theorem val_rev (i : Fin n) : (rev i).val = n - (i + 1) := rfl
-
-grind_pattern val_rev => i.rev
+@[simp, grind =] theorem val_rev (i : Fin n) : (rev i).val = n - (i + 1) := rfl
 
 @[simp] theorem rev_rev (i : Fin n) : rev (rev i) = i := Fin.ext <| by
   rw [val_rev, val_rev, ← Nat.sub_sub, Nat.sub_sub_self (by exact i.2), Nat.add_sub_cancel]
@@ -295,8 +284,6 @@ theorem rev_eq {n a : Nat} (i : Fin (n + 1)) (h : n = a + i) :
 
 @[simp] theorem val_last (n : Nat) : (last n).1 = n := rfl
 
-grind_pattern val_last => last n
-
 @[simp] theorem last_zero : (Fin.last 0 : Fin 1) = 0 := by
   ext
   simp
@@ -406,8 +393,6 @@ theorem zero_ne_one : (0 : Fin (n + 2)) ≠ 1 := Fin.ne_of_lt zero_lt_one
 
 @[simp] theorem val_succ (j : Fin n) : (j.succ : Nat) = j + 1 := rfl
 
-grind_pattern val_succ => j.succ
-
 @[simp] theorem succ_pos (a : Fin n) : (0 : Fin (n + 1)) < a.succ := by
   simp [Fin.lt_def]
 
@@ -468,18 +453,12 @@ theorem one_lt_succ_succ (a : Fin n) : (1 : Fin (n + 2)) < a.succ.succ := by
 theorem succ_succ_ne_one (a : Fin n) : Fin.succ (Fin.succ a) ≠ 1 :=
   Fin.ne_of_gt (one_lt_succ_succ a)
 
-@[simp, grind =] theorem val_castLT (i : Fin m) (h : i.1 < n) : (castLT i h : Nat) = i := rfl
-
-@[deprecated val_castLT (since := "2025-11-21")]
-theorem coe_castLT (i : Fin m) (h : i.1 < n) : (castLT i h : Nat) = i := rfl
+@[simp] theorem coe_castLT (i : Fin m) (h : i.1 < n) : (castLT i h : Nat) = i := rfl
 
 @[simp] theorem castLT_mk (i n m : Nat) (hn : i < n) (hm : i < m) : castLT ⟨i, hn⟩ hm = ⟨i, hm⟩ :=
   rfl
 
-@[simp, grind =] theorem val_castLE (h : n ≤ m) (i : Fin n) : (castLE h i : Nat) = i := rfl
-
-@[deprecated val_castLE (since := "2025-11-21")]
-theorem coe_castLE (h : n ≤ m) (i : Fin n) : (castLE h i : Nat) = i := rfl
+@[simp, grind =] theorem coe_castLE (h : n ≤ m) (i : Fin n) : (castLE h i : Nat) = i := rfl
 
 @[simp] theorem castLE_mk (i n m : Nat) (hn : i < n) (h : n ≤ m) :
     castLE h ⟨i, hn⟩ = ⟨i, Nat.lt_of_lt_of_le hn h⟩ := rfl
@@ -491,16 +470,13 @@ theorem coe_castLE (h : n ≤ m) (i : Fin n) : (castLE h i : Nat) = i := rfl
 
 @[simp] theorem castLE_castLE {k m n} (km : k ≤ m) (mn : m ≤ n) (i : Fin k) :
     Fin.castLE mn (Fin.castLE km i) = Fin.castLE (Nat.le_trans km mn) i :=
-  Fin.ext (by simp only [val_castLE])
+  Fin.ext (by simp only [coe_castLE])
 
 @[simp] theorem castLE_comp_castLE {k m n} (km : k ≤ m) (mn : m ≤ n) :
     Fin.castLE mn ∘ Fin.castLE km = Fin.castLE (Nat.le_trans km mn) :=
   funext (castLE_castLE km mn)
 
-@[simp, grind =] theorem val_cast (h : n = m) (i : Fin n) : (i.cast h : Nat) = i := rfl
-
-@[deprecated val_cast (since := "2025-11-21")]
-theorem coe_cast (h : n = m) (i : Fin n) : (i.cast h : Nat) = i := rfl
+@[simp] theorem coe_cast (h : n = m) (i : Fin n) : (i.cast h : Nat) = i := rfl
 
 @[simp] theorem cast_castLE {k m n} (km : k ≤ m) (mn : m = n) (i : Fin k) :
     Fin.cast mn (i.castLE km) = i.castLE (mn ▸ km) :=
@@ -513,7 +489,7 @@ theorem coe_cast (h : n = m) (i : Fin n) : (i.cast h : Nat) = i := rfl
 @[simp] theorem cast_zero [NeZero n] [NeZero m] (h : n = m) : Fin.cast h 0 = 0 := rfl
 
 @[simp] theorem cast_last {n' : Nat} {h : n + 1 = n' + 1} : (last n).cast h  = last n' :=
-  Fin.ext (by rw [val_cast, val_last, val_last, Nat.succ.inj h])
+  Fin.ext (by rw [coe_cast, val_last, val_last, Nat.succ.inj h])
 
 @[simp] theorem cast_mk (h : n = m) (i : Nat) (hn : i < n) : Fin.cast h ⟨i, hn⟩ = ⟨i, h ▸ hn⟩ := rfl
 
@@ -528,10 +504,7 @@ theorem coe_cast (h : n = m) (i : Fin n) : (i.cast h : Nat) = i := rfl
 
 theorem castLE_of_eq {m n : Nat} (h : m = n) {h' : m ≤ n} : castLE h' = Fin.cast h := rfl
 
-@[simp, grind =] theorem val_castAdd (m : Nat) (i : Fin n) : (castAdd m i : Nat) = i := rfl
-
-@[deprecated val_castAdd (since := "2025-11-21")]
-theorem coe_castAdd (m : Nat) (i : Fin n) : (castAdd m i : Nat) = i := rfl
+@[simp] theorem coe_castAdd (m : Nat) (i : Fin n) : (castAdd m i : Nat) = i := rfl
 
 @[simp] theorem castAdd_zero : (castAdd 0 : Fin n → Fin (n + 0)) = Fin.cast rfl := rfl
 
@@ -567,10 +540,7 @@ the reverse direction. -/
 theorem succ_cast_eq {n' : Nat} (i : Fin n) (h : n = n') :
     (i.cast h).succ = i.succ.cast (by rw [h]) := rfl
 
-@[simp, grind =] theorem val_castSucc (i : Fin n) : (i.castSucc : Nat) = i := rfl
-
-@[deprecated val_castSucc (since := "2025-11-21")]
-theorem coe_castSucc (i : Fin n) : (i.castSucc : Nat) = i := rfl
+@[simp] theorem coe_castSucc (i : Fin n) : (i.castSucc : Nat) = i := rfl
 
 @[simp] theorem castSucc_mk (n i : Nat) (h : i < n) : castSucc ⟨i, h⟩ = ⟨i, Nat.lt_succ_of_lt h⟩ := rfl
 
@@ -578,7 +548,7 @@ theorem coe_castSucc (i : Fin n) : (i.castSucc : Nat) = i := rfl
     i.castSucc.cast h = (i.cast (Nat.succ.inj h)).castSucc := rfl
 
 theorem castSucc_lt_succ {i : Fin n} : i.castSucc < i.succ :=
-  lt_def.2 <| by simp only [val_castSucc, val_succ, Nat.lt_succ_self]
+  lt_def.2 <| by simp only [coe_castSucc, val_succ, Nat.lt_succ_self]
 
 theorem le_castSucc_iff {i : Fin (n + 1)} {j : Fin n} : i ≤ j.castSucc ↔ i < j.succ := by
   simpa only [lt_def, le_def] using Nat.add_one_le_add_one_iff.symm
@@ -632,7 +602,7 @@ theorem coeSucc_eq_succ {a : Fin n} : a.castSucc + 1 = a.succ := by
 
 @[deprecated castSucc_lt_succ (since := "2025-10-29")]
 theorem lt_succ {a : Fin n} : a.castSucc < a.succ := by
-  rw [castSucc, lt_def, val_castAdd, val_succ]; exact Nat.lt_succ_self a.val
+  rw [castSucc, lt_def, coe_castAdd, val_succ]; exact Nat.lt_succ_self a.val
 
 theorem exists_castSucc_eq {n : Nat} {i : Fin (n + 1)} : (∃ j, castSucc j = i) ↔ i ≠ last n :=
   ⟨fun ⟨j, hj⟩ => hj ▸ Fin.ne_of_lt j.castSucc_lt_last,
@@ -640,10 +610,7 @@ theorem exists_castSucc_eq {n : Nat} {i : Fin (n + 1)} : (∃ j, castSucc j = i)
 
 theorem succ_castSucc {n : Nat} (i : Fin n) : i.castSucc.succ = i.succ.castSucc := rfl
 
-@[simp, grind =] theorem val_addNat (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := rfl
-
-@[deprecated val_addNat (since := "2025-11-21")]
-theorem coe_addNat (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := rfl
+@[simp] theorem coe_addNat (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := rfl
 
 @[simp] theorem addNat_zero (n : Nat) (i : Fin n) : addNat i 0 = i := by
   ext
@@ -671,10 +638,7 @@ theorem cast_addNat_left {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :
     (addNat i m').cast h = addNat i m :=
   Fin.ext <| (congrArg ((· + ·) (i : Nat)) (Nat.add_left_cancel h) : _)
 
-@[simp, grind =] theorem val_natAdd (n : Nat) {m : Nat} (i : Fin m) : (natAdd n i : Nat) = n + i := rfl
-
-@[deprecated val_natAdd (since := "2025-11-21")]
-theorem coe_natAdd (n : Nat) {m : Nat} (i : Fin m) : (natAdd n i : Nat) = n + i := rfl
+@[simp] theorem coe_natAdd (n : Nat) {m : Nat} (i : Fin m) : (natAdd n i : Nat) = n + i := rfl
 
 @[simp] theorem natAdd_mk (n i : Nat) (hi : i < m) :
     natAdd n ⟨i, hi⟩ = ⟨n + i, Nat.add_lt_add_left hi n⟩ := rfl
@@ -731,7 +695,7 @@ theorem natAdd_castSucc {m n : Nat} {i : Fin m} : natAdd n (castSucc i) = castSu
   omega
 
 theorem rev_castAdd (k : Fin n) (m : Nat) : rev (castAdd m k) = addNat (rev k) m := Fin.ext <| by
-  rw [val_rev, val_castAdd, val_addNat, val_rev, Nat.sub_add_comm (Nat.succ_le_of_lt k.is_lt)]
+  rw [val_rev, coe_castAdd, coe_addNat, val_rev, Nat.sub_add_comm (Nat.succ_le_of_lt k.is_lt)]
 
 theorem rev_addNat (k : Fin n) (m : Nat) : rev (addNat k m) = castAdd m (rev k) := by
   rw [← rev_rev (castAdd ..), rev_castAdd, rev_rev]
@@ -753,12 +717,7 @@ theorem castSucc_natAdd (n : Nat) (i : Fin k) :
 
 /-! ### pred -/
 
-@[simp] theorem val_pred (j : Fin (n + 1)) (h : j ≠ 0) : (j.pred h : Nat) = j - 1 := rfl
-
-grind_pattern val_pred => j.pred h
-
-@[deprecated val_pred (since := "2025-11-21")]
-theorem coe_pred (j : Fin (n + 1)) (h : j ≠ 0) : (j.pred h : Nat) = j - 1 := rfl
+@[simp] theorem coe_pred (j : Fin (n + 1)) (h : j ≠ 0) : (j.pred h : Nat) = j - 1 := rfl
 
 @[simp] theorem succ_pred : ∀ (i : Fin (n + 1)) (h : i ≠ 0), (i.pred h).succ = i
   | ⟨0, _⟩, hi => by simp only [mk_zero, ne_eq, not_true] at hi
@@ -776,7 +735,7 @@ theorem pred_eq_iff_eq_succ {n : Nat} {i : Fin (n + 1)} (hi : i ≠ 0) {j : Fin
 theorem pred_mk_succ (i : Nat) (h : i < n + 1) :
     Fin.pred ⟨i + 1, Nat.add_lt_add_right h 1⟩ (ne_of_val_ne (Nat.ne_of_gt (mk_succ_pos i h))) =
       ⟨i, h⟩ := by
-  simp only [Fin.ext_iff, val_pred, Nat.add_sub_cancel]
+  simp only [Fin.ext_iff, coe_pred, Nat.add_sub_cancel]
 
 @[simp] theorem pred_mk_succ' (i : Nat) (h₁ : i + 1 < n + 1 + 1) (h₂) :
     Fin.pred ⟨i + 1, h₁⟩ h₂ = ⟨i, Nat.lt_of_succ_lt_succ h₁⟩ := pred_mk_succ i _
@@ -803,13 +762,10 @@ theorem pred_mk {n : Nat} (i : Nat) (h : i < n + 1) (w) : Fin.pred ⟨i, h⟩ w
 
 theorem pred_add_one (i : Fin (n + 2)) (h : (i : Nat) < n + 1) :
     pred (i + 1) (Fin.ne_of_gt (add_one_pos _ (lt_def.2 h))) = castLT i h := by
-  rw [Fin.ext_iff, val_pred, val_castLT, val_add, val_one, Nat.mod_eq_of_lt, Nat.add_sub_cancel]
+  rw [Fin.ext_iff, coe_pred, coe_castLT, val_add, val_one, Nat.mod_eq_of_lt, Nat.add_sub_cancel]
   exact Nat.add_lt_add_right h 1
 
-@[simp, grind =] theorem val_subNat (i : Fin (n + m)) (h : m ≤ i) : (i.subNat m h : Nat) = i - m := rfl
-
-@[deprecated val_subNat (since := "2025-11-21")]
-theorem coe_subNat (i : Fin (n + m)) (h : m ≤ i) : (i.subNat m h : Nat) = i - m := rfl
+@[simp] theorem coe_subNat (i : Fin (n + m)) (h : m ≤ i) : (i.subNat m h : Nat) = i - m := rfl
 
 @[simp] theorem subNat_mk {i : Nat} (h₁ : i < n + m) (h₂ : m ≤ i) :
     subNat m ⟨i, h₁⟩ h₂ = ⟨i - m, Nat.sub_lt_right_of_lt_add h₂ h₁⟩ := rfl
@@ -874,11 +830,11 @@ step. `Fin.succRec` is a version of this induction principle that takes the `Fin
     (zero : ∀ n, motive (n + 1) 0) (succ : ∀ n i, motive n i → motive (Nat.succ n) i.succ) :
     motive n i := i.succRec zero succ
 
-@[simp, grind =] theorem succRecOn_zero {motive : ∀ n, Fin n → Sort _} {zero succ} (n) :
+@[simp] theorem succRecOn_zero {motive : ∀ n, Fin n → Sort _} {zero succ} (n) :
     @Fin.succRecOn (n + 1) 0 motive zero succ = zero n := by
   cases n <;> rfl
 
-@[simp, grind =] theorem succRecOn_succ {motive : ∀ n, Fin n → Sort _} {zero succ} {n} (i : Fin n) :
+@[simp] theorem succRecOn_succ {motive : ∀ n, Fin n → Sort _} {zero succ} {n} (i : Fin n) :
     @Fin.succRecOn (n + 1) i.succ motive zero succ = succ n i (Fin.succRecOn i zero succ) := by
   cases i; rfl
 
@@ -906,11 +862,11 @@ where
   | 0, hi => by rwa [Fin.mk_zero]
   | i+1, hi => succ ⟨i, Nat.lt_of_succ_lt_succ hi⟩ (go i (Nat.lt_of_succ_lt hi))
 
-@[simp, grind =] theorem induction_zero {motive : Fin (n + 1) → Sort _} (zero : motive 0)
+@[simp] theorem induction_zero {motive : Fin (n + 1) → Sort _} (zero : motive 0)
     (hs : ∀ i : Fin n, motive (castSucc i) → motive i.succ) :
     (induction zero hs : ∀ i : Fin (n + 1), motive i) 0 = zero := rfl
 
-@[simp, grind =] theorem induction_succ {motive : Fin (n + 1) → Sort _} (zero : motive 0)
+@[simp] theorem induction_succ {motive : Fin (n + 1) → Sort _} (zero : motive 0)
     (succ : ∀ i : Fin n, motive (castSucc i) → motive i.succ) (i : Fin n) :
     induction (motive := motive) zero succ i.succ = succ i (induction zero succ (castSucc i)) := rfl
 
@@ -942,13 +898,13 @@ The corresponding induction principle is `Fin.induction`.
     (zero : motive 0) (succ : ∀ i : Fin n, motive i.succ) :
     ∀ i : Fin (n + 1), motive i := induction zero fun i _ => succ i
 
-@[simp, grind =] theorem cases_zero {n} {motive : Fin (n + 1) → Sort _} {zero succ} :
+@[simp] theorem cases_zero {n} {motive : Fin (n + 1) → Sort _} {zero succ} :
     @Fin.cases n motive zero succ 0 = zero := rfl
 
-@[simp, grind =] theorem cases_succ {n} {motive : Fin (n + 1) → Sort _} {zero succ} (i : Fin n) :
+@[simp] theorem cases_succ {n} {motive : Fin (n + 1) → Sort _} {zero succ} (i : Fin n) :
     @Fin.cases n motive zero succ i.succ = succ i := rfl
 
-@[simp, grind =] theorem cases_succ' {n} {motive : Fin (n + 1) → Sort _} {zero succ}
+@[simp] theorem cases_succ' {n} {motive : Fin (n + 1) → Sort _} {zero succ}
     {i : Nat} (h : i + 1 < n + 1) :
     @Fin.cases n motive zero succ ⟨i.succ, h⟩ = succ ⟨i, Nat.lt_of_succ_lt_succ h⟩ := rfl
 
@@ -998,7 +954,7 @@ For the induction:
       | j + 1 => go j (by omega) (by omega) (cast ⟨j, by omega⟩ x)
   go _ _ (by omega) last
 
-@[simp, grind =] theorem reverseInduction_last {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ} :
+@[simp] theorem reverseInduction_last {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ} :
     (reverseInduction zero succ (Fin.last n) : motive (Fin.last n)) = zero := by
   rw [reverseInduction, reverseInduction.go]; simp
 
@@ -1015,7 +971,7 @@ private theorem reverseInduction_castSucc_aux {n : Nat} {motive : Fin (n + 1)
     dsimp only
     rw [ih _ _ (by omega), eq_comm, reverseInduction.go, dif_neg (by change i.1 + 1 ≠ _; omega)]
 
-@[simp, grind =] theorem reverseInduction_castSucc {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ}
+@[simp] theorem reverseInduction_castSucc {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ}
     (i : Fin n) : reverseInduction (motive := motive) zero succ (castSucc i) =
       succ i (reverseInduction zero succ i.succ) := by
   rw [reverseInduction, reverseInduction_castSucc_aux _ _ _ i.isLt, reverseInduction]
@@ -1034,11 +990,11 @@ The corresponding induction principle is `Fin.reverseInduction`.
     (cast : ∀ i : Fin n, motive (castSucc i)) (i : Fin (n + 1)) : motive i :=
   reverseInduction last (fun i _ => cast i) i
 
-@[simp, grind =] theorem lastCases_last {n : Nat} {motive : Fin (n + 1) → Sort _} {last cast} :
+@[simp] theorem lastCases_last {n : Nat} {motive : Fin (n + 1) → Sort _} {last cast} :
     (Fin.lastCases last cast (Fin.last n) : motive (Fin.last n)) = last :=
   reverseInduction_last ..
 
-@[simp, grind =] theorem lastCases_castSucc {n : Nat} {motive : Fin (n + 1) → Sort _} {last cast}
+@[simp] theorem lastCases_castSucc {n : Nat} {motive : Fin (n + 1) → Sort _} {last cast}
     (i : Fin n) : (Fin.lastCases last cast (Fin.castSucc i) : motive (Fin.castSucc i)) = cast i :=
   reverseInduction_castSucc ..
 
@@ -1058,11 +1014,11 @@ as `Fin.natAdd m (j : Fin n)`.
   if hi : (i : Nat) < m then (castAdd_castLT n i hi) ▸ (left (castLT i hi))
   else (natAdd_subNat_cast (Nat.le_of_not_lt hi)) ▸ (right _)
 
-@[simp, grind =] theorem addCases_left {m n : Nat} {motive : Fin (m + n) → Sort _} {left right} (i : Fin m) :
+@[simp] theorem addCases_left {m n : Nat} {motive : Fin (m + n) → Sort _} {left right} (i : Fin m) :
     addCases (motive := motive) left right (Fin.castAdd n i) = left i := by
   rw [addCases, dif_pos (castAdd_lt _ _)]; rfl
 
-@[simp, grind =]
+@[simp]
 theorem addCases_right {m n : Nat} {motive : Fin (m + n) → Sort _} {left right} (i : Fin n) :
     addCases (motive := motive) left right (natAdd m i) = right i := by
   have : ¬(natAdd m i : Nat) < m := Nat.not_lt.2 (le_coe_natAdd ..)
@@ -1095,7 +1051,6 @@ theorem add_ofNat [NeZero n] (x : Fin n) (y : Nat) :
 
 /-! ### sub -/
 
-@[deprecated val_sub (since := "2025-11-21")]
 protected theorem coe_sub (a b : Fin n) : ((a - b : Fin n) : Nat) = ((n - b) + a) % n := by
   cases a; cases b; rfl
 
@@ -1147,7 +1102,6 @@ theorem coe_sub_iff_lt {a b : Fin n} : (↑(a - b) : Nat) = n + a - b ↔ a < b
 
 /-! ### neg -/
 
-@[grind =]
 theorem val_neg {n : Nat} [NeZero n] (x : Fin n) :
     (-x).val = if x = 0 then 0 else n - x.val := by
   change (n - ↑x) % n = _
@@ -1163,7 +1117,7 @@ protected theorem sub_eq_add_neg {n : Nat} (x y : Fin n) : x - y = x + -y := by
     apply elim0 x
   · replace h : NeZero n := ⟨h⟩
     ext
-    rw [Fin.val_sub, Fin.val_add, val_neg]
+    rw [Fin.coe_sub, Fin.val_add, val_neg]
     split
     · simp_all
     · simp [Nat.add_comm]
@@ -1184,6 +1138,9 @@ theorem mul_ofNat [NeZero n] (x : Fin n) (y : Nat) :
 
 @[deprecated mul_ofNat (since := "2025-05-28")] abbrev mul_ofNat' := @mul_ofNat
 
+theorem val_mul {n : Nat} : ∀ a b : Fin n, (a * b).val = a.val * b.val % n
+  | ⟨_, _⟩, ⟨_, _⟩ => rfl
+
 @[deprecated val_mul (since := "2025-10-26")]
 theorem coe_mul {n : Nat} : ∀ a b : Fin n, ((a * b : Fin n) : Nat) = a * b % n
   | ⟨_, _⟩, ⟨_, _⟩ => rfl

src/Init/Data/FloatArray/Basic.lean

@@ -129,7 +129,7 @@ protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : FloatA
       | ForInStep.yield b => loop i (Nat.le_of_lt h') b
   loop as.size (Nat.le_refl _) b
 
-instance [Monad m] : ForIn m FloatArray Float where
+instance : ForIn m FloatArray Float where
   forIn := FloatArray.forIn
 
 /-- See comment at `forInUnsafe` -/

src/Init/Data/Format/Instances.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Init.Data.Array.Basic
-import Init.Data.String.Search
+import Init.Data.String.Basic
 
 public section
 
@@ -47,7 +47,7 @@ Converts a string to a pretty-printer document, replacing newlines in the string
 `Std.Format.line`.
 -/
 def String.toFormat (s : String) : Std.Format :=
-  Std.Format.joinSep (s.split '\n').toList Std.Format.line
+  Std.Format.joinSep (s.splitOn "\n") Std.Format.line
 
 instance : ToFormat String.Pos.Raw where
   format p := format p.byteIdx

src/Init/Data/Int/Basic.lean

@@ -392,9 +392,9 @@ Examples:
 * `(0 : Int) ^ 10 = 0`
 * `(-7 : Int) ^ 3 = -343`
 -/
-protected def pow : Int → Nat → Int
-  | (m : Nat), n => Int.ofNat (m ^ n)
-  | m@-[_+1], n => if n % 2 = 0 then Int.ofNat (m.natAbs ^ n) else - Int.ofNat (m.natAbs ^ n)
+protected def pow (m : Int) : Nat → Int
+  | 0      => 1
+  | succ n => Int.pow m n * m
 
 instance : NatPow Int where
   pow := Int.pow

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

@@ -24,17 +24,12 @@ theorem natCast_shiftRight (n s : Nat) : n >>> s = (n : Int) >>> s := rfl
 theorem negSucc_shiftRight (m n : Nat) :
     -[m+1] >>> n = -[m >>>n +1] := rfl
 
+@[grind _=_]
 theorem shiftRight_add (i : Int) (m n : Nat) :
     i >>> (m + n) = i >>> m >>> n := by
   simp only [shiftRight_eq, Int.shiftRight]
   cases i <;> simp [Nat.shiftRight_add]
 
-grind_pattern shiftRight_add => i >>> (m + n) where
-  i =/= 0
-
-grind_pattern shiftRight_add => i >>> m >>> n where
-  i =/= 0
-
 theorem shiftRight_eq_div_pow (m : Int) (n : Nat) :
     m >>> n = m / ((2 ^ n) : Nat) := by
   simp only [shiftRight_eq, Int.shiftRight, Nat.shiftRight_eq_div_pow]

src/Init/Data/Int/DivMod.lean

@@ -9,4 +9,3 @@ prelude
 public import Init.Data.Int.DivMod.Basic
 public import Init.Data.Int.DivMod.Bootstrap
 public import Init.Data.Int.DivMod.Lemmas
-public import Init.Data.Int.DivMod.Pow

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

@@ -145,12 +145,6 @@ theorem dvd_of_mul_dvd_mul_left {a m n : Int} (ha : a ≠ 0) (h : a * m ∣ a *
 theorem dvd_of_mul_dvd_mul_right {a m n : Int} (ha : a ≠ 0) (h : m * a ∣ n * a) : m ∣ n :=
   dvd_of_mul_dvd_mul_left ha (by simpa [Int.mul_comm] using h)
 
-theorem dvd_mul_of_dvd_right {a b c : Int} (h : a ∣ c) : a ∣ b * c :=
-  Int.dvd_trans h (Int.dvd_mul_left b c)
-
-theorem dvd_mul_of_dvd_left {a b c : Int} (h : a ∣ b) : a ∣ b * c :=
-  Int.dvd_trans h (Int.dvd_mul_right b c)
-
 @[norm_cast] theorem natCast_dvd_natCast {m n : Nat} : (↑m : Int) ∣ ↑n ↔ m ∣ n where
   mp := by
     rintro ⟨a, h⟩
@@ -1235,7 +1229,7 @@ private theorem ediv_ediv_of_pos {x y z : Int} (hy : 0 < y) (hz : 0 < z) :
   · rw [Int.mul_comm y, ← Int.mul_assoc, ← Int.add_mul, Int.mul_comm _ z]
     exact Int.lt_mul_of_ediv_lt hy (Int.lt_mul_ediv_self_add hz)
 
-theorem ediv_ediv_of_nonneg {x y z : Int} (hy : 0 ≤ y) : x / y / z = x / (y * z) := by
+theorem ediv_ediv {x y z : Int} (hy : 0 ≤ y) : x / y / z = x / (y * z) := by
   rcases y with (_ | a) | a
   · simp
   · rcases z with (_ | b) | b
@@ -1244,21 +1238,6 @@ theorem ediv_ediv_of_nonneg {x y z : Int} (hy : 0 ≤ y) : x / y / z = x / (y *
     · simp [Int.negSucc_eq, Int.mul_neg, ediv_ediv_of_pos]
   · simp at hy
 
-theorem ediv_ediv {x y z : Int} : x / y / z = x / (y * z) - if y < 0 ∧ ¬ z ∣ x / y then z.sign else 0 := by
-  rcases y with y | y
-  · rw [ediv_ediv_of_nonneg (by simp), if_neg (by simp; omega)]
-    simp
-  · rw [Int.negSucc_eq, Int.ediv_neg, Int.neg_mul, Int.ediv_neg, Int.neg_ediv, ediv_ediv_of_nonneg (by omega)]
-    simp
-
-theorem ediv_mul {x y z : Int} : x / (y * z) = x / y / z + if y < 0 ∧ ¬ z ∣ x / y then z.sign else 0 := by
-  have := ediv_ediv (x := x) (y := y) (z := z)
-  omega
-
-theorem ediv_mul_of_nonneg {x y z : Int} (hy : 0 ≤ y) : x / (y * z) = x / y / z := by
-  have := ediv_ediv_of_nonneg (x := x) (y := y) (z := z) hy
-  omega
-
 /-! ### tdiv -/
 
 -- `tdiv` analogues of `ediv` lemmas from `Bootstrap.lean`
@@ -1781,16 +1760,6 @@ theorem ediv_lt_ediv_iff_of_dvd_of_neg_of_neg {a b c d : Int} (hb : b < 0) (hd :
   obtain ⟨⟨x, rfl⟩, y, rfl⟩ := hba, hdc
   simp [*, Int.ne_of_lt, d.mul_assoc, b.mul_comm]
 
-theorem ediv_lt_ediv_of_lt {a b c : Int} (h : a < b) (hcb : c ∣ b) (hc : 0 < c) :
-    a / c < b / c :=
-  Int.lt_ediv_of_mul_lt (Int.le_of_lt hc) hcb 
-    (Int.lt_of_le_of_lt (Int.ediv_mul_le _ (Int.ne_of_gt hc)) h)
-  
-theorem ediv_lt_ediv_of_lt_of_neg {a b c : Int} (h : b < a) (hca : c ∣ a) (hc : c < 0) :
-    a / c < b / c :=
-  (Int.ediv_lt_iff_of_dvd_of_neg hc hca).2 
-    (Int.lt_of_le_of_lt (Int.mul_ediv_self_le (Int.ne_of_lt hc)) h)
-
 /-! ### `tdiv` and ordering -/
 
 -- Theorems about `tdiv` and ordering, whose `ediv` analogues are in `Bootstrap.lean`.

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

@@ -1,35 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
--/
-module
-prelude
-public import Init.Data.Int.DivMod.Lemmas
-public import Init.Data.Int.Pow
-
-/-!
-# Lemmas about divisibility of powers
--/
-
-namespace Int
-
-theorem dvd_pow {a b : Int} {n : Nat} (hab : b ∣ a) : b ^ n ∣ a ^ n := by
-  rcases hab with ⟨c, rfl⟩
-  rw [Int.mul_pow]
-  exact Int.dvd_mul_right (b ^ n) (c ^ n)
-
-theorem ediv_pow {a b : Int} {n : Nat} (hab : b ∣ a) :
-    (a / b) ^ n = a ^ n / b ^ n := by
-  obtain ⟨c, rfl⟩ := hab
-  by_cases b = 0
-  · by_cases n = 0 <;> simp [*, Int.zero_pow]
-  · simp [Int.mul_pow, Int.pow_ne_zero, *]
-
-theorem tdiv_pow {a b : Int} {n : Nat} (hab : b ∣ a) :
-    (a.tdiv b) ^ n = (a ^ n).tdiv (b ^ n) := by
-  rw [Int.tdiv_eq_ediv_of_dvd hab, ediv_pow hab, Int.tdiv_eq_ediv_of_dvd (dvd_pow hab)]
-
-theorem fdiv_pow {a b : Int} {n : Nat} (hab : b ∣ a) :
-    (a.fdiv b) ^ n = (a ^ n).fdiv (b ^ n) := by
-  rw [Int.fdiv_eq_ediv_of_dvd hab, ediv_pow hab, Int.fdiv_eq_ediv_of_dvd (dvd_pow hab)]

src/Init/Data/Int/Lemmas.lean

@@ -552,7 +552,7 @@ protected theorem mul_eq_zero {a b : Int} : a * b = 0 ↔ a = 0 ∨ b = 0 := by
   exact match a, b, h with
   | .ofNat 0, _, _ => by simp
   | _, .ofNat 0, _ => by simp
-  | .ofNat (_+1), .negSucc _, h => by cases h
+  | .ofNat (a+1), .negSucc b, h => by cases h
 
 protected theorem mul_ne_zero {a b : Int} (a0 : a ≠ 0) (b0 : b ≠ 0) : a * b ≠ 0 :=
   Or.rec a0 b0 ∘ Int.mul_eq_zero.mp

src/Init/Data/Int/Order.lean

@@ -377,15 +377,6 @@ protected theorem le_iff_lt_add_one {a b : Int} : a ≤ b ↔ a < b + 1 := by
 
 @[grind =] protected theorem max_def (n m : Int) : max n m = if n ≤ m then m else n := rfl
 
-end Int
-namespace Lean.Meta.Grind.Lia
-
-scoped grind_pattern Int.min_def => min n m
-scoped grind_pattern Int.max_def => max n m
-
-end Lean.Meta.Grind.Lia
-namespace Int
-
 @[simp] protected theorem neg_min_neg (a b : Int) : min (-a) (-b) = -max a b := by
   rw [Int.min_def, Int.max_def]
   simp

src/Init/Data/Int/Pow.lean

@@ -14,20 +14,9 @@ namespace Int
 
 /-! # pow -/
 
-@[simp, norm_cast]
-theorem natCast_pow (m n : Nat) : (m ^ n : Nat) = (m : Int) ^ n := rfl
-
-theorem negSucc_pow (m n : Nat) : (-[m+1] : Int) ^ n = if n % 2 = 0 then Int.ofNat (m.succ ^ n) else Int.negOfNat (m.succ ^ n) := rfl
-
-@[simp] protected theorem pow_zero (m : Int) : m ^ 0 = 1 := by cases m <;> simp [← natCast_pow, negSucc_pow]
-
-protected theorem pow_succ (m : Int) (n : Nat) : m ^ n.succ = m ^ n * m := by
-  rcases m with _ | a
-  · rfl
-  · simp only [negSucc_pow, Nat.succ_mod_succ_eq_zero_iff, Nat.reduceAdd, ← Nat.mod_two_ne_zero,
-      Nat.pow_succ, ofNat_eq_natCast, @negOfNat_eq (_ * _), ite_not, apply_ite (· * -[a+1]),
-      ofNat_mul_negSucc, negOfNat_mul_negSucc]
+@[simp] protected theorem pow_zero (b : Int) : b^0 = 1 := rfl
 
+protected theorem pow_succ (b : Int) (e : Nat) : b ^ (e+1) = (b ^ e) * b := rfl
 protected theorem pow_succ' (b : Int) (e : Nat) : b ^ (e+1) = b * (b ^ e) := by
   rw [Int.mul_comm, Int.pow_succ]
 
@@ -43,46 +32,29 @@ protected theorem zero_pow {n : Nat} (h : n ≠ 0) : (0 : Int) ^ n = 0 := by
 protected theorem one_pow {n : Nat} : (1 : Int) ^ n = 1 := by
   induction n with simp_all [Int.pow_succ]
 
-protected theorem mul_pow {a b : Int} {n : Nat} : (a * b) ^ n = a ^ n * b ^ n := by
-  induction n with
-  | zero => simp
-  | succ n ih =>
-    rw [Int.pow_succ, Int.pow_succ, Int.pow_succ, ih, Int.mul_assoc, Int.mul_assoc,
-      Int.mul_left_comm (b^n)]
-
-protected theorem pow_one (a : Int) : a ^ 1 = a := by
-  rw [Int.pow_succ, Int.pow_zero, Int.one_mul]
-
-protected theorem pow_mul {a : Int} {n m : Nat} : a ^ (n * m) = (a ^ n) ^ m := by
-  induction m with
-  | zero => simp
-  | succ m ih =>
-    rw [Int.pow_succ, Nat.mul_add_one, Int.pow_add, ih]
-
 protected theorem pow_pos {n : Int} {m : Nat} : 0 < n → 0 < n ^ m := by
   induction m with
   | zero => simp
-  | succ m ih =>
-    simp only [Int.pow_succ]
-    exact fun h => Int.mul_pos (ih h) h
+  | succ m ih => exact fun h => Int.mul_pos (ih h) h
 
 protected theorem pow_nonneg {n : Int} {m : Nat} : 0 ≤ n → 0 ≤ n ^ m := by
   induction m with
   | zero => simp
-  | succ m ih =>
-    simp only [Int.pow_succ]
-    exact fun h => Int.mul_nonneg (ih h) h
+  | succ m ih => exact fun h => Int.mul_nonneg (ih h) h
 
 protected theorem pow_ne_zero {n : Int} {m : Nat} : n ≠ 0 → n ^ m ≠ 0 := by
   induction m with
   | zero => simp
-  | succ m ih =>
-    simp only [Int.pow_succ]
-    exact fun h => Int.mul_ne_zero (ih h) h
+  | succ m ih => exact fun h => Int.mul_ne_zero (ih h) h
 
 instance {n : Int} {m : Nat} [NeZero n] : NeZero (n ^ m) := ⟨Int.pow_ne_zero (NeZero.ne _)⟩
 
-instance {n : Int} : NeZero (n^0) := ⟨by simp⟩
+@[simp, norm_cast]
+protected theorem natCast_pow (b n : Nat) : ((b^n : Nat) : Int) = (b : Int) ^ n := by
+  match n with
+  | 0 => rfl
+  | n + 1 =>
+    simp only [Nat.pow_succ, Int.pow_succ, Int.natCast_mul, Int.natCast_pow _ n]
 
 @[simp]
 protected theorem two_pow_pred_sub_two_pow {w : Nat} (h : 0 < w) :
@@ -105,7 +77,7 @@ theorem pow_lt_pow_of_lt {a : Int} {b c : Nat} (ha : 1 < a) (hbc : b < c):
   omega
 
 @[simp] theorem natAbs_pow (n : Int) : (k : Nat) → (n ^ k).natAbs = n.natAbs ^ k
-  | 0 => by simp
+  | 0 => rfl
   | k + 1 => by rw [Int.pow_succ, natAbs_mul, natAbs_pow, Nat.pow_succ]
 
 theorem toNat_pow_of_nonneg {x : Int} (h : 0 ≤ x) (k : Nat) : (x ^ k).toNat = x.toNat ^ k := by
@@ -114,21 +86,4 @@ theorem toNat_pow_of_nonneg {x : Int} (h : 0 ≤ x) (k : Nat) : (x ^ k).toNat =
   | succ k ih =>
     rw [Int.pow_succ, Int.toNat_mul (Int.pow_nonneg h) h, ih, Nat.pow_succ]
 
-protected theorem sq_nonnneg (m : Int) : 0 ≤ m ^ 2 := by
-  rw [Int.pow_succ, Int.pow_one]
-  cases m
-  · apply Int.mul_nonneg <;> simp
-  · apply Int.mul_nonneg_of_nonpos_of_nonpos <;> exact negSucc_le_zero _
-
-protected theorem pow_nonneg_of_even {m : Int} {n : Nat} (h : n % 2 = 0) : 0 ≤ m ^ n := by
-  rw [← Nat.mod_add_div n 2, h, Nat.zero_add, Int.pow_mul]
-  apply Int.pow_nonneg
-  exact Int.sq_nonnneg m
-
-protected theorem neg_pow {m : Int} {n : Nat} : (-m)^n = (-1)^(n % 2) * m^n := by
-  rw [Int.neg_eq_neg_one_mul, Int.mul_pow]
-  rw (occs := [1]) [← Nat.mod_add_div n 2]
-  rw [Int.pow_add, Int.pow_mul]
-  simp [Int.one_pow]
-
 end Int

src/Init/Data/Iterators.lean

@@ -9,7 +9,6 @@ prelude
 public import Init.Data.Iterators.Basic
 public import Init.Data.Iterators.PostconditionMonad
 public import Init.Data.Iterators.Consumers
-public import Init.Data.Iterators.Producers
 public import Init.Data.Iterators.Combinators
 public import Init.Data.Iterators.Lemmas
 public import Init.Data.Iterators.ToIterator

src/Init/Data/Iterators/Basic.lean

@@ -678,7 +678,6 @@ Given this typeclass, termination proofs for well-founded recursion over an iter
 `it.finitelyManySteps` as a termination measure.
 -/
 class Finite (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] : Prop where
-  /-- The relation of plausible successors is well-founded. -/
   wf : WellFounded (IterM.IsPlausibleSuccessorOf (α := α) (m := m))
 
 theorem Finite.wf_of_id {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] :
@@ -798,7 +797,6 @@ Given this typeclass, termination proofs for well-founded recursion over an iter
 `it.finitelyManySkips` as a termination measure.
 -/
 class Productive (α m) {β} [Iterator α m β] : Prop where
-  /-- The relation of plausible successors during skips is well-founded. -/
   wf : WellFounded (IterM.IsPlausibleSkipSuccessorOf (α := α) (m := m))
 
 /--
@@ -819,24 +817,6 @@ def IterM.TerminationMeasures.Productive.Rel
     TerminationMeasures.Productive α m → TerminationMeasures.Productive α m → Prop :=
   Relation.TransGen <| InvImage IterM.IsPlausibleSkipSuccessorOf IterM.TerminationMeasures.Productive.it
 
-theorem IterM.TerminationMeasures.Finite.Rel.of_productive
-    {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] {a b : Finite α m} :
-    Productive.Rel ⟨a.it⟩ ⟨b.it⟩ → Finite.Rel a b := by
-  generalize ha' : Productive.mk a.it = a'
-  generalize hb' : Productive.mk b.it = b'
-  have ha : a = ⟨a'.it⟩ := by simp [← ha']
-  have hb : b = ⟨b'.it⟩ := by simp [← hb']
-  rw [ha, hb]
-  clear ha hb ha' hb' a b
-  rw [Productive.Rel, Finite.Rel]
-  intro h
-  induction h
-  · rename_i ih
-    exact .single ⟨_, rfl, ih⟩
-  · rename_i hab ih
-    refine .trans ih ?_
-    exact .single ⟨_, rfl, hab⟩
-
 instance {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
     [Productive α m] : WellFoundedRelation (IterM.TerminationMeasures.Productive α m) where
   rel := IterM.TerminationMeasures.Productive.Rel

src/Init/Data/Iterators/Combinators.lean

@@ -9,5 +9,4 @@ prelude
 public import Init.Data.Iterators.Combinators.Monadic
 public import Init.Data.Iterators.Combinators.FilterMap
 public import Init.Data.Iterators.Combinators.FlatMap
-public import Init.Data.Iterators.Combinators.Take
 public import Init.Data.Iterators.Combinators.ULift

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

@@ -8,5 +8,4 @@ module
 prelude
 public import Init.Data.Iterators.Combinators.Monadic.FilterMap
 public import Init.Data.Iterators.Combinators.Monadic.FlatMap
-public import Init.Data.Iterators.Combinators.Monadic.Take
 public import Init.Data.Iterators.Combinators.Monadic.ULift

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

@@ -106,6 +106,16 @@ instance Attach.instIteratorLoopPartial {α β : Type w} {m : Type w → Type w'
     IteratorLoopPartial (Attach α m P) m n :=
   .defaultImplementation
 
+instance {α β : Type w} {m : Type w → Type w'} [Monad m]
+    {P : β → Prop} [Iterator α m β] [IteratorSize α m] :
+    IteratorSize (Attach α m P) m where
+  size it := IteratorSize.size it.internalState.inner
+
+instance {α β : Type w} {m : Type w → Type w'} [Monad m]
+    {P : β → Prop} [Iterator α m β] [IteratorSizePartial α m] :
+    IteratorSizePartial (Attach α m P) m where
+  size it := IteratorSizePartial.size it.internalState.inner
+
 end Types
 
 /--

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

@@ -604,4 +604,30 @@ def IterM.filter {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [M
     (f : β → Bool) (it : IterM (α := α) m β) :=
   (it.filterMap (fun b => if f b then some b else none) : IterM m β)
 
+instance {α β γ : 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] :
+    IteratorSize (FilterMap α m n lift f) n :=
+  .defaultImplementation
+
+instance {α β γ : 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 γ)} :
+    IteratorSizePartial (FilterMap α m n lift f) n :=
+  .defaultImplementation
+
+instance {α β γ : Type w} {m : Type w → Type w'}
+    {n : Type w → Type w''} [Monad n] [Iterator α m β]
+    {lift : ⦃α : Type w⦄ → m α → n α}
+    {f : β → PostconditionT n γ} [IteratorSize α m] :
+    IteratorSize (Map α m n lift f) n where
+  size it := lift (IteratorSize.size it.internalState.inner)
+
+instance {α β γ : Type w} {m : Type w → Type w'}
+    {n : Type w → Type w''} [Monad n] [Iterator α m β]
+    {lift : ⦃α : Type w⦄ → m α → n α}
+    {f : β → PostconditionT n γ} [IteratorSizePartial α m] :
+    IteratorSizePartial (Map α m n lift f) n where
+  size it := lift (IteratorSizePartial.size it.internalState.inner)
+
 end Std.Iterators

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

@@ -1,223 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Paul Reichert
--/
-module
-
-prelude
-public import Init.Data.Nat.Lemmas
-public import Init.Data.Iterators.Consumers.Monadic.Collect
-public import Init.Data.Iterators.Consumers.Monadic.Loop
-public import Init.Data.Iterators.Internal.Termination
-
-@[expose] public section
-
-/-!
-This module provides the iterator combinator `IterM.take`.
--/
-
-namespace Std.Iterators
-
-variable {α : Type w} {m : Type w → Type w'} {β : Type w}
-
-/--
-The internal state of the `IterM.take` iterator combinator.
--/
-@[unbox]
-structure Take (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where
-  /--
-  Internal implementation detail of the iterator library.
-  Caution: For `take n`, `countdown` is `n + 1`.
-  If `countdown` is zero, the combinator only terminates when `inner` terminates.
-  -/
-  countdown : Nat
-  /-- Internal implementation detail of the iterator library -/
-  inner : IterM (α := α) m β
-  /--
-  Internal implementation detail of the iterator library.
-  This proof term ensures that a `take` always produces a finite iterator from a productive one.
-  -/
-  finite : countdown > 0 ∨ Finite α m
-
-/--
-Given an iterator `it` and a natural number `n`, `it.take n` is an iterator that outputs
-up to the first `n` of `it`'s values in order and then terminates.
-
-**Marble diagram:**
-
-```text
-it          ---a----b---c--d-e--⊥
-it.take 3   ---a----b---c⊥
-
-it          ---a--⊥
-it.take 3   ---a--⊥
-```
-
-**Termination properties:**
-
-* `Finite` instance: only if `it` is productive
-* `Productive` instance: only if `it` is productive
-
-**Performance:**
-
-This combinator incurs an additional O(1) cost with each output of `it`.
--/
-@[always_inline, inline]
-def IterM.take [Iterator α m β] (n : Nat) (it : IterM (α := α) m β) :=
-  toIterM (Take.mk (n + 1) it (Or.inl <| Nat.zero_lt_succ _)) m β
-
-/--
-This combinator is only useful for advanced use cases.
-
-Given a finite iterator `it`, returns an iterator that behaves exactly like `it` but is of the same
-type as `it.take n`.
-
-**Marble diagram:**
-
-```text
-it          ---a----b---c--d-e--⊥
-it.toTake   ---a----b---c--d-e--⊥
-```
-
-**Termination properties:**
-
-* `Finite` instance: always
-* `Productive` instance: always
-
-**Performance:**
-
-This combinator incurs an additional O(1) cost with each output of `it`.
--/
-@[always_inline, inline]
-def IterM.toTake [Iterator α m β] [Finite α m] (it : IterM (α := α) m β) :=
-  toIterM (Take.mk 0 it (Or.inr inferInstance)) m β
-
-theorem IterM.take.surjective_of_zero_lt {α : Type w} {m : Type w → Type w'} {β : Type w}
-    [Iterator α m β] (it : IterM (α := Take α m) m β) (h : 0 < it.internalState.countdown) :
-    ∃ (it₀ : IterM (α := α) m β) (k : Nat), it = it₀.take k := by
-  refine ⟨it.internalState.inner, it.internalState.countdown - 1, ?_⟩
-  simp only [take, Nat.sub_add_cancel (m := 1) (n := it.internalState.countdown) (by omega)]
-  rfl
-
-inductive Take.PlausibleStep [Iterator α m β] (it : IterM (α := Take α m) m β) :
-    (step : IterStep (IterM (α := Take α m) m β) β) → Prop where
-  | yield : ∀ {it' out}, it.internalState.inner.IsPlausibleStep (.yield it' out) →
-      (h : it.internalState.countdown ≠ 1) → PlausibleStep it (.yield ⟨it.internalState.countdown - 1, it', it.internalState.finite.imp_left (by omega)⟩ out)
-  | skip : ∀ {it'}, it.internalState.inner.IsPlausibleStep (.skip it') →
-      it.internalState.countdown ≠ 1 → PlausibleStep it (.skip ⟨it.internalState.countdown, it', it.internalState.finite⟩)
-  | done : it.internalState.inner.IsPlausibleStep .done → PlausibleStep it .done
-  | depleted : it.internalState.countdown = 1 →
-      PlausibleStep it .done
-
-@[always_inline, inline]
-instance Take.instIterator [Monad m] [Iterator α m β] : Iterator (Take α m) m β where
-  IsPlausibleStep := Take.PlausibleStep
-  step it :=
-    if h : it.internalState.countdown = 1 then
-      pure <| .deflate <| .done (.depleted h)
-    else do
-      match (← it.internalState.inner.step).inflate with
-      | .yield it' out h' =>
-        pure <| .deflate <| .yield ⟨it.internalState.countdown - 1, it', (it.internalState.finite.imp_left (by omega))⟩ out (.yield h' h)
-      | .skip it' h' => pure <| .deflate <| .skip ⟨it.internalState.countdown, it', it.internalState.finite⟩ (.skip h' h)
-      | .done h' => pure <| .deflate <| .done (.done h')
-
-def Take.Rel (m : Type w → Type w') [Monad m] [Iterator α m β] [Productive α m] :
-    IterM (α := Take α m) m β → IterM (α := Take α m) m β → Prop :=
-  open scoped Classical in
-  if _ : Finite α m then
-    InvImage (Prod.Lex Nat.lt_wfRel.rel IterM.TerminationMeasures.Finite.Rel)
-      (fun it => (it.internalState.countdown, it.internalState.inner.finitelyManySteps))
-  else
-    InvImage (Prod.Lex Nat.lt_wfRel.rel IterM.TerminationMeasures.Productive.Rel)
-      (fun it => (it.internalState.countdown, it.internalState.inner.finitelyManySkips))
-
-theorem Take.rel_of_countdown [Monad m] [Iterator α m β] [Productive α m]
-    {it it' : IterM (α := Take α m) m β}
-    (h : it'.internalState.countdown < it.internalState.countdown) : Take.Rel m it' it := by
-  simp only [Rel]
-  split <;> exact Prod.Lex.left _ _ h
-
-theorem Take.rel_of_inner [Monad m] [Iterator α m β] [Productive α m] {remaining : Nat}
-    {it it' : IterM (α := α) m β}
-    (h : it'.finitelyManySkips.Rel it.finitelyManySkips) :
-    Take.Rel m (it'.take remaining) (it.take remaining) := by
-  simp only [Rel]
-  split
-  · exact Prod.Lex.right _ (.of_productive h)
-  · exact Prod.Lex.right _ h
-
-theorem Take.rel_of_zero_of_inner [Monad m] [Iterator α m β]
-    {it it' : IterM (α := Take α m) m β}
-    (h : it.internalState.countdown = 0) (h' : it'.internalState.countdown = 0)
-    (h'' : haveI := it.internalState.finite.resolve_left (by omega); it'.internalState.inner.finitelyManySteps.Rel it.internalState.inner.finitelyManySteps) :
-    haveI := it.internalState.finite.resolve_left (by omega)
-    Take.Rel m it' it := by
-  haveI := it.internalState.finite.resolve_left (by omega)
-  simp only [Rel, this, ↓reduceDIte, InvImage, h, h']
-  exact Prod.Lex.right _ h''
-
-private def Take.instFinitenessRelation [Monad m] [Iterator α m β]
-    [Productive α m] :
-    FinitenessRelation (Take α m) m where
-  rel := Take.Rel m
-  wf := by
-    rw [Rel]
-    split
-    all_goals
-      apply InvImage.wf
-      refine ⟨fun (a, b) => Prod.lexAccessible (WellFounded.apply ?_ a) (WellFounded.apply ?_) b⟩
-      · exact WellFoundedRelation.wf
-      · exact WellFoundedRelation.wf
-  subrelation {it it'} h := by
-    obtain ⟨step, h, h'⟩ := h
-    cases h'
-    case yield it' out k h' h'' =>
-      cases h
-      cases it.internalState.finite
-      · apply rel_of_countdown
-        simp only
-        omega
-      · by_cases h : it.internalState.countdown = 0
-        · simp only [h, Nat.zero_le, Nat.sub_eq_zero_of_le]
-          apply rel_of_zero_of_inner h rfl
-          exact .single ⟨_, rfl, h'⟩
-        · apply rel_of_countdown
-          simp only
-          omega
-    case skip it' out k h' h'' =>
-      cases h
-      by_cases h : it.internalState.countdown = 0
-      · simp only [h]
-        apply Take.rel_of_zero_of_inner h rfl
-        exact .single ⟨_, rfl, h'⟩
-      · obtain ⟨it, k, rfl⟩ := IterM.take.surjective_of_zero_lt it (by omega)
-        apply Take.rel_of_inner
-        exact IterM.TerminationMeasures.Productive.rel_of_skip h'
-    case done _ =>
-      cases h
-    case depleted _ =>
-      cases h
-
-instance Take.instFinite [Monad m] [Iterator α m β] [Productive α m] :
-    Finite (Take α m) m :=
-  by exact Finite.of_finitenessRelation instFinitenessRelation
-
-instance Take.instIteratorCollect {n : Type w → Type w'} [Monad m] [Monad n] [Iterator α m β] :
-    IteratorCollect (Take α m) m n :=
-  .defaultImplementation
-
-instance Take.instIteratorCollectPartial {n : Type w → Type w'} [Monad m] [Monad n] [Iterator α m β] :
-    IteratorCollectPartial (Take α m) m n :=
-  .defaultImplementation
-
-instance Take.instIteratorLoop {n : Type x → Type x'} [Monad m] [Monad n] [Iterator α m β] :
-    IteratorLoop (Take α m) m n :=
-  .defaultImplementation
-
-instance Take.instIteratorLoopPartial [Monad m] [Monad n] [Iterator α m β] :
-    IteratorLoopPartial (Take α m) m n :=
-  .defaultImplementation
-
-end Std.Iterators

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

@@ -74,7 +74,7 @@ variable {α : Type u} {m : Type u → Type u'} {n : Type max u v → Type v'}
 /--
 Transforms a step of the base iterator into a step of the `uLift` iterator.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 def Types.ULiftIterator.Monadic.modifyStep (step : IterStep (IterM (α := α) m β) β) :
     IterStep (IterM (α := ULiftIterator.{v} α m n β lift) n (ULift.{v} β)) (ULift.{v} β) :=
   match step with
@@ -140,6 +140,15 @@ instance Types.ULiftIterator.instIteratorCollectPartial {o} [Monad n] [Monad o]
     IteratorCollectPartial (ULiftIterator α m n β lift) n o :=
   .defaultImplementation
 
+instance Types.ULiftIterator.instIteratorSize [Monad n] [Iterator α m β] [IteratorSize α m]
+    [Finite (ULiftIterator α m n β lift) n] :
+    IteratorSize (ULiftIterator α m n β lift) n :=
+  .defaultImplementation
+
+instance Types.ULiftIterator.instIteratorSizePartial [Monad n] [Iterator α m β] [IteratorSize α m] :
+    IteratorSizePartial (ULiftIterator α m n β lift) n :=
+  .defaultImplementation
+
 /--
 Transforms an `m`-monadic iterator with values in `β` into an `n`-monadic iterator with
 values in `ULift β`. Requires a `MonadLift m (ULiftT n)` instance.

src/Init/Data/Iterators/Combinators/Take.lean

@@ -1,70 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Paul Reichert
--/
-module
-
-prelude
-public import Init.Data.Iterators.Combinators.Monadic.Take
-
-@[expose] public section
-
-namespace Std.Iterators
-
-/--
-Given an iterator `it` and a natural number `n`, `it.take n` is an iterator that outputs
-up to the first `n` of `it`'s values in order and then terminates.
-
-**Marble diagram:**
-
-```text
-it          ---a----b---c--d-e--⊥
-it.take 3   ---a----b---c⊥
-
-it          ---a--⊥
-it.take 3   ---a--⊥
-```
-
-**Termination properties:**
-
-* `Finite` instance: only if `it` is productive
-* `Productive` instance: only if `it` is productive
-
-**Performance:**
-
-This combinator incurs an additional O(1) cost with each output of `it`.
--/
-@[always_inline, inline]
-def Iter.take {α : Type w} {β : Type w} [Iterator α Id β] (n : Nat) (it : Iter (α := α) β) :
-    Iter (α := Take α Id) β :=
-  it.toIterM.take n |>.toIter
-
-/--
-This combinator is only useful for advanced use cases.
-
-Given a finite iterator `it`, returns an iterator that behaves exactly like `it` but is of the same
-type as `it.take n`.
-
-**Marble diagram:**
-
-```text
-it          ---a----b---c--d-e--⊥
-it.toTake   ---a----b---c--d-e--⊥
-```
-
-**Termination properties:**
-
-* `Finite` instance: always
-* `Productive` instance: always
-
-**Performance:**
-
-This combinator incurs an additional O(1) cost with each output of `it`.
--/
-@[always_inline, inline]
-def Iter.toTake {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] (it : Iter (α := α) β) :
-    Iter (α := Take α Id) β :=
-  it.toIterM.toTake.toIter
-
-end Std.Iterators

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

@@ -9,8 +9,6 @@ prelude
 public import Init.Data.Iterators.Consumers.Collect
 public import Init.Data.Iterators.Consumers.Monadic.Loop
 
-set_option linter.missingDocs true
-
 public section
 
 /-!
@@ -48,9 +46,6 @@ instance (α : Type w) (β : Type w) (n : Type x → Type x') [Monad n]
   haveI : ForIn' n (Iter (α := α) β) β _ := Iter.instForIn'
   instForInOfForIn'
 
-/--
-An implementation of `for h : ... in ... do ...` notation for partial iterators.
--/
 @[always_inline, inline]
 def Iter.Partial.instForIn' {α : Type w} {β : Type w} {n : Type x → Type x'} [Monad n]
     [Iterator α Id β] [IteratorLoopPartial α Id n] :
@@ -68,12 +63,12 @@ instance (α : Type w) (β : Type w) (n : Type x → Type x') [Monad n]
   instForInOfForIn'
 
 instance {m : Type x → Type x'}
-    {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id m] [Monad m] :
+    {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id m] :
     ForM m (Iter (α := α) β) β where
   forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
 
 instance {m : Type x → Type x'}
-    {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoopPartial α Id m] [Monad m] :
+    {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoopPartial α Id m] :
     ForM m (Iter.Partial (α := α) β) β where
   forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
 
@@ -207,11 +202,6 @@ def Iter.all {α β : Type w}
     (p : β → Bool) (it : Iter (α := α) β) : Bool :=
   (it.allM (fun x => pure (f := Id) (p x))).run
 
-/--
-Steps through the iterator until the monadic function `f` returns `some` for an element, at which
-point iteration stops and the result of `f` is returned. If the iterator is completely consumed
-without `f` returning `some`, then the result is `none`.
--/
 @[inline]
 def Iter.findSomeM? {α β : Type w} {γ : Type x} {m : Type x → Type w'} [Monad m] [Iterator α Id β]
     [IteratorLoop α Id m] [Finite α Id] (it : Iter (α := α) β) (f : β → m (Option γ)) :
@@ -221,7 +211,7 @@ def Iter.findSomeM? {α β : Type w} {γ : Type x} {m : Type x → Type w'} [Mon
     | none => return .yield none
     | some fx => return .done (some fx))
 
-@[inline, inherit_doc Iter.findSomeM?]
+@[inline]
 def Iter.Partial.findSomeM? {α β : Type w} {γ : Type x} {m : Type x → Type w'} [Monad m]
     [Iterator α Id β] [IteratorLoopPartial α Id m] (it : Iter.Partial (α := α) β)
     (f : β → m (Option γ)) :
@@ -231,100 +221,62 @@ def Iter.Partial.findSomeM? {α β : Type w} {γ : Type x} {m : Type x → Type
     | none => return .yield none
     | some fx => return .done (some fx))
 
-/--
-Steps through the iterator until `f` returns `some` for an element, at which point iteration stops
-and the result of `f` is returned. If the iterator is completely consumed without `f` returning
-`some`, then the result is `none`.
--/
 @[inline]
 def Iter.findSome? {α β : Type w} {γ : Type x} [Iterator α Id β]
     [IteratorLoop α Id Id] [Finite α Id] (it : Iter (α := α) β) (f : β → Option γ) :
     Option γ :=
   Id.run (it.findSomeM? (pure <| f ·))
 
-@[inline, inherit_doc Iter.findSome?]
+@[inline]
 def Iter.Partial.findSome? {α β : Type w} {γ : Type x} [Iterator α Id β]
     [IteratorLoopPartial α Id Id] (it : Iter.Partial (α := α) β) (f : β → Option γ) :
     Option γ :=
   Id.run (it.findSomeM? (pure <| f ·))
 
-/--
-Steps through the iterator until an element satisfies the monadic predicate `f`, at which point
-iteration stops and the element is returned. If no element satisfies `f`, then the result is
-`none`.
--/
 @[inline]
 def Iter.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β]
     [IteratorLoop α Id m] [Finite α Id] (it : Iter (α := α) β) (f : β → m (ULift Bool)) :
     m (Option β) :=
   it.findSomeM? (fun x => return if (← f x).down then some x else none)
 
-@[inline, inherit_doc Iter.findM?]
+@[inline]
 def Iter.Partial.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β]
     [IteratorLoopPartial α Id m] (it : Iter.Partial (α := α) β) (f : β → m (ULift Bool)) :
     m (Option β) :=
   it.findSomeM? (fun x => return if (← f x).down then some x else none)
 
-/--
-Steps through the iterator until an element satisfies `f`, at which point iteration stops and the
-element is returned. If no element satisfies `f`, then the result is `none`.
--/
 @[inline]
 def Iter.find? {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
     [Finite α Id] (it : Iter (α := α) β) (f : β → Bool) : Option β :=
   Id.run (it.findM? (pure <| .up <| f ·))
 
-@[inline, inherit_doc Iter.find?]
+@[inline]
 def Iter.Partial.find? {α β : Type w} [Iterator α Id β] [IteratorLoopPartial α Id Id]
     (it : Iter.Partial (α := α) β) (f : β → Bool) : Option β :=
   Id.run (it.findM? (pure <| .up <| f ·))
 
-/--
-Steps through the whole iterator, counting the number of outputs emitted.
-
-**Performance**:
-
-This function's runtime is linear in the number of steps taken by the iterator.
--/
-@[always_inline, inline, expose]
-def Iter.count {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id]
+@[always_inline, inline, expose, inherit_doc IterM.size]
+def Iter.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorSize α Id]
     (it : Iter (α := α) β) : Nat :=
-  it.toIterM.count.run.down
+  (IteratorSize.size it.toIterM).run.down
 
-/--
-Steps through the whole iterator, counting the number of outputs emitted.
-
-**Performance**:
-
-This function's runtime is linear in the number of steps taken by the iterator.
--/
-@[always_inline, inline, expose, deprecated Iter.count (since := "2025-10-29")]
-def Iter.size {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id]
+@[always_inline, inline, inherit_doc IterM.Partial.size]
+def Iter.Partial.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorSizePartial α Id]
     (it : Iter (α := α) β) : Nat :=
-   it.count
+  (IteratorSizePartial.size it.toIterM).run.down
 
 /--
-Steps through the whole iterator, counting the number of outputs emitted.
+`LawfulIteratorSize α m` ensures that the `size` function of an iterator behaves as if it
+iterated over the whole iterator, counting its elements and causing all the monadic side effects
+of the iterations. This is a fairly strong condition for monadic iterators and it will be false
+for many efficient implementations of `size` that compute the size without actually iterating.
 
-**Performance**:
-
-This function's runtime is linear in the number of steps taken by the iterator.
+This class is experimental and users of the iterator API should not explicitly depend on it.
 -/
-@[always_inline, inline, expose]
-def Iter.Partial.count {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoopPartial α Id Id]
-    (it : Iter.Partial (α := α) β) : Nat :=
-  it.it.toIterM.allowNontermination.count.run.down
-
-/--
-Steps through the whole iterator, counting the number of outputs emitted.
-
-**Performance**:
-
-This function's runtime is linear in the number of steps taken by the iterator.
--/
-@[always_inline, inline, expose, deprecated Iter.Partial.count (since := "2025-10-29")]
-def Iter.Partial.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoopPartial α Id Id]
-    (it : Iter.Partial (α := α) β) : Nat :=
-  it.count
+class LawfulIteratorSize (α : Type w) {β : Type w} [Iterator α Id β] [Finite α Id]
+    [IteratorSize α Id] where
+    size_eq_size_toArray {it : Iter (α := α) β} : it.size =
+      haveI : IteratorCollect α Id Id := .defaultImplementation
+      it.toArray.size
 
 end Std.Iterators

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

@@ -88,6 +88,27 @@ class IteratorLoopPartial (α : Type w) (m : Type w → Type w') {β : Type w} [
       (it : IterM (α := α) m β) → γ →
       ((b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (ForInStep γ)) → n γ
 
+/--
+`IteratorSize α m` provides an implementation of the `IterM.size` function.
+
+This class is experimental and users of the iterator API should not explicitly depend on it.
+They can, however, assume that consumers that require an instance will work for all iterators
+provided by the standard library.
+-/
+class IteratorSize (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where
+  size : IterM (α := α) m β → m (ULift Nat)
+
+/--
+`IteratorSizePartial α m` provides an implementation of the `IterM.Partial.size` function that
+can be used as `it.allowTermination.size`.
+
+This class is experimental and users of the iterator API should not explicitly depend on it.
+They can, however, assume that consumers that require an instance will work for all iterators
+provided by the standard library.
+-/
+class IteratorSizePartial (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where
+  size : IterM (α := α) m β → m (ULift Nat)
+
 end Typeclasses
 
 /-- Internal implementation detail of the iterator library. -/
@@ -247,10 +268,10 @@ This `ForIn'`-style loop construct traverses a finite iterator using an `Iterato
 -/
 @[always_inline, inline]
 def IteratorLoop.finiteForIn' {m : Type w → Type w'} {n : Type x → Type x'}
-    {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n] [Monad n]
+    {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n]
     (lift : ∀ γ δ, (γ → n δ) → m γ → n δ) :
     ForIn' n (IterM (α := α) m β) β ⟨fun it out => it.IsPlausibleIndirectOutput out⟩ where
-  forIn' {γ} it init f :=
+  forIn' {γ} [Monad n] it init f :=
     IteratorLoop.forIn (α := α) (m := m) lift γ (fun _ _ _ => True)
       wellFounded_of_finite
       it init (fun out h acc => (⟨·, .intro⟩) <$> f out h acc)
@@ -288,13 +309,13 @@ instance {m : Type w → Type w'} {n : Type w → Type w''}
   instForInOfForIn'
 
 instance {m : Type w → Type w'} {n : Type w → Type w''}
-    {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n] [Monad n]
+    {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n]
     [MonadLiftT m n] :
     ForM n (IterM (α := α) m β) β where
   forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
 
 instance {m : Type w → Type w'} {n : Type w → Type w''}
-    {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoopPartial α m n] [Monad n]
+    {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoopPartial α m n]
     [MonadLiftT m n] :
     ForM n (IterM.Partial (α := α) m β) β where
   forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
@@ -612,58 +633,86 @@ def IterM.Partial.find? {α β : Type w} {m : Type w → Type w'} [Monad m] [Ite
     m (Option β) :=
   it.findM? (pure <| .up <| f ·)
 
-section Count
+section Size
 
 /--
-Steps through the whole iterator, counting the number of outputs emitted.
-
-**Performance**:
-
-This function's runtime is linear in the number of steps taken by the iterator.
+This is the implementation of the default instance `IteratorSize.defaultImplementation`.
 -/
 @[always_inline, inline]
-def IterM.count {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] [Finite α m]
-    [IteratorLoop α m m]
-    [Monad m] (it : IterM (α := α) m β) : m (ULift Nat) :=
+def IterM.DefaultConsumers.size {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
+    [Iterator α m β] [IteratorLoop α m m] [Finite α m] (it : IterM (α := α) m β) :
+    m (ULift Nat) :=
   it.fold (init := .up 0) fun acc _ => .up (acc.down + 1)
 
 /--
-Steps through the whole iterator, counting the number of outputs emitted.
-
-**Performance**:
-
-This function's runtime is linear in the number of steps taken by the iterator.
--/
-@[always_inline, inline, deprecated IterM.count (since := "2025-10-29")]
-def IterM.size {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] [Finite α m]
-    [IteratorLoop α m m]
-    [Monad m] (it : IterM (α := α) m β) : m (ULift Nat) :=
-  it.count
-
-/--
-Steps through the whole iterator, counting the number of outputs emitted.
-
-**Performance**:
-
-This function's runtime is linear in the number of steps taken by the iterator.
+This is the implementation of the default instance `IteratorSizePartial.defaultImplementation`.
 -/
 @[always_inline, inline]
-def IterM.Partial.count {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
-    [IteratorLoopPartial α m m] [Monad m] (it : IterM.Partial (α := α) m β) : m (ULift Nat) :=
-  it.fold (init := .up 0) fun acc _ => .up (acc.down + 1)
+def IterM.DefaultConsumers.sizePartial {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
+    [Iterator α m β] [IteratorLoopPartial α m m] (it : IterM (α := α) m β) :
+    m (ULift Nat) :=
+  it.allowNontermination.fold (init := .up 0) fun acc _ => .up (acc.down + 1)
 
 /--
-Steps through the whole iterator, counting the number of outputs emitted.
+This is the default implementation of the `IteratorSize` class.
+It simply iterates using `IteratorLoop` and counts the elements.
+For certain iterators, more efficient implementations are possible and should be used instead.
+-/
+@[always_inline, inline]
+def IteratorSize.defaultImplementation {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α m β] [Finite α m] [IteratorLoop α m m] :
+    IteratorSize α m where
+  size := IterM.DefaultConsumers.size
+
+
+/--
+This is the default implementation of the `IteratorSizePartial` class.
+It simply iterates using `IteratorLoopPartial` and counts the elements.
+For certain iterators, more efficient implementations are possible and should be used instead.
+-/
+@[always_inline, inline]
+instance IteratorSizePartial.defaultImplementation {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α m β] [IteratorLoopPartial α m m] :
+    IteratorSizePartial α m where
+  size := IterM.DefaultConsumers.sizePartial
+
+/--
+Computes how many elements the iterator returns. In monadic situations, it is unclear which effects
+are caused by calling `size`, and if the monad is nondeterministic, it is also unclear what the
+returned value should be. The reference implementation, `IteratorSize.defaultImplementation`,
+simply iterates over the whole iterator monadically, counting the number of emitted values.
+An `IteratorSize` instance is considered lawful if it is equal to the reference implementation.
 
 **Performance**:
 
-This function's runtime is linear in the number of steps taken by the iterator.
+Default performance is linear in the number of steps taken by the iterator.
 -/
-@[always_inline, inline, deprecated IterM.Partial.count (since := "2025-10-29")]
-def IterM.Partial.size {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
-    [IteratorLoopPartial α m m] [Monad m] (it : IterM.Partial (α := α) m β) : m (ULift Nat) :=
-  it.count
+@[always_inline, inline]
+def IterM.size {α : Type} {m : Type → Type w'} {β : Type} [Iterator α m β] [Monad m]
+    (it : IterM (α := α) m β) [IteratorSize α m] : m Nat :=
+  ULift.down <$> IteratorSize.size it
 
-end Count
+/--
+Computes how many elements the iterator emits.
+
+With monadic iterators (`IterM`), it is unclear which effects
+are caused by calling `size`, and if the monad is nondeterministic, it is also unclear what the
+returned value should be. The reference implementation, `IteratorSize.defaultImplementation`,
+simply iterates over the whole iterator monadically, counting the number of emitted values.
+An `IteratorSize` instance is considered lawful if it is equal to the reference implementation.
+
+This is the partial version of `size`. It does not require a proof of finiteness and might loop
+forever. It is not possible to verify the behavior in Lean because it uses `partial`.
+
+**Performance**:
+
+Default performance is linear in the number of steps taken by the iterator.
+-/
+@[always_inline, inline]
+def IterM.Partial.size {α : Type} {m : Type → Type w'} {β : Type} [Iterator α m β] [Monad m]
+    (it : IterM.Partial (α := α) m β) [IteratorSizePartial α m] : m Nat :=
+  ULift.down <$> IteratorSizePartial.size it.it
+
+end Size
 
 end Std.Iterators

src/Init/Data/Iterators/Lemmas.lean

@@ -8,4 +8,3 @@ module
 prelude
 public import Init.Data.Iterators.Lemmas.Consumers
 public import Init.Data.Iterators.Lemmas.Combinators
-public import Init.Data.Iterators.Lemmas.Producers

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

@@ -10,5 +10,4 @@ public import Init.Data.Iterators.Lemmas.Combinators.Attach
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic
 public import Init.Data.Iterators.Lemmas.Combinators.FilterMap
 public import Init.Data.Iterators.Lemmas.Combinators.FlatMap
-public import Init.Data.Iterators.Lemmas.Combinators.Take
 public import Init.Data.Iterators.Lemmas.Combinators.ULift

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

@@ -11,7 +11,6 @@ import all Init.Data.Iterators.Combinators.Attach
 import all Init.Data.Iterators.Combinators.Monadic.Attach
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
 public import Init.Data.Iterators.Lemmas.Consumers.Collect
-public import Init.Data.Iterators.Lemmas.Consumers.Loop
 public import Init.Data.Array.Attach
 
 public section
@@ -83,14 +82,4 @@ theorem Iter.toArray_attachWith [Iterator α Id β]
     simpa only [Array.toList_inj]
   simp [Iter.toList_toArray]
 
-@[simp]
-theorem Iter.count_attachWith [Iterator α Id β]
-    {it : Iter (α := α) β} {hP}
-    [Finite α Id] [IteratorLoop α Id Id]
-    [LawfulIteratorLoop α Id Id] :
-    (it.attachWith P hP).count = it.count := by
-  letI : IteratorCollect α Id Id := .defaultImplementation
-  rw [← Iter.length_toList_eq_count, toList_attachWith]
-  simp
-
 end Std.Iterators

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

@@ -467,17 +467,6 @@ theorem Iter.fold_map {α β γ : Type w} {δ : Type x}
 
 end Fold
 
-section Count
-
-@[simp]
-theorem Iter.count_map {α β β' : Type w} [Iterator α Id β]
-    [IteratorLoop α Id Id] [Finite α Id] [LawfulIteratorLoop α Id Id]
-    {it : Iter (α := α) β} {f : β → β'} :
-    (it.map f).count = it.count := by
-  simp [map_eq_toIter_map_toIterM, count_eq_count_toIterM]
-
-end Count
-
 theorem Iter.anyM_filterMapM {α β β' : Type w} {m : Type w → Type w'}
     [Iterator α Id β] [Finite α Id] [Monad m] [LawfulMonad m]
     {it : Iter (α := α) β} {f : β → m (Option β')} {p : β' → m (ULift Bool)} :

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

@@ -9,5 +9,4 @@ prelude
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
-public import Init.Data.Iterators.Lemmas.Combinators.Monadic.Take
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift

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

@@ -9,7 +9,6 @@ prelude
 public import Init.Data.Iterators.Combinators.Monadic.Attach
 import all Init.Data.Iterators.Combinators.Monadic.Attach
 public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
-public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
 
 public section
 
@@ -60,14 +59,4 @@ theorem IterM.map_unattach_toArray_attachWith [Iterator α m β] [Monad m] [Mona
   rw [← toArray_toList, ← toArray_toList, ← map_unattach_toList_attachWith (it := it) (hP := hP)]
   simp [-map_unattach_toList_attachWith, -IterM.toArray_toList]
 
-@[simp]
-theorem IterM.count_attachWith [Iterator α m β] [Monad m] [Monad n]
-    {it : IterM (α := α) m β} {hP}
-    [Finite α m] [IteratorLoop α m m] [LawfulMonad m] [LawfulIteratorLoop α m m] :
-    (it.attachWith P hP).count = it.count := by
-  letI : IteratorCollect α m m := .defaultImplementation
-  rw [← up_length_toList_eq_count, ← up_length_toList_eq_count,
-    ← map_unattach_toList_attachWith (it := it) (P := P) (hP := hP)]
-  simp only [Functor.map_map, List.length_unattach]
-
 end Std.Iterators

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

@@ -895,23 +895,6 @@ theorem IterM.fold_map {α β γ δ : Type w} {m : Type w → Type w'}
 
 end Fold
 
-section Count
-
-@[simp]
-theorem IterM.count_map {α β β' : Type w} {m : Type w → Type w'} [Iterator α m β] [Monad m]
-    [IteratorLoop α m m] [Finite α m] [LawfulMonad m] [LawfulIteratorLoop α m m]
-    {it : IterM (α := α) m β} {f : β → β'} :
-    (it.map f).count = it.count := by
-  induction it using IterM.inductSteps with | step it ihy ihs
-  rw [count_eq_match_step, count_eq_match_step, step_map, bind_assoc]
-  apply bind_congr; intro step
-  cases step.inflate using PlausibleIterStep.casesOn
-  · simp [ihy ‹_›]
-  · simp [ihs ‹_›]
-  · simp
-
-end Count
-
 section AnyAll
 
 theorem IterM.anyM_filterMapM {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''}

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

@@ -1,77 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Paul Reichert
--/
-module
-
-prelude
-public import Init.Data.Iterators.Combinators.Monadic.Take
-public import Init.Data.Iterators.Lemmas.Consumers.Monadic
-
-@[expose] public section
-
-namespace Std.Iterators
-
-theorem Take.isPlausibleStep_take_yield [Monad m] [Iterator α m β] {n : Nat}
-    {it : IterM (α := α) m β} (h : it.IsPlausibleStep (.yield it' out)) :
-    (it.take (n + 1)).IsPlausibleStep (.yield (it'.take n) out) :=
-  (.yield h (by simp [IterM.take]))
-
-theorem Take.isPlausibleStep_take_skip [Monad m] [Iterator α m β] {n : Nat}
-    {it : IterM (α := α) m β} (h : it.IsPlausibleStep (.skip it')) :
-    (it.take (n + 1)).IsPlausibleStep (.skip (it'.take (n + 1))) :=
-  (.skip h (by simp [IterM.take]))
-
-theorem IterM.step_take {α m β} [Monad m] [Iterator α m β] {n : Nat}
-    {it : IterM (α := α) m β} :
-    (it.take n).step = (match n with
-      | 0 => pure <| .deflate <| .done (.depleted rfl)
-      | k + 1 => do
-        match (← it.step).inflate with
-        | .yield it' out h => pure <| .deflate <| .yield (it'.take k) out (Take.isPlausibleStep_take_yield h)
-        | .skip it' h => pure <| .deflate <| .skip (it'.take (k + 1)) (Take.isPlausibleStep_take_skip h)
-        | .done h => pure <| .deflate <| .done (.done h)) := by
-  simp only [take, step, Iterator.step, internalState_toIterM]
-  cases n
-  case zero => rfl
-  case succ k =>
-    apply bind_congr
-    intro step
-    cases step.inflate using PlausibleIterStep.casesOn <;> rfl
-
-theorem IterM.toList_take_zero {α m β} [Monad m] [LawfulMonad m] [Iterator α m β]
-    [Finite (Take α m) m]
-    [IteratorCollect (Take α m) m m] [LawfulIteratorCollect (Take α m) m m]
-    {it : IterM (α := α) m β} :
-    (it.take 0).toList = pure [] := by
-  rw [toList_eq_match_step]
-  simp [step_take]
-
-theorem IterM.step_toTake {α m β} [Monad m] [Iterator α m β] [Finite α m]
-    {it : IterM (α := α) m β} :
-    it.toTake.step = (do
-        match (← it.step).inflate with
-        | .yield it' out h => pure <| .deflate <| .yield it'.toTake out (.yield h Nat.zero_ne_one)
-        | .skip it' h => pure <| .deflate <| .skip it'.toTake (.skip h Nat.zero_ne_one)
-        | .done h => pure <| .deflate <| .done (.done h)) := by
-  simp only [toTake, step, Iterator.step, internalState_toIterM]
-  apply bind_congr
-  intro step
-  cases step.inflate using PlausibleIterStep.casesOn <;> rfl
-
-@[simp]
-theorem IterM.toList_toTake {α m β} [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
-    [IteratorCollect α m m] [LawfulIteratorCollect α m m]
-    {it : IterM (α := α) m β} :
-    it.toTake.toList = it.toList := by
-  induction it using IterM.inductSteps with | step it ihy ihs
-  rw [toList_eq_match_step, toList_eq_match_step]
-  simp only [step_toTake, bind_assoc]
-  apply bind_congr; intro step
-  cases step.inflate using PlausibleIterStep.casesOn
-  · simp [ihy ‹_›]
-  · simp [ihs ‹_›]
-  · simp
-
-end Std.Iterators

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

@@ -7,8 +7,8 @@ module
 
 prelude
 public import Init.Data.Iterators.Combinators.Monadic.ULift
+import all Init.Data.Iterators.Combinators.Monadic.ULift
 public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
-public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
 
 public section
 
@@ -20,13 +20,9 @@ variable {α : Type u} {m : Type u → Type u'} {n : Type max u v → Type v'}
 theorem IterM.step_uLift [Iterator α m β] [Monad n] {it : IterM (α := α) m β}
     [MonadLiftT m (ULiftT n)] :
     (it.uLift n).step = (do
-      match (← (monadLift it.step : ULiftT n _).run).down.inflate with
-      | .yield it' out h => return .deflate (.yield (it'.uLift n) (.up out) ⟨_, h, rfl⟩)
-      | .skip it' h => return .deflate (.skip (it'.uLift n) ⟨_, h, rfl⟩)
-      | .done h => return .deflate (.done ⟨_, h, rfl⟩)) := by
-  simp only [IterM.step, Iterator.step, IterM.uLift]
-  apply bind_congr; intro step
-  split <;> simp [Types.ULiftIterator.Monadic.modifyStep, *]
+      let step := (← (monadLift it.step : ULiftT n _).run).down
+      return .deflate ⟨Types.ULiftIterator.Monadic.modifyStep step.inflate.val, step.inflate.val, step.inflate.property, rfl⟩) :=
+  rfl
 
 @[simp]
 theorem IterM.toList_uLift [Iterator α m β] [Monad m] [Monad n] {it : IterM (α := α) m β}
@@ -37,11 +33,14 @@ theorem IterM.toList_uLift [Iterator α m β] [Monad m] [Monad n] {it : IterM (
       (fun l => l.down.map ULift.up) <$> (monadLift it.toList : ULiftT n _).run := by
   induction it using IterM.inductSteps with | step it ihy ihs
   rw [IterM.toList_eq_match_step, IterM.toList_eq_match_step, step_uLift]
-  simp only [bind_assoc, map_eq_pure_bind, monadLift_bind, ULiftT.run_bind]
-  apply bind_congr; intro step
+  simp only [bind_pure_comp, bind_map_left, liftM_bind, ULiftT.run_bind, map_bind]
+  apply bind_congr
+  intro step
+  simp [Types.ULiftIterator.Monadic.modifyStep]
   cases step.down.inflate using PlausibleIterStep.casesOn
-  · simp [ihy ‹_›]
-  · simp [ihs ‹_›]
+  · simp only [uLift] at ihy
+    simp [ihy ‹_›]
+  · exact ihs ‹_›
   · simp
 
 @[simp]
@@ -64,20 +63,4 @@ theorem IterM.toArray_uLift [Iterator α m β] [Monad m] [Monad n] {it : IterM (
   rw [← toArray_toList, ← toArray_toList, toList_uLift, monadLift_map]
   simp
 
-@[simp]
-theorem IterM.count_uLift [Iterator α m β] [Monad m] [Monad n] {it : IterM (α := α) m β}
-    [MonadLiftT m (ULiftT n)] [Finite α m] [IteratorLoop α m m]
-    [LawfulMonad m] [LawfulMonad n] [LawfulIteratorLoop α m m]
-    [LawfulMonadLiftT m (ULiftT n)] :
-    (it.uLift n).count =
-      (.up ·.down.down) <$> (monadLift (n := ULiftT n) it.count).run := by
-  induction it using IterM.inductSteps with | step it ihy ihs
-  rw [count_eq_match_step, count_eq_match_step, monadLift_bind, map_eq_pure_bind, step_uLift]
-  simp only [bind_assoc, ULiftT.run_bind]
-  apply bind_congr; intro step
-  cases step.down.inflate using PlausibleIterStep.casesOn
-  · simp [ihy ‹_›]
-  · simp [ihs ‹_›]
-  · simp
-
 end Std.Iterators

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

@@ -10,7 +10,6 @@ public import Init.Data.Iterators.Combinators.ULift
 import all Init.Data.Iterators.Combinators.ULift
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
 public import Init.Data.Iterators.Lemmas.Consumers.Collect
-public import Init.Data.Iterators.Lemmas.Consumers.Loop
 
 public section
 
@@ -23,16 +22,14 @@ theorem Iter.uLift_eq_toIter_uLift_toIterM {it : Iter (α := α) β} :
   rfl
 
 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⟩
-      | .skip it' h => .skip it'.uLift ⟨_, h, rfl⟩
-      | .done h => .done ⟨_, h, rfl⟩ := by
+    it.uLift.step =
+      ⟨Types.ULiftIterator.modifyStep it.step.val,
+        it.step.val.mapIterator Iter.toIterM, it.step.property,
+        by simp [Types.ULiftIterator.modifyStep]⟩ := by
   rw [Subtype.ext_iff]
   simp only [uLift_eq_toIter_uLift_toIterM, step, IterM.Step.toPure, toIterM_toIter,
-    IterM.step_uLift, toIter_toIterM]
-  simp only [monadLift, ULiftT.run_pure, PlausibleIterStep.yield, PlausibleIterStep.skip,
-    PlausibleIterStep.done, pure_bind]
-  cases it.toIterM.step.run.inflate using PlausibleIterStep.casesOn <;> simp
+    IterM.step_uLift, bind_pure_comp, Id.run_map, toIter_toIterM]
+  simp [Types.ULiftIterator.modifyStep, monadLift]
 
 @[simp]
 theorem Iter.toList_uLift [Iterator α Id β] {it : Iter (α := α) β}
@@ -58,12 +55,4 @@ theorem Iter.toArray_uLift [Iterator α Id β] {it : Iter (α := α) β}
   rw [← toArray_toList, ← toArray_toList, toList_uLift]
   simp [-toArray_toList]
 
-@[simp]
-theorem Iter.count_uLift [Iterator α Id β] {it : Iter (α := α) β}
-    [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] :
-    it.uLift.count = it.count := by
-  simp only [monadLift, uLift_eq_toIter_uLift_toIterM, count_eq_count_toIterM, toIterM_toIter]
-  rw [IterM.count_uLift]
-  simp [monadLift]
-
 end Std.Iterators

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

@@ -68,7 +68,8 @@ theorem Iter.forIn_eq {α β : Type w} [Iterator α Id β] [Finite α Id]
   rw [← h]
 
 theorem Iter.forIn'_eq_forIn'_toIterM {α β : Type w} [Iterator α Id β]
-    [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m] [IteratorLoop α Id m]
+    [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
+    [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
     {γ : Type w} {it : Iter (α := α) β} {init : γ}
     {f : (out : β) → _ → γ → m (ForInStep γ)} :
     letI : ForIn' m (Iter (α := α) β) β _ := Iter.instForIn'
@@ -80,7 +81,7 @@ theorem Iter.forIn'_eq_forIn'_toIterM {α β : Type w} [Iterator α Id β]
 
 theorem Iter.forIn_eq_forIn_toIterM {α β : Type w} [Iterator α Id β]
     [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
-    [IteratorLoop α Id m]
+    [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
     {γ : Type w} {it : Iter (α := α) β} {init : γ}
     {f : β → γ → m (ForInStep γ)} :
     ForIn.forIn it init f =
@@ -330,7 +331,7 @@ theorem Iter.foldM_eq_forIn {α β : Type w} {γ : Type x} [Iterator α Id β] [
 
 theorem Iter.foldM_eq_foldM_toIterM {α β : Type w} [Iterator α Id β]
     [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
-    [IteratorLoop α Id m]
+    [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
     {γ : Type w} {it : Iter (α := α) β} {init : γ} {f : γ → β → m γ} :
     it.foldM (init := init) f = it.toIterM.foldM (init := init) f := by
   simp [foldM_eq_forIn, IterM.foldM_eq_forIn, forIn_eq_forIn_toIterM]
@@ -395,7 +396,7 @@ theorem Iter.fold_eq_foldM {α β : Type w} {γ : Type x} [Iterator α Id β]
   simp [foldM_eq_forIn, fold_eq_forIn]
 
 theorem Iter.fold_eq_fold_toIterM {α β : Type w} {γ : Type w} [Iterator α Id β]
-    [Finite α Id] [IteratorLoop α Id Id]
+    [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α 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]
@@ -421,9 +422,8 @@ theorem Iter.fold_eq_match_step {α β : Type w} {γ : Type x} [Iterator α Id
   cases step using PlausibleIterStep.casesOn <;> simp
 
 -- The argument `f : γ₁ → γ₂` is intentionally explicit, as it is sometimes not found by unification.
-theorem Iter.fold_hom {γ₁ : Type x₁} {γ₂ : Type x₂} [Iterator α Id β] [Finite α Id]
-    [IteratorLoop α Id Id.{x₁}] [LawfulIteratorLoop α Id Id.{x₁}]
-    [IteratorLoop α Id Id.{x₂}] [LawfulIteratorLoop α Id Id.{x₂}]
+theorem Iter.fold_hom [Iterator α Id β] [Finite α Id]
+    [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
     {it : Iter (α := α) β}
     (f : γ₁ → γ₂) {g₁ : γ₁ → β → γ₁} {g₂ : γ₂ → β → γ₂} {init : γ₁}
     (H : ∀ x y, g₂ (f x) y = f (g₁ x y)) :
@@ -469,72 +469,30 @@ theorem Iter.foldl_toArray {α β : Type w} {γ : Type x} [Iterator α Id β] [F
     it.toArray.foldl (init := init) f = it.fold (init := init) f := by
   rw [fold_eq_foldM, Array.foldl_eq_foldlM, ← Iter.foldlM_toArray]
 
-theorem Iter.count_eq_count_toIterM {α β : Type w} [Iterator α Id β]
-    [Finite α Id] [IteratorLoop α Id Id.{w}] {it : Iter (α := α) β} :
-    it.count = it.toIterM.count.run.down :=
-  (rfl)
-
-theorem Iter.count_eq_fold {α β : Type w} [Iterator α Id β]
-    [Finite α Id] [IteratorLoop α Id Id.{w}] [LawfulIteratorLoop α Id Id.{w}]
-    [IteratorLoop α Id Id.{0}] [LawfulIteratorLoop α Id Id.{0}]
+@[simp]
+theorem Iter.size_toArray_eq_size {α β : Type w} [Iterator α Id β] [Finite α Id]
+    [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    [IteratorSize α Id] [LawfulIteratorSize α]
     {it : Iter (α := α) β} :
-    it.count = it.fold (γ := Nat) (init := 0) (fun acc _ => acc + 1) := by
-  rw [count_eq_count_toIterM, IterM.count_eq_fold, ← fold_eq_fold_toIterM]
-  rw [← fold_hom (f := ULift.down)]
-  simp
-
-theorem Iter.count_eq_forIn {α β : Type w} [Iterator α Id β]
-    [Finite α Id] [IteratorLoop α Id Id.{w}] [LawfulIteratorLoop α Id Id.{w}]
-    [IteratorLoop α Id Id.{0}] [LawfulIteratorLoop α Id Id.{0}]
-    {it : Iter (α := α) β} :
-    it.count = (ForIn.forIn (m := Id) it 0 (fun _ acc => return .yield (acc + 1))).run := by
-  rw [count_eq_fold, forIn_pure_yield_eq_fold, Id.run_pure]
-
-theorem Iter.count_eq_match_step {α β : Type w} [Iterator α Id β]
-    [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
-    {it : Iter (α := α) β} :
-    it.count = (match it.step.val with
-      | .yield it' _ => it'.count + 1
-      | .skip it' => it'.count
-      | .done => 0) := by
-  simp only [count_eq_count_toIterM]
-  rw [IterM.count_eq_match_step]
-  simp only [bind_pure_comp, id_map', Id.run_bind, Iter.step]
-  cases it.toIterM.step.run.inflate using PlausibleIterStep.casesOn <;> simp
+    it.toArray.size = it.size := by
+  simp only [toArray_eq_toArray_toIterM, LawfulIteratorCollect.toArray_eq]
+  simp [← toArray_eq_toArray_toIterM, LawfulIteratorSize.size_eq_size_toArray]
 
 @[simp]
-theorem Iter.size_toArray_eq_count {α β : Type w} [Iterator α Id β] [Finite α Id]
+theorem Iter.length_toList_eq_size {α β : Type w} [Iterator α Id β] [Finite α Id]
     [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
-    [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    [IteratorSize α Id] [LawfulIteratorSize α]
     {it : Iter (α := α) β} :
-    it.toArray.size = it.count := by
-  simp only [toArray_eq_toArray_toIterM, count_eq_count_toIterM, Id.run_map,
-    ← IterM.up_size_toArray_eq_count]
-
-@[deprecated Iter.size_toArray_eq_count (since := "2025-10-29")]
-def Iter.size_toArray_eq_size := @size_toArray_eq_count
+    it.toList.length = it.size := by
+  rw [← toList_toArray, Array.length_toList, size_toArray_eq_size]
 
 @[simp]
-theorem Iter.length_toList_eq_count {α β : Type w} [Iterator α Id β] [Finite α Id]
+theorem Iter.length_toListRev_eq_size {α β : Type w} [Iterator α Id β] [Finite α Id]
     [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
-    [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    [IteratorSize α Id] [LawfulIteratorSize α]
     {it : Iter (α := α) β} :
-    it.toList.length = it.count := by
-  rw [← toList_toArray, Array.length_toList, size_toArray_eq_count]
-
-@[deprecated Iter.length_toList_eq_count (since := "2025-10-29")]
-def Iter.length_toList_eq_size := @length_toList_eq_count
-
-@[simp]
-theorem Iter.length_toListRev_eq_count {α β : Type w} [Iterator α Id β] [Finite α Id]
-    [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
-    [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
-    {it : Iter (α := α) β} :
-    it.toListRev.length = it.count := by
-  rw [toListRev_eq, List.length_reverse, length_toList_eq_count]
-
-@[deprecated Iter.length_toListRev_eq_count (since := "2025-10-29")]
-def Iter.length_toListRev_eq_size := @length_toListRev_eq_count
+    it.toListRev.length = it.size := by
+  rw [toListRev_eq, List.length_reverse, length_toList_eq_size]
 
 theorem Iter.anyM_eq_forIn {α β : Type w} {m : Type → Type w'} [Iterator α Id β]
     [Finite α Id] [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]

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

@@ -335,73 +335,6 @@ theorem IterM.drain_eq_map_toArray {α β : Type w} {m : Type w → Type w'} [It
     it.drain = (fun _ => .unit) <$> it.toList := by
   simp [IterM.drain_eq_map_toList]
 
-theorem IterM.count_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
-    [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m]
-    {it : IterM (α := α) m β} :
-    it.count = it.fold (init := .up 0) (fun acc _ => .up <| acc.down + 1) :=
-  (rfl)
-
-theorem IterM.count_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
-    [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m]
-    {it : IterM (α := α) m β} :
-    it.count = ForIn.forIn it (.up 0) (fun _ acc => return .yield (.up (acc.down + 1))) :=
-  (rfl)
-
-theorem IterM.count_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
-    [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
-    {it : IterM (α := α) m β} :
-    it.count = (do
-      match (← it.step).inflate.val with
-      | .yield it' _ => return .up ((← it'.count).down + 1)
-      | .skip it' => return .up (← it'.count).down
-      | .done => return .up 0) := by
-  simp only [count_eq_fold]
-  have (acc : Nat) (it' : IterM (α := α) m β) :
-      it'.fold (init := ULift.up acc) (fun acc _ => .up (acc.down + 1)) =
-        (ULift.up <| ·.down + acc) <$>
-          it'.fold (init := ULift.up 0) (fun acc _ => .up (acc.down + 1)) := by
-    rw [← fold_hom]
-    · simp only [Nat.zero_add]; rfl
-    · simp only [ULift.up.injEq]; omega
-  rw [fold_eq_match_step]
-  apply bind_congr; intro step
-  cases step.inflate using PlausibleIterStep.casesOn
-  · simp only [Nat.zero_add, bind_pure_comp]
-    rw [this 1]
-  · simp
-  · simp
-
-@[simp]
-theorem IterM.up_size_toArray_eq_count {α β : Type w} [Iterator α m β] [Finite α m]
-    [Monad m] [LawfulMonad m]
-    [IteratorCollect α m m] [LawfulIteratorCollect α m m]
-    [IteratorLoop α m m] [LawfulIteratorLoop α m m]
-    {it : IterM (α := α) m β} :
-    (.up <| ·.size) <$> it.toArray = it.count := by
-  rw [toArray_eq_fold, count_eq_fold, ← fold_hom]
-  · simp only [List.size_toArray, List.length_nil]; rfl
-  · simp
-
-@[simp]
-theorem IterM.up_length_toList_eq_count {α β : Type w} [Iterator α m β] [Finite α m]
-    [Monad m] [LawfulMonad m]
-    [IteratorCollect α m m] [LawfulIteratorCollect α m m]
-    [IteratorLoop α m m] [LawfulIteratorLoop α m m]
-    {it : IterM (α := α) m β} :
-    (.up <| ·.length) <$> it.toList = it.count := by
-  rw [toList_eq_fold, count_eq_fold, ← fold_hom]
-  · simp only [List.length_nil]; rfl
-  · simp
-
-@[simp]
-theorem IterM.up_length_toListRev_eq_count {α β : Type w} [Iterator α m β] [Finite α m]
-    [Monad m] [LawfulMonad m]
-    [IteratorCollect α m m] [LawfulIteratorCollect α m m]
-    [IteratorLoop α m m] [LawfulIteratorLoop α m m]
-    {it : IterM (α := α) m β} :
-    (.up <| ·.length) <$> it.toListRev = it.count := by
-  simp only [toListRev_eq, Functor.map_map, List.length_reverse, up_length_toList_eq_count]
-
 theorem IterM.anyM_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
     [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
     {it : IterM (α := α) m β} {p : β → m (ULift Bool)} :

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

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

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

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

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

@@ -1,71 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Paul Reichert
--/
-module
-
-prelude
-public import Init.Data.Iterators.Lemmas.Consumers.Monadic
-public import Init.Data.Iterators.Producers.Monadic.List
-
-@[expose] public section
-
-/-!
-# Lemmas about list iterators
-
-This module provides lemmas about the interactions of `List.iterM` with `IterM.step` and various
-collectors.
--/
-
-namespace Std.Iterators
-open Std.Internal
-
-variable {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] {β : Type w}
-
-@[simp]
-theorem _root_.List.step_iterM_nil :
-    (([] : List β).iterM m).step = pure (.deflate ⟨.done, rfl⟩) := by
-  simp only [IterM.step, Iterator.step]; rfl
-
-@[simp]
-theorem _root_.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
-
-theorem _root_.List.step_iterM {l : List β} :
-    (l.iterM m).step = match l with
-      | [] => pure (.deflate ⟨.done, rfl⟩)
-      | x :: xs => pure (.deflate ⟨.yield (xs.iterM m) x, rfl⟩) := by
-  cases l <;> simp [List.step_iterM_cons, List.step_iterM_nil]
-
-theorem ListIterator.toArrayMapped_iterM [Monad n] [LawfulMonad n]
-    {β : Type w} {γ : Type w} {lift : ⦃δ : Type w⦄ → m δ → n δ}
-    [LawfulMonadLiftFunction lift] {f : β → n γ} {l : List β} :
-    IteratorCollect.toArrayMapped lift f (l.iterM m) (m := m) = List.toArray <$> l.mapM f := by
-  rw [LawfulIteratorCollect.toArrayMapped_eq]
-  induction l with
-  | nil =>
-    rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step]
-    simp [List.step_iterM_nil, LawfulMonadLiftFunction.lift_pure]
-  | cons x xs ih =>
-    rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step]
-    simp [List.step_iterM_cons, List.mapM_cons, pure_bind, ih, LawfulMonadLiftFunction.lift_pure]
-
-@[simp]
-theorem _root_.List.toArray_iterM [LawfulMonad m] {l : List β} :
-    (l.iterM m).toArray = pure l.toArray := by
-  simp only [IterM.toArray, ListIterator.toArrayMapped_iterM]
-  rw [List.mapM_pure, map_pure, List.map_id']
-
-@[simp]
-theorem _root_.List.toList_iterM [LawfulMonad m] {l : List β} :
-    (l.iterM m).toList = pure l := by
-  rw [← IterM.toList_toArray, List.toArray_iterM, map_pure, List.toList_toArray]
-
-@[simp]
-theorem _root_.List.toListRev_iterM [LawfulMonad m] {l : List β} :
-    (l.iterM m).toListRev = pure l.reverse := by
-  simp [IterM.toListRev_eq, List.toList_iterM]
-
-end Std.Iterators

src/Init/Data/Iterators/Producers.lean

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

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

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

src/Init/Data/Iterators/ToIterator.lean

@@ -19,45 +19,104 @@ open Std.Iterators
 
 namespace Std.Iterators
 
-/-- This typeclass provides an iterator for elements of type `γ`. -/
-class ToIterator (γ : Type u) (m : Type w → Type w') (α β : outParam (Type w)) where
-  iterMInternal (x : γ) : IterM (α := α) m β
+/--
+This typeclass provides an iterator for the given element `x : γ`. Usually, instances are provided
+for all elements of a type `γ`.
+-/
+class ToIterator {γ : Type u} (x : γ) (m : Type w → Type w') (β : outParam (Type w)) where
+  State : Type w
+  iterMInternal : IterM (α := State) m β
 
 /-- Converts `x` into a monadic iterator. -/
 @[always_inline, inline, expose]
-def ToIterator.iterM (x : γ) [ToIterator γ m α β] : IterM (α := α) m β :=
+def ToIterator.iterM (x : γ) [ToIterator x m β] : IterM (α := ToIterator.State x m) m β :=
   ToIterator.iterMInternal (x := x)
 
 /-- Converts `x` into a pure iterator. -/
 @[always_inline, inline, expose]
-def ToIterator.iter [ToIterator γ Id α β] (x : γ) : Iter (α := α) β :=
+def ToIterator.iter (x : γ) [ToIterator x Id β] : Iter (α := ToIterator.State x Id) β :=
   ToIterator.iterM x |>.toIter
 
 /-- Creates a monadic `ToIterator` instance. -/
 @[always_inline, inline, expose]
-def ToIterator.ofM (α : Type w)
-    (iterM : γ → IterM (α := α) m β) :
-    ToIterator γ m α β where
-  iterMInternal x := iterM x
+def ToIterator.ofM {x : γ} (State : Type w)
+    (iterM : IterM (α := State) m β) :
+    ToIterator x m β where
+  State := State
+  iterMInternal := iterM
 
 /-- Creates a pure `ToIterator` instance. -/
 @[always_inline, inline, expose]
-def ToIterator.of (α : Type w)
-    (iter : γ → Iter (α := α) β) :
-    ToIterator γ Id α β where
-  iterMInternal x := iter x |>.toIterM
+def ToIterator.of {x : γ} (State : Type w)
+    (iter : Iter (α := State) β) :
+    ToIterator x Id β where
+  State := State
+  iterMInternal := iter.toIterM
 
-/-- Replaces `ToIterator.iterM` with its definition. -/
-theorem ToIterator.iterM_eq {γ : Type u} {α β : Type v}
-    {it : γ → IterM (α := α) Id β} {x} :
-    letI : ToIterator γ Id α β := .ofM α it
-    ToIterator.iterM x = it x :=
+theorem ToIterator.iterM_eq {γ : Type u} {x : γ} {State : Type v} {β : Type v} {it} :
+    letI : ToIterator x Id β := .ofM State it
+    ToIterator.iterM x = it :=
   rfl
 
-/-- Replaces `ToIterator.iter` with its definition. -/
-theorem ToIterator.iter_eq {γ : Type u} {x : γ} {α β : Type v} {it} :
-    letI : ToIterator γ Id α β := .ofM α it
-    ToIterator.iter x = (it x).toIter :=
+theorem ToIterator.iter_eq {γ : Type u} {x : γ} {State : Type v} {β : Type v} {it} :
+    letI : ToIterator x Id β := .ofM State it
+    ToIterator.iter x = it.toIter :=
   rfl
 
+/-!
+## Instance forwarding
+
+If the type defined as `ToIterator.State` implements an iterator typeclass, then this typeclass
+should also be available when the type is syntactically visible as `ToIteratorState`. The following
+instances are responsible for this forwarding.
+-/
+
+instance {x : γ} {State : Type w} {iter}
+    [Iterator State m β] :
+    letI i : ToIterator x m β := .ofM State iter
+    Iterator (α := i.State) m β :=
+  inferInstanceAs <| Iterator State m β
+
+instance {x : γ} {State : Type w} {iter}
+    [Iterator (α := State) m β] [Finite State m] :
+    letI i : ToIterator x m β := .ofM State iter
+    Finite (α := i.State) m :=
+  inferInstanceAs <| Finite (α := State) m
+
+instance {x : γ} {State : Type w} {iter}
+    [Iterator (α := State) m β] [IteratorCollect State m n] :
+    letI i : ToIterator x m β := .ofM State iter
+    IteratorCollect (α := i.State) m n :=
+  inferInstanceAs <| IteratorCollect (α := State) m n
+
+instance {x : γ} {State : Type w} {iter}
+    [Iterator (α := State) m β] [IteratorCollectPartial State m n] :
+    letI i : ToIterator x m β := .ofM State iter
+    IteratorCollectPartial (α := i.State) m n :=
+  inferInstanceAs <| IteratorCollectPartial (α := State) m n
+
+instance {x : γ} {State : Type w} {iter}
+    [Iterator (α := State) m β] [IteratorLoop State m n] :
+    letI i : ToIterator x m β := .ofM State iter
+    IteratorLoop (α := i.State) m n :=
+  inferInstanceAs <| IteratorLoop (α := State) m n
+
+instance {x : γ} {State : Type w} {iter}
+    [Iterator (α := State) m β] [IteratorLoopPartial State m n] :
+    letI i : ToIterator x m β := .ofM State iter
+    IteratorLoopPartial (α := i.State) m n :=
+  inferInstanceAs <| IteratorLoopPartial (α := State) m n
+
+instance {x : γ} {State : Type w} {iter}
+    [Iterator (α := State) m β] [IteratorSize State m] :
+    letI i : ToIterator x m β := .ofM State iter
+    IteratorSize (α := i.State) m :=
+  inferInstanceAs <| IteratorSize (α := State) m
+
+instance {x : γ} {State : Type w} {iter}
+    [Iterator (α := State) m β] [IteratorSizePartial State m] :
+    letI i : ToIterator x m β := .ofM State iter
+    IteratorSizePartial (α := i.State) m :=
+  inferInstanceAs <| IteratorSizePartial (α := State) m
+
 end Std.Iterators

src/Init/Data/List/Basic.lean

@@ -622,17 +622,11 @@ instance : Std.LawfulIdentity (α := List α) (· ++ ·) [] where
   | nil => simp
   | cons _ as ih => simp [ih, Nat.succ_add]
 
-@[simp] theorem append_assoc (as bs cs : List α) : (as ++ bs) ++ cs = as ++ (bs ++ cs) := by
+@[simp, grind _=_] theorem append_assoc (as bs cs : List α) : (as ++ bs) ++ cs = as ++ (bs ++ cs) := by
   induction as with
   | nil => rfl
   | cons a as ih => simp [ih]
 
-grind_pattern append_assoc => (as ++ bs) ++ cs where
-  as =/= []; bs =/= []; cs =/= []
-
-grind_pattern append_assoc => as ++ (bs ++ cs) where
-  as =/= []; bs =/= []; cs =/= []
-
 instance : Std.Associative (α := List α) (· ++ ·) := ⟨append_assoc⟩
 
 -- Arguments are explicit as there is often ambiguity inferring the arguments.
@@ -2092,18 +2086,6 @@ def min? [Min α] : List α → Option α
   | []    => none
   | a::as => some <| as.foldl min a
 
-/-! ### min -/
-
-/--
-Returns the smallest element of a non-empty list.
-
-Examples:
-* `[4].min (by decide) = 4`
-* `[1, 4, 2, 10, 6].min (by decide) = 1`
--/
-protected def min [Min α] : (l : List α) → (h : l ≠ []) → α
-  | a::as, _ => as.foldl min a
-
 /-! ### max? -/
 
 /--
@@ -2118,18 +2100,6 @@ def max? [Max α] : List α → Option α
   | []    => none
   | a::as => some <| as.foldl max a
 
-/-! ### max -/
-
-/--
-Returns the largest element of a non-empty list.
-
-Examples:
-* `[4].max (by decide) = 4`
-* `[1, 4, 2, 10, 6].max (by decide) = 10`
--/
-protected def max [Max α] : (l : List α) → (h : l ≠ []) → α
-  | a::as, _ => as.foldl max a
-
 /-! ## Other list operations
 
 The functions are currently mostly used in meta code,

src/Init/Data/List/BasicAux.lean

@@ -272,8 +272,8 @@ theorem sizeOf_get [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.g
     apply Nat.lt_trans ih
     simp +arith
 
-theorem lex_trichotomous [DecidableEq α] {r : α → α → Prop} [DecidableRel r]
-    (trichotomous : ∀ x y : α, ¬ r x y → ¬ r y x → x = y)
+theorem not_lex_antisymm [DecidableEq α] {r : α → α → Prop} [DecidableRel r]
+    (antisymm : ∀ x y : α, ¬ r x y → ¬ r y x → x = y)
     {as bs : List α} (h₁ : ¬ Lex r bs as) (h₂ : ¬ Lex r as bs) : as = bs :=
   match as, bs with
   | [],    []    => rfl
@@ -286,26 +286,20 @@ theorem lex_trichotomous [DecidableEq α] {r : α → α → Prop} [DecidableRel
       · subst eq
         have h₁ : ¬ Lex r bs as := fun h => h₁ (List.Lex.cons h)
         have h₂ : ¬ Lex r as bs := fun h => h₂ (List.Lex.cons h)
-        simp [lex_trichotomous trichotomous h₁ h₂]
+        simp [not_lex_antisymm antisymm h₁ h₂]
       · exfalso
         by_cases hba : r b a
         · exact h₁ (Lex.rel hba)
-        · exact eq (trichotomous _ _ hab hba)
-
-@[deprecated lex_trichotomous (since := "2025-10-27")]
-theorem not_lex_antisymm [DecidableEq α] {r : α → α → Prop} [DecidableRel r]
-    (antisymm : ∀ x y : α, ¬ r x y → ¬ r y x → x = y)
-    {as bs : List α} (h₁ : ¬ Lex r bs as) (h₂ : ¬ Lex r as bs) : as = bs :=
-  lex_trichotomous antisymm h₁ h₂
+        · exact eq (antisymm _ _ hab hba)
 
 protected theorem le_antisymm [LT α]
-    [i : Std.Trichotomous (· < · : α → α → Prop)]
+    [i : Std.Antisymm (¬ · < · : α → α → Prop)]
     {as bs : List α} (h₁ : as ≤ bs) (h₂ : bs ≤ as) : as = bs :=
   open Classical in
-  lex_trichotomous i.trichotomous h₁ h₂
+  not_lex_antisymm i.antisymm h₁ h₂
 
 instance [LT α]
-    [s : Std.Trichotomous (· < · : α → α → Prop)] :
+    [s : Std.Antisymm (¬ · < · : α → α → Prop)] :
     Std.Antisymm (· ≤ · : List α → List α → Prop) where
   antisymm _ _ h₁ h₂ := List.le_antisymm h₁ h₂
 

src/Init/Data/List/Control.lean

@@ -471,7 +471,7 @@ theorem findM?_eq_findSomeM? [Monad m] [LawfulMonad m] {p : α → m Bool} {as :
         loop as' b this
   loop as init ⟨[], rfl⟩
 
-instance [Monad m] : ForIn' m (List α) α inferInstance where
+instance : ForIn' m (List α) α inferInstance where
   forIn' := List.forIn'
 
 -- No separate `ForIn` instance is required because it can be derived from `ForIn'`.
@@ -485,7 +485,7 @@ instance [Monad m] : ForIn' m (List α) α inferInstance where
 @[simp, grind =] theorem forIn_nil [Monad m] {f : α → β → m (ForInStep β)} {b : β} : forIn [] b f = pure b :=
   rfl
 
-instance [Monad m] : ForM m (List α) α where
+instance : ForM m (List α) α where
   forM := List.forM
 
 -- We simplify `List.forM` to `forM`.

src/Init/Data/List/Erase.lean

@@ -291,11 +291,9 @@ theorem eraseP_comm {l : List α} (h : ∀ a ∈ l, ¬ p a ∨ ¬ q a) :
       · simp [h₁, h₂]
       · simp [h₁, h₂, ih (fun b m => h b (mem_cons_of_mem _ m))]
 
-@[grind ←]
 theorem head_eraseP_mem {xs : List α} {p : α → Bool} (h) : (xs.eraseP p).head h ∈ xs :=
   eraseP_sublist.head_mem h
 
-@[grind ←]
 theorem getLast_eraseP_mem {xs : List α} {p : α → Bool} (h) : (xs.eraseP p).getLast h ∈ xs :=
   eraseP_sublist.getLast_mem h
 

src/Init/Data/List/FinRange.lean

@@ -60,10 +60,6 @@ theorem finRange_reverse {n} : (finRange n).reverse = (finRange n).map Fin.rev :
     congr 2; funext
     simp [Fin.rev_succ]
 
-@[simp, grind ←]
-theorem mem_finRange {n} (x : Fin n) : x ∈ finRange n := by
-  simp [finRange]
-
 end List
 
 namespace Fin

src/Init/Data/List/Find.lean

@@ -659,18 +659,6 @@ theorem findIdx_eq {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs.length
   simp at h3
   simp_all [not_of_lt_findIdx h3]
 
-@[simp]
-theorem lt_findIdx_iff (xs : List α) (p : α → Bool) (i : Nat) :
-    i < xs.findIdx p ↔ ∃ h : i < xs.length, ∀ j, (hj : j ≤ i) → p xs[j] = false :=
-  ⟨fun h => ⟨by have := findIdx_le_length (xs := xs) (p := p); omega,
-    fun j hj => by apply not_of_lt_findIdx; omega⟩,
-    fun ⟨h, w⟩ => by apply lt_findIdx_of_not h; simpa using w⟩
-
-@[simp, grind =]
-theorem findIdx_map (xs : List α) (f : α → β) (p : β → Bool) :
-    (xs.map f).findIdx p = xs.findIdx (p ∘ f) := by
-  induction xs with simp_all [findIdx_cons]
-
 @[grind =]
 theorem findIdx_append {p : α → Bool} {l₁ l₂ : List α} :
     (l₁ ++ l₂).findIdx p =

src/Init/Data/List/Impl.lean

@@ -38,7 +38,7 @@ The following operations are still missing `@[csimp]` replacements:
 The following operations are not recursive to begin with
 (or are defined in terms of recursive primitives):
 `isEmpty`, `isSuffixOf`, `isSuffixOf?`, `rotateLeft`, `rotateRight`, `insert`, `zip`, `enum`,
-`min?`, `max?`, `min`, `max` and `removeAll`.
+`min?`, `max?`, and `removeAll`.
 
 The following operations were already given `@[csimp]` replacements in `Init/Data/List/Basic.lean`:
 `length`, `map`, `filter`, `replicate`, `leftPad`, `unzip`, `range'`, `iota`, `intersperse`.

src/Init/Data/List/Lemmas.lean

@@ -13,9 +13,6 @@ import all Init.Data.List.BasicAux
 public import Init.Data.List.Control
 import all Init.Data.List.Control
 public import Init.BinderPredicates
-import Init.Grind.Annotated
-
-grind_annotated "2025-01-24"
 
 public section
 
@@ -63,7 +60,7 @@ See also
 * `Init.Data.List.Erase` for lemmas about `List.eraseP` and `List.erase`.
 * `Init.Data.List.Find` for lemmas about `List.find?`, `List.findSome?`, `List.findIdx`,
   `List.findIdx?`, and `List.indexOf`
-* `Init.Data.List.MinMax` for lemmas about `List.min?`, `List.min`, `List.max?` and `List.max`.
+* `Init.Data.List.MinMax` for lemmas about `List.min?` and `List.max?`.
 * `Init.Data.List.Pairwise` for lemmas about `List.Pairwise` and `List.Nodup`.
 * `Init.Data.List.Sublist` for lemmas about `List.Subset`, `List.Sublist`, `List.IsPrefix`,
   `List.IsSuffix`, and `List.IsInfix`.
@@ -254,10 +251,6 @@ theorem getElem_eq_getElem?_get {l : List α} {i : Nat} (h : i < l.length) :
     l[i] = l[i]?.get (by simp [h]) := by
   simp
 
-theorem getElem_eq_getD {l : List α} {i : Nat} {h : i < l.length} (fallback : α) :
-    l[i] = l.getD i fallback := by
-  rw [getElem_eq_getElem?_get, List.getD, Option.get_eq_getD]
-
 theorem getD_getElem? {l : List α} {i : Nat} {d : α} :
     l[i]?.getD d = if p : i < l.length then l[i]'p else d := by
   if h : i < l.length then
@@ -305,12 +298,6 @@ theorem ext_getElem {l₁ l₂ : List α} (hl : length l₁ = length l₂)
       have h₁ := Nat.le_of_not_lt h₁
       rw [getElem?_eq_none h₁, getElem?_eq_none]; rwa [← hl]
 
-theorem ext_getElem_iff {l₁ l₂ : List α} :
-    l₁ = l₂ ↔ l₁.length = l₂.length ∧ ∀ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length), l₁[i]'h₁ = l₂[i]'h₂ := by
-  constructor
-  · simp +contextual
-  · exact fun h => ext_getElem h.1 h.2
-
 @[simp] theorem getElem_concat_length {l : List α} {a : α} {i : Nat} (h : i = l.length) (w) :
     (l ++ [a])[i]'w = a := by
   subst h; simp
@@ -1230,13 +1217,9 @@ theorem tailD_map {f : α → β} {l l' : List α} :
 theorem getLastD_map {f : α → β} {l : List α} {a : α} : (map f l).getLastD (f a) = f (l.getLastD a) := by
   simp
 
-@[simp] theorem map_map {g : β → γ} {f : α → β} {l : List α} :
+@[simp, grind _=_] theorem map_map {g : β → γ} {f : α → β} {l : List α} :
     map g (map f l) = map (g ∘ f) l := by induction l <;> simp_all
 
-grind_pattern map_map => map g (map f l) where
-  g =/= List.reverse
-  f =/= List.reverse
-
 /-! ### filter -/
 
 @[simp] theorem filter_cons_of_pos {p : α → Bool} {a : α} {l} (pa : p a) :
@@ -1445,16 +1428,13 @@ theorem filterMap_eq_filter {p : α → Bool} :
   | nil => rfl
   | cons a l IH => by_cases pa : p a <;> simp [Option.guard, pa, ← IH]
 
+@[grind =]
 theorem filterMap_filterMap {f : α → Option β} {g : β → Option γ} {l : List α} :
     filterMap g (filterMap f l) = filterMap (fun x => (f x).bind g) l := by
   induction l with
   | nil => rfl
   | cons a l IH => cases h : f a <;> simp [filterMap_cons, *]
 
-grind_pattern filterMap_filterMap => filterMap g (filterMap f l) where
-  f =/= some
-  g =/= some
-
 @[grind =]
 theorem map_filterMap {f : α → Option β} {g : β → γ} {l : List α} :
     map g (filterMap f l) = filterMap (fun x => (f x).map g) l := by
@@ -2476,28 +2456,16 @@ theorem getLast_of_mem_getLast? {l : List α} (hx : x ∈ l.getLast?) :
     simp only [reverse_cons, filterMap_append, filterMap_cons, ih]
     split <;> simp_all
 
-@[simp] theorem reverse_append {as bs : List α} : (as ++ bs).reverse = bs.reverse ++ as.reverse := by
+@[simp, grind _=_] theorem reverse_append {as bs : List α} : (as ++ bs).reverse = bs.reverse ++ as.reverse := by
   induction as <;> simp_all
 
-grind_pattern reverse_append => (as ++ bs).reverse where
-  as =/= []
-  bs =/= []
-grind_pattern reverse_append => bs.reverse ++ as.reverse where
-  as =/= []
-  bs =/= []
-
 @[simp] theorem reverse_eq_append_iff {xs ys zs : List α} :
     xs.reverse = ys ++ zs ↔ xs = zs.reverse ++ ys.reverse := by
   rw [reverse_eq_iff, reverse_append]
 
-theorem reverse_concat {l : List α} {a : α} : (l ++ [a]).reverse = a :: l.reverse := by
+@[grind _=_] theorem reverse_concat {l : List α} {a : α} : (l ++ [a]).reverse = a :: l.reverse := by
   rw [reverse_append]; rfl
 
-grind_pattern reverse_concat => (l ++ [a]).reverse where
-  l =/= []
-grind_pattern reverse_concat => a :: l.reverse where
-  l =/= []
-
 theorem reverse_eq_concat {xs ys : List α} {a : α} :
     xs.reverse = ys ++ [a] ↔ xs = a :: ys.reverse := by
   rw [reverse_eq_iff, reverse_concat]
@@ -2515,15 +2483,9 @@ theorem flatten_reverse {L : List (List α)} :
 @[grind =] theorem reverse_flatMap {β} {l : List α} {f : α → List β} : (l.flatMap f).reverse = l.reverse.flatMap (reverse ∘ f) := by
   induction l <;> simp_all
 
-grind_pattern reverse_flatMap => (l.flatMap f).reverse where
-  f =/= List.reverse ∘ _
-
-theorem flatMap_reverse {β} {l : List α} {f : α → List β} : l.reverse.flatMap f = (l.flatMap (reverse ∘ f)).reverse := by
+@[grind =] theorem flatMap_reverse {β} {l : List α} {f : α → List β} : (l.reverse.flatMap f) = (l.flatMap (reverse ∘ f)).reverse := by
   induction l <;> simp_all
 
-grind_pattern flatMap_reverse => l.reverse.flatMap f where
-  f =/= List.reverse ∘ _
-
 @[simp] theorem reverseAux_eq {as bs : List α} : reverseAux as bs = reverse as ++ bs :=
   reverseAux_eq_append ..
 
@@ -2670,22 +2632,6 @@ theorem foldr_map_hom {g : α → β} {f : α → α → α} {f' : β → β →
 @[simp, grind _=_] theorem foldr_append {f : α → β → β} {b : β} {l l' : List α} :
     (l ++ l').foldr f b = l.foldr f (l'.foldr f b) := by simp [foldr_eq_foldrM, -foldrM_pure]
 
-theorem foldl_flatMap {f : α → List β} {g : γ → β → γ} {l : List α} {init : γ} :
-    (l.flatMap f).foldl g init = l.foldl (fun acc x => (f x).foldl g acc) init := by
-  induction l generalizing init
-  · simp
-  next a l ih =>
-    simp only [flatMap_cons, foldl_cons]
-    rw [foldl_append, ih]
-
-theorem foldr_flatMap {f : α → List β} {g : β → γ → γ} {l : List α} {init : γ} :
-    (l.flatMap f).foldr g init = l.foldr (fun x acc => (f x).foldr g acc) init := by
-  induction l generalizing init
-  · simp
-  next a l ih =>
-    simp only [flatMap_cons, foldr_cons]
-    rw [foldr_append, ih]
-
 @[grind =] theorem foldl_flatten {f : β → α → β} {b : β} {L : List (List α)} :
     (flatten L).foldl f b = L.foldl (fun b l => l.foldl f b) b := by
   induction L generalizing b <;> simp_all

src/Init/Data/List/Lex.lean

@@ -98,7 +98,7 @@ theorem not_cons_lex_cons_iff [DecidableEq α] [DecidableRel r] {a b} {l₁ l₂
 
 theorem cons_le_cons_iff [LT α]
     [i₁ : Std.Asymm (· < · : α → α → Prop)]
-    [i₂ : Std.Trichotomous (· < · : α → α → Prop)]
+    [i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
     {a b} {l₁ l₂ : List α} :
     (a :: l₁) ≤ (b :: l₂) ↔ a < b ∨ a = b ∧ l₁ ≤ l₂ := by
   dsimp only [instLE, instLT, List.le, List.lt]
@@ -110,12 +110,12 @@ theorem cons_le_cons_iff [LT α]
       apply Decidable.byContradiction
       intro h₃
       apply h₂
-      exact i₂.trichotomous _ _ h₁ h₃
+      exact i₂.antisymm _ _ h₁ h₃
     · if h₃ : a < b then
         exact .inl h₃
       else
         right
-        exact ⟨i₂.trichotomous _ _ h₃ h₁, h₂⟩
+        exact ⟨i₂.antisymm _ _ h₃ h₁, h₂⟩
   · rintro (h | ⟨h₁, h₂⟩)
     · left
       exact ⟨i₁.asymm _ _ h, fun w => Irrefl.irrefl _ (w ▸ h)⟩
@@ -124,7 +124,7 @@ theorem cons_le_cons_iff [LT α]
 
 theorem not_lt_of_cons_le_cons [LT α]
     [i₁ : Std.Asymm (· < · : α → α → Prop)]
-    [i₂ : Std.Trichotomous (· < · : α → α → Prop)]
+    [i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
     {a b : α} {l₁ l₂ : List α} (h : a :: l₁ ≤ b :: l₂) : ¬ b < a := by
   rw [cons_le_cons_iff] at h
   rcases h with h | ⟨rfl, h⟩
@@ -138,7 +138,7 @@ theorem left_le_left_of_cons_le_cons [LT α] [LE α] [IsLinearOrder α]
 theorem le_of_cons_le_cons [LT α]
     [i₀ : Std.Irrefl (· < · : α → α → Prop)]
     [i₁ : Std.Asymm (· < · : α → α → Prop)]
-    [i₂ : Std.Trichotomous (· < · : α → α → Prop)]
+    [i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
     {a} {l₁ l₂ : List α} (h : a :: l₁ ≤ a :: l₂) : l₁ ≤ l₂ := by
   rw [cons_le_cons_iff] at h
   rcases h with h | ⟨_, h⟩
@@ -212,7 +212,7 @@ protected theorem lt_of_le_of_lt [LT α] [LE α] [IsLinearOrder α] [LawfulOrder
 @[deprecated List.lt_of_le_of_lt (since := "2025-08-01")]
 protected theorem lt_of_le_of_lt' [LT α]
     [Std.Asymm (· < · : α → α → Prop)]
-    [Std.Trichotomous (· < · : α → α → Prop)]
+    [Std.Antisymm (¬ · < · : α → α → Prop)]
     [Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)]
     {l₁ l₂ l₃ : List α} (h₁ : l₁ ≤ l₂) (h₂ : l₂ < l₃) : l₁ < l₃ :=
   letI : LE α := .ofLT α
@@ -226,7 +226,7 @@ protected theorem le_trans [LT α] [LE α] [IsLinearOrder α] [LawfulOrderLT α]
 @[deprecated List.le_trans (since := "2025-08-01")]
 protected theorem le_trans' [LT α]
     [Std.Asymm (· < · : α → α → Prop)]
-    [Std.Trichotomous (· < · : α → α → Prop)]
+    [Std.Antisymm (¬ · < · : α → α → Prop)]
     [Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)]
     {l₁ l₂ l₃ : List α} (h₁ : l₁ ≤ l₂) (h₂ : l₂ ≤ l₃) : l₁ ≤ l₃ :=
   letI := LE.ofLT α
@@ -298,7 +298,7 @@ protected theorem le_of_lt [LT α]
 
 protected theorem le_iff_lt_or_eq [LT α]
     [Std.Irrefl (· < · : α → α → Prop)]
-    [Std.Trichotomous (· < · : α → α → Prop)]
+    [Std.Antisymm (¬ · < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     {l₁ l₂ : List α} : l₁ ≤ l₂ ↔ l₁ < l₂ ∨ l₁ = l₂ := by
   constructor
@@ -484,7 +484,7 @@ protected theorem lt_iff_exists [LT α] {l₁ l₂ : List α} :
 
 protected theorem le_iff_exists [LT α]
     [Std.Asymm (· < · : α → α → Prop)]
-    [Std.Trichotomous (· < · : α → α → Prop)] {l₁ l₂ : List α} :
+    [Std.Antisymm (¬ · < · : α → α → Prop)] {l₁ l₂ : List α} :
     l₁ ≤ l₂ ↔
       (l₁ = l₂.take l₁.length) ∨
         (∃ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length),
@@ -497,7 +497,7 @@ protected theorem le_iff_exists [LT α]
     conv => lhs; simp +singlePass [exists_comm]
   · simpa using Std.Irrefl.irrefl
   · simpa using Std.Asymm.asymm
-  · simpa using Std.Trichotomous.trichotomous
+  · simpa using Std.Antisymm.antisymm
 
 theorem append_left_lt [LT α] {l₁ l₂ l₃ : List α} (h : l₂ < l₃) :
     l₁ ++ l₂ < l₁ ++ l₃ := by
@@ -507,7 +507,7 @@ theorem append_left_lt [LT α] {l₁ l₂ l₃ : List α} (h : l₂ < l₃) :
 
 theorem append_left_le [LT α]
     [Std.Asymm (· < · : α → α → Prop)]
-    [Std.Trichotomous (· < · : α → α → Prop)]
+    [Std.Antisymm (¬ · < · : α → α → Prop)]
     {l₁ l₂ l₃ : List α} (h : l₂ ≤ l₃) :
     l₁ ++ l₂ ≤ l₁ ++ l₃ := by
   induction l₁ with
@@ -540,9 +540,9 @@ protected theorem map_lt [LT α] [LT β]
 
 protected theorem map_le [LT α] [LT β]
     [Std.Asymm (· < · : α → α → Prop)]
-    [Std.Trichotomous (· < · : α → α → Prop)]
+    [Std.Antisymm (¬ · < · : α → α → Prop)]
     [Std.Asymm (· < · : β → β → Prop)]
-    [Std.Trichotomous (· < · : β → β → Prop)]
+    [Std.Antisymm (¬ · < · : β → β → Prop)]
     {l₁ l₂ : List α} {f : α → β} (w : ∀ x y, x < y → f x < f y) (h : l₁ ≤ l₂) :
     map f l₁ ≤ map f l₂ := by
   rw [List.le_iff_exists] at h ⊢

src/Init/Data/List/MinMax.lean

@@ -46,9 +46,6 @@ theorem isSome_min?_of_mem {l : List α} [Min α] {a : α} (h : a ∈ l) :
     l.min?.isSome := by
   cases l <;> simp_all [min?_cons']
 
-theorem isSome_min?_of_ne_nil [Min α] : {l : List α} → (hl : l ≠ []) → l.min?.isSome
-  | x::xs, h => by simp [min?_cons']
-
 theorem min?_eq_head? {α : Type u} [Min α] {l : List α}
     (h : l.Pairwise (fun a b => min a b = a)) : l.min? = l.head? := by
   cases l with
@@ -158,48 +155,6 @@ theorem foldl_min [Min α] [Std.IdempotentOp (min : α → α → α)] [Std.Asso
     {l : List α} {a : α} : l.foldl (init := a) min = min a (l.min?.getD a) := by
   cases l <;> simp [min?, foldl_assoc, Std.IdempotentOp.idempotent]
 
-/-! ### min -/
-
-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']
-
-theorem min_eq_get_min? [Min α] : (l : List α) → (hl : l ≠ []) →
-    l.min hl = l.min?.get (isSome_min?_of_ne_nil hl)
-  | a::as, _ => by simp [List.min, List.min?_cons']
-
-theorem min_eq_head {α : Type u} [Min α] {l : List α} (hl : l ≠ [])
-    (h : l.Pairwise (fun a b => min a b = a)) : l.min hl = l.head hl := by
-  apply Option.some.inj
-  rw [← min?_eq_some_min, ← head?_eq_some_head]
-  exact min?_eq_head? h
-
-theorem min_mem [Min α] [MinEqOr α] {l : List α} (hl : l ≠ []) : l.min hl ∈ l :=
-  min?_mem (min?_eq_some_min hl)
-
-theorem min_le_of_mem [Min α] [LE α] [Std.IsLinearOrder α] [Std.LawfulOrderMin α]
-    {l : List α} {a : α} (ha : a ∈ l) :
-    l.min (ne_nil_of_mem ha) ≤ a :=
-  (min?_eq_some_iff.mp (min?_eq_some_min (List.ne_nil_of_mem ha))).right a ha
-
-protected theorem le_min_iff [Min α] [LE α] [LawfulOrderInf α]
-    {l : List α} (hl : l ≠ []) : ∀ {x}, x ≤ l.min hl ↔ ∀ b, b ∈ l → x ≤ b :=
-  le_min?_iff (min?_eq_some_min hl)
-
-theorem min_eq_iff [Min α] [LE α] {l : List α} [IsLinearOrder α] [LawfulOrderMin α] (hl : l ≠ []) :
-    l.min hl = a ↔ a ∈ l ∧ ∀ b, b ∈ l → a ≤ b := by
-  simpa [min?_eq_some_min hl] using (min?_eq_some_iff (xs := l))
-
-@[simp] theorem min_replicate [Min α] [MinEqOr α] {n : Nat} {a : α} (h : replicate n a ≠ []) :
-    (replicate n a).min h = a := by
-  have n_pos : 0 < n := Nat.pos_of_ne_zero (fun hn => by simp [hn] at h)
-  simpa [min?_eq_some_min h] using (min?_replicate_of_pos (a := a) n_pos)
-
-theorem foldl_min_eq_min [Min α] [Std.IdempotentOp (min : α → α → α)] [Std.Associative (min : α → α → α)]
-    {l : List α} (hl : l ≠ []) {a : α} :
-    l.foldl min a = min a (l.min hl) := by
-  simpa [min?_eq_some_min hl] using foldl_min (l := l)
-
 /-! ### max? -/
 
 @[simp] theorem max?_nil [Max α] : ([] : List α).max? = none := rfl
@@ -219,9 +174,6 @@ theorem isSome_max?_of_mem {l : List α} [Max α] {a : α} (h : a ∈ l) :
     l.max?.isSome := by
   cases l <;> simp_all [max?_cons']
 
-theorem isSome_max?_of_ne_nil [Max α] : {l : List α} → (hl : l ≠ []) → l.max?.isSome
-  | x::xs, h => by simp [max?_cons']
-
 theorem max?_eq_head? {α : Type u} [Max α] {l : List α}
     (h : l.Pairwise (fun a b => max a b = a)) : l.max? = l.head? := by
   cases l with
@@ -344,46 +296,4 @@ theorem foldl_max [Max α] [Std.IdempotentOp (max : α → α → α)] [Std.Asso
     {l : List α} {a : α} : l.foldl (init := a) max = max a (l.max?.getD a) := by
   cases l <;> simp [max?, foldl_assoc, Std.IdempotentOp.idempotent]
 
-/-! ### max -/
-
-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']
-
-theorem max_eq_get_max? [Max α] : (l : List α) → (hl : l ≠ []) →
-    l.max hl = l.max?.get (isSome_max?_of_ne_nil hl)
-  | a::as, _ => by simp [List.max, List.max?_cons']
-
-theorem max_eq_head {α : Type u} [Max α] {l : List α} (hl : l ≠ [])
-    (h : l.Pairwise (fun a b => max a b = a)) : l.max hl = l.head hl := by
-  apply Option.some.inj
-  rw [← max?_eq_some_max, ← head?_eq_some_head]
-  exact max?_eq_head? h
-
-theorem max_mem [Max α] [MaxEqOr α] {l : List α} (hl : l ≠ []) : l.max hl ∈ l :=
-  max?_mem (max?_eq_some_max hl)
-
-protected theorem max_le_iff [Max α] [LE α] [LawfulOrderSup α]
-    {l : List α} (hl : l ≠ []) : ∀ {x}, l.max hl ≤ x ↔ ∀ b, b ∈ l → b ≤ x :=
-  max?_le_iff (max?_eq_some_max hl)
-
-theorem max_eq_iff [Max α] [LE α] {l : List α} [IsLinearOrder α] [LawfulOrderMax α] (hl : l ≠ []) :
-    l.max hl = a ↔ a ∈ l ∧ ∀ b, b ∈ l → b ≤ a := by
-  simpa [max?_eq_some_max hl] using (max?_eq_some_iff (xs := l))
-
-theorem le_max_of_mem [Max α] [LE α] [Std.IsLinearOrder α] [Std.LawfulOrderMax α]
-    {l : List α} {a : α} (ha : a ∈ l) :
-    a ≤ l.max (List.ne_nil_of_mem ha) :=
-  (max?_eq_some_iff.mp (max?_eq_some_max (List.ne_nil_of_mem ha))).right a ha
-
-@[simp] theorem max_replicate [Max α] [MaxEqOr α] {n : Nat} {a : α} (h : replicate n a ≠ []) :
-    (replicate n a).max h = a := by
-  have n_pos : 0 < n := Nat.pos_of_ne_zero (fun hn => by simp [hn] at h)
-  simpa [max?_eq_some_max h] using (max?_replicate_of_pos (a := a) n_pos)
-
-theorem foldl_max_eq_max [Max α] [Std.IdempotentOp (max : α → α → α)] [Std.Associative (max : α → α → α)]
-    {l : List α} (hl : l ≠ []) {a : α} :
-    l.foldl max a = max a (l.max hl) := by
-  simpa [max?_eq_some_max hl] using foldl_max (l := l)
-
 end List

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

@@ -68,13 +68,10 @@ theorem getElem?_modifyHead {l : List α} {f : α → α} {i} :
 @[simp, grind =] theorem tail_modifyHead {f : α → α} {l : List α} :
     (l.modifyHead f).tail = l.tail := by cases l <;> simp
 
-@[simp] theorem take_modifyHead {f : α → α} {l : List α} {i} :
+@[simp, grind =] theorem take_modifyHead {f : α → α} {l : List α} {i} :
     (l.modifyHead f).take i = (l.take i).modifyHead f := by
   cases l <;> cases i <;> simp
 
-grind_pattern take_modifyHead => (l.modifyHead f).take i where
-  i =/= 0
-
 @[simp] theorem drop_modifyHead_of_pos {f : α → α} {l : List α} {i} (h : 0 < i) :
     (l.modifyHead f).drop i = l.drop i := by
   cases l <;> cases i <;> simp_all
@@ -106,9 +103,7 @@ theorem eraseIdx_eq_modifyTailIdx : ∀ i (l : List α), eraseIdx l i = l.modify
   | _+1, [] => rfl
   | _+1, _ :: _ => congrArg (cons _) (eraseIdx_eq_modifyTailIdx _ _)
 
--- This is not suitable as a `@[grind =]` lemma:
--- as soon as it is instantiated the hypothesis `H` causes an infinite chain of instantiations.
-@[simp] theorem length_modifyTailIdx (f : List α → List α) (H : ∀ l, (f l).length = l.length) :
+@[simp, grind =] theorem length_modifyTailIdx (f : List α → List α) (H : ∀ l, (f l).length = l.length) :
     ∀ (l : List α) i, (l.modifyTailIdx i f).length = l.length
   | _, 0 => H _
   | [], _+1 => rfl
@@ -218,6 +213,7 @@ theorem modify_eq_self {f : α → α} {i} {l : List α} (h : l.length ≤ i) :
     intro h
     omega
 
+@[grind =]
 theorem modify_modify_eq (f g : α → α) (i) (l : List α) :
     (l.modify i f).modify i g = l.modify i (g ∘ f) := by
   apply ext_getElem
@@ -226,9 +222,6 @@ theorem modify_modify_eq (f g : α → α) (i) (l : List α) :
     simp only [getElem_modify, Function.comp_apply]
     split <;> simp
 
-grind_pattern modify_modify_eq => (l.modify i f).modify i g where
-  l =/= []
-
 theorem modify_modify_ne (f g : α → α) {i j} (l : List α) (h : i ≠ j) :
     (l.modify i f).modify j g = (l.modify j g).modify i f := by
   apply ext_getElem

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

@@ -374,22 +374,6 @@ theorem drop_take : ∀ {i j : Nat} {l : List α}, drop i (take j l) = take (j -
   rw [drop_take]
   simp
 
-@[simp]
-theorem drop_eq_drop_iff :
-    ∀ {l : List α} {i j : Nat}, l.drop i = l.drop j ↔ min i l.length = min j l.length
-  | [], i, j => by simp
-  | _ :: xs, 0, 0 => by simp
-  | x :: xs, i + 1, 0 => by
-    rw [List.ext_getElem_iff]
-    simp [succ_min_succ, show ¬ xs.length - i = xs.length + 1 by omega]
-  | x :: xs, 0, j + 1 => by
-    rw [List.ext_getElem_iff]
-    simp [succ_min_succ, show ¬ xs.length + 1 = xs.length - j by omega]
-  | x :: xs, i + 1, j + 1 => by simp [succ_min_succ, drop_eq_drop_iff]
-
-theorem drop_eq_drop_min {l : List α} {i : Nat} : l.drop i = l.drop (min i l.length) := by
-  simp
-
 theorem take_reverse {α} {xs : List α} {i : Nat} :
     xs.reverse.take i = (xs.drop (xs.length - i)).reverse := by
   by_cases h : i ≤ xs.length

src/Init/Data/List/Sublist.lean

@@ -98,18 +98,14 @@ theorem eq_nil_of_subset_nil {l : List α} : l ⊆ [] → l = [] := subset_nil.m
 theorem map_subset {l₁ l₂ : List α} (f : α → β) (h : l₁ ⊆ l₂) : map f l₁ ⊆ map f l₂ :=
   fun x => by simp only [mem_map]; exact .imp fun a => .imp_left (@h _)
 
-grind_pattern map_subset => l₁ ⊆ l₂, map f l₁ where
-  l₂ =/= List.map _ _
-grind_pattern map_subset => l₁ ⊆ l₂, map f l₂ where
-  l₁ =/= List.map _ _
+grind_pattern map_subset => l₁ ⊆ l₂, map f l₁
+grind_pattern map_subset => l₁ ⊆ l₂, map f l₂
 
 theorem filter_subset {l₁ l₂ : List α} (p : α → Bool) (H : l₁ ⊆ l₂) : filter p l₁ ⊆ filter p l₂ :=
   fun x => by simp_all [mem_filter, subset_def.1 H]
 
-grind_pattern filter_subset => l₁ ⊆ l₂, filter p l₁ where
-  l₂ =/= List.filter _ _
-grind_pattern filter_subset => l₁ ⊆ l₂, filter p l₂ where
-  l₁ =/= List.filter _ _
+grind_pattern filter_subset => l₁ ⊆ l₂, filter p l₁
+grind_pattern filter_subset => l₁ ⊆ l₂, filter p l₂
 
 theorem filterMap_subset {l₁ l₂ : List α} (f : α → Option β) (H : l₁ ⊆ l₂) :
     filterMap f l₁ ⊆ filterMap f l₂ := by
@@ -118,10 +114,8 @@ theorem filterMap_subset {l₁ l₂ : List α} (f : α → Option β) (H : l₁
   rintro ⟨a, h, w⟩
   exact ⟨a, H h, w⟩
 
-grind_pattern filterMap_subset => l₁ ⊆ l₂, filterMap f l₁ where
-  l₂ =/= List.filterMap _ _
-grind_pattern filterMap_subset => l₁ ⊆ l₂, filterMap f l₂ where
-  l₁ =/= List.filterMap _ _
+grind_pattern filterMap_subset => l₁ ⊆ l₂, filterMap f l₁
+grind_pattern filterMap_subset => l₁ ⊆ l₂, filterMap f l₂
 
 theorem subset_append_left (l₁ l₂ : List α) : l₁ ⊆ l₁ ++ l₂ := fun _ => mem_append_left _
 
@@ -212,11 +206,13 @@ theorem Sublist.head_mem (s : ys <+ xs) (h) : ys.head h ∈ xs :=
   s.mem (List.head_mem h)
 
 grind_pattern Sublist.head_mem => ys <+ xs, ys.head h
+grind_pattern Sublist.head_mem => ys.head h ∈ xs -- This is somewhat aggressive, as it initiates sublist based reasoning.
 
 theorem Sublist.getLast_mem (s : ys <+ xs) (h) : ys.getLast h ∈ xs :=
   s.mem (List.getLast_mem h)
 
 grind_pattern Sublist.getLast_mem => ys <+ xs, ys.getLast h
+grind_pattern Sublist.getLast_mem => ys.getLast h ∈ xs -- This is somewhat aggressive, as it initiates sublist based reasoning.
 
 instance : Trans (@Sublist α) Subset Subset :=
   ⟨fun h₁ h₂ => trans h₁.subset h₂⟩
@@ -286,28 +282,20 @@ protected theorem Sublist.map (f : α → β) {l₁ l₂} (s : l₁ <+ l₂) : m
 grind_pattern Sublist.map => l₁ <+ l₂, map f l₁
 grind_pattern Sublist.map => l₁ <+ l₂, map f l₂
 
+@[grind ←]
 protected theorem Sublist.filterMap (f : α → Option β) (s : l₁ <+ l₂) :
     filterMap f l₁ <+ filterMap f l₂ := by
   induction s <;> simp [filterMap_cons] <;> split <;> simp [*, cons]
 
-grind_pattern Sublist.filterMap => filterMap f l₁ <+ filterMap f l₂ where
-  l₁ =/= List.filterMap _ _
-  l₂ =/= List.filterMap _ _
-grind_pattern Sublist.filterMap => l₁ <+ l₂, filterMap f l₁ where
-  l₂ =/= List.filterMap _ _
-grind_pattern Sublist.filterMap => l₁ <+ l₂, filterMap f l₂ where
-  l₁ =/= List.filterMap _ _
+grind_pattern Sublist.filterMap => l₁ <+ l₂, filterMap f l₁
+grind_pattern Sublist.filterMap => l₁ <+ l₂, filterMap f l₂
 
+@[grind ←]
 protected theorem Sublist.filter (p : α → Bool) {l₁ l₂} (s : l₁ <+ l₂) : filter p l₁ <+ filter p l₂ := by
   rw [← filterMap_eq_filter]; apply s.filterMap
 
-grind_pattern Sublist.filter => filter p l₁ <+ filter p l₂ where
-  l₁ =/= List.filter _ _
-  l₂ =/= List.filter _ _
-grind_pattern Sublist.filter => l₁ <+ l₂, l₁.filter p where
-  l₂ =/= List.filter _ _
-grind_pattern Sublist.filter => l₁ <+ l₂, l₂.filter p where
-  l₁ =/= List.filter _ _
+grind_pattern Sublist.filter => l₁ <+ l₂, l₁.filter p
+grind_pattern Sublist.filter => l₁ <+ l₂, l₂.filter p
 
 theorem head_filter_mem (xs : List α) (p : α → Bool) (h) : (xs.filter p).head h ∈ xs :=
   filter_sublist.head_mem h

src/Init/Data/Nat/Basic.lean

@@ -473,13 +473,8 @@ protected theorem eq_iff_le_and_ge : ∀{a b : Nat}, a = b ↔ a ≤ b ∧ b ≤
 instance : Std.Antisymm ( . ≤ . : Nat → Nat → Prop) where
   antisymm _ _ h₁ h₂ := Nat.le_antisymm h₁ h₂
 
-instance : Std.Trichotomous (. < . : Nat → Nat → Prop) where
-  trichotomous _ _ h₁ h₂ := Nat.le_antisymm (Nat.ge_of_not_lt h₂) (Nat.ge_of_not_lt h₁)
-
-set_option linter.missingDocs false in
-@[deprecated Nat.instTrichotomousLt (since := "2025-10-27")]
-def Nat.instAntisymmNotLt : Std.Antisymm (¬ . < . : Nat → Nat → Prop) where
-  antisymm := Nat.instTrichotomousLt.trichotomous
+instance : Std.Antisymm (¬ . < . : Nat → Nat → Prop) where
+  antisymm _ _ h₁ h₂ := Nat.le_antisymm (Nat.ge_of_not_lt h₂) (Nat.ge_of_not_lt h₁)
 
 protected theorem add_le_add_left {n m : Nat} (h : n ≤ m) (k : Nat) : k + n ≤ k + m :=
   match le.dest h with
@@ -822,8 +817,6 @@ protected theorem two_pow_pos (w : Nat) : 0 < 2^w := Nat.pow_pos (by decide)
 instance {n m : Nat} [NeZero n] : NeZero (n^m) :=
   ⟨Nat.ne_zero_iff_zero_lt.mpr (Nat.pow_pos (pos_of_neZero _))⟩
 
-instance {n : Nat} : NeZero (n^0) := ⟨Nat.one_ne_zero⟩
-
 protected theorem mul_pow (a b n : Nat) : (a * b) ^ n = a ^ n * b ^ n := by
   induction n with
   | zero => simp [Nat.pow_zero]

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

@@ -139,12 +139,4 @@ Returns `true` if the `(n+1)`th least significant bit is `1`, or `false` if it i
   -- `1 &&& n` is faster than `n &&& 1` for big `n`.
   1 &&& (m >>> n) != 0
 
-/--
-Asserts that the `(n+1)`th least significant bit of `m` is not set.
-
-(This definition is used by Lean internally for compact bitmaps.)
--/
-@[expose, reducible] protected def hasNotBit (m n : Nat) : Prop :=
-  Nat.land 1 (Nat.shiftRight m n) ≠ 1
-
 end Nat

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

@@ -485,16 +485,11 @@ protected theorem and_comm (x y : Nat) : x &&& y = y &&& x := by
    apply Nat.eq_of_testBit_eq
    simp [Bool.and_comm]
 
+@[grind _=_]
 protected theorem and_assoc (x y z : Nat) : (x &&& y) &&& z = x &&& (y &&& z) := by
    apply Nat.eq_of_testBit_eq
    simp [Bool.and_assoc]
 
-grind_pattern Nat.and_assoc => (x &&& y) &&& z where
-  x =/= 0; y =/= 0; z =/= 0
-
-grind_pattern Nat.and_assoc => x &&& (y &&& z) where
-  x =/= 0; y =/= 0; z =/= 0
-
 instance : Std.Associative (α := Nat) (· &&& ·) where
   assoc := Nat.and_assoc
 

src/Init/Data/Nat/Lemmas.lean

@@ -1719,16 +1719,11 @@ theorem shiftRight_succ_inside : ∀m n, m >>> (n+1) = (m/2) >>> n
   | 0 => by simp
   | n + 1 => by simp [zero_shiftRight n, shiftRight_succ]
 
+@[grind _=_]
 theorem shiftLeft_add (m n : Nat) : ∀ k, m <<< (n + k) = (m <<< n) <<< k
   | 0 => rfl
   | k + 1 => by simp [← Nat.add_assoc, shiftLeft_add _ _ k, shiftLeft_succ]
 
-grind_pattern shiftLeft_add => m <<< (n + k) where
-  m =/= 0
-
-grind_pattern shiftLeft_add => (m <<< n) <<< k where
-  m =/= 0
-
 @[simp] theorem shiftLeft_shiftRight (x n : Nat) : x <<< n >>> n = x := by
   rw [Nat.shiftLeft_eq, Nat.shiftRight_eq_div_pow, Nat.mul_div_cancel _ (Nat.two_pow_pos _)]
 

src/Init/Data/Option/Basic.lean

@@ -15,40 +15,7 @@ public section
 
 namespace Option
 
-instance instDecidableEq {α} [inst : DecidableEq α] : DecidableEq (Option α) := fun a b =>
-  /-
-  Structured for compatibility with the decidable-equality-with-none instances.
-  -/
-  match a with
-  | none => match b with
-    | none => .isTrue rfl
-    | some _ => .isFalse Option.noConfusion
-  | some a => match b with
-    | none => .isFalse Option.noConfusion
-    | some b => match inst a b with
-      | .isTrue h => .isTrue (h ▸ rfl)
-      | .isFalse n => .isFalse (Option.noConfusion · n)
-
-/--
-Equality with `none` is decidable even if the wrapped type does not have decidable equality.
--/
-instance decidableEqNone (o : Option α) : Decidable (o = none) :=
-  /- We use a `match` instead of transferring from `isNone_iff_eq_none` for
-    compatibility with the `DecidableEq` instance. -/
-  match o with
-  | none => .isTrue rfl
-  | some _ => .isFalse Option.noConfusion
-
-/--
-Equality with `none` is decidable even if the wrapped type does not have decidable equality.
--/
-instance decidableNoneEq (o : Option α) : Decidable (none = o) :=
-  /- We use a `match` instead of transferring from `isNone_iff_eq_none` for
-    compatibility with the `DecidableEq` instance. -/
-  match o with
-  | none => .isTrue rfl
-  | some _ => .isFalse Option.noConfusion
-
+deriving instance DecidableEq for Option
 deriving instance BEq for Option
 
 @[simp, grind =] theorem getD_none : getD none a = a := rfl

src/Init/Data/Option/Instances.lean

@@ -35,6 +35,17 @@ instance [DecidableEq α] (j : α) (o : Option α) : Decidable (j ∈ o) :=
 
 theorem some_inj {a b : α} : some a = some b ↔ a = b := by simp; rfl
 
+/--
+Equality with `none` is decidable even if the wrapped type does not have decidable equality.
+
+This is not an instance because it is not definitionally equal to the standard instance of
+`DecidableEq (Option α)`, which can cause problems. It can be locally bound if needed.
+
+Try to use the Boolean comparisons `Option.isNone` or `Option.isSome` instead.
+-/
+@[inline] def decidableEqNone {o : Option α} : Decidable (o = none) :=
+  decidable_of_decidable_of_iff isNone_iff_eq_none
+
 instance decidableForallMem {p : α → Prop} [DecidablePred p] :
     ∀ o : Option α, Decidable (∀ a, a ∈ o → p a)
   | none => isTrue nofun
@@ -168,10 +179,10 @@ Examples:
   | none  , _ => pure ⟨⟩
   | some a, f => f a
 
-instance [Monad m] : ForM m (Option α) α :=
+instance : ForM m (Option α) α :=
   ⟨Option.forM⟩
 
-instance [Monad m] : ForIn' m (Option α) α inferInstance where
+instance : ForIn' m (Option α) α inferInstance where
   forIn' x init f := do
     match x with
     | none => return init

src/Init/Data/Option/Lemmas.lean

@@ -212,13 +212,10 @@ theorem bind_comm {f : α → β → Option γ} (a : Option α) (b : Option β)
     (a.bind fun x => b.bind (f x)) = b.bind fun y => a.bind fun x => f x y := by
   cases a <;> cases b <;> rfl
 
+@[grind =]
 theorem bind_assoc (x : Option α) (f : α → Option β) (g : β → Option γ) :
     (x.bind f).bind g = x.bind fun y => (f y).bind g := by cases x <;> rfl
 
-grind_pattern bind_assoc => (x.bind f).bind g where
-  f =/= some
-  g =/= some
-
 theorem bind_congr {α β} {o : Option α} {f g : α → Option β} :
     (h : ∀ a, o = some a → f a = g a) → o.bind f = o.bind g := by
   cases o <;> simp

src/Init/Data/Ord/Basic.lean

@@ -631,7 +631,7 @@ instance [Ord α] : DecidableRel (@LT.lt α ltOfOrd) := fun a b =>
   decidable_of_bool (compare a b).isLT Ordering.isLT_iff_eq_lt
 
 /--
-Constructs an `LE` instance from an `Ord` instance that asserts that the result of `compare`
+Constructs an `LT` instance from an `Ord` instance that asserts that the result of `compare`
 satisfies `Ordering.isLE`.
 -/
 @[expose] def leOfOrd [Ord α] : LE α where

src/Init/Data/Order/Factories.lean

@@ -234,13 +234,13 @@ If an `LT α` instance is asymmetric and its negation is transitive and antisymm
 public theorem IsLinearOrder.of_lt {α : Type u} [LT α]
     (lt_asymm : Asymm (α := α) (· < ·) := by exact inferInstance)
     (not_lt_trans : Trans (α := α) (¬ · < ·) (¬ · < ·) (¬ · < ·) := by exact inferInstance)
-    (lt_trichotomous : Trichotomous (α := α) (· < ·) := by exact inferInstance) :
+    (not_lt_antisymm : Antisymm (α := α) (¬ · < ·) := by exact inferInstance) :
     haveI := LE.ofLT α
     IsLinearOrder α :=
   letI := LE.ofLT α
   haveI : IsLinearPreorder α := .of_lt
   { le_antisymm := by
-      simpa [LE.ofLT] using fun a b hab hba => lt_trichotomous.trichotomous a b hba hab }
+      simpa [LE.ofLT] using fun a b hab hba => not_lt_antisymm.antisymm a b hba hab }
 
 /--
 This lemma characterizes in terms of `LT α` when a `Min α` instance

src/Init/Data/Order/Lemmas.lean

@@ -22,53 +22,17 @@ section AxiomaticInstances
 public instance (r : α → α → Prop) [Asymm r] : Irrefl r where
   irrefl a h := Asymm.asymm a a h h
 
-public instance (r : α → α → Prop) [Total r] : Refl r where
+public instance {r : α → α → Prop} [Total r] : Refl r where
   refl a := by simpa using Total.total a a
 
-public instance (r : α → α → Prop) [Asymm r] : Antisymm r where
-  antisymm a b h h' := (Asymm.asymm a b h h').elim
-
-public instance (r : α → α → Prop) [Total r] : Trichotomous r where
-  trichotomous a b h h' := by simpa [h, h'] using Total.total (r := r) a b
-
-public theorem Trichotomous.rel_or_eq_or_rel_swap {r : α → α → Prop} [i : Trichotomous r] {a b} :
-    r a b ∨ a = b ∨ r b a := match Classical.em (r a b) with
-  | .inl hab => .inl hab | .inr hab => match Classical.em (r b a) with
-    | .inl hba => .inr <| .inr hba
-    | .inr hba => .inr <| .inl <| i.trichotomous _ _ hab hba
-
-public theorem trichotomous_of_rel_or_eq_or_rel_swap {r : α → α → Prop}
-    (h : ∀ {a b}, r a b ∨ a = b ∨ r b a) : Trichotomous r where
-  trichotomous _ _ hab hba := (h.resolve_left hab).resolve_right hba
-
-public instance Antisymm.trichotomous_of_antisymm_not {r : α → α → Prop} [i : Antisymm (¬ r · ·)] :
-    Trichotomous r where trichotomous := i.antisymm
-
-public theorem Trichotomous.antisymm_not {r : α → α → Prop} [i : Trichotomous r] :
-    Antisymm (¬ r · ·) where antisymm := i.trichotomous
-
-public theorem Total.rel_of_not_rel_swap {r : α → α → Prop} [Total r] {a b} (h : ¬ r a b) : r b a :=
-  (Total.total a b).elim (fun h' => (h h').elim) (·)
-
-public theorem total_of_not_rel_swap_imp_rel {r : α → α → Prop} (h : ∀ {a b}, ¬ r a b → r b a) :
-    Total r where
-  total a b := match Classical.em (r a b) with | .inl hab => .inl hab | .inr hab => .inr (h hab)
-
-public theorem total_of_refl_of_trichotomous (r : α → α → Prop) [Refl r] [Trichotomous r] :
-    Total r where
-  total a b := (Trichotomous.rel_or_eq_or_rel_swap (a := a) (b := b) (r := r)).elim Or.inl <|
-    fun h => h.elim (fun h => h ▸ Or.inl (Refl.refl _)) Or.inr
-
-public theorem asymm_of_irrefl_of_antisymm (r : α → α → Prop) [Irrefl r] [Antisymm r] :
-    Asymm r where asymm a b h h' := Irrefl.irrefl _ (Antisymm.antisymm a b h h' ▸ h)
-
 public instance Total.asymm_of_total_not {r : α → α → Prop} [i : Total (¬ r · ·)] : Asymm r where
-  asymm a b h := (i.total a b).resolve_left (· h)
+  asymm a b h := by cases i.total a b <;> trivial
 
 public theorem Asymm.total_not {r : α → α → Prop} [i : Asymm r] : Total (¬ r · ·) where
-  total a b := match Classical.em (r b a) with
-    | .inl hba => .inl <| i.asymm b a hba
-    | .inr hba => .inr hba
+  total a b := by
+    apply Classical.byCases (p := r a b) <;> intro hab
+    · exact Or.inr <| i.asymm a b hab
+    · exact Or.inl hab
 
 public instance {α : Type u} [LE α] [IsPartialOrder α] :
     Antisymm (α := α) (· ≤ ·) where
@@ -110,7 +74,9 @@ public theorem le_total {α : Type u} [LE α] [Std.Total (α := α) (· ≤ ·)]
   Std.Total.total a b
 
 public theorem le_of_not_ge {α : Type u} [LE α] [Std.Total (α := α) (· ≤ ·)] {a b : α} :
-    ¬ b ≤ a → a ≤ b := Total.rel_of_not_rel_swap
+    ¬ b ≤ a → a ≤ b := by
+  intro h
+  simpa [h] using Std.Total.total a b (r := (· ≤ ·))
 
 end LE
 
@@ -124,30 +90,18 @@ public theorem lt_iff_le_and_not_ge {α : Type u} [LT α] [LE α] [LawfulOrderLT
     a < b ↔ a ≤ b ∧ ¬ b ≤ a :=
   LawfulOrderLT.lt_iff a b
 
-public theorem not_lt_iff_not_le_or_ge {α : Type u} [LT α] [LE α] [LawfulOrderLT α]
-    {a b : α} : ¬ a < b ↔ ¬ a ≤ b ∨ b ≤ a := by
-  simp only [lt_iff_le_and_not_ge, Classical.not_and_iff_not_or_not, Classical.not_not]
-
-public theorem not_le_of_gt {α : Type u} [LT α] [LE α] [LawfulOrderLT α] {a b : α}
-    (h : a < b) : ¬ b ≤ a := (lt_iff_le_and_not_ge.1 h).2
-
-public theorem not_lt_of_ge {α : Type u} [LT α] [LE α] [LawfulOrderLT α] {a b : α}
-    (h : a ≤ b) : ¬ b < a := imp_not_comm.1 not_le_of_gt h
-
-public instance {α : Type u} {_ : LE α} [LT α] [LawfulOrderLT α]
-    [Trichotomous (α := α) (· < ·)] : Antisymm (α := α) (· ≤ ·) where
-  antisymm _ _ hab hba := Trichotomous.trichotomous _ _ (not_lt_of_ge hba) (not_lt_of_ge hab)
+public theorem not_lt {α : Type u} [LT α] [LE α] [Std.Total (α := α) (· ≤ ·)] [LawfulOrderLT α]
+    {a b : α} : ¬ a < b ↔ b ≤ a := by
+  simp [lt_iff_le_and_not_ge, Classical.not_not, Std.Total.total]
 
 public theorem not_gt_of_lt {α : Type u} [LT α] [i : Std.Asymm (α := α) (· < ·)] {a b : α}
     (h : a < b) : ¬ b < a :=
   i.asymm a b h
 
 public theorem le_of_lt {α : Type u} [LT α] [LE α] [LawfulOrderLT α] {a b : α} (h : a < b) :
-    a ≤ b := (lt_iff_le_and_not_ge.1 h).1
-
-public instance {α : Type u} {_ : LT α} [LE α] [LawfulOrderLT α]
-    [Antisymm (α := α) (· ≤ ·)] : Antisymm (α := α) (· < ·) where
-  antisymm _ _ hab hba := Antisymm.antisymm _ _ (le_of_lt hab) (le_of_lt hba)
+    a ≤ b := by
+  simp only [LawfulOrderLT.lt_iff] at h
+  exact h.1
 
 public instance {α : Type u} [LT α] [LE α] [LawfulOrderLT α] :
     Std.Asymm (α := α) (· < ·) where
@@ -156,9 +110,8 @@ public instance {α : Type u} [LT α] [LE α] [LawfulOrderLT α] :
     intro h h'
     exact h.2.elim h'.1
 
-@[deprecated instIrreflOfAsymm (since := "2025-10-24")]
-public theorem instIrreflLtOfIsPreorderOfLawfulOrderLT {α : Type u} [LT α] [LE α]
-    [LawfulOrderLT α] : Std.Irrefl (α := α) (· < ·) := inferInstance
+public instance {α : Type u} [LT α] [LE α] [LawfulOrderLT α] :
+    Std.Irrefl (α := α) (· < ·) := inferInstance
 
 public instance {α : Type u} [LT α] [LE α] [Trans (α := α) (· ≤ ·) (· ≤ ·) (· ≤ ·) ]
     [LawfulOrderLT α] : Trans (α := α) (· < ·) (· < ·) (· < ·) where
@@ -169,19 +122,10 @@ public instance {α : Type u} [LT α] [LE α] [Trans (α := α) (· ≤ ·) (·
     · intro hca
       exact hab.2.elim (le_trans hbc.1 hca)
 
-public theorem not_lt {α : Type u} [LT α] [LE α] [Std.Total (α := α) (· ≤ ·)] [LawfulOrderLT α]
-    {a b : α} : ¬ a < b ↔ b ≤ a := by
-  simp [not_lt_iff_not_le_or_ge]
-  exact le_of_not_ge
-
-public theorem not_le {α : Type u} [LT α] [LE α] [Std.Total (α := α) (· ≤ ·)] [LawfulOrderLT α]
-    {a b : α} : ¬ a ≤ b ↔ b < a := by
-  simp [lt_iff_le_and_not_ge]
-  exact le_of_not_ge
-
 public instance {α : Type u} {_ : LT α} [LE α] [LawfulOrderLT α]
-    [Total (α := α) (· ≤ ·)] [Antisymm (α := α) (· ≤ ·)] : Trichotomous (α := α) (· < ·) where
-  trichotomous a b hab hba := by
+    [Total (α := α) (· ≤ ·)] [Antisymm (α := α) (· ≤ ·)] :
+    Antisymm (α := α) (¬ · < ·) where
+  antisymm a b hab hba := by
     simp only [not_lt] at hab hba
     exact Antisymm.antisymm (r := (· ≤ ·)) a b hba hab
 
@@ -192,9 +136,9 @@ public instance {α : Type u} {_ : LT α} [LE α] [LawfulOrderLT α]
     simp only [not_lt] at hab hbc ⊢
     exact le_trans hbc hab
 
-@[deprecated Asymm.total_not (since := "2025-10-24")]
-public theorem instTotalNotLtOfLawfulOrderLTOfLe {α : Type u} {_ : LT α} [LE α] [LawfulOrderLT α]
-    : Total (α := α) (¬ · < ·) := Asymm.total_not
+public instance {α : Type u} {_ : LT α} [LE α] [LawfulOrderLT α] [Total (α := α) (· ≤ ·)] :
+    Total (α := α) (¬ · < ·) where
+  total a b := by simp [not_lt, Std.Total.total]
 
 public theorem lt_of_le_of_lt {α : Type u} [LE α] [LT α]
     [Trans (α := α) (· ≤ ·) (· ≤ ·) (· ≤ ·)] [LawfulOrderLT α] {a b c : α} (hab : a ≤ b)

src/Init/Data/Range/Basic.lean

@@ -43,7 +43,7 @@ universe u v
   have := range.step_pos
   loop init range.start (by simp)
 
-instance [Monad m] : ForIn' m Range Nat inferInstance where
+instance : ForIn' m Range Nat inferInstance where
   forIn' := Range.forIn'
 
 -- No separate `ForIn` instance is required because it can be derived from `ForIn'`.
@@ -59,7 +59,7 @@ instance [Monad m] : ForIn' m Range Nat inferInstance where
   have := range.step_pos
   loop range.start
 
-instance [Monad m] : ForM m Range Nat where
+instance : ForM m Range Nat where
   forM := Range.forM
 
 syntax:max "[" withoutPosition(":" term) "]" : term

src/Init/Data/Range/Polymorphic.lean

@@ -18,7 +18,6 @@ public import Init.Data.Range.Polymorphic.UInt
 public import Init.Data.Range.Polymorphic.SInt
 
 public import Init.Data.Range.Polymorphic.NatLemmas
-public import Init.Data.Range.Polymorphic.IntLemmas
 public import Init.Data.Range.Polymorphic.GetElemTactic
 
 public section

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

@@ -1,39 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Alexander Bentkamp
--/
-module
-
-prelude
-public import Init.Data.Range.Polymorphic.Int
-public import Init.Data.Range.Polymorphic.Lemmas
-
-public section
-
-namespace Std.PRange.Int
-
-@[simp]
-theorem size_rco {a b : Int} :
-    (a...b).size = (b - a).toNat := by
-  simp only [Rco.size, Rxo.HasSize.size, Rxc.HasSize.size]
-  omega
-
-@[simp]
-theorem size_rcc {a b : Int} :
-    (a...=b).size = (b + 1 - a).toNat := by
-  simp [Rcc.size, Rxc.HasSize.size]
-
-@[simp]
-theorem size_roc {a b : Int} :
-    (a<...=b).size = (b - a).toNat := by
-  simp only [Roc.size, Rxc.HasSize.size]
-  omega
-
-@[simp]
-theorem size_roo {a b : Int} :
-    (a<...b).size = (b - a - 1).toNat := by
-  simp [Roo.size, Rxo.HasSize.size, Rxc.HasSize.size]
-  omega
-
-end Std.PRange.Int

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

@@ -19,6 +19,45 @@ open Std.Iterators
 namespace Std
 open PRange
 
+namespace Rxc
+
+/--
+Iterators for right-closed ranges implementing {name}`Rxc.HasSize` support {name}`Iter.size`.
+-/
+instance [Rxc.HasSize α] [UpwardEnumerable α] [LE α] [DecidableLE α] :
+    IteratorSize (Rxc.Iterator α) Id where
+  size it := match it.internalState.next with
+    | none => pure (.up 0)
+    | some next => pure (.up (Rxc.HasSize.size next it.internalState.upperBound))
+
+end Rxc
+
+namespace Rxo
+
+/--
+Iterators for ranges implementing {name}`Rxo.HasSize` support {name}`Iter.size`.
+-/
+instance [Rxo.HasSize α] [UpwardEnumerable α] [LT α] [DecidableLT α] :
+    IteratorSize (Rxo.Iterator α) Id where
+  size it := match it.internalState.next with
+    | none => pure (.up 0)
+    | some next => pure (.up (Rxo.HasSize.size next it.internalState.upperBound))
+
+end Rxo
+
+namespace Rxi
+
+/--
+Iterators for ranges implementing {name}`Rxi.HasSize` support {name}`Iter.size`.
+-/
+instance [Rxi.HasSize α] [UpwardEnumerable α] :
+    IteratorSize (Rxi.Iterator α) Id where
+  size it := match it.internalState.next with
+    | none => pure (.up 0)
+    | some next => pure (.up (Rxi.HasSize.size next))
+
+end Rxi
+
 namespace Rcc
 
 variable {α : Type u}
@@ -53,8 +92,8 @@ def toArray [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerab
 Returns the number of elements contained in the given closed range.
 -/
 @[always_inline, inline]
-def size [Rxc.HasSize α] (r : Rcc α) : Nat :=
-  Rxc.HasSize.size r.lower r.upper
+def size [Rxc.HasSize α] [UpwardEnumerable α] [LE α] [DecidableLE α] (r : Rcc α) : Nat :=
+  Internal.iter r |>.size
 
 section Iterator
 
@@ -139,8 +178,8 @@ def toArray [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerab
 Returns the number of elements contained in the given left-closed right-open range.
 -/
 @[always_inline, inline]
-def size [Rxo.HasSize α] (r : Rco α) : Nat :=
-  Rxo.HasSize.size r.lower r.upper
+def size [Rxo.HasSize α] [UpwardEnumerable α] [LT α] [DecidableLT α] (r : Rco α) : Nat :=
+  Internal.iter r |>.size
 
 section Iterator
 
@@ -226,8 +265,8 @@ def toArray [UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinit
 Returns the number of elements contained in the given left-closed right-unbounded range.
 -/
 @[always_inline, inline]
-def size [Rxi.HasSize α] (r : Rci α) : Nat :=
-  Rxi.HasSize.size r.lower
+def size [Rxi.HasSize α] [UpwardEnumerable α] (r : Rci α) : Nat :=
+  Internal.iter r |>.size
 
 section Iterator
 
@@ -310,10 +349,8 @@ def toArray [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerab
 Returns the number of elements contained in the given left-open right-closed range.
 -/
 @[always_inline, inline]
-def size [Rxc.HasSize α] [UpwardEnumerable α] (r : Roc α) : Nat :=
-  match UpwardEnumerable.succ? r.lower with
-  | none => 0
-  | some lower => Rxc.HasSize.size lower r.upper
+def size [Rxc.HasSize α] [UpwardEnumerable α] [LE α] [DecidableLE α] (r : Roc α) : Nat :=
+  Internal.iter r |>.size
 
 section Iterator
 
@@ -391,10 +428,8 @@ def toArray [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerab
 Returns the number of elements contained in the given open range.
 -/
 @[always_inline, inline]
-def size [Rxo.HasSize α] [UpwardEnumerable α] (r : Roo α) : Nat :=
-  match UpwardEnumerable.succ? r.lower with
-  | none => 0
-  | some lower => Rxo.HasSize.size lower r.upper
+def size [Rxo.HasSize α] [UpwardEnumerable α] [LT α] [DecidableLT α] (r : Roo α) : Nat :=
+  Internal.iter r |>.size
 
 section Iterator
 
@@ -472,9 +507,7 @@ Returns the number of elements contained in the given left-open right-unbounded
 -/
 @[always_inline, inline]
 def size [Rxi.HasSize α] [UpwardEnumerable α] (r : Roi α) : Nat :=
-  match UpwardEnumerable.succ? r.lower with
-  | none => 0
-  | some lower => Rxi.HasSize.size lower
+  Internal.iter r |>.size
 
 section Iterator
 
@@ -547,10 +580,8 @@ def toArray [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUp
 Returns the number of elements contained in the given closed range.
 -/
 @[always_inline, inline]
-def size [Rxc.HasSize α] [Least? α] (r : Ric α) : Nat :=
-  match Least?.least? (α := α) with
-  | none => 0
-  | some least => Rxc.HasSize.size least r.upper
+def size [Rxc.HasSize α] [UpwardEnumerable α] [Least? α] [LE α] [DecidableLE α] (r : Ric α) : Nat :=
+  Internal.iter r |>.size
 
 section Iterator
 
@@ -622,10 +653,8 @@ def toArray [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUp
 Returns the number of elements contained in the given closed range.
 -/
 @[always_inline, inline]
-def size [Rxo.HasSize α] [Least? α] (r : Rio α) : Nat :=
-  match Least?.least? (α := α) with
-  | none => 0
-  | some least => Rxo.HasSize.size least r.upper
+def size [Rxo.HasSize α] [UpwardEnumerable α] [Least? α] [LT α] [DecidableLT α] (r : Rio α) : Nat :=
+  Internal.iter r |>.size
 
 section Iterator
 
@@ -698,10 +727,8 @@ def toArray {α} [UpwardEnumerable α] [Least? α] (r : Rii α)
 Returns the number of elements contained in the full range.
 -/
 @[always_inline, inline]
-def size (_ : Rii α) [Least? α] [Rxi.HasSize α] : Nat :=
-  match Least?.least? (α := α) with
-  | none => 0
-  | some least => Rxi.HasSize.size least
+def size [UpwardEnumerable α] [Least? α] (r : Rii α) [IteratorSize (Rxi.Iterator α) Id] : Nat :=
+  Internal.iter r |>.size
 
 section Iterator