merge master

src/Init/Data/Array/Lemmas.lean

@@ -14,7 +14,7 @@ import Init.TacticsExtra
 /-!
 ## Bootstrapping theorems about arrays
 
-This file contains some theorems about `Array` and `List` needed for `Std.List.Basic`.
+This file contains some theorems about `Array` and `List` needed for `Init.Data.List.Impl`.
 -/
 
 namespace Array
@@ -34,9 +34,13 @@ attribute [simp] data_toArray uset
 
 @[simp] theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size]
 
-theorem getElem_eq_data_get (a : Array α) (h : i < a.size) : a[i] = a.data.get ⟨i, h⟩ := by
+theorem getElem_eq_data_getElem (a : Array α) (h : i < a.size) : a[i] = a.data[i] := by
   by_cases i < a.size <;> (try simp [*]) <;> rfl
 
+@[deprecated getElem_eq_data_getElem (since := "2024-06-12")]
+theorem getElem_eq_data_get (a : Array α) (h : i < a.size) : a[i] = a.data.get ⟨i, h⟩ := by
+  simp [getElem_eq_data_getElem]
+
 theorem foldlM_eq_foldlM_data.aux [Monad m]
     (f : β → α → m β) (arr : Array α) (i j) (H : arr.size ≤ i + j) (b) :
     foldlM.loop f arr arr.size (Nat.le_refl _) i j b = (arr.data.drop j).foldlM f b := by
@@ -114,11 +118,11 @@ theorem foldr_push (f : α → β → β) (init : β) (arr : Array α) (a : α)
 theorem get_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]
     (a.push x)[i] = a[i] := by
-  simp only [push, getElem_eq_data_get, List.concat_eq_append, List.get_append_left, h]
+  simp only [push, getElem_eq_data_getElem, List.concat_eq_append, List.getElem_append_left, h]
 
 @[simp] theorem get_push_eq (a : Array α) (x : α) : (a.push x)[a.size] = x := by
-  simp only [push, getElem_eq_data_get, List.concat_eq_append]
-  rw [List.get_append_right] <;> simp [getElem_eq_data_get, Nat.zero_lt_one]
+  simp only [push, getElem_eq_data_getElem, List.concat_eq_append]
+  rw [List.getElem_append_right] <;> simp [getElem_eq_data_getElem, Nat.zero_lt_one]
 
 theorem get_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) :
     (a.push x)[i] = if h : i < a.size then a[i] else x := by
@@ -233,11 +237,11 @@ theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default
 @[simp] theorem getElem_set_eq (a : Array α) (i : Fin a.size) (v : α) {j : Nat}
       (eq : i.val = j) (p : j < (a.set i v).size) :
     (a.set i v)[j]'p = v := by
-  simp [set, getElem_eq_data_get, ←eq]
+  simp [set, getElem_eq_data_getElem, ←eq]
 
 @[simp] theorem getElem_set_ne (a : Array α) (i : Fin a.size) (v : α) {j : Nat} (pj : j < (a.set i v).size)
     (h : i.val ≠ j) : (a.set i v)[j]'pj = a[j]'(size_set a i v ▸ pj) := by
-  simp only [set, getElem_eq_data_get, List.get_set_ne _ h]
+  simp only [set, getElem_eq_data_getElem, List.getElem_set_ne _ h]
 
 theorem getElem_set (a : Array α) (i : Fin a.size) (v : α) (j : Nat)
     (h : j < (a.set i v).size) :
@@ -321,7 +325,7 @@ termination_by n - i
 @[simp] theorem mkArray_data (n : Nat) (v : α) : (mkArray n v).data = List.replicate n v := rfl
 
 @[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) :
-    (mkArray n v)[i] = v := by simp [Array.getElem_eq_data_get]
+    (mkArray n v)[i] = v := by simp [Array.getElem_eq_data_getElem]
 
 /-- # mem -/
 
@@ -332,7 +336,7 @@ theorem not_mem_nil (a : α) : ¬ a ∈ #[] := nofun
 /-- # get lemmas -/
 
 theorem getElem?_mem {l : Array α} {i : Fin l.size} : l[i] ∈ l := by
-  erw [Array.mem_def, getElem_eq_data_get]
+  erw [Array.mem_def, getElem_eq_data_getElem]
   apply List.get_mem
 
 theorem getElem_fin_eq_data_get (a : Array α) (i : Fin _) : a[i] = a.data.get i := rfl
@@ -347,7 +351,7 @@ theorem get?_len_le (a : Array α) (i : Nat) (h : a.size ≤ i) : a[i]? = none :
   simp [getElem?_neg, h]
 
 theorem getElem_mem_data (a : Array α) (h : i < a.size) : a[i] ∈ a.data := by
-  simp only [getElem_eq_data_get, List.get_mem]
+  simp only [getElem_eq_data_getElem, List.getElem_mem]
 
 theorem getElem?_eq_data_get? (a : Array α) (i : Nat) : a[i]? = a.data.get? i := by
   by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg, List.get?_eq_get, eq_comm]; rfl
@@ -395,7 +399,7 @@ theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x el
 
 theorem get_set_eq (a : Array α) (i : Fin a.size) (v : α) :
     (a.set i v)[i.1] = v := by
-  simp only [set, getElem_eq_data_get, List.get_set_eq]
+  simp only [set, getElem_eq_data_getElem, List.getElem_set_eq]
 
 theorem get?_set_eq (a : Array α) (i : Fin a.size) (v : α) :
     (a.set i v)[i.1]? = v := by simp [getElem?_pos, i.2]
