merge master

This adds a Python script that helps find which commit introduced a
behavior change in Lean. It supports multiple modes:

- Auto-discovery: Just provide a file and it searches backwards
- Nightly bisection: Binary search through nightly builds
- Version ranges: Convert v4.X.Y tags to nightly ranges
- Commit bisection: Search individual commits with CI artifact caching

Key features:
- Downloads pre-built CI artifacts when available (~30s vs 2-5min build)
- Caches artifacts in ~/.cache/lean-bisect/artifacts/
- Skips commits with failed CI builds automatically
- Supports short or full commit SHAs

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <noreply@anthropic.com>

.claude/CLAUDE.md

@@ -29,19 +29,6 @@ After rebuilding, LSP diagnostics may be stale until the user interacts with fil
 
 If the user expresses frustration with you, stop and ask them to help update this `.claude/CLAUDE.md` file with missing guidance.
 
-## Creating pull requests
+## Creating pull requests.
 
-Follow the commit convention in `doc/dev/commit_convention.md`.
-
-**Title format:** `<type>: <subject>` where type is one of: `feat`, `fix`, `doc`, `style`, `refactor`, `test`, `chore`, `perf`.
-Subject should use imperative present tense ("add" not "added"), no capitalization, no trailing period.
-
-**Body format:** The first paragraph must start with "This PR". This paragraph is automatically incorporated into release notes. Use imperative present tense. Include motivation and contrast with previous behavior when relevant.
-
-Example:
-```
-feat: add optional binder limit to `mkPatternFromTheorem`
-
-This PR adds a `num?` parameter to `mkPatternFromTheorem` to control how many
-leading quantifiers are stripped when creating a pattern.
-```
+All PRs must have a first paragraph starting with "This PR". This paragraph is automatically incorporated into release notes. Read `lean4/doc/dev/commit_convention.md` when making PRs.

.github/workflows/actionlint.yml

@@ -15,7 +15,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
     - name: Checkout
-      uses: actions/checkout@v6
+      uses: actions/checkout@v5
     - name: actionlint
       uses: raven-actions/actionlint@v2
       with:

.github/workflows/build-template.yml

@@ -67,13 +67,13 @@ jobs:
         if: runner.os == 'macOS'
       - name: Checkout
         if: (!endsWith(matrix.os, '-with-cache'))
-        uses: actions/checkout@v6
+        uses: actions/checkout@v5
         with:
           # the default is to use a virtual merge commit between the PR and master: just use the PR
           ref: ${{ github.event.pull_request.head.sha }}
       - name: Namespace Checkout
         if: endsWith(matrix.os, '-with-cache')
-        uses: namespacelabs/nscloud-checkout-action@v8
+        uses: namespacelabs/nscloud-checkout-action@v7
         with:
           ref: ${{ github.event.pull_request.head.sha }}
       - name: Open Nix shell once

.github/workflows/check-prelude.yml

@@ -7,7 +7,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@v6
+        uses: actions/checkout@v5
         with:
           # the default is to use a virtual merge commit between the PR and master: just use the PR
           ref: ${{ github.event.pull_request.head.sha }}

.github/workflows/check-stage0.yml

@@ -8,7 +8,7 @@ jobs:
   check-stage0-on-queue:
     runs-on: ubuntu-latest
     steps:
-    - uses: actions/checkout@v6
+    - uses: actions/checkout@v5
       with:
         ref: ${{ github.event.pull_request.head.sha }}
         fetch-depth: 0

.github/workflows/ci.yml

@@ -50,7 +50,7 @@ jobs:
 
     steps:
       - name: Checkout
-        uses: actions/checkout@v6
+        uses: actions/checkout@v5
         # don't schedule nightlies on forks
         if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4' || inputs.action == 'release nightly' || (startsWith(github.ref, 'refs/tags/') && github.repository == 'leanprover/lean4')
       - name: Set Nightly
@@ -434,7 +434,7 @@ jobs:
         with:
           path: artifacts
       - name: Release
