diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 4252bd32c1dd..75e27fa48d77 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -662,9 +662,15 @@ def any (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool
 def all (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool :=
   Id.run <| as.allM p start stop
 
+/-- `as.contains a` is true if there is some element `b` in `as` such that `a == b`. -/
 def contains [BEq α] (as : Array α) (a : α) : Bool :=
   as.any (a == ·)
 
+/--
+Variant of `Array.contains` with arguments reversed.
+
+For verification purposes, we simplify this to `contains`.
+-/
 def elem [BEq α] (a : α) (as : Array α) : Bool :=
   as.contains a
 
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index 49e4b9240ee9..80ded6d67c4f 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -483,7 +483,7 @@ theorem any_iff_exists {p : α → Bool} {as : Array α} {start stop} :
   rw [Bool.eq_false_iff, Ne, any_eq_true]
   simp
 
-theorem any_toList {p : α → Bool} (as : Array α) : as.toList.any p = as.any p := by
+@[simp] theorem any_toList {p : α → Bool} (as : Array α) : as.toList.any p = as.any p := by
   rw [Bool.eq_iff_iff, any_eq_true, List.any_eq_true]
   simp only [List.mem_iff_getElem, getElem_toList]
   exact ⟨fun ⟨_, ⟨i, w, rfl⟩, h⟩ => ⟨i, w, h⟩, fun ⟨i, w, h⟩ => ⟨_, ⟨i, w, rfl⟩, h⟩⟩
@@ -522,7 +522,7 @@ theorem all_iff_forall {p : α → Bool} {as : Array α} {start stop} :
   rw [Bool.eq_false_iff, Ne, all_eq_true]
   simp
 
-theorem all_toList {p : α → Bool} (as : Array α) : as.toList.all p = as.all p := by
+@[simp] theorem all_toList {p : α → Bool} (as : Array α) : as.toList.all p = as.all p := by
   rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true]
   simp only [List.mem_iff_getElem, getElem_toList]
   constructor
@@ -534,20 +534,6 @@ theorem all_toList {p : α → Bool} (as : Array α) : as.toList.all p = as.all
 theorem all_eq_true_iff_forall_mem {l : Array α} : l.all p ↔ ∀ x, x ∈ l → p x := by
   simp only [← all_toList, List.all_eq_true, mem_def]
 
-theorem _root_.List.anyM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
-    l.toArray.anyM p = l.anyM p := by
-  rw [← anyM_toList]
-
-theorem _root_.List.any_toArray (p : α → Bool) (l : List α) : l.toArray.any p = l.any p := by
-  rw [any_toList]
-
-theorem _root_.List.allM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
-    l.toArray.allM p = l.allM p := by
-  rw [← allM_toList]
-
-theorem _root_.List.all_toArray (p : α → Bool) (l : List α) : l.toArray.all p = l.all p := by
-  rw [all_toList]
-
 /-- Variant of `anyM_toArray` with a side condition on `stop`. -/
 @[simp] theorem _root_.List.anyM_toArray' [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α)
     (h : stop = l.toArray.size) :
@@ -574,6 +560,20 @@ theorem _root_.List.all_toArray (p : α → Bool) (l : List α) : l.toArray.all
   subst h
   rw [all_toList]
 
+theorem _root_.List.anyM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
+    l.toArray.anyM p = l.anyM p := by
+  rw [← anyM_toList]
+
+theorem _root_.List.any_toArray (p : α → Bool) (l : List α) : l.toArray.any p = l.any p := by
+  rw [any_toList]
+
+theorem _root_.List.allM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
+    l.toArray.allM p = l.allM p := by
+  rw [← allM_toList]
+
+theorem _root_.List.all_toArray (p : α → Bool) (l : List α) : l.toArray.all p = l.all p := by
+  rw [all_toList]
+
 /-- Variant of `any_eq_true` in terms of membership rather than an array index. -/
 theorem any_eq_true' {p : α → Bool} {as : Array α} :
     as.any p = true ↔ (∃ x, x ∈ as ∧ p x) := by
@@ -641,7 +641,7 @@ theorem decide_forall_mem {xs : Array α} {p : α → Prop} [DecidablePred p] :
     l.toArray.contains a = l.contains a := by
   simp [Array.contains, List.any_beq]
 
-@[simp] theorem _root_.List.elem_toArray [BEq α] {l : List α} {a : α} :
+theorem _root_.List.elem_toArray [BEq α] {l : List α} {a : α} :
     Array.elem a l.toArray = List.elem a l := by
   simp [Array.elem]
 
@@ -663,26 +663,32 @@ theorem all_bne' [BEq α] [PartialEquivBEq α] {xs : Array α} :
     (xs.all fun x => x != a) = !xs.contains a := by
   simp only [bne_comm, all_bne]
 
-theorem mem_of_elem_eq_true [BEq α] [LawfulBEq α] {a : α} {as : Array α} : elem a as = true → a ∈ as := by
+theorem mem_of_contains_eq_true [BEq α] [LawfulBEq α] {a : α} {as : Array α} : as.contains a = true → a ∈ as := by
   cases as
   simp
 
-theorem elem_eq_true_of_mem [BEq α] [LawfulBEq α] {a : α} {as : Array α} (h : a ∈ as) : elem a as = true := by
+@[deprecated mem_of_contains_eq_true (since := "2024-12-12")]
+abbrev mem_of_elem_eq_true := @mem_of_contains_eq_true
+
+theorem contains_eq_true_of_mem [BEq α] [LawfulBEq α] {a : α} {as : Array α} (h : a ∈ as) : as.contains a = true := by
   cases as
   simpa using h
 
+@[deprecated contains_eq_true_of_mem (since := "2024-12-12")]
+abbrev elem_eq_true_of_mem := @contains_eq_true_of_mem
+
 instance [BEq α] [LawfulBEq α] (a : α) (as : Array α) : Decidable (a ∈ as) :=
-  decidable_of_decidable_of_iff (Iff.intro mem_of_elem_eq_true elem_eq_true_of_mem)
+  decidable_of_decidable_of_iff (Iff.intro mem_of_contains_eq_true contains_eq_true_of_mem)
 
 @[simp] theorem elem_eq_contains [BEq α] {a : α} {l : Array α} :
     elem a l = l.contains a := by
   simp [elem]
 
 theorem elem_iff [BEq α] [LawfulBEq α] {a : α} {as : Array α} :
-    elem a as = true ↔ a ∈ as := ⟨mem_of_elem_eq_true, elem_eq_true_of_mem⟩
+    elem a as = true ↔ a ∈ as := ⟨mem_of_contains_eq_true, contains_eq_true_of_mem⟩
 
 theorem contains_iff [BEq α] [LawfulBEq α] {a : α} {as : Array α} :
-    as.contains a = true ↔ a ∈ as := ⟨mem_of_elem_eq_true, elem_eq_true_of_mem⟩
+    as.contains a = true ↔ a ∈ as := ⟨mem_of_contains_eq_true, contains_eq_true_of_mem⟩
 
 theorem elem_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : Array α) :
     elem a as = decide (a ∈ as) := by rw [Bool.eq_iff_iff, elem_iff, decide_eq_true_iff]
