fix: grind sort internalization

This PR ensures sorts are internalized by `grind`.

.github/workflows/build-template.yml

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

.github/workflows/ci.yml

@@ -213,7 +213,7 @@ jobs:
               },*/
               {
                 "name": "macOS",
-                "os": "macos-15-intel",
+                "os": "macos-13",
                 "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-sequoia-arm64-6x14" : "macos-15",
+                "os": large && !isPr ? "nscloud-macos-sonoma-arm64-6x14" : "macos-14",
                 "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
                 "release": true,
                 "shell": "bash -euxo pipefail {0}",

.github/workflows/update-stage0.yml

@@ -69,10 +69,10 @@ jobs:
           build/stage1/**/*.ir
           build/stage1/**/*.c
           build/stage1/**/*.c.o*
-        key: Linux Lake-build-v4-${{ github.sha }}
+        key: Linux Lake-build-v3-${{ github.sha }}
         # fall back to (latest) previous cache
         restore-keys: |
-          Linux Lake-build-v4
+          Linux Lake-build-v3
     - 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.
-      --^ completion
+      --^ textDocument/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

lean.code-workspace

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

script/Modulize.lean

@@ -1,91 +0,0 @@
-import Lake.CLI.Main
-
-/-!
-A simple script that inserts `module` and `@[expose] public section` into un-modulized files and
-bumps their imports to `public`.
--/
-
-open Lean Parser.Module
-
-def main (args : List String) : IO Unit := do
-  initSearchPath (← findSysroot)
-  -- the list of root modules
-  let mut mods := args.toArray.map (·.toName)
-
-  if mods.isEmpty then
-    -- Determine default module(s) to run modulize on
-    mods ← 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 #[]
-
-  -- 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 env ← importModules imps {}
-
-  let srcSearchPath ← getSrcSearchPath
-
-  for mod in env.header.moduleNames do
-    if !pkg.isPrefixOf mod then
-      continue
-
-    -- Parse the input file
-    let some path ← srcSearchPath.findModuleWithExt "lean" mod
-      | throw <| .userError "error: failed to find source file for {mod}"
-    let mut text ← IO.FS.readFile path
-    let inputCtx := Parser.mkInputContext text path.toString
-    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
-
-    let looksMeta := mod.components.any (· ∈ [`Tactic, `Linter])
-
-    -- initial whitespace if empty header
-    let startPos := header.raw.getPos? |>.getD parserState.pos
-
-    -- insert section if any trailing text
-    if header.raw.getTrailingTailPos?.all (· < text.endPos) then
-      let insertPos := header.raw.getTailPos? |>.getD startPos  -- empty header
-      let mut sec := if looksMeta then
-        "public meta section"
-      else
-        "@[expose] public section"
-      if !imps.isEmpty then
-        sec := "\n\n" ++ sec
-      if header.raw.getTailPos?.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 looksMeta 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

@@ -1,584 +0,0 @@
-/-
-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

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

script/lean-toolchain

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

src/CMakeLists.txt

@@ -797,9 +797,6 @@ 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()
@@ -847,13 +844,15 @@ 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_BUILD_TYPE} MATCHES "Debug|Release|RelWithDebInfo|MinSizeRel")
-  set(CMAKE_BUILD_TYPE_TOML "${CMAKE_BUILD_TYPE}")
-else()
-  set(CMAKE_BUILD_TYPE_TOML "Release")
+if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
+  set(LAKE_LIB_PREFIX "lib")
 endif()
 
 if(USE_LAKE)

src/Init/Classical.lean

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

src/Init/Control.lean

@@ -16,3 +16,5 @@ 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,3 +10,5 @@ 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,8 +9,6 @@ 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
@@ -112,121 +110,6 @@ 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,3 +9,5 @@ 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,6 +64,10 @@ 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,14 +39,13 @@ 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, expose]
+@[always_inline, inline]
 protected def bind (x : OptionT m α) (f : α → OptionT m β) : OptionT m β := OptionT.mk do
   match (← x) with
   | some a => f a
@@ -55,7 +54,7 @@ protected def bind (x : OptionT m α) (f : α → OptionT m β) : OptionT m β :
 /--
 Succeeds with the provided value.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 protected def pure (a : α) : OptionT m α := OptionT.mk do
   pure (some a)
 

src/Init/Core.lean

