copy across some Find API to Array

This PR makes the stage2 Leanc build use the stage2 oleans rather than
stage1 oleans. This was happening because Leanc's own OLEAN_OUT is at
the build root rather than the lib/lean subdirectory, so when the build
added this OLEAN_OUT to LEAN_PATH no oleans were found there and the
search fell back to the stage1 installation location.

src/Init/Data/Array/Attach.lean

@@ -8,8 +8,9 @@ import Init.Data.Array.Mem
 import Init.Data.Array.Lemmas
 import Init.Data.Array.Count
 import Init.Data.List.Attach
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Array
 

src/Init/Data/Array/Basic.lean

@@ -14,8 +14,8 @@ import Init.GetElem
 import Init.Data.List.ToArrayImpl
 import Init.Data.Array.Set
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 universe u v w
 
@@ -1090,6 +1090,11 @@ def split (as : Array α) (p : α → Bool) : Array α × Array α :=
   as.foldl (init := (#[], #[])) fun (as, bs) a =>
     if p a then (as.push a, bs) else (as, bs.push a)
 
+def replace [BEq α] (xs : Array α) (a b : α) : Array α :=
+  match xs.finIdxOf? a with
+  | none => xs
+  | some i => xs.set i b
+
 /-! ### Lexicographic ordering -/
 
 instance instLT [LT α] : LT (Array α) := ⟨fun as bs => as.toList < bs.toList⟩

src/Init/Data/Array/BasicAux.lean

@@ -8,8 +8,8 @@ import Init.Data.Array.Basic
 import Init.Data.Nat.Linear
 import Init.NotationExtra
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 theorem Array.of_push_eq_push {as bs : Array α} (h : as.push a = bs.push b) : as = bs ∧ a = b := by
   simp only [push, mk.injEq] at h

src/Init/Data/Array/BinSearch.lean

@@ -9,7 +9,7 @@ import Init.Data.Int.DivMod.Lemmas
 import Init.Omega
 universe u v
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 -- We do not use `linter.indexVariables` here as it is helpful to name the index variables as `lo`, `mid`, and `hi`.
 
 namespace Array

src/Init/Data/Array/Bootstrap.lean

@@ -13,8 +13,8 @@ import Init.Data.List.TakeDrop
 This file contains some theorems about `Array` and `List` needed for `Init.Data.List.Impl`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Array
 

src/Init/Data/Array/Count.lean

@@ -11,8 +11,8 @@ import Init.Data.List.Nat.Count
 # Lemmas about `Array.countP` and `Array.count`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Array
 

src/Init/Data/Array/DecidableEq.lean

@@ -9,8 +9,8 @@ import Init.Data.BEq
 import Init.Data.List.Nat.BEq
 import Init.ByCases
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Array
 

src/Init/Data/Array/Erase.lean

@@ -12,8 +12,8 @@ import Init.Data.List.Nat.Basic
 # Lemmas about `Array.eraseP`, `Array.erase`, and `Array.eraseIdx`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Array
 

src/Init/Data/Array/Extract.lean

@@ -13,8 +13,8 @@ import Init.Data.List.Nat.TakeDrop
 This file follows the contents of `Init.Data.List.TakeDrop` and `Init.Data.List.Nat.TakeDrop`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 open Nat
 namespace Array

src/Init/Data/Array/FinRange.lean

@@ -7,8 +7,8 @@ prelude
 import Init.Data.List.FinRange
 import Init.Data.Array.OfFn
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Array
 

src/Init/Data/Array/Find.lean

@@ -13,8 +13,8 @@ import Init.Data.Array.Range
 # Lemmas about `Array.findSome?`, `Array.find?, `Array.findIdx`, `Array.findIdx?`, `Array.idxOf`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 namespace Array
 
 open Nat
@@ -299,24 +299,6 @@ theorem find?_eq_some_iff_getElem {xs : Array α} {p : α → Bool} {b : α} :
   rcases xs with ⟨xs⟩
   simp [List.find?_eq_some_iff_getElem]
 
-/-! ### findFinIdx? -/
-
-@[simp] theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := rfl
-
--- We can't mark this as a `@[congr]` lemma since the head of the RHS is not `findFinIdx?`.
-theorem findFinIdx?_congr {p : α → Bool} {xs ys : Array α} (w : xs = ys) :
-    findFinIdx? p xs = (findFinIdx? p ys).map (fun i => i.cast (by simp [w])) := by
-  subst w
-  simp
-
-@[simp] theorem findFinIdx?_subtype {p : α → Prop} {xs : Array { x // p x }}
-    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
-    xs.findFinIdx? f = (xs.unattach.findFinIdx? g).map (fun i => i.cast (by simp)) := by
-  cases xs
-  simp only [List.findFinIdx?_toArray, hf, List.findFinIdx?_subtype]
-  rw [findFinIdx?_congr List.unattach_toArray]
-  simp [Function.comp_def]
-
 /-! ### findIdx -/
 
 theorem findIdx_of_getElem?_eq_some {xs : Array α} (w : xs[xs.findIdx p]? = some y) : p y := by
@@ -542,6 +524,47 @@ theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : Array α} {p q : α → Bo
   cases xs
   simp
 
+/-! ### findFinIdx? -/
+
+@[simp] theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := rfl
+
+-- We can't mark this as a `@[congr]` lemma since the head of the RHS is not `findFinIdx?`.
+theorem findFinIdx?_congr {p : α → Bool} {xs ys : Array α} (w : xs = ys) :
+    findFinIdx? p xs = (findFinIdx? p ys).map (fun i => i.cast (by simp [w])) := by
+  subst w
+  simp
+
+theorem findFinIdx?_eq_pmap_findIdx? {xs : Array α} {p : α → Bool} :
+    xs.findFinIdx? p =
+      (xs.findIdx? p).pmap
+        (fun i m => by simp [findIdx?_eq_some_iff_getElem] at m; exact ⟨i, m.choose⟩)
+        (fun i h => h) := by
+  simp [findIdx?_eq_map_findFinIdx?_val, Option.pmap_map]
+
+@[simp] theorem findFinIdx?_eq_none_iff {xs : Array α} {p : α → Bool} :
+    xs.findFinIdx? p = none ↔ ∀ x, x ∈ xs → ¬ p x := by
+  simp [findFinIdx?_eq_pmap_findIdx?]
+
+@[simp]
+theorem findFinIdx?_eq_some_iff {xs : Array α} {p : α → Bool} {i : Fin xs.size} :
+    xs.findFinIdx? p = some i ↔
+      p xs[i] ∧ ∀ j (hji : j < i), ¬p (xs[j]'(Nat.lt_trans hji i.2)) := by
+  simp only [findFinIdx?_eq_pmap_findIdx?, Option.pmap_eq_some_iff, findIdx?_eq_some_iff_getElem,
+    Bool.not_eq_true, Option.mem_def, exists_and_left, and_exists_self, Fin.getElem_fin]
+  constructor
+  · rintro ⟨a, ⟨h, w₁, w₂⟩, rfl⟩
+    exact ⟨w₁, fun j hji => by simpa using w₂ j hji⟩
+  · rintro ⟨h, w⟩
+    exact ⟨i, ⟨i.2, h, fun j hji => w ⟨j, by omega⟩ hji⟩, rfl⟩
+
+@[simp] theorem findFinIdx?_subtype {p : α → Prop} {xs : Array { x // p x }}
+    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+    xs.findFinIdx? f = (xs.unattach.findFinIdx? g).map (fun i => i.cast (by simp)) := by
+  cases xs
+  simp only [List.findFinIdx?_toArray, hf, List.findFinIdx?_subtype]
+  rw [findFinIdx?_congr List.unattach_toArray]
+  simp [Function.comp_def]
+
 /-! ### idxOf
 
 The verification API for `idxOf` is still incomplete.
@@ -579,10 +602,26 @@ The lemmas below should be made consistent with those for `findIdx?` (and proved
   rcases xs with ⟨xs⟩
   simp [List.idxOf?_eq_none_iff]
 
-/-! ### finIdxOf? -/
+/-! ### finIdxOf?
+
+The verification API for `finIdxOf?` is still incomplete.
+The lemmas below should be made consistent with those for `findFinIdx?` (and proved using them).
+-/
 
 theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : Array α} {a : α} :
     xs.idxOf? a = (xs.finIdxOf? a).map (·.val) := by
   simp [idxOf?, finIdxOf?, findIdx?_eq_map_findFinIdx?_val]
 
+@[simp] theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := rfl
+
+@[simp] theorem finIdxOf?_eq_none_iff [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
+    xs.finIdxOf? a = none ↔ a ∉ xs := by
+  rcases xs with ⟨xs⟩
+  simp [List.finIdxOf?_eq_none_iff]
+
+@[simp] theorem finIdxOf?_eq_some_iff [BEq α] [LawfulBEq α] {xs : Array α} {a : α} {i : Fin xs.size} :
+    xs.finIdxOf? a = some i ↔ xs[i] = a ∧ ∀ j (_ : j < i), ¬xs[j] = a := by
+  rcases xs with ⟨xs⟩
+  simp [List.finIdxOf?_eq_some_iff]
+
 end Array

src/Init/Data/Array/GetLit.lean

@@ -7,8 +7,8 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Array.Basic
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Array
 

src/Init/Data/Array/InsertIdx.lean

@@ -13,8 +13,8 @@ import Init.Data.List.Nat.InsertIdx
 Proves various lemmas about `Array.insertIdx`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 open Function
 

src/Init/Data/Array/InsertionSort.lean

@@ -6,8 +6,8 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Array.Basic
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 @[inline] def Array.insertionSort (xs : Array α) (lt : α → α → Bool := by exact (· < ·)) : Array α :=
   traverse xs 0 xs.size

src/Init/Data/Array/Lemmas.lean

@@ -22,8 +22,8 @@ import Init.Data.List.ToArray
 ## Theorems about `Array`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Array
 
@@ -833,9 +833,9 @@ theorem getElem?_set (xs : Array α) (i : Nat) (h : i < xs.size) (v : α) (j : N
   cases xs
   simp
 
-@[simp] theorem set_eq_empty_iff {xs : Array α} (n : Nat) (a : α) (h) :
-     xs.set n a = #[] ↔ xs = #[] := by
-  cases xs <;> cases n <;> simp [set]
+@[simp] theorem set_eq_empty_iff {xs : Array α} (i : Nat) (a : α) (h) :
+     xs.set i a = #[] ↔ xs = #[] := by
+  cases xs <;> cases i <;> simp [set]
 
 theorem set_comm (a b : α)
     {i j : Nat} (xs : Array α) {hi : i < xs.size} {hj : j < (xs.set i a).size} (h : i ≠ j) :
@@ -2021,7 +2021,7 @@ theorem flatten_eq_flatMap {xss : Array (Array α)} : flatten xss = xss.flatMap
   rw [← Function.comp_def, ← List.map_map, flatten_toArray_map]
 
 theorem flatten_filter_not_isEmpty {xss : Array (Array α)} :
-    flatten (xss.filter fun l => !l.isEmpty) = xss.flatten := by
+    flatten (xss.filter fun xs => !xs.isEmpty) = xss.flatten := by
   induction xss using array₂_induction
   simp [List.filter_map, Function.comp_def, List.flatten_filter_not_isEmpty]
 
@@ -3421,6 +3421,81 @@ theorem eq_push_pop_back!_of_size_ne_zero [Inhabited α] {xs : Array α} (h : xs
       rw [getElem_push_eq, back!]
       simp [← getElem!_pos]
 
+/-! ### replace -/
+
+section replace
+variable [BEq α]
+
+@[simp] theorem size_replace {xs : Array α} : (xs.replace a b).size = xs.size := by
+  simp only [replace]
+  split <;> simp
+
+-- This hypothesis could probably be dropped from some of the lemmas below,
+-- by proving them direct from the definition rather than going via `List`.
+variable [LawfulBEq α]
+
+@[simp] theorem replace_of_not_mem {xs : Array α} (h : ¬ a ∈ xs) : xs.replace a b = xs := by
+  cases xs
+  simp_all
+
+theorem getElem?_replace {xs : Array α} {i : Nat} :
+    (xs.replace a b)[i]? = if xs[i]? == some a then if a ∈ xs.take i then some a else some b else xs[i]? := by
+  rcases xs with ⟨xs⟩
+  simp only [List.replace_toArray, List.getElem?_toArray, List.getElem?_replace, beq_iff_eq,
+    take_eq_extract, List.extract_toArray, List.extract_eq_drop_take, Nat.sub_zero, List.drop_zero,
+    mem_toArray]
+  split <;> rename_i h
+  · rw (occs := [2]) [if_pos]
+    simpa using h
+  · rw [if_neg]
+    simpa using h
+
+theorem getElem?_replace_of_ne {xs : Array α} {i : Nat} (h : xs[i]? ≠ some a) :
+    (xs.replace a b)[i]? = xs[i]? := by
+  simp_all [getElem?_replace]
+
+theorem getElem_replace {xs : Array α} {i : Nat} (h : i < xs.size) :
+    (xs.replace a b)[i]'(by simpa) = if xs[i] == a then if a ∈ xs.take i then a else b else xs[i] := by
+  apply Option.some.inj
+  rw [← getElem?_eq_getElem, getElem?_replace]
+  split <;> split <;> simp_all
+
+theorem getElem_replace_of_ne {xs : Array α} {i : Nat} {h : i < xs.size} (h' : xs[i] ≠ a) :
+    (xs.replace a b)[i]'(by simpa) = xs[i]'(h) := by
+  rw [getElem_replace h]
+  simp [h']
+
+theorem replace_append {xs ys : Array α} :
+    (xs ++ ys).replace a b = if a ∈ xs then xs.replace a b ++ ys else xs ++ ys.replace a b := by
+  rcases xs with ⟨xs⟩
+  rcases ys with ⟨ys⟩
+  simp only [List.append_toArray, List.replace_toArray, List.replace_append, mem_toArray]
+  split <;> simp
+
+theorem replace_append_left {xs ys : Array α} (h : a ∈ xs) :
+    (xs ++ ys).replace a b = xs.replace a b ++ ys := by
+  simp [replace_append, h]
+
+theorem replace_append_right {xs ys : Array α} (h : ¬ a ∈ xs) :
+    (xs ++ ys).replace a b = xs ++ ys.replace a b := by
+  simp [replace_append, h]
+
+theorem replace_extract {xs : Array α} {i : Nat} :
+    (xs.extract 0 i).replace a b = (xs.replace a b).extract 0 i := by
+  rcases xs with ⟨xs⟩
+  simp [List.replace_take]
+
+@[simp] theorem replace_mkArray_self {a : α} (h : 0 < n) :
+    (mkArray n a).replace a b = #[b] ++ mkArray (n - 1) a := by
+  cases n <;> simp_all [mkArray_succ', replace_append]
+
+@[simp] theorem replace_mkArray_ne {a b c : α} (h : !b == a) :
+    (mkArray n a).replace b c = mkArray n a := by
+  rw [replace_of_not_mem]
+  simp_all
+
+end replace
+
 /-! Content below this point has not yet been aligned with `List`. -/
 
 /-! ### sum -/

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

@@ -8,8 +8,8 @@ import Init.Data.Array.Basic
 import Init.Data.Nat.Lemmas
 import Init.Data.Range
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Array
 

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

@@ -7,8 +7,8 @@ prelude
 import Init.Data.Array.Lemmas
 import Init.Data.List.Lex
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Array
 

src/Init/Data/Array/MapIdx.lean

@@ -8,8 +8,8 @@ import Init.Data.Array.Lemmas
 import Init.Data.Array.Attach
 import Init.Data.List.MapIdx
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Array
 

src/Init/Data/Array/Mem.lean

@@ -8,8 +8,8 @@ import Init.Data.Array.Basic
 import Init.Data.Nat.Linear
 import Init.Data.List.BasicAux
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Array
 

src/Init/Data/Array/Monadic.lean

@@ -12,8 +12,8 @@ import Init.Data.List.Monadic
 # Lemmas about `Array.forIn'` and `Array.forIn`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Array
 

src/Init/Data/Array/OfFn.lean

@@ -11,8 +11,8 @@ import Init.Data.List.OfFn
 # Theorems about `Array.ofFn`
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Array
 

src/Init/Data/Array/Perm.lean

@@ -7,8 +7,8 @@ prelude
 import Init.Data.List.Nat.Perm
 import Init.Data.Array.Lemmas
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Array
 

src/Init/Data/Array/QSort.lean

@@ -7,7 +7,7 @@ prelude
 import Init.Data.Vector.Basic
 import Init.Data.Ord
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 -- We do not enable `linter.indexVariables` because it is helpful to name index variables `lo`, `mid`, `hi`, etc.
 
 namespace Array

src/Init/Data/Array/Range.lean

@@ -15,8 +15,8 @@ import Init.Data.List.Nat.Range
 
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Array
 
@@ -149,9 +149,9 @@ theorem range_succ (n : Nat) : range (succ n) = range n ++ #[n] := by
       dite_eq_ite]
     split <;> omega
 
-theorem range_add (a b : Nat) : range (a + b) = range a ++ (range b).map (a + ·) := by
+theorem range_add (n m : Nat) : range (n + m) = range n ++ (range m).map (n + ·) := by
   rw [← range'_eq_map_range]
-  simpa [range_eq_range', Nat.add_comm] using (range'_append_1 0 a b).symm
+  simpa [range_eq_range', Nat.add_comm] using (range'_append_1 0 n m).symm
 
 theorem reverse_range' (s n : Nat) : reverse (range' s n) = map (s + n - 1 - ·) (range n) := by
   simp [← toList_inj, List.reverse_range']
@@ -164,7 +164,7 @@ theorem not_mem_range_self {n : Nat} : n ∉ range n := by simp
 
 theorem self_mem_range_succ (n : Nat) : n ∈ range (n + 1) := by simp
 
-@[simp] theorem take_range (m n : Nat) : take (range n) m = range (min m n) := by
+@[simp] 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} :

src/Init/Data/Array/Set.lean

@@ -6,8 +6,8 @@ Authors: Leonardo de Moura, Mario Carneiro
 prelude
 import Init.Tactics
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 
 /--

src/Init/Data/Array/Subarray.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Array.Basic
 
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 universe u v w
 

src/Init/Data/Array/Subarray/Split.lean

@@ -15,8 +15,8 @@ automation. Placing them in another module breaks an import cycle, because `omeg
 array library.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Subarray
 /--

src/Init/Data/Array/TakeDrop.lean

@@ -12,8 +12,8 @@ These lemmas are used in the internals of HashMap.
 They should find a new home and/or be reformulated.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

src/Init/Data/Array/Zip.lean

@@ -11,8 +11,8 @@ import Init.Data.List.Zip
 # Lemmas about `Array.zip`, `Array.zipWith`, `Array.zipWithAll`, and `Array.unzip`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Array
 
@@ -114,7 +114,7 @@ theorem map_zipWith {δ : Type _} (f : α → β) (g : γ → δ → α) (cs : A
   cases ds
   simp [List.map_zipWith]
 
-theorem take_zipWith : (zipWith f as bs).take n = zipWith f (as.take n) (bs.take n) := by
+theorem take_zipWith : (zipWith f as bs).take i = zipWith f (as.take i) (bs.take i) := by
   cases as
   cases bs
   simp [List.take_zipWith]

src/Init/Data/Int/Linear.lean

@@ -856,6 +856,25 @@ theorem eq_norm (ctx : Context) (p₁ p₂ : Poly) (h : p₁.norm == p₂) : p
   simp at h
   simp [*]
 
+def eq_coeff_cert (p p' : Poly) (k : Int) : Bool :=
+  p == p'.mul k && k > 0
+
+theorem eq_coeff (ctx : Context) (p p' : Poly) (k : Int) : eq_coeff_cert p p' k → p.denote' ctx = 0 → p'.denote' ctx = 0 := by
+  simp [eq_coeff_cert]
+  intro _ _; simp [mul_eq_zero_iff, *]
+
+theorem eq_unsat (ctx : Context) (p : Poly) : p.isUnsatEq → p.denote' ctx = 0 → False := by
+  simp [Poly.isUnsatEq] <;> split <;> simp
+
+def eq_unsat_coeff_cert (p : Poly) (k : Int) : Bool :=
+  p.divCoeffs k && k > 0 && cmod p.getConst k < 0
+
+theorem eq_unsat_coeff (ctx : Context) (p : Poly) (k : Int) : eq_unsat_coeff_cert p k → p.denote' ctx = 0 → False := by
+  simp [eq_unsat_coeff_cert]
+  intro h₁ h₂ h₃
+  have h := poly_eq_zero_eq_false ctx h₁ h₂ h₃; clear h₁ h₂ h₃
+  simp [h]
+
 def Poly.coeff (p : Poly) (x : Var) : Int :=
   match p with
   | .add a y p => bif x == y then a else coeff p x
@@ -978,6 +997,15 @@ theorem eq_le_subst_nonpos (ctx : Context) (x : Var) (p₁ : Poly) (p₂ : Poly)
   rw [Int.mul_comm]
   assumption
 
+def eq_of_core_cert (p₁ : Poly) (p₂ : Poly) (p₃ : Poly) : Bool :=
+  p₃ == p₁.combine (p₂.mul (-1))
+
+theorem eq_of_core (ctx : Context) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly)
+    : eq_of_core_cert p₁ p₂ p₃ → p₁.denote' ctx = p₂.denote' ctx → p₃.denote' ctx = 0 := by
+  simp [eq_of_core_cert]
+  intro; subst p₃; simp
+  intro h; rw [h, ←Int.sub_eq_add_neg, Int.sub_self]
+
 end Int.Linear
 
 theorem Int.not_le_eq (a b : Int) : (¬a ≤ b) = (b + 1 ≤ a) := by

src/Init/Data/List/Attach.lean

@@ -8,8 +8,8 @@ import Init.Data.List.Count
 import Init.Data.Subtype
 import Init.BinderNameHint
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

src/Init/Data/List/Basic.lean

@@ -58,8 +58,8 @@ Further operations are defined in `Init.Data.List.BasicAux`
 -/
 
 set_option linter.missingDocs true -- keep it documented
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 open Decidable List
 

src/Init/Data/List/BasicAux.lean

@@ -6,8 +6,8 @@ Author: Leonardo de Moura
 prelude
 import Init.Data.Nat.Linear
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 universe u
 

src/Init/Data/List/Control.lean

@@ -9,8 +9,8 @@ import Init.Control.Id
 import Init.Control.Lawful
 import Init.Data.List.Basic
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 universe u v w u₁ u₂

src/Init/Data/List/Count.lean

@@ -10,8 +10,8 @@ import Init.Data.List.Sublist
 # Lemmas about `List.countP` and `List.count`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

src/Init/Data/List/Erase.lean

@@ -12,8 +12,8 @@ import Init.Data.List.Find
 # Lemmas about `List.eraseP`, `List.erase`, and `List.eraseIdx`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

src/Init/Data/List/FinRange.lean

@@ -6,8 +6,8 @@ Authors: François G. Dorais
 prelude
 import Init.Data.List.OfFn
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

src/Init/Data/List/Find.lean

@@ -15,8 +15,8 @@ Lemmas about `List.findSome?`, `List.find?`, `List.findIdx`, `List.findIdx?`, `L
 and `List.lookup`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 
 namespace List
@@ -514,47 +514,6 @@ private theorem findIdx?_go_eq {p : α → Bool} {xs : List α} {i : Nat} :
     (x :: xs).findIdx? p = if p x then some 0 else (xs.findIdx? p).map fun i => i + 1 := by
   simp [findIdx?, findIdx?_go_eq]
 
-/-! ### findFinIdx? -/
-
-@[simp] theorem findFinIdx?_nil {p : α → Bool} : findFinIdx? p [] = none := rfl
-
-theorem findIdx?_go_eq_map_findFinIdx?_go_val {xs : List α} {p : α → Bool} {i : Nat} {h} :
-    List.findIdx?.go p xs i =
-      (List.findFinIdx?.go p l xs i h).map (·.val) := by
-  unfold findIdx?.go
-  unfold findFinIdx?.go
-  split
-  · simp_all
-  · simp only
-    split
-    · simp
-    · rw [findIdx?_go_eq_map_findFinIdx?_go_val]
-
-theorem findIdx?_eq_map_findFinIdx?_val {xs : List α} {p : α → Bool} :
-    xs.findIdx? p = (xs.findFinIdx? p).map (·.val) := by
-  simp [findIdx?, findFinIdx?]
-  rw [findIdx?_go_eq_map_findFinIdx?_go_val]
-
-@[simp] theorem findFinIdx?_cons {p : α → Bool} {x : α} {xs : List α} :
-    findFinIdx? p (x :: xs) = if p x then some 0 else (findFinIdx? p xs).map Fin.succ := by
-  rw [← Option.map_inj_right (f := Fin.val) (fun a b => Fin.eq_of_val_eq)]
-  rw [← findIdx?_eq_map_findFinIdx?_val]
-  rw [findIdx?_cons]
-  split
-  · simp
-  · rw [findIdx?_eq_map_findFinIdx?_val]
-    simp [Function.comp_def]
-
-@[simp] theorem findFinIdx?_subtype {p : α → Prop} {l : List { x // p x }}
-    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
-    l.findFinIdx? f = (l.unattach.findFinIdx? g).map (fun i => i.cast (by simp)) := by
-  unfold unattach
-  induction l with
-  | nil => simp
-  | cons a l ih =>
-    simp [hf, findFinIdx?_cons]
-    split <;> simp [ih, Function.comp_def]
-
 /-! ### findIdx -/
 
 theorem findIdx_cons (p : α → Bool) (b : α) (l : List α) :
@@ -976,6 +935,71 @@ theorem findIdx_eq_getD_findIdx? {xs : List α} {p : α → Bool} :
     simp [hf, findIdx?_cons]
     split <;> simp [ih, Function.comp_def]
 
+/-! ### findFinIdx? -/
+
+@[simp] theorem findFinIdx?_nil {p : α → Bool} : findFinIdx? p [] = none := rfl
+
+theorem findIdx?_go_eq_map_findFinIdx?_go_val {xs : List α} {p : α → Bool} {i : Nat} {h} :
+    List.findIdx?.go p xs i =
+      (List.findFinIdx?.go p l xs i h).map (·.val) := by
+  unfold findIdx?.go
+  unfold findFinIdx?.go
+  split
+  · simp_all
+  · simp only
+    split
+    · simp
+    · rw [findIdx?_go_eq_map_findFinIdx?_go_val]
+
+theorem findIdx?_eq_map_findFinIdx?_val {xs : List α} {p : α → Bool} :
+    xs.findIdx? p = (xs.findFinIdx? p).map (·.val) := by
+  simp [findIdx?, findFinIdx?]
+  rw [findIdx?_go_eq_map_findFinIdx?_go_val]
+
+theorem findFinIdx?_eq_pmap_findIdx? {xs : List α} {p : α → Bool} :
+    xs.findFinIdx? p =
+      (xs.findIdx? p).pmap
+        (fun i m => by simp [findIdx?_eq_some_iff_getElem] at m; exact ⟨i, m.choose⟩)
+        (fun i h => h) := by
+  simp [findIdx?_eq_map_findFinIdx?_val, Option.pmap_map]
+
+@[simp] theorem findFinIdx?_cons {p : α → Bool} {x : α} {xs : List α} :
+    findFinIdx? p (x :: xs) = if p x then some 0 else (findFinIdx? p xs).map Fin.succ := by
+  rw [← Option.map_inj_right (f := Fin.val) (fun a b => Fin.eq_of_val_eq)]
+  rw [← findIdx?_eq_map_findFinIdx?_val]
+  rw [findIdx?_cons]
+  split
+  · simp
+  · rw [findIdx?_eq_map_findFinIdx?_val]
+    simp [Function.comp_def]
+
+@[simp] theorem findFinIdx?_eq_none_iff {l : List α} {p : α → Bool} :
+    l.findFinIdx? p = none ↔ ∀ x ∈ l, ¬ p x := by
+  simp [findFinIdx?_eq_pmap_findIdx?]
+
+@[simp]
+theorem findFinIdx?_eq_some_iff {xs : List α} {p : α → Bool} {i : Fin xs.length} :
+    xs.findFinIdx? p = some i ↔
+      p xs[i] ∧ ∀ j (hji : j < i), ¬p (xs[j]'(Nat.lt_trans hji i.2)) := by
+  simp only [findFinIdx?_eq_pmap_findIdx?, Option.pmap_eq_some_iff, findIdx?_eq_some_iff_getElem,
+    Bool.not_eq_true, Option.mem_def, exists_and_left, and_exists_self, Fin.getElem_fin]
+  constructor
+  · rintro ⟨a, ⟨h, w₁, w₂⟩, rfl⟩
+    exact ⟨w₁, fun j hji => by simpa using w₂ j hji⟩
+  · rintro ⟨h, w⟩
+    exact ⟨i, ⟨i.2, h, fun j hji => w ⟨j, by omega⟩ hji⟩, rfl⟩
+
+@[simp] theorem findFinIdx?_subtype {p : α → Prop} {l : List { x // p x }}
+    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+    l.findFinIdx? f = (l.unattach.findFinIdx? g).map (fun i => i.cast (by simp)) := by
+  unfold unattach
+  induction l with
+  | nil => simp
+  | cons a l ih =>
+    simp [hf, findFinIdx?_cons]
+    split <;> simp [ih, Function.comp_def]
+
+
 /-! ### idxOf
 
 The verification API for `idxOf` is still incomplete.
@@ -1035,6 +1059,36 @@ theorem idxOf_lt_length [BEq α] [LawfulBEq α] {l : List α} (h : a ∈ l) : l.
 @[deprecated idxOf_lt_length (since := "2025-01-29")]
 abbrev indexOf_lt_length := @idxOf_lt_length
 
+/-! ### finIdxOf?
+
+The verification API for `finIdxOf?` is still incomplete.
+The lemmas below should be made consistent with those for `findFinIdx?` (and proved using them).
+-/
+
+theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : List α} {a : α} :
+    xs.idxOf? a = (xs.finIdxOf? a).map (·.val) := by
+  simp [idxOf?, finIdxOf?, findIdx?_eq_map_findFinIdx?_val]
+
+@[simp] theorem finIdxOf?_nil [BEq α] : ([] : List α).finIdxOf? a = none := rfl
+
+@[simp] theorem finIdxOf?_cons [BEq α] (a : α) (xs : List α) :
+    (a :: xs).finIdxOf? b =
+      if a == b then some ⟨0, by simp⟩ else (xs.finIdxOf? b).map (·.succ) := by
+  simp [finIdxOf?]
+
+@[simp] theorem finIdxOf?_eq_none_iff [BEq α] [LawfulBEq α] {l : List α} {a : α} :
+    l.finIdxOf? a = none ↔ a ∉ l := by
+  simp only [finIdxOf?, findFinIdx?_eq_none_iff, beq_iff_eq]
+  constructor
+  · intro w m
+    exact w a m rfl
+  · rintro h a m rfl
+    exact h m
+
+@[simp] theorem finIdxOf?_eq_some_iff [BEq α] [LawfulBEq α] {l : List α} {a : α} {i : Fin l.length} :
+    l.finIdxOf? a = some i ↔ l[i] = a ∧ ∀ j (_ : j < i), ¬l[j] = a := by
+  simp only [finIdxOf?, findFinIdx?_eq_some_iff, beq_iff_eq]
+
 /-! ### idxOf?
 
 The verification API for `idxOf?` is still incomplete.
@@ -1060,12 +1114,6 @@ theorem idxOf?_cons [BEq α] (a : α) (xs : List α) (b : α) :
 @[deprecated idxOf?_eq_none_iff (since := "2025-01-29")]
 abbrev indexOf?_eq_none_iff := @idxOf?_eq_none_iff
 
-/-! ### finIdxOf? -/
-
-theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : List α} {a : α} :
-    xs.idxOf? a = (xs.finIdxOf? a).map (·.val) := by
-  simp [idxOf?, finIdxOf?, findIdx?_eq_map_findFinIdx?_val]
-
 /-! ### lookup -/
 
 section lookup

src/Init/Data/List/Impl.lean

@@ -16,8 +16,8 @@ If you import `Init.Data.List.Basic` but do not import this file,
 then at runtime you will get non-tail recursive versions of the following definitions.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

src/Init/Data/List/Lemmas.lean

@@ -74,8 +74,8 @@ Also
 
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 
@@ -3086,8 +3086,12 @@ variable [BEq α]
 @[simp] theorem replace_cons_self [LawfulBEq α] {a : α} : (a::as).replace a b = b::as := by
   simp [replace_cons]
 
-@[simp] theorem replace_of_not_mem {l : List α} (h : !l.elem a) : l.replace a b = l := by
-  induction l <;> simp_all [replace_cons]
+@[simp] theorem replace_of_not_mem [LawfulBEq α] {l : List α} (h : a ∉ l) : l.replace a b = l := by
+  induction l with
+  | nil => rfl
+  | cons x xs ih =>
+    simp only [replace_cons]
+    split <;> simp_all
 
 @[simp] theorem length_replace {l : List α} : (l.replace a b).length = l.length := by
   induction l with
@@ -3170,7 +3174,7 @@ theorem replace_take {l : List α} {i : Nat} :
     (replicate n a).replace a b = b :: replicate (n - 1) a := by
   cases n <;> simp_all [replicate_succ, replace_cons]
 
-@[simp] theorem replace_replicate_ne {a b c : α} (h : !b == a) :
+@[simp] theorem replace_replicate_ne [LawfulBEq α] {a b c : α} (h : !b == a) :
     (replicate n a).replace b c = replicate n a := by
   rw [replace_of_not_mem]
   simp_all

src/Init/Data/List/Lex.lean

@@ -7,8 +7,8 @@ prelude
 import Init.Data.List.Lemmas
 import Init.Data.List.Nat.TakeDrop
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

src/Init/Data/List/MapIdx.lean

@@ -11,8 +11,8 @@ import Init.Data.List.OfFn
 import Init.Data.Fin.Lemmas
 import Init.Data.Option.Attach
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

src/Init/Data/List/MinMax.lean

@@ -10,8 +10,8 @@ import Init.Data.List.Lemmas
 # Lemmas about `List.min?` and `List.max?.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

src/Init/Data/List/Monadic.lean

@@ -11,8 +11,8 @@ import Init.Data.List.Attach
 # Lemmas about `List.mapM` and `List.forM`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

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

@@ -7,8 +7,8 @@ prelude
 import Init.Data.Nat.Lemmas
 import Init.Data.List.Basic
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

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

@@ -15,8 +15,8 @@ import Init.Data.Nat.Lemmas
 In particular, `omega` is available here.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 open Nat
 
@@ -95,12 +95,12 @@ theorem getElem_eq_getElem_reverse {l : List α} {i} (h : i < l.length) :
   to the larger of `n` and `l.length` -/
 -- We don't mark this as a `@[simp]` lemma since we allow `simp` to unfold `leftpad`,
 -- so the left hand side simplifies directly to `n - l.length + l.length`.
-theorem length_lengthpad (n : Nat) (a : α) (l : List α) :
+theorem length_leftpad (n : Nat) (a : α) (l : List α) :
     (leftpad n a l).length = max n l.length := by
   simp only [leftpad, length_append, length_replicate, Nat.sub_add_eq_max]
 
-@[deprecated length_lengthpad (since := "2025-02-24")]
-abbrev leftpad_length := @length_lengthpad
+@[deprecated length_leftpad (since := "2025-02-24")]
+abbrev leftpad_length := @length_leftpad
 
 theorem length_rightpad (n : Nat) (a : α) (l : List α) :
     (rightpad n a l).length = max n l.length := by

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

@@ -7,8 +7,8 @@ prelude
 import Init.Data.List.Count
 import Init.Data.Nat.Lemmas
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

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

@@ -7,8 +7,8 @@ prelude
 import Init.Data.List.Nat.TakeDrop
 import Init.Data.List.Erase
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

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

@@ -7,8 +7,8 @@ prelude
 import Init.Data.List.Nat.Range
 import Init.Data.List.Find
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

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

@@ -12,8 +12,8 @@ import Init.Data.List.Nat.Modify
 Proves various lemmas about `List.insertIdx`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 open Function Nat
 

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

@@ -8,8 +8,8 @@ prelude
 import Init.Data.List.Nat.TakeDrop
 import Init.Data.List.Nat.Erase
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

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

@@ -12,8 +12,8 @@ import Init.Data.List.Pairwise
 # Lemmas about `List.Pairwise`
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

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

@@ -7,8 +7,8 @@ prelude
 import Init.Data.List.Nat.TakeDrop
 import Init.Data.List.Perm
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

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

@@ -14,8 +14,8 @@ import Init.Data.List.Erase
 # Lemmas about `List.range` and `List.enum`
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

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

@@ -16,8 +16,8 @@ These are in a separate file from most of the lemmas about `List.IsSuffix`
 as they required importing more lemmas about natural numbers, and use `omega`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

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

@@ -16,8 +16,8 @@ These are in a separate file from most of the list lemmas
 as they required importing more lemmas about natural numbers, and use `omega`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 
@@ -115,12 +115,12 @@ 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 j : Nat, take i (replicate j a) = replicate (min i j) a
+@[simp] 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 j : Nat, drop i (replicate j a) = replicate (j - i) a
+@[simp] 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]

src/Init/Data/List/Notation.lean

@@ -11,8 +11,8 @@ import Init.Data.Nat.Div.Basic
 -/
 
 set_option linter.missingDocs true -- keep it documented
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 open Decidable List
 

src/Init/Data/List/OfFn.lean

@@ -11,8 +11,8 @@ import Init.Data.Fin.Fold
 # Theorems about `List.ofFn`
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

src/Init/Data/List/Pairwise.lean

@@ -11,8 +11,8 @@ import Init.Data.List.Attach
 # Lemmas about `List.Pairwise` and `List.Nodup`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

src/Init/Data/List/Perm.lean

@@ -18,8 +18,8 @@ another.
 The notation `~` is used for permutation equivalence.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 open Nat
 

src/Init/Data/List/Range.lean

@@ -14,8 +14,8 @@ Most of the results are deferred to `Data.Init.List.Nat.Range`, where more resul
 natural arithmetic are available.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 
@@ -74,7 +74,7 @@ theorem mem_range' : ∀{n}, m ∈ range' s n step ↔ ∃ i < n, m = s + step *
     rw [exists_comm]; simp [Nat.mul_succ, Nat.add_assoc, Nat.add_comm]
 
 theorem getElem?_range' (s step) :
-    ∀ {i j : Nat}, i < j → (range' s j step)[i]? = some (s + step * i)
+    ∀ {i n : Nat}, i < n → (range' s n step)[i]? = some (s + step * i)
   | 0, n + 1, _ => by simp [range'_succ]
   | m + 1, n + 1, h => by
     simp only [range'_succ, getElem?_cons_succ]
@@ -147,10 +147,10 @@ theorem range_loop_range' : ∀ s n : Nat, range.loop s (range' s n) = range' 0
 theorem range_eq_range' (n : Nat) : range n = range' 0 n :=
   (range_loop_range' n 0).trans <| by rw [Nat.zero_add]
 
-theorem getElem?_range {i j : Nat} (h : i < j) : (range j)[i]? = some i := by
+theorem getElem?_range {i n : Nat} (h : i < n) : (range n)[i]? = some i := by
   simp [range_eq_range', getElem?_range' _ _ h]
 
-@[simp] theorem getElem_range {i : Nat} (j) (h : j < (range i).length) : (range i)[j] = j := by
+@[simp] theorem getElem_range {n : Nat} (j) (h : j < (range n).length) : (range n)[j] = j := by
   simp [range_eq_range']
 
 theorem range_succ_eq_map (n : Nat) : range (n + 1) = 0 :: map succ (range n) := by
@@ -183,9 +183,9 @@ theorem range_subset {m n : Nat} : range m ⊆ range n ↔ m ≤ n := by
 theorem range_succ (n : Nat) : range (succ n) = range n ++ [n] := by
   simp only [range_eq_range', range'_1_concat, Nat.zero_add]
 
-theorem range_add (a b : Nat) : range (a + b) = range a ++ (range b).map (a + ·) := by
+theorem range_add (n m : Nat) : range (n + m) = range n ++ (range m).map (n + ·) := by
   rw [← range'_eq_map_range]
-  simpa [range_eq_range', Nat.add_comm] using (range'_append_1 0 a b).symm
+  simpa [range_eq_range', Nat.add_comm] using (range'_append_1 0 n m).symm
 
 theorem head?_range (n : Nat) : (range n).head? = if n = 0 then none else some 0 := by
   induction n with

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

@@ -14,8 +14,8 @@ These definitions are intended for verification purposes,
 and are replaced at runtime by efficient versions in `Init.Data.List.Sort.Impl`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

src/Init/Data/List/Sort/Impl.lean

@@ -31,8 +31,8 @@ as long as such improvements are carefully validated by benchmarking,
 they can be done without changing the theory, as long as a `@[csimp]` lemma is provided.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 open List
 

src/Init/Data/List/Sort/Lemmas.lean

@@ -21,8 +21,8 @@ import Init.Data.Bool
 
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

src/Init/Data/List/Sublist.lean

@@ -11,8 +11,8 @@ import Init.Data.List.TakeDrop
 # Lemmas about `List.Subset`, `List.Sublist`, `List.IsPrefix`, `List.IsSuffix`, and `List.IsInfix`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

src/Init/Data/List/TakeDrop.lean

@@ -10,8 +10,8 @@ import Init.Data.List.Lemmas
 # Lemmas about `List.take` and `List.drop`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

src/Init/Data/List/ToArray.lean

@@ -15,8 +15,8 @@ import Init.Data.Array.Lex.Basic
 We prefer to pull `List.toArray` outwards past `Array` operations.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Array
 
@@ -658,6 +658,40 @@ private theorem insertIdx_loop_toArray (i : Nat) (l : List α) (j : Nat) (hj : j
   · simp only [size_toArray, Nat.not_le] at h'
     rw [List.insertIdx_of_length_lt (h := h')]
 
+@[simp]
+theorem replace_toArray [BEq α] [LawfulBEq α] (l : List α) (a b : α) :
+    l.toArray.replace a b = (l.replace a b).toArray := by
+  rw [Array.replace]
+  split <;> rename_i i h
+  · simp only [finIdxOf?_toArray, finIdxOf?_eq_none_iff] at h
+    rw [replace_of_not_mem]
+    simpa
+  · simp_all only [finIdxOf?_toArray, finIdxOf?_eq_some_iff, Fin.getElem_fin, set_toArray,
+      mk.injEq]
+    apply List.ext_getElem
+    · simp
+    · intro j h₁ h₂
+      rw [List.getElem_replace, List.getElem_set]
+      by_cases h₃ : j < i
+      · rw [if_neg (by omega), if_neg]
+        simp only [length_set] at h₁ h₃
+        simpa using h.2 ⟨j, by omega⟩ h₃
+      · by_cases h₃ : j = i
+        · rw [if_pos (by omega), if_pos, if_neg]
+          · simp only [mem_take_iff_getElem, not_exists]
+            intro k hk
+            simpa using h.2 ⟨k, by omega⟩ (by show k < i.1; omega)
+          · subst h₃
+            simpa using h.1
+        · rw [if_neg (by omega)]
+          split
+          · rw [if_pos]
+            · simp_all
+            · simp only [mem_take_iff_getElem]
+              simp only [length_set] at h₁
+              exact ⟨i, by omega, h.1⟩
+          · rfl
+
 @[simp] theorem leftpad_toArray (n : Nat) (a : α) (l : List α) :
     Array.leftpad n a l.toArray = (leftpad n a l).toArray := by
   simp [leftpad, Array.leftpad, ← toArray_replicate]

src/Init/Data/List/ToArrayImpl.lean

@@ -6,8 +6,8 @@ Authors: Henrik Böving
 prelude
 import Init.Data.List.Basic
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 /--
 Auxiliary definition for `List.toArray`.

src/Init/Data/List/Zip.lean

@@ -11,8 +11,8 @@ import Init.Data.Function
 # Lemmas about `List.zip`, `List.zipWith`, `List.zipWithAll`, and `List.unzip`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

src/Init/Data/Option/Lemmas.lean

@@ -654,6 +654,11 @@ theorem map_pmap {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (o H)
     Option.map g (pmap f o H) = pmap (fun a h => g (f a h)) o H := by
   cases o <;> simp
 
+theorem pmap_map (o : Option α) (f : α → β) {p : β → Prop} (g : ∀ b, p b → γ) (H) :
+    pmap g (o.map f) H =
+      pmap (fun a h => g (f a) h) o (fun a m => H (f a) (mem_map_of_mem f m)) := by
+  cases o <;> simp
+
 /-! ### pelim -/
 
 @[simp] theorem pelim_none : pelim none b f = b := rfl

src/Init/Data/Vector/Basic.lean

@@ -455,6 +455,9 @@ to avoid having to have the predicate live in `p : α → m (ULift Bool)`.
 @[inline] def count [BEq α] (a : α) (xs : Vector α n) : Nat :=
   xs.toArray.count a
 
+@[inline] def replace [BEq α] (xs : Vector α n) (a b : α) : Vector α n :=
+  ⟨xs.toArray.replace a b, by simp⟩
+
 /--
 Pad a vector on the left with a given element.
 

src/Init/Data/Vector/Count.lean

@@ -11,8 +11,8 @@ import Init.Data.Vector.Lemmas
 # Lemmas about `Vector.countP` and `Vector.count`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Vector
 
@@ -101,6 +101,7 @@ theorem countP_set (p : α → Bool) (xs : Vector α n) (i : Nat) (a : α) (h :
   rcases xs with ⟨xs, rfl⟩
   simp
 
+set_option linter.listVariables false in -- This can probably be removed later.
 @[simp] theorem countP_flatten (xss : Vector (Vector α m) n) :
     countP p xss.flatten = (xss.map (countP p)).sum := by
   rcases xss with ⟨xss, rfl⟩
@@ -159,6 +160,7 @@ theorem count_le_count_push (a b : α) (xs : Vector α n) : count a xs ≤ count
     count a (xs ++ ys) = count a xs + count a ys :=
   countP_append ..
 
+set_option linter.listVariables false in -- This can probably be removed later.
 @[simp] theorem count_flatten (a : α) (xss : Vector (Vector α m) n) :
     count a xss.flatten = (xss.map (count a)).sum := by
   rcases xss with ⟨xss, rfl⟩

src/Init/Data/Vector/DecidableEq.lean

@@ -7,8 +7,8 @@ prelude
 import Init.Data.Array.DecidableEq
 import Init.Data.Vector.Lemmas
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Vector
 

src/Init/Data/Vector/Erase.lean

@@ -11,8 +11,8 @@ import Init.Data.Array.Erase
 # Lemmas about `Vector.eraseIdx`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Vector
 

src/Init/Data/Vector/Extract.lean

@@ -11,8 +11,8 @@ import Init.Data.Array.Extract
 # Lemmas about `Vector.extract`
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 open Nat
 

src/Init/Data/Vector/FinRange.lean

@@ -7,8 +7,8 @@ prelude
 import Init.Data.Array.FinRange
 import Init.Data.Vector.OfFn
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Vector
 

src/Init/Data/Vector/InsertIdx.lean

@@ -13,8 +13,8 @@ import Init.Data.Array.InsertIdx
 Proves various lemmas about `Vector.insertIdx`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 open Function Nat
 

src/Init/Data/Vector/Lemmas.lean

@@ -12,6 +12,7 @@ import Init.Data.Array.Find
 ## Vectors
 Lemmas about `Vector α n`
 -/
+
 -- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 -- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
@@ -245,6 +246,9 @@ abbrev zipWithIndex_mk := @zipIdx_mk
 @[simp] theorem count_mk [BEq α] (xs : Array α) (h : xs.size = n) (a : α) :
     (Vector.mk xs h).count a = xs.count a := rfl
 
+@[simp] theorem replace_mk [BEq α] (xs : Array α) (h : xs.size = n) (a b) :
+    (Vector.mk xs h).replace a b = Vector.mk (xs.replace a b) (by simp [h]) := rfl
+
 @[simp] theorem eq_mk : xs = Vector.mk as h ↔ xs.toArray = as := by
   cases xs
   simp
@@ -405,6 +409,9 @@ theorem toArray_mapM_go [Monad m] [LawfulMonad m] (f : α → m β) (xs : Vector
   cases xs
   simp
 
+@[simp] theorem replace_toArray [BEq α] (xs : Vector α n) (a b) :
+    xs.toArray.replace a b = (xs.replace a b).toArray := rfl
+
 @[simp] theorem find?_toArray (p : α → Bool) (xs : Vector α n) :
     xs.toArray.find? p = xs.find? p := by
   cases xs
@@ -2369,8 +2376,8 @@ theorem back?_eq_some_iff {xs : Vector α n} {a : α} :
 
 @[simp] theorem back_append_of_neZero {xs : Vector α n} {ys : Vector α m} [NeZero m] :
     (xs ++ ys).back = ys.back := by
-  rcases xs with ⟨l⟩
-  rcases ys with ⟨l'⟩
+  rcases xs with ⟨xs, rfl⟩
+  rcases ys with ⟨ys, rfl⟩
   simp only [mk_append_mk, back_mk]
   rw [Array.back_append_of_size_pos]
 
@@ -2416,6 +2423,7 @@ theorem back?_flatMap {xs : Vector α n} {f : α → Vector β m} :
   simp [Array.back?_flatMap]
   rfl
 
+set_option linter.listVariables false in -- This can probably be removed later.
 theorem back?_flatten {xss : Vector (Vector α m) n} :
     (flatten xss).back? = xss.reverse.findSome? fun xs => xs.back? := by
   rcases xss with ⟨xss, rfl⟩
@@ -2502,6 +2510,81 @@ theorem pop_append {xs : Vector α n} {ys : Vector α m} :
 @[simp] theorem pop_mkVector (n) (a : α) : (mkVector n a).pop = mkVector (n - 1) a := by
   ext <;> simp
 
+/-! ### replace -/
+
+section replace
+variable [BEq α]
+
+@[simp] theorem replace_cast {xs : Vector α n} {a b : α} :
+    (xs.cast h).replace a b = (xs.replace a b).cast (by simp [h]) := by
+  rcases xs with ⟨xs, rfl⟩
+  simp
+
+-- This hypothesis could probably be dropped from some of the lemmas below,
+-- by proving them direct from the definition rather than going via `List`.
+variable [LawfulBEq α]
+
+@[simp] theorem replace_of_not_mem {xs : Vector α n} (h : ¬ a ∈ xs) : xs.replace a b = xs := by
+  rcases xs with ⟨xs, rfl⟩
+  simp_all
+
+theorem getElem?_replace {xs : Vector α n} {i : Nat} :
+    (xs.replace a b)[i]? = if xs[i]? == some a then if a ∈ xs.take i then some a else some b else xs[i]? := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.getElem?_replace]
+  split <;> rename_i h
+  · rw (occs := [2]) [if_pos]
+    simpa using h
+  · rw [if_neg]
+    simpa using h
+
+theorem getElem?_replace_of_ne {xs : Vector α n} {i : Nat} (h : xs[i]? ≠ some a) :
+    (xs.replace a b)[i]? = xs[i]? := by
+  simp_all [getElem?_replace]
+
+theorem getElem_replace {xs : Vector α n} {i : Nat} (h : i < n) :
+    (xs.replace a b)[i] = if xs[i] == a then if a ∈ xs.take i then a else b else xs[i] := by
+  apply Option.some.inj
+  rw [← getElem?_eq_getElem, getElem?_replace]
+  split <;> split <;> simp_all
+
+theorem getElem_replace_of_ne {xs : Vector α n} {i : Nat} {h : i < n} (h' : xs[i] ≠ a) :
+    (xs.replace a b)[i]'(by simpa) = xs[i]'(h) := by
+  rw [getElem_replace h]
+  simp [h']
+
+theorem replace_append {xs : Vector α n} {ys : Vector α m} :
+    (xs ++ ys).replace a b = if a ∈ xs then xs.replace a b ++ ys else xs ++ ys.replace a b := by
+  rcases xs with ⟨xs, rfl⟩
+  rcases ys with ⟨ys, rfl⟩
+  simp only [mk_append_mk, replace_mk, eq_mk, Array.replace_append]
+  split <;> simp_all
+
+theorem replace_append_left {xs : Vector α n} {ys : Vector α m} (h : a ∈ xs) :
+    (xs ++ ys).replace a b = xs.replace a b ++ ys := by
+  simp [replace_append, h]
+
+theorem replace_append_right {xs : Vector α n} {ys : Vector α m} (h : ¬ a ∈ xs) :
+    (xs ++ ys).replace a b = xs ++ ys.replace a b := by
+  simp [replace_append, h]
+
+theorem replace_extract {xs : Vector α n} {i : Nat} :
+    (xs.extract 0 i).replace a b = (xs.replace a b).extract 0 i := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.replace_extract]
+
+@[simp] theorem replace_mkArray_self {a : α} (h : 0 < n) :
+    (mkVector n a).replace a b = (#v[b] ++ mkVector (n - 1) a).cast (by omega) := by
+  match n, h with
+  | n + 1, _ => simp_all [mkVector_succ', replace_append]
+
+@[simp] theorem replace_mkArray_ne {a b c : α} (h : !b == a) :
+    (mkVector n a).replace b c = mkVector n a := by
+  rw [replace_of_not_mem]
+  simp_all
+
+end replace
+
 /-! Content below this point has not yet been aligned with `List` and `Array`. -/
 
 set_option linter.indexVariables false in

src/Init/Data/Vector/Lex.lean

@@ -8,8 +8,8 @@ import Init.Data.Vector.Basic
 import Init.Data.Vector.Lemmas
 import Init.Data.Array.Lex.Lemmas
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Vector
 

src/Init/Data/Vector/MapIdx.lean

@@ -8,8 +8,8 @@ import Init.Data.Array.MapIdx
 import Init.Data.Vector.Attach
 import Init.Data.Vector.Lemmas
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Vector
 

src/Init/Data/Vector/Monadic.lean

@@ -13,8 +13,8 @@ import Init.Control.Lawful.Lemmas
 # Lemmas about `Vector.forIn'` and `Vector.forIn`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Vector
 

src/Init/Data/Vector/OfFn.lean

@@ -11,8 +11,8 @@ import Init.Data.Array.OfFn
 # Theorems about `Vector.ofFn`
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Vector
 

src/Init/Data/Vector/Range.lean

@@ -14,8 +14,8 @@ import Init.Data.Array.Range
 
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Vector
 

src/Init/Data/Vector/Zip.lean

@@ -11,8 +11,8 @@ import Init.Data.Vector.Lemmas
 # Lemmas about `Vector.zip`, `Vector.zipWith`, `Vector.zipWithAll`, and `Vector.unzip`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Vector
 

src/Lean/Linter/List.lean

@@ -237,20 +237,23 @@ def listVariablesLinter : Linter
           if let .str _ n := n then
           let n := stripBinderName n
           if !allowedListNames.contains n then
-            unless (ty.getArg! 0).isAppOf `List && (n == "L" || n == "xss") do
+            -- Allow `L` or `xss` for `List (List α)` or `List (Array α)`
+            unless ((ty.getArg! 0).isAppOf `List || (ty.getArg! 0).isAppOf `Array) && (n == "L" || n == "xss") do
               Linter.logLint linter.listVariables stx
                 m!"Forbidden variable appearing as a `List` name: {n}"
         for (stx, n, ty) in binders.filter fun (_, _, ty) => ty.isAppOf `Array do
           if let .str _ n := n then
           let n := stripBinderName n
           if !allowedArrayNames.contains n then
-            unless (ty.getArg! 0).isAppOf `Array && n == "xss" do
+            -- Allow `xss` for `Array (Array α)` or `Array (Vector α)`
+            unless ((ty.getArg! 0).isAppOf `Array || (ty.getArg! 0).isAppOf `Vector) && n == "xss" do
               Linter.logLint linter.listVariables stx
                 m!"Forbidden variable appearing as a `Array` name: {n}"
         for (stx, n, ty) in binders.filter fun (_, _, ty) => ty.isAppOf `Vector do
           if let .str _ n := n then
           let n := stripBinderName n
           if !allowedVectorNames.contains n then
+            -- Allow `xss` for `Vector (Vector α)`
             unless (ty.getArg! 0).isAppOf `Vector && n == "xss" do
               Linter.logLint linter.listVariables stx
                 m!"Forbidden variable appearing as a `Vector` name: {n}"

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

@@ -20,6 +20,8 @@ namespace Lean
 builtin_initialize registerTraceClass `grind.cutsat
 builtin_initialize registerTraceClass `grind.cutsat.subst
 builtin_initialize registerTraceClass `grind.cutsat.eq
+builtin_initialize registerTraceClass `grind.cutsat.eq.unsat (inherited := true)
+builtin_initialize registerTraceClass `grind.cutsat.eq.trivial (inherited := true)
 builtin_initialize registerTraceClass `grind.cutsat.assert
 builtin_initialize registerTraceClass `grind.cutsat.assert.dvd
 builtin_initialize registerTraceClass `grind.cutsat.dvd

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

@@ -26,51 +26,67 @@ def DvdCnstr.norm (c : DvdCnstr) : GoalM DvdCnstr := do
   else
     return c
 
+/--
+Given an equation `c₁` containing the monomial `a*x`, and a divisibility constraint `c₂`
+containing the monomial `b*x`, eliminate `x` by applying substitution.
+-/
+def DvdCnstr.applyEq (a : Int) (x : Var) (c₁ : EqCnstr) (b : Int) (c₂ : DvdCnstr) : GoalM DvdCnstr := do
+  let p := c₁.p
+  let q := c₂.p
+  let d := Int.ofNat (a * c₂.d).natAbs
+  let p := (q.mul a |>.combine (p.mul (-b)))
+  trace[grind.cutsat.subst] "{← getVar x}, {← c₁.pp}, {← c₂.pp}"
+  mkDvdCnstr d p (.subst x c₁ c₂)
+
+partial def DvdCnstr.applySubsts (c : DvdCnstr) : GoalM DvdCnstr := withIncRecDepth do
+  let some (b, x, c₁) ← c.p.findVarToSubst | return c
+  let a := c₁.p.coeff x
+  let c ← c.applyEq a x c₁ b
+  applySubsts c
+
 /-- Asserts divisibility constraint. -/
 partial def DvdCnstr.assert (c : DvdCnstr) : GoalM Unit := withIncRecDepth do
-  if (← isInconsistent) then return ()
+  if (← inconsistent) then return ()
   let c ← c.norm
+  let c ← c.applySubsts
   if c.isUnsat then
-    trace[grind.cutsat.dvd.unsat] "{← c.pp}"
-    let hf ← withProofContext do
-      return mkApp5 (mkConst ``Int.Linear.dvd_unsat) (← getContext) (toExpr c.d) (toExpr c.p) reflBoolTrue (← c.toExprProof)
-    closeGoal hf
-  else if c.isTrivial then
+    setInconsistent (.dvd c)
+    return ()
+  if c.isTrivial then
     trace[grind.cutsat.dvd.trivial] "{← c.pp}"
     return ()
+  let d₁ := c.d
+  let .add a₁ x p₁ := c.p | c.throwUnexpected
+  if (← c.satisfied) == .false then
+    resetAssignmentFrom x
+  if let some c' := (← get').dvdCnstrs[x]! then
+    trace[grind.cutsat.dvd.solve] "{← c.pp}, {← c'.pp}"
+    let d₂ := c'.d
+    let .add a₂ _ p₂ := c'.p | c'.throwUnexpected
+    let (d, α, β) := gcdExt (a₁*d₂) (a₂*d₁)
+    /-
+    We have that
+    `d = α*a₁*d₂ + β*a₂*d₁`
+    `d = gcd (a₁*d₂) (a₂*d₁)`
+    and two implied divisibility constraints:
+    - `d₁*d₂ ∣ d*x + α*d₂*p₁ + β*d₁*p₂`
+    - `d ∣ a₂*p₁ - a₁*p₂`
+    -/
+    let α_d₂_p₁ := p₁.mul (α*d₂)
+    let β_d₁_p₂ := p₂.mul (β*d₁)
+    let combine ← mkDvdCnstr (d₁*d₂) (.add d x (α_d₂_p₁.combine β_d₁_p₂)) (.solveCombine c c')
+    trace[grind.cutsat.dvd.solve.combine] "{← combine.pp}"
+    modify' fun s => { s with dvdCnstrs := s.dvdCnstrs.set x none}
+    combine.assert
+    let a₂_p₁ := p₁.mul a₂
+    let a₁_p₂ := p₂.mul (-a₁)
+    let elim ← mkDvdCnstr d (a₂_p₁.combine a₁_p₂) (.solveElim c c')
+    trace[grind.cutsat.dvd.solve.elim] "{← elim.pp}"
+    elim.assert
   else
-    let d₁ := c.d
-    let .add a₁ x p₁ := c.p | c.throwUnexpected
-    if (← c.satisfied) == .false then
-      resetAssignmentFrom x
-    if let some c' := (← get').dvdCnstrs[x]! then
-      trace[grind.cutsat.dvd.solve] "{← c.pp}, {← c'.pp}"
-      let d₂ := c'.d
-      let .add a₂ _ p₂ := c'.p | c'.throwUnexpected
-      let (d, α, β) := gcdExt (a₁*d₂) (a₂*d₁)
-      /-
-      We have that
-      `d = α*a₁*d₂ + β*a₂*d₁`
-      `d = gcd (a₁*d₂) (a₂*d₁)`
-      and two implied divisibility constraints:
-      - `d₁*d₂ ∣ d*x + α*d₂*p₁ + β*d₁*p₂`
-      - `d ∣ a₂*p₁ - a₁*p₂`
-      -/
-      let α_d₂_p₁ := p₁.mul (α*d₂)
-      let β_d₁_p₂ := p₂.mul (β*d₁)
-      let combine ← mkDvdCnstr (d₁*d₂) (.add d x (α_d₂_p₁.combine β_d₁_p₂)) (.solveCombine c c')
-      trace[grind.cutsat.dvd.solve.combine] "{← combine.pp}"
-      modify' fun s => { s with dvdCnstrs := s.dvdCnstrs.set x none}
-      combine.assert
-      let a₂_p₁ := p₁.mul a₂
-      let a₁_p₂ := p₂.mul (-a₁)
-      let elim ← mkDvdCnstr d (a₂_p₁.combine a₁_p₂) (.solveElim c c')
-      trace[grind.cutsat.dvd.solve.elim] "{← elim.pp}"
-      elim.assert
-    else
-      trace[grind.cutsat.dvd.update] "{← c.pp}"
-      c.p.updateOccs
-      modify' fun s => { s with dvdCnstrs := s.dvdCnstrs.set x (some c) }
+    trace[grind.cutsat.dvd.update] "{← c.pp}"
+    c.p.updateOccs
+    modify' fun s => { s with dvdCnstrs := s.dvdCnstrs.set x (some c) }
 
 builtin_grind_propagator propagateDvd ↓Dvd.dvd := fun e => do
   let_expr Dvd.dvd _ inst a b ← e | return ()

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

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr
 
 namespace Lean.Meta.Grind.Arith.Cutsat
 
@@ -37,20 +38,7 @@ where
         else
           go k x 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_.Int.Linear.Poly.findVarToSubst (p : Poly) : GoalM (Option (Int × Var × EqCnstr)) := do
-  match p with
-  | .num _ => return none
-  | .add k x p =>
-    if let some c := (← get').elimEqs[x]! then
-      return some (k, x, c)
-    else
-      findVarToSubst p
-
-partial def applySubsts (c : EqCnstr) : GoalM EqCnstr := do
+partial def EqCnstr.applySubsts (c : EqCnstr) : GoalM EqCnstr := withIncRecDepth do
   let some (a, x, c₁) ← c.p.findVarToSubst | return c
   trace[grind.cutsat.subst] "{← getVar x}, {← c.pp}, {← c₁.pp}"
   let b := c₁.p.coeff x
@@ -58,16 +46,88 @@ partial def applySubsts (c : EqCnstr) : GoalM EqCnstr := do
   let c ← mkEqCnstr p (.subst x c₁ c)
   applySubsts c
 
+private def updateDvdCnstr (a : Int) (x : Var) (c : EqCnstr) (y : Var) : GoalM Unit := do
+  let some c' := (← get').dvdCnstrs[y]! | return ()
+  let b := c'.p.coeff x
+  if b == 0 then return ()
+  modify' fun s => { s with dvdCnstrs := s.dvdCnstrs.set y none }
+  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)
+
+/--
+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 : Int) (x : Var) (c₁ : EqCnstr) (todo : Array (Int × LeCnstr)) : GoalM Unit := do
+  for (b, c₂) in todo do
+    let c₂ ← c₂.applyEq a x c₁ b
+    c₂.assert
+    if (← inconsistent) then return ()
+
+/--
+Given an equation `c₁` containing `a*x`, eliminate `x` from lower bound inequalities of `y`.
+-/
+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]!
+  modify' 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 : Int) (x : Var) (c : EqCnstr) (y : Var) : GoalM Unit := do
+  if (← inconsistent) then return ()
+  let (uppers', todo) ← split x (← get').uppers[y]!
+  modify' fun s => { s with uppers := s.uppers.set y uppers' }
+  updateLeCnstrs a x c todo
+
+private def updateOccsAt (k : Int) (x : Var) (c : EqCnstr) (y : Var) : GoalM Unit := do
+  updateDvdCnstr k x c y
+  updateLowers k x c y
+  updateUppers k x c y
+
+private def updateOccs (k : Int) (x : Var) (c : EqCnstr) : GoalM Unit := do
+  let ys := (← get').occurs[x]!
+  modify' fun s => { s with occurs := s.occurs.set x {} }
+  updateOccsAt k x c x
+  for y in ys do
+    updateOccsAt k x c y
+
 def EqCnstr.assert (c : EqCnstr) : GoalM Unit := do
-  if (← isInconsistent) then return ()
+  if (← inconsistent) then return ()
   trace[grind.cutsat.assert] "{← c.pp}"
   let c ← c.norm
-  let c ← applySubsts c
-  -- TODO: check coeffsr
+  let c ← c.applySubsts
+  if c.p.isUnsatEq then
+    setInconsistent (.eq c)
+    return ()
+  if c.isTrivial then
+    trace[grind.cutsat.le.trivial] "{← c.pp}"
+    return ()
+  let k := c.p.gcdCoeffs'
+  if c.p.getConst % k > 0 then
+    setInconsistent (.eq c)
+    return ()
+  let c ← if k == 1 then
+    pure c
+  else
+    mkEqCnstr (c.p.div k) (.divCoeffs c)
   trace[grind.cutsat.eq] "{← c.pp}"
   let some (k, x) := c.p.pickVarToElim? | c.throwUnexpected
-  -- TODO: eliminate `x` from lowers, uppers, and dvdCnstrs
-  -- TODO: reset `x`s occurrences
+  updateOccs k x c
+  if (← inconsistent) then return ()
   -- assert a divisibility constraint IF `|k| != 1`
   if k.natAbs != 1 then
     let p := c.p.insert (-k) x
@@ -79,21 +139,36 @@ def EqCnstr.assert (c : EqCnstr) : GoalM Unit := do
     elimStack := x :: s.elimStack
   }
 
+private def exprAsPoly (a : Expr) : GoalM Poly := do
+  if let some p := (← get').terms.find? { expr := a } then
+    return p
+  else if let some var := (← get').varMap.find? { expr := a } then
+    return .add 1 var (.num 0)
+  else if let some k ← getIntValue? a then
+    return .num k
+  else
+    throwError "internal `grind` error, expression is not relevant to cutsat{indentExpr a}"
+
 @[export lean_process_cutsat_eq]
 def processNewEqImpl (a b : Expr) : GoalM Unit := do
-  trace[grind.cutsat.eq] "{mkIntEq a b}"
-  -- TODO
-  return ()
+  let p₁ ← exprAsPoly a
+  let p₂ ← exprAsPoly b
+  let p := p₁.combine (p₂.mul (-1))
+  let c ← mkEqCnstr p (.core p₁ p₂ (← mkEqProof a b))
+  c.assert
 
 @[export lean_process_new_cutsat_lit]
 def processNewEqLitImpl (a ke : Expr) : GoalM Unit := do
   let some k ← getIntValue? ke | return ()
-  let some p := (← get').terms.find? { expr := a } | return ()
-  if k == 0 then
-    (← mkEqCnstr p (.expr (← mkEqProof a ke))).assert
+  let p₁ ← exprAsPoly a
+  let h ← mkEqProof a ke
+  let c ← if k == 0 then
+    mkEqCnstr p₁ (.expr h)
   else
-    -- TODO
-    return ()
+    let p₂ ← exprAsPoly ke
+    let p := p₁.combine (p₂.mul (-1))
+    mkEqCnstr p (.core p₁ p₂ h)
+  c.assert
 
 /-- Different kinds of terms internalized by this module. -/
 private inductive SupportedTermKind where

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

@@ -33,8 +33,9 @@ def _root_.Int.Linear.Poly.checkOccs (p : Poly) : GoalM Unit := do
 def _root_.Int.Linear.Poly.checkCnstrOf (p : Poly) (x : Var) : GoalM Unit := do
   assert! p.isSorted
   assert! p.checkCoeffs
-  p.checkNoElimVars
-  p.checkOccs
+  unless (← inconsistent) do
+    p.checkNoElimVars
+    p.checkOccs
   let .add _ y _ := p | unreachable!
   assert! x == y
 

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

@@ -25,28 +25,47 @@ def LeCnstr.norm (c : LeCnstr) : GoalM LeCnstr := do
   else
     return c
 
-def LeCnstr.assert (c : LeCnstr) : GoalM Unit := do
-  if (← isInconsistent) then return ()
-  let c ← c.norm
-  if c.isUnsat then
-    trace[grind.cutsat.le.unsat] "{← c.pp}"
-    let hf ← withProofContext do
-      return mkApp4 (mkConst ``Int.Linear.le_unsat) (← getContext) (toExpr c.p) reflBoolTrue (← c.toExprProof)
-    closeGoal hf
-  else if c.isTrivial then
-    trace[grind.cutsat.le.trivial] "{← c.pp}"
+/--
+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 LeCnstr.applyEq (a : Int) (x : Var) (c₁ : EqCnstr) (b : Int) (c₂ : LeCnstr) : GoalM LeCnstr := do
+  let p := c₁.p
+  let q := c₂.p
+  let p := if a ≥ 0 then
+    q.mul a |>.combine (p.mul (-b))
   else
-    let .add a x _ := c.p | c.throwUnexpected
-    if a < 0 then
-      trace[grind.cutsat.le.lower] "{← c.pp}"
-      c.p.updateOccs
-      modify' fun s => { s with lowers := s.lowers.modify x (·.push c) }
-    else
-      trace[grind.cutsat.le.upper] "{← c.pp}"
-      c.p.updateOccs
-      modify' fun s => { s with uppers := s.uppers.modify x (·.push c) }
-    if (← c.satisfied) == .false then
-      resetAssignmentFrom x
+    p.mul b |>.combine (q.mul (-a))
+  trace[grind.cutsat.subst] "{← getVar x}, {← c₁.pp}, {← c₂.pp}"
+  mkLeCnstr p (.subst x c₁ c₂)
+
+partial def LeCnstr.applySubsts (c : LeCnstr) : GoalM LeCnstr := withIncRecDepth do
+  let some (b, x, c₁) ← c.p.findVarToSubst | return c
+  let a := c₁.p.coeff x
+  let c ← c.applyEq a x c₁ b
+  applySubsts c
+
+def LeCnstr.assert (c : LeCnstr) : GoalM Unit := do
+  if (← inconsistent) then return ()
+  let c ← c.norm
+  let c ← c.applySubsts
+  if c.isUnsat then
+    setInconsistent (.le c)
+    return ()
+  if c.isTrivial then
+    trace[grind.cutsat.le.trivial] "{← c.pp}"
+    return ()
+  let .add a x _ := c.p | c.throwUnexpected
+  if a < 0 then
+    trace[grind.cutsat.le.lower] "{← c.pp}"
+    c.p.updateOccs
+    modify' fun s => { s with lowers := s.lowers.modify x (·.push c) }
+  else
+    trace[grind.cutsat.le.upper] "{← c.pp}"
+    c.p.updateOccs
+    modify' fun s => { s with uppers := s.uppers.modify x (·.push c) }
+  if (← c.satisfied) == .false then
+    resetAssignmentFrom x
 
 private def reportNonNormalized (e : Expr) : GoalM Unit := do
   reportIssue! "unexpected non normalized inequality constraint found{indentExpr e}"

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

@@ -37,11 +37,14 @@ partial def DvdCnstr.toExprProof (c' : DvdCnstr) : ProofM Expr := c'.caching do
     return mkApp10 (mkConst ``Int.Linear.dvd_solve_elim)
       (← getContext) (toExpr c₁.d) (toExpr c₁.p) (toExpr c₂.d) (toExpr c₂.p) (toExpr c'.d) (toExpr c'.p)
       reflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
-  | .subst _x _c₁ _c₂ => throwError "NIY"
   | .ofEq x c =>
     return mkApp7 (mkConst ``Int.Linear.dvd_of_eq)
       (← getContext) (toExpr x) (toExpr c.p) (toExpr c'.d) (toExpr c'.p)
       reflBoolTrue (← c.toExprProof)
+  | .subst x c₁ c₂ =>
+    return mkApp10 (mkConst ``Int.Linear.eq_dvd_subst)
+      (← getContext) (toExpr x) (toExpr c₁.p) (toExpr c₂.d) (toExpr c₂.p) (toExpr c'.d) (toExpr c'.p)
+      reflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
 
 partial def LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr := c'.caching do
   match c'.h with
@@ -59,18 +62,51 @@ partial def LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr := c'.caching do
       (← getContext) (toExpr c₁.p) (toExpr c₂.p) (toExpr c'.p)
       reflBoolTrue
       (← c₁.toExprProof) (← c₂.toExprProof)
-  | .subst _x _c₁ _c₂ => throwError "NIY"
+  | .subst x c₁ c₂ =>
+    let a := c₁.p.coeff x
+    let thm := if a ≥ 0 then
+      mkConst ``Int.Linear.eq_le_subst_nonneg
+    else
+      mkConst ``Int.Linear.eq_le_subst_nonpos
+    return mkApp8 thm
+        (← getContext) (toExpr x) (toExpr c₁.p) (toExpr c₂.p) (toExpr c'.p)
+        reflBoolTrue
+        (← c₁.toExprProof) (← c₂.toExprProof)
 
 partial def EqCnstr.toExprProof (c' : EqCnstr) : ProofM Expr := c'.caching do
   match c'.h with
   | .expr h =>
     return h
+  | .core p₁ p₂ h =>
+    return mkApp6 (mkConst ``Int.Linear.eq_of_core) (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c'.p) reflBoolTrue h
   | .norm c =>
     return mkApp5 (mkConst ``Int.Linear.eq_norm) (← getContext) (toExpr c.p) (toExpr c'.p) reflBoolTrue (← c.toExprProof)
+  | .divCoeffs c =>
+    let k := c.p.gcdCoeffs c.p.getConst
+    return mkApp6 (mkConst ``Int.Linear.eq_coeff) (← getContext) (toExpr c.p) (toExpr c'.p) (toExpr k) reflBoolTrue (← c.toExprProof)
   | .subst x c₁ c₂  =>
     return mkApp8 (mkConst ``Int.Linear.eq_eq_subst)
       (← getContext) (toExpr x) (toExpr c₁.p) (toExpr c₂.p) (toExpr c'.p)
       reflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
 
 end
+
+def setInconsistent (h : UnsatProof) : GoalM Unit := do
+  let hf ← withProofContext do
+    match h with
+    | .le c =>
+      trace[grind.cutsat.le.unsat] "{← c.pp}"
+      return mkApp4 (mkConst ``Int.Linear.le_unsat) (← getContext) (toExpr c.p) reflBoolTrue (← c.toExprProof)
+    | .dvd c =>
+      trace[grind.cutsat.dvd.unsat] "{← c.pp}"
+      return mkApp5 (mkConst ``Int.Linear.dvd_unsat) (← getContext) (toExpr c.d) (toExpr c.p) reflBoolTrue (← c.toExprProof)
+    | .eq c =>
+      trace[grind.cutsat.eq.unsat] "{← c.pp}"
+      if c.p.isUnsatEq then
+        return mkApp4 (mkConst ``Int.Linear.eq_unsat) (← getContext) (toExpr c.p) reflBoolTrue (← c.toExprProof)
+      else
+        let k := c.p.gcdCoeffs'
+        return mkApp5 (mkConst ``Int.Linear.eq_unsat_coeff) (← getContext) (toExpr c.p) (toExpr (Int.ofNat k)) reflBoolTrue (← c.toExprProof)
+  closeGoal hf
+
 end Lean.Meta.Grind.Arith.Cutsat

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

@@ -145,7 +145,7 @@ def hasAssignment : GoalM Bool := do
 private def isDone : GoalM Bool := do
   if (← hasAssignment) then
     return true
-  if (← isInconsistent) then
+  if (← inconsistent) then
     return true
   return false
 

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

@@ -58,10 +58,23 @@ structure EqCnstr where
 
 inductive EqCnstrProof where
   | expr (h : Expr)
+  | core (p₁ p₂ : Poly) (h : Expr)
   | norm (c : EqCnstr)
+  | divCoeffs (c : EqCnstr)
   | subst (x : Var) (c₁ : EqCnstr) (c₂ : EqCnstr)
 end
 
+/--
+A proof of `False`.
+Remark: We will later add support for a backtraking search inside of cutsat.
+-/
+inductive UnsatProof where
+  | dvd (c : DvdCnstr)
+  | le (c : LeCnstr)
+  | eq (c : EqCnstr)
+
+abbrev VarSet := RBTree Var compare
+
 /-- State of the cutsat procedure. -/
 structure State where
   /-- Mapping from variables to their denotations. -/
@@ -102,7 +115,7 @@ structure State where
   If `x` occurs in `dvdCnstrs[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 (PHashSet Var) := {}
+  occurs : PArray VarSet := {}
   /-- Partial assignment being constructed by cutsat. -/
   assignment : PArray Int := {}
   /-- Next unique id for a constraint. -/

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

@@ -44,6 +44,12 @@ def get' : GoalM State := do
 @[inline] def modify' (f : State → State) : GoalM Unit := do
   modify fun s => { s with arith.cutsat := f s.arith.cutsat }
 
+/-- Returns `true` if the cutsat state is inconsistent. -/
+def inconsistent : GoalM Bool := do
+  -- TODO: we will have a nested backtracking search in cutsat
+  -- and this function will have to be refined.
+  isInconsistent
+
 def getVars : GoalM (PArray Expr) :=
   return (← get').vars
 
@@ -114,7 +120,7 @@ def LeCnstr.denoteExpr (c : LeCnstr) : GoalM Expr := do
 def LeCnstr.throwUnexpected (c : LeCnstr) : GoalM α := do
   throwError "`grind` internal error, unexpected{indentD (← c.pp)}"
 
-def EqCnstr.isTrivial (c : LeCnstr) : Bool :=
+def EqCnstr.isTrivial (c : EqCnstr) : Bool :=
   match c.p with
   | .num k => k == 0
   | _ => false
@@ -129,7 +135,7 @@ def EqCnstr.throwUnexpected (c : EqCnstr) : GoalM α := do
   throwError "`grind` internal error, unexpected{indentD (← c.pp)}"
 
 /-- Returns occurrences of `x`. -/
-def getOccursOf (x : Var) : GoalM (PHashSet Var) :=
+def getOccursOf (x : Var) : GoalM VarSet :=
   return (← get').occurs[x]!
 
 /--
@@ -225,4 +231,17 @@ Returns `.true` if `c` is satisfied by the current partial model,
 def LeCnstr.satisfied (c : LeCnstr) : GoalM LBool := do
   c.p.satisfiedLe
 
+/--
+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_.Int.Linear.Poly.findVarToSubst (p : Poly) : GoalM (Option (Int × Var × EqCnstr)) := do
+  match p with
+  | .num _ => return none
+  | .add k x p =>
+    if let some c := (← get').elimEqs[x]! then
+      return some (k, x, c)
+    else
+      findVarToSubst p
+
 end Lean.Meta.Grind.Arith.Cutsat

src/lake/Lake/Build/Fetch.lean

@@ -22,13 +22,14 @@ using the `fetch` function defined in this module.
 
 namespace Lake
 
-/-- The internal core monad of Lake builds. Not intended for user use. -/
+/-- The internal core monad of Lake builds. **Not intended for user use.** -/
+@[deprecated "Deprecated without replacement." (since := "2025-02-22")]
 abbrev CoreBuildM := BuildT LogIO
 
 /--
 A recursive build of a Lake build store that may encounter a cycle.
 
-An internal monad. Not intended for user use.
+An internal monad. **Not intended for user use.**
 -/
 abbrev RecBuildT (m : Type → Type) :=
   CallStackT BuildKey <| StateRefT' IO.RealWorld BuildStore <| BuildT m
@@ -43,18 +44,21 @@ instance [Monad m] [MonadError m] : MonadCycleOf BuildKey (RecBuildT m) where
 /--
 A recursive build of a Lake build store that may encounter a cycle.
 
-An internal monad. Not intended for user use.
+An internal monad. **Not intended for user use.**
 -/
 abbrev RecBuildM := RecBuildT LogIO
 
 /-- Run a recursive build. -/
-@[inline] def RecBuildM.run
-  (stack : CallStack BuildKey) (store : BuildStore) (build : RecBuildM α)
-: CoreBuildM (α × BuildStore) :=
+@[inline] def RecBuildT.run
+  [Monad m] [MonadLiftT (ST IO.RealWorld) m]
+  (stack : CallStack BuildKey) (store : BuildStore) (build : RecBuildT m α)
+: BuildT m (α × BuildStore) :=
   build stack |>.run store
 
 /-- Run a recursive build in a fresh build store. -/
-@[inline] def RecBuildM.run' (build : RecBuildM α) : CoreBuildM α := do
+@[inline] def RecBuildT.run'
+  [Monad m] [MonadLiftT (ST IO.RealWorld) m] (build : RecBuildT m α)
+: BuildT m α := do
   (·.1) <$> build.run {} {}
 
 /-- A build function for any element of the Lake build index. -/

src/lake/Lake/Build/Index.lean

@@ -77,10 +77,13 @@ def recBuildWithIndex : (info : BuildInfo) → FetchM (Job (BuildData info.key))
 | .dynlibExternLib lib =>
   mkTargetFacetBuild ExternLib.dynlibFacet lib.recComputeDynlib
 
+/-- Recursive build function with memoization. -/
+def recFetchWithIndex : (info : BuildInfo) → RecBuildM (Job (BuildData info.key)) :=
+ inline <| recFetchMemoize (β := (Job <| BuildData ·)) BuildInfo.key recBuildWithIndex
+
 /--
 Run a recursive Lake build using the Lake build index
 and a topological / suspending scheduler.
 -/
-def FetchM.run (x : FetchM α) : RecBuildM α :=
-  x <| inline <|
-    recFetchMemoize (β := (Job <| BuildData ·)) BuildInfo.key recBuildWithIndex
+@[inline] def FetchT.run (x : FetchT m α) : RecBuildT m α :=
+  x recFetchWithIndex

src/lake/Lake/Build/Job/Monad.lean

@@ -110,8 +110,8 @@ namespace Job
 
 /-- Spawn a job that asynchronously performs `act`. -/
 @[inline] protected def async
-  (act : JobM α) (prio := Task.Priority.default)
-: SpawnM (Job α) := fun fetch stack store ctx => .ofTask <$> do
+  (act : JobM α) (prio := Task.Priority.default) (caption := "")
+: SpawnM (Job α) := fun fetch stack store ctx => .ofTask (caption := caption) <$> do
   BaseIO.asTask (prio := prio) do (withLoggedIO act) fetch stack store ctx {}
 
 /-- Wait a the job to complete and return the result. -/

src/lake/Lake/Build/Job/Register.lean

@@ -32,13 +32,17 @@ def Job.renew (self : Job α) : Job α :=
 Registers the job for the top-level build monitor,
 (e.g., the Lake CLI progress UI), assigning it `caption`.
 -/
-def registerJob (caption : String) (job : Job α) (optional := false) : FetchM (Job α) := do
+@[inline] def registerJob
+  [Monad m] [MonadLiftT (ST IO.RealWorld) m] [MonadBuild m]
+  (caption : String) (job : Job α) (optional := false)
+: m (Job α) := do
   let job : Job α := {job with caption, optional}
   (← getBuildContext).registeredJobs.modify (·.push job)
   return job.renew
 
 /-- Wraps stray I/O, logs, and errors in `x` into the produced job.  -/
-def ensureJob (x : FetchM (Job α))
+def ensureJob
+  (x : FetchM (Job α))
 : FetchM (Job α) := fun fetch stack store ctx log => do
   let iniPos := log.endPos
   match (← (withLoggedIO x) fetch stack store ctx log) with

src/lake/Lake/Build/Run.lean

@@ -32,7 +32,7 @@ def Monitor.spinnerFrames :=
 
 /-- Context of the Lake build monitor. -/
 structure MonitorContext where
-  totalJobs : Nat
+  jobs : IO.Ref (Array OpaqueJob)
   out : IO.FS.Stream
   outLv : LogLevel
   failLv : LogLevel
@@ -45,7 +45,8 @@ structure MonitorContext where
 
 /-- State of the Lake build monitor. -/
 structure MonitorState where
-  jobNo : Nat := 1
+  jobNo : Nat := 0
+  totalJobs : Nat := 0
   failures : Array String
   resetCtrl : String
   lastUpdate : Nat
@@ -84,8 +85,8 @@ namespace Monitor
   flush (← read).out
 
 def renderProgress (running unfinished : Array OpaqueJob) (h : 0 < unfinished.size) : MonitorM PUnit := do
-  let {jobNo, ..} ← get
-  let {totalJobs, useAnsi, showProgress, ..} ← read
+  let {jobNo, totalJobs, ..} ← get
+  let {useAnsi, showProgress, ..} ← read
   if showProgress ∧ useAnsi then
     let spinnerIcon ← modifyGet fun s =>
         (spinnerFrames[s.spinnerIdx], {s with spinnerIdx := s.spinnerIdx + ⟨1, by decide⟩})
@@ -99,8 +100,8 @@ def renderProgress (running unfinished : Array OpaqueJob) (h : 0 < unfinished.si
     flush
 
 def reportJob (job : OpaqueJob) : MonitorM PUnit := do
-  let {jobNo, ..} ← get
-  let {totalJobs, failLv, outLv, showOptional, out, useAnsi, showProgress, minAction, ..} ← read
+  let {jobNo, totalJobs, ..} ← get
+  let {failLv, outLv, showOptional, out, useAnsi, showProgress, minAction, ..} ← read
   let {task, caption, optional} := job
   let {log, action, ..} := task.get.state
   let maxLv := log.maxLv
@@ -129,8 +130,10 @@ def reportJob (job : OpaqueJob) : MonitorM PUnit := do
       log.replay (logger := .stream out outLv useAnsi)
     flush
 
-def poll (jobs : Array OpaqueJob): MonitorM (Array OpaqueJob × Array OpaqueJob) := do
-  jobs.foldlM (init := (#[], #[])) fun (running, unfinished) job => do
+def poll (unfinished : Array OpaqueJob) : MonitorM (Array OpaqueJob × Array OpaqueJob) := do
+  let newJobs ← (← read).jobs.modifyGet ((·, #[]))
+  modify fun s => {s with totalJobs := s.totalJobs + newJobs.size}
+  let pollJobs := fun (running, unfinished) job => do
     match (← IO.getTaskState job.task) with
     | .finished =>
       reportJob job
@@ -140,6 +143,8 @@ def poll (jobs : Array OpaqueJob): MonitorM (Array OpaqueJob × Array OpaqueJob)
       return (running.push job, unfinished.push job)
     | .waiting =>
       return (running, unfinished.push job)
+  let r ← unfinished.foldlM pollJobs (#[], #[])
+  newJobs.foldlM pollJobs r
 
 def sleep : MonitorM PUnit := do
   let now ← IO.monoMsNow
@@ -150,15 +155,15 @@ def sleep : MonitorM PUnit := do
   let now ← IO.monoMsNow
   modify fun s => {s with lastUpdate := now}
 
-partial def loop (jobs : Array OpaqueJob) : MonitorM PUnit := do
-  let (running, unfinished) ← poll jobs
+partial def loop (unfinished : Array OpaqueJob) : MonitorM PUnit := do
+  let (running, unfinished) ← poll unfinished
   if h : 0 < unfinished.size then
     renderProgress running unfinished h
     sleep
     loop unfinished
 
-def main (jobs : Array OpaqueJob) : MonitorM PUnit := do
-  loop jobs
+def main (init : Array OpaqueJob) : MonitorM PUnit := do
+  loop init
   let resetCtrl ← modifyGet fun s => (s.resetCtrl, {s with resetCtrl := ""})
   unless resetCtrl.isEmpty do
     print resetCtrl
@@ -168,18 +173,18 @@ end Monitor
 
 /-- The job monitor function. An auxiliary definition for `runFetchM`. -/
 def monitorJobs
-  (jobs : Array OpaqueJob)
+  (initJobs : Array OpaqueJob)
+  (jobs : IO.Ref (Array OpaqueJob))
   (out : IO.FS.Stream)
   (failLv outLv : LogLevel)
   (minAction : JobAction)
   (showOptional useAnsi showProgress : Bool)
   (resetCtrl : String := "")
   (initFailures : Array String := #[])
-  (totalJobs := jobs.size)
   (updateFrequency := 100)
 : BaseIO (Array String) := do
   let ctx := {
-    totalJobs, out, failLv, outLv, minAction, showOptional
+    jobs, out, failLv, outLv, minAction, showOptional
     useAnsi, showProgress, updateFrequency
   }
   let s := {
@@ -187,7 +192,7 @@ def monitorJobs
     lastUpdate := ← IO.monoMsNow
     failures := initFailures
   }
-  let (_,s) ← Monitor.main jobs |>.run ctx s
+  let (_,s) ← Monitor.main initJobs |>.run ctx s
   return s.failures
 
 /--
@@ -204,41 +209,19 @@ def Workspace.runFetchM
   let outLv := cfg.outLv
   let failLv := cfg.failLv
   let showProgress := cfg.showProgress
-  let showAnsiProgress := showProgress ∧ useAnsi
   let ctx ← mkBuildContext ws cfg
   -- Job Computation
-  let caption := "Computing build jobs"
-  if showAnsiProgress then
-    print! out s!"⣿ [?/?] {caption}"
-    flush out
-  let (a?, log) ← ((withLoggedIO build).run.run'.run ctx).run?
-  let failed := log.hasEntries ∧ log.maxLv ≥ failLv
-  if failed ∨ (log.hasEntries ∧ log.maxLv ≥ outLv) then
-    let icon := log.maxLv.icon
-    let caption := s!"{icon} [?/?] {caption}"
-    if useAnsi then
-      let caption := Ansi.chalk log.maxLv.ansiColor caption
-      if showProgress then
-        print! out s!"{Ansi.resetLine}{caption}"
-      else
-        print! out caption
-    else
-      print! out caption
-    print! out "\n"
-    let outLv := if failed then .trace else outLv
-    log.replay (logger := .stream out outLv useAnsi)
-    flush out
-  let failures := if failed then #[caption] else #[]
+  let caption := "job computation"
+  let compute := Job.async build (caption := caption)
+  let job ← compute.run.run'.run ctx |>.run nilTrace
   -- Job Monitor
-  let jobs ← ctx.registeredJobs.get
-  let resetCtrl := if showAnsiProgress then Ansi.resetLine else ""
   let minAction := if cfg.verbosity = .verbose then .unknown else .fetch
   let showOptional := cfg.verbosity = .verbose
-  let failures ← monitorJobs jobs out failLv outLv minAction showOptional useAnsi showProgress
-    (resetCtrl := resetCtrl) (initFailures := failures)
+  let failures ← monitorJobs #[job] ctx.registeredJobs
+    out failLv outLv minAction showOptional useAnsi showProgress
   -- Failure Report
   if failures.isEmpty then
-    let some a := a?
+    let some a ← job.wait?
       | error "top-level build failed"
     return a
   else

src/stdlib.make.in

@@ -129,4 +129,4 @@ ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_D
 lean: ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}
 
 Leanc:
-	+"${LEAN_BIN}/leanmake" bin PKG=Leanc BIN_NAME=leanc${CMAKE_EXECUTABLE_SUFFIX} $(LEANMAKE_OPTS) LINK_OPTS='${CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE}' OUT="${CMAKE_BINARY_DIR}" OLEAN_OUT="${CMAKE_BINARY_DIR}"
+	+"${LEAN_BIN}/leanmake" bin PKG=Leanc BIN_NAME=leanc${CMAKE_EXECUTABLE_SUFFIX} $(LEANMAKE_OPTS) LINK_OPTS='${CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE}' OUT="${CMAKE_BINARY_DIR}" OLEAN_OUT="${CMAKE_BINARY_DIR}" LEAN_PATH="${CMAKE_LIBRARY_OUTPUT_DIRECTORY}"