feat: rename Array.mkArray to replicate

src/Init/Data/Array/Basic.lean

@@ -161,7 +161,10 @@ def pop (a : Array α) : Array α where
   | ⟨[]⟩ => rfl
   | ⟨a::as⟩ => simp [pop, Nat.succ_sub_succ_eq_sub, size]
 
-@[extern "lean_mk_array"]
+def replicate {α : Type u} (n : Nat) (v : α) : Array α where
+  toList := List.replicate n v
+
+@[extern "lean_mk_array", deprecated replicate (since := "2025-01-16")]
 def mkArray {α : Type u} (n : Nat) (v : α) : Array α where
   toList := List.replicate n v
 

src/Init/Data/Array/Find.lean

@@ -98,21 +98,26 @@ theorem back?_flatten {L : Array (Array α)} :
   cases L using array₂_induction
   simp [List.getLast?_flatten, ← List.map_reverse, List.findSome?_map, Function.comp_def]
 
-theorem findSome?_mkArray : findSome? f (mkArray n a) = if n = 0 then none else f a := by
+theorem findSome?_replicate : findSome? f (replicate n a) = if n = 0 then none else f a := by
   simp [← List.toArray_replicate, List.findSome?_replicate]
 
-@[simp] theorem findSome?_mkArray_of_pos (h : 0 < n) : findSome? f (mkArray n a) = f a := by
-  simp [findSome?_mkArray, Nat.ne_of_gt h]
+@[simp] theorem findSome?_replicate_of_pos (h : 0 < n) : findSome? f (replicate n a) = f a := by
+  simp [findSome?_replicate, Nat.ne_of_gt h]
 
 -- Argument is unused, but used to decide whether `simp` should unfold.
-@[simp] theorem findSome?_mkArray_of_isSome (_ : (f a).isSome) :
-   findSome? f (mkArray n a) = if n = 0 then none else f a := by
-  simp [findSome?_mkArray]
+@[simp] theorem findSome?_replicate_of_isSome (_ : (f a).isSome) :
+   findSome? f (replicate n a) = if n = 0 then none else f a := by
+  simp [findSome?_replicate]
 
-@[simp] theorem findSome?_mkArray_of_isNone (h : (f a).isNone) :
-    findSome? f (mkArray n a) = none := by
+@[simp] theorem findSome?_replicate_of_isNone (h : (f a).isNone) :
+    findSome? f (replicate n a) = none := by
   rw [Option.isNone_iff_eq_none] at h
-  simp [findSome?_mkArray, h]
+  simp [findSome?_replicate, h]
+
+@[deprecated findSome?_replicate (since := "2025-01-16")] abbrev findSome?_mkArray := @findSome?_replicate
+@[deprecated findSome?_replicate_of_pos (since := "2025-01-16")] abbrev findSome?_mkArray_of_pos := @findSome?_replicate_of_pos
+@[deprecated findSome?_replicate_of_isSome (since := "2025-01-16")] abbrev findSome?_mkArray_of_isSome := @findSome?_replicate_of_isSome
+@[deprecated findSome?_replicate_of_isNone (since := "2025-01-16")] abbrev findSome?_mkArray_of_isNone := @findSome?_replicate_of_isNone
 
 /-! ### find? -/
 