@@ -144,9 +144,8 @@ 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.
-/-- Implementation detail. -/
-@[inline] def Thunk.fnImpl (x : Thunk α) : Unit → α := fun _ => x.get
-@[csimp] theorem Thunk.fn_eq_fnImpl : @Thunk.fn = @Thunk.fnImpl := rfl
+@[inline] private def Thunk.fnImpl (x : Thunk α) : Unit → α := fun _ => x.get
+@[csimp] private 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
@@ -1606,7 +1605,7 @@ gen_injective_theorems% PSigma
 gen_injective_theorems% PSum
 gen_injective_theorems% Sigma
 gen_injective_theorems% String
-gen_injective_theorems% String.Pos.Raw
+gen_injective_theorems% String.Pos
 gen_injective_theorems% Substring
 gen_injective_theorems% Subtype
 gen_injective_theorems% Sum

src/Init/Data.lean

@@ -30,7 +30,6 @@ 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
@@ -53,3 +52,5 @@ 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,3 +30,5 @@ 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] def pmapImpl {P : α → Prop} (f : ∀ a, P a → β) (xs : Array α) (H : ∀ a ∈ xs, P a) :
+@[inline] private 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] theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by
+@[csimp] private 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] theorem pmap_empty {P : α → Prop} (f : ∀ a, P a → β) : pmap f #[] (by simp) = #[] := rfl
+@[simp, grind =] theorem pmap_empty {P : α → Prop} (f : ∀ a, P a → β) : pmap f #[] (by simp) = #[] := rfl
 
-@[simp] theorem pmap_push {P : α → Prop} (f : ∀ a, P a → β) (a : α) (xs : Array α) (h : ∀ b ∈ xs.push a, P b) :
+@[simp, grind =] 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] theorem attach_empty : (#[] : Array α).attach = #[] := rfl
+@[simp, grind =] theorem attach_empty : (#[] : Array α).attach = #[] := rfl
 
-@[simp] theorem attachWith_empty {P : α → Prop} (H : ∀ x ∈ #[], P x) : (#[] : Array α).attachWith P H = #[] := rfl
+@[simp, grind =] 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,11 +125,13 @@ 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
@@ -145,14 +147,14 @@ theorem attachWith_congr {xs ys : Array α} (w : xs = ys) {P : α → Prop} {H :
   subst w
   simp
 
-@[simp] theorem attach_push {a : α} {xs : Array α} :
+@[simp, grind =] 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] theorem attachWith_push {a : α} {xs : Array α} {P : α → Prop} {H : ∀ x ∈ xs.push a, P x} :
+@[simp, grind =] 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
@@ -174,6 +176,9 @@ 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
@@ -182,6 +187,9 @@ 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
@@ -286,23 +294,25 @@ 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] theorem pmap_attach {xs : Array α} {p : {x // x ∈ xs} → Prop} {f : ∀ a, p a → β} (H) :
+@[simp, grind =] 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] theorem pmap_attachWith {xs : Array α} {p : {x // q x} → Prop} {f : ∀ a, p a → β} (H₁ H₂) :
+@[simp, grind =] 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
@@ -360,18 +370,20 @@ 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] theorem map_attachWith {xs : Array α} {P : α → Prop} {H : ∀ (a : α), a ∈ xs → P a}
+@[simp, grind =] 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
@@ -389,6 +401,9 @@ 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
@@ -424,6 +439,7 @@ 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
@@ -431,7 +447,7 @@ theorem pmap_pmap {p : α → Prop} {q : β → Prop} {g : ∀ a, p a → β} {f
   cases xs
   simp [List.pmap_pmap, List.pmap_map]
 
-@[simp] theorem pmap_append {p : ι → Prop} {f : ∀ a : ι, p a → α} {xs ys : Array ι}
+@[simp, grind =] 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)) ++
@@ -446,7 +462,7 @@ theorem pmap_append' {p : α → Prop} {f : ∀ a : α, p a → β} {xs ys : Arr
       xs.pmap f h₁ ++ ys.pmap f h₂ :=
   pmap_append _
 
-@[simp] theorem attach_append {xs ys : Array α} :
+@[simp, grind =] 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
@@ -454,59 +470,62 @@ 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] theorem attachWith_append {P : α → Prop} {xs ys : Array α}
+@[simp, grind =] 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] theorem pmap_reverse {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
+@[simp, grind =] 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] theorem attachWith_reverse {P : α → Prop} {xs : Array α}
+@[simp, grind =] 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] theorem attach_reverse {xs : Array α} :
+@[simp, grind =] 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] theorem back?_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
+@[simp, grind =] 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] theorem back?_attachWith {P : α → Prop} {xs : Array α}
+@[simp, grind =] 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]
+@[simp, grind =]
 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,11 +129,20 @@ 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
 
@@ -403,6 +412,10 @@ 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.
 
