fix: use GitHub App token for Batteries/Mathlib checkout in PR release

The MATHLIB4_BOT PAT has been deprecated as part of the migration to GitHub Apps.
This PR updates the workflow to use the mathlib-nightly-testing GitHub App instead.

**Required setup:** Add the following secrets to leanprover/lean4:
- MATHLIB_NIGHTLY_TESTING_APP_ID
- MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY

These are the same values used in leanprover-community/mathlib4 and batteries.

.claude/CLAUDE.md

@@ -1,29 +1,6 @@
 To build Lean you should use `make -j -C build/release`.
 
-## Running Tests
-
-See `doc/dev/testing.md` for full documentation. Quick reference:
-
-```bash
-# Full test suite (use after builds to verify correctness)
-make -j -C build/release test ARGS="-j$(nproc)"
-
-# Specific test by name (supports regex via ctest -R)
-make -j -C build/release test ARGS='-R grind_ematch --output-on-failure'
-
-# Rerun only previously failed tests
-make -j -C build/release test ARGS='--rerun-failed --output-on-failure'
-
-# Single test from tests/lean/run/ (quick check during development)
-cd tests/lean/run && ./test_single.sh example_test.lean
-
-# ctest directly (from stage1 build dir)
-cd build/release/stage1 && ctest -j$(nproc) --output-on-failure --timeout 300
-```
-
-The full test suite includes `tests/lean/`, `tests/lean/run/`, `tests/lean/interactive/`,
-`tests/compiler/`, `tests/pkg/`, Lake tests, and more. Using `make test` or `ctest` runs
-all of them; `test_single.sh` in `tests/lean/run/` only covers that one directory.
+To run a test you should use `cd tests/lean/run && ./test_single.sh example_test.lean`.
 
 ## New features
 

.github/workflows/ci.yml

@@ -60,23 +60,10 @@ jobs:
           if [[ -n '${{ secrets.PUSH_NIGHTLY_TOKEN }}' ]]; then
             git remote add nightly https://foo:'${{ secrets.PUSH_NIGHTLY_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-nightly.git
             git fetch nightly --tags
-            if [[ '${{ github.event_name }}' == 'workflow_dispatch' ]]; then
-              # Manual re-release: create a revision of the most recent nightly
-              BASE_NIGHTLY=$(git tag -l 'nightly-*' | sort -rV | head -1)
-              # Strip any existing -revK suffix to get the base date tag
-              BASE_NIGHTLY="${BASE_NIGHTLY%%-rev*}"
-              REV=1
-              while git rev-parse "refs/tags/${BASE_NIGHTLY}-rev${REV}" >/dev/null 2>&1; do
-                REV=$((REV + 1))
-              done
-              LEAN_VERSION_STRING="${BASE_NIGHTLY}-rev${REV}"
+            LEAN_VERSION_STRING="nightly-$(date -u +%F)"
+            # do nothing if commit already has a different tag
+            if [[ "$(git name-rev --name-only --tags --no-undefined HEAD 2> /dev/null || echo "$LEAN_VERSION_STRING")" == "$LEAN_VERSION_STRING" ]]; then
               echo "nightly=$LEAN_VERSION_STRING" >> "$GITHUB_OUTPUT"
-            else
-              # Scheduled: do nothing if commit already has a different tag
-              LEAN_VERSION_STRING="nightly-$(date -u +%F)"
-              if [[ "$(git name-rev --name-only --tags --no-undefined HEAD 2> /dev/null || echo "$LEAN_VERSION_STRING")" == "$LEAN_VERSION_STRING" ]]; then
-                echo "nightly=$LEAN_VERSION_STRING" >> "$GITHUB_OUTPUT"
-              fi
             fi
           fi
 
@@ -273,7 +260,7 @@ jobs:
               {
                 "name": "Linux fsanitize",
                 // Always run on large if available, more reliable regarding timeouts
-                "os": large ? "nscloud-ubuntu-22.04-amd64-16x32-with-cache" : "ubuntu-latest",
+                "os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
                 "enabled": level >= 2,
                 // do not fail nightlies on this for now
                 "secondary": level <= 2,
@@ -290,7 +277,7 @@ jobs:
                 // * `grind_guide` always times out.
                 // * `pkg/|lake/` tests sometimes time out (likely even hang), related to Lake CI
                 //   failures?
-                "CTEST_OPTIONS": "-E 'StackOverflow|reverse-ffi|interactive|async_select_channel|9366|run/bv_|grind_guide|grind_bitvec2|grind_constProp|grind_indexmap|grind_list|grind_lint|grind_array_attach|grind_ite_trace|pkg/|lake/'"
+                "CTEST_OPTIONS": "-E 'StackOverflow|reverse-ffi|interactive|async_select_channel|9366|run/bv_|grind_guide|pkg/|lake/'"
               },
               {
                 "name": "macOS",
@@ -488,7 +475,7 @@ jobs:
           git tag "${{ needs.configure.outputs.nightly }}"
           git push nightly "${{ needs.configure.outputs.nightly }}"
           git push -f origin refs/tags/${{ needs.configure.outputs.nightly }}:refs/heads/nightly
-          last_tag="$(git log HEAD^ --simplify-by-decoration --pretty="format:%d" | grep -o "nightly-[^ ,)]*" | head -n 1)"
+          last_tag="$(git log HEAD^ --simplify-by-decoration --pretty="format:%d" | grep -o "nightly-[-0-9]*" | head -n 1)"
           echo -e "*Changes since ${last_tag}:*\n\n" > diff.md
           git show "$last_tag":RELEASES.md > old.md
           #./script/diff_changelogs.py old.md doc/changes.md >> diff.md
@@ -511,18 +498,8 @@ jobs:
           gh workflow -R leanprover/release-index run update-index.yml
         env:
           GITHUB_TOKEN: ${{ secrets.RELEASE_INDEX_TOKEN }}
-      - name: Generate mathlib nightly-testing app token
-        id: mathlib-app-token
-        uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
-        continue-on-error: true
-        with:
-          app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }}
-          private-key: ${{ secrets.MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY }}
-          owner: leanprover-community
-          repositories: mathlib4-nightly-testing
       - name: Update toolchain on mathlib4's nightly-testing branch
-        if: steps.mathlib-app-token.outcome == 'success'
         run: |
-          gh workflow -R leanprover-community/mathlib4-nightly-testing run nightly_bump_and_merge.yml
+          gh workflow -R leanprover-community/mathlib4-nightly-testing run nightly_bump_toolchain.yml
         env:
-          GITHUB_TOKEN: ${{ steps.mathlib-app-token.outputs.token }}
+          GITHUB_TOKEN: ${{ secrets.MATHLIB4_BOT }}

.github/workflows/pr-release.yml

@@ -170,18 +170,6 @@ jobs:
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         uses: dcarbone/install-jq-action@v3.2.0
 
-      # Generate a token for posting comments to Lean PRs about mathlib compatibility.
-      # This app is in the leanprover org and installed on leanprover/lean4.
-      - name: Generate GitHub App token for Lean PR comments
-        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        id: mathlib-comment-token
-        uses: actions/create-github-app-token@3ff1caaa28b64c9cc276ce0a02e2ff584f3900c5 # v2.0.2
-        with:
-          app-id: ${{ secrets.MATHLIB_LEAN_PR_TESTING_APP_ID }}
-          private-key: ${{ secrets.MATHLIB_LEAN_PR_TESTING_PRIVATE_KEY }}
-          owner: leanprover
-          repositories: lean4
-
       # Check that the most recently nightly coincides with 'git merge-base HEAD master'
       - name: Check merge-base and nightly-testing-YYYY-MM-DD for Mathlib/Batteries
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
@@ -216,9 +204,8 @@ jobs:
 
           if [[ -n "$MESSAGE" ]]; then
             # Check if force-mathlib-ci label is present
-            # Use GITHUB_TOKEN for read-only label fetch (MATHLIB4_COMMENT_BOT is only for posting comments)
             LABELS="$(curl --retry 3 --location --silent \
-                          -H "Authorization: token ${{ secrets.GITHUB_TOKEN }}" \
+                          -H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
                           -H "Accept: application/vnd.github.v3+json" \
                           "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/labels" \
                           | jq -r '.[].name')"
@@ -239,10 +226,10 @@ jobs:
 
             # Use GitHub API to check if a comment already exists
             existing_comment="$(curl --retry 3 --location --silent \
-                                    -H "Authorization: token ${{ steps.mathlib-comment-token.outputs.token }}" \
+                                    -H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
                                     -H "Accept: application/vnd.github.v3+json" \
                                     "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments" \
-                                    | jq 'first(.[] | select(.body | test("^- . Mathlib") or startswith("Mathlib CI status")) | select(.user.login == "mathlib-lean-pr-testing[bot]"))')"
+                                    | jq 'first(.[] | select(.body | test("^- . Mathlib") or startswith("Mathlib CI status")) | select(.user.login == "leanprover-community-bot"))')"
             existing_comment_id="$(echo "$existing_comment" | jq -r .id)"
             existing_comment_body="$(echo "$existing_comment" | jq -r .body)"
 
@@ -252,14 +239,14 @@ jobs:
               echo "Posting message to the comments: $MESSAGE"
 
               # Append new result to the existing comment or post a new comment
-              # Use the mathlib-lean-pr-testing app token so Mathlib CI can subsequently edit the comment.
+              # It's essential we use the MATHLIB4_COMMENT_BOT token here, so that Mathlib CI can subsequently edit the comment.
               if [ -z "$existing_comment_id" ]; then
                 INTRO="Mathlib CI status ([docs](https://leanprover-community.github.io/contribute/tags_and_branches.html)):"
                 # Post new comment with a bullet point
                 echo "Posting as new comment at leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
                 curl -L -s \
                   -X POST \
-                  -H "Authorization: token ${{ steps.mathlib-comment-token.outputs.token }}" \
+                  -H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
                   -H "Accept: application/vnd.github.v3+json" \
                   -d "$(jq --null-input --arg intro "$INTRO" --arg val "$MESSAGE" '{"body":($intro + "\n" + $val)}')" \
                   "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
@@ -268,7 +255,7 @@ jobs:
                 echo "Appending to existing comment at leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
                 curl -L -s \
                   -X PATCH \
-                  -H "Authorization: token ${{ steps.mathlib-comment-token.outputs.token }}" \
+                  -H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
                   -H "Accept: application/vnd.github.v3+json" \
                   -d "$(jq --null-input --arg existing "$existing_comment_body" --arg message "$MESSAGE" '{"body":($existing + "\n" + $message)}')" \
                   "https://api.github.com/repos/leanprover/lean4/issues/comments/$existing_comment_id"

doc/dev/bootstrap.md

@@ -6,7 +6,7 @@ building Lean itself - which is needed to again build those parts. This cycle is
 broken by using pre-built C files checked into the repository (which ultimately
 go back to a point where the Lean compiler was not written in Lean) in place of
 these Lean inputs and then compiling everything in multiple stages up to a fixed
-point. The build directory is organized into these stages:
+point. The build directory is organized in these stages:
 
 ```bash
 stage0/
@@ -79,7 +79,7 @@ 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`.
 The same is true for further stages except that a rebuild of them is retriggered on any committed change, not just to a specific directory.
-Thus when debugging e.g. stage 2 failures, you can resume the build from these failures on but you may want to explicitly call `clean-stdlib` to either observe changes from `.olean` files of modules that built successfully or to check that you did not break modules that built successfully at some prior point.
+Thus when debugging e.g. stage 2 failures, you can resume the build from these failures on but may want to explicitly call `clean-stdlib` to either observe changes from `.olean` files of modules that built successfully or to check that you did not break modules that built successfully at some prior point.
 
 If you have write access to the lean4 repository, you can also manually
 trigger that process, for example to be able to use new features in the compiler itself.
@@ -101,7 +101,7 @@ The script `script/rebase-stage0.sh` can be used for that.
 
 The CI should prevent PRs with changes to stage0 (besides `stdlib_flags.h`)
 from entering `master` through the (squashing!) merge queue, and label such PRs
-with the `changes-stage0` label. Such PRs should have a cleaned-up history,
+with the `changes-stage0` label. Such PRs should have a cleaned up history,
 with separate stage0 update commits; then coordinate with the admins to merge
 your PR using rebase merge, bypassing the merge queue.
 

doc/dev/release_checklist.md

