diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index 33d8c79b97b6..e70e62b7c831 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -1658,9 +1658,9 @@ theorem getElem_of_append {l l₁ l₂ : Array α} (eq : l = l₁.push a ++ l₂
   rw [← getElem?_eq_getElem, eq, getElem?_append_left (by simp; omega), ← h]
   simp
 
-@[simp 1100] theorem append_singleton {a : α} {as : Array α} : as ++ #[a] = as.push a := by
-  cases as
-  simp
+@[simp 1100] theorem append_singleton {a : α} {as : Array α} : as ++ #[a] = as.push a := rfl
+
+theorem push_eq_append {a : α} {as : Array α} : as.push a = as ++ #[a] := rfl
 
 theorem append_inj {s₁ s₂ t₁ t₂ : Array α} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : s₁.size = s₂.size) :
     s₁ = s₂ ∧ t₁ = t₂ := by
diff --git a/src/Init/Data/Array/MapIdx.lean b/src/Init/Data/Array/MapIdx.lean
index b25f3653dcf6..92100795f614 100644
--- a/src/Init/Data/Array/MapIdx.lean
+++ b/src/Init/Data/Array/MapIdx.lean
@@ -5,6 +5,7 @@ Authors: Mario Carneiro, Kim Morrison
 -/
 prelude
 import Init.Data.Array.Lemmas
+import Init.Data.Array.Attach
 import Init.Data.List.MapIdx
 
 namespace Array
@@ -111,3 +112,293 @@ namespace List
   ext <;> simp
 
 end List
