feat: make tests smaller, add functions

localhost:8080 now is parsed as a scheme and a path, to work with the URI RFC and HTTP1.1 RFC

.github/workflows/actionlint.yml

@@ -15,7 +15,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
     - name: Checkout
-      uses: actions/checkout@v5
+      uses: actions/checkout@v6
     - 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@v5
+        uses: actions/checkout@v6
         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@v7
+        uses: namespacelabs/nscloud-checkout-action@v8
         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@v5
+        uses: actions/checkout@v6
         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@v5
+    - uses: actions/checkout@v6
       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@v5
+        uses: actions/checkout@v6
         # 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@6da8fa9354ddfdc4aeace5fc48d7f679b5214090
+        uses: softprops/action-gh-release@a06a81a03ee405af7f2048a818ed3f03bbf83c7b
         with:
           files: artifacts/*/*
           fail_on_unmatched_files: true
@@ -455,7 +455,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@v5
+        uses: actions/checkout@v6
         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@6da8fa9354ddfdc4aeace5fc48d7f679b5214090
+        uses: softprops/action-gh-release@a06a81a03ee405af7f2048a818ed3f03bbf83c7b
         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@v5
+    - uses: actions/checkout@v6
 
     - 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@6da8fa9354ddfdc4aeace5fc48d7f679b5214090
+        uses: softprops/action-gh-release@a06a81a03ee405af7f2048a818ed3f03bbf83c7b
         with:
           name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }}
           # There are coredumps files here as well, but all in deeper subdirectories.
@@ -86,7 +86,7 @@ jobs:
 
       - name: Release (SHA-suffixed format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: softprops/action-gh-release@6da8fa9354ddfdc4aeace5fc48d7f679b5214090
+        uses: softprops/action-gh-release@a06a81a03ee405af7f2048a818ed3f03bbf83c7b
         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@v5
+        uses: actions/checkout@v6
         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@v5
+        uses: actions/checkout@v6
         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@v5
+        uses: actions/checkout@v6
         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@v5
+    - uses: actions/checkout@v6
       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
-docstring is relevant to their task. The first (or only) sentence of
+constant 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,6 +1123,110 @@ 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,12 +338,14 @@ 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 (env : Environment) (i : ModuleIdx) :
-    Std.HashMap (ModuleIdx × NeedsKind) (Option (Name × Name)) := Id.run do
+def getExplanations (s : State) (i : ModuleIdx) : Explanations := Id.run do
+  let env := s.env
   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
@@ -364,18 +366,25 @@ def getExplanations (env : Environment) (i : ModuleIdx) :
 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 }
-          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)
+          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
       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 }
@@ -542,7 +551,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"
+          IO.eprintln s!"`{imp}` is needed{if needs.has k j then " (calculated)" else ""}"
         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
@@ -660,7 +669,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.env i
+    let explanation := getExplanations s 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!

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)
+  list(APPEND STDLIBS Lake LeanChecker)
 endif()
 
 add_custom_target(make_stdlib ALL
@@ -758,6 +758,12 @@ 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 a monadic counterpart to the short-circuiting `||` operator, usually accessed via the `<||>`
+This is 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 a monadic counterpart to the short-circuiting `&&` operator, usually accessed via the `<&&>`
+This is 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 describe's how to iterate over its elements. The monadic
+A collection's `ForIn` or `ForIn'` instance describes 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/DecidableEq.lean

@@ -125,6 +125,22 @@ 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/Iterators/Basic.lean

@@ -10,6 +10,7 @@ public import Init.Classical
 public import Init.Ext
 
 set_option doc.verso true
+set_option linter.missingDocs true
 
 public section
 
@@ -349,14 +350,24 @@ abbrev PlausibleIterStep.casesOn {IsPlausibleStep : IterStep α β → Prop}
 end IterStep
 
 /--
-The typeclass providing the step function of an iterator in `Iter (α := α) β` or
-`IterM (α := α) m β`.
+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
@@ -369,7 +380,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]
+@[deprecated IterM.mk (since := "2025-12-01"), inline, expose, inherit_doc IterM.mk]
 def Iterators.toIterM := @IterM.mk
 
 @[simp]
@@ -377,6 +388,7 @@ 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
 
@@ -459,8 +471,10 @@ 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
 
@@ -470,7 +484,9 @@ 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
 
@@ -595,8 +611,10 @@ 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
 
@@ -627,7 +645,9 @@ 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
 
@@ -701,6 +721,11 @@ 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 β
 
 /--
@@ -827,6 +852,11 @@ 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 β
 
 /--
@@ -930,6 +960,9 @@ 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
@@ -940,14 +973,13 @@ This structure provides a more convenient way to define `Finite α m` instances
 -/
 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`.
+  /--
+  A well-founded relation such that if `it'` is a successor iterator of `it`, then `Rel it' it`.
   -/
   Rel (it' it : IterM (α := α) m β) : Prop
-  /- A proof that `Rel` is well-founded. -/
+  /-- `Rel` is well-founded. -/
   wf : WellFounded Rel
-  /- A proof that if `it'` is a successor iterator of `it`, then `Rel it' it`. -/
+  /-- 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
@@ -967,14 +999,13 @@ This structure provides a more convenient way to define `Productive α m` instan
 -/
 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`.
+  /--
+  A well-founded relation such that if `it'` is obtained from `it` by skipping, then `Rel it' it`.
   -/
   Rel : (IterM (α := α) m β) → (IterM (α := α) m β) → Prop
-  /- A proof that `Rel` is well-founded. -/
+  /-- `Rel` is well-founded. -/
   wf : WellFounded Rel
-  /- A proof that if `it'` is obtained from `it` by skipping, then `Rel it' it`. -/
+  /-- 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

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

@@ -9,6 +9,8 @@ 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,6 +8,8 @@ module
 prelude
 public import Init.Data.Iterators.Basic
 
+set_option linter.missingDocs true
+
 public section
 
 namespace Std
@@ -57,8 +59,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
@@ -68,6 +70,11 @@ 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,6 +11,8 @@ 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,6 +11,8 @@ 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
 
 /-!
@@ -70,6 +72,9 @@ 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 β) → γ →
@@ -82,7 +87,9 @@ 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
@@ -163,6 +170,7 @@ 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))) :
@@ -219,6 +227,7 @@ 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] :
@@ -226,6 +235,7 @@ 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,6 +8,8 @@ module
 prelude
 public import Init.Data.Iterators.Basic
 
+set_option linter.missingDocs true
+
 public section
 
 namespace Std
@@ -16,6 +18,9 @@ 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,12 +9,19 @@ 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,6 +8,8 @@ module
 prelude
 public import Init.Data.Iterators.Basic
 
+set_option linter.missingDocs true
+
 public section
 
 namespace Std
@@ -16,6 +18,9 @@ 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,6 +9,8 @@ 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,12 +9,19 @@ 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/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 a function `PostconditionT m α → PostconditionT m β`,
+Given a function `f : α → β`, returns 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 a function
+Given a function `α → PostconditionT m β`, returns a function
 `PostconditionT m α → PostconditionT m β`, turning `PostconditionT m` into a monad.
 -/
 @[always_inline, inline, expose]

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 that `a == b` implies
+The `BEq α` and `Hashable α` instances on `α` are compatible. This means that `a == b` implies
 `hash a = hash b`.
 
 This is automatic if the `BEq` instance is lawful.

src/Init/Data/List/Basic.lean

@@ -717,6 +717,7 @@ 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
 
 
@@ -730,6 +731,7 @@ 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 a non-tail-recursive variant that may be
+This implementation is tail recursive. `List.mapM'` is 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 a non-tail-recursive variant that may
+This implementation is tail recursive. `List.zipWithM'` is a non-tail-recursive variant that may
 be more convenient to reason about.
 -/
 @[inline, expose]

src/Init/Data/List/Lemmas.lean

@@ -2941,9 +2941,6 @@ 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/Nat/Bitwise/Lemmas.lean

@@ -223,6 +223,16 @@ 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
@@ -231,6 +241,10 @@ 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/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
+public import Init.Data.Nat.Power2.Basic
 public import Init.Data.Nat.Mod
 import Init.TacticsExtra
 import Init.BinderPredicates

src/Init/Data/Nat/Power2.lean

@@ -6,66 +6,5 @@ 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
+public import Init.Data.Nat.Power2.Basic
+public import Init.Data.Nat.Power2.Lemmas

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

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

@@ -0,0 +1,62 @@
+/-
+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 typeclasses for ordered types for which `compare a a = .eq` for all `a`. -/
+/-- A typeclass 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/UpwardEnumerable.lean

@@ -246,8 +246,12 @@ 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/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 resulting the slices is {lit}`γ`.
+The type of the resulting slices is {lit}`γ`.
 -/
 class Rco.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
   /--

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

@@ -57,4 +57,10 @@ 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] def toLower (s : String) : String :=
+@[inline, expose] def toLower (s : String) : String :=
   s.map Char.toLower
 
 /--

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

@@ -119,7 +119,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 from `stackPos - needlePos` to `stackPos` (exclusive) is a
+      -- **Invariant 3:** the range from `stackPos - needlePos` to `stackPos` (exclusive) is a
       -- prefix of the pattern.
       if h₁ : stackPos < s.rawEndPos then
         let stackByte := s.getUTF8Byte stackPos h₁

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 occurence of a pattern. Currently the supported patterns are:
+  first occurrence 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

src/Init/Grind/Config.lean

@@ -21,6 +21,8 @@ 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 (generalizing := false) a with
+          a) = match a with
             | num n => Poly.num (n ^ k)
             | .intCast n => .num (n^k)
             | .natCast n => .num (n^k)

src/Init/MetaTypes.lean

@@ -132,6 +132,11 @@ 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
@@ -297,6 +302,11 @@ 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 the same as `f x`,
+Haskell-like pipe operator `<|`. `f <| x` means 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 the same as `f x`,
+Alternative syntax for `<|`. `f $ x` means 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,9 +782,16 @@ 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
+  guardMsgsFilter <|> guardMsgsWhitespace <|> guardMsgsOrdering <|> guardMsgsPositions <|> guardMsgsSubstring
 
 set_option linter.missingDocs false in
 syntax guardMsgsSpec := "(" guardMsgsSpecElt,* ")"
@@ -860,6 +867,11 @@ 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.
 
@@ -873,6 +885,13 @@ 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 "-") <|> "⊢") unifConstraint : command
+  " where " withPosition(unifConstraintElem*) patternIgnore(atomic("|" noWs "-") <|> "⊢") ppSpace 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

@@ -907,7 +907,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 who's type may live in `Sort s`.
+`PLift` that allows lifting values whose 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 +3525,7 @@ instance : DecidableEq String.Pos.Raw :=
 /--
 A region or slice of some underlying string.
 
-A substring contains an string together with the start and end byte positions of a region of
+A substring contains a 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,6 +38,12 @@ 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 return its result.
+Waits until any of the tasks in the list has finished, then returns 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 the where reads and writes occur in the
+Handles have an associated read/write cursor that determines 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 a exclusive lock while already possessing a shared lock will **not** reliably succeed: it
+Acquiring an 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 a exclusive lock while already possessing a shared lock will **not** reliably succeed: it
+Acquiring an 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 a its path to an `IO`
+Creates a temporary directory in the most secure manner possible, providing 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 return its exit code.
+Blocks until the child process has exited and returns 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 it's designated
+The `FileRight` structure describes these permissions for a file's owner, members of its 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` any any object reachable from it never being
+Discards the passed owned reference. This leads to `a` and 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/Try.lean

@@ -58,6 +58,9 @@ 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` evalutes to a ground term. -/
+/-- Helper gadget that prevents reduction of `Nat.eager n` unless `n` evaluates 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 to `WellFounded.fix`, this fixpoint operator reduces on closed terms. (More precisely:
-when `h x` evalutes to a ground value)
+In contrast to `WellFounded.fix`, this fixpoint operator reduces on closed terms. (More precisely:
+when `h x` evaluates to a ground value)
 
 -/
 def Nat.fix : (x : α) → motive x :=

src/Lean/Compiler/LCNF/Basic.lean

@@ -147,18 +147,11 @@ inductive Alt where
   | alt (ctorName : Name) (params : Array Param) (code : Code)
   | default (code : Code)
 
-structure FunDecl where
-  fvarId : FVarId
-  binderName : Name
-  params : Array Param
-  type : Expr
-  value : Code
+inductive FunDecl where
+  | mk (fvarId : FVarId) (binderName : Name) (params : Array Param) (type : Expr) (value : Code)
 
-structure Cases where
-  typeName : Name
-  resultType : Expr
-  discr : FVarId
-  alts : Array Alt
+inductive Cases where
+  | mk (typeName : Name) (resultType : Expr) (discr : FVarId) (alts : Array Alt)
   deriving Inhabited
 
 inductive Code where
@@ -173,6 +166,57 @@ 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
 
@@ -281,14 +325,18 @@ 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 with alts }
+  | .cases cs => if ptrEq cs.alts alts then c else .cases <| cs.updateAlts 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 with discr, resultType, alts }
+  | .cases cs =>
+    if ptrEq cs.alts alts && ptrEq cs.resultType resultType && cs.discr == discr then
+      c
+    else
+      .cases <| ⟨cs.typeName, resultType, discr, alts⟩
   | _ => unreachable!
 
 @[implemented_by updateCasesImp] opaque Code.updateCases! (c : Code) (resultType : Expr) (discr : FVarId) (alts : Array Alt) : Code
@@ -368,7 +416,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 with type, params, value }
+    ⟨decl.fvarId, decl.binderName, params, type, value⟩
 
 /--
 Low-level update `FunDecl` function. It does not update the local context.
@@ -378,7 +426,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 with alts := cases.alts.eraseIdx i })
+  let found i := (cases.alts[i]!, cases.updateAlts (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 with alts, resultType }
+      return .cases ⟨c.typeName, resultType, c.discr, alts⟩
     | .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 with borrow := false } }
+            modify fun s => { s with params := s.params.push <| funDecl.toParam 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, type, params, value }
+  let funDecl := ⟨fvarId, binderName, params, type, 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 with type, params, value }
+    let decl := ⟨decl.fvarId, decl.binderName, params, type, 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 := { decl with binderName, fvarId, params, type, value }
+  let decl := ⟨fvarId, binderName, 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 with discr, alts, resultType }
+      return .cases ⟨c.typeName, resultType, discr, alts⟩
 
 end
 

src/Lean/Compiler/LCNF/JoinPoints.lean

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

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 with binderName }
+    let decl := decl.updateBinderName 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 with alts := altsNew })
+    let value := LCNF.attachCodeDecls decls (.cases <| cases.updateAlts altsNew)
     let decl ← decl.updateValue value
     let code := .jp decl (← visit k)
     return LCNF.attachCodeDecls jpAltDecls code

src/Lean/Compiler/LCNF/Specialize.lean

@@ -115,7 +115,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 { params, .. } => pure ((args.size < params.size) : Bool)
+      | some (.mk (params := 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, discr := base, alts }
+        return .cases ⟨typeName, resultType, 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/ToLCNF.lean

@@ -63,7 +63,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 with alts, resultType }
+  let result := .cases ⟨cases.typeName, resultType, cases.discr, alts⟩
   let result := s.foldl (init := result) fun result _ altJp => .jp altJp result
   return .jp jpDecl result
 where
@@ -147,7 +147,7 @@ where
       if alts.isEmpty then
         throwError "`Code.bind` failed, empty `cases` found"
       let resultType ← mkCasesResultType alts
-      return .cases { c with alts, resultType }
+      return .cases ⟨c.typeName, resultType, c.discr, alts⟩
     | .return fvarId => return .jmp jpDecl.fvarId #[.fvar fvarId]
     | .jmp .. | .unreach .. => return code
 
@@ -183,7 +183,7 @@ where
           result instead of a join point that takes a closure.
           -/
           eraseParam auxParam
-          let auxFunDecl := { auxParam with params := #[], value := .cases cases : FunDecl }
+          let auxFunDecl := ⟨auxParam.fvarId, auxParam.binderName, #[], auxParam.type, .cases cases⟩
           modifyLCtx fun lctx => lctx.addFunDecl auxFunDecl
           let auxFunDecl ← auxFunDecl.etaExpand
           go seq (i - 1) (.fun auxFunDecl c)
@@ -597,7 +597,7 @@ where
           let (altType, alt) ← visitAlt numParams args[i]!
           resultType := joinTypes altType resultType
           alts := alts.push alt
-        let cases : Cases := { typeName, discr := discrFVarId, resultType, alts }
+        let cases := ⟨typeName, resultType, discrFVarId, 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 { c with resultType, alts, typeName := ``Bool }
+  return .cases ⟨``Bool, resultType, c.discr, alts⟩
 
 /-- 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 { discr := isZeroDecl.fvarId, resultType, alts, typeName := ``Bool }))
+  return .let zeroDecl (.let isZeroDecl (.cases ⟨``Bool, resultType, isZeroDecl.fvarId, alts⟩))
 
 /-- 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 { discr := isNegDecl.fvarId, resultType, alts, typeName := ``Bool })))
+  return .let zeroNatDecl (.let zeroIntDecl (.let isNegDecl (.cases ⟨``Bool, resultType, isNegDecl.fvarId, alts⟩)))
 
 /-- 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 := {
-    fvarId := p.fvarId
-    binderName := p.binderName
-    type := (← mkArrow paramType anyExpr)
-    params := #[← mkAuxParam paramType]
-    value := .let letDecl (.return letDecl.fvarId)
-  }
+  let decl := ⟨
+    p.fvarId,
+    p.binderName,
+    #[← mkAuxParam paramType],
+    (← mkArrow paramType anyExpr),
+    .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 { discr := c.discr, resultType, typeName, alts }
+        return .cases ⟨typeName, resultType, c.discr, alts⟩
       else
         let alts ← c.alts.mapM fun alt =>
           match alt with

src/Lean/Elab/Attributes.lean

@@ -45,26 +45,29 @@ def toAttributeKind (attrKindStx : Syntax) : MacroM AttributeKind := do
 def mkAttrKindGlobal : Syntax :=
   mkNode ``Lean.Parser.Term.attrKind #[mkNullNode]
 
-def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLiftT IO m] (attrInstance : Syntax) : m Attribute := do
-  /- attrInstance     := ppGroup $ leading_parser attrKind >> attrParser -/
-  let attrKind ← liftMacroM <| toAttributeKind attrInstance[0]
-  let attr := attrInstance[1]
-  let attr ← liftMacroM <| expandMacros attr
-  let attrName ← if attr.getKind == ``Parser.Attr.simple then
-    pure attr[0].getId.eraseMacroScopes
-  else match attr.getKind with
-    | .str _ s => pure <| Name.mkSimple s
-    | _ => throwErrorAt attr  "Unknown attribute"
-  let .ok _impl := getAttributeImpl (← getEnv) attrName
-    | throwError "Unknown attribute `[{attrName}]`"
-  if let .ok impl := getAttributeImpl (← getEnv) attrName then
-    if regularInitAttr.getParam? (← getEnv) impl.ref |>.isSome then  -- skip `builtin_initialize` attributes
-      recordExtraModUseFromDecl (isMeta := true) impl.ref
-  /- The `AttrM` does not have sufficient information for expanding macros in `args`.
-     So, we expand them before here before we invoke the attributer handlers implemented using `AttrM`. -/
-  return { kind := attrKind, name := attrName, stx := attr }
+def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLiftT IO m] [MonadFinally m] (attrInstance : Syntax) : m Attribute := do
+  -- Resolving the attribute itself can be done in the private scope; running the attribute handler
+  -- will later be done in a scope determined by `applyAttributesCore`.
+  withoutExporting do
+    /- attrInstance     := ppGroup $ leading_parser attrKind >> attrParser -/
+    let attrKind ← liftMacroM <| toAttributeKind attrInstance[0]
+    let attr := attrInstance[1]
+    let attr ← liftMacroM <| expandMacros attr
+    let attrName ← if attr.getKind == ``Parser.Attr.simple then
+      pure attr[0].getId.eraseMacroScopes
+    else match attr.getKind with
+      | .str _ s => pure <| Name.mkSimple s
+      | _ => throwErrorAt attr  "Unknown attribute"
+    let .ok _impl := getAttributeImpl (← getEnv) attrName
+      | throwError "Unknown attribute `[{attrName}]`"
+    if let .ok impl := getAttributeImpl (← getEnv) attrName then
+      if regularInitAttr.getParam? (← getEnv) impl.ref |>.isSome then  -- skip `builtin_initialize` attributes
+        recordExtraModUseFromDecl (isMeta := true) impl.ref
+    /- The `AttrM` does not have sufficient information for expanding macros in `args`.
+      So, we expand them before here before we invoke the attributer handlers implemented using `AttrM`. -/
+    return { kind := attrKind, name := attrName, stx := attr }
 
-def elabAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadLiftT IO m] (attrInstances : Array Syntax) : m (Array Attribute) := do
+def elabAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadLiftT IO m] [MonadFinally m] (attrInstances : Array Syntax) : m (Array Attribute) := do
   let mut attrs := #[]
   for attr in attrInstances do
     try
@@ -74,7 +77,7 @@ def elabAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadM
   return attrs
 
 -- leading_parser "@[" >> sepBy1 attrInstance ", " >> "]"
-def elabDeclAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadLiftT IO m] (stx : Syntax) : m (Array Attribute) :=
+def elabDeclAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadLiftT IO m] [MonadFinally m] (stx : Syntax) : m (Array Attribute) :=
   elabAttrs stx[1].getSepArgs
 
 end Lean.Elab

src/Lean/Elab/Extra.lean

@@ -573,11 +573,16 @@ def elabDefaultOrNonempty : TermElab :=  fun stx expectedType? => do
   | some expectedType =>
     try
       mkDefault expectedType
-    catch ex => try
+    catch _ => try
       mkOfNonempty expectedType
     catch _ =>
       if stx[1].isNone then
-        throw ex
+        throwError "\
+          failed to synthesize '{.ofConstName ``Inhabited}' or '{.ofConstName ``Nonempty}' instance for\
+          {indentExpr expectedType}\n\
+          \n\
+          If this type is defined using the 'structure' or 'inductive' command, \
+          you can try adding a 'deriving Nonempty' clause to it."
       else
         -- It is in the context of an `unsafe` constant. We can use sorry instead.
         -- Another option is to make a recursive application since it is unsafe.

src/Lean/Elab/GuardMsgs.lean

@@ -11,10 +11,13 @@ public import Lean.Server.CodeActions.Attr
 
 public section
 
-/-! `#guard_msgs` command for testing commands
+/-! `#guard_msgs` and `#guard_panic` commands for testing commands
 
-This module defines a command to test that another command produces the expected messages.
-See the docstring on the `#guard_msgs` command.
+This module defines commands to test that other commands produce expected messages:
+- `#guard_msgs`: tests that a command produces exactly the expected messages
+- `#guard_panic`: tests that a command produces a panic message (without checking the exact text)
+
+See the docstrings on the individual commands.
 -/
 
 open Lean Parser.Tactic Elab Command
@@ -88,6 +91,8 @@ structure GuardMsgsSpec where
   ordering : MessageOrdering := .exact
   /-- Whether to report position information. -/
   reportPositions : Bool := false
+  /-- Whether to check for substring containment instead of exact match. -/
+  substring : Bool := false
 
 def parseGuardMsgsFilterAction (action? : Option (TSyntax ``guardMsgsFilterAction)) :
     CommandElabM FilterSpec := do
@@ -118,7 +123,7 @@ def parseGuardMsgsSpec (spec? : Option (TSyntax ``guardMsgsSpec)) : CommandElabM
     | `(guardMsgsSpec| ($[$elts:guardMsgsSpecElt],*)) => pure elts
     | _ => throwUnsupportedSyntax
   let defaultFilterFn := cfg.filterFn
-  let mut { whitespace, ordering, reportPositions .. } := cfg
+  let mut { whitespace, ordering, reportPositions, substring .. } := cfg
   let mut p? : Option (Message → FilterSpec) := none
   let pushP (action : FilterSpec) (msgP : Message → Bool) (p? : Option (Message → FilterSpec))
       (msg : Message) : FilterSpec :=
@@ -136,9 +141,11 @@ def parseGuardMsgsSpec (spec? : Option (TSyntax ``guardMsgsSpec)) : CommandElabM
     | `(guardMsgsSpecElt| ordering := sorted)       => ordering := .sorted
     | `(guardMsgsSpecElt| positions := true)        => reportPositions := true
     | `(guardMsgsSpecElt| positions := false)       => reportPositions := false
+    | `(guardMsgsSpecElt| substring := true)        => substring := true
+    | `(guardMsgsSpecElt| substring := false)       => substring := false
     | _ => throwUnsupportedSyntax
   let filterFn := p?.getD defaultFilterFn
-  return { filterFn, whitespace, ordering, reportPositions }
+  return { filterFn, whitespace, ordering, reportPositions, substring }
 
 /-- An info tree node corresponding to a failed `#guard_msgs` invocation,
 used for code action support. -/
@@ -176,22 +183,31 @@ def MessageOrdering.apply (mode : MessageOrdering) (msgs : List String) : List S
   | .exact => msgs
   | .sorted => msgs |>.toArray.qsort (· < ·) |>.toList
 
+/--
+Runs a command and collects all messages (sync and async) it produces.
+Clears the snapshot tasks after collection.
+Returns the collected messages.
+-/
+def runAndCollectMessages (cmd : Syntax) : CommandElabM MessageLog := do
+  -- do not forward snapshot as we don't want messages assigned to it to leak outside
+  withReader ({ · with snap? := none }) do
+    -- The `#guard_msgs` command is special-cased in `elabCommandTopLevel` to ensure linters only run once.
+    elabCommandTopLevel cmd
+  -- collect sync and async messages
+  let msgs := (← get).messages ++
+    (← get).snapshotTasks.foldl (· ++ ·.get.getAll.foldl (· ++ ·.diagnostics.msgLog) .empty) .empty
+  -- clear async messages as we don't want them to leak outside
+  modify ({ · with snapshotTasks := #[] })
+  return msgs
+
 @[builtin_command_elab Lean.guardMsgsCmd] def elabGuardMsgs : CommandElab
   | `(command| $[$dc?:docComment]? #guard_msgs%$tk $(spec?)? in $cmd) => do
     let expected : String := (← dc?.mapM (getDocStringText ·)).getD ""
         |>.trimAscii |>.copy |> removeTrailingWhitespaceMarker
-    let { whitespace, ordering, filterFn, reportPositions } ← parseGuardMsgsSpec spec?
-    -- do not forward snapshot as we don't want messages assigned to it to leak outside
-    withReader ({ · with snap? := none }) do
-      -- The `#guard_msgs` command is special-cased in `elabCommandTopLevel` to ensure linters only run once.
-      elabCommandTopLevel cmd
-    -- collect sync and async messages
-    let msgs := (← get).messages ++
-      (← get).snapshotTasks.foldl (· ++ ·.get.getAll.foldl (· ++ ·.diagnostics.msgLog) {}) {}
-    -- clear async messages as we don't want them to leak outside
-    modify ({ · with snapshotTasks := #[] })
-    let mut toCheck : MessageLog := .empty
-    let mut toPassthrough : MessageLog := .empty
+    let { whitespace, ordering, filterFn, reportPositions, substring } ← parseGuardMsgsSpec spec?
+    let msgs ← runAndCollectMessages cmd
+    let mut toCheck : MessageLog := MessageLog.empty
+    let mut toPassthrough : MessageLog := MessageLog.empty
     for msg in msgs.toList do
       if msg.isSilent then
         continue
@@ -207,7 +223,13 @@ def MessageOrdering.apply (mode : MessageOrdering) (msgs : List String) : List S
     let strings ← toCheck.toList.mapM (messageToString · reportPos?)
     let strings := ordering.apply strings
     let res := "---\n".intercalate strings |>.trimAscii |>.copy
-    if whitespace.apply expected == whitespace.apply res then
+    let passed := if substring then
+      -- Substring mode: check that expected appears within res (after whitespace normalization)
+      (whitespace.apply res).contains (whitespace.apply expected)
+    else
+      -- Exact mode: check equality (after whitespace normalization)
+      whitespace.apply expected == whitespace.apply res
+    if passed then
       -- Passed. Only put toPassthrough messages back on the message log
       modify fun st => { st with messages := toPassthrough }
     else
@@ -257,4 +279,24 @@ def guardMsgsCodeAction : CommandCodeAction := fun _ _ _ node => do
       }
   }]
 
+@[builtin_command_elab Lean.guardPanicCmd] def elabGuardPanic : CommandElab
+  | `(command| #guard_panic in $cmd) => do
+    let msgs ← runAndCollectMessages cmd
+    -- Check if any message contains "PANIC"
+    let mut foundPanic := false
+    for msg in msgs.toList do
+      if msg.isSilent then continue
+      let msgStr ← msg.data.toString
+      if msgStr.contains "PANIC" then
+        foundPanic := true
+        break
+    if foundPanic then
+      -- Success - clear the messages so they don't appear
+      modify fun st => { st with messages := MessageLog.empty }
+    else
+      -- Failed - put the messages back and add our error
+      modify fun st => { st with messages := msgs }
+      logError "Expected a PANIC but none was found"
+  | _ => throwUnsupportedSyntax
+
 end Lean.Elab.Tactic.GuardMsgs

src/Lean/Elab/Inductive.lean

@@ -29,72 +29,76 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) (isCoi
   let (binders, type?) := expandOptDeclSig decl[2]
   let declId           := decl[1]
   let ⟨name, declName, levelNames, docString?⟩ ← Term.expandDeclId (← getCurrNamespace) (← Term.getLevelNames) declId modifiers
-  if modifiers.isMeta then
-    modifyEnv (markMeta · declName)
-  addDeclarationRangesForBuiltin declName modifiers.stx decl
-  /-
-    Relates to issue
-    https://github.com/leanprover/lean4/issues/10503
-  -/
-  if declName.hasMacroScopes && isCoinductive then
-    throwError "Coinductive predicates are not allowed inside of macro scopes"
-  let ctors      ← decl[4].getArgs.mapM fun ctor => withRef ctor do
-    /-
-    ```
-    def ctor := leading_parser optional docComment >> "\n| " >> declModifiers >> rawIdent >> optDeclSig
-    ```
-    -/
-    let modifiersStx := ctor[2]
-    let mut ctorModifiers ← elabModifiers ⟨modifiersStx⟩
-    if let some leadingDocComment := ctor[0].getOptional? then
-      if ctorModifiers.docString?.isSome then
-        logErrorAt leadingDocComment "Duplicate doc string"
-      ctorModifiers := { ctorModifiers with
-        docString? := some (⟨leadingDocComment⟩, doc.verso.get (← getOptions)) }
-    if ctorModifiers.isPrivate && modifiers.isPrivate then
-      let hint ← do
-        let .original .. := modifiersStx.getHeadInfo | pure .nil
-        let some range := modifiersStx[2].getRangeWithTrailing? | pure .nil
-        -- Drop the doc comment from both the `declModifiers` and outer `ctor`, as well as
-        -- everything after the constructor name (yielding invalid syntax with the desired range)
-        let previewSpan? := ctor.modifyArgs (·[2...4].toArray.modify 0 (·.modifyArgs (·[1...*])))
-        MessageData.hint "Remove `private` modifier from constructor" #[{
-          suggestion := ""
-          span? := Syntax.ofRange range
-          previewSpan?
-          toCodeActionTitle? := some fun _ => "Delete `private` modifier"
-        }]
-      throwError m!"Constructor cannot be marked `private` because it is already in a `private` inductive datatype" ++ hint
-    if ctorModifiers.isProtected && modifiers.isPrivate then
-      throwError "Constructor cannot be `protected` because it is in a `private` inductive datatype"
-    checkValidCtorModifier ctorModifiers
-    let ctorName := ctor.getIdAt 3
-    let ctorName := declName ++ ctorName
-    let ctorName ← withRef ctor[3] <| applyVisibility ctorModifiers ctorName
-    let (binders, type?) := expandOptDeclSig ctor[4]
-    addDeclarationRangesFromSyntax ctorName ctor ctor[3]
+  -- In the case of mutual inductives, this is the earliests point where we can establish the
+  -- correct scope for each individual inductive declaration (used e.g. to infer ctor visibility
+  -- below), so let's do that now.
+  withExporting (isExporting := !isPrivateName declName) do
     if modifiers.isMeta then
-      modifyEnv (markMeta · ctorName)
-    return { ref := ctor, declId := ctor[3], modifiers := ctorModifiers, declName := ctorName, binders := binders, type? := type? : CtorView }
-  let computedFields ← (decl[5].getOptional?.map (·[1].getArgs) |>.getD #[]).mapM fun cf => withRef cf do
-    return { ref := cf, modifiers := cf[0], fieldId := cf[1].getId, type := ⟨cf[3]⟩, matchAlts := ⟨cf[4]⟩ }
-  let classes ← getOptDerivingClasses decl[6]
-  if decl[3][0].isToken ":=" then
-    -- https://github.com/leanprover/lean4/issues/5236
-    withRef decl[0] <| Linter.logLintIf Linter.linter.deprecated decl[3]
-      "`inductive ... :=` has been deprecated in favor of `inductive ... where`"
-  return {
-    ref             := decl
-    shortDeclName   := name
-    derivingClasses := classes
-    allowIndices    := true
-    allowSortPolymorphism := true
-    declId, modifiers, isClass, declName, levelNames
-    binders, type?, ctors
-    computedFields
-    docString?
-    isCoinductive := isCoinductive
-  }
+      modifyEnv (markMeta · declName)
+    addDeclarationRangesForBuiltin declName modifiers.stx decl
+    /-
+      Relates to issue
+      https://github.com/leanprover/lean4/issues/10503
+    -/
+    if declName.hasMacroScopes && isCoinductive then
+      throwError "Coinductive predicates are not allowed inside of macro scopes"
+    let ctors      ← decl[4].getArgs.mapM fun ctor => withRef ctor do
+      /-
+      ```
+      def ctor := leading_parser optional docComment >> "\n| " >> declModifiers >> rawIdent >> optDeclSig
+      ```
+      -/
+      let modifiersStx := ctor[2]
+      let mut ctorModifiers ← elabModifiers ⟨modifiersStx⟩
+      if let some leadingDocComment := ctor[0].getOptional? then
+        if ctorModifiers.docString?.isSome then
+          logErrorAt leadingDocComment "Duplicate doc string"
+        ctorModifiers := { ctorModifiers with
+          docString? := some (⟨leadingDocComment⟩, doc.verso.get (← getOptions)) }
+      if ctorModifiers.isPrivate && modifiers.isPrivate then
+        let hint ← do
+          let .original .. := modifiersStx.getHeadInfo | pure .nil
+          let some range := modifiersStx[2].getRangeWithTrailing? | pure .nil
+          -- Drop the doc comment from both the `declModifiers` and outer `ctor`, as well as
+          -- everything after the constructor name (yielding invalid syntax with the desired range)
+          let previewSpan? := ctor.modifyArgs (·[2...4].toArray.modify 0 (·.modifyArgs (·[1...*])))
+          MessageData.hint "Remove `private` modifier from constructor" #[{
+            suggestion := ""
+            span? := Syntax.ofRange range
+            previewSpan?
+            toCodeActionTitle? := some fun _ => "Delete `private` modifier"
+          }]
+        throwError m!"Constructor cannot be marked `private` because it is already in a `private` inductive datatype" ++ hint
+      if ctorModifiers.isProtected && modifiers.isPrivate then
+        throwError "Constructor cannot be `protected` because it is in a `private` inductive datatype"
+      checkValidCtorModifier ctorModifiers
+      let ctorName := ctor.getIdAt 3
+      let ctorName := declName ++ ctorName
+      let ctorName ← withRef ctor[3] <| applyVisibility ctorModifiers ctorName
+      let (binders, type?) := expandOptDeclSig ctor[4]
+      addDeclarationRangesFromSyntax ctorName ctor ctor[3]
+      if modifiers.isMeta then
+        modifyEnv (markMeta · ctorName)
+      return { ref := ctor, declId := ctor[3], modifiers := ctorModifiers, declName := ctorName, binders := binders, type? := type? : CtorView }
+    let computedFields ← (decl[5].getOptional?.map (·[1].getArgs) |>.getD #[]).mapM fun cf => withRef cf do
+      return { ref := cf, modifiers := cf[0], fieldId := cf[1].getId, type := ⟨cf[3]⟩, matchAlts := ⟨cf[4]⟩ }
+    let classes ← getOptDerivingClasses decl[6]
+    if decl[3][0].isToken ":=" then
+      -- https://github.com/leanprover/lean4/issues/5236
+      withRef decl[0] <| Linter.logLintIf Linter.linter.deprecated decl[3]
+        "`inductive ... :=` has been deprecated in favor of `inductive ... where`"
+    return {
+      ref             := decl
+      shortDeclName   := name
+      derivingClasses := classes
+      allowIndices    := true
+      allowSortPolymorphism := true
+      declId, modifiers, isClass, declName, levelNames
+      binders, type?, ctors
+      computedFields
+      docString?
+      isCoinductive := isCoinductive
+    }
 
 private def isInductiveFamily (numParams : Nat) (indFVar : Expr) : TermElabM Bool := do
   let indFVarType ← inferType indFVar

src/Lean/Elab/Match.lean

@@ -886,7 +886,7 @@ private def generalize (discrs : Array Discr) (matchType : Expr) (altViews : Arr
       let matchType' ← forallBoundedTelescope matchType discrs.size fun ds type => do
         let type ← mkForallFVars ys type
         let (discrs', ds') := Array.unzip <| Array.zip discrExprs ds |>.filter fun (di, _) => di.isFVar
-        let type ← type.replaceFVarsM discrs' ds'
+        let type := type.replaceFVars discrs' ds'
         mkForallFVars ds type
       if (← isTypeCorrect matchType') then
         let discrs := discrs ++  ys.map fun y => { expr := y : Discr }
@@ -1119,11 +1119,11 @@ private def elabMatchAux (generalizing? : Option Bool) (discrStxs : Array Syntax
       withRef altLHS.ref do
         for d in altLHS.fvarDecls do
           if d.hasExprMVar then
-            -- This code path is a vestige prior to fixing #8099, but it is still appears to be
-            -- important for testcase 1300.lean.
             tryPostpone
             withExistingLocalDecls altLHS.fvarDecls do
               runPendingTacticsAt d.type
+              if (← instantiateMVars d.type).hasExprMVar then
+                throwMVarError m!"Invalid match expression: The type of pattern variable '{d.toExpr}' contains metavariables:{indentExpr d.type}"
         for p in altLHS.patterns do
           if (← Match.instantiatePatternMVars p).hasExprMVar then
             tryPostpone

src/Lean/Elab/Tactic/Basic.lean

@@ -369,6 +369,33 @@ def withoutRecover (x : TacticM α) : TacticM α :=
 def withRecover (recover : Bool) (x : TacticM α) : TacticM α :=
   withReader (fun ctx => { ctx with recover }) x
 
+/-! ## Message log utilities -/
+
+/-- Execute an action while suppressing any new messages it generates.
+    Restores the original message log after the action completes.
+    Useful for trying tactics without polluting the message log with errors from failed attempts. -/
+def withSuppressedMessages (action : TacticM α) : TacticM α := do
+  let initialLog ← Core.getMessageLog
+  try
+    action
+  finally
+    Core.setMessageLog initialLog
+
+/-- Execute an action and return any new messages it generates.
+    Restores the original message log afterward.
+    Useful for inspecting messages produced by a tactic without committing them. -/
+def withCapturedMessages (action : TacticM α) : TacticM (α × List Message) := do
+  let initialLog ← Core.getMessageLog
+  let initialMsgCount := initialLog.toList.length
+  let result ← action
+  let newMsgs := (← Core.getMessageLog).toList.drop initialMsgCount
+  Core.setMessageLog initialLog
+  return (result, newMsgs)
+
+/-- Check if any messages in the list are errors. -/
+def hasErrorMessages (msgs : List Message) : Bool :=
+  msgs.any (·.severity == .error)
+
 /--
 Like `throwErrorAt`, but, if recovery is enabled, logs the error instead.
 -/

src/Lean/Elab/Tactic/Grind/Main.lean

@@ -182,6 +182,7 @@ open LibrarySuggestions in
 def elabGrindSuggestions
     (params : Grind.Params) (suggestions : Array Suggestion := #[]) : MetaM Grind.Params := do
   let mut params := params
+  let mut added : Array Name := #[]
   for p in suggestions do
     let attr ← match p.flag with
     | some flag => parseModifier flag
@@ -190,6 +191,7 @@ def elabGrindSuggestions
     | .ematch kind =>
       try
         params ← addEMatchTheorem params (mkIdent p.name) p.name kind false (warn := false)
+        added := added.push p.name
       catch _ => pure () -- Don't worry if library suggestions gave bad theorems.
     | _ =>
       -- We could actually support arbitrary grind modifiers,
@@ -197,26 +199,40 @@ def elabGrindSuggestions
       -- but this would require a larger refactor.
       -- Let's only do this if there is a prospect of a library suggestion engine supporting this.
       throwError "unexpected modifier {p.flag}"
+  unless added.isEmpty do
+    trace[grind.debug.suggestions] "{added}"
   return params
 
-open LibrarySuggestions in
-def elabGrindParamsAndSuggestions
-    (params : Grind.Params)
-    (ps : TSyntaxArray ``Parser.Tactic.grindParam)
-    (suggestions : Array Suggestion := #[])
-    (only : Bool) (lax : Bool := false) : TermElabM Grind.Params := do
-  let params ← elabGrindParams params ps (lax := lax) (only := only)
-  elabGrindSuggestions params suggestions
+/-- Add all definitions from the current file. -/
+def elabGrindLocals (params : Grind.Params) : MetaM Grind.Params := do
+  let env ← getEnv
+  let mut params := params
+  let mut added : Array Name := #[]
+  for (name, ci) in env.constants.map₂.toList do
+    -- Filter similar to LibrarySuggestions.isDeniedPremise (but inlined to avoid dependency)
+    -- Skip internal details, but allow private names (which are accessible from current module)
+    if name.isInternalDetail && !isPrivateName name then continue
+    if (← Meta.isInstance name) then continue
+    match ci with
+    | .defnInfo _ =>
+      try
+        params ← addEMatchTheorem params (mkIdent name) name (.default false) false (warn := false)
+        added := added.push name
+      catch _ => pure ()
+    | _ => continue
+  unless added.isEmpty do
+    trace[grind.debug.locals] "{added}"
+  return params
 
 def mkGrindParams
     (config : Grind.Config) (only : Bool) (ps : TSyntaxArray ``Parser.Tactic.grindParam) (mvarId : MVarId) :
     TermElabM Grind.Params := do
   let params ← if only then Grind.mkOnlyParams config else Grind.mkDefaultParams config
-  let suggestions ← if config.suggestions then
-    LibrarySuggestions.select mvarId { caller := some "grind" }
-  else
-    pure #[]
-  let mut params ← elabGrindParamsAndSuggestions params ps suggestions (only := only) (lax := config.lax)
+  let mut params ← elabGrindParams params ps (lax := config.lax) (only := only)
+  if config.suggestions then
+    params ← elabGrindSuggestions params (← LibrarySuggestions.select mvarId { caller := some "grind" })
+  if config.locals then
+    params ← elabGrindLocals params
   trace[grind.debug.inj] "{params.extensions[0]!.inj.getOrigins.map (·.pp)}"
   if params.anchorRefs?.isSome then
     /-
@@ -289,21 +305,24 @@ def setGrindParams (stx : TSyntax `tactic) (params : Array Syntax) : TSyntax `ta
 def getGrindParams (stx : TSyntax `tactic) : Array Syntax :=
   stx.raw[grindParamsPos][1].getSepArgs
 
-/-- Filter out `+suggestions` from the config syntax -/
-def filterSuggestionsFromGrindConfig (config : TSyntax ``Lean.Parser.Tactic.optConfig) :
+/-- Filter out `+suggestions` and `+locals` from the config syntax -/
+def filterSuggestionsAndLocalsFromGrindConfig (config : TSyntax ``Lean.Parser.Tactic.optConfig) :
     TSyntax ``Lean.Parser.Tactic.optConfig :=
-  let configItems := config.raw.getArgs
-  let filteredItems := configItems.filter fun item =>
-    -- Keep all items except +suggestions
-    -- Structure: null node -> configItem -> posConfigItem -> ["+", ident]
-    match item[0]? with
-    | some configItem => match configItem[0]? with
-      | some posConfigItem => match posConfigItem[1]? with
-        | some ident => !(posConfigItem.getKind == ``Lean.Parser.Tactic.posConfigItem && ident.getId == `suggestions)
-        | none => true
+  -- optConfig structure: (Tactic.optConfig [configItem1, configItem2, ...])
+  -- config.raw.getArgs returns #[null_node], so we need to filter the null node's children
+  let nullNode := config.raw[0]!
+  let configItems := nullNode.getArgs
+  let filteredItems := configItems.filter fun configItem =>
+    -- Keep all items except +suggestions and +locals
+    -- Structure: configItem -> posConfigItem -> ["+", ident]
+    match configItem[0]? with
+    | some posConfigItem => match posConfigItem[1]? with
+      | some ident =>
+        let id := ident.getId.eraseMacroScopes
+        !(posConfigItem.getKind == ``Lean.Parser.Tactic.posConfigItem && (id == `suggestions || id == `locals))
       | none => true
     | none => true
-  ⟨config.raw.setArgs filteredItems⟩
+  ⟨config.raw.setArg 0 (nullNode.setArgs filteredItems)⟩
 
 private def elabGrindConfig' (config : TSyntax ``Lean.Parser.Tactic.optConfig) (interactive : Bool) : TacticM Grind.Config := do
   if interactive then
@@ -345,7 +364,7 @@ def evalGrindTraceCore (stx : Syntax) (trace := true) (verbose := true) (useSorr
       let finish ← Grind.Action.mkFinish
       let goal :: _ ← Grind.getGoals
         | -- Goal was closed during initialization
-          let configStx' := filterSuggestionsFromGrindConfig configStx
+          let configStx' := filterSuggestionsAndLocalsFromGrindConfig configStx
           if termParamStxs.isEmpty then
             let tac ← `(tactic| grind $configStx':optConfig only)
             return #[tac]
@@ -357,7 +376,7 @@ def evalGrindTraceCore (stx : Syntax) (trace := true) (verbose := true) (useSorr
         -- let saved ← saveState
         match (← finish.run goal) with
         | .closed seq =>
-          let configStx' := filterSuggestionsFromGrindConfig configStx
+          let configStx' := filterSuggestionsAndLocalsFromGrindConfig configStx
           let tacs ← Grind.mkGrindOnlyTactics configStx' seq termParamStxs
           let seq := Grind.Action.mkGrindSeq seq
           let tac ← `(tactic| grind $configStx':optConfig => $seq:grindSeq)

src/Lean/Elab/Tactic/Simp.lean

@@ -416,6 +416,28 @@ structure MkSimpContextResult where
   /-- The elaborated simp arguments with syntax -/
   simpArgs         : Array (Syntax × ElabSimpArgResult) := #[]
 
+/-- Add all definitions from the current file to unfold. -/
+def elabSimpLocals (thms : SimpTheorems) (kind : SimpKind) : MetaM SimpTheorems := do
+  let env ← getEnv
+  let mut thms := thms
+  for (name, ci) in env.constants.map₂.toList do
+    -- Skip internal details, but allow private names (which are accessible from current module)
+    if name.isInternalDetail && !isPrivateName name then continue
+    if (← Meta.isInstance name) then continue
+    match ci with
+    | .defnInfo _ =>
+      -- Definitions are added to unfold
+      try
+        if kind == .dsimp then
+          thms := thms.addDeclToUnfoldCore name
+        else
+          let entries ← mkSimpEntryOfDeclToUnfold name
+          for entry in entries do
+            thms := thms.addSimpEntry entry
+      catch _ => pure () -- Skip definitions that can't be added
+    | _ => continue
+  return thms
+
 /--
    Create the `Simp.Context` for the `simp`, `dsimp`, and `simp_all` tactics.
    If `kind != SimpKind.simp`, the `discharge` option must be `none`
@@ -437,14 +459,18 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp)
       throwError "Tactic `dsimp` does not support the `discharger' option"
   let dischargeWrapper ← mkDischargeWrapper stx[2]
   let simpOnly := !stx[simpOnlyPos].isNone
-  let simpTheorems ← if simpOnly then
+  let mut simpTheorems ← if simpOnly then
     simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems)
   else
     simpTheorems
   let simprocs ← if simpOnly then pure {} else Simp.getSimprocs
   let congrTheorems ← getSimpCongrTheorems
+  let config ← elabSimpConfig stx[1] (kind := kind)
+  -- Add local definitions if +locals is enabled
+  if config.locals then
+    simpTheorems ← elabSimpLocals simpTheorems kind
   let ctx ← Simp.mkContext
-     (config := (← elabSimpConfig stx[1] (kind := kind)))
+     (config := config)
      (simpTheorems := #[simpTheorems])
      congrTheorems
   let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) (simprocs := #[simprocs]) (ignoreStarArg := ignoreStarArg) ctx

src/Lean/Elab/Tactic/SimpTrace.lean

@@ -21,19 +21,21 @@ The `simp?` tactic is a simple wrapper around the simp with trace behavior.
 namespace Lean.Elab.Tactic
 open Lean Elab Parser Tactic Meta Simp Tactic.TryThis
 
-/-- Filter out `+suggestions` from the config syntax -/
-def filterSuggestionsFromSimpConfig (cfg : TSyntax ``Lean.Parser.Tactic.optConfig) :
+/-- Filter out `+suggestions` and `+locals` from the config syntax -/
+def filterSuggestionsAndLocalsFromSimpConfig (cfg : TSyntax ``Lean.Parser.Tactic.optConfig) :
     MetaM (TSyntax ``Lean.Parser.Tactic.optConfig) := do
   -- The config has one arg: a null node containing configItem nodes
   let nullNode := cfg.raw.getArg 0
   let configItems := nullNode.getArgs
 
-  -- Filter out configItem nodes that contain +suggestions
+  -- Filter out configItem nodes that contain +suggestions or +locals
   let filteredItems := configItems.filter fun item =>
     match item[0]?, item.getKind with
     | some posConfigItem, ``Lean.Parser.Tactic.configItem =>
       match posConfigItem[1]?, posConfigItem.getKind with
-      | some ident, ``Lean.Parser.Tactic.posConfigItem => ident.getId != `suggestions
+      | some ident, ``Lean.Parser.Tactic.posConfigItem =>
+        let id := ident.getId.eraseMacroScopes
+        id != `suggestions && id != `locals
       | _, _ => true
     | _, _ => true
 
@@ -72,7 +74,7 @@ def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tacti
     else
       `(tactic| simp%$tk $cfg:optConfig $[$discharger]? $[only%$o]? [$argsArray,*] $[$loc]?)
     -- Build syntax for suggestion (without +suggestions config)
-    let filteredCfg ← filterSuggestionsFromSimpConfig cfg
+    let filteredCfg ← filterSuggestionsAndLocalsFromSimpConfig cfg
     let stxForSuggestion ← if bang.isSome then
       `(tactic| simp!%$tk $filteredCfg:optConfig $[$discharger]? $[only%$o]? [$argsArray,*] $[$loc]?)
     else
@@ -118,7 +120,7 @@ def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tacti
         else
           `(tactic| simp_all%$tk $cfg:optConfig $[$discharger]? $[only%$o]? [$argsArray,*])
     -- Build syntax for suggestion (without +suggestions config)
-    let filteredCfg ← filterSuggestionsFromSimpConfig cfg
+    let filteredCfg ← filterSuggestionsAndLocalsFromSimpConfig cfg
     let stxForSuggestion ←
       if argsArray.isEmpty then
         if bang.isSome then

src/Lean/Elab/Tactic/Try.lean

@@ -196,17 +196,22 @@ private def evalSuggestAtomic (tac : TSyntax `tactic) : TacticM (TSyntax `tactic
   else
     return tac
 
-/-- Check if a config contains `+suggestions` -/
-private def configHasSuggestions (config : TSyntax ``Lean.Parser.Tactic.optConfig) : Bool :=
-  let configItems := config.raw.getArgs
-  configItems.any fun item =>
-    match item[0]? with
-    | some configItem => match configItem[0]? with
+/-- Check if a config contains `+suggestions` or `+locals` -/
+private def configHasSuggestionsOrLocals (config : TSyntax ``Lean.Parser.Tactic.optConfig) : Bool :=
+  -- optConfig structure: (Tactic.optConfig [configItem1, configItem2, ...])
+  -- config.raw.getArgs returns #[null_node], so we need to access the null node's children
+  let nullNode := config.raw[0]?
+  match nullNode with
+  | some node =>
+    node.getArgs.any fun configItem =>
+      match configItem[0]? with
       | some posConfigItem => match posConfigItem[1]? with
-        | some ident => posConfigItem.getKind == ``Lean.Parser.Tactic.posConfigItem && ident.getId == `suggestions
+        | some ident =>
+          let id := ident.getId.eraseMacroScopes
+          posConfigItem.getKind == ``Lean.Parser.Tactic.posConfigItem && (id == `suggestions || id == `locals)
         | none => false
       | none => false
-    | none => false
+  | none => false
 
 private def grindTraceToGrind (tac : TSyntax `tactic) : TacticM (TSyntax `tactic) := do
   match tac with
@@ -534,7 +539,7 @@ private def evalSuggestGrindTrace : TryTactic := fun tac => do
       trace[try.debug] ">> {tac1}"
     if (← read).config.only then
       -- If config has +suggestions, only return the 'only' version, not the original
-      if configHasSuggestions configStx then
+      if configHasSuggestionsOrLocals configStx then
         mkTrySuggestions tacs
       else
         mkTrySuggestions (#[tac] ++ tacs)
@@ -552,7 +557,7 @@ private def evalSuggestSimpTrace : TryTactic := fun tac => do (← getMainGoal).
       if (← read).config.only then
         let tac' ← mkSimpCallStx tac stats.usedTheorems
         -- If config has +suggestions, only return the 'only' version, not the original
-        if configHasSuggestions configStx then
+        if configHasSuggestionsOrLocals configStx then
           mkTrySuggestions #[tac']
         else
           mkTrySuggestions #[tac, tac']
@@ -565,7 +570,7 @@ private def evalSuggestSimpAllTrace : TryTactic := fun tac => do
   | `(tactic| simp_all? $[!%$_bang]? $configStx:optConfig $(_discharger)? $[only%$_only]? $[[$_args,*]]?) =>
     (← getMainGoal).withContext do
       withOriginalHeartbeats do
-        let hasSuggestions := configHasSuggestions configStx
+        let hasSuggestionsOrLocals := configHasSuggestionsOrLocals configStx
 
         -- Get library suggestions if +suggestions is present
         let config ← elabSimpConfig configStx (kind := .simpAll)
@@ -598,13 +603,13 @@ private def evalSuggestSimpAllTrace : TryTactic := fun tac => do
         | some mvarId => replaceMainGoal [mvarId]
         trace[try.debug] "`simp_all` succeeded"
         if (← read).config.only then
-          -- Remove +suggestions from config for the output (similar to SimpTrace.lean)
-          let filteredCfg ← filterSuggestionsFromSimpConfig configStx
+          -- Remove +suggestions and +locals from config for the output (similar to SimpTrace.lean)
+          let filteredCfg ← filterSuggestionsAndLocalsFromSimpConfig configStx
           -- Convert simp_all? to simp_all for mkSimpCallStx (similar to simpTraceToSimp)
           let tacWithoutTrace ← `(tactic| simp_all $filteredCfg:optConfig $[only%$_only]? $[[$_args,*]]?)
           let tac' ← mkSimpCallStx tacWithoutTrace stats.usedTheorems
-          -- If config has +suggestions, only return the 'only' version, not the original
-          if hasSuggestions then
+          -- If config has +suggestions or +locals, only return the 'only' version, not the original
+          if hasSuggestionsOrLocals then
             mkTrySuggestions #[tac']
           else
             mkTrySuggestions #[tac, tac']
@@ -731,6 +736,15 @@ private partial def evalSuggestAttemptAllPar (tacs : Array (TSyntax ``Parser.Tac
   else
     throwError "`attempt_all_par` failed"
 
+/-- `evalSuggest` for `first_par` tactic - returns first successful result, cancels others. -/
+private partial def evalSuggestFirstPar (tacs : Array (TSyntax ``Parser.Tactic.tacticSeq)) : TryTacticM (TSyntax `tactic) := do
+  unless (← read).terminal do
+    throwError "invalid occurrence of `first_par` in non-terminal position for `try?` script{indentD (← read).root}"
+  let ctx ← read
+  let jobs : List (TacticM (TSyntax `tactic)) := tacs.toList.map fun tacSeq =>
+    withOriginalHeartbeats (evalSuggestTacticSeq tacSeq) ctx
+  TacticM.parFirst jobs
+
 private partial def evalSuggestDefault (tac : TSyntax `tactic) : TryTacticM (TSyntax `tactic) := do
   let kind := tac.raw.getKind
   match (← getEvalFns kind) with
@@ -778,6 +792,7 @@ private partial def evalSuggestImpl : TryTactic := fun tac => do
   | `(tactic| try $tac:tacticSeq) => evalSuggestTry tac
   | `(tactic| attempt_all $[| $tacs]*) => evalSuggestAttemptAll tacs
   | `(tactic| attempt_all_par $[| $tacs]*) => evalSuggestAttemptAllPar tacs
+  | `(tactic| first_par $[| $tacs]*) => evalSuggestFirstPar tacs
   | _ =>
     let k := tac.raw.getKind
     if k == ``Parser.Tactic.seq1 then
@@ -821,13 +836,12 @@ private def addSuggestions (tk : Syntax) (s : Array Tactic.TryThis.Suggestion) :
     Tactic.TryThis.addSuggestions tk (s.map fun stx => stx) (origSpan? := (← getRef))
 
 def evalAndSuggest (tk : Syntax) (tac : TSyntax `tactic) (originalMaxHeartbeats : Nat) (config : Try.Config := {}) : TacticM Unit := do
-  let initialLog ← Core.getMessageLog
-  let tac' ← try
-    evalSuggest tac |>.run { terminal := true, root := tac, config, originalMaxHeartbeats }
-  catch _ =>
-    throwEvalAndSuggestFailed config
-  -- Restore message log to suppress "Try this" messages from intermediate tactic executions
-  Core.setMessageLog initialLog
+  -- Suppress "Try this" messages from intermediate tactic executions
+  let tac' ← withSuppressedMessages do
+    try
+      evalSuggest tac |>.run { terminal := true, root := tac, config, originalMaxHeartbeats }
+    catch _ =>
+      throwEvalAndSuggestFailed config
   let s := (getSuggestions tac')[*...config.max].toArray
   if s.isEmpty then
     throwEvalAndSuggestFailed config
@@ -882,7 +896,10 @@ Note: We previously included `simp_all? +suggestions` here, but removed it due t
 We would like to restore it in the future once `simp_all? +suggestions` is faster for general use.
 -/
 private def mkAtomicWithSuggestionsStx : CoreM (TSyntax `tactic) :=
-  `(tactic| grind? +suggestions)
+  `(tactic| first_par
+      | grind? +suggestions
+      | grind? +locals
+      | grind? +locals +suggestions)
 
 /-- `simple` tactics -/
 private def mkSimpleTacStx : CoreM (TSyntax `tactic) :=
@@ -947,8 +964,9 @@ private unsafe def mkTryEvalSuggestStxUnsafe (goal : MVarId) (info : Try.Info) :
 
   let atomic ← `(tactic| attempt_all_par | $simple:tactic | $simp:tactic | $grind:tactic | simp_all)
   let atomicSuggestions ← mkAtomicWithSuggestionsStx
-  let funInds ← mkAllFunIndStx info atomic
-  let inds ← mkAllIndStx info atomic
+  let atomicOrSuggestions ← `(tactic| first | $atomic:tactic | $atomicSuggestions:tactic)
+  let funInds ← mkAllFunIndStx info atomicOrSuggestions
+  let inds ← mkAllIndStx info atomicOrSuggestions
   let extra ← `(tactic| (intros; first | $simple:tactic | $simp:tactic | exact?))
 
   -- Collect user-defined suggestions (runs after built-in tactics)
@@ -985,13 +1003,12 @@ private def wrapSuggestionWithBy (sugg : Tactic.TryThis.Suggestion) : TacticM Ta
 
 /-- Version of `evalAndSuggest` that wraps tactic suggestions with `by` for term mode. -/
 private def evalAndSuggestWithBy (tk : Syntax) (tac : TSyntax `tactic) (originalMaxHeartbeats : Nat) (config : Try.Config) : TacticM Unit := do
-  let initialLog ← Core.getMessageLog
-  let tac' ← try
-    evalSuggest tac |>.run { terminal := true, root := tac, config, originalMaxHeartbeats }
-  catch _ =>
-    throwEvalAndSuggestFailed config
-  -- Restore message log to suppress "Try this" messages from intermediate tactic executions
-  Core.setMessageLog initialLog
+  -- Suppress "Try this" messages from intermediate tactic executions
+  let tac' ← withSuppressedMessages do
+    try
+      evalSuggest tac |>.run { terminal := true, root := tac, config, originalMaxHeartbeats }
+    catch _ =>
+      throwEvalAndSuggestFailed config
   let suggestions := (getSuggestions tac')[*...config.max].toArray
   if suggestions.isEmpty then
     throwEvalAndSuggestFailed config

src/Lean/Environment.lean

@@ -1502,7 +1502,8 @@ def mkEmptyEnvironment (trustLevel : UInt32 := 0) : IO Environment := do
   return {
     base := .const {
       const2ModIdx    := {}
-      constants       := {}
+      -- Make sure we return a sharing-friendly map set to stage 2, like in `finalizeImport`.
+      constants       := SMap.empty.switch
       header          := { trustLevel }
       extensions      := exts
       irBaseExts      := exts

src/Lean/LibrarySuggestions/SineQuaNon.lean

@@ -9,7 +9,7 @@ prelude
 public import Lean.CoreM
 public import Lean.Meta.Basic
 import Lean.Meta.Instances
-import Lean.LibrarySuggestions.SymbolFrequency
+import all Lean.LibrarySuggestions.SymbolFrequency
 public import Lean.LibrarySuggestions.Basic
 
 /-!
@@ -108,7 +108,7 @@ builtin_initialize sineQuaNonExt : PersistentEnvExtension (NameMap (List (Name
     addImportedFn   := fun mapss _ => pure mapss
     addEntryFn      := nofun
     -- TODO: it would be nice to avoid the `toArray` here, e.g. via iterators.
-    exportEntriesFnEx := fun env _ _ => env.unsafeRunMetaM do return #[← prepareTriggers (env.constants.map₂.toArray.map (·.1))]
+    exportEntriesFnEx := fun env _ _ => unsafe env.unsafeRunMetaM do return #[← prepareTriggers (env.constants.map₂.toArray.map (·.1))]
     statsFn         := fun _ => "sine qua non premise selection extension"
   }
 

src/Lean/LibrarySuggestions/SymbolFrequency.lean

@@ -69,10 +69,10 @@ public def localSymbolFrequency (n : Name) : MetaM Nat := do
 Helper function for running `MetaM` code during module export, when there is nothing but an `Environment` available.
 Panics on errors.
 -/
-public def _root_.Lean.Environment.unsafeRunMetaM [Inhabited α] (env : Environment) (x : MetaM α) : α :=
-   match unsafe unsafeEIO ((((withoutExporting x).run' {} {}).run' { fileName := "symbolFrequency", fileMap := default } { env })) with
+unsafe def _root_.Lean.Environment.unsafeRunMetaM [Inhabited α] (env : Environment) (x : MetaM α) : α :=
+   match unsafeEIO ((((withoutExporting x).run' {} {}).run' { fileName := "symbolFrequency", fileMap := default } { env })) with
    | Except.ok a => a
-   | Except.error ex => panic! match unsafe unsafeIO ex.toMessageData.toString with
+   | Except.error ex => panic! match unsafeIO ex.toMessageData.toString with
      | Except.ok s => s
      | Except.error ex => ex.toString
 
@@ -90,7 +90,7 @@ builtin_initialize symbolFrequencyExt : PersistentEnvExtension (NameMap Nat) Emp
     mkInitial       := pure ∅
     addImportedFn   := fun mapss _ => pure mapss
     addEntryFn      := nofun
-    exportEntriesFnEx := fun env _ _ => env.unsafeRunMetaM do return #[← cachedLocalSymbolFrequencyMap]
+    exportEntriesFnEx := fun env _ _ => unsafe env.unsafeRunMetaM do return #[← cachedLocalSymbolFrequencyMap]
     statsFn         := fun _ => "symbol frequency extension"
   }
 

src/Lean/Meta.lean

@@ -59,3 +59,5 @@ public import Lean.Meta.Hint
 public import Lean.Meta.MethodSpecs
 public import Lean.Meta.CtorIdxHInj
 public import Lean.Meta.Sym
+public import Lean.Meta.MonadSimp
+public import Lean.Meta.HaveTelescope

src/Lean/Meta/Basic.lean

@@ -1097,13 +1097,6 @@ Similar to `Expr.abstract`, but handles metavariables correctly.
 def _root_.Lean.Expr.abstractM (e : Expr) (xs : Array Expr) : MetaM Expr :=
   e.abstractRangeM xs.size xs
 
-/--
-Replace occurrences of the free variables `fvars` in `e` with `vs`.
-Similar to `Expr.replaceFVars`, but handles metavariables correctly.
--/
-def _root_.Lean.Expr.replaceFVarsM (e : Expr) (fvars : Array Expr) (vs : Array Expr) : MetaM Expr :=
-  return (← e.abstractM fvars).instantiateRev vs
-
 /--
 Collect forward dependencies for the free variables in `toRevert`.
 Recall that when reverting free variables `xs`, we must also revert their forward dependencies.

src/Lean/Meta/HaveTelescope.lean

@@ -0,0 +1,461 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller, Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Basic
+public import Lean.Meta.MonadSimp
+import Lean.Util.CollectFVars
+import Lean.Util.CollectLooseBVars
+import Lean.Meta.InferType
+import Lean.Meta.AppBuilder
+public section
+namespace Lean.Meta
+/-!
+Support for representing `HaveTelescope`s and simplifying them.
+We use this module to implement both `Sym.simp` and `Meta.simp` using the `MonadSimp` adapter.
+-/
+
+/--
+Information about a single `have` in a `have` telescope.
+Created by `getHaveTelescopeInfo`.
+-/
+structure HaveInfo where
+  /-- Previous `have`s that the type of this `have` depends on, as indices into `HaveTelescopeInfo.haveInfo`.
+  Used in `computeFixedUsed` to compute used `have`s. -/
+  typeBackDeps : Std.HashSet Nat
+  /-- Previous `have`s that the value of this `have` depends on, as indices into `HaveTelescopeInfo.haveInfo`.
+  Used in `computeFixedUsed` to compute used `have`s. -/
+  valueBackDeps : Std.HashSet Nat
+  /-- The local decl for the `have`, so that the local context can be re-entered `have`-by-`have`.
+  N.B. This stores the fvarid for the `have` as well as cached versions of the value and type
+  instantiated with the fvars from the telescope. -/
+  decl : LocalDecl
+  /-- The level of the type for this `have`, cached. -/
+  level : Level
+  deriving Inhabited
+
+/--
+Information about a `have` telescope.
+Created by `getHaveTelescopeInfo` and used in `simpHaveTelescope`.
+
+The data is used to avoid applying `Expr.abstract` more than once on any given subexpression
+when constructing terms and proofs during simplification. Abstraction is linear in the size `t` of a term,
+and so in a depth-`n` telescope it is `O(nt)`, quadratic in `n`, since `n ≤ t`.
+For example, given `have x₁ := v₁; ...; have xₙ := vₙ; b` and `h : b = b'`, we need to construct
+```lean
+have_body_congr (fun x₁ => ... have_body_congr (fun xₙ => h)))
+```
+We apply `Expr.abstract` to `h` *once* and then build the term, rather than
+using `mkLambdaFVars #[fvarᵢ] pfᵢ` at each step.
+
+As an additional optimization, we save the fvar-instantiated terms calculated by `getHaveTelescopeInfo`
+so that we don't have to compute them again. This is only saving a constant factor.
+
+It is also used for computing used `have`s in `computeFixedUsed`.
+In `have x₁ := v; have x₂ := x₁; ⋯; have xₙ := xₙ₋₁; b`, if `xₙ` is unused in `b`, then all the
+`have`s are unused. Without a global computation of used `have`s, the proof term would be quadratic
+in the number of `have`s (with `n` iterations of `simp`). Knowing which `have`s are transitively
+unused lets the proof term be linear in size.
+-/
+structure HaveTelescopeInfo where
+  /-- Information about each `have` in the telescope. -/
+  haveInfo : Array HaveInfo := #[]
+  /-- The set of `have`s that the body depends on, as indices into `haveInfo`.
+  Used in `computeFixedUsed` to compute used `have`s. -/
+  bodyDeps : Std.HashSet Nat := {}
+  /-- The set of `have`s that the type of the body depends on, as indices into `haveInfo`.
+  This is the set of fixed `have`s. -/
+  bodyTypeDeps : Std.HashSet Nat := {}
+  /-- A cached version of the telescope body, instantiated with fvars from each `HaveInfo.decl`. -/
+  body : Expr := Expr.const `_have_telescope_info_dummy_ []
+  /-- A cached version of the telescope body's type, instantiated with fvars from each `HaveInfo.decl`. -/
+  bodyType : Expr := Expr.const `_have_telescope_info_dummy_ []
+  /-- The universe level for the `have` expression, cached. -/
+  level : Level := Level.param `_have_telescope_info_dummy_
+  deriving Inhabited
+
+/--
+Efficiently collect dependency information for a `have` telescope.
+This is part of a scheme to avoid quadratic overhead from the locally nameless discipline
+(see `HaveTelescopeInfo` and `simpHaveTelescope`).
+
+The expression `e` must not have loose bvars.
+-/
+def getHaveTelescopeInfo (e : Expr) : MetaM HaveTelescopeInfo := do
+  collect e 0 {} (← getLCtx) #[]
+where
+  collect (e : Expr) (numHaves : Nat) (info : HaveTelescopeInfo) (lctx : LocalContext) (fvars : Array Expr) : MetaM HaveTelescopeInfo := do
+    /-
+    Gives indices into `fvars` that the uninstantiated expression `a` depends on, from collecting its bvars.
+    This is more efficient than collecting `fvars` from an instantiated expression,
+    since the expression likely contains many fvars for the pre-existing local context.
+    -/
+    let getBackDeps (a : Expr) : Std.HashSet Nat :=
+      a.collectLooseBVars.fold (init := {}) fun deps vidx =>
+        -- Since the original expression has no bvars, `vidx < numHaves` must be true.
+        deps.insert (numHaves - vidx - 1)
+    match e with
+    | .letE n t v b true =>
+      let typeBackDeps := getBackDeps t
+      let valueBackDeps := getBackDeps v
+      let t := t.instantiateRev fvars
+      let v := v.instantiateRev fvars
+      let level ← withLCtx' lctx <| getLevel t
+      let fvarId ← mkFreshFVarId
+      let decl := LocalDecl.ldecl 0 fvarId n t v true .default
+      let info := { info with haveInfo := info.haveInfo.push { typeBackDeps, valueBackDeps, decl, level } }
+      let lctx := lctx.addDecl decl
+      let fvars := fvars.push (mkFVar fvarId)
+      collect b (numHaves + 1) info lctx fvars
+    | _ =>
+      let bodyDeps := getBackDeps e
+      withLCtx' lctx do
+        let body := e.instantiateRev fvars
+        let bodyType ← inferType body
+        let level ← getLevel bodyType
+        -- Collect fvars appearing in the type of `e`. Computing `bodyType` in particular is where `MetaM` is necessary.
+        let bodyTypeFVarIds := (collectFVars {} bodyType).fvarSet
+        let bodyTypeDeps : Std.HashSet Nat := Nat.fold fvars.size (init := {}) fun idx _ deps =>
+          if bodyTypeFVarIds.contains fvars[idx].fvarId! then
+            deps.insert idx
+          else
+            deps
+        return { info with bodyDeps, bodyTypeDeps, body, bodyType, level }
+
+/--
+Computes which `have`s in the telescope are fixed and which are unused.
+The length of the unused array may be less than the number of `have`s: use `unused.getD i true`.
+-/
+def HaveTelescopeInfo.computeFixedUsed (info : HaveTelescopeInfo) (keepUnused : Bool) :
+    MetaM (Array Bool × Array Bool) := do
+  let fixed ← go info.bodyTypeDeps
+  if keepUnused then
+    return (fixed, #[])
+  else
+    let used ← go info.bodyDeps
+    return (fixed, used)
+where
+  updateArrayFromBackDeps (arr : Array Bool) (s : Std.HashSet Nat) : Array Bool :=
+    s.fold (init := arr) fun arr idx => arr.set! idx true
+  go init : MetaM (Array Bool) := do
+    let numHaves := info.haveInfo.size
+    let mut used : Array Bool := Array.replicate numHaves false
+    -- Initialize `used` with the body's dependencies.
+    -- There is no need to consider `info.bodyTypeDeps` in this computation.
+    used := updateArrayFromBackDeps used init
+    -- For each used `have`, in reverse order, update `used`.
+    for i in *...numHaves do
+      let idx := numHaves - i - 1
+      if used[idx]! then
+        let hinfo := info.haveInfo[idx]!
+        used := updateArrayFromBackDeps used hinfo.typeBackDeps
+        used := updateArrayFromBackDeps used hinfo.valueBackDeps
+    return used
+
+/--
+Auxiliary structure used to represent the return value of `simpHaveTelescopeAux`.
+See `simpHaveTelescope` for an overview and `HaveTelescopeInfo` for an example.
+-/
+private structure SimpHaveResult where
+  /--
+  The simplified expression in `(fun x => b) v` form. Note that it may contain loose bound variables.
+  `simpHaveTelescope` attempts to minimize the quadratic overhead imposed
+  by the locally nameless discipline in a sequence of `have` expressions.
+  -/
+  expr     : Expr
+  /--
+  The type of `expr`. It may contain loose bound variables like in the `expr` field.
+  Used in proof construction.
+  -/
+  exprType : Expr
+  /--
+  The initial expression in `(fun x => b) v` form.
+  -/
+  exprInit   : Expr
+  /--
+  The expression `expr` in `have x := v; b` form.
+  -/
+  exprResult : Expr
+  /--
+  The proof that the simplified expression is equal to the input one.
+  It may contain loose bound variables like in the `expr` field.
+  -/
+  proof    : Expr
+  /--
+  `modified := false` iff `expr` is structurally equal to the input expression.
+  When false, `proof` is `Eq.refl`.
+  -/
+  modified : Bool
+
+  /-
+  Re-enters the telescope recorded in `info` using `withExistingLocalDecls` while simplifying according to `fixed`/`used`.
+  Note that we must use the low-level `Expr` APIs because the expressions may contain loose bound variables.
+  Note also that we don't enter the body's local context all at once, since we need to be sure that
+  when we simplify values they have their correct local context.
+  -/
+  deriving Inhabited
+
+variable {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] [MonadSimp m]
+
+/-
+Re-enters the telescope recorded in `info` using `withExistingLocalDecls` while simplifying according to `fixed`/`used`.
+Note that we must use the low-level `Expr` APIs because the expressions may contain loose bound variables.
+Note also that we don't enter the body's local context all at once, since we need to be sure that
+when we simplify values they have their correct local context.
+-/
+private def simpHaveTelescopeAux (info : HaveTelescopeInfo) (fixed : Array Bool) (used : Array Bool)
+      (e : Expr) (i : Nat) (xs : Array Expr) : m SimpHaveResult := do
+  if h : i < info.haveInfo.size then
+    let hinfo := info.haveInfo[i]
+    -- `x` and `val` are the fvar and value with respect to the local context.
+    let x := hinfo.decl.toExpr
+    let val := hinfo.decl.value true
+    -- Invariant: `v == val.abstract xs`.
+    let .letE n t v b true := e | unreachable!
+    -- Universe levels to use for each of the `have_*` theorems. It's the level of `val` and the level of the body.
+    let us := [hinfo.level, info.level]
+    if !used.getD i true then
+      /-
+      Unused `have`: do not add `x` to the local context then `simp` only the body.
+      -/
+      (do trace[Debug.Meta.Tactic.simp] "have telescope; unused {n} := {val}" : MetaM _)
+      /-
+      Complication: Unused `have`s might only be transitively unused.
+      This means that `b.hasLooseBVar 0` might actually be true.
+      This matters because `t` and `v` appear in the proof term.
+      We use a dummy `x` for debugging purposes. (Recall that `Expr.abstract` skips non-fvar/mvars.)
+      -/
+      let x := mkConst `_simp_let_unused_dummy
+      let rb ← simpHaveTelescopeAux info fixed used b (i + 1) (xs.push x)
+      -- TODO(kmill): This is a source of quadratic complexity. It might be possible to avoid this,
+      -- but we will need to carefully re-review the logic (note that `rb.proof` still refers to `x`).
+      let expr := rb.expr.lowerLooseBVars 1 1
+      let exprType := rb.exprType.lowerLooseBVars 1 1
+      let exprInit := mkApp (mkLambda n .default t rb.exprInit) v
+      let exprResult := rb.exprResult.lowerLooseBVars 1 1
+      if rb.modified then
+        let proof := mkApp6 (mkConst ``have_unused_dep' us) t exprType v (mkLambda n .default t rb.exprInit) expr
+          (mkLambda n .default t rb.proof)
+        return { expr, exprType, exprInit, exprResult, proof, modified := true }
+      else
+        -- If not modified, this must have been a non-transitively unused `have`, so no need for `dep` form.
+        let proof := mkApp6 (mkConst ``have_unused' us) t exprType v expr expr
+          (mkApp2 (mkConst ``Eq.refl [info.level]) exprType expr)
+        return { expr, exprType, exprInit, exprResult, proof, modified := true }
+    else if fixed.getD i true then
+      /-
+      Fixed `have` (like `CongrArgKind.fixed`): dsimp the value and simp the body.
+      The variable appears in the type of the body.
+      -/
+      let val' ← MonadSimp.dsimp val
+      (do trace[Debug.Meta.Tactic.simp] "have telescope; fixed {n} := {val} => {val'}" : MetaM _)
+      let vModified := val != val'
+      let v' := if vModified then val'.abstract xs else v
+      withExistingLocalDecls [hinfo.decl] <| MonadSimp.withNewLemmas #[x] do
+        let rb ← simpHaveTelescopeAux info fixed used b (i + 1) (xs.push x)
+        let expr := mkApp (mkLambda n .default t rb.expr) v'
+        let exprType := mkApp (mkLambda n .default t rb.exprType) v'
+        let exprInit := mkApp (mkLambda n .default t rb.exprInit) v
+        let exprResult := mkHave n t v' rb.exprResult
+        -- Note: if `vModified`, then the kernel will reduce the telescopes and potentially do an expensive defeq check.
+        -- If this is a performance issue, we could try using a `letFun` encoding here make use of the `is_def_eq_args` optimization.
+        -- Namely, to guide the defeqs via the sequence
+        --   `(fun x => b) v` = `letFun (fun x => b) v` = `letFun (fun x => b) v'` = `(fun x => b) v'`
+        if rb.modified then
+          let proof := mkApp6 (mkConst ``have_body_congr_dep' us) t (mkLambda n .default t rb.exprType) v'
+            (mkLambda n .default t rb.exprInit) (mkLambda n .default t rb.expr) (mkLambda n .default t rb.proof)
+          return { expr, exprType, exprInit, exprResult, proof, modified := true }
+        else
+          let proof := mkApp2 (mkConst ``Eq.refl [info.level]) exprType expr
+          return { expr, exprType, exprInit, exprResult, proof, modified := vModified }
+    else
+      /-
+      Non-fixed `have` (like `CongrArgKind.eq`): simp both the value and the body.
+      The variable does not appear in the type of the body.
+      -/
+      let (v', valModified, vproof) ← match (← MonadSimp.simp val) with
+        | .rfl => pure (v, false, mkApp2 (mkConst `Eq.refl [hinfo.level]) t v)
+        | .step val' h =>
+          (do trace[Debug.Meta.Tactic.simp] "have telescope; non-fixed {n} := {val} => {val'}" : MetaM _)
+          pure (val'.abstract xs, true, h.abstract xs)
+      withExistingLocalDecls [hinfo.decl] <| MonadSimp.withNewLemmas #[x] do
+        let rb ← simpHaveTelescopeAux info fixed used b (i + 1) (xs.push x)
+        let expr := mkApp (mkLambda n .default t rb.expr) v'
+        assert! !rb.exprType.hasLooseBVar 0
+        let exprType := rb.exprType.lowerLooseBVars 1 1
+        let exprInit := mkApp (mkLambda n .default t rb.exprInit) v
+        let exprResult := mkHave n t v' rb.exprResult
+        match valModified, rb.modified with
+        | false, false =>
+          let proof := mkApp2 (mkConst `Eq.refl [info.level]) exprType expr
+          return { expr, exprType, exprInit, exprResult, proof, modified := false }
+        | true, false =>
+          let proof := mkApp6 (mkConst ``have_val_congr' us) t exprType v v'
+            (mkLambda n .default t rb.exprInit) vproof
+          return { expr, exprType, exprInit, exprResult, proof, modified := true }
+        | false, true =>
+          let proof := mkApp6 (mkConst ``have_body_congr' us) t exprType v
+            (mkLambda n .default t rb.exprInit) (mkLambda n .default t rb.expr) (mkLambda n .default t rb.proof)
+          return { expr, exprType, exprInit, exprResult, proof, modified := true }
+        | true, true =>
+          let proof := mkApp8 (mkConst ``have_congr' us) t exprType v v'
+            (mkLambda n .default t rb.exprInit) (mkLambda n .default t rb.expr) vproof (mkLambda n .default t rb.proof)
+          return { expr, exprType, exprInit, exprResult, proof, modified := true }
+  else
+    -- Base case: simplify the body.
+    (do trace[Debug.Meta.Tactic.simp] "have telescope; simplifying body {info.body}" : MetaM _)
+    let exprType := info.bodyType.abstract xs
+    match (← MonadSimp.simp info.body) with
+    | .rfl =>
+      let proof := mkApp2 (mkConst `Eq.refl [info.level]) exprType e
+      return { expr := e, exprType, exprInit := e, exprResult := e, proof, modified := false }
+    | .step body' h =>
+      let expr := body'.abstract xs
+      let proof := h.abstract xs
+      -- Optimization: if the proof is a `simpHaveTelescope` proof, then remove the type hint
+      -- to avoid the zeta/beta reductions that the kernel would otherwise do.
+      -- In `SimpHaveResult.toResult` we insert two type hints; the inner one
+      -- encodes the `exprInit` and `expr`.
+      let detectSimpHaveLemma (proof : Expr) : Option SimpHaveResult := do
+        let_expr id eq proof' := proof | failure
+        guard <| eq.isAppOfArity ``Eq 3
+        let_expr id eq' proof'' := proof' | failure
+        let_expr Eq _ lhs rhs := eq' | failure
+        let .const n _ := proof''.getAppFn | failure
+        guard (n matches ``have_unused_dep' | ``have_unused' | ``have_body_congr_dep' | ``have_val_congr' | ``have_body_congr' | ``have_congr')
+        return { expr := rhs, exprType, exprInit := lhs, exprResult := expr, proof := proof'', modified := true }
+      if let some res := detectSimpHaveLemma proof then
+        return res
+      return { expr, exprType, exprInit := e, exprResult := expr, proof, modified := true }
+
+/-- Configuration for specifying how unused let-declarations are eliminated. -/
+inductive ZetaUnusedMode where
+  | /-- Do not eliminate unused `let`-declarations. -/
+    no
+  | /-- Simplify and eliminate unused `let`-declarations in a single pass. -/
+    singlePass
+  | /-- Simplify and then eliminate unused `let`-declarations. -/
+    twoPasses
+
+/-- Remove unused-let declarations. -/
+def zetaUnused (e : Expr) : MetaM Expr := do
+  letTelescope e fun xs body => do
+    let mut s := collectFVars {} body
+    let mut ys := #[]
+    let mut i := xs.size
+    while i > 0 do
+      i := i - 1
+      let x := xs[i]!
+      let xFVarId := x.fvarId!
+      if s.fvarSet.contains xFVarId then
+        let decl ← xFVarId.getDecl
+        s  := collectFVars s decl.type
+        s  := collectFVars s (decl.value (allowNondep := true))
+        ys := ys.push x
+    if ys.size == xs.size then
+      return e
+    else
+      mkLetFVars (generalizeNondepLet := false) ys.reverse body
+
+/--
+Constructs the final result. If `keepUnused` is `false`, it eliminates unused let-declarations from
+`exprResult` using `zetaUnused` above. This flag is used when we set `ZetaUnusedMode.twoPasses`.
+-/
+private def SimpHaveResult.toResult (u : Level) (source : Expr) (result : SimpHaveResult) (keepUnused : Bool) : MetaM MonadSimp.Result := do
+  match result with
+  | { expr, exprType, exprInit, exprResult, proof, modified, .. } =>
+    if modified then
+      let proof :=
+          -- Add a type hint to convert back into `have` form.
+          mkExpectedPropHint (expectedProp := mkApp3 (mkConst ``Eq [u]) exprType source exprResult) <|
+            -- Add in a second type hint, for use in an optimization to avoid zeta/beta reductions in the kernel
+            -- The base case in `simpHaveTelescopeAux` detects this construction and uses `exprType`/`exprInit`
+            -- to construct the `SimpHaveResult`.
+            -- If the kernel were to support `have` forms of the congruence lemmas this would not be necessary.
+            mkExpectedPropHint (expectedProp := mkApp3 (mkConst ``Eq [u]) exprType exprInit expr) proof
+      if keepUnused then
+        return .step exprResult proof
+      else
+        let exprResult' ← zetaUnused exprResult
+        if exprResult' == exprResult then
+          return .step exprResult proof
+        else
+          let proof := mkApp6 (mkConst ``Eq.trans [u]) exprType source exprResult exprResult' proof
+            (mkApp2 (mkConst ``Eq.refl [u]) exprType exprResult')
+          return .step exprResult' proof
+    else if keepUnused then
+      return .rfl
+    else
+      let exprResult ← zetaUnused source
+      if exprResult == source then
+        return .rfl
+      else
+        let proof := mkApp2 (mkConst ``Eq.refl [u]) exprType exprResult
+        return .step exprResult proof
+
+/--
+Routine for simplifying `have` telescopes. Used by `simpLet`.
+This is optimized to be able to handle deep `have` telescopes while avoiding quadratic complexity
+arising from the locally nameless expression representations.
+
+## Overview
+
+Consider a `have` telescope:
+```
+have x₁ : T₁ := v₁; ...; have xₙ : Tₙ := vₙ; b
+```
+We say `xᵢ` is *fixed* if it appears in the type of `b`.
+If `xᵢ` is fixed, then it can only be rewritten using definitional equalities.
+Otherwise, we can freely rewrite the value using a propositional equality `vᵢ = vᵢ'`.
+The body `b` can always be freely rewritten using a propositional equality `b = b'`.
+(All the mentioned equalities must be type correct with respect to the obvious local contexts.)
+
+If `xᵢ` neither appears in `b` nor any `Tⱼ` nor any `vⱼ`, then its `have` is *unused*.
+Unused `have`s can be eliminated, which we do if `cfg.zetaUnused` is true.
+We clear `have`s from the end, to be able to transitively clear chains of unused `have`s.
+This is why we honor `zetaUnused` here even though `reduceStep` is also responsible for it;
+`reduceStep` can only eliminate unused `have`s at the start of a telescope.
+Eliminating all transitively unused `have`s at once like this also avoids quadratic complexity.
+
+If `debug.simp.check.have` is enabled then we typecheck the resulting expression and proof.
+
+## Proof generation
+
+There are two main complications with generating proofs.
+1. We work almost exclusively with expressions with loose bound variables,
+   to avoid overhead from instantiating and abstracting free variables,
+   which can lead to complexity quadratic in the telescope length.
+   (See `HaveTelescopeInfo`.)
+2. We want to avoid triggering zeta reductions in the kernel.
+
+Regarding this second point, the issue is that we cannot organize the proof using congruence theorems
+in the obvious way. For example, given
+```
+theorem have_congr {α : Sort u} {β : Sort v} {a a' : α} {f f' : α → β}
+    (h₁ : a = a') (h₂ : ∀ x, f x = f' x) :
+    (have x := a; f x) = (have x := a'; f' x)
+```
+the kernel sees that the type of `have_congr (fun x => b) (fun x => b') h₁ h₂`
+is `(have x := a; (fun x => b) x) = (have x := a'; (fun x => b') x)`,
+since when instantiating values it does not beta reduce at the same time.
+Hence, when `is_def_eq` is applied to the LHS and `have x := a; b` for example,
+it will do `whnf_core` to both sides.
+
+Instead, we use the form `(fun x => b) a = (fun x => b') a'` in the proofs,
+which we can reliably match up without triggering beta reductions in the kernel.
+The zeta/beta reductions are then limited to the type hint for the entire telescope,
+when we convert this back into `have` form.
+In the base case, we include an optimization to avoid unnecessary zeta/beta reductions,
+by detecting a `simpHaveTelescope` proofs and removing the type hint.
+-/
+def simpHaveTelescope (e : Expr) (zetaUnusedMode : ZetaUnusedMode := .twoPasses) : m MonadSimp.Result := do
+  let info ← getHaveTelescopeInfo e
+  assert! !info.haveInfo.isEmpty
+  let (fixed, used) ← info.computeFixedUsed (keepUnused := zetaUnusedMode matches .no | .twoPasses)
+  let r ← simpHaveTelescopeAux info fixed used e 0 (Array.mkEmpty info.haveInfo.size)
+  r.toResult info.level e (keepUnused := zetaUnusedMode matches .no | .singlePass)
+
+end Lean.Meta

src/Lean/Meta/MonadSimp.lean

@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Expr
+public section
+namespace Lean.Meta
+/-!
+Abstract simplifier API
+-/
+
+inductive MonadSimp.Result where
+  | rfl
+  | step (e : Expr) (h : Expr)
+  deriving Inhabited
+
+class MonadSimp (m : Type → Type) where
+  withNewLemmas (xs : Array Expr) (k : m α) : m α
+  dsimp : Expr → m Expr
+  simp : Expr → m MonadSimp.Result
+
+end Lean.Meta

src/Lean/Meta/Sym/AlphaShareBuilder.lean

@@ -144,4 +144,37 @@ def mkHaveS (x : Name) (t : Expr) (v : Expr) (b : Expr) : m Expr := do
     assertShared b
   share1 <| .letE x t v b true
 
+@[inline] def _root_.Lean.Expr.updateAppS! (e : Expr) (newFn : Expr) (newArg : Expr) : m Expr := do
+  let .app fn arg := e | panic! "application expected"
+  if isSameExpr fn newFn && isSameExpr arg newArg then return e else mkAppS newFn newArg
+
+@[inline] def _root_.Lean.Expr.updateMDataS! (e : Expr) (newExpr : Expr) : m Expr := do
+  let .mdata d a := e | panic! "mdata expected"
+  if isSameExpr a newExpr then return e else mkMDataS d newExpr
+
+@[inline] def _root_.Lean.Expr.updateProjS! (e : Expr) (newExpr : Expr) : m Expr := do
+  let .proj s i a := e | panic! "proj expected"
+  if isSameExpr a newExpr then return e else mkProjS s i newExpr
+
+@[inline] def _root_.Lean.Expr.updateForallS! (e : Expr) (newDomain : Expr) (newBody : Expr) : m Expr := do
+  let .forallE n d b bi := e | panic! "forall expected"
+  if isSameExpr d newDomain && isSameExpr b newBody then
+    return e
+  else
+    mkForallS n bi newDomain newBody
+
+@[inline] def _root_.Lean.Expr.updateLambdaS! (e : Expr) (newDomain : Expr) (newBody : Expr) : m Expr := do
+  let .lam n d b bi := e | panic! "lambda expected"
+  if isSameExpr d newDomain && isSameExpr b newBody then
+    return e
+  else
+    mkLambdaS n bi newDomain newBody
+
+@[inline] def _root_.Lean.Expr.updateLetS! (e : Expr) (newType : Expr) (newVal : Expr) (newBody : Expr) : m Expr := do
+  let .letE n t v b nondep := e | panic! "let expression expected"
+  if isSameExpr t newType && isSameExpr v newVal && isSameExpr b newBody then
+    return e
+  else
+    mkLetS n newType newVal newBody nondep
+
 end Lean.Meta.Sym.Internal

src/Lean/Meta/Sym/InstantiateS.lean

@@ -165,34 +165,39 @@ where
       if let some r := (← get)[key]? then
         return r
       else
-        save key (← mkAppS (← visitAppDefault f offset) (← visitChild a offset))
+        save key (← e.updateAppS! (← visitAppDefault f offset) (← visitChild a offset))
     | e => visitChild e offset
 
-  visitAppBeta (f : Expr) (argsRev : Array Expr) (offset : Nat) : M Expr := do
+  visitAppBeta (e : Expr) (f : Expr) (argsRev : Array Expr) (offset : Nat) (modified : Bool) : M Expr := do
     match f with
-    | .app f a => visitAppBeta f (argsRev.push (← visitChild a offset)) offset
+    | .app f a =>
+      let a' ← visitChild a offset
+      visitAppBeta e f (argsRev.push a') offset (modified || !isSameExpr a a')
     | .bvar bidx =>
-      let f ← visitBVar f bidx offset
-      betaRevS f argsRev
+      let f' ← visitBVar f bidx offset
+      if modified || !isSameExpr f f' then
+        betaRevS f' argsRev
+      else
+        return e
     | _ => unreachable!
 
-  visitApp (f : Expr) (arg : Expr) (offset : Nat) : M Expr := do
-    let arg ← visitChild arg offset
+  visitApp (e : Expr) (f : Expr) (arg : Expr) (offset : Nat) (_ : e = .app f arg) : M Expr := do
+    let arg' ← visitChild arg offset
     if f.getAppFn.isBVar then
-      visitAppBeta f #[arg] offset
+      visitAppBeta e f #[arg'] offset (!isSameExpr arg arg')
     else
-      mkAppS (← visitAppDefault f offset) arg
+      e.updateAppS! (← visitAppDefault f offset) arg'
 
   visit (e : Expr) (offset : Nat) : M Expr := do
-    match e with
+    match h : e with
     | .lit _ | .mvar _ | .fvar _ | .const _ _ | .sort _ => unreachable!
     | .bvar bidx => visitBVar e bidx offset
-    | .app f a => visitApp f a offset
-    | .mdata m a => mkMDataS m (← visitChild a offset)
-    | .proj s i a => mkProjS s i (← visitChild a offset)
-    | .forallE n d b bi => mkForallS n bi (← visitChild d offset) (← visitChild b (offset+1))
-    | .lam n d b bi => mkLambdaS n bi (← visitChild d offset) (← visitChild b (offset+1))
-    | .letE n t v b d => mkLetS n (← visitChild t offset) (← visitChild v offset) (← visitChild b (offset+1)) (nondep := d)
+    | .app f a => visitApp e f a offset h
+    | .mdata _ a => e.updateMDataS! (← visitChild a offset)
+    | .proj _ _ a => e.updateProjS! (← visitChild a offset)
+    | .forallE _ d b _ => e.updateForallS! (← visitChild d offset) (← visitChild b (offset+1))
+    | .lam _ d b _ => e.updateLambdaS! (← visitChild d offset) (← visitChild b (offset+1))
+    | .letE _ t v b _ => e.updateLetS! (← visitChild t offset) (← visitChild v offset) (← visitChild b (offset+1))
 
 /--
 Similar to `instantiateRevS`, but beta-reduces nested applications whose function becomes a lambda

src/Lean/Meta/Sym/ReplaceS.lean

@@ -33,12 +33,12 @@ mutual
 @[specialize] def visit (e : Expr) (offset : Nat) (fn : Expr → Nat → AlphaShareBuilderM (Option Expr)) : M Expr := do
   match e with
   | .lit _ | .mvar _ | .bvar _ | .fvar _ | .const _ _ | .sort _ => unreachable!
-  | .app f a => mkAppS (← visitChild f offset fn) (← visitChild a offset fn)
-  | .mdata m a => mkMDataS m (← visitChild a offset fn)
-  | .proj s i a => mkProjS s i (← visitChild a offset fn)
-  | .forallE n d b bi => mkForallS n bi (← visitChild d offset fn) (← visitChild b (offset+1) fn)
-  | .lam n d b bi => mkLambdaS n bi (← visitChild d offset fn) (← visitChild b (offset+1) fn)
-  | .letE n t v b d => mkLetS n (← visitChild t offset fn) (← visitChild v offset fn) (← visitChild b (offset+1) fn) (nondep := d)
+  | .app f a => e.updateAppS! (← visitChild f offset fn) (← visitChild a offset fn)
+  | .mdata _ a => e.updateMDataS! (← visitChild a offset fn)
+  | .proj _ _ a => e.updateProjS! (← visitChild a offset fn)
+  | .forallE _ d b _ => e.updateForallS! (← visitChild d offset fn) (← visitChild b (offset+1) fn)
+  | .lam _ d b _ => e.updateLambdaS! (← visitChild d offset fn) (← visitChild b (offset+1) fn)
+  | .letE _ t v b _ => e.updateLetS! (← visitChild t offset fn) (← visitChild v offset fn) (← visitChild b (offset+1) fn)
 end
 
 /--

src/Lean/Meta/Sym/Simp/Funext.lean

@@ -7,7 +7,10 @@ module
 prelude
 public import Lean.Meta.Basic
 import Lean.Meta.InferType
+import Lean.Meta.Closure
+import Lean.Meta.AppBuilder
 namespace Lean.Meta.Sym.Simp
+
 /--
 Given `xs` containing free variables
 `(x₁ : α₁) (x₂ : α₂[x₁]) ... (xₙ : αₙ[x₁, ..., x_{n-1}])`
@@ -24,31 +27,67 @@ This auxiliary theorem is used by the simplifier when visiting lambda expression
 public def mkFunextFor (xs : Array Expr) (β : Expr) : MetaM Expr := do
   let type ← mkForallFVars xs β
   let v ← getLevel β
+  let w ← getLevel type
   withLocalDeclD `f type fun f =>
   withLocalDeclD `g type fun g => do
-  let lhs := mkAppN f xs
-  let rhs := mkAppN g xs
-  let p := mkApp3 (mkConst ``Eq [v]) β lhs rhs
-  let p ← mkForallFVars xs p
-  withLocalDeclD `h p fun h => do
-  let mut result := mkAppN h xs |>.abstract xs
-  let mut i := xs.size
-  let mut β := β.abstract xs
-  let mut v := v
-  let mut f := mkAppN f xs |>.abstract xs
-  let mut g := mkAppN g xs |>.abstract xs
-  while i > 0 do
-    i := i - 1
-    let x := xs[i]!
-    let α_i ← inferType x
-    let u_i ← getLevel α_i
-    let α_i := α_i.abstractRange i xs
-    f := f.appFn!.lowerLooseBVars 1 1
-    g := g.appFn!.lowerLooseBVars 1 1
-    result := mkLambda `x default α_i result
-    result := mkApp5 (mkConst ``funext [u_i, v]) α_i (mkLambda `x .default α_i β) f g result
-    β := mkForall `x .default α_i β
-    v := mkLevelIMax' u_i v
-  mkLambdaFVars #[f, g, h] result
+  let eq := mkApp3 (mkConst ``Eq [v]) β (mkAppN f xs) (mkAppN g xs)
+  withLocalDeclD `h (← mkForallFVars xs eq) fun h => do
+  let eqv ← mkLambdaFVars #[f, g] (← mkForallFVars xs eq)
+  let quotEqv := mkApp2 (mkConst ``Quot [w]) type eqv
+  withLocalDeclD `f' quotEqv fun f' => do
+  let lift := mkApp6 (mkConst ``Quot.lift [w, v]) type eqv β
+    (mkLambda `f .default type (mkAppN (.bvar 0) xs))
+    (mkLambda `f .default type (mkLambda `g .default type (mkLambda `h .default (mkApp2 eqv (.bvar 1) (.bvar 0)) (mkAppN (.bvar 0) xs))))
+    f'
+  let extfunAppVal ← mkLambdaFVars (#[f'] ++ xs) lift
+  let extfunApp := extfunAppVal
+  let quotSound := mkApp5 (mkConst ``Quot.sound [w]) type eqv f g h
+  let Quot_mk_f := mkApp3 (mkConst ``Quot.mk [w]) type eqv f
+  let Quot_mk_g := mkApp3 (mkConst ``Quot.mk [w]) type eqv g
+  let result := mkApp6 (mkConst ``congrArg [w, w]) quotEqv type Quot_mk_f Quot_mk_g extfunApp quotSound
+  let result ← mkLambdaFVars #[f, g, h] result
+  return result
+
+/--
+Given `xs` containing free variables
+`(x₁ : α₁) (x₂ : α₂[x₁]) ... (xₙ : αₙ[x₁, ..., x_{n-1}])`,
+creates the custom forall congruence theorem
+```
+∀ (p q : (x₁ : α₁) → (x₂ : α₂[x₁]) → ... → (xₙ : αₙ[x₁, ..., x_{n-1}]) → Prop)
+  (h : ∀ x₁ ... xₙ, p x₁ ... xₙ = q x₁ ... xₙ),
+  (∀ x₁ ... xₙ, p x₁ ... xₙ) = (∀ x₁ ... xₙ, q x₁ ... xₙ)
+```
+The theorem has three arguments `p`, `q`, and `h`.
+This auxiliary theorem is used by the simplifier when visiting forall expressions.
+The proof uses the approach used in `mkFunextFor` followed by an `Eq.ndrec`.
+-/
+public def mkForallCongrFor (xs : Array Expr) : MetaM Expr := do
+  let prop := mkSort 0
+  let type ← mkForallFVars xs prop
+  let w ← getLevel type
+  withLocalDeclD `p type fun p =>
+  withLocalDeclD `q type fun q => do
+  let eq := mkApp3 (mkConst ``Eq [1]) prop (mkAppN p xs) (mkAppN q xs)
+  withLocalDeclD `h (← mkForallFVars xs eq) fun h => do
+  let eqv ← mkLambdaFVars #[p, q] (← mkForallFVars xs eq)
+  let quotEqv := mkApp2 (mkConst ``Quot [w]) type eqv
+  withLocalDeclD `p' quotEqv fun p' => do
+  let lift := mkApp6 (mkConst ``Quot.lift [w, 1]) type eqv prop
+    (mkLambda `p .default type (mkAppN (.bvar 0) xs))
+    (mkLambda `p .default type (mkLambda `q .default type (mkLambda `h .default (mkApp2 eqv (.bvar 1) (.bvar 0)) (mkAppN (.bvar 0) xs))))
+    p'
+  let extfunAppVal ← mkLambdaFVars (#[p'] ++ xs) lift
+  let extfunApp := extfunAppVal
+  let quotSound := mkApp5 (mkConst ``Quot.sound [w]) type eqv p q h
+  let Quot_mk_p := mkApp3 (mkConst ``Quot.mk [w]) type eqv p
+  let Quot_mk_q := mkApp3 (mkConst ``Quot.mk [w]) type eqv q
+  let p_eq_q := mkApp6 (mkConst ``congrArg [w, w]) quotEqv type Quot_mk_p Quot_mk_q extfunApp quotSound
+  let lhs ← mkForallFVars xs (mkAppN p xs)
+  let rhs ← mkForallFVars xs (mkAppN q xs)
+  let motive ← mkLambdaFVars #[q] (mkApp3 (mkConst ``Eq [1]) prop lhs rhs)
+  let rfl := mkApp2 (mkConst ``Eq.refl [1]) prop lhs
+  let result := mkApp6 (mkConst ``Eq.ndrec [0, w]) type p motive rfl q p_eq_q
+  let result ← mkLambdaFVars #[p, q, h] result
+  return result
 
 end Lean.Meta.Sym.Simp

src/Lean/Meta/Sym/Simp/Main.lean

@@ -6,6 +6,8 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Sym.Simp.SimpM
+import Lean.Meta.MonadSimp
+import Lean.Meta.HaveTelescope
 import Lean.Meta.Sym.AlphaShareBuilder
 import Lean.Meta.Sym.InferType
 import Lean.Meta.Sym.Simp.Result
@@ -15,14 +17,19 @@ import Lean.Meta.Sym.Simp.Funext
 namespace Lean.Meta.Sym.Simp
 open Internal
 
+instance : MonadSimp SimpM where
+  dsimp e := return e
+  withNewLemmas _ k := k
+  simp e := do match (← simp (← share e)) with
+    | .rfl _ => return .rfl
+    | .step e' h _ => return .step e' h
+
 def simpLambda (e : Expr) : SimpM Result := do
-  -- **TODO**: Add free variable reuse
   lambdaTelescope e fun xs b => do
     match (← simp b) with
     | .rfl _ => return .rfl
     | .step b' h _ =>
       let h ← mkLambdaFVars xs h
-      -- **TODO**: Add `mkLambdaFVarsS`?
       let e' ← shareCommonInc (← mkLambdaFVars xs b')
       let funext ← getFunext xs b
       return .step e' (mkApp3 funext e e' h)
@@ -37,13 +44,61 @@ where
       modify fun s => { s with funext := s.funext.insert { expr := key } h }
       return h
 
-def simpForall (_ : Expr) : SimpM Result := do
-  -- **TODO**
-  return .rfl
+def simpArrow (e : Expr) : SimpM Result := do
+  let p := e.bindingDomain!
+  let q := e.bindingBody!
+  match (← simp p), (← simp q) with
+  | .rfl _, .rfl _ =>
+    return .rfl
+  | .step p' h _, .rfl _ =>
+    let u ← getLevel p
+    let v ← getLevel q
+    let e' ← e.updateForallS! p' q
+    return .step e' <| mkApp4 (mkConst ``implies_congr_left [u, v]) p p' q h
+  | .rfl _, .step q' h _ =>
+    let u ← getLevel p
+    let v ← getLevel q
+    let e' ← e.updateForallS! p q'
+    return .step e' <| mkApp4 (mkConst ``implies_congr_right [u, v]) p q q' h
+  | .step p' h₁ _, .step q' h₂ _ =>
+    let u ← getLevel p
+    let v ← getLevel q
+    let e' ← e.updateForallS! p' q'
+    return .step e' <| mkApp6 (mkConst ``implies_congr [u, v]) p p' q q' h₁ h₂
 
-def simpLet (_ : Expr) : SimpM Result := do
-  -- **TODO**
-  return .rfl
+def simpForall (e : Expr) : SimpM Result := do
+  if e.isArrow then
+    simpArrow e
+  else if (← isProp e) then
+    let n := getForallTelescopeSize e.bindingBody! 1
+    forallBoundedTelescope e n fun xs b => do
+    match (← simp b) with
+    | .rfl _ => return .rfl
+    | .step b' h _ =>
+      let h ← mkLambdaFVars xs h
+      let e' ← shareCommonInc (← mkForallFVars xs b')
+      -- **Note**: consider caching the forall-congr theorems
+      let hcongr ← mkForallCongrFor xs
+      return .step e' (mkApp3 hcongr (← mkLambdaFVars xs b) (← mkLambdaFVars xs b') h)
+  else
+    return .rfl
+where
+  -- **Note**: Optimize if this is quadratic in practice
+  getForallTelescopeSize (e : Expr) (n : Nat) : Nat :=
+    match e with
+    | .forallE _ _ b _ => if b.hasLooseBVar 0 then getForallTelescopeSize b (n+1) else n
+    | _ => n
+
+def simpLet (e : Expr) : SimpM Result := do
+  if !e.letNondep! then
+    /-
+    **Note**: We don't do anything if it is a dependent `let`.
+    Users may decide to `zeta`-expand them or apply `letToHave` at `pre`/`post`.
+    -/
+    return .rfl
+  else match (← Meta.simpHaveTelescope e) with
+    | .rfl => return .rfl
+    | .step e' h => return .step (← shareCommon e') h
 
 def simpApp (e : Expr) : SimpM Result := do
   congrArgs e

src/Lean/Meta/Tactic/Congr.lean

@@ -51,13 +51,6 @@ def MVarId.congr? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
     let some congrThm ← mkCongrSimp? lhs.getAppFn (subsingletonInstImplicitRhs := false) (maxArgs? := lhs.getAppNumArgs) | return none
     applyCongrThm? mvarId congrThm
 
-/--
-Try to apply a `simp` congruence theorem and throw an error if it fails.
--/
-def MVarId.congr (mvarId : MVarId) : MetaM (List MVarId) := do
-  let some mvarIds ← mvarId.congr? | throwError "Failed to apply `simp` congruence theorem"
-  return mvarIds
-
 /--
 Try to apply a `hcongr` congruence theorem, and then tries to close resulting goals
 using `Eq.refl`, `HEq.refl`, and assumption.

src/Lean/Meta/Tactic/Grind.lean

@@ -101,5 +101,7 @@ builtin_initialize registerTraceClass `grind.debug.proveEq
 builtin_initialize registerTraceClass `grind.debug.pushNewFact
 builtin_initialize registerTraceClass `grind.debug.appMap
 builtin_initialize registerTraceClass `grind.debug.ext
+builtin_initialize registerTraceClass `grind.debug.suggestions
+builtin_initialize registerTraceClass `grind.debug.locals
 
 end Lean

src/Lean/Meta/Tactic/LibrarySearch.lean

@@ -13,6 +13,7 @@ public import Lean.Util.Heartbeats
 import Init.Grind.Util
 import Init.Try
 import Lean.Elab.Tactic.Basic
+import Lean.Linter.Deprecated
 
 public section
 
@@ -83,9 +84,8 @@ def tryDischarger (mvarId : MVarId) : MetaM (Option (List MVarId)) := do
     let tacStx ← `(tactic| try?)
     let remainingGoals ← Elab.Term.TermElabM.run' <| Elab.Tactic.run subgoal do
       -- Suppress info messages from try?
-      let initialLog ← Core.getMessageLog
-      Elab.Tactic.evalTactic tacStx
-      Core.setMessageLog initialLog
+      Elab.Tactic.withSuppressedMessages do
+        Elab.Tactic.evalTactic tacStx
     if remainingGoals.isEmpty then
       return some []
     else
@@ -138,7 +138,9 @@ to find candidate lemmas.
 open LazyDiscrTree (InitEntry findMatches)
 
 private def addImport (name : Name) (constInfo : ConstantInfo) :
-    MetaM (Array (InitEntry (Name × DeclMod))) :=
+    MetaM (Array (InitEntry (Name × DeclMod))) := do
+  -- Don't report deprecated lemmas.
+  if Linter.isDeprecated (← getEnv) name then return #[]
   -- Don't report lemmas from metaprogramming namespaces.
   if name.isMetaprogramming then return #[] else
   forallTelescope constInfo.type fun _ type => do

src/Lean/Meta/Tactic/Refl.lean

@@ -62,13 +62,4 @@ def _root_.Lean.MVarId.hrefl (mvarId : MVarId) : MetaM Unit := do
     let some [] ← observing? do mvarId.apply (mkConst ``HEq.refl [← mkFreshLevelMVar])
       | throwTacticEx `hrefl mvarId
 
-/--
-Close given goal using `Subsingleton.helim`.
--/
-def _root_.Lean.MVarId.helim (mvarId : MVarId) : MetaM (List MVarId) :=
-  mvarId.withContext do
-    let some subGoals ← observing? do mvarId.apply (mkConst ``Subsingleton.helim [← mkFreshLevelMVar])
-      | throwTacticEx `hrefl mvarId
-    return subGoals
-
 end Lean.Meta

src/Lean/Meta/Tactic/Rewrites.lean

@@ -13,6 +13,7 @@ public import Lean.Meta.Tactic.Refl
 public import Lean.Meta.Tactic.SolveByElim
 public import Lean.Meta.Tactic.TryThis
 public import Lean.Util.Heartbeats
+import Lean.Linter.Deprecated
 
 public section
 
@@ -47,6 +48,8 @@ private def addImport (name : Name) (constInfo : ConstantInfo) :
     MetaM (Array (InitEntry (Name × RwDirection))) := do
   if constInfo.isUnsafe then return #[]
   if !allowCompletion (←getEnv) name then return #[]
+  -- Don't report deprecated lemmas.
+  if Linter.isDeprecated (← getEnv) name then return #[]
   -- We now remove some injectivity lemmas which are not useful to rewrite by.
   match name with
   | .str _ n => if n = "injEq" ∨ n = "sizeOf_spec" ∨ n.endsWith "_inj" ∨ n.endsWith "_inj'" then return #[]

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -4,18 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Replace
 public import Lean.Meta.Tactic.Simp.Rewrite
 public import Lean.Meta.Tactic.Simp.Diagnostics
 public import Lean.Meta.Match.Value
+public import Lean.Meta.MonadSimp
 public import Lean.Util.CollectLooseBVars
+import Lean.Meta.HaveTelescope
 import Lean.PrettyPrinter
 import Lean.ExtraModUses
-
 public section
-
 namespace Lean.Meta
 namespace Simp
 
@@ -263,6 +262,16 @@ def withNewLemmas {α} (xs : Array Expr) (f : SimpM α) : SimpM α := do
   else
     withFreshCache do f
 
+instance : MonadSimp SimpM where
+  simp e := do
+    let r ← simp e
+    if r.expr == e then
+      return .rfl
+    else
+      return .step r.expr (← r.getProof)
+  dsimp := dsimp
+  withNewLemmas := withNewLemmas
+
 def simpProj (e : Expr) : SimpM Result := do
   match (← withSimpMetaConfig <| reduceProj? e) with
   | some e => return { expr := e }
@@ -378,393 +387,17 @@ def simpForall (e : Expr) : SimpM Result := withParent e do
   else
     return { expr := (← dsimp e) }
 
-/--
-Information about a single `have` in a `have` telescope.
-Created by `getHaveTelescopeInfo`.
--/
-structure HaveInfo where
-  /-- Previous `have`s that the type of this `have` depends on, as indices into `HaveTelescopeInfo.haveInfo`.
-  Used in `computeFixedUsed` to compute used `have`s. -/
-  typeBackDeps : Std.HashSet Nat
-  /-- Previous `have`s that the value of this `have` depends on, as indices into `HaveTelescopeInfo.haveInfo`.
-  Used in `computeFixedUsed` to compute used `have`s. -/
-  valueBackDeps : Std.HashSet Nat
-  /-- The local decl for the `have`, so that the local context can be re-entered `have`-by-`have`.
-  N.B. This stores the fvarid for the `have` as well as cached versions of the value and type
-  instantiated with the fvars from the telescope. -/
-  decl : LocalDecl
-  /-- The level of the type for this `have`, cached. -/
-  level : Level
-  deriving Inhabited
-
-/--
-Information about a `have` telescope.
-Created by `getHaveTelescopeInfo` and used in `simpHaveTelescope`.
-
-The data is used to avoid applying `Expr.abstract` more than once on any given subexpression
-when constructing terms and proofs during simplification. Abstraction is linear in the size `t` of a term,
-and so in a depth-`n` telescope it is `O(nt)`, quadratic in `n`, since `n ≤ t`.
-For example, given `have x₁ := v₁; ...; have xₙ := vₙ; b` and `h : b = b'`, we need to construct
-```lean
-have_body_congr (fun x₁ => ... have_body_congr (fun xₙ => h)))
-```
-We apply `Expr.abstract` to `h` *once* and then build the term, rather than
-using `mkLambdaFVars #[fvarᵢ] pfᵢ` at each step.
-
-As an additional optimization, we save the fvar-instantiated terms calculated by `getHaveTelescopeInfo`
-so that we don't have to compute them again. This is only saving a constant factor.
-
-It is also used for computing used `have`s in `computeFixedUsed`.
-In `have x₁ := v; have x₂ := x₁; ⋯; have xₙ := xₙ₋₁; b`, if `xₙ` is unused in `b`, then all the
-`have`s are unused. Without a global computation of used `have`s, the proof term would be quadratic
-in the number of `have`s (with `n` iterations of `simp`). Knowing which `have`s are transitively
-unused lets the proof term be linear in size.
--/
-structure HaveTelescopeInfo where
-  /-- Information about each `have` in the telescope. -/
-  haveInfo : Array HaveInfo := #[]
-  /-- The set of `have`s that the body depends on, as indices into `haveInfo`.
-  Used in `computeFixedUsed` to compute used `have`s. -/
-  bodyDeps : Std.HashSet Nat := {}
-  /-- The set of `have`s that the type of the body depends on, as indices into `haveInfo`.
-  This is the set of fixed `have`s. -/
-  bodyTypeDeps : Std.HashSet Nat := {}
-  /-- A cached version of the telescope body, instantiated with fvars from each `HaveInfo.decl`. -/
-  body : Expr := Expr.const `_have_telescope_info_dummy_ []
-  /-- A cached version of the telescope body's type, instantiated with fvars from each `HaveInfo.decl`. -/
-  bodyType : Expr := Expr.const `_have_telescope_info_dummy_ []
-  /-- The universe level for the `have` expression, cached. -/
-  level : Level := Level.param `_have_telescope_info_dummy_
-  deriving Inhabited
-
-/--
-Efficiently collect dependency information for a `have` telescope.
-This is part of a scheme to avoid quadratic overhead from the locally nameless discipline
-(see `HaveTelescopeInfo` and `simpHaveTelescope`).
-
-The expression `e` must not have loose bvars.
--/
-def getHaveTelescopeInfo (e : Expr) : MetaM HaveTelescopeInfo := do
-  collect e 0 {} (← getLCtx) #[]
-where
-  collect (e : Expr) (numHaves : Nat) (info : HaveTelescopeInfo) (lctx : LocalContext) (fvars : Array Expr) : MetaM HaveTelescopeInfo := do
-    /-
-    Gives indices into `fvars` that the uninstantiated expression `a` depends on, from collecting its bvars.
-    This is more efficient than collecting `fvars` from an instantiated expression,
-    since the expression likely contains many fvars for the pre-existing local context.
-    -/
-    let getBackDeps (a : Expr) : Std.HashSet Nat :=
-      a.collectLooseBVars.fold (init := {}) fun deps vidx =>
-        -- Since the original expression has no bvars, `vidx < numHaves` must be true.
-        deps.insert (numHaves - vidx - 1)
-    match e with
-    | .letE n t v b true =>
-      let typeBackDeps := getBackDeps t
-      let valueBackDeps := getBackDeps v
-      let t := t.instantiateRev fvars
-      let v := v.instantiateRev fvars
-      let level ← withLCtx' lctx <| getLevel t
-      let fvarId ← mkFreshFVarId
-      let decl := LocalDecl.ldecl 0 fvarId n t v true .default
-      let info := { info with haveInfo := info.haveInfo.push { typeBackDeps, valueBackDeps, decl, level } }
-      let lctx := lctx.addDecl decl
-      let fvars := fvars.push (mkFVar fvarId)
-      collect b (numHaves + 1) info lctx fvars
-    | _ =>
-      let bodyDeps := getBackDeps e
-      withLCtx' lctx do
-        let body := e.instantiateRev fvars
-        let bodyType ← inferType body
-        let level ← getLevel bodyType
-        -- Collect fvars appearing in the type of `e`. Computing `bodyType` in particular is where `MetaM` is necessary.
-        let bodyTypeFVarIds := (collectFVars {} bodyType).fvarSet
-        let bodyTypeDeps : Std.HashSet Nat := Nat.fold fvars.size (init := {}) fun idx _ deps =>
-          if bodyTypeFVarIds.contains fvars[idx].fvarId! then
-            deps.insert idx
-          else
-            deps
-        return { info with bodyDeps, bodyTypeDeps, body, bodyType, level }
-
-/--
-Computes which `have`s in the telescope are fixed and which are unused.
-The length of the unused array may be less than the number of `have`s: use `unused.getD i true`.
--/
-def HaveTelescopeInfo.computeFixedUsed (info : HaveTelescopeInfo) (keepUnused : Bool) :
-    MetaM (Array Bool × Array Bool) := do
-  let fixed ← go info.bodyTypeDeps
-  if keepUnused then
-    return (fixed, #[])
-  else
-    let used ← go info.bodyDeps
-    return (fixed, used)
-where
-  updateArrayFromBackDeps (arr : Array Bool) (s : Std.HashSet Nat) : Array Bool :=
-    s.fold (init := arr) fun arr idx => arr.set! idx true
-  go init : MetaM (Array Bool) := do
-    let numHaves := info.haveInfo.size
-    let mut used : Array Bool := Array.replicate numHaves false
-    -- Initialize `used` with the body's dependencies.
-    -- There is no need to consider `info.bodyTypeDeps` in this computation.
-    used := updateArrayFromBackDeps used init
-    -- For each used `have`, in reverse order, update `used`.
-    for i in *...numHaves do
-      let idx := numHaves - i - 1
-      if used[idx]! then
-        let hinfo := info.haveInfo[idx]!
-        used := updateArrayFromBackDeps used hinfo.typeBackDeps
-        used := updateArrayFromBackDeps used hinfo.valueBackDeps
-    return used
-
-/--
-Auxiliary structure used to represent the return value of `simpHaveTelescopeAux`.
-See `simpHaveTelescope` for an overview and `HaveTelescopeInfo` for an example.
--/
-private structure SimpHaveResult where
-  /--
-  The simplified expression in `(fun x => b) v` form. Note that it may contain loose bound variables.
-  `simpHaveTelescope` attempts to minimize the quadratic overhead imposed
-  by the locally nameless discipline in a sequence of `have` expressions.
-  -/
-  expr     : Expr
-  /--
-  The type of `expr`. It may contain loose bound variables like in the `expr` field.
-  Used in proof construction.
-  -/
-  exprType : Expr
-  /--
-  The initial expression in `(fun x => b) v` form.
-  -/
-  exprInit   : Expr
-  /--
-  The expression `expr` in `have x := v; b` form.
-  -/
-  exprResult : Expr
-  /--
-  The proof that the simplified expression is equal to the input one.
-  It may contain loose bound variables like in the `expr` field.
-  -/
-  proof    : Expr
-  /--
-  `modified := false` iff `expr` is structurally equal to the input expression.
-  When false, `proof` is `Eq.refl`.
-  -/
-  modified : Bool
-
-private def SimpHaveResult.toResult (u : Level) (source : Expr) : SimpHaveResult → Result
-  | { expr, exprType, exprInit, exprResult, proof, modified, .. } =>
-    { expr := exprResult
-      proof? :=
-        if modified then
-          -- Add a type hint to convert back into `have` form.
-          some <| mkExpectedPropHint (expectedProp := mkApp3 (mkConst ``Eq [u]) exprType source exprResult) <|
-            -- Add in a second type hint, for use in an optimization to avoid zeta/beta reductions in the kernel
-            -- The base case in `simpHaveTelescopeAux` detects this construction and uses `exprType`/`exprInit`
-            -- to construct the `SimpHaveResult`.
-            -- If the kernel were to support `have` forms of the congruence lemmas this would not be necessary.
-            mkExpectedPropHint (expectedProp := mkApp3 (mkConst ``Eq [u]) exprType exprInit expr) proof
-        else
-          none }
-
-/--
-Routine for simplifying `have` telescopes. Used by `simpLet`.
-This is optimized to be able to handle deep `have` telescopes while avoiding quadratic complexity
-arising from the locally nameless expression representations.
-
-## Overview
-
-Consider a `have` telescope:
-```
-have x₁ : T₁ := v₁; ...; have xₙ : Tₙ := vₙ; b
-```
-We say `xᵢ` is *fixed* if it appears in the type of `b`.
-If `xᵢ` is fixed, then it can only be rewritten using definitional equalities.
-Otherwise, we can freely rewrite the value using a propositional equality `vᵢ = vᵢ'`.
-The body `b` can always be freely rewritten using a propositional equality `b = b'`.
-(All the mentioned equalities must be type correct with respect to the obvious local contexts.)
-
-If `xᵢ` neither appears in `b` nor any `Tⱼ` nor any `vⱼ`, then its `have` is *unused*.
-Unused `have`s can be eliminated, which we do if `cfg.zetaUnused` is true.
-We clear `have`s from the end, to be able to transitively clear chains of unused `have`s.
-This is why we honor `zetaUnused` here even though `reduceStep` is also responsible for it;
-`reduceStep` can only eliminate unused `have`s at the start of a telescope.
-Eliminating all transitively unused `have`s at once like this also avoids quadratic complexity.
-
-If `debug.simp.check.have` is enabled then we typecheck the resulting expression and proof.
-
-## Proof generation
-
-There are two main complications with generating proofs.
-1. We work almost exclusively with expressions with loose bound variables,
-   to avoid overhead from instantiating and abstracting free variables,
-   which can lead to complexity quadratic in the telescope length.
-   (See `HaveTelescopeInfo`.)
-2. We want to avoid triggering zeta reductions in the kernel.
-
-Regarding this second point, the issue is that we cannot organize the proof using congruence theorems
-in the obvious way. For example, given
-```
-theorem have_congr {α : Sort u} {β : Sort v} {a a' : α} {f f' : α → β}
-    (h₁ : a = a') (h₂ : ∀ x, f x = f' x) :
-    (have x := a; f x) = (have x := a'; f' x)
-```
-the kernel sees that the type of `have_congr (fun x => b) (fun x => b') h₁ h₂`
-is `(have x := a; (fun x => b) x) = (have x := a'; (fun x => b') x)`,
-since when instantiating values it does not beta reduce at the same time.
-Hence, when `is_def_eq` is applied to the LHS and `have x := a; b` for example,
-it will do `whnf_core` to both sides.
-
-Instead, we use the form `(fun x => b) a = (fun x => b') a'` in the proofs,
-which we can reliably match up without triggering beta reductions in the kernel.
-The zeta/beta reductions are then limited to the type hint for the entire telescope,
-when we convert this back into `have` form.
-In the base case, we include an optimization to avoid unnecessary zeta/beta reductions,
-by detecting a `simpHaveTelescope` proofs and removing the type hint.
--/
+/-- Adapter for `Meta.simpHaveTelescope` -/
 def simpHaveTelescope (e : Expr) : SimpM Result := do
-  Prod.fst <$> withTraceNode `Debug.Meta.Tactic.simp (fun
-      | .ok (_, used, fixed, modified) => pure m!"{checkEmoji} have telescope; used: {used}; fixed: {fixed}; modified: {modified}"
-      | .error ex => pure m!"{crossEmoji} {ex.toMessageData}") do
-    let info ← getHaveTelescopeInfo e
-    assert! !info.haveInfo.isEmpty
-    let (fixed, used) ← info.computeFixedUsed (keepUnused := !(← getConfig).zetaUnused)
-    let r ← simpHaveTelescopeAux info fixed used e 0 (Array.mkEmpty info.haveInfo.size)
-    if r.modified && debug.simp.check.have.get (← getOptions) then
-      check r.expr
-      check r.proof
-    return (r.toResult info.level e, used, fixed, r.modified)
-where
-  /-
-  Re-enters the telescope recorded in `info` using `withExistingLocalDecls` while simplifying according to `fixed`/`used`.
-  Note that we must use the low-level `Expr` APIs because the expressions may contain loose bound variables.
-  Note also that we don't enter the body's local context all at once, since we need to be sure that
-  when we simplify values they have their correct local context.
-  -/
-  simpHaveTelescopeAux (info : HaveTelescopeInfo) (fixed : Array Bool) (used : Array Bool) (e : Expr) (i : Nat) (xs : Array Expr) : SimpM SimpHaveResult := do
-    if h : i < info.haveInfo.size then
-      let hinfo := info.haveInfo[i]
-      -- `x` and `val` are the fvar and value with respect to the local context.
-      let x := hinfo.decl.toExpr
-      let val := hinfo.decl.value true
-      -- Invariant: `v == val.abstract xs`.
-      let .letE n t v b true := e | unreachable!
-      -- Universe levels to use for each of the `have_*` theorems. It's the level of `val` and the level of the body.
-      let us := [hinfo.level, info.level]
-      if !used.getD i true then
-        /-
-        Unused `have`: do not add `x` to the local context then `simp` only the body.
-        -/
-        trace[Debug.Meta.Tactic.simp] "have telescope; unused {n} := {val}"
-        /-
-        Complication: Unused `have`s might only be transitively unused.
-        This means that `b.hasLooseBVar 0` might actually be true.
-        This matters because `t` and `v` appear in the proof term.
-        We use a dummy `x` for debugging purposes. (Recall that `Expr.abstract` skips non-fvar/mvars.)
-        -/
-        let x := mkConst `_simp_let_unused_dummy
-        let rb ← simpHaveTelescopeAux info fixed used b (i + 1) (xs.push x)
-        -- TODO(kmill): This is a source of quadratic complexity. It might be possible to avoid this,
-        -- but we will need to carefully re-review the logic (note that `rb.proof` still refers to `x`).
-        let expr := rb.expr.lowerLooseBVars 1 1
-        let exprType := rb.exprType.lowerLooseBVars 1 1
-        let exprInit := mkApp (mkLambda n .default t rb.exprInit) v
-        let exprResult := rb.exprResult.lowerLooseBVars 1 1
-        if rb.modified then
-          let proof := mkApp6 (mkConst ``have_unused_dep' us) t exprType v (mkLambda n .default t rb.exprInit) expr
-            (mkLambda n .default t rb.proof)
-          return { expr, exprType, exprInit, exprResult, proof, modified := true }
-        else
-          -- If not modified, this must have been a non-transitively unused `have`, so no need for `dep` form.
-          let proof := mkApp6 (mkConst ``have_unused' us) t exprType v expr expr
-            (mkApp2 (mkConst ``Eq.refl [info.level]) exprType expr)
-          return { expr, exprType, exprInit, exprResult, proof, modified := true }
-      else if fixed.getD i true then
-        /-
-        Fixed `have` (like `CongrArgKind.fixed`): dsimp the value and simp the body.
-        The variable appears in the type of the body.
-        -/
-        let val' ← dsimp val
-        trace[Debug.Meta.Tactic.simp] "have telescope; fixed {n} := {val} => {val'}"
-        let vModified := val != val'
-        let v' := if vModified then val'.abstract xs else v
-        withExistingLocalDecls [hinfo.decl] <| withNewLemmas #[x] do
-          let rb ← simpHaveTelescopeAux info fixed used b (i + 1) (xs.push x)
-          let expr := mkApp (mkLambda n .default t rb.expr) v'
-          let exprType := mkApp (mkLambda n .default t rb.exprType) v'
-          let exprInit := mkApp (mkLambda n .default t rb.exprInit) v
-          let exprResult := mkHave n t v' rb.exprResult
-          -- Note: if `vModified`, then the kernel will reduce the telescopes and potentially do an expensive defeq check.
-          -- If this is a performance issue, we could try using a `letFun` encoding here make use of the `is_def_eq_args` optimization.
-          -- Namely, to guide the defeqs via the sequence
-          --   `(fun x => b) v` = `letFun (fun x => b) v` = `letFun (fun x => b) v'` = `(fun x => b) v'`
-          if rb.modified then
-            let proof := mkApp6 (mkConst ``have_body_congr_dep' us) t (mkLambda n .default t rb.exprType) v'
-              (mkLambda n .default t rb.exprInit) (mkLambda n .default t rb.expr) (mkLambda n .default t rb.proof)
-            return { expr, exprType, exprInit, exprResult, proof, modified := true }
-          else
-            let proof := mkApp2 (mkConst ``Eq.refl [info.level]) exprType expr
-            return { expr, exprType, exprInit, exprResult, proof, modified := vModified }
-      else
-        /-
-        Non-fixed `have` (like `CongrArgKind.eq`): simp both the value and the body.
-        The variable does not appear in the type of the body.
-        -/
-        let rval' ← simp val
-        trace[Debug.Meta.Tactic.simp] "have telescope; non-fixed {n} := {val} => {rval'.expr}"
-        let valModified := rval'.expr != val
-        let v' := if valModified then rval'.expr.abstract xs else v
-        let vproof ← if valModified then
-          pure <| (← rval'.getProof).abstract xs
-        else
-          pure <| mkApp2 (mkConst `Eq.refl [hinfo.level]) t v
-        withExistingLocalDecls [hinfo.decl] <| withNewLemmas #[x] do
-          let rb ← simpHaveTelescopeAux info fixed used b (i + 1) (xs.push x)
-          let expr := mkApp (mkLambda n .default t rb.expr) v'
-          assert! !rb.exprType.hasLooseBVar 0
-          let exprType := rb.exprType.lowerLooseBVars 1 1
-          let exprInit := mkApp (mkLambda n .default t rb.exprInit) v
-          let exprResult := mkHave n t v' rb.exprResult
-          match valModified, rb.modified with
-          | false, false =>
-            let proof := mkApp2 (mkConst `Eq.refl [info.level]) exprType expr
-            return { expr, exprType, exprInit, exprResult, proof, modified := false }
-          | true, false =>
-            let proof := mkApp6 (mkConst ``have_val_congr' us) t exprType v v'
-              (mkLambda n .default t rb.exprInit) vproof
-            return { expr, exprType, exprInit, exprResult, proof, modified := true }
-          | false, true =>
-            let proof := mkApp6 (mkConst ``have_body_congr' us) t exprType v
-              (mkLambda n .default t rb.exprInit) (mkLambda n .default t rb.expr) (mkLambda n .default t rb.proof)
-            return { expr, exprType, exprInit, exprResult, proof, modified := true }
-          | true, true =>
-            let proof := mkApp8 (mkConst ``have_congr' us) t exprType v v'
-              (mkLambda n .default t rb.exprInit) (mkLambda n .default t rb.expr) vproof (mkLambda n .default t rb.proof)
-            return { expr, exprType, exprInit, exprResult, proof, modified := true }
-    else
-      -- Base case: simplify the body.
-      trace[Debug.Meta.Tactic.simp] "have telescope; simplifying body {info.body}"
-      let r ← simp info.body
-      let exprType := info.bodyType.abstract xs
-      if r.expr == info.body then
-        let proof := mkApp2 (mkConst `Eq.refl [info.level]) exprType e
-        return { expr := e, exprType, exprInit := e, exprResult := e, proof, modified := false }
-      else
-        let expr := r.expr.abstract xs
-        let proof := (← r.getProof).abstract xs
-        -- Optimization: if the proof is a `simpHaveTelescope` proof, then remove the type hint
-        -- to avoid the zeta/beta reductions that the kernel would otherwise do.
-        -- In `SimpHaveResult.toResult` we insert two type hints; the inner one
-        -- encodes the `exprInit` and `expr`.
-        let detectSimpHaveLemma (proof : Expr) : Option SimpHaveResult := do
-          let_expr id eq proof' := proof | failure
-          guard <| eq.isAppOfArity ``Eq 3
-          let_expr id eq' proof'' := proof' | failure
-          let_expr Eq _ lhs rhs := eq' | failure
-          let .const n _ := proof''.getAppFn | failure
-          guard (n matches ``have_unused_dep' | ``have_unused' | ``have_body_congr_dep' | ``have_val_congr' | ``have_body_congr' | ``have_congr')
-          return { expr := rhs, exprType, exprInit := lhs, exprResult := expr, proof := proof'', modified := true }
-        if let some res := detectSimpHaveLemma proof then
-          return res
-        return { expr, exprType, exprInit := e, exprResult := expr, proof, modified := true }
+  -- **Note**: Eliminating unused-let declarations in a single pass may produce O(n^2) proofs.
+  let zetaUnusedMode := if (← getConfig).zetaUnused then .singlePass else .no
+  match (← Meta.simpHaveTelescope e zetaUnusedMode) with
+  | .rfl => return { expr := e }
+  | .step e' h =>
+    if debug.simp.check.have.get (← getOptions) then
+      check e'
+      check h
+    return { expr := e', proof? := h }
 
 /--
 Routine for simplifying `let` expressions.

src/LeanChecker.lean

@@ -0,0 +1,115 @@
+/-
+Copyright (c) 2023 Kim Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison, Sebastian Ullrich
+-/
+import Lean.CoreM
+import Lean.Replay
+import LeanChecker.Replay
+import Lake.Load.Manifest
+
+open Lean
+
+unsafe def replayFromImports (module : Name) : IO Unit := do
+  let mFile ← findOLean module
+  unless (← mFile.pathExists) do
+    throw <| IO.userError s!"object file '{mFile}' of module {module} does not exist"
+  -- Load all module data parts (exported, server, private)
+  let mut fnames := #[mFile]
+  let sFile := OLeanLevel.server.adjustFileName mFile
+  if (← sFile.pathExists) then
+    fnames := fnames.push sFile
+    let pFile := OLeanLevel.private.adjustFileName mFile
+    if (← pFile.pathExists) then
+      fnames := fnames.push pFile
+  let parts ← readModuleDataParts fnames
+  if h : parts.size = 0 then throw <| IO.userError "failed to read module data" else
+  let (mod, _) := parts[0]
+  let (_, s) ← importModulesCore mod.imports |>.run
+  let env ← finalizeImport s mod.imports {} 0 false false (isModule := true)
+  let mut newConstants := {}
+  -- Collect constants from last ("most private") part, which subsumes all prior ones
+  for name in parts[parts.size-1].1.constNames, ci in parts[parts.size-1].1.constants do
+    newConstants := newConstants.insert name ci
+  let env' ← env.replay' newConstants
+  env'.freeRegions
+
+unsafe def replayFromFresh (module : Name) : IO Unit := do
+  Lean.withImportModules #[{module}] {} fun env => do
+    discard <| (← mkEmptyEnvironment).replay' env.constants.map₁
+
+/-- Read the name of the main module from the `lake-manifest`. -/
+-- This has been copied from `ImportGraph.getCurrentModule` in the
+-- https://github.com/leanprover-community/import-graph repository.
+def getCurrentModule : IO Name := do
+  match (← Lake.Manifest.load? ⟨"lake-manifest.json"⟩) with
+  | none =>
+    -- TODO: should this be caught?
+    pure .anonymous
+  | some manifest =>
+    -- TODO: This assumes that the `package` and the default `lean_lib`
+    -- have the same name up to capitalisation.
+    -- Would be better to read the `.defaultTargets` from the
+    -- `← getRootPackage` from `Lake`, but I can't make that work with the monads involved.
+    return manifest.name.capitalize
+
+
+/--
+Run as e.g. `leanchecker` to check everything in the current project.
+or e.g. `leanchecker Mathlib.Data.Nat` to check everything with module name
+starting with `Mathlib.Data.Nat`.
+
+This will replay all the new declarations from the target file into the `Environment`
+as it was at the beginning of the file, using the kernel to check them.
+
+You can also use `leanchecker --fresh Mathlib.Data.Nat.Prime.Basic`
+to replay all the constants (both imported and defined in that file) into a fresh environment.
+This can only be used on a single file.
+
+This is not an external verifier, simply a tool to detect "environment hacking".
+-/
+unsafe def main (args : List String) : IO UInt32 := do
+  -- Contributor's note: lean4lean is intended to have a CLI interface matching leanchecker,
+  -- so if you want to make a change here please either make a sibling PR to
+  -- https://github.com/digama0/lean4lean or ping @digama0 (Mario Carneiro) to go fix it.
+  initSearchPath (← findSysroot)
+  let (flags, args) := args.partition fun s => s.startsWith "-"
+  let verbose := "-v" ∈ flags || "--verbose" ∈ flags
+  let fresh := "--fresh" ∈ flags
+  let targets ← do
+    match args with
+    | [] => pure [← getCurrentModule]
+    | args => args.mapM fun arg => do
+      let mod := arg.toName
+      if mod.isAnonymous then
+        throw <| IO.userError s!"Could not resolve module: {arg}"
+      else
+        pure mod
+  let mut targetModules := []
+  let sp ← searchPathRef.get
+  for target in targets do
+    let mut found := false
+    for path in (← SearchPath.findAllWithExt sp "olean") do
+      if let some m := (← searchModuleNameOfFileName path sp) then
+        if !fresh && target.isPrefixOf m || target == m then
+          targetModules := targetModules.insert m
+          found := true
+    if not found then
+      throw <| IO.userError s!"Could not find any oleans for: {target}"
+  if fresh then
+    if targetModules.length != 1 then
+      throw <| IO.userError s!"--fresh flag is only valid when specifying a single module:\n\
+        {targetModules}"
+    for m in targetModules do
+      if verbose then IO.println s!"replaying {m} with --fresh"
+      replayFromFresh m
+  else
+    let mut tasks := #[]
+    for m in targetModules do
+      tasks := tasks.push (m, ← IO.asTask (replayFromImports m))
+    for (m, t) in tasks do
+      if verbose then IO.println s!"replaying {m}"
+      if let .error e := t.get then
+        IO.eprintln s!"leanchecker found a problem in {m}"
+        throw e
+  return 0

src/LeanChecker/Replay.lean

@@ -0,0 +1,191 @@
+/-
+Copyright (c) 2023 Kim Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Lean.CoreM
+import Lean.AddDecl
+import Lean.Util.FoldConsts
+
+/-!
+# `Lean.Environment.replay`
+
+`replay env constantMap` will "replay" all the constants in `constantMap : HashMap Name ConstantInfo` into `env`,
+sending each declaration to the kernel for checking.
+
+`replay` does not send constructors or recursors in `constantMap` to the kernel,
+but rather checks that they are identical to constructors or recursors generated in the environment
+after replaying any inductive definitions occurring in `constantMap`.
+
+`replay` can be used either as:
+* a verifier for an `Environment`, by sending everything to the kernel, or
+* a mechanism to safely transfer constants from one `Environment` to another.
+
+## Implementation notes
+
+This is a patched version of `Lean.Environment.Replay`, which is in the `lean4` repository
+up to `v4.18.0`, but will be deprecated in `v4.19.0` and then removed. Once it it removed,
+the prime on the `Replay'` namespace, the prime on `Lean.Environment.replay'`
+should be removed here.
+
+-/
+
+namespace Lean.Environment
+
+namespace Replay'
+
+structure Context where
+  newConstants : Std.HashMap Name ConstantInfo
+
+structure State where
+  env : Kernel.Environment
+  remaining : NameSet := {}
+  pending : NameSet := {}
+  postponedConstructors : NameSet := {}
+  postponedRecursors : NameSet := {}
+
+abbrev M := ReaderT Context <| StateRefT State IO
+
+/-- Check if a `Name` still needs processing. If so, move it from `remaining` to `pending`. -/
+def isTodo (name : Name) : M Bool := do
+  let r := (← get).remaining
+  if r.contains name then
+    modify fun s => { s with remaining := s.remaining.erase name, pending := s.pending.insert name }
+    return true
+  else
+    return false
+
+/-- Use the current `Environment` to throw a `Kernel.Exception`. -/
+def throwKernelException (ex : Kernel.Exception) : M Unit := do
+  throw <| .userError <| (← ex.toMessageData {} |>.toString)
+
+/-- Add a declaration, possibly throwing a `Kernel.Exception`. -/
+def addDecl (d : Declaration) : M Unit := do
+  match (← get).env.addDeclCore 0 d (cancelTk? := none) with
+  | .ok env => modify fun s => { s with env := env }
+  | .error ex => throwKernelException ex
+
+mutual
+/--
+Check if a `Name` still needs to be processed (i.e. is in `remaining`).
+
+If so, recursively replay any constants it refers to,
+to ensure we add declarations in the right order.
+
+The construct the `Declaration` from its stored `ConstantInfo`,
+and add it to the environment.
+-/
+partial def replayConstant (name : Name) : M Unit := do
+  if ← isTodo name then
+    let some ci := (← read).newConstants[name]? | unreachable!
+    replayConstants ci.getUsedConstantsAsSet
+    -- Check that this name is still pending: a mutual block may have taken care of it.
+    if (← get).pending.contains name then
+      match ci with
+      | .defnInfo   info =>
+        addDecl (Declaration.defnDecl   info)
+      | .thmInfo    info =>
+        -- Ignore duplicate theorems. This code is identical to that in `finalizeImport` before it
+        -- added extended duplicates support for the module system, which is not relevant for us
+        -- here as we always load all .olean information. We need this case *because* of the module
+        -- system -- as we have more data loaded than it, we might encounter duplicate private
+        -- theorems where elaboration under the module system would have only one of them in scope.
+        if let some (.thmInfo info') := (← get).env.find? ci.name then
+          if info.name == info'.name &&
+            info.type == info'.type &&
+            info.levelParams == info'.levelParams &&
+            info.all == info'.all
+          then
+            return
+        addDecl (Declaration.thmDecl    info)
+      | .axiomInfo  info =>
+        addDecl (Declaration.axiomDecl  info)
+      | .opaqueInfo info =>
+        addDecl (Declaration.opaqueDecl info)
+      | .inductInfo info =>
+        let lparams := info.levelParams
+        let nparams := info.numParams
+        let all ← info.all.mapM fun n => do pure <| ((← read).newConstants[n]!)
+        for o in all do
+          modify fun s =>
+            { s with remaining := s.remaining.erase o.name, pending := s.pending.erase o.name }
+        let ctorInfo ← all.mapM fun ci => do
+          pure (ci, ← ci.inductiveVal!.ctors.mapM fun n => do
+            pure ((← read).newConstants[n]!))
+        -- Make sure we are really finished with the constructors.
+        for (_, ctors) in ctorInfo do
+          for ctor in ctors do
+            replayConstants ctor.getUsedConstantsAsSet
+        let types : List InductiveType := ctorInfo.map fun ⟨ci, ctors⟩ =>
+          { name := ci.name
+            type := ci.type
+            ctors := ctors.map fun ci => { name := ci.name, type := ci.type } }
+        addDecl (Declaration.inductDecl lparams nparams types false)
+      -- We postpone checking constructors,
+      -- and at the end make sure they are identical
+      -- to the constructors generated when we replay the inductives.
+      | .ctorInfo info =>
+        modify fun s => { s with postponedConstructors := s.postponedConstructors.insert info.name }
+      -- Similarly we postpone checking recursors.
+      | .recInfo info =>
+        modify fun s => { s with postponedRecursors := s.postponedRecursors.insert info.name }
+      | .quotInfo _ =>
+        -- `Quot.lift` and `Quot.ind` have types that reference `Eq`,
+        -- so we need to ensure `Eq` is replayed before adding the quotient declaration.
+        replayConstant `Eq
+        addDecl (Declaration.quotDecl)
+      modify fun s => { s with pending := s.pending.erase name }
+
+/-- Replay a set of constants one at a time. -/
+partial def replayConstants (names : NameSet) : M Unit := do
+  for n in names do replayConstant n
+
+end
+
+/--
+Check that all postponed constructors are identical to those generated
+when we replayed the inductives.
+-/
+def checkPostponedConstructors : M Unit := do
+  for ctor in (← get).postponedConstructors do
+    match (← get).env.find? ctor, (← read).newConstants[ctor]? with
+    | some (.ctorInfo info), some (.ctorInfo info') =>
+      if ! (info == info') then throw <| IO.userError s!"Invalid constructor {ctor}"
+    | _, _ => throw <| IO.userError s!"No such constructor {ctor}"
+
+/--
+Check that all postponed recursors are identical to those generated
+when we replayed the inductives.
+-/
+def checkPostponedRecursors : M Unit := do
+  for ctor in (← get).postponedRecursors do
+    match (← get).env.find? ctor, (← read).newConstants[ctor]? with
+    | some (.recInfo info), some (.recInfo info') =>
+      if ! (info == info') then throw <| IO.userError s!"Invalid recursor {ctor}"
+    | _, _ => throw <| IO.userError s!"No such recursor {ctor}"
+
+end Replay'
+
+open Replay'
+
+/--
+"Replay" some constants into an `Environment`, sending them to the kernel for checking.
+
+Throws a `IO.userError` if the kernel rejects a constant,
+or if there are malformed recursors or constructors for inductive types.
+-/
+def replay' (newConstants : Std.HashMap Name ConstantInfo) (env : Environment) : IO Environment := do
+  let mut remaining : NameSet := ∅
+  for (n, ci) in newConstants.toList do
+    -- We skip unsafe constants, and also partial constants.
+    -- Later we may want to handle partial constants.
+    if !ci.isUnsafe && !ci.isPartial then
+      remaining := remaining.insert n
+  let (_, s) ← StateRefT'.run (s := { env := env.toKernelEnv, remaining }) do
+    ReaderT.run (r := { newConstants }) do
+      for n in remaining do
+        replayConstant n
+      checkPostponedConstructors
+      checkPostponedRecursors
+  return .ofKernelEnv s.env

src/Std/Data/ExtHashMap/Basic.lean

@@ -107,7 +107,7 @@ def containsThenInsertIfNew [EquivBEq α] [LawfulHashable α]
   ⟨replaced, ⟨r⟩⟩
 
 /--
-Checks whether a key is present in a map, returning the associate value, and inserts a value for
+Checks whether a key is present in a map, returning the associated value, and inserts a value for
 the key if it was not found.
 
 If the returned value is `some v`, then the returned map is unaltered. If it is `none`, then the

src/Std/Data/HashMap/Basic.lean

@@ -108,7 +108,7 @@ instance : LawfulSingleton (α × β) (HashMap α β) := ⟨fun _ => rfl⟩
   ⟨replaced, ⟨r⟩⟩
 
 /--
-Checks whether a key is present in a map, returning the associate value, and inserts a value for
+Checks whether a key is present in a map, returning the associated value, and inserts a value for
 the key if it was not found.
 
 If the returned value is `some v`, then the returned map is unaltered. If it is `none`, then the

src/Std/Do/SPred/DerivedLaws.lean

@@ -220,7 +220,7 @@ Decomposing assertions in postconditions into conjunctions of simpler predicates
 chance that automation will be able to prove the entailment of the postcondition and the next precondition.
 -/
 class IsAnd (P : SPred σs) (Q₁ Q₂ : outParam (SPred σs)) where
-  /-- A proof the the decomposition is logically equivalent to the original predicate. -/
+  /-- A proof that the decomposition is logically equivalent to the original predicate. -/
   to_and : P ⊣⊢ₛ Q₁ ∧ Q₂
 instance (σs) (Q₁ Q₂ : SPred σs) : IsAnd (σs:=σs) spred(Q₁ ∧ Q₂) Q₁ Q₂ where to_and := .rfl
 instance (σs) : IsAnd (σs:=σs) ⌜p ∧ q⌝ ⌜p⌝ ⌜q⌝ where to_and := pure_and.symm

src/Std/Internal.lean

@@ -9,6 +9,7 @@ prelude
 public import Std.Internal.Async
 public import Std.Internal.Parsec
 public import Std.Internal.UV
+public import Std.Internal.Http
 
 @[expose] public section
 

src/Std/Internal/Async/Basic.lean

@@ -22,13 +22,13 @@ namespace Async
 This module provides a layered approach to asynchronous programming, combining monadic types,
 type classes, and concrete task types that work together in a cohesive system.
 
-- **Monadic Types**: These types provide a good way to to chain and manipulate context. These
+- **Monadic Types**: These types provide a good way to chain and manipulate context. These
   can contain a `Task`, enabling manipulation of both asynchronous and synchronous code.
 - **Concrete Task Types**: Concrete units of work that can be executed within these contexts.
 
 ## Monadic Types
 
-These types provide a good way to to chain and manipulate context. These can contain a `Task`,
+These types provide a good way to chain and manipulate context. These can contain a `Task`,
 enabling manipulation of both asynchronous and synchronous code.
 
 - `BaseAsync`: A monadic type for infallible asynchronous computations
@@ -548,7 +548,7 @@ def concurrentlyAll (xs : Array (BaseAsync α)) (prio := Task.Priority.default)
 
 /--
 Runs all computations concurrently and returns the result of the first one to finish.
-All other results are lost, and the tasks are not cancelled, so they'll continue their executing
+All other results are lost, and the tasks are not cancelled, so they'll continue their execution
 until the end.
 -/
 @[inline, specialize]
@@ -753,6 +753,10 @@ instance : MonadLift (EIO ε) (EAsync ε) where
 instance : MonadLift BaseAsync (EAsync ε) where
   monadLift x := .mk <| x.map (.ok)
 
+instance : MonadAttach BaseAsync := .trivial
+
+instance : MonadAttach (EAsync ε) := .trivial
+
 @[inline]
 protected partial def forIn
     {β : Type} (init : β)
@@ -829,7 +833,7 @@ def concurrentlyAll (xs : Array (EAsync ε α)) (prio := Task.Priority.default)
 
 /--
 Runs all computations concurrently and returns the result of the first one to finish.
-All other results are lost, and the tasks are not cancelled, so they'll continue their executing
+All other results are lost, and the tasks are not cancelled, so they'll continue their execution
 until the end.
 -/
 @[inline, specialize]
@@ -969,7 +973,7 @@ def concurrentlyAll (xs : Array (Async α)) (prio := Task.Priority.default) : As
 
 /--
 Runs all computations concurrently and returns the result of the first one to finish.
-All other results are lost, and the tasks are not cancelled, so they'll continue their executing
+All other results are lost, and the tasks are not cancelled, so they'll continue their execution
 until the end.
 -/
 @[inline, specialize]