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,155 +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_replicate : (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
-
 /-! 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.
@@ -3324,6 +3185,54 @@ 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

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/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,103 +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]
-
 /-! 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) :

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/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/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/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/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/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