@@ -414,7 +418,7 @@ theorem get_set (a : Array α) (i : Fin a.size) (j : Nat) (hj : j < a.size) (v :
 
 @[simp] theorem get_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α) (hj : j < a.size)
     (h : i.1 ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
-  simp only [set, getElem_eq_data_get, List.get_set_ne _ h]
+  simp only [set, getElem_eq_data_getElem, List.getElem_set_ne _ h]
 
 theorem getElem_setD (a : Array α) (i : Nat) (v : α) (h : i < (setD a i v).size) :
   (setD a i v)[i] = v := by
@@ -452,7 +456,7 @@ theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
 
 @[simp] theorem getElem_pop (a : Array α) (i : Nat) (hi : i < a.pop.size) :
     a.pop[i] = a[i]'(Nat.lt_of_lt_of_le (a.size_pop ▸ hi) (Nat.sub_le _ _)) :=
-  List.get_dropLast ..
+  List.getElem_dropLast ..
 
 theorem eq_empty_of_size_eq_zero {as : Array α} (h : as.size = 0) : as = #[] := by
   apply ext
@@ -500,6 +504,7 @@ theorem size_eq_length_data (as : Array α) : as.size = as.data.length := rfl
     simp only [mkEmpty_eq, size_push] at *
     omega
 
+set_option linter.deprecated false in
 @[simp] theorem reverse_data (a : Array α) : a.reverse.data = a.data.reverse := by
   let rec go (as : Array α) (i j hj)
       (h : i + j + 1 = a.size) (h₂ : as.size = a.size)
@@ -517,10 +522,10 @@ theorem size_eq_length_data (as : Array α) : as.size = as.data.length := rfl
         simp only [H, getElem_eq_data_get, ← List.get?_eq_get, Nat.le_of_lt h₁, getElem?_eq_data_get?]
         split <;> rename_i h₂
         · simp only [← h₂, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, and_false]
-          exact (List.get?_reverse' _ _ (Eq.trans (by simp_arith) h)).symm
+          exact (List.get?_reverse' (j+1) i (Eq.trans (by simp_arith) h)).symm
         split <;> rename_i h₃
         · simp only [← h₃, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, false_and]
-          exact (List.get?_reverse' _ _ (Eq.trans (by simp_arith) h)).symm
+          exact (List.get?_reverse' i (j+1) (Eq.trans (by simp_arith) h)).symm
         simp only [Nat.succ_le, Nat.lt_iff_le_and_ne.trans (and_iff_left h₃),
           Nat.lt_succ.symm.trans (Nat.lt_iff_le_and_ne.trans (and_iff_left (Ne.symm h₂)))]
     · rw [H]; split <;> rename_i h₂
@@ -533,7 +538,7 @@ theorem size_eq_length_data (as : Array α) : as.size = as.data.length := rfl
   split
   · match a with | ⟨[]⟩ | ⟨[_]⟩ => rfl
   · have := Nat.sub_add_cancel (Nat.le_of_not_le ‹_›)
-    refine List.ext <| go _ _ _ _ (by simp [this]) rfl fun k => ?_
+    refine List.ext_get? <| go _ _ _ _ (by simp [this]) rfl fun k => ?_
     split
     · rfl
     · rename_i h
@@ -769,17 +774,17 @@ theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size :=
 
 theorem get_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
     (as ++ bs)[i] = as[i] := by
-  simp only [getElem_eq_data_get]
+  simp only [getElem_eq_data_getElem]
   have h' : i < (as.data ++ bs.data).length := by rwa [← data_length, append_data] at h
-  conv => rhs; rw [← List.get_append_left (bs:=bs.data) (h':=h')]
+  conv => rhs; rw [← List.getElem_append_left (bs := bs.data) (h' := h')]
   apply List.get_of_eq; rw [append_data]
 
 theorem get_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i)
     (hlt : i - as.size < bs.size := Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h)) :
     (as ++ bs)[i] = bs[i - as.size] := by
-  simp only [getElem_eq_data_get]
+  simp only [getElem_eq_data_getElem]
   have h' : i < (as.data ++ bs.data).length := by rwa [← data_length, append_data] at h
-  conv => rhs; rw [← List.get_append_right (h':=h') (h:=Nat.not_lt_of_ge hle)]
+  conv => rhs; rw [← List.getElem_append_right (h' := h') (h := Nat.not_lt_of_ge hle)]
   apply List.get_of_eq; rw [append_data]
 
 @[simp] theorem append_nil (as : Array α) : as ++ #[] = as := by
@@ -987,13 +992,13 @@ theorem all_eq_true (p : α → Bool) (as : Array α) : all as p ↔ ∀ i : Fin
   simp [all_iff_forall, Fin.isLt]
 
 theorem all_def {p : α → Bool} (as : Array α) : as.all p = as.data.all p := by
-  rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true]; simp only [List.mem_iff_get]
+  rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true]; simp only [List.mem_iff_getElem]
   constructor
-  · rintro w x ⟨r, rfl⟩
-    rw [← getElem_eq_data_get]
-    apply w
+  · rintro w x ⟨r, h, rfl⟩
+    rw [← getElem_eq_data_getElem]
+    exact w ⟨r, h⟩
   · intro w i
-    exact w as[i] ⟨i, (getElem_eq_data_get as i.2).symm⟩
+    exact w as[i] ⟨i, i.2, (getElem_eq_data_getElem as i.2).symm⟩
 
 theorem all_eq_true_iff_forall_mem {l : Array α} : l.all p ↔ ∀ x, x ∈ l → p x := by
   simp only [all_def, List.all_eq_true, mem_def]

src/Init/Data/List/BasicAux.lean

@@ -44,13 +44,15 @@ See also `get?` and `get!`.
 def getD (as : List α) (i : Nat) (fallback : α) : α :=
   (as.get? i).getD fallback
 
-@[ext] theorem ext : ∀ {l₁ l₂ : List α}, (∀ n, l₁.get? n = l₂.get? n) → l₁ = l₂
+theorem ext_get? : ∀ {l₁ l₂ : List α}, (∀ n, l₁.get? n = l₂.get? n) → l₁ = l₂
   | [], [], _ => rfl
   | a :: l₁, [], h => nomatch h 0
   | [], a' :: l₂, h => nomatch h 0
   | a :: l₁, a' :: l₂, h => by
     have h0 : some a = some a' := h 0
-    injection h0 with aa; simp only [aa, ext fun n => h (n+1)]
+    injection h0 with aa; simp only [aa, ext_get? fun n => h (n+1)]
+
+@[deprecated (since := "2024-06-07")] abbrev ext := @ext_get?
 
 /--
 Returns the first element in the list.
@@ -191,7 +193,7 @@ def rotateRight (xs : List α) (n : Nat := 1) : List α :=
     let e := xs.drop n
     e ++ b
 
-theorem get_append_left (as bs : List α) (h : i < as.length) {h'} : (as ++ bs).get ⟨i, h'⟩ = as.get ⟨i, h⟩ := by
+theorem getElem_append_left (as bs : List α) (h : i < as.length) {h'} : (as ++ bs)[i] = as[i] := by
   induction as generalizing i with
   | nil => trivial
   | cons a as ih =>
@@ -199,7 +201,7 @@ theorem get_append_left (as bs : List α) (h : i < as.length) {h'} : (as ++ bs).
     | zero => rfl
     | succ i => apply ih
 
-theorem get_append_right (as bs : List α) (h : ¬ i < as.length) {h' h''} : (as ++ bs).get ⟨i, h'⟩ = bs.get ⟨i - as.length, h''⟩ := by
+theorem getElem_append_right (as bs : List α) (h : ¬ i < as.length) {h' h''} : (as ++ bs)[i]'h' = bs[i - as.length]'h'' := by
   induction as generalizing i with
   | nil => trivial
   | cons a as ih =>

src/Init/Data/List/Lemmas.lean

@@ -41,6 +41,64 @@ attribute [simp] concat_eq_append append_assoc
 @[simp] theorem and_nil : [].and = true := rfl
 @[simp] theorem and_cons : (a::l).and = (a && l.and) := rfl
 
+theorem get?_len_le : ∀ {l : List α} {n}, length l ≤ n → l.get? n = none
+  | [], _, _ => rfl
+  | _ :: l, _+1, h => get?_len_le (l := l) <| Nat.le_of_succ_le_succ h
+
+theorem get?_eq_get : ∀ {l : List α} {n} (h : n < l.length), l.get? n = some (get l ⟨n, h⟩)
+  | _ :: _, 0, _ => rfl
+  | _ :: l, _+1, _ => get?_eq_get (l := l) _
+
+theorem get?_eq_some : l.get? n = some a ↔ ∃ h, get l ⟨n, h⟩ = a :=
+  ⟨fun e =>
+    have : n < length l := Nat.gt_of_not_le fun hn => by cases get?_len_le hn ▸ e
+    ⟨this, by rwa [get?_eq_get this, Option.some.injEq] at e⟩,
+  fun ⟨h, e⟩ => e ▸ get?_eq_get _⟩
+
+theorem get?_eq_none : l.get? n = none ↔ length l ≤ n :=
+  ⟨fun e => Nat.ge_of_not_lt (fun h' => by cases e ▸ get?_eq_some.2 ⟨h', rfl⟩), get?_len_le⟩
+
+@[simp] theorem get?_eq_getElem? (l : List α) (i : Nat) : l.get? i = l[i]? := by
+  simp only [getElem?]; split
+  · exact (get?_eq_get ‹_›)
+  · exact (get?_eq_none.2 <| Nat.not_lt.1 ‹_›)
+
+@[simp] theorem get_eq_getElem (l : List α) (i : Fin l.length) : l.get i = l[i.1]'i.2 := rfl
+
+@[simp] theorem getElem?_nil {n : Nat} : ([] : List α)[n]? = none := rfl
+
+@[simp] theorem getElem?_cons_zero {l : List α} : (a::l)[0]? = some a := by
+  simp only [← get?_eq_getElem?]
+  rfl
+
+@[simp] theorem getElem?_cons_succ {l : List α} : (a::l)[n+1]? = l[n]? := by
+  simp only [← get?_eq_getElem?]
+  rfl
+
+theorem getElem?_len_le : ∀ {l : List α} {n}, length l ≤ n → l[n]? = none
+  | [], _, _ => rfl
+  | _ :: l, _+1, h => by
+    rw [getElem?_cons_succ, getElem?_len_le (l := l) <| Nat.le_of_succ_le_succ h]
+
+theorem getElem?_eq_getElem {l : List α} {n} (h : n < l.length) : l[n]? = some l[n] := by
+  simp only [← get?_eq_getElem?, get?_eq_get, h, get_eq_getElem]
+
+theorem getElem?_eq_some {l : List α} : l[n]? = some a ↔ ∃ h : n < l.length, l[n] = a := by
+  simp only [← get?_eq_getElem?, get?_eq_some, get_eq_getElem]
+
+@[simp] theorem getElem?_eq_none : l[n]? = none ↔ length l ≤ n := by
+  simp only [← get?_eq_getElem?, get?_eq_none]
+
+@[simp] theorem getElem!_nil [Inhabited α] {n : Nat} : ([] : List α)[n]! = default := rfl
+
+@[simp] theorem getElem!_cons_zero [Inhabited α] {l : List α} : (a::l)[0]! = a := by
+  rw [getElem!_pos] <;> simp
+
+@[simp] theorem getElem!_cons_succ [Inhabited α] {l : List α} : (a::l)[n+1]! = l[n]! := by
+  by_cases h : n < 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]
+
 /-! ### length -/
 
 theorem eq_nil_of_length_eq_zero (_ : length l = 0) : l = [] := match l with | [] => rfl
@@ -100,10 +158,23 @@ theorem append_left_inj {s₁ s₂ : List α} (t) : s₁ ++ t = s₂ ++ t ↔ s
 @[simp] theorem append_eq_nil : p ++ q = [] ↔ p = [] ∧ q = [] := by
   cases p <;> simp
 
-theorem get_append : ∀ {l₁ l₂ : List α} (n : Nat) (h : n < l₁.length),
-    (l₁ ++ l₂).get ⟨n, length_append .. ▸ Nat.lt_add_right _ h⟩ = l₁.get ⟨n, h⟩
+theorem getElem_append : ∀ {l₁ l₂ : List α} (n : Nat) (h : n < l₁.length),
+    (l₁ ++ l₂)[n]'(length_append .. ▸ Nat.lt_add_right _ h) = l₁[n]
 | a :: l, _, 0, h => rfl
-| a :: l, _, n+1, h => by simp only [get, cons_append]; apply get_append
+| a :: l, _, n+1, h => by simp only [get, cons_append]; apply getElem_append
+
+@[deprecated getElem_append (since := "2024-06-12")]
+theorem get_append {l₁ l₂ : List α} (n : Nat) (h : n < l₁.length) :
+    (l₁ ++ l₂).get ⟨n, length_append .. ▸ Nat.lt_add_right _ h⟩ = l₁.get ⟨n, h⟩ := by
+  simp [getElem_append, h]
+
+@[deprecated getElem_append_left (since := "2024-06-12")]
+theorem get_append_left (as bs : List α) (h : i < as.length) {h'} : (as ++ bs).get ⟨i, h'⟩ = as.get ⟨i, h⟩ := by
+  simp [getElem_append_left, h, h']
+
+@[deprecated getElem_append_right (since := "2024-06-12")]
+theorem get_append_right (as bs : List α) (h : ¬ i < as.length) {h' h''} : (as ++ bs).get ⟨i, h'⟩ = bs.get ⟨i - as.length, h''⟩ := by
+  simp [getElem_append_right, h, h', h'']
 
 /-! ### map -/
 
@@ -171,48 +242,56 @@ theorem reverse_map (f : α → β) (l : List α) : (l.map f).reverse = l.revers
 
 /-! ### nth element -/
 
-theorem get_of_mem : ∀ {a} {l : List α}, a ∈ l → ∃ n, get l n = a
-  | _, _ :: _, .head .. => ⟨⟨0, Nat.succ_pos _⟩, rfl⟩
-  | _, _ :: _, .tail _ m => let ⟨⟨n, h⟩, e⟩ := get_of_mem m; ⟨⟨n+1, Nat.succ_lt_succ h⟩, e⟩
+theorem getElem_of_mem : ∀ {a} {l : List α}, a ∈ l → ∃ (n : Nat) (h : n < l.length), l[n]'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⟩
+
+theorem get_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n, get l n = a := by
+  obtain ⟨n, h, e⟩ := getElem_of_mem h
+  exact ⟨⟨n, h⟩, e⟩
+
+theorem getElem_mem : ∀ (l : List α) n (h : n < l.length), l[n]'h ∈ l
+  | _ :: _, 0, _ => .head ..
+  | _ :: l, _+1, _ => .tail _ (getElem_mem l ..)
 
 theorem get_mem : ∀ (l : List α) n h, get l ⟨n, h⟩ ∈ l
   | _ :: _, 0, _ => .head ..
   | _ :: l, _+1, _ => .tail _ (get_mem l ..)
 
+theorem mem_iff_getElem {a} {l : List α} : a ∈ l ↔ ∃ (n : Nat) (h : n < l.length), l[n]'h = a :=
+  ⟨getElem_of_mem, fun ⟨_, _, e⟩ => e ▸ getElem_mem ..⟩
+
 theorem mem_iff_get {a} {l : List α} : a ∈ l ↔ ∃ n, get l n = a :=
   ⟨get_of_mem, fun ⟨_, e⟩ => e ▸ get_mem ..⟩
 
-theorem get?_len_le : ∀ {l : List α} {n}, length l ≤ n → l.get? n = none
-  | [], _, _ => rfl
-  | _ :: l, _+1, h => get?_len_le (l := l) <| Nat.le_of_succ_le_succ h
+@[simp] theorem getElem?_map (f : α → β) : ∀ (l : List α) (n : Nat), (map f l)[n]? = Option.map f l[n]?
+  | [], _ => rfl
+  | _ :: _, 0 => by simp
+  | _ :: l, n+1 => by simp [getElem?_map f l n]
 
-theorem get?_eq_get : ∀ {l : List α} {n} (h : n < l.length), l.get? n = some (get l ⟨n, h⟩)
-  | _ :: _, 0, _ => rfl
-  | _ :: l, _+1, _ => get?_eq_get (l := l) _
-
-theorem get?_eq_some : l.get? n = some a ↔ ∃ h, get l ⟨n, h⟩ = a :=
-  ⟨fun e =>
-    have : n < length l := Nat.gt_of_not_le fun hn => by cases get?_len_le hn ▸ e
-    ⟨this, by rwa [get?_eq_get this, Option.some.injEq] at e⟩,
-  fun ⟨h, e⟩ => e ▸ get?_eq_get _⟩
-
-@[simp] theorem get?_eq_none : l.get? n = none ↔ length l ≤ n :=
-  ⟨fun e => Nat.ge_of_not_lt (fun h' => by cases e ▸ get?_eq_some.2 ⟨h', rfl⟩), get?_len_le⟩
-
-@[simp] theorem get?_map (f : α → β) : ∀ l n, (map f l).get? n = (l.get? n).map f
+@[deprecated getElem?_map (since := "2024-06-12")]
+theorem get?_map (f : α → β) : ∀ l n, (map f l).get? n = (l.get? n).map f
   | [], _ => rfl
   | _ :: _, 0 => rfl
   | _ :: l, n+1 => get?_map f l n
 
-theorem get?_append {l₁ l₂ : List α} {n : Nat} (hn : n < l₁.length) :
-  (l₁ ++ l₂).get? n = l₁.get? n := by
+theorem getElem?_append {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 <|
     length_append .. ▸ Nat.le_add_right ..
-  rw [get?_eq_get hn, get?_eq_get hn', get_append]
+  simp_all [getElem?_eq_getElem, getElem_append]
 
-@[simp] theorem get?_concat_length : ∀ (l : List α) (a : α), (l ++ [a]).get? l.length = some a
+@[deprecated (since := "2024-06-12")]
+theorem get?_append {l₁ l₂ : List α} {n : Nat} (hn : n < l₁.length) :
+    (l₁ ++ l₂).get? n = l₁.get? n := by
+  simp [getElem?_append hn]
+
+@[simp] theorem getElem?_concat_length : ∀ (l : List α) (a : α), (l ++ [a])[l.length]? = some a
   | [], a => rfl
-  | b :: l, a => by rw [cons_append, length_cons]; simp only [get?, get?_concat_length]
+  | b :: l, a => by rw [cons_append, length_cons]; simp [getElem?_concat_length]
+
+@[deprecated getElem?_concat_length (since := "2024-06-12")]
+theorem get?_concat_length (l : List α) (a : α) : (l ++ [a]).get? l.length = some a := by simp
 
 theorem getLast_eq_get : ∀ (l : List α) (h : l ≠ []),
     getLast l h = l.get ⟨l.length - 1, by
@@ -236,51 +315,78 @@ theorem getLast?_eq_get? : ∀ (l : List α), getLast? l = l.get? (l.length - 1)
 @[simp] theorem getLast?_concat (l : List α) : getLast? (l ++ [a]) = some a := by
   simp [getLast?_eq_get?, Nat.succ_sub_succ]
 
-theorem getD_eq_get? : ∀ l n (a : α), getD l n a = (get? l n).getD a
-  | [], _, _ => rfl
-  | _a::_, 0, _ => rfl
-  | _::l, _+1, _ => getD_eq_get? (l := l) ..
+@[simp] theorem getD_eq_getElem? (l) (n) (a : α) : getD l n a = (l[n]?).getD a := by
+  simp [getD]
 
-theorem get?_append_right : ∀ {l₁ l₂ : List α} {n : Nat}, l₁.length ≤ n →
-  (l₁ ++ l₂).get? n = l₂.get? (n - l₁.length)
+@[deprecated getD_eq_getElem? (since := "2024-06-12")]
+theorem getD_eq_get? : ∀ l n (a : α), getD l n a = (get? l n).getD a := by simp
+
+theorem getElem?_append_right : ∀ {l₁ l₂ : List α} {n : Nat}, l₁.length ≤ n →
+  (l₁ ++ l₂)[n]? = l₂[n - l₁.length]?
 | [], _, n, _ => rfl
 | a :: l, _, n+1, h₁ => by
   rw [cons_append]
-  simp [Nat.succ_sub_succ_eq_sub, get?_append_right (Nat.lt_succ.1 h₁)]
+  simp [Nat.succ_sub_succ_eq_sub, getElem?_append_right (Nat.lt_succ.1 h₁)]
 
-theorem get?_reverse' : ∀ {l : List α} (i j), i + j + 1 = length l →
-    get? l.reverse i = get? l j
+@[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
+  simp [getElem?_append_right, h]
+
+theorem getElem?_reverse' : ∀ {l : List α} (i j), i + j + 1 = length l →
+    l.reverse[i]? = l[j]?
   | [], _, _, _ => rfl
-  | a::l, i, 0, h => by simp [Nat.succ.injEq] at h; simp [h, get?_append_right, Nat.succ.injEq]
+  | a::l, i, 0, h => by simp [Nat.succ.injEq] at h; simp [h, getElem?_append_right, Nat.succ.injEq]
   | a::l, i, j+1, h => by
     have := Nat.succ.inj h; simp at this ⊢
-    rw [get?_append, get?_reverse' _ j this]
+    rw [getElem?_append, getElem?_reverse' _ _ this]
     rw [length_reverse, ← this]; apply Nat.lt_add_of_pos_right (Nat.succ_pos _)
 
-theorem get?_reverse {l : List α} (i) (h : i < length l) :
-    get? l.reverse i = get? l (l.length - 1 - i) :=
-  get?_reverse' _ _ <| by
+@[deprecated getElem?_reverse' (since := "2024-06-12")]
+theorem get?_reverse' {l : List α} (i j) (h : i + j + 1 = length l) : get? l.reverse i = get? l j := by
+  simp [getElem?_reverse' _ _ h]
+
+theorem getElem?_reverse {l : List α} {i} (h : i < length l) :
+    l.reverse[i]? = l[l.length - 1 - i]? :=
+  getElem?_reverse' _ _ <| by
     rw [Nat.add_sub_of_le (Nat.le_sub_one_of_lt h),
       Nat.sub_add_cancel (Nat.lt_of_le_of_lt (Nat.zero_le _) h)]
 
+@[deprecated getElem?_reverse (since := "2024-06-12")]
+theorem get?_reverse {l : List α} {i} (h : i < length l) :
+    get? l.reverse i = get? l (l.length - 1 - i) := by
+  simp [getElem?_reverse h]
+
 @[simp] theorem getD_nil : getD [] n d = d := rfl
 
 @[simp] theorem getD_cons_zero : getD (x :: xs) 0 d = x := rfl
 
 @[simp] theorem getD_cons_succ : getD (x :: xs) (n + 1) d = getD xs n d := rfl
 
-theorem ext_get {l₁ l₂ : List α} (hl : length l₁ = length l₂)
-    (h : ∀ n h₁ h₂, get l₁ ⟨n, h₁⟩ = get l₂ ⟨n, h₂⟩) : l₁ = l₂ :=
-  ext fun n =>
+@[ext] theorem ext_getElem? {l₁ l₂ : List α} (h : ∀ n : Nat, l₁[n]? = l₂[n]?) : 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₂ :=
+  ext_getElem? fun n =>
     if h₁ : n < length l₁ then by
-      rw [get?_eq_get, get?_eq_get, h n h₁ (by rwa [← hl])]
+      simp_all [getElem?_eq_getElem]
     else by
       have h₁ := Nat.le_of_not_lt h₁
-      rw [get?_len_le h₁, get?_len_le]; rwa [← hl]
+      rw [getElem?_len_le h₁, getElem?_len_le]; rwa [← hl]
 
-@[simp] theorem get_map (f : α → β) {l n} :
-    get (map f l) n = f (get l ⟨n, length_map l f ▸ n.2⟩) :=
-  Option.some.inj <| by rw [← get?_eq_get, get?_map, get?_eq_get]; rfl
+theorem ext_get {l₁ l₂ : List α} (hl : length l₁ = length l₂)
+    (h : ∀ n h₁ h₂, get l₁ ⟨n, h₁⟩ = get l₂ ⟨n, h₂⟩) : l₁ = l₂ :=
+  ext_getElem hl (by simp_all)
+
+@[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)) :=
+  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
+  simp
 
 /-! ### take and drop -/
 
@@ -436,7 +542,7 @@ theorem mapM'_eq_mapM [Monad m] [LawfulMonad m] (f : α → m β) (l : List α)
 /-! ### forM -/
 
 -- We use `List.forM` as the simp normal form, rather that `ForM.forM`.
--- As such we need to replace `List.forM_nil` and `List.forM_cons` from Lean:
+-- As such we need to replace `List.forM_nil` and `List.forM_cons`:
 
 @[simp] theorem forM_nil' [Monad m] : ([] : List α).forM f = (pure .unit : m PUnit) := rfl
 
@@ -484,6 +590,7 @@ theorem filter_eq_nil {l} : filter p l = [] ↔ ∀ a, a ∈ l → ¬p a := by
 /-! ### findSome? -/
 
 @[simp] theorem findSome?_nil : ([] : List α).findSome? f = none := rfl
+
 theorem findSome?_cons {f : α → Option β} :
     (a::as).findSome? f = match f a with | some b => some b | none => as.findSome? f :=
   rfl
@@ -491,26 +598,32 @@ theorem findSome?_cons {f : α → Option β} :
 /-! ### replace -/
 
 @[simp] theorem replace_nil [BEq α] : ([] : List α).replace a b = [] := rfl
+
 theorem replace_cons [BEq α] {a : α} :
     (a::as).replace b c = match a == b with | true => c::as | false => a :: replace as b c :=
   rfl
+
 @[simp] theorem replace_cons_self [BEq α] [LawfulBEq α] {a : α} : (a::as).replace a b = b::as := by
   simp [replace_cons]
 
 /-! ### elem -/
 
 @[simp] theorem elem_nil [BEq α] : ([] : List α).elem a = false := rfl
+
 theorem elem_cons [BEq α] {a : α} :
     (a::as).elem b = match a == b with | true => true | false => as.elem b := rfl
+
 @[simp] theorem elem_cons_self [BEq α] [LawfulBEq α] {a : α} : (a::as).elem a = true := by
   simp [elem_cons]
 
 /-! ### lookup -/
 
 @[simp] theorem lookup_nil [BEq α] : ([] : List (α × β)).lookup a = none := rfl
+
 theorem lookup_cons [BEq α] {k : α} :
     ((k,b)::es).lookup a = match a == k with | true => some b | false => es.lookup a :=
   rfl
+
 @[simp] theorem lookup_cons_self [BEq α] [LawfulBEq α] {k : α} : ((k,b)::es).lookup k = some b := by
   simp [lookup_cons]
 
@@ -526,8 +639,8 @@ theorem lookup_cons [BEq α] {k : α} :
     zipWith f (a :: as) (b :: bs) = f a b :: zipWith f as bs := by
   rfl
 
-theorem zipWith_get? {f : α → β → γ} :
-    (List.zipWith f as bs).get? i = match as.get? i, bs.get? i with
+theorem getElem?_zipWith {f : α → β → γ} {i : Nat} :
+    (List.zipWith f as bs)[i]? = match as[i]?, bs[i]? with
       | some a, some b => some (f a b) | _, _ => none := by
   induction as generalizing bs i with
   | nil => cases bs with
@@ -537,10 +650,19 @@ theorem zipWith_get? {f : α → β → γ} :
     | nil => simp
     | cons b bs => cases i <;> simp_all
 
+@[deprecated getElem?_zipWith (since := "2024-06-12")]
+theorem get?_zipWith {f : α → β → γ} :
+    (List.zipWith f as bs).get? i = match as.get? i, bs.get? i with
+      | some a, some b => some (f a b) | _, _ => none := by
+  simp [getElem?_zipWith]
+
+set_option linter.deprecated false in
+@[deprecated getElem?_zipWith (since := "2024-06-07")] abbrev zipWith_get? := @get?_zipWith
+
 /-! ### zipWithAll -/
 
-theorem zipWithAll_get? {f : Option α → Option β → γ} :
-    (zipWithAll f as bs).get? i = match as.get? i, bs.get? i with
+theorem getElem?_zipWithAll {f : Option α → Option β → γ} {i : Nat } :
+    (zipWithAll f as bs)[i]? = match as[i]?, bs[i]? with
       | none, none => .none | a?, b? => some (f a? b?) := by
   induction as generalizing bs i with
   | nil => induction bs generalizing i with
@@ -552,6 +674,15 @@ theorem zipWithAll_get? {f : Option α → Option β → γ} :
       cases i <;> simp_all
     | cons b bs => cases i <;> simp_all
 
+@[deprecated getElem?_zipWithAll (since := "2024-06-12")]
+theorem get?_zipWithAll {f : Option α → Option β → γ} :
+    (zipWithAll f as bs).get? i = match as.get? i, bs.get? i with
+      | none, none => .none | a?, b? => some (f a? b?) := by
+  simp [getElem?_zipWithAll]
+
+set_option linter.deprecated false in
+@[deprecated getElem?_zipWithAll (since := "2024-06-07")] abbrev zipWithAll_get? := @get?_zipWithAll
+
 /-! ### zip -/
 
 @[simp] theorem zip_nil_left : zip ([] : List α) (l : List β)  = [] := by
@@ -566,6 +697,7 @@ theorem zipWithAll_get? {f : Option α → Option β → γ} :
 /-! ### unzip -/
 
 @[simp] theorem unzip_nil : ([] : List (α × β)).unzip = ([], []) := rfl
+
 @[simp] theorem unzip_cons {h : α × β} :
     (h :: t).unzip = match unzip t with | (al, bl) => (h.1::al, h.2::bl) := rfl
 
@@ -702,8 +834,8 @@ theorem minimum?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ ·
 @[simp] theorem set_succ (x : α) (xs : List α) (n : Nat) (a : α) :
   (x :: xs).set n.succ a = x :: xs.set n a := rfl
 
-@[simp] theorem get_set_eq (l : List α) (i : Nat) (a : α) (h : i < (l.set i a).length) :
-    (l.set i a).get ⟨i, h⟩ = a :=
+@[simp] theorem getElem_set_eq (l : List α) (i : Nat) (a : α) (h : i < (l.set i a).length) :
+    (l.set i a)[i] = a :=
   match l, i with
   | [], _ => by
     simp at h
@@ -711,11 +843,16 @@ theorem minimum?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ ·
   | _ :: _, 0 => by
     simp
   | _ :: l, i + 1 => by
-    simp [get_set_eq l]
+    simp [getElem_set_eq l]
 
-@[simp] theorem get_set_ne (l : List α) {i j : Nat} (h : i ≠ j) (a : α)
+@[deprecated getElem_set_eq (since := "2024-06-12")]
+theorem get_set_eq (l : List α) (i : Nat) (a : α) (h : i < (l.set i a).length) :
+    (l.set i a).get ⟨i, h⟩ = a :=
+  by simp
+
+@[simp] theorem getElem_set_ne (l : List α) {i j : Nat} (h : i ≠ j) (a : α)
     (hj : j < (l.set i a).length) :
-    (l.set i a).get ⟨j, hj⟩ = l.get ⟨j, by simp at hj; exact hj⟩ :=
+    (l.set i a)[j] = l[j]'(by simp at hj; exact hj) :=
   match l, i, j with
   | [], _, _ => by
     simp
@@ -727,8 +864,13 @@ theorem minimum?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ ·
     simp
   | _ :: l, i + 1, j + 1 => by
     have g : i ≠ j := h ∘ congrArg (· + 1)
-    simp [get_set_ne l g]
+    simp [getElem_set_ne l g]
 
+@[deprecated getElem_set_ne (since := "2024-06-12")]
+theorem get_set_ne (l : List α) {i j : Nat} (h : i ≠ j) (a : α)
+    (hj : j < (l.set i a).length) :
+    (l.set i a).get ⟨j, hj⟩ = l.get ⟨j, by simp at hj; exact hj⟩ := by
+  simp [h]
 
 open Nat
 
@@ -1213,10 +1355,15 @@ theorem dropLast_append_cons : dropLast (l₁ ++ b::l₂) = l₁ ++ dropLast (b:
   | [] => rfl
   | x::xs => by simp
 
-@[simp] theorem get_dropLast : ∀ (xs : List α) (i : Fin xs.dropLast.length),
-    xs.dropLast.get i = xs.get ⟨i, Nat.lt_of_lt_of_le i.isLt (length_dropLast .. ▸ Nat.pred_le _)⟩
-  | _::_::_, ⟨0, _⟩ => rfl
-  | _::_::_, ⟨i+1, _⟩ => get_dropLast _ ⟨i, _⟩
+@[simp] theorem getElem_dropLast : ∀ (xs : List α) (i : Nat) (h : i < xs.dropLast.length),
+    xs.dropLast[i] = xs[i]'(Nat.lt_of_lt_of_le h (length_dropLast .. ▸ Nat.pred_le _))
+  | _::_::_, 0, _ => rfl
+  | _::_::_, i+1, _ => getElem_dropLast _ i _
+
+@[deprecated getElem_dropLast (since := "2024-06-12")]
+theorem get_dropLast (xs : List α) (i : Fin xs.dropLast.length) :
+    xs.dropLast.get i = xs.get ⟨i, Nat.lt_of_lt_of_le i.isLt (length_dropLast .. ▸ Nat.pred_le _)⟩ := by
+  simp
 
 /-! ### nth element -/
 
@@ -1233,9 +1380,15 @@ theorem get!_len_le [Inhabited α] : ∀ {l : List α} {n}, length l ≤ n → l
   | [], _, _ => rfl
   | _ :: l, _+1, h => get!_len_le (l := l) <| Nat.le_of_succ_le_succ h
 
+theorem getElem?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n : Nat, l[n]? = some a :=
+  let ⟨n, _, e⟩ := getElem_of_mem h; ⟨n, e ▸ getElem?_eq_getElem _⟩
+
 theorem get?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n, l.get? n = some a :=
   let ⟨⟨n, _⟩, e⟩ := get_of_mem h; ⟨n, e ▸ get?_eq_get _⟩
 
+theorem getElem?_mem {l : List α} {n : Nat} {a : α} (e : l[n]? = some a) : a ∈ l :=
+  let ⟨_, e⟩ := getElem?_eq_some.1 e; e ▸ getElem_mem ..
+
 theorem get?_mem {l : List α} {n a} (e : l.get? n = some a) : a ∈ l :=
   let ⟨_, e⟩ := get?_eq_some.1 e; e ▸ get_mem ..
 
@@ -1243,57 +1396,104 @@ theorem get?_mem {l : List α} {n a} (e : l.get? n = some a) : a ∈ l :=
 theorem Fin.exists_iff (p : Fin n → Prop) : (∃ i, p i) ↔ ∃ i h, p ⟨i, h⟩ :=
   ⟨fun ⟨i, h⟩ => ⟨i.1, i.2, h⟩, fun ⟨i, hi, h⟩ => ⟨⟨i, hi⟩, h⟩⟩
 
+theorem mem_iff_getElem? {a} {l : List α} : a ∈ l ↔ ∃ n : Nat, l[n]? = some a := by
+  simp [getElem?_eq_some, mem_iff_getElem]
+
 theorem mem_iff_get? {a} {l : List α} : a ∈ l ↔ ∃ n, l.get? n = some a := by
-  simp [get?_eq_some, Fin.exists_iff, mem_iff_get]
+  simp [getElem?_eq_some, Fin.exists_iff, mem_iff_get]
 
 theorem get?_zero (l : List α) : l.get? 0 = l.head? := by cases l <;> rfl
 
-@[simp] theorem getElem_eq_get (l : List α) (i : Nat) (h) : l[i]'h = l.get ⟨i, h⟩ := rfl
-
-@[simp] theorem getElem?_eq_get? (l : List α) (i : Nat) : l[i]? = l.get? i := by
-  simp only [getElem?]; split
-  · exact (get?_eq_get ‹_›).symm
-  · exact (get?_eq_none.2 <| Nat.not_lt.1 ‹_›).symm
+/--
+If one has `l[i]` in an expression and `h : l = l'`,
+`rw [h]` will give a "motive it not type correct" error, as it cannot rewrite the
+implicit `i < l.length` to `i < l'.length` directly. The theorem `getElem_of_eq` can be used to make
+such a rewrite, with `rw [getElem_of_eq h]`.
+-/
+theorem getElem_of_eq {l l' : List α} (h : l = l') {i : Nat} (w : i < l.length) :
+    l[i] = l'[i]'(h ▸ w) := by cases h; rfl
 
 /--
-If one has `get l i hi` in a formula and `h : l = l'`, one can not `rw h` in the formula as
-`hi` gives `i < l.length` and not `i < l'.length`. The theorem `get_of_eq` can be used to make
+If one has `l.get i` in an expression (with `i : Fin l.length`) and `h : l = l'`,
+`rw [h]` will give a "motive it not type correct" error, as it cannot rewrite the
+`i : Fin l.length` to `Fin l'.length` directly. The theorem `get_of_eq` can be used to make
 such a rewrite, with `rw [get_of_eq h]`.
 -/
 theorem get_of_eq {l l' : List α} (h : l = l') (i : Fin l.length) :
     get l i = get l' ⟨i, h ▸ i.2⟩ := by cases h; rfl
 
-@[simp] theorem get_singleton (a : α) : (n : Fin 1) → get [a] n = a
-  | ⟨0, _⟩ => rfl
+@[simp] theorem getElem_singleton (a : α) (h : i < 1) : [a][i] = a :=
+  match i, h with
+  | 0, _ => rfl
+
+@[deprecated getElem_singleton (since := "2024-06-12")]
+theorem get_singleton (a : α) (n : Fin 1) : get [a] n = a := by simp
+
+theorem getElem_zero {l : List α} (h : 0 < l.length) : l[0] = l.head (length_pos.mp h) :=
+  match l, h with
+  | _ :: _, _ => rfl
 
 theorem get_mk_zero : ∀ {l : List α} (h : 0 < l.length), l.get ⟨0, h⟩ = l.head (length_pos.mp h)
   | _::_, _ => rfl
 
+theorem getElem_append_right' {l₁ l₂ : List α} {n : Nat} (h₁ : l₁.length ≤ n) (h₂) :
+    (l₁ ++ l₂)[n]'h₂ =
+      l₂[n - l₁.length]'(by rw [length_append] at h₂; exact Nat.sub_lt_left_of_lt_add h₁ h₂) :=
+  Option.some.inj <| by rw [← getElem?_eq_getElem, ← getElem?_eq_getElem, getElem?_append_right h₁]
+
+@[deprecated (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
   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₂⟩ :=
-Option.some.inj <| by rw [← get?_eq_get, ← get?_eq_get, get?_append_right 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
+  rw [← getElem?_eq_getElem, eq, getElem?_append_right (h ▸ Nat.le_refl _), h]
+  simp
+
+@[deprecated (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
 
+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
   rw [← get?_eq_get, eq, get?_append_right (h ▸ Nat.le_refl _), h, Nat.sub_self]; rfl
 
-@[simp] theorem get_replicate (a : α) {n : Nat} (m : Fin _) : (replicate n a).get m = a :=
+@[simp] theorem getElem_replicate (a : α) {n : Nat} {m} (h : m < (replicate n a).length) :
+    (replicate n a)[m] = a :=
   eq_of_mem_replicate (get_mem _ _ _)
 
+@[deprecated getElem_replicate (since := "2024-06-12")]
+theorem get_replicate (a : α) {n : Nat} (m : Fin _) : (replicate n a).get m = a := by
+  simp
+
 @[simp] theorem getLastD_concat (a b l) : @getLastD α (l ++ [b]) a = b := by
   rw [getLastD_eq_getLast?, getLast?_concat]; rfl
 
+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
+  rw [getLast_eq_get]; cases h; rfl
+
+@[deprecated getElem_cons_length (since := "2024-06-12")]
 theorem get_cons_length (x : α) (xs : List α) (n : Nat) (h : n = xs.length) :
     (x :: xs).get ⟨n, by simp [h]⟩ = (x :: xs).getLast (cons_ne_nil x xs) := by
-  rw [getLast_eq_get]; cases h; rfl
+  simp [getElem_cons_length, h]
+
+theorem getElem!_of_getElem? [Inhabited α] : ∀ {l : List α} {n : Nat}, l[n]? = some a → l[n]! = a
+  | _a::_, 0, _ => by
+    rw [getElem!_pos] <;> simp_all
+  | _::l, _+1, e => by
+    simp at e
+    simp_all [getElem!_of_getElem? (l := l) e]
 
 theorem get!_of_get? [Inhabited α] : ∀ {l : List α} {n}, get? l n = some a → get! l n = a
   | _a::_, 0, rfl => rfl
@@ -1323,9 +1523,17 @@ theorem set_set (a b : α) : ∀ (l : List α) (n : Nat), (l.set n a).set n b =
   | _ :: _, 0 => by simp [set]
   | _ :: _, _+1 => by simp [set, set_set]
 
+theorem getElem_set (a : α) {m n} (l : List α) (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_eq, ↓reduceIte]
+  else
+    simp [h]
+
+@[deprecated getElem_set (since := "2024-06-12")]
 theorem get_set (a : α) {m n} (l : List α) (h) :
     (set l m a).get ⟨n, h⟩ = if m = n then a else l.get ⟨n, length_set .. ▸ h⟩ := by
-  if h : m = n then subst m; simp else simp [h]
+  simp [getElem_set]
 
 theorem mem_or_eq_of_mem_set : ∀ {l : List α} {n : Nat} {a b : α}, a ∈ l.set n b → a ∈ l ∨ a = b
   | _ :: _, 0, _, _, h => ((mem_cons ..).1 h).symm.imp_left (.tail _)

src/Init/Data/List/TakeDrop.lean

@@ -88,18 +88,33 @@ theorem take_append {l₁ l₂ : List α} (i : Nat) :
 
 /-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
 length `> i`. Version designed to rewrite from the big list to the small list. -/
-theorem get_take (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) :
-    get L ⟨i, hi⟩ = get (L.take j) ⟨i, length_take .. ▸ Nat.lt_min.mpr ⟨hj, hi⟩⟩ :=
-  get_of_eq (take_append_drop j L).symm _ ▸ get_append ..
+theorem getElem_take (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) :
+    L[i] = (L.take j)[i]'(length_take .. ▸ Nat.lt_min.mpr ⟨hj, hi⟩) :=
+  getElem_of_eq (take_append_drop j L).symm _ ▸ getElem_append ..
 
 /-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
 length `> i`. Version designed to rewrite from the small list to the big list. -/
+theorem getElem_take' (L : List α) {j i : Nat} {h : i < (L.take j).length} :
+    (L.take j)[i] =
+    L[i]'(Nat.lt_of_lt_of_le h (length_take_le' _ _)) := by
+  rw [length_take, Nat.lt_min] at h; rw [getElem_take L _ h.1]
+
+/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
+length `> i`. Version designed to rewrite from the big list to the small list. -/
+@[deprecated getElem_take (since := "2024-06-12")]
+theorem get_take (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) :
+    get L ⟨i, hi⟩ = get (L.take j) ⟨i, length_take .. ▸ Nat.lt_min.mpr ⟨hj, hi⟩⟩ := by
+  simp [getElem_take _ hi hj]
+
+/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
+length `> i`. Version designed to rewrite from the small list to the big list. -/
+@[deprecated getElem_take (since := "2024-06-12")]
 theorem get_take' (L : List α) {j i} :
     get (L.take j) i =
     get L ⟨i.1, Nat.lt_of_lt_of_le i.2 (length_take_le' _ _)⟩ := by
-  let ⟨i, hi⟩ := i; rw [length_take, Nat.lt_min] at hi; rw [get_take L _ hi.1]
+  simp [getElem_take']
 
-theorem get?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n).get? m = l.get? m := by
+theorem getElem?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n)[m]? = l[m]? := by
   induction n generalizing l m with
   | zero =>
     exact absurd h (Nat.not_lt_of_le m.zero_le)
@@ -108,31 +123,45 @@ theorem get?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n).get? m = l.
     | nil => simp only [take_nil]
     | cons hd tl =>
       cases m
-      · simp only [get?, take]
-      · simpa only using hn (Nat.lt_of_succ_lt_succ h)
+      · simp
+      · simpa using hn (Nat.lt_of_succ_lt_succ h)
 
+@[deprecated getElem?_take (since := "2024-06-12")]
+theorem get?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n).get? m = l.get? m := by
+  simp [getElem?_take, h]
+
+theorem getElem?_take_eq_none {l : List α} {n m : Nat} (h : n ≤ m) :
+    (l.take n)[m]? = none :=
+  getElem?_eq_none.mpr <| Nat.le_trans (length_take_le _ _) h
+
+@[deprecated getElem?_take_eq_none (since := "2024-06-12")]
 theorem get?_take_eq_none {l : List α} {n m : Nat} (h : n ≤ m) :
-    (l.take n).get? m = none :=
-  get?_eq_none.mpr <| Nat.le_trans (length_take_le _ _) h
+    (l.take n).get? m = none := by
+  simp [getElem?_take_eq_none h]
 
+theorem getElem?_take_eq_if {l : List α} {n m : Nat} :
+    (l.take n)[m]? = if m < n then l[m]? else none := by
+  split
+  · next h => exact getElem?_take h
+  · next h => exact getElem?_take_eq_none (Nat.le_of_not_lt h)
+
+@[deprecated getElem?_take_eq_if (since := "2024-06-12")]
 theorem get?_take_eq_if {l : List α} {n m : Nat} :
     (l.take n).get? m = if m < n then l.get? m else none := by
-  split
-  · next h => exact get?_take h
-  · next h => exact get?_take_eq_none (Nat.le_of_not_lt h)
+  simp [getElem?_take_eq_if]
 
 @[simp]
-theorem nth_take_of_succ {l : List α} {n : Nat} : (l.take (n + 1)).get? n = l.get? n :=
-  get?_take (Nat.lt_succ_self n)
+theorem get?_take_of_succ {l : List α} {n : Nat} : (l.take (n + 1))[n]? = l[n]? :=
+  getElem?_take (Nat.lt_succ_self n)
 
-theorem take_succ {l : List α} {n : Nat} : l.take (n + 1) = l.take n ++ (l.get? n).toList := by
+theorem take_succ {l : List α} {n : Nat} : l.take (n + 1) = l.take n ++ l[n]?.toList := by
   induction l generalizing n with
   | nil =>
-    simp only [Option.toList, get?, take_nil, append_nil]
+    simp only [take_nil, Option.toList, getElem?_nil, append_nil]
   | cons hd tl hl =>
     cases n
-    · simp only [Option.toList, get?, eq_self_iff_true, take, nil_append]
-    · simp only [hl, cons_append, get?, eq_self_iff_true, take]
+    · simp only [take, Option.toList, getElem?_cons_zero, nil_append]
+    · simp only [take, hl, getElem?_cons_succ, cons_append]
 
 @[simp]
 theorem take_eq_nil_iff {l : List α} {k : Nat} : l.take k = [] ↔ l = [] ∨ k = 0 := by
@@ -254,24 +283,40 @@ theorem lt_length_drop (L : List α) {i j : Nat} (h : i + j < L.length) : j < (L
 
 /-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
 dropping the first `i` elements. Version designed to rewrite from the big list to the small list. -/
-theorem get_drop (L : List α) {i j : Nat} (h : i + j < L.length) :
-    get L ⟨i + j, h⟩ = get (L.drop i) ⟨j, lt_length_drop L h⟩ := by
+theorem getElem_drop (L : List α) {i j : Nat} (h : i + j < L.length) :
+    L[i + j] = (L.drop i)[j]'(lt_length_drop L h) := by
   have : i ≤ L.length := Nat.le_trans (Nat.le_add_right _ _) (Nat.le_of_lt h)
-  rw [get_of_eq (take_append_drop i L).symm ⟨i + j, h⟩, get_append_right'] <;>
+  rw [getElem_of_eq (take_append_drop i L).symm h, getElem_append_right'] <;>
     simp [Nat.min_eq_left this, Nat.add_sub_cancel_left, Nat.le_add_right]
 
+/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
+dropping the first `i` elements. Version designed to rewrite from the big list to the small list. -/
+@[deprecated getElem_drop (since := "2024-06-12")]
+theorem get_drop (L : List α) {i j : Nat} (h : i + j < L.length) :
+    get L ⟨i + j, h⟩ = get (L.drop i) ⟨j, lt_length_drop L h⟩ := by
+  simp [getElem_drop]
+
 /-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
 dropping the first `i` elements. Version designed to rewrite from the small list to the big list. -/
+theorem getElem_drop' (L : List α) {i : Nat} {j : Nat} {h : j < (L.drop i).length} :
+    (L.drop i)[j] = L[i + j]'(by
+      rw [Nat.add_comm]
+      exact Nat.add_lt_of_lt_sub (length_drop i L ▸ h)) := by
+  rw [getElem_drop]
+
+/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
+dropping the first `i` elements. Version designed to rewrite from the small list to the big list. -/
+@[deprecated getElem_drop' (since := "2024-06-12")]
 theorem get_drop' (L : List α) {i j} :
     get (L.drop i) j = get L ⟨i + j, by
       rw [Nat.add_comm]
       exact Nat.add_lt_of_lt_sub (length_drop i L ▸ j.2)⟩ := by
-  rw [get_drop]
+  simp [getElem_drop']
 
 @[simp]
-theorem get?_drop (L : List α) (i j : Nat) : get? (L.drop i) j = get? L (i + j) := by
+theorem getElem?_drop (L : List α) (i j : Nat) : (L.drop i)[j]? = L[i + j]? := by
   ext
-  simp only [get?_eq_some, get_drop', Option.mem_def]
+  simp only [getElem?_eq_some, getElem_drop', Option.mem_def]
   constructor <;> intro ⟨h, ha⟩
   · exact ⟨_, ha⟩
   · refine ⟨?_, ha⟩
@@ -279,6 +324,10 @@ theorem get?_drop (L : List α) (i j : Nat) : get? (L.drop i) j = get? L (i + j)
     rw [Nat.add_comm] at h
     apply Nat.lt_sub_of_add_lt h
 
+@[deprecated getElem?_drop (since := "2024-06-12")]
+theorem get?_drop (L : List α) (i j : Nat) : get? (L.drop i) j = get? L (i + j) := by
+  simp
+
 @[simp] theorem drop_drop (n : Nat) : ∀ (m) (l : List α), drop n (drop m l) = drop (n + m) l
   | m, [] => by simp
   | 0, l => by simp
@@ -331,12 +380,21 @@ theorem reverse_take {α} {xs : List α} (n : Nat) (h : n ≤ xs.length) :
     rfl
 
 @[simp]
-theorem get_cons_drop : ∀ (l : List α) i, get l i :: drop (i + 1) l = drop i l
-  | _::_, ⟨0, _⟩ => rfl
-  | _::_, ⟨i+1, _⟩ => get_cons_drop _ ⟨i, _⟩
+theorem getElem_cons_drop : ∀ (l : List α) (i : Nat) (h : i < l.length),
+    l[i] :: drop (i + 1) l = drop i l
+  | _::_, 0, _ => rfl
+  | _::_, i+1, _ => getElem_cons_drop _ i _
 
-theorem drop_eq_get_cons {n} {l : List α} (h) : drop n l = get l ⟨n, h⟩ :: drop (n + 1) l :=
-  (get_cons_drop _ ⟨n, h⟩).symm
+@[deprecated getElem_cons_drop (since := "2024-06-12")]
+theorem get_cons_drop (l : List α) (i) : get l i :: drop (i + 1) l = drop i l := by
+  simp
+
+theorem drop_eq_getElem_cons {n} {l : List α} (h) : drop n l = l[n] :: drop (n + 1) l :=
+  (getElem_cons_drop _ n h).symm
+
+@[deprecated drop_eq_getElem_cons (since := "2024-06-12")]
+theorem drop_eq_get_cons {n} {l : List α} (h) : drop n l = get l ⟨n, h⟩ :: drop (n + 1) l := by
+  simp [drop_eq_getElem_cons]
 
 theorem drop_eq_nil_of_eq_nil : ∀ {as : List α} {i}, as = [] → as.drop i = []
   | _, _, rfl => drop_nil

src/Init/GetElem.lean

@@ -141,12 +141,16 @@ instance : GetElem (List α) Nat α fun as i => i < as.length where
 
 instance : LawfulGetElem (List α) Nat α fun as i => i < as.length where
 
-@[simp] theorem cons_getElem_zero (a : α) (as : List α) (h : 0 < (a :: as).length) : getElem (a :: as) 0 h = a := by
+@[simp] theorem getElem_cons_zero (a : α) (as : List α) (h : 0 < (a :: as).length) : getElem (a :: as) 0 h = a := by
   rfl
 
-@[simp] theorem cons_getElem_succ (a : α) (as : List α) (i : Nat) (h : i + 1 < (a :: as).length) : getElem (a :: as) (i+1) h = getElem as i (Nat.lt_of_succ_lt_succ h) := by
+@[deprecated (since := "2024-6-12")] abbrev cons_getElem_zero := @getElem_cons_zero
+
+@[simp] theorem getElem_cons_succ (a : α) (as : List α) (i : Nat) (h : i + 1 < (a :: as).length) : getElem (a :: as) (i+1) h = getElem as i (Nat.lt_of_succ_lt_succ h) := by
   rfl
 
+@[deprecated (since := "2024-6-12")] abbrev cons_getElem_succ := @getElem_cons_succ
+
 theorem get_drop_eq_drop (as : List α) (i : Nat) (h : i < as.length) : as[i] :: as.drop (i+1) = as.drop i :=
   match as, i with
   | _::_, 0   => rfl

src/Init/Omega/IntList.lean

@@ -28,8 +28,8 @@ def get (xs : IntList) (i : Nat) : Int := (xs.get? i).getD 0
 @[simp] theorem get_cons_succ : get (x :: xs) (i+1) = get xs i := rfl
 
 theorem get_map {xs : IntList} (h : f 0 = 0) : get (xs.map f) i = f (xs.get i) := by
-  simp only [get, List.get?_map]
-  cases xs.get? i <;> simp_all
+  simp only [get, List.get?_eq_getElem?, List.getElem?_map]
+  cases xs[i]? <;> simp_all
 
 theorem get_of_length_le {xs : IntList} (h : xs.length ≤ i) : xs.get i = 0 := by
   rw [get, List.get?_eq_none.mpr h]
@@ -66,8 +66,8 @@ theorem add_def (xs ys : IntList) :
   rfl
 
 @[simp] theorem add_get (xs ys : IntList) (i : Nat) : (xs + ys).get i = xs.get i + ys.get i := by
-  simp only [add_def, get, List.zipWithAll_get?, List.get?_eq_none]
-  cases xs.get? i <;> cases ys.get? i <;> simp
+  simp only [get, add_def, List.get?_eq_getElem?, List.getElem?_zipWithAll]
+  cases xs[i]? <;> cases ys[i]? <;> simp
 
 @[simp] theorem add_nil (xs : IntList) : xs + [] = xs := by simp [add_def]
 @[simp] theorem nil_add (xs : IntList) : [] + xs = xs := by simp [add_def]
@@ -83,8 +83,8 @@ theorem mul_def (xs ys : IntList) : xs * ys = List.zipWith (· * ·) xs ys :=
   rfl
 
 @[simp] theorem mul_get (xs ys : IntList) (i : Nat) : (xs * ys).get i = xs.get i * ys.get i := by
-  simp only [mul_def, get, List.zipWith_get?]
-  cases xs.get? i <;> cases ys.get? i <;> simp
+  simp only [get, mul_def, List.get?_eq_getElem?, List.getElem?_zipWith]
+  cases xs[i]? <;> cases ys[i]? <;> simp
 
 @[simp] theorem mul_nil_left : ([] : IntList) * ys = [] := rfl
 @[simp] theorem mul_nil_right : xs * ([] : IntList) = [] := List.zipWith_nil_right
@@ -98,8 +98,8 @@ instance : Neg IntList := ⟨neg⟩
 theorem neg_def (xs : IntList) : - xs = xs.map fun x => -x := rfl
 
 @[simp] theorem neg_get (xs : IntList) (i : Nat) : (- xs).get i = - xs.get i := by
-  simp only [neg_def, get, List.get?_map]
-  cases xs.get? i <;> simp
+  simp only [get, neg_def, List.get?_eq_getElem?, List.getElem?_map]
+  cases xs[i]? <;> simp
 
 @[simp] theorem neg_nil : (- ([] : IntList)) = [] := rfl
 @[simp] theorem neg_cons : (- (x::xs : IntList)) = -x :: -xs := rfl
@@ -124,8 +124,8 @@ instance : HMul Int IntList IntList where
 theorem smul_def (xs : IntList) (i : Int) : i * xs = xs.map fun x => i * x := rfl
 
 @[simp] theorem smul_get (xs : IntList) (a : Int) (i : Nat) : (a * xs).get i = a * xs.get i := by
-  simp only [smul_def, get, List.get?_map]
-  cases xs.get? i <;> simp
+  simp only [get, smul_def, List.get?_eq_getElem?, List.getElem?_map]
+  cases xs[i]? <;> simp
 
 @[simp] theorem smul_nil {i : Int} : i * ([] : IntList) = [] := rfl
 @[simp] theorem smul_cons {i : Int} : i * (x::xs : IntList) = i * x :: i * xs := rfl