chore: fix test

This PR adds a new helper parser for implementing parsers that contain
hexadecimal numbers. We are going to use it to implement anchors in
the `grind` interactive mode.

.github/workflows/awaiting-manual.yml

@@ -12,7 +12,7 @@ jobs:
       - name: Check awaiting-manual label
         id: check-awaiting-manual-label
         if: github.event_name == 'pull_request'
-        uses: actions/github-script@v7
+        uses: actions/github-script@v8
         with:
           script: |
             const { labels, number: prNumber } = context.payload.pull_request;

.github/workflows/awaiting-mathlib.yml

@@ -12,7 +12,7 @@ jobs:
       - name: Check awaiting-mathlib label
         id: check-awaiting-mathlib-label
         if: github.event_name == 'pull_request'
-        uses: actions/github-script@v7
+        uses: actions/github-script@v8
         with:
           script: |
             const { labels, number: prNumber } = context.payload.pull_request;

.github/workflows/build-template.yml

@@ -116,10 +116,10 @@ jobs:
             build/stage1/**/*.ir
             build/stage1/**/*.c
             build/stage1/**/*.c.o*' || '' }}
-          key: ${{ matrix.name }}-build-v3-${{ github.sha }}
+          key: ${{ matrix.name }}-build-v4-${{ github.sha }}
           # fall back to (latest) previous cache
           restore-keys: |
-            ${{ matrix.name }}-build-v3
+            ${{ matrix.name }}-build-v4
       # open nix-shell once for initial setup
       - name: Setup
         run: |

.github/workflows/check-stage0.yml

@@ -31,7 +31,7 @@ jobs:
 
     - if: github.event_name == 'pull_request'
       name: Set label
-      uses: actions/github-script@v7
+      uses: actions/github-script@v8
       with:
         script: |
           const { owner, repo, number: issue_number  } = context.issue;

.github/workflows/ci.yml

@@ -137,7 +137,7 @@ jobs:
 
       - name: Configure build matrix
         id: set-matrix
-        uses: actions/github-script@v7
+        uses: actions/github-script@v8
         with:
           script: |
             const level = ${{ steps.set-level.outputs.check-level }};