@@ -30,7 +30,7 @@ We'll use `v4.6.0` as the intended release version as a running example.
     run `script/release_notes.py --since v4.5.0` on the `releases/v4.6.0` branch,
     and see the section "Writing the release notes" below for more information.
   - Release notes live in https://github.com/leanprover/reference-manual, in e.g. `Manual/Releases/v4.6.0.lean`.
-    It's best if you update these at the same time as you update the `lean-toolchain` for the `reference-manual` repository, see below.
+    It's best if you update these at the same time as a you update the `lean-toolchain` for the `reference-manual` repository, see below.
 - Go to https://github.com/leanprover/lean4/releases and verify that the `v4.6.0` release appears.
   - Verify on Github that "Set as the latest release" is checked.
 - Next, we will move a curated list of downstream repos to the latest stable release.
@@ -54,7 +54,7 @@ We'll use `v4.6.0` as the intended release version as a running example.
     - `verso`:
       - The `subverso` dependency is unusual in that it needs to be compatible with _every_ Lean release simultaneously.
         Usually you don't need to do anything.
-        If you think something is wrong here, please contact David Thrane Christiansen (@david-christiansen)
+        If you think something is wrong here please contact David Thrane Christiansen (@david-christiansen)
       - Warnings during `lake update` and `lake build` are expected.
     - `reference-manual`: the release notes generated by `script/release_notes.py` as described above must be included in
       `Manual/Releases/v4.6.0.lean`, and `import` and `include` statements adding in `Manual/Releases.lean`. 

doc/examples/IJCAR2026/README.md

@@ -1,6 +0,0 @@
-# IJCAR 2026: `grind`, An SMT-Inspired Tactic for Lean 4
-
-Ancillary materials for the paper.
-
-- `examples.lean`: interactive examples from the paper
-- `analyze_grind_loc.py`: script used for the evaluation section, analyzing `grind` adoption and lines-of-code changes in Mathlib

doc/examples/IJCAR2026/analyze_grind_loc.py

@@ -1,401 +0,0 @@
-#!/usr/bin/env python3
-"""
-Analyze grind adoption LoC changes in mathlib.
-
-For each theorem/lemma in master that uses grind, find the most recent
-commit where it didn't use grind, and measure the LoC change.
-
-This script was used in preparing the "Evaluation" section of the grind paper.
-"""
-
-import subprocess
-import re
-import csv
-import sys
-from pathlib import Path
-from dataclasses import dataclass
-from concurrent.futures import ThreadPoolExecutor, as_completed
-from typing import Iterator
-from functools import lru_cache
-
-
-@dataclass
-class GrindUsage:
-    file: str
-    line_no: int
-    decl_name: str
-    decl_type: str  # theorem, lemma, def, example, etc.
-
-
-@dataclass
-class LocChange:
-    file: str
-    decl_name: str
-    decl_type: str
-    old_loc: int
-    new_loc: int
-    loc_saved: int
-    commit_sha: str
-    commit_date: str
-
-
-def run_git(args: list[str], repo: str = ".") -> str:
-    """Run a git command and return stdout."""
-    result = subprocess.run(
-        ["git", "-C", repo] + args,
-        capture_output=True, text=True, check=True
-    )
-    return result.stdout
-
-
-def run_git_safe(args: list[str], repo: str = ".") -> str | None:
-    """Run a git command, return None on failure."""
-    result = subprocess.run(
-        ["git", "-C", repo] + args,
-        capture_output=True, text=True
-    )
-    if result.returncode != 0:
-        return None
-    return result.stdout
-
-
-@lru_cache(maxsize=4096)
-def get_file_at_commit(repo: str, commit: str, file_path: str) -> str | None:
-    """Get file contents at a specific commit (cached)."""
-    return run_git_safe(["show", f"{commit}:{file_path}"], repo)
-
-
-def find_grind_usages(repo: str = ".") -> tuple[list[GrindUsage], int, int]:
-    """Find all declarations using grind in current master.
-    Returns (usages, total_grind_calls, grind_in_decls) where:
-    - total_grind_calls is the count of grind tactic calls (after filtering comments/attrs)
-    - grind_in_decls is the count of those that are inside named declarations
-    """
-    # Use git grep to find lines containing 'grind' (excludes lake packages)
-    result = run_git(["grep", "-n", "grind", "master", "--", "Mathlib/"], repo)
-
-    usages = []
-    seen = set()  # (file, decl_name) to dedupe
-    total_grind_calls = 0
-    grind_in_decls = 0
-
-    for line in result.strip().split('\n'):
-        if not line:
-            continue
-        # Format: master:path/to/file.lean:123:line content
-        match = re.match(r'^master:(.+\.lean):(\d+):(.*)$', line)
-        if not match:
-            continue
-
-        file_path, line_no_str, content = match.groups()
-        line_no = int(line_no_str)
-
-        # Skip comments and attributes (not tactic calls)
-        content_stripped = content.strip()
-        if content_stripped.startswith('--') or content_stripped.startswith('/-'):
-            continue
-        if content_stripped.startswith('attribute'):
-            continue
-        if '@[' in content and 'grind' in content:
-            # Could be an attribute like @[grind =], skip
-            if 'by' not in content and ':=' not in content:
-                continue
-
-        total_grind_calls += 1
-
-        # Find the declaration this grind belongs to
-        decl_name, decl_type = find_decl_at_line(repo, file_path, line_no)
-        if decl_name is None:
-            continue
-
-        grind_in_decls += 1
-
-        key = (file_path, decl_name)
-        if key in seen:
-            continue
-        seen.add(key)
-
-        usages.append(GrindUsage(
-            file=file_path,
-            line_no=line_no,
-            decl_name=decl_name,
-            decl_type=decl_type
-        ))
-
-    return usages, total_grind_calls, grind_in_decls
-
-
-def find_decl_at_line(repo: str, file_path: str, grind_line: int) -> tuple[str | None, str | None]:
-    """
-    Find the declaration name and type that contains the grind at the given line.
-    Search backwards from grind_line to find the most recent declaration.
-    """
-    # Get file content at master
-    content = get_file_at_commit(repo, "master", file_path)
-    if content is None:
-        return None, None
-
-    lines = content.split('\n')
-
-    # Search backwards from grind_line for a declaration
-    # Match declarations with optional leading modifiers and attributes
-    decl_pattern = re.compile(r'^(?:@\[.*?\]\s*)*(?:private\s+|protected\s+|noncomputable\s+|scoped\s+)*(theorem|lemma|def|example|instance|abbrev|structure|class)\s+(\w+)')
-
-    for i in range(grind_line - 1, -1, -1):
-        if i >= len(lines):
-            continue
-        line = lines[i]
-        match = decl_pattern.match(line)
-        if match:
-            return match.group(2), match.group(1)
-
-    return None, None
-
-
-def find_grind_introduction_commit(repo: str, file_path: str, decl_name: str) -> str | None:
-    """
-    Find the commit that introduced grind to this declaration.
-    Returns None if the declaration was born with grind.
-    """
-    # First, find the line range of the declaration in master
-    content = get_file_at_commit(repo, "master", file_path)
-    if content is None:
-        return None
-
-    lines = content.split('\n')
-    decl_start = None
-    decl_end = None
-
-    # Find declaration start
-    decl_pattern = re.compile(rf'^(?:@\[.*?\]\s*)*(?:private\s+|protected\s+|noncomputable\s+|scoped\s+)*(theorem|lemma|def|example|instance|abbrev|structure|class)\s+{re.escape(decl_name)}\b')
-    for i, line in enumerate(lines):
-        if decl_pattern.match(line):
-            decl_start = i
-            break
-
-    if decl_start is None:
-        return None
-
-    # Find declaration end (next top-level declaration or EOF)
-    end_patterns = re.compile(r'^(?:private\s+|protected\s+|noncomputable\s+|scoped\s+)*(theorem|lemma|def|example|instance|abbrev|structure|class|namespace|section|end\s|@\[|#|/-)')
-    for i in range(decl_start + 1, len(lines)):
-        line = lines[i]
-        if line and not line[0].isspace() and end_patterns.match(line):
-            decl_end = i
-            break
-    if decl_end is None:
-        decl_end = len(lines)
-
-    # Find grind line within declaration
-    grind_line = None
-    for i in range(decl_start, decl_end):
-        if 'grind' in lines[i]:
-            grind_line = i + 1  # 1-indexed
-            break
-
-    if grind_line is None:
-        return None
-
-    # Use git blame to find when that grind line was added
-    blame_result = run_git_safe(["blame", "-L", f"{grind_line},{grind_line}", "--porcelain", "master", "--", file_path], repo)
-    if blame_result is None:
-        return None
-
-    # First line of porcelain output is the commit SHA
-    first_line = blame_result.split('\n')[0]
-    commit_sha = first_line.split()[0]
-
-    # Check if this declaration existed before this commit (without grind)
-    parent_sha = run_git_safe(["rev-parse", f"{commit_sha}^"], repo)
-    if parent_sha is None:
-        return None  # Initial commit, born with grind
-    parent_sha = parent_sha.strip()
-
-    # Check if declaration existed in parent
-    parent_content = get_file_at_commit(repo, parent_sha, file_path)
-    if parent_content is None:
-        # File didn't exist in parent - might be new file or renamed
-        return None
-
-    # Check if declaration existed and didn't have grind
-    if decl_name not in parent_content:
-        return None  # Declaration didn't exist - born with grind
-
-    # Check if it already had grind in parent
-    parent_lines = parent_content.split('\n')
-    in_decl = False
-    for line in parent_lines:
-        if decl_pattern.match(line):
-            in_decl = True
-        elif in_decl:
-            if line and not line[0].isspace() and end_patterns.match(line):
-                break
-            if 'grind' in line:
-                # Already had grind in parent — not the introduction commit
-                return None
-
-    return commit_sha
-
-
-def extract_proof_loc(repo: str, file_path: str, decl_name: str, commit: str) -> int | None:
-    """
-    Extract the number of lines in a declaration's proof at a given commit.
-    Returns None if the declaration doesn't exist at that commit.
-    """
-    content = get_file_at_commit(repo, commit, file_path)
-    if content is None:
-        return None
-
-    lines = content.split('\n')
-
-    # Find declaration start
-    decl_pattern = re.compile(rf'^(?:@\[.*?\]\s*)*(?:private\s+|protected\s+|noncomputable\s+|scoped\s+)*(theorem|lemma|def|example|instance|abbrev|structure|class)\s+{re.escape(decl_name)}\b')
-    decl_start = None
-    for i, line in enumerate(lines):
-        if decl_pattern.match(line):
-            decl_start = i
-            break
-
-    if decl_start is None:
-        return None
-
-    # Find declaration end
-    end_patterns = re.compile(r'^(?:private\s+|protected\s+|noncomputable\s+|scoped\s+)*(theorem|lemma|def|example|instance|abbrev|structure|class|namespace|section|end\s|@\[|#|/-)')
-    decl_end = None
-    for i in range(decl_start + 1, len(lines)):
-        line = lines[i]
-        if line and not line[0].isspace() and end_patterns.match(line):
-            decl_end = i
-            break
-    if decl_end is None:
-        decl_end = len(lines)
-
-    # Count non-empty lines in declaration
-    loc = sum(1 for i in range(decl_start, decl_end) if lines[i].strip())
-    return loc
-
-
-def get_commit_date(repo: str, sha: str) -> str:
-    """Get the date of a commit."""
-    result = run_git(["log", "-1", "--format=%ci", sha], repo)
-    return result.strip().split()[0]  # Just the date part
-
-
-def analyze_usage_detailed(repo: str, usage: GrindUsage) -> tuple[LocChange | None, str]:
-    """Analyze a single grind usage, returning (result, skip_reason)."""
-    commit = find_grind_introduction_commit(repo, usage.file, usage.decl_name)
-    if commit is None:
-        return None, "born_with_grind"
-
-    parent = run_git_safe(["rev-parse", f"{commit}^"], repo)
-    if parent is None:
-        return None, "no_parent"
-    parent = parent.strip()
-
-    old_loc = extract_proof_loc(repo, usage.file, usage.decl_name, parent)
-    new_loc = extract_proof_loc(repo, usage.file, usage.decl_name, "master")
-
-    if old_loc is None:
-        return None, "old_loc_failed"
-    if new_loc is None:
-        return None, "new_loc_failed"
-
-    commit_date = get_commit_date(repo, commit)
-
-    return LocChange(
-        file=usage.file,
-        decl_name=usage.decl_name,
-        decl_type=usage.decl_type,
-        old_loc=old_loc,
-        new_loc=new_loc,
-        loc_saved=old_loc - new_loc,
-        commit_sha=commit[:12],
-        commit_date=commit_date
-    ), "success"
-
-
-def main(repo: str = "."):
-    print("Finding grind usages in master...", file=sys.stderr)
-    usages, total_grind_calls, grind_in_decls = find_grind_usages(repo)
-    print(f"Found {len(usages)} declarations using grind ({grind_in_decls}/{total_grind_calls} grind calls)", file=sys.stderr)
-
-    print("Analyzing git history (this may take a while)...", file=sys.stderr)
-    results: list[LocChange] = []
-    skip_reasons: dict[str, int] = {}
-
-    with ThreadPoolExecutor(max_workers=64) as executor:
-        futures = {executor.submit(analyze_usage_detailed, repo, usage): usage for usage in usages}
-
-        for i, future in enumerate(as_completed(futures)):
-            if (i + 1) % 50 == 0:
-                print(f"  Progress: {i + 1}/{len(usages)}", file=sys.stderr, flush=True)
-
-            result, reason = future.result()
-            if result:
-                results.append(result)
-            else:
-                skip_reasons[reason] = skip_reasons.get(reason, 0) + 1
-
-    total_skipped = sum(skip_reasons.values())
-    print(f"\nAnalyzed {len(results)} declarations, skipped {total_skipped}:", file=sys.stderr)
-    for reason, count in sorted(skip_reasons.items(), key=lambda x: -x[1]):
-        print(f"  - {reason}: {count}", file=sys.stderr)
-
-    # Sort by LoC saved (descending)
-    results.sort(key=lambda r: r.loc_saved, reverse=True)
-
-    # Output CSV
-    writer = csv.writer(sys.stdout)
-    writer.writerow(["file", "declaration", "type", "old_loc", "new_loc", "loc_saved", "commit", "date"])
-    for r in results:
-        writer.writerow([r.file, r.decl_name, r.decl_type, r.old_loc, r.new_loc, r.loc_saved, r.commit_sha, r.commit_date])
-
-    # Summary stats to stderr
-    total_old = sum(r.old_loc for r in results) if results else 0
-    total_new = sum(r.new_loc for r in results) if results else 0
-    total_saved = sum(r.loc_saved for r in results) if results else 0
-    avg_saved = total_saved / len(results) if results else 0
-
-    print("\n" + "=" * 60, file=sys.stderr)
-    print("GRIND ADOPTION LOC ANALYSIS", file=sys.stderr)
-    print("=" * 60, file=sys.stderr)
-
-    print("\n## Declaration Counts\n", file=sys.stderr)
-    print(f"  Total grind tactic calls:         {total_grind_calls}", file=sys.stderr)
-    print(f"  In named declarations:            {grind_in_decls} ({total_grind_calls - grind_in_decls} in anonymous/other)", file=sys.stderr)
-    print(f"  Unique declarations:              {len(usages)}", file=sys.stderr)
-    print(f"  Converted to grind:               {len(results)}", file=sys.stderr)
-    print(f"  Born with grind:                  {skip_reasons.get('born_with_grind', 0)}", file=sys.stderr)
-    if skip_reasons.get('old_loc_failed', 0) > 0:
-        print(f"  Could not trace history:          {skip_reasons.get('old_loc_failed', 0)}", file=sys.stderr)
-
-    print("\n## Lines of Code Impact\n", file=sys.stderr)
-    print(f"  Total LoC before grind:           {total_old}", file=sys.stderr)
-    print(f"  Total LoC after grind:            {total_new}", file=sys.stderr)
-    print(f"  Total LoC saved:                  {total_saved}", file=sys.stderr)
-    print(f"  Average LoC saved per theorem:    {avg_saved:.1f}", file=sys.stderr)
-    big_savings = sum(1 for r in results if r.loc_saved >= 10)
-    print(f"  Declarations shrunk by 10+ lines: {big_savings}", file=sys.stderr)
-
-    if results:
-        print("\n## Top 10 Biggest LoC Savings\n", file=sys.stderr)
-        for r in results[:10]:
-            print(f"  {r.loc_saved:+4d} lines: {r.decl_name} ({r.file})", file=sys.stderr)
-
-        # Show any that got bigger (negative savings)
-        got_bigger = [r for r in results if r.loc_saved < 0]
-        if got_bigger:
-            print(f"\n## Declarations That Got Bigger ({len(got_bigger)} total)\n", file=sys.stderr)
-            print("  (showing 5 worst):", file=sys.stderr)
-            for r in got_bigger[-5:]:  # Show worst 5
-                print(f"  {r.loc_saved:+4d} lines: {r.decl_name} ({r.file})", file=sys.stderr)
-
-    print("\n" + "=" * 60, file=sys.stderr)
-
-
-if __name__ == "__main__":
-    import argparse
-    parser = argparse.ArgumentParser(description="Analyze grind LoC savings")
-    parser.add_argument("--repo", "-r", default=".", help="Repository path")
-    args = parser.parse_args()
-    main(args.repo)

