diff --git a/src/Init/Data/Vector/Attach.lean b/src/Init/Data/Vector/Attach.lean
index 5bb276fb62..f00db1eda0 100644
--- a/src/Init/Data/Vector/Attach.lean
+++ b/src/Init/Data/Vector/Attach.lean
@@ -69,7 +69,8 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
 
 @[simp] theorem toList_attachWith {xs : Vector α n} {P : α → Prop} {H : ∀ x ∈ xs, P x} :
    (xs.attachWith P H).toList = xs.toList.attachWith P (by simpa using H) := by
-  simp [attachWith]
+  rcases xs with ⟨xs, rfl⟩
+  simp
 
 @[simp] theorem toList_attach {xs : Vector α n} :
     xs.attach.toList = xs.toList.attachWith (· ∈ xs) (by simp) := by
@@ -77,7 +78,8 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
 
 @[simp] theorem toList_pmap {xs : Vector α n} {P : α → Prop} {f : ∀ a, P a → β} {H : ∀ a ∈ xs, P a} :
     (xs.pmap f H).toList = xs.toList.pmap f (fun a m => H a (by simpa using m)) := by
-  simp [pmap]
+  rcases xs with ⟨xs, rfl⟩
+  simp
 
 /-- Implementation of `pmap` using the zero-copy version of `attach`. -/
 @[inline] private def pmapImpl {P : α → Prop} (f : ∀ a, P a → β) (xs : Vector α n) (H : ∀ a ∈ xs, P a) :
