copy across some Find API to Array

src/Init/Data/Array/Basic.lean

@@ -1090,6 +1090,11 @@ def split (as : Array α) (p : α → Bool) : Array α × Array α :=
   as.foldl (init := (#[], #[])) fun (as, bs) a =>
     if p a then (as.push a, bs) else (as, bs.push a)
 
+def replace [BEq α] (xs : Array α) (a b : α) : Array α :=
+  match xs.finIdxOf? a with
+  | none => xs
+  | some i => xs.set i b
+
 /-! ### Lexicographic ordering -/
 
 instance instLT [LT α] : LT (Array α) := ⟨fun as bs => as.toList < bs.toList⟩

src/Init/Data/Array/Find.lean

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

src/Init/Data/Array/Lemmas.lean

@@ -3421,6 +3421,81 @@ theorem eq_push_pop_back!_of_size_ne_zero [Inhabited α] {xs : Array α} (h : xs
       rw [getElem_push_eq, back!]
       simp [← getElem!_pos]
 
+/-! ### replace -/
+
+section replace
+variable [BEq α]
+
+@[simp] theorem size_replace {xs : Array α} : (xs.replace a b).size = xs.size := by
+  simp only [replace]
+  split <;> simp
+
+-- This hypothesis could probably be dropped from some of the lemmas below,
+-- by proving them direct from the definition rather than going via `List`.
+variable [LawfulBEq α]
+
+@[simp] theorem replace_of_not_mem {xs : Array α} (h : ¬ a ∈ xs) : xs.replace a b = xs := by
+  cases xs
+  simp_all
+
+theorem getElem?_replace {xs : Array α} {i : Nat} :
+    (xs.replace a b)[i]? = if xs[i]? == some a then if a ∈ xs.take i then some a else some b else xs[i]? := by
+  rcases xs with ⟨xs⟩
+  simp only [List.replace_toArray, List.getElem?_toArray, List.getElem?_replace, beq_iff_eq,
+    take_eq_extract, List.extract_toArray, List.extract_eq_drop_take, Nat.sub_zero, List.drop_zero,
+    mem_toArray]
+  split <;> rename_i h
+  · rw (occs := [2]) [if_pos]
+    simpa using h
+  · rw [if_neg]
+    simpa using h
+
+theorem getElem?_replace_of_ne {xs : Array α} {i : Nat} (h : xs[i]? ≠ some a) :
+    (xs.replace a b)[i]? = xs[i]? := by
+  simp_all [getElem?_replace]
+
+theorem getElem_replace {xs : Array α} {i : Nat} (h : i < xs.size) :
+    (xs.replace a b)[i]'(by simpa) = if xs[i] == a then if a ∈ xs.take i then a else b else xs[i] := by
+  apply Option.some.inj
+  rw [← getElem?_eq_getElem, getElem?_replace]
+  split <;> split <;> simp_all
+
+theorem getElem_replace_of_ne {xs : Array α} {i : Nat} {h : i < xs.size} (h' : xs[i] ≠ a) :
+    (xs.replace a b)[i]'(by simpa) = xs[i]'(h) := by
+  rw [getElem_replace h]
+  simp [h']
+
+theorem replace_append {xs ys : Array α} :
+    (xs ++ ys).replace a b = if a ∈ xs then xs.replace a b ++ ys else xs ++ ys.replace a b := by
+  rcases xs with ⟨xs⟩
+  rcases ys with ⟨ys⟩
+  simp only [List.append_toArray, List.replace_toArray, List.replace_append, mem_toArray]
+  split <;> simp
+
+theorem replace_append_left {xs ys : Array α} (h : a ∈ xs) :
+    (xs ++ ys).replace a b = xs.replace a b ++ ys := by
+  simp [replace_append, h]
+
+theorem replace_append_right {xs ys : Array α} (h : ¬ a ∈ xs) :
+    (xs ++ ys).replace a b = xs ++ ys.replace a b := by
+  simp [replace_append, h]
+
+theorem replace_extract {xs : Array α} {i : Nat} :
+    (xs.extract 0 i).replace a b = (xs.replace a b).extract 0 i := by
+  rcases xs with ⟨xs⟩
+  simp [List.replace_take]
+
+@[simp] theorem replace_mkArray_self {a : α} (h : 0 < n) :
+    (mkArray n a).replace a b = #[b] ++ mkArray (n - 1) a := by
+  cases n <;> simp_all [mkArray_succ', replace_append]
+
+@[simp] theorem replace_mkArray_ne {a b c : α} (h : !b == a) :
+    (mkArray n a).replace b c = mkArray n a := by
+  rw [replace_of_not_mem]
+  simp_all
+
+end replace
+
 /-! Content below this point has not yet been aligned with `List`. -/
 
 /-! ### sum -/

src/Init/Data/List/Find.lean

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

src/Init/Data/List/Lemmas.lean

@@ -3086,8 +3086,12 @@ variable [BEq α]
 @[simp] theorem replace_cons_self [LawfulBEq α] {a : α} : (a::as).replace a b = b::as := by
   simp [replace_cons]
 
-@[simp] theorem replace_of_not_mem {l : List α} (h : !l.elem a) : l.replace a b = l := by
+@[simp] theorem replace_of_not_mem [LawfulBEq α] {l : List α} (h : a ∉ l) : l.replace a b = l := by
-  induction l <;> simp_all [replace_cons]
+  induction l with
+  | nil => rfl
+  | cons x xs ih =>
+    simp only [replace_cons]
+    split <;> simp_all
 
 @[simp] theorem length_replace {l : List α} : (l.replace a b).length = l.length := by
   induction l with
@@ -3170,7 +3174,7 @@ theorem replace_take {l : List α} {i : Nat} :
     (replicate n a).replace a b = b :: replicate (n - 1) a := by
   cases n <;> simp_all [replicate_succ, replace_cons]
 
-@[simp] theorem replace_replicate_ne {a b c : α} (h : !b == a) :
+@[simp] theorem replace_replicate_ne [LawfulBEq α] {a b c : α} (h : !b == a) :
     (replicate n a).replace b c = replicate n a := by
   rw [replace_of_not_mem]
   simp_all

src/Init/Data/List/ToArray.lean

@@ -658,6 +658,40 @@ private theorem insertIdx_loop_toArray (i : Nat) (l : List α) (j : Nat) (hj : j
   · simp only [size_toArray, Nat.not_le] at h'
     rw [List.insertIdx_of_length_lt (h := h')]
 
+@[simp]
+theorem replace_toArray [BEq α] [LawfulBEq α] (l : List α) (a b : α) :
+    l.toArray.replace a b = (l.replace a b).toArray := by
+  rw [Array.replace]
+  split <;> rename_i i h
+  · simp only [finIdxOf?_toArray, finIdxOf?_eq_none_iff] at h
+    rw [replace_of_not_mem]
+    simpa
+  · simp_all only [finIdxOf?_toArray, finIdxOf?_eq_some_iff, Fin.getElem_fin, set_toArray,
+      mk.injEq]
+    apply List.ext_getElem
+    · simp
+    · intro j h₁ h₂
+      rw [List.getElem_replace, List.getElem_set]
+      by_cases h₃ : j < i
+      · rw [if_neg (by omega), if_neg]
+        simp only [length_set] at h₁ h₃
+        simpa using h.2 ⟨j, by omega⟩ h₃
+      · by_cases h₃ : j = i
+        · rw [if_pos (by omega), if_pos, if_neg]
+          · simp only [mem_take_iff_getElem, not_exists]
+            intro k hk
+            simpa using h.2 ⟨k, by omega⟩ (by show k < i.1; omega)
+          · subst h₃
+            simpa using h.1
+        · rw [if_neg (by omega)]
+          split
+          · rw [if_pos]
+            · simp_all
+            · simp only [mem_take_iff_getElem]
+              simp only [length_set] at h₁
+              exact ⟨i, by omega, h.1⟩
+          · rfl
+
 @[simp] theorem leftpad_toArray (n : Nat) (a : α) (l : List α) :
     Array.leftpad n a l.toArray = (leftpad n a l).toArray := by
   simp [leftpad, Array.leftpad, ← toArray_replicate]

src/Init/Data/Option/Lemmas.lean

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

src/Init/Data/Vector/Basic.lean

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

src/Init/Data/Vector/Lemmas.lean

@@ -246,6 +246,9 @@ abbrev zipWithIndex_mk := @zipIdx_mk
 @[simp] theorem count_mk [BEq α] (xs : Array α) (h : xs.size = n) (a : α) :
     (Vector.mk xs h).count a = xs.count a := rfl
 
+@[simp] theorem replace_mk [BEq α] (xs : Array α) (h : xs.size = n) (a b) :
+    (Vector.mk xs h).replace a b = Vector.mk (xs.replace a b) (by simp [h]) := rfl
+
 @[simp] theorem eq_mk : xs = Vector.mk as h ↔ xs.toArray = as := by
   cases xs
   simp
@@ -406,6 +409,9 @@ theorem toArray_mapM_go [Monad m] [LawfulMonad m] (f : α → m β) (xs : Vector
   cases xs
   simp
 
+@[simp] theorem replace_toArray [BEq α] (xs : Vector α n) (a b) :
+    xs.toArray.replace a b = (xs.replace a b).toArray := rfl
+
 @[simp] theorem find?_toArray (p : α → Bool) (xs : Vector α n) :
     xs.toArray.find? p = xs.find? p := by
   cases xs
@@ -2504,6 +2510,81 @@ theorem pop_append {xs : Vector α n} {ys : Vector α m} :
 @[simp] theorem pop_mkVector (n) (a : α) : (mkVector n a).pop = mkVector (n - 1) a := by
   ext <;> simp
 
+/-! ### replace -/
+
+section replace
+variable [BEq α]
+
+@[simp] theorem replace_cast {xs : Vector α n} {a b : α} :
+    (xs.cast h).replace a b = (xs.replace a b).cast (by simp [h]) := by
+  rcases xs with ⟨xs, rfl⟩
+  simp
+
+-- This hypothesis could probably be dropped from some of the lemmas below,
+-- by proving them direct from the definition rather than going via `List`.
+variable [LawfulBEq α]
+
+@[simp] theorem replace_of_not_mem {xs : Vector α n} (h : ¬ a ∈ xs) : xs.replace a b = xs := by
+  rcases xs with ⟨xs, rfl⟩
+  simp_all
+
+theorem getElem?_replace {xs : Vector α n} {i : Nat} :
+    (xs.replace a b)[i]? = if xs[i]? == some a then if a ∈ xs.take i then some a else some b else xs[i]? := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.getElem?_replace]
+  split <;> rename_i h
+  · rw (occs := [2]) [if_pos]
+    simpa using h
+  · rw [if_neg]
+    simpa using h
+
+theorem getElem?_replace_of_ne {xs : Vector α n} {i : Nat} (h : xs[i]? ≠ some a) :
+    (xs.replace a b)[i]? = xs[i]? := by
+  simp_all [getElem?_replace]
+
+theorem getElem_replace {xs : Vector α n} {i : Nat} (h : i < n) :
+    (xs.replace a b)[i] = if xs[i] == a then if a ∈ xs.take i then a else b else xs[i] := by
+  apply Option.some.inj
+  rw [← getElem?_eq_getElem, getElem?_replace]
+  split <;> split <;> simp_all
+
+theorem getElem_replace_of_ne {xs : Vector α n} {i : Nat} {h : i < n} (h' : xs[i] ≠ a) :
+    (xs.replace a b)[i]'(by simpa) = xs[i]'(h) := by
+  rw [getElem_replace h]
+  simp [h']
+
+theorem replace_append {xs : Vector α n} {ys : Vector α m} :
+    (xs ++ ys).replace a b = if a ∈ xs then xs.replace a b ++ ys else xs ++ ys.replace a b := by
+  rcases xs with ⟨xs, rfl⟩
+  rcases ys with ⟨ys, rfl⟩
+  simp only [mk_append_mk, replace_mk, eq_mk, Array.replace_append]
+  split <;> simp_all
+
+theorem replace_append_left {xs : Vector α n} {ys : Vector α m} (h : a ∈ xs) :
+    (xs ++ ys).replace a b = xs.replace a b ++ ys := by
+  simp [replace_append, h]
+
+theorem replace_append_right {xs : Vector α n} {ys : Vector α m} (h : ¬ a ∈ xs) :
+    (xs ++ ys).replace a b = xs ++ ys.replace a b := by
+  simp [replace_append, h]
+
+theorem replace_extract {xs : Vector α n} {i : Nat} :
+    (xs.extract 0 i).replace a b = (xs.replace a b).extract 0 i := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.replace_extract]
+
+@[simp] theorem replace_mkArray_self {a : α} (h : 0 < n) :
+    (mkVector n a).replace a b = (#v[b] ++ mkVector (n - 1) a).cast (by omega) := by
+  match n, h with
+  | n + 1, _ => simp_all [mkVector_succ', replace_append]
+
+@[simp] theorem replace_mkArray_ne {a b c : α} (h : !b == a) :
+    (mkVector n a).replace b c = mkVector n a := by
+  rw [replace_of_not_mem]
+  simp_all
+
+end replace
+
 /-! Content below this point has not yet been aligned with `List` and `Array`. -/
 
 set_option linter.indexVariables false in