@@ -762,24 +768,24 @@ theorem getElem?_set (a : Array α) (i : Nat) (h : i < a.size) (v : α) (j : Nat
   cases as <;> cases n <;> simp [set]
 
 theorem set_comm (a b : α)
-    {n m : Nat} (as : Array α) {hn : n < as.size} {hm : m < (as.set n a).size} (h : n ≠ m) :
-    (as.set n a).set m b = (as.set m b (by simpa using hm)).set n a (by simpa using hn) := by
+    {i j : Nat} (as : Array α) {hi : i < as.size} {hj : j < (as.set i a).size} (h : i ≠ j) :
+    (as.set i a).set j b = (as.set j b (by simpa using hj)).set i a (by simpa using hi) := by
   cases as
   simp [List.set_comm _ _ _ h]
 
 @[simp]
-theorem set_set (a b : α) (as : Array α) (n : Nat) (h : n < as.size) :
-    (as.set n a).set n b (by simpa using h) = as.set n b := by
+theorem set_set (a b : α) (as : Array α) (i : Nat) (h : i < as.size) :
+    (as.set i a).set i b (by simpa using h) = as.set i b := by
   cases as
   simp
 
-theorem mem_set (as : Array α) (n : Nat) (h : n < as.size) (a : α) :
-    a ∈ as.set n a := by
+theorem mem_set (as : Array α) (i : Nat) (h : i < as.size) (a : α) :
+    a ∈ as.set i a := by
   simp [mem_iff_getElem]
-  exact ⟨n, (by simpa using h), by simp⟩
+  exact ⟨i, (by simpa using h), by simp⟩
 
 theorem mem_or_eq_of_mem_set
-    {as : Array α} {n : Nat} {a b : α} {w : n < as.size} (h : a ∈ as.set n b) : a ∈ as ∨ a = b := by
+    {as : Array α} {i : Nat} {a b : α} {w : i < as.size} (h : a ∈ as.set i b) : a ∈ as ∨ a = b := by
   cases as
   simpa using List.mem_or_eq_of_mem_set (by simpa using h)
 
@@ -788,7 +794,10 @@ theorem mem_or_eq_of_mem_set
 
 /-! ### setIfInBounds -/
 
-@[simp] theorem set!_is_setIfInBounds : @set! = @setIfInBounds := rfl
+@[simp] theorem set!_eq_setIfInBounds : @set! = @setIfInBounds := rfl
+
+@[deprecated set!_eq_setIfInBounds (since := "2024-12-12")]
+abbrev set!_is_setIfInBounds := @set!_eq_setIfInBounds
 
 @[simp] theorem size_setIfInBounds (as : Array α) (index : Nat) (val : α) :
     (as.setIfInBounds index val).size = as.size := by
@@ -820,19 +829,23 @@ abbrev getElem_setIfInBounds_eq := @getElem_setIfInBounds_self
     (as.setIfInBounds i v)[j]'hj = as[j]'(by simpa using hj) := by
   simp [getElem_setIfInBounds, h]
 
+theorem getElem?_setIfInBounds {as : Array α} {i j : Nat} {a : α}  :
+    (as.setIfInBounds i a)[j]? = if i = j then if i < as.size then some a else none else as[j]? := by
+  cases as
+  simp [List.getElem?_set]
+
+theorem getElem?_setIfInBounds_self (as : Array α) {i : Nat} (v : α) :
+    (as.setIfInBounds i v)[i]? = if i < as.size then some v else none := by
+  simp [getElem?_setIfInBounds]
+
 @[simp]
-theorem getElem?_setIfInBounds_self (as : Array α) {i : Nat} (p : i < as.size) (v : α) :
+theorem getElem?_setIfInBounds_self_of_lt (as : Array α) {i : Nat} (v : α) (h : i < as.size) :
     (as.setIfInBounds i v)[i]? = some v := by
-  simp [getElem?_eq_getElem, p]
+  simp [getElem?_setIfInBounds, h]
 
 @[deprecated getElem?_setIfInBounds_self (since := "2024-12-11")]
 abbrev getElem?_setIfInBounds_eq := @getElem?_setIfInBounds_self
 
-theorem getElem?_setIfInBounds {as : Array α} {i j : Nat} {a : α}  :
-    (as.setIfInBounds i a)[j]? = if i = j then if i < as.size then some a else none else as[j]? := by
-  cases as
-  simp [List.getElem?_set]
-
 @[simp] theorem getElem?_setIfInBounds_ne {as : Array α} {i j : Nat} (h : i ≠ j) {a : α}  :
     (as.setIfInBounds i a)[j]? = as[j]? := by
   simp [getElem?_setIfInBounds, h]
@@ -847,24 +860,24 @@ theorem setIfInBounds_eq_of_size_le {l : Array α} {n : Nat} (h : l.size ≤ n)
   cases as <;> cases n <;> simp
 
 theorem setIfInBounds_comm (a b : α)
-    {n m : Nat} (as : Array α) (h : n ≠ m) :
-    (as.setIfInBounds n a).setIfInBounds m b = (as.setIfInBounds m b).setIfInBounds n a := by
+    {i j : Nat} (as : Array α) (h : i ≠ j) :
+    (as.setIfInBounds i a).setIfInBounds j b = (as.setIfInBounds j b).setIfInBounds i a := by
   cases as
   simp [List.set_comm _ _ _ h]
 
 @[simp]
-theorem setIfInBounds_setIfInBounds (a b : α) (as : Array α) (n : Nat) :
-    (as.setIfInBounds n a).setIfInBounds n b = as.setIfInBounds n b := by
+theorem setIfInBounds_setIfInBounds (a b : α) (as : Array α) (i : Nat) :
+    (as.setIfInBounds i a).setIfInBounds i b = as.setIfInBounds i b := by
   cases as
   simp
 
-theorem mem_setIfInBounds (as : Array α) (n : Nat) (h : n < as.size) (a : α) :
-    a ∈ as.setIfInBounds n a := by
+theorem mem_setIfInBounds (as : Array α) (i : Nat) (h : i < as.size) (a : α) :
+    a ∈ as.setIfInBounds i a := by
   simp [mem_iff_getElem]
-  exact ⟨n, (by simpa using h), by simp⟩
+  exact ⟨i, (by simpa using h), by simp⟩
 
 theorem mem_or_eq_of_mem_setIfInBounds
-    {as : Array α} {n : Nat} {a b : α} (h : a ∈ as.setIfInBounds n b) : a ∈ as ∨ a = b := by
+    {as : Array α} {i : Nat} {a b : α} (h : a ∈ as.setIfInBounds i b) : a ∈ as ∨ a = b := by
   cases as
   simpa using List.mem_or_eq_of_mem_set (by simpa using h)
 
@@ -2395,7 +2408,7 @@ abbrev get?_eq_toList_get? := @get?_eq_get?_toList
 @[deprecated eq_push_pop_back!_of_size_ne_zero (since := "2024-10-31")]
 abbrev eq_push_pop_back_of_size_ne_zero := @eq_push_pop_back!_of_size_ne_zero
 
-@[deprecated set!_is_setIfInBounds (since := "2024-11-24")] abbrev set_is_setIfInBounds := @set!_is_setIfInBounds
+@[deprecated set!_is_setIfInBounds (since := "2024-11-24")] abbrev set_is_setIfInBounds := @set!_eq_setIfInBounds
 @[deprecated size_setIfInBounds (since := "2024-11-24")] abbrev size_setD := @size_setIfInBounds
 @[deprecated getElem_setIfInBounds_eq (since := "2024-11-24")] abbrev getElem_setD_eq := @getElem_setIfInBounds_self
 @[deprecated getElem?_setIfInBounds_eq (since := "2024-11-24")] abbrev get?_setD_eq := @getElem?_setIfInBounds_self
diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean
index 6efd7af75bf0..b6b7e12bfaa2 100644
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -38,6 +38,10 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
     a ∈ Vector.mk data size ↔ a ∈ data :=
   ⟨fun ⟨h⟩ => h, fun h => ⟨h⟩⟩
 
+@[simp] theorem contains_mk [BEq α] {data : Array α} {size : data.size = n} {a : α} :
+    (Vector.mk data size).contains a = data.contains a := by
+  simp [contains]
+
 @[simp] theorem push_mk {data : Array α} {size : data.size = n} {x : α} :
     (Vector.mk data size).push x =
       Vector.mk (data.push x) (by simp [size, Nat.succ_eq_add_one]) := rfl
@@ -212,6 +216,26 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
 @[simp] theorem toArray_zipWith (f : α → β → γ) (a : Vector α n) (b : Vector β n) :
     (Vector.zipWith a b f).toArray = Array.zipWith a.toArray b.toArray f := rfl
 
+@[simp] theorem anyM_toArray [Monad m] (p : α → m Bool) (v : Vector α n) :
+    v.toArray.anyM p = v.anyM p := by
+  cases v
+  simp
+
+@[simp] theorem allM_toArray [Monad m] (p : α → m Bool) (v : Vector α n) :
+    v.toArray.allM p = v.allM p := by
+  cases v
+  simp
+
+@[simp] theorem any_toArray (p : α → Bool) (v : Vector α n) :
+    v.toArray.any p = v.any p := by
+  cases v
+  simp
+
+@[simp] theorem all_toArray (p : α → Bool) (v : Vector α n) :
+    v.toArray.all p = v.all p := by
+  cases v
+  simp
+
 theorem toArray_inj : ∀ {v w : Vector α n}, v.toArray = w.toArray → v = w
   | {..}, {..}, rfl => rfl
 
@@ -291,6 +315,26 @@ theorem toList_swap (a : Vector α n) (i j) (hi hj) :
 @[simp] theorem toList_zipWith (f : α → β → γ) (a : Vector α n) (b : Vector β n) :
     (Vector.zipWith a b f).toArray = Array.zipWith a.toArray b.toArray f := rfl
 
+@[simp] theorem anyM_toList [Monad m] (p : α → m Bool) (v : Vector α n) :
+    v.toList.anyM p = v.anyM p := by
+  cases v
+  simp
+
+@[simp] theorem allM_toList [Monad m] [LawfulMonad m] (p : α → m Bool) (v : Vector α n) :
+    v.toList.allM p = v.allM p := by
+  cases v
+  simp
+
+@[simp] theorem any_toList (p : α → Bool) (v : Vector α n) :
+    v.toList.any p = v.any p := by
+  cases v
+  simp
+
+@[simp] theorem all_toList (p : α → Bool) (v : Vector α n) :
+    v.toList.all p = v.all p := by
+  cases v
+  simp
+
 theorem toList_inj : ∀ {v w : Vector α n}, v.toList = w.toList → v = w
   | {..}, {..}, rfl => rfl
 
@@ -598,6 +642,271 @@ instance {xs : Vector α n} {p : α → Prop} [DecidablePred p] :
     exact
       ⟨by rintro ⟨i, h, w⟩; exact ⟨_, ⟨i, h, rfl⟩, w⟩, fun ⟨_, ⟨i, h, rfl⟩, w⟩ => ⟨i, h, w⟩⟩)
 
