feat: throw an error when export declarations have borrow annotations

.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-5gb"]', matrix.os)) || matrix.os }}
+    runs-on: ${{ endsWith(matrix.os, '-with-cache') && fromJSON(format('["{0}", "nscloud-git-mirror-1gb"]', 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=${{ matrix.name == 'Linux Lake (Cached)' && '10' || '1' }} origin ${{ github.sha }}
+          git fetch --depth=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: Configure Build
+      - name: Build
         run: |
           ulimit -c unlimited  # coredumps
           [ -d build ] || mkdir build
@@ -162,21 +162,7 @@ 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/..
-      - 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
+          time make $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
@@ -195,21 +181,6 @@ 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

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

@@ -61,19 +61,15 @@ jobs:
             git remote add nightly https://foo:'${{ secrets.PUSH_NIGHTLY_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-nightly.git
             git fetch nightly --tags
             if [[ '${{ github.event_name }}' == 'workflow_dispatch' ]]; then
-              # Manual re-release: retry today's nightly, or create a revision if it already exists
-              TODAY_NIGHTLY="nightly-$(date -u +%F)"
-              if git rev-parse "refs/tags/${TODAY_NIGHTLY}" >/dev/null 2>&1; then
-                # Today's nightly already exists, create a revision
-                REV=1
-                while git rev-parse "refs/tags/${TODAY_NIGHTLY}-rev${REV}" >/dev/null 2>&1; do
-                  REV=$((REV + 1))
-                done
-                LEAN_VERSION_STRING="${TODAY_NIGHTLY}-rev${REV}"
-              else
-                # Today's nightly doesn't exist yet (e.g. scheduled run failed), create it
-                LEAN_VERSION_STRING="${TODAY_NIGHTLY}"
-              fi
+              # Manual re-release: create a revision of the most recent nightly
+              BASE_NIGHTLY=$(git tag -l 'nightly-*' | sort -rV | head -1)
+              # Strip any existing -revK suffix to get the base date tag
+              BASE_NIGHTLY="${BASE_NIGHTLY%%-rev*}"
+              REV=1
+              while git rev-parse "refs/tags/${BASE_NIGHTLY}-rev${REV}" >/dev/null 2>&1; do
+                REV=$((REV + 1))
+              done
+              LEAN_VERSION_STRING="${BASE_NIGHTLY}-rev${REV}"
               echo "nightly=$LEAN_VERSION_STRING" >> "$GITHUB_OUTPUT"
             else
               # Scheduled: do nothing if commit already has a different tag
@@ -244,7 +240,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-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
+                "os": large && fast ? "nscloud-ubuntu-22.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 +261,7 @@ jobs:
               },
               {
                 "name": "Linux Lake",
-                "os": large ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
+                "os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
                 "enabled": true,
                 "check-rebootstrap": level >= 1,
                 "check-stage3": level >= 2,
@@ -273,19 +269,7 @@ 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 -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",
+                "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror",
               },
               {
                 "name": "Linux Reldebug",
@@ -299,7 +283,7 @@ jobs:
               {
                 "name": "Linux fsanitize",
                 // Always run on large if available, more reliable regarding timeouts
-                "os": large ? "nscloud-ubuntu-24.04-amd64-16x32-with-cache" : "ubuntu-latest",
+                "os": large ? "nscloud-ubuntu-22.04-amd64-16x32-with-cache" : "ubuntu-latest",
                 "enabled": level >= 2,
                 // do not fail nightlies on this for now
                 "secondary": level <= 2,

doc/examples/interp.lean.out.expected

@@ -1,4 +1,3 @@
 30
 interp.lean:146:4: warning: declaration uses `sorry`
-interp.lean:146:0: warning: declaration uses `sorry`
 3628800

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-") or version1.startswith("leanprover/lean4-nightly:"):
+    if version1.startswith("leanprover/lean4:nightly-"):
         return False
     return parse_version(version1) >= parse_version(version2)
 

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

@@ -72,11 +72,11 @@ public instance [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m]
 
 public instance [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] :
     WeaklyLawfulMonadAttach (StateRefT' ω σ m) :=
-  inferInstanceAs (WeaklyLawfulMonadAttach (ReaderT (ST.Ref ω σ) m))
+  inferInstanceAs (WeaklyLawfulMonadAttach (ReaderT _ _))
 
 public instance [Monad m] [MonadAttach m] [LawfulMonad m] [LawfulMonadAttach m] :
     LawfulMonadAttach (StateRefT' ω σ m) :=
-  inferInstanceAs (LawfulMonadAttach (ReaderT (ST.Ref ω σ) m))
+  inferInstanceAs (LawfulMonadAttach (ReaderT _ _))
 
 section
 

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

@@ -103,11 +103,11 @@ namespace StateRefT'
 instance {ω σ : Type} {m : Type → Type} [Monad m] : LawfulMonadLift m (StateRefT' ω σ m) where
   monadLift_pure _ := by
     simp only [MonadLift.monadLift, pure]
-    unfold StateRefT'.lift instMonad._aux_5 ReaderT.pure
+    unfold StateRefT'.lift ReaderT.pure
     simp only
   monadLift_bind _ _ := by
     simp only [MonadLift.monadLift, bind]
-    unfold StateRefT'.lift instMonad._aux_13 ReaderT.bind
+    unfold StateRefT'.lift ReaderT.bind
     simp only
 
 end StateRefT'

src/Init/Data/BEq.lean

@@ -66,8 +66,3 @@ 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,8 +98,4 @@ 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/Iterators/Combinators/Monadic/FilterMap.lean

@@ -168,13 +168,6 @@ instance Map.instIterator {α β γ : Type w} {m : Type w → Type w'} {n : Type
     Iterator (Map α m n lift f) n γ :=
   inferInstanceAs <| Iterator (FilterMap α m n lift _) n γ
 
-theorem Map.instIterator_eq_filterMapInstIterator {α β γ : Type w} {m : Type w → Type w'}
-    {n : Type w → Type w''} [Monad n]
-    [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n γ} :
-    Map.instIterator (α := α) (β := β) (γ := γ) (m := m) (n := n) (lift := lift) (f := f) =
-      FilterMap.instIterator :=
-  rfl
-
 private def FilterMap.instFinitenessRelation {α β γ : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α}
     {f : β → PostconditionT n (Option γ)} [Finite α m] :

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

@@ -699,16 +699,18 @@ theorem IterM.toList_map {α β β' : Type w} {m : Type w → Type w'} [Monad m]
     (it : IterM (α := α) m β) :
     (it.map f).toList = (fun x => x.map f) <$> it.toList := by
   rw [← List.filterMap_eq_map, ← toList_filterMap]
-  simp only [map, mapWithPostcondition, InternalCombinators.map, filterMap,
-    filterMapWithPostcondition, InternalCombinators.filterMap]
-  unfold Map
+  let t := type_of% (it.map f)
+  let t' := type_of% (it.filterMap (some ∘ f))
   congr
-  · simp
-  · rw [Map.instIterator_eq_filterMapInstIterator]
+  · simp [Map]
+  · simp [Map.instIterator, inferInstanceAs]
     congr
     simp
-  · simp
-  · simp
+  · simp only [map, mapWithPostcondition, InternalCombinators.map, Function.comp_apply, filterMap,
+    filterMapWithPostcondition, InternalCombinators.filterMap]
+    congr
+    · simp [Map]
+    · simp
 
 @[simp]
 theorem IterM.toList_filter {α : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m]
@@ -1308,8 +1310,7 @@ theorem IterM.forIn_mapWithPostcondition
     haveI : MonadLift n o := ⟨monadLift⟩
     forIn (it.mapWithPostcondition f) init g =
       forIn it init (fun out acc => do g (← (f out).run) acc) := by
-  unfold mapWithPostcondition InternalCombinators.map Map.instIteratorLoop Map
-  rw [Map.instIterator_eq_filterMapInstIterator]
+  unfold mapWithPostcondition InternalCombinators.map Map.instIterator Map.instIteratorLoop Map
   rw [← InternalCombinators.filterMap, ← filterMapWithPostcondition, forIn_filterMapWithPostcondition]
   simp
 

src/Init/Data/List/MinMaxIdx.lean

@@ -481,13 +481,13 @@ protected theorem maxIdxOn_nil_eq_iff_false [LE β] [DecidableLE β] {f : α →
 @[simp]
 protected theorem maxIdxOn_singleton [LE β] [DecidableLE β] {x : α} {f : α → β} :
     [x].maxIdxOn f (of_decide_eq_false rfl) = 0 :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.minIdxOn_singleton
 
 @[simp]
 protected theorem maxIdxOn_lt_length [LE β] [DecidableLE β] {f : α → β} {xs : List α}
     (h : xs ≠ []) : xs.maxIdxOn f h < xs.length :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.minIdxOn_lt_length h
 
 protected theorem maxIdxOn_le_of_apply_getElem_le_apply_maxOn [LE β] [DecidableLE β] [IsLinearPreorder β]
@@ -495,7 +495,7 @@ protected theorem maxIdxOn_le_of_apply_getElem_le_apply_maxOn [LE β] [Decidable
     {k : Nat} (hi : k < xs.length) (hle : f (xs.maxOn f h) ≤ f xs[k]) :
     xs.maxIdxOn f h ≤ k := by
   simp only [List.maxIdxOn_eq_minIdxOn, List.maxOn_eq_minOn] at hle ⊢
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   exact List.minIdxOn_le_of_apply_getElem_le_apply_minOn h hi (by simpa [LE.le_opposite_iff] using hle)
 
 protected theorem apply_maxOn_lt_apply_getElem_of_lt_maxIdxOn [LE β] [DecidableLE β] [LT β] [IsLinearPreorder β]
@@ -513,7 +513,7 @@ protected theorem getElem_maxIdxOn [LE β] [DecidableLE β] [IsLinearPreorder β
     {f : α → β} {xs : List α} (h : xs ≠ []) :
     xs[xs.maxIdxOn f h] = xs.maxOn f h := by
   simp only [List.maxIdxOn_eq_minIdxOn, List.maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   exact List.getElem_minIdxOn h
 
 protected theorem le_maxIdxOn_of_apply_getElem_lt_apply_getElem [LE β] [DecidableLE β] [LT β]
@@ -562,14 +562,14 @@ protected theorem maxIdxOn_cons
       else if f (xs.maxOn f h) ≤ f x then 0
       else (xs.maxIdxOn f h) + 1 := by
   simp only [List.maxIdxOn_eq_minIdxOn, List.maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa [LE.le_opposite_iff] using List.minIdxOn_cons (f := f)
 
 protected theorem maxIdxOn_eq_zero_iff [LE β] [DecidableLE β] [IsLinearPreorder β]
     {xs : List α} {f : α → β} (h : xs ≠ []) :
     xs.maxIdxOn f h = 0 ↔ ∀ x ∈ xs, f x ≤ f (xs.head h) := by
   simp only [List.maxIdxOn_eq_minIdxOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa [LE.le_opposite_iff] using List.minIdxOn_eq_zero_iff h (f := f)
 
 protected theorem maxIdxOn_append [LE β] [DecidableLE β] [IsLinearPreorder β]
@@ -580,26 +580,26 @@ protected theorem maxIdxOn_append [LE β] [DecidableLE β] [IsLinearPreorder β]
       else
         xs.length + ys.maxIdxOn f hys := by
   simp only [List.maxIdxOn_eq_minIdxOn, List.maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa [LE.le_opposite_iff] using List.minIdxOn_append hxs hys (f := f)
 
 protected theorem left_le_maxIdxOn_append [LE β] [DecidableLE β] [IsLinearPreorder β]
     {xs ys : List α} {f : α → β} (h : xs ≠ []) :
     xs.maxIdxOn f h ≤ (xs ++ ys).maxIdxOn f (by simp [h]) :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.left_le_minIdxOn_append h
 
 protected theorem maxIdxOn_take_le [LE β] [DecidableLE β] [IsLinearPreorder β]
     {xs : List α} {f : α → β} {i : Nat} (h : xs.take i ≠ []) :
     (xs.take i).maxIdxOn f h ≤ xs.maxIdxOn f (List.ne_nil_of_take_ne_nil h) :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.minIdxOn_take_le h
 
 @[simp]
 protected theorem maxIdxOn_replicate [LE β] [DecidableLE β] [Refl (α := β) (· ≤ ·)]
     {n : Nat} {a : α} {f : α → β} (h : replicate n a ≠ []) :
     (replicate n a).maxIdxOn f h = 0 :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.minIdxOn_replicate h
 
 @[simp]

src/Init/Data/List/MinMaxOn.lean

@@ -297,13 +297,13 @@ protected theorem maxOn_cons
     (x :: xs).maxOn f (by exact of_decide_eq_false rfl) =
       if h : xs = [] then x else maxOn f x (xs.maxOn f h) := by
   simp only [maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   exact List.minOn_cons (f := f)
 
 protected theorem maxOn_cons_cons [LE β] [DecidableLE β] {a b : α} {l : List α} {f : α → β} :
     (a :: b :: l).maxOn f (by simp) = (maxOn f a b :: l).maxOn f (by simp) := by
   simp only [List.maxOn_eq_minOn, maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   exact List.minOn_cons_cons
 
 @[simp]
@@ -334,51 +334,51 @@ protected theorem maxOn_id [Max α] [LE α] [DecidableLE α] [LawfulOrderLeftLea
     {xs : List α} (h : xs ≠ []) :
     xs.maxOn id h = xs.max h := by
   simp only [List.maxOn_eq_minOn]
-  letI : LE α := (inferInstance : LE α).opposite
-  letI : Min α := (inferInstance : Max α).oppositeMin
+  letI : LE α := (inferInstanceAs (LE α)).opposite
+  letI : Min α := (inferInstanceAs (Max α)).oppositeMin
   simpa only [List.max_eq_min] using List.minOn_id h
 
 @[simp]
 protected theorem maxOn_mem [LE β] [DecidableLE β] {xs : List α}
     {f : α → β} {h : xs ≠ []} : xs.maxOn f h ∈ xs :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.minOn_mem (f := f)
 
 protected theorem le_apply_maxOn_of_mem [LE β] [DecidableLE β] [IsLinearPreorder β]
     {xs : List α} {f : α → β} {y : α} (hx : y ∈ xs) :
     f y ≤ f (xs.maxOn f (List.ne_nil_of_mem hx)) := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa [LE.le_opposite_iff] using List.apply_minOn_le_of_mem (f := f) hx
 
 protected theorem apply_maxOn_le_iff [LE β] [DecidableLE β] [IsLinearPreorder β] {xs : List α}
     {f : α → β} (h : xs ≠ []) {b : β} :
     f (xs.maxOn f h) ≤ b ↔ ∀ x ∈ xs, f x ≤ b := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa [LE.le_opposite_iff] using List.le_apply_minOn_iff (f := f) h
 
 protected theorem le_apply_maxOn_iff [LE β] [DecidableLE β] [IsLinearPreorder β] {xs : List α}
     {f : α → β} (h : xs ≠ []) {b : β} :
     b ≤ f (xs.maxOn f h) ↔ ∃ x ∈ xs, b ≤ f x := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa [LE.le_opposite_iff] using List.apply_minOn_le_iff (f := f) h
 
 protected theorem apply_maxOn_lt_iff
      [LE β] [DecidableLE β] [LT β] [IsLinearPreorder β] [LawfulOrderLT β]
     {xs : List α} {f : α → β} (h : xs ≠ []) {b : β} :
     f (xs.maxOn f h) < b ↔ ∀ x ∈ xs, f x < b := by
-  letI : LE β := (inferInstance : LE β).opposite
-  letI : LT β := (inferInstance : LT β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LT β := (inferInstanceAs (LT β)).opposite
   simpa [LT.lt_opposite_iff] using List.lt_apply_minOn_iff (f := f) h
 
 protected theorem lt_apply_maxOn_iff
      [LE β] [DecidableLE β] [LT β] [IsLinearPreorder β] [LawfulOrderLT β]
     {xs : List α} {f : α → β} (h : xs ≠ []) {b : β} :
     b < f (xs.maxOn f h) ↔ ∃ x ∈ xs, b < f x := by
-  letI : LE β := (inferInstance : LE β).opposite
-  letI : LT β := (inferInstance : LT β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LT β := (inferInstanceAs (LT β)).opposite
   simpa [LT.lt_opposite_iff] using List.apply_minOn_lt_iff (f := f) h
 
 protected theorem apply_maxOn_le_apply_maxOn_of_subset [LE β] [DecidableLE β]
@@ -386,14 +386,14 @@ protected theorem apply_maxOn_le_apply_maxOn_of_subset [LE β] [DecidableLE β]
     haveI : xs ≠ [] := by intro h; rw [h] at hxs; simp_all [subset_nil]
     f (ys.maxOn f hys) ≤ f (xs.maxOn f this) := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa [LE.le_opposite_iff] using List.apply_minOn_le_apply_minOn_of_subset (f := f) hxs hys
 
 protected theorem apply_maxOn_take_le [LE β] [DecidableLE β] [IsLinearPreorder β]
     {xs : List α} {f : α → β} {i : Nat} (h : xs.take i ≠ []) :
     f ((xs.take i).maxOn f h) ≤ f (xs.maxOn f (List.ne_nil_of_take_ne_nil h)) := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa [LE.le_opposite_iff] using List.le_apply_minOn_take (f := f) h
 
 protected theorem le_apply_maxOn_append_left [LE β] [DecidableLE β] [IsLinearPreorder β]
@@ -401,7 +401,7 @@ protected theorem le_apply_maxOn_append_left [LE β] [DecidableLE β] [IsLinearP
     f (xs.maxOn f h) ≤
       f ((xs ++ ys).maxOn f (append_ne_nil_of_left_ne_nil h ys)) := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa [LE.le_opposite_iff] using List.apply_minOn_append_le_left (f := f) h
 
 protected theorem le_apply_maxOn_append_right [LE β] [DecidableLE β] [IsLinearPreorder β]
@@ -409,7 +409,7 @@ protected theorem le_apply_maxOn_append_right [LE β] [DecidableLE β] [IsLinear
     f (ys.maxOn f h) ≤
       f ((xs ++ ys).maxOn f (append_ne_nil_of_right_ne_nil xs h)) := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa [LE.le_opposite_iff] using List.apply_minOn_append_le_right (f := f) h
 
 @[simp]
@@ -417,21 +417,21 @@ protected theorem maxOn_append [LE β] [DecidableLE β] [IsLinearPreorder β] {x
     {f : α → β} (hxs : xs ≠ []) (hys : ys ≠ []) :
     (xs ++ ys).maxOn f (by simp [hxs]) = maxOn f (xs.maxOn f hxs) (ys.maxOn f hys) := by
   simp only [List.maxOn_eq_minOn, maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa [LE.le_opposite_iff] using List.minOn_append (f := f) hxs hys
 
 protected theorem maxOn_eq_head [LE β] [DecidableLE β] [IsLinearPreorder β] {xs : List α}
     {f : α → β} (h : xs ≠ []) (h' : ∀ x ∈ xs, f x ≤ f (xs.head h)) :
     xs.maxOn f h = xs.head h := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa [LE.le_opposite_iff] using List.minOn_eq_head (f := f) h (by simpa [LE.le_opposite_iff] using h')
 
 protected theorem max_map
     [LE β] [DecidableLE β] [Max β] [IsLinearPreorder β] [LawfulOrderLeftLeaningMax β] {xs : List α}
     {f : α → β} (h : xs ≠ []) : (xs.map f).max (by simpa) = f (xs.maxOn f h) := by
-  letI : LE β := (inferInstance : LE β).opposite
-  letI : Min β := (inferInstance : Max β).oppositeMin
+  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : Min β := (inferInstanceAs (Max β)).oppositeMin
   simpa [List.max_eq_min] using List.min_map (f := f) h
 
 protected theorem maxOn_eq_max [Max α] [LE α] [DecidableLE α] [LawfulOrderLeftLeaningMax α]
@@ -458,7 +458,7 @@ protected theorem max_map_eq_max [Max α] [LE α] [DecidableLE α] [LawfulOrderL
 protected theorem maxOn_replicate [LE β] [DecidableLE β] [IsLinearPreorder β]
     {n : Nat} {a : α} {f : α → β} (h : replicate n a ≠ []) :
     (replicate n a).maxOn f h = a :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.minOn_replicate (f := f) h
 
 /-! # minOn? -/
@@ -579,7 +579,7 @@ protected theorem maxOn?_nil [LE β] [DecidableLE β] {f : α → β} :
 protected theorem maxOn?_cons_eq_some_maxOn
     [LE β] [DecidableLE β] {f : α → β} {x : α} {xs : List α} :
     (x :: xs).maxOn? f = some ((x :: xs).maxOn f (fun h => nomatch h)) :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.minOn?_cons_eq_some_minOn
 
 protected theorem maxOn?_cons
@@ -588,7 +588,7 @@ protected theorem maxOn?_cons
   have : maxOn f x = (letI : LE β := LE.opposite inferInstance; minOn f x) := by
     ext; simp only [maxOn_eq_minOn]
   simp only [List.maxOn?_eq_minOn?, this]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   exact List.minOn?_cons
 
 @[simp]
@@ -599,8 +599,8 @@ protected theorem maxOn?_singleton [LE β] [DecidableLE β] {x : α} {f : α →
 @[simp]
 protected theorem maxOn?_id [Max α] [LE α] [DecidableLE α] [LawfulOrderLeftLeaningMax α]
     {xs : List α} : xs.maxOn? id = xs.max? := by
-  letI : LE α := (inferInstance : LE α).opposite
-  letI : Min α := (inferInstance : Max α).oppositeMin
+  letI : LE α := (inferInstanceAs (LE α)).opposite
+  letI : Min α := (inferInstanceAs (Max α)).oppositeMin
   simpa only [List.maxOn?_eq_minOn?, List.max?_eq_min?] using List.minOn?_id (α := α)
 
 protected theorem maxOn?_eq_if
@@ -610,7 +610,7 @@ protected theorem maxOn?_eq_if
       some (xs.maxOn f h)
     else
       none :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.minOn?_eq_if
 
 @[simp]
@@ -620,55 +620,55 @@ protected theorem isSome_maxOn?_iff [LE β] [DecidableLE β] {f : α → β} {xs
 
 protected theorem maxOn_eq_get_maxOn? [LE β] [DecidableLE β] {f : α → β} {xs : List α}
     (h : xs ≠ []) : xs.maxOn f h = (xs.maxOn? f).get (List.isSome_maxOn?_iff.mpr h) :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.minOn_eq_get_minOn? (f := f) h
 
 protected theorem maxOn?_eq_some_maxOn [LE β] [DecidableLE β] {f : α → β} {xs : List α}
     (h : xs ≠ []) : xs.maxOn? f = some (xs.maxOn f h) :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.minOn?_eq_some_minOn (f := f) h
 
 @[simp]
 protected theorem get_maxOn? [LE β] [DecidableLE β] {f : α → β} {xs : List α}
     (h : xs ≠ []) : (xs.maxOn? f).get (List.isSome_maxOn?_iff.mpr h) = xs.maxOn f h :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.get_minOn? (f := f) h
 
 protected theorem maxOn_eq_of_maxOn?_eq_some
     [LE β] [DecidableLE β] {f : α → β} {xs : List α} {x : α} (h : xs.maxOn? f = some x) :
     xs.maxOn f (List.isSome_maxOn?_iff.mp (Option.isSome_of_eq_some h)) = x :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.minOn_eq_of_minOn?_eq_some (f := f) h
 
 protected theorem isSome_maxOn?_of_mem
     [LE β] [DecidableLE β] {f : α → β} {xs : List α} {x : α} (h : x ∈ xs) :
     (xs.maxOn? f).isSome :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.isSome_minOn?_of_mem (f := f) h
 
 protected theorem le_apply_get_maxOn?_of_mem
     [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β} {xs : List α} {x : α} (h : x ∈ xs) :
     f x ≤ f ((xs.maxOn? f).get (List.isSome_maxOn?_of_mem h)) := by
   simp only [List.maxOn?_eq_minOn?]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa [LE.le_opposite_iff] using List.apply_get_minOn?_le_of_mem (f := f) h
 
 protected theorem maxOn?_mem [LE β] [DecidableLE β] {xs : List α}
     {f : α → β} (h : xs.maxOn? f = some a) : a ∈ xs :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.minOn?_mem (f := f) h
 
 protected theorem maxOn?_replicate [LE β] [DecidableLE β] [IsLinearPreorder β]
     {n : Nat} {a : α} {f : α → β} :
     (replicate n a).maxOn? f = if n = 0 then none else some a :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.minOn?_replicate
 
 @[simp]
 protected theorem maxOn?_replicate_of_pos [LE β] [DecidableLE β] [IsLinearPreorder β]
     {n : Nat} {a : α} {f : α → β} (h : 0 < n) :
     (replicate n a).maxOn? f = some a :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.minOn?_replicate_of_pos (f := f) h
 
 @[simp]
@@ -678,7 +678,7 @@ protected theorem maxOn?_append [LE β] [DecidableLE β] [IsLinearPreorder β]
   have : maxOn f = (letI : LE β := LE.opposite inferInstance; minOn f) := by
     ext; simp only [maxOn_eq_minOn]
   simp only [List.maxOn?_eq_minOn?, this]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   exact List.minOn?_append xs ys f
 
 end List

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 b (n.digitChar :: cs) init = ofDigitChars b cs (b * init + n) := by
+    ofDigitChars 10 (n.digitChar :: cs) init = ofDigitChars 10 cs (10 * 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,17 +320,15 @@ 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]
 
-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 (by omega : m < 10)]
-  | digit m k hk hm ih =>
-    rw [← Nat.toDigits_append_toDigits hb' hm hk,
-      ofDigitChars_append, ih, Nat.toDigits_of_lt_base hk,
-      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)
+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
+  | single m hm =>
+    simp [Nat.toDigits_of_lt_base hm, ofDigitChars_cons_digitChar_of_lt_ten hm]
+  | digit m k hk hm ih =>
+    rw [← Nat.toDigits_append_toDigits this hm hk,
+      ofDigitChars_append, ih, Nat.toDigits_of_lt_base hk,
+      ofDigitChars_cons_digitChar_of_lt_ten hk, ofDigitChars_nil]
 
 end Nat

src/Init/Data/Order/MinMaxOn.lean

@@ -39,8 +39,8 @@ public theorem minOn_id [Min α] [LE α] [DecidableLE α] [LawfulOrderLeftLeanin
 
 public theorem maxOn_id [Max α] [LE α] [DecidableLE α] [LawfulOrderLeftLeaningMax α] {x y : α} :
     maxOn id x y = max x y := by
-  letI : LE α := (inferInstance : LE α).opposite
-  letI : Min α := (inferInstance : Max α).oppositeMin
+  letI : LE α := (inferInstanceAs (LE α)).opposite
+  letI : Min α := (inferInstanceAs (Max α)).oppositeMin
   simp [maxOn, minOn_id, Max.min_oppositeMin, this]
 
 public theorem minOn_eq_or [LE β] [DecidableLE β] {f : α → β} {x y : α} :
@@ -168,32 +168,32 @@ public theorem maxOn_eq_right_of_lt
     [LE β] [DecidableLE β] [LT β] [Total (α := β) (· ≤ ·)] [LawfulOrderLT β]
     {f : α → β} {x y : α} (h : f x < f y) :
     maxOn f x y = y :=
-  letI : LE β := (inferInstance : LE β).opposite
-  letI : LT β := (inferInstance : LT β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LT β := (inferInstanceAs (LT β)).opposite
   minOn_eq_right_of_lt (h := by simpa [LT.lt_opposite_iff] using h) ..
 
 public theorem left_le_apply_maxOn [le : LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β}
     {x y : α} : f x ≤ f (maxOn f x y) := by
   rw [maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa only [LE.le_opposite_iff] using apply_minOn_le_left (f := f) ..
 
 public theorem right_le_apply_maxOn [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β}
     {x y : α} : f y ≤ f (maxOn f x y) := by
   rw [maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa only [LE.le_opposite_iff] using apply_minOn_le_right (f := f)
 
 public theorem apply_maxOn_le_iff [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β}
     {x y : α} {b : β} :
     f (maxOn f x y) ≤ b ↔ f x ≤ b ∧ f y ≤ b := by
   rw [maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa only [LE.le_opposite_iff] using le_apply_minOn_iff (f := f)
 
 public theorem maxOn_assoc [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β}
     {x y z : α} : maxOn f (maxOn f x y) z = maxOn f x (maxOn f y z) :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   minOn_assoc (f := f)
 
 public instance [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β} :
@@ -203,8 +203,8 @@ public instance [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β} :
 
 public theorem max_apply [LE β] [DecidableLE β] [Max β] [LawfulOrderLeftLeaningMax β]
     {f : α → β} {x y : α} : max (f x) (f y) = f (maxOn f x y) := by
-  letI : LE β := (inferInstance : LE β).opposite
-  letI : Min β := (inferInstance : Max β).oppositeMin
+  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : Min β := (inferInstanceAs (Max β)).oppositeMin
   simpa [Max.min_oppositeMin] using min_apply (f := f)
 
 public theorem apply_maxOn [LE β] [DecidableLE β] [Max β] [LawfulOrderLeftLeaningMax β]

src/Init/Data/Order/Opposite.lean

@@ -44,7 +44,7 @@ def min' [LE α] [DecidableLE α] (a b : α) : α :=
 
 open scoped Std.OppositeOrderInstances in
 def max' [LE α] [DecidableLE α] (a b : α) : α :=
-  letI : LE α := (inferInstance : LE α).opposite
+  letI : LE α := (inferInstanceAs (LE α)).opposite
   -- `DecidableLE` for the opposite order is derived automatically via `OppositeOrderInstances`
   min' a b
 ```

src/Init/Data/String/Basic.lean

@@ -852,10 +852,6 @@ 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,9 +187,6 @@ 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,5 +6,29 @@ Authors: Markus Himmel
 module
 
 prelude
-public import Init.Data.String.Iter.Basic
-public import Init.Data.String.Iter.Intercalate
+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/Basic.lean

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

@@ -1,36 +0,0 @@
-/-
-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,8 +17,6 @@ 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
 import Init.Data.Order.Lemmas
 public import Init.Data.String.Basic
 import Init.Data.Char.Lemmas

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

@@ -1,25 +0,0 @@
-/-
-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,7 +10,6 @@ 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
 
@@ -43,16 +42,6 @@ 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
@@ -60,23 +49,6 @@ 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]
@@ -93,10 +65,6 @@ 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

@@ -1,50 +0,0 @@
-/-
-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,7 +23,6 @@ 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
 
@@ -71,11 +70,6 @@ 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
@@ -84,9 +78,4 @@ 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/Slice.lean

@@ -33,22 +33,8 @@ 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) :=
-  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])
+theorem beq_eq_decide {s t : Slice} : (s == t) = decide (s.copy = t.copy) := by
+  cases h : s == t <;> simp_all
 
 end BEq
 

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.Basic
+public import Init.Data.String.Iter
 public import Init.Data.String.Iterate
 import Init.Data.Iterators.Consumers.Collect
 import Init.Data.Iterators.Consumers.Loop
@@ -84,11 +84,10 @@ instance : ToString String.Slice where
 theorem toStringToString_eq : ToString.toString = String.Slice.copy := (rfl)
 
 @[extern "lean_slice_hash"]
-protected def hash (s : @& Slice) : UInt64 :=
-  String.hash s.copy
+opaque hash (s : @& Slice) : UInt64
 
 instance : Hashable Slice where
-  hash := Slice.hash
+  hash := hash
 
 instance : LT Slice where
   lt x y := x.copy < y.copy
@@ -1152,19 +1151,6 @@ 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/Config.lean

@@ -111,10 +111,11 @@ structure Config where
   ring := true
   /--
   Maximum number of steps performed by the `ring` solver.
-  A step is counted whenever one polynomial is used to simplify another,
-  weighted by the number of terms in the resulting polynomial.
+  A step is counted whenever one polynomial is used to simplify another.
+  For example, given `x^2 + 1` and `x^2 * y^3 + x * y`, the first can be
+  used to simplify the second to `-1 * y^3 + x * y`.
   -/
-  ringSteps := 100000
+  ringSteps := 10000
   /--
   When `true` (default: `true`), uses procedure for handling linear arithmetic for `IntModule`, and
   `CommRing`.

src/Init/Grind/Interactive.lean

@@ -107,9 +107,6 @@ 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
@@ -208,7 +205,7 @@ macro:1 x:grind tk:" <;> " y:grind:2 : grind => `(grind|
     with_annotate_state $tk skip
     all_goals $y:grind)
 
-/-- `first (tac) ...` runs each `tac` until one succeeds, or else fails. -/
+/-- `first | tac | ...` runs each `tac` until one succeeds, or else fails. -/
 syntax (name := first) "first " withPosition((ppDedent(ppLine) colGe "(" grindSeq ")")+) : grind
 
 /-- `try tac` runs `tac` and succeeds even if `tac` failed. -/
@@ -307,19 +304,5 @@ syntax (name := symInternalizeAll) "internalize_all" : grind
 Only available in `sym =>` mode. -/
 syntax (name := symByContra) "by_contra" : grind
 
-/--
-`simp` applies the structural simplifier to the goal target.
-Only available in `sym =>` mode.
-
-- `simp` — uses the default (identity) variant
-- `simp myVariant` — uses a named variant registered via `register_sym_simp`
-- `simp [thm₁, thm₂, ...]` — default variant with extra rewrite theorems appended to `post`
-- `simp myVariant [thm₁, thm₂, ...]` — named variant with extra theorems
--/
-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/Internal/Order/Basic.lean

@@ -954,7 +954,7 @@ theorem monotone_readerTRun [PartialOrder γ]
 instance [inst : PartialOrder (m α)] : PartialOrder (StateRefT' ω σ m α) := instOrderPi
 instance [inst : CCPO (m α)] : CCPO (StateRefT' ω σ m α) := instCCPOPi
 instance [Monad m] [∀ α, PartialOrder (m α)] [MonoBind m] : MonoBind (StateRefT' ω σ m) :=
-  inferInstanceAs (MonoBind (ReaderT (ST.Ref ω σ) m))
+  inferInstanceAs (MonoBind (ReaderT _ _))
 
 @[partial_fixpoint_monotone]
 theorem monotone_stateRefT'Run [PartialOrder γ]

src/Init/Prelude.lean

@@ -185,17 +185,18 @@ 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 a value of any target type by typeclass
+inference. This is just like `inferInstance` except that `α` is given
+explicitly instead of being inferred from the target type. It is especially
+useful when the target type is some `α'` which is definitionally equal to `α`,
+but the instance we are looking for is only registered for `α` (because
+typeclass search does not unfold most definitions, but definitional equality
+does.) Example:
 ```
 #check inferInstanceAs (Inhabited Nat) -- Inhabited Nat
 ```
 -/
-abbrev «inferInstanceAs» (α : Sort u) [i : α] : α := i
+abbrev inferInstanceAs (α : Sort u) [i : α] : α := i
 
 
 
@@ -4082,7 +4083,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) :=
-  (a : @&ρ) → m α
+  ρ → m α
 
 /--
 Interpret `ρ → m α` as an element of `ReaderT ρ m α`.

src/Init/Sym.lean

@@ -6,4 +6,3 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Init.Sym.Lemmas
-public import Init.Sym.Simp.SimprocDSL

src/Init/Sym/Simp/SimprocDSL.lean

@@ -1,137 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Init.Tactics
-public section
-namespace Lean.Parser.Sym.Simp
-
-/-!
-# Simproc and Discharger DSLs for `Sym.simp`
-
-## Simproc DSL (`sym_simproc`)
-
-A syntax category for specifying `pre` and `post` simproc chains in `Sym.simp` variants.
-
-### Primitives
-- `ground` — evaluates ground (fully concrete) terms
-- `telescope` — simplifies telescope binders (have-values, arrow hypotheses) but not the final body
-- `rewrite setName [with discharger]` — rewrites using a named theorem set
-- `rewrite [thm₁, thm₂, ...] [with discharger]` — rewrites using inline theorems
-- `self` — recursive simplification (calls the full simplifier)
-- `none` — identity (no simplification)
-
-### Combinators
-- `a >> b` — apply `a`, then apply `b` to the result (andThen)
-- `a <|> b` — try `a`, if no progress try `b` (orElse)
-
-## Discharger DSL (`sym_discharger`)
-
-A syntax category for specifying dischargers used in the `with` clause of `rewrite`.
-Dischargers attempt to prove side conditions of conditional rewrite rules.
-
-### Primitives
-- `self` — recursive simplifier discharge (`dischargeSimpSelf`)
-- `none` — no discharge, only unconditional rewrites apply (`dischargeNone`)
--/
-
-declare_syntax_cat sym_simproc (behavior := both)
-declare_syntax_cat sym_discharger (behavior := both)
-
--- Simproc primitives
-
-/-- Evaluate ground (fully concrete) terms. -/
-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
-
-/-- Rewrite using inline theorems. Optionally specify a discharger for conditional rewrites. -/
-syntax (name := rewriteInline) "rewrite" " [" ident,* "]" (" with " sym_discharger)? : sym_simproc
-
-/-- Recursive simplification (calls the full simplifier). -/
-syntax (name := self) "self" : sym_simproc
-
-/-- Identity simproc (no simplification). -/
-syntax (name := none) "none" : sym_simproc
-
--- Simproc combinators
-
-/-- Apply `a`, then apply `b` to the result. -/
-syntax:60 (name := andThen) sym_simproc:61 " >> " sym_simproc:60 : sym_simproc
-
-/-- Try `a`, if no progress try `b`. -/
-syntax:20 (name := orElse) sym_simproc:21 " <|> " sym_simproc:20 : sym_simproc
-
-/-- Parenthesized simproc expression. -/
-syntax (name := simprocParen) "(" sym_simproc ")" : sym_simproc
-
--- Discharger primitives
-
-/-- Recursive simplifier discharge. Calls the full simplifier to prove side conditions. -/
-syntax (name := dischSelf) "self" : sym_discharger
-
-/-- No discharge. Only unconditional rewrites will apply. -/
-syntax (name := dischNone) "none" : sym_discharger
-
-/-- Parenthesized discharger expression. -/
-syntax (name := dischParen) "(" sym_discharger ")" : sym_discharger
-
-end Lean.Parser.Sym.Simp
-
-/-!
-## `register_sym_simp` command
-
-Declares a named `Sym.simp` variant with `pre`/`post` simproc chains and optional config overrides.
-
-```
-register_sym_simp myVariant where
-  pre  := telescope
-  post := ground >> rewrite mySet with self
-```
--/
-
-namespace Lean.Parser.Command
-
-declare_syntax_cat sym_simp_field (behavior := both)
-
-/-- Pre-processing simproc chain. -/
-syntax (name := symSimpFieldPre) "pre" " := " sym_simproc : sym_simp_field
-
-/-- Post-processing simproc chain. -/
-syntax (name := symSimpFieldPost) "post" " := " sym_simproc : sym_simp_field
-
-/-- Maximum number of simplification steps. -/
-syntax (name := symSimpFieldMaxSteps) "maxSteps" " := " num : sym_simp_field
-
-/-- Maximum depth of recursive discharge attempts. -/
-syntax (name := symSimpFieldMaxDischargeDepth) "maxDischargeDepth" " := " num : sym_simp_field
-
-/--
-Register a named `Sym.simp` variant.
-
-```
-register_sym_simp myVariant where
-  pre  := telescope
-  post := ground >> rewrite [thm1, thm2] with self
-  maxSteps := 50000
-```
--/
-syntax (name := registerSymSimp) "register_sym_simp" ident "where"
-  (colGt sym_simp_field)* : command
-
-end Lean.Parser.Command

src/Init/Tactics.lean

@@ -524,6 +524,9 @@ syntax location := withPosition(ppGroup(" at" (locationWildcard <|> locationHyp)
 -/
 syntax (name := change) "change " term (location)? : tactic
 
+@[tactic_alt change]
+syntax (name := changeWith) "change " term " with " term (location)? : tactic
+
 /--
 `show t` finds the first goal whose target unifies with `t`. It makes that the main goal,
 performs the unification, and replaces the target with the unified version of `t`.

src/Lean/Compiler/IR/AddExtern.lean

@@ -21,7 +21,6 @@ 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

@@ -136,11 +136,12 @@ def findEnvDecl (env : Environment) (declName : Name) : Option Decl :=
   Compiler.LCNF.findExtEntry? env declMapExt declName findAtSorted? (·.2.find?)
 
 @[export lean_ir_find_env_decl]
-private def findInterpDecl (env : Environment) (declName : Name) : Option Decl :=
+private def findInterpDecl (env : Environment) (declName : Name) (includeServer := false) : Option Decl :=
   -- This function is never used in `leanir`, so no need for `findExtEntry?`
   match env.getModuleIdxFor? declName with
   | some modIdx =>
-    -- `meta import/import all` and additional server-mode IR
+    -- `meta import/import all` and, optionally, additional server-mode IR
+    guard (includeServer || env.header.modules[modIdx]?.any (·.irPhases != .runtime)) *>
     findAtSorted? (declMapExt.getModuleIREntries env modIdx) declName <|>
     -- (closure of) `meta def`; will report `.extern`s for other `def`s so needs to come second
     findAtSorted? (declMapExt.getModuleEntries env modIdx) declName

src/Lean/Compiler/InitAttr.lean

@@ -171,7 +171,7 @@ private unsafe def runInitAttrs (env : Environment) (opts : Options) : IO Unit :
     -- libraries with their corresponding module in the Environment) must
     -- first be initialized
     let pkg? := env.getModulePackageByIdx? modIdx
-    if env.header.isModule then
+    if env.header.isModule && /- TODO: remove after reboostrap -/ false then
       let initializedRuntime ← pure initRuntime <&&> runModInit (phases := .runtime) mod.module pkg?
       let initializedComptime ← runModInit (phases := .comptime) mod.module pkg?
       if initializedRuntime || initializedComptime then

src/Lean/Compiler/LCNF/CompilerM.lean

@@ -49,7 +49,7 @@ structure CompilerM.Context where
 abbrev CompilerM := ReaderT CompilerM.Context $ StateRefT CompilerM.State CoreM
 
 @[always_inline]
-instance : Monad CompilerM := let i : Monad CompilerM := inferInstance; { pure := i.pure, bind := i.bind }
+instance : Monad CompilerM := let i := inferInstanceAs (Monad CompilerM); { pure := i.pure, bind := i.bind }
 
 @[inline] def withPhase (phase : Phase) (x : CompilerM α) : CompilerM α :=
   withReader (fun ctx => { ctx with phase }) x

src/Lean/Compiler/LCNF/ExplicitRC.lean

@@ -97,7 +97,6 @@ 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

src/Lean/Compiler/LCNF/InferBorrow.lean

@@ -213,8 +213,6 @@ 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
@@ -231,7 +229,6 @@ 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
@@ -243,19 +240,13 @@ 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 ..
-  -- 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
+  | .jpArgPropagation .. => 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 ..
-  | .ownedAnnotation => true
+  | .forwardProjectionProp .. | .backwardProjectionProp .. => true
 
 /--
 Infer the borrowing annotations in a SCC through dataflow analysis.
@@ -265,19 +256,10 @@ 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 }
-      loop
+      go
     else
       return ()
 
@@ -379,16 +361,6 @@ 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)

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 => throwError "getOtherDeclType unsupported for impure"
+  | .impure => getOtherDeclImpureType declName
 
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/PrettyPrinter.lean

@@ -154,18 +154,16 @@ 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 check persistent k _ =>
-      let ann := (if persistent then "[persistent]" else "") ++ (if !check then "[ref]" else "")
+    | .inc fvarId n _ _ k _ =>
       if n != 1 then
-        return f!"inc[{n}]{ann} {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
+        return f!"inc[{n}] {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
       else
-        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 "")
+        return f!"inc {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
+    | .dec fvarId n _ _ k _ =>
       if n != 1 then
-        return f!"dec[{n}]{ann} {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
+        return f!"dec[{n}] {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
       else
-        return f!"dec{ann} {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
+        return f!"dec {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
     | .del fvarId k _ =>
       return f!"del {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
 

src/Lean/Compiler/LCNF/PropagateBorrow.lean

@@ -105,22 +105,9 @@ where
 
   collectLetValue (z : FVarId) (v : LetValue .impure) : InferM Unit := do
     match v with
-    | .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
+    | .oproj _ x _ =>
+      let xVal ← getOwnedness x
+      join z xVal
     | .ctor .. | .fap .. | .fvar .. | .pap .. | .sproj .. | .uproj .. | .erased .. | .lit .. =>
       join z .own
     | _ => unreachable!

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

@@ -78,7 +78,7 @@ structure State where
 abbrev SimpM := ReaderT Context $ StateRefT State DiscrM
 
 @[always_inline]
-instance : Monad SimpM := let i : Monad SimpM := inferInstance; { pure := i.pure, bind := i.bind }
+instance : Monad SimpM := let i := inferInstanceAs (Monad SimpM); { pure := i.pure, bind := i.bind }
 
 instance : MonadFVarSubst SimpM .pure false where
   getSubst := return (← get).subst

src/Lean/Compiler/LCNF/ToImpureType.lean

@@ -240,4 +240,12 @@ 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

@@ -256,7 +256,7 @@ abbrev CoreM := ReaderT Context <| StateRefT State (EIO Exception)
 -- Make the compiler generate specialized `pure`/`bind` so we do not have to optimize through the
 -- whole monad stack at every use site. May eventually be covered by `deriving`.
 @[always_inline]
-instance : Monad CoreM := let i : Monad CoreM := inferInstance; { pure := i.pure, bind := i.bind }
+instance : Monad CoreM := let i := inferInstanceAs (Monad CoreM); { pure := i.pure, bind := i.bind }
 
 instance : Inhabited (CoreM α) where
   default := fun _ _ => throw default
@@ -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) (allowOpaque := false) : CoreM Expr := do
+def instantiateValueLevelParams (c : ConstantInfo) (us : List Level) : CoreM Expr := do
   if let some (us', r) := (← get).cache.instLevelValue.find? c.name then
     if us == us' then
       return r
-  unless c.hasValue (allowOpaque := allowOpaque) do
+  unless c.hasValue do
     throwError "Not a definition or theorem: {.ofConstName c.name}"
-  let r := c.instantiateValueLevelParams! us (allowOpaque := allowOpaque)
+  let r := c.instantiateValueLevelParams! us
   modifyInstLevelValueCache fun s => s.insert c.name (us, r)
   return r
 

src/Lean/Declaration.lean

@@ -14,35 +14,29 @@ public section
 
 namespace Lean
 /--
-Reducibility hints guide the kernel's *lazy delta reduction* strategy. When the kernel encounters a
-definitional equality constraint
+Reducibility hints are used in the convertibility checker.
+When trying to solve a constraint such a
 
            (f ...) =?= (g ...)
 
-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:
+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.
 
-* 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 arguments of the `regular` Constructor are: the definitional height and the flag `selfOpt`.
 
-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.
+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 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 hint only affects performance. None of the hints prevent the kernel from unfolding a
+declaration during Type checking.
 
-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. -/
+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. -/
 inductive ReducibilityHints where
   | opaque  : ReducibilityHints
   | abbrev  : ReducibilityHints
@@ -475,37 +469,24 @@ 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, ..}   => if allowOpaque then some value else none
+  | .thmInfo  {value, ..}   => some value
   | .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  _   => allowOpaque
+  | .thmInfo  _   => true
   | .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, ..}   => if allowOpaque then value else panic! "declaration with value expected"
+  | .thmInfo  {value, ..}   => value
   | .opaqueInfo {value, ..} => if allowOpaque then value else panic! "declaration with value expected"
   | _                       => panic! s!"declaration with value expected, but {info.name} has none"
 
@@ -529,10 +510,6 @@ 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? (allowOpaque := true) then
+      if let some value := info.value? then
         isRflProofCore info.type value
       else
         pure false

src/Lean/Elab/BuiltinTerm.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Lean.Meta.Diagnostics
-public import Lean.Meta.InstanceNormalForm
 public import Lean.Elab.Open
 public import Lean.Elab.SetOption
 public import Lean.Elab.Eval
@@ -314,34 +313,6 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
     return val
   | _ => panic! "resolveId? returned an unexpected expression"
 
-@[builtin_term_elab Lean.Parser.Term.inferInstanceAs] def elabInferInstanceAs : TermElab := fun stx expectedType? => do
-  -- 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
-  let type ← instantiateMVars type
-  -- Rebuild type with fresh synthetic mvars for instance-implicit args, so that
-  -- synthesis is not influenced by the expected type's instance choices.
-  let type ← abstractInstImplicitArgs type
-  let inst ← synthInstance type
-  let inst ← if backward.inferInstanceAs.wrap.get (← getOptions) then
-    -- Normalize to instance normal form.
-    let logCompileErrors := !(← read).isNoncomputableSection && !(← read).declName?.any (Lean.isNoncomputable (← getEnv))
-    let isMeta := (← read).declName?.any (isMarkedMeta (← getEnv))
-    withNewMCtxDepth <| normalizeInstance inst expectedType (logCompileErrors := logCompileErrors) (isMeta := isMeta)
-  else
-    pure inst
-  ensureHasType expectedType? inst
-
 @[builtin_term_elab clear] def elabClear : TermElab := fun stx expectedType? => do
   let some (.fvar fvarId) ← isLocalIdent? stx[1]
     | throwErrorAt stx[1] "not in scope"
@@ -412,13 +383,14 @@ private opaque evalFilePath (stx : Syntax) : TermElabM System.FilePath
       let name ← mkAuxDeclName `_private
       withoutExporting do
         let e ← elabTermAndSynthesize e expectedType?
+        let compile := !(← read).isNoncomputableSection && !(← read).declName?.any (Lean.isNoncomputable (← getEnv))
         let e ← mkAuxDefinitionFor (compile := false) name e
-        -- Inline as changing visibility should not affect run time.
-        setInlineAttribute name
-        if (← read).declName?.any (isMarkedMeta (← getEnv)) then
-          modifyEnv (markMeta · name)
-        let logCompileErrors := !(← read).isNoncomputableSection && !(← read).declName?.any (Lean.isNoncomputable (← getEnv))
-        compileDecls (logErrors := logCompileErrors) #[name]
+        if compile then
+          -- Inline as changing visibility should not affect run time.
+          setInlineAttribute name
+          if (← read).declName?.any (isMarkedMeta (← getEnv)) then
+            modifyEnv (markMeta · name)
+          compileDecls #[name]
         return e
     else
       elabTerm e expectedType?

src/Lean/Elab/Command.lean

@@ -71,7 +71,7 @@ whole monad stack at every use site. May eventually be covered by `deriving`.
 Remark: see comment at TermElabM
 -/
 @[always_inline]
-instance : Monad CommandElabM := let i : Monad CommandElabM := inferInstance; { pure := i.pure, bind := i.bind }
+instance : Monad CommandElabM := let i := inferInstanceAs (Monad CommandElabM); { pure := i.pure, bind := i.bind }
 
 /--
 Like `Core.tryCatchRuntimeEx`; runtime errors are generally used to abort term elaboration, so we do
@@ -666,8 +666,7 @@ private def mkTermContext (ctx : Context) (s : State) : CommandElabM Term.Contex
   return {
     macroStack             := ctx.macroStack
     sectionVars            := sectionVars
-    isNoncomputableSection := scope.isNoncomputable
-    isMetaSection          := scope.isMeta }
+    isNoncomputableSection := scope.isNoncomputable }
 
 /--
 Lift the `TermElabM` monadic action `x` into a `CommandElabM` monadic action.

src/Lean/Elab/Deriving/Basic.lean

@@ -9,7 +9,6 @@ prelude
 public import Lean.Elab.App
 public import Lean.Elab.DeclNameGen
 import Lean.Compiler.NoncomputableAttr
-import Lean.Meta.InstanceNormalForm
 
 public section
 
@@ -188,7 +187,7 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) (isNoncomputable
   let ConstantInfo.defnInfo info ← getConstInfo declName
     | throwError "Failed to delta derive instance, `{.ofConstName declName}` is not a definition."
   let value := info.value.beta decl.getAppArgs
-  let (result, preNormValue, instName) : Closure.MkValueTypeClosureResult × Expr × Name ←
+  let result : Closure.MkValueTypeClosureResult ←
     -- Assumption: users intend delta deriving to apply to the body of a definition, even if in the source code
     -- the function is written as a lambda expression.
     -- Furthermore, we don't use `forallTelescope` because users want to derive instances for monads.
@@ -211,34 +210,22 @@ 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.
-            let preNormClosure ← Closure.mkValueTypeClosure result.instType result.instVal (zetaDelta := true)
-            -- Compute instance name early so `normalizeInstance` 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
-                  (logCompileErrors := false)  -- covered by noncomputable check below
-                  (isMeta := isMeta)
-            else
-              pure result.instVal
-            let closure ← Closure.mkValueTypeClosure result.instType inst (zetaDelta := true)
-            return (closure, preNormClosure.value, instName)
+            Closure.mkValueTypeClosure result.instType result.instVal (zetaDelta := true)
         finally
           Core.setMessageLog (msgLog ++ (← Core.getMessageLog))
   let env ← getEnv
+  let mut instName := (← getCurrNamespace) ++ (← NameGen.mkBaseNameWithSuffix "inst" result.type)
+  -- We don't have a facility to let users override derived names, so make an unused name if needed.
+  instName ← liftMacroM <| mkUnusedBaseName instName
+  -- Make the instance private if the declaration is private.
+  if isPrivateName declName then
+    instName := mkPrivateName env instName
   let hints := ReducibilityHints.regular (getMaxHeight env result.value + 1)
   let decl ← mkDefinitionValInferringUnsafe instName result.levelParams.toList result.type result.value hints
   -- Pre-check: if the instance value depends on noncomputable definitions and the user didn't write
   -- `noncomputable`, give an actionable error with a `Try this:` suggestion.
   unless isNoncomputable || (← read).isNoncomputableSection || (← isProp result.type) do
-    let noncompRef? := preNormValue.foldConsts none fun n acc =>
+    let noncompRef? := result.value.foldConsts none fun n acc =>
       acc <|> if Lean.isNoncomputable (asyncMode := .local) env n then some n else none
     if let some noncompRef := noncompRef? then
       if let some cmdRef := cmdRef? then

src/Lean/Elab/PreDefinition/Basic.lean

@@ -10,7 +10,6 @@ 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.Elab.DefView
 public section
 

src/Lean/Elab/PreDefinition/Mutual.lean

@@ -63,11 +63,10 @@ def addPreDefAttributes (preDefs : Array PreDefinition) : TermElabM Unit := do
   a wrong setting and creates bad `defEq` equations.
   -/
   for preDef in preDefs do
-    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
+    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,7 +184,6 @@ 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,32 +80,6 @@ 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/Basic.lean

@@ -63,7 +63,7 @@ See comment at `Monad TermElabM`
 -/
 @[always_inline]
 instance : Monad TacticM :=
-  let i : Monad TacticM := inferInstance;
+  let i := inferInstanceAs (Monad TacticM);
   { pure := i.pure, bind := i.bind }
 
 instance : Inhabited (TacticM α) where

src/Lean/Elab/Tactic/Decide.lean

@@ -155,7 +155,7 @@ where
         .hint' m!"Reduction got stuck on `▸` ({.ofConstName ``Eq.rec}), \
           which suggests that one of the `{.ofConstName ``Decidable}` instances is defined using tactics such as `rw` or `simp`. \
           To avoid tactics, make use of functions such as \
-          `{.ofConstName `inferInstanceAs}` or `{.ofConstName ``decidable_of_decidable_of_iff}` \
+          `{.ofConstName ``inferInstanceAs}` or `{.ofConstName ``decidable_of_decidable_of_iff}` \
           to alter a proposition."
       else if reason.isAppOf ``Classical.choice then
         .hint' m!"Reduction got stuck on `{.ofConstName ``Classical.choice}`, \

src/Lean/Elab/Tactic/Grind.lean

@@ -16,6 +16,3 @@ public import Lean.Elab.Tactic.Grind.Lint
 public import Lean.Elab.Tactic.Grind.LintExceptions
 public import Lean.Elab.Tactic.Grind.Annotated
 public import Lean.Elab.Tactic.Grind.Sym
-public import Lean.Elab.Tactic.Grind.SimprocDSL
-public import Lean.Elab.Tactic.Grind.SimprocDSLBuiltin
-public import Lean.Elab.Tactic.Grind.RegisterSymSimp

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

@@ -10,7 +10,6 @@ public import Lean.Meta.Tactic.Grind.Main
 import Lean.Meta.Tactic.Grind.Intro
 public import Lean.Meta.Sym.Apply
 public import Lean.Meta.Sym.Util
-public import Lean.Meta.Sym.Simp.SimpM
 import Init.Omega
 public section
 namespace Lean.Elab.Tactic.Grind
@@ -25,25 +24,11 @@ structure Context extends Tactic.Context where
 
 open Meta.Grind (Goal)
 
-/-- An extra theorem passed to `simp` in `sym =>` mode. -/
-inductive ExtraTheorem where
-  | const (declName : Name)
-  | fvar  (fvarId : FVarId)
-  deriving BEq, Hashable
-
-/-- Cache key for `Sym.simp` variant invocations. -/
-structure SimpCacheKey where
-  variant : Name
-  extras  : Array ExtraTheorem
-  deriving BEq, Hashable
-
 structure Cache where
   /-- Cache for `BackwardRule`s created from declaration names (sym mode only). -/
   backwardRuleName : PHashMap Name Sym.BackwardRule := {}
   /-- Cache for `BackwardRule`s created from elaborated terms, keyed by syntax byte position range (sym mode only). -/
   backwardRuleSyntax : PHashMap (Nat × Nat) Sym.BackwardRule := {}
-  /-- Per-variant persistent `Sym.simp` cache. Keyed by variant name + extra theorem names. -/
-  simpState : Std.HashMap SimpCacheKey Sym.Simp.State := {}
 
 structure State where
   symState   : Meta.Sym.State
@@ -89,7 +74,7 @@ def SavedState.restore (b : SavedState) (restoreInfo := false) : GrindTacticM Un
 
 @[always_inline]
 instance : Monad GrindTacticM :=
-  let i : Monad GrindTacticM := inferInstance
+  let i := inferInstanceAs (Monad GrindTacticM)
   { pure := i.pure, bind := i.bind }
 
 instance : Inhabited (GrindTacticM α) where

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

@@ -76,10 +76,6 @@ 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/RegisterSymSimp.lean

@@ -1,73 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-import Init.Sym.Simp.SimprocDSL
-import Lean.Meta.Sym.Simp.Variant
-import Lean.Elab.Tactic.Grind.SimprocDSL
-import Lean.Elab.Command
-namespace Lean.Elab.Command
-open Meta Sym.Simp
-
-/--
-Runs a `GrindTacticM` computation in a minimal context for validation.
--/
-def withGrindTacticM (k : Tactic.Grind.GrindTacticM α) : CommandElabM α := do
-  liftTermElabM do
-  let params ← Grind.mkDefaultParams {}
-  let (ctx, state) ← Grind.GrindM.run (params := params) do
-    let methods ← Grind.getMethods
-    let grindCtx ← readThe Meta.Grind.Context
-    let symCtx ← readThe Sym.Context
-    let grindState ← get
-    let symState ← getThe Sym.State
-    let ctx := {
-      elaborator := `registerSymSimp,
-      ctx := grindCtx, sctx := symCtx, methods, params
-    }
-    return (ctx, { grindState, symState, goals := [] })
-  let (a, _) ← Tactic.Grind.GrindTacticM.run k ctx state
-  return a
-
-def validateOptionSimprocSyntax (proc? : Option Syntax) : CommandElabM Unit := do
-  let some proc := proc? | return ()
-  discard <| withGrindTacticM <| Tactic.Grind.elabSymSimproc proc
-
-@[builtin_command_elab Lean.Parser.Command.registerSymSimp]
-def elabRegisterSymSimp : CommandElab := fun stx => do
-  let id := stx[1]
-  let name := id.getId
-  -- Check for duplicate variant
-  if (getSymSimpVariant? (← getEnv) name).isSome then
-    throwErrorAt id "Sym.simp variant `{name}` is already registered"
-  let fields := stx[3].getArgs
-  let mut pre? : Option Syntax := none
-  let mut post? : Option Syntax := none
-  let mut maxSteps? : Option Nat := none
-  let mut maxDischargeDepth? : Option Nat := none
-  for field in fields do
-    match field with
-    | `(sym_simp_field| maxSteps := $val:num) =>
-      unless maxSteps?.isNone do throwErrorAt field "duplicate `maxSteps` field"
-      maxSteps? := some val.getNat
-    | `(sym_simp_field| maxDischargeDepth := $val:num) =>
-      unless maxDischargeDepth?.isNone do throwErrorAt field "duplicate `maxDischargeDepth` field"
-      maxDischargeDepth? := some val.getNat
-    | `(sym_simp_field| pre := $proc) =>
-      unless pre?.isNone do throwErrorAt field "duplicate `pre` field"
-      pre? := some proc
-    | `(sym_simp_field| post := $proc) =>
-      unless post?.isNone do throwErrorAt field "duplicate `post` field"
-      post? := some proc
-    | _ => throwErrorAt field "unexpected field"
-  -- Validate pre/post by elaborating them
-  validateOptionSimprocSyntax pre?
-  validateOptionSimprocSyntax post?
-  let config := { maxSteps := maxSteps?.getD 100_000, maxDischargeDepth := maxDischargeDepth?.getD 2 }
-  let variant : SymSimpVariant := { pre?, post?, config }
-  modifyEnv fun env => symSimpVariantExtension.addEntry env { name, variant }
-
-end Lean.Elab.Command

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

@@ -1,57 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Elab.Tactic.Grind.Basic
-public import Lean.Meta.Sym.Simp.Discharger
-import Init.Sym.Simp.SimprocDSL
-public section
-namespace Lean.Elab.Tactic.Grind
-open Meta Sym.Simp
-
-/-- Elaboration function for `sym_simproc` syntax. -/
-abbrev SymSimprocElab := Syntax → GrindTacticM Simproc
-
-/-- Elaboration function for `sym_discharger` syntax. -/
-abbrev SymDischargerElab := Syntax → GrindTacticM Discharger
-
-unsafe builtin_initialize symSimprocElabAttribute : KeyedDeclsAttribute SymSimprocElab ←
-  mkElabAttribute SymSimprocElab `builtin_sym_simproc `sym_simproc
-    `Lean.Parser.Sym.Simp `Lean.Elab.Tactic.Grind.SymSimprocElab "sym_simproc"
-
-unsafe builtin_initialize symDischargerElabAttribute : KeyedDeclsAttribute SymDischargerElab ←
-  mkElabAttribute SymDischargerElab `builtin_sym_discharger `sym_discharger
-    `Lean.Parser.Sym.Simp `Lean.Elab.Tactic.Grind.SymDischargerElab "sym_discharger"
-
-/-- Elaborate a `sym_simproc` syntax node into a `Simproc`. -/
-partial def elabSymSimproc (stx : Syntax) : GrindTacticM Simproc := do
-  let elabFns := symSimprocElabAttribute.getEntries (← getEnv) stx.getKind
-  for elabFn in elabFns do
-    try
-      return (← elabFn.value stx)
-    catch ex =>
-      match ex with
-      | .internal id _ =>
-        if id == unsupportedSyntaxExceptionId then continue
-        else throw ex
-      | _ => throw ex
-  throwErrorAt stx "unsupported sym_simproc syntax `{stx.getKind}`"
-
-/-- Elaborate a `sym_discharger` syntax node into a `Discharger`. -/
-def elabSymDischarger (stx : Syntax) : GrindTacticM Discharger := do
-  let elabFns := symDischargerElabAttribute.getEntries (← getEnv) stx.getKind
-  for elabFn in elabFns do
-    try
-      return (← elabFn.value stx)
-    catch ex =>
-      match ex with
-      | .internal id _ =>
-        if id == unsupportedSyntaxExceptionId then continue
-        else throw ex
-      | _ => throw ex
-  throwErrorAt stx "unsupported sym_discharger syntax `{stx.getKind}`"
-
-end Lean.Elab.Tactic.Grind

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

@@ -1,99 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-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
-
--- Simproc elaborators
-
-@[builtin_sym_simproc ground]
-def elabSimprocGround : SymSimprocElab := fun _ =>
-  return evalGround
-
-@[builtin_sym_simproc telescope]
-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
-
-@[builtin_sym_simproc none]
-def elabSimprocNone : SymSimprocElab := fun _ =>
-  return fun _ => return .rfl
-
-def elabOptDischarger (discharger? : Option (TSyntax `sym_discharger)) : GrindTacticM Discharger := do
-  let some discharger := discharger? | return dischargeNone
-  elabSymDischarger discharger
-
-@[builtin_sym_simproc rewriteSet]
-def elabSimprocRewriteSet : SymSimprocElab := fun stx => do
-  let `(sym_simproc| rewrite $setName:ident $[with $d?]?) := stx | throwUnsupportedSyntax
-  let some ext ← getSymSimpExtension? setName.getId
-    | throwErrorAt setName "unknown Sym.simp theorem set `{setName}`"
-  let thms ← ext.getTheorems
-  return thms.rewrite (← elabOptDischarger d?)
-
-@[builtin_sym_simproc rewriteInline]
-def elabSimprocRewriteInline : SymSimprocElab := fun stx => do
-  let `(sym_simproc| rewrite [ $[$names:ident],* ] $[with $d?]?) := stx | throwUnsupportedSyntax
-  let mut thms : Theorems := {}
-  for name in names do
-    let declName ← realizeGlobalConstNoOverload name
-    thms := thms.insert (← mkTheoremFromDecl declName)
-  return thms.rewrite (← elabOptDischarger d?)
-
-@[builtin_sym_simproc andThen]
-def elabSimprocAndThen : SymSimprocElab := fun stx => do
-  let `(sym_simproc| $left >> $right) := stx | throwUnsupportedSyntax
-  let left ← elabSymSimproc left
-  let right ← elabSymSimproc right
-  return left >> right
-
-@[builtin_sym_simproc Lean.Parser.Sym.Simp.orElse]
-def elabSimprocOrElse : SymSimprocElab := fun stx => do
-  let `(sym_simproc| $left <|> $right) := stx | throwUnsupportedSyntax
-  let left ← elabSymSimproc left
-  let right ← elabSymSimproc right
-  return left <|> right
-
-@[builtin_sym_simproc simprocParen]
-def elabSimprocParen : SymSimprocElab := fun stx => do
-  let `(sym_simproc| ( $proc) ) := stx | throwUnsupportedSyntax
-  elabSymSimproc proc
-
--- Discharger elaborators
-
-@[builtin_sym_discharger dischSelf]
-def elabDischSelf : SymDischargerElab := fun _ =>
-  return dischargeSimpSelf
-
-@[builtin_sym_discharger dischNone]
-def elabDischNone : SymDischargerElab := fun _ =>
-  return dischargeNone
-
-@[builtin_sym_discharger dischParen]
-def elabDischParen : SymDischargerElab := fun stx => do
-  let `(sym_discharger| ( $d ) ) := stx | throwUnsupportedSyntax
-  elabSymDischarger d
-
-end Lean.Elab.Tactic.Grind

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

@@ -6,15 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 import Lean.Elab.Tactic.Grind.Basic
-import Lean.Elab.Tactic.Grind.SimprocDSL
 import Lean.Meta.Sym.Grind
-import Lean.Meta.Sym.Simp.Variant
-import Lean.Meta.Sym.Simp.Rewrite
-import Lean.Meta.Sym.Simp.EvalGround
-import Lean.Meta.Sym.Simp.Goal
-import Lean.Meta.Sym.Simp.Attr
-import Lean.Meta.Sym.Simp.ControlFlow
-import Lean.Meta.Sym.Simp.Forall
 import Lean.Meta.Tactic.Apply
 import Lean.Elab.SyntheticMVars
 namespace Lean.Elab.Tactic.Grind
@@ -143,75 +135,4 @@ private def getOrCreateBackwardRuleFromTerm (term : Syntax) : GrindTacticM Sym.B
   let goal ← liftGrindM <| Grind.Goal.internalizeAll goal
   replaceMainGoal [goal]
 
-section
-open Sym.Simp
-
-def trivialSimproc : Simproc := fun _ =>
-  return .rfl
-
-def elabOptSimproc (stx? : Option Syntax) : GrindTacticM Simproc := do
-  let some stx := stx? | return trivialSimproc
-  elabSymSimproc stx
-
-def resolveExtraTheorems (ids? :  Option (Array (TSyntax `ident))) : GrindTacticM (Array ExtraTheorem × Array Theorem) := do
-  let some ids := ids? | return (#[], #[])
-  let mut extras := #[]
-  let mut thms := #[]
-  let lctx ← getLCtx
-  for id in ids do
-    if let some decl := lctx.findFromUserName? id.getId then
-      extras := extras.push <| .fvar decl.fvarId
-      thms := thms.push (← mkTheoremFromExpr decl.toExpr)
-    else
-      let declName ← realizeGlobalConstNoOverload id
-      extras := extras.push <| .const declName
-      thms := thms.push (← mkTheoremFromDecl declName)
-  return (extras, thms)
-
-def addExtraTheorems (post : Simproc) (extraThms : Array Theorem) : GrindTacticM Simproc := do
-  if extraThms.isEmpty then return post
-  let mut thms : Theorems := {}
-  for thm in extraThms do
-    thms := thms.insert thm
-  return post >> thms.rewrite
-
-def mkDefaultMethods (extraThms : Array Theorem) : GrindTacticM Sym.Simp.Methods := do
-  let thms ← getSymSimpTheorems
-  let pre := simpControl >> simpArrowTelescope
-  let post ← addExtraTheorems (evalGround >> thms.rewrite) extraThms
-  return { pre, post }
-
-def elabVariant (variantName : Name) (extraThms : Array Theorem) : GrindTacticM (Sym.Simp.Methods × Sym.Simp.Config) := do
-  if variantName.isAnonymous then
-    return (← mkDefaultMethods extraThms, {})
-  let some v := getSymSimpVariant? (← getEnv) variantName
-    | throwError "unknown Sym.simp variant `{variantName}`"
-  let pre ← elabOptSimproc v.pre?
-  let post ← addExtraTheorems (← elabOptSimproc v.post?) extraThms
-  return ({ pre, post}, v.config)
-
-@[builtin_grind_tactic Parser.Tactic.Grind.symSimp] def evalSymSimp : GrindTactic := fun stx => withMainContext do
-  ensureSym
-  let `(grind| simp $[$variantId?]? $[[ $[$extraIds],* ]]?) := stx | throwUnsupportedSyntax
-  -- Resolve variant
-  let variantName := variantId?.map (·.getId) |>.getD .anonymous
-  -- Resolve extra theorems (local hypotheses first, then global constants)
-  let (extras, thms) ← resolveExtraTheorems extraIds
-  -- Cache lookup/creation
-  let cacheKey : SimpCacheKey := { variant := variantName, extras }
-  let simpState := (← get).cache.simpState[cacheKey]?.getD {}
-  let (methods, config) ← elabVariant variantName thms
-  let goal ← getMainGoal
-  let (simpResult, simpState) ← liftGrindM <| goal.withContext do
-    Sym.Simp.SimpM.run (Sym.Simp.simp (← goal.mvarId.getType)) methods config simpState
-  -- Save updated cache
-  modify fun s => { s with cache.simpState := s.cache.simpState.insert cacheKey simpState }
-  -- Apply result to goal
-  match (← liftGrindM <| Sym.Simp.Result.toSimpGoalResult simpResult goal.mvarId) with
-  | .closed => replaceMainGoal []
-  | .goal mvarId => replaceMainGoal [{ goal with mvarId }]
-  | .noProgress => throwError "`Sym.simp` made no progress"
-
-end
-
 end Lean.Elab.Tactic.Grind

src/Lean/Elab/Tactic/Try.lean

@@ -787,7 +787,6 @@ 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,8 +309,6 @@ 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. -/
@@ -373,7 +371,7 @@ whole monad stack at every use site. May eventually be covered by `deriving`.
 -/
 @[always_inline]
 instance : Monad TermElabM :=
-  let i : Monad TermElabM := inferInstance
+  let i := inferInstanceAs (Monad TermElabM)
   { pure := i.pure, bind := i.bind }
 
 open Meta

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) (allowOpaque := false) : Expr :=
-  (c.value! (allowOpaque := allowOpaque)).instantiateLevelParams c.levelParams ls
+def instantiateValueLevelParams! (c : ConstantInfo) (ls : List Level) : Expr :=
+  c.value!.instantiateLevelParams c.levelParams ls
 
 end ConstantInfo
 
@@ -2755,28 +2755,13 @@ 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 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
+    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,6 @@ 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.LetToHave
 public import Lean.Meta.ForEachExpr
 public import Lean.Meta.Transform

src/Lean/Meta/AbstractNestedProofs.lean

@@ -87,13 +87,8 @@ partial def visit (e : Expr) : M Expr := do
         lctx := lctx.modifyLocalDecl xFVarId fun _ => localDecl
       withLCtx lctx localInstances k
     checkCache { val := e : ExprStructEq } fun _ => do
-      if (← isNonTrivialProof e) && !e.hasSorry then
-        /- Ensure proofs nested in type are also abstracted.
-           We skip abstraction for proofs containing `sorry` to avoid generating extra
-           "declaration uses sorry" warnings for auxiliary theorems: one per abstracted proof
-           instead of a single warning for the main declaration. Additionally, the `zetaDelta`
-           expansion in `mkAuxTheorem` can inline let-bound sorry values, causing warnings
-           even for proofs that only transitively reference sorry-containing definitions. -/
+      if (← isNonTrivialProof e) then
+        /- Ensure proofs nested in type are also abstracted -/
         abstractProof e (← read).cache visit
       else match e with
         | .lam ..

src/Lean/Meta/Basic.lean

@@ -565,7 +565,7 @@ abbrev MetaM  := ReaderT Context $ StateRefT State CoreM
 -- Make the compiler generate specialized `pure`/`bind` so we do not have to optimize through the
 -- whole monad stack at every use site. May eventually be covered by `deriving`.
 @[always_inline]
-instance : Monad MetaM := let i : Monad MetaM := inferInstance; { pure := i.pure, bind := i.bind }
+instance : Monad MetaM := let i := inferInstanceAs (Monad MetaM); { pure := i.pure, bind := i.bind }
 
 instance : Inhabited (MetaM α) where
   default := fun _ _ => default
@@ -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 (ConstantInfo.thmInfo _)          => return none
+  | some (info@(ConstantInfo.thmInfo _))  => getTheoremInfo info
   | some (info@(ConstantInfo.defnInfo _)) => getDefInfoTemp info
   | some info                             => pure (some info)
   | none                                  => throwUnknownConstantAt (← getRef) constName

src/Lean/Meta/Closure.lean

@@ -431,8 +431,7 @@ end Closure
   A "closure" is computed, and a term of the form `name.{u_1 ... u_n} t_1 ... t_m` is
   returned where `u_i`s are universe parameters and metavariables `type` and `value` depend on,
   and `t_j`s are free and meta variables `type` and `value` depend on. -/
-def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zetaDelta : Bool := false)
-    (compile : Bool := true) (logCompileErrors : Bool := true) : MetaM Expr := do
+def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zetaDelta : Bool := false) (compile : Bool := true) : MetaM Expr := do
   let result ← Closure.mkValueTypeClosure type value zetaDelta
   let env ← getEnv
   let hints := ReducibilityHints.regular (getMaxHeight env result.value + 1)
@@ -440,16 +439,14 @@ def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zetaDelta : Bool
     result.type result.value  hints)
   addDecl decl
   if compile then
-    compileDecl decl (logErrors := logCompileErrors)
+    compileDecl decl
   return mkAppN (mkConst name result.levelArgs.toList) result.exprArgs
 
 /-- Similar to `mkAuxDefinition`, but infers the type of `value`. -/
-def mkAuxDefinitionFor (name : Name) (value : Expr) (zetaDelta : Bool := false)
-    (compile := true) (logCompileErrors : Bool := true) : MetaM Expr := do
+def mkAuxDefinitionFor (name : Name) (value : Expr) (zetaDelta : Bool := false) (compile := true) : MetaM Expr := do
   let type ← inferType value
   let type := type.headBeta
   mkAuxDefinition name type value (zetaDelta := zetaDelta) (compile := compile)
-    (logCompileErrors := logCompileErrors)
 
 /--
   Create an auxiliary theorem with the given name, type and value. It is similar to `mkAuxDefinition`.

src/Lean/Meta/ExprDefEq.lean

@@ -1126,7 +1126,6 @@ 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
@@ -2234,7 +2233,6 @@ 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,7 +46,11 @@ 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 => return none
+  | .thm =>
+    if (← shouldReduceAll) then
+      return some ainfo.toConstantInfo
+    else
+      return none
   | .defn => if (← canUnfold ainfo.toConstantInfo) then return ainfo.toConstantInfo else return none
   | _ => return none
 
@@ -55,7 +59,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 (.thmInfo _)          => return none
+  | some (info@(.thmInfo _))  => getTheoremInfo info
   | 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,7 +206,6 @@ 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/InstanceNormalForm.lean

@@ -1,193 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Authors: Eric Wieser, Kyle Miller, Jovan Gerbscheid, Kim Morrison, Sebastian Ullrich
--/
-module
-
-prelude
-public import Lean.Meta.Closure
-public import Lean.Meta.SynthInstance
-public import Lean.Meta.CtorRecognizer
-
-public section
-
-/-!
-# Instance Normal Form
-
-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.
-
-## 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
-`instances` transparency:
-
-1. If `I'` is not a class, return `i` unchanged.
-2. If `I'` is a proposition, wrap `i` in an auxiliary theorem of type `I'` and return it
-   (controlled by `backward.inferInstanceAs.wrap.instances`).
-3. Reduce `i` to whnf.
-4. If `i` is not a constructor application: if the type of `i` is already defeq to `I'`,
-   return `i`; otherwise wrap it in an auxiliary definition of type `I'` and return it
-   (controlled by `backward.inferInstanceAs.wrap.instances`).
-5. Otherwise, for `i = ctor a₁ ... aₙ` with `ctor : C ?p₁ ... ?pₙ`:
-   - Unify `C ?p₁ ... ?pₙ` with `I'`.
-   - Return a new application `ctor a₁' ... aₙ' : I'` where each `aᵢ'` is constructed as:
-     - If the field type is a proposition: assign directly if types are defeq, otherwise
-       wrap in an auxiliary theorem.
-     - If the field type is a class: first try to reuse an existing synthesized instance
-       for the target type (controlled by `backward.inferInstanceAs.wrap.reuseSubInstances`);
-       if that fails, recurse with source instance `aᵢ` and expected type `?pᵢ`.
-     - Otherwise (data field): assign directly if types are defeq, otherwise wrap in an
-       auxiliary definition to fix the type (controlled by `backward.inferInstanceAs.wrap.data`).
-
-## Options
-
-- `backward.inferInstanceAs.wrap`: master switch for normalization 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
-- `backward.inferInstanceAs.wrap.instances`: wrap non-reducible instances in auxiliary
-  definitions
-- `backward.inferInstanceAs.wrap.data`: wrap data fields in auxiliary definitions
--/
-
-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"
-}
-
-register_builtin_option backward.inferInstanceAs.wrap.reuseSubInstances : Bool := {
-  defValue := true
-  descr := "when recursing into sub-instances, reuse existing instances for the target type instead of re-wrapping them, which can be important to avoid non-defeq instance diamonds"
-}
-
-register_builtin_option backward.inferInstanceAs.wrap.instances : Bool := {
-  defValue := true
-  descr := "wrap non-reducible instances in auxiliary definitions to fix their types"
-}
-
-register_builtin_option backward.inferInstanceAs.wrap.data : Bool := {
-  defValue := true
-  descr := "wrap data fields in auxiliary definitions to fix their types"
-}
-
-builtin_initialize registerTraceClass `Meta.instanceNormalForm
-
-/--
-Rebuild a type application with fresh synthetic metavariables for instance-implicit arguments.
-Non-instance-implicit arguments are assigned from the original application's arguments.
-If the function is over-applied, extra arguments are preserved.
--/
-def abstractInstImplicitArgs (type : Expr) : MetaM Expr := do
-  let fn := type.getAppFn
-  let args := type.getAppArgs
-  let (mvars, bis, _) ← forallMetaTelescope (← inferType fn)
-  for i in [:mvars.size] do
-    unless bis[i]!.isInstImplicit do
-      mvars[i]!.mvarId!.assign args[i]!
-  let args := mvars ++ args.drop mvars.size
-  instantiateMVars (mkAppN fn args)
-
-/--
-Normalize an instance value to "instance normal form".
-See the module docstring for the full algorithm specification.
--/
-partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true)
-    (logCompileErrors : Bool := true) (isMeta : Bool := false) : MetaM Expr := withTransparency .instances do
-  withTraceNode `Meta.instanceNormalForm
-      (fun _ => return m!"type: {expectedType}") do
-  let some className ← isClass? expectedType
-    | return inst
-  trace[Meta.instanceNormalForm] "class is {className}"
-
-  if ← isProp expectedType then
-    if backward.inferInstanceAs.wrap.instances.get (← getOptions) then
-      return (← mkAuxTheorem expectedType inst (zetaDelta := true))
-    else
-      return inst
-
-  -- Try to reduce it to a constructor.
-  let inst ← whnf inst
-  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}"
-        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 := 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 \
-        constructor application `{f}`: {args}"
-    else
-      unless ← isDefEq expectedType cls do
-        throwError "instance normal form: `{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
-          simp only [ne_eq, Decidable.not_not] at h₁
-          rw [← h₁]
-          get_elem_tactic
-        let mvarId := mvars[i].mvarId!
-        let mvarDecl ← mvarId.getDecl
-        let argExpectedType ← instantiateMVars mvarDecl.type
-        let arg := args[i]
-        if ← isProp argExpectedType then
-          let argType ← inferType arg
-          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}"
-            mvarId.assign (← mkAuxTheorem argExpectedType arg (zetaDelta := true))
-        -- Recurse into instance arguments of the constructor
-        else if (← isClass? argExpectedType).isSome then
-          if backward.inferInstanceAs.wrap.reuseSubInstances.get (← getOptions) then
-            -- Reuse existing instance for the target type if any. This is especially important when recursing
-            -- as it guarantees subinstances of overlapping instances are defeq under more than just
-            -- semireducible transparency.
-            try
-              if let .some new ← trySynthInstance argExpectedType then
-                trace[Meta.instanceNormalForm] "using existing instance {new}"
-                mvarId.assign new
-                continue
-            catch _ => pure ()
-
-          mvarId.assign (← normalizeInstance 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
-            let argType ← inferType arg
-            if ← isDefEq argExpectedType argType then
-              mvarId.assign arg
-            else
-              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
-          else
-            mvarId.assign arg
-      return mkAppN f (← mvars.mapM instantiateMVars)
-
-end Lean.Meta

src/Lean/Meta/LevelDefEq.lean

@@ -85,7 +85,6 @@ 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,7 +138,6 @@ 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
   /-
@@ -247,7 +246,6 @@ 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,7 +785,6 @@ 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.lean

@@ -23,6 +23,3 @@ public import Lean.Meta.Sym.Simp.Discharger
 public import Lean.Meta.Sym.Simp.ControlFlow
 public import Lean.Meta.Sym.Simp.Goal
 public import Lean.Meta.Sym.Simp.Telescope
-public import Lean.Meta.Sym.Simp.Attr
-public import Lean.Meta.Sym.Simp.Variant
-public import Lean.Meta.Sym.Simp.RegisterCommand

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

@@ -1,74 +0,0 @@
-/-
-Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Sym.Simp.Theorems
-import Lean.Meta.Tactic.Simp.SimpTheorems -- for ignoreEquations
-import Lean.Meta.Eqns -- for getEqnsFor?
-public section
-namespace Lean.Meta.Sym.Simp
-
-/--
-Adds a `Sym.Simp` theorem (an equality) to the given extension.
--/
-def addSymSimpTheorem (ext : SymSimpExtension) (declName : Name) (attrKind : AttributeKind) : MetaM Unit := do
-  let thm ← mkTheoremFromDecl declName
-  ext.add thm attrKind
-
-/--
-Creates a `Sym.Simp` attribute for a named theorem set.
-When a proposition is tagged, it is added as a rewrite theorem.
-When a definition is tagged, its equation theorems are added.
--/
-def mkSymSimpAttr (attrName : Name) (attrDescr : String) (ext : SymSimpExtension)
-    (ref : Name := by exact decl_name%) : IO Unit :=
-  registerBuiltinAttribute {
-    ref   := ref
-    name  := attrName
-    descr := attrDescr
-    applicationTime := AttributeApplicationTime.afterCompilation
-    add   := fun declName _ attrKind => do
-      let go : MetaM Unit := do
-        let info ← getAsyncConstInfo declName
-        if (← isProp info.sig.get.type) then
-          addSymSimpTheorem ext declName attrKind
-        else if info.kind matches .defn then
-          if (← Simp.ignoreEquations declName) then
-            throwError "Cannot add `{attrName}` attribute to `{.ofConstName declName}`: \
-              It is a reducible definition or projection. `Sym.simp` does not support unfolding."
-          else if let some eqns ← getEqnsFor? declName then
-            for eqn in eqns do
-              addSymSimpTheorem ext eqn attrKind
-          else
-            throwError "Cannot add `{attrName}` attribute to `{.ofConstName declName}`: \
-              No equation theorems found."
-        else
-          throwError "Cannot add `{attrName}` attribute to `{.ofConstName declName}`: \
-            It is not a proposition nor a definition with equation theorems."
-      discard <| go.run {} {}
-    erase := fun _declName => do
-      throwError "Erasing `Sym.simp` attributes is not supported yet."
-  }
-
-/--
-Registers a named `Sym.Simp` theorem set. Each set gets its own attribute
-and its own `SymSimpExtension` (persistent environment extension).
-
-Must be called during initialization.
--/
-def registerSymSimpAttr (attrName : Name) (attrDescr : String)
-    (ref : Name := by exact decl_name%) : IO SymSimpExtension := do
-  let ext ← mkSymSimpExt ref
-  mkSymSimpAttr attrName attrDescr ext ref
-  symSimpExtensionMapRef.modify fun map => map.insert attrName ext
-  return ext
-
-builtin_initialize symSimpExtension : SymSimpExtension ← registerSymSimpAttr `sym_simp "Sym.simp theorem"
-
-def getSymSimpTheorems : CoreM Theorems :=
-  symSimpExtension.getTheorems
-
-end Lean.Meta.Sym.Simp

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

@@ -40,7 +40,6 @@ 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/Simp/RegisterCommand.lean

@@ -1,23 +0,0 @@
-/-
-Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Sym.Simp.Attr
-public import Lean.Meta.Sym.Simp.Variant
-public meta import Init.Data.ToString.Name
-public meta import Init.Data.String.Extra
-public section
-namespace Lean.Meta.Sym.Simp
-
-macro (name := _root_.Lean.Parser.Command.registerSymSimpAttr) doc:(docComment)?
-  "register_sym_simp_attr" id:ident : command => do
-  let str := id.getId.toString
-  let idParser := mkIdentFrom id (`Parser.Attr ++ id.getId)
-  let descr := quote ((doc.map (·.getDocString) |>.getD s!"Sym.simp set for {id.getId.toString}").removeLeadingSpaces)
-  `($[$doc:docComment]? public meta initialize ext : SymSimpExtension ← registerSymSimpAttr $(quote id.getId) $descr
-    $[$doc:docComment]? syntax (name := $idParser:ident) $(quote str):str : attr)
-
-end Lean.Meta.Sym.Simp

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

@@ -9,7 +9,6 @@ public import Lean.Meta.Sym.Simp.Simproc
 public import Lean.Meta.Sym.Simp.Theorems
 public import Lean.Meta.Sym.Simp.App
 public import Lean.Meta.Sym.Simp.Discharger
-import Lean.Meta.ACLt
 import Lean.Meta.Sym.InstantiateS
 import Lean.Meta.Sym.InstantiateMVarsS
 import Init.Data.Range.Polymorphic.Iterators
@@ -72,16 +71,10 @@ public def Theorem.rewrite (thm : Theorem) (e : Expr) (d : Discharger := dischar
     let expr  ← instantiateRevBetaS rhs args.toArray
     if isSameExpr e expr then
       return mkRflResultCD isCD
-    else if !(← checkPerm thm.perm e expr) then
-      return mkRflResultCD isCD
     else
       return .step expr proof (contextDependent := isCD)
   else
     return .rfl
-where
-  checkPerm (perm : Bool) (e result : Expr) : MetaM Bool := do
-    if !perm then return true
-    acLt result e
 
 public def Theorems.rewrite (thms : Theorems) (d : Discharger := dischargeNone) : Simproc := fun e => do
   -- Track `cd` across all attempted theorems. If theorem A fails with cd=true

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

@@ -106,7 +106,6 @@ structure Config where
   Prevents infinite loops when conditional rewrite rules trigger recursive discharge attempts.
   -/
   maxDischargeDepth : Nat := 2
-  deriving Inhabited
 
 /--
 The result of simplifying an expression `e`.

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

@@ -8,9 +8,6 @@ prelude
 public import Lean.Meta.Sym.Pattern
 public import Lean.Meta.DiscrTree
 import Lean.Meta.Sym.Simp.DiscrTree
-import Lean.Meta.AppBuilder
-import Lean.ExtraModUses
-import Init.Omega
 public section
 namespace Lean.Meta.Sym.Simp
 
@@ -27,10 +24,6 @@ structure Theorem where
   pattern : Pattern
   /-- Right-hand side of the equation. -/
   rhs     : Expr
-  /-- If `true`, the theorem is a permutation rule (e.g., `x + y = y + x`).
-  Rewriting is only applied when the result is strictly less than the input
-  (using `acLt`), preventing infinite loops. -/
-  perm    : Bool := false
   deriving Inhabited
 
 instance : BEq Theorem where
@@ -39,7 +32,6 @@ instance : BEq Theorem where
 /-- Collection of simplification theorems available to the simplifier. -/
 structure Theorems where
   thms : DiscrTree Theorem := {}
-  deriving Inhabited
 
 def Theorems.insert (thms : Theorems) (thm : Theorem) : Theorems :=
   { thms with thms := insertPattern thms.thms thm.pattern thm }
@@ -50,141 +42,8 @@ def Theorems.getMatch (thms : Theorems) (e : Expr) : Array Theorem :=
 def Theorems.getMatchWithExtra (thms : Theorems) (e : Expr) : Array (Theorem × Nat) :=
   Sym.getMatchWithExtra thms.thms e
 
-/--
-Check whether `lhs` and `rhs` (with `numVars` pattern variables represented as `.bvar` indices
-`≥ 0` before any binder entry) are permutations of each other — same structure with only
-pattern variable indices rearranged via a consistent bijection.
-
-Bvars with index `< offset` are "local" (introduced by binders inside the pattern) and must
-match exactly. Bvars with index `≥ offset` are pattern variables and may be permuted,
-but the mapping must be a bijection.
-
-Simplified compared to `Meta.simp`'s `isPerm`:
-- Uses de Bruijn indices instead of metavariables
-- No `.proj` (folded into applications) or `.letE` (zeta-expanded) cases
--/
-private abbrev IsPermM := ReaderT Nat $ StateT (Array (Option Nat)) $ Except Unit
-
-private partial def isPermAux (a b : Expr) : IsPermM Unit := do
-  match a, b with
-  | .bvar i, .bvar j =>
-    let offset ← read
-    if i < offset && j < offset then
-      unless i == j do throw ()
-    else if i >= offset && j >= offset then
-      let pi := i - offset
-      let pj := j - offset
-      let fwd ← get
-      if h : pi >= fwd.size then throw () else
-      match fwd[pi] with
-      | none =>
-        -- Check injectivity: pj must not already be a target of another mapping
-        if fwd.contains (some pj) then throw ()
-        set (fwd.set pi (some pj))
-      | some pj' => unless pj == pj' do throw ()
-    else throw ()
-  | .app f₁ a₁, .app f₂ a₂ => isPermAux f₁ f₂; isPermAux a₁ a₂
-  | .mdata _ s, t => isPermAux s t
-  | s, .mdata _ t => isPermAux s t
-  | .forallE _ d₁ b₁ _, .forallE _ d₂ b₂ _ => isPermAux d₁ d₂; withReader (· + 1) (isPermAux b₁ b₂)
-  | .lam _ d₁ b₁ _, .lam _ d₂ b₂ _ => isPermAux d₁ d₂; withReader (· + 1) (isPermAux b₁ b₂)
-  | s, t => unless s == t do throw ()
-
-def isPerm (numVars : Nat) (lhs rhs : Expr) : Bool :=
-  ((isPermAux lhs rhs).run 0 |>.run (Array.replicate numVars none)) matches .ok _
-
-/-- Describes how a theorem's conclusion was adapted to an equality for use in `Sym.simp`. -/
-private inductive EqAdaptation where
-  /-- Already an equality `lhs = rhs`. Proof is used as-is. -/
-  | eq
-  /-- Was `¬ p`. Proof `h` adapted to `eq_false h : p = False`. -/
-  | eqFalse
-  /-- Was `p ↔ q`. Proof `h` adapted to `propext h : p = q`. -/
-  | iff
-  /-- Was a proposition `p`. Proof `h` adapted to `eq_true h : p = True`. -/
-  | eqTrue
-
-/--
-Analyze the conclusion of a theorem type and extract `(lhs, rhs)` for use as a
-rewrite rule in `Sym.simp`. Handles:
-- `lhs = rhs` — used as-is
-- `¬ p` — adapted to `p = False`
-- `p ↔ q` — adapted to `p = q`
-- `p` (proposition) — adapted to `p = True`
--/
-private def selectEqKey (type : Expr) : MetaM (Expr × Expr × EqAdaptation) := do
-  match_expr type with
-  | Eq _ lhs rhs => return (lhs, rhs, .eq)
-  | Not p => return (p, mkConst ``False, .eqFalse)
-  | Iff lhs rhs => return (lhs, rhs, .iff)
-  | _ =>
-    unless (← isProp type) do
-      throwError "cannot use as a simp theorem, conclusion is not a proposition{indentExpr type}"
-    return (type, mkConst ``True, .eqTrue)
-
-/--
-Wrap a proof expression according to the adaptation applied to its type.
-Given a proof `h : <original type>`, returns a proof of the adapted equality.
-This wrapping must be applied AFTER the proof has been applied to its quantified arguments.
--/
-private def wrapProof (numVars : Nat) (expr : Expr) (adaptation : EqAdaptation) : MetaM Expr :=
-  match adaptation with
-  | .eq => return expr
-  | .eqFalse =>
-    wrapInner numVars expr fun h => mkAppM ``eq_false #[h]
-  | .iff =>
-    wrapInner numVars expr fun h => mkAppM ``propext #[h]
-  | .eqTrue =>
-    wrapInner numVars expr fun h => mkAppM ``eq_true #[h]
-where
-  /-- Wraps the innermost application of `expr` (after `numVars` arguments) with `wrap`. -/
-  wrapInner (numVars : Nat) (expr : Expr) (wrap : Expr → MetaM Expr) : MetaM Expr := do
-    let type ← inferType expr
-    forallBoundedTelescope type numVars fun xs _ => do
-      let h := mkAppN expr xs
-      mkLambdaFVars xs (← wrap h)
-
 def mkTheoremFromDecl (declName : Name) : MetaM Theorem := do
-  let (pattern, (rhs, adaptation)) ← mkPatternFromDeclWithKey declName selectEqKey
-  let expr ← wrapProof pattern.varTypes.size (mkConst declName) adaptation
-  let perm := isPerm pattern.varTypes.size pattern.pattern rhs
-  return { expr, pattern, rhs, perm }
-
-/-- Create a `Theorem` from a proof expression. Handles equalities, `¬`, `↔`, and propositions. -/
-def mkTheoremFromExpr (e : Expr) : MetaM Theorem := do
-  let (pattern, (rhs, adaptation)) ← mkPatternFromExprWithKey e [] selectEqKey
-  let expr ← wrapProof pattern.varTypes.size e adaptation
-  let perm := isPerm pattern.varTypes.size pattern.pattern rhs
-  return { expr, pattern, rhs, perm }
-
-/--
-Environment extension storing a set of `Sym.Simp` theorems.
-Each named set gets its own extension, created by `registerSymSimpAttr`.
--/
-abbrev SymSimpExtension := SimpleScopedEnvExtension Theorem Theorems
-
-def SymSimpExtension.getTheorems (ext : SymSimpExtension) : CoreM Theorems :=
-  return ext.getState (← getEnv)
-
-def mkSymSimpExt (name : Name := by exact decl_name%) : IO SymSimpExtension :=
-  registerSimpleScopedEnvExtension {
-    name     := name
-    initial  := {}
-    addEntry := fun thms thm => thms.insert thm
-    exportEntry? := fun lvl thm => do
-      let .const declName _ := thm.expr | return thm
-      guard (lvl == .private || !isPrivateName declName)
-      return thm
-  }
-
-abbrev SymSimpExtensionMap := Std.HashMap Name SymSimpExtension
-
-builtin_initialize symSimpExtensionMapRef : IO.Ref SymSimpExtensionMap ← IO.mkRef {}
-
-def getSymSimpExtension? (attrName : Name) : CoreM (Option SymSimpExtension) := do
-  let ext? := (← symSimpExtensionMapRef.get)[attrName]?
-  if let some ext := ext? then
-    recordExtraModUseFromDecl (isMeta := true) ext.ext.name
-  return ext?
+  let (pattern, rhs) ← mkEqPatternFromDecl declName
+  return { expr := mkConst declName, pattern, rhs }
 
 end Lean.Meta.Sym.Simp

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

@@ -1,45 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Sym.Simp.SimpM
-import Lean.ScopedEnvExtension
-public section
-namespace Lean.Meta.Sym.Simp
-
-/--
-A named `Sym.simp` variant. Stores `pre`/`post` simproc chains as syntax
-(elaborated at use time in `GrindTacticM`) and configuration overrides.
--/
-structure SymSimpVariant where
-  /-- Pre-processing simproc chain (elaborated at use time). -/
-  pre?   : Option Syntax := none
-  /-- Post-processing simproc chain (elaborated at use time). -/
-  post?  : Option Syntax := none
-  /-- Configuration overrides. -/
-  config : Config := {}
-  deriving Inhabited
-
-/-- Entry for the scoped environment extension. -/
-structure SymSimpVariantEntry where
-  name    : Name
-  variant : SymSimpVariant
-  deriving Inhabited
-
-/-- Persistent environment extension mapping variant names to their definitions. -/
-builtin_initialize symSimpVariantExtension :
-    SimpleScopedEnvExtension SymSimpVariantEntry (Std.HashMap Name SymSimpVariant) ←
-  registerSimpleScopedEnvExtension {
-    name     := `symSimpVariantExtension
-    initial  := {}
-    addEntry := fun map entry => map.insert entry.name entry.variant
-  }
-
-/-- Look up a named `Sym.simp` variant. -/
-def getSymSimpVariant? (env : Environment) (name : Name) : Option SymSimpVariant :=
-  (symSimpVariantExtension.getState env)[name]?
-
-end Lean.Meta.Sym.Simp

src/Lean/Meta/Sym/SymM.lean

@@ -15,48 +15,6 @@ register_builtin_option sym.debug : Bool := {
   descr    := "check invariants"
 }
 
-/-!
-## 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.
 
@@ -175,8 +133,6 @@ 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 := #[]
   debug : Bool := false
 
 abbrev SymM := ReaderT Context <| StateRefT State MetaM
@@ -194,8 +150,7 @@ private def mkSharedExprs : AlphaShareCommonM SharedExprs := do
 def SymM.run (x : SymM α) : MetaM α := do
   let (sharedExprs, share) := mkSharedExprs |>.run {}
   let debug := sym.debug.get (← getOptions)
-  let extensions ← SymExtensions.mkInitialStates
-  x { sharedExprs } |>.run' { debug, share, extensions }
+  x { sharedExprs } |>.run' { debug, share }
 
 /-- Returns maximally shared commonly used terms -/
 def getSharedExprs : SymM SharedExprs :=
@@ -275,26 +230,4 @@ 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,7 +944,6 @@ 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/Delta.lean

@@ -10,18 +10,18 @@ import Lean.Meta.Transform
 public section
 namespace Lean.Meta
 
-def delta? (e : Expr) (p : Name → Bool := fun _ => true) (allowOpaque := false) : CoreM (Option Expr) :=
+def delta? (e : Expr) (p : Name → Bool := fun _ => true) : CoreM (Option Expr) :=
   matchConst e.getAppFn (fun _ => return none) fun fInfo fLvls => do
-    if p fInfo.name && fInfo.hasValue (allowOpaque := allowOpaque) && fInfo.levelParams.length == fLvls.length then
-      let f ← instantiateValueLevelParams fInfo fLvls (allowOpaque := allowOpaque)
+    if p fInfo.name && fInfo.hasValue && fInfo.levelParams.length == fLvls.length then
+      let f ← instantiateValueLevelParams fInfo fLvls
       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) (allowOpaque := false) : CoreM Expr :=
+def deltaExpand (e : Expr) (p : Name → Bool) : CoreM Expr :=
   Core.transform e fun e => do
-    match (← delta? e p (allowOpaque := allowOpaque)) with
+    match (← delta? e p) with
     | some e' => return .visit e'
     | none    => return .continue
 

src/Lean/Meta/Tactic/FunInd.lean

@@ -347,13 +347,11 @@ 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 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}"
+      -- 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}"
 
     match e with
     | .app e1 e2 =>
@@ -744,13 +742,6 @@ 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/Arith/CommRing/EqCnstr.lean

@@ -109,7 +109,7 @@ def _root_.Lean.Grind.CommRing.Poly.findSimp? (p : Poly) : RingM (Option EqCnstr
 /-- Simplifies `d.p` using `c`, and returns an extended polynomial derivation. -/
 def PolyDerivation.simplifyWith (d : PolyDerivation) (c : EqCnstr) : RingM PolyDerivation := do
   let some r := d.p.simp? c.p (← nonzeroChar?) | return d
-  incSteps r.p.numTerms
+  incSteps
   trace_goal[grind.ring.simp] "{← r.p.denoteExpr}"
   return .step r.p r.k₁ d r.k₂ r.m₂ c
 
@@ -137,7 +137,7 @@ def EqCnstr.simplifyWithCore (c₁ c₂ : EqCnstr) : RingM (Option EqCnstr) := d
     p := r.p
     h := .simp r.k₁ c₁ r.k₂ r.m₂ c₂
   }
-  incSteps r.p.numTerms
+  incSteps
   trace_goal[grind.ring.simp] "{← c.p.denoteExpr}"
   return some c
 

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

@@ -184,15 +184,6 @@ def Poly.degree : Poly → Nat
   | .num _ => 0
   | .add _ m _ => m.degree
 
-/-- Returns the number of monomials in the polynomial. -/
-def Poly.numTerms (p : Poly) : Nat :=
-  go p 0
-where
-  go (p : Poly) (acc : Nat) : Nat :=
-    match p with
-    | .num .. => acc
-    | .add _ _ p => go p (acc + 1)
-
 /-- Returns `true` if the leading monomial of `p` divides `m`. -/
 def Poly.divides (p : Poly) (m : Mon) : Bool :=
   match p with

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

@@ -13,8 +13,8 @@ namespace Lean.Meta.Grind.Arith.CommRing
 def checkMaxSteps : GoalM Bool := do
   return (← get').steps >= (← getConfig).ringSteps
 
-def incSteps (n : Nat := 1) : GoalM Unit := do
-  modify' fun s => { s with steps := s.steps + n }
+def incSteps : GoalM Unit := do
+  modify' fun s => { s with steps := s.steps + 1 }
 
 structure RingM.Context where
   ringId : Nat

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

@@ -276,7 +276,6 @@ 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
@@ -339,7 +338,6 @@ 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,7 +99,6 @@ 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,9 +325,7 @@ 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,7 +64,6 @@ 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,7 +239,6 @@ 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}"