chore: update grind IndexMap example

.github/workflows/build-template.yml

@@ -102,7 +102,7 @@ jobs:
         if: matrix.cmultilib
       - name: Restore Cache
         id: restore-cache
-        uses: actions/cache/restore@v5
+        uses: actions/cache/restore@v4
         with:
           # NOTE: must be in sync with `save` below and with `restore-cache` in `update-stage0.yml`
           path: |
@@ -175,7 +175,7 @@ jobs:
         # Caching on cancellation created some mysterious issues perhaps related to improper build
         # shutdown
         if: steps.restore-cache.outputs.cache-hit != 'true' && !cancelled()
-        uses: actions/cache/save@v5
+        uses: actions/cache/save@v4
         with:
           # NOTE: must be in sync with `restore` above
           path: |

.github/workflows/ci.yml

@@ -433,7 +433,7 @@ jobs:
     runs-on: ubuntu-latest
     needs: build
     steps:
-      - uses: actions/download-artifact@v7
+      - uses: actions/download-artifact@v6
         with:
           path: artifacts
       - name: Release
@@ -465,7 +465,7 @@ jobs:
           # Doesn't seem to be working when additionally fetching from lean4-nightly
           #filter: tree:0
           token: ${{ secrets.PUSH_NIGHTLY_TOKEN }}
-      - uses: actions/download-artifact@v7
+      - uses: actions/download-artifact@v6
         with:
           path: artifacts
       - name: Prepare Nightly Release

.github/workflows/pr-release.yml

@@ -396,18 +396,6 @@ jobs:
       # We next automatically create a Batteries branch using this toolchain.
       # Batteries doesn't itself have a mechanism to report results of CI from this branch back to Lean
       # Instead this is taken care of by Mathlib CI, which will fail if Batteries fails.
-
-      # Generate a token from the mathlib-nightly-testing GitHub App for cross-org access
-      - name: Generate GitHub App token for leanprover-community repos
-        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        id: mathlib-app-token
-        uses: actions/create-github-app-token@3ff1caaa28b64c9cc276ce0a02e2ff584f3900c5 # v2.0.2
-        with:
-          app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }}
-          private-key: ${{ secrets.MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY }}
-          owner: leanprover-community
-          repositories: batteries,mathlib4-nightly-testing
-
       - name: Cleanup workspace
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
         run: |
@@ -419,7 +407,7 @@ jobs:
         uses: actions/checkout@v6
         with:
           repository: leanprover-community/batteries