doc/examples/IJCAR2026/examples.lean

@@ -1,127 +0,0 @@
-/- Examples from the paper "grind: An SMT-Inspired Tactic for Lean 4" -/
-open Lean Grind
-
-/- Congruence closure. -/
-
-example (f : Nat → Nat) (h : a = b) : f (f b) = f (f a) := by grind
-
-/-
-E-matching.
-
-Any `f` that is the left inverse of `g` would work on this example.
--/
-def f (x : Nat) := x - 1
-def g (x : Nat) := x + 1
-
-@[grind =] theorem fg : f (g x) = x := by simp [f, g]
-example : f a = b → a = g c → b = c := by grind
-
-/-
-Any `R` that is transitive and symmetric would work on this example.
--/
-def R : Nat → Nat → Prop := (· % 7 = · % 7)
-@[grind →] theorem Rtrans : R x y → R y z → R x z := by grind [R]
-@[grind →] theorem Rsymm  : R x y → R y x := by grind [R]
-example : R a b → R c b → R d c → R a d := by grind
-
-/- Big step operational semantics example. -/
-
-abbrev Variable := String
-def State := Variable → Nat
-inductive Stmt : Type where
-  | skip : Stmt
-  | assign : Variable → (State → Nat) → Stmt
-  | seq : Stmt → Stmt → Stmt
-  | ifThenElse : (State → Prop) → Stmt → Stmt → Stmt
-  | whileDo : (State → Prop) → Stmt → Stmt
-infix:60 ";; " => Stmt.seq
-export Stmt (skip assign seq ifThenElse whileDo)
-set_option quotPrecheck false in
-notation s:70 "[" x:70 "↦" n:70 "]" => (fun v ↦ if v = x then n else s v)
-inductive BigStep : Stmt → State → State → Prop where
-  | skip (s : State) : BigStep skip s s
-  | assign (x : Variable) (a : State → Nat) (s : State) : BigStep (assign x a) s (s[x ↦ a s])
-  | seq {S T : Stmt} {s t u : State} (hS : BigStep S s t) (hT : BigStep T t u) :
-    BigStep (S;; T) s u
-  | if_true {B : State → Prop} {s t : State} (hcond : B s) (S T : Stmt) (hbody : BigStep S s t) :
-    BigStep (ifThenElse B S T) s t
-  | if_false {B : State → Prop} {s t : State} (hcond : ¬ B s) (S T : Stmt) (hbody : BigStep T s t) :
-    BigStep (ifThenElse B S T) s t
-  | while_true {B S s t u} (hcond : B s) (hbody : BigStep S s t) (hrest : BigStep (whileDo B S) t u) :
-    BigStep (whileDo B S) s u
-  | while_false {B S s} (hcond : ¬ B s) : BigStep (whileDo B S) s s
-notation:55 "(" S:55 "," s:55 ")" " ==> " t:55 => BigStep S s t
-
-example {B S T s t} (hcond : B s) : (ifThenElse B S T, s) ==> t → (S, s) ==> t := by
-  grind [cases BigStep]
-
-theorem cases_if_of_true {B S T s t} (hcond : B s) : (ifThenElse B S T, s) ==> t → (S, s) ==> t := by
-  grind [cases BigStep]
-
-theorem cases_if_of_false {B S T s t} (hcond : ¬ B s) : (ifThenElse B S T, s) ==> t → (T, s) ==> t := by
-  grind [cases BigStep]
-
-example {B S T s t} : (ifThenElse B S T, s) ==> t ↔ (B s ∧ (S, s) ==> t) ∨ (¬ B s ∧ (T, s) ==> t) := by
-  grind [BigStep] -- shortcut for `cases BigStep` and `intro BigStep`
-
-attribute [grind] BigStep
-theorem if_iff {B S T s t} : (ifThenElse B S T, s) ==>
-    t ↔ (B s ∧ (S, s) ==> t) ∨ (¬ B s ∧ (T, s) ==> t) := by grind
-
-/- Dependent pattern matching. -/
-
-inductive Vec (α : Type u) : Nat → Type u
-  | nil : Vec α 0
-  | cons : α → Vec α n → Vec α (n+1)
-@[grind =] def Vec.head : Vec α (n+1) → α
-  | .cons a _ => a
-example (as bs : Vec Int (n+1)) : as.head = bs.head
-    → (match as, bs with
-       | .cons a _, .cons b _ => a + b) = 2 * as.head := by grind
-
-/- Theory solvers. -/
-
-example [CommRing α] (a b c : α) :
-    a + b + c = 3 →
-    a^2 + b^2 + c^2 = 5 →
-    a^3 + b^3 + c^3 = 7 →
-    a^4 + b^4 + c^4 = 9 := by grind
-
-example (x : BitVec 8) : (x - 16) * (x + 16) = x^2 := by grind
-
-example [CommSemiring α] [AddRightCancel α] (x y : α) :
-    x^2*y = 1 → x*y^2 = y → y*x = 1 := by grind
-
-example (a b : UInt32) : a ≤ 2 → b ≤ 3 → a + b ≤ 5 := by grind
-
-example [LE α] [Std.IsLinearPreorder α] (a b c d : α) :
-    a ≤ b → ¬ (c ≤ b) → ¬ (d ≤ c) → a ≤ d := by grind
-
-/- Theory combination. -/
-
-example [CommRing α] [NoNatZeroDivisors α]
-    (a b c : α) (f : α → Nat) :
-    a + b + c = 3 → a^2 + b^2 + c^2 = 5 → a^3 + b^3 + c^3 = 7 →
-    f (a^4 + b^4) + f (9 - c^4) ≠ 1 := by grind
-
-/- Interactive mode. -/
-
--- Remark: Mathlib contains the definition of `Real`, `sin`, and `cos`.
-axiom Real : Type
-instance : Lean.Grind.CommRing Real := sorry
-
-axiom cos : Real → Real
-axiom sin : Real → Real
-axiom trig_identity : ∀ x, (cos x)^2 + (sin x)^2 = 1
-
--- Manually specify the patterns for `trig_identity`
-grind_pattern trig_identity => cos x
-grind_pattern trig_identity => sin x
-
-example : (cos x + sin x)^2 = 2 * cos x * sin x + 1 := by
-  grind? -- Provides code action
-
-example : (cos x + sin x)^2 = 2 * cos x * sin x + 1 := by
-  grind =>
-    instantiate only [trig_identity]
-    ring

flake.lock

