feat: getElem_tail lemmas (#905)

Co-authored-by: François G. Dorais <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>

Author: 3 people

Batteries/Data/List/Lemmas.lean

@@ -228,6 +228,17 @@ theorem get?_set_of_lt' (a : α) {m n} (l : List α) (h : m < length l) :
 
 @[deprecated (since := "2024-05-06")] alias length_removeNth := length_eraseIdx
 
+/-! ### tail -/
+
+theorem length_tail_add_one (l : List α) (h : 0 < length l) : (length (tail l)) + 1 = length l := by
+  simp [Nat.sub_add_cancel h]
+
+@[simp] theorem getElem?_tail (l : List α) : l.tail[n]? = l[n + 1]? := by cases l <;> simp
+
+@[simp] theorem getElem_tail (l : List α) (h : n < l.tail.length) :
+    l.tail[n] = l[n + 1]'(by simp at h; omega) := by
+  cases l; contradiction; simp
+
 /-! ### eraseP -/
 
 @[simp] theorem extractP_eq_find?_eraseP

lake-manifest.json

@@ -1,4 +1,4 @@
-{"version": "1.0.0",
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages": [],
  "name": "batteries",