final tweaks

.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
 
 

src/Init/Data/Array/Lemmas.lean

@@ -483,11 +483,11 @@ theorem mem_iff_getElem? {a} {xs : Array α} : a ∈ xs ↔ ∃ i : Nat, xs[i]?
   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
+    (∃ x ∈ xs, P x) ↔ ∃ (i : Nat), ∃ hi, 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
+    (∀ x ∈ xs, P x) ↔ ∀ (i : Nat) hi, P (xs[i]) := by
   cases xs; simp [List.forall_mem_iff_forall_getElem]
 
 @[deprecated forall_mem_iff_forall_getElem (since := "2026-01-29")]
@@ -1978,14 +1978,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

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/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/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/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/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/Lemmas.lean

@@ -1042,11 +1042,11 @@ theorem mem_iff_getElem? {a} {xs : Vector α n} : a ∈ xs ↔ ∃ i : Nat, xs[i
   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
+    (∃ x ∈ xs, P x) ↔ ∃ (i : Nat), ∃ hi, 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
+    (∀ x ∈ xs, P x) ↔ ∀ (i : Nat) hi, P (xs[i]) := by
   cases xs; simp [*, Array.forall_mem_iff_forall_getElem]
 
 @[deprecated forall_mem_iff_forall_getElem (since := "2026-01-29")]

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/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/LCNF/Basic.lean

@@ -421,7 +421,7 @@ inductive Code (pu : Purity) where
   | 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)
+  | sset (var : FVarId) (i : Nat) (offset : Nat) (y : FVarId)  (ty : Expr) (k : Code pu) (h : pu = .impure := by purity_tac)
   deriving Inhabited
 
 end
@@ -497,13 +497,10 @@ 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 +511,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
 
@@ -1022,17 +1017,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
@@ -1080,13 +1072,6 @@ 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

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.

src/Lean/Compiler/LCNF/DependsOn.lean

@@ -57,8 +57,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/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
@@ -196,15 +190,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

src/Lean/Compiler/LCNF/Internalize.lean

@@ -140,7 +140,7 @@ partial def internalizeCode (code : Code pu) : InternalizeM pu (Code pu) := do
       let alts ← c.alts.mapM fun
         | .alt ctorName params k _ => return .alt ctorName (← params.mapM internalizeParam) (← internalizeCode k)
         | .default k => return .default (← internalizeCode k)
-        | .ctorAlt i k _ => return .ctorAlt i (← internalizeCode k)
+        | .ctorAlt i k _ => return .default (← internalizeCode k)
       return .cases ⟨c.typeName, resultType, discr, alts⟩
   | .sset fvarId i offset y ty k _ =>
     withNormFVarResult (← normFVar fvarId) fun fvarId => do
@@ -158,17 +158,6 @@ partial def internalizeCodeDecl (decl : CodeDecl pu) : InternalizeM pu (CodeDecl
   | .let decl => return .let (← internalizeLetDecl decl)
   | .fun decl _ => return .fun (← internalizeFunDecl decl)
   | .jp decl => return .jp (← internalizeFunDecl decl)
-  | .uset var i y _ =>
-    -- Something weird should be happening if these become erased...
-    let .fvar var ← normFVar var | unreachable!
-    let .fvar y ← normFVar y | unreachable!
-    return .uset var i y
-  | .sset var i offset y ty _ =>
-    let .fvar var ← normFVar var | unreachable!
-    let .fvar y ← normFVar y | unreachable!
-    let ty ← normExpr ty
-    return .sset var i offset y ty
-
 
 end Internalize
 

src/Lean/Compiler/LCNF/LCtx.lean

@@ -77,7 +77,6 @@ mutual
     | .let decl k => eraseCode k <| lctx.eraseLetDecl decl
     | .jp decl k | .fun decl k _ => eraseCode k <| eraseFunDecl lctx decl
     | .cases c => eraseAlts c.alts lctx
-    | .uset _ _ _ k _ | .sset _ _ _ _ _ k _ => eraseCode k lctx
     | _ => lctx
 end
 

src/Lean/Compiler/LCNF/PassManager.lean

@@ -202,7 +202,7 @@ def run (manager : PassManager) (installer : PassInstaller) : CoreM PassManager
   | .mono =>
     return { manager with monoPasses := (← installer.install manager.monoPasses) }
   | .impure =>
-    return { manager with impurePasses := (← installer.install manager.impurePasses) }
+    return { manager with impurePasses := (← installer.install manager.monoPasses) }
 
 private unsafe def getPassInstallerUnsafe (declName : Name) : CoreM PassInstaller := do
   ofExcept <| (← getEnv).evalConstCheck PassInstaller (← getOptions) ``PassInstaller declName

src/Lean/Compiler/LCNF/Passes.lean

@@ -20,7 +20,6 @@ public import Lean.Compiler.LCNF.ExtractClosed
 public import Lean.Compiler.LCNF.Visibility
 public import Lean.Compiler.LCNF.Simp
 public import Lean.Compiler.LCNF.ToImpure
-public import Lean.Compiler.LCNF.PushProj
 
 public section
 
@@ -142,7 +141,6 @@ def builtinPassManager : PassManager := {
   ]
   impurePasses := #[
     saveImpure, -- End of impure phase
-    pushProj (occurrence := 0),
     inferVisibility (phase := .impure),
   ]
 }

src/Lean/Compiler/LCNF/PushProj.lean

@@ -1,158 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Henrik Böving
--/
-module
-
-prelude
-public import Lean.Compiler.LCNF.CompilerM
-public import Lean.Compiler.LCNF.PassManager
-import Lean.Compiler.LCNF.Internalize
-
-namespace Lean.Compiler.LCNF
-
-/-!
-This pass pushes projections into directly neighboring nested case statements.
-
-Suppose we have an LCNF pure input that looks as follows:
-```
-cases a with
-| alt1 p1 p2 =>
-  cases b with
-  | alt2 p3 p4 =>
-    ...
-  | alt3 p5 p6 =>
-    ...
-| ...
-```
-ToImpure will convert this into:
-```
-cases a with
-| alt1 p1 p2 =>
-  let p1 := proj[0] a;
-  let p2 := proj[1] a;
-  cases b with
-  | alt2 p3 p4 =>
-    let p3 := proj[0] b;
-    let p4 := proj[1] b;
-    ...
-  | alt3 p5 p6 =>
-    let p5 := proj[0] b;
-    let p6 := proj[1] b;
-    ...
-| ...
-```
-Let's assume `p1` is used in both `alt2` and `alt3` and `p2` is used only in `alt3` then this pass
-will convert the code into:
-```
-cases a with
-| alt1 p1 p2 =>
-  cases b with
-  | alt2 p3 p4 =>
-    let p1 := proj[0] a;
-    let p3 := proj[0] b;
-    let p4 := proj[1] b;
-    ...
-  | alt3 p5 p6 =>
-    let p1 := proj[0] a;
-    let p2 := proj[1] a;
-    let p5 := proj[0] b;
-    let p6 := proj[1] b;
-    ...
-| ...
-```
-This helps to avoid loading memory that is not actually required in all branches.
-
-Note that unlike `floatLetIn`, this pass is willing to duplicate projections that are being pushed
-around.
-
-
-TODO: we suspect it might also help with reuse analysis, check this. This pass was ported from IR to
-LCNF.
--/
-
-mutual
-
-partial def Cases.pushProjs (c : Cases .impure) (decls : Array (CodeDecl .impure)) :
-    CompilerM (Code .impure) := do
-  let altsUsed := c.alts.map (·.getCode.collectUsed)
-  let ctxUsed := ({} : FVarIdHashSet) |>.insert c.discr
-  let (bs, alts) ← go decls c.alts altsUsed #[] ctxUsed
-  let alts ← alts.mapM (·.mapCodeM Code.pushProj)
-  let c := c.updateAlts alts
-  return attachCodeDecls bs (.cases c)
-where
-  /-
-  Here:
-  - `decls` are the declarations that are still under consideration for being pushed into `alts`
-  - `alts` are the alternatives of the current case arms,
-  - `altsUsed` contains the used fvars per arm, both these sets and `alts` will be updated as we push
-    things into them
-  - `ctx` is the set of declarations that we decided not to push into any alt already
-  - `ctxUsed` fulfills the same purpose as `altsUsed` for `ctx`
-  -/
-  go (decls : Array (CodeDecl .impure)) (alts : Array (Alt .impure)) (altsUsed : Array FVarIdHashSet)
-      (ctx : Array (CodeDecl .impure)) (ctxUsed : FVarIdHashSet) :
-      CompilerM (Array (CodeDecl .impure) × Array (Alt .impure)) :=
-    if decls.isEmpty then
-      return (ctx.reverse, alts)
-    else
-      let b := decls.back!
-      let bs := decls.pop
-      let done := return (bs.push b ++ ctx.reverse, alts)
-      let skip := go bs alts altsUsed (ctx.push b) (b.collectUsed ctxUsed)
-      let push (fvar : FVarId) : CompilerM (Array (CodeDecl .impure) × Array (Alt .impure)) := do
-        if !ctxUsed.contains fvar then
-          let alts ← alts.mapIdxM fun i alt => alt.mapCodeM fun k => do
-            if altsUsed[i]!.contains fvar then
-              return attachCodeDecls #[b] k
-            else
-              return k
-          let altsUsed := altsUsed.map fun used =>
-            if used.contains fvar then
-              b.collectUsed used
-            else
-              used
-          go bs alts altsUsed ctx ctxUsed
-        else
-          skip
-      match b with
-      | .let decl =>
-        match decl.value with
-        | .uproj .. | .oproj .. | .sproj .. => push decl.fvarId
-        -- TODO | .isShared .. => skip
-        | _ => done
-      | _ => done
-
-partial def Code.pushProj (code : Code .impure) : CompilerM (Code .impure) := do
-  go code #[]
-where
-  go (c : Code .impure) (decls : Array (CodeDecl .impure)) : CompilerM (Code .impure) := do
-    match c with
-    | .let decl k => go k (decls.push (.let decl))
-    | .jp decl k =>
-      let decl ← decl.updateValue (← decl.value.pushProj)
-      go k (decls.push (.jp decl))
-    | .uset var i y k _ =>
-      go k (decls.push (.uset var i y))
-    | .sset var i offset y ty k _ =>
-      go k (decls.push (.sset var i offset y ty))
-    | .cases c => c.pushProjs decls
-    | .jmp .. | .return .. | .unreach .. =>
-      return attachCodeDecls decls c
-
-end
-
-def Decl.pushProj (decl : Decl .impure) : CompilerM (Decl .impure) := do
-  let value ← decl.value.mapCodeM (·.pushProj)
-  let decl := { decl with value }
-  decl.internalize
-
-public def pushProj (occurrence : Nat) : Pass :=
-  Pass.mkPerDeclaration `pushProj .impure Decl.pushProj occurrence
-
-builtin_initialize
-  registerTraceClass `Compiler.pushProj (inherited := true)
-
-end Lean.Compiler.LCNF