@@ -1799,6 +1812,7 @@ 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,6 +24,29 @@ 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
@@ -85,6 +108,9 @@ 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,13 +324,6 @@ 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,6 +278,9 @@ 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`.
@@ -303,6 +306,9 @@ 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
@@ -312,11 +318,17 @@ 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]
@@ -334,19 +346,34 @@ 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,6 +80,9 @@ 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
 
@@ -104,10 +107,17 @@ 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
@@ -361,7 +371,6 @@ 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
@@ -533,12 +542,18 @@ 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]
 
@@ -2981,6 +2996,11 @@ 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
@@ -3566,6 +3586,8 @@ 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⟩
@@ -4690,3 +4712,44 @@ 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,3 +8,5 @@ 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
-public import Init.Data.Range.Polymorphic.Iterators
-public import Init.Data.Range.Polymorphic.Nat
+import Init.Data.Range.Polymorphic.Iterators
+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.Rco.lt_upper_of_mem h
+    have : i < min as.size bs.size := Std.PRange.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,7 +42,8 @@ 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
-  simp [lex, Std.Rco.forIn'_eq_if]
+  rw [lex, Std.PRange.forIn'_eq_match]
+  simp [Std.PRange.SupportsUpperBound.IsSatisfied]
 
 private theorem cons_lex_cons.forIn'_congr_aux [Monad m] {as bs : ρ} {_ : Membership α ρ}
     [ForIn' m ρ α inferInstance] (w : as = bs)
@@ -63,13 +64,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.Rco.forIn'_eq_forIn'_toList]
+    Nat.add_min_add_left, Nat.add_lt_add_iff_left, Std.PRange.forIn'_eq_forIn'_toList]
   conv =>
     lhs; congr; congr
-    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 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 (if_pos (by omega)) rfl (fun _ _ _ => rfl)]
-  simp only [Std.toList_Roo_eq_toList_Rco_of_isSome_succ? (lo := 0) (h := rfl),
+  simp only [Std.PRange.toList_Rox_eq_toList_Rcx_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]
@@ -82,10 +83,16 @@ 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₂ <;> simp [lex, Std.Rco.forIn'_eq_if]
+    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]
   | cons x l₁ ih =>
     cases l₂ with
-    | nil => simp [lex, Std.Rco.forIn'_eq_if]
+    | nil =>
+      rw [lex, Std.PRange.forIn'_eq_match]
+      simp [Std.PRange.SupportsUpperBound.IsSatisfied]
     | cons y l₂ =>
       rw [List.toArray_cons, List.toArray_cons y, cons_lex_cons, List.lex, ih]
 

src/Init/Data/Array/QSort.lean

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

src/Init/Data/Array/Subarray.lean

@@ -7,7 +7,6 @@ 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,3 +16,5 @@ 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,3 +13,5 @@ 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,6 +29,10 @@ 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,7 +17,6 @@ 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,7 +9,6 @@ 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,7 +8,6 @@ module
 
 prelude
 public import Init.Data.BitVec.Bootstrap
-import Init.Ext
 
 public section
 
@@ -50,11 +49,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) (by exact Classical.not_forall_not)
+  decidable_of_iff (¬ ∀ v, ¬ P v) 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) (by exact Classical.not_forall_not)
+  decidable_of_iff (¬ ∀ v, ¬ P v) 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,9 +22,6 @@ 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
 
@@ -77,6 +74,10 @@ 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
 
@@ -349,14 +350,25 @@ 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])
@@ -6349,4 +6361,15 @@ 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,3 +10,5 @@ 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,8 +13,6 @@ 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
 
@@ -36,40 +34,18 @@ instance : Inhabited ByteArray where
 instance : EmptyCollection ByteArray where
   emptyCollection := ByteArray.empty
 
-/--
-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]
@@ -80,65 +56,37 @@ 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", inherit_doc ByteArray.set]
+@[extern "lean_byte_array_uset"]
 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
 
 /--
-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.
--/
+  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. -/
 @[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
@@ -165,9 +113,6 @@ 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
@@ -178,12 +123,16 @@ def toList (bs : ByteArray) : List UInt8 :=
     decreasing_by decreasing_trivial_pre_omega
   loop 0 []
 
-/--
-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`.
+@[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
 
-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
@@ -195,29 +144,11 @@ The index is returned along with a proof that it is a valid index in the array.
   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`.
+  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.
 
-The variant {name}`findFinIdx?` additionally returns a proof that the found index is in bounds.
+  TODO: avoid code duplication in the future after we improve the compiler.
 -/
-@[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
@@ -230,11 +161,7 @@ We claim this unsafe implementation is correct because an array cannot have more
       pure b
   loop 0 b
 
-/--
-The reference implementation of {name}`ForIn.forIn` for {name}`ByteArray`.
-
-In compiled code, this is replaced by the more efficient {name}`ByteArray.forInUnsafe`.
--/
+/-- Reference implementation for `forIn` -/
 @[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
@@ -252,13 +179,7 @@ protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteAr
 instance : ForIn m ByteArray UInt8 where
   forIn := ByteArray.forIn
 
-/--
-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.
--/
+/-- See comment at `forInUnsafe` -/
 -- 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 β :=
@@ -275,14 +196,7 @@ unsafe def foldlMUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (f : β
   else
     pure init
 
-/--
-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.
--/
+/-- Reference implementation for `foldlM` -/
 @[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) :=
@@ -300,23 +214,11 @@ 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
 
-set_option doc.verso false -- Awaiting intra-module forward reference support
-/--
-Iterator over the bytes (`UInt8`) of a `ByteArray`.
+/-- Iterator over the bytes (`UInt8`) of a `ByteArray`.
 
 Typically created by `arr.iter`, where `arr` is a `ByteArray`.
 
@@ -340,7 +242,6 @@ 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 :=
@@ -358,25 +259,16 @@ theorem Iterator.sizeOf_eq (i : Iterator) : sizeOf i = i.array.size - i.idx :=
 
 namespace Iterator
 
-/--
-The number of bytes remaining in the iterator.
--/
+/-- Number of bytes remaining in the iterator. -/
 def remainingBytes : Iterator → Nat
   | ⟨arr, i⟩ => arr.size - i
 
 @[inherit_doc Iterator.idx]
 def pos := Iterator.idx
 
-/-- True if the iterator is past the array's last byte. -/
-@[inline]
-def atEnd : Iterator → Bool
-  | ⟨arr, i⟩ => i ≥ arr.size
+/-- The byte at the current position.
 
-/--
-The byte at the current position.
-
-On an invalid position, returns {lean}`(default : UInt8)`.
--/
+On an invalid position, returns `(default : UInt8)`. -/
 @[inline]
 def curr : Iterator → UInt8
   | ⟨arr, i⟩ =>
@@ -385,28 +277,27 @@ 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.*
-{name}`Iterator.atEnd` is {name}`false`; otherwise, the resulting iterator will be invalid.
--/
+`Iterator.atEnd` is `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 valid; that is, it is not past the array's last byte.
--/
+/-- 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. -/
 @[inline]
 def hasNext : Iterator → Bool
   | ⟨arr, i⟩ => i < arr.size
@@ -432,21 +323,17 @@ 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.
 
-Given {given}`i : ByteArray.Iterator`, note that {lean}`i.toEnd.atEnd` is always {name}`true`.
--/
+Note that `i.toEnd.atEnd` is always `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⟩
@@ -454,11 +341,9 @@ 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,19 +10,12 @@ 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,13 +9,7 @@ prelude
 public import Init.Data.ByteArray.Basic
 import Init.Data.String.Basic
 
-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.
--/
+/-- Interpret a `ByteArray` of size 8 as a little-endian `UInt64`. -/
 public def ByteArray.toUInt64LE! (bs : ByteArray) : UInt64 :=
   assert! bs.size == 8
   (bs.get! 7).toUInt64 <<< 0x38 |||
@@ -27,11 +21,7 @@ public def ByteArray.toUInt64LE! (bs : ByteArray) : UInt64 :=
   (bs.get! 1).toUInt64 <<< 0x8  |||
   (bs.get! 0).toUInt64
 
-/--
-Interprets a {name}`ByteArray` of size 8 as a big-endian {name}`UInt64`.
-
-Panics if the array's size is not 8.
--/
+/-- Interpret a `ByteArray` of size 8 as a big-endian `UInt64`. -/
 public def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 :=
   assert! bs.size == 8
   (bs.get! 0).toUInt64 <<< 0x38 |||

src/Init/Data/ByteArray/Lemmas.lean

@@ -11,13 +11,6 @@ public import Init.Data.Array.Extract
 
 public section
 
--- At present the preferred normal form for empty byte arrays is `ByteArray.empty`
-@[simp]
-theorem emptyc_eq_empty : (∅ : ByteArray) = ByteArray.empty := rfl
-
-@[simp]
-theorem emptyWithCapacity_eq_empty : ByteArray.emptyWithCapacity 0 = ByteArray.empty := rfl
-
 @[simp]
 theorem ByteArray.data_empty : ByteArray.empty.data = #[] := rfl
 
@@ -167,9 +160,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 j : Nat} (hi : i = a.size) (hj : j = a.size + b.size) :
-    (a ++ b).extract i j = b := by
-  subst hi hj
+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
   ext1
   simp [← size_data]
 

src/Init/Data/Char.lean

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

src/Init/Data/Fin.lean

@@ -11,3 +11,5 @@ 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, by exact Nat.lt_of_le_of_lt (Nat.mod_le _ _) h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨a % b,  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, by exact Nat.lt_of_le_of_lt (Nat.div_le_self _ _) h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨a / b, 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, by exact Nat.lt_of_le_of_lt (Nat.mod_le _ _) h⟩
+  | ⟨a, h⟩, m => ⟨a % m, Nat.lt_of_le_of_lt (Nat.mod_le _ _) h⟩
 
 /--
 Bitwise and.

src/Init/Data/Fin/Lemmas.lean

@@ -7,6 +7,7 @@ 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
@@ -326,9 +327,7 @@ 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⟩
-  · 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]
+  · 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)
 

src/Init/Data/FloatArray.lean

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

src/Init/Data/Format.lean

@@ -10,3 +10,5 @@ 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.Raw where
+instance : ToFormat String.Pos 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.Raw where
+instance : Hashable String.Pos where
   hash p := UInt64.ofNat p.byteIdx
 
 instance [Hashable α] [Hashable β] : Hashable (α × β) where
@@ -76,3 +76,22 @@ 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,3 +18,5 @@ 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,3 +8,5 @@ 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,7 +9,6 @@ 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,3 +9,5 @@ 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,6 +206,9 @@ 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,7 +13,6 @@ 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
 
@@ -123,8 +122,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 a b =>
-  decidable_of_decidable_of_iff (p := b % a = 0) (by exact (dvd_iff_emod_eq_zero ..).symm)
+instance decidableDvd : DecidableRel (α := Int) (· ∣ ·) := fun _ _ =>
+  decidable_of_decidable_of_iff (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,6 +8,7 @@ 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,20 +88,6 @@ 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,6 +1347,8 @@ 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,9 +50,14 @@ 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 _)⟩
 
--- This can't be removed until the next update-stage0
+@[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
+
 @[deprecated Nat.pow_pos (since := "2025-02-17")]
-abbrev _root_.Nat.pos_pow_of_pos := @Nat.pow_pos
+abbrev 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,3 +9,5 @@ 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,3 +8,5 @@ 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,3 +13,5 @@ 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,3 +10,5 @@ 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,3 +8,5 @@ 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,3 +8,5 @@ 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,3 +10,5 @@ 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,7 +195,8 @@ 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
@@ -316,119 +317,4 @@ 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,3 +9,5 @@ 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,129 +414,4 @@ 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,3 +9,5 @@ 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,32 +44,20 @@ 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} {m : Type w → Type w'} [Monad m]
-    [Iterator α Id β] [Finite α Id] [IteratorLoop α Id m]
+@[congr] theorem Iter.forIn'_congr {α β : Type w}
+    [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id]
     {ita itb : Iter (α := α) β} (w : ita = itb)
     {b b' : γ} (hb : b = b')
-    {f : (a' : β) → _ → γ → m (ForInStep γ)}
-    {g : (a' : β) → _ → γ → m (ForInStep γ)}
+    {f : (a' : β) → _ → γ → Id (ForInStep γ)}
+    {g : (a' : β) → _ → γ → Id (ForInStep γ)}
     (h : ∀ a m b, f a (by simpa [w] using m) b = g a m b) :
-    letI : ForIn' m (Iter (α := α) β) β _ := Iter.instForIn'
+    letI : ForIn' Id (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,3 +8,5 @@ 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,34 +60,20 @@ 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'}
-    {n : Type w → Type w''} [Monad n] [Monad m]
-    [Iterator α m β] [Finite α m] [IteratorLoop α m n] [MonadLiftT m n]
+@[congr] theorem IterM.forIn'_congr {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α m β] [Finite α m] [IteratorLoop α m m]
     {ita itb : IterM (α := α) m β} (w : ita = itb)
     {b b' : γ} (hb : b = b')
-    {f : (a' : β) → _ → γ → n (ForInStep γ)}
-    {g : (a' : β) → _ → γ → n (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' n (IterM (α := α) m β) β _ := IterM.instForIn'
+    letI : ForIn' m (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

@@ -1,30 +0,0 @@
-/-
-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,3 +31,5 @@ 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] def pmapImpl {P : α → Prop} (f : ∀ a, P a → β) (l : List α) (H : ∀ a ∈ l, P a) :
+@[inline] private 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] theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by
+@[csimp] private 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,12 +95,14 @@ 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
@@ -147,6 +149,9 @@ 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 _)
@@ -155,6 +160,9 @@ 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 _)
@@ -246,6 +254,13 @@ 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}
@@ -262,6 +277,15 @@ 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)) :=
@@ -283,13 +307,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] theorem pmap_attach {l : List α} {p : {x // x ∈ l} → Prop} {f : ∀ a, p a → β} (H) :
+@[simp, grind =] 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] theorem pmap_attachWith {l : List α} {p : {x // q x} → Prop} {f : ∀ a, p a → β} (H₁ H₂) :
+@[simp, grind =] 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
@@ -347,24 +371,26 @@ 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] theorem foldl_attachWith
+@[simp, grind =] 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] theorem foldr_attachWith
+@[simp, grind =] 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
@@ -403,16 +429,18 @@ 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] theorem map_attachWith {l : List α} {P : α → Prop} {H : ∀ (a : α), a ∈ l → P a}
+@[simp, grind =] 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
@@ -438,6 +466,10 @@ 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
@@ -468,6 +500,7 @@ 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
@@ -479,7 +512,7 @@ theorem attach_filter {l : List α} (p : α → Bool) :
 
 -- We are still missing here `attachWith_filterMap` and `attachWith_filter`.
 
-@[simp]
+@[simp, grind =]
 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
@@ -488,7 +521,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]
+@[simp, grind =]
 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
@@ -498,13 +531,14 @@ 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] theorem pmap_append {p : ι → Prop} {f : ∀ a : ι, p a → α} {l₁ l₂ : List ι}
+@[simp, grind =] 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)) ++
@@ -521,47 +555,50 @@ theorem pmap_append' {p : α → Prop} {f : ∀ a : α, p a → β} {l₁ l₂ :
       l₁.pmap f h₁ ++ l₂.pmap f h₂ :=
   pmap_append _
 
-@[simp] theorem attach_append {xs ys : List α} :
+@[simp, grind =] 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] theorem attachWith_append {P : α → Prop} {xs ys : List α}
+@[simp, grind =] 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] theorem pmap_reverse {P : α → Prop} {f : (a : α) → P a → β} {xs : List α}
+@[simp, grind =] 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] theorem attachWith_reverse {P : α → Prop} {xs : List α}
+@[simp, grind =] 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] theorem attach_reverse {xs : List α} :
+@[simp, grind =] 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]
@@ -615,7 +652,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, grind =]
+@[simp]
 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,6 +289,16 @@ 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,6 +21,65 @@ 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 -/
 
 /--
@@ -222,6 +281,17 @@ 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` with `@[grind =]`,
+Because we mark `countP_eq_length_filter` and `count_eq_countP` 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,6 +360,9 @@ 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`.
@@ -400,6 +403,9 @@ 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
@@ -428,10 +434,16 @@ 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
@@ -824,6 +836,9 @@ 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
@@ -839,6 +854,9 @@ 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,6 +107,9 @@ 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
 
@@ -139,12 +142,18 @@ 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.
@@ -189,6 +198,38 @@ 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`.
@@ -332,9 +373,26 @@ 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, grind ←] theorem not_mem_nil {a : α} : ¬ a ∈ [] := nofun
+@[simp] 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, *],
@@ -523,9 +581,15 @@ 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
@@ -2817,6 +2881,9 @@ 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]
 