-          token: ${{ steps.mathlib-app-token.outputs.token }}
+          token: ${{ secrets.MATHLIB4_BOT }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
           filter: tree:0
@@ -479,7 +467,7 @@ jobs:
         uses: actions/checkout@v6
         with:
           repository: leanprover-community/mathlib4-nightly-testing
-          token: ${{ steps.mathlib-app-token.outputs.token }}
+          token: ${{ secrets.MATHLIB4_BOT }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
           filter: tree:0

.github/workflows/update-stage0.yml

@@ -58,7 +58,7 @@ jobs:
       shell: 'nix develop -c bash -euxo pipefail {0}'
     - name: Restore Cache
       if: env.should_update_stage0 == 'yes'
-      uses: actions/cache/restore@v5
+      uses: actions/cache/restore@v4
       with:
         # NOTE: must be in sync with `restore-cache` in `build-template.yml`
         path: |

src/CMakeLists.txt

@@ -375,6 +375,9 @@ if(CCACHE AND NOT CMAKE_CXX_COMPILER_LAUNCHER AND NOT CMAKE_C_COMPILER_LAUNCHER)
   endif()
 endif()
 
+# Python
+find_package(PythonInterp)
+
 include_directories(${CMAKE_BINARY_DIR}/include)
 
 # Pick up `llvm-config` to setup LLVM flags.
@@ -665,13 +668,6 @@ endif()
 
 add_subdirectory(initialize)
 add_subdirectory(shell)
-
-# The relative path doesn't work once the CMakeLists.txt files have been copied into the stage0 dir.
-# Since stage0 needs no tests, we just ignore them instead of fixing the path.
-if(NOT STAGE EQUAL 0)
-  add_subdirectory(../tests "${CMAKE_CURRENT_BINARY_DIR}/tests")
-endif()
-
 # to be included in `leanshared` but not the smaller `leanshared_*` (as it would pull
 # in the world)
 add_library(leaninitialize STATIC $<TARGET_OBJECTS:initialize>)

src/Init/Classical.lean

@@ -142,7 +142,6 @@ is classically true but not constructively. -/
 
 /-- Transfer decidability of `¬ p` to decidability of `p`. -/
 -- This can not be an instance as it would be tried everywhere.
-@[instance_reducible]
 def decidable_of_decidable_not (p : Prop) [h : Decidable (¬ p)] : Decidable p :=
   match h with
   | isFalse h => isTrue (Classical.not_not.mp h)

src/Init/Control/Lawful/Instances.lean

@@ -121,11 +121,6 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (ExceptT ε m) where
 @[simp] theorem run_control [Monad m] [LawfulMonad m] (f : ({β : Type u} → ExceptT ε m β → m (stM m (ExceptT ε m) β)) → m (stM m (ExceptT ε m) α)) :
     ExceptT.run (control f) = f fun x => x.run := run_controlAt f
 
-@[simp, grind =]
-theorem run_adapt [Monad m] (f : ε → ε') (x : ExceptT ε m α)
-    : run (ExceptT.adapt f x : ExceptT ε' m α) = Except.mapError f <$> run x :=
-  rfl
-
 end ExceptT
 
 /-! # Except -/
@@ -472,24 +467,6 @@ namespace EStateM
 @[simp, grind =] theorem run_throw (e : ε) (s : σ):
     EStateM.run (throw e : EStateM ε σ PUnit) s = .error e s := rfl
 
-@[simp, grind =] theorem run_bind (x : EStateM ε σ α) (f : α → EStateM ε σ β)
-    : EStateM.run (x >>= f : EStateM ε σ β) s
-      =
-      match EStateM.run x s with
-      | .ok x s => EStateM.run (f x) s
-      | .error e s => .error e s :=
-  rfl
-
-@[simp, grind =]
-theorem run_adaptExcept (f : ε → ε') (x : EStateM ε σ α) (s : σ)
-    : EStateM.run (EStateM.adaptExcept f x : EStateM ε' σ α) s
-     =
-     match EStateM.run x s with
-     | .ok x s => .ok x s
-     | .error e s => .error (f e) s := by
-  simp only [EStateM.run, EStateM.adaptExcept]
-  cases (x s) <;> rfl
-
 instance : LawfulMonad (EStateM ε σ) := .mk'
   (id_map := fun x => funext <| fun s => by
     simp only [Functor.map, EStateM.map]

src/Init/Control/MonadAttach.lean

@@ -70,7 +70,7 @@ information to the return value, except a trivial proof of {name}`True`.
 This instance is used whenever no more useful {name}`MonadAttach` instance can be implemented.
 It always has a {name}`WeaklyLawfulMonadAttach`, but usually no {name}`LawfulMonadAttach` instance.
 -/
-@[expose, instance_reducible]
+@[expose]
 public protected def MonadAttach.trivial {m : Type u → Type v} [Monad m] : MonadAttach m where
   CanReturn _ _ := True
   attach x := (⟨·, .intro⟩) <$> x

src/Init/Conv.lean

@@ -51,10 +51,6 @@ scoped syntax (name := withAnnotateState)
 /-- `skip` does nothing. -/
 syntax (name := skip) "skip" : conv
 
-/-- `cbv` performs simplification that closely mimics call-by-value evaluation,
-using equations associated with definitions and the matchers. -/
-syntax (name := cbv) "cbv" : conv
-
 /--
 Traverses into the left subterm of a binary operator.
 

src/Init/Core.lean

@@ -2360,10 +2360,8 @@ namespace Lean
 /--
 Depends on the correctness of the Lean compiler, interpreter, and all `[implemented_by ...]` and `[extern ...]` annotations.
 -/
-@[deprecated "in-kernel native reduction is deprecated; assert native evaluations with axioms instead" (since := "2026-02-01")]
 axiom trustCompiler : True
 
-set_option linter.deprecated false in
 /--
 When the kernel tries to reduce a term `Lean.reduceBool c`, it will invoke the Lean interpreter to evaluate `c`.
 The kernel will not use the interpreter if `c` is not a constant.
@@ -2383,13 +2381,11 @@ Recall that the compiler trusts the correctness of all `[implemented_by ...]` an
 If an extern function is executed, then the trusted code base will also include the implementation of the associated
 foreign function.
 -/
-@[deprecated "in-kernel native reduction is deprecated; assert native evaluations with axioms instead" (since := "2026-02-01")]
 opaque reduceBool (b : Bool) : Bool :=
   -- This ensures that `#print axioms` will track use of `reduceBool`.
   have := trustCompiler
   b
 
-set_option linter.deprecated false in
 /--
 Similar to `Lean.reduceBool` for closed `Nat` terms.
 
@@ -2397,14 +2393,12 @@ Remark: we do not have plans for supporting a generic `reduceValue {α} (a : α)
 The main issue is that it is non-trivial to convert an arbitrary runtime object back into a Lean expression.
 We believe `Lean.reduceBool` enables most interesting applications (e.g., proof by reflection).
 -/
-@[deprecated "in-kernel native reduction is deprecated; assert native evaluations with axioms instead" (since := "2026-02-01")]
 opaque reduceNat (n : Nat) : Nat :=
   -- This ensures that `#print axioms` will track use of `reduceNat`.
   have := trustCompiler
   n
 
 
-set_option linter.deprecated false in
 /--
 The axiom `ofReduceBool` is used to perform proofs by reflection. See `reduceBool`.
 
@@ -2418,10 +2412,8 @@ external type checkers that do not implement this feature.
 Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter.
 So, you are mainly losing the capability of type checking your development using external checkers.
 -/
-@[deprecated "in-kernel native reduction is deprecated; assert native evaluations with axioms instead" (since := "2026-02-01")]
 axiom ofReduceBool (a b : Bool) (h : reduceBool a = b) : a = b
 
-set_option linter.deprecated false in
 /--
 The axiom `ofReduceNat` is used to perform proofs by reflection. See `reduceBool`.
 
@@ -2431,7 +2423,6 @@ external type checkers that do not implement this feature.
 Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter.
 So, you are mainly losing the capability of type checking your development using external checkers.
 -/
-@[deprecated "in-kernel native reduction is deprecated; assert native evaluations with axioms instead" (since := "2026-02-01")]
 axiom ofReduceNat (a b : Nat) (h : reduceNat a = b) : a = b
 
 
@@ -2482,7 +2473,7 @@ class IdempotentOp (op : α → α → α) : Prop where
   idempotent : (x : α) → op x x = x
 
 /--
-`LeftIdentity op o` indicates `o` is a left identity of `op`.
+`LeftIdentify op o` indicates `o` is a left identity of `op`.
 
 This class does not require a proof that `o` is an identity, and
 is used primarily for inferring the identity using class resolution.
@@ -2490,7 +2481,7 @@ is used primarily for inferring the identity using class resolution.
 class LeftIdentity (op : α → β → β) (o : outParam α) : Prop
 
 /--
-`LawfulLeftIdentity op o` indicates `o` is a verified left identity of
+`LawfulLeftIdentify op o` indicates `o` is a verified left identity of
 `op`.
 -/
 class LawfulLeftIdentity (op : α → β → β) (o : outParam α) : Prop extends LeftIdentity op o where
@@ -2498,7 +2489,7 @@ class LawfulLeftIdentity (op : α → β → β) (o : outParam α) : Prop extend
   left_id : ∀ a, op o a = a
 
 /--
-`RightIdentity op o` indicates `o` is a right identity `o` of `op`.
+`RightIdentify op o` indicates `o` is a right identity `o` of `op`.
 
 This class does not require a proof that `o` is an identity, and is used
 primarily for inferring the identity using class resolution.
@@ -2506,7 +2497,7 @@ primarily for inferring the identity using class resolution.
 class RightIdentity (op : α → β → α) (o : outParam β) : Prop
 
 /--
-`LawfulRightIdentity op o` indicates `o` is a verified right identity of
+`LawfulRightIdentify op o` indicates `o` is a verified right identity of
 `op`.
 -/
 class LawfulRightIdentity (op : α → β → α) (o : outParam β) : Prop extends RightIdentity op o where

src/Init/Data/Array.lean

@@ -31,5 +31,3 @@ public import Init.Data.Array.Zip
 public import Init.Data.Array.InsertIdx
 public import Init.Data.Array.Extract
 public import Init.Data.Array.MinMax
-public import Init.Data.Array.Nat
-public import Init.Data.Array.Int

src/Init/Data/Array/Count.lean

@@ -9,7 +9,6 @@ prelude
 import all Init.Data.Array.Basic
 public import Init.Data.Array.Lemmas
 public import Init.Data.List.Nat.Count
-import Init.Grind.Util
 
 public section
 
@@ -93,18 +92,6 @@ theorem countP_le_size : countP p xs ≤ xs.size := by
   rcases xs with ⟨xs⟩
   simp
 
-/-- This lemma is only relevant for `grind`. -/
-@[grind ←=]
-theorem _root_.Std.Internal.Array.countP_eq_zero_of_forall {xs : Array α} (h : ∀ x ∈ xs, ¬ p x) : xs.countP p = 0 :=
-  countP_eq_zero.mpr h
-
-/-- This lemma is only relevant for `grind`. -/
-theorem _root_.Std.Internal.Array.not_of_countP_eq_zero_of_mem {xs : Array α} (h : xs.countP p = 0) (h' : x ∈ xs) : ¬ p x :=
-   countP_eq_zero.mp h _ h'
-
-grind_pattern Std.Internal.Array.not_of_countP_eq_zero_of_mem => xs.countP p, x ∈ xs where
-  guard xs.countP p = 0
-
 @[simp] theorem countP_eq_size {p} : countP p xs = xs.size ↔ ∀ a ∈ xs, p a := by
   rcases xs with ⟨xs⟩
   simp

src/Init/Data/Array/Find.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Data.List.Nat.Find
-import Init.Data.List.Nat.Sum
 import all Init.Data.Array.Basic
 public import Init.Data.Array.Range
 
@@ -115,7 +114,7 @@ theorem getElem_zero_flatten.proof {xss : Array (Array α)} (h : 0 < xss.flatten
   simp only [List.findSome?_toArray, List.findSome?_map, Function.comp_def, List.getElem?_toArray,
     List.findSome?_isSome_iff, isSome_getElem?]
   simp only [flatten_toArray_map_toArray, List.size_toArray, List.length_flatten,
-    List.sum_pos_iff_exists_pos_nat, List.mem_map] at h
+    Nat.sum_pos_iff_exists_pos, List.mem_map] at h
   obtain ⟨_, ⟨xs, m, rfl⟩, h⟩ := h
   exact ⟨xs, m, by simpa using h⟩
 

src/Init/Data/Array/Int.lean

@@ -1,35 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison, Sebastian Graf, Paul Reichert
--/
-module
-
-prelude
-public import Init.Data.List.Int.Sum
-public import Init.Data.Array.Lemmas
-public import Init.Data.Int.DivMod.Bootstrap
-import Init.Data.Int.DivMod.Lemmas
-import Init.Data.List.MinMax
-
-public section
-
-set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-set_option linter.indexVariables true -- Enforce naming conventions for index variables.
-
-namespace Array
-
-@[simp] theorem sum_replicate_int {n : Nat} {a : Int} : (replicate n a).sum = n * a := by
-  rw [← List.toArray_replicate, List.sum_toArray]
-  simp
-
-theorem sum_append_int {as₁ as₂ : Array Int} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
-  simp [sum_append]
-
-theorem sum_reverse_int (xs : Array Int) : xs.reverse.sum = xs.sum := by
-  simp [sum_reverse]
-
-theorem sum_eq_foldl_int {xs : Array Int} : xs.sum = xs.foldl (init := 0) (· + ·) := by
-  simp only [foldl_eq_foldr_reverse, Int.add_comm, ← sum_eq_foldr, sum_reverse_int]
-
-end Array

src/Init/Data/Array/Lemmas.lean

@@ -482,18 +482,9 @@ theorem mem_iff_getElem {a} {xs : Array α} : a ∈ xs ↔ ∃ (i : Nat) (h : i
 theorem mem_iff_getElem? {a} {xs : Array α} : a ∈ xs ↔ ∃ i : Nat, xs[i]? = some a := by
   simp [getElem?_eq_some_iff, mem_iff_getElem]
 
-theorem exists_mem_iff_exists_getElem {P : α → Prop} {xs : Array α} :
-    (∃ x ∈ xs, P x) ↔ ∃ (i : Nat), ∃ (hi : i < xs.size), P (xs[i]) := by
-  cases xs; simp [List.exists_mem_iff_exists_getElem]
-
-theorem forall_mem_iff_forall_getElem {P : α → Prop} {xs : Array α} :
-    (∀ x ∈ xs, P x) ↔ ∀ (i : Nat) (hi : i < xs.size), P (xs[i]) := by
-  cases xs; simp [List.forall_mem_iff_forall_getElem]
-
-@[deprecated forall_mem_iff_forall_getElem (since := "2026-01-29")]
 theorem forall_getElem {xs : Array α} {p : α → Prop} :
     (∀ (i : Nat) h, p (xs[i]'h)) ↔ ∀ a, a ∈ xs → p a := by
-  exact forall_mem_iff_forall_getElem.symm
+  cases xs; simp [List.forall_getElem]
 
 /-! ### isEmpty -/
 
@@ -1978,14 +1969,6 @@ theorem append_eq_append_iff {ws xs ys zs : Array α} :
     · left; exact ⟨as.toList, by simp⟩
     · right; exact ⟨cs.toList, by simp⟩
 
-theorem append_eq_append_iff_of_size_eq_left {ws xs ys zs : Array α} (h : ws.size = xs.size) :
-    ws ++ ys = xs ++ zs ↔ ws = xs ∧ ys = zs := by
-  simpa [← Array.toList_inj] using List.append_eq_append_iff_of_size_eq_left h
-
-theorem append_eq_append_iff_of_size_eq_right {ws xs ys zs : Array α} (h : ys.size = zs.size) :
-    ws ++ ys = xs ++ zs ↔ ws = xs ∧ ys = zs := by
-  simpa [← Array.toList_inj] using List.append_eq_append_iff_of_size_eq_right h
-
 @[grind =] theorem set_append {xs ys : Array α} {i : Nat} {x : α} (h : i < (xs ++ ys).size) :
     (xs ++ ys).set i x =
       if h' : i < xs.size then
@@ -2517,6 +2500,10 @@ theorem flatMap_replicate {f : α → Array β} : (replicate n a).flatMap f = (r
   rw [← List.toArray_replicate, List.isEmpty_toArray]
   simp
 
+@[simp] theorem sum_replicate_nat {n : Nat} {a : Nat} : (replicate n a).sum = n * a := by
+  rw [← List.toArray_replicate, List.sum_toArray]
+  simp
+
 /-! ### Preliminaries about `swap` needed for `reverse`. -/
 
 @[grind =]
@@ -4302,31 +4289,19 @@ theorem getElem?_range {n : Nat} {i : Nat} : (Array.range n)[i]? = if i < n then
 /-! ### sum -/
 
 @[simp, grind =] theorem sum_empty [Add α] [Zero α] : (#[] : Array α).sum = 0 := rfl
-theorem sum_eq_foldr [Add α] [Zero α] {xs : Array α} :
-    xs.sum = xs.foldr (init := 0) (· + ·) :=
-  rfl
 
 -- Without further algebraic hypotheses, there's no useful `sum_push` lemma.
 
 @[simp, grind =]
-theorem sum_toList [Add α] [Zero α] {as : Array α} : as.toList.sum = as.sum := by
+theorem sum_eq_sum_toList [Add α] [Zero α] {as : Array α} : as.toList.sum = as.sum := by
   cases as
   simp [Array.sum, List.sum]
 
-@[deprecated sum_toList (since := "2026-01-14")]
-def sum_eq_sum_toList := @sum_toList
-
 @[simp, grind =]
-theorem sum_append [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
-    [Std.LeftIdentity (α := α) (· + ·) 0] [Std.LawfulLeftIdentity (α := α) (· + ·) 0]
-    {as₁ as₂ : Array α} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
-  simp [← sum_toList, List.sum_append]
-
-@[simp, grind =]
-theorem sum_reverse [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
-    [Std.Commutative (α := α) (· + ·)]
-    [Std.LawfulLeftIdentity (α := α) (· + ·) 0] (xs : Array α) : xs.reverse.sum = xs.sum := by
-  simp [← sum_toList, List.sum_reverse]
+theorem sum_append_nat {as₁ as₂ : Array Nat} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
+  cases as₁
+  cases as₂
+  simp [List.sum_append_nat]
 
 theorem foldl_toList_eq_flatMap {l : List α} {acc : Array β}
     {F : Array β → α → Array β} {G : α → List β}

src/Init/Data/Array/Nat.lean

@@ -1,39 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison, Sebastian Graf, Paul Reichert
--/
-module
-
-prelude
-public import Init.Data.Array.Lemmas
-import Init.Data.List.Nat.Sum
-
-public section
-
-set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-set_option linter.indexVariables true -- Enforce naming conventions for index variables.
-
-namespace Array
-
-protected theorem sum_pos_iff_exists_pos_nat {xs : Array Nat} : 0 < xs.sum ↔ ∃ x ∈ xs, 0 < x := by
-  simp [← sum_toList, List.sum_pos_iff_exists_pos_nat]
-
-protected theorem sum_eq_zero_iff_forall_eq_nat {xs : Array Nat} :
-    xs.sum = 0 ↔ ∀ x ∈ xs, x = 0 := by
-  simp [← sum_toList, List.sum_eq_zero_iff_forall_eq_nat]
-
-@[simp] theorem sum_replicate_nat {n : Nat} {a : Nat} : (replicate n a).sum = n * a := by
-  rw [← List.toArray_replicate, List.sum_toArray]
-  simp
-
-theorem sum_append_nat {as₁ as₂ : Array Nat} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
-  simp [sum_append]
-
-theorem sum_reverse_nat (xs : Array Nat) : xs.reverse.sum = xs.sum := by
-  simp [sum_reverse]
-
-theorem sum_eq_foldl_nat {xs : Array Nat} : xs.sum = xs.foldl (init := 0) (· + ·) := by
-  simp only [foldl_eq_foldr_reverse, Nat.add_comm, ← sum_eq_foldr, sum_reverse_nat]
-
-end Array

src/Init/Data/Array/OfFn.lean

@@ -53,11 +53,6 @@ theorem ofFn_succ' {f : Fin (n+1) → α} :
   apply Array.toList_inj.mp
   simp [List.ofFn_succ]
 
-@[simp]
-theorem ofFn_getElem {xs : Array α} :
-    Array.ofFn (fun i : Fin xs.size => xs[i.val]) = xs := by
-  ext <;> simp
-
 @[simp]
 theorem ofFn_eq_empty_iff {f : Fin n → α} : ofFn f = #[] ↔ n = 0 := by
   rw [← Array.toList_inj]
@@ -72,12 +67,6 @@ theorem mem_ofFn {n} {f : Fin n → α} {a : α} : a ∈ ofFn f ↔ ∃ i, f i =
   · rintro ⟨i, rfl⟩
     apply mem_of_getElem (i := i) <;> simp
 
-@[simp, grind =]
-theorem map_ofFn {f : Fin n → α} {g : α → β} :
-    (Array.ofFn f).map g = Array.ofFn (g ∘ f) := by
-  apply Array.ext_getElem?
-  simp [Array.getElem?_ofFn]
-
 /-! ### ofFnM -/
 
 /-- Construct (in a monadic context) an array by applying a monadic function to each index. -/

src/Init/Data/Bool.lean

@@ -636,7 +636,7 @@ def boolPredToPred : Coe (α → Bool) (α  → Prop) where
 This should not be turned on globally as an instance because it degrades performance in Mathlib,
 but may be used locally.
 -/
-@[expose, instance_reducible] def boolRelToRel : Coe (α → α → Bool) (α → α → Prop) where
+@[expose] def boolRelToRel : Coe (α → α → Bool) (α → α → Prop) where
   coe r := fun a b => Eq (r a b) true
 
 /-! ### subtypes -/

src/Init/Data/ByteArray/Lemmas.lean

@@ -286,21 +286,4 @@ theorem extract_zero_max_size {a : ByteArray} {i : Nat} : a.extract 0 (max i a.s
   ext1
   simp [Nat.le_max_right]
 
-theorem append_eq_append_iff_of_size_eq_left {ws xs ys zs : ByteArray} (h : ws.size = xs.size) :
-    ws ++ ys = xs ++ zs ↔ ws = xs ∧ ys = zs := by
-  simpa [ByteArray.ext_iff] using Array.append_eq_append_iff_of_size_eq_left h
-
-theorem append_eq_append_iff_of_size_eq_right {ws xs ys zs : ByteArray} (h : ys.size = zs.size) :
-    ws ++ ys = xs ++ zs ↔ ws = xs ∧ ys = zs := by
-  simpa [ByteArray.ext_iff] using Array.append_eq_append_iff_of_size_eq_right h
-
-@[simp]
-theorem size_push {bs : ByteArray} {b : UInt8} : (bs.push b).size = bs.size + 1 := by
-  rw [ByteArray.size, data_push, Array.size_push, ← ByteArray.size]
-
-theorem ext_getElem {a b : ByteArray} (h₀ : a.size = b.size) (h : ∀ (i : Nat) hi hi', a[i]'hi = b[i]'hi') : a = b := by
-  rw [ByteArray.ext_iff]
-  apply Array.ext (by simpa using h₀)
-  simpa [← ByteArray.getElem_eq_getElem_data]
-
 end ByteArray

src/Init/Data/Char/Lemmas.lean

@@ -48,7 +48,6 @@ instance ltTrans : Trans (· < · : Char → Char → Prop) (· < ·) (· < ·)
   trans := Char.lt_trans
 
 -- This instance is useful while setting up instances for `String`.
-@[instance_reducible]
 def notLTTrans : Trans (¬ · < · : Char → Char → Prop) (¬ · < ·) (¬ · < ·) where
   trans h₁ h₂ := by simpa using Char.le_trans (by simpa using h₂) (by simpa using h₁)
 

src/Init/Data/Fin/Lemmas.lean

@@ -118,7 +118,7 @@ For example, for `x : Fin k` and `n : Nat`,
 it causes `x < n` to be elaborated as `x < ↑n` rather than `↑x < n`,
 silently introducing wraparound arithmetic.
 -/
-@[expose, instance_reducible]
+@[expose]
 def instNatCast (n : Nat) [NeZero n] : NatCast (Fin n) where
   natCast a := Fin.ofNat n a
 
@@ -140,7 +140,7 @@ This is not a global instance, but may be activated locally via `open Fin.IntCas
 
 See the doc-string for `Fin.NatCast.instNatCast` for more details.
 -/
-@[expose, instance_reducible]
+@[expose]
 def instIntCast (n : Nat) [NeZero n] : IntCast (Fin n) where
   intCast := Fin.intCast
 

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

@@ -19,10 +19,6 @@ public section
 namespace Std
 open Std.Iterators
 
-@[simp]
-theorem IterM.run_toList_mk' {α : Type u} {β : Type u} [Std.Iterator α Id β] (a : α) :
-    (Std.IterM.mk' (m := Id) a).toList.run = (Std.Iter.mk a).toList := rfl
-
 theorem Iter.toArray_eq_toArray_toIterM {α β} [Iterator α Id β] [Finite α Id]
     {it : Iter (α := α) β} :
     it.toArray = it.toIterM.toArray.run :=

src/Init/Data/List.lean

@@ -20,7 +20,6 @@ public import Init.Data.List.MinMaxIdx
 public import Init.Data.List.MinMaxOn
 public import Init.Data.List.Monadic
 public import Init.Data.List.Nat
-public import Init.Data.List.Int
 public import Init.Data.List.Notation
 public import Init.Data.List.Pairwise
 public import Init.Data.List.Sublist

src/Init/Data/List/Basic.lean

@@ -2017,7 +2017,6 @@ def sum {α} [Add α] [Zero α] : List α → α :=
 
 @[simp, grind =] theorem sum_nil [Add α] [Zero α] : ([] : List α).sum = 0 := rfl
 @[simp, grind =] theorem sum_cons [Add α] [Zero α] {a : α} {l : List α} : (a::l).sum = a + l.sum := rfl
-theorem sum_eq_foldr [Add α] [Zero α] {l : List α} : l.sum = l.foldr (· + ·) 0 := rfl
 
 /-! ### range -/
 

src/Init/Data/List/Count.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Data.List.Sublist
-import Init.Grind.Util
 
 public section
 
@@ -98,18 +97,6 @@ theorem countP_le_length : countP p l ≤ l.length := by
 @[simp] theorem countP_eq_zero {p} : countP p l = 0 ↔ ∀ a ∈ l, ¬p a := by
   simp only [countP_eq_length_filter, length_eq_zero_iff, filter_eq_nil_iff]
 
-/-- This lemma is only relevant for `grind`. -/
-@[grind ←=]
-theorem _root_.Std.Internal.List.countP_eq_zero_of_forall {xs : List α} (h : ∀ x ∈ xs, ¬ p x) : xs.countP p = 0 :=
-  countP_eq_zero.mpr h
-
-/-- This lemma is only relevant for `grind`. -/
-theorem _root_.Std.Internal.List.not_of_countP_eq_zero_of_mem {xs : List α} (h : xs.countP p = 0) (h' : x ∈ xs) : ¬ p x :=
-   countP_eq_zero.mp h _ h'
-
-grind_pattern Std.Internal.List.not_of_countP_eq_zero_of_mem => xs.countP p, x ∈ xs where
-  guard xs.countP p = 0
-
 @[simp] theorem countP_eq_length {p} : countP p l = l.length ↔ ∀ a ∈ l, p a := by
   rw [countP_eq_length_filter, length_filter_eq_length_iff]
 

src/Init/Data/List/Int.lean

@@ -1,9 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Paul Reichert
--/
-module
-
-prelude
-public import Init.Data.List.Int.Sum

src/Init/Data/List/Int/Sum.lean

@@ -1,107 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison, Sebastian Graf, Paul Reichert
--/
-module
-
-prelude
-public import Init.Data.Int.DivMod.Bootstrap
-import Init.Data.Int.DivMod.Lemmas
-import Init.Data.List.MinMax
-
-public section
-
-set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-set_option linter.indexVariables true -- Enforce naming conventions for index variables.
-
-namespace List
-
-@[simp]
-theorem sum_replicate_int {n : Nat} {a : Int} : (replicate n a).sum = n * a := by
-  induction n <;> simp_all [replicate_succ, Int.add_mul, Int.add_comm]
-
-theorem sum_append_int {l₁ l₂ : List Int} : (l₁ ++ l₂).sum = l₁.sum + l₂.sum := by
-  simp [sum_append]
-
-theorem sum_reverse_int (xs : List Int) : xs.reverse.sum = xs.sum := by
-  simp [sum_reverse]
-
-theorem min_mul_length_le_sum_int {xs : List Int} (h : xs ≠ []) :
-    xs.min h * xs.length ≤ xs.sum := by
-  induction xs
-  · contradiction
-  · rename_i x xs ih
-    cases xs
-    · simp_all [List.min_singleton]
-    · simp only [ne_eq, reduceCtorEq, not_false_eq_true, min_eq_get_min?,
-      List.min?_cons (α := Int), Option.get_some, length_cons, Int.natCast_add, Int.cast_ofNat_Int,
-      forall_const] at ih ⊢
-      rw [Int.mul_add, Int.mul_one, Int.add_comm]
-      apply Int.add_le_add
-      · apply Int.min_le_left
-      · refine Int.le_trans ?_ ih
-        rw [Int.mul_le_mul_right (by omega)]
-        apply Int.min_le_right
-
-theorem mul_length_le_sum_of_min?_eq_some_int {xs : List Int} (h : xs.min? = some x) :
-    x * xs.length ≤ xs.sum := by
-  cases xs
-  · simp_all
-  · simp only [min?_eq_some_min (cons_ne_nil _ _), Option.some.injEq] at h
-    simpa [← h] using min_mul_length_le_sum_int _
-
-theorem min_le_sum_div_length_int {xs : List Int} (h : xs ≠ []) :
-    xs.min h ≤ xs.sum / xs.length := by
-  have := min_mul_length_le_sum_int h
-  rwa [Int.le_ediv_iff_mul_le]
-  simp [List.length_pos_iff, h]
-
-theorem le_sum_div_length_of_min?_eq_some_int {xs : List Int} (h : xs.min? = some x) :
-    x ≤ xs.sum / xs.length := by
-  cases xs
-  · simp_all
-  · simp only [min?_eq_some_min (cons_ne_nil _ _), Option.some.injEq] at h
-    simpa [← h] using min_le_sum_div_length_int _
-
-theorem sum_le_max_mul_length_int {xs : List Int} (h : xs ≠ []) :
-    xs.sum ≤ xs.max h * xs.length := by
-  induction xs
-  · contradiction
-  · rename_i x xs ih
-    cases xs
-    · simp_all [List.max_singleton]
-    · simp only [ne_eq, reduceCtorEq, not_false_eq_true, max_eq_get_max?,
-      List.max?_cons (α := Int), Option.get_some, length_cons, Int.natCast_add, Int.cast_ofNat_Int,
-      forall_const] at ih ⊢
-      rw [Int.mul_add, Int.mul_one, Int.add_comm]
-      apply Int.add_le_add
-      · apply Int.le_max_left
-      · refine Int.le_trans ih ?_
-        rw [Int.mul_le_mul_right (by omega)]
-        apply Int.le_max_right
-
-theorem sum_le_max_mul_length_of_max?_eq_some_int {xs : List Int} (h : xs.max? = some x) :
-    xs.sum ≤ x * xs.length := by
-  cases xs
-  · simp_all
-  · simp only [max?_eq_some_max (cons_ne_nil _ _), Option.some.injEq] at h
-    simpa [← h] using sum_le_max_mul_length_int _
-
-theorem sum_div_length_le_max_int {xs : List Int} (h : xs ≠ []) :
-    xs.sum / xs.length ≤ xs.max h := by
-  have := sum_le_max_mul_length_int h
-  rw [Int.ediv_le_iff_le_mul]
-  · refine Int.lt_of_le_of_lt this ?_
-    apply Int.lt_add_of_pos_right
-    simp [← Nat.ne_zero_iff_zero_lt, h]
-  · simp [List.length_pos_iff, h]
-
-theorem sum_div_length_le_max_of_max?_eq_some_int {xs : List Int} (h : xs.max? = some x) :
-    xs.sum / xs.length ≤ x := by
-  cases xs
-  · simp_all
-  · simp only [max?_eq_some_max (cons_ne_nil _ _), Option.some.injEq] at h
-    simpa [← h] using sum_div_length_le_max_int _
-
-end List

src/Init/Data/List/Lemmas.lean

@@ -482,28 +482,25 @@ theorem mem_iff_getElem {a} {l : List α} : a ∈ l ↔ ∃ (i : Nat) (h : i < l
 theorem mem_iff_getElem? {a} {l : List α} : a ∈ l ↔ ∃ i : Nat, l[i]? = some a := by
   simp [getElem?_eq_some_iff, mem_iff_getElem]
 
-theorem exists_mem_iff_exists_getElem {P : α → Prop} {l : List α} :
-    (∃ x ∈ l, P x) ↔ ∃ (i : Nat), ∃ hi, P (l[i]) := by
-  simp only [mem_iff_getElem]
-  apply Iff.intro
-  · rintro ⟨_, ⟨i, hi, rfl⟩, hP⟩
-    exact ⟨i, hi, hP⟩
-  · rintro ⟨i, hi, hP⟩
-    exact ⟨_, ⟨i, hi, rfl⟩, hP⟩
-
-theorem forall_mem_iff_forall_getElem {P : α → Prop} {l : List α} :
-    (∀ x ∈ l, P x) ↔ ∀ (i : Nat) hi, P (l[i]) := by
-  simp only [mem_iff_getElem]
-  apply Iff.intro
-  · intro h i hi
-    exact h l[i] ⟨i, hi, rfl⟩
-  · rintro h _ ⟨i, hi, rfl⟩
-    exact h i hi
-
-@[deprecated forall_mem_iff_forall_getElem (since := "2026-01-29")]
 theorem forall_getElem {l : List α} {p : α → Prop} :
-    (∀ (i : Nat) h, p (l[i]'h)) ↔ ∀ a, a ∈ l → p a :=
-  forall_mem_iff_forall_getElem.symm
+    (∀ (i : Nat) h, p (l[i]'h)) ↔ ∀ a, a ∈ l → p a := by
+  induction l with
+  | nil => simp
+  | cons a l ih =>
+    simp only [length_cons, mem_cons, forall_eq_or_imp]
+    constructor
+    · intro w
+      constructor
+      · exact w 0 (by simp)
+      · apply ih.1
+        intro n h
+        simpa using w (n+1) (Nat.add_lt_add_right h 1)
+    · rintro ⟨h, w⟩
+      rintro (_ | n) h
+      · simpa
+      · apply w
+        simp only [getElem_cons_succ]
+        exact getElem_mem (lt_of_succ_lt_succ h)
 
 @[simp] theorem elem_eq_contains [BEq α] {a : α} {l : List α} :
     elem a l = l.contains a := by
@@ -1830,17 +1827,12 @@ theorem append_eq_map_iff {f : α → β} :
   rw [eq_comm, map_eq_append_iff]
 
 @[simp, grind =]
-theorem sum_append [Add α] [Zero α] [Std.LawfulLeftIdentity (α := α) (· + ·) 0]
-    [Std.Associative (α := α) (· + ·)] {l₁ l₂ : List α} : (l₁ ++ l₂).sum = l₁.sum + l₂.sum := by
-  induction l₁ generalizing l₂ <;> simp_all [Std.Associative.assoc, Std.LawfulLeftIdentity.left_id]
+theorem sum_append_nat {l₁ l₂ : List Nat} : (l₁ ++ l₂).sum = l₁.sum + l₂.sum := by
+  induction l₁ generalizing l₂ <;> simp_all [Nat.add_assoc]
 
 @[simp, grind =]
-theorem sum_reverse [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
-    [Std.Commutative (α := α) (· + ·)]
-    [Std.LawfulLeftIdentity (α := α) (· + ·) 0] (xs : List α) : xs.reverse.sum = xs.sum := by
-  induction xs <;>
-    simp_all [sum_append, Std.Commutative.comm (α := α) _ 0,
-      Std.LawfulLeftIdentity.left_id, Std.Commutative.comm]
+theorem sum_reverse_nat (xs : List Nat) : xs.reverse.sum = xs.sum := by
+  induction xs <;> simp_all [Nat.add_comm]
 
 /-! ### concat
 
@@ -2371,6 +2363,9 @@ theorem replicateRecOn {α : Type _} {p : List α → Prop} (l : List α)
     exact hi _ _ _ _ h hn (replicateRecOn (b :: l') h0 hr hi)
 termination_by l.length
 
+@[simp] theorem sum_replicate_nat {n : Nat} {a : Nat} : (replicate n a).sum = n * a := by
+  induction n <;> simp_all [replicate_succ, Nat.add_mul, Nat.add_comm]
+
 /-! ### reverse -/
 
 @[simp, grind =] theorem length_reverse {as : List α} : (as.reverse).length = as.length := by

src/Init/Data/List/MinMax.lean

@@ -47,7 +47,7 @@ theorem min?_cons' [Min α] {xs : List α} : (x :: xs).min? = some (foldl min x
   cases xs <;> simp [min?]
 
 @[simp, grind =]
-public theorem isSome_min?_iff [Min α] {xs : List α} : xs.min?.isSome ↔ xs ≠ [] := by
+public theorem isSome_min?_iff {xs : List α} [Min α] : xs.min?.isSome ↔ xs ≠ [] := by
   cases xs <;> simp [min?]
 
 @[grind .]
@@ -55,8 +55,8 @@ theorem isSome_min?_of_mem {l : List α} [Min α] {a : α} (h : a ∈ l) :
     l.min?.isSome := by
   cases l <;> simp_all [min?_cons']
 
-theorem isSome_min?_of_ne_nil [Min α] {l : List α} (hl : l ≠ []) : l.min?.isSome := by
-  rwa [isSome_min?_iff]
+theorem isSome_min?_of_ne_nil [Min α] : {l : List α} → (hl : l ≠ []) → l.min?.isSome
+  | x::xs, h => by simp [min?_cons']
 
 theorem min?_eq_head? {α : Type u} [Min α] {l : List α}
     (h : l.Pairwise (fun a b => min a b = a)) : l.min? = l.head? := by
@@ -242,7 +242,7 @@ theorem max?_cons' [Max α] {xs : List α} : (x :: xs).max? = some (foldl max x
   cases xs <;> simp [max?]
 
 @[simp, grind =]
-public theorem isSome_max?_iff [Max α] {xs : List α} : xs.max?.isSome ↔ xs ≠ [] := by
+public theorem isSome_max?_iff {xs : List α} [Max α] : xs.max?.isSome ↔ xs ≠ [] := by
   cases xs <;> simp [max?]
 
 @[grind .]
@@ -250,8 +250,8 @@ theorem isSome_max?_of_mem {l : List α} [Max α] {a : α} (h : a ∈ l) :
     l.max?.isSome := by
   cases l <;> simp_all [max?_cons']
 
-theorem isSome_max?_of_ne_nil [Max α] {l : List α} (hl : l ≠ []) : l.max?.isSome := by
-  rwa [isSome_max?_iff]
+theorem isSome_max?_of_ne_nil [Max α] : {l : List α} → (hl : l ≠ []) → l.max?.isSome
+  | x::xs, h => by simp [max?_cons']
 
 theorem max?_eq_head? {α : Type u} [Max α] {l : List α}
     (h : l.Pairwise (fun a b => max a b = a)) : l.max? = l.head? := by

src/Init/Data/List/MinMaxOn.lean

@@ -130,7 +130,7 @@ protected theorem apply_minOn_le_of_mem [LE β] [DecidableLE β] [IsLinearPreord
   | x :: xs =>
     fun_induction xs.foldl (init := x) (_root_.minOn f) generalizing y
     · simp only [mem_cons] at hx
-      simp_all
+      simp_all [le_refl _]
     · rename_i x y _ ih
       simp at ih ⊢
       rcases mem_cons.mp hx with rfl | hx

src/Init/Data/List/Nat.lean

@@ -12,7 +12,6 @@ public import Init.Data.List.Nat.Range
 public import Init.Data.List.Nat.Sublist
 public import Init.Data.List.Nat.TakeDrop
 public import Init.Data.List.Nat.Count
-public import Init.Data.List.Nat.Sum
 public import Init.Data.List.Nat.Erase
 public import Init.Data.List.Nat.Find
 public import Init.Data.List.Nat.BEq

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

@@ -254,18 +254,4 @@ theorem le_max?_getD_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
     a ≤ l.max?.getD k :=
   Option.get_eq_getD _ ▸ le_max?_get_of_mem h
 
-/-! #### append -/
-
-theorem append_eq_append_iff_of_size_eq_left {ws xs ys zs : List α}
-    (h : ws.length = xs.length) : ws ++ ys = xs ++ zs ↔ ws = xs ∧ ys = zs := by
-  rw [append_eq_append_iff]
-  refine ⟨?_, ?_⟩
-  · rintro (⟨as, rfl, rfl⟩|⟨as, rfl, rfl⟩) <;> simp_all
-  · rintro ⟨rfl, rfl⟩ <;> simp_all
-
-theorem append_eq_append_iff_of_size_eq_right {ws xs ys zs : List α}
-    (h : ys.length = zs.length) : ws ++ ys = xs ++ zs ↔ ws = xs ∧ ys = zs := by
-  rw [← reverse_inj, reverse_append, reverse_append,
-    append_eq_append_iff_of_size_eq_left (by simpa), reverse_inj, reverse_inj, and_comm]
-
 end List

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

@@ -13,6 +13,13 @@ public section
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
+protected theorem Nat.sum_pos_iff_exists_pos {l : List Nat} : 0 < l.sum ↔ ∃ x ∈ l, 0 < x := by
+  induction l with
+  | nil => simp
+  | cons x xs ih =>
+    simp [← ih]
+    omega
+
 namespace List
 
 open Nat

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

@@ -1,128 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison, Sebastian Graf, Paul Reichert
--/
-module
-
-prelude
-public import Init.Data.Int.DivMod.Bootstrap
-import Init.Data.Int.DivMod.Lemmas
-import Init.Data.List.MinMax
-
-public section
-
-set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-set_option linter.indexVariables true -- Enforce naming conventions for index variables.
-
-namespace List
-
-protected theorem sum_pos_iff_exists_pos_nat {l : List Nat} : 0 < l.sum ↔ ∃ x ∈ l, 0 < x := by
-  induction l with
-  | nil => simp
-  | cons x xs ih =>
-    simp [← ih]
-    omega
-
-@[deprecated List.sum_pos_iff_exists_pos_nat (since := "2025-01-15")]
-protected def _root_.Nat.sum_pos_iff_exists_pos := @List.sum_pos_iff_exists_pos_nat
-
-protected theorem sum_eq_zero_iff_forall_eq_nat {xs : List Nat} :
-    xs.sum = 0 ↔ ∀ x ∈ xs, x = 0 := by
-  rw [← Decidable.not_iff_not]
-  simp [← Nat.pos_iff_ne_zero, List.sum_pos_iff_exists_pos_nat]
-
-@[deprecated List.sum_pos_iff_exists_pos_nat (since := "2025-01-15")]
-protected def _root_.Nat.sum_eq_zero_iff_forall_eq := @List.sum_eq_zero_iff_forall_eq_nat
-
-@[simp]
-theorem sum_replicate_nat {n : Nat} {a : Nat} : (replicate n a).sum = n * a := by
-  induction n <;> simp_all [replicate_succ, Nat.add_mul, Nat.add_comm]
-
-theorem sum_append_nat {l₁ l₂ : List Nat} : (l₁ ++ l₂).sum = l₁.sum + l₂.sum := by
-  simp [sum_append]
-
-theorem sum_reverse_nat (xs : List Nat) : xs.reverse.sum = xs.sum := by
-  simp [sum_reverse]
-
-theorem sum_eq_foldl_nat {xs : List Nat} : xs.sum = xs.foldl (init := 0) (· + ·) := by
-  simp only [foldl_eq_foldr_reverse, Nat.add_comm, ← sum_eq_foldr, sum_reverse_nat]
-
-theorem min_mul_length_le_sum_nat {xs : List Nat} (h : xs ≠ []) :
-    xs.min h * xs.length ≤ xs.sum := by
-  induction xs
-  · contradiction
-  · rename_i x xs ih
-    cases xs
-    · simp_all [List.min_singleton]
-    · simp only [ne_eq, reduceCtorEq, not_false_eq_true, min_eq_get_min?,
-      List.min?_cons (α := Nat), Option.get_some, length_cons,
-      forall_const] at ih ⊢
-      rw [Nat.mul_add, Nat.mul_one, Nat.add_comm]
-      apply Nat.add_le_add
-      · apply Nat.min_le_left
-      · refine Nat.le_trans ?_ ih
-        rw [Nat.mul_le_mul_right_iff (by omega)]
-        apply Nat.min_le_right
-
-theorem mul_length_le_sum_of_min?_eq_some_nat {xs : List Nat} (h : xs.min? = some x) :
-    x * xs.length ≤ xs.sum := by
-  cases xs
-  · simp_all
-  · simp only [min?_eq_some_min (cons_ne_nil _ _), Option.some.injEq] at h
-    simpa [← h] using min_mul_length_le_sum_nat _
-
-theorem min_le_sum_div_length_nat {xs : List Nat} (h : xs ≠ []) :
-    xs.min h ≤ xs.sum / xs.length := by
-  have := min_mul_length_le_sum_nat h
-  rwa [Nat.le_div_iff_mul_le]
-  simp [List.length_pos_iff, h]
-
-theorem le_sum_div_length_of_min?_eq_some_nat {xs : List Nat} (h : xs.min? = some x) :
-    x ≤ xs.sum / xs.length := by
-  cases xs
-  · simp_all
-  · simp only [min?_eq_some_min (cons_ne_nil _ _), Option.some.injEq] at h
-    simpa [← h] using min_le_sum_div_length_nat _
-
-theorem sum_le_max_mul_length_nat {xs : List Nat} (h : xs ≠ []) :
-    xs.sum ≤ xs.max h * xs.length := by
-  induction xs
-  · contradiction
-  · rename_i x xs ih
-    cases xs
-    · simp_all [List.max_singleton]
-    · simp only [ne_eq, reduceCtorEq, not_false_eq_true, max_eq_get_max?,
-      List.max?_cons (α := Nat), Option.get_some, length_cons,
-      forall_const, Option.elim_some] at ih ⊢
-      rw [Nat.mul_add, Nat.mul_one, Nat.add_comm]
-      apply Nat.add_le_add
-      · apply Nat.le_max_left
-      · refine Nat.le_trans ih ?_
-        rw [Nat.mul_le_mul_right_iff (by omega)]
-        apply Nat.le_max_right
-
-theorem sum_le_max_mul_length_of_max?_eq_some_nat {xs : List Nat} (h : xs.max? = some x) :
-    xs.sum ≤ x * xs.length := by
-  cases xs
-  · simp_all
-  · simp only [max?_eq_some_max (cons_ne_nil _ _), Option.some.injEq] at h
-    simp only [← h]
-    apply sum_le_max_mul_length_nat
-
-theorem sum_div_length_le_max_nat {xs : List Nat} (h : xs ≠ []) :
-    xs.sum / xs.length ≤ xs.max h := by
-  have := sum_le_max_mul_length_nat h
-  rw [Nat.div_le_iff_le_mul, Nat.add_sub_assoc]
-  · exact Nat.le_trans this (Nat.le_add_right _ _)
-  · simp [Nat.one_le_iff_ne_zero, h]
-  · simp [← Nat.ne_zero_iff_zero_lt, h]
-
-theorem sum_div_length_le_max_of_max?_eq_some_nat {xs : List Nat} (h : xs.max? = some x) :
-    xs.sum / xs.length ≤ x := by
-  cases xs
-  · simp_all
-  · simp only [max?_eq_some_max (cons_ne_nil _ _), Option.some.injEq] at h
-    simpa only [← h] using sum_div_length_le_max_nat _
-
-end List

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

@@ -137,7 +137,6 @@ theorem take_append {l₁ l₂ : List α} {i : Nat} :
       congr 1
       omega
 
-@[grind =]
 theorem take_append_of_le_length {l₁ l₂ : List α} {i : Nat} (h : i ≤ l₁.length) :
     (l₁ ++ l₂).take i = l₁.take i := by
   simp [take_append, Nat.sub_eq_zero_of_le h]
@@ -373,7 +372,7 @@ theorem drop_take : ∀ {i j : Nat} {l : List α}, drop i (take j l) = take (j -
     simp only [take_succ_cons, drop_succ_cons, drop_take, take_eq_take_iff, length_drop]
     omega
 
-@[simp, grind =] theorem drop_take_self : drop i (take i l) = [] := by
+@[simp] theorem drop_take_self : drop i (take i l) = [] := by
   rw [drop_take]
   simp
 

src/Init/Data/List/OfFn.lean

@@ -100,11 +100,6 @@ theorem ofFn_add {n m} {f : Fin (n + m) → α} :
 theorem ofFn_eq_nil_iff {f : Fin n → α} : ofFn f = [] ↔ n = 0 := by
   cases n <;> simp only [ofFn_zero, ofFn_succ, Nat.succ_ne_zero, reduceCtorEq]
 
-@[simp]
-theorem ofFn_getElem {xs : List α} :
-    List.ofFn (fun i : Fin xs.length => xs[i.val]) = xs := by
-  apply ext_getElem <;> simp
-
 @[simp 500, grind =]
 theorem mem_ofFn {n} {f : Fin n → α} {a : α} : a ∈ ofFn f ↔ ∃ i, f i = a := by
   constructor
@@ -114,12 +109,6 @@ theorem mem_ofFn {n} {f : Fin n → α} {a : α} : a ∈ ofFn f ↔ ∃ i, f i =
   · rintro ⟨i, rfl⟩
     apply mem_of_getElem (i := i) <;> simp
 
-@[simp, grind =]
-theorem map_ofFn {f : Fin n → α} {g : α → β} :
-    (List.ofFn f).map g = List.ofFn (g ∘ f) := by
-  apply List.ext_getElem?
-  simp [List.getElem?_ofFn]
-
 @[grind =] theorem head_ofFn {n} {f : Fin n → α} (h : ofFn f ≠ []) :
     (ofFn f).head h = f ⟨0, Nat.pos_of_ne_zero (mt ofFn_eq_nil_iff.2 h)⟩ := by
   rw [← getElem_zero (length_ofFn ▸ Nat.pos_of_ne_zero (mt ofFn_eq_nil_iff.2 h)),

src/Init/Data/List/Sublist.lean

@@ -580,7 +580,7 @@ theorem sublist_flatten_iff {L : List (List α)} {l} :
     · rintro ⟨L', rfl, h⟩
       simp only [flatten_nil, sublist_nil, flatten_eq_nil_iff]
       simp only [getElem?_nil, Option.getD_none, sublist_nil] at h
-      exact (forall_mem_iff_forall_getElem (P := (· = []))).2 h
+      exact (forall_getElem (p := (· = []))).1 h
   | cons l' L ih =>
     simp only [flatten_cons, sublist_append_iff, ih]
     constructor
@@ -1124,11 +1124,9 @@ theorem drop_subset (i) (l : List α) : drop i l ⊆ l :=
 
 grind_pattern drop_subset => drop i l ⊆ l
 
-@[grind →]
 theorem mem_of_mem_take {l : List α} (h : a ∈ l.take i) : a ∈ l :=
   take_subset _ _ h
 
-@[grind →]
 theorem mem_of_mem_drop {i} {l : List α} (h : a ∈ l.drop i) : a ∈ l :=
   drop_subset _ _ h
 

src/Init/Data/Option/Lemmas.lean

@@ -883,10 +883,6 @@ theorem guard_or_guard : (guard p a).or (guard q a) = guard (fun x => p x || q x
   simp only [guard]
   split <;> simp_all
 
-theorem any_or_of_any_left {o₁ o₂ : Option α} {f : α → Bool} (h : o₁.any f) :
-    (o₁.or o₂).any f := by
-  cases o₁ <;> simp_all
-
 /-! ### `orElse` -/
 
 /-- The `simp` normal form of `o <|> o'` is `o.or o'` via `orElse_eq_orElse` and `orElse_eq_or`. -/

src/Init/Data/Ord/Basic.lean

@@ -609,22 +609,21 @@ protected theorem compare_nil_right_eq_eq {α} [Ord α] {xs : List α} :
 end List
 
 /-- The lexicographic order on pairs. -/
-@[expose, instance_reducible]
-def lexOrd [Ord α] [Ord β] : Ord (α × β) where
+@[expose] def lexOrd [Ord α] [Ord β] : Ord (α × β) where
   compare := compareLex (compareOn (·.1)) (compareOn (·.2))
 
 /--
 Constructs an `BEq` instance from an `Ord` instance that asserts that the result of `compare` is
 `Ordering.eq`.
 -/
-@[expose, instance_reducible] def beqOfOrd [Ord α] : BEq α where
+@[expose] def beqOfOrd [Ord α] : BEq α where
   beq a b := (compare a b).isEq
 
 /--
 Constructs an `LT` instance from an `Ord` instance that asserts that the result of `compare` is
 `Ordering.lt`.
 -/
-@[expose, instance_reducible] def ltOfOrd [Ord α] : LT α where
+@[expose] def ltOfOrd [Ord α] : LT α where
   lt a b := compare a b = Ordering.lt
 
 @[inline]

src/Init/Data/Order/Factories.lean

@@ -23,7 +23,7 @@ preferring `a` over `b` when in doubt.
 
 Has a `LawfulOrderLeftLeaningMin α` instance.
 -/
-@[inline, instance_reducible]
+@[inline]
 public def _root_.Min.leftLeaningOfLE (α : Type u) [LE α] [DecidableLE α] : Min α where
   min a b := if a ≤ b then a else b
 
@@ -33,7 +33,7 @@ preferring `a` over `b` when in doubt.
 
 Has a `LawfulOrderLeftLeaningMax α` instance.
 -/
-@[inline, instance_reducible]
+@[inline]
 public def _root_.Max.leftLeaningOfLE (α : Type u) [LE α] [DecidableLE α] : Max α where
   max a b := if b ≤ a then a else b
 

src/Init/Data/Order/FactoriesExtra.lean

@@ -18,7 +18,7 @@ Creates an `LE α` instance from an `Ord α` instance.
 `OrientedOrd α` must be satisfied so that the resulting `LE α` instance faithfully represents
 the `Ord α` instance.
 -/
-@[inline, expose, instance_reducible]
+@[inline, expose]
 public def _root_.LE.ofOrd (α : Type u) [Ord α] : LE α where
   le a b := (compare a b).isLE
 
@@ -38,7 +38,7 @@ Creates an `LT α` instance from an `Ord α` instance.
 `OrientedOrd α` must be satisfied so that the resulting `LT α` instance faithfully represents
 the `Ord α` instance.
 -/
-@[inline, expose, instance_reducible]
+@[inline, expose]
 public def _root_.LT.ofOrd (α : Type u) [Ord α] :
     LT α where
   lt a b := compare a b = .lt
@@ -82,7 +82,7 @@ public def _root_.DecidableLT.ofOrd (α : Type u) [LE α] [LT α] [Ord α] [Lawf
 
 /--
 Creates a `BEq α` instance from an `Ord α` instance. -/
-@[inline, expose, instance_reducible]
+@[inline, expose]
 public def _root_.BEq.ofOrd (α : Type u) [Ord α] :
     BEq α where
   beq a b := compare a b = .eq

src/Init/Data/Order/Lemmas.lean

@@ -90,13 +90,9 @@ end AxiomaticInstances
 
 section LE
 
-@[simp]
 public theorem le_refl {α : Type u} [LE α] [Refl (α := α) (· ≤ ·)] (a : α) : a ≤ a := by
   simp [Refl.refl]
 
-public theorem le_of_eq [LE α] [Refl (α := α) (· ≤ ·)] {a b : α} : a = b → a ≤ b :=
-  (· ▸ le_refl _)
-
 public theorem le_antisymm {α : Type u} [LE α] [Std.Antisymm (α := α) (· ≤ ·)] {a b : α}
     (hab : a ≤ b) (hba : b ≤ a) : a = b :=
   Antisymm.antisymm _ _ hab hba
@@ -230,18 +226,6 @@ public theorem lt_of_le_of_ne {α : Type u} [LE α] [LT α]
   intro hge
   exact hne.elim <| Std.Antisymm.antisymm a b hle hge
 
-public theorem ne_of_lt {α : Type u} [LT α] [Std.Irrefl (α := α) (· < ·)] {a b : α} : a < b → a ≠ b :=
-  fun h h' => absurd (h' ▸ h) (h' ▸ lt_irrefl)
-
-public theorem le_iff_lt_or_eq [LE α] [LT α] [LawfulOrderLT α] [IsPartialOrder α] {a b : α} :
-    a ≤ b ↔ a < b ∨ a = b := by
-  refine ⟨fun h => ?_, fun h => h.elim le_of_lt le_of_eq⟩
-  simp [Classical.or_iff_not_imp_left, Std.lt_iff_le_and_not_ge, h, ← Std.le_antisymm_iff]
-
-public theorem lt_iff_le_and_ne [LE α] [LT α] [LawfulOrderLT α] [IsPartialOrder α] {a b : α} :
-    a < b ↔ a ≤ b ∧ a ≠ b := by
-  simpa [le_iff_lt_or_eq, or_and_right] using Std.ne_of_lt
-
 end LT
 end Std
 

src/Init/Data/Order/LemmasExtra.lean

@@ -66,7 +66,7 @@ public theorem compare_eq_eq_iff_eq {α : Type u} [Ord α] [LawfulEqOrd α] {a b
 
 public theorem IsLinearPreorder.of_ord {α : Type u} [LE α] [Ord α] [LawfulOrderOrd α]
     [TransOrd α] : IsLinearPreorder α where
-  le_refl a := by simp
+  le_refl a := by simp [← isLE_compare]
   le_trans a b c := by simpa [← isLE_compare] using TransOrd.isLE_trans
   le_total a b := Total.total a b
 

src/Init/Data/Order/PackageFactories.lean

@@ -663,7 +663,7 @@ public def LinearPreorderPackage.ofOrd (α : Type u)
         isGE_compare]
     decidableLE := args.decidableLE
     decidableLT := args.decidableLT
-    le_refl a := by simp
+    le_refl a := by simp [← isLE_compare]
     le_total a b := by cases h : compare a b <;> simp [h, ← isLE_compare (a := a), ← isGE_compare (a := a)]
     le_trans a b c := by simpa [← isLE_compare] using TransOrd.isLE_trans }
 

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

@@ -240,9 +240,6 @@ This propositional typeclass ensures that `UpwardEnumerable.succ?` will never re
 In other words, it ensures that there will always be a successor.
 -/
 class InfinitelyUpwardEnumerable (α : Type u) [UpwardEnumerable α] where
-  /--
-  Every element of `α` has a successor.
-  -/
   isSome_succ? : ∀ a : α, (UpwardEnumerable.succ? a).isSome
 
 /--

src/Init/Data/SInt/Basic.lean

@@ -409,7 +409,7 @@ Examples:
  * `(if (5 : Int8) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : Int8) < 7) by decide`
 -/
-@[extern "lean_int8_dec_lt", instance_reducible]
+@[extern "lean_int8_dec_lt"]
 def Int8.decLt (a b : Int8) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
 
@@ -425,7 +425,7 @@ Examples:
  * `(if (15 : Int8) ≤ 5 then "yes" else "no") = "no"`
  * `show (7 : Int8) ≤ 7 by decide`
 -/
-@[extern "lean_int8_dec_le", instance_reducible]
+@[extern "lean_int8_dec_le"]
 def Int8.decLe (a b : Int8) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
@@ -778,7 +778,7 @@ Examples:
  * `(if (5 : Int16) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : Int16) < 7) by decide`
 -/
-@[extern "lean_int16_dec_lt", instance_reducible]
+@[extern "lean_int16_dec_lt"]
 def Int16.decLt (a b : Int16) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
 
@@ -794,7 +794,7 @@ Examples:
  * `(if (15 : Int16) ≤ 5 then "yes" else "no") = "no"`
  * `show (7 : Int16) ≤ 7 by decide`
 -/
-@[extern "lean_int16_dec_le", instance_reducible]
+@[extern "lean_int16_dec_le"]
 def Int16.decLe (a b : Int16) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
@@ -1163,7 +1163,7 @@ Examples:
  * `(if (5 : Int32) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : Int32) < 7) by decide`
 -/
-@[extern "lean_int32_dec_lt", instance_reducible]
+@[extern "lean_int32_dec_lt"]
 def Int32.decLt (a b : Int32) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
 
@@ -1179,7 +1179,7 @@ Examples:
  * `(if (15 : Int32) ≤ 5 then "yes" else "no") = "no"`
  * `show (7 : Int32) ≤ 7 by decide`
 -/
-@[extern "lean_int32_dec_le", instance_reducible]
+@[extern "lean_int32_dec_le"]
 def Int32.decLe (a b : Int32) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
@@ -1568,7 +1568,7 @@ Examples:
  * `(if (5 : Int64) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : Int64) < 7) by decide`
 -/
-@[extern "lean_int64_dec_lt", instance_reducible]
+@[extern "lean_int64_dec_lt"]
 def Int64.decLt (a b : Int64) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
 /--
@@ -1583,7 +1583,7 @@ Examples:
  * `(if (15 : Int64) ≤ 5 then "yes" else "no") = "no"`
  * `show (7 : Int64) ≤ 7 by decide`
 -/
-@[extern "lean_int64_dec_le", instance_reducible]
+@[extern "lean_int64_dec_le"]
 def Int64.decLe (a b : Int64) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
@@ -1958,7 +1958,7 @@ Examples:
  * `(if (5 : ISize) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : ISize) < 7) by decide`
 -/
-@[extern "lean_isize_dec_lt", instance_reducible]
+@[extern "lean_isize_dec_lt"]
 def ISize.decLt (a b : ISize) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
 
@@ -1974,7 +1974,7 @@ Examples:
  * `(if (15 : ISize) ≤ 5 then "yes" else "no") = "no"`
  * `show (7 : ISize) ≤ 7 by decide`
 -/
-@[extern "lean_isize_dec_le", instance_reducible]
+@[extern "lean_isize_dec_le"]
 def ISize.decLe (a b : ISize) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 

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

@@ -61,7 +61,7 @@ instance SubarrayIterator.instFinite : Finite (SubarrayIterator α) Id :=
 
 instance [Monad m] : IteratorLoop (SubarrayIterator α) Id m := .defaultImplementation
 
-@[inline, expose, instance_reducible]
+@[inline, expose]
 def Subarray.instToIterator :=
   ToIterator.of (γ := Slice (Internal.SubarrayData α)) (β := α) (SubarrayIterator α) (⟨⟨·⟩⟩)
 attribute [instance] Subarray.instToIterator

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

@@ -24,7 +24,7 @@ open Std Slice PRange Iterators
 
 variable {α : Type u}
 
-@[inline, expose, instance_reducible]
+@[inline, expose]
 def ListSlice.instToIterator :=
   ToIterator.of (γ := Slice (Internal.ListSliceData α)) _ (fun s => match s.internalRepresentation.stop with
       | some n => s.internalRepresentation.list.iter.take n

src/Init/Data/String.lean

@@ -25,5 +25,4 @@ public import Init.Data.String.Termination
 public import Init.Data.String.ToSlice
 public import Init.Data.String.Search
 public import Init.Data.String.Legacy
-public import Init.Data.String.OrderInstances
-public import Init.Data.String.FindPos
+public import Init.Data.String.Grind

src/Init/Data/String/Basic.lean

@@ -1740,6 +1740,38 @@ theorem Pos.copy_toSlice_eq_cast {s : String} (p : s.Pos) :
     p.toSlice.copy = p.cast copy_toSlice.symm :=
   Pos.ext (by simp)
 
+/-- Given a byte position within a string slice, obtains the smallest valid position that is
+strictly greater than the given byte position. -/
+@[inline]
+def Slice.findNextPos (offset : String.Pos.Raw) (s : Slice) (_h : offset < s.rawEndPos) : s.Pos :=
+  go offset.inc
+where
+  go (offset : String.Pos.Raw) : s.Pos :=
+    if h : offset < s.rawEndPos then
+      if h' : (s.getUTF8Byte offset h).IsUTF8FirstByte then
+        s.pos offset (Pos.Raw.isValidForSlice_iff_isUTF8FirstByte.2 (Or.inr ⟨_, h'⟩))
+      else
+        go offset.inc
+    else
+      s.endPos
+  termination_by s.utf8ByteSize - offset.byteIdx
+  decreasing_by
+    simp only [Pos.Raw.lt_iff, byteIdx_rawEndPos, utf8ByteSize_eq, Pos.Raw.byteIdx_inc] at h ⊢
+    omega
+
+private theorem Slice.le_offset_findNextPosGo {s : Slice} {o : String.Pos.Raw} (h : o ≤ s.rawEndPos) :
+    o ≤ (findNextPos.go s o).offset := by
+  fun_induction findNextPos.go with
+  | case1 => simp
+  | case2 x h₁ h₂ ih =>
+    refine Pos.Raw.le_of_lt (Pos.Raw.lt_of_lt_of_le Pos.Raw.lt_inc (ih ?_))
+    rw [Pos.Raw.le_iff, Pos.Raw.byteIdx_inc]
+    exact Nat.succ_le_iff.2 h₁
+  | case3 x h => exact h
+
+theorem Slice.lt_offset_findNextPos {s : Slice} {o : String.Pos.Raw} (h) : o < (s.findNextPos o h).offset :=
+  Pos.Raw.lt_of_lt_of_le Pos.Raw.lt_inc (le_offset_findNextPosGo (Pos.Raw.inc_le.2 h))
+
 theorem Slice.Pos.prevAuxGo_le_self {s : Slice} {p : Nat} {h : p < s.utf8ByteSize} :
     prevAux.go p h ≤ ⟨p⟩ := by
   induction p with
@@ -2012,15 +2044,6 @@ theorem Slice.Pos.next_le_of_lt {s : Slice} {p q : s.Pos} {h} : p < q → p.next
 theorem Pos.ofToSlice_le_iff {s : String} {p : s.toSlice.Pos} {q : s.Pos} :
     ofToSlice p ≤ q ↔ p ≤ q.toSlice := Iff.rfl
 
-theorem Pos.ofToSlice_lt_iff {s : String} {p : s.toSlice.Pos} {q : s.Pos} :
-    ofToSlice p < q ↔ p < q.toSlice := Iff.rfl
-
-theorem Pos.lt_ofToSlice_iff {s : String} {p : s.Pos} {q : s.toSlice.Pos} :
-    p < ofToSlice q ↔ p.toSlice < q := Iff.rfl
-
-theorem Pos.le_ofToSlice_iff {s : String} {p : s.Pos} {q : s.toSlice.Pos} :
-    p ≤ ofToSlice q ↔ p.toSlice ≤ q := Iff.rfl
-
 @[simp]
 theorem Pos.toSlice_lt_toSlice_iff {s : String} {p q : s.Pos} :
     p.toSlice < q.toSlice ↔ p < q := Iff.rfl

src/Init/Data/String/FindPos.lean

@@ -1,62 +0,0 @@
-/-
-Copyright (c) 2025 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.String.Basic
-
-set_option doc.verso true
-
-/-!
-# Finding positions in a string relative to a given raw position
--/
-
-public section
-
-namespace String
-
-/--
-Obtains the smallest valid position that is greater than or equal to the given byte position.
--/
-def Slice.posGE (s : Slice) (offset : String.Pos.Raw)  (_h : offset ≤ s.rawEndPos) : s.Pos :=
-  if h : offset < s.rawEndPos then
-    if h' : (s.getUTF8Byte offset h).IsUTF8FirstByte then
-      s.pos offset (Pos.Raw.isValidForSlice_iff_isUTF8FirstByte.2 (Or.inr ⟨_, h'⟩))
-    else
-      s.posGE offset.inc (by simpa)
-  else
-    s.endPos
-termination_by s.utf8ByteSize - offset.byteIdx
-decreasing_by
-  simp only [Pos.Raw.lt_iff, byteIdx_rawEndPos, utf8ByteSize_eq, Pos.Raw.byteIdx_inc] at h ⊢
-  omega
-
-/--
-Obtains the smallest valid position that is strictly greater than the given byte position.
--/
-@[inline]
-def Slice.posGT (s : Slice) (offset : String.Pos.Raw)  (h : offset < s.rawEndPos) : s.Pos :=
-  s.posGE offset.inc (by simpa)
-
-@[deprecated Slice.posGT (since := "2026-02-03")]
-def Slice.findNextPos (offset : String.Pos.Raw) (s : Slice) (h : offset < s.rawEndPos) : s.Pos :=
-  s.posGT offset h
-
-/--
-Obtains the smallest valid position that is greater than or equal to the given byte position.
--/
-@[inline]
-def posGE (s : String) (offset : String.Pos.Raw) (h : offset ≤ s.rawEndPos) : s.Pos :=
-  Pos.ofToSlice (s.toSlice.posGE offset (by simpa))
-
-/--
-Obtains the smallest valid position that is strictly greater than the given byte position.
--/
-@[inline]
-def posGT (s : String) (offset : String.Pos.Raw) (h : offset < s.rawEndPos) : s.Pos :=
-  Pos.ofToSlice (s.toSlice.posGT offset (by simpa))
-
-end String

src/Init/Data/String/Lemmas.lean

@@ -9,9 +9,6 @@ prelude
 public import Init.Data.String.Lemmas.Splits
 public import Init.Data.String.Lemmas.Modify
 public import Init.Data.String.Lemmas.Search
-public import Init.Data.String.Lemmas.FindPos
-public import Init.Data.String.Lemmas.Basic
-public import Init.Data.String.Lemmas.Order
 public import Init.Data.Char.Order
 public import Init.Data.Char.Lemmas
 public import Init.Data.List.Lex

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

@@ -55,21 +55,4 @@ theorem Slice.Pos.startPos_le {s : Slice} (p : s.Pos) : s.startPos ≤ p := by
 theorem Slice.Pos.le_endPos {s : Slice} (p : s.Pos) : p ≤ s.endPos :=
   p.isValidForSlice.le_rawEndPos
 
-theorem getUTF8Byte_eq_getUTF8Byte_toSlice {s : String} {p : String.Pos.Raw} {h} :
-    s.getUTF8Byte p h = s.toSlice.getUTF8Byte p (by simpa) := by
-  simp [Slice.getUTF8Byte]
-
-theorem getUTF8Byte_toSlice {s : String} {p : String.Pos.Raw} {h} :
-    s.toSlice.getUTF8Byte p h = s.getUTF8Byte p (by simpa) := by
-  simp [Slice.getUTF8Byte]
-
-@[simp]
-theorem Pos.byte_toSlice {s : String} {p : s.Pos} {h} :
-    p.toSlice.byte h = p.byte (ne_of_apply_ne Pos.toSlice (by simpa)) := by
-  simp [byte]
-
-theorem Pos.byte_eq_byte_toSlice {s : String} {p : s.Pos} {h} :
-    p.byte h = p.toSlice.byte (ne_of_apply_ne Pos.ofToSlice (by simpa)) := by
-  simp
-
 end String

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

@@ -1,207 +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.String.FindPos
-import all Init.Data.String.FindPos
-import Init.Data.String.OrderInstances
-import Init.Data.String.Lemmas.Basic
-import Init.Data.String.Lemmas.Order
-
-public section
-
-namespace String
-
-namespace Slice
-
-@[simp]
-theorem le_offset_posGE {s : Slice} {p : Pos.Raw} {h : p ≤ s.rawEndPos} :
-    p ≤ (s.posGE p h).offset := by
-  fun_induction posGE with
-  | case1 => simp
-  | case2 => exact Std.le_trans (Std.le_of_lt (Pos.Raw.lt_inc)) ‹_›
-  | case3 => assumption
-
-@[simp]
-theorem posGE_le_iff {s : Slice} {p : Pos.Raw} {h : p ≤ s.rawEndPos} {q : s.Pos} :
-    s.posGE p h ≤ q ↔ p ≤ q.offset := by
-  fun_induction posGE with
-  | case1 => simp [Pos.le_iff]
-  | case2 r h₁ h₂ h₃ ih =>
-    suffices r ≠ q.offset by simp [ih, Pos.Raw.inc_le, Std.le_iff_lt_or_eq (a := r), this]
-    exact fun h => h₃ (h ▸ q.isUTF8FirstByte_getUTF8Byte_offset)
-  | case3 r h₁ h₂ =>
-    obtain rfl : r = s.rawEndPos := Std.le_antisymm h₁ (Std.not_lt.1 h₂)
-    simp only [Pos.endPos_le, ← offset_endPos, ← Pos.le_iff]
-
-@[simp]
-theorem lt_posGE_iff {s : Slice} {p : Pos.Raw} {h : p ≤ s.rawEndPos} {q : s.Pos} :
-    q < s.posGE p h ↔ q.offset < p := by
-  rw [← Std.not_le, posGE_le_iff, Std.not_le]
-
-theorem posGE_eq_iff {s : Slice} {p : Pos.Raw} {h : p ≤ s.rawEndPos} {q : s.Pos} :
-    s.posGE p h = q ↔ p ≤ q.offset ∧ ∀ q', p ≤ q'.offset → q ≤ q' :=
-  ⟨by rintro rfl; simp, fun ⟨h₁, h₂⟩ => Std.le_antisymm (by simpa) (h₂ _ (by simp))⟩
-
-theorem posGT_eq_posGE {s : Slice} {p : Pos.Raw} {h : p < s.rawEndPos} :
-    s.posGT p h = s.posGE p.inc (by simpa) :=
-  (rfl)
-
-@[simp]
-theorem posGE_inc {s : Slice} {p : Pos.Raw} {h : p.inc ≤ s.rawEndPos} :
-    s.posGE p.inc h = s.posGT p (by simpa) :=
-  (rfl)
-
-@[simp]
-theorem lt_offset_posGT {s : Slice} {p : Pos.Raw} {h : p < s.rawEndPos} :
-    p < (s.posGT p h).offset :=
-  Std.lt_of_lt_of_le p.lt_inc (by simp [posGT_eq_posGE, -posGE_inc])
-
-@[simp]
-theorem posGT_le_iff {s : Slice} {p : Pos.Raw} {h : p < s.rawEndPos} {q : s.Pos} :
-    s.posGT p h ≤ q ↔ p < q.offset := by
-  rw [posGT_eq_posGE, posGE_le_iff, Pos.Raw.inc_le]
-
-@[simp]
-theorem lt_posGT_iff {s : Slice} {p : Pos.Raw} {h : p < s.rawEndPos} {q : s.Pos} :
-    q < s.posGT p h ↔ q.offset ≤ p := by
-  rw [posGT_eq_posGE, lt_posGE_iff, Pos.Raw.lt_inc_iff]
-
-theorem posGT_eq_iff {s : Slice} {p : Pos.Raw} {h : p < s.rawEndPos} {q : s.Pos} :
-    s.posGT p h = q ↔ p < q.offset ∧ ∀ q', p < q'.offset → q ≤ q' := by
-  simp [posGT_eq_posGE, -posGE_inc, posGE_eq_iff]
-
-@[simp]
-theorem Pos.posGE_offset {s : Slice} {p : s.Pos} : s.posGE p.offset (by simp) = p := by
-  simp [posGE_eq_iff, Pos.le_iff]
-
-@[simp]
-theorem offset_posGE_eq_self_iff {s : Slice} {p : String.Pos.Raw} {h} :
-    (s.posGE p h).offset = p ↔ p.IsValidForSlice s :=
-  ⟨fun h' => by simpa [h'] using (s.posGE p h).isValidForSlice,
-   fun h' => by simpa using congrArg Pos.offset (Pos.posGE_offset (p := s.pos p h'))⟩
-
-theorem posGE_eq_pos {s : Slice} {p : String.Pos.Raw} (h : p.IsValidForSlice s) :
-    s.posGE p h.le_rawEndPos = s.pos p h := by
-  simpa using Pos.posGE_offset (p := s.pos p h)
-
-theorem pos_eq_posGE {s : Slice} {p : String.Pos.Raw} {h} :
-    s.pos p h = s.posGE p h.le_rawEndPos := by
-  simp [posGE_eq_pos h]
-
-@[simp]
-theorem Pos.posGT_offset {s : Slice} {p : s.Pos} {h} :
-    s.posGT p.offset h = p.next (by simpa using h) := by
-  rw [posGT_eq_iff, ← Pos.lt_iff]
-  simp [← Pos.lt_iff]
-
-theorem posGT_eq_next {s : Slice} {p : String.Pos.Raw} {h} (h' : p.IsValidForSlice s) :
-    s.posGT p h = (s.pos p h').next (by simpa [Pos.ext_iff] using Pos.Raw.ne_of_lt h) := by
-  simpa using Pos.posGT_offset (h := h) (p := s.pos p h')
-
-theorem next_eq_posGT {s : Slice} {p : s.Pos} {h} :
-    p.next h = s.posGT p.offset (by simpa) := by
-  simp
-
-end Slice
-
-@[simp]
-theorem le_offset_posGE {s : String} {p : Pos.Raw} {h : p ≤ s.rawEndPos} :
-    p ≤ (s.posGE p h).offset := by
-  simp [posGE]
-
-@[simp]
-theorem posGE_le_iff {s : String} {p : Pos.Raw} {h : p ≤ s.rawEndPos} {q : s.Pos} :
-    s.posGE p h ≤ q ↔ p ≤ q.offset := by
-  simp [posGE, Pos.ofToSlice_le_iff]
-
-@[simp]
-theorem lt_posGE_iff {s : String} {p : Pos.Raw} {h : p ≤ s.rawEndPos} {q : s.Pos} :
-    q < s.posGE p h ↔ q.offset < p := by
-  simp [posGE, Pos.lt_ofToSlice_iff]
-
-theorem posGE_eq_iff {s : String} {p : Pos.Raw} {h : p ≤ s.rawEndPos} {q : s.Pos} :
-    s.posGE p h = q ↔ p ≤ q.offset ∧ ∀ q', p ≤ q'.offset → q ≤ q' :=
-  ⟨by rintro rfl; simp, fun ⟨h₁, h₂⟩ => Std.le_antisymm (by simpa) (h₂ _ (by simp))⟩
-
-theorem posGT_eq_posGE {s : String} {p : Pos.Raw} {h : p < s.rawEndPos} :
-    s.posGT p h = s.posGE p.inc (by simpa) :=
-  (rfl)
-
-@[simp]
-theorem posGE_inc {s : String} {p : Pos.Raw} {h : p.inc ≤ s.rawEndPos} :
-    s.posGE p.inc h = s.posGT p (by simpa) :=
-  (rfl)
-
-@[simp]
-theorem lt_offset_posGT {s : String} {p : Pos.Raw} {h : p < s.rawEndPos} :
-    p < (s.posGT p h).offset :=
-  Std.lt_of_lt_of_le p.lt_inc (by simp [posGT_eq_posGE, -posGE_inc])
-
-@[simp]
-theorem posGT_le_iff {s : String} {p : Pos.Raw} {h : p < s.rawEndPos} {q : s.Pos} :
-    s.posGT p h ≤ q ↔ p < q.offset := by
-  rw [posGT_eq_posGE, posGE_le_iff, Pos.Raw.inc_le]
-
-@[simp]
-theorem lt_posGT_iff {s : String} {p : Pos.Raw} {h : p < s.rawEndPos} {q : s.Pos} :
-    q < s.posGT p h ↔ q.offset ≤ p := by
-  rw [posGT_eq_posGE, lt_posGE_iff, Pos.Raw.lt_inc_iff]
-
-theorem posGT_eq_iff {s : String} {p : Pos.Raw} {h : p < s.rawEndPos} {q : s.Pos} :
-    s.posGT p h = q ↔ p < q.offset ∧ ∀ q', p < q'.offset → q ≤ q' := by
-  simp [posGT_eq_posGE, -posGE_inc, posGE_eq_iff]
-
-theorem posGE_toSlice {s : String} {p : Pos.Raw} (h : p ≤ s.toSlice.rawEndPos) :
-    s.toSlice.posGE p h = (s.posGE p (by simpa)).toSlice := by
-  simp [posGE]
-
-theorem posGE_eq_posGE_toSlice {s : String} {p : Pos.Raw} (h : p ≤ s.rawEndPos) :
-    s.posGE p h = Pos.ofToSlice (s.toSlice.posGE p (by simpa)) := by
-  simp [posGE]
-
-theorem posGT_toSlice {s : String} {p : Pos.Raw} (h : p < s.toSlice.rawEndPos) :
-    s.toSlice.posGT p h = (s.posGT p (by simpa)).toSlice := by
-  simp [posGT]
-
-theorem posGT_eq_posGT_toSlice {s : String} {p : Pos.Raw} (h : p < s.rawEndPos) :
-    s.posGT p h = Pos.ofToSlice (s.toSlice.posGT p (by simpa)) := by
-  simp [posGT]
-
-@[simp]
-theorem Pos.posGE_offset {s : String} {p : s.Pos} : s.posGE p.offset (by simp) = p := by
-  simp [posGE_eq_iff, Pos.le_iff]
-
-@[simp]
-theorem offset_posGE_eq_self_iff {s : String} {p : String.Pos.Raw} {h} :
-    (s.posGE p h).offset = p ↔ p.IsValid s :=
-  ⟨fun h' => by simpa [h'] using (s.posGE p h).isValid,
-   fun h' => by simpa using congrArg Pos.offset (Pos.posGE_offset (p := s.pos p h'))⟩
-
-theorem posGE_eq_pos {s : String} {p : String.Pos.Raw} (h : p.IsValid s) :
-    s.posGE p h.le_rawEndPos = s.pos p h := by
-  simpa using Pos.posGE_offset (p := s.pos p h)
-
-theorem pos_eq_posGE {s : String} {p : String.Pos.Raw} {h} :
-    s.pos p h = s.posGE p h.le_rawEndPos := by
-  simp [posGE_eq_pos h]
-
-@[simp]
-theorem Pos.posGT_offset {s : String} {p : s.Pos} {h} :
-    s.posGT p.offset h = p.next (by simpa using h) := by
-  rw [posGT_eq_iff, ← Pos.lt_iff]
-  simp [← Pos.lt_iff]
-
-theorem posGT_eq_next {s : String} {p : String.Pos.Raw} {h} (h' : p.IsValid s) :
-    s.posGT p h = (s.pos p h').next (by simpa [Pos.ext_iff] using Pos.Raw.ne_of_lt h) := by
-  simpa using Pos.posGT_offset (h := h) (p := s.pos p h')
-
-theorem next_eq_posGT {s : String} {p : s.Pos} {h} :
-    p.next h = s.posGT p.offset (by simpa) := by
-  simp
-
-end String

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

@@ -1,109 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Markus Himmel
--/
-module
-
-prelude
-public import Init.Data.String.Basic
-import Init.Data.String.OrderInstances
-import Init.Data.String.Lemmas.Basic
-
-public section
-
-namespace String
-
-@[simp]
-theorem Slice.Pos.next_le_iff_lt {s : Slice} {p q : s.Pos} {h} : p.next h ≤ q ↔ p < q :=
-  ⟨fun h => Std.lt_of_lt_of_le lt_next h, next_le_of_lt⟩
-
-@[simp]
-theorem Slice.Pos.lt_next_iff_le {s : Slice} {p q : s.Pos} {h} : p < q.next h ↔ p ≤ q := by
-  rw [← Decidable.not_iff_not, Std.not_lt, next_le_iff_lt, Std.not_le]
-
-@[simp]
-theorem Pos.next_le_iff_lt {s : String} {p q : s.Pos} {h} : p.next h ≤ q ↔ p < q := by
-  rw [next, Pos.ofToSlice_le_iff, ← Pos.toSlice_lt_toSlice_iff]
-  exact Slice.Pos.next_le_iff_lt
-
-@[simp]
-theorem Slice.Pos.le_startPos {s : Slice} (p : s.Pos) : p ≤ s.startPos ↔ p = s.startPos :=
-  ⟨fun h => Std.le_antisymm h (startPos_le _), by simp +contextual⟩
-
-@[simp]
-theorem Slice.Pos.startPos_lt_iff {s : Slice} (p : s.Pos) : s.startPos < p ↔ p ≠ s.startPos := by
-  simp [← le_startPos, Std.not_le]
-
-@[simp]
-theorem Slice.Pos.endPos_le {s : Slice} (p : s.Pos) : s.endPos ≤ p ↔ p = s.endPos :=
-  ⟨fun h => Std.le_antisymm (le_endPos _) h, by simp +contextual⟩
-
-@[simp]
-theorem Pos.le_startPos {s : String} (p : s.Pos) : p ≤ s.startPos ↔ p = s.startPos :=
-  ⟨fun h => Std.le_antisymm h (startPos_le _), by simp +contextual⟩
-
-@[simp]
-theorem Pos.endPos_le {s : String} (p : s.Pos) : s.endPos ≤ p ↔ p = s.endPos :=
-  ⟨fun h => Std.le_antisymm (le_endPos _) h, by simp +contextual [Std.le_refl]⟩
-
-@[simp]
-theorem Slice.Pos.not_lt_startPos {s : Slice} {p : s.Pos} : ¬ p < s.startPos :=
-  fun h => Std.lt_irrefl (Std.lt_of_lt_of_le h (Slice.Pos.startPos_le _))
-
-theorem Slice.Pos.ne_startPos_of_lt {s : Slice} {p q : s.Pos} : p < q → q ≠ s.startPos := by
-  rintro h rfl
-  simp at h
-
-@[simp]
-theorem Slice.Pos.next_ne_startPos {s : Slice} {p : s.Pos} {h} :
-    p.next h ≠ s.startPos :=
-  ne_startPos_of_lt lt_next
-
-theorem Slice.Pos.ofSliceFrom_lt_ofSliceFrom_iff {s : Slice} {p : s.Pos}
-    {q r : (s.sliceFrom p).Pos} : Slice.Pos.ofSliceFrom q < Slice.Pos.ofSliceFrom r ↔ q < r := by
-  simp [Slice.Pos.lt_iff, Pos.Raw.lt_iff]
-
-theorem Slice.Pos.ofSliceFrom_le_ofSliceFrom_iff {s : Slice} {p : s.Pos}
-    {q r : (s.sliceFrom p).Pos} : Slice.Pos.ofSliceFrom q ≤ Slice.Pos.ofSliceFrom r ↔ q ≤ r := by
-  simp [Slice.Pos.le_iff, Pos.Raw.le_iff]
-
-@[simp]
-theorem Slice.Pos.offset_le_rawEndPos {s : Slice} {p : s.Pos} :
-    p.offset ≤ s.rawEndPos :=
-  p.isValidForSlice.le_rawEndPos
-
-@[simp]
-theorem Pos.offset_le_rawEndPos {s : String} {p : s.Pos} :
-    p.offset ≤ s.rawEndPos :=
-  p.isValid.le_rawEndPos
-
-@[simp]
-theorem Slice.Pos.offset_lt_rawEndPos_iff {s : Slice} {p : s.Pos} :
-    p.offset < s.rawEndPos ↔ p ≠ s.endPos := by
-  simp [Std.lt_iff_le_and_ne, p.offset_le_rawEndPos, Pos.ext_iff]
-
-@[simp]
-theorem Pos.offset_lt_rawEndPos_iff {s : String} {p : s.Pos} :
-    p.offset < s.rawEndPos ↔ p ≠ s.endPos := by
-  simp [Std.lt_iff_le_and_ne, p.offset_le_rawEndPos, Pos.ext_iff]
-
-@[simp]
-theorem Slice.Pos.getUTF8Byte_offset {s : Slice} {p : s.Pos} {h} :
-    s.getUTF8Byte p.offset h = p.byte (by simpa using h) := by
-  simp [Pos.byte]
-
-theorem Slice.Pos.isUTF8FirstByte_getUTF8Byte_offset {s : Slice} {p : s.Pos} {h} :
-    (s.getUTF8Byte p.offset h).IsUTF8FirstByte := by
-  simpa [getUTF8Byte_offset] using isUTF8FirstByte_byte
-
-theorem Pos.getUTF8Byte_offset {s : String} {p : s.Pos} {h} :
-    s.getUTF8Byte p.offset h = p.byte (by simpa using h) := by
-  simp only [getUTF8Byte_eq_getUTF8Byte_toSlice, ← Pos.offset_toSlice,
-    Slice.Pos.getUTF8Byte_offset, byte_toSlice]
-
-theorem Pos.isUTF8FirstByte_getUTF8Byte_offset {s : String} {p : s.Pos} {h} :
-    (s.getUTF8Byte p.offset h).IsUTF8FirstByte := by
-  simpa [getUTF8Byte_offset] using isUTF8FirstByte_byte
-
-end String

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

@@ -8,10 +8,8 @@ module
 prelude
 public import Init.Data.String.Pattern.Basic
 public import Init.Data.Iterators.Consumers.Monadic.Loop
-public import Init.Data.Vector.Basic
-public import Init.Data.String.FindPos
 import Init.Data.String.Termination
-import Init.Data.String.Lemmas.FindPos
+public import Init.Data.Vector.Basic
 
 set_option doc.verso true
 
@@ -150,15 +148,15 @@ instance (s : Slice) : Std.Iterator (ForwardSliceSearcher s) Id (SearchStep s) w
             let basePos := s.pos! stackPos
             -- Since we report (mis)matches by code point and not by byte, missing in the first byte
             -- means that we should skip ahead to the next code point.
-            let nextStackPos := s.posGT stackPos h₁
+            let nextStackPos := s.findNextPos stackPos h₁
             let res := .rejected basePos nextStackPos
             -- Invariants still satisfied
             pure (.deflate ⟨.yield ⟨.proper needle table htable nextStackPos.offset 0
               (by simp [Pos.Raw.lt_iff] at hn ⊢; omega)⟩ res,
                by simpa using ⟨_, _, ⟨rfl, rfl⟩, by simp [Pos.Raw.lt_iff] at hn ⊢; omega,
                 Or.inl (by
-                  have := lt_offset_posGT (h := h₁)
-                  have t₀ := (posGT _ _ h₁).isValidForSlice.le_utf8ByteSize
+                  have := lt_offset_findNextPos h₁
+                  have t₀ := (findNextPos _ _ h₁).isValidForSlice.le_utf8ByteSize
                   simp [nextStackPos, Pos.Raw.lt_iff] at this ⊢; omega)⟩⟩)
           else
             let newNeedlePos := table[needlePos.byteIdx - 1]'(by simp [Pos.Raw.lt_iff] at hn; omega)
@@ -167,16 +165,19 @@ instance (s : Slice) : Std.Iterator (ForwardSliceSearcher s) Id (SearchStep s) w
               let basePos := s.pos! (stackPos.unoffsetBy needlePos)
               -- Since we report (mis)matches by code point and not by byte, missing in the first byte
               -- means that we should skip ahead to the next code point.
-              let nextStackPos := s.posGE stackPos (Pos.Raw.le_of_lt h₁)
+              let nextStackPos := (s.pos? stackPos).getD (s.findNextPos stackPos h₁)
               let res := .rejected basePos nextStackPos
               -- Invariants still satisfied
               pure (.deflate ⟨.yield ⟨.proper needle table htable nextStackPos.offset 0
                 (by simp [Pos.Raw.lt_iff] at hn ⊢; omega)⟩ res,
                  by simpa using ⟨_, _, ⟨rfl, rfl⟩, by simp [Pos.Raw.lt_iff] at hn ⊢; omega, by
-                  have h₂ := le_offset_posGE (h := Pos.Raw.le_of_lt h₁)
-                  have h₃ := (s.posGE _ (Pos.Raw.le_of_lt h₁)).isValidForSlice.le_utf8ByteSize
-                  simp [Pos.Raw.le_iff, Pos.Raw.lt_iff, Pos.Raw.ext_iff, nextStackPos] at ⊢ h₂
-                  omega⟩⟩)
+                  simp only [pos?, Pos.Raw.isValidForSlice_eq_true_iff, nextStackPos]
+                  split
+                  · exact Or.inr (by simp [Pos.Raw.lt_iff]; omega)
+                  · refine Or.inl ?_
+                    have := lt_offset_findNextPos h₁
+                    have t₀ := (findNextPos _ _ h₁).isValidForSlice.le_utf8ByteSize
+                    simp [Pos.Raw.lt_iff] at this ⊢; omega⟩⟩)
             else
               let oldBasePos := s.pos! (stackPos.decreaseBy needlePos.byteIdx)
               let newBasePos := s.pos! (stackPos.decreaseBy newNeedlePos)
@@ -263,7 +264,8 @@ def startsWith (pat : Slice) (s : Slice) : Bool :=
     have hs := by
       simp [Pos.Raw.le_iff] at h ⊢
       omega
-    have hp := by simp
+    have hp := by
+      simp [Pos.Raw.le_iff]
     Internal.memcmpSlice s pat s.startPos.offset pat.startPos.offset pat.rawEndPos hs hp
   else
     false
@@ -299,7 +301,7 @@ def endsWith (pat : Slice) (s : Slice) : Bool :=
       simp [sStart, Pos.Raw.le_iff] at h ⊢
       omega
     have hp := by
-      simp [patStart] at h ⊢
+      simp [patStart, Pos.Raw.le_iff] at h ⊢
     Internal.memcmpSlice s pat sStart patStart pat.rawEndPos hs hp
   else
     false

src/Init/Data/String/PosRaw.lean

@@ -144,11 +144,8 @@ theorem Pos.Raw.offsetBy_assoc {p q r : Pos.Raw} :
 
 @[simp]
 theorem Pos.Raw.offsetBy_zero_left {p : Pos.Raw} : (0 : Pos.Raw).offsetBy p = p := by
-  simp [Pos.Raw.ext_iff]
-
-@[simp]
-theorem Pos.Raw.offsetBy_zero {p : Pos.Raw} : p.offsetBy 0 = p := by
-  simp [Pos.Raw.ext_iff]
+  ext
+  simp
 
 /--
 Decreases `p` by `offset`. This is not an `HSub` instance because it should be a relatively
@@ -177,14 +174,6 @@ theorem Pos.Raw.unoffsetBy_offsetBy {p q : Pos.Raw} : (p.offsetBy q).unoffsetBy
   ext
   simp
 
-@[simp]
-theorem Pos.Raw.unoffsetBy_zero {p : Pos.Raw} : p.unoffsetBy 0 = p := by
-  simp [Pos.Raw.ext_iff]
-
-@[simp]
-theorem Pos.Raw.unoffsetBy_le_self {p q : Pos.Raw} : p.unoffsetBy q ≤ p := by
-  simp [Pos.Raw.le_iff]
-
 @[simp]
 theorem Pos.Raw.eq_zero_iff {p : Pos.Raw} : p = 0 ↔ p.byteIdx = 0 :=
   Pos.Raw.ext_iff
@@ -206,10 +195,6 @@ def Pos.Raw.increaseBy (p : Pos.Raw) (n : Nat) : Pos.Raw where
 theorem Pos.Raw.byteIdx_increaseBy {p : Pos.Raw} {n : Nat} :
     (p.increaseBy n).byteIdx = p.byteIdx + n := (rfl)
 
-@[simp]
-theorem Pos.Raw.increaseBy_zero {p : Pos.Raw} : p.increaseBy 0 = p := by
-  simp [Pos.Raw.ext_iff]
-
 /--
 Move the position `p` back by `n` bytes. This is not an `HSub` instance because it should be a
 relatively rare operation, so we use a name to make accidental use less likely. To remove the size
@@ -227,10 +212,6 @@ def Pos.Raw.decreaseBy (p : Pos.Raw) (n : Nat) : Pos.Raw where
 theorem Pos.Raw.byteIdx_decreaseBy {p : Pos.Raw} {n : Nat} :
     (p.decreaseBy n).byteIdx = p.byteIdx - n := (rfl)
 
-@[simp]
-theorem Pos.Raw.decreaseBy_zero {p : Pos.Raw} : p.decreaseBy 0 = p := by
-  simp [Pos.Raw.ext_iff]
-
 theorem Pos.Raw.increaseBy_charUtf8Size {p : Pos.Raw} {c : Char} :
     p.increaseBy c.utf8Size = p + c := by
   simp [Pos.Raw.ext_iff]
@@ -243,10 +224,6 @@ def Pos.Raw.inc (p : Pos.Raw) : Pos.Raw :=
 @[simp]
 theorem Pos.Raw.byteIdx_inc {p : Pos.Raw} : p.inc.byteIdx = p.byteIdx + 1 := (rfl)
 
-@[simp]
-theorem Pos.Raw.inc_unoffsetBy_inc {p q : Pos.Raw} : p.inc.unoffsetBy q.inc = p.unoffsetBy q := by
-  simp [Pos.Raw.ext_iff]
-
 /-- Decreases the byte offset of the position by `1`. Not to be confused with `Pos.prev`. -/
 @[inline, expose]
 def Pos.Raw.dec (p : Pos.Raw) : Pos.Raw :=
@@ -258,17 +235,12 @@ theorem Pos.Raw.byteIdx_dec {p : Pos.Raw} : p.dec.byteIdx = p.byteIdx - 1 := (rf
 @[simp]
 theorem Pos.Raw.le_refl {p : Pos.Raw} : p ≤ p := by simp [le_iff]
 
-@[simp]
 theorem Pos.Raw.lt_inc {p : Pos.Raw} : p < p.inc := by simp [lt_iff]
 
 theorem Pos.Raw.le_of_lt {p q : Pos.Raw} : p < q → p ≤ q := by simpa [lt_iff, le_iff] using Nat.le_of_lt
 
-@[simp]
 theorem Pos.Raw.inc_le {p q : Pos.Raw} : p.inc ≤ q ↔ p < q := by simpa [lt_iff, le_iff] using Nat.succ_le_iff
 
-@[simp]
-theorem Pos.Raw.lt_inc_iff {p q : Pos.Raw} : p < q.inc ↔ p ≤ q := by simpa [lt_iff, le_iff] using Nat.lt_add_one_iff
-
 theorem Pos.Raw.lt_of_le_of_lt {a b c : Pos.Raw} : a ≤ b → b < c → a < c := by
   simpa [le_iff, lt_iff] using Nat.lt_of_le_of_lt
 

src/Init/Data/String/Slice.lean

@@ -66,7 +66,7 @@ The implementation is an efficient equivalent of {lean}`s1.copy == s2.copy`
 -/
 def beq (s1 s2 : Slice) : Bool :=
   if h : s1.utf8ByteSize = s2.utf8ByteSize then
-    have h1 := by simp
+    have h1 := by simp [h, String.Pos.Raw.le_iff]
     have h2 := by simp [h, String.Pos.Raw.le_iff]
     Internal.memcmpSlice s1 s2 s1.startPos.offset s2.startPos.offset s1.rawEndPos h1 h2
   else

src/Init/Data/UInt/Basic.lean

@@ -373,7 +373,7 @@ Examples:
  * `(if (5 : UInt16) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : UInt16) < 7) by decide`
 -/
-@[extern "lean_uint16_dec_lt", instance_reducible]
+@[extern "lean_uint16_dec_lt"]
 def UInt16.decLt (a b : UInt16) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
 
@@ -390,7 +390,7 @@ Examples:
  * `(if (5 : UInt16) ≤ 15 then "yes" else "no") = "yes"`
  * `show (7 : UInt16) ≤ 7 by decide`
 -/
-@[extern "lean_uint16_dec_le", instance_reducible]
+@[extern "lean_uint16_dec_le"]
 def UInt16.decLe (a b : UInt16) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
 
@@ -737,7 +737,7 @@ Examples:
  * `(if (5 : UInt64) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : UInt64) < 7) by decide`
 -/
-@[extern "lean_uint64_dec_lt", instance_reducible]
+@[extern "lean_uint64_dec_lt"]
 def UInt64.decLt (a b : UInt64) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
 
@@ -753,7 +753,7 @@ Examples:
  * `(if (5 : UInt64) ≤ 15 then "yes" else "no") = "yes"`
  * `show (7 : UInt64) ≤ 7 by decide`
 -/
-@[extern "lean_uint64_dec_le", instance_reducible]
+@[extern "lean_uint64_dec_le"]
 def UInt64.decLe (a b : UInt64) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
 

src/Init/Data/UInt/BasicAux.lean

@@ -397,7 +397,7 @@ Examples:
  * `(if (5 : USize) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : USize) < 7) by decide`
 -/
-@[extern "lean_usize_dec_lt", instance_reducible]
+@[extern "lean_usize_dec_lt"]
 def USize.decLt (a b : USize) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
 
@@ -413,7 +413,7 @@ Examples:
  * `(if (5 : USize) ≤ 15 then "yes" else "no") = "yes"`
  * `show (7 : USize) ≤ 7 by decide`
 -/
-@[extern "lean_usize_dec_le", instance_reducible]
+@[extern "lean_usize_dec_le"]
 def USize.decLe (a b : USize) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
 

src/Init/Data/Vector.lean

@@ -24,5 +24,3 @@ public import Init.Data.Vector.Perm
 public import Init.Data.Vector.Find
 public import Init.Data.Vector.Algebra
 public import Init.Data.Vector.Stream
-public import Init.Data.Vector.Nat
-public import Init.Data.Vector.Int

src/Init/Data/Vector/Algebra.lean

@@ -74,7 +74,6 @@ def mul [Mul α] (xs ys : Vector α n) : Vector α n :=
 Pointwise multiplication of vectors.
 This is not a global instance as in some applications different multiplications may be relevant.
 -/
-@[instance_reducible]
 def instMul [Mul α] : Mul (Vector α n) := ⟨mul⟩
 
 section mul

src/Init/Data/Vector/Basic.lean

@@ -12,7 +12,6 @@ public import Init.Data.Array.Range
 public import Init.Data.Range
 -- TODO: Making this private leads to a panic in Init.Grind.Ring.Poly.
 public import Init.Data.Slice.Array.Iterator
-import Init.Data.Array.Nat
 
 public section
 

src/Init/Data/Vector/Count.lean

@@ -70,18 +70,6 @@ theorem countP_le_size {xs : Vector α n} : countP p xs ≤ n := by
   cases xs
   simp
 
-/-- This lemma is only relevant for `grind`. -/
-@[grind ←=]
-theorem _root_.Std.Internal.Vector.countP_eq_zero_of_forall {xs : Vector α n} (h : ∀ x ∈ xs, ¬ p x) : xs.countP p = 0 :=
-  countP_eq_zero.mpr h
-
-/-- This lemma is only relevant for `grind`. -/
-theorem _root_.Std.Internal.Vector.not_of_countP_eq_zero_of_mem {xs : Vector α n} (h : xs.countP p = 0) (h' : x ∈ xs) : ¬ p x :=
-   countP_eq_zero.mp h _ h'
-
-grind_pattern Std.Internal.Vector.not_of_countP_eq_zero_of_mem => xs.countP p, x ∈ xs where
-  guard xs.countP p = 0
-
 @[simp] theorem countP_eq_size {p} {xs : Vector α n} : countP p xs = n ↔ ∀ a ∈ xs, p a := by
   rcases xs with ⟨xs, rfl⟩
   simp
@@ -99,7 +87,6 @@ theorem boole_getElem_le_countP {p : α → Bool} {xs : Vector α n} (h : i < n)
   rcases xs with ⟨xs, rfl⟩
   simp [Array.boole_getElem_le_countP]
 
-@[grind =]
 theorem countP_set {p : α → Bool} {xs : Vector α n} {a : α} (h : i < n) :
     (xs.set i a).countP p = xs.countP p - (if p xs[i] then 1 else 0) + (if p a then 1 else 0) := by
   rcases xs with ⟨xs, rfl⟩

src/Init/Data/Vector/Int.lean

@@ -1,32 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison, Sebastian Graf, Paul Reichert
--/
-module
-
-prelude
-public import Init.Data.Vector.Lemmas
-public import Init.Data.Vector.Basic
-import Init.Data.Array.Int
-
-public section
-
-set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-set_option linter.indexVariables true -- Enforce naming conventions for index variables.
-
-namespace Vector
-
-@[simp] theorem sum_replicate_int {n : Nat} {a : Int} : (replicate n a).sum = n * a := by
-  simp [← sum_toArray, Array.sum_replicate_int]
-
-theorem sum_append_int {as₁ as₂ : Vector Int n} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
-  simp [← sum_toArray]
-
-theorem sum_reverse_int (xs : Vector Int n) : xs.reverse.sum = xs.sum := by
-  simp [sum_reverse]
-
-theorem sum_eq_foldl_int {xs : Vector Int n} : xs.sum = xs.foldl (b := 0) (· + ·) := by
-  simp only [foldl_eq_foldr_reverse, Int.add_comm, ← sum_eq_foldr, sum_reverse_int]
-
-end Vector

src/Init/Data/Vector/Lemmas.lean

@@ -254,9 +254,6 @@ theorem toArray_mk {xs : Array α} (h : xs.size = n) : (Vector.mk xs h).toArray
 @[simp] theorem sum_mk [Add α] [Zero α] {xs : Array α} (h : xs.size = n) :
     (Vector.mk xs h).sum = xs.sum := rfl
 
-@[simp, grind =] theorem sum_toArray [Add α] [Zero α] {xs : Vector α n} :
-    xs.toArray.sum = xs.sum := rfl
-
 @[simp] theorem eq_mk : xs = Vector.mk as h ↔ xs.toArray = as := by
   cases xs
   simp
@@ -506,15 +503,6 @@ protected theorem ext {xs ys : Vector α n} (h : (i : Nat) → (_ : i < n) → x
 
 @[simp, grind =] theorem toList_mk : (Vector.mk xs h).toList = xs.toList := rfl
 
-@[simp, grind =] theorem sum_toList [Add α] [Zero α] {xs : Vector α n} :
-    xs.toList.sum = xs.sum := by
-  rw [← toList_toArray, Array.sum_toList, sum_toArray]
-
-@[simp, grind =]
-theorem Vector.toList_zip {as : Vector α n} {bs : Vector β n} :
-    (Vector.zip as bs).toList = List.zip as.toList bs.toList := by
-  rw [mk_zip_mk, toList_mk, Array.toList_zip, toList_toArray, toList_toArray]
-
 @[simp] theorem getElem_toList {xs : Vector α n} {i : Nat} (h : i < xs.toList.length) :
     xs.toList[i] = xs[i]'(by simpa using h) := by
   cases xs
@@ -525,7 +513,6 @@ theorem Vector.toList_zip {as : Vector α n} {bs : Vector β n} :
   cases xs
   simp
 
-@[simp, grind =]
 theorem toList_append {xs : Vector α m} {ys : Vector α n} :
     (xs ++ ys).toList = xs.toList ++ ys.toList := by simp [toList]
 
@@ -582,7 +569,7 @@ theorem toList_push {xs : Vector α n} {x} : (xs.push x).toList = xs.toList ++ [
 
 theorem toList_range : (Vector.range n).toList = List.range n := by simp [toList]
 
-@[simp] theorem toList_reverse {xs : Vector α n} : xs.reverse.toList = xs.toList.reverse := by simp [toList]
+theorem toList_reverse {xs : Vector α n} : xs.reverse.toList = xs.toList.reverse := by simp [toList]
 
 theorem toList_set {xs : Vector α n} {i x} (h) :
     (xs.set i x).toList = xs.toList.set i x := rfl
@@ -1041,18 +1028,10 @@ theorem mem_iff_getElem {a} {xs : Vector α n} : a ∈ xs ↔ ∃ (i : Nat) (h :
 theorem mem_iff_getElem? {a} {xs : Vector α n} : a ∈ xs ↔ ∃ i : Nat, xs[i]? = some a := by
   simp [getElem?_eq_some_iff, mem_iff_getElem]
 
-theorem exists_mem_iff_exists_getElem {P : α → Prop} {xs : Vector α n} :
-    (∃ x ∈ xs, P x) ↔ ∃ (i : Nat), ∃ (hi : i < n), P (xs[i]) := by
-  cases xs; simp [*, Array.exists_mem_iff_exists_getElem]
-
-theorem forall_mem_iff_forall_getElem {P : α → Prop} {xs : Vector α n} :
-    (∀ x ∈ xs, P x) ↔ ∀ (i : Nat) (hi : i < n), P (xs[i]) := by
-  cases xs; simp [*, Array.forall_mem_iff_forall_getElem]
-
-@[deprecated forall_mem_iff_forall_getElem (since := "2026-01-29")]
 theorem forall_getElem {xs : Vector α n} {p : α → Prop} :
-    (∀ (i : Nat) h, p (xs[i]'h)) ↔ ∀ a, a ∈ xs → p a :=
-  forall_mem_iff_forall_getElem.symm
+    (∀ (i : Nat) h, p (xs[i]'h)) ↔ ∀ a, a ∈ xs → p a := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.forall_getElem]
 
 /-! ### Decidability of bounded quantifiers -/
 
@@ -2159,6 +2138,9 @@ theorem flatMap_replicate {f : α → Vector β m} : (replicate n a).flatMap f =
   ext i h
   simp
 
+@[simp] theorem sum_replicate_nat {n : Nat} {a : Nat} : (replicate n a).sum = n * a := by
+  simp [sum, toArray_replicate]
+
 /-! ### reverse -/
 
 theorem reverse_empty : reverse (#v[] : Vector α 0) = #v[] := rfl
@@ -3040,19 +3022,9 @@ instance instDecidableExistsVectorSucc (P : Vector α (n+1) → Prop)
 
 /-! ### sum -/
 
-@[simp, grind =] theorem sum_empty [Add α] [Zero α] : (#v[] : Vector α 0).sum = 0 := rfl
-theorem sum_eq_foldr [Add α] [Zero α] {xs : Vector α n} :
-    xs.sum = xs.foldr (b := 0) (· + ·) :=
-  rfl
-
 @[simp, grind =]
-theorem sum_append [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
-    [Std.LeftIdentity (α := α) (· + ·) 0] [Std.LawfulLeftIdentity (α := α) (· + ·) 0]
-    {as₁ as₂ : Vector α n} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
-  simp [← sum_toList, List.sum_append]
-
-@[simp, grind =]
-theorem sum_reverse [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
-    [Std.Commutative (α := α) (· + ·)]
-    [Std.LawfulLeftIdentity (α := α) (· + ·) 0] (xs : Vector α n) : xs.reverse.sum = xs.sum := by
-  simp [← sum_toList, List.sum_reverse]
+theorem sum_append_nat {xs₁ : Vector Nat n} {xs₂ : Vector Nat m} :
+    (xs₁ ++ xs₂).sum = xs₁.sum + xs₂.sum := by
+  rcases xs₁ with ⟨xs₁, rfl⟩
+  rcases xs₂ with ⟨xs₂, rfl⟩
+  simp [Array.sum_append_nat]

src/Init/Data/Vector/Nat.lean

@@ -1,39 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison, Sebastian Graf, Paul Reichert
--/
-module
-
-prelude
-public import Init.Data.Vector.Lemmas
-public import Init.Data.Vector.Basic
-import Init.Data.Array.Nat
-
-public section
-
-set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-set_option linter.indexVariables true -- Enforce naming conventions for index variables.
-
-namespace Vector
-
-protected theorem sum_pos_iff_exists_pos_nat {xs : Vector Nat n} : 0 < xs.sum ↔ ∃ x ∈ xs, 0 < x := by
-  simp [← sum_toArray, Array.sum_pos_iff_exists_pos_nat]
-
-protected theorem sum_eq_zero_iff_forall_eq_nat {xs : Vector Nat n} :
-    xs.sum = 0 ↔ ∀ x ∈ xs, x = 0 := by
-  simp [← sum_toArray, Array.sum_eq_zero_iff_forall_eq_nat]
-
-@[simp] theorem sum_replicate_nat {n : Nat} {a : Nat} : (replicate n a).sum = n * a := by
-  simp [← sum_toArray, Array.sum_replicate_nat]
-
-theorem sum_append_nat {as₁ as₂ : Vector Nat n} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
-  simp [← sum_toArray]
-
-theorem sum_reverse_nat (xs : Vector Nat n) : xs.reverse.sum = xs.sum := by
-  simp [sum_reverse]
-
-theorem sum_eq_foldl_nat {xs : Vector Nat n} : xs.sum = xs.foldl (b := 0) (· + ·) := by
-  simp only [foldl_eq_foldr_reverse, Nat.add_comm, ← sum_eq_foldr, sum_reverse_nat]
-
-end Vector

src/Init/Data/Vector/OfFn.lean

@@ -37,11 +37,6 @@ theorem mem_ofFn {n} {f : Fin n → α} {a : α} : a ∈ ofFn f ↔ ∃ i, f i =
   · rintro ⟨i, rfl⟩
     apply mem_of_getElem (i := i) <;> simp
 
-@[simp, grind =]
-theorem map_ofFn {f : Fin n → α} {g : α → β} :
-    (Vector.ofFn f).map g = Vector.ofFn (g ∘ f) := by
-  simp [← Vector.toArray_inj]
-
 @[grind =] theorem back_ofFn {n} [NeZero n] {f : Fin n → α} :
     (ofFn f).back = f ⟨n - 1, by have := NeZero.ne n; omega⟩ := by
   simp [back]
@@ -64,11 +59,6 @@ theorem ofFn_succ' {f : Fin (n+1) → α} :
   apply Vector.toArray_inj.mp
   simp [Array.ofFn_succ']
 
-@[simp]
-theorem ofFn_getElem {xs : Vector α n} :
-    Vector.ofFn (fun i : Fin n => xs[i.val]) = xs := by
-  ext; simp
-
 /-! ### ofFnM -/
 
 /-- Construct (in a monadic context) a vector by applying a monadic function to each index. -/

src/Init/Grind/Config.lean

@@ -213,11 +213,6 @@ structure Config where
   reducible declarations are always unfolded in those contexts.
   -/
   reducible := true
-  /--
-  Maximum number of library suggestions to use. If `none`, uses the default limit.
-  Only relevant when `suggestions` is `true`.
-  -/
-  maxSuggestions : Option Nat := none
   deriving Inhabited, BEq
 
 /--

src/Init/Grind/Module/Basic.lean

@@ -60,7 +60,6 @@ class NatModule (M : Type u) extends AddCommMonoid M where
   /-- Scalar multiplication by a successor. -/
   add_one_nsmul : ∀ n : Nat, ∀ a : M, (n + 1) • a = n • a + a
 
-attribute [instance_reducible] NatModule.nsmul
 attribute [instance 100] NatModule.toAddCommMonoid NatModule.nsmul
 
 /--
@@ -83,7 +82,6 @@ class IntModule (M : Type u) extends AddCommGroup M where
   /-- Scalar multiplication by natural numbers is consistent with scalar multiplication by integers. -/
   zsmul_natCast_eq_nsmul : ∀ n : Nat, ∀ a : M, (n : Int) • a = n • a
 
-attribute [instance_reducible] IntModule.zsmul
 attribute [instance 100] IntModule.toAddCommGroup IntModule.zsmul
 
 namespace IntModule

src/Init/Grind/Module/Envelope.lean

@@ -203,7 +203,6 @@ theorem zsmul_natCast_eq_nsmul (n : Nat) (a : Q α) : zsmul (n : Int) a = nsmul
   induction a using Q.ind with | _ a
   rcases a with ⟨a₁, a₂⟩; simp; omega
 
-@[instance_reducible]
 def ofNatModule : IntModule (Q α) := {
   nsmul := ⟨nsmul⟩,
   zsmul := ⟨zsmul⟩,
@@ -305,7 +304,7 @@ instance [LE α] [IsPreorder α] [OrderedAdd α] : IsPreorder (OfNatModule.Q α)
     obtain ⟨⟨a₁, a₂⟩⟩ := a
     change Q.mk _ ≤ Q.mk _
     simp only [mk_le_mk]
-    simp [AddCommMonoid.add_comm]
+    simp [AddCommMonoid.add_comm]; exact le_refl (a₁ + a₂)
   le_trans {a b c} h₁ h₂ := by
     induction a using Q.ind with | _ a
     induction b using Q.ind with | _ b

src/Init/Grind/Order.lean

@@ -225,7 +225,7 @@ theorem le_eq_true_of_lt {α} [LE α] [LT α] [Std.LawfulOrderLT α]
 
 theorem le_eq_true {α} [LE α] [Std.IsPreorder α]
     {a : α} : (a ≤ a) = True := by
-  simp
+  simp; exact Std.le_refl a
 
 theorem le_eq_true_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α]
     {a : α} {k : Int} : (0 : Int).ble' k → (a ≤ a + k) = True := by

src/Init/Grind/Ordered/Linarith.lean

@@ -327,6 +327,7 @@ theorem eq_norm {α} [IntModule α] (ctx : Context α) (lhs rhs : Expr) (p : Pol
 theorem le_of_eq {α} [IntModule α] [LE α] [IsPreorder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
     : norm_cert lhs rhs p → lhs.denote ctx = rhs.denote ctx → p.denote' ctx ≤ 0 := by
   simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote, h₁, sub_self]
+  apply le_refl
 
 theorem diseq_norm {α} [IntModule α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
     : norm_cert lhs rhs p → lhs.denote ctx ≠ rhs.denote ctx → p.denote' ctx ≠ 0 := by

src/Init/Grind/Ordered/Ring.lean

@@ -44,7 +44,7 @@ theorem neg_one_lt_zero : (-1 : R) < 0 := by
 
 theorem ofNat_nonneg (x : Nat) : (OfNat.ofNat x : R) ≥ 0 := by
   induction x
-  next => simp [OfNat.ofNat, Zero.zero]
+  next => simp [OfNat.ofNat, Zero.zero]; apply le_refl
   next n ih =>
     have := OrderedRing.zero_lt_one (R := R)
     rw [Semiring.ofNat_succ]
@@ -134,8 +134,8 @@ theorem lt_of_intCast_lt_intCast (a b : Int) : (a : R) < (b : R) → a < b := by
     omega
 
 theorem natCast_le_natCast_of_le (a b : Nat) : a ≤ b → (a : R) ≤ (b : R) := by
-  induction a generalizing b <;> cases b <;> simp [- Std.le_refl]
-  next => simp [Semiring.natCast_zero]
+  induction a generalizing b <;> cases b <;> simp
+  next => simp [Semiring.natCast_zero, Std.IsPreorder.le_refl]
   next n =>
     have := ofNat_nonneg (R := R) n
     simp [Semiring.ofNat_eq_natCast] at this

src/Init/Grind/Ring/Basic.lean

@@ -88,8 +88,6 @@ class Semiring (α : Type u) extends Add α, Mul α where
   -/
   nsmul_eq_natCast_mul : ∀ n : Nat, ∀ a : α, n • a = Nat.cast n * a := by intros; rfl
 
-attribute [instance_reducible] Semiring.npow Semiring.ofNat Semiring.natCast
-
 /--
 A ring, i.e. a type equipped with addition, negation, multiplication, and a map from the integers,
 satisfying appropriate compatibilities.
@@ -114,8 +112,6 @@ class Ring (α : Type u) extends Semiring α, Neg α, Sub α where
   /-- The canonical map from the integers is consistent with negation. -/
   intCast_neg : ∀ i : Int, Int.cast (R := α) (-i) = -Int.cast i := by intros; rfl
 
-attribute [instance_reducible] Ring.intCast Ring.zsmul
-
 /--
 A commutative semiring, i.e. a semiring with commutative multiplication.
 

src/Init/Grind/Ring/Envelope.lean

@@ -244,7 +244,6 @@ theorem neg_zsmul (i : Int) (a : Q α) : zsmul (-i) a = neg (zsmul i a) := by
     · have : i = 0 := by omega
       simp [this]
 
-@[instance_reducible]
 def ofSemiring : Ring (Q α) := {
   nsmul := ⟨nsmul⟩
   zsmul := ⟨zsmul⟩
@@ -393,7 +392,7 @@ instance [LE α] [IsPreorder α] [OrderedAdd α] : IsPreorder (OfSemiring.Q α)
     obtain ⟨⟨a₁, a₂⟩⟩ := a
     change Q.mk _ ≤ Q.mk _
     simp only [mk_le_mk]
-    simp [Semiring.add_comm]
+    simp [Semiring.add_comm]; exact le_refl (a₁ + a₂)
   le_trans {a b c} h₁ h₂ := by
     induction a using Q.ind with | _ a
     induction b using Q.ind with | _ b
@@ -505,7 +504,6 @@ theorem mul_comm (a b : OfSemiring.Q α) : OfSemiring.mul a b = OfSemiring.mul b
   obtain ⟨⟨b₁, b₂⟩⟩ := b
   apply Quot.sound; refine ⟨0, ?_⟩; simp; ac_rfl
 
-@[instance_reducible]
 def ofCommSemiring : CommRing (OfSemiring.Q α) :=
   { OfSemiring.ofSemiring with
     mul_comm := mul_comm }

src/Init/Grind/Ring/Field.lean

@@ -33,7 +33,6 @@ class Field (α : Type u) extends CommRing α, Inv α, Div α where
   /-- Raising to a negative power is the inverse of raising to the positive power. -/
   zpow_neg : ∀ (a : α) (n : Int), a ^ (-n) = (a ^ n)⁻¹
 
-attribute [instance_reducible] Field.zpow
 attribute [instance 100] Field.toInv Field.toDiv Field.zpow
 
 namespace Field

src/Init/GrindInstances/Ring/SInt.lean

@@ -15,11 +15,11 @@ public section
 
 namespace Lean.Grind
 
-@[expose, instance_reducible]
+@[expose]
 def Int8.natCast : NatCast Int8 where
   natCast x := Int8.ofNat x
 
-@[expose, instance_reducible]
+@[expose]
 def Int8.intCast : IntCast Int8 where
   intCast x := Int8.ofInt x
 
@@ -70,11 +70,11 @@ example : ToInt.Sub Int8 (.sint 8) := inferInstance
 
 instance : ToInt.Pow Int8 (.sint 8) := ToInt.pow_of_semiring (by simp)
 
-@[expose, instance_reducible]
+@[expose]
 def Int16.natCast : NatCast Int16 where
   natCast x := Int16.ofNat x
 
-@[expose, instance_reducible]
+@[expose]
 def Int16.intCast : IntCast Int16 where
   intCast x := Int16.ofInt x
 
@@ -125,11 +125,11 @@ example : ToInt.Sub Int16 (.sint 16) := inferInstance
 
 instance : ToInt.Pow Int16 (.sint 16) := ToInt.pow_of_semiring (by simp)
 
-@[expose, instance_reducible]
+@[expose]
 def Int32.natCast : NatCast Int32 where
   natCast x := Int32.ofNat x
 
-@[expose, instance_reducible]
+@[expose]
 def Int32.intCast : IntCast Int32 where
   intCast x := Int32.ofInt x
 
@@ -180,11 +180,11 @@ example : ToInt.Sub Int32 (.sint 32) := inferInstance
 
 instance : ToInt.Pow Int32 (.sint 32) := ToInt.pow_of_semiring (by simp)
 
-@[expose, instance_reducible]
+@[expose]
 def Int64.natCast : NatCast Int64 where
   natCast x := Int64.ofNat x
 
-@[expose, instance_reducible]
+@[expose]
 def Int64.intCast : IntCast Int64 where
   intCast x := Int64.ofInt x
 
@@ -235,11 +235,11 @@ example : ToInt.Sub Int64 (.sint 64) := inferInstance
 
 instance : ToInt.Pow Int64 (.sint 64) := ToInt.pow_of_semiring (by simp)
 
-@[expose, instance_reducible]
+@[expose]
 def ISize.natCast : NatCast ISize where
   natCast x := ISize.ofNat x
 
-@[expose, instance_reducible]
+@[expose]
 def ISize.intCast : IntCast ISize where
   intCast x := ISize.ofInt x
 

src/Init/GrindInstances/Ring/UInt.lean

@@ -17,11 +17,11 @@ namespace UInt8
 /-- Variant of `UInt8.ofNat_mod_size` replacing `2 ^ 8` with `256`.-/
 theorem ofNat_mod_size' : ofNat (x % 256) = ofNat x := ofNat_mod_size
 
-@[expose, instance_reducible]
+@[expose]
 def natCast : NatCast UInt8 where
   natCast x := UInt8.ofNat x
 
-@[expose, instance_reducible]
+@[expose]
 def intCast : IntCast UInt8 where
   intCast x := UInt8.ofInt x
 
@@ -47,11 +47,11 @@ namespace UInt16
 /-- Variant of `UInt16.ofNat_mod_size` replacing `2 ^ 16` with `65536`.-/
 theorem ofNat_mod_size' : ofNat (x % 65536) = ofNat x := ofNat_mod_size
 
-@[expose, instance_reducible]
+@[expose]
 def natCast : NatCast UInt16 where
   natCast x := UInt16.ofNat x
 
-@[expose, instance_reducible]
+@[expose]
 def intCast : IntCast UInt16 where
   intCast x := UInt16.ofInt x
 
@@ -77,11 +77,11 @@ namespace UInt32
 /-- Variant of `UInt32.ofNat_mod_size` replacing `2 ^ 32` with `4294967296`.-/
 theorem ofNat_mod_size' : ofNat (x % 4294967296) = ofNat x := ofNat_mod_size
 
-@[expose, instance_reducible]
+@[expose]
 def natCast : NatCast UInt32 where
   natCast x := UInt32.ofNat x
 
-@[expose, instance_reducible]
+@[expose]
 def intCast : IntCast UInt32 where
   intCast x := UInt32.ofInt x
 
@@ -107,11 +107,11 @@ namespace UInt64
 /-- Variant of `UInt64.ofNat_mod_size` replacing `2 ^ 64` with `18446744073709551616`.-/
 theorem ofNat_mod_size' : ofNat (x % 18446744073709551616) = ofNat x := ofNat_mod_size
 
-@[expose, instance_reducible]
+@[expose]
 def natCast : NatCast UInt64 where
   natCast x := UInt64.ofNat x
 
-@[expose, instance_reducible]
+@[expose]
 def intCast : IntCast UInt64 where
   intCast x := UInt64.ofInt x
 
@@ -134,11 +134,11 @@ end UInt64
 
 namespace USize
 
-@[expose, instance_reducible]
+@[expose]
 def natCast : NatCast USize where
   natCast x := USize.ofNat x
 
-@[expose, instance_reducible]
+@[expose]
 def intCast : IntCast USize where
   intCast x := USize.ofInt x
 

src/Init/Internal/Order/Basic.lean

@@ -62,9 +62,9 @@ A chain is a totally ordered set (representing a set as a predicate).
 
 This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
 -/
-@[expose] def chain (c : α → Prop) : Prop := ∀ x y , c x → c y → x ⊑ y ∨ y ⊑ x
+def chain (c : α → Prop) : Prop := ∀ x y , c x → c y → x ⊑ y ∨ y ⊑ x
 
-@[expose] def is_sup {α : Sort u} [PartialOrder α] (c : α → Prop) (s : α) : Prop :=
+def is_sup {α : Sort u} [PartialOrder α] (c : α → Prop) (s : α) : Prop :=
   ∀ x, s ⊑ x ↔ (∀ y, c y → y ⊑ x)
 
 theorem is_sup_unique {α} [PartialOrder α] {c : α → Prop} {s₁ s₂ : α}

src/Init/Meta/Defs.lean

@@ -701,64 +701,36 @@ partial def expandMacros (stx : Syntax) (p : SyntaxNodeKind → Bool := fun k =>
 /-! # Helper functions for processing Syntax programmatically -/
 
 /--
-Creates an identifier with its position copied from `src`.
-
-To refer to a specific constant without a risk of variable capture, use `mkCIdentFrom` instead.
--/
+  Create an identifier copying the position from `src`.
+  To refer to a specific constant, use `mkCIdentFrom` instead. -/
 def mkIdentFrom (src : Syntax) (val : Name) (canonical := false) : Ident :=
   ⟨Syntax.ident (SourceInfo.fromRef src canonical) (Name.Internal.Meta.toString val).toRawSubstring val []⟩
 
-/--
-Creates an identifier with its position copied from the syntax returned by `getRef`.
-
-To refer to a specific constant without a risk of variable capture, use `mkCIdentFromRef` instead.
--/
 def mkIdentFromRef [Monad m] [MonadRef m] (val : Name) (canonical := false) : m Ident := do
   return mkIdentFrom (← getRef) val canonical
 
 /--
-Creates an identifier referring to a constant `c`. The identifier's position is copied from `src`.
-
-This variant of `mkIdentFrom` makes sure that the identifier cannot accidentally be captured.
--/
+  Create an identifier referring to a constant `c` copying the position from `src`.
+  This variant of `mkIdentFrom` makes sure that the identifier cannot accidentally
+  be captured. -/
 def mkCIdentFrom (src : Syntax) (c : Name) (canonical := false) : Ident :=
   -- Remark: We use the reserved macro scope to make sure there are no accidental collision with our frontend
   let id   := addMacroScope `_internal c reservedMacroScope
   ⟨Syntax.ident (SourceInfo.fromRef src canonical) (Name.Internal.Meta.toString id).toRawSubstring id [.decl c []]⟩
 
-/--
-Creates an identifier referring to a constant `c`. The identifier's position is copied from the
-syntax returned by `getRef`.
-
-This variant of `mkIdentFrom` makes sure that the identifier cannot accidentally be captured.
--/
 def mkCIdentFromRef [Monad m] [MonadRef m] (c : Name) (canonical := false) : m Syntax := do
   return mkCIdentFrom (← getRef) c canonical
 
-/--
-Creates an identifier that refers to a constant `c`. The identifier has no source position.
-
-This variant of `mkIdent` makes sure that the identifier cannot accidentally be captured.
--/
 def mkCIdent (c : Name) : Ident :=
   mkCIdentFrom Syntax.missing c
 
-/--
-Creates an identifier from a name. The resulting identifier has no source position.
--/
 @[export lean_mk_syntax_ident]
 def mkIdent (val : Name) : Ident :=
   ⟨Syntax.ident SourceInfo.none (Name.Internal.Meta.toString val).toRawSubstring val []⟩
 
-/--
-Creates a group node, as if it were parsed by `Lean.Parser.group`.
--/
 @[inline] def mkGroupNode (args : Array Syntax := #[]) : Syntax :=
   mkNode groupKind args
 
-/--
-Creates an array of syntax, separated by `sep`.
--/
 def mkSepArray (as : Array Syntax) (sep : Syntax) : Array Syntax := Id.run do
   let mut i := 0
   let mut r := #[]
@@ -770,45 +742,22 @@ def mkSepArray (as : Array Syntax) (sep : Syntax) : Array Syntax := Id.run do
     i := i + 1
   return r
 
-/--
-Creates an optional node.
-
-Optional nodes consist of null nodes that contain either zero or one element.
--/
 def mkOptionalNode (arg : Option Syntax) : Syntax :=
   match arg with
   | some arg => mkNullNode #[arg]
   | none     => mkNullNode #[]
 
-/--
-Creates a hole (`_`). The hole's position is copied from `ref`.
--/
 def mkHole (ref : Syntax) (canonical := false) : Syntax :=
   mkNode `Lean.Parser.Term.hole #[mkAtomFrom ref "_" canonical]
 
 namespace Syntax
 
-/--
-Creates the syntax of a separated array of items. `sep` is inserted between each item from `a`, and
-the result is wrapped in a null node.
--/
 def mkSep (a : Array Syntax) (sep : Syntax) : Syntax :=
   mkNullNode <| mkSepArray a sep
 
-/--
-Constructs a typed separated array from elements by adding suitable separators.
-The provided array should not include the separators.
-
-Like `Syntax.TSepArray.ofElems` but for untyped syntax.
--/
 def SepArray.ofElems {sep} (elems : Array Syntax) : SepArray sep :=
 ⟨mkSepArray elems (if String.Internal.isEmpty sep then mkNullNode else mkAtom sep)⟩
 
-/--
-Constructs a typed separated array from elements by adding suitable separators.
-The provided array should not include the separators.
-The generated separators' source location is that of the syntax returned by `getRef`.
--/
 def SepArray.ofElemsUsingRef [Monad m] [MonadRef m] {sep} (elems : Array Syntax) : m (SepArray sep) := do
   let ref ← getRef;
   return ⟨mkSepArray elems (if String.Internal.isEmpty sep then mkNullNode else mkAtomFrom ref sep)⟩
@@ -817,8 +766,8 @@ instance : Coe (Array Syntax) (SepArray sep) where
   coe := SepArray.ofElems
 
 /--
-Constructs a typed separated array from elements by adding suitable separators.
-The provided array should not include the separators.
+Constructs a typed separated array from elements.
+The given array does not include the separators.
 
 Like `Syntax.SepArray.ofElems` but for typed syntax.
 -/
@@ -828,77 +777,33 @@ def TSepArray.ofElems {sep} (elems : Array (TSyntax k)) : TSepArray k sep :=
 instance : Coe (TSyntaxArray k) (TSepArray k sep) where
   coe := TSepArray.ofElems
 
-/--
-Creates syntax representing a Lean term application, but avoids degenerate empty applications.
--/
+/-- Create syntax representing a Lean term application, but avoid degenerate empty applications. -/
 def mkApp (fn : Term) : (args : TSyntaxArray `term) → Term
   | #[]  => fn
   | args => ⟨mkNode `Lean.Parser.Term.app #[fn, mkNullNode args.raw]⟩
 
-/--
-Creates syntax representing a Lean constant application, but avoids degenerate empty applications.
--/
 def mkCApp (fn : Name) (args : TSyntaxArray `term) : Term :=
   mkApp (mkCIdent fn) args
 
-/--
-Creates a literal of the given kind. It is the caller's responsibility to ensure that the provided
-literal is a valid atom for the provided kind.
-
-If `info` is provided, then the literal's source information is copied from it.
--/
 def mkLit (kind : SyntaxNodeKind) (val : String) (info := SourceInfo.none) : TSyntax kind :=
   let atom : Syntax := Syntax.atom info val
   mkNode kind #[atom]
 
-/--
-Creates literal syntax for the given character.
-
-If `info` is provided, then the literal's source information is copied from it.
--/
 def mkCharLit (val : Char) (info := SourceInfo.none) : CharLit :=
   mkLit charLitKind (Char.quote val) info
 
-/--
-Creates literal syntax for the given string.
-
-If `info` is provided, then the literal's source information is copied from it.
--/
 def mkStrLit (val : String) (info := SourceInfo.none) : StrLit :=
   mkLit strLitKind (String.quote val) info
 
-/--
-Creates literal syntax for a number, which is provided as a string. The caller must ensure that the
-string is a valid token for the `num` token parser.
-
-If `info` is provided, then the literal's source information is copied from it.
--/
 def mkNumLit (val : String) (info := SourceInfo.none) : NumLit :=
   mkLit numLitKind val info
 
-/--
-Creates literal syntax for a natural number.
-
-If `info` is provided, then the literal's source information is copied from it.
--/
 def mkNatLit (val : Nat) (info := SourceInfo.none) : NumLit :=
   mkLit numLitKind (toString val) info
 
-/--
-Creates literal syntax for a number in scientific notation. The caller must ensure that the provided
-string is a valid scientific notation literal.
-
-If `info` is provided, then the literal's source information is copied from it.
--/
 def mkScientificLit (val : String) (info := SourceInfo.none) : TSyntax scientificLitKind :=
   mkLit scientificLitKind val info
 
-/--
-Creates literal syntax for a name. The caller must ensure that the provided string is a valid name
-literal.
-
-If `info` is provided, then the literal's source information is copied from it.
--/
 def mkNameLit (val : String) (info := SourceInfo.none) : NameLit :=
   mkLit nameLitKind val info
 
@@ -989,10 +894,9 @@ def isNatLit? (s : Syntax) : Option Nat :=
 def isFieldIdx? (s : Syntax) : Option Nat :=
   isNatLitAux fieldIdxKind s
 
-/--
-Decodes a 'scientific number' string which is consumed by the `OfScientific` class. Takes as input a
-string such as `123`, `123.456e7` and returns a triple `(n, sign, e)` with value given by
-`n * 10^-e` if `sign` else `n * 10^e`.
+/-- Decodes a 'scientific number' string which is consumed by the `OfScientific` class.
+  Takes as input a string such as `123`, `123.456e7` and returns a triple `(n, sign, e)` with value given by
+  `n * 10^-e` if `sign` else `n * 10^e`.
 -/
 partial def decodeScientificLitVal? (s : String) : Option (Nat × Bool × Nat) :=
   let len := String.Internal.length s
@@ -1382,17 +1286,8 @@ def HygieneInfo.mkIdent (s : HygieneInfo) (val : Name) (canonical := false) : Id
   let id := { extractMacroScopes src.getId with name := val.eraseMacroScopes }.review
   ⟨Syntax.ident (SourceInfo.fromRef src canonical) (Name.Internal.Meta.toString val).toRawSubstring id []⟩
 
-/--
-Converts a runtime value into surface syntax that denotes it.
-
-Instances do not need to guarantee that the resulting syntax will always re-elaborate into an
-equivalent value. For example, the syntax may omit implicit arguments that can usually be found
-automatically.
--/
+/-- Reflect a runtime datum back to surface syntax (best-effort). -/
 class Quote (α : Type) (k : SyntaxNodeKind := `term) where
-  /--
-  Returns syntax for the given value.
-  -/
   quote : α → TSyntax k
 
 export Quote (quote)
@@ -1543,19 +1438,12 @@ end Array
 
 namespace Lean.Syntax
 
-/--
-Extracts the non-separator elements of a separated array.
--/
 def SepArray.getElems (sa : SepArray sep) : Array Syntax :=
   sa.elemsAndSeps.getSepElems
 
-@[inherit_doc SepArray.getElems]
 def TSepArray.getElems (sa : TSepArray k sep) : TSyntaxArray k :=
   .mk sa.elemsAndSeps.getSepElems
 
-/--
-Adds an element to the end of a separated array, adding a separator as needed.
--/
 def TSepArray.push (sa : TSepArray k sep) (e : TSyntax k) : TSepArray k sep :=
   if sa.elemsAndSeps.isEmpty then
     { elemsAndSeps := #[e] }

src/Init/MetaTypes.lean

@@ -309,11 +309,6 @@ structure Config where
   -/
   suggestions : Bool := false
   /--
-  Maximum number of library suggestions to use. If `none`, uses the default limit.
-  Only relevant when `suggestions` is `true`.
-  -/
-  maxSuggestions : Option Nat := none
-  /--
   If `locals` is `true`, `simp` will unfold all definitions from the current file.
   For local theorems, use `+suggestions` instead.
   -/

src/Init/Prelude.lean

@@ -2478,7 +2478,7 @@ Examples:
  * `(if (5 : UInt8) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : UInt8) < 7) by decide`
 -/
-@[extern "lean_uint8_dec_lt", instance_reducible]
+@[extern "lean_uint8_dec_lt"]
 def UInt8.decLt (a b : UInt8) : Decidable (LT.lt a b) :=
   inferInstanceAs (Decidable (LT.lt a.toBitVec b.toBitVec))
 
@@ -2494,7 +2494,7 @@ Examples:
  * `(if (5 : UInt8) ≤ 15 then "yes" else "no") = "yes"`
  * `show (7 : UInt8) ≤ 7 by decide`
 -/
-@[extern "lean_uint8_dec_le", instance_reducible]
+@[extern "lean_uint8_dec_le"]
 def UInt8.decLe (a b : UInt8) : Decidable (LE.le a b) :=
   inferInstanceAs (Decidable (LE.le a.toBitVec b.toBitVec))
 
@@ -2638,7 +2638,7 @@ Examples:
  * `(if (5 : UInt32) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : UInt32) < 7) by decide`
 -/
-@[extern "lean_uint32_dec_lt", instance_reducible]
+@[extern "lean_uint32_dec_lt"]
 def UInt32.decLt (a b : UInt32) : Decidable (LT.lt a b) :=
   inferInstanceAs (Decidable (LT.lt a.toBitVec b.toBitVec))
 
@@ -2654,7 +2654,7 @@ Examples:
  * `(if (5 : UInt32) ≤ 15 then "yes" else "no") = "yes"`
  * `show (7 : UInt32) ≤ 7 by decide`
 -/
-@[extern "lean_uint32_dec_le", instance_reducible]
+@[extern "lean_uint32_dec_le"]
 def UInt32.decLe (a b : UInt32) : Decidable (LE.le a b) :=
   inferInstanceAs (Decidable (LE.le a.toBitVec b.toBitVec))
 

src/Init/Tactics.lean

@@ -1321,7 +1321,7 @@ structure DecideConfig where
   however kernel reduction ignores transparency settings. -/
   kernel : Bool := false
   /-- If true (default: false), then uses the native code compiler to evaluate the `Decidable` instance,
-  admitting the result via an axiom. This can be significantly more efficient,
+  admitting the result via the axiom `Lean.ofReduceBool`.  This can be significantly more efficient,
   but it is at the cost of increasing the trusted code base, namely the Lean compiler
   and all definitions with an `@[implemented_by]` attribute.
   The instance is only evaluated once. The `native_decide` tactic is a synonym for `decide +native`. -/
@@ -1351,7 +1351,7 @@ Options:
   It has two key properties: (1) since it uses the kernel, it ignores transparency and can unfold everything,
   and (2) it reduces the `Decidable` instance only once instead of twice.
 - `decide +native` uses the native code compiler (`#eval`) to evaluate the `Decidable` instance,
-  admitting the result via an axiom. This can be significantly more efficient than using reduction, but it is at the cost of increasing the size
+  admitting the result via the `Lean.ofReduceBool` axiom.
   This can be significantly more efficient than using reduction, but it is at the cost of increasing the size
   of the trusted code base.
   Namely, it depends on the correctness of the Lean compiler and all definitions with an `@[implemented_by]` attribute.
@@ -1412,7 +1412,7 @@ of `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this
 uses `#eval` to evaluate the decidability instance.
 
 This should be used with care because it adds the entire lean compiler to the trusted
-part, and a new axiom will show up in `#print axioms` for theorems using
+part, and the axiom `Lean.ofReduceBool` will show up in `#print axioms` for theorems using
 this method or anything that transitively depends on them. Nevertheless, because it is
 compiled, this can be significantly more efficient than using `decide`, and for very
 large computations this is one way to run external programs and trust the result.
@@ -1827,7 +1827,8 @@ In order to avoid calling a SAT solver every time, the proof can be cached with
 If solving your problem relies inherently on using associativity or commutativity, consider enabling
 the `bv.ac_nf` option.
 
-Note: `bv_decide` trusts the correctness of the code generator and adds a axioms asserting its result.
+
+Note: `bv_decide` uses `ofReduceBool` and thus trusts the correctness of the code generator.
 
 Note: include `import Std.Tactic.BVDecide`
 -/

src/Lean.lean

@@ -47,4 +47,3 @@ public import Lean.ErrorExplanation
 public import Lean.DefEqAttrib
 public import Lean.Shell
 public import Lean.ExtraModUses
-public import Lean.OriginalConstKind

src/Lean/AddDecl.lean

@@ -8,8 +8,6 @@ module
 prelude
 public import Lean.Meta.Sorry
 public import Lean.Util.CollectAxioms
-public import Lean.OriginalConstKind
-import all Lean.OriginalConstKind  -- for accessing `privateConstKindsExt`
 
 public section
 
@@ -47,6 +45,28 @@ where go env
   | .str p _ => if isNamespaceName p then go (env.registerNamespace p) p else env
   | _        => env
 
+private builtin_initialize privateConstKindsExt : MapDeclarationExtension ConstantKind ←
+  -- Use `sync` so we can add entries from anywhere without restrictions
+  mkMapDeclarationExtension (asyncMode := .sync)
+
+/--
+Returns the kind of the declaration as originally declared instead of as exported. This information
+is stored by `Lean.addDecl` and may be inaccurate if that function was circumvented. Returns `none`
+if the declaration was not found.
+-/
+def getOriginalConstKind? (env : Environment) (declName : Name) : Option ConstantKind := do
+  -- Use `local` as for asynchronous decls from the current module, `findAsync?` below will yield
+  -- the same result but potentially earlier (after `addConstAsync` instead of `addDecl`)
+  privateConstKindsExt.find? (asyncMode := .local) env declName <|>
+    (env.setExporting false |>.findAsync? declName).map (·.kind)
+
+/--
+Checks whether the declaration was originally declared as a theorem; see also
+`Lean.getOriginalConstKind?`. Returns `false` if the declaration was not found.
+-/
+def wasOriginallyTheorem (env : Environment) (declName : Name) : Bool :=
+  getOriginalConstKind? env declName |>.map (· matches .thm) |>.getD false
+
 /-- If `warn.sorry` is set to true, then, so long as the message log does not already have any errors,
 declarations with `sorryAx` generate the "declaration uses `sorry`" warning. -/
 register_builtin_option warn.sorry : Bool := {

src/Lean/Class.lean

@@ -4,10 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
+
 prelude
 public import Lean.Attributes
-import Lean.Util.CollectLevelParams
+
 public section
+
 namespace Lean
 
 /-- An entry for the persistent environment extension for declared type classes -/
@@ -15,21 +17,14 @@ structure ClassEntry where
   /-- Class name. -/
   name      : Name
   /--
-  Position of the class `outParams`.
-  For example, for class
-  ```
-  class GetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w)) (dom : outParam (cont → idx → Prop)) where
-  ```
-  `outParams := #[2, 3]`
+    Position of the class `outParams`.
+    For example, for class
+    ```
+    class GetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w)) (dom : outParam (cont → idx → Prop)) where
+    ```
+    `outParams := #[2, 3]`
   -/
   outParams : Array Nat
-  /--
-  Positions of universe level parameters that only appear in output parameter types.
-  For example, for `HAdd (α : Type u) (β : Type v) (γ : outParam (Type w))`,
-  `outLevelParams := #[2]` since universe `w` only appears in the output parameter `γ`.
-  This is used to normalize TC resolution cache keys.
-  -/
-  outLevelParams : Array Nat
 
 namespace ClassEntry
 
@@ -41,15 +36,12 @@ end ClassEntry
 /-- State of the type class environment extension. -/
 structure ClassState where
   outParamMap : SMap Name (Array Nat) := SMap.empty
-  outLevelParamMap : SMap Name (Array Nat) := SMap.empty
   deriving Inhabited
 
 namespace ClassState
 
 def addEntry (s : ClassState) (entry : ClassEntry) : ClassState :=
-  { s with
-    outParamMap := s.outParamMap.insert entry.name entry.outParams
-    outLevelParamMap := s.outLevelParamMap.insert entry.name entry.outLevelParams }
+  { s with outParamMap := s.outParamMap.insert entry.name entry.outParams }
 
 /--
 Switch the state into persistent mode. We switch to this mode after
@@ -57,9 +49,7 @@ we read all imported .olean files.
 Recall that we use a `SMap` for implementing the state of the type class environment extension.
 -/
 def switch (s : ClassState) : ClassState :=
-  { s with
-    outParamMap := s.outParamMap.switch
-    outLevelParamMap := s.outLevelParamMap.switch }
+  { s with outParamMap := s.outParamMap.switch }
 
 end ClassState
 
@@ -89,10 +79,6 @@ def hasOutParams (env : Environment) (declName : Name) : Bool :=
   | some outParams => !outParams.isEmpty
   | none => false
 
-/-- If `declName` is a class, return the positions of universe level parameters that only appear in output parameter types. -/
-def getOutLevelParamPositions? (env : Environment) (declName : Name) : Option (Array Nat) :=
-  (classExtension.getState env).outLevelParamMap.find? declName
-
 /--
   Auxiliary function for collection the position class `outParams`, and
   checking whether they are being correctly used.
@@ -160,39 +146,6 @@ where
         keepBinderInfo ()
     | _ => type
 
-/--
-Compute positions of universe level parameters that only appear in output parameter types.
-
-During type class resolution, the cache key for a query like
-`HAppend.{0, 0, ?u} (BitVec 8) (BitVec 8) ?m` should be independent of the specific
-metavariable IDs in output parameter positions. To achieve this, output parameter arguments
-are erased from the cache key. However, universe levels that only appear in output parameter
-types (e.g., `?u` corresponding to the result type's universe) must also be erased to avoid
-cache misses when the same query is issued with different universe metavariable IDs.
-
-This function identifies which universe level parameter positions are "output-only" by
-collecting all level param names that appear in non-output parameter domains, then returning
-the positions of any level params not in that set.
--/
-private partial def computeOutLevelParams (type : Expr) (outParams : Array Nat) (levelParams : List Name) : Array Nat := Id.run do
-  let nonOutLevels := go type 0 {} |>.params
-  let mut result := #[]
-  let mut i := 0
-  for name in levelParams do
-    unless nonOutLevels.contains name do
-      result := result.push i
-    i := i + 1
-  result
-where
-  go (type : Expr) (i : Nat) (s : CollectLevelParams.State) : CollectLevelParams.State :=
-    match type with
-    | .forallE _ d b _ =>
-      if outParams.contains i then
-        go b (i + 1) s
-      else
-        go b (i + 1) (collectLevelParams s d)
-    | _ => s
-
 /--
 Add a new type class with the given name to the environment.
 `declName` must not be the name of an existing type class,
@@ -208,8 +161,7 @@ def addClass (env : Environment) (clsName : Name) : Except MessageData Environme
   unless decl matches .inductInfo .. | .axiomInfo .. do
     throw m!"invalid 'class', declaration '{.ofConstName clsName}' must be inductive datatype, structure, or constant"
   let outParams ← checkOutParam 0 #[] #[] decl.type
-  let outLevelParams := computeOutLevelParams decl.type outParams decl.levelParams
-  return classExtension.addEntry env { name := clsName, outParams, outLevelParams }
+  return classExtension.addEntry env { name := clsName, outParams }
 
 /--
 Registers an inductive type or structure as a type class. Using `class` or `class inductive` is

src/Lean/Compiler/IR.lean

@@ -47,6 +47,8 @@ def compile (decls : Array Decl) : CompilerM (Array Decl) := do
   logDecls `init decls
   checkDecls decls
   let mut decls := decls
+  decls := decls.map Decl.pushProj
+  logDecls `push_proj decls
   if compiler.reuse.get (← getOptions) then
     decls := decls.map (Decl.insertResetReuse (← getEnv))
     logDecls `reset_reuse decls

src/Lean/Compiler/IR/AddExtern.lean

@@ -9,9 +9,6 @@ module
 prelude
 public import Lean.Compiler.IR.Boxing
 import Lean.Compiler.IR.RC
-import Lean.Compiler.LCNF.ToImpureType
-import Lean.Compiler.LCNF.ToImpure
-import Lean.Compiler.LCNF.ToImpureType
 
 public section
 
@@ -19,60 +16,23 @@ namespace Lean.IR
 
 @[export lean_add_extern]
 def addExtern (declName : Name) (externAttrData : ExternAttrData) : CoreM Unit := do
+  let mut type ← Compiler.LCNF.getOtherDeclMonoType declName
+  let mut params := #[]
+  let mut nextVarIndex := 0
+  repeat
+    let .forallE _ d b _ := type | break
+    let borrow := isMarkedBorrowed d
+    let ty ← toIRType d
+    params := params.push { x := ⟨nextVarIndex⟩, borrow, ty }
+    type := b
+    nextVarIndex := nextVarIndex + 1
+  let irType ← toIRType type
+  let decls := #[.extern declName params irType externAttrData]
   if !isPrivateName declName then
     modifyEnv (Compiler.LCNF.setDeclPublic · declName)
-  let monoDecl ← addMono declName
-  let impureDecl ← addImpure monoDecl
-  addIr impureDecl
-where
-  addMono (declName : Name) : CoreM (Compiler.LCNF.Decl .pure) := do
-    let type ← Compiler.LCNF.getOtherDeclMonoType declName
-    let mut typeIter := type
-    let mut params := #[]
-    repeat
-      let .forallE binderName ty b _ := typeIter | break
-      let borrow := isMarkedBorrowed ty
-      params := params.push {
-        fvarId := (← mkFreshFVarId)
-        type := ty,
-        binderName,
-        borrow
-      }
-      typeIter := b
-    let decl := {
-      name := declName,
-      levelParams := [],
-      value := .extern externAttrData,
-      inlineAttr? := some .noinline,
-      type,
-      params,
-    }
-    decl.saveMono
-    return decl
-
-  addImpure (decl : Compiler.LCNF.Decl .pure) : CoreM (Compiler.LCNF.Decl .impure) := do
-    let type ← Compiler.LCNF.lowerResultType decl.type decl.params.size
-    let params ← decl.params.mapM fun param =>
-      return { param with type := ← Compiler.LCNF.toImpureType param.type }
-    let decl := {
-      name := decl.name,
-      levelParams := decl.levelParams,
-      value := .extern externAttrData
-      inlineAttr? := some .noinline,
-      type,
-      params
-    }
-    decl.saveImpure
-    return decl
-
-  addIr (decl : Compiler.LCNF.Decl .impure) : CoreM Unit := do
-    let params := decl.params.mapIdx fun idx param =>
-      { x := ⟨idx⟩, borrow := param.borrow, ty := toIRType param.type  }
-    let type := toIRType decl.type
-    let decls := #[.extern declName params type externAttrData]
-    let decls := ExplicitBoxing.addBoxedVersions (← Lean.getEnv) decls
-    let decls ← explicitRC decls
-    logDecls `result decls
-    addDecls decls
+  let decls := ExplicitBoxing.addBoxedVersions (← Lean.getEnv) decls
+  let decls ← explicitRC decls
+  logDecls `result decls
+  addDecls decls
 
 end Lean.IR

src/Lean/Compiler/IR/ToIR.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Lean.Compiler.IR.CompilerM
-import Lean.Compiler.IR.ToIRType
+public import Lean.Compiler.IR.ToIRType
 
 public section
 
@@ -15,22 +15,48 @@ namespace Lean.IR
 
 open Lean.Compiler (LCNF.Alt LCNF.Arg LCNF.Code LCNF.Decl LCNF.DeclValue LCNF.LCtx LCNF.LetDecl
   LCNF.LetValue LCNF.LitValue LCNF.Param LCNF.getMonoDecl? LCNF.FVarSubst LCNF.MonadFVarSubst
-  LCNF.MonadFVarSubstState LCNF.addSubst LCNF.normLetValue LCNF.normFVar LCNF.getType LCNF.CtorInfo)
+  LCNF.MonadFVarSubstState LCNF.addSubst LCNF.normLetValue LCNF.normFVar)
 
 namespace ToIR
 
+/--
+Marks an extern definition to be guaranteed to always return tagged values.
+This information is used to optimize reference counting in the compiler.
+-/
+@[builtin_doc]
+builtin_initialize taggedReturnAttr : TagAttribute ←
+  registerTagAttribute `tagged_return "mark extern definition to always return tagged values"
+
 structure BuilderState where
   vars : Std.HashMap FVarId Arg := {}
   joinPoints : Std.HashMap FVarId JoinPointId := {}
   nextId : Nat := 1
+  /--
+  We keep around a substitution here because we run a second trivial structure elimination when
+  converting to IR. This elimination is aware of the fact that `Void` is irrelevant while the first
+  one in LCNF isn't because LCNF is still pure. However, IR does not allow us to have bindings of
+  the form `let x := y` which might occur when for example projecting out of a trivial structure
+  where previously a binding would've been `let x := proj y i` and now becomes `let x := y`.
+  For this reason we carry around these kinds of bindings in this substitution and apply it whenever
+  we access an fvar in the conversion.
+  -/
+  subst : LCNF.FVarSubst .pure := {}
 
 abbrev M := StateRefT BuilderState CoreM
 
+instance : LCNF.MonadFVarSubst M .pure false where
+  getSubst := return (← get).subst
+
+instance : LCNF.MonadFVarSubstState M .pure where
+  modifySubst f := modify fun s => { s with subst := f s.subst }
+
 def M.run (x : M α) : CoreM α := do
   x.run' {}
 
 def getFVarValue (fvarId : FVarId) : M Arg := do
-  return (← get).vars.get! fvarId
+  match ← LCNF.normFVar fvarId with
+  | .fvar fvarId => return (← get).vars.get! fvarId
+  | .erased => return .erased
 
 def getJoinPointValue (fvarId : FVarId) : M JoinPointId := do
   return (← get).joinPoints.get! fvarId
@@ -41,6 +67,14 @@ def bindVar (fvarId : FVarId) : M VarId := do
     ⟨varId, { s with vars := s.vars.insertIfNew fvarId (.var varId),
                      nextId := s.nextId + 1 }⟩
 
+def bindVarToVarId (fvarId : FVarId) (varId : VarId) : M Unit := do
+  modify fun s => { s with vars := s.vars.insertIfNew fvarId (.var varId) }
+
+def newVar : M VarId := do
+  modifyGet fun s =>
+    let varId := { idx := s.nextId }
+    ⟨varId, { s with nextId := s.nextId + 1 }⟩
+
 def bindJoinPoint (fvarId : FVarId) : M JoinPointId := do
   modifyGet fun s =>
     let joinPointId := { idx := s.nextId }
@@ -50,6 +84,9 @@ def bindJoinPoint (fvarId : FVarId) : M JoinPointId := do
 def bindErased (fvarId : FVarId) : M Unit := do
   modify fun s => { s with vars := s.vars.insertIfNew fvarId .erased }
 
+def findDecl (n : Name) : M (Option Decl) :=
+  return findEnvDecl (← Lean.getEnv) n
+
 def addDecl (d : Decl) : M Unit :=
   Lean.modifyEnv fun env => declMapExt.addEntry env d
 
@@ -65,22 +102,34 @@ def lowerLitValue (v : LCNF.LitValue) : LitVal × IRType :=
   | .uint64 v => ⟨.num (UInt64.toNat v), .uint64⟩
   | .usize v => ⟨.num (UInt64.toNat v), .usize⟩
 
-def lowerArg (a : LCNF.Arg .impure) : M Arg := do
+def lowerArg (a : LCNF.Arg .pure) : M Arg := do
   match a with
   | .fvar fvarId => getFVarValue fvarId
-  | .erased => return .erased
+  | .erased | .type .. => return .erased
 
-def lowerParam (p : LCNF.Param .impure) : M Param := do
+inductive TranslatedProj where
+  | expr (e : Expr)
+  | erased
+  deriving Inhabited
+
+def lowerProj (base : VarId) (ctorInfo : CtorInfo) (field : CtorFieldInfo)
+    : TranslatedProj × IRType :=
+  match field with
+  | .object i irType => ⟨.expr (.proj i base), irType⟩
+  | .usize i => ⟨.expr (.uproj i base), .usize⟩
+  | .scalar _ offset irType => ⟨.expr (.sproj (ctorInfo.size + ctorInfo.usize) offset base), irType⟩
+  | .erased => ⟨.erased, .erased⟩
+  | .void => ⟨.erased, .void⟩
+
+def lowerParam (p : LCNF.Param .pure) : M Param := do
   let x ← bindVar p.fvarId
-  let ty := toIRType p.type
+  let ty ← toIRType p.type
+  if ty.isVoid || ty.isErased then
+    Compiler.LCNF.addSubst p.fvarId (.erased : LCNF.Arg .pure)
   return { x, borrow := p.borrow, ty }
 
-@[inline]
-def lowerCtorInfo (i : LCNF.CtorInfo) : CtorInfo :=
-  ⟨i.name, i.cidx, i.size, i.usize, i.ssize⟩
-
 mutual
-partial def lowerCode (c : LCNF.Code .impure) : M FnBody := do
+partial def lowerCode (c : LCNF.Code .pure) : M FnBody := do
   match c with
   | .let decl k => lowerLet decl k
   | .jp decl k =>
@@ -92,75 +141,222 @@ partial def lowerCode (c : LCNF.Code .impure) : M FnBody := do
     let joinPointId ← getJoinPointValue fvarId
     return .jmp joinPointId (← args.mapM lowerArg)
   | .cases cases =>
-    let .var varId := (← getFVarValue cases.discr) | unreachable!
-    return .case cases.typeName
-                 varId
-                 (nameToIRType cases.typeName)
-                 (← cases.alts.mapM (lowerAlt))
+    if let some info ← hasTrivialStructure? cases.typeName then
+      assert! cases.alts.size == 1
+      let .alt ctorName ps k := cases.alts[0]! | unreachable!
+      assert! ctorName == info.ctorName
+      assert! info.fieldIdx < ps.size
+      for idx in 0...ps.size do
+        let p := ps[idx]!
+        if idx == info.fieldIdx then
+          LCNF.addSubst p.fvarId (.fvar cases.discr : LCNF.Arg .pure)
+        else
+          bindErased p.fvarId
+      lowerCode k
+    else
+      -- `casesOn` for inductive predicates should have already been expanded.
+      let .var varId := (← getFVarValue cases.discr) | unreachable!
+      return .case cases.typeName
+                   varId
+                   (← nameToIRType cases.typeName)
+                   (← cases.alts.mapM (lowerAlt varId))
   | .return fvarId =>
-    let ret ← getFVarValue fvarId
-    return .ret ret
+    return .ret (← getFVarValue fvarId)
   | .unreach .. => return .unreachable
-  | .sset var i offset y type k _ =>
-    let .var y ← getFVarValue y | unreachable!
-    let .var var ← getFVarValue var | unreachable!
-    return .sset var i offset y (toIRType type) (← lowerCode k)
-  | .uset var i y k _ =>
-    let .var y ← getFVarValue y | unreachable!
-    let .var var ← getFVarValue var | unreachable!
-    return .uset var i y (← lowerCode k)
   | .fun .. => panic! "all local functions should be λ-lifted"
 
-partial def lowerLet (decl : LCNF.LetDecl .impure) (k : LCNF.Code .impure) : M FnBody := do
-  let type := toIRType decl.type
-  let continueLet (e : Expr) : M FnBody := do
-    let letVar ← bindVar decl.fvarId
-    return .vdecl letVar type e (← lowerCode k)
-  match decl.value with
+partial def lowerLet (decl : LCNF.LetDecl .pure) (k : LCNF.Code .pure) : M FnBody := do
+  let value ← LCNF.normLetValue decl.value
+  match value with
   | .lit litValue =>
-    let ⟨litValue, _⟩ := lowerLitValue litValue
-    continueLet (.lit litValue)
-  | .oproj i var _ =>
-    withGetFVarValue var fun var =>
-      continueLet (.proj i var)
-  | .uproj i var _ =>
-    withGetFVarValue var fun var =>
-      continueLet (.uproj i var)
-  | .sproj i offset var _ =>
-    withGetFVarValue var fun var =>
-      continueLet (.sproj i offset var)
-  | .ctor info args _ => continueLet (.ctor (lowerCtorInfo info) (← args.mapM lowerArg))
-  | .fap fn args => continueLet (.fap fn (← args.mapM lowerArg))
-  | .pap fn args => continueLet (.pap fn (← args.mapM lowerArg))
+    let var ← bindVar decl.fvarId
+    let ⟨litValue, type⟩ := lowerLitValue litValue
+    return .vdecl var type (.lit litValue) (← lowerCode k)
+  | .proj typeName i fvarId =>
+    if let some info ← hasTrivialStructure? typeName then
+      if info.fieldIdx == i then
+        LCNF.addSubst decl.fvarId (.fvar fvarId : LCNF.Arg .pure)
+      else
+        bindErased decl.fvarId
+      lowerCode k
+    else
+      match (← getFVarValue fvarId) with
+      | .var varId =>
+        let some (.inductInfo { ctors := [ctorName], .. }) := (← Lean.getEnv).find? typeName
+          | panic! "projection of non-structure type"
+        let ⟨ctorInfo, fields⟩ ← getCtorLayout ctorName
+        let ⟨result, type⟩ := lowerProj varId ctorInfo fields[i]!
+        match result with
+        | .expr e =>
+          let var ← bindVar decl.fvarId
+          return .vdecl var type e (← lowerCode k)
+        | .erased =>
+          bindErased decl.fvarId
+          lowerCode k
+      | .erased =>
+        bindErased decl.fvarId
+        lowerCode k
+  | .const name _ args =>
+    let irArgs ← args.mapM lowerArg
+    if let some decl ← findDecl name then
+      return (← mkApplication name decl.params.size irArgs)
+    if let some decl ← LCNF.getMonoDecl? name then
+      return (← mkApplication name decl.params.size irArgs)
+    let env ← Lean.getEnv
+    match env.find? name with
+    | some (.ctorInfo ctorVal) =>
+      if let some info ← hasTrivialStructure? ctorVal.induct then
+        let arg := args[info.numParams + info.fieldIdx]!
+        LCNF.addSubst decl.fvarId arg
+        lowerCode k
+      else
+        let type ← nameToIRType ctorVal.induct
+        if type.isScalar then
+          let var ← bindVar decl.fvarId
+          return .vdecl var type (.lit (.num ctorVal.cidx)) (← lowerCode k)
+
+        let ⟨ctorInfo, fields⟩ ← getCtorLayout name
+        let irArgs := irArgs.extract (start := ctorVal.numParams)
+        if irArgs.size != fields.size then
+          -- An overapplied constructor arises from compiler
+          -- transformations on unreachable code
+          return .unreachable
+
+        let objArgs : Array Arg ← do
+          let mut result : Array Arg := #[]
+          for h : i in *...fields.size do
+            match fields[i] with
+            | .object .. =>
+              result := result.push irArgs[i]!
+            | .usize .. | .scalar .. | .erased | .void => pure ()
+          pure result
+        let objVar ← bindVar decl.fvarId
+        let rec lowerNonObjectFields (_ : Unit) : M FnBody :=
+          let rec loop (i : Nat) : M FnBody := do
+            match irArgs[i]? with
+            | some (.var varId) =>
+              match fields[i]! with
+              | .usize usizeIdx =>
+                let k ← loop (i + 1)
+                return .uset objVar usizeIdx varId k
+              | .scalar _ offset argType =>
+                let k ← loop (i + 1)
+                return .sset objVar (ctorInfo.size + ctorInfo.usize) offset varId argType k
+              | .object .. | .erased | .void => loop (i + 1)
+            | some .erased => loop (i + 1)
+            | none => lowerCode k
+          loop 0
+        return .vdecl objVar ctorInfo.type (.ctor ctorInfo objArgs) (← lowerNonObjectFields ())
+    | some (.defnInfo ..) | some (.opaqueInfo ..) =>
+      mkFap name irArgs
+    | some (.axiomInfo ..) | .some (.quotInfo ..) | .some (.inductInfo ..) | .some (.thmInfo ..) =>
+      -- Should have been caught by `ToLCNF`
+      throwError f!"ToIR: unexpected use of noncomputable declaration `{name}`; please report this issue"
+    | some (.recInfo ..) =>
+      throwError f!"code generator does not support recursor `{name}` yet, consider using 'match ... with' and/or structural recursion"
+    | none => panic! "reference to unbound name"
   | .fvar fvarId args =>
-    withGetFVarValue fvarId fun id => do
+    match (← getFVarValue fvarId) with
+    | .var id =>
       let irArgs ← args.mapM lowerArg
-      continueLet (.ap id irArgs)
+      mkAp id irArgs
+    | .erased => mkErased ()
   | .erased => mkErased ()
 where
+  mkVar (v : VarId) : M FnBody := do
+    bindVarToVarId decl.fvarId v
+    lowerCode k
+
   mkErased (_ : Unit) : M FnBody := do
     bindErased decl.fvarId
     lowerCode k
 
-  withGetFVarValue (fvarId : FVarId) (f : VarId → M FnBody) : M FnBody := do
-    match (← getFVarValue fvarId) with
-    | .var id => f id
-    | .erased => mkErased ()
+  mkFap (name : Name) (args : Array Arg) : M FnBody := do
+    let var ← bindVar decl.fvarId
+    let type ← toIRType decl.type
+    return .vdecl var type (.fap name args) (← lowerCode k)
 
-partial def lowerAlt (a : LCNF.Alt .impure) : M Alt := do
+  mkPap (name : Name) (args : Array Arg) : M FnBody := do
+    let var ← bindVar decl.fvarId
+    return .vdecl var .object (.pap name args) (← lowerCode k)
+
+  mkAp (fnVar : VarId) (args : Array Arg) : M FnBody := do
+    let var ← bindVar decl.fvarId
+    let type := (← toIRType decl.type).boxed
+    return .vdecl var type (.ap fnVar args) (← lowerCode k)
+
+  mkOverApplication (name : Name) (numParams : Nat) (args : Array Arg) : M FnBody := do
+    let var ← bindVar decl.fvarId
+    let type := (← toIRType decl.type).boxed
+    let tmpVar ← newVar
+    let firstArgs := args.extract 0 numParams
+    let restArgs := args.extract numParams args.size
+    return .vdecl tmpVar .object (.fap name firstArgs) <|
+           .vdecl var type (.ap tmpVar restArgs) (← lowerCode k)
+
+  mkApplication (name : Name) (numParams : Nat) (args : Array Arg) : M FnBody := do
+    let numArgs := args.size
+    if numArgs < numParams then
+      mkPap name args
+    else if numArgs == numParams then
+      mkFap name args
+    else
+      mkOverApplication name numParams args
+
+partial def lowerAlt (discr : VarId) (a : LCNF.Alt .pure) : M Alt := do
   match a with
-  | .ctorAlt info k => return .ctor (lowerCtorInfo info) (← lowerCode k)
-  | .default code => return .default (← lowerCode code)
+  | .alt ctorName params code =>
+    let ⟨ctorInfo, fields⟩ ← getCtorLayout ctorName
+    let lowerParams (params : Array (LCNF.Param .pure)) (fields : Array CtorFieldInfo) : M FnBody := do
+      let rec loop (i : Nat) : M FnBody := do
+        match params[i]?, fields[i]? with
+        | some param, some field =>
+          let ⟨result, type⟩ := lowerProj discr ctorInfo field
+          match result with
+          | .expr e =>
+            return .vdecl (← bindVar param.fvarId)
+                          type
+                          e
+                          (← loop (i + 1))
+          | .erased =>
+            bindErased param.fvarId
+            loop (i + 1)
+        | none, none => lowerCode code
+        | _, _ => panic! "mismatched fields and params"
+      loop 0
+    let body ← lowerParams params fields
+    return .ctor ctorInfo body
+  | .default code =>
+    return .default (← lowerCode code)
 end
 
-def lowerDecl (d : LCNF.Decl .impure) : M (Option Decl) := do
+def lowerResultType (type : Lean.Expr) (arity : Nat) : M IRType :=
+  toIRType (resultTypeForArity type arity)
+where resultTypeForArity (type : Lean.Expr) (arity : Nat) : Lean.Expr :=
+  if arity == 0 then
+    type
+  else
+    match type with
+    | .forallE _ _ b _ => resultTypeForArity b (arity - 1)
+    | .const ``lcErased _ => mkConst ``lcErased
+    | _ => panic! "invalid arity"
+
+def lowerDecl (d : LCNF.Decl .pure) : M (Option Decl) := do
   let params ← d.params.mapM lowerParam
-  let resultType := toIRType d.type
+  let mut resultType ← lowerResultType d.type d.params.size
+  let taggedReturn := taggedReturnAttr.hasTag (← getEnv) d.name
   match d.value with
   | .code code =>
+    if taggedReturn then
+      throwError m!"Error while compiling function '{d.name}': @[tagged_return] is only valid for extern declarations"
     let body ← lowerCode code
     pure <| some <| .fdecl d.name params resultType body {}
   | .extern externAttrData =>
+    if taggedReturn then
+      if resultType.isScalar then
+        throwError m!"@[tagged_return] on function '{d.name}' with scalar return type {resultType}"
+      else
+        resultType := .tagged
     if externAttrData.entries.isEmpty then
       -- TODO: This matches the behavior of the old compiler, but we should
       -- find a better way to handle this.
@@ -171,7 +367,7 @@ def lowerDecl (d : LCNF.Decl .impure) : M (Option Decl) := do
 
 end ToIR
 
-def toIR (decls: Array (LCNF.Decl .impure)) : CoreM (Array Decl) := do
+def toIR (decls: Array (LCNF.Decl .pure)) : CoreM (Array Decl) := do
   let mut irDecls := #[]
   for decl in decls do
     if let some irDecl ← ToIR.lowerDecl decl |>.run then

src/Lean/Compiler/IR/ToIRType.lean

@@ -14,39 +14,237 @@ public section
 namespace Lean
 namespace IR
 
-open Lean.Compiler
+open Lean.Compiler (LCNF.CacheExtension LCNF.isTypeFormerType LCNF.toLCNFType LCNF.toMonoType
+  LCNF.TrivialStructureInfo LCNF.getOtherDeclBaseType LCNF.getParamTypes LCNF.instantiateForall
+  LCNF.Irrelevant.hasTrivialStructure?)
 
-def nameToIRType (n : Name) : IRType :=
-  match n with
-  | ``Float => .float
-  | ``Float32 => .float32
-  | ``UInt8 => .uint8
-  | ``UInt16 => .uint16
-  | ``UInt32 => .uint32
-  | ``UInt64 => .uint64
-  | ``lcErased => .erased
-  | `obj => .object
-  | `tobj => .tobject
-  | `tagged => .tagged
-  | ``lcVoid => .void
-  | _ => unreachable!
+def irTypeForEnum (numCtors : Nat) : IRType :=
+  if numCtors == 1 then
+    .tagged
+  else if numCtors < Nat.pow 2 8 then
+    .uint8
+  else if numCtors < Nat.pow 2 16 then
+    .uint16
+  else if numCtors < Nat.pow 2 32 then
+    .uint32
+  else
+    .tagged
 
+builtin_initialize irTypeExt : LCNF.CacheExtension Name IRType ←
+  LCNF.CacheExtension.register
 
-def toIRType (type : Lean.Expr) : IRType :=
+builtin_initialize trivialStructureInfoExt :
+    LCNF.CacheExtension Name (Option LCNF.TrivialStructureInfo) ←
+  LCNF.CacheExtension.register
+
+/--
+The idea of this function is the same as in `ToMono`, however the notion of "irrelevancy" has
+changed because we now have the `void` type which can only be erased in impure context and thus at
+earliest at the conversion from mono to IR.
+-/
+def hasTrivialStructure? (declName : Name) : CoreM (Option LCNF.TrivialStructureInfo) := do
+  let isVoidType type := do
+    let type ← Meta.whnfD type
+    return type matches .proj ``Subtype 0 (.app (.const ``Void.nonemptyType []) _)
+  let irrelevantType type :=
+    Meta.isProp type <||> Meta.isTypeFormerType type <||> isVoidType type
+  LCNF.Irrelevant.hasTrivialStructure? trivialStructureInfoExt irrelevantType declName
+
+def nameToIRType (name : Name) : CoreM IRType := do
+  match (← irTypeExt.find? name) with
+  | some type => return type
+  | none =>
+    let type ← fillCache
+    irTypeExt.insert name type
+    return type
+where fillCache : CoreM IRType := do
+    match name with
+    | ``UInt8 => return .uint8
+    | ``UInt16 => return .uint16
+    | ``UInt32 => return .uint32
+    | ``UInt64 => return .uint64
+    | ``USize => return .usize
+    | ``Float => return .float
+    | ``Float32 => return .float32
+    | ``lcErased => return .erased
+    -- `Int` is specified as an inductive type with two constructors that have relevant arguments,
+    -- but it has the same runtime representation as `Nat` and thus needs to be special-cased here.
+    | ``Int => return .tobject
+    | ``lcVoid => return .void
+    | _ =>
+      let env ← Lean.getEnv
+      let some (.inductInfo inductiveVal) := env.find? name | return .tobject
+      let ctorNames := inductiveVal.ctors
+      let numCtors := ctorNames.length
+      let mut numScalarCtors := 0
+      for ctorName in ctorNames do
+        let some (.ctorInfo ctorInfo) := env.find? ctorName | unreachable!
+        let hasRelevantField ← Meta.MetaM.run' <|
+                               Meta.forallTelescope ctorInfo.type fun params _ => do
+          for field in params[ctorInfo.numParams...*] do
+            let fieldType ← field.fvarId!.getType
+            let lcnfFieldType ← LCNF.toLCNFType fieldType
+            let monoFieldType ← LCNF.toMonoType lcnfFieldType
+            if !monoFieldType.isErased then return true
+          return false
+        if !hasRelevantField then
+          numScalarCtors := numScalarCtors + 1
+      if numScalarCtors == numCtors then
+        return irTypeForEnum numCtors
+      else if numScalarCtors == 0 then
+        return .object
+      else
+        return .tobject
+
+private def isAnyProducingType (type : Lean.Expr) : Bool :=
   match type with
-  | LCNF.ImpureType.float => .float
-  | LCNF.ImpureType.float32 => .float32
-  | LCNF.ImpureType.uint8 => .uint8
-  | LCNF.ImpureType.uint16 => .uint16
-  | LCNF.ImpureType.uint32 => .uint32
-  | LCNF.ImpureType.uint64 => .uint64
-  | LCNF.ImpureType.usize => .usize
-  | LCNF.ImpureType.erased => .erased
-  | LCNF.ImpureType.object => .object
-  | LCNF.ImpureType.tobject => .tobject
-  | LCNF.ImpureType.tagged => .tagged
-  | LCNF.ImpureType.void => .void
+  | .const ``lcAny _ => true
+  | .forallE _ _ b _ => isAnyProducingType b
+  | _ => false
+
+partial def toIRType (type : Lean.Expr) : CoreM IRType := do
+  match type with
+  | .const name _ => visitApp name #[]
+  | .app .. =>
+    -- All mono types are in headBeta form.
+    let .const name _ := type.getAppFn | unreachable!
+    visitApp name type.getAppArgs
+  | .forallE _ _ b _ =>
+    -- Type formers are erased, but can be used polymorphically as
+    -- an arrow type producing `lcAny`. The runtime representation of
+    -- erased values is a tagged scalar, so this means that any such
+    -- polymorphic type must be represented as `.tobject`.
+    if isAnyProducingType b then
+      return .tobject
+    else
+      return .object
+  | .mdata _ b => toIRType b
   | _ => unreachable!
+where
+  visitApp (declName : Name) (args : Array Lean.Expr) : CoreM IRType := do
+    if let some info ← hasTrivialStructure? declName then
+      let ctorType ← LCNF.getOtherDeclBaseType info.ctorName []
+      let monoType ← LCNF.toMonoType (LCNF.getParamTypes (← LCNF.instantiateForall ctorType args[*...info.numParams]))[info.fieldIdx]!
+      toIRType monoType
+    else
+      nameToIRType declName
+
+inductive CtorFieldInfo where
+  | erased
+  | object (i : Nat) (type : IRType)
+  | usize  (i : Nat)
+  | scalar (sz : Nat) (offset : Nat) (type : IRType)
+  | void
+  deriving Inhabited
+
+namespace CtorFieldInfo
+
+def format : CtorFieldInfo → Format
+  | erased => "◾"
+  | void => "void"
+  | object i type => f!"obj@{i}:{type}"
+  | usize i    => f!"usize@{i}"
+  | scalar sz offset type => f!"scalar#{sz}@{offset}:{type}"
+
+instance : ToFormat CtorFieldInfo := ⟨format⟩
+
+end CtorFieldInfo
+
+structure CtorLayout where
+  ctorInfo : CtorInfo
+  fieldInfo : Array CtorFieldInfo
+  deriving Inhabited
+
+builtin_initialize ctorLayoutExt : LCNF.CacheExtension Name CtorLayout ←
+  LCNF.CacheExtension.register
+
+def getCtorLayout (ctorName : Name) : CoreM CtorLayout := do
+  match (← ctorLayoutExt.find? ctorName) with
+  | some info => return info
+  | none =>
+    let info ← fillCache
+    ctorLayoutExt.insert ctorName info
+    return info
+where fillCache := do
+  let .some (.ctorInfo ctorInfo) := (← getEnv).find? ctorName | unreachable!
+  Meta.MetaM.run' <| Meta.forallTelescopeReducing ctorInfo.type fun params _ => do
+    let mut fields : Array CtorFieldInfo := .emptyWithCapacity ctorInfo.numFields
+    let mut nextIdx := 0
+    let mut has1BScalar := false
+    let mut has2BScalar := false
+    let mut has4BScalar := false
+    let mut has8BScalar := false
+    for field in params[ctorInfo.numParams...(ctorInfo.numParams + ctorInfo.numFields)] do
+      let fieldType ← field.fvarId!.getType
+      let lcnfFieldType ← LCNF.toLCNFType fieldType
+      let monoFieldType ← LCNF.toMonoType lcnfFieldType
+      let irFieldType ← toIRType monoFieldType
+      let ctorField ← match irFieldType with
+      | .object | .tagged | .tobject => do
+        let i := nextIdx
+        nextIdx := nextIdx + 1
+        pure <| .object i irFieldType
+      | .usize => pure <| .usize 0
+      | .erased => .pure <| .erased
+      | .void => .pure <| .void
+      | .uint8 =>
+        has1BScalar := true
+        .pure <| .scalar 1 0 .uint8
+      | .uint16 =>
+        has2BScalar := true
+        .pure <| .scalar 2 0 .uint16
+      | .uint32 =>
+        has4BScalar := true
+        .pure <| .scalar 4 0 .uint32
+      | .uint64 =>
+        has8BScalar := true
+        .pure <| .scalar 8 0 .uint64
+      | .float32 =>
+        has4BScalar := true
+        .pure <| .scalar 4 0 .float32
+      | .float =>
+        has8BScalar := true
+        .pure <| .scalar 8 0 .float
+      | .struct .. | .union .. => unreachable!
+      fields := fields.push ctorField
+    let numObjs := nextIdx
+    ⟨fields, nextIdx⟩ := Id.run <| StateT.run (s := nextIdx) <| fields.mapM fun field => do
+      match field with
+      | .usize _ => do
+        let i ← modifyGet fun nextIdx => (nextIdx, nextIdx + 1)
+        return .usize i
+      | .object .. | .scalar .. | .erased | .void => return field
+    let numUSize := nextIdx - numObjs
+    let adjustScalarsForSize (fields : Array CtorFieldInfo) (size : Nat) (nextOffset : Nat)
+        : Array CtorFieldInfo × Nat :=
+      Id.run <| StateT.run (s := nextOffset) <| fields.mapM fun field => do
+        match field with
+        | .scalar sz _ type => do
+          if sz == size then
+            let offset ← modifyGet fun nextOffset => (nextOffset, nextOffset + sz)
+            return .scalar sz offset type
+          else
+            return field
+        | .object .. | .usize _ | .erased | .void => return field
+    let mut nextOffset := 0
+    if has8BScalar then
+      ⟨fields, nextOffset⟩ := adjustScalarsForSize fields 8 nextOffset
+    if has4BScalar then
+      ⟨fields, nextOffset⟩ := adjustScalarsForSize fields 4 nextOffset
+    if has2BScalar then
+      ⟨fields, nextOffset⟩ := adjustScalarsForSize fields 2 nextOffset
+    if has1BScalar then
+      ⟨fields, nextOffset⟩ := adjustScalarsForSize fields 1 nextOffset
+    return {
+      ctorInfo := {
+        name := ctorName
+        cidx := ctorInfo.cidx
+        size := numObjs
+        usize := numUSize
+        ssize := nextOffset
+      }
+      fieldInfo := fields
+    }
 
 end IR
 end Lean

src/Lean/Compiler/LCNF/Basic.lean

@@ -60,140 +60,6 @@ def Purity.withAssertPurity [Inhabited α] (is : Purity) (should : Purity)
 
 scoped macro "purity_tac" : tactic => `(tactic| first | with_reducible rfl | assumption)
 
-namespace ImpureType
-
-/-!
-This section defines the low level IR types used in the impure phase of LCNF.
--/
-
-/--
-`float` is a 64-bit floating point number.
--/
-@[inline, expose, match_pattern]
-def float : Expr := .const ``Float []
-
-
-/--
-`float32` is a 32-bit floating point number.
--/
-@[inline, expose, match_pattern]
-def float32 : Expr := .const ``Float32 []
-
-/--
-`uint8` is an 8-bit unsigned integer.
--/
-@[inline, expose, match_pattern]
-def uint8 : Expr := .const ``UInt8 []
-
-/--
-`uint16` is a 16-bit unsigned integer.
--/
-@[inline, expose, match_pattern]
-def uint16 : Expr := .const ``UInt16 []
-
-/--
-`uint32` is a 32-bit unsigned integer.
--/
-@[inline, expose, match_pattern]
-def uint32 : Expr := .const ``UInt32 []
-
-/--
-`uint64` is a 64-bit unsigned integer.
--/
-@[inline, expose, match_pattern]
-def uint64 : Expr := .const ``UInt64 []
-
-/--
-`usize` represents the C `size_t` type. It has a separate representation because depending on the
-target architecture it has a different width and we try to generate platform independent C code.
-
-We generally assume that `sizeof(size_t) == sizeof(void)`.
--/
-@[inline, expose, match_pattern]
-def usize : Expr := .const ``USize []
-
-/--
-`erased` represents type arguments, propositions and proofs which are no longer relevant at this
-point in time.
--/
-@[inline, expose, match_pattern]
-def erased : Expr := .const ``lcErased []
-
-/-
-`object` is a pointer to a value in the heap.
--/
-@[inline, expose, match_pattern]
-def object : Expr := .const `obj []
-
-/--
-`tobject` is either an `object` or a `tagged` pointer.
-
-Crucially the RC the RC operations for `tobject` are slightly more expensive because we
-first need to test whether the `tobject` is really a pointer or not.
--/
-@[inline, expose, match_pattern]
-def tobject : Expr := .const `tobj []
-
-/--
-tagged` is a tagged pointer (i.e., the least significant bit is 1) storing a scalar value.
--/
-@[inline, expose, match_pattern]
-def tagged : Expr := .const `tagged []
-
-/--
-`void` is used to identify uses of the state token from `BaseIO` which do no longer need
-to be passed around etc. at this point in the pipeline.
--/
-@[inline, expose, match_pattern]
-def void : Expr := .const ``lcVoid []
-
-/--
-Whether the type is a scalar as opposed to a pointer (or a value disguised as a pointer).
--/
-def Lean.Expr.isScalar : Expr → Bool
-  | ImpureType.float    => true
-  | ImpureType.float32  => true
-  | ImpureType.uint8    => true
-  | ImpureType.uint16   => true
-  | ImpureType.uint32   => true
-  | ImpureType.uint64   => true
-  | ImpureType.usize    => true
-  | _        => false
-
-/--
-Whether the type is an object which is to say a pointer or a value disguised as a pointer.
--/
-def Lean.Expr.isObj : Expr → Bool
-  | ImpureType.object  => true
-  | ImpureType.tagged  => true
-  | ImpureType.tobject => true
-  | ImpureType.void    => true
-  | _       => false
-
-/--
-Whether the type might be an actual pointer (crucially this excludes `tagged`).
--/
-def Lean.Expr.isPossibleRef : Expr → Bool
-  | ImpureType.object | ImpureType.tobject => true
-  | _ => false
-
-/--
-Whether the type is a pointer for sure.
--/
-def Lean.Expr.isDefiniteRef : Expr → Bool
-  | ImpureType.object => true
-  | _ => false
-
-/--
-The boxed version of types.
--/
-def Lean.Expr.boxed : Expr → Expr
-  | ImpureType.object | ImpureType.float | ImpureType.float32 => ImpureType.object
-  | ImpureType.void | ImpureType.tagged | ImpureType.uint8 | ImpureType.uint16 => ImpureType.tagged
-  | _ => ImpureType.tobject
-
-end ImpureType
-
 structure Param (pu : Purity) where
   fvarId     : FVarId
   binderName : Name
@@ -225,15 +91,6 @@ def LitValue.toExpr : LitValue → Expr
   | .uint64 v => .app (.const ``UInt64.ofNat []) (.lit (.natVal (UInt64.toNat v)))
   | .usize v => .app (.const ``USize.ofNat []) (.lit (.natVal (UInt64.toNat v)))
 
-def LitValue.impureTypeScalarNumLit (e : Expr) (n : Nat) : LitValue :=
-  match e with
-  | ImpureType.uint8 => .uint8 n.toUInt8
-  | ImpureType.uint16 => .uint16 n.toUInt16
-  | ImpureType.uint32 => .uint32 n.toUInt32
-  | ImpureType.uint64 => .uint64 n.toUInt64
-  | ImpureType.usize => .usize n.toUInt64
-  | _ => panic! s!"Provided invalid type to impureTypeScalarNumLit: {e}"
-
 inductive Arg (pu : Purity) where
   | erased
   | fvar (fvarId : FVarId)
@@ -263,79 +120,12 @@ private unsafe def Arg.updateFVarImp (arg : Arg pu) (fvarId' : FVarId) : Arg pu
 
 @[implemented_by Arg.updateFVarImp] opaque Arg.updateFVar! (arg : Arg pu) (fvarId' : FVarId) : Arg pu
 
-/-- Constructor information.
-
-   - `name` is the Name of the Constructor in Lean.
-   - `cidx` is the Constructor index (aka tag).
-   - `size` is the number of arguments of type `object/tobject`.
-   - `usize` is the number of arguments of type `usize`.
-   - `ssize` is the number of bytes used to store scalar values.
-
-Recall that a Constructor object contains a header, then a sequence of
-pointers to other Lean objects, a sequence of `USize` (i.e., `size_t`)
-scalar values, and a sequence of other scalar values. -/
-structure CtorInfo where
-  name : Name
-  cidx : Nat
-  size : Nat
-  usize : Nat
-  ssize : Nat
-  deriving Inhabited, BEq, Repr, Hashable
-
-def CtorInfo.isRef (info : CtorInfo) : Bool :=
-  info.size > 0 || info.usize > 0 || info.ssize > 0
-
-def CtorInfo.isScalar (info : CtorInfo) : Bool :=
-  !info.isRef
-
-def CtorInfo.type (info : CtorInfo) : Expr :=
-  if info.isRef then ImpureType.object else ImpureType.tagged
-
 inductive LetValue (pu : Purity) where
-  /--
-  A literal value.
-  -/
   | lit (value : LitValue)
-  /--
-  An erased value that is irrelevant for computation.
-  -/
   | erased
-  /--
-  A projection from a pure LCNF value.
-  -/
   | proj (typeName : Name) (idx : Nat) (struct : FVarId) (h : pu = .pure := by purity_tac)
-  /--
-  A pure application of a constant.
-  -/
   | const (declName : Name) (us : List Level) (args : Array (Arg pu)) (h : pu = .pure := by purity_tac)
-  /--
-  An application of a free variable
-  -/
   | fvar (fvarId : FVarId) (args : Array (Arg pu))
-  /--
-  Allocating a constructor.
-  -/
-  | ctor (i : CtorInfo) (args : Array (Arg pu)) (h : pu = .impure := by purity_tac)
-  /--
-  Projecting objects out of a value.
-  -/
-  | oproj (i : Nat) (var : FVarId) (h : pu = .impure := by purity_tac)
-  /--
-  Projecting USize scalars out of a value.
-  -/
-  | uproj (i : Nat) (var : FVarId) (h : pu = .impure := by purity_tac)
-  /--
-  Projecting non-USize scalars out of a value
-  -/
-  | sproj (n : Nat) (offset : Nat) (var : FVarId) (h : pu = .impure := by purity_tac)
-  /--
-  Full, impure, application of a function.
-  -/
-  | fap (fn : Name) (args : Array (Arg pu)) (h : pu = .impure := by purity_tac)
-  /--
-  Partial application of a function.
-  -/
-  | pap (fn : Name) (args : Array (Arg pu)) (h : pu = .impure := by purity_tac)
   deriving Inhabited, BEq, Hashable
 
 def Arg.toLetValue (arg : Arg pu) : LetValue pu :=
@@ -346,9 +136,6 @@ def Arg.toLetValue (arg : Arg pu) : LetValue pu :=
 private unsafe def LetValue.updateProjImp (e : LetValue pu) (fvarId' : FVarId) : LetValue pu :=
   match e with
   | .proj s i fvarId _ => if fvarId == fvarId' then e else .proj s i fvarId'
-  | .sproj i offset fvarId _ => if fvarId == fvarId' then e else .sproj i offset fvarId'
-  | .uproj i fvarId _ => if fvarId == fvarId' then e else .uproj i fvarId'
-  | .oproj i fvarId _ => if fvarId == fvarId' then e else .oproj i fvarId'
   | _ => unreachable!
 
 @[implemented_by LetValue.updateProjImp] opaque LetValue.updateProj! (e : LetValue pu) (fvarId' : FVarId) : LetValue pu
@@ -371,9 +158,6 @@ private unsafe def LetValue.updateArgsImp (e : LetValue pu) (args' : Array (Arg
   match e with
   | .const declName us args h => if ptrEq args args' then e else .const declName us args'
   | .fvar fvarId args => if ptrEq args args' then e else .fvar fvarId args'
-  | .pap declName args _  => if ptrEq args args' then e else .pap declName args'
-  | .fap declName args _  => if ptrEq args args' then e else .fap declName args'
-  | .ctor info args _  => if ptrEq args args' then e else .ctor info args'
   | _ => unreachable!
 
 @[implemented_by LetValue.updateArgsImp] opaque LetValue.updateArgs! (e : LetValue pu) (args' : Array (Arg pu)) : LetValue pu
@@ -385,11 +169,6 @@ def LetValue.toExpr (e : LetValue pu) : Expr :=
   | .proj n i s _ => .proj n i (.fvar s)
   | .const n us as _ => mkAppN (.const n us) (as.map Arg.toExpr)
   | .fvar fvarId as => mkAppN (.fvar fvarId) (as.map Arg.toExpr)
-  | .ctor i as _ => mkAppN (.const i.name []) (as.map Arg.toExpr)
-  | .fap fn as _ | .pap fn as _ => mkAppN (.const fn []) (as.map Arg.toExpr)
-  | .oproj i var _ => mkApp2 (.const `oproj []) (ToExpr.toExpr i) (.fvar var)
-  | .uproj i var _ => mkApp2 (.const `uproj []) (ToExpr.toExpr i) (.fvar var)
-  | .sproj i offset var _ => mkApp3 (.const `sproj []) (ToExpr.toExpr i) (ToExpr.toExpr offset) (.fvar var)
 
 structure LetDecl (pu : Purity) where
   fvarId : FVarId
@@ -402,7 +181,6 @@ mutual
 
 inductive Alt (pu : Purity) where
   | alt (ctorName : Name) (params : Array (Param pu)) (code : Code pu) (h : pu = .pure := by purity_tac)
-  | ctorAlt (info : CtorInfo) (code : Code pu) (h : pu = .impure := by purity_tac)
   | default (code : Code pu)
 
 inductive FunDecl (pu : Purity) where
@@ -420,8 +198,6 @@ inductive Code (pu : Purity) where
   | cases (cases : Cases pu)
   | return (fvarId : FVarId)
   | unreach (type : Expr)
-  | uset (var : FVarId) (i : Nat) (y : FVarId) (k : Code pu) (h : pu = .impure := by purity_tac)
-  | sset (var : FVarId) (i : Nat) (offset : Nat) (y : FVarId) (ty : Expr) (k : Code pu) (h : pu = .impure := by purity_tac)
   deriving Inhabited
 
 end
@@ -491,19 +267,15 @@ def Cases.getCtorNames (c : Cases pu) : NameSet :=
     match alt with
     | .default _ => ctorNames
     | .alt ctorName .. => ctorNames.insert ctorName
-    | .ctorAlt info .. => ctorNames.insert info.name
 
 inductive CodeDecl (pu : Purity) where
   | let (decl : LetDecl pu)
   | fun (decl : FunDecl pu) (h : pu = .pure := by purity_tac)
   | jp (decl : FunDecl pu)
-  | uset (var : FVarId) (i : Nat) (y : FVarId) (h : pu = .impure := by purity_tac)
-  | sset (var : FVarId) (i : Nat) (offset : Nat) (y : FVarId)  (ty : Expr) (h : pu = .impure := by purity_tac)
   deriving Inhabited
 
 def CodeDecl.fvarId : CodeDecl pu → FVarId
   | .let decl | .fun decl _ | .jp decl => decl.fvarId
-  | .uset var .. | .sset var .. => var
 
 def attachCodeDecls (decls : Array (CodeDecl pu)) (code : Code pu) : Code pu :=
   go decls.size code
@@ -514,8 +286,6 @@ where
       | .let decl => go (i-1) (.let decl code)
       | .fun decl _ => go (i-1) (.fun decl code)
       | .jp decl => go (i-1) (.jp decl code)
-      | .uset var idx y _ => go (i-1) (.uset var idx y code)
-      | .sset var idx offset y ty _ => go (i-1) (.sset var idx offset y ty code)
     else
       code
 
@@ -565,9 +335,8 @@ instance : BEq (FunDecl pu) where
 def Alt.getCode : Alt pu → Code pu
   | .default k => k
   | .alt _ _ k _ => k
-  | .ctorAlt _ k _ => k
 
-def Alt.getParams : Alt .pure → Array (Param .pure)
+def Alt.getParams : Alt pu → Array (Param pu)
   | .default _ => #[]
   | .alt _ ps _ _ => ps
 
@@ -575,13 +344,11 @@ def Alt.forCodeM [Monad m] (alt : Alt pu) (f : Code pu → m Unit) : m Unit := d
   match alt with
   | .default k => f k
   | .alt _ _ k _ => f k
-  | .ctorAlt _ k _ => f k
 
 private unsafe def updateAltCodeImp (alt : Alt pu) (k' : Code pu) : Alt pu :=
   match alt with
   | .default k => if ptrEq k k' then alt else .default k'
   | .alt ctorName ps k _ => if ptrEq k k' then alt else .alt ctorName ps k'
-  | .ctorAlt info k _ => if ptrEq k k' then alt else .ctorAlt info k'
 
 @[implemented_by updateAltCodeImp] opaque Alt.updateCode (alt : Alt pu) (c : Code pu) : Alt pu
 
@@ -622,8 +389,6 @@ private unsafe def updateAltImp (alt : Alt pu) (ps' : Array (Param pu)) (k' : Co
   | .let decl k => if ptrEq k k' then c else .let decl k'
   | .fun decl k _ => if ptrEq k k' then c else .fun decl k'
   | .jp decl k => if ptrEq k k' then c else .jp decl k'
-  | .sset fvarId i offset y ty k _ => if ptrEq k k' then c else .sset fvarId i offset y ty k'
-  | .uset fvarId offset y k _ => if ptrEq k k' then c else .uset fvarId offset y k'
   | _ => unreachable!
 
 @[implemented_by updateContImp] opaque Code.updateCont! (c : Code pu) (k' : Code pu) : Code pu
@@ -657,32 +422,6 @@ private unsafe def updateAltImp (alt : Alt pu) (ps' : Array (Param pu)) (k' : Co
 
 @[implemented_by updateUnreachImp] opaque Code.updateUnreach! (c : Code pu) (type' : Expr) : Code pu
 
-@[inline] private unsafe def updateSsetImp (c : Code pu) (fvarId' : FVarId) (i' : Nat)
-    (offset' : Nat) (y' : FVarId) (ty' : Expr) (k' : Code pu) : Code pu :=
-  match c with
-  | .sset fvarId i offset y ty k _ =>
-    if ptrEq fvarId fvarId' && i == i' && offset == offset' && ptrEq y y' && ptrEq ty ty' && ptrEq k k' then
-      c
-    else
-      .sset fvarId' i' offset' y' ty' k'
-  | _ => unreachable!
-
-@[implemented_by updateSsetImp] opaque Code.updateSset! (c : Code pu) (fvarId' : FVarId) (i' : Nat)
-    (offset' : Nat) (y' : FVarId) (ty' : Expr) (k' : Code pu) : Code pu
-
-@[inline] private unsafe def updateUsetImp (c : Code pu) (fvarId' : FVarId)
-    (offset' : Nat) (y' : FVarId) (k' : Code pu) : Code pu :=
-  match c with
-  | .sset fvarId i offset y ty k _ =>
-    if ptrEq fvarId fvarId' && offset == offset' && ptrEq y y' && ptrEq k k' then
-      c
-    else
-      .uset fvarId' offset' y' k'
-  | _ => unreachable!
-
-@[implemented_by updateUsetImp] opaque Code.updateUset! (c : Code pu) (fvarId' : FVarId)
-    (offset' : Nat) (y' : FVarId) (k' : Code pu) : Code pu
-
 private unsafe def updateParamCoreImp (p : Param pu) (type : Expr) : Param pu :=
   if ptrEq type p.type then
     p
@@ -751,7 +490,7 @@ partial def Code.size (c : Code pu) : Nat :=
 where
   go (c : Code pu) (n : Nat) : Nat :=
     match c with
-    | .let _ k | .sset _ _ _ _ _ k _ | .uset _ _ _ k _ => go k (n + 1)
+    | .let _ k => go k (n+1)
     | .jp decl k | .fun decl k _ => go k <| go decl.value n
     | .cases c => c.alts.foldl (init := n+1) fun n alt => go alt.getCode (n+1)
     | .jmp .. => n+1
@@ -769,7 +508,7 @@ where
 
   go (c : Code pu) : EStateM Unit Nat Unit := do
     match c with
-    | .let _ k | .sset _ _ _ _ _ k _ | .uset _ _ _ k _ => inc; go k
+    | .let _ k => inc; go k
     | .jp decl k | .fun decl k _ => inc; go decl.value; go k
     | .cases c => inc; c.alts.forM fun alt => go alt.getCode
     | .jmp .. => inc
@@ -781,7 +520,7 @@ where
   go (c : Code pu) : m Unit := do
     f c
     match c with
-    | .let _ k | .sset _ _ _ _ _ k _ | .uset _ _ _ k _ => go k
+    | .let _ k => go k
     | .fun decl k _ | .jp decl k => go decl.value; go k
     | .cases c => c.alts.forM fun alt => go alt.getCode
     | .unreach .. | .return .. | .jmp .. => return ()
@@ -861,13 +600,13 @@ def DeclValue.isCodeAndM [Monad m] (v : DeclValue pu) (f : Code pu → m Bool) :
   | .extern .. => pure false
 
 /--
-The signature of a declaration being processed by the Lean to Lean compiler passes.
+Declaration being processed by the Lean to Lean compiler passes.
 -/
-structure Signature (pu : Purity) where
+structure Decl (pu : Purity) where
   /--
   The name of the declaration from the `Environment` it came from
   -/
-  name : Name
+  name  : Name
   /--
   Universe level parameter names.
   -/
@@ -875,8 +614,7 @@ structure Signature (pu : Purity) where
   /--
   The type of the declaration. Note that this is an erased LCNF type
   instead of the fully dependent one that might have been the original
-  type of the declaration in the `Environment`. Furthermore, once in the
-  impure staged of LCNF this type is only the return type.
+  type of the declaration in the `Environment`.
   -/
   type  : Expr
   /--
@@ -884,6 +622,21 @@ structure Signature (pu : Purity) where
   -/
   params : Array (Param pu)
   /--
+  The body of the declaration, usually changes as it progresses
+  through compiler passes.
+  -/
+  value : DeclValue pu
+  /--
+  We set this flag to true during LCNF conversion. When we receive
+  a block of functions to be compiled, we set this flag to `true`
+  if there is an application to the function in the block containing
+  it. This is an approximation, but it should be good enough because
+  in the frontend, we invoke the compiler with blocks of strongly connected
+  components only.
+  We use this information to control inlining.
+  -/
+  recursive : Bool := false
+  /--
   We set this flag to false during LCNF conversion if the Lean function
   associated with this function was tagged as partial or unsafe. This
   information affects how static analyzers treat function applications
@@ -907,27 +660,6 @@ structure Signature (pu : Purity) where
   exhaust resources or output a looping computation.
   -/
   safe : Bool := true
-  deriving Inhabited, BEq
-
-/--
-Declaration being processed by the Lean to Lean compiler passes.
--/
-structure Decl (pu : Purity) extends Signature pu where
-  /--
-  The body of the declaration, usually changes as it progresses
-  through compiler passes.
-  -/
-  value : DeclValue pu
-  /--
-  We set this flag to true during LCNF conversion. When we receive
-  a block of functions to be compiled, we set this flag to `true`
-  if there is an application to the function in the block containing
-  it. This is an approximation, but it should be good enough because
-  in the frontend, we invoke the compiler with blocks of strongly connected
-  components only.
-  We use this information to control inlining.
-  -/
-  recursive : Bool := false
   /--
   We store the inline attribute at LCNF declarations to make sure we can set them for
   auxiliary declarations created during compilation.
@@ -1022,17 +754,14 @@ def Decl.isTemplateLike (decl : Decl pu) : CoreM Bool := do
     return false
 
 private partial def collectType (e : Expr) : FVarIdHashSet → FVarIdHashSet :=
-  if e.hasFVar then
-    match e with
-    | .forallE _ d b _ => collectType b ∘ collectType d
-    | .lam _ d b _     => collectType b ∘ collectType d
-    | .app f a         => collectType f ∘ collectType a
-    | .fvar fvarId     => fun s => s.insert fvarId
-    | .mdata _ b       => collectType b
-    | .proj .. | .letE .. => unreachable!
-    | _                => id
-  else
-    id
+  match e with
+  | .forallE _ d b _ => collectType b ∘ collectType d
+  | .lam _ d b _     => collectType b ∘ collectType d
+  | .app f a         => collectType f ∘ collectType a
+  | .fvar fvarId     => fun s => s.insert fvarId
+  | .mdata _ b       => collectType b
+  | .proj .. | .letE .. => unreachable!
+  | _                => id
 
 private def collectArg (arg : Arg pu) (s : FVarIdHashSet) : FVarIdHashSet :=
   match arg with
@@ -1046,8 +775,8 @@ private def collectArgs (args : Array (Arg pu)) (s : FVarIdHashSet) : FVarIdHash
 private def collectLetValue (e : LetValue pu) (s : FVarIdHashSet) : FVarIdHashSet :=
   match e with
   | .fvar fvarId args => collectArgs args <| s.insert fvarId
-  | .const _ _ args _ | .pap _ args _ | .fap _ args _ | .ctor _ args _  => collectArgs args s
-  | .proj _ _ fvarId _ | .sproj _ _ fvarId _ | .uproj _ fvarId _ | .oproj _ fvarId _ => s.insert fvarId
+  | .const _ _ args _ => collectArgs args s
+  | .proj _ _ fvarId _ => s.insert fvarId
   | .lit .. | .erased => s
 
 private partial def collectParams (ps : Array (Param pu)) (s : FVarIdHashSet) : FVarIdHashSet :=
@@ -1066,27 +795,16 @@ partial def Code.collectUsed (code : Code pu) (s : FVarIdHashSet := {}) : FVarId
     let s := collectType c.resultType s
     c.alts.foldl (init := s) fun s alt =>
       match alt with
-      | .default k | .ctorAlt _ k _  => k.collectUsed s
+      | .default k => k.collectUsed s
       | .alt _ ps k _ => k.collectUsed <| collectParams ps s
   | .return fvarId => s.insert fvarId
   | .unreach type => collectType type s
   | .jmp fvarId args => collectArgs args <| s.insert fvarId
-  | .sset var _ _ y _ k _ | .uset var _ y k _ =>
-    let s := s.insert var
-    let s := s.insert y
-    k.collectUsed s
 end
 
 @[inline] def collectUsedAtExpr (s : FVarIdHashSet) (e : Expr) : FVarIdHashSet :=
   collectType e s
 
-def CodeDecl.collectUsed (codeDecl : CodeDecl pu) (s : FVarIdHashSet := ∅) : FVarIdHashSet :=
-  match codeDecl with
-  | .let decl => collectLetValue decl.value <| collectType decl.type s
-  | .jp decl | .fun decl _ => decl.collectUsed s
-  | .sset var _ _ y ty _ => s.insert var |>.insert y |> collectType ty
-  | .uset var _ y _ => s.insert var |>.insert y
-
 /--
 Traverse the given block of potentially mutually recursive functions
 and mark a declaration `f` as recursive if there is an application
@@ -1109,13 +827,10 @@ where
     | .cases c => c.alts.forM fun alt => visit alt.getCode
     | .unreach .. | .jmp .. | .return .. => return ()
     | .let decl k =>
-      match decl.value with
-      | .const declName .. | .fap declName .. | .pap declName .. =>
+      if let .const declName _ _ _ := decl.value then
         if decls.any (·.name == declName) then
           modify fun s => s.insert declName
-      | _ => pure ()
       visit k
-    | .uset _ _ _ k _ | .sset _ _ _ _ _ k _ => visit k
 
   go : StateM NameSet Unit :=
     decls.forM (·.value.forCodeM visit)

src/Lean/Compiler/LCNF/Bind.lean

@@ -46,7 +46,6 @@ where
       let alts ← c.alts.mapM fun
         | .alt ctorName params k _ => return .alt ctorName params (← go k)
         | .default k => return .default (← go k)
-        | .ctorAlt info k _ => return .ctorAlt info (← go k)
       if alts.isEmpty then
         throwError "`Code.bind` failed, empty `cases` found"
       let resultType ← mkCasesResultType alts
@@ -68,8 +67,6 @@ where
       eraseCode k
       eraseParam auxParam
       return .unreach typeNew
-    | .sset fvarId i offset y ty k _ => return .sset fvarId i offset y ty (← go k)
-    | .uset fvarId offset y k _ => return .uset fvarId offset y (← go k)
 
 instance : MonadCodeBind CompilerM where
   codeBind := CompilerM.codeBind

src/Lean/Compiler/LCNF/Check.lean

@@ -260,6 +260,6 @@ end Check
 def Decl.check (decl : Decl pu) : CompilerM Unit := do
   match pu with
   | .pure => Check.Pure.run do decl.value.forCodeM (Check.Pure.checkFunDeclCore decl.name decl.params decl.type)
-  | .impure => return () -- TODO: port the IR check once it actually makes sense to
+  | .impure => panic! "Check for impure unimplemented" -- TODO
 
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/CompilerM.lean

@@ -149,7 +149,6 @@ def eraseCodeDecl (decl : CodeDecl pu) : CompilerM Unit := do
   match decl with
   | .let decl => eraseLetDecl decl
   | .jp decl | .fun decl _ => eraseFunDecl decl
-  | .sset .. | .uset .. => return ()
 
 /--
 Erase all free variables occurring in `decls` from the local context.
@@ -275,12 +274,10 @@ See `normExprImp`
 private partial def normLetValueImp (s : FVarSubst pu) (e : LetValue pu) (translator : Bool) : LetValue pu :=
   match e with
   | .erased | .lit .. => e
-  | .proj _ _ fvarId _ | .sproj _ _ fvarId _ | .uproj _ fvarId _ | .oproj _ fvarId _  =>
-    match normFVarImp s fvarId translator with
+  | .proj _ _ fvarId _ => match normFVarImp s fvarId translator with
     | .fvar fvarId' => e.updateProj! fvarId'
     | .erased => .erased
-  | .const _ _ args _ | .ctor _ args _ | .fap _ args _ | .pap _ args _ =>
-    e.updateArgs! (normArgsImp s args translator)
+  | .const _ _ args _ => e.updateArgs! (normArgsImp s args translator)
   | .fvar fvarId args => match normFVarImp s fvarId translator with
     | .fvar fvarId' => e.updateFVar! fvarId' (normArgsImp s args translator)
     | .erased => .erased
@@ -465,16 +462,8 @@ mutual
         let alts ← c.alts.mapMonoM fun alt =>
           match alt with
           | .alt _ params k _ => return alt.updateAlt! (← normParams params) (← normCodeImp k)
-          | .default k | .ctorAlt _ k _ => return alt.updateCode (← normCodeImp k)
+          | .default k => return alt.updateCode (← normCodeImp k)
         return code.updateCases! resultType discr alts
-    | .sset fvarId i offset y ty k _ =>
-      withNormFVarResult (← normFVar fvarId) fun fvarId => do
-      withNormFVarResult (← normFVar y) fun y => do
-        return code.updateSset! fvarId i offset y (← normExpr ty) (← normCodeImp k)
-    | .uset fvarId offset y k _ =>
-      withNormFVarResult (← normFVar fvarId) fun fvarId => do
-      withNormFVarResult (← normFVar y) fun y => do
-        return code.updateUset! fvarId offset y (← normCodeImp k)
 end
 
 @[inline] def normFunDecl [MonadLiftT CompilerM m] [Monad m] [MonadFVarSubst m pu t] (decl : FunDecl pu) : m (FunDecl pu) := do

src/Lean/Compiler/LCNF/DeclHash.lean

@@ -23,7 +23,6 @@ partial def hashAlt (alt : Alt pu) : UInt64 :=
   match alt with
   | .alt ctorName ps k _ => mixHash (mixHash (hash ctorName) (hash ps)) (hashCode k)
   | .default k => hashCode k
-  | .ctorAlt info k _ => mixHash (hash info) (hashCode k)
 
 partial def hashAlts (alts : Array (Alt pu)) : UInt64 :=
   alts.foldl (fun r a => mixHash r (hashAlt a)) 7
@@ -37,10 +36,6 @@ partial def hashCode (code : Code pu) : UInt64 :=
   | .unreach type => hash type
   | .jmp fvarId args => mixHash (hash fvarId) (hash args)
   | .cases c => mixHash (mixHash (hash c.discr) (hash c.resultType)) (hashAlts c.alts)
-  | .sset fvarId i offset y ty k _ =>
-    mixHash (mixHash (hash fvarId) (hash i)) (mixHash (mixHash (hash offset) (hash y)) (mixHash (hash ty) (hashCode k)))
-  | .uset fvarId offset y k _ =>
-    mixHash (mixHash (hash fvarId) (hash offset)) (mixHash (hash y) (hashCode k))
 
 end
 
@@ -48,7 +43,6 @@ instance : Hashable (Code pu) where
   hash c := hashCode c
 
 deriving instance Hashable for DeclValue
-deriving instance Hashable for Signature
 deriving instance Hashable for Decl
 
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/DependsOn.lean

@@ -30,9 +30,9 @@ private def argDepOn (a : Arg pu) : M Bool := do
 private def letValueDepOn (e : LetValue pu) : M Bool :=
   match e with
   | .erased | .lit .. => return false
-  | .proj _ _ fvarId _ | .oproj _ fvarId _ | .uproj _ fvarId _ | .sproj _ _ fvarId _ => fvarDepOn fvarId
+  | .proj _ _ fvarId _ => fvarDepOn fvarId
   | .fvar fvarId args => fvarDepOn fvarId <||> args.anyM argDepOn
-  | .const _ _ args _ | .ctor _ args _ | .fap _ args _ | .pap _ args _ => args.anyM argDepOn
+  | .const _ _ args _ => args.anyM argDepOn
 
 private def LetDecl.depOn (decl : LetDecl pu) : M Bool :=
   typeDepOn decl.type <||> letValueDepOn decl.value
@@ -45,7 +45,6 @@ private partial def depOn (c : Code pu) : M Bool :=
   | .jmp fvarId args => fvarDepOn fvarId <||> args.anyM argDepOn
   | .return fvarId => fvarDepOn fvarId
   | .unreach _ => return false
-  | .sset fv1 _ _ fv2 _ k _ | .uset fv1 _ fv2 k _ => fvarDepOn fv1 <||> fvarDepOn fv2 <||> depOn k
 
 @[inline] def LetDecl.dependsOn (decl : LetDecl pu) (s : FVarIdSet) :  Bool :=
   decl.depOn s
@@ -57,8 +56,6 @@ def CodeDecl.dependsOn (decl : CodeDecl pu) (s : FVarIdSet) : Bool :=
   match decl with
   | .let decl => decl.dependsOn s
   | .jp decl | .fun decl _ => decl.dependsOn s
-  | .uset var _ y _ => s.contains var || s.contains y
-  | .sset var _ _ y ty _ => s.contains var || s.contains y || (typeDepOn ty s)
 
 /--
 Return `true` is `c` depends on a free variable in `s`.

src/Lean/Compiler/LCNF/ElimDeadBranches.lean

@@ -678,7 +678,7 @@ def Decl.elimDeadBranches (decls : Array (Decl .pure)) : CompilerM (Array (Decl
   decls.mapIdxM fun i decl => if decl.safe then elimDead assignments[i]! decl else return decl
 
 def elimDeadBranches : Pass :=
-  { name := `elimDeadBranches, run := Decl.elimDeadBranches, phase := .mono, phaseOut := .mono }
+  { name := `elimDeadBranches, run := Decl.elimDeadBranches, phase := .mono }
 
 builtin_initialize
   registerTraceClass `Compiler.elimDeadBranches (inherited := true)

src/Lean/Compiler/LCNF/FVarUtil.lean

@@ -19,36 +19,30 @@ class TraverseFVar (α : Type) where
 export TraverseFVar (mapFVarM forFVarM)
 
 partial def Expr.mapFVarM [MonadLiftT CompilerM m] [Monad m] (f : FVarId → m FVarId) (e : Expr) : m Expr := do
-  if e.hasFVar then
-    match e with
-    | .app fn arg => return e.updateApp! (← mapFVarM f fn) (← mapFVarM f arg)
-    | .fvar fvarId => return e.updateFVar! (← f fvarId)
-    | .lam _ ty body _ => return e.updateLambdaE! (← mapFVarM f ty) (← mapFVarM f body)
-    | .forallE _ ty body _ => return e.updateForallE! (← mapFVarM f ty) (← mapFVarM f body)
-    | .bvar .. | .sort .. => return e
-    | .mdata .. | .const .. | .lit .. => return e
-    | .letE ..  | .proj .. | .mvar .. => unreachable! -- LCNF types do not have this kind of expr
-  else
-    return e
+  match e with
+  | .app fn arg => return e.updateApp! (← mapFVarM f fn) (← mapFVarM f arg)
+  | .fvar fvarId => return e.updateFVar! (← f fvarId)
+  | .lam _ ty body _ => return e.updateLambdaE! (← mapFVarM f ty) (← mapFVarM f body)
+  | .forallE _ ty body _ => return e.updateForallE! (← mapFVarM f ty) (← mapFVarM f body)
+  | .bvar .. | .sort .. => return e
+  | .mdata .. | .const .. | .lit .. => return e
+  | .letE ..  | .proj .. | .mvar .. => unreachable! -- LCNF types do not have this kind of expr
 
 partial def Expr.forFVarM [Monad m] (f : FVarId → m Unit) (e : Expr) : m Unit := do
-  if e.hasFVar then
-    match e with
-    | .app fn arg =>
-      forFVarM f fn
-      forFVarM f arg
-    | .fvar fvarId => f fvarId
-    | .lam _ ty body .. =>
-      forFVarM f ty
-      forFVarM f body
-    | .forallE _ ty body .. =>
-      forFVarM f ty
-      forFVarM f body
-    | .bvar .. | .sort .. => return
-    | .mdata .. | .const .. | .lit .. => return
-    | .mvar .. | .letE .. | .proj .. => unreachable! -- LCNF types do not have this kind of expr
-  else
-    return ()
+  match e with
+  | .app fn arg =>
+    forFVarM f fn
+    forFVarM f arg
+  | .fvar fvarId => f fvarId
+  | .lam _ ty body .. =>
+    forFVarM f ty
+    forFVarM f body
+  | .forallE _ ty body .. =>
+    forFVarM f ty
+    forFVarM f body
+  | .bvar .. | .sort .. => return
+  | .mdata .. | .const .. | .lit .. => return
+  | .mvar .. | .letE .. | .proj .. => unreachable! -- LCNF types do not have this kind of expr
 
 instance : TraverseFVar Expr where
   mapFVarM := Expr.mapFVarM
@@ -73,18 +67,15 @@ instance : TraverseFVar (Arg pu) where
 def LetValue.mapFVarM [MonadLiftT CompilerM m] [Monad m] (f : FVarId → m FVarId) (e : LetValue pu) : m (LetValue pu) := do
   match e with
   | .lit .. | .erased => return e
-  | .proj _ _ fvarId _ | .oproj _ fvarId _ | .sproj _ _ fvarId _ | .uproj _ fvarId _ =>
-    return e.updateProj! (← f fvarId)
-  | .const _ _ args _ | .pap _ args _ | .fap _ args _ | .ctor _ args _ =>
-    return e.updateArgs! (← args.mapM (TraverseFVar.mapFVarM f))
+  | .proj _ _ fvarId _ => return e.updateProj! (← f fvarId)
+  | .const _ _ args _ => return e.updateArgs! (← args.mapM (TraverseFVar.mapFVarM f))
   | .fvar fvarId args => return e.updateFVar! (← f fvarId) (← args.mapM (TraverseFVar.mapFVarM f))
 
 def LetValue.forFVarM [Monad m] (f : FVarId → m Unit) (e : LetValue pu) : m Unit := do
   match e with
   | .lit .. | .erased => return ()
-  | .proj _ _ fvarId _ | .oproj _ fvarId _ | .sproj _ _ fvarId _ | .uproj _ fvarId _ => f fvarId
-  | .const _ _ args _ | .pap _ args _ | .fap _ args _ | .ctor _ args _ =>
-    args.forM (TraverseFVar.forFVarM f)
+  | .proj _ _ fvarId _ => f fvarId
+  | .const _ _ args _ => args.forM (TraverseFVar.forFVarM f)
   | .fvar fvarId args => f fvarId; args.forM (TraverseFVar.forFVarM f)
 
 instance : TraverseFVar (LetValue pu) where
@@ -133,10 +124,6 @@ partial def Code.mapFVarM [MonadLiftT CompilerM m] [Monad m] (f : FVarId → m F
     return Code.updateReturn! c (← f var)
   | .unreach typ =>
     return Code.updateUnreach! c (← Expr.mapFVarM f typ)
-  | .sset fvarId i offset y ty k _ =>
-    return Code.updateSset! c (← f fvarId) i offset (← f y) (← Expr.mapFVarM f ty) (← mapFVarM f k)
-  | .uset fvarId offset y k _ =>
-    return Code.updateUset! c (← f fvarId) offset (← f y) (← mapFVarM f k)
 
 partial def Code.forFVarM [Monad m] (f : FVarId → m Unit) (c : Code pu) : m Unit := do
   match c with
@@ -163,15 +150,6 @@ partial def Code.forFVarM [Monad m] (f : FVarId → m Unit) (c : Code pu) : m Un
   | .return var => f var
   | .unreach typ =>
     Expr.forFVarM f typ
-  | .sset fvarId _ _ y ty k _ =>
-    f fvarId
-    f y
-    Expr.forFVarM f ty
-    forFVarM f k
-  | .uset fvarId _ y k _ =>
-    f fvarId
-    f y
-    forFVarM f k
 
 instance : TraverseFVar (Code pu) where
   mapFVarM := Code.mapFVarM
@@ -196,15 +174,11 @@ instance : TraverseFVar (CodeDecl pu) where
     | .fun decl _ => return .fun (← mapFVarM f decl)
     | .jp decl => return .jp (← mapFVarM f decl)
     | .let decl => return .let (← mapFVarM f decl)
-    | .uset var i y _ => return .uset (← f var) i (← f y)
-    | .sset var i offset y ty _ => return .sset (← f var) i offset (← f y) (← mapFVarM f ty)
   forFVarM f decl :=
     match decl with
     | .fun decl _ => forFVarM f decl
     | .jp decl => forFVarM f decl
     | .let decl => forFVarM f decl
-    | .uset var i y _ => do f var; f y
-    | .sset var i offset y ty _ => do f var; f y; forFVarM f ty
 
 instance : TraverseFVar (Alt pu) where
   mapFVarM f alt := do
@@ -213,14 +187,12 @@ instance : TraverseFVar (Alt pu) where
       let params ← params.mapM (Param.mapFVarM f)
       return .alt ctor params (← Code.mapFVarM f c)
     | .default c => return .default (← Code.mapFVarM f c)
-    | .ctorAlt i c _ => return .ctorAlt i (← Code.mapFVarM f c)
   forFVarM f alt := do
     match alt with
     | .alt _ params c _ =>
       params.forM (Param.forFVarM f)
       Code.forFVarM f c
     | .default c => Code.forFVarM f c
-    | .ctorAlt i c _ => Code.forFVarM f c
 
 def anyFVarM [Monad m] [TraverseFVar α] (f : FVarId → m Bool) (x : α) : m Bool := do
   return (← TraverseFVar.forFVarM go x |>.run) matches none