diff --git a/src/Init/Data/Array/Attach.lean b/src/Init/Data/Array/Attach.lean
index 3e87b0aeec..36ffd5fe7c 100644
--- a/src/Init/Data/Array/Attach.lean
+++ b/src/Init/Data/Array/Attach.lean
@@ -6,6 +6,7 @@ Authors: Joachim Breitner, Mario Carneiro
 prelude
 import Init.Data.Array.Mem
 import Init.Data.Array.Lemmas
+import Init.Data.Array.Count
 import Init.Data.List.Attach
 
 namespace Array
@@ -142,10 +143,16 @@ theorem pmap_eq_map_attach {p : α → Prop} (f : ∀ a, p a → β) (l H) :
   cases l
   simp [List.pmap_eq_map_attach]
 
+@[simp]
+theorem pmap_eq_attachWith {p q : α → Prop} (f : ∀ a, p a → q a) (l H) :
+    pmap (fun a h => ⟨a, f a h⟩) l H = l.attachWith q (fun x h => f x (H x h)) := by
+  cases l
+  simp [List.pmap_eq_attachWith]
+
 theorem attach_map_coe (l : Array α) (f : α → β) :
     (l.attach.map fun (i : {i // i ∈ l}) => f i) = l.map f := by
   cases l
-  simp [List.attach_map_coe]
+  simp
 
 theorem attach_map_val (l : Array α) (f : α → β) : (l.attach.map fun i => f i.val) = l.map f :=
   attach_map_coe _ _
@@ -172,6 +179,12 @@ theorem mem_attach (l : Array α) : ∀ x, x ∈ l.attach
     rcases this with ⟨⟨_, _⟩, m, rfl⟩
     exact m
 
+@[simp]
+theorem mem_attachWith (l : Array α) {q : α → Prop} (H) (x : {x // q x}) :
+    x ∈ l.attachWith q H ↔ x.1 ∈ l := by
+  cases l
+  simp
+
 @[simp]
 theorem mem_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H b} :
     b ∈ pmap f l H ↔ ∃ (a : _) (h : a ∈ l), f a (H a h) = b := by
@@ -223,16 +236,16 @@ theorem attachWith_ne_empty_iff {l : Array α} {P : α → Prop} {H : ∀ a ∈
   cases l; simp
 
 @[simp]
-theorem getElem?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : Array α} (h : ∀ a ∈ l, p a) (n : Nat) :
-    (pmap f l h)[n]? = Option.pmap f l[n]? fun x H => h x (mem_of_getElem? H) := by
+theorem getElem?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : Array α} (h : ∀ a ∈ l, p a) (i : Nat) :
+    (pmap f l h)[i]? = Option.pmap f l[i]? fun x H => h x (mem_of_getElem? H) := by
   cases l; simp
 
 @[simp]
-theorem getElem_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : Array α} (h : ∀ a ∈ l, p a) {n : Nat}
-    (hn : n < (pmap f l h).size) :
-    (pmap f l h)[n] =
-      f (l[n]'(@size_pmap _ _ p f l h ▸ hn))
-        (h _ (getElem_mem (@size_pmap _ _ p f l h ▸ hn))) := by
+theorem getElem_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : Array α} (h : ∀ a ∈ l, p a) {i : Nat}
+    (hi : i < (pmap f l h).size) :
+    (pmap f l h)[i] =
+      f (l[i]'(@size_pmap _ _ p f l h ▸ hi))
+        (h _ (getElem_mem (@size_pmap _ _ p f l h ▸ hi))) := by
   cases l; simp
 
 @[simp]
@@ -256,6 +269,18 @@ theorem getElem_attach {xs : Array α} {i : Nat} (h : i < xs.attach.size) :
     xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem (by simpa using h)⟩ :=
   getElem_attachWith h
 
+@[simp] theorem pmap_attach (l : Array α) {p : {x // x ∈ l} → Prop} (f : ∀ a, p a → β) (H) :
+    pmap f l.attach H =
+      l.pmap (P := fun a => ∃ h : a ∈ l, p ⟨a, h⟩)
+        (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨h, H ⟨a, h⟩ (by simp)⟩) := by
+  ext <;> simp
+
+@[simp] theorem pmap_attachWith (l : Array α) {p : {x // q x} → Prop} (f : ∀ a, p a → β) (H₁ H₂) :
+    pmap f (l.attachWith q H₁) H₂ =
+      l.pmap (P := fun a => ∃ h : q a, p ⟨a, h⟩)
+        (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨H₁ _ h, H₂ ⟨a, H₁ _ h⟩ (by simpa)⟩) := by
+  ext <;> simp
+
 theorem foldl_pmap (l : Array α) {P : α → Prop} (f : (a : α) → P a → β)
   (H : ∀ (a : α), a ∈ l → P a) (g : γ → β → γ) (x : γ) :
     (l.pmap f H).foldl g x = l.attach.foldl (fun acc a => g acc (f a.1 (H _ a.2))) x := by
@@ -313,11 +338,7 @@ theorem attachWith_map {l : Array α} (f : α → β) {P : β → Prop} {H : ∀
     (l.map f).attachWith P H = (l.attachWith (P ∘ f) (fun _ h => H _ (mem_map_of_mem f h))).map
       fun ⟨x, h⟩ => ⟨f x, h⟩ := by
   cases l
-  ext
-  · simp
-  · simp only [List.map_toArray, List.attachWith_toArray, List.getElem_toArray,
-      List.getElem_attachWith, List.getElem_map, Function.comp_apply]
-    erw [List.getElem_attachWith] -- Why is `erw` needed here?
+  simp [List.attachWith_map]
 
 theorem map_attachWith {l : Array α} {P : α → Prop} {H : ∀ (a : α), a ∈ l → P a}
     (f : { x // P x } → β) :
@@ -347,7 +368,23 @@ theorem attach_filter {l : Array α} (p : α → Bool) :
   simp [List.attach_filter, List.map_filterMap, Function.comp_def]
 
 -- We are still missing here `attachWith_filterMap` and `attachWith_filter`.
--- Also missing are `filterMap_attach`, `filter_attach`, `filterMap_attachWith` and `filter_attachWith`.
+
+@[simp]
+theorem filterMap_attachWith {q : α → Prop} {l : Array α} {f : {x // q x} → Option β} (H)
+    (w : stop = (l.attachWith q H).size) :
+    (l.attachWith q H).filterMap f 0 stop = l.attach.filterMap (fun ⟨x, h⟩ => f ⟨x, H _ h⟩) := by
+  subst w
+  cases l
+  simp [Function.comp_def]
+
+@[simp]
+theorem filter_attachWith {q : α → Prop} {l : Array α} {p : {x // q x} → Bool} (H)
+    (w : stop = (l.attachWith q H).size) :
+    (l.attachWith q H).filter p 0 stop =
+      (l.attach.filter (fun ⟨x, h⟩ => p ⟨x, H _ h⟩)).map (fun ⟨x, h⟩ => ⟨x, H _ h⟩) := by
+  subst w
+  cases l
+  simp [Function.comp_def, List.filter_map]
 
 theorem pmap_pmap {p : α → Prop} {q : β → Prop} (g : ∀ a, p a → β) (f : ∀ b, q b → γ) (l H₁ H₂) :
     pmap f (pmap g l H₁) H₂ =
@@ -427,16 +464,48 @@ theorem reverse_attach (xs : Array α) :
 
 @[simp] theorem back?_attachWith {P : α → Prop} {xs : Array α}
     {H : ∀ (a : α), a ∈ xs → P a} :
-    (xs.attachWith P H).back? = xs.back?.pbind (fun a h => some ⟨a, H _ (mem_of_back?_eq_some h)⟩) := by
+    (xs.attachWith P H).back? = xs.back?.pbind (fun a h => some ⟨a, H _ (mem_of_back? h)⟩) := by
   cases xs
   simp
 
 @[simp]
 theorem back?_attach {xs : Array α} :
-    xs.attach.back? = xs.back?.pbind fun a h => some ⟨a, mem_of_back?_eq_some h⟩ := by
+    xs.attach.back? = xs.back?.pbind fun a h => some ⟨a, mem_of_back? h⟩ := by
   cases xs
   simp
 
+@[simp]
+theorem countP_attach (l : Array α) (p : α → Bool) :
+    l.attach.countP (fun a : {x // x ∈ l} => p a) = l.countP p := by
+  cases l
+  simp [Function.comp_def]
+
+@[simp]
+theorem countP_attachWith {p : α → Prop} (l : Array α) (H : ∀ a ∈ l, p a) (q : α → Bool) :
+    (l.attachWith p H).countP (fun a : {x // p x} => q a) = l.countP q := by
+  cases l
+  simp
+
+@[simp]
+theorem count_attach [DecidableEq α] (l : Array α) (a : {x // x ∈ l}) :
+    l.attach.count a = l.count ↑a := by
+  rcases l with ⟨l⟩
+  simp only [List.attach_toArray, List.attachWith_mem_toArray, List.count_toArray]
+  rw [List.map_attach, List.count_eq_countP]
+  simp only [Subtype.beq_iff]
+  rw [List.countP_pmap, List.countP_attach (p := (fun x => x == a.1)), List.count]
+
+@[simp]
+theorem count_attachWith [DecidableEq α] {p : α → Prop} (l : Array α) (H : ∀ a ∈ l, p a) (a : {x // p x}) :
+    (l.attachWith p H).count a = l.count ↑a := by
+  cases l
+  simp
+
+@[simp] theorem countP_pmap {p : α → Prop} (g : ∀ a, p a → β) (f : β → Bool) (l : Array α) (H₁) :
+    (l.pmap g H₁).countP f =
+      l.attach.countP (fun ⟨a, m⟩ => f (g a (H₁ a m))) := by
+  simp [pmap_eq_map_attach, countP_map, Function.comp_def]
+
 /-! ## unattach
 
 `Array.unattach` is the (one-sided) inverse of `Array.attach`. It is a synonym for `Array.map Subtype.val`.
@@ -455,7 +524,7 @@ and is ideally subsequently simplified away by `unattach_attach`.
 
 If not, usually the right approach is `simp [Array.unattach, -Array.map_subtype]` to unfold.
 -/
-def unattach {α : Type _} {p : α → Prop} (l : Array { x // p x }) := l.map (·.val)
+def unattach {α : Type _} {p : α → Prop} (l : Array { x // p x }) : Array α := l.map (·.val)
 
 @[simp] theorem unattach_nil {p : α → Prop} : (#[] : Array { x // p x }).unattach = #[] := rfl
 @[simp] theorem unattach_push {p : α → Prop} {a : { x // p x }} {l : Array { x // p x }} :
@@ -578,4 +647,16 @@ and simplifies these to the function directly taking the value.
   cases l₂
   simp
 
+@[simp] theorem unattach_flatten {p : α → Prop} {l : Array (Array { x // p x })} :
+    l.flatten.unattach = (l.map unattach).flatten := by
+  unfold unattach
+  cases l using array₂_induction
+  simp only [flatten_toArray, List.map_map, Function.comp_def, List.map_id_fun', id_eq,
+    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 }} :
+    (Array.mkArray n x).unattach = Array.mkArray n x.1 := by
+  simp [unattach]
+
 end Array
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index b41356c671..0fece3ac67 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -3253,9 +3253,11 @@ theorem back!_eq_back? [Inhabited α] (a : Array α) : a.back! = a.back?.getD de
 @[simp] theorem back!_push [Inhabited α] (a : Array α) : (a.push x).back! = x := by
   simp [back!_eq_back?]
 
-theorem mem_of_back?_eq_some {xs : Array α} {a : α} (h : xs.back? = some a) : a ∈ xs := by
+theorem mem_of_back? {xs : Array α} {a : α} (h : xs.back? = some a) : a ∈ xs := by
   cases xs
-  simpa using List.mem_of_getLast?_eq_some (by simpa using h)
+  simpa using List.mem_of_getLast? (by simpa using h)
+
+@[deprecated mem_of_back? (since := "2024-10-21")] abbrev mem_of_back?_eq_some := @mem_of_back?
 
 theorem getElem?_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
     (a.push x)[i]? = some a[i] := by
diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean
index 2b9a494eff..a83d1976cb 100644
--- a/src/Init/Data/Bool.lean
+++ b/src/Init/Data/Bool.lean
@@ -620,3 +620,12 @@ but may be used locally.
 -/
 def boolRelToRel : Coe (α → α → Bool) (α → α → Prop) where
   coe r := fun a b => Eq (r a b) true
+
+/-! ### subtypes -/
+
+@[simp] theorem Subtype.beq_iff {α : Type u} [DecidableEq α] {p : α → Prop} {x y : {a : α // p a}} :
+    (x == y) = (x.1 == y.1) := by
+  cases x
+  cases y
+  rw [Bool.eq_iff_iff]
+  simp [beq_iff_eq]
diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean
index a13f7dfa6f..e54de34b65 100644
--- a/src/Init/Data/List/Attach.lean
+++ b/src/Init/Data/List/Attach.lean
@@ -111,6 +111,14 @@ theorem pmap_eq_map_attach {p : α → Prop} (f : ∀ a, p a → β) (l H) :
     pmap f l H = l.attach.map fun x => f x.1 (H _ x.2) := by
   rw [attach, attachWith, map_pmap]; exact pmap_congr_left l fun _ _ _ _ => rfl
 
+@[simp]
+theorem pmap_eq_attachWith {p q : α → Prop} (f : ∀ a, p a → q a) (l H) :
+    pmap (fun a h => ⟨a, f a h⟩) l H = l.attachWith q (fun x h => f x (H x h)) := by
+  induction l with
+  | nil => rfl
+  | cons a l ih =>
+    simp [pmap, attachWith, ih]
+
 theorem attach_map_coe (l : List α) (f : α → β) :
     (l.attach.map fun (i : {i // i ∈ l}) => f i) = l.map f := by
   rw [attach, attachWith, map_pmap]; exact pmap_eq_map _ _ _ _
@@ -136,10 +144,23 @@ theorem attachWith_map_subtype_val {p : α → Prop} (l : List α) (H : ∀ a 
 @[simp]
 theorem mem_attach (l : List α) : ∀ x, x ∈ l.attach
   | ⟨a, h⟩ => by
-    have := mem_map.1 (by rw [attach_map_subtype_val] <;> exact h)
+    have := mem_map.1 (by rw [attach_map_subtype_val]; exact h)
     rcases this with ⟨⟨_, _⟩, m, rfl⟩
     exact m
 
+@[simp]
+theorem mem_attachWith (l : List α) {q : α → Prop} (H) (x : {x // q x}) :
+    x ∈ l.attachWith q H ↔ x.1 ∈ l := by
+  induction l with
+  | nil => simp
+  | cons a l ih =>
+    simp [ih]
+    constructor
+    · rintro (_ | _) <;> simp_all
+    · rintro (h | h)
+      · simp [← h]
+      · simp_all
+
 @[simp]
 theorem mem_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H b} :
     b ∈ pmap f l H ↔ ∃ (a : _) (h : a ∈ l), f a (H a h) = b := by
@@ -266,6 +287,18 @@ theorem getElem_attach {xs : List α} {i : Nat} (h : i < xs.attach.length) :
     xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem (by simpa using h)⟩ :=
   getElem_attachWith h
 
+@[simp] theorem pmap_attach (l : List α) {p : {x // x ∈ l} → Prop} (f : ∀ a, p a → β) (H) :
+    pmap f l.attach H =
+      l.pmap (P := fun a => ∃ h : a ∈ l, p ⟨a, h⟩)
+        (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨h, H ⟨a, h⟩ (by simp)⟩) := by
+  apply ext_getElem <;> simp
+
+@[simp] theorem pmap_attachWith (l : List α) {p : {x // q x} → Prop} (f : ∀ a, p a → β) (H₁ H₂) :
+    pmap f (l.attachWith q H₁) H₂ =
+      l.pmap (P := fun a => ∃ h : q a, p ⟨a, h⟩)
+        (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨H₁ _ h, H₂ ⟨a, H₁ _ h⟩ (by simpa)⟩) := by
+  apply ext_getElem <;> simp
+
 @[simp] theorem head?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List α)
     (H : ∀ (a : α), a ∈ xs → P a) :
     (xs.pmap f H).head? = xs.attach.head?.map fun ⟨a, m⟩ => f a (H a m) := by
@@ -431,7 +464,25 @@ theorem attach_filter {l : List α} (p : α → Bool) :
   split <;> simp
 
 -- We are still missing here `attachWith_filterMap` and `attachWith_filter`.
--- Also missing are `filterMap_attach`, `filter_attach`, `filterMap_attachWith` and `filter_attachWith`.
+
+@[simp]
+theorem filterMap_attachWith {q : α → Prop} {l : List α} {f : {x // q x} → Option β} (H) :
+    (l.attachWith q H).filterMap f = l.attach.filterMap (fun ⟨x, h⟩ => f ⟨x, H _ h⟩) := by
+  induction l with
+  | nil => rfl
+  | cons x xs ih =>
+    simp only [attachWith_cons, filterMap_cons]
+    split <;> simp_all [Function.comp_def]
+
+@[simp]
+theorem filter_attachWith {q : α → Prop} {l : List α} {p : {x // q x} → Bool} (H) :
+    (l.attachWith q H).filter p =
+      (l.attach.filter (fun ⟨x, h⟩ => p ⟨x, H _ h⟩)).map (fun ⟨x, h⟩ => ⟨x, H _ h⟩) := by
+  induction l with
+  | nil => rfl
+  | cons x xs ih =>
+    simp only [attachWith_cons, filter_cons]
+    split <;> simp_all [Function.comp_def, filter_map]
 
 theorem pmap_pmap {p : α → Prop} {q : β → Prop} (g : ∀ a, p a → β) (f : ∀ b, q b → γ) (l H₁ H₂) :
     pmap f (pmap g l H₁) H₂ =
@@ -520,7 +571,7 @@ theorem reverse_attach (xs : List α) :
 
 @[simp] theorem getLast?_attachWith {P : α → Prop} {xs : List α}
     {H : ∀ (a : α), a ∈ xs → P a} :
-    (xs.attachWith P H).getLast? = xs.getLast?.pbind (fun a h => some ⟨a, H _ (mem_of_getLast?_eq_some h)⟩) := by
+    (xs.attachWith P H).getLast? = xs.getLast?.pbind (fun a h => some ⟨a, H _ (mem_of_getLast? h)⟩) := by
   rw [getLast?_eq_head?_reverse, reverse_attachWith, head?_attachWith]
   simp
 
@@ -531,7 +582,7 @@ theorem reverse_attach (xs : List α) :
 
 @[simp]
 theorem getLast?_attach {xs : List α} :
-    xs.attach.getLast? = xs.getLast?.pbind fun a h => some ⟨a, mem_of_getLast?_eq_some h⟩ := by
+    xs.attach.getLast? = xs.getLast?.pbind fun a h => some ⟨a, mem_of_getLast? h⟩ := by
   rw [getLast?_eq_head?_reverse, reverse_attach, head?_map, head?_attach]
   simp
 
@@ -560,6 +611,11 @@ theorem count_attachWith [DecidableEq α] {p : α → Prop} (l : List α) (H : 
     (l.attachWith p H).count a = l.count ↑a :=
   Eq.trans (countP_congr fun _ _ => by simp [Subtype.ext_iff]) <| countP_attachWith _ _ _
 
+@[simp] theorem countP_pmap {p : α → Prop} (g : ∀ a, p a → β) (f : β → Bool) (l : List α) (H₁) :
+    (l.pmap g H₁).countP f =
+      l.attach.countP (fun ⟨a, m⟩ => f (g a (H₁ a m))) := by
+  simp [pmap_eq_map_attach, countP_map, Function.comp_def]
+
 /-! ## unattach
 
 `List.unattach` is the (one-sided) inverse of `List.attach`. It is a synonym for `List.map Subtype.val`.
@@ -578,7 +634,7 @@ and is ideally subsequently simplified away by `unattach_attach`.
 
 If not, usually the right approach is `simp [List.unattach, -List.map_subtype]` to unfold.
 -/
-def unattach {α : Type _} {p : α → Prop} (l : List { x // p x }) := l.map (·.val)
+def unattach {α : Type _} {p : α → Prop} (l : List { x // p x }) : List α := l.map (·.val)
 
 @[simp] theorem unattach_nil {p : α → Prop} : ([] : List { x // p x }).unattach = [] := rfl
 @[simp] theorem unattach_cons {p : α → Prop} {a : { x // p x }} {l : List { x // p x }} :
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index da932cb5ca..a07da6dfcc 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -2750,10 +2750,12 @@ theorem getLast?_eq_some_iff {xs : List α} {a : α} : xs.getLast? = some a ↔
   rw [getLast?_eq_head?_reverse, head?_isSome]
   simp
 
-theorem mem_of_getLast?_eq_some {xs : List α} {a : α} (h : xs.getLast? = some a) : a ∈ xs := by
+theorem mem_of_getLast? {xs : List α} {a : α} (h : xs.getLast? = some a) : a ∈ xs := by
   obtain ⟨ys, rfl⟩ := getLast?_eq_some_iff.1 h
   exact mem_concat_self ys a
 
+@[deprecated mem_of_getLast? (since := "2024-10-21")] abbrev mem_of_getLast?_eq_some := @mem_of_getLast?
+
 @[simp] theorem getLast_reverse {l : List α} (h : l.reverse ≠ []) :
     l.reverse.getLast h = l.head (by simp_all) := by
   simp [getLast_eq_head_reverse]
diff --git a/src/Init/Data/Subtype.lean b/src/Init/Data/Subtype.lean
index d8be8da53a..5102dc9348 100644
--- a/src/Init/Data/Subtype.lean
+++ b/src/Init/Data/Subtype.lean
@@ -5,6 +5,7 @@ Authors: Johannes Hölzl
 -/
 prelude
 import Init.Ext
+import Init.Core
 
 namespace Subtype
 
diff --git a/src/Init/Data/Vector/Attach.lean b/src/Init/Data/Vector/Attach.lean
new file mode 100644
index 0000000000..ce77d9e164
--- /dev/null
+++ b/src/Init/Data/Vector/Attach.lean
@@ -0,0 +1,551 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.Vector.Lemmas
+import Init.Data.Array.Attach
+
+namespace Vector
+
+/--
+`O(n)`. Partial map. If `f : Π a, P a → β` is a partial function defined on
+`a : α` satisfying `P`, then `pmap f l h` is essentially the same as `map f l`
+but is defined only when all members of `l` satisfy `P`, using the proof
+to apply `f`.
+
+We replace this at runtime with a more efficient version via the `csimp` lemma `pmap_eq_pmapImpl`.
+-/
+def pmap {P : α → Prop} (f : ∀ a, P a → β) (l : Vector α n) (H : ∀ a ∈ l, P a) : Vector β n :=
+  Vector.mk (l.toArray.pmap f (fun a m => H a (by simpa using m))) (by simp)
+
+/--
+Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of
+`Vector {x // P x} n` is the same as the input `Vector α n`.
+-/
+@[inline] private unsafe def attachWithImpl
+    (xs : Vector α n) (P : α → Prop) (_ : ∀ x ∈ xs, P x) : Vector {x // P x} n := unsafeCast xs
+
+/-- `O(1)`. "Attach" a proof `P x` that holds for all the elements of `xs` to produce a new array
+  with the same elements but in the type `{x // P x}`. -/
+@[implemented_by attachWithImpl] def attachWith
+    (xs : Vector α n) (P : α → Prop) (H : ∀ x ∈ xs, P x) : Vector {x // P x} n :=
+  Vector.mk (xs.toArray.attachWith P fun x h => H x (by simpa using h)) (by simp)
+
+/-- `O(1)`. "Attach" the proof that the elements of `xs` are in `xs` to produce a new vector
+  with the same elements but in the type `{x // x ∈ xs}`. -/
+@[inline] def attach (xs : Vector α n) : Vector {x // x ∈ xs} n := xs.attachWith _ fun _ => id
+
+@[simp] theorem attachWith_mk {xs : Array α} {h : xs.size = n} {P : α → Prop} {H : ∀ x ∈ mk xs h, P x} :
+    (mk xs h).attachWith P H = mk (xs.attachWith P (by simpa using H)) (by simpa using h) := by
+  simp [attachWith]
+
+@[simp] theorem attach_mk {xs : Array α} {h : xs.size = n} :
+    (mk xs h).attach = mk (xs.attachWith (· ∈ mk xs h) (by simp)) (by simpa using h):= by
+  simp [attach]
+
+@[simp] theorem pmap_mk {xs : Array α} {h : xs.size = n} {P : α → Prop} {f : ∀ a, P a → β}
+    {H : ∀ a ∈ mk xs h, P a} :
+    (mk xs h).pmap f H = mk (xs.pmap f (by simpa using H)) (by simpa using h) := by
+  simp [pmap]
+
+@[simp] theorem toArray_attachWith {l : Vector α n} {P : α → Prop} {H : ∀ x ∈ l, P x} :
+   (l.attachWith P H).toArray = l.toArray.attachWith P (by simpa using H) := by
+  simp [attachWith]
+
+@[simp] theorem toArray_attach {α : Type _} {l : Vector α n} :
+    l.attach.toArray = l.toArray.attachWith (· ∈ l) (by simp) := by
+  simp [attach]
+
+@[simp] theorem toArray_pmap {l : Vector α n} {P : α → Prop} {f : ∀ a, P a → β} {H : ∀ a ∈ l, P a} :
+    (l.pmap f H).toArray = l.toArray.pmap f (fun a m => H a (by simpa using m)) := by
+  simp [pmap]
+
+@[simp] theorem toList_attachWith {l : Vector α n} {P : α → Prop} {H : ∀ x ∈ l, P x} :
+   (l.attachWith P H).toList = l.toList.attachWith P (by simpa using H) := by
+  simp [attachWith]
+
+@[simp] theorem toList_attach {α : Type _} {l : Vector α n} :
+    l.attach.toList = l.toList.attachWith (· ∈ l) (by simp) := by
+  simp [attach]
+
+@[simp] theorem toList_pmap {l : Vector α n} {P : α → Prop} {f : ∀ a, P a → β} {H : ∀ a ∈ l, P a} :
+    (l.pmap f H).toList = l.toList.pmap f (fun a m => H a (by simpa using m)) := by
+  simp [pmap]
+
+/-- Implementation of `pmap` using the zero-copy version of `attach`. -/
+@[inline] private def pmapImpl {P : α → Prop} (f : ∀ a, P a → β) (l : Vector α n) (H : ∀ a ∈ l, P a) :
+    Vector β n := (l.attachWith _ H).map fun ⟨x, h'⟩ => f x h'
+
+@[csimp] private theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by
+  funext α β n p f L h'
+  rcases L with ⟨L, rfl⟩
+  simp only [pmap, pmapImpl, attachWith_mk, map_mk, Array.map_attachWith, eq_mk]
+  apply Array.pmap_congr_left
+  intro a m h₁ h₂
+  congr
+
+@[simp] theorem pmap_empty {P : α → Prop} (f : ∀ a, P a → β) : pmap f #v[] (by simp) = #v[] := rfl
+
+@[simp] theorem pmap_push {P : α → Prop} (f : ∀ a, P a → β) (a : α) (l : Vector α n) (h : ∀ b ∈ l.push a, P b) :
+    pmap f (l.push a) h =
+      (pmap f l (fun a m => by simp at h; exact h a (.inl m))).push (f a (h a (by simp))) := by
+  simp [pmap]
+
+@[simp] theorem attach_empty : (#v[] : Vector α 0).attach = #v[] := rfl
+
+@[simp] theorem attachWith_empty {P : α → Prop} (H : ∀ x ∈ #v[], P x) : (#v[] : Vector α 0).attachWith P H = #v[] := rfl
+
+@[simp]
+theorem pmap_eq_map (p : α → Prop) (f : α → β) (l : Vector α n) (H) :
+    @pmap _ _ _ p (fun a _ => f a) l H = map f l := by
+  cases l; simp
+
+theorem pmap_congr_left {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a, q a → β} (l : Vector α n) {H₁ H₂}
+    (h : ∀ a ∈ l, ∀ (h₁ h₂), f a h₁ = g a h₂) : pmap f l H₁ = pmap g l H₂ := by
+  rcases l with ⟨l, rfl⟩
+  simp only [pmap_mk, eq_mk]
+  apply Array.pmap_congr_left
+  simpa using h
+
+theorem map_pmap {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (l : Vector α n) (H) :
+    map g (pmap f l H) = pmap (fun a h => g (f a h)) l H := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.map_pmap]
+
+theorem pmap_map {p : β → Prop} (g : ∀ b, p b → γ) (f : α → β) (l : Vector α n) (H) :
+    pmap g (map f l) H = pmap (fun a h => g (f a) h) l fun _ h => H _ (mem_map_of_mem _ h) := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.pmap_map]
+
+theorem attach_congr {l₁ l₂ : Vector α n} (h : l₁ = l₂) :
+    l₁.attach = l₂.attach.map (fun x => ⟨x.1, h ▸ x.2⟩) := by
+  subst h
+  simp
+
+theorem attachWith_congr {l₁ l₂ : Vector α n} (w : l₁ = l₂) {P : α → Prop} {H : ∀ x ∈ l₁, P x} :
+    l₁.attachWith P H = l₂.attachWith P fun _ h => H _ (w ▸ h) := by
+  subst w
+  simp
+
+@[simp] theorem attach_push {a : α} {l : Vector α n} :
+    (l.push a).attach =
+      (l.attach.map (fun ⟨x, h⟩ => ⟨x, mem_push_of_mem a h⟩)).push ⟨a, by simp⟩ := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.map_attachWith]
+
+@[simp] theorem attachWith_push {a : α} {l : Vector α n} {P : α → Prop} {H : ∀ x ∈ l.push a, P x} :
+    (l.push a).attachWith P H =
+      (l.attachWith P (fun x h => by simp at H; exact H x (.inl h))).push ⟨a, H a (by simp)⟩ := by
+  rcases l with ⟨l, rfl⟩
+  simp
+
+theorem pmap_eq_map_attach {p : α → Prop} (f : ∀ a, p a → β) (l : Vector α n) (H) :
+    pmap f l H = l.attach.map fun x => f x.1 (H _ x.2) := by
+  rcases l with ⟨l, rfl⟩
+  simp only [pmap_mk, Array.pmap_eq_map_attach, attach_mk, map_mk, eq_mk]
+  rw [Array.map_attach, Array.map_attachWith]
+  ext i hi₁ hi₂ <;> simp
+
+@[simp]
+theorem pmap_eq_attachWith {p q : α → Prop} (f : ∀ a, p a → q a) (l : Vector α n) (H) :
+    pmap (fun a h => ⟨a, f a h⟩) l H = l.attachWith q (fun x h => f x (H x h)) := by
+  cases l
+  simp
+
+theorem attach_map_coe (l : Vector α n) (f : α → β) :
+    (l.attach.map fun (i : {i // i ∈ l}) => f i) = l.map f := by
+  cases l
+  simp
+
+theorem attach_map_val (l : Vector α n) (f : α → β) : (l.attach.map fun i => f i.val) = l.map f :=
+  attach_map_coe _ _
+
+theorem attach_map_subtype_val (l : Vector α n) : l.attach.map Subtype.val = l := by
+  cases l; simp
+
+theorem attachWith_map_coe {p : α → Prop} (f : α → β) (l : Vector α n) (H : ∀ a ∈ l, p a) :
+    ((l.attachWith p H).map fun (i : { i // p i}) => f i) = l.map f := by
+  cases l; simp
+
+theorem attachWith_map_val {p : α → Prop} (f : α → β) (l : Vector α n) (H : ∀ a ∈ l, p a) :
+    ((l.attachWith p H).map fun i => f i.val) = l.map f :=
+  attachWith_map_coe _ _ _
+
+theorem attachWith_map_subtype_val {p : α → Prop} (l : Vector α n) (H : ∀ a ∈ l, p a) :
+    (l.attachWith p H).map Subtype.val = l := by
+  cases l; simp
+
+@[simp]
+theorem mem_attach (l : Vector α n) : ∀ x, x ∈ l.attach
+  | ⟨a, h⟩ => by
+    have := mem_map.1 (by rw [attach_map_subtype_val] <;> exact h)
+    rcases this with ⟨⟨_, _⟩, m, rfl⟩
+    exact m
+
+@[simp]
+theorem mem_attachWith (l : Vector α n) {q : α → Prop} (H) (x : {x // q x}) :
+    x ∈ l.attachWith q H ↔ x.1 ∈ l := by
+  rcases l with ⟨l, rfl⟩
+  simp
+
+@[simp]
+theorem mem_pmap {p : α → Prop} {f : ∀ a, p a → β} {l : Vector α n} {H b} :
+    b ∈ pmap f l H ↔ ∃ (a : _) (h : a ∈ l), f a (H a h) = b := by
+  simp only [pmap_eq_map_attach, mem_map, mem_attach, true_and, Subtype.exists, eq_comm]
+
+theorem mem_pmap_of_mem {p : α → Prop} {f : ∀ a, p a → β} {l : Vector α n} {H} {a} (h : a ∈ l) :
+    f a (H a h) ∈ pmap f l H := by
+  rw [mem_pmap]
+  exact ⟨a, h, rfl⟩
+
+theorem pmap_eq_self {l : Vector α n} {p : α → Prop} {hp : ∀ (a : α), a ∈ l → p a}
+    {f : (a : α) → p a → α} : l.pmap f hp = l ↔ ∀ a (h : a ∈ l), f a (hp a h) = a := by
+  cases l; simp [Array.pmap_eq_self]
+
+@[simp]
+theorem getElem?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : Vector α n} (h : ∀ a ∈ l, p a) (i : Nat) :
+    (pmap f l h)[i]? = Option.pmap f l[i]? fun x H => h x (mem_of_getElem? H) := by
+  cases l; simp
+
+@[simp]
+theorem getElem_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : Vector α n} (h : ∀ a ∈ l, p a) {i : Nat}
+    (hn : i < n) :
+    (pmap f l h)[i] = f (l[i]) (h _ (by simp)) := by
+  cases l; simp
+
+@[simp]
+theorem getElem?_attachWith {xs : Vector α n} {i : Nat} {P : α → Prop} {H : ∀ a ∈ xs, P a} :
+    (xs.attachWith P H)[i]? = xs[i]?.pmap Subtype.mk (fun _ a => H _ (mem_of_getElem? a)) :=
+  getElem?_pmap ..
+
+@[simp]
+theorem getElem?_attach {xs : Vector α n} {i : Nat} :
+    xs.attach[i]? = xs[i]?.pmap Subtype.mk (fun _ a => mem_of_getElem? a) :=
+  getElem?_attachWith
+
+@[simp]
+theorem getElem_attachWith {xs : Vector α n} {P : α → Prop} {H : ∀ a ∈ xs, P a}
+    {i : Nat} (h : i < n) :
+    (xs.attachWith P H)[i] = ⟨xs[i]'(by simpa using h), H _ (getElem_mem (by simpa using h))⟩ :=
+  getElem_pmap _ _ h
+
+@[simp]
+theorem getElem_attach {xs : Vector α n} {i : Nat} (h : i < n) :
+    xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem (by simpa using h)⟩ :=
+  getElem_attachWith h
+
+@[simp] theorem pmap_attach (l : Vector α n) {p : {x // x ∈ l} → Prop} (f : ∀ a, p a → β) (H) :
+    pmap f l.attach H =
+      l.pmap (P := fun a => ∃ h : a ∈ l, p ⟨a, h⟩)
+        (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨h, H ⟨a, h⟩ (by simp)⟩) := by
+  ext <;> simp
+
+@[simp] theorem pmap_attachWith (l : Vector α n) {p : {x // q x} → Prop} (f : ∀ a, p a → β) (H₁ H₂) :
+    pmap f (l.attachWith q H₁) H₂ =
+      l.pmap (P := fun a => ∃ h : q a, p ⟨a, h⟩)
+        (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨H₁ _ h, H₂ ⟨a, H₁ _ h⟩ (by simpa)⟩) := by
+  ext <;> simp
+
+theorem foldl_pmap (l : Vector α n) {P : α → Prop} (f : (a : α) → P a → β)
+  (H : ∀ (a : α), a ∈ l → P a) (g : γ → β → γ) (x : γ) :
+    (l.pmap f H).foldl g x = l.attach.foldl (fun acc a => g acc (f a.1 (H _ a.2))) x := by
+  rw [pmap_eq_map_attach, foldl_map]
+
+theorem foldr_pmap (l : Vector α n) {P : α → Prop} (f : (a : α) → P a → β)
+  (H : ∀ (a : α), a ∈ l → P a) (g : β → γ → γ) (x : γ) :
+    (l.pmap f H).foldr g x = l.attach.foldr (fun a acc => g (f a.1 (H _ a.2)) acc) x := by
+  rw [pmap_eq_map_attach, foldr_map]
+
+/--
+If we fold over `l.attach` with a function that ignores the membership predicate,
+we get the same results as folding over `l` directly.
+
+This is useful when we need to use `attach` to show termination.
+
+Unfortunately this can't be applied by `simp` because of the higher order unification problem,
+and even when rewriting we need to specify the function explicitly.
+See however `foldl_subtype` below.
+-/
+theorem foldl_attach (l : Vector α n) (f : β → α → β) (b : β) :
+    l.attach.foldl (fun acc t => f acc t.1) b = l.foldl f b := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.foldl_attach]
+
+/--
+If we fold over `l.attach` with a function that ignores the membership predicate,
+we get the same results as folding over `l` directly.
+
+This is useful when we need to use `attach` to show termination.
+
+Unfortunately this can't be applied by `simp` because of the higher order unification problem,
+and even when rewriting we need to specify the function explicitly.
+See however `foldr_subtype` below.
+-/
+theorem foldr_attach (l : Vector α n) (f : α → β → β) (b : β) :
+    l.attach.foldr (fun t acc => f t.1 acc) b = l.foldr f b := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.foldr_attach]
+
+theorem attach_map {l : Vector α n} (f : α → β) :
+    (l.map f).attach = l.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem f h⟩) := by
+  cases l
+  ext <;> simp
+
+theorem attachWith_map {l : Vector α n} (f : α → β) {P : β → Prop} {H : ∀ (b : β), b ∈ l.map f → P b} :
+    (l.map f).attachWith P H = (l.attachWith (P ∘ f) (fun _ h => H _ (mem_map_of_mem f h))).map
+      fun ⟨x, h⟩ => ⟨f x, h⟩ := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.attachWith_map]
+
+theorem map_attachWith {l : Vector α n} {P : α → Prop} {H : ∀ (a : α), a ∈ l → P a}
+    (f : { x // P x } → β) :
+    (l.attachWith P H).map f =
+      l.pmap (fun a (h : a ∈ l ∧ P a) => f ⟨a, H _ h.1⟩) (fun a h => ⟨h, H a h⟩) := by
+  cases l
+  ext <;> simp
+
+/-- See also `pmap_eq_map_attach` for writing `pmap` in terms of `map` and `attach`. -/
+theorem map_attach {l : Vector α n} (f : { x // x ∈ l } → β) :
+    l.attach.map f = l.pmap (fun a h => f ⟨a, h⟩) (fun _ => id) := by
+  cases l
+  ext <;> simp
+
+theorem pmap_pmap {p : α → Prop} {q : β → Prop} (g : ∀ a, p a → β) (f : ∀ b, q b → γ) (l : Vector α n) (H₁ H₂) :
+    pmap f (pmap g l H₁) H₂ =
+      pmap (α := { x // x ∈ l }) (fun a h => f (g a h) (H₂ (g a h) (mem_pmap_of_mem a.2))) l.attach
+        (fun a _ => H₁ a a.2) := by
+  rcases l with ⟨l, rfl⟩
+  ext <;> simp
+
+@[simp] theorem pmap_append {p : ι → Prop} (f : ∀ a : ι, p a → α) (l₁ : Vector ι n) (l₂ : Vector ι m)
+    (h : ∀ a ∈ l₁ ++ l₂, p a) :
+    (l₁ ++ l₂).pmap f h =
+      (l₁.pmap f fun a ha => h a (mem_append_left l₂ ha)) ++
+        l₂.pmap f fun a ha => h a (mem_append_right l₁ ha) := by
+  cases l₁
+  cases l₂
+  simp
+
+theorem pmap_append' {p : α → Prop} (f : ∀ a : α, p a → β) (l₁ : Vector α n) (l₂ : Vector α m)
+    (h₁ : ∀ a ∈ l₁, p a) (h₂ : ∀ a ∈ l₂, p a) :
+    ((l₁ ++ l₂).pmap f fun a ha => (mem_append.1 ha).elim (h₁ a) (h₂ a)) =
+      l₁.pmap f h₁ ++ l₂.pmap f h₂ :=
+  pmap_append f l₁ l₂ _
+
+@[simp] theorem attach_append (xs : Vector α n) (ys : Vector α m) :
+    (xs ++ ys).attach = xs.attach.map (fun ⟨x, h⟩ => (⟨x, mem_append_left ys h⟩ : { x // x ∈ xs ++ ys })) ++
+      ys.attach.map (fun ⟨y, h⟩ => (⟨y, mem_append_right xs h⟩ : { y // y ∈ xs ++ ys })) := by
+  rcases xs with ⟨xs, rfl⟩
+  rcases ys with ⟨ys, rfl⟩
+  simp [Array.map_attachWith]
+
+@[simp] theorem attachWith_append {P : α → Prop} {xs : Vector α n} {ys : Vector α m}
+    {H : ∀ (a : α), a ∈ xs ++ ys → P a} :
+    (xs ++ ys).attachWith P H = xs.attachWith P (fun a h => H a (mem_append_left ys h)) ++
+      ys.attachWith P (fun a h => H a (mem_append_right xs h)) := by
+  simp [attachWith, attach_append, map_pmap, pmap_append]
+
+@[simp] theorem pmap_reverse {P : α → Prop} (f : (a : α) → P a → β) (xs : Vector α n)
+    (H : ∀ (a : α), a ∈ xs.reverse → P a) :
+    xs.reverse.pmap f H = (xs.pmap f (fun a h => H a (by simpa using h))).reverse := by
+  induction xs <;> simp_all
+
+theorem reverse_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : Vector α n)
+    (H : ∀ (a : α), a ∈ xs → P a) :
+    (xs.pmap f H).reverse = xs.reverse.pmap f (fun a h => H a (by simpa using h)) := by
+  rw [pmap_reverse]
+
+@[simp] theorem attachWith_reverse {P : α → Prop} {xs : Vector α n}
+    {H : ∀ (a : α), a ∈ xs.reverse → P a} :
+    xs.reverse.attachWith P H =
+      (xs.attachWith P (fun a h => H a (by simpa using h))).reverse := by
+  cases xs
+  simp
+
+theorem reverse_attachWith {P : α → Prop} {xs : Vector α n}
+    {H : ∀ (a : α), a ∈ xs → P a} :
+    (xs.attachWith P H).reverse = (xs.reverse.attachWith P (fun a h => H a (by simpa using h))) := by
+  cases xs
+  simp
+
+@[simp] theorem attach_reverse (xs : Vector α n) :
+    xs.reverse.attach = xs.attach.reverse.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
+  cases xs
+  rw [attach_congr (reverse_mk ..)]
+  simp [Array.map_attachWith]
+
+theorem reverse_attach (xs : Vector α n) :
+    xs.attach.reverse = xs.reverse.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
+  cases xs
+  simp [Array.map_attachWith]
+
+@[simp] theorem back?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : Vector α n)
+    (H : ∀ (a : α), a ∈ xs → P a) :
+    (xs.pmap f H).back? = xs.attach.back?.map fun ⟨a, m⟩ => f a (H a m) := by
+  cases xs
+  simp
+
+@[simp] theorem back?_attachWith {P : α → Prop} {xs : Vector α n}
+    {H : ∀ (a : α), a ∈ xs → P a} :
+    (xs.attachWith P H).back? = xs.back?.pbind (fun a h => some ⟨a, H _ (mem_of_back? h)⟩) := by
+  cases xs
+  simp
+
+@[simp]
+theorem back?_attach {xs : Vector α n} :
+    xs.attach.back? = xs.back?.pbind fun a h => some ⟨a, mem_of_back? h⟩ := by
+  cases xs
+  simp
+
+@[simp]
+theorem countP_attach (l : Vector α n) (p : α → Bool) :
+    l.attach.countP (fun a : {x // x ∈ l} => p a) = l.countP p := by
+  cases l
+  simp [Function.comp_def]
+
+@[simp]
+theorem countP_attachWith {p : α → Prop} (l : Vector α n) (H : ∀ a ∈ l, p a) (q : α → Bool) :
+    (l.attachWith p H).countP (fun a : {x // p x} => q a) = l.countP q := by
+  cases l
+  simp
+
+@[simp]
+theorem count_attach [DecidableEq α] (l : Vector α n) (a : {x // x ∈ l}) :
+    l.attach.count a = l.count ↑a := by
+  rcases l with ⟨l, rfl⟩
+  simp
+
+@[simp]
+theorem count_attachWith [DecidableEq α] {p : α → Prop} (l : Vector α n) (H : ∀ a ∈ l, p a) (a : {x // p x}) :
+    (l.attachWith p H).count a = l.count ↑a := by
+  cases l
+  simp
+
+@[simp] theorem countP_pmap {p : α → Prop} (g : ∀ a, p a → β) (f : β → Bool) (l : Vector α n) (H₁) :
+    (l.pmap g H₁).countP f =
+      l.attach.countP (fun ⟨a, m⟩ => f (g a (H₁ a m))) := by
+  rcases l with ⟨l, rfl⟩
+  simp only [pmap_mk, countP_mk, Array.countP_pmap]
+  simp [Array.countP_eq_size_filter]
+
+/-! ## unattach
+
+`Vector.unattach` is the (one-sided) inverse of `Vector.attach`. It is a synonym for `Vector.map Subtype.val`.
+
+We use it by providing a simp lemma `l.attach.unattach = l`, and simp lemmas which recognize higher order
+functions applied to `l : Vector { x // p x }` which only depend on the value, not the predicate, and rewrite these
+in terms of a simpler function applied to `l.unattach`.
+
+Further, we provide simp lemmas that push `unattach` inwards.
+-/
+
+/--
+A synonym for `l.map (·.val)`. Mostly this should not be needed by users.
+It is introduced as in intermediate step by lemmas such as `map_subtype`,
+and is ideally subsequently simplified away by `unattach_attach`.
+
+If not, usually the right approach is `simp [Vector.unattach, -Vector.map_subtype]` to unfold.
+-/
+def unattach {α : Type _} {p : α → Prop} (l : Vector { x // p x } n) : Vector α n := l.map (·.val)
+
+@[simp] theorem unattach_nil {p : α → Prop} : (#v[] : Vector { x // p x } 0).unattach = #v[] := rfl
+@[simp] theorem unattach_push {p : α → Prop} {a : { x // p x }} {l : Vector { x // p x } n} :
+    (l.push a).unattach = l.unattach.push a.1 := by
+  simp only [unattach, Vector.map_push]
+
+@[simp] theorem unattach_mk {p : α → Prop} {l : Array { x // p x }} {h : l.size = n} :
+    (mk l h).unattach = mk l.unattach (by simpa using h) := by
+  simp [unattach]
+
+@[simp] theorem toArray_unattach {p : α → Prop} {l : Vector { x // p x } n} :
+    l.unattach.toArray = l.toArray.unattach := by
+  simp [unattach]
+
+@[simp] theorem toList_unattach {p : α → Prop} {l : Array { x // p x }} :
+    l.unattach.toList = l.toList.unattach := by
+  simp [unattach]
+
+@[simp] theorem unattach_attach {l : Vector α n} : l.attach.unattach = l := by
+  rcases l with ⟨l, rfl⟩
+  simp
+
+@[simp] theorem unattach_attachWith {p : α → Prop} {l : Vector α n}
+    {H : ∀ a ∈ l, p a} :
+    (l.attachWith p H).unattach = l := by
+  cases l
+  simp
+
+@[simp] theorem getElem?_unattach {p : α → Prop} {l : Vector { x // p x } n} (i : Nat) :
+    l.unattach[i]? = l[i]?.map Subtype.val := by
+  simp [unattach]
+
+@[simp] theorem getElem_unattach
+    {p : α → Prop} {l : Vector { x // p x } n} (i : Nat) (h : i < n) :
+    l.unattach[i] = (l[i]'(by simpa using h)).1 := by
+  simp [unattach]
+
+/-! ### Recognizing higher order functions using a function that only depends on the value. -/
+
+/--
+This lemma identifies folds over arrays of subtypes, where the function only depends on the value, not the proposition,
+and simplifies these to the function directly taking the value.
+-/
+@[simp] theorem foldl_subtype {p : α → Prop} {l : Vector { x // p x } n}
+    {f : β → { x // p x } → β} {g : β → α → β} {x : β}
+    {hf : ∀ b x h, f b ⟨x, h⟩ = g b x} :
+    l.foldl f x = l.unattach.foldl g x := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.foldl_subtype (hf := hf)]
+
+/--
+This lemma identifies folds over arrays of subtypes, where the function only depends on the value, not the proposition,
+and simplifies these to the function directly taking the value.
+-/
+@[simp] theorem foldr_subtype {p : α → Prop} {l : Vector { x // p x } n}
+    {f : { x // p x } → β → β} {g : α → β → β} {x : β}
+    {hf : ∀ x h b, f ⟨x, h⟩ b = g x b} :
+    l.foldr f x = l.unattach.foldr g x := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.foldr_subtype (hf := hf)]
+
+/--
+This lemma identifies maps over arrays of subtypes, where the function only depends on the value, not the proposition,
+and simplifies these to the function directly taking the value.
+-/
+@[simp] theorem map_subtype {p : α → Prop} {l : Vector { x // p x } n}
+    {f : { x // p x } → β} {g : α → β} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
+    l.map f = l.unattach.map g := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.map_subtype (hf := hf)]
+
+/-! ### Simp lemmas pushing `unattach` inwards. -/
+
+@[simp] theorem unattach_reverse {p : α → Prop} {l : Vector { x // p x } n} :
+    l.reverse.unattach = l.unattach.reverse := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.unattach_reverse]
+
+
+@[simp] theorem unattach_append {p : α → Prop} {l₁ l₂ : Vector { x // p x } n} :
+    (l₁ ++ l₂).unattach = l₁.unattach ++ l₂.unattach := by
+  rcases l₁
+  rcases l₂
+  simp
+
+@[simp] theorem unattach_flatten {p : α → Prop} {l : Vector (Vector { x // p x } n) n} :
+    l.flatten.unattach = (l.map unattach).flatten := by
+  unfold unattach
+  cases l using vector₂_induction
+  simp only [flatten_mk, Array.map_map, Function.comp_apply, Array.map_subtype,
+    Array.unattach_attach, Array.map_id_fun', id_eq, map_mk, Array.map_flatten, map_subtype,
+    map_id_fun', unattach_mk, eq_mk]
+  unfold Array.unattach
+  rfl
+
+@[simp] theorem unattach_mkVector {p : α → Prop} {n : Nat} {x : { x // p x }} :
+    (mkVector n x).unattach = mkVector n x.1 := by
+  simp [unattach]
+
+end Vector
diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean
index d818ffdaca..07fa54d7ae 100644
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -779,6 +779,10 @@ theorem getElem?_of_mem {a} {l : Vector α n} (h : a ∈ l) : ∃ i : Nat, l[i]?
 theorem mem_of_getElem? {l : Vector α n} {i : Nat} {a : α} (e : l[i]? = some a) : a ∈ l :=
   let ⟨_, e⟩ := getElem?_eq_some_iff.1 e; e ▸ getElem_mem ..
 
+theorem mem_of_back? {xs : Vector α n} {a : α} (h : xs.back? = some a) : a ∈ xs := by
+  cases xs
+  simpa using Array.mem_of_back? (by simpa using h)
+
 theorem mem_iff_getElem {a} {l : Vector α n} : a ∈ l ↔ ∃ (i : Nat) (h : i < n), l[i]'h = a :=
   ⟨getElem_of_mem, fun ⟨_, _, e⟩ => e ▸ getElem_mem ..⟩
 
@@ -1147,6 +1151,11 @@ theorem mem_setIfInBounds (v : Vector α n) (i : Nat) (hi : i < n) (a : α) :
   cases a
   simp
 
+@[simp] theorem getElem?_map (f : α → β) (a : Vector α n) (i : Nat) :
+    (a.map f)[i]? = a[i]?.map f := by
+  cases a
+  simp
+
 /-- The empty vector maps to the empty vector. -/
 @[simp]
 theorem map_empty (f : α → β) : map f #v[] = #v[] := by
@@ -1323,10 +1332,10 @@ theorem singleton_eq_toVector_singleton (a : α) : #v[a] = #[a].toVector := rfl
   cases t
   simp
 
-theorem mem_append_left {a : α} {s : Vector α n} {t : Vector α m} (h : a ∈ s) : a ∈ s ++ t :=
+theorem mem_append_left {a : α} {s : Vector α n} (t : Vector α m) (h : a ∈ s) : a ∈ s ++ t :=
   mem_append.2 (Or.inl h)
 
-theorem mem_append_right {a : α} {s : Vector α n} {t : Vector α m} (h : a ∈ t) : a ∈ s ++ t :=
+theorem mem_append_right {a : α} (s : Vector α n) {t : Vector α m} (h : a ∈ t) : a ∈ s ++ t :=
   mem_append.2 (Or.inr h)
 
 theorem not_mem_append {a : α} {s : Vector α n} {t : Vector α m} (h₁ : a ∉ s) (h₂ : a ∉ t) :