feat: lemmas about indexing and membership for Vector

src/Init/Data/Array/Lemmas.lean

@@ -174,7 +174,7 @@ theorem some_eq_getElem?_iff {a : Array α} : some b = a[i]? ↔ ∃ h : i < a.s
     (a[i]? = some a[i]) ↔ True := by
   simp [h]
 
-theorem getElem_eq_iff {a : Array α} {n : Nat} {h : n < a.size} : a[n] = x ↔ a[n]? = some x := by
+theorem getElem_eq_iff {a : Array α} {i : Nat} {h : i < a.size} : a[i] = x ↔ a[i]? = some x := by
   simp only [getElem?_eq_some_iff]
   exact ⟨fun w => ⟨h, w⟩, fun h => h.2⟩
 
@@ -190,7 +190,7 @@ theorem getD_getElem? (a : Array α) (i : Nat) (d : α) :
     have p : i ≥ a.size := Nat.le_of_not_gt h
     simp [getElem?_eq_none p, h]
 
-@[simp] theorem getElem?_empty {n : Nat} : (#[] : Array α)[n]? = none := rfl
+@[simp] theorem getElem?_empty {i : Nat} : (#[] : Array α)[i]? = none := rfl
 
 theorem getElem_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
     have : i < (a.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]
@@ -251,19 +251,19 @@ theorem eq_empty_iff_forall_not_mem {l : Array α} : l = #[] ↔ ∀ a, a ∉ l
   cases l
   simp [List.eq_nil_iff_forall_not_mem]
 
-@[simp] theorem mem_dite_nil_left {x : α} [Decidable p] {l : ¬ p → Array α} :
+@[simp] theorem mem_dite_empty_left {x : α} [Decidable p] {l : ¬ p → Array α} :
     (x ∈ if h : p then #[] else l h) ↔ ∃ h : ¬ p, x ∈ l h := by
   split <;> simp_all
 
-@[simp] theorem mem_dite_nil_right {x : α} [Decidable p] {l : p → Array α} :
+@[simp] theorem mem_dite_empty_right {x : α} [Decidable p] {l : p → Array α} :
     (x ∈ if h : p then l h else #[]) ↔ ∃ h : p, x ∈ l h := by
   split <;> simp_all
 
-@[simp] theorem mem_ite_nil_left {x : α} [Decidable p] {l : Array α} :
+@[simp] theorem mem_ite_empty_left {x : α} [Decidable p] {l : Array α} :
     (x ∈ if p then #[] else l) ↔ ¬ p ∧ x ∈ l := by
   split <;> simp_all
 
-@[simp] theorem mem_ite_nil_right {x : α} [Decidable p] {l : Array α} :
+@[simp] theorem mem_ite_empty_right {x : α} [Decidable p] {l : Array α} :
     (x ∈ if p then l else #[]) ↔ p ∧ x ∈ l := by
   split <;> simp_all
 
@@ -290,7 +290,7 @@ theorem forall_mem_empty (p : α → Prop) : ∀ (x) (_ : x ∈ #[]), p x := nof
 
 theorem exists_mem_push {p : α → Prop} {a : α} {xs : Array α} :
     (∃ x, ∃ _ : x ∈ xs.push a, p x) ↔ p a ∨ ∃ x, ∃ _ : x ∈ xs, p x := by
-  simp
+  simp only [mem_push, exists_prop]
   constructor
   · rintro ⟨x, (h | rfl), h'⟩
     · exact .inr ⟨x, h, h'⟩
@@ -319,7 +319,7 @@ theorem eq_or_ne_mem_of_mem {a b : α} {l : Array α} (h' : a ∈ l.push b) :
   if h : a = b then
     exact .inl h
   else
-    simp [h] at h'
+    simp only [mem_push, h, or_false] at h'
     exact .inr ⟨h, h'⟩
 
 theorem ne_empty_of_mem {a : α} {l : Array α} (h : a ∈ l) : l ≠ #[] := by
@@ -343,27 +343,27 @@ theorem not_mem_push_of_ne_of_not_mem {a y : α} {l : Array α} : a ≠ y → a
 theorem ne_and_not_mem_of_not_mem_push {a y : α} {l : Array α} : a ∉ l.push y → a ≠ y ∧ a ∉ l := by
   simp +contextual
 
-theorem getElem_of_mem {a} {l : Array α} (h : a ∈ l) : ∃ (n : Nat) (h : n < l.size), l[n]'h = a := by
+theorem getElem_of_mem {a} {l : Array α} (h : a ∈ l) : ∃ (i : Nat) (h : i < l.size), l[i]'h = a := by
   cases l
   simp [List.getElem_of_mem (by simpa using h)]
 
-theorem getElem?_of_mem {a} {l : Array α} (h : a ∈ l) : ∃ n : Nat, l[n]? = some a :=
+theorem getElem?_of_mem {a} {l : Array α} (h : a ∈ l) : ∃ i : Nat, l[i]? = some a :=
   let ⟨n, _, e⟩ := getElem_of_mem h; ⟨n, e ▸ getElem?_eq_getElem _⟩
 
-theorem mem_of_getElem? {l : Array α} {n : Nat} {a : α} (e : l[n]? = some a) : a ∈ l :=
+theorem mem_of_getElem? {l : Array α} {i : Nat} {a : α} (e : l[i]? = some a) : a ∈ l :=
   let ⟨_, e⟩ := getElem?_eq_some_iff.1 e; e ▸ getElem_mem ..
 
-theorem mem_iff_getElem {a} {l : Array α} : a ∈ l ↔ ∃ (n : Nat) (h : n < l.size), l[n]'h = a :=
+theorem mem_iff_getElem {a} {l : Array α} : a ∈ l ↔ ∃ (i : Nat) (h : i < l.size), l[i]'h = a :=
   ⟨getElem_of_mem, fun ⟨_, _, e⟩ => e ▸ getElem_mem ..⟩
 
-theorem mem_iff_getElem? {a} {l : Array α} : a ∈ l ↔ ∃ n : Nat, l[n]? = some a := by
+theorem mem_iff_getElem? {a} {l : Array α} : a ∈ l ↔ ∃ i : Nat, l[i]? = some a := by
   simp [getElem?_eq_some_iff, mem_iff_getElem]
 
 theorem forall_getElem {l : Array α} {p : α → Prop} :
-    (∀ (n : Nat) h, p (l[n]'h)) ↔ ∀ a, a ∈ l → p a := by
+    (∀ (i : Nat) h, p (l[i]'h)) ↔ ∀ a, a ∈ l → p a := by
   cases l; simp [List.forall_getElem]
 
-/-! ### isEmpty-/
+/-! ### isEmpty -/
 
 @[simp] theorem isEmpty_toList {l : Array α} : l.toList.isEmpty = l.isEmpty := by
   rcases l with ⟨_ | _⟩ <;> simp
@@ -718,9 +718,6 @@ theorem all_push [BEq α] {as : Array α} {a : α} {p : α → Bool} :
 
 /-! ### set -/
 
-
-/-! # set -/
-
 @[simp] theorem getElem_set_self (a : Array α) (i : Nat) (h : i < a.size) (v : α) {j : Nat}
       (eq : i = j) (p : j < (a.set i v).size) :
     (a.set i v)[j]'p = v := by
@@ -786,7 +783,10 @@ theorem mem_or_eq_of_mem_set
   cases as
   simpa using List.mem_or_eq_of_mem_set (by simpa using h)
 
-/-! # setIfInBounds -/
+@[simp] theorem toList_set (a : Array α) (i x h) :
+    (a.set i x).toList = a.toList.set i x := rfl
+
+/-! ### setIfInBounds -/
 
 @[simp] theorem set!_is_setIfInBounds : @set! = @setIfInBounds := rfl
 
@@ -874,6 +874,15 @@ theorem mem_or_eq_of_mem_setIfInBounds
   by_cases h : i < a.size <;>
     simp [setIfInBounds, Nat.not_lt_of_le, h,  getD_getElem?]
 
+@[simp] theorem toList_setIfInBounds (a : Array α) (i x) :
+    (a.setIfInBounds i x).toList = a.toList.set i x := by
+  simp only [setIfInBounds]
+  split <;> rename_i h
+  · simp
+  · simp [List.set_eq_of_length_le (by simpa using h)]
+
+/-! Content below this point has not yet been aligned with `List`. -/
+
 theorem singleton_inj : #[a] = #[b] ↔ a = b := by
   simp
 
@@ -1000,7 +1009,7 @@ theorem getElem?_len_le (a : Array α) {i : Nat} (h : a.size ≤ i) : a[i]? = no
 
 @[deprecated getD_getElem? (since := "2024-12-11")] abbrev getD_get? := @getD_getElem?
 
-@[simp] theorem getD_eq_get? (a : Array α) (n d) : a.getD n d = (a[n]?).getD d := by
+@[simp] theorem getD_eq_get? (a : Array α) (i d) : a.getD i d = (a[i]?).getD d := by
   simp only [getD, get_eq_getElem, get?_eq_getElem?]; split <;> simp [getD_getElem?, *]
 
 theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default := rfl
@@ -1088,22 +1097,6 @@ theorem getElem?_mkArray (n : Nat) (v : α) (i : Nat) :
 
 theorem not_mem_nil (a : α) : ¬ a ∈ #[] := nofun
 
-@[simp] theorem mem_dite_empty_left {x : α} [Decidable p] {l : ¬ p → Array α} :
-    (x ∈ if h : p then #[] else l h) ↔ ∃ h : ¬ p, x ∈ l h := by
-  split <;> simp_all
-
-@[simp] theorem mem_dite_empty_right {x : α} [Decidable p] {l : p → Array α} :
-    (x ∈ if h : p then l h else #[]) ↔ ∃ h : p, x ∈ l h := by
-  split <;> simp_all
-
-@[simp] theorem mem_ite_empty_left {x : α} [Decidable p] {l : Array α} :
-    (x ∈ if p then #[] else l) ↔ ¬ p ∧ x ∈ l := by
-  split <;> simp_all
-
-@[simp] theorem mem_ite_empty_right {x : α} [Decidable p] {l : Array α} :
-    (x ∈ if p then l else #[]) ↔ p ∧ x ∈ l := by
-  split <;> simp_all
-
 /-! # get lemmas -/
 
 theorem lt_of_getElem {x : α} {a : Array α} {idx : Nat} {hidx : idx < a.size} (_ : a[idx] = x) :
@@ -1160,8 +1153,6 @@ theorem getElem?_push_eq (a : Array α) (x : α) : (a.push x)[a.size]? = some x
 
 @[deprecated getElem?_size (since := "2024-10-21")] abbrev get?_size := @getElem?_size
 
-@[simp] theorem toList_set (a : Array α) (i v h) : (a.set i v).toList = a.toList.set i v := rfl
-
 theorem get_set_eq (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
     (a.set i v h)[i]'(by simp [h]) = v := by
   simp only [set, ← getElem_toList, List.getElem_set_self]
@@ -1724,21 +1715,21 @@ theorem getElem_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle :
   conv => rhs; rw [← List.getElem_append_right (h₁ := hle) (h₂ := h')]
   apply List.get_of_eq; rw [toList_append]
 
-theorem getElem?_append_left {as bs : Array α} {n : Nat} (hn : n < as.size) :
-    (as ++ bs)[n]? = as[n]? := by
-  have hn' : n < (as ++ bs).size := Nat.lt_of_lt_of_le hn <|
+theorem getElem?_append_left {as bs : Array α} {i : Nat} (hn : i < as.size) :
+    (as ++ bs)[i]? = as[i]? := by
+  have hn' : i < (as ++ bs).size := Nat.lt_of_lt_of_le hn <|
     size_append .. ▸ Nat.le_add_right ..
   simp_all [getElem?_eq_getElem, getElem_append]
 
-theorem getElem?_append_right {as bs : Array α} {n : Nat} (h : as.size ≤ n) :
-    (as ++ bs)[n]? = bs[n - as.size]? := by
+theorem getElem?_append_right {as bs : Array α} {i : Nat} (h : as.size ≤ i) :
+    (as ++ bs)[i]? = bs[i - as.size]? := by
   cases as
   cases bs
   simp at h
   simp [List.getElem?_append_right, h]
 
-theorem getElem?_append {as bs : Array α} {n : Nat} :
-    (as ++ bs)[n]? = if n < as.size then as[n]? else bs[n - as.size]? := by
+theorem getElem?_append {as bs : Array α} {i : Nat} :
+    (as ++ bs)[i]? = if i < as.size then as[i]? else bs[i - as.size]? := by
   split <;> rename_i h
   · exact getElem?_append_left h
   · exact getElem?_append_right (by simpa using h)

src/Init/Data/List/Lemmas.lean

@@ -191,50 +191,50 @@ We simplify away `getD`, replacing `getD l n a` with `(l[n]?).getD a`.
 Because of this, there is only minimal API for `getD`.
 -/
 
-@[simp] theorem getD_eq_getElem?_getD (l) (n) (a : α) : getD l n a = (l[n]?).getD a := by
+@[simp] theorem getD_eq_getElem?_getD (l) (i) (a : α) : getD l i a = (l[i]?).getD a := by
   simp [getD]
 
 /-! ### get!
 
-We simplify `l.get! n` to `l[n]!`.
+We simplify `l.get! i` to `l[i]!`.
 -/
 
-theorem get!_eq_getD [Inhabited α] : ∀ (l : List α) n, l.get! n = l.getD n default
+theorem get!_eq_getD [Inhabited α] : ∀ (l : List α) i, l.get! i = l.getD i default
   | [], _      => rfl
   | _a::_, 0   => rfl
   | _a::l, n+1 => get!_eq_getD l n
 
-@[simp] theorem get!_eq_getElem! [Inhabited α] (l : List α) (n) : l.get! n = l[n]! := by
+@[simp] theorem get!_eq_getElem! [Inhabited α] (l : List α) (i) : l.get! i = l[i]! := by
   simp [get!_eq_getD]
   rfl
 
 /-! ### getElem!
 
-We simplify `l[n]!` to `(l[n]?).getD default`.
+We simplify `l[i]!` to `(l[i]?).getD default`.
 -/
 
-@[simp] theorem getElem!_eq_getElem?_getD [Inhabited α] (l : List α) (n : Nat) :
-    l[n]! = (l[n]?).getD (default : α) := by
+@[simp] theorem getElem!_eq_getElem?_getD [Inhabited α] (l : List α) (i : Nat) :
+    l[i]! = (l[i]?).getD (default : α) := by
   simp only [getElem!_def]
   split <;> simp_all
 
 /-! ### getElem? and getElem -/
 
-@[simp] theorem getElem?_eq_none_iff : l[n]? = none ↔ length l ≤ n := by
+@[simp] theorem getElem?_eq_none_iff : l[i]? = none ↔ length l ≤ i := by
   simp only [← get?_eq_getElem?, get?_eq_none_iff]
 
-@[simp] theorem none_eq_getElem?_iff {l : List α} {n : Nat} : none = l[n]? ↔ length l ≤ n := by
+@[simp] theorem none_eq_getElem?_iff {l : List α} {i : Nat} : none = l[i]? ↔ length l ≤ i := by
   simp [eq_comm (a := none)]
 
-theorem getElem?_eq_none (h : length l ≤ n) : l[n]? = none := getElem?_eq_none_iff.mpr h
+theorem getElem?_eq_none (h : length l ≤ i) : l[i]? = none := getElem?_eq_none_iff.mpr h
 
-@[simp] theorem getElem?_eq_getElem {l : List α} {n} (h : n < l.length) : l[n]? = some l[n] :=
+@[simp] theorem getElem?_eq_getElem {l : List α} {i} (h : i < l.length) : l[i]? = some l[i] :=
   getElem?_pos ..
 
-theorem getElem?_eq_some_iff {l : List α} : l[n]? = some a ↔ ∃ h : n < l.length, l[n] = a := by
+theorem getElem?_eq_some_iff {l : List α} : l[i]? = some a ↔ ∃ h : i < l.length, l[i] = a := by
   simp only [← get?_eq_getElem?, get?_eq_some_iff, get_eq_getElem]
 
-theorem some_eq_getElem?_iff {l : List α} : some a = l[n]? ↔ ∃ h : n < l.length, l[n] = a := by
+theorem some_eq_getElem?_iff {l : List α} : some a = l[i]? ↔ ∃ h : i < l.length, l[i] = a := by
   rw [eq_comm, getElem?_eq_some_iff]
 
 @[simp] theorem some_getElem_eq_getElem?_iff (xs : List α) (i : Nat) (h : i < xs.length) :
@@ -245,7 +245,7 @@ theorem some_eq_getElem?_iff {l : List α} : some a = l[n]? ↔ ∃ h : n < l.le
     (xs[i]? = some xs[i]) ↔ True := by
   simp [h]
 
-theorem getElem_eq_iff {l : List α} {n : Nat} {h : n < l.length} : l[n] = x ↔ l[n]? = some x := by
+theorem getElem_eq_iff {l : List α} {i : Nat} {h : i < l.length} : l[i] = x ↔ l[i]? = some x := by
   simp only [getElem?_eq_some_iff]
   exact ⟨fun w => ⟨h, w⟩, fun h => h.2⟩
 
@@ -261,7 +261,7 @@ theorem getD_getElem? (l : List α) (i : Nat) (d : α) :
     have p : i ≥ l.length := Nat.le_of_not_gt h
     simp [getElem?_eq_none p, h]
 
-@[simp] theorem getElem?_nil {n : Nat} : ([] : List α)[n]? = none := rfl
+@[simp] theorem getElem?_nil {i : Nat} : ([] : List α)[i]? = none := rfl
 
 theorem getElem_cons {l : List α} (w : i < (a :: l).length) :
     (a :: l)[i] =
@@ -270,7 +270,7 @@ theorem getElem_cons {l : List α} (w : i < (a :: l).length) :
 
 theorem getElem?_cons_zero {l : List α} : (a::l)[0]? = some a := by simp
 
-@[simp] theorem getElem?_cons_succ {l : List α} : (a::l)[n+1]? = l[n]? := by
+@[simp] theorem getElem?_cons_succ {l : List α} : (a::l)[i+1]? = l[i]? := by
   simp only [← get?_eq_getElem?]
   rfl
 
@@ -297,11 +297,11 @@ theorem getElem_zero {l : List α} (h : 0 < l.length) : l[0] = l.head (length_po
   match l, h with
   | _ :: _, _ => rfl
 
-@[ext] theorem ext_getElem? {l₁ l₂ : List α} (h : ∀ n : Nat, l₁[n]? = l₂[n]?) : l₁ = l₂ :=
+@[ext] theorem ext_getElem? {l₁ l₂ : List α} (h : ∀ i : Nat, l₁[i]? = l₂[i]?) : l₁ = l₂ :=
   ext_get? fun n => by simp_all
 
 theorem ext_getElem {l₁ l₂ : List α} (hl : length l₁ = length l₂)
-    (h : ∀ (n : Nat) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁[n]'h₁ = l₂[n]'h₂) : l₁ = l₂ :=
+    (h : ∀ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length), l₁[i]'h₁ = l₂[i]'h₂) : l₁ = l₂ :=
   ext_getElem? fun n =>
     if h₁ : n < length l₁ then by
       simp_all [getElem?_eq_getElem]
@@ -422,25 +422,25 @@ theorem not_mem_cons_of_ne_of_not_mem {a y : α} {l : List α} : a ≠ y → a
 theorem ne_and_not_mem_of_not_mem_cons {a y : α} {l : List α} : a ∉ y :: l → a ≠ y ∧ a ∉ l :=
   fun p => ⟨ne_of_not_mem_cons p, not_mem_of_not_mem_cons p⟩
 
-theorem getElem_of_mem : ∀ {a} {l : List α}, a ∈ l → ∃ (n : Nat) (h : n < l.length), l[n]'h = a
+theorem getElem_of_mem : ∀ {a} {l : List α}, a ∈ l → ∃ (i : Nat) (h : i < l.length), l[i]'h = a
   | _, _ :: _, .head .. => ⟨0, Nat.succ_pos _, rfl⟩
-  | _, _ :: _, .tail _ m => let ⟨n, h, e⟩ := getElem_of_mem m; ⟨n+1, Nat.succ_lt_succ h, e⟩
+  | _, _ :: _, .tail _ m => let ⟨i, h, e⟩ := getElem_of_mem m; ⟨i+1, Nat.succ_lt_succ h, e⟩
 
-theorem getElem?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n : Nat, l[n]? = some a := by
+theorem getElem?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ i : Nat, l[i]? = some a := by
   let ⟨n, _, e⟩ := getElem_of_mem h
   exact ⟨n, e ▸ getElem?_eq_getElem _⟩
 
-theorem mem_of_getElem? {l : List α} {n : Nat} {a : α} (e : l[n]? = some a) : a ∈ l :=
+theorem mem_of_getElem? {l : List α} {i : Nat} {a : α} (e : l[i]? = some a) : a ∈ l :=
   let ⟨_, e⟩ := getElem?_eq_some_iff.1 e; e ▸ getElem_mem ..
 
-theorem mem_iff_getElem {a} {l : List α} : a ∈ l ↔ ∃ (n : Nat) (h : n < l.length), l[n]'h = a :=
+theorem mem_iff_getElem {a} {l : List α} : a ∈ l ↔ ∃ (i : Nat) (h : i < l.length), l[i]'h = a :=
   ⟨getElem_of_mem, fun ⟨_, _, e⟩ => e ▸ getElem_mem ..⟩
 
-theorem mem_iff_getElem? {a} {l : List α} : a ∈ l ↔ ∃ n : Nat, l[n]? = some a := by
+theorem mem_iff_getElem? {a} {l : List α} : a ∈ l ↔ ∃ i : Nat, l[i]? = some a := by
   simp [getElem?_eq_some_iff, mem_iff_getElem]
 
 theorem forall_getElem {l : List α} {p : α → Prop} :
-    (∀ (n : Nat) h, p (l[n]'h)) ↔ ∀ a, a ∈ l → p a := by
+    (∀ (i : Nat) h, p (l[i]'h)) ↔ ∀ a, a ∈ l → p a := by
   induction l with
   | nil => simp
   | cons a l ih =>
@@ -593,10 +593,10 @@ theorem getElem?_set_self' {l : List α} {i : Nat} {a : α} :
     simp_all
   · rw [getElem?_eq_none (by simp_all), getElem?_eq_none (by simp_all)]
 
-theorem getElem_set {l : List α} {m n} {a} (h) :
-    (set l m a)[n]'h = if m = n then a else l[n]'(length_set .. ▸ h) := by
-  if h : m = n then
-    subst m; simp only [getElem_set_self, ↓reduceIte]
+theorem getElem_set {l : List α} {i j} {a} (h) :
+    (set l i a)[j]'h = if i = j then a else l[j]'(length_set .. ▸ h) := by
+  if h : i = j then
+    subst h; simp only [getElem_set_self, ↓reduceIte]
   else
     simp [h]
 
@@ -1019,8 +1019,8 @@ theorem getLastD_mem_cons : ∀ (l : List α) (a : α), getLastD l a ∈ a::l
   | [], _ => .head ..
   | _::_, _ => .tail _ <| getLast_mem _
 
-theorem getElem_cons_length (x : α) (xs : List α) (n : Nat) (h : n = xs.length) :
-    (x :: xs)[n]'(by simp [h]) = (x :: xs).getLast (cons_ne_nil x xs) := by
+theorem getElem_cons_length (x : α) (xs : List α) (i : Nat) (h : i = xs.length) :
+    (x :: xs)[i]'(by simp [h]) = (x :: xs).getLast (cons_ne_nil x xs) := by
   rw [getLast_eq_getElem]; cases h; rfl
 
 @[deprecated getElem_cons_length (since := "2024-06-12")]
@@ -1252,24 +1252,24 @@ theorem map_singleton (f : α → β) (a : α) : map f [a] = [f a] := rfl
   | nil => simp [List.map]
   | cons _ as ih => simp [List.map, ih]
 
-@[simp] theorem getElem?_map (f : α → β) : ∀ (l : List α) (n : Nat), (map f l)[n]? = Option.map f l[n]?
+@[simp] theorem getElem?_map (f : α → β) : ∀ (l : List α) (i : Nat), (map f l)[i]? = Option.map f l[i]?
   | [], _ => rfl
   | _ :: _, 0 => by simp
-  | _ :: l, n+1 => by simp [getElem?_map f l n]
+  | _ :: l, i+1 => by simp [getElem?_map f l i]
 
 @[deprecated getElem?_map (since := "2024-06-12")]
-theorem get?_map (f : α → β) : ∀ l n, (map f l).get? n = (l.get? n).map f
+theorem get?_map (f : α → β) : ∀ l i, (map f l).get? i = (l.get? i).map f
   | [], _ => rfl
   | _ :: _, 0 => rfl
-  | _ :: l, n+1 => get?_map f l n
+  | _ :: l, i+1 => get?_map f l i
 
-@[simp] theorem getElem_map (f : α → β) {l} {n : Nat} {h : n < (map f l).length} :
-    (map f l)[n] = f (l[n]'(length_map l f ▸ h)) :=
+@[simp] theorem getElem_map (f : α → β) {l} {i : Nat} {h : i < (map f l).length} :
+    (map f l)[i] = f (l[i]'(length_map l f ▸ h)) :=
   Option.some.inj <| by rw [← getElem?_eq_getElem, getElem?_map, getElem?_eq_getElem]; rfl
 
 @[deprecated getElem_map (since := "2024-06-12")]
-theorem get_map (f : α → β) {l n} :
-    get (map f l) n = f (get l ⟨n, length_map l f ▸ n.2⟩) := by
+theorem get_map (f : α → β) {l i} :
+    get (map f l) i = f (get l ⟨i, length_map l f ▸ i.2⟩) := by
   simp
 
 @[simp] theorem mem_map {f : α → β} : ∀ {l : List α}, b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b
@@ -1700,71 +1700,71 @@ theorem filterMap_eq_cons_iff {l} {b} {bs} :
 @[simp] theorem cons_append_fun (a : α) (as : List α) :
     (fun bs => ((a :: as) ++ bs)) = fun bs => a :: (as ++ bs) := rfl
 
-theorem getElem_append {l₁ l₂ : List α} (n : Nat) (h : n < (l₁ ++ l₂).length) :
-    (l₁ ++ l₂)[n] = if h' : n < l₁.length then l₁[n] else l₂[n - l₁.length]'(by simp at h h'; exact Nat.sub_lt_left_of_lt_add h' h) := by
+theorem getElem_append {l₁ l₂ : List α} (i : Nat) (h : i < (l₁ ++ l₂).length) :
+    (l₁ ++ l₂)[i] = if h' : i < l₁.length then l₁[i] else l₂[i - l₁.length]'(by simp at h h'; exact Nat.sub_lt_left_of_lt_add h' h) := by
   split <;> rename_i h'
   · rw [getElem_append_left h']
   · rw [getElem_append_right (by simpa using h')]
 
-theorem getElem?_append_left {l₁ l₂ : List α} {n : Nat} (hn : n < l₁.length) :
-    (l₁ ++ l₂)[n]? = l₁[n]? := by
-  have hn' : n < (l₁ ++ l₂).length := Nat.lt_of_lt_of_le hn <|
+theorem getElem?_append_left {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) :
+    (l₁ ++ l₂)[i]? = l₁[i]? := by
+  have hn' : i < (l₁ ++ l₂).length := Nat.lt_of_lt_of_le hn <|
     length_append .. ▸ Nat.le_add_right ..
   simp_all [getElem?_eq_getElem, getElem_append]
 
-theorem getElem?_append_right : ∀ {l₁ l₂ : List α} {n : Nat}, l₁.length ≤ n →
-  (l₁ ++ l₂)[n]? = l₂[n - l₁.length]?
+theorem getElem?_append_right : ∀ {l₁ l₂ : List α} {i : Nat}, l₁.length ≤ i →
+  (l₁ ++ l₂)[i]? = l₂[i - l₁.length]?
 | [], _, _, _ => rfl
-| a :: l, _, n+1, h₁ => by
+| a :: l, _, i+1, h₁ => by
   rw [cons_append]
   simp [Nat.succ_sub_succ_eq_sub, getElem?_append_right (Nat.lt_succ.1 h₁)]
 
-theorem getElem?_append {l₁ l₂ : List α} {n : Nat} :
-    (l₁ ++ l₂)[n]? = if n < l₁.length then l₁[n]? else l₂[n - l₁.length]? := by
+theorem getElem?_append {l₁ l₂ : List α} {i : Nat} :
+    (l₁ ++ l₂)[i]? = if i < l₁.length then l₁[i]? else l₂[i - l₁.length]? := by
   split <;> rename_i h
   · exact getElem?_append_left h
   · exact getElem?_append_right (by simpa using h)
 
 @[deprecated getElem?_append_right (since := "2024-06-12")]
-theorem get?_append_right {l₁ l₂ : List α} {n : Nat} (h : l₁.length ≤ n) :
-    (l₁ ++ l₂).get? n = l₂.get? (n - l₁.length) := by
+theorem get?_append_right {l₁ l₂ : List α} {i : Nat} (h : l₁.length ≤ i) :
+    (l₁ ++ l₂).get? i = l₂.get? (i - l₁.length) := by
   simp [getElem?_append_right, h]
 
 /-- Variant of `getElem_append_left` useful for rewriting from the small list to the big list. -/
-theorem getElem_append_left' (l₂ : List α) {l₁ : List α} {n : Nat} (hn : n < l₁.length) :
-    l₁[n] = (l₁ ++ l₂)[n]'(by simpa using Nat.lt_add_right l₂.length hn) := by
+theorem getElem_append_left' (l₂ : List α) {l₁ : List α} {i : Nat} (hi : i < l₁.length) :
+    l₁[i] = (l₁ ++ l₂)[i]'(by simpa using Nat.lt_add_right l₂.length hi) := by
   rw [getElem_append_left] <;> simp
 
 /-- Variant of `getElem_append_right` useful for rewriting from the small list to the big list. -/
-theorem getElem_append_right' (l₁ : List α) {l₂ : List α} {n : Nat} (hn : n < l₂.length) :
-    l₂[n] = (l₁ ++ l₂)[n + l₁.length]'(by simpa [Nat.add_comm] using Nat.add_lt_add_left hn _) := by
+theorem getElem_append_right' (l₁ : List α) {l₂ : List α} {i : Nat} (hi : i < l₂.length) :
+    l₂[i] = (l₁ ++ l₂)[i + l₁.length]'(by simpa [Nat.add_comm] using Nat.add_lt_add_left hi _) := by
   rw [getElem_append_right] <;> simp [*, le_add_left]
 
 @[deprecated "Deprecated without replacement." (since := "2024-06-12")]
-theorem get_append_right_aux {l₁ l₂ : List α} {n : Nat}
-  (h₁ : l₁.length ≤ n) (h₂ : n < (l₁ ++ l₂).length) : n - l₁.length < l₂.length := by
+theorem get_append_right_aux {l₁ l₂ : List α} {i : Nat}
+  (h₁ : l₁.length ≤ i) (h₂ : i < (l₁ ++ l₂).length) : i - l₁.length < l₂.length := by
   rw [length_append] at h₂
   exact Nat.sub_lt_left_of_lt_add h₁ h₂
 
 set_option linter.deprecated false in
 @[deprecated getElem_append_right (since := "2024-06-12")]
-theorem get_append_right' {l₁ l₂ : List α} {n : Nat} (h₁ : l₁.length ≤ n) (h₂) :
-    (l₁ ++ l₂).get ⟨n, h₂⟩ = l₂.get ⟨n - l₁.length, get_append_right_aux h₁ h₂⟩ :=
+theorem get_append_right' {l₁ l₂ : List α} {i : Nat} (h₁ : l₁.length ≤ i) (h₂) :
+    (l₁ ++ l₂).get ⟨i, h₂⟩ = l₂.get ⟨i - l₁.length, get_append_right_aux h₁ h₂⟩ :=
   Option.some.inj <| by rw [← get?_eq_get, ← get?_eq_get, get?_append_right h₁]
 
-theorem getElem_of_append {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = n) :
-    l[n]'(eq ▸ h ▸ by simp_arith) = a := Option.some.inj <| by
+theorem getElem_of_append {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = i) :
+    l[i]'(eq ▸ h ▸ by simp_arith) = a := Option.some.inj <| by
   rw [← getElem?_eq_getElem, eq, getElem?_append_right (h ▸ Nat.le_refl _), h]
   simp
 
 @[deprecated "Deprecated without replacement." (since := "2024-06-12")]
 theorem get_of_append_proof {l : List α}
-    (eq : l = l₁ ++ a :: l₂) (h : l₁.length = n) : n < length l := eq ▸ h ▸ by simp_arith
+    (eq : l = l₁ ++ a :: l₂) (h : l₁.length = i) : i < length l := eq ▸ h ▸ by simp_arith
 
 set_option linter.deprecated false in
 @[deprecated getElem_of_append (since := "2024-06-12")]
-theorem get_of_append {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = n) :
-    l.get ⟨n, get_of_append_proof eq h⟩ = a := Option.some.inj <| by
+theorem get_of_append {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = i) :
+    l.get ⟨i, get_of_append_proof eq h⟩ = a := Option.some.inj <| by
   rw [← get?_eq_get, eq, get?_append_right (h ▸ Nat.le_refl _), h, Nat.sub_self]; rfl
 
 /--
@@ -3404,12 +3404,12 @@ theorem getElem!_nil [Inhabited α] {n : Nat} : ([] : List α)[n]! = default :=
 theorem getElem!_cons_zero [Inhabited α] {l : List α} : (a::l)[0]! = a := by
   rw [getElem!_pos] <;> simp
 
-theorem getElem!_cons_succ [Inhabited α] {l : List α} : (a::l)[n+1]! = l[n]! := by
-  by_cases h : n < l.length
+theorem getElem!_cons_succ [Inhabited α] {l : List α} : (a::l)[i+1]! = l[i]! := by
+  by_cases h : i < l.length
   · rw [getElem!_pos, getElem!_pos] <;> simp_all [Nat.succ_lt_succ_iff]
   · rw [getElem!_neg, getElem!_neg] <;> simp_all [Nat.succ_lt_succ_iff]
 
-theorem getElem!_of_getElem? [Inhabited α] : ∀ {l : List α} {n : Nat}, l[n]? = some a → l[n]! = a
+theorem getElem!_of_getElem? [Inhabited α] : ∀ {l : List α} {i : Nat}, l[i]? = some a → l[i]! = a
   | _a::_, 0, _ => by
     rw [getElem!_pos] <;> simp_all
   | _::l, _+1, e => by
@@ -3558,7 +3558,7 @@ theorem isSome_getElem? {l : List α} {n : Nat} : l[n]?.isSome ↔ n < l.length
   simp
 
 @[deprecated _root_.isNone_getElem? (since := "2024-12-09")]
-theorem isNone_getElem? {l : List α} {n : Nat} : l[n]?.isNone ↔ l.length ≤ n := by
+theorem isNone_getElem? {l : List α} {i : Nat} : l[i]?.isNone ↔ l.length ≤ i := by
   simp
 
 end List

src/Init/Data/Vector/Basic.lean

@@ -70,6 +70,16 @@ instance [Inhabited α] : Inhabited (Vector α n) where
 instance : GetElem (Vector α n) Nat α fun _ i => i < n where
   getElem x i h := get x ⟨i, h⟩
 
+/-- Check if there is an element which satisfies `a == ·`. -/
+def contains [BEq α] (v : Vector α n) (a : α) : Bool := v.toArray.contains a
+
+/-- `a ∈ v` is a predicate which asserts that `a` is in the vector `v`. -/
+structure Mem (as : Vector α n) (a : α) : Prop where
+  val : a ∈ as.toArray
+
+instance : Membership α (Vector α n) where
+  mem := Mem
+
 /--
 Get an element of a vector using a `Nat` index. Returns the given default value if the index is out
 of bounds.
@@ -254,3 +264,19 @@ no element of the index matches the given value.
 /-- Returns `true` when `v` is a prefix of the vector `w`. -/
 @[inline] def isPrefixOf [BEq α] (v : Vector α m) (w : Vector α n) : Bool :=
   v.toArray.isPrefixOf w.toArray
+
+/-- Returns `true` with the monad if `p` returns `true` for any element of the vector. -/
+@[inline] def anyM [Monad m] (p : α → m Bool) (v : Vector α n) : m Bool :=
+  v.toArray.anyM p
+
+/-- Returns `true` with the monad if `p` returns `true` for all elements of the vector. -/
+@[inline] def allM [Monad m] (p : α → m Bool) (v : Vector α n) : m Bool :=
+  v.toArray.allM p
+
+/-- Returns `true` if `p` returns `true` for any element of the vector. -/
+@[inline] def any (v : Vector α n) (p : α → Bool) : Bool :=
+  v.toArray.any p
+
+/-- Returns `true` if `p` returns `true` for all elements of the vector. -/
+@[inline] def all (v : Vector α n) (p : α → Bool) : Bool :=
+  v.toArray.all p

src/Init/Data/Vector/Lemmas.lean

@@ -22,44 +22,21 @@ end Array
 
 namespace Vector
 
+/-! ### mk lemmas -/
+
+theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a := rfl
+
 @[simp] theorem getElem_mk {data : Array α} {size : data.size = n} {i : Nat} (h : i < n) :
     (Vector.mk data size)[i] = data[i] := rfl
 
-@[simp] theorem getElem_toArray {α n} (xs : Vector α n) (i : Nat) (h : i < xs.toArray.size) :
-    xs.toArray[i] = xs[i]'(by simpa using h) := by
-  cases xs
-  simp
+@[simp] theorem getElem?_mk {data : Array α} {size : data.size = n} {i : Nat} :
+    (Vector.mk data size)[i]? = data[i]? := by
+  subst size
+  simp [getElem?_def]
 
-@[simp] theorem getElem_ofFn {α n} (f : Fin n → α) (i : Nat) (h : i < n) :
-    (Vector.ofFn f)[i] = f ⟨i, by simpa using h⟩ := by
-  simp [ofFn]
-
-/-- The empty vector maps to the empty vector. -/
-@[simp]
-theorem map_empty (f : α → β) : map f #v[] = #v[] := by
-  rw [map, mk.injEq]
-  exact Array.map_empty f
-
-theorem toArray_inj : ∀ {v w : Vector α n}, v.toArray = w.toArray → v = w
-  | {..}, {..}, rfl => rfl
-
-/-- A vector of length `0` is the empty vector. -/
-protected theorem eq_empty (v : Vector α 0) : v = #v[] := by
-  apply Vector.toArray_inj
-  apply Array.eq_empty_of_size_eq_zero v.2
-
-/--
-`Vector.ext` is an extensionality theorem.
-Vectors `a` and `b` are equal to each other if their elements are equal for each valid index.
--/
-@[ext]
-protected theorem ext {a b : Vector α n} (h : (i : Nat) → (_ : i < n) → a[i] = b[i]) : a = b := by
-  apply Vector.toArray_inj
-  apply Array.ext
-  · rw [a.size_toArray, b.size_toArray]
-  · intro i hi _
-    rw [a.size_toArray] at hi
-    exact h i hi
+@[simp] theorem mem_mk {data : Array α} {size : data.size = n} {a : α} :
+    a ∈ Vector.mk data size ↔ a ∈ data :=
+  ⟨fun ⟨h⟩ => h, fun h => ⟨h⟩⟩
 
 @[simp] theorem push_mk {data : Array α} {size : data.size = n} {x : α} :
     (Vector.mk data size).push x =
@@ -68,40 +45,6 @@ protected theorem ext {a b : Vector α n} (h : (i : Nat) → (_ : i < n) → a[i
 @[simp] theorem pop_mk {data : Array α} {size : data.size = n} :
     (Vector.mk data size).pop = Vector.mk data.pop (by simp [size]) := rfl
 
-@[simp] theorem getElem_push_last {v : Vector α n} {x : α} : (v.push x)[n] = x := by
-  rcases v with ⟨data, rfl⟩
-  simp
-
-@[simp] theorem getElem_push_lt {v : Vector α n} {x : α} {i : Nat} (h : i < n) :
-    (v.push x)[i] = v[i] := by
-  rcases v with ⟨data, rfl⟩
-  simp [Array.getElem_push_lt, h]
-
-@[simp] theorem getElem_pop {v : Vector α n} {i : Nat} (h : i < n - 1) : (v.pop)[i] = v[i] := by
-  rcases v with ⟨data, rfl⟩
-  simp
-
-/--
-Variant of `getElem_pop` that will sometimes fire when `getElem_pop` gets stuck because of
-defeq issues in the implicit size argument.
--/
-@[simp] theorem getElem_pop' (v : Vector α (n + 1)) (i : Nat) (h : i < n + 1 - 1) :
-    @getElem (Vector α n) Nat α (fun _ i => i < n) instGetElemNatLt v.pop i h = v[i] :=
-  getElem_pop h
-
-@[simp] theorem push_pop_back (v : Vector α (n + 1)) : v.pop.push v.back = v := by
-  ext i
-  by_cases h : i < n
-  · 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]
-
-
-/-! ### mk lemmas -/
-
-theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a := rfl
-
 @[simp] theorem allDiff_mk [BEq α] (a : Array α) (h : a.size = n) :
     (Vector.mk a h).allDiff = a.allDiff := rfl
 
@@ -177,8 +120,30 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
       (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
 
+@[simp] theorem anyM_mk [Monad m] (p : α → m Bool) (a : Array α) (h : a.size = n) :
+    (Vector.mk a h).anyM p = a.anyM p := rfl
+
+@[simp] theorem allM_mk [Monad m] (p : α → m Bool) (a : Array α) (h : a.size = n) :
+    (Vector.mk a h).allM p = a.allM p := rfl
+
+@[simp] theorem any_mk (p : α → Bool) (a : Array α) (h : a.size = n) :
+    (Vector.mk a h).any p = a.any p := rfl
+
+@[simp] theorem all_mk (p : α → Bool) (a : Array α) (h : a.size = n) :
+    (Vector.mk a h).all p = a.all p := rfl
+
 /-! ### toArray lemmas -/
 
+@[simp] theorem getElem_toArray {α n} (xs : Vector α n) (i : Nat) (h : i < xs.toArray.size) :
+    xs.toArray[i] = xs[i]'(by simpa using h) := by
+  cases xs
+  simp
+
+@[simp] theorem getElem?_toArray {α n} (xs : Vector α n) (i : Nat) :
+    xs.toArray[i]? = xs[i]? := by
+  cases xs
+  simp
+
 @[simp] theorem toArray_append (a : Vector α m) (b : Vector α n) :
     (a ++ b).toArray = a.toArray ++ b.toArray := rfl
 
@@ -247,18 +212,443 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
 @[simp] theorem toArray_zipWith (f : α → β → γ) (a : Vector α n) (b : Vector β n) :
     (Vector.zipWith a b f).toArray = Array.zipWith a.toArray b.toArray f := rfl
 
-/-! ### toList lemmas -/
+theorem toArray_inj : ∀ {v w : Vector α n}, v.toArray = w.toArray → v = w
+  | {..}, {..}, rfl => rfl
+
+@[simp] theorem toArray_eq_empty_iff (v : Vector α n) : v.toArray = #[] ↔ n = 0 := by
+  rcases v with ⟨v, h⟩
+  exact ⟨by rintro rfl; simp_all, by rintro rfl; simpa using h⟩
+
+@[simp] theorem mem_toArray_iff (a : α) (v : Vector α n) : a ∈ v.toArray ↔ a ∈ v :=
+  ⟨fun h => ⟨h⟩, fun ⟨h⟩ => h⟩
+
+/-! ### toList -/
+
+@[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
+  simp
+
+@[simp] theorem getElem?_toList {α n} (xs : Vector α n) (i : Nat) :
+    xs.toList[i]? = xs[i]? := by
+  cases xs
+  simp
+
+theorem toList_append (a : Vector α m) (b : Vector α n) :
+    (a ++ b).toList = a.toList ++ b.toList := by simp
+
+@[simp] theorem toList_drop (a : Vector α n) (m) :
+    (a.drop m).toList = a.toList.drop m := by
+  simp [List.take_of_length_le]
+
+theorem toList_empty : (#v[] : Vector α 0).toArray = #[] := by simp
+
+theorem toList_mkEmpty (cap) :
+    (Vector.mkEmpty (α := α) cap).toList = [] := rfl
+
+theorem toList_eraseIdx (a : Vector α n) (i) (h) :
+    (a.eraseIdx i h).toList = a.toList.eraseIdx i := by simp
+
+@[simp] theorem toList_eraseIdx! (a : Vector α n) (i) (hi : i < n) :
+    (a.eraseIdx! i).toList = a.toList.eraseIdx i := by
+  cases a; simp_all [Array.eraseIdx!]
+
+theorem toList_cast (a : Vector α n) (h : n = m) :
+    (a.cast h).toList = a.toList := rfl
+
+theorem toList_extract (a : Vector α n) (start stop) :
+    (a.extract start stop).toList = (a.toList.drop start).take (stop - start) := by
+  simp
+
+theorem toList_map (f : α → β) (a : Vector α n) :
+    (a.map f).toList = a.toList.map f := 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
+
+theorem toList_push (a : Vector α n) (x) : (a.push x).toList = a.toList ++ [x] := by simp
+
+theorem toList_range : (Vector.range n).toList = List.range n := by simp
+
+theorem toList_reverse (a : Vector α n) : a.reverse.toList = a.toList.reverse := by simp
+
+theorem toList_set (a : Vector α n) (i x h) :
+    (a.set i x).toList = a.toList.set i x := rfl
+
+@[simp] theorem toList_setIfInBounds (a : Vector α n) (i x) :
+    (a.setIfInBounds i x).toList = a.toList.set i x := by
+  simp [Vector.setIfInBounds]
+
+theorem toList_singleton (x : α) : (Vector.singleton x).toList = [x] := rfl
+
+theorem toList_swap (a : Vector α n) (i j) (hi hj) :
+    (a.swap i j).toList = (a.toList.set i a[j]).set j a[i] := rfl
+
+@[simp] theorem toList_take (a : Vector α n) (m) : (a.take m).toList = a.toList.take m := by
+  simp [List.take_of_length_le]
+
+@[simp] theorem toList_zipWith (f : α → β → γ) (a : Vector α n) (b : Vector β n) :
+    (Vector.zipWith a b f).toArray = Array.zipWith a.toArray b.toArray f := rfl
+
+theorem toList_inj : ∀ {v w : Vector α n}, v.toList = w.toList → v = w
+  | {..}, {..}, rfl => rfl
+
+@[simp] theorem toList_eq_empty_iff (v : Vector α n) : v.toList = [] ↔ n = 0 := by
+  rcases v with ⟨v, h⟩
+  simp only [Array.toList_eq_nil_iff]
+  exact ⟨by rintro rfl; simp_all, by rintro rfl; simpa using h⟩
+
+@[simp] theorem mem_toList_iff (a : α) (v : Vector α n) : a ∈ v.toList ↔ a ∈ v := by
+  simp
 
 theorem length_toList {α n} (xs : Vector α n) : xs.toList.length = n := by 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 simp
+/-! ### empty -/
 
-theorem toList_inj {a b : Vector α n} (h : a.toList = b.toList) : a = b := by
-  rcases a with ⟨⟨a⟩, ha⟩
-  rcases b with ⟨⟨b⟩, hb⟩
+@[simp] theorem empty_eq {xs : Vector α 0} : #v[] = xs ↔ xs = #v[] := by
+  cases xs
+  simp
+
+/-- A vector of length `0` is the empty vector. -/
+protected theorem eq_empty (v : Vector α 0) : v = #v[] := by
+  apply Vector.toArray_inj
+  apply Array.eq_empty_of_size_eq_zero v.2
+
+
+/-! ### size -/
+
+theorem eq_empty_of_size_eq_zero (xs : Vector α n) (h : n = 0) : xs = #v[].cast h.symm := by
+  rcases xs with ⟨xs, rfl⟩
+  apply toArray_inj
+  simp only [List.length_eq_zero, Array.toList_eq_nil_iff] at h
+  simp [h]
+
+theorem size_eq_one {xs : Vector α 1} : ∃ a, xs = #v[a] := by
+  rcases xs with ⟨xs, h⟩
+  simpa using Array.size_eq_one.mp h
+
+/-! ### push -/
+
+theorem back_eq_of_push_eq {a b : α} {xs ys : Vector α n} (h : xs.push a = ys.push b) : a = b := by
+  cases xs
+  cases ys
+  replace h := congrArg Vector.toArray h
+  simp only [push_mk] at h
+  apply Array.back_eq_of_push_eq h
+
+theorem pop_eq_of_push_eq {a b : α} {xs ys : Vector α n} (h : xs.push a = ys.push b) : xs = ys := by
+  cases xs
+  cases ys
+  replace h := congrArg Vector.toArray h
+  simp only [push_mk] at h
+  simpa using Array.pop_eq_of_push_eq h
+
+theorem push_inj_left {a : α} {xs ys : Vector α n} : xs.push a = ys.push a ↔ xs = ys :=
+  ⟨pop_eq_of_push_eq, fun h => by simp [h]⟩
+
+theorem push_inj_right {a b : α} {xs : Vector α n} : xs.push a = xs.push b ↔ a = b :=
+  ⟨back_eq_of_push_eq, fun h => by simp [h]⟩
+
+theorem push_eq_push {a b : α} {xs ys : Vector α n} : xs.push a = ys.push b ↔ a = b ∧ xs = ys := by
+  constructor
+  · intro h
+    exact ⟨back_eq_of_push_eq h, pop_eq_of_push_eq h⟩
+  · rintro ⟨rfl, rfl⟩
+    rfl
+
+theorem exists_push {xs : Vector α (n + 1)} :
+    ∃ (ys : Vector α n) (a : α), xs = ys.push a := by
+  rcases xs with ⟨xs, w⟩
+  obtain ⟨ys, a, h⟩ := Array.exists_push_of_size_eq_add_one w
+  exact ⟨⟨ys, by simp_all⟩, a, toArray_inj h⟩
+
+/-! ## L[i] and L[i]? -/
+
+@[simp] theorem getElem?_eq_none_iff {a : Vector α n} : a[i]? = none ↔ n ≤ i := by
+  by_cases h : i < n
+  · simp [getElem?_pos, h]
+  · rw [getElem?_neg a i h]
+    simp_all
+
+@[simp] theorem none_eq_getElem?_iff {a : Vector α n} {i : Nat} : none = a[i]? ↔ n ≤ i := by
+  simp [eq_comm (a := none)]
+
+theorem getElem?_eq_none {a : Vector α n} (h : n ≤ i) : a[i]? = none := by
+  simp [getElem?_eq_none_iff, h]
+
+@[simp] theorem getElem?_eq_getElem {a : Vector α n} {i : Nat} (h : i < n) : a[i]? = some a[i] :=
+  getElem?_pos ..
+
+theorem getElem?_eq_some_iff {a : Vector α n} : a[i]? = some b ↔ ∃ h : i < n, a[i] = b := by
+  simp [getElem?_def]
+
+theorem some_eq_getElem?_iff {a : Vector α n} : some b = a[i]? ↔ ∃ h : i < n, a[i] = b := by
+  rw [eq_comm, getElem?_eq_some_iff]
+
+@[simp] theorem some_getElem_eq_getElem?_iff (a : Vector α n) (i : Nat) (h : i < n) :
+    (some a[i] = a[i]?) ↔ True := by
+  simp [h]
+
+@[simp] theorem getElem?_eq_some_getElem_iff (a : Vector α n) (i : Nat) (h : i < n) :
+    (a[i]? = some a[i]) ↔ True := by
+  simp [h]
+
+theorem getElem_eq_iff {a : Vector α n} {i : Nat} {h : i < n} : a[i] = x ↔ a[i]? = some x := by
+  simp only [getElem?_eq_some_iff]
+  exact ⟨fun w => ⟨h, w⟩, fun h => h.2⟩
+
+theorem getElem_eq_getElem?_get (a : Vector α n) (i : Nat) (h : i < n) :
+    a[i] = a[i]?.get (by simp [getElem?_eq_getElem, h]) := by
+  simp [getElem_eq_iff]
+
+theorem getD_getElem? (a : Vector α n) (i : Nat) (d : α) :
+    a[i]?.getD d = if p : i < n then a[i]'p else d := by
+  if h : i < n then
+    simp [h, getElem?_def]
+  else
+    have p : i ≥ n := Nat.le_of_not_gt h
+    simp [getElem?_eq_none p, h]
+
+@[simp] theorem getElem?_empty {n : Nat} : (#v[] : Vector α 0)[n]? = none := rfl
+
+@[simp] theorem getElem_push_lt {v : Vector α n} {x : α} {i : Nat} (h : i < n) :
+    (v.push x)[i] = v[i] := by
+  rcases v with ⟨data, rfl⟩
+  simp [Array.getElem_push_lt, h]
+
+@[simp] theorem getElem_push_eq (a : Vector α n) (x : α) : (a.push x)[n] = x := by
+  rcases a with ⟨a, rfl⟩
+  simp
+
+theorem getElem_push (a : Vector α n) (x : α) (i : Nat) (h : i < n + 1) :
+    (a.push x)[i] = if h : i < n then a[i] else x := by
+  rcases a with ⟨a, rfl⟩
+  simp [Array.getElem_push]
+
+theorem getElem?_push {a : Vector α n} {x} : (a.push x)[i]? = if i = n then some x else a[i]? := by
+  simp [getElem?_def, getElem_push]
+  (repeat' split) <;> first | rfl | omega
+
+@[simp] theorem getElem?_push_size {a : Vector α n} {x} : (a.push x)[n]? = some x := by
+  simp [getElem?_push]
+
+@[simp] theorem getElem_singleton (a : α) (h : i < 1) : #v[a][i] = a :=
+  match i, h with
+  | 0, _ => rfl
+
+theorem getElem?_singleton (a : α) (i : Nat) : #v[a][i]? = if i = 0 then some a else none := by
+  simp [List.getElem?_singleton]
+
+/-! ### mem -/
+
+@[simp] theorem getElem_mem {l : Vector α n} {i : Nat} (h : i < n) : l[i] ∈ l := by
+  rcases l with ⟨l, rfl⟩
+  simp
+
+@[simp] theorem not_mem_empty (a : α) : ¬ a ∈ #v[] := nofun
+
+@[simp] theorem mem_push {a : Vector α n} {x y : α} : x ∈ a.push y ↔ x ∈ a ∨ x = y := by
+  cases a
+  simp
+
+theorem mem_push_self {a : Vector α n} {x : α} : x ∈ a.push x :=
+  mem_push.2 (Or.inr rfl)
+
+theorem eq_push_append_of_mem {xs : Vector α n} {x : α} (h : x ∈ xs) :
+    ∃ (n₁ n₂ : Nat) (as : Vector α n₁) (bs : Vector α n₂) (h : n₁ + 1 + n₂ = n),
+      xs = (as.push x ++ bs).cast h ∧ x ∉ as:= by
+  rcases xs with ⟨xs, rfl⟩
+  obtain ⟨as, bs, h, w⟩ := Array.eq_push_append_of_mem (by simpa using h)
+  simp only at h
+  obtain rfl := h
+  exact ⟨_, _, as.toVector, bs.toVector, by simp, by simp, by simpa using w⟩
+
+theorem mem_push_of_mem {a : Vector α n} {x : α} (y : α) (h : x ∈ a) : x ∈ a.push y :=
+  mem_push.2 (Or.inl h)
+
+theorem exists_mem_of_size_pos (l : Vector α n) (h : 0 < n) : ∃ x, x ∈ l := by
+  simpa using List.exists_mem_of_ne_nil l.toList (by simpa using (Nat.ne_of_gt h))
+
+theorem size_zero_iff_forall_not_mem {l : Vector α n} : n = 0 ↔ ∀ a, a ∉ l := by
+  simpa using List.eq_nil_iff_forall_not_mem (l := l.toList)
+
+@[simp] theorem mem_dite_empty_left {x : α} [Decidable p] {l : ¬ p → Vector α 0} :
+    (x ∈ if h : p then #v[] else l h) ↔ ∃ h : ¬ p, x ∈ l h := by
+  split <;> simp_all
+
+@[simp] theorem mem_dite_empty_right {x : α} [Decidable p] {l : p → Vector α 0} :
+    (x ∈ if h : p then l h else #v[]) ↔ ∃ h : p, x ∈ l h := by
+  split <;> simp_all
+
+@[simp] theorem mem_ite_empty_left {x : α} [Decidable p] {l : Vector α 0} :
+    (x ∈ if p then #v[] else l) ↔ ¬ p ∧ x ∈ l := by
+  split <;> simp_all
+
+@[simp] theorem mem_ite_empty_right {x : α} [Decidable p] {l : Vector α 0} :
+    (x ∈ if p then l else #v[]) ↔ p ∧ x ∈ l := by
+  split <;> simp_all
+
+theorem eq_of_mem_singleton (h : a ∈ #v[b]) : a = b := by
   simpa using h
 
+@[simp] theorem mem_singleton {a b : α} : a ∈ #v[b] ↔ a = b :=
+  ⟨eq_of_mem_singleton, (by simp [·])⟩
+
+theorem forall_mem_push {p : α → Prop} {xs : Vector α n} {a : α} :
+    (∀ x, x ∈ xs.push a → p x) ↔ p a ∧ ∀ x, x ∈ xs → p x := by
+  cases xs
+  simp [or_comm, forall_eq_or_imp]
+
+theorem forall_mem_ne {a : α} {l : Vector α n} : (∀ a' : α, a' ∈ l → ¬a = a') ↔ a ∉ l :=
+  ⟨fun h m => h _ m rfl, fun h _ m e => h (e.symm ▸ m)⟩
+
+theorem forall_mem_ne' {a : α} {l : Vector α n} : (∀ a' : α, a' ∈ l → ¬a' = a) ↔ a ∉ l :=
+  ⟨fun h m => h _ m rfl, fun h _ m e => h (e.symm ▸ m)⟩
+
+theorem exists_mem_empty (p : α → Prop) : ¬ (∃ x, ∃ _ : x ∈ #v[], p x) := nofun
+
+theorem forall_mem_empty (p : α → Prop) : ∀ (x) (_ : x ∈ #v[]), p x := nofun
+
+theorem exists_mem_push {p : α → Prop} {a : α} {xs : Vector α n} :
+    (∃ x, ∃ _ : x ∈ xs.push a, p x) ↔ p a ∨ ∃ x, ∃ _ : x ∈ xs, p x := by
+  simp only [mem_push, exists_prop]
+  constructor
+  · rintro ⟨x, (h | rfl), h'⟩
+    · exact .inr ⟨x, h, h'⟩
+    · exact .inl h'
+  · rintro (h | ⟨x, h, h'⟩)
+    · exact ⟨a, by simp, h⟩
+    · exact ⟨x, .inl h, h'⟩
+
+theorem forall_mem_singleton {p : α → Prop} {a : α} : (∀ (x) (_ : x ∈ #v[a]), p x) ↔ p a := by
+  simp only [mem_singleton, forall_eq]
+
+theorem mem_empty_iff (a : α) : a ∈ (#v[] : Vector α 0) ↔ False := by simp
+
+theorem mem_singleton_self (a : α) : a ∈ #v[a] := by simp
+
+theorem mem_of_mem_push_of_mem {a b : α} {l : Vector α n} : a ∈ l.push b → b ∈ l → a ∈ l := by
+  rcases l with ⟨l, rfl⟩
+  simpa using Array.mem_of_mem_push_of_mem
+
+theorem eq_or_ne_mem_of_mem {a b : α} {l : Vector α n} (h' : a ∈ l.push b) :
+    a = b ∨ (a ≠ b ∧ a ∈ l) := by
+  if h : a = b then
+    exact .inl h
+  else
+    simp only [mem_push, h, or_false] at h'
+    exact .inr ⟨h, h'⟩
+
+theorem size_ne_zero_of_mem {a : α} {l : Vector α n} (h : a ∈ l) : n ≠ 0 := by
+  rcases l with ⟨l, rfl⟩
+  simpa using Array.ne_empty_of_mem (by simpa using h)
+
+theorem mem_of_ne_of_mem {a y : α} {l : Vector α n} (h₁ : a ≠ y) (h₂ : a ∈ l.push y) : a ∈ l := by
+  simpa [h₁] using h₂
+
+theorem ne_of_not_mem_push {a b : α} {l : Vector α n} (h : a ∉ l.push b) : a ≠ b := by
+  simp only [mem_push, not_or] at h
+  exact h.2
+
+theorem not_mem_of_not_mem_push {a b : α} {l : Vector α n} (h : a ∉ l.push b) : a ∉ l := by
+  simp only [mem_push, not_or] at h
+  exact h.1
+
+theorem not_mem_push_of_ne_of_not_mem {a y : α} {l : Vector α n} : a ≠ y → a ∉ l → a ∉ l.push y :=
+  mt ∘ mem_of_ne_of_mem
+
+theorem ne_and_not_mem_of_not_mem_push {a y : α} {l : Vector α n} : a ∉ l.push y → a ≠ y ∧ a ∉ l := by
+  simp +contextual
+
+theorem getElem_of_mem {a} {l : Vector α n} (h : a ∈ l) : ∃ (i : Nat) (h : i < n), l[i]'h = a := by
+  rcases l with ⟨l, rfl⟩
+  simpa using Array.getElem_of_mem (by simpa using h)
+
+theorem getElem?_of_mem {a} {l : Vector α n} (h : a ∈ l) : ∃ i : Nat, l[i]? = some a :=
+  let ⟨n, _, e⟩ := getElem_of_mem h; ⟨n, e ▸ getElem?_eq_getElem _⟩
+
+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_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 ..⟩
+
+theorem mem_iff_getElem? {a} {l : Vector α n} : a ∈ l ↔ ∃ i : Nat, l[i]? = some a := by
+  simp [getElem?_eq_some_iff, mem_iff_getElem]
+
+theorem forall_getElem {l : Vector α n} {p : α → Prop} :
+    (∀ (i : Nat) h, p (l[i]'h)) ↔ ∀ a, a ∈ l → p a := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.forall_getElem]
+
+/-! ### Decidability of bounded quantifiers -/
+
+instance {xs : Vector α n} {p : α → Prop} [DecidablePred p] :
+    Decidable (∀ x, x ∈ xs → p x) :=
+  decidable_of_iff (∀ (i : Nat) h, p (xs[i]'h)) (by
+    simp only [mem_iff_getElem, forall_exists_index]
+    exact
+      ⟨by rintro w _ i h rfl; exact w i h, fun w i h => w _ i h rfl⟩)
+
+instance {xs : Vector α n} {p : α → Prop} [DecidablePred p] :
+    Decidable (∃ x, x ∈ xs ∧ p x) :=
+  decidable_of_iff (∃ (i : Nat), ∃ (h : i < n), p (xs[i]'h)) (by
+    simp [mem_iff_getElem]
+    exact
+      ⟨by rintro ⟨i, h, w⟩; exact ⟨_, ⟨i, h, rfl⟩, w⟩, fun ⟨_, ⟨i, h, rfl⟩, w⟩ => ⟨i, h, w⟩⟩)
+
+
+/-! Content below this point has not yet been aligned with `List` and `Array`. -/
+
+@[simp] theorem getElem_ofFn {α n} (f : Fin n → α) (i : Nat) (h : i < n) :
+    (Vector.ofFn f)[i] = f ⟨i, by simpa using h⟩ := by
+  simp [ofFn]
+
+/-- The empty vector maps to the empty vector. -/
+@[simp]
+theorem map_empty (f : α → β) : map f #v[] = #v[] := by
+  rw [map, mk.injEq]
+  exact Array.map_empty f
+
+
+/--
+`Vector.ext` is an extensionality theorem.
+Vectors `a` and `b` are equal to each other if their elements are equal for each valid index.
+-/
+@[ext]
+protected theorem ext {a b : Vector α n} (h : (i : Nat) → (_ : i < n) → a[i] = b[i]) : a = b := by
+  apply Vector.toArray_inj
+  apply Array.ext
+  · rw [a.size_toArray, b.size_toArray]
+  · intro i hi _
+    rw [a.size_toArray] at hi
+    exact h i hi
+
+@[simp] theorem getElem_push_last {v : Vector α n} {x : α} : (v.push x)[n] = x := by
+  rcases v with ⟨data, rfl⟩
+  simp
+
+@[simp] theorem getElem_pop {v : Vector α n} {i : Nat} (h : i < n - 1) : (v.pop)[i] = v[i] := by
+  rcases v with ⟨data, rfl⟩
+  simp
+
+/--
+Variant of `getElem_pop` that will sometimes fire when `getElem_pop` gets stuck because of
+defeq issues in the implicit size argument.
+-/
+@[simp] theorem getElem_pop' (v : Vector α (n + 1)) (i : Nat) (h : i < n + 1 - 1) :
+    @getElem (Vector α n) Nat α (fun _ i => i < n) instGetElemNatLt v.pop i h = v[i] :=
+  getElem_pop h
+
+@[simp] theorem push_pop_back (v : Vector α (n + 1)) : v.pop.push v.back = v := by
+  ext i
+  by_cases h : i < n
+  · 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]
+
 /-! ### set -/
 
 theorem getElem_set (a : Vector α n) (i : Nat) (x : α) (hi : i < n) (j : Nat) (hj : j < n) :