feat: deprecate Array.mkArray in favour of Array.replicate

src/Init/Data/Array/Attach.lean

@@ -743,10 +743,13 @@ and simplifies these to the function directly taking the value.
     List.map_toArray, List.map_flatten, map_subtype, map_id_fun', List.unattach_toArray, mk.injEq]
   simp only [List.unattach]
 
-@[simp] theorem unattach_mkArray {p : α → Prop} {n : Nat} {x : { x // p x }} :
+@[simp] theorem unattach_replicate {p : α → Prop} {n : Nat} {x : { x // p x }} :
-    (Array.mkArray n x).unattach = Array.mkArray n x.1 := by
+    (Array.replicate n x).unattach = Array.replicate n x.1 := by
   simp [unattach]
 
+@[deprecated unattach_replicate (since := "2025-03-18")]
+abbrev unattach_mkArray := @unattach_replicate
+
 /-! ### Well-founded recursion preprocessing setup -/
 
 @[wf_preprocess] theorem Array.map_wfParam (xs : Array α) (f : α → β) :

src/Init/Data/Array/Basic.lean

@@ -202,12 +202,26 @@ Creates an array that contains `n` repetitions of `v`.
 
 The corresponding `List` function is `List.replicate`.
 
+Examples:
+ * `Array.replicate 2 true = #[true, true]`
+ * `Array.replicate 3 () = #[(), (), ()]`
+ * `Array.replicate 0 "anything" = #[]`
+-/
+@[extern "lean_mk_array"]
+def replicate {α : Type u} (n : Nat) (v : α) : Array α where
+  toList := List.replicate n v
+
+/--
+Creates an array that contains `n` repetitions of `v`.
+
+The corresponding `List` function is `List.replicate`.
+
 Examples:
  * `Array.mkArray 2 true = #[true, true]`
  * `Array.mkArray 3 () = #[(), (), ()]`
  * `Array.mkArray 0 "anything" = #[]`
 -/
-@[extern "lean_mk_array"]
+@[extern "lean_mk_array", deprecated replicate (since := "2025-03-18")]
 def mkArray {α : Type u} (n : Nat) (v : α) : Array α where
   toList := List.replicate n v
 
@@ -2056,7 +2070,7 @@ Examples:
  * `#["red", "green", "blue"].leftpad 3 "blank" = #["red", "green", "blue"]`
  * `#["red", "green", "blue"].leftpad 1 "blank" = #["red", "green", "blue"]`
 -/
-def leftpad (n : Nat) (a : α) (xs : Array α) : Array α := mkArray (n - xs.size) a ++ xs
+def leftpad (n : Nat) (a : α) (xs : Array α) : Array α := replicate (n - xs.size) a ++ xs
 
 /--
 Pads `xs : Array α` on the right with repeated occurrences of `a : α` until it is of length `n`. If
@@ -2068,7 +2082,7 @@ Examples:
  * `#["red", "green", "blue"].rightpad 3 "blank" = #["red", "green", "blue"]`
  * `#["red", "green", "blue"].rightpad 1 "blank" = #["red", "green", "blue"]`
 -/
-def rightpad (n : Nat) (a : α) (xs : Array α) : Array α := xs ++ mkArray (n - xs.size) a
+def rightpad (n : Nat) (a : α) (xs : Array α) : Array α := xs ++ replicate (n - xs.size) a
 
 /- ### reduceOption -/
 

src/Init/Data/Array/Count.lean

@@ -88,10 +88,13 @@ theorem countP_le_size : countP p xs ≤ xs.size := by
   rcases xs with ⟨xs⟩
   simp
 
-theorem countP_mkArray (p : α → Bool) (a : α) (n : Nat) :
+theorem countP_replicate (p : α → Bool) (a : α) (n : Nat) :
-    countP p (mkArray n a) = if p a then n else 0 := by
+    countP p (replicate n a) = if p a then n else 0 := by
   simp [← List.toArray_replicate, List.countP_replicate]
 
+@[deprecated countP_replicate (since := "2025-03-18")]
+abbrev countP_mkArray := @countP_replicate
+
 theorem boole_getElem_le_countP (p : α → Bool) (xs : Array α) (i : Nat) (h : i < xs.size) :
     (if p xs[i] then 1 else 0) ≤ xs.countP p := by
   rcases xs with ⟨xs⟩
@@ -241,25 +244,34 @@ theorem count_eq_size {xs : Array α} : count a xs = xs.size ↔ ∀ b ∈ xs, a
   · simpa using h b hb
   · rw [h b hb, beq_self_eq_true]
 
-@[simp] theorem count_mkArray_self (a : α) (n : Nat) : count a (mkArray n a) = n := by
+@[simp] theorem count_replicate_self (a : α) (n : Nat) : count a (replicate n a) = n := by
   simp [← List.toArray_replicate]
 
-theorem count_mkArray (a b : α) (n : Nat) : count a (mkArray n b) = if b == a then n else 0 := by
+@[deprecated count_replicate_self (since := "2025-03-18")]
+abbrev count_mkArray_self := @count_replicate_self
+
+theorem count_replicate (a b : α) (n : Nat) : count a (replicate n b) = if b == a then n else 0 := by
   simp [← List.toArray_replicate, List.count_replicate]
 
-theorem filter_beq (xs : Array α) (a : α) : xs.filter (· == a) = mkArray (count a xs) a := by
+@[deprecated count_replicate (since := "2025-03-18")]
+abbrev count_mkArray := @count_replicate
+
+theorem filter_beq (xs : Array α) (a : α) : xs.filter (· == a) = replicate (count a xs) a := by
   rcases xs with ⟨xs⟩
   simp [List.filter_beq]
 
-theorem filter_eq {α} [DecidableEq α] (xs : Array α) (a : α) : xs.filter (· = a) = mkArray (count a xs) a :=
+theorem filter_eq {α} [DecidableEq α] (xs : Array α) (a : α) : xs.filter (· = a) = replicate (count a xs) a :=
   filter_beq xs a
 
-theorem mkArray_count_eq_of_count_eq_size {xs : Array α} (h : count a xs = xs.size) :
+theorem replicate_count_eq_of_count_eq_size {xs : Array α} (h : count a xs = xs.size) :
-    mkArray (count a xs) a = xs := by
+    replicate (count a xs) a = xs := by
   rcases xs with ⟨xs⟩
   rw [← toList_inj]
   simp [List.replicate_count_eq_of_count_eq_length (by simpa using h)]
 
+@[deprecated replicate_count_eq_of_count_eq_size (since := "2025-03-18")]
+abbrev mkArray_count_eq_of_count_eq_size := @replicate_count_eq_of_count_eq_size
+
 @[simp] theorem count_filter {xs : Array α} (h : p a) : count a (filter p xs) = count a xs := by
   rcases xs with ⟨xs⟩
   simp [List.count_filter, h]

src/Init/Data/Array/Erase.lean

@@ -122,21 +122,30 @@ theorem eraseP_append {xs : Array α} {ys : Array α} :
   simp only [List.append_toArray, List.eraseP_toArray, List.eraseP_append, List.any_toArray]
   split <;> simp
 
-theorem eraseP_mkArray (n : Nat) (a : α) (p : α → Bool) :
+theorem eraseP_replicate (n : Nat) (a : α) (p : α → Bool) :
-    (mkArray n a).eraseP p = if p a then mkArray (n - 1) a else mkArray n a := by
+    (replicate n a).eraseP p = if p a then replicate (n - 1) a else replicate n a := by
   simp only [← List.toArray_replicate, List.eraseP_toArray, List.eraseP_replicate]
   split <;> simp
 
-@[simp] theorem eraseP_mkArray_of_pos {n : Nat} {a : α} (h : p a) :
+@[deprecated eraseP_replicate (since := "2025-03-18")]
-    (mkArray n a).eraseP p = mkArray (n - 1) a := by
+abbrev eraseP_mkArray := @eraseP_replicate
+
+@[simp] theorem eraseP_replicate_of_pos {n : Nat} {a : α} (h : p a) :
+    (replicate n a).eraseP p = replicate (n - 1) a := by
   simp only [← List.toArray_replicate, List.eraseP_toArray]
   simp [h]
 
-@[simp] theorem eraseP_mkArray_of_neg {n : Nat} {a : α} (h : ¬p a) :
+@[deprecated eraseP_replicate_of_pos (since := "2025-03-18")]
-    (mkArray n a).eraseP p = mkArray n a := by
+abbrev eraseP_mkArray_of_pos := @eraseP_replicate_of_pos
+
+@[simp] theorem eraseP_replicate_of_neg {n : Nat} {a : α} (h : ¬p a) :
+    (replicate n a).eraseP p = replicate n a := by
   simp only [← List.toArray_replicate, List.eraseP_toArray]
   simp [h]
 
+@[deprecated eraseP_replicate_of_neg (since := "2025-03-18")]
+abbrev eraseP_mkArray_of_neg := @eraseP_replicate_of_neg
+
 theorem eraseP_eq_iff {p} {xs : Array α} :
     xs.eraseP p = ys ↔
       ((∀ a ∈ xs, ¬ p a) ∧ xs = ys) ∨
@@ -243,12 +252,15 @@ theorem erase_append [LawfulBEq α] {a : α} {xs ys : Array α} :
   simp only [List.append_toArray, List.erase_toArray, List.erase_append, mem_toArray]
   split <;> simp
 
-theorem erase_mkArray [LawfulBEq α] (n : Nat) (a b : α) :
+theorem erase_replicate [LawfulBEq α] (n : Nat) (a b : α) :
-    (mkArray n a).erase b = if b == a then mkArray (n - 1) a else mkArray n a := by
+    (replicate n a).erase b = if b == a then replicate (n - 1) a else replicate n a := by
   simp only [← List.toArray_replicate, List.erase_toArray]
   simp only [List.erase_replicate, beq_iff_eq, List.toArray_replicate]
   split <;> simp
 
+@[deprecated erase_replicate (since := "2025-03-18")]
+abbrev erase_mkArray := @erase_replicate
+
 theorem erase_comm [LawfulBEq α] (a b : α) (xs : Array α) :
     (xs.erase a).erase b = (xs.erase b).erase a := by
   rcases xs with ⟨xs⟩
@@ -268,16 +280,22 @@ theorem erase_eq_iff [LawfulBEq α] {a : α} {xs : Array α} :
     · left; simp_all
     · right; refine ⟨a, as, h, rfl, bs, by simp⟩
 
-@[simp] theorem erase_mkArray_self [LawfulBEq α] {a : α} :
+@[simp] theorem erase_replicate_self [LawfulBEq α] {a : α} :
-    (mkArray n a).erase a = mkArray (n - 1) a := by
+    (replicate n a).erase a = replicate (n - 1) a := by
   simp only [← List.toArray_replicate, List.erase_toArray]
   simp [List.erase_replicate]
 
-@[simp] theorem erase_mkArray_ne [LawfulBEq α] {a b : α} (h : !b == a) :
+@[deprecated erase_replicate_self (since := "2025-03-18")]
-    (mkArray n a).erase b = mkArray n a := by
+abbrev erase_mkArray_self := @erase_replicate_self
+
+@[simp] theorem erase_replicate_ne [LawfulBEq α] {a b : α} (h : !b == a) :
+    (replicate n a).erase b = replicate n a := by
   rw [erase_of_not_mem]
   simp_all
 
+@[deprecated erase_replicate_ne (since := "2025-03-18")]
+abbrev erase_mkArray_ne := @erase_replicate_ne
+
 end erase
 
 /-! ### eraseIdx -/
@@ -353,12 +371,15 @@ theorem eraseIdx_append_of_length_le {xs : Array α} {k : Nat} (hk : xs.size ≤
   simp at hk
   simp [List.eraseIdx_append_of_length_le, *]
 
-theorem eraseIdx_mkArray {n : Nat} {a : α} {k : Nat} {h} :
+theorem eraseIdx_replicate {n : Nat} {a : α} {k : Nat} {h} :
-    (mkArray n a).eraseIdx k = mkArray (n - 1) a := by
+    (replicate n a).eraseIdx k = replicate (n - 1) a := by
   simp at h
   simp only [← List.toArray_replicate, List.eraseIdx_toArray]
   simp [List.eraseIdx_replicate, h]
 
+@[deprecated eraseIdx_replicate (since := "2025-03-18")]
+abbrev eraseIdx_mkArray := @eraseIdx_replicate
+
 theorem mem_eraseIdx_iff_getElem {x : α} {xs : Array α} {k} {h} : x ∈ xs.eraseIdx k h ↔ ∃ i w, i ≠ k ∧ xs[i]'w = x := by
   rcases xs with ⟨xs⟩
   simp [List.mem_eraseIdx_iff_getElem, *]

src/Init/Data/Array/Extract.lean

@@ -249,12 +249,15 @@ theorem extract_append_left {as bs : Array α} :
   · simp only [size_map, size_extract] at h₁ h₂
     simp only [getElem_map, getElem_extract]
 
-@[simp] theorem extract_mkArray {a : α} {n i j : Nat} :
+@[simp] theorem extract_replicate {a : α} {n i j : Nat} :
-    (mkArray n a).extract i j = mkArray (min j n - i) a := by
+    (replicate n a).extract i j = replicate (min j n - i) a := by
   ext l h₁ h₂
   · simp
-  · simp only [size_extract, size_mkArray] at h₁ h₂
+  · simp only [size_extract, size_replicate] at h₁ h₂
-    simp only [getElem_extract, getElem_mkArray]
+    simp only [getElem_extract, getElem_replicate]
+
+@[deprecated extract_replicate (since := "2025-03-18")]
+abbrev extract_mkArray := @extract_replicate
 
 theorem extract_eq_extract_right {as : Array α} {i j j' : Nat} :
     as.extract i j = as.extract i j' ↔ min (j - i) (as.size - i) = min (j' - i) (as.size - i) := by
@@ -387,24 +390,36 @@ theorem popWhile_append {xs ys : Array α} :
   rw [List.dropWhile_append_of_pos]
   simpa
 
-@[simp] theorem takeWhile_mkArray_eq_filter (p : α → Bool) :
+@[simp] theorem takeWhile_replicate_eq_filter (p : α → Bool) :
-    (mkArray n a).takeWhile p = (mkArray n a).filter p := by
+    (replicate n a).takeWhile p = (replicate n a).filter p := by
   simp [← List.toArray_replicate]
 
-theorem takeWhile_mkArray (p : α → Bool) :
+@[deprecated takeWhile_replicate_eq_filter (since := "2025-03-18")]
-    (mkArray n a).takeWhile p = if p a then mkArray n a else #[] := by
+abbrev takeWhile_mkArray_eq_filter := @takeWhile_replicate_eq_filter
-  simp [takeWhile_mkArray_eq_filter, filter_mkArray]
 
-@[simp] theorem popWhile_mkArray_eq_filter_not (p : α → Bool) :
+theorem takeWhile_replicate (p : α → Bool) :
-    (mkArray n a).popWhile p = (mkArray n a).filter (fun a => !p a) := by
+    (replicate n a).takeWhile p = if p a then replicate n a else #[] := by
+  simp [takeWhile_replicate_eq_filter, filter_replicate]
+
+@[deprecated takeWhile_replicate (since := "2025-03-18")]
+abbrev takeWhile_mkArray := @takeWhile_replicate
+
+@[simp] theorem popWhile_replicate_eq_filter_not (p : α → Bool) :
+    (replicate n a).popWhile p = (replicate n a).filter (fun a => !p a) := by
   simp [← List.toArray_replicate, ← List.filter_reverse]
 
-theorem popWhile_mkArray (p : α → Bool) :
+@[deprecated popWhile_replicate_eq_filter_not (since := "2025-03-18")]
-    (mkArray n a).popWhile p = if p a then #[] else mkArray n a := by
+abbrev popWhile_mkArray_eq_filter_not := @popWhile_replicate_eq_filter_not
-  simp only [popWhile_mkArray_eq_filter_not, size_mkArray, filter_mkArray, Bool.not_eq_eq_eq_not,
+
+theorem popWhile_replicate (p : α → Bool) :
+    (replicate n a).popWhile p = if p a then #[] else replicate n a := by
+  simp only [popWhile_replicate_eq_filter_not, size_replicate, filter_replicate, Bool.not_eq_eq_eq_not,
     Bool.not_true]
   split <;> simp_all
 
+@[deprecated popWhile_replicate (since := "2025-03-18")]
+abbrev popWhile_mkArray := @popWhile_replicate
+
 theorem extract_takeWhile {as : Array α} {i : Nat} :
     (as.takeWhile p).extract 0 i = (as.extract 0 i).takeWhile p := by
   rcases as with ⟨as⟩

src/Init/Data/Array/Find.lean

@@ -99,21 +99,33 @@ theorem getElem_zero_flatten {xss : Array (Array α)} (h) :
   simp [getElem?_eq_getElem, h] at t
   simp [← t]
 
-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
+@[deprecated findSome?_replicate (since := "2025-03-18")]
-  simp [findSome?_mkArray, Nat.ne_of_gt h]
+abbrev findSome?_mkArray := @findSome?_replicate
+
+@[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]
+
+@[deprecated findSome?_replicate_of_pos (since := "2025-03-18")]
+abbrev findSome?_mkArray_of_pos := @findSome?_replicate_of_pos
 
 -- Argument is unused, but used to decide whether `simp` should unfold.
-@[simp] theorem findSome?_mkArray_of_isSome (_ : (f a).isSome) :
+@[simp] theorem findSome?_replicate_of_isSome (_ : (f a).isSome) :
-   findSome? f (mkArray n a) = if n = 0 then none else f a := by
+   findSome? f (replicate n a) = if n = 0 then none else f a := by
-  simp [findSome?_mkArray]
+  simp [findSome?_replicate]
 
-@[simp] theorem findSome?_mkArray_of_isNone (h : (f a).isNone) :
+@[deprecated findSome?_replicate_of_isSome (since := "2025-03-18")]
-    findSome? f (mkArray n a) = none := by
+abbrev findSome?_mkArray_of_isSome := @findSome?_replicate_of_isSome
+
+@[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_of_isNone (since := "2025-03-18")]
+abbrev findSome?_mkArray_of_isNone := @findSome?_replicate_of_isNone
 
 /-! ### find? -/
 
@@ -254,40 +266,58 @@ theorem find?_flatMap_eq_none_iff {xs : Array α} {f : α → Array β} {p : β
 @[deprecated find?_flatMap_eq_none_iff (since := "2025-02-03")]
 abbrev find?_flatMap_eq_none := @find?_flatMap_eq_none_iff
 
-theorem find?_mkArray :
+theorem find?_replicate :
-    find? p (mkArray n a) = if n = 0 then none else if p a then some a else none := by
+    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) :
+@[deprecated find?_replicate (since := "2025-03-18")]
-    find? p (mkArray n a) = if p a then some a else none := by
+abbrev find?_mkArray := @find?_replicate
-  simp [find?_mkArray, Nat.ne_of_gt h]
 
-@[simp] theorem find?_mkArray_of_pos (h : p a) :
+@[simp] theorem find?_replicate_of_size_pos (h : 0 < n) :
-    find? p (mkArray n a) = if n = 0 then none else some a := by
+    find? p (replicate n a) = if p a then some a else none := by
-  simp [find?_mkArray, h]
+  simp [find?_replicate, Nat.ne_of_gt h]
 
-@[simp] theorem find?_mkArray_of_neg (h : ¬ p a) : find? p (mkArray n a) = none := by
+@[deprecated find?_replicate_of_size_pos (since := "2025-03-18")]
-  simp [find?_mkArray, h]
+abbrev find?_mkArray_of_length_pos := @find?_replicate_of_size_pos
+
+@[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]
+
+@[deprecated find?_replicate_of_pos (since := "2025-03-18")]
+abbrev find?_mkArray_of_pos := @find?_replicate_of_pos
+
+@[simp] theorem find?_replicate_of_neg (h : ¬ p a) : find? p (replicate n a) = none := by
+  simp [find?_replicate, h]
+
+@[deprecated find?_replicate_of_neg (since := "2025-03-18")]
+abbrev find?_mkArray_of_neg := @find?_replicate_of_neg
 
 -- 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_iff {n : Nat} {a : α} {p : α → Bool} :
+theorem find?_replicate_eq_none_iff {n : Nat} {a : α} {p : α → Bool} :
-    (mkArray n a).find? p = none ↔ n = 0 ∨ !p a := by
+    (replicate n a).find? p = none ↔ n = 0 ∨ !p a := by
   simp [← List.toArray_replicate, List.find?_replicate_eq_none_iff, Classical.or_iff_not_imp_left]
 
-@[deprecated find?_mkArray_eq_none_iff (since := "2025-02-03")]
+@[deprecated find?_replicate_eq_none_iff (since := "2025-03-18")]
-abbrev find?_mkArray_eq_none := @find?_mkArray_eq_none_iff
+abbrev find?_mkArray_eq_none_iff := @find?_replicate_eq_none_iff
 
-@[simp] theorem find?_mkArray_eq_some_iff {n : Nat} {a b : α} {p : α → Bool} :
+@[simp] theorem find?_replicate_eq_some_iff {n : Nat} {a b : α} {p : α → Bool} :
-    (mkArray n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b := by
+    (replicate n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b := by
   simp [← List.toArray_replicate]
 
-@[deprecated find?_mkArray_eq_some_iff (since := "2025-02-03")]
+@[deprecated find?_replicate_eq_some_iff (since := "2025-03-18")]
-abbrev find?_mkArray_eq_some := @find?_mkArray_eq_some_iff
+abbrev find?_mkArray_eq_some_iff := @find?_replicate_eq_some_iff
 
-@[simp] theorem get_find?_mkArray (n : Nat) (a : α) (p : α → Bool) (h) :
+@[deprecated find?_replicate_eq_some_iff (since := "2025-02-03")]
-    ((mkArray n a).find? p).get h = a := by
+abbrev find?_mkArray_eq_some := @find?_replicate_eq_some_iff
+
+@[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 get_find?_replicate (since := "2025-03-18")]
+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
@@ -481,12 +511,15 @@ theorem findIdx?_flatten {xss : Array (Array α)} {p : α → Bool} :
   cases xss using array₂_induction
   simp [List.findIdx?_flatten, Function.comp_def]
 
-@[simp] theorem findIdx?_mkArray :
+@[simp] theorem findIdx?_replicate :
-    (mkArray n a).findIdx? p = if 0 < n ∧ p a then some 0 else none := by
+    (replicate n a).findIdx? p = if 0 < n ∧ p a then some 0 else none := by
   rw [← List.toArray_replicate]
   simp only [List.findIdx?_toArray]
   simp
 
+@[deprecated findIdx?_replicate (since := "2025-03-18")]
+abbrev findIdx?_mkArray := @findIdx?_replicate
+
 theorem findIdx?_eq_findSome?_zipIdx {xs : Array α} {p : α → Bool} :
     xs.findIdx? p = xs.zipIdx.findSome? fun ⟨a, i⟩ => if p a then some i else none := by
   rcases xs with ⟨xs⟩

src/Init/Data/Array/Lemmas.lean

@@ -321,27 +321,45 @@ theorem eq_push_of_size_ne_zero {xs : Array α} (h : xs.size ≠ 0) :
 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
+@[deprecated size_replicate (since := "2025-03-18")]
-  simp only [mkArray]
+abbrev size_mkArray := @size_replicate
 
-@[simp] theorem mkArray_zero : mkArray 0 a = #[] := rfl
+@[simp] theorem toList_replicate : (replicate n a).toList = List.replicate n a := by
+  simp only [replicate]
 
-theorem mkArray_succ : mkArray (n + 1) a = (mkArray n a).push a := by
+@[deprecated toList_replicate (since := "2025-03-18")]
+abbrev toList_mkArray := @toList_replicate
+
+@[simp] theorem replicate_zero : replicate 0 a = #[] := rfl
+
+@[deprecated replicate_zero (since := "2025-03-18")]
+abbrev mkArray_zero := @replicate_zero
+
+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) :
+@[deprecated replicate_succ (since := "2025-03-18")]
-    (mkArray n v)[i] = v := by simp [← getElem_toList]
+abbrev mkArray_succ := @replicate_succ
 
-theorem getElem?_mkArray (n : Nat) (v : α) (i : Nat) :
+@[simp] theorem getElem_replicate (n : Nat) (v : α) (h : i < (replicate n v).size) :
-    (mkArray n v)[i]? = if i < n then some v else none := by
+    (replicate n v)[i] = v := by simp [← getElem_toList]
+
+@[deprecated getElem_replicate (since := "2025-03-18")]
+abbrev getElem_mkArray := @getElem_replicate
+
+@[simp] 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 getElem?_replicate (since := "2025-03-18")]
+abbrev getElem?_mkArray := @getElem?_replicate
+
 /-! ### mem -/
 
 theorem not_mem_empty (a : α) : ¬ a ∈ #[] := by simp
@@ -1037,15 +1055,18 @@ 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} :
+@[simp] theorem replicate_beq_replicate [BEq α] {a b : α} {n : Nat} :
-    (mkArray n a == mkArray n b) = (n == 0 || a == b) := by
+    (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-03-18")]
+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
@@ -2306,147 +2327,234 @@ theorem flatMap_eq_foldl (f : α → Array β) (xs : Array α) :
     rw [List.foldl_cons, ih]
     simp [toArray_append]
 
-/-! ### mkArray -/
+/-! ### replicate -/
 
-@[simp] theorem mkArray_one : mkArray 1 a = #[a] := rfl
+@[simp] theorem replicate_one : replicate 1 a = #[a] := rfl
 
-/-- Variant of `mkArray_succ` that prepends `a` at the beginning of the array. -/
+@[deprecated replicate_one (since := "2025-03-18")]
-theorem mkArray_succ' : mkArray (n + 1) a = #[a] ++ mkArray n a := by
+abbrev mkArray_one := @replicate_one
+
+/-- Variant of `replicate_succ` that prepends `a` at the beginning of the array. -/
+theorem replicate_succ' : replicate (n + 1) a = #[a] ++ replicate 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
+@[deprecated replicate_succ' (since := "2025-03-18")]
-  unfold mkArray
+abbrev mkArray_succ' := @replicate_succ'
+
+@[simp] theorem mem_replicate {a b : α} {n} : b ∈ replicate n a ↔ n ≠ 0 ∧ b = a := by
+  unfold replicate
   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
+@[deprecated mem_replicate (since := "2025-03-18")]
+abbrev mem_mkArray := @mem_replicate
 
-theorem forall_mem_mkArray {p : α → Prop} {a : α} {n} :
+theorem eq_of_mem_replicate {a b : α} {n} (h : b ∈ replicate n a) : b = a := (mem_replicate.1 h).2
-    (∀ 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
+@[deprecated eq_of_mem_mkArray (since := "2025-03-18")]
-  simp [mkArray_succ]
+abbrev eq_of_mem_mkArray := @eq_of_mem_replicate
 
-@[simp] theorem mkArray_eq_empty_iff {n : Nat} (a : α) : mkArray n a = #[] ↔ n = 0 := by
+theorem forall_mem_replicate {p : α → Prop} {a : α} {n} :
+    (∀ b, b ∈ replicate n a → p b) ↔ n = 0 ∨ p a := by
+  cases n <;> simp [mem_replicate]
+
+@[deprecated forall_mem_replicate (since := "2025-03-18")]
+abbrev forall_mem_mkArray := @forall_mem_replicate
+
+@[simp] theorem replicate_succ_ne_empty (n : Nat) (a : α) : replicate (n+1) a ≠ #[] := by
+  simp [replicate_succ]
+
+@[deprecated replicate_succ_ne_empty (since := "2025-03-18")]
+abbrev mkArray_succ_ne_empty := @replicate_succ_ne_empty
+
+@[simp] theorem replicate_eq_empty_iff {n : Nat} (a : α) : replicate n a = #[] ↔ n = 0 := by
   cases n <;> simp
 
-@[simp] theorem getElem?_mkArray_of_lt {n : Nat} {i : Nat} (h : i < n) : (mkArray n a)[i]? = some a := by
+@[deprecated replicate_eq_empty_iff (since := "2025-03-18")]
-  simp [getElem?_mkArray, h]
+abbrev mkArray_eq_empty_iff := @replicate_eq_empty_iff
 
-@[simp] theorem mkArray_inj : mkArray n a = mkArray m b ↔ n = m ∧ (n = 0 ∨ a = b) := by
+@[simp] theorem replicate_inj : replicate n a = replicate m b ↔ n = m ∧ (n = 0 ∨ a = b) := by
   rw [← toList_inj]
   simp
 
-theorem eq_mkArray_of_mem {a : α} {xs : Array α} (h : ∀ (b) (_ : b ∈ xs), b = a) : xs = mkArray xs.size a := by
+@[deprecated replicate_inj (since := "2025-03-18")]
+abbrev mkArray_inj := @replicate_inj
+
+theorem eq_replicate_of_mem {a : α} {xs : Array α} (h : ∀ (b) (_ : b ∈ xs), b = a) : xs = replicate xs.size a := by
   rw [← toList_inj]
   simpa using List.eq_replicate_of_mem (by simpa using h)
 
-theorem eq_mkArray_iff {a : α} {n} {xs : Array α} :
+@[deprecated eq_replicate_of_mem (since := "2025-03-18")]
-    xs = mkArray n a ↔ xs.size = n ∧ ∀ (b) (_ : b ∈ xs), b = a := by
+abbrev eq_mkArray_of_mem := @eq_replicate_of_mem
+
+theorem eq_replicate_iff {a : α} {n} {xs : Array α} :
+    xs = replicate n a ↔ xs.size = n ∧ ∀ (b) (_ : b ∈ xs), b = a := by
   rw [← toList_inj]
   simpa using List.eq_replicate_iff (l := xs.toList)
 
-theorem map_eq_mkArray_iff {xs : Array α} {f : α → β} {b : β} :
+@[deprecated eq_replicate_iff (since := "2025-03-18")]
-    xs.map f = mkArray xs.size b ↔ ∀ x ∈ xs, f x = b := by
+abbrev eq_mkArray_iff := @eq_replicate_iff
-  simp [eq_mkArray_iff]
 
-@[simp] theorem map_const (xs : Array α) (b : β) : map (Function.const α b) xs = mkArray xs.size b :=
+theorem map_eq_replicate_iff {xs : Array α} {f : α → β} {b : β} :
-  map_eq_mkArray_iff.mpr fun _ _ => rfl
+    xs.map f = replicate xs.size b ↔ ∀ x ∈ xs, f x = b := by
+  simp [eq_replicate_iff]
 
-@[simp] theorem map_const_fun (x : β) : map (Function.const α x) = (mkArray ·.size x) := by
+@[deprecated map_eq_replicate_iff (since := "2025-03-18")]
+abbrev map_eq_mkArray_iff := @map_eq_replicate_iff
+
+@[simp] theorem map_const (xs : Array α) (b : β) : map (Function.const α b) xs = replicate xs.size b :=
+  map_eq_replicate_iff.mpr fun _ _ => rfl
+
+@[simp] theorem map_const_fun (x : β) : map (Function.const α x) = (replicate ·.size x) := by
   funext xs
   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' (xs : Array α) (b : β) : map (fun _ => b) xs = mkArray xs.size b :=
+theorem map_const' (xs : Array α) (b : β) : map (fun _ => b) xs = replicate xs.size b :=
   map_const xs b
 
-@[simp] theorem set_mkArray_self : (mkArray n a).set i a h = mkArray n a := by
+@[simp] theorem set_replicate_self : (replicate n a).set i a h = replicate n a := by
   apply Array.ext'
   simp
 
-@[simp] theorem setIfInBounds_mkArray_self : (mkArray n a).setIfInBounds i a = mkArray n a := by
+@[deprecated set_replicate_self (since := "2025-03-18")]
+abbrev set_mkArray_self := @set_replicate_self
+
+@[simp] theorem setIfInBounds_replicate_self : (replicate n a).setIfInBounds i a = replicate n a := by
   apply Array.ext'
   simp
 
-@[simp] theorem mkArray_append_mkArray : mkArray n a ++ mkArray m a = mkArray (n + m) a := by
+@[deprecated setIfInBounds_replicate_self (since := "2025-03-18")]
+abbrev setIfInBounds_mkArray_self := @setIfInBounds_replicate_self
+
+@[simp] theorem replicate_append_replicate : replicate n a ++ replicate m a = replicate (n + m) a := by
   apply Array.ext'
   simp
 
-theorem append_eq_mkArray_iff {xs ys : Array α} {a : α} :
+@[deprecated replicate_append_replicate (since := "2025-03-18")]
-    xs ++ ys = mkArray n a ↔
+abbrev mkArray_append_mkArray := @replicate_append_replicate
-      xs.size + ys.size = n ∧ xs = mkArray xs.size a ∧ ys = mkArray ys.size a := by
+
+theorem append_eq_replicate_iff {xs ys : Array α} {a : α} :
+    xs ++ ys = replicate n a ↔
+      xs.size + ys.size = n ∧ xs = replicate xs.size a ∧ ys = replicate ys.size a := by
   simp [← toList_inj, List.append_eq_replicate_iff]
 
-theorem mkArray_eq_append_iff {xs ys : Array α} {a : α} :
+@[deprecated append_eq_replicate_iff (since := "2025-03-18")]
-    mkArray n a = xs ++ ys ↔
+abbrev append_eq_mkArray_iff := @append_eq_replicate_iff
-      xs.size + ys.size = n ∧ xs = mkArray xs.size a ∧ ys = mkArray ys.size a := by
-  rw [eq_comm, append_eq_mkArray_iff]
 
-@[simp] theorem map_mkArray : (mkArray n a).map f = mkArray n (f a) := by
+theorem replicate_eq_append_iff {xs ys : Array α} {a : α} :
+    replicate n a = xs ++ ys ↔
+      xs.size + ys.size = n ∧ xs = replicate xs.size a ∧ ys = replicate ys.size a := by
+  rw [eq_comm, append_eq_replicate_iff]
+
+@[deprecated replicate_eq_append_iff (since := "2025-03-18")]
+abbrev replicate_eq_mkArray_iff := @replicate_eq_append_iff
+
+@[simp] theorem map_replicate : (replicate n a).map f = replicate n (f a) := by
   apply Array.ext'
   simp
 
-theorem filter_mkArray (w : stop = n) :
+@[deprecated map_replicate (since := "2025-03-18")]
-    (mkArray n a).filter p 0 stop = if p a then mkArray n a else #[] := by
+abbrev map_mkArray := @map_replicate
+
+theorem filter_replicate (w : stop = n) :
+    (replicate n a).filter p 0 stop = if p a then replicate n a else #[] := by
   apply Array.ext'
-  simp only [w, toList_filter', toList_mkArray, List.filter_replicate]
+  simp only [w, toList_filter', toList_replicate, List.filter_replicate]
   split <;> simp_all
 
-@[simp] theorem filter_mkArray_of_pos (w : stop = n) (h : p a) :
+@[deprecated filter_replicate (since := "2025-03-18")]
-    (mkArray n a).filter p 0 stop = mkArray n a := by
+abbrev filter_mkArray := @filter_replicate
-  simp [filter_mkArray, h, w]
 
-@[simp] theorem filter_mkArray_of_neg (w : stop = n) (h : ¬ p a) :
+@[simp] theorem filter_replicate_of_pos (w : stop = n) (h : p a) :
-    (mkArray n a).filter p 0 stop = #[] := by
+    (replicate n a).filter p 0 stop = replicate n a := by
-  simp [filter_mkArray, h, w]
+  simp [filter_replicate, h, w]
 
-theorem filterMap_mkArray {f : α → Option β} (w : stop = n := by simp) :
+@[deprecated filter_replicate_of_pos (since := "2025-03-18")]
-    (mkArray n a).filterMap f 0 stop = match f a with | none => #[] | .some b => mkArray n b := by
+abbrev filter_mkArray_of_pos := @filter_replicate_of_pos
+
+@[simp] theorem filter_replicate_of_neg (w : stop = n) (h : ¬ p a) :
+    (replicate n a).filter p 0 stop = #[] := by
+  simp [filter_replicate, h, w]
+
+@[deprecated filter_replicate_of_neg (since := "2025-03-18")]
+abbrev filter_mkArray_of_neg := @filter_replicate_of_neg
+
+theorem filterMap_replicate {f : α → Option β} (w : stop = n := by simp) :
+    (replicate n a).filterMap f 0 stop = match f a with | none => #[] | .some b => replicate n b := by
   apply Array.ext'
-  simp only [w, size_mkArray, toList_filterMap', toList_mkArray, List.filterMap_replicate]
+  simp only [w, size_replicate, toList_filterMap', toList_replicate, List.filterMap_replicate]
   split <;> simp_all
 
+@[deprecated filterMap_replicate (since := "2025-03-18")]
+abbrev filterMap_mkArray := @filterMap_replicate
+
 -- This is not a useful `simp` lemma because `b` is unknown.
-theorem filterMap_mkArray_of_some {f : α → Option β} (h : f a = some b) :
+theorem filterMap_replicate_of_some {f : α → Option β} (h : f a = some b) :
-    (mkArray n a).filterMap f = mkArray n b := by
+    (replicate n a).filterMap f = replicate n b := by
-  simp [filterMap_mkArray, h]
+  simp [filterMap_replicate, h]
 
-@[simp] theorem filterMap_mkArray_of_isSome {f : α → Option β} (h : (f a).isSome) :
+@[deprecated filterMap_replicate_of_some (since := "2025-03-18")]
-    (mkArray n a).filterMap f = mkArray n (Option.get _ h) := by
+abbrev filterMap_mkArray_of_some := @filterMap_replicate_of_some
+
+@[simp] theorem filterMap_replicate_of_isSome {f : α → Option β} (h : (f a).isSome) :
+    (replicate n a).filterMap f = replicate n (Option.get _ h) := by
   match w : f a, h with
-  | some b, _ => simp [filterMap_mkArray, h, w]
+  | some b, _ => simp [filterMap_replicate, h, w]
 
-@[simp] theorem filterMap_mkArray_of_none {f : α → Option β} (h : f a = none) :
+@[deprecated filterMap_replicate_of_isSome (since := "2025-03-18")]
-    (mkArray n a).filterMap f = #[] := by
+abbrev filterMap_mkArray_of_isSome := @filterMap_replicate_of_isSome
-  simp [filterMap_mkArray, h]
 
-@[simp] theorem flatten_mkArray_empty : (mkArray n (#[] : Array α)).flatten = #[] := by
+@[simp] theorem filterMap_replicate_of_none {f : α → Option β} (h : f a = none) :
+    (replicate n a).filterMap f = #[] := by
+  simp [filterMap_replicate, h]
+
+@[deprecated filterMap_replicate_of_none (since := "2025-03-18")]
+abbrev filterMap_mkArray_of_none := @filterMap_replicate_of_none
+
+@[simp] theorem flatten_replicate_empty : (replicate n (#[] : Array α)).flatten = #[] := by
   rw [← toList_inj]
   simp
 
-@[simp] theorem flatten_mkArray_singleton : (mkArray n #[a]).flatten = mkArray n a := by
+@[deprecated flatten_replicate_empty (since := "2025-03-18")]
+abbrev flatten_mkArray_empty := @flatten_replicate_empty
+
+@[simp] theorem flatten_replicate_singleton : (replicate n #[a]).flatten = replicate n a := by
   rw [← toList_inj]
   simp
 
-@[simp] theorem flatten_mkArray_mkArray : (mkArray n (mkArray m a)).flatten = mkArray (n * m) a := by
+@[deprecated flatten_replicate_singleton (since := "2025-03-18")]
+abbrev flatten_mkArray_singleton := @flatten_replicate_singleton
+
+@[simp] theorem flatten_replicate_replicate : (replicate n (replicate m a)).flatten = replicate (n * m) a := by
   rw [← toList_inj]
   simp
 
-theorem flatMap_mkArray {β} (f : α → Array β) : (mkArray n a).flatMap f = (mkArray n (f a)).flatten := by
+@[deprecated flatten_replicate_replicate (since := "2025-03-18")]
+abbrev flatten_mkArray_replicate := @flatten_replicate_replicate
+
+theorem flatMap_replicate {β} (f : α → Array β) : (replicate n a).flatMap f = (replicate 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
+@[deprecated flatMap_replicate (since := "2025-03-18")]
+abbrev flatMap_mkArray := @flatMap_replicate
+
+@[simp] theorem isEmpty_replicate : (replicate 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
+@[deprecated isEmpty_replicate (since := "2025-03-18")]
+abbrev isEmpty_mkArray := @isEmpty_replicate
+
+@[simp] theorem sum_replicate_nat (n : Nat) (a : Nat) : (replicate n a).sum = n * a := by
   rw [← List.toArray_replicate, List.sum_toArray]
   simp
 
+@[deprecated sum_replicate_nat (since := "2025-03-18")]
+abbrev sum_mkArray_nat := @sum_replicate_nat
+
 /-! ### Preliminaries about `swap` needed for `reverse`. -/
 
 theorem getElem?_swap (xs : Array α) (i j : Nat) (hi hj) (k : Nat) : (xs.swap i j hi hj)[k]? =
@@ -2625,10 +2733,13 @@ theorem flatMap_reverse {β} (xs : Array α) (f : α → Array β) :
   cases xs
   simp [List.flatMap_reverse, Function.comp_def]
 
-@[simp] theorem reverse_mkArray (n) (a : α) : reverse (mkArray n a) = mkArray n a := by
+@[simp] theorem reverse_replicate (n) (a : α) : reverse (replicate n a) = replicate n a := by
   rw [← toList_inj]
   simp
 
+@[deprecated reverse_replicate (since := "2025-03-18")]
+abbrev reverse_mkArray := @reverse_replicate
+
 /-! ### extract -/
 
 theorem extract_loop_zero (xs ys : Array α) (start : Nat) : extract.loop xs 0 start ys = ys := by
@@ -3464,14 +3575,20 @@ theorem back?_flatten {xss : Array (Array α)} :
     (flatten xss).back? = xss.reverse.findSome? fun xs => xs.back? := by
   simp [← flatMap_id, back?_flatMap]
 
-theorem back?_mkArray (a : α) (n : Nat) :
+theorem back?_replicate (a : α) (n : Nat) :
-    (mkArray n a).back? = if n = 0 then none else some a := by
+    (replicate n a).back? = if n = 0 then none else some a := by
-  rw [mkArray_eq_toArray_replicate]
+  rw [replicate_eq_toArray_replicate]
   simp only [List.back?_toArray, List.getLast?_replicate]
 
-@[simp] theorem back_mkArray (w : 0 < n) : (mkArray n a).back (by simpa using w) = a := by
+@[deprecated back?_replicate (since := "2025-03-18")]
+abbrev back?_mkArray := @back?_replicate
+
+@[simp] theorem back_replicate (w : 0 < n) : (replicate n a).back (by simpa using w) = a := by
   simp [back_eq_getElem]
 
+@[deprecated back_replicate (since := "2025-03-18")]
+abbrev back_mkArray := @back_replicate
+
 /-! ## Additional operations -/
 
 /-! ### leftpad -/
@@ -3508,9 +3625,12 @@ theorem pop_append {xs ys : Array α} :
     (xs ++ ys).pop = if ys.isEmpty then xs.pop else xs ++ ys.pop := by
   split <;> simp_all
 
-@[simp] theorem pop_mkArray (n) (a : α) : (mkArray n a).pop = mkArray (n - 1) a := by
+@[simp] theorem pop_replicate (n) (a : α) : (replicate n a).pop = replicate (n - 1) a := by
   ext <;> simp
 
+@[deprecated pop_replicate (since := "2025-03-18")]
+abbrev pop_mkArray := @pop_replicate
+
 /-! ### modify -/
 
 @[simp] theorem size_modify (xs : Array α) (i : Nat) (f : α → α) : (xs.modify i f).size = xs.size := by
@@ -3675,15 +3795,21 @@ theorem replace_extract {xs : Array α} {i : Nat} :
   rcases xs with ⟨xs⟩
   simp [List.replace_take]
 
-@[simp] theorem replace_mkArray_self {a : α} (h : 0 < n) :
+@[simp] theorem replace_replicate_self {a : α} (h : 0 < n) :
-    (mkArray n a).replace a b = #[b] ++ mkArray (n - 1) a := by
+    (replicate n a).replace a b = #[b] ++ replicate (n - 1) a := by
-  cases n <;> simp_all [mkArray_succ', replace_append]
+  cases n <;> simp_all [replicate_succ', replace_append]
 
-@[simp] theorem replace_mkArray_ne {a b c : α} (h : !b == a) :
+@[deprecated replace_replicate_self (since := "2025-03-18")]
-    (mkArray n a).replace b c = mkArray n a := by
+abbrev replace_mkArray_self := @replace_replicate_self
+
+@[simp] theorem replace_replicate_ne {a b c : α} (h : !b == a) :
+    (replicate n a).replace b c = replicate n a := by
   rw [replace_of_not_mem]
   simp_all
 
+@[deprecated replace_replicate_ne (since := "2025-03-18")]
+abbrev replace_mkArray_ne := @replace_replicate_ne
+
 end replace
 
 /-! ## Logic -/
@@ -3911,13 +4037,19 @@ theorem any_reverse {xs : Array α} : xs.reverse.any f 0 = xs.any f := by
 theorem all_reverse {xs : Array α} : xs.reverse.all f 0 = xs.all f := by
   simp
 
-@[simp] theorem any_mkArray {n : Nat} {a : α} :
+@[simp] theorem any_replicate {n : Nat} {a : α} :
-    (mkArray n a).any f = if n = 0 then false else f a := by
+    (replicate n a).any f = if n = 0 then false else f a := by
-  induction n <;> simp_all [mkArray_succ']
+  induction n <;> simp_all [replicate_succ']
 
-@[simp] theorem all_mkArray {n : Nat} {a : α} :
+@[deprecated any_replicate (since := "2025-03-18")]
-    (mkArray n a).all f = if n = 0 then true else f a := by
+abbrev any_mkArray := @any_replicate
-  induction n <;> simp_all +contextual [mkArray_succ']
+
+@[simp] theorem all_replicate {n : Nat} {a : α} :
+    (replicate n a).all f = if n = 0 then true else f a := by
+  induction n <;> simp_all +contextual [replicate_succ']
+
+@[deprecated all_replicate (since := "2025-03-18")]
+abbrev all_mkArray := @all_replicate
 
 /-! ### toListRev -/
 

src/Init/Data/Array/MapIdx.lean

@@ -292,12 +292,15 @@ theorem mapFinIdx_eq_mapFinIdx_iff {xs : Array α} {f g : (i : Nat) → α → (
     (xs.mapFinIdx f).mapFinIdx g = xs.mapFinIdx (fun i a h => g i (f i a h) (by simpa using h)) := by
   simp [mapFinIdx_eq_iff]
 
-theorem mapFinIdx_eq_mkArray_iff {xs : Array α} {f : (i : Nat) → α → (h : i < xs.size) → β} {b : β} :
+theorem mapFinIdx_eq_replicate_iff {xs : Array α} {f : (i : Nat) → α → (h : i < xs.size) → β} {b : β} :
-    xs.mapFinIdx f = mkArray xs.size b ↔ ∀ (i : Nat) (h : i < xs.size), f i xs[i] h = b := by
+    xs.mapFinIdx f = replicate xs.size b ↔ ∀ (i : Nat) (h : i < xs.size), f i xs[i] h = b := by
   rcases xs with ⟨l⟩
   rw [← toList_inj]
   simp [List.mapFinIdx_eq_replicate_iff]
 
+@[deprecated mapFinIdx_eq_replicate_iff (since := "2025-03-18")]
+abbrev mapFinIdx_eq_mkArray_iff := @mapFinIdx_eq_replicate_iff
+
 @[simp] theorem mapFinIdx_reverse {xs : Array α} {f : (i : Nat) → α → (h : i < xs.reverse.size) → β} :
     xs.reverse.mapFinIdx f = (xs.mapFinIdx (fun i a h => f (xs.size - 1 - i) a (by simp; omega))).reverse := by
   rcases xs with ⟨l⟩
@@ -431,12 +434,15 @@ theorem mapIdx_eq_mapIdx_iff {xs : Array α} :
     (xs.mapIdx f).mapIdx g = xs.mapIdx (fun i => g i ∘ f i) := by
   simp [mapIdx_eq_iff]
 
-theorem mapIdx_eq_mkArray_iff {xs : Array α} {f : Nat → α → β} {b : β} :
+theorem mapIdx_eq_replicate_iff {xs : Array α} {f : Nat → α → β} {b : β} :
-    mapIdx f xs = mkArray xs.size b ↔ ∀ (i : Nat) (h : i < xs.size), f i xs[i] = b := by
+    mapIdx f xs = replicate xs.size b ↔ ∀ (i : Nat) (h : i < xs.size), f i xs[i] = b := by
   rcases xs with ⟨xs⟩
   rw [← toList_inj]
   simp [List.mapIdx_eq_replicate_iff]
 
+@[deprecated mapIdx_eq_replicate_iff (since := "2025-03-18")]
+abbrev mapIdx_eq_mkArray_iff := @mapIdx_eq_replicate_iff
+
 @[simp] theorem mapIdx_reverse {xs : Array α} {f : Nat → α → β} :
     xs.reverse.mapIdx f = (mapIdx (fun i => f (xs.size - 1 - i)) xs).reverse := by
   rcases xs with ⟨xs⟩

src/Init/Data/Array/Zip.lean

@@ -149,10 +149,13 @@ theorem zipWith_eq_append_iff {f : α → β → γ} {as : Array α} {bs : Array
   · rintro ⟨⟨ws⟩, ⟨xs⟩, ⟨ys⟩, ⟨zs⟩, h, rfl, rfl, h₁, h₂⟩
     exact ⟨ws, xs, ys, zs, by simp_all⟩
 
-@[simp] theorem zipWith_mkArray {a : α} {b : β} {m n : Nat} :
+@[simp] theorem zipWith_replicate {a : α} {b : β} {m n : Nat} :
-    zipWith f (mkArray m a) (mkArray n b) = mkArray (min m n) (f a b) := by
+    zipWith f (replicate m a) (replicate n b) = replicate (min m n) (f a b) := by
   simp [← List.toArray_replicate]
 
+@[deprecated zipWith_replicate (since := "2025-03-18")]
+abbrev zipWith_mkArray := @zipWith_replicate
+
 theorem map_uncurry_zip_eq_zipWith (f : α → β → γ) (as : Array α) (bs : Array β) :
     map (Function.uncurry f) (as.zip bs) = zipWith f as bs := by
   cases as
@@ -270,10 +273,13 @@ theorem zip_eq_append_iff {as : Array α} {bs : Array β} :
       ∃ as₁ as₂ bs₁ bs₂, as₁.size = bs₁.size ∧ as = as₁ ++ as₂ ∧ bs = bs₁ ++ bs₂ ∧ xs = zip as₁ bs₁ ∧ ys = zip as₂ bs₂ := by
   simp [zip_eq_zipWith, zipWith_eq_append_iff]
 
-@[simp] theorem zip_mkArray {a : α} {b : β} {m n : Nat} :
+@[simp] theorem zip_replicate {a : α} {b : β} {m n : Nat} :
-    zip (mkArray m a) (mkArray n b) = mkArray (min m n) (a, b) := by
+    zip (replicate m a) (replicate n b) = replicate (min m n) (a, b) := by
   simp [← List.toArray_replicate]
 
+@[deprecated zip_replicate (since := "2025-03-18")]
+abbrev zip_mkArray := @zip_replicate
+
 theorem zip_eq_zip_take_min (as : Array α) (bs : Array β) :
     zip as bs = zip (as.take (min as.size bs.size)) (bs.take (min as.size bs.size)) := by
   cases as
@@ -317,9 +323,12 @@ theorem map_zipWithAll {δ : Type _} (f : α → β) (g : Option γ → Option
   simp [List.map_zipWithAll]
 
 @[simp] theorem zipWithAll_replicate {a : α} {b : β} {n : Nat} :
-    zipWithAll f (mkArray n a) (mkArray n b) = mkArray n (f a b) := by
+    zipWithAll f (replicate n a) (replicate n b) = replicate n (f a b) := by
   simp [← List.toArray_replicate]
 
+@[deprecated zipWithAll_replicate (since := "2025-03-18")]
+abbrev zipWithAll_mkArray := @zipWithAll_replicate
+
 /-! ### unzip -/
 
 @[simp] theorem unzip_fst : (unzip l).fst = l.map Prod.fst := by
@@ -360,6 +369,9 @@ theorem zip_of_prod {as : Array α} {bs : Array β} {xs : Array (α × β)} (hl
     (hr : xs.map Prod.snd = bs) : xs = as.zip bs := by
   rw [← hl, ← hr, ← zip_unzip xs, ← unzip_fst, ← unzip_snd, zip_unzip, zip_unzip]
 
-@[simp] theorem unzip_mkArray {n : Nat} {a : α} {b : β} :
+@[simp] theorem unzip_replicate {n : Nat} {a : α} {b : β} :
-    unzip (mkArray n (a, b)) = (mkArray n a, mkArray n b) := by
+    unzip (replicate n (a, b)) = (replicate n a, replicate n b) := by
   ext1 <;> simp
+
+@[deprecated unzip_replicate (since := "2025-03-18")]
+abbrev unzip_mkArray := @unzip_replicate

src/Init/Data/List/ToArray.lean

@@ -538,11 +538,16 @@ private theorem popWhile_toArray_aux (p : α → Bool) (l : List α) :
   · 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
 
-theorem _root_.Array.mkArray_eq_toArray_replicate : mkArray n v = (List.replicate n v).toArray := by
+theorem _root_.Array.replicate_eq_toArray_replicate :
+    Array.replicate n v = (List.replicate n v).toArray := by
   simp
 
+@[deprecated _root_.Array.replicate_eq_toArray_replicate (since := "2025-03-18")]
+abbrev _root_.Array.mkArray_eq_toArray_replicate := @_root_.Array.replicate_eq_toArray_replicate
+
 @[simp] theorem flatMap_empty {β} (f : α → Array β) : (#[] : Array α).flatMap f = #[] := rfl
 
 theorem flatMap_toArray_cons {β} (f : α → Array β) (a : α) (as : List α) :

src/Init/Data/Vector/Attach.lean

@@ -593,8 +593,11 @@ and simplifies these to the function directly taking the value.
   unfold Array.unattach
   rfl
 
-@[simp] theorem unattach_mkVector {p : α → Prop} {n : Nat} {x : { x // p x }} :
+@[simp] theorem unattach_replicate {p : α → Prop} {n : Nat} {x : { x // p x }} :
-    (mkVector n x).unattach = mkVector n x.1 := by
+    (replicate n x).unattach = replicate n x.1 := by
   simp [unattach]
 
+@[deprecated unattach_replicate (since := "2025-03-18")]
+abbrev unattach_mkVector := @unattach_replicate
+
 end Vector

src/Init/Data/Vector/Basic.lean

@@ -67,16 +67,19 @@ def elimAsList {motive : Vector α n → Sort u}
 abbrev mkEmpty := @emptyWithCapacity
 
 /-- 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-03-18")]
+abbrev mkVector := @replicate
 
 instance : Nonempty (Vector α 0) := ⟨#v[]⟩
-instance [Nonempty α] : Nonempty (Vector α n) := ⟨mkVector _ Classical.ofNonempty⟩
+instance [Nonempty α] : Nonempty (Vector α n) := ⟨replicate _ Classical.ofNonempty⟩
 
 /-- 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 (xs : Vector α n) (i : Fin n) : α :=
@@ -471,7 +474,7 @@ Note that we immediately simplify this to an `++` operation,
 and do not provide separate verification theorems.
 -/
 @[inline, simp] def leftpad (n : Nat) (a : α) (xs : Vector α m) : Vector α (max n m) :=
-  (mkVector (n - m) a ++ xs).cast (by omega)
+  (replicate (n - m) a ++ xs).cast (by omega)
 
 /--
 Pad a vector on the right with a given element.
@@ -480,7 +483,7 @@ Note that we immediately simplify this to an `++` operation,
 and do not provide separate verification theorems.
 -/
 @[inline, simp] def rightpad (n : Nat) (a : α) (xs : Vector α m) : Vector α (max n m) :=
-  (xs ++ mkVector (n - m) a).cast (by omega)
+  (xs ++ replicate (n - m) a).cast (by omega)
 
 /-! ### ForIn instance -/
 

src/Init/Data/Vector/Count.lean

@@ -72,10 +72,13 @@ theorem countP_le_size {xs : Vector α n} : countP p xs ≤ n := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
-theorem countP_mkVector (p : α → Bool) (a : α) (n : Nat) :
+theorem countP_replicate (p : α → Bool) (a : α) (n : Nat) :
-    countP p (mkVector n a) = if p a then n else 0 := by
+    countP p (replicate n a) = if p a then n else 0 := by
-  simp only [mkVector_eq_mk_mkArray, countP_cast, countP_mk]
+  simp only [replicate_eq_mk_replicate, countP_cast, countP_mk]
-  simp [Array.countP_mkArray]
+  simp [Array.countP_replicate]
+
+@[deprecated countP_replicate (since := "2025-03-18")]
+abbrev countP_mkVector := @countP_replicate
 
 theorem boole_getElem_le_countP (p : α → Bool) (xs : Vector α n) (i : Nat) (h : i < n) :
     (if p xs[i] then 1 else 0) ≤ xs.countP p := by
@@ -217,13 +220,19 @@ theorem count_eq_size {xs : Vector α n} : count a xs = xs.size ↔ ∀ b ∈ xs
   rcases xs with ⟨xs, rfl⟩
   simp [Array.count_eq_size]
 
-@[simp] theorem count_mkVector_self (a : α) (n : Nat) : count a (mkVector n a) = n := by
+@[simp] theorem count_replicate_self (a : α) (n : Nat) : count a (replicate n a) = n := by
-  simp only [mkVector_eq_mk_mkArray, count_cast, count_mk]
+  simp only [replicate_eq_mk_replicate, count_cast, count_mk]
   simp
 
-theorem count_mkVector (a b : α) (n : Nat) : count a (mkVector n b) = if b == a then n else 0 := by
+@[deprecated count_replicate_self (since := "2025-03-18")]
-  simp only [mkVector_eq_mk_mkArray, count_cast, count_mk]
+abbrev count_mkVector_self := @count_replicate_self
-  simp [Array.count_mkArray]
+
+theorem count_replicate (a b : α) (n : Nat) : count a (replicate n b) = if b == a then n else 0 := by
+  simp only [replicate_eq_mk_replicate, count_cast, count_mk]
+  simp [Array.count_replicate]
+
+@[deprecated count_replicate (since := "2025-03-18")]
+abbrev count_mkVector := @count_replicate
 
 theorem count_le_count_map [DecidableEq β] (xs : Vector α n) (f : α → β) (x : α) :
     count x xs ≤ count (f x) (map f xs) := by

src/Init/Data/Vector/Erase.lean

@@ -69,10 +69,13 @@ theorem eraseIdx_cast {xs : Vector α n} {k : Nat} (h : k < m) :
   rcases xs with ⟨xs⟩
   simp
 
-theorem eraseIdx_mkVector {n : Nat} {a : α} {k : Nat} {h} :
+theorem eraseIdx_replicate {n : Nat} {a : α} {k : Nat} {h} :
-    (mkVector n a).eraseIdx k = mkVector (n - 1) a := by
+    (replicate n a).eraseIdx k = replicate (n - 1) a := by
-  rw [mkVector_eq_mk_mkArray, eraseIdx_mk]
+  rw [replicate_eq_mk_replicate, eraseIdx_mk]
-  simp [Array.eraseIdx_mkArray, *]
+  simp [Array.eraseIdx_replicate, *]
+
+@[deprecated eraseIdx_replicate (since := "2025-03-18")]
+abbrev eraseIdx_mkVector := @eraseIdx_replicate
 
 theorem mem_eraseIdx_iff_getElem {x : α} {xs : Vector α n} {k} {h} : x ∈ xs.eraseIdx k h ↔ ∃ i w, i ≠ k ∧ xs[i]'w = x := by
   rcases xs with ⟨xs⟩

src/Init/Data/Vector/Extract.lean

@@ -131,11 +131,14 @@ theorem extract_append_left {xs : Vector α n} {ys : Vector α m} :
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp] theorem extract_mkVector {a : α} {n i j : Nat} :
+@[simp] theorem extract_replicate {a : α} {n i j : Nat} :
-    (mkVector n a).extract i j = mkVector (min j n - i) a := by
+    (replicate n a).extract i j = replicate (min j n - i) a := by
   ext i h
   simp
 
+@[deprecated extract_mkVector (since := "2025-03-18")]
+abbrev extract_mkVector := @extract_replicate
+
 theorem extract_add_left {xs : Vector α n} {i j k : Nat} :
     xs.extract (i + j) k = ((xs.extract i k).extract j (k - i)).cast (by omega) := by
   rcases xs with ⟨xs, rfl⟩

src/Init/Data/Vector/Find.lean

@@ -100,21 +100,33 @@ theorem getElem_zero_flatten {xss : Vector (Vector α m) n} (h : 0 < n * m) :
   simp [getElem?_eq_getElem, h] at t
   simp [← t]
 
-theorem findSome?_mkVector : findSome? f (mkVector 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
-  rw [mkVector_eq_mk_mkArray, findSome?_mk, Array.findSome?_mkArray]
+  rw [replicate_eq_mk_replicate, findSome?_mk, Array.findSome?_replicate]
 
-@[simp] theorem findSome?_mkVector_of_pos (h : 0 < n) : findSome? f (mkVector n a) = f a := by
+@[deprecated findSome?_replicate (since := "2025-03-18")]
-  simp [findSome?_mkVector, Nat.ne_of_gt h]
+abbrev findSome?_mkVector := @findSome?_replicate
+
+@[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]
+
+@[deprecated findSome?_replicate_of_pos (since := "2025-03-18")]
+abbrev findSome?_mkVector_of_pos := @findSome?_replicate_of_pos
 
 -- Argument is unused, but used to decide whether `simp` should unfold.
-@[simp] theorem findSome?_mkVector_of_isSome (_ : (f a).isSome) :
+@[simp] theorem findSome?_replicate_of_isSome (_ : (f a).isSome) :
-   findSome? f (mkVector n a) = if n = 0 then none else f a := by
+   findSome? f (replicate n a) = if n = 0 then none else f a := by
-  simp [findSome?_mkVector]
+  simp [findSome?_replicate]
 
-@[simp] theorem findSome?_mkVector_of_isNone (h : (f a).isNone) :
+@[deprecated findSome?_replicate_of_isSome (since := "2025-03-18")]
-    findSome? f (mkVector n a) = none := by
+abbrev findSome?_mkVector_of_isSome := @findSome?_replicate_of_isSome
+
+@[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?_mkVector, h]
+  simp [findSome?_replicate, h]
+
+@[deprecated findSome?_replicate_of_isNone (since := "2025-03-18")]
+abbrev findSome?_mkVector_of_isNone := @findSome?_replicate_of_isNone
 
 /-! ### find? -/
 
@@ -211,36 +223,57 @@ theorem find?_flatMap_eq_none_iff {xs : Vector α n} {f : α → Vector β m} {p
     (xs.flatMap f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y := by
   simp
 
-theorem find?_mkVector :
+theorem find?_replicate :
-    find? p (mkVector n a) = if n = 0 then none else if p a then some a else none := by
+    find? p (replicate n a) = if n = 0 then none else if p a then some a else none := by
-  rw [mkVector_eq_mk_mkArray, find?_mk, Array.find?_mkArray]
+  rw [replicate_eq_mk_replicate, find?_mk, Array.find?_replicate]
 
-@[simp] theorem find?_mkVector_of_length_pos (h : 0 < n) :
+@[deprecated find?_replicate (since := "2025-03-18")]
-    find? p (mkVector n a) = if p a then some a else none := by
+abbrev find?_mkVector := @find?_replicate
-  simp [find?_mkVector, Nat.ne_of_gt h]
 
-@[simp] theorem find?_mkVector_of_pos (h : p a) :
+@[simp] theorem find?_replicate_of_size_pos (h : 0 < n) :
-    find? p (mkVector n a) = if n = 0 then none else some a := by
+    find? p (replicate n a) = if p a then some a else none := by
-  simp [find?_mkVector, h]
+  simp [find?_replicate, Nat.ne_of_gt h]
 
-@[simp] theorem find?_mkVector_of_neg (h : ¬ p a) : find? p (mkVector n a) = none := by
+@[deprecated find?_replicate_of_size_pos (since := "2025-03-18")]
-  simp [find?_mkVector, h]
+abbrev find?_mkVector_of_length_pos := @find?_replicate_of_size_pos
+
+@[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]
+
+@[deprecated find?_replicate_of_pos (since := "2025-03-18")]
+abbrev find?_mkVector_of_pos := @find?_replicate_of_pos
+
+@[simp] theorem find?_replicate_of_neg (h : ¬ p a) : find? p (replicate n a) = none := by
+  simp [find?_replicate, h]
+
+@[deprecated find?_replicate_of_neg (since := "2025-03-18")]
+abbrev find?_mkVector_of_neg := @find?_replicate_of_neg
 
 -- This isn't a `@[simp]` lemma since there is already a lemma for `l.find? p = none` for any `l`.
-theorem find?_mkVector_eq_none_iff {n : Nat} {a : α} {p : α → Bool} :
+theorem find?_replicate_eq_none_iff {n : Nat} {a : α} {p : α → Bool} :
-    (mkVector n a).find? p = none ↔ n = 0 ∨ !p a := by
+    (replicate n a).find? p = none ↔ n = 0 ∨ !p a := by
   simp [Classical.or_iff_not_imp_left]
 
-@[simp] theorem find?_mkVector_eq_some_iff {n : Nat} {a b : α} {p : α → Bool} :
+@[deprecated find?_replicate_eq_none_iff (since := "2025-03-18")]
-    (mkVector n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b := by
+abbrev find?_mkVector_eq_none_iff := @find?_replicate_eq_none_iff
-  rw [mkVector_eq_mk_mkArray, find?_mk]
+
+@[simp] theorem find?_replicate_eq_some_iff {n : Nat} {a b : α} {p : α → Bool} :
+    (replicate n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b := by
+  rw [replicate_eq_mk_replicate, find?_mk]
   simp
 
-@[simp] theorem get_find?_mkVector (n : Nat) (a : α) (p : α → Bool) (h) :
+@[deprecated find?_replicate_eq_some_iff (since := "2025-03-18")]
-    ((mkVector n a).find? p).get h = a := by
+abbrev find?_mkVector_eq_some_iff := @find?_replicate_eq_some_iff
-  simp only [mkVector_eq_mk_mkArray, find?_mk]
+
+@[simp] theorem get_find?_replicate (n : Nat) (a : α) (p : α → Bool) (h) :
+    ((replicate n a).find? p).get h = a := by
+  simp only [replicate_eq_mk_replicate, find?_mk]
   simp
 
+@[deprecated get_find?_replicate (since := "2025-03-18")]
+abbrev get_find?_mkVector := @get_find?_replicate
+
 theorem find?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : Vector α n)
     (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/Vector/Lemmas.lean

@@ -465,7 +465,10 @@ theorem toArray_mapM_go [Monad m] [LawfulMonad m] (f : α → m β) (xs : Vector
   rcases xs with ⟨xs, rfl⟩
   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-03-18")]
+abbrev toArray_mkVector := @toArray_replicate
 
 @[simp] theorem toArray_inj {xs ys : Vector α n} : xs.toArray = ys.toArray ↔ xs = ys := by
   cases xs
@@ -642,7 +645,10 @@ theorem toList_swap (xs : Vector α n) (i j) (hi hj) :
   rcases xs with ⟨xs, rfl⟩
   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-03-18")]
+abbrev toList_mkVector := @toList_replicate
 
 theorem toList_inj {xs ys : Vector α n} : xs.toList = ys.toList ↔ xs = ys := by
   cases xs
@@ -758,23 +764,38 @@ theorem singleton_inj : #v[a] = #v[b] ↔ a = b := by
   · rintro rfl
     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
+@[deprecated replicate_zero (since := "2025-03-18")]
-  simp [mkVector, Array.mkArray_succ]
+abbrev replicate_mkVector := @replicate_zero
 
-@[simp] theorem mkVector_inj : mkVector n a = mkVector n b ↔ n = 0 ∨ a = b := by
+theorem replicate_succ : replicate (n + 1) a = (replicate n a).push a := by
-  simp [← toArray_inj, toArray_mkVector, Array.mkArray_inj]
+  simp [replicate, Array.replicate_succ]
 
-@[simp] theorem _root_.Array.mk_mkArray (a : α) (n : Nat) (h : (mkArray n a).size = m) :
+@[deprecated replicate_succ (since := "2025-03-18")]
-    mk (Array.mkArray n a) h = (mkVector n a).cast (by simpa using h) := rfl
+abbrev replicate_mkVector_succ := @replicate_succ
 
-theorem mkVector_eq_mk_mkArray (a : α) (n : Nat) :
+@[simp] theorem replicate_inj : replicate n a = replicate n b ↔ n = 0 ∨ a = b := by
-    mkVector n a = mk (mkArray n a) (by simp) := by
+  simp [← toArray_inj, toArray_replicate, Array.replicate_inj]
+
+@[deprecated replicate_inj (since := "2025-03-18")]
+abbrev mkVector_inj := @replicate_inj
+
+@[simp] theorem _root_.Array.vector_mk_replicate (a : α) (n : Nat) :
+    mk (n := n) (Array.replicate n a) (by simp) = replicate n a := rfl
+
+@[deprecated _root_.Array.vector_mk_replicate (since := "2025-03-18")]
+abbrev _root_.Array.mk_mkArray := @_root_.Array.vector_mk_replicate
+
+theorem replicate_eq_mk_replicate (a : α) (n : Nat) :
+    replicate n a = mk (n := n) (Array.replicate n a) (by simp) := by
   simp
 
+@[deprecated replicate_eq_mk_replicate (since := "2025-03-18")]
+abbrev mkVector_eq_mk_mkArray := @replicate_eq_mk_replicate
+
 /-! ## L[i] and L[i]? -/
 
 @[simp] theorem getElem?_eq_none_iff {xs : Vector α n} : xs[i]? = none ↔ n ≤ i := by
@@ -1294,15 +1315,18 @@ theorem mem_setIfInBounds (xs : Vector α n) (i : Nat) (hi : i < n) (a : α) :
   cases ys
   simp
 
-@[simp] theorem mkVector_beq_mkVector [BEq α] {a b : α} {n : Nat} :
+@[simp] theorem replicate_beq_replicate [BEq α] {a b : α} {n : Nat} :
-    (mkVector n a == mkVector n b) = (n == 0 || a == b) := by
+    (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-03-18")]
+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, _ =>
@@ -1310,8 +1334,8 @@ theorem mem_setIfInBounds (xs : Vector α n) (i : Nat) (hi : i < n) (a : α) :
     · intro h
       constructor
       intro a
-      suffices (mkVector (n + 1) a == mkVector (n + 1) a) = true by
+      suffices (replicate (n + 1) a == replicate (n + 1) a) = true by
-        rw [mkVector_succ, push_beq_push, Bool.and_eq_true] at this
+        rw [replicate_succ, push_beq_push, Bool.and_eq_true] at this
         exact this.2
       simp
     · intro h
@@ -1326,15 +1350,15 @@ theorem mem_setIfInBounds (xs : 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
+        suffices (replicate (n + 1) a == replicate (n + 1) a) = true by
-          rw [mkVector_beq_mkVector] at this
+          rw [replicate_beq_replicate] at this
           simpa
         simp
     · intro h
@@ -1438,8 +1462,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)
+    replace h := congrFun h (replicate n a)
-    simp only [mkVector, map_mk, mk.injEq, Array.map_inj_left, Array.mem_mkArray,  and_imp,
+    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
@@ -1957,104 +1981,169 @@ theorem map_eq_flatMap {α β} (f : α → β) (xs : Vector α n) :
   rcases xs with ⟨xs, rfl⟩
   simp [Array.map_eq_flatMap]
 
-/-! ### mkVector -/
+/-! ### replicate -/
 
-@[simp] theorem mkVector_one : mkVector 1 a = #v[a] := rfl
+@[simp] theorem replicate_one : replicate 1 a = #v[a] := rfl
 
-/-- Variant of `mkVector_succ` that prepends `a` at the beginning of the vector. -/
+@[deprecated replicate_one (since := "2025-03-18")]
-theorem mkVector_succ' : mkVector (n + 1) a = (#v[a] ++ mkVector n a).cast (by omega) := by
+abbrev replicate_mkVector_one := @replicate_one
+
+/-- Variant of `replicate_succ` that prepends `a` at the beginning of the vector. -/
+theorem replicate_succ' : replicate (n + 1) a = (#v[a] ++ replicate n a).cast (by omega) := by
   rw [← toArray_inj]
-  simp [Array.mkArray_succ']
+  simp [Array.replicate_succ']
 
-@[simp] theorem mem_mkVector {a b : α} {n} : b ∈ mkVector n a ↔ n ≠ 0 ∧ b = a := by
+@[deprecated replicate_succ' (since := "2025-03-18")]
-  unfold mkVector
+abbrev mkVector_succ' := @replicate_succ'
+
+@[simp] theorem mem_replicate {a b : α} {n} : b ∈ replicate n a ↔ n ≠ 0 ∧ b = a := by
+  unfold replicate
   simp only [mem_mk]
   simp
 
-theorem eq_of_mem_mkVector {a b : α} {n} (h : b ∈ mkVector n a) : b = a := (mem_mkVector.1 h).2
+@[deprecated mem_replicate (since := "2025-03-18")]
+abbrev mem_mkVector := @mem_replicate
 
-theorem forall_mem_mkVector {p : α → Prop} {a : α} {n} :
+theorem eq_of_mem_replicate {a b : α} {n} (h : b ∈ replicate n a) : b = a := (mem_replicate.1 h).2
-    (∀ 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
+@[deprecated eq_of_mem_replicate (since := "2025-03-18")]
-  rw [mkVector_eq_mk_mkArray, getElem_mk]
+abbrev eq_of_mem_mkVector := @eq_of_mem_replicate
+
+theorem forall_mem_replicate {p : α → Prop} {a : α} {n} :
+    (∀ b, b ∈ replicate n a → p b) ↔ n = 0 ∨ p a := by
+  cases n <;> simp [mem_replicate]
+
+@[deprecated forall_mem_replicate (since := "2025-03-18")]
+abbrev forall_mem_mkVector := @forall_mem_replicate
+
+@[simp] theorem getElem_replicate (a : α) (n i : Nat) (h : i < n) : (replicate n a)[i] = a := by
+  rw [replicate_eq_mk_replicate, getElem_mk]
   simp
 
-theorem getElem?_mkVector (a : α) (n i : Nat) : (mkVector n a)[i]? = if i < n then some a else none := by
+@[deprecated getElem_replicate (since := "2025-03-18")]
+abbrev getElem_mkVector := @getElem_replicate
+
+theorem getElem?_replicate (a : α) (n i : Nat) : (replicate n a)[i]? = if i < n then some a else none := by
   simp [getElem?_def]
 
-@[simp] theorem getElem?_mkVector_of_lt {n : Nat} {i : Nat} (h : i < n) : (mkVector n a)[i]? = some a := by
+@[deprecated getElem?_replicate (since := "2025-03-18")]
-  simp [getElem?_mkVector, h]
+abbrev getElem?_mkVector := @getElem?_replicate
 
-theorem eq_mkVector_of_mem {a : α} {xs : Vector α n} (h : ∀ (b) (_ : b ∈ xs), b = a) : xs = mkVector n a := by
+@[simp] theorem getElem?_replicate_of_lt {n : Nat} {i : Nat} (h : i < n) : (replicate n a)[i]? = some a := by
+  simp [getElem?_replicate, h]
+
+@[deprecated getElem?_replicate_of_lt (since := "2025-03-18")]
+abbrev getElem?_mkVector_of_lt := @getElem?_replicate_of_lt
+
+theorem eq_replicate_of_mem {a : α} {xs : Vector α n} (h : ∀ (b) (_ : b ∈ xs), b = a) : xs = replicate n a := by
   rw [← toArray_inj]
-  simpa using Array.eq_mkArray_of_mem (xs := xs.toArray) (by simpa using h)
+  simpa using Array.eq_replicate_of_mem (xs := xs.toArray) (by simpa using h)
 
-theorem eq_mkVector_iff {a : α} {n} {xs : Vector α n} :
+@[deprecated eq_replicate_of_mem (since := "2025-03-18")]
-    xs = mkVector n a ↔ ∀ (b) (_ : b ∈ xs), b = a := by
+abbrev eq_mkVector_of_mem := @eq_replicate_of_mem
+
+theorem eq_replicate_iff {a : α} {n} {xs : Vector α n} :
+    xs = replicate n a ↔ ∀ (b) (_ : b ∈ xs), b = a := by
   rw [← toArray_inj]
-  simpa using Array.eq_mkArray_iff (xs := xs.toArray) (n := n)
+  simpa using Array.eq_replicate_iff (xs := xs.toArray) (n := n)
 
-theorem map_eq_mkVector_iff {xs : Vector α n} {f : α → β} {b : β} :
+@[deprecated eq_replicate_iff (since := "2025-03-18")]
-    xs.map f = mkVector n b ↔ ∀ x ∈ xs, f x = b := by
+abbrev eq_mkVector_iff := @eq_replicate_iff
-  simp [eq_mkVector_iff]
 
-@[simp] theorem map_const (xs : Vector α n) (b : β) : map (Function.const α b) xs = mkVector n b :=
+theorem map_eq_replicate_iff {xs : Vector α n} {f : α → β} {b : β} :
-  map_eq_mkVector_iff.mpr fun _ _ => rfl
+    xs.map f = replicate n b ↔ ∀ x ∈ xs, f x = b := by
+  simp [eq_replicate_iff]
 
-@[simp] theorem map_const_fun (x : β) : map (n := n) (Function.const α x) = fun _ => mkVector n x := by
+@[deprecated map_eq_replicate_iff (since := "2025-03-18")]
+abbrev map_eq_mkVector_iff := @map_eq_replicate_iff
+
+@[simp] theorem map_const (xs : Vector α n) (b : β) : map (Function.const α b) xs = replicate n b :=
+  map_eq_replicate_iff.mpr fun _ _ => rfl
+
+@[simp] theorem map_const_fun (x : β) : map (n := n) (Function.const α x) = fun _ => replicate n x := by
   funext xs
   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' (xs : Vector α n) (b : β) : map (fun _ => b) xs = mkVector n b :=
+theorem map_const' (xs : Vector α n) (b : β) : map (fun _ => b) xs = replicate n b :=
   map_const xs b
 
-@[simp] theorem set_mkVector_self : (mkVector n a).set i a h = mkVector n a := by
+@[simp] theorem set_replicate_self : (replicate n a).set i a h = replicate n a := by
   rw [← toArray_inj]
   simp
 
-@[simp] theorem setIfInBounds_mkVector_self : (mkVector n a).setIfInBounds i a = mkVector n a := by
+@[deprecated set_replicate_self (since := "2025-03-18")]
+abbrev set_mkVector_self := @set_replicate_self
+
+@[simp] theorem setIfInBounds_replicate_self : (replicate n a).setIfInBounds i a = replicate n a := by
   rw [← toArray_inj]
   simp
 
-@[simp] theorem mkVector_append_mkVector : mkVector n a ++ mkVector m a = mkVector (n + m) a := by
+@[deprecated setIfInBounds_replicate_self (since := "2025-03-18")]
+abbrev setIfInBounds_mkVector_self := @setIfInBounds_replicate_self
+
+@[simp] theorem replicate_append_replicate : replicate n a ++ replicate m a = replicate (n + m) a := by
   rw [← toArray_inj]
   simp
 
-theorem append_eq_mkVector_iff {xs : Vector α n} {ys : Vector α m} {a : α} :
+@[deprecated replicate_append_replicate (since := "2025-03-18")]
-    xs ++ ys = mkVector (n + m) a ↔ xs = mkVector n a ∧ ys = mkVector m a := by
+abbrev mkVector_append_mkVector := @replicate_append_replicate
-  simp [← toArray_inj, Array.append_eq_mkArray_iff]
 
-theorem mkVector_eq_append_iff {xs : Vector α n} {ys : Vector α m} {a : α} :
+theorem append_eq_replicate_iff {xs : Vector α n} {ys : Vector α m} {a : α} :
-    mkVector (n + m) a = xs ++ ys ↔ xs = mkVector n a ∧ ys = mkVector m a := by
+    xs ++ ys = replicate (n + m) a ↔ xs = replicate n a ∧ ys = replicate m a := by
-  rw [eq_comm, append_eq_mkVector_iff]
+  simp [← toArray_inj, Array.append_eq_replicate_iff]
 
-@[simp] theorem map_mkVector : (mkVector n a).map f = mkVector n (f a) := by
+@[deprecated append_eq_replicate_iff (since := "2025-03-18")]
+abbrev append_eq_mkVector_iff := @append_eq_replicate_iff
+
+theorem replicate_eq_append_iff {xs : Vector α n} {ys : Vector α m} {a : α} :
+    replicate (n + m) a = xs ++ ys ↔ xs = replicate n a ∧ ys = replicate m a := by
+  rw [eq_comm, append_eq_replicate_iff]
+
+@[deprecated replicate_eq_append_iff (since := "2025-03-18")]
+abbrev mkVector_eq_append_iff := @replicate_eq_append_iff
+
+@[simp] theorem map_replicate : (replicate n a).map f = replicate n (f a) := by
   rw [← toArray_inj]
   simp
 
+@[deprecated map_replicate (since := "2025-03-18")]
+abbrev map_mkVector := @map_replicate
 
-@[simp] theorem flatten_mkVector_empty : (mkVector n (#v[] : Vector α 0)).flatten = #v[] := by
+@[simp] theorem flatten_replicate_empty : (replicate 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
+@[deprecated flatten_replicate_empty (since := "2025-03-18")]
+abbrev flatten_mkVector_empty := @flatten_replicate_empty
+
+@[simp] theorem flatten_replicate_singleton : (replicate n #v[a]).flatten = (replicate 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
+@[deprecated flatten_replicate_singleton (since := "2025-03-18")]
+abbrev flatten_mkVector_singleton := @flatten_replicate_singleton
+
+@[simp] theorem flatten_replicate_replicate : (replicate n (replicate m a)).flatten = replicate (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
+@[deprecated flatten_replicate_replicate (since := "2025-03-18")]
+abbrev flatten_mkVector_mkVector := @flatten_replicate_replicate
+
+theorem flatMap_replicate {β} (f : α → Vector β m) : (replicate n a).flatMap f = (replicate 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
+@[deprecated flatMap_replicate (since := "2025-03-18")]
-  simp [toArray_mkVector]
+abbrev flatMap_mkVector := @flatMap_replicate
+
+@[simp] theorem sum_replicate_nat (n : Nat) (a : Nat) : (replicate n a).sum = n * a := by
+  simp [toArray_replicate]
+
+@[deprecated sum_replicate_nat (since := "2025-03-18")]
+abbrev sum_mkVector := @sum_replicate_nat
 
 /-! ### reverse -/
 
@@ -2148,10 +2237,13 @@ theorem flatMap_reverse {β} (xs : Vector α n) (f : α → Vector β m) :
   rcases xs with ⟨xs, rfl⟩
   simp [Array.flatMap_reverse, Function.comp_def]
 
-@[simp] theorem reverse_mkVector (n) (a : α) : reverse (mkVector n a) = mkVector n a := by
+@[simp] theorem reverse_replicate (n) (a : α) : reverse (replicate n a) = replicate n a := by
   rw [← toArray_inj]
   simp
 
+@[deprecated reverse_replicate (since := "2025-03-18")]
+abbrev reverse_mkVector := @reverse_replicate
+
 /-! ### extract -/
 
 @[simp] theorem getElem_extract {as : Vector α n} {start stop : Nat}
@@ -2454,14 +2546,20 @@ theorem back?_flatten {xss : Vector (Vector α m) n} :
   simp [Array.back?_flatten, ← Array.map_reverse, Array.findSome?_map, Function.comp_def]
   rfl
 
-theorem back?_mkVector (a : α) (n : Nat) :
+theorem back?_replicate (a : α) (n : Nat) :
-    (mkVector n a).back? = if n = 0 then none else some a := by
+    (replicate n a).back? = if n = 0 then none else some a := by
-  rw [mkVector_eq_mk_mkArray]
+  rw [replicate_eq_mk_replicate]
-  simp only [back?_mk, Array.back?_mkArray]
+  simp only [back?_mk, Array.back?_replicate]
 
-@[simp] theorem back_mkArray [NeZero n] : (mkVector n a).back = a := by
+@[deprecated back?_replicate (since := "2025-03-18")]
+abbrev back?_mkVector := @back?_replicate
+
+@[simp] theorem back_replicate [NeZero n] : (replicate n a).back = a := by
   simp [back_eq_getElem]
 
+@[deprecated back_replicate (since := "2025-03-18")]
+abbrev back_mkVector := @back_replicate
+
 /-! ### leftpad and rightpad -/
 
 @[simp] theorem leftpad_mk (n : Nat) (a : α) (xs : Array α) (h : xs.size = m) :
@@ -2539,9 +2637,12 @@ theorem pop_append {xs : Vector α n} {ys : Vector α m} :
   rw [Array.pop_append]
   split <;> simp_all
 
-@[simp] theorem pop_mkVector (n) (a : α) : (mkVector n a).pop = mkVector (n - 1) a := by
+@[simp] theorem pop_replicate (n) (a : α) : (replicate n a).pop = replicate (n - 1) a := by
   ext <;> simp
 
+@[deprecated pop_replicate (since := "2025-03-18")]
+abbrev pop_mkVector := @pop_replicate
+
 /-! ### replace -/
 
 section replace
@@ -2605,16 +2706,22 @@ theorem replace_extract {xs : Vector α n} {i : Nat} :
   rcases xs with ⟨xs, rfl⟩
   simp [Array.replace_extract]
 
-@[simp] theorem replace_mkArray_self {a : α} (h : 0 < n) :
+@[simp] theorem replace_replicate_self {a : α} (h : 0 < n) :
-    (mkVector n a).replace a b = (#v[b] ++ mkVector (n - 1) a).cast (by omega) := by
+    (replicate n a).replace a b = (#v[b] ++ replicate (n - 1) a).cast (by omega) := by
   match n, h with
-  | n + 1, _ => simp_all [mkVector_succ', replace_append]
+  | n + 1, _ => simp_all [replicate_succ', replace_append]
 
-@[simp] theorem replace_mkArray_ne {a b c : α} (h : !b == a) :
+@[deprecated replace_replicate_self (since := "2025-03-18")]
-    (mkVector n a).replace b c = mkVector n a := by
+abbrev replace_mkArray_self := @replace_replicate_self
+
+@[simp] theorem replace_replicate_ne {a b c : α} (h : !b == a) :
+    (replicate n a).replace b c = replicate n a := by
   rw [replace_of_not_mem]
   simp_all
 
+@[deprecated replace_replicate_ne (since := "2025-03-18")]
+abbrev replace_mkArray_ne := @replace_replicate_ne
+
 end replace
 
 /-! ## Logic -/
@@ -2764,13 +2871,19 @@ theorem any_eq_not_all_not (xs : Vector α n) (p : α → Bool) : xs.any p = !xs
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp] theorem any_mkVector {n : Nat} {a : α} :
+@[simp] theorem any_replicate {n : Nat} {a : α} :
-    (mkVector n a).any f = if n = 0 then false else f a := by
+    (replicate n a).any f = if n = 0 then false else f a := by
-  induction n <;> simp_all [mkVector_succ']
+  induction n <;> simp_all [replicate_succ']
 
-@[simp] theorem all_mkVector {n : Nat} {a : α} :
+@[deprecated any_replicate (since := "2025-03-18")]
-    (mkVector n a).all f = if n = 0 then true else f a := by
+abbrev any_mkVector := @any_replicate
-  induction n <;> simp_all +contextual [mkVector_succ']
+
+@[simp] theorem all_replicate {n : Nat} {a : α} :
+    (replicate n a).all f = if n = 0 then true else f a := by
+  induction n <;> simp_all +contextual [replicate_succ']
+
+@[deprecated all_replicate (since := "2025-03-18")]
+abbrev all_mkVector := @all_replicate
 
 /-! Content below this point has not yet been aligned with `List` and `Array`. -/
 

src/Init/Data/Vector/MapIdx.lean

@@ -217,10 +217,13 @@ theorem mapFinIdx_eq_mapFinIdx_iff {xs : Vector α n} {f g : (i : Nat) → α
     (xs.mapFinIdx f).mapFinIdx g = xs.mapFinIdx (fun i a h => g i (f i a h) h) := by
   simp [mapFinIdx_eq_iff]
 
-theorem mapFinIdx_eq_mkVector_iff {xs : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} {b : β} :
+theorem mapFinIdx_eq_replicate_iff {xs : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} {b : β} :
-    xs.mapFinIdx f = mkVector n b ↔ ∀ (i : Nat) (h : i < n), f i xs[i] h = b := by
+    xs.mapFinIdx f = replicate n b ↔ ∀ (i : Nat) (h : i < n), f i xs[i] h = b := by
   rcases xs with ⟨xs, rfl⟩
-  simp [Array.mapFinIdx_eq_mkArray_iff]
+  simp [Array.mapFinIdx_eq_replicate_iff]
+
+@[deprecated mapFinIdx_eq_replicate_iff (since := "2025-03-18")]
+abbrev mapFinIdx_eq_mkVector_iff := @mapFinIdx_eq_replicate_iff
 
 @[simp] theorem mapFinIdx_reverse {xs : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} :
     xs.reverse.mapFinIdx f = (xs.mapFinIdx (fun i a h => f (n - 1 - i) a (by omega))).reverse := by
@@ -350,10 +353,13 @@ theorem mapIdx_eq_mapIdx_iff {xs : Vector α n} :
     (xs.mapIdx f).mapIdx g = xs.mapIdx (fun i => g i ∘ f i) := by
   simp [mapIdx_eq_iff]
 
-theorem mapIdx_eq_mkVector_iff {xs : Vector α n} {f : Nat → α → β} {b : β} :
+theorem mapIdx_eq_replicate_iff {xs : Vector α n} {f : Nat → α → β} {b : β} :
-    mapIdx f xs = mkVector n b ↔ ∀ (i : Nat) (h : i < n), f i xs[i] = b := by
+    mapIdx f xs = replicate n b ↔ ∀ (i : Nat) (h : i < n), f i xs[i] = b := by
   rcases xs with ⟨xs, rfl⟩
-  simp [Array.mapIdx_eq_mkArray_iff]
+  simp [Array.mapIdx_eq_replicate_iff]
+
+@[deprecated mapIdx_eq_replicate_iff (since := "2025-03-18")]
+abbrev mapIdx_eq_mkVector_iff := @mapIdx_eq_replicate_iff
 
 @[simp] theorem mapIdx_reverse {xs : Vector α n} {f : Nat → α → β} :
     xs.reverse.mapIdx f = (mapIdx (fun i => f (xs.size - 1 - i)) xs).reverse := by

src/Init/Data/Vector/Zip.lean

@@ -144,11 +144,14 @@ theorem zipWith_eq_append_iff {f : α → β → γ} {as : Vector α (n + m)} {b
     simp only at w₁ w₂
     exact ⟨as₁, as₂, bs₁, bs₂, by simpa [hw, hy] using ⟨w₁, w₂⟩⟩
 
-@[simp] theorem zipWith_mkVector {a : α} {b : β} {n : Nat} :
+@[simp] theorem zipWith_replicate {a : α} {b : β} {n : Nat} :
-    zipWith f (mkVector n a) (mkVector n b) = mkVector n (f a b) := by
+    zipWith f (replicate n a) (replicate n b) = replicate n (f a b) := by
   ext
   simp
 
+@[deprecated zipWith_replicate (since := "2025-03-18")]
+abbrev zipWith_mkVector := @zipWith_replicate
+
 theorem map_uncurry_zip_eq_zipWith (f : α → β → γ) (as : Vector α n) (bs : Vector β n) :
     map (Function.uncurry f) (as.zip bs) = zipWith f as bs := by
   rcases as with ⟨as, rfl⟩
@@ -240,10 +243,12 @@ theorem zip_eq_append_iff {as : Vector α (n + m)} {bs : Vector β (n + m)} {xs
       ∃ as₁ as₂ bs₁ bs₂, as₁.size = bs₁.size ∧ as = as₁ ++ as₂ ∧ bs = bs₁ ++ bs₂ ∧ xs = zip as₁ bs₁ ∧ ys = zip as₂ bs₂ := by
   simp [zip_eq_zipWith, zipWith_eq_append_iff]
 
-@[simp] theorem zip_mkVector {a : α} {b : β} {n : Nat} :
+@[simp] theorem zip_replicate {a : α} {b : β} {n : Nat} :
-    zip (mkVector n a) (mkVector n b) = mkVector n (a, b) := by
+    zip (replicate n a) (replicate n b) = replicate n (a, b) := by
   ext <;> simp
 
+@[deprecated zip_replicate (since := "2025-03-18")]
+abbrev zip_mkVector := @zip_replicate
 
 /-! ### unzip -/
 
@@ -285,8 +290,11 @@ theorem zip_of_prod {as : Vector α n} {bs : Vector β n} {xs : Vector (α × β
     (hr : xs.map Prod.snd = bs) : xs = as.zip bs := by
   rw [← hl, ← hr, ← zip_unzip xs, ← unzip_fst, ← unzip_snd, zip_unzip, zip_unzip]
 
-@[simp] theorem unzip_mkVector {n : Nat} {a : α} {b : β} :
+@[simp] theorem unzip_replicate {a : α} {b : β} {n : Nat} :
-    unzip (mkVector n (a, b)) = (mkVector n a, mkVector n b) := by
+    unzip (replicate n (a, b)) = (replicate n a, replicate n b) := by
   ext1 <;> simp
 
+@[deprecated unzip_replicate (since := "2025-03-18")]
+abbrev unzip_mkVector := @unzip_replicate
+
 end Vector

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 (.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 (.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

@@ -148,7 +148,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 (.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

@@ -34,7 +34,7 @@ Example:
 -/
 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 result : Array (Option Int) := Array.replicate (pattern.length * word.length * 2) none
-  let mut runLengths : Array Int := Array.mkArray (pattern.length * word.length) 0
+  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

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/ComputedFields.lean

@@ -58,7 +58,7 @@ abbrev M := ReaderT Context MetaM
 def getComputedFieldValue (computedField : Name) (ctorTerm : Expr) : MetaM Expr := do
   let ctorName := ctorTerm.getAppFn.constName!
   let ind ← getConstInfoInduct (← getConstInfoCtor ctorName).induct
-  let val ← mkAppOptM computedField (mkArray (ind.numParams+ind.numIndices) none ++ #[some ctorTerm])
+  let val ← mkAppOptM computedField (.replicate (ind.numParams+ind.numIndices) none ++ #[some ctorTerm])
   let val ←
     if let some wfEqn := WF.eqnInfoExt.find? (← getEnv) computedField then
       pure <| mkAppN (wfEqn.value.instantiateLevelParams wfEqn.levelParams val.getAppFn.constLevels!) val.getAppArgs

src/Lean/Elab/MutualInductive.lean

@@ -389,9 +389,9 @@ For `i ∈ [numParams, arity)`, we have that `result[i]` if this index of the in
 private def computeFixedIndexBitMask (numParams : Nat) (indType : InductiveType) (indFVars : Array Expr) : MetaM (Array Bool) := do
   let arity ← getArity indType
   if arity ≤ numParams then
-    return mkArray arity false
+    return .replicate arity false
   else
-    let maskRef ← IO.mkRef (mkArray numParams false ++ mkArray (arity - numParams) true)
+    let maskRef ← IO.mkRef (.replicate numParams false ++ .replicate (arity - numParams) true)
     let rec go (ctors : List Constructor) : MetaM (Array Bool) := do
       match ctors with
       | [] => maskRef.get

src/Lean/Elab/PreDefinition/FixedParams.lean

@@ -81,7 +81,7 @@ structure Info where
 
 def Info.init (revDeps : Array (Array (Array Nat))) : Info where
   graph := revDeps.map fun deps =>
-    mkArray deps.size (some (mkArray revDeps.size none))
+    .replicate deps.size (some (.replicate revDeps.size none))
   revDeps
 
 def Info.addSelfCalls (info : Info) : Info :=
@@ -309,7 +309,7 @@ scope.
 -/
 private partial def FixedParamPerm.forallTelescopeImpl (perm : FixedParamPerm)
     (type : Expr) (k : Array Expr → MetaM α) : MetaM α := do
-  go 0 type (mkArray perm.numFixed (mkSort 0))
+  go 0 type (.replicate perm.numFixed (mkSort 0))
 where
   go i type xs := do
     match perm[i]? with
@@ -382,7 +382,7 @@ def FixedParamPerm.pickFixed (perm : FixedParamPerm) (xs : Array α) : Array α
     pure #[]
   else
     let dummy := xs[0]
-    let ys := mkArray perm.numFixed dummy
+    let ys := .replicate perm.numFixed dummy
     go (perm.zip xs).toList ys
 where
   go | [], ys => return ys
@@ -437,7 +437,7 @@ def FixedParamPerms.fixedArePrefix (fixedParamPerms : FixedParamPerms) : Bool :=
   fixedParamPerms.perms.all fun paramInfos =>
     paramInfos ==
       (Array.range fixedParamPerms.numFixed).map Option.some ++
-      mkArray (paramInfos.size - fixedParamPerms.numFixed) .none
+      .replicate (paramInfos.size - fixedParamPerms.numFixed) .none
 
 /--
 If `xs` are the fixed parameters that are in scope, and `toErase` are, for each function, the
@@ -453,7 +453,7 @@ def FixedParamPerms.erase  (fixedParamPerms : FixedParamPerms) (xs : Array Expr)
   assert! fixedParamPerms.numFixed  = xs.size
   assert! toErase.size = fixedParamPerms.perms.size
   -- Calculate a mask on the fixed parameters of variables to erase
-  let mut mask := mkArray fixedParamPerms.numFixed false
+  let mut mask := Array.replicate fixedParamPerms.numFixed false
   for funIdx in [:toErase.size], paramIdxs in toErase, mapping in fixedParamPerms.perms do
     for paramIdx in paramIdxs do
       assert! paramIdx < mapping.size

src/Lean/Elab/PreDefinition/Structural/BRecOn.lean

@@ -77,7 +77,7 @@ private def withBelowDict [Inhabited α] (below : Expr) (numIndParams : Nat)
     let motiveTypes ← inferArgumentTypesN numTypeFormers pre
     let numMotives : Nat := positions.numIndices
     trace[Elab.definition.structural] "numMotives: {numMotives}"
-    let mut CTypes := Array.mkArray numMotives (.sort 37) -- dummy value
+    let mut CTypes := Array.replicate numMotives (.sort 37) -- dummy value
     for poss in positions, motiveType in motiveTypes do
       for pos in poss do
         CTypes := CTypes.set! pos motiveType
@@ -274,7 +274,7 @@ def inferBRecOnFTypes (recArgInfos : Array RecArgInfo) (positions : Positions)
     -- And return the types of the next arguments
     arrowDomainsN numTypeFormers brecOnType
 
-  let mut FTypes := Array.mkArray positions.numIndices (Expr.sort 0)
+  let mut FTypes := Array.replicate positions.numIndices (Expr.sort 0)
   for packedFType in packedFTypes, poss in positions do
     for pos in poss do
       FTypes := FTypes.set! pos packedFType

src/Lean/Elab/PreDefinition/Structural/Basic.lean

@@ -70,7 +70,7 @@ def Positions.numIndices (positions : Positions) : Nat :=
 `positions.inverse[k] = i` means that function `i` has type k
 -/
 def Positions.inverse (positions : Positions) : Array Nat := Id.run do
-  let mut r := mkArray positions.numIndices 0
+  let mut r := .replicate positions.numIndices 0
   for _h : i in [:positions.size] do
     for k in positions[i] do
       r := r.set! k i

src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean

@@ -47,7 +47,7 @@ arguments, and other parameters.
 -/
 def RecArgInfo.pickIndicesMajor (info : RecArgInfo) (xs : Array Expr) : (Array Expr × Array Expr) := Id.run do
   -- To simplify the index calculation, pad xs with dummy values where fixed parameters are
-  let xs := info.fixedParamPerm.buildArgs (mkArray info.fixedParamPerm.numFixed (mkSort 0)) xs
+  let xs := info.fixedParamPerm.buildArgs (.replicate info.fixedParamPerm.numFixed (mkSort 0)) xs
   -- First indices and major arg, using the order they appear in `info.indicesPos`
   let mut indexMajorArgs := #[]
   let indexMajorPos := info.indicesPos.push info.recArgPos

src/Lean/Elab/PreDefinition/WF/Fix.lean

@@ -194,7 +194,7 @@ The close coupling with how arguments are packed and termination goals look like
 but it works for now.
 -/
 def groupGoalsByFunction (argsPacker : ArgsPacker) (numFuncs : Nat) (goals : Array MVarId) : MetaM (Array (Array MVarId)) := do
-  let mut r := mkArray numFuncs #[]
+  let mut r := .replicate numFuncs #[]
   for goal in goals do
     let type ← goal.getType
     let (.mdata _ (.app _ param)) := type

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

@@ -494,7 +494,7 @@ def RecCallCache.mk (funNames : Array Name) (decrTactics : Array (Option Decreas
   let decrTactic? := decrTactics[rcc.caller]!
   let callerMeasures := measuress[rcc.caller]!
   let calleeMeasures := measuress[rcc.callee]!
-  let cache ← IO.mkRef <| Array.mkArray callerMeasures.size (Array.mkArray calleeMeasures.size Option.none)
+  let cache ← IO.mkRef <| Array.replicate callerMeasures.size (Array.replicate calleeMeasures.size Option.none)
   return { callerName, decrTactic?, callerMeasures, calleeMeasures, rcc, cache }
 
 /-- Run `evalRecCall` and cache there result -/
@@ -551,7 +551,7 @@ where
   -- Enumerate all permissible uniform combinations
   goUniform (idx : Nat) : OptionT (StateM (Array (Array Nat))) Unit  := do
     if numMeasures.all (idx < ·) then
-      modify (·.push (Array.mkArray numMeasures.size idx))
+      modify (·.push (Array.replicate numMeasures.size idx))
       goUniform (idx + 1)
 
   -- Enumerate all other permissible combinations

src/Lean/Elab/Quotation.lean

@@ -411,7 +411,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
         let no ← no
         match k with
         | `optional =>
-          let nones := mkArray ids.size (← `(none))
+          let nones := .replicate ids.size (← `(none))
           `(let_delayed yes _ $ids* := $yes;
             if __discr.isNone then yes () $[ $nones]*
             else match __discr with

src/Lean/Elab/Tactic/BVDecide/LRAT/Trim.lean

@@ -80,7 +80,7 @@ def run (proof : Array IntAction) (x : M α) : Except String α := do
     | .del .. => acc
   let proof := proof.foldl (init := {}) folder
   let used := Nat.fold proof.size (init := ByteArray.emptyWithCapacity proof.size) (fun _ _ acc => acc.push 0)
-  let mapped := Array.mkArray proof.size 0
+  let mapped := Array.replicate proof.size 0
   return ReaderT.run x { proof, initialId, addEmptyId } |>.run' { used, mapped }
 
 @[inline]

src/Lean/Elab/Tactic/Ext.lean

@@ -110,7 +110,7 @@ def realizeExtTheorem (structName : Name) (flat : Bool) : Elab.Command.CommandEl
         let type ← mkExtType structName flat
         let pf ← withSynthesize do
           let indVal ← getConstInfoInduct structName
-          let params := Array.mkArray indVal.numParams (← `(_))
+          let params := Array.replicate indVal.numParams (← `(_))
           Elab.Term.elabTermEnsuringType (expectedType? := type) (implicitLambda := false)
             -- introduce the params, do cases on 'x' and 'y', and then substitute each equation
             (← `(by intro $params* {..} {..}; intros; subst_eqs; rfl))

src/Lean/Elab/Tactic/Omega/Frontend.lean

@@ -595,7 +595,7 @@ where
       |> String.join
 
   mentioned (atoms : Array Expr) (constraints : Std.HashMap Coeffs Fact) : MetaM (Array Bool) := do
-    let initMask := Array.mkArray atoms.size false
+    let initMask := .replicate atoms.size false
     return constraints.fold (init := initMask) fun mask coeffs _ =>
       coeffs.zipIdx.foldl (init := mask) fun mask (c, i) =>
         if c = 0 then mask else mask.set! i true

src/Lean/Environment.lean

@@ -1635,7 +1635,7 @@ private def setImportedEntries (env : Environment) (mods : Array ModuleData) (st
   for extDescr in extDescrs[startingAt:] do
     -- safety: as in `modifyState`
     states := unsafe extDescr.toEnvExtension.modifyStateImpl states fun s =>
-      { s with importedEntries := mkArray mods.size #[] }
+      { s with importedEntries := .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

@@ -1136,7 +1136,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 (.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
@@ -1151,7 +1151,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 (.replicate nargs dummy) nargs
 
 private def getAppRevArgsAux : Expr → Array Expr → Array Expr
   | app f a, as => getAppRevArgsAux f (as.push a)
@@ -1169,7 +1169,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 (.replicate nargs dummy) (nargs-1)
 
 /-- Return the function (name) and arguments of an application. -/
 def getAppFnArgs (e : Expr) : Name × Array Expr :=
@@ -1182,7 +1182,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 (.replicate n dummy)
 where
   loop : Nat → Expr → Array Expr → Array Expr
     | 0,   _,        as => as

src/Lean/Linter/List.lean

@@ -106,8 +106,8 @@ def numericalWidths (t : InfoTree) : List (Syntax × Name) :=
     if let .ofTermInfo info := info then
       let idxs := match_expr info.expr with
       | List.replicate _ n _ => [n]
-      | Array.mkArray _ n _ => [n]
+      | Array.replicate _ n _ => [n]
-      | Vector.mkVector _ n _ => [n]
+      | Vector.replicate _ n _ => [n]
       | List.range n => [n]
       | List.range' _ n _ => [n]
       | Array.range n => [n]

src/Lean/Meta/IndPredBelow.lean

@@ -441,7 +441,7 @@ partial def mkBelowMatcher
   withExistingLocalDecls (lhss.foldl (init := []) fun s v => s ++ v.fvarDecls) do
     for lhs in lhss do
       trace[Meta.IndPredBelow.match] "{lhs.patterns.map (·.toMessageData)}"
-  let res ← Match.mkMatcher (exceptionIfContainsSorry := true) { matcherName, matchType, discrInfos := mkArray (mkMatcherInput.numDiscrs + 1) {}, lhss }
+  let res ← Match.mkMatcher (exceptionIfContainsSorry := true) { matcherName, matchType, discrInfos := .replicate (mkMatcherInput.numDiscrs + 1) {}, lhss }
   res.addMatcher
   -- if a wrong index is picked, the resulting matcher can be type-incorrect.
   -- we check here, so that errors can propagate higher up the call stack.
@@ -491,7 +491,7 @@ where
       -- `belowCtor` carries a `below`, a non-`below` and a `motive` version of each
       -- field that occurs in a recursive application of the inductive predicate.
       -- `belowIndices` is a mapping from non-`below` to the `below` version of each field.
-      let mut belowFieldOpts := mkArray belowCtor.numFields none
+      let mut belowFieldOpts := .replicate belowCtor.numFields none
       let fields := fields.toArray
       for fieldIdx in [:fields.size] do
         belowFieldOpts := belowFieldOpts.set! belowIndices[fieldIdx]! (some fields[fieldIdx]!)

src/Lean/Meta/Match/MatcherApp/Basic.lean

@@ -54,7 +54,7 @@ def matchMatcherApp? [Monad m] [MonadEnv m] [MonadError m] (e : Expr) (alsoCases
       let params     := args[:info.numParams]
       let motive     := args[info.numParams]!
       let discrs     := args[info.numParams + 1 : info.numParams + 1 + info.numIndices + 1]
-      let discrInfos := Array.mkArray (info.numIndices + 1) {}
+      let discrInfos := .replicate (info.numIndices + 1) {}
       let alts       := args[info.numParams + 1 + info.numIndices + 1 : info.numParams + 1 + info.numIndices + 1 + info.numCtors]
       let remaining  := args[info.numParams + 1 + info.numIndices + 1 + info.numCtors :]
       let uElimPos?  := if info.levelParams.length == declLevels.length then none else some 0

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 ++ .replicate (lemmaArity - ctorInfo.numParams - ctorInfo.numFields) (none (α := Expr))
     let lemmaArgMask := lemmaArgMask ++ ctorFields.toArray.map some
     mkAppOptM lemmaName lemmaArgMask
 

src/Lean/Meta/Tactic/FunInd.lean

@@ -1213,7 +1213,7 @@ def deriveCases (name : Name) : MetaM Unit := do
     setFunIndInfo {
       funIndName := casesName
       levelMask := usMask
-      params := mkArray motiveArity .target
+      params := .replicate motiveArity .target
     }
 
 

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

@@ -16,12 +16,12 @@ def mkModel (goal : Goal) : MetaM (Array (Expr × Nat)) := do
   let dbg := grind.debug.get (← getOptions)
   let nodes := s.nodes
   let isInterpreted (u : Nat) : Bool := isNatNum s.nodes[u]!
-  let mut pre : Array (Option Int) := mkArray nodes.size none
+  let mut pre : Array (Option Int) := .replicate nodes.size none
   /-
   `needAdjust[u]` is true if `u` assignment is not connected to an interpreted value in the graph.
   That is, its assignment may be negative.
   -/
-  let mut needAdjust : Array Bool := mkArray nodes.size true
+  let mut needAdjust : Array Bool := .replicate nodes.size true
   -- Initialize `needAdjust`
   for u in [: nodes.size] do
     if isInterpreted u then

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

@@ -40,7 +40,7 @@ def propagateCtor (a b : Expr) : GoalM Unit := do
     unless (← getEnv).contains injDeclName do return ()
     let info ← getConstInfo injDeclName
     let n := info.type.getForallArity
-    let mask : Array (Option Expr) := mkArray n none
+    let mask : Array (Option Expr) := .replicate n none
     let mask := mask.set! (n-1) (some (← mkEqProof a b))
     let injLemma ← mkAppOptM injDeclName mask
     propagateInjEqs (← inferType injLemma) injLemma

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

@@ -334,7 +334,7 @@ private def main (p : Expr) (cnstrs : List Cnstr) : M Unit := do
   let some apps := (← getThe Goal).appMap.find? p.toHeadIndex
     | return ()
   let numParams  := (← read).thm.numParams
-  let assignment := mkArray numParams unassigned
+  let assignment := .replicate numParams unassigned
   let useMT      := (← read).useMT
   let gmt        := (← getThe Goal).ematch.gmt
   for app in apps do
@@ -356,7 +356,7 @@ It traverses disequalities `a = b`, and tries to solve two matching problems:
 private def matchEqBwdPat (p : Expr) : M Unit := do
   let_expr Grind.eqBwdPattern pα plhs prhs := p | return ()
   let numParams  := (← read).thm.numParams
-  let assignment := mkArray numParams unassigned
+  let assignment := .replicate numParams unassigned
   let useMT      := (← read).useMT
   let gmt        := (← getThe Goal).ematch.gmt
   let false      ← getFalseExpr

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,
+        bottomUps    := .replicate args.size false,
-        higherOrders := mkArray args.size false,
+        higherOrders := .replicate args.size false,
-        provideds    := mkArray args.size false,
+        provideds    := .replicate args.size false,
-        funBinders   := mkArray args.size false
+        funBinders   := .replicate args.size false
       }
 
       if !rest.isEmpty then

src/Lean/Syntax.lean

@@ -509,7 +509,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 (.replicate nesting (mkAtom "$"))
   let term :=
     if term.isIdent then term
     else if term.isOfKind `Lean.Parser.Term.hole then term[0]
@@ -572,7 +572,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 (.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 := .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`
+  { keys    := .replicate cacheSize.toNat (cast lcProof ()), -- `()` is not a valid `Expr`
-    results := mkArray cacheSize.toNat default }
+    results := .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

@@ -171,7 +171,7 @@ namespace Raw₀
 
 /-- Internal implementation detail of the hash map -/
 @[inline] def emptyWithCapacity (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 _)⟩
 
 @[deprecated emptyWithCapacity (since := "2025-03-12"), inherit_doc emptyWithCapacity]
@@ -191,7 +191,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

@@ -221,10 +221,14 @@ theorem toListModel_updateAllBuckets {m : Raw₀ α β} {f : AssocList α β →
 namespace IsHashSelf
 
 @[simp]
-theorem mkArray [BEq α] [Hashable α] {c : Nat} : IsHashSelf
+theorem replicate [BEq α] [Hashable α] {c : Nat} : IsHashSelf
-    (mkArray c (AssocList.nil : AssocList α β)) :=
+    (Array.replicate c (AssocList.nil : AssocList α β)) :=
   ⟨by simp⟩
 
+set_option linter.missingDocs false in
+@[deprecated replicate (since := "2025-03-18")]
+abbrev mkArray := @replicate
+
 theorem uset [BEq α] [Hashable α] {m : Array (AssocList α β)} {i : USize} {h : i.toNat < m.size}
     {d : AssocList α β}
     (hd : HashesTo m[i].toList i.toNat m.size → HashesTo d.toList i.toNat m.size)

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

@@ -30,12 +30,16 @@ open List
 namespace Std.DHashMap.Internal
 
 @[simp]
-theorem toListModel_mkArray_nil {c} :
+theorem toListModel_replicate_nil {c} :
-    toListModel (mkArray c (AssocList.nil : AssocList α β)) = [] := by
+    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]
 
+set_option linter.missingDocs false in
+@[deprecated toListModel_replicate_nil (since := "2025-03-18")]
+abbrev toListModel_mkArray_nil := @toListModel_replicate_nil
+
 @[simp]
 theorem computeSize_eq {buckets : Array (AssocList α β)} :
     computeSize buckets = (toListModel buckets).length := by
@@ -218,7 +222,7 @@ namespace Raw₀
 
 @[simp]
 theorem toListModel_buckets_emptyWithCapacity {c} : toListModel (emptyWithCapacity c : Raw₀ α β).1.buckets = [] :=
-  toListModel_mkArray_nil
+  toListModel_replicate_nil
 
 set_option linter.missingDocs false in
 @[deprecated toListModel_buckets_emptyWithCapacity (since := "2025-03-12")]
@@ -312,7 +316,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⟩
+    ⟨.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)) (.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 := .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

@@ -107,17 +107,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 : (Array.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 hb : ModifiedAssignmentsInvariant (.replicate n unassigned) := by
-      have hsize : (mkArray n unassigned).size = n := by simp only [Array.size_mkArray]
+      have hsize : (Array.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 +185,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