@@ -244,34 +249,42 @@ theorem find?_flatMap_eq_none {xs : Array α} {f : α → Array β} {p : β →
     (xs.flatMap f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y := by
   simp
 
-theorem find?_mkArray :
-    find? p (mkArray n a) = if n = 0 then none else if p a then some a else none := by
+theorem find?_replicate :
+    find? p (replicate n a) = if n = 0 then none else if p a then some a else none := by
   simp [← List.toArray_replicate, List.find?_replicate]
 
-@[simp] theorem find?_mkArray_of_length_pos (h : 0 < n) :
-    find? p (mkArray n a) = if p a then some a else none := by
-  simp [find?_mkArray, Nat.ne_of_gt h]
+@[simp] theorem find?_replicate_of_length_pos (h : 0 < n) :
+    find? p (replicate n a) = if p a then some a else none := by
+  simp [find?_replicate, Nat.ne_of_gt h]
 
-@[simp] theorem find?_mkArray_of_pos (h : p a) :
-    find? p (mkArray n a) = if n = 0 then none else some a := by
-  simp [find?_mkArray, h]
+@[simp] theorem find?_replicate_of_pos (h : p a) :
+    find? p (replicate n a) = if n = 0 then none else some a := by
+  simp [find?_replicate, h]
 
-@[simp] theorem find?_mkArray_of_neg (h : ¬ p a) : find? p (mkArray n a) = none := by
-  simp [find?_mkArray, h]
+@[simp] theorem find?_replicate_of_neg (h : ¬ p a) : find? p (replicate n a) = none := by
+  simp [find?_replicate, h]
 
 -- This isn't a `@[simp]` lemma since there is already a lemma for `l.find? p = none` for any `l`.
-theorem find?_mkArray_eq_none {n : Nat} {a : α} {p : α → Bool} :
-    (mkArray n a).find? p = none ↔ n = 0 ∨ !p a := by
+theorem find?_replicate_eq_none {n : Nat} {a : α} {p : α → Bool} :
+    (replicate n a).find? p = none ↔ n = 0 ∨ !p a := by
   simp [← List.toArray_replicate, List.find?_replicate_eq_none, Classical.or_iff_not_imp_left]
 
-@[simp] theorem find?_mkArray_eq_some {n : Nat} {a b : α} {p : α → Bool} :
-    (mkArray n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b := by
+@[simp] theorem find?_replicate_eq_some {n : Nat} {a b : α} {p : α → Bool} :
+    (replicate n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b := by
   simp [← List.toArray_replicate]
 
-@[simp] theorem get_find?_mkArray (n : Nat) (a : α) (p : α → Bool) (h) :
-    ((mkArray n a).find? p).get h = a := by
+@[simp] theorem get_find?_replicate (n : Nat) (a : α) (p : α → Bool) (h) :
+    ((replicate n a).find? p).get h = a := by
   simp [← List.toArray_replicate]
 
+@[deprecated find?_replicate (since := "2025-01-16")] abbrev find?_mkArray := @find?_replicate
+@[deprecated find?_replicate_of_length_pos (since := "2025-01-16")] abbrev find?_mkArray_of_length_pos := @find?_replicate_of_length_pos
+@[deprecated find?_replicate_of_pos (since := "2025-01-16")] abbrev find?_mkArray_of_pos := @find?_replicate_of_pos
+@[deprecated find?_replicate_of_neg (since := "2025-01-16")] abbrev find?_mkArray_of_neg := @find?_replicate_of_neg
+@[deprecated find?_replicate_eq_none (since := "2025-01-16")] abbrev find?_mkArray_eq_none := @find?_replicate_eq_none
+@[deprecated find?_replicate_eq_some (since := "2025-01-16")] abbrev find?_mkArray_eq_some := @find?_replicate_eq_some
+@[deprecated get_find?_mkArray (since := "2025-01-16")] abbrev get_find?_mkArray := @get_find?_replicate
+
 theorem find?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : Array α)
     (H : ∀ (a : α), a ∈ xs → P a) (p : β → Bool) :
     (xs.pmap f H).find? p = (xs.attach.find? (fun ⟨a, m⟩ => p (f a (H a m)))).map fun ⟨a, m⟩ => f a (H a m) := by

src/Init/Data/Array/Lemmas.lean

@@ -93,7 +93,7 @@ theorem size_eq_one {l : Array α} : l.size = 1 ↔ ∃ a, l = #[a] := by
 
 /-! ### push -/
 
-@[simp] theorem push_ne_empty {a : α} {xs : Array α} : xs.push a ≠ #[] := by
+theorem push_ne_empty {a : α} {xs : Array α} : xs.push a ≠ #[] := by
   cases xs
   simp
 
@@ -160,27 +160,38 @@ theorem exists_push_of_size_eq_add_one {xs : Array α} (h : xs.size = n + 1) :
 theorem singleton_inj : #[a] = #[b] ↔ a = b := by
   simp
 
-/-! ### mkArray -/
+/-! ### replicate -/
 
-@[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
+@[simp] theorem size_replicate (n : Nat) (v : α) : (replicate n v).size = n :=
   List.length_replicate ..
 
-@[simp] theorem toList_mkArray : (mkArray n a).toList = List.replicate n a := by
-  simp only [mkArray]
+@[simp] theorem toList_replicate : (replicate n a).toList = List.replicate n a := by
+  simp only [replicate]
 
-@[simp] theorem mkArray_zero : mkArray 0 a = #[] := rfl
+@[simp] theorem replicate_zero : replicate 0 a = #[] := rfl
 
-theorem mkArray_succ : mkArray (n + 1) a = (mkArray n a).push a := by
+theorem replicate_succ : replicate (n + 1) a = (replicate n a).push a := by
   apply toList_inj.1
   simp [List.replicate_succ']
 
-@[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) :
-    (mkArray n v)[i] = v := by simp [← getElem_toList]
+theorem replicate_inj : replicate n a = replicate m b ↔ n = m ∧ (n = 0 ∨ a = b) := by
+  rw [← List.replicate_inj, ← toList_inj]
+  simp
 
-theorem getElem?_mkArray (n : Nat) (v : α) (i : Nat) :
-    (mkArray n v)[i]? = if i < n then some v else none := by
+@[simp] theorem getElem_replicate (n : Nat) (v : α) (h : i < (replicate n v).size) :
+    (replicate n v)[i] = v := by simp [← getElem_toList]
+
+theorem getElem?_replicate (n : Nat) (v : α) (i : Nat) :
+    (replicate n v)[i]? = if i < n then some v else none := by
   simp [getElem?_def]
 
+@[deprecated size_replicate (since := "2025-01-16")] abbrev size_mkArray := @size_replicate
+@[deprecated replicate_zero (since := "2025-01-16")] abbrev replicate_mkArray_zero := @replicate_zero
+@[deprecated replicate_succ (since := "2025-01-16")] abbrev replicate_mkArray_succ := @replicate_succ
+@[deprecated replicate_inj (since := "2025-01-16")] abbrev replicate_mkArray_inj := @replicate_inj
+@[deprecated getElem_replicate (since := "2025-01-16")] abbrev getElem_mkArray := @getElem_replicate
+@[deprecated getElem?_replicate (since := "2025-01-16")] abbrev getElem?_mkArray := @getElem?_replicate
+
 /-! ## L[i] and L[i]? -/
 
 @[simp] theorem getElem?_eq_none_iff {a : Array α} : a[i]? = none ↔ a.size ≤ i := by
@@ -958,15 +969,17 @@ theorem size_eq_of_beq [BEq α] {xs ys : Array α} (h : xs == ys) : xs.size = ys
   cases ys
   simp [List.length_eq_of_beq (by simpa using h)]
 
-@[simp] theorem mkArray_beq_mkArray [BEq α] {a b : α} {n : Nat} :
-    (mkArray n a == mkArray n b) = (n == 0 || a == b) := by
+@[simp] theorem replicate_beq_replicate [BEq α] {a b : α} {n : Nat} :
+    (replicate n a == replicate n b) = (n == 0 || a == b) := by
   cases n with
   | zero => simp
   | succ n =>
-    rw [mkArray_succ, mkArray_succ, push_beq_push, mkArray_beq_mkArray]
+    rw [replicate_succ, replicate_succ, push_beq_push, replicate_beq_replicate]
     rw [Bool.eq_iff_iff]
     simp +contextual
 
+@[deprecated replicate_beq_replicate (since := "2025-01-16")] abbrev mkArray_beq_mkArray := @replicate_beq_replicate
+
 private theorem beq_of_beq_singleton [BEq α] {a b : α} : #[a] == #[b] → a == b := by
   intro h
   have : isEqv #[a] #[b] BEq.beq = true := h
@@ -2046,11 +2059,6 @@ theorem flatMap_toList (l : Array α) (f : α → List β) :
   rcases l with ⟨l⟩
   simp
 
-@[simp] theorem toList_flatMap (l : Array α) (f : α → Array β) :
-    (l.flatMap f).toList = l.toList.flatMap fun a => (f a).toList := by
-  rcases l with ⟨l⟩
-  simp
-
 @[simp] theorem flatMap_id (l : Array (Array α)) : l.flatMap id = l.flatten := by simp [flatMap_def]
 
 @[simp] theorem flatMap_id' (l : Array (Array α)) : l.flatMap (fun a => a) = l.flatten := by simp [flatMap_def]
@@ -2097,7 +2105,7 @@ theorem flatMap_singleton (f : α → Array β) (x : α) : #[x].flatMap f = f x
 theorem flatMap_assoc {α β} (l : Array α) (f : α → Array β) (g : β → Array γ) :
     (l.flatMap f).flatMap g = l.flatMap fun x => (f x).flatMap g := by
   rcases l with ⟨l⟩
-  simp [List.flatMap_assoc, ← toList_flatMap]
+  simp [List.flatMap_assoc, flatMap_toList]
 
 theorem map_flatMap (f : β → γ) (g : α → Array β) (l : Array α) :
      (l.flatMap g).map f = l.flatMap fun a => (g a).map f := by
@@ -2136,317 +2144,8 @@ theorem flatMap_eq_foldl (f : α → Array β) (l : Array α) :
     intro l'
     simp [ih ((l' ++ (f a).toList)), toArray_append]
 
-/-! ### mkArray -/
-
-@[simp] theorem mkArray_one : mkArray 1 a = #[a] := rfl
-
-/-- Variant of `mkArray_succ` that prepends `a` at the beginning of the array. -/
-theorem mkArray_succ' : mkArray (n + 1) a = #[a] ++ mkArray n a := by
-  apply Array.ext'
-  simp [List.replicate_succ]
-
-@[simp] theorem mem_mkArray {a b : α} {n} : b ∈ mkArray n a ↔ n ≠ 0 ∧ b = a := by
-  unfold mkArray
-  simp only [mem_toArray, List.mem_replicate]
-
-theorem eq_of_mem_mkArray {a b : α} {n} (h : b ∈ mkArray n a) : b = a := (mem_mkArray.1 h).2
-
-theorem forall_mem_mkArray {p : α → Prop} {a : α} {n} :
-    (∀ b, b ∈ mkArray n a → p b) ↔ n = 0 ∨ p a := by
-  cases n <;> simp [mem_mkArray]
-
-@[simp] theorem mkArray_succ_ne_empty (n : Nat) (a : α) : mkArray (n+1) a ≠ #[] := by
-  simp [mkArray_succ]
-
-@[simp] theorem mkArray_eq_empty_iff {n : Nat} (a : α) : mkArray n a = #[] ↔ n = 0 := by
-  cases n <;> simp
-
-@[simp] theorem getElem?_mkArray_of_lt {n : Nat} {m : Nat} (h : m < n) : (mkArray n a)[m]? = some a := by
-  simp [getElem?_mkArray, h]
-
-@[simp] theorem mkArray_inj : mkArray n a = mkArray m b ↔ n = m ∧ (n = 0 ∨ a = b) := by
-  rw [← toList_inj]
-  simp
-
-theorem eq_mkArray_of_mem {a : α} {l : Array α} (h : ∀ (b) (_ : b ∈ l), b = a) : l = mkArray l.size a := by
-  rw [← toList_inj]
-  simpa using List.eq_replicate_of_mem (by simpa using h)
-
-theorem eq_mkArray_iff {a : α} {n} {l : Array α} :
-    l = mkArray n a ↔ l.size = n ∧ ∀ (b) (_ : b ∈ l), b = a := by
-  rw [← toList_inj]
-  simpa using List.eq_replicate_iff (l := l.toList)
-
-theorem map_eq_mkArray_iff {l : Array α} {f : α → β} {b : β} :
-    l.map f = mkArray l.size b ↔ ∀ x ∈ l, f x = b := by
-  simp [eq_mkArray_iff]
-
-@[simp] theorem map_const (l : Array α) (b : β) : map (Function.const α b) l = mkArray l.size b :=
-  map_eq_mkArray_iff.mpr fun _ _ => rfl
-
-@[simp] theorem map_const_fun (x : β) : map (Function.const α x) = (mkArray ·.size x) := by
-  funext l
-  simp
-
-/-- Variant of `map_const` using a lambda rather than `Function.const`. -/
--- This can not be a `@[simp]` lemma because it would fire on every `List.map`.
-theorem map_const' (l : Array α) (b : β) : map (fun _ => b) l = mkArray l.size b :=
-  map_const l b
-
-@[simp] theorem set_mkArray_self : (mkArray n a).set i a h = mkArray n a := by
-  apply Array.ext'
-  simp
-
-@[simp] theorem setIfInBounds_mkArray_self : (mkArray n a).setIfInBounds i a = mkArray n a := by
-  apply Array.ext'
-  simp
-
-@[simp] theorem mkArray_append_mkArray : mkArray n a ++ mkArray m a = mkArray (n + m) a := by
-  apply Array.ext'
-  simp
-
-theorem append_eq_mkArray_iff {l₁ l₂ : Array α} {a : α} :
-    l₁ ++ l₂ = mkArray n a ↔
-      l₁.size + l₂.size = n ∧ l₁ = mkArray l₁.size a ∧ l₂ = mkArray l₂.size a := by
-  simp [← toList_inj, List.append_eq_replicate_iff]
-
-theorem mkArray_eq_append_iff {l₁ l₂ : Array α} {a : α} :
-    mkArray n a = l₁ ++ l₂ ↔
-      l₁.size + l₂.size = n ∧ l₁ = mkArray l₁.size a ∧ l₂ = mkArray l₂.size a := by
-  rw [eq_comm, append_eq_mkArray_iff]
-
-@[simp] theorem map_mkArray : (mkArray n a).map f = mkArray n (f a) := by
-  apply Array.ext'
-  simp
-
-theorem filter_mkArray (w : stop = n) :
-    (mkArray n a).filter p 0 stop = if p a then mkArray n a else #[] := by
-  apply Array.ext'
-  simp only [w, toList_filter', toList_mkArray, List.filter_replicate]
-  split <;> simp_all
-
-@[simp] theorem filter_mkArray_of_pos (w : stop = n) (h : p a) :
-    (mkArray n a).filter p 0 stop = mkArray n a := by
-  simp [filter_mkArray, h, w]
-
-@[simp] theorem filter_mkArray_of_neg (w : stop = n) (h : ¬ p a) :
-    (mkArray n a).filter p 0 stop = #[] := by
-  simp [filter_mkArray, h, w]
-
-theorem filterMap_mkArray {f : α → Option β} (w : stop = n := by simp) :
-    (mkArray n a).filterMap f 0 stop = match f a with | none => #[] | .some b => mkArray n b := by
-  apply Array.ext'
-  simp only [w, size_mkArray, toList_filterMap', toList_mkArray, List.filterMap_replicate]
-  split <;> simp_all
-
--- This is not a useful `simp` lemma because `b` is unknown.
-theorem filterMap_mkArray_of_some {f : α → Option β} (h : f a = some b) :
-    (mkArray n a).filterMap f = mkArray n b := by
-  simp [filterMap_mkArray, h]
-
-@[simp] theorem filterMap_mkArray_of_isSome {f : α → Option β} (h : (f a).isSome) :
-    (mkArray n a).filterMap f = mkArray n (Option.get _ h) := by
-  match w : f a, h with
-  | some b, _ => simp [filterMap_mkArray, h, w]
-
-@[simp] theorem filterMap_mkArray_of_none {f : α → Option β} (h : f a = none) :
-    (mkArray n a).filterMap f = #[] := by
-  simp [filterMap_mkArray, h]
-
-@[simp] theorem flatten_mkArray_empty : (mkArray n (#[] : Array α)).flatten = #[] := by
-  rw [← toList_inj]
-  simp
-
-@[simp] theorem flatten_mkArray_singleton : (mkArray n #[a]).flatten = mkArray n a := by
-  rw [← toList_inj]
-  simp
-
-@[simp] theorem flatten_mkArray_mkArray : (mkArray n (mkArray m a)).flatten = mkArray (n * m) a := by
-  rw [← toList_inj]
-  simp
-
-theorem flatMap_mkArray {β} (f : α → Array β) : (mkArray n a).flatMap f = (mkArray n (f a)).flatten := by
-  rw [← toList_inj]
-  simp [flatMap_toList, List.flatMap_replicate]
-
-@[simp] theorem isEmpty_mkArray : (mkArray n a).isEmpty = decide (n = 0) := by
-  rw [← List.toArray_replicate, List.isEmpty_toArray]
-  simp
-
-@[simp] theorem sum_mkArray_nat (n : Nat) (a : Nat) : (mkArray n a).sum = n * a := by
-  rw [← List.toArray_replicate, List.sum_toArray]
-  simp
-
-/-! ### Preliminaries about `swap` needed for `reverse`. -/
-
-theorem swap_def (a : Array α) (i j : Nat) (hi hj) :
-    a.swap i j hi hj = (a.set i a[j]).set j a[i] (by simpa using hj) := by
-  simp [swap]
-
-theorem getElem?_swap (a : Array α) (i j : Nat) (hi hj) (k : Nat) : (a.swap i j hi hj)[k]? =
-    if j = k then some a[i] else if i = k then some a[j] else a[k]? := by
-  simp [swap_def, getElem?_set]
-
-/-! ### reverse -/
-
-@[simp] theorem size_reverse (a : Array α) : a.reverse.size = a.size := by
-  let rec go (as : Array α) (i j) : (reverse.loop as i j).size = as.size := by
-    rw [reverse.loop]
-    if h : i < j then
-      simp [(go · (i+1) ⟨j-1, ·⟩), h]
-    else simp [h]
-    termination_by j - i
-  simp only [reverse]; split <;> simp [go]
-
-@[simp] theorem toList_reverse (a : Array α) : a.reverse.toList = a.toList.reverse := by
-  let rec go (as : Array α) (i j hj)
-      (h : i + j + 1 = a.size) (h₂ : as.size = a.size)
-      (H : ∀ k, as.toList[k]? = if i ≤ k ∧ k ≤ j then a.toList[k]? else a.toList.reverse[k]?)
-      (k : Nat) : (reverse.loop as i ⟨j, hj⟩).toList[k]? = a.toList.reverse[k]? := by
-    rw [reverse.loop]; dsimp only; split <;> rename_i h₁
-    · match j with | j+1 => ?_
-      simp only [Nat.add_sub_cancel]
-      rw [(go · (i+1) j)]
-      · rwa [Nat.add_right_comm i]
-      · simp [size_swap, h₂]
-      · intro k
-        rw [getElem?_toList, getElem?_swap]
-        simp only [H, ← getElem_toList, ← List.getElem?_eq_getElem, Nat.le_of_lt h₁,
-          ← getElem?_toList]
-        split <;> rename_i h₂
-        · simp only [← h₂, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, and_false]
-          exact (List.getElem?_reverse' (j+1) i (Eq.trans (by simp_arith) h)).symm
-        split <;> rename_i h₃
-        · simp only [← h₃, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, false_and]
-          exact (List.getElem?_reverse' i (j+1) (Eq.trans (by simp_arith) h)).symm
-        simp only [Nat.succ_le, Nat.lt_iff_le_and_ne.trans (and_iff_left h₃),
-          Nat.lt_succ.symm.trans (Nat.lt_iff_le_and_ne.trans (and_iff_left (Ne.symm h₂)))]
-    · rw [H]; split <;> rename_i h₂
-      · cases Nat.le_antisymm (Nat.not_lt.1 h₁) (Nat.le_trans h₂.1 h₂.2)
-        cases Nat.le_antisymm h₂.1 h₂.2
-        exact (List.getElem?_reverse' _ _ h).symm
-      · rfl
-    termination_by j - i
-  simp only [reverse]
-  split
-  · match a with | ⟨[]⟩ | ⟨[_]⟩ => rfl
-  · have := Nat.sub_add_cancel (Nat.le_of_not_le ‹_›)
-    refine List.ext_getElem? <| go _ _ _ _ (by simp [this]) rfl fun k => ?_
-    split
-    · rfl
-    · rename_i h
-      simp only [← show k < _ + 1 ↔ _ from Nat.lt_succ (n := a.size - 1), this, Nat.zero_le,
-        true_and, Nat.not_lt] at h
-      rw [List.getElem?_eq_none_iff.2 ‹_›, List.getElem?_eq_none_iff.2 (a.toList.length_reverse ▸ ‹_›)]
-
-@[simp] theorem _root_.List.reverse_toArray (l : List α) : l.toArray.reverse = l.reverse.toArray := by
-  apply ext'
-  simp only [toList_reverse]
-
-@[simp] theorem reverse_push (as : Array α) (a : α) : (as.push a).reverse = #[a] ++ as.reverse := by
-  cases as
-  simp
-
-@[simp] theorem mem_reverse {x : α} {as : Array α} : x ∈ as.reverse ↔ x ∈ as := by
-  cases as
-  simp
-
-@[simp] theorem getElem_reverse (as : Array α) (i : Nat) (hi : i < as.reverse.size) :
-    (as.reverse)[i] = as[as.size - 1 - i]'(by simp at hi; omega) := by
-  cases as
-  simp
-
-@[simp] theorem reverse_eq_empty_iff {xs : Array α} : xs.reverse = #[] ↔ xs = #[] := by
-  cases xs
-  simp
-
-theorem reverse_ne_empty_iff {xs : Array α} : xs.reverse ≠ #[] ↔ xs ≠ #[] :=
-  not_congr reverse_eq_empty_iff
-
-/-- Variant of `getElem?_reverse` with a hypothesis giving the linear relation between the indices. -/
-theorem getElem?_reverse' {l : Array α} (i j) (h : i + j + 1 = l.size) : l.reverse[i]? = l[j]? := by
-  rcases l with ⟨l⟩
-  simp at h
-  simp only [List.reverse_toArray, List.getElem?_toArray]
-  rw [List.getElem?_reverse' (l := l) _ _ h]
-
-@[simp]
-theorem getElem?_reverse {l : Array α} {i} (h : i < l.size) :
-    l.reverse[i]? = l[l.size - 1 - i]? := by
-  cases l
-  simp_all
-
-@[simp] theorem reverse_reverse (as : Array α) : as.reverse.reverse = as := by
-  cases as
-  simp
-
-theorem reverse_eq_iff {as bs : Array α} : as.reverse = bs ↔ as = bs.reverse := by
-  constructor <;> (rintro rfl; simp)
-
-@[simp] theorem reverse_inj {xs ys : Array α} : xs.reverse = ys.reverse ↔ xs = ys := by
-  simp [reverse_eq_iff]
-
-@[simp] theorem reverse_eq_push_iff {xs : Array α} {ys : Array α} {a : α} :
-    xs.reverse = ys.push a ↔ xs = #[a] ++ ys.reverse := by
-  rw [reverse_eq_iff, reverse_push]
-
-@[simp] theorem map_reverse (f : α → β) (l : Array α) : l.reverse.map f = (l.map f).reverse := by
-  cases l <;> simp [*]
-
-@[simp] theorem filter_reverse (p : α → Bool) (l : Array α) : (l.reverse.filter p) = (l.filter p).reverse := by
-  cases l
-  simp
-
-@[simp] theorem filterMap_reverse (f : α → Option β) (l : Array α) : (l.reverse.filterMap f) = (l.filterMap f).reverse := by
-  cases l
-  simp
-
-@[simp] theorem reverse_append (as bs : Array α) : (as ++ bs).reverse = bs.reverse ++ as.reverse := by
-  cases as
-  cases bs
-  simp
-
-@[simp] theorem reverse_eq_append_iff {xs ys zs : Array α} :
-    xs.reverse = ys ++ zs ↔ xs = zs.reverse ++ ys.reverse := by
-  cases xs
-  cases ys
-  cases zs
-  simp
-
-/-- Reversing a flatten is the same as reversing the order of parts and reversing all parts. -/
-theorem reverse_flatten (L : Array (Array α)) :
-    L.flatten.reverse = (L.map reverse).reverse.flatten := by
-  cases L using array₂_induction
-  simp [flatten_toArray, List.reverse_flatten, Function.comp_def]
-
-/-- Flattening a reverse is the same as reversing all parts and reversing the flattened result. -/
-theorem flatten_reverse (L : Array (Array α)) :
-    L.reverse.flatten = (L.map reverse).flatten.reverse := by
-  cases L using array₂_induction
-  simp [flatten_toArray, List.flatten_reverse, Function.comp_def]
-
-theorem reverse_flatMap {β} (l : Array α) (f : α → Array β) :
-    (l.flatMap f).reverse = l.reverse.flatMap (reverse ∘ f) := by
-  cases l
-  simp [List.reverse_flatMap, Function.comp_def]
-
-theorem flatMap_reverse {β} (l : Array α) (f : α → Array β) :
-    (l.reverse.flatMap f) = (l.flatMap (reverse ∘ f)).reverse := by
-  cases l
-  simp [List.flatMap_reverse, Function.comp_def]
-
-@[simp] theorem reverse_mkArray (n) (a : α) : reverse (mkArray n a) = mkArray n a := by
-  rw [← toList_inj]
-  simp
-
 /-! Content below this point has not yet been aligned with `List`. -/
 
-/-! ### sum -/
-
-theorem sum_eq_sum_toList [Add α] [Zero α] (as : Array α) : as.toList.sum = as.sum := by
-  cases as
-  simp [Array.sum, List.sum]
-
 -- This is a duplicate of `List.toArray_toList`.
 -- It's confusing to guess which namespace this theorem should live in,
 -- so we provide both.
@@ -2630,7 +2329,6 @@ theorem getElem?_push_eq (a : Array α) (x : α) : (a.push x)[a.size]? = some x
 
 @[deprecated getElem?_size (since := "2024-10-21")] abbrev get?_size := @getElem?_size
 
-@[deprecated getElem_set_self (since := "2025-01-17")]
 theorem get_set_eq (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
     (a.set i v h)[i]'(by simp [h]) = v := by
   simp only [set, ← getElem_toList, List.getElem_set_self]
@@ -2654,9 +2352,17 @@ theorem get_set (a : Array α) (i : Nat) (hi : i < a.size) (j : Nat) (hj : j < a
     (h : i ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
   simp only [set, ← getElem_toList, List.getElem_set_ne h]
 
+theorem swap_def (a : Array α) (i j : Nat) (hi hj) :
+    a.swap i j hi hj = (a.set i a[j]).set j a[i] (by simpa using hj) := by
+  simp [swap]
+
 @[simp] theorem toList_swap (a : Array α) (i j : Nat) (hi hj) :
     (a.swap i j hi hj).toList = (a.toList.set i a[j]).set j a[i] := by simp [swap_def]
 
+theorem getElem?_swap (a : Array α) (i j : Nat) (hi hj) (k : Nat) : (a.swap i j hi hj)[k]? =
+    if j = k then some a[i] else if i = k then some a[j] else a[k]? := by
+  simp [swap_def, get?_set]
+
 @[simp] theorem swapAt_def (a : Array α) (i : Nat) (v : α) (hi) :
     a.swapAt i v hi = (a[i], a.set i v) := rfl
 
@@ -2710,6 +2416,15 @@ theorem size_eq_length_toList (as : Array α) : as.size = as.toList.length := rf
 
 @[deprecated size_swapIfInBounds (since := "2024-11-24")] abbrev size_swap! := @size_swapIfInBounds
 
+@[simp] theorem size_reverse (a : Array α) : a.reverse.size = a.size := by
+  let rec go (as : Array α) (i j) : (reverse.loop as i j).size = as.size := by
+    rw [reverse.loop]
+    if h : i < j then
+      simp [(go · (i+1) ⟨j-1, ·⟩), h]
+    else simp [h]
+    termination_by j - i
+  simp only [reverse]; split <;> simp [go]
+
 @[simp] theorem size_range {n : Nat} : (range n).size = n := by
   induction n <;> simp [range]
 
@@ -2720,6 +2435,61 @@ theorem size_eq_length_toList (as : Array α) : as.size = as.toList.length := rf
 theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Array.range n)[x] = x := by
   simp [← getElem_toList]
 
+@[simp] theorem toList_reverse (a : Array α) : a.reverse.toList = a.toList.reverse := by
+  let rec go (as : Array α) (i j hj)
+      (h : i + j + 1 = a.size) (h₂ : as.size = a.size)
+      (H : ∀ k, as.toList[k]? = if i ≤ k ∧ k ≤ j then a.toList[k]? else a.toList.reverse[k]?)
+      (k : Nat) : (reverse.loop as i ⟨j, hj⟩).toList[k]? = a.toList.reverse[k]? := by
+    rw [reverse.loop]; dsimp only; split <;> rename_i h₁
+    · match j with | j+1 => ?_
+      simp only [Nat.add_sub_cancel]
+      rw [(go · (i+1) j)]
+      · rwa [Nat.add_right_comm i]
+      · simp [size_swap, h₂]
+      · intro k
+        rw [getElem?_toList, getElem?_swap]
+        simp only [H, ← getElem_toList, ← List.getElem?_eq_getElem, Nat.le_of_lt h₁,
+          ← getElem?_toList]
+        split <;> rename_i h₂
+        · simp only [← h₂, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, and_false]
+          exact (List.getElem?_reverse' (j+1) i (Eq.trans (by simp_arith) h)).symm
+        split <;> rename_i h₃
+        · simp only [← h₃, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, false_and]
+          exact (List.getElem?_reverse' i (j+1) (Eq.trans (by simp_arith) h)).symm
+        simp only [Nat.succ_le, Nat.lt_iff_le_and_ne.trans (and_iff_left h₃),
+          Nat.lt_succ.symm.trans (Nat.lt_iff_le_and_ne.trans (and_iff_left (Ne.symm h₂)))]
+    · rw [H]; split <;> rename_i h₂
+      · cases Nat.le_antisymm (Nat.not_lt.1 h₁) (Nat.le_trans h₂.1 h₂.2)
+        cases Nat.le_antisymm h₂.1 h₂.2
+        exact (List.getElem?_reverse' _ _ h).symm
+      · rfl
+    termination_by j - i
+  simp only [reverse]
+  split
+  · match a with | ⟨[]⟩ | ⟨[_]⟩ => rfl
+  · have := Nat.sub_add_cancel (Nat.le_of_not_le ‹_›)
+    refine List.ext_getElem? <| go _ _ _ _ (by simp [this]) rfl fun k => ?_
+    split
+    · rfl
+    · rename_i h
+      simp only [← show k < _ + 1 ↔ _ from Nat.lt_succ (n := a.size - 1), this, Nat.zero_le,
+        true_and, Nat.not_lt] at h
+      rw [List.getElem?_eq_none_iff.2 ‹_›, List.getElem?_eq_none_iff.2 (a.toList.length_reverse ▸ ‹_›)]
+
+end Array
+
+open Array
+
+namespace List
+
+@[simp] theorem reverse_toArray (l : List α) : l.toArray.reverse = l.reverse.toArray := by
+  apply ext'
+  simp only [toList_reverse]
+
+end List
+
+namespace Array
+
 /-! ### foldlM and foldrM -/
 
 theorem foldlM_append [Monad m] [LawfulMonad m] (f : β → α → m β) (b) (l l' : Array α) :
@@ -3415,6 +3185,65 @@ theorem foldr_map' (g : α → β) (f : α → α → α) (f' : β → β → β
   | nil => simp
   | cons xs xss ih => simp [ih]
 
+/-! ### sum -/
+
+theorem sum_eq_sum_toList [Add α] [Zero α] (as : Array α) : as.sum = as.toList.sum := by
+  cases as
+  simp [Array.sum, List.sum]
+
+/-! ### replicate -/
+
+theorem eq_replicate_of_mem {a : α} {l : Array α} (h : ∀ (b) (_ : b ∈ l), b = a) : l = replicate l.size a := by
+  rcases l with ⟨l⟩
+  have := List.eq_replicate_of_mem (by simpa using h)
+  rw [this]
+  simp
+
+theorem eq_replicate_iff {a : α} {n} {l : Array α} :
+    l = replicate n a ↔ l.size = n ∧ ∀ (b) (_ : b ∈ l), b = a := by
+  rcases l with ⟨l⟩
+  simp [← List.eq_replicate_iff, toArray_eq]
+
+theorem map_eq_replicate_iff {l : Array α} {f : α → β} {b : β} :
+    l.map f = replicate l.size b ↔ ∀ x ∈ l, f x = b := by
+  simp [eq_replicate_iff]
+
+@[simp] theorem mem_replicate (a : α) (n : Nat) : b ∈ replicate n a ↔ n ≠ 0 ∧ b = a := by
+  rw [replicate, mem_toArray]
+  simp
+
+@[simp] theorem map_const (l : Array α) (b : β) : map (Function.const α b) l = replicate l.size b :=
+  map_eq_replicate_iff.mpr fun _ _ => rfl
+
+@[simp] theorem map_const_fun (x : β) : map (Function.const α x) = (replicate ·.size x) := by
+  funext l
+  simp
+
+/-- Variant of `map_const` using a lambda rather than `Function.const`. -/
+-- This can not be a `@[simp]` lemma because it would fire on every `Array.map`.
+theorem map_const' (l : Array α) (b : β) : map (fun _ => b) l = replicate l.size b :=
+  map_const l b
+
+@[simp] theorem sum_replicate_nat (n : Nat) (a : Nat) : (replicate n a).sum = n * a := by
+  simp [sum_eq_sum_toList, List.sum_replicate_nat]
+
+@[deprecated eq_replicate_of_mem (since := "2025-01-16")] abbrev eq_mkArray_of_mem := @eq_replicate_of_mem
+@[deprecated eq_replicate_iff (since := "2025-01-16")] abbrev eq_mkArray_iff := @eq_replicate_iff
+@[deprecated map_eq_replicate_iff (since := "2025-01-16")] abbrev map_eq_mkArray_iff := @map_eq_replicate_iff
+@[deprecated mem_replicate (since := "2025-01-16")] abbrev mem_mkArray := @mem_replicate
+@[deprecated sum_replicate_nat (since := "2025-01-16")] abbrev sum_mkArray_nat := @sum_replicate_nat
+
+/-! ### reverse -/
+
+@[simp] theorem mem_reverse {x : α} {as : Array α} : x ∈ as.reverse ↔ x ∈ as := by
+  cases as
+  simp
+
+@[simp] theorem getElem_reverse (as : Array α) (i : Nat) (hi : i < as.reverse.size) :
+    (as.reverse)[i] = as[as.size - 1 - i]'(by simp at hi; omega) := by
+  cases as
+  simp [Array.getElem_reverse]
+
 /-! ### findSomeRevM?, findRevM?, findSomeRev?, findRev? -/
 
 @[simp] theorem findSomeRevM?_eq_findSomeM?_reverse

src/Init/Data/List/Lemmas.lean

@@ -2274,7 +2274,7 @@ theorem map_const' (l : List α) (b : β) : map (fun _ => b) l = replicate l.len
   · intro i h₁ h₂
     simp [getElem_set]
 
-@[simp] theorem replicate_append_replicate : replicate n a ++ replicate m a = replicate (n + m) a := by
+@[simp] theorem append_replicate_replicate : replicate n a ++ replicate m a = replicate (n + m) a := by
   rw [eq_replicate_iff]
   constructor
   · simp
@@ -2282,9 +2282,6 @@ theorem map_const' (l : List α) (b : β) : map (fun _ => b) l = replicate l.len
     simp only [mem_append, mem_replicate, ne_eq]
     rintro (⟨-, rfl⟩ | ⟨_, rfl⟩) <;> rfl
 
-@[deprecated replicate_append_replicate (since := "2025-01-16")]
-abbrev append_replicate_replicate := @replicate_append_replicate
-
 theorem append_eq_replicate_iff {l₁ l₂ : List α} {a : α} :
     l₁ ++ l₂ = replicate n a ↔
       l₁.length + l₂.length = n ∧ l₁ = replicate l₁.length a ∧ l₂ = replicate l₂.length a := by
@@ -2295,11 +2292,6 @@ theorem append_eq_replicate_iff {l₁ l₂ : List α} {a : α} :
 
 @[deprecated append_eq_replicate_iff (since := "2024-09-05")] abbrev append_eq_replicate := @append_eq_replicate_iff
 
-theorem replicate_eq_append_iff {l₁ l₂ : List α} {a : α} :
-    replicate n a = l₁ ++ l₂ ↔
-      l₁.length + l₂.length = n ∧ l₁ = replicate l₁.length a ∧ l₂ = replicate l₂.length a := by
-  rw [eq_comm, append_eq_replicate_iff]
-
 @[simp] theorem map_replicate : (replicate n a).map f = replicate n (f a) := by
   ext1 n
   simp only [getElem?_map, getElem?_replicate]
@@ -2351,7 +2343,7 @@ theorem filterMap_replicate_of_some {f : α → Option β} (h : f a = some b) :
   induction n with
   | zero => simp
   | succ n ih =>
-    simp only [replicate_succ, flatten_cons, ih, replicate_append_replicate, replicate_inj, or_true,
+    simp only [replicate_succ, flatten_cons, ih, append_replicate_replicate, replicate_inj, or_true,
       and_true, add_one_mul, Nat.add_comm]
 
 theorem flatMap_replicate {β} (f : α → List β) : (replicate n a).flatMap f = (replicate n (f a)).flatten := by

src/Init/Data/List/ToArray.lean

@@ -392,7 +392,7 @@ theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
   · simp
   · simp_all [List.set_eq_of_length_le]
 
-@[simp] theorem toArray_replicate (n : Nat) (v : α) : (List.replicate n v).toArray = mkArray n v := rfl
+@[simp] theorem toArray_replicate (n : Nat) (v : α) : (List.replicate n v).toArray = Array.replicate n v := rfl
 
 @[deprecated toArray_replicate (since := "2024-12-13")]
 abbrev _root_.Array.mkArray_eq_toArray_replicate := @toArray_replicate

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -711,32 +711,6 @@ theorem mul_add_lt_is_or {b : Nat} (b_lt : b < 2^i) (a : Nat) : 2^i * a + b = 2^
   rw [mod_two_eq_one_iff_testBit_zero, testBit_shiftLeft]
   simp
 
-theorem testBit_mul_two_pow (x i n : Nat) :
-    (x * 2 ^ n).testBit i = (decide (n ≤ i) && x.testBit (i - n)) := by
-  rw [← testBit_shiftLeft, shiftLeft_eq]
-
-theorem bitwise_mul_two_pow (of_false_false : f false false = false := by rfl) :
-    (bitwise f x y) * 2 ^ n = bitwise f (x * 2 ^ n) (y * 2 ^ n) := by
-  apply Nat.eq_of_testBit_eq
-  simp only [testBit_mul_two_pow, testBit_bitwise of_false_false, Bool.if_false_right]
-  intro i
-  by_cases hn : n ≤ i
-  · simp [hn]
-  · simp [hn, of_false_false]
-
-theorem shiftLeft_bitwise_distrib {a b : Nat} (of_false_false : f false false = false := by rfl) :
-    (bitwise f a b) <<< i = bitwise f (a <<< i) (b <<< i) := by
-  simp [shiftLeft_eq, bitwise_mul_two_pow of_false_false]
-
-theorem shiftLeft_and_distrib {a b : Nat} : (a &&& b) <<< i = a <<< i &&& b <<< i :=
-  shiftLeft_bitwise_distrib
-
-theorem shiftLeft_or_distrib {a b : Nat} : (a ||| b) <<< i = a <<< i ||| b <<< i :=
-  shiftLeft_bitwise_distrib
-
-theorem shiftLeft_xor_distrib {a b : Nat} : (a ^^^ b) <<< i = a <<< i ^^^ b <<< i :=
-  shiftLeft_bitwise_distrib
-
 @[simp] theorem decide_shiftRight_mod_two_eq_one :
     decide (x >>> i % 2 = 1) = x.testBit i := by
   simp only [testBit, one_and_eq_mod_two, mod_two_bne_zero]

src/Init/Data/Nat/Lemmas.lean

@@ -622,14 +622,6 @@ protected theorem pos_of_mul_pos_right {a b : Nat} (h : 0 < a * b) : 0 < a := by
     0 < a * b ↔ 0 < a :=
   ⟨Nat.pos_of_mul_pos_right, fun w => Nat.mul_pos w h⟩
 
-protected theorem pos_of_lt_mul_left {a b c : Nat} (h : a < b * c) : 0 < c := by
-  replace h : 0 < b * c := by omega
-  exact Nat.pos_of_mul_pos_left h
-
-protected theorem pos_of_lt_mul_right {a b c : Nat} (h : a < b * c) : 0 < b := by
-  replace h : 0 < b * c := by omega
-  exact Nat.pos_of_mul_pos_right h
-
 /-! ### div/mod -/
 
 theorem mod_two_eq_zero_or_one (n : Nat) : n % 2 = 0 ∨ n % 2 = 1 :=

src/Init/Data/Vector/Basic.lean

@@ -52,13 +52,15 @@ def elimAsList {motive : Vector α n → Sort u}
 @[inline] def mkEmpty (capacity : Nat) : Vector α 0 := ⟨.mkEmpty capacity, rfl⟩
 
 /-- Makes a vector of size `n` with all cells containing `v`. -/
-@[inline] def mkVector (n) (v : α) : Vector α n := ⟨mkArray n v, by simp⟩
+@[inline] def replicate (n) (v : α) : Vector α n := ⟨Array.replicate n v, by simp⟩
+
+@[deprecated replicate (since := "2025-01-16")] abbrev mkVector := @replicate
 
 /-- Returns a vector of size `1` with element `v`. -/
 @[inline] def singleton (v : α) : Vector α 1 := ⟨#[v], rfl⟩
 
 instance [Inhabited α] : Inhabited (Vector α n) where
-  default := mkVector n default
+  default := replicate n default
 
 /-- Get an element of a vector using a `Fin` index. -/
 @[inline] def get (v : Vector α n) (i : Fin n) : α :=

src/Init/Data/Vector/Lemmas.lean

@@ -269,7 +269,9 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
   cases v
   simp
 
-@[simp] theorem toArray_mkVector : (mkVector n a).toArray = mkArray n a := rfl
+@[simp] theorem toArray_replicate : (replicate n a).toArray = Array.replicate n a := rfl
+
+@[deprecated toArray_replicate (since := "2025-01-16")] abbrev toArray_mkVector := @toArray_replicate
 
 @[simp] theorem toArray_inj {v w : Vector α n} : v.toArray = w.toArray ↔ v = w := by
   cases v
@@ -389,7 +391,9 @@ theorem toList_swap (a : Vector α n) (i j) (hi hj) :
   cases v
   simp
 
-@[simp] theorem toList_mkVector : (mkVector n a).toList = List.replicate n a := rfl
+@[simp] theorem toList_replicate : (replicate n a).toList = List.replicate n a := rfl
+
+@[deprecated toList_replicate (since := "2025-01-16")] abbrev toList_mkVector := @toList_replicate
 
 theorem toList_inj {v w : Vector α n} : v.toList = w.toList ↔ v = w := by
   cases v
@@ -468,15 +472,19 @@ theorem exists_push {xs : Vector α (n + 1)} :
 theorem singleton_inj : #v[a] = #v[b] ↔ a = b := by
   simp
 
-/-! ### mkVector -/
+/-! ### replicate -/
 
-@[simp] theorem mkVector_zero : mkVector 0 a = #v[] := rfl
+@[simp] theorem replicate_zero : replicate 0 a = #v[] := rfl
 
-theorem mkVector_succ : mkVector (n + 1) a = (mkVector n a).push a := by
-  simp [mkVector, Array.mkArray_succ]
+theorem replicate_succ : replicate (n + 1) a = (replicate n a).push a := by
+  simp [replicate, Array.replicate_succ]
 
-@[simp] theorem mkVector_inj : mkVector n a = mkVector n b ↔ n = 0 ∨ a = b := by
-  simp [← toArray_inj, toArray_mkVector, Array.mkArray_inj]
+theorem replicate_inj : replicate n a = replicate n b ↔ n = 0 ∨ a = b := by
+  simp [← toArray_inj, toArray_replicate, Array.replicate_inj]
+
+@[deprecated replicate_zero (since := "2025-01-16")] abbrev mkVector_zero := @replicate_zero
+@[deprecated replicate_succ (since := "2025-01-16")] abbrev mkVector_succ := @replicate_succ
+@[deprecated replicate_inj (since := "2025-01-16")] abbrev mkVector_inj := @replicate_inj
 
 /-! ## L[i] and L[i]? -/
 
@@ -1005,15 +1013,17 @@ theorem mem_setIfInBounds (v : Vector α n) (i : Nat) (hi : i < n) (a : α) :
   cases w
   simp
 
-@[simp] theorem mkVector_beq_mkVector [BEq α] {a b : α} {n : Nat} :
-    (mkVector n a == mkVector n b) = (n == 0 || a == b) := by
+@[simp] theorem replicate_beq_replicate [BEq α] {a b : α} {n : Nat} :
+    (replicate n a == replicate n b) = (n == 0 || a == b) := by
   cases n with
   | zero => simp
   | succ n =>
-    rw [mkVector_succ, mkVector_succ, push_beq_push, mkVector_beq_mkVector]
+    rw [replicate_succ, replicate_succ, push_beq_push, replicate_beq_replicate]
     rw [Bool.eq_iff_iff]
     simp +contextual
 
+@[deprecated replicate_beq_replicate (since := "2025-01-16")] abbrev mkVector_beq_mkVector := @replicate_beq_replicate
+
 @[simp] theorem reflBEq_iff [BEq α] [NeZero n] : ReflBEq (Vector α n) ↔ ReflBEq α := by
   match n, NeZero.ne n with
   | n + 1, _ =>
@@ -1021,8 +1031,8 @@ theorem mem_setIfInBounds (v : Vector α n) (i : Nat) (hi : i < n) (a : α) :
     · intro h
       constructor
       intro a
-      suffices (mkVector (n + 1) a == mkVector (n + 1) a) = true by
-        rw [mkVector_succ, push_beq_push, Bool.and_eq_true] at this
+      suffices (replicate (n + 1) a == replicate (n + 1) a) = true by
+        rw [replicate_succ, push_beq_push, Bool.and_eq_true] at this
         exact this.2
       simp
     · intro h
@@ -1037,15 +1047,15 @@ theorem mem_setIfInBounds (v : Vector α n) (i : Nat) (hi : i < n) (a : α) :
     · intro h
       constructor
       · intro a b h
-        have := mkVector_inj (n := n+1) (a := a) (b := b)
+        have := replicate_inj (n := n+1) (a := a) (b := b)
         simp only [Nat.add_one_ne_zero, false_or] at this
         rw [← this]
         apply eq_of_beq
-        rw [mkVector_beq_mkVector]
+        rw [replicate_beq_replicate]
         simpa
       · intro a
-        suffices (mkVector (n + 1) a == mkVector (n + 1) a) = true by
-          rw [mkVector_beq_mkVector] at this
+        suffices (replicate (n + 1) a == replicate (n + 1) a) = true by
+          rw [replicate_beq_replicate] at this
           simpa
         simp
     · intro h
@@ -1131,8 +1141,8 @@ theorem map_inj [NeZero n] : map (n := n) f = map g ↔ f = g := by
   constructor
   · intro h
     ext a
-    replace h := congrFun h (mkVector n a)
-    simp only [mkVector, map_mk, mk.injEq, Array.map_inj_left, Array.mem_mkArray,  and_imp,
+    replace h := congrFun h (replicate n a)
+    simp only [replicate, map_mk, mk.injEq, Array.map_inj_left, Array.mem_replicate, and_imp,
       forall_eq_apply_imp_iff] at h
     exact h (NeZero.ne n)
   · intro h; subst h; rfl
@@ -1456,44 +1466,6 @@ theorem append_eq_map_iff {f : α → β} :
       mk (L.map toArray).flatten (by simp [Function.comp_def, Array.map_const', h]) := by
   simp [flatten]
 
-@[simp] theorem getElem_flatten (l : Vector (Vector β m) n) (i : Nat) (hi : i < n * m) :
-    l.flatten[i] =
-      haveI : i / m < n := by rwa [Nat.div_lt_iff_lt_mul (Nat.pos_of_lt_mul_left hi)]
-      haveI : i % m < m := Nat.mod_lt _ (Nat.pos_of_lt_mul_left hi)
-      l[i / m][i % m] := by
-  rcases l with ⟨⟨l⟩, rfl⟩
-  simp only [flatten_mk, List.map_toArray, getElem_mk, List.getElem_toArray, Array.flatten_toArray]
-  induction l generalizing i with
-  | nil => simp at hi
-  | cons a l ih =>
-    simp only [List.map_cons, List.map_map, List.flatten_cons]
-    by_cases h : i < m
-    · rw [List.getElem_append_left (by simpa)]
-      have h₁ : i / m = 0 := Nat.div_eq_of_lt h
-      have h₂ : i % m = i := Nat.mod_eq_of_lt h
-      simp [h₁, h₂]
-    · have h₁ : a.toList.length ≤ i := by simp; omega
-      rw [List.getElem_append_right h₁]
-      simp only [Array.length_toList, size_toArray]
-      specialize ih (i - m) (by simp_all [Nat.add_one_mul]; omega)
-      have h₂ : i / m = (i - m) / m + 1 := by
-        conv => lhs; rw [show i = i - m + m by omega]
-        rw [Nat.add_div_right]
-        exact Nat.pos_of_lt_mul_left hi
-      simp only [Array.length_toList, size_toArray] at h₁
-      have h₃ : (i - m) % m = i % m := (Nat.mod_eq_sub_mod h₁).symm
-      simp_all
-
-theorem getElem?_flatten (l : Vector (Vector β m) n) (i : Nat) :
-    l.flatten[i]? =
-      if hi : i < n * m then
-        haveI : i / m < n := by rwa [Nat.div_lt_iff_lt_mul (Nat.pos_of_lt_mul_left hi)]
-        haveI : i % m < m := Nat.mod_lt _ (Nat.pos_of_lt_mul_left hi)
-        some l[i / m][i % m]
-      else
-        none := by
-  simp [getElem?_def]
-
 @[simp] theorem flatten_singleton (l : Vector α n) : #v[l].flatten = l.cast (by simp) := by
   simp [flatten]
 
@@ -1580,23 +1552,6 @@ theorem flatMap_def (l : Vector α n) (f : α → Vector β m) : l.flatMap f = f
   rcases l with ⟨l, rfl⟩
   simp [Array.flatMap_def, Function.comp_def]
 
-@[simp] theorem getElem_flatMap (l : Vector α n) (f : α → Vector β m) (i : Nat) (hi : i < n * m) :
-    (l.flatMap f)[i] =
-      haveI : i / m < n := by rwa [Nat.div_lt_iff_lt_mul (Nat.pos_of_lt_mul_left hi)]
-      haveI : i % m < m := Nat.mod_lt _ (Nat.pos_of_lt_mul_left hi)
-      (f (l[i / m]))[i % m] := by
-  rw [flatMap_def, getElem_flatten, getElem_map]
-
-theorem getElem?_flatMap (l : Vector α n) (f : α → Vector β m) (i : Nat) :
-    (l.flatMap f)[i]? =
-      if hi : i < n * m then
-        haveI : i / m < n := by rwa [Nat.div_lt_iff_lt_mul (Nat.pos_of_lt_mul_left hi)]
-        haveI : i % m < m := Nat.mod_lt _ (Nat.pos_of_lt_mul_left hi)
-        some ((f (l[i / m]))[i % m])
-      else
-        none := by
-  simp [getElem?_def]
-
 @[simp] theorem flatMap_id (l : Vector (Vector α m) n) : l.flatMap id = l.flatten := by simp [flatMap_def]
 
 @[simp] theorem flatMap_id' (l : Vector (Vector α m) n) : l.flatMap (fun a => a) = l.flatten := by simp [flatMap_def]
@@ -1649,189 +1604,6 @@ theorem map_eq_flatMap {α β} (f : α → β) (l : Vector α n) :
   rcases l with ⟨l, rfl⟩
   simp [Array.map_eq_flatMap]
 
-/-! ### mkVector -/
-
-@[simp] theorem mkVector_one : mkVector 1 a = #v[a] := rfl
-
-/-- Variant of `mkVector_succ` that prepends `a` at the beginning of the vector. -/
-theorem mkVector_succ' : mkVector (n + 1) a = (#v[a] ++ mkVector n a).cast (by omega) := by
-  rw [← toArray_inj]
-  simp [Array.mkArray_succ']
-
-@[simp] theorem mem_mkVector {a b : α} {n} : b ∈ mkVector n a ↔ n ≠ 0 ∧ b = a := by
-  unfold mkVector
-  simp
-
-theorem eq_of_mem_mkVector {a b : α} {n} (h : b ∈ mkVector n a) : b = a := (mem_mkVector.1 h).2
-
-theorem forall_mem_mkVector {p : α → Prop} {a : α} {n} :
-    (∀ b, b ∈ mkVector n a → p b) ↔ n = 0 ∨ p a := by
-  cases n <;> simp [mem_mkVector]
-
-@[simp] theorem getElem_mkVector (a : α) (n i : Nat) (h : i < n) : (mkVector n a)[i] = a := by
-  simp [mkVector]
-
-theorem getElem?_mkVector (a : α) (n i : Nat) : (mkVector n a)[i]? = if i < n then some a else none := by
-  simp [getElem?_def]
-
-@[simp] theorem getElem?_mkVector_of_lt {n : Nat} {m : Nat} (h : m < n) : (mkVector n a)[m]? = some a := by
-  simp [getElem?_mkVector, h]
-
-theorem eq_mkVector_of_mem {a : α} {l : Vector α n} (h : ∀ (b) (_ : b ∈ l), b = a) : l = mkVector n a := by
-  rw [← toArray_inj]
-  simpa using Array.eq_mkArray_of_mem (l := l.toArray) (by simpa using h)
-
-theorem eq_mkVector_iff {a : α} {n} {l : Vector α n} :
-    l = mkVector n a ↔ ∀ (b) (_ : b ∈ l), b = a := by
-  rw [← toArray_inj]
-  simpa using Array.eq_mkArray_iff (l := l.toArray) (n := n)
-
-theorem map_eq_mkVector_iff {l : Vector α n} {f : α → β} {b : β} :
-    l.map f = mkVector n b ↔ ∀ x ∈ l, f x = b := by
-  simp [eq_mkVector_iff]
-
-@[simp] theorem map_const (l : Vector α n) (b : β) : map (Function.const α b) l = mkVector n b :=
-  map_eq_mkVector_iff.mpr fun _ _ => rfl
-
-@[simp] theorem map_const_fun (x : β) : map (n := n) (Function.const α x) = fun _ => mkVector n x := by
-  funext l
-  simp
-
-/-- Variant of `map_const` using a lambda rather than `Function.const`. -/
--- This can not be a `@[simp]` lemma because it would fire on every `List.map`.
-theorem map_const' (l : Vector α n) (b : β) : map (fun _ => b) l = mkVector n b :=
-  map_const l b
-
-@[simp] theorem set_mkVector_self : (mkVector n a).set i a h = mkVector n a := by
-  rw [← toArray_inj]
-  simp
-
-@[simp] theorem setIfInBounds_mkVector_self : (mkVector n a).setIfInBounds i a = mkVector n a := by
-  rw [← toArray_inj]
-  simp
-
-@[simp] theorem mkVector_append_mkVector : mkVector n a ++ mkVector m a = mkVector (n + m) a := by
-  rw [← toArray_inj]
-  simp
-
-theorem append_eq_mkVector_iff {l₁ : Vector α n} {l₂ : Vector α m} {a : α} :
-    l₁ ++ l₂ = mkVector (n + m) a ↔ l₁ = mkVector n a ∧ l₂ = mkVector m a := by
-  simp [← toArray_inj, Array.append_eq_mkArray_iff]
-
-theorem mkVector_eq_append_iff {l₁ : Vector α n} {l₂ : Vector α m} {a : α} :
-    mkVector (n + m) a = l₁ ++ l₂ ↔ l₁ = mkVector n a ∧ l₂ = mkVector m a := by
-  rw [eq_comm, append_eq_mkVector_iff]
-
-@[simp] theorem map_mkVector : (mkVector n a).map f = mkVector n (f a) := by
-  rw [← toArray_inj]
-  simp
-
-
-@[simp] theorem flatten_mkVector_empty : (mkVector n (#v[] : Vector α 0)).flatten = #v[] := by
-  rw [← toArray_inj]
-  simp
-
-@[simp] theorem flatten_mkVector_singleton : (mkVector n #v[a]).flatten = (mkVector n a).cast (by simp) := by
-  ext i h
-  simp [h]
-
-@[simp] theorem flatten_mkVector_mkVector : (mkVector n (mkVector m a)).flatten = mkVector (n * m) a := by
-  ext i h
-  simp [h]
-
-theorem flatMap_mkArray {β} (f : α → Vector β m) : (mkVector n a).flatMap f = (mkVector n (f a)).flatten := by
-  ext i h
-  simp [h]
-
-@[simp] theorem sum_mkArray_nat (n : Nat) (a : Nat) : (mkVector n a).sum = n * a := by
-  simp [toArray_mkVector]
-
-/-! ### reverse -/
-
-@[simp] theorem reverse_push (as : Vector α n) (a : α) :
-    (as.push a).reverse = (#v[a] ++ as.reverse).cast (by omega) := by
-  rcases as with ⟨as, rfl⟩
-  simp [Array.reverse_push]
-
-@[simp] theorem mem_reverse {x : α} {as : Vector α n} : x ∈ as.reverse ↔ x ∈ as := by
-  cases as
-  simp
-
-@[simp] theorem getElem_reverse (a : Vector α n) (i : Nat) (hi : i < n) :
-    (a.reverse)[i] = a[n - 1 - i] := by
-  rcases a with ⟨a, rfl⟩
-  simp
-
-/-- Variant of `getElem?_reverse` with a hypothesis giving the linear relation between the indices. -/
-theorem getElem?_reverse' {l : Vector α n} (i j) (h : i + j + 1 = n) : l.reverse[i]? = l[j]? := by
-  rcases l with ⟨l, rfl⟩
-  simpa using Array.getElem?_reverse' i j h
-
-@[simp]
-theorem getElem?_reverse {l : Vector α n} {i} (h : i < n) :
-    l.reverse[i]? = l[n - 1 - i]? := by
-  cases l
-  simp_all
-
-@[simp] theorem reverse_reverse (as : Vector α n) : as.reverse.reverse = as := by
-  rcases as with ⟨as, rfl⟩
-  simp [Array.reverse_reverse]
-
-theorem reverse_eq_iff {as bs : Vector α n} : as.reverse = bs ↔ as = bs.reverse := by
-  constructor <;> (rintro rfl; simp)
-
-@[simp] theorem reverse_inj {xs ys : Vector α n} : xs.reverse = ys.reverse ↔ xs = ys := by
-  simp [reverse_eq_iff]
-
-@[simp] theorem reverse_eq_push_iff {xs : Vector α (n + 1)} {ys : Vector α n} {a : α} :
-    xs.reverse = ys.push a ↔ xs = (#v[a] ++ ys.reverse).cast (by omega) := by
-  rcases xs with ⟨xs, h⟩
-  rcases ys with ⟨ys, rfl⟩
-  simp [Array.reverse_eq_push_iff]
-
-@[simp] theorem map_reverse (f : α → β) (l : Vector α n) : l.reverse.map f = (l.map f).reverse := by
-  rcases l with ⟨l, rfl⟩
-  simp [Array.map_reverse]
-
-@[simp] theorem reverse_append (as : Vector α n) (bs : Vector α m) :
-    (as ++ bs).reverse = (bs.reverse ++ as.reverse).cast (by omega) := by
-  rcases as with ⟨as, rfl⟩
-  rcases bs with ⟨bs, rfl⟩
-  simp [Array.reverse_append]
-
-@[simp] theorem reverse_eq_append_iff {xs : Vector α (n + m)} {ys : Vector α n} {zs : Vector α m} :
-    xs.reverse = ys ++ zs ↔ xs = (zs.reverse ++ ys.reverse).cast (by omega) := by
-  cases xs
-  cases ys
-  cases zs
-  simp
-
-/-- Reversing a flatten is the same as reversing the order of parts and reversing all parts. -/
-theorem reverse_flatten (L : Vector (Vector α m) n) :
-    L.flatten.reverse = (L.map reverse).reverse.flatten := by
-  cases L using vector₂_induction
-  simp [Array.reverse_flatten]
-
-/-- Flattening a reverse is the same as reversing all parts and reversing the flattened result. -/
-theorem flatten_reverse (L : Vector (Vector α m) n) :
-    L.reverse.flatten = (L.map reverse).flatten.reverse := by
-  cases L using vector₂_induction
-  simp [Array.flatten_reverse]
-
-theorem reverse_flatMap {β} (l : Vector α n) (f : α → Vector β m) :
-    (l.flatMap f).reverse = l.reverse.flatMap (reverse ∘ f) := by
-  rcases l with ⟨l, rfl⟩
-  simp [Array.reverse_flatMap, Function.comp_def]
-
-theorem flatMap_reverse {β} (l : Vector α n) (f : α → Vector β m) :
-    (l.reverse.flatMap f) = (l.flatMap (reverse ∘ f)).reverse := by
-  rcases l with ⟨l, rfl⟩
-  simp [Array.flatMap_reverse, Function.comp_def]
-
-@[simp] theorem reverse_mkVector (n) (a : α) : reverse (mkVector n a) = mkVector n a := by
-  rw [← toArray_inj]
-  simp
-
 /-! Content below this point has not yet been aligned with `List` and `Array`. -/
 
 @[simp] theorem getElem_ofFn {α n} (f : Fin n → α) (i : Nat) (h : i < n) :
@@ -1963,6 +1735,13 @@ theorem swap_comm (a : Vector α n) {i j : Nat} {hi hj} :
   cases a
   simp
 
+/-! ### reverse -/
+
+@[simp] theorem getElem_reverse (a : Vector α n) (i : Nat) (hi : i < n) :
+    (a.reverse)[i] = a[n - 1 - i] := by
+  rcases a with ⟨a, rfl⟩
+  simp
+
 /-! ### Decidable quantifiers. -/
 
 theorem forall_zero_iff {P : Vector α 0 → Prop} :

src/Init/Grind/Tactics.lean

@@ -14,9 +14,7 @@ syntax grindEqRhs  := atomic("=" "_")
 syntax grindBwd    := "←"
 syntax grindFwd    := "→"
 
-syntax grindThmMod := grindEqBoth <|> grindEqRhs <|> grindEq <|> grindBwd <|> grindFwd
-
-syntax (name := grind) "grind" (grindThmMod)? : attr
+syntax (name := grind) "grind" (grindEqBoth <|> grindEqRhs <|> grindEq <|> grindBwd <|> grindFwd)? : attr
 
 end Lean.Parser.Attr
 
@@ -61,13 +59,7 @@ namespace Lean.Parser.Tactic
 `grind` tactic and related tactics.
 -/
 
-syntax grindErase := "-" ident
-syntax grindLemma := (Attr.grindThmMod)? ident
-syntax grindParam := grindErase <|> grindLemma
-
-syntax (name := grind)
-  "grind" optConfig (&" only")?
-  (" [" withoutPosition(grindParam,*) "]")?
-  ("on_failure " term)? : tactic
+-- TODO: parameters
+syntax (name := grind) "grind" optConfig ("on_failure " term)? : tactic
 
 end Lean.Parser.Tactic

src/Init/Prelude.lean

@@ -150,9 +150,6 @@ It can also be written as `()`.
 /-- Marker for information that has been erased by the code generator. -/
 unsafe axiom lcErased : Type
 
-/-- Marker for type dependency that has been erased by the code generator. -/
-unsafe axiom lcAny : Type
-
 /--
 Auxiliary unsafe constant used by the Compiler when erasing proofs from code.
 

src/Lean/Compiler/IR/ExpandResetReuse.lean

@@ -85,7 +85,7 @@ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (ke
 /-- Try to erase `inc` instructions on projections of `y` occurring in the tail of `bs`.
    Return the updated `bs` and a bit mask specifying which `inc`s have been removed. -/
 def eraseProjIncFor (n : Nat) (y : VarId) (bs : Array FnBody) : Array FnBody × Mask :=
-  eraseProjIncForAux y bs (mkArray n none) #[]
+  eraseProjIncForAux y bs (Array.replicate n none) #[]
 
 /-- Replace `reuse x ctor ...` with `ctor ...`, and remove `dec x` -/
 partial def reuseToCtor (x : VarId) : FnBody → FnBody

src/Lean/Compiler/LCNF/FixedParams.lean

@@ -169,7 +169,7 @@ def mkFixedParamsMap (decls : Array Decl) : NameMap (Array Bool) := Id.run do
   for decl in decls do
     let values := mkInitialValues decl.params.size
     let assignment := mkAssignment decl values
-    let fixed := Array.mkArray decl.params.size true
+    let fixed := Array.replicate decl.params.size true
     match decl.value with
     | .code c =>
       match evalCode c |>.run { main := decl, decls, assignment } |>.run { fixed } with

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

@@ -98,7 +98,7 @@ where
       return { ctx with discrCtorMap := ctx.discrCtorMap.insert discr ctorInfo, ctorDiscrMap := ctx.ctorDiscrMap.insert ctor.toExpr discr }
     else
       -- For the discrCtor map, the constructor parameters are irrelevant for optimizations that use this information
-      let ctorInfo := .ctor ctorVal (mkArray ctorVal.numParams Arg.erased ++ fieldArgs)
+      let ctorInfo := .ctor ctorVal (Array.replicate ctorVal.numParams Arg.erased ++ fieldArgs)
       return { ctx with discrCtorMap := ctx.discrCtorMap.insert discr ctorInfo }
 
 @[inline, inherit_doc withDiscrCtorImp] def withDiscrCtor [MonadFunctorT DiscrM m] (discr : FVarId) (ctorName : Name) (ctorFields : Array Param) : m α → m α :=

src/Lean/Compiler/LCNF/SpecInfo.lean

@@ -147,7 +147,7 @@ def saveSpecParamInfo (decls : Array Decl) : CompilerM Unit := do
   let mut declsInfo := #[]
   for decl in decls do
     if hasNospecializeAttribute (← getEnv) decl.name then
-      declsInfo := declsInfo.push (mkArray decl.params.size .other)
+      declsInfo := declsInfo.push (Array.replicate decl.params.size .other)
     else
       let specArgs? := getSpecializationArgs? (← getEnv) decl.name
       let contains (i : Nat) : Bool := specArgs?.getD #[] |>.contains i

src/Lean/Compiler/LCNF/ToMono.lean

@@ -150,7 +150,18 @@ where
 
 def toMono : Pass where
   name     := `toMono
-  run      := (·.mapM (·.toMono))
+  run      := fun decls => do
+    let decls ← decls.filterM fun decl => do
+      if hasLocalInst decl.type then
+        /-
+        Declaration is a "template" for the code specialization pass.
+        So, we should delete it before going to next phase.
+        -/
+        decl.erase
+        return false
+      else
+        return true
+    decls.mapM (·.toMono)
   phase    := .base
   phaseOut := .mono
 

src/Lean/Data/Array.lean

@@ -24,7 +24,7 @@ order, exists in the array.
 -/
 def filterPairsM {m} [Monad m] {α} (a : Array α) (f : α → α → m (Bool × Bool)) :
     m (Array α) := do
-  let mut removed := Array.mkArray a.size false
+  let mut removed := Array.replicate a.size false
   let mut numRemoved := 0
   for h1 : i in [:a.size] do for h2 : j in [i+1:a.size] do
     unless removed[i]! || removed[j]! do

src/Lean/Data/FuzzyMatching.lean

@@ -99,11 +99,11 @@ private def fuzzyMatchCore (pattern word : String) (patternRoles wordRoles : Arr
   between the substrings pattern[:i+1] and word[:j+1] assuming that pattern[i] misses at word[j] (k = 0, i.e.
   it was matched earlier), or matches at word[j] (k = 1). A value of `none` corresponds to a score of -∞, and is used
   where no such match/miss is possible or for unneeded parts of the table. -/
-  let mut result : Array (Option Int) := Array.mkArray (pattern.length * word.length * 2) none
-  let mut runLengths : Array Int := Array.mkArray (pattern.length * word.length) 0
+  let mut result : Array (Option Int) := Array.replicate (pattern.length * word.length * 2) none
+  let mut runLengths : Array Int := Array.replicate (pattern.length * word.length) 0
 
   -- penalty for starting a consecutive run at each index
-  let mut startPenalties : Array Int := Array.mkArray word.length 0
+  let mut startPenalties : Array Int := Array.replicate word.length 0
 
   let mut lastSepIdx := 0
   let mut penaltyNs : Int := 0
@@ -124,8 +124,8 @@ private def fuzzyMatchCore (pattern word : String) (patternRoles wordRoles : Arr
    `word.length - pattern.length` at each index (because at the very end, we can only consider fuzzy matches
     of `pattern` with a longer substring of `word`). -/
     for wordIdx in [patternIdx:word.length-(pattern.length - patternIdx - 1)] do
-      let missScore? := 
-        if wordIdx >= 1 then 
+      let missScore? :=
+        if wordIdx >= 1 then
           selectBest
             (getMiss result patternIdx (wordIdx - 1))
             (getMatch result patternIdx (wordIdx - 1))
@@ -134,7 +134,7 @@ private def fuzzyMatchCore (pattern word : String) (patternRoles wordRoles : Arr
       let mut matchScore? := none
 
       if allowMatch (pattern.get ⟨patternIdx⟩) (word.get ⟨wordIdx⟩) (patternRoles.get! patternIdx) (wordRoles.get! wordIdx) then
-        if patternIdx >= 1 then 
+        if patternIdx >= 1 then
           let runLength := runLengths.get! (getIdx (patternIdx - 1) (wordIdx - 1)) + 1
           runLengths := runLengths.set! (getIdx patternIdx wordIdx) runLength
 
@@ -213,7 +213,7 @@ private def fuzzyMatchCore (pattern word : String) (patternRoles wordRoles : Arr
       /- Consecutive character match. -/
       if let some bonus := consecutive then
         /- consecutive run bonus -/
-        score := score + bonus 
+        score := score + bonus
       return score
 
 /-- Match the given pattern with the given word using a fuzzy matching

src/Lean/Data/HashMap.lean

@@ -32,7 +32,7 @@ private def numBucketsForCapacity (capacity : Nat) : Nat :=
 def mkHashMapImp {α : Type u} {β : Type v} (capacity := 8) : HashMapImp α β :=
   { size       := 0
     buckets    :=
-    ⟨mkArray (numBucketsForCapacity capacity).nextPowerOfTwo AssocList.nil,
+    ⟨Array.replicate (numBucketsForCapacity capacity).nextPowerOfTwo AssocList.nil,
      by simp; apply Nat.isPowerOfTwo_nextPowerOfTwo⟩ }
 
 namespace HashMapImp
@@ -101,7 +101,7 @@ decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapImp α β :=
   let bucketsNew : HashMapBucket α β := ⟨
-    mkArray (buckets.val.size * 2) AssocList.nil,
+    Array.replicate (buckets.val.size * 2) AssocList.nil,
     by simp; apply Nat.mul2_isPowerOfTwo_of_isPowerOfTwo buckets.property
   ⟩
   { size    := size,

src/Lean/Data/HashSet.lean

@@ -28,7 +28,7 @@ structure HashSetImp (α : Type u) where
 def mkHashSetImp {α : Type u} (capacity := 8) : HashSetImp α :=
   { size       := 0
     buckets    :=
-    ⟨mkArray ((capacity * 4) / 3).nextPowerOfTwo [],
+    ⟨Array.replicate ((capacity * 4) / 3).nextPowerOfTwo [],
      by simp; apply Nat.isPowerOfTwo_nextPowerOfTwo⟩ }
 
 namespace HashSetImp
@@ -92,7 +92,7 @@ decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def expand [Hashable α] (size : Nat) (buckets : HashSetBucket α) : HashSetImp α :=
   let bucketsNew : HashSetBucket α := ⟨
-    mkArray (buckets.val.size * 2) [],
+    Array.replicate (buckets.val.size * 2) [],
     by simp; apply Nat.mul2_isPowerOfTwo_of_isPowerOfTwo buckets.property
   ⟩
   { size    := size,

src/Lean/Data/PersistentHashMap.lean

@@ -39,7 +39,7 @@ abbrev maxDepth      : USize  := 7
 abbrev maxCollisions : Nat    := 4
 
 def mkEmptyEntriesArray {α β} : Array (Entry α β (Node α β)) :=
-  (Array.mkArray PersistentHashMap.branching.toNat PersistentHashMap.Entry.null)
+  (Array.replicate PersistentHashMap.branching.toNat PersistentHashMap.Entry.null)
 
 end PersistentHashMap
 

src/Lean/Elab/Tactic/Grind.lean

@@ -34,44 +34,8 @@ def elabGrindPattern : CommandElab := fun stx => do
         Grind.addEMatchTheorem declName xs.size patterns.toList
   | _ => throwUnsupportedSyntax
 
-def elabGrindParams (params : Grind.Params) (ps :  TSyntaxArray ``Parser.Tactic.grindParam) : MetaM Grind.Params := do
-  let mut params := params
-  for p in ps do
-    match p with
-    | `(Parser.Tactic.grindParam| - $id:ident) =>
-      let declName ← realizeGlobalConstNoOverloadWithInfo id
-      if (← isInductivePredicate declName) then
-        throwErrorAt p "NIY"
-      else
-        params := { params with ematch := (← params.ematch.eraseDecl declName) }
-    | `(Parser.Tactic.grindParam| $[$mod?:grindThmMod]? $id:ident) =>
-      let declName ← realizeGlobalConstNoOverloadWithInfo id
-      let kind ← if let some mod := mod? then Grind.getTheoremKindCore mod else pure .default
-      if (← isInductivePredicate declName) then
-        throwErrorAt p "NIY"
-      else if (← getConstInfo declName).isTheorem then
-        params := { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName kind) }
-      else if let some eqns ← getEqnsFor? declName then
-        for eqn in eqns do
-          params := { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl eqn kind) }
-      else
-        throwError "invalid `grind` parameter, `{declName}` is not a theorem, definition, or inductive type"
-    | _ => throwError "unexpected `grind` parameter{indentD p}"
-  return params
-
-def mkGrindParams (config : Grind.Config) (only : Bool) (ps :  TSyntaxArray ``Parser.Tactic.grindParam) : MetaM Grind.Params := do
-  let params ← Grind.mkParams config
-  let ematch ← if only then pure {} else Grind.getEMatchTheorems
-  let params := { params with ematch }
-  elabGrindParams params ps
-
-def grind
-    (mvarId : MVarId) (config : Grind.Config)
-    (only : Bool)
-    (ps   :  TSyntaxArray ``Parser.Tactic.grindParam)
-    (mainDeclName : Name) (fallback : Grind.Fallback) : MetaM Unit := do
-  let params ← mkGrindParams config only ps
-  let goals ← Grind.main mvarId params mainDeclName fallback
+def grind (mvarId : MVarId) (config : Grind.Config) (mainDeclName : Name) (fallback : Grind.Fallback) : MetaM Unit := do
+  let goals ← Grind.main mvarId config mainDeclName fallback
   unless goals.isEmpty do
     throwError "`grind` failed\n{← Grind.goalsToMessageData goals config}"
 
@@ -94,14 +58,12 @@ private def elabFallback (fallback? : Option Term) : TermElabM (Grind.GoalM Unit
 
 @[builtin_tactic Lean.Parser.Tactic.grind] def evalApplyRfl : Tactic := fun stx => do
   match stx with
-  | `(tactic| grind $config:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]? $[on_failure $fallback?]?) =>
+  | `(tactic| grind $config:optConfig $[on_failure $fallback?]?) =>
     let fallback ← elabFallback fallback?
-    let only := only.isSome
-    let params := if let some params := params then params.getElems else #[]
     logWarningAt stx "The `grind` tactic is experimental and still under development. Avoid using it in production projects"
     let declName := (← Term.getDeclName?).getD `_grind
     let config ← elabGrindConfig config
-    withMainContext do liftMetaFinishingTactic (grind · config only params declName fallback)
+    withMainContext do liftMetaFinishingTactic (grind · config declName fallback)
   | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Tactic

src/Lean/Environment.lean

@@ -735,7 +735,7 @@ private def setImportedEntries (env : Environment) (mods : Array ModuleData) (st
   let extDescrs ← persistentEnvExtensionsRef.get
   /- For extensions starting at `startingAt`, ensure their `importedEntries` array have size `mods.size`. -/
   for extDescr in extDescrs[startingAt:] do
-    env := extDescr.toEnvExtension.modifyState env fun s => { s with importedEntries := mkArray mods.size #[] }
+    env := extDescr.toEnvExtension.modifyState env fun s => { s with importedEntries := Array.replicate mods.size #[] }
   /- For each module `mod`, and `mod.entries`, if the extension name is one of the extensions after `startingAt`, set `entries` -/
   let extNameIdx ← mkExtNameMap startingAt
   for h : modIdx in [:mods.size] do

src/Lean/Expr.lean

@@ -1127,7 +1127,7 @@ private def getAppArgsAux : Expr → Array Expr → Nat → Array Expr
 @[inline] def getAppArgs (e : Expr) : Array Expr :=
   let dummy := mkSort levelZero
   let nargs := e.getAppNumArgs
-  getAppArgsAux e (mkArray nargs dummy) (nargs-1)
+  getAppArgsAux e (Array.replicate nargs dummy) (nargs-1)
 
 private def getBoundedAppArgsAux : Expr → Array Expr → Nat → Array Expr
   | app f a, as, i + 1 => getBoundedAppArgsAux f (as.set! i a) i
@@ -1142,7 +1142,7 @@ where `k` is minimal such that the size of this array is at most `maxArgs`.
 @[inline] def getBoundedAppArgs (maxArgs : Nat) (e : Expr) : Array Expr :=
   let dummy := mkSort levelZero
   let nargs := min maxArgs e.getAppNumArgs
-  getBoundedAppArgsAux e (mkArray nargs dummy) nargs
+  getBoundedAppArgsAux e (Array.replicate nargs dummy) nargs
 
 private def getAppRevArgsAux : Expr → Array Expr → Array Expr
   | app f a, as => getAppRevArgsAux f (as.push a)
@@ -1160,7 +1160,7 @@ private def getAppRevArgsAux : Expr → Array Expr → Array Expr
 @[inline] def withApp (e : Expr) (k : Expr → Array Expr → α) : α :=
   let dummy := mkSort levelZero
   let nargs := e.getAppNumArgs
-  withAppAux k e (mkArray nargs dummy) (nargs-1)
+  withAppAux k e (Array.replicate nargs dummy) (nargs-1)
 
 /-- Return the function (name) and arguments of an application. -/
 def getAppFnArgs (e : Expr) : Name × Array Expr :=
@@ -1173,7 +1173,7 @@ The resulting array has size `n` even if `f.getAppNumArgs < n`.
 -/
 @[inline] def getAppArgsN (e : Expr) (n : Nat) : Array Expr :=
   let dummy := mkSort levelZero
-  loop n e (mkArray n dummy)
+  loop n e (Array.replicate n dummy)
 where
   loop : Nat → Expr → Array Expr → Array Expr
     | 0,   _,        as => as

src/Lean/Meta/Diagnostics.lean

@@ -72,12 +72,12 @@ def mkDiagSynthPendingFailure (failures : PHashMap Expr MessageData) : MetaM Dia
 /--
 We use below that this returns `m` unchanged if `s.isEmpty`
 -/
-def appendSection (m : Array MessageData) (cls : Name) (header : String) (s : DiagSummary) (resultSummary := true) : Array MessageData :=
+def appendSection (m : MessageData) (cls : Name) (header : String) (s : DiagSummary) (resultSummary := true) : MessageData :=
   if s.isEmpty then
     m
   else
     let header := if resultSummary then s!"{header} (max: {s.max}, num: {s.data.size}):" else header
-    m.push <| .trace { cls } header s.data
+    m ++ .trace { cls } header s.data
 
 def reportDiag : MetaM Unit := do
   if (← isDiagnosticsEnabled) then
@@ -89,7 +89,7 @@ def reportDiag : MetaM Unit := do
     let inst ← mkDiagSummaryForUsedInstances
     let synthPending ← mkDiagSynthPendingFailure (← get).diag.synthPendingFailures
     let unfoldKernel ← mkDiagSummary `kernel (Kernel.getDiagnostics (← getEnv)).unfoldCounter
-    let m := #[]
+    let m := MessageData.nil
     let m := appendSection m `reduction "unfolded declarations" unfoldDefault
     let m := appendSection m `reduction "unfolded instances" unfoldInstance
     let m := appendSection m `reduction "unfolded reducible declarations" unfoldReducible
@@ -99,8 +99,8 @@ def reportDiag : MetaM Unit := do
               synthPending (resultSummary := false)
     let m := appendSection m `def_eq "heuristic for solving `f a =?= f b`" heu
     let m := appendSection m `kernel "unfolded declarations" unfoldKernel
-    unless m.isEmpty do
-      let m := m.push "use `set_option diagnostics.threshold <num>` to control threshold for reporting counters"
-      logInfo <| .trace { cls := `diag, collapsed := false } "Diagnostics" m
+    unless m matches .nil do
+      let m := m ++ "use `set_option diagnostics.threshold <num>` to control threshold for reporting counters"
+      logInfo m
 
 end Lean.Meta

src/Lean/Meta/SizeOf.lean

@@ -196,7 +196,7 @@ def mkSizeOfSpecLemmaInstance (ctorApp : Expr) : MetaM Expr :=
     let lemmaInfo  ← getConstInfo lemmaName
     let lemmaArity ← forallTelescopeReducing lemmaInfo.type fun xs _ => return xs.size
     let lemmaArgMask := ctorParams.toArray.map some
-    let lemmaArgMask := lemmaArgMask ++ mkArray (lemmaArity - ctorInfo.numParams - ctorInfo.numFields) (none (α := Expr))
+    let lemmaArgMask := lemmaArgMask ++ Array.replicate (lemmaArity - ctorInfo.numParams - ctorInfo.numFields) (none (α := Expr))
     let lemmaArgMask := lemmaArgMask ++ ctorFields.toArray.map some
     mkAppOptM lemmaName lemmaArgMask
 

src/Lean/Meta/Tactic/Grind.lean

@@ -38,7 +38,6 @@ builtin_initialize registerTraceClass `grind.ematch.pattern
 builtin_initialize registerTraceClass `grind.ematch.pattern.search
 builtin_initialize registerTraceClass `grind.ematch.instance
 builtin_initialize registerTraceClass `grind.ematch.instance.assignment
-builtin_initialize registerTraceClass `grind.eqResolution
 builtin_initialize registerTraceClass `grind.issues
 builtin_initialize registerTraceClass `grind.simp
 builtin_initialize registerTraceClass `grind.split

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

@@ -551,7 +551,7 @@ def getEMatchTheorems : CoreM EMatchTheorems :=
 
 inductive TheoremKind where
   | eqLhs | eqRhs | eqBoth | fwd | bwd | default
-  deriving Inhabited, BEq, Repr
+  deriving Inhabited, BEq
 
 private def TheoremKind.toAttribute : TheoremKind → String
   | .eqLhs   => "[grind =]"
@@ -677,22 +677,19 @@ where
       levelParams, origin
     }
 
-/-- Return theorem kind for `stx` of the form `Attr.grindThmMod` -/
-def getTheoremKindCore (stx : Syntax) : CoreM TheoremKind := do
-  match stx with
-  | `(Parser.Attr.grindThmMod| =) => return .eqLhs
-  | `(Parser.Attr.grindThmMod| →) => return .fwd
-  | `(Parser.Attr.grindThmMod| ←) => return .bwd
-  | `(Parser.Attr.grindThmMod| =_) => return .eqRhs
-  | `(Parser.Attr.grindThmMod| _=_) => return .eqBoth
-  | _ => throwError "unexpected `grind` theorem kind: `{stx}`"
-
-/-- Return theorem kind for `stx` of the form `(Attr.grindThmMod)?` -/
-def getTheoremKindFromOpt (stx : Syntax) : CoreM TheoremKind := do
+private def getKind (stx : Syntax) : TheoremKind :=
   if stx[1].isNone then
-    return .default
+    .default
+  else if stx[1][0].getKind == ``Parser.Attr.grindEq then
+    .eqLhs
+  else if stx[1][0].getKind == ``Parser.Attr.grindFwd then
+    .fwd
+  else if stx[1][0].getKind == ``Parser.Attr.grindEqRhs then
+    .eqRhs
+  else if stx[1][0].getKind == ``Parser.Attr.grindEqBoth then
+    .eqBoth
   else
-    getTheoremKindCore stx[1][0]
+    .bwd
 
 private def addGrindEqAttr (declName : Name) (attrKind : AttributeKind) (thmKind : TheoremKind) (useLhs := true) : MetaM Unit := do
   if (← getConstInfo declName).isTheorem then
@@ -705,11 +702,6 @@ private def addGrindEqAttr (declName : Name) (attrKind : AttributeKind) (thmKind
   else
     throwError s!"`{thmKind.toAttribute}` attribute can only be applied to equational theorems or function definitions"
 
-def mkEMatchTheoremForDecl (declName : Name) (thmKind : TheoremKind) : MetaM EMatchTheorem := do
-  let some thm ← mkEMatchTheoremWithKind? (.decl declName) #[] (← getProofFor declName) thmKind
-    | throwError "`@{thmKind.toAttribute} theorem {declName}` {thmKind.explainFailure}, consider using different options or the `grind_pattern` command"
-  return thm
-
 private def addGrindAttr (declName : Name) (attrKind : AttributeKind) (thmKind : TheoremKind) : MetaM Unit := do
   if thmKind == .eqLhs then
     addGrindEqAttr declName attrKind thmKind (useLhs := true)
@@ -721,26 +713,10 @@ private def addGrindAttr (declName : Name) (attrKind : AttributeKind) (thmKind :
   else if !(← getConstInfo declName).isTheorem then
     addGrindEqAttr declName attrKind thmKind
   else
-    let thm ← mkEMatchTheoremForDecl declName thmKind
+    let some thm ← mkEMatchTheoremWithKind? (.decl declName) #[] (← getProofFor declName) thmKind
+      | throwError "`@{thmKind.toAttribute} theorem {declName}` {thmKind.explainFailure}, consider using different options or the `grind_pattern` command"
     ematchTheoremsExt.add thm attrKind
 
-def EMatchTheorems.eraseDecl (s : EMatchTheorems) (declName : Name) : MetaM EMatchTheorems := do
-  let throwErr {α} : MetaM α :=
-    throwError "`{declName}` is not marked with the `[grind]` attribute"
-  let info ← getConstInfo declName
-  if !info.isTheorem then
-    if let some eqns ← getEqnsFor? declName then
-       let s := ematchTheoremsExt.getState (← getEnv)
-       unless eqns.all fun eqn => s.contains (.decl eqn) do
-         throwErr
-       return eqns.foldl (init := s) fun s eqn => s.erase (.decl eqn)
-    else
-      throwErr
-  else
-    unless ematchTheoremsExt.getState (← getEnv) |>.contains (.decl declName) do
-      throwErr
-    return s.erase <| .decl declName
-
 builtin_initialize
   registerBuiltinAttribute {
     name := `grind
@@ -763,7 +739,7 @@ builtin_initialize
       `grind` will add an instance of this theorem to the local context whenever it encounters the pattern `foo (foo x)`."
     applicationTime := .afterCompilation
     add := fun declName stx attrKind => do
-      addGrindAttr declName attrKind (← getTheoremKindFromOpt stx) |>.run' {}
+      addGrindAttr declName attrKind (getKind stx) |>.run' {}
     erase := fun declName => MetaM.run' do
       /-
       Remark: consider the following example
@@ -779,9 +755,21 @@ builtin_initialize
       attribute [-grind] foo  -- ok
       ```
       -/
-      let s := ematchTheoremsExt.getState (← getEnv)
-      let s ← s.eraseDecl declName
-      modifyEnv fun env => ematchTheoremsExt.modifyState env fun _ => s
+      let throwErr := throwError "`{declName}` is not marked with the `[grind]` attribute"
+      let info ← getConstInfo declName
+      if !info.isTheorem then
+        if let some eqns ← getEqnsFor? declName then
+           let s := ematchTheoremsExt.getState (← getEnv)
+           unless eqns.all fun eqn => s.contains (.decl eqn) do
+             throwErr
+           modifyEnv fun env => ematchTheoremsExt.modifyState env fun s =>
+             eqns.foldl (init := s) fun s eqn => s.erase (.decl eqn)
+        else
+          throwErr
+      else
+        unless ematchTheoremsExt.getState (← getEnv) |>.contains (.decl declName) do
+          throwErr
+        modifyEnv fun env => ematchTheoremsExt.modifyState env fun s => s.erase (.decl declName)
   }
 
 end Lean.Meta.Grind

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

@@ -1,49 +0,0 @@
-/-
-Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.Meta.AppBuilder
-
-namespace Lean.Meta.Grind
-/-!
-A basic "equality resolution" procedure to make Kim happy.
--/
-
-private def eqResCore (prop proof : Expr) : MetaM (Option (Expr × Expr)) := withNewMCtxDepth do
-  let (ms, _, type) ← forallMetaTelescopeReducing prop
-  if ms.isEmpty then return none
-  let mut progress := false
-  for m in ms do
-    let type ← inferType m
-    let_expr Eq _ lhs rhs ← type
-      | pure ()
-    if (← isDefEq lhs rhs) then
-      unless (← m.mvarId!.checkedAssign (← mkEqRefl lhs)) do
-        return none
-      progress := true
-  unless progress do
-    return none
-  if (← ms.anyM fun m => m.mvarId!.isDelayedAssigned) then
-    return none
-  let prop' ← instantiateMVars type
-  let proof' ← instantiateMVars (mkAppN proof ms)
-  let ms ← ms.filterM fun m => return !(← m.mvarId!.isAssigned)
-  let prop' ← mkForallFVars ms prop' (binderInfoForMVars := .default)
-  let proof' ← mkLambdaFVars ms proof'
-  return some (prop', proof')
-
-/--
-A basic "equality resolution" procedure: Given a proposition `prop` with a proof `proof`, it attempts to resolve equality hypotheses using `isDefEq`. For example, it reduces `∀ x y, f x = f (g y y) → g x y = y` to `∀ y, g (g y y) y = y`, and `∀ (x : Nat), f x ≠ f a` to `False`.
-If successful, the result is a pair `(prop', proof)`, where `prop'` is the simplified proposition,
-and `proof : prop → prop'`
--/
-def eqResolution (prop : Expr) : MetaM (Option (Expr × Expr)) :=
-  withLocalDeclD `h prop fun h => do
-    let some (prop', proof') ← eqResCore prop h
-      | return none
-    let proof' ← mkLambdaFVars #[h] proof'
-    return some (prop', proof')
-
-end Lean.Meta.Grind

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

@@ -8,7 +8,6 @@ import Init.Grind.Lemmas
 import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Internalize
 import Lean.Meta.Tactic.Grind.Simp
-import Lean.Meta.Tactic.Grind.EqResolution
 
 namespace Lean.Meta.Grind
 /--
@@ -97,13 +96,7 @@ def propagateForallPropDown (e : Expr) : GoalM Unit := do
       pushEqTrue a <| mkApp3 (mkConst ``Grind.eq_true_of_imp_eq_false) a b h
       pushEqFalse b <| mkApp3 (mkConst ``Grind.eq_false_of_imp_eq_false) a b h
   else if (← isEqTrue e) then
-    if let some (e', h') ← eqResolution e then
-      trace[grind.eqResolution] "{e}, {e'}"
-      let h := mkOfEqTrueCore e (← mkEqTrueProof e)
-      let h' := mkApp h' h
-      addNewFact h' e' (← getGeneration e)
-    else
-      if b.hasLooseBVars then
-        addLocalEMatchTheorems e
+    if b.hasLooseBVars then
+      addLocalEMatchTheorems e
 
 end Lean.Meta.Grind

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

@@ -20,19 +20,6 @@ import Lean.Meta.Tactic.Grind.SimpUtil
 
 namespace Lean.Meta.Grind
 
-structure Params where
-  config    : Grind.Config
-  ematch    : EMatchTheorems := {}
-  extra     : PArray EMatchTheorem := {}
-  norm      : Simp.Context
-  normProcs : Array Simprocs
-  -- TODO: inductives to split
-
-def mkParams (config : Grind.Config) : MetaM Params := do
-  let norm ← Grind.getSimpContext
-  let normProcs ← Grind.getSimprocs
-  return { config, norm, normProcs }
-
 def mkMethods (fallback : Fallback) : CoreM Methods := do
   let builtinPropagators ← builtinPropagatorsRef.get
   return {
@@ -50,29 +37,26 @@ def mkMethods (fallback : Fallback) : CoreM Methods := do
        prop e
   }
 
-def GrindM.run (x : GrindM α) (mainDeclName : Name) (params : Params) (fallback : Fallback) : MetaM α := do
+def GrindM.run (x : GrindM α) (mainDeclName : Name) (config : Grind.Config) (fallback : Fallback) : MetaM α := do
   let scState := ShareCommon.State.mk _
   let (falseExpr, scState) := ShareCommon.State.shareCommon scState (mkConst ``False)
   let (trueExpr, scState)  := ShareCommon.State.shareCommon scState (mkConst ``True)
   let (natZExpr, scState)  := ShareCommon.State.shareCommon scState (mkNatLit 0)
-  let simprocs := params.normProcs
-  let simp := params.norm
-  let config := params.config
+  let simprocs ← Grind.getSimprocs
+  let simp ← Grind.getSimpContext
   x (← mkMethods fallback).toMethodsRef { mainDeclName, config, simprocs, simp } |>.run' { scState, trueExpr, falseExpr, natZExpr }
 
-private def mkGoal (mvarId : MVarId) (params : Params) : GrindM Goal := do
+private def mkGoal (mvarId : MVarId) : GrindM Goal := do
   let trueExpr ← getTrueExpr
   let falseExpr ← getFalseExpr
   let natZeroExpr ← getNatZeroExpr
-  let thmMap := params.ematch
+  let thmMap ← getEMatchTheorems
   GoalM.run' { mvarId, thmMap } do
     mkENodeCore falseExpr (interpreted := true) (ctor := false) (generation := 0)
     mkENodeCore trueExpr (interpreted := true) (ctor := false) (generation := 0)
     mkENodeCore natZeroExpr (interpreted := true) (ctor := false) (generation := 0)
-    for thm in params.extra do
-      activateTheorem thm 0
 
-private def initCore (mvarId : MVarId) (params : Params) : GrindM (List Goal) := do
+private def initCore (mvarId : MVarId) : GrindM (List Goal) := do
   mvarId.ensureProp
   -- TODO: abstract metavars
   mvarId.ensureNoMVar
@@ -81,13 +65,13 @@ private def initCore (mvarId : MVarId) (params : Params) : GrindM (List Goal) :=
   let mvarId ← mvarId.unfoldReducible
   let mvarId ← mvarId.betaReduce
   appendTagSuffix mvarId `grind
-  let goals ← intros (← mkGoal mvarId params) (generation := 0)
+  let goals ← intros (← mkGoal mvarId) (generation := 0)
   goals.forM (·.checkInvariants (expensive := true))
   return goals.filter fun goal => !goal.inconsistent
 
-def main (mvarId : MVarId) (params : Params) (mainDeclName : Name) (fallback : Fallback) : MetaM (List Goal) := do
+def main (mvarId : MVarId) (config : Grind.Config) (mainDeclName : Name) (fallback : Fallback) : MetaM (List Goal) := do
   let go : GrindM (List Goal) := do
-    let goals ← initCore mvarId params
+    let goals ← initCore mvarId
     let goals ← solve goals
     let goals ← goals.filterMapM fun goal => do
       if goal.inconsistent then return none
@@ -97,6 +81,6 @@ def main (mvarId : MVarId) (params : Params) (mainDeclName : Name) (fallback : F
       return some goal
     trace[grind.debug.final] "{← ppGoals goals}"
     return goals
-  go.run mainDeclName params fallback
+  go.run mainDeclName config fallback
 
 end Lean.Meta.Grind

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

@@ -52,12 +52,12 @@ def reportDiag (diag : Simp.Diagnostics) : MetaM Unit := do
     let congr ← mkDiagSummary `simp diag.congrThmCounter
     let thmsWithBadKeys ← mkTheoremsWithBadKeySummary diag.thmsWithBadKeys
     unless used.isEmpty && tried.isEmpty && congr.isEmpty && thmsWithBadKeys.isEmpty do
-      let m := #[]
+      let m := MessageData.nil
       let m := appendSection m `simp "used theorems" used
       let m := appendSection m `simp "tried theorems" tried
       let m := appendSection m `simp "tried congruence theorems" congr
       let m := appendSection m `simp "theorems with bad keys" thmsWithBadKeys (resultSummary := false)
-      let m := m.push <| "use `set_option diagnostics.threshold <num>` to control threshold for reporting counters"
-      logInfo <| .trace { cls := `simp, collapsed := false } "Diagnostics" m
+      let m := m ++ "use `set_option diagnostics.threshold <num>` to control threshold for reporting counters"
+      logInfo m
 
 end Lean.Meta.Simp

src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean

@@ -419,10 +419,10 @@ mutual
         || (getPPAnalyzeTrustSubtypeMk (← getOptions) && (← getExpr).isAppOfArity ``Subtype.mk 4)
 
       analyzeAppStagedCore { f, fType, args, mvars, bInfos, forceRegularApp } |>.run' {
-        bottomUps    := mkArray args.size false,
-        higherOrders := mkArray args.size false,
-        provideds    := mkArray args.size false,
-        funBinders   := mkArray args.size false
+        bottomUps    := Array.replicate args.size false,
+        higherOrders := Array.replicate args.size false,
+        provideds    := Array.replicate args.size false,
+        funBinders   := Array.replicate args.size false
       }
 
       if !rest.isEmpty then

src/Lean/Syntax.lean

@@ -495,7 +495,7 @@ def getCanonicalAntiquot (stx : Syntax) : Syntax :=
     stx
 
 def mkAntiquotNode (kind : Name) (term : Syntax) (nesting := 0) (name : Option String := none) (isPseudoKind := false) : Syntax :=
-  let nesting := mkNullNode (mkArray nesting (mkAtom "$"))
+  let nesting := mkNullNode (Array.replicate nesting (mkAtom "$"))
   let term :=
     if term.isIdent then term
     else if term.isOfKind `Lean.Parser.Term.hole then term[0]
@@ -558,7 +558,7 @@ def getAntiquotSpliceSuffix (stx : Syntax) : Syntax :=
     stx[1]
 
 def mkAntiquotSpliceNode (kind : SyntaxNodeKind) (contents : Array Syntax) (suffix : String) (nesting := 0) : Syntax :=
-  let nesting := mkNullNode (mkArray nesting (mkAtom "$"))
+  let nesting := mkNullNode (Array.replicate nesting (mkAtom "$"))
   mkNode (kind ++ `antiquot_splice) #[mkAtom "$", nesting, mkAtom "[", mkNullNode contents, mkAtom "]", mkAtom suffix]
 
 -- `$x,*` etc.

src/Lean/Util/ForEachExprWhere.lean

@@ -31,7 +31,7 @@ structure State where
   checked : Std.HashSet Expr
 
 unsafe def initCache : State := {
-  visited := mkArray cacheSize.toNat (cast lcProof ())
+  visited := Array.replicate cacheSize.toNat (cast lcProof ())
   checked := {}
 }
 

src/Lean/Util/ReplaceLevel.lean

@@ -56,8 +56,8 @@ unsafe def replaceUnsafeM (f? : Level → Option Level) (size : USize) (e : Expr
   visit e
 
 unsafe def initCache : State :=
-  { keys    := mkArray cacheSize.toNat (cast lcProof ()), -- `()` is not a valid `Expr`
-    results := mkArray cacheSize.toNat default }
+  { keys    := Array.replicate cacheSize.toNat (cast lcProof ()), -- `()` is not a valid `Expr`
+    results := Array.replicate cacheSize.toNat default }
 
 unsafe def replaceUnsafe (f? : Level → Option Level) (e : Expr) : Expr :=
   (replaceUnsafeM f? cacheSize e).run' initCache

src/Std/Data/DHashMap/Internal/Defs.lean

@@ -170,7 +170,7 @@ namespace Raw₀
 
 /-- Internal implementation detail of the hash map -/
 @[inline] def empty (capacity := 8) : Raw₀ α β :=
-  ⟨⟨0, mkArray (numBucketsForCapacity capacity).nextPowerOfTwo AssocList.nil⟩,
+  ⟨⟨0, Array.replicate (numBucketsForCapacity capacity).nextPowerOfTwo AssocList.nil⟩,
     by simpa using Nat.pos_of_isPowerOfTwo (Nat.isPowerOfTwo_nextPowerOfTwo _)⟩
 
 -- Take `hash` as a function instead of `Hashable α` as per
@@ -187,7 +187,7 @@ def expand [Hashable α] (data : { d : Array (AssocList α β) // 0 < d.size })
     { d : Array (AssocList α β) // 0 < d.size } :=
   let ⟨data, hd⟩ := data
   let nbuckets := data.size * 2
-  go 0 data ⟨mkArray nbuckets AssocList.nil, by simpa [nbuckets] using Nat.mul_pos hd Nat.two_pos⟩
+  go 0 data ⟨Array.replicate nbuckets AssocList.nil, by simpa [nbuckets] using Nat.mul_pos hd Nat.two_pos⟩
 where
   /-- Inner loop of `expand`. Copies elements `source[i:]` into `target`,
   destroying `source` in the process. -/

src/Std/Data/DHashMap/Internal/Model.lean

@@ -219,8 +219,8 @@ theorem toListModel_updateAllBuckets {m : Raw₀ α β} {f : AssocList α β →
 namespace IsHashSelf
 
 @[simp]
-theorem mkArray [BEq α] [Hashable α] {c : Nat} : IsHashSelf
-    (mkArray c (AssocList.nil : AssocList α β)) :=
+theorem replicate [BEq α] [Hashable α] {c : Nat} : IsHashSelf
+    (Array.replicate c (AssocList.nil : AssocList α β)) :=
   ⟨by simp⟩
 
 theorem uset [BEq α] [Hashable α] {m : Array (AssocList α β)} {i : USize} {h : i.toNat < m.size}

src/Std/Data/DHashMap/Internal/WF.lean

@@ -29,8 +29,8 @@ open List
 namespace Std.DHashMap.Internal
 
 @[simp]
-theorem toListModel_mkArray_nil {c} :
-    toListModel (mkArray c (AssocList.nil : AssocList α β)) = [] := by
+theorem toListModel_replicate_nil {c} :
+    toListModel (Array.replicate c (AssocList.nil : AssocList α β)) = [] := by
   suffices ∀ d, (List.replicate d AssocList.nil).flatMap AssocList.toList = [] from this _
   intro d
   induction d <;> simp_all [List.replicate]
@@ -143,7 +143,7 @@ namespace Raw₀
 
 @[simp]
 theorem toListModel_buckets_empty {c} : toListModel (empty c : Raw₀ α β).1.buckets = [] :=
-  toListModel_mkArray_nil
+  toListModel_replicate_nil
 
 theorem wfImp_empty [BEq α] [Hashable α] {c} : Raw.WFImp (empty c : Raw₀ α β).1 where
   buckets_hash_self := by simp [Raw.empty, Raw₀.empty]
@@ -229,7 +229,7 @@ theorem toListModel_expand [BEq α] [Hashable α] [PartialEquivBEq α]
     {buckets : {d : Array (AssocList α β) // 0 < d.size}} :
     Perm (toListModel (expand buckets).1) (toListModel buckets.1) := by
   simpa [expand, expand.go_eq] using toListModel_foldl_reinsertAux (toListModel buckets.1)
-    ⟨mkArray (buckets.1.size * 2) .nil, by simpa using Nat.mul_pos buckets.2 Nat.two_pos⟩
+    ⟨Array.replicate (buckets.1.size * 2) .nil, by simpa using Nat.mul_pos buckets.2 Nat.two_pos⟩
 
 theorem toListModel_expandIfNecessary [BEq α] [Hashable α] [PartialEquivBEq α] (m : Raw₀ α β) :
     Perm (toListModel (expandIfNecessary m).1.2) (toListModel m.1.2) := by

src/Std/Sat/AIG/CNF.lean

@@ -162,7 +162,7 @@ structure Cache.Inv (cnf : CNF (CNFVar aig)) (marks : Array Bool) (hmarks : mark
 /--
 The `Cache` invariant always holds for an empty CNF when all nodes are unmarked.
 -/
-theorem Cache.Inv_init : Inv ([] : CNF (CNFVar aig)) (mkArray aig.decls.size false) (by simp) where
+theorem Cache.Inv_init : Inv ([] : CNF (CNFVar aig)) (Array.replicate aig.decls.size false) (by simp) where
   hmark := by
     intro lhs rhs linv rinv idx hbound hmarked heq
     simp at hmarked
@@ -254,7 +254,7 @@ theorem Cache.IsExtensionBy_set (cache1 : Cache aig cnf1) (cache2 : Cache aig cn
 A cache with no entries is valid for an empty CNF.
 -/
 def Cache.init (aig : AIG Nat) : Cache aig [] where
-  marks := mkArray aig.decls.size false
+  marks := Array.replicate aig.decls.size false
   hmarks := by simp
   inv := Inv_init
 

src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean

@@ -74,6 +74,9 @@ instance [Clause α β] : Entails α β where
 instance [Clause α β] (p : α → Bool) (c : β) : Decidable (p ⊨ c) :=
   inferInstanceAs (Decidable (Clause.eval p c = true))
 
+instance [Clause α β] : Inhabited β where
+  default := empty
+
 end Clause
 
 /--

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.lean

@@ -67,7 +67,7 @@ can appear in the formula (hence why the parameter `n` is called `numVarsSucc` b
 namespace DefaultFormula
 
 instance {n : Nat} : Inhabited (DefaultFormula n) where
-  default := ⟨#[], #[], #[], Array.mkArray n unassigned⟩
+  default := ⟨#[], #[], #[], Array.replicate n unassigned⟩
 
 /-- Note: This function is only for reasoning about semantics. Its efficiency doesn't actually matter -/
 def toList {n : Nat} (f : DefaultFormula n) : List (DefaultClause n) :=
@@ -88,7 +88,7 @@ Note: This function assumes that the provided `clauses` Array is indexed accordi
 field invariant described in the DefaultFormula doc comment.
 -/
 def ofArray {n : Nat} (clauses : Array (Option (DefaultClause n))) : DefaultFormula n :=
-  let assignments := clauses.foldl ofArray_fold_fn (Array.mkArray n unassigned)
+  let assignments := clauses.foldl ofArray_fold_fn (Array.replicate n unassigned)
   ⟨clauses, #[], #[], assignments⟩
 
 def insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) : DefaultFormula n :=

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean

@@ -20,6 +20,7 @@ namespace DefaultFormula
 
 open Std.Sat
 open DefaultClause DefaultFormula Assignment
+open Array (replicate)
 
 /--
 This invariant states that if the `assignments` field of a default formula `f` indicates that `f`
@@ -107,17 +108,17 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
   · simp only [ofArray]
   · have hsize : (ofArray arr).assignments.size = n := by
       simp only [ofArray, ← Array.foldl_toList]
-      have hb : (mkArray n unassigned).size = n := by simp only [Array.size_mkArray]
+      have hb : (replicate n unassigned).size = n := by simp only [Array.size_replicate]
       have hl (acc : Array Assignment) (ih : acc.size = n) (cOpt : Option (DefaultClause n)) (_cOpt_in_arr : cOpt ∈ arr.toList) :
         (ofArray_fold_fn acc cOpt).size = n := by rw [size_ofArray_fold_fn acc cOpt, ih]
-      exact List.foldlRecOn arr.toList ofArray_fold_fn (mkArray n unassigned) hb hl
+      exact List.foldlRecOn arr.toList ofArray_fold_fn (replicate n unassigned) hb hl
     apply Exists.intro hsize
     let ModifiedAssignmentsInvariant (assignments : Array Assignment) : Prop :=
       ∃ hsize : assignments.size = n,
         ∀ i : PosFin n, ∀ b : Bool, hasAssignment b (assignments[i.1]'(by rw [hsize]; exact i.2.2)) →
         (unit (i, b)) ∈ toList (ofArray arr)
-    have hb : ModifiedAssignmentsInvariant (mkArray n unassigned) := by
-      have hsize : (mkArray n unassigned).size = n := by simp only [Array.size_mkArray]
+    have hb : ModifiedAssignmentsInvariant (replicate n unassigned) := by
+      have hsize : (replicate n unassigned).size = n := by simp only [Array.size_replicate]
       apply Exists.intro hsize
       intro i b h
       by_cases hb : b <;> simp [hasAssignment, hb, hasPosAssignment, hasNegAssignment] at h
@@ -185,7 +186,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
           · next i_ne_l =>
             simp only [Array.getElem_modify_of_ne (Ne.symm i_ne_l)] at h
             exact ih i b h
-    rcases List.foldlRecOn arr.toList ofArray_fold_fn (mkArray n unassigned) hb hl with ⟨_h_size, h'⟩
+    rcases List.foldlRecOn arr.toList ofArray_fold_fn (replicate n unassigned) hb hl with ⟨_h_size, h'⟩
     intro i b h
     simp only [ofArray, ← Array.foldl_toList] at h
     exact h' i b h

tests/lean/run/4171.lean

@@ -714,10 +714,8 @@ example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
 
 
 /--
-info: [simp] Diagnostics
-  [simp] theorems with bad keys
-    [simp] foo, key: @Quiver.Hom.unop _ _ _ _ (@Opposite.op (@Quiver.Hom _ _ _.1 _.1) _)
-  use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+info: [simp] theorems with bad keys
+  [simp] foo, key: @Quiver.Hom.unop _ _ _ _ (@Opposite.op (@Quiver.Hom _ _ _.1 _.1) _)use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
 example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
@@ -735,10 +733,8 @@ example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
 attribute [simp] foo
 
 /--
-info: [simp] Diagnostics
-  [simp] theorems with bad keys
-    [simp] foo, key: @Quiver.Hom.unop _ _ _ _ (@Opposite.op (@Quiver.Hom _ _ _.1 _.1) _)
-  use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+info: [simp] theorems with bad keys
+  [simp] foo, key: @Quiver.Hom.unop _ _ _ _ (@Opposite.op (@Quiver.Hom _ _ _.1 _.1) _)use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
 example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where

tests/lean/run/ack.lean

@@ -5,25 +5,21 @@ def ack : Nat → Nat → Nat
 termination_by a b => (a, b)
 
 /--
-info: [diag] Diagnostics
-  [reduction] unfolded declarations (max: 2567, num: 5):
-    [reduction] Nat.rec ↦ 2567
-    [reduction] Eq.rec ↦ 1517
-    [reduction] Acc.rec ↦ 1158
-    [reduction] Or.rec ↦ 770
-    [reduction] PSigma.rec ↦ 514
-  [reduction] unfolded reducible declarations (max: 2337, num: 4):
-    [reduction] Nat.casesOn ↦ 2337
-    [reduction] Eq.ndrec ↦ 1307
-    [reduction] Or.casesOn ↦ 770
-    [reduction] PSigma.casesOn ↦ 514
-  [kernel] unfolded declarations (max: 1193, num: 5):
-    [kernel] Nat.casesOn ↦ 1193
-    [kernel] Nat.rec ↦ 1065
-    [kernel] Eq.ndrec ↦ 973
-    [kernel] Eq.rec ↦ 973
-    [kernel] Acc.rec ↦ 754
-  use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+info: [reduction] unfolded declarations (max: 2567, num: 5):
+  [reduction] Nat.rec ↦ 2567
+  [reduction] Eq.rec ↦ 1517
+  [reduction] Acc.rec ↦ 1158
+  [reduction] Or.rec ↦ 770
+  [reduction] PSigma.rec ↦ 514[reduction] unfolded reducible declarations (max: 2337, num: 4):
+  [reduction] Nat.casesOn ↦ 2337
+  [reduction] Eq.ndrec ↦ 1307
+  [reduction] Or.casesOn ↦ 770
+  [reduction] PSigma.casesOn ↦ 514[kernel] unfolded declarations (max: 1193, num: 5):
+  [kernel] Nat.casesOn ↦ 1193
+  [kernel] Nat.rec ↦ 1065
+  [kernel] Eq.ndrec ↦ 973
+  [kernel] Eq.rec ↦ 973
+  [kernel] Acc.rec ↦ 754use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
 unseal ack in

tests/lean/run/diagRec.lean

@@ -7,15 +7,12 @@ termination_by n
 /--
 info: 89
 ---
-info: [diag] Diagnostics
-  [reduction] unfolded declarations (max: 407, num: 3):
-    [reduction] Nat.rec ↦ 407
-    [reduction] Or.rec ↦ 144
-    [reduction] Acc.rec ↦ 108
-  [reduction] unfolded reducible declarations (max: 352, num: 2):
-    [reduction] Nat.casesOn ↦ 352
-    [reduction] Or.casesOn ↦ 144
-  use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+info: [reduction] unfolded declarations (max: 407, num: 3):
+  [reduction] Nat.rec ↦ 407
+  [reduction] Or.rec ↦ 144
+  [reduction] Acc.rec ↦ 108[reduction] unfolded reducible declarations (max: 352, num: 2):
+  [reduction] Nat.casesOn ↦ 352
+  [reduction] Or.casesOn ↦ 144use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
 set_option diagnostics true in

tests/lean/run/diagnostics.lean

@@ -9,19 +9,15 @@ theorem f_eq : f (x + 1) = q (f x) := rfl
 set_option trace.Meta.debug true
 
 /--
-info: [diag] Diagnostics
-  [reduction] unfolded declarations (max: 15, num: 6):
-    [reduction] Nat.rec ↦ 15
-    [reduction] Add.add ↦ 10
-    [reduction] HAdd.hAdd ↦ 10
-    [reduction] Nat.add ↦ 10
-    [reduction] f ↦ 5
-    [reduction] OfNat.ofNat ↦ 5
-  [reduction] unfolded instances (max: 5, num: 1):
-    [reduction] instOfNatNat ↦ 5
-  [reduction] unfolded reducible declarations (max: 15, num: 1):
-    [reduction] Nat.casesOn ↦ 15
-  use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+info: [reduction] unfolded declarations (max: 15, num: 6):
+  [reduction] Nat.rec ↦ 15
+  [reduction] Add.add ↦ 10
+  [reduction] HAdd.hAdd ↦ 10
+  [reduction] Nat.add ↦ 10
+  [reduction] f ↦ 5
+  [reduction] OfNat.ofNat ↦ 5[reduction] unfolded instances (max: 5, num: 1):
+  [reduction] instOfNatNat ↦ 5[reduction] unfolded reducible declarations (max: 15, num: 1):
+  [reduction] Nat.casesOn ↦ 15use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
 example : f (x + 5) = q (q (q (q (q (f x))))) :=
@@ -30,19 +26,15 @@ example : f (x + 5) = q (q (q (q (q (f x))))) :=
   rfl
 
 /--
-info: [diag] Diagnostics
-  [reduction] unfolded declarations (max: 15, num: 6):
-    [reduction] Nat.rec ↦ 15
-    [reduction] Add.add ↦ 10
-    [reduction] HAdd.hAdd ↦ 10
-    [reduction] Nat.add ↦ 10
-    [reduction] f ↦ 5
-    [reduction] OfNat.ofNat ↦ 5
-  [reduction] unfolded instances (max: 5, num: 1):
-    [reduction] instOfNatNat ↦ 5
-  [reduction] unfolded reducible declarations (max: 15, num: 1):
-    [reduction] Nat.casesOn ↦ 15
-  use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+info: [reduction] unfolded declarations (max: 15, num: 6):
+  [reduction] Nat.rec ↦ 15
+  [reduction] Add.add ↦ 10
+  [reduction] HAdd.hAdd ↦ 10
+  [reduction] Nat.add ↦ 10
+  [reduction] f ↦ 5
+  [reduction] OfNat.ofNat ↦ 5[reduction] unfolded instances (max: 5, num: 1):
+  [reduction] instOfNatNat ↦ 5[reduction] unfolded reducible declarations (max: 15, num: 1):
+  [reduction] Nat.casesOn ↦ 15use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
 example : f (x + 5) = q (q (q (q (q (f x))))) := by

tests/lean/run/grind_offset.lean

@@ -23,7 +23,7 @@ info: [grind.assert] f (y + 1) = a
 [grind.assert] f (y + 1) = g (f y)
 -/
 #guard_msgs (info) in
-example : f (y + 1) = a → a = g (f y) := by
+example : f (y + 1) = a → a = g (f y):= by
   grind
 
 /--

tests/lean/run/grind_params.lean

@@ -1,81 +0,0 @@
-def foo (x : Nat) := x + 2
-
-example (f : Nat → Nat) : f (foo a) = b → f (c + 1) = d → c = a + 1 → b = d := by
-  grind [foo]
-
-opaque bla : Nat → Nat
-theorem blathm : bla (bla x) = bla x := sorry
-
-example : bla (foo a) = b → bla b = bla (a + 2) := by
-  grind [foo, blathm]
-
-example : bla (foo a) = b → bla b = bla (a + 2) := by
-  grind [foo, = blathm]
-
-/--
-error: invalid `grind` forward theorem, theorem `blathm` does not have propositional hypotheses
--/
-#guard_msgs (error) in
-example : bla (foo a) = b → bla b = bla (a + 2) := by
-  grind [foo, → blathm]
-
-opaque P : Nat → Prop
-opaque Q : Nat → Prop
-opaque R : Nat → Prop
-
-theorem pq : P x → Q x := sorry
-theorem qr : Q x → R x := sorry
-
-example : P x → R x := by
-  grind [→ pq, → qr]
-
-/--
-error: `grind` failed
-case grind
-x : Nat
-a✝ : P x
-x✝ : ¬R x
-⊢ False
-[grind] Diagnostics
-  [facts] Asserted facts
-    [prop] P x
-    [prop] ¬R x
-  [eqc] True propositions
-    [prop] P x
-  [eqc] False propositions
-    [prop] R x
-  [ematch] E-matching
-    [thm] pq:
-        ∀ {x : Nat}, P x → Q x
-        patterns: [Q #1]
-    [thm] qr: ∀ {x : Nat}, Q x → R x patterns: [Q #1]
--/
-#guard_msgs (error) in
-example : P x → R x := by
-  grind [← pq, → qr]
-
-example : P x → R x := by
-  grind [← pq, ← qr]
-
-attribute [grind] blathm
-
-example : bla (bla (bla (bla x))) = bla x := by
-  grind
-
-example : bla (bla (bla (bla x))) = bla x := by
-  fail_if_success grind [-blathm]
-  sorry
-
-example : bla (bla (bla (bla x))) = bla x := by
-  grind only [blathm]
-
-example : bla (bla (bla (bla x))) = bla x := by
-  fail_if_success grind only
-  sorry
-
-/--
-error: `pq` is not marked with the `[grind]` attribute
--/
-#guard_msgs (error) in
-example : P x → R x := by
-  grind [-pq]

tests/lean/run/grind_t1.lean

@@ -290,6 +290,3 @@ example {m n : Nat} : m < n ↔ m ≤ n ∧ ¬ n ≤ m := by
 
 example {α} (f : α → Type) (a : α) (h : ∀ x, Nonempty (f x)) : Nonempty (f a) := by
   grind
-
-example {α β} (f : α → β) (a : α) : ∃ a', f a' = f a := by
-  grind

tests/lean/run/simpDiag.lean

@@ -8,14 +8,11 @@ theorem f_eq : f (x + 1) = q (f x) := rfl
 axiom q_eq (x : Nat) : q x = x
 
 /--
-info: [simp] Diagnostics
-  [simp] used theorems (max: 50, num: 2):
-    [simp] f_eq ↦ 50
-    [simp] q_eq ↦ 50
-  [simp] tried theorems (max: 101, num: 2):
-    [simp] f_eq ↦ 101, succeeded: 50
-    [simp] q_eq ↦ 50, succeeded: 50
-  use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+info: [simp] used theorems (max: 50, num: 2):
+  [simp] f_eq ↦ 50
+  [simp] q_eq ↦ 50[simp] tried theorems (max: 101, num: 2):
+  [simp] f_eq ↦ 101, succeeded: 50
+  [simp] q_eq ↦ 50, succeeded: 50use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
 example : f (x + 50) = f x := by
@@ -32,15 +29,12 @@ def ack : Nat → Nat → Nat
   | x+1, y+1 => ack x (ack (x+1) y)
 
 /--
-info: [simp] Diagnostics
-  [simp] used theorems (max: 1201, num: 3):
-    [simp] ack.eq_3 ↦ 1201
-    [simp] Nat.reduceAdd (builtin simproc) ↦ 771
-    [simp] ack.eq_1 ↦ 768
-  [simp] tried theorems (max: 1973, num: 2):
-    [simp] ack.eq_3 ↦ 1973, succeeded: 1201
-    [simp] ack.eq_1 ↦ 768, succeeded: 768
-  use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+info: [simp] used theorems (max: 1201, num: 3):
+  [simp] ack.eq_3 ↦ 1201
+  [simp] Nat.reduceAdd (builtin simproc) ↦ 771
+  [simp] ack.eq_1 ↦ 768[simp] tried theorems (max: 1973, num: 2):
+  [simp] ack.eq_3 ↦ 1973, succeeded: 1201
+  [simp] ack.eq_1 ↦ 768, succeeded: 768use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 ---
 error: tactic 'simp' failed, nested error:
 maximum recursion depth has been reached
@@ -98,21 +92,15 @@ opaque q1 : Nat → Nat → Prop
 @[simp] axiom q1_ax (x : Nat) : q1 x 10
 
 /--
-info: [simp] Diagnostics
-  [simp] used theorems (max: 1, num: 1):
-    [simp] q1_ax ↦ 1
-  [simp] tried theorems (max: 1, num: 1):
-    [simp] q1_ax ↦ 1, succeeded: 1
-  use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+info: [simp] used theorems (max: 1, num: 1):
+  [simp] q1_ax ↦ 1[simp] tried theorems (max: 1, num: 1):
+  [simp] q1_ax ↦ 1, succeeded: 1use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 ---
-info: [diag] Diagnostics
-  [reduction] unfolded declarations (max: 246, num: 2):
-    [reduction] Nat.rec ↦ 246
-    [reduction] OfNat.ofNat ↦ 24
-  [reduction] unfolded reducible declarations (max: 246, num: 2):
-    [reduction] h ↦ 246
-    [reduction] Nat.casesOn ↦ 246
-  use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+info: [reduction] unfolded declarations (max: 246, num: 2):
+  [reduction] Nat.rec ↦ 246
+  [reduction] OfNat.ofNat ↦ 24[reduction] unfolded reducible declarations (max: 246, num: 2):
+  [reduction] h ↦ 246
+  [reduction] Nat.casesOn ↦ 246use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
 example : q1 x (h 40) := by