-        uses: softprops/action-gh-release@a06a81a03ee405af7f2048a818ed3f03bbf83c7b
+        uses: softprops/action-gh-release@6da8fa9354ddfdc4aeace5fc48d7f679b5214090
         with:
           files: artifacts/*/*
           fail_on_unmatched_files: true
@@ -455,7 +455,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@v6
+        uses: actions/checkout@v5
         with:
           # needed for tagging
           fetch-depth: 0
@@ -480,7 +480,7 @@ jobs:
           echo -e "\n*Full commit log*\n" >> diff.md
           git log --oneline "$last_tag"..HEAD | sed 's/^/* /' >> diff.md
       - name: Release Nightly
-        uses: softprops/action-gh-release@a06a81a03ee405af7f2048a818ed3f03bbf83c7b
+        uses: softprops/action-gh-release@6da8fa9354ddfdc4aeace5fc48d7f679b5214090
         with:
           body_path: diff.md
           prerelease: true

.github/workflows/copyright-header.yml

@@ -6,7 +6,7 @@ jobs:
   check-lean-files:
     runs-on: ubuntu-latest
     steps:
-    - uses: actions/checkout@v6
+    - uses: actions/checkout@v5
 
     - name: Verify .lean files start with a copyright header.
       run: |

.github/workflows/pr-release.yml

@@ -71,7 +71,7 @@ jobs:
           GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
       - name: Release (short format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: softprops/action-gh-release@a06a81a03ee405af7f2048a818ed3f03bbf83c7b
+        uses: softprops/action-gh-release@6da8fa9354ddfdc4aeace5fc48d7f679b5214090
         with:
           name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }}
           # There are coredumps files here as well, but all in deeper subdirectories.
@@ -86,7 +86,7 @@ jobs:
 
       - name: Release (SHA-suffixed format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: softprops/action-gh-release@a06a81a03ee405af7f2048a818ed3f03bbf83c7b
+        uses: softprops/action-gh-release@6da8fa9354ddfdc4aeace5fc48d7f679b5214090
         with:
           name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }} (${{ steps.workflow-info.outputs.sourceHeadSha }})
           # There are coredumps files here as well, but all in deeper subdirectories.
@@ -387,7 +387,7 @@ jobs:
       # Checkout the Batteries repository with all branches
       - name: Checkout Batteries repository
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        uses: actions/checkout@v6
+        uses: actions/checkout@v5
         with:
           repository: leanprover-community/batteries
           token: ${{ secrets.MATHLIB4_BOT }}
@@ -447,7 +447,7 @@ jobs:
       # Checkout the mathlib4 repository with all branches
       - name: Checkout mathlib4 repository
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        uses: actions/checkout@v6
+        uses: actions/checkout@v5
         with:
           repository: leanprover-community/mathlib4-nightly-testing
           token: ${{ secrets.MATHLIB4_BOT }}
@@ -530,7 +530,7 @@ jobs:
       # Checkout the reference manual repository with all branches
       - name: Checkout mathlib4 repository
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true'
-        uses: actions/checkout@v6
+        uses: actions/checkout@v5
         with:
           repository: leanprover/reference-manual
           token: ${{ secrets.MANUAL_PR_BOT }}

.github/workflows/update-stage0.yml

@@ -27,7 +27,7 @@ jobs:
     # This action should push to an otherwise protected branch, so it
     # uses a deploy key with write permissions, as suggested at
     # https://stackoverflow.com/a/76135647/946226
-    - uses: actions/checkout@v6
+    - uses: actions/checkout@v5
       with:
         ssh-key: ${{secrets.STAGE0_SSH_KEY}}
     - run: echo "should_update_stage0=yes" >> "$GITHUB_ENV"

doc/style.md

@@ -810,7 +810,7 @@ Docstrings for constants should have the following structure:
 
 The **short summary** should be 1–3 sentences (ideally 1) and provide
 enough information for most readers to quickly decide whether the
-constant is relevant to their task. The first (or only) sentence of
+docstring is relevant to their task. The first (or only) sentence of
 the short summary should be a *sentence fragment* in which the subject
 is implied to be the documented item, written in present tense
 indicative, or a *noun phrase* that characterizes the documented
@@ -1123,110 +1123,6 @@ infix:50 " ⇔ " => Bijection
 recommended_spelling "bij" for "⇔" in [Bijection, «term_⇔_»]
 ```
 
-#### Tactics
-
-Docstrings for tactics should have the following structure:
-
-* Short summary
-* Details
-* Variants
-* Examples
-
-Sometimes more than one declaration is needed to implement what the user
-sees as a single tactic. In that case, only one declaration should have
-the associated docstring, and the others should have the `tactic_alt`
-attribute to mark them as an implementation detail.
-
-The **short summary** should be 1–3 sentences (ideally 1) and provide
-enough information for most readers to quickly decide whether the
-tactic is relevant to their task. The first (or only) sentence of
-the short summary should be a full sentence in which the subject
-is an example invocation of the tactic, written in present tense
-indicative. If the example tactic invocation names parameters, then the
-short summary may refer to them. For the example invocation, prefer the
-simplest or most typical example. Explain more complicated forms in the
-variants section. If needed, abbreviate the invocation by naming part of
-the syntax and expanding it in the next sentence. The summary should be
-written as a single paragraph.
-
-**Details**, if needed, may be 1-3 paragraphs that describe further
-relevant information. They may insert links as needed. This section
-should fully explain the scope of the tactic: its syntax format,
-on which goals it works and what the resulting goal(s) look like. It
-should be clear whether the tactic fails if it does not close the main
-goal and whether it creates any side goals. The details may include
-explanatory examples that can’t necessarily be machine checked and
-don’t fit the format.
-
-If the tactic is extensible using `macro_rules`, mention this in the
-details, with a link to `lean-manual://section/tactic-macro-extension`
-and give a one-line example. If the tactic provides an attribute or a
-command that allows the user to extend its behavior, the documentation
-on how to extend the tactic belongs to that attribute or command. In the
-tactic docstring, use a single sentence to refer the reader to this
-further documentation.
-
-**Variants**, if needed, should be a bulleted list describing different
-options and forms of the same tactic. The reader should be able to parse
-and understand the parts of a tactic invocation they are hovering over,
-using this list. Each list item should describe an individual variant
-and take one of two formats: the **short summary** as above, or a
-**named list item**. A named list item consists of a title in bold
-followed by an indented short paragraph.
-
-Variants should be explained from the perspective of the tactic's users, not
-their implementers. A tactic that is implemented as a single Lean parser may
-have multiple variants from the perspective of users, while a tactic that is
-implemented as multiple parsers may have no variants, but merely an optional
-part of the syntax.
-
-**Examples** should start with the line `Examples:` (or `Example:` if
-there’s exactly one). The section should consist of a sequence of code
-blocks, each showing a Lean declaration (usually with the `example`
-keyword) that invokes the tactic. When the effect of the tactic is not
-clear from the code, you can use code comments to describe this. Do
-not include text between examples, because it can be unclear whether
-the text refers to the code before or after the example.
-
-##### Example
-
-````
-`rw [e]` uses the expression `e` as a rewrite rule on the main goal,
-then tries to close the goal by "cheap" (reducible) `rfl`.
-
-If `e` is a defined constant, then the equational theorems associated with `e`
-are used. This provides a convenient way to unfold `e`. If `e` has parameters,
-the tactic will try to fill these in by unification with the matching part of
-the target. Parameters are only filled in once per rule, restricting which
-later rewrites can be found. Parameters that are not filled in after
-unification will create side goals. If the `rfl` fails to close the main goal,
-no error is raised.
-
-`rw` may fail to rewrite terms "under binders", such as `∀ x, ...` or `∃ x,
-...`. `rw` can also fail with a "motive is type incorrect" error in the context
-of dependent types. In these cases, consider using `simp only`.
-
-* `rw [e₁, ... eₙ]` applies the given rules sequentially.
-* `rw [← e]` or `rw [<- e]` applies the rewrite in the reverse direction.
-* `rw [e] at l` rewrites with `e` at location(s) `l`.
-* `rw (occs := .pos L) [e]`, where `L` is a literal list of natural numbers,
-  only rewrites the given occurrences in the target. Occurrences count from 1.
-* `rw (occs := .neg L) [e]`, where `L` is a literal list of natural numbers,
-  skips rewriting the given occurrences in the target. Occurrences count from 1.
-
-Examples:
-
-```lean
-example {a b : Nat} (h : a + a = b) : (a + a) + (a + a) = b + b := by rw [h]
-```
-
-```lean
-example {f : Nat -> Nat} (h : ∀ x, f x = 1) (a b : Nat) : f a = f b := by
-  rw [h] -- `rw` instantiates `h` only once, so this is equivalent to: `rw [h a]`
-  -- goal: ⊢ 1 = f b
-  rw [h] -- equivalent to: `rw [h b]`
-```
-````
 
 
 ## Dictionary

script/Shake.lean

@@ -338,14 +338,12 @@ where
                 deps := deps.union k {indMod}
       return deps
 
-abbrev Explanations := Std.HashMap (ModuleIdx × NeedsKind) (Option (Name × Name))
-
 /--
 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 (s : State) (i : ModuleIdx) : Explanations := Id.run do
-  let env := s.env
+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
     -- Added guard for cases like `structure` that are still exported even if private
@@ -366,25 +364,18 @@ def getExplanations (s : State) (i : ModuleIdx) : Explanations := Id.run do
 where
   /-- Accumulate the results from expression `e` into `deps`. -/
   visitExpr (k : NeedsKind) name e deps :=
-    let env := s.env
     Lean.Expr.foldConsts e deps fun c deps => Id.run do
       let mut deps := deps
       if let some c := getDepConstName? env c then
         if let some j := env.getModuleIdxFor? c then
           let k := { k with isMeta := k.isMeta && !isDeclMeta' env c }
-          deps := addExplanation j k name c deps
-        for indMod in (indirectModUseExt.getState env)[c]?.getD #[] do
-          if s.transDeps[i]!.has k indMod then
-            deps := addExplanation indMod k name (`_indirect ++ c) deps
+          if
+            if let some (some (name', _)) := deps[(j, k)]? then
+              decide (name.toString.length < name'.toString.length)
+            else true
+          then
+            deps := deps.insert (j, k) (name, c)
       return deps
-  addExplanation (j : ModuleIdx) (k : NeedsKind) (use def_ : Name) (deps : Explanations) : Explanations :=
-    if
-      if let some (some (name', _)) := deps[(j, k)]? then
-        decide (use.toString.length < name'.toString.length)
-      else true
-    then
-      deps.insert (j, k) (use, def_)
-    else deps
 
 partial def initStateFromEnv (env : Environment) : State := Id.run do
   let mut s := { env }
@@ -551,7 +542,7 @@ def visitModule (pkg : Name) (srcSearchPath : SearchPath)
         let mut imp : Import := { k with module := s.modNames[j]! }
         let mut j := j
         if args.trace then
-          IO.eprintln s!"`{imp}` is needed{if needs.has k j then " (calculated)" else ""}"
+          IO.eprintln s!"`{imp}` is needed"
         if args.addPublic && !k.isExported &&
             -- also add as public if previously `public meta`, which could be from automatic porting
             (s.transDepsOrig[i]!.has { k with isExported := true } j || s.transDepsOrig[i]!.has { k with isExported := true, isMeta := true } j) then
@@ -669,7 +660,7 @@ def visitModule (pkg : Name) (srcSearchPath : SearchPath)
   modify fun s => { s with transDeps := s.transDeps.set! i newTransDepsI }
 
   if args.explain then
-    let explanation := getExplanations s i
+    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!

script/release_repos.yml

@@ -142,15 +142,3 @@ repositories:
     branch: master
     dependencies:
       - verso-web-components
-
-  - name: comparator
-    url: https://github.com/leanprover/comparator
-    toolchain-tag: true
-    stable-branch: false
-    branch: master
-
-  - name: lean4export
-    url: https://github.com/leanprover/lean4export
-    toolchain-tag: true
-    stable-branch: false
-    branch: master

src/CMakeLists.txt

@@ -695,7 +695,7 @@ endif()
 
 set(STDLIBS Init Std Lean Leanc)
 if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
-  list(APPEND STDLIBS Lake LeanChecker)
+  list(APPEND STDLIBS Lake)
 endif()
 
 add_custom_target(make_stdlib ALL
@@ -758,12 +758,6 @@ if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
     DEPENDS lake_shared
     COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make lake
     VERBATIM)
-
-  add_custom_target(leanchecker ALL
-    WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
-    DEPENDS lake_shared
-    COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanchecker
-    VERBATIM)
 endif()
 
 if(PREV_STAGE)

src/Init/Classical.lean

@@ -102,7 +102,7 @@ noncomputable def strongIndefiniteDescription {α : Sort u} (p : α → Prop) (h
       ⟨xp.val, fun _ => xp.property⟩)
     (fun hp => ⟨choice h, fun h => absurd h hp⟩)
 
-/-- The Hilbert epsilon function. -/
+/-- the Hilbert epsilon Function -/
 noncomputable def epsilon {α : Sort u} [h : Nonempty α] (p : α → Prop) : α :=
   (strongIndefiniteDescription p h).val
 

src/Init/Control/Basic.lean

@@ -144,7 +144,7 @@ instance : ToBool Bool where
 Converts the result of the monadic action `x` to a `Bool`. If it is `true`, returns it and ignores
 `y`; otherwise, runs `y` and returns its result.
 
-This is a monadic counterpart to the short-circuiting `||` operator, usually accessed via the `<||>`
+This a monadic counterpart to the short-circuiting `||` operator, usually accessed via the `<||>`
 operator.
 -/
 @[macro_inline] def orM {m : Type u → Type v} {β : Type u} [Monad m] [ToBool β] (x y : m β) : m β := do
@@ -161,7 +161,7 @@ recommended_spelling "orM" for "<||>" in [orM, «term_<||>_»]
 Converts the result of the monadic action `x` to a `Bool`. If it is `true`, returns `y`; otherwise,
 returns the original result of `x`.
 
-This is a monadic counterpart to the short-circuiting `&&` operator, usually accessed via the `<&&>`
+This a monadic counterpart to the short-circuiting `&&` operator, usually accessed via the `<&&>`
 operator.
 -/
 @[macro_inline] def andM {m : Type u → Type v} {β : Type u} [Monad m] [ToBool β] (x y : m β) : m β := do

src/Init/Core.lean

@@ -337,7 +337,7 @@ inductive Exists {α : Sort u} (p : α → Prop) : Prop where
 An indication of whether a loop's body terminated early that's used to compile the `for x in xs`
 notation.
 
-A collection's `ForIn` or `ForIn'` instance describes how to iterate over its elements. The monadic
+A collection's `ForIn` or `ForIn'` instance describe's how to iterate over its elements. The monadic
 action that represents the body of the loop returns a `ForInStep α`, where `α` is the local state
 used to implement features such as `let mut`.
 -/
@@ -510,12 +510,12 @@ abbrev SSuperset [HasSSubset α] (a b : α) := SSubset b a
 
 /-- Notation type class for the union operation `∪`. -/
 class Union (α : Type u) where
-  /-- `a ∪ b` is the union of `a` and `b`. -/
+  /-- `a ∪ b` is the union of`a` and `b`. -/
   union : α → α → α
 
 /-- Notation type class for the intersection operation `∩`. -/
 class Inter (α : Type u) where
-  /-- `a ∩ b` is the intersection of `a` and `b`. -/
+  /-- `a ∩ b` is the intersection of`a` and `b`. -/
   inter : α → α → α
 
 /-- Notation type class for the set difference `\`. -/
@@ -538,10 +538,10 @@ infix:50 " ⊇ " => Superset
 /-- Strict superset relation: `a ⊃ b`  -/
 infix:50 " ⊃ " => SSuperset
 
-/-- `a ∪ b` is the union of `a` and `b`. -/
+/-- `a ∪ b` is the union of`a` and `b`. -/
 infixl:65 " ∪ " => Union.union
 
-/-- `a ∩ b` is the intersection of `a` and `b`. -/
+/-- `a ∩ b` is the intersection of`a` and `b`. -/
 infixl:70 " ∩ " => Inter.inter
 
 /--

src/Init/Data/Array/Basic.lean

@@ -589,8 +589,6 @@ unsafe def foldlMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Mon
   if start < stop then
     if stop ≤ as.size then
       fold (USize.ofNat start) (USize.ofNat stop) init
-    else if start < as.size then
-      fold (USize.ofNat start) (USize.ofNat as.size) init
     else
       pure init
   else

src/Init/Data/Array/DecidableEq.lean

@@ -125,22 +125,6 @@ instance instDecidableEmpEq (ys : Array α) : Decidable (#[] = ys) :=
   | ⟨[]⟩ => isTrue rfl
   | ⟨_ :: _⟩ => isFalse (fun h => Array.noConfusion rfl (heq_of_eq h) (fun h => List.noConfusion rfl h))
 
-@[inline]
-def instDecidableEqEmpImpl (xs : Array α) : Decidable (xs = #[]) :=
-  decidable_of_iff xs.isEmpty <| by rcases xs with ⟨⟨⟩⟩ <;> simp [Array.isEmpty]
-
-@[inline]
-def instDecidableEmpEqImpl (xs : Array α) : Decidable (#[] = xs) :=
-  decidable_of_iff xs.isEmpty <| by rcases xs with ⟨⟨⟩⟩ <;> simp [Array.isEmpty]
-
-@[csimp]
-theorem instDecidableEqEmp_csimp : @instDecidableEqEmp = @instDecidableEqEmpImpl :=
-  Subsingleton.allEq _ _
-
-@[csimp]
-theorem instDecidableEmpEq_csimp : @instDecidableEmpEq = @instDecidableEmpEqImpl :=
-  Subsingleton.allEq _ _
-
 theorem beq_eq_decide [BEq α] (xs ys : Array α) :
     (xs == ys) = if h : xs.size = ys.size then
       decide (∀ (i : Nat) (h' : i < xs.size), xs[i] == ys[i]'(h ▸ h')) else false := by

src/Init/Data/Array/Lemmas.lean

@@ -62,9 +62,6 @@ theorem eq_empty_of_size_eq_zero (h : xs.size = 0) : xs = #[] := by
   cases xs
   simp_all
 
-grind_pattern eq_empty_of_size_eq_zero => xs.size where
-  guard xs.size = 0
-
 theorem ne_empty_of_size_eq_add_one (h : xs.size = n + 1) : xs ≠ #[] := by
   cases xs
   simpa using List.ne_nil_of_length_eq_add_one h
@@ -115,8 +112,7 @@ theorem none_eq_getElem?_iff {xs : Array α} {i : Nat} : none = xs[i]? ↔ xs.si
 theorem getElem?_eq_none {xs : Array α} (h : xs.size ≤ i) : xs[i]? = none := by
   simp [h]
 
-grind_pattern Array.getElem?_eq_none => xs.size, xs[i]? where
-  guard xs.size ≤ i
+grind_pattern Array.getElem?_eq_none => xs.size, xs[i]?
 
 @[simp] theorem getElem?_eq_getElem {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i]? = some xs[i] :=
   getElem?_pos ..

src/Init/Data/BitVec/Lemmas.lean

@@ -67,9 +67,6 @@ theorem none_eq_getElem?_iff {l : BitVec w} : none = l[n]? ↔ w ≤ n := by
 @[simp]
 theorem getElem?_eq_none {l : BitVec w} (h : w ≤ n) : l[n]? = none := getElem?_eq_none_iff.mpr h
 
-grind_pattern BitVec.getElem?_eq_none => l[n]? where
-  guard w ≤ n
-
 theorem getElem?_eq (l : BitVec w) (i : Nat) :
     l[i]? = if h : i < w then some l[i] else none := by
   split <;> simp_all

src/Init/Data/ByteArray/Basic.lean

@@ -269,8 +269,6 @@ unsafe def foldlMUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (f : β
   if start < stop then
     if stop ≤ as.size then
       fold (USize.ofNat start) (USize.ofNat stop) init
-    else if start < as.size then
-      fold (USize.ofNat start) (USize.ofNat as.size) init
     else
       pure init
   else

src/Init/Data/FloatArray/Basic.lean

@@ -144,8 +144,6 @@ unsafe def foldlMUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (f : β
   if start < stop then
     if stop ≤ as.size then
       fold (USize.ofNat start) (USize.ofNat stop) init
-    else if start < as.size then
-      fold (USize.ofNat start) (USize.ofNat as.size) init
     else
       pure init
   else

src/Init/Data/Int/Gcd.lean

@@ -113,8 +113,6 @@ theorem gcd_eq_right_iff_dvd (hb : 0 ≤ b) : gcd a b = b ↔ b ∣ a := by
 
 theorem gcd_assoc (a b c : Int) : gcd (gcd a b) c = gcd a (gcd b c) := Nat.gcd_assoc ..
 
-theorem gcd_left_comm (a b c : Int) : gcd a (gcd b c) = gcd b (gcd a c) := Nat.gcd_left_comm ..
-
 theorem gcd_mul_left (m n k : Int) : gcd (m * n) (m * k) = m.natAbs * gcd n k := by
   simp [gcd_eq_natAbs_gcd_natAbs, Nat.gcd_mul_left, natAbs_mul]
 

src/Init/Data/Iterators/Basic.lean

@@ -10,7 +10,6 @@ public import Init.Classical
 public import Init.Ext
 
 set_option doc.verso true
-set_option linter.missingDocs true
 
 public section
 
@@ -350,24 +349,14 @@ abbrev PlausibleIterStep.casesOn {IsPlausibleStep : IterStep α β → Prop}
 end IterStep
 
 /--
-The step function of an iterator in `Iter (α := α) β` or `IterM (α := α) m β`.
+The typeclass providing the step function of an iterator in `Iter (α := α) β` or
+`IterM (α := α) m β`.
 
 In order to allow intrinsic termination proofs when iterating with the `step` function, the
 step object is bundled with a proof that it is a "plausible" step for the given current iterator.
 -/
 class Iterator (α : Type w) (m : Type w → Type w') (β : outParam (Type w)) where
-  /--
-  A relation that governs the allowed steps from a given iterator.
-
-  The "plausible" steps are those which make sense for a given state; plausibility can ensure
-  properties such as the successor iterator being drawn from the same collection, that an iterator
-  resulting from a skip will return the same next value, or that the next item yielded is next one
-  in the original collection.
-  -/
   IsPlausibleStep : IterM (α := α) m β → IterStep (IterM (α := α) m β) β → Prop
-  /--
-  Carries out a step of iteration.
-  -/
   step : (it : IterM (α := α) m β) → m (Shrink <| PlausibleIterStep <| IsPlausibleStep it)
 
 section Monadic
@@ -380,7 +369,7 @@ def IterM.mk {α : Type w} (it : α) (m : Type w → Type w') (β : Type w) :
     IterM (α := α) m β :=
   ⟨it⟩
 
-@[deprecated IterM.mk (since := "2025-12-01"), inline, expose, inherit_doc IterM.mk]
+@[deprecated IterM.mk (since := "2025-12-01"), inline, expose]
 def Iterators.toIterM := @IterM.mk
 
 @[simp]
@@ -388,7 +377,6 @@ theorem IterM.mk_internalState {α m β} (it : IterM (α := α) m β) :
     .mk it.internalState m β = it :=
   rfl
 
-set_option linter.missingDocs false in
 @[deprecated IterM.mk_internalState (since := "2025-12-01")]
 def Iterators.toIterM_internalState := @IterM.mk_internalState
 
@@ -471,10 +459,8 @@ number of steps.
 -/
 inductive IterM.IsPlausibleIndirectOutput {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
     : IterM (α := α) m β → β → Prop where
-  /-- The output value could plausibly be emitted in the next step. -/
   | direct {it : IterM (α := α) m β} {out : β} : it.IsPlausibleOutput out →
       it.IsPlausibleIndirectOutput out
-  /-- The output value could plausibly be emitted in a step after the next step. -/
   | indirect {it it' : IterM (α := α) m β} {out : β} : it'.IsPlausibleSuccessorOf it →
       it'.IsPlausibleIndirectOutput out → it.IsPlausibleIndirectOutput out
 
@@ -484,9 +470,7 @@ finitely many steps. This relation is reflexive.
 -/
 inductive IterM.IsPlausibleIndirectSuccessorOf {α β : Type w} {m : Type w → Type w'}
     [Iterator α m β] : IterM (α := α) m β → IterM (α := α) m β → Prop where
-  /-- Every iterator is a plausible indirect successor of itself. -/
   | refl (it : IterM (α := α) m β) : it.IsPlausibleIndirectSuccessorOf it
-  /-- The iterator is a plausible successor of one of the current iterator's successors. -/
   | cons_right {it'' it' it : IterM (α := α) m β} (h' : it''.IsPlausibleIndirectSuccessorOf it')
       (h : it'.IsPlausibleSuccessorOf it) : it''.IsPlausibleIndirectSuccessorOf it
 
@@ -611,10 +595,8 @@ number of steps.
 -/
 inductive Iter.IsPlausibleIndirectOutput {α β : Type w} [Iterator α Id β] :
     Iter (α := α) β → β → Prop where
-  /-- The output value could plausibly be emitted in the next step. -/
   | direct {it : Iter (α := α) β} {out : β} : it.IsPlausibleOutput out →
       it.IsPlausibleIndirectOutput out
-  /-- The output value could plausibly be emitted in a step after the next step. -/
   | indirect {it it' : Iter (α := α) β} {out : β} : it'.IsPlausibleSuccessorOf it →
       it'.IsPlausibleIndirectOutput out → it.IsPlausibleIndirectOutput out
 
@@ -645,9 +627,7 @@ finitely many steps. This relation is reflexive.
 -/
 inductive Iter.IsPlausibleIndirectSuccessorOf {α : Type w} {β : Type w} [Iterator α Id β] :
     Iter (α := α) β → Iter (α := α) β → Prop where
-  /-- Every iterator is a plausible indirect successor of itself. -/
   | refl (it : Iter (α := α) β) : IsPlausibleIndirectSuccessorOf it it
-  /-- The iterator is a plausible indirect successor of one of the current iterator's successors. -/
   | cons_right {it'' it' it : Iter (α := α) β} (h' : it''.IsPlausibleIndirectSuccessorOf it')
       (h : it'.IsPlausibleSuccessorOf it) : it''.IsPlausibleIndirectSuccessorOf it
 
@@ -721,11 +701,6 @@ recursion over finite iterators. See also `IterM.finitelyManySteps` and `Iter.fi
 -/
 structure IterM.TerminationMeasures.Finite
     (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where
-  /--
-  The wrapped iterator.
-
-  In the wrapper, its finiteness is used as a termination measure.
-  -/
   it : IterM (α := α) m β
 
 /--
@@ -852,11 +827,6 @@ recursion over productive iterators. See also `IterM.finitelyManySkips` and `Ite
 -/
 structure IterM.TerminationMeasures.Productive
     (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where
-  /--
-  The wrapped iterator.
-
-  In the wrapper, its productivity is used as a termination measure.
-  -/
   it : IterM (α := α) m β
 
 /--
@@ -960,63 +930,6 @@ library.
 -/
 class LawfulDeterministicIterator (α : Type w) (m : Type w → Type w') [Iterator α m β]
     where
-  /--
-  Every iterator with state `α` in monad `m` has exactly one plausible step.
-  -/
   isPlausibleStep_eq_eq : ∀ it : IterM (α := α) m β, ∃ step, it.IsPlausibleStep = (· = step)
 
-namespace Iterators
-
-/--
-This structure provides a more convenient way to define `Finite α m` instances using
-`Finite.of_finitenessRelation : FinitenessRelation α m → Finite α m`.
--/
-structure FinitenessRelation (α : Type w) (m : Type w → Type w') {β : Type w}
-    [Iterator α m β] where
-  /--
-  A well-founded relation such that if `it'` is a successor iterator of `it`, then `Rel it' it`.
-  -/
-  Rel (it' it : IterM (α := α) m β) : Prop
-  /-- `Rel` is well-founded. -/
-  wf : WellFounded Rel
-  /-- If `it'` is a successor iterator of `it`, then `Rel it' it`. -/
-  subrelation : ∀ {it it'}, it'.IsPlausibleSuccessorOf it → Rel it' it
-
-theorem Finite.of_finitenessRelation
-    {α : Type w} {m : Type w → Type w'} {β : Type w}
-    [Iterator α m β] (r : FinitenessRelation α m) : Finite α m where
-  wf := by
-    refine Subrelation.wf (r := r.Rel) ?_ ?_
-    · intro x y h
-      apply FinitenessRelation.subrelation
-      exact h
-    · apply InvImage.wf
-      exact r.wf
-
-/--
-This structure provides a more convenient way to define `Productive α m` instances using
-`Productive.of_productivenessRelation : ProductivenessRelation α m → Productive α m`.
--/
-structure ProductivenessRelation (α : Type w) (m : Type w → Type w') {β : Type w}
-    [Iterator α m β] where
-  /--
-  A well-founded relation such that if `it'` is obtained from `it` by skipping, then `Rel it' it`.
-  -/
-  Rel : (IterM (α := α) m β) → (IterM (α := α) m β) → Prop
-  /-- `Rel` is well-founded. -/
-  wf : WellFounded Rel
-  /-- If `it'` is obtained from `it` by skipping, then `Rel it' it`. -/
-  subrelation : ∀ {it it'}, it'.IsPlausibleSkipSuccessorOf it → Rel it' it
-
-theorem Productive.of_productivenessRelation
-    {α : Type w} {m : Type w → Type w'} {β : Type w}
-    [Iterator α m β] (r : ProductivenessRelation α m) : Productive α m where
-  wf := by
-    refine Subrelation.wf (r := r.Rel) ?_ ?_
-    · intro x y h
-      apply ProductivenessRelation.subrelation
-      exact h
-    · apply InvImage.wf
-      exact r.wf
-
-end Std.Iterators
+end Std

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

@@ -6,6 +6,7 @@ Authors: Paul Reichert
 module
 
 prelude
+public import Init.Data.Iterators.Internal.Termination
 public import Init.Data.Iterators.Consumers.Loop
 
 public section
@@ -46,7 +47,7 @@ instance Attach.instIterator {α β : Type w} {m : Type w → Type w'} [Monad m]
 def Attach.instFinitenessRelation {α β : Type w} {m : Type w → Type w'} [Monad m]
     [Iterator α m β] [Finite α m] {P : β → Prop} :
     FinitenessRelation (Attach α m P) m where
-  Rel := InvImage WellFoundedRelation.rel fun it => it.internalState.inner.finitelyManySteps
+  rel := InvImage WellFoundedRelation.rel fun it => it.internalState.inner.finitelyManySteps
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by
     apply Relation.TransGen.single
@@ -67,7 +68,7 @@ instance Attach.instFinite {α β : Type w} {m : Type w → Type w'} [Monad m]
 def Attach.instProductivenessRelation {α β : Type w} {m : Type w → Type w'} [Monad m]
     [Iterator α m β] [Productive α m] {P : β → Prop} :
     ProductivenessRelation (Attach α m P) m where
-  Rel := InvImage WellFoundedRelation.rel fun it => it.internalState.inner.finitelyManySkips
+  rel := InvImage WellFoundedRelation.rel fun it => it.internalState.inner.finitelyManySkips
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by
     apply Relation.TransGen.single

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

@@ -8,6 +8,7 @@ module
 prelude
 public import Init.Data.Iterators.Consumers.Loop
 public import Init.Data.Iterators.PostconditionMonad
+public import Init.Data.Iterators.Internal.Termination
 
 public section
 
@@ -171,7 +172,7 @@ private def FilterMap.instFinitenessRelation {α β γ : Type w} {m : Type w →
     {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α}
     {f : β → PostconditionT n (Option γ)} [Finite α m] :
     FinitenessRelation (FilterMap α m n lift f) n where
-  Rel := InvImage IterM.IsPlausibleSuccessorOf (FilterMap.inner ∘ IterM.internalState)
+  rel := InvImage IterM.IsPlausibleSuccessorOf (FilterMap.inner ∘ IterM.internalState)
   wf := InvImage.wf _ Finite.wf
   subrelation {it it'} h := by
     obtain ⟨step, h, h'⟩ := h
@@ -204,7 +205,7 @@ private def Map.instProductivenessRelation {α β γ : Type w} {m : Type w → T
     {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α}
     {f : β → PostconditionT n γ} [Productive α m] :
     ProductivenessRelation (Map α m n lift f) n where
-  Rel := InvImage IterM.IsPlausibleSkipSuccessorOf (FilterMap.inner ∘ IterM.internalState)
+  rel := InvImage IterM.IsPlausibleSkipSuccessorOf (FilterMap.inner ∘ IterM.internalState)
   wf := InvImage.wf _ Productive.wf
   subrelation {it it'} h := by
     cases h

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

@@ -277,7 +277,7 @@ theorem Flatten.rel_of_right₂ [Monad m] [Iterator α m (IterM (α := α₂) m
 def Flatten.instFinitenessRelation [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
     [Finite α m] [Finite α₂ m] :
     FinitenessRelation (Flatten α α₂ β m) m where
-  Rel := Rel α β m
+  rel := Rel α β m
   wf := by
     apply InvImage.wf
     refine ⟨fun (a, b) => Prod.lexAccessible (WellFounded.apply ?_ a) (WellFounded.apply ?_) b⟩
@@ -342,7 +342,7 @@ theorem Flatten.productiveRel_of_right₂ [Monad m] [Iterator α m (IterM (α :=
 def Flatten.instProductivenessRelation [Monad m] [Iterator α m (IterM (α := α₂) m β)]
     [Iterator α₂ m β] [Finite α m] [Productive α₂ m] :
     ProductivenessRelation (Flatten α α₂ β m) m where
-  Rel := ProductiveRel α β m
+  rel := ProductiveRel α β m
   wf := by
     apply InvImage.wf
     refine ⟨fun (a, b) => Prod.lexAccessible (WellFounded.apply ?_ a) (WellFounded.apply ?_) b⟩

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

@@ -9,6 +9,7 @@ prelude
 public import Init.Data.Nat.Lemmas
 public import Init.Data.Iterators.Consumers.Monadic.Collect
 public import Init.Data.Iterators.Consumers.Monadic.Loop
+public import Init.Data.Iterators.Internal.Termination
 
 @[expose] public section
 
@@ -164,7 +165,7 @@ theorem Take.rel_of_zero_of_inner [Monad m] [Iterator α m β]
 private def Take.instFinitenessRelation [Monad m] [Iterator α m β]
     [Productive α m] :
     FinitenessRelation (Take α m) m where
-  Rel := Take.Rel m
+  rel := Take.Rel m
   wf := by
     rw [Rel]
     split

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

@@ -6,6 +6,7 @@ Authors: Paul Reichert
 module
 
 prelude
+public import Init.Data.Iterators.Internal.Termination
 public import Init.Data.Iterators.Consumers.Monadic
 
 public section
@@ -98,7 +99,7 @@ instance ULiftIterator.instIterator [Iterator α m β] [Monad n] :
 
 private def ULiftIterator.instFinitenessRelation [Iterator α m β] [Finite α m] [Monad n] :
     FinitenessRelation (ULiftIterator α m n β lift) n where
-  Rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.inner.finitelyManySteps)
+  rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.inner.finitelyManySteps)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation h := by
     rcases h with ⟨_, hs, step, hp, rfl⟩
@@ -114,7 +115,7 @@ instance ULiftIterator.instFinite [Iterator α m β] [Finite α m] [Monad n] :
 
 private def ULiftIterator.instProductivenessRelation [Iterator α m β] [Productive α m] [Monad n] :
     ProductivenessRelation (ULiftIterator α m n β lift) n where
-  Rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.inner.finitelyManySkips)
+  rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.inner.finitelyManySkips)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation h := by
     rcases h with ⟨step, hp, hs⟩

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

@@ -9,8 +9,6 @@ prelude
 public import Init.Data.Iterators.Consumers.Loop
 public import Init.Data.Iterators.Consumers.Monadic.Access
 
-set_option linter.missingDocs true
-
 @[expose] public section
 
 namespace Std

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

@@ -8,8 +8,6 @@ module
 prelude
 public import Init.Data.Iterators.Basic
 
-set_option linter.missingDocs true
-
 public section
 
 namespace Std
@@ -59,8 +57,8 @@ theorem IterM.not_isPlausibleNthOutputStep_yield {α β : Type w} {m : Type w
 
 /--
 `IteratorAccess α m` provides efficient implementations for random access or iterators that support
-it. `it.nextAtIdx? n` either returns the step in which the `n`th value of `it` is emitted
-(necessarily of the form `.yield _ _`) or `.done` if `it` terminates before emitting the `n`th
+it. `it.nextAtIdx? n` either returns the step in which the `n`-th value of `it` is emitted
+(necessarily of the form `.yield _ _`) or `.done` if `it` terminates before emitting the `n`-th
 value.
 
 For monadic iterators, the monadic effects of this operation may differ from manually iterating
@@ -70,11 +68,6 @@ is guaranteed to plausible in the sense of `IterM.IsPlausibleNthOutputStep`.
 This class is experimental and users of the iterator API should not explicitly depend on it.
 -/
 class IteratorAccess (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where
-  /--
-  `nextAtIdx? it n` either returns the step in which the `n`th value of `it` is emitted
-  (necessarily of the form `.yield _ _`) or `.done` if `it` terminates before emitting the `n`th
-  value.
-  -/
   nextAtIdx? (it : IterM (α := α) m β) (n : Nat) :
     m (PlausibleIterStep (it.IsPlausibleNthOutputStep n))
 

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

@@ -11,8 +11,6 @@ public import Init.Data.Iterators.Consumers.Monadic.Total
 public import Init.Data.Iterators.Internal.LawfulMonadLiftFunction
 public import Init.WFExtrinsicFix
 
-set_option linter.missingDocs true
-
 @[expose] public section
 
 /-!

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

@@ -11,8 +11,6 @@ public import Init.Data.Iterators.Internal.LawfulMonadLiftFunction
 public import Init.WFExtrinsicFix
 public import Init.Data.Iterators.Consumers.Monadic.Total
 
-set_option linter.missingDocs true
-
 public section
 
 /-!
@@ -72,9 +70,6 @@ provided by the standard library.
 @[ext]
 class IteratorLoop (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β]
     (n : Type x → Type x') where
-  /--
-  Iteration over the iterator `it` in the manner expected by `for` loops.
-  -/
   forIn : ∀ (_liftBind : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) (γ : Type x),
       (plausible_forInStep : β → γ → ForInStep γ → Prop) →
       (it : IterM (α := α) m β) → γ →
@@ -87,9 +82,7 @@ end Typeclasses
 structure IteratorLoop.WithWF (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β]
     {γ : Type x} (PlausibleForInStep : β → γ → ForInStep γ → Prop)
     (hwf : IteratorLoop.WellFounded α m PlausibleForInStep) where
-  /-- Internal implementation detail of the iterator library. -/
   it : IterM (α := α) m β
-  /-- Internal implementation detail of the iterator library. -/
   acc : γ
 
 instance IteratorLoop.WithWF.instWellFoundedRelation
@@ -170,7 +163,6 @@ Asserts that a given `IteratorLoop` instance is equal to `IteratorLoop.defaultIm
 -/
 class LawfulIteratorLoop (α : Type w) (m : Type w → Type w') (n : Type x → Type x')
     [Monad m] [Monad n] [Iterator α m β] [i : IteratorLoop α m n] where
-  /-- The implementation of `IteratorLoop.forIn` in `i` is equal to the default implementation. -/
   lawful lift [LawfulMonadLiftBindFunction lift] γ it init
       (Pl : β → γ → ForInStep γ → Prop) (wf : IteratorLoop.WellFounded α m Pl)
       (f : (b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c))) :
@@ -227,7 +219,6 @@ instance IterM.instForInOfIteratorLoop {m : Type w → Type w'} {n : Type w →
   haveI : ForIn' n (IterM (α := α) m β) β _ := IterM.instForIn'
   instForInOfForIn'
 
-/-- Internal implementation detail of the iterator library. -/
 @[always_inline, inline]
 def IterM.Partial.instForIn' {m : Type w → Type w'} {n : Type w → Type w''}
     {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] [Monad n] :
@@ -235,7 +226,6 @@ def IterM.Partial.instForIn' {m : Type w → Type w'} {n : Type w → Type w''}
   forIn' it init f :=
     haveI := @IterM.instForIn'; forIn' it.it init f
 
-/-- Internal implementation detail of the iterator library. -/
 @[always_inline, inline]
 def IterM.Total.instForIn' {m : Type w → Type w'} {n : Type w → Type w''}
     {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] [Monad n]

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

@@ -8,8 +8,6 @@ module
 prelude
 public import Init.Data.Iterators.Basic
 
-set_option linter.missingDocs true
-
 public section
 
 namespace Std
@@ -18,9 +16,6 @@ namespace Std
 A wrapper around an iterator that provides partial consumers. See `IterM.allowNontermination`.
 -/
 structure IterM.Partial {α : Type w} (m : Type w → Type w') (β : Type w) where
-  /--
-  The wrapped iterator, which was wrapped by `IterM.allowNontermination`.
-  -/
   it : IterM (α := α) m β
 
 /--

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

@@ -9,19 +9,12 @@ prelude
 public import Init.Data.Iterators.Basic
 
 set_option doc.verso true
-set_option linter.missingDocs true
 
 public section
 
 namespace Std
 
-/--
-A wrapper around an iterator that provides total consumers. See `IterM.ensureTermination`.
--/
 structure IterM.Total {α : Type w} (m : Type w → Type w') (β : Type w) where
-  /--
-  The wrapped iterator, which was wrapped by `IterM.ensureTermination`.
-  -/
   it : IterM (α := α) m β
 
 /--

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

@@ -8,8 +8,6 @@ module
 prelude
 public import Init.Data.Iterators.Basic
 
-set_option linter.missingDocs true
-
 public section
 
 namespace Std
@@ -18,9 +16,6 @@ namespace Std
 A wrapper around an iterator that provides partial consumers. See `Iter.allowNontermination`.
 -/
 structure Iter.Partial {α : Type w} (β : Type w) where
-  /--
-  The wrapped iterator, which was wrapped by `Iter.allowNontermination`.
-  -/
   it : Iter (α := α) β
 
 /--

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

@@ -9,8 +9,6 @@ prelude
 public import Init.Data.Stream
 public import Init.Data.Iterators.Consumers.Access
 
-set_option linter.missingDocs true
-
 public section
 
 namespace Std

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

@@ -9,19 +9,12 @@ prelude
 public import Init.Data.Iterators.Basic
 
 set_option doc.verso true
-set_option linter.missingDocs true
 
 public section
 
 namespace Std
 
-/--
-A wrapper around an iterator that provides total consumers. See `Iter.ensureTermination`.
--/
 structure Iter.Total {α : Type w} (β : Type w) where
-  /--
-  The wrapped iterator, which was wrapped by `Iter.ensureTermination`.
-  -/
   it : Iter (α := α) β
 
 /--

src/Init/Data/Iterators/Internal.lean

@@ -7,3 +7,4 @@ module
 
 prelude
 public import Init.Data.Iterators.Internal.LawfulMonadLiftFunction
+public import Init.Data.Iterators.Internal.Termination

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

@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Init.Data.Iterators.Basic
+
+public section
+
+/-!
+This is an internal module used by iterator implementations.
+-/
+
+namespace Std.Iterators
+
+/--
+Internal implementation detail of the iterator library.
+The purpose of this class is that it implies a `Finite` instance but
+it is more convenient to implement.
+-/
+structure FinitenessRelation (α : Type w) (m : Type w → Type w') {β : Type w}
+    [Iterator α m β] where
+  rel : (IterM (α := α) m β) → (IterM (α := α) m β) → Prop
+  wf : WellFounded rel
+  subrelation : ∀ {it it'}, it'.IsPlausibleSuccessorOf it → rel it' it
+
+theorem Finite.of_finitenessRelation
+    {α : Type w} {m : Type w → Type w'} {β : Type w}
+    [Iterator α m β] (r : FinitenessRelation α m) : Finite α m where
+  wf := by
+    refine Subrelation.wf (r := r.rel) ?_ ?_
+    · intro x y h
+      apply FinitenessRelation.subrelation
+      exact h
+    · apply InvImage.wf
+      exact r.wf
+
+/--
+Internal implementation detail of the iterator library.
+The purpose of this class is that it implies a `Productive` instance but
+it is more convenient to implement.
+-/
+structure ProductivenessRelation (α : Type w) (m : Type w → Type w') {β : Type w}
+    [Iterator α m β] where
+  rel : (IterM (α := α) m β) → (IterM (α := α) m β) → Prop
+  wf : WellFounded rel
+  subrelation : ∀ {it it'}, it'.IsPlausibleSkipSuccessorOf it → rel it' it
+
+theorem Productive.of_productivenessRelation
+    {α : Type w} {m : Type w → Type w'} {β : Type w}
+    [Iterator α m β] (r : ProductivenessRelation α m) : Productive α m where
+  wf := by
+    refine Subrelation.wf (r := r.rel) ?_ ?_
+    · intro x y h
+      apply ProductivenessRelation.subrelation
+      exact h
+    · apply InvImage.wf
+      exact r.wf
+
+end Std.Iterators

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

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

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

@@ -1,26 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Paul Reichert
--/
-module
-
-prelude
-public import Init.Data.Iterators.Consumers.Access
-
-namespace Std.Iter
-open Std.Iterators
-
-public theorem atIdxSlow?_eq_match [Iterator α Id β] [Productive α Id]
-    {n : Nat} {it : Iter (α := α) β} :
-    it.atIdxSlow? n =
-      (match it.step.val with
-      | .yield it' out =>
-        match n with
-        | 0 => some out
-        | n + 1 => it'.atIdxSlow? n
-      | .skip it' => it'.atIdxSlow? n
-      | .done => none) := by
-  fun_induction it.atIdxSlow? n <;> simp_all
-
-end Std.Iter

src/Init/Data/Iterators/PostconditionMonad.lean

@@ -72,7 +72,7 @@ def PostconditionT.liftWithProperty {α : Type w} {m : Type w → Type w'} {P :
   ⟨P, x⟩
 
 /--
-Given a function `f : α → β`, returns a function `PostconditionT m α → PostconditionT m β`,
+Given a function `f : α → β`, returns a a function `PostconditionT m α → PostconditionT m β`,
 turning `PostconditionT m` into a functor.
 
 The postcondition of the `x.map f` states that the return value is the image under `f` of some
@@ -85,7 +85,7 @@ protected def PostconditionT.map {m : Type w → Type w'} [Functor m] {α : Type
     (fun a => ⟨f a.val, _, rfl⟩) <$> x.operation⟩
 
 /--
-Given a function `α → PostconditionT m β`, returns a function
+Given a function `α → PostconditionT m β`, returns a a function
 `PostconditionT m α → PostconditionT m β`, turning `PostconditionT m` into a monad.
 -/
 @[always_inline, inline, expose]
@@ -287,12 +287,6 @@ theorem PostconditionT.run_attachLift {m : Type w → Type w'} [Monad m] [MonadA
     {x : m α} : (attachLift x).run = x := by
   simp [attachLift, run_eq_map, WeaklyLawfulMonadAttach.map_attach]
 
-@[simp]
-theorem PostconditionT.operation_attachLift {m : Type w → Type w'} [Monad m] [MonadAttach m]
-    {α : Type w} {x : m α} : (attachLift x : PostconditionT m α).operation =
-      MonadAttach.attach x := by
-  rfl
-
 instance {m : Type w → Type w'} {n : Type w → Type w''} [MonadLift m n] :
     MonadLift (PostconditionT m) (PostconditionT n) where
   monadLift x := ⟨_, monadLift x.operation⟩

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

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.Iterators.Consumers
+public import Init.Data.Iterators.Internal.Termination
 
 @[expose] public section
 
@@ -64,7 +65,7 @@ instance ListIterator.instIterator {α : Type w} [Pure m] : Iterator (ListIterat
 
 private def ListIterator.instFinitenessRelation [Pure m] :
     FinitenessRelation (ListIterator α) m where
-  Rel := InvImage WellFoundedRelation.rel (ListIterator.list ∘ IterM.internalState)
+  rel := InvImage WellFoundedRelation.rel (ListIterator.list ∘ IterM.internalState)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by
     simp_wf

src/Init/Data/LawfulHashable.lean

@@ -11,7 +11,7 @@ public import Init.Core
 public section
 
 /--
-The `BEq α` and `Hashable α` instances on `α` are compatible. This means that `a == b` implies
+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.

src/Init/Data/List/Basic.lean

@@ -169,10 +169,10 @@ Examples:
   | a::as, b::bs, eqv => eqv a b && isEqv as bs eqv
   | _,     _,     _   => false
 
-@[simp, grind =] theorem isEqv_nil_nil : isEqv ([] : List α) [] eqv = true := rfl
-@[simp, grind =] theorem isEqv_nil_cons : isEqv ([] : List α) (a::as) eqv = false := rfl
-@[simp, grind =] theorem isEqv_cons_nil : isEqv (a::as : List α) [] eqv = false := rfl
-@[grind =] theorem isEqv_cons₂ : isEqv (a::as) (b::bs) eqv = (eqv a b && isEqv as bs eqv) := rfl
+@[simp] theorem isEqv_nil_nil : isEqv ([] : List α) [] eqv = true := rfl
+@[simp] theorem isEqv_nil_cons : isEqv ([] : List α) (a::as) eqv = false := rfl
+@[simp] theorem isEqv_cons_nil : isEqv (a::as : List α) [] eqv = false := rfl
+theorem isEqv_cons₂ : isEqv (a::as) (b::bs) eqv = (eqv a b && isEqv as bs eqv) := rfl
 
 
 /-! ## Lexicographic ordering -/
@@ -717,7 +717,6 @@ Examples:
  * `["red", "green", "blue"].leftpad 3 "blank" = ["red", "green", "blue"]`
  * `["red", "green", "blue"].leftpad 1 "blank" = ["red", "green", "blue"]`
 -/
-@[simp, grind =]
 def leftpad (n : Nat) (a : α) (l : List α) : List α := replicate (n - length l) a ++ l
 
 
@@ -731,7 +730,6 @@ Examples:
  * `["red", "green", "blue"].rightpad 3 "blank" = ["red", "green", "blue"]`
  * `["red", "green", "blue"].rightpad 1 "blank" = ["red", "green", "blue"]`
 -/
-@[simp, grind =]
 def rightpad (n : Nat) (a : α) (l : List α) : List α := l ++ replicate (n - length l) a
 
 /-! ### reduceOption -/

src/Init/Data/List/Control.lean

@@ -50,7 +50,7 @@ Users that want to use `mapM` with `Applicative` should use `mapA` instead.
 Applies the monadic action `f` to every element in the list, left-to-right, and returns the list of
 results.
 
-This implementation is tail recursive. `List.mapM'` is a non-tail-recursive variant that may be
+This implementation is tail recursive. `List.mapM'` is a a non-tail-recursive variant that may be
 more convenient to reason about. `List.forM` is the variant that discards the results and
 `List.mapA` is the variant that works with `Applicative`.
 -/
@@ -107,7 +107,7 @@ Applies the monadic action `f` to the corresponding elements of two lists, left-
 at the end of the shorter list. `zipWithM f as bs` is equivalent to `mapM id (zipWith f as bs)`
 for lawful `Monad` instances.
 
-This implementation is tail recursive. `List.zipWithM'` is a non-tail-recursive variant that may
+This implementation is tail recursive. `List.zipWithM'` is a a non-tail-recursive variant that may
 be more convenient to reason about.
 -/
 @[inline, expose]

src/Init/Data/List/Lemmas.lean

@@ -97,11 +97,10 @@ open Nat
 
 /-! ### length -/
 
+-- Note: this is not a good `grind` candidate,
+-- as in some circumstances it results in many case splits.
 theorem eq_nil_of_length_eq_zero (_ : length l = 0) : l = [] := match l with | [] => rfl
 
-grind_pattern eq_nil_of_length_eq_zero => length l where
-  guard l.length = 0
-
 theorem ne_nil_of_length_eq_add_one (_ : length l = n + 1) : l ≠ [] := fun _ => nomatch l
 
 theorem ne_nil_of_length_pos (_ : 0 < length l) : l ≠ [] := fun _ => nomatch l
@@ -2941,6 +2940,9 @@ theorem getLast?_replicate {a : α} {n : Nat} : (replicate n a).getLast? = if n
 
 /-! ### leftpad -/
 
+-- We unfold `leftpad` and `rightpad` for verification purposes.
+attribute [simp, grind =] leftpad rightpad
+
 -- `length_leftpad` and `length_rightpad` are in `Init.Data.List.Nat.Basic`.
 
 theorem leftpad_prefix {n : Nat} {a : α} {l : List α} :

src/Init/Data/List/Sublist.lean

@@ -249,13 +249,12 @@ theorem Sublist.eq_of_length : l₁ <+ l₂ → length l₁ = length l₂ → l
   | .cons a s, h => nomatch Nat.not_lt.2 s.length_le (h ▸ lt_succ_self _)
   | .cons₂ a s, h => by rw [s.eq_of_length (succ.inj h)]
 
+-- Only activate `eq_of_length` if we're already thinking about lengths.
+grind_pattern Sublist.eq_of_length => l₁ <+ l₂, length l₁, length l₂
+
 theorem Sublist.eq_of_length_le (s : l₁ <+ l₂) (h : length l₂ ≤ length l₁) : l₁ = l₂ :=
   s.eq_of_length <| Nat.le_antisymm s.length_le h
 
--- Only activate `eq_of_length_le` if we're already thinking about lengths.
-grind_pattern Sublist.eq_of_length_le => l₁ <+ l₂, length l₁, length l₂ where
-  guard length l₂ ≤ length l₁
-
 theorem Sublist.length_eq (s : l₁ <+ l₂) : length l₁ = length l₂ ↔ l₁ = l₂ :=
   ⟨s.eq_of_length, congrArg _⟩
 

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

@@ -223,16 +223,6 @@ theorem testBit_lt_two_pow {x i : Nat} (lt : x < 2^i) : x.testBit i = false := b
     exfalso
     exact Nat.not_le_of_gt lt (ge_two_pow_of_testBit p)
 
-theorem testBit_of_two_pow_le_and_two_pow_add_one_gt {n i : Nat}
-    (hle : 2^i ≤ n) (hgt : n < 2^(i + 1)) : n.testBit i = true := by
-  rcases exists_ge_and_testBit_of_ge_two_pow hle with ⟨i', ⟨_, _⟩⟩
-  have : i = i' := by
-    false_or_by_contra
-    have : 2 ^ (i + 1) ≤ 2 ^ i' := Nat.pow_le_pow_of_le (by decide) (by omega)
-    have : n.testBit i' = false := testBit_lt_two_pow (by omega)
-    simp_all only [Bool.false_eq_true]
-  rwa [this]
-
 theorem lt_pow_two_of_testBit (x : Nat) (p : ∀i, i ≥ n → testBit x i = false) : x < 2^n := by
   apply Decidable.by_contra
   intro not_lt
@@ -241,10 +231,6 @@ theorem lt_pow_two_of_testBit (x : Nat) (p : ∀i, i ≥ n → testBit x i = fal
   have test_false := p _ i_ge_n
   simp [test_true] at test_false
 
-theorem testBit_log2 {n : Nat} (h : n ≠ 0) : n.testBit n.log2 = true := by
-  have := log2_eq_iff (n := n) (k := n.log2) (by omega)
-  apply testBit_of_two_pow_le_and_two_pow_add_one_gt <;> omega
-
 private theorem succ_mod_two : succ x % 2 = 1 - x % 2 := by
   induction x with
   | zero =>

src/Init/Data/Nat/Gcd.lean

@@ -129,9 +129,6 @@ theorem gcd_assoc (m n k : Nat) : gcd (gcd m n) k = gcd m (gcd n k) :=
       (Nat.dvd_trans (gcd_dvd_right m (gcd n k)) (gcd_dvd_right n k)))
 instance : Std.Associative gcd := ⟨gcd_assoc⟩
 
-theorem gcd_left_comm (m n k : Nat) : gcd m (gcd n k) = gcd n (gcd m k) := by
-  rw [← gcd_assoc, ← gcd_assoc, gcd_comm m n]
-
 @[simp] theorem gcd_one_right (n : Nat) : gcd n 1 = 1 := (gcd_comm n 1).trans (gcd_one_left n)
 
 theorem gcd_mul_left (m n k : Nat) : gcd (m * n) (m * k) = m * gcd n k := by

src/Init/Data/Nat/Lemmas.lean

@@ -10,7 +10,7 @@ import all Init.Data.Nat.Bitwise.Basic
 public import Init.Data.Nat.MinMax
 public import Init.Data.Nat.Log2
 import all Init.Data.Nat.Log2
-public import Init.Data.Nat.Power2.Basic
+public import Init.Data.Nat.Power2
 public import Init.Data.Nat.Mod
 import Init.TacticsExtra
 import Init.BinderPredicates

src/Init/Data/Nat/Power2.lean

@@ -6,5 +6,66 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.Nat.Power2.Basic
-public import Init.Data.Nat.Power2.Lemmas
+public import Init.Data.Nat.Linear
+
+public section
+
+namespace Nat
+
+theorem nextPowerOfTwo_dec {n power : Nat} (h₁ : power > 0) (h₂ : power < n) : n - power * 2 < n - power := by
+  have : power * 2 = power + power := by simp +arith
+  rw [this, Nat.sub_add_eq]
+  exact Nat.sub_lt (Nat.zero_lt_sub_of_lt h₂) h₁
+
+/--
+Returns the least power of two that's greater than or equal to `n`.
+
+Examples:
+ * `Nat.nextPowerOfTwo 0 = 1`
+ * `Nat.nextPowerOfTwo 1 = 1`
+ * `Nat.nextPowerOfTwo 2 = 2`
+ * `Nat.nextPowerOfTwo 3 = 4`
+ * `Nat.nextPowerOfTwo 5 = 8`
+-/
+def nextPowerOfTwo (n : Nat) : Nat :=
+  go 1 (by decide)
+where
+  go (power : Nat) (h : power > 0) : Nat :=
+    if power < n then
+      go (power * 2) (Nat.mul_pos h (by decide))
+    else
+      power
+  termination_by n - power
+  decreasing_by simp_wf; apply nextPowerOfTwo_dec <;> assumption
+
+/--
+A natural number `n` is a power of two if there exists some `k : Nat` such that `n = 2 ^ k`.
+-/
+def isPowerOfTwo (n : Nat) := ∃ k, n = 2 ^ k
+
+theorem isPowerOfTwo_one : isPowerOfTwo 1 :=
+  ⟨0, by decide⟩
+
+theorem isPowerOfTwo_mul_two_of_isPowerOfTwo (h : isPowerOfTwo n) : isPowerOfTwo (n * 2) :=
+  have ⟨k, h⟩ := h
+  ⟨k+1, by simp [h, Nat.pow_succ]⟩
+
+theorem pos_of_isPowerOfTwo (h : isPowerOfTwo n) : n > 0 := by
+  have ⟨k, h⟩ := h
+  rw [h]
+  apply Nat.pow_pos
+  decide
+
+theorem isPowerOfTwo_nextPowerOfTwo (n : Nat) : n.nextPowerOfTwo.isPowerOfTwo := by
+  apply isPowerOfTwo_go
+  apply isPowerOfTwo_one
+where
+  isPowerOfTwo_go (power : Nat) (h₁ : power > 0) (h₂ : power.isPowerOfTwo) : (nextPowerOfTwo.go n power h₁).isPowerOfTwo := by
+    unfold nextPowerOfTwo.go
+    split
+    . exact isPowerOfTwo_go (power*2) (Nat.mul_pos h₁ (by decide)) (Nat.isPowerOfTwo_mul_two_of_isPowerOfTwo h₂)
+    . assumption
+  termination_by n - power
+  decreasing_by simp_wf; apply nextPowerOfTwo_dec <;> assumption
+
+end Nat

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

@@ -1,71 +0,0 @@
-/-
-Copyright (c) 2022 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.Data.Nat.Linear
-
-public section
-
-namespace Nat
-
-theorem nextPowerOfTwo_dec {n power : Nat} (h₁ : power > 0) (h₂ : power < n) : n - power * 2 < n - power := by
-  have : power * 2 = power + power := by simp +arith
-  rw [this, Nat.sub_add_eq]
-  exact Nat.sub_lt (Nat.zero_lt_sub_of_lt h₂) h₁
-
-/--
-Returns the least power of two that's greater than or equal to `n`.
-
-Examples:
- * `Nat.nextPowerOfTwo 0 = 1`
- * `Nat.nextPowerOfTwo 1 = 1`
- * `Nat.nextPowerOfTwo 2 = 2`
- * `Nat.nextPowerOfTwo 3 = 4`
- * `Nat.nextPowerOfTwo 5 = 8`
--/
-def nextPowerOfTwo (n : Nat) : Nat :=
-  go 1 (by decide)
-where
-  go (power : Nat) (h : power > 0) : Nat :=
-    if power < n then
-      go (power * 2) (Nat.mul_pos h (by decide))
-    else
-      power
-  termination_by n - power
-  decreasing_by simp_wf; apply nextPowerOfTwo_dec <;> assumption
-
-/--
-A natural number `n` is a power of two if there exists some `k : Nat` such that `n = 2 ^ k`.
--/
-def isPowerOfTwo (n : Nat) := ∃ k, n = 2 ^ k
-
-theorem isPowerOfTwo_one : isPowerOfTwo 1 :=
-  ⟨0, by decide⟩
-
-theorem isPowerOfTwo_mul_two_of_isPowerOfTwo (h : isPowerOfTwo n) : isPowerOfTwo (n * 2) :=
-  have ⟨k, h⟩ := h
-  ⟨k+1, by simp [h, Nat.pow_succ]⟩
-
-theorem pos_of_isPowerOfTwo (h : isPowerOfTwo n) : n > 0 := by
-  have ⟨k, h⟩ := h
-  rw [h]
-  apply Nat.pow_pos
-  decide
-
-theorem isPowerOfTwo_nextPowerOfTwo (n : Nat) : n.nextPowerOfTwo.isPowerOfTwo := by
-  apply isPowerOfTwo_go
-  apply isPowerOfTwo_one
-where
-  isPowerOfTwo_go (power : Nat) (h₁ : power > 0) (h₂ : power.isPowerOfTwo) : (nextPowerOfTwo.go n power h₁).isPowerOfTwo := by
-    unfold nextPowerOfTwo.go
-    split
-    . exact isPowerOfTwo_go (power*2) (Nat.mul_pos h₁ (by decide)) (Nat.isPowerOfTwo_mul_two_of_isPowerOfTwo h₂)
-    . assumption
-  termination_by n - power
-  decreasing_by simp_wf; apply nextPowerOfTwo_dec <;> assumption
-
-end Nat

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

@@ -1,62 +0,0 @@
-/-
-Copyright (c) George Rennie. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: George Rennie
--/
-module
-
-prelude
-import all Init.Data.Nat.Power2.Basic
-public import Init.Data.Nat.Bitwise.Lemmas
-
-public section
-
-/-!
-# Further lemmas about `Nat.isPowerOfTwo`, with the convenience of having bitwise lemmas available.
--/
-
-namespace Nat
-
-theorem not_isPowerOfTwo_zero : ¬isPowerOfTwo 0 := by
-  rw [isPowerOfTwo, not_exists]
-  intro x
-  have := one_le_pow x 2 (by decide)
-  omega
-
-theorem and_sub_one_testBit_log2 {n : Nat} (h : n ≠ 0) (hpow2 : ¬n.isPowerOfTwo) :
-    (n &&& (n - 1)).testBit n.log2 := by
-  rw [testBit_and, Bool.and_eq_true]
-  constructor
-  · exact testBit_log2 (by omega)
-  · by_cases n = 2^n.log2
-    · rw [isPowerOfTwo, not_exists] at hpow2
-      have := hpow2 n.log2
-      trivial
-    · have := log2_eq_iff (n := n) (k := n.log2) (by omega)
-      have : (n - 1).log2 = n.log2 := by rw [log2_eq_iff] <;> omega
-      rw [←this]
-      exact testBit_log2 (by omega)
-
-theorem and_sub_one_eq_zero_iff_isPowerOfTwo {n : Nat} (h : n ≠ 0) :
-    (n &&& (n - 1)) = 0 ↔ n.isPowerOfTwo := by
-  constructor
-  · intro hbitwise
-    false_or_by_contra
-    rename_i hpow2
-    have := and_sub_one_testBit_log2 h hpow2
-    rwa [hbitwise, zero_testBit n.log2, Bool.false_eq_true] at this
-  · intro hpow2
-    rcases hpow2 with ⟨_, hpow2⟩
-    rw [hpow2, and_two_pow_sub_one_eq_mod, mod_self]
-
-theorem ne_zero_and_sub_one_eq_zero_iff_isPowerOfTwo {n : Nat} :
-    ((n ≠ 0) ∧ (n &&& (n - 1)) = 0) ↔ n.isPowerOfTwo := by
-  match h : n with
-  | 0 => simp [not_isPowerOfTwo_zero]
-  | n + 1 => simp; exact and_sub_one_eq_zero_iff_isPowerOfTwo (by omega)
-
-@[inline]
-instance {n : Nat} : Decidable n.isPowerOfTwo :=
-  decidable_of_iff _ ne_zero_and_sub_one_eq_zero_iff_isPowerOfTwo
-
-end Nat

src/Init/Data/Order/Ord.lean

@@ -46,7 +46,7 @@ theorem ne_of_cmp_ne_eq {α : Type u} {cmp : α → α → Ordering} [Std.ReflCm
 
 end ReflCmp
 
-/-- A typeclass for ordered types for which `compare a a = .eq` for all `a`. -/
+/-- A typeclasses for ordered types for which `compare a a = .eq` for all `a`. -/
 abbrev ReflOrd (α : Type u) [Ord α] := ReflCmp (compare : α → α → Ordering)
 
 @[simp]

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

@@ -6,6 +6,7 @@ Authors: Paul Reichert
 module
 
 prelude
+public import Init.Data.Iterators.Internal.Termination
 public import Init.Data.Iterators.Consumers.Access
 import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
 public import Init.Data.Range.Polymorphic.PRange
@@ -231,7 +232,7 @@ private def List.length_filter_strict_mono {l : List α} {P Q : α → Bool} {a
 private def Iterator.instFinitenessRelation [UpwardEnumerable α] [LE α] [DecidableLE α]
     [LawfulUpwardEnumerable α] [Rxc.IsAlwaysFinite α] :
     FinitenessRelation (Rxc.Iterator α) Id where
-  Rel it' it := it'.IsPlausibleSuccessorOf it
+  rel it' it := it'.IsPlausibleSuccessorOf it
   wf := by
     constructor
     intro it
@@ -284,7 +285,7 @@ instance Iterator.instFinite [UpwardEnumerable α] [LE α] [DecidableLE α]
 private def Iterator.instProductivenessRelation [UpwardEnumerable α] [LE α] [DecidableLE α]
     [LawfulUpwardEnumerable α] :
     ProductivenessRelation (Rxc.Iterator α) Id where
-  Rel := emptyWf.rel
+  rel := emptyWf.rel
   wf := emptyWf.wf
   subrelation {it it'} h := by
     exfalso
@@ -807,7 +808,7 @@ private def List.length_filter_strict_mono {l : List α} {P Q : α → Bool} {a
 private def Iterator.instFinitenessRelation [UpwardEnumerable α] [LT α] [DecidableLT α]
     [LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] :
     FinitenessRelation (Rxo.Iterator α) Id where
-  Rel it' it := it'.IsPlausibleSuccessorOf it
+  rel it' it := it'.IsPlausibleSuccessorOf it
   wf := by
     constructor
     intro it
@@ -860,7 +861,7 @@ instance Iterator.instFinite [UpwardEnumerable α] [LT α] [DecidableLT α]
 private def Iterator.instProductivenessRelation [UpwardEnumerable α] [LT α] [DecidableLT α]
     [LawfulUpwardEnumerable α] :
     ProductivenessRelation (Rxo.Iterator α) Id where
-  Rel := emptyWf.rel
+  rel := emptyWf.rel
   wf := emptyWf.wf
   subrelation {it it'} h := by
     exfalso
@@ -1329,7 +1330,7 @@ theorem Iterator.isSome_next_of_isPlausibleIndirectOutput
 private def Iterator.instFinitenessRelation [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] :
     FinitenessRelation (Rxi.Iterator α) Id where
-  Rel it' it := it'.IsPlausibleSuccessorOf it
+  rel it' it := it'.IsPlausibleSuccessorOf it
   wf := by
     constructor
     intro it
@@ -1374,7 +1375,7 @@ instance Iterator.instFinite [UpwardEnumerable α]
 private def Iterator.instProductivenessRelation [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] :
     ProductivenessRelation (Rxi.Iterator α) Id where
-  Rel := emptyWf.rel
+  rel := emptyWf.rel
   wf := emptyWf.wf
   subrelation {it it'} h := by
     exfalso

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

@@ -246,12 +246,8 @@ class InfinitelyUpwardEnumerable (α : Type u) [UpwardEnumerable α] where
 This propositional typeclass ensures that `UpwardEnumerable.succ?` is injective.
 -/
 class LinearlyUpwardEnumerable (α : Type u) [UpwardEnumerable α] where
-  /-- The implementation of `UpwardEnumerable.succ?` for `α` is injective. -/
   eq_of_succ?_eq : ∀ a b : α, UpwardEnumerable.succ? a = UpwardEnumerable.succ? b → a = b
 
-/--
-If a type is infinitely upwardly enumerable, then every element has a successor.
--/
 theorem UpwardEnumerable.isSome_succ? {α : Type u} [UpwardEnumerable α]
     [InfinitelyUpwardEnumerable α] {a : α} : (succ? a).isSome :=
   InfinitelyUpwardEnumerable.isSome_succ? a

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

@@ -45,7 +45,7 @@ instance : Iterator (SubarrayIterator α) Id α where
   step it := pure <| .deflate ⟨SubarrayIterator.step it, rfl⟩
 
 private def SubarrayIterator.instFinitelessRelation : FinitenessRelation (SubarrayIterator α) Id where
-  Rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.xs.stop - it.internalState.xs.start)
+  rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.xs.stop - it.internalState.xs.start)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by
     simp [IterM.IsPlausibleSuccessorOf, IterM.IsPlausibleStep, Iterator.IsPlausibleStep, step] at h

src/Init/Data/Slice/Notation.lean

@@ -40,7 +40,7 @@ class Rcc.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type
 This typeclass indicates how to obtain slices of elements of {lit}`α` over ranges in the index type
 {lit}`β`, the ranges being left-closed right-open.
 
-The type of the resulting slices is {lit}`γ`.
+The type of resulting the slices is {lit}`γ`.
 -/
 class Rco.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
   /--

src/Init/Data/String/Decode.lean

@@ -1396,7 +1396,6 @@ scalar value.
 public def IsUTF8FirstByte (c : UInt8) : Prop :=
   c &&& 0x80 = 0 ∨ c &&& 0xe0 = 0xc0 ∨ c &&& 0xf0 = 0xe0 ∨ c &&& 0xf8 = 0xf0
 
-@[inline]
 public instance {c : UInt8} : Decidable c.IsUTF8FirstByte :=
   inferInstanceAs <| Decidable (c &&& 0x80 = 0 ∨ c &&& 0xe0 = 0xc0 ∨ c &&& 0xf0 = 0xe0 ∨ c &&& 0xf8 = 0xf0)
 

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

@@ -57,10 +57,4 @@ theorem length_map {f : Char → Char} {s : String} : (s.map f).length = s.lengt
 theorem map_eq_empty {f : Char → Char} {s : String} : s.map f = "" ↔ s = "" := by
   simp [← toList_eq_nil_iff]
 
-@[simp]
-theorem map_idempotent {s : String} (h : (c : Char) → f (f c) = f c) : (s.map f |>.map f) = s.map f := by
-  apply String.ext
-  simp [String.toList_map, List.map_map]
-  exact fun c _ => h c
-
 end String

src/Init/Data/String/Modify.lean

@@ -230,7 +230,7 @@ Examples:
 * `"Orange".toLower = "orange"`
 * `"ABc123".toLower = "abc123"`
 -/
-@[inline, expose] def toLower (s : String) : String :=
+@[inline] def toLower (s : String) : String :=
   s.map Char.toLower
 
 /--

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

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.String.Pattern.Basic
+public import Init.Data.Iterators.Internal.Termination
 public import Init.Data.Iterators.Consumers.Monadic.Loop
 import Init.Data.String.Termination
 
@@ -58,7 +59,7 @@ instance (s : Slice) : Std.Iterator (ForwardCharSearcher c s) Id (SearchStep s)
         pure (.deflate ⟨.yield nextIt (.rejected currPos nextPos), by simp [h1, h2, nextIt, nextPos]⟩)
 
 def finitenessRelation : Std.Iterators.FinitenessRelation (ForwardCharSearcher s c) Id where
-  Rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.currPos)
+  rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.currPos)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by
     simp_wf
@@ -123,7 +124,7 @@ instance (s : Slice) : Std.Iterator (BackwardCharSearcher s) Id (SearchStep s) w
         pure (.deflate ⟨.yield nextIt (.rejected nextPos currPos), by simp [h1, h2, nextIt, nextPos]⟩)
 
 def finitenessRelation : Std.Iterators.FinitenessRelation (BackwardCharSearcher s) Id where
-  Rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.currPos.down)
+  rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.currPos.down)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by
     simp_wf

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

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.String.Pattern.Basic
+public import Init.Data.Iterators.Internal.Termination
 public import Init.Data.Iterators.Consumers.Monadic.Loop
 import Init.Data.String.Termination
 
@@ -60,7 +61,7 @@ instance (s : Slice) : Std.Iterator (ForwardCharPredSearcher p s) Id (SearchStep
 
 
 def finitenessRelation : Std.Iterators.FinitenessRelation (ForwardCharPredSearcher p s) Id where
-  Rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.currPos)
+  rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.currPos)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by
     simp_wf
@@ -133,7 +134,7 @@ instance (s : Slice) : Std.Iterator (BackwardCharPredSearcher s) Id (SearchStep
         pure (.deflate ⟨.yield nextIt (.rejected nextPos currPos), by simp [h1, h2, nextIt, nextPos]⟩)
 
 def finitenessRelation : Std.Iterators.FinitenessRelation (BackwardCharPredSearcher s) Id where
-  Rel := InvImage WellFoundedRelation.rel
+  rel := InvImage WellFoundedRelation.rel
       (fun it => it.internalState.currPos.offset.byteIdx)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by

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

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.String.Pattern.Basic
+public import Init.Data.Iterators.Internal.Termination
 public import Init.Data.Iterators.Consumers.Monadic.Loop
 import Init.Data.String.Termination
 public import Init.Data.Vector.Basic
@@ -119,7 +120,7 @@ instance (s : Slice) : Std.Iterator (ForwardSliceSearcher s) Id (SearchStep s) w
       -- **Invariant 1:** we have already covered everything up until `stackPos - needlePos` (exclusive),
       -- with matches and rejections.
       -- **Invariant 2:** `stackPos - needlePos` is a valid position
-      -- **Invariant 3:** the range from `stackPos - needlePos` to `stackPos` (exclusive) is a
+      -- **Invariant 3:** the range from from `stackPos - needlePos` to `stackPos` (exclusive) is a
       -- prefix of the pattern.
       if h₁ : stackPos < s.rawEndPos then
         let stackByte := s.getUTF8Byte stackPos h₁
@@ -222,7 +223,7 @@ private instance : WellFoundedRelation (ForwardSliceSearcher s) where
 
 private def finitenessRelation :
     Std.Iterators.FinitenessRelation (ForwardSliceSearcher s) Id where
-  Rel := InvImage WellFoundedRelation.rel (fun it => it.internalState)
+  rel := InvImage WellFoundedRelation.rel (fun it => it.internalState)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by
     simp_wf

src/Init/Data/String/Slice.lean

@@ -20,7 +20,7 @@ functionality for searching for various kinds of pattern matches in slices to it
 provide subslices according to matches etc. The key design principles behind this module are:
 - Instead of providing one function per kind of pattern the API is generic over various kinds of
   patterns. Thus it only provides e.g. one kind of function for looking for the position of the
-  first occurrence of a pattern. Currently the supported patterns are:
+  first occurence of a pattern. Currently the supported patterns are:
   - {name}`Char`
   - {lean}`Char → Bool`
   - {name}`String` and {name}`String.Slice` (partially: doing non trivial searches backwards is not
@@ -165,7 +165,7 @@ private def toOption : SplitIterator pat s → Option (Std.Iter (α := σ s) (Se
 
 private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
     Std.Iterators.FinitenessRelation (SplitIterator pat s) Id where
-  Rel := InvImage (Option.lt Std.Iter.IsPlausibleSuccessorOf)
+  rel := InvImage (Option.lt Std.Iter.IsPlausibleSuccessorOf)
     (SplitIterator.toOption ∘ Std.IterM.internalState)
   wf := InvImage.wf _ (Option.wellFounded_lt Std.Iterators.Finite.wf_of_id)
   subrelation {it it'} h := by
@@ -256,7 +256,7 @@ private def toOption : SplitInclusiveIterator pat s → Option (Std.Iter (α :=
 
 private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
     Std.Iterators.FinitenessRelation (SplitInclusiveIterator pat s) Id where
-  Rel := InvImage (Option.lt Std.Iter.IsPlausibleSuccessorOf)
+  rel := InvImage (Option.lt Std.Iter.IsPlausibleSuccessorOf)
     (SplitInclusiveIterator.toOption ∘ Std.IterM.internalState)
   wf := InvImage.wf _ (Option.wellFounded_lt Std.Iterators.Finite.wf_of_id)
   subrelation {it it'} h := by
@@ -596,7 +596,7 @@ private def toOption : RevSplitIterator ρ s → Option (Std.Iter (α := σ s) (
 
 private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
     Std.Iterators.FinitenessRelation (RevSplitIterator ρ s) Id where
-  Rel := InvImage (Option.lt Std.Iter.IsPlausibleSuccessorOf)
+  rel := InvImage (Option.lt Std.Iter.IsPlausibleSuccessorOf)
     (RevSplitIterator.toOption ∘ Std.IterM.internalState)
   wf := InvImage.wf _ (Option.wellFounded_lt Std.Iterators.Finite.wf_of_id)
   subrelation {it it'} h := by
@@ -867,7 +867,7 @@ instance [Pure m] :
 
 private def finitenessRelation [Pure m] :
     Std.Iterators.FinitenessRelation (PosIterator s) m where
-  Rel := InvImage WellFoundedRelation.rel
+  rel := InvImage WellFoundedRelation.rel
       (fun it => s.utf8ByteSize - it.internalState.currPos.offset.byteIdx)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by
@@ -949,7 +949,7 @@ instance [Pure m] :
 
 private def finitenessRelation [Pure m] :
     Std.Iterators.FinitenessRelation (RevPosIterator s) m where
-  Rel := InvImage WellFoundedRelation.rel
+  rel := InvImage WellFoundedRelation.rel
       (fun it => it.internalState.currPos.offset.byteIdx)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by
@@ -1024,7 +1024,7 @@ instance [Pure m] : Std.Iterator ByteIterator m UInt8 where
 
 private def finitenessRelation [Pure m] :
     Std.Iterators.FinitenessRelation (ByteIterator) m where
-  Rel := InvImage WellFoundedRelation.rel
+  rel := InvImage WellFoundedRelation.rel
       (fun it => it.internalState.s.utf8ByteSize - it.internalState.offset.byteIdx)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by
@@ -1104,7 +1104,7 @@ instance [Pure m] : Std.Iterator RevByteIterator m UInt8 where
 
 private def finitenessRelation [Pure m] :
     Std.Iterators.FinitenessRelation (RevByteIterator) m where
-  Rel := InvImage WellFoundedRelation.rel
+  rel := InvImage WellFoundedRelation.rel
       (fun it => it.internalState.offset.byteIdx)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by

src/Init/Data/Vector/Lemmas.lean

@@ -796,8 +796,7 @@ theorem getElem?_eq_none {xs : Vector α n} (h : n ≤ i) : xs[i]? = none := by
 
 -- This is a more aggressive pattern than for `List/Array.getElem?_eq_none`, because
 -- `length/size` won't appear.
-grind_pattern Vector.getElem?_eq_none => xs[i]? where
-  guard n ≤ i
+grind_pattern Vector.getElem?_eq_none => xs[i]?
 
 @[simp] theorem getElem?_eq_getElem {xs : Vector α n} {i : Nat} (h : i < n) : xs[i]? = some xs[i] :=
   getElem?_pos ..

src/Init/GetElem.lean

@@ -366,11 +366,9 @@ instance : GetElem? (List α) Nat α fun as i => i < as.length where
 theorem none_eq_getElem?_iff {l : List α} {i : Nat} : none = l[i]? ↔ length l ≤ i := by
   simp [eq_comm (a := none)]
 
+@[grind =]
 theorem getElem?_eq_none (h : length l ≤ i) : l[i]? = none := getElem?_eq_none_iff.mpr h
 
-grind_pattern getElem?_eq_none => l.length, l[i]? where
-  guard l.length ≤ i
-
 instance : LawfulGetElem (List α) Nat α fun as i => i < as.length where
   getElem?_def as i h := by
     split <;> simp_all

src/Init/Grind/Attr.lean

@@ -198,55 +198,6 @@ Given an application `f a₁ a₂ … aₙ`, when `funCC := true`,
 -/
 syntax grindFunCC  := &"funCC"
 /--
-The `norm` modifier instructs `grind` to use a theorem as a normalization rule. That is,
-the theorem is applied during the preprocessing step.
-This feature is meant for advanced users who understand how the preprocessor and `grind`'s search
-procedure interact with each other.
-New users can still benefit from this feature by restricting its use to theorems that completely
-eliminate a symbol from the goal. Example:
-```
-theorem max_def : max n m = if n ≤ m then m else n
-```
-For a negative example, consider:
-```
-opaque f : Int → Int → Int → Int
-theorem fax1 : f x 0 1 = 1 := sorry
-theorem fax2 : f 1 x 1 = 1 := sorry
-attribute [grind norm] fax1
-attribute [grind =] fax2
-
-example (h : c = 1) : f c 0 c = 1 := by
-  grind -- fails
-```
-In this example, `fax1` is a normalization rule, but it is not applicable to the input goal since
-`f c 0 c` is not an instance of `f x 0 1`. However, `f c 0 c` matches the pattern `f 1 x 1` modulo
-the equality `c = 1`. Thus, `grind` instantiates `fax2` with `x := 0`, producing the equality
-`f 1 0 1 = 1`, which the normalizer simplifies to `True`. As a result, nothing useful is learned.
-In the future, we plan to include linters to automatically detect issues like these.
-Example:
-```
-opaque f : Nat → Nat
-opaque g : Nat → Nat
-
-@[grind norm] axiom fax : f x = x + 2
-@[grind norm ←] axiom fg : f x = g x
-
-example : f x ≥ 2 := by grind
-example : f x ≥ g x := by grind
-example : f x + g x ≥ 4 := by grind
-```
--/
-syntax grindNorm  := &"norm" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("← " <|> "<- ")?
-/--
-The `unfold` modifier instructs `grind` to unfold the given definition during the preprocessing step.
-Example:
-```
-@[grind unfold] def h (x : Nat) := 2 * x
-example : 6 ∣ 3*h x := by grind
-```
--/
-syntax grindUnfold := &"unfold"
-/--
 `symbol <prio>` sets the priority of a constant for `grind`’s pattern-selection
 procedure. `grind` prefers patterns that contain higher-priority symbols.
 Example:
@@ -273,7 +224,7 @@ syntax grindMod :=
     grindEqBoth <|> grindEqRhs <|> grindEq <|> grindEqBwd <|> grindBwd
     <|> grindFwd <|> grindRL <|> grindLR <|> grindUsr <|> grindCasesEager
     <|> grindCases <|> grindIntro <|> grindExt <|> grindGen <|> grindSym <|> grindInj
-    <|> grindFunCC <|> grindNorm <|> grindUnfold <|> grindDef
+    <|> grindFunCC <|> grindDef
 
 /--
 Marks a theorem or definition for use by the `grind` tactic.
@@ -304,7 +255,6 @@ theorem fg_eq (h : x > 0) : f (g x) = x
 -- With minimal subexpression:
 @[grind! <-] theorem fg_eq (h : x > 0) : f (g x) = x
 -- Pattern selected: `g x`
-```
 -/
 syntax (name := grind!) "grind!" (ppSpace grindMod)? : attr
 /--

src/Init/Grind/Config.lean

@@ -21,8 +21,6 @@ structure Config where
   /-- If `suggestions` is `true`, `grind` will invoke the currently configured library suggestion engine on the current goal,
   and add attempt to use the resulting suggestions as additional parameters to the `grind` tactic. -/
   suggestions : Bool := false
-  /-- If `locals` is `true`, `grind` will add all definitions from the current file. -/
-  locals : Bool := false
   /-- Maximum number of case-splits in a proof search branch. It does not include splits performed during normalization. -/
   splits : Nat := 9
   /-- Maximum number of E-matching (aka heuristic theorem instantiation) rounds before each case split. -/

src/Init/Grind/Ring/CommSolver.lean

@@ -766,7 +766,7 @@ def Poly.cancelVar (c : Int) (x : Var) (p : Poly) : Poly :=
           (fun _ _ _ _ => a.toPoly_k.pow k)
           (fun _ _ _ _ => a.toPoly_k.pow k)
           (fun _ _ _ => a.toPoly_k.pow k)
-          a) = match a with
+          a) = match (generalizing := false) a with
             | num n => Poly.num (n ^ k)
             | .intCast n => .num (n^k)
             | .natCast n => .num (n^k)

src/Init/MetaTypes.lean

@@ -36,8 +36,6 @@ inductive TransparencyMode where
   | reducible
   /-- Unfolds reducible constants and constants tagged with the `@[instance]` attribute. -/
   | instances
-  /-- Do not unfold anything -/
-  | none
   deriving Inhabited, BEq
 
 /-- Which structure types should eta be used with? -/
@@ -132,11 +130,6 @@ structure Config where
   Unused `have`s are still removed if `zeta` or `zetaUnused` are true.
   -/
   zetaHave : Bool := true
-  /--
-  If `locals` is `true`, `dsimp` will unfold all definitions from the current file.
-  For local theorems, use `+suggestions` instead.
-  -/
-  locals : Bool := false
   deriving Inhabited, BEq
 
 end DSimp
@@ -302,11 +295,6 @@ structure Config where
   and attempt to use the resulting suggestions as parameters to the `simp` tactic.
   -/
   suggestions : Bool := false
-  /--
-  If `locals` is `true`, `simp` will unfold all definitions from the current file.
-  For local theorems, use `+suggestions` instead.
-  -/
-  locals : Bool := false
   deriving Inhabited, BEq
 
 -- Configuration object for `simp_all`

src/Init/Notation.lean

@@ -523,7 +523,7 @@ macro_rules
   | `(bif $c then $t else $e) => `(cond $c $t $e)
 
 /--
-Haskell-like pipe operator `<|`. `f <| x` means the same as `f x`,
+Haskell-like pipe operator `<|`. `f <| x` means the same as the same as `f x`,
 except that it parses `x` with lower precedence, which means that `f <| g <| x`
 is interpreted as `f (g x)` rather than `(f g) x`.
 -/
@@ -557,7 +557,7 @@ macro_rules
   | `($a |> $f)        => `($f $a)
 
 /--
-Alternative syntax for `<|`. `f $ x` means the same as `f x`,
+Alternative syntax for `<|`. `f $ x` means the same as the same as `f x`,
 except that it parses `x` with lower precedence, which means that `f $ g $ x`
 is interpreted as `f (g x)` rather than `(f g) x`.
 -/
@@ -782,16 +782,9 @@ Position reporting for `#guard_msgs`:
 -/
 syntax guardMsgsPositions := &"positions" " := " guardMsgsPositionsArg
 
-/--
-Substring matching for `#guard_msgs`:
-- `substring := true` checks that the docstring appears as a substring of the output.
-- `substring := false` (the default) requires exact matching (modulo whitespace normalization).
--/
-syntax guardMsgsSubstring := &"substring" " := " (&"true" <|> &"false")
-
 set_option linter.missingDocs false in
 syntax guardMsgsSpecElt :=
-  guardMsgsFilter <|> guardMsgsWhitespace <|> guardMsgsOrdering <|> guardMsgsPositions <|> guardMsgsSubstring
+  guardMsgsFilter <|> guardMsgsWhitespace <|> guardMsgsOrdering <|> guardMsgsPositions
 
 set_option linter.missingDocs false in
 syntax guardMsgsSpec := "(" guardMsgsSpecElt,* ")"
@@ -867,11 +860,6 @@ Position reporting:
   `#guard_msgs` appears.
 - `positions := false` does not report position info.
 
-Substring matching:
-- `substring := true` checks that the docstring appears as a substring of the output
-  (after whitespace normalization). This is useful when you only care about part of the message.
-- `substring := false` (the default) requires exact matching (modulo whitespace normalization).
-
 For example, `#guard_msgs (error, drop all) in cmd` means to check errors and drop
 everything else.
 
@@ -885,13 +873,6 @@ The top-level command elaborator only runs the linters if `#guard_msgs` is not p
 syntax (name := guardMsgsCmd)
   (plainDocComment)? "#guard_msgs" (ppSpace guardMsgsSpec)? " in" ppLine command : command
 
-/--
-`#guard_panic in cmd` runs `cmd` and succeeds if the command produces a panic message.
-This is useful for testing that a command panics without matching the exact (volatile) panic text.
--/
-syntax (name := guardPanicCmd)
-  "#guard_panic" " in" ppLine command : command
-
 /--
 Format and print the info trees for a given command.
 This is mostly useful for debugging info trees.

src/Init/NotationExtra.lean

@@ -67,7 +67,7 @@ syntax unifConstraint := term patternIgnore(" =?= " <|> " ≟ ") term
 syntax unifConstraintElem := colGe unifConstraint ", "?
 
 syntax (docComment)? attrKind "unif_hint" (ppSpace ident)? (ppSpace bracketedBinder)*
-  " where " withPosition(unifConstraintElem*) patternIgnore(atomic("|" noWs "-") <|> "⊢") ppSpace unifConstraint : command
+  " where " withPosition(unifConstraintElem*) patternIgnore(atomic("|" noWs "-") <|> "⊢") unifConstraint : command
 
 macro_rules
   | `($[$doc?:docComment]? $kind:attrKind unif_hint $(n)? $bs* where $[$cs₁ ≟ $cs₂]* |- $t₁ ≟ $t₂) => do
@@ -120,7 +120,7 @@ calc
   _ = z := pyz
 ```
 It is also possible to write the *first* relation as `<lhs>\n  _ = <rhs> :=
-<proof>`. This is useful for aligning relation symbols, especially on longer
+<proof>`. This is useful for aligning relation symbols, especially on longer:
 identifiers:
 ```
 calc abc

src/Init/Prelude.lean

@@ -375,10 +375,6 @@ theorem congr {α : Sort u} {β : Sort v} {f₁ f₂ : α → β} {a₁ a₂ :
 theorem congrFun {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} (h : Eq f g) (a : α) : Eq (f a) (g a) :=
   h ▸ rfl
 
-/-- Similar to `congrFun` but `β` does not depend on `α`. -/
-theorem congrFun' {α : Sort u} {β : Sort v} {f g : α → β} (h : Eq f g) (a : α) : Eq (f a) (g a) :=
-  h ▸ rfl
-
 /-!
 Initialize the Quotient Module, which effectively adds the following definitions:
 ```
@@ -907,7 +903,7 @@ instance [Inhabited α] : Inhabited (ULift α) where
 Lifts a type or proposition to a higher universe level.
 
 `PULift α` wraps a value of type `α`. It is a generalization of
-`PLift` that allows lifting values whose type may live in `Sort s`.
+`PLift` that allows lifting values who's type may live in `Sort s`.
 It also subsumes `PLift`.
 -/
 -- The universe variable `r` is written first so that `ULift.{r} α` can be used
@@ -3525,7 +3521,7 @@ instance : DecidableEq String.Pos.Raw :=
 /--
 A region or slice of some underlying string.
 
-A substring contains a string together with the start and end byte positions of a region of
+A substring contains an string together with the start and end byte positions of a region of
 interest. Actually extracting a substring requires copying and memory allocation, while many
 substrings of the same underlying string may exist with very little overhead, and they are more
 convenient than tracking the bounds by hand.

src/Init/SimpLemmas.lean

@@ -38,12 +38,6 @@ theorem eq_false_of_decide {p : Prop} {_ : Decidable p} (h : decide p = false) :
 theorem implies_congr {p₁ p₂ : Sort u} {q₁ q₂ : Sort v} (h₁ : p₁ = p₂) (h₂ : q₁ = q₂) : (p₁ → q₁) = (p₂ → q₂) :=
   h₁ ▸ h₂ ▸ rfl
 
-theorem implies_congr_left {p₁ p₂ : Sort u} {q : Sort v} (h : p₁ = p₂) : (p₁ → q) = (p₂ → q) :=
-  h ▸ rfl
-
-theorem implies_congr_right {p : Sort u} {q₁ q₂ : Sort v} (h : q₁ = q₂) : (p → q₁) = (p → q₂) :=
-  h ▸ rfl
-
 theorem iff_congr {p₁ p₂ q₁ q₂ : Prop} (h₁ : p₁ ↔ p₂) (h₂ : q₁ ↔ q₂) : (p₁ ↔ q₁) ↔ (p₂ ↔ q₂) :=
   Iff.of_eq (propext h₁ ▸ propext h₂ ▸ rfl)
 

src/Init/System/FilePath.lean

@@ -150,7 +150,7 @@ def parent (p : FilePath) : Option FilePath :=
 /--
 Extracts the last element of a path if it is a file or directory name.
 
-Returns `none` if the last entry is a special name (such as `.` or `..`) or if the path is the root
+Returns `none ` if the last entry is a special name (such as `.` or `..`) or if the path is the root
 directory.
 -/
 def fileName (p : FilePath) : Option String :=

src/Init/System/IO.lean

@@ -561,7 +561,7 @@ Waits for the task to finish, then returns its result.
   return t.get
 
 /--
-Waits until any of the tasks in the list has finished, then returns its result.
+Waits until any of the tasks in the list has finished, then return its result.
 -/
 @[extern "lean_io_wait_any"] opaque waitAny (tasks : @& List (Task α))
     (h : tasks.length > 0 := by exact Nat.zero_lt_succ _) : BaseIO α :=
@@ -679,7 +679,7 @@ File handles wrap the underlying operating system's file descriptors. There is n
 to close a file: when the last reference to a file handle is dropped, the file is closed
 automatically.
 
-Handles have an associated read/write cursor that determines where reads and writes occur in the
+Handles have an associated read/write cursor that determines the where reads and writes occur in the
 file.
 -/
 opaque FS.Handle : Type := Unit
@@ -790,7 +790,7 @@ An exception is thrown if the file cannot be opened.
 /--
 Acquires an exclusive or shared lock on the handle. Blocks to wait for the lock if necessary.
 
-Acquiring an exclusive lock while already possessing a shared lock will **not** reliably succeed: it
+Acquiring a exclusive lock while already possessing a shared lock will **not** reliably succeed: it
 works on Unix-like systems but not on Windows.
 -/
 @[extern "lean_io_prim_handle_lock"] opaque lock (h : @& Handle) (exclusive := true) : IO Unit
@@ -798,7 +798,7 @@ works on Unix-like systems but not on Windows.
 Tries to acquire an exclusive or shared lock on the handle and returns `true` if successful. Will
 not block if the lock cannot be acquired, but instead returns `false`.
 
-Acquiring an exclusive lock while already possessing a shared lock will **not** reliably succeed: it
+Acquiring a exclusive lock while already possessing a shared lock will **not** reliably succeed: it
 works on Unix-like systems but not on Windows.
 -/
 @[extern "lean_io_prim_handle_try_lock"] opaque tryLock (h : @& Handle) (exclusive := true) : IO Bool
@@ -1350,7 +1350,7 @@ def withTempFile [Monad m] [MonadFinally m] [MonadLiftT IO m] (f : Handle → Fi
     removeFile path
 
 /--
-Creates a temporary directory in the most secure manner possible, providing its path to an `IO`
+Creates a temporary directory in the most secure manner possible, providing a its path to an `IO`
 action. Afterwards, all files in the temporary directory are recursively deleted, regardless of how
 or when they were created.
 
@@ -1480,7 +1480,7 @@ possible to close the child's standard input before the process terminates, whic
 @[extern "lean_io_process_spawn"] opaque spawn (args : SpawnArgs) : IO (Child args.toStdioConfig)
 
 /--
-Blocks until the child process has exited and returns its exit code.
+Blocks until the child process has exited and return its exit code.
 -/
 @[extern "lean_io_process_child_wait"] opaque Child.wait {cfg : @& StdioConfig} : @& Child cfg → IO UInt32
 
@@ -1586,7 +1586,7 @@ end Process
 /--
 POSIX-style file permissions.
 
-The `FileRight` structure describes these permissions for a file's owner, members of its designated
+The `FileRight` structure describes these permissions for a file's owner, members of it's designated
 group, and all others.
 -/
 structure AccessRight where
@@ -1863,7 +1863,7 @@ unsafe def Runtime.markPersistent (a : α) : BaseIO α := return a
 
 set_option linter.unusedVariables false in
 /--
-Discards the passed owned reference. This leads to `a` and any object reachable from it never being
+Discards the passed owned reference. This leads to `a` any any object reachable from it never being
 freed. This can be a useful optimization for eliding deallocation time of big object graphs that are
 kept alive close to the end of the process anyway (in which case calling `Runtime.markPersistent`
 would be similarly costly to deallocation). It is still considered a safe operation as it cannot

src/Init/Tactics.lean

@@ -369,12 +369,6 @@ In this setting all definitions that are not opaque are unfolded.
 -/
 syntax (name := withUnfoldingAll) "with_unfolding_all " tacticSeq : tactic
 
-/--
-`with_unfolding_none tacs` executes `tacs` using the `.none` transparency setting.
-In this setting no definitions are unfolded.
--/
-syntax (name := withUnfoldingNone) "with_unfolding_none " tacticSeq : tactic
-
 /-- `first | tac | ...` runs each `tac` until one succeeds, or else fails. -/
 syntax (name := first) "first " withPosition((ppDedent(ppLine) colGe "| " tacticSeq)+) : tactic
 

src/Init/Try.lean

@@ -58,9 +58,6 @@ syntax (name := attemptAll) "attempt_all " withPosition((ppDedent(ppLine) colGe
 /-- Helper internal tactic for implementing the tactic `try?` with parallel execution. -/
 syntax (name := attemptAllPar) "attempt_all_par " withPosition((ppDedent(ppLine) colGe "| " tacticSeq)+) : tactic
 
-/-- Helper internal tactic for implementing the tactic `try?` with parallel execution, returning first success. -/
-syntax (name := firstPar) "first_par " withPosition((ppDedent(ppLine) colGe "| " tacticSeq)+) : tactic
-
 /-- Helper internal tactic used to implement `evalSuggest` in `try?` -/
 syntax (name := tryResult) "try_suggestions " tactic* : tactic
 

src/Init/WF.lean

@@ -463,7 +463,7 @@ variable {motive : α → Sort v}
 variable (h : α → Nat)
 variable (F : (x : α) → ((y : α) → InvImage (· < ·) h y x → motive y) → motive x)
 
-/-- Helper gadget that prevents reduction of `Nat.eager n` unless `n` evaluates to a ground term. -/
+/-- Helper gadget that prevents reduction of `Nat.eager n` unless `n` evalutes to a ground term. -/
 def Nat.eager (n : Nat) : Nat :=
   if Nat.beq n n = true then n else n
 
@@ -474,8 +474,8 @@ A well-founded fixpoint operator specialized for `Nat`-valued measures. Given a
 its higher order function argument `F` to invoke its argument only on values `y` that are smaller
 than `x` with regard to `h`.
 
-In contrast to `WellFounded.fix`, this fixpoint operator reduces on closed terms. (More precisely:
-when `h x` evaluates to a ground value)
+In contrast to to `WellFounded.fix`, this fixpoint operator reduces on closed terms. (More precisely:
+when `h x` evalutes to a ground value)
 
 -/
 def Nat.fix : (x : α) → motive x :=

src/Lean.lean

@@ -44,6 +44,7 @@ public import Lean.LibrarySuggestions
 public import Lean.Namespace
 public import Lean.EnvExtension
 public import Lean.ErrorExplanation
+public import Lean.ErrorExplanations
 public import Lean.DefEqAttrib
 public import Lean.Shell
 public import Lean.ExtraModUses

src/Lean/Compiler/LCNF/Basic.lean

@@ -147,11 +147,18 @@ inductive Alt where
   | alt (ctorName : Name) (params : Array Param) (code : Code)
   | default (code : Code)
 
-inductive FunDecl where
-  | mk (fvarId : FVarId) (binderName : Name) (params : Array Param) (type : Expr) (value : Code)
+structure FunDecl where
+  fvarId : FVarId
+  binderName : Name
+  params : Array Param
+  type : Expr
+  value : Code
 
-inductive Cases where
-  | mk (typeName : Name) (resultType : Expr) (discr : FVarId) (alts : Array Alt)
+structure Cases where
+  typeName : Name
+  resultType : Expr
+  discr : FVarId
+  alts : Array Alt
   deriving Inhabited
 
 inductive Code where
@@ -166,57 +173,6 @@ inductive Code where
 
 end
 
-@[inline]
-def FunDecl.fvarId : FunDecl → FVarId
-  | .mk (fvarId := fvarId) .. => fvarId
-
-@[inline]
-def FunDecl.binderName : FunDecl → Name
-  | .mk (binderName := binderName) .. => binderName
-
-@[inline]
-def FunDecl.params : FunDecl → Array Param
-  | .mk (params := params) .. => params
-
-@[inline]
-def FunDecl.type : FunDecl → Expr
-  | .mk (type := type) .. => type
-
-@[inline]
-def FunDecl.value : FunDecl → Code
-  | .mk (value := value) .. => value
-
-@[inline]
-def FunDecl.updateBinderName : FunDecl → Name → FunDecl
-  | .mk fvarId _ params type value, new =>
-    .mk fvarId new params type value
-
-@[inline]
-def FunDecl.toParam (decl : FunDecl) (borrow : Bool) : Param :=
-  match decl with
-  | .mk fvarId binderName _ type .. => ⟨fvarId, binderName, type, borrow⟩
-
-@[inline]
-def Cases.typeName : Cases → Name
-  | .mk (typeName := typeName) .. => typeName
-
-@[inline]
-def Cases.resultType : Cases → Expr
-  | .mk (resultType := resultType) .. => resultType
-
-@[inline]
-def Cases.discr : Cases → FVarId
-  | .mk (discr := discr) .. => discr
-
-@[inline]
-def Cases.alts : Cases → Array Alt
-  | .mk (alts := alts) .. => alts
-
-@[inline]
-def Cases.updateAlts : Cases → Array Alt → Cases
-  | .mk typeName resultType discr _, new =>
-    .mk typeName resultType discr new
-
 deriving instance Inhabited for Alt
 deriving instance Inhabited for FunDecl
 
@@ -325,18 +281,14 @@ private unsafe def updateAltImp (alt : Alt) (ps' : Array Param) (k' : Code) : Al
 
 @[inline] private unsafe def updateAltsImp (c : Code) (alts : Array Alt) : Code :=
   match c with
-  | .cases cs => if ptrEq cs.alts alts then c else .cases <| cs.updateAlts alts
+  | .cases cs => if ptrEq cs.alts alts then c else .cases { cs with alts }
   | _ => unreachable!
 
 @[implemented_by updateAltsImp] opaque Code.updateAlts! (c : Code) (alts : Array Alt) : Code
 
 @[inline] private unsafe def updateCasesImp (c : Code) (resultType : Expr) (discr : FVarId) (alts : Array Alt) : Code :=
   match c with
-  | .cases cs =>
-    if ptrEq cs.alts alts && ptrEq cs.resultType resultType && cs.discr == discr then
-      c
-    else
-      .cases <| ⟨cs.typeName, resultType, discr, alts⟩
+  | .cases cs => if ptrEq cs.alts alts && ptrEq cs.resultType resultType && cs.discr == discr then c else .cases { cs with discr, resultType, alts }
   | _ => unreachable!
 
 @[implemented_by updateCasesImp] opaque Code.updateCases! (c : Code) (resultType : Expr) (discr : FVarId) (alts : Array Alt) : Code
@@ -416,7 +368,7 @@ private unsafe def updateFunDeclCoreImp (decl: FunDecl) (type : Expr) (params :
   if ptrEq type decl.type && ptrEq params decl.params && ptrEq value decl.value then
     decl
   else
-    ⟨decl.fvarId, decl.binderName, params, type, value⟩
+    { decl with type, params, value }
 
 /--
 Low-level update `FunDecl` function. It does not update the local context.
@@ -426,7 +378,7 @@ to be updated.
 @[implemented_by updateFunDeclCoreImp] opaque FunDecl.updateCore (decl : FunDecl) (type : Expr) (params : Array Param) (value : Code) : FunDecl
 
 def Cases.extractAlt! (cases : Cases) (ctorName : Name) : Alt × Cases :=
-  let found i := (cases.alts[i]!, cases.updateAlts (cases.alts.eraseIdx! i))
+  let found i := (cases.alts[i], { cases with alts := cases.alts.eraseIdx i })
   if let some i := cases.alts.findFinIdx? fun | .alt ctorName' .. => ctorName == ctorName' | _ => false then
     found i
   else if let some i := cases.alts.findFinIdx? fun | .default _ => true | _ => false then

src/Lean/Compiler/LCNF/Bind.lean

@@ -48,7 +48,7 @@ where
       if alts.isEmpty then
         throwError "`Code.bind` failed, empty `cases` found"
       let resultType ← mkCasesResultType alts
-      return .cases ⟨c.typeName, resultType, c.discr, alts⟩
+      return .cases { c with alts, resultType }
     | .return fvarId => f fvarId
     | .jmp fvarId .. =>
       unless (← read).contains fvarId do

src/Lean/Compiler/LCNF/Closure.lean

@@ -137,7 +137,7 @@ mutual
         /- We only collect the variables in the scope of the function application being specialized. -/
         if let some funDecl ← findFunDecl? fvarId then
           if ctx.abstract funDecl.fvarId then
-            modify fun s => { s with params := s.params.push <| funDecl.toParam false }
+            modify fun s => { s with params := s.params.push <| { funDecl with borrow := false } }
           else
             collectFunDecl funDecl
             modify fun s => { s with decls := s.decls.push <| .fun funDecl }

src/Lean/Compiler/LCNF/CompilerM.lean

@@ -359,7 +359,7 @@ def mkLetDecl (binderName : Name) (type : Expr) (value : LetValue) : CompilerM L
 def mkFunDecl (binderName : Name) (type : Expr) (params : Array Param) (value : Code) : CompilerM FunDecl := do
   let fvarId ← mkFreshFVarId
   let binderName ← ensureNotAnonymous binderName `_f
-  let funDecl := ⟨fvarId, binderName, params, type, value⟩
+  let funDecl := { fvarId, binderName, type, params, value }
   modifyLCtx fun lctx => lctx.addFunDecl funDecl
   return funDecl
 
@@ -397,7 +397,7 @@ private unsafe def updateFunDeclImp (decl : FunDecl) (type : Expr) (params : Arr
   if ptrEq type decl.type && ptrEq params decl.params && ptrEq value decl.value then
     return decl
   else
-    let decl := ⟨decl.fvarId, decl.binderName, params, type, value⟩
+    let decl := { decl with type, params, value }
     modifyLCtx fun lctx => lctx.addFunDecl decl
     return decl
 

src/Lean/Compiler/LCNF/Internalize.lean

@@ -119,7 +119,7 @@ partial def internalizeFunDecl (decl : FunDecl) : InternalizeM FunDecl := do
   let params ← decl.params.mapM internalizeParam
   let value ← internalizeCode decl.value
   let fvarId ← mkNewFVarId decl.fvarId
-  let decl := ⟨fvarId, binderName, params, type, value⟩
+  let decl := { decl with binderName, fvarId, params, type, value }
   modifyLCtx fun lctx => lctx.addFunDecl decl
   return decl
 
@@ -139,7 +139,7 @@ partial def internalizeCode (code : Code) : InternalizeM Code := do
       let alts ← c.alts.mapM fun
         | .alt ctorName params k => return .alt ctorName (← params.mapM internalizeParam) (← internalizeAltCode k)
         | .default k => return .default (← internalizeAltCode k)
-      return .cases ⟨c.typeName, resultType, discr, alts⟩
+      return .cases { c with discr, alts, resultType }
 
 end
 

src/Lean/Compiler/LCNF/JoinPoints.lean

@@ -229,8 +229,10 @@ where
       | _, _ => return Code.updateLet! code decl (← go k)
     | .fun decl k =>
       if let some replacement := (← read)[decl.fvarId]? then
-        let newValue ← go decl.value
-        let newDecl := ⟨decl.fvarId, replacement, decl.params, decl.type, newValue⟩
+        let newDecl := { decl with
+          binderName := replacement,
+          value := (← go decl.value)
+        }
         modifyLCtx fun lctx => lctx.addFunDecl newDecl
         return .jp newDecl (← go k)
       else

src/Lean/Compiler/LCNF/Main.lean

@@ -4,14 +4,16 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
+
 prelude
 public import Lean.Compiler.Options
 public import Lean.Compiler.IR
 public import Lean.Compiler.LCNF.Passes
 public import Lean.Compiler.LCNF.ToDecl
 public import Lean.Compiler.LCNF.Check
-import Lean.Meta.Match.MatcherInfo
+
 public section
+
 namespace Lean.Compiler.LCNF
 /--
 We do not generate code for `declName` if

src/Lean/Compiler/LCNF/Renaming.lean

@@ -35,7 +35,7 @@ def LetDecl.applyRenaming (decl : LetDecl) (r : Renaming) : CompilerM LetDecl :=
 mutual
 partial def FunDecl.applyRenaming (decl : FunDecl) (r : Renaming) : CompilerM FunDecl := do
   if let some binderName := r.get? decl.fvarId then
-    let decl := decl.updateBinderName binderName
+    let decl := { decl with binderName }
     modifyLCtx fun lctx => lctx.addFunDecl decl
     decl.updateValue (← decl.value.applyRenaming r)
   else

src/Lean/Compiler/LCNF/Simp/JpCases.lean

@@ -268,7 +268,7 @@ where
         else
           altsNew := altsNew.push (alt.updateCode k)
     modify fun s => s.insert decl.fvarId jpAltMap
-    let value := LCNF.attachCodeDecls decls (.cases <| cases.updateAlts altsNew)
+    let value := LCNF.attachCodeDecls decls (.cases { cases with alts := altsNew })
     let decl ← decl.updateValue value
     let code := .jp decl (← visit k)
     return LCNF.attachCodeDecls jpAltDecls code

src/Lean/Compiler/LCNF/Specialize.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
+
 prelude
 public import Lean.Compiler.LCNF.SpecInfo
 public import Lean.Compiler.LCNF.MonadScope
@@ -12,7 +13,7 @@ import Lean.Compiler.LCNF.Simp
 import Lean.Compiler.LCNF.ToExpr
 import Lean.Compiler.LCNF.Level
 import Lean.Compiler.LCNF.Closure
-import Lean.Meta.Transform
+
 namespace Lean.Compiler.LCNF
 namespace Specialize
 
@@ -115,7 +116,7 @@ def isGround [TraverseFVar α] (e : α) : SpecializeM Bool := do
       match ← findFunDecl? fnFVarId with
       -- This ascription to `Bool` is required to avoid this being inferred as `Prop`,
       -- even with a type specified on the `let` binding.
-      | some (.mk (params := params) ..) => pure ((args.size < params.size) : Bool)
+      | some { params, .. } => pure ((args.size < params.size) : Bool)
       | none => pure false
     | _ => pure false
   let fvarId := decl.fvarId

src/Lean/Compiler/LCNF/StructProjCases.lean

@@ -72,7 +72,7 @@ partial def visitCode (code : Code) : M Code := do
         modify fun s => { s with projMap := s.projMap.erase base }
         let resultType ← toMonoType (← k.inferType)
         let alts := #[.alt ctorInfo.name params k]
-        return .cases ⟨typeName, resultType, base, alts⟩
+        return .cases { typeName, resultType, discr := base, alts }
     | _ => return code.updateLet! (← decl.updateValue (← visitLetValue decl.value)) (← visitCode k)
   | .fun decl k =>
     let decl ← decl.updateValue (← visitCode decl.value)

src/Lean/Compiler/LCNF/ToDecl.lean

@@ -4,12 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
+
 prelude
 public import Lean.Compiler.InitAttr
 public import Lean.Compiler.LCNF.ToLCNF
-import Lean.Meta.Transform
-import Lean.Meta.Match.MatcherInfo
+
 public section
+
 namespace Lean.Compiler.LCNF
 /--
 Inline constants tagged with the `[macro_inline]` attribute occurring in `e`.

src/Lean/Compiler/LCNF/ToLCNF.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
+
 prelude
 public import Lean.Meta.AppBuilder
 public import Lean.Compiler.CSimpAttr
@@ -11,8 +12,9 @@ public import Lean.Compiler.ImplementedByAttr
 public import Lean.Compiler.LCNF.Bind
 public import Lean.Compiler.NeverExtractAttr
 import Lean.Meta.CasesInfo
-import Lean.Meta.WHNF
+
 public section
+
 namespace Lean.Compiler.LCNF
 namespace ToLCNF
 
@@ -63,7 +65,7 @@ That is, our goal is to try to promote the pre join points `_alt.<idx>` into a p
 partial def bindCases (jpDecl : FunDecl) (cases : Cases) : CompilerM Code := do
   let (alts, s) ← visitAlts cases.alts |>.run {}
   let resultType ← mkCasesResultType alts
-  let result := .cases ⟨cases.typeName, resultType, cases.discr, alts⟩
+  let result := .cases { cases with alts, resultType }
   let result := s.foldl (init := result) fun result _ altJp => .jp altJp result
   return .jp jpDecl result
 where
@@ -147,7 +149,7 @@ where
       if alts.isEmpty then
         throwError "`Code.bind` failed, empty `cases` found"
       let resultType ← mkCasesResultType alts
-      return .cases ⟨c.typeName, resultType, c.discr, alts⟩
+      return .cases { c with alts, resultType }
     | .return fvarId => return .jmp jpDecl.fvarId #[.fvar fvarId]
     | .jmp .. | .unreach .. => return code
 
@@ -183,7 +185,7 @@ where
           result instead of a join point that takes a closure.
           -/
           eraseParam auxParam
-          let auxFunDecl := ⟨auxParam.fvarId, auxParam.binderName, #[], auxParam.type, .cases cases⟩
+          let auxFunDecl := { auxParam with params := #[], value := .cases cases : FunDecl }
           modifyLCtx fun lctx => lctx.addFunDecl auxFunDecl
           let auxFunDecl ← auxFunDecl.etaExpand
           go seq (i - 1) (.fun auxFunDecl c)
@@ -597,7 +599,7 @@ where
           let (altType, alt) ← visitAlt numParams args[i]!
           resultType := joinTypes altType resultType
           alts := alts.push alt
-        let cases := ⟨typeName, resultType, discrFVarId, alts⟩
+        let cases : Cases := { typeName, discr := discrFVarId, resultType, alts }
         let auxDecl ← mkAuxParam resultType
         pushElement (.cases auxDecl cases)
         let result := .fvar auxDecl.fvarId

src/Lean/Compiler/LCNF/ToMono.lean

@@ -205,7 +205,7 @@ partial def decToMono (c : Cases) (_ : c.typeName == ``Decidable) : ToMonoM Code
       eraseParams ps
       let ctorName := if ctorName == ``Decidable.isTrue then ``Bool.true else ``Bool.false
       return .alt ctorName #[] (← k.toMono)
-  return .cases ⟨``Bool, resultType, c.discr, alts⟩
+  return .cases { c with resultType, alts, typeName := ``Bool }
 
 /-- Eliminate `cases` for `Nat`. -/
 partial def casesNatToMono (c: Cases) (_ : c.typeName == ``Nat) : ToMonoM Code := do
@@ -226,7 +226,7 @@ partial def casesNatToMono (c: Cases) (_ : c.typeName == ``Nat) : ToMonoM Code :
         return .alt ``Bool.false #[] (.let oneDecl (.let subOneDecl (← k.toMono)))
       else
         return .alt ``Bool.true #[] (← k.toMono)
-  return .let zeroDecl (.let isZeroDecl (.cases ⟨``Bool, resultType, isZeroDecl.fvarId, alts⟩))
+  return .let zeroDecl (.let isZeroDecl (.cases { discr := isZeroDecl.fvarId, resultType, alts, typeName := ``Bool }))
 
 /-- Eliminate `cases` for `Int`. -/
 partial def casesIntToMono (c: Cases) (_ : c.typeName == ``Int) : ToMonoM Code := do
@@ -251,7 +251,7 @@ partial def casesIntToMono (c: Cases) (_ : c.typeName == ``Int) : ToMonoM Code :
         let absDecl := { fvarId := p.fvarId, binderName := p.binderName, type := natType, value := .const ``Int.natAbs [] #[.fvar c.discr] }
         modifyLCtx fun lctx => lctx.addLetDecl absDecl
         return .alt ``Bool.false #[] (.let absDecl (← k.toMono))
-  return .let zeroNatDecl (.let zeroIntDecl (.let isNegDecl (.cases ⟨``Bool, resultType, isNegDecl.fvarId, alts⟩)))
+  return .let zeroNatDecl (.let zeroIntDecl (.let isNegDecl (.cases { discr := isNegDecl.fvarId, resultType, alts, typeName := ``Bool })))
 
 /-- Eliminate `cases` for `UInt` types. -/
 partial def casesUIntToMono (c : Cases) (uintName : Name) (_ : c.typeName == uintName) : ToMonoM Code := do
@@ -317,13 +317,13 @@ partial def casesThunkToMono (c : Cases) (_ : c.typeName == ``Thunk) : ToMonoM C
   let letValue := .const ``Thunk.get [] #[.erased, .fvar c.discr]
   let letDecl ← mkLetDecl (← mkFreshBinderName `_x) anyExpr letValue
   let paramType := .const `PUnit []
-  let decl := ⟨
-    p.fvarId,
-    p.binderName,
-    #[← mkAuxParam paramType],
-    (← mkArrow paramType anyExpr),
-    .let letDecl (.return letDecl.fvarId)
-  ⟩
+  let decl := {
+    fvarId := p.fvarId
+    binderName := p.binderName
+    type := (← mkArrow paramType anyExpr)
+    params := #[← mkAuxParam paramType]
+    value := .let letDecl (.return letDecl.fvarId)
+  }
   modifyLCtx fun lctx => lctx.addFunDecl decl
   let k ← k.toMono
   return .fun decl k
@@ -418,7 +418,7 @@ partial def Code.toMono (code : Code) : ToMonoM Code := do
             let ps ← mkFieldParamsForComputedFields ctorInfo.type ctorInfo.numParams numNewFields ps
             let k ← k.toMono
             return .alt implCtorName ps k
-        return .cases ⟨typeName, resultType, c.discr, alts⟩
+        return .cases { discr := c.discr, resultType, typeName, alts }
       else
         let alts ← c.alts.mapM fun alt =>
           match alt with

src/Lean/Data/PersistentArray.lean

@@ -277,25 +277,9 @@ instance [Monad m] : ForIn m (PersistentArray α) α where
   | node cs => cs.forM (fun c => forMAux f c)
   | leaf vs => vs.forM f
 
-@[specialize] def forMFrom0 (t : PersistentArray α) (f : α → m PUnit) : m PUnit :=
+@[specialize] def forM (t : PersistentArray α) (f : α → m PUnit) : m PUnit :=
   forMAux f t.root *> t.tail.forM f
 
-@[specialize] private partial def forFromMAux (f : α → m PUnit) : PersistentArrayNode α → USize → USize → m PUnit
-  | node cs, i, shift => do
-    let j    := (div2Shift i shift).toNat
-    forFromMAux f cs[j]! (mod2Shift i shift) (shift - initShift)
-    cs.forM (start := j+1) (forMAux f)
-  | leaf vs, i, _ => vs.forM (start := i.toNat) f
-
-@[specialize] def forM (t : PersistentArray α) (f : α → m PUnit) (start : Nat := 0) : m PUnit := do
-  if start == 0 then
-    forMFrom0 t f
-  else if start >= t.tailOff then
-    t.tail.forM (start := start - t.tailOff) f
-  else do
-    forFromMAux f t.root (USize.ofNat start) t.shift
-    t.tail.forM f
-
 end
 
 @[inline] def foldl (t : PersistentArray α) (f : β → α → β) (init : β) (start : Nat := 0) : β :=

src/Lean/Data/PersistentHashMap.lean

@@ -193,28 +193,6 @@ partial def findEntryAux [BEq α] : Node α β → USize → α → Option (α
 def findEntry? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → Option (α × β)
   | { root }, k => findEntryAux root (hash k |>.toUSize) k
 
-partial def findKeyDAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k : α) (k₀ : α) : α :=
-  if h : i < keys.size then
-    let k' := keys[i]
-    if k == k' then k'
-    else findKeyDAtAux keys vals heq (i+1) k k₀
-  else k₀
-
-partial def findKeyDAux [BEq α] : Node α β → USize → α → α → α
-  | .entries entries, h, k, k₀ =>
-    let j     := (mod2Shift h shift).toNat
-    match entries[j]! with
-    | .null       => k₀
-    | .ref node   => findKeyDAux node (div2Shift h shift) k k₀
-    | .entry k' _ => if k == k' then k' else k₀
-  | .collision keys vals heq, _, k, k₀ => findKeyDAtAux keys vals heq 0 k k₀
-
-/--
-A more efficient `m.findEntry? a |>.map (·.1) |>.getD a₀`
--/
-@[inline] def findKeyD {_ : BEq α} {_ : Hashable α} (m : PersistentHashMap α β) (a : α) (a₀ : α) : α :=
-  findKeyDAux m.root (hash a |>.toUSize) a a₀
-
 partial def containsAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k : α) : Bool :=
   if h : i < keys.size then
     let k' := keys[i]

src/Lean/Data/PersistentHashSet.lean

@@ -45,9 +45,6 @@ variable {_ : BEq α} {_ : Hashable α}
   | some (a, _) => some a
   | none        => none
 
-@[inline] def findD (s : PersistentHashSet α) (a : α) (a₀ : α) : α :=
-  s.set.findKeyD a a₀
-
 @[inline] def contains (s : PersistentHashSet α) (a : α) : Bool :=
   s.set.contains a