chore: add TODO for offset equalities

This PR hopefully fixes a problem from #8471, which even the most
cursory testing (by me!) should have detected.

.github/workflows/awaiting-mathlib.yml

@@ -10,11 +10,29 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Check awaiting-mathlib label
+        id: check-awaiting-mathlib-label
         if: github.event_name == 'pull_request'
         uses: actions/github-script@v7
         with:
           script: |
-            const { labels } = context.payload.pull_request;
-            if (labels.some(label => label.name == "awaiting-mathlib") && !labels.some(label => label.name == "builds-mathlib")) {
-              core.setFailed('PR is marked "awaiting-mathlib" but "builds-mathlib" label has not been applied yet by the bot');
+            const { labels, number: prNumber } = context.payload.pull_request;
+            const hasAwaiting = labels.some(label => label.name == "awaiting-mathlib");
+            const hasBreaks = labels.some(label => label.name == "breaks-mathlib");
+            const hasBuilds = labels.some(label => label.name == "builds-mathlib");
+
+            if (hasAwaiting && hasBreaks) {
+              core.setFailed('PR has both "awaiting-mathlib" and "breaks-mathlib" labels.');
+            } else if (hasAwaiting && !hasBreaks && !hasBuilds) {
+              core.info('PR is marked "awaiting-mathlib" but neither "breaks-mathlib" nor "builds-mathlib" labels are present.');
+              core.setOutput('awaiting', 'true');
             }
+      
+      - name: Wait for mathlib compatibility
+        if: github.event_name == 'pull_request' && steps.check-awaiting-mathlib-label.outputs.awaiting == 'true'
+        run: |
+          echo "::notice title=Awaiting mathlib::PR is marked 'awaiting-mathlib' but neither 'breaks-mathlib' nor 'builds-mathlib' labels are present."
+          echo "This check will remain in progress until the PR is updated with appropriate mathlib compatibility labels."
+          # Keep the job running indefinitely to show "in progress" status
+          while true; do
+            sleep 3600  # Sleep for 1 hour at a time
+          done

.github/workflows/update-stage0.yml

@@ -40,34 +40,24 @@ jobs:
       run: |
           git config --global user.name "Lean stage0 autoupdater"
           git config --global user.email "<>"
-    # Would be nice, but does not work yet:
-    # https://github.com/DeterminateSystems/magic-nix-cache/issues/39
-    # This action does not run that often and building runs in a few minutes, so ok for now
-    #- if: env.should_update_stage0 == 'yes'
-    #  uses: DeterminateSystems/magic-nix-cache-action@v2
-    - if: env.should_update_stage0 == 'yes'
-      name: Restore Build Cache
-      uses: actions/cache/restore@v4
-      with:
-        path: nix-store-cache
-        key: Nix Linux-nix-store-cache-${{ github.sha }}
-        # fall back to (latest) previous cache
-        restore-keys: |
-          Nix Linux-nix-store-cache
-    - if: env.should_update_stage0 == 'yes'
-      name: Further Set Up Nix Cache
-      shell: bash -euxo pipefail {0}
-      run: |
-        # Nix seems to mutate the cache, so make a copy
-        cp -r nix-store-cache nix-store-cache-copy || true
     - if: env.should_update_stage0 == 'yes'
       name: Install Nix
       uses: DeterminateSystems/nix-installer-action@main
-      with:
-        extra-conf: |
-          substituters = file://${{ github.workspace }}/nix-store-cache-copy?priority=10&trusted=true https://cache.nixos.org  
+    - name: Open Nix shell once
+      if: env.should_update_stage0 == 'yes'
+      run: true
+      shell: 'nix develop -c bash -euxo pipefail {0}'
+    - name: Set up NPROC
+      if: env.should_update_stage0 == 'yes'
+      run: |
+        echo "NPROC=$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)" >> $GITHUB_ENV
+      shell: 'nix develop -c bash -euxo pipefail {0}'
     - if: env.should_update_stage0 == 'yes'
-      run: nix run .#update-stage0-commit
+      run: cmake --preset release
+      shell: 'nix develop -c bash -euxo pipefail {0}'
+    - if: env.should_update_stage0 == 'yes'
+      run: make -j$NPROC -C build/release  update-stage0-commit
+      shell: 'nix develop -c bash -euxo pipefail {0}'
     - if: env.should_update_stage0 == 'yes'
       run: git show --stat
     - if: env.should_update_stage0 == 'yes' && github.event_name == 'push'

src/Init/Control/Lawful/Basic.lean

@@ -6,6 +6,7 @@ Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
 module
 
 prelude
+import Init.Ext
 import Init.SimpLemmas
 import Init.Meta
 
@@ -241,13 +242,23 @@ theorem LawfulMonad.mk' (m : Type u → Type v) [Monad m]
 
 namespace Id
 
-@[simp] theorem map_eq (x : Id α) (f : α → β) : f <$> x = f x := rfl
-@[simp] theorem bind_eq (x : Id α) (f : α → id β) : x >>= f = f x := rfl
-@[simp] theorem pure_eq (a : α) : (pure a : Id α) = a := rfl
+@[ext] theorem ext {x y : Id α} (h : x.run = y.run) : x = y := h
 
 instance : LawfulMonad Id := by
   refine LawfulMonad.mk' _ ?_ ?_ ?_ <;> intros <;> rfl
 
+@[simp] theorem run_map (x : Id α) (f : α → β) : (f <$> x).run = f x.run := rfl
+@[simp] theorem run_bind (x : Id α) (f : α → Id β) : (x >>= f).run = (f x.run).run := rfl
+@[simp] theorem run_pure (a : α) : (pure a : Id α).run = a := rfl
+@[simp] theorem run_seqRight (x y : Id α) : (x *> y).run = y.run := rfl
+@[simp] theorem run_seqLeft (x y : Id α) : (x <* y).run = x.run := rfl
+@[simp] theorem run_seq (f : Id (α → β)) (x : Id α) : (f <*> x).run = f.run x.run := rfl
+
+-- These lemmas are bad as they abuse the defeq of `Id α` and `α`
+@[deprecated run_map (since := "2025-03-05")] theorem map_eq (x : Id α) (f : α → β) : f <$> x = f x := rfl
+@[deprecated run_bind (since := "2025-03-05")] theorem bind_eq (x : Id α) (f : α → id β) : x >>= f = f x := rfl
+@[deprecated run_pure (since := "2025-03-05")] theorem pure_eq (a : α) : (pure a : Id α) = a := rfl
+
 end Id
 
 /-! # Option -/

src/Init/Data/Array/Basic.lean

@@ -544,7 +544,7 @@ Examples:
 -/
 @[inline]
 def modify (xs : Array α) (i : Nat) (f : α → α) : Array α :=
-  Id.run <| modifyM xs i f
+  Id.run <| modifyM xs i (pure <| f ·)
 
 set_option linter.indexVariables false in -- Changing `idx` causes bootstrapping issues, haven't investigated.
 /--
@@ -1059,7 +1059,7 @@ Examples:
 -/
 @[inline]
 def foldl {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : Array α) (start := 0) (stop := as.size) : β :=
-  Id.run <| as.foldlM f init start stop
+  Id.run <| as.foldlM (pure <| f · ·) init start stop
 
 /--
 Folds a function over an array from the right, accumulating a value starting with `init`. The
@@ -1076,7 +1076,7 @@ Examples:
 -/
 @[inline]
 def foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : Array α) (start := as.size) (stop := 0) : β :=
-  Id.run <| as.foldrM f init start stop
+  Id.run <| as.foldrM (pure <| f · ·) init start stop
 
 /--
 Computes the sum of the elements of an array.
@@ -1124,7 +1124,7 @@ Examples:
 -/
 @[inline]
 def map {α : Type u} {β : Type v} (f : α → β) (as : Array α) : Array β :=
-  Id.run <| as.mapM f
+  Id.run <| as.mapM (pure <| f ·)
 
 instance : Functor Array where
   map := map
@@ -1139,7 +1139,7 @@ valid.
 -/
 @[inline]
 def mapFinIdx {α : Type u} {β : Type v} (as : Array α) (f : (i : Nat) → α → (h : i < as.size) → β) : Array β :=
-  Id.run <| as.mapFinIdxM f
+  Id.run <| as.mapFinIdxM (pure <| f · · ·)
 
 /--
 Applies a function to each element of the array along with the index at which that element is found,
@@ -1150,7 +1150,7 @@ is valid.
 -/
 @[inline]
 def mapIdx {α : Type u} {β : Type v} (f : Nat → α → β) (as : Array α) : Array β :=
-  Id.run <| as.mapIdxM f
+  Id.run <| as.mapIdxM (pure <| f · ·)
 
 /--
 Pairs each element of an array with its index, optionally starting from an index other than `0`.
@@ -1198,7 +1198,7 @@ some 10
 -/
 @[inline]
 def findSome? {α : Type u} {β : Type v} (f : α → Option β) (as : Array α) : Option β :=
-  Id.run <| as.findSomeM? f
+  Id.run <| as.findSomeM? (pure <| f ·)
 
 /--
 Returns the first non-`none` result of applying the function `f` to each element of the
@@ -1232,7 +1232,7 @@ Examples:
 -/
 @[inline]
 def findSomeRev? {α : Type u} {β : Type v} (f : α → Option β) (as : Array α) : Option β :=
-  Id.run <| as.findSomeRevM? f
+  Id.run <| as.findSomeRevM? (pure <| f ·)
 
 /--
 Returns the last element of the array for which the predicate `p` returns `true`, or `none` if no
@@ -1244,7 +1244,7 @@ Examples:
 -/
 @[inline]
 def findRev? {α : Type} (p : α → Bool) (as : Array α) : Option α :=
-  Id.run <| as.findRevM? p
+  Id.run <| as.findRevM? (pure <| p ·)
 
 /--
 Returns the index of the first element for which `p` returns `true`, or `none` if there is no such