src/Lean/Data.lean

@@ -25,6 +25,7 @@ public import Lean.Data.Position
 public import Lean.Data.PrefixTree
 public import Lean.Data.SMap
 public import Lean.Data.Trie
+public import Lean.Data.Xml
 public import Lean.Data.NameTrie
 public import Lean.Data.RBTree
 public import Lean.Data.RBMap

src/Lean/Data/Xml.lean

@@ -0,0 +1,10 @@
+/-
+Copyright (c) 2021 Daniel Fabian. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Daniel Fabian
+-/
+module
+
+prelude
+public import Lean.Data.Xml.Basic
+public import Lean.Data.Xml.Parser

src/Lean/Data/Xml/Basic.lean

@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Dany Fabian
+-/
+module
+
+prelude
+public import Std.Data.TreeMap.Basic
+public import Init.Data.Ord.String
+
+public section
+
+namespace Lean
+namespace Xml
+
+@[expose] def Attributes := Std.TreeMap String String
+instance : ToString Attributes := ⟨λ as => as.foldl (λ s n v => s ++ s!" {n}=\"{v}\"") ""⟩
+
+mutual
+inductive Element
+| Element
+  (name : String)
+  (attributes : Attributes)
+  (content : Array Content)
+
+inductive Content
+| Element (element : Element)
+| Comment (comment : String)
+| Character (content : String)
+deriving Inhabited
+end
+
+mutual
+private partial def eToString : Element → String
+| Element.Element n a c => s!"<{n}{a}>{c.map cToString |>.foldl (· ++ ·) ""}</{n}>"
+
+private partial def cToString : Content → String
+| Content.Element e => eToString e
+| Content.Comment c => s!"<!--{c}-->"
+| Content.Character c => c
+
+end
+instance : ToString Element := ⟨private_decl% eToString⟩
+instance : ToString Content := ⟨private_decl% cToString⟩

src/Lean/Data/Xml/Parser.lean