+/-! ### any / all -/
+
+theorem any_iff_exists {p : α → Bool} {xs : Vector α n} :
+    xs.any p ↔ ∃ (i : Nat) (_ : i < n), p xs[i] := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.any_iff_exists]
+
+theorem all_iff_forall {p : α → Bool} {xs : Vector α n} :
+    xs.all p ↔ ∀ (i : Nat) (_ : i < n), p xs[i] := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.all_iff_forall]
+
+theorem any_eq_true {p : α → Bool} {xs : Vector α n} :
+    xs.any p = true ↔ ∃ (i : Nat) (_ : i < n), p xs[i] := by
+  simp [any_iff_exists]
+
+theorem any_eq_false {p : α → Bool} {xs : Vector α n} :
+    xs.any p = false ↔ ∀ (i : Nat) (_ : i < n), ¬p xs[i] := by
+  rw [Bool.eq_false_iff, Ne, any_eq_true]
+  simp
+
+theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] {p : α → m Bool} {xs : Vector α n} :
+    xs.allM p = (! ·) <$> xs.anyM ((! ·) <$> p ·) := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.allM_eq_not_anyM_not]
+
+theorem all_eq_not_any_not {p : α → Bool} {xs : Vector α n} :
+    xs.all p = !(xs.any (!p ·)) := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.all_eq_not_any_not]
+
+@[simp] theorem all_eq_true {p : α → Bool} {xs : Vector α n} :
+    xs.all p = true ↔ ∀ (i : Nat) (_ : i < n), p xs[i] := by
+  simp [all_iff_forall]
+
+@[simp] theorem all_eq_false {p : α → Bool} {xs : Vector α n} :
+    xs.all p = false ↔ ∃ (i : Nat) (_ : i < n), ¬p xs[i] := by
+  rw [Bool.eq_false_iff, Ne, all_eq_true]
+  simp
+
+theorem all_eq_true_iff_forall_mem {xs : Vector α n} : xs.all p ↔ ∀ x, x ∈ xs → p x := by
+  rcases xs with ⟨xs, rfl⟩
+  simp only [all_mk, Array.all_eq_true_iff_forall_mem]
+  simp
+
+/-- Variant of `any_eq_true` in terms of membership rather than an array index. -/
+theorem any_eq_true' {p : α → Bool} {xs : Vector α n} :
+    xs.any p = true ↔ (∃ x, x ∈ xs ∧ p x) := by
+  rcases xs with ⟨xs, rfl⟩
+  simp only [any_mk, Array.any_eq_true']
+  simp
+
+/-- Variant of `any_eq_false` in terms of membership rather than an array index. -/
+theorem any_eq_false' {p : α → Bool} {xs : Vector α n} :
+    xs.any p = false ↔ ∀ x, x ∈ xs → ¬p x := by
+  rcases xs with ⟨xs, rfl⟩
+  simp only [any_mk, Array.any_eq_false']
+  simp
+
+/-- Variant of `all_eq_true` in terms of membership rather than an array index. -/
+theorem all_eq_true' {p : α → Bool} {xs : Vector α n} :
+    xs.all p = true ↔ ∀ x, x ∈ xs → p x := by
+  rcases xs with ⟨xs, rfl⟩
+  simp only [all_mk, Array.all_eq_true']
+  simp
+
+/-- Variant of `all_eq_false` in terms of membership rather than an array index. -/
+theorem all_eq_false' {p : α → Bool} {xs : Vector α n} :
+    xs.all p = false ↔ ∃ x, x ∈ xs ∧ ¬p x := by
+  rcases xs with ⟨xs, rfl⟩
+  simp only [all_mk, Array.all_eq_false']
+  simp
+
+theorem any_eq {xs : Vector α n} {p : α → Bool} : xs.any p = decide (∃ i : Nat, ∃ h, p (xs[i]'h)) := by
+  by_cases h : xs.any p
+  · simp_all [any_eq_true]
+  · simp_all [any_eq_false]
+
+/-- Variant of `any_eq` in terms of membership rather than an array index. -/
+theorem any_eq' {xs : Vector α n} {p : α → Bool} : xs.any p = decide (∃ x, x ∈ xs ∧ p x) := by
+  by_cases h : xs.any p
+  · simp_all [any_eq_true']
+  · simp only [Bool.not_eq_true] at h
+    simp only [h]
+    simp only [any_eq_false'] at h
+    simpa using h
+
+theorem all_eq {xs : Vector α n} {p : α → Bool} : xs.all p = decide (∀ i, (_ : i < n) → p xs[i]) := by
+  by_cases h : xs.all p
+  · simp_all [all_eq_true]
+  · simp only [Bool.not_eq_true] at h
+    simp only [h]
+    simp only [all_eq_false] at h
+    simpa using h
+
+/-- Variant of `all_eq` in terms of membership rather than an array index. -/
+theorem all_eq' {xs : Vector α n} {p : α → Bool} : xs.all p = decide (∀ x, x ∈ xs → p x) := by
+  rcases xs with ⟨xs, rfl⟩
+  simp only [all_mk, Array.all_eq']
+  simp
+
+theorem decide_exists_mem {xs : Vector α n} {p : α → Prop} [DecidablePred p] :
+    decide (∃ x, x ∈ xs ∧ p x) = xs.any p := by
+  simp [any_eq']
+
+theorem decide_forall_mem {xs : Vector α n} {p : α → Prop} [DecidablePred p] :
+    decide (∀ x, x ∈ xs → p x) = xs.all p := by
+  simp [all_eq']
+
+theorem any_beq [BEq α] {xs : Vector α n} {a : α} : (xs.any fun x => a == x) = xs.contains a := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.any_beq]
+
+/-- Variant of `any_beq` with `==` reversed. -/
+theorem any_beq' [BEq α] [PartialEquivBEq α] {xs : Vector α n} :
+    (xs.any fun x => x == a) = xs.contains a := by
+  simp only [BEq.comm, any_beq]
+
+theorem all_bne [BEq α] {xs : Vector α n} : (xs.all fun x => a != x) = !xs.contains a := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.all_bne]
+
+/-- Variant of `all_bne` with `!=` reversed. -/
+theorem all_bne' [BEq α] [PartialEquivBEq α] {xs : Vector α n} :
+    (xs.all fun x => x != a) = !xs.contains a := by
+  simp only [bne_comm, all_bne]
+
+theorem mem_of_contains_eq_true [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} :
+    as.contains a = true → a ∈ as := by
+  rcases as with ⟨as, rfl⟩
+  simp [Array.mem_of_contains_eq_true]
+
+theorem contains_eq_true_of_mem [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} (h : a ∈ as) :
+    as.contains a = true := by
+  rcases as with ⟨as, rfl⟩
+  simp only [mem_mk] at h
+  simp [Array.contains_eq_true_of_mem, h]
+
+instance [BEq α] [LawfulBEq α] (a : α) (as : Vector α n) : Decidable (a ∈ as) :=
+  decidable_of_decidable_of_iff (Iff.intro mem_of_contains_eq_true contains_eq_true_of_mem)
+
+theorem contains_iff [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} :
+    as.contains a = true ↔ a ∈ as := ⟨mem_of_contains_eq_true, contains_eq_true_of_mem⟩
+
+@[simp] theorem contains_eq_mem [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} :
+    as.contains a = decide (a ∈ as) := by
+  rw [Bool.eq_iff_iff, contains_iff, decide_eq_true_iff]
+
+@[simp] theorem any_push [BEq α] {as : Vector α n} {a : α} {p : α → Bool} :
+    (as.push a).any p = (as.any p || p a) := by
+  rcases as with ⟨as, rfl⟩
+  simp [Array.any_push]
+
+@[simp] theorem all_push [BEq α] {as : Vector α n} {a : α} {p : α → Bool} :
+    (as.push a).all p = (as.all p && p a) := by
+  rcases as with ⟨as, rfl⟩
+  simp [Array.all_push]
+
+@[simp] theorem contains_push [BEq α] {l : Vector α n} {a : α} {b : α} :
+    (l.push a).contains b = (l.contains b || b == a) := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.contains_push]
+
+/-! ### set -/
+
+theorem getElem_set (v : Vector α n) (i : Nat) (x : α) (hi : i < n) (j : Nat) (hj : j < n) :
+    (v.set i x hi)[j] = if i = j then x else v[j] := by
+  cases v
+  split <;> simp_all [Array.getElem_set]
+
+@[simp] theorem getElem_set_self (v : Vector α n) (i : Nat) (x : α) (hi : i < n) :
+    (v.set i x hi)[i] = x := by simp [getElem_set]
+
+@[deprecated getElem_set_self (since := "2024-12-12")]
+abbrev getElem_set_eq := @getElem_set_self
+
+@[simp] theorem getElem_set_ne (v : Vector α n) (i : Nat) (x : α) (hi : i < n) (j : Nat)
+    (hj : j < n) (h : i ≠ j) : (v.set i x hi)[j] = v[j] := by simp [getElem_set, h]
+
+theorem getElem?_set (v : Vector α n) (i : Nat) (hi : i < n) (x : α) (j : Nat) :
+    (v.set i x hi)[j]? = if i = j then some x else v[j]? := by
+  cases v
+  split <;> simp_all [getElem?_eq_getElem, getElem_set]
+
+@[simp] theorem getElem?_set_self (v : Vector α n) (i : Nat) (hi : i < n) (x : α) :
+    (v.set i x hi)[i]? = some x := by simp [getElem?_eq_getElem, hi]
+
+@[simp] theorem getElem?_set_ne (v : Vector α n) (i : Nat) (hi : i < n) (x : α) (j : Nat)
+    (h : i ≠ j) : (v.set i x hi)[j]? = v[j]? := by
+  simp [getElem?_set, h]
+
+@[simp] theorem set_getElem_self {v : Vector α n} {i : Nat} (hi : i < n) :
+    v.set i v[i] hi = v := by
+  cases v
+  simp
+
+theorem set_comm (a b : α) {i j : Nat} (v : Vector α n) {hi : i < n} {hj : j < n} (h : i ≠ j) :
+    (v.set i a hi).set j b hj = (v.set j b hj).set i a hi := by
+  cases v
+  simp [Array.set_comm, h]
+
+@[simp] theorem set_set (a b : α) (v : Vector α n) (i : Nat) (hi : i < n) :
+    (v.set i a hi).set i b hi = v.set i b hi := by
+  cases v
+  simp
+
+theorem mem_set (v : Vector α n) (i : Nat) (hi : i < n) (a : α) :
+    a ∈ v.set i a hi := by
+  simp [mem_iff_getElem]
+  exact ⟨i, (by simpa using hi), by simp⟩
+
+theorem mem_or_eq_of_mem_set {v : Vector α n} {i : Nat} {a b : α} {w : i < n} (h : a ∈ v.set i b) : a ∈ v ∨ a = b := by
+  cases v
+  simpa using Array.mem_or_eq_of_mem_set (by simpa using h)
+
+/-! ### setIfInBounds -/
+
+theorem getElem_setIfInBounds (a : Vector α n) (i : Nat) (x : α) (j : Nat)
+    (hj : j < n) : (a.setIfInBounds i x)[j] = if i = j then x else a[j] := by
+  cases a
+  split <;> simp_all [Array.getElem_setIfInBounds]
+
+@[simp] theorem getElem_setIfInBounds_self (v : Vector α n) (i : Nat) (x : α) (hi : i < n) :
+    (v.setIfInBounds i x)[i] = x := by simp [getElem_setIfInBounds, hi]
+
+@[deprecated getElem_setIfInBounds_self (since := "2024-12-12")]
+abbrev getElem_setIfInBounds_eq := @getElem_setIfInBounds_self
+
+@[simp] theorem getElem_setIfInBounds_ne (v : Vector α n) (i : Nat) (x : α) (j : Nat)
+    (hj : j < n) (h : i ≠ j) : (v.setIfInBounds i x)[j] = v[j] := by simp [getElem_setIfInBounds, h]
+
+theorem getElem?_setIfInBounds (v : Vector α n) (i : Nat) (x : α) (j : Nat) :
+    (v.setIfInBounds i x)[j]? = if i = j then if i < n then some x else none else v[j]? := by
+  rcases v with ⟨v, rfl⟩
+  simp [Array.getElem?_setIfInBounds]
+
+theorem getElem?_setIfInBounds_self (v : Vector α n) (i : Nat) (x : α) :
+    (v.setIfInBounds i x)[i]? = if i < n then some x else none := by simp [getElem?_setIfInBounds]
+
+@[simp] theorem getElem?_setIfInBounds_self_of_lt (v : Vector α n) (i : Nat) (x : α) (h : i < n) :
+    (v.setIfInBounds i x)[i]? = some x := by simp [getElem?_setIfInBounds, h]
+
+@[simp] theorem getElem?_setIfInBounds_ne (a : Vector α n) (i : Nat) (x : α) (j : Nat)
+    (h : i ≠ j) : (a.setIfInBounds i x)[j]? = a[j]? := by simp [getElem?_setIfInBounds, h]
+
+theorem setIfInBounds_eq_of_size_le {l : Vector α n} {m : Nat} (h : l.size ≤ m) {a : α} :
+    l.setIfInBounds m a = l := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.setIfInBounds_eq_of_size_le (by simpa using h)]
+
+theorem setIfInBound_comm (a b : α) {i j : Nat} (v : Vector α n) (h : i ≠ j) :
+    (v.setIfInBounds i a).setIfInBounds j b = (v.setIfInBounds j b).setIfInBounds i a := by
+  rcases v with ⟨v, rfl⟩
+  simp only [setIfInBounds_mk, mk.injEq]
+  rw [Array.setIfInBounds_comm _ _ _ h]
+
+@[simp] theorem setIfInBounds_setIfInBounds (a b : α) (v : Vector α n) (i : Nat) :
+    (v.setIfInBounds i a).setIfInBounds i b = v.setIfInBounds i b := by
+  rcases v with ⟨v, rfl⟩
+  simp
+
+theorem mem_setIfInBounds (v : Vector α n) (i : Nat) (hi : i < n) (a : α) :
+    a ∈ v.setIfInBounds i a := by
+  simp [mem_iff_getElem]
+  exact ⟨i, (by simpa using hi), by simp⟩
 
 /-! Content below this point has not yet been aligned with `List` and `Array`. -/
 
@@ -649,32 +958,6 @@ defeq issues in the implicit size argument.
     subst h
     simp [pop, back, back!, ← Array.eq_push_pop_back!_of_size_ne_zero]
 
-/-! ### set -/
-
-theorem getElem_set (a : Vector α n) (i : Nat) (x : α) (hi : i < n) (j : Nat) (hj : j < n) :
-    (a.set i x hi)[j] = if i = j then x else a[j] := by
-  cases a
-  split <;> simp_all [Array.getElem_set]
-
-@[simp] theorem getElem_set_eq (a : Vector α n) (i : Nat) (x : α) (hi : i < n) :
-    (a.set i x hi)[i] = x := by simp [getElem_set]
-
-@[simp] theorem getElem_set_ne (a : Vector α n) (i : Nat) (x : α) (hi : i < n) (j : Nat)
-    (hj : j < n) (h : i ≠ j) : (a.set i x hi)[j] = a[j] := by simp [getElem_set, h]
-
-/-! ### setIfInBounds -/
-
-theorem getElem_setIfInBounds (a : Vector α n) (i : Nat) (x : α) (j : Nat)
-    (hj : j < n) : (a.setIfInBounds i x)[j] = if i = j then x else a[j] := by
-  cases a
-  split <;> simp_all [Array.getElem_setIfInBounds]
-
-@[simp] theorem getElem_setIfInBounds_eq (a : Vector α n) (i : Nat) (x : α) (hj : i < n) :
-    (a.setIfInBounds i x)[i] = x := by simp [getElem_setIfInBounds]
-
-@[simp] theorem getElem_setIfInBounds_ne (a : Vector α n) (i : Nat) (x : α) (j : Nat)
-    (hj : j < n) (h : i ≠ j) : (a.setIfInBounds i x)[j] = a[j] := by simp [getElem_setIfInBounds, h]
-
 /-! ### append -/
 
 theorem getElem_append (a : Vector α n) (b : Vector α m) (i : Nat) (hi : i < n + m) :