refactor: move issue tracker from grind to SymM (#13125)

This PR moves the issue tracking infrastructure from `GrindM` to `SymM`.
Issues can occur in different places within a `sym =>` block (e.g.,
during
arithmetic normalization, simplification), not just during `grind`
invocations. Moving them to `SymM` makes them available to all modules
operating within the symbolic computation framework.

- `Sym.reportIssue`: adds an issue to the `SymM` state
- `Sym.getIssues`: retrieves accumulated issues
- `Sym.withNewIssueContext`: saves/restores the issue list around a
  computation, used at grind entry points to isolate per-invocation
  issues while preserving them in the outer context
- `GrindM.State.issues` removed; `Grind.reportIssue` delegates to
`Sym.reportIssue`

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

---------

Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

.github/workflows/build-template.yml

@@ -33,7 +33,7 @@ jobs:
         include: ${{fromJson(inputs.config)}}
       # complete all jobs
       fail-fast: false
-    runs-on: ${{ endsWith(matrix.os, '-with-cache') && fromJSON(format('["{0}", "nscloud-git-mirror-1gb"]', matrix.os)) || matrix.os }}
+    runs-on: ${{ endsWith(matrix.os, '-with-cache') && fromJSON(format('["{0}", "nscloud-git-mirror-5gb"]', matrix.os)) || matrix.os }}
     defaults:
       run:
         shell: ${{ matrix.shell || 'nix develop -c bash -euxo pipefail {0}' }}
@@ -78,7 +78,7 @@ jobs:
       # (needs to be after "Install *" to use the right shell)
       - name: CI Merge Checkout
         run: |
-          git fetch --depth=1 origin ${{ github.sha }}
+          git fetch --depth=${{ matrix.name == 'Linux Lake (Cached)' && '10' || '1' }} origin ${{ github.sha }}
           git checkout FETCH_HEAD flake.nix flake.lock script/prepare-* tests/elab/importStructure.lean
         if: github.event_name == 'pull_request'
       # (needs to be after "Checkout" so files don't get overridden)
@@ -125,7 +125,7 @@ jobs:
           else
             echo "TARGET_STAGE=stage1" >> $GITHUB_ENV
           fi
-      - name: Build
+      - name: Configure Build
         run: |
           ulimit -c unlimited  # coredumps
           [ -d build ] || mkdir build
@@ -162,7 +162,21 @@ jobs:
           fi
           # contortion to support empty OPTIONS with old macOS bash
           cmake .. --preset ${{ matrix.CMAKE_PRESET || 'release' }} -B . ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/..
-          time make $TARGET_STAGE -j$NPROC
+      - name: Build Stage 0 & Configure Stage 1
+        run: |
+          ulimit -c unlimited  # coredumps
+          time make -C build stage1-configure -j$NPROC
+      - name: Download Lake Cache
+        if: matrix.name == 'Linux Lake (Cached)'
+        run: |
+          cd src
+          ../build/stage0/bin/lake cache get --repo=${{ github.repository }}
+        timeout-minutes: 20 # prevent excessive hanging from network issues
+        continue-on-error: true
+      - name: Build Target Stage
+        run: |
+          ulimit -c unlimited  # coredumps
+          time make -C build $TARGET_STAGE -j$NPROC
       # Should be done as early as possible and in particular *before* "Check rebootstrap" which
       # changes the state of stage1/
       - name: Save Cache
@@ -181,6 +195,21 @@ jobs:
             build/stage1/**/*.c
             build/stage1/**/*.c.o*' || '' }}
           key: ${{ steps.restore-cache.outputs.cache-primary-key }}
+      - name: Upload Lake Cache
+        # Caching on cancellation created some mysterious issues perhaps related to improper build
+        # shutdown. Also, since this needs access to secrets, it cannot be run on forks.
+        if: matrix.name == 'Linux Lake' && !cancelled() && (github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository)
+        run: |
+          curl --version
+          cd src
+          time ../build/stage0/bin/lake build -o ../build/lake-mappings.jsonl
+          time ../build/stage0/bin/lake cache put ../build/lake-mappings.jsonl --repo=${{ github.repository }}
+        env:
+          LAKE_CACHE_KEY: ${{ secrets.LAKE_CACHE_KEY }}
+          LAKE_CACHE_ARTIFACT_ENDPOINT: ${{ vars.LAKE_CACHE_ENDPOINT }}/a1
+          LAKE_CACHE_REVISION_ENDPOINT: ${{ vars.LAKE_CACHE_ENDPOINT }}/r1
+        timeout-minutes: 20 # prevent excessive hanging from network issues
+        continue-on-error: true
       - name: Install
         run: |
           make -C build/$TARGET_STAGE install

.github/workflows/check-empty-pr.yml

@@ -0,0 +1,29 @@
+name: Check for empty PR
+
+on:
+  merge_group:
+  pull_request:
+
+jobs:
+  check-empty-pr:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v6
+      with:
+        ref: ${{ github.event_name == 'pull_request' && github.event.pull_request.head.sha || github.sha }}
+        fetch-depth: 0
+        filter: tree:0
+
+    - name: Check for empty diff
+      run: |
+        if [[ "${{ github.event_name }}" == "pull_request" ]]; then
+          base=$(git merge-base "origin/${{ github.base_ref }}" HEAD)
+        else
+          base=$(git rev-parse HEAD^1)
+        fi
+        if git diff --quiet "$base" HEAD --; then
+          echo "This PR introduces no changes compared to its base branch." | tee "$GITHUB_STEP_SUMMARY"
+          echo "It may be a duplicate of an already-merged PR." | tee -a "$GITHUB_STEP_SUMMARY"
+          exit 1
+        fi
+      shell: bash

.github/workflows/ci.yml

@@ -76,9 +76,20 @@ jobs:
               fi
               echo "nightly=$LEAN_VERSION_STRING" >> "$GITHUB_OUTPUT"
             else
-              # Scheduled: do nothing if commit already has a different tag
+              # Scheduled: do nothing if commit already has a different tag (e.g. a release tag)
               LEAN_VERSION_STRING="nightly-$(date -u +%F)"
-              if [[ "$(git name-rev --name-only --tags --no-undefined HEAD 2> /dev/null || echo "$LEAN_VERSION_STRING")" == "$LEAN_VERSION_STRING" ]]; then
+              HEAD_TAG="$(git name-rev --name-only --tags --no-undefined HEAD 2> /dev/null || true)"
+              if [[ -n "$HEAD_TAG" && "$HEAD_TAG" != "$LEAN_VERSION_STRING" ]]; then
+                echo "HEAD already tagged as ${HEAD_TAG}, skipping nightly"
+              elif git rev-parse "refs/tags/${LEAN_VERSION_STRING}" >/dev/null 2>&1; then
+                # Today's nightly already exists (e.g. from a manual release), create a revision
+                REV=1
+                while git rev-parse "refs/tags/${LEAN_VERSION_STRING}-rev${REV}" >/dev/null 2>&1; do
+                  REV=$((REV + 1))
+                done
+                LEAN_VERSION_STRING="${LEAN_VERSION_STRING}-rev${REV}"
+                echo "nightly=$LEAN_VERSION_STRING" >> "$GITHUB_OUTPUT"
+              else
                 echo "nightly=$LEAN_VERSION_STRING" >> "$GITHUB_OUTPUT"
               fi
             fi
@@ -244,7 +255,7 @@ jobs:
                 // portable release build: use channel with older glibc (2.26)
                 "name": "Linux release",
                 // usually not a bottleneck so make exclusive to `fast-ci`
-                "os": large && fast ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
+                "os": large && fast ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
                 "release": true,
                 // Special handling for release jobs. We want:
                 // 1. To run it in PRs so developers get PR toolchains (so secondary without tests is sufficient)
@@ -265,7 +276,7 @@ jobs:
               },
               {
                 "name": "Linux Lake",
-                "os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
+                "os": large ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
                 "enabled": true,
                 "check-rebootstrap": level >= 1,
                 "check-stage3": level >= 2,
@@ -273,7 +284,19 @@ jobs:
                 // NOTE: `test-bench` currently seems to be broken on `ubuntu-latest`
                 "test-bench": large && level >= 2,
                 // We are not warning-free yet on all platforms, start here
-                "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror",
+                "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror -DUSE_LAKE_CACHE=ON",
+              },
+              {
+                "name": "Linux Lake (Cached)",
+                "os": large ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
+                "enabled": true,
+                "check-rebootstrap": level >= 1,
+                "check-stage3": level >= 2,
+                "test": true,
+                "secondary": true,
+                // NOTE: `test-bench` currently seems to be broken on `ubuntu-latest`
+                "test-bench": large && level >= 2,
+                "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror -DUSE_LAKE_CACHE=ON",
               },
               {
                 "name": "Linux Reldebug",
@@ -287,7 +310,7 @@ jobs:
               {
                 "name": "Linux fsanitize",
                 // Always run on large if available, more reliable regarding timeouts
-                "os": large ? "nscloud-ubuntu-22.04-amd64-16x32-with-cache" : "ubuntu-latest",
+                "os": large ? "nscloud-ubuntu-24.04-amd64-16x32-with-cache" : "ubuntu-latest",
                 "enabled": level >= 2,
                 // do not fail nightlies on this for now
                 "secondary": level <= 2,

script/release_checklist.py

@@ -236,7 +236,7 @@ def parse_version(version_str):
 def is_version_gte(version1, version2):
     """Check if version1 >= version2, including proper handling of release candidates."""
     # Check if version1 is a nightly toolchain
-    if version1.startswith("leanprover/lean4:nightly-"):
+    if version1.startswith("leanprover/lean4:nightly-") or version1.startswith("leanprover/lean4-nightly:"):
         return False
     return parse_version(version1) >= parse_version(version2)
 

src/Init/Data/BEq.lean

@@ -66,3 +66,8 @@ theorem BEq.neq_of_beq_of_neq [BEq α] [PartialEquivBEq α] {a b c : α} :
 instance (priority := low) [BEq α] [LawfulBEq α] : EquivBEq α where
   symm h := beq_iff_eq.2 <| Eq.symm <| beq_iff_eq.1 h
   trans hab hbc := beq_iff_eq.2 <| (beq_iff_eq.1 hab).trans <| beq_iff_eq.1 hbc
+
+theorem equivBEq_of_iff_apply_eq [BEq α] (f : α → β) (hf : ∀ a b, a == b ↔ f a = f b) : EquivBEq α where
+  rfl := by simp [hf]
+  symm := by simp [hf, eq_comm]
+  trans hab hbc := (hf _ _).2 (Eq.trans ((hf _ _).1 hab) ((hf _ _).1 hbc))

src/Init/Data/Char/Lemmas.lean

@@ -98,4 +98,8 @@ theorem toNat_inj {c d : Char} : c.toNat = d.toNat ↔ c = d := by
 theorem isDigit_iff_toNat {c : Char} : c.isDigit ↔ '0'.toNat ≤ c.toNat ∧ c.toNat ≤ '9'.toNat := by
   simp [isDigit, UInt32.le_iff_toNat_le]
 
+@[simp]
+theorem toNat_mk {val : UInt32} {h} : (Char.mk val h).toNat = val.toNat := by
+  simp [← toNat_val]
+
 end Char

src/Init/Data/Nat/ToString.lean

@@ -298,7 +298,7 @@ theorem ofDigitChars_cons {c : Char} {cs : List Char} {init : Nat} :
   simp [ofDigitChars]
 
 theorem ofDigitChars_cons_digitChar_of_lt_ten {n : Nat} (hn : n < 10) {cs : List Char} {init : Nat} :
-    ofDigitChars 10 (n.digitChar :: cs) init = ofDigitChars 10 cs (10 * init + n) := by
+    ofDigitChars b (n.digitChar :: cs) init = ofDigitChars b cs (b * init + n) := by
   simp [ofDigitChars_cons, Nat.toNat_digitChar_sub_48_of_lt_ten hn]
 
 theorem ofDigitChars_eq_ofDigitChars_zero {l : List Char} {init : Nat} :
@@ -320,15 +320,17 @@ theorem ofDigitChars_replicate_zero {n : Nat} : ofDigitChars b (List.replicate n
   | zero => simp
   | succ n ih => simp [List.replicate_succ, ofDigitChars_cons, ih, Nat.pow_succ, Nat.mul_assoc]
 
-@[simp]
-theorem ofDigitChars_toDigits {n : Nat} : ofDigitChars 10 (toDigits 10 n) 0 = n := by
-  have : 1 < 10 := by decide
-  induction n using base_induction 10 this with
+theorem ofDigitChars_toDigits {b n : Nat} (hb' : 1 < b) (hb : b ≤ 10) : ofDigitChars b (toDigits b n) 0 = n := by
+  induction n using base_induction b hb' with
   | single m hm =>
-    simp [Nat.toDigits_of_lt_base hm, ofDigitChars_cons_digitChar_of_lt_ten hm]
+    simp [Nat.toDigits_of_lt_base hm, ofDigitChars_cons_digitChar_of_lt_ten (by omega : m < 10)]
   | digit m k hk hm ih =>
-    rw [← Nat.toDigits_append_toDigits this hm hk,
+    rw [← Nat.toDigits_append_toDigits hb' hm hk,
       ofDigitChars_append, ih, Nat.toDigits_of_lt_base hk,
-      ofDigitChars_cons_digitChar_of_lt_ten hk, ofDigitChars_nil]
+      ofDigitChars_cons_digitChar_of_lt_ten (Nat.lt_of_lt_of_le hk hb), ofDigitChars_nil]
+
+@[simp]
+theorem ofDigitChars_ten_toDigits {n : Nat} : ofDigitChars 10 (toDigits 10 n) 0 = n :=
+  ofDigitChars_toDigits (by decide) (by decide)
 
 end Nat

src/Init/Data/String/Basic.lean

@@ -852,6 +852,10 @@ theorem Slice.rawEndPos_copy {s : Slice} : s.copy.rawEndPos = s.rawEndPos := by
 theorem copy_toSlice {s : String} : s.toSlice.copy = s := by
   simp [← toByteArray_inj, Slice.toByteArray_copy, ← size_toByteArray]
 
+@[simp]
+theorem copy_comp_toSlice : String.Slice.copy ∘ String.toSlice = id := by
+  ext; simp
+
 theorem Slice.getUTF8Byte_eq_getUTF8Byte_copy {s : Slice} {p : Pos.Raw} {h : p < s.rawEndPos} :
     s.getUTF8Byte p h = s.copy.getUTF8Byte p (by simpa) := by
   simp [getUTF8Byte, String.getUTF8Byte, toByteArray_copy, ByteArray.getElem_extract]

src/Init/Data/String/Defs.lean

@@ -187,6 +187,9 @@ theorem append_right_inj (s : String) {t₁ t₂ : String} :
 theorem append_assoc {s₁ s₂ s₃ : String} : s₁ ++ s₂ ++ s₃ = s₁ ++ (s₂ ++ s₃) := by
   simp [← toByteArray_inj, ByteArray.append_assoc]
 
+instance : Std.Associative (α := String) (· ++ ·) where
+  assoc _ _ _ := append_assoc
+
 @[simp]
 theorem utf8ByteSize_eq_zero_iff {s : String} : s.utf8ByteSize = 0 ↔ s = "" := by
   refine ⟨fun h => ?_, fun h => h ▸ utf8ByteSize_empty⟩

src/Init/Data/String/Iter.lean

@@ -6,29 +6,5 @@ Authors: Markus Himmel
 module
 
 prelude
-public import Init.Data.Iterators.Combinators.FilterMap
-public import Init.Data.Iterators.Consumers.Collect
-
-set_option doc.verso true
-
-namespace Std
-
-/--
-Convenience function for turning an iterator into a list of strings, provided the output of the
-iterator implements {name}`ToString`.
--/
-@[inline]
-public abbrev Iter.toStringList {α β : Type} [Iterator α Id β] [ToString β]
-    (it : Iter (α := α) β) : List String :=
-  it.map toString |>.toList
-
-/--
-Convenience function for turning an iterator into an array of strings, provided the output of the
-iterator implements {name}`ToString`.
--/
-@[inline]
-public abbrev Iter.toStringArray {α β : Type} [Iterator α Id β] [ToString β]
-    (it : Iter (α := α) β) : Array String :=
-  it.map toString |>.toArray
-
-end Std
+public import Init.Data.String.Iter.Basic
+public import Init.Data.String.Iter.Intercalate

src/Init/Data/String/Iter/Basic.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.Iterators.Combinators.FilterMap
+public import Init.Data.Iterators.Consumers.Collect
+
+set_option doc.verso true
+
+namespace Std
+
+/--
+Convenience function for turning an iterator into a list of strings, provided the output of the
+iterator implements {name}`ToString`.
+-/
+@[inline]
+public abbrev Iter.toStringList {α β : Type} [Iterator α Id β] [ToString β]
+    (it : Iter (α := α) β) : List String :=
+  it.map toString |>.toList
+
+/--
+Convenience function for turning an iterator into an array of strings, provided the output of the
+iterator implements {name}`ToString`.
+-/
+@[inline]
+public abbrev Iter.toStringArray {α β : Type} [Iterator α Id β] [ToString β]
+    (it : Iter (α := α) β) : Array String :=
+  it.map toString |>.toArray
+
+end Std

src/Init/Data/String/Iter/Intercalate.lean

@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Julia Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.Iterators.Combinators.Monadic.FilterMap
+public import Init.Data.String.Basic
+import Init.Data.String.Slice
+
+set_option doc.verso true
+
+namespace Std
+
+/--
+Appends all the elements in the iterator, in order.
+-/
+public def Iter.joinString {α β : Type} [Iterator α Id β] [ToString β]
+    (it : Std.Iter (α := α) β) : String :=
+  (it.map toString).fold (init := "") (· ++ ·)
+
+/--
+Appends the elements of the iterator into a string, placing the separator {name}`s` between them.
+-/
+@[inline]
+public def Iter.intercalateString {α β : Type} [Iterator α Id β] [ToString β]
+    (s : String.Slice) (it : Std.Iter (α := α) β) : String :=
+  it.map toString
+    |>.fold (init := none) (fun
+      | none, sl => some sl
+      | some str, sl => some (str ++ s ++ sl))
+    |>.getD ""
+
+end Std

src/Init/Data/String/Lemmas.lean

@@ -17,6 +17,9 @@ public import Init.Data.String.Lemmas.Pattern
 public import Init.Data.String.Lemmas.Slice
 public import Init.Data.String.Lemmas.Iterate
 public import Init.Data.String.Lemmas.Intercalate
+public import Init.Data.String.Lemmas.Iter
+public import Init.Data.String.Lemmas.Hashable
+public import Init.Data.String.Lemmas.TakeDrop
 import Init.Data.Order.Lemmas
 public import Init.Data.String.Basic
 import Init.Data.Char.Lemmas

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

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.String.Basic
+import all Init.Data.String.Basic
 import Init.Data.ByteArray.Lemmas
 import Init.Data.Nat.MinMax
 
@@ -56,6 +57,11 @@ theorem singleton_ne_empty {c : Char} : singleton c ≠ "" := by
 theorem empty_ne_singleton {c : Char} : "" ≠ singleton c := by
   simp
 
+@[simp]
+theorem ofList_cons {c : Char} {l : List Char} :
+    String.ofList (c :: l) = String.singleton c ++ String.ofList l := by
+  simp [← toList_inj]
+
 @[simp]
 theorem Slice.Pos.copy_inj {s : Slice} {p₁ p₂ : s.Pos} : p₁.copy = p₂.copy ↔ p₁ = p₂ := by
   simp [String.Pos.ext_iff, Pos.ext_iff]
@@ -244,4 +250,46 @@ theorem Pos.get_ofToSlice {s : String} {p : (s.toSlice).Pos} {h} :
 @[simp]
 theorem push_empty {c : Char} : "".push c = singleton c := rfl
 
+namespace Slice.Pos
+
+@[simp]
+theorem nextn_zero {s : Slice} {p : s.Pos} : p.nextn 0 = p := by
+  simp [nextn]
+
+theorem nextn_add_one {s : Slice} {p : s.Pos} :
+    p.nextn (n + 1) = if h : p = s.endPos then p else (p.next h).nextn n := by
+  simp [nextn]
+
+@[simp]
+theorem nextn_endPos {s : Slice} : s.endPos.nextn n = s.endPos := by
+  cases n <;> simp [nextn_add_one]
+
+end Slice.Pos
+
+namespace Pos
+
+theorem nextn_eq_nextn_toSlice {s : String} {p : s.Pos} : p.nextn n = Pos.ofToSlice (p.toSlice.nextn n) :=
+  (rfl)
+
+@[simp]
+theorem nextn_zero {s : String} {p : s.Pos} : p.nextn 0 = p := by
+  simp [nextn_eq_nextn_toSlice]
+
+theorem nextn_add_one {s : String} {p : s.Pos} :
+    p.nextn (n + 1) = if h : p = s.endPos then p else (p.next h).nextn n := by
+  simp only [nextn_eq_nextn_toSlice, Slice.Pos.nextn_add_one, endPos_toSlice, toSlice_inj]
+  split <;> simp [Pos.next_toSlice]
+
+theorem nextn_toSlice {s : String} {p : s.Pos} : p.toSlice.nextn n = (p.nextn n).toSlice := by
+  induction n generalizing p with simp_all [nextn_add_one, Slice.Pos.nextn_add_one, apply_dite Pos.toSlice, next_toSlice]
+
+theorem toSlice_nextn {s : String} {p : s.Pos} : (p.nextn n).toSlice = p.toSlice.nextn n :=
+  nextn_toSlice.symm
+
+@[simp]
+theorem nextn_endPos {s : String} : s.endPos.nextn n = s.endPos := by
+  cases n <;> simp [nextn_add_one]
+
+end Pos
+
 end String

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

@@ -11,6 +11,8 @@ import all Init.Data.String.FindPos
 import Init.Data.String.OrderInstances
 import Init.Data.String.Lemmas.Order
 import Init.Data.Order.Lemmas
+import Init.Data.Option.Lemmas
+import Init.ByCases
 
 public section
 
@@ -217,6 +219,23 @@ theorem Pos.prev_next {s : Slice} {p : s.Pos} {h} : (p.next h).prev (by simp) =
 theorem Pos.next_prev {s : Slice} {p : s.Pos} {h} : (p.prev h).next (by simp) = p :=
   next_eq_iff.2 (by simp)
 
+theorem Pos.prev?_eq_dif {s : Slice} {p : s.Pos} : p.prev? = if h : p = s.startPos then none else some (p.prev h) :=
+  (rfl)
+
+theorem Pos.prev?_eq_some_prev {s : Slice} {p : s.Pos} (h : p ≠ s.startPos) : p.prev? = some (p.prev h) := by
+  simp [Pos.prev?, h]
+
+@[simp]
+theorem Pos.prev?_eq_none_iff {s : Slice} {p : s.Pos} : p.prev? = none ↔ p = s.startPos := by
+  simp [Pos.prev?]
+
+theorem Pos.prev?_eq_none {s : Slice} {p : s.Pos} (h : p = s.startPos) : p.prev? = none :=
+  prev?_eq_none_iff.2 h
+
+@[simp]
+theorem Pos.prev?_startPos {s : Slice} : s.startPos.prev? = none := by
+  simp
+
 end Slice
 
 @[simp]
@@ -428,10 +447,18 @@ theorem Pos.toSlice_prev {s : String} {p : s.Pos} {h} :
     (p.prev h).toSlice = p.toSlice.prev (by simpa [toSlice_inj]) := by
   simp [prev]
 
+theorem Pos.ofToSlice_prev {s : String} {p : s.toSlice.Pos} {h} :
+    Pos.ofToSlice (p.prev h) = (Pos.ofToSlice p).prev (by simpa [← toSlice_inj]) := by
+  simp [prev]
+
 theorem Pos.prev_toSlice {s : String} {p : s.Pos} {h} :
     p.toSlice.prev h = (p.prev (by simpa [← toSlice_inj])).toSlice := by
   simp [prev]
 
+theorem Pos.prev_ofToSlice {s : String} {p : s.toSlice.Pos} {h} :
+    (Pos.ofToSlice p).prev h = Pos.ofToSlice (p.prev (by simpa [← ofToSlice_inj])) := by
+  simp [prev]
+
 theorem Pos.prevn_le {s : String} {p : s.Pos} {n : Nat} :
     p.prevn n ≤ p := by
   simpa [Pos.le_iff, ← offset_toSlice] using Slice.Pos.prevn_le
@@ -444,4 +471,71 @@ theorem Pos.prev_next {s : String} {p : s.Pos} {h} : (p.next h).prev (by simp) =
 theorem Pos.next_prev {s : String} {p : s.Pos} {h} : (p.prev h).next (by simp) = p :=
   next_eq_iff.2 (by simp)
 
+theorem Pos.prev?_eq_prev?_toSlice {s : String} {p : s.Pos} : p.prev? = p.toSlice.prev?.map Pos.ofToSlice :=
+  (rfl)
+
+theorem Pos.prev?_toSlice {s : String} {p : s.Pos} : p.toSlice.prev? = p.prev?.map Pos.toSlice := by
+  simp [prev?_eq_prev?_toSlice]
+
+theorem Pos.prev?_eq_dif {s : String} {p : s.Pos} : p.prev? = if h : p = s.startPos then none else some (p.prev h) := by
+  simp [prev?_eq_prev?_toSlice, Slice.Pos.prev?_eq_dif, apply_dite (Option.map Pos.ofToSlice),
+    ofToSlice_prev]
+
+theorem Pos.prev?_eq_some_prev {s : String} {p : s.Pos} (h : p ≠ s.startPos) : p.prev? = some (p.prev h) := by
+  simp [prev?_eq_prev?_toSlice, Slice.Pos.prev?_eq_some_prev (by simpa : p.toSlice ≠ s.toSlice.startPos),
+    ofToSlice_prev]
+
+@[simp]
+theorem Pos.prev?_eq_none_iff {s : String} {p : s.Pos} : p.prev? = none ↔ p = s.startPos := by
+  simp [prev?_eq_prev?_toSlice]
+
+theorem Pos.prev?_eq_none {s : String} {p : s.Pos} (h : p = s.startPos) : p.prev? = none :=
+  prev?_eq_none_iff.2 h
+
+@[simp]
+theorem Pos.prev?_startPos {s : String} : s.startPos.prev? = none := by
+  simp
+
+namespace Slice.Pos
+
+@[simp]
+theorem prevn_zero {s : Slice} {p : s.Pos} : p.prevn 0 = p := by
+  simp [prevn]
+
+theorem prevn_add_one {s : Slice} {p : s.Pos} :
+    p.prevn (n + 1) = if h : p = s.startPos then p else (p.prev h).prevn n := by
+  simp [prevn]
+
+@[simp]
+theorem prevn_startPos {s : Slice} : s.startPos.prevn n = s.startPos := by
+  cases n <;> simp [prevn_add_one]
+
+end Slice.Pos
+
+namespace Pos
+
+theorem prevn_eq_prevn_toSlice {s : String} {p : s.Pos} : p.prevn n = Pos.ofToSlice (p.toSlice.prevn n) :=
+  (rfl)
+
+@[simp]
+theorem prevn_zero {s : String} {p : s.Pos} : p.prevn 0 = p := by
+  simp [prevn_eq_prevn_toSlice]
+
+theorem prevn_add_one {s : String} {p : s.Pos} :
+    p.prevn (n + 1) = if h : p = s.startPos then p else (p.prev h).prevn n := by
+  simp only [prevn_eq_prevn_toSlice, Slice.Pos.prevn_add_one, startPos_toSlice, toSlice_inj]
+  split <;> simp [Pos.prev_toSlice]
+
+theorem prevn_toSlice {s : String} {p : s.Pos} : p.toSlice.prevn n = (p.prevn n).toSlice := by
+  induction n generalizing p with simp_all [prevn_add_one, Slice.Pos.prevn_add_one, apply_dite Pos.toSlice, prev_toSlice]
+
+theorem toSlice_prevn {s : String} {p : s.Pos} : (p.prevn n).toSlice = p.toSlice.prevn n :=
+  prevn_toSlice.symm
+
+@[simp]
+theorem prevn_startPos {s : String} : s.startPos.prevn n = s.startPos := by
+  cases n <;> simp [prevn_add_one]
+
+end Pos
+
 end String

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

@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Julia Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.String.Slice
+public import Init.Data.LawfulHashable
+import all Init.Data.String.Slice
+import Init.Data.String.Lemmas.Slice
+
+namespace String
+
+public theorem hash_eq {s : String} : hash s = String.hash s := rfl
+
+namespace Slice
+
+public theorem hash_eq {s : String.Slice} : hash s = String.hash s.copy := (rfl)
+
+public instance : LawfulHashable String.Slice where
+  hash_eq a b hab := by simp [hash_eq, beq_eq_true_iff.1 hab]
+
+end String.Slice

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

@@ -10,6 +10,7 @@ public import Init.Data.String.Defs
 import all Init.Data.String.Defs
 public import Init.Data.String.Slice
 import all Init.Data.String.Slice
+import Init.ByCases
 
 public section
 
@@ -42,6 +43,16 @@ theorem intercalate_cons_of_ne_nil {s t : String} {l : List String} (h : l ≠ [
   match l, h with
   | u::l, _ => by simp
 
+theorem intercalate_append_of_ne_nil {l m : List String} {s : String} (hl : l ≠ []) (hm : m ≠ []) :
+    s.intercalate (l ++ m) = s.intercalate l ++ s ++ s.intercalate m := by
+  induction l with
+  | nil => simp_all
+  | cons hd tl ih =>
+    rw [List.cons_append, intercalate_cons_of_ne_nil (by simp_all)]
+    by_cases ht : tl = []
+    · simp_all
+    · simp [ih ht, intercalate_cons_of_ne_nil ht, String.append_assoc]
+
 @[simp]
 theorem toList_intercalate {s : String} {l : List String} :
     (s.intercalate l).toList = s.toList.intercalate (l.map String.toList) := by
@@ -49,6 +60,23 @@ theorem toList_intercalate {s : String} {l : List String} :
   | nil => simp
   | cons hd tl ih => cases tl <;> simp_all
 
+theorem join_eq_foldl : join l = l.foldl (fun r s => r ++ s) "" :=
+  (rfl)
+
+@[simp]
+theorem join_nil : join [] = "" := by
+  simp [join]
+
+@[simp]
+theorem join_cons : join (s :: l) = s ++ join l := by
+  simp only [join, List.foldl_cons, empty_append]
+  conv => lhs; rw [← String.append_empty (s := s)]
+  rw [List.foldl_assoc]
+
+@[simp]
+theorem toList_join {l : List String} : (String.join l).toList = l.flatMap String.toList := by
+  induction l <;> simp_all
+
 namespace Slice
 
 @[simp]
@@ -65,6 +93,10 @@ theorem intercalate_eq {s : Slice} {l : List Slice} :
   | nil => simp [intercalate]
   | cons hd tl ih => cases tl <;> simp_all [intercalate, intercalate.go, intercalateGo_append]
 
+@[simp]
+theorem join_eq {l : List Slice} : join l = String.join (l.map copy) := by
+  simp [join, String.join, List.foldl_map]
+
 end Slice
 
 end String

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

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Julia Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.String.Iter.Intercalate
+public import Init.Data.String.Slice
+import all Init.Data.String.Iter.Intercalate
+import all Init.Data.String.Defs
+import Init.Data.String.Lemmas.Intercalate
+import Init.Data.Iterators.Lemmas.Consumers.Loop
+import Init.Data.Iterators.Lemmas.Combinators.FilterMap
+
+namespace Std.Iter
+
+@[simp]
+public theorem joinString_eq {α β : Type} [Std.Iterator α Id β] [Std.Iterators.Finite α Id]
+    [ToString β] {it : Std.Iter (α := α) β} :
+    it.joinString = String.join (it.toList.map toString) := by
+  rw [joinString, String.join, ← foldl_toList, toList_map]
+
+@[simp]
+public theorem intercalateString_eq {α β : Type} [Std.Iterator α Id β] [Std.Iterators.Finite α Id]
+    [ToString β] {s : String.Slice} {it : Std.Iter (α := α) β} :
+    it.intercalateString s = s.copy.intercalate (it.toList.map toString) := by
+  simp only [intercalateString, String.appendSlice_eq, ← foldl_toList, toList_map]
+  generalize s.copy = s
+  suffices ∀ (l m : List String),
+      (l.foldl (init := if m = [] then none else some (s.intercalate m))
+        (fun | none, sl => some sl | some str, sl => some (str ++ s ++ sl))).getD ""
+        = s.intercalate (m ++ l) by
+    simpa [-foldl_toList] using this (it.toList.map toString) []
+  intro l m
+  induction l generalizing m with
+  | nil => cases m <;> simp
+  | cons hd tl ih =>
+    rw [List.append_cons, ← ih, List.foldl_cons]
+    congr
+    simp only [List.append_eq_nil_iff, List.cons_ne_self, and_false, ↓reduceIte]
+    match m with
+    | [] => simp
+    | x::xs =>
+      simp only [reduceCtorEq, ↓reduceIte, List.cons_append, Option.some.injEq]
+      rw [← List.cons_append, String.intercalate_append_of_ne_nil (by simp) (by simp),
+        String.intercalate_singleton]
+
+end Std.Iter

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

@@ -23,6 +23,7 @@ import Init.Data.String.OrderInstances
 import Init.Data.String.Lemmas.Order
 import Init.Data.String.Lemmas.Intercalate
 import Init.Data.List.SplitOn.Lemmas
+import Init.Data.String.Lemmas.Slice
 
 public section
 
@@ -70,6 +71,11 @@ theorem Slice.toList_split_intercalate {c : Char} {l : List Slice} (hl : ∀ s
   · simp_all
   · rw [List.splitOn_intercalate] <;> simp_all
 
+theorem Slice.toList_split_intercalate_beq {c : Char} {l : List Slice} (hl : ∀ s ∈ l, c ∉ s.copy.toList) :
+    ((Slice.intercalate (String.singleton c) l).split c).toList ==
+      if l = [] then ["".toSlice] else l := by
+  split <;> simp_all [toList_split_intercalate hl, beq_list_iff]
+
 theorem toList_split_intercalate {c : Char} {l : List String} (hl : ∀ s ∈ l, c ∉ s.toList) :
     ((String.intercalate (String.singleton c) l).split c).toList.map (·.copy) =
       if l = [] then [""] else l := by
@@ -78,4 +84,9 @@ theorem toList_split_intercalate {c : Char} {l : List String} (hl : ∀ s ∈ l,
   · simp_all
   · rw [List.splitOn_intercalate] <;> simp_all
 
+theorem toList_split_intercalate_beq {c : Char} {l : List String} (hl : ∀ s ∈ l, c ∉ s.toList) :
+    ((String.intercalate (String.singleton c) l).split c).toList ==
+      if l = [] then ["".toSlice] else l.map String.toSlice := by
+  split <;> simp_all [toList_split_intercalate hl, Slice.beq_list_iff]
+
 end String

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

@@ -8,6 +8,8 @@ module
 prelude
 public import Init.Data.String.Search
 import all Init.Data.String.Search
+import Init.Data.String.Lemmas.Slice
+import Init.Data.String.Lemmas.FindPos
 
 public section
 
@@ -28,4 +30,42 @@ theorem Pos.le_find {s : String} (pos : s.Pos) (pattern : ρ) [ToForwardSearcher
     pos ≤ pos.find pattern := by
   simp [Pos.find, ← toSlice_le]
 
+@[simp]
+theorem front?_toSlice {s : String} : s.toSlice.front? = s.front? :=
+  (rfl)
+
+theorem front?_eq_get? {s : String} : s.front? = s.startPos.get? := by
+  simp [← front?_toSlice, ← Pos.get?_toSlice, Slice.front?_eq_get?]
+
+theorem front?_eq {s : String} : s.front? = s.toList.head? := by
+  simp [← front?_toSlice, Slice.front?_eq]
+
+@[simp]
+theorem front_toSlice {s : String} : s.toSlice.front = s.front :=
+  (rfl)
+
+@[simp]
+theorem front_eq {s : String} : s.front = s.front?.getD default := by
+  simp [← front_toSlice, Slice.front_eq]
+
+@[simp]
+theorem back?_toSlice {s : String} : s.toSlice.back? = s.back? :=
+  (rfl)
+
+theorem back?_eq_get? {s : String} : s.back? = s.endPos.prev?.bind Pos.get? := by
+  simp only [← back?_toSlice, Slice.back?_eq_get?, endPos_toSlice, Slice.Pos.prev?_eq_dif,
+    startPos_toSlice, Pos.toSlice_inj, Pos.prev?_eq_dif]
+  split <;> simp [← Pos.get?_toSlice, Pos.toSlice_prev]
+
+theorem back?_eq {s : String} : s.back? = s.toList.getLast? := by
+  simp [← back?_toSlice, Slice.back?_eq]
+
+@[simp]
+theorem back_toSlice {s : String} : s.toSlice.back = s.back :=
+  (rfl)
+
+@[simp]
+theorem back_eq {s : String} : s.back = s.back?.getD default := by
+  simp [← back_toSlice, Slice.back_eq]
+
 end String

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

@@ -11,6 +11,8 @@ import all Init.Data.String.Slice
 import Init.Data.String.Lemmas.Pattern.Memcmp
 import Init.Data.String.Lemmas.Basic
 import Init.Data.ByteArray.Lemmas
+import Init.Data.String.Lemmas.IsEmpty
+import Init.Data.String.Lemmas.FindPos
 
 public section
 
@@ -33,9 +35,104 @@ theorem beq_eq_true_iff {s t : Slice} : s == t ↔ s.copy = t.copy := by
 theorem beq_eq_false_iff {s t : Slice} : (s == t) = false ↔ s.copy ≠ t.copy := by
   simp [← Bool.not_eq_true]
 
-theorem beq_eq_decide {s t : Slice} : (s == t) = decide (s.copy = t.copy) := by
-  cases h : s == t <;> simp_all
+theorem beq_eq_decide {s t : Slice} : (s == t) = decide (s.copy = t.copy) :=
+  Bool.eq_iff_iff.2 (by simp)
+
+instance : EquivBEq String.Slice :=
+  equivBEq_of_iff_apply_eq copy (by simp)
+
+theorem beq_list_iff {l l' : List String.Slice} : l == l' ↔ l.map copy = l'.map copy := by
+  induction l generalizing l' <;> cases l' <;> simp_all
+
+theorem beq_list_eq_false_iff {l l' : List String.Slice} :
+    (l == l') = false ↔ l.map copy ≠ l'.map copy := by
+  simp [← Bool.not_eq_true, beq_list_iff]
+
+theorem beq_list_eq_decide {l l' : List String.Slice} :
+    (l == l') = decide (l.map copy = l'.map copy) :=
+  Bool.eq_iff_iff.2 (by simp [beq_list_iff])
 
 end BEq
 
-end String.Slice
+namespace Pos
+
+theorem get?_eq_dif {s : Slice} {p : s.Pos} : p.get? = if h : p = s.endPos then none else some (p.get h) :=
+  (rfl)
+
+theorem get?_eq_some_get {s : Slice} {p : s.Pos} (h : p ≠ s.endPos) : p.get? = some (p.get h) := by
+  simp [Pos.get?, h]
+
+@[simp]
+theorem get?_eq_none_iff {s : Slice} {p : s.Pos} : p.get? = none ↔ p = s.endPos := by
+  simp [Pos.get?]
+
+theorem get?_eq_none {s : Slice} {p : s.Pos} (h : p = s.endPos) : p.get? = none :=
+  get?_eq_none_iff.2 h
+
+@[simp]
+theorem get?_endPos {s : Slice} : s.endPos.get? = none := by
+  simp
+
+end Pos
+
+end Slice
+
+namespace Pos
+
+theorem get?_toSlice {s : String} {p : s.Pos} : p.toSlice.get? = p.get? :=
+  (rfl)
+
+theorem get?_eq_dif {s : String} {p : s.Pos} : p.get? = if h : p = s.endPos then none else some (p.get h) := by
+  simp [← get?_toSlice, Slice.Pos.get?_eq_dif]
+
+theorem get?_eq_some_get {s : String} {p : s.Pos} (h : p ≠ s.endPos) : p.get? = some (p.get h) := by
+  simpa [← get?_toSlice] using Slice.Pos.get?_eq_some_get (by simpa)
+
+@[simp]
+theorem get?_eq_none_iff {s : String} {p : s.Pos} : p.get? = none ↔ p = s.endPos := by
+  simp [← get?_toSlice]
+
+theorem get?_eq_none {s : String} {p : s.Pos} (h : p = s.endPos) : p.get? = none :=
+  get?_eq_none_iff.2 h
+
+@[simp]
+theorem get?_endPos {s : String} : s.endPos.get? = none := by
+  simp
+
+end Pos
+
+namespace Slice
+
+theorem front?_eq_get? {s : Slice} : s.front? = s.startPos.get? :=
+  (rfl)
+
+theorem front?_eq {s : Slice} : s.front? = s.copy.toList.head? := by
+  simp only [front?_eq_get?, Pos.get?_eq_dif]
+  split
+  · simp_all [startPos_eq_endPos_iff, eq_comm (a := none)]
+  · rename_i h
+    obtain ⟨t, ht⟩ := s.splits_startPos.exists_eq_singleton_append h
+    simp [ht]
+
+@[simp]
+theorem front_eq {s : Slice} : s.front = s.front?.getD default := by
+  simp [front]
+
+theorem back?_eq_get? {s : Slice} : s.back? = s.endPos.prev?.bind Pos.get? :=
+  (rfl)
+
+theorem back?_eq {s : Slice} : s.back? = s.copy.toList.getLast? := by
+  simp [back?_eq_get?, Pos.prev?_eq_dif]
+  split
+  · simp_all [startPos_eq_endPos_iff, eq_comm (a := s.endPos), eq_comm (a := none)]
+  · rename_i h
+    obtain ⟨t, ht⟩ := s.splits_endPos.exists_eq_append_singleton_of_ne_startPos h
+    simp [ht, Pos.get?_eq_some_get]
+
+@[simp]
+theorem back_eq {s : Slice} : s.back = s.back?.getD default := by
+  simp [back]
+
+end Slice
+
+end String

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

@@ -17,6 +17,8 @@ import Init.Data.String.OrderInstances
 import Init.Data.Nat.Order
 import Init.Omega
 import Init.Data.String.Lemmas.FindPos
+import Init.Data.List.TakeDrop
+import Init.Data.List.Nat.TakeDrop
 
 /-!
 # `Splits` predicates on `String.Pos` and `String.Slice.Pos`.
@@ -649,4 +651,51 @@ theorem Slice.splits_slice {s : Slice} {p₀ p₁ : s.Pos} (h) (p : (s.slice p
     p.Splits (s.slice p₀ (Pos.ofSlice p) Pos.le_ofSlice).copy (s.slice (Pos.ofSlice p) p₁ Pos.ofSlice_le).copy := by
   simpa using p.splits
 
+theorem Slice.Pos.Splits.nextn {s : Slice} {t₁ t₂ : String} {p : s.Pos} (h : p.Splits t₁ t₂) (n : Nat) :
+    (p.nextn n).Splits (t₁ ++ String.ofList (t₂.toList.take n)) (String.ofList (t₂.toList.drop n)) := by
+  induction n generalizing p t₁ t₂ with
+  | zero => simpa
+  | succ n ih =>
+    rw [Pos.nextn_add_one]
+    split
+    · simp_all
+    · obtain ⟨t₂, rfl⟩ := h.exists_eq_singleton_append ‹_›
+      simpa [← append_assoc] using ih h.next
+
+theorem Slice.splits_nextn_startPos (s : Slice) (n : Nat) :
+    (s.startPos.nextn n).Splits (String.ofList (s.copy.toList.take n)) (String.ofList (s.copy.toList.drop n)) := by
+  simpa using s.splits_startPos.nextn n
+
+theorem Pos.Splits.nextn {s t₁ t₂ : String} {p : s.Pos} (h : p.Splits t₁ t₂) (i : Nat) :
+    (p.nextn i).Splits (t₁ ++ String.ofList (t₂.toList.take i)) (String.ofList (t₂.toList.drop i)) := by
+  simpa [← splits_toSlice_iff, toSlice_nextn] using h.toSlice.nextn i
+
+theorem splits_nextn_startPos (s : String) (n : Nat) :
+    (s.startPos.nextn n).Splits (String.ofList (s.toList.take n)) (String.ofList (s.toList.drop n)) := by
+  simpa using s.splits_startPos.nextn n
+
+theorem Slice.Pos.Splits.prevn {s : Slice} {t₁ t₂ : String} {p : s.Pos} (h : p.Splits t₁ t₂) (n : Nat) :
+    (p.prevn n).Splits (String.ofList (t₁.toList.take (t₁.length - n))) (String.ofList (t₁.toList.drop (t₁.length - n)) ++ t₂) := by
+  induction n generalizing p t₁ t₂ with
+  | zero => simpa [← String.length_toList]
+  | succ n ih =>
+    rw [Pos.prevn_add_one]
+    split
+    · simp_all
+    · obtain ⟨t₂, rfl⟩ := h.exists_eq_append_singleton_of_ne_startPos ‹_›
+      simpa [Nat.add_sub_add_right, List.take_append, List.drop_append, ← append_assoc] using ih h.prev
+
+theorem Slice.splits_prevn_endPos (s : Slice) (n : Nat) :
+    (s.endPos.prevn n).Splits (String.ofList (s.copy.toList.take (s.copy.length - n)))
+      (String.ofList (s.copy.toList.drop (s.copy.length - n))) := by
+  simpa using s.splits_endPos.prevn n
+
+theorem Pos.Splits.prevn {s t₁ t₂ : String} {p : s.Pos} (h : p.Splits t₁ t₂) (n : Nat) :
+    (p.prevn n).Splits (String.ofList (t₁.toList.take (t₁.length - n))) (String.ofList (t₁.toList.drop (t₁.length - n)) ++ t₂) := by
+  simpa [← splits_toSlice_iff, toSlice_prevn] using h.toSlice.prevn n
+
+theorem splits_prevn_endPos (s : String) (n : Nat) :
+    (s.endPos.prevn n).Splits (String.ofList (s.toList.take (s.length - n))) (String.ofList (s.toList.drop (s.length - n))) := by
+  simpa using s.splits_endPos.prevn n
+
 end String

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

@@ -0,0 +1,86 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Julia Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.String.TakeDrop
+import all Init.Data.String.Slice
+import all Init.Data.String.TakeDrop
+import Init.Data.String.Lemmas.Splits
+
+public section
+
+namespace String
+
+namespace Slice
+
+theorem drop_eq_sliceFrom {s : Slice} {n : Nat} : s.drop n = s.sliceFrom (s.startPos.nextn n) :=
+  (rfl)
+
+@[simp]
+theorem toList_copy_drop {s : Slice} {n : Nat} : (s.drop n).copy.toList = s.copy.toList.drop n := by
+  simp [drop_eq_sliceFrom, (s.splits_nextn_startPos n).copy_sliceFrom_eq]
+
+theorem dropEnd_eq_sliceTo {s : Slice} {n : Nat} : s.dropEnd n = s.sliceTo (s.endPos.prevn n) :=
+  (rfl)
+
+@[simp]
+theorem toList_copy_dropEnd {s : Slice} {n : Nat} :
+    (s.dropEnd n).copy.toList = s.copy.toList.take (s.copy.length - n) := by
+  simp [dropEnd_eq_sliceTo, (s.splits_prevn_endPos n).copy_sliceTo_eq]
+
+theorem take_eq_sliceTo {s : Slice} {n : Nat} : s.take n = s.sliceTo (s.startPos.nextn n) :=
+  (rfl)
+
+@[simp]
+theorem toList_copy_take {s : Slice} {n : Nat} : (s.take n).copy.toList = s.copy.toList.take n := by
+  simp [take_eq_sliceTo, (s.splits_nextn_startPos n).copy_sliceTo_eq]
+
+theorem takeEnd_eq_sliceFrom {s : Slice} {n : Nat} : s.takeEnd n = s.sliceFrom (s.endPos.prevn n) :=
+  (rfl)
+
+@[simp]
+theorem toList_copy_takeEnd {s : Slice} {n : Nat} :
+    (s.takeEnd n).copy.toList = s.copy.toList.drop (s.copy.length - n) := by
+  simp [takeEnd_eq_sliceFrom, (s.splits_prevn_endPos n).copy_sliceFrom_eq]
+
+end Slice
+
+@[simp]
+theorem drop_toSlice {s : String} {n : Nat} : s.toSlice.drop n = s.drop n :=
+  (rfl)
+
+@[simp]
+theorem toList_copy_drop {s : String} {n : Nat} : (s.drop n).copy.toList = s.toList.drop n := by
+  simp [← drop_toSlice]
+
+@[simp]
+theorem dropEnd_toSlice {s : String} {n : Nat} : s.toSlice.dropEnd n = s.dropEnd n :=
+  (rfl)
+
+@[simp]
+theorem toList_copy_dropEnd {s : String} {n : Nat} :
+    (s.dropEnd n).copy.toList = s.toList.take (s.length - n) := by
+  simp [← dropEnd_toSlice]
+
+@[simp]
+theorem take_toSlice {s : String} {n : Nat} : s.toSlice.take n = s.take n :=
+  (rfl)
+
+@[simp]
+theorem toList_copy_take {s : String} {n : Nat} : (s.take n).copy.toList = s.toList.take n := by
+  simp [← take_toSlice]
+
+@[simp]
+theorem takeEnd_toSlice {s : String} {n : Nat} : s.toSlice.takeEnd n = s.takeEnd n :=
+  (rfl)
+
+@[simp]
+theorem toList_copy_takeEnd {s : String} {n : Nat} :
+    (s.takeEnd n).copy.toList = s.toList.drop (s.length - n) := by
+  simp [← takeEnd_toSlice]
+
+end String

src/Init/Data/String/Slice.lean

@@ -11,7 +11,7 @@ public import Init.Data.Ord.Basic
 public import Init.Data.Iterators.Combinators.FilterMap
 public import Init.Data.String.ToSlice
 public import Init.Data.String.Subslice
-public import Init.Data.String.Iter
+public import Init.Data.String.Iter.Basic
 public import Init.Data.String.Iterate
 import Init.Data.Iterators.Consumers.Collect
 import Init.Data.Iterators.Consumers.Loop
@@ -84,10 +84,11 @@ instance : ToString String.Slice where
 theorem toStringToString_eq : ToString.toString = String.Slice.copy := (rfl)
 
 @[extern "lean_slice_hash"]
-opaque hash (s : @& Slice) : UInt64
+protected def hash (s : @& Slice) : UInt64 :=
+  String.hash s.copy
 
 instance : Hashable Slice where
-  hash := hash
+  hash := Slice.hash
 
 instance : LT Slice where
   lt x y := x.copy < y.copy
@@ -1151,6 +1152,19 @@ where go (acc : String) (s : Slice) : List Slice → String
   | a :: as => go (acc ++ s ++ a) s as
   | []      => acc
 
+/--
+Appends all the slices in a list of slices, in order.
+
+Use {name}`String.Slice.intercalate` to place a separator string between the strings in a list.
+
+Examples:
+ * {lean}`String.Slice.join ["gr", "ee", "n"] = "green"`
+ * {lean}`String.Slice.join ["b", "", "l", "", "ue"] = "blue"`
+ * {lean}`String.Slice.join [] = ""`
+-/
+def join (l : List String.Slice) : String :=
+  l.foldl (fun (r : String) (s : String.Slice) => r ++ s) ""
+
 /--
 Converts a string to the Lean compiler's representation of names. The resulting name is
 hierarchical, and the string is split at the dots ({lean}`'.'`).

src/Init/Grind/Interactive.lean

@@ -107,6 +107,9 @@ syntax (name := showLocalThms) "show_local_thms" : grind
 -/
 syntax (name := showTerm) "show_term " grindSeq : grind
 
+/-- Shows the pending goals. -/
+syntax (name := showGoals) "show_goals" : grind
+
 declare_syntax_cat grind_ref (behavior := both)
 
 syntax:max anchor : grind_ref
@@ -315,5 +318,8 @@ Only available in `sym =>` mode.
 -/
 syntax (name := symSimp) "simp" (ppSpace colGt ident)? (" [" ident,* "]")? : grind
 
+/-- `exact e` closes the main goal if its target type matches that of `e`. -/
+macro "exact " e:term : grind => `(grind| tactic => exact $e:term)
+
 end Grind
 end Lean.Parser.Tactic

src/Init/Prelude.lean

@@ -185,15 +185,21 @@ example : foo.default = (default, default) :=
 abbrev inferInstance {α : Sort u} [i : α] : α := i
 
 set_option checkBinderAnnotations false in
-/-- `inferInstanceAs α` synthesizes an instance of type `α` and normalizes it to
-"instance normal form": the result is a constructor application whose sub-instance fields
-are canonical instances and whose types match `α` exactly. This is useful when `α` is
-definitionally equal to some `α'` for which instances are registered, as it prevents
-leaking the definition's RHS at lower transparencies. See `Lean.Meta.InstanceNormalForm`
-for details. Example:
+/-- `inferInstanceAs α` synthesizes an instance of type `α`, transporting it from a
+definitionally equal type if necessary. This is useful when `α` is definitionally equal to
+some `α'` for which instances are registered, as it prevents leaking the definition's RHS
+at lower transparencies.
+
+`inferInstanceAs` requires an expected type from context. If you just need to synthesize an
+instance without transporting between types, use `inferInstance` instead.
+
+Example:
 ```
-#check inferInstanceAs (Inhabited Nat) -- Inhabited Nat
+def D := Nat
+instance : Inhabited D := inferInstanceAs (Inhabited Nat)
 ```
+
+See `Lean.Meta.WrapInstance` for details.
 -/
 abbrev «inferInstanceAs» (α : Sort u) [i : α] : α := i
 
@@ -3261,7 +3267,7 @@ Version of `Array.get!Internal` that does not increment the reference count of i
 This is only intended for direct use by the compiler.
 -/
 @[extern "lean_array_get_borrowed"]
-unsafe opaque Array.get!InternalBorrowed {α : Type u} [Inhabited α] (a : @& Array α) (i : @& Nat) : α
+unsafe opaque Array.get!InternalBorrowed {α : Type u} [@&Inhabited α] (a : @& Array α) (i : @& Nat) : α
 
 /--
 Use the indexing notation `a[i]!` instead.
@@ -3269,7 +3275,7 @@ Use the indexing notation `a[i]!` instead.
 Access an element from an array, or panic if the index is out of bounds.
 -/
 @[extern "lean_array_get"]
-def Array.get!Internal {α : Type u} [Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
+def Array.get!Internal {α : Type u} [@&Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
   Array.getD a i default
 
 /--
@@ -3648,8 +3654,8 @@ will prevent the actual monad from being "copied" to the code being specialized.
 When we reimplement the specializer, we may consider copying `inst` if it also
 occurs outside binders or if it is an instance.
 -/
-@[never_extract, extern "lean_panic_fn"]
-def panicCore {α : Sort u} [Inhabited α] (msg : String) : α := default
+@[never_extract, extern "lean_panic_fn_borrowed"]
+def panicCore {α : Sort u} [@&Inhabited α] (msg : String) : α := default
 
 /--
 `(panic "msg" : α)` has a built-in implementation which prints `msg` to
@@ -4082,7 +4088,7 @@ Actions in the resulting monad are functions that take the local value as a para
 ordinary actions in `m`.
 -/
 def ReaderT (ρ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
-  ρ → m α
+  (a : @&ρ) → m α
 
 /--
 Interpret `ρ → m α` as an element of `ReaderT ρ m α`.

src/Init/Sym/Simp/SimprocDSL.lean

@@ -49,6 +49,14 @@ syntax (name := ground) "ground" : sym_simproc
 /-- Simplify telescope binders but not the final body. -/
 syntax (name := telescope) "telescope" : sym_simproc
 
+/-- Simplify control-flow expressions (`if-then-else`, `match`, `cond`, `dite`).
+Visits only conditions and discriminants. Intended as a `pre` simproc. -/
+syntax (name := control) "control" : sym_simproc
+
+/-- Simplify arrow telescopes (`p₁ → p₂ → ... → q`) without entering binders.
+Simplifies each `pᵢ` and `q` individually. Intended as a `pre` simproc. -/
+syntax (name := arrowTelescope) "arrow_telescope" : sym_simproc
+
 /-- Rewrite using a named theorem set. Optionally specify a discharger for conditional rewrites. -/
 syntax (name := rewriteSet) "rewrite" ident (" with " sym_discharger)? : sym_simproc
 

src/Init/Tactics.lean

@@ -2259,42 +2259,6 @@ with grind
 ```
 This is more convenient than the equivalent `· by rename_i _ acc _; exact I1 acc`.
 
-### Witnesses
-
-When a specification has a parameter whose type is tagged with `@[mvcgen_witness_type]`, `mvcgen`
-classifies the corresponding goal as a *witness* rather than a verification condition.
-Witnesses are concrete values that the user must provide (inspired by zero-knowledge proofs),
-as opposed to invariants (predicates maintained across loop iterations) or verification conditions
-(propositions to prove).
-
-Witness goals are labelled `witness1`, `witness2`, etc. and can be provided in a `witnesses` section
-that appears before the `invariants` section:
-```
-mvcgen [...] witnesses
-· W1
-· W2
-invariants
-· I1
-with grind
-```
-Like invariants, witnesses support case label syntax:
-```
-mvcgen [...] witnesses
-| witness1 => W1
-```
-
-See the `@[mvcgen_witness_type]` attribute for how to register custom witness types.
-
-### Invariant and witness type attributes
-
-The `@[mvcgen_invariant_type]` and `@[mvcgen_witness_type]` tag attributes control how `mvcgen`
-classifies subgoals:
-* A goal whose type is an application of a type tagged with `@[mvcgen_invariant_type]` is classified
-  as an invariant (`inv<n>`).
-* A goal whose type is an application of a type tagged with `@[mvcgen_witness_type]` is classified
-  as a witness (`witness<n>`).
-* All other goals are classified as verification conditions (`vc<n>`).
-
 ### Invariant suggestions
 
 `mvcgen` will suggest invariants for you if you use the `invariants?` keyword.

src/Lean/Compiler/IR/AddExtern.lean

@@ -21,6 +21,7 @@ public section
 
 namespace Lean.IR
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_add_extern]
 def addExtern (declName : Name) (externAttrData : ExternAttrData) : CoreM Unit := do
   if !isPrivateName declName then

src/Lean/Compiler/IR/CompilerM.lean

@@ -10,6 +10,7 @@ public import Lean.Compiler.IR.Format
 public import Lean.Compiler.ExportAttr
 public import Lean.Compiler.LCNF.PublicDeclsExt
 import Lean.Compiler.InitAttr
+import all Lean.Compiler.ModPkgExt
 import Init.Data.Format.Macro
 import Lean.Compiler.LCNF.Basic
 
@@ -129,8 +130,14 @@ private def exportIREntries (env : Environment) : Array (Name × Array EnvExtens
   -- safety: cast to erased type
   let initDecls : Array EnvExtensionEntry := unsafe unsafeCast initDecls
 
+  -- needed during initialization via interpreter
+  let modPkg : Array (Option PkgId) := modPkgExt.exportEntriesFn env (modPkgExt.getState env) .private
+  -- safety: cast to erased type
+  let modPkg : Array EnvExtensionEntry := unsafe unsafeCast modPkg
+
   #[(declMapExt.name, irEntries),
-    (Lean.regularInitAttr.ext.name, initDecls)]
+    (Lean.regularInitAttr.ext.name, initDecls),
+    (modPkgExt.name, modPkg)]
 
 def findEnvDecl (env : Environment) (declName : Name) : Option Decl :=
   Compiler.LCNF.findExtEntry? env declMapExt declName findAtSorted? (·.2.find?)

src/Lean/Compiler/LCNF/Basic.lean

@@ -342,6 +342,11 @@ def LetValue.toExpr (e : LetValue pu) : Expr :=
   | .unbox var _ => mkApp (.const `unbox []) (.fvar var)
   | .isShared fvarId _ => mkApp (.const `isShared []) (.fvar fvarId)
 
+def LetValue.isPersistent (val : LetValue .impure) : Bool :=
+  match val with
+  | .fap _ xs => xs.isEmpty -- all global constants are persistent
+  | _ => false
+
 structure LetDecl (pu : Purity) where
   fvarId : FVarId
   binderName : Name

src/Lean/Compiler/LCNF/ExplicitRC.lean

@@ -97,6 +97,7 @@ partial def collectCode (code : Code .impure) : M Unit := do
     match decl.value with
     | .oproj _ parent =>
       addDerivedValue parent decl.fvarId
+    -- Keep in sync with PropagateBorrow, InferBorrow
     | .fap ``Array.getInternal args =>
       if let .fvar parent := args[1]! then
         addDerivedValue parent decl.fvarId
@@ -234,11 +235,6 @@ def withParams (ps : Array (Param .impure)) (x : RcM α) : RcM α := do
       { ctx with idx := ctx.idx + 1, varMap }
   withReader update x
 
-def LetValue.isPersistent (val : LetValue .impure) : Bool :=
-  match val with
-  | .fap _ xs => xs.isEmpty -- all global constants are persistent
-  | _ => false
-
 @[inline]
 def withLetDecl (decl : LetDecl .impure) (x : RcM α) : RcM α := do
   let update := fun ctx =>

src/Lean/Compiler/LCNF/InferBorrow.lean

@@ -213,6 +213,8 @@ inductive OwnReason where
   | jpArgPropagation (jpFVar : FVarId)
   /-- Tail call preservation at a join point jump. -/
   | jpTailCallPreservation (jpFVar : FVarId)
+  /-- Annotated as an owned parameter (currently only triggerable through `@[export]`)-/
+  | ownedAnnotation
 
 def OwnReason.toString (reason : OwnReason) : CompilerM String := do
   PP.run do
@@ -229,6 +231,7 @@ def OwnReason.toString (reason : OwnReason) : CompilerM String := do
     | .tailCallPreservation funcName => return s!"tail call preservation of {funcName}"
     | .jpArgPropagation jpFVar => return s!"backward propagation from JP {← PP.ppFVar jpFVar}"
     | .jpTailCallPreservation jpFVar => return s!"JP tail call preservation {← PP.ppFVar jpFVar}"
+    | .ownedAnnotation => return s!"Annotated as owned"
 
 /--
 Determine whether an `OwnReason` is necessary for correctness (forced) or just an optimization
@@ -240,13 +243,19 @@ def OwnReason.isForced (reason : OwnReason) : Bool :=
   -- All of these reasons propagate through ABI decisions and can thus safely be ignored as they
   -- will be accounted for by the reference counting pass.
   | .constructorArg .. | .functionCallArg .. | .fvarCall .. | .partialApplication ..
-  | .jpArgPropagation .. => false
+  | .jpArgPropagation ..
+  -- forward propagation can never affect a user-annotated parameter
+  | .forwardProjectionProp ..
+  -- backward propagation on a user-annotated parameter is only necessary if the projected value
+  -- directly flows into a reset-reuse. However, the borrow annotation propagator ensures this
+  -- situation never arises
+  | .backwardProjectionProp .. => false
   -- Results of functions and constructors are naturally owned.
   | .constructorResult .. | .functionCallResult ..
   -- We cannot pass borrowed values to reset or have borrow annotations destroy tail calls for
   -- correctness reasons.
   | .resetReuse .. | .tailCallPreservation .. | .jpTailCallPreservation ..
-  | .forwardProjectionProp .. | .backwardProjectionProp .. => true
+  | .ownedAnnotation => true
 
 /--
 Infer the borrowing annotations in a SCC through dataflow analysis.
@@ -256,10 +265,19 @@ partial def infer (decls : Array (Decl .impure)) : CompilerM ParamMap := do
   return map.paramMap
 where
   go : InferM Unit := do
+    for (_, params) in (← get).paramMap.map do
+      for param in params do
+        if !param.borrow && param.type.isPossibleRef then
+          -- if the param already disqualifies as borrow now this is because of an annotation
+          ownFVar param.fvarId .ownedAnnotation
+    modify fun s => { s with modified := false }
+    loop
+
+  loop : InferM Unit := do
     step
     if (← get).modified then
       modify fun s => { s with modified := false }
-      go
+      loop
     else
       return ()
 
@@ -361,10 +379,23 @@ where
     | .oproj _ x _ =>
       if ← isOwned x then ownFVar z (.forwardProjectionProp z)
       if ← isOwned z then ownFVar x (.backwardProjectionProp z)
+    -- Keep in sync with ExplicitRC, PropagateBorrow
+    | .fap ``Array.getInternal args =>
+      if let .fvar parent := args[1]! then
+        if ← isOwned parent then ownFVar z (.forwardProjectionProp z)
+    | .fap ``Array.get!Internal args =>
+      if let .fvar parent := args[2]! then
+        if ← isOwned parent then ownFVar z (.forwardProjectionProp z)
+    | .fap ``Array.uget args =>
+      if let .fvar parent := args[1]! then
+        if ← isOwned parent then ownFVar z (.forwardProjectionProp z)
     | .fap f args =>
-      let ps ← getParamInfo (.decl f)
-      ownFVar z (.functionCallResult z)
-      ownArgsUsingParams args ps (.functionCallArg z)
+      -- Constants remain alive at least until the end of execution and can thus effectively be seen
+      -- as a "borrowed" read.
+      if args.size > 0 then
+        let ps ← getParamInfo (.decl f)
+        ownFVar z (.functionCallResult z)
+        ownArgsUsingParams args ps (.functionCallArg z)
     | .fvar x args =>
       ownFVar z (.functionCallResult z); ownFVar x (.fvarCall z); ownArgs (.fvarCall z) args
     | .pap _ args => ownFVar z (.functionCallResult z); ownArgs (.partialApplication z) args

src/Lean/Compiler/LCNF/OtherDecl.lean

@@ -21,6 +21,6 @@ def getOtherDeclType (declName : Name) (us : List Level := []) : CompilerM Expr
   match (← getPhase) with
   | .base => getOtherDeclBaseType declName us
   | .mono => getOtherDeclMonoType declName
-  | .impure => getOtherDeclImpureType declName
+  | .impure => throwError "getOtherDeclType unsupported for impure"
 
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/PrettyPrinter.lean

@@ -154,16 +154,18 @@ mutual
       return f!"oset {← ppFVar fvarId} [{i}] := {← ppArg y};" ++ .line ++ (← ppCode k)
     | .setTag fvarId cidx k _ =>
       return f!"setTag {← ppFVar fvarId} := {cidx};" ++ .line ++ (← ppCode k)
-    | .inc fvarId n _ _ k _ =>
+    | .inc fvarId n check persistent k _ =>
+      let ann := (if persistent then "[persistent]" else "") ++ (if !check then "[ref]" else "")
       if n != 1 then
-        return f!"inc[{n}] {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
+        return f!"inc[{n}]{ann} {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
       else
-        return f!"inc {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
-    | .dec fvarId n _ _ k _ =>
+        return f!"inc{ann} {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
+    | .dec fvarId n check persistent k _ =>
+      let ann := (if persistent then "[persistent]" else "") ++ (if !check then "[ref]" else "")
       if n != 1 then
-        return f!"dec[{n}] {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
+        return f!"dec[{n}]{ann} {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
       else
-        return f!"dec {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
+        return f!"dec{ann} {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
     | .del fvarId k _ =>
       return f!"del {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
 

src/Lean/Compiler/LCNF/PropagateBorrow.lean

@@ -105,10 +105,26 @@ where
 
   collectLetValue (z : FVarId) (v : LetValue .impure) : InferM Unit := do
     match v with
-    | .oproj _ x _ =>
-      let xVal ← getOwnedness x
-      join z xVal
-    | .ctor .. | .fap .. | .fvar .. | .pap .. | .sproj .. | .uproj .. | .erased .. | .lit .. =>
+    | .oproj _ parent _ =>
+      let parentVal ← getOwnedness parent
+      join z parentVal
+    -- Keep in sync with ExplicitRC, InferBorrow
+    | .fap ``Array.getInternal args =>
+      if let .fvar parent := args[1]! then
+        let parentVal ← getOwnedness parent
+        join z parentVal
+    | .fap ``Array.get!Internal args =>
+      if let .fvar parent := args[2]! then
+        let parentVal ← getOwnedness parent
+        join z parentVal
+    | .fap ``Array.uget args =>
+      if let .fvar parent := args[1]! then
+        let parentVal ← getOwnedness parent
+        join z parentVal
+    | .fap _ args =>
+      let value := if args.isEmpty then .borrow else .own
+      join z value
+    | .ctor .. | .fvar .. | .pap .. | .sproj .. | .uproj .. | .erased .. | .lit .. =>
       join z .own
     | _ => unreachable!
 

src/Lean/Compiler/LCNF/ToImpureType.lean

@@ -240,12 +240,4 @@ where fillCache := do
       fieldInfo := fields
     }
 
-public def getOtherDeclImpureType (declName : Name) : CoreM Expr := do
-  match (← impureTypeExt.find? declName) with
-  | some type => return type
-  | none =>
-    let type ← toImpureType (← getOtherDeclMonoType declName)
-    monoTypeExt.insert declName type
-    return type
-
 end Lean.Compiler.LCNF

src/Lean/CoreM.lean

@@ -343,13 +343,13 @@ def instantiateTypeLevelParams (c : ConstantVal) (us : List Level) : CoreM Expr
   modifyInstLevelTypeCache fun s => s.insert c.name (us, r)
   return r
 
-def instantiateValueLevelParams (c : ConstantInfo) (us : List Level) : CoreM Expr := do
+def instantiateValueLevelParams (c : ConstantInfo) (us : List Level) (allowOpaque := false) : CoreM Expr := do
   if let some (us', r) := (← get).cache.instLevelValue.find? c.name then
     if us == us' then
       return r
-  unless c.hasValue do
+  unless c.hasValue (allowOpaque := allowOpaque) do
     throwError "Not a definition or theorem: {.ofConstName c.name}"
-  let r := c.instantiateValueLevelParams! us
+  let r := c.instantiateValueLevelParams! us (allowOpaque := allowOpaque)
   modifyInstLevelValueCache fun s => s.insert c.name (us, r)
   return r
 

src/Lean/Declaration.lean

@@ -14,29 +14,35 @@ public section
 
 namespace Lean
 /--
-Reducibility hints are used in the convertibility checker.
-When trying to solve a constraint such a
+Reducibility hints guide the kernel's *lazy delta reduction* strategy. When the kernel encounters a
+definitional equality constraint
 
            (f ...) =?= (g ...)
 
-where f and g are definitions, the checker has to decide which one will be unfolded.
-  If      f (g) is opaque,     then g (f) is unfolded if it is also not marked as opaque,
-  Else if f (g) is abbrev,     then f (g) is unfolded if g (f) is also not marked as abbrev,
-  Else if f and g are regular, then we unfold the one with the biggest definitional height.
-  Otherwise both are unfolded.
+where `f` and `g` are definitions, it must decide which side to unfold. The rules (implemented in
+`lazy_delta_reduction_step` in `src/kernel/type_checker.cpp`) are:
 
-The arguments of the `regular` Constructor are: the definitional height and the flag `selfOpt`.
+* If `f` and `g` have the **same hint kind**:
+  - Both `.opaque` or both `.abbrev`: unfold both.
+  - Both `.regular`: unfold the one with the **greater** height first. If their heights are equal
+    (in particular, if `f` and `g` are the same definition), first try to compare their arguments
+    for definitional equality (short-circuiting the unfolding if they match), then unfold both.
+* If `f` and `g` have **different hint kinds**: unfold the one that is *not* `.opaque`, preferring to
+  unfold `.abbrev` over `.regular`.
 
-The definitional height is by default computed by the kernel. It only takes into account
-other regular definitions used in a definition. When creating declarations using meta-programming,
-we can specify the definitional depth manually.
+The `.regular` constructor carries a `UInt32` *definitional height*, which is computed by the
+elaborator as one plus the maximum height of all `.regular` constants appearing in the definition's
+body (see `getMaxHeight`). This means `.abbrev` and `.opaque` constants do not contribute to the
+height. When creating declarations via meta-programming, the height can be specified manually.
 
-Remark: the hint only affects performance. None of the hints prevent the kernel from unfolding a
-declaration during Type checking.
+The hints only affect performance — they control the order in which definitions are unfolded, but
+never prevent the kernel from unfolding a definition during type checking.
 
-Remark: the ReducibilityHints are not related to the attributes: reducible/irrelevance/semireducible.
-These attributes are used by the Elaborator. The ReducibilityHints are used by the kernel (and Elaborator).
-Moreover, the ReducibilityHints cannot be changed after a declaration is added to the kernel. -/
+The `ReducibilityHints` are not related to the `@[reducible]`/`@[irreducible]`/`@[semireducible]`
+attributes. Those attributes are used by the elaborator to control which definitions tactics like
+`simp`, `rfl`, and `dsimp` will unfold; they do not affect the kernel. Conversely,
+`ReducibilityHints` are set when a declaration is added to the kernel and cannot be changed
+afterwards. -/
 inductive ReducibilityHints where
   | opaque  : ReducibilityHints
   | abbrev  : ReducibilityHints
@@ -469,24 +475,37 @@ def numLevelParams (d : ConstantInfo) : Nat :=
 def type (d : ConstantInfo) : Expr :=
   d.toConstantVal.type
 
+/--
+Returns the value of a definition. With `allowOpaque := true`, values
+of theorems and opaque declarations are also returned.
+-/
 def value? (info : ConstantInfo) (allowOpaque := false) : Option Expr :=
   match info with
   | .defnInfo {value, ..}   => some value
-  | .thmInfo  {value, ..}   => some value
+  | .thmInfo  {value, ..}   => if allowOpaque then some value else none
   | .opaqueInfo {value, ..} => if allowOpaque then some value else none
   | _                       => none
 
+/--
+Returns `true` if this declaration as a value for the purpose of reduction
+and type-checking, i.e. is a definition.
+With `allowOpaque := true`, theorems and opaque declarations are also considered to have values.
+-/
 def hasValue (info : ConstantInfo) (allowOpaque := false) : Bool :=
   match info with
   | .defnInfo _   => true
-  | .thmInfo  _   => true
+  | .thmInfo  _   => allowOpaque
   | .opaqueInfo _ => allowOpaque
   | _             => false
 
+/--
+Returns the value of a definition. With `allowOpaque := true`, values
+of theorems and opaque declarations are also returned.
+-/
 def value! (info : ConstantInfo) (allowOpaque := false) : Expr :=
   match info with
   | .defnInfo {value, ..}   => value
-  | .thmInfo  {value, ..}   => value
+  | .thmInfo  {value, ..}   => if allowOpaque then value else panic! "declaration with value expected"
   | .opaqueInfo {value, ..} => if allowOpaque then value else panic! "declaration with value expected"
   | _                       => panic! s!"declaration with value expected, but {info.name} has none"
 
@@ -510,6 +529,10 @@ def isDefinition : ConstantInfo → Bool
   | .defnInfo _ => true
   | _           => false
 
+def isTheorem : ConstantInfo → Bool
+  | .thmInfo _ => true
+  | _          => false
+
 def inductiveVal! : ConstantInfo → InductiveVal
   | .inductInfo val => val
   | _ => panic! "Expected a `ConstantInfo.inductInfo`."

src/Lean/DefEqAttrib.lean

@@ -101,7 +101,7 @@ def inferDefEqAttr (declName : Name) : MetaM Unit := do
   withoutExporting do
     let info ← getConstInfo declName
     let isRfl ←
-      if let some value := info.value? then
+      if let some value := info.value? (allowOpaque := true) then
         isRflProofCore info.type value
       else
         pure false

src/Lean/Elab/BuiltinTerm.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Lean.Meta.Diagnostics
-public import Lean.Meta.InstanceNormalForm
+public import Lean.Meta.WrapInstance
 public import Lean.Elab.Open
 public import Lean.Elab.SetOption
 public import Lean.Elab.Eval
@@ -315,9 +315,16 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
   | _ => panic! "resolveId? returned an unexpected expression"
 
 @[builtin_term_elab Lean.Parser.Term.inferInstanceAs] def elabInferInstanceAs : TermElab := fun stx expectedType? => do
-  let expectedType ← tryPostponeIfHasMVars expectedType? "`inferInstanceAs` failed"
   -- The type argument is the last child (works for both `inferInstanceAs T` and `inferInstanceAs <| T`)
   let typeStx := stx[stx.getNumArgs - 1]!
+  if !backward.inferInstanceAs.wrap.get (← getOptions) then
+    return (← elabTerm (← `(_root_.inferInstanceAs $(⟨typeStx⟩))) expectedType?)
+
+  let some expectedType ← tryPostponeIfHasMVars? expectedType? |
+    throwError (m!"`inferInstanceAs` failed, expected type contains metavariables{indentD expectedType?}" ++
+      .note "`inferInstanceAs` requires full knowledge of the expected (\"target\") type to do its \
+        instance translation. If you do not intend to transport instances between two types, \
+        consider using `inferInstance` or `(inferInstance : expectedType)` instead.")
   let type ← withSynthesize (postpone := .yes) <| elabType typeStx
   -- Unify with expected type to resolve metavariables (e.g., `_` placeholders)
   discard <| isDefEq type expectedType
@@ -327,9 +334,10 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
   let type ← abstractInstImplicitArgs type
   let inst ← synthInstance type
   let inst ← if backward.inferInstanceAs.wrap.get (← getOptions) then
-    -- Normalize to instance normal form.
+    -- Wrap instance so its type matches the expected type exactly.
     let logCompileErrors := !(← read).isNoncomputableSection && !(← read).declName?.any (Lean.isNoncomputable (← getEnv))
-    withNewMCtxDepth <| normalizeInstance inst expectedType (logCompileErrors := logCompileErrors)
+    let isMeta := (← read).declName?.any (isMarkedMeta (← getEnv))
+    withNewMCtxDepth <| wrapInstance inst expectedType (logCompileErrors := logCompileErrors) (isMeta := isMeta)
   else
     pure inst
   ensureHasType expectedType? inst

src/Lean/Elab/Command.lean

@@ -666,7 +666,8 @@ private def mkTermContext (ctx : Context) (s : State) : CommandElabM Term.Contex
   return {
     macroStack             := ctx.macroStack
     sectionVars            := sectionVars
-    isNoncomputableSection := scope.isNoncomputable }
+    isNoncomputableSection := scope.isNoncomputable
+    isMetaSection          := scope.isMeta }
 
 /--
 Lift the `TermElabM` monadic action `x` into a `CommandElabM` monadic action.

src/Lean/Elab/Deriving/Basic.lean

@@ -9,7 +9,7 @@ prelude
 public import Lean.Elab.App
 public import Lean.Elab.DeclNameGen
 import Lean.Compiler.NoncomputableAttr
-import Lean.Meta.InstanceNormalForm
+import Lean.Meta.WrapInstance
 
 public section
 
@@ -211,19 +211,21 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) (isNoncomputable
           -- We don't reduce because of abbreviations such as `DecidableEq`
           forallTelescope classExpr fun _ classExpr => do
             let result ← mkInst classExpr declName decl value
-            -- Save the pre-normalization value for the noncomputable check below,
-            -- since `normalizeInstance` may inline noncomputable constants.
+            -- Save the pre-wrapping value for the noncomputable check below,
+            -- since `wrapInstance` may inline noncomputable constants.
             let preNormClosure ← Closure.mkValueTypeClosure result.instType result.instVal (zetaDelta := true)
-            -- Compute instance name early so `normalizeInstance` can use it for aux def naming.
+            -- Compute instance name early so `wrapInstance` can use it for aux def naming.
             let env ← getEnv
             let mut instName := (← getCurrNamespace) ++ (← NameGen.mkBaseNameWithSuffix "inst" preNormClosure.type)
             instName ← liftMacroM <| mkUnusedBaseName instName
             if isPrivateName declName then
               instName := mkPrivateName env instName
+            let isMeta := (← read).declName?.any (isMarkedMeta (← getEnv))
             let inst ← if backward.inferInstanceAs.wrap.get (← getOptions) then
               withDeclNameForAuxNaming instName <| withNewMCtxDepth <|
-                normalizeInstance result.instVal result.instType
+                wrapInstance result.instVal result.instType
                   (logCompileErrors := false)  -- covered by noncomputable check below
+                  (isMeta := isMeta)
             else
               pure result.instVal
             let closure ← Closure.mkValueTypeClosure result.instType inst (zetaDelta := true)

src/Lean/Elab/PreDefinition/Basic.lean

@@ -10,7 +10,7 @@ public import Lean.Compiler.NoncomputableAttr
 public import Lean.Util.NumApps
 public import Lean.Meta.Eqns
 public import Lean.Elab.RecAppSyntax
-public import Lean.Meta.InstanceNormalForm
+public import Lean.Meta.WrapInstance
 public import Lean.Elab.DefView
 public section
 

src/Lean/Elab/PreDefinition/Mutual.lean

@@ -63,10 +63,11 @@ def addPreDefAttributes (preDefs : Array PreDefinition) : TermElabM Unit := do
   a wrong setting and creates bad `defEq` equations.
   -/
   for preDef in preDefs do
-    unless preDef.modifiers.attrs.any fun a =>
-        a.name = `reducible || a.name = `semireducible ||
-        a.name = `instance_reducible || a.name = `implicit_reducible do
-      setIrreducibleAttribute preDef.declName
+    unless preDef.kind.isTheorem do
+      unless preDef.modifiers.attrs.any fun a =>
+          a.name = `reducible || a.name = `semireducible ||
+          a.name = `instance_reducible || a.name = `implicit_reducible do
+        setIrreducibleAttribute preDef.declName
 
   /-
   `enableRealizationsForConst` must happen before `generateEagerEqns`

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -184,6 +184,7 @@ def getUnfoldFor? (declName : Name) : MetaM (Option Name) := do
   else
     return none
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_get_structural_rec_arg_pos]
 def getStructuralRecArgPosImp? (declName : Name) : CoreM (Option Nat) := do
   let some info := eqnInfoExt.find? (← getEnv) declName | return none

src/Lean/Elab/PreDefinition/Structural/Main.lean

@@ -80,6 +80,32 @@ private def elimMutualRecursion (preDefs : Array PreDefinition) (fixedParamPerms
       withRecFunsAsAxioms preDefs do
         mkBRecOnF recArgInfos positions r values[idx]! FTypes[idx]!
   trace[Elab.definition.structural] "FArgs: {FArgs}"
+
+  -- Extract the functionals into named `_f` helper definitions (e.g. `foo._f`) so they show up
+  -- with a helpful name in kernel diagnostics. The `_f` definitions are `.abbrev` so the kernel
+  -- unfolds them eagerly; their body heights are registered via `setDefHeightOverride` so that
+  -- `getMaxHeight` computes the correct height for parent definitions.
+  -- For inductive predicates, the previous inline behavior is kept.
+  let FArgs ←
+    if isIndPred then
+      pure FArgs
+    else
+      let us := preDefs[0]!.levelParams.map mkLevelParam
+      FArgs.mapIdxM fun idx fArg => do
+        let fName := preDefs[idx]!.declName ++ `_f
+        let fValue ← eraseRecAppSyntaxExpr (← mkLambdaFVars xs fArg)
+        let fType ← Meta.letToHave (← inferType fValue)
+        let fHeight := getMaxHeight (← getEnv) fValue
+        addDecl (.defnDecl {
+          name := fName, levelParams := preDefs[idx]!.levelParams,
+          type := fType, value := fValue,
+          hints := .abbrev,
+          safety := if preDefs[idx]!.modifiers.isUnsafe then .unsafe else .safe,
+          all := [fName] })
+        modifyEnv (setDefHeightOverride · fName fHeight)
+        setReducibleAttribute fName
+        return mkAppN (mkConst fName us) xs
+
   let brecOn := brecOnConst 0
   -- the indices and the major premise are not mentioned in the minor premises
   -- so using `default` is fine here

src/Lean/Elab/Tactic/Do/Attr.lean

@@ -268,24 +268,3 @@ def isMVCGenInvariantType (env : Environment) (ty : Expr) : Bool :=
     mvcgenInvariantAttr.hasTag env name
   else
     false
-
-/--
-Marks a type as a witness type for the `mvcgen` tactic.
-Goals whose type is an application of a tagged type will be classified
-as witnesses rather than verification conditions.
-In the spirit of zero-knowledge proofs, witnesses are concrete values that the user
-must provide, as opposed to invariants (predicates maintained across iterations)
-or verification conditions (propositions to prove).
--/
-builtin_initialize mvcgenWitnessTypeAttr : TagAttribute ←
-  registerTagAttribute `mvcgen_witness_type
-    "marks a type as a witness type for the `mvcgen` tactic"
-
-/--
-Returns `true` if `ty` is an application of a type tagged with `@[mvcgen_witness_type]`.
--/
-def isMVCGenWitnessType (env : Environment) (ty : Expr) : Bool :=
-  if let .const name .. := ty.getAppFn then
-    mvcgenWitnessTypeAttr.hasTag env name
-  else
-    false

src/Lean/Elab/Tactic/Do/VCGen.lean

@@ -35,7 +35,6 @@ namespace VCGen
 
 structure Result where
   invariants : Array MVarId
-  witnesses : Array MVarId
   vcs : Array MVarId
 
 partial def genVCs (goal : MVarId) (ctx : Context) (fuel : Fuel) : MetaM Result := do
@@ -46,13 +45,10 @@ partial def genVCs (goal : MVarId) (ctx : Context) (fuel : Fuel) : MetaM Result
     for h : idx in *...state.invariants.size do
       let mv := state.invariants[idx]
       mv.setTag (Name.mkSimple ("inv" ++ toString (idx + 1)))
-    for h : idx in *...state.witnesses.size do
-      let mv := state.witnesses[idx]
-      mv.setTag (Name.mkSimple ("witness" ++ toString (idx + 1)))
     for h : idx in *...state.vcs.size do
       let mv := state.vcs[idx]
       mv.setTag (Name.mkSimple ("vc" ++ toString (idx + 1)) ++ (← mv.getTag).eraseMacroScopes)
-    return { invariants := state.invariants, witnesses := state.witnesses, vcs := state.vcs }
+    return { invariants := state.invariants, vcs := state.vcs }
 where
   onFail (goal : MGoal) (name : Name) : VCGenM Expr := do
     -- trace[Elab.Tactic.Do.vcgen] "fail {goal.toExpr}"
@@ -356,70 +352,53 @@ where
 
 end VCGen
 
-/-- Shared implementation for elaborating goal sections (invariants, witnesses).
-    `tagPrefix` is `"inv"` or `"witness"`, used to parse labels like `inv1` or `witness2`.
-    `label` is `"invariant"` or `"witness"`, used in error messages.
-    When `requireAll` is true, an error is thrown if fewer alts are provided than goals. -/
-private def elabGoalSection (goals : Array MVarId) (alts : Array Syntax)
-    (tagPrefix : String) (label : String) (requireAll := true) : TacticM Unit := do
-  let goals ← goals.filterM (not <$> ·.isAssigned)
-  let mut dotOrCase := LBool.undef -- .true => dot
-  for h : n in 0...alts.size do
-    let alt := alts[n]
-    match alt with
-    | `(goalDotAlt| · $rhs) =>
-      if dotOrCase matches .false then
-        logErrorAt alt m!"Alternation between labelled and bulleted {label}s is not supported."
-        break
-      dotOrCase := .true
-      let some mv := goals[n]? | do
-        logErrorAt alt m!"More {label}s have been defined ({alts.size}) than there were unassigned {label} goals `{tagPrefix}<n>` ({goals.size})."
-        continue
-      withRef rhs do
-      discard <| evalTacticAt (← `(tactic| exact $rhs)) mv
-    | `(goalCaseAlt| | $tag $args* => $rhs) =>
-      if dotOrCase matches .true then
-        logErrorAt alt m!"Alternation between labelled and bulleted {label}s is not supported."
-        break
-      dotOrCase := .false
-      let n? : Option Nat := do
-          let `(binderIdent| $tag:ident) := tag | some n -- fall back to ordinal
-          let .str .anonymous s := tag.getId | none
-          s.dropPrefix? tagPrefix >>= String.Slice.toNat?
-      let some mv := do goals[(← n?) - 1]? | do
-        logErrorAt alt m!"No {label} with label {tag} {repr tag}."
-        continue
-      if ← mv.isAssigned then
-        logErrorAt alt m!"{label} {n?.get!} is already assigned."
-        continue
-      withRef rhs do
-      discard <| evalTacticAt (← `(tactic| rename_i $args*; exact $rhs)) mv
-    | _ => logErrorAt alt m!"Expected `goalDotAlt`, got {alt}"
-  if requireAll && alts.size < goals.size then
-    let missingTypes ← goals[alts.size:].toArray.mapM (·.getType)
-    throwError "Lacking definitions for the following {label}s.\n{toMessageList missingTypes}"
-
-def elabWitnesses (stx : Syntax) (witnesses : Array MVarId) : TacticM Unit := do
-  let some stx := stx.getOptional? | return ()
-  let stx : TSyntax ``witnessAlts := ⟨stx⟩
-  withRef stx do
-  match stx with
-  | `(witnessAlts| witnesses $alts*) =>
-    elabGoalSection witnesses alts "witness" "witness"
-  | _ => logErrorAt stx m!"Expected witnessAlts, got {stx}"
-
 def elabInvariants (stx : Syntax) (invariants : Array MVarId) (suggestInvariant : MVarId → TacticM Term) : TacticM Unit := do
   let some stx := stx.getOptional? | return ()
   let stx : TSyntax ``invariantAlts := ⟨stx⟩
   withRef stx do
   match stx with
   | `(invariantAlts| $invariantsKW $alts*) =>
+    let invariants ← invariants.filterM (not <$> ·.isAssigned)
+
+    let mut dotOrCase := LBool.undef -- .true => dot
+    for h : n in 0...alts.size do
+      let alt := alts[n]
+      match alt with
+      | `(goalDotAlt| · $rhs) =>
+        if dotOrCase matches .false then
+          logErrorAt alt m!"Alternation between labelled and bulleted invariants is not supported."
+          break
+        dotOrCase := .true
+        let some mv := invariants[n]? | do
+          logErrorAt alt m!"More invariants have been defined ({alts.size}) than there were unassigned invariants goals `inv<n>` ({invariants.size})."
+          continue
+        withRef rhs do
+        discard <| evalTacticAt (← `(tactic| exact $rhs)) mv
+      | `(goalCaseAlt| | $tag $args* => $rhs) =>
+        if dotOrCase matches .true then
+          logErrorAt alt m!"Alternation between labelled and bulleted invariants is not supported."
+          break
+        dotOrCase := .false
+        let n? : Option Nat := do
+            let `(binderIdent| $tag:ident) := tag | some n -- fall back to ordinal
+            let .str .anonymous s := tag.getId | none
+            s.dropPrefix? "inv" >>= String.Slice.toNat?
+        let some mv := do invariants[(← n?) - 1]? | do
+          logErrorAt alt m!"No invariant with label {tag} {repr tag}."
+          continue
+        if ← mv.isAssigned then
+          logErrorAt alt m!"Invariant {n?.get!} is already assigned."
+          continue
+        withRef rhs do
+        discard <| evalTacticAt (← `(tactic| rename_i $args*; exact $rhs)) mv
+      | _ => logErrorAt alt m!"Expected `goalDotAlt`, got {alt}"
+
     if let `(invariantsKW| invariants) := invariantsKW then
-      elabGoalSection invariants alts "inv" "invariant"
+      if alts.size < invariants.size then
+        let missingTypes ← invariants[alts.size:].toArray.mapM (·.getType)
+        throwErrorAt stx m!"Lacking definitions for the following invariants.\n{toMessageList missingTypes}"
     else
-      -- We have `invariants?`. First elaborate any user-provided alts, then suggest the rest.
-      elabGoalSection invariants alts "inv" "invariant" (requireAll := false)
-      let invariants ← invariants.filterM (not <$> ·.isAssigned)
+      -- Otherwise, we have `invariants?`. Suggest missing invariants.
       let mut suggestions := #[]
       for i in 0...invariants.size do
         let mv := invariants[i]!
@@ -478,8 +457,8 @@ def elabMVCGen : Tactic := fun stx => withMainContext do
     | none => .unlimited
   let goal ← getMainGoal
   let goal ← if ctx.config.elimLets then elimLets goal else pure goal
-  let { invariants, witnesses, vcs } ← VCGen.genVCs goal ctx fuel
-  trace[Elab.Tactic.Do.vcgen] "after genVCs {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}"
+  let { invariants, vcs } ← VCGen.genVCs goal ctx fuel
+  trace[Elab.Tactic.Do.vcgen] "after genVCs {← (invariants ++ vcs).mapM fun m => m.getTag}"
   let runOnVCs (tac : TSyntax `tactic) (extraMsg : MessageData) (vcs : Array MVarId) : TermElabM (Array MVarId) :=
     vcs.flatMapM fun vc =>
       tryCatchRuntimeEx
@@ -488,13 +467,10 @@ def elabMVCGen : Tactic := fun stx => withMainContext do
         (fun ex => throwError "Error while running {tac} on {vc}Message: {indentD ex.toMessageData}\n{extraMsg}")
   let invariants ←
     if ctx.config.leave then runOnVCs (← `(tactic| try mleave)) "Try again with -leave." invariants else pure invariants
-  trace[Elab.Tactic.Do.vcgen] "before elabWitnesses {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}"
-  elabWitnesses stx[3] witnesses
-  let witnesses ← witnesses.filterM (not <$> ·.isAssigned)
-  trace[Elab.Tactic.Do.vcgen] "before elabInvariants {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}"
-  elabInvariants stx[4] invariants (suggestInvariant vcs)
+  trace[Elab.Tactic.Do.vcgen] "before elabInvariants {← (invariants ++ vcs).mapM fun m => m.getTag}"
+  elabInvariants stx[3] invariants (suggestInvariant vcs)
   let invariants ← invariants.filterM (not <$> ·.isAssigned)
-  trace[Elab.Tactic.Do.vcgen] "before trying trivial VCs {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}"
+  trace[Elab.Tactic.Do.vcgen] "before trying trivial VCs {← (invariants ++ vcs).mapM fun m => m.getTag}"
   let vcs ← do
     let vcs ← if ctx.config.trivial then runOnVCs (← `(tactic| try mvcgen_trivial)) "Try again with -trivial." vcs else pure vcs
     let vcs ← if ctx.config.leave then runOnVCs (← `(tactic| try mleave)) "Try again with -leave." vcs else pure vcs
@@ -502,17 +478,17 @@ def elabMVCGen : Tactic := fun stx => withMainContext do
   -- Eliminating lets here causes some metavariables in `mkFreshPair_triple` to become nonassignable
   -- so we don't do it. Presumably some weird delayed assignment thing is going on.
   -- let vcs ← if ctx.config.elimLets then liftMetaM <| vcs.mapM elimLets else pure vcs
-  trace[Elab.Tactic.Do.vcgen] "before elabVCs {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}"
-  let vcs ← elabVCs stx[5] vcs
-  trace[Elab.Tactic.Do.vcgen] "before replacing main goal {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}"
-  replaceMainGoal (invariants ++ witnesses ++ vcs).toList
+  trace[Elab.Tactic.Do.vcgen] "before elabVCs {← (invariants ++ vcs).mapM fun m => m.getTag}"
+  let vcs ← elabVCs stx[4] vcs
+  trace[Elab.Tactic.Do.vcgen] "before replacing main goal {← (invariants ++ vcs).mapM fun m => m.getTag}"
+  replaceMainGoal (invariants ++ vcs).toList
   -- trace[Elab.Tactic.Do.vcgen] "replaced main goal, new: {← getGoals}"
 
 @[builtin_tactic Lean.Parser.Tactic.mvcgenHint]
 def elabMVCGenHint : Tactic := fun stx => withMainContext do
   let stx' : TSyntax ``mvcgen := TSyntax.mk <| stx
     |>.setKind ``Lean.Parser.Tactic.mvcgen
-    |>.modifyArgs (·.set! 0 (mkAtom "mvcgen") |>.push mkNullNode |>.push (mkNullNode #[← `(invariantAlts| invariants?)]) |>.push mkNullNode)
+    |>.modifyArgs (·.set! 0 (mkAtom "mvcgen") |>.push (mkNullNode #[← `(invariantAlts| invariants?)]) |>.push mkNullNode)
   -- logInfo m!"{stx}\n{toString stx}\n{repr stx}"
   -- logInfo m!"{stx'}\n{toString stx'}\n{repr stx'}"
   Lean.Meta.Tactic.TryThis.addSuggestion stx stx'

src/Lean/Elab/Tactic/Do/VCGen/Basic.lean

@@ -73,10 +73,6 @@ structure State where
   -/
   invariants : Array MVarId := #[]
   /--
-  Holes of witness type that have been generated so far.
-  -/
-  witnesses : Array MVarId := #[]
-  /--
   The verification conditions that have been generated so far.
   -/
   vcs : Array MVarId := #[]
@@ -108,11 +104,8 @@ def addSubGoalAsVC (goal : MVarId) : VCGenM PUnit := do
   -- VC to the user as-is, without abstracting any variables in the local context.
   -- This only makes sense for synthetic opaque metavariables.
   goal.setKind .syntheticOpaque
-  let env ← getEnv
-  if isMVCGenInvariantType env ty then
+  if isMVCGenInvariantType (← getEnv) ty then
     modify fun s => { s with invariants := s.invariants.push goal }
-  else if isMVCGenWitnessType env ty then
-    modify fun s => { s with witnesses := s.witnesses.push goal }
   else
     modify fun s => { s with vcs := s.vcs.push goal }
 

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

@@ -76,6 +76,10 @@ def evalGrindSeq : GrindTactic := fun stx =>
 @[builtin_grind_tactic skip] def evalSkip : GrindTactic := fun _ =>
   return ()
 
+@[builtin_grind_tactic showGoals] def evalShowGoals : GrindTactic := fun _ => do
+  let goals ← getUnsolvedGoalMVarIds
+  addRawTrace (goalsToMessageData goals)
+
 @[builtin_grind_tactic paren] def evalParen : GrindTactic := fun stx =>
   evalGrindTactic stx[1]
 

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

@@ -9,6 +9,8 @@ import Lean.Elab.Tactic.Grind.SimprocDSL
 import Init.Sym.Simp.SimprocDSL
 import Lean.Meta.Sym.Simp.EvalGround
 import Lean.Meta.Sym.Simp.Telescope
+import Lean.Meta.Sym.Simp.ControlFlow
+import Lean.Meta.Sym.Simp.Forall
 import Lean.Meta.Sym.Simp.Rewrite
 namespace Lean.Elab.Tactic.Grind
 open Meta Sym.Simp
@@ -23,6 +25,14 @@ def elabSimprocGround : SymSimprocElab := fun _ =>
 def elabSimprocTelescope : SymSimprocElab := fun _ =>
   return simpTelescope
 
+@[builtin_sym_simproc Lean.Parser.Sym.Simp.control]
+def elabSimprocControl : SymSimprocElab := fun _ =>
+  return simpControl
+
+@[builtin_sym_simproc Lean.Parser.Sym.Simp.arrowTelescope]
+def elabSimprocArrowTelescope : SymSimprocElab := fun _ =>
+  return simpArrowTelescope
+
 @[builtin_sym_simproc self]
 def elabSimprocSelf : SymSimprocElab := fun _ =>
   return simp

src/Lean/Elab/Tactic/Try.lean

@@ -787,6 +787,7 @@ where
           throw ex
 
 -- `evalSuggest` implementation
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_eval_suggest_tactic]
 private partial def evalSuggestImpl : TryTactic := fun tac => do
   trace[try.debug] "{tac}"

src/Lean/Elab/Term/TermElabM.lean

@@ -309,6 +309,8 @@ structure Context where
   heedElabAsElim     : Bool            := true
   /-- Noncomputable sections automatically add the `noncomputable` modifier to any declaration we cannot generate code for. -/
   isNoncomputableSection : Bool        := false
+  /-- `true` when inside a `meta section`. -/
+  isMetaSection : Bool                 := false
   /-- When `true` we skip TC failures. We use this option when processing patterns. -/
   ignoreTCFailures : Bool := false
   /-- `true` when elaborating patterns. It affects how we elaborate named holes. -/

src/Lean/Environment.lean

@@ -1193,8 +1193,8 @@ namespace ConstantInfo
 def instantiateTypeLevelParams (c : ConstantInfo) (ls : List Level) : Expr :=
   c.toConstantVal.instantiateTypeLevelParams ls
 
-def instantiateValueLevelParams! (c : ConstantInfo) (ls : List Level) : Expr :=
-  c.value!.instantiateLevelParams c.levelParams ls
+def instantiateValueLevelParams! (c : ConstantInfo) (ls : List Level) (allowOpaque := false) : Expr :=
+  (c.value! (allowOpaque := allowOpaque)).instantiateLevelParams c.levelParams ls
 
 end ConstantInfo
 
@@ -2755,13 +2755,28 @@ def mkThmOrUnsafeDef [Monad m] [MonadEnv m] (thm : TheoremVal) : m Declaration :
   else
     return .thmDecl thm
 
+/-- Environment extension for overriding the height that `getMaxHeight` assigns to a definition.
+This is consulted for all definitions regardless of their reducibility hints. Currently used by
+structural recursion to ensure that parent definitions get the correct height even though the
+`_f` helper definitions are marked as `.abbrev` (which `getMaxHeight` would otherwise ignore). -/
+builtin_initialize defHeightOverrideExt : EnvExtension (NameMap UInt32) ←
+  registerEnvExtension (pure {}) (asyncMode := .local)
+
+/-- Register a height override for a definition so that `getMaxHeight` uses it. -/
+def setDefHeightOverride (env : Environment) (declName : Name) (height : UInt32) : Environment :=
+  defHeightOverrideExt.modifyState env fun m => m.insert declName height
+
 def getMaxHeight (env : Environment) (e : Expr) : UInt32 :=
+  let overrides := defHeightOverrideExt.getState env
   e.foldConsts 0 fun constName max =>
-    match env.findAsync? constName with
-    | some { kind := .defn, constInfo := info, .. } =>
-      match info.get.hints with
-      | ReducibilityHints.regular h => if h > max then h else max
-      | _                           => max
-    | _ => max
+    match overrides.find? constName with
+    | some h => if h > max then h else max
+    | none =>
+      match env.findAsync? constName with
+      | some { kind := .defn, constInfo := info, .. } =>
+        match info.get.hints with
+        | ReducibilityHints.regular h => if h > max then h else max
+        | _                           => max
+      | _ => max
 
 end Lean

src/Lean/Expr.lean

@@ -73,7 +73,7 @@ inductive BinderInfo where
   | default
   /-- Implicit binder annotation, e.g., `{x : α}` -/
   | implicit
-  /-- Strict implicit binder annotation, e.g., `{{ x : α }}` -/
+  /-- Strict implicit binder annotation, e.g., `⦃x : α⦄` -/
   | strictImplicit
   /-- Local instance binder annotation, e.g., `[Decidable α]` -/
   | instImplicit
@@ -107,7 +107,7 @@ def BinderInfo.isImplicit : BinderInfo → Bool
   | BinderInfo.implicit => true
   | _                   => false
 
-/-- Return `true` if the given `BinderInfo` is a strict implicit annotation (e.g., `{{α : Type u}}`) -/
+/-- Return `true` if the given `BinderInfo` is a strict implicit annotation (e.g., `⦃α : Type u⦄`) -/
 def BinderInfo.isStrictImplicit : BinderInfo → Bool
   | BinderInfo.strictImplicit => true
   | _                         => false

src/Lean/Meta.lean

@@ -27,7 +27,7 @@ public import Lean.Meta.Match
 public import Lean.Meta.ReduceEval
 public import Lean.Meta.Closure
 public import Lean.Meta.AbstractNestedProofs
-public import Lean.Meta.InstanceNormalForm
+public import Lean.Meta.WrapInstance
 public import Lean.Meta.LetToHave
 public import Lean.Meta.ForEachExpr
 public import Lean.Meta.Transform

src/Lean/Meta/Basic.lean

@@ -1321,7 +1321,7 @@ private def getDefInfoTemp (info : ConstantInfo) : MetaM (Option ConstantInfo) :
    `constName` is an instance. This difference should be irrelevant for `isClassQuickConst?`. -/
 private def getConstTemp? (constName : Name) : MetaM (Option ConstantInfo) := do
   match (← getEnv).find? constName with
-  | some (info@(ConstantInfo.thmInfo _))  => getTheoremInfo info
+  | some (ConstantInfo.thmInfo _)          => return none
   | some (info@(ConstantInfo.defnInfo _)) => getDefInfoTemp info
   | some info                             => pure (some info)
   | none                                  => throwUnknownConstantAt (← getRef) constName

src/Lean/Meta/ExprDefEq.lean

@@ -1126,6 +1126,7 @@ def checkAssignment (mvarId : MVarId) (fvars : Array Expr) (v : Expr) : MetaM (O
       return none
     return some v
 
+set_option compiler.ignoreBorrowAnnotation true in
 -- Implementation for `_root_.Lean.MVarId.checkedAssign`
 @[export lean_checked_assign]
 def checkedAssignImpl (mvarId : MVarId) (val : Expr) : MetaM Bool := do
@@ -2233,6 +2234,7 @@ private def whnfCoreAtDefEq (e : Expr) : MetaM Expr := do
   else
     whnfCore e
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_is_expr_def_eq]
 partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecDepth do
   withTraceNodeBefore `Meta.isDefEq (fun _ => return m!"{t} =?= {s}") do

src/Lean/Meta/GetUnfoldableConst.lean

@@ -46,11 +46,7 @@ External users wanting to look up names should be using `Lean.getConstInfo`.
 def getUnfoldableConst? (constName : Name) : MetaM (Option ConstantInfo) := do
   let some ainfo := (← getEnv).findAsync? constName | throwUnknownConstantAt (← getRef) constName
   match ainfo.kind with
-  | .thm =>
-    if (← shouldReduceAll) then
-      return some ainfo.toConstantInfo
-    else
-      return none
+  | .thm => return none
   | .defn => if (← canUnfold ainfo.toConstantInfo) then return ainfo.toConstantInfo else return none
   | _ => return none
 
@@ -59,7 +55,7 @@ As with `getUnfoldableConst?` but return `none` instead of failing if the consta
 -/
 def getUnfoldableConstNoEx? (constName : Name) : MetaM (Option ConstantInfo) := do
   match (← getEnv).find? constName with
-  | some (info@(.thmInfo _))  => getTheoremInfo info
+  | some (.thmInfo _)          => return none
   | some (info@(.defnInfo _)) => if (← canUnfold info) then return info else return none
   | some (.axiomInfo _)       => recordUnfoldAxiom constName; return none
   | _                         => return none

src/Lean/Meta/InferType.lean

@@ -206,6 +206,7 @@ because it overrides unrelated configurations.
     else
       withConfig (fun cfg => { cfg with beta := true, iota := true, zeta := true, zetaHave := true, zetaDelta := true, proj := .yesWithDelta, etaStruct := .all }) x
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_infer_type]
 def inferTypeImp (e : Expr) : MetaM Expr :=
   let rec infer (e : Expr) :  MetaM Expr := do

src/Lean/Meta/LevelDefEq.lean

@@ -85,6 +85,7 @@ private def isMVarWithGreaterDepth (v : Level) (mvarId : LMVarId) : MetaM Bool :
   | Level.mvar mvarId' => return (← mvarId'.getLevel) > (← mvarId.getLevel)
   | _ => return false
 
+set_option compiler.ignoreBorrowAnnotation true in
 mutual
 
   private partial def solve (u v : Level) : MetaM LBool := do

src/Lean/Meta/Match/MatchEqs.lean

@@ -138,6 +138,7 @@ Creates conditional equations and splitter for the given match auxiliary declara
 
 See also `getEquationsFor`.
 -/
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_get_match_equations_for]
 def getEquationsForImpl (matchDeclName : Name) : MetaM MatchEqns := do
   /-
@@ -246,6 +247,7 @@ where go baseName splitterName := withConfig (fun c => { c with etaStruct := .no
     let result := { eqnNames, splitterName, splitterMatchInfo }
     registerMatchEqns matchDeclName result
 
+set_option compiler.ignoreBorrowAnnotation true in
 /--
 Generate the congruence equations for the given match auxiliary declaration.
 The congruence equations have a completely unrestricted left-hand side (arbitrary discriminants),

src/Lean/Meta/Sym/Pattern.lean

@@ -785,6 +785,7 @@ def isDefEqApp (tFn : Expr) (t : Expr) (s : Expr) (_ : tFn = t.getAppFn) : DefEq
   let numArgs := t.getAppNumArgs
   isDefEqAppWithInfo t s (numArgs - 1) info
 
+set_option compiler.ignoreBorrowAnnotation true in
 /--
 `isDefEqMain` implementation.
 -/

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

@@ -40,6 +40,7 @@ abbrev cacheResult (e : Expr) (r : Result) : SimpM Result := do
     modify fun s => { s with persistentCache := s.persistentCache.insert { expr := e } r }
   return r
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_sym_simp]
 def simpImpl (e₁ : Expr) : SimpM Result := withIncRecDepth do
   let numSteps := (← get).numSteps

src/Lean/Meta/Sym/SymM.lean

@@ -15,6 +15,50 @@ register_builtin_option sym.debug : Bool := {
   descr    := "check invariants"
 }
 
+builtin_initialize registerTraceClass `sym.issues
+
+/-!
+## Sym Extensions
+
+Extensible state mechanism for `SymM`, allowing modules to register persistent state
+that lives across `simp` invocations within a `sym =>` block. Follows the same pattern
+as `Grind.SolverExtension` in `Lean/Meta/Tactic/Grind/Types.lean`.
+-/
+
+/-- Opaque extension state type used to store type-erased extension values. -/
+opaque SymExtensionStateSpec : (α : Type) × Inhabited α := ⟨Unit, ⟨()⟩⟩
+@[expose] def SymExtensionState : Type := SymExtensionStateSpec.fst
+instance : Inhabited SymExtensionState := SymExtensionStateSpec.snd
+
+/--
+A registered extension for `SymM`. Each extension gets a unique index into the
+extensions array in `Sym.State`. Can only be created via `registerSymExtension`.
+-/
+structure SymExtension (σ : Type) where private mk ::
+  id        : Nat
+  mkInitial : IO σ
+  deriving Inhabited
+
+private builtin_initialize symExtensionsRef : IO.Ref (Array (SymExtension SymExtensionState)) ← IO.mkRef #[]
+
+/--
+Registers a new `SymM` state extension. Extensions can only be registered during initialization.
+Returns a handle for typed access to the extension's state.
+-/
+def registerSymExtension {σ : Type} (mkInitial : IO σ) : IO (SymExtension σ) := do
+  unless (← initializing) do
+    throw (IO.userError "failed to register `Sym` extension, extensions can only be registered during initialization")
+  let exts ← symExtensionsRef.get
+  let id := exts.size
+  let ext : SymExtension σ := { id, mkInitial }
+  symExtensionsRef.modify fun exts => exts.push (unsafe unsafeCast ext)
+  return ext
+
+/-- Returns initial state for all registered extensions. -/
+def SymExtensions.mkInitialStates : IO (Array SymExtensionState) := do
+  let exts ← symExtensionsRef.get
+  exts.mapM fun ext => ext.mkInitial
+
 /--
 Information about a single argument position in a function's type signature.
 
@@ -92,9 +136,16 @@ structure SharedExprs where
   ordEqExpr  : Expr
   intExpr    : Expr
 
+/-- Configuration options for the symbolic computation framework. -/
+structure Config where
+  /-- When `true`, issues are collected during proof search and reported on failure. -/
+  verbose : Bool := true
+  deriving Inhabited
+
 /-- Readonly context for the symbolic computation framework. -/
 structure Context where
   sharedExprs : SharedExprs
+  config      : Config := {}
 
 /-- Mutable state for the symbolic computation framework. -/
 structure State where
@@ -133,6 +184,13 @@ structure State where
   congrInfo : PHashMap ExprPtr CongrInfo := {}
   /-- Cache for `isDefEqI` results -/
   defEqI : PHashMap (ExprPtr × ExprPtr) Bool := {}
+  /-- State for registered `SymExtension`s, indexed by extension id. -/
+  extensions : Array SymExtensionState := #[]
+  /--
+  Issues found during symbolic computation. Accumulated across operations
+  within a `sym =>` block and reported when a tactic fails.
+  -/
+  issues : List MessageData := []
   debug : Bool := false
 
 abbrev SymM := ReaderT Context <| StateRefT State MetaM
@@ -150,7 +208,8 @@ private def mkSharedExprs : AlphaShareCommonM SharedExprs := do
 def SymM.run (x : SymM α) : MetaM α := do
   let (sharedExprs, share) := mkSharedExprs |>.run {}
   let debug := sym.debug.get (← getOptions)
-  x { sharedExprs } |>.run' { debug, share }
+  let extensions ← SymExtensions.mkInitialStates
+  x { sharedExprs } |>.run' { debug, share, extensions }
 
 /-- Returns maximally shared commonly used terms -/
 def getSharedExprs : SymM SharedExprs :=
@@ -221,6 +280,55 @@ abbrev share (e : Expr) : SymM Expr :=
 @[inline] def isDebugEnabled : SymM Bool :=
   return (← get).debug
 
+def getConfig : SymM Config :=
+  return (← readThe Context).config
+
+/-- Adds an issue message to the issue tracker. -/
+def reportIssue (msg : MessageData) : SymM Unit := do
+  let msg ← addMessageContext msg
+  modify fun s => { s with issues := .trace { cls := `issue } msg #[] :: s.issues }
+  trace[sym.issues] msg
+
+/-- Reports an issue if `verbose` mode is enabled. Does nothing if `verbose` is `false`. -/
+@[inline] def reportIssueIfVerbose (msg : MessageData) : SymM Unit := do
+  if (← getConfig).verbose then
+    reportIssue msg
+
+private meta def expandReportIssueMacro (s : Syntax) : MacroM (TSyntax `doElem) := do
+  let msg ← if s.getKind == interpolatedStrKind then `(m! $(⟨s⟩)) else `(($(⟨s⟩) : MessageData))
+  `(doElem| Sym.reportIssueIfVerbose $msg)
+
+/-- Reports an issue if `verbose` mode is enabled. -/
+macro "reportIssue!" s:(interpolatedStr(term) <|> term) : doElem => do
+  expandReportIssueMacro s.raw
+
+/-- Reports an issue if both `verbose` and `sym.debug` are enabled. Does nothing otherwise. -/
+@[inline] def reportDbgIssue (msg : MessageData) : SymM Unit := do
+  if (← getConfig).verbose then
+    if sym.debug.get (← getOptions) then
+      reportIssue msg
+
+meta def expandReportDbgIssueMacro (s : Syntax) : MacroM (TSyntax `doElem) := do
+  let msg ← if s.getKind == interpolatedStrKind then `(m! $(⟨s⟩)) else `(($(⟨s⟩) : MessageData))
+  `(doElem| Sym.reportDbgIssue $msg)
+
+/-- Similar to `reportIssue!`, but only reports issue if `sym.debug` is set to `true`. -/
+macro "reportDbgIssue!" s:(interpolatedStr(term) <|> term) : doElem => do
+  expandReportDbgIssueMacro s.raw
+
+/-- Returns all accumulated issues without clearing them. -/
+def getIssues : SymM (List MessageData) :=
+  return (← get).issues
+
+/--
+Runs `x` with a fresh issue context. Issues reported during `x` are
+prepended to the issues that existed before the call.
+-/
+def withNewIssueContext (x : SymM α) : SymM α := do
+  let saved := (← get).issues
+  modify fun s => { s with issues := [] }
+  try x finally modify fun s => { s with issues := s.issues ++ saved }
+
 /-- Similar to `Meta.isDefEqI`, but the result is cache using pointer equality. -/
 def isDefEqI (s t : Expr) : SymM Bool := do
   let key := (⟨s⟩, ⟨t⟩)
@@ -230,4 +338,26 @@ def isDefEqI (s t : Expr) : SymM Bool := do
   modify fun s => { s with defEqI := s.defEqI.insert key result }
   return result
 
+instance : Inhabited (SymM α) where
+  default := throwError "<SymM default value>"
+
+/-! ### SymExtension accessors -/
+
+private unsafe def SymExtension.getStateCoreImpl (ext : SymExtension σ) (extensions : Array SymExtensionState) : IO σ :=
+  return unsafeCast extensions[ext.id]!
+
+@[implemented_by SymExtension.getStateCoreImpl]
+opaque SymExtension.getStateCore (ext : SymExtension σ) (extensions : Array SymExtensionState) : IO σ
+
+def SymExtension.getState (ext : SymExtension σ) : SymM σ := do
+  ext.getStateCore (← get).extensions
+
+private unsafe def SymExtension.modifyStateImpl (ext : SymExtension σ) (f : σ → σ) : SymM Unit := do
+  modify fun s => { s with
+    extensions := s.extensions.modify ext.id fun state => unsafeCast (f (unsafeCast state))
+  }
+
+@[implemented_by SymExtension.modifyStateImpl]
+opaque SymExtension.modifyState (ext : SymExtension σ) (f : σ → σ) : SymM Unit
+
 end Lean.Meta.Sym

src/Lean/Meta/SynthInstance.lean

@@ -944,6 +944,7 @@ def synthInstance (type : Expr) (maxResultSize? : Option Nat := none) : MetaM Ex
       | none        => throwFailedToSynthesize type)
     (fun _ => throwFailedToSynthesize type)
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_synth_pending]
 private def synthPendingImp (mvarId : MVarId) : MetaM Bool := withIncRecDepth <| mvarId.withContext do
   let mvarDecl ← mvarId.getDecl

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

@@ -206,7 +206,7 @@ def handleApp : Simproc := fun e => do
   match fn with
   | .const constName _ =>
     if (← isCbvOpaque constName) then
-      return (← tryCbvTheorems e).markAsDone
+      return markAsDoneIfFailed <| ← tryCbvTheorems e
     let info ← getConstInfo constName
     tryCbvTheorems <|> (guardSimproc (fun _ => info.hasValue) handleConstApp) <|> reduceRecMatcher <| e
   | .lam .. => betaReduce e
@@ -215,7 +215,7 @@ def handleApp : Simproc := fun e => do
 def handleOpaqueConst : Simproc := fun e => do
   let .const constName _ := e | return .rfl
   if (← isCbvOpaque constName) then
-    return (← tryCbvTheorems e).markAsDone
+    return markAsDoneIfFailed <| ← tryCbvTheorems e
   return .rfl
 
 def foldLit : Simproc := fun e => do

src/Lean/Meta/Tactic/Cbv/Util.lean

@@ -108,4 +108,8 @@ public partial def getListLitElems (e : Expr) (acc : Array Expr := #[]) : Option
   | List.cons _ a as => getListLitElems as <| acc.push a
   | _ => none
 
+public def markAsDoneIfFailed : Result → Result
+  | .rfl _ cd => .rfl true cd
+  | .step e h d cd => .step e h d cd
+
 end Lean.Meta.Tactic.Cbv

src/Lean/Meta/Tactic/Delta.lean

@@ -10,18 +10,18 @@ import Lean.Meta.Transform
 public section
 namespace Lean.Meta
 
-def delta? (e : Expr) (p : Name → Bool := fun _ => true) : CoreM (Option Expr) :=
+def delta? (e : Expr) (p : Name → Bool := fun _ => true) (allowOpaque := false) : CoreM (Option Expr) :=
   matchConst e.getAppFn (fun _ => return none) fun fInfo fLvls => do
-    if p fInfo.name && fInfo.hasValue && fInfo.levelParams.length == fLvls.length then
-      let f ← instantiateValueLevelParams fInfo fLvls
+    if p fInfo.name && fInfo.hasValue (allowOpaque := allowOpaque) && fInfo.levelParams.length == fLvls.length then
+      let f ← instantiateValueLevelParams fInfo fLvls (allowOpaque := allowOpaque)
       return some (f.betaRev e.getAppRevArgs (useZeta := true))
     else
       return none
 
 /-- Low-level delta expansion. It is used to implement equation lemmas and elimination principles for recursive definitions. -/
-def deltaExpand (e : Expr) (p : Name → Bool) : CoreM Expr :=
+def deltaExpand (e : Expr) (p : Name → Bool) (allowOpaque := false) : CoreM Expr :=
   Core.transform e fun e => do
-    match (← delta? e p) with
+    match (← delta? e p (allowOpaque := allowOpaque)) with
     | some e' => return .visit e'
     | none    => return .continue
 

src/Lean/Meta/Tactic/FunInd.lean

@@ -347,11 +347,13 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
 
     if e.getAppArgs.any (·.isFVarOf oldIH) then
       -- Sometimes Fix.lean abstracts over oldIH in a proof definition.
-      -- So beta-reduce that definition. We need to look through theorems here!
-      if let some e' ← withTransparency .all do unfoldDefinition? e then
-        return ← foldAndCollect oldIH newIH isRecCall e'
-      else
-        throwError "Internal error in `foldAndCollect`: Cannot reduce application of `{e.getAppFn}` in:{indentExpr e}"
+      -- So delta-beta-reduce that definition. We need to look through theorems here!
+      if let .const declName lvls := e.getAppFn then
+        if let some cinfo := (← getEnv).find? declName then
+          if let some val := cinfo.value? (allowOpaque := true) then
+            let e' := (val.instantiateLevelParams cinfo.levelParams lvls).betaRev e.getAppRevArgs
+            return ← foldAndCollect oldIH newIH isRecCall e'
+      throwError "Internal error in `foldAndCollect`: Cannot reduce application of `{e.getAppFn}` in:{indentExpr e}"
 
     match e with
     | .app e1 e2 =>
@@ -742,6 +744,13 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
         let b' ← buildInductionBody toErase toClear goal' oldIH newIH isRecCall (b.instantiate1 x)
         mkLambdaFVars #[x] b'
 
+  -- Unfold constant applications that take `oldIH` as an argument (e.g. `_f` auxiliary
+  -- definitions from structural recursion), so that we can see their body structure.
+  -- Similar to the case in `foldAndCollect`.
+  if e.getAppFn.isConst && e.getAppArgs.any (·.isFVarOf oldIH) then
+    if let some e' ← withTransparency .all (unfoldDefinition? e) then
+      return ← buildInductionBody toErase toClear goal oldIH newIH isRecCall e'
+
   liftM <| buildInductionCase oldIH newIH isRecCall toErase toClear goal e
 
 /--

src/Lean/Meta/Tactic/Grind.lean

@@ -63,7 +63,6 @@ builtin_initialize registerTraceClass `grind.ematch.instance
 builtin_initialize registerTraceClass `grind.ematch.instance.assignment
 builtin_initialize registerTraceClass `grind.ematch.instance.delayed
 builtin_initialize registerTraceClass `grind.eqResolution
-builtin_initialize registerTraceClass `grind.issues
 builtin_initialize registerTraceClass `grind.simp
 builtin_initialize registerTraceClass `grind.split
 builtin_initialize registerTraceClass `grind.split.candidate

src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean

@@ -53,7 +53,7 @@ def mkEqCnstr (p : Poly) (h : EqCnstrProof) : RingM EqCnstr := do
 Returns the ring expression denoting the given Lean expression.
 Recall that we compute the ring expressions during internalization.
 -/
-private def toRingExpr? [Monad m] [MonadLiftT GrindM m] [MonadRing m] (e : Expr) : m (Option RingExpr) := do
+private def toRingExpr? [Monad m] [MonadLiftT GrindM m] [MonadLiftT Sym.SymM m] [MonadRing m] (e : Expr) : m (Option RingExpr) := do
   let ring ← getRing
   if let some re := ring.denote.find? { expr := e } then
     return some re
@@ -67,7 +67,7 @@ private def toRingExpr? [Monad m] [MonadLiftT GrindM m] [MonadRing m] (e : Expr)
 Returns the semiring expression denoting the given Lean expression.
 Recall that we compute the semiring expressions during internalization.
 -/
-private def toSemiringExpr? [Monad m] [MonadLiftT GrindM m] [MonadSemiring m] (e : Expr) : m (Option SemiringExpr) := do
+private def toSemiringExpr? [Monad m] [MonadLiftT GrindM m] [MonadLiftT Sym.SymM m] [MonadSemiring m] (e : Expr) : m (Option SemiringExpr) := do
   let semiring ← getSemiring
   if let some re := semiring.denote.find? { expr := e } then
     return some re

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean

@@ -276,6 +276,7 @@ private def propagateNonlinearPow (x : Var) : GoalM Bool := do
   c'.assert
   return true
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_cutsat_propagate_nonlinear]
 def propagateNonlinearTermImpl (y : Var) (x : Var) : GoalM Bool := do
   unless (← isVarEqConst? y).isSome do return false
@@ -338,6 +339,7 @@ partial def _root_.Int.Linear.Poly.updateOccsForElimEq (p : Poly) (x : Var) : Go
     go p
   go p
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_cutsat_assert_eq]
 def EqCnstr.assertImpl (c : EqCnstr) : GoalM Unit := do
   if (← inconsistent) then return ()

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean

@@ -99,6 +99,7 @@ where
         return some { p := c.p.addConst 1, h := .ofLeDiseq c c' }
     return none
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_cutsat_assert_le]
 def LeCnstr.assertImpl (c : LeCnstr) : GoalM Unit := do
   if (← inconsistent) then return ()

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean

@@ -325,7 +325,9 @@ private def mkPowEqProof (ka : Int) (ca? : Option EqCnstr) (kb : Nat) (cb? : Opt
   let h := mkApp8 (mkConst ``Int.Linear.pow_eq) a b (toExpr ka) (toExpr kbInt) (toExpr k) h₁ h₂ eagerReflBoolTrue
   return mkApp6 (mkConst ``Int.Linear.of_var_eq) (← getContext) (← mkVarDecl x) (toExpr k) (← mkPolyDecl c'.p) eagerReflBoolTrue h
 
+set_option compiler.ignoreBorrowAnnotation true in
 mutual
+
 @[export lean_cutsat_eq_cnstr_to_proof]
 private partial def EqCnstr.toExprProofImpl (c' : EqCnstr) : ProofM Expr := caching c' do
   trace[grind.debug.lia.proof] "{← c'.pp}"

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.lean

@@ -64,6 +64,7 @@ where
         registerNonlinearOcc e x
     | _ => registerNonlinearOcc e x
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_cutsat_mk_var]
 def mkVarImpl (expr : Expr) : GoalM Var := do
   if let some var := (← get').varMap.find? { expr } then

src/Lean/Meta/Tactic/Grind/Canon.lean

@@ -239,6 +239,7 @@ private def normOfNatArgs? (args : Array Expr) : MetaM (Option (Array Expr)) :=
       return some args.toArray
   return none
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_canon]
 partial def canonImpl (e : Expr) : GoalM Expr := do profileitM Exception "grind canon" (← getOptions) do
   trace_goal[grind.debug.canon] "{e}"

src/Lean/Meta/Tactic/Grind/Core.lean

@@ -348,6 +348,7 @@ where
       internalize rhs generation p
       addEqCore lhs rhs proof isHEq
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_process_new_facts]
 private def processNewFactsImpl : GoalM Unit := do
   repeat

src/Lean/Meta/Tactic/Grind/EMatch.lean

@@ -456,7 +456,7 @@ private def getUnassignedLevelMVars (e : Expr) : MetaM (Array LMVarId) := do
 -- **Note**: issues reported by the E-matching module are too distractive. We only
 -- report them if `set_option grind.debug true`
 macro "reportEMatchIssue!" s:(interpolatedStr(term) <|> term) : doElem => do
-  expandReportDbgIssueMacro s.raw
+  Sym.expandReportDbgIssueMacro s.raw
 
 /--
 Stores new theorem instance in the state.

src/Lean/Meta/Tactic/Grind/Internalize.lean

@@ -535,6 +535,7 @@ private def internalizeOfNatFinBitVecLiteral (e : Expr) (generation : Nat) (pare
   updateIndicesFound (.const ``OfNat.ofNat)
   activateTheorems ``OfNat.ofNat generation
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_internalize]
 private partial def internalizeImpl (e : Expr) (generation : Nat) (parent? : Option Expr := none) : GoalM Unit := withIncRecDepth do
   if (← alreadyInternalized e) then

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

@@ -104,6 +104,8 @@ private def discharge? (e : Expr) : SimpM (Option Expr) := do
 open Sym
 
 def GrindM.run (x : GrindM α) (params : Params) (evalTactic? : Option EvalTactic := none) : MetaM α := Sym.SymM.run do
+  withNewIssueContext do
+  withReader (fun ctx => { ctx with config.verbose := params.config.verbose }) do
   /- **Note**: Consider using `Sym.simp` in the future. -/
   let simprocs  := params.normProcs
   let simpMethods := Simp.mkMethods simprocs discharge? (wellBehavedDischarge := true)
@@ -332,7 +334,7 @@ private def initCore (mvarId : MVarId) : GrindM Goal := do
     processHypotheses goal
 
 def mkResult (params : Params) (failure? : Option Goal) : GrindM Result := do
-  let issues     := (← get).issues
+  let issues     ← Sym.getIssues
   let counters   := (← get).counters
   let splitDiags := (← get).splitDiags
   let simp       := { (← get).simp with }

src/Lean/Meta/Tactic/Grind/Proof.lean

@@ -328,6 +328,7 @@ mutual
 
 end
 
+set_option compiler.ignoreBorrowAnnotation true in
 /--
 Returns a proof that `a = b`.
 It assumes `a` and `b` are in the same equivalence class.
@@ -338,6 +339,7 @@ def mkEqProofImpl (a b : Expr) : GoalM Expr := do
     throwError "internal `grind` error, `mkEqProof` invoked with terms of different types{indentExpr a}\nhas type{indentExpr (← inferType a)}\nbut{indentExpr b}\nhas type{indentExpr (← inferType b)}"
   mkEqProofCore a b (heq := false)
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_mk_heq_proof]
 def mkHEqProofImpl (a b : Expr) : GoalM Expr :=
   mkEqProofCore a b (heq := true)

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

@@ -42,6 +42,7 @@ def dsimpCore (e : Expr) : GrindM Expr := do profileitM Exception "grind dsimp"
   modify fun s => { s with simp }
   return r
 
+set_option compiler.ignoreBorrowAnnotation true in
 /--
 Preprocesses `e` using `grind` normalization theorems and simprocs,
 and then applies several other preprocessing steps.

src/Lean/Meta/Tactic/Grind/SimpUtil.lean

@@ -202,6 +202,7 @@ protected def getSimpContext (config : Grind.Config) : MetaM Simp.Context := do
     (simpTheorems := #[thms])
     (congrTheorems := (← getSimpCongrTheorems))
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_normalize]
 def normalizeImp (e : Expr) (config : Grind.Config) : MetaM Expr := do
   let (r, _) ← Meta.simp e (← Grind.getSimpContext config) (← Grind.getSimprocs)

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -214,11 +214,6 @@ structure State where
   and implement the macro `trace_goal`.
   -/
   lastTag    : Name := .anonymous
-  /--
-  Issues found during the proof search. These issues are reported to
-  users when `grind` fails.
-  -/
-  issues     : List MessageData := []
   /-- Performance counters -/
   counters   : Counters := {}
   /-- Split diagnostic information. This information is only collected when `set_option diagnostics true` -/
@@ -401,35 +396,6 @@ def mkHCongrWithArity (f : Expr) (numArgs : Nat) : GrindM CongrTheorem := do
   modify fun s => { s with congrThms := s.congrThms.insert key result }
   return result
 
-def reportIssue (msg : MessageData) : GrindM Unit := do
-  let msg ← addMessageContext msg
-  modify fun s => { s with issues := .trace { cls := `issue } msg #[] :: s.issues }
-  /-
-  We also add a trace message because we may want to know when
-  an issue happened relative to other trace messages.
-  -/
-  trace[grind.issues] msg
-
-private meta def expandReportIssueMacro (s : Syntax) : MacroM (TSyntax `doElem) := do
-  let msg ← if s.getKind == interpolatedStrKind then `(m! $(⟨s⟩)) else `(($(⟨s⟩) : MessageData))
-  `(doElem| do
-    if (← getConfig).verbose then
-      reportIssue $msg)
-
-macro "reportIssue!" s:(interpolatedStr(term) <|> term) : doElem => do
-  expandReportIssueMacro s.raw
-
-/-- Similar to `expandReportIssueMacro`, but only reports issue if `grind.debug` is set to `true` -/
-meta def expandReportDbgIssueMacro (s : Syntax) : MacroM (TSyntax `doElem) := do
-  let msg ← if s.getKind == interpolatedStrKind then `(m! $(⟨s⟩)) else `(($(⟨s⟩) : MessageData))
-  `(doElem| do
-    if (← getConfig).verbose then
-      if grind.debug.get (← getOptions) then
-        reportIssue $msg)
-
-/-- Similar to `reportIssue!`, but only reports issue if `grind.debug` is set to `true` -/
-macro "reportDbgIssue!" s:(interpolatedStr(term) <|> term) : doElem => do
-  expandReportDbgIssueMacro s.raw
 
 /--
 Each E-node may have "solver terms" attached to them.

src/Lean/Meta/Tactic/Grind/Util.lean

@@ -130,7 +130,7 @@ def foldProjs (e : Expr) : MetaM Expr := do
   let post (e : Expr) := do
     let .proj structName idx s := e | return .done e
     let some info := getStructureInfo? (← getEnv) structName |
-      trace[grind.issues] "found `Expr.proj` but `{structName}` is not marked as structure{indentExpr e}"
+      trace[sym.issues] "found `Expr.proj` but `{structName}` is not marked as structure{indentExpr e}"
       return .done e
     if h : idx < info.fieldNames.size then
       let fieldName := info.fieldNames[idx]
@@ -149,7 +149,7 @@ def foldProjs (e : Expr) : MetaM Expr := do
       -/
       return .visit (← withDefault <| mkProjection s fieldName)
     else
-      trace[grind.issues] "found `Expr.proj` with invalid field index `{idx}`{indentExpr e}"
+      trace[sym.issues] "found `Expr.proj` with invalid field index `{idx}`{indentExpr e}"
       return .done e
   Meta.transform e (post := post)
 

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean

@@ -52,6 +52,12 @@ builtin_dsimproc [simp, seval] reduceSingleton (String.singleton _) := fun e =>
   let some c ← Char.fromExpr? e.appArg! | return .continue
   return .done <| toExpr (String.singleton c)
 
+builtin_dsimproc_decl reduceToSingleton ((_ : String)) := fun e => do
+  let some s ← fromExpr? e | return .continue
+  let l := s.toList
+  let [c] := l | return .continue
+  return .done <| mkApp (mkConst ``String.singleton) (toExpr c)
+
 @[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : String → String → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← fromExpr? e.appFn!.appArg! | return .continue

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

@@ -512,6 +512,7 @@ Auxiliary `dsimproc` for not visiting `Char` literal subterms.
 -/
 private def doNotVisitCharLit : DSimproc := doNotVisit isCharLit ``Char.ofNat
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_dsimp]
 private partial def dsimpImpl (e : Expr) : SimpM Expr := do
   let cfg ← getConfig
@@ -710,6 +711,7 @@ where
       r ← r.mkEqTrans (← simpLoop r.expr)
     cacheResult e cfg r
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_simp]
 def simpImpl (e : Expr) : SimpM Result := withIncRecDepth do
   checkSystem "simp"

src/Lean/Meta/Transform.lean

@@ -240,8 +240,8 @@ def unfoldDeclsFrom (biggerEnv : Environment) (e : Expr) : CoreM Expr := do
       if env.contains declName then
         return .done e
       let some info := biggerEnv.find? declName | return .done e
-      if info.hasValue then
-        return .visit (← instantiateValueLevelParams info us)
+      if info.hasValue (allowOpaque := true) then
+        return .visit (← instantiateValueLevelParams info us (allowOpaque := true))
       else
         return .done e
     Core.transform e (pre := pre)
@@ -282,7 +282,7 @@ def unfoldIfArgIsAppOf (fnNames : Array Name) (numSectionVars : Nat) (e : Expr)
         -/
         if revArgs.any isInterestingArg then
           if let some info@(.thmInfo _) := env.find? f.constName! then
-            return .visit <| (← instantiateValueLevelParams info f.constLevels!).betaRev revArgs
+            return .visit <| (← instantiateValueLevelParams info f.constLevels! (allowOpaque := true)).betaRev revArgs
       return .continue)
   where
     isInterestingArg (a : Expr) : Bool := a.withApp fun af axs =>

src/Lean/Meta/WHNF.lean

@@ -1100,6 +1100,7 @@ private def cache (useCache : Bool) (e r : Expr) : MetaM Expr := do
     modify fun s => { s with cache.whnf := s.cache.whnf.insert key r }
   return r
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_whnf]
 partial def whnfImp (e : Expr) : MetaM Expr :=
   withIncRecDepth <| whnfEasyCases e fun e => do

src/Lean/Meta/WrapInstance.lean

@@ -13,17 +13,16 @@ public import Lean.Meta.CtorRecognizer
 public section
 
 /-!
-# Instance Normal Form
+# Instance Wrapping
 
-Both `inferInstanceAs` and the default `deriving` handler normalize instance bodies to
-"instance normal form". This ensures that when deriving or inferring an instance for a
-semireducible type definition, the definition's RHS is not leaked when reduced at lower
-than semireducible transparency.
+Both `inferInstanceAs` and the default `deriving` handler wrap instance bodies to ensure
+that when deriving or inferring an instance for a semireducible type definition, the
+definition's RHS is not leaked when reduced at lower than semireducible transparency.
 
 ## Algorithm
 
 Given an instance `i : I` and expected type `I'` (where `I'` must be mvar-free),
-`normalizeInstance` constructs a result instance as follows, executing all steps at
+`wrapInstance` constructs a result instance as follows, executing all steps at
 `instances` transparency:
 
 1. If `I'` is not a class, return `i` unchanged.
@@ -46,7 +45,7 @@ Given an instance `i : I` and expected type `I'` (where `I'` must be mvar-free),
 
 ## Options
 
-- `backward.inferInstanceAs.wrap`: master switch for normalization in both `inferInstanceAs`
+- `backward.inferInstanceAs.wrap`: master switch for wrapping in both `inferInstanceAs`
   and the default `deriving` handler
 - `backward.inferInstanceAs.wrap.reuseSubInstances`: reuse existing instances for sub-instance
   fields to avoid non-defeq instance diamonds
@@ -59,7 +58,7 @@ namespace Lean.Meta
 
 register_builtin_option backward.inferInstanceAs.wrap : Bool := {
   defValue := true
-  descr := "normalize instance bodies to constructor-based normal form in `inferInstanceAs` and the default `deriving` handler"
+  descr := "wrap instance bodies in `inferInstanceAs` and the default `deriving` handler"
 }
 
 register_builtin_option backward.inferInstanceAs.wrap.reuseSubInstances : Bool := {
@@ -77,7 +76,7 @@ register_builtin_option backward.inferInstanceAs.wrap.data : Bool := {
   descr := "wrap data fields in auxiliary definitions to fix their types"
 }
 
-builtin_initialize registerTraceClass `Meta.instanceNormalForm
+builtin_initialize registerTraceClass `Meta.wrapInstance
 
 /--
 Rebuild a type application with fresh synthetic metavariables for instance-implicit arguments.
@@ -95,16 +94,16 @@ def abstractInstImplicitArgs (type : Expr) : MetaM Expr := do
   instantiateMVars (mkAppN fn args)
 
 /--
-Normalize an instance value to "instance normal form".
+Wrap an instance value so its type matches the expected type exactly.
 See the module docstring for the full algorithm specification.
 -/
-partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true)
-    (logCompileErrors : Bool := true) : MetaM Expr := withTransparency .instances do
-  withTraceNode `Meta.instanceNormalForm
+partial def wrapInstance (inst expectedType : Expr) (compile : Bool := true)
+    (logCompileErrors : Bool := true) (isMeta : Bool := false) : MetaM Expr := withTransparency .instances do
+  withTraceNode `Meta.wrapInstance
       (fun _ => return m!"type: {expectedType}") do
   let some className ← isClass? expectedType
     | return inst
-  trace[Meta.instanceNormalForm] "class is {className}"
+  trace[Meta.wrapInstance] "class is {className}"
 
   if ← isProp expectedType then
     if backward.inferInstanceAs.wrap.instances.get (← getOptions) then
@@ -117,27 +116,29 @@ partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true
   inst.withApp fun f args => do
     let some (.ctorInfo ci) ← f.constName?.mapM getConstInfo
       | do
-        trace[Meta.instanceNormalForm] "did not reduce to constructor application, returning/wrapping as is: {inst}"
+        trace[Meta.wrapInstance] "did not reduce to constructor application, returning/wrapping as is: {inst}"
         if backward.inferInstanceAs.wrap.instances.get (← getOptions) then
           let instType ← inferType inst
           if ← isDefEq expectedType instType then
             return inst
           else
             let name ← mkAuxDeclName
-            let wrapped ← mkAuxDefinition name expectedType inst (compile := compile)
-              (logCompileErrors := logCompileErrors)
+            let wrapped ← mkAuxDefinition name expectedType inst (compile := false)
             setReducibilityStatus name .implicitReducible
+            if isMeta then modifyEnv (markMeta · name)
+            if compile then
+              compileDecls (logErrors := logCompileErrors) #[name]
             enableRealizationsForConst name
             return wrapped
         else
           return inst
     let (mvars, _, cls) ← forallMetaTelescope (← inferType f)
     if h₁ : args.size ≠ mvars.size then
-      throwError "instance normal form: incorrect number of arguments for \
+      throwError "wrapInstance: incorrect number of arguments for \
         constructor application `{f}`: {args}"
     else
       unless ← isDefEq expectedType cls do
-        throwError "instance normal form: `{expectedType}` does not unify with the conclusion of \
+        throwError "wrapInstance: `{expectedType}` does not unify with the conclusion of \
           `{.ofConstName ci.name}`"
       for h₂ : i in ci.numParams...args.size do
         have : i < mvars.size := by
@@ -153,7 +154,7 @@ partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true
           if ← isDefEq argExpectedType argType then
             mvarId.assign arg
           else
-            trace[Meta.instanceNormalForm] "proof field {i} does not have expected type {argExpectedType} but {argType}, wrapping in auxiliary theorem: {arg}"
+            trace[Meta.wrapInstance] "proof field {i} does not have expected type {argExpectedType} but {argType}, wrapping in auxiliary theorem: {arg}"
             mvarId.assign (← mkAuxTheorem argExpectedType arg (zetaDelta := true))
         -- Recurse into instance arguments of the constructor
         else if (← isClass? argExpectedType).isSome then
@@ -163,13 +164,13 @@ partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true
             -- semireducible transparency.
             try
               if let .some new ← trySynthInstance argExpectedType then
-                trace[Meta.instanceNormalForm] "using existing instance {new}"
+                trace[Meta.wrapInstance] "using existing instance {new}"
                 mvarId.assign new
                 continue
             catch _ => pure ()
 
-          mvarId.assign (← normalizeInstance arg argExpectedType (compile := compile)
-            (logCompileErrors := logCompileErrors))
+          mvarId.assign (← wrapInstance arg argExpectedType (compile := compile)
+            (logCompileErrors := logCompileErrors) (isMeta := isMeta))
         else
           -- For data fields, assign directly or wrap in aux def to fix types.
           if backward.inferInstanceAs.wrap.data.get (← getOptions) then
@@ -180,6 +181,7 @@ partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true
               let name ← mkAuxDeclName
               mvarId.assign (← mkAuxDefinition name argExpectedType arg (compile := false))
               setInlineAttribute name
+              if isMeta then modifyEnv (markMeta · name)
               if compile then
                 compileDecls (logErrors := logCompileErrors) #[name]
               enableRealizationsForConst name

src/Lean/Parser.lean

@@ -65,6 +65,7 @@ end Parser
 namespace PrettyPrinter
 namespace Parenthesizer
 
+set_option compiler.ignoreBorrowAnnotation true in
 -- Close the mutual recursion loop; see corresponding `[extern]` in the parenthesizer.
 @[export lean_mk_antiquot_parenthesizer]
 def mkAntiquot.parenthesizer (name : String) (kind : SyntaxNodeKind) (anonymous := true) (isPseudoKind := true) : Parenthesizer :=
@@ -80,6 +81,7 @@ def mkAntiquot.parenthesizer (name : String) (kind : SyntaxNodeKind) (anonymous
 
 open Lean.Parser
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_pretty_printer_parenthesizer_interpret_parser_descr]
 unsafe def interpretParserDescr : ParserDescr → CoreM Parenthesizer
   | ParserDescr.const n                             => getConstAlias parenthesizerAliasesRef n
@@ -101,6 +103,7 @@ end Parenthesizer
 
 namespace Formatter
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_mk_antiquot_formatter]
 def mkAntiquot.formatter (name : String) (kind : SyntaxNodeKind) (anonymous := true) (isPseudoKind := true) : Formatter :=
   Parser.mkAntiquot.formatter name kind anonymous isPseudoKind
@@ -113,6 +116,7 @@ def mkAntiquot.formatter (name : String) (kind : SyntaxNodeKind) (anonymous := t
 
 open Lean.Parser
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_pretty_printer_formatter_interpret_parser_descr]
 unsafe def interpretParserDescr : ParserDescr → CoreM Formatter
   | ParserDescr.const n                             => getConstAlias formatterAliasesRef n

src/Lean/Parser/Term.lean

@@ -774,10 +774,15 @@ In particular, it is like a unary operation with a fixed parameter `b`, where on
 @[builtin_term_parser] def noImplicitLambda := leading_parser
   "no_implicit_lambda% " >> termParser maxPrec
 /--
-`inferInstanceAs α` synthesizes an instance of type `α` and normalizes it to
-"instance normal form": the result is a constructor application whose sub-instance
-fields are canonical instances and whose types match `α` exactly. See
-`Lean.Meta.InstanceNormalForm` for details.
+`inferInstanceAs α` synthesizes an instance of type `α`, transporting it from a
+definitionally equal type if necessary. This is useful when `α` is definitionally equal to
+some `α'` for which instances are registered, as it prevents leaking the definition's RHS
+at lower transparencies.
+
+`inferInstanceAs` requires an expected type from context. If you just need to synthesize an
+instance without transporting between types, use `inferInstance` instead.
+
+See `Lean.Meta.WrapInstance` for details.
 -/
 @[builtin_term_parser] def «inferInstanceAs» := leading_parser
   "inferInstanceAs" >> (((" $ " <|> " <| ") >> termParser minPrec) <|> (ppSpace >> termParser argPrec))

src/Lean/Util/FoldConsts.lean

@@ -64,11 +64,10 @@ namespace ConstantInfo
 
 /-- Return all names appearing in the type or value of a `ConstantInfo`. -/
 def getUsedConstantsAsSet (c : ConstantInfo) : NameSet :=
-  c.type.getUsedConstantsAsSet ++ match c.value? with
+  c.type.getUsedConstantsAsSet ++ match c.value? (allowOpaque := true) with
   | some v => v.getUsedConstantsAsSet
   | none => match c with
     | .inductInfo val => .ofList val.ctors
-    | .opaqueInfo val => val.value.getUsedConstantsAsSet
     | .ctorInfo val => ({} : NameSet).insert val.name
     | .recInfo val => .ofList val.all
     | _ => {}

src/Std/Data/String/ToInt.lean

@@ -98,18 +98,34 @@ end Slice
 public theorem isInt_toSlice {s : String} : s.toSlice.isInt = s.isInt :=
   (rfl)
 
+@[simp]
+public theorem isInt_comp_toSlice : String.Slice.isInt ∘ String.toSlice = String.isInt := by
+  ext; simp
+
 @[simp]
 public theorem toInt?_toSlice {s : String} : s.toSlice.toInt? = s.toInt? :=
   (rfl)
 
+@[simp]
+public theorem toInt?_comp_toSlice : String.Slice.toInt? ∘ String.toSlice = String.toInt? := by
+  ext; simp
+
 @[simp]
 public theorem Slice.isInt_copy {s : Slice} : s.copy.isInt = s.isInt := by
   simpa [← isInt_toSlice] using Slice.isInt_congr (by simp)
 
+@[simp]
+public theorem Slice.isInt_comp_copy : String.isInt ∘ String.Slice.copy = String.Slice.isInt := by
+  ext; simp
+
 @[simp]
 public theorem Slice.toInt?_copy {s : Slice} : s.copy.toInt? = s.toInt? := by
   simpa [← isInt_toSlice] using Slice.toInt?_congr (by simp)
 
+@[simp]
+public theorem Slice.toInt?_comp_copy : String.toInt? ∘ String.Slice.copy = String.Slice.toInt? := by
+  ext; simp
+
 public theorem toInt?_eq_some_iff {s : String} {a : Int} :
     s.toInt? = some a ↔ (∃ b, s.toNat? = some b ∧ a = (b : Int)) ∨ ∃ t, s = "-" ++ t ∧ ∃ b, t.toNat? = some b ∧ a = -(b : Int) := by
   simp [← toInt?_toSlice, Slice.toInt?_eq_some_iff]

src/Std/Data/String/ToNat.lean

@@ -221,18 +221,34 @@ namespace String
 public theorem isNat_toSlice {s : String} : s.toSlice.isNat = s.isNat :=
   (rfl)
 
+@[simp]
+public theorem isNat_comp_toSlice : String.Slice.isNat ∘ String.toSlice = String.isNat := by
+  ext; simp
+
 @[simp]
 public theorem toNat?_toSlice {s : String} : s.toSlice.toNat? = s.toNat? :=
   (rfl)
 
+@[simp]
+public theorem toNat?_comp_toSlice : String.Slice.toNat? ∘ String.toSlice = String.toNat? := by
+  ext; simp
+
 @[simp]
 public theorem Slice.isNat_copy {s : Slice} : s.copy.isNat = s.isNat := by
   simpa [← isNat_toSlice] using Slice.isNat_congr (by simp)
 
+@[simp]
+public theorem Slice.isNat_comp_copy : String.isNat ∘ String.Slice.copy = String.Slice.isNat := by
+  ext; simp
+
 @[simp]
 public theorem Slice.toNat?_copy {s : Slice} : s.copy.toNat? = s.toNat? := by
   simpa [← isNat_toSlice] using Slice.toNat?_congr (by simp)
 
+@[simp]
+public theorem Slice.toNat?_comp_copy : String.toNat? ∘ String.Slice.copy = String.Slice.toNat? := by
+  ext; simp
+
 public theorem isNat_iff {s : String} :
     s.isNat = true ↔
       s ≠ "" ∧

src/Std/Do/Triple/SpecLemmas.lean

@@ -136,6 +136,15 @@ theorem Cursor.pos_at {l : List α} {n : Nat} (h : n < l.length) :
 theorem Cursor.pos_mk {l pre suff : List α} (h : pre ++ suff = l) :
     (Cursor.mk pre suff h).pos = pre.length := rfl
 
+theorem Cursor.pos_le_length {c : Cursor l} : c.pos ≤ l.length := by
+  simp [← congrArg List.length c.property]
+
+theorem Cursor.length_prefix_le_length {c : Cursor l} : c.prefix.length ≤ l.length :=
+  pos_le_length
+
+theorem Cursor.length_suffix_le_length {c : Cursor l} : c.suffix.length ≤ l.length := by
+  simp [← congrArg List.length c.property]
+
 @[grind →]
 theorem eq_of_range'_eq_append_cons (h : range' s n step = xs ++ cur :: ys) :
     cur = s + step * xs.length := by

src/Std/Tactic/Do/Syntax.lean

@@ -364,30 +364,15 @@ macro "mvcgen_trivial" : tactic =>
   )
 
 /--
-A goal section alternative of the form `· term`, one per goal.
-Used by both `invariants` and `witnesses` sections.
+An invariant alternative of the form `· term`, one per invariant goal.
 -/
 syntax goalDotAlt := ppDedent(ppLine) cdotTk (colGe term)
 
 /--
-A goal section alternative of the form `| label<n> a b c => term`, one per goal.
-Used by both `invariants` and `witnesses` sections.
+An invariant alternative of the form `| inv<n> a b c => term`, one per invariant goal.
 -/
 syntax goalCaseAlt := ppDedent(ppLine) "| " caseArg " => " (colGe term)
 
-/--
-The contextual keyword ` witnesses `.
--/
-syntax witnessesKW := &"witnesses "
-
-/--
-After `mvcgen [...]`, there can be an optional `witnesses` followed by either
-* a bulleted list of witnesses `· term; · term`.
-* a labelled list of witnesses `| witness1 => term; witness2 a b c => term`, which is useful for
-  naming inaccessibles.
--/
-syntax witnessAlts := witnessesKW withPosition((colGe (goalDotAlt <|> goalCaseAlt))*)
-
 /--
 Either the contextual keyword ` invariants ` or its tracing form ` invariants? ` which suggests
 skeletons for missing invariants as a hint.
@@ -395,7 +380,7 @@ skeletons for missing invariants as a hint.
 syntax invariantsKW := &"invariants " <|> &"invariants? "
 
 /--
-After `mvcgen [...] witnesses ...`, there can be an optional `invariants` followed by either
+After `mvcgen [...]`, there can be an optional `invariants` followed by either
 * a bulleted list of invariants `· term; · term`.
 * a labelled list of invariants `| inv1 => term; inv2 a b c => term`, which is useful for naming
   inaccessibles.
@@ -419,7 +404,7 @@ syntax vcAlts := "with " (ppSpace colGt tactic)? withPosition((colGe vcAlt)*)
 @[tactic_alt Lean.Parser.Tactic.mvcgenMacro]
 syntax (name := mvcgen) "mvcgen" optConfig
   (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "] ")?
-  (witnessAlts)? (invariantAlts)? (vcAlts)? : tactic
+  (invariantAlts)? (vcAlts)? : tactic
 
 /--
 A hint tactic that expands to `mvcgen invariants?`.

src/include/lean/lean.h

@@ -319,6 +319,7 @@ LEAN_EXPORT void lean_set_panic_messages(bool flag);
 
 LEAN_EXPORT void lean_panic(char const * msg, bool force_stderr);
 LEAN_EXPORT lean_object * lean_panic_fn(lean_object * default_val, lean_object * msg);
+LEAN_EXPORT lean_object * lean_panic_fn_borrowed(b_lean_obj_arg default_val, lean_object * msg);
 
 LEAN_EXPORT LEAN_NORETURN void lean_internal_panic(char const * msg);
 LEAN_EXPORT LEAN_NORETURN void lean_internal_panic_out_of_memory(void);
@@ -847,11 +848,10 @@ static inline lean_obj_res lean_array_fget_borrowed(b_lean_obj_arg a, b_lean_obj
 
 LEAN_EXPORT lean_obj_res lean_array_get_panic(lean_obj_arg def_val);
 
-static inline lean_object * lean_array_get(lean_obj_arg def_val, b_lean_obj_arg a, b_lean_obj_arg i) {
+static inline lean_object * lean_array_get(b_lean_obj_arg def_val, b_lean_obj_arg a, b_lean_obj_arg i) {
     if (lean_is_scalar(i)) {
         size_t idx = lean_unbox(i);
         if (idx < lean_array_size(a)) {
-            lean_dec(def_val);
             return lean_array_uget(a, idx);
         }
     }
@@ -859,14 +859,14 @@ static inline lean_object * lean_array_get(lean_obj_arg def_val, b_lean_obj_arg
        i > LEAN_MAX_SMALL_NAT == MAX_UNSIGNED >> 1
        but each array entry is 8 bytes in 64-bit machines and 4 in 32-bit ones.
        In both cases, we would be out-of-memory. */
+    lean_inc(def_val);
     return lean_array_get_panic(def_val);
 }
 
-static inline lean_object * lean_array_get_borrowed(lean_obj_arg def_val, b_lean_obj_arg a, b_lean_obj_arg i) {
+static inline lean_object * lean_array_get_borrowed(b_lean_obj_arg def_val, b_lean_obj_arg a, b_lean_obj_arg i) {
     if (lean_is_scalar(i)) {
         size_t idx = lean_unbox(i);
         if (idx < lean_array_size(a)) {
-            lean_dec(def_val);
             return lean_array_get_core(a, idx);
         }
     }
@@ -874,6 +874,7 @@ static inline lean_object * lean_array_get_borrowed(lean_obj_arg def_val, b_lean
        i > LEAN_MAX_SMALL_NAT == MAX_UNSIGNED >> 1
        but each array entry is 8 bytes in 64-bit machines and 4 in 32-bit ones.
        In both cases, we would be out-of-memory. */
+    lean_inc(def_val);
     return lean_array_get_panic(def_val);
 }