@@ -0,0 +1,492 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Dany Fabian
+-/
+module
+
+prelude
+public import Std.Internal.Parsec
+public import Lean.Data.Xml.Basic
+import Init.Data.String.Search
+
+public section
+
+open System
+open Lean
+
+namespace Lean
+namespace Xml
+
+open Std.Internal.Parsec
+open Std.Internal.Parsec.String
+
+namespace Parser
+
+abbrev LeanChar := Char
+
+/-- consume a newline character sequence pretending, that we read '\n'. As per spec:
+  https://www.w3.org/TR/xml/#sec-line-ends -/
+def endl : Parser LeanChar := (skipString "\r\n" <|> skipChar '\r' <|> skipChar '\n') *> pure '\n'
+
+def quote (p : Parser α) : Parser α :=
+  skipChar '\'' *> p <* skipChar '\''
+  <|> skipChar '"' *> p <* skipChar '"'
+
+/-- https://www.w3.org/TR/xml/#NT-Char -/
+def Char : Parser LeanChar :=
+  (attempt do
+  let c ← any
+  let cNat := c.toNat
+  if (0x20 ≤ cNat ∧ cNat ≤ 0xD7FF)
+   ∨ (0xE000 ≤ cNat ∧ cNat ≤ 0xFFFD)
+   ∨ (0x10000 ≤ cNat ∧ cNat ≤ 0x10FFFF) then pure c else fail "expected xml char")
+  <|> pchar '\t' <|> endl
+
+/-- https://www.w3.org/TR/xml/#NT-S -/
+def S : Parser String :=
+  many1Chars (pchar ' ' <|> endl <|> pchar '\t')
+
+/-- https://www.w3.org/TR/xml/#NT-Eq -/
+def Eq : Parser Unit :=
+  optional S *> skipChar '=' <* optional S
+
+private def nameStartCharRanges : Array (Nat × Nat) :=
+  #[(0xC0, 0xD6),
+    (0xD8, 0xF6),
+    (0xF8, 0x2FF),
+    (0x370, 0x37D),
+    (0x37F, 0x1FFF),
+    (0x200C, 0x200D),
+    (0x2070, 0x218F),
+    (0x2C00, 0x2FEF),
+    (0x3001, 0xD7FF),
+    (0xF900, 0xFDCF),
+    (0xFDF0, 0xFFFD),
+    (0x10000, 0xEFFFF)]
+
+/-- https://www.w3.org/TR/xml/#NT-NameStartChar -/
+def NameStartChar : Parser LeanChar := attempt do
+  let c ← any
+  if ('A' ≤ c ∧ c ≤ 'Z') ∨ ('a' ≤ c ∧ c ≤ 'z') then pure c
+  else if c = ':' ∨ c = '_' then pure c
+  else
+    let cNum := c.toNat
+    if nameStartCharRanges.any (fun (lo, hi) => lo ≤ cNum ∧ cNum ≤ hi) then pure c
+    else fail "expected a name character"
+
+/-- https://www.w3.org/TR/xml/#NT-NameChar -/
+def NameChar : Parser LeanChar :=
+  NameStartChar <|> digit <|> pchar '-' <|> pchar '.' <|> pchar '\xB7'
+  <|> satisfy (λ c => ('\u0300' ≤ c ∧ c ≤ '\u036F') ∨ ('\u203F' ≤ c ∧ c ≤ '\u2040'))
+
+/-- https://www.w3.org/TR/xml/#NT-Name -/
+def Name : Parser String := do
+  let x ← NameStartChar
+  manyCharsCore NameChar x.toString
+
+/-- https://www.w3.org/TR/xml/#NT-VersionNum -/
+def VersionNum : Parser Unit :=
+  skipString "1." <* (many1 digit)
+
+/-- https://www.w3.org/TR/xml/#NT-VersionInfo -/
+def VersionInfo : Parser Unit := do
+  S *>
+  skipString "version"
+  Eq
+  quote VersionNum
+
+/-- https://www.w3.org/TR/xml/#NT-EncName -/
+def EncName : Parser String := do
+  let x ← asciiLetter
+  manyCharsCore (asciiLetter <|> digit <|> pchar '-' <|> pchar '_' <|> pchar '.') x.toString
+
+/-- https://www.w3.org/TR/xml/#NT-EncodingDecl -/
+def EncodingDecl : Parser String := do
+  S *>
+  skipString "encoding"
+  Eq
+  quote EncName
+
+/-- https://www.w3.org/TR/xml/#NT-SDDecl -/
+def SDDecl : Parser String := do
+  S *> skipString "standalone" *> Eq *> quote (pstring "yes" <|> pstring "no")
+
+/-- https://www.w3.org/TR/xml/#NT-XMLDecl -/
+def XMLdecl : Parser Unit := do
+  skipString "<?xml"
+  VersionInfo
+  optional EncodingDecl *>
+  optional SDDecl *>
+  optional S *>
+  skipString "?>"
+
+/-- https://www.w3.org/TR/xml/#NT-Comment -/
+def Comment : Parser String :=
+  let notDash := Char.toString <$> satisfy (λ c => c ≠ '-')
+  skipString "<!--" *>
+  Array.foldl String.append "" <$> many (attempt <| notDash <|> (do
+    let d ← pchar '-'
+    let c ← notDash
+    pure $ d.toString ++ c))
+  <* skipString "-->"
+
+/-- https://www.w3.org/TR/xml/#NT-PITarget -/
+def PITarget : Parser String :=
+  Name <* (skipChar 'X' <|> skipChar 'x') <* (skipChar 'M' <|> skipChar 'm') <* (skipChar 'L' <|> skipChar 'l')
+
+/-- https://www.w3.org/TR/xml/#NT-PI -/
+def PI : Parser Unit := do
+  skipString "<?"
+  <* PITarget <*
+  optional (S *> manyChars (notFollowedBy (skipString "?>") *> Char))
+  skipString "?>"
+
+/-- https://www.w3.org/TR/xml/#NT-Misc -/
+def Misc : Parser Unit :=
+  Comment *> pure () <|> PI <|> S *> pure ()
+
+/-- https://www.w3.org/TR/xml/#NT-SystemLiteral -/
+def SystemLiteral : Parser String :=
+  pchar '"' *> manyChars (satisfy λ c => c ≠ '"') <* pchar '"'
+  <|> pchar '\'' *> manyChars (satisfy λ c => c ≠ '\'') <* pure '\''
+
+/-- https://www.w3.org/TR/xml/#NT-PubidChar -/
+def PubidChar : Parser LeanChar :=
+  asciiLetter <|> digit <|> endl <|> attempt do
+  let c : _root_.Char := ← any
+  if "-'()+,./:=?;!*#@$_%".contains c then pure c else fail "PublidChar expected"
+
+/-- https://www.w3.org/TR/xml/#NT-PubidLiteral -/
+def PubidLiteral : Parser String :=
+  pchar '"' *> manyChars PubidChar <* pchar '"'
+  <|> pchar '\'' *> manyChars (attempt do
+    let c ← PubidChar
+    if c = '\'' then fail "'\\'' not expected" else pure c) <* pchar '\''
+
+/-- https://www.w3.org/TR/xml/#NT-ExternalID -/
+def ExternalID : Parser Unit :=
+  skipString "SYSTEM" *> S *> SystemLiteral *> pure ()
+  <|> skipString "PUBLIC" *> S *> PubidLiteral *> S *> SystemLiteral *> pure ()
+
+/-- https://www.w3.org/TR/xml/#NT-Mixed -/
+def Mixed : Parser Unit :=
+  (do
+    skipChar '('
+    optional S *>
+    skipString "#PCDATA" *>
+    many (optional S *> skipChar '|' *> optional S *> Name) *>
+    optional S *>
+    skipString ")*")
+  <|> skipChar '(' *> (optional S) *> skipString "#PCDATA" <* (optional S) <* skipChar ')'
+
+mutual
+  /-- https://www.w3.org/TR/xml/#NT-cp -/
+  partial def cp : Parser Unit :=
+    (Name *> pure () <|> choice <|> seq) <* optional (skipChar '?' <|> skipChar '*' <|> skipChar '+')
+
+  /-- https://www.w3.org/TR/xml/#NT-choice -/
+  partial def choice : Parser Unit := do
+    skipChar '('
+    optional S *>
+    cp
+    many1 (optional S *> skipChar '|' *> optional S *> cp) *>
+    optional S *>
+    skipChar ')'
+
+  /-- https://www.w3.org/TR/xml/#NT-seq -/
+  partial def seq : Parser Unit := do
+    skipChar '('
+    optional S *>
+    cp
+    many (optional S *> skipChar ',' *> optional S *> cp) *>
+    optional S *>
+    skipChar ')'
+end
+
+/-- https://www.w3.org/TR/xml/#NT-children -/
+def children : Parser Unit :=
+  (choice <|> seq) <* optional (skipChar '?' <|> skipChar '*' <|> skipChar '+')
+
+/-- https://www.w3.org/TR/xml/#NT-contentspec -/
+def contentspec : Parser Unit := do
+  skipString "EMPTY" <|> skipString "ANY" <|> Mixed <|> children
+
+/-- https://www.w3.org/TR/xml/#NT-elementdecl -/
+def elementDecl : Parser Unit := do
+  skipString "<!ELEMENT"
+  S *>
+  Name *>
+  contentspec *>
+  optional S *>
+  skipChar '>'
+
+/-- https://www.w3.org/TR/xml/#NT-StringType -/
+def StringType : Parser Unit :=
+  skipString "CDATA"
+
+/-- https://www.w3.org/TR/xml/#NT-TokenizedType -/
+def TokenizedType : Parser Unit :=
+  skipString "ID"
+  <|> skipString "IDREF"
+  <|> skipString "IDREFS"
+  <|> skipString "ENTITY"
+  <|> skipString "ENTITIES"
+  <|> skipString "NMTOKEN"
+  <|> skipString "NMTOKENS"
+
+/-- https://www.w3.org/TR/xml/#NT-NotationType -/
+def NotationType : Parser Unit := do
+  skipString "NOTATION"
+  S *>
+  skipChar '(' <*
+  optional S
+  Name *> many (optional S *> skipChar '|' *> optional S *> Name) *>
+  optional S *>
+  skipChar ')'
+
+/-- https://www.w3.org/TR/xml/#NT-Nmtoken -/
+def Nmtoken : Parser String := do
+  many1Chars NameChar
+
+/-- https://www.w3.org/TR/xml/#NT-Enumeration -/
+def Enumeration : Parser Unit := do
+  skipChar '('
+  optional S *>
+  Nmtoken *> many (optional S *> skipChar '|' *> optional S *> Nmtoken) *>
+  optional S *>
+  skipChar ')'
+
+/-- https://www.w3.org/TR/xml/#NT-EnumeratedType -/
+def EnumeratedType : Parser Unit :=
+  NotationType <|> Enumeration
+
+/-- https://www.w3.org/TR/xml/#NT-AttType -/
+def AttType : Parser Unit :=
+  StringType <|> TokenizedType <|> EnumeratedType
+
+def predefinedEntityToChar : String → Option LeanChar
+| "lt" => some '<'
+| "gt" => some '>'
+| "amp" => some '&'
+| "apos" => some '\''
+| "quot" => some '"'
+| _ => none
+
+/-- https://www.w3.org/TR/xml/#NT-EntityRef -/
+def EntityRef : Parser $ Option LeanChar := attempt $
+  skipChar '&' *> predefinedEntityToChar <$> Name <* skipChar ';'
+
+@[inline]
+def hexDigitToNat (c : LeanChar) : Nat :=
+  if '0' ≤ c ∧ c ≤ '9' then c.toNat - '0'.toNat
+  else if 'a' ≤ c ∧ c ≤ 'f' then c.toNat - 'a'.toNat + 10
+  else c.toNat - 'A'.toNat + 10
+
+def digitsToNat (base : Nat) (digits : Array Nat) : Nat :=
+  digits.foldl (λ r d => r * base + d) 0
+
+/-- https://www.w3.org/TR/xml/#NT-CharRef -/
+def CharRef : Parser LeanChar := do
+  skipString "&#"
+  let charCode ←
+    digitsToNat 10 <$> many1 (hexDigitToNat <$> digit)
+    <|> skipChar 'x' *> digitsToNat 16 <$> many1 (hexDigitToNat <$> hexDigit)
+  skipChar ';'
+  return Char.ofNat charCode
+
+/-- https://www.w3.org/TR/xml/#NT-Reference -/
+def Reference : Parser $ Option LeanChar :=
+  EntityRef <|> some <$> CharRef
+
+/-- https://www.w3.org/TR/xml/#NT-AttValue -/
+def AttValue : Parser String := do
+  let chars ←
+  (do
+    skipChar '"'
+    many (some <$> satisfy (λ c => c ≠ '<' ∧ c ≠ '&' ∧ c ≠ '"') <|> Reference) <*
+    skipChar '"')
+  <|> (do
+    skipChar '\''
+    many (some <$> satisfy (λ c => c ≠ '<' ∧ c ≠ '&' ∧ c ≠ '\'') <|> Reference) <*
+    skipChar '\'')
+  return chars.foldl (λ s c => if let some c := c then s.push c else s) ""
+
+/-- https://www.w3.org/TR/xml/#NT-DefaultDecl -/
+def DefaultDecl : Parser Unit :=
+  skipString "#REQUIRED"
+  <|> skipString "#IMPLIED"
+  <|> optional (skipString "#FIXED" <* S) *> AttValue *> pure ()
+
+/-- https://www.w3.org/TR/xml/#NT-AttDef -/
+def AttDef : Parser Unit :=
+  S *> Name *> S *> AttType *> S *> DefaultDecl
+
+/-- https://www.w3.org/TR/xml/#NT-AttlistDecl -/
+def AttlistDecl : Parser Unit :=
+  skipString "<!ATTLIST" *> S *> Name *> many AttDef *> optional S *> skipChar '>'
+
+/-- https://www.w3.org/TR/xml/#NT-PEReference -/
+def PEReference : Parser Unit :=
+  skipChar '%' *> Name *> skipChar ';'
+
+/-- https://www.w3.org/TR/xml/#NT-EntityValue -/
+def EntityValue : Parser String := do
+  let chars ←
+  (do
+    skipChar '"'
+    many (some <$> satisfy (λ c => c ≠ '%' ∧ c ≠ '&' ∧ c ≠ '"') <|> PEReference *> pure none <|> Reference) <*
+    skipChar '"')
+  <|> (do
+    skipChar '\''
+    many (some <$> satisfy (λ c => c ≠ '%' ∧ c ≠ '&' ∧ c ≠ '\'') <|> PEReference *> pure none <|> Reference) <*
+    skipChar '\'')
+  return chars.foldl (λ s c => if let some c := c then s.push c else s) ""
+
+
+/-- https://www.w3.org/TR/xml/#NT-NDataDecl -/
+def NDataDecl : Parser Unit :=
+  S *> skipString "NDATA" <* S <* Name
+
+/-- https://www.w3.org/TR/xml/#NT-EntityDef -/
+def EntityDef : Parser Unit :=
+  EntityValue *> pure () <|> (ExternalID <* optional NDataDecl)
+
+/-- https://www.w3.org/TR/xml/#NT-GEDecl -/
+def GEDecl : Parser Unit :=
+  skipString "<!ENTITY" *> S *> Name *> S *> EntityDef *> optional S *> skipChar '>'
+
+/-- https://www.w3.org/TR/xml/#NT-PEDef -/
+def PEDef : Parser Unit :=
+  EntityValue *> pure () <|> ExternalID
+
+/-- https://www.w3.org/TR/xml/#NT-PEDecl -/
+def PEDecl : Parser Unit :=
+  skipString "<!ENTITY" *> S *> skipChar '%' *> S *> Name *> PEDef *> optional S *> skipChar '>'
+
+/-- https://www.w3.org/TR/xml/#NT-EntityDecl -/
+def EntityDecl : Parser Unit :=
+  GEDecl <|> PEDecl
+
+/-- https://www.w3.org/TR/xml/#NT-PublicID -/
+def PublicID : Parser Unit :=
+  skipString "PUBLIC" <* S <* PubidLiteral
+
+/-- https://www.w3.org/TR/xml/#NT-NotationDecl -/
+def NotationDecl : Parser Unit :=
+  skipString "<!NOTATION" *> S *> Name *> (ExternalID <|> PublicID) *> optional S *> skipChar '>'
+
+/-- https://www.w3.org/TR/xml/#NT-markupdecl -/
+def markupDecl : Parser Unit :=
+  elementDecl <|> AttlistDecl <|> EntityDecl <|> NotationDecl <|> PI <|> (Comment *> pure ())
+
+/-- https://www.w3.org/TR/xml/#NT-DeclSep -/
+def DeclSep : Parser Unit :=
+  PEReference <|> S *> pure ()
+
+/-- https://www.w3.org/TR/xml/#NT-intSubset -/
+def intSubset : Parser Unit :=
+  many (markupDecl <|> DeclSep) *> pure ()
+
+/-- https://www.w3.org/TR/xml/#NT-doctypedecl -/
+def doctypedecl : Parser Unit := do
+  skipString "<!DOCTYPE"
+  S *>
+  Name *>
+  optional (S *> ExternalID) *> pure ()
+  <* optional S
+  optional (skipChar '[' *> intSubset <* skipChar ']' <* optional S) *>
+  skipChar '>'
+
+/-- https://www.w3.org/TR/xml/#NT-prolog -/
+def prolog : Parser Unit :=
+  optional XMLdecl *>
+  many Misc *>
+  optional (doctypedecl <* many Misc) *> pure ()
+
+/-- https://www.w3.org/TR/xml/#NT-Attribute -/
+def Attribute : Parser (String × String) := do
+  let name ← Name
+  Eq
+  let value ← AttValue
+  return (name, value)
+
+protected def elementPrefix : Parser (Array Content → Element) := do
+  skipChar '<'
+  let name ← Name
+  let attributes ← many (attempt <| S *> Attribute)
+  optional S *> pure ()
+  return Element.Element name (Std.TreeMap.ofList attributes.toList compare)
+
+/-- https://www.w3.org/TR/xml/#NT-EmptyElemTag -/
+def EmptyElemTag (elem : Array Content → Element) : Parser Element := do
+  skipString "/>" *> pure (elem #[])
+
+/-- https://www.w3.org/TR/xml/#NT-STag -/
+def STag (elem : Array Content → Element) : Parser (Array Content → Element) := do
+  skipChar '>' *> pure elem
+
+/-- https://www.w3.org/TR/xml/#NT-ETag -/
+def ETag : Parser Unit :=
+  skipString "</" *> Name *> optional S *> skipChar '>'
+
+/-- https://www.w3.org/TR/xml/#NT-CDStart -/
+def CDStart : Parser Unit :=
+  skipString "<![CDATA["
+
+/-- https://www.w3.org/TR/xml/#NT-CDEnd -/
+def CDEnd : Parser Unit :=
+  skipString "]]>"
+
+/-- https://www.w3.org/TR/xml/#NT-CData -/
+def CData : Parser String :=
+  manyChars (notFollowedBy (skipString "]]>") *> any)
+
+/-- https://www.w3.org/TR/xml/#NT-CDSect -/
+def CDSect : Parser String :=
+  CDStart *> CData <* CDEnd
+
+/-- https://www.w3.org/TR/xml/#NT-CharData -/
+def CharData : Parser String :=
+  notFollowedBy (skipString "]]>") *> manyChars (satisfy λ c => c ≠ '<' ∧ c ≠ '&')
+
+mutual
+  /-- https://www.w3.org/TR/xml/#NT-content -/
+  partial def content : Parser (Array Content) := do
+    let x ← optional (Content.Character <$> CharData)
+    let xs ← many do
+      let y ←
+        attempt (some <$> Content.Element <$> element)
+        <|> (do let c ← Reference; pure <| c.map (Content.Character ∘ Char.toString))
+        <|> some <$> Content.Character <$> CDSect
+        <|> PI *> pure none
+        <|> some <$> Content.Comment <$> Comment
+
+      let z ← optional (Content.Character <$> CharData)
+      pure #[y, z]
+    let xs := #[x] ++ xs.flatMap id |>.filterMap id
+    let mut res := #[]
+    for x in xs do
+      if res.size > 0 then
+        match res.back!, x with
+        | Content.Character x, Content.Character y => res := res.set! (res.size - 1) (Content.Character $ x ++ y)
+        | _, x => res := res.push x
+      else res := res.push x
+    return res
+
+  /-- https://www.w3.org/TR/xml/#NT-element -/
+  partial def element : Parser Element := do
+    let elem ← Parser.elementPrefix
+    EmptyElemTag elem <|> STag elem <*> content <* ETag
+
+end
+
+/-- https://www.w3.org/TR/xml/#NT-document -/
+def document : Parser Element := prolog *> element <* many Misc <* eof
+
+end Parser
+
+def parse (s : String) : Except String Element :=
+  Parser.run Xml.Parser.document s
+
+end Xml

src/Lean/DocString/Add.lean

@@ -98,51 +98,6 @@ def parseVersoDocString
 
 
 
-open Lean.Parser Command in
-/--
-Reports parse errors from a Verso docstring parse failure.
-
-When Verso docstring parsing fails at parse time, a `parseFailure` node is created containing the
-raw text, because emitting an error at that stage could lead to unwanted parser backtracking. This
-function reports the actual error messages with proper source positions.
--/
-def reportVersoParseFailure
-    [Monad m] [MonadFileMap m] [MonadError m] [MonadEnv m] [MonadOptions m] [MonadLog m]
-    [MonadResolveName m]
-    (parseFailure : Syntax) : m Unit := do
-  let some rawAtom := parseFailure[0]?
-    | return  -- malformed node, nothing to report
-  let some startPos := rawAtom.getPos? (canonicalOnly := true)
-    | return
-  let some endPos := rawAtom.getTailPos? (canonicalOnly := true)
-    | return
-
-  let text ← getFileMap
-  let endPos := if endPos ≤ text.source.rawEndPos then endPos else text.source.rawEndPos
-  have endPos_valid : endPos ≤ text.source.rawEndPos := by
-    unfold endPos; split <;> simp [*]
-
-  let env ← getEnv
-  let ictx : InputContext :=
-    .mk text.source (← getFileName) (fileMap := text)
-      (endPos := endPos) (endPos_valid := endPos_valid)
-  let pmctx : ParserModuleContext := {
-    env,
-    options := ← getOptions,
-    currNamespace := ← getCurrNamespace,
-    openDecls := ← getOpenDecls
-  }
-  let s := mkParserState text.source |>.setPos startPos
-  let s := Doc.Parser.document.run ictx pmctx (getTokenTable env) s
-
-  for (pos, _, err) in s.allErrors do
-    logMessage {
-      fileName := ← getFileName,
-      pos := text.toPosition pos,
-      data := err.toString,
-      severity := .error
-    }
-
 open Lean.Doc in
 open Lean.Parser.Command in
 /--

src/Lean/Elab/BuiltinCommand.lean

@@ -27,13 +27,8 @@ namespace Lean.Elab.Command
     else
       throwError m!"Can't add Markdown-format module docs because there is already Verso-format content present."
   | Syntax.node _ ``Lean.Parser.Command.versoCommentBody args =>
-    let docSyntax := args.getD 0 .missing
-    if docSyntax.getKind == `Lean.Doc.Syntax.parseFailure then
-      -- Report parser errors without attempting elaboration
-      runTermElabM fun _ => reportVersoParseFailure docSyntax
-    else
-      runTermElabM fun _ => do
-        addVersoModDocString range ⟨docSyntax⟩
+    runTermElabM fun _ => do
+      addVersoModDocString range ⟨args.getD 0 .missing⟩
   | _ => throwErrorAt stx "unexpected module doc string{indentD <| stx}"
 
 private def addScope (isNewNamespace : Bool) (header : String) (newNamespace : Name)

src/Lean/Elab/DefView.lean

@@ -162,9 +162,15 @@ def mkDefViewOfTheorem (modifiers : Modifiers) (stx : Syntax) : DefView :=
 
 def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do
   -- leading_parser Term.attrKind >> "instance " >> optNamedPrio >> optional declId >> declSig >> declVal
+  /-
+  **Note**: add `instance_reducible` attribute if declaration is not already marked with `@[reducible]`
+  -/
+  let modifiers       := if modifiers.anyAttr fun attr => attr.name == `reducible then
+    modifiers
+  else
+    modifiers.addAttr { name := `instance_reducible }
   let attrKind        ← liftMacroM <| toAttributeKind stx[0]
   let prio            ← liftMacroM <| expandOptNamedPrio stx[2]
-  -- NOTE: `[instance_reducible]` is added conditionally in `elabMutualDef`
   let attrStx         ← `(attr| instance $(quote prio):num)
   let modifiers       := modifiers.addAttr { kind := attrKind, name := `instance, stx := attrStx }
   let (binders, type) := expandDeclSig stx[4]

src/Lean/Elab/MutualDef.lean

@@ -1221,14 +1221,6 @@ where
     withSaveInfoContext do  -- save adjusted env in info tree
     let headers ← elabHeaders views expandedDeclIds bodyPromises tacPromises
     let headers ← levelMVarToParamHeaders views headers
-
-    -- Now that we have elaborated types, default data instances to `[instance_reducible]`. This
-    -- should happen before attribute application as `[instance]` will check for it.
-    for header in headers do
-      if header.kind == .instance && !header.modifiers.anyAttr (·.name matches `reducible | `irreducible) then
-        if !(← isProp header.type) then
-          setReducibilityStatus header.declName .instanceReducible
-
     if let (#[view], #[declId]) := (views, expandedDeclIds) then
       if Elab.async.get (← getOptions) && view.kind.isTheorem &&
           !deprecated.oldSectionVars.get (← getOptions) &&

src/Lean/Elab/PreDefinition/Basic.lean

@@ -176,9 +176,7 @@ def addPreDefInfo (preDef : PreDefinition) : TermElabM Unit := do
     addTermInfo' preDef.ref (← mkConstWithLevelParams preDef.declName) (isBinder := true)
 
 
-private def addNonRecAux (docCtx : LocalContext × LocalInstances) (preDef : PreDefinition) (compile : Bool)
-    (all : List Name) (applyAttrAfterCompilation := true) (cacheProofs := true) (cleanupValue := false)
-    (isRecursive := false) : TermElabM Unit :=
+private def addNonRecAux (docCtx : LocalContext × LocalInstances) (preDef : PreDefinition) (compile : Bool) (all : List Name) (applyAttrAfterCompilation := true) (cacheProofs := true) (cleanupValue := false) : TermElabM Unit :=
   withRef preDef.ref do
     let preDef ← abstractNestedProofs (cache := cacheProofs) preDef
     let preDef ← letToHaveType preDef
@@ -212,7 +210,6 @@ private def addNonRecAux (docCtx : LocalContext × LocalInstances) (preDef : Pre
       | DefKind.def | DefKind.example => mkDefDecl
       | DefKind.«instance» => if ← Meta.isProp preDef.type then mkThmDecl else mkDefDecl
     addDecl decl
-    if isRecursive then markAsRecursive preDef.declName
     applyAttributesOf #[preDef] AttributeApplicationTime.afterTypeChecking
     match preDef.modifiers.computeKind with
     -- Tags may have been added by `elabMutualDef` already, but that is not the only caller
@@ -232,15 +229,11 @@ private def addNonRecAux (docCtx : LocalContext × LocalInstances) (preDef : Pre
     addPreDefInfo preDef
 
 
-def addAndCompileNonRec (docCtx : LocalContext × LocalInstances) (preDef : PreDefinition)
-    (all : List Name := [preDef.declName]) (cleanupValue := false) (isRecursive := false) : TermElabM Unit := do
-  addNonRecAux docCtx preDef (compile := true) (all := all) (cleanupValue := cleanupValue) (isRecursive := isRecursive)
+def addAndCompileNonRec (docCtx : LocalContext × LocalInstances) (preDef : PreDefinition) (all : List Name := [preDef.declName]) (cleanupValue := false) : TermElabM Unit := do
+  addNonRecAux docCtx preDef (compile := true) (all := all) (cleanupValue := cleanupValue)
 
-def addNonRec (docCtx : LocalContext × LocalInstances) (preDef : PreDefinition)
-    (applyAttrAfterCompilation := true) (all : List Name := [preDef.declName]) (cacheProofs := true)
-    (cleanupValue := false) (isRecursive := false) : TermElabM Unit := do
-  addNonRecAux docCtx preDef (compile := false) (applyAttrAfterCompilation := applyAttrAfterCompilation)
-    (all := all) (cacheProofs := cacheProofs) (cleanupValue := cleanupValue) (isRecursive := isRecursive)
+def addNonRec (docCtx : LocalContext × LocalInstances) (preDef : PreDefinition) (applyAttrAfterCompilation := true) (all : List Name := [preDef.declName]) (cacheProofs := true) (cleanupValue := false) : TermElabM Unit := do
+  addNonRecAux docCtx preDef (compile := false) (applyAttrAfterCompilation := applyAttrAfterCompilation) (all := all) (cacheProofs := cacheProofs) (cleanupValue := cleanupValue)
 
 /--
   Eliminate recursive application annotations containing syntax. These annotations are used by the well-founded recursion module

src/Lean/Elab/PreDefinition/Mutual.lean

@@ -29,19 +29,19 @@ def addPreDefsFromUnary (docCtx : LocalContext × LocalInstances) (preDefs : Arr
   let preDefNonRec := unaryPreDefNonRec.filterAttrs fun attr => attr.name != `implemented_by
   let declNames := preDefs.toList.map (·.declName)
 
+  preDefs.forM fun preDef =>
+    unless preDef.kind.isTheorem do
+      markAsRecursive preDef.declName
+
   -- Do not complain if the user sets @[semireducible], which usually is a noop,
   -- we recognize that below and then do not set @[irreducible]
   withOptions (allowUnsafeReducibility.set · true) do
     if unaryPreDefNonRec.declName = preDefs[0]!.declName then
       addNonRec docCtx preDefNonRec (applyAttrAfterCompilation := false) (cacheProofs := cacheProofs)
-        (isRecursive := true)
     else
       withEnableInfoTree false do
         addNonRec docCtx preDefNonRec (applyAttrAfterCompilation := false) (cacheProofs := cacheProofs)
-          (isRecursive := true)
-      preDefsNonrec.forM fun preDefNonRec =>
-        addNonRec docCtx preDefNonRec (applyAttrAfterCompilation := false) (all := declNames)
-          (cacheProofs := cacheProofs) (isRecursive := true)
+      preDefsNonrec.forM (addNonRec docCtx · (applyAttrAfterCompilation := false) (all := declNames) (cacheProofs := cacheProofs))
 
 /--
 Cleans the right-hand-sides of the predefinitions, to prepare for inclusion in the EqnInfos:

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

@@ -127,6 +127,7 @@ def reportTermMeasure (preDef : PreDefinition) (recArgPos : Nat) : MetaM Unit :=
     let stx ← termMeasure.delab arity (extraParams := preDef.termination.extraParams)
     Tactic.TryThis.addSuggestion ref stx
 
+
 def structuralRecursion
     (docCtx : LocalContext × LocalInstances) (preDefs : Array PreDefinition)
     (termMeasure?s : Array (Option TerminationMeasure)) :
@@ -139,9 +140,11 @@ def structuralRecursion
   preDefsNonRec.forM fun preDefNonRec => do
     let preDefNonRec ← eraseRecAppSyntax preDefNonRec
     prependError m!"structural recursion failed, produced type incorrect term" do
+      unless preDefNonRec.kind.isTheorem do
+        markAsRecursive preDefNonRec.declName
       -- We create the `_unsafe_rec` before we abstract nested proofs.
       -- Reason: the nested proofs may be referring to the _unsafe_rec.
-      addNonRec docCtx preDefNonRec (applyAttrAfterCompilation := false) (all := names.toList) (isRecursive := true)
+      addNonRec docCtx preDefNonRec (applyAttrAfterCompilation := false) (all := names.toList)
   let preDefs ← preDefs.mapM (eraseRecAppSyntax ·)
   addAndCompilePartialRec docCtx preDefs
   for preDef in preDefs, recArgPos in recArgPoss do

src/Lean/Elab/Print.lean

@@ -239,7 +239,7 @@ private def printAxiomsOf (constName : Name) : CommandElabM Unit := do
   if axioms.isEmpty then
     logInfo m!"'{constName}' does not depend on any axioms"
   else
-    logInfo m!"'{constName}' depends on axioms: {axioms.qsort Name.lt |>.map MessageData.ofConstName |>.toList}"
+    logInfo m!"'{constName}' depends on axioms: {axioms.qsort Name.lt |>.toList}"
 
 @[builtin_command_elab «printAxioms»] def elabPrintAxioms : CommandElab
   | `(#print%$tk axioms $id) => withRef tk do

src/Lean/Elab/Tactic.lean

@@ -54,4 +54,3 @@ public import Lean.Elab.Tactic.SimpArith
 public import Lean.Elab.Tactic.Show
 public import Lean.Elab.Tactic.Lets
 public import Lean.Elab.Tactic.Do
-public import Lean.Elab.Tactic.Decide

src/Lean/Elab/Tactic/BVDecide.lean

@@ -57,8 +57,8 @@ There are also some options to influence the behavior of `bv_decide` and friends
 8. Chain all the proofs so far to demonstrate that the original goal holds.
 
 ## Axioms
-`bv_decide` makes use of proof by reflection and adds the result of the compiled check as an axoim,
-thus adding the Lean compiler to the trusted code base.
+`bv_decide` makes use of proof by reflection and `ofReduceBool`, thus adding the Lean compiler to
+the trusted code base.
 
 
 ## Adding a new primitive

src/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean

@@ -36,7 +36,7 @@ def mkContext (lratPath : System.FilePath) (cfg : BVDecideConfig) : TermElabM Ta
   TacticContext.new lratPath cfg
 
 /--
-Prepare an `Expr` that proves `bvExpr.unsat` using native evalution.
+Prepare an `Expr` that proves `bvExpr.unsat` using `ofReduceBool`.
 -/
 def lratChecker (ctx : TacticContext) (reflectionResult : ReflectionResult) : MetaM Expr := do
   let cert ← LratCert.ofFile ctx.lratPath ctx.config.trimProofs

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean

@@ -9,7 +9,6 @@ prelude
 public import Lean.Elab.Tactic.BVDecide.Frontend.BVDecide.SatAtBVLogical
 public import Lean.Elab.Tactic.BVDecide.Frontend.Normalize
 public import Lean.Elab.Tactic.BVDecide.Frontend.LRAT
-import Lean.Meta.Native
 
 public section
 
@@ -284,15 +283,27 @@ def LratCert.toReflectionProof (cert : LratCert) (cfg : TacticContext)
 
   let reflectedExpr := mkConst cfg.exprDef
   let certExpr := mkConst cfg.certDef
-  let reflectionTerm := mkApp2 (mkConst ``verifyBVExpr) reflectedExpr certExpr
 
-  withTraceNode `Meta.Tactic.sat (fun _ => return "Compiling and evaluating reflection proof term") do
-    match (← nativeEqTrue `bv_decide reflectionTerm (axiomDeclRange? := (← getRef))) with
-    | .notTrue =>
-      throwError m!"Tactic `bv_decide` failed: The LRAT certificate could not be verified; \
-        evaluating the following term returned `false`:{indentExpr reflectionTerm}"
-    | .success auxProof =>
-      return mkApp3 (mkConst ``unsat_of_verifyBVExpr_eq_true) reflectedExpr certExpr auxProof
+  withTraceNode `Meta.Tactic.sat (fun _ => return "Compiling reflection proof term") do
+    let auxValue := mkApp2 (mkConst ``verifyBVExpr) reflectedExpr certExpr
+    mkAuxDecl cfg.reflectionDef auxValue (mkConst ``Bool)
+
+  let auxType ← mkEq (mkConst cfg.reflectionDef) (toExpr true)
+  let auxProof :=
+    mkApp3
+      (mkConst ``Lean.ofReduceBool)
+      (mkConst cfg.reflectionDef)
+      (toExpr true)
+      (← mkEqRefl (toExpr true))
+  try
+    let auxLemma ←
+      -- disable async TC so we can catch its exceptions
+      withOptions (Elab.async.set · false) do
+        withTraceNode `Meta.Tactic.sat (fun _ => return "Verifying LRAT certificate") do
+          mkAuxLemma [] auxType auxProof
+    return mkApp3 (mkConst ``unsat_of_verifyBVExpr_eq_true) reflectedExpr certExpr (mkConst auxLemma)
+  catch e =>
+    throwError m!"Failed to check the LRAT certificate in the kernel:\n{e.toMessageData}"
 where
   /--
   Add an auxiliary declaration. Only used to create constants that appear in our reflection proof.

src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean

@@ -63,7 +63,7 @@ where
     else
       return option
 
-/-- An LRAT proof read from a file. This will get parsed using native evaluation. -/
+/-- An LRAT proof read from a file. This will get parsed using ofReduceBool. -/
 abbrev LratCert := String
 
 instance : ToExpr LRAT.IntAction where

src/Lean/Elab/Tactic/Conv.lean

@@ -15,4 +15,3 @@ public import Lean.Elab.Tactic.Conv.Simp
 public import Lean.Elab.Tactic.Conv.Pattern
 public import Lean.Elab.Tactic.Conv.Delta
 public import Lean.Elab.Tactic.Conv.Unfold
-public import Lean.Elab.Tactic.Conv.Cbv

src/Lean/Elab/Tactic/Conv/Cbv.lean

@@ -1,29 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Wojciech Różowski
--/
-
-module
-
-prelude
-public import Lean.Meta.Tactic.Cbv
-public import Lean.Elab.Tactic.Conv.Basic
-
-section
-
-namespace Lean.Elab.Tactic.Conv
-open Lean.Meta.Tactic.Cbv
-
-
-@[builtin_tactic Lean.Parser.Tactic.Conv.cbv] public def evalCbv : Tactic := fun stx => withMainContext do
-  if cbv.warning.get (← getOptions) then
-    logWarningAt stx "The `cbv` tactic is experimental and still under development. Avoid using it in production projects"
-  let lhs ← getLhs
-  let evalResult ← cbvEntry lhs
-  match evalResult with
-  | .rfl .. => return ()
-  | .step e' proof _ =>
-    updateLhs e' proof
-
-end Lean.Elab.Tactic.Conv

src/Lean/Elab/Tactic/Decide.lean

@@ -1,187 +0,0 @@
-/-
-Copyright (c) 2020 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-
-prelude
-public import Lean.Elab.Tactic.Basic
-import Lean.Meta.Native
-import Lean.Elab.Tactic.ElabTerm
-
-public section
-
-namespace Lean.Elab.Tactic
-open Meta
-
-/--
-Make sure `expectedType` does not contain free and metavariables.
-It applies zeta and zetaDelta-reduction to eliminate let-free-vars.
--/
-private def preprocessPropToDecide (expectedType : Expr) : TermElabM Expr := do
-  let mut expectedType ← instantiateMVars expectedType
-  if expectedType.hasFVar then
-    expectedType ← zetaReduce expectedType
-  if expectedType.hasMVar then
-    throwError "Expected type must not contain metavariables{indentExpr expectedType}"
-  if expectedType.hasFVar then
-    throwError m!"Expected type must not contain free variables{indentExpr expectedType}"
-      ++ .hint' m!"Use the `+revert` option to automatically clean up and revert free variables"
-  return expectedType
-
-/--
-Given the decidable instance `inst`, reduces it and returns a decidable instance expression
-in whnf that can be regarded as the reason for the failure of `inst` to fully reduce.
--/
-private partial def blameDecideReductionFailure (inst : Expr) : MetaM Expr := withIncRecDepth do
-  let inst ← whnf inst
-  -- If it's the Decidable recursor, then blame the major premise.
-  if inst.isAppOfArity ``Decidable.rec 5 then
-    return ← blameDecideReductionFailure inst.appArg!
-  -- If it is a matcher, look for a discriminant that's a Decidable instance to blame.
-  if let .const c _ := inst.getAppFn then
-    if let some info ← getMatcherInfo? c then
-      if inst.getAppNumArgs == info.arity then
-        let args := inst.getAppArgs
-        for i in *...info.numDiscrs do
-          let inst' := args[info.numParams + 1 + i]!
-          if (← Meta.isClass? (← inferType inst')) == ``Decidable then
-            let inst'' ← whnf inst'
-            if !(inst''.isAppOf ``isTrue || inst''.isAppOf ``isFalse) then
-              return ← blameDecideReductionFailure inst''
-  return inst
-
-def elabNativeDecideCore (tacticName : Name) (expectedType : Expr) : TacticM Expr := do
-  let d ← mkDecide expectedType
-  match (← nativeEqTrue tacticName d (axiomDeclRange? := (← getRef))) with
-  | .notTrue =>
-    throwError m!"\
-      Tactic `{tacticName}` evaluated that the proposition\
-      {indentExpr expectedType}\n\
-      is false"
-  | .success prf =>
-    -- get instance from `d`
-    let s := d.appArg!
-    return mkApp3 (mkConst ``of_decide_eq_true) expectedType s prf
-
-def evalDecideCore (tacticName : Name) (cfg : Parser.Tactic.DecideConfig) : TacticM Unit := do
-  if cfg.revert then
-    -- In revert mode: clean up the local context and then revert everything that is left.
-    liftMetaTactic1 fun g => do
-      let g ← g.cleanup
-      let (_, g) ← g.revert (clearAuxDeclsInsteadOfRevert := true) (← g.getDecl).lctx.getFVarIds
-      return g
-  closeMainGoalUsing tacticName fun expectedType _ => do
-    if cfg.kernel && cfg.native then
-      throwError "Tactic `{tacticName}` failed: Cannot simultaneously set both `+kernel` and `+native`"
-    let expectedType ← preprocessPropToDecide expectedType
-    if cfg.native then
-      elabNativeDecideCore tacticName expectedType
-    else if cfg.kernel then
-      doKernel expectedType
-    else
-      doElab expectedType
-where
-  doElab (expectedType : Expr) : TacticM Expr := do
-    let pf ← mkDecideProof expectedType
-    -- Get instance from `pf`
-    let s := pf.appFn!.appArg!
-    let r ← withAtLeastTransparency .default <| whnf s
-    if r.isAppOf ``isTrue then
-      -- Success!
-      -- While we have a proof from reduction, we do not embed it in the proof term,
-      -- and instead we let the kernel recompute it during type checking from the following more
-      -- efficient term. The kernel handles the unification `e =?= true` specially.
-      return pf
-    else
-      -- Diagnose the failure, lazily so that there is no performance impact if `decide` isn't being used interactively.
-      throwError MessageData.ofLazyM (es := #[expectedType]) do
-        diagnose expectedType s r
-
-  doKernel (expectedType : Expr) : TacticM Expr := do
-    let pf ← mkDecideProof expectedType
-    -- Get instance from `pf`
-    let s := pf.appFn!.appArg!
-    -- Reduce the decidable instance to (hopefully!) `isTrue` by passing `pf` to the kernel.
-    -- The `mkAuxLemma` function caches the result in two ways:
-    -- 1. First, the function makes use of a `type`-indexed cache per module.
-    -- 2. Second, once the proof is added to the environment, the kernel doesn't need to check the proof again.
-    let levelsInType := (collectLevelParams {} expectedType).params
-    -- Level variables occurring in `expectedType`, in ambient order
-    let lemmaLevels := (← Term.getLevelNames).reverse.filter levelsInType.contains
-    try
-      let lemmaName ← withOptions (Elab.async.set · false) do
-        mkAuxLemma lemmaLevels expectedType pf
-      return mkConst lemmaName (lemmaLevels.map .param)
-    catch ex =>
-      -- Diagnose the failure, lazily so that there is no performance impact if `decide` isn't being used interactively.
-      throwError MessageData.ofLazyM (es := #[expectedType]) do
-        let r ← withAtLeastTransparency .default <| whnf s
-        if r.isAppOf ``isTrue then
-          return m!"\
-            Tactic `{tacticName}` failed. The elaborator is able to reduce the \
-            `{.ofConstName ``Decidable}` instance, but the kernel fails with:\n\
-            {indentD ex.toMessageData}"
-        diagnose expectedType s r
-
-  diagnose (expectedType s : Expr) (r : Expr) : MetaM MessageData := do
-    if r.isAppOf ``isFalse then
-      return m!"\
-        Tactic `{tacticName}` proved that the proposition\
-        {indentExpr expectedType}\n\
-        is false"
-    -- Re-reduce the instance and collect diagnostics, to get all unfolded Decidable instances
-    let (reason, unfoldedInsts) ← withoutModifyingState <| withOptions (fun opt => diagnostics.set opt true) do
-      modifyDiag (fun _ => {})
-      let reason ← withAtLeastTransparency .default <| blameDecideReductionFailure s
-      let unfolded := (← get).diag.unfoldCounter.foldl (init := #[]) fun cs n _ => cs.push n
-      let unfoldedInsts ← unfolded |>.qsort Name.lt |>.filterMapM fun n => do
-        let e ← mkConstWithLevelParams n
-        if (← Meta.isClass? (← inferType e)) == ``Decidable then
-          return m!"`{.ofConst e}`"
-        else
-          return none
-      return (reason, unfoldedInsts)
-    let stuckMsg :=
-      if unfoldedInsts.isEmpty then
-        m!"Reduction got stuck at the `{.ofConstName ``Decidable}` instance{indentExpr reason}"
-      else
-        let instances := if unfoldedInsts.size == 1 then "instance" else "instances"
-        m!"After unfolding the {instances} {.andList unfoldedInsts.toList}, \
-        reduction got stuck at the `{.ofConstName ``Decidable}` instance{indentExpr reason}"
-    let hint :=
-      if reason.isAppOf ``Eq.rec then
-        .hint' m!"Reduction got stuck on `▸` ({.ofConstName ``Eq.rec}), \
-          which suggests that one of the `{.ofConstName ``Decidable}` instances is defined using tactics such as `rw` or `simp`. \
-          To avoid tactics, make use of functions such as \
-          `{.ofConstName ``inferInstanceAs}` or `{.ofConstName ``decidable_of_decidable_of_iff}` \
-          to alter a proposition."
-      else if reason.isAppOf ``Classical.choice then
-        .hint' m!"Reduction got stuck on `{.ofConstName ``Classical.choice}`, \
-          which indicates that a `{.ofConstName ``Decidable}` instance \
-          is defined using classical reasoning, proving an instance exists rather than giving a concrete construction. \
-          The `{tacticName}` tactic works by evaluating a decision procedure via reduction, \
-          and it cannot make progress with such instances. \
-          This can occur due to the `open scoped Classical` command, which enables the instance \
-          `{.ofConstName ``Classical.propDecidable}`."
-      else
-        MessageData.nil
-    return m!"\
-      Tactic `{tacticName}` failed for proposition\
-      {indentExpr expectedType}\n\
-      because its `{.ofConstName ``Decidable}` instance\
-      {indentExpr s}\n\
-      did not reduce to `{.ofConstName ``isTrue}` or `{.ofConstName ``isFalse}`.\n\n\
-      {stuckMsg}{hint}"
-
-declare_config_elab elabDecideConfig Parser.Tactic.DecideConfig
-
-@[builtin_tactic Lean.Parser.Tactic.decide] def evalDecide : Tactic := fun stx => do
-  let cfg ← elabDecideConfig stx[1]
-  evalDecideCore `decide cfg
-
-@[builtin_tactic Lean.Parser.Tactic.nativeDecide] def evalNativeDecide : Tactic := fun stx => do
-  let cfg ← elabDecideConfig stx[1]
-  let cfg := { cfg with native := true }
-  evalDecideCore `native_decide cfg

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -361,4 +361,215 @@ def elabAsFVar (stx : Syntax) (userName? : Option Name := none) : TacticM FVarId
       replaceMainGoal [← (← getMainGoal).rename fvarId h.getId]
   | _ => throwUnsupportedSyntax
 
+
+/--
+Make sure `expectedType` does not contain free and metavariables.
+It applies zeta and zetaDelta-reduction to eliminate let-free-vars.
+-/
+private def preprocessPropToDecide (expectedType : Expr) : TermElabM Expr := do
+  let mut expectedType ← instantiateMVars expectedType
+  if expectedType.hasFVar then
+    expectedType ← zetaReduce expectedType
+  if expectedType.hasMVar then
+    throwError "Expected type must not contain metavariables{indentExpr expectedType}"
+  if expectedType.hasFVar then
+    throwError m!"Expected type must not contain free variables{indentExpr expectedType}"
+      ++ .hint' m!"Use the `+revert` option to automatically clean up and revert free variables"
+  return expectedType
+
+/--
+Given the decidable instance `inst`, reduces it and returns a decidable instance expression
+in whnf that can be regarded as the reason for the failure of `inst` to fully reduce.
+-/
+private partial def blameDecideReductionFailure (inst : Expr) : MetaM Expr := withIncRecDepth do
+  let inst ← whnf inst
+  -- If it's the Decidable recursor, then blame the major premise.
+  if inst.isAppOfArity ``Decidable.rec 5 then
+    return ← blameDecideReductionFailure inst.appArg!
+  -- If it is a matcher, look for a discriminant that's a Decidable instance to blame.
+  if let .const c _ := inst.getAppFn then
+    if let some info ← getMatcherInfo? c then
+      if inst.getAppNumArgs == info.arity then
+        let args := inst.getAppArgs
+        for i in *...info.numDiscrs do
+          let inst' := args[info.numParams + 1 + i]!
+          if (← Meta.isClass? (← inferType inst')) == ``Decidable then
+            let inst'' ← whnf inst'
+            if !(inst''.isAppOf ``isTrue || inst''.isAppOf ``isFalse) then
+              return ← blameDecideReductionFailure inst''
+  return inst
+
+private unsafe def elabNativeDecideCoreUnsafe (tacticName : Name) (expectedType : Expr) : TacticM Expr := do
+  let d ← mkDecide expectedType
+  let levels := (collectLevelParams {} expectedType).params.toList
+  let auxDeclName ← Term.mkAuxName `_nativeDecide
+  let decl := Declaration.defnDecl {
+    name := auxDeclName
+    levelParams := levels
+    type := mkConst ``Bool
+    value := d
+    hints := .abbrev
+    safety := .safe
+  }
+  try
+    -- disable async codegen so we can catch its exceptions; we don't want to report `evalConst`
+    -- failures below when the actual reason was a codegen failure
+    withOptions (Elab.async.set · false) do
+      addAndCompile decl
+  catch ex =>
+    throwError m!"Tactic `{tacticName}` failed. Error: {ex.toMessageData}"
+
+  -- get instance from `d`
+  let s := d.appArg!
+  let rflPrf ← mkEqRefl (toExpr true)
+  let levelParams := levels.map .param
+  let pf := mkApp3 (mkConst ``of_decide_eq_true) expectedType s <|
+    mkApp3 (mkConst ``Lean.ofReduceBool) (mkConst auxDeclName levelParams) (toExpr true) rflPrf
+  try
+    -- disable async TC so we can catch its exceptions
+    withOptions (Elab.async.set · false) do
+      let lemmaName ← mkAuxLemma levels expectedType pf
+      return .const lemmaName levelParams
+  catch ex =>
+    -- Diagnose error
+    throwError MessageData.ofLazyM (es := #[expectedType]) do
+      let r ←
+        try
+          evalConst Bool auxDeclName
+        catch ex =>
+          return m!"\
+            Tactic `{tacticName}` failed: Could not evaluate decidable instance. \
+            Error: {ex.toMessageData}"
+      if !r then
+        return m!"\
+          Tactic `{tacticName}` evaluated that the proposition\
+          {indentExpr expectedType}\n\
+          is false"
+      else
+        return m!"Tactic `{tacticName}` failed. Error: {ex.toMessageData}"
+
+@[implemented_by elabNativeDecideCoreUnsafe]
+private opaque elabNativeDecideCore (tacticName : Name) (expectedType : Expr) : TacticM Expr
+
+def evalDecideCore (tacticName : Name) (cfg : Parser.Tactic.DecideConfig) : TacticM Unit := do
+  if cfg.revert then
+    -- In revert mode: clean up the local context and then revert everything that is left.
+    liftMetaTactic1 fun g => do
+      let g ← g.cleanup
+      let (_, g) ← g.revert (clearAuxDeclsInsteadOfRevert := true) (← g.getDecl).lctx.getFVarIds
+      return g
+  closeMainGoalUsing tacticName fun expectedType _ => do
+    if cfg.kernel && cfg.native then
+      throwError "Tactic `{tacticName}` failed: Cannot simultaneously set both `+kernel` and `+native`"
+    let expectedType ← preprocessPropToDecide expectedType
+    if cfg.native then
+      elabNativeDecideCore tacticName expectedType
+    else if cfg.kernel then
+      doKernel expectedType
+    else
+      doElab expectedType
+where
+  doElab (expectedType : Expr) : TacticM Expr := do
+    let pf ← mkDecideProof expectedType
+    -- Get instance from `pf`
+    let s := pf.appFn!.appArg!
+    let r ← withAtLeastTransparency .default <| whnf s
+    if r.isAppOf ``isTrue then
+      -- Success!
+      -- While we have a proof from reduction, we do not embed it in the proof term,
+      -- and instead we let the kernel recompute it during type checking from the following more
+      -- efficient term. The kernel handles the unification `e =?= true` specially.
+      return pf
+    else
+      -- Diagnose the failure, lazily so that there is no performance impact if `decide` isn't being used interactively.
+      throwError MessageData.ofLazyM (es := #[expectedType]) do
+        diagnose expectedType s r
+
+  doKernel (expectedType : Expr) : TacticM Expr := do
+    let pf ← mkDecideProof expectedType
+    -- Get instance from `pf`
+    let s := pf.appFn!.appArg!
+    -- Reduce the decidable instance to (hopefully!) `isTrue` by passing `pf` to the kernel.
+    -- The `mkAuxLemma` function caches the result in two ways:
+    -- 1. First, the function makes use of a `type`-indexed cache per module.
+    -- 2. Second, once the proof is added to the environment, the kernel doesn't need to check the proof again.
+    let levelsInType := (collectLevelParams {} expectedType).params
+    -- Level variables occurring in `expectedType`, in ambient order
+    let lemmaLevels := (← Term.getLevelNames).reverse.filter levelsInType.contains
+    try
+      let lemmaName ← withOptions (Elab.async.set · false) do
+        mkAuxLemma lemmaLevels expectedType pf
+      return mkConst lemmaName (lemmaLevels.map .param)
+    catch ex =>
+      -- Diagnose the failure, lazily so that there is no performance impact if `decide` isn't being used interactively.
+      throwError MessageData.ofLazyM (es := #[expectedType]) do
+        let r ← withAtLeastTransparency .default <| whnf s
+        if r.isAppOf ``isTrue then
+          return m!"\
+            Tactic `{tacticName}` failed. The elaborator is able to reduce the \
+            `{.ofConstName ``Decidable}` instance, but the kernel fails with:\n\
+            {indentD ex.toMessageData}"
+        diagnose expectedType s r
+
+  diagnose (expectedType s : Expr) (r : Expr) : MetaM MessageData := do
+    if r.isAppOf ``isFalse then
+      return m!"\
+        Tactic `{tacticName}` proved that the proposition\
+        {indentExpr expectedType}\n\
+        is false"
+    -- Re-reduce the instance and collect diagnostics, to get all unfolded Decidable instances
+    let (reason, unfoldedInsts) ← withoutModifyingState <| withOptions (fun opt => diagnostics.set opt true) do
+      modifyDiag (fun _ => {})
+      let reason ← withAtLeastTransparency .default <| blameDecideReductionFailure s
+      let unfolded := (← get).diag.unfoldCounter.foldl (init := #[]) fun cs n _ => cs.push n
+      let unfoldedInsts ← unfolded |>.qsort Name.lt |>.filterMapM fun n => do
+        let e ← mkConstWithLevelParams n
+        if (← Meta.isClass? (← inferType e)) == ``Decidable then
+          return m!"`{.ofConst e}`"
+        else
+          return none
+      return (reason, unfoldedInsts)
+    let stuckMsg :=
+      if unfoldedInsts.isEmpty then
+        m!"Reduction got stuck at the `{.ofConstName ``Decidable}` instance{indentExpr reason}"
+      else
+        let instances := if unfoldedInsts.size == 1 then "instance" else "instances"
+        m!"After unfolding the {instances} {.andList unfoldedInsts.toList}, \
+        reduction got stuck at the `{.ofConstName ``Decidable}` instance{indentExpr reason}"
+    let hint :=
+      if reason.isAppOf ``Eq.rec then
+        .hint' m!"Reduction got stuck on `▸` ({.ofConstName ``Eq.rec}), \
+          which suggests that one of the `{.ofConstName ``Decidable}` instances is defined using tactics such as `rw` or `simp`. \
+          To avoid tactics, make use of functions such as \
+          `{.ofConstName ``inferInstanceAs}` or `{.ofConstName ``decidable_of_decidable_of_iff}` \
+          to alter a proposition."
+      else if reason.isAppOf ``Classical.choice then
+        .hint' m!"Reduction got stuck on `{.ofConstName ``Classical.choice}`, \
+          which indicates that a `{.ofConstName ``Decidable}` instance \
+          is defined using classical reasoning, proving an instance exists rather than giving a concrete construction. \
+          The `{tacticName}` tactic works by evaluating a decision procedure via reduction, \
+          and it cannot make progress with such instances. \
+          This can occur due to the `open scoped Classical` command, which enables the instance \
+          `{.ofConstName ``Classical.propDecidable}`."
+      else
+        MessageData.nil
+    return m!"\
+      Tactic `{tacticName}` failed for proposition\
+      {indentExpr expectedType}\n\
+      because its `{.ofConstName ``Decidable}` instance\
+      {indentExpr s}\n\
+      did not reduce to `{.ofConstName ``isTrue}` or `{.ofConstName ``isFalse}`.\n\n\
+      {stuckMsg}{hint}"
+
+declare_config_elab elabDecideConfig Parser.Tactic.DecideConfig
+
+@[builtin_tactic Lean.Parser.Tactic.decide] def evalDecide : Tactic := fun stx => do
+  let cfg ← elabDecideConfig stx[1]
+  evalDecideCore `decide cfg
+
+@[builtin_tactic Lean.Parser.Tactic.nativeDecide] def evalNativeDecide : Tactic := fun stx => do
+  let cfg ← elabDecideConfig stx[1]
+  let cfg := { cfg with native := true }
+  evalDecideCore `native_decide cfg
+
 end Lean.Elab.Tactic

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

@@ -230,11 +230,7 @@ def mkGrindParams
   let params ← if only then Grind.mkOnlyParams config else Grind.mkDefaultParams config
   let mut params ← elabGrindParams params ps (lax := config.lax) (only := only)
   if config.suggestions then
-    let lsConfig : LibrarySuggestions.Config := { caller := some "grind" }
-    let lsConfig := match config.maxSuggestions with
-      | some n => { lsConfig with maxSuggestions := n }
-      | none => lsConfig
-    params ← elabGrindSuggestions params (← LibrarySuggestions.select mvarId lsConfig)
+    params ← elabGrindSuggestions params (← LibrarySuggestions.select mvarId { caller := some "grind" })
   if config.locals then
     params ← elabGrindLocals params
   trace[grind.debug.inj] "{params.extensions[0]!.inj.getOrigins.map (·.pp)}"

src/Lean/Elab/Tactic/SimpTrace.lean

@@ -59,11 +59,7 @@ def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tacti
       if let some a := args then a.getElems else #[]
     if config.suggestions then
       -- Get premise suggestions from the premise selector
-      let lsConfig : LibrarySuggestions.Config := { caller := some "simp" }
-      let lsConfig := match config.maxSuggestions with
-        | some n => { lsConfig with maxSuggestions := n }
-        | none => lsConfig
-      let suggestions ← Lean.LibrarySuggestions.select (← getMainGoal) lsConfig
+      let suggestions ← Lean.LibrarySuggestions.select (← getMainGoal) { caller := some "simp" }
       -- Convert suggestions to simp argument syntax and add them to the args
       -- If a name is ambiguous, we add ALL interpretations
       for sugg in suggestions do
@@ -102,11 +98,7 @@ def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tacti
       if let some a := args then a.getElems else #[]
     if config.suggestions then
       -- Get premise suggestions from the premise selector
-      let lsConfig : LibrarySuggestions.Config := { caller := some "simp_all" }
-      let lsConfig := match config.maxSuggestions with
-        | some n => { lsConfig with maxSuggestions := n }
-        | none => lsConfig
-      let suggestions ← Lean.LibrarySuggestions.select (← getMainGoal) lsConfig
+      let suggestions ← Lean.LibrarySuggestions.select (← getMainGoal) { caller := some "simp_all" }
       -- Convert suggestions to simp argument syntax and add them to the args
       -- If a name is ambiguous, we add ALL interpretations
       for sugg in suggestions do

src/Lean/Elab/Tactic/Try.lean

@@ -576,11 +576,7 @@ private def evalSuggestSimpAllTrace : TryTactic := fun tac => do
         let config ← elabSimpConfig configStx (kind := .simpAll)
         let mut argsArray : TSyntaxArray [`Lean.Parser.Tactic.simpErase, `Lean.Parser.Tactic.simpLemma] := #[]
         if config.suggestions then
-          let lsConfig : LibrarySuggestions.Config := { caller := some "simp_all" }
-          let lsConfig := match config.maxSuggestions with
-            | some n => { lsConfig with maxSuggestions := n }
-            | none => lsConfig
-          let suggestions ← Lean.LibrarySuggestions.select (← getMainGoal) lsConfig
+          let suggestions ← Lean.LibrarySuggestions.select (← getMainGoal)
           for sugg in suggestions do
             let ident := mkIdent sugg.name
             let candidates ← resolveGlobalConst ident

src/Lean/Environment.lean

@@ -2491,7 +2491,6 @@ where
       let decl ← match info with
         | .thmInfo thm   => pure <| .thmDecl thm
         | .defnInfo defn => pure <| .defnDecl defn
-        | .axiomInfo ax  => pure <| .axiomDecl ax
         | _              =>
           return panic! s!"{c.constInfo.name} must be definition/theorem"
       -- realized kernel additions cannot be interrupted - which would be bad anyway as they can be

src/Lean/Meta/GetUnfoldableConst.lean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Basic
+public import Lean.Meta.GlobalInstances -- **TODO**: Delete after update stage0
 import Lean.ReducibilityAttrs
 public section
 namespace Lean.Meta
@@ -19,7 +19,8 @@ private def canUnfoldDefault (cfg : Config) (info : ConstantInfo) : CoreM Bool :
     let status ← getReducibilityStatus info.name
     if status == .reducible then
       return true
-    else if m == .instances && status == .instanceReducible then
+    -- **TODO**: Delete `isGlobalInstance` after update stage0
+    else if m == .instances && (isGlobalInstance (← getEnv) info.name || status == .instanceReducible) then
       return true
     else
       return false

src/Lean/Meta/GlobalInstances.lean

@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+
+prelude
+public import Lean.Meta.Basic
+
+public section
+
+namespace Lean.Meta
+
+builtin_initialize globalInstanceExtension : SimpleScopedEnvExtension Name (PersistentHashMap Name Unit)  ←
+  registerSimpleScopedEnvExtension {
+    initial  := {}
+    addEntry := fun s n => s.insert n ()
+  }
+
+def addGlobalInstance (declName : Name) (attrKind : AttributeKind) : MetaM Unit := do
+  globalInstanceExtension.add declName attrKind
+
+@[export lean_is_instance]
+def isGlobalInstance (env : Environment) (declName : Name) : Bool :=
+  globalInstanceExtension.getState env |>.contains declName
+
+end Lean.Meta

src/Lean/Meta/Instances.lean

@@ -10,7 +10,6 @@ public import Lean.Meta.DiscrTree.Main
 public import Lean.Meta.CollectMVars
 import Lean.ReducibilityAttrs
 import Lean.Meta.WHNF
-import Lean.AddDecl
 public section
 namespace Lean.Meta
 
@@ -236,9 +235,10 @@ def addInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) : Meta
   unless status matches .reducible | .instanceReducible do
     let info ← getConstInfo declName
     if info.isDefinition then
-      logWarning m!"instance `{declName}` must be marked with `@[reducible]` or `@[instance_reducible]`"
-    else if wasOriginallyDefn (← getEnv) declName then
-      logWarning m!"instance `{declName}` must be marked with `@[expose]`"
+      -- **TODO**: uncomment after update stage0
+      -- logWarning m!"instance `{declName}` must be marked with @[reducible] or @[instance_reducible]"
+      pure ()
+  addGlobalInstance declName attrKind
   let projInfo? ← getProjectionFnInfo? declName
   let synthOrder ← computeSynthOrder c projInfo?
   instanceExtension.add { keys, val := c, priority := prio, globalName? := declName, attrKind, synthOrder } attrKind
@@ -368,4 +368,15 @@ def getDefaultInstancesPriorities [Monad m] [MonadEnv m] : m PrioritySet :=
 def getDefaultInstances [Monad m] [MonadEnv m] (className : Name) : m (List (Name × Nat)) :=
   return defaultInstanceExtension.getState (← getEnv) |>.defaultInstances.find? className |>.getD []
 
-end Lean.Meta
+end Meta
+
+-- **TODO**: Move to `ReducibilityAttrs.lean` after update stage0
+def isInstanceReducibleCore (env : Environment) (declName : Name) : Bool :=
+  getReducibilityStatusCore env declName matches .instanceReducible
+    || Meta.isInstanceCore env declName -- **TODO**: Delete after update stage0
+
+/-- Return `true` if the given declaration has been marked as `[instance_reducible]`. -/
+def isInstanceReducible [Monad m] [MonadEnv m] (declName : Name) : m Bool :=
+  return isInstanceReducibleCore (← getEnv) declName
+
+end Lean

src/Lean/Meta/Native.lean

@@ -1,85 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joachim Breitner
--/
-
-module
-prelude
-public import Lean.Meta.Basic
-import Lean.Util.CollectLevelParams
-import Lean.AddDecl
-import Lean.Meta.AppBuilder
-import Lean.Elab.DeclarationRange
-
-open Lean Meta
-
-namespace Lean.Meta
-
-/-!
-This module contains infrastructure for proofs by native evaluation (`native decide`, `bv_decide`).
-Such proofs involve a native computation using the Lean kernel, and then asserting the result
-of that computation as an axiom towards the logic.
--/
-
-public inductive NativeEqTrueResult where
-  /-- The given expression `e` evalutes to true. `prf` is a proof of `e = true`. -/
-  | success (prf : Expr)
-  /-- The given expression `e` evalutes to false. -/
-  | notTrue
-
-/--
-A call to `nativeEqTrue tacName e`, where `e` is a closed value of type `Bool`, will compile and run
-that value, check that it evaluates to `true`, and if so, will add an axiom asserting `e = true` and
-return that axiom.
-
-It is the basis for `native_decide` and `bv_decide` tactics.
--/
-public def nativeEqTrue (tacticName : Name) (e : Expr) (axiomDeclRange? : Option Syntax := none) : MetaM NativeEqTrueResult  := do
-  let e ← instantiateMVars e
-  if e.hasFVar then
-    throwError m!"Tactic `{tacticName}` failed: Cannot native decide proposition with free variables:{indentExpr e}"
-  if e.hasMVar then
-    throwError m!"Tactic `{tacticName}` failed: Cannot native decide proposition with metavariables:{indentExpr e}"
-  let levels := (collectLevelParams {} e).params.toList
-  let isTrue ← withoutModifyingEnv do
-    let auxDeclName ← mkAuxDeclName <| `_native ++ tacticName ++ `decl
-    let decl := Declaration.defnDecl {
-      name := auxDeclName
-      levelParams := levels
-      type := mkConst ``Bool
-      value := e
-      hints := .abbrev
-      safety := .safe
-    }
-    try
-      -- disable async codegen so we can catch its exceptions; we don't want to report `evalConst`
-      -- failures below when the actual reason was a codegen failure
-      withOptions (Elab.async.set · false) do
-        addAndCompile decl
-    catch ex =>
-      throwError m!"Tactic `{tacticName}` failed. Error: {ex.toMessageData}"
-
-    -- Now evaluate the constant, and check that it is true.
-    try
-      unsafe evalConst Bool auxDeclName
-    catch ex =>
-      throwError m!"\
-        Tactic `{tacticName}` failed: Could not evaluate decidable instance. \
-        Error: {ex.toMessageData}"
-
-  unless isTrue do return .notTrue
-
-  let auxAxiomName ← mkAuxDeclName <| `_native ++ tacticName ++ `ax
-  let axDecl := Declaration.axiomDecl {
-    name := auxAxiomName
-    levelParams := levels
-    type := mkApp3 (mkConst ``Eq [1]) (mkConst ``Bool) e (mkConst ``Bool.true)
-    isUnsafe := false
-  }
-  addDecl axDecl
-  if let some ref := axiomDeclRange? then
-    Elab.addDeclarationRangesFromSyntax auxAxiomName ref
-
-  let levelParams := levels.map mkLevelParam
-  return .success <| mkConst auxAxiomName levelParams