@@ -1383,7 +1383,7 @@ Examples:
 -/
 @[inline]
 def any (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool :=
-  Id.run <| as.anyM p start stop
+  Id.run <| as.anyM (pure <| p ·) start stop
 
 /--
 Returns `true` if `p` returns `true` for every element of `as`.
@@ -1401,7 +1401,7 @@ Examples:
 -/
 @[inline]
 def all (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool :=
-  Id.run <| as.allM p start stop
+  Id.run <| as.allM (pure <| p ·) start stop
 
 /--
 Checks whether `a` is an element of `as`, using `==` to compare elements.
@@ -1670,7 +1670,7 @@ Example:
 -/
 @[inline]
 def filterMap (f : α → Option β) (as : Array α) (start := 0) (stop := as.size) : Array β :=
-  Id.run <| as.filterMapM f (start := start) (stop := stop)
+  Id.run <| as.filterMapM (pure <| f ·) (start := start) (stop := stop)
 
 /--
 Returns the largest element of the array, as determined by the comparison `lt`, or `none` if

src/Init/Data/Array/BasicAux.lean

@@ -88,4 +88,4 @@ pointer equality, and does not allocate a new array if the result of each functi
 pointer-equal to its argument.
 -/
 @[inline] def Array.mapMono (as : Array α) (f : α → α) : Array α :=
-  Id.run <| as.mapMonoM f
+  Id.run <| as.mapMonoM (pure <| f ·)

src/Init/Data/Array/BinSearch.lean

@@ -129,6 +129,6 @@ Examples:
 * `#[].binInsert (· < ·) 1 = #[1]`
 -/
 @[inline] def binInsert {α : Type u} (lt : α → α → Bool) (as : Array α) (k : α) : Array α :=
-  Id.run <| binInsertM lt (fun _ => k) (fun _ => k) as k
+  Id.run <| binInsertM lt (fun _ => pure k) (fun _ => pure k) as k
 
 end Array

src/Init/Data/Array/Lemmas.lean

@@ -63,7 +63,7 @@ theorem toArray_eq : List.toArray as = xs ↔ as = xs.toList := by
 
 /-! ### size -/
 
-@[grind →] theorem eq_empty_of_size_eq_zero (h : xs.size = 0) : xs = #[] := by
+theorem eq_empty_of_size_eq_zero (h : xs.size = 0) : xs = #[] := by
   cases xs
   simp_all
 
@@ -75,7 +75,6 @@ theorem ne_empty_of_size_pos (h : 0 < xs.size) : xs ≠ #[] := by
   cases xs
   simpa using List.ne_nil_of_length_pos h
 
-@[grind]
 theorem size_eq_zero_iff : xs.size = 0 ↔ xs = #[] :=
   ⟨eq_empty_of_size_eq_zero, fun h => h ▸ rfl⟩
 
@@ -117,14 +116,11 @@ abbrev size_eq_one := @size_eq_one_iff
 
 /-! ## L[i] and L[i]? -/
 
-@[simp] theorem getElem?_eq_none_iff {xs : Array α} : xs[i]? = none ↔ xs.size ≤ i := by
-  by_cases h : i < xs.size
-  · simp [getElem?_pos, h]
-  · rw [getElem?_neg xs i h]
-    simp_all
+theorem getElem?_eq_none_iff {xs : Array α} : xs[i]? = none ↔ xs.size ≤ i := by
+  simp
 
-@[simp] theorem none_eq_getElem?_iff {xs : Array α} {i : Nat} : none = xs[i]? ↔ xs.size ≤ i := by
-  simp [eq_comm (a := none)]
+theorem none_eq_getElem?_iff {xs : Array α} {i : Nat} : none = xs[i]? ↔ xs.size ≤ i := by
+  simp
 
 theorem getElem?_eq_none {xs : Array α} (h : xs.size ≤ i) : xs[i]? = none := by
   simp [getElem?_eq_none_iff, h]
@@ -134,8 +130,8 @@ grind_pattern Array.getElem?_eq_none => xs.size ≤ i, xs[i]?
 @[simp] theorem getElem?_eq_getElem {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i]? = some xs[i] :=
   getElem?_pos ..
 
-theorem getElem?_eq_some_iff {xs : Array α} : xs[i]? = some b ↔ ∃ h : i < xs.size, xs[i] = b := by
-  simp [getElem?_def]
+theorem getElem?_eq_some_iff {xs : Array α} : xs[i]? = some b ↔ ∃ h : i < xs.size, xs[i] = b :=
+  _root_.getElem?_eq_some_iff
 
 @[grind →]
 theorem getElem_of_getElem? {xs : Array α} : xs[i]? = some a → ∃ h : i < xs.size, xs[i] = a :=
@@ -613,13 +609,13 @@ theorem anyM_loop_cons [Monad m] {p : α → m Bool} {a : α} {as : List α} {st
 
 -- Auxiliary for `any_iff_exists`.
 theorem anyM_loop_iff_exists {p : α → Bool} {as : Array α} {start stop} (h : stop ≤ as.size) :
-    anyM.loop (m := Id) p as stop h start = true ↔
+    (anyM.loop (m := Id) (pure <| p ·) as stop h start).run = true ↔
       ∃ (i : Nat) (_ : i < as.size), start ≤ i ∧ i < stop ∧ p as[i] = true := by
   unfold anyM.loop
   split <;> rename_i h₁
   · dsimp
     split <;> rename_i h₂
-    · simp only [true_iff]
+    · simp only [true_iff, Id.run_pure]
       refine ⟨start, by omega, by omega, by omega, h₂⟩
     · rw [anyM_loop_iff_exists]
       constructor
@@ -636,9 +632,9 @@ termination_by stop - start
 -- This could also be proved from `SatisfiesM_anyM_iff_exists` in `Batteries.Data.Array.Init.Monadic`
 theorem any_iff_exists {p : α → Bool} {as : Array α} {start stop} :
     as.any p start stop ↔ ∃ (i : Nat) (_ : i < as.size), start ≤ i ∧ i < stop ∧ p as[i] := by
-  dsimp [any, anyM, Id.run]
+  dsimp [any, anyM]
   split
-  · rw [anyM_loop_iff_exists]
+  · rw [anyM_loop_iff_exists (p := p)]
   · rw [anyM_loop_iff_exists]
     constructor
     · rintro ⟨i, hi, ge, _, h⟩
@@ -1370,17 +1366,17 @@ theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] {f : α → m β} {xs : Ar
 
 @[deprecated "Use `mapM_eq_foldlM` instead" (since := "2025-01-08")]
 theorem mapM_map_eq_foldl {as : Array α} {f : α → β} {i : Nat} :
-    mapM.map (m := Id) f as i b = as.foldl (start := i) (fun acc a => acc.push (f a)) b := by
+    mapM.map (m := Id) (pure <| f ·) as i b = pure (as.foldl (start := i) (fun acc a => acc.push (f a)) b) := by
   unfold mapM.map
   split <;> rename_i h
-  · simp only [Id.bind_eq]
-    dsimp [foldl, Id.run, foldlM]
+  · ext : 1
+    dsimp [foldl, foldlM]
     rw [mapM_map_eq_foldl, dif_pos (by omega), foldlM.loop, dif_pos h]
     -- Calling `split` here gives a bad goal.
     have : size as - i = Nat.succ (size as - i - 1) := by omega
     rw [this]
-    simp [foldl, foldlM, Id.run, Nat.sub_add_eq]
-  · dsimp [foldl, Id.run, foldlM]
+    simp [foldl, foldlM, Nat.sub_add_eq]
+  · dsimp [foldl, foldlM]
     rw [dif_pos (by omega), foldlM.loop, dif_neg h]
     rfl
 termination_by as.size - i
@@ -1602,8 +1598,8 @@ theorem filterMap_congr {as bs : Array α} (h : as = bs)
     as.toList ++ List.filterMap f xs := ?_
   exact this #[]
   induction xs
-  · simp_all [Id.run]
-  · simp_all [Id.run, List.filterMap_cons]
+  · simp_all
+  · simp_all [List.filterMap_cons]
     split <;> simp_all
 
 @[grind] theorem toList_filterMap {f : α → Option β} {xs : Array α} :
@@ -2798,7 +2794,7 @@ theorem reverse_eq_iff {xs ys : Array α} : xs.reverse = ys ↔ xs = ys.reverse
   cases xs
   simp
 
-@[grind _=_]theorem filterMap_reverse {f : α → Option β} {xs : Array α} : (xs.reverse.filterMap f) = (xs.filterMap f).reverse := by
+@[grind _=_] theorem filterMap_reverse {f : α → Option β} {xs : Array α} : (xs.reverse.filterMap f) = (xs.filterMap f).reverse := by
   cases xs
   simp
 
@@ -3215,18 +3211,16 @@ theorem foldlM_push [Monad m] [LawfulMonad m] {xs : Array α} {a : α} {f : β
   rw [foldr, foldrM_start_stop, ← foldrM_toList, List.foldrM_pure, foldr_toList, foldr, ← foldrM_start_stop]
 
 theorem foldl_eq_foldlM {f : β → α → β} {b} {xs : Array α} {start stop : Nat} :
-    xs.foldl f b start stop = xs.foldlM (m := Id) f b start stop := by
-  simp [foldl, Id.run]
+    xs.foldl f b start stop = (xs.foldlM (m := Id) (pure <| f · ·) b start stop).run := rfl
 
 theorem foldr_eq_foldrM {f : α → β → β} {b} {xs : Array α} {start stop : Nat} :
-    xs.foldr f b start stop = xs.foldrM (m := Id) f b start stop := by
-  simp [foldr, Id.run]
+    xs.foldr f b start stop = (xs.foldrM (m := Id) (pure <| f · ·) b start stop).run := rfl
 
 @[simp] theorem id_run_foldlM {f : β → α → Id β} {b} {xs : Array α} {start stop : Nat} :
-    Id.run (xs.foldlM f b start stop) = xs.foldl f b start stop := foldl_eq_foldlM.symm
+    Id.run (xs.foldlM f b start stop) = xs.foldl (f · · |>.run) b start stop := rfl
 
 @[simp] theorem id_run_foldrM {f : α → β → Id β} {b} {xs : Array α} {start stop : Nat} :
-    Id.run (xs.foldrM f b start stop) = xs.foldr f b start stop := foldr_eq_foldrM.symm
+    Id.run (xs.foldrM f b start stop) = xs.foldr (f · · |>.run) b start stop := rfl
 
 /-- Variant of `foldlM_reverse` with a side condition for the `stop` argument. -/
 @[simp] theorem foldlM_reverse' [Monad m] {xs : Array α} {f : β → α → m β} {b} {stop : Nat}
@@ -3526,17 +3520,16 @@ theorem foldrM_append [Monad m] [LawfulMonad m] {f : α → β → m β} {b} {xs
 
 @[simp] theorem foldr_append' {f : α → β → β} {b} {xs ys : Array α} {start : Nat}
     (w : start = xs.size + ys.size) :
-    (xs ++ ys).foldr f b start 0 = xs.foldr f (ys.foldr f b) := by
-  subst w
-  simp [foldr_eq_foldrM]
+    (xs ++ ys).foldr f b start 0 = xs.foldr f (ys.foldr f b) :=
+  foldrM_append' w
 
-@[grind _=_]theorem foldl_append {β : Type _} {f : β → α → β} {b} {xs ys : Array α} :
-    (xs ++ ys).foldl f b = ys.foldl f (xs.foldl f b) := by
-  simp [foldl_eq_foldlM]
+@[grind _=_] theorem foldl_append {β : Type _} {f : β → α → β} {b} {xs ys : Array α} :
+    (xs ++ ys).foldl f b = ys.foldl f (xs.foldl f b) :=
+  foldlM_append
 
 @[grind _=_] theorem foldr_append {f : α → β → β} {b} {xs ys : Array α} :
-    (xs ++ ys).foldr f b = xs.foldr f (ys.foldr f b) := by
-  simp [foldr_eq_foldrM]
+    (xs ++ ys).foldr f b = xs.foldr f (ys.foldr f b) :=
+  foldrM_append
 
 @[simp] theorem foldl_flatten' {f : β → α → β} {b} {xss : Array (Array α)} {stop : Nat}
     (w : stop = xss.flatten.size) :
@@ -3565,21 +3558,22 @@ theorem foldrM_append [Monad m] [LawfulMonad m] {f : α → β → m β} {b} {xs
 /-- Variant of `foldl_reverse` with a side condition for the `stop` argument. -/
 @[simp] theorem foldl_reverse' {xs : Array α} {f : β → α → β} {b} {stop : Nat}
     (w : stop = xs.size) :
-    xs.reverse.foldl f b 0 stop = xs.foldr (fun x y => f y x) b := by
-  simp [w, foldl_eq_foldlM, foldr_eq_foldrM]
+    xs.reverse.foldl f b 0 stop = xs.foldr (fun x y => f y x) b :=
+  foldlM_reverse' w
 
 /-- Variant of `foldr_reverse` with a side condition for the `start` argument. -/
 @[simp] theorem foldr_reverse' {xs : Array α} {f : α → β → β} {b} {start : Nat}
     (w : start = xs.size) :
-    xs.reverse.foldr f b start 0 = xs.foldl (fun x y => f y x) b := by
-  simp [w, foldl_eq_foldlM, foldr_eq_foldrM]
+    xs.reverse.foldr f b start 0 = xs.foldl (fun x y => f y x) b :=
+  foldrM_reverse' w
 
 @[grind] theorem foldl_reverse {xs : Array α} {f : β → α → β} {b} :
-    xs.reverse.foldl f b = xs.foldr (fun x y => f y x) b := by simp [foldl_eq_foldlM, foldr_eq_foldrM]
+    xs.reverse.foldl f b = xs.foldr (fun x y => f y x) b :=
+  foldlM_reverse
 
 @[grind] theorem foldr_reverse {xs : Array α} {f : α → β → β} {b} :
     xs.reverse.foldr f b = xs.foldl (fun x y => f y x) b :=
-  (foldl_reverse ..).symm.trans <| by simp
+  foldrM_reverse
 
 theorem foldl_eq_foldr_reverse {xs : Array α} {f : β → α → β} {b} :
     xs.foldl f b = xs.reverse.foldr (fun x y => f y x) b := by simp
@@ -3785,7 +3779,7 @@ theorem contains_iff_exists_mem_beq [BEq α] {xs : Array α} {a : α} :
   rcases xs with ⟨xs⟩
   simp [List.contains_iff_exists_mem_beq]
 
-@[grind]
+@[grind _=_]
 theorem contains_iff_mem [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     xs.contains a ↔ a ∈ xs := by
   simp
@@ -4094,15 +4088,16 @@ abbrev all_mkArray := @all_replicate
 /-! ### modify -/
 
 @[simp] theorem size_modify {xs : Array α} {i : Nat} {f : α → α} : (xs.modify i f).size = xs.size := by
-  unfold modify modifyM Id.run
+  unfold modify modifyM
   split <;> simp
 
 theorem getElem_modify {xs : Array α} {j i} (h : i < (xs.modify j f).size) :
     (xs.modify j f)[i] = if j = i then f (xs[i]'(by simpa using h)) else xs[i]'(by simpa using h) := by
-  simp only [modify, modifyM, Id.run, Id.pure_eq]
+  simp only [modify, modifyM]
   split
-  · simp only [Id.bind_eq, getElem_set]; split <;> simp [*]
-  · rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))]
+  · simp only [getElem_set, Id.run_pure, Id.run_bind]; split <;> simp [*]
+  · simp only [Id.run_pure]
+    rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))]
 
 @[simp] theorem toList_modify {xs : Array α} {f : α → α} {i : Nat} :
     (xs.modify i f).toList = xs.toList.modify i f := by
@@ -4643,12 +4638,12 @@ namespace Array
 @[simp] theorem findSomeRev?_eq_findSome?_reverse {f : α → Option β} {xs : Array α} :
     xs.findSomeRev? f = xs.reverse.findSome? f := by
   cases xs
-  simp [findSomeRev?, Id.run]
+  simp [findSomeRev?]
 
 @[simp] theorem findRev?_eq_find?_reverse {f : α → Bool} {xs : Array α} :
     xs.findRev? f = xs.reverse.find? f := by
   cases xs
-  simp [findRev?, Id.run]
+  simp [findRev?]
 
 /-! ### unzip -/
 

src/Init/Data/Array/Lex/Lemmas.lean

@@ -29,16 +29,16 @@ protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {xs ys
   Decidable.not_not
 
 @[simp] theorem lex_empty [BEq α] {lt : α → α → Bool} {xs : Array α} : xs.lex #[] lt = false := by
-  simp [lex, Id.run]
+  simp [lex]
 
 @[simp] theorem singleton_lex_singleton [BEq α] {lt : α → α → Bool} : #[a].lex #[b] lt = lt a b := by
   simp only [lex, List.getElem_toArray, List.getElem_singleton]
-  cases lt a b <;> cases a != b <;> simp [Id.run]
+  cases lt a b <;> cases a != b <;> simp
 
 private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs ys : Array α} :
      (#[a] ++ xs).lex (#[b] ++ ys) lt =
        (lt a b || a == b && xs.lex ys lt) := by
-  simp only [lex, Id.run]
+  simp only [lex]
   simp only [Std.Range.forIn'_eq_forIn'_range', size_append, List.size_toArray, List.length_singleton,
     Nat.add_comm 1]
   simp [Nat.add_min_add_right, List.range'_succ, getElem_append_left, List.range'_succ_left,
@@ -51,10 +51,10 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs
 @[simp, grind =] theorem _root_.List.lex_toArray [BEq α] {lt : α → α → Bool} {l₁ l₂ : List α} :
     l₁.toArray.lex l₂.toArray lt = l₁.lex l₂ lt := by
   induction l₁ generalizing l₂ with
-  | nil => cases l₂ <;> simp [lex, Id.run]
+  | nil => cases l₂ <;> simp [lex]
   | cons x l₁ ih =>
     cases l₂ with
-    | nil => simp [lex, Id.run]
+    | nil => simp [lex]
     | cons y l₂ =>
       rw [List.toArray_cons, List.toArray_cons y, cons_lex_cons, List.lex, ih]
 

src/Init/Data/Array/MapIdx.lean

@@ -27,7 +27,7 @@ theorem mapFinIdx_induction (xs : Array α) (f : (i : Nat) → α → (h : i < x
     motive xs.size ∧ ∃ eq : (Array.mapFinIdx xs f).size = xs.size,
       ∀ i h, p i ((Array.mapFinIdx xs f)[i]) h := by
   let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : ∀ i h h', p i bs[i] h) (hm : motive j) :
-    let as : Array β := Array.mapFinIdxM.map (m := Id) xs f i j h bs
+    let as : Array β := Id.run <| Array.mapFinIdxM.map xs (pure <| f · · ·) i j h bs
     motive xs.size ∧ ∃ eq : as.size = xs.size, ∀ i h, p i as[i] h := by
     induction i generalizing j bs with simp [mapFinIdxM.map]
     | zero =>

src/Init/Data/Array/Monadic.lean

@@ -36,7 +36,11 @@ open Nat
     xs.mapM (m := m) (pure <| f ·) = pure (xs.map f) := by
   induction xs; simp_all
 
-@[simp] theorem mapM_id {xs : Array α} {f : α → Id β} : xs.mapM f = xs.map f :=
+@[simp] theorem idRun_mapM {xs : Array α} {f : α → Id β} : (xs.mapM f).run = xs.map (f · |>.run) :=
+  mapM_pure
+
+@[deprecated idRun_mapM (since := "2025-05-21")]
+theorem mapM_id {xs : Array α} {f : α → Id β} : xs.mapM f = xs.map f :=
   mapM_pure
 
 @[simp] theorem mapM_map [Monad m] [LawfulMonad m] {f : α → β} {g : β → m γ} {xs : Array α} :
@@ -191,12 +195,18 @@ theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
   rcases xs with ⟨xs⟩
   simp [List.forIn'_pure_yield_eq_foldl, List.foldl_map]
 
-@[simp] theorem forIn'_yield_eq_foldl
+@[simp] theorem idRun_forIn'_yield_eq_foldl
+    {xs : Array α} (f : (a : α) → a ∈ xs → β → Id β) (init : β) :
+    (forIn' xs init (fun a m b => .yield <$> f a m b)).run =
+      xs.attach.foldl (fun b ⟨a, h⟩ => f a h b |>.run) init :=
+  forIn'_pure_yield_eq_foldl _ _
+
+@[deprecated idRun_forIn'_yield_eq_foldl (since := "2025-05-21")]
+theorem forIn'_yield_eq_foldl
     {xs : Array α} (f : (a : α) → a ∈ xs → β → β) (init : β) :
     forIn' (m := Id) xs init (fun a m b => .yield (f a m b)) =
-      xs.attach.foldl (fun b ⟨a, h⟩ => f a h b) init := by
-  rcases xs with ⟨xs⟩
-  simp [List.foldl_map]
+      xs.attach.foldl (fun b ⟨a, h⟩ => f a h b) init :=
+  forIn'_pure_yield_eq_foldl _ _
 
 @[simp] theorem forIn'_map [Monad m] [LawfulMonad m]
     {xs : Array α} (g : α → β) (f : (b : β) → b ∈ xs.map g → γ → m (ForInStep γ)) :
@@ -233,12 +243,18 @@ theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
   rcases xs with ⟨xs⟩
   simp [List.forIn_pure_yield_eq_foldl, List.foldl_map]
 
-@[simp] theorem forIn_yield_eq_foldl
+@[simp] theorem idRun_forIn_yield_eq_foldl
+    {xs : Array α} (f : α → β → Id β) (init : β) :
+    (forIn xs init (fun a b => .yield <$> f a b)).run =
+      xs.foldl (fun b a => f a b |>.run) init :=
+  forIn_pure_yield_eq_foldl _ _
+
+@[deprecated idRun_forIn_yield_eq_foldl (since := "2025-05-21")]
+theorem forIn_yield_eq_foldl
     {xs : Array α} (f : α → β → β) (init : β) :
     forIn (m := Id) xs init (fun a b => .yield (f a b)) =
-      xs.foldl (fun b a => f a b) init := by
-  rcases xs with ⟨xs⟩
-  simp [List.foldl_map]
+      xs.foldl (fun b a => f a b) init :=
+  forIn_pure_yield_eq_foldl _ _
 
 @[simp] theorem forIn_map [Monad m] [LawfulMonad m]
     {xs : Array α} {g : α → β} {f : β → γ → m (ForInStep γ)} :

src/Init/Data/Array/OfFn.lean

@@ -82,7 +82,7 @@ theorem ofFnM_succ' {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} :
       let a ← f 0
       let as ← ofFnM fun i => f i.succ
       pure (#[a] ++ as)) := by
-  simp [ofFnM, Fin.foldlM_eq_finRange_foldlM, List.foldlM_push_eq_append, List.finRange_succ, Function.comp_def]
+  simp [ofFnM, Fin.foldlM_eq_foldlM_finRange, List.foldlM_push_eq_append, List.finRange_succ, Function.comp_def]
 
 theorem ofFnM_succ {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} :
     ofFnM f = (do
@@ -129,7 +129,6 @@ theorem ofFnM_pure [Monad m] [LawfulMonad m] {n} {f : Fin n → α} :
 
 @[simp, grind =] theorem idRun_ofFnM {f : Fin n → Id α} :
     Id.run (ofFnM f) = ofFn (fun i => Id.run (f i)) := by
-  unfold Id.run
   induction n with
   | zero => simp
   | succ n ih => simp [ofFnM_succ', ofFn_succ', ih]

src/Init/Data/Array/QSort/Basic.lean

@@ -27,23 +27,27 @@ Internal implementation of `Array.qsort`.
 
 It does so by first swapping the elements at indices `lo`, `mid := (lo + hi) / 2`, and `hi`
 if necessary so that the middle (pivot) element is at index `hi`.
-We then iterate from `j = lo` to `j = hi`, with a pointer `i` starting at `lo`, and
+We then iterate from `k = lo` to `k = hi`, with a pointer `i` starting at `lo`, and
 swapping each element which is less than the pivot to position `i`, and then incrementing `i`.
 -/
-def qpartition {n} (as : Vector α n) (lt : α → α → Bool) (lo hi : Nat)
-    (hlo : lo < n := by omega) (hhi : hi < n := by omega) : {m : Nat // lo ≤ m ∧ m < n} × Vector α n :=
+def qpartition {n} (as : Vector α n) (lt : α → α → Bool) (lo hi : Nat) (w : lo ≤ hi := by omega)
+    (hlo : lo < n := by omega) (hhi : hi < n := by omega) : {m : Nat // lo ≤ m ∧ m ≤ hi} × Vector α n :=
   let mid := (lo + hi) / 2
   let as  := if lt as[mid] as[lo] then as.swap lo mid else as
   let as  := if lt as[hi]  as[lo] then as.swap lo hi  else as
   let as  := if lt as[mid] as[hi] then as.swap mid hi else as
   let pivot := as[hi]
-  let rec loop (as : Vector α n) (i j : Nat)
-      (ilo : lo ≤ i := by omega) (jh : j < n := by omega) (w : i ≤ j := by omega) :=
-    if h : j < hi then
-      if lt as[j] pivot then
-        loop (as.swap i j) (i+1) (j+1)
+  -- During this loop, elements below in `[lo, i)` are less than `pivot`,
+  -- elements in `[i, k)` are greater than or equal to `pivot`,
+  -- elements in `[k, hi)` are unexamined,
+  -- while `as[hi]` is (by definition) the pivot.
+  let rec loop (as : Vector α n) (i k : Nat)
+      (ilo : lo ≤ i := by omega) (ik : i ≤ k := by omega) (w : k ≤ hi := by omega) :=
+    if h : k < hi then
+      if lt as[k] pivot then
+        loop (as.swap i k) (i+1) (k+1)
       else
-        loop as i (j+1)
+        loop as i (k+1)
     else
       (⟨i, ilo, by omega⟩, as.swap i hi)
   loop as lo lo
@@ -51,25 +55,28 @@ def qpartition {n} (as : Vector α n) (lt : α → α → Bool) (lo hi : Nat)
 /--
 In-place quicksort.
 
-`qsort as lt low high` sorts the subarray `as[low:high+1]` in-place using `lt` to compare elements.
+`qsort as lt lo hi` sorts the subarray `as[lo:hi+1]` in-place using `lt` to compare elements.
 -/
 @[inline] def qsort (as : Array α) (lt : α → α → Bool := by exact (· < ·))
-    (low := 0) (high := as.size - 1) : Array α :=
-  let rec @[specialize] sort {n} (as : Vector α n) (lo hi : Nat)
+    (lo := 0) (hi := as.size - 1) : Array α :=
+  let rec @[specialize] sort {n} (as : Vector α n) (lo hi : Nat) (w : lo ≤ hi := by omega)
       (hlo : lo < n := by omega) (hhi : hi < n := by omega) :=
     if h₁ : lo < hi then
       let ⟨⟨mid, hmid⟩, as⟩ := qpartition as lt lo hi
       if h₂ : mid ≥ hi then
+        -- This only occurs when `hi ≤ lo`,
+        -- and thus `as[lo:hi+1]` is trivially already sorted.
         as
       else
+        -- Otherwise, we recursively sort the two subarrays.
         sort (sort as lo mid) (mid+1) hi
     else as
   if h : as.size = 0 then
     as
   else
-    let low := min low (as.size - 1)
-    let high := min high (as.size - 1)
-    sort as.toVector low high |>.toArray
+    let lo := min lo (as.size - 1)
+    let hi := max lo (min hi (as.size - 1))
+    sort as.toVector lo hi |>.toArray
 
 set_option linter.unusedVariables.funArgs false in
 /--

src/Init/Data/Array/Subarray.lean

@@ -290,7 +290,7 @@ Examples:
 -/
 @[inline]
 def foldl {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : Subarray α) : β :=
-  Id.run <| as.foldlM f (init := init)
+  Id.run <| as.foldlM (pure <| f · ·) (init := init)
 
 /--
 Folds an operation from right to left over the elements in a subarray.
@@ -304,7 +304,7 @@ Examples:
 -/
 @[inline]
 def foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : Subarray α) : β :=
-  Id.run <| as.foldrM f (init := init)
+  Id.run <| as.foldrM (pure <| f · ·) (init := init)
 
 /--
 Checks whether any of the elements in a subarray satisfy a Boolean predicate.
@@ -314,7 +314,7 @@ an element that satisfies the predicate is found.
 -/
 @[inline]
 def any {α : Type u} (p : α → Bool) (as : Subarray α) : Bool :=
-  Id.run <| as.anyM p
+  Id.run <| as.anyM (pure <| p ·)
 
 /--
 Checks whether all of the elements in a subarray satisfy a Boolean predicate.
@@ -324,7 +324,7 @@ an element that does not satisfy the predicate is found.
 -/
 @[inline]
 def all {α : Type u} (p : α → Bool) (as : Subarray α) : Bool :=
-  Id.run <| as.allM p
+  Id.run <| as.allM (pure <| p ·)
 
 /--
 Applies a monadic function to each element in a subarray in reverse order, stopping at the first
@@ -394,7 +394,7 @@ Examples:
 -/
 @[inline]
 def findRev? {α : Type} (as : Subarray α) (p : α → Bool) : Option α :=
-  Id.run <| as.findRevM? p
+  Id.run <| as.findRevM? (pure <| p ·)
 
 end Subarray
 

src/Init/Data/BitVec/Lemmas.lean

@@ -68,11 +68,11 @@ theorem lt_of_getMsbD {x : BitVec w} {i : Nat} : getMsbD x i = true → i < w :=
 @[simp] theorem getElem?_eq_getElem {l : BitVec w} {n} (h : n < w) : l[n]? = some l[n] := by
   simp only [getElem?_def, h, ↓reduceDIte]
 
-theorem getElem?_eq_some_iff {l : BitVec w} : l[n]? = some a ↔ ∃ h : n < w, l[n] = a := by
-  simp only [getElem?_def]
-  split
-  · simp_all
-  · simp; omega
+theorem getElem?_eq_some_iff {l : BitVec w} : l[n]? = some a ↔ ∃ h : n < w, l[n] = a :=
+  _root_.getElem?_eq_some_iff
+
+theorem some_eq_getElem?_iff {l : BitVec w} : some a = l[n]? ↔ ∃ h : n < w, l[n] = a :=
+  _root_.some_eq_getElem?_iff
 
 theorem getElem_of_getElem? {l : BitVec w} : l[n]? = some a → ∃ h : n < w, l[n] = a :=
   getElem?_eq_some_iff.mp
@@ -81,11 +81,11 @@ set_option linter.missingDocs false in
 @[deprecated getElem?_eq_some_iff (since := "2025-02-17")]
 abbrev getElem?_eq_some := @getElem?_eq_some_iff
 
-@[simp] theorem getElem?_eq_none_iff {l : BitVec w} : l[n]? = none ↔ w ≤ n := by
-  simp only [getElem?_def]
-  split
-  · simp_all
-  · simp; omega
+theorem getElem?_eq_none_iff {l : BitVec w} : l[n]? = none ↔ w ≤ n := by
+  simp
+
+theorem none_eq_getElem?_iff {l : BitVec w} : none = l[n]? ↔ w ≤ n := by
+  simp
 
 theorem getElem?_eq_none {l : BitVec w} (h : w ≤ n) : l[n]? = none := getElem?_eq_none_iff.mpr h
 

src/Init/Data/ByteArray/Basic.lean

@@ -205,7 +205,7 @@ def foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 →
 
 @[inline]
 def foldl {β : Type v} (f : β → UInt8 → β) (init : β) (as : ByteArray) (start := 0) (stop := as.size) : β :=
-  Id.run <| as.foldlM f init start stop
+  Id.run <| as.foldlM (pure <| f · ·) init start stop
 
 /-- Iterator over the bytes (`UInt8`) of a `ByteArray`.
 

src/Init/Data/Fin/Fold.lean

@@ -266,7 +266,7 @@ theorem foldl_add (f : α → Fin (n + m) → α) (x) :
   | succ m ih => simp [foldl_succ_last, ih, ← Nat.add_assoc]
 
 theorem foldl_eq_foldlM (f : α → Fin n → α) (x) :
-    foldl n f x = foldlM (m:=Id) n f x := by
+    foldl n f x = (foldlM (m := Id) n (pure <| f · ·) x).run := by
   induction n generalizing x <;> simp [foldl_succ, foldlM_succ, *]
 
 -- This is not marked `@[simp]` as it would match on every occurrence of `foldlM`.
@@ -319,7 +319,7 @@ theorem foldr_add (f : Fin (n + m) → α → α) (x) :
   | succ m ih => simp [foldr_succ_last, ih, ← Nat.add_assoc]
 
 theorem foldr_eq_foldrM (f : Fin n → α → α) (x) :
-    foldr n f x = foldrM (m:=Id) n f x := by
+    foldr n f x = (foldrM (m := Id) n (pure <| f · ·) x).run := by
   induction n <;> simp [foldr_succ, foldrM_succ, *]
 
 theorem foldl_rev (f : Fin n → α → α) (x) :

src/Init/Data/FloatArray/Basic.lean

@@ -165,7 +165,7 @@ def foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → Float →
 
 @[inline]
 def foldl {β : Type v} (f : β → Float → β) (init : β) (as : FloatArray) (start := 0) (stop := as.size) : β :=
-  Id.run <| as.foldlM f init start stop
+  Id.run <| as.foldlM (pure <| f · ·) init start stop
 
 end FloatArray
 

src/Init/Data/List/BasicAux.lean

@@ -254,7 +254,7 @@ pointer-equal to its argument.
 For verification purposes, `List.mapMono = List.map`.
 -/
 def mapMono (as : List α) (f : α → α) : List α :=
-  Id.run <| as.mapMonoM f
+  Id.run <| as.mapMonoM (pure <| f ·)
 
 /-! ## Additional lemmas required for bootstrapping `Array`. -/
 

src/Init/Data/List/Control.lean

@@ -348,9 +348,16 @@ theorem findM?_pure {m} [Monad m] [LawfulMonad m] (p : α → Bool) (as : List
     | false => simp [ih]
 
 @[simp]
-theorem findM?_id (p : α → Bool) (as : List α) : findM? (m := Id) p as = as.find? p :=
+theorem idRun_findM? (p : α → Id Bool) (as : List α) :
+    (findM? p as).run = as.find? (p · |>.run) :=
   findM?_pure _ _
 
+@[deprecated idRun_findM? (since := "2025-05-21")]
+theorem findM?_id (p : α → Id Bool) (as : List α) :
+    findM? (m := Id) p as = as.find? p :=
+  findM?_pure _ _
+
+
 /--
 Returns the first non-`none` result of applying the monadic function `f` to each element of the
 list, in order. Returns `none` if `f` returns `none` for all elements.
@@ -394,7 +401,13 @@ theorem findSomeM?_pure [Monad m] [LawfulMonad m] {f : α → Option β} {as : L
     | none   => simp [ih]
 
 @[simp]
-theorem findSomeM?_id {f : α → Option β} {as : List α} : findSomeM? (m := Id) f as = as.findSome? f :=
+theorem idRun_findSomeM? (f : α → Id (Option β)) (as : List α) :
+    (findSomeM? f as).run = as.findSome? (f · |>.run) :=
+  findSomeM?_pure
+
+@[deprecated idRun_findSomeM? (since := "2025-05-21")]
+theorem findSomeM?_id (f : α → Id (Option β)) (as : List α) :
+    findSomeM? (m := Id) f as = as.findSome? f :=
   findSomeM?_pure
 
 theorem findM?_eq_findSomeM? [Monad m] [LawfulMonad m] {p : α → m Bool} {as : List α} :

src/Init/Data/List/FinRange.lean

@@ -61,7 +61,7 @@ end List
 
 namespace Fin
 
-theorem foldlM_eq_finRange_foldlM [Monad m] (f : α → Fin n → m α) (x : α) :
+theorem foldlM_eq_foldlM_finRange [Monad m] (f : α → Fin n → m α) (x : α) :
     foldlM n f x = (List.finRange n).foldlM f x := by
   induction n generalizing x with
   | zero => simp
@@ -71,7 +71,7 @@ theorem foldlM_eq_finRange_foldlM [Monad m] (f : α → Fin n → m α) (x : α)
     funext y
     simp [ih, List.foldlM_map]
 
-theorem foldrM_eq_finRange_foldrM [Monad m] [LawfulMonad m] (f : Fin n → α → m α) (x : α) :
+theorem foldrM_eq_foldrM_finRange [Monad m] [LawfulMonad m] (f : Fin n → α → m α) (x : α) :
     foldrM n f x = (List.finRange n).foldrM f x := by
   induction n generalizing x with
   | zero => simp
@@ -101,7 +101,7 @@ theorem ofFnM_succ {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} :
       let a ← f 0
       let as ← ofFnM fun i => f i.succ
       pure (a :: as)) := by
-  simp [ofFnM, Fin.foldlM_eq_finRange_foldlM, List.finRange_succ, List.foldlM_cons_eq_append,
+  simp [ofFnM, Fin.foldlM_eq_foldlM_finRange, List.finRange_succ, List.foldlM_cons_eq_append,
     List.foldlM_map]
 
 end List

src/Init/Data/List/Lemmas.lean

@@ -2541,17 +2541,25 @@ theorem flatten_reverse {L : List (List α)} :
   induction l generalizing b <;> simp [*]
 
 theorem foldl_eq_foldlM {f : β → α → β} {b : β} {l : List α} :
-    l.foldl f b = l.foldlM (m := Id) f b := by
-  induction l generalizing b <;> simp [*, foldl]
+    l.foldl f b = (l.foldlM (m := Id) (pure <| f · ·) b).run := by
+  simp
 
 theorem foldr_eq_foldrM {f : α → β → β} {b : β} {l : List α} :
-    l.foldr f b = l.foldrM (m := Id) f b := by
-  induction l <;> simp [*, foldr]
+    l.foldr f b = (l.foldrM (m := Id) (pure <| f · ·) b).run := by
+  simp
 
-@[simp] theorem id_run_foldlM {f : β → α → Id β} {b : β} {l : List α} :
+theorem idRun_foldlM {f : β → α → Id β} {b : β} {l : List α} :
+    Id.run (l.foldlM f b) = l.foldl (f · · |>.run) b := foldl_eq_foldlM.symm
+
+@[deprecated idRun_foldlM (since := "2025-05-21")]
+theorem id_run_foldlM {f : β → α → Id β} {b : β} {l : List α} :
     Id.run (l.foldlM f b) = l.foldl f b := foldl_eq_foldlM.symm
 
-@[simp] theorem id_run_foldrM {f : α → β → Id β} {b : β} {l : List α} :
+theorem idRun_foldrM {f : α → β → Id β} {b : β} {l : List α} :
+    Id.run (l.foldrM f b) = l.foldr (f · · |>.run) b := foldr_eq_foldrM.symm
+
+@[deprecated idRun_foldrM (since := "2025-05-21")]
+theorem id_run_foldrM {f : α → β → Id β} {b : β} {l : List α} :
     Id.run (l.foldrM f b) = l.foldr f b := foldr_eq_foldrM.symm
 
 @[simp] theorem foldlM_reverse [Monad m] {l : List α} {f : β → α → m β} {b : β} :
@@ -2646,10 +2654,10 @@ theorem foldr_map_hom {g : α → β} {f : α → α → α} {f' : β → β →
   induction l <;> simp [*]
 
 @[simp, grind _=_] theorem foldl_append {β : Type _} {f : β → α → β} {b : β} {l l' : List α} :
-    (l ++ l').foldl f b = l'.foldl f (l.foldl f b) := by simp [foldl_eq_foldlM]
+    (l ++ l').foldl f b = l'.foldl f (l.foldl f b) := by simp [foldl_eq_foldlM, -foldlM_pure]
 
 @[simp, grind _=_] theorem foldr_append {f : α → β → β} {b : β} {l l' : List α} :
-    (l ++ l').foldr f b = l.foldr f (l'.foldr f b) := by simp [foldr_eq_foldrM]
+    (l ++ l').foldr f b = l.foldr f (l'.foldr f b) := by simp [foldr_eq_foldrM, -foldrM_pure]
 
 @[grind] theorem foldl_flatten {f : β → α → β} {b : β} {L : List (List α)} :
     (flatten L).foldl f b = L.foldl (fun b l => l.foldl f b) b := by
@@ -2660,7 +2668,8 @@ theorem foldr_map_hom {g : α → β} {f : α → α → α} {f' : β → β →
   induction L <;> simp_all
 
 @[simp, grind] theorem foldl_reverse {l : List α} {f : β → α → β} {b : β} :
-    l.reverse.foldl f b = l.foldr (fun x y => f y x) b := by simp [foldl_eq_foldlM, foldr_eq_foldrM]
+    l.reverse.foldl f b = l.foldr (fun x y => f y x) b := by
+  simp [foldl_eq_foldlM, foldr_eq_foldrM, -foldrM_pure]
 
 @[simp, grind] theorem foldr_reverse {l : List α} {f : α → β → β} {b : β} :
     l.reverse.foldr f b = l.foldl (fun x y => f y x) b :=
@@ -2943,7 +2952,7 @@ theorem contains_iff_exists_mem_beq [BEq α] {l : List α} {a : α} :
     l.contains a ↔ ∃ a' ∈ l, a == a' := by
   induction l <;> simp_all
 
-@[grind]
+@[grind _=_]
 theorem contains_iff_mem [BEq α] [LawfulBEq α] {l : List α} {a : α} :
     l.contains a ↔ a ∈ l := by
   simp

src/Init/Data/List/Monadic.lean

@@ -68,7 +68,11 @@ theorem mapM'_eq_mapM [Monad m] [LawfulMonad m] {f : α → m β} {l : List α}
     l.mapM (m := m) (pure <| f ·) = pure (l.map f) := by
   induction l <;> simp_all
 
-@[simp] theorem mapM_id {l : List α} {f : α → Id β} : l.mapM f = l.map f :=
+@[simp] theorem idRun_mapM {l : List α} {f : α → Id β} : (l.mapM f).run = l.map (f · |>.run) :=
+  mapM_pure
+
+@[deprecated idRun_mapM (since := "2025-05-21")]
+theorem mapM_id {l : List α} {f : α → Id β} : (l.mapM f).run = l.map (f · |>.run) :=
   mapM_pure
 
 @[simp] theorem mapM_map [Monad m] [LawfulMonad m] {f : α → β} {g : β → m γ} {l : List α} :
@@ -345,12 +349,18 @@ theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
   simp only [forIn'_eq_foldlM]
   induction l.attach generalizing init <;> simp_all
 
-@[simp] theorem forIn'_yield_eq_foldl
+@[simp] theorem idRun_forIn'_yield_eq_foldl
+    (l : List α) (f : (a : α) → a ∈ l → β → Id β) (init : β) :
+    (forIn' l init (fun a m b => .yield <$> f a m b)).run =
+      l.attach.foldl (fun b ⟨a, h⟩ => f a h b |>.run) init :=
+  forIn'_pure_yield_eq_foldl _ _
+
+@[deprecated idRun_forIn'_yield_eq_foldl (since := "2025-05-21")]
+theorem forIn'_yield_eq_foldl
     {l : List α} (f : (a : α) → a ∈ l → β → β) (init : β) :
     forIn' (m := Id) l init (fun a m b => .yield (f a m b)) =
-      l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init := by
-  simp only [forIn'_eq_foldlM]
-  induction l.attach generalizing init <;> simp_all
+      l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init :=
+  forIn'_pure_yield_eq_foldl _ _
 
 @[simp] theorem forIn'_map [Monad m] [LawfulMonad m]
     {l : List α} (g : α → β) (f : (b : β) → b ∈ l.map g → γ → m (ForInStep γ)) :
@@ -398,12 +408,18 @@ theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
   simp only [forIn_eq_foldlM]
   induction l generalizing init <;> simp_all
 
-@[simp] theorem forIn_yield_eq_foldl
+@[simp] theorem idRun_forIn_yield_eq_foldl
+    (l : List α) (f : α → β → Id β) (init : β) :
+    (forIn l init (fun a b => .yield <$> f a b)).run =
+      l.foldl (fun b a => f a b |>.run) init :=
+  forIn_pure_yield_eq_foldl _ _
+
+@[deprecated idRun_forIn_yield_eq_foldl (since := "2025-05-21")]
+theorem forIn_yield_eq_foldl
     {l : List α} (f : α → β → β) (init : β) :
     forIn (m := Id) l init (fun a b => .yield (f a b)) =
-      l.foldl (fun b a => f a b) init := by
-  simp only [forIn_eq_foldlM]
-  induction l generalizing init <;> simp_all
+      l.foldl (fun b a => f a b) init :=
+  forIn_pure_yield_eq_foldl _ _
 
 @[simp] theorem forIn_map [Monad m] [LawfulMonad m]
     {l : List α} {g : α → β} {f : β → γ → m (ForInStep γ)} :

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

@@ -56,7 +56,7 @@ theorem getElem?_take_eq_none {l : List α} {i j : Nat} (h : i ≤ j) :
     (l.take i)[j]? = none :=
   getElem?_eq_none <| Nat.le_trans (length_take_le _ _) h
 
-@[grind =]theorem getElem?_take {l : List α} {i j : Nat} :
+@[grind =] theorem getElem?_take {l : List α} {i j : Nat} :
     (l.take i)[j]? = if j < i then l[j]? else none := by
   split
   · next h => exact getElem?_take_of_lt h

src/Init/Data/List/OfFn.lean

@@ -71,6 +71,7 @@ protected theorem getElem?_ofFn {f : Fin n → α} :
 theorem ofFn_zero {f : Fin 0 → α} : ofFn f = [] := by
   rw [ofFn, Fin.foldr_zero]
 
+@[simp]
 theorem ofFn_succ {n} {f : Fin (n + 1) → α} : ofFn f = f 0 :: ofFn fun i => f i.succ :=
   ext_get (by simp) (fun i hi₁ hi₂ => by
     cases i
@@ -91,7 +92,7 @@ theorem ofFn_add {n m} {f : Fin (n + m) → α} :
     ofFn f = (ofFn fun i => f (i.castLE (Nat.le_add_right n m))) ++ (ofFn fun i => f (i.natAdd n)) := by
   induction m with
   | zero => simp
-  | succ m ih => simp [ofFn_succ_last, ih]
+  | succ m ih => simp [-ofFn_succ, ofFn_succ_last, ih]
 
 @[simp]
 theorem ofFn_eq_nil_iff {f : Fin n → α} : ofFn f = [] ↔ n = 0 := by
@@ -172,9 +173,8 @@ theorem ofFnM_pure [Monad m] [LawfulMonad m] {n} {f : Fin n → α} :
 
 @[simp, grind =] theorem idRun_ofFnM {f : Fin n → Id α} :
     Id.run (ofFnM f) = ofFn (fun i => Id.run (f i)) := by
-  unfold Id.run
   induction n with
   | zero => simp
-  | succ n ih => simp [ofFnM_succ_last, ofFn_succ_last, ih]
+  | succ n ih => simp [-ofFn_succ, ofFnM_succ_last, ofFn_succ_last, ih]
 
 end List

src/Init/Data/List/TakeDrop.lean

@@ -31,6 +31,11 @@ theorem take_cons {l : List α} (h : 0 < i) : (a :: l).take i = a :: l.take (i -
   | zero => exact absurd h (Nat.lt_irrefl _)
   | succ i => rfl
 
+theorem drop_cons {l : List α} (h : 0 < i) : (a :: l).drop i = l.drop (i - 1) := by
+  cases i with
+  | zero => exact absurd h (Nat.lt_irrefl _)
+  | succ i => rfl
+
 @[simp]
 theorem drop_one : ∀ {l : List α}, l.drop 1 = l.tail
   | [] | _ :: _ => rfl

src/Init/Data/List/ToArray.lean

@@ -256,16 +256,16 @@ theorem findRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : Lis
 
 @[simp, grind =] theorem findSome?_toArray (f : α → Option β) (l : List α) :
     l.toArray.findSome? f = l.findSome? f := by
-  rw [Array.findSome?, ← findSomeM?_id, findSomeM?_toArray, Id.run]
+  rw [Array.findSome?, findSomeM?_toArray, findSomeM?_pure, Id.run_pure]
 
 @[simp, grind =] theorem find?_toArray (f : α → Bool) (l : List α) :
     l.toArray.find? f = l.find? f := by
   rw [Array.find?]
-  simp only [Id.run, Id, Id.pure_eq, Id.bind_eq, forIn_toArray]
+  simp only [forIn_toArray]
   induction l with
   | nil => simp
   | cons a l ih =>
-    simp only [forIn_cons, Id.pure_eq, Id.bind_eq, find?]
+    simp only [forIn_cons, find?]
     by_cases f a <;> simp_all
 
 private theorem findFinIdx?_loop_toArray (w : l' = l.drop j) :

src/Init/Data/Option/Array.lean

@@ -39,11 +39,11 @@ namespace Option
     o.toArray.foldr f a = o.elim a (fun b => f b a) := by
   cases o <;> simp
 
-@[simp]
+@[simp, grind =]
 theorem toList_toArray {o : Option α} : o.toArray.toList = o.toList := by
   cases o <;> simp
 
-@[simp]
+@[simp, grind =]
 theorem toArray_toList {o : Option α} : o.toList.toArray = o.toArray := by
   cases o <;> simp
 
@@ -69,7 +69,8 @@ theorem toArray_min [Min α] {o o' : Option α} :
 theorem size_toArray_le {o : Option α} : o.toArray.size ≤ 1 := by
   cases o <;> simp
 
-theorem size_toArray_eq_ite {o : Option α} :
+@[grind =]
+theorem size_toArray {o : Option α} :
     o.toArray.size = if o.isSome then 1 else 0 := by
   cases o <;> simp
 

src/Init/Data/Option/Attach.lean

@@ -51,12 +51,12 @@ terminates.
 -/
 @[inline] def attach (xs : Option α) : Option {x // xs = some x} := xs.attachWith _ fun _ => id
 
-@[simp] theorem attach_none : (none : Option α).attach = none := rfl
-@[simp] theorem attachWith_none : (none : Option α).attachWith P H = none := rfl
+@[simp, grind =] theorem attach_none : (none : Option α).attach = none := rfl
+@[simp, grind =] theorem attachWith_none : (none : Option α).attachWith P H = none := rfl
 
-@[simp] theorem attach_some {x : α} :
+@[simp, grind =] theorem attach_some {x : α} :
     (some x).attach = some ⟨x, rfl⟩ := rfl
-@[simp] theorem attachWith_some {x : α} {P : α → Prop} (h : ∀ (b : α), some x = some b → P b) :
+@[simp, grind =] theorem attachWith_some {x : α} {P : α → Prop} (h : ∀ (b : α), some x = some b → P b) :
     (some x).attachWith P h = some ⟨x, by simpa using h⟩ := rfl
 
 theorem attach_congr {o₁ o₂ : Option α} (h : o₁ = o₂) :
@@ -76,7 +76,7 @@ theorem attach_map_val (o : Option α) (f : α → β) :
 @[deprecated attach_map_val (since := "2025-02-17")]
 abbrev attach_map_coe := @attach_map_val
 
-theorem attach_map_subtype_val (o : Option α) :
+@[simp, grind =]theorem attach_map_subtype_val (o : Option α) :
     o.attach.map Subtype.val = o :=
   (attach_map_val _ _).trans (congrFun Option.map_id _)
 
@@ -87,7 +87,7 @@ theorem attachWith_map_val {p : α → Prop} (f : α → β) (o : Option α) (H
 @[deprecated attachWith_map_val (since := "2025-02-17")]
 abbrev attachWith_map_coe := @attachWith_map_val
 
-theorem attachWith_map_subtype_val {p : α → Prop} (o : Option α) (H : ∀ a, o = some a → p a) :
+@[simp, grind =] theorem attachWith_map_subtype_val {p : α → Prop} (o : Option α) (H : ∀ a, o = some a → p a) :
     (o.attachWith p H).map Subtype.val = o :=
   (attachWith_map_val _ _ _).trans (congrFun Option.map_id _)
 
@@ -98,17 +98,17 @@ theorem attach_eq_some : ∀ (o : Option α) (x : {x // o = some x}), o.attach =
 theorem mem_attach : ∀ (o : Option α) (x : {x // o = some x}), x ∈ o.attach :=
   attach_eq_some
 
-@[simp] theorem isNone_attach (o : Option α) : o.attach.isNone = o.isNone := by
+@[simp, grind =] theorem isNone_attach (o : Option α) : o.attach.isNone = o.isNone := by
   cases o <;> simp
 
-@[simp] theorem isNone_attachWith {p : α → Prop} (o : Option α) (H : ∀ a, o = some a → p a) :
+@[simp, grind =] theorem isNone_attachWith {p : α → Prop} (o : Option α) (H : ∀ a, o = some a → p a) :
     (o.attachWith p H).isNone = o.isNone := by
   cases o <;> simp
 
-@[simp] theorem isSome_attach (o : Option α) : o.attach.isSome = o.isSome := by
+@[simp, grind =] theorem isSome_attach (o : Option α) : o.attach.isSome = o.isSome := by
   cases o <;> simp
 
-@[simp] theorem isSome_attachWith {p : α → Prop} (o : Option α) (H : ∀ a, o = some a → p a) :
+@[simp, grind =] theorem isSome_attachWith {p : α → Prop} (o : Option α) (H : ∀ a, o = some a → p a) :
     (o.attachWith p H).isSome = o.isSome := by
   cases o <;> simp
 
@@ -127,25 +127,28 @@ theorem mem_attach : ∀ (o : Option α) (x : {x // o = some x}), x ∈ o.attach
     o.attachWith p H = some x ↔ o = some x.val := by
   cases o <;> cases x <;> simp
 
-@[simp] theorem get_attach {o : Option α} (h : o.attach.isSome = true) :
+@[simp, grind =] theorem get_attach {o : Option α} (h : o.attach.isSome = true) :
     o.attach.get h = ⟨o.get (by simpa using h), by simp⟩ :=
   Subsingleton.elim _ _
 
-@[simp] theorem getD_attach {o : Option α} {fallback} :
+@[simp, grind =] theorem getD_attach {o : Option α} {fallback} :
     o.attach.getD fallback = fallback :=
   Subsingleton.elim _ _
 
-@[simp] theorem get!_attach {o : Option α} [Inhabited { x // o = some x }] :
+@[simp, grind =] theorem get!_attach {o : Option α} [Inhabited { x // o = some x }] :
     o.attach.get! = default :=
   Subsingleton.elim _ _
 
-@[simp] theorem get_attachWith {p : α → Prop} {o : Option α} (H : ∀ a, o = some a → p a) (h : (o.attachWith p H).isSome) :
+@[simp, grind =] theorem get_attachWith {p : α → Prop} {o : Option α} (H : ∀ a, o = some a → p a) (h : (o.attachWith p H).isSome) :
     (o.attachWith p H).get h = ⟨o.get (by simpa using h), H _ (by simp)⟩ := by
   cases o <;> simp
 
-@[simp] theorem getD_attachWith {p : α → Prop} {o : Option α} {h} {fallback} :
+@[simp, grind =] theorem getD_attachWith {p : α → Prop} {o : Option α} {h} {fallback} :
     (o.attachWith p h).getD fallback =
-      ⟨o.getD fallback.1, by cases o <;> (try exact fallback.2) <;> exact h _ (by simp)⟩ := by
+      ⟨o.getD fallback.val, by
+        cases o
+        · exact fallback.property
+        · exact h _ (by simp)⟩ := by
   cases o <;> simp
 
 theorem toList_attach (o : Option α) :
@@ -168,23 +171,23 @@ theorem toArray_attachWith {p : α → Prop} {o : Option α} {h} :
     o.toList.attach = (o.attach.map fun ⟨a, h⟩ => ⟨a, by simpa using h⟩).toList := by
   cases o <;> simp [toList]
 
-theorem attach_map {o : Option α} (f : α → β) :
+@[grind =] theorem attach_map {o : Option α} (f : α → β) :
     (o.map f).attach = o.attach.map (fun ⟨x, h⟩ => ⟨f x, map_eq_some_iff.2 ⟨_, h, rfl⟩⟩) := by
   cases o <;> simp
 
-theorem attachWith_map {o : Option α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), o.map f = some b → P b} :
+@[grind =] theorem attachWith_map {o : Option α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), o.map f = some b → P b} :
     (o.map f).attachWith P H = (o.attachWith (P ∘ f) (fun _ h => H _ (map_eq_some_iff.2 ⟨_, h, rfl⟩))).map
       fun ⟨x, h⟩ => ⟨f x, h⟩ := by
   cases o <;> simp
 
-theorem map_attach_eq_pmap {o : Option α} (f : { x // o = some x } → β) :
+@[grind =] theorem map_attach_eq_pmap {o : Option α} (f : { x // o = some x } → β) :
     o.attach.map f = o.pmap (fun a (h : o = some a) => f ⟨a, h⟩) (fun _ h => h) := by
   cases o <;> simp
 
 @[deprecated map_attach_eq_pmap (since := "2025-02-09")]
 abbrev map_attach := @map_attach_eq_pmap
 
-@[simp] theorem map_attachWith {l : Option α} {P : α → Prop} {H : ∀ (a : α), l = some a → P a}
+@[simp, grind =] theorem map_attachWith {l : Option α} {P : α → Prop} {H : ∀ (a : α), l = some a → P a}
     (f : { x // P x } → β) :
     (l.attachWith P H).map f = l.attach.map fun ⟨x, h⟩ => f ⟨x, H _ h⟩ := by
   cases l <;> simp_all
@@ -200,12 +203,12 @@ theorem map_attach_eq_attachWith {o : Option α} {p : α → Prop} (f : ∀ a, o
     o.attach.map (fun x => ⟨x.1, f x.1 x.2⟩) = o.attachWith p f := by
   cases o <;> simp_all [Function.comp_def]
 
-theorem attach_bind {o : Option α} {f : α → Option β} :
+@[grind =] theorem attach_bind {o : Option α} {f : α → Option β} :
     (o.bind f).attach =
       o.attach.bind fun ⟨x, h⟩ => (f x).attach.map fun ⟨y, h'⟩ => ⟨y, bind_eq_some_iff.2 ⟨_, h, h'⟩⟩ := by
   cases o <;> simp
 
-theorem bind_attach {o : Option α} {f : {x // o = some x} → Option β} :
+@[grind =] theorem bind_attach {o : Option α} {f : {x // o = some x} → Option β} :
     o.attach.bind f = o.pbind fun a h => f ⟨a, h⟩ := by
   cases o <;> simp
 
@@ -213,7 +216,7 @@ theorem pbind_eq_bind_attach {o : Option α} {f : (a : α) → o = some a → Op
     o.pbind f = o.attach.bind fun ⟨x, h⟩ => f x h := by
   cases o <;> simp
 
-theorem attach_filter {o : Option α} {p : α → Bool} :
+@[grind =] theorem attach_filter {o : Option α} {p : α → Bool} :
     (o.filter p).attach =
       o.attach.bind fun ⟨x, h⟩ => if h' : p x then some ⟨x, by simp_all⟩ else none := by
   cases o with
@@ -229,12 +232,12 @@ theorem attach_filter {o : Option α} {p : α → Bool} :
     · rintro ⟨h, rfl⟩
       simp [h]
 
-theorem filter_attachWith {P : α → Prop} {o : Option α} {h : ∀ x, o = some x → P x} {q : α → Bool} :
+@[grind =] theorem filter_attachWith {P : α → Prop} {o : Option α} {h : ∀ x, o = some x → P x} {q : α → Bool} :
     (o.attachWith P h).filter q =
       (o.filter q).attachWith P (fun _ h' => h _ (eq_some_of_filter_eq_some h')) := by
   cases o <;> simp [filter_some] <;> split <;> simp
 
-theorem filter_attach {o : Option α} {p : {x // o = some x} → Bool} :
+@[grind =] theorem filter_attach {o : Option α} {p : {x // o = some x} → Bool} :
     o.attach.filter p = o.pbind fun a h => if p ⟨a, h⟩ then some ⟨a, h⟩ else none := by
   cases o <;> simp [filter_some]
 
@@ -278,7 +281,7 @@ theorem toArray_pmap {p : α → Prop} {o : Option α} {f : (a : α) → p a →
     (o.pmap f h).toArray = o.attach.toArray.map (fun x => f x.1 (h _ x.2)) := by
   cases o <;> simp
 
-theorem attach_pfilter {o : Option α} {p : (a : α) → o = some a → Bool} :
+@[grind =] theorem attach_pfilter {o : Option α} {p : (a : α) → o = some a → Bool} :
     (o.pfilter p).attach =
       o.attach.pbind fun x h => if h' : p x (by simp_all) then
         some ⟨x.1, by simpa [pfilter_eq_some_iff] using ⟨_, h'⟩⟩ else none := by

src/Init/Data/Option/Lemmas.lean

@@ -14,7 +14,7 @@ import Init.Ext
 
 namespace Option
 
-theorem default_eq_none : (default : Option α) = none := rfl
+@[grind =] theorem default_eq_none : (default : Option α) = none := rfl
 
 @[deprecated mem_def (since := "2025-04-07")]
 theorem mem_iff {a : α} {b : Option α} : a ∈ b ↔ b = some a := .rfl
@@ -254,11 +254,11 @@ theorem isSome_apply_of_isSome_bind {α β : Type _} {x : Option α} {f : α →
       (isSome_apply_of_isSome_bind h) := by
   cases x <;> trivial
 
-theorem any_bind {p : β → Bool} {f : α → Option β} {o : Option α} :
+@[grind =] theorem any_bind {p : β → Bool} {f : α → Option β} {o : Option α} :
     (o.bind f).any p = o.any (Option.any p ∘ f) := by
   cases o <;> simp
 
-theorem all_bind {p : β → Bool} {f : α → Option β} {o : Option α} :
+@[grind =] theorem all_bind {p : β → Bool} {f : α → Option β} {o : Option α} :
     (o.bind f).all p = o.all (Option.all p ∘ f) := by
   cases o <;> simp
 
@@ -431,7 +431,7 @@ theorem filter_eq_bind (x : Option α) (p : α → Bool) :
     x.filter p = x.bind (Option.guard p) :=
   (bind_guard x p).symm
 
-@[simp] theorem any_filter : (o : Option α) →
+@[simp, grind =] theorem any_filter : (o : Option α) →
     (Option.filter p o).any q = Option.any (fun a => p a && q a) o
   | none => rfl
   | some a =>
@@ -439,7 +439,7 @@ theorem filter_eq_bind (x : Option α) (p : α → Bool) :
     | false => by simp [filter_some_neg h, h]
     | true => by simp [filter_some_pos h, h]
 
-@[simp] theorem all_filter : (o : Option α) →
+@[simp, grind =] theorem all_filter : (o : Option α) →
     (Option.filter p o).all q = Option.all (fun a => !p a || q a) o
   | none => rfl
   | some a =>
@@ -447,7 +447,7 @@ theorem filter_eq_bind (x : Option α) (p : α → Bool) :
     | false => by simp [filter_some_neg h, h]
     | true => by simp [filter_some_pos h, h]
 
-@[simp] theorem isNone_filter :
+@[simp, grind =] theorem isNone_filter :
     Option.isNone (Option.filter p o) = Option.all (fun a => !p a) o :=
   match o with
   | none => rfl
@@ -468,7 +468,7 @@ theorem filter_eq_bind (x : Option α) (p : α → Bool) :
     Option.filter q (Option.filter p o) = Option.filter (fun x => p x && q x) o := by
   cases o <;> repeat (simp_all [filter_some]; try split)
 
-theorem filter_bind {f : α → Option β} :
+@[grind =] theorem filter_bind {f : α → Option β} :
     (Option.bind x f).filter p = (x.filter (fun a => (f a).any p)).bind f := by
   cases x with
   | none => simp
@@ -483,16 +483,16 @@ theorem filter_bind {f : α → Option β} :
 theorem eq_some_of_filter_eq_some {o : Option α} {a : α} (h : o.filter p = some a) : o = some a :=
   filter_eq_some_iff.1 h |>.1
 
-theorem filter_map {f : α → β} {p : β → Bool} :
+@[grind =] theorem filter_map {f : α → β} {p : β → Bool} :
     (Option.map f x).filter p = (x.filter (p ∘ f)).map f := by
   cases x <;> simp [filter_some]
 
-@[simp, grind] theorem all_guard (a : α) :
+@[simp] theorem all_guard (a : α) :
     Option.all q (guard p a) = (!p a || q a) := by
   simp only [guard]
   split <;> simp_all
 
-@[simp, grind] theorem any_guard (a : α) : Option.any q (guard p a) = (p a && q a) := by
+@[simp] theorem any_guard (a : α) : Option.any q (guard p a) = (p a && q a) := by
   simp only [guard]
   split <;> simp_all
 
@@ -563,21 +563,21 @@ theorem bind_map_comm {α β} {x : Option (Option α)} {f : α → β} :
 theorem mem_of_mem_join {a : α} {x : Option (Option α)} (h : a ∈ x.join) : some a ∈ x :=
   h.symm ▸ join_eq_some_iff.1 h
 
-theorem any_join {p : α → Bool} {x : Option (Option α)} :
+@[grind _=_] theorem any_join {p : α → Bool} {x : Option (Option α)} :
     x.join.any p = x.any (Option.any p) := by
   cases x <;> simp
 
-theorem all_join {p : α → Bool} {x : Option (Option α)} :
+@[grind _=_] theorem all_join {p : α → Bool} {x : Option (Option α)} :
     x.join.all p = x.all (Option.all p) := by
   cases x <;> simp
 
-theorem isNone_join {x : Option (Option α)} : x.join.isNone = x.all Option.isNone := by
+@[grind =] theorem isNone_join {x : Option (Option α)} : x.join.isNone = x.all Option.isNone := by
   cases x <;> simp
 
-theorem isSome_join {x : Option (Option α)} : x.join.isSome = x.any Option.isSome := by
+@[grind =]theorem isSome_join {x : Option (Option α)} : x.join.isSome = x.any Option.isSome := by
   cases x <;> simp
 
-theorem get_join {x : Option (Option α)} {h} : x.join.get h =
+@[grind =] theorem get_join {x : Option (Option α)} {h} : x.join.get h =
     (x.get (Option.isSome_of_any (Option.isSome_join ▸ h))).get (get_of_any_eq_true _ _ (Option.isSome_join ▸ h)) := by
   cases x with
   | none => simp at h
@@ -588,11 +588,11 @@ theorem join_eq_get {x : Option (Option α)} {h} : x.join = x.get h := by
   | none => simp at h
   | some _ => simp
 
-theorem getD_join {x : Option (Option α)} {default : α} :
+@[grind =] theorem getD_join {x : Option (Option α)} {default : α} :
     x.join.getD default = (x.getD (some default)).getD default := by
   cases x <;> simp
 
-theorem get!_join [Inhabited α] {x : Option (Option α)} :
+@[grind =] theorem get!_join [Inhabited α] {x : Option (Option α)} :
     x.join.get! = x.get!.get! := by
   cases x <;> simp [default_eq_none]
 
@@ -602,13 +602,13 @@ theorem get!_join [Inhabited α] {x : Option (Option α)} :
 @[deprecated guard_eq_some_iff (since := "2025-04-10")]
 abbrev guard_eq_some := @guard_eq_some_iff
 
-@[simp] theorem isSome_guard : (Option.guard p a).isSome = p a :=
+@[simp, grind =] theorem isSome_guard : (Option.guard p a).isSome = p a :=
   if h : p a then by simp [Option.guard, h] else by simp [Option.guard, h]
 
 @[deprecated isSome_guard (since := "2025-03-18")]
 abbrev guard_isSome := @isSome_guard
 
-@[simp] theorem isNone_guard : (Option.guard p a).isNone = !p a := by
+@[simp, grind =] theorem isNone_guard : (Option.guard p a).isNone = !p a := by
   rw [← not_isSome, isSome_guard]
 
 @[simp] theorem guard_eq_none_iff : Option.guard p a = none ↔ p a = false :=
@@ -643,7 +643,7 @@ theorem get_none (a : α) {h} : none.get h = a := by
 theorem get_none_eq_iff_true {h} : (none : Option α).get h = a ↔ True := by
   simp at h
 
-theorem get_guard : (guard p a).get h = a := by
+@[simp, grind =] theorem get_guard : (guard p a).get h = a := by
   simp only [guard]
   split <;> simp
 
@@ -672,7 +672,7 @@ theorem map_guard {p : α → Bool} {f : α → β} {x : α} :
     (Option.guard p x).map f = if p x then some (f x) else none := by
   simp [guard_eq_ite]
 
-theorem join_filter {p : Option α → Bool} : {o : Option (Option α)} →
+@[grind =] theorem join_filter {p : Option α → Bool} : {o : Option (Option α)} →
     (o.filter p).join = o.join.filter (fun a => p (some a))
   | none => by simp
   | some none => by
@@ -682,7 +682,7 @@ theorem join_filter {p : Option α → Bool} : {o : Option (Option α)} →
     simp only [join_some, filter_some]
     split <;> simp
 
-theorem filter_join {p : α → Bool} : {o : Option (Option α)} →
+@[grind =] theorem filter_join {p : α → Bool} : {o : Option (Option α)} →
     o.join.filter p = (o.filter (Option.any p)).join
   | none => by simp
   | some none => by
@@ -754,22 +754,22 @@ theorem merge_eq_some_iff {o o' : Option α} {f : α → α → α} {a : α} :
 theorem merge_eq_none_iff {o o' : Option α} : o.merge f o' = none ↔ o = none ∧ o' = none := by
   cases o <;> cases o' <;> simp
 
-@[simp]
+@[simp, grind =]
 theorem any_merge {p : α → Bool} {f : α → α → α} (hpf : ∀ a b, p (f a b) = (p a || p b))
     {o o' : Option α} : (o.merge f o').any p = (o.any p || o'.any p) := by
   cases o <;> cases o' <;> simp [*]
 
-@[simp]
+@[simp, grind =]
 theorem all_merge {p : α → Bool} {f : α → α → α} (hpf : ∀ a b, p (f a b) = (p a && p b))
     {o o' : Option α} : (o.merge f o').all p = (o.all p && o'.all p) := by
   cases o <;> cases o' <;> simp [*]
 
-@[simp]
+@[simp, grind =]
 theorem isSome_merge {o o' : Option α} {f : α → α → α} :
     (o.merge f o').isSome = (o.isSome || o'.isSome) := by
   simp [← any_true]
 
-@[simp]
+@[simp, grind =]
 theorem isNone_merge {o o' : Option α} {f : α → α → α} :
     (o.merge f o').isNone = (o.isNone && o'.isNone) := by
   simp [← all_false]
@@ -783,7 +783,7 @@ theorem get_merge {o o' : Option α} {f : α → α → α} {i : α} [Std.Lawful
 
 @[simp, grind] theorem elim_some (x : β) (f : α → β) (a : α) : (some a).elim x f = f a := rfl
 
-theorem elim_filter {o : Option α} {b : β} :
+@[grind =] theorem elim_filter {o : Option α} {b : β} :
     Option.elim (Option.filter p o) b f = Option.elim o b (fun a => if p a then f a else b) :=
   match o with
   | none => rfl
@@ -792,7 +792,7 @@ theorem elim_filter {o : Option α} {b : β} :
     | false => by simp [filter_some_neg h, h]
     | true => by simp [filter_some_pos, h]
 
-theorem elim_join {o : Option (Option α)} {b : β} {f : α → β} :
+@[grind =] theorem elim_join {o : Option (Option α)} {b : β} {f : α → β} :
     o.join.elim b f = o.elim b (·.elim b f) := by
   cases o <;> simp
 
@@ -830,9 +830,16 @@ theorem choice_eq_default [Subsingleton α] [Inhabited α] : choice α = some de
 theorem choice_eq_none_iff_not_nonempty : choice α = none ↔ ¬Nonempty α := by
   simp [choice]
 
+theorem isNone_choice_iff_not_nonempty : (choice α).isNone ↔ ¬Nonempty α := by
+  rw [isNone_iff_eq_none, choice_eq_none_iff_not_nonempty]
+
+grind_pattern isNone_choice_iff_not_nonempty => (choice α).isNone
+
 theorem isSome_choice_iff_nonempty : (choice α).isSome ↔ Nonempty α :=
   ⟨fun h => ⟨(choice α).get h⟩, fun h => by simp only [choice, dif_pos h, isSome_some]⟩
 
+grind_pattern isSome_choice_iff_nonempty => (choice α).isSome
+
 @[simp]
 theorem isSome_choice [Nonempty α] : (choice α).isSome :=
   isSome_choice_iff_nonempty.2 inferInstance
@@ -840,19 +847,16 @@ theorem isSome_choice [Nonempty α] : (choice α).isSome :=
 @[deprecated isSome_choice_iff_nonempty (since := "2025-03-18")]
 abbrev choice_isSome_iff_nonempty := @isSome_choice_iff_nonempty
 
-theorem isNone_choice_iff_not_nonempty : (choice α).isNone ↔ ¬Nonempty α := by
-  rw [isNone_iff_eq_none, choice_eq_none_iff_not_nonempty]
-
 @[simp]
 theorem isNone_choice_eq_false [Nonempty α] : (choice α).isNone = false := by
   simp [← not_isSome]
 
-@[simp]
+@[simp, grind =]
 theorem getD_choice {a} :
     (choice α).getD a = (choice α).get (isSome_choice_iff_nonempty.2 ⟨a⟩) := by
   rw [get_eq_getD]
 
-@[simp]
+@[simp, grind =]
 theorem get!_choice [Inhabited α] : (choice α).get! = (choice α).get isSome_choice := by
   rw [get_eq_get!]
 
@@ -933,16 +937,16 @@ theorem or_of_isNone {o o' : Option α} (h : o.isNone) : o.or o' = o' := by
   match o, h with
   | none, _ => simp
 
-@[simp, grind]
+@[simp, grind =]
 theorem getD_or {o o' : Option α} {fallback : α} :
     (o.or o').getD fallback = o.getD (o'.getD fallback) := by
   cases o <;> simp
 
-@[simp]
+@[simp, grind =]
 theorem get!_or {o o' : Option α} [Inhabited α] : (o.or o').get! = o.getD o'.get! := by
   cases o <;> simp
 
-@[simp] theorem filter_or_filter {o o' : Option α} {f : α → Bool} :
+@[simp, grind =] theorem filter_or_filter {o o' : Option α} {f : α → Bool} :
     (o.or (o'.filter f)).filter f = (o.or o').filter f := by
   cases o <;> cases o' <;> simp
 
@@ -1026,16 +1030,16 @@ variable [BEq α]
 
 @[simp] theorem beq_none {o : Option α} : (o == none) = o.isNone := by cases o <;> simp
 
-@[simp]
-theorem filter_beq_self [ReflBEq α] {p : α → Bool} {o : Option α} : (o.filter p == o) = (o.all p) := by
+@[simp, grind =]
+theorem filter_beq_self [ReflBEq α] {p : α → Bool} {o : Option α} : (o.filter p == o) = o.all p := by
   cases o with
   | none => simp
   | some _ =>
     simp only [filter_some]
     split <;> simp [*]
 
-@[simp]
-theorem self_beq_filter [ReflBEq α] {p : α → Bool} {o : Option α} : (o == o.filter p) = (o.all p) := by
+@[simp, grind =]
+theorem self_beq_filter [ReflBEq α] {p : α → Bool} {o : Option α} : (o == o.filter p) = o.all p := by
   cases o with
   | none => simp
   | some _ =>
@@ -1204,7 +1208,7 @@ theorem pbind_eq_some_iff {o : Option α} {f : (a : α) → o = some a → Optio
     o.pbind f = some b ↔ ∃ a h, f a h = some b := by
   cases o <;> simp
 
-theorem pbind_join {o : Option (Option α)} {f : (a : α) → o.join = some a → Option β} :
+@[grind =] theorem pbind_join {o : Option (Option α)} {f : (a : α) → o.join = some a → Option β} :
     o.join.pbind f = o.pbind (fun o' ho' => o'.pbind (fun a ha => f a (by simp_all))) := by
   cases o <;> simp <;> congr
 
@@ -1218,7 +1222,7 @@ theorem isSome_get_of_isSome_pbind {o : Option α} {f : (a : α) → o = some a
   | none => simp at h
   | some a => simp [← h]
 
-@[simp]
+@[simp, grind =]
 theorem get_pbind {o : Option α} {f : (a : α) → o = some a → Option β} {h} :
     (o.pbind f).get h = (f (o.get (isSome_of_isSome_pbind h)) (by simp)).get (isSome_get_of_isSome_pbind h) := by
   cases o <;> simp
@@ -1256,7 +1260,7 @@ theorem get_pbind {o : Option α} {f : (a : α) → o = some a → Option β} {h
     · rintro ⟨h, rfl⟩
       rfl
 
-@[simp, grind]
+@[simp]
 theorem pmap_eq_map (p : α → Prop) (f : α → β) (o : Option α) (H) :
     @pmap _ _ p (fun a _ => f a) o H = Option.map f o := by
   cases o <;> simp
@@ -1305,7 +1309,7 @@ theorem pmap_guard {q : α → Bool} {p : α → Prop} (f : (x : α) → p x →
   simp only [guard_eq_ite]
   split <;> simp_all
 
-@[simp]
+@[simp, grind =]
 theorem get_pmap {p : α → Bool} {f : (x : α) → p x → β} {o : Option α}
     {h : ∀ a, o = some a → p a} {h'} :
     (o.pmap f h).get h' = f (o.get (by simpa using h')) (h _ (by simp)) := by
@@ -1316,7 +1320,7 @@ theorem get_pmap {p : α → Bool} {f : (x : α) → p x → β} {o : Option α}
 @[simp, grind] theorem pelim_none : pelim none b f = b := rfl
 @[simp, grind] theorem pelim_some : pelim (some a) b f = f a rfl := rfl
 
-@[simp, grind] theorem pelim_eq_elim : pelim o b (fun a _ => f a) = o.elim b f := by
+@[simp] theorem pelim_eq_elim : pelim o b (fun a _ => f a) = o.elim b f := by
   cases o <;> simp
 
 @[simp, grind] theorem elim_pmap {p : α → Prop} (f : (a : α) → p a → β) (o : Option α)
@@ -1329,7 +1333,7 @@ theorem pelim_congr_left {o o' : Option α } {b : β} {f : (a : α) → (a ∈ o
     pelim o b f = pelim o' b (fun a ha => f a (h ▸ ha)) := by
   cases h; rfl
 
-theorem pelim_filter {o : Option α} {b : β} {f : (a : α) → a ∈ o.filter p → β} :
+@[grind =] theorem pelim_filter {o : Option α} {b : β} {f : (a : α) → a ∈ o.filter p → β} :
     Option.pelim (Option.filter p o) b f =
       Option.pelim o b (fun a h => if hp : p a then f a (Option.mem_filter_iff.2 ⟨h, hp⟩) else b) :=
   match o with
@@ -1339,7 +1343,7 @@ theorem pelim_filter {o : Option α} {b : β} {f : (a : α) → a ∈ o.filter p
     | false => by simp [pelim_congr_left (filter_some_neg h), h]
     | true => by simp [pelim_congr_left (filter_some_pos h), h]
 
-theorem pelim_join {o : Option (Option α)} {b : β} {f : (a : α) → a ∈ o.join → β} :
+@[grind =] theorem pelim_join {o : Option (Option α)} {b : β} {f : (a : α) → a ∈ o.join → β} :
     o.join.pelim b f = o.pelim b (fun o' ho' => o'.pelim b (fun a ha => f a (by simp_all))) := by
   cases o <;> simp <;> congr
 
@@ -1417,7 +1421,7 @@ theorem eq_some_of_pfilter_eq_some {o : Option α} {p : (a : α) → o = some a
     {a : α} (h : o.pfilter p = some a) : o = some a :=
   pfilter_eq_some_iff.1 h |>.1
 
-theorem filter_pbind {f : (a : α) → o = some a → Option β} :
+@[grind =] theorem filter_pbind {f : (a : α) → o = some a → Option β} :
     (Option.pbind o f).filter p =
       (o.pfilter (fun a h => (f a h).any p)).pbind (fun a h => f a (eq_some_of_pfilter_eq_some h)) := by
   cases o with
@@ -1429,7 +1433,7 @@ theorem filter_pbind {f : (a : α) → o = some a → Option β} :
     · simp only [h, filter_some, any_some]
       split <;> simp [h]
 
-@[simp, grind] theorem pfilter_eq_filter {α : Type _} {o : Option α} {p : α → Bool} :
+@[simp] theorem pfilter_eq_filter {α : Type _} {o : Option α} {p : α → Bool} :
     o.pfilter (fun a _ => p a) = o.filter p := by
   cases o with
   | none => rfl
@@ -1468,7 +1472,7 @@ theorem pfilter_eq_pbind_ite {α : Type _} {o : Option α}
   · rfl
   · simp only [Option.pfilter, Bool.cond_eq_ite, Option.pbind_some]
 
-theorem filter_pmap {p : α → Prop} {f : (a : α) → p a → β} {h : ∀ (a : α), o = some a → p a}
+@[grind =] theorem filter_pmap {p : α → Prop} {f : (a : α) → p a → β} {h : ∀ (a : α), o = some a → p a}
     {q : β → Bool} : (o.pmap f h).filter q = (o.pfilter (fun a h' => q (f a (h _ h')))).pmap f
       (fun _ h' => h _ (eq_some_of_pfilter_eq_some h')) := by
   cases o with
@@ -1477,7 +1481,7 @@ theorem filter_pmap {p : α → Prop} {f : (a : α) → p a → β} {h : ∀ (a
     simp only [pmap_some, filter_some, pfilter_some]
     split <;> simp
 
-theorem pfilter_join {o : Option (Option α)} {p : (a : α) → o.join = some a → Bool} :
+@[grind =] theorem pfilter_join {o : Option (Option α)} {p : (a : α) → o.join = some a → Bool} :
     o.join.pfilter p = (o.pfilter (fun o' h => o'.pelim false (fun a ha => p a (by simp_all)))).join := by
   cases o with
   | none => simp
@@ -1488,11 +1492,11 @@ theorem pfilter_join {o : Option (Option α)} {p : (a : α) → o.join = some a
       simp only [join_some, pfilter_some, pelim_some]
       split <;> simp
 
-theorem join_pfilter {o : Option (Option α)} {p : (o' : Option α) → o = some o' → Bool} :
+@[grind =] theorem join_pfilter {o : Option (Option α)} {p : (o' : Option α) → o = some o' → Bool} :
     (o.pfilter p).join = o.pbind (fun o' ho' => if p o' ho' then o' else none) := by
   cases o <;> simp <;> split <;> simp
 
-theorem elim_pfilter {o : Option α} {b : β} {f : α → β} {p : (a : α) → o = some a → Bool} :
+@[grind =] theorem elim_pfilter {o : Option α} {b : β} {f : α → β} {p : (a : α) → o = some a → Bool} :
     (o.pfilter p).elim b f = o.pelim b (fun a ha => if p a ha then f a else b) := by
   cases o with
   | none => simp
@@ -1500,7 +1504,7 @@ theorem elim_pfilter {o : Option α} {b : β} {f : α → β} {p : (a : α) →
     simp only [pfilter_some, pelim_some]
     split <;> simp
 
-theorem pelim_pfilter {o : Option α} {b : β} {p : (a : α) → o = some a → Bool}
+@[grind =] theorem pelim_pfilter {o : Option α} {b : β} {p : (a : α) → o = some a → Bool}
     {f : (a : α) → o.pfilter p = some a → β} :
     (o.pfilter p).pelim b f = o.pelim b
       (fun a ha => if hp : p a ha then f a (pfilter_eq_some_iff.2 ⟨_, hp⟩) else b) := by
@@ -1789,19 +1793,19 @@ theorem min_pfilter_right [Min α] [Std.IdempotentOp (α := α) min] {o : Option
     simp only [pfilter_some]
     split <;> simp [Std.IdempotentOp.idempotent]
 
-@[simp]
+@[simp, grind =]
 theorem isSome_max [Max α] {o o' : Option α} : (max o o').isSome = (o.isSome || o'.isSome) := by
   cases o <;> cases o' <;> simp
 
-@[simp]
+@[simp, grind =]
 theorem isNone_max [Max α] {o o' : Option α} : (max o o').isNone = (o.isNone && o'.isNone) := by
   cases o <;> cases o' <;> simp
 
-@[simp]
+@[simp, grind =]
 theorem isSome_min [Min α] {o o' : Option α} : (min o o').isSome = (o.isSome && o'.isSome) := by
   cases o <;> cases o' <;> simp
 
-@[simp]
+@[simp, grind =]
 theorem isNone_min [Min α] {o o' : Option α} : (min o o').isNone = (o.isNone || o'.isNone) := by
   cases o <;> cases o' <;> simp
 
@@ -1813,7 +1817,7 @@ theorem max_join_right [Max α] {o : Option α} {o' : Option (Option α)} :
     max o o'.join = (max (some o) o').get (by simp) := by
   cases o' <;> simp
 
-theorem join_max [Max α] {o o' : Option (Option α)} :
+@[grind _=_] theorem join_max [Max α] {o o' : Option (Option α)} :
     (max o o').join = max o.join o'.join := by
   cases o <;> cases o' <;> simp
 
@@ -1825,7 +1829,7 @@ theorem min_join_right [Min α] {o : Option α} {o' : Option (Option α)} :
     min o o'.join = (min (some o) o').join := by
   cases o' <;> simp
 
-theorem join_min [Min α] {o o' : Option (Option α)} :
+@[grind _=_] theorem join_min [Min α] {o o' : Option (Option α)} :
     (min o o').join = min o.join o'.join := by
   cases o <;> cases o' <;> simp
 
@@ -1873,12 +1877,12 @@ theorem min_eq_none_iff [Min α] {o o' : Option α} :
     min o o' = none ↔ o = none ∨ o' = none := by
   cases o <;> cases o' <;> simp
 
-@[simp]
+@[simp, grind =]
 theorem any_max [Max α] {o o' : Option α} {p : α → Bool} (hp : ∀ a b, p (max a b) = (p a || p b)) :
     (max o o').any p = (o.any p || o'.any p) := by
   cases o <;> cases o' <;> simp [hp]
 
-@[simp]
+@[simp, grind =]
 theorem all_min [Min α] {o o' : Option α} {p : α → Bool} (hp : ∀ a b, p (min a b) = (p a || p b)) :
     (min o o').all p = (o.all p || o'.all p) := by
   cases o <;> cases o' <;> simp [hp]
@@ -1889,7 +1893,7 @@ theorem isSome_left_of_isSome_min [Min α] {o o' : Option α} : (min o o').isSom
 theorem isSome_right_of_isSome_min [Min α] {o o' : Option α} : (min o o').isSome → o'.isSome := by
   cases o' <;> simp
 
-@[simp]
+@[simp, grind =]
 theorem get_min [Min α] {o o' : Option α} {h} :
     (min o o').get h = min (o.get (isSome_left_of_isSome_min h)) (o'.get (isSome_right_of_isSome_min h)) := by
   cases o <;> cases o' <;> simp

src/Init/Data/Option/List.lean

@@ -73,7 +73,8 @@ theorem toList_min [Min α] {o o' : Option α} :
 theorem length_toList_le {o : Option α} : o.toList.length ≤ 1 := by
   cases o <;> simp
 
-theorem length_toList_eq_ite {o : Option α} :
+@[grind =]
+theorem length_toList {o : Option α} :
     o.toList.length = if o.isSome then 1 else 0 := by
   cases o <;> simp
 

src/Init/Data/Option/Monadic.lean

@@ -90,11 +90,18 @@ theorem forIn'_eq_pelim [Monad m] [LawfulMonad m]
       pure (f := m) (o.pelim b (fun a h => f a h b)) := by
   cases o <;> simp
 
-@[simp] theorem forIn'_id_yield_eq_pelim
+@[simp] theorem idRun_forIn'_yield_eq_pelim
+    (o : Option α) (f : (a : α) → a ∈ o → β → Id β) (b : β) :
+    (forIn' o b (fun a m b => .yield <$> f a m b)).run =
+      o.pelim b (fun a h => f a h b |>.run) :=
+  forIn'_pure_yield_eq_pelim _ _ _
+
+@[deprecated idRun_forIn'_yield_eq_pelim (since := "2025-05-21")]
+theorem forIn'_id_yield_eq_pelim
     (o : Option α) (f : (a : α) → a ∈ o → β → β) (b : β) :
     forIn' (m := Id) o b (fun a m b => .yield (f a m b)) =
-      o.pelim b (fun a h => f a h b) := by
-  cases o <;> simp
+      o.pelim b (fun a h => f a h b) :=
+  forIn'_pure_yield_eq_pelim _ _ _
 
 @[simp, grind] theorem forIn'_map [Monad m] [LawfulMonad m]
     (o : Option α) (g : α → β) (f : (b : β) → b ∈ o.map g → γ → m (ForInStep γ)) :
@@ -126,11 +133,18 @@ theorem forIn_eq_elim [Monad m] [LawfulMonad m]
       pure (f := m) (o.elim b (fun a => f a b)) := by
   cases o <;> simp
 
-@[simp] theorem forIn_id_yield_eq_elim
+@[simp] theorem idRun_forIn_yield_eq_elim
+    (o : Option α) (f : (a : α) → β → Id β) (b : β) :
+    (forIn o b (fun a b => .yield <$> f a b)).run =
+      o.elim b (fun a => f a b |>.run) :=
+  forIn_pure_yield_eq_elim _ _ _
+
+@[deprecated idRun_forIn_yield_eq_elim (since := "2025-05-21")]
+theorem forIn_id_yield_eq_elim
     (o : Option α) (f : (a : α) → β → β) (b : β) :
     forIn (m := Id) o b (fun a b => .yield (f a b)) =
-      o.elim b (fun a => f a b) := by
-  cases o <;> simp
+      o.elim b (fun a => f a b) :=
+  forIn_pure_yield_eq_elim _ _ _
 
 @[simp, grind] theorem forIn_map [Monad m] [LawfulMonad m]
     (o : Option α) (g : α → β) (f : β → γ → m (ForInStep γ)) :
@@ -142,26 +156,26 @@ theorem forIn_join [Monad m] [LawfulMonad m]
     forIn o.join init f = forIn o init (fun o' b => ForInStep.yield <$> forIn o' b f) := by
   cases o <;> simp
 
-@[simp] theorem elimM_pure [Monad m] [LawfulMonad m] (x : Option α) (y : m β) (z : α → m β) :
+@[simp, grind =] theorem elimM_pure [Monad m] [LawfulMonad m] (x : Option α) (y : m β) (z : α → m β) :
     Option.elimM (pure x : m (Option α)) y z = x.elim y z := by
   simp [Option.elimM]
 
-@[simp] theorem elimM_bind [Monad m] [LawfulMonad m] (x : m α) (f : α → m (Option β))
+@[simp, grind =] theorem elimM_bind [Monad m] [LawfulMonad m] (x : m α) (f : α → m (Option β))
     (y : m γ) (z : β → m γ) : Option.elimM (x >>= f) y z = (do Option.elimM (f (← x)) y z) := by
   simp [Option.elimM]
 
-@[simp] theorem elimM_map [Monad m] [LawfulMonad m] (x : m α) (f : α → Option β)
+@[simp, grind =] theorem elimM_map [Monad m] [LawfulMonad m] (x : m α) (f : α → Option β)
     (y : m γ) (z : β → m γ) : Option.elimM (f <$> x) y z = (do Option.elim (f (← x)) y z) := by
   simp [Option.elimM]
 
-@[simp] theorem tryCatch_eq_or (o : Option α) (alternative : Unit → Option α) :
+@[simp, grind =] theorem tryCatch_eq_or (o : Option α) (alternative : Unit → Option α) :
     tryCatch o alternative = o.or (alternative ()) := by cases o <;> rfl
 
-@[simp] theorem throw_eq_none : throw () = (none : Option α) := rfl
+@[simp, grind =] theorem throw_eq_none : throw () = (none : Option α) := rfl
 
-@[simp, grind] theorem filterM_none [Applicative m] (p : α → m Bool) :
+@[simp, grind =] theorem filterM_none [Applicative m] (p : α → m Bool) :
     none.filterM p = pure none := rfl
-theorem filterM_some [Applicative m] (p : α → m Bool) (a : α) :
+@[grind =] theorem filterM_some [Applicative m] (p : α → m Bool) (a : α) :
     (some a).filterM p = (fun b => if b then some a else none) <$> p a := rfl
 
 theorem sequence_join [Applicative m] [LawfulApplicative m] {o : Option (Option (m α))} :

src/Init/Data/Ord.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Dany Fabian, Sebastian Ullrich
 -/
-
 module
 
 prelude
@@ -21,13 +20,13 @@ The relationship between the compared items may be:
  * `Ordering.gt`: greater than
 -/
 inductive Ordering where
-  | /-- Less than. -/
-    lt
-  | /-- Equal. -/
-    eq
-  | /-- Greater than. -/
-    gt
-deriving Inhabited, DecidableEq
+  /-- Less than. -/
+  | lt
+  /-- Equal. -/
+  | eq
+  /-- Greater than. -/
+  | gt
+deriving Inhabited, DecidableEq, Repr
 
 namespace Ordering
 
@@ -39,6 +38,7 @@ Examples:
  * `Ordering.eq.swap = Ordering.eq`
  * `Ordering.gt.swap = Ordering.lt`
 -/
+@[inline]
 def swap : Ordering → Ordering
   | .lt => .gt
   | .eq => .eq
@@ -96,6 +96,7 @@ Ordering.lt
 /--
 Checks whether the ordering is `eq`.
 -/
+@[inline]
 def isEq : Ordering → Bool
   | eq => true
   | _ => false
@@ -103,6 +104,7 @@ def isEq : Ordering → Bool
 /--
 Checks whether the ordering is not `eq`.
 -/
+@[inline]
 def isNe : Ordering → Bool
   | eq => false
   | _ => true
@@ -110,6 +112,7 @@ def isNe : Ordering → Bool
 /--
 Checks whether the ordering is `lt` or `eq`.
 -/
+@[inline]
 def isLE : Ordering → Bool
   | gt => false
   | _ => true
@@ -117,6 +120,7 @@ def isLE : Ordering → Bool
 /--
 Checks whether the ordering is `lt`.
 -/
+@[inline]
 def isLT : Ordering → Bool
   | lt => true
   | _ => false
@@ -124,6 +128,7 @@ def isLT : Ordering → Bool
 /--
 Checks whether the ordering is `gt`.
 -/
+@[inline]
 def isGT : Ordering → Bool
   | gt => true
   | _ => false
@@ -131,203 +136,158 @@ def isGT : Ordering → Bool
 /--
 Checks whether the ordering is `gt` or `eq`.
 -/
+@[inline]
 def isGE : Ordering → Bool
   | lt => false
   | _ => true
 
 section Lemmas
 
-@[simp]
-theorem isLT_lt : lt.isLT := rfl
+protected theorem «forall» {p : Ordering → Prop} : (∀ o, p o) ↔ p .lt ∧ p .eq ∧ p .gt := by
+  constructor
+  · intro h
+    exact ⟨h _, h _, h _⟩
+  · rintro ⟨h₁, h₂, h₃⟩ (_ | _ | _) <;> assumption
 
-@[simp]
-theorem isLE_lt : lt.isLE := rfl
+protected theorem «exists» {p : Ordering → Prop} : (∃ o, p o) ↔ p .lt ∨ p .eq ∨ p .gt := by
+  constructor
+  · rintro ⟨(_ | _ | _), h⟩
+    · exact .inl h
+    · exact .inr (.inl h)
+    · exact .inr (.inr h)
+  · rintro (h | h | h) <;> exact ⟨_, h⟩
 
-@[simp]
-theorem isEq_lt : lt.isEq = false := rfl
+instance [DecidablePred p] : Decidable (∀ o : Ordering, p o) :=
+  decidable_of_decidable_of_iff Ordering.«forall».symm
 
-@[simp]
-theorem isNe_lt : lt.isNe = true := rfl
+instance [DecidablePred p] : Decidable (∃ o : Ordering, p o) :=
+  decidable_of_decidable_of_iff Ordering.«exists».symm
 
-@[simp]
-theorem isGE_lt : lt.isGE = false := rfl
+@[simp] theorem isLT_lt : lt.isLT := rfl
+@[simp] theorem isLE_lt : lt.isLE := rfl
+@[simp] theorem isEq_lt : lt.isEq = false := rfl
+@[simp] theorem isNe_lt : lt.isNe = true := rfl
+@[simp] theorem isGE_lt : lt.isGE = false := rfl
+@[simp] theorem isGT_lt : lt.isGT = false := rfl
 
-@[simp]
-theorem isGT_lt : lt.isGT = false := rfl
+@[simp] theorem isLT_eq : eq.isLT = false := rfl
+@[simp] theorem isLE_eq : eq.isLE := rfl
+@[simp] theorem isEq_eq : eq.isEq := rfl
+@[simp] theorem isNe_eq : eq.isNe = false := rfl
+@[simp] theorem isGE_eq : eq.isGE := rfl
+@[simp] theorem isGT_eq : eq.isGT = false := rfl
 
-@[simp]
-theorem isLT_eq : eq.isLT = false := rfl
+@[simp] theorem isLT_gt : gt.isLT = false := rfl
+@[simp] theorem isLE_gt : gt.isLE = false := rfl
+@[simp] theorem isEq_gt : gt.isEq = false := rfl
+@[simp] theorem isNe_gt : gt.isNe = true := rfl
+@[simp] theorem isGE_gt : gt.isGE := rfl
+@[simp] theorem isGT_gt : gt.isGT := rfl
 
-@[simp]
-theorem isLE_eq : eq.isLE := rfl
+@[simp] theorem lt_beq_eq : (lt == eq) = false := rfl
+@[simp] theorem lt_beq_gt : (lt == gt) = false := rfl
+@[simp] theorem eq_beq_lt : (eq == lt) = false := rfl
+@[simp] theorem eq_beq_gt : (eq == gt) = false := rfl
+@[simp] theorem gt_beq_lt : (gt == lt) = false := rfl
+@[simp] theorem gt_beq_eq : (gt == eq) = false := rfl
 
-@[simp]
-theorem isEq_eq : eq.isEq := rfl
+@[simp] theorem swap_lt : lt.swap = .gt := rfl
+@[simp] theorem swap_eq : eq.swap = .eq := rfl
+@[simp] theorem swap_gt : gt.swap = .lt := rfl
 
-@[simp]
-theorem isNe_eq : eq.isNe = false := rfl
+theorem eq_eq_of_isLE_of_isLE_swap : ∀ {o : Ordering}, o.isLE → o.swap.isLE → o = .eq := by decide
+theorem eq_eq_of_isGE_of_isGE_swap : ∀ {o : Ordering}, o.isGE → o.swap.isGE → o = .eq := by decide
+theorem eq_eq_of_isLE_of_isGE : ∀ {o : Ordering}, o.isLE → o.isGE → o = .eq := by decide
+theorem eq_swap_iff_eq_eq : ∀ {o : Ordering}, o = o.swap ↔ o = .eq := by decide
+theorem eq_eq_of_eq_swap : ∀ {o : Ordering}, o = o.swap → o = .eq := eq_swap_iff_eq_eq.mp
 
-@[simp]
-theorem isGE_eq : eq.isGE := rfl
+@[simp] theorem isLE_eq_false : ∀ {o : Ordering}, o.isLE = false ↔ o = .gt := by decide
+@[simp] theorem isGE_eq_false : ∀ {o : Ordering}, o.isGE = false ↔ o = .lt := by decide
+@[simp] theorem isNe_eq_false : ∀ {o : Ordering}, o.isNe = false ↔ o = .eq := by decide
+@[simp] theorem isEq_eq_false : ∀ {o : Ordering}, o.isEq = false ↔ ¬o = .eq := by decide
 
-@[simp]
-theorem isGT_eq : eq.isGT = false := rfl
+@[simp] theorem swap_eq_gt : ∀ {o : Ordering}, o.swap = .gt ↔ o = .lt := by decide
+@[simp] theorem swap_eq_lt : ∀ {o : Ordering}, o.swap = .lt ↔ o = .gt := by decide
+@[simp] theorem swap_eq_eq : ∀ {o : Ordering}, o.swap = .eq ↔ o = .eq := by decide
 
-@[simp]
-theorem isLT_gt : gt.isLT = false := rfl
+@[simp] theorem isLT_swap : ∀ {o : Ordering}, o.swap.isLT = o.isGT := by decide
+@[simp] theorem isLE_swap : ∀ {o : Ordering}, o.swap.isLE = o.isGE := by decide
+@[simp] theorem isEq_swap : ∀ {o : Ordering}, o.swap.isEq = o.isEq := by decide
+@[simp] theorem isNe_swap : ∀ {o : Ordering}, o.swap.isNe = o.isNe := by decide
+@[simp] theorem isGE_swap : ∀ {o : Ordering}, o.swap.isGE = o.isLE := by decide
+@[simp] theorem isGT_swap : ∀ {o : Ordering}, o.swap.isGT = o.isLT := by decide
 
-@[simp]
-theorem isLE_gt : gt.isLE = false := rfl
+theorem isLE_of_eq_lt : ∀ {o : Ordering}, o = .lt → o.isLE := by decide
+theorem isLE_of_eq_eq : ∀ {o : Ordering}, o = .eq → o.isLE := by decide
+theorem isGE_of_eq_gt : ∀ {o : Ordering}, o = .gt → o.isGE := by decide
+theorem isGE_of_eq_eq : ∀ {o : Ordering}, o = .eq → o.isGE := by decide
 
-@[simp]
-theorem isEq_gt : gt.isEq = false := rfl
+theorem ne_eq_of_eq_lt : ∀ {o : Ordering}, o = .lt → o ≠ .eq := by decide
+theorem ne_eq_of_eq_gt : ∀ {o : Ordering}, o = .gt → o ≠ .eq := by decide
 
-@[simp]
-theorem isNe_gt : gt.isNe = true := rfl
+@[simp] theorem isLT_iff_eq_lt : ∀ {o : Ordering}, o.isLT ↔ o = .lt := by decide
+@[simp] theorem isGT_iff_eq_gt : ∀ {o : Ordering}, o.isGT ↔ o = .gt := by decide
+@[simp] theorem isEq_iff_eq_eq : ∀ {o : Ordering}, o.isEq ↔ o = .eq := by decide
+@[simp] theorem isNe_iff_ne_eq : ∀ {o : Ordering}, o.isNe ↔ ¬o = .eq := by decide
 
-@[simp]
-theorem isGE_gt : gt.isGE := rfl
+theorem isLE_iff_ne_gt : ∀ {o : Ordering}, o.isLE ↔ ¬o = .gt := by decide
+theorem isGE_iff_ne_lt : ∀ {o : Ordering}, o.isGE ↔ ¬o = .lt := by decide
+theorem isLE_iff_eq_lt_or_eq_eq : ∀ {o : Ordering}, o.isLE ↔ o = .lt ∨ o = .eq := by decide
+theorem isGE_iff_eq_gt_or_eq_eq : ∀ {o : Ordering}, o.isGE ↔ o = .gt ∨ o = .eq := by decide
 
-@[simp]
-theorem isGT_gt : gt.isGT := rfl
+theorem isLT_eq_beq_lt : ∀ {o : Ordering}, o.isLT = (o == .lt) := by decide
+theorem isLE_eq_not_beq_gt : ∀ {o : Ordering}, o.isLE = (!o == .gt) := by decide
+theorem isLE_eq_isLT_or_isEq : ∀ {o : Ordering}, o.isLE = (o.isLT || o.isEq) := by decide
+theorem isGT_eq_beq_gt : ∀ {o : Ordering}, o.isGT = (o == .gt) := by decide
+theorem isGE_eq_not_beq_lt : ∀ {o : Ordering}, o.isGE = (!o == .lt) := by decide
+theorem isGE_eq_isGT_or_isEq : ∀ {o : Ordering}, o.isGE = (o.isGT || o.isEq) := by decide
+theorem isEq_eq_beq_eq : ∀ {o : Ordering}, o.isEq = (o == .eq) := by decide
+theorem isNe_eq_not_beq_eq : ∀ {o : Ordering}, o.isNe = (!o == .eq) := by decide
+theorem isNe_eq_isLT_or_isGT : ∀ {o : Ordering}, o.isNe = (o.isLT || o.isGT) := by decide
 
-@[simp]
-theorem swap_lt : lt.swap = .gt := rfl
+@[simp] theorem not_isLT_eq_isGE : ∀ {o : Ordering}, !o.isLT = o.isGE := by decide
+@[simp] theorem not_isLE_eq_isGT : ∀ {o : Ordering}, !o.isLE = o.isGT := by decide
+@[simp] theorem not_isGT_eq_isLE : ∀ {o : Ordering}, !o.isGT = o.isLE := by decide
+@[simp] theorem not_isGE_eq_isLT : ∀ {o : Ordering}, !o.isGE = o.isLT := by decide
+@[simp] theorem not_isNe_eq_isEq : ∀ {o : Ordering}, !o.isNe = o.isEq := by decide
+theorem not_isEq_eq_isNe : ∀ {o : Ordering}, !o.isEq = o.isNe := by decide
 
-@[simp]
-theorem swap_eq : eq.swap = .eq := rfl
+theorem ne_lt_iff_isGE : ∀ {o : Ordering}, ¬o = .lt ↔ o.isGE := by decide
+theorem ne_gt_iff_isLE : ∀ {o : Ordering}, ¬o = .gt ↔ o.isLE := by decide
 
-@[simp]
-theorem swap_gt : gt.swap = .lt := rfl
+@[simp] theorem swap_swap : ∀ {o : Ordering}, o.swap.swap = o := by decide
+@[simp] theorem swap_inj : ∀ {o₁ o₂ : Ordering}, o₁.swap = o₂.swap ↔ o₁ = o₂ := by decide
 
-theorem eq_eq_of_isLE_of_isLE_swap {o : Ordering} : o.isLE → o.swap.isLE → o = .eq := by
-  cases o <;> simp
+theorem swap_then : ∀ (o₁ o₂ : Ordering), (o₁.then o₂).swap = o₁.swap.then o₂.swap := by decide
 
-theorem eq_eq_of_isGE_of_isGE_swap {o : Ordering} : o.isGE → o.swap.isGE → o = .eq := by
-  cases o <;> simp
+theorem then_eq_lt : ∀ {o₁ o₂ : Ordering}, o₁.then o₂ = lt ↔ o₁ = lt ∨ o₁ = eq ∧ o₂ = lt := by decide
+theorem then_eq_gt : ∀ {o₁ o₂ : Ordering}, o₁.then o₂ = gt ↔ o₁ = gt ∨ o₁ = eq ∧ o₂ = gt := by decide
+@[simp] theorem then_eq_eq : ∀ {o₁ o₂ : Ordering}, o₁.then o₂ = eq ↔ o₁ = eq ∧ o₂ = eq := by decide
 
-theorem eq_eq_of_isLE_of_isGE {o : Ordering} : o.isLE → o.isGE → o = .eq := by
-  cases o <;> simp
+theorem isLT_then : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isLT = (o₁.isLT || o₁.isEq && o₂.isLT) := by decide
+theorem isEq_then : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isEq = (o₁.isEq && o₂.isEq) := by decide
+theorem isNe_then : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isNe = (o₁.isNe || o₂.isNe) := by decide
+theorem isGT_then : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isGT = (o₁.isGT || o₁.isEq && o₂.isGT) := by decide
 
-theorem eq_swap_iff_eq_eq {o : Ordering} : o = o.swap ↔ o = .eq := by
-  cases o <;> simp
+@[simp] theorem lt_then {o : Ordering} : lt.then o = lt := rfl
+@[simp] theorem gt_then {o : Ordering} : gt.then o = gt := rfl
+@[simp] theorem eq_then {o : Ordering} : eq.then o = o := rfl
 
-theorem eq_eq_of_eq_swap {o : Ordering} : o = o.swap → o = .eq :=
-  eq_swap_iff_eq_eq.mp
+@[simp] theorem then_eq : ∀ {o : Ordering}, o.then eq = o := by decide
+@[simp] theorem then_self : ∀ {o : Ordering}, o.then o = o := by decide
+theorem then_assoc : ∀ (o₁ o₂ o₃ : Ordering), (o₁.then o₂).then o₃ = o₁.then (o₂.then o₃) := by decide
 
-@[simp]
-theorem isLE_eq_false {o : Ordering} : o.isLE = false ↔ o = .gt := by
-  cases o <;> simp
+theorem isLE_then_iff_or : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isLE ↔ o₁ = lt ∨ (o₁ = eq ∧ o₂.isLE) := by decide
+theorem isLE_then_iff_and : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isLE ↔ o₁.isLE ∧ (o₁ = lt ∨ o₂.isLE) := by decide
+theorem isLE_left_of_isLE_then : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isLE → o₁.isLE := by decide
+theorem isGE_left_of_isGE_then : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isGE → o₁.isGE := by decide
 
-@[simp]
-theorem isGE_eq_false {o : Ordering} : o.isGE = false ↔ o = .lt := by
-  cases o <;> simp
+instance : Std.Associative Ordering.then := ⟨then_assoc⟩
+instance : Std.IdempotentOp Ordering.then := ⟨fun _ => then_self⟩
 
-@[simp]
-theorem swap_eq_gt {o : Ordering} : o.swap = .gt ↔ o = .lt := by
-  cases o <;> simp
-
-@[simp]
-theorem swap_eq_lt {o : Ordering} : o.swap = .lt ↔ o = .gt := by
-  cases o <;> simp
-
-@[simp]
-theorem swap_eq_eq {o : Ordering} : o.swap = .eq ↔ o = .eq := by
-  cases o <;> simp
-
-@[simp]
-theorem isLT_swap {o : Ordering} : o.swap.isLT = o.isGT := by
-  cases o <;> simp
-
-@[simp]
-theorem isLE_swap {o : Ordering} : o.swap.isLE = o.isGE := by
-  cases o <;> simp
-
-@[simp]
-theorem isEq_swap {o : Ordering} : o.swap.isEq = o.isEq := by
-  cases o <;> simp
-
-@[simp]
-theorem isNe_swap {o : Ordering} : o.swap.isNe = o.isNe := by
-  cases o <;> simp
-
-@[simp]
-theorem isGE_swap {o : Ordering} : o.swap.isGE = o.isLE := by
-  cases o <;> simp
-
-@[simp]
-theorem isGT_swap {o : Ordering} : o.swap.isGT = o.isLT := by
-  cases o <;> simp
-
-theorem isLT_iff_eq_lt {o : Ordering} : o.isLT ↔ o = .lt := by
-  cases o <;> simp
-
-theorem isLE_iff_eq_lt_or_eq_eq {o : Ordering} : o.isLE ↔ o = .lt ∨ o = .eq := by
-  cases o <;> simp
-
-theorem isLE_of_eq_lt {o : Ordering} : o = .lt → o.isLE := by
-  rintro rfl; rfl
-
-theorem isLE_of_eq_eq {o : Ordering} : o = .eq → o.isLE := by
-  rintro rfl; rfl
-
-theorem isEq_iff_eq_eq {o : Ordering} : o.isEq ↔ o = .eq := by
-  cases o <;> simp
-
-theorem isNe_iff_ne_eq {o : Ordering} : o.isNe ↔ o ≠ .eq := by
-  cases o <;> simp
-
-theorem isGE_iff_eq_gt_or_eq_eq {o : Ordering} : o.isGE ↔ o = .gt ∨ o = .eq := by
-  cases o <;> simp
-
-theorem isGE_of_eq_gt {o : Ordering} : o = .gt → o.isGE := by
-  rintro rfl; rfl
-
-theorem isGE_of_eq_eq {o : Ordering} : o = .eq → o.isGE := by
-  rintro rfl; rfl
-
-theorem isGT_iff_eq_gt {o : Ordering} : o.isGT ↔ o = .gt := by
-  cases o <;> simp
-
-@[simp]
-theorem swap_swap {o : Ordering} : o.swap.swap = o := by
-  cases o <;> simp
-
-@[simp] theorem swap_inj {o₁ o₂ : Ordering} : o₁.swap = o₂.swap ↔ o₁ = o₂ :=
-  ⟨fun h => by simpa using congrArg swap h, congrArg _⟩
-
-theorem swap_then (o₁ o₂ : Ordering) : (o₁.then o₂).swap = o₁.swap.then o₂.swap := by
-  cases o₁ <;> rfl
-
-theorem then_eq_lt {o₁ o₂ : Ordering} : o₁.then o₂ = lt ↔ o₁ = lt ∨ o₁ = eq ∧ o₂ = lt := by
-  cases o₁ <;> cases o₂ <;> decide
-
-theorem then_eq_eq {o₁ o₂ : Ordering} : o₁.then o₂ = eq ↔ o₁ = eq ∧ o₂ = eq := by
-  cases o₁ <;> simp [«then»]
-
-theorem then_eq_gt {o₁ o₂ : Ordering} : o₁.then o₂ = gt ↔ o₁ = gt ∨ o₁ = eq ∧ o₂ = gt := by
-  cases o₁ <;> cases o₂ <;> decide
-
-@[simp]
-theorem lt_then {o : Ordering} : lt.then o = lt := rfl
-
-@[simp]
-theorem gt_then {o : Ordering} : gt.then o = gt := rfl
-
-@[simp]
-theorem eq_then {o : Ordering} : eq.then o = o := rfl
-
-theorem isLE_then_iff_or {o₁ o₂ : Ordering} : (o₁.then o₂).isLE ↔ o₁ = lt ∨ (o₁ = eq ∧ o₂.isLE) := by
-  cases o₁ <;> simp
-
-theorem isLE_then_iff_and {o₁ o₂ : Ordering} : (o₁.then o₂).isLE ↔ o₁.isLE ∧ (o₁ = lt ∨ o₂.isLE) := by
-  cases o₁ <;> simp
-
-theorem isLE_left_of_isLE_then {o₁ o₂ : Ordering} (h : (o₁.then o₂).isLE) : o₁.isLE := by
-  cases o₁ <;> simp_all
-
-theorem isGE_left_of_isGE_then {o₁ o₂ : Ordering} (h : (o₁.then o₂).isGE) : o₁.isGE := by
-  cases o₁ <;> simp_all
+instance : Std.LawfulIdentity Ordering.then eq where
+  left_id _ := eq_then
+  right_id _ := then_eq
 
 end Lemmas
 
@@ -375,7 +335,7 @@ section Lemmas
 @[simp]
 theorem compareLex_eq_eq {α} {cmp₁ cmp₂} {a b : α} :
     compareLex cmp₁ cmp₂ a b = .eq ↔ cmp₁ a b = .eq ∧ cmp₂ a b = .eq := by
-  simp [compareLex, Ordering.then_eq_eq]
+  simp [compareLex]
 
 theorem compareOfLessAndEq_eq_swap_of_lt_iff_not_gt_and_ne {α : Type u} [LT α] [DecidableLT α] [DecidableEq α]
     (h : ∀ x y : α, x < y ↔ ¬ y < x ∧ x ≠ y) {x y : α} :
@@ -384,14 +344,14 @@ theorem compareOfLessAndEq_eq_swap_of_lt_iff_not_gt_and_ne {α : Type u} [LT α]
   split
   · rename_i h'
     rw [h] at h'
-    simp only [h'.1, h'.2.symm, reduceIte, Ordering.swap_gt]
+    simp only [h'.1, h'.2.symm, ↓reduceIte, Ordering.swap_gt]
   · split
     · rename_i h'
       have : ¬ y < y := Not.imp (·.2 rfl) <| (h y y).mp
-      simp only [h', this, reduceIte, Ordering.swap_eq]
+      simp only [h', this, ↓reduceIte, Ordering.swap_eq]
     · rename_i h' h''
       replace h' := (h y x).mpr ⟨h', Ne.symm h''⟩
-      simp only [h', Ne.symm h'', reduceIte, Ordering.swap_lt]
+      simp only [h', Ne.symm h'', ↓reduceIte, Ordering.swap_lt]
 
 theorem lt_iff_not_gt_and_ne_of_antisymm_of_total_of_not_le
     {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α]
@@ -478,13 +438,13 @@ but this is not enforced by the typeclass.
 There is a derive handler, so appending `deriving Ord` to an inductive type or structure
 will attempt to create an `Ord` instance.
 -/
+@[ext]
 class Ord (α : Type u) where
   /-- Compare two elements in `α` using the comparator contained in an `[Ord α]` instance. -/
   compare : α → α → Ordering
 
 export Ord (compare)
 
-set_option linter.unusedVariables false in  -- allow specifying `ord` explicitly
 /--
 Compares two values by comparing the results of applying a function.
 
@@ -764,6 +724,13 @@ end Vector
 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] 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`.
@@ -771,8 +738,9 @@ Constructs an `LT` instance from an `Ord` instance that asserts that the result
 @[expose] def ltOfOrd [Ord α] : LT α where
   lt a b := compare a b = Ordering.lt
 
-instance [Ord α] : DecidableRel (@LT.lt α ltOfOrd) :=
-  inferInstanceAs (DecidableRel (fun a b => compare a b = Ordering.lt))
+@[inline]
+instance [Ord α] : DecidableRel (@LT.lt α ltOfOrd) := fun a b =>
+  decidable_of_bool (compare a b).isLT Ordering.isLT_iff_eq_lt
 
 /--
 Constructs an `LT` instance from an `Ord` instance that asserts that the result of `compare`
@@ -781,35 +749,29 @@ satisfies `Ordering.isLE`.
 @[expose] def leOfOrd [Ord α] : LE α where
   le a b := (compare a b).isLE
 
-instance [Ord α] : DecidableRel (@LE.le α leOfOrd) :=
-  inferInstanceAs (DecidableRel (fun a b => (compare a b).isLE))
+@[inline]
+instance [Ord α] : DecidableRel (@LE.le α leOfOrd) := fun _ _ => instDecidableEqBool ..
 
 namespace Ord
 
 /--
 Constructs a `BEq` instance from an `Ord` instance.
 -/
-protected def toBEq (ord : Ord α) : BEq α where
-  beq x y := ord.compare x y == .eq
+@[expose] protected abbrev toBEq (ord : Ord α) : BEq α :=
+  beqOfOrd
 
 /--
 Constructs an `LT` instance from an `Ord` instance.
 -/
-@[expose] protected def toLT (ord : Ord α) : LT α :=
+@[expose] protected abbrev toLT (ord : Ord α) : LT α :=
   ltOfOrd
 
-instance [i : Ord α] : DecidableRel (@LT.lt _ (Ord.toLT i)) :=
-  inferInstanceAs (DecidableRel (fun a b => compare a b = Ordering.lt))
-
 /--
 Constructs an `LE` instance from an `Ord` instance.
 -/
-@[expose] protected def toLE (ord : Ord α) : LE α :=
+@[expose] protected abbrev toLE (ord : Ord α) : LE α :=
   leOfOrd
 
-instance [i : Ord α] : DecidableRel (@LE.le _ (Ord.toLE i)) :=
-  inferInstanceAs (DecidableRel (fun a b => (compare a b).isLE))
-
 /--
 Inverts the order of an `Ord` instance.
 
@@ -833,7 +795,7 @@ protected def on (_ : Ord β) (f : α → β) : Ord α where
 /--
 Constructs the lexicographic order on products `α × β` from orders for `α` and `β`.
 -/
-protected def lex (_ : Ord α) (_ : Ord β) : Ord (α × β) :=
+protected abbrev lex (_ : Ord α) (_ : Ord β) : Ord (α × β) :=
   lexOrd
 
 /--

src/Init/Data/Vector/Basic.lean

@@ -198,6 +198,8 @@ result is empty. If `stop` is greater than the size of the vector, the size is u
 /--
 Extract the first `i` elements of a vector. If `i` is greater than or equal to the size of the
 vector then the vector is returned unchanged.
+
+We immediately simplify this to the `extract` operation, so there is no verification API for this function.
 -/
 @[inline] def take (xs : Vector α n) (i : Nat) : Vector α (min i n) :=
   ⟨xs.toArray.take i, by simp⟩
@@ -207,16 +209,22 @@ vector then the vector is returned unchanged.
 /--
 Deletes the first `i` elements of a vector. If `i` is greater than or equal to the size of the
 vector then the empty vector is returned.
+
+We immediately simplify this to the `extract` operation, so there is no verification API for this function.
 -/
 @[inline] def drop (xs : Vector α n) (i : Nat) : Vector α (n - i) :=
   ⟨xs.toArray.drop i, by simp⟩
 
 set_option linter.indexVariables false in
 @[simp] theorem drop_eq_cast_extract (xs : Vector α n) (i : Nat) :
-    xs.drop i = (xs.extract i n).cast (by simp) := by
+    xs.drop i = (xs.extract i).cast (by simp) := by
   simp [drop, extract, Vector.cast]
 
-/-- Shrinks a vector to the first `m` elements, by repeatedly popping the last element. -/
+/--
+Shrinks a vector to the first `m` elements, by repeatedly popping the last element.
+
+We immediately simplify this to the `extract` operation, so there is no verification API for this function.
+-/
 @[inline] def shrink (xs : Vector α n) (i : Nat) : Vector α (min i n) :=
   ⟨xs.toArray.shrink i, by simp⟩
 
@@ -394,12 +402,17 @@ instance [BEq α] : BEq (Vector α n) where
     have : Inhabited (Vector α (n+1)) := ⟨xs.push x⟩
     panic! "index out of bounds"
 
-/-- Delete the first element of a vector. Returns the empty vector if the input vector is empty. -/
-@[inline] def tail (xs : Vector α n) : Vector α (n-1) :=
-  if _ : 0 < n then
-    xs.eraseIdx 0
-  else
-    xs.cast (by omega)
+/--
+Delete the first element of a vector. Returns the empty vector if the input vector is empty.
+
+We immediately simplify this to the `extract` operation, so there is no verification API for this function.
+-/
+@[inline]
+def tail (xs : Vector α n) : Vector α (n-1) :=
+  (xs.extract 1).cast (by omega)
+
+@[simp] theorem tail_eq_cast_extract (xs : Vector α n) :
+    xs.tail = (xs.extract 1).cast (by omega) := rfl
 
 /--
 Finds the first index of a given value in a vector using `==` for comparison. Returns `none` if the

src/Init/Data/Vector/Lemmas.lean

@@ -486,7 +486,7 @@ abbrev toArray_mkVector := @toArray_replicate
 `Vector.ext` is an extensionality theorem.
 Vectors `a` and `b` are equal to each other if their elements are equal for each valid index.
 -/
-@[ext]
+@[ext, grind ext]
 protected theorem ext {xs ys : Vector α n} (h : (i : Nat) → (_ : i < n) → xs[i] = ys[i]) : xs = ys := by
   apply Vector.toArray_inj.1
   apply Array.ext
@@ -816,14 +816,11 @@ abbrev mkVector_eq_mk_mkArray := @replicate_eq_mk_replicate
 
 /-! ## L[i] and L[i]? -/
 
-@[simp] theorem getElem?_eq_none_iff {xs : Vector α n} : xs[i]? = none ↔ n ≤ i := by
-  by_cases h : i < n
-  · simp [getElem?_pos, h]
-  · rw [getElem?_neg xs i h]
-    simp_all
+theorem getElem?_eq_none_iff {xs : Vector α n} : xs[i]? = none ↔ n ≤ i := by
+  simp
 
-@[simp] theorem none_eq_getElem?_iff {xs : Vector α n} {i : Nat} : none = xs[i]? ↔ n ≤ i := by
-  simp [eq_comm (a := none)]
+theorem none_eq_getElem?_iff {xs : Vector α n} {i : Nat} : none = xs[i]? ↔ n ≤ i := by
+  simp
 
 theorem getElem?_eq_none {xs : Vector α n} (h : n ≤ i) : xs[i]? = none := by
   simp [getElem?_eq_none_iff, h]
@@ -835,15 +832,15 @@ grind_pattern Vector.getElem?_eq_none => n ≤ i, xs[i]?
 @[simp] theorem getElem?_eq_getElem {xs : Vector α n} {i : Nat} (h : i < n) : xs[i]? = some xs[i] :=
   getElem?_pos ..
 
-theorem getElem?_eq_some_iff {xs : Vector α n} : xs[i]? = some b ↔ ∃ h : i < n, xs[i] = b := by
-  simp [getElem?_def]
+theorem getElem?_eq_some_iff {xs : Vector α n} : xs[i]? = some b ↔ ∃ h : i < n, xs[i] = b :=
+  _root_.getElem?_eq_some_iff
 
 @[grind →]
 theorem getElem_of_getElem? {xs : Vector α n} : xs[i]? = some a → ∃ h : i < n, xs[i] = a :=
   getElem?_eq_some_iff.mp
 
-theorem some_eq_getElem?_iff {xs : Vector α n} : some b = xs[i]? ↔ ∃ h : i < n, xs[i] = b := by
-  rw [eq_comm, getElem?_eq_some_iff]
+theorem some_eq_getElem?_iff {xs : Vector α n} : some b = xs[i]? ↔ ∃ h : i < n, xs[i] = b :=
+  _root_.some_eq_getElem?_iff
 
 @[simp] theorem some_getElem_eq_getElem?_iff {xs : Vector α n} {i : Nat} (h : i < n) :
     (some xs[i] = xs[i]?) ↔ True := by
@@ -2105,7 +2102,7 @@ abbrev forall_mem_mkVector := @forall_mem_replicate
 @[deprecated getElem_replicate (since := "2025-03-18")]
 abbrev getElem_mkVector := @getElem_replicate
 
-@[grind]theorem getElem?_replicate {a : α} {n i : Nat} : (replicate n a)[i]? = if i < n then some a else none := by
+@[grind] theorem getElem?_replicate {a : α} {n i : Nat} : (replicate n a)[i]? = if i < n then some a else none := by
   simp [getElem?_def]
 
 @[deprecated getElem?_replicate (since := "2025-03-18")]
@@ -2385,19 +2382,23 @@ theorem foldrM_pure [Monad m] [LawfulMonad m] {f : α → β → β} {b} {xs : V
   Array.foldrM_pure
 
 theorem foldl_eq_foldlM {f : β → α → β} {b} {xs : Vector α n} :
-    xs.foldl f b = xs.foldlM (m := Id) f b := by
-  rcases xs with ⟨xs, rfl⟩
-  simp [Array.foldl_eq_foldlM]
+    xs.foldl f b = (xs.foldlM (m := Id) (pure <| f · ·) b).run := rfl
 
 theorem foldr_eq_foldrM {f : α → β → β} {b} {xs : Vector α n} :
-    xs.foldr f b = xs.foldrM (m := Id) f b := by
-  rcases xs with ⟨xs, rfl⟩
-  simp [Array.foldr_eq_foldrM]
+    xs.foldr f b = (xs.foldrM (m := Id) (pure <| f · ·) b).run := rfl
 
-@[simp] theorem id_run_foldlM {f : β → α → Id β} {b} {xs : Vector α n} :
+@[simp] theorem idRun_foldlM {f : β → α → Id β} {b} {xs : Vector α n} :
+    Id.run (xs.foldlM f b) = xs.foldl (f · · |>.run) b := foldl_eq_foldlM.symm
+
+@[deprecated idRun_foldlM (since := "2025-05-21")]
+theorem id_run_foldlM {f : β → α → Id β} {b} {xs : Vector α n} :
     Id.run (xs.foldlM f b) = xs.foldl f b := foldl_eq_foldlM.symm
 
-@[simp] theorem id_run_foldrM {f : α → β → Id β} {b} {xs : Vector α n} :
+@[simp] theorem idRun_foldrM {f : α → β → Id β} {b} {xs : Vector α n} :
+    Id.run (xs.foldrM f b) = xs.foldr (f · · |>.run) b := foldr_eq_foldrM.symm
+
+@[deprecated idRun_foldrM (since := "2025-05-21")]
+theorem id_run_foldrM {f : α → β → Id β} {b} {xs : Vector α n} :
     Id.run (xs.foldrM f b) = xs.foldr f b := foldr_eq_foldrM.symm
 
 @[simp] theorem foldlM_reverse [Monad m] {xs : Vector α n} {f : β → α → m β} {b} :
@@ -2485,10 +2486,10 @@ theorem foldr_map_hom {g : α → β} {f : α → α → α} {f' : β → β →
   simp
 
 @[simp, grind _=_] theorem foldl_append {β : Type _} {f : β → α → β} {b} {xs : Vector α n} {ys : Vector α k} :
-    (xs ++ ys).foldl f b = ys.foldl f (xs.foldl f b) := by simp [foldl_eq_foldlM]
+    (xs ++ ys).foldl f b = ys.foldl f (xs.foldl f b) := foldlM_append
 
 @[simp, grind _=_] theorem foldr_append {f : α → β → β} {b} {xs : Vector α n} {ys : Vector α k} :
-    (xs ++ ys).foldr f b = xs.foldr f (ys.foldr f b) := by simp [foldr_eq_foldrM]
+    (xs ++ ys).foldr f b = xs.foldr f (ys.foldr f b) := foldrM_append
 
 @[simp, grind] theorem foldl_flatten {f : β → α → β} {b} {xss : Vector (Vector α m) n} :
     (flatten xss).foldl f b = xss.foldl (fun b xs => xs.foldl f b) b := by
@@ -2501,7 +2502,8 @@ theorem foldr_map_hom {g : α → β} {f : α → α → α} {f' : β → β →
   simp [Array.foldr_flatten', Array.foldr_map']
 
 @[simp, grind] theorem foldl_reverse {xs : Vector α n} {f : β → α → β} {b} :
-    xs.reverse.foldl f b = xs.foldr (fun x y => f y x) b := by simp [foldl_eq_foldlM, foldr_eq_foldrM]
+    xs.reverse.foldl f b = xs.foldr (fun x y => f y x) b :=
+  foldlM_reverse
 
 @[simp, grind] theorem foldr_reverse {xs : Vector α n} {f : α → β → β} {b} :
     xs.reverse.foldr f b = xs.foldl (fun x y => f y x) b :=
@@ -2680,7 +2682,7 @@ theorem contains_iff_exists_mem_beq [BEq α] {xs : Vector α n} {a : α} :
   rcases xs with ⟨xs, rfl⟩
   simp [Array.contains_iff_exists_mem_beq]
 
-@[grind]
+@[grind _=_]
 theorem contains_iff_mem [BEq α] [LawfulBEq α] {xs : Vector α n} {a : α} :
     xs.contains a ↔ a ∈ xs := by
   simp

src/Init/Data/Vector/Lex.lean

@@ -60,7 +60,7 @@ protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {xs ys
 
 @[simp] theorem singleton_lex_singleton [BEq α] {lt : α → α → Bool} : #v[a].lex #v[b] lt = lt a b := by
   simp only [lex, getElem_mk, List.getElem_toArray, List.getElem_singleton]
-  cases lt a b <;> cases a != b <;> simp [Id.run]
+  cases lt a b <;> cases a != b <;> simp
 
 protected theorem lt_irrefl [LT α] [Std.Irrefl (· < · : α → α → Prop)] (xs : Vector α n) : ¬ xs < xs :=
   Array.lt_irrefl xs.toArray

src/Init/Data/Vector/Monadic.lean

@@ -148,12 +148,18 @@ theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
   rcases xs with ⟨xs, rfl⟩
   simp [Array.forIn'_pure_yield_eq_foldl, Array.foldl_map]
 
-@[simp] theorem forIn'_yield_eq_foldl
+@[simp] theorem idRun_forIn'_yield_eq_foldl
+    {xs : Vector α n} (f : (a : α) → a ∈ xs → β → Id β) (init : β) :
+    (forIn' xs init (fun a m b => .yield <$> f a m b)).run =
+      xs.attach.foldl (fun b ⟨a, h⟩ => f a h b |>.run) init :=
+  forIn'_pure_yield_eq_foldl _ _
+
+@[deprecated forIn'_yield_eq_foldl (since := "2025-05-21")]
+theorem forIn'_yield_eq_foldl
     {xs : Vector α n} (f : (a : α) → a ∈ xs → β → β) (init : β) :
     forIn' (m := Id) xs init (fun a m b => .yield (f a m b)) =
-      xs.attach.foldl (fun b ⟨a, h⟩ => f a h b) init := by
-  rcases xs with ⟨xs, rfl⟩
-  simp [List.foldl_map]
+      xs.attach.foldl (fun b ⟨a, h⟩ => f a h b) init :=
+  forIn'_pure_yield_eq_foldl _ _
 
 @[simp] theorem forIn'_map [Monad m] [LawfulMonad m]
     {xs : Vector α n} (g : α → β) (f : (b : β) → b ∈ xs.map g → γ → m (ForInStep γ)) :
@@ -190,12 +196,18 @@ theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
   rcases xs with ⟨xs, rfl⟩
   simp [Array.forIn_pure_yield_eq_foldl, Array.foldl_map]
 
-@[simp] theorem forIn_yield_eq_foldl
+@[simp] theorem idRun_forIn_yield_eq_foldl
+    {xs : Vector α n} (f : α → β → Id β) (init : β) :
+    (forIn xs init (fun a b => .yield <$> f a b)).run =
+      xs.foldl (fun b a => f a b |>.run) init :=
+  forIn_pure_yield_eq_foldl _ _
+
+@[deprecated idRun_forIn_yield_eq_foldl (since := "2025-05-21")]
+theorem forIn_yield_eq_foldl
     {xs : Vector α n} (f : α → β → β) (init : β) :
     forIn (m := Id) xs init (fun a b => .yield (f a b)) =
-      xs.foldl (fun b a => f a b) init := by
-  rcases xs with ⟨xs, rfl⟩
-  simp
+      xs.foldl (fun b a => f a b) init :=
+  forIn_pure_yield_eq_foldl _ _
 
 @[simp] theorem forIn_map [Monad m] [LawfulMonad m]
     {xs : Vector α n} (g : α → β) (f : β → γ → m (ForInStep γ)) :

src/Init/Data/Vector/OfFn.lean

@@ -154,7 +154,6 @@ theorem ofFnM_pure [Monad m] [LawfulMonad m] {n} {f : Fin n → α} :
 
 @[simp, grind =] theorem idRun_ofFnM {f : Fin n → Id α} :
     Id.run (ofFnM f) = ofFn (fun i => Id.run (f i)) := by
-  unfold Id.run
   induction n with
   | zero => simp
   | succ n ih => simp [ofFnM_succ', ofFn_succ', ih]

src/Init/Ext.lean

@@ -82,6 +82,8 @@ end Lean
 attribute [ext] Prod PProd Sigma PSigma
 attribute [ext] funext propext Subtype.eq Array.ext
 
+attribute [grind ext] Array.ext
+
 @[ext] protected theorem PUnit.ext (x y : PUnit) : x = y := rfl
 protected theorem Unit.ext (x y : Unit) : x = y := rfl
 

src/Init/GetElem.lean

@@ -198,6 +198,58 @@ theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem d
   simp only [getElem?_def]
   split <;> simp_all
 
+@[simp] theorem none_eq_getElem?_iff [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+    (c : cont) (i : idx) [Decidable (dom c i)] : none = c[i]? ↔ ¬dom c i := by
+  simp only [getElem?_def]
+  split <;> simp_all
+
+theorem of_getElem?_eq_some [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+    {c : cont} {i : idx} [Decidable (dom c i)] (h : c[i]? = some e) : dom c i := by
+  simp only [getElem?_def] at h
+  split at h <;> rename_i h'
+  case isTrue =>
+    exact h'
+  case isFalse =>
+    simp at h
+
+theorem getElem?_eq_some_iff [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+    {c : cont} {i : idx} [Decidable (dom c i)] : c[i]? = some e ↔ Exists fun h : dom c i => c[i] = e := by
+  simp only [getElem?_def]
+  split <;> rename_i h
+  case isTrue =>
+    constructor
+    case mp =>
+      intro w
+      refine ⟨h, ?_⟩
+      simpa using w
+    case mpr =>
+      intro ⟨h, w⟩
+      simpa using w
+  case isFalse =>
+    simp only [reduceCtorEq, false_iff]
+    intro ⟨w, w'⟩
+    exact h w
+
+theorem some_eq_getElem?_iff [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+    {c : cont} {i : idx} [Decidable (dom c i)] : some e = c[i]? ↔ Exists fun h : dom c i => c[i] = e := by
+  rw [eq_comm, getElem?_eq_some_iff]
+
+theorem getElem_of_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+    {c : cont} {i : idx} [Decidable (dom c i)] (h : c[i]? = some e) : Exists fun h : dom c i => c[i] = e :=
+  getElem?_eq_some_iff.mp h
+
+grind_pattern getElem_of_getElem? => c[i]?, some e
+
+@[simp] theorem some_getElem_eq_getElem?_iff [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+    {c : cont} {i : idx} [Decidable (dom c i)] (h : dom c i):
+    (some c[i] = c[i]?) ↔ True := by
+  simpa [some_eq_getElem?_iff, h] using ⟨h, trivial⟩
+
+@[simp] theorem getElem?_eq_some_getElem_iff [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+    {c : cont} {i : idx} [Decidable (dom c i)] (h : dom c i):
+    (c[i]? = some c[i]) ↔ True := by
+  simpa [getElem?_eq_some_iff, h] using ⟨h, trivial⟩
+
 @[deprecated getElem?_eq_none_iff (since := "2025-02-17")]
 abbrev getElem?_eq_none := @getElem?_eq_none_iff
 

src/Init/Grind.lean

@@ -16,4 +16,5 @@ import Init.Grind.Offset
 import Init.Grind.PP
 import Init.Grind.CommRing
 import Init.Grind.Module
+import Init.Grind.Ordered
 import Init.Grind.Ext

src/Init/Grind/Cases.lean

@@ -9,5 +9,5 @@ prelude
 import Init.Core
 import Init.Grind.Tactics
 
-attribute [grind cases eager] And Prod False Empty True Unit Exists Subtype
+attribute [grind cases eager] And Prod False Empty True PUnit Exists Subtype
 attribute [grind cases] Or

src/Init/Grind/CommRing/Basic.lean

@@ -104,6 +104,12 @@ theorem ofNat_mul (a b : Nat) : OfNat.ofNat (α := α) (a * b) = OfNat.ofNat a *
 theorem natCast_mul (a b : Nat) : ((a * b : Nat) : α) = ((a : α) * (b : α)) := by
   rw [← ofNat_eq_natCast, ofNat_mul, ofNat_eq_natCast, ofNat_eq_natCast]
 
+theorem pow_one (a : α) : a ^ 1 = a := by
+  rw [pow_succ, pow_zero, one_mul]
+
+theorem pow_two (a : α) : a ^ 2 = a * a := by
+  rw [pow_succ, pow_one]
+
 theorem pow_add (a : α) (k₁ k₂ : Nat) : a ^ (k₁ + k₂) = a^k₁ * a^k₂ := by
   induction k₂
   next => simp [pow_zero, mul_one]
@@ -274,7 +280,6 @@ instance : IntModule α where
   hmul_zero := by simp [mul_zero]
   hmul_add := by simp [left_distrib]
   mul_hmul := by simp [intCast_mul, mul_assoc]
-  neg_hmul := by simp [intCast_neg, neg_mul]
   neg_add_cancel := by simp [neg_add_cancel]
   sub_eq_add_neg := by simp [sub_eq_add_neg]
 

src/Init/Grind/CommRing/Field.lean

@@ -12,8 +12,8 @@ namespace Lean.Grind
 
 class Field (α : Type u) extends CommRing α, Inv α, Div α where
   div_eq_mul_inv : ∀ a b : α, a / b = a * b⁻¹
+  zero_ne_one : (0 : α) ≠ 1
   inv_zero : (0 : α)⁻¹ = 0
-  inv_one : (1 : α)⁻¹ = 1
   mul_inv_cancel : ∀ {a : α}, a ≠ 0 → a * a⁻¹ = 1
 
 attribute [instance 100] Field.toInv Field.toDiv
@@ -25,6 +25,52 @@ variable [Field α] {a : α}
 theorem inv_mul_cancel (h : a ≠ 0) : a⁻¹ * a = 1 := by
   rw [CommSemiring.mul_comm, mul_inv_cancel h]
 
+theorem eq_inv_of_mul_eq_one (h : a * b = 1) : a = b⁻¹ := by
+  by_cases h' : b = 0
+  · subst h'
+    rw [Semiring.mul_zero] at h
+    exfalso
+    exact zero_ne_one h
+  · replace h := congrArg (fun x => x * b⁻¹) h
+    simpa [Semiring.mul_assoc, mul_inv_cancel h', Semiring.mul_one, Semiring.one_mul] using h
+
+theorem inv_one : (1 : α)⁻¹ = 1 :=
+  (eq_inv_of_mul_eq_one (Semiring.mul_one 1)).symm
+
+theorem inv_inv (a : α) : a⁻¹⁻¹ = a := by
+  by_cases h : a = 0
+  · subst h
+    simp [Field.inv_zero]
+  · symm
+    apply eq_inv_of_mul_eq_one
+    exact mul_inv_cancel h
+
+theorem inv_neg (a : α) : (-a)⁻¹ = -a⁻¹ := by
+  by_cases h : a = 0
+  · subst h
+    simp [Field.inv_zero, Ring.neg_zero]
+  · symm
+    apply eq_inv_of_mul_eq_one
+    simp [Ring.neg_mul, Ring.mul_neg, Ring.neg_neg, Field.inv_mul_cancel h]
+
+theorem inv_eq_zero_iff {a : α} : a⁻¹ = 0 ↔ a = 0 := by
+  constructor
+  · intro w
+    by_cases h : a = 0
+    · subst h
+      rfl
+    · have := congrArg (fun x => x * a) w
+      dsimp at this
+      rw [Semiring.zero_mul, inv_mul_cancel h] at this
+      exfalso
+      exact zero_ne_one this.symm
+  · intro w
+    subst w
+    simp [Field.inv_zero]
+
+theorem zero_eq_inv_iff {a : α} : 0 = a⁻¹ ↔ 0 = a := by
+  rw [eq_comm, inv_eq_zero_iff, eq_comm]
+
 instance [IsCharP α 0] : NoNatZeroDivisors α where
   no_nat_zero_divisors := by
     intro a b h w

src/Init/Grind/Module.lean

@@ -7,4 +7,3 @@ module
 
 prelude
 import Init.Grind.Module.Basic
-import Init.Grind.Module.Int

src/Init/Grind/Module/Basic.lean

@@ -32,16 +32,17 @@ class IntModule (M : Type u) extends Zero M, Add M, Neg M, Sub M, HMul Int M M w
   zero_hmul : ∀ a : M, (0 : Int) * a = 0
   one_hmul : ∀ a : M, (1 : Int) * a = a
   add_hmul : ∀ n m : Int, ∀ a : M, (n + m) * a = n * a + m * a
-  neg_hmul : ∀ n : Int, ∀ a : M, (-n) * a = - (n * a)
   hmul_zero : ∀ n : Int, n * (0 : M) = 0
   hmul_add : ∀ n : Int, ∀ a b : M, n * (a + b) = n * a + n * b
   mul_hmul : ∀ n m : Int, ∀ a : M, (n * m) * a = n * (m * a)
   neg_add_cancel : ∀ a : M, -a + a = 0
   sub_eq_add_neg : ∀ a b : M, a - b = a + -b
 
+namespace IntModule
+
 attribute [instance 100] IntModule.toZero IntModule.toAdd IntModule.toNeg IntModule.toSub IntModule.toHMul
 
-instance IntModule.toNatModule (M : Type u) [i : IntModule M] : NatModule M :=
+instance toNatModule (M : Type u) [i : IntModule M] : NatModule M :=
   { i with
     hMul a x := (a : Int) * x
     hmul_zero := by simp [IntModule.hmul_zero]
@@ -49,22 +50,58 @@ instance IntModule.toNatModule (M : Type u) [i : IntModule M] : NatModule M :=
     hmul_add := by simp [IntModule.hmul_add]
     mul_hmul := by simp [IntModule.mul_hmul] }
 
-/-- A preorder is a reflexive, transitive relation `≤` with `a < b` defined in the obvious way. -/
-class Preorder (α : Type u) extends LE α, LT α where
-  le_refl : ∀ a : α, a ≤ a
-  le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c
-  lt := fun a b => a ≤ b ∧ ¬b ≤ a
-  lt_iff_le_not_le : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬b ≤ a := by intros; rfl
+variable {M : Type u} [IntModule M]
 
-class IntModule.IsOrdered (M : Type u) [Preorder M] [IntModule M] where
-  neg_le_iff : ∀ a b : M, -a ≤ b ↔ -b ≤ a
-  neg_lt_iff : ∀ a b : M, -a < b ↔ -b < a
-  add_lt_left : ∀ a b c : M, a < b → a + c < b + c
-  add_lt_right : ∀ a b c : M, a < b → c + a < c + b
-  hmul_pos : ∀ (k : Int) (a : M), 0 < a → (0 < k ↔ 0 < k * a)
-  hmul_neg : ∀ (k : Int) (a : M), a < 0 → (0 < k ↔ k * a < 0)
-  hmul_nonneg : ∀ (k : Int) (a : M), 0 ≤ a → 0 ≤ k → 0 ≤ k * a
-  hmul_nonpos : ∀ (k : Int) (a : M), a ≤ 0 → 0 ≤ k → k * a ≤ 0
+theorem add_neg_cancel (a : M) : a + -a = 0 := by
+  rw [add_comm, neg_add_cancel]
+
+theorem add_left_inj {a b : M} (c : M) : a + c = b + c ↔ a = b :=
+  ⟨fun h => by simpa [add_assoc, add_neg_cancel, add_zero] using (congrArg (· + -c) h),
+   fun g => congrArg (· + c) g⟩
+
+theorem add_right_inj (a b c : M) : a + b = a + c ↔ b = c := by
+  rw [add_comm a b, add_comm a c, add_left_inj]
+
+theorem neg_zero : (-0 : M) = 0 := by
+  rw [← add_left_inj 0, neg_add_cancel, add_zero]
+
+theorem neg_neg (a : M) : -(-a) = a := by
+  rw [← add_left_inj (-a), neg_add_cancel, add_neg_cancel]
+
+theorem neg_eq_zero (a : M) : -a = 0 ↔ a = 0 :=
+  ⟨fun h => by
+    replace h := congrArg (-·) h
+    simpa [neg_neg, neg_zero] using h,
+   fun h => by rw [h, neg_zero]⟩
+
+theorem neg_add (a b : M) : -(a + b) = -a + -b := by
+  rw [← add_left_inj (a + b), neg_add_cancel, add_assoc (-a), add_comm a b, ← add_assoc (-b),
+    neg_add_cancel, zero_add, neg_add_cancel]
+
+theorem neg_sub (a b : M) : -(a - b) = b - a := by
+  rw [sub_eq_add_neg, neg_add, neg_neg, sub_eq_add_neg, add_comm]
+
+theorem sub_self (a : M) : a - a = 0 := by
+  rw [sub_eq_add_neg, add_neg_cancel]
+
+theorem sub_eq_iff {a b c : M} : a - b = c ↔ a = c + b := by
+  rw [sub_eq_add_neg]
+  constructor
+  next => intro; subst c; rw [add_assoc, neg_add_cancel, add_zero]
+  next => intro; subst a; rw [add_assoc, add_comm b, neg_add_cancel, add_zero]
+
+theorem sub_eq_zero_iff {a b : M} : a - b = 0 ↔ a = b := by
+  simp [sub_eq_iff, zero_add]
+
+theorem neg_hmul (n : Int) (a : M) : (-n) * a = - (n * a) := by
+  apply (add_left_inj (n * a)).mp
+  rw [← add_hmul, Int.add_left_neg, zero_hmul, neg_add_cancel]
+
+theorem hmul_neg (n : Int) (a : M) : n * (-a) = - (n * a) := by
+  apply (add_left_inj (n * a)).mp
+  rw [← hmul_add, neg_add_cancel, neg_add_cancel, hmul_zero]
+
+end IntModule
 
 /--
 Special case of Mathlib's `NoZeroSMulDivisors Nat α`.

src/Init/Grind/Ordered.lean

@@ -0,0 +1,13 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+import Init.Grind.Ordered.Order
+import Init.Grind.Ordered.Module
+import Init.Grind.Ordered.Ring
+import Init.Grind.Ordered.Field
+import Init.Grind.Ordered.Int

src/Init/Grind/Ordered/Field.lean

@@ -0,0 +1,188 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+import Init.Grind.CommRing.Field
+import Init.Grind.Ordered.Ring
+
+namespace Lean.Grind
+
+namespace Field.IsOrdered
+
+variable {R : Type u} [Field R] [LinearOrder R] [Ring.IsOrdered R]
+
+open Ring.IsOrdered
+
+theorem pos_of_inv_pos {a : R} (h : 0 < a⁻¹) : 0 < a := by
+  rcases LinearOrder.trichotomy 0 a with (h' | rfl | h')
+  · exact h'
+  · simpa [Field.inv_zero] using h
+  · exfalso
+    have := Ring.IsOrdered.mul_neg_of_pos_of_neg h h'
+    rw [inv_mul_cancel (Preorder.ne_of_lt h')] at this
+    exact Ring.IsOrdered.not_one_lt_zero this
+
+theorem inv_pos_iff {a : R} : 0 < a⁻¹ ↔ 0 < a := by
+  constructor
+  · exact pos_of_inv_pos
+  · intro h
+    rw [← Field.inv_inv a] at h
+    exact pos_of_inv_pos h
+
+theorem inv_neg_iff {a : R} : a⁻¹ < 0 ↔ a < 0 := by
+  have := inv_pos_iff (a := -a)
+  rw [Field.inv_neg] at this
+  simpa [IntModule.IsOrdered.neg_pos_iff]
+
+theorem inv_nonneg_iff {a : R} : 0 ≤ a⁻¹ ↔ 0 ≤ a := by
+  simp [PartialOrder.le_iff_lt_or_eq, inv_pos_iff, Field.zero_eq_inv_iff]
+
+theorem inv_nonpos_iff {a : R} : a⁻¹ ≤ 0 ↔ a ≤ 0 := by
+  have := inv_nonneg_iff (a := -a)
+  rw [Field.inv_neg] at this
+  simpa [IntModule.IsOrdered.neg_nonneg_iff] using this
+
+private theorem mul_le_of_le_mul_inv {a b c : R} (h : 0 < c) (h' : a ≤ b * c⁻¹) : a * c ≤ b := by
+  simpa [Semiring.mul_assoc, Field.inv_mul_cancel (Preorder.ne_of_gt h), Semiring.mul_one] using
+    Ring.IsOrdered.mul_le_mul_of_nonneg_right h' (Preorder.le_of_lt h)
+
+private theorem le_mul_inv_of_mul_le {a b c : R} (h : 0 < b) (h' : a * b ≤ c) : a ≤ c * b⁻¹ := by
+  simpa [Semiring.mul_assoc, Field.mul_inv_cancel (Preorder.ne_of_gt h), Semiring.mul_one] using
+    Ring.IsOrdered.mul_le_mul_of_nonneg_right h' (Preorder.le_of_lt (inv_pos_iff.mpr h))
+
+theorem le_mul_inv_iff_mul_le (a b : R) {c : R} (h : 0 < c) : a ≤ b * c⁻¹ ↔ a * c ≤ b :=
+  ⟨mul_le_of_le_mul_inv h, le_mul_inv_of_mul_le h⟩
+
+private theorem mul_inv_le_iff_le_mul (a c : R) {b : R} (h : 0 < b) : a * b⁻¹ ≤ c ↔ a ≤ c * b := by
+  have := (le_mul_inv_iff_mul_le a c (inv_pos_iff.mpr h)).symm
+  simpa [Field.inv_inv] using this
+
+private theorem mul_lt_of_lt_mul_inv {a b c : R} (h : 0 < c) (h' : a < b * c⁻¹) : a * c < b := by
+  simpa [Semiring.mul_assoc, Field.inv_mul_cancel (Preorder.ne_of_gt h), Semiring.mul_one] using
+    Ring.IsOrdered.mul_lt_mul_of_pos_right h' h
+
+private theorem lt_mul_inv_of_mul_lt {a b c : R} (h : 0 < b) (h' : a * b < c) : a < c * b⁻¹ := by
+  simpa [Semiring.mul_assoc, Field.mul_inv_cancel (Preorder.ne_of_gt h), Semiring.mul_one] using
+    Ring.IsOrdered.mul_lt_mul_of_pos_right h' (inv_pos_iff.mpr h)
+
+theorem lt_mul_inv_iff_mul_lt (a b : R) {c : R} (h : 0 < c) : a < b * c⁻¹ ↔ a * c < b :=
+  ⟨mul_lt_of_lt_mul_inv h, lt_mul_inv_of_mul_lt h⟩
+
+theorem mul_inv_lt_iff_lt_mul (a c : R) {b : R} (h : 0 < b) : a * b⁻¹ < c ↔ a < c * b := by
+  simpa [Field.inv_inv] using (lt_mul_inv_iff_mul_lt a c (inv_pos_iff.mpr h)).symm
+
+private theorem le_mul_of_le_mul_inv {a b c : R} (h : c < 0) (h' : a ≤ b * c⁻¹) : b ≤ a * c := by
+  simpa [Semiring.mul_assoc, Field.inv_mul_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
+    Ring.IsOrdered.mul_le_mul_of_nonpos_right h' (Preorder.le_of_lt h)
+
+private theorem mul_le_of_mul_inv_le {a b c : R} (h : b < 0) (h' : a * b⁻¹ ≤ c) : c * b ≤ a := by
+  simpa [Semiring.mul_assoc, Field.inv_mul_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
+    Ring.IsOrdered.mul_le_mul_of_nonpos_right h' (Preorder.le_of_lt h)
+
+private theorem mul_inv_le_of_mul_le {a b c : R} (h : b < 0) (h' : a * b ≤ c) : c * b⁻¹ ≤ a := by
+  simpa [Semiring.mul_assoc, Field.mul_inv_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
+    Ring.IsOrdered.mul_le_mul_of_nonpos_right h' (Preorder.le_of_lt (inv_neg_iff.mpr h))
+
+private theorem le_mul_inv_of_le_mul {a b c : R} (h : c < 0) (h' : a ≤ b * c) : b ≤ a * c⁻¹ := by
+  simpa [Semiring.mul_assoc, Field.mul_inv_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
+    Ring.IsOrdered.mul_le_mul_of_nonpos_right h' (Preorder.le_of_lt (inv_neg_iff.mpr h))
+
+theorem le_mul_inv_iff_le_mul_of_neg (a b : R) {c : R} (h : c < 0) : a ≤ b * c⁻¹ ↔ b ≤ a * c :=
+  ⟨le_mul_of_le_mul_inv h, le_mul_inv_of_le_mul h⟩
+
+theorem mul_inv_le_iff_mul_le_of_neg (a c : R) {b : R} (h : b < 0) : a * b⁻¹ ≤ c ↔ c * b ≤ a :=
+  ⟨mul_le_of_mul_inv_le h, mul_inv_le_of_mul_le h⟩
+
+private theorem lt_mul_of_lt_mul_inv {a b c : R} (h : c < 0) (h' : a < b * c⁻¹) : b < a * c := by
+  simpa [Semiring.mul_assoc, Field.inv_mul_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
+    Ring.IsOrdered.mul_lt_mul_of_neg_right h' h
+
+private theorem mul_lt_of_mul_inv_lt {a b c : R} (h : b < 0) (h' : a * b⁻¹ < c) : c * b < a := by
+  simpa [Semiring.mul_assoc, Field.inv_mul_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
+    Ring.IsOrdered.mul_lt_mul_of_neg_right h' h
+
+private theorem mul_inv_lt_of_mul_lt {a b c : R} (h : b < 0) (h' : a * b < c) : c * b⁻¹ < a := by
+  simpa [Semiring.mul_assoc, Field.mul_inv_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
+    Ring.IsOrdered.mul_lt_mul_of_neg_right h' (inv_neg_iff.mpr h)
+
+private theorem lt_mul_inv_of_lt_mul {a b c : R} (h : c < 0) (h' : a < b * c) : b < a * c⁻¹ := by
+  simpa [Semiring.mul_assoc, Field.mul_inv_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
+    Ring.IsOrdered.mul_lt_mul_of_neg_right h' (inv_neg_iff.mpr h)
+
+theorem lt_mul_inv_iff_lt_mul_of_neg (a b : R) {c : R} (h : c < 0) : a < b * c⁻¹ ↔ b < a * c :=
+  ⟨lt_mul_of_lt_mul_inv h, lt_mul_inv_of_lt_mul h⟩
+
+theorem mul_inv_lt_iff_mul_lt_of_neg (a c : R) {b : R} (h : b < 0) : a * b⁻¹ < c ↔ c * b < a :=
+  ⟨mul_lt_of_mul_inv_lt h, mul_inv_lt_of_mul_lt h⟩
+
+theorem mul_lt_mul_iff_of_pos_right {a b c : R} (h : 0 < c) : a * c < b * c ↔ a < b := by
+  constructor
+  · intro h'
+    have := mul_lt_mul_of_pos_right h' (inv_pos_iff.mpr h)
+    rwa [Semiring.mul_assoc, Semiring.mul_assoc, mul_inv_cancel (Preorder.ne_of_gt h),
+      Semiring.mul_one, Semiring.mul_one] at this
+  · exact (mul_lt_mul_of_pos_right · h)
+
+theorem mul_lt_mul_iff_of_pos_left {a b c : R} (h : 0 < c) : c * a < c * b ↔ a < b := by
+  constructor
+  · intro h'
+    have := mul_lt_mul_of_pos_left h' (inv_pos_iff.mpr h)
+    rwa [← Semiring.mul_assoc, ← Semiring.mul_assoc, inv_mul_cancel (Preorder.ne_of_gt h),
+      Semiring.one_mul, Semiring.one_mul] at this
+  · exact (mul_lt_mul_of_pos_left · h)
+
+theorem mul_lt_mul_iff_of_neg_right {a b c : R} (h : c < 0) : a * c < b * c ↔ b < a := by
+  constructor
+  · intro h'
+    have := mul_lt_mul_of_neg_right h' (inv_neg_iff.mpr h)
+    rwa [Semiring.mul_assoc, Semiring.mul_assoc, mul_inv_cancel (Preorder.ne_of_lt h),
+      Semiring.mul_one, Semiring.mul_one] at this
+  · exact (mul_lt_mul_of_neg_right · h)
+
+theorem mul_lt_mul_iff_of_neg_left {a b c : R} (h : c < 0) : c * a < c * b ↔ b < a := by
+  constructor
+  · intro h'
+    have := mul_lt_mul_of_neg_left h' (inv_neg_iff.mpr h)
+    rwa [← Semiring.mul_assoc, ← Semiring.mul_assoc, inv_mul_cancel (Preorder.ne_of_lt h),
+      Semiring.one_mul, Semiring.one_mul] at this
+  · exact (mul_lt_mul_of_neg_left · h)
+
+theorem mul_le_mul_iff_of_pos_right {a b c : R} (h : 0 < c) : a * c ≤ b * c ↔ a ≤ b := by
+  constructor
+  · intro h'
+    have := mul_le_mul_of_nonneg_right h' (Preorder.le_of_lt (inv_pos_iff.mpr h))
+    rwa [Semiring.mul_assoc, Semiring.mul_assoc, mul_inv_cancel (Preorder.ne_of_gt h),
+      Semiring.mul_one, Semiring.mul_one] at this
+  · exact (mul_le_mul_of_nonneg_right · (Preorder.le_of_lt h))
+
+theorem mul_le_mul_iff_of_pos_left {a b c : R} (h : 0 < c) : c * a ≤ c * b ↔ a ≤ b := by
+  constructor
+  · intro h'
+    have := mul_le_mul_of_nonneg_left h' (Preorder.le_of_lt (inv_pos_iff.mpr h))
+    rwa [← Semiring.mul_assoc, ← Semiring.mul_assoc, inv_mul_cancel (Preorder.ne_of_gt h),
+      Semiring.one_mul, Semiring.one_mul] at this
+  · exact (mul_le_mul_of_nonneg_left · (Preorder.le_of_lt h))
+
+theorem mul_le_mul_iff_of_neg_right {a b c : R} (h : c < 0) : a * c ≤ b * c ↔ b ≤ a := by
+  constructor
+  · intro h'
+    have := mul_le_mul_of_nonpos_right h' (Preorder.le_of_lt (inv_neg_iff.mpr h))
+    rwa [Semiring.mul_assoc, Semiring.mul_assoc, mul_inv_cancel (Preorder.ne_of_lt h),
+      Semiring.mul_one, Semiring.mul_one] at this
+  · exact (mul_le_mul_of_nonpos_right · (Preorder.le_of_lt h))
+
+theorem mul_le_mul_iff_of_neg_left {a b c : R} (h : c < 0) : c * a ≤ c * b ↔ b ≤ a := by
+  constructor
+  · intro h'
+    have := mul_le_mul_of_nonpos_left h' (Preorder.le_of_lt (inv_neg_iff.mpr h))
+    rwa [← Semiring.mul_assoc, ← Semiring.mul_assoc, inv_mul_cancel (Preorder.ne_of_lt h),
+      Semiring.one_mul, Semiring.one_mul] at this
+  · exact (mul_le_mul_of_nonpos_left · (Preorder.le_of_lt h))
+
+end Field.IsOrdered
+
+end Lean.Grind

src/Init/Grind/Ordered/Int.lean

@@ -6,7 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
-import Init.Grind.Module.Basic
+import Init.Grind.Ordered.Ring
 import Init.Grind.CommRing.Int
 import Init.Omega
 
@@ -18,17 +18,18 @@ namespace Lean.Grind
 
 instance : Preorder Int where
   le_refl := Int.le_refl
-  le_trans _ _ _ := Int.le_trans
+  le_trans := Int.le_trans
   lt_iff_le_not_le := by omega
 
 instance : IntModule.IsOrdered Int where
   neg_le_iff := by omega
-  neg_lt_iff := by omega
-  add_lt_left := by omega
-  add_lt_right := by omega
+  add_le_left := by omega
   hmul_pos k a ha := ⟨fun hk => Int.mul_pos hk ha, fun h => Int.pos_of_mul_pos_left h ha⟩
-  hmul_neg k a ha := ⟨fun hk => Int.mul_neg_of_pos_of_neg hk ha, fun h => Int.pos_of_mul_neg_left h ha⟩
-  hmul_nonpos k a ha hk := Int.mul_nonpos_of_nonneg_of_nonpos hk ha
-  hmul_nonneg k a ha hk := Int.mul_nonneg hk ha
+  hmul_nonneg hk ha := Int.mul_nonneg hk ha
+
+instance : Ring.IsOrdered Int where
+  zero_lt_one := by omega
+  mul_lt_mul_of_pos_left := Int.mul_lt_mul_of_pos_left
+  mul_lt_mul_of_pos_right := Int.mul_lt_mul_of_pos_right
 
 end Lean.Grind

src/Init/Grind/Ordered/Module.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+import Init.Data.Int.Order
+import Init.Grind.Module.Basic
+import Init.Grind.Ordered.Order
+
+namespace Lean.Grind
+
+class IntModule.IsOrdered (M : Type u) [Preorder M] [IntModule M] where
+  neg_le_iff : ∀ a b : M, -a ≤ b ↔ -b ≤ a
+  add_le_left : ∀ {a b : M}, a ≤ b → (c : M) → a + c ≤ b + c
+  hmul_pos : ∀ (k : Int) {a : M}, 0 < a → (0 < k ↔ 0 < k * a)
+  hmul_nonneg : ∀ {k : Int} {a : M}, 0 ≤ k → 0 ≤ a → 0 ≤ k * a
+
+namespace IntModule.IsOrdered
+
+variable {M : Type u} [Preorder M] [IntModule M] [IntModule.IsOrdered M]
+
+theorem le_neg_iff {a b : M} : a ≤ -b ↔ b ≤ -a := by
+  conv => lhs; rw [← neg_neg a]
+  rw [neg_le_iff, neg_neg]
+
+theorem neg_lt_iff {a b : M} : -a < b ↔ -b < a := by
+  simp [Preorder.lt_iff_le_not_le]
+  rw [neg_le_iff, le_neg_iff]
+
+theorem lt_neg_iff {a b : M} : a < -b ↔ b < -a := by
+  conv => lhs; rw [← neg_neg a]
+  rw [neg_lt_iff, neg_neg]
+
+theorem neg_nonneg_iff {a : M} : 0 ≤ -a ↔ a ≤ 0 := by
+  rw [le_neg_iff, neg_zero]
+
+theorem neg_pos_iff {a : M} : 0 < -a ↔ a < 0 := by
+  rw [lt_neg_iff, neg_zero]
+
+theorem add_lt_left {a b : M} (h : a < b) (c : M) : a + c < b + c := by
+  simp [Preorder.lt_iff_le_not_le] at h ⊢
+  constructor
+  · exact add_le_left h.1 _
+  · intro w
+    apply h.2
+    replace w := add_le_left w (-c)
+    rw [add_assoc, add_assoc, add_neg_cancel, add_zero, add_zero] at w
+    exact w
+
+theorem add_le_right (a : M) {b c : M} (h : b ≤ c) : a + b ≤ a + c := by
+  rw [add_comm a b, add_comm a c]
+  exact add_le_left h a
+
+theorem add_lt_right (a : M) {b c : M} (h : b < c) : a + b < a + c := by
+  rw [add_comm a b, add_comm a c]
+  exact add_lt_left h a
+
+theorem hmul_neg (k : Int) {a : M} (h : a < 0) : 0 < k ↔ k * a < 0 := by
+  simpa [IntModule.hmul_neg, neg_pos_iff] using hmul_pos k (neg_pos_iff.mpr h)
+
+theorem hmul_nonpos {k : Int} {a : M} (hk : 0 ≤ k) (ha : a ≤ 0) : k * a ≤ 0 := by
+  simpa [IntModule.hmul_neg, neg_nonneg_iff] using hmul_nonneg hk (neg_nonneg_iff.mpr ha)
+
+end IntModule.IsOrdered
+
+end Lean.Grind

src/Init/Grind/Ordered/Order.lean

@@ -0,0 +1,96 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+import Init.Data.Int.Order
+
+namespace Lean.Grind
+
+/-- A preorder is a reflexive, transitive relation `≤` with `a < b` defined in the obvious way. -/
+class Preorder (α : Type u) extends LE α, LT α where
+  le_refl : ∀ a : α, a ≤ a
+  le_trans : ∀ {a b c : α}, a ≤ b → b ≤ c → a ≤ c
+  lt := fun a b => a ≤ b ∧ ¬b ≤ a
+  lt_iff_le_not_le : ∀ {a b : α}, a < b ↔ a ≤ b ∧ ¬b ≤ a := by intros; rfl
+
+namespace Preorder
+
+variable {α : Type u} [Preorder α]
+
+theorem le_of_lt {a b : α} (h : a < b) : a ≤ b := (lt_iff_le_not_le.mp h).1
+
+theorem lt_of_lt_of_le {a b c : α} (h₁ : a < b) (h₂ : b ≤ c) : a < c := by
+  simp [lt_iff_le_not_le] at h₁ ⊢
+  exact ⟨le_trans h₁.1 h₂, fun h => h₁.2 (le_trans h₂ h)⟩
+
+theorem lt_of_le_of_lt {a b c : α} (h₁ : a ≤ b) (h₂ : b < c) : a < c := by
+  simp [lt_iff_le_not_le] at h₂ ⊢
+  exact ⟨le_trans h₁ h₂.1, fun h => h₂.2 (le_trans h h₁)⟩
+
+theorem lt_trans {a b c : α} (h₁ : a < b) (h₂ : b < c) : a < c :=
+  lt_of_lt_of_le h₁ (le_of_lt h₂)
+
+theorem lt_irrefl (a : α) : ¬ (a < a) := by
+  intro h
+  simp [lt_iff_le_not_le] at h
+
+theorem ne_of_lt {a b : α} (h : a < b) : a ≠ b :=
+  fun w => lt_irrefl a (w.symm ▸ h)
+
+theorem ne_of_gt {a b : α} (h : a > b) : a ≠ b :=
+  fun w => lt_irrefl b (w.symm ▸ h)
+
+theorem not_ge_of_lt {a b : α} (h : a < b) : ¬b ≤ a :=
+  fun w => lt_irrefl a (lt_of_lt_of_le h w)
+
+theorem not_gt_of_lt {a b : α} (h : a < b) : ¬a > b :=
+  fun w => lt_irrefl a (lt_trans h w)
+
+end Preorder
+
+class PartialOrder (α : Type u) extends Preorder α where
+  le_antisymm : ∀ {a b : α}, a ≤ b → b ≤ a → a = b
+
+namespace PartialOrder
+
+variable {α : Type u} [PartialOrder α]
+
+theorem le_iff_lt_or_eq {a b : α} : a ≤ b ↔ a < b ∨ a = b := by
+  constructor
+  · intro h
+    rw [Preorder.lt_iff_le_not_le, Classical.or_iff_not_imp_right]
+    exact fun w => ⟨h, fun w' => w (le_antisymm h w')⟩
+  · intro h
+    cases h with
+    | inl h => exact Preorder.le_of_lt h
+    | inr h => subst h; exact Preorder.le_refl a
+
+end PartialOrder
+
+class LinearOrder (α : Type u) extends PartialOrder α where
+  le_total : ∀ a b : α, a ≤ b ∨ b ≤ a
+
+namespace LinearOrder
+
+variable {α : Type u} [LinearOrder α]
+
+theorem trichotomy (a b : α) : a < b ∨ a = b ∨ b < a := by
+  cases LinearOrder.le_total a b with
+  | inl h =>
+    rw [PartialOrder.le_iff_lt_or_eq] at h
+    cases h with
+    | inl h => left; exact h
+    | inr h => right; left; exact h
+  | inr h =>
+    rw [PartialOrder.le_iff_lt_or_eq] at h
+    cases h with
+    | inl h => right; right; exact h
+    | inr h => right; left; exact h.symm
+
+end LinearOrder
+
+end Lean.Grind

src/Init/Grind/Ordered/Ring.lean

@@ -0,0 +1,159 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+import Init.Grind.CommRing.Basic
+import Init.Grind.Ordered.Module
+
+namespace Lean.Grind
+
+class Ring.IsOrdered (R : Type u) [Ring R] [Preorder R] extends IntModule.IsOrdered R where
+  /-- In a strict ordered semiring, we have `0 < 1`. -/
+  zero_lt_one : (0 : R) < 1
+  /-- In a strict ordered semiring, we can multiply an inequality `a < b` on the left
+  by a positive element `0 < c` to obtain `c * a < c * b`. -/
+  mul_lt_mul_of_pos_left : ∀ {a b c : R}, a < b → 0 < c → c * a < c * b
+  /-- In a strict ordered semiring, we can multiply an inequality `a < b` on the right
+  by a positive element `0 < c` to obtain `a * c < b * c`. -/
+  mul_lt_mul_of_pos_right : ∀ {a b c : R}, a < b → 0 < c → a * c < b * c
+
+namespace Ring.IsOrdered
+
+variable {R : Type u} [Ring R]
+section PartialOrder
+
+variable [PartialOrder R] [Ring.IsOrdered R]
+
+theorem zero_le_one : (0 : R) ≤ 1 := Preorder.le_of_lt zero_lt_one
+
+theorem not_one_lt_zero : ¬ ((1 : R) < 0) :=
+  fun h => Preorder.lt_irrefl (0 : R) (Preorder.lt_trans zero_lt_one h)
+
+theorem mul_le_mul_of_nonneg_left {a b c : R} (h : a ≤ b) (h' : 0 ≤ c) : c * a ≤ c * b := by
+  rw [PartialOrder.le_iff_lt_or_eq] at h'
+  cases h' with
+  | inl h' =>
+    have p := mul_lt_mul_of_pos_left (a := a) (b := b) (c := c)
+    rw [PartialOrder.le_iff_lt_or_eq] at h
+    cases h with
+    | inl h => exact Preorder.le_of_lt (p h h')
+    | inr h => subst h; exact Preorder.le_refl (c * a)
+  | inr h' => subst h'; simp [Semiring.zero_mul, Preorder.le_refl]
+
+theorem mul_le_mul_of_nonneg_right {a b c : R} (h : a ≤ b) (h' : 0 ≤ c) : a * c ≤ b * c := by
+  rw [PartialOrder.le_iff_lt_or_eq] at h'
+  cases h' with
+  | inl h' =>
+    have p := mul_lt_mul_of_pos_right (a := a) (b := b) (c := c)
+    rw [PartialOrder.le_iff_lt_or_eq] at h
+    cases h with
+    | inl h => exact Preorder.le_of_lt (p h h')
+    | inr h => subst h; exact Preorder.le_refl (a * c)
+  | inr h' => subst h'; simp [Semiring.mul_zero, Preorder.le_refl]
+
+theorem mul_le_mul_of_nonpos_left {a b c : R} (h : a ≤ b) (h' : c ≤ 0) : c * b ≤ c * a := by
+  have := mul_le_mul_of_nonneg_left h (IntModule.IsOrdered.neg_nonneg_iff.mpr h')
+  rwa [Ring.neg_mul, Ring.neg_mul, IntModule.IsOrdered.neg_le_iff, IntModule.neg_neg] at this
+
+theorem mul_le_mul_of_nonpos_right {a b c : R} (h : a ≤ b) (h' : c ≤ 0) : b * c ≤ a * c := by
+  have := mul_le_mul_of_nonneg_right h (IntModule.IsOrdered.neg_nonneg_iff.mpr h')
+  rwa [Ring.mul_neg, Ring.mul_neg, IntModule.IsOrdered.neg_le_iff, IntModule.neg_neg] at this
+
+theorem mul_lt_mul_of_neg_left {a b c : R} (h : a < b) (h' : c < 0) : c * b < c * a := by
+  have := mul_lt_mul_of_pos_left h (IntModule.IsOrdered.neg_pos_iff.mpr h')
+  rwa [Ring.neg_mul, Ring.neg_mul, IntModule.IsOrdered.neg_lt_iff, IntModule.neg_neg] at this
+
+theorem mul_lt_mul_of_neg_right {a b c : R} (h : a < b) (h' : c < 0) : b * c < a * c := by
+  have := mul_lt_mul_of_pos_right h (IntModule.IsOrdered.neg_pos_iff.mpr h')
+  rwa [Ring.mul_neg, Ring.mul_neg, IntModule.IsOrdered.neg_lt_iff, IntModule.neg_neg] at this
+
+theorem mul_nonneg {a b : R} (h₁ : 0 ≤ a) (h₂ : 0 ≤ b) : 0 ≤ a * b := by
+  simpa [Semiring.zero_mul] using mul_le_mul_of_nonneg_right h₁ h₂
+
+theorem mul_nonneg_of_nonpos_of_nonpos {a b : R} (h₁ : a ≤ 0) (h₂ : b ≤ 0) : 0 ≤ a * b := by
+  have := mul_nonneg (IntModule.IsOrdered.neg_nonneg_iff.mpr h₁) (IntModule.IsOrdered.neg_nonneg_iff.mpr h₂)
+  simpa [Ring.neg_mul, Ring.mul_neg, Ring.neg_neg] using this
+
+theorem mul_nonpos_of_nonneg_of_nonpos {a b : R} (h₁ : 0 ≤ a) (h₂ : b ≤ 0) : a * b ≤ 0 := by
+  rw [← IntModule.IsOrdered.neg_nonneg_iff, ← Ring.mul_neg]
+  apply mul_nonneg h₁ (IntModule.IsOrdered.neg_nonneg_iff.mpr h₂)
+
+theorem mul_nonpos_of_nonpos_of_nonneg {a b : R} (h₁ : a ≤ 0) (h₂ : 0 ≤ b) : a * b ≤ 0 := by
+  rw [← IntModule.IsOrdered.neg_nonneg_iff, ← Ring.neg_mul]
+  apply mul_nonneg (IntModule.IsOrdered.neg_nonneg_iff.mpr h₁) h₂
+
+theorem mul_pos {a b : R} (h₁ : 0 < a) (h₂ : 0 < b) : 0 < a * b := by
+  simpa [Semiring.zero_mul] using mul_lt_mul_of_pos_right h₁ h₂
+
+theorem mul_pos_of_neg_of_neg {a b : R} (h₁ : a < 0) (h₂ : b < 0) : 0 < a * b := by
+  have := mul_pos (IntModule.IsOrdered.neg_pos_iff.mpr h₁) (IntModule.IsOrdered.neg_pos_iff.mpr h₂)
+  simpa [Ring.neg_mul, Ring.mul_neg, Ring.neg_neg] using this
+
+theorem mul_neg_of_pos_of_neg {a b : R} (h₁ : 0 < a) (h₂ : b < 0) : a * b < 0 := by
+  rw [← IntModule.IsOrdered.neg_pos_iff, ← Ring.mul_neg]
+  apply mul_pos h₁ (IntModule.IsOrdered.neg_pos_iff.mpr h₂)
+
+theorem mul_neg_of_neg_of_pos {a b : R} (h₁ : a < 0) (h₂ : 0 < b) : a * b < 0 := by
+  rw [← IntModule.IsOrdered.neg_pos_iff, ← Ring.neg_mul]
+  apply mul_pos (IntModule.IsOrdered.neg_pos_iff.mpr h₁) h₂
+
+end PartialOrder
+
+section LinearOrder
+
+variable [LinearOrder R] [Ring.IsOrdered R]
+
+theorem mul_nonneg_iff {a b : R} : 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 := by
+  rcases LinearOrder.trichotomy 0 a with (ha | rfl | ha)
+  · rcases LinearOrder.trichotomy 0 b with (hb | rfl | hb)
+    · simp [Preorder.le_of_lt ha, Preorder.le_of_lt hb, mul_nonneg]
+    · simp [Semiring.mul_zero, Preorder.le_refl, LinearOrder.le_total]
+    · have m : a * b < 0 := mul_neg_of_pos_of_neg ha hb
+      simp [Preorder.le_of_lt ha, Preorder.le_of_lt hb, Preorder.not_ge_of_lt m,
+        Preorder.not_ge_of_lt ha, Preorder.not_ge_of_lt hb]
+  · simp [Semiring.zero_mul, Preorder.le_refl, LinearOrder.le_total]
+  · rcases LinearOrder.trichotomy 0 b with (hb | rfl | hb)
+    · have m : a * b < 0 := mul_neg_of_neg_of_pos ha hb
+      simp [Preorder.le_of_lt ha, Preorder.le_of_lt hb, Preorder.not_ge_of_lt m,
+        Preorder.not_ge_of_lt ha, Preorder.not_ge_of_lt hb]
+    · simp [Semiring.mul_zero, Preorder.le_refl, LinearOrder.le_total]
+    · simp [Preorder.le_of_lt ha, Preorder.le_of_lt hb, mul_nonneg_of_nonpos_of_nonpos]
+
+theorem mul_pos_iff {a b : R} : 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0 := by
+  rcases LinearOrder.trichotomy 0 a with (ha | rfl | ha)
+  · rcases LinearOrder.trichotomy 0 b with (hb | rfl | hb)
+    · simp [ha, hb, mul_pos]
+    · simp [Preorder.lt_irrefl, Semiring.mul_zero]
+    · have m : a * b < 0 := mul_neg_of_pos_of_neg ha hb
+      simp [ha, hb, Preorder.not_gt_of_lt m,
+        Preorder.not_gt_of_lt ha, Preorder.not_gt_of_lt hb]
+  · simp [Preorder.lt_irrefl, Semiring.zero_mul]
+  · rcases LinearOrder.trichotomy 0 b with (hb | rfl | hb)
+    · have m : a * b < 0 := mul_neg_of_neg_of_pos ha hb
+      simp [ha, hb, Preorder.not_gt_of_lt m,
+        Preorder.not_gt_of_lt ha, Preorder.not_gt_of_lt hb]
+    · simp [Preorder.lt_irrefl, Semiring.mul_zero]
+    · simp [ha, hb, mul_pos_of_neg_of_neg]
+
+theorem sq_nonneg {a : R} : 0 ≤ a^2 := by
+  rw [Semiring.pow_two, mul_nonneg_iff]
+  rcases LinearOrder.le_total 0 a with (h | h)
+  · exact .inl ⟨h, h⟩
+  · exact .inr ⟨h, h⟩
+
+theorem sq_pos {a : R} (h : a ≠ 0) : 0 < a^2 := by
+  rw [Semiring.pow_two, mul_pos_iff]
+  rcases LinearOrder.trichotomy 0 a with (h' | rfl | h')
+  · exact .inl ⟨h', h'⟩
+  · simp at h
+  · exact .inr ⟨h', h'⟩
+
+end LinearOrder
+
+end Ring.IsOrdered
+
+end Lean.Grind

src/Init/Grind/Tactics.lean

@@ -30,6 +30,7 @@ syntax grindIntro  := &"intro "
 syntax grindExt    := &"ext "
 syntax grindMod := grindEqBoth <|> grindEqRhs <|> grindEq <|> grindEqBwd <|> grindBwd <|> grindFwd <|> grindRL <|> grindLR <|> grindUsr <|> grindCasesEager <|> grindCases <|> grindIntro <|> grindExt
 syntax (name := grind) "grind" (grindMod)? : attr
+syntax (name := grind?) "grind?" (grindMod)? : attr
 end Attr
 end Lean.Parser
 
@@ -67,8 +68,6 @@ structure Config where
   if the implication is true. Otherwise, it will split only if `p` is an arithmetic predicate.
   -/
   splitImp : Bool := false
-  /-- By default, `grind` halts as soon as it encounters a sub-goal where no further progress can be made. -/
-  failures : Nat := 1
   /-- Maximum number of heartbeats (in thousands) the canonicalizer can spend per definitional equality test. -/
   canonHeartbeats : Nat := 1000
   /-- If `ext` is `true`, `grind` uses extensionality theorems that have been marked with `[grind ext]`. -/
@@ -98,7 +97,7 @@ structure Config where
   This approach is cheaper but incomplete. -/
   qlia : Bool := false
   /--
-  If `mbtc` is `true`, `grind` will use model-based theory commbination for creating new case splits.
+  If `mbtc` is `true`, `grind` will use model-based theory combination for creating new case splits.
   See paper "Model-based Theory Combination" for details.
   -/
   mbtc : Bool := true

src/Init/Meta.lean

@@ -1317,7 +1317,7 @@ test with the predicate `p`. The resulting array contains the tested elements fo
 `true`, separated by the corresponding separator elements.
 -/
 def filterSepElems (a : Array Syntax) (p : Syntax → Bool) : Array Syntax :=
-  Id.run <| a.filterSepElemsM p
+  Id.run <| a.filterSepElemsM (pure <| p ·)
 
 private partial def mapSepElemsMAux {m : Type → Type} [Monad m] (a : Array Syntax) (f : Syntax → m Syntax) (i : Nat) (acc : Array Syntax) : m (Array Syntax) := do
   if h : i < a.size then
@@ -1334,7 +1334,7 @@ def mapSepElemsM {m : Type → Type} [Monad m] (a : Array Syntax) (f : Syntax
   mapSepElemsMAux a f 0 #[]
 
 def mapSepElems (a : Array Syntax) (f : Syntax → Syntax) : Array Syntax :=
-  Id.run <| a.mapSepElemsM f
+  Id.run <| a.mapSepElemsM (pure <| f ·)
 
 end Array
 

src/Init/MetaTypes.lean

@@ -244,6 +244,11 @@ structure Config where
   `let x := v; e` simplifies to `e` when `x` does not occur in `e`.
   -/
   zetaUnused : Bool := true
+  /--
+  When `true` (default : `true`), then simps will catch runtime exceptions and
+  convert them into `simp` exceptions.
+  -/
+  catchRuntime : Bool := true
   deriving Inhabited, BEq
 
 -- Configuration object for `simp_all`

src/Lean/Compiler/IR/EmitC.lean

@@ -497,8 +497,13 @@ def emitNumLit (t : IRType) (v : Nat) : M Unit := do
   else
     if v < UInt32.size then
       emit v
+    else if t == .usize then
+      emit "((size_t)"
+      emit v
+      emit "ULL)"
     else
-      emit v; emit "ULL"
+      emit v
+      emit "ULL"
 
 def emitLit (z : VarId) (t : IRType) (v : LitVal) : M Unit := do
   emitLhs z;

src/Lean/Compiler/IR/ToIR.lean

@@ -70,7 +70,7 @@ def lowerLitValue (v : LCNF.LitValue) : LitVal :=
   | .uint8 v => .num (UInt8.toNat v)
   | .uint16 v => .num (UInt16.toNat v)
   | .uint32 v => .num (UInt32.toNat v)
-  | .uint64 v => .num (UInt64.toNat v)
+  | .uint64 v | .usize v => .num (UInt64.toNat v)
 
 -- TODO: This should be cached.
 def lowerEnumToScalarType (name : Name) : M (Option IRType) := do

src/Lean/Compiler/LCNF/Basic.lean

@@ -40,7 +40,9 @@ inductive LitValue where
   | uint16 (val : UInt16)
   | uint32 (val : UInt32)
   | uint64 (val : UInt64)
-  -- TODO: add constructors for `Int`, `Float`, `USize` ...
+  -- USize has a maximum size of 64 bits
+  | usize (val : UInt64)
+  -- TODO: add constructors for `Int`, `Float`, ...
   deriving Inhabited, BEq, Hashable
 
 def LitValue.toExpr : LitValue → Expr
@@ -50,6 +52,7 @@ def LitValue.toExpr : LitValue → Expr
   | .uint16 v => .app (.const ``UInt16.ofNat []) (.lit (.natVal (UInt16.toNat v)))
   | .uint32 v => .app (.const ``UInt32.ofNat []) (.lit (.natVal (UInt32.toNat v)))
   | .uint64 v => .app (.const ``UInt64.ofNat []) (.lit (.natVal (UInt64.toNat v)))
+  | .usize v => .app (.const ``USize.ofNat []) (.lit (.natVal (UInt64.toNat v)))
 
 inductive Arg where
   | erased

src/Lean/Compiler/LCNF/ElimDeadBranches.lean

@@ -177,7 +177,7 @@ def ofLCNFLit : LCNF.LitValue → Value
 | .uint8 v => ofNat (UInt8.toNat v)
 | .uint16 v => ofNat (UInt16.toNat v)
 | .uint32 v => ofNat (UInt32.toNat v)
-| .uint64 v => ofNat (UInt64.toNat v)
+| .uint64 v | .usize v => ofNat (UInt64.toNat v)
 
 partial def proj : Value → Nat → Value
 | .ctor _ vs , i => vs.getD i bot

src/Lean/Compiler/LCNF/ExtractClosed.lean

@@ -0,0 +1,156 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Cameron Zwarich
+-/
+prelude
+import Lean.Compiler.ClosedTermCache
+import Lean.Compiler.NeverExtractAttr
+import Lean.Compiler.LCNF.Basic
+import Lean.Compiler.LCNF.InferType
+import Lean.Compiler.LCNF.Internalize
+import Lean.Compiler.LCNF.MonoTypes
+import Lean.Compiler.LCNF.PassManager
+import Lean.Compiler.LCNF.ToExpr
+
+namespace Lean.Compiler.LCNF
+namespace ExtractClosed
+
+abbrev ExtractM := StateRefT (Array CodeDecl) CompilerM
+
+mutual
+
+partial def extractLetValue (v : LetValue) : ExtractM Unit := do
+  match v with
+  | .const _ _ args => args.forM extractArg
+  | .fvar fnVar args =>
+    extractFVar fnVar
+    args.forM extractArg
+  | .proj _ _ baseVar => extractFVar baseVar
+  | .lit _ | .erased => return ()
+
+partial def extractArg (arg : Arg) : ExtractM Unit := do
+  match arg with
+  | .fvar fvarId => extractFVar fvarId
+  | .type _ | .erased => return ()
+
+partial def extractFVar (fvarId : FVarId) : ExtractM Unit := do
+  if let some letDecl ← findLetDecl? fvarId then
+    modify fun decls => decls.push (.let letDecl)
+    extractLetValue letDecl.value
+
+end
+
+def isIrrelevantArg (arg : Arg) : Bool :=
+  match arg with
+  | .erased | .type _ => true
+  | .fvar _ => false
+
+structure Context where
+  baseName : Name
+  sccDecls : Array Decl
+
+structure State where
+  decls : Array Decl := {}
+
+abbrev M := ReaderT Context $ StateRefT State CompilerM
+
+mutual
+
+partial def shouldExtractLetValue (isRoot : Bool) (v : LetValue) : M Bool := do
+  match v with
+  | .lit (.str _) => return true
+  | .lit (.nat v) =>
+    -- The old compiler's implementation used the runtime's `is_scalar` function, which
+    -- introduces a dependency on the architecture used by the compiler.
+    return v >= Nat.pow 2 63
+  | .lit _ | .erased => return !isRoot
+  | .const name _ args =>
+    if (← read).sccDecls.any (·.name == name) then
+      return false
+    if hasNeverExtractAttribute (← getEnv) name then
+      return false
+    if isRoot then
+      if let some constInfo := (← getEnv).find? name then
+        let shouldExtract := match constInfo with
+        | .defnInfo val => val.type.isForall
+        | .ctorInfo _ => !(args.all isIrrelevantArg)
+        | _ => true
+        if !shouldExtract then
+          return false
+    args.allM shouldExtractArg
+  | .fvar fnVar args => return (← shouldExtractFVar fnVar) && (← args.allM shouldExtractArg)
+  | .proj _ _ baseVar => shouldExtractFVar baseVar
+
+partial def shouldExtractArg (arg : Arg) : M Bool := do
+  match arg with
+  | .fvar fvarId => shouldExtractFVar fvarId
+  | .type _ | .erased => return true
+
+partial def shouldExtractFVar (fvarId : FVarId) : M Bool := do
+  if let some letDecl ← findLetDecl? fvarId then
+    shouldExtractLetValue false letDecl.value
+  else
+    return false
+
+end
+
+mutual
+
+partial def visitCode (code : Code) : M Code := do
+  match code with
+  | .let decl k =>
+    if (← shouldExtractLetValue true decl.value) then
+      let ⟨_, decls⟩ ← extractLetValue decl.value |>.run {}
+      let decls := decls.reverse.push (.let decl)
+      let decls ← decls.mapM Internalize.internalizeCodeDecl |>.run' {}
+      let closedCode := attachCodeDecls decls (.return decls.back!.fvarId)
+      let closedExpr := closedCode.toExpr
+      let env ← getEnv
+      let name ← if let some closedTermName := getClosedTermName? env closedExpr then
+        eraseCode closedCode
+        pure closedTermName
+      else
+        let name := (← read).baseName ++ (`_closedTerm).appendIndexAfter (← get).decls.size
+        cacheClosedTermName env closedExpr name |> setEnv
+        let decl := { name, levelParams := [], type := decl.type, params := #[],
+                      value := .code closedCode, inlineAttr? := some .noinline }
+        decl.saveMono
+        modify fun s => { s with decls := s.decls.push decl }
+        pure name
+      let decl ← decl.updateValue (.const name [] #[])
+      return code.updateLet! decl (← visitCode k)
+    else
+      return code.updateLet! decl (← visitCode k)
+  | .fun decl k =>
+    let decl ← decl.updateValue (← visitCode decl.value)
+    return code.updateFun! decl (← visitCode k)
+  | .jp decl k =>
+    let decl ← decl.updateValue (← visitCode decl.value)
+    return code.updateFun! decl (← visitCode k)
+  | .cases cases =>
+    let alts ← cases.alts.mapM (fun alt => do return alt.updateCode (← visitCode alt.getCode))
+    return code.updateAlts! alts
+  | .jmp .. | .return _ | .unreach .. => return code
+
+end
+
+def visitDecl (decl : Decl) : M Decl := do
+  let value ← decl.value.mapCodeM visitCode
+  return { decl with value }
+
+end ExtractClosed
+
+partial def Decl.extractClosed (decl : Decl) (sccDecls : Array Decl) : CompilerM (Array Decl) := do
+  let ⟨decl, s⟩ ← ExtractClosed.visitDecl decl |>.run { baseName := decl.name, sccDecls } |>.run {}
+  return s.decls.push decl
+
+def extractClosed : Pass where
+  phase := .mono
+  name := `extractClosed
+  run := fun decls =>
+    decls.foldlM (init := #[]) fun newDecls decl => return newDecls ++ (← decl.extractClosed decls)
+
+builtin_initialize registerTraceClass `Compiler.extractClosed (inherited := true)
+
+end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/FVarUtil.lean

@@ -205,9 +205,9 @@ where
     if !(← f fvar) then failure
 
 def anyFVar [TraverseFVar α] (f : FVarId → Bool) (x : α) : Bool :=
-  Id.run <| anyFVarM f x
+  Id.run <| anyFVarM (pure <| f ·) x
 
 def allFVar [TraverseFVar α] (f : FVarId → Bool) (x : α) : Bool :=
-  Id.run <| allFVarM f x
+  Id.run <| allFVarM (pure <| f ·) x
 
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/InferType.lean

@@ -109,6 +109,7 @@ def inferLitValueType (value : LitValue) : Expr :=
   | .uint16 .. => mkConst ``UInt16
   | .uint32 .. => mkConst ``UInt32
   | .uint64 .. => mkConst ``UInt64
+  | .usize .. => mkConst ``USize
 
 mutual
   partial def inferArgType (arg : Arg) : InferTypeM Expr :=

src/Lean/Compiler/LCNF/Passes.lean

@@ -19,6 +19,7 @@ import Lean.Compiler.LCNF.FloatLetIn
 import Lean.Compiler.LCNF.ReduceArity
 import Lean.Compiler.LCNF.ElimDeadBranches
 import Lean.Compiler.LCNF.StructProjCases
+import Lean.Compiler.LCNF.ExtractClosed
 
 namespace Lean.Compiler.LCNF
 
@@ -79,7 +80,8 @@ def builtinPassManager : PassManager := {
     simp (occurrence := 5) (phase := .mono),
     structProjCases,
     cse (occurrence := 2) (phase := .mono),
-    saveMono  -- End of mono phase
+    saveMono,  -- End of mono phase
+    extractClosed
   ]
 }
 

src/Lean/Compiler/LCNF/PhaseExt.lean

@@ -13,7 +13,8 @@ abbrev DeclExtState := PHashMap Name Decl
 private abbrev declLt (a b : Decl) :=
   Name.quickLt a.name b.name
 
-private abbrev sortDecls (decls : Array Decl) : Array Decl :=
+private def sortedDecls (s : DeclExtState) : Array Decl :=
+  let decls := s.foldl (init := #[]) fun ps _ v => ps.push v
   decls.qsort declLt
 
 private abbrev findAtSorted? (decls : Array Decl) (declName : Name) : Option Decl :=
@@ -21,17 +22,28 @@ private abbrev findAtSorted? (decls : Array Decl) (declName : Name) : Option Dec
   let tmpDecl := { tmpDecl with name := declName }
   decls.binSearch tmpDecl declLt
 
-abbrev DeclExt := SimplePersistentEnvExtension Decl DeclExtState
+def DeclExt := PersistentEnvExtension Decl Decl DeclExtState
 
-def mkDeclExt (name : Name := by exact decl_name%) : IO DeclExt := do
-  registerSimplePersistentEnvExtension {
-    name            := name
-    addImportedFn   := fun _ => {}
-    addEntryFn      := fun decls decl => decls.insert decl.name decl
-    toArrayFn       := (sortDecls ·.toArray)
-    asyncMode       := .sync  -- compilation is non-parallel anyway
-    replay?         := some <| SimplePersistentEnvExtension.replayOfFilter
-      (fun s d => !s.contains d.name) (fun decls decl => decls.insert decl.name decl)
+instance : Inhabited DeclExt :=
+  inferInstanceAs (Inhabited (PersistentEnvExtension Decl Decl DeclExtState))
+
+def mkDeclExt (name : Name := by exact decl_name%) : IO DeclExt :=
+  registerPersistentEnvExtension {
+    name,
+    mkInitial := pure {},
+    addImportedFn := fun _ => pure {},
+    addEntryFn := fun s decl => s.insert decl.name decl
+    exportEntriesFn := sortedDecls
+    statsFn := fun s =>
+      let numEntries := s.foldl (init := 0) (fun count _ _ => count + 1)
+      format "number of local entries: " ++ format numEntries
+    asyncMode := .sync,
+    replay? := some <| fun oldState newState _ otherState =>
+      newState.foldl (init := otherState) fun otherState k v =>
+        if oldState.contains k then
+          otherState
+        else
+          otherState.insert k v
   }
 
 builtin_initialize baseExt : DeclExt ← mkDeclExt

src/Lean/Compiler/LCNF/PrettyPrinter.lean

@@ -58,7 +58,7 @@ def ppArgs (args : Array Arg) : M Format := do
 
 def ppLitValue (lit : LitValue) : M Format := do
   match lit with
-  | .nat v | .uint8 v | .uint16 v | .uint32 v | .uint64 v => return format v
+  | .nat v | .uint8 v | .uint16 v | .uint32 v | .uint64 v | .usize v => return format v
   | .str v => return format (repr v)
 
 def ppLetValue (e : LetValue) : M Format := do

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

@@ -368,6 +368,7 @@ def conversionFolders : List (Name × Folder) := [
   (``UInt16.ofNat, Folder.ofNat (fun v => .uint16 (UInt16.ofNat v))),
   (``UInt32.ofNat, Folder.ofNat (fun v => .uint32 (UInt32.ofNat v))),
   (``UInt64.ofNat, Folder.ofNat (fun v => .uint64 (UInt64.ofNat v))),
+  (``USize.ofNat, Folder.ofNat (fun v => .usize (UInt64.ofNat v))),
 ]
 
 /--

src/Lean/Compiler/LCNF/StructProjCases.lean

@@ -31,11 +31,11 @@ def mkFieldParamsForCtorType (e : Expr) (numParams : Nat): CompilerM (Array Para
     | _ => return params
   loop #[] e numParams
 
-structure StructProjState where
+structure State where
   projMap : Std.HashMap FVarId (Array FVarId) := {}
   fvarMap : Std.HashMap FVarId FVarId := {}
 
-abbrev M := StateRefT StructProjState CompilerM
+abbrev M := StateRefT State CompilerM
 
 def M.run (x : M α) : CompilerM α := do
   x.run' {}
@@ -128,4 +128,6 @@ end StructProjCases
 def structProjCases : Pass :=
   .mkPerDeclaration `structProjCases (StructProjCases.visitDecl · |>.run) .mono
 
+builtin_initialize registerTraceClass `Compiler.structProjCases (inherited := true)
+
 end Lean.Compiler.LCNF

src/Lean/Data/AssocList.lean

@@ -38,7 +38,7 @@ def isEmpty : AssocList α β → Bool
     foldlM f d es
 
 @[inline] def foldl (f : δ → α → β → δ) (init : δ) (as : AssocList α β) : δ :=
-  Id.run (foldlM f init as)
+  Id.run (foldlM (pure <| f · · ·) init as)
 
 def toList (as : AssocList α β) : List (α × β) :=
   as.foldl (init := []) (fun r a b => (a, b)::r) |>.reverse

src/Lean/Data/NameTrie.lean

@@ -75,9 +75,9 @@ def NameTrie.forM [Monad m] (t : NameTrie β) (f : β → m Unit) : m Unit :=
   t.forMatchingM Name.anonymous f
 
 def NameTrie.matchingToArray (t : NameTrie β) (k : Name) : Array β :=
-  Id.run <| t.foldMatchingM k #[] fun v acc => acc.push v
+  Id.run <| t.foldMatchingM k #[] fun v acc => return acc.push v
 
 def NameTrie.toArray (t : NameTrie β) : Array β :=
-  Id.run <| t.foldM #[] fun v acc => acc.push v
+  Id.run <| t.foldM #[] fun v acc => return acc.push v
 
 end Lean

src/Lean/Data/PersistentArray.lean

@@ -281,10 +281,10 @@ instance : ForIn m (PersistentArray α) α where
 end
 
 @[inline] def foldl (t : PersistentArray α) (f : β → α → β) (init : β) (start : Nat := 0) : β :=
-  Id.run <| t.foldlM f init start
+  Id.run <| t.foldlM (pure <| f · ·) init start
 
 @[inline] def foldr (t : PersistentArray α) (f : α → β → β) (init : β) : β :=
-  Id.run <| t.foldrM f init
+  Id.run <| t.foldrM (pure <| f · ·) init
 
 @[inline] def filter (as : PersistentArray α) (p : α → Bool) : PersistentArray α :=
   as.foldl (init := {}) fun asNew a => if p a then asNew.push a else asNew
@@ -301,10 +301,10 @@ def append (t₁ t₂ : PersistentArray α) : PersistentArray α :=
 instance : Append (PersistentArray α) := ⟨append⟩
 
 @[inline] def findSome? {β} (t : PersistentArray α) (f : α → (Option β)) : Option β :=
-  Id.run $ t.findSomeM? f
+  Id.run $ t.findSomeM? (pure <| f ·)
 
 @[inline] def findSomeRev? {β} (t : PersistentArray α) (f : α → (Option β)) : Option β :=
-  Id.run $ t.findSomeRevM? f
+  Id.run $ t.findSomeRevM? (pure <| f ·)
 
 def toList (t : PersistentArray α) : List α :=
   (t.foldl (init := []) fun xs x => x :: xs).reverse
@@ -325,7 +325,7 @@ variable {m : Type → Type w} [Monad m]
 end
 
 @[inline] def any (a : PersistentArray α) (p : α → Bool) : Bool :=
-  Id.run $ anyM a p
+  Id.run $ anyM a (pure <| p ·)
 
 @[inline] def all (a : PersistentArray α) (p : α → Bool) : Bool :=
   !any a fun v => !p v
@@ -346,7 +346,7 @@ variable {β : Type u}
 end
 
 @[inline] def map {β} (f : α → β) (t : PersistentArray α) : PersistentArray β :=
-  Id.run $ t.mapM f
+  Id.run $ t.mapM (pure <| f ·)
 
 structure Stats where
   numNodes : Nat

src/Lean/Data/PersistentHashMap.lean

@@ -288,7 +288,7 @@ def forM {_ : BEq α} {_ : Hashable α} (map : PersistentHashMap α β) (f : α
   map.foldlM (fun _ => f) ⟨⟩
 
 def foldl {_ : BEq α} {_ : Hashable α} (map : PersistentHashMap α β) (f : σ → α → β → σ) (init : σ) : σ :=
-  Id.run <| map.foldlM f init
+  Id.run <| map.foldlM (pure <| f · · ·) init
 
 protected def forIn {_ : BEq α} {_ : Hashable α} [Monad m]
     (map : PersistentHashMap α β) (init : σ) (f : α × β → σ → m (ForInStep σ)) : m σ := do
@@ -322,7 +322,7 @@ def mapM {α : Type u} {β : Type v} {σ : Type u} {m : Type u → Type w} [Mona
   return { root }
 
 def map {α : Type u} {β : Type v} {σ : Type u} {_ : BEq α} {_ : Hashable α} (pm : PersistentHashMap α β) (f : β → σ) : PersistentHashMap α σ :=
-  Id.run <| pm.mapM f
+  Id.run <| pm.mapM (pure <| f ·)
 
 def toList {_ : BEq α} {_ : Hashable α} (m : PersistentHashMap α β) : List (α × β) :=
   m.foldl (init := []) fun ps k v => (k, v) :: ps

src/Lean/Data/PersistentHashSet.lean

@@ -48,7 +48,7 @@ variable {_ : BEq α} {_ : Hashable α}
   s.set.foldlM (init := init) fun d a _ => f d a
 
 @[inline] def fold {β : Type v} (f : β → α → β) (init : β) (s : PersistentHashSet α) : β :=
-  Id.run $ s.foldM f init
+  Id.run $ s.foldM (pure <| f · ·) init
 
 def toList (s : PersistentHashSet α) : List α :=
   s.set.toList.map (·.1)

src/Lean/Elab/App.lean

@@ -1146,8 +1146,11 @@ inductive LValResolution where
   The `fullName` is the name of the recursive function, and `baseName` is the base name of the type to search for in the parameter list. -/
   | localRec (baseName : Name) (fullName : Name) (fvar : Expr)
 
-private def throwLValError (e : Expr) (eType : Expr) (msg : MessageData) : TermElabM α :=
-  throwError "{msg}{indentExpr e}\nhas type{indentExpr eType}"
+private def throwLValErrorAt (ref : Syntax) (e : Expr) (eType : Expr) (msg : MessageData) : TermElabM α :=
+  throwErrorAt ref "{msg}{indentExpr e}\nhas type{indentExpr eType}"
+
+private def throwLValError (e : Expr) (eType : Expr) (msg : MessageData) : TermElabM α := do
+  throwLValErrorAt (← getRef) e eType msg
 
 /--
 `findMethod? S fName` tries the for each namespace `S'` in the resolution order for `S` to resolve the name `S'.fname`.
@@ -1206,7 +1209,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
           return LValResolution.projIdx structName (idx - 1)
       else
         throwLValError e eType m!"invalid projection, structure has only {numFields} field(s)"
-  | some structName, LVal.fieldName _ fieldName _ _ =>
+  | some structName, LVal.fieldName _ fieldName _ fullRef =>
     let env ← getEnv
     if isStructure env structName then
       if let some baseStructName := findField? env structName (Name.mkSimple fieldName) then
@@ -1223,10 +1226,10 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
     if let some (baseStructName, fullName) ← findMethod? structName (.mkSimple fieldName) then
       return LValResolution.const baseStructName structName fullName
     let msg := mkUnknownIdentifierMessage m!"invalid field '{fieldName}', the environment does not contain '{Name.mkStr structName fieldName}'"
-    throwLValError e eType msg
-  | none, LVal.fieldName _ _ (some suffix) _ =>
+    throwLValErrorAt fullRef e eType msg
+  | none, LVal.fieldName _ _ (some suffix) fullRef =>
     if e.isConst then
-      throwUnknownConstant (e.constName! ++ suffix)
+      throwUnknownConstantAt fullRef (e.constName! ++ suffix)
     else
       throwInvalidFieldNotation e eType
   | _, _ => throwInvalidFieldNotation e eType
@@ -1511,7 +1514,7 @@ where
       else if let some (fvar, []) ← resolveLocalName idNew then
         return fvar
       else
-        throwUnknownIdentifier m!"invalid dotted identifier notation, unknown identifier `{idNew}` from expected type{indentExpr expectedType}"
+        throwUnknownIdentifierAt id m!"invalid dotted identifier notation, unknown identifier `{idNew}` from expected type{indentExpr expectedType}"
     catch
       | ex@(.error ..) =>
         match (← unfoldDefinition? resultType) with

src/Lean/Elab/Declaration.lean

@@ -311,7 +311,7 @@ def elabMutual : CommandElab := fun stx => do
         if (← Simp.isBuiltinSimproc name) then
           pure [name]
         else
-          throwUnknownConstant name
+          throwUnknownConstantAt ident name
     let declName ← ensureNonAmbiguous ident declNames
     Term.applyAttributes declName attrs
     for attrName in toErase do

src/Lean/Elab/Extra.lean

@@ -209,14 +209,14 @@ where
         | none => processLeaf s
 
   processBinOp (ref : Syntax) (kind : BinOpKind) (f lhs rhs : Syntax) := do
-    let some f ← resolveId? f | throwUnknownConstant f.getId
+    let some f ← resolveId? f | throwUnknownConstantAt f f.getId
     -- treat corresponding argument as leaf for `leftact/rightact`
     let lhs ← if kind == .leftact then processLeaf lhs else go lhs
     let rhs ← if kind == .rightact then processLeaf rhs else go rhs
     return .binop ref kind f lhs rhs
 
   processUnOp (ref : Syntax) (f arg : Syntax) := do
-    let some f ← resolveId? f | throwUnknownConstant f.getId
+    let some f ← resolveId? f | throwUnknownConstantAt f f.getId
     return .unop ref f (← go arg)
 
   processLeaf (s : Syntax) := do
@@ -547,7 +547,7 @@ def elabBinRelCore (noProp : Bool) (stx : Syntax) (expectedType? : Option Expr)
       let result ← toExprCore (← applyCoe tree maxType (isPred := true))
       trace[Elab.binrel] "result: {result}"
       return result
-  | none   => throwUnknownConstant stx[1].getId
+  | none   => throwUnknownConstantAt stx[1] stx[1].getId
 where
   /-- If `noProp == true` and `e` has type `Prop`, then coerce it to `Bool`. -/
   toBoolIfNecessary (e : Expr) : TermElabM Expr := do

src/Lean/Elab/Tactic/Grind.lean

@@ -141,7 +141,7 @@ def grind
     let type ← mvarId.getType
     let mvar' ← mkFreshExprSyntheticOpaqueMVar type
     let result ← Grind.main mvar'.mvarId! params fallback
-    if result.hasFailures then
+    if result.hasFailed then
       throwError "`grind` failed\n{← result.toMessageData}"
     -- `grind` proofs are often big
     let e ← if (← isProp type) then

src/Lean/Elab/Tactic/Simp.lean

@@ -202,7 +202,7 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
                   if (← Simp.isBuiltinSimproc name) then
                     simprocs := simprocs.erase name
                   else
-                    withRef id <| throwUnknownConstant name
+                    throwUnknownConstantAt id name
             else if arg.getKind == ``Lean.Parser.Tactic.simpLemma then
               let post :=
                 if arg[0].isNone then

src/Lean/Elab/Term.lean

@@ -1979,7 +1979,7 @@ where
            isValidAutoBoundImplicitName n (relaxedAutoImplicit.get (← getOptions)) then
         throwAutoBoundImplicitLocal n
       else
-        throwUnknownIdentifier m!"unknown identifier '{Lean.mkConst n}'"
+        throwUnknownIdentifierAt stx m!"unknown identifier '{Lean.mkConst n}'"
     mkConsts candidates explicitLevels
 
 /--

src/Lean/Environment.lean

@@ -454,6 +454,9 @@ private partial def AsyncConsts.findRec? (aconsts : AsyncConsts) (declName : Nam
   let c ← aconsts.findPrefix? declName
   if c.constInfo.name == declName then
     return c
+  -- If privacy is the only difference between `declName` and `findPrefix?` result, we can assume
+  -- `declName` does not exist according to the `add` invariant
+  guard <| privateToUserName c.constInfo.name != privateToUserName declName
   let aconsts ← c.consts.get.get? AsyncConsts
   AsyncConsts.findRec? aconsts declName
 

src/Lean/Exception.lean

@@ -76,28 +76,43 @@ prompt the code action.
 -/
 def unknownIdentifierMessageTag : Name := `unknownIdentifier
 
+/-- Throw an error exception using the given message data and reference syntax. -/
+protected def throwErrorAt [Monad m] [MonadError m] (ref : Syntax) (msg : MessageData) : m α := do
+  withRef ref <| Lean.throwError msg
+
 /--
 Creates a `MessageData` that is tagged with `unknownIdentifierMessageTag`.
 This tag is used by the 'import unknown identifier' code action to detect messages that should
 prompt the code action.
+The end position of the range of an unknown identifier message should always point at the end of the
+unknown identifier.
 -/
 def mkUnknownIdentifierMessage (msg : MessageData) : MessageData :=
   MessageData.tagged unknownIdentifierMessageTag msg
 
 /--
 Throw an unknown identifier error message that is tagged with `unknownIdentifierMessageTag`.
+The end position of the range of `ref` should always point at the unknown identifier.
 See also `mkUnknownIdentifierMessage`.
 -/
-def throwUnknownIdentifier [Monad m] [MonadError m] (msg : MessageData) : m α :=
-  Lean.throwError <| mkUnknownIdentifierMessage msg
+def throwUnknownIdentifierAt [Monad m] [MonadError m] (ref : Syntax) (msg : MessageData) : m α :=
+  Lean.throwErrorAt ref <| mkUnknownIdentifierMessage msg
 
-/-- Throw an unknown constant error message. -/
-def throwUnknownConstant [Monad m] [MonadError m] (constName : Name) : m α :=
-  throwUnknownIdentifier m!"unknown constant '{.ofConstName constName}'"
+/--
+Throw an unknown constant error message.
+The end position of the range of `ref` should point at the unknown identifier.
+See also `mkUnknownIdentifierMessage`.
+-/
+def throwUnknownConstantAt [Monad m] [MonadError m] (ref : Syntax) (constName : Name) : m α := do
+  throwUnknownIdentifierAt ref m!"unknown constant '{.ofConstName constName}'"
 
-/-- Throw an error exception using the given message data and reference syntax. -/
-protected def throwErrorAt [Monad m] [MonadError m] (ref : Syntax) (msg : MessageData) : m α := do
-  withRef ref <| Lean.throwError msg
+/--
+Throw an unknown constant error message.
+The end position of the range of the current reference should point at the unknown identifier.
+See also `mkUnknownIdentifierMessage`.
+-/
+def throwUnknownConstant [Monad m] [MonadError m] (constName : Name) : m α := do
+  throwUnknownConstantAt (← getRef) constName
 
 /--
 Convert an `Except` into a `m` monadic action, where `m` is any monad that

src/Lean/Expr.lean

@@ -750,7 +750,7 @@ def mkStrLit (s : String) : Expr :=
 def mkAppN (f : Expr) (args : Array Expr) : Expr :=
   args.foldl mkApp f
 
-private partial def mkAppRangeAux (n : Nat) (args : Array Expr) (i : Nat) (e : Expr) : Expr :=
+private def mkAppRangeAux (n : Nat) (args : Array Expr) (i : Nat) (e : Expr) : Expr :=
   if i < n then mkAppRangeAux n args (i+1) (mkApp e args[i]!) else e
 
 /-- `mkAppRange f i j #[a_1, ..., a_i, ..., a_j, ... ]` ==> the expression `f a_i ... a_{j-1}` -/
@@ -1502,8 +1502,8 @@ abbrev PersistentExprStructMap (α : Type) := PHashMap ExprStructEq α
 
 namespace Expr
 
-private partial def mkAppRevRangeAux (revArgs : Array Expr) (start : Nat) (b : Expr) (i : Nat) : Expr :=
-  if i == start then b
+private def mkAppRevRangeAux (revArgs : Array Expr) (start : Nat) (b : Expr) (i : Nat) : Expr :=
+  if i ≤ start then b
   else
     let i := i - 1
     mkAppRevRangeAux revArgs start (mkApp b revArgs[i]!) i
@@ -1880,7 +1880,7 @@ def updateFn : Expr → Expr → Expr
 /--
 Eta reduction. If `e` is of the form `(fun x => f x)`, then return `f`.
 -/
-partial def eta (e : Expr) : Expr :=
+def eta (e : Expr) : Expr :=
   match e with
   | Expr.lam _ d b _ =>
     let b' := b.eta

src/Lean/Language/Basic.lean

@@ -82,6 +82,12 @@ structure SnapshotTask (α : Type) where
   `Syntax` processed by this `SnapshotTask`.
   The `Syntax` is used by the language server to determine whether to force this `SnapshotTask`
   when a request is made.
+  In general, the elaborator retains the following invariant:
+  If `stx?` is `none`, then this snapshot task (and all of its children) do not contain `InfoTree`
+  information that can be used in the language server, and so the language server will ignore it
+  when it is looking for an `InfoTree`.
+  Nonetheless, if `stx?` is `none`, then this snapshot task (and any of its children) may still
+  contain message log information.
   -/
   stx? : Option Syntax
   /--
@@ -309,7 +315,7 @@ def SnapshotTree.runAndReport (s : SnapshotTree) (opts : Options)
 
 /-- Waits on and returns all snapshots in the tree. -/
 def SnapshotTree.getAll (s : SnapshotTree) : Array Snapshot :=
-  Id.run <| s.foldM (·.push ·) #[]
+  Id.run <| s.foldM (pure <| ·.push ·) #[]
 
 /-- Returns a task that waits on all snapshots in the tree. -/
 def SnapshotTree.waitAll : SnapshotTree → BaseIO (Task Unit)

src/Lean/Language/Lean.lean

@@ -687,7 +687,8 @@ where
           -- create a temporary snapshot tree containing all tasks but it
           let snaps := #[
             { stx? := stx', task := elabPromise.result!.map (sync := true) toSnapshotTree, cancelTk? := none },
-            { stx? := stx', task := resultPromise.result!.map (sync := true) toSnapshotTree, cancelTk? := none }] ++
+            { stx? := stx', task := resultPromise.result!.map (sync := true) toSnapshotTree, cancelTk? := none },
+            { stx? := stx', task := finishedPromise.result!.map (sync := true) toSnapshotTree, cancelTk? := none }] ++
             cmdState.snapshotTasks
           let tree := SnapshotTree.mk { diagnostics := .empty } snaps
           BaseIO.bindTask (← tree.waitAll) fun _ => do

src/Lean/Level.lean

@@ -295,9 +295,10 @@ private def isAlreadyNormalizedCheap : Level → Bool
 
 /- Auxiliary function used at `normalize` -/
 private def mkIMaxAux : Level → Level → Level
-  | _,    zero => zero
-  | zero, u    => u
-  | u₁,   u₂   => if u₁ == u₂ then u₁ else mkLevelIMax u₁ u₂
+  | _,    zero   => zero
+  | zero, u      => u
+  | succ zero, u => u
+  | u₁,   u₂     => if u₁ == u₂ then u₁ else mkLevelIMax u₁ u₂
 
 /- Auxiliary function used at `normalize` -/
 @[specialize] private partial def getMaxArgsAux (normalize : Level → Level) : Level → Bool → Array Level → Array Level

src/Lean/LocalContext.lean

@@ -397,19 +397,19 @@ instance : ForIn m LocalContext LocalDecl where
     | some d => f d b
 
 @[inline] def foldl (lctx : LocalContext) (f : β → LocalDecl → β) (init : β) (start : Nat := 0) : β :=
-  Id.run <| lctx.foldlM f init start
+  Id.run <| lctx.foldlM (pure <| f · ·) init start
 
 @[inline] def foldr (lctx : LocalContext) (f : LocalDecl → β → β) (init : β) : β :=
-  Id.run <| lctx.foldrM f init
+  Id.run <| lctx.foldrM (pure <| f · ·) init
 
 def size (lctx : LocalContext) : Nat :=
   lctx.foldl (fun n _ => n+1) 0
 
 @[inline] def findDecl? (lctx : LocalContext) (f : LocalDecl → Option β) : Option β :=
-  Id.run <| lctx.findDeclM? f
+  Id.run <| lctx.findDeclM? (pure <| f ·)
 
 @[inline] def findDeclRev? (lctx : LocalContext) (f : LocalDecl → Option β) : Option β :=
-  Id.run <| lctx.findDeclRevM? f
+  Id.run <| lctx.findDeclRevM? (pure <| f ·)
 
 partial def isSubPrefixOfAux (a₁ a₂ : PArray (Option LocalDecl)) (exceptFVars : Array Expr) (i j : Nat) : Bool :=
   if h : i < a₁.size then
@@ -473,11 +473,11 @@ def mkForall (lctx : LocalContext) (xs : Array Expr) (b : Expr) : Expr :=
 
 /-- Return `true` if `lctx` contains a local declaration satisfying `p`. -/
 @[inline] def any (lctx : LocalContext) (p : LocalDecl → Bool) : Bool :=
-  Id.run <| lctx.anyM p
+  Id.run <| lctx.anyM (pure <| p ·)
 
 /-- Return `true` if all declarations in `lctx` satisfy `p`. -/
 @[inline] def all (lctx : LocalContext) (p : LocalDecl → Bool) : Bool :=
-  Id.run <| lctx.allM p
+  Id.run <| lctx.allM (pure <| p ·)
 
 /-- If option `pp.sanitizeNames` is set to `true`, add tombstone to shadowed local declaration names and ones contains macroscopes. -/
 def sanitizeNames (lctx : LocalContext) : StateM NameSanitizerState LocalContext := do

src/Lean/Meta/Basic.lean

@@ -1221,7 +1221,7 @@ private def getConstTemp? (constName : Name) : MetaM (Option ConstantInfo) := do
   | some (info@(ConstantInfo.thmInfo _))  => getTheoremInfo info
   | some (info@(ConstantInfo.defnInfo _)) => getDefInfoTemp info
   | some info                             => pure (some info)
-  | none                                  => throwUnknownConstant constName
+  | none                                  => throwUnknownConstantAt (← getRef) constName
 
 private def isClassQuickConst? (constName : Name) : MetaM (LOption Name) := do
   if isClass (← getEnv) constName then

src/Lean/Meta/Constructions/NoConfusion.lean

@@ -7,6 +7,13 @@ prelude
 import Lean.AddDecl
 import Lean.Meta.AppBuilder
 import Lean.Meta.CompletionName
+import Lean.Meta.Constructions.NoConfusionLinear
+
+
+register_builtin_option backwards.linearNoConfusionType : Bool := {
+  defValue := true
+  descr    := "use the linear-size construction for the `noConfusionType` declaration of an inductive type. Set to false to use the previous, simpler but quadratic-size construction. "
+}
 
 namespace Lean
 
@@ -21,12 +28,23 @@ def mkNoConfusionCore (declName : Name) : MetaM Unit := do
   let recInfo ← getConstInfo (mkRecName declName)
   unless recInfo.levelParams.length > indVal.levelParams.length do return
 
-  let name := Name.mkStr declName "noConfusionType"
-  let decl ← ofExceptKernelException (mkNoConfusionTypeCoreImp (← getEnv) declName)
-  addDecl decl
-  setReducibleAttribute name
-  modifyEnv fun env => addToCompletionBlackList env name
-  modifyEnv fun env => addProtected env name
+  let useLinear ←
+    if backwards.linearNoConfusionType.get (← getOptions) then
+      NoConfusionLinear.deps.allM (hasConst · (skipRealize := true))
+    else
+      pure false
+
+  if useLinear then
+    NoConfusionLinear.mkWithCtorType declName
+    NoConfusionLinear.mkWithCtor declName
+    NoConfusionLinear.mkNoConfusionTypeLinear declName
+  else
+    let name := Name.mkStr declName "noConfusionType"
+    let decl ← ofExceptKernelException (mkNoConfusionTypeCoreImp (← getEnv) declName)
+    addDecl decl
+    setReducibleAttribute name
+    modifyEnv fun env => addToCompletionBlackList env name
+    modifyEnv fun env => addProtected env name
 
   let name := Name.mkStr declName "noConfusion"
   let decl ← ofExceptKernelException (mkNoConfusionCoreImp (← getEnv) declName)

src/Lean/Meta/Constructions/NoConfusionLinear.lean

@@ -0,0 +1,226 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+prelude
+import Lean.AddDecl
+import Lean.Meta.AppBuilder
+import Lean.Meta.CompletionName
+
+/-!
+This module produces a construction for the `noConfusionType` that is linear in size in the number of
+constructors of the inductive type. This is in contrast to the previous construction (definde in
+`no_confusion.cpp`), that is quadratic in size due to nested `.brecOn` applications.
+
+We still use the old construction when processing the prelude, for the few inductives that we need
+until below (`Nat`, `Bool`, `Decidable`).
+
+The main trick is to use a `withCtor` helper that is like a match with one constructor pattern and
+one catch-all pattern, and thus linear in size. And the helper itself is a single function
+definition, rather than one for each constructor, using a `withCtorType` helper in the function.
+
+See the `linearNoConfusion.lean` test for exemplary output of this translation (checked to be
+up-to-date).
+
+The `withCtor` functions could be generally useful, but for that they should probably eliminate into
+`Sort _` rather than `Type _`, and then writing the `withCtorType` function runs into universe level
+confusion, which may be solvable if the kernel had more complete univere level normalization.
+Until then we put these helper in the `noConfusionType` namespace to indicate that they are not
+general purpose.
+
+This module is written in a rather manual style, constructing the `Expr` directly. It's best
+read with the expected output to the side.
+-/
+
+namespace Lean.NoConfusionLinear
+
+open Meta
+
+/--
+List of constants that the linear `noConfusionType` construction depends on.
+-/
+def deps : Array Lean.Name :=
+  #[ ``Nat.lt, ``cond, ``Nat, ``PUnit, ``Eq, ``Not, ``dite, ``Nat.decEq, ``Nat.blt ]
+
+def mkNatLookupTable (n : Expr) (es : Array Expr) (default : Expr) : MetaM Expr := do
+  let type ← inferType default
+  let u ← getLevel type
+  let rec go (start stop : Nat) (hstart : start < stop := by omega) (hstop : stop ≤ es.size := by omega) : MetaM Expr := do
+    if h : start + 1 = stop then
+      return es[start]
+    else
+      let mid := (start + stop) / 2
+      let low ← go start mid
+      let high ← go mid stop
+      return mkApp4 (mkConst ``cond [u]) type (mkApp2 (mkConst ``Nat.blt) n (mkRawNatLit mid)) low high
+  if h : es.size = 0 then
+    pure default
+  else
+    go 0 es.size
+
+def mkWithCtorTypeName (indName : Name) : Name :=
+  Name.str indName "noConfusionType" |>.str "withCtorType"
+
+def mkWithCtorName (indName : Name) : Name :=
+  Name.str indName "noConfusionType" |>.str "withCtor"
+
+def mkNoConfusionTypeName (indName : Name) : Name :=
+  Name.str indName "noConfusionType"
+
+def mkWithCtorType (indName : Name) : MetaM Unit := do
+  let ConstantInfo.inductInfo info ← getConstInfo indName | unreachable!
+  let casesOnName := mkCasesOnName indName
+  let casesOnInfo ← getConstVal casesOnName
+  let v::us := casesOnInfo.levelParams.map mkLevelParam | panic! "unexpected universe levels on `casesOn`"
+  let indTyCon := mkConst indName us
+  let indTyKind ← inferType indTyCon
+  let indLevel ← getLevel indTyKind
+  let e ← forallBoundedTelescope indTyKind info.numParams fun xs  _ => do
+    withLocalDeclD `P (mkSort v.succ) fun P => do
+    withLocalDeclD `ctorIdx (mkConst ``Nat) fun ctorIdx => do
+      let default ← mkArrow (mkConst ``PUnit [indLevel]) P
+      let es ← info.ctors.toArray.mapM fun ctorName => do
+        let ctor := mkAppN (mkConst ctorName us) xs
+        let ctorType ← inferType ctor
+        let argType ← forallTelescope ctorType fun ys _ =>
+          mkForallFVars ys P
+        mkArrow (mkConst ``PUnit [indLevel]) argType
+      let e ← mkNatLookupTable ctorIdx es default
+      mkLambdaFVars ((xs.push P).push ctorIdx) e
+
+  let declName := mkWithCtorTypeName indName
+  addAndCompile (.defnDecl (← mkDefinitionValInferrringUnsafe
+    (name        := declName)
+    (levelParams := casesOnInfo.levelParams)
+    (type        := (← inferType e))
+    (value       := e)
+    (hints       := ReducibilityHints.abbrev)
+  ))
+  modifyEnv fun env => addToCompletionBlackList env declName
+  modifyEnv fun env => addProtected env declName
+  setReducibleAttribute declName
+
+def mkWithCtor (indName : Name) : MetaM Unit := do
+  let ConstantInfo.inductInfo info ← getConstInfo indName | unreachable!
+  let withCtorTypeName := mkWithCtorTypeName indName
+  let casesOnName := mkCasesOnName indName
+  let casesOnInfo ← getConstVal casesOnName
+  let v::us := casesOnInfo.levelParams.map mkLevelParam | panic! "unexpected universe levels on `casesOn`"
+  let indTyCon := mkConst indName us
+  let indTyKind ← inferType indTyCon
+  let indLevel ← getLevel indTyKind
+  let e ← forallBoundedTelescope indTyKind info.numParams fun xs t => do
+    withLocalDeclD `P (mkSort v.succ) fun P => do
+    withLocalDeclD `ctorIdx (mkConst ``Nat) fun ctorIdx => do
+      let withCtorTypeNameApp := mkAppN (mkConst withCtorTypeName (v :: us)) (xs.push P)
+      let kType := mkApp withCtorTypeNameApp  ctorIdx
+      withLocalDeclD `k kType fun k =>
+      withLocalDeclD `k' P fun k' =>
+      forallBoundedTelescope t info.numIndices fun ys t' => do
+        let t' ← whnfD t'
+        assert! t'.isSort
+        withLocalDeclD `x (mkAppN indTyCon (xs ++ ys)) fun x => do
+          let e := mkConst (mkCasesOnName indName) (v.succ :: us)
+          let e := mkAppN e xs
+          let motive ← mkLambdaFVars (ys.push x) P
+          let e := mkApp e motive
+          let e := mkAppN e ys
+          let e := mkApp e x
+          let alts ← info.ctors.toArray.mapIdxM fun i ctorName => do
+            let ctor := mkAppN (mkConst ctorName us) xs
+            let ctorType ← inferType ctor
+            forallTelescope ctorType fun zs _ => do
+              let heq := mkApp3 (mkConst ``Eq [1]) (mkConst ``Nat) ctorIdx (mkRawNatLit i)
+              let «then» ← withLocalDeclD `h heq fun h => do
+                let e ← mkEqNDRec (motive := withCtorTypeNameApp) k h
+                let e := mkApp e (mkConst ``PUnit.unit [indLevel])
+                let e := mkAppN e zs
+                -- ``Eq.ndrec
+                mkLambdaFVars #[h] e
+              let «else» ← withLocalDeclD `h (mkNot heq) fun h =>
+                mkLambdaFVars #[h] k'
+              let alt := mkApp5 (mkConst ``dite [v.succ])
+                  P heq (mkApp2 (mkConst ``Nat.decEq) ctorIdx (mkRawNatLit i))
+                  «then» «else»
+              mkLambdaFVars zs alt
+          let e := mkAppN e alts
+          mkLambdaFVars (xs ++ #[P, ctorIdx, k, k'] ++ ys ++ #[x]) e
+
+  let declName := mkWithCtorName indName
+  -- not compiled to avoid old code generator bug #1774
+  addDecl (.defnDecl (← mkDefinitionValInferrringUnsafe
+    (name        := declName)
+    (levelParams := casesOnInfo.levelParams)
+    (type        := (← inferType e))
+    (value       := e)
+    (hints       := ReducibilityHints.abbrev)
+  ))
+  modifyEnv fun env => addToCompletionBlackList env declName
+  modifyEnv fun env => addProtected env declName
+  setReducibleAttribute declName
+
+def mkNoConfusionTypeLinear (indName : Name) : MetaM Unit := do
+  let declName := mkNoConfusionTypeName indName
+  let ConstantInfo.inductInfo info ← getConstInfo indName | unreachable!
+  let casesOnName := mkCasesOnName indName
+  let casesOnInfo ← getConstVal casesOnName
+  let v::us := casesOnInfo.levelParams.map mkLevelParam | panic! "unexpected universe levels on `casesOn`"
+  let e := mkConst casesOnName (v.succ::us)
+  let t ← inferType e
+  let e ← forallBoundedTelescope t info.numParams fun xs t => do
+    let e := mkAppN e xs
+    let PType := mkSort v
+    withLocalDeclD `P PType fun P => do
+      let motive ← forallTelescope (← whnfD t).bindingDomain! fun ys _ =>
+        mkLambdaFVars ys PType
+      let t ← instantiateForall t #[motive]
+      let e := mkApp e motive
+      forallBoundedTelescope t info.numIndices fun ys t => do
+        let e := mkAppN e ys
+        let xType := mkAppN (mkConst indName us) (xs ++ ys)
+        withLocalDeclD `x1 xType fun x1 => do
+        withLocalDeclD `x2 xType fun x2 => do
+          let t ← instantiateForall t #[x1]
+          let e := mkApp e x1
+          forallBoundedTelescope t info.numCtors fun alts _ => do
+            let alts' ← alts.mapIdxM fun i alt => do
+              let altType ← inferType alt
+              forallTelescope altType fun zs1 _ => do
+                let alt := mkConst (mkWithCtorName indName) (v :: us)
+                let alt := mkAppN alt xs
+                let alt := mkApp alt PType
+                let alt := mkApp alt (mkRawNatLit i)
+                let k ← forallTelescopeReducing (← inferType alt).bindingDomain! fun zs2 _ => do
+                  let eqs ← (Array.zip zs1 zs2[1:]).filterMapM fun (z1,z2) => do
+                    if (← isProof z1) then
+                      return none
+                    else
+                      return some (← mkEqHEq z1 z2)
+                  let k ← mkArrowN eqs P
+                  let k ← mkArrow k P
+                  mkLambdaFVars zs2 k
+                let alt := mkApp alt k
+                let alt := mkApp alt P
+                let alt := mkAppN alt ys
+                let alt := mkApp alt x2
+                mkLambdaFVars zs1 alt
+            let e := mkAppN e alts'
+            let e ← mkLambdaFVars #[x1, x2] e
+            let e ← mkLambdaFVars #[P] e
+            let e ← mkLambdaFVars ys e
+            let e ← mkLambdaFVars xs e
+            pure e
+
+  addDecl (.defnDecl (← mkDefinitionValInferrringUnsafe
+    (name        := declName)
+    (levelParams := casesOnInfo.levelParams)
+    (type        := (← inferType e))
+    (value       := e)
+    (hints       := ReducibilityHints.abbrev)
+  ))
+  modifyEnv fun env => addToCompletionBlackList env declName
+  modifyEnv fun env => addProtected env declName
+  setReducibleAttribute declName
+
+end Lean.NoConfusionLinear

src/Lean/Meta/DiscrTree.lean

@@ -795,7 +795,7 @@ Fold the values stored in a `Trie`.
 -/
 @[inline]
 def foldValues (f : σ → α → σ) (init : σ) (t : Trie α) : σ :=
-  Id.run <| t.foldValuesM (init := init) f
+  Id.run <| t.foldValuesM (init := init) (pure <| f · ·)
 
 /--
 The number of values stored in a `Trie`.
@@ -835,7 +835,7 @@ Fold over the values stored in a `DiscrTree`.
 -/
 @[inline]
 def foldValues (f : σ → α → σ) (init : σ) (t : DiscrTree α) : σ :=
-  Id.run <| t.foldValuesM (init := init) f
+  Id.run <| t.foldValuesM (init := init) (pure <| f · ·)
 
 /--
 Check for the presence of a value satisfying a predicate.

src/Lean/Meta/GetUnfoldableConst.lean

@@ -37,7 +37,7 @@ This is part of the implementation of `whnf`.
 External users wanting to look up names should be using `Lean.getConstInfo`.
 -/
 def getUnfoldableConst? (constName : Name) : MetaM (Option ConstantInfo) := do
-  let some ainfo := (← getEnv).findAsync? constName | throwUnknownConstant constName
+  let some ainfo := (← getEnv).findAsync? constName | throwUnknownConstantAt (← getRef) constName
   match ainfo.kind with
   | .thm =>
     if (← shouldReduceAll) then

src/Lean/Meta/Tactic/Apply.lean

@@ -155,8 +155,8 @@ private def reorderGoals (mvars : Array Expr) : ApplyNewGoals → MetaM (List MV
   | ApplyNewGoals.all => return mvars.toList.map Lean.Expr.mvarId!
 
 /-- Custom `isDefEq` for the `apply` tactic -/
-private def isDefEqApply (cfg : ApplyConfig) (a b : Expr) : MetaM Bool := do
-  if cfg.approx then
+private def isDefEqApply (approx : Bool) (a b : Expr) : MetaM Bool := do
+  if approx then
     approxDefEq <| isDefEqGuarded a b
   else
     isDefEqGuarded a b
@@ -201,7 +201,7 @@ def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig :=
       if i < rangeNumArgs.stop then
         let s ← saveState
         let (newMVars, binderInfos, eType) ← forallMetaTelescopeReducing eType i
-        if (← isDefEqApply cfg eType targetType) then
+        if (← isDefEqApply cfg.approx eType targetType) then
           return (newMVars, binderInfos)
         else
           s.restore
@@ -231,6 +231,21 @@ def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig :=
 def _root_.Lean.MVarId.applyConst (mvar : MVarId) (c : Name) (cfg : ApplyConfig := {}) : MetaM (List MVarId) := do
   mvar.apply (← mkConstWithFreshMVarLevels c) cfg (term? := m!"'{.ofConstName c}'")
 
+/-- Close the given goal using `e`, instantiated with `n` metavariables. -/
+def _root_.Lean.MVarId.applyN (mvarId : MVarId) (e : Expr) (n : Nat) (useApproxDefEq := true) : MetaM (List MVarId) :=
+  mvarId.withContext do
+    mvarId.checkNotAssigned `apply
+    let targetType ← mvarId.getType
+    let eType      ← inferType e
+    let (mvarIds, _, eType) ← forallMetaBoundedTelescope eType n
+    unless mvarIds.size == n do
+      throwError "Applied type takes fewer than {n} arguments:\n{indentExpr eType}"
+    unless (← isDefEqApply useApproxDefEq eType targetType) do
+      throwError "Type mismatch: target is{indentExpr targetType}\nbut applied expression has \
+        type{indentExpr eType}\nafter applying {n} arguments."
+    mvarId.assign (e.beta mvarIds)
+    return (mvarIds.map (·.mvarId!)).toList
+
 end Meta
 
 open Meta

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

@@ -0,0 +1,112 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Grind.ENodeKey
+
+namespace Lean.Meta.Grind
+
+private def hashChild (e : Expr) : UInt64 :=
+  match e with
+  | .bvar .. | .mvar .. | .const .. | .fvar .. | .sort .. | .lit .. =>
+    hash e
+  | .app .. | .letE .. | .forallE .. | .lam .. | .mdata .. | .proj .. =>
+    (unsafe ptrAddrUnsafe e).toUInt64
+
+private def alphaHash (e : Expr) : UInt64 :=
+  match e with
+  | .bvar .. | .mvar .. | .const .. | .fvar .. | .sort .. | .lit .. =>
+    hash e
+  | .app f a => mixHash (hashChild f) (hashChild a)
+  | .letE _ _ v b _ => mixHash (hashChild v) (hashChild b)
+  | .forallE _ d b _ | .lam _ d b _ => mixHash (hashChild d) (hashChild b)
+  | .mdata _ b => mixHash 13 (hashChild b)
+  | .proj n i b => mixHash (mixHash (hash n) (hash i)) (hashChild b)
+
+private def alphaEq (e₁ e₂ : Expr) : Bool := Id.run do
+  match e₁ with
+  | .bvar .. | .mvar .. | .const .. | .fvar .. | .sort .. | .lit .. =>
+    e₁ == e₂
+  | .app f₁ a₁ =>
+    let .app f₂ a₂ := e₂ | false
+    isSameExpr f₁ f₂ && isSameExpr a₁ a₂
+  | .letE _ _ v₁ b₁ _ =>
+    let .letE _ _ v₂ b₂ _ := e₂ | false
+    isSameExpr v₁ v₂ && isSameExpr b₁ b₂
+  | .forallE _ d₁ b₁ _ =>
+    let .forallE _ d₂ b₂ _ := e₂ | false
+    isSameExpr d₁ d₂ && isSameExpr b₁ b₂
+  | .lam _ d₁ b₁ _ =>
+    let .lam _ d₂ b₂ _ := e₂ | false
+    isSameExpr d₁ d₂ && isSameExpr b₁ b₂
+  | .mdata d₁ b₁ =>
+    let .mdata d₂ b₂ := e₂ | false
+    return isSameExpr b₁ b₂ && d₁ == d₂
+  | .proj n₁ i₁ b₁ =>
+    let .proj n₂ i₂ b₂ := e₂ | false
+    n₁ == n₂ && i₁ == i₂ && isSameExpr b₁ b₂
+
+structure AlphaKey where
+  expr : Expr
+
+instance : Hashable AlphaKey where
+  hash k := alphaHash k.expr
+
+instance : BEq AlphaKey where
+  beq k₁ k₂ := alphaEq k₁.expr k₂.expr
+
+structure AlphaShareCommon.State where
+  map : PHashMap ENodeKey Expr := {}
+  set : PHashSet AlphaKey := {}
+
+abbrev AlphaShareCommonM := StateM AlphaShareCommon.State
+
+private def save (e : Expr) (r : Expr) : AlphaShareCommonM Expr := do
+  if let some r := (← get).set.find? { expr := r } then
+    let r := r.expr
+    modify fun { set, map } => {
+      set
+      map := map.insert { expr := e } r
+    }
+    return r
+  else
+    modify fun { set, map } => {
+      set := set.insert { expr := r }
+      map := map.insert { expr := e } r |>.insert { expr := r } r
+    }
+    return r
+
+private abbrev visit (e : Expr) (k : AlphaShareCommonM Expr) : AlphaShareCommonM Expr := do
+  if let some r := (← get).map.find? { expr := e } then
+    return r
+  else
+    save e (← k)
+
+/-- Similar to `shareCommon`, but handles alpha-equivalence. -/
+def shareCommonAlpha (e : Expr) : AlphaShareCommonM Expr :=
+  go e
+where
+  go (e : Expr) : AlphaShareCommonM Expr := do
+    match e with
+    | .bvar .. | .mvar .. | .const .. | .fvar .. | .sort .. | .lit .. =>
+      if let some r := (← get).set.find? { expr := e } then
+        return r.expr
+      else
+        modify fun { set, map } => { set := set.insert { expr := e }, map }
+        return e
+    | .app f a =>
+      visit e (return mkApp (← go f) (← go a))
+    | .letE n t v b nd =>
+      visit e (return mkLet n t (← go v) (← go b) nd)
+    | .forallE n d b bi =>
+      visit e (return mkForall n bi (← go d) (← go b))
+    | .lam n d b bi =>
+      visit e (return mkLambda n bi (← go d) (← go b))
+    | .mdata d b =>
+      visit e (return mkMData d (← go b))
+    | .proj n i b =>
+      visit e (return mkProj n i (← go b))
+
+end Lean.Meta.Grind

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

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Meta.Tactic.Grind.Combinators
 import Lean.Meta.Tactic.Grind.Canon
 import Lean.Meta.Tactic.Grind.MBTC
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Model
@@ -36,8 +35,8 @@ private def eqAssignment (a b : Expr) : GoalM Bool := do
   let some v₂ ← getAssignmentExt? b | return false
   return v₁ == v₂
 
-def mbtcTac : GrindTactic :=
-  Grind.mbtcTac {
+def mbtc : GoalM Bool := do
+  Grind.mbtc {
     hasTheoryVar := hasTheoryVar
     isInterpreted := isInterpreted
     eqAssignment := eqAssignment

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

@@ -95,7 +95,7 @@ def mkModel (goal : Goal) : MetaM (Array (Expr × Rat)) := do
   -- Assign on expressions associated with cutsat terms or interpreted terms
   for e in goal.exprs do
     let node ← goal.getENode e
-    if isSameExpr node.root node.self then
+    if node.isRoot then
     if (← isIntNatENode node) then
       if let some v ← getAssignment? goal node.self then
         if v.den == 1 then used := used.insert v.num
@@ -111,7 +111,7 @@ def mkModel (goal : Goal) : MetaM (Array (Expr × Rat)) := do
   -- Assign the remaining ones with values not used by cutsat
   for e in goal.exprs do
     let node ← goal.getENode e
-    if isSameExpr node.root node.self then
+    if node.isRoot then
     if (← isIntNatENode node) then
     if model[node.self]?.isNone then
       let v := pickUnusedValue goal model node.self nextVal used

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

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.Tactic.Grind.PropagatorAttr
-import Lean.Meta.Tactic.Grind.Combinators
 import Lean.Meta.Tactic.Grind.Arith.Offset
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Search
@@ -37,20 +36,13 @@ builtin_grind_propagator propagateLE ↓LE.le := fun e => do
       Offset.assertFalse c (← mkEqFalseProof e)
     Cutsat.propagateIfSupportedLe e (eqTrue := false)
 
-def check : GrindTactic := fun goal => do
-  let (progress, goal) ← GoalM.run goal do
-    let c₁ ← Cutsat.check
-    let c₂ ← CommRing.check
-    if c₁ || c₂ then
-      processNewFacts
-      return true
-    else
-      return false
-  unless progress do
-    return none
-  if goal.inconsistent then
-    return some []
+def check : GoalM Bool := do
+  let c₁ ← Cutsat.check
+  let c₂ ← CommRing.check
+  if c₁ || c₂ then
+    processNewFacts
+    return true
   else
-    return some [goal]
+    return false
 
 end Lean.Meta.Grind.Arith

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

@@ -49,11 +49,20 @@ def getAttrKindFromOpt (stx : Syntax) : CoreM AttrKind := do
 def throwInvalidUsrModifier : CoreM α :=
   throwError "the modifier `usr` is only relevant in parameters for `grind only`"
 
-builtin_initialize
+/--
+Auxiliary function for registering `grind` and `grind?` attributes.
+The `grind?` is an alias for `grind` which displays patterns using `logInfo`.
+It is just a convenience for users.
+-/
+private def registerGrindAttr (showInfo : Bool) : IO Unit :=
   registerBuiltinAttribute {
-    name := `grind
+    name := if showInfo then `grind? else `grind
     descr :=
-      "The `[grind]` attribute is used to annotate declarations.\
+      let header := if showInfo then
+        "The `[grind?]` attribute is identical to the `[grind]` attribute, but displays inferred pattern information."
+      else
+        "The `[grind]` attribute is used to annotate declarations."
+      header ++ "\
       \
       When applied to an equational theorem, `[grind =]`, `[grind =_]`, or `[grind _=_]`\
       will mark the theorem for use in heuristic instantiations by the `grind` tactic,
@@ -73,12 +82,12 @@ builtin_initialize
     add := fun declName stx attrKind => MetaM.run' do
       match (← getAttrKindFromOpt stx) with
       | .ematch .user => throwInvalidUsrModifier
-      | .ematch k => addEMatchAttr declName attrKind k
+      | .ematch k => addEMatchAttr declName attrKind k (showInfo := showInfo)
       | .cases eager => addCasesAttr declName eager attrKind
       | .intro =>
         if let some info ← isCasesAttrPredicateCandidate? declName false then
           for ctor in info.ctors do
-            addEMatchAttr ctor attrKind .default
+            addEMatchAttr ctor attrKind .default (showInfo := showInfo)
         else
           throwError "invalid `[grind intro]`, `{declName}` is not an inductive predicate"
       | .ext => addExtAttr declName attrKind
@@ -89,10 +98,12 @@ builtin_initialize
             -- If it is an inductive predicate,
             -- we also add the constructors (intro rules) as E-matching rules
             for ctor in info.ctors do
-              addEMatchAttr ctor attrKind .default
+              addEMatchAttr ctor attrKind .default (showInfo := showInfo)
         else
-          addEMatchAttr declName attrKind .default
+          addEMatchAttr declName attrKind .default (showInfo := showInfo)
     erase := fun declName => MetaM.run' do
+      if showInfo then
+        throwError "`[grind?]` is a helper attribute for displaying inferred patterns, if you want to remove the attribute, consider using `[grind]` instead"
       if (← isCasesAttrCandidate declName false) then
         eraseCasesAttr declName
       else if (← isExtTheorem declName) then
@@ -101,4 +112,8 @@ builtin_initialize
         eraseEMatchAttr declName
   }
 
+builtin_initialize
+  registerGrindAttr true
+  registerGrindAttr false
+
 end Lean.Meta.Grind

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

@@ -77,7 +77,15 @@ def canonElemCore (parent : Expr) (f : Expr) (i : Nat) (e : Expr) (useIsDefEqBou
   let eType ← inferType e
   let cs := s.argMap.find? key |>.getD []
   for (c, cType) in cs do
-    -- We first check the typesr
+    /-
+    We first check the types
+    The following checks are a performance bottleneck.
+    For example, in the test `grind_ite.lean`, there are many checks of the form:
+    ```
+    w_4 ∈ assign.insert v true → Prop =?= w_1 ∈ assign.insert v false → Prop
+    ```
+    where `grind` unfolds the definition of `DHashMap.insert` and `TreeMap.insert`.
+    -/
     if (← withDefault <| isDefEq eType cType) then
       if (← isDefEq e c) then
         -- We used to check `c.fvarsSubset e` because it is not
@@ -196,7 +204,7 @@ where
 end Canon
 
 /-- Canonicalizes nested types, type formers, and instances in `e`. -/
-def canon (e : Expr) : GoalM Expr := do
+def canon (e : Expr) : GoalM Expr := do profileitM Exception "grind canon" (← getOptions) do
   trace_goal[grind.debug.canon] "{e}"
   unsafe Canon.canonImpl e
 

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

@@ -70,20 +70,9 @@ def getCasesTypes : CoreM CasesTypes :=
 def isSplit (declName : Name) : CoreM Bool := do
   return (← getCasesTypes).isSplit declName
 
-private def getAlias? (value : Expr) : MetaM (Option Name) :=
-  lambdaTelescope value fun _ body => do
-    if let .const declName _ := body.getAppFn' then
-      return some declName
-    else
-      return none
-
 partial def isCasesAttrCandidate? (declName : Name) (eager : Bool) : CoreM (Option Name) := do
   match (← getConstInfo declName) with
   | .inductInfo info => if !info.isRec || !eager then return some declName else return none
-  | .defnInfo info =>
-    let some declName ← getAlias? info.value |>.run' {} {}
-      | return none
-    isCasesAttrCandidate? declName eager
   | _ => return none
 
 def isCasesAttrCandidate (declName : Name) (eager : Bool) : CoreM Bool := do
@@ -161,6 +150,10 @@ def cases (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := mvarId.withConte
   let k (mvarId : MVarId) (fvarId : FVarId) (indices : Array FVarId) : MetaM (List MVarId) := do
     let indicesExpr := indices.map mkFVar
     let recursor ← mkRecursorAppPrefix mvarId `grind.cases fvarId recursorInfo indicesExpr
+    let lctx ← getLCtx
+    let lctx := lctx.setKind fvarId .implDetail
+    let lctx := indices.foldl (init := lctx) fun lctx fvarId => lctx.setKind fvarId .implDetail
+    let localInsts ← getLocalInstances
     let mut recursor := mkApp (mkAppN recursor indicesExpr) (mkFVar fvarId)
     let mut recursorType ← inferType recursor
     let mut mvarIdsNew := #[]
@@ -170,10 +163,9 @@ def cases (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := mvarId.withConte
         | throwTacticEx `grind.cases mvarId "unexpected recursor type"
       recursorType := recursorTypeNew
       let tagNew := if recursorInfo.numMinors > 1 then Name.num tag idx else tag
-      let mvar ← mkFreshExprSyntheticOpaqueMVar targetNew tagNew
+      let mvar ← mkFreshExprMVarAt lctx localInsts targetNew .syntheticOpaque tagNew
       recursor := mkApp recursor mvar
-      let mvarIdNew ← mvar.mvarId!.tryClearMany (indices.push fvarId)
-      mvarIdsNew := mvarIdsNew.push mvarIdNew
+      mvarIdsNew := mvarIdsNew.push mvar.mvarId!
       idx := idx + 1
     mvarId.assign recursor
     return mvarIdsNew.toList

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

@@ -1,71 +0,0 @@
-/-
-Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.Meta.Tactic.Grind.Types
-
-namespace Lean.Meta.Grind
-
-/-!
-Combinators for manipulating `GrindTactic`s.
-TODO: a proper tactic language for `grind`.
--/
-
-def GrindTactic := Goal → GrindM (Option (List Goal))
-
-def GrindTactic.try (x : GrindTactic) : GrindTactic := fun g => do
-  let some gs ← x g | return some [g]
-  return some gs
-
-def applyToAll (x : GrindTactic)  (goals : List Goal) : GrindM (List Goal) := do
-  go goals []
-where
-  go (goals : List Goal) (acc : List Goal) : GrindM (List Goal) := do
-    match goals with
-    | [] => return acc.reverse
-    | goal :: goals => match (← x goal) with
-      | none => go goals (goal :: acc)
-      | some goals' => go goals (goals' ++ acc)
-
-partial def GrindTactic.andThen (x y : GrindTactic) : GrindTactic := fun goal => do
-  let some goals ← x goal | return none
-  applyToAll y goals
-
-instance : AndThen GrindTactic where
-  andThen a b := GrindTactic.andThen a (b ())
-
-partial def GrindTactic.iterate (x : GrindTactic) : GrindTactic := fun goal => do
-  go [goal] []
-where
-  go (todo : List Goal) (result : List Goal) : GrindM (List Goal) := do
-    match todo with
-    | [] => return result
-    | goal :: todo =>
-      if let some goalsNew ← x goal then
-        go (goalsNew ++ todo) result
-      else
-        go todo (goal :: result)
-
-partial def GrindTactic.orElse (x y : GrindTactic) : GrindTactic := fun goal => do
-  let some goals ← x goal | y goal
-  return goals
-
-instance : OrElse GrindTactic where
-  orElse a b := GrindTactic.andThen a (b ())
-
-def toGrindTactic (f : GoalM Unit) : GrindTactic := fun goal => do
-  let goal ← GoalM.run' goal f
-  if goal.inconsistent then
-    return some []
-  else
-    return some [goal]
-
-def GrindTactic' := Goal → GrindM (List Goal)
-
-def GrindTactic'.toGrindTactic (x : GrindTactic') : GrindTactic := fun goal => do
-  let goals ← x goal
-  return some goals
-
-end Lean.Meta.Grind

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

@@ -474,7 +474,7 @@ end EMatch
 open EMatch
 
 /-- Performs one round of E-matching, and returns new instances. -/
-def ematch : GoalM Unit := do
+private def ematchCore : GoalM Unit := do
   let go (thms newThms : PArray EMatchTheorem) : EMatch.M Unit := do
     withReader (fun ctx => { ctx with useMT := true }) <| ematchTheorems thms
     withReader (fun ctx => { ctx with useMT := false }) <| ematchTheorems newThms
@@ -489,12 +489,10 @@ def ematch : GoalM Unit := do
       ematch.num       := s.ematch.num + 1
     }
 
-/-- Performs one round of E-matching, and assert new instances. -/
-def ematchAndAssert : GrindTactic := fun goal => do
-  let numInstances := goal.ematch.numInstances
-  let goal ← GoalM.run' goal ematch
-  if goal.ematch.numInstances == numInstances then
-    return none
-  assertAll goal
+/-- Performs one round of E-matching, and returns `true` if new instances were generated. -/
+def ematch : GoalM Bool := do
+  let numInstances := (← get).ematch.numInstances
+  ematchCore
+  return (← get).ematch.numInstances != numInstances
 
 end Lean.Meta.Grind

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

@@ -589,18 +589,24 @@ private def ppParamsAt (proof : Expr) (numParams : Nat) (paramPos : List Nat) :
         msg := msg ++ m!"{x} : {← inferType x}"
     addMessageContextFull msg
 
+private def logPatternWhen (showInfo : Bool) (origin : Origin) (patterns : List Expr) : MetaM Unit := do
+  if showInfo then
+    logInfo m!"{← origin.pp}: {patterns.map ppPattern}"
+
 /--
 Creates an E-matching theorem for a theorem with proof `proof`, `numParams` parameters, and the given set of patterns.
 Pattern variables are represented using de Bruijn indices.
 -/
-def mkEMatchTheoremCore (origin : Origin) (levelParams : Array Name) (numParams : Nat) (proof : Expr) (patterns : List Expr) (kind : EMatchTheoremKind) : MetaM EMatchTheorem := do
+def mkEMatchTheoremCore (origin : Origin) (levelParams : Array Name) (numParams : Nat) (proof : Expr)
+    (patterns : List Expr) (kind : EMatchTheoremKind) (showInfo := false) : MetaM EMatchTheorem := do
   let (patterns, symbols, bvarFound) ← NormalizePattern.main patterns
   if symbols.isEmpty then
     throwError "invalid pattern for `{← origin.pp}`{indentD (patterns.map ppPattern)}\nthe pattern does not contain constant symbols for indexing"
-  trace[grind.ematch.pattern] "{MessageData.ofConst proof}: {patterns.map ppPattern}"
+  trace[grind.ematch.pattern] "{← origin.pp}: {patterns.map ppPattern}"
   if let .missing pos ← checkCoverage proof numParams bvarFound then
      let pats : MessageData := m!"{patterns.map ppPattern}"
      throwError "invalid pattern(s) for `{← origin.pp}`{indentD pats}\nthe following theorem parameters cannot be instantiated:{indentD (← ppParamsAt proof numParams pos)}"
+  logPatternWhen showInfo origin patterns
   return {
     proof, patterns, numParams, symbols
     levelParams, origin, kind
@@ -627,7 +633,7 @@ Given a theorem with proof `proof` and type of the form `∀ (a_1 ... a_n), lhs
 creates an E-matching pattern for it using `addEMatchTheorem n [lhs]`
 If `normalizePattern` is true, it applies the `grind` simplification theorems and simprocs to the pattern.
 -/
-def mkEMatchEqTheoremCore (origin : Origin) (levelParams : Array Name) (proof : Expr) (normalizePattern : Bool) (useLhs : Bool) : MetaM EMatchTheorem := do
+def mkEMatchEqTheoremCore (origin : Origin) (levelParams : Array Name) (proof : Expr) (normalizePattern : Bool) (useLhs : Bool) (showInfo := false) : MetaM EMatchTheorem := do
   let (numParams, patterns) ← forallTelescopeReducing (← inferType proof) fun xs type => do
     let (lhs, rhs) ← match_expr type with
       | Eq _ lhs rhs => pure (lhs, rhs)
@@ -640,15 +646,15 @@ def mkEMatchEqTheoremCore (origin : Origin) (levelParams : Array Name) (proof :
     trace[grind.debug.ematch.pattern] "mkEMatchEqTheoremCore: after preprocessing: {pat}, {← normalize pat normConfig}"
     let pats := splitWhileForbidden (pat.abstract xs)
     return (xs.size, pats)
-  mkEMatchTheoremCore origin levelParams numParams proof patterns (if useLhs then .eqLhs else .eqRhs)
+  mkEMatchTheoremCore origin levelParams numParams proof patterns (if useLhs then .eqLhs else .eqRhs) (showInfo := showInfo)
 
-def mkEMatchEqBwdTheoremCore (origin : Origin) (levelParams : Array Name) (proof : Expr) : MetaM EMatchTheorem := do
+def mkEMatchEqBwdTheoremCore (origin : Origin) (levelParams : Array Name) (proof : Expr) (showInfo := false) : MetaM EMatchTheorem := do
   let (numParams, patterns) ← forallTelescopeReducing (← inferType proof) fun xs type => do
     let_expr f@Eq α lhs rhs := type
       | throwError "invalid E-matching `←=` theorem, conclusion must be an equality{indentExpr type}"
     let pat ← preprocessPattern (mkEqBwdPattern f.constLevels! α lhs rhs)
     return (xs.size, [pat.abstract xs])
-  mkEMatchTheoremCore origin levelParams numParams proof patterns .eqBwd
+  mkEMatchTheoremCore origin levelParams numParams proof patterns .eqBwd (showInfo := showInfo)
 
 /--
 Given theorem with name `declName` and type of the form `∀ (a_1 ... a_n), lhs = rhs`,
@@ -657,8 +663,8 @@ creates an E-matching pattern for it using `addEMatchTheorem n [lhs]`
 If `normalizePattern` is true, it applies the `grind` simplification theorems and simprocs to the
 pattern.
 -/
-def mkEMatchEqTheorem (declName : Name) (normalizePattern := true) (useLhs : Bool := true) : MetaM EMatchTheorem := do
-  mkEMatchEqTheoremCore (.decl declName) #[] (← getProofFor declName) normalizePattern useLhs
+def mkEMatchEqTheorem (declName : Name) (normalizePattern := true) (useLhs : Bool := true) (showInfo := false) : MetaM EMatchTheorem := do
+  mkEMatchEqTheoremCore (.decl declName) #[] (← getProofFor declName) normalizePattern useLhs (showInfo := showInfo)
 
 /--
 Adds an E-matching theorem to the environment.
@@ -844,13 +850,13 @@ since the theorem is already in the `grind` state and there is nothing to be ins
 -/
 def mkEMatchTheoremWithKind?
       (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : EMatchTheoremKind)
-      (groundPatterns := true) : MetaM (Option EMatchTheorem) := do
+      (groundPatterns := true) (showInfo := false) : MetaM (Option EMatchTheorem) := do
   if kind == .eqLhs then
-    return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := true) (useLhs := true))
+    return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := true) (useLhs := true) (showInfo := showInfo))
   else if kind == .eqRhs then
-    return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := true) (useLhs := false))
+    return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := true) (useLhs := false) (showInfo := showInfo))
   else if kind == .eqBwd then
-    return (← mkEMatchEqBwdTheoremCore origin levelParams proof)
+    return (← mkEMatchEqBwdTheoremCore origin levelParams proof (showInfo := showInfo))
   let type ← inferType proof
   /-
   Remark: we should not use `forallTelescopeReducing` (with default reducibility) here
@@ -894,25 +900,26 @@ where
       return none
     let numParams := xs.size
     trace[grind.ematch.pattern] "{← origin.pp}: {patterns.map ppPattern}"
+    logPatternWhen showInfo origin patterns
     return some {
       proof, patterns, numParams, symbols
       levelParams, origin, kind
     }
 
-def mkEMatchTheoremForDecl (declName : Name) (thmKind : EMatchTheoremKind) : MetaM EMatchTheorem := do
-  let some thm ← mkEMatchTheoremWithKind? (.decl declName) #[] (← getProofFor declName) thmKind
+def mkEMatchTheoremForDecl (declName : Name) (thmKind : EMatchTheoremKind) (showInfo := false) : MetaM EMatchTheorem := do
+  let some thm ← mkEMatchTheoremWithKind? (.decl declName) #[] (← getProofFor declName) thmKind (showInfo := showInfo)
     | throwError "`@{thmKind.toAttribute} theorem {declName}` {thmKind.explainFailure}, consider using different options or the `grind_pattern` command"
   return thm
 
-def mkEMatchEqTheoremsForDef? (declName : Name) : MetaM (Option (Array EMatchTheorem)) := do
+def mkEMatchEqTheoremsForDef? (declName : Name) (showInfo := false) : MetaM (Option (Array EMatchTheorem)) := do
   let some eqns ← getEqnsFor? declName | return none
   eqns.mapM fun eqn => do
-    mkEMatchEqTheorem eqn (normalizePattern := true)
+    mkEMatchEqTheorem eqn (normalizePattern := true) (showInfo := showInfo)
 
-private def addGrindEqAttr (declName : Name) (attrKind : AttributeKind) (thmKind : EMatchTheoremKind) (useLhs := true) : MetaM Unit := do
+private def addGrindEqAttr (declName : Name) (attrKind : AttributeKind) (thmKind : EMatchTheoremKind) (useLhs := true) (showInfo := false) : MetaM Unit := do
   if wasOriginallyTheorem (← getEnv) declName then
-    ematchTheoremsExt.add (← mkEMatchEqTheorem declName (normalizePattern := true) (useLhs := useLhs)) attrKind
-  else if let some thms ← mkEMatchEqTheoremsForDef? declName then
+    ematchTheoremsExt.add (← mkEMatchEqTheorem declName (normalizePattern := true) (useLhs := useLhs) (showInfo := showInfo)) attrKind
+  else if let some thms ← mkEMatchEqTheoremsForDef? declName (showInfo := showInfo) then
     unless useLhs do
       throwError "`{declName}` is a definition, you must only use the left-hand side for extracting patterns"
     thms.forM (ematchTheoremsExt.add · attrKind)
@@ -935,20 +942,20 @@ def EMatchTheorems.eraseDecl (s : EMatchTheorems) (declName : Name) : MetaM EMat
       throwErr
     return s.erase <| .decl declName
 
-def addEMatchAttr (declName : Name) (attrKind : AttributeKind) (thmKind : EMatchTheoremKind) : MetaM Unit := do
+def addEMatchAttr (declName : Name) (attrKind : AttributeKind) (thmKind : EMatchTheoremKind) (showInfo := false) : MetaM Unit := do
   if thmKind == .eqLhs then
-    addGrindEqAttr declName attrKind thmKind (useLhs := true)
+    addGrindEqAttr declName attrKind thmKind (useLhs := true) (showInfo := showInfo)
   else if thmKind == .eqRhs then
-    addGrindEqAttr declName attrKind thmKind (useLhs := false)
+    addGrindEqAttr declName attrKind thmKind (useLhs := false) (showInfo := showInfo)
   else if thmKind == .eqBoth then
-    addGrindEqAttr declName attrKind thmKind (useLhs := true)
-    addGrindEqAttr declName attrKind thmKind (useLhs := false)
+    addGrindEqAttr declName attrKind thmKind (useLhs := true) (showInfo := showInfo)
+    addGrindEqAttr declName attrKind thmKind (useLhs := false) (showInfo := showInfo)
   else
     let info ← getConstInfo declName
     if !wasOriginallyTheorem (← getEnv) declName && !info.isCtor && !info.isAxiom then
-      addGrindEqAttr declName attrKind thmKind
+      addGrindEqAttr declName attrKind thmKind (showInfo := showInfo)
     else
-      let thm ← mkEMatchTheoremForDecl declName thmKind
+      let thm ← mkEMatchTheoremForDecl declName thmKind (showInfo := showInfo)
       ematchTheoremsExt.add thm attrKind
 
 def eraseEMatchAttr (declName : Name) : MetaM Unit := do