finish

src/Init/Data/Array/Lemmas.lean

diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index 2e98cfe..336bf8a 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -1046,7 +1046,7 @@
   cases xs
   simp [List.getLast?_eq_getElem?]
 
-@[simp] theorem back_mem{xs : Array α} (h : 0 < xs.size) : xs.back ∈ xs := by
+@[simp] theorem back_mem {xs : Array α} (h : 0 < xs.size) : xs.back h ∈ xs := by
   cases xs
   simp
 
@@ -3325,7 +3325,7 @@
   simp [List.getLast?_flatMap]
 
 theorem back?_flatten {xss : Array (Array α)} :
-    (flatten xss).back? = xss.reverse.findSome? fun l => l.back? := by
+    (flatten xss).back? = xss.reverse.findSome? fun xs => xs.back? := by
   simp [← flatMap_id, back?_flatMap]
 
 theorem back?_mkArray (a : α) (n : Nat) :

src/Init/Data/NeZero.lean

diff --git a/src/Init/Data/NeZero.lean b/src/Init/Data/NeZero.lean
index 6fba725..6cebc7b 100644
--- a/src/Init/Data/NeZero.lean
+++ b/src/Init/Data/NeZero.lean
@@ -40,3 +40,20 @@
 instance {p : Prop} [Decidable p] {n m : Nat} [NeZero n] [NeZero m] :
     NeZero (if p then n else m) := by
   split <;> infer_instance
+
+instance {n m : Nat} [h : NeZero n] : NeZero (n + m) where
+  out :=
+    match n, h, m with
+    | _ + 1, _, 0
+    | _ + 1, _, _ + 1 => fun h => nomatch h
+
+instance {n m : Nat} [h : NeZero m] : NeZero (n + m) where
+  out :=
+    match m, h, n with
+    | _ + 1, _, 0 => fun h => nomatch h
+    | _ + 1, _, _ + 1 => fun h => nomatch h
+
+instance {n m : Nat} [hn : NeZero n] [hm : NeZero m] : NeZero (n * m) where
+  out :=
+    match n, hn, m, hm with
+    | _ + 1, _, _ + 1, _ => fun h => nomatch h

src/Init/Data/Vector/Lemmas.lean

diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean
index b07c8b6..8449f64 100644
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -6,6 +6,7 @@
 prelude
 import Init.Data.Vector.Basic
 import Init.Data.Array.Attach
+import Init.Data.Array.Find
 
 /-!
 ## Vectors
@@ -1337,6 +1338,20 @@
   cases ys
   simp
 
+/-! ### back -/
+
+theorem back_eq_getElem [NeZero n] (xs : Vector α n) : xs.back = xs[n - 1]'(by have := NeZero.ne n; omega) := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.back_eq_getElem]
+
+theorem back?_eq_getElem? (xs : Vector α n) : xs.back? = xs[n - 1]? := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.back?_eq_getElem?]
+
+@[simp] theorem back_mem [NeZero n] {xs : Vector α n} : xs.back ∈ xs := by
+  cases xs
+  simp
+
 /-! ### map -/
 
 @[simp] theorem getElem_map (f : α → β) (xs : Vector α n) (i : Nat) (hi : i < n) :
@@ -2331,6 +2346,90 @@
   rcases xs with ⟨xs⟩
   simp
 
+/-! #### Further results about `back` and `back?` -/
+
+@[simp] theorem back?_eq_none_iff {xs : Vector α n} : xs.back? = none ↔ n = 0 := by
+  rcases xs with ⟨xs, rfl⟩
+  simp
+
+theorem back?_eq_some_iff {xs : Vector α n} {a : α} :
+    xs.back? = some a ↔ ∃ (w : 0 < n)(ys : Vector α (n - 1)), xs = (ys.push a).cast (by omega) := by
+  rcases xs with ⟨xs, rfl⟩
+  simp only [back?_mk, Array.back?_eq_some_iff, mk_eq, toArray_cast, toArray_push]
+  constructor
+  · rintro ⟨ys, rfl⟩
+    simp
+    exact ⟨⟨ys, by simp⟩, by simp⟩
+  · rintro ⟨w, ⟨ys, h₁⟩, h₂⟩
+    exact ⟨ys, by simpa using h₂⟩
+
+@[simp] theorem back?_isSome {xs : Vector α n} : xs.back?.isSome ↔ n ≠ 0 := by
+  rcases xs with ⟨xs, rfl⟩
+  simp
+
+@[simp] theorem back_append_of_neZero {xs : Vector α n} {ys : Vector α m} [NeZero m] :
+    (xs ++ ys).back = ys.back := by
+  rcases xs with ⟨l⟩
+  rcases ys with ⟨l'⟩
+  simp only [mk_append_mk, back_mk]
+  rw [Array.back_append_of_size_pos]
+
+theorem back_append {xs : Vector α n} {ys : Vector α m} [NeZero (n + m)] :
+    (xs ++ ys).back =
+      if h' : m = 0 then
+        have : NeZero n := by subst h'; simp_all
+        xs.back
+      else
+        have : NeZero m := ⟨h'⟩
+        ys.back := by
+  rcases xs with ⟨xs, rfl⟩
+  rcases ys with ⟨ys, rfl⟩
+  simp [Array.back_append]
+  split <;> rename_i h
+  · rw [dif_pos]
+    simp_all
+  · rw [dif_neg]
+    rwa [Array.isEmpty_iff_size_eq_zero] at h
+
+theorem back_append_right {xs : Vector α n} {ys : Vector α m} [NeZero m] :
+    (xs ++ ys).back = ys.back := by
+  rcases xs with ⟨xs⟩
+  rcases ys with ⟨ys⟩
+  simp only [mk_append_mk, back_mk]
+  rw [Array.back_append_right]
+
+theorem back_append_left {xs : Vector α n} {ys : Vector α 0} [NeZero n] :
+    (xs ++ ys).back = xs.back := by
+  rcases xs with ⟨xs, rfl⟩
+  rcases ys with ⟨ys, h⟩
+  simp only [mk_append_mk, back_mk]
+  rw [Array.back_append_left _ h]
+
+@[simp] theorem back?_append {xs : Vector α n} {ys : Vector α m} : (xs ++ ys).back? = ys.back?.or xs.back? := by
+  rcases xs with ⟨xs, rfl⟩
+  rcases ys with ⟨ys, rfl⟩
+  simp
+
+theorem back?_flatMap {xs : Vector α n} {f : α → Vector β m} :
+    (xs.flatMap f).back? = xs.reverse.findSome? fun a => (f a).back? := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.back?_flatMap]
+  rfl
+
+theorem back?_flatten {xss : Vector (Vector α m) n} :
+    (flatten xss).back? = xss.reverse.findSome? fun xs => xs.back? := by
+  rcases xss with ⟨xss, rfl⟩
+  simp [Array.back?_flatten, ← Array.map_reverse, Array.findSome?_map, Function.comp_def]
+  rfl
+
+theorem back?_mkVector (a : α) (n : Nat) :
+    (mkVector n a).back? = if n = 0 then none else some a := by
+  rw [mkVector_eq_mk_mkArray]
+  simp only [back?_mk, Array.back?_mkArray]
+
+@[simp] theorem back_mkArray [NeZero n] : (mkVector n a).back = a := by
+  simp [back_eq_getElem]
+
 /-! ### leftpad and rightpad -/
 
 @[simp] theorem leftpad_mk (n : Nat) (a : α) (xs : Array α) (h : xs.size = m) :