+
+namespace Array
+
+/-! ### zipWithIndex -/
+
+@[simp] theorem getElem_zipWithIndex (a : Array α) (i : Nat) (h : i < a.zipWithIndex.size) :
+    (a.zipWithIndex)[i] = (a[i]'(by simp_all), i) := by
+  simp [zipWithIndex]
+
+@[simp] theorem zipWithIndex_toArray {l : List α} :
+    l.toArray.zipWithIndex = (l.enum.map fun (i, x) => (x, i)).toArray := by
+  ext i hi₁ hi₂ <;> simp
+
+@[simp] theorem toList_zipWithIndex (a : Array α) :
+    a.zipWithIndex.toList = a.toList.enum.map (fun (i, a) => (a, i)) := by
+  rcases a with ⟨a⟩
+  simp
+
+theorem mk_mem_zipWithIndex_iff_getElem? {x : α} {i : Nat} {l : Array α} :
+    (x, i) ∈ l.zipWithIndex ↔ l[i]? = x := by
+  rcases l with ⟨l⟩
+  simp only [zipWithIndex_toArray, mem_toArray, List.mem_map, Prod.mk.injEq, Prod.exists,
+    List.mk_mem_enum_iff_getElem?, List.getElem?_toArray]
+  constructor
+  · rintro ⟨a, b, h, rfl, rfl⟩
+    exact h
+  · intro h
+    exact ⟨i, x, by simp [h]⟩
+
+theorem mem_enum_iff_getElem? {x : α × Nat} {l : Array α} : x ∈ l.zipWithIndex ↔ l[x.2]? = some x.1 :=
+  mk_mem_zipWithIndex_iff_getElem?
+
+/-! ### mapFinIdx -/
+
+@[congr] theorem mapFinIdx_congr {xs ys : Array α} (w : xs = ys)
+    (f : (i : Nat) → α → (h : i < xs.size) → β) :
+    mapFinIdx xs f = mapFinIdx ys (fun i a h => f i a (by simp [w]; omega)) := by
+  subst w
+  rfl
+
+@[simp]
+theorem mapFinIdx_empty {f : (i : Nat) → α → (h : i < 0) → β} : mapFinIdx #[] f = #[] :=
+  rfl
+
+theorem mapFinIdx_eq_ofFn {as : Array α} {f : (i : Nat) → α → (h : i < as.size) → β} :
+    as.mapFinIdx f = Array.ofFn fun i : Fin as.size => f i as[i] i.2 := by
+  cases as
+  simp [List.mapFinIdx_eq_ofFn]
+
+theorem mapFinIdx_append {K L : Array α} {f : (i : Nat) → α → (h : i < (K ++ L).size) → β} :
+    (K ++ L).mapFinIdx f =
+      K.mapFinIdx (fun i a h => f i a (by simp; omega)) ++
+        L.mapFinIdx (fun i a h => f (i + K.size) a (by simp; omega)) := by
+  cases K
+  cases L
+  simp [List.mapFinIdx_append]
+
+@[simp]
+theorem mapFinIdx_push {l : Array α} {a : α} {f : (i : Nat) → α → (h : i < (l.push a).size) → β} :
+    mapFinIdx (l.push a) f =
+      (mapFinIdx l (fun i a h => f i a (by simp; omega))).push (f l.size a (by simp)) := by
+  simp [← append_singleton, mapFinIdx_append]
+
+theorem mapFinIdx_singleton {a : α} {f : (i : Nat) → α → (h : i < 1) → β} :
+    #[a].mapFinIdx f = #[f 0 a (by simp)] := by
+  simp
+
+theorem mapFinIdx_eq_zipWithIndex_map {l : Array α} {f : (i : Nat) → α → (h : i < l.size) → β} :
+    l.mapFinIdx f = l.zipWithIndex.attach.map
+      fun ⟨⟨x, i⟩, m⟩ =>
+        f i x (by simp [mk_mem_zipWithIndex_iff_getElem?, getElem?_eq_some_iff] at m; exact m.1) := by
+  ext <;> simp
+
+@[simp]
+theorem mapFinIdx_eq_empty_iff {l : Array α} {f : (i : Nat) → α → (h : i < l.size) → β} :
+    l.mapFinIdx f = #[] ↔ l = #[] := by
+  cases l
+  simp
+
+theorem mapFinIdx_ne_empty_iff {l : Array α} {f : (i : Nat) → α → (h : i < l.size) → β} :
+    l.mapFinIdx f ≠ #[] ↔ l ≠ #[] := by
+  simp
+
+theorem exists_of_mem_mapFinIdx {b : β} {l : Array α} {f : (i : Nat) → α → (h : i < l.size) → β}
+    (h : b ∈ l.mapFinIdx f) : ∃ (i : Nat) (h : i < l.size), f i l[i] h = b := by
+  rcases l with ⟨l⟩
+  exact List.exists_of_mem_mapFinIdx (by simpa using h)
+
+@[simp] theorem mem_mapFinIdx {b : β} {l : Array α} {f : (i : Nat) → α → (h : i < l.size) → β} :
+    b ∈ l.mapFinIdx f ↔ ∃ (i : Nat) (h : i < l.size), f i l[i] h = b := by
+  rcases l with ⟨l⟩
+  simp
+
+theorem mapFinIdx_eq_iff {l : Array α} {f : (i : Nat) → α → (h : i < l.size) → β} :
+    l.mapFinIdx f = l' ↔ ∃ h : l'.size = l.size, ∀ (i : Nat) (h : i < l.size), l'[i] = f i l[i] h := by
+  rcases l with ⟨l⟩
+  rcases l' with ⟨l'⟩
+  simpa using List.mapFinIdx_eq_iff
+
+@[simp] theorem mapFinIdx_eq_singleton_iff {l : Array α} {f : (i : Nat) → α → (h : i < l.size) → β} {b : β} :
+    l.mapFinIdx f = #[b] ↔ ∃ (a : α) (w : l = #[a]), f 0 a (by simp [w]) = b := by
+  rcases l with ⟨l⟩
+  simp
+
+theorem mapFinIdx_eq_append_iff {l : Array α} {f : (i : Nat) → α → (h : i < l.size) → β} {l₁ l₂ : Array β} :
+    l.mapFinIdx f = l₁ ++ l₂ ↔
+      ∃ (l₁' : Array α) (l₂' : Array α) (w : l = l₁' ++ l₂'),
+        l₁'.mapFinIdx (fun i a h => f i a (by simp [w]; omega)) = l₁ ∧
+        l₂'.mapFinIdx (fun i a h => f (i + l₁'.size) a (by simp [w]; omega)) = l₂ := by
+  rcases l with ⟨l⟩
+  rcases l₁ with ⟨l₁⟩
+  rcases l₂ with ⟨l₂⟩
+  simp only [List.mapFinIdx_toArray, List.append_toArray, mk.injEq, List.mapFinIdx_eq_append_iff,
+    toArray_eq_append_iff]
+  constructor
+  · rintro ⟨l₁, l₂, rfl, rfl, rfl⟩
+    refine ⟨l₁.toArray, l₂.toArray, by simp_all⟩
+  · rintro ⟨⟨l₁⟩, ⟨l₂⟩, rfl, h₁, h₂⟩
+    simp [← toList_inj] at h₁ h₂
+    obtain rfl := h₁
+    obtain rfl := h₂
+    refine ⟨l₁, l₂, by simp_all⟩
+
+theorem mapFinIdx_eq_push_iff {l : Array α} {b : β} {f : (i : Nat) → α → (h : i < l.size) → β} :
+    l.mapFinIdx f = l₂.push b ↔
+      ∃ (l₁ : Array α) (a : α) (w : l = l₁.push a),
+        l₁.mapFinIdx (fun i a h => f i a (by simp [w]; omega)) = l₂ ∧ b = f (l.size - 1) a (by simp [w]) := by
+  rw [push_eq_append, mapFinIdx_eq_append_iff]
+  constructor
+  · rintro ⟨l₁, l₂, rfl, rfl, h₂⟩
+    simp only [mapFinIdx_eq_singleton_iff, Nat.zero_add] at h₂
+    obtain ⟨a, rfl, rfl⟩ := h₂
+    exact ⟨l₁, a, by simp⟩
+  · rintro ⟨l₁, a, rfl, rfl, rfl⟩
+    exact ⟨l₁, #[a], by simp⟩
+
+theorem mapFinIdx_eq_mapFinIdx_iff {l : Array α} {f g : (i : Nat) → α → (h : i < l.size) → β} :
+    l.mapFinIdx f = l.mapFinIdx g ↔ ∀ (i : Nat) (h : i < l.size), f i l[i] h = g i l[i] h := by
+  rw [eq_comm, mapFinIdx_eq_iff]
+  simp
+
+@[simp] theorem mapFinIdx_mapFinIdx {l : Array α}
+    {f : (i : Nat) → α → (h : i < l.size) → β}
+    {g : (i : Nat) → β → (h : i < (l.mapFinIdx f).size) → γ} :
+    (l.mapFinIdx f).mapFinIdx g = l.mapFinIdx (fun i a h => g i (f i a h) (by simpa using h)) := by
+  simp [mapFinIdx_eq_iff]
+
+theorem mapFinIdx_eq_mkArray_iff {l : Array α} {f : (i : Nat) → α → (h : i < l.size) → β} {b : β} :
+    l.mapFinIdx f = mkArray l.size b ↔ ∀ (i : Nat) (h : i < l.size), f i l[i] h = b := by
+  rcases l with ⟨l⟩
+  rw [← toList_inj]
+  simp [List.mapFinIdx_eq_replicate_iff]
+
+@[simp] theorem mapFinIdx_reverse {l : Array α} {f : (i : Nat) → α → (h : i < l.reverse.size) → β} :
+    l.reverse.mapFinIdx f = (l.mapFinIdx (fun i a h => f (l.size - 1 - i) a (by simp; omega))).reverse := by
+  rcases l with ⟨l⟩
+  simp [List.mapFinIdx_reverse]
+
+/-! ### mapIdx -/
+
+@[simp]
+theorem mapIdx_empty {f : Nat → α → β} : mapIdx f #[] = #[] :=
+  rfl
+
+@[simp] theorem mapFinIdx_eq_mapIdx {l : Array α} {f : (i : Nat) → α → (h : i < l.size) → β} {g : Nat → α → β}
+    (h : ∀ (i : Nat) (h : i < l.size), f i l[i] h = g i l[i]) :
+    l.mapFinIdx f = l.mapIdx g := by
+  simp_all [mapFinIdx_eq_iff]
+
+theorem mapIdx_eq_mapFinIdx {l : Array α} {f : Nat → α → β} :
+    l.mapIdx f = l.mapFinIdx (fun i a _ => f i a) := by
+  simp [mapFinIdx_eq_mapIdx]
+
+theorem mapIdx_eq_zipWithIndex_map {l : Array α} {f : Nat → α → β} :
+    l.mapIdx f = l.zipWithIndex.map fun ⟨a, i⟩ => f i a := by
+  ext <;> simp
+
+theorem mapIdx_append {K L : Array α} :
+    (K ++ L).mapIdx f = K.mapIdx f ++ L.mapIdx fun i => f (i + K.size) := by
+  rcases K with ⟨K⟩
+  rcases L with ⟨L⟩
+  simp [List.mapIdx_append]
+
+@[simp]
+theorem mapIdx_push {l : Array α} {a : α} :
+    mapIdx f (l.push a) = (mapIdx f l).push (f l.size a) := by
+  simp [← append_singleton, mapIdx_append]
+
+theorem mapIdx_singleton {a : α} : mapIdx f #[a] = #[f 0 a] := by
+  simp
+
+@[simp]
+theorem mapIdx_eq_empty_iff {l : Array α} : mapIdx f l = #[] ↔ l = #[] := by
+  rcases l with ⟨l⟩
+  simp
+
+theorem mapIdx_ne_empty_iff {l : Array α} :
+    mapIdx f l ≠ #[] ↔ l ≠ #[] := by
+  simp
+
+theorem exists_of_mem_mapIdx {b : β} {l : Array α}
+    (h : b ∈ mapIdx f l) : ∃ (i : Nat) (h : i < l.size), f i l[i] = b := by
+  rw [mapIdx_eq_mapFinIdx] at h
+  simpa [Fin.exists_iff] using exists_of_mem_mapFinIdx h
+
+@[simp] theorem mem_mapIdx {b : β} {l : Array α} :
+    b ∈ mapIdx f l ↔ ∃ (i : Nat) (h : i < l.size), f i l[i] = b := by
+  constructor
+  · intro h
+    exact exists_of_mem_mapIdx h
+  · rintro ⟨i, h, rfl⟩
+    rw [mem_iff_getElem]
+    exact ⟨i, by simpa using h, by simp⟩
+
+theorem mapIdx_eq_push_iff {l : Array α} {b : β} :
+    mapIdx f l = l₂.push b ↔
+      ∃ (a : α) (l₁ : Array α), l = l₁.push a ∧ mapIdx f l₁ = l₂ ∧ f l₁.size a = b := by
+  rw [mapIdx_eq_mapFinIdx, mapFinIdx_eq_push_iff]
+  simp only [mapFinIdx_eq_mapIdx, exists_and_left, exists_prop]
+  constructor
+  · rintro ⟨l₁, rfl, a, rfl, rfl⟩
+    exact ⟨a, l₁, by simp⟩
+  · rintro ⟨a, l₁, rfl, rfl, rfl⟩
+    exact ⟨l₁, rfl, a, by simp⟩
+
+@[simp] theorem mapIdx_eq_singleton_iff {l : Array α} {f : Nat → α → β} {b : β} :
+    mapIdx f l = #[b] ↔ ∃ (a : α), l = #[a] ∧ f 0 a = b := by
+  rcases l with ⟨l⟩
+  simp [List.mapIdx_eq_singleton_iff]
+
+theorem mapIdx_eq_append_iff {l : Array α} {f : Nat → α → β} {l₁ l₂ : Array β} :
+    mapIdx f l = l₁ ++ l₂ ↔
+      ∃ (l₁' : Array α) (l₂' : Array α), l = l₁' ++ l₂' ∧
+        l₁'.mapIdx f = l₁ ∧
+        l₂'.mapIdx (fun i => f (i + l₁'.size)) = l₂ := by
+  rcases l with ⟨l⟩
+  rcases l₁ with ⟨l₁⟩
+  rcases l₂ with ⟨l₂⟩
+  simp only [List.mapIdx_toArray, List.append_toArray, mk.injEq, List.mapIdx_eq_append_iff,
+    toArray_eq_append_iff]
+  constructor
+  · rintro ⟨l₁, l₂, rfl, rfl, rfl⟩
+    exact ⟨l₁.toArray, l₂.toArray, by simp⟩
+  · rintro ⟨⟨l₁⟩, ⟨l₂⟩, rfl, h₁, h₂⟩
+    simp only [List.mapIdx_toArray, mk.injEq, size_toArray] at h₁ h₂
+    obtain rfl := h₁
+    obtain rfl := h₂
+    exact ⟨l₁, l₂, by simp⟩
+
+theorem mapIdx_eq_iff {l : Array α} : mapIdx f l = l' ↔ ∀ i : Nat, l'[i]? = l[i]?.map (f i) := by
+  rcases l with ⟨l⟩
+  rcases l' with ⟨l'⟩
+  simp [List.mapIdx_eq_iff]
+
+theorem mapIdx_eq_mapIdx_iff {l : Array α} :
+    mapIdx f l = mapIdx g l ↔ ∀ i : Nat, (h : i < l.size) → f i l[i] = g i l[i] := by
+  rcases l with ⟨l⟩
+  simp [List.mapIdx_eq_mapIdx_iff]
+
+@[simp] theorem mapIdx_set {l : Array α} {i : Nat} {h : i < l.size} {a : α} :
+    (l.set i a).mapIdx f = (l.mapIdx f).set i (f i a) (by simpa) := by
+  rcases l with ⟨l⟩
+  simp [List.mapIdx_set]
+
+@[simp] theorem mapIdx_setIfInBounds {l : Array α} {i : Nat} {a : α} :
+    (l.setIfInBounds i a).mapIdx f = (l.mapIdx f).setIfInBounds i (f i a) := by
+  rcases l with ⟨l⟩
+  simp [List.mapIdx_set]
+
+@[simp] theorem back?_mapIdx {l : Array α} {f : Nat → α → β} :
+    (mapIdx f l).back? = (l.back?).map (f (l.size - 1)) := by
+  rcases l with ⟨l⟩
+  simp [List.getLast?_mapIdx]
+
+@[simp] theorem mapIdx_mapIdx {l : Array α} {f : Nat → α → β} {g : Nat → β → γ} :
+    (l.mapIdx f).mapIdx g = l.mapIdx (fun i => g i ∘ f i) := by
+  simp [mapIdx_eq_iff]
+
+theorem mapIdx_eq_mkArray_iff {l : Array α} {f : Nat → α → β} {b : β} :
+    mapIdx f l = mkArray l.size b ↔ ∀ (i : Nat) (h : i < l.size), f i l[i] = b := by
+  rcases l with ⟨l⟩
+  rw [← toList_inj]
+  simp [List.mapIdx_eq_replicate_iff]
+
+@[simp] theorem mapIdx_reverse {l : Array α} {f : Nat → α → β} :
+    l.reverse.mapIdx f = (mapIdx (fun i => f (l.size - 1 - i)) l).reverse := by
+  rcases l with ⟨l⟩
+  simp [List.mapIdx_reverse]
+
+end Array
diff --git a/src/Init/Data/List/MapIdx.lean b/src/Init/Data/List/MapIdx.lean
index e1a248b4d51e..5c7030a6896b 100644
--- a/src/Init/Data/List/MapIdx.lean
+++ b/src/Init/Data/List/MapIdx.lean
@@ -17,12 +17,13 @@ namespace List
 
 /-! ### mapIdx -/
 