@@ -3620,6 +3687,10 @@ 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
@@ -3629,6 +3700,18 @@ 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
@@ -3654,11 +3737,30 @@ 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,3 +18,5 @@ 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,7 +8,6 @@ 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,6 +105,9 @@ 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,19 +14,10 @@ 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,6 +196,9 @@ 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] =
@@ -258,6 +261,9 @@ 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

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

@@ -176,7 +176,7 @@ theorem modifyHead_eq_modify_zero (f : α → α) (l : List α) :
   | n, [], _+1 => by cases n <;> rfl
   | 0, _ :: l, j+1 => by cases h : l[j]? <;> simp [h, modify]
   | i+1, a :: l, j+1 => by
-    simp only [modify_succ_cons, getElem?_cons_succ, Option.map_eq_map]
+    simp only [modify_succ_cons, getElem?_cons_succ, Nat.reduceEqDiff, Option.map_eq_map]
     refine (getElem?_modify f i l j).trans ?_
     cases h' : l[j]? <;> by_cases h : i = j <;>
       simp [h, Option.map]

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

@@ -103,14 +103,14 @@ theorem range'_eq_append_iff : range' s n step = xs ++ ys ↔ ∃ k, k ≤ n ∧
       · simp only [ih] at h
         obtain ⟨k, h, rfl, rfl⟩ := h
         refine ⟨k + 1, ?_⟩