@@ -492,7 +494,8 @@ def unattach {α : Type _} {p : α → Prop} (xs : Vector { x // p x } n) : Vect
 
 @[simp] theorem toList_unattach {p : α → Prop} {xs : Vector { x // p x } n} :
     xs.unattach.toList = xs.toList.unattach := by
-  simp [unattach]
+  rcases xs with ⟨xs, rfl⟩
+  simp
 
 @[simp] theorem unattach_attach {xs : Vector α n} : xs.attach.unattach = xs := by
   rcases xs with ⟨xs, rfl⟩
diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean
index eef56e719c..b481cc7616 100644
--- a/src/Init/Data/Vector/Basic.lean
+++ b/src/Init/Data/Vector/Basic.lean
@@ -24,7 +24,9 @@ set_option linter.listVariables true -- Enforce naming conventions for `List`/`A
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 /-- `Vector α n` is an `Array α` with size `n`. -/
-structure Vector (α : Type u) (n : Nat) extends Array α where
+structure Vector (α : Type u) (n : Nat) where
+  /-- The underlying array. -/
+  toArray : Array α
   /-- Array size. -/
   size_toArray : toArray.size = n
 deriving Repr, DecidableEq
@@ -38,6 +40,9 @@ abbrev Array.toVector (xs : Array α) : Vector α xs.size := .mk xs rfl
 
 namespace Vector
 
+/-- The size of a vector. -/
+abbrev size {α n} (_ : Vector α n) : Nat := n
+
 /-- Syntax for `Vector α n` -/
 syntax (name := «term#v[_,]») "#v[" withoutPosition(term,*,?) "]" : term
 
@@ -48,6 +53,9 @@ macro_rules
 recommended_spelling "empty" for "#v[]" in [Vector.mk, «term#v[_,]»]
 recommended_spelling "singleton" for "#v[x]" in [Vector.mk, «term#v[_,]»]
 
+/-- Convert a vector to a list. -/
+def toList (xs : Vector α n) : List α := xs.toArray.toList
+
 /-- Custom eliminator for `Vector α n` through `Array α` -/
 @[elab_as_elim]
 def elimAsArray {motive : Vector α n → Sort u}
@@ -469,6 +477,16 @@ to avoid having to have the predicate live in `p : α → m (ULift Bool)`.
 @[inline] def replace [BEq α] (xs : Vector α n) (a b : α) : Vector α n :=
   ⟨xs.toArray.replace a b, by simp⟩
 
+/--
+Computes the sum of the elements of a vector.
+
+Examples:
+ * `#v[a, b, c].sum = a + (b + (c + 0))`
+ * `#v[1, 2, 5].sum = 8`
+-/
+@[inline] def sum [Add α] [Zero α] (xs : Vector α n) : α :=
+  xs.toArray.sum
+
 /--
 Pad a vector on the left with a given element.
 
diff --git a/src/Init/Data/Vector/Count.lean b/src/Init/Data/Vector/Count.lean
index 463659343c..c3cf4e002a 100644
--- a/src/Init/Data/Vector/Count.lean
+++ b/src/Init/Data/Vector/Count.lean
@@ -66,8 +66,8 @@ theorem countP_le_size {xs : Vector α n} : countP p xs ≤ n := by
   cases xs
   simp
 
-@[simp] theorem countP_eq_size {p} : countP p xs = xs.size ↔ ∀ a ∈ xs, p a := by
-  cases xs
+@[simp] theorem countP_eq_size {p} {xs : Vector α n} : countP p xs = n ↔ ∀ a ∈ xs, p a := by
+  rcases xs with ⟨xs, rfl⟩
   simp
 
 @[simp] theorem countP_cast (p : α → Bool) (xs : Vector α n) : countP p (xs.cast h) = countP p xs := by
@@ -213,7 +213,7 @@ theorem not_mem_of_count_eq_zero {a : α} {xs : Vector α n} (h : count a xs = 0
 theorem count_eq_zero {xs : Vector α n} : count a xs = 0 ↔ a ∉ xs :=
   ⟨not_mem_of_count_eq_zero, count_eq_zero_of_not_mem⟩
 
-theorem count_eq_size {xs : Vector α n} : count a xs = xs.size ↔ ∀ b ∈ xs, a = b := by
+theorem count_eq_size {xs : Vector α n} : count a xs = n ↔ ∀ b ∈ xs, a = b := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.count_eq_size]
 
diff --git a/src/Init/Data/Vector/Extract.lean b/src/Init/Data/Vector/Extract.lean
index b287d7edc7..93bc8e14cc 100644
--- a/src/Init/Data/Vector/Extract.lean
+++ b/src/Init/Data/Vector/Extract.lean
@@ -88,7 +88,7 @@ theorem extract_set {xs : Vector α n} {i j k : Nat} (h : k < n) {a : α} :
     (xs.set k a).extract i j =
       if _ : k < i then
         xs.extract i j
-      else if _ : k < min j xs.size then
+      else if _ : k < min j n then
         (xs.extract i j).set (k - i) a (by omega)
       else xs.extract i j := by
   rcases xs with ⟨xs, rfl⟩
diff --git a/src/Init/Data/Vector/Find.lean b/src/Init/Data/Vector/Find.lean
index ef45d45281..9ace879a79 100644
--- a/src/Init/Data/Vector/Find.lean
+++ b/src/Init/Data/Vector/Find.lean
@@ -196,20 +196,6 @@ theorem get_find?_mem {xs : Vector α n} (h) : (xs.find? p).get h ∈ xs := by
   cases xs
   simp [Array.get_find?_mem]
 
-@[simp] theorem find?_filter {xs : Vector α n} (p q : α → Bool) :
-    (xs.filter p).find? q = xs.find? (fun a => p a ∧ q a) := by
-  cases xs; simp
-
-@[simp] theorem getElem?_zero_filter {p : α → Bool} {xs : Vector α n} :
-    (xs.filter p)[0]? = xs.find? p := by
-  cases xs; simp [← List.head?_eq_getElem?]
-
-@[simp] theorem getElem_zero_filter {p : α → Bool} {xs : Vector α n} (h) :
-    (xs.filter p)[0] =
-      (xs.find? p).get (by cases xs; simpa [← Array.countP_eq_size_filter] using h) := by
-  cases xs
-  simp [List.getElem_zero_eq_head]
-
 @[simp] theorem find?_map {f : β → α} {xs : Vector β n} :
     find? p (xs.map f) = (xs.find? (p ∘ f)).map f := by
   cases xs; simp
@@ -323,7 +309,7 @@ theorem findFinIdx?_push {xs : Vector α n} {a : α} {p : α → Bool} :
 theorem findFinIdx?_append {xs : Vector α n₁} {ys : Vector α n₂} {p : α → Bool} :
     (xs ++ ys).findFinIdx? p =
       ((xs.findFinIdx? p).map (Fin.castLE (by simp))).or
-        ((ys.findFinIdx? p).map (Fin.natAdd xs.size) |>.map (Fin.cast (by simp))) := by
+        ((ys.findFinIdx? p).map (Fin.natAdd n₁)) := by
   rcases xs with ⟨xs, rfl⟩
   rcases ys with ⟨ys, rfl⟩
   simp [Array.findFinIdx?_append, Option.map_or, Function.comp_def]
diff --git a/src/Init/Data/Vector/InsertIdx.lean b/src/Init/Data/Vector/InsertIdx.lean
index ad1a150be0..da508df6dc 100644
--- a/src/Init/Data/Vector/InsertIdx.lean
+++ b/src/Init/Data/Vector/InsertIdx.lean
@@ -104,7 +104,7 @@ theorem getElem?_insertIdx {xs : Vector α n} {x : α} {i k : Nat} (h : i ≤ n)
         xs[k]?
       else
         if k = i then
-          if k ≤ xs.size then some x else none
+          if k ≤ n then some x else none
         else
           xs[k-1]? := by
   rcases xs with ⟨xs, rfl⟩
diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean
index 47397d674b..d00cc957aa 100644
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -63,9 +63,6 @@ theorem toArray_mk {xs : Array α} (h : xs.size = n) : (Vector.mk xs h).toArray
     (Vector.mk xs h == Vector.mk ys h') = (xs == ys) := by
   simp [instBEq, isEqv, Array.instBEq, Array.isEqv, h, h']
 
-@[simp] theorem allDiff_mk [BEq α] {xs : Array α} (h : xs.size = n) :
-    (Vector.mk xs h).allDiff = xs.allDiff := rfl
-
 @[simp] theorem mk_append_mk {xs ys : Array α} (h : xs.size = n) (h' : ys.size = m) :
     Vector.mk xs h ++ Vector.mk ys h' = Vector.mk (xs ++ ys) (by simp [h, h']) := rfl
 
@@ -253,6 +250,9 @@ abbrev zipWithIndex_mk := @zipIdx_mk
 @[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 sum_mk [Add α] [Zero α] {xs : Array α} (h : xs.size = n) :
+    (Vector.mk xs h).sum = xs.sum := rfl
+
 @[simp] theorem eq_mk : xs = Vector.mk as h ↔ xs.toArray = as := by
   cases xs
   simp
@@ -276,8 +276,10 @@ abbrev zipWithIndex_mk := @zipIdx_mk
 @[simp, grind _=_] theorem toArray_append {xs : Vector α m} {ys : Vector α n} :
     (xs ++ ys).toArray = xs.toArray ++ ys.toArray := rfl
 
+set_option linter.indexVariables false in
 @[simp, grind] theorem toArray_drop {xs : Vector α n} {i} :
-    (xs.drop i).toArray = xs.toArray.extract i xs.size := rfl
+    (xs.drop i).toArray = xs.toArray.extract i n := by
+  simp [drop]
 
 @[simp, grind] theorem toArray_empty : (#v[] : Vector α 0).toArray = #[] := rfl
 
@@ -498,7 +500,13 @@ protected theorem ext {xs ys : Vector α n} (h : (i : Nat) → (_ : i < n) → x
 
 /-! ### toList -/
 
-theorem toArray_toList {xs : Vector α n} : xs.toArray.toList = xs.toList := rfl
+@[simp, grind] theorem length_toList {xs : Vector α n} : xs.toList.length = n := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [toList]
+
+@[grind =_] theorem toList_toArray {xs : Vector α n} : xs.toArray.toList = xs.toList := rfl
+
+@[simp, grind] theorem toList_mk : (Vector.mk xs h).toList = xs.toList := rfl
 
 @[simp] theorem getElem_toList {xs : Vector α n} {i : Nat} (h : i < xs.toList.length) :
     xs.toList[i] = xs[i]'(by simpa using h) := by
@@ -511,11 +519,11 @@ theorem toArray_toList {xs : Vector α n} : xs.toArray.toList = xs.toList := rfl
   simp
 
 theorem toList_append {xs : Vector α m} {ys : Vector α n} :
-    (xs ++ ys).toList = xs.toList ++ ys.toList := by simp
+    (xs ++ ys).toList = xs.toList ++ ys.toList := by simp [toList]
 
 @[simp] theorem toList_drop {xs : Vector α n} {i} :
     (xs.drop i).toList = xs.toList.drop i := by
-  simp [List.take_of_length_le]
+  simp [toList, List.take_of_length_le]
 
 theorem toList_empty : (#v[] : Vector α 0).toList = [] := rfl
 
@@ -526,14 +534,14 @@ theorem toList_emptyWithCapacity {cap} :
 abbrev toList_mkEmpty := @toList_emptyWithCapacity
 
 theorem toList_eraseIdx {xs : Vector α n} {i} (h) :
-    (xs.eraseIdx i h).toList = xs.toList.eraseIdx i := by simp
+    (xs.eraseIdx i h).toList = xs.toList.eraseIdx i := by simp [toList]
 
 @[simp] theorem toList_eraseIdx! {xs : Vector α n} {i} (hi : i < n) :
     (xs.eraseIdx! i).toList = xs.toList.eraseIdx i := by
   cases xs; simp_all [Array.eraseIdx!]
 
 theorem toList_insertIdx {xs : Vector α n} {i x} (h) :
-    (xs.insertIdx i x h).toList = xs.toList.insertIdx i x := by simp
+    (xs.insertIdx i x h).toList = xs.toList.insertIdx i x := by simp [toList]
 
 theorem toList_insertIdx! {xs : Vector α n} {i x} (hi : i ≤ n) :
     (xs.insertIdx! i x).toList = xs.toList.insertIdx i x := by
@@ -544,39 +552,39 @@ theorem toList_cast {xs : Vector α n} (h : n = m) :
 
 theorem toList_extract {xs : Vector α n} {start stop} :
     (xs.extract start stop).toList = (xs.toList.drop start).take (stop - start) := by
-  simp
+  simp [toList]
 
 theorem toList_map {f : α → β} {xs : Vector α n} :
-    (xs.map f).toList = xs.toList.map f := by simp
+    (xs.map f).toList = xs.toList.map f := by simp [toList]
 
 theorem toList_mapIdx {f : Nat → α → β} {xs : Vector α n} :
-    (xs.mapIdx f).toList = xs.toList.mapIdx f := by simp
+    (xs.mapIdx f).toList = xs.toList.mapIdx f := by simp [toList]
 
 theorem toList_mapFinIdx {f : (i : Nat) → α → (h : i < n) → β} {xs : Vector α n} :
     (xs.mapFinIdx f).toList =
       xs.toList.mapFinIdx (fun i a h => f i a (by simpa [xs.size_toArray] using h)) := by
-  simp
+  simp [toList]
 
-theorem toList_ofFn {f : Fin n → α} : (Vector.ofFn f).toList = List.ofFn f := by simp
+theorem toList_ofFn {f : Fin n → α} : (Vector.ofFn f).toList = List.ofFn f := by simp [toList]
 
-theorem toList_pop {xs : Vector α n} : xs.pop.toList = xs.toList.dropLast := rfl
+theorem toList_pop {xs : Vector α n} : xs.pop.toList = xs.toList.dropLast := by simp [toList]
 
-theorem toList_push {xs : Vector α n} {x} : (xs.push x).toList = xs.toList ++ [x] := by simp
+theorem toList_push {xs : Vector α n} {x} : (xs.push x).toList = xs.toList ++ [x] := by simp [toList]
 
 @[simp] theorem toList_beq_toList [BEq α] {xs : Vector α n} {ys : Vector α n} :
     (xs.toList == ys.toList) = (xs == ys) := by
-  simp [instBEq, isEqv, Array.instBEq, Array.isEqv, xs.2, ys.2]
+  simp [toList]
 
-theorem toList_range : (Vector.range n).toList = List.range n := by simp
+theorem toList_range : (Vector.range n).toList = List.range n := by simp [toList]
 
-theorem toList_reverse {xs : Vector α n} : xs.reverse.toList = xs.toList.reverse := by simp
+theorem toList_reverse {xs : Vector α n} : xs.reverse.toList = xs.toList.reverse := by simp [toList]
 
 theorem toList_set {xs : Vector α n} {i x} (h) :
     (xs.set i x).toList = xs.toList.set i x := rfl
 
 @[simp] theorem toList_setIfInBounds {xs : Vector α n} {i x} :
     (xs.setIfInBounds i x).toList = xs.toList.set i x := by
-  simp [Vector.setIfInBounds]
+  simp [toList, Vector.setIfInBounds]
 
 theorem toList_singleton {x : α} : (Vector.singleton x).toList = [x] := rfl
 
@@ -584,7 +592,7 @@ theorem toList_swap {xs : Vector α n} {i j} (hi hj) :
     (xs.swap i j).toList = (xs.toList.set i xs[j]).set j xs[i] := rfl
 
 @[simp] theorem toList_take {xs : Vector α n} {i} : (xs.take i).toList = xs.toList.take i := by
-  simp [List.take_of_length_le]
+  simp [toList, List.take_of_length_le]
 
 @[simp] theorem toList_zipWith {f : α → β → γ} {as : Vector α n} {bs : Vector β n} :
     (Vector.zipWith f as bs).toList = List.zipWith f as.toList bs.toList := by
@@ -664,16 +672,14 @@ theorem toList_inj {xs ys : Vector α n} : xs.toList = ys.toList ↔ xs = ys :=
 
 @[simp] theorem toList_eq_nil_iff {xs : Vector α n} : xs.toList = [] ↔ n = 0 := by
   rcases xs with ⟨xs, h⟩
-  simp only [Array.toList_eq_nil_iff]
+  simp only [toList, Array.toList_eq_nil_iff]
   exact ⟨by rintro rfl; simp_all, by rintro rfl; simpa using h⟩
 
 @[deprecated toList_eq_nil_iff (since := "2025-04-04")]
 abbrev toList_eq_empty_iff {α n} (xs) := @toList_eq_nil_iff α n xs
 
 @[simp] theorem mem_toList_iff {a : α} {xs : Vector α n} : a ∈ xs.toList ↔ a ∈ xs := by
-  simp
-
-theorem length_toList {α n} (xs : Vector α n) : xs.toList.length = n := by simp
+  simp [toList]
 
 /-! ### empty -/
 
@@ -1320,7 +1326,7 @@ theorem getElem?_setIfInBounds_self {xs : Vector α n} {x : α} :
 @[simp] theorem getElem?_setIfInBounds_ne {xs : Vector α n} {x : α} (h : i ≠ j) :
     (xs.setIfInBounds i x)[j]? = xs[j]? := by simp [getElem?_setIfInBounds, h]
 
-theorem setIfInBounds_eq_of_size_le {xs : Vector α n} {i : Nat} (h : xs.size ≤ i) {a : α} :
+theorem setIfInBounds_eq_of_size_le {xs : Vector α n} {i : Nat} (h : n ≤ i) {a : α} :
     xs.setIfInBounds i a = xs := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.setIfInBounds_eq_of_size_le (by simpa using h)]
@@ -1864,7 +1870,7 @@ set_option linter.listVariables false in
   induction l generalizing i with
   | nil => simp at hi
   | cons xs l ih =>
-    simp only [List.map_cons, List.map_map, List.flatten_cons]
+    simp only [List.map_cons, List.map_map, List.flatten_cons, toList_toArray]
     by_cases h : i < m
     · rw [List.getElem_append_left (by simpa)]
       have h₁ : i / m = 0 := Nat.div_eq_of_lt h
@@ -1872,13 +1878,13 @@ set_option linter.listVariables false in
       simp [h₁, h₂]
     · have h₁ : xs.toList.length ≤ i := by simp; omega
       rw [List.getElem_append_right h₁]
-      simp only [Array.length_toList, size_toArray]
+      simp only [length_toList]
       specialize ih (i := i - m) (by simp_all [Nat.add_one_mul]; omega)
       have h₂ : i / m = (i - m) / m + 1 := by
         conv => lhs; rw [show i = i - m + m by omega]
         rw [Nat.add_div_right]
         exact Nat.pos_of_lt_mul_left hi
-      simp only [Array.length_toList, size_toArray] at h₁
+      simp only [length_toList] at h₁
       have h₃ : (i - m) % m = i % m := (Nat.mod_eq_sub_mod h₁).symm
       simp_all
 
@@ -2215,7 +2221,7 @@ theorem flatMap_replicate {f : α → Vector β m} : (replicate n a).flatMap f =
 abbrev flatMap_mkVector := @flatMap_replicate
 
 @[simp] theorem sum_replicate_nat {n : Nat} {a : Nat} : (replicate n a).sum = n * a := by
-  simp [toArray_replicate]
+  simp [sum, toArray_replicate]
 
 @[deprecated sum_replicate_nat (since := "2025-03-18")]
 abbrev sum_mkVector := @sum_replicate_nat
@@ -2233,10 +2239,6 @@ theorem reverse_empty : reverse (#v[] : Vector α 0) = #v[] := rfl
   cases as
   simp
 
-@[simp] theorem isEmpty_reverse {xs : Vector α n} : xs.reverse.isEmpty = xs.isEmpty := by
-  rcases xs with ⟨xs, rfl⟩
-  simp
-
 @[simp, grind] theorem getElem_reverse {xs : Vector α n} {i : Nat} (hi : i < n) :
     (xs.reverse)[i] = xs[n - 1 - i] := by
   rcases xs with ⟨xs, rfl⟩
@@ -2448,14 +2450,16 @@ theorem foldr_map {f : α₁ → α₂} {g : α₂ → β → β} {xs : Vector 
     (xs.map f).foldr g init = xs.foldr (fun x y => g (f x) y) init := by
   cases xs; simp [Array.foldr_map']
 
+@[deprecated "Deprecated without replacement; `filterMap` is not part of the `Vector` API." (since := "2025-05-09")]
 theorem foldl_filterMap {f : α → Option β} {g : γ → β → γ} {xs : Vector α n} {init : γ} :
-    (xs.filterMap f).foldl g init = xs.foldl (fun x y => match f y with | some b => g x b | none => x) init := by
+    (xs.toArray.filterMap f).foldl g init = xs.foldl (fun x y => match f y with | some b => g x b | none => x) init := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.foldl_filterMap']
   rfl
 
+@[deprecated "Deprecated without replacement; `filterMap` is not part of the `Vector` API." (since := "2025-05-09")]
 theorem foldr_filterMap {f : α → Option β} {g : β → γ → γ} {xs : Vector α n} {init : γ} :
-    (xs.filterMap f).foldr g init = xs.foldr (fun x y => match f x with | some b => g b y | none => y) init := by
+    (xs.toArray.filterMap f).foldr g init = xs.foldr (fun x y => match f x with | some b => g b y | none => y) init := by
   cases xs; simp [Array.foldr_filterMap']
   rfl
 
@@ -2555,12 +2559,12 @@ theorem foldr_rel {xs : Vector α n} {f g : α → β → β} {a b : β} {r : β
   simpa using Array.foldr_rel h (by simpa using h')
 
 @[simp] theorem foldl_add_const {xs : Vector α n} {a b : Nat} :
-    xs.foldl (fun x _ => x + a) b = b + a * xs.size := by
+    xs.foldl (fun x _ => x + a) b = b + a * n := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
 @[simp] theorem foldr_add_const {xs : Vector α n} {a b : Nat} :
-    xs.foldr (fun _ x => x + a) b = b + a * xs.size := by
+    xs.foldr (fun _ x => x + a) b = b + a * n := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
@@ -2697,15 +2701,15 @@ theorem contains_map [BEq β] {xs : Vector α n} {x : β} {f : α → β} :
   rcases xs with ⟨xs⟩
   simp
 
-@[simp, grind]
+@[deprecated "Deprecated without replacement; `filter` is not part of the `Vector` API." (since := "2025-05-09")]
 theorem contains_filter [BEq α] {xs : Vector α n} {x : α} {p : α → Bool} :
-    (xs.filter p).contains x = xs.any (fun a => x == a && p a) := by
+    (xs.toArray.filter p).contains x = xs.any (fun a => x == a && p a) := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp, grind]
+@[deprecated "Deprecated without replacement; `filterMap` is not part of the `Vector` API." (since := "2025-05-09")]
 theorem contains_filterMap [BEq β] {xs : Vector α n} {x : β} {f : α → Option β} :
-    (xs.filterMap f).contains x = xs.any (fun a => (f a).any fun b => x == b) := by
+    (xs.toArray.filterMap f).contains x = xs.any (fun a => (f a).any fun b => x == b) := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
@@ -2835,24 +2839,28 @@ theorem any_eq_not_all_not {xs : Vector α n} {p : α → Bool} : xs.any p = !xs
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp] theorem any_filter {xs : Vector α n} {p q : α → Bool} :
-    (xs.filter p).any q = xs.any fun a => p a && q a := by
+@[deprecated "Deprecated without replacement; `filter` is not part of the `Vector` API." (since := "2025-05-09")]
+theorem any_filter {xs : Vector α n} {p q : α → Bool} :
+    (xs.toArray.filter p).any q = xs.any fun a => p a && q a := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp] theorem all_filter {xs : Vector α n} {p q : α → Bool} :
-    (xs.filter p).all q = xs.all fun a => !(p a) || q a := by
+@[deprecated "Deprecated without replacement; `filter` is not part of the `Vector` API." (since := "2025-05-09")]
+theorem all_filter {xs : Vector α n} {p q : α → Bool} :
+    (xs.toArray.filter p).all q = xs.all fun a => !(p a) || q a := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp] theorem any_filterMap {xs : Vector α n} {f : α → Option β} {p : β → Bool} :
-    (xs.filterMap f).any p = xs.any fun a => match f a with | some b => p b | none => false := by
+@[deprecated "Deprecated without replacement; `filterMap` is not part of the `Vector` API." (since := "2025-05-09")]
+theorem any_filterMap {xs : Vector α n} {f : α → Option β} {p : β → Bool} :
+    (xs.toArray.filterMap f).any p = xs.any fun a => match f a with | some b => p b | none => false := by
   rcases xs with ⟨xs, rfl⟩
   simp
   rfl
 
-@[simp] theorem all_filterMap {xs : Vector α n} {f : α → Option β} {p : β → Bool} :
-    (xs.filterMap f).all p = xs.all fun a => match f a with | some b => p b | none => true := by
+@[deprecated "Deprecated without replacement; `filterMap` is not part of the `Vector` API." (since := "2025-05-09")]
+theorem all_filterMap {xs : Vector α n} {f : α → Option β} {p : β → Bool} :
+    (xs.toArray.filterMap f).all p = xs.all fun a => match f a with | some b => p b | none => true := by
   rcases xs with ⟨xs, rfl⟩
   simp
   rfl
@@ -3051,7 +3059,7 @@ set_option linter.indexVariables false in
   ext i
   by_cases h : i < n
   · simp [h]
-  · replace h : i = xs.size - 1 := by rw [size_toArray]; omega
+  · replace h : i = n := by omega
     subst h
     simp [back]
 
diff --git a/src/Init/Data/Vector/MapIdx.lean b/src/Init/Data/Vector/MapIdx.lean
index 69618323ed..54640cef11 100644
--- a/src/Init/Data/Vector/MapIdx.lean
+++ b/src/Init/Data/Vector/MapIdx.lean
@@ -134,7 +134,7 @@ theorem mapFinIdx_append {xs : Vector α n} {ys : Vector α m} {f : (i : Nat) 
 @[simp]
 theorem mapFinIdx_push {xs : Vector α n} {a : α} {f : (i : Nat) → α → (h : i < n + 1) → β} :
     mapFinIdx (xs.push a) f =
-      (mapFinIdx xs (fun i a h => f i a (by omega))).push (f xs.size a (by simp)) := by
+      (mapFinIdx xs (fun i a h => f i a (by omega))).push (f n a (by simp)) := by
   simp [← append_singleton, mapFinIdx_append]
 
 theorem mapFinIdx_singleton {a : α} {f : (i : Nat) → α → (h : i < 1) → β} :
@@ -255,14 +255,14 @@ theorem mapIdx_eq_zipIdx_map {xs : Vector α n} {f : Nat → α → β} :
 abbrev mapIdx_eq_zipWithIndex_map := @mapIdx_eq_zipIdx_map
 
 theorem mapIdx_append {xs : Vector α n} {ys : Vector α m} :
-    (xs ++ ys).mapIdx f = xs.mapIdx f ++ ys.mapIdx fun i => f (i + xs.size) := by
+    (xs ++ ys).mapIdx f = xs.mapIdx f ++ ys.mapIdx fun i => f (i + n) := by
   rcases xs with ⟨xs, rfl⟩
   rcases ys with ⟨ys, rfl⟩
   simp [Array.mapIdx_append]
 
 @[simp]
 theorem mapIdx_push {xs : Vector α n} {a : α} :
-    mapIdx f (xs.push a) = (mapIdx f xs).push (f xs.size a) := by
+    mapIdx f (xs.push a) = (mapIdx f xs).push (f n a) := by
   simp [← append_singleton, mapIdx_append]
 
 theorem mapIdx_singleton {a : α} : mapIdx f #v[a] = #v[f 0 a] := by
@@ -284,7 +284,7 @@ theorem exists_of_mem_mapIdx {b : β} {xs : Vector α n}
 
 theorem mapIdx_eq_push_iff {xs : Vector α (n + 1)} {b : β} :
     mapIdx f xs = ys.push b ↔
-      ∃ (a : α) (zs : Vector α n), xs = zs.push a ∧ mapIdx f zs = ys ∧ f zs.size a = b := by
+      ∃ (a : α) (zs : Vector α n), xs = zs.push a ∧ mapIdx f zs = ys ∧ f n a = b := by
   rw [mapIdx_eq_mapFinIdx, mapFinIdx_eq_push_iff]
   simp only [mapFinIdx_eq_mapIdx, exists_and_left, exists_prop]
   constructor
@@ -302,7 +302,7 @@ theorem mapIdx_eq_append_iff {xs : Vector α (n + m)} {f : Nat → α → β} {y
     mapIdx f xs = ys ++ zs ↔
       ∃ (ys' : Vector α n) (zs' : Vector α m), xs = ys' ++ zs' ∧
         ys'.mapIdx f = ys ∧
-        zs'.mapIdx (fun i => f (i + ys'.size)) = zs := by
+        zs'.mapIdx (fun i => f (i + n)) = zs := by
   rcases xs with ⟨xs, h⟩
   rcases ys with ⟨ys, rfl⟩
   rcases zs with ⟨zs, rfl⟩
@@ -342,12 +342,12 @@ theorem mapIdx_eq_mapIdx_iff {xs : Vector α n} :
   simp
 
 @[simp] theorem back?_mapIdx {xs : Vector α n} {f : Nat → α → β} :
-    (mapIdx f xs).back? = (xs.back?).map (f (xs.size - 1)) := by
+    (mapIdx f xs).back? = (xs.back?).map (f (n - 1)) := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
 @[simp] theorem back_mapIdx [NeZero n] {xs : Vector α n} {f : Nat → α → β} :
-    (mapIdx f xs).back = f (xs.size - 1) (xs.back) := by
+    (mapIdx f xs).back = f (n - 1) (xs.back) := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
@@ -364,7 +364,7 @@ theorem mapIdx_eq_replicate_iff {xs : Vector α n} {f : Nat → α → β} {b :
 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
+    xs.reverse.mapIdx f = (mapIdx (fun i => f (n - 1 - i)) xs).reverse := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.mapIdx_reverse]
 
diff --git a/src/Init/Data/Vector/Monadic.lean b/src/Init/Data/Vector/Monadic.lean
index f95042d116..9805a7b4df 100644
--- a/src/Init/Data/Vector/Monadic.lean
+++ b/src/Init/Data/Vector/Monadic.lean
@@ -70,32 +70,6 @@ theorem foldrM_map [Monad m] [LawfulMonad m] {f : β₁ → β₂} {g : β₂ 
   rcases xs with ⟨xs, rfl⟩
   simp [Array.foldrM_map]
 
-theorem foldlM_filterMap [Monad m] [LawfulMonad m] {f : α → Option β} {g : γ → β → m γ} {xs : Vector α n} {init : γ} :
-    (xs.filterMap f).foldlM g init =
-      xs.foldlM (fun x y => match f y with | some b => g x b | none => pure x) init := by
-  rcases xs with ⟨xs, rfl⟩
-  simp [Array.foldlM_filterMap]
-  rfl
-
-theorem foldrM_filterMap [Monad m] [LawfulMonad m] {f : α → Option β} {g : β → γ → m γ} {xs : Vector α n} {init : γ} :
-    (xs.filterMap f).foldrM g init =
-      xs.foldrM (fun x y => match f x with | some b => g b y | none => pure y) init := by
-  rcases xs with ⟨xs, rfl⟩
-  simp [Array.foldrM_filterMap]
-  rfl
-
-theorem foldlM_filter [Monad m] [LawfulMonad m] {p : α → Bool} {g : β → α → m β} {xs : Vector α n} {init : β} :
-    (xs.filter p).foldlM g init =
-      xs.foldlM (fun x y => if p y then g x y else pure x) init := by
-  rcases xs with ⟨xs, rfl⟩
-  simp [Array.foldlM_filter]
-
-theorem foldrM_filter [Monad m] [LawfulMonad m] {p : α → Bool} {g : α → β → m β} {xs : Vector α n} {init : β} :
-    (xs.filter p).foldrM g init =
-      xs.foldrM (fun x y => if p x then g x y else pure y) init := by
-  rcases xs with ⟨xs, rfl⟩
-  simp [Array.foldrM_filter]
-
 @[simp] theorem foldlM_attachWith [Monad m]
     {xs : Vector α n} {q : α → Prop} (H : ∀ a, a ∈ xs → q a) {f : β → { x // q x} → m β} {b} :
     (xs.attachWith q H).foldlM f b = xs.attach.foldlM (fun b ⟨a, h⟩ => f b ⟨a, H _ h⟩) b := by
diff --git a/src/Init/Data/Vector/Range.lean b/src/Init/Data/Vector/Range.lean
index 4bcb49e884..14dea9bc37 100644
--- a/src/Init/Data/Vector/Range.lean
+++ b/src/Init/Data/Vector/Range.lean
@@ -140,7 +140,7 @@ theorem range_add {n m : Nat} : range (n + m) = range n ++ (range m).map (n + ·
   simpa [range_eq_range', Nat.add_comm] using (range'_append_1 (s := 0)).symm
 
 theorem reverse_range' {s n : Nat} : reverse (range' s n) = map (s + n - 1 - ·) (range n) := by
-  simp [← toList_inj, List.reverse_range']
+  simp [← toArray_inj, Array.reverse_range']
 
 @[simp]
 theorem mem_range {m n : Nat} : m ∈ range n ↔ m < n := by
diff --git a/src/Init/Data/Vector/Zip.lean b/src/Init/Data/Vector/Zip.lean
index 023478bd87..6c54433105 100644
--- a/src/Init/Data/Vector/Zip.lean
+++ b/src/Init/Data/Vector/Zip.lean
@@ -243,7 +243,7 @@ theorem map_prod_right_eq_zip {xs : Vector α n} {f : α → β} :
 
 theorem zip_eq_append_iff {as : Vector α (n + m)} {bs : Vector β (n + m)} {xs : Vector (α × β) n} {ys : Vector (α × β) m} :
     zip as bs = xs ++ ys ↔
-      ∃ as₁ as₂ bs₁ bs₂, as₁.size = bs₁.size ∧ as = as₁ ++ as₂ ∧ bs = bs₁ ++ bs₂ ∧ xs = zip as₁ bs₁ ∧ ys = zip as₂ bs₂ := by
+      ∃ as₁ as₂ bs₁ bs₂, 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_replicate {a : α} {b : β} {n : Nat} :