feat: lemmas about ordered modules

We started running into OOMs in the test suite. This is the faster
alternative to lowering test parallelism.

.github/workflows/ci.yml

@@ -164,7 +164,7 @@ jobs:
               {
                 // portable release build: use channel with older glibc (2.26)
                 "name": "Linux release",
-                "os": large ? "nscloud-ubuntu-22.04-amd64-4x8" : "ubuntu-latest",
+                "os": large && level < 2 ? "nscloud-ubuntu-22.04-amd64-4x16" : "ubuntu-latest",
                 "release": true,
                 "check-level": 2,
                 "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
@@ -176,7 +176,7 @@ jobs:
               },
               {
                 "name": "Linux Lake",
-                "os": large ? "nscloud-ubuntu-22.04-amd64-8x8" : "ubuntu-latest",
+                "os": large && level < 2 ? "nscloud-ubuntu-22.04-amd64-8x16" : "ubuntu-latest",
                 "check-level": 0,
                 "test": true,
                 "check-rebootstrap": level >= 1,
@@ -215,7 +215,8 @@ jobs:
               },
               {
                 "name": "macOS aarch64",
-                "os": "macos-14",
+                // standard GH runner only comes with 7GB so use large runner if possible
+                "os": large ? "nscloud-macos-sonoma-arm64-6x14" : "macos-14",
                 "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
                 "release": true,
                 "shell": "bash -euxo pipefail {0}",
@@ -246,7 +247,7 @@ jobs:
               },
               {
                 "name": "Linux aarch64",
-                "os": "nscloud-ubuntu-22.04-arm64-4x8",
+                "os": "nscloud-ubuntu-22.04-arm64-4x16",
                 "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-linux_aarch64",
                 "release": true,
                 "check-level": 2,

src/Init/Data/Array/Count.lean

@@ -52,6 +52,7 @@ theorem countP_push {a : α} {xs : Array α} : countP p (xs.push a) = countP p x
   rcases xs with ⟨xs⟩
   simp_all
 
+@[grind =]
 theorem countP_singleton {a : α} : countP p #[a] = if p a then 1 else 0 := by
   simp
 
@@ -59,10 +60,12 @@ theorem size_eq_countP_add_countP {xs : Array α} : xs.size = countP p xs + coun
   rcases xs with ⟨xs⟩
   simp [List.length_eq_countP_add_countP (p := p)]
 
+@[grind _=_]
 theorem countP_eq_size_filter {xs : Array α} : countP p xs = (filter p xs).size := by
   rcases xs with ⟨xs⟩
   simp [List.countP_eq_length_filter]
 
+@[grind =]
 theorem countP_eq_size_filter' : countP p = size ∘ filter p := by
   funext xs
   apply countP_eq_size_filter
@@ -71,7 +74,7 @@ theorem countP_le_size : countP p xs ≤ xs.size := by
   simp only [countP_eq_size_filter]
   apply size_filter_le
 
-@[simp] theorem countP_append {xs ys : Array α} : countP p (xs ++ ys) = countP p xs + countP p ys := by
+@[simp, grind =] theorem countP_append {xs ys : Array α} : countP p (xs ++ ys) = countP p xs + countP p ys := by
   rcases xs with ⟨xs⟩
   rcases ys with ⟨ys⟩
   simp
@@ -102,6 +105,7 @@ theorem boole_getElem_le_countP {xs : Array α} {i : Nat} (h : i < xs.size) :
   rcases xs with ⟨xs⟩
   simp [List.boole_getElem_le_countP]
 
+@[grind =]
 theorem countP_set {xs : Array α} {i : Nat} {a : α} (h : i < xs.size) :
     (xs.set i a).countP p = xs.countP p - (if p xs[i] then 1 else 0) + (if p a then 1 else 0) := by
   rcases xs with ⟨xs⟩
@@ -146,7 +150,7 @@ theorem countP_flatMap {p : β → Bool} {xs : Array α} {f : α → Array β} :
   rcases xs with ⟨xs⟩
   simp [List.countP_flatMap, Function.comp_def]
 
-@[simp] theorem countP_reverse {xs : Array α} : countP p xs.reverse = countP p xs := by
+@[simp, grind =] theorem countP_reverse {xs : Array α} : countP p xs.reverse = countP p xs := by
   rcases xs with ⟨xs⟩
   simp [List.countP_reverse]
 
@@ -173,7 +177,7 @@ variable [BEq α]
   cases xs
   simp
 
-@[simp] theorem count_empty {a : α} : count a #[] = 0 := rfl
+@[simp, grind =] theorem count_empty {a : α} : count a #[] = 0 := rfl
 
 theorem count_push {a b : α} {xs : Array α} :
     count a (xs.push b) = count a xs + if b == a then 1 else 0 := by
@@ -186,21 +190,28 @@ theorem count_eq_countP' {a : α} : count a = countP (· == a) := by
 
 theorem count_le_size {a : α} {xs : Array α} : count a xs ≤ xs.size := countP_le_size
 
+grind_pattern count_le_size => count a xs
+
+@[grind =]
+theorem count_eq_size_filter {a : α} {xs : Array α} : count a xs = (filter (· == a) xs).size := by
+  simp [count, countP_eq_size_filter]
+
 theorem count_le_count_push {a b : α} {xs : Array α} : count a xs ≤ count a (xs.push b) := by
   simp [count_push]
 
+@[grind =]
 theorem count_singleton {a b : α} : count a #[b] = if b == a then 1 else 0 := by
   simp [count_eq_countP]
 
-@[simp] theorem count_append {a : α} {xs ys : Array α} : count a (xs ++ ys) = count a xs + count a ys :=
+@[simp, grind =] theorem count_append {a : α} {xs ys : Array α} : count a (xs ++ ys) = count a xs + count a ys :=
   countP_append
 
-@[simp] theorem count_flatten {a : α} {xss : Array (Array α)} :
+@[simp, grind =] theorem count_flatten {a : α} {xss : Array (Array α)} :
     count a xss.flatten = (xss.map (count a)).sum := by
   cases xss using array₂_induction
   simp [List.count_flatten, Function.comp_def]
 
-@[simp] theorem count_reverse {a : α} {xs : Array α} : count a xs.reverse = count a xs := by
+@[simp, grind =] theorem count_reverse {a : α} {xs : Array α} : count a xs.reverse = count a xs := by
   rcases xs with ⟨xs⟩
   simp
 
@@ -209,6 +220,7 @@ theorem boole_getElem_le_count {xs : Array α} {i : Nat} {a : α} (h : i < xs.si
   rw [count_eq_countP]
   apply boole_getElem_le_countP (p := (· == a))
 
+@[grind =]
 theorem count_set {xs : Array α} {i : Nat} {a b : α} (h : i < xs.size) :
     (xs.set i a).count b = xs.count b - (if xs[i] == b then 1 else 0) + (if a == b then 1 else 0) := by
   simp [count_eq_countP, countP_set, h]

src/Init/Data/Array/Extract.lean

@@ -46,7 +46,7 @@ theorem size_extract_of_le {as : Array α} {i j : Nat} (h : j ≤ as.size) :
   simp
   omega
 
-@[simp]
+@[simp, grind =]
 theorem extract_push {as : Array α} {b : α} {start stop : Nat} (h : stop ≤ as.size) :
     (as.push b).extract start stop = as.extract start stop := by
   ext i h₁ h₂
@@ -56,7 +56,7 @@ theorem extract_push {as : Array α} {b : α} {start stop : Nat} (h : stop ≤ a
     simp only [getElem_extract, getElem_push]
     rw [dif_pos (by omega)]
 
-@[simp]
+@[simp, grind =]
 theorem extract_eq_pop {as : Array α} {stop : Nat} (h : stop = as.size - 1) :
     as.extract 0 stop = as.pop := by
   ext i h₁ h₂
@@ -65,7 +65,7 @@ theorem extract_eq_pop {as : Array α} {stop : Nat} (h : stop = as.size - 1) :
   · simp only [size_extract, size_pop] at h₁ h₂
     simp [getElem_extract, getElem_pop]
 
-@[simp]
+@[simp, grind _=_]
 theorem extract_append_extract {as : Array α} {i j k : Nat} :
     as.extract i j ++ as.extract j k = as.extract (min i j) (max j k) := by
   ext l h₁ h₂
@@ -169,7 +169,7 @@ theorem getElem?_extract_of_succ {as : Array α} {j : Nat} :
   simp [getElem?_extract]
   omega
 
-@[simp] theorem extract_extract {as : Array α} {i j k l : Nat} :
+@[simp, grind =] theorem extract_extract {as : Array α} {i j k l : Nat} :
     (as.extract i j).extract k l = as.extract (i + k) (min (i + l) j) := by
   ext m h₁ h₂
   · simp
@@ -185,6 +185,7 @@ theorem ne_empty_of_extract_ne_empty {as : Array α} {i j : Nat} (h : as.extract
     as ≠ #[] :=
   mt extract_eq_empty_of_eq_empty h
 
+@[grind =]
 theorem extract_set {as : Array α} {i j k : Nat} (h : k < as.size) {a : α} :
     (as.set k a).extract i j =
       if _ : k < i then
@@ -211,13 +212,14 @@ theorem extract_set {as : Array α} {i j k : Nat} (h : k < as.size) {a : α} :
         simp [getElem_set]
         omega
 
+@[grind =]
 theorem set_extract {as : Array α} {i j k : Nat} (h : k < (as.extract i j).size) {a : α} :
     (as.extract i j).set k a = (as.set (i + k) a (by simp at h; omega)).extract i j := by
   ext l h₁ h₂
   · simp
   · simp_all [getElem_set]
 
-@[simp]
+@[simp, grind =]
 theorem extract_append {as bs : Array α} {i j : Nat} :
     (as ++ bs).extract i j = as.extract i j ++ bs.extract (i - as.size) (j - as.size) := by
   ext l h₁ h₂
@@ -242,14 +244,14 @@ theorem extract_append_right {as bs : Array α} :
     (as ++ bs).extract as.size (as.size + i) = bs.extract 0 i := by
   simp
 
-@[simp] theorem map_extract {as : Array α} {i j : Nat} :
+@[simp, grind =] theorem map_extract {as : Array α} {i j : Nat} :
     (as.extract i j).map f = (as.map f).extract i j := by
   ext l h₁ h₂
   · simp
   · simp only [size_map, size_extract] at h₁ h₂
     simp only [getElem_map, getElem_extract]
 
-@[simp] theorem extract_replicate {a : α} {n i j : Nat} :
+@[simp, grind =] theorem extract_replicate {a : α} {n i j : Nat} :
     (replicate n a).extract i j = replicate (min j n - i) a := by
   ext l h₁ h₂
   · simp
@@ -297,6 +299,7 @@ theorem set_eq_push_extract_append_extract {as : Array α} {i : Nat} (h : i < as
   simp at h
   simp [List.set_eq_take_append_cons_drop, h, List.take_of_length_le]
 
+@[grind =]
 theorem extract_reverse {as : Array α} {i j : Nat} :
     as.reverse.extract i j = (as.extract (as.size - j) (as.size - i)).reverse := by
   ext l h₁ h₂
@@ -307,6 +310,7 @@ theorem extract_reverse {as : Array α} {i j : Nat} :
     congr 1
     omega
 
+@[grind =]
 theorem reverse_extract {as : Array α} {i j : Nat} :
     (as.extract i j).reverse = as.reverse.extract (as.size - j) (as.size - i) := by
   rw [extract_reverse]

src/Init/Data/Array/InsertIdx.lean

@@ -47,11 +47,16 @@ theorem insertIdx_zero {xs : Array α} {x : α} : xs.insertIdx 0 x = #[x] ++ xs
   simp at h
   simp [List.length_insertIdx, h]
 
-theorem eraseIdx_insertIdx {i : Nat} {xs : Array α} (h : i ≤ xs.size) :
+theorem eraseIdx_insertIdx_self {i : Nat} {xs : Array α} (h : i ≤ xs.size) :
     (xs.insertIdx i a).eraseIdx i (by simp; omega) = xs := by
   rcases xs with ⟨xs⟩
   simp_all
 
+@[deprecated eraseIdx_insertIdx_self (since := "2025-06-15")]
+theorem eraseIdx_insertIdx {i : Nat} {xs : Array α} (h : i ≤ xs.size) :
+    (xs.insertIdx i a).eraseIdx i (by simp; omega) = xs := by
+  simp [eraseIdx_insertIdx_self]
+
 theorem insertIdx_eraseIdx_of_ge {as : Array α}
     (w₁ : i < as.size) (w₂ : j ≤ (as.eraseIdx i).size) (h : i ≤ j) :
     (as.eraseIdx i).insertIdx j a =
@@ -66,6 +71,18 @@ theorem insertIdx_eraseIdx_of_le {as : Array α}
   cases as
   simpa using List.insertIdx_eraseIdx_of_le (by simpa) (by simpa)
 
+@[grind =]
+theorem insertIdx_eraseIdx {as : Array α} (h₁ : i < as.size) (h₂ : j ≤ (as.eraseIdx i).size) :
+    (as.eraseIdx i).insertIdx j a =
+      if h : i ≤ j then
+        (as.insertIdx (j + 1) a (by simp_all; omega)).eraseIdx i (by simp_all; omega)
+      else
+        (as.insertIdx j a).eraseIdx (i + 1) (by simp_all) := by
+  split <;> rename_i h'
+  · rw [insertIdx_eraseIdx_of_ge] <;> omega
+  · rw [insertIdx_eraseIdx_of_le] <;> omega
+
+@[grind =]
 theorem insertIdx_comm (a b : α) {i j : Nat} {xs : Array α} (_ : i ≤ j) (_ : j ≤ xs.size) :
     (xs.insertIdx i a).insertIdx (j + 1) b (by simpa) =
       (xs.insertIdx j b).insertIdx i a (by simp; omega) := by
@@ -81,6 +98,7 @@ theorem insertIdx_size_self {xs : Array α} {x : α} : xs.insertIdx xs.size x =
   rcases xs with ⟨xs⟩
   simp
 
+@[grind =]
 theorem getElem_insertIdx {xs : Array α} {x : α} {i k : Nat} (w : i ≤ xs.size) (h : k < (xs.insertIdx i x).size) :
     (xs.insertIdx i x)[k] =
       if h₁ : k < i then
@@ -106,6 +124,7 @@ theorem getElem_insertIdx_of_gt {xs : Array α} {x : α} {i k : Nat} (w : k ≤
   simp [getElem_insertIdx, w, h]
   rw [dif_neg (by omega), dif_neg (by omega)]
 
+@[grind =]
 theorem getElem?_insertIdx {xs : Array α} {x : α} {i k : Nat} (h : i ≤ xs.size) :
     (xs.insertIdx i x)[k]? =
       if k < i then

src/Init/Data/Array/Lemmas.lean

@@ -89,6 +89,8 @@ theorem size_pos_of_mem {a : α} {xs : Array α} (h : a ∈ xs) : 0 < xs.size :=
   simp only [mem_toArray] at h
   simpa using List.length_pos_of_mem h
 
+grind_pattern size_pos_of_mem => a ∈ xs, xs.size
+
 theorem exists_mem_of_size_pos {xs : Array α} (h : 0 < xs.size) : ∃ a, a ∈ xs := by
   cases xs
   simpa using List.exists_mem_of_length_pos h

src/Init/Data/Array/Perm.lean

@@ -91,17 +91,26 @@ theorem Perm.mem_iff {a : α} {xs ys : Array α} (p : xs ~ ys) : a ∈ xs ↔ a
   simp only [perm_iff_toList_perm] at p
   simpa using p.mem_iff
 
+grind_pattern Perm.mem_iff => xs ~ ys, a ∈ xs
+grind_pattern Perm.mem_iff => xs ~ ys, a ∈ ys
+
 theorem Perm.append {xs ys as bs : Array α} (p₁ : xs ~ ys) (p₂ : as ~ bs) :
     xs ++ as ~ ys ++ bs := by
   cases xs; cases ys; cases as; cases bs
   simp only [append_toArray, perm_iff_toList_perm] at p₁ p₂ ⊢
   exact p₁.append p₂
 
+grind_pattern Perm.append => xs ~ ys, as ~ bs, xs ++ as
+grind_pattern Perm.append => xs ~ ys, as ~ bs, ys ++ bs
+
 theorem Perm.push (x : α) {xs ys : Array α} (p : xs ~ ys) :
     xs.push x ~ ys.push x := by
   rw [push_eq_append_singleton]
   exact p.append .rfl
 
+grind_pattern Perm.push => xs ~ ys, xs.push x
+grind_pattern Perm.push => xs ~ ys, ys.push x
+
 theorem Perm.push_comm (x y : α) {xs ys : Array α} (p : xs ~ ys) :
     (xs.push x).push y ~ (ys.push y).push x := by
   cases xs; cases ys

src/Init/Data/Array/Range.lean

@@ -128,6 +128,16 @@ theorem erase_range' :
   simp only [← List.toArray_range', List.erase_toArray]
   simp [List.erase_range']
 
+@[simp, grind =]
+theorem count_range' {a s n step} (h : 0 < step := by simp) :
+    count a (range' s n step) = if ∃ i, i < n ∧ a = s + step * i then 1 else 0 := by
+  rw [← List.toArray_range', List.count_toArray, ← List.count_range' h]
+
+@[simp, grind =]
+theorem count_range_1' {a s n} :
+    count a (range' s n) = if s ≤ a ∧ a < s + n then 1 else 0 := by
+  rw [← List.toArray_range', List.count_toArray, ← List.count_range_1']
+
 /-! ### range -/
 
 @[grind _=_]
@@ -179,11 +189,11 @@ theorem self_mem_range_succ {n : Nat} : n ∈ range (n + 1) := by simp
 @[simp, grind =] theorem take_range {i n : Nat} : take (range n) i = range (min i n) := by
   ext <;> simp
 
-@[simp] theorem find?_range_eq_some {n : Nat} {i : Nat} {p : Nat → Bool} :
+@[simp, grind =] theorem find?_range_eq_some {n : Nat} {i : Nat} {p : Nat → Bool} :
     (range n).find? p = some i ↔ p i ∧ i ∈ range n ∧ ∀ j, j < i → !p j := by
   simp [range_eq_range']
 
-@[simp] theorem find?_range_eq_none {n : Nat} {p : Nat → Bool} :
+@[simp, grind =] theorem find?_range_eq_none {n : Nat} {p : Nat → Bool} :
     (range n).find? p = none ↔ ∀ i, i < n → !p i := by
   simp only [← List.toArray_range, List.find?_toArray, List.find?_range_eq_none]
 
@@ -191,6 +201,10 @@ theorem self_mem_range_succ {n : Nat} : n ∈ range (n + 1) := by simp
 theorem erase_range : (range n).erase i = range (min n i) ++ range' (i + 1) (n - (i + 1)) := by
   simp [range_eq_range', erase_range']
 
+@[simp, grind =]
+theorem count_range {a n} :
+    count a (range n) = if a < n then 1 else 0 := by
+  rw [← List.toArray_range, List.count_toArray, ← List.count_range]
 
 /-! ### zipIdx -/
 
@@ -199,7 +213,7 @@ theorem zipIdx_eq_empty_iff {xs : Array α} {i : Nat} : xs.zipIdx i = #[] ↔ xs
   cases xs
   simp
 
-@[simp]
+@[simp, grind =]
 theorem getElem?_zipIdx {xs : Array α} {i j} : (zipIdx xs i)[j]? = xs[j]?.map fun a => (a, i + j) := by
   simp [getElem?_def]
 
@@ -242,7 +256,7 @@ theorem zipIdx_eq_map_add {xs : Array α} {i : Nat} :
   simp only [zipIdx_toArray, List.map_toArray, mk.injEq]
   rw [List.zipIdx_eq_map_add]
 
-@[simp]
+@[simp, grind =]
 theorem zipIdx_singleton {x : α} {k : Nat} : zipIdx #[x] k = #[(x, k)] :=
   rfl
 
@@ -290,6 +304,7 @@ theorem zipIdx_map {xs : Array α} {k : Nat} {f : α → β} :
   cases xs
   simp [List.zipIdx_map]
 
+@[grind =]
 theorem zipIdx_append {xs ys : Array α} {k : Nat} :
     zipIdx (xs ++ ys) k = zipIdx xs k ++ zipIdx ys (k + xs.size) := by
   cases xs

src/Init/Data/List/Basic.lean

@@ -673,7 +673,7 @@ instance : Std.Associative (α := List α) (· ++ ·) := ⟨append_assoc⟩
 theorem append_cons (as : List α) (b : α) (bs : List α) : as ++ b :: bs = as ++ [b] ++ bs := by
   simp
 
-@[simp] theorem concat_eq_append {as : List α} {a : α} : as.concat a = as ++ [a] := by
+@[simp, grind =] theorem concat_eq_append {as : List α} {a : α} : as.concat a = as ++ [a] := by
   induction as <;> simp [concat, *]
 
 theorem reverseAux_eq_append {as bs : List α} : reverseAux as bs = reverseAux as [] ++ bs := by

src/Init/Data/List/Count.lean

@@ -64,8 +64,8 @@ theorem length_eq_countP_add_countP (p : α → Bool) {l : List α} : length l =
       · rfl
       · simp [h]
 
-@[grind =]
-theorem countP_eq_length_filter {l : List α} : countP p l = length (filter p l) := by
+@[grind _=_]  -- This to quite aggressive, as it introduces `filter` based reasoning whenever we see `countP`.
+theorem countP_eq_length_filter {l : List α} : countP p l = (filter p l).length := by
   induction l with
   | nil => rfl
   | cons x l ih =>
@@ -82,7 +82,7 @@ theorem countP_le_length : countP p l ≤ l.length := by
   simp only [countP_eq_length_filter]
   apply length_filter_le
 
-@[simp] theorem countP_append {l₁ l₂ : List α} : countP p (l₁ ++ l₂) = countP p l₁ + countP p l₂ := by
+@[simp, grind =] theorem countP_append {l₁ l₂ : List α} : countP p (l₁ ++ l₂) = countP p l₁ + countP p l₂ := by
   simp only [countP_eq_length_filter, filter_append, length_append]
 
 @[simp] theorem countP_pos_iff {p} : 0 < countP p l ↔ ∃ a ∈ l, p a := by
@@ -120,10 +120,24 @@ theorem Sublist.countP_le (s : l₁ <+ l₂) : countP p l₁ ≤ countP p l₂ :
   simp only [countP_eq_length_filter]
   apply s.filter _ |>.length_le
 
+grind_pattern Sublist.countP_le => l₁ <+ l₂, countP p l₁
+grind_pattern Sublist.countP_le => l₁ <+ l₂, countP p l₂
+
 theorem IsPrefix.countP_le (s : l₁ <+: l₂) : countP p l₁ ≤ countP p l₂ := s.sublist.countP_le
+
+grind_pattern IsPrefix.countP_le => l₁ <+: l₂, countP p l₁
+grind_pattern IsPrefix.countP_le => l₁ <+: l₂, countP p l₂
+
 theorem IsSuffix.countP_le (s : l₁ <:+ l₂) : countP p l₁ ≤ countP p l₂ := s.sublist.countP_le
+
+grind_pattern IsSuffix.countP_le => l₁ <:+ l₂, countP p l₁
+grind_pattern IsSuffix.countP_le => l₁ <:+ l₂, countP p l₂
+
 theorem IsInfix.countP_le (s : l₁ <:+: l₂) : countP p l₁ ≤ countP p l₂ := s.sublist.countP_le
 
+grind_pattern IsInfix.countP_le => l₁ <:+: l₂, countP p l₁
+grind_pattern IsInfix.countP_le => l₁ <:+: l₂, countP p l₂
+
 -- See `Init.Data.List.Nat.Count` for `Sublist.le_countP : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁`.
 
 @[grind]
@@ -174,7 +188,7 @@ theorem countP_flatMap {p : β → Bool} {l : List α} {f : α → List β} :
     countP p (l.flatMap f) = sum (map (countP p ∘ f) l) := by
   rw [List.flatMap, countP_flatten, map_map]
 
-@[simp] theorem countP_reverse {l : List α} : countP p l.reverse = countP p l := by
+@[simp, grind =] theorem countP_reverse {l : List α} : countP p l.reverse = countP p l := by
   simp [countP_eq_length_filter, filter_reverse]
 
 theorem countP_mono_left (h : ∀ x ∈ l, p x → q x) : countP p l ≤ countP q l := by
@@ -203,18 +217,22 @@ section count
 
 variable [BEq α]
 
-@[simp] theorem count_nil {a : α} : count a [] = 0 := rfl
+@[simp, grind =] theorem count_nil {a : α} : count a [] = 0 := rfl
 
 @[grind]
 theorem count_cons {a b : α} {l : List α} :
     count a (b :: l) = count a l + if b == a then 1 else 0 := by
   simp [count, countP_cons]
 
-@[grind =] theorem count_eq_countP {a : α} {l : List α} : count a l = countP (· == a) l := rfl
+theorem count_eq_countP {a : α} {l : List α} : count a l = countP (· == a) l := rfl
 theorem count_eq_countP' {a : α} : count a = countP (· == a) := by
   funext l
   apply count_eq_countP
 
+@[grind =]
+theorem count_eq_length_filter {a : α} {l : List α} : count a l = (filter (· == a) l).length := by
+  simp [count, countP_eq_length_filter]
+
 @[grind]
 theorem count_tail : ∀ {l : List α} {a : α},
       l.tail.count a = l.count a - if l.head? == some a then 1 else 0
@@ -223,12 +241,28 @@ theorem count_tail : ∀ {l : List α} {a : α},
 
 theorem count_le_length {a : α} {l : List α} : count a l ≤ l.length := countP_le_length
 
+grind_pattern count_le_length => count a l
+
 theorem Sublist.count_le (a : α) (h : l₁ <+ l₂) : count a l₁ ≤ count a l₂ := h.countP_le
 
+grind_pattern Sublist.count_le => l₁ <+ l₂, count a l₁
+grind_pattern Sublist.count_le => l₁ <+ l₂, count a l₂
+
 theorem IsPrefix.count_le (a : α) (h : l₁ <+: l₂) : count a l₁ ≤ count a l₂ := h.sublist.count_le a
+
+grind_pattern IsPrefix.count_le => l₁ <+: l₂, count a l₁
+grind_pattern IsPrefix.count_le => l₁ <+: l₂, count a l₂
+
 theorem IsSuffix.count_le (a : α) (h : l₁ <:+ l₂) : count a l₁ ≤ count a l₂ := h.sublist.count_le a
+
+grind_pattern IsSuffix.count_le => l₁ <:+ l₂, count a l₁
+grind_pattern IsSuffix.count_le => l₁ <:+ l₂, count a l₂
+
 theorem IsInfix.count_le (a : α) (h : l₁ <:+: l₂) : count a l₁ ≤ count a l₂ := h.sublist.count_le a
 
+grind_pattern IsInfix.count_le => l₁ <:+: l₂, count a l₁
+grind_pattern IsInfix.count_le => l₁ <:+: l₂, count a l₂
+
 -- See `Init.Data.List.Nat.Count` for `Sublist.le_count : count a l₂ - (l₂.length - l₁.length) ≤ countP a l₁`.
 
 theorem count_tail_le {a : α} {l : List α} : count a l.tail ≤ count a l :=
@@ -245,10 +279,11 @@ theorem count_singleton {a b : α} : count a [b] = if b == a then 1 else 0 := by
 @[simp, grind =] theorem count_append {a : α} {l₁ l₂ : List α} : count a (l₁ ++ l₂) = count a l₁ + count a l₂ :=
   countP_append
 
+@[grind =]
 theorem count_flatten {a : α} {l : List (List α)} : count a l.flatten = (l.map (count a)).sum := by
   simp only [count_eq_countP, countP_flatten, count_eq_countP']
 
-@[simp] theorem count_reverse {a : α} {l : List α} : count a l.reverse = count a l := by
+@[simp, grind =] theorem count_reverse {a : α} {l : List α} : count a l.reverse = count a l := by
   simp only [count_eq_countP, countP_eq_length_filter, filter_reverse, length_reverse]
 
 @[grind]

src/Init/Data/List/Lemmas.lean

@@ -109,9 +109,11 @@ abbrev length_eq_zero := @length_eq_zero_iff
 theorem eq_nil_iff_length_eq_zero : l = [] ↔ length l = 0 :=
   length_eq_zero_iff.symm
 
-@[grind →] theorem length_pos_of_mem {a : α} : ∀ {l : List α}, a ∈ l → 0 < length l
+theorem length_pos_of_mem {a : α} : ∀ {l : List α}, a ∈ l → 0 < length l
   | _::_, _ => Nat.zero_lt_succ _
 
+grind_pattern length_pos_of_mem => a ∈ l, length l
+
 theorem exists_mem_of_length_pos : ∀ {l : List α}, 0 < length l → ∃ a, a ∈ l
   | _::_, _ => ⟨_, .head ..⟩
 
@@ -2740,11 +2742,11 @@ def foldlRecOn {motive : β → Sort _} : ∀ (l : List α) (op : β → α →
     foldlRecOn tl op (hl b hb hd mem_cons_self)
       fun y hy x hx => hl y hy x (mem_cons_of_mem hd hx)
 
-@[simp] theorem foldlRecOn_nil {motive : β → Sort _} {op : β → α → β} (hb : motive b)
+@[simp, grind =] theorem foldlRecOn_nil {motive : β → Sort _} {op : β → α → β} (hb : motive b)
     (hl : ∀ (b : β) (_ : motive b) (a : α) (_ : a ∈ []), motive (op b a)) :
     foldlRecOn [] op hb hl = hb := rfl
 
-@[simp] theorem foldlRecOn_cons {motive : β → Sort _} {op : β → α → β} (hb : motive b)
+@[simp, grind =] theorem foldlRecOn_cons {motive : β → Sort _} {op : β → α → β} (hb : motive b)
     (hl : ∀ (b : β) (_ : motive b) (a : α) (_ : a ∈ x :: l), motive (op b a)) :
     foldlRecOn (x :: l) op hb hl =
       foldlRecOn l op (hl b hb x mem_cons_self)
@@ -2775,11 +2777,11 @@ def foldrRecOn {motive : β → Sort _} : ∀ (l : List α) (op : α → β →
     hl (foldr op b l)
       (foldrRecOn l op hb fun b c a m => hl b c a (mem_cons_of_mem x m)) x mem_cons_self
 
-@[simp] theorem foldrRecOn_nil {motive : β → Sort _} {op : α → β → β} (hb : motive b)
+@[simp, grind =] theorem foldrRecOn_nil {motive : β → Sort _} {op : α → β → β} (hb : motive b)
     (hl : ∀ (b : β) (_ : motive b) (a : α) (_ : a ∈ []), motive (op a b)) :
     foldrRecOn [] op hb hl = hb := rfl
 
-@[simp] theorem foldrRecOn_cons {motive : β → Sort _} {op : α → β → β} (hb : motive b)
+@[simp, grind =] theorem foldrRecOn_cons {motive : β → Sort _} {op : α → β → β} (hb : motive b)
     (hl : ∀ (b : β) (_ : motive b) (a : α) (_ : a ∈ x :: l), motive (op a b)) :
     foldrRecOn (x :: l) op hb hl =
       hl _ (foldrRecOn l op hb fun b c a m => hl b c a (mem_cons_of_mem x m))
@@ -2915,13 +2917,13 @@ theorem getLast_filterMap_of_eq_some {f : α → Option β} {l : List α} (w : l
   rw [head_filterMap_of_eq_some (by simp_all)]
   simp_all
 
-theorem getLast?_flatMap {l : List α} {f : α → List β} :
+@[grind =] theorem getLast?_flatMap {l : List α} {f : α → List β} :
     (l.flatMap f).getLast? = l.reverse.findSome? fun a => (f a).getLast? := by
   simp only [← head?_reverse, reverse_flatMap]
   rw [head?_flatMap]
   rfl
 
-theorem getLast?_flatten {L : List (List α)} :
+@[grind =] theorem getLast?_flatten {L : List (List α)} :
     (flatten L).getLast? = L.reverse.findSome? fun l => l.getLast? := by
   simp [← flatMap_id, getLast?_flatMap]
 
@@ -2936,7 +2938,7 @@ theorem getLast?_replicate {a : α} {n : Nat} : (replicate n a).getLast? = if n
 /-! ### leftpad -/
 
 -- We unfold `leftpad` and `rightpad` for verification purposes.
-attribute [simp] leftpad rightpad
+attribute [simp, grind] leftpad rightpad
 
 -- `length_leftpad` and `length_rightpad` are in `Init.Data.List.Nat.Basic`.
 
@@ -3040,6 +3042,9 @@ we do not separately develop much theory about it.
 theorem mem_partition : a ∈ l ↔ a ∈ (partition p l).1 ∨ a ∈ (partition p l).2 := by
   by_cases p a <;> simp_all
 
+grind_pattern mem_partition => a ∈ (partition p l).1
+grind_pattern mem_partition => a ∈ (partition p l).2
+
 /-! ### dropLast
 
 `dropLast` is the specification for `Array.pop`, so theorems about `List.dropLast`
@@ -3111,7 +3116,7 @@ theorem dropLast_concat_getLast : ∀ {l : List α} (h : l ≠ []), dropLast l +
     congr
     exact dropLast_concat_getLast (cons_ne_nil b l)
 
-@[simp] theorem map_dropLast {f : α → β} {l : List α} : l.dropLast.map f = (l.map f).dropLast := by
+@[simp, grind _=_] theorem map_dropLast {f : α → β} {l : List α} : l.dropLast.map f = (l.map f).dropLast := by
   induction l with
   | nil => rfl
   | cons x xs ih => cases xs <;> simp [ih]
@@ -3123,6 +3128,7 @@ theorem dropLast_concat_getLast : ∀ {l : List α} (h : l ≠ []), dropLast l +
     rw [cons_append, dropLast, dropLast_append_of_ne_nil h, cons_append]
     simp [h]
 
+@[grind =]
 theorem dropLast_append {l₁ l₂ : List α} :
     (l₁ ++ l₂).dropLast = if l₂.isEmpty then l₁.dropLast else l₁ ++ l₂.dropLast := by
   split <;> simp_all
@@ -3130,9 +3136,9 @@ theorem dropLast_append {l₁ l₂ : List α} :
 theorem dropLast_append_cons : dropLast (l₁ ++ b :: l₂) = l₁ ++ dropLast (b :: l₂) := by
   simp
 
-@[simp] theorem dropLast_concat : dropLast (l₁ ++ [b]) = l₁ := by simp
+@[simp, grind =] theorem dropLast_concat : dropLast (l₁ ++ [b]) = l₁ := by simp
 
-@[simp] theorem dropLast_replicate {n : Nat} {a : α} : dropLast (replicate n a) = replicate (n - 1) a := by
+@[simp, grind =] theorem dropLast_replicate {n : Nat} {a : α} : dropLast (replicate n a) = replicate (n - 1) a := by
   match n with
   | 0 => simp
   | 1 => simp [replicate_succ]
@@ -3145,7 +3151,7 @@ theorem dropLast_append_cons : dropLast (l₁ ++ b :: l₂) = l₁ ++ dropLast (
     dropLast (a :: replicate n a) = replicate n a := by
   rw [← replicate_succ, dropLast_replicate, Nat.add_sub_cancel]
 
-@[simp] theorem tail_reverse {l : List α} : l.reverse.tail = l.dropLast.reverse := by
+@[simp, grind _=_] theorem tail_reverse {l : List α} : l.reverse.tail = l.dropLast.reverse := by
   apply ext_getElem
   · simp
   · intro i h₁ h₂
@@ -3385,6 +3391,7 @@ theorem replace_append_right [LawfulBEq α] {l₁ l₂ : List α} (h : ¬ a ∈
     (l₁ ++ l₂).replace a b = l₁ ++ l₂.replace a b := by
   simp [replace_append, h]
 
+@[grind _=_]
 theorem replace_take {l : List α} {i : Nat} :
     (l.take i).replace a b = (l.replace a b).take i := by
   induction l generalizing i with
@@ -3551,10 +3558,10 @@ end insert
 
 /-! ### `removeAll` -/
 
-@[simp] theorem removeAll_nil [BEq α] {xs : List α} : xs.removeAll [] = xs := by
+@[simp, grind =] theorem removeAll_nil [BEq α] {xs : List α} : xs.removeAll [] = xs := by
   simp [removeAll]
 
-theorem cons_removeAll [BEq α] {x : α} {xs ys : List α} :
+@[grind =] theorem cons_removeAll [BEq α] {x : α} {xs ys : List α} :
     (x :: xs).removeAll ys =
       if ys.contains x = false then
         x :: xs.removeAll ys
@@ -3562,6 +3569,7 @@ theorem cons_removeAll [BEq α] {x : α} {xs ys : List α} :
         xs.removeAll ys := by
   simp [removeAll, filter_cons]
 
+@[grind =]
 theorem removeAll_cons [BEq α] {xs : List α} {y : α} {ys : List α} :
     xs.removeAll (y :: ys) = (xs.filter fun x => !x == y).removeAll ys := by
   simp [removeAll, Bool.and_comm]
@@ -3581,7 +3589,7 @@ theorem removeAll_cons [BEq α] {xs : List α} {y : α} {ys : List α} :
 
 /-! ### `eraseDupsBy` and `eraseDups` -/
 
-@[simp] theorem eraseDupsBy_nil : ([] : List α).eraseDupsBy r = [] := rfl
+@[simp, grind =] theorem eraseDupsBy_nil : ([] : List α).eraseDupsBy r = [] := rfl
 
 private theorem eraseDupsBy_loop_cons {as bs : List α} {r : α → α → Bool} :
     eraseDupsBy.loop r as bs = bs.reverse ++ eraseDupsBy.loop r (as.filter fun a => !bs.any (r a)) [] := by
@@ -3601,17 +3609,19 @@ private theorem eraseDupsBy_loop_cons {as bs : List α} {r : α → α → Bool}
       simp
 termination_by as.length
 
+@[grind =]
 theorem eraseDupsBy_cons :
     (a :: as).eraseDupsBy r = a :: (as.filter fun b => r b a = false).eraseDupsBy r := by
   simp only [eraseDupsBy, eraseDupsBy.loop, any_nil]
   rw [eraseDupsBy_loop_cons]
   simp
 
-@[simp] theorem eraseDups_nil [BEq α] : ([] : List α).eraseDups = [] := rfl
-theorem eraseDups_cons [BEq α] {a : α} {as : List α} :
+@[simp, grind =] theorem eraseDups_nil [BEq α] : ([] : List α).eraseDups = [] := rfl
+@[grind =] theorem eraseDups_cons [BEq α] {a : α} {as : List α} :
     (a :: as).eraseDups = a :: (as.filter fun b => !b == a).eraseDups := by
   simp [eraseDups, eraseDupsBy_cons]
 
+@[grind =]
 theorem eraseDups_append [BEq α] [LawfulBEq α] {as bs : List α} :
     (as ++ bs).eraseDups = as.eraseDups ++ (bs.removeAll as).eraseDups := by
   match as with

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

@@ -26,6 +26,7 @@ namespace List
 
 /-! ### dropLast -/
 
+@[grind _=_]
 theorem tail_dropLast {l : List α} : tail (dropLast l) = dropLast (tail l) := by
   ext1
   simp only [getElem?_tail, getElem?_dropLast, length_tail]
@@ -35,7 +36,7 @@ theorem tail_dropLast {l : List α} : tail (dropLast l) = dropLast (tail l) := b
   · omega
   · rfl
 
-@[simp] theorem dropLast_reverse {l : List α} : l.reverse.dropLast = l.tail.reverse := by
+@[simp, grind _=_] theorem dropLast_reverse {l : List α} : l.reverse.dropLast = l.tail.reverse := by
   apply ext_getElem
   · simp
   · intro i h₁ h₂
@@ -114,7 +115,7 @@ section intersperse
 
 variable {l : List α} {sep : α} {i : Nat}
 
-@[simp] theorem length_intersperse : (l.intersperse sep).length = 2 * l.length - 1 := by
+@[simp, grind =] theorem length_intersperse : (l.intersperse sep).length = 2 * l.length - 1 := by
   fun_induction intersperse <;> simp only [intersperse, length_cons, length_nil] at *
   rename_i h _
   have := length_pos_iff.mpr h

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

@@ -16,6 +16,7 @@ namespace List
 
 open Nat
 
+@[grind =]
 theorem countP_set {p : α → Bool} {l : List α} {i : Nat} {a : α} (h : i < l.length) :
     (l.set i a).countP p = l.countP p - (if p l[i] then 1 else 0) + (if p a then 1 else 0) := by
   induction l generalizing i with
@@ -29,10 +30,12 @@ theorem countP_set {p : α → Bool} {l : List α} {i : Nat} {a : α} (h : i < l
       have : (if p l[i] = true then 1 else 0) ≤ l.countP p := boole_getElem_le_countP (p := p) h
       omega
 
+@[grind =]
 theorem count_set [BEq α] {a b : α} {l : List α} {i : Nat} (h : i < l.length) :
     (l.set i a).count b = l.count b - (if l[i] == b then 1 else 0) + (if a == b then 1 else 0) := by
   simp [count_eq_countP, countP_set, h]
 
+@[grind =]
 theorem countP_replace [BEq α] [LawfulBEq α] {a b : α} {l : List α} {p : α → Bool} :
     (l.replace a b).countP p =
       if l.contains a then l.countP p + (if p b then 1 else 0) - (if p a then 1 else 0) else l.countP p := by
@@ -55,11 +58,31 @@ theorem countP_replace [BEq α] [LawfulBEq α] {a b : α} {l : List α} {p : α
           omega
       · omega
 
+@[grind =]
 theorem count_replace [BEq α] [LawfulBEq α] {a b c : α} {l : List α} :
     (l.replace a b).count c =
       if l.contains a then l.count c + (if b == c then 1 else 0) - (if a == c then 1 else 0) else l.count c := by
   simp [count_eq_countP, countP_replace]
 
+@[grind =] theorem count_insert [BEq α] [LawfulBEq α] {a b : α} {l : List α} :
+    count a (List.insert b l) = max (count a l) (if b == a then 1 else 0) := by
+  simp only [List.insert, contains_eq_mem, decide_eq_true_eq, beq_iff_eq]
+  split <;> rename_i h
+  · split <;> rename_i h'
+    · rw [Nat.max_def]
+      simp only [beq_iff_eq] at h'
+      split
+      · have := List.count_pos_iff.mpr (h' ▸ h)
+        omega
+      · rfl
+    · simp [h']
+  · rw [count_cons]
+    split <;> rename_i h'
+    · simp only [beq_iff_eq] at h'
+      rw [count_eq_zero.mpr (h' ▸ h)]
+      simp [h']
+    · simp
+
 /--
 The number of elements satisfying a predicate in a sublist is at least the number of elements satisfying the predicate in the list,
 minus the difference in the lengths.
@@ -80,15 +103,23 @@ theorem Sublist.le_countP (s : l₁ <+ l₂) (p) : countP p l₂ - (l₂.length
     have := s.length_le
     split <;> omega
 
+grind_pattern Sublist.le_countP => l₁ <+ l₂, countP p l₁, countP p l₂
+
 theorem IsPrefix.le_countP (s : l₁ <+: l₂) : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁ :=
   s.sublist.le_countP _
 
+grind_pattern IsPrefix.le_countP => l₁ <+: l₂, countP p l₁, countP p l₂
+
 theorem IsSuffix.le_countP (s : l₁ <:+ l₂) : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁ :=
   s.sublist.le_countP _
 
+grind_pattern IsSuffix.le_countP => l₁ <:+ l₂, countP p l₁, countP p l₂
+
 theorem IsInfix.le_countP (s : l₁ <:+: l₂) : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁ :=
   s.sublist.le_countP _
 
+grind_pattern IsInfix.le_countP => l₁ <:+: l₂, countP p l₁, countP p l₂
+
 /--
 The number of elements satisfying a predicate in the tail of a list is
 at least one less than the number of elements satisfying the predicate in the list.
@@ -98,21 +129,33 @@ theorem le_countP_tail {l} : countP p l - 1 ≤ countP p l.tail := by
   simp only [length_tail] at this
   omega
 
+grind_pattern le_countP_tail => countP p l.tail
+
 variable [BEq α]
 
 theorem Sublist.le_count (s : l₁ <+ l₂) (a : α) : count a l₂ - (l₂.length - l₁.length) ≤ count a l₁ :=
   s.le_countP _
 
+grind_pattern Sublist.le_count => l₁ <+ l₂, count a l₁, count a l₂
+
 theorem IsPrefix.le_count (s : l₁ <+: l₂) (a : α) : count a l₂ - (l₂.length - l₁.length) ≤ count a l₁ :=
   s.sublist.le_count _
 
+grind_pattern IsPrefix.le_count => l₁ <+: l₂, count a l₁, count a l₂
+
 theorem IsSuffix.le_count (s : l₁ <:+ l₂) (a : α) : count a l₂ - (l₂.length - l₁.length) ≤ count a l₁ :=
   s.sublist.le_count _
 
+grind_pattern IsSuffix.le_count => l₁ <:+ l₂, count a l₁, count a l₂
+
 theorem IsInfix.le_count (s : l₁ <:+: l₂) (a : α) : count a l₂ - (l₂.length - l₁.length) ≤ count a l₁ :=
   s.sublist.le_count _
 
+grind_pattern IsInfix.le_count => l₁ <:+: l₂, count a l₁, count a l₂
+
 theorem le_count_tail {a : α} {l : List α} : count a l - 1 ≤ count a l.tail :=
   le_countP_tail
 
+grind_pattern le_count_tail => count a l.tail
+
 end List

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

@@ -187,7 +187,7 @@ theorem set_eraseIdx {xs : List α} {i : Nat} {j : Nat} {a : α} :
       · have t : ¬ n < i := by omega
         simp [t]
 
-@[simp] theorem eraseIdx_length_sub_one {l : List α} :
+@[simp, grind =] theorem eraseIdx_length_sub_one {l : List α} :
     (l.eraseIdx (l.length - 1)) = l.dropLast := by
   apply ext_getElem
   · simp [length_eraseIdx]

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

@@ -30,19 +30,20 @@ section InsertIdx
 
 variable {a : α}
 
-@[simp]
+@[simp, grind =]
 theorem insertIdx_zero {xs : List α} {x : α} : xs.insertIdx 0 x = x :: xs :=
   rfl
 
-@[simp]
+@[simp, grind =]
 theorem insertIdx_succ_nil {n : Nat} {a : α} : ([] : List α).insertIdx (n + 1) a = [] :=
   rfl
 
-@[simp]
+@[simp, grind =]
 theorem insertIdx_succ_cons {xs : List α} {hd x : α} {i : Nat} :
     (hd :: xs).insertIdx (i + 1) x = hd :: xs.insertIdx i x :=
   rfl
 
+@[grind =]
 theorem length_insertIdx : ∀ {i} {as : List α}, (as.insertIdx i a).length = if i ≤ as.length then as.length + 1 else as.length
   | 0, _ => by simp
   | n + 1, [] => by simp
@@ -56,14 +57,9 @@ theorem length_insertIdx_of_le_length (h : i ≤ length as) (a : α) : (as.inser
 theorem length_insertIdx_of_length_lt (h : length as < i) (a : α) : (as.insertIdx i a).length = as.length := by
   simp [length_insertIdx, h]
 
-@[simp]
-theorem eraseIdx_insertIdx {i : Nat} {l : List α} (a : α) : (l.insertIdx i a).eraseIdx i = l := by
-  rw [eraseIdx_eq_modifyTailIdx, insertIdx, modifyTailIdx_modifyTailIdx_self]
-  exact modifyTailIdx_id _ _
-
 theorem insertIdx_eraseIdx_of_ge :
-    ∀ {i m as},
-      i < length as → i ≤ m → (as.eraseIdx i).insertIdx m a = (as.insertIdx (m + 1) a).eraseIdx i
+    ∀ {i j as},
+      i < length as → i ≤ j → (as.eraseIdx i).insertIdx j a = (as.insertIdx (j + 1) a).eraseIdx i
   | 0, 0, [], has, _ => (Nat.lt_irrefl _ has).elim
   | 0, 0, _ :: as, _, _ => by simp [eraseIdx, insertIdx]
   | 0, _ + 1, _ :: _, _, _ => rfl
@@ -79,6 +75,15 @@ theorem insertIdx_eraseIdx_of_le :
     congrArg (cons a) <|
       insertIdx_eraseIdx_of_le (Nat.lt_of_succ_lt_succ has) (Nat.le_of_succ_le_succ hmn)
 
+@[grind =]
+theorem insertIdx_eraseIdx (h : i < length as) :
+    (as.eraseIdx i).insertIdx j a =
+      if i ≤ j then (as.insertIdx (j + 1) a).eraseIdx i else (as.insertIdx j a).eraseIdx (i + 1) := by
+  split <;> rename_i h'
+  · rw [insertIdx_eraseIdx_of_ge h h']
+  · rw [insertIdx_eraseIdx_of_le h (by omega)]
+
+@[grind =]
 theorem insertIdx_comm (a b : α) :
     ∀ {i j : Nat} {l : List α} (_ : i ≤ j) (_ : j ≤ length l),
       (l.insertIdx i a).insertIdx (j + 1) b = (l.insertIdx j b).insertIdx i a
@@ -110,6 +115,11 @@ theorem insertIdx_of_length_lt {l : List α} {x : α} {i : Nat} (h : l.length <
     · simp only [Nat.succ_lt_succ_iff, length] at h
       simpa using ih h
 
+@[simp, grind =]
+theorem eraseIdx_insertIdx_self {i : Nat} {l : List α} (a : α) : (l.insertIdx i a).eraseIdx i = l := by
+  rw [eraseIdx_eq_modifyTailIdx, insertIdx, modifyTailIdx_modifyTailIdx_self]
+  exact modifyTailIdx_id _ _
+
 @[simp]
 theorem insertIdx_length_self {l : List α} {x : α} : l.insertIdx l.length x = l ++ [x] := by
   induction l with
@@ -185,6 +195,7 @@ theorem getElem_insertIdx_of_gt {l : List α} {x : α} {i j : Nat} (hn : i < j)
 @[deprecated getElem_insertIdx_of_gt (since := "2025-02-04")]
 abbrev getElem_insertIdx_of_ge := @getElem_insertIdx_of_gt
 
+@[grind =]
 theorem getElem_insertIdx {l : List α} {x : α} {i j : Nat} (h : j < (l.insertIdx i x).length) :
     (l.insertIdx i x)[j] =
       if h₁ : j < i then
@@ -201,6 +212,7 @@ theorem getElem_insertIdx {l : List α} {x : α} {i j : Nat} (h : j < (l.insertI
       rw [getElem_insertIdx_self h]
     · rw [getElem_insertIdx_of_gt (by omega)]
 
+@[grind =]
 theorem getElem?_insertIdx {l : List α} {x : α} {i j : Nat} :
     (l.insertIdx i x)[j]? =
       if j < i then

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

@@ -17,7 +17,7 @@ namespace List
 
 /-! ### modifyHead -/
 
-@[simp] theorem length_modifyHead {f : α → α} {l : List α} : (l.modifyHead f).length = l.length := by
+@[simp, grind =] theorem length_modifyHead {f : α → α} {l : List α} : (l.modifyHead f).length = l.length := by
   cases l <;> simp [modifyHead]
 
 theorem modifyHead_eq_set [Inhabited α] (f : α → α) (l : List α) :
@@ -26,9 +26,10 @@ theorem modifyHead_eq_set [Inhabited α] (f : α → α) (l : List α) :
 @[simp] theorem modifyHead_eq_nil_iff {f : α → α} {l : List α} :
     l.modifyHead f = [] ↔ l = [] := by cases l <;> simp [modifyHead]
 
-@[simp] theorem modifyHead_modifyHead {l : List α} {f g : α → α} :
+@[simp, grind =] theorem modifyHead_modifyHead {l : List α} {f g : α → α} :
     (l.modifyHead f).modifyHead g = l.modifyHead (g ∘ f) := by cases l <;> simp [modifyHead]
 
+@[grind =]
 theorem getElem_modifyHead {l : List α} {f : α → α} {i} (h : i < (l.modifyHead f).length) :
     (l.modifyHead f)[i] = if h' : i = 0 then f (l[0]'(by simp at h; omega)) else l[i]'(by simpa using h) := by
   cases l with
@@ -41,6 +42,7 @@ theorem getElem_modifyHead {l : List α} {f : α → α} {i} (h : i < (l.modifyH
 @[simp] theorem getElem_modifyHead_succ {l : List α} {f : α → α} {n} (h : n + 1 < (l.modifyHead f).length) :
     (l.modifyHead f)[n + 1] = l[n + 1]'(by simpa using h) := by simp [getElem_modifyHead]
 
+@[grind =]
 theorem getElem?_modifyHead {l : List α} {f : α → α} {i} :
     (l.modifyHead f)[i]? = if i = 0 then l[i]?.map f else l[i]? := by
   cases l with
@@ -53,19 +55,19 @@ theorem getElem?_modifyHead {l : List α} {f : α → α} {i} :
 @[simp] theorem getElem?_modifyHead_succ {l : List α} {f : α → α} {n} :
     (l.modifyHead f)[n + 1]? = l[n + 1]? := by simp [getElem?_modifyHead]
 
-@[simp] theorem head_modifyHead (f : α → α) (l : List α) (h) :
+@[simp, grind =] theorem head_modifyHead (f : α → α) (l : List α) (h) :
     (l.modifyHead f).head h = f (l.head (by simpa using h)) := by
   cases l with
   | nil => simp at h
   | cons hd tl => simp
 
-@[simp] theorem head?_modifyHead {l : List α} {f : α → α} :
+@[simp, grind =] theorem head?_modifyHead {l : List α} {f : α → α} :
     (l.modifyHead f).head? = l.head?.map f := by cases l <;> simp
 
-@[simp] theorem tail_modifyHead {f : α → α} {l : List α} :
+@[simp, grind =] theorem tail_modifyHead {f : α → α} {l : List α} :
     (l.modifyHead f).tail = l.tail := by cases l <;> simp
 
-@[simp] theorem take_modifyHead {f : α → α} {l : List α} {i} :
+@[simp, grind =] theorem take_modifyHead {f : α → α} {l : List α} {i} :
     (l.modifyHead f).take i = (l.take i).modifyHead f := by
   cases l <;> cases i <;> simp
 
@@ -73,6 +75,7 @@ theorem getElem?_modifyHead {l : List α} {f : α → α} {i} :
     (l.modifyHead f).drop i = l.drop i := by
   cases l <;> cases i <;> simp_all
 
+@[grind =]
 theorem eraseIdx_modifyHead_zero {f : α → α} {l : List α} :
     (l.modifyHead f).eraseIdx 0 = l.eraseIdx 0 := by simp
 
@@ -81,7 +84,7 @@ theorem eraseIdx_modifyHead_zero {f : α → α} {l : List α} :
 
 @[simp] theorem modifyHead_id : modifyHead (id : α → α) = id := by funext l; cases l <;> simp
 
-@[simp] theorem modifyHead_dropLast {l : List α} {f : α → α} :
+@[simp, grind _=_] theorem modifyHead_dropLast {l : List α} {f : α → α} :
     l.dropLast.modifyHead f = (l.modifyHead f).dropLast := by
   rcases l with _|⟨a, l⟩
   · simp
@@ -99,7 +102,7 @@ theorem eraseIdx_eq_modifyTailIdx : ∀ i (l : List α), eraseIdx l i = l.modify
   | _+1, [] => rfl
   | _+1, _ :: _ => congrArg (cons _) (eraseIdx_eq_modifyTailIdx _ _)
 
-@[simp] theorem length_modifyTailIdx (f : List α → List α) (H : ∀ l, (f l).length = l.length) :
+@[simp, grind =] theorem length_modifyTailIdx (f : List α → List α) (H : ∀ l, (f l).length = l.length) :
     ∀ (l : List α) i, (l.modifyTailIdx i f).length = l.length
   | _, 0 => H _
   | [], _+1 => rfl
@@ -142,7 +145,7 @@ theorem modifyTailIdx_modifyTailIdx_self {f g : List α → List α} (i : Nat) (
 
 /-! ### modify -/
 
-@[simp] theorem modify_nil (f : α → α) (i) : [].modify i f = [] := by cases i <;> rfl
+@[simp, grind =] theorem modify_nil (f : α → α) (i) : [].modify i f = [] := by cases i <;> rfl
 
 @[simp] theorem modify_zero_cons (f : α → α) (a : α) (l : List α) :
     (a :: l).modify 0 f = f a :: l := rfl
@@ -150,6 +153,15 @@ theorem modifyTailIdx_modifyTailIdx_self {f g : List α → List α} (i : Nat) (
 @[simp] theorem modify_succ_cons (f : α → α) (a : α) (l : List α) (i) :
     (a :: l).modify (i + 1) f = a :: l.modify i f := rfl
 
+@[grind =]
+theorem modify_cons {f : α → α} {a : α} {l : List α} {i : Nat} :
+    (a :: l).modify i f =
+      if i = 0 then f a :: l else a :: l.modify (i - 1) f := by
+  split <;> rename_i h
+  · subst h
+    simp
+  · match i, h with | i + 1, _ => simp
+
 theorem modifyHead_eq_modify_zero (f : α → α) (l : List α) :
     l.modifyHead f = l.modify 0 f := by cases l <;> simp
 
@@ -200,6 +212,7 @@ theorem modify_eq_self {f : α → α} {i} {l : List α} (h : l.length ≤ i) :
     intro h
     omega
 
+@[grind =]
 theorem modify_modify_eq (f g : α → α) (i) (l : List α) :
     (l.modify i f).modify i g = l.modify i (g ∘ f) := by
   apply ext_getElem
@@ -245,7 +258,7 @@ theorem exists_of_modify (f : α → α) {i} {l : List α} (h : i < l.length) :
 @[simp] theorem modify_id (i) (l : List α) : l.modify i id = l := by
   simp [modify]
 
-@[grind =]
+@[grind _=_]
 theorem take_modify (f : α → α) (i j) (l : List α) :
     (l.modify i f).take j = (l.take j).modify i f := by
   induction j generalizing l i with

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

@@ -27,11 +27,12 @@ open Nat
 
 /-! ### range' -/
 
-@[simp] theorem mem_range'_1 : m ∈ range' s n ↔ s ≤ m ∧ m < s + n := by
+@[simp, grind =] theorem mem_range'_1 : m ∈ range' s n ↔ s ≤ m ∧ m < s + n := by
   simp [mem_range']; exact ⟨
     fun ⟨i, h, e⟩ => e ▸ ⟨Nat.le_add_right .., Nat.add_lt_add_left h _⟩,
     fun ⟨h₁, h₂⟩ => ⟨m - s, Nat.sub_lt_left_of_lt_add h₁ h₂, (Nat.add_sub_cancel' h₁).symm⟩⟩
 
+@[grind =]
 theorem getLast?_range' {n : Nat} : (range' s n).getLast? = if n = 0 then none else some (s + n - 1) := by
   induction n generalizing s with
   | zero => simp
@@ -43,7 +44,7 @@ theorem getLast?_range' {n : Nat} : (range' s n).getLast? = if n = 0 then none e
     · rw [if_neg h]
       simp
 
-@[simp] theorem getLast_range' {n : Nat} (h) : (range' s n).getLast h = s + n - 1 := by
+@[simp, grind =] theorem getLast_range' {n : Nat} (h) : (range' s n).getLast h = s + n - 1 := by
   cases n with
   | zero => simp at h
   | succ n => simp [getLast?_range', getLast_eq_iff_getLast?_eq_some]
@@ -158,6 +159,26 @@ theorem erase_range' :
       simp [p]
       omega
 
+@[simp, grind =]
+theorem count_range' {a s n step} (h : 0 < step := by simp) :
+    count a (range' s n step) = if ∃ i, i < n ∧ a = s + step * i then 1 else 0 := by
+  rw [(nodup_range' step h).count]
+  simp only [mem_range']
+
+@[simp, grind =]
+theorem count_range_1' {a s n} :
+    count a (range' s n) = if s ≤ a ∧ a < s + n then 1 else 0 := by
+  rw [count_range' (by simp)]
+  split <;> rename_i h
+  · obtain ⟨i, h, rfl⟩ := h
+    simp [h]
+  · simp at h
+    rw [if_neg]
+    simp only [not_and, Nat.not_lt]
+    intro w
+    specialize h (a - s)
+    omega
+
 /-! ### range -/
 
 theorem reverse_range' : ∀ {s n : Nat}, reverse (range' s n) = map (s + n - 1 - ·) (range n)
@@ -167,7 +188,7 @@ theorem reverse_range' : ∀ {s n : Nat}, reverse (range' s n) = map (s + n - 1
       show s + (n + 1) - 1 = s + n from rfl, map, map_map]
     simp [reverse_range', Nat.sub_right_comm, Nat.sub_sub]
 
-@[simp]
+@[simp, grind =]
 theorem mem_range {m n : Nat} : m ∈ range n ↔ m < n := by
   simp only [range_eq_range', mem_range'_1, Nat.zero_le, true_and, Nat.zero_add]
 
@@ -181,7 +202,7 @@ theorem pairwise_lt_range {n : Nat} : Pairwise (· < ·) (range n) := by
 theorem pairwise_le_range {n : Nat} : Pairwise (· ≤ ·) (range n) :=
   Pairwise.imp Nat.le_of_lt pairwise_lt_range
 
-@[simp] theorem take_range {i n : Nat} : take i (range n) = range (min i n) := by
+@[simp, grind =] theorem take_range {i n : Nat} : take i (range n) = range (min i n) := by
   apply List.ext_getElem
   · simp
   · simp +contextual [getElem_take, Nat.lt_min]
@@ -189,10 +210,11 @@ theorem pairwise_le_range {n : Nat} : Pairwise (· ≤ ·) (range n) :=
 theorem nodup_range {n : Nat} : Nodup (range n) := by
   simp +decide only [range_eq_range', nodup_range']
 
-@[simp] theorem find?_range_eq_some {n : Nat} {i : Nat} {p : Nat → Bool} :
+@[simp, grind] theorem find?_range_eq_some {n : Nat} {i : Nat} {p : Nat → Bool} :
     (range n).find? p = some i ↔ p i ∧ i ∈ range n ∧ ∀ j, j < i → !p j := by
   simp [range_eq_range']
 
+@[grind]
 theorem find?_range_eq_none {n : Nat} {p : Nat → Bool} :
     (range n).find? p = none ↔ ∀ i, i < n → !p i := by
   simp
@@ -200,6 +222,12 @@ theorem find?_range_eq_none {n : Nat} {p : Nat → Bool} :
 theorem erase_range : (range n).erase i = range (min n i) ++ range' (i + 1) (n - (i + 1)) := by
   simp [range_eq_range', erase_range']
 
+@[simp, grind =]
+theorem count_range {a n} :
+    count a (range n) = if a < n then 1 else 0 := by
+  rw [range_eq_range', count_range_1']
+  simp
+
 /-! ### iota -/
 
 section
@@ -348,15 +376,15 @@ end
 
 /-! ### zipIdx -/
 
-@[simp]
+@[simp, grind =]
 theorem zipIdx_singleton {x : α} {k : Nat} : zipIdx [x] k = [(x, k)] :=
   rfl
 
-@[simp] theorem head?_zipIdx {l : List α} {k : Nat} :
+@[simp, grind =] theorem head?_zipIdx {l : List α} {k : Nat} :
     (zipIdx l k).head? = l.head?.map fun a => (a, k) := by
   simp [head?_eq_getElem?]
 
-@[simp] theorem getLast?_zipIdx {l : List α} {k : Nat} :
+@[simp, grind =] theorem getLast?_zipIdx {l : List α} {k : Nat} :
     (zipIdx l k).getLast? = l.getLast?.map fun a => (a, k + l.length - 1) := by
   simp [getLast?_eq_getElem?]
   cases l <;> simp
@@ -379,6 +407,7 @@ to avoid the inequality and the subtraction. -/
 theorem mk_mem_zipIdx_iff_getElem? {i : Nat} {x : α} {l : List α} : (x, i) ∈ zipIdx l ↔ l[i]? = some x := by
   simp [mk_mem_zipIdx_iff_le_and_getElem?_sub]
 
+@[grind =]
 theorem mem_zipIdx_iff_le_and_getElem?_sub {x : α × Nat} {l : List α} {k : Nat} :
     x ∈ zipIdx l k ↔ k ≤ x.2 ∧ l[x.2 - k]? = some x.1 := by
   cases x
@@ -441,6 +470,7 @@ theorem zipIdx_map {l : List α} {k : Nat} {f : α → β} :
     rw [map_cons, zipIdx_cons', zipIdx_cons', map_cons, map_map, IH, map_map]
     rfl
 
+@[grind =]
 theorem zipIdx_append {xs ys : List α} {k : Nat} :
     zipIdx (xs ++ ys) k = zipIdx xs k ++ zipIdx ys (k + xs.length) := by
   induction xs generalizing ys k with

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

@@ -118,6 +118,7 @@ theorem suffix_iff_eq_append : l₁ <:+ l₂ ↔ take (length l₂ - length l₁
   ⟨by rintro ⟨r, rfl⟩; simp only [length_append, Nat.add_sub_cancel_right, take_left], fun e =>
     ⟨_, e⟩⟩
 
+@[grind =]
 theorem prefix_take_iff {xs ys : List α} {i : Nat} : xs <+: ys.take i ↔ xs <+: ys ∧ xs.length ≤ i := by
   constructor
   · intro h

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

@@ -99,6 +99,7 @@ theorem getLast_take {l : List α} (h : l.take i ≠ []) :
   · rw [getElem?_eq_none (by omega), getLast_eq_getElem]
     simp
 
+@[grind =]
 theorem take_take : ∀ {i j} {l : List α}, take i (take j l) = take (min i j) l
   | n, 0, l => by rw [Nat.min_zero, take_zero, take_nil]
   | 0, m, l => by rw [Nat.zero_min, take_zero, take_zero]
@@ -117,19 +118,19 @@ theorem take_set_of_le {a : α} {i j : Nat} {l : List α} (h : j ≤ i) :
 @[deprecated take_set_of_le (since := "2025-02-04")]
 abbrev take_set_of_lt := @take_set_of_le
 
-@[simp] theorem take_replicate {a : α} : ∀ {i n : Nat}, take i (replicate n a) = replicate (min i n) a
+@[simp, grind =] theorem take_replicate {a : α} : ∀ {i n : Nat}, take i (replicate n a) = replicate (min i n) a
   | n, 0 => by simp [Nat.min_zero]
   | 0, m => by simp [Nat.zero_min]
   | succ n, succ m => by simp [replicate_succ, succ_min_succ, take_replicate]
 
-@[simp] theorem drop_replicate {a : α} : ∀ {i n : Nat}, drop i (replicate n a) = replicate (n - i) a
+@[simp, grind =] theorem drop_replicate {a : α} : ∀ {i n : Nat}, drop i (replicate n a) = replicate (n - i) a
   | n, 0 => by simp
   | 0, m => by simp
   | succ n, succ m => by simp [replicate_succ, succ_sub_succ, drop_replicate]
 
 /-- Taking the first `i` elements in `l₁ ++ l₂` is the same as appending the first `i` elements
 of `l₁` to the first `n - l₁.length` elements of `l₂`. -/
-theorem take_append_eq_append_take {l₁ l₂ : List α} {i : Nat} :
+theorem take_append {l₁ l₂ : List α} {i : Nat} :
     take i (l₁ ++ l₂) = take i l₁ ++ take (i - l₁.length) l₂ := by
   induction l₁ generalizing i
   · simp
@@ -140,15 +141,18 @@ theorem take_append_eq_append_take {l₁ l₂ : List α} {i : Nat} :
       congr 1
       omega
 
+@[deprecated take_append (since := "2025-06-16")]
+abbrev take_append_eq_append_take := @take_append
+
 theorem take_append_of_le_length {l₁ l₂ : List α} {i : Nat} (h : i ≤ l₁.length) :
     (l₁ ++ l₂).take i = l₁.take i := by
-  simp [take_append_eq_append_take, Nat.sub_eq_zero_of_le h]
+  simp [take_append, Nat.sub_eq_zero_of_le h]
 
 /-- Taking the first `l₁.length + i` elements in `l₁ ++ l₂` is the same as appending the first
 `i` elements of `l₂` to `l₁`. -/
-theorem take_append {l₁ l₂ : List α} (i : Nat) :
+theorem take_length_add_append {l₁ l₂ : List α} (i : Nat) :
     take (l₁.length + i) (l₁ ++ l₂) = l₁ ++ take i l₂ := by
-  rw [take_append_eq_append_take, take_of_length_le (Nat.le_add_right _ _), Nat.add_sub_cancel_left]
+  rw [take_append, take_of_length_le (Nat.le_add_right _ _), Nat.add_sub_cancel_left]
 
 @[simp]
 theorem take_eq_take_iff :
@@ -162,11 +166,12 @@ theorem take_eq_take_iff :
 @[deprecated take_eq_take_iff (since := "2025-02-16")]
 abbrev take_eq_take := @take_eq_take_iff
 
+@[grind =]
 theorem take_add {l : List α} {i j : Nat} : l.take (i + j) = l.take i ++ (l.drop i).take j := by
   suffices take (i + j) (take i l ++ drop i l) = take i l ++ take j (drop i l) by
     rw [take_append_drop] at this
     assumption
-  rw [take_append_eq_append_take, take_of_length_le, append_right_inj]
+  rw [take_append, take_of_length_le, append_right_inj]
   · simp only [take_eq_take_iff, length_take, length_drop]
     omega
   apply Nat.le_trans (m := i)
@@ -236,7 +241,7 @@ dropping the first `i` elements. Version designed to rewrite from the small list
       exact Nat.add_lt_of_lt_sub (length_drop ▸ h)) := by
   rw [getElem_drop']
 
-@[simp]
+@[simp, grind =]
 theorem getElem?_drop {xs : List α} {i j : Nat} : (xs.drop i)[j]? = xs[i + j]? := by
   ext
   simp only [getElem?_eq_some_iff, getElem_drop]
@@ -285,7 +290,7 @@ theorem getLast?_drop {l : List α} : (l.drop i).getLast? = if l.length ≤ i th
     congr
     omega
 
-@[simp] theorem getLast_drop {l : List α} (h : l.drop i ≠ []) :
+@[simp, grind =] theorem getLast_drop {l : List α} (h : l.drop i ≠ []) :
     (l.drop i).getLast h = l.getLast (ne_nil_of_length_pos (by simp at h; omega)) := by
   simp only [ne_eq, drop_eq_nil_iff] at h
   apply Option.some_inj.1
@@ -306,7 +311,8 @@ theorem drop_length_cons {l : List α} (h : l ≠ []) (a : α) :
 
 /-- Dropping the elements up to `i` in `l₁ ++ l₂` is the same as dropping the elements up to `i`
 in `l₁`, dropping the elements up to `i - l₁.length` in `l₂`, and appending them. -/
-theorem drop_append_eq_append_drop {l₁ l₂ : List α} {i : Nat} :
+@[grind =]
+theorem drop_append {l₁ l₂ : List α} {i : Nat} :
     drop i (l₁ ++ l₂) = drop i l₁ ++ drop (i - l₁.length) l₂ := by
   induction l₁ generalizing i
   · simp
@@ -316,15 +322,18 @@ theorem drop_append_eq_append_drop {l₁ l₂ : List α} {i : Nat} :
       congr 1
       omega
 
+@[deprecated drop_append (since := "2025-06-16")]
+abbrev drop_append_eq_append_drop := @drop_append
+
 theorem drop_append_of_le_length {l₁ l₂ : List α} {i : Nat} (h : i ≤ l₁.length) :
     (l₁ ++ l₂).drop i = l₁.drop i ++ l₂ := by
-  simp [drop_append_eq_append_drop, Nat.sub_eq_zero_of_le h]
+  simp [drop_append, Nat.sub_eq_zero_of_le h]
 
 /-- Dropping the elements up to `l₁.length + i` in `l₁ + l₂` is the same as dropping the elements
 up to `i` in `l₂`. -/
 @[simp]
-theorem drop_append {l₁ l₂ : List α} (i : Nat) : drop (l₁.length + i) (l₁ ++ l₂) = drop i l₂ := by
-  rw [drop_append_eq_append_drop, drop_eq_nil_of_le] <;>
+theorem drop_length_add_append {l₁ l₂ : List α} (i : Nat) : drop (l₁.length + i) (l₁ ++ l₂) = drop i l₂ := by
+  rw [drop_append, drop_eq_nil_of_le] <;>
     simp [Nat.add_sub_cancel_left, Nat.le_add_right]
 
 theorem set_eq_take_append_cons_drop {l : List α} {i : Nat} {a : α} :
@@ -458,7 +467,7 @@ theorem false_of_mem_take_findIdx {xs : List α} {p : α → Bool} (h : x ∈ xs
   obtain ⟨i, h, rfl⟩ := h
   exact not_of_lt_findIdx (by omega)
 
-@[simp] theorem findIdx_take {xs : List α} {i : Nat} {p : α → Bool} :
+@[simp, grind =] theorem findIdx_take {xs : List α} {i : Nat} {p : α → Bool} :
     (xs.take i).findIdx p = min i (xs.findIdx p) := by
   induction xs generalizing i with
   | nil => simp
@@ -470,7 +479,7 @@ theorem false_of_mem_take_findIdx {xs : List α} {p : α → Bool} (h : x ∈ xs
       · simp
       · rw [Nat.add_min_add_right]
 
-@[simp] theorem min_findIdx_findIdx {xs : List α} {p q : α → Bool} :
+@[simp, grind =] theorem min_findIdx_findIdx {xs : List α} {p q : α → Bool} :
     min (xs.findIdx p) (xs.findIdx q) = xs.findIdx (fun a => p a || q a) := by
   induction xs with
   | nil => simp
@@ -512,7 +521,7 @@ theorem dropWhile_eq_drop_findIdx_not {xs : List α} {p : α → Bool} :
 
 /-! ### rotateLeft -/
 
-@[simp] theorem rotateLeft_replicate {n} {a : α} : rotateLeft (replicate m a) n = replicate m a := by
+@[simp, grind =] theorem rotateLeft_replicate {n} {a : α} : rotateLeft (replicate m a) n = replicate m a := by
   cases n with
   | zero => simp
   | succ n =>
@@ -525,7 +534,7 @@ theorem dropWhile_eq_drop_findIdx_not {xs : List α} {p : α → Bool} :
 
 /-! ### rotateRight -/
 
-@[simp] theorem rotateRight_replicate {n} {a : α} : rotateRight (replicate m a) n = replicate m a := by
+@[simp, grind =] theorem rotateRight_replicate {n} {a : α} : rotateRight (replicate m a) n = replicate m a := by
   cases n with
   | zero => simp
   | succ n =>

src/Init/Data/List/Pairwise.lean

@@ -279,7 +279,11 @@ theorem nodup_nil : @Nodup α [] :=
 theorem nodup_cons {a : α} {l : List α} : Nodup (a :: l) ↔ a ∉ l ∧ Nodup l := by
   simp only [Nodup, pairwise_cons, forall_mem_ne]
 
-@[grind →] theorem Nodup.sublist : l₁ <+ l₂ → Nodup l₂ → Nodup l₁ :=
+@[grind =] theorem nodup_append {l₁ l₂ : List α} :
+    (l₁ ++ l₂).Nodup ↔ l₁.Nodup ∧ l₂.Nodup ∧ ∀ a ∈ l₁, ∀ b ∈ l₂, a ≠ b :=
+  pairwise_append
+
+theorem Nodup.sublist : l₁ <+ l₂ → Nodup l₂ → Nodup l₁ :=
   Pairwise.sublist
 
 grind_pattern Nodup.sublist => l₁ <+ l₂, Nodup l₁
@@ -312,4 +316,48 @@ theorem getElem?_inj {xs : List α}
 @[simp, grind =] theorem nodup_replicate {n : Nat} {a : α} :
     (replicate n a).Nodup ↔ n ≤ 1 := by simp [Nodup]
 
+theorem Nodup.count [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : Nodup l) : count a l = if a ∈ l then 1 else 0 := by
+  split <;> rename_i h'
+  · obtain ⟨s, t, rfl⟩ := List.append_of_mem h'
+    rw [nodup_append] at h
+    simp_all
+    rw [count_eq_zero.mpr ?_, count_eq_zero.mpr ?_]
+    · exact h.2.1.1
+    · intro w
+      simpa using h.2.2 _ w
+  · rw [count_eq_zero_of_not_mem h']
+
+grind_pattern Nodup.count => count a l, Nodup l
+
+@[grind =]
+theorem nodup_iff_count [BEq α] [LawfulBEq α] {l : List α} : l.Nodup ↔ ∀ a, count a l ≤ 1 := by
+  induction l with
+  | nil => simp
+  | cons x l ih =>
+    constructor
+    · intro h a
+      simp at h
+      rw [count_cons]
+      split <;> rename_i h'
+      · simp at h'
+        rw [count_eq_zero.mpr ?_]
+        · exact Nat.le_refl _
+        · exact h' ▸ h.1
+      · simp at h'
+        refine ih.mp h.2 a
+    · intro h
+      simp only [count_cons] at h
+      simp only [nodup_cons]
+      constructor
+      · intro w
+        specialize h x
+        simp at h
+        have := count_pos_iff.mpr w
+        replace h := le_of_lt_succ h
+        apply Nat.lt_irrefl _ (Nat.lt_of_lt_of_le this h)
+      · rw [ih]
+        intro a
+        specialize h a
+        exact le_of_add_right_le h
+
 end List

src/Init/Data/List/Perm.lean

@@ -23,8 +23,7 @@ The notation `~` is used for permutation equivalence.
 -/
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- TODO: restore after an update-stage0
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 open Nat
 
@@ -90,6 +89,9 @@ theorem Perm.mem_iff {a : α} {l₁ l₂ : List α} (p : l₁ ~ l₂) : a ∈ l
   | swap => simp only [mem_cons, or_left_comm]
   | trans _ _ ih₁ ih₂ => simp only [ih₁, ih₂]
 
+grind_pattern Perm.mem_iff => l₁ ~ l₂, a ∈ l₁
+grind_pattern Perm.mem_iff => l₁ ~ l₂, a ∈ l₂
+
 theorem Perm.subset {l₁ l₂ : List α} (p : l₁ ~ l₂) : l₁ ⊆ l₂ := fun _ => p.mem_iff.mp
 
 theorem Perm.append_right {l₁ l₂ : List α} (t₁ : List α) (p : l₁ ~ l₂) : l₁ ++ t₁ ~ l₂ ++ t₁ := by
@@ -106,9 +108,15 @@ theorem Perm.append_left {t₁ t₂ : List α} : ∀ l : List α, t₁ ~ t₂
 theorem Perm.append {l₁ l₂ t₁ t₂ : List α} (p₁ : l₁ ~ l₂) (p₂ : t₁ ~ t₂) : l₁ ++ t₁ ~ l₂ ++ t₂ :=
   (p₁.append_right t₁).trans (p₂.append_left l₂)
 
+grind_pattern Perm.append => l₁ ~ l₂, t₁ ~ t₂, l₁ ++ t₁
+grind_pattern Perm.append => l₁ ~ l₂, t₁ ~ t₂, l₂ ++ t₂
+
 theorem Perm.append_cons (a : α) {l₁ l₂ r₁ r₂ : List α} (p₁ : l₁ ~ l₂) (p₂ : r₁ ~ r₂) :
     l₁ ++ a :: r₁ ~ l₂ ++ a :: r₂ := p₁.append (p₂.cons a)
 
+grind_pattern Perm.append_cons => l₁ ~ l₂, r₁ ~ r₂, l₁ ++ a :: r₁
+grind_pattern Perm.append_cons => l₁ ~ l₂, r₁ ~ r₂, l₂ ++ a :: r₂
+
 @[simp] theorem perm_middle {a : α} : ∀ {l₁ l₂ : List α}, l₁ ++ a :: l₂ ~ a :: (l₁ ++ l₂)
   | [], _ => .refl _
   | b :: _, _ => (Perm.cons _ perm_middle).trans (swap a b _)
@@ -194,9 +202,15 @@ theorem Perm.filterMap (f : α → Option β) {l₁ l₂ : List α} (p : l₁ ~
   | swap x y l₂ => cases hx : f x <;> cases hy : f y <;> simp [hx, hy, filterMap_cons, swap]
   | trans _p₁ _p₂ IH₁ IH₂ => exact IH₁.trans IH₂
 
+grind_pattern Perm.filterMap => l₁ ~ l₂, filterMap f l₁
+grind_pattern Perm.filterMap => l₁ ~ l₂, filterMap f l₂
+
 theorem Perm.map (f : α → β) {l₁ l₂ : List α} (p : l₁ ~ l₂) : map f l₁ ~ map f l₂ :=
   filterMap_eq_map ▸ p.filterMap _
 
+grind_pattern Perm.map => l₁ ~ l₂, map f l₁
+grind_pattern Perm.map => l₁ ~ l₂, map f l₂
+
 theorem Perm.pmap {p : α → Prop} (f : ∀ a, p a → β) {l₁ l₂ : List α} (p : l₁ ~ l₂) {H₁ H₂} :
     pmap f l₁ H₁ ~ pmap f l₂ H₂ := by
   induction p with
@@ -205,12 +219,18 @@ theorem Perm.pmap {p : α → Prop} (f : ∀ a, p a → β) {l₁ l₂ : List α
   | swap x y => simp [swap]
   | trans _p₁ p₂ IH₁ IH₂ => exact IH₁.trans (IH₂ (H₁ := fun a m => H₂ a (p₂.subset m)))
 
+grind_pattern Perm.pmap => l₁ ~ l₂, pmap f l₁ H₁
+grind_pattern Perm.pmap => l₁ ~ l₂, pmap f l₂ H₂
+
 theorem Perm.unattach {α : Type u} {p : α → Prop} {l₁ l₂ : List { x // p x }} (h : l₁ ~ l₂) :
     l₁.unattach.Perm l₂.unattach := h.map _
 
 theorem Perm.filter (p : α → Bool) {l₁ l₂ : List α} (s : l₁ ~ l₂) :
     filter p l₁ ~ filter p l₂ := by rw [← filterMap_eq_filter]; apply s.filterMap
 
+grind_pattern Perm.filter => l₁ ~ l₂, filter p l₁
+grind_pattern Perm.filter => l₁ ~ l₂, filter p l₂
+
 theorem filter_append_perm (p : α → Bool) (l : List α) :
     filter p l ++ filter (fun x => !p x) l ~ l := by
   induction l with
@@ -388,12 +408,16 @@ theorem Perm.erase (a : α) {l₁ l₂ : List α} (p : l₁ ~ l₂) : l₁.erase
     have h₂ : a ∉ l₂ := mt p.mem_iff.2 h₁
     rw [erase_of_not_mem h₁, erase_of_not_mem h₂]; exact p
 
+grind_pattern Perm.erase => l₁ ~ l₂, l₁.erase a
+grind_pattern Perm.erase => l₁ ~ l₂, l₂.erase a
+
 theorem cons_perm_iff_perm_erase {a : α} {l₁ l₂ : List α} :
     a :: l₁ ~ l₂ ↔ a ∈ l₂ ∧ l₁ ~ l₂.erase a := by
   refine ⟨fun h => ?_, fun ⟨m, h⟩ => (h.cons a).trans (perm_cons_erase m).symm⟩
   have : a ∈ l₂ := h.subset mem_cons_self
   exact ⟨this, (h.trans <| perm_cons_erase this).cons_inv⟩
 
+@[grind =]
 theorem perm_iff_count {l₁ l₂ : List α} : l₁ ~ l₂ ↔ ∀ a, count a l₁ = count a l₂ := by
   refine ⟨Perm.count_eq, fun H => ?_⟩
   induction l₁ generalizing l₂ with
@@ -410,6 +434,12 @@ theorem perm_iff_count {l₁ l₂ : List α} : l₁ ~ l₂ ↔ ∀ a, count a l
     rw [(perm_cons_erase this).count_eq] at H
     by_cases h : b = a <;> simpa [h, count_cons, Nat.succ_inj] using H
 
+theorem Perm.count (h : l₁ ~ l₂) (a : α) : count a l₁ = count a l₂ := by
+  rw [perm_iff_count.mp h]
+
+grind_pattern Perm.count => l₁ ~ l₂, count a l₁
+grind_pattern Perm.count => l₁ ~ l₂, count a l₂
+
 theorem isPerm_iff : ∀ {l₁ l₂ : List α}, l₁.isPerm l₂ ↔ l₁ ~ l₂
   | [], [] => by simp [isPerm, isEmpty]
   | [], _ :: _ => by simp [isPerm, isEmpty, Perm.nil_eq]
@@ -425,6 +455,9 @@ protected theorem Perm.insert (a : α) {l₁ l₂ : List α} (p : l₁ ~ l₂) :
     have := p.cons a
     simpa [h, mt p.mem_iff.2 h] using this
 
+grind_pattern Perm.insert => l₁ ~ l₂, l₁.insert a
+grind_pattern Perm.insert => l₁ ~ l₂, l₂.insert a
+
 theorem perm_insert_swap (x y : α) (l : List α) :
     List.insert x (List.insert y l) ~ List.insert y (List.insert x l) := by
   by_cases xl : x ∈ l <;> by_cases yl : y ∈ l <;> simp [xl, yl]
@@ -491,6 +524,9 @@ theorem Perm.nodup {l l' : List α} (hl : l ~ l') (hR : l.Nodup) : l'.Nodup := h
 theorem Perm.nodup_iff {l₁ l₂ : List α} : l₁ ~ l₂ → (Nodup l₁ ↔ Nodup l₂) :=
   Perm.pairwise_iff <| @Ne.symm α
 
+grind_pattern Perm.nodup_iff => l₁ ~ l₂, Nodup l₁
+grind_pattern Perm.nodup_iff => l₁ ~ l₂, Nodup l₂
+
 theorem Perm.flatten {l₁ l₂ : List (List α)} (h : l₁ ~ l₂) : l₁.flatten ~ l₂.flatten := by
   induction h with
   | nil => rfl
@@ -541,20 +577,30 @@ theorem perm_insertIdx {α} (x : α) (l : List α) {i} (h : i ≤ l.length) :
 
 namespace Perm
 
-theorem take {l₁ l₂ : List α} (h : l₁ ~ l₂) {n : Nat} (w : l₁.drop n ~ l₂.drop n) :
-    l₁.take n ~ l₂.take n := by
+theorem take {l₁ l₂ : List α} (h : l₁ ~ l₂) {i : Nat} (w : l₁.drop i ~ l₂.drop i) :
+    l₁.take i ~ l₂.take i := by
   classical
   rw [perm_iff_count] at h w ⊢
-  rw [← take_append_drop n l₁, ← take_append_drop n l₂] at h
+  rw [← take_append_drop i l₁, ← take_append_drop i l₂] at h
   simpa only [count_append, w, Nat.add_right_cancel_iff] using h
 
-theorem drop {l₁ l₂ : List α} (h : l₁ ~ l₂) {n : Nat} (w : l₁.take n ~ l₂.take n) :
-    l₁.drop n ~ l₂.drop n := by
+theorem drop {l₁ l₂ : List α} (h : l₁ ~ l₂) {i : Nat} (w : l₁.take i ~ l₂.take i) :
+    l₁.drop i ~ l₂.drop i := by
   classical
   rw [perm_iff_count] at h w ⊢
-  rw [← take_append_drop n l₁, ← take_append_drop n l₂] at h
+  rw [← take_append_drop i l₁, ← take_append_drop i l₂] at h
   simpa only [count_append, w, Nat.add_left_cancel_iff] using h
 
+theorem sum_nat {l₁ l₂ : List Nat} (h : l₁ ~ l₂) : l₁.sum = l₂.sum := by
+  induction h with
+  | nil => simp
+  | cons _ _ ih => simp [ih]
+  | swap => simpa [List.sum_cons] using Nat.add_left_comm ..
+  | trans _ _ ih₁ ih₂ => simp [ih₁, ih₂]
+
+grind_pattern Perm.sum_nat => l₁ ~ l₂, l₁.sum
+grind_pattern Perm.sum_nat => l₁ ~ l₂, l₂.sum
+
 end Perm
 
 end List

src/Init/Data/List/TakeDrop.lean

@@ -467,7 +467,7 @@ theorem replace_takeWhile [BEq α] [LawfulBEq α] {l : List α} {p : α → Bool
 
 /-! ### splitAt -/
 
-@[simp] theorem splitAt_eq {i : Nat} {l : List α} : splitAt i l = (l.take i, l.drop i) := by
+@[simp, grind =] theorem splitAt_eq {i : Nat} {l : List α} : splitAt i l = (l.take i, l.drop i) := by
   rw [splitAt, splitAt_go, reverse_nil, nil_append]
   split <;> simp_all [take_of_length_le, drop_of_length_le]
 

src/Init/Data/Nat/Basic.lean

@@ -406,6 +406,12 @@ theorem le_of_add_right_le {n m k : Nat} (h : n + k ≤ m) : n ≤ m :=
 theorem le_add_right_of_le {n m k : Nat} (h : n ≤ m) : n ≤ m + k :=
   Nat.le_trans h (le_add_right m k)
 
+theorem le_of_add_left_le {n m k : Nat} (h : k + n ≤ m) : n ≤ m :=
+  Nat.le_trans (le_add_left n k) h
+
+theorem le_add_left_of_le {n m k : Nat} (h : n ≤ m) : n ≤ k + m :=
+  Nat.le_trans h (le_add_left m k)
+
 theorem lt_of_add_one_le {n m : Nat} (h : n + 1 ≤ m) : n < m := h
 
 theorem add_one_le_of_lt {n m : Nat} (h : n < m) : n + 1 ≤ m := h

src/Init/Data/Vector/Count.lean

@@ -40,6 +40,7 @@ theorem countP_push {a : α} {xs : Vector α n} : countP p (xs.push a) = countP
   rcases xs with ⟨xs, rfl⟩
   simp [Array.countP_push]
 
+@[grind =]
 theorem countP_singleton {a : α} : countP p #v[a] = if p a then 1 else 0 := by
   simp
 
@@ -51,7 +52,7 @@ theorem countP_le_size {xs : Vector α n} : countP p xs ≤ n := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.countP_le_size (p := p)]
 
-@[simp] theorem countP_append {xs : Vector α n} {ys : Vector α m} : countP p (xs ++ ys) = countP p xs + countP p ys := by
+@[simp, grind =] theorem countP_append {xs : Vector α n} {ys : Vector α m} : countP p (xs ++ ys) = countP p xs + countP p ys := by
   cases xs
   cases ys
   simp
@@ -116,7 +117,7 @@ theorem countP_flatMap {p : β → Bool} {xs : Vector α n} {f : α → Vector
   rcases xs with ⟨xs, rfl⟩
   simp [Array.countP_flatMap, Function.comp_def]
 
-@[simp] theorem countP_reverse {xs : Vector α n} : countP p xs.reverse = countP p xs := by
+@[simp, grind =] theorem countP_reverse {xs : Vector α n} : countP p xs.reverse = countP p xs := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
@@ -136,7 +137,7 @@ section count
 
 variable [BEq α]
 
-@[simp] theorem count_empty {a : α} : count a #v[] = 0 := rfl
+@[simp, grind =] theorem count_empty {a : α} : count a #v[] = 0 := rfl
 
 theorem count_push {a b : α} {xs : Vector α n} :
     count a (xs.push b) = count a xs + if b == a then 1 else 0 := by
@@ -151,23 +152,25 @@ theorem count_eq_countP' {a : α} : count (n := n) a = countP (· == a) := by
 
 theorem count_le_size {a : α} {xs : Vector α n} : count a xs ≤ n := countP_le_size
 
+grind_pattern count_le_size => count a xs
+
 theorem count_le_count_push {a b : α} {xs : Vector α n} : count a xs ≤ count a (xs.push b) := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.count_push]
 
-@[simp] theorem count_singleton {a b : α} : count a #v[b] = if b == a then 1 else 0 := by
+@[simp, grind =] theorem count_singleton {a b : α} : count a #v[b] = if b == a then 1 else 0 := by
   simp [count_eq_countP]
 
-@[simp] theorem count_append {a : α} {xs : Vector α n} {ys : Vector α m} :
+@[simp, grind =] theorem count_append {a : α} {xs : Vector α n} {ys : Vector α m} :
     count a (xs ++ ys) = count a xs + count a ys :=
   countP_append ..
 
-@[simp] theorem count_flatten {a : α} {xss : Vector (Vector α m) n} :
+@[simp, grind =] theorem count_flatten {a : α} {xss : Vector (Vector α m) n} :
     count a xss.flatten = (xss.map (count a)).sum := by
   rcases xss with ⟨xss, rfl⟩
   simp [Array.count_flatten, Function.comp_def]
 
-@[simp] theorem count_reverse {a : α} {xs : Vector α n} : count a xs.reverse = count a xs := by
+@[simp, grind =] theorem count_reverse {a : α} {xs : Vector α n} : count a xs.reverse = count a xs := by
   rcases xs with ⟨xs, rfl⟩
   simp
 

src/Init/Data/Vector/Extract.lean

@@ -28,19 +28,19 @@ set_option linter.indexVariables false
   rcases xs with ⟨as, rfl⟩
   simp [h]
 
-@[simp]
+@[simp, grind =]
 theorem extract_push {xs : Vector α n} {b : α} {start stop : Nat} (h : stop ≤ n) :
     (xs.push b).extract start stop = (xs.extract start stop).cast (by omega) := by
   rcases xs with ⟨xs, rfl⟩
   simp [h]
 
-@[simp]
+@[simp, grind =]
 theorem extract_eq_pop {xs : Vector α n} {stop : Nat} (h : stop = n - 1) :
     xs.extract 0 stop = xs.pop.cast (by omega) := by
   rcases xs with ⟨xs, rfl⟩
   simp [h]
 
-@[simp]
+@[simp, grind _=_]
 theorem extract_append_extract {xs : Vector α n} {i j k : Nat} :
     xs.extract i j ++ xs.extract j k =
       (xs.extract (min i j) (max j k)).cast (by omega) := by
@@ -79,11 +79,12 @@ theorem getElem?_extract_of_succ {xs : Vector α n} {j : Nat} :
   · rw [if_neg (by omega)]
     simp_all
 
-@[simp] theorem extract_extract {xs : Vector α n} {i j k l : Nat} :
+@[simp, grind =] theorem extract_extract {xs : Vector α n} {i j k l : Nat} :
     (xs.extract i j).extract k l = (xs.extract (i + k) (min (i + l) j)).cast (by omega) := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
+@[grind =]
 theorem extract_set {xs : Vector α n} {i j k : Nat} (h : k < n) {a : α} :
     (xs.set k a).extract i j =
       if _ : k < i then
@@ -97,12 +98,13 @@ theorem extract_set {xs : Vector α n} {i j k : Nat} (h : k < n) {a : α} :
   · simp
   · split <;> simp
 
+@[grind =]
 theorem set_extract {xs : Vector α n} {i j k : Nat} (h : k < min j n - i) {a : α} :
     (xs.extract i j).set k a = (xs.set (i + k) a).extract i j := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.set_extract]
 
-@[simp]
+@[simp, grind =]
 theorem extract_append {xs : Vector α n} {ys : Vector α m} {i j : Nat} :
     (xs ++ ys).extract i j =
       (xs.extract i j ++ ys.extract (i - n) (j - n)).cast (by omega) := by
@@ -128,12 +130,12 @@ theorem extract_append_left {xs : Vector α n} {ys : Vector α m} :
   congr 1
   omega
 
-@[simp] theorem map_extract {xs : Vector α n} {i j : Nat} :
+@[simp, grind =] theorem map_extract {xs : Vector α n} {i j : Nat} :
     (xs.extract i j).map f = (xs.map f).extract i j := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp] theorem extract_replicate {a : α} {n i j : Nat} :
+@[simp, grind =] theorem extract_replicate {a : α} {n i j : Nat} :
     (replicate n a).extract i j = replicate (min j n - i) a := by
   ext i h
   simp
@@ -161,6 +163,7 @@ theorem set_eq_push_extract_append_extract {xs : Vector α n} {i : Nat} (h : i <
   rcases xs with ⟨as, rfl⟩
   simp [Array.set_eq_push_extract_append_extract, h]
 
+@[grind =]
 theorem extract_reverse {xs : Vector α n} {i j : Nat} :
     xs.reverse.extract i j = (xs.extract (n - j) (n - i)).reverse.cast (by omega) := by
   ext i h
@@ -168,6 +171,7 @@ theorem extract_reverse {xs : Vector α n} {i j : Nat} :
   congr 1
   omega
 
+@[grind =]
 theorem reverse_extract {xs : Vector α n} {i j : Nat} :
     (xs.extract i j).reverse = (xs.reverse.extract (n - j) (n - i)).cast (by omega) := by
   rcases xs with ⟨xs, rfl⟩

src/Init/Data/Vector/InsertIdx.lean

@@ -30,15 +30,20 @@ section InsertIdx
 
 variable {a : α}
 
-@[simp]
+@[simp, grind =]
 theorem insertIdx_zero {xs : Vector α n} {x : α} : xs.insertIdx 0 x = (#v[x] ++ xs).cast (by omega) := by
   cases xs
   simp
 
-theorem eraseIdx_insertIdx {i : Nat} {xs : Vector α n} {h : i ≤ n} :
+theorem eraseIdx_insertIdx_self {i : Nat} {xs : Vector α n} {h : i ≤ n} :
     (xs.insertIdx i a).eraseIdx i = xs := by
   rcases xs with ⟨xs, rfl⟩
-  simp_all [Array.eraseIdx_insertIdx]
+  simp_all [Array.eraseIdx_insertIdx_self]
+
+@[deprecated eraseIdx_insertIdx_self (since := "2025-06-15")]
+theorem eraseIdx_insertIdx {i : Nat} {xs : Vector α n} {h : i ≤ n} :
+    (xs.insertIdx i a).eraseIdx i = xs := by
+  simp [eraseIdx_insertIdx_self]
 
 theorem insertIdx_eraseIdx_of_ge {xs : Vector α n}
     (w₁ : i < n) (w₂ : j ≤ n - 1) (h : i ≤ j) :
@@ -54,6 +59,18 @@ theorem insertIdx_eraseIdx_of_le {xs : Vector α n}
   rcases xs with ⟨as, rfl⟩
   simpa using Array.insertIdx_eraseIdx_of_le (by simpa) (by simpa) (by simpa)
 
+@[grind =]
+theorem insertIdx_eraseIdx {as : Vector α n} (h₁ : i < n) (h₂ : j ≤ n - 1) :
+    (as.eraseIdx i).insertIdx j a =
+      if h : i ≤ j then
+        ((as.insertIdx (j + 1) a).eraseIdx i).cast (by omega)
+      else
+        ((as.insertIdx j a).eraseIdx (i + 1) (by simp_all)).cast (by omega) := by
+  split <;> rename_i h'
+  · rw [insertIdx_eraseIdx_of_ge] <;> omega
+  · rw [insertIdx_eraseIdx_of_le] <;> omega
+
+@[grind =]
 theorem insertIdx_comm (a b : α) {i j : Nat} {xs : Vector α n} (_ : i ≤ j) (_ : j ≤ n) :
     (xs.insertIdx i a).insertIdx (j + 1) b =
       (xs.insertIdx j b).insertIdx i a := by
@@ -70,6 +87,7 @@ theorem insertIdx_size_self {xs : Vector α n} {x : α} : xs.insertIdx n x = xs.
   rcases xs with ⟨as, rfl⟩
   simp
 
+@[grind =]
 theorem getElem_insertIdx {xs : Vector α n} {x : α} {i k : Nat} (w : i ≤ n) (h : k < n + 1) :
     (xs.insertIdx i x)[k] =
       if h₁ : k < i then
@@ -98,6 +116,7 @@ theorem getElem_insertIdx_of_gt {xs : Vector α n} {x : α} {i k : Nat} (w : k
   simp [Array.getElem_insertIdx, w, h]
   rw [dif_neg (by omega), dif_neg (by omega)]
 
+@[grind =]
 theorem getElem?_insertIdx {xs : Vector α n} {x : α} {i k : Nat} (h : i ≤ n) :
     (xs.insertIdx i x)[k]? =
       if k < i then

src/Init/Data/Vector/Range.lean

@@ -112,14 +112,25 @@ theorem range'_eq_append_iff : range' s (n + m) = xs ++ ys ↔ xs = range' s n
   · rintro ⟨h₁, h₂⟩
     exact ⟨n, by omega, by simp_all⟩
 
-@[simp] theorem find?_range'_eq_some {s n : Nat} {i : Nat} {p : Nat → Bool} :
+@[simp, grind =] theorem find?_range'_eq_some {s n : Nat} {i : Nat} {p : Nat → Bool} :
     (range' s n).find? p = some i ↔ p i ∧ i ∈ range' s n ∧ ∀ j, s ≤ j → j < i → !p j := by
   simp [range'_eq_mk_range']
 
-@[simp] theorem find?_range'_eq_none {s n : Nat} {p : Nat → Bool} :
+@[simp, grind =] theorem find?_range'_eq_none {s n : Nat} {p : Nat → Bool} :
     (range' s n).find? p = none ↔ ∀ i, s ≤ i → i < s + n → !p i := by
   simp [range'_eq_mk_range']
 
+@[simp, grind =]
+theorem count_range' {a s n step} (h : 0 < step := by simp) :
+    count a (range' s n step) = if ∃ i, i < n ∧ a = s + step * i then 1 else 0 := by
+  rw [range'_eq_mk_range', count_mk, ← Array.count_range' h]
+
+@[simp, grind =]
+theorem count_range_1' {a s n} :
+    count a (range' s n) = if s ≤ a ∧ a < s + n then 1 else 0 := by
+  rw [range'_eq_mk_range', count_mk, ← Array.count_range_1']
+
+
 /-! ### range -/
 
 @[simp, grind =] theorem getElem_range {i : Nat} (hi : i < n) : (Vector.range n)[i] = i := by
@@ -171,9 +182,15 @@ theorem self_mem_range_succ {n : Nat} : n ∈ range (n + 1) := by simp
     (range n).find? p = none ↔ ∀ i, i < n → !p i := by
   simp [range_eq_range']
 
+@[simp, grind =]
+theorem count_range {a n} :
+    count a (range n) = if a < n then 1 else 0 := by
+  rw [range_eq_range', count_range_1']
+  simp
+
 /-! ### zipIdx -/
 
-@[simp]
+@[simp, grind =]
 theorem getElem?_zipIdx {xs : Vector α n} {i j} : (zipIdx xs i)[j]? = xs[j]?.map fun a => (a, i + j) := by
   simp [getElem?_def]
 
@@ -216,7 +233,7 @@ theorem zipIdx_eq_map_add {xs : Vector α n} {i : Nat} :
   simp only [zipIdx_mk, map_mk, eq_mk]
   rw [Array.zipIdx_eq_map_add]
 
-@[simp]
+@[simp, grind =]
 theorem zipIdx_singleton {x : α} {k : Nat} : zipIdx (#v[x]) k = #v[(x, k)] :=
   rfl
 
@@ -265,6 +282,7 @@ theorem zipIdx_map {f : α → β} {xs : Vector α n} {k : Nat} :
   rcases xs with ⟨xs, rfl⟩
   simp [Array.zipIdx_map]
 
+@[grind =]
 theorem zipIdx_append {xs : Vector α n} {ys : Vector α m} {k : Nat} :
     zipIdx (xs ++ ys) k = zipIdx xs k ++ zipIdx ys (k + n) := by
   rcases xs with ⟨xs, rfl⟩

src/Init/Grind/Module/Basic.lean

@@ -37,6 +37,15 @@ class IntModule (M : Type u) extends Zero M, Add M, Neg M, Sub M, HMul Int M M w
   neg_add_cancel : ∀ a : M, -a + a = 0
   sub_eq_add_neg : ∀ a b : M, a - b = a + -b
 
+namespace NatModule
+
+variable {M : Type u} [NatModule M]
+
+theorem zero_add (a : M) : 0 + a = a := by
+  rw [add_comm, add_zero]
+
+end NatModule
+
 namespace IntModule
 
 attribute [instance 100] IntModule.toZero IntModule.toAdd IntModule.toNeg IntModule.toSub IntModule.toHMul
@@ -104,6 +113,12 @@ theorem sub_eq_iff {a b c : M} : a - b = c ↔ a = c + b := by
 theorem sub_eq_zero_iff {a b : M} : a - b = 0 ↔ a = b := by
   simp [sub_eq_iff, zero_add]
 
+theorem add_sub_cancel {a b : M} : a + b - b = a := by
+  rw [sub_eq_add_neg, add_assoc, add_neg_cancel, add_zero]
+
+theorem sub_add_cancel {a b : M} : a - b + b = a := by
+  rw [sub_eq_add_neg, add_assoc, neg_add_cancel, add_zero]
+
 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]
@@ -112,6 +127,12 @@ 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]
 
+theorem hmul_sub (k : Int) (a b : M) : k * (a - b) = k * a - k * b := by
+  rw [sub_eq_add_neg, hmul_add, hmul_neg, ← sub_eq_add_neg]
+
+theorem sub_hmul (k₁ k₂ : Int) (a : M) : (k₁ - k₂) * a = k₁ * a - k₂ * a := by
+  rw [Int.sub_eq_add_neg, add_hmul, neg_hmul, ← sub_eq_add_neg]
+
 end IntModule
 
 /--

src/Init/Grind/Ordered/Linarith.lean

@@ -7,6 +7,7 @@ module
 prelude
 import Init.Grind.Ordered.Module
 import Init.Grind.Ordered.Ring
+import Init.Grind.CommRing.Field
 import all Init.Data.Ord
 import all Init.Data.AC
 import Init.Data.RArray
@@ -83,6 +84,11 @@ theorem Poly.denote'_go_eq_denote {α} [IntModule α] (ctx : Context α) (p : Po
 theorem Poly.denote'_eq_denote {α} [IntModule α] (ctx : Context α) (p : Poly) : p.denote' ctx = p.denote ctx := by
   unfold denote' <;> split <;> simp [denote, denote'_go_eq_denote] <;> ac_rfl
 
+def Poly.coeff (p : Poly) (x : Var) : Int :=
+  match p with
+  | .add a y p => bif x == y then a else coeff p x
+  | .nil => 0
+
 def Poly.insert (k : Int) (v : Var) (p : Poly) : Poly :=
   match p with
   | .nil => .add k v .nil
@@ -283,12 +289,6 @@ theorem le_lt_combine {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α]
   replace h₂ := hmul_neg (↑p₁.leadCoeff.natAbs) h₂ |>.mp hp
   exact le_add_lt h₁ h₂
 
-theorem le_eq_combine {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ p₂ p₃ : Poly)
-    : le_le_combine_cert p₁ p₂ p₃ → p₁.denote' ctx ≤ 0 → p₂.denote' ctx = 0 → p₃.denote' ctx ≤ 0 := by
-  simp [le_le_combine_cert]; intro _ h₁ h₂; subst p₃; simp [h₂]
-  replace h₁ := hmul_nonpos (coe_natAbs_nonneg p₂.leadCoeff) h₁
-  assumption
-
 def lt_lt_combine_cert (p₁ p₂ p₃ : Poly) : Bool :=
   let a₁ := p₁.leadCoeff.natAbs
   let a₂ := p₂.leadCoeff.natAbs
@@ -301,21 +301,6 @@ theorem lt_lt_combine {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α]
   replace h₂ := hmul_neg (↑p₁.leadCoeff.natAbs) h₂ |>.mp hp₂
   exact lt_add_lt h₁ h₂
 
-def lt_eq_combine_cert (p₁ p₂ p₃ : Poly) : Bool :=
-  let a₁ := p₁.leadCoeff.natAbs
-  let a₂ := p₂.leadCoeff.natAbs
-  a₂ > (0 : Int) && p₃ == (p₁.mul a₂ |>.combine (p₂.mul a₁))
-
-theorem lt_eq_combine {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ p₂ p₃ : Poly)
-    : lt_eq_combine_cert p₁ p₂ p₃ → p₁.denote' ctx < 0 → p₂.denote' ctx = 0 → p₃.denote' ctx < 0 := by
-  simp [-Int.natAbs_pos, -Int.ofNat_pos, lt_eq_combine_cert]; intro hp₁ _ h₁ h₂; subst p₃; simp [h₂]
-  replace h₁ := hmul_neg (↑p₂.leadCoeff.natAbs) h₁ |>.mp hp₁
-  assumption
-
-theorem eq_eq_combine {α} [IntModule α] (ctx : Context α) (p₁ p₂ p₃ : Poly)
-    : le_le_combine_cert p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx = 0 → p₃.denote' ctx = 0 := by
-  simp [le_le_combine_cert]; intro _ h₁ h₂; subst p₃; simp [h₁, h₂]
-
 def diseq_split_cert (p₁ p₂ : Poly) : Bool :=
   p₂ == p₁.mul (-1)
 
@@ -335,30 +320,6 @@ theorem diseq_split_resolve {α} [IntModule α] [LinearOrder α] [IntModule.IsOr
   intro h₁ h₂ h₃
   exact (diseq_split ctx p₁ p₂ h₁ h₂).resolve_left h₃
 
-def eq_diseq_combine_cert (p₁ p₂ p₃ : Poly) : Bool :=
-  let a₁ := p₁.leadCoeff.natAbs
-  let a₂ := p₂.leadCoeff.natAbs
-  a₁ ≠ 0 && p₃ == (p₁.mul a₂ |>.combine (p₂.mul a₁))
-
-theorem eq_diseq_combine {α} [IntModule α] [NoNatZeroDivisors α] (ctx : Context α) (p₁ p₂ p₃ : Poly)
-    : eq_diseq_combine_cert p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx ≠ 0 → p₃.denote' ctx ≠ 0 := by
-  simp [- Int.natAbs_eq_zero, -Int.natCast_eq_zero, eq_diseq_combine_cert]; intro hne _ h₁ h₂; subst p₃
-  simp [h₁, h₂]; intro h
-  have := no_nat_zero_divisors (p₁.leadCoeff.natAbs) (p₂.denote ctx) hne h
-  contradiction
-
-def eq_diseq_combine_cert' (p₁ p₂ p₃ : Poly) (k : Int) : Bool :=
-  p₃ == (p₁.mul k |>.combine p₂)
-
-/-
-Special case of `eq_diseq_combine` where leading coefficient `c₁` of `p₁` is `-k*c₂`, where
-`c₂` is the leading coefficient of `p₂`.
--/
-theorem eq_diseq_combine' {α} [IntModule α] (ctx : Context α) (p₁ p₂ p₃ : Poly) (k : Int)
-    : eq_diseq_combine_cert' p₁ p₂ p₃ k → p₁.denote' ctx = 0 → p₂.denote' ctx ≠ 0 → p₃.denote' ctx ≠ 0 := by
-  simp [eq_diseq_combine_cert']; intro _ h₁ h₂; subst p₃
-  simp [h₁, h₂]
-
 /-!
 Helper theorems for internalizing facts into the linear arithmetic procedure
 -/
@@ -464,17 +425,57 @@ theorem zero_lt_one {α} [Ring α] [Preorder α] [Ring.IsOrdered α] (ctx : Cont
   simp [zero_lt_one_cert]; intro _ h; subst p; simp [Poly.denote, h, One.one, neg_hmul]
   rw [neg_lt_iff, neg_zero]; apply Ring.IsOrdered.zero_lt_one
 
+def zero_ne_one_cert (p : Poly) : Bool :=
+  p == .add 1 0 .nil
+
+theorem zero_ne_one_of_ord_ring {α} [Ring α] [Preorder α] [Ring.IsOrdered α] (ctx : Context α) (p : Poly)
+    : zero_ne_one_cert p → (0 : Var).denote ctx = One.one → p.denote' ctx ≠ 0 := by
+  simp [zero_ne_one_cert]; intro _ h; subst p; simp [Poly.denote, h, One.one]
+  intro h; have := Ring.IsOrdered.zero_lt_one (R := α); simp [h, Preorder.lt_irrefl] at this
+
+theorem zero_ne_one_of_field {α} [Field α] (ctx : Context α) (p : Poly)
+    : zero_ne_one_cert p → (0 : Var).denote ctx = One.one → p.denote' ctx ≠ 0 := by
+  simp [zero_ne_one_cert]; intro _ h; subst p; simp [Poly.denote, h, One.one]
+  intro h; have := Field.zero_ne_one (α := α); simp [h] at this
+
+theorem zero_ne_one_of_char0 {α} [Ring α] [IsCharP α 0] (ctx : Context α) (p : Poly)
+    : zero_ne_one_cert p → (0 : Var).denote ctx = One.one → p.denote' ctx ≠ 0 := by
+  simp [zero_ne_one_cert]; intro _ h; subst p; simp [Poly.denote, h, One.one]
+  intro h; have := IsCharP.intCast_eq_zero_iff (α := α) 0 1; simp [Ring.intCast_one] at this
+  contradiction
+
+def zero_ne_one_of_charC_cert (c : Nat) (p : Poly) : Bool :=
+  (c:Int) > 1 && p == .add 1 0 .nil
+
+theorem zero_ne_one_of_charC {α c} [Ring α] [IsCharP α c] (ctx : Context α) (p : Poly)
+    : zero_ne_one_of_charC_cert c p → (0 : Var).denote ctx = One.one → p.denote' ctx ≠ 0 := by
+  simp [zero_ne_one_of_charC_cert]; intro hc _ h; subst p; simp [Poly.denote, h, One.one]
+  intro h; have h' := IsCharP.intCast_eq_zero_iff (α := α) c 1; simp [Ring.intCast_one] at h'
+  replace h' := h'.mp h
+  have := Int.emod_eq_of_lt (by decide) hc
+  simp [this] at h'
+
 /-!
 Coefficient normalization
 -/
 
-def coeff_cert (p₁ p₂ : Poly) (k : Nat) :=
-  k > 0 && p₁ == p₂.mul k
+def eq_neg_cert (p₁ p₂ : Poly) :=
+  p₂ == p₁.mul (-1)
+
+theorem eq_neg {α} [IntModule α] (ctx : Context α) (p₁ p₂ : Poly)
+    : eq_neg_cert p₁ p₂ → p₁.denote' ctx = 0 → p₂.denote' ctx = 0 := by
+  simp [eq_neg_cert]; intros; simp [*]
+
+def eq_coeff_cert (p₁ p₂ : Poly) (k : Nat) :=
+  k != 0 && p₁ == p₂.mul k
 
 theorem eq_coeff {α} [IntModule α] [NoNatZeroDivisors α] (ctx : Context α) (p₁ p₂ : Poly) (k : Nat)
-    : coeff_cert p₁ p₂ k → p₁.denote' ctx = 0 → p₂.denote' ctx = 0 := by
-  simp [coeff_cert]; intro h _; subst p₁; simp
-  exact no_nat_zero_divisors k (p₂.denote ctx) (Nat.ne_zero_of_lt h)
+    : eq_coeff_cert p₁ p₂ k → p₁.denote' ctx = 0 → p₂.denote' ctx = 0 := by
+  simp [eq_coeff_cert]; intro h _; subst p₁; simp [*]
+  exact no_nat_zero_divisors k (p₂.denote ctx) h
+
+def coeff_cert (p₁ p₂ : Poly) (k : Nat) :=
+  k > 0 && p₁ == p₂.mul k
 
 theorem le_coeff {α} [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ p₂ : Poly) (k : Nat)
     : coeff_cert p₁ p₂ k → p₁.denote' ctx ≤ 0 → p₂.denote' ctx ≤ 0 := by
@@ -499,4 +500,65 @@ theorem diseq_neg {α} [IntModule α] (ctx : Context α) (p p' : Poly) : p' == p
   intro h; replace h := congrArg (- ·) h; simp [neg_neg, neg_zero] at h
   contradiction
 
+/-!
+Substitution
+-/
+
+def eq_diseq_subst_cert (k₁ k₂ : Int) (p₁ p₂ p₃ : Poly) : Bool :=
+  k₁.natAbs ≠ 0 && p₃ == (p₁.mul k₂ |>.combine (p₂.mul k₁))
+
+theorem eq_diseq_subst {α} [IntModule α] [NoNatZeroDivisors α] (ctx : Context α) (k₁ k₂ : Int) (p₁ p₂ p₃ : Poly)
+    : eq_diseq_subst_cert k₁ k₂ p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx ≠ 0 → p₃.denote' ctx ≠ 0 := by
+  simp [eq_diseq_subst_cert, - Int.natAbs_eq_zero, -Int.natCast_eq_zero]; intro hne _ h₁ h₂; subst p₃
+  simp [h₁, h₂]; intro h₃
+  have :  k₁.natAbs * Poly.denote ctx p₂ = 0 := by
+    have : (k₁.natAbs : Int) * Poly.denote ctx p₂ = 0 := by
+      cases Int.natAbs_eq_iff.mp (Eq.refl k₁.natAbs)
+      next h => rw [← h]; assumption
+      next h => replace h := congrArg (- ·) h; simp at h; rw [← h, IntModule.neg_hmul, h₃, IntModule.neg_zero]
+    exact this
+  have := no_nat_zero_divisors (k₁.natAbs) (p₂.denote ctx) hne this
+  contradiction
+
+def eq_diseq_subst1_cert (k : Int) (p₁ p₂ p₃ : Poly) : Bool :=
+  p₃ == (p₁.mul k |>.combine p₂)
+
+/-
+Special case of `diseq_eq_subst` where leading coefficient `c₁` of `p₁` is `-k*c₂`, where
+`c₂` is the leading coefficient of `p₂`.
+-/
+theorem eq_diseq_subst1 {α} [IntModule α] (ctx : Context α) (k : Int) (p₁ p₂ p₃ : Poly)
+    : eq_diseq_subst1_cert k p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx ≠ 0 → p₃.denote' ctx ≠ 0 := by
+  simp [eq_diseq_subst1_cert]; intro _ h₁ h₂; subst p₃
+  simp [h₁, h₂]
+
+def eq_le_subst_cert (x : Var) (p₁ p₂ p₃ : Poly) :=
+  let a := p₁.coeff x
+  let b := p₂.coeff x
+  a ≥ 0 && p₃ == (p₂.mul a |>.combine (p₁.mul (-b)))
+
+theorem eq_le_subst {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (x : Var) (p₁ p₂ p₃ : Poly)
+    : eq_le_subst_cert x p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx ≤ 0 → p₃.denote' ctx ≤ 0 := by
+  simp [eq_le_subst_cert]; intro h _ h₁ h₂; subst p₃; simp [h₁]
+  exact hmul_nonpos h h₂
+
+def eq_lt_subst_cert (x : Var) (p₁ p₂ p₃ : Poly) :=
+  let a := p₁.coeff x
+  let b := p₂.coeff x
+  a > 0 && p₃ == (p₂.mul a |>.combine (p₁.mul (-b)))
+
+theorem eq_lt_subst {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (x : Var) (p₁ p₂ p₃ : Poly)
+    : eq_lt_subst_cert x p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx < 0 → p₃.denote' ctx < 0 := by
+  simp [eq_lt_subst_cert]; intro h _ h₁ h₂; subst p₃; simp [h₁]
+  exact IsOrdered.hmul_neg (p₁.coeff x) h₂ |>.mp h
+
+def eq_eq_subst_cert (x : Var) (p₁ p₂ p₃ : Poly) :=
+  let a := p₁.coeff x
+  let b := p₂.coeff x
+  p₃ == (p₂.mul a |>.combine (p₁.mul (-b)))
+
+theorem eq_eq_subst {α} [IntModule α] (ctx : Context α) (x : Var) (p₁ p₂ p₃ : Poly)
+    : eq_eq_subst_cert x p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx = 0 → p₃.denote' ctx = 0 := by
+  simp [eq_eq_subst_cert]; intro _ h₁ h₂; subst p₃; simp [h₁, h₂]
+
 end Lean.Grind.Linarith

src/Init/Grind/Ordered/Module.lean

@@ -12,12 +12,57 @@ import Init.Grind.Ordered.Order
 
 namespace Lean.Grind
 
+class NatModule.IsOrdered (M : Type u) [Preorder M] [NatModule M] where
+  add_le_left_iff : ∀ {a b : M} (c : M), a ≤ b ↔ a + c ≤ b + c
+  hmul_pos : ∀ (k : Nat) {a : M}, 0 < a → (0 < k ↔ 0 < k * a)
+  hmul_nonneg : ∀ {k : Nat} {a : M}, 0 ≤ a → 0 ≤ k * a
+
 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 NatModule.IsOrdered
+
+variable {M : Type u} [Preorder M] [NatModule M] [NatModule.IsOrdered M]
+
+theorem add_le_right_iff {a b : M} (c : M) : a ≤ b ↔ c + a ≤ c + b := by
+  rw [add_comm c a, add_comm c b,add_le_left_iff]
+
+theorem add_le_left {a b : M} (h : a ≤ b) (c : M) : a + c ≤ b + c :=
+  (add_le_left_iff c).mp h
+
+theorem add_le_right {a b : M} (h : a ≤ b) (c : M) : c + a ≤ c + b :=
+  (add_le_right_iff c).mp h
+
+theorem add_lt_left {a b : M} (h : a < b) (c : M) : a + c < b + c := by
+  simp only [Preorder.lt_iff_le_not_le] at h ⊢
+  constructor
+  · exact add_le_left h.1 _
+  · intro w
+    apply h.2
+    exact (add_le_left_iff c).mpr w
+
+theorem add_lt_right {a b : M} (h : a < b) (c : M) : c + a < c + b := by
+  rw [add_comm c a, add_comm c b]
+  exact add_lt_left h c
+
+theorem add_lt_left_iff {a b : M} (c : M) : a < b ↔ a + c < b + c := by
+  constructor
+  · exact fun h => add_lt_left h c
+  · intro w
+    simp only [Preorder.lt_iff_le_not_le] at w ⊢
+    constructor
+    · exact (add_le_left_iff c).mpr w.1
+    · intro h
+      exact w.2 ((add_le_left_iff c).mp h)
+
+theorem add_lt_right_iff {a b : M} (c : M) : a < b ↔ c + a < c + b := by
+  rw [add_comm c a, add_comm c b, add_lt_left_iff]
+
+end NatModule.IsOrdered
+
 namespace IntModule.IsOrdered
 
 variable {M : Type u} [Preorder M] [IntModule M] [IntModule.IsOrdered M]
@@ -41,7 +86,7 @@ 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 ⊢
+  simp only [Preorder.lt_iff_le_not_le] at h ⊢
   constructor
   · exact add_le_left h.1 _
   · intro w
@@ -58,12 +103,59 @@ 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 add_le_left_iff {a b : M} (c : M) : a ≤ b ↔ a + c ≤ b + c := by
+  constructor
+  · intro w
+    exact add_le_left w c
+  · intro w
+    have := add_le_left w (-c)
+    rwa [add_assoc, add_neg_cancel, add_zero, add_assoc, add_neg_cancel, add_zero] at this
+
+theorem add_le_right_iff {a b : M} (c : M) : a ≤ b ↔ c + a ≤ c + b := by
+  constructor
+  · intro w
+    exact add_le_right c w
+  · intro w
+    have := add_le_right (-c) w
+    rwa [← add_assoc, neg_add_cancel, zero_add, ← add_assoc, neg_add_cancel, zero_add] at this
+
+theorem add_lt_left_iff {a b : M} (c : M) : a < b ↔ a + c < b + c := by
+  constructor
+  · intro w
+    exact add_lt_left w c
+  · intro w
+    have := add_lt_left w (-c)
+    rwa [add_assoc, add_neg_cancel, add_zero, add_assoc, add_neg_cancel, add_zero] at this
+
+theorem add_lt_right_iff {a b : M} (c : M) : a < b ↔ c + a < c + b := by
+  constructor
+  · intro w
+    exact add_lt_right c w
+  · intro w
+    have := add_lt_right (-c) w
+    rwa [← add_assoc, neg_add_cancel, zero_add, ← add_assoc, neg_add_cancel, zero_add] at this
+
+theorem sub_nonneg_iff {a b : M} : 0 ≤ a - b ↔ b ≤ a := by
+  rw [add_le_left_iff b, zero_add, sub_add_cancel]
+
 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)
 
+theorem hmul_le_hmul_of_le_of_le_of_nonneg_of_nonneg
+    {k₁ k₂ : Int} {x y : M} (hk : k₁ ≤ k₂) (h : x ≤ y) (w : 0 ≤ k₁) (w' : 0 ≤ x) :
+    k₁ * x ≤ k₂ * y := by
+  apply Preorder.le_trans
+  · have : 0 ≤ k₁ * (y - x) := hmul_nonneg w (sub_nonneg_iff.mpr h)
+    rwa [IntModule.hmul_sub, sub_nonneg_iff] at this
+  · have : 0 ≤ (k₂ - k₁) * y := hmul_nonneg (Int.sub_nonneg.mpr hk) (Preorder.le_trans w' h)
+    rwa [IntModule.sub_hmul, sub_nonneg_iff] at this
+
+theorem add_le_add {a b c d : M} (hab : a ≤ b) (hcd : c ≤ d) : a + c ≤ b + d :=
+  Preorder.le_trans (add_le_right a hcd) (add_le_left hab d)
+
 end IntModule.IsOrdered
 
 end Lean.Grind

src/Lean/BuiltinDocAttr.lean

@@ -22,8 +22,8 @@ This allows the documentation of core Lean features to be visible without import
 are defined in. This is only useful during bootstrapping and should not be used outside of
 the Lean source code.
 -/
-@[builtin_init, builtin_doc]
-private def initFn :=
+@[builtin_doc]
+builtin_initialize
   registerBuiltinAttribute {
     name  := `builtin_doc
     descr := "make the docs and location of this declaration available as a builtin"

src/Lean/Compiler/LCNF/FloatLetIn.lean

@@ -118,13 +118,12 @@ up to this point, with respect to `cs`. The initial decisions are:
 -/
 def initialDecisions (cs : Cases) : BaseFloatM (Std.HashMap FVarId Decision) := do
   let mut map := Std.HashMap.emptyWithCapacity (← read).decls.length
-  let folder val acc := do
+  map ← (← read).decls.foldrM (init := map) fun val acc => do
     if let .let decl := val then
       if (← ignore? decl) then
         return acc.insert decl.fvarId .dont
     return acc.insert val.fvarId .unknown
 
-  map ← (← read).decls.foldrM (init := map) folder
   if map.contains cs.discr then
     map := map.insert cs.discr .dont
   (_, map) ← goCases cs |>.run map
@@ -135,7 +134,7 @@ where
       if decision == .unknown then
         modify fun s => s.insert var plannedDecision
       else if decision != plannedDecision then
-          modify fun s => s.insert var .dont
+        modify fun s => s.insert var .dont
       -- otherwise we already have the proper decision
 
   goAlt (alt : Alt) : StateRefT (Std.HashMap FVarId Decision) BaseFloatM Unit :=
@@ -229,10 +228,10 @@ def float (decl : CodeDecl) : FloatM Unit := do
 where
   goFVar (fvar : FVarId) (arm : Decision) : FloatM Unit := do
     let some decision := (← get).decision[fvar]? | return ()
-    if decision != arm then
-      modify fun s => { s with decision := s.decision.insert fvar .dont }
-    else if decision == .unknown then
+    if decision == .unknown then
       modify fun s => { s with decision := s.decision.insert fvar arm }
+    else if decision != arm then
+      modify fun s => { s with decision := s.decision.insert fvar .dont }
 
 /--
 Iterate through `decl`, pushing local declarations that are only used in one
@@ -285,14 +284,13 @@ where
       }
       let (_, res) ← goCases |>.run base
       let remainders := res.newArms[Decision.dont]!
-      let altMapper alt := do
+      let newAlts ← cs.alts.mapM fun alt => do
         let decision := Decision.ofAlt alt
         let newCode := res.newArms[decision]!
         trace[Compiler.floatLetIn] "Size of code that was pushed into arm: {repr decision} {newCode.length}"
         let fused ← withNewScope do
           go (attachCodeDecls newCode.toArray alt.getCode)
         return alt.updateCode fused
-      let newAlts ← cs.alts.mapM altMapper
       let mut newCases := Code.updateCases! code cs.resultType cs.discr newAlts
       return attachCodeDecls remainders.toArray newCases
     | .jmp .. | .return .. | .unreach .. =>

src/Lean/Data/Name.lean

@@ -185,6 +185,11 @@ def anyS (n : Name) (f : String → Bool) : Bool :=
   | .num p _ => p.anyS f
   | _ => false
 
+/-- Return true if the name is in a namespace associated to metaprogramming. -/
+def isMetaprogramming (n : Name) : Bool :=
+  let components := n.components
+  components.head? == some `Lean || (components.any fun n => n == `Tactic || n == `Linter)
+
 end Name
 end Lean
 

src/Lean/Elab/InheritDoc.lean

@@ -14,8 +14,8 @@ Uses documentation from a specified declaration.
 
 `@[inherit_doc decl]` is used to inherit the documentation from the declaration `decl`.
 -/
-@[builtin_init, builtin_doc]
-private def init :=
+@[builtin_doc]
+builtin_initialize
   registerBuiltinAttribute {
     name := `inherit_doc
     descr := "inherit documentation from a specified declaration"

src/Lean/Elab/MutualDef.lean

@@ -32,8 +32,8 @@ Makes the bodies of definitions available to importing modules.
 This only has an effect if both the module the definition is defined in and the importing module
 have the module system enabled.
 -/
-@[builtin_init, builtin_doc]
-private def init :=
+@[builtin_doc]
+builtin_initialize
   registerBuiltinAttribute {
     name := `expose
     descr := "(module system) Make bodies of definitions available to importing modules."
@@ -49,8 +49,8 @@ be exposed in a section tagged `@[expose]`
 This only has an effect if both the module the definition is defined in and the importing module
 have the module system enabled.
 -/
-@[builtin_init, builtin_doc]
-private def init2 :=
+@[builtin_doc]
+builtin_initialize
   registerBuiltinAttribute {
     name := `no_expose
     descr := "(module system) Negate previous `[expose]` attribute."

src/Lean/Elab/Structure.lean

@@ -840,8 +840,6 @@ where
             name := toParentName
             declName := parentFieldInfo.declName
           }
-          if parentView.name?.isSome then
-            Term.addTermInfo' parentView.projRef parentFieldInfo.fvar (isBinder := true)
           go (i + 1)
     else
       k
@@ -997,7 +995,6 @@ where
                            name := view.name, declName := view.declName, fvar := fieldFVar, default? := default?,
                            binfo := view.binderInfo, paramInfoOverrides,
                            kind := StructFieldKind.newField }
-            Term.addTermInfo' view.nameId fieldFVar (isBinder := true)
             go (i+1)
         | none, some (.optParam value) =>
           let type ← inferType value
@@ -1006,7 +1003,6 @@ where
                            name := view.name, declName := view.declName, fvar := fieldFVar, default? := default?,
                            binfo := view.binderInfo, paramInfoOverrides,
                            kind := StructFieldKind.newField }
-            Term.addTermInfo' view.nameId fieldFVar (isBinder := true)
             go (i+1)
         | none, some (.autoParam _) =>
           throwError "field '{view.name}' has an autoparam but no type"

src/Lean/Elab/Tactic/Monotonicity.lean

@@ -36,8 +36,8 @@ Monotonicity theorems should have `Lean.Order.monotone ...` as a conclusion. The
 `monotonicity` tactic (scoped in the `Lean.Order` namespace) to automatically prove monotonicity
 for functions defined using `partial_fixpoint`.
 -/
-@[builtin_init, builtin_doc]
-private def init := registerBuiltinAttribute {
+@[builtin_doc]
+builtin_initialize registerBuiltinAttribute {
   name := `partial_fixpoint_monotone
   descr := "monotonicity theorem"
   add := fun decl _ kind => MetaM.run' do

src/Lean/Elab/Term.lean

@@ -2100,8 +2100,8 @@ builtin_initialize builtinIncrementalElabs : IO.Ref NameSet ← IO.mkRef {}
 def addBuiltinIncrementalElab (decl : Name) : IO Unit := do
   builtinIncrementalElabs.modify fun s => s.insert decl
 
-@[builtin_init, inherit_doc incrementalAttr, builtin_doc]
-private def init :=
+@[inherit_doc incrementalAttr, builtin_doc]
+builtin_initialize
   registerBuiltinAttribute {
     name            := `builtin_incremental
     descr           := s!"(builtin) {incrementalAttr.attr.descr}"

src/Lean/Meta/Instances.lean

@@ -242,8 +242,8 @@ in particular for `opaque` instances.
 To assign priorities to instances, `@[instance prio]` can be used (where `prio` is a priority).
 This corresponds to the `instance (priority := prio)` notation.
 -/
-@[builtin_init, builtin_doc]
-private def init :=
+@[builtin_doc]
+builtin_initialize
   registerBuiltinAttribute {
     name  := `instance
     descr := "type class instance"

src/Lean/Meta/Tactic/ElimInfo.lean

@@ -209,8 +209,8 @@ example (x : Three) (p : Three → Prop) : p x := by
 
 `@[cases_eliminator]` works similarly for the `cases` tactic.
 -/
-@[builtin_init, builtin_doc]
-private def init : IO Unit :=
+@[builtin_doc]
+builtin_initialize
   registerBuiltinAttribute {
     name  := `induction_eliminator
     descr := "custom `rec`-like eliminator for the `induction` tactic"
@@ -249,8 +249,8 @@ example (x : Three) (p : Three → Prop) : p x := by
 
 `@[induction_eliminator]` works similarly for the `induction` tactic.
 -/
-@[builtin_init, builtin_doc]
-private def init2 : IO Unit :=
+@[builtin_doc]
+builtin_initialize
   registerBuiltinAttribute {
     name  := `cases_eliminator
     descr := "custom `casesOn`-like eliminator for the `cases` tactic"

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

@@ -129,22 +129,8 @@ where
     let commRing := mkApp (mkConst ``Grind.CommRing [u]) type
     let .some commRingInst ← trySynthInstance commRing | return none
     trace_goal[grind.ring] "new ring: {type}"
-    let charInst? ← withNewMCtxDepth do
-      let n ← mkFreshExprMVar (mkConst ``Nat)
-      let charType := mkApp3 (mkConst ``Grind.IsCharP [u]) type ringInst n
-      let .some charInst ← trySynthInstance charType | pure none
-      let n ← instantiateMVars n
-      let some n ← evalNat n |>.run
-        | trace_goal[grind.ring] "found instance for{indentExpr charType}\nbut characteristic is not a natural number"; pure none
-      trace_goal[grind.ring] "characteristic: {n}"
-      pure <| some (charInst, n)
-    let noZeroDivInst? ← withNewMCtxDepth do
-      let zeroType := mkApp (mkConst ``Zero [u]) type
-      let .some zeroInst ← trySynthInstance zeroType | return none
-      let hmulType := mkApp3 (mkConst ``HMul [0, u, u]) (mkConst ``Nat []) type type
-      let .some hmulInst ← trySynthInstance hmulType | return none
-      let noZeroDivType := mkApp3 (mkConst ``Grind.NoNatZeroDivisors [u]) type zeroInst hmulInst
-      LOption.toOption <$> trySynthInstance noZeroDivType
+    let charInst? ← getIsCharInst? u type ringInst
+    let noZeroDivInst? ← getNoZeroDivInst? u type
     trace_goal[grind.ring] "NoNatZeroDivisors available: {noZeroDivInst?.isSome}"
     let field := mkApp (mkConst ``Grind.Field [u]) type
     let fieldInst? : Option Expr ← LOption.toOption <$> trySynthInstance field

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

@@ -120,16 +120,8 @@ private def updateDvdCnstr (a : Int) (x : Var) (c : EqCnstr) (y : Var) : GoalM U
   let c' ← c'.applyEq a x c b
   c'.assert
 
-private def split (x : Var) (cs : PArray LeCnstr) : GoalM (PArray LeCnstr × Array (Int × LeCnstr)) := do
-  let mut cs' := {}
-  let mut todo := #[]
-  for c in cs do
-    let b := c.p.coeff x
-    if b == 0 then
-      cs' := cs'.push c
-    else
-      todo := todo.push (b, c)
-  return (cs', todo)
+private def splitLeCnstrs (x : Var) (cs : PArray LeCnstr) : PArray LeCnstr × Array (Int × LeCnstr) :=
+  split cs fun c => c.p.coeff x
 
 /--
 Given an equation `c₁` containing `a*x`, eliminate `x` from the inequalities in `todo`.
@@ -146,7 +138,7 @@ Given an equation `c₁` containing `a*x`, eliminate `x` from lower bound inequa
 -/
 private def updateLowers (a : Int) (x : Var) (c : EqCnstr) (y : Var) : GoalM Unit := do
   if (← inconsistent) then return ()
-  let (lowers', todo) ← split x (← get').lowers[y]!
+  let (lowers', todo) := splitLeCnstrs x (← get').lowers[y]!
   modify' fun s => { s with lowers := s.lowers.set y lowers' }
   updateLeCnstrs a x c todo
 
@@ -155,24 +147,16 @@ Given an equation `c₁` containing `a*x`, eliminate `x` from upper bound inequa
 -/
 private def updateUppers (a : Int) (x : Var) (c : EqCnstr) (y : Var) : GoalM Unit := do
   if (← inconsistent) then return ()
-  let (uppers', todo) ← split x (← get').uppers[y]!
+  let (uppers', todo) := splitLeCnstrs x (← get').uppers[y]!
   modify' fun s => { s with uppers := s.uppers.set y uppers' }
   updateLeCnstrs a x c todo
 
-private def splitDiseqs (x : Var) (cs : PArray DiseqCnstr) : GoalM (PArray DiseqCnstr × Array (Int × DiseqCnstr)) := do
-  let mut cs' := {}
-  let mut todo := #[]
-  for c in cs do
-    let b := c.p.coeff x
-    if b == 0 then
-      cs' := cs'.push c
-    else
-      todo := todo.push (b, c)
-  return (cs', todo)
+private def splitDiseqs (x : Var) (cs : PArray DiseqCnstr) : PArray DiseqCnstr × Array (Int × DiseqCnstr) :=
+  split cs fun c => c.p.coeff x
 
 private def updateDiseqs (a : Int) (x : Var) (c : EqCnstr) (y : Var) : GoalM Unit := do
   if (← inconsistent) then return ()
-  let (diseqs', todo) ← splitDiseqs x (← get').diseqs[y]!
+  let (diseqs', todo) := splitDiseqs x (← get').diseqs[y]!
   modify' fun s => { s with diseqs := s.diseqs.set y diseqs' }
   for (b, c₂) in todo do
     let c₂ ← c₂.applyEq a x c b

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

@@ -114,11 +114,10 @@ def LeCnstr.assertImpl (c : LeCnstr) : GoalM Unit := do
     return ()
   let c ← refineWithDiseq c
   trace[grind.cutsat.assert.store] "{← c.pp}"
+  c.p.updateOccs
   if a < 0 then
-    c.p.updateOccs
     modify' fun s => { s with lowers := s.lowers.modify x (·.push c) }
   else
-    c.p.updateOccs
     modify' fun s => { s with uppers := s.uppers.modify x (·.push c) }
   if (← c.satisfied) == .false then
     resetAssignmentFrom x

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

@@ -6,11 +6,13 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Meta.Tactic.Grind.Arith.Offset
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Inv
+import Lean.Meta.Tactic.Grind.Arith.Linear.Inv
 
 namespace Lean.Meta.Grind.Arith
 
 def checkInvariants : GoalM Unit := do
   Offset.checkInvariants
   Cutsat.checkInvariants
+  Linear.checkInvariants
 
 end Lean.Meta.Grind.Arith

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

@@ -30,11 +30,13 @@ builtin_initialize registerTraceClass `grind.linarith.model
 builtin_initialize registerTraceClass `grind.linarith.assert.unsat (inherited := true)
 builtin_initialize registerTraceClass `grind.linarith.assert.trivial (inherited := true)
 builtin_initialize registerTraceClass `grind.linarith.assert.store (inherited := true)
+builtin_initialize registerTraceClass `grind.linarith.assert.ignored (inherited := true)
 
 builtin_initialize registerTraceClass `grind.debug.linarith.search
 builtin_initialize registerTraceClass `grind.debug.linarith.search.conflict (inherited := true)
 builtin_initialize registerTraceClass `grind.debug.linarith.search.assign (inherited := true)
 builtin_initialize registerTraceClass `grind.debug.linarith.search.split (inherited := true)
 builtin_initialize registerTraceClass `grind.debug.linarith.search.backtrack (inherited := true)
+builtin_initialize registerTraceClass `grind.debug.linarith.subst
 
 end Lean

src/Lean/Meta/Tactic/Grind/Arith/Linear/DenoteExpr.lean

@@ -59,6 +59,9 @@ private def denoteIneq (p : Poly) (strict : Bool) : M Expr := do
 def IneqCnstr.denoteExpr (c : IneqCnstr) : M Expr := do
   denoteIneq c.p c.strict
 
+def EqCnstr.denoteExpr (c : EqCnstr) : M Expr := do
+  mkEq (← c.p.denoteExpr) (← getStruct).ofNatZero
+
 private def denoteNum (k : Int) : LinearM Expr := do
   return mkApp2 (← getStruct).hmulFn (mkIntLit k) (← getOne)
 

src/Lean/Meta/Tactic/Grind/Arith/Linear/IneqCnstr.lean

@@ -38,6 +38,7 @@ def IneqCnstr.assert (c : IneqCnstr) : LinearM Unit := do
       trace[grind.linarith.trivial] "{← c.denoteExpr}"
   | .add a x _ =>
     trace[grind.linarith.assert.store] "{← c.denoteExpr}"
+    c.p.updateOccs
     if a < 0 then
       modifyStruct fun s => { s with lowers := s.lowers.modify x (·.push c) }
     else

src/Lean/Meta/Tactic/Grind/Arith/Linear/Inv.lean

@@ -0,0 +1,106 @@
+/-
+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.Arith.Linear.Util
+
+namespace Lean.Meta.Grind.Arith.Linear
+
+/--
+Returns `true` if the variables in the given polynomial are sorted
+in decreasing order.
+-/
+def _root_.Lean.Grind.Linarith.Poly.isSorted (p : Poly) : Bool :=
+  go none p
+where
+  go : Option Var → Poly → Bool
+  | _,      .nil       => true
+  | none,   .add _ y p => go (some y) p
+  | some x, .add _ y p => x > y && go (some y) p
+
+/-- Returns `true` if all coefficients are not `0`. -/
+def _root_.Lean.Grind.Linarith.Poly.checkCoeffs : Poly → Bool
+  | .nil => true
+  | .add k _ p => k != 0 && checkCoeffs p
+
+def _root_.Lean.Grind.Linarith.Poly.checkOccs (p : Poly) : LinearM Unit := do
+  let .add _ y p := p | return ()
+  let rec go (p : Poly) : LinearM Unit := do
+    let .add _ x p := p | return ()
+    assert! (← getOccursOf x).contains y
+    go p
+  go p
+
+def _root_.Lean.Grind.Linarith.Poly.checkNoElimVars (p : Poly) : LinearM Unit := do
+  let .add _ x p := p | return ()
+  assert! !(← eliminated x)
+  checkNoElimVars p
+
+def _root_.Lean.Grind.Linarith.Poly.checkCnstrOf (p : Poly) (x : Var) : LinearM Unit := do
+  assert! p.isSorted
+  assert! p.checkCoeffs
+  unless (← inconsistent) do
+    p.checkNoElimVars
+    p.checkOccs
+    pure ()
+  let .add _ y _ := p | unreachable!
+  assert! x == y
+
+def checkLeCnstrs (css : PArray (PArray IneqCnstr)) (isLower : Bool) : LinearM Unit := do
+  let mut x := 0
+  for cs in css do
+    for c in cs do
+      c.p.checkCnstrOf x
+      let .add a _ _ := c.p | unreachable!
+      assert! isLower == (a < 0)
+    x := x + 1
+  return ()
+
+def checkLowers : LinearM Unit := do
+  let s ← getStruct
+  assert! s.lowers.size == s.vars.size
+  checkLeCnstrs s.lowers (isLower := true)
+
+def checkUppers : LinearM Unit := do
+  let s ← getStruct
+  assert! s.uppers.size == s.vars.size
+  checkLeCnstrs s.uppers (isLower := false)
+
+def checkDiseqCnstrs : LinearM Unit := do
+  let s ← getStruct
+  assert! s.vars.size == s.diseqs.size
+  let mut x := 0
+  for cs in s.diseqs do
+    for c in cs do
+      c.p.checkCnstrOf x
+    x := x + 1
+  return ()
+
+def checkVars : LinearM Unit := do
+  let s ← getStruct
+  let mut num := 0
+  for ({ expr }, var) in s.varMap do
+    if h : var < s.vars.size then
+      let expr' := s.vars[var]
+      assert! isSameExpr expr expr'
+    else
+      unreachable!
+    num := num + 1
+  assert! s.vars.size == num
+
+def checkStructInvs : LinearM Unit := do
+  checkVars
+  checkLowers
+  checkUppers
+  checkDiseqCnstrs
+
+def checkInvariants : GoalM Unit := do
+  unless grind.debug.get (← getOptions) do return ()
+  for structId in [: (← get').structs.size] do
+    LinearM.run structId do
+      assert! (← getStructId) == structId
+      checkStructInvs
+
+end Lean.Meta.Grind.Arith.Linear

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

@@ -125,6 +125,14 @@ private def mkIntModThmPrefix (declName : Name) : ProofM Expr := do
   let s ← getStruct
   return mkApp3 (mkConst declName [s.u]) s.type s.intModuleInst (← getContext)
 
+/--
+Returns the prefix of a theorem with name `declName` where the first three arguments are
+`{α} [IntModule α] [NoNatZeroDivisors α] (ctx : Context α)`
+-/
+private def mkIntModNoNatDivThmPrefix (declName : Name) : ProofM Expr := do
+  let s ← getStruct
+  return mkApp4 (mkConst declName [s.u]) s.type s.intModuleInst (← getNoNatDivInst) (← getContext)
+
 /--
 Returns the prefix of a theorem with name `declName` where the first four arguments are
 `{α} [IntModule α] [Preorder α] (ctx : Context α)`
@@ -237,6 +245,32 @@ partial def DiseqCnstr.toExprProof (c' : DiseqCnstr) : ProofM Expr := caching c'
   | .neg c =>
     let h ← mkIntModThmPrefix ``Grind.Linarith.diseq_neg
     return mkApp4 h (← mkPolyDecl c.p) (← mkPolyDecl c'.p) reflBoolTrue (← c.toExprProof)
+  | .subst k₁ k₂ c₁ c₂ =>
+    let h ← mkIntModNoNatDivThmPrefix ``Grind.Linarith.eq_diseq_subst
+    return mkApp8 h (toExpr k₁) (toExpr k₂) (← mkPolyDecl c₁.p) (← mkPolyDecl c₂.p) (← mkPolyDecl c'.p)
+      reflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
+  | .subst1 k c₁ c₂ =>
+    let h ← mkIntModThmPrefix ``Grind.Linarith.eq_diseq_subst1
+    return mkApp7 h (toExpr k) (← mkPolyDecl c₁.p) (← mkPolyDecl c₂.p) (← mkPolyDecl c'.p) reflBoolTrue
+      (← c₁.toExprProof) (← c₂.toExprProof)
+  | .oneNeZero => throwError "NIY"
+
+partial def EqCnstr.toExprProof (c' : EqCnstr) : ProofM Expr := caching c' do
+  match c'.h with
+  | .core a b lhs rhs =>
+    let h ← mkIntModThmPrefix ``Grind.Linarith.eq_norm
+    return mkApp5 h (← mkExprDecl lhs) (← mkExprDecl rhs) (← mkPolyDecl c'.p) reflBoolTrue (← mkEqProof a b)
+  | .coreCommRing a b ra rb p lhs' => throwError "NIY"
+  | .neg c =>
+    let h ← mkIntModThmPrefix ``Grind.Linarith.eq_neg
+    return mkApp4 h (← mkPolyDecl c.p) (← mkPolyDecl c'.p) reflBoolTrue (← c.toExprProof)
+  | .coeff k c =>
+    let h ← mkIntModNoNatDivThmPrefix ``Grind.Linarith.eq_coeff
+    return mkApp5 h (← mkPolyDecl c.p) (← mkPolyDecl c'.p) (toExpr k) reflBoolTrue (← c.toExprProof)
+  | .subst x c₁ c₂ =>
+    let h ← mkIntModThmPrefix ``Grind.Linarith.eq_eq_subst
+    return mkApp7 h (toExpr x) (← mkPolyDecl c₁.p) (← mkPolyDecl c₂.p) (← mkPolyDecl c'.p) reflBoolTrue
+      (← c₁.toExprProof) (← c₂.toExprProof)
 
 partial def UnsatProof.toExprProofCore (h : UnsatProof) : ProofM Expr := do
   match h with
@@ -271,13 +305,21 @@ partial def IneqCnstr.collectDecVars (c' : IneqCnstr) : CollectDecVarsM Unit :=
   | .norm c₁ _ => c₁.collectDecVars
   | .dec h => markAsFound h
   | .ofDiseqSplit (decVars := decVars) .. => decVars.forM markAsFound
+  | .subst _ c₁ c₂ => c₁.collectDecVars; c₂.collectDecVars
 
 -- `DiseqCnstr` is currently mutually recursive with `IneqCnstr`, but it will be in the future.
 -- Actually, it cannot even contain decision variables in the current implementation.
 partial def DiseqCnstr.collectDecVars (c' : DiseqCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c') do
   match c'.h with
-  | .core .. | .coreCommRing .. => return ()
+  | .core .. | .coreCommRing .. | .oneNeZero => return ()
   | .neg c => c.collectDecVars
+  | .subst _ _ c₁ c₂ | .subst1 _ c₁ c₂ => c₁.collectDecVars; c₂.collectDecVars
+
+partial def EqCnstr.collectDecVars (c' : EqCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c') do
+  match c'.h with
+  | .subst _ c₁ c₂ => c₁.collectDecVars; c₂.collectDecVars
+  | .core .. | .coreCommRing .. => return ()
+  | .neg c | .coeff _ c => c.collectDecVars
 
 end
 

src/Lean/Meta/Tactic/Grind/Arith/Linear/PropagateEq.lean

@@ -15,6 +15,32 @@ import Lean.Meta.Tactic.Grind.Arith.Linear.DenoteExpr
 import Lean.Meta.Tactic.Grind.Arith.Linear.Proof
 
 namespace Lean.Meta.Grind.Arith.Linear
+
+private def _root_.Lean.Grind.Linarith.Poly.substVar (p : Poly) : LinearM (Option (Var × EqCnstr × Poly)) := do
+  let some (a, x, c) ← p.findVarToSubst | return none
+  let b := c.p.coeff x
+  let p' := p.mul (-b) |>.combine (c.p.mul a)
+  trace[grind.debug.linarith.subst] "{← p.denoteExpr}, {a}, {← getVar x}, {← c.denoteExpr}, {b}, {← p'.denoteExpr}"
+  return some (x, c, p')
+
+/--
+Given an equation `c₁` containing the monomial `a*x`, and a disequality constraint `c₂`
+containing the monomial `b*x`, eliminate `x` by applying substitution.
+-/
+def DiseqCnstr.applyEq? (a : Int) (x : Var) (c₁ : EqCnstr) (b : Int) (c₂ : DiseqCnstr) : LinearM (Option DiseqCnstr) := do
+  trace[grind.linarith.subst] "{← getVar x}, {← c₁.denoteExpr}, {← c₂.denoteExpr}"
+  let p := c₁.p
+  let q := c₂.p
+  if b % a == 0 then
+    let k := - b / a
+    let p := p.mul k |>.combine q
+    return some { p, h := .subst1 k c₁ c₂ }
+  else if (← hasNoNatZeroDivisors) then
+    let p := p.mul b |>.combine (q.mul (-a))
+    return some { p, h := .subst (-a) b c₁ c₂ }
+  else
+    return none
+
 /-- Returns `some structId` if `a` and `b` are elements of the same structure. -/
 def inSameStruct? (a b : Expr) : GoalM (Option Nat) := do
   let some structId ← getTermStructId? a | return none
@@ -22,7 +48,7 @@ def inSameStruct? (a b : Expr) : GoalM (Option Nat) := do
   unless structId == structId' do return none -- This can happen when we have heterogeneous equalities
   return structId
 
-private def processNewCommRingEq (a b : Expr) : LinearM Unit := do
+private def processNewCommRingEq' (a b : Expr) : LinearM Unit := do
   let some lhs ← withRingM <| CommRing.reify? a (skipVar := false) | return ()
   let some rhs ← withRingM <| CommRing.reify? b (skipVar := false) | return ()
   let gen := max (← getGeneration a) (← getGeneration b)
@@ -40,7 +66,7 @@ private def processNewCommRingEq (a b : Expr) : LinearM Unit := do
   let c₂ : IneqCnstr := { p, strict := false, h := .ofCommRingEq b a rhs lhs p' lhs' }
   c₂.assert
 
-private def processNewIntModuleEq (a b : Expr) : LinearM Unit := do
+private def processNewIntModuleEq' (a b : Expr) : LinearM Unit := do
   let some lhs ← reify? a (skipVar := false) | return ()
   let some rhs ← reify? b (skipVar := false) | return ()
   let p := (lhs.sub rhs).norm
@@ -51,31 +77,165 @@ private def processNewIntModuleEq (a b : Expr) : LinearM Unit := do
   let c₂ : IneqCnstr := { p, strict := false, h := .ofEq b a rhs lhs }
   c₂.assert
 
-@[export lean_process_linarith_eq]
-def processNewEqImpl (a b : Expr) : GoalM Unit := do
-  if isSameExpr a b then return () -- TODO: check why this is needed
-  let some structId ← inSameStruct? a b | return ()
-  LinearM.run structId do
-    -- TODO: support non ordered case
-    unless (← isOrdered) do return ()
-    trace_goal[grind.linarith.assert] "{← mkEq a b}"
-    if (← isCommRing) then
-      processNewCommRingEq a b
-    else
-      processNewIntModuleEq a b
+def EqCnstr.norm (c : EqCnstr) : LinearM (Nat × Var × EqCnstr) := do
+  let mut c := c
+  if (← hasNoNatZeroDivisors) then
+    let k := c.p.gcdCoeffs
+    if k != 1 then
+      c := { p := c.p.div k, h := .coeff k c }
+  let some (k, x) := c.p.pickVarToElim? | unreachable!
+  if k < 0 then
+    c := { p := c.p.mul (-1), h := .neg c }
+  return (k.natAbs, x, c)
+
+partial def EqCnstr.applySubsts (c : EqCnstr) : LinearM EqCnstr := withIncRecDepth do
+  let some (x, c₁, p) ← c.p.substVar | return c
+  trace[grind.debug.linarith.subst] "{← getVar x}, {← c.denoteExpr}, {← c₁.denoteExpr}"
+  applySubsts { p, h := .subst x c₁ c : EqCnstr }
+
+/--
+Given an equation `c₁` containing the monomial `a*x`, and an inequality constraint `c₂`
+containing the monomial `b*x`, eliminate `x` by applying substitution.
+-/
+def IneqCnstr.applyEq (a : Nat) (x : Var) (c₁ : EqCnstr) (b : Int) (c₂ : IneqCnstr) : LinearM IneqCnstr := do
+  let p := c₁.p
+  let q := c₂.p
+  let p := q.mul a |>.combine (p.mul (-b))
+  trace[grind.linarith.subst] "{← getVar x}, {← c₁.denoteExpr}, {← c₂.denoteExpr}"
+  return { p, h := .subst x c₁ c₂, strict := c₂.strict }
+
+/--
+Given an equation `c₁` containing `a*x`, eliminate `x` from the inequalities in `todo`.
+`todo` contains pairs of the form `(b, c₂)` where `b` is the coefficient of `x` in `c₂`.
+-/
+private def updateLeCnstrs (a : Nat) (x : Var) (c₁ : EqCnstr) (todo : Array (Int × IneqCnstr)) : LinearM Unit := do
+  for (b, c₂) in todo do
+    let c₂ ← c₂.applyEq a x c₁ b
+    c₂.assert
+    if (← inconsistent) then return ()
+
+private def splitIneqCnstrs (x : Var) (cs : PArray IneqCnstr) : PArray IneqCnstr × Array (Int × IneqCnstr) :=
+  split cs fun c => c.p.coeff x
+
+/--
+Given an equation `c₁` containing `a*x`, eliminate `x` from lower bound inequalities of `y`.
+-/
+private def updateLowers (a : Nat) (x : Var) (c : EqCnstr) (y : Var) : LinearM Unit := do
+  if (← inconsistent) then return ()
+  let (lowers', todo) := splitIneqCnstrs x (← getStruct).lowers[y]!
+  modifyStruct fun s => { s with lowers := s.lowers.set y lowers' }
+  updateLeCnstrs a x c todo
+
+/--
+Given an equation `c₁` containing `a*x`, eliminate `x` from upper bound inequalities of `y`.
+-/
+private def updateUppers (a : Nat) (x : Var) (c : EqCnstr) (y : Var) : LinearM Unit := do
+  if (← inconsistent) then return ()
+  let (uppers', todo) := splitIneqCnstrs x (← getStruct).uppers[y]!
+  modifyStruct fun s => { s with uppers := s.uppers.set y uppers' }
+  updateLeCnstrs a x c todo
+
+def DiseqCnstr.ignore (c : DiseqCnstr) : LinearM Unit := do
+  -- Remark: we filter duplicates before displaying diagnostics to users
+  trace[grind.linarith.assert.ignored] "{← c.denoteExpr}"
+  let diseq ← c.denoteExpr
+  modifyStruct fun s => { s with ignored := s.ignored.push diseq }
+
+partial def DiseqCnstr.applySubsts? (c₂ : DiseqCnstr) : LinearM (Option DiseqCnstr) := withIncRecDepth do
+  let some (b, x, c₁) ← c₂.p.findVarToSubst | return some c₂
+  let a := c₁.p.coeff x
+  if let some c₂ ← c₂.applyEq? a x c₁ b then
+    c₂.applySubsts?
+  else
+    -- Failed to eliminate
+    c₂.ignore
+    return none
 
 def DiseqCnstr.assert (c : DiseqCnstr) : LinearM Unit := do
   trace[grind.linarith.assert] "{← c.denoteExpr}"
+  let some c ← c.applySubsts? | return ()
   match c.p with
   | .nil =>
     trace[grind.linarith.unsat] "{← c.denoteExpr}"
     setInconsistent (.diseq c)
   | .add _ x _ =>
     trace[grind.linarith.assert.store] "{← c.denoteExpr}"
+    c.p.updateOccs
     modifyStruct fun s => { s with diseqs := s.diseqs.modify x (·.push c) }
     if (← c.satisfied) == .false then
       resetAssignmentFrom x
 
+private def splitDiseqs (x : Var) (cs : PArray DiseqCnstr) : PArray DiseqCnstr × Array (Int × DiseqCnstr) :=
+  split cs fun c => c.p.coeff x
+
+private def updateDiseqs (a : Int) (x : Var) (c : EqCnstr) (y : Var) : LinearM Unit := do
+  if (← inconsistent) then return ()
+  let (diseqs', todo) := splitDiseqs x (← getStruct).diseqs[y]!
+  modifyStruct fun s => { s with diseqs := s.diseqs.set y diseqs' }
+  for (b, c₂) in todo do
+    if let some c₂ ← c₂.applyEq? a x c b then
+      c₂.assert
+      if (← inconsistent) then return ()
+    else
+      -- Failed to eliminate
+      c₂.ignore
+
+private def updateOccsAt (a : Nat) (x : Var) (c : EqCnstr) (y : Var) : LinearM Unit := do
+  updateLowers a x c y
+  updateUppers a x c y
+  updateDiseqs a x c y
+
+private def updateOccs (a : Nat) (x : Var) (c : EqCnstr) : LinearM Unit := do
+  let ys := (← getStruct).occurs[x]!
+  modifyStruct fun s => { s with occurs := s.occurs.set x {} }
+  updateOccsAt a x c x
+  for y in ys do
+    updateOccsAt a x c y
+
+def EqCnstr.assert (c : EqCnstr) : LinearM Unit := do
+  trace[grind.linarith.assert] "{← c.denoteExpr}"
+  let c ← c.applySubsts
+  if c.p == .nil then
+    trace[grind.linarith.trivial] "{← c.denoteExpr}"
+    return ()
+  let (a, x, c) ← c.norm
+  trace[grind.debug.linarith.subst] ">> {← getVar x}, {← c.denoteExpr}"
+  trace[grind.linarith.assert.store] "{← c.denoteExpr}"
+  modifyStruct fun s => { s with
+    elimEqs := s.elimEqs.set x (some c)
+    elimStack := x :: s.elimStack
+  }
+  updateOccs a x c
+
+private def processNewCommRingEq (a b : Expr) : LinearM Unit := do
+  trace[Meta.debug] "{a}, {b}"
+  -- TODO
+
+private def processNewIntModuleEq (a b : Expr) : LinearM Unit := do
+  let some lhs ← reify? a (skipVar := false) | return ()
+  let some rhs ← reify? b (skipVar := false) | return ()
+  let p := (lhs.sub rhs).norm
+  if p == .nil then return ()
+  let c : EqCnstr := { p, h := .core a b lhs rhs }
+  c.assert
+
+@[export lean_process_linarith_eq]
+def processNewEqImpl (a b : Expr) : GoalM Unit := do
+  if isSameExpr a b then return () -- TODO: check why this is needed
+  let some structId ← inSameStruct? a b | return ()
+  LinearM.run structId do
+    if (← isOrdered) then
+      trace_goal[grind.linarith.assert] "{← mkEq a b}"
+      if (← isCommRing) then
+        processNewCommRingEq' a b
+      else
+        processNewIntModuleEq' a b
+    else
+      if (← isCommRing) then
+        processNewCommRingEq a b
+      else
+        processNewIntModuleEq a b
+
 private def processNewCommRingDiseq (a b : Expr) : LinearM Unit := do
   let some lhs ← withRingM <| CommRing.reify? a (skipVar := false) | return ()
   let some rhs ← withRingM <| CommRing.reify? b (skipVar := false) | return ()

src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean

@@ -38,6 +38,23 @@ private def ensureDefEq (a b : Expr) : MetaM Unit := do
   unless (← withDefault <| isDefEq a b) do
     throwError (← mkExpectedDefEqMsg a b)
 
+private def addZeroLtOne (one : Var) : LinearM Unit := do
+  let p := Poly.add (-1) one .nil
+  modifyStruct fun s => { s with
+    lowers := s.lowers.modify one fun cs => cs.push { p, h := .oneGtZero, strict := true }
+  }
+
+private def addZeroNeOne (one : Var) : LinearM Unit := do
+  let p := Poly.add 1 one .nil
+  modifyStruct fun s => { s with
+    diseqs := s.diseqs.modify one fun cs => cs.push { p, h := .oneNeZero }
+  }
+
+private def isNonTrivialIsCharInst (isCharInst? : Option (Expr × Nat)) : Bool :=
+  match isCharInst? with
+  | some (_, c) => c != 1
+  | none => false
+
 def getStructId? (type : Expr) : GoalM (Option Nat) := do
   unless (← getConfig).linarith do return none
   if (← getConfig).cutsat && Cutsat.isSupportedType type then
@@ -144,6 +161,7 @@ where
     let hsmulNatFn? ← getHSMulNatFn?
     let ringId? ← CommRing.getRingId? type
     let ringInst? ← getInst? ``Grind.Ring
+    let fieldInst? ← getInst? ``Grind.Field
     let getOne? : GoalM (Option Expr) := do
       let some oneInst ← getInst? ``One | return none
       let one ← internalizeConst <| mkApp2 (mkConst ``One.one [u]) type oneInst
@@ -161,6 +179,7 @@ where
           return none
       return some inst
     let ringIsOrdInst? ← getRingIsOrdInst?
+    let charInst? ← if let some ringInst := ringInst? then getIsCharInst? u type ringInst else pure none
     let getNoNatZeroDivInst? : GoalM (Option Expr) := do
       let hmulNat := mkApp3 (mkConst ``HMul [0, u, u]) Nat.mkType type type
       let .some hmulInst ← trySynthInstance hmulNat | return none
@@ -171,17 +190,21 @@ where
     let struct : Struct := {
       id, type, u, intModuleInst, preorderInst?, isOrdInst?, partialInst?, linearInst?, noNatDivInst?
       leFn?, ltFn?, addFn, subFn, negFn, hmulFn, hmulNatFn, hsmulFn?, hsmulNatFn?, zero, one?
-      ringInst?, commRingInst?, ringIsOrdInst?, ringId?, ofNatZero
+      ringInst?, commRingInst?, ringIsOrdInst?, charInst?, ringId?, fieldInst?, ofNatZero
     }
     modify' fun s => { s with structs := s.structs.push struct }
     if let some one := one? then
       if ringInst?.isSome then LinearM.run id do
-        -- Create `1` variable, and assert strict lower bound `0 < 1`
-        let x ← mkVar one (mark := false)
-        let p := Poly.add (-1) x .nil
-        modifyStruct fun s => { s with
-          lowers := s.lowers.modify x fun cs => cs.push { p, h := .oneGtZero, strict := true }
-        }
+        if ringIsOrdInst?.isSome then
+          -- Create `1` variable, and assert strict lower bound `0 < 1` and `0 ≠ 1`
+          let x ← mkVar one (mark := false)
+          addZeroLtOne x
+          addZeroNeOne x
+        else if fieldInst?.isSome || isNonTrivialIsCharInst charInst? then
+          -- Create `1` variable, and assert `0 ≠ 1`
+          let x ← mkVar one (mark := false)
+          addZeroNeOne x
+
     return some id
 
 end Lean.Meta.Grind.Arith.Linear

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

@@ -19,6 +19,18 @@ deriving instance Hashable for Poly
 deriving instance Hashable for Grind.Linarith.Expr
 
 mutual
+/-- An equality constraint and its justification/proof. -/
+structure EqCnstr where
+  p      : Poly
+  h      : EqCnstrProof
+
+inductive EqCnstrProof where
+  | core (a b : Expr) (lhs rhs : LinExpr)
+  | coreCommRing (a b : Expr) (ra rb : Grind.CommRing.Expr) (p : Grind.CommRing.Poly) (lhs' : LinExpr)
+  | neg (c : EqCnstr)
+  | coeff (k : Nat) (c : EqCnstr)
+  | subst (x : Var) (c₁ : EqCnstr) (c₂ : EqCnstr)
+
 /-- An inequality constraint and its justification/proof. -/
 structure IneqCnstr where
   p      : Poly
@@ -39,6 +51,7 @@ inductive IneqCnstrProof where
     ofEq (a b : Expr) (la lb : LinExpr)
   | /-- `a ≤ b` from an equality `a = b` coming from the core. -/
     ofCommRingEq (a b : Expr) (ra rb : Grind.CommRing.Expr) (p : Grind.CommRing.Poly) (lhs' : LinExpr)
+  | subst (x : Var) (c₁ : EqCnstr) (c₂ : IneqCnstr)
 
 structure DiseqCnstr where
   p  : Poly
@@ -48,6 +61,9 @@ inductive DiseqCnstrProof where
   | core (a b : Expr) (lhs rhs : LinExpr)
   | coreCommRing (a b : Expr) (ra rb : Grind.CommRing.Expr) (p : Grind.CommRing.Poly) (lhs' : LinExpr)
   | neg (c : DiseqCnstr)
+  | subst (k₁ k₂ : Int) (c₁ : EqCnstr) (c₂ : DiseqCnstr)
+  | subst1 (k : Int) (c₁ : EqCnstr) (c₂ : DiseqCnstr)
+  | oneNeZero
 
 inductive UnsatProof where
   | diseq (c : DiseqCnstr)
@@ -58,6 +74,11 @@ end
 instance : Inhabited DiseqCnstr where
   default := { p := .nil, h := .core default default .zero .zero }
 
+instance : Inhabited EqCnstr where
+  default := { p := .nil, h := .core default default .zero .zero }
+
+abbrev VarSet := RBTree Var compare
+
 /--
 State for each algebraic structure by this module.
 Each type must at least implement the instance `IntModule`.
@@ -88,6 +109,10 @@ structure Struct where
   commRingInst?    : Option Expr
   /-- `Ring.IsOrdered` instance with `Preorder` -/
   ringIsOrdInst?   : Option Expr
+  /-- `Field` instance -/
+  fieldInst?       : Option Expr
+  /-- `IsCharP` instance for `type` if available. -/
+  charInst?        : Option (Expr × Nat)
   zero             : Expr
   ofNatZero        : Expr
   one?             : Option Expr
@@ -142,6 +167,24 @@ structure Struct where
   -/
   diseqSplits : PHashMap Poly FVarId := {}
   /--
+  Mapping from variable to equation constraint used to eliminate it. `solved` variables should not occur in
+  `diseqs`, `lowers`, or `uppers`.
+  -/
+  elimEqs : PArray (Option EqCnstr) := {}
+  /--
+  Elimination stack. For every variable in `elimStack`. If `x` in `elimStack`, then `elimEqs[x]` is not `none`.
+  -/
+  elimStack : List Var := []
+  /--
+  Mapping from variable to occurrences.
+  For example, an entry `x ↦ {y, z}` means that `x` may occur in `lowers`, or `uppers`, or `diseqs` of
+  variables `y` and `z`.
+  If `x` occurs in `diseqs[y]`, `lowers[y]`, or `uppers[y]`, then `y` is in `occurs[x]`,
+  but the reverse is not true.
+  If `x` is in `elimStack`, then `occurs[x]` is the empty set.
+  -/
+  occurs : PArray VarSet := {}
+  /--
   Linear constraints that are not supported.
   We use this information for diagnostics.
   TODO: store constraints instead.

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

@@ -110,6 +110,11 @@ def setTermStructId (e : Expr) : LinearM Unit := do
     return ()
   modify' fun s => { s with exprToStructId := s.exprToStructId.insert { expr := e } structId }
 
+def getNoNatDivInst : LinearM Expr := do
+  let some inst := (← getStruct).noNatDivInst?
+    | throwError "`grind linarith` internal error, structure does not implement `NoNatZeroDivisors`"
+  return inst
+
 def getPreorderInst : LinearM Expr := do
   let some inst := (← getStruct).preorderInst?
     | throwError "`grind linarith` internal error, structure is not a preorder"
@@ -189,4 +194,78 @@ def resetAssignmentFrom (x : Var) : LinearM Unit := do
 def getVar (x : Var) : LinearM Expr :=
   return (← getStruct).vars[x]!
 
+/-- Returns `true` if the linarith state is inconsistent. -/
+def inconsistent : LinearM Bool := do
+  if (← isInconsistent) then return true
+  return (← getStruct).conflict?.isSome
+
+/-- Returns `true` if `x` has been eliminated using an equality constraint. -/
+def eliminated (x : Var) : LinearM Bool :=
+  return (← getStruct).elimEqs[x]!.isSome
+
+/-- Returns occurrences of `x`. -/
+def getOccursOf (x : Var) : LinearM VarSet :=
+  return (← getStruct).occurs[x]!
+
+/--
+Adds `y` as an occurrence of `x`.
+That is, `x` occurs in `lowers[y]`, `uppers[y]`, or `diseqs[y]`.
+-/
+def addOcc (x : Var) (y : Var) : LinearM Unit := do
+  unless (← getOccursOf x).contains y do
+    modifyStruct fun s => { s with occurs := s.occurs.modify x fun ys => ys.insert y }
+
+/--
+Given `p` a polynomial being inserted into `lowers`, `uppers`, or `diseqs`,
+get its leading variable `y`, and adds `y` as an occurrence for the remaining variables in `p`.
+-/
+partial def _root_.Lean.Grind.Linarith.Poly.updateOccs (p : Poly) : LinearM Unit := do
+  let .add _ y p := p | throwError "`grind linarith` internal error, unexpected constant polynomial"
+  let rec go (p : Poly) : LinearM Unit := do
+    let .add _ x p := p | return ()
+    addOcc x y; go p
+  go p
+
+/--
+Given a polynomial `p`, returns `some (x, k, c)` if `p` contains the monomial `k*x`,
+and `x` has been eliminated using the equality `c`.
+-/
+def _root_.Lean.Grind.Linarith.Poly.findVarToSubst (p : Poly) : LinearM (Option (Int × Var × EqCnstr)) := do
+  match p with
+  | .nil => return none
+  | .add k x p =>
+    if let some c := (← getStruct).elimEqs[x]! then
+      return some (k, x, c)
+    else
+      findVarToSubst p
+
+def _root_.Lean.Grind.Linarith.Poly.gcdCoeffsAux : Poly → Nat → Nat
+  | .nil, k => k
+  | .add k' _ p, k => gcdCoeffsAux p (Int.gcd k' k)
+
+def _root_.Lean.Grind.Linarith.Poly.gcdCoeffs (p : Poly) : Nat :=
+  match p with
+  | .add k _ p => p.gcdCoeffsAux k.natAbs
+  | .nil => 1
+
+def _root_.Lean.Grind.Linarith.Poly.div (p : Poly) (k : Int) : Poly :=
+  match p with
+  | .add a x p => .add (a / k) x (p.div k)
+  | .nil => .nil
+
+/--
+Selects the variable in the given linear polynomial whose coefficient has the smallest absolute value.
+-/
+def _root_.Lean.Grind.Linarith.Poly.pickVarToElim? (p : Poly) : Option (Int × Var) :=
+  match p with
+  | .nil => none
+  | .add k x p => go k x p
+where
+  go (k : Int) (x : Var) (p : Poly) : Int × Var :=
+    if k == 1 || k == -1 then
+      (k, x)
+    else match p with
+      | .nil => (k, x)
+      | .add k' x' p => if k'.natAbs < k.natAbs then go k' x' p else go k x p
+
 end Lean.Meta.Grind.Arith.Linear

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

@@ -19,6 +19,8 @@ def mkVar (e : Expr) (mark := true) : LinearM Var := do
     lowers     := s.lowers.push {}
     uppers     := s.uppers.push {}
     diseqs     := s.diseqs.push {}
+    occurs     := s.occurs.push {}
+    elimEqs    := s.elimEqs.push none
   }
   setTermStructId e
   if mark then

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

@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Expr
-import Lean.Message
+import Init.Grind.CommRing.Basic
+import Lean.Meta.SynthInstance
+import Lean.Meta.Basic
 import Std.Internal.Rat
 
 namespace Lean.Meta.Grind.Arith
@@ -151,4 +152,32 @@ def isIntModuleVirtualParent (parent? : Option Expr) : Bool :=
   | none => false
   | some parent => parent == getIntModuleVirtualParent
 
+def getIsCharInst? (u : Level) (type : Expr) (ringInst : Expr) : MetaM (Option (Expr × Nat)) := do withNewMCtxDepth do
+  let n ← mkFreshExprMVar (mkConst ``Nat)
+  let charType := mkApp3 (mkConst ``Grind.IsCharP [u]) type ringInst n
+  let .some charInst ← trySynthInstance charType | pure none
+  let n ← instantiateMVars n
+  let some n ← evalNat n |>.run
+    | pure none
+  pure <| some (charInst, n)
+
+def getNoZeroDivInst? (u : Level) (type : Expr) : MetaM (Option Expr) := do
+  let zeroType := mkApp (mkConst ``Zero [u]) type
+  let .some zeroInst ← trySynthInstance zeroType | return none
+  let hmulType := mkApp3 (mkConst ``HMul [0, u, u]) (mkConst ``Nat []) type type
+  let .some hmulInst ← trySynthInstance hmulType | return none
+  let noZeroDivType := mkApp3 (mkConst ``Grind.NoNatZeroDivisors [u]) type zeroInst hmulInst
+  LOption.toOption <$> trySynthInstance noZeroDivType
+
+@[specialize] def split (cs : PArray α) (getCoeff : α → Int) : PArray α × Array (Int × α) := Id.run do
+  let mut cs' := {}
+  let mut todo := #[]
+  for c in cs do
+    let b := getCoeff c
+    if b == 0 then
+      cs' := cs'.push c
+    else
+      todo := todo.push (b, c)
+  return (cs', todo)
+
 end Lean.Meta.Grind.Arith

src/Lean/Meta/Tactic/LibrarySearch.lean

@@ -71,12 +71,14 @@ open LazyDiscrTree (InitEntry findMatches)
 
 private def addImport (name : Name) (constInfo : ConstantInfo) :
     MetaM (Array (InitEntry (Name × DeclMod))) :=
+  -- Don't report lemmas from metaprogramming namespaces.
+  if name.isMetaprogramming then return #[] else
   forallTelescope constInfo.type fun _ type => do
     let e ← InitEntry.fromExpr type (name, DeclMod.none)
     let a := #[e]
     if e.key == .const ``Iff 2 then
-      let a := a.push (←e.mkSubEntry 0 (name, DeclMod.mp))
-      let a := a.push (←e.mkSubEntry 1 (name, DeclMod.mpr))
+      let a := a.push (← e.mkSubEntry 0 (name, DeclMod.mp))
+      let a := a.push (← e.mkSubEntry 1 (name, DeclMod.mpr))
       pure a
     else
       pure a

src/Lean/Meta/Tactic/Rewrites.lean

@@ -44,11 +44,11 @@ private def addImport (name : Name) (constInfo : ConstantInfo) :
   if constInfo.isUnsafe then return #[]
   if !allowCompletion (←getEnv) name then return #[]
   -- We now remove some injectivity lemmas which are not useful to rewrite by.
-  if name matches .str _ "injEq" then return #[]
-  if name matches .str _ "sizeOf_spec" then return #[]
   match name with
-  | .str _ n => if n.endsWith "_inj" ∨ n.endsWith "_inj'" then return #[]
+  | .str _ n => if n = "injEq" ∨ n = "sizeOf_spec" ∨ n.endsWith "_inj" ∨ n.endsWith "_inj'" then return #[]
   | _ => pure ()
+  -- Don't report lemmas from metaprogramming namespaces.
+  if name.isMetaprogramming then return #[]
   withNewMCtxDepth do withReducible do
     forallTelescopeReducing constInfo.type fun _ type => do
       match type.getAppFnArgs with

src/Lean/Meta/Tactic/Rfl.lean

@@ -35,8 +35,8 @@ A reflexivity lemma should have the conclusion `r x x` where `r` is an arbitrary
 It is not possible to tag reflexivity lemmas for `=` using this attribute. These are handled as a
 special case in the `rfl` tactic.
 -/
-@[builtin_init, builtin_doc]
-private def initFn := registerBuiltinAttribute {
+@[builtin_doc]
+builtin_initialize registerBuiltinAttribute {
   name := `refl
   descr := "reflexivity relation"
   add := fun decl _ kind => MetaM.run' do

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

@@ -136,8 +136,8 @@ theorem Option.pbind_congr
   ...
 ```
 -/
-@[builtin_init, builtin_doc]
-private def init :=
+@[builtin_doc]
+builtin_initialize
   registerBuiltinAttribute {
     name  := `congr
     descr := "congruence theorem"

src/Lean/Meta/Tactic/Symm.lean

@@ -31,8 +31,8 @@ Tags symmetry lemmas to be used by the `symm` tactic.
 
 A symmetry lemma should be of the form `r x y → r y x` where `r` is an arbitrary relation.
 -/
-@[builtin_init, builtin_doc]
-private def initFn := registerBuiltinAttribute {
+@[builtin_doc]
+builtin_initialize registerBuiltinAttribute {
   name := `symm
   descr := "symmetric relation"
   add := fun decl _ kind => MetaM.run' do

src/Std/Data/ExtDHashMap/Lemmas.lean

@@ -51,15 +51,10 @@ theorem not_insert_eq_empty [EquivBEq α] [LawfulHashable α] {k : α} {v : β k
 theorem mem_iff_contains [EquivBEq α] [LawfulHashable α] {a : α} : a ∈ m ↔ m.contains a :=
   Iff.rfl
 
-@[simp, grind =]
+@[simp, grind _=_]
 theorem contains_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} : m.contains a ↔ a ∈ m :=
   Iff.rfl
 
--- We need to specify the pattern for the reverse direction manually,
--- as the default heuristic leaves the `ExtDHashMap α β` argument as a wildcard.
-grind_pattern contains_iff_mem => @Membership.mem α (ExtDHashMap α β) _ m a
-
-
 theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : m.contains a = m.contains b :=
   m.inductionOn fun _ => DHashMap.contains_congr hab
 

tests/lean/grind/algebra/ordered_modules.lean

@@ -23,40 +23,15 @@ example (a b c : R) (_ : a < b) (_ : b < c) : a < c := by grind
 example (a : R) (h : 2 * a < 0) : a < 0 := by grind
 example (a : R) (h : 2 * a < 0) : 0 ≤ -a := by grind
 
-example (a b : R) (_ : a < b) (_ : b < a) : False := by grind
-example (a b : R) (_ : a < b ∧ b < a) : False := by grind
-example (a b : R) (_ : a < b) : a ≠ b := by grind
-
 example (a b c e v0 v1 : R) (h1 : v0 = 5 * a) (h2 : v1 = 3 * b) (h3 : v0 + v1 + c = 10 * e) :
     v0 + 5 * e + (v1 - 3 * e) + (c - 2 * e) = 10 * e := by
   grind
 
-example (x y z : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : 12 * y - 4 * z < 0) : False := by
-  grind
-example (x y z : R) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : 12 * y - 4 * z < 0) : False := by
-  grind
-
-example (x y z : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : x * y < 5) (h3 : 12 * y - 4 * z < 0) :
-    False := by grind
-example (x y z : R) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : 12 * y - 4 * z < 0) :
-    False := by grind
-
-example (x y z : Int) (hx : x ≤ 3 * y) (h2 : y ≤ 2 * z) (h3 : x ≥ 6 * z) : x = 3*y := by
-  grind
 example (x y z : R) (hx : x ≤ 3 * y) (h2 : y ≤ 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
   grind
 
-example (x y z : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : x * y < 5) : ¬ 12*y - 4* z < 0 := by
-  grind
-example (x y z : R) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) : ¬ 12 * y - 4 * z < 0 := by
-  grind
-
-example (x y z : Int) (hx : ¬ x > 3 * y) (h2 : ¬ y > 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
-  grind
 example (x y z : R) (hx : ¬ x > 3 * y) (h2 : ¬ y > 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
   grind
 
-example (x y z : Nat) (hx : x ≤ 3 * y) (h2 : y ≤ 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
-  grind
 example (x y z : R) (hx : x ≤ 3 * y) (h2 : y ≤ 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
   grind

tests/lean/grind/dhashmap_pattern.lean

@@ -1,43 +0,0 @@
-import Std.Data.HashMap
-import Std.Data.TreeMap
-
-open Std
-
-/--
-info: Std.DTreeMap.contains_iff_mem.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp}
-  {k : α} : t.contains k = true ↔ k ∈ t
--/
-#guard_msgs in
-#check DTreeMap.contains_iff_mem
-
--- I like what `[grind _=_]` does here!
-/--
-info: DTreeMap.contains_iff_mem: [@DTreeMap.contains #4 #3 #2 #1 #0, true]
----
-info: DTreeMap.contains_iff_mem: [@Membership.mem #4 (@DTreeMap _ #3 #2) _ #1 #0]
--/
-#guard_msgs in
-attribute [grind? _=_] DTreeMap.contains_iff_mem
-
--- Similarly for every other `contains_iff_mem` we encounter (`List`, `Array`, `Vector`, `HashSet`, `HashMap`, etc.)
-
--- But:
-
-/--
-info: Std.DHashMap.contains_iff_mem.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α β}
-  {a : α} : m.contains a = true ↔ a ∈ m
--/
-#guard_msgs in
-#check DHashMap.contains_iff_mem
-
--- Here the reverse direction of `[grind _=_]` gives a pattern than matches too often: `@Membership.mem #5 _ _ #1 #0`.
-/--
-info: DHashMap.contains_iff_mem: [@DHashMap.contains #5 #4 #3 #2 #1 #0, true]
----
-info: DHashMap.contains_iff_mem: [@Membership.mem #5 _ _ #1 #0]
--/
-#guard_msgs in
-attribute [grind? _=_] DHashMap.contains_iff_mem
-
--- We can do this manually with
-grind_pattern DHashMap.contains_iff_mem => @Membership.mem α (DHashMap α β) _ m a

tests/lean/grind/experiments/list_count.lean

@@ -2,18 +2,8 @@
 
 open List
 
-
 variable [BEq α] [LawfulBEq α]
 
-theorem filter_beq {l : List α} (a : α) : l.filter (· == a) = replicate (count a l) a := by
-  ext
-  grind
-
-theorem count_flatten {a : α} {l : List (List α)} : count a l.flatten = (l.map (count a)).sum := by
-  grind (ematch := 10) (gen := 10) -- fails
-
-theorem count_concat_self {a : α} {l : List α} : count a (concat l a) = count a l + 1 := by grind [concat_eq_append] -- fails?!
-
 theorem count_eq_length {l : List α} : count a l = l.length ↔ ∀ b ∈ l, a = b := by
   induction l with grind
 
@@ -27,7 +17,3 @@ theorem replicate_count_eq_of_count_eq_length {l : List α} (h : count a l = len
 theorem count_filterMap {α} [BEq β] {b : β} {f : α → Option β} {l : List α} :
     count b (filterMap f l) = countP (fun a => f a == some b) l := by
   grind
-
-theorem count_flatMap {α} [BEq β] {l : List α} {f : α → List β} {x : β} :
-    count x (l.flatMap f) = sum (map (count x ∘ f) l) := by
-  grind

tests/lean/grind/experiments/map.lean

@@ -4,7 +4,8 @@ import Std.Data.ExtHashMap
 open Std
 
 -- Do we want this?
-example (m : HashMap Nat Nat) (h : m.isEmpty) : m[3]? = none := by grind [HashMap.getElem?_of_isEmpty]
+grind_pattern HashMap.getElem?_of_isEmpty => m.isEmpty, m[a]?
+example (m : HashMap Nat Nat) (h : m.isEmpty) : m[3]? = none := by grind
 
 -- Do this for List etc?
 -- attribute [grind] HashMap.getElem?_eq_some_getElem -- Do we do this for list?

tests/lean/librarySearch.lean

@@ -276,6 +276,12 @@ error: apply? didn't find any relevant lemmas
 #guard_msgs in
 example {α : Sort u} (x y : α) : Eq x y := by apply?
 
+-- If this lemma is added later to the library, please update this `#guard_msgs`.
+-- The point of this test is to ensure that `Lean.Grind.not_eq_prop` is not reported to users.
+/-- error: `exact?` could not close the goal. Try `apply?` to see partial suggestions. -/
+#guard_msgs in
+example (p q : Prop) : (¬ p = q) = (p = ¬ q) := by exact?
+
 -- Verify that there is a `sorry` warning when `apply?` closes the goal.
 #guard_msgs (drop info) in
 example : False := by apply?

tests/lean/librarySearch.lean.expected.out

@@ -1 +1 @@
-librarySearch.lean:281:0-281:7: warning: declaration uses 'sorry'
+librarySearch.lean:287:0-287:7: warning: declaration uses 'sorry'

tests/lean/run/grind_field_div.lean

@@ -1,4 +1,5 @@
 open Lean Grind
+set_option grind.debug true
 
 example [Field α] [IsCharP α 0] (a b c : α) : a/3 = b → c = a/3 → a/2 + a/2 = b + 2*c  := by
   grind

tests/lean/run/grind_field_norm.lean

@@ -1,4 +1,5 @@
 open Lean.Grind
+set_option grind.debug true
 
 variable (R : Type u) [Field R]
 

tests/lean/run/grind_indexmap.lean

@@ -49,6 +49,15 @@ instance {m : IndexMap α β} {a : α} : Decidable (a ∈ m) :=
 @[local grind] private theorem mem_indices_of_mem {m : IndexMap α β} {a : α} :
     a ∈ m ↔ a ∈ m.indices := Iff.rfl
 
+@[inline] def findIdx? (m : IndexMap α β) (a : α) : Option Nat := m.indices[a]?
+
+@[inline] def findIdx (m : IndexMap α β) (a : α) (h : a ∈ m := by get_elem_tactic) : Nat := m.indices[a]
+
+@[inline] def getIdx? (m : IndexMap α β) (i : Nat) : Option β := m.values[i]?
+
+@[inline] def getIdx (m : IndexMap α β) (i : Nat) (h : i < m.size := by get_elem_tactic) : β :=
+  m.values[i]
+
 variable [LawfulBEq α] [LawfulHashable α]
 
 attribute [local grind _=_] IndexMap.WF
@@ -70,25 +79,7 @@ instance : GetElem? (IndexMap α β) α β (fun m a => a ∈ m) where
 @[local grind] private theorem getElem?_def (m : IndexMap α β) (a : α) :
     m[a]? = m.indices[a]?.bind (fun i => (m.values[i]?)) := rfl
 @[local grind] private theorem getElem!_def [Inhabited β] (m : IndexMap α β) (a : α) :
-    m[a]! = (m.indices[a]?.bind (fun i => (m.values[i]?)) |>.getD default) := rfl
-
-@[local grind] private theorem WF' (i : Nat) (a : α) (h₁ : i < m.keys.size) (h₂ : a ∈ m) :
-    m.keys[i] = a ↔ m.indices[a] = i := by
-  have := m.WF i a
-  grind
-
-@[local grind] private theorem getElem_keys_getElem_indices
-    {m : IndexMap α β} {a : α} {h : a ∈ m} :
-  m.keys[m.indices[a]'h] = a := by grind
-
-@[inline] def findIdx? (m : IndexMap α β) (a : α) : Option Nat := m.indices[a]?
-
-@[inline] def findIdx (m : IndexMap α β) (a : α) (h : a ∈ m) : Nat := m.indices[a]
-
-@[inline] def getIdx? (m : IndexMap α β) (i : Nat) : Option β := m.values[i]?
-
-@[inline] def getIdx (m : IndexMap α β) (i : Nat) (h : i < m.size := by get_elem_tactic) : β :=
-  m.values[i]
+    m[a]! = (m.indices[a]?.bind (fun i => (m.values[i]?))).getD default := rfl
 
 instance : LawfulGetElem (IndexMap α β) α β (fun m a => a ∈ m) where
   getElem?_def := by grind
@@ -115,6 +106,11 @@ instance [LawfulBEq α] : Insert (α × β) (IndexMap α β) :=
 instance [LawfulBEq α] : LawfulSingleton (α × β) (IndexMap α β) :=
     ⟨fun _ => rfl⟩
 
+@[local grind] private theorem WF' (i : Nat) (a : α) (h₁ : i < m.keys.size) (h₂ : a ∈ m) :
+    m.keys[i] = a ↔ m.indices[a] = i := by
+  have := m.WF i a
+  grind
+
 /--
 Erase the key-value pair with the given key, moving the last pair into its place in the order.
 If the key is not present, the map is unchanged.
@@ -139,18 +135,18 @@ If the key is not present, the map is unchanged.
 attribute [local grind] getIdx findIdx insert
 
 @[grind] theorem getIdx_findIdx (m : IndexMap α β) (a : α) (h : a ∈ m) :
-    m.getIdx (m.findIdx a h) = m[a] := by grind
+    m.getIdx (m.findIdx a) = m[a] := by grind
 
 @[grind] theorem mem_insert (m : IndexMap α β) (a a' : α) (b : β) :
     a' ∈ m.insert a b ↔ a' = a ∨ a' ∈ m := by
   grind
 
 @[grind] theorem getElem_insert (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
-    (m.insert a b)[a']'h = if h' : a' == a then b else m[a'] := by
+    (m.insert a b)[a'] = if h' : a' == a then b else m[a'] := by
   grind
 
 @[grind] theorem findIdx_insert_self (m : IndexMap α β) (a : α) (b : β) :
-    (m.insert a b).findIdx a (by grind) = if h : a ∈ m then m.findIdx a h else m.size := by
+    (m.insert a b).findIdx a = if h : a ∈ m then m.findIdx a else m.size := by
   grind
 
 end IndexMap

tests/lean/run/grind_indexmap_pre.lean

@@ -41,20 +41,20 @@ instance : Membership α (IndexMap α β) where
 instance {m : IndexMap α β} {a : α} : Decidable (a ∈ m) :=
   inferInstanceAs (Decidable (a ∈ m.indices))
 
-instance : GetElem? (IndexMap α β) α β (fun m a => a ∈ m) where
-  getElem m a h := m.values[m.indices[a]'h]'(by sorry)
-  getElem? m a := m.indices[a]?.bind (fun i => (m.values[i]?))
-  getElem! m a := m.indices[a]?.bind (fun i => (m.values[i]?)) |>.getD default
-
 @[inline] def findIdx? (m : IndexMap α β) (a : α) : Option Nat := m.indices[a]?
 
-@[inline] def findIdx (m : IndexMap α β) (a : α) (h : a ∈ m) : Nat := m.indices[a]
+@[inline] def findIdx (m : IndexMap α β) (a : α) (h : a ∈ m := by get_elem_tactic) : Nat := m.indices[a]
 
 @[inline] def getIdx? (m : IndexMap α β) (i : Nat) : Option β := m.values[i]?
 
 @[inline] def getIdx (m : IndexMap α β) (i : Nat) (h : i < m.size := by get_elem_tactic) : β :=
   m.values[i]
 
+instance : GetElem? (IndexMap α β) α β (fun m a => a ∈ m) where
+  getElem m a h := m.values[m.indices[a]'h]'(by sorry)
+  getElem? m a := m.indices[a]?.bind (fun i => (m.values[i]?))
+  getElem! m a := m.indices[a]?.bind (fun i => (m.values[i]?)) |>.getD default
+
 instance : LawfulGetElem (IndexMap α β) α β (fun m a => a ∈ m) where
   getElem?_def := sorry
   getElem!_def := sorry

tests/lean/run/grind_linarith_1.lean

@@ -1,4 +1,5 @@
 open Lean.Grind
+set_option grind.debug true
 
 example [IntModule α] [Preorder α] [IntModule.IsOrdered α] (a b : α)
     : (2:Int)*a + b < b + a + a → False := by

tests/lean/run/grind_linarith_2.lean

@@ -1,4 +1,5 @@
 open Lean Grind
+set_option grind.debug true
 
 example [IntModule α] [Preorder α] [IntModule.IsOrdered α] (a b : α)
     : a + b = b + a  := by

tests/lean/run/grind_list2.lean

@@ -93,6 +93,14 @@ theorem getD_cons_succ : getD (x :: xs) (n + 1) d = getD xs n d := by grind
 
 /-! ### mem -/
 
+-- I've gone back and forth on this one. It's an expensive lemma to instantiate merely because we see `a ∈ l`,
+-- so globally it is set up with `grind_pattern length_pos_of_mem => a ∈ l, length l`.
+-- While it's quite useful as simply `grind →` in this "very eary theory", it doesn't  seem essential?
+
+section length_pos_of_mem
+
+attribute [local grind →] length_pos_of_mem
+
 theorem not_mem_nil {a : α} : ¬ a ∈ [] := by grind
 
 theorem mem_cons : a ∈ b :: l ↔ a = b ∨ a ∈ l := by grind
@@ -196,6 +204,8 @@ theorem contains_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
 theorem contains_cons [BEq α] {a : α} {b : α} {l : List α} :
     (a :: l).contains b = (b == a || l.contains b) := by grind
 
+end length_pos_of_mem
+
 /-! ### `isEmpty` -/
 
 theorem isEmpty_iff {l : List α} : l.isEmpty ↔ l = [] := by grind

tests/lean/run/grind_list_count.lean

@@ -122,9 +122,6 @@ theorem count_nil {a : α} : count a [] = 0 := by grind
 theorem count_cons {a b : α} {l : List α} :
     count a (b :: l) = count a l + if b == a then 1 else 0 := by grind
 
-theorem count_eq_countP {a : α} {l : List α} : count a l = countP (· == a) l := by grind
-theorem count_eq_countP' {a : α} : count a = countP (· == a) := by grind
-
 theorem count_tail {l : List α} (h : l ≠ []) (a : α) :
       l.tail.count a = l.count a - if l.head h == a then 1 else 0 := by
   induction l with grind
@@ -213,4 +210,13 @@ theorem filter_beq {l : List α} (a : α) : l.filter (· == a) = replicate (coun
   ext
   grind
 
+theorem count_flatten {α} [BEq α] {a : α} {l : List (List α)} : count a l.flatten = (l.map (count a)).sum := by
+  grind
+
+theorem count_concat_self {a : α} {l : List α} : count a (concat l a) = count a l + 1 := by grind
+
+theorem count_flatMap {α} [BEq β] {l : List α} {f : α → List β} {x : β} :
+    count x (l.flatMap f) = sum (map (count x ∘ f) l) := by
+  grind
+
 end count

tests/lean/run/grind_list_erase.lean

@@ -28,4 +28,4 @@ theorem getLast_eraseP_mem {xs : List α} {p : α → Bool} (h) : (xs.eraseP p).
 theorem set_getElem_succ_eraseIdx_succ
     {xs : Array α} {i : Nat} (h : i + 1 < xs.size) :
     (xs.eraseIdx (i + 1)).set i xs[i + 1] (by grind) = xs.eraseIdx i := by
-  grind (splits := 9)
+  grind (splits := 12)

tests/lean/run/grind_list_perm.lean

@@ -0,0 +1,21 @@
+open List
+
+example : [3,1,4,2] ~ [2,4,1,3] := by grind
+
+example (xs ys zs : List Nat) (h₁ : xs ⊆ ys) (h₂ : ys ~ zs) : xs ⊆ zs := by grind
+example (xs ys zs : List Nat) (h₁ : xs <+ ys) (h₂ : ys ~ zs) : xs ⊆ zs := by grind
+example (xs ys zs : List Nat) (h₁ : xs ~ ys) (h₂ : ys ~ zs) : xs ~ zs := by grind
+
+example : List.range 10 ~ (List.range 5 ++ List.range' 5 5).reverse := by grind
+
+variable [BEq α] [LawfulBEq α]
+
+example (xs ys : List (List α)) (h : xs ~ ys) : xs.flatten ~ ys.flatten := by grind
+
+example {l l' : List α} (hl : l ~ l') (_ : l'.Nodup) : l.Nodup := by grind
+
+example {a b : α} {as bs : List α} :
+    a :: as ++ b :: bs ~ b :: as ++ a :: bs := by grind
+
+example (x y : α) (l : List α) :
+    List.insert x (List.insert y l) ~ List.insert y (List.insert x l) := by grind

tests/lean/run/grind_module_eqs.lean

@@ -0,0 +1,37 @@
+open Lean Grind
+
+example [IntModule α] (x y : α) : x - y ≠ 0 - 2*y → x + y = 0 → False := by
+  grind
+
+example [IntModule α] (x y : α) : 2*x + 2*y ≠ 0 → x + y = 0 → False := by
+  grind
+
+example [IntModule α] (x y : α) : 2*x + 2*y ≠ 0 → 2*x + 2*y = 0 → False := by
+  grind
+
+example [IntModule α] [NoNatZeroDivisors α] (x y : α) : x + y ≠ 0 → 2*x + 2*y = 0 → False := by
+  grind
+
+example [IntModule α] [NoNatZeroDivisors α] (x y z : α) : x + y + z ≠ 0 → 2*x + 3*y = 0 → y = 2*z → False := by
+  grind
+
+example [IntModule α] [NoNatZeroDivisors α] (x y z : α) : x + y + z ≠ 0 → -3*y = 2*x → y = 2*z → False := by
+  grind
+
+example [IntModule α] (x y : α) : x + y = 0 → x - y = 0 - 2*y := by
+  grind
+
+example [IntModule α] (x y : α) : x + y = 0 → 2*x + 2*y = 0 := by
+  grind
+
+example [IntModule α] (x y : α) : 2*x + 2*y = 0 → 2*x = 0 - 2*y := by
+  grind
+
+example [IntModule α] [NoNatZeroDivisors α] (x y : α) : 2*x + 2*y = 0 → x = -y := by
+  grind
+
+example [IntModule α] [NoNatZeroDivisors α] (x y z : α) : 2*x + 3*y = 0 → y = 2*z → x + y + z = 0 := by
+  grind
+
+example [IntModule α] [NoNatZeroDivisors α] (x y z : α) : -3*y = 2*x → y = 2*z → x + y + z = 0 := by
+  grind

tests/lean/run/grind_module_normalization.lean

@@ -1,5 +1,6 @@
 open Lean Grind
 variable (R : Type u) [IntModule R]
+set_option grind.debug true
 
 example (a b : R) : a + b = b + a := by grind
 example (a : R) : a + 0 = a := by grind

tests/lean/run/grind_module_relations.lean

@@ -22,6 +22,6 @@ example (a b c : R) (h : 2 * a + 2 * b = 4 * c) : 3 * a + c = 5 * c - b + (-b) +
 
 -- In a `RatModule` we can clear common divisors.
 example (a : R) (h : a + a = 0) : a = 0 := by grind
-example (a b c : R) (h : 2 * a + 2 * b = 4 * c) : 3 * a + c = 5 * c - 3 * b := by grind
+example (a b c : R) (h : 2 * a + 2 * b = 4 * c) : 3 * a + c = 7 * c - 3 * b := by grind
 
 end RatModule

tests/lean/run/grind_ring_1.lean

@@ -16,7 +16,6 @@ example (x : UInt8) : (x + 16)*(x - 16) = x^2 := by
 
 /--
 trace: [grind.ring] new ring: Int
-[grind.ring] characteristic: 0
 [grind.ring] NoNatZeroDivisors available: true
 -/
 #guard_msgs (trace) in
@@ -29,10 +28,8 @@ example (x : BitVec 8) : (x + 16)*(x - 16) = x^2 := by
 
 /--
 trace: [grind.ring] new ring: Int
-[grind.ring] characteristic: 0
 [grind.ring] NoNatZeroDivisors available: true
 [grind.ring] new ring: BitVec 8
-[grind.ring] characteristic: 256
 [grind.ring] NoNatZeroDivisors available: false
 -/
 #guard_msgs (trace) in

tests/lean/run/grind_t1.lean

@@ -188,7 +188,6 @@ trace: [grind.assert] ∀ (a : α), a ∈ b → p a
 [grind.assert] w ∈ b
 [grind.assert] ¬p w
 [grind.ematch.instance] h₁: w ∈ b → p w
-[grind.ematch.instance] List.length_pos_of_mem: w ∈ b → 0 < b.length
 [grind.assert] w ∈ b → p w
 -/
 #guard_msgs (trace) in