@@ -2,11 +2,11 @@
   "nodes": {
     "nixpkgs": {
       "locked": {
-        "lastModified": 1769018530,
-        "narHash": "sha256-S/5RU76BdQ32bbE99a+G9gMuatpVWEvIfeSjEqyoFS4=",
-        "rev": "88d3861acdd3d2f0e361767018218e51810df8a1",
+        "lastModified": 1745636243,
+        "narHash": "sha256-kbNvlQZf8wwok3d2X1kM/TlXH/MZ+03ZNv+IPPBx+DM=",
+        "rev": "f771eb401a46846c1aebd20552521b233dd7e18b",
         "type": "tarball",
-        "url": "https://releases.nixos.org/nixos/unstable/nixos-26.05pre931542.88d3861acdd3/nixexprs.tar.xz"
+        "url": "https://releases.nixos.org/nixos/unstable/nixos-25.05pre789333.f771eb401a46/nixexprs.tar.xz"
       },
       "original": {
         "type": "tarball",

flake.nix

@@ -18,13 +18,13 @@
       # An old nixpkgs for creating releases with an old glibc
       pkgsDist-old-aarch = import inputs.nixpkgs-old { localSystem.config = "aarch64-unknown-linux-gnu"; };
 
-      llvmPackages = pkgs.llvmPackages_19;
+      llvmPackages = pkgs.llvmPackages_15;
 
       devShellWithDist = pkgsDist: pkgs.mkShell.override {
           stdenv = pkgs.overrideCC pkgs.stdenv llvmPackages.clang;
         } ({
           buildInputs = with pkgs; [
-            cmake gmp libuv ccache pkg-config openssl
+            cmake gmp libuv ccache pkg-config
             llvmPackages.bintools  # wrapped lld
             llvmPackages.llvm  # llvm-symbolizer for asan/lsan
             gdb

script/lean-bisect

@@ -36,7 +36,7 @@ sys.path.insert(0, str(Path(__file__).parent))
 import build_artifact
 
 # Constants
-NIGHTLY_PATTERN = re.compile(r'^nightly-(\d{4})-(\d{2})-(\d{2})(-rev(\d+))?$')
+NIGHTLY_PATTERN = re.compile(r'^nightly-(\d{4})-(\d{2})-(\d{2})$')
 VERSION_PATTERN = re.compile(r'^v4\.(\d+)\.(\d+)(-rc\d+)?$')
 # Accept short SHAs (7+ chars) - we'll resolve to full SHA later
 SHA_PATTERN = re.compile(r'^[0-9a-f]{7,40}$')
@@ -158,7 +158,7 @@ def parse_identifier(s: str) -> Tuple[str, str]:
         return ('sha', full_sha)
     error(f"Invalid identifier format: '{s}'\n"
           f"Expected one of:\n"
-          f"  - nightly-YYYY-MM-DD or nightly-YYYY-MM-DD-revK (e.g., nightly-2024-06-15, nightly-2024-06-15-rev1)\n"
+          f"  - nightly-YYYY-MM-DD (e.g., nightly-2024-06-15)\n"
           f"  - v4.X.Y or v4.X.Y-rcK (e.g., v4.8.0, v4.9.0-rc1)\n"
           f"  - commit SHA (short or full)")
 
@@ -244,13 +244,8 @@ def fetch_nightly_tags() -> List[str]:
         if len(data) < 100:
             break
 
-    # Sort by date and revision (nightly-YYYY-MM-DD-revK needs numeric comparison on rev)
-    def nightly_sort_key(tag):
-        m = NIGHTLY_PATTERN.match(tag)
-        if m:
-            return (int(m.group(1)), int(m.group(2)), int(m.group(3)), int(m.group(5) or 0))
-        return (0, 0, 0, 0)
-    tags.sort(key=nightly_sort_key)
+    # Sort by date (nightly-YYYY-MM-DD format sorts lexicographically)
+    tags.sort()
     return tags
 
 def get_commit_for_nightly(nightly: str) -> str:
@@ -1029,7 +1024,6 @@ Range Syntax:
 Identifier Formats:
 
   nightly-YYYY-MM-DD    Nightly build date (e.g., nightly-2024-06-15)
-  nightly-YYYY-MM-DD-revK  Revised nightly (e.g., nightly-2024-06-15-rev1)
                         Uses pre-built toolchains from leanprover/lean4-nightly.
                         Fast: downloads via elan (~30s each).
 
@@ -1157,9 +1151,9 @@ Examples:
     # Validate --nightly-only
     if args.nightly_only:
         if from_val is not None and from_type != 'nightly':
-            error("--nightly-only requires FROM to be a nightly identifier (nightly-YYYY-MM-DD or nightly-YYYY-MM-DD-revK)")
+            error("--nightly-only requires FROM to be a nightly identifier (nightly-YYYY-MM-DD)")
         if to_type != 'nightly':
-            error("--nightly-only requires TO to be a nightly identifier (nightly-YYYY-MM-DD or nightly-YYYY-MM-DD-revK)")
+            error("--nightly-only requires TO to be a nightly identifier (nightly-YYYY-MM-DD)")
 
     if from_val:
         info(f"From: {from_val} ({from_type})")

src/CMakeLists.txt

@@ -250,7 +250,7 @@ else()
 endif()
 
 if(NOT MSVC)
-  set(CMAKE_CXX_FLAGS "-Wall -Wextra -std=c++20 ${CMAKE_CXX_FLAGS}")
+  set(CMAKE_CXX_FLAGS "-Wall -Wextra -std=c++14 ${CMAKE_CXX_FLAGS}")
   set(CMAKE_CXX_FLAGS_DEBUG "-g3 ${CMAKE_CXX_FLAGS_DEBUG}")
   if(CMAKE_SYSTEM_NAME MATCHES "Emscripten")
     # smallest+slower | -Oz .. -Os .. -O3 | largest+faster
@@ -347,35 +347,6 @@ if(NOT LEAN_STANDALONE)
   string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${LIBUV_LDFLAGS}")
 endif()
 
-# OpenSSL
-if("${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten")
-  # Only on WebAssembly we compile OpenSSL ourselves
-  set(OPENSSL_EMSCRIPTEN_FLAGS "${EMSCRIPTEN_SETTINGS}")
-
-  # OpenSSL needs to be configured for Emscripten using their configuration system
-  ExternalProject_add(openssl
-    PREFIX openssl
-    GIT_REPOSITORY https://github.com/openssl/openssl
-    # Sync version with flake.nix if applicable
-    GIT_TAG openssl-3.0.15
-    CONFIGURE_COMMAND <SOURCE_DIR>/Configure linux-generic32 no-shared no-dso no-engine no-tests --prefix=<INSTALL_DIR> CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER} AR=${CMAKE_AR} CFLAGS=${OPENSSL_EMSCRIPTEN_FLAGS}
-    BUILD_COMMAND emmake make -j
-    INSTALL_COMMAND emmake make install_sw
-    BUILD_IN_SOURCE ON)
-  set(OPENSSL_INCLUDE_DIR "${CMAKE_BINARY_DIR}/openssl/include")
-  set(OPENSSL_CRYPTO_LIBRARY "${CMAKE_BINARY_DIR}/openssl/lib/libcrypto.a")
-  set(OPENSSL_SSL_LIBRARY "${CMAKE_BINARY_DIR}/openssl/lib/libssl.a")
-  set(OPENSSL_LIBRARIES "${OPENSSL_SSL_LIBRARY} ${OPENSSL_CRYPTO_LIBRARY}")
-else()
-  find_package(OpenSSL REQUIRED)
-  set(OPENSSL_LIBRARIES ${OPENSSL_SSL_LIBRARY} ${OPENSSL_CRYPTO_LIBRARY})
-endif()
-include_directories(${OPENSSL_INCLUDE_DIR})
-if(NOT LEAN_STANDALONE)
-  string(JOIN " " OPENSSL_LIBRARIES ${OPENSSL_LIBRARIES})
-  string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${OPENSSL_LIBRARIES}")
-endif()
-
 # Windows SDK (for ICU)
 if(CMAKE_SYSTEM_NAME MATCHES "Windows")
   # Pass 'tools' to skip MSVC version check (as MSVC/Visual Studio is not necessarily installed)
@@ -750,9 +721,9 @@ if(STAGE GREATER 1)
   endif()
 else()
   add_subdirectory(runtime)
-  if("${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten")
-    add_dependencies(leanrt libuv openssl)
-    add_dependencies(leanrt_initial-exec libuv openssl)
+  if(CMAKE_SYSTEM_NAME MATCHES "Emscripten")
+    add_dependencies(leanrt libuv)
+    add_dependencies(leanrt_initial-exec libuv)
   endif()
 
   add_subdirectory(util)

src/Init.lean

@@ -42,7 +42,7 @@ public import Init.While
 public import Init.Syntax
 public import Init.Internal
 public import Init.Try
-public meta import Init.Try  -- shake: keep (make sure `Try.Config` can be evaluated anywhere)
+public meta import Init.Try  -- make sure `Try.Config` can be evaluated anywhere
 public import Init.BinderNameHint
 public import Init.Task
 public import Init.MethodSpecsSimp

src/Init/BinderNameHint.lean

@@ -7,8 +7,7 @@ Authors: Joachim Breitner
 module
 
 prelude
-public import Init.Prelude
-import Init.Tactics
+public import Init.Tactics
 
 public section
 

src/Init/BinderPredicates.lean

@@ -6,10 +6,7 @@ Authors: Gabriel Ebner
 module
 
 prelude
-public meta import Init.Grind.Tactics
-public import Init.Notation
-import Init.Meta.Defs
-import Init.NotationExtra
+public import Init.NotationExtra
 
 public section
 

src/Init/ByCases.lean

@@ -6,9 +6,7 @@ Authors: Leonardo de Moura, Mario Carneiro
 module
 
 prelude
-public meta import Init.Grind.Tactics
-public import Init.Grind.Tactics
-import Init.SimpLemmas
+public import Init.Classical
 
 public section
 

src/Init/Control.lean

@@ -17,4 +17,3 @@ public import Init.Control.Lawful
 public import Init.Control.StateCps
 public import Init.Control.ExceptCps
 public import Init.Control.MonadAttach
-public import Init.Control.EState

src/Init/Control/Basic.lean

@@ -29,7 +29,7 @@ instance (priority := 500) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α
     (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
-  simp [forIn]
+  simp [instForInOfForIn']
   congr
   apply funext
   intro a
@@ -322,8 +322,6 @@ class MonadControl (m : semiOutParam (Type u → Type v)) (n : Type u → Type w
   -/
   restoreM : {α : Type u} → m (stM α) → n α
 
-attribute [reducible] MonadControl.stM
-
 /--
 A way to lift a computation from one monad to another while providing the lifted computation with a
 means of interpreting computations from the outer monad. This provides a means of lifting
@@ -351,8 +349,6 @@ class MonadControlT (m : Type u → Type v) (n : Type u → Type w) where
   -/
   restoreM {α : Type u} : stM α → n α
 
-attribute [reducible] MonadControlT.stM
-
 export MonadControlT (stM liftWith restoreM)
 
 @[always_inline]

src/Init/Control/EState.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Data.ToString.Basic
-public import Init.Control.State
 
 public section
 universe u v

src/Init/Control/ExceptCps.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Control.Lawful.Basic
-import Init.SimpLemmas
 
 public section
 

src/Init/Control/Id.lean

@@ -8,6 +8,7 @@ The identity Monad.
 module
 
 prelude
+public import Init.Core
 public import Init.Control.MonadAttach
 
 public section

src/Init/Control/Lawful/Basic.lean

@@ -6,9 +6,7 @@ Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
 module
 
 prelude
-public import Init.Control.Id
-public import Init.Grind.Tactics
-import Init.Ext
+public import Init.Ext
 
 public section
 

src/Init/Control/Lawful/Instances.lean

@@ -12,8 +12,6 @@ public import Init.Control.Option
 import all Init.Control.Option
 import all Init.Control.State
 public import Init.Control.StateRef
-public import Init.Control.State
-public import Init.Ext
 
 public section
 
@@ -104,7 +102,7 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (ExceptT ε m) where
 
 @[simp] theorem map_throw [Monad m] [LawfulMonad m] {α β : Type _} (f : α → β) (e : ε) :
     f <$> (throw e : ExceptT ε m α) = (throw e : ExceptT ε m β) := by
-  simp only [Functor.map, ExceptT.map, ExceptT.mk, throw, throwThe, MonadExceptOf.throw,
+  simp only [ExceptT.instMonad, ExceptT.map, ExceptT.mk, throw, throwThe, MonadExceptOf.throw,
     pure_bind]
 
 /-! Note that the `MonadControl` instance for `ExceptT` is not monad-generic. -/

src/Init/Control/Lawful/Lemmas.lean

@@ -7,9 +7,7 @@ module
 
 prelude
 public import Init.Control.Lawful.Basic
-public import Init.Classical
-public import Init.Ext
-import Init.ByCases
+public import Init.ByCases
 
 public section
 

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

@@ -6,11 +6,9 @@ Authors: Paul Reichert
 module
 
 prelude
+public import Init.Control.Reader
+public import Init.Control.Lawful.Instances
 import Init.Control.Lawful.MonadAttach.Lemmas
-public import Init.Control.Lawful.Basic
-public import Init.Control.State
-public import Init.Control.StateRef
-public import Init.Ext
 
 public instance [Monad m] [LawfulMonad m] [MonadAttach m] [WeaklyLawfulMonadAttach m] :
     WeaklyLawfulMonadAttach (ReaderT ρ m) where

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

@@ -6,12 +6,10 @@ Authors: Paul Reichert
 module
 
 prelude
+public import Init.Control.MonadAttach
 import all Init.Control.MonadAttach
-public import Init.Classical
-public import Init.Control.Lawful.Basic
-public import Init.Control.Lawful.MonadLift.Basic
-import Init.Control.Lawful.MonadLift.Lemmas
-import Init.RCases
+public import Init.Control.Lawful.Lemmas
+public import Init.Control.Lawful.MonadLift.Lemmas
 
 public theorem LawfulMonadAttach.canReturn_bind_imp' [Monad m] [LawfulMonad m]
     [MonadAttach m] [LawfulMonadAttach m]

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

@@ -6,7 +6,7 @@ Authors: Quang Dao
 module
 
 prelude
-public import Init.Notation
+public import Init.Control.Basic
 
 public section
 

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

@@ -14,12 +14,8 @@ import all Init.Control.StateRef
 public import Init.Control.StateCps
 import all Init.Control.StateCps
 import all Init.Control.Id
-public import Init.Control.Lawful.MonadLift.Basic
-public import Init.Control.Option
-public import Init.Control.State
-public import Init.Control.StateRef
-import Init.Control.Lawful.Instances
-import Init.Control.Lawful.MonadLift.Lemmas
+public import Init.Control.Lawful.MonadLift.Lemmas
+public import Init.Control.Lawful.Instances
 
 public section
 
@@ -67,7 +63,7 @@ variable [Monad m] [LawfulMonad m]
 @[simp]
 theorem lift_bind {α β : Type u} (ma : m α) (f : α → m β) :
     OptionT.lift (ma >>= f) = OptionT.lift ma >>= (fun a => OptionT.lift (f a)) := by
-  simp only [bind, OptionT.bind, OptionT.mk, OptionT.lift, bind_pure_comp, bind_map_left,
+  simp only [instMonad, OptionT.bind, OptionT.mk, OptionT.lift, bind_pure_comp, bind_map_left,
     map_bind]
 
 instance : LawfulMonadLift m (OptionT m) where
@@ -83,7 +79,7 @@ variable [Monad m] [LawfulMonad m]
 @[simp]
 theorem lift_bind {α β ε : Type u} (ma : m α) (f : α → m β) :
     ExceptT.lift (ε := ε) (ma >>= f) = ExceptT.lift ma >>= (fun a => ExceptT.lift (f a)) := by
-  simp only [bind, ExceptT.bind, mk, ExceptT.lift, bind_map_left, ExceptT.bindCont, map_bind]
+  simp only [instMonad, ExceptT.bind, mk, ExceptT.lift, bind_map_left, ExceptT.bindCont, map_bind]
 
 instance : LawfulMonadLift m (ExceptT ε m) where
   monadLift_pure := lift_pure
@@ -93,7 +89,8 @@ instance : LawfulMonadLift (Except ε) (ExceptT ε m) where
   monadLift_pure _ := by
     simp only [MonadLift.monadLift, mk, pure, Except.pure, ExceptT.pure]
   monadLift_bind ma _ := by
-    simp only [bind, ExceptT.bind, mk, MonadLift.monadLift, pure_bind, ExceptT.bindCont, Except.bind]
+    simp only [instMonad, ExceptT.bind, mk, MonadLift.monadLift, pure_bind, ExceptT.bindCont,
+      Except.instMonad, Except.bind]
     rcases ma with _ | _ <;> simp
 
 end ExceptT

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

@@ -6,9 +6,9 @@ Authors: Quang Dao
 module
 
 prelude
+public import Init.Control.Id
 public import Init.Control.Lawful.Basic
 public import Init.Control.Lawful.MonadLift.Basic
-import Init.Ext
 
 public section
 
@@ -17,7 +17,7 @@ universe u v w
 theorem instMonadLiftTOfMonadLift_instMonadLiftTOfPure [Monad m] [Monad n] {_ : MonadLift m n}
     [LawfulMonadLift m n] : instMonadLiftTOfMonadLift Id m n = Id.instMonadLiftTOfPure := by
   have hext {a b : MonadLiftT Id n} (h : @a.monadLift = @b.monadLift) : a = b := by
-    cases a; cases b; simp [monadLift] at h; simp [h]
+    cases a <;> cases b <;> simp_all
   apply hext
   ext α x
   simp [monadLift, LawfulMonadLift.monadLift_pure]

src/Init/Control/MonadAttach.lean

@@ -6,7 +6,7 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Init.Core
+public import Init.Control.Basic
 
 set_option linter.all true
 

src/Init/Control/Option.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Init.Data.Option.Basic
-public import Init.Control.MonadAttach
+public import Init.Control.Except
 
 public section
 

src/Init/Control/StateCps.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Control.Lawful.Basic
-public import Init.Ext
 
 public section
 

src/Init/Control/StateRef.lean

@@ -9,7 +9,6 @@ module
 
 prelude
 public import Init.System.ST
-public import Init.Control.Reader
 
 public section
 

src/Init/Conv.lean

@@ -51,19 +51,8 @@ scoped syntax (name := withAnnotateState)
 /-- `skip` does nothing. -/
 syntax (name := skip) "skip" : conv
 
-/--
-`cbv` performs simplification that closely mimics call-by-value evaluation.
-It reduces the target term by unfolding definitions using their defining equations and
-applying matcher equations. The unfolding is propositional, so `cbv` also works
-with functions defined via well-founded recursion or partial fixpoints.
-
-The proofs produced by `cbv` only use the three standard axioms.
-In particular, they do not require trust in the correctness of the code
-generator.
-
-This tactic is experimental and its behavior is likely to change in upcoming
-releases of Lean.
--/
+/-- `cbv` performs simplification that closely mimics call-by-value evaluation,
+using equations associated with definitions and the matchers. -/
 syntax (name := cbv) "cbv" : conv
 
 /--

src/Init/Core.lean

@@ -9,7 +9,6 @@ module
 
 prelude
 public import Init.SizeOf
-public import Init.Tactics
 
 public section
 set_option linter.missingDocs true -- keep it documented
@@ -489,8 +488,6 @@ class HasEquiv (α : Sort u) where
   the notion of equivalence is type-dependent. -/
   Equiv : α → α → Sort v
 
-attribute [reducible] HasEquiv.Equiv
-
 @[inherit_doc] infix:50 " ≈ "  => HasEquiv.Equiv
 
 recommended_spelling "equiv" for "≈" in [HasEquiv.Equiv, «term_≈_»]

src/Init/Data/AC.lean

@@ -7,9 +7,7 @@ Authors: Dany Fabian
 module
 
 prelude
-public import Init.GetElem
-import Init.ByCases
-import Init.PropLemmas
+public import Init.ByCases
 
 @[expose] public section
 

src/Init/Data/Array.lean

@@ -33,4 +33,3 @@ public import Init.Data.Array.Extract
 public import Init.Data.Array.MinMax
 public import Init.Data.Array.Nat
 public import Init.Data.Array.Int
-public import Init.Data.Array.Count

src/Init/Data/Array/Attach.lean

@@ -6,10 +6,8 @@ Authors: Joachim Breitner, Mario Carneiro
 module
 
 prelude
+public import Init.Data.Array.Count
 import all Init.Data.List.Attach
-public import Init.Data.Array.Lemmas
-import Init.Data.Array.Bootstrap
-import Init.Data.Array.Count
 
 public section
 

src/Init/Data/Array/Basic.lean

@@ -11,9 +11,6 @@ public import Init.Data.List.ToArrayImpl
 import all Init.Data.List.ToArrayImpl
 public import Init.Data.Array.Set
 import all Init.Data.Array.Set
-public import Init.WF
-meta import Init.MetaTypes
-import Init.WFTactics
 
 public section
 
@@ -2125,7 +2122,7 @@ Examples:
 
 /-! ### Repr and ToString -/
 
-protected def repr {α : Type u} [Repr α] (xs : Array α) : Std.Format :=
+protected def Array.repr {α : Type u} [Repr α] (xs : Array α) : Std.Format :=
   let _ : Std.ToFormat α := ⟨repr⟩
   if xs.size == 0 then
     "#[]"

src/Init/Data/Array/BasicAux.lean

@@ -7,9 +7,7 @@ module
 
 prelude
 import all Init.Data.Array.Basic
-public import Init.Data.Array.Set
-public import Init.Util
-import Init.Data.Nat.Linear
+public import Init.Data.Nat.Linear
 
 public section
 

src/Init/Data/Array/BinSearch.lean

@@ -6,10 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.Array.Basic
-import Init.Data.Bool
-import Init.Omega
-import Init.WFTactics
+public import Init.Data.Int.DivMod.Lemmas
 
 public section
 universe u v

src/Init/Data/Array/Bootstrap.lean

@@ -7,10 +7,8 @@ Authors: Mario Carneiro
 module
 
 prelude
+public import Init.Data.List.TakeDrop
 import all Init.Data.Array.Basic
-public import Init.Data.List.Control
-import Init.Data.List.Lemmas
-import Init.Data.List.TakeDrop
 
 public section
 

src/Init/Data/Array/Count.lean

@@ -7,14 +7,9 @@ module
 
 prelude
 import all Init.Data.Array.Basic
-import Init.Grind.Util  -- shake: keep (`@[grind]` dependency)
-public import Init.BinderPredicates
-public import Init.Ext
-public import Init.NotationExtra
-import Init.Data.Array.Lemmas
-import Init.Data.Bool
-import Init.Data.List.Count
-import Init.Data.List.Nat.Count
+public import Init.Data.Array.Lemmas
+public import Init.Data.List.Nat.Count
+import Init.Grind.Util
 
 public section
 

src/Init/Data/Array/DecidableEq.lean

@@ -7,14 +7,8 @@ module
 
 prelude
 import all Init.Data.Array.Basic
-public import Init.Data.Array.Basic
-public import Init.Data.Nat.Lemmas
-import Init.ByCases
-import Init.Classical
-import Init.Data.BEq
-import Init.Data.Bool
-import Init.Data.List.Nat.BEq
-import Init.RCases
+public import Init.Data.BEq
+public import Init.Data.List.Nat.BEq
 
 public section
 

src/Init/Data/Array/Erase.lean

@@ -8,13 +8,6 @@ module
 prelude
 import all Init.Data.Array.Basic
 public import Init.Data.Array.Lemmas
-import Init.Data.Array.Bootstrap
-import Init.Data.Bool
-import Init.Data.List.Erase
-import Init.Data.List.Nat.Basic
-import Init.Data.List.Nat.Erase
-import Init.Data.List.TakeDrop
-import Init.Omega
 
 public section
 

src/Init/Data/Array/Extract.lean

@@ -6,16 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Init.BinderPredicates
-public import Init.Ext
-public import Init.NotationExtra
-import Init.ByCases
-import Init.Data.Array.Bootstrap
-import Init.Data.Array.Lemmas
-import Init.Data.Bool
-import Init.Data.List.Nat.TakeDrop
-import Init.Data.List.TakeDrop
-import Init.Omega
+public import Init.Data.Array.Lemmas
 
 public section
 

src/Init/Data/Array/FinRange.lean

@@ -6,11 +6,7 @@ Authors: François G. Dorais
 module
 
 prelude
-public import Init.Data.Array.Basic
-import Init.Data.Array.Lemmas
-import Init.Data.Array.OfFn
-import Init.Data.Fin.Lemmas
-import Init.Omega
+public import Init.Data.Array.OfFn
 
 public section
 

src/Init/Data/Array/Find.lean

@@ -6,22 +6,10 @@ Authors: Kim Morrison
 module
 
 prelude
+public import Init.Data.List.Nat.Find
 import Init.Data.List.Nat.Sum
 import all Init.Data.Array.Basic
-public import Init.Data.Array.Attach
-public import Init.Data.Option.BasicAux
-import Init.ByCases
-import Init.Data.Array.Bootstrap
-import Init.Data.Array.MapIdx
-import Init.Data.Bool
-import Init.Data.Fin.Lemmas
-import Init.Data.List.Count
-import Init.Data.List.Find
-import Init.Data.List.Impl
-import Init.Data.List.Nat.Find
-import Init.Data.List.Nat.TakeDrop
-import Init.Data.List.TakeDrop
-import Init.Omega
+public import Init.Data.Array.Range
 
 public section
 

src/Init/Data/Array/GetLit.lean

@@ -7,8 +7,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.GetElem
-import Init.Data.Array.Basic
+public import Init.Data.Array.Basic
 
 public section
 

src/Init/Data/Array/InsertIdx.lean

@@ -6,11 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Init.Data.Array.Basic
-import Init.Data.List.Nat.InsertIdx
-import Init.Data.List.ToArray
-import Init.Data.Nat.Lemmas
-import Init.Omega
+public import Init.Data.Array.Lemmas
 
 public section
 

src/Init/Data/Array/Int.lean

@@ -7,8 +7,10 @@ module
 
 prelude
 public import Init.Data.List.Int.Sum
-public import Init.Data.Array.MinMax
-import Init.Data.Int.Lemmas
+public import Init.Data.Array.Lemmas
+public import Init.Data.Int.DivMod.Bootstrap
+import Init.Data.Int.DivMod.Lemmas
+import Init.Data.List.MinMax
 
 public section
 
@@ -30,48 +32,4 @@ theorem sum_reverse_int (xs : Array Int) : xs.reverse.sum = xs.sum := by
 theorem sum_eq_foldl_int {xs : Array Int} : xs.sum = xs.foldl (init := 0) (· + ·) := by
   simp only [foldl_eq_foldr_reverse, Int.add_comm, ← sum_eq_foldr, sum_reverse_int]
 
-theorem min_mul_length_le_sum_int {xs : Array Int} (h : xs ≠ #[]) :
-    xs.min h * xs.size ≤ xs.sum := by
-  rcases xs with ⟨l⟩
-  simpa [List.min_toArray, List.sum_toArray] using List.min_mul_length_le_sum_int (by simpa using h)
-
-theorem mul_length_le_sum_of_min?_eq_some_int {xs : Array Int} (h : xs.min? = some x) :
-    x * xs.size ≤ xs.sum := by
-  rcases xs with ⟨l⟩
-  simpa [List.min?_toArray, List.sum_toArray] using
-    List.mul_length_le_sum_of_min?_eq_some_int (by simpa using h)
-
-theorem min_le_sum_div_length_int {xs : Array Int} (h : xs ≠ #[]) :
-    xs.min h ≤ xs.sum / xs.size := by
-  rcases xs with ⟨l⟩
-  simpa [List.min_toArray, List.sum_toArray] using List.min_le_sum_div_length_int (by simpa using h)
-
-theorem le_sum_div_length_of_min?_eq_some_int {xs : Array Int} (h : xs.min? = some x) :
-    x ≤ xs.sum / xs.size := by
-  rcases xs with ⟨l⟩
-  simpa [List.min?_toArray, List.sum_toArray] using
-    List.le_sum_div_length_of_min?_eq_some_int (by simpa using h)
-
-theorem sum_le_max_mul_length_int {xs : Array Int} (h : xs ≠ #[]) :
-    xs.sum ≤ xs.max h * xs.size := by
-  rcases xs with ⟨l⟩
-  simpa [List.max_toArray, List.sum_toArray] using List.sum_le_max_mul_length_int (by simpa using h)
-
-theorem sum_le_max_mul_length_of_max?_eq_some_int {xs : Array Int} (h : xs.max? = some x) :
-    xs.sum ≤ x * xs.size := by
-  rcases xs with ⟨l⟩
-  simpa [List.max?_toArray, List.sum_toArray] using
-    List.sum_le_max_mul_length_of_max?_eq_some_int (by simpa using h)
-
-theorem sum_div_length_le_max_int {xs : Array Int} (h : xs ≠ #[]) :
-    xs.sum / xs.size ≤ xs.max h := by
-  rcases xs with ⟨l⟩
-  simpa [List.max_toArray, List.sum_toArray] using List.sum_div_length_le_max_int (by simpa using h)
-
-theorem sum_div_length_le_max_of_max?_eq_some_int {xs : Array Int} (h : xs.max? = some x) :
-    xs.sum / xs.size ≤ x := by
-  rcases xs with ⟨l⟩
-  simpa [List.max?_toArray, List.sum_toArray] using
-    List.sum_div_length_le_max_of_max?_eq_some_int (by simpa using h)
-
 end Array

src/Init/Data/Array/Lemmas.lean

@@ -6,28 +6,14 @@ Authors: Mario Carneiro, Kim Morrison
 module
 
 prelude
+public import Init.Data.List.Nat.Basic
+public import Init.Data.Array.Mem
+public import Init.Data.Array.DecidableEq
+public import Init.Data.Range.Lemmas
 public import Init.Data.List.ToArray
 import all Init.Data.List.Control
 import all Init.Data.Array.Basic
 import all Init.Data.Array.Bootstrap
-public import Init.Data.Nat.Lemmas
-public import Init.Data.Nat.MinMax
-import Init.ByCases
-import Init.Data.Array.DecidableEq
-import Init.Data.Bool
-import Init.Data.Fin.Lemmas
-import Init.Data.List.Find
-import Init.Data.List.Nat.Basic
-import Init.Data.List.Nat.Modify
-import Init.Data.List.Nat.TakeDrop
-import Init.Data.List.Range
-import Init.Data.List.Zip
-import Init.Data.Nat.Linear
-import Init.Data.Nat.Simproc
-import Init.Data.Option.Lemmas
-import Init.Data.Prod
-import Init.Omega
-import Init.TacticsExtra
 
 public section
 

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

@@ -6,10 +6,9 @@ Author: Kim Morrison
 module
 
 prelude
-public import Init.Data.Range.Polymorphic.RangeIterator
-import Init.Data.Range.Polymorphic.Iterators
-import Init.Data.Range.Polymorphic.Nat
-import Init.Omega
+public import Init.Data.Range.Polymorphic.Iterators
+public import Init.Data.Range.Polymorphic.Nat
+import Init.Data.Iterators.Consumers
 
 public section
 

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

@@ -8,13 +8,9 @@ module
 prelude
 import all Init.Data.Array.Lex.Basic
 public import Init.Data.Array.Lex.Basic
+public import Init.Data.Array.Lemmas
+public import Init.Data.List.Lex
 import Init.Data.Range.Polymorphic.NatLemmas
-public import Init.Data.BEq
-import Init.Data.Array.DecidableEq
-import Init.Data.Array.Lemmas
-import Init.Data.Bool
-import Init.Data.List.Lex
-import Init.Data.Range.Polymorphic.Lemmas
 
 public section
 

src/Init/Data/Array/MapIdx.lean

@@ -7,9 +7,9 @@ module
 
 prelude
 import all Init.Data.Array.Basic
+public import Init.Data.Array.OfFn
 public import Init.Data.List.MapIdx
 import all Init.Data.List.MapIdx
-import Init.Data.Array.OfFn
 
 public section
 

src/Init/Data/Array/Mem.lean

@@ -6,11 +6,7 @@ Authors: Leonardo de Moura, Joachim Breitner
 module
 
 prelude
-public import Init.Data.Array.Basic
-public import Init.WFTactics
-import Init.Data.List.BasicAux
-import Init.Data.Nat.Linear
-meta import Init.MetaTypes
+public import Init.Data.List.BasicAux
 
 public section
 

src/Init/Data/Array/MinMax.lean

@@ -6,13 +6,11 @@ Authors: Paul Reichert
 module
 
 prelude
+public import Init.Data.Array.Bootstrap
 public import Init.Data.Array.Lemmas
+public import Init.Data.Array.DecidableEq
 import Init.Data.List.MinMax
-public import Init.Data.Order.Classes
-import Init.Data.Array.Bootstrap
-import Init.Data.Array.DecidableEq
-import Init.Data.List.TakeDrop
-import Init.Data.Order.Lemmas
+import Init.Data.List.ToArray
 
 namespace Array
 

src/Init/Data/Array/Monadic.lean

@@ -9,7 +9,6 @@ prelude
 import all Init.Data.List.Control
 import all Init.Data.Array.Basic
 public import Init.Data.Array.Attach
-import Init.Data.Bool
 
 public section
 

src/Init/Data/Array/Nat.lean

@@ -6,9 +6,8 @@ Authors: Kim Morrison, Sebastian Graf, Paul Reichert
 module
 
 prelude
-public import Init.Data.Array.MinMax
+public import Init.Data.Array.Lemmas
 import Init.Data.List.Nat.Sum
-import Init.Data.Array.Lemmas
 
 public section
 
@@ -37,48 +36,4 @@ theorem sum_reverse_nat (xs : Array Nat) : xs.reverse.sum = xs.sum := by
 theorem sum_eq_foldl_nat {xs : Array Nat} : xs.sum = xs.foldl (init := 0) (· + ·) := by
   simp only [foldl_eq_foldr_reverse, Nat.add_comm, ← sum_eq_foldr, sum_reverse_nat]
 
-theorem min_mul_length_le_sum_nat {xs : Array Nat} (h : xs ≠ #[]) :
-    xs.min h * xs.size ≤ xs.sum := by
-  rcases xs with ⟨l⟩
-  simpa [List.min_toArray, List.sum_toArray] using List.min_mul_length_le_sum_nat (by simpa using h)
-
-theorem mul_length_le_sum_of_min?_eq_some_nat {xs : Array Nat} (h : xs.min? = some x) :
-    x * xs.size ≤ xs.sum := by
-  rcases xs with ⟨l⟩
-  simpa [List.min?_toArray, List.sum_toArray] using
-    List.mul_length_le_sum_of_min?_eq_some_nat (by simpa using h)
-
-theorem min_le_sum_div_length_nat {xs : Array Nat} (h : xs ≠ #[]) :
-    xs.min h ≤ xs.sum / xs.size := by
-  rcases xs with ⟨l⟩
-  simpa [List.min_toArray, List.sum_toArray] using List.min_le_sum_div_length_nat (by simpa using h)
-
-theorem le_sum_div_length_of_min?_eq_some_nat {xs : Array Nat} (h : xs.min? = some x) :
-    x ≤ xs.sum / xs.size := by
-  rcases xs with ⟨l⟩
-  simpa [List.min?_toArray, List.sum_toArray] using
-    List.le_sum_div_length_of_min?_eq_some_nat (by simpa using h)
-
-theorem sum_le_max_mul_length_nat {xs : Array Nat} (h : xs ≠ #[]) :
-    xs.sum ≤ xs.max h * xs.size := by
-  rcases xs with ⟨l⟩
-  simpa [List.max_toArray, List.sum_toArray] using List.sum_le_max_mul_length_nat (by simpa using h)
-
-theorem sum_le_max_mul_length_of_max?_eq_some_nat {xs : Array Nat} (h : xs.max? = some x) :
-    xs.sum ≤ x * xs.size := by
-  rcases xs with ⟨l⟩
-  simpa [List.max?_toArray, List.sum_toArray] using
-    List.sum_le_max_mul_length_of_max?_eq_some_nat (by simpa using h)
-
-theorem sum_div_length_le_max_nat {xs : Array Nat} (h : xs ≠ #[]) :
-    xs.sum / xs.size ≤ xs.max h := by
-  rcases xs with ⟨l⟩
-  simpa [List.max_toArray, List.sum_toArray] using List.sum_div_length_le_max_nat (by simpa using h)
-
-theorem sum_div_length_le_max_of_max?_eq_some_nat {xs : Array Nat} (h : xs.max? = some x) :
-    xs.sum / xs.size ≤ x := by
-  rcases xs with ⟨l⟩
-  simpa [List.max?_toArray, List.sum_toArray] using
-    List.sum_div_length_le_max_of_max?_eq_some_nat (by simpa using h)
-
 end Array

src/Init/Data/Array/OfFn.lean

@@ -7,13 +7,8 @@ module
 
 prelude
 import all Init.Data.Array.Basic
-public import Init.Data.List.OfFn
-import Init.Data.Array.Bootstrap
-import Init.Data.Array.Monadic
-import Init.Data.Fin.Lemmas
-import Init.Data.List.FinRange
-import Init.Data.Option.Lemmas
-import Init.Omega
+public import Init.Data.Array.Monadic
+public import Init.Data.List.FinRange
 
 public section
 

src/Init/Data/Array/Perm.lean

@@ -6,13 +6,9 @@ Authors: Kim Morrison
 module
 
 prelude
+public import Init.Data.List.Nat.Perm
 import all Init.Data.Array.Basic
-public import Init.Data.Array.Basic
-import Init.Data.Array.Lemmas
-import Init.Data.List.Nat.Perm
-import Init.Data.List.Nat.TakeDrop
-import Init.Data.List.Perm
-import Init.Omega
+public import Init.Data.Array.Lemmas
 
 public section
 

src/Init/Data/Array/QSort/Basic.lean

@@ -8,7 +8,6 @@ module
 prelude
 public import Init.Data.Vector.Basic
 public import Init.Data.Ord.Basic
-import Init.Omega
 
 public section
 

src/Init/Data/Array/Range.lean

@@ -8,16 +8,8 @@ module
 prelude
 import all Init.Data.Array.Basic
 import all Init.Data.Array.OfFn
-public import Init.BinderPredicates
-public import Init.Data.Nat.Lemmas
-public import Init.Ext
-import Init.ByCases
-import Init.Data.Array.Count
-import Init.Data.Array.MapIdx
-import Init.Data.Array.Zip
-import Init.Data.List.Find
-import Init.Data.List.Nat.Range
-import Init.Data.List.Range
+public import Init.Data.Array.MapIdx
+public import Init.Data.Array.Zip
 
 public section
 

src/Init/Data/Array/Subarray.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.Array.Basic
+import Init.Data.Array.GetLit
 public import Init.Data.Slice.Basic
 
 public section

src/Init/Data/Array/Subarray/Split.lean

@@ -9,7 +9,7 @@ module
 prelude
 public import Init.Data.Array.Subarray
 import all Init.Data.Array.Subarray
-import Init.Omega
+public import Init.Omega
 
 public section
 

src/Init/Data/Array/TakeDrop.lean

@@ -7,11 +7,7 @@ module
 
 prelude
 import all Init.Data.Array.Basic
-public import Init.Data.Array.Basic
-public import Init.NotationExtra
-import Init.Data.Array.Lemmas
-import Init.Data.List.Nat.TakeDrop
-import Init.Data.List.TakeDrop
+public import Init.Data.Array.Lemmas
 
 public section
 

src/Init/Data/Array/Zip.lean

@@ -7,14 +7,7 @@ module
 
 prelude
 import all Init.Data.Array.Basic
-public import Init.Control.Lawful
-public import Init.Data.Function
-import Init.Data.Array.Lemmas
-import Init.Data.List.Nat.TakeDrop
-import Init.Data.List.Zip
-import Init.Data.Option.Lemmas
-import Init.Data.Prod
-import Init.Omega
+public import Init.Data.Array.TakeDrop
 
 public section
 

src/Init/Data/BEq.lean

@@ -6,8 +6,7 @@ Authors: Mario Carneiro, Markus Himmel
 module
 
 prelude
-public import Init.Grind.Tactics
-import Init.Data.Bool
+public import Init.Data.Bool
 
 public section
 

src/Init/Data/BitVec/Basic.lean

@@ -6,16 +6,8 @@ Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro, Alex
 module
 
 prelude
+public import Init.Data.Nat.Bitwise.Lemmas
 public import Init.Data.Int.Bitwise.Basic
-public import Init.Data.Bool
-public import Init.Data.Int.DivMod.Basic
-public import Init.WF
-import Init.Data.Nat.Bitwise.Lemmas
-import Init.Data.Nat.Lemmas
-import Init.Data.Nat.Linear
-import Init.Meta.Defs
-import Init.Omega
-import Init.WFTactics
 
 @[expose] public section
 
@@ -210,7 +202,7 @@ protected def toHex {n : Nat} (x : BitVec n) : String :=
   String.Internal.append t s
 
 /-- `BitVec` representation. -/
-protected def repr (a : BitVec n) : Std.Format :=
+protected def BitVec.repr (a : BitVec n) : Std.Format :=
   "0x" ++ (a.toHex : Std.Format) ++ "#" ++ repr n
 
 instance : Repr (BitVec n) where
@@ -269,7 +261,7 @@ Usually accessed via the `/` operator.
 -/
 @[expose]
 def udiv (x y : BitVec n) : BitVec n :=
-  (x.toNat / y.toNat)#'(by exact Nat.lt_of_le_of_lt (Nat.div_le_self _ _) x.isLt)
+  (x.toNat / y.toNat)#'(Nat.lt_of_le_of_lt (Nat.div_le_self _ _) x.isLt)
 instance : Div (BitVec n) := ⟨.udiv⟩
 
 /--
@@ -279,7 +271,7 @@ SMT-LIB name: `bvurem`.
 -/
 @[expose]
 def umod (x y : BitVec n) : BitVec n :=
-  (x.toNat % y.toNat)#'(by exact Nat.lt_of_le_of_lt (Nat.mod_le _ _) x.isLt)
+  (x.toNat % y.toNat)#'(Nat.lt_of_le_of_lt (Nat.mod_le _ _) x.isLt)
 instance : Mod (BitVec n) := ⟨.umod⟩
 
 /--
@@ -523,7 +515,7 @@ Example:
 -/
 @[expose]
 protected def and (x y : BitVec n) : BitVec n :=
-  (x.toNat &&& y.toNat)#'(by exact Nat.and_lt_two_pow x.toNat y.isLt)
+  (x.toNat &&& y.toNat)#'(Nat.and_lt_two_pow x.toNat y.isLt)
 instance : AndOp (BitVec w) := ⟨.and⟩
 
 /--
@@ -536,7 +528,7 @@ Example:
 -/
 @[expose]
 protected def or (x y : BitVec n) : BitVec n :=
-  (x.toNat ||| y.toNat)#'(by exact Nat.or_lt_two_pow x.isLt y.isLt)
+  (x.toNat ||| y.toNat)#'(Nat.or_lt_two_pow x.isLt y.isLt)
 instance : OrOp (BitVec w) := ⟨.or⟩
 
 /--
@@ -549,7 +541,7 @@ Example:
 -/
 @[expose]
 protected def xor (x y : BitVec n) : BitVec n :=
-  (x.toNat ^^^ y.toNat)#'(by exact Nat.xor_lt_two_pow x.isLt y.isLt)
+  (x.toNat ^^^ y.toNat)#'(Nat.xor_lt_two_pow x.isLt y.isLt)
 instance : XorOp (BitVec w) := ⟨.xor⟩
 
 /--

src/Init/Data/BitVec/BasicAux.lean

@@ -6,7 +6,7 @@ Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro, Alex
 module
 
 prelude
-public import Init.Grind.Tactics
+public import Init.Data.Fin.Basic
 
 public section
 

src/Init/Data/BitVec/Bitblast.lean

@@ -7,20 +7,12 @@ module
 
 prelude
 import all Init.Data.Nat.Bitwise.Basic
+public import Init.Data.Int.DivMod
 import all Init.Data.Int.DivMod
 import all Init.Data.BitVec.Basic
+public import Init.Data.BitVec.Decidable
 public import Init.Data.BitVec.Folds
-public import Init.BinderPredicates
-public import Init.Data.BitVec.Lemmas
-public import Init.Data.Nat.Lemmas
-import Init.ByCases
-import Init.Data.BitVec.Bootstrap
-import Init.Data.BitVec.Decidable
-import Init.Data.Int.Pow
-import Init.Data.Nat.Div.Lemmas
-import Init.Data.Nat.Mod
-import Init.Data.Nat.Simproc
-import Init.TacticsExtra
+import Init.BinderPredicates
 
 @[expose] public section
 
@@ -2241,7 +2233,7 @@ def aandRec (x y : BitVec w) (s : Nat) (hs : s < w) : Bool :=
 -/
 def resRec (x y : BitVec w) (s : Nat) (hs : s < w) (hslt : 0 < s) : Bool :=
   match hs0 : s with
-  | 0 => False.elim (by omega)
+  | 0 => by omega
   | s' + 1 =>
     match hs' : s' with
     | 0 => aandRec x y 1 (by omega)

src/Init/Data/BitVec/Bootstrap.lean

@@ -8,10 +8,8 @@ module
 prelude
 public import Init.Data.BitVec.Basic
 import all Init.Data.BitVec.Basic
+import Init.Data.Int.Bitwise.Lemmas
 import Init.Ext
-import Init.ByCases
-import Init.Data.Nat.Div.Lemmas
-import Init.TacticsExtra
 
 public section
 

src/Init/Data/BitVec/Decidable.lean

@@ -7,11 +7,8 @@ Authors: Joe Hendrix, Harun Khan, Alex Keizer, Abdalrhman M Mohamed, Siddharth B
 module
 
 prelude
+public import Init.Data.BitVec.Bootstrap
 import Init.Ext
-public import Init.Data.BitVec.Basic
-public import Init.PropLemmas
-import Init.Classical
-import Init.Data.BitVec.Bootstrap
 
 public section
 

src/Init/Data/BitVec/Folds.lean

@@ -7,10 +7,8 @@ module
 
 prelude
 import all Init.Data.BitVec.Basic
-public import Init.Data.BitVec.Basic
-public import Init.Ext
-import Init.Data.BitVec.Lemmas
-import Init.Data.Fin.Iterate
+public import Init.Data.BitVec.Lemmas
+public import Init.Data.Fin.Iterate
 
 public section
 

src/Init/Data/BitVec/Lemmas.lean

@@ -9,20 +9,11 @@ prelude
 import all Init.Data.BitVec.Basic
 import all Init.Data.BitVec.BasicAux
 public import Init.Data.Fin.Lemmas
+public import Init.Data.Int.Bitwise.Lemmas
+public import Init.Data.Int.LemmasAux
+public import Init.Data.BitVec.Bootstrap
 public import Init.Data.List.BasicAux
 import Init.Data.List.Lemmas
-public import Init.Data.BitVec.Basic
-import Init.ByCases
-import Init.Data.BitVec.Bootstrap
-import Init.Data.Int.Bitwise.Lemmas
-import Init.Data.Int.DivMod.Lemmas
-import Init.Data.Int.LemmasAux
-import Init.Data.Int.Pow
-import Init.Data.Nat.Div.Lemmas
-import Init.Data.Nat.MinMax
-import Init.Data.Nat.Mod
-import Init.Data.Nat.Simproc
-import Init.TacticsExtra
 
 public section
 

src/Init/Data/ByteArray/Basic.lean

@@ -6,12 +6,9 @@ Author: Leonardo de Moura
 module
 
 prelude
+public import Init.Data.UInt.Basic
 import all Init.Data.UInt.BasicAux
-public import Init.Data.Array.DecidableEq
-public import Init.Data.List.Attach
-import Init.Data.Array.Bootstrap
-import Init.Data.Array.Lemmas
-import Init.Omega
+public import Init.Data.Array.Extract
 
 set_option doc.verso true
 

src/Init/Data/ByteArray/Extra.lean

@@ -7,8 +7,7 @@ module
 
 prelude
 public import Init.Data.ByteArray.Basic
-import Init.Data.String.Defs
-import Init.Data.UInt.Basic
+import Init.Data.String.Basic
 
 set_option doc.verso true
 

src/Init/Data/ByteArray/Lemmas.lean

@@ -7,11 +7,6 @@ module
 
 prelude
 public import Init.Data.ByteArray.Basic
-import Init.ByCases
-import Init.Data.Array.Bootstrap
-import Init.Data.Array.Extract
-import Init.Data.Array.Lemmas
-import Init.Omega
 
 public section
 
@@ -308,24 +303,4 @@ theorem ext_getElem {a b : ByteArray} (h₀ : a.size = b.size) (h : ∀ (i : Nat
   apply Array.ext (by simpa using h₀)
   simpa [← ByteArray.getElem_eq_getElem_data]
 
-@[simp]
-theorem _root_.List.toByteArray_inj {l l' : List UInt8} : l.toByteArray = l'.toByteArray ↔ l = l' := by
-  simp [ByteArray.ext_iff]
-
-theorem extract_eq_extract_iff_getElem {as bs : ByteArray} {i j len : Nat}
-    (hi : i + len ≤ as.size) (hj : j + len ≤ bs.size) :
-    as.extract i (i + len) = bs.extract j (j + len) ↔ ∀ k, (hk : k < len) → as[i + k] = bs[j + k] := by
-  induction len with
-  | zero => simp
-  | succ len ih =>
-    rw [← Nat.add_assoc, ← Nat.add_assoc, ByteArray.extract_eq_extract_append_extract (i + len) (by omega) (by omega),
-      ByteArray.extract_eq_extract_append_extract (a := bs) (j + len) (by omega) (by omega),
-      ByteArray.append_eq_append_iff_of_size_eq_left (by simp; omega), ih (by omega) (by omega),
-      ByteArray.extract_add_one (by omega), ByteArray.extract_add_one (by omega)]
-    simp only [List.toByteArray_inj, List.cons.injEq, and_true]
-    refine ⟨fun ⟨h, h'⟩ k hk => ?_, fun h => ⟨fun k hk => h k (by omega), h len (by omega)⟩⟩
-    by_cases hk' : k < len
-    · exact h k hk'
-    · exact (by omega : k = len) ▸ h'
-
 end ByteArray

src/Init/Data/Char/Basic.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Data.UInt.BasicAux
-import Init.Data.Nat.Div.Basic
 
 @[expose] public section
 
@@ -163,19 +162,16 @@ The lowercase ASCII letters are the following: `abcdefghijklmnopqrstuvwxyz`.
 -/
 @[inline]
 def toUpper (c : Char) : Char :=
-  if h : 'a'.val ≤ c.val ∧ c.val ≤ 'z'.val then
+  if h : c.val ≥ 'a'.val ∧ c.val ≤ 'z'.val then
     ⟨c.val + ('A'.val - 'a'.val), ?_⟩
   else
     c
 where finally
-  -- This expression is a ground non-value; generalize for better
-  -- control on where it is evaluated.
-  generalize hx : 'A'.val - 'a'.val = x
-  have h₁ : 2^32 ≤ c.val.toNat + x.toNat :=
-    @Nat.add_le_add 'a'.val.toNat _ (2^32 - 'a'.val.toNat) _ h.1 (by rw [← hx]; decide)
-  have h₂ : c.val.toBitVec.toNat + x.toNat < 2^32 + 0xd800 :=
-    Nat.add_lt_of_lt_sub (Nat.lt_of_le_of_lt h.2 (by rw [← hx]; decide))
-  have add_eq {x y : UInt32} : (x + y).toNat = (x.toNat + y.toNat) % 2^32 := id rfl
+  have h₁ : 2^32 ≤ c.val.toNat + ('A'.val - 'a'.val).toNat :=
+    @Nat.add_le_add 'a'.val.toNat _ (2^32 - 'a'.val.toNat) _ h.1 (by decide)
+  have h₂ : c.val.toBitVec.toNat + ('A'.val - 'a'.val).toNat < 2^32 + 0xd800 :=
+    Nat.add_lt_add_right (Nat.lt_of_le_of_lt h.2 (by decide)) _
+  have add_eq {x y : UInt32} : (x + y).toNat = (x.toNat + y.toNat) % 2^32 := rfl
   replace h₂ := Nat.sub_lt_left_of_lt_add h₁ h₂
   exact .inl <| lt_of_eq_of_lt (add_eq.trans (Nat.mod_eq_sub_mod h₁) |>.trans
     (Nat.mod_eq_of_lt (Nat.lt_trans h₂ (by decide)))) h₂

src/Init/Data/Char/Lemmas.lean

@@ -7,9 +7,7 @@ module
 
 prelude
 import all Init.Data.Char.Basic
-public import Init.Data.Char.Basic
-public import Init.Ext
-import Init.Data.UInt.Lemmas
+public import Init.Data.UInt.Lemmas
 
 public section
 
@@ -83,7 +81,6 @@ def notLTTotal : Std.Total (¬ · < · : Char → Char → Prop) where
 @[simp]
 theorem toUInt8_val {c : Char} : c.val.toUInt8 = c.toUInt8 := rfl
 
-@[simp]
 theorem toString_eq_singleton {c : Char} : c.toString = String.singleton c := rfl
 
 end Char

src/Init/Data/Char/Order.lean

@@ -8,9 +8,7 @@ module
 prelude
 public import Init.Data.Char.Basic
 import Init.Data.Char.Lemmas
-public import Init.Data.Order.Classes
-import Init.Data.Order.Factories
-import Init.PropLemmas
+public import Init.Data.Order.Factories
 
 open Std
 

src/Init/Data/Char/Ordinal.lean

@@ -7,18 +7,11 @@ module
 
 prelude
 public import Init.Data.Fin.OverflowAware
+public import Init.Data.UInt.Basic
 public import Init.Data.Function
 import Init.Data.Char.Lemmas
 import Init.Data.Char.Order
 import Init.Grind
-public import Init.Data.Char.Basic
-import Init.ByCases
-import Init.Data.Fin.Lemmas
-import Init.Data.Int.OfNat
-import Init.Data.Nat.Linear
-import Init.Data.Nat.Simproc
-import Init.Data.Option.Lemmas
-import Init.Data.UInt.Lemmas
 
 /-!
 # Bijection between `Char` and `Fin Char.numCodePoints`

src/Init/Data/Dyadic/Basic.lean

@@ -6,17 +6,9 @@ Authors: Kim Morrison, Robin Arnez
 module
 
 prelude
+public import Init.Data.Rat.Lemmas
 import Init.Data.Int.Bitwise.Lemmas
-public import Init.Data.Int.Bitwise.Basic
-public import Init.Data.Order.Classes
-public import Init.Data.Rat.Basic
-import Init.ByCases
-import Init.Data.Int.DivMod.Lemmas
-import Init.Data.Int.Pow
-import Init.Data.Nat.Bitwise.Lemmas
-import Init.Data.Option.Lemmas
-import Init.Data.Rat.Lemmas
-import Init.Omega
+import Init.Hints
 
 /-!
 # The dyadic rationals

src/Init/Data/Dyadic/Instances.lean

@@ -8,7 +8,6 @@ module
 prelude
 public import Init.Data.Dyadic.Basic
 public import Init.Grind.Ordered.Ring
-import Init.Data.Rat.Lemmas
 
 /-! # Internal `grind` algebra instances for `Dyadic`. -/
 

src/Init/Data/Dyadic/Inv.lean

@@ -7,7 +7,8 @@ module
 
 prelude
 public import Init.Data.Dyadic.Basic
-import Init.Data.Rat.Lemmas
+import Init.Data.Dyadic.Round
+import Init.Grind.Ordered.Ring
 
 /-!
 # Inversion for dyadic numbers

src/Init/Data/Dyadic/Round.lean

@@ -10,12 +10,6 @@ public import Init.Data.Dyadic.Basic
 import Init.Data.Dyadic.Instances
 import Init.Grind.Ordered.Rat
 import Init.Grind.Ordered.Field
-import Init.ByCases
-import Init.Data.Int.Bitwise.Lemmas
-import Init.Data.Int.DivMod.Lemmas
-import Init.Data.Int.Pow
-import Init.Data.Option.Lemmas
-import Init.Omega
 
 namespace Dyadic
 

src/Init/Data/Fin/Basic.lean

@@ -7,8 +7,6 @@ module
 
 prelude
 public import Init.Data.Nat.Bitwise.Basic
-public import Init.Data.Nat.Basic
-import Init.Data.Nat.Div.Basic
 
 public section
 

src/Init/Data/Fin/Bitwise.lean

@@ -6,9 +6,7 @@ Authors: Markus Himmel
 module
 
 prelude
-public import Init.Data.Fin.Basic
-import Init.Data.Nat.Bitwise.Lemmas
-import Init.Data.Nat.Div.Basic
+public import Init.Data.Nat.Bitwise
 
 public section
 

src/Init/Data/Fin/Fold.lean

@@ -7,12 +7,7 @@ module
 
 prelude
 public import Init.Control.Lawful.Basic
-public import Init.Ext
-import Init.Data.Fin.Lemmas
-import Init.Data.Nat.Lemmas
-import Init.Omega
-import Init.TacticsExtra
-import Init.WFTactics
+public import Init.Data.Fin.Lemmas
 
 public section
 

src/Init/Data/Fin/Iterate.lean

@@ -6,9 +6,7 @@ Authors: Joe Hendrix
 module
 
 prelude
-public import Init.Data.Fin.Basic
-import Init.PropLemmas
-import Init.WFTactics
+public import Init.PropLemmas
 
 public section
 

src/Init/Data/Fin/Lemmas.lean

@@ -6,15 +6,9 @@ Authors: Mario Carneiro, Leonardo de Moura
 module
 
 prelude
+public import Init.Data.Nat.Lemmas
 public import Init.Ext
-public import Init.Data.Nat.Div.Basic
-public import Init.Data.Order.Classes
-public import Init.NotationExtra
-import Init.ByCases
-import Init.Data.Nat.Lemmas
-import Init.Data.Nat.Linear
-import Init.Omega
-import Init.TacticsExtra
+import Init.Data.Order.Lemmas
 
 @[expose] public section
 
@@ -992,7 +986,7 @@ For the induction:
   let rec go (j : Nat) (h) (h2 : i ≤ j) (x : motive ⟨j, h⟩) : motive i :=
     if hi : i.1 = j then _root_.cast (by simp [← hi]) x
     else match j with
-      | 0 => False.elim (by omega)
+      | 0 => by omega
       | j + 1 => go j (by omega) (by omega) (cast ⟨j, by omega⟩ x)
   go _ _ (by omega) last
 

src/Init/Data/Fin/Log2.lean

@@ -6,8 +6,7 @@ Authors: Henrik Böving
 module
 
 prelude
-public import Init.Prelude
-import Init.Data.Nat.Log2
+public import Init.Data.Nat.Log2
 
 public section
 

src/Init/Data/FloatArray/Basic.lean

@@ -8,7 +8,7 @@ module
 prelude
 public import Init.Data.Float
 import Init.Ext
-public import Init.GetElem
+public import Init.Data.Array.DecidableEq
 
 public section
 universe u

src/Init/Data/Format/Basic.lean

@@ -6,10 +6,9 @@ Author: Leonardo de Moura
 module
 
 prelude
+public import Init.Control.State
 public import Init.Data.Int.Basic
 public import Init.Data.String.Bootstrap
-import Init.Control.State
-import Init.Data.Nat.Bitwise.Basic
 
 public section
 

src/Init/Data/Format/Instances.lean

@@ -6,9 +6,8 @@ Author: Leonardo de Moura
 module
 
 prelude
+public import Init.Data.Array.Basic
 import Init.Data.String.Search
-public import Init.Data.ToString.Basic
-import Init.Data.Iterators.Consumers.Collect
 
 public section
 

src/Init/Data/Format/Macro.lean

@@ -6,8 +6,8 @@ Author: Leonardo de Moura
 module
 
 prelude
-public meta import Init.Meta
-public import Init.Notation
+public import Init.Data.Format.Basic
+public import Init.Data.ToString.Macro
 
 public section
 

src/Init/Data/Format/Syntax.lean

@@ -6,10 +6,10 @@ Author: Leonardo de Moura
 module
 
 prelude
+public import Init.Data.Format.Macro
+public import Init.Data.Format.Instances
+public import Init.Meta
 import Init.Data.ToString.Name
-public import Init.Data.ToString.Basic
-import Init.Data.Format.Instances
-import Init.Data.Format.Macro
 
 public section
 

src/Init/Data/Hashable.lean

@@ -6,8 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.String.PosRaw
-public import Init.Data.UInt.Basic
+public import Init.Data.String.Basic
 
 public section
 universe u

src/Init/Data/Int/Basic.lean

@@ -9,7 +9,7 @@ module
 
 prelude
 public import Init.Data.Cast
-public import Init.Data.Nat.Basic
+public import Init.Data.Nat.Div.Basic
 
 public section
 

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

@@ -6,16 +6,10 @@ Authors: Siddharth Bhat, Jeremy Avigad
 module
 
 prelude
+public import Init.Data.Nat.Bitwise.Lemmas
 public import Init.Data.Int.Bitwise.Basic
 import all Init.Data.Int.Bitwise.Basic
-public import Init.Data.Int.DivMod.Basic
-import Init.ByCases
-import Init.Data.Int.DivMod.Lemmas
-import Init.Data.Int.Pow
-import Init.Data.Nat.Bitwise.Lemmas
-import Init.Data.Nat.Lemmas
-import Init.Omega
-import Init.RCases
+public import Init.Data.Int.DivMod.Lemmas
 
 public section