-
 /--
 Given a list `as = [a₀, a₁, ...]` function `f : Fin as.length → α → β`, returns the list
 `[f 0 a₀, f 1 a₁, ...]`.
 -/
-@[inline] def mapFinIdx (as : List α) (f : (i : Nat) → α → (h : i < as.length) → β) : List β := go as #[] (by simp) where
+@[inline] def mapFinIdx (as : List α) (f : (i : Nat) → α → (h : i < as.length) → β) : List β :=
+  go as #[] (by simp)
+where
   /-- Auxiliary for `mapFinIdx`:
   `mapFinIdx.go [a₀, a₁, ...] acc = acc.toList ++ [f 0 a₀, f 1 a₁, ...]` -/
   @[specialize] go : (bs : List α) → (acc : Array β) → bs.length + acc.size = as.length → List β
@@ -43,6 +44,12 @@ Given a function `f : Nat → α → β` and `as : List α`, `as = [a₀, a₁,
 
 /-! ### mapFinIdx -/
 
+@[congr] theorem mapFinIdx_congr {xs ys : List α} (w : xs = ys)
+    (f : (i : Nat) → α → (h : i < xs.length) → β) :
+    mapFinIdx xs f = mapFinIdx ys (fun i a h => f i a (by simp [w]; omega)) := by
+  subst w
+  rfl
+
 @[simp]
 theorem mapFinIdx_nil {f : (i : Nat) → α → (h : i < 0) → β} : mapFinIdx [] f = [] :=
   rfl
@@ -188,6 +195,49 @@ theorem mapFinIdx_eq_iff {l : List α} {f : (i : Nat) → α → (h : i < l.leng
   · rintro ⟨h, w⟩
     apply ext_getElem <;> simp_all
 
+@[simp] theorem mapFinIdx_eq_singleton_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} {b : β} :
+    l.mapFinIdx f = [b] ↔ ∃ (a : α) (w : l = [a]), f 0 a (by simp [w]) = b := by
+  simp [mapFinIdx_eq_cons_iff]
+
+theorem mapFinIdx_eq_append_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
+    l.mapFinIdx f = l₁ ++ l₂ ↔
+      ∃ (l₁' : List α) (l₂' : List α) (w : l = l₁' ++ l₂'),
+        l₁'.mapFinIdx (fun i a h => f i a (by simp [w]; omega)) = l₁ ∧
+        l₂'.mapFinIdx (fun i a h => f (i + l₁'.length) a (by simp [w]; omega)) = l₂ := by
+  rw [mapFinIdx_eq_iff]
+  constructor
+  · intro ⟨h, w⟩
+    simp only [length_append] at h
+    refine ⟨l.take l₁.length, l.drop l₁.length, by simp, ?_⟩
+    constructor
+    · apply ext_getElem
+      · simp
+        omega
+      · intro i hi₁ hi₂
+        simp only [getElem_mapFinIdx, getElem_take]
+        specialize w i (by omega)
+        rw [getElem_append_left hi₂] at w
+        exact w.symm
+    · apply ext_getElem
+      · simp
+        omega
+      · intro i hi₁ hi₂
+        simp only [getElem_mapFinIdx, getElem_take]
+        simp only [length_take, getElem_drop]
+        have : l₁.length ≤ l.length := by omega
+        simp only [Nat.min_eq_left this, Nat.add_comm]
+        specialize w (i + l₁.length) (by omega)
+        rw [getElem_append_right (by omega)] at w
+        simpa using w.symm
+  · rintro ⟨l₁', l₂', rfl, rfl, rfl⟩
+    refine ⟨by simp, fun i h => ?_⟩
+    rw [getElem_append]
+    split <;> rename_i h'
+    · simp [getElem_append_left (by simpa using h')]
+    · simp only [length_mapFinIdx, Nat.not_lt] at h'
+      have : i - l₁'.length + l₁'.length = i := by omega
+      simp [getElem_append_right h', this]
+
 theorem mapFinIdx_eq_mapFinIdx_iff {l : List α} {f g : (i : Nat) → α → (h : i < l.length) → β} :
     l.mapFinIdx f = l.mapFinIdx g ↔ ∀ (i : Nat) (h : i < l.length), f i l[i] h = g i l[i] h := by
   rw [eq_comm, mapFinIdx_eq_iff]
@@ -338,6 +388,10 @@ theorem mapIdx_eq_cons_iff' {l : List α} {b : β} :
       l.head?.map (f 0) = some b ∧ l.tail?.map (mapIdx fun i => f (i + 1)) = some l₂ := by
   cases l <;> simp
 
+@[simp] theorem mapIdx_eq_singleton_iff {l : List α} {f : Nat → α → β} {b : β} :
+    mapIdx f l = [b] ↔ ∃ (a : α), l = [a] ∧ f 0 a = b := by
+  simp [mapIdx_eq_cons_iff]
+
 theorem mapIdx_eq_iff {l : List α} : mapIdx f l = l' ↔ ∀ i : Nat, l'[i]? = l[i]?.map (f i) := by
   constructor
   · intro w i
@@ -346,6 +400,19 @@ theorem mapIdx_eq_iff {l : List α} : mapIdx f l = l' ↔ ∀ i : Nat, l'[i]? =
     ext1 i
     simp [w]
 
+theorem mapIdx_eq_append_iff {l : List α} :
+    mapIdx f l = l₁ ++ l₂ ↔
+      ∃ (l₁' : List α) (l₂' : List α), l = l₁' ++ l₂' ∧
+        mapIdx f l₁' = l₁ ∧
+        mapIdx (fun i => f (i + l₁'.length)) l₂' = l₂ := by
+  rw [mapIdx_eq_mapFinIdx, mapFinIdx_eq_append_iff]
+  simp only [mapFinIdx_eq_mapIdx, exists_and_left, exists_prop]
+  constructor
+  · rintro ⟨l₁, rfl, l₂, rfl, h⟩
+    refine ⟨l₁, l₂, by simp_all⟩
+  · rintro ⟨l₁, l₂, rfl, rfl, rfl⟩
+    refine ⟨l₁, rfl, l₂, by simp_all⟩
+
 theorem mapIdx_eq_mapIdx_iff {l : List α} :
     mapIdx f l = mapIdx g l ↔ ∀ i : Nat, (h : i < l.length) → f i l[i] = g i l[i] := by
   constructor
diff --git a/src/Init/Data/Vector.lean b/src/Init/Data/Vector.lean
index 87a6d17b5e5a..9e32effb6fdd 100644
--- a/src/Init/Data/Vector.lean
+++ b/src/Init/Data/Vector.lean
@@ -5,3 +5,6 @@ Authors: Kim Morrison
 -/
 prelude
 import Init.Data.Vector.Basic
+import Init.Data.Vector.Lemmas
+import Init.Data.Vector.Lex
+import Init.Data.Vector.MapIdx
diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean
index 32b336c4801d..a12414dba568 100644
--- a/src/Init/Data/Vector/Basic.lean
+++ b/src/Init/Data/Vector/Basic.lean
@@ -6,6 +6,7 @@ Authors: Shreyas Srinivas, François G. Dorais, Kim Morrison
 
 prelude
 import Init.Data.Array.Lemmas
+import Init.Data.Array.MapIdx
 import Init.Data.Range
 
 /-!
@@ -90,14 +91,12 @@ of bounds.
 /-- The last element of a vector. Panics if the vector is empty. -/
 @[inline] def back! [Inhabited α] (v : Vector α n) : α := v.toArray.back!
 
-/-- The last element of a vector, or `none` if the array is empty. -/
+/-- The last element of a vector, or `none` if the vector is empty. -/
 @[inline] def back? (v : Vector α n) : Option α := v.toArray.back?
 
 /-- The last element of a non-empty vector. -/
 @[inline] def back [NeZero n] (v : Vector α n) : α :=
-  -- TODO: change to just `v[n]`
-  have : Inhabited α := ⟨v[0]'(Nat.pos_of_neZero n)⟩
-  v.back!
+  v[n - 1]'(Nat.sub_one_lt (NeZero.ne n))
 
 /-- The first element of a non-empty vector.  -/
 @[inline] def head [NeZero n] (v : Vector α n) := v[0]'(Nat.pos_of_neZero n)
@@ -170,6 +169,15 @@ result is empty. If `stop` is greater than the size of the vector, the size is u
 @[inline] def map (f : α → β) (v : Vector α n) : Vector β n :=
   ⟨v.toArray.map f, by simp⟩
 
+/-- Maps elements of a vector using the function `f`, which also receives the index of the element. -/
+@[inline] def mapIdx (f : Nat → α → β) (v : Vector α n) : Vector β n :=
+  ⟨v.toArray.mapIdx f, by simp⟩
+
+/-- Maps elements of a vector using the function `f`,
+which also receives the index of the element, and the fact that the index is less than the size of the vector. -/
+@[inline] def mapFinIdx (v : Vector α n) (f : (i : Nat) → α → (h : i < n) → β) : Vector β n :=
+  ⟨v.toArray.mapFinIdx (fun i a h => f i a (by simpa [v.size_toArray] using h)), by simp⟩
+
 @[inline] def flatten (v : Vector (Vector α n) m) : Vector α (m * n) :=
   ⟨(v.toArray.map Vector.toArray).flatten,
     by rcases v; simp_all [Function.comp_def, Array.map_const']⟩
@@ -177,6 +185,9 @@ result is empty. If `stop` is greater than the size of the vector, the size is u
 @[inline] def flatMap (v : Vector α n) (f : α → Vector β m) : Vector β (n * m) :=
   ⟨v.toArray.flatMap fun a => (f a).toArray, by simp [Array.map_const']⟩
 
+@[inline] def zipWithIndex (v : Vector α n) : Vector (α × Nat) n :=
+  ⟨v.toArray.zipWithIndex, by simp⟩
+
 /-- Maps corresponding elements of two vectors of equal size using the function `f`. -/
 @[inline] def zipWith (a : Vector α n) (b : Vector β n) (f : α → β → φ) : Vector φ n :=
   ⟨Array.zipWith a.toArray b.toArray f, by simp⟩
diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean
index b12146a9a091..30ef609d91a1 100644
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -23,7 +23,6 @@ end Array
 
 namespace Vector
 
-
 /-! ### mk lemmas -/
 
 theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a := rfl
@@ -70,6 +69,10 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
 @[simp] theorem back?_mk (a : Array α) (h : a.size = n) :
     (Vector.mk a h).back? = a.back? := rfl
 
+@[simp] theorem back_mk [NeZero n] (a : Array α) (h : a.size = n) :
+    (Vector.mk a h).back =
+      a[n - 1]'(Nat.lt_of_lt_of_eq (Nat.sub_one_lt (NeZero.ne n)) h.symm) := rfl
+
 @[simp] theorem foldlM_mk [Monad m] (f : β → α → m β) (b : β) (a : Array α) (h : a.size = n) :
     (Vector.mk a h).foldlM f b = a.foldlM f b := rfl
 
@@ -111,6 +114,13 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
 @[simp] theorem map_mk (a : Array α) (h : a.size = n) (f : α → β) :
     (Vector.mk a h).map f = Vector.mk (a.map f) (by simp [h]) := rfl
 
+@[simp] theorem mapIdx_mk (a : Array α) (h : a.size = n) (f : Nat → α → β) :
+    (Vector.mk a h).mapIdx f = Vector.mk (a.mapIdx f) (by simp [h]) := rfl
+
+@[simp] theorem mapFinIdx_mk (a : Array α) (h : a.size = n) (f : (i : Nat) → α → (h : i < n) → β) :
+    (Vector.mk a h).mapFinIdx f =
+      Vector.mk (a.mapFinIdx fun i a h' => f i a (by simpa [h] using h')) (by simp [h]) := rfl
+
 @[simp] theorem reverse_mk (a : Array α) (h : a.size = n) :
     (Vector.mk a h).reverse = Vector.mk a.reverse (by simp [h]) := rfl
 
@@ -141,6 +151,9 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
 @[simp] theorem take_mk (a : Array α) (h : a.size = n) (m) :
     (Vector.mk a h).take m = Vector.mk (a.take m) (by simp [h]) := rfl
 
+@[simp] theorem zipWithIndex_mk (a : Array α) (h : a.size = n) :
+    (Vector.mk a h).zipWithIndex = Vector.mk (a.zipWithIndex) (by simp [h]) := rfl
+
 @[simp] theorem mk_zipWith_mk (f : α → β → γ) (a : Array α) (b : Array β)
       (ha : a.size = n) (hb : b.size = n) : zipWith (Vector.mk a ha) (Vector.mk b hb) f =
         Vector.mk (Array.zipWith a b f) (by simp [ha, hb]) := rfl
@@ -204,6 +217,14 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
 @[simp] theorem toArray_map (f : α → β) (a : Vector α n) :
     (a.map f).toArray = a.toArray.map f := rfl
 
+@[simp] theorem toArray_mapIdx (f : Nat → α → β) (a : Vector α n) :
+    (a.mapIdx f).toArray = a.toArray.mapIdx f := rfl
+
+@[simp] theorem toArray_mapFinIdx (f : (i : Nat) → α → (h : i < n) → β) (v : Vector α n) :
+    (v.mapFinIdx f).toArray =
+      v.toArray.mapFinIdx (fun i a h => f i a (by simpa [v.size_toArray] using h)) :=
+  rfl
+
 @[simp] theorem toArray_ofFn (f : Fin n → α) : (Vector.ofFn f).toArray = Array.ofFn f := rfl
 
 @[simp] theorem toArray_pop (a : Vector α n) : a.pop.toArray = a.toArray.pop := rfl
@@ -246,6 +267,9 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
 
 @[simp] theorem toArray_take (a : Vector α n) (m) : (a.take m).toArray = a.toArray.take m := rfl
 
+@[simp] theorem toArray_zipWithIndex (a : Vector α n) :
+    (a.zipWithIndex).toArray = a.toArray.zipWithIndex := rfl
+
 @[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
 
@@ -298,6 +322,8 @@ protected theorem ext {a b : Vector α n} (h : (i : Nat) → (_ : i < n) → a[i
 
 /-! ### toList -/
 
+theorem toArray_toList (a : Vector α n) : a.toArray.toList = a.toList := rfl
+
 @[simp] theorem getElem_toList {α n} (xs : Vector α n) (i : Nat) (h : i < xs.toList.length) :
     xs.toList[i] = xs[i]'(by simpa using h) := by
   cases xs
@@ -337,6 +363,14 @@ theorem toList_extract (a : Vector α n) (start stop) :
 theorem toList_map (f : α → β) (a : Vector α n) :
     (a.map f).toList = a.toList.map f := by simp
 
+theorem toList_mapIdx (f : Nat → α → β) (a : Vector α n) :
+    (a.mapIdx f).toList = a.toList.mapIdx f := by simp
+
+theorem toList_mapFinIdx (f : (i : Nat) → α → (h : i < n) → β) (v : Vector α n) :
+    (v.mapFinIdx f).toList =
+      v.toList.mapFinIdx (fun i a h => f i a (by simpa [v.size_toArray] using h)) := by
+  simp
+
 theorem toList_ofFn (f : Fin n → α) : (Vector.ofFn f).toList = List.ofFn f := by simp
 
 theorem toList_pop (a : Vector α n) : a.pop.toList = a.toList.dropLast := rfl
@@ -1860,7 +1894,7 @@ defeq issues in the implicit size argument.
   · simp [h]
   · replace h : i = v.size - 1 := by rw [size_toArray]; omega
     subst h
-    simp [pop, back, back!, ← Array.eq_push_pop_back!_of_size_ne_zero]
+    simp [back]
 
 /-! ### extract -/
 
diff --git a/src/Init/Data/Vector/MapIdx.lean b/src/Init/Data/Vector/MapIdx.lean
new file mode 100644
index 000000000000..fbcc3dac6b53
--- /dev/null
+++ b/src/Init/Data/Vector/MapIdx.lean
@@ -0,0 +1,333 @@
+/-
+Copyright (c) 2025 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.Array.MapIdx
+import Init.Data.Vector.Lemmas
+
+namespace Vector
+
+/-! ### mapFinIdx -/
+
+@[simp] theorem getElem_mapFinIdx (a : Vector α n) (f : (i : Nat) → α → (h : i < n) → β) (i : Nat)
+    (h : i < n) :
+    (a.mapFinIdx f)[i] = f i a[i] h := by
+  rcases a with ⟨a, rfl⟩
+  simp
+
+@[simp] theorem getElem?_mapFinIdx (a : Vector α n) (f : (i : Nat) → α → (h : i < n) → β) (i : Nat) :
+    (a.mapFinIdx f)[i]? =
+      a[i]?.pbind fun b h => f i b (getElem?_eq_some_iff.1 h).1 := by
+  simp only [getElem?_def, getElem_mapFinIdx]
+  split <;> simp_all
+
+/-! ### mapIdx -/
+
+@[simp] theorem getElem_mapIdx (f : Nat → α → β) (a : Vector α n) (i : Nat) (h : i < n) :
+    (a.mapIdx f)[i] = f i (a[i]'(by simp_all)) := by
+  rcases a with ⟨a, rfl⟩
+  simp
+
+@[simp] theorem getElem?_mapIdx (f : Nat → α → β) (a : Vector α n) (i : Nat) :
+    (a.mapIdx f)[i]? = a[i]?.map (f i) := by
+  rcases a with ⟨a, rfl⟩
+  simp
+
+end Vector
+
+namespace Array
+
+@[simp] theorem mapFinIdx_toVector (l : Array α) (f : (i : Nat) → α → (h : i < l.size) → β) :
+    l.toVector.mapFinIdx f = (l.mapFinIdx f).toVector.cast (by simp) := by
+  ext <;> simp
+
+@[simp] theorem mapIdx_toVector (f : Nat → α → β) (l : Array α) :
+    l.toVector.mapIdx f = (l.mapIdx f).toVector.cast (by simp) := by
+  ext <;> simp
+
+end Array
+
+namespace Vector
+
+/-! ### zipWithIndex -/
+
+@[simp] theorem toList_zipWithIndex (a : Vector α n) :
+    a.zipWithIndex.toList = a.toList.enum.map (fun (i, a) => (a, i)) := by
+  rcases a with ⟨a, rfl⟩
+  simp
+
+@[simp] theorem getElem_zipWithIndex (a : Vector α n) (i : Nat) (h : i < n) :
+    (a.zipWithIndex)[i] = (a[i]'(by simp_all), i) := by
+  rcases a with ⟨a, rfl⟩
+  simp
+
+@[simp] theorem zipWithIndex_toVector {l : Array α} :
+    l.toVector.zipWithIndex = l.zipWithIndex.toVector.cast (by simp) := by
+  ext <;> simp
+
+theorem mk_mem_zipWithIndex_iff_getElem? {x : α} {i : Nat} {l : Vector α n} :
+    (x, i) ∈ l.zipWithIndex ↔ l[i]? = x := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.mk_mem_zipWithIndex_iff_getElem?]
+
+theorem mem_enum_iff_getElem? {x : α × Nat} {l : Vector α n} :
+    x ∈ l.zipWithIndex ↔ l[x.2]? = some x.1 :=
+  mk_mem_zipWithIndex_iff_getElem?
+
+/-! ### mapFinIdx -/
+
+@[congr] theorem mapFinIdx_congr {xs ys : Vector α n} (w : xs = ys)
+    (f : (i : Nat) → α → (h : i < n) → β) :
+    mapFinIdx xs f = mapFinIdx ys f := by
+  subst w
+  rfl
+
+@[simp]
+theorem mapFinIdx_empty {f : (i : Nat) → α → (h : i < 0) → β} : mapFinIdx #v[] f = #v[] :=
+  rfl
+
+theorem mapFinIdx_eq_ofFn {as : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} :
+    as.mapFinIdx f = Vector.ofFn fun i : Fin n => f i as[i] i.2 := by
+  rcases as with ⟨as, rfl⟩
+  simp [Array.mapFinIdx_eq_ofFn]
+
+theorem mapFinIdx_append {K : Vector α n} {L : Vector α m} {f : (i : Nat) → α → (h : i < n + m) → β} :
+    (K ++ L).mapFinIdx f =
+      K.mapFinIdx (fun i a h => f i a (by omega)) ++
+        L.mapFinIdx (fun i a h => f (i + n) a (by omega)) := by
+  rcases K with ⟨K, rfl⟩
+  rcases L with ⟨L, rfl⟩
+  simp [Array.mapFinIdx_append]
+
+@[simp]
+theorem mapFinIdx_push {l : Vector α n} {a : α} {f : (i : Nat) → α → (h : i < n + 1) → β} :
+    mapFinIdx (l.push a) f =
+      (mapFinIdx l (fun i a h => f i a (by omega))).push (f l.size a (by simp)) := by
+  simp [← append_singleton, mapFinIdx_append]
+
+theorem mapFinIdx_singleton {a : α} {f : (i : Nat) → α → (h : i < 1) → β} :
+    #v[a].mapFinIdx f = #v[f 0 a (by simp)] := by
+  simp
+
+-- FIXME this lemma can't be stated until we've aligned `List/Array/Vector.attach`:
+-- theorem mapFinIdx_eq_zipWithIndex_map {l : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} :
+--     l.mapFinIdx f = l.zipWithIndex.attach.map
+--       fun ⟨⟨x, i⟩, m⟩ =>
+--         f i x (by simp [mk_mem_zipWithIndex_iff_getElem?, getElem?_eq_some_iff] at m; exact m.1) := by
+--   ext <;> simp
+
+theorem exists_of_mem_mapFinIdx {b : β} {l : Vector α n} {f : (i : Nat) → α → (h : i < n) → β}
+    (h : b ∈ l.mapFinIdx f) : ∃ (i : Nat) (h : i < n), f i l[i] h = b := by
+  rcases l with ⟨l, rfl⟩
+  exact List.exists_of_mem_mapFinIdx (by simpa using h)
+
+@[simp] theorem mem_mapFinIdx {b : β} {l : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} :
+    b ∈ l.mapFinIdx f ↔ ∃ (i : Nat) (h : i < n), f i l[i] h = b := by
+  rcases l with ⟨l, rfl⟩
+  simp
+
+theorem mapFinIdx_eq_iff {l : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} :
+    l.mapFinIdx f = l' ↔ ∀ (i : Nat) (h : i < n), l'[i] = f i l[i] h := by
+  rcases l with ⟨l, rfl⟩
+  rcases l' with ⟨l', h⟩
+  simp [mapFinIdx_mk, eq_mk, getElem_mk, Array.mapFinIdx_eq_iff, h]
+
+@[simp] theorem mapFinIdx_eq_singleton_iff {l : Vector α 1} {f : (i : Nat) → α → (h : i < 1) → β} {b : β} :
+    l.mapFinIdx f = #v[b] ↔ ∃ (a : α), l = #v[a] ∧ f 0 a (by omega) = b := by
+  rcases l with ⟨l, h⟩
+  simp only [mapFinIdx_mk, eq_mk, Array.mapFinIdx_eq_singleton_iff]
+  constructor
+  · rintro ⟨a, rfl, rfl⟩
+    exact ⟨a, by simp⟩
+  · rintro ⟨a, rfl, rfl⟩
+    exact ⟨a, by simp⟩
+
+theorem mapFinIdx_eq_append_iff {l : Vector α (n + m)} {f : (i : Nat) → α → (h : i < n + m) → β}
+    {l₁ : Vector β n} {l₂ : Vector β m} :
+    l.mapFinIdx f = l₁ ++ l₂ ↔
+      ∃ (l₁' : Vector α n) (l₂' : Vector α m), l = l₁' ++ l₂' ∧
+        l₁'.mapFinIdx (fun i a h => f i a (by omega)) = l₁ ∧
+        l₂'.mapFinIdx (fun i a h => f (i + n) a (by omega)) = l₂ := by
+  rcases l with ⟨l, h⟩
+  rcases l₁ with ⟨l₁, rfl⟩
+  rcases l₂ with ⟨l₂, rfl⟩
+  simp only [mapFinIdx_mk, mk_append_mk, eq_mk, Array.mapFinIdx_eq_append_iff, toArray_mapFinIdx,
+    mk_eq, toArray_append, exists_and_left, exists_prop]
+  constructor
+  · rintro ⟨l₁', l₂', rfl, h₁, h₂⟩
+    have h₁' := congrArg Array.size h₁
+    have h₂' := congrArg Array.size h₂
+    simp only [Array.size_mapFinIdx] at h₁' h₂'
+    exact ⟨⟨l₁', h₁'⟩, ⟨l₂', h₂'⟩, by simp_all⟩
+  · rintro ⟨⟨l₁, s₁⟩, ⟨l₂, s₂⟩, rfl, h₁, h₂⟩
+    refine ⟨l₁, l₂, by simp_all⟩
+
+theorem mapFinIdx_eq_push_iff {l : Vector α (n + 1)} {b : β} {f : (i : Nat) → α → (h : i < n + 1) → β} {l₂ : Vector β n} :
+    l.mapFinIdx f = l₂.push b ↔
+      ∃ (l₁ : Vector α n) (a : α), l = l₁.push a ∧
+        l₁.mapFinIdx (fun i a h => f i a (by omega)) = l₂ ∧ b = f n a (by omega) := by
+  rcases l with ⟨l, h⟩
+  rcases l₂ with ⟨l₂, rfl⟩
+  simp only [mapFinIdx_mk, push_mk, eq_mk, Array.mapFinIdx_eq_push_iff, mk_eq, toArray_push,
+    toArray_mapFinIdx]
+  constructor
+  · rintro ⟨l₁, a, rfl, h₁, rfl⟩
+    simp only [Array.size_push, Nat.add_right_cancel_iff] at h
+    exact ⟨⟨l₁, h⟩, a, by simp_all⟩
+  · rintro ⟨⟨l₁, h⟩, a, rfl, h₁, rfl⟩
+    exact ⟨l₁, a, by simp_all⟩
+
+theorem mapFinIdx_eq_mapFinIdx_iff {l : Vector α n} {f g : (i : Nat) → α → (h : i < n) → β} :
+    l.mapFinIdx f = l.mapFinIdx g ↔ ∀ (i : Nat) (h : i < n), f i l[i] h = g i l[i] h := by
+  rw [eq_comm, mapFinIdx_eq_iff]
+  simp
+
+@[simp] theorem mapFinIdx_mapFinIdx {l : Vector α n}
+    {f : (i : Nat) → α → (h : i < n) → β}
+    {g : (i : Nat) → β → (h : i < n) → γ} :
+    (l.mapFinIdx f).mapFinIdx g = l.mapFinIdx (fun i a h => g i (f i a h) h) := by
+  simp [mapFinIdx_eq_iff]
+
+theorem mapFinIdx_eq_mkVector_iff {l : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} {b : β} :
+    l.mapFinIdx f = mkVector n b ↔ ∀ (i : Nat) (h : i < n), f i l[i] h = b := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.mapFinIdx_eq_mkArray_iff]
+
+@[simp] theorem mapFinIdx_reverse {l : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} :
+    l.reverse.mapFinIdx f = (l.mapFinIdx (fun i a h => f (n - 1 - i) a (by omega))).reverse := by
+  rcases l with ⟨l, rfl⟩
+  simp
+
+/-! ### mapIdx -/
+
+@[simp]
+theorem mapIdx_empty {f : Nat → α → β} : mapIdx f #v[] = #v[] :=
+  rfl
+
+@[simp] theorem mapFinIdx_eq_mapIdx {l : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} {g : Nat → α → β}
+    (h : ∀ (i : Nat) (h : i < n), f i l[i] h = g i l[i]) :
+    l.mapFinIdx f = l.mapIdx g := by
+  simp_all [mapFinIdx_eq_iff]
+
+theorem mapIdx_eq_mapFinIdx {l : Vector α n} {f : Nat → α → β} :
+    l.mapIdx f = l.mapFinIdx (fun i a _ => f i a) := by
+  simp [mapFinIdx_eq_mapIdx]
+
+theorem mapIdx_eq_zipWithIndex_map {l : Vector α n} {f : Nat → α → β} :
+    l.mapIdx f = l.zipWithIndex.map fun ⟨a, i⟩ => f i a := by
+  ext <;> simp
+
+theorem mapIdx_append {K : Vector α n} {L : Vector α m} :
+    (K ++ L).mapIdx f = K.mapIdx f ++ L.mapIdx fun i => f (i + K.size) := by
+  rcases K with ⟨K, rfl⟩
+  rcases L with ⟨L, rfl⟩
+  simp [Array.mapIdx_append]
+
+@[simp]
+theorem mapIdx_push {l : Vector α n} {a : α} :
+    mapIdx f (l.push a) = (mapIdx f l).push (f l.size a) := by
+  simp [← append_singleton, mapIdx_append]
+
+theorem mapIdx_singleton {a : α} : mapIdx f #v[a] = #v[f 0 a] := by
+  simp
+
+theorem exists_of_mem_mapIdx {b : β} {l : Vector α n}
+    (h : b ∈ l.mapIdx f) : ∃ (i : Nat) (h : i < n), f i l[i] = b := by
+  rw [mapIdx_eq_mapFinIdx] at h
+  simpa [Fin.exists_iff] using exists_of_mem_mapFinIdx h
+
+@[simp] theorem mem_mapIdx {b : β} {l : Vector α n} :
+    b ∈ l.mapIdx f ↔ ∃ (i : Nat) (h : i < n), f i l[i] = b := by
+  constructor
+  · intro h
+    exact exists_of_mem_mapIdx h
+  · rintro ⟨i, h, rfl⟩
+    rw [mem_iff_getElem]
+    exact ⟨i, by simpa using h, by simp⟩
+
+theorem mapIdx_eq_push_iff {l : Vector α (n + 1)} {b : β} :
+    mapIdx f l = l₂.push b ↔
+      ∃ (a : α) (l₁ : Vector α n), l = l₁.push a ∧ mapIdx f l₁ = l₂ ∧ f l₁.size a = b := by
+  rw [mapIdx_eq_mapFinIdx, mapFinIdx_eq_push_iff]
+  simp only [mapFinIdx_eq_mapIdx, exists_and_left, exists_prop]
+  constructor
+  · rintro ⟨l₁, a, rfl, rfl, rfl⟩
+    exact ⟨a, l₁, by simp⟩
+  · rintro ⟨a, l₁, rfl, rfl, rfl⟩
+    exact ⟨l₁, a, rfl, by simp⟩
+
+@[simp] theorem mapIdx_eq_singleton_iff {l : Vector α 1} {f : Nat → α → β} {b : β} :
+    mapIdx f l = #v[b] ↔ ∃ (a : α), l = #v[a] ∧ f 0 a = b := by
+  rcases l with ⟨l⟩
+  simp
+
+theorem mapIdx_eq_append_iff {l : Vector α (n + m)} {f : Nat → α → β} {l₁ : Vector β n} {l₂ : Vector β m} :
+    mapIdx f l = l₁ ++ l₂ ↔
+      ∃ (l₁' : Vector α n) (l₂' : Vector α m), l = l₁' ++ l₂' ∧
+        l₁'.mapIdx f = l₁ ∧
+        l₂'.mapIdx (fun i => f (i + l₁'.size)) = l₂ := by
+  rcases l with ⟨l, h⟩
+  rcases l₁ with ⟨l₁, rfl⟩
+  rcases l₂ with ⟨l₂, rfl⟩
+  rw [mapIdx_eq_mapFinIdx, mapFinIdx_eq_append_iff]
+  simp
+
+theorem mapIdx_eq_iff {l : Vector α n} :
+    mapIdx f l = l' ↔ ∀ (i : Nat) (h : i < n), f i l[i] = l'[i] := by
+  rcases l with ⟨l, rfl⟩
+  rcases l' with ⟨l', h⟩
+  simp only [mapIdx_mk, eq_mk, Array.mapIdx_eq_iff, getElem_mk]
+  constructor
+  · rintro h' i h
+    specialize h' i
+    simp_all
+  · intro h' i
+    specialize h' i
+    by_cases w : i < l.size
+    · specialize h' w
+      simp_all
+    · simp only [Nat.not_lt] at w
+      simp_all [Array.getElem?_eq_none_iff.mpr w]
+
+theorem mapIdx_eq_mapIdx_iff {l : Vector α n} :
+    mapIdx f l = mapIdx g l ↔ ∀ (i : Nat) (h : i < n), f i l[i] = g i l[i] := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.mapIdx_eq_mapIdx_iff]
+
+@[simp] theorem mapIdx_set {l : Vector α n} {i : Nat} {h : i < n} {a : α} :
+    (l.set i a).mapIdx f = (l.mapIdx f).set i (f i a) (by simpa) := by
+  rcases l with ⟨l, rfl⟩
+  simp
+
+@[simp] theorem mapIdx_setIfInBounds {l : Vector α n} {i : Nat} {a : α} :
+    (l.setIfInBounds i a).mapIdx f = (l.mapIdx f).setIfInBounds i (f i a) := by
+  rcases l with ⟨l, rfl⟩
+  simp
+
+@[simp] theorem back?_mapIdx {l : Vector α n} {f : Nat → α → β} :
+    (mapIdx f l).back? = (l.back?).map (f (l.size - 1)) := by
+  rcases l with ⟨l, rfl⟩
+  simp
+
+@[simp] theorem back_mapIdx [NeZero n] {l : Vector α n} {f : Nat → α → β} :
+    (mapIdx f l).back = f (l.size - 1) (l.back) := by
+  rcases l with ⟨l, rfl⟩
+  simp
+
+@[simp] theorem mapIdx_mapIdx {l : Vector α n} {f : Nat → α → β} {g : Nat → β → γ} :
+    (l.mapIdx f).mapIdx g = l.mapIdx (fun i => g i ∘ f i) := by
+  simp [mapIdx_eq_iff]
+
+theorem mapIdx_eq_mkVector_iff {l : Vector α n} {f : Nat → α → β} {b : β} :
+    mapIdx f l = mkVector n b ↔ ∀ (i : Nat) (h : i < n), f i l[i] = b := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.mapIdx_eq_mkArray_iff]
+
+@[simp] theorem mapIdx_reverse {l : Vector α n} {f : Nat → α → β} :
+    l.reverse.mapIdx f = (mapIdx (fun i => f (l.size - 1 - i)) l).reverse := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.mapIdx_reverse]
+
+end Vector