@@ -213,7 +213,7 @@ jobs:
               },*/
               {
                 "name": "macOS",
-                "os": "macos-13",
+                "os": "macos-15-intel",
                 "release": true,
                 "check-level": 2,
                 "shell": "bash -euxo pipefail {0}",
@@ -226,7 +226,7 @@ jobs:
               {
                 "name": "macOS aarch64",
                 // standard GH runner only comes with 7GB so use large runner if possible when running tests
-                "os": large && !isPr ? "nscloud-macos-sonoma-arm64-6x14" : "macos-14",
+                "os": large && !isPr ? "nscloud-macos-sequoia-arm64-6x14" : "macos-15",
                 "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
                 "release": true,
                 "shell": "bash -euxo pipefail {0}",
@@ -350,7 +350,7 @@ jobs:
         content: |
           A build of `${{ github.ref_name }}`, triggered by event `${{ github.event_name }}`, [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}).
     - if: contains(needs.*.result, 'failure')
-      uses: actions/github-script@v7
+      uses: actions/github-script@v8
       with:
         script: |
             core.setFailed('Some jobs failed')
@@ -367,7 +367,7 @@ jobs:
         with:
           path: artifacts
       - name: Release
-        uses: softprops/action-gh-release@72f2c25fcb47643c292f7107632f7a47c1df5cd8
+        uses: softprops/action-gh-release@6cbd405e2c4e67a21c47fa9e383d020e4e28b836
         with:
           files: artifacts/*/*
           fail_on_unmatched_files: true
@@ -411,7 +411,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@72f2c25fcb47643c292f7107632f7a47c1df5cd8
+        uses: softprops/action-gh-release@6cbd405e2c4e67a21c47fa9e383d020e4e28b836
         with:
           body_path: diff.md
           prerelease: true

.github/workflows/grove.yml

@@ -110,7 +110,7 @@ jobs:
       # material.
       - id: deploy-alias
         if: ${{ steps.should-run.outputs.should-run == 'true' }}
-        uses: actions/github-script@v7
+        uses: actions/github-script@v8
         name: Compute Alias
         with:
           result-encoding: string

.github/workflows/labels-from-comments.yml

@@ -17,7 +17,7 @@ jobs:
 
     steps:
     - name: Add label based on comment
-      uses: actions/github-script@v7
+      uses: actions/github-script@v8
       with:
         github-token: ${{ secrets.GITHUB_TOKEN }}
         script: |

.github/workflows/pr-body.yml

@@ -11,7 +11,7 @@ jobs:
     steps:
       - name: Check PR body
         if: github.event_name == 'pull_request'
-        uses: actions/github-script@v7
+        uses: actions/github-script@v8
         with:
           script: |
             const { title, body, labels, draft } = context.payload.pull_request;

.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@72f2c25fcb47643c292f7107632f7a47c1df5cd8
+        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@72f2c25fcb47643c292f7107632f7a47c1df5cd8
+        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.
@@ -101,7 +101,7 @@ jobs:
 
       - name: Report release status (short format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: actions/github-script@v7
+        uses: actions/github-script@v8
         with:
           script: |
             await github.rest.repos.createCommitStatus({
@@ -115,7 +115,7 @@ jobs:
 
       - name: Report release status (SHA-suffixed format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: actions/github-script@v7
+        uses: actions/github-script@v8
         with:
           script: |
             await github.rest.repos.createCommitStatus({
@@ -129,7 +129,7 @@ jobs:
 
       - name: Add label
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: actions/github-script@v7
+        uses: actions/github-script@v8
         with:
           script: |
             await github.rest.issues.addLabels({
@@ -368,7 +368,7 @@ jobs:
 
       - name: Report mathlib base
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' }}
-        uses: actions/github-script@v7
+        uses: actions/github-script@v8
         with:
           script: |
             const description =

.github/workflows/pr-title.yml

@@ -10,7 +10,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Check PR title
-        uses: actions/github-script@v7
+        uses: actions/github-script@v8
         with:
           script: |
             const msg = context.payload.pull_request? context.payload.pull_request.title : context.payload.merge_group.head_commit.message;

.github/workflows/stale.yml

@@ -11,7 +11,7 @@ jobs:
   stale:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/stale@v9
+      - uses: actions/stale@v10
         with:
           days-before-stale: -1
           days-before-pr-stale: 30

.github/workflows/update-stage0.yml

@@ -69,10 +69,10 @@ jobs:
           build/stage1/**/*.ir
           build/stage1/**/*.c
           build/stage1/**/*.c.o*
-        key: Linux Lake-build-v3-${{ github.sha }}
+        key: Linux Lake-build-v4-${{ github.sha }}
         # fall back to (latest) previous cache
         restore-keys: |
-          Linux Lake-build-v3
+          Linux Lake-build-v4
     - if: env.should_update_stage0 == 'yes'
       # sync options with `Linux Lake` to ensure cache reuse
       run: |

doc/dev/testing.md

@@ -59,7 +59,7 @@ All these tests are included by [src/shell/CMakeLists.txt](https://github.com/le
     open Foo in
     theorem tst2 (h : a ≤ b) : a + 2 ≤ b + 2 :=
     Bla.
-      --^ textDocument/completion
+      --^ completion
     ```
     In this example, the test driver [`test_single.sh`](https://github.com/leanprover/lean4/tree/master/tests/lean/interactive/test_single.sh) will simulate an
     auto-completion request at `Bla.`. The expected output is stored in

flake.nix

@@ -25,6 +25,7 @@
         } ({
           buildInputs = with pkgs; [
             cmake gmp libuv ccache pkg-config
+            llvmPackages.bintools  # wrapped lld
             llvmPackages.llvm  # llvm-symbolizer for asan/lsan
             gdb
             tree  # for CI

lean.code-workspace

@@ -8,6 +8,9 @@
 		},
 		{
 			"path": "tests"
+		},
+		{
+			"path": "script"
 		}
 	],
 	"settings": {

script/Modulize.lean

@@ -0,0 +1,75 @@
+import Lake.CLI.Main
+
+/-!
+
+Usage: `lean --run script/Modulize.lean [--meta] file1.lean file2.lean ...`
+
+A simple script that inserts `module` and `public section` into un-modulized files and
+bumps their imports to `public`.
+
+When `--meta` is passed, `public meta section` and `public meta import` is used instead.
+-/
+
+open Lean Parser.Module
+
+def main (args : List String) : IO Unit := do
+  let mut args := args
+  let mut doMeta := false
+  while !args.isEmpty && args[0]!.startsWith "-" do
+    match args[0]! with
+    | "--meta" => doMeta := true
+    | arg => throw <| .userError s!"unknown flag '{arg}'"
+    args := args.tail
+
+  for path in args do
+    -- Parse the input file
+    let mut text ← IO.FS.readFile path
+    let inputCtx := Parser.mkInputContext text path
+    let (header, parserState, msgs) ← Parser.parseHeader inputCtx
+    if !msgs.toList.isEmpty then -- skip this file if there are parse errors
+      msgs.forM fun msg => msg.toString >>= IO.println
+      throw <| .userError "parse errors in file"
+    let `(header| $[module%$moduleTk?]? $imps:import*) := header
+      | throw <| .userError s!"unexpected header syntax of {path}"
+    if moduleTk?.isSome then
+      continue
+
+    -- initial whitespace if empty header
+    let startPos := header.raw.getPos? |>.getD parserState.pos
+
+    let dummyEnv ← mkEmptyEnvironment
+    let (initCmd, parserState', _) :=
+      Parser.parseCommand inputCtx { env := dummyEnv, options := {} } parserState msgs
+
+    -- insert section if any trailing command
+    if !initCmd.isOfKind ``Parser.Command.eoi then
+      let insertPos? :=
+          -- put below initial module docstring if any
+          guard (initCmd.isOfKind ``Parser.Command.moduleDoc) *> initCmd.getTailPos? <|>
+          -- else below header
+          header.raw.getTailPos?
+      let insertPos := insertPos?.getD startPos  -- empty header
+      let mut sec := if doMeta then
+        "public meta section"
+      else
+        "@[expose] public section"
+      if !imps.isEmpty then
+        sec := "\n\n" ++ sec
+      if insertPos?.isNone then
+        sec := sec ++ "\n\n"
+      text := text.extract 0 insertPos ++ sec ++ text.extract insertPos text.endPos
+
+    -- prepend each import with `public `
+    for imp in imps.reverse do
+      let insertPos := imp.raw.getPos?.get!
+      let prfx := if doMeta then "public meta " else "public "
+      text := text.extract 0 insertPos ++ prfx ++ text.extract insertPos text.endPos
+
+    -- insert `module` header
+    let mut initText := text.extract 0 startPos
+    if !initText.trim.isEmpty then
+      -- If there is a header comment, preserve it and put `module` in the line after
+      initText := initText.trimRight ++ "\n"
+    text := initText ++ "module\n\n" ++ text.extract startPos text.endPos
+
+    IO.FS.writeFile path text

script/Shake.lean

@@ -0,0 +1,584 @@
+/-
+Copyright (c) 2023 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, Sebastian Ullrich
+-/
+import Lake.CLI.Main
+import Lean.ExtraModUses
+
+/-! # `lake exe shake` command
+
+This command will check the current project (or a specified target module) and all dependencies for
+unused imports. This works by looking at generated `.olean` files to deduce required imports and
+ensuring that every import is used to contribute some constant or other elaboration dependency
+recorded by `recordExtraModUse`. Because recompilation is not needed this is quite fast (about 8
+seconds to check `Mathlib` and all dependencies).
+-/
+
+/-- help string for the command line interface -/
+def help : String := "Lean project tree shaking tool
+Usage: lake exe shake [OPTIONS] <MODULE>..
+
+Arguments:
+  <MODULE>
+    A module path like `Mathlib`. All files transitively reachable from the
+    provided module(s) will be checked.
+
+Options:
+  --force
+    Skips the `lake build --no-build` sanity check
+
+  --fix
+    Apply the suggested fixes directly. Make sure you have a clean checkout
+    before running this, so you can review the changes.
+"
+
+open Lean
+
+/-- We use `Nat` as a bitset for doing efficient set operations.
+The bit indexes will usually be a module index. -/
+structure Bitset where
+  toNat : Nat
+deriving Inhabited, DecidableEq, Repr
+
+namespace Bitset
+
+instance : EmptyCollection Bitset where
+  emptyCollection := { toNat := 0 }
+
+instance : Insert Nat Bitset where
+  insert i s := { toNat := s.toNat ||| (1 <<< i) }
+
+instance : Singleton Nat Bitset where
+  singleton i := insert i ∅
+
+instance : Inter Bitset where
+  inter a b := { toNat := a.toNat &&& b.toNat }
+
+instance : Union Bitset where
+  union a b := { toNat := a.toNat ||| b.toNat }
+
+instance : XorOp Bitset where
+  xor a b := { toNat := a.toNat ^^^ b.toNat }
+
+def has (s : Bitset) (i : Nat) : Bool := s ∩ {i} ≠ ∅
+
+end Bitset
+
+/-- The kind of a module dependency, corresponding to the homonymous `ExtraModUse` fields. -/
+structure NeedsKind where
+  isExported : Bool
+  isMeta : Bool
+deriving Inhabited, BEq, Repr, Hashable
+
+namespace NeedsKind
+
+@[match_pattern]  abbrev priv : NeedsKind := { isExported := false, isMeta := false }
+@[match_pattern]  abbrev pub  : NeedsKind := { isExported := true,  isMeta := false }
+@[match_pattern]  abbrev metaPriv : NeedsKind := { isExported := false, isMeta := true }
+@[match_pattern]  abbrev metaPub  : NeedsKind := { isExported := true,  isMeta := true }
+
+def all : Array NeedsKind := #[pub, priv, metaPub, metaPriv]
+
+def ofImport : Lean.Import → NeedsKind
+  | { isExported := true, isMeta := true, .. } => .metaPub
+  | { isExported := true, isMeta := false, .. } => .pub
+  | { isExported := false, isMeta := true, .. } => .metaPriv
+  | { isExported := false, isMeta := false, .. } => .priv
+
+end NeedsKind
+
+/-- Logically, a map `NeedsKind → Bitset`. -/
+structure Needs where
+  pub : Bitset
+  priv : Bitset
+  metaPub : Bitset
+  metaPriv : Bitset
+deriving Inhabited, Repr
+
+def Needs.empty : Needs := default
+
+def Needs.get (needs : Needs) (k : NeedsKind) : Bitset :=
+  match k with
+  | .pub => needs.pub
+  | .priv => needs.priv
+  | .metaPub => needs.metaPub
+  | .metaPriv => needs.metaPriv
+
+def Needs.has (needs : Needs) (k : NeedsKind) (i : ModuleIdx) : Bool :=
+  needs.get k |>.has i
+
+def Needs.set (needs : Needs) (k : NeedsKind) (s : Bitset) : Needs :=
+  match k with
+  | .pub   => { needs with pub := s }
+  | .priv  => { needs with priv := s }
+  | .metaPub => { needs with metaPub := s }
+  | .metaPriv => { needs with metaPriv := s }
+
+def Needs.modify (needs : Needs) (k : NeedsKind) (f : Bitset → Bitset) : Needs :=
+  needs.set k (f (needs.get k))
+
+def Needs.union (needs : Needs) (k : NeedsKind) (s : Bitset) : Needs :=
+  needs.modify k (· ∪ s)
+
+def Needs.sub (needs : Needs) (k : NeedsKind) (s : Bitset) : Needs :=
+  needs.modify k (fun s' => s' ^^^ (s' ∩ s))
+
+/-- The main state of the checker, containing information on all loaded modules. -/
+structure State where
+  env  : Environment
+  /--
+  `transDeps[i]` is the (non-reflexive) transitive closure of `mods[i].imports`. More specifically,
+  * `j ∈ transDeps[i].pub` if `i -(public import)->+ j`
+  * `j ∈ transDeps[i].priv` if `i -(import ...)-> _ -(public import)->* j`
+  * `j ∈ transDeps[i].priv` if `i -(import all)->+ -(public import ...)-> _ -(public import)->* j`
+  * `j ∈ transDeps[i].metaPub` if `i -(public (meta)? import)->* _ -(public meta import)-> _ -(public (meta)? import ...)->* j`
+  * `j ∈ transDeps[i].metaPriv` if `i -(meta import ...)-> _ -(public (meta)? import ...)->* j`
+  * `j ∈ transDeps[i].metaPriv` if `i -(import all)->+ -(public meta import ...)-> _ -(public (meta)? import ...)->* j`
+  -/
+  transDeps : Array Needs := #[]
+  /--
+  `transDepsOrig` is the initial value of `transDeps` before changes potentially resulting from
+  changes to upstream headers.
+  -/
+  transDepsOrig : Array Needs := #[]
+
+def State.mods (s : State) := s.env.header.moduleData
+def State.modNames (s : State) := s.env.header.moduleNames
+
+/--
+Given module `j`'s transitive dependencies, computes the union of `transImps` and the transitive
+dependencies resulting from importing the module via `imp` according to the rules of
+`State.transDeps`.
+-/
+def addTransitiveImps (transImps : Needs) (imp : Import) (j : Nat) (impTransImps : Needs) : Needs := Id.run do
+  let mut transImps := transImps
+
+  -- `j ∈ transDeps[i].pub` if `i -(public import)->+ j`
+  if imp.isExported && !imp.isMeta then
+    transImps := transImps.union .pub {j} |>.union .pub (impTransImps.get .pub)
+
+  if !imp.isExported && !imp.isMeta then
+    -- `j ∈ transDeps[i].priv` if `i -(import ...)-> _ -(public import)->* j`
+    transImps := transImps.union .priv {j} |>.union .priv (impTransImps.get .pub)
+    if imp.importAll then
+      -- `j ∈ transDeps[i].priv` if `i -(import all)->+ -(public import ...)-> _ -(public import)->* j`
+      transImps := transImps.union .priv (impTransImps.get .pub)
+
+  -- `j ∈ transDeps[i].metaPub` if `i -(public (meta)? import)->* _ -(public meta import)-> _ -(public (meta)? import ...)->* j`
+  if imp.isExported then
+    transImps := transImps.union .metaPub (impTransImps.get .metaPub)
+    if imp.isMeta then
+      transImps := transImps.union .metaPub {j} |>.union .metaPub (impTransImps.get .pub ∪ impTransImps.get .metaPub)
+
+  if !imp.isExported then
+    if imp.isMeta then
+      -- `j ∈ transDeps[i].metaPriv` if `i -(meta import ...)-> _ -(public (meta)? import ...)->* j`
+      transImps := transImps.union .metaPriv {j} |>.union .metaPriv (impTransImps.get .pub ∪ impTransImps.get .metaPub)
+    if imp.importAll then
+      -- `j ∈ transDeps[i].metaPriv` if `i -(import all)->+ -(public meta import ...)-> _ -(public (meta)? import ...)->* j`
+      transImps := transImps.union .metaPriv (impTransImps.get .metaPub)
+
+  transImps
+
+/-- Calculates the needs for a given module `mod` from constants and recorded extra uses. -/
+def calcNeeds (env : Environment) (i : ModuleIdx) : Needs := Id.run do
+  let mut needs := default
+  for ci in env.header.moduleData[i]!.constants do
+    let pubCI? := env.setExporting true |>.find? ci.name
+    let k := { isExported := pubCI?.isSome, isMeta := isMeta env ci.name }
+    needs := visitExpr k ci.type needs
+    if let some e := ci.value? (allowOpaque := true) then
+      -- type and value has identical visibility under `meta`
+      let k := if k.isMeta then k else
+        if pubCI?.any (·.hasValue (allowOpaque := true)) then .pub else .priv
+      needs := visitExpr k e needs
+
+  for use in getExtraModUses env i do
+    let j := env.getModuleIdx? use.module |>.get!
+    needs := needs.union { use with } {j}
+
+  return needs
+where
+  /-- Accumulate the results from expression `e` into `deps`. -/
+  visitExpr (k : NeedsKind) e deps :=
+    Lean.Expr.foldConsts e deps fun c deps => match env.getModuleIdxFor? c with
+      | some j =>
+        let k := { k with isMeta := k.isMeta && !isMeta env c }
+        if j != i then deps.union k {j} else deps
+      | _ => deps
+
+/--
+Calculates the same as `calcNeeds` but tracing each module to a use-def declaration pair or
+`none` if merely a recorded extra use.
+-/
+def getExplanations (env : Environment) (i : ModuleIdx) :
+    Std.HashMap (ModuleIdx × NeedsKind) (Option (Name × Name)) := Id.run do
+  let mut deps := default
+  for ci in env.header.moduleData[i]!.constants do
+    let pubCI? := env.setExporting true |>.find? ci.name
+    let k := { isExported := pubCI?.isSome, isMeta := isMeta env ci.name }
+    deps := visitExpr k ci.name ci.type deps
+    if let some e := ci.value? (allowOpaque := true) then
+      let k := if k.isMeta then k else
+        if pubCI?.any (·.hasValue (allowOpaque := true)) then .pub else .priv
+      deps := visitExpr k ci.name e deps
+
+  for use in getExtraModUses env i do
+    let j := env.getModuleIdx? use.module |>.get!
+    if !deps.contains (j, { use with }) then
+      deps := deps.insert (j, { use with }) none
+
+  return deps
+where
+  /-- Accumulate the results from expression `e` into `deps`. -/
+  visitExpr (k : NeedsKind) name e deps :=
+    Lean.Expr.foldConsts e deps fun c deps => match env.getModuleIdxFor? c with
+      | some i =>
+        let k := { k with isMeta := k.isMeta && !isMeta env c }
+        if
+          if let some (some (name', _)) := deps[(i, k)]? then
+            decide (name.toString.length < name'.toString.length)
+          else true
+        then
+          deps.insert (i, k) (name, c)
+        else
+          deps
+      | _ => deps
+
+partial def initStateFromEnv (env : Environment) : State := Id.run do
+  let mut s := { env }
+  for i in 0...env.header.moduleData.size do
+    let mod := env.header.moduleData[i]!
+    let mut imps := #[]
+    let mut transImps := Needs.empty
+    for imp in mod.imports do
+      let j := env.getModuleIdx? imp.module |>.get!
+      imps := imps.push j
+      transImps := addTransitiveImps transImps imp j s.transDeps[j]!
+    s := { s with transDeps := s.transDeps.push transImps }
+  s := { s with transDepsOrig := s.transDeps }
+  return s
+
+/-- The list of edits that will be applied in `--fix`. `edits[i] = (removed, added)` where:
+
+* If `j ∈ removed` then we want to delete module named `j` from the imports of `i`
+* If `j ∈ added` then we want to add module index `j` to the imports of `i`.
+-/
+abbrev Edits := Std.HashMap Name (Array Import × Array Import)
+
+/-- Register that we want to remove `tgt` from the imports of `src`. -/
+def Edits.remove (ed : Edits) (src : Name) (tgt : Import) : Edits :=
+  match ed.get? src with
+  | none => ed.insert src (#[tgt], #[])
+  | some (a, b) => ed.insert src (a.push tgt, b)
+
+/-- Register that we want to add `tgt` to the imports of `src`. -/
+def Edits.add (ed : Edits) (src : Name) (tgt : Import) : Edits :=
+  match ed.get? src with
+  | none => ed.insert src (#[], #[tgt])
+  | some (a, b) => ed.insert src (a, b.push tgt)
+
+/-- Parse a source file to extract the location of the import lines, for edits and error messages.
+
+Returns `(path, inputCtx, imports, endPos)` where `imports` is the `Lean.Parser.Module.import` list
+and `endPos` is the position of the end of the header.
+-/
+def parseHeaderFromString (text path : String) :
+    IO (System.FilePath × Parser.InputContext ×
+      TSyntaxArray ``Parser.Module.import × String.Pos) := do
+  let inputCtx := Parser.mkInputContext text path
+  let (header, parserState, msgs) ← Parser.parseHeader inputCtx
+  if !msgs.toList.isEmpty then -- skip this file if there are parse errors
+    msgs.forM fun msg => msg.toString >>= IO.println
+    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.endPos insertion + ⟨1⟩
+  pure (path, inputCtx, .mk header.raw[2].getArgs, insertion)
+
+/-- Parse a source file to extract the location of the import lines, for edits and error messages.
+
+Returns `(path, inputCtx, imports, endPos)` where `imports` is the `Lean.Parser.Module.import` list
+and `endPos` is the position of the end of the header.
+-/
+def parseHeader (srcSearchPath : SearchPath) (mod : Name) :
+    IO (System.FilePath × Parser.InputContext ×
+      TSyntaxArray ``Parser.Module.import × String.Pos) := do
+  -- Parse the input file
+  let some path ← srcSearchPath.findModuleWithExt "lean" mod
+    | throw <| .userError s!"error: failed to find source file for {mod}"
+  let text ← IO.FS.readFile path
+  parseHeaderFromString text path.toString
+
+def decodeImport : TSyntax ``Parser.Module.import → Import
+  | `(Parser.Module.import| $[public%$pubTk?]? $[meta%$metaTk?]? import $[all%$allTk?]? $id) =>
+    { module := id.getId, isExported := pubTk?.isSome, isMeta := metaTk?.isSome, importAll := allTk?.isSome }
+  | stx => panic! s!"unexpected syntax {stx}"
+
+/-- Analyze and report issues from module `i`. Arguments:
+
+* `srcSearchPath`: Used to find the path for error reporting purposes
+* `i`: the module index
+* `needs`: the module's calculated needs
+* `pinned`: dependencies that should be preserved even if unused
+* `edits`: accumulates the list of edits to apply if `--fix` is true
+* `addOnly`: if true, only add missing imports, do not remove unused ones
+-/
+def visitModule (srcSearchPath : SearchPath)
+    (i : Nat) (needs : Needs) (preserve : Needs) (edits : Edits)
+    (addOnly := false) (githubStyle := false) (explain := false) : StateT State IO Edits := do
+  let s ← get
+  -- Do transitive reduction of `needs` in `deps`.
+  let mut deps := needs
+  for j in [0:s.mods.size] do
+    let transDeps := s.transDeps[j]!
+    for k in NeedsKind.all do
+      if s.transDepsOrig[i]!.has k j && preserve.has k j then
+        deps := deps.union k {j}
+      if deps.has k j then
+        let transDeps := addTransitiveImps .empty { k with module := .anonymous } j transDeps
+        for k' in NeedsKind.all do
+          deps := deps.sub k' (transDeps.sub k' {j} |>.get k')
+
+  -- Any import which is not in `transDeps` was unused.
+  -- Also accumulate `newDeps` which is the transitive closure of the remaining imports
+  let mut toRemove : Array Import := #[]
+  let mut newDeps := Needs.empty
+  for imp in s.mods[i]!.imports do
+    let j := s.env.getModuleIdx? imp.module |>.get!
+    if
+        -- skip folder-nested imports
+        s.modNames[i]!.isPrefixOf imp.module ||
+        imp.importAll then
+      newDeps := addTransitiveImps newDeps imp j s.transDeps[j]!
+    else
+      let k := NeedsKind.ofImport imp
+      if !addOnly && !deps.has k j && !deps.has { k with isExported := false } j then
+        toRemove := toRemove.push imp
+      else
+        newDeps := addTransitiveImps newDeps imp j s.transDeps[j]!
+
+  -- If `newDeps` does not cover `deps`, then we have to add back some imports until it does.
+  -- To minimize new imports we pick only new imports which are not transitively implied by
+  -- another new import
+  let mut toAdd : Array Import := #[]
+  for j in [0:s.mods.size] do
+    for k in NeedsKind.all do
+      if deps.has k j && !newDeps.has k j && !newDeps.has { k with isExported := true } j then
+        let imp := { k with module := s.modNames[j]! }
+        toAdd := toAdd.push imp
+        newDeps := addTransitiveImps newDeps imp j s.transDeps[j]!
+
+  -- mark and report the removals
+  let mut edits := toRemove.foldl (init := edits) fun edits imp =>
+    edits.remove s.modNames[i]! imp
+
+  if !toAdd.isEmpty || !toRemove.isEmpty || explain then
+    if let some path ← srcSearchPath.findModuleWithExt "lean" s.modNames[i]! then
+      println! "{path}:"
+    else
+      println! "{s.modNames[i]!}:"
+
+  if !toRemove.isEmpty then
+    println! "  remove {toRemove}"
+
+  if githubStyle then
+    try
+      let (path, inputCtx, imports, endHeader) ← parseHeader srcSearchPath s.modNames[i]!
+      for stx in imports do
+        if toRemove.any fun imp => imp == decodeImport stx then
+          let pos := inputCtx.fileMap.toPosition stx.raw.getPos?.get!
+          println! "{path}:{pos.line}:{pos.column+1}: warning: unused import \
+            (use `lake exe shake --fix` to fix this, or `lake exe shake --update` to ignore)"
+      if !toAdd.isEmpty then
+        -- we put the insert message on the beginning of the last import line
+        let pos := inputCtx.fileMap.toPosition endHeader
+        println! "{path}:{pos.line-1}:1: warning: \
+          add {toAdd} instead"
+    catch _ => pure ()
+
+  -- mark and report the additions
+  edits := toAdd.foldl (init := edits) fun edits imp =>
+    edits.add s.modNames[i]! imp
+
+  if !toAdd.isEmpty then
+    println! "  add {toAdd}"
+
+  -- recalculate transitive dependencies of downstream modules
+  let mut newTransDepsI := Needs.empty
+  for imp in s.mods[i]!.imports do
+    if !toRemove.contains imp then
+      let j := s.env.getModuleIdx? imp.module |>.get!
+      newTransDepsI := addTransitiveImps newTransDepsI imp j s.transDeps[j]!
+  for imp in toAdd do
+    let j := s.env.getModuleIdx? imp.module |>.get!
+    newTransDepsI := addTransitiveImps newTransDepsI imp j s.transDeps[j]!
+
+  set { s with transDeps := s.transDeps.set! i newTransDepsI }
+
+  if explain then
+    let explanation := getExplanations s.env i
+    let sanitize n := if n.hasMacroScopes then (sanitizeName n).run' { options := {} } else n
+    let run (imp : Import) := do
+      let j := s.env.getModuleIdx? imp.module |>.get!
+      if let some exp? := explanation[(j, NeedsKind.ofImport imp)]? then
+        println! "  note: `{imp}` required"
+        if let some (n, c) := exp? then
+          println! "    because `{sanitize n}` refers to `{sanitize c}`"
+        else
+          println! "    because of additional compile-time dependencies"
+    for j in s.mods[i]!.imports do
+      if !toRemove.contains j then
+        run j
+    for i in toAdd do run i
+
+  return edits
+
+/-- Convert a list of module names to a bitset of module indexes -/
+def toBitset (s : State) (ns : List Name) : Bitset :=
+  ns.foldl (init := ∅) fun c name =>
+    match s.env.getModuleIdxFor? name with
+    | some i => c ∪ {i}
+    | none => c
+
+/-- The parsed CLI arguments. See `help` for more information -/
+structure Args where
+  /-- `--help`: shows the help -/
+  help : Bool := false
+  /-- `--force`: skips the `lake build --no-build` sanity check -/
+  force : Bool := false
+  /-- `--gh-style`: output messages that can be parsed by `gh-problem-matcher-wrap` -/
+  githubStyle : Bool := false
+  /-- `--explain`: give constants explaining why each module is needed -/
+  explain : Bool := false
+  /-- `--fix`: apply the fixes directly -/
+  fix : Bool := false
+  /-- `<MODULE>..`: the list of root modules to check -/
+  mods : Array Name := #[]
+
+local instance : Ord Import where
+  compare a b :=
+    if a.isExported && !b.isExported then
+      Ordering.lt
+    else if !a.isExported && b.isExported then
+      Ordering.gt
+    else
+      a.module.cmp b.module
+
+/-- The main entry point. See `help` for more information on arguments. -/
+def main (args : List String) : IO UInt32 := do
+  initSearchPath (← findSysroot)
+  -- Parse the arguments
+  let rec parseArgs (args : Args) : List String → Args
+    | [] => args
+    | "--help" :: rest => parseArgs { args with help := true } rest
+    | "--force" :: rest => parseArgs { args with force := true } rest
+    | "--fix" :: rest => parseArgs { args with fix := true } rest
+    | "--explain" :: rest => parseArgs { args with explain := true } rest
+    | "--gh-style" :: rest => parseArgs { args with githubStyle := true } rest
+    | "--" :: rest => { args with mods := args.mods ++ rest.map (·.toName) }
+    | other :: rest => parseArgs { args with mods := args.mods.push other.toName } rest
+  let args := parseArgs {} args
+
+  -- Bail if `--help` is passed
+  if args.help then
+    IO.println help
+    IO.Process.exit 0
+
+  if !args.force then
+    if (← IO.Process.output { cmd := "lake", args := #["build", "--no-build"] }).exitCode != 0 then
+      IO.println "There are out of date oleans. Run `lake build` or `lake exe cache get` first"
+      IO.Process.exit 1
+
+  -- Determine default module(s) to run shake on
+  let defaultTargetModules : Array Name ← try
+    let (elanInstall?, leanInstall?, lakeInstall?) ← Lake.findInstall?
+    let config ← Lake.MonadError.runEIO <| Lake.mkLoadConfig { elanInstall?, leanInstall?, lakeInstall? }
+    let some workspace ← Lake.loadWorkspace config |>.toBaseIO
+      | throw <| IO.userError "failed to load Lake workspace"
+    let defaultTargetModules := workspace.root.defaultTargets.flatMap fun target =>
+      if let some lib := workspace.root.findLeanLib? target then
+        lib.roots
+      else if let some exe := workspace.root.findLeanExe? target then
+        #[exe.config.root]
+      else
+        #[]
+    pure defaultTargetModules
+  catch _ =>
+    pure #[]
+
+  let srcSearchPath ← getSrcSearchPath
+  -- the list of root modules
+  let mods := if args.mods.isEmpty then defaultTargetModules else args.mods
+  -- Only submodules of `pkg` will be edited or have info reported on them
+  let pkg := mods[0]!.components.head!
+
+  -- Load all the modules
+  let imps := mods.map ({ module := · })
+  let (_, s) ← importModulesCore imps (isExported := true) |>.run
+  let s := s.markAllExported
+  let env ← finalizeImport s (isModule := true) imps {} (leakEnv := false) (loadExts := false)
+
+  StateT.run' (s := initStateFromEnv env) do
+
+  let s ← get
+  -- Parse the config file
+
+  -- Run the calculation of the `needs` array in parallel
+  let needs := s.mods.mapIdx fun i _ =>
+    Task.spawn fun _ => calcNeeds s.env i
+
+  if args.fix then
+    println! "The following changes will be made automatically:"
+
+  -- Check all selected modules
+  let mut edits : Edits := ∅
+  let mut revNeeds : Needs := default
+  for i in [0:s.mods.size], t in needs do
+    edits ← visitModule (addOnly := !pkg.isPrefixOf s.modNames[i]!) srcSearchPath i t.get revNeeds edits args.githubStyle args.explain
+    if isExtraRevModUse s.env i then
+      revNeeds := revNeeds.union .priv {i}
+
+  if !args.fix then
+    -- return error if any issues were found
+    return if edits.isEmpty then 0 else 1
+
+  -- Apply the edits to existing files
+  let count ← edits.foldM (init := 0) fun count mod (remove, add) => do
+    let add : Array Import := add.qsortOrd
+
+    -- Parse the input file
+    let (path, inputCtx, imports, insertion) ←
+      try parseHeader srcSearchPath mod
+      catch e => println! e.toString; return count
+    let text := inputCtx.fileMap.source
+
+    -- Calculate the edit result
+    let mut pos : String.Pos := 0
+    let mut out : String := ""
+    let mut seen : Std.HashSet Import := {}
+    for stx in imports do
+      let mod := decodeImport stx
+      if remove.contains mod || seen.contains mod then
+        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.endPos stx.raw.getTailPos?.get! + ⟨1⟩
+      seen := seen.insert mod
+    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 ++ text.extract insertion text.endPos
+
+    IO.FS.writeFile path out
+    return count + 1
+
+  -- Since we throw an error upon encountering issues, we can be sure that everything worked
+  -- if we reach this point of the script.
+  if count > 0 then
+    println! "Successfully applied {count} suggestions."
+  else
+    println! "No edits required."
+  return 0

script/lakefile.toml

@@ -0,0 +1,9 @@
+name = "scripts"
+
+[[lean_exe]]
+name = "modulize"
+root = "Modulize"
+
+[[lean_exe]]
+name = "shake"
+root = "Shake"

script/lean-toolchain

@@ -0,0 +1 @@
+lean4

src/CMakeLists.txt

@@ -34,7 +34,14 @@ if (NOT LEAN_PLATFORM_TARGET)
     OUTPUT_VARIABLE LEAN_PLATFORM_TARGET OUTPUT_STRIP_TRAILING_WHITESPACE)
 endif()
 
-set(LEAN_EXTRA_LINKER_FLAGS "" CACHE STRING "Additional flags used by the linker")
+set(LEAN_EXTRA_LINKER_FLAGS_DEFAULT "")
+# Use lld by default, if available
+find_program(LLD_PATH lld)
+if(LLD_PATH)
+  string(APPEND LEAN_EXTRA_LINKER_FLAGS_DEFAULT " -fuse-ld=lld")
+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")
 set(LEAN_TEST_VARS "LEAN_CC=${CMAKE_C_COMPILER}" CACHE STRING "Additional environment variables used when running tests")
 
@@ -82,6 +89,7 @@ option(USE_MIMALLOC "use mimalloc" ON)
 # development-specific options
 option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current version of Lean" OFF)
 option(USE_LAKE "Use Lake instead of lean.mk for building core libs from language server" ON)
+option(USE_LAKE_CACHE "Use the Lake artifact cache for stage 1 builds (requires USE_LAKE)" OFF)
 
 set(LEAN_EXTRA_MAKE_OPTS  ""                           CACHE STRING "extra options to lean --make")
 set(LEANC_CC              ${CMAKE_C_COMPILER}          CACHE STRING "C compiler to use in `leanc`")
@@ -797,6 +805,9 @@ install(DIRECTORY "${CMAKE_BINARY_DIR}/lib/" DESTINATION lib
 
 # symlink source into expected installation location for go-to-definition, if file system allows it
 file(MAKE_DIRECTORY ${CMAKE_BINARY_DIR}/src)
+# get rid of all files in `src/lean` that may have been loaded from the cache
+# (at the time of writing this, this is the case for some lake test .c files)
+file(REMOVE_RECURSE ${CMAKE_BINARY_DIR}/src/lean)
 if(${STAGE} EQUAL 0)
   file(CREATE_LINK ${CMAKE_SOURCE_DIR}/../../src ${CMAKE_BINARY_DIR}/src/lean RESULT _IGNORE_RES SYMBOLIC)
 else()
@@ -823,10 +834,13 @@ if(LEAN_INSTALL_PREFIX)
   set(CMAKE_INSTALL_PREFIX "${LEAN_INSTALL_PREFIX}/lean-${LEAN_VERSION_STRING}${LEAN_INSTALL_SUFFIX}")
 endif()
 
-if (STAGE GREATER 1)
+
+if (USE_LAKE_CACHE AND STAGE EQUAL 1)
+  set(LAKE_ARTIFACT_CACHE_TOML "true")
+else()
   # The build of stage2+ may depend on local changes made to src/ that are not reflected by the
   # commit hash in stage1/bin/lean, so we make sure to disable the global cache
-  string(APPEND LEAN_EXTRA_LAKEFILE_TOML "\n\nenableArtifactCache = false")
+  set(LAKE_ARTIFACT_CACHE_TOML "false")
 endif()
 
 # Escape for `make`. Yes, twice.
@@ -844,15 +858,13 @@ endfunction()
 string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_CC "${LEANC_CC}")
 string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_INTERNAL_FLAGS "${LEANC_INTERNAL_FLAGS}")
 string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_INTERNAL_LINKER_FLAGS "${LEANC_INTERNAL_LINKER_FLAGS}")
-set(LEANC_OPTS_TOML "${LEANC_OPTS} ${LEANC_EXTRA_CC_FLAGS} ${LEANC_INTERNAL_FLAGS}")
-set(LINK_OPTS_TOML "${LEANC_INTERNAL_LINKER_FLAGS} -L${CMAKE_BINARY_DIR}/lib/lean ${LEAN_EXTRA_LINKER_FLAGS}")
 
 toml_escape("${LEAN_EXTRA_MAKE_OPTS}" LEAN_EXTRA_OPTS_TOML)
-toml_escape("${LEANC_OPTS_TOML}" LEANC_OPTS_TOML)
-toml_escape("${LINK_OPTS_TOML}" LINK_OPTS_TOML)
 
-if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
-  set(LAKE_LIB_PREFIX "lib")
+if(${CMAKE_BUILD_TYPE} MATCHES "Debug|Release|RelWithDebInfo|MinSizeRel")
+  set(CMAKE_BUILD_TYPE_TOML "${CMAKE_BUILD_TYPE}")
+else()
+  set(CMAKE_BUILD_TYPE_TOML "Release")
 endif()
 
 if(USE_LAKE)

src/Init/Classical.lean

@@ -8,7 +8,7 @@ module
 prelude
 public import Init.PropLemmas
 
-public section
+@[expose] public section
 
 universe u v
 

src/Init/Control.lean

@@ -16,5 +16,3 @@ public import Init.Control.Option
 public import Init.Control.Lawful
 public import Init.Control.StateCps
 public import Init.Control.ExceptCps
-
-public section

src/Init/Control/Lawful.lean

@@ -10,5 +10,3 @@ public import Init.Control.Lawful.Basic
 public import Init.Control.Lawful.Instances
 public import Init.Control.Lawful.Lemmas
 public import Init.Control.Lawful.MonadLift
-
-public section

src/Init/Control/Lawful/Instances.lean

@@ -9,6 +9,8 @@ prelude
 public import Init.Control.Lawful.Basic
 public import Init.Control.Except
 import all Init.Control.Except
+public import Init.Control.Option
+import all Init.Control.Option
 public import Init.Control.State
 import all Init.Control.State
 public import Init.Control.StateRef
@@ -110,6 +112,121 @@ instance : LawfulMonad (Except ε) := LawfulMonad.mk'
 instance : LawfulApplicative (Except ε) := inferInstance
 instance : LawfulFunctor (Except ε) := inferInstance
 
+/-! # OptionT -/
+
+namespace OptionT
+
+@[ext] theorem ext {x y : OptionT m α} (h : x.run = y.run) : x = y := by
+  simp [run] at h
+  assumption
+
+@[simp, grind =] theorem run_mk {m : Type u → Type v} (x : m (Option α)) :
+    OptionT.run (OptionT.mk x) = x := by rfl
+
+@[simp, grind =] theorem run_pure [Monad m] (x : α) : run (pure x : OptionT m α) = pure (some x) := by
+  simp [run, pure, OptionT.pure, OptionT.mk]
+
+@[simp, grind =] theorem run_lift  [Monad.{u, v} m] (x : m α) : run (OptionT.lift x : OptionT m α) = (return some (← x) : m (Option α)) := by
+  simp [run, OptionT.lift, OptionT.mk]
+
+@[simp, grind =] theorem run_throw [Monad m] : run (throw e : OptionT m β) = pure none := by
+  simp [run, throw, throwThe, MonadExceptOf.throw, OptionT.fail, OptionT.mk]
+
+@[simp, grind =] theorem run_bind_lift [Monad m] [LawfulMonad m] (x : m α) (f : α → OptionT m β) : run (OptionT.lift x >>= f : OptionT m β) = x >>= fun a => run (f a) := by
+  simp [OptionT.run, OptionT.lift, bind, OptionT.bind, OptionT.mk]
+
+@[simp, grind =] theorem bind_throw [Monad m] [LawfulMonad m] (f : α → OptionT m β) : (throw e >>= f) = throw e := by
+  simp [throw, throwThe, MonadExceptOf.throw, bind, OptionT.bind, OptionT.mk, OptionT.fail]
+
+@[simp, grind =] theorem run_bind (f : α → OptionT m β) [Monad m] :
+    (x >>= f).run = Option.elimM x.run (pure none) (fun x => (f x).run) := by
+  change x.run >>= _ = _
+  simp [Option.elimM]
+  exact bind_congr fun |some _ => rfl | none => rfl
+
+@[simp, grind =] theorem lift_pure [Monad m] [LawfulMonad m] {α : Type u} (a : α) : OptionT.lift (pure a : m α) = pure a := by
+  simp only [OptionT.lift, OptionT.mk, bind_pure_comp, map_pure, pure, OptionT.pure]
+
+@[simp, grind =] theorem run_map [Monad m] [LawfulMonad m] (f : α → β) (x : OptionT m α)
+    : (f <$> x).run = Option.map f <$> x.run := by
+  simp [Functor.map, Option.map, ←bind_pure_comp]
+  apply bind_congr
+  intro a; cases a <;> simp [OptionT.pure, OptionT.mk]
+
+protected theorem seq_eq {α β : Type u} [Monad m] (mf : OptionT m (α → β)) (x : OptionT m α) : mf <*> x = mf >>= fun f => f <$> x :=
+  rfl
+
+protected theorem bind_pure_comp [Monad m] (f : α → β) (x : OptionT m α) : x >>= pure ∘ f = f <$> x := by
+  intros; rfl
+
+protected theorem seqLeft_eq {α β : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (x : OptionT m α) (y : OptionT m β) : x <* y = const β <$> x <*> y := by
+  change (x >>= fun a => y >>= fun _ => pure a) = (const (α := α) β <$> x) >>= fun f => f <$> y
+  rw [← OptionT.bind_pure_comp]
+  apply ext
+  simp [Option.elimM, Option.elim]
+  apply bind_congr
+  intro
+  | none => simp
+  | some _ =>
+    simp [←bind_pure_comp]; apply bind_congr; intro b;
+    cases b <;> simp [const]
+
+protected theorem seqRight_eq [Monad m] [LawfulMonad m] (x : OptionT m α) (y : OptionT m β) : x *> y = const α id <$> x <*> y := by
+  change (x >>= fun _ => y) = (const α id <$> x) >>= fun f => f <$> y
+  rw [← OptionT.bind_pure_comp]
+  apply ext
+  simp [Option.elimM, Option.elim]
+  apply bind_congr
+  intro a; cases a <;> simp
+
+instance [Monad m] [LawfulMonad m] : LawfulMonad (OptionT m) where
+  id_map         := by intros; apply ext; simp
+  map_const      := by intros; rfl
+  seqLeft_eq     := OptionT.seqLeft_eq
+  seqRight_eq    := OptionT.seqRight_eq
+  pure_seq       := by intros; apply ext; simp [OptionT.seq_eq, Option.elimM, Option.elim]
+  bind_pure_comp := OptionT.bind_pure_comp
+  bind_map       := by intros; rfl
+  pure_bind      := by intros; apply ext; simp [Option.elimM, Option.elim]
+  bind_assoc     := by intros; apply ext; simp [Option.elimM, Option.elim]; apply bind_congr; intro a; cases a <;> simp
+
+@[simp] theorem run_seq [Monad m] [LawfulMonad m] (f : OptionT m (α → β)) (x : OptionT m α) :
+    (f <*> x).run = Option.elimM f.run (pure none) (fun f => Option.map f <$> x.run) := by
+  simp [seq_eq_bind, Option.elimM, Option.elim]
+
+@[simp] theorem run_seqLeft [Monad m] [LawfulMonad m] (x : OptionT m α) (y : OptionT m β) :
+    (x <* y).run = Option.elimM x.run (pure none)
+      (fun x => Option.map (Function.const β x) <$> y.run) := by
+  simp [seqLeft_eq, seq_eq_bind, Option.elimM, OptionT.run_bind]
+
+@[simp] theorem run_seqRight [Monad m] [LawfulMonad m] (x : OptionT m α) (y : OptionT m β) :
+    (x *> y).run = Option.elimM x.run (pure none) (Function.const α y.run) := by
+  simp only [seqRight_eq, run_seq, Option.elimM, run_map, Option.elim, bind_map_left]
+  refine bind_congr (fun | some _ => by simp | none => by simp)
+
+@[simp, grind =] theorem run_failure [Monad m] : (failure : OptionT m α).run = pure none := by rfl
+
+@[simp] theorem map_failure [Monad m] [LawfulMonad m] {α β : Type _} (f : α → β) :
+    f <$> (failure : OptionT m α) = (failure : OptionT m β) := by
+  simp [OptionT.mk, Functor.map, Alternative.failure, OptionT.fail, OptionT.bind]
+
+@[simp] theorem run_orElse [Monad m] (x : OptionT m α) (y : OptionT m α) :
+    (x <|> y).run = Option.elimM x.run y.run (fun x => pure (some x)) :=
+  bind_congr fun | some _ => by rfl | none => by rfl
+
+end OptionT
+
+/-! # Option -/
+
+instance : LawfulMonad Option := LawfulMonad.mk'
+  (id_map := fun x => by cases x <;> rfl)
+  (pure_bind := fun _ _ => by rfl)
+  (bind_assoc := fun a _ _ => by cases a <;> rfl)
+  (bind_pure_comp := bind_pure_comp)
+
+instance : LawfulApplicative Option := inferInstance
+instance : LawfulFunctor Option := inferInstance
+
 /-! # ReaderT -/
 
 namespace ReaderT

src/Init/Control/Lawful/MonadLift.lean

@@ -9,5 +9,3 @@ prelude
 public import Init.Control.Lawful.MonadLift.Basic
 public import Init.Control.Lawful.MonadLift.Lemmas
 public import Init.Control.Lawful.MonadLift.Instances
-
-public section

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

@@ -64,10 +64,6 @@ namespace OptionT
 
 variable [Monad m] [LawfulMonad m]
 
-@[simp]
-theorem lift_pure {α : Type u} (a : α) : OptionT.lift (pure a : m α) = pure a := by
-  simp only [OptionT.lift, OptionT.mk, bind_pure_comp, map_pure, pure, OptionT.pure]
-
 @[simp]
 theorem lift_bind {α β : Type u} (ma : m α) (f : α → m β) :
     OptionT.lift (ma >>= f) = OptionT.lift ma >>= (fun a => OptionT.lift (f a)) := by

src/Init/Control/Option.lean

@@ -39,13 +39,14 @@ variable {m : Type u → Type v} [Monad m] {α β : Type u}
 Converts an action that returns an `Option` into one that might fail, with `none` indicating
 failure.
 -/
+@[always_inline, inline, expose]
 protected def mk (x : m (Option α)) : OptionT m α :=
   x
 
 /--
 Sequences two potentially-failing actions. The second action is run only if the first succeeds.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 protected def bind (x : OptionT m α) (f : α → OptionT m β) : OptionT m β := OptionT.mk do
   match (← x) with
   | some a => f a
@@ -54,7 +55,7 @@ protected def bind (x : OptionT m α) (f : α → OptionT m β) : OptionT m β :
 /--
 Succeeds with the provided value.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 protected def pure (a : α) : OptionT m α := OptionT.mk do
   pure (some a)
 

src/Init/Core.lean

@@ -144,8 +144,9 @@ Computed values are cached, so the value is not recomputed.
   x.fn ()
 
 -- Ensure `Thunk.fn` is still computable even if it shouldn't be accessed directly.
-@[inline] private def Thunk.fnImpl (x : Thunk α) : Unit → α := fun _ => x.get
-@[csimp] private theorem Thunk.fn_eq_fnImpl : @Thunk.fn = @Thunk.fnImpl := rfl
+/-- Implementation detail. -/
+@[inline] def Thunk.fnImpl (x : Thunk α) : Unit → α := fun _ => x.get
+@[csimp] theorem Thunk.fn_eq_fnImpl : @Thunk.fn = @Thunk.fnImpl := rfl
 
 /--
 Constructs a new thunk that forces `x` and then applies `x` to the result. Upon forcing, the result
@@ -1605,7 +1606,7 @@ gen_injective_theorems% PSigma
 gen_injective_theorems% PSum
 gen_injective_theorems% Sigma
 gen_injective_theorems% String
-gen_injective_theorems% String.Pos
+gen_injective_theorems% String.Pos.Raw
 gen_injective_theorems% Substring
 gen_injective_theorems% Subtype
 gen_injective_theorems% Sum

src/Init/Data.lean

@@ -30,6 +30,7 @@ public import Init.Data.Random
 public import Init.Data.ToString
 public import Init.Data.Range
 public import Init.Data.Hashable
+public import Init.Data.LawfulHashable
 public import Init.Data.OfScientific
 public import Init.Data.Format
 public import Init.Data.Stream
@@ -52,5 +53,3 @@ public import Init.Data.Slice
 public import Init.Data.Order
 public import Init.Data.Rat
 public import Init.Data.Dyadic
-
-public section

src/Init/Data/Array.lean

@@ -30,5 +30,3 @@ public import Init.Data.Array.Erase
 public import Init.Data.Array.Zip
 public import Init.Data.Array.InsertIdx
 public import Init.Data.Array.Extract
-
-public section

src/Init/Data/Array/Attach.lean

@@ -84,10 +84,10 @@ well-founded recursion mechanism to prove that the function terminates.
   simp [pmap]
 
 /-- Implementation of `pmap` using the zero-copy version of `attach`. -/
-@[inline] private def pmapImpl {P : α → Prop} (f : ∀ a, P a → β) (xs : Array α) (H : ∀ a ∈ xs, P a) :
+@[inline] def pmapImpl {P : α → Prop} (f : ∀ a, P a → β) (xs : Array α) (H : ∀ a ∈ xs, P a) :
     Array β := (xs.attachWith _ H).map fun ⟨x, h'⟩ => f x h'
 
-@[csimp] private theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by
+@[csimp] theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by
   funext α β p f xs H
   cases xs
   simp only [pmap, pmapImpl, List.attachWith_toArray, List.map_toArray, mk.injEq, List.map_attachWith_eq_pmap]
@@ -95,16 +95,16 @@ well-founded recursion mechanism to prove that the function terminates.
   intro a m h₁ h₂
   congr
 
-@[simp, grind =] theorem pmap_empty {P : α → Prop} (f : ∀ a, P a → β) : pmap f #[] (by simp) = #[] := rfl
+@[simp] theorem pmap_empty {P : α → Prop} (f : ∀ a, P a → β) : pmap f #[] (by simp) = #[] := rfl
 
-@[simp, grind =] theorem pmap_push {P : α → Prop} (f : ∀ a, P a → β) (a : α) (xs : Array α) (h : ∀ b ∈ xs.push a, P b) :
+@[simp] theorem pmap_push {P : α → Prop} (f : ∀ a, P a → β) (a : α) (xs : Array α) (h : ∀ b ∈ xs.push a, P b) :
     pmap f (xs.push a) h =
       (pmap f xs (fun a m => by simp at h; exact h a (.inl m))).push (f a (h a (by simp))) := by
   simp [pmap]
 
-@[simp, grind =] theorem attach_empty : (#[] : Array α).attach = #[] := rfl
+@[simp] theorem attach_empty : (#[] : Array α).attach = #[] := rfl
 
-@[simp, grind =] theorem attachWith_empty {P : α → Prop} (H : ∀ x ∈ #[], P x) : (#[] : Array α).attachWith P H = #[] := rfl
+@[simp] theorem attachWith_empty {P : α → Prop} (H : ∀ x ∈ #[], P x) : (#[] : Array α).attachWith P H = #[] := rfl
 
 @[simp] theorem _root_.List.attachWith_mem_toArray {l : List α} :
     l.attachWith (fun x => x ∈ l.toArray) (fun x h => by simpa using h) =
@@ -125,13 +125,11 @@ theorem pmap_congr_left {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a,
   simp only [List.pmap_toArray, mk.injEq]
   rw [List.pmap_congr_left _ h]
 
-@[grind =]
 theorem map_pmap {p : α → Prop} {g : β → γ} {f : ∀ a, p a → β} {xs : Array α} (H) :
     map g (pmap f xs H) = pmap (fun a h => g (f a h)) xs H := by
   cases xs
   simp [List.map_pmap]
 
-@[grind =]
 theorem pmap_map {p : β → Prop} {g : ∀ b, p b → γ} {f : α → β} {xs : Array α} (H) :
     pmap g (map f xs) H = pmap (fun a h => g (f a) h) xs fun _ h => H _ (mem_map_of_mem h) := by
   cases xs
@@ -147,14 +145,14 @@ theorem attachWith_congr {xs ys : Array α} (w : xs = ys) {P : α → Prop} {H :
   subst w
   simp
 
-@[simp, grind =] theorem attach_push {a : α} {xs : Array α} :
+@[simp] theorem attach_push {a : α} {xs : Array α} :
     (xs.push a).attach =
       (xs.attach.map (fun ⟨x, h⟩ => ⟨x, mem_push_of_mem a h⟩)).push ⟨a, by simp⟩ := by
   cases xs
   rw [attach_congr (List.push_toArray _ _)]
   simp [Function.comp_def]
 
-@[simp, grind =] theorem attachWith_push {a : α} {xs : Array α} {P : α → Prop} {H : ∀ x ∈ xs.push a, P x} :
+@[simp] theorem attachWith_push {a : α} {xs : Array α} {P : α → Prop} {H : ∀ x ∈ xs.push a, P x} :
     (xs.push a).attachWith P H =
       (xs.attachWith P (fun x h => by simp at H; exact H x (.inl h))).push ⟨a, H a (by simp)⟩ := by
   cases xs
@@ -176,9 +174,6 @@ theorem attach_map_val (xs : Array α) (f : α → β) :
   cases xs
   simp
 
-@[deprecated attach_map_val (since := "2025-02-17")]
-abbrev attach_map_coe := @attach_map_val
-
 -- The argument `xs : Array α` is explicit to allow rewriting from right to left.
 theorem attach_map_subtype_val (xs : Array α) : xs.attach.map Subtype.val = xs := by
   cases xs; simp
@@ -187,9 +182,6 @@ theorem attachWith_map_val {p : α → Prop} {f : α → β} {xs : Array α} (H
     ((xs.attachWith p H).map fun (i : { i // p i}) => f i) = xs.map f := by
   cases xs; simp
 
-@[deprecated attachWith_map_val (since := "2025-02-17")]
-abbrev attachWith_map_coe := @attachWith_map_val
-
 theorem attachWith_map_subtype_val {p : α → Prop} {xs : Array α} (H : ∀ a ∈ xs, p a) :
     (xs.attachWith p H).map Subtype.val = xs := by
   cases xs; simp
@@ -294,25 +286,23 @@ theorem getElem_attach {xs : Array α} {i : Nat} (h : i < xs.attach.size) :
     xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem (by simpa using h)⟩ :=
   getElem_attachWith h
 
-@[simp, grind =] theorem pmap_attach {xs : Array α} {p : {x // x ∈ xs} → Prop} {f : ∀ a, p a → β} (H) :
+@[simp] theorem pmap_attach {xs : Array α} {p : {x // x ∈ xs} → Prop} {f : ∀ a, p a → β} (H) :
     pmap f xs.attach H =
       xs.pmap (P := fun a => ∃ h : a ∈ xs, p ⟨a, h⟩)
         (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨h, H ⟨a, h⟩ (by simp)⟩) := by
   ext <;> simp
 
-@[simp, grind =] theorem pmap_attachWith {xs : Array α} {p : {x // q x} → Prop} {f : ∀ a, p a → β} (H₁ H₂) :
+@[simp] theorem pmap_attachWith {xs : Array α} {p : {x // q x} → Prop} {f : ∀ a, p a → β} (H₁ H₂) :
     pmap f (xs.attachWith q H₁) H₂ =
       xs.pmap (P := fun a => ∃ h : q a, p ⟨a, h⟩)
         (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨H₁ _ h, H₂ ⟨a, H₁ _ h⟩ (by simpa)⟩) := by
   ext <;> simp
 
-@[grind =]
 theorem foldl_pmap {xs : Array α} {P : α → Prop} {f : (a : α) → P a → β}
     (H : ∀ (a : α), a ∈ xs → P a) (g : γ → β → γ) (x : γ) :
     (xs.pmap f H).foldl g x = xs.attach.foldl (fun acc a => g acc (f a.1 (H _ a.2))) x := by
   rw [pmap_eq_map_attach, foldl_map]
 
-@[grind =]
 theorem foldr_pmap {xs : Array α} {P : α → Prop} {f : (a : α) → P a → β}
     (H : ∀ (a : α), a ∈ xs → P a) (g : β → γ → γ) (x : γ) :
     (xs.pmap f H).foldr g x = xs.attach.foldr (fun a acc => g (f a.1 (H _ a.2)) acc) x := by
@@ -370,20 +360,18 @@ theorem foldr_attach {xs : Array α} {f : α → β → β} {b : β} :
   ext
   simpa using fun a => List.mem_of_getElem? a
 
-@[grind =]
 theorem attach_map {xs : Array α} {f : α → β} :
     (xs.map f).attach = xs.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem h⟩) := by
   cases xs
   ext <;> simp
 
-@[grind =]
 theorem attachWith_map {xs : Array α} {f : α → β} {P : β → Prop} (H : ∀ (b : β), b ∈ xs.map f → P b) :
     (xs.map f).attachWith P H = (xs.attachWith (P ∘ f) (fun _ h => H _ (mem_map_of_mem h))).map
       fun ⟨x, h⟩ => ⟨f x, h⟩ := by
   cases xs
   simp [List.attachWith_map]
 
-@[simp, grind =] theorem map_attachWith {xs : Array α} {P : α → Prop} {H : ∀ (a : α), a ∈ xs → P a}
+@[simp] theorem map_attachWith {xs : Array α} {P : α → Prop} {H : ∀ (a : α), a ∈ xs → P a}
     {f : { x // P x } → β} :
     (xs.attachWith P H).map f = xs.attach.map fun ⟨x, h⟩ => f ⟨x, H _ h⟩ := by
   cases xs <;> simp_all
@@ -401,9 +389,6 @@ theorem map_attach_eq_pmap {xs : Array α} {f : { x // x ∈ xs } → β} :
   cases xs
   ext <;> simp
 
-@[deprecated map_attach_eq_pmap (since := "2025-02-09")]
-abbrev map_attach := @map_attach_eq_pmap
-
 @[grind =]
 theorem attach_filterMap {xs : Array α} {f : α → Option β} :
     (xs.filterMap f).attach = xs.attach.filterMap
@@ -439,7 +424,6 @@ theorem filter_attachWith {q : α → Prop} {xs : Array α} {p : {x // q x} →
   cases xs
   simp [Function.comp_def, List.filter_map]
 
-@[grind =]
 theorem pmap_pmap {p : α → Prop} {q : β → Prop} {g : ∀ a, p a → β} {f : ∀ b, q b → γ} {xs} (H₁ H₂) :
     pmap f (pmap g xs H₁) H₂ =
       pmap (α := { x // x ∈ xs }) (fun a h => f (g a h) (H₂ (g a h) (mem_pmap_of_mem a.2))) xs.attach
@@ -447,7 +431,7 @@ theorem pmap_pmap {p : α → Prop} {q : β → Prop} {g : ∀ a, p a → β} {f
   cases xs
   simp [List.pmap_pmap, List.pmap_map]
 
-@[simp, grind =] theorem pmap_append {p : ι → Prop} {f : ∀ a : ι, p a → α} {xs ys : Array ι}
+@[simp] theorem pmap_append {p : ι → Prop} {f : ∀ a : ι, p a → α} {xs ys : Array ι}
     (h : ∀ a ∈ xs ++ ys, p a) :
     (xs ++ ys).pmap f h =
       (xs.pmap f fun a ha => h a (mem_append_left ys ha)) ++
@@ -462,7 +446,7 @@ theorem pmap_append' {p : α → Prop} {f : ∀ a : α, p a → β} {xs ys : Arr
       xs.pmap f h₁ ++ ys.pmap f h₂ :=
   pmap_append _
 
-@[simp, grind =] theorem attach_append {xs ys : Array α} :
+@[simp] theorem attach_append {xs ys : Array α} :
     (xs ++ ys).attach = xs.attach.map (fun ⟨x, h⟩ => ⟨x, mem_append_left ys h⟩) ++
       ys.attach.map fun ⟨x, h⟩ => ⟨x, mem_append_right xs h⟩ := by
   cases xs
@@ -470,62 +454,59 @@ theorem pmap_append' {p : α → Prop} {f : ∀ a : α, p a → β} {xs ys : Arr
   rw [attach_congr (List.append_toArray _ _)]
   simp [List.attach_append, Function.comp_def]
 
-@[simp, grind =] theorem attachWith_append {P : α → Prop} {xs ys : Array α}
+@[simp] theorem attachWith_append {P : α → Prop} {xs ys : Array α}
     {H : ∀ (a : α), a ∈ xs ++ ys → P a} :
     (xs ++ ys).attachWith P H = xs.attachWith P (fun a h => H a (mem_append_left ys h)) ++
       ys.attachWith P (fun a h => H a (mem_append_right xs h)) := by
   simp [attachWith]
 
-@[simp, grind =] theorem pmap_reverse {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
+@[simp] theorem pmap_reverse {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
     (H : ∀ (a : α), a ∈ xs.reverse → P a) :
     xs.reverse.pmap f H = (xs.pmap f (fun a h => H a (by simpa using h))).reverse := by
   induction xs <;> simp_all
 
-@[grind =]
 theorem reverse_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
     (H : ∀ (a : α), a ∈ xs → P a) :
     (xs.pmap f H).reverse = xs.reverse.pmap f (fun a h => H a (by simpa using h)) := by
   rw [pmap_reverse]
 
-@[simp, grind =] theorem attachWith_reverse {P : α → Prop} {xs : Array α}
+@[simp] theorem attachWith_reverse {P : α → Prop} {xs : Array α}
     {H : ∀ (a : α), a ∈ xs.reverse → P a} :
     xs.reverse.attachWith P H =
       (xs.attachWith P (fun a h => H a (by simpa using h))).reverse := by
   cases xs
   simp
 
-@[grind =]
 theorem reverse_attachWith {P : α → Prop} {xs : Array α}
     {H : ∀ (a : α), a ∈ xs → P a} :
     (xs.attachWith P H).reverse = (xs.reverse.attachWith P (fun a h => H a (by simpa using h))) := by
   cases xs
   simp
 
-@[simp, grind =] theorem attach_reverse {xs : Array α} :
+@[simp] theorem attach_reverse {xs : Array α} :
     xs.reverse.attach = xs.attach.reverse.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
   cases xs
   rw [attach_congr List.reverse_toArray]
   simp
 
-@[grind =]
 theorem reverse_attach {xs : Array α} :
     xs.attach.reverse = xs.reverse.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
   cases xs
   simp
 
-@[simp, grind =] theorem back?_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
+@[simp] theorem back?_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
     (H : ∀ (a : α), a ∈ xs → P a) :
     (xs.pmap f H).back? = xs.attach.back?.map fun ⟨a, m⟩ => f a (H a m) := by
   cases xs
   simp
 
-@[simp, grind =] theorem back?_attachWith {P : α → Prop} {xs : Array α}
+@[simp] theorem back?_attachWith {P : α → Prop} {xs : Array α}
     {H : ∀ (a : α), a ∈ xs → P a} :
     (xs.attachWith P H).back? = xs.back?.pbind (fun a h => some ⟨a, H _ (mem_of_back? h)⟩) := by
   cases xs
   simp
 
-@[simp, grind =]
+@[simp]
 theorem back?_attach {xs : Array α} :
     xs.attach.back? = xs.back?.pbind fun a h => some ⟨a, mem_of_back? h⟩ := by
   cases xs

src/Init/Data/Array/Basic.lean

@@ -129,20 +129,11 @@ end Array
 
 namespace List
 
-@[deprecated Array.toArray_toList (since := "2025-02-17")]
-abbrev toArray_toList := @Array.toArray_toList
-
 -- This does not need to be a simp lemma, as already after the `whnfR` the right hand side is `as`.
 theorem toList_toArray {as : List α} : as.toArray.toList = as := rfl
 
-@[deprecated toList_toArray (since := "2025-02-17")]
-abbrev _root_.Array.toList_toArray := @List.toList_toArray
-
 @[simp, grind =] theorem size_toArray {as : List α} : as.toArray.size = as.length := by simp [Array.size]
 
-@[deprecated size_toArray (since := "2025-02-17")]
-abbrev _root_.Array.size_toArray := @List.size_toArray
-
 @[simp, grind =] theorem getElem_toArray {xs : List α} {i : Nat} (h : i < xs.toArray.size) :
     xs.toArray[i] = xs[i]'(by simpa using h) := rfl
 
@@ -412,10 +403,6 @@ that requires a proof the array is non-empty.
 def back? (xs : Array α) : Option α :=
   xs[xs.size - 1]?
 
-@[deprecated "Use `a[i]?` instead." (since := "2025-02-12"), expose]
-def get? (xs : Array α) (i : Nat) : Option α :=
-  if h : i < xs.size then some xs[i] else none
-
 /--
 Swaps a new element with the element at the given index.
 
@@ -1812,7 +1799,6 @@ Examples:
 * `#["apple", "pear", "orange"].eraseIdxIfInBounds 3 = #["apple", "pear", "orange"]`
 * `#["apple", "pear", "orange"].eraseIdxIfInBounds 5 = #["apple", "pear", "orange"]`
 -/
-@[grind]
 def eraseIdxIfInBounds (xs : Array α) (i : Nat) : Array α :=
   if h : i < xs.size then xs.eraseIdx i h else xs
 

src/Init/Data/Array/Bootstrap.lean

@@ -24,29 +24,6 @@ set_option linter.indexVariables true -- Enforce naming conventions for index va
 
 namespace Array
 
-/--
-Use the indexing notation `a[i]` instead.
-
-Access an element from an array without needing a runtime bounds checks,
-using a `Nat` index and a proof that it is in bounds.
-
-This function does not use `get_elem_tactic` to automatically find the proof that
-the index is in bounds. This is because the tactic itself needs to look up values in
-arrays.
--/
-@[deprecated "Use indexing notation `as[i]` instead" (since := "2025-02-17")]
-def get {α : Type u} (xs : @& Array α) (i : @& Nat) (h : LT.lt i xs.size) : α :=
-  xs.toList.get ⟨i, h⟩
-
-/--
-Use the indexing notation `a[i]!` instead.
-
-Access an element from an array, or panic if the index is out of bounds.
--/
-@[deprecated "Use indexing notation `as[i]!` instead" (since := "2025-02-17"), expose]
-def get! {α : Type u} [Inhabited α] (xs : @& Array α) (i : @& Nat) : α :=
-  Array.getD xs i default
-
 theorem foldlM_toList.aux [Monad m]
     {f : β → α → m β} {xs : Array α} {i j} (H : xs.size ≤ i + j) {b} :
     foldlM.loop f xs xs.size (Nat.le_refl _) i j b = (xs.toList.drop j).foldlM f b := by
@@ -108,9 +85,6 @@ abbrev push_toList := @toList_push
 
 @[simp, grind =] theorem toList_pop {xs : Array α} : xs.pop.toList = xs.toList.dropLast := rfl
 
-@[deprecated toList_pop (since := "2025-02-17")]
-abbrev pop_toList := @Array.toList_pop
-
 @[simp] theorem append_eq_append {xs ys : Array α} : xs.append ys = xs ++ ys := rfl
 
 @[simp, grind =] theorem toList_append {xs ys : Array α} :

src/Init/Data/Array/Count.lean

@@ -63,7 +63,7 @@ theorem size_eq_countP_add_countP {xs : Array α} : xs.size = countP p xs + coun
   rcases xs with ⟨xs⟩
   simp [List.length_eq_countP_add_countP (p := p)]
 
-@[grind _=_]
+@[grind =]
 theorem countP_eq_size_filter {xs : Array α} : countP p xs = (filter p xs).size := by
   rcases xs with ⟨xs⟩
   simp [List.countP_eq_length_filter]

src/Init/Data/Array/Erase.lean

@@ -324,6 +324,13 @@ abbrev erase_mkArray_ne := @erase_replicate_ne
 
 end erase
 
+/-! ### eraseIdxIfInBounds -/
+
+@[grind =]
+theorem eraseIdxIfInBounds_eq {xs : Array α} {i : Nat} :
+    xs.eraseIdxIfInBounds i = if h : i < xs.size then xs.eraseIdx i else xs := by
+  simp [eraseIdxIfInBounds]
+
 /-! ### eraseIdx -/
 
 theorem eraseIdx_eq_eraseIdxIfInBounds {xs : Array α} {i : Nat} (h : i < xs.size) :

src/Init/Data/Array/Find.lean

@@ -278,9 +278,6 @@ theorem find?_flatten_eq_none_iff {xss : Array (Array α)} {p : α → Bool} :
     xss.flatten.find? p = none ↔ ∀ ys ∈ xss, ∀ x ∈ ys, !p x := by
   simp
 
-@[deprecated find?_flatten_eq_none_iff (since := "2025-02-03")]
-abbrev find?_flatten_eq_none := @find?_flatten_eq_none_iff
-
 /--
 If `find? p` returns `some a` from `xs.flatten`, then `p a` holds, and
 some array in `xs` contains `a`, and no earlier element of that array satisfies `p`.
@@ -306,9 +303,6 @@ theorem find?_flatten_eq_some_iff {xss : Array (Array α)} {p : α → Bool} {a
       ⟨zs.toList, bs.toList.map Array.toList, by simpa using h⟩,
         by simpa using h₁, by simpa using h₂⟩
 
-@[deprecated find?_flatten_eq_some_iff (since := "2025-02-03")]
-abbrev find?_flatten_eq_some := @find?_flatten_eq_some_iff
-
 @[simp, grind =] theorem find?_flatMap {xs : Array α} {f : α → Array β} {p : β → Bool} :
     (xs.flatMap f).find? p = xs.findSome? (fun x => (f x).find? p) := by
   cases xs
@@ -318,17 +312,11 @@ theorem find?_flatMap_eq_none_iff {xs : Array α} {f : α → Array β} {p : β
     (xs.flatMap f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y := by
   simp
 
-@[deprecated find?_flatMap_eq_none_iff (since := "2025-02-03")]
-abbrev find?_flatMap_eq_none := @find?_flatMap_eq_none_iff
-
 @[grind =]
 theorem find?_replicate :
     find? p (replicate n a) = if n = 0 then none else if p a then some a else none := by
   simp [← List.toArray_replicate, List.find?_replicate]
 
-@[deprecated find?_replicate (since := "2025-03-18")]
-abbrev find?_mkArray := @find?_replicate
-
 @[simp] theorem find?_replicate_of_size_pos (h : 0 < n) :
     find? p (replicate n a) = if p a then some a else none := by
   simp [find?_replicate, Nat.ne_of_gt h]
@@ -346,34 +334,19 @@ abbrev find?_mkArray_of_pos := @find?_replicate_of_pos
 @[simp] theorem find?_replicate_of_neg (h : ¬ p a) : find? p (replicate n a) = none := by
   simp [find?_replicate, h]
 
-@[deprecated find?_replicate_of_neg (since := "2025-03-18")]
-abbrev find?_mkArray_of_neg := @find?_replicate_of_neg
-
 -- This isn't a `@[simp]` lemma since there is already a lemma for `l.find? p = none` for any `l`.
 theorem find?_replicate_eq_none_iff {n : Nat} {a : α} {p : α → Bool} :
     (replicate n a).find? p = none ↔ n = 0 ∨ !p a := by
   simp [← List.toArray_replicate, Classical.or_iff_not_imp_left]
 
-@[deprecated find?_replicate_eq_none_iff (since := "2025-03-18")]
-abbrev find?_mkArray_eq_none_iff := @find?_replicate_eq_none_iff
-
 @[simp] theorem find?_replicate_eq_some_iff {n : Nat} {a b : α} {p : α → Bool} :
     (replicate n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b := by
   simp [← List.toArray_replicate]
 
-@[deprecated find?_replicate_eq_some_iff (since := "2025-03-18")]
-abbrev find?_mkArray_eq_some_iff := @find?_replicate_eq_some_iff
-
-@[deprecated find?_replicate_eq_some_iff (since := "2025-02-03")]
-abbrev find?_mkArray_eq_some := @find?_replicate_eq_some_iff
-
 @[simp] theorem get_find?_replicate {n : Nat} {a : α} {p : α → Bool} (h) :
     ((replicate n a).find? p).get h = a := by
   simp [← List.toArray_replicate]
 
-@[deprecated get_find?_replicate (since := "2025-03-18")]
-abbrev get_find?_mkArray := @get_find?_replicate
-
 @[grind =]
 theorem find?_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
     (H : ∀ (a : α), a ∈ xs → P a) {p : β → Bool} :

src/Init/Data/Array/Lemmas.lean

@@ -80,9 +80,6 @@ theorem ne_empty_of_size_pos (h : 0 < xs.size) : xs ≠ #[] := by
 @[simp] theorem size_eq_zero_iff : xs.size = 0 ↔ xs = #[] :=
   ⟨eq_empty_of_size_eq_zero, fun h => h ▸ rfl⟩
 
-@[deprecated size_eq_zero_iff (since := "2025-02-24")]
-abbrev size_eq_zero := @size_eq_zero_iff
-
 theorem eq_empty_iff_size_eq_zero : xs = #[] ↔ xs.size = 0 :=
   size_eq_zero_iff.symm
 
@@ -107,17 +104,10 @@ theorem exists_mem_of_size_eq_add_one {xs : Array α} (h : xs.size = n + 1) :
 theorem size_pos_iff {xs : Array α} : 0 < xs.size ↔ xs ≠ #[] :=
   Nat.pos_iff_ne_zero.trans (not_congr size_eq_zero_iff)
 
-@[deprecated size_pos_iff (since := "2025-02-24")]
-abbrev size_pos := @size_pos_iff
-
 theorem size_eq_one_iff {xs : Array α} : xs.size = 1 ↔ ∃ a, xs = #[a] := by
   cases xs
   simpa using List.length_eq_one_iff
 
-@[deprecated size_eq_one_iff (since := "2025-02-24")]
-abbrev size_eq_one := @size_eq_one_iff
-
-
 /-! ## L[i] and L[i]? -/
 
 theorem getElem?_eq_none_iff {xs : Array α} : xs[i]? = none ↔ xs.size ≤ i := by
@@ -371,6 +361,7 @@ abbrev getElem?_mkArray := @getElem?_replicate
 
 /-! ### mem -/
 
+@[grind ←]
 theorem not_mem_empty (a : α) : ¬ a ∈ #[] := by simp
 
 @[simp, grind =] theorem mem_push {xs : Array α} {x y : α} : x ∈ xs.push y ↔ x ∈ xs ∨ x = y := by
@@ -542,18 +533,12 @@ theorem isEmpty_eq_false_iff_exists_mem {xs : Array α} :
 @[simp] theorem isEmpty_iff {xs : Array α} : xs.isEmpty ↔ xs = #[] := by
   cases xs <;> simp
 
-@[deprecated isEmpty_iff (since := "2025-02-17")]
-abbrev isEmpty_eq_true := @isEmpty_iff
-
 @[grind →]
 theorem empty_of_isEmpty {xs : Array α} (h : xs.isEmpty) : xs = #[] := Array.isEmpty_iff.mp h
 
 @[simp] theorem isEmpty_eq_false_iff {xs : Array α} : xs.isEmpty = false ↔ xs ≠ #[] := by
   cases xs <;> simp
 
-@[deprecated isEmpty_eq_false_iff (since := "2025-02-17")]
-abbrev isEmpty_eq_false := @isEmpty_eq_false_iff
-
 theorem isEmpty_iff_size_eq_zero {xs : Array α} : xs.isEmpty ↔ xs.size = 0 := by
   rw [isEmpty_iff, size_eq_zero_iff]
 
@@ -2996,11 +2981,6 @@ theorem _root_.List.toArray_drop {l : List α} {k : Nat} :
     (l.drop k).toArray = l.toArray.extract k := by
   rw [List.drop_eq_extract, List.extract_toArray, List.size_toArray]
 
-@[deprecated extract_size (since := "2025-02-27")]
-theorem take_size {xs : Array α} : xs.take xs.size = xs := by
-  cases xs
-  simp
-
 /-! ### shrink -/
 
 @[simp] private theorem size_shrink_loop {xs : Array α} {n : Nat} : (shrink.loop n xs).size = xs.size - n := by
@@ -3586,8 +3566,6 @@ theorem foldr_eq_foldl_reverse {xs : Array α} {f : α → β → β} {b} :
   subst w
   rw [foldr_eq_foldl_reverse, foldl_push_eq_append rfl, map_reverse]
 
-@[deprecated foldr_push_eq_append (since := "2025-02-09")] abbrev foldr_flip_push_eq_append := @foldr_push_eq_append
-
 theorem foldl_assoc {op : α → α → α} [ha : Std.Associative op] {xs : Array α} {a₁ a₂} :
      xs.foldl op (op a₁ a₂) = op a₁ (xs.foldl op a₂) := by
   rcases xs with ⟨l⟩
@@ -4712,44 +4690,3 @@ namespace List
       simp_all
 
 end List
-
-/-! ### Deprecations -/
-namespace Array
-
-set_option linter.deprecated false in
-@[deprecated "`get?` is deprecated" (since := "2025-02-12"), simp]
-theorem get?_eq_getElem? (xs : Array α) (i : Nat) : xs.get? i = xs[i]? := rfl
-
-@[deprecated getD_eq_getD_getElem? (since := "2025-02-12")] abbrev getD_eq_get? := @getD_eq_getD_getElem?
-
-set_option linter.deprecated false in
-@[deprecated getElem!_eq_getD (since := "2025-02-12")]
-theorem get!_eq_getD [Inhabited α] (xs : Array α) : xs.get! n = xs.getD n default := rfl
-
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]!` instead of `a.get! i`." (since := "2025-02-12")]
-theorem get!_eq_getD_getElem? [Inhabited α] (xs : Array α) (i : Nat) :
-    xs.get! i = xs[i]?.getD default := by
-  by_cases p : i < xs.size <;>
-  simp [get!, getD_eq_getD_getElem?, p]
-
-set_option linter.deprecated false in
-@[deprecated get!_eq_getD_getElem? (since := "2025-02-12")] abbrev get!_eq_getElem? := @get!_eq_getD_getElem?
-
-set_option linter.deprecated false in
-@[deprecated "`Array.get?` is deprecated, use `a[i]?` instead." (since := "2025-02-12")]
-theorem get?_eq_get?_toList (xs : Array α) (i : Nat) : xs.get? i = xs.toList.get? i := by
-  simp [← getElem?_toList]
-
-set_option linter.deprecated false in
-@[deprecated get!_eq_getD_getElem? (since := "2025-02-12")] abbrev get!_eq_get? := @get!_eq_getD_getElem?
-
-/-! ### set -/
-
-@[deprecated getElem?_set_self (since := "2025-02-27")] abbrev get?_set_eq := @getElem?_set_self
-@[deprecated getElem?_set_ne (since := "2025-02-27")] abbrev get?_set_ne := @getElem?_set_ne
-@[deprecated getElem?_set (since := "2025-02-27")] abbrev get?_set := @getElem?_set
-@[deprecated get_set (since := "2025-02-27")] abbrev get_set := @getElem_set
-@[deprecated get_set_ne (since := "2025-02-27")] abbrev get_set_ne := @getElem_set_ne
-
-end Array

src/Init/Data/Array/Lex.lean

@@ -8,5 +8,3 @@ module
 prelude
 public import Init.Data.Array.Lex.Basic
 public import Init.Data.Array.Lex.Lemmas
-
-public section

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

@@ -9,8 +9,8 @@ prelude
 public import Init.Core
 import Init.Data.Array.Basic
 import Init.Data.Nat.Lemmas
-import Init.Data.Range.Polymorphic.Iterators
-import Init.Data.Range.Polymorphic.Nat
+public import Init.Data.Range.Polymorphic.Iterators
+public import Init.Data.Range.Polymorphic.Nat
 import Init.Data.Iterators.Consumers
 
 public section
@@ -31,7 +31,7 @@ Specifically, `Array.lex as bs lt` is true if
 def lex [BEq α] (as bs : Array α) (lt : α → α → Bool := by exact (· < ·)) : Bool := Id.run do
   for h : i in 0...(min as.size bs.size) do
     -- TODO: `get_elem_tactic` should be able to find this itself.
-    have : i < min as.size bs.size := Std.PRange.lt_upper_of_mem h
+    have : i < min as.size bs.size := Std.Rco.lt_upper_of_mem h
     if lt as[i] bs[i] then
       return true
     else if as[i] != bs[i] then

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

@@ -42,8 +42,7 @@ protected theorem not_le_iff_gt [LT α] {xs ys : Array α} :
   Classical.not_not
 
 @[simp] theorem lex_empty [BEq α] {lt : α → α → Bool} {xs : Array α} : xs.lex #[] lt = false := by
-  rw [lex, Std.PRange.forIn'_eq_match]
-  simp [Std.PRange.SupportsUpperBound.IsSatisfied]
+  simp [lex, Std.Rco.forIn'_eq_if]
 
 private theorem cons_lex_cons.forIn'_congr_aux [Monad m] {as bs : ρ} {_ : Membership α ρ}
     [ForIn' m ρ α inferInstance] (w : as = bs)
@@ -64,13 +63,13 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs
      (#[a] ++ xs).lex (#[b] ++ ys) lt =
        (lt a b || a == b && xs.lex ys lt) := by
   simp only [lex, size_append, List.size_toArray, List.length_cons, List.length_nil, Nat.zero_add,
-    Nat.add_min_add_left, Nat.add_lt_add_iff_left, Std.PRange.forIn'_eq_forIn'_toList]
+    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.PRange.toList_eq_match rfl (fun _ _ _ => rfl)]
-    simp only [Std.PRange.SupportsUpperBound.IsSatisfied, bind_pure_comp, map_pure]
+    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.PRange.toList_Rox_eq_toList_Rcx_of_isSome_succ? (lo := 0) (h := 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,
     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]
@@ -83,16 +82,10 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs
     l₁.toArray.lex l₂.toArray lt = l₁.lex l₂ lt := by
   induction l₁ generalizing l₂ with
   | nil =>
-    cases l₂
-    · rw [lex, Std.PRange.forIn'_eq_match]
-      simp [Std.PRange.SupportsUpperBound.IsSatisfied]
-    · rw [lex, Std.PRange.forIn'_eq_match]
-      simp [Std.PRange.SupportsUpperBound.IsSatisfied]
+    cases l₂ <;> simp [lex, Std.Rco.forIn'_eq_if]
   | cons x l₁ ih =>
     cases l₂ with
-    | nil =>
-      rw [lex, Std.PRange.forIn'_eq_match]
-      simp [Std.PRange.SupportsUpperBound.IsSatisfied]
+    | nil => simp [lex, Std.Rco.forIn'_eq_if]
     | cons y l₂ =>
       rw [List.toArray_cons, List.toArray_cons y, cons_lex_cons, List.lex, ih]
 

src/Init/Data/Array/QSort.lean

@@ -7,5 +7,3 @@ module
 
 prelude
 public import Init.Data.Array.QSort.Basic
-
-public section

src/Init/Data/Array/Subarray.lean

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

src/Init/Data/Basic.lean

@@ -16,5 +16,3 @@ public import Init.Data.UInt
 public import Init.Data.Repr
 public import Init.Data.ToString.Basic
 public import Init.Data.String.Extra
-
-public section

src/Init/Data/BitVec.lean

@@ -13,5 +13,3 @@ public import Init.Data.BitVec.Bitblast
 public import Init.Data.BitVec.Decidable
 public import Init.Data.BitVec.Lemmas
 public import Init.Data.BitVec.Folds
-
-public section

src/Init/Data/BitVec/Basic.lean

@@ -29,10 +29,6 @@ set_option linter.missingDocs true
 
 namespace BitVec
 
-@[inline, deprecated BitVec.ofNatLT (since := "2025-02-13"), inherit_doc BitVec.ofNatLT]
-protected def ofNatLt {n : Nat} (i : Nat) (p : i < 2 ^ n) : BitVec n :=
-  BitVec.ofNatLT i p
-
 section Nat
 
 /--

src/Init/Data/BitVec/Bitblast.lean

@@ -17,6 +17,7 @@ import all Init.Data.BitVec.Basic
 public import Init.Data.BitVec.Decidable
 public import Init.Data.BitVec.Lemmas
 public import Init.Data.BitVec.Folds
+import Init.BinderPredicates
 
 @[expose] public section
 

src/Init/Data/BitVec/Bootstrap.lean

@@ -9,6 +9,7 @@ prelude
 public import Init.Data.BitVec.Basic
 import all Init.Data.BitVec.Basic
 import Init.Data.Int.Bitwise.Lemmas
+import Init.Ext
 
 public section
 

src/Init/Data/BitVec/Decidable.lean

@@ -8,6 +8,7 @@ module
 
 prelude
 public import Init.Data.BitVec.Bootstrap
+import Init.Ext
 
 public section
 
@@ -49,11 +50,11 @@ instance instDecidableForallBitVecSucc (P : BitVec (n+1) → Prop) [DecidablePre
 
 instance instDecidableExistsBitVecZero (P : BitVec 0 → Prop) [Decidable (P 0#0)] :
     Decidable (∃ v, P v) :=
-  decidable_of_iff (¬ ∀ v, ¬ P v) Classical.not_forall_not
+  decidable_of_iff (¬ ∀ v, ¬ P v) (by exact Classical.not_forall_not)
 
 instance instDecidableExistsBitVecSucc (P : BitVec (n+1) → Prop) [DecidablePred P]
     [Decidable (∀ (x : Bool) (v : BitVec n), ¬ P (v.cons x))] : Decidable (∃ v, P v) :=
-  decidable_of_iff (¬ ∀ v, ¬ P v) Classical.not_forall_not
+  decidable_of_iff (¬ ∀ v, ¬ P v) (by exact Classical.not_forall_not)
 
 /--
 For small numerals this isn't necessary (as typeclass search can use the above two instances),

src/Init/Data/BitVec/Lemmas.lean

@@ -22,6 +22,9 @@ public import Init.Data.Int.Pow
 public import Init.Data.Int.LemmasAux
 public import Init.Data.BitVec.Bootstrap
 public import Init.Data.Order.Factories
+public import Init.Data.List.BasicAux
+import Init.Data.List.Lemmas
+import Init.Data.BEq
 
 public section
 
@@ -74,10 +77,6 @@ theorem some_eq_getElem?_iff {l : BitVec w} : some a = l[n]? ↔ ∃ h : n < w,
 theorem getElem_of_getElem? {l : BitVec w} : l[n]? = some a → ∃ h : n < w, l[n] = a :=
   getElem?_eq_some_iff.mp
 
-set_option linter.missingDocs false in
-@[deprecated getElem?_eq_some_iff (since := "2025-02-17")]
-abbrev getElem?_eq_some := @getElem?_eq_some_iff
-
 theorem getElem?_eq_none_iff {l : BitVec w} : l[n]? = none ↔ w ≤ n := by
   simp
 
@@ -350,25 +349,14 @@ theorem ofBool_eq_iff_eq : ∀ {b b' : Bool}, BitVec.ofBool b = BitVec.ofBool b'
 @[simp] theorem ofBool_xor_ofBool : ofBool b ^^^ ofBool b' = ofBool (b ^^ b') := by
   cases b <;> cases b' <;> rfl
 
-@[deprecated toNat_ofNatLT (since := "2025-02-13")]
-theorem toNat_ofNatLt (x : Nat) (p : x < 2^w) : (x#'p).toNat = x := rfl
-
 @[simp, grind =] theorem getLsbD_ofNatLT {n : Nat} (x : Nat) (lt : x < 2^n) (i : Nat) :
   getLsbD (x#'lt) i = x.testBit i := by
   simp [getLsbD, BitVec.ofNatLT]
 
-@[deprecated getLsbD_ofNatLT (since := "2025-02-13")]
-theorem getLsbD_ofNatLt {n : Nat} (x : Nat) (lt : x < 2^n) (i : Nat) :
-  getLsbD (x#'lt) i = x.testBit i := getLsbD_ofNatLT x lt i
-
 @[simp, grind =] theorem getMsbD_ofNatLT {n x i : Nat} (h : x < 2^n) :
     getMsbD (x#'h) i = (decide (i < n) && x.testBit (n - 1 - i)) := by
   simp [getMsbD, getLsbD]
 
-@[deprecated getMsbD_ofNatLT (since := "2025-02-13")]
-theorem getMsbD_ofNatLt {n x i : Nat} (h : x < 2^n) :
-    getMsbD (x#'h) i = (decide (i < n) && x.testBit (n - 1 - i)) := getMsbD_ofNatLT h
-
 @[grind =]
 theorem ofNatLT_eq_ofNat {w : Nat} {n : Nat} (hn) : BitVec.ofNatLT n hn = BitVec.ofNat w n :=
   eq_of_toNat_eq (by simp [Nat.mod_eq_of_lt hn])
@@ -6361,15 +6349,4 @@ theorem two_pow_ctz_le_toNat_of_ne_zero {x : BitVec w} (hx : x ≠ 0#w) :
   have hclz := getLsbD_true_ctz_of_ne_zero (x := x) hx
   exact Nat.ge_two_pow_of_testBit hclz
 
-/-! ### Deprecations -/
-
-set_option linter.missingDocs false
-
-@[deprecated toFin_uShiftRight (since := "2025-02-18")]
-abbrev toFin_uShiftRight := @toFin_ushiftRight
-
-
-
-
-
 end BitVec

src/Init/Data/ByteArray.lean

@@ -10,5 +10,3 @@ public import Init.Data.ByteArray.Basic
 public import Init.Data.ByteArray.Bootstrap
 public import Init.Data.ByteArray.Extra
 public import Init.Data.ByteArray.Lemmas
-
-public section

src/Init/Data/ByteArray/Basic.lean

@@ -13,6 +13,8 @@ import all Init.Data.UInt.BasicAux
 public import Init.Data.Option.Basic
 public import Init.Data.Array.Extract
 
+set_option doc.verso true
+
 @[expose] public section
 universe u
 
@@ -34,24 +36,40 @@ instance : Inhabited ByteArray where
 instance : EmptyCollection ByteArray where
   emptyCollection := ByteArray.empty
 
-@[simp, grind =]
-theorem empty_eq_emptyc : @empty = ∅ := rfl
-
-@[simp, grind =]
-theorem emptyWithCapacity_eq_emptyc : @emptyWithCapacity n = ∅ := rfl
+/--
+Retrieves the size of the array as a platform-specific fixed-width integer.
 
+Because {name}`USize` is big enough to address all memory on every platform that Lean supports,
+there are in practice no {name}`ByteArray`s that have more elements that {name}`USize` can count.
+-/
 @[extern "lean_sarray_size", simp]
 def usize (a : @& ByteArray) : USize :=
   a.size.toUSize
 
+/--
+Retrieves the byte at the indicated index. Callers must prove that the index is in bounds. The index
+is represented by a platform-specific fixed-width integer (either 32 or 64 bits).
+
+Because {name}`USize` is big enough to address all memory on every platform that Lean supports, there are
+in practice no {name}`ByteArray`s for which {name}`uget` cannot retrieve all elements.
+-/
 @[extern "lean_byte_array_uget"]
 def uget : (a : @& ByteArray) → (i : USize) → (h : i.toNat < a.size := by get_elem_tactic) → UInt8
   | ⟨bs⟩, i, h => bs[i]
 
+/--
+Retrieves the byte at the indicated index. Panics if the index is out of bounds.
+-/
 @[extern "lean_byte_array_get"]
 def get! : (@& ByteArray) → (@& Nat) → UInt8
   | ⟨bs⟩, i => bs[i]!
 
+/--
+Retrieves the byte at the indicated index. Callers must prove that the index is in bounds.
+
+Use {name}`uget` for a more efficient alternative or {name}`get!` for a variant that panics if the
+index is out of bounds.
+-/
 @[extern "lean_byte_array_fget"]
 def get : (a : @& ByteArray) → (i : @& Nat) → (h : i < a.size := by get_elem_tactic) → UInt8
   | ⟨bs⟩, i, _ => bs[i]
@@ -62,37 +80,65 @@ instance : GetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
 instance : GetElem ByteArray USize UInt8 fun xs i => i.toFin < xs.size where
   getElem xs i h := xs.uget i h
 
+/--
+Replaces the byte at the given index.
+
+The array is modified in-place if there are no other references to it.
+
+If the index is out of bounds, the array is returned unmodified.
+-/
 @[extern "lean_byte_array_set"]
 def set! : ByteArray → (@& Nat) → UInt8 → ByteArray
   | ⟨bs⟩, i, b => ⟨bs.set! i b⟩
 
+/--
+Replaces the byte at the given index.
+
+No bounds check is performed, but the function requires a proof that the index is in bounds. This
+proof can usually be omitted, and will be synthesized automatically.
+
+The array is modified in-place if there are no other references to it.
+-/
 @[extern "lean_byte_array_fset"]
 def set : (a : ByteArray) → (i : @& Nat) → UInt8 → (h : i < a.size := by get_elem_tactic) → ByteArray
   | ⟨bs⟩, i, b, h => ⟨bs.set i b h⟩
 
-@[extern "lean_byte_array_uset"]
+@[extern "lean_byte_array_uset", inherit_doc ByteArray.set]
 def uset : (a : ByteArray) → (i : USize) → UInt8 → (h : i.toNat < a.size := by get_elem_tactic) → ByteArray
   | ⟨bs⟩, i, v, h => ⟨bs.uset i v h⟩
 
+/--
+Computes a hash for a {name}`ByteArray`.
+-/
 @[extern "lean_byte_array_hash"]
 protected opaque hash (a : @& ByteArray) : UInt64
 
 instance : Hashable ByteArray where
   hash := ByteArray.hash
 
+/--
+Returns {name}`true` when {name}`s` contains zero bytes.
+-/
 def isEmpty (s : ByteArray) : Bool :=
   s.size == 0
 
 /--
-  Copy the slice at `[srcOff, srcOff + len)` in `src` to `[destOff, destOff + len)` in `dest`, growing `dest` if necessary.
-  If `exact` is `false`, the capacity will be doubled when grown. -/
+Copies the slice at `[srcOff, srcOff + len)` in {name}`src` to `[destOff, destOff + len)` in
+{name}`dest`, growing {name}`dest` if necessary. If {name}`exact` is {name}`false`, the capacity
+will be doubled when grown.
+-/
 @[extern "lean_byte_array_copy_slice"]
 def copySlice (src : @& ByteArray) (srcOff : Nat) (dest : ByteArray) (destOff len : Nat) (exact : Bool := true) : ByteArray :=
   ⟨dest.data.extract 0 destOff ++ src.data.extract srcOff (srcOff + len) ++ dest.data.extract (destOff + min len (src.data.size - srcOff)) dest.data.size⟩
 
+/--
+Copies the bytes with indices {name}`b` (inclusive) to {name}`e` (exclusive) to a new
+{name}`ByteArray`.
+-/
 def extract (a : ByteArray) (b e : Nat) : ByteArray :=
   a.copySlice b empty 0 (e - b)
 
+@[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
   b.copySlice 0 a a.size b.size false
@@ -119,6 +165,9 @@ theorem append_eq {a b : ByteArray} : a.append b = a ++ b := rfl
 theorem fastAppend_eq {a b : ByteArray} : a.fastAppend b = a ++ b := by
   simp [← append_eq_fastAppend]
 
+/--
+Converts a packed array of bytes to a linked list.
+-/
 def toList (bs : ByteArray) : List UInt8 :=
   let rec loop (i : Nat) (r : List UInt8) :=
     if i < bs.size then
@@ -129,16 +178,12 @@ def toList (bs : ByteArray) : List UInt8 :=
     decreasing_by decreasing_trivial_pre_omega
   loop 0 []
 
-@[inline] def findIdx? (a : ByteArray) (p : UInt8 → Bool) (start := 0) : Option Nat :=
-  let rec @[specialize] loop (i : Nat) :=
-    if h : i < a.size then
-      if p a[i] then some i else loop (i+1)
-    else
-      none
-    termination_by a.size - i
-    decreasing_by decreasing_trivial_pre_omega
-  loop start
+/--
+Finds the index of the first byte in {name}`a` for which {name}`p` returns {name}`true`. If no byte
+in {name}`a` satisfies {name}`p`, then the result is {name}`none`.
 
+The index is returned along with a proof that it is a valid index in the array.
+-/
 @[inline] def findFinIdx? (a : ByteArray) (p : UInt8 → Bool) (start := 0) : Option (Fin a.size) :=
   let rec @[specialize] loop (i : Nat) :=
     if h : i < a.size then
@@ -150,11 +195,29 @@ def toList (bs : ByteArray) : List UInt8 :=
   loop start
 
 /--
-  We claim this unsafe implementation is correct because an array cannot have more than `usizeSz` elements in our runtime.
-  This is similar to the `Array` version.
+Finds the index of the first byte in {name}`a` for which {name}`p` returns {name}`true`. If no byte
+in {name}`a` satisfies {name}`p`, then the result is {name}`none`.
 
-  TODO: avoid code duplication in the future after we improve the compiler.
+The variant {name}`findFinIdx?` additionally returns a proof that the found index is in bounds.
 -/
+@[inline] def findIdx? (a : ByteArray) (p : UInt8 → Bool) (start := 0) : Option Nat :=
+  let rec @[specialize] loop (i : Nat) :=
+    if h : i < a.size then
+      if p a[i] then some i else loop (i+1)
+    else
+      none
+    termination_by a.size - i
+    decreasing_by decreasing_trivial_pre_omega
+  loop start
+
+/--
+An efficient implementation of {name}`ForIn.forIn` for {name}`ByteArray` that uses {name}`USize`
+rather than {name}`Nat` for indices.
+
+We claim this unsafe implementation is correct because an array cannot have more than
+{name}`USize.size` elements in our runtime. This is similar to the {name}`Array` version.
+-/
+-- TODO: avoid code duplication in the future after we improve the compiler.
 @[inline] unsafe def forInUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteArray) (b : β) (f : UInt8 → β → m (ForInStep β)) : m β :=
   let sz := as.usize
   let rec @[specialize] loop (i : USize) (b : β) : m β := do
@@ -167,7 +230,11 @@ def toList (bs : ByteArray) : List UInt8 :=
       pure b
   loop 0 b
 
-/-- Reference implementation for `forIn` -/
+/--
+The reference implementation of {name}`ForIn.forIn` for {name}`ByteArray`.
+
+In compiled code, this is replaced by the more efficient {name}`ByteArray.forInUnsafe`.
+-/
 @[implemented_by ByteArray.forInUnsafe]
 protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteArray) (b : β) (f : UInt8 → β → m (ForInStep β)) : m β :=
   let rec loop (i : Nat) (h : i ≤ as.size) (b : β) : m β := do
@@ -185,7 +252,13 @@ protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteAr
 instance : ForIn m ByteArray UInt8 where
   forIn := ByteArray.forIn
 
-/-- See comment at `forInUnsafe` -/
+/--
+An efficient implementation of a monadic left fold on for {name}`ByteArray` that uses {name}`USize`
+rather than {name}`Nat` for indices.
+
+We claim this unsafe implementation is correct because an array cannot have more than
+{name}`USize.size` elements in our runtime. This is similar to the {name}`Array` version.
+-/
 -- TODO: avoid code duplication.
 @[inline]
 unsafe def foldlMUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 → m β) (init : β) (as : ByteArray) (start := 0) (stop := as.size) : m β :=
@@ -202,7 +275,14 @@ unsafe def foldlMUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (f : β
   else
     pure init
 
-/-- Reference implementation for `foldlM` -/
+/--
+A monadic left fold on {name}`ByteArray` that iterates over an array from low to high indices,
+computing a running value.
+
+Each element of the array is combined with the value from the prior elements using a monadic
+function {name}`f`. The initial value {name}`init` is the starting value before any elements have
+been processed.
+-/
 @[implemented_by foldlMUnsafe]
 def foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 → m β) (init : β) (as : ByteArray) (start := 0) (stop := as.size) : m β :=
   let fold (stop : Nat) (h : stop ≤ as.size) :=
@@ -220,11 +300,23 @@ def foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 →
   else
     fold as.size (Nat.le_refl _)
 
+/--
+A left fold on {name}`ByteArray` that iterates over an array from low to high indices, computing a
+running value.
+
+Each element of the array is combined with the value from the prior elements using a function
+{name}`f`. The initial value {name}`init` is the starting value before any elements have been
+processed.
+
+{name}`ByteArray.foldlM` is a monadic variant of this function.
+-/
 @[inline]
 def foldl {β : Type v} (f : β → UInt8 → β) (init : β) (as : ByteArray) (start := 0) (stop := as.size) : β :=
   Id.run <| as.foldlM (pure <| f · ·) init start stop
 
-/-- Iterator over the bytes (`UInt8`) of a `ByteArray`.
+set_option doc.verso false -- Awaiting intra-module forward reference support
+/--
+Iterator over the bytes (`UInt8`) of a `ByteArray`.
 
 Typically created by `arr.iter`, where `arr` is a `ByteArray`.
 
@@ -248,6 +340,7 @@ structure Iterator where
   current byte is `(default : UInt8)`. -/
   idx : Nat
   deriving Inhabited
+set_option doc.verso true
 
 /-- Creates an iterator at the beginning of an array. -/
 def mkIterator (arr : ByteArray) : Iterator :=
@@ -265,16 +358,25 @@ theorem Iterator.sizeOf_eq (i : Iterator) : sizeOf i = i.array.size - i.idx :=
 
 namespace Iterator
 
-/-- Number of bytes remaining in the iterator. -/
+/--
+The number of bytes remaining in the iterator.
+-/
 def remainingBytes : Iterator → Nat
   | ⟨arr, i⟩ => arr.size - i
 
 @[inherit_doc Iterator.idx]
 def pos := Iterator.idx
 
-/-- The byte at the current position.
+/-- True if the iterator is past the array's last byte. -/
+@[inline]
+def atEnd : Iterator → Bool
+  | ⟨arr, i⟩ => i ≥ arr.size
 
-On an invalid position, returns `(default : UInt8)`. -/
+/--
+The byte at the current position.
+
+On an invalid position, returns {lean}`(default : UInt8)`.
+-/
 @[inline]
 def curr : Iterator → UInt8
   | ⟨arr, i⟩ =>
@@ -283,27 +385,28 @@ def curr : Iterator → UInt8
     else
       default
 
-/-- Moves the iterator's position forward by one byte, unconditionally.
+/--
+Moves the iterator's position forward by one byte, unconditionally.
 
 It is only valid to call this function if the iterator is not at the end of the array, *i.e.*
-`Iterator.atEnd` is `false`; otherwise, the resulting iterator will be invalid. -/
+{name}`Iterator.atEnd` is {name}`false`; otherwise, the resulting iterator will be invalid.
+-/
 @[inline]
 def next : Iterator → Iterator
   | ⟨arr, i⟩ => ⟨arr, i + 1⟩
 
-/-- Decreases the iterator's position.
+/--
+Decreases the iterator's position.
 
-If the position is zero, this function is the identity. -/
+If the position is zero, this function is the identity.
+-/
 @[inline]
 def prev : Iterator → Iterator
   | ⟨arr, i⟩ => ⟨arr, i - 1⟩
 
-/-- True if the iterator is past the array's last byte. -/
-@[inline]
-def atEnd : Iterator → Bool
-  | ⟨arr, i⟩ => i ≥ arr.size
-
-/-- True if the iterator is not past the array's last byte. -/
+/--
+True if the iterator is valid; that is, it is not past the array's last byte.
+-/
 @[inline]
 def hasNext : Iterator → Bool
   | ⟨arr, i⟩ => i < arr.size
@@ -329,17 +432,21 @@ def next' (it : Iterator) (_h : it.hasNext) : Iterator :=
 def hasPrev : Iterator → Bool
   | ⟨_, i⟩ => i > 0
 
-/-- Moves the iterator's position to the end of the array.
+/--
+Moves the iterator's position to the end of the array.
 
-Note that `i.toEnd.atEnd` is always `true`. -/
+Given {given}`i : ByteArray.Iterator`, note that {lean}`i.toEnd.atEnd` is always {name}`true`.
+-/
 @[inline]
 def toEnd : Iterator → Iterator
   | ⟨arr, _⟩ => ⟨arr, arr.size⟩
 
-/-- Moves the iterator's position several bytes forward.
+/--
+Moves the iterator's position several bytes forward.
 
 The resulting iterator is only valid if the number of bytes to skip is less than or equal to
-the number of bytes left in the iterator. -/
+the number of bytes left in the iterator.
+-/
 @[inline]
 def forward : Iterator → Nat → Iterator
   | ⟨arr, i⟩, f => ⟨arr, i + f⟩
@@ -347,9 +454,11 @@ def forward : Iterator → Nat → Iterator
 @[inherit_doc forward, inline]
 def nextn : Iterator → Nat → Iterator := forward
 
-/-- Moves the iterator's position several bytes back.
+/--
+Moves the iterator's position several bytes back.
 
-If asked to go back more bytes than available, stops at the beginning of the array. -/
+If asked to go back more bytes than available, stops at the beginning of the array.
+-/
 @[inline]
 def prevn : Iterator → Nat → Iterator
   | ⟨arr, i⟩, f => ⟨arr, i - f⟩

src/Init/Data/ByteArray/Bootstrap.lean

@@ -10,12 +10,19 @@ public import Init.Prelude
 public import Init.Data.List.Basic
 
 public section
+set_option doc.verso true
 
 namespace ByteArray
 
 @[simp]
 theorem data_push {a : ByteArray} {b : UInt8} : (a.push b).data = a.data.push b := rfl
 
+/--
+Appends two byte arrays.
+
+In compiled code, calls to {name}`ByteArray.append` are replaced with the much more efficient
+{name (scope:="Init.Data.ByteArray.Basic")}`ByteArray.fastAppend`.
+-/
 @[expose]
 protected def append (a b : ByteArray) : ByteArray :=
   ⟨⟨a.data.toList ++ b.data.toList⟩⟩

src/Init/Data/ByteArray/Extra.lean

@@ -9,7 +9,13 @@ prelude
 public import Init.Data.ByteArray.Basic
 import Init.Data.String.Basic
 
-/-- Interpret a `ByteArray` of size 8 as a little-endian `UInt64`. -/
+set_option doc.verso true
+
+/--
+Interprets a {name}`ByteArray` of size 8 as a little-endian {name}`UInt64`.
+
+Panics if the array's size is not 8.
+-/
 public def ByteArray.toUInt64LE! (bs : ByteArray) : UInt64 :=
   assert! bs.size == 8
   (bs.get! 7).toUInt64 <<< 0x38 |||
@@ -21,7 +27,11 @@ public def ByteArray.toUInt64LE! (bs : ByteArray) : UInt64 :=
   (bs.get! 1).toUInt64 <<< 0x8  |||
   (bs.get! 0).toUInt64
 
-/-- Interpret a `ByteArray` of size 8 as a big-endian `UInt64`. -/
+/--
+Interprets a {name}`ByteArray` of size 8 as a big-endian {name}`UInt64`.
+
+Panics if the array's size is not 8.
+-/
 public def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 :=
   assert! bs.size == 8
   (bs.get! 0).toUInt64 <<< 0x38 |||

src/Init/Data/ByteArray/Lemmas.lean

@@ -11,10 +11,15 @@ public import Init.Data.Array.Extract
 
 public section
 
-theorem ByteArray.data_empty : ByteArray.empty.data = #[] := rfl
+-- At present the preferred normal form for empty byte arrays is `ByteArray.empty`
+@[simp]
+theorem emptyc_eq_empty : (∅ : ByteArray) = ByteArray.empty := rfl
 
 @[simp]
-theorem ByteArray.data_emptyc : (∅ : ByteArray).data = #[] := rfl
+theorem emptyWithCapacity_eq_empty : ByteArray.emptyWithCapacity 0 = ByteArray.empty := rfl
+
+@[simp]
+theorem ByteArray.data_empty : ByteArray.empty.data = #[] := rfl
 
 @[simp]
 theorem ByteArray.data_extract {a : ByteArray} {b e : Nat} :
@@ -30,7 +35,7 @@ theorem ByteArray.extract_zero_size {b : ByteArray} : b.extract 0 b.size = b :=
   simp
 
 @[simp]
-theorem ByteArray.extract_same {b : ByteArray} {i : Nat} : b.extract i i = ∅ := by
+theorem ByteArray.extract_same {b : ByteArray} {i : Nat} : b.extract i i = ByteArray.empty := by
   ext1
   simp [Nat.min_le_left]
 
@@ -52,11 +57,8 @@ theorem ByteArray.data_append {l l' : ByteArray} :
     (l ++ l').data = l.data ++ l'.data := by
   simp [← Array.toList_inj]
 
-theorem ByteArray.size_empty : ByteArray.empty.size = 0 := by
-  simp [← ByteArray.size_data]
-
 @[simp]
-theorem ByteArray.size_emptyc : (∅ : ByteArray).size = 0 := by
+theorem ByteArray.size_empty : ByteArray.empty.size = 0 := by
   simp [← ByteArray.size_data]
 
 @[simp]
@@ -64,7 +66,7 @@ theorem List.data_toByteArray {l : List UInt8} :
     l.toByteArray.data = l.toArray := by
   rw [List.toByteArray]
   suffices ∀ a b, (List.toByteArray.loop a b).data = b.data ++ a.toArray by
-    simpa using this l ∅
+    simpa using this l ByteArray.empty
   intro a b
   fun_induction List.toByteArray.loop a b with simp_all
 
@@ -74,15 +76,15 @@ theorem List.size_toByteArray {l : List UInt8} :
   simp [← ByteArray.size_data]
 
 @[simp]
-theorem List.toByteArray_nil : List.toByteArray [] = ∅ := rfl
+theorem List.toByteArray_nil : List.toByteArray [] = ByteArray.empty := rfl
 
 @[simp]
-theorem ByteArray.empty_append {b : ByteArray} : ∅ ++ b = b := by
+theorem ByteArray.empty_append {b : ByteArray} : ByteArray.empty ++ b = b := by
   ext1
   simp
 
 @[simp]
-theorem ByteArray.append_empty {b : ByteArray} : b ++ ∅ = b := by
+theorem ByteArray.append_empty {b : ByteArray} : b ++ ByteArray.empty = b := by
   ext1
   simp
 
@@ -91,7 +93,7 @@ theorem ByteArray.size_append {a b : ByteArray} : (a ++ b).size = a.size + b.siz
   simp [← size_data]
 
 @[simp]
-theorem ByteArray.size_eq_zero_iff {a : ByteArray} : a.size = 0 ↔ a = ∅ := by
+theorem ByteArray.size_eq_zero_iff {a : ByteArray} : a.size = 0 ↔ a = ByteArray.empty := by
   refine ⟨fun h => ?_, fun h => h ▸ ByteArray.size_empty⟩
   ext1
   simp [← Array.size_eq_zero_iff, h]
@@ -126,23 +128,23 @@ theorem ByteArray.size_extract {a : ByteArray} {b e : Nat} :
   simp [← size_data]
 
 @[simp]
-theorem ByteArray.extract_eq_empty_iff {b : ByteArray} {i j : Nat} : b.extract i j = ∅ ↔ min j b.size ≤ i := by
+theorem ByteArray.extract_eq_empty_iff {b : ByteArray} {i j : Nat} : b.extract i j = ByteArray.empty ↔ min j b.size ≤ i := by
   rw [← size_eq_zero_iff, size_extract]
   omega
 
 @[simp]
-theorem ByteArray.extract_add_left {b : ByteArray} {i j : Nat} : b.extract (i + j) i = ∅ := by
+theorem ByteArray.extract_add_left {b : ByteArray} {i j : Nat} : b.extract (i + j) i = ByteArray.empty := by
   simp only [extract_eq_empty_iff]
   exact Nat.le_trans (Nat.min_le_left _ _) (by simp)
 
 @[simp]
 theorem ByteArray.append_eq_empty_iff {a b : ByteArray} :
-    a ++ b = ∅ ↔ a = ∅ ∧ b = ∅ := by
+    a ++ b = ByteArray.empty ↔ a = ByteArray.empty ∧ b = ByteArray.empty := by
   simp [← size_eq_zero_iff, size_append]
 
 @[simp]
 theorem List.toByteArray_eq_empty {l : List UInt8} :
-    l.toByteArray = ∅ ↔ l = [] := by
+    l.toByteArray = ByteArray.empty ↔ l = [] := by
   simp [← ByteArray.size_eq_zero_iff]
 
 theorem ByteArray.append_right_inj {ys₁ ys₂ : ByteArray} (xs : ByteArray) :
@@ -165,9 +167,9 @@ theorem ByteArray.append_inj_left {xs₁ xs₂ ys₁ ys₂ : ByteArray} (h : xs
   simp only [ByteArray.ext_iff, ← ByteArray.size_data, ByteArray.data_append] at *
   exact Array.append_inj_left h hl
 
-theorem ByteArray.extract_append_eq_right {a b : ByteArray} {i : Nat} (hi : i = a.size) :
-    (a ++ b).extract i (a ++ b).size = b := by
-  subst hi
+theorem ByteArray.extract_append_eq_right {a b : ByteArray} {i j : Nat} (hi : i = a.size) (hj : j = a.size + b.size) :
+    (a ++ b).extract i j = b := by
+  subst hi hj
   ext1
   simp [← size_data]
 
@@ -247,10 +249,8 @@ theorem ByteArray.append_assoc {a b c : ByteArray} : a ++ b ++ c = a ++ (b ++ c)
   simp
 
 @[simp]
-theorem ByteArray.toList_empty : (∅ : ByteArray).toList = [] := by
-  simp [ByteArray.toList]
-  rw [toList.loop]
-  simp
+theorem ByteArray.toList_empty : ByteArray.empty.toList = [] := by
+  simp [ByteArray.toList, ByteArray.toList.loop]
 
 theorem ByteArray.copySlice_eq_append {src : ByteArray} {srcOff : Nat} {dest : ByteArray} {destOff len : Nat} {exact : Bool} :
     ByteArray.copySlice src srcOff dest destOff len exact =

src/Init/Data/Char.lean

@@ -9,5 +9,3 @@ prelude
 public import Init.Data.Char.Basic
 public import Init.Data.Char.Lemmas
 public import Init.Data.Char.Order
-
-public section

src/Init/Data/Dyadic/Basic.lean

@@ -9,6 +9,7 @@ prelude
 public import Init.Data.Rat.Lemmas
 import Init.Data.Int.Bitwise.Lemmas
 import Init.Data.Int.DivMod.Lemmas
+import Init.Hints
 
 /-!
 # The dyadic rationals

src/Init/Data/Fin.lean

@@ -11,5 +11,3 @@ public import Init.Data.Fin.Log2
 public import Init.Data.Fin.Iterate
 public import Init.Data.Fin.Fold
 public import Init.Data.Fin.Lemmas
-
-public section

src/Init/Data/Fin/Basic.lean

@@ -140,7 +140,7 @@ Modulus of bounded numbers, usually invoked via the `%` operator.
 The resulting value is that computed by the `%` operator on `Nat`.
 -/
 protected def mod : Fin n → Fin n → Fin n
-  | ⟨a, h⟩, ⟨b, _⟩ => ⟨a % b,  Nat.lt_of_le_of_lt (Nat.mod_le _ _) h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨a % b, by exact Nat.lt_of_le_of_lt (Nat.mod_le _ _) h⟩
 
 /--
 Division of bounded numbers, usually invoked via the `/` operator.
@@ -154,7 +154,7 @@ Examples:
  * `(5 : Fin 10) / (7 : Fin 10) = (0 : Fin 10)`
 -/
 protected def div : Fin n → Fin n → Fin n
-  | ⟨a, h⟩, ⟨b, _⟩ => ⟨a / b, Nat.lt_of_le_of_lt (Nat.div_le_self _ _) h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨a / b, by exact Nat.lt_of_le_of_lt (Nat.div_le_self _ _) h⟩
 
 /--
 Modulus of bounded numbers with respect to a `Nat`.
@@ -162,7 +162,7 @@ Modulus of bounded numbers with respect to a `Nat`.
 The resulting value is that computed by the `%` operator on `Nat`.
 -/
 def modn : Fin n → Nat → Fin n
-  | ⟨a, h⟩, m => ⟨a % m, Nat.lt_of_le_of_lt (Nat.mod_le _ _) h⟩
+  | ⟨a, h⟩, m => ⟨a % m, by exact Nat.lt_of_le_of_lt (Nat.mod_le _ _) h⟩
 
 /--
 Bitwise and.

src/Init/Data/Fin/Lemmas.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Data.Nat.Lemmas
-public import Init.Data.Int.DivMod.Lemmas
 public import Init.Ext
 public import Init.ByCases
 public import Init.Conv
@@ -15,7 +14,7 @@ public import Init.Omega
 public import Init.Data.Order.Factories
 import Init.Data.Order.Lemmas
 
-public section
+@[expose] public section
 
 open Std
 
@@ -327,7 +326,9 @@ theorem subsingleton_iff_le_one : Subsingleton (Fin n) ↔ n ≤ 1 := by
   (match n with | 0 | 1 | n+2 => ?_) <;> try simp
   · exact ⟨nofun⟩
   · exact ⟨fun ⟨0, _⟩ ⟨0, _⟩ => rfl⟩
-  · exact fun h => by have := zero_lt_one (n := n); simp_all [h.elim 0 1]
+  · have : ¬ n + 2 ≤ 1 := by simp [Nat.not_le]
+    simp only [this, iff_false]
+    exact fun h => by have := zero_lt_one (n := n); simp_all [h.elim 0 1]
 
 instance subsingleton_zero : Subsingleton (Fin 0) := subsingleton_iff_le_one.2 (by decide)
 
@@ -914,16 +915,21 @@ theorem exists_fin_succ {P : Fin (n + 1) → Prop} : (∃ i, P i) ↔ P 0 ∨
   ⟨fun ⟨i, h⟩ => Fin.cases Or.inl (fun i hi => Or.inr ⟨i, hi⟩) i h, fun h =>
     (h.elim fun h => ⟨0, h⟩) fun ⟨i, hi⟩ => ⟨i.succ, hi⟩⟩
 
-theorem forall_fin_one {p : Fin 1 → Prop} : (∀ i, p i) ↔ p 0 :=
+@[simp] theorem forall_fin_zero {p : Fin 0 → Prop} : (∀ i, p i) ↔ True :=
+  ⟨fun _ => trivial, fun _ ⟨_, h⟩ => False.elim <| Nat.not_lt_zero _ h⟩
+
+@[simp] theorem exists_fin_zero {p : Fin 0 → Prop} : (∃ i, p i) ↔ False := by simp
+
+@[simp] theorem forall_fin_one {p : Fin 1 → Prop} : (∀ i, p i) ↔ p 0 :=
   ⟨fun h => h _, fun h i => Subsingleton.elim i 0 ▸ h⟩
 
-theorem exists_fin_one {p : Fin 1 → Prop} : (∃ i, p i) ↔ p 0 :=
+@[simp] theorem exists_fin_one {p : Fin 1 → Prop} : (∃ i, p i) ↔ p 0 :=
   ⟨fun ⟨i, h⟩ => Subsingleton.elim i 0 ▸ h, fun h => ⟨_, h⟩⟩
 
-theorem forall_fin_two {p : Fin 2 → Prop} : (∀ i, p i) ↔ p 0 ∧ p 1 :=
+@[simp] theorem forall_fin_two {p : Fin 2 → Prop} : (∀ i, p i) ↔ p 0 ∧ p 1 :=
   forall_fin_succ.trans <| and_congr_right fun _ => forall_fin_one
 
-theorem exists_fin_two {p : Fin 2 → Prop} : (∃ i, p i) ↔ p 0 ∨ p 1 :=
+@[simp] theorem exists_fin_two {p : Fin 2 → Prop} : (∃ i, p i) ↔ p 0 ∨ p 1 :=
   exists_fin_succ.trans <| or_congr_right exists_fin_one
 
 theorem fin_two_eq_of_eq_zero_iff : ∀ {a b : Fin 2}, (a = 0 ↔ b = 0) → a = b := by

src/Init/Data/FloatArray.lean

@@ -7,5 +7,3 @@ module
 
 prelude
 public import Init.Data.FloatArray.Basic
-
-public section

src/Init/Data/Format.lean

@@ -10,5 +10,3 @@ public import Init.Data.Format.Basic
 public import Init.Data.Format.Macro
 public import Init.Data.Format.Instances
 public import Init.Data.Format.Syntax
-
-public section

src/Init/Data/Format/Instances.lean

@@ -51,5 +51,5 @@ Converts a string to a pretty-printer document, replacing newlines in the string
 def String.toFormat (s : String) : Std.Format :=
   Std.Format.joinSep (s.splitOn "\n") Std.Format.line
 
-instance : ToFormat String.Pos where
+instance : ToFormat String.Pos.Raw where
   format p := format p.byteIdx

src/Init/Data/Hashable.lean

@@ -16,7 +16,7 @@ universe u
 instance : Hashable Nat where
   hash n := UInt64.ofNat n
 
-instance : Hashable String.Pos where
+instance : Hashable String.Pos.Raw where
   hash p := UInt64.ofNat p.byteIdx
 
 instance [Hashable α] [Hashable β] : Hashable (α × β) where
@@ -76,22 +76,3 @@ instance (P : Prop) : Hashable P where
 /-- An opaque (low-level) hash operation used to implement hashing for pointers. -/
 @[always_inline, inline] def hash64 (u : UInt64) : UInt64 :=
   mixHash u 11
-
-/--
-The `BEq α` and `Hashable α` instances on `α` are compatible. This means that that `a == b` implies
-`hash a = hash b`.
-
-This is automatic if the `BEq` instance is lawful.
--/
-class LawfulHashable (α : Type u) [BEq α] [Hashable α] where
-  /-- If `a == b`, then `hash a = hash b`. -/
-  hash_eq (a b : α) : a == b → hash a = hash b
-
-/--
-A lawful hash function respects its Boolean equality test.
--/
-theorem hash_eq [BEq α] [Hashable α] [LawfulHashable α] {a b : α} : a == b → hash a = hash b :=
-  LawfulHashable.hash_eq a b
-
-instance (priority := low) [BEq α] [Hashable α] [LawfulBEq α] : LawfulHashable α where
-  hash_eq _ _ h := eq_of_beq h ▸ rfl

src/Init/Data/Int.lean

@@ -18,5 +18,3 @@ public import Init.Data.Int.Pow
 public import Init.Data.Int.Cooper
 public import Init.Data.Int.Linear
 public import Init.Data.Int.OfNat
-
-public section

src/Init/Data/Int/Bitwise.lean

@@ -8,5 +8,3 @@ module
 prelude
 public import Init.Data.Int.Bitwise.Basic
 public import Init.Data.Int.Bitwise.Lemmas
-
-public section

src/Init/Data/Int/Compare.lean

@@ -9,6 +9,7 @@ prelude
 public import Init.Data.Ord.Basic
 import all Init.Data.Ord.Basic
 public import Init.Data.Int.Order
+import Init.Omega
 
 public section
 

src/Init/Data/Int/DivMod.lean

@@ -9,5 +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 section

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

@@ -206,9 +206,6 @@ theorem ediv_nonneg_iff_of_pos {a b : Int} (h : 0 < b) : 0 ≤ a / b ↔ 0 ≤ a
   | Int.ofNat (b+1), _ =>
     rcases a with ⟨a⟩ <;> simp [Int.ediv, -natCast_ediv]
 
-@[deprecated ediv_nonneg_iff_of_pos (since := "2025-02-28")]
-abbrev div_nonneg_iff_of_pos := @ediv_nonneg_iff_of_pos
-
 /-! ### emod -/
 
 theorem emod_nonneg : ∀ (a : Int) {b : Int}, b ≠ 0 → 0 ≤ a % b

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

@@ -13,6 +13,7 @@ public import Init.Data.Int.Order
 public import Init.Data.Int.Lemmas
 public import Init.Data.Nat.Dvd
 public import Init.RCases
+import Init.TacticsExtra
 
 public section
 
@@ -122,8 +123,8 @@ theorem eq_one_of_mul_eq_one_right {a b : Int} (H : 0 ≤ a) (H' : a * b = 1) :
 theorem eq_one_of_mul_eq_one_left {a b : Int} (H : 0 ≤ b) (H' : a * b = 1) : b = 1 :=
   eq_one_of_mul_eq_one_right (b := a) H <| by rw [Int.mul_comm, H']
 
-instance decidableDvd : DecidableRel (α := Int) (· ∣ ·) := fun _ _ =>
-  decidable_of_decidable_of_iff (dvd_iff_emod_eq_zero ..).symm
+instance decidableDvd : DecidableRel (α := Int) (· ∣ ·) := fun a b =>
+  decidable_of_decidable_of_iff (p := b % a = 0) (by exact (dvd_iff_emod_eq_zero ..).symm)
 
 protected theorem mul_dvd_mul_iff_left {a b c : Int} (h : a ≠ 0) : (a * b) ∣ (a * c) ↔ b ∣ c :=
   ⟨by rintro ⟨d, h'⟩; exact ⟨d, by rw [Int.mul_assoc] at h'; exact (mul_eq_mul_left_iff h).mp h'⟩,

src/Init/Data/Int/LemmasAux.lean

@@ -8,7 +8,6 @@ module
 prelude
 public import Init.Data.Int.Order
 public import Init.Data.Int.Pow
-public import Init.Data.Int.DivMod.Lemmas
 public import Init.Omega
 
 public section

src/Init/Data/Int/OfNat.lean

@@ -88,6 +88,20 @@ theorem finVal {n : Nat} {a : Fin n} {a' : Int}
     (h₁ : Lean.Grind.ToInt.toInt a = a') : NatCast.natCast (a.val) = a' := by
   rw [← h₁, Lean.Grind.ToInt.toInt, Lean.Grind.instToIntFinCoOfNatIntCast]
 
+theorem eq_eq {a b : Nat} {a' b' : Int}
+    (h₁ : NatCast.natCast a = a') (h₂ : NatCast.natCast b = b') : (a = b) = (a' = b') := by
+  simp [← h₁, ←h₂]; constructor
+  next => intro; subst a; rfl
+  next => simp [Int.natCast_inj]
+
+theorem lt_eq {a b : Nat} {a' b' : Int}
+    (h₁ : NatCast.natCast a = a') (h₂ : NatCast.natCast b = b') : (a < b) = (a' < b') := by
+  simp only [← h₁, ← h₂, Int.ofNat_lt]
+
+theorem le_eq {a b : Nat} {a' b' : Int}
+    (h₁ : NatCast.natCast a = a') (h₂ : NatCast.natCast b = b') : (a ≤ b) = (a' ≤ b') := by
+  simp only [← h₁, ← h₂, Int.ofNat_le]
+
 end Nat.ToInt
 
 namespace Int.Nonneg

src/Init/Data/Int/Order.lean

@@ -1347,8 +1347,6 @@ theorem neg_of_sign_eq_neg_one : ∀ {a : Int}, sign a = -1 → a < 0
   | 0 => Int.mul_zero _
   | -[_+1] => Int.mul_neg_one _
 
-@[deprecated mul_sign_self (since := "2025-02-24")] abbrev mul_sign := @mul_sign_self
-
 @[simp] theorem sign_mul_self (i : Int) : sign i * i = natAbs i := by
   rw [Int.mul_comm, mul_sign_self]
 

src/Init/Data/Int/Pow.lean

@@ -50,14 +50,9 @@ protected theorem pow_ne_zero {n : Int} {m : Nat} : n ≠ 0 → n ^ m ≠ 0 := b
 
 instance {n : Int} {m : Nat} [NeZero n] : NeZero (n ^ m) := ⟨Int.pow_ne_zero (NeZero.ne _)⟩
 
-@[deprecated Nat.pow_le_pow_left (since := "2025-02-17")]
-abbrev pow_le_pow_of_le_left := @Nat.pow_le_pow_left
-
-@[deprecated Nat.pow_le_pow_right (since := "2025-02-17")]
-abbrev pow_le_pow_of_le_right := @Nat.pow_le_pow_right
-
+-- This can't be removed until the next update-stage0
 @[deprecated Nat.pow_pos (since := "2025-02-17")]
-abbrev pos_pow_of_pos := @Nat.pow_pos
+abbrev _root_.Nat.pos_pow_of_pos := @Nat.pow_pos
 
 @[simp, norm_cast]
 protected theorem natCast_pow (b n : Nat) : ((b^n : Nat) : Int) = (b : Int) ^ n := by

src/Init/Data/Iterators/Combinators.lean

@@ -9,5 +9,3 @@ prelude
 public import Init.Data.Iterators.Combinators.Monadic
 public import Init.Data.Iterators.Combinators.FilterMap
 public import Init.Data.Iterators.Combinators.ULift
-
-public section

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

@@ -8,5 +8,3 @@ module
 prelude
 public import Init.Data.Iterators.Combinators.Monadic.FilterMap
 public import Init.Data.Iterators.Combinators.Monadic.ULift
-
-public section

src/Init/Data/Iterators/Consumers.lean

@@ -13,5 +13,3 @@ public import Init.Data.Iterators.Consumers.Loop
 public import Init.Data.Iterators.Consumers.Partial
 
 public import Init.Data.Iterators.Consumers.Stream
-
-public section

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

@@ -10,5 +10,3 @@ public import Init.Data.Iterators.Consumers.Monadic.Access
 public import Init.Data.Iterators.Consumers.Monadic.Collect
 public import Init.Data.Iterators.Consumers.Monadic.Loop
 public import Init.Data.Iterators.Consumers.Monadic.Partial
-
-public section

src/Init/Data/Iterators/Internal.lean

@@ -8,5 +8,3 @@ module
 prelude
 public import Init.Data.Iterators.Internal.LawfulMonadLiftFunction
 public import Init.Data.Iterators.Internal.Termination
-
-public section

src/Init/Data/Iterators/Lemmas.lean

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

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

@@ -10,5 +10,3 @@ 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.ULift
-
-public section

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

@@ -195,8 +195,7 @@ theorem Iter.step_mapM {f : β → n γ}
   match step with
   | .yield it' out h =>
     simp only [bind_pure_comp]
-    simp only [Functor.map, 
-      ]
+    simp only [Functor.map]
     rfl
   | .skip it' h => rfl
   | .done h => rfl
@@ -317,4 +316,119 @@ theorem Iter.toArray_filter
     (it.filter f).toArray = it.toArray.filter f := by
   simp [filter_eq_toIter_filter_toIterM, IterM.toArray_filter, Iter.toArray_eq_toArray_toIterM]
 
+section Fold
+
+theorem Iter.foldM_filterMapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
+    [Iterator α Id β] [Finite α Id] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n]
+    [IteratorLoop α Id Id] [IteratorLoop α Id m] [IteratorLoop α Id n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    [LawfulIteratorLoop α Id Id] [LawfulIteratorLoop α Id m] [LawfulIteratorLoop α Id n]
+    {f : β → m (Option γ)} {g : δ → γ → n δ} {init : δ} {it : Iter (α := α) β} :
+    (it.filterMapM f).foldM (init := init) g =
+      it.foldM (init := init) (fun d b => do
+          let some c ← f b | pure d
+          g d c) := by
+  rw [foldM_eq_foldM_toIterM, filterMapM_eq_toIter_filterMapM_toIterM, IterM.foldM_filterMapM]
+  congr
+  simp [instMonadLiftTOfMonadLift, Id.instMonadLiftTOfPure]
+
+theorem Iter.foldM_mapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
+    [Iterator α Id β] [Finite α Id] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n]
+    [IteratorLoop α Id m] [IteratorLoop α Id n]
+    [LawfulIteratorLoop α Id m] [LawfulIteratorLoop α Id n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    {f : β → m γ} {g : δ → γ → n δ} {init : δ} {it : Iter (α := α) β} :
+    (it.mapM f).foldM (init := init) g =
+      it.foldM (init := init) (fun d b => do let c ← f b; g d c) := by
+  rw [foldM_eq_foldM_toIterM, mapM_eq_toIter_mapM_toIterM, IterM.foldM_mapM]
+  congr
+  simp [instMonadLiftTOfMonadLift, Id.instMonadLiftTOfPure]
+
+theorem Iter.foldM_filterMap {α β γ : Type w} {δ : Type x} {m : Type x → Type w'}
+    [Iterator α Id β] [Finite α Id] [Monad m] [LawfulMonad m]
+    [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
+    {f : β → Option γ} {g : δ → γ → m δ} {init : δ} {it : Iter (α := α) β} :
+    (it.filterMap f).foldM (init := init) g =
+      it.foldM (init := init) (fun d b => do
+          let some c := f b | pure d
+          g d c) := by
+  induction it using Iter.inductSteps generalizing init with | step it ihy ihs
+  rw [foldM_eq_match_step, foldM_eq_match_step, step_filterMap]
+  -- There seem to be some type dependencies that, combined with nested match expressions,
+  -- force us to split a lot.
+  split <;> rename_i h
+  · split at h
+    · split at h
+      · cases h
+      · cases h; simp [*, ihy ‹_›]
+    · cases h
+    · cases h
+  · split at h
+    · split at h
+      · cases h; simp [*, ihy ‹_›]
+      · cases h
+    · cases h; simp [*, ihs ‹_›]
+    · cases h
+  · split at h
+    · split at h
+      · cases h
+      · cases h
+    · cases h
+    · simp [*]
+
+theorem Iter.foldM_map {α β γ : Type w} {δ : Type x} {m : Type x → Type w'}
+    [Iterator α Id β] [Finite α Id] [Monad m] [LawfulMonad m]
+    [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
+    {f : β → γ} {g : δ → γ → m δ} {init : δ} {it : Iter (α := α) β} :
+    (it.map f).foldM (init := init) g =
+      it.foldM (init := init) (fun d b => g d (f b)) := by
+  induction it using Iter.inductSteps generalizing init with | step it ihy ihs
+  rw [foldM_eq_match_step, foldM_eq_match_step, step_map]
+  cases it.step using PlausibleIterStep.casesOn
+  · simp [*, ihy ‹_›]
+  · simp [*, ihs ‹_›]
+  · simp
+
+theorem Iter.fold_filterMapM {α β γ δ : Type w} {m : Type w → Type w'}
+    [Iterator α Id β] [Finite α Id] [Monad m] [LawfulMonad m]
+    [IteratorLoop α Id Id.{w}] [IteratorLoop α Id m]
+    [LawfulIteratorLoop α Id Id] [LawfulIteratorLoop α Id m]
+    {f : β → m (Option γ)} {g : δ → γ → δ} {init : δ} {it : Iter (α := α) β} :
+    (it.filterMapM f).fold (init := init) g =
+      it.foldM (init := init) (fun d b => do
+          let some c ← f b | pure d
+          return g d c) := by
+  rw [foldM_eq_foldM_toIterM, filterMapM_eq_toIter_filterMapM_toIterM, IterM.fold_filterMapM]
+  rfl
+
+theorem Iter.fold_mapM {α β γ δ : Type w} {m : Type w → Type w'}
+    [Iterator α Id β] [Finite α Id] [Monad m] [LawfulMonad m]
+    [IteratorLoop α Id Id.{w}] [IteratorLoop α Id m]
+    [LawfulIteratorLoop α Id Id] [LawfulIteratorLoop α Id m]
+    {f : β → m γ} {g : δ → γ → δ} {init : δ} {it : Iter (α := α) β} :
+    (it.mapM f).fold (init := init) g =
+      it.foldM (init := init) (fun d b => do return g d (← f b)) := by
+  rw [foldM_eq_foldM_toIterM, mapM_eq_toIter_mapM_toIterM, IterM.fold_mapM]
+
+theorem Iter.fold_filterMap {α β γ : Type w} {δ : Type x}
+    [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    {f : β → Option γ} {g : δ → γ → δ} {init : δ} {it : Iter (α := α) β} :
+    (it.filterMap f).fold (init := init) g =
+      it.fold (init := init) (fun d b =>
+          match f b with
+          | some c => g d c
+          | _ => d) := by
+  simp only [fold_eq_foldM, foldM_filterMap]
+  rfl
+
+theorem Iter.fold_map {α β γ : Type w} {δ : Type x}
+    [Iterator α Id β] [Finite α Id]
+    [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    {f : β → γ} {g : δ → γ → δ} {init : δ} {it : Iter (α := α) β} :
+    (it.map f).fold (init := init) g =
+      it.fold (init := init) (fun d b => g d (f b)) := by
+  simp [fold_eq_foldM, foldM_map]
+
+end Fold
+
 end Std.Iterators

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

@@ -9,5 +9,3 @@ 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.ULift
-
-public section

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

@@ -414,4 +414,129 @@ theorem IterM.toArray_filter {α : Type w} {m : Type w → Type w'} [Monad m] [L
 
 end ToArray
 
+section Fold
+
+theorem IterM.foldM_filterMapM {α β γ δ : Type w}
+    {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Iterator α m β] [Finite α m]
+    [Monad m] [Monad n] [Monad o] [LawfulMonad m] [LawfulMonad n] [LawfulMonad o]
+    [IteratorLoop α m n] [IteratorLoop α m o]
+    [LawfulIteratorLoop α m n] [LawfulIteratorLoop α m o]
+    [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
+    {f : β → n (Option γ)} {g : δ → γ → o δ} {init : δ} {it : IterM (α := α) m β} :
+    haveI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
+    (it.filterMapM f).foldM (init := init) g =
+      it.foldM (init := init) (fun d b => do
+          let some c ← f b | pure d
+          g d c) := by
+  letI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
+  induction it using IterM.inductSteps generalizing init with | step it ihy ihs
+  rw [foldM_eq_match_step, foldM_eq_match_step, step_filterMapM, liftM_bind, bind_assoc]
+  apply bind_congr; intro step
+  split
+  · simp only [PlausibleIterStep.skip, PlausibleIterStep.yield, liftM_bind, bind_assoc]
+    apply bind_congr; intro c?
+    split <;> simp [ihy ‹_›]
+  · simp [ihs ‹_›]
+  · simp
+
+theorem IterM.foldM_mapM {α β γ δ : Type w}
+    {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Iterator α m β] [Finite α m]
+    [Monad m] [Monad n] [Monad o] [LawfulMonad m] [LawfulMonad n] [LawfulMonad o]
+    [IteratorLoop α m n] [IteratorLoop α m o]
+    [LawfulIteratorLoop α m n] [LawfulIteratorLoop α m o]
+    [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
+    {f : β → n γ} {g : δ → γ → o δ} {init : δ} {it : IterM (α := α) m β} :
+    haveI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
+    (it.mapM f).foldM (init := init) g =
+      it.foldM (init := init) (fun d b => do let c ← f b; g d c) := by
+  letI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
+  induction it using IterM.inductSteps generalizing init with | step it ihy ihs
+  rw [foldM_eq_match_step, foldM_eq_match_step, step_mapM, liftM_bind, bind_assoc]
+  apply bind_congr; intro step
+  split
+  · simp [ihy ‹_›]
+  · simp [ihs ‹_›]
+  · simp
+
+theorem IterM.foldM_filterMap {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
+    [Iterator α m β] [Finite α m] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n]
+    [IteratorLoop α m m] [IteratorLoop α m n]
+    [LawfulIteratorLoop α m m] [LawfulIteratorLoop α m n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    {f : β → Option γ} {g : δ → γ → n δ} {init : δ} {it : IterM (α := α) m β} :
+    (it.filterMap f).foldM (init := init) g =
+      it.foldM (init := init) (fun d b => do
+          let some c := f b | pure d
+          g d c) := by
+  induction it using IterM.inductSteps generalizing init with | step it ihy ihs
+  rw [foldM_eq_match_step, foldM_eq_match_step, step_filterMap, liftM_bind, bind_assoc]
+  apply bind_congr; intro step
+  split
+  · split <;> simp [ihy ‹_›, *]
+  · simp [ihs ‹_›]
+  · simp
+
+theorem IterM.foldM_map {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
+    [Iterator α m β] [Finite α m] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n]
+    [IteratorLoop α m m] [IteratorLoop α m n]
+    [LawfulIteratorLoop α m m] [LawfulIteratorLoop α m n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    {f : β → γ} {g : δ → γ → n δ} {init : δ} {it : IterM (α := α) m β} :
+    (it.map f).foldM (init := init) g =
+      it.foldM (init := init) (fun d b => do g d (f b)) := by
+  induction it using IterM.inductSteps generalizing init with | step it ihy ihs
+  rw [foldM_eq_match_step, foldM_eq_match_step, step_map, liftM_bind, bind_assoc]
+  apply bind_congr; intro step
+  split
+  · simp [ihy ‹_›]
+  · simp [ihs ‹_›]
+  · simp
+
+theorem IterM.fold_filterMapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
+    [Iterator α m β] [Finite α m] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n]
+    [IteratorLoop α m m] [IteratorLoop α m n]
+    [LawfulIteratorLoop α m m] [LawfulIteratorLoop α m n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    {f : β → n (Option γ)} {g : δ → γ → δ} {init : δ} {it : IterM (α := α) m β} :
+    (it.filterMapM f).fold (init := init) g =
+      it.foldM (init := init) (fun d b => do
+          let some c ← f b | pure d
+          return g d c) := by
+  simp [fold_eq_foldM, foldM_filterMapM]
+
+theorem IterM.fold_mapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
+    [Iterator α m β] [Finite α m] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n]
+    [IteratorLoop α m m] [IteratorLoop α m n]
+    [LawfulIteratorLoop α m m] [LawfulIteratorLoop α m n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    {f : β → n γ} {g : δ → γ → δ} {init : δ} {it : IterM (α := α) m β} :
+    (it.mapM f).fold (init := init) g =
+      it.foldM (init := init) (fun d b => do let c ← f b; return g d c) := by
+  simp [fold_eq_foldM, foldM_mapM]
+
+theorem IterM.fold_filterMap {α β γ δ : Type w} {m : Type w → Type w'}
+    [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m]
+    [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    {f : β → Option γ} {g : δ → γ → δ} {init : δ} {it : IterM (α := α) m β} :
+    (it.filterMap f).fold (init := init) g =
+      it.fold (init := init) (fun d b =>
+          match f b with
+          | some c => g d c
+          | _ => d) := by
+  simp [fold_eq_foldM, foldM_filterMap]
+  congr; ext
+  split <;> simp
+
+theorem IterM.fold_map {α β γ δ : Type w} {m : Type w → Type w'}
+    [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m]
+    [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    {f : β → γ} {g : δ → γ → δ} {init : δ} {it : IterM (α := α) m β} :
+    (it.map f).fold (init := init) g =
+      it.fold (init := init) (fun d b => g d (f b)) := by
+  simp [fold_eq_foldM, foldM_map]
+
+end Fold
+
 end Std.Iterators

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

@@ -9,5 +9,3 @@ prelude
 public import Init.Data.Iterators.Lemmas.Consumers.Monadic
 public import Init.Data.Iterators.Lemmas.Consumers.Collect
 public import Init.Data.Iterators.Lemmas.Consumers.Loop
-
-public section

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

@@ -44,20 +44,32 @@ theorem Iter.forIn_eq {α β : Type w} [Iterator α Id β] [Finite α Id]
             f out acc) := by
   simp [ForIn.forIn, forIn'_eq, -forIn'_eq_forIn]
 
-@[congr] theorem Iter.forIn'_congr {α β : Type w}
-    [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id]
+@[congr] theorem Iter.forIn'_congr {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α Id β] [Finite α Id] [IteratorLoop α Id m]
     {ita itb : Iter (α := α) β} (w : ita = itb)
     {b b' : γ} (hb : b = b')
-    {f : (a' : β) → _ → γ → Id (ForInStep γ)}
-    {g : (a' : β) → _ → γ → Id (ForInStep γ)}
+    {f : (a' : β) → _ → γ → m (ForInStep γ)}
+    {g : (a' : β) → _ → γ → m (ForInStep γ)}
     (h : ∀ a m b, f a (by simpa [w] using m) b = g a m b) :
-    letI : ForIn' Id (Iter (α := α) β) β _ := Iter.instForIn'
+    letI : ForIn' m (Iter (α := α) β) β _ := Iter.instForIn'
     forIn' ita b f = forIn' itb b' g := by
   subst_eqs
   simp only [← funext_iff] at h
   rw [← h]
   rfl
 
+@[congr] theorem Iter.forIn_congr {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α Id β] [Finite α Id] [IteratorLoop α Id m]
+    {ita itb : Iter (α := α) β} (w : ita = itb)
+    {b b' : γ} (hb : b = b')
+    {f : (a' : β) → γ → m (ForInStep γ)}
+    {g : (a' : β) → γ → m (ForInStep γ)}
+    (h : ∀ a b, f a b = g a b) :
+    forIn ita b f = forIn itb b' g := by
+  subst_eqs
+  simp only [← funext_iff] at h
+  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] [LawfulIteratorLoop α Id m]

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

@@ -8,5 +8,3 @@ module
 prelude
 public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
 public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
-
-public section

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

@@ -60,20 +60,34 @@ theorem IterM.forIn_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m
         IteratorLoop.wellFounded_of_finite it init _ (fun _ => id) (fun out _ acc => (⟨·, .intro⟩) <$> f out acc) := by
   simp only [ForIn.forIn, forIn'_eq]
 
-@[congr] theorem IterM.forIn'_congr {α β : Type w} {m : Type w → Type w'} [Monad m]
-    [Iterator α m β] [Finite α m] [IteratorLoop α m m]
+@[congr] theorem IterM.forIn'_congr {α β : Type w} {m : Type w → Type w'}
+    {n : Type w → Type w''} [Monad n] [Monad m]
+    [Iterator α m β] [Finite α m] [IteratorLoop α m n] [MonadLiftT m n]
     {ita itb : IterM (α := α) m β} (w : ita = itb)
     {b b' : γ} (hb : b = b')
-    {f : (a' : β) → _ → γ → m (ForInStep γ)}
-    {g : (a' : β) → _ → γ → m (ForInStep γ)}
+    {f : (a' : β) → _ → γ → n (ForInStep γ)}
+    {g : (a' : β) → _ → γ → n (ForInStep γ)}
     (h : ∀ a m b, f a (by simpa [w] using m) b = g a m b) :
-    letI : ForIn' m (IterM (α := α) m β) β _ := IterM.instForIn'
+    letI : ForIn' n (IterM (α := α) m β) β _ := IterM.instForIn'
     forIn' ita b f = forIn' itb b' g := by
   subst_eqs
   simp only [← funext_iff] at h
   rw [← h]
   rfl
 
+@[congr] theorem IterM.forIn_congr {α β : Type w} {m : Type w → Type w'}
+    {n : Type w → Type w''} [Monad n] [Monad m]
+    [Iterator α m β] [Finite α m] [IteratorLoop α m n] [MonadLiftT m n]
+    {ita itb : IterM (α := α) m β} (w : ita = itb)
+    {b b' : γ} (hb : b = b')
+    {f : (a' : β) → γ → n (ForInStep γ)}
+    {g : (a' : β) → γ → n (ForInStep γ)}
+    (h : ∀ a b, f a b = g a b) :
+    forIn ita b f = forIn itb b' g := by
+  subst_eqs
+  simp only [← funext_iff] at h
+  rw [← h]
+
 theorem IterM.forIn'_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
     [Finite α m] {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n]
     [IteratorLoop α m n] [LawfulIteratorLoop α m n]

src/Init/Data/LawfulHashable.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+
+prelude
+public import Init.Core
+
+public section
+
+/--
+The `BEq α` and `Hashable α` instances on `α` are compatible. This means that that `a == b` implies
+`hash a = hash b`.
+
+This is automatic if the `BEq` instance is lawful.
+-/
+class LawfulHashable (α : Type u) [BEq α] [Hashable α] where
+  /-- If `a == b`, then `hash a = hash b`. -/
+  hash_eq (a b : α) : a == b → hash a = hash b
+
+/--
+A lawful hash function respects its Boolean equality test.
+-/
+theorem hash_eq [BEq α] [Hashable α] [LawfulHashable α] {a b : α} : a == b → hash a = hash b :=
+  LawfulHashable.hash_eq a b
+
+instance (priority := low) [BEq α] [Hashable α] [LawfulBEq α] : LawfulHashable α where
+  hash_eq _ _ h := eq_of_beq h ▸ rfl

src/Init/Data/List.lean

@@ -31,5 +31,3 @@ public import Init.Data.List.MapIdx
 public import Init.Data.List.OfFn
 public import Init.Data.List.FinRange
 public import Init.Data.List.Lex
-
-public section

src/Init/Data/List/Attach.lean

@@ -61,10 +61,10 @@ well-founded recursion mechanism to prove that the function terminates.
 @[inline, expose] def attach (l : List α) : List {x // x ∈ l} := attachWith l _ fun _ => id
 
 /-- Implementation of `pmap` using the zero-copy version of `attach`. -/
-@[inline] private def pmapImpl {P : α → Prop} (f : ∀ a, P a → β) (l : List α) (H : ∀ a ∈ l, P a) :
+@[inline] def pmapImpl {P : α → Prop} (f : ∀ a, P a → β) (l : List α) (H : ∀ a ∈ l, P a) :
     List β := (l.attachWith _ H).map fun ⟨x, h'⟩ => f x h'
 
-@[csimp] private theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by
+@[csimp] theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by
   funext α β p f l h'
   let rec go : ∀ l' (hL' : ∀ ⦃x⦄, x ∈ l' → p x),
       pmap f l' hL' = map (fun ⟨x, hx⟩ => f x hx) (pmap Subtype.mk l' hL')
@@ -95,14 +95,12 @@ theorem pmap_congr_left {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a,
   | cons x l ih =>
     rw [pmap, pmap, h _ mem_cons_self, ih fun a ha => h a (mem_cons_of_mem _ ha)]
 
-@[grind =]
 theorem map_pmap {p : α → Prop} {g : β → γ} {f : ∀ a, p a → β} {l : List α} (H) :
     map g (pmap f l H) = pmap (fun a h => g (f a h)) l H := by
   induction l
   · rfl
   · simp only [*, pmap, map]
 
-@[grind =]
 theorem pmap_map {p : β → Prop} {g : ∀ b, p b → γ} {f : α → β} {l : List α} (H) :
     pmap g (map f l) H = pmap (fun a h => g (f a) h) l fun _ h => H _ (mem_map_of_mem h) := by
   induction l
@@ -149,9 +147,6 @@ theorem attach_map_val {l : List α} {f : α → β} :
     (l.attach.map fun (i : {i // i ∈ l}) => f i) = l.map f := by
   rw [attach, attachWith, map_pmap]; exact pmap_eq_map _
 
-@[deprecated attach_map_val (since := "2025-02-17")]
-abbrev attach_map_coe := @attach_map_val
-
 -- The argument `l : List α` is explicit to allow rewriting from right to left.
 theorem attach_map_subtype_val (l : List α) : l.attach.map Subtype.val = l :=
   attach_map_val.trans (List.map_id _)
@@ -160,9 +155,6 @@ theorem attachWith_map_val {p : α → Prop} {f : α → β} {l : List α} (H :
     ((l.attachWith p H).map fun (i : { i // p i}) => f i) = l.map f := by
   rw [attachWith, map_pmap]; exact pmap_eq_map _
 
-@[deprecated attachWith_map_val (since := "2025-02-17")]
-abbrev attachWith_map_coe := @attachWith_map_val
-
 theorem attachWith_map_subtype_val {p : α → Prop} {l : List α} (H : ∀ a ∈ l, p a) :
     (l.attachWith p H).map Subtype.val = l :=
   (attachWith_map_val _).trans (List.map_id _)
@@ -254,13 +246,6 @@ theorem getElem?_pmap {p : α → Prop} {f : ∀ a, p a → β} {l : List α} (h
     · simp
     · simp only [pmap, getElem?_cons_succ, hl]
 
-set_option linter.deprecated false in
-@[deprecated List.getElem?_pmap (since := "2025-02-12")]
-theorem get?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) (n : Nat) :
-    get? (pmap f l h) n = Option.pmap f (get? l n) fun x H => h x (mem_of_get? H) := by
-  simp only [get?_eq_getElem?]
-  simp [getElem?_pmap]
-
 -- The argument `f` is explicit to allow rewriting from right to left.
 @[simp, grind =]
 theorem getElem_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) {i : Nat}
@@ -277,15 +262,6 @@ theorem getElem_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h
     · simp
     · simp [hl]
 
-@[deprecated getElem_pmap (since := "2025-02-13")]
-theorem get_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) {n : Nat}
-    (hn : n < (pmap f l h).length) :
-    get (pmap f l h) ⟨n, hn⟩ =
-      f (get l ⟨n, @length_pmap _ _ p f l h ▸ hn⟩)
-        (h _ (getElem_mem (@length_pmap _ _ p f l h ▸ hn))) := by
-  simp only [get_eq_getElem]
-  simp [getElem_pmap]
-
 @[simp, grind =]
 theorem getElem?_attachWith {xs : List α} {i : Nat} {P : α → Prop} {H : ∀ a ∈ xs, P a} :
     (xs.attachWith P H)[i]? = xs[i]?.pmap Subtype.mk (fun _ a => H _ (mem_of_getElem? a)) :=
@@ -307,13 +283,13 @@ theorem getElem_attach {xs : List α} {i : Nat} (h : i < xs.attach.length) :
     xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem (by simpa using h)⟩ :=
   getElem_attachWith h
 
-@[simp, grind =] theorem pmap_attach {l : List α} {p : {x // x ∈ l} → Prop} {f : ∀ a, p a → β} (H) :
+@[simp] theorem pmap_attach {l : List α} {p : {x // x ∈ l} → Prop} {f : ∀ a, p a → β} (H) :
     pmap f l.attach H =
       l.pmap (P := fun a => ∃ h : a ∈ l, p ⟨a, h⟩)
         (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨h, H ⟨a, h⟩ (by simp)⟩) := by
   apply ext_getElem <;> simp
 
-@[simp, grind =] theorem pmap_attachWith {l : List α} {p : {x // q x} → Prop} {f : ∀ a, p a → β} (H₁ H₂) :
+@[simp] theorem pmap_attachWith {l : List α} {p : {x // q x} → Prop} {f : ∀ a, p a → β} (H₁ H₂) :
     pmap f (l.attachWith q H₁) H₂ =
       l.pmap (P := fun a => ∃ h : q a, p ⟨a, h⟩)
         (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨H₁ _ h, H₂ ⟨a, H₁ _ h⟩ (by simpa)⟩) := by
@@ -371,26 +347,24 @@ theorem getElem_attach {xs : List α} {i : Nat} (h : i < xs.attach.length) :
     xs.attach.tail = xs.tail.attach.map (fun ⟨x, h⟩ => ⟨x, mem_of_mem_tail h⟩) := by
   cases xs <;> simp
 
-@[grind =]
 theorem foldl_pmap {l : List α} {P : α → Prop} {f : (a : α) → P a → β}
     (H : ∀ (a : α), a ∈ l → P a) (g : γ → β → γ) (x : γ) :
     (l.pmap f H).foldl g x = l.attach.foldl (fun acc a => g acc (f a.1 (H _ a.2))) x := by
   rw [pmap_eq_map_attach, foldl_map]
 
-@[grind =]
 theorem foldr_pmap {l : List α} {P : α → Prop} {f : (a : α) → P a → β}
     (H : ∀ (a : α), a ∈ l → P a) (g : β → γ → γ) (x : γ) :
     (l.pmap f H).foldr g x = l.attach.foldr (fun a acc => g (f a.1 (H _ a.2)) acc) x := by
   rw [pmap_eq_map_attach, foldr_map]
 
-@[simp, grind =] theorem foldl_attachWith
+@[simp] theorem foldl_attachWith
     {l : List α} {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : β → { x // q x } → β} {b} :
     (l.attachWith q H).foldl f b = l.attach.foldl (fun b ⟨a, h⟩ => f b ⟨a, H _ h⟩) b := by
   induction l generalizing b with
   | nil => simp
   | cons a l ih => simp [ih, foldl_map]
 
-@[simp, grind =] theorem foldr_attachWith
+@[simp] theorem foldr_attachWith
     {l : List α} {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : { x // q x } → β → β} {b} :
     (l.attachWith q H).foldr f b = l.attach.foldr (fun a acc => f ⟨a.1, H _ a.2⟩ acc) b := by
   induction l generalizing b with
@@ -429,18 +403,16 @@ theorem foldr_attach {l : List α} {f : α → β → β} {b : β} :
   | nil => simp
   | cons a l ih => rw [foldr_cons, attach_cons, foldr_cons, foldr_map, ih]
 
-@[grind =]
 theorem attach_map {l : List α} {f : α → β} :
     (l.map f).attach = l.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem h⟩) := by
   induction l <;> simp [*]
 
-@[grind =]
 theorem attachWith_map {l : List α} {f : α → β} {P : β → Prop} (H : ∀ (b : β), b ∈ l.map f → P b) :
     (l.map f).attachWith P H = (l.attachWith (P ∘ f) (fun _ h => H _ (mem_map_of_mem h))).map
       fun ⟨x, h⟩ => ⟨f x, h⟩ := by
   induction l <;> simp [*]
 
-@[simp, grind =] theorem map_attachWith {l : List α} {P : α → Prop} {H : ∀ (a : α), a ∈ l → P a}
+@[simp] theorem map_attachWith {l : List α} {P : α → Prop} {H : ∀ (a : α), a ∈ l → P a}
     {f : { x // P x } → β} :
     (l.attachWith P H).map f = l.attach.map fun ⟨x, h⟩ => f ⟨x, H _ h⟩ := by
   induction l <;> simp_all
@@ -466,10 +438,6 @@ theorem map_attach_eq_pmap {l : List α} {f : { x // x ∈ l } → β} :
     apply pmap_congr_left
     simp
 
-@[deprecated map_attach_eq_pmap (since := "2025-02-09")]
-abbrev map_attach := @map_attach_eq_pmap
-
-@[grind =]
 theorem attach_filterMap {l : List α} {f : α → Option β} :
     (l.filterMap f).attach = l.attach.filterMap
       fun ⟨x, h⟩ => (f x).pbind (fun b m => some ⟨b, mem_filterMap.mpr ⟨x, h, m⟩⟩) := by
@@ -500,7 +468,6 @@ theorem attach_filterMap {l : List α} {f : α → Option β} :
       ext
       simp
 
-@[grind =]
 theorem attach_filter {l : List α} (p : α → Bool) :
     (l.filter p).attach = l.attach.filterMap
       fun x => if w : p x.1 then some ⟨x.1, mem_filter.mpr ⟨x.2, w⟩⟩ else none := by
@@ -512,7 +479,7 @@ theorem attach_filter {l : List α} (p : α → Bool) :
 
 -- We are still missing here `attachWith_filterMap` and `attachWith_filter`.
 
-@[simp, grind =]
+@[simp]
 theorem filterMap_attachWith {q : α → Prop} {l : List α} {f : {x // q x} → Option β} (H) :
     (l.attachWith q H).filterMap f = l.attach.filterMap (fun ⟨x, h⟩ => f ⟨x, H _ h⟩) := by
   induction l with
@@ -521,7 +488,7 @@ theorem filterMap_attachWith {q : α → Prop} {l : List α} {f : {x // q x} →
     simp only [attachWith_cons, filterMap_cons]
     split <;> simp_all [Function.comp_def]
 
-@[simp, grind =]
+@[simp]
 theorem filter_attachWith {q : α → Prop} {l : List α} {p : {x // q x} → Bool} (H) :
     (l.attachWith q H).filter p =
       (l.attach.filter (fun ⟨x, h⟩ => p ⟨x, H _ h⟩)).map (fun ⟨x, h⟩ => ⟨x, H _ h⟩) := by
@@ -531,14 +498,13 @@ theorem filter_attachWith {q : α → Prop} {l : List α} {p : {x // q x} → Bo
     simp only [attachWith_cons, filter_cons]
     split <;> simp_all [Function.comp_def, filter_map]
 
-@[grind =]
 theorem pmap_pmap {p : α → Prop} {q : β → Prop} {g : ∀ a, p a → β} {f : ∀ b, q b → γ} {l} (H₁ H₂) :
     pmap f (pmap g l H₁) H₂ =
       pmap (α := { x // x ∈ l }) (fun a h => f (g a h) (H₂ (g a h) (mem_pmap_of_mem a.2))) l.attach
         (fun a _ => H₁ a a.2) := by
   simp [pmap_eq_map_attach, attach_map]
 
-@[simp, grind =] theorem pmap_append {p : ι → Prop} {f : ∀ a : ι, p a → α} {l₁ l₂ : List ι}
+@[simp] theorem pmap_append {p : ι → Prop} {f : ∀ a : ι, p a → α} {l₁ l₂ : List ι}
     (h : ∀ a ∈ l₁ ++ l₂, p a) :
     (l₁ ++ l₂).pmap f h =
       (l₁.pmap f fun a ha => h a (mem_append_left l₂ ha)) ++
@@ -555,50 +521,47 @@ theorem pmap_append' {p : α → Prop} {f : ∀ a : α, p a → β} {l₁ l₂ :
       l₁.pmap f h₁ ++ l₂.pmap f h₂ :=
   pmap_append _
 
-@[simp, grind =] theorem attach_append {xs ys : List α} :
+@[simp] theorem attach_append {xs ys : List α} :
     (xs ++ ys).attach = xs.attach.map (fun ⟨x, h⟩ => ⟨x, mem_append_left ys h⟩) ++
       ys.attach.map fun ⟨x, h⟩ => ⟨x, mem_append_right xs h⟩ := by
   simp only [attach, attachWith, map_pmap, pmap_append]
   congr 1 <;>
   exact pmap_congr_left _ fun _ _ _ _ => rfl
 
-@[simp, grind =] theorem attachWith_append {P : α → Prop} {xs ys : List α}
+@[simp] theorem attachWith_append {P : α → Prop} {xs ys : List α}
     {H : ∀ (a : α), a ∈ xs ++ ys → P a} :
     (xs ++ ys).attachWith P H = xs.attachWith P (fun a h => H a (mem_append_left ys h)) ++
       ys.attachWith P (fun a h => H a (mem_append_right xs h)) := by
   simp only [attachWith, pmap_append]
 
-@[simp, grind =] theorem pmap_reverse {P : α → Prop} {f : (a : α) → P a → β} {xs : List α}
+@[simp] theorem pmap_reverse {P : α → Prop} {f : (a : α) → P a → β} {xs : List α}
     (H : ∀ (a : α), a ∈ xs.reverse → P a) :
     xs.reverse.pmap f H = (xs.pmap f (fun a h => H a (by simpa using h))).reverse := by
   induction xs <;> simp_all
 
-@[grind =]
 theorem reverse_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : List α}
     (H : ∀ (a : α), a ∈ xs → P a) :
     (xs.pmap f H).reverse = xs.reverse.pmap f (fun a h => H a (by simpa using h)) := by
   rw [pmap_reverse]
 
-@[simp, grind =] theorem attachWith_reverse {P : α → Prop} {xs : List α}
+@[simp] theorem attachWith_reverse {P : α → Prop} {xs : List α}
     {H : ∀ (a : α), a ∈ xs.reverse → P a} :
     xs.reverse.attachWith P H =
       (xs.attachWith P (fun a h => H a (by simpa using h))).reverse :=
   pmap_reverse ..
 
-@[grind =]
 theorem reverse_attachWith {P : α → Prop} {xs : List α}
     {H : ∀ (a : α), a ∈ xs → P a} :
     (xs.attachWith P H).reverse = (xs.reverse.attachWith P (fun a h => H a (by simpa using h))) :=
   reverse_pmap ..
 
-@[simp, grind =] theorem attach_reverse {xs : List α} :
+@[simp] theorem attach_reverse {xs : List α} :
     xs.reverse.attach = xs.attach.reverse.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
   simp only [attach, attachWith, reverse_pmap, map_pmap]
   apply pmap_congr_left
   intros
   rfl
 
-@[grind =]
 theorem reverse_attach {xs : List α} :
     xs.attach.reverse = xs.reverse.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
   simp only [attach, attachWith, reverse_pmap, map_pmap]
@@ -652,7 +615,7 @@ theorem countP_attachWith {p : α → Prop} {q : α → Bool} {l : List α} (H :
     (l.attachWith p H).countP (fun a : {x // p x} => q a) = l.countP q := by
   simp only [← Function.comp_apply (g := Subtype.val), ← countP_map, attachWith_map_subtype_val]
 
-@[simp]
+@[simp, grind =]
 theorem count_attach [BEq α] {l : List α} {a : {x // x ∈ l}} :
     l.attach.count a = l.count ↑a :=
   Eq.trans (countP_congr fun _ _ => by simp) <| countP_attach

src/Init/Data/List/Basic.lean

@@ -289,16 +289,6 @@ theorem cons_lex_nil [BEq α] {a} {as : List α} : lex (a :: as) [] lt = false :
 @[simp] theorem lex_nil [BEq α] {as : List α} : lex as [] lt = false := by
   cases as <;> simp [nil_lex_nil, cons_lex_nil]
 
-@[deprecated nil_lex_nil (since := "2025-02-10")]
-theorem lex_nil_nil [BEq α] : lex ([] : List α) [] lt = false := rfl
-@[deprecated nil_lex_cons (since := "2025-02-10")]
-theorem lex_nil_cons [BEq α] {b} {bs : List α} : lex [] (b :: bs) lt = true := rfl
-@[deprecated cons_lex_nil (since := "2025-02-10")]
-theorem lex_cons_nil [BEq α] {a} {as : List α} : lex (a :: as) [] lt = false := rfl
-@[deprecated cons_lex_cons (since := "2025-02-10")]
-theorem lex_cons_cons [BEq α] {a b} {as bs : List α} :
-    lex (a :: as) (b :: bs) lt = (lt a b || (a == b && lex as bs lt)) := rfl
-
 /-! ## Alternative getters -/
 
 /-! ### getLast -/

src/Init/Data/List/BasicAux.lean

@@ -21,65 +21,6 @@ namespace List
 
 /-! ## Alternative getters -/
 
-/-! ### get? -/
-
-/--
-Returns the `i`-th element in the list (zero-based).
-
-If the index is out of bounds (`i ≥ as.length`), this function returns `none`.
-Also see `get`, `getD` and `get!`.
--/
-@[deprecated "Use `a[i]?` instead." (since := "2025-02-12"), expose]
-def get? : (as : List α) → (i : Nat) → Option α
-  | a::_,  0   => some a
-  | _::as, n+1 => get? as n
-  | _,     _   => none
-
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]?` instead." (since := "2025-02-12"), simp]
-theorem get?_nil : @get? α [] n = none := rfl
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]?` instead." (since := "2025-02-12"), simp]
-theorem get?_cons_zero : @get? α (a::l) 0 = some a := rfl
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]?` instead." (since := "2025-02-12"), simp]
-theorem get?_cons_succ : @get? α (a::l) (n+1) = get? l n := rfl
-
-set_option linter.deprecated false in
-@[deprecated "Use `List.ext_getElem?`." (since := "2025-02-12")]
-theorem ext_get? : ∀ {l₁ l₂ : List α}, (∀ n, l₁.get? n = l₂.get? n) → l₁ = l₂
-  | [], [], _ => rfl
-  | _ :: _, [], h => nomatch h 0
-  | [], _ :: _, h => nomatch h 0
-  | a :: l₁, a' :: l₂, h => by
-    have h0 : some a = some a' := h 0
-    injection h0 with aa; simp only [aa, ext_get? fun n => h (n+1)]
-
-/-! ### get! -/
-
-/--
-Returns the `i`-th element in the list (zero-based).
-
-If the index is out of bounds (`i ≥ as.length`), this function panics when executed, and returns
-`default`. See `get?` and `getD` for safer alternatives.
--/
-@[deprecated "Use `a[i]!` instead." (since := "2025-02-12"), expose]
-def get! [Inhabited α] : (as : List α) → (i : Nat) → α
-  | a::_,  0   => a
-  | _::as, n+1 => get! as n
-  | _,     _   => panic! "invalid index"
-
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]
-theorem get!_nil [Inhabited α] (n : Nat) : [].get! n = (default : α) := rfl
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]
-theorem get!_cons_succ [Inhabited α] (l : List α) (a : α) (n : Nat) :
-    (a::l).get! (n+1) = get! l n := rfl
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]
-theorem get!_cons_zero [Inhabited α] (l : List α) (a : α) : (a::l).get! 0 = a := rfl
-
 /-! ### getD -/
 
 /--
@@ -281,17 +222,6 @@ theorem getElem_append_right {as bs : List α} {i : Nat} (h₁ : as.length ≤ i
     cases i with simp [Nat.succ_sub_succ] <;> simp at h₁
     | succ i => apply ih; simp [h₁]
 
-@[deprecated "Deprecated without replacement." (since := "2025-02-13")]
-theorem get_last {as : List α} {i : Fin (length (as ++ [a]))} (h : ¬ i.1 < as.length) : (as ++ [a] : List _).get i = a := by
-  cases i; rename_i i h'
-  induction as generalizing i with
-  | nil => cases i with
-    | zero => simp [List.get]
-    | succ => simp +arith at h'
-  | cons a as ih =>
-    cases i with simp at h
-    | succ i => apply ih; simp [h]
-
 theorem sizeOf_lt_of_mem [SizeOf α] {as : List α} (h : a ∈ as) : sizeOf a < sizeOf as := by
   induction h with
   | head => simp +arith

src/Init/Data/List/Count.lean

@@ -13,7 +13,7 @@ public section
 /-!
 # Lemmas about `List.countP` and `List.count`.
 
-Because we mark `countP_eq_length_filter` and `count_eq_countP` with `@[grind _=_]`,
+Because we mark `countP_eq_length_filter` with `@[grind =]`,
 we don't need many other `@[grind]` annotations here.
 -/
 
@@ -66,7 +66,7 @@ theorem length_eq_countP_add_countP (p : α → Bool) {l : List α} : length l =
       · rfl
       · simp [h]
 
-@[grind _=_]  -- This to quite aggressive, as it introduces `filter` based reasoning whenever we see `countP`.
+@[grind =]  -- This to quite aggressive, as it introduces `filter` based reasoning whenever we see `countP`.
 theorem countP_eq_length_filter {l : List α} : countP p l = (filter p l).length := by
   induction l with
   | nil => rfl

src/Init/Data/List/Find.lean

@@ -360,9 +360,6 @@ theorem find?_flatten_eq_none_iff {xs : List (List α)} {p : α → Bool} :
     xs.flatten.find? p = none ↔ ∀ ys ∈ xs, ∀ x ∈ ys, !p x := by
   simp
 
-@[deprecated find?_flatten_eq_none_iff (since := "2025-02-03")]
-abbrev find?_flatten_eq_none := @find?_flatten_eq_none_iff
-
 /--
 If `find? p` returns `some a` from `xs.flatten`, then `p a` holds, and
 some list in `xs` contains `a`, and no earlier element of that list satisfies `p`.
@@ -403,9 +400,6 @@ theorem find?_flatten_eq_some_iff {xs : List (List α)} {p : α → Bool} {a :
     · exact h₁ l ml a m
     · exact h₂ a m
 
-@[deprecated find?_flatten_eq_some_iff (since := "2025-02-03")]
-abbrev find?_flatten_eq_some := @find?_flatten_eq_some_iff
-
 @[simp, grind =] theorem find?_flatMap {xs : List α} {f : α → List β} {p : β → Bool} :
     (xs.flatMap f).find? p = xs.findSome? (fun x => (f x).find? p) := by
   simp [flatMap_def, findSome?_map]; rfl
@@ -434,16 +428,10 @@ theorem find?_replicate_eq_none_iff {n : Nat} {a : α} {p : α → Bool} :
     (replicate n a).find? p = none ↔ n = 0 ∨ !p a := by
   simp [Classical.or_iff_not_imp_left]
 
-@[deprecated find?_replicate_eq_none_iff (since := "2025-02-03")]
-abbrev find?_replicate_eq_none := @find?_replicate_eq_none_iff
-
 @[simp] theorem find?_replicate_eq_some_iff {n : Nat} {a b : α} {p : α → Bool} :
     (replicate n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b := by
   cases n <;> simp
 
-@[deprecated find?_replicate_eq_some_iff (since := "2025-02-03")]
-abbrev find?_replicate_eq_some := @find?_replicate_eq_some_iff
-
 @[simp] theorem get_find?_replicate {n : Nat} {a : α} {p : α → Bool} (h) : ((replicate n a).find? p).get h = a := by
   cases n with
   | zero => simp at h
@@ -836,9 +824,6 @@ theorem of_findIdx?_eq_some {xs : List α} {p : α → Bool} (w : xs.findIdx? p
     simp_all only [findIdx?_cons]
     split at w <;> cases i <;> simp_all
 
-@[deprecated of_findIdx?_eq_some (since := "2025-02-02")]
-abbrev findIdx?_of_eq_some := @of_findIdx?_eq_some
-
 theorem of_findIdx?_eq_none {xs : List α} {p : α → Bool} (w : xs.findIdx? p = none) :
     ∀ i : Nat, match xs[i]? with | some a => ¬ p a | none => true := by
   intro i
@@ -854,9 +839,6 @@ theorem of_findIdx?_eq_none {xs : List α} {p : α → Bool} (w : xs.findIdx? p
       apply ih
       split at w <;> simp_all
 
-@[deprecated of_findIdx?_eq_none (since := "2025-02-02")]
-abbrev findIdx?_of_eq_none := @of_findIdx?_eq_none
-
 @[simp, grind _=_] theorem findIdx?_map {f : β → α} {l : List β} : findIdx? p (l.map f) = l.findIdx? (p ∘ f) := by
   induction l with
   | nil => simp

src/Init/Data/List/Lemmas.lean

@@ -107,9 +107,6 @@ theorem ne_nil_of_length_pos (_ : 0 < length l) : l ≠ [] := fun _ => nomatch l
 @[simp] theorem length_eq_zero_iff : length l = 0 ↔ l = [] :=
   ⟨eq_nil_of_length_eq_zero, fun h => h ▸ rfl⟩
 
-@[deprecated length_eq_zero_iff (since := "2025-02-24")]
-abbrev length_eq_zero := @length_eq_zero_iff
-
 theorem eq_nil_iff_length_eq_zero : l = [] ↔ length l = 0 :=
   length_eq_zero_iff.symm
 
@@ -142,18 +139,12 @@ theorem exists_cons_of_length_eq_add_one :
 theorem length_pos_iff {l : List α} : 0 < length l ↔ l ≠ [] :=
   Nat.pos_iff_ne_zero.trans (not_congr length_eq_zero_iff)
 
-@[deprecated length_pos_iff (since := "2025-02-24")]
-abbrev length_pos := @length_pos_iff
-
 theorem ne_nil_iff_length_pos {l : List α} : l ≠ [] ↔ 0 < length l :=
   length_pos_iff.symm
 
 theorem length_eq_one_iff {l : List α} : length l = 1 ↔ ∃ a, l = [a] :=
   ⟨fun h => match l, h with | [_], _ => ⟨_, rfl⟩, fun ⟨_, h⟩ => by simp [h]⟩
 
-@[deprecated length_eq_one_iff (since := "2025-02-24")]
-abbrev length_eq_one := @length_eq_one_iff
-
 /-! ### cons -/
 
 -- The arguments here are intentionally explicit.
@@ -198,38 +189,6 @@ We simplify `l.get i` to `l[i.1]'i.2` and `l.get? i` to `l[i]?`.
 @[simp, grind =]
 theorem get_eq_getElem {l : List α} {i : Fin l.length} : l.get i = l[i.1]'i.2 := rfl
 
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]?` instead." (since := "2025-02-12")]
-theorem get?_eq_none : ∀ {l : List α} {n}, length l ≤ n → l.get? n = none
-  | [], _, _ => rfl
-  | _ :: l, _+1, h => get?_eq_none (l := l) <| Nat.le_of_succ_le_succ h
-
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]?` instead." (since := "2025-02-12")]
-theorem get?_eq_get : ∀ {l : List α} {n} (h : n < l.length), l.get? n = some (get l ⟨n, h⟩)
-  | _ :: _, 0, _ => rfl
-  | _ :: l, _+1, _ => get?_eq_get (l := l) _
-
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]?` instead." (since := "2025-02-12")]
-theorem get?_eq_some_iff : l.get? n = some a ↔ ∃ h, get l ⟨n, h⟩ = a :=
-  ⟨fun e =>
-    have : n < length l := Nat.gt_of_not_le fun hn => by cases get?_eq_none hn ▸ e
-    ⟨this, by rwa [get?_eq_get this, Option.some.injEq] at e⟩,
-  fun ⟨_, e⟩ => e ▸ get?_eq_get _⟩
-
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]?` instead." (since := "2025-02-12")]
-theorem get?_eq_none_iff : l.get? n = none ↔ length l ≤ n :=
-  ⟨fun e => Nat.ge_of_not_lt (fun h' => by cases e ▸ get?_eq_some_iff.2 ⟨h', rfl⟩), get?_eq_none⟩
-
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]?` instead." (since := "2025-02-12"), simp]
-theorem get?_eq_getElem? {l : List α} {i : Nat} : l.get? i = l[i]? := by
-  simp only [getElem?_def]; split
-  · exact (get?_eq_get ‹_›)
-  · exact (get?_eq_none_iff.2 <| Nat.not_lt.1 ‹_›)
-
 /-! ### getElem!
 
 We simplify `l[i]!` to `(l[i]?).getD default`.
@@ -373,26 +332,9 @@ theorem getD_eq_getElem?_getD {l : List α} {i : Nat} {a : α} : getD l i a = (l
 theorem getD_cons_zero : getD (x :: xs) 0 d = x := by simp
 theorem getD_cons_succ : getD (x :: xs) (n + 1) d = getD xs n d := by simp
 
-/-! ### get!
-
-We simplify `l.get! i` to `l[i]!`.
--/
-
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]
-theorem get!_eq_getD [Inhabited α] : ∀ (l : List α) i, l.get! i = l.getD i default
-  | [], _      => rfl
-  | _a::_, 0   => by simp [get!]
-  | _a::l, n+1 => by simpa using get!_eq_getD l n
-
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]!` instead." (since := "2025-02-12"), simp]
-theorem get!_eq_getElem! [Inhabited α] (l : List α) (i) : l.get! i = l[i]! := by
-  simp [get!_eq_getD]
-
 /-! ### mem -/
 
-@[simp] theorem not_mem_nil {a : α} : ¬ a ∈ [] := nofun
+@[simp, grind ←] theorem not_mem_nil {a : α} : ¬ a ∈ [] := nofun
 
 @[simp, grind =] theorem mem_cons : a ∈ b :: l ↔ a = b ∨ a ∈ l :=
   ⟨fun h => by cases h <;> simp [Membership.mem, *],
@@ -581,15 +523,9 @@ theorem elem_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
 @[grind →]
 theorem nil_of_isEmpty {l : List α} (h : l.isEmpty) : l = [] := List.isEmpty_iff.mp h
 
-@[deprecated isEmpty_iff (since := "2025-02-17")]
-abbrev isEmpty_eq_true := @isEmpty_iff
-
 @[simp] theorem isEmpty_eq_false_iff {l : List α} : l.isEmpty = false ↔ l ≠ [] := by
   cases l <;> simp
 
-@[deprecated isEmpty_eq_false_iff (since := "2025-02-17")]
-abbrev isEmpty_eq_false := @isEmpty_eq_false_iff
-
 theorem isEmpty_eq_false_iff_exists_mem {xs : List α} :
     xs.isEmpty = false ↔ ∃ x, x ∈ xs := by
   cases xs <;> simp
@@ -2881,9 +2817,6 @@ theorem getLast_eq_head_reverse {l : List α} (h : l ≠ []) :
     l.getLast h = l.reverse.head (by simp_all) := by
   rw [← head_reverse]
 
-@[deprecated getLast_eq_iff_getLast?_eq_some (since := "2025-02-17")]
-abbrev getLast_eq_iff_getLast_eq_some := @getLast_eq_iff_getLast?_eq_some
-
 @[simp] theorem getLast?_eq_none_iff {xs : List α} : xs.getLast? = none ↔ xs = [] := by
   rw [getLast?_eq_head?_reverse, head?_eq_none_iff, reverse_eq_nil_iff]
 
@@ -3687,10 +3620,6 @@ theorem get_cons_succ' {as : List α} {i : Fin as.length} :
 theorem get_mk_zero : ∀ {l : List α} (h : 0 < l.length), l.get ⟨0, h⟩ = l.head (length_pos_iff.mp h)
   | _::_, _ => rfl
 
-set_option linter.deprecated false in
-@[deprecated "Use `a[0]?` instead." (since := "2025-02-12")]
-theorem get?_zero (l : List α) : l.get? 0 = l.head? := by cases l <;> rfl
-
 /--
 If one has `l.get i` in an expression (with `i : Fin l.length`) and `h : l = l'`,
 `rw [h]` will give a "motive is not type correct" error, as it cannot rewrite the
@@ -3700,18 +3629,6 @@ such a rewrite, with `rw [get_of_eq h]`.
 theorem get_of_eq {l l' : List α} (h : l = l') (i : Fin l.length) :
     get l i = get l' ⟨i, h ▸ i.2⟩ := by cases h; rfl
 
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]?` instead." (since := "2025-02-12")]
-theorem get!_of_get? [Inhabited α] : ∀ {l : List α} {n}, get? l n = some a → get! l n = a
-  | _a::_, 0, rfl => rfl
-  | _::l, _+1, e => get!_of_get? (l := l) e
-
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]
-theorem get!_len_le [Inhabited α] : ∀ {l : List α} {n}, length l ≤ n → l.get! n = (default : α)
-  | [], _, _ => rfl
-  | _ :: l, _+1, h => get!_len_le (l := l) <| Nat.le_of_succ_le_succ h
-
 theorem getElem!_nil [Inhabited α] {n : Nat} : ([] : List α)[n]! = default := rfl
 
 theorem getElem!_cons_zero [Inhabited α] {l : List α} : (a::l)[0]! = a := by
@@ -3737,30 +3654,11 @@ theorem get_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n, get l n = a := by
   obtain ⟨n, h, e⟩ := getElem_of_mem h
   exact ⟨⟨n, h⟩, e⟩
 
-set_option linter.deprecated false in
-@[deprecated getElem?_of_mem (since := "2025-02-12")]
-theorem get?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n, l.get? n = some a :=
-  let ⟨⟨n, _⟩, e⟩ := get_of_mem h; ⟨n, e ▸ get?_eq_get _⟩
-
 theorem get_mem : ∀ (l : List α) n, get l n ∈ l
   | _ :: _, ⟨0, _⟩ => .head ..
   | _ :: l, ⟨_+1, _⟩ => .tail _ (get_mem l ..)
 
-set_option linter.deprecated false in
-@[deprecated mem_of_getElem? (since := "2025-02-12")]
-theorem mem_of_get? {l : List α} {n a} (e : l.get? n = some a) : a ∈ l :=
-  let ⟨_, e⟩ := get?_eq_some_iff.1 e; e ▸ get_mem ..
-
 theorem mem_iff_get {a} {l : List α} : a ∈ l ↔ ∃ n, get l n = a :=
   ⟨get_of_mem, fun ⟨_, e⟩ => e ▸ get_mem ..⟩
 
-set_option linter.deprecated false in
-@[deprecated mem_iff_getElem? (since := "2025-02-12")]
-theorem mem_iff_get? {a} {l : List α} : a ∈ l ↔ ∃ n, l.get? n = some a := by
-  simp [getElem?_eq_some_iff, Fin.exists_iff, mem_iff_get]
-
-/-! ### Deprecations -/
-
-
-
 end List

src/Init/Data/List/Nat.lean

@@ -18,5 +18,3 @@ public import Init.Data.List.Nat.BEq
 public import Init.Data.List.Nat.Modify
 public import Init.Data.List.Nat.InsertIdx
 public import Init.Data.List.Nat.Perm
-
-public section

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

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

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

@@ -105,9 +105,6 @@ theorem length_leftpad {n : Nat} {a : α} {l : List α} :
     (leftpad n a l).length = max n l.length := by
   simp only [leftpad, length_append, length_replicate, Nat.sub_add_eq_max]
 
-@[deprecated length_leftpad (since := "2025-02-24")]
-abbrev leftpad_length := @length_leftpad
-
 theorem length_rightpad {n : Nat} {a : α} {l : List α} :
     (rightpad n a l).length = max n l.length := by
   simp [rightpad]

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

@@ -14,10 +14,19 @@ public section
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
+protected theorem Nat.sum_pos_iff_exists_pos {l : List Nat} : 0 < l.sum ↔ ∃ x ∈ l, 0 < x := by
+  induction l with
+  | nil => simp
+  | cons x xs ih =>
+    simp [← ih]
+    omega
+
 namespace List
 
 open Nat
 
+/-! ### Results about `List.sum` specialized to `Nat` -/
+
 theorem find?_eq_some_iff_getElem {xs : List α} {p : α → Bool} {b : α} :
     xs.find? p = some b ↔ p b ∧ ∃ i h, xs[i] = b ∧ ∀ j : Nat, (hj : j < i) → !p xs[j] := by
   rw [find?_eq_some_iff_append]

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

@@ -196,9 +196,6 @@ theorem getElem_insertIdx_of_gt {l : List α} {x : α} {i j : Nat} (hn : i < j)
         | zero => omega
         | succ j => simp
 
-@[deprecated getElem_insertIdx_of_gt (since := "2025-02-04")]
-abbrev getElem_insertIdx_of_ge := @getElem_insertIdx_of_gt
-
 @[grind =]
 theorem getElem_insertIdx {l : List α} {x : α} {i j : Nat} (h : j < (l.insertIdx i x).length) :
     (l.insertIdx i x)[j] =
@@ -261,9 +258,6 @@ theorem getElem?_insertIdx_of_gt {l : List α} {x : α} {i j : Nat} (h : i < j)
     (l.insertIdx i x)[j]? = l[j - 1]? := by
   rw [getElem?_insertIdx, if_neg (by omega), if_neg (by omega)]
 
-@[deprecated getElem?_insertIdx_of_gt (since := "2025-02-04")]
-abbrev getElem?_insertIdx_of_ge := @getElem?_insertIdx_of_gt
-
 end InsertIdx
 
 end List