-        simp_all [range'_succ, Nat.add_assoc, (by omega : n + 1 - (k + 1) = n - k)]
+        simp_all [range'_succ, Nat.add_assoc]
     · rintro ⟨k, h, rfl, rfl⟩
       cases k with
       | zero => simp [range'_succ]
       | succ k =>
         simp only [range'_succ, reduceCtorEq, false_and, cons.injEq, true_and, ih, exists_eq_left', false_or]
         refine ⟨k, ?_⟩
-        simp_all [Nat.add_assoc, (by omega : n + 1 - (k + 1) = n - k)]
+        simp_all [Nat.add_assoc]
 
 @[simp] theorem find?_range'_eq_some {s n : Nat} {i : Nat} {p : Nat → Bool} :
     (range' s n).find? p = some i ↔ p i ∧ i ∈ range' s n ∧ ∀ j, s ≤ j → j < i → !p j := by
@@ -203,13 +203,7 @@ theorem sum_range' : (range' start n step).sum = n * start + n * (n - 1) * step
 theorem drop_range' : (List.range' start n step).drop k = List.range' (start + k * step) (n - k) step := by
   induction k generalizing start n with
   | zero => simp
-  | succ =>
-    cases n
-    · simp [*, Nat.add_mul, ← Nat.add_assoc, Nat.add_right_comm]
-    · simp only [range'_succ, drop_succ_cons, Nat.add_mul, Nat.one_mul, ← Nat.add_assoc,
-      Nat.add_right_comm, *]
-      rename_i n₁ _ n₂
-      rw [(by omega : n₂ + 1 - (n₁ + 1) = n₂ - n₁)]
+  | succ => cases n <;> simp [*, List.range'_succ, Nat.add_mul, ← Nat.add_assoc, Nat.add_right_comm]
 
 @[simp, grind =]
 theorem take_range'_of_length_le (h : n ≤ k) : (List.range' start n step).take k = List.range' start n step := by

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

@@ -117,6 +117,9 @@ theorem take_set_of_le {a : α} {i j : Nat} {l : List α} (h : j ≤ i) :
     next h' => rw [getElem?_set_ne (by omega)]
     · rfl
 
+@[deprecated take_set_of_le (since := "2025-02-04")]
+abbrev take_set_of_lt := @take_set_of_le
+
 @[simp, grind =] theorem take_replicate {a : α} : ∀ {i n : Nat}, take i (replicate n a) = replicate (min i n) a
   | n, 0 => by simp
   | 0, m => by simp
@@ -162,8 +165,8 @@ theorem take_eq_take_iff :
   | x :: xs, 0, j + 1 => by simp [succ_min_succ]
   | x :: xs, i + 1, j + 1 => by simp [succ_min_succ, take_eq_take_iff]
 
-theorem take_eq_take_min {l : List α} {i : Nat} : l.take i = l.take (min i l.length) := by
-  simp
+@[deprecated take_eq_take_iff (since := "2025-02-16")]
+abbrev take_eq_take := @take_eq_take_iff
 
 @[grind =]
 theorem take_add {l : List α} {i j : Nat} : l.take (i + j) = l.take i ++ (l.drop i).take j := by
@@ -370,8 +373,7 @@ theorem drop_take : ∀ {i j : Nat} {l : List α}, drop i (take j l) = take (j -
   | _, 0, _ => by simp
   | _, _, [] => by simp
   | i+1, j+1, h :: t => by
-    simp only [take_succ_cons, drop_succ_cons, drop_take, take_eq_take_iff, length_drop]
-    omega
+    simp [take_succ_cons, drop_succ_cons, drop_take]
 
 @[simp] theorem drop_take_self : drop i (take i l) = [] := by
   rw [drop_take]

src/Init/Data/List/OfFn.lean

@@ -6,8 +6,8 @@ Authors: Mario Carneiro, Kim Morrison
 module
 
 prelude
+public import Init.Data.List.Basic
 public import Init.Data.Fin.Fold
-public import Init.Data.List.Lemmas
 
 public section
 
@@ -114,7 +114,7 @@ theorem mem_ofFn {n} {f : Fin n → α} {a : α} : a ∈ ofFn f ↔ ∃ i, f i =
   rw [← getElem_zero (length_ofFn ▸ Nat.pos_of_ne_zero (mt ofFn_eq_nil_iff.2 h)),
     List.getElem_ofFn]
 
-@[grind =] theorem getLast_ofFn {n} {f : Fin n → α} (h : ofFn f ≠ []) :
+@[grind =]theorem getLast_ofFn {n} {f : Fin n → α} (h : ofFn f ≠ []) :
     (ofFn f).getLast h = f ⟨n - 1, Nat.sub_one_lt (mt ofFn_eq_nil_iff.2 h)⟩ := by
   simp [getLast_eq_getElem, length_ofFn, List.getElem_ofFn]
 

src/Init/Data/List/Sort.lean

@@ -9,3 +9,5 @@ prelude
 public import Init.Data.List.Sort.Basic
 public import Init.Data.List.Sort.Impl
 public import Init.Data.List.Sort.Lemmas
+
+public section

src/Init/Data/List/TakeDrop.lean

@@ -165,6 +165,9 @@ theorem take_set {l : List α} {i j : Nat} {a : α} :
     | nil => simp
     | cons hd tl => cases j <;> simp_all
 
+@[deprecated take_set (since := "2025-02-17")]
+abbrev set_take := @take_set
+
 theorem drop_set {l : List α} {i j : Nat} {a : α} :
     (l.set j a).drop i = if j < i then l.drop i else (l.drop i).set (j - i) a := by
   induction i generalizing l j with

src/Init/Data/Nat.lean

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

src/Init/Data/Nat/Basic.lean

@@ -19,12 +19,12 @@ namespace Nat
 
 /-- Compiled version of `Nat.rec` so that we can define `Nat.recAux` to be defeq to `Nat.rec`.
 This is working around the fact that the compiler does not currently support recursors. -/
-def recCompiled {motive : Nat → Sort u} (zero : motive zero) (succ : (n : Nat) → motive n → motive (Nat.succ n)) : (t : Nat) → motive t
+private def recCompiled {motive : Nat → Sort u} (zero : motive zero) (succ : (n : Nat) → motive n → motive (Nat.succ n)) : (t : Nat) → motive t
   | .zero => zero
   | .succ n => succ n (recCompiled zero succ n)
 
 @[csimp]
-theorem rec_eq_recCompiled : @Nat.rec = @Nat.recCompiled :=
+private theorem rec_eq_recCompiled : @Nat.rec = @Nat.recCompiled :=
   funext fun _ => funext fun _ => funext fun succ => funext fun t =>
     Nat.recOn t rfl (fun n ih => congrArg (succ n) ih)
 
@@ -791,6 +791,18 @@ protected theorem pow_le_pow_right {n : Nat} (hx : n > 0) {i : Nat} : ∀ {j}, i
     | Or.inr h =>
       h.symm ▸ Nat.le_refl _
 
+set_option linter.missingDocs false in
+@[deprecated Nat.pow_le_pow_left (since := "2025-02-17")]
+abbrev pow_le_pow_of_le_left := @Nat.pow_le_pow_left
+
+set_option linter.missingDocs false in
+@[deprecated Nat.pow_le_pow_right (since := "2025-02-17")]
+abbrev pow_le_pow_of_le_right := @Nat.pow_le_pow_right
+
+set_option linter.missingDocs false in
+@[deprecated Nat.pow_pos (since := "2025-02-17")]
+abbrev pos_pow_of_pos := @Nat.pow_pos
+
 @[simp] theorem zero_pow_of_pos (n : Nat) (h : 0 < n) : 0 ^ n = 0 := by
   cases n with
   | zero => cases h
@@ -870,6 +882,9 @@ protected theorem ne_zero_of_lt (h : b < a) : a ≠ 0 := by
   exact absurd h (Nat.not_lt_zero _)
   apply Nat.noConfusion
 
+@[deprecated Nat.ne_zero_of_lt (since := "2025-02-06")]
+theorem not_eq_zero_of_lt (h : b < a) : a ≠ 0 := Nat.ne_zero_of_lt h
+
 theorem pred_lt_of_lt {n m : Nat} (h : m < n) : pred n < n :=
   pred_lt (Nat.ne_zero_of_lt h)
 

src/Init/Data/Nat/Bitwise.lean

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

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

@@ -14,7 +14,6 @@ import all Init.Data.Nat.Bitwise.Basic
 public import Init.Data.Nat.Lemmas
 public import Init.Data.Nat.Simproc
 public import Init.TacticsExtra
-import Init.BinderPredicates
 
 public section
 

src/Init/Data/Nat/Div.lean

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