feat: finish alignment of List/Array/Vector.append lemmas

src/Init/Data/Array/Lemmas.lean

@@ -1504,14 +1504,20 @@ theorem filterMap_eq_push_iff {f : α → Option β} {l : Array α} {l' : Array
   · rintro ⟨⟨l₁⟩, a, ⟨l₂⟩, h₁, h₂, h₃, h₄⟩
     refine ⟨l₂.reverse, a, l₁.reverse, by simp_all⟩
 
-/-! Content below this point has not yet been aligned with `List`. -/
-
 /-! ### singleton -/
 
 @[simp] theorem singleton_def (v : α) : Array.singleton v = #[v] := rfl
 
 /-! ### append -/
 
+@[simp] theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
+  simp only [size, toList_append, List.length_append]
+
+@[simp] theorem append_push {as bs : Array α} {a : α} : as ++ bs.push a = (as ++ bs).push a := by
+  cases as
+  cases bs
+  simp
+
 @[simp] theorem toArray_eq_append_iff {xs : List α} {as bs : Array α} :
     xs.toArray = as ++ bs ↔ xs = as.toList ++ bs.toList := by
   cases as
@@ -1539,8 +1545,24 @@ theorem mem_append_left {a : α} {l₁ : Array α} (l₂ : Array α) (h : a ∈
 theorem mem_append_right {a : α} (l₁ : Array α) {l₂ : Array α} (h : a ∈ l₂) : a ∈ l₁ ++ l₂ :=
   mem_append.2 (Or.inr h)
 
-@[simp] theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
-  simp only [size, toList_append, List.length_append]
+theorem not_mem_append {a : α} {s t : Array α} (h₁ : a ∉ s) (h₂ : a ∉ t) : a ∉ s ++ t :=
+  mt mem_append.1 $ not_or.mpr ⟨h₁, h₂⟩
+
+/--
+See also `eq_push_append_of_mem`, which proves a stronger version
+in which the initial array must not contain the element.
+-/
+theorem append_of_mem {a : α} {l : Array α} (h : a ∈ l) : ∃ s t : Array α, l = s.push a ++ t := by
+  obtain ⟨s, t, w⟩ := List.append_of_mem (l := l.toList) (by simpa using h)
+  replace w := congrArg List.toArray w
+  refine ⟨s.toArray, t.toArray, by simp_all⟩
+
+theorem mem_iff_append {a : α} {l : Array α} : a ∈ l ↔ ∃ s t : Array α, l = s.push a ++ t :=
+  ⟨append_of_mem, fun ⟨s, t, e⟩ => e ▸ by simp⟩
+
+theorem forall_mem_append {p : α → Prop} {l₁ l₂ : Array α} :
+    (∀ (x) (_ : x ∈ l₁ ++ l₂), p x) ↔ (∀ (x) (_ : x ∈ l₁), p x) ∧ (∀ (x) (_ : x ∈ l₂), p x) := by
+  simp only [mem_append, or_imp, forall_and]
 
 theorem empty_append (as : Array α) : #[] ++ as = as := by simp
 
@@ -1599,6 +1621,194 @@ 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
+
+theorem append_inj {s₁ s₂ t₁ t₂ : Array α} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : s₁.size = s₂.size) :
+    s₁ = s₂ ∧ t₁ = t₂ := by
+  rcases s₁ with ⟨s₁⟩
+  rcases s₂ with ⟨s₂⟩
+  rcases t₁ with ⟨t₁⟩
+  rcases t₂ with ⟨t₂⟩
+  simpa using List.append_inj (by simpa using h) (by simpa using hl)
+
+theorem append_inj_right {s₁ s₂ t₁ t₂ : Array α}
+    (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : s₁.size = s₂.size) : t₁ = t₂ :=
+  (append_inj h hl).right
+
+theorem append_inj_left {s₁ s₂ t₁ t₂ : Array α}
+    (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : s₁.size = s₂.size) : s₁ = s₂ :=
+  (append_inj h hl).left
+
+/-- Variant of `append_inj` instead requiring equality of the sizes of the second arrays. -/
+theorem append_inj' {s₁ s₂ t₁ t₂ : Array α} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : t₁.size = t₂.size) :
+    s₁ = s₂ ∧ t₁ = t₂ :=
+  append_inj h <| @Nat.add_right_cancel _ t₁.size _ <| by
+    let hap := congrArg size h; simp only [size_append, ← hl] at hap; exact hap
+
+/-- Variant of `append_inj_right` instead requiring equality of the sizes of the second arrays. -/
+theorem append_inj_right' {s₁ s₂ t₁ t₂ : Array α}
+    (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : t₁.size = t₂.size) : t₁ = t₂ :=
+  (append_inj' h hl).right
+
+/-- Variant of `append_inj_left` instead requiring equality of the sizes of the second arrays. -/
+theorem append_inj_left' {s₁ s₂ t₁ t₂ : Array α}
+    (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : t₁.size = t₂.size) : s₁ = s₂ :=
+  (append_inj' h hl).left
+
+theorem append_right_inj {t₁ t₂ : Array α} (s) : s ++ t₁ = s ++ t₂ ↔ t₁ = t₂ :=
+  ⟨fun h => append_inj_right h rfl, congrArg _⟩
+
+theorem append_left_inj {s₁ s₂ : Array α} (t) : s₁ ++ t = s₂ ++ t ↔ s₁ = s₂ :=
+  ⟨fun h => append_inj_left' h rfl, congrArg (· ++ _)⟩
+
+@[simp] theorem append_left_eq_self {x y : Array α} : x ++ y = y ↔ x = #[] := by
+  rw [← append_left_inj (s₁ := x), nil_append]
+
+@[simp] theorem self_eq_append_left {x y : Array α} : y = x ++ y ↔ x = #[] := by
+  rw [eq_comm, append_left_eq_self]
+
+@[simp] theorem append_right_eq_self {x y : Array α} : x ++ y = x ↔ y = #[] := by
+  rw [← append_right_inj (t₁ := y), append_nil]
+
+@[simp] theorem self_eq_append_right {x y : Array α} : x = x ++ y ↔ y = #[] := by
+  rw [eq_comm, append_right_eq_self]
+
+@[simp] theorem append_eq_empty_iff : p ++ q = #[] ↔ p = #[] ∧ q = #[] := by
+  cases p <;> simp
+
+@[simp] theorem empty_eq_append_iff : #[] = a ++ b ↔ a = #[] ∧ b = #[] := by
+  rw [eq_comm, append_eq_empty_iff]
+
+theorem append_ne_empty_of_left_ne_empty {s : Array α} (h : s ≠ #[]) (t : Array α) :
+    s ++ t ≠ #[] := by
+  simp_all
+
+theorem append_ne_empty_of_right_ne_empty (s : Array α) : t ≠ #[] → s ++ t ≠ #[] := by
+  simp_all
+
+theorem append_eq_push_iff {a b c : Array α} {x : α} :
+    a ++ b = c.push x ↔ (b = #[] ∧ a = c.push x) ∨ (∃ b', b = b'.push x ∧ c = a ++ b') := by
+  rcases a with ⟨a⟩
+  rcases b with ⟨b⟩
+  rcases c with ⟨c⟩
+  simp only [List.append_toArray, List.push_toArray, mk.injEq, List.append_eq_append_iff,
+    toArray_eq_append_iff]
+  constructor
+  · rintro (⟨a', rfl, rfl⟩ | ⟨b', rfl, h⟩)
+    · right; exact ⟨⟨a'⟩, by simp⟩
+    · rw [List.singleton_eq_append_iff] at h
+      obtain (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩) := h
+      · right; exact ⟨#[], by simp⟩
+      · left; simp
+  · rintro (⟨rfl, rfl⟩ | ⟨b', h, rfl⟩)
+    · right; exact ⟨[x], by simp⟩
+    · left; refine ⟨b'.toList, ?_⟩
+      replace h := congrArg Array.toList h
+      simp_all
+
+theorem push_eq_append_iff {a b c : Array α} {x : α} :
+    c.push x = a ++ b ↔ (b = #[] ∧ a = c.push x) ∨ (∃ b', b = b'.push x ∧ c = a ++ b') := by
+  rw [eq_comm, append_eq_push_iff]
+
+theorem append_eq_singleton_iff {a b : Array α} {x : α} :
+    a ++ b = #[x] ↔ (a = #[] ∧ b = #[x]) ∨ (a = #[x] ∧ b = #[]) := by
+  rcases a with ⟨a⟩
+  rcases b with ⟨b⟩
+  simp only [List.append_toArray, mk.injEq, List.append_eq_singleton_iff, toArray_eq_append_iff]
+
+theorem singleton_eq_append_iff {a b : Array α} {x : α} :
+    #[x] = a ++ b ↔ (a = #[] ∧ b = #[x]) ∨ (a = #[x] ∧ b = #[]) := by
+  rw [eq_comm, append_eq_singleton_iff]
+
+theorem append_eq_append_iff {a b c d : Array α} :
+    a ++ b = c ++ d ↔ (∃ a', c = a ++ a' ∧ b = a' ++ d) ∨ ∃ c', a = c ++ c' ∧ d = c' ++ b := by
+  rcases a with ⟨a⟩
+  rcases b with ⟨b⟩
+  rcases c with ⟨c⟩
+  rcases d with ⟨d⟩
+  simp only [List.append_toArray, mk.injEq, List.append_eq_append_iff, toArray_eq_append_iff]
+  constructor
+  · rintro (⟨a', rfl, rfl⟩ | ⟨c', rfl, rfl⟩)
+    · left; exact ⟨⟨a'⟩, by simp⟩
+    · right; exact ⟨⟨c'⟩, by simp⟩
+  · rintro (⟨a', rfl, rfl⟩ | ⟨c', rfl, rfl⟩)
+    · left; exact ⟨a'.toList, by simp⟩
+    · right; exact ⟨c'.toList, by simp⟩
+
+theorem set_append {s t : Array α} {i : Nat} {x : α} (h : i < (s ++ t).size) :
+    (s ++ t).set i x =
+      if h' : i < s.size then
+        s.set i x ++ t
+      else
+        s ++ t.set (i - s.size) x (by simp at h; omega) := by
+  rcases s with ⟨s⟩
+  rcases t with ⟨t⟩
+  simp only [List.append_toArray, List.set_toArray, List.set_append]
+  split <;> simp
+
+@[simp] theorem set_append_left {s t : Array α} {i : Nat} {x : α} (h : i < s.size) :
+    (s ++ t).set i x (by simp; omega) = s.set i x ++ t := by
+  simp [set_append, h]
+
+@[simp] theorem set_append_right {s t : Array α} {i : Nat} {x : α}
+    (h' : i < (s ++ t).size) (h : s.size ≤ i) :
+    (s ++ t).set i x = s ++ t.set (i - s.size) x (by simp at h'; omega) := by
+  rw [set_append, dif_neg (by omega)]
+
+theorem setIfInBounds_append {s t : Array α} {i : Nat} {x : α} :
+    (s ++ t).setIfInBounds i x =
+      if i < s.size then
+        s.setIfInBounds i x ++ t
+      else
+        s ++ t.setIfInBounds (i - s.size) x := by
+  rcases s with ⟨s⟩
+  rcases t with ⟨t⟩
+  simp only [List.append_toArray, List.setIfInBounds_toArray, List.set_append]
+  split <;> simp
+
+@[simp] theorem setIfInBounds_append_left {s t : Array α} {i : Nat} {x : α} (h : i < s.size) :
+    (s ++ t).setIfInBounds i x = s.setIfInBounds i x ++ t := by
+  simp [setIfInBounds_append, h]
+
+@[simp] theorem setIfInBounds_append_right {s t : Array α} {i : Nat} {x : α} (h : s.size ≤ i) :
+    (s ++ t).setIfInBounds i x = s ++ t.setIfInBounds (i - s.size) x := by
+  rw [setIfInBounds_append, if_neg (by omega)]
+
+theorem filterMap_eq_append_iff {f : α → Option β} :
+    filterMap f l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂ := by
+  rcases l with ⟨l⟩
+  rcases L₁ with ⟨L₁⟩
+  rcases L₂ with ⟨L₂⟩
+  simp only [size_toArray, List.filterMap_toArray', List.append_toArray, mk.injEq,
+    List.filterMap_eq_append_iff, toArray_eq_append_iff]
+  constructor
+  · rintro ⟨l₁, l₂, rfl, rfl, rfl⟩
+    exact ⟨⟨l₁⟩, ⟨l₂⟩, by simp⟩
+  · rintro ⟨⟨l₁⟩, ⟨l₂⟩, rfl, h₁, h₂⟩
+    exact ⟨l₁, l₂, by simp_all⟩
+
+theorem append_eq_filterMap_iff {f : α → Option β} :
+    L₁ ++ L₂ = filterMap f l ↔
+      ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂ := by
+  rw [eq_comm, filterMap_eq_append_iff]
+
+@[simp] theorem map_append (f : α → β) (l₁ l₂ : Array α) :
+    map f (l₁ ++ l₂) = map f l₁ ++ map f l₂ := by
+  cases l₁
+  cases l₂
+  simp
+
+theorem map_eq_append_iff {f : α → β} :
+    map f l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂ := by
+  rw [← filterMap_eq_map, filterMap_eq_append_iff]
+
+theorem append_eq_map_iff {f : α → β} :
+    L₁ ++ L₂ = map f l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂ := by
+  rw [eq_comm, map_eq_append_iff]
+
+/-! Content below this point has not yet been aligned with `List`. -/
 
 -- This is a duplicate of `List.toArray_toList`.
 -- It's confusing to guess which namespace this theorem should live in,

src/Init/Data/List/Lemmas.lean

@@ -1494,6 +1494,34 @@ 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
 
+@[simp] theorem mem_append {a : α} {s t : List α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t := by
+  induction s <;> simp_all [or_assoc]
+
+theorem not_mem_append {a : α} {s t : List α} (h₁ : a ∉ s) (h₂ : a ∉ t) : a ∉ s ++ t :=
+  mt mem_append.1 $ not_or.mpr ⟨h₁, h₂⟩
+
+@[deprecated mem_append (since := "2025-01-13")]
+theorem mem_append_eq (a : α) (s t : List α) : (a ∈ s ++ t) = (a ∈ s ∨ a ∈ t) :=
+  propext mem_append
+
+@[deprecated mem_append_left (since := "2024-11-20")] abbrev mem_append_of_mem_left := @mem_append_left
+@[deprecated mem_append_right (since := "2024-11-20")] abbrev mem_append_of_mem_right := @mem_append_right
+
+/--
+See also `eq_append_cons_of_mem`, which proves a stronger version
+in which the initial list must not contain the element.
+-/
+theorem append_of_mem {a : α} {l : List α} : a ∈ l → ∃ s t : List α, l = s ++ a :: t
+  | .head l => ⟨[], l, rfl⟩
+  | .tail b h => let ⟨s, t, h'⟩ := append_of_mem h; ⟨b::s, t, by rw [h', cons_append]⟩
+
+theorem mem_iff_append {a : α} {l : List α} : a ∈ l ↔ ∃ s t : List α, l = s ++ a :: t :=
+  ⟨append_of_mem, fun ⟨s, t, e⟩ => e ▸ by simp⟩
+
+theorem forall_mem_append {p : α → Prop} {l₁ l₂ : List α} :
+    (∀ (x) (_ : x ∈ l₁ ++ l₂), p x) ↔ (∀ (x) (_ : x ∈ l₁), p x) ∧ (∀ (x) (_ : x ∈ l₂), p x) := by
+  simp only [mem_append, or_imp, forall_and]
+
 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'
@@ -1561,14 +1589,6 @@ theorem get_of_append {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.lengt
     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
 
-/--
-See also `eq_append_cons_of_mem`, which proves a stronger version
-in which the initial list must not contain the element.
--/
-theorem append_of_mem {a : α} {l : List α} : a ∈ l → ∃ s t : List α, l = s ++ a :: t
-  | .head l => ⟨[], l, rfl⟩
-  | .tail b h => let ⟨s, t, h'⟩ := append_of_mem h; ⟨b::s, t, by rw [h', cons_append]⟩
-
 @[simp 1100] theorem singleton_append : [x] ++ l = x :: l := rfl
 
 theorem append_inj :
@@ -1585,8 +1605,8 @@ theorem append_inj_left (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : length s₁ = le
 
 /-- Variant of `append_inj` instead requiring equality of the lengths of the second lists. -/
 theorem append_inj' (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : length t₁ = length t₂) : s₁ = s₂ ∧ t₁ = t₂ :=
-  append_inj h <| @Nat.add_right_cancel _ (length t₁) _ <| by
-  let hap := congrArg length h; simp only [length_append, ← hl] at hap; exact hap
+  append_inj h <| @Nat.add_right_cancel _ t₁.length _ <| by
+    let hap := congrArg length h; simp only [length_append, ← hl] at hap; exact hap
 
 /-- Variant of `append_inj_right` instead requiring equality of the lengths of the second lists. -/
 theorem append_inj_right' (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : length t₁ = length t₂) : t₁ = t₂ :=
@@ -1614,9 +1634,6 @@ theorem append_left_inj {s₁ s₂ : List α} (t) : s₁ ++ t = s₂ ++ t ↔ s
 @[simp] theorem self_eq_append_right {x y : List α} : x = x ++ y ↔ y = [] := by
   rw [eq_comm, append_right_eq_self]
 
-@[simp] theorem append_eq_nil : p ++ q = [] ↔ p = [] ∧ q = [] := by
-  cases p <;> simp
-
 theorem getLast_concat {a : α} : ∀ (l : List α), getLast (l ++ [a]) (by simp) = a
   | [] => rfl
   | a::t => by
@@ -1642,6 +1659,54 @@ theorem get?_append {l₁ l₂ : List α} {n : Nat} (hn : n < l₁.length) :
     (l₁ ++ l₂).get? n = l₁.get? n := by
   simp [getElem?_append_left hn]
 
+@[simp] theorem append_eq_nil_iff : p ++ q = [] ↔ p = [] ∧ q = [] := by
+  cases p <;> simp
+
+@[deprecated append_eq_nil_iff (since := "2025-01-13")] abbrev append_eq_nil := @append_eq_nil_iff
+
+@[simp] theorem nil_eq_append_iff : [] = a ++ b ↔ a = [] ∧ b = [] := by
+  rw [eq_comm, append_eq_nil_iff]
+
+@[deprecated nil_eq_append_iff (since := "2024-07-24")] abbrev nil_eq_append := @nil_eq_append_iff
+
+theorem append_ne_nil_of_left_ne_nil {s : List α} (h : s ≠ []) (t : List α) : s ++ t ≠ [] := by simp_all
+theorem append_ne_nil_of_right_ne_nil (s : List α) : t ≠ [] → s ++ t ≠ [] := by simp_all
+
+@[deprecated append_ne_nil_of_left_ne_nil (since := "2024-07-24")]
+theorem append_ne_nil_of_ne_nil_left {s : List α} (h : s ≠ []) (t : List α) : s ++ t ≠ [] := by simp_all
+@[deprecated append_ne_nil_of_right_ne_nil (since := "2024-07-24")]
+theorem append_ne_nil_of_ne_nil_right (s : List α) : t ≠ [] → s ++ t ≠ [] := by simp_all
+
+theorem append_eq_cons_iff :
+    a ++ b = x :: c ↔ (a = [] ∧ b = x :: c) ∨ (∃ a', a = x :: a' ∧ c = a' ++ b) := by
+  cases a with simp | cons a as => ?_
+  exact ⟨fun h => ⟨as, by simp [h]⟩, fun ⟨a', ⟨aeq, aseq⟩, h⟩ => ⟨aeq, by rw [aseq, h]⟩⟩
+
+@[deprecated append_eq_cons_iff (since := "2024-07-24")] abbrev append_eq_cons := @append_eq_cons_iff
+
+theorem cons_eq_append_iff :
+    x :: c = a ++ b ↔ (a = [] ∧ b = x :: c) ∨ (∃ a', a = x :: a' ∧ c = a' ++ b) := by
+  rw [eq_comm, append_eq_cons_iff]
+
+@[deprecated cons_eq_append_iff (since := "2024-07-24")] abbrev cons_eq_append := @cons_eq_append_iff
+
+theorem append_eq_singleton_iff :
+    a ++ b = [x] ↔ (a = [] ∧ b = [x]) ∨ (a = [x] ∧ b = []) := by
+  cases a <;> cases b <;> simp
+
+theorem singleton_eq_append_iff :
+    [x] = a ++ b ↔ (a = [] ∧ b = [x]) ∨ (a = [x] ∧ b = []) := by
+  cases a <;> cases b <;> simp [eq_comm]
+
+theorem append_eq_append_iff {a b c d : List α} :
+    a ++ b = c ++ d ↔ (∃ a', c = a ++ a' ∧ b = a' ++ d) ∨ ∃ c', a = c ++ c' ∧ d = c' ++ b := by
+  induction a generalizing c with
+  | nil => simp_all
+  | cons a as ih => cases c <;> simp [eq_comm, and_assoc, ih, and_or_left]
+
+@[deprecated append_inj (since := "2024-07-24")] abbrev append_inj_of_length_left := @append_inj
+@[deprecated append_inj' (since := "2024-07-24")] abbrev append_inj_of_length_right := @append_inj'
+
 @[simp] theorem head_append_of_ne_nil {l : List α} {w₁} (w₂) :
     head (l ++ l') w₁ = head l w₂ := by
   match l, w₂ with
@@ -1691,60 +1756,6 @@ theorem tail_append {l l' : List α} : (l ++ l').tail = if l.isEmpty then l'.tai
 
 @[deprecated tail_append_of_ne_nil (since := "2024-07-24")] abbrev tail_append_left := @tail_append_of_ne_nil
 
-theorem nil_eq_append_iff : [] = a ++ b ↔ a = [] ∧ b = [] := by
-  rw [eq_comm, append_eq_nil]
-
-@[deprecated nil_eq_append_iff (since := "2024-07-24")] abbrev nil_eq_append := @nil_eq_append_iff
-
-theorem append_ne_nil_of_left_ne_nil {s : List α} (h : s ≠ []) (t : List α) : s ++ t ≠ [] := by simp_all
-theorem append_ne_nil_of_right_ne_nil (s : List α) : t ≠ [] → s ++ t ≠ [] := by simp_all
-
-@[deprecated append_ne_nil_of_left_ne_nil (since := "2024-07-24")]
-theorem append_ne_nil_of_ne_nil_left {s : List α} (h : s ≠ []) (t : List α) : s ++ t ≠ [] := by simp_all
-@[deprecated append_ne_nil_of_right_ne_nil (since := "2024-07-24")]
-theorem append_ne_nil_of_ne_nil_right (s : List α) : t ≠ [] → s ++ t ≠ [] := by simp_all
-
-theorem append_eq_cons_iff :
-    a ++ b = x :: c ↔ (a = [] ∧ b = x :: c) ∨ (∃ a', a = x :: a' ∧ c = a' ++ b) := by
-  cases a with simp | cons a as => ?_
-  exact ⟨fun h => ⟨as, by simp [h]⟩, fun ⟨a', ⟨aeq, aseq⟩, h⟩ => ⟨aeq, by rw [aseq, h]⟩⟩
-
-@[deprecated append_eq_cons_iff (since := "2024-07-24")] abbrev append_eq_cons := @append_eq_cons_iff
-
-theorem cons_eq_append_iff :
-    x :: c = a ++ b ↔ (a = [] ∧ b = x :: c) ∨ (∃ a', a = x :: a' ∧ c = a' ++ b) := by
-  rw [eq_comm, append_eq_cons_iff]
-
-@[deprecated cons_eq_append_iff (since := "2024-07-24")] abbrev cons_eq_append := @cons_eq_append_iff
-
-theorem append_eq_append_iff {a b c d : List α} :
-    a ++ b = c ++ d ↔ (∃ a', c = a ++ a' ∧ b = a' ++ d) ∨ ∃ c', a = c ++ c' ∧ d = c' ++ b := by
-  induction a generalizing c with
-  | nil => simp_all
-  | cons a as ih => cases c <;> simp [eq_comm, and_assoc, ih, and_or_left]
-
-@[deprecated append_inj (since := "2024-07-24")] abbrev append_inj_of_length_left := @append_inj
-@[deprecated append_inj' (since := "2024-07-24")] abbrev append_inj_of_length_right := @append_inj'
-
-@[simp] theorem mem_append {a : α} {s t : List α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t := by
-  induction s <;> simp_all [or_assoc]
-
-theorem not_mem_append {a : α} {s t : List α} (h₁ : a ∉ s) (h₂ : a ∉ t) : a ∉ s ++ t :=
-  mt mem_append.1 $ not_or.mpr ⟨h₁, h₂⟩
-
-theorem mem_append_eq (a : α) (s t : List α) : (a ∈ s ++ t) = (a ∈ s ∨ a ∈ t) :=
-  propext mem_append
-
-@[deprecated mem_append_left (since := "2024-11-20")] abbrev mem_append_of_mem_left := @mem_append_left
-@[deprecated mem_append_right (since := "2024-11-20")] abbrev mem_append_of_mem_right := @mem_append_right
-
-theorem mem_iff_append {a : α} {l : List α} : a ∈ l ↔ ∃ s t : List α, l = s ++ a :: t :=
-  ⟨append_of_mem, fun ⟨s, t, e⟩ => e ▸ by simp⟩
-
-theorem forall_mem_append {p : α → Prop} {l₁ l₂ : List α} :
-    (∀ (x) (_ : x ∈ l₁ ++ l₂), p x) ↔ (∀ (x) (_ : x ∈ l₁), p x) ∧ (∀ (x) (_ : x ∈ l₂), p x) := by
-  simp only [mem_append, or_imp, forall_and]
-
 theorem set_append {s t : List α} :
     (s ++ t).set i x = if i < s.length then s.set i x ++ t else s ++ t.set (i - s.length) x := by
   induction s generalizing i with
@@ -1974,8 +1985,8 @@ theorem flatten_eq_append_iff {xs : List (List α)} {ys zs : List α} :
   constructor
   · induction xs generalizing ys with
     | nil =>
-      simp only [flatten_nil, nil_eq, append_eq_nil, and_false, cons_append, false_and, exists_const,
-        exists_false, or_false, and_imp, List.cons_ne_nil]
+      simp only [flatten_nil, nil_eq, append_eq_nil_iff, and_false, cons_append, false_and,
+        exists_const, exists_false, or_false, and_imp, List.cons_ne_nil]
       rintro rfl rfl
       exact ⟨[], [], by simp⟩
     | cons x xs ih =>

src/Init/Data/List/Zip.lean

@@ -203,11 +203,11 @@ theorem zipWith_eq_append_iff {f : α → β → γ} {l₁ : List α} {l₂ : Li
     cases l₂ with
     | nil =>
       constructor
-      · simp only [zipWith_nil_right, nil_eq, append_eq_nil, exists_and_left, and_imp]
+      · simp only [zipWith_nil_right, nil_eq, append_eq_nil_iff, exists_and_left, and_imp]
         rintro rfl  rfl
         exact ⟨[], x₁ :: l₁, [], by simp⟩
       · rintro ⟨w, x, y, z, h₁, _, h₃, rfl, rfl⟩
-        simp only [nil_eq, append_eq_nil] at h₃
+        simp only [nil_eq, append_eq_nil_iff] at h₃
         obtain ⟨rfl, rfl⟩ := h₃
         simp
     | cons x₂ l₂ =>

src/Init/Data/Vector/Lemmas.lean

@@ -693,6 +693,24 @@ theorem forall_getElem {l : Vector α n} {p : α → Prop} :
   rcases l with ⟨l, rfl⟩
   simp [Array.forall_getElem]
 
+
+/-! ### cast -/
+
+@[simp] theorem getElem_cast (a : Vector α n) (h : n = m) (i : Nat) (hi : i < m) :
+    (a.cast h)[i] = a[i] := by
+  cases a
+  simp
+
+@[simp] theorem getElem?_cast {l : Vector α n} {m : Nat} {w : n = m} {i : Nat} :
+    (l.cast w)[i]? = l[i]? := by
+  rcases l with ⟨l, rfl⟩
+  simp
+
+@[simp] theorem mem_cast {a : α} {l : Vector α n} {m : Nat} {w : n = m} :
+    a ∈ l.cast w ↔ a ∈ l := by
+  rcases l with ⟨l, rfl⟩
+  simp
+
 /-! ### Decidability of bounded quantifiers -/
 
 instance {xs : Vector α n} {p : α → Prop} [DecidablePred p] :
@@ -1167,6 +1185,227 @@ theorem map_eq_iff {f : α → β} {l : Vector α n} {l' : Vector β n} :
   cases as
   simp
 
+/-! ### singleton -/
+
+@[simp] theorem singleton_def (v : α) : Vector.singleton v = #v[v] := rfl
+
+/-! ### append -/
+
+@[simp] theorem append_push {as : Vector α n} {bs : Vector α m} {a : α} :
+    as ++ bs.push a = (as ++ bs).push a := by
+  cases as
+  cases bs
+  simp
+
+theorem singleton_eq_toVector_singleton (a : α) : #v[a] = #[a].toVector := rfl
+
+@[simp] theorem mem_append {a : α} {s : Vector α n} {t : Vector α m} :
+    a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t := by
+  cases s
+  cases t
+  simp
+
+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 :=
+  mem_append.2 (Or.inr h)
+
+theorem not_mem_append {a : α} {s : Vector α n} {t : Vector α m} (h₁ : a ∉ s) (h₂ : a ∉ t) :
+    a ∉ s ++ t :=
+  mt mem_append.1 $ not_or.mpr ⟨h₁, h₂⟩
+
+/--
+See also `eq_push_append_of_mem`, which proves a stronger version
+in which the initial array must not contain the element.
+-/
+theorem append_of_mem {a : α} {l : Vector α n} (h : a ∈ l) :
+    ∃ (m k : Nat) (w : m + 1 + k = n) (s : Vector α m) (t : Vector α k),
+      l = (s.push a ++ t).cast w := by
+  rcases l with ⟨l, rfl⟩
+  obtain ⟨s, t, rfl⟩ := Array.append_of_mem (by simpa using h)
+  refine ⟨_, _, by simp, s.toVector, t.toVector, by simp_all⟩
+
+theorem mem_iff_append {a : α} {l : Vector α n} :
+    a ∈ l ↔ ∃ (m k : Nat) (w : m + 1 + k = n) (s : Vector α m) (t : Vector α k),
+      l = (s.push a ++ t).cast w :=
+  ⟨append_of_mem, by rintro ⟨m, k, rfl, s, t, rfl⟩; simp⟩
+
+theorem forall_mem_append {p : α → Prop} {l₁ : Vector α n} {l₂ : Vector α m} :
+    (∀ (x) (_ : x ∈ l₁ ++ l₂), p x) ↔ (∀ (x) (_ : x ∈ l₁), p x) ∧ (∀ (x) (_ : x ∈ l₂), p x) := by
+  simp only [mem_append, or_imp, forall_and]
+
+theorem empty_append (as : Vector α n) : (#v[] : Vector α 0) ++ as = as.cast (by omega) := by
+  rcases as with ⟨as, rfl⟩
+  simp
+
+theorem append_empty (as : Vector α n) : as ++ (#v[] : Vector α 0) = as := by
+  rw [← toArray_inj, toArray_append, Array.append_nil]
+
+theorem getElem_append (a : Vector α n) (b : Vector α m) (i : Nat) (hi : i < n + m) :
+    (a ++ b)[i] = if h : i < n then a[i] else b[i - n] := by
+  rcases a with ⟨a, rfl⟩
+  rcases b with ⟨b, rfl⟩
+  simp [Array.getElem_append, hi]
+
+theorem getElem_append_left {a : Vector α n} {b : Vector α m} {i : Nat} (hi : i < n) :
+    (a ++ b)[i] = a[i] := by simp [getElem_append, hi]
+
+theorem getElem_append_right {a : Vector α n} {b : Vector α m} {i : Nat} (h : i < n + m) (hi : n ≤ i) :
+    (a ++ b)[i] = b[i - n] := by
+  rw [getElem_append, dif_neg (by omega)]
+
+theorem getElem?_append_left {as : Vector α n} {bs : Vector α m} {i : Nat} (hn : i < n) :
+    (as ++ bs)[i]? = as[i]? := by
+  have hn' : i < n + m := by omega
+  simp_all [getElem?_eq_getElem, getElem_append]
+
+theorem getElem?_append_right {as : Vector α n} {bs : Vector α m} {i : Nat} (h : n ≤ i) :
+    (as ++ bs)[i]? = bs[i - n]? := by
+  rcases as with ⟨as, rfl⟩
+  rcases bs with ⟨bs, rfl⟩
+  simp [Array.getElem?_append_right, h]
+
+theorem getElem?_append {as : Vector α n} {bs : Vector α m} {i : Nat} :
+    (as ++ bs)[i]? = if i < n then as[i]? else bs[i - n]? := by
+  split <;> rename_i h
+  · exact getElem?_append_left h
+  · exact getElem?_append_right (by simpa using h)
+
+/-- Variant of `getElem_append_left` useful for rewriting from the small array to the big array. -/
+theorem getElem_append_left' (l₁ : Vector α m) {l₂ : Vector α n} {i : Nat} (hi : i < m) :
+    l₁[i] = (l₁ ++ l₂)[i] := by
+  rw [getElem_append_left] <;> simp
+
+/-- Variant of `getElem_append_right` useful for rewriting from the small array to the big array. -/
+theorem getElem_append_right' (l₁ : Vector α m) {l₂ : Vector α n} {i : Nat} (hi : i < n) :
+    l₂[i] = (l₁ ++ l₂)[i + m] := by
+  rw [getElem_append_right] <;> simp [*, Nat.le_add_left]
+
+theorem getElem_of_append {l : Vector α n} {l₁ : Vector α m} {l₂ : Vector α k}
+    (w : m + 1 + k = n) (eq : l = (l₁.push a ++ l₂).cast w) :
+    l[m] = a := Option.some.inj <| by
+  rw [← getElem?_eq_getElem, eq, getElem?_cast, getElem?_append_left (by simp)]
+  simp
+
+@[simp 1100] theorem append_singleton {a : α} {as : Vector α n} : as ++ #v[a] = as.push a := by
+  cases as
+  simp
+
+theorem append_inj {s₁ s₂ : Vector α n} {t₁ t₂ : Vector α m} (h : s₁ ++ t₁ = s₂ ++ t₂) :
+    s₁ = s₂ ∧ t₁ = t₂ := by
+  rcases s₁ with ⟨s₁, rfl⟩
+  rcases s₂ with ⟨s₂, hs⟩
+  rcases t₁ with ⟨t₁, rfl⟩
+  rcases t₂ with ⟨t₂, ht⟩
+  simpa using Array.append_inj (by simpa using h) (by omega)
+
+theorem append_inj_right {s₁ s₂ : Vector α n} {t₁ t₂ : Vector α m}
+    (h : s₁ ++ t₁ = s₂ ++ t₂) : t₁ = t₂ :=
+  (append_inj h).right
+
+theorem append_inj_left {s₁ s₂ : Vector α n} {t₁ t₂ : Vector α m}
+    (h : s₁ ++ t₁ = s₂ ++ t₂) : s₁ = s₂ :=
+  (append_inj h).left
+
+theorem append_right_inj {t₁ t₂ : Vector α m} (s : Vector α n) : s ++ t₁ = s ++ t₂ ↔ t₁ = t₂ :=
+  ⟨fun h => append_inj_right h, congrArg _⟩
+
+theorem append_left_inj {s₁ s₂ : Vector α n} (t : Vector α m) : s₁ ++ t = s₂ ++ t ↔ s₁ = s₂ :=
+  ⟨fun h => append_inj_left h, congrArg (· ++ _)⟩
+
+theorem append_eq_append_iff {a : Vector α n} {b : Vector α m} {c : Vector α k} {d : Vector α l}
+    (w : k + l = n + m) :
+    a ++ b = (c ++ d).cast w ↔
+      if h : n ≤ k then
+        ∃ a' : Vector α (k - n), c = (a ++ a').cast (by omega) ∧ b = (a' ++ d).cast (by omega)
+      else
+        ∃ c' : Vector α (n - k), a = (c ++ c').cast (by omega) ∧ d = (c' ++ b).cast (by omega) := by
+  rcases a with ⟨a, rfl⟩
+  rcases b with ⟨b, rfl⟩
+  rcases c with ⟨c, rfl⟩
+  rcases d with ⟨d, rfl⟩
+  simp only [mk_append_mk, Array.append_eq_append_iff, mk_eq, toArray_cast]
+  constructor
+  · rintro (⟨a', rfl, rfl⟩ | ⟨c', rfl, rfl⟩)
+    · rw [dif_pos (by simp)]
+      exact ⟨a'.toVector.cast (by simp; omega), by simp⟩
+    · split <;> rename_i h
+      · have hc : c'.size = 0 := by simp at h; omega
+        simp at hc
+        exact ⟨#v[].cast (by simp; omega), by simp_all⟩
+      · exact ⟨c'.toVector.cast (by simp; omega), by simp⟩
+  · split <;> rename_i h
+    · rintro ⟨a', hc, rfl⟩
+      left
+      refine ⟨a'.toArray, hc, rfl⟩
+    · rintro ⟨c', ha, rfl⟩
+      right
+      refine ⟨c'.toArray, ha, rfl⟩
+
+theorem set_append {s : Vector α n} {t : Vector α m} {i : Nat} {x : α} (h : i < n + m) :
+    (s ++ t).set i x =
+      if h' : i < n then
+        s.set i x ++ t
+      else
+        s ++ t.set (i - n) x := by
+  rcases s with ⟨s, rfl⟩
+  rcases t with ⟨t, rfl⟩
+  simp only [mk_append_mk, set_mk, Array.set_append]
+  split <;> simp
+
+@[simp] theorem set_append_left {s : Vector α n} {t : Vector α m} {i : Nat} {x : α} (h : i < n) :
+    (s ++ t).set i x = s.set i x ++ t := by
+  simp [set_append, h]
+
+@[simp] theorem set_append_right {s : Vector α n} {t : Vector α m} {i : Nat} {x : α}
+    (h' : i < n + m) (h : n ≤ i) :
+    (s ++ t).set i x = s ++ t.set (i - n) x := by
+  rw [set_append, dif_neg (by omega)]
+
+theorem setIfInBounds_append {s : Vector α n} {t : Vector α m} {i : Nat} {x : α} :
+    (s ++ t).setIfInBounds i x =
+      if i < n then
+        s.setIfInBounds i x ++ t
+      else
+        s ++ t.setIfInBounds (i - n) x := by
+  rcases s with ⟨s, rfl⟩
+  rcases t with ⟨t, rfl⟩
+  simp only [mk_append_mk, setIfInBounds_mk, Array.setIfInBounds_append]
+  split <;> simp
+
+@[simp] theorem setIfInBounds_append_left {s : Vector α n} {t : Vector α m} {i : Nat} {x : α} (h : i < n) :
+    (s ++ t).setIfInBounds i x = s.setIfInBounds i x ++ t := by
+  simp [setIfInBounds_append, h]
+
+@[simp] theorem setIfInBounds_append_right {s : Vector α n} {t : Vector α m} {i : Nat} {x : α}
+    (h : n ≤ i) :
+    (s ++ t).setIfInBounds i x = s ++ t.setIfInBounds (i - n) x := by
+  rw [setIfInBounds_append, if_neg (by omega)]
+
+@[simp] theorem map_append (f : α → β) (l₁ : Vector α n) (l₂ : Vector α m) :
+    map f (l₁ ++ l₂) = map f l₁ ++ map f l₂ := by
+  rcases l₁ with ⟨l₁, rfl⟩
+  rcases l₂ with ⟨l₂, rfl⟩
+  simp
+
+theorem map_eq_append_iff {f : α → β} :
+    map f l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂ := by
+  rcases l with ⟨l, h⟩
+  rcases L₁ with ⟨L₁, rfl⟩
+  rcases L₂ with ⟨L₂, rfl⟩
+  simp only [map_mk, mk_append_mk, eq_mk, Array.map_eq_append_iff, mk_eq, toArray_append,
+    toArray_map]
+  constructor
+  · rintro ⟨l₁, l₂, rfl, rfl, rfl⟩
+    exact ⟨l₁.toVector.cast (by simp), l₂.toVector.cast (by simp), by simp⟩
+  · rintro ⟨⟨l₁⟩, ⟨l₂⟩, rfl, h₁, h₂⟩
+    exact ⟨l₁, l₂, by simp_all⟩
+
+theorem append_eq_map_iff {f : α → β} :
+    L₁ ++ L₂ = map f l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂ := by
+  rw [eq_comm, map_eq_append_iff]
+
 /-! 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) :
@@ -1197,28 +1436,6 @@ defeq issues in the implicit size argument.
     subst h
     simp [pop, back, back!, ← Array.eq_push_pop_back!_of_size_ne_zero]
 
-/-! ### append -/
-
-theorem getElem_append (a : Vector α n) (b : Vector α m) (i : Nat) (hi : i < n + m) :
-    (a ++ b)[i] = if h : i < n then a[i] else b[i - n] := by
-  rcases a with ⟨a, rfl⟩
-  rcases b with ⟨b, rfl⟩
-  simp [Array.getElem_append, hi]
-
-theorem getElem_append_left {a : Vector α n} {b : Vector α m} {i : Nat} (hi : i < n) :
-    (a ++ b)[i] = a[i] := by simp [getElem_append, hi]
-
-theorem getElem_append_right {a : Vector α n} {b : Vector α m} {i : Nat} (h : i < n + m) (hi : n ≤ i) :
-    (a ++ b)[i] = b[i - n] := by
-  rw [getElem_append, dif_neg (by omega)]
-
-/-! ### cast -/
-
-@[simp] theorem getElem_cast (a : Vector α n) (h : n = m) (i : Nat) (hi : i < m) :
-    (a.cast h)[i] = a[i] := by
-  cases a
-  simp
-
 /-! ### extract -/
 
 @[simp] theorem getElem_extract (a : Vector α n) (start stop) (i : Nat) (hi : i < min stop n - start) :