diff --git a/src/Init/Data/AC.lean b/src/Init/Data/AC.lean
index f197f36357..29aad6ab5c 100644
--- a/src/Init/Data/AC.lean
+++ b/src/Init/Data/AC.lean
@@ -39,7 +39,7 @@ class EvalInformation (α : Sort u) (β : Sort v) where
   evalVar : α → Nat → β
 
 def Context.var (ctx : Context α) (idx : Nat) : Variable ctx.op :=
-  ctx.vars.getD idx ⟨ctx.arbitrary, none⟩
+  ctx.vars[idx]?.getD ⟨ctx.arbitrary, none⟩
 
 instance : ContextInformation (Context α) where
   isNeutral ctx x := ctx.var x |>.neutral.isSome
diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 10b473c64f..f12d08b3c2 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -48,7 +48,7 @@ theorem ext (a b : Array α)
     : a = b := by
   let rec extAux (a b : List α)
       (h₁ : a.length = b.length)
-      (h₂ : (i : Nat) → (hi₁ : i < a.length) → (hi₂ : i < b.length) → a.get ⟨i, hi₁⟩ = b.get ⟨i, hi₂⟩)
+      (h₂ : (i : Nat) → (hi₁ : i < a.length) → (hi₂ : i < b.length) → a[i] = b[i])
       : a = b := by
     induction a generalizing b with
     | nil =>
@@ -63,11 +63,11 @@ theorem ext (a b : Array α)
         have hz₂ : 0 < (b::bs).length := by rw [List.length_cons]; apply Nat.zero_lt_succ
         have headEq : a = b := h₂ 0 hz₁ hz₂
         have h₁' : as.length = bs.length := by rw [List.length_cons, List.length_cons] at h₁; injection h₁
-        have h₂' : (i : Nat) → (hi₁ : i < as.length) → (hi₂ : i < bs.length) → as.get ⟨i, hi₁⟩ = bs.get ⟨i, hi₂⟩ := by
+        have h₂' : (i : Nat) → (hi₁ : i < as.length) → (hi₂ : i < bs.length) → as[i] = bs[i] := by
           intro i hi₁ hi₂
           have hi₁' : i+1 < (a::as).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
           have hi₂' : i+1 < (b::bs).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
-          have : (a::as).get ⟨i+1, hi₁'⟩ = (b::bs).get ⟨i+1, hi₂'⟩ := h₂ (i+1) hi₁' hi₂'
+          have : (a::as)[i+1] = (b::bs)[i+1] := h₂ (i+1) hi₁' hi₂'
           apply this
         have tailEq : as = bs := ih bs h₁' h₂'
         rw [headEq, tailEq]
@@ -123,7 +123,8 @@ namespace List
 @[simp] theorem getElem?_toArray {a : List α} {i : Nat} : a.toArray[i]? = a[i]? := rfl
 
 @[simp] theorem getElem!_toArray [Inhabited α] {a : List α} {i : Nat} :
-    a.toArray[i]! = a[i]! := rfl
+    a.toArray[i]! = a[i]! := by
+  simp [getElem!_def]
 
 end List
 
@@ -254,17 +255,37 @@ def range' (start size : Nat) (step : Nat := 1) : Array Nat :=
 
 @[inline] protected def singleton (v : α) : Array α := #[v]
 
+/--
+Return the last element of an array, or panic if the array is empty.
+
+See `back` for the version that requires a proof the array is non-empty,
+or `back?` for the version that returns an option.
+-/
 def back! [Inhabited α] (a : Array α) : α :=
   a[a.size - 1]!
 
-@[deprecated back! (since := "2024-10-31")] abbrev back := @back!
+/--
+Return the last element of an array, given a proof that the array is not empty.
 
-def get? (a : Array α) (i : Nat) : Option α :=
-  if h : i < a.size then some a[i] else none
+See `back!` for the version that panics if the array is empty,
+or `back?` for the version that returns an option.
+-/
+def back (a : Array α) (h : 0 < a.size := by get_elem_tactic) : α :=
+  a[a.size - 1]'(Nat.sub_one_lt_of_lt h)
 
+/--
+Return the last element of an array, or `none` if the array is empty.
+
+See `back!` for the version that panics if the array is empty,
+or `back` for the version that requires a proof the array is non-empty.
+-/
 def back? (a : Array α) : Option α :=
   a[a.size - 1]?
 
+@[deprecated "Use `a[i]?` instead." (since := "2025-02-12")]
+def get? (a : Array α) (i : Nat) : Option α :=
+  if h : i < a.size then some a[i] else none
+
 @[inline] def swapAt (a : Array α) (i : Nat) (v : α) (hi : i < a.size := by get_elem_tactic) : α × Array α :=
   let e := a[i]
   let a := a.set i v
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index 978a5e38ed..683745bf53 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -3226,7 +3226,9 @@ theorem getElem?_lt
 theorem getElem?_ge
     (a : Array α) {i : Nat} (h : i ≥ a.size) : a[i]? = none := dif_neg (Nat.not_lt_of_le h)
 
-@[simp] theorem get?_eq_getElem? (a : Array α) (i : Nat) : a.get? i = a[i]? := rfl
+set_option linter.deprecated false in
+@[deprecated "`get?` is deprecated" (since := "2025-02-12"), simp]
+theorem get?_eq_getElem? (a : Array α) (i : Nat) : a.get? i = a[i]? := rfl
 
 @[deprecated getElem?_eq_none (since := "2024-12-11")]
 theorem getElem?_len_le (a : Array α) {i : Nat} (h : a.size ≤ i) : a[i]? = none := by
@@ -3234,15 +3236,26 @@ 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 α) (i d) : a.getD i d = (a[i]?).getD d := by
-  simp only [getD, get_eq_getElem, get?_eq_getElem?]; split <;> simp [getD_getElem?, *]
+@[simp] theorem getD_eq_getD_getElem? (a : Array α) (i d) : a.getD i d = a[i]?.getD d := by
+  simp only [getD, get_eq_getElem]; split <;> simp [getD_getElem?, *]
 
+@[deprecated getD_eq_getD_getElem? (since := "2025-02-12")] abbrev getD_eq_get? := @getD_eq_getD_getElem?
+
+theorem getElem!_eq_getD [Inhabited α] (a : Array α) : a[i]! = a.getD i default := by
+  simp only [← get!_eq_getElem!]
+  rfl
+
+@[deprecated getElem!_eq_getD (since := "2025-02-12")]
 theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default := rfl
 
-theorem get!_eq_getElem? [Inhabited α] (a : Array α) (i : Nat) :
-    a.get! i = (a.get? i).getD default := by
+@[deprecated "Use `a[i]!` instead of `a.get! i`." (since := "2025-02-12")]
+theorem get!_eq_getD_getElem? [Inhabited α] (a : Array α) (i : Nat) :
+    a.get! i = a[i]?.getD default := by
   by_cases p : i < a.size <;>
-  simp only [get!_eq_getD, getD_eq_get?, getD_getElem?, p, get?_eq_getElem?]
+  simp only [get!_eq_getElem!, getElem!_eq_getD, getD_eq_getD_getElem?, getD_getElem?, p]
+
+set_option linter.deprecated false in
+@[deprecated get!_eq_getD_getElem? (since := "2025-02-12")] abbrev get!_eq_getElem? := @get!_eq_getD_getElem?
 
 /-! # ofFn -/
 
@@ -3325,11 +3338,13 @@ theorem getElem?_size_le (a : Array α) (i : Nat) (h : a.size ≤ i) : a[i]? = n
 theorem getElem_mem_toList (a : Array α) (h : i < a.size) : a[i] ∈ a.toList := by
   simp only [← getElem_toList, List.getElem_mem]
 
+set_option linter.deprecated false in
+@[deprecated "`Array.get?` is deprecated, use `a[i]?` instead." (since := "2025-02-12")]
 theorem get?_eq_get?_toList (a : Array α) (i : Nat) : a.get? i = a.toList.get? i := by
   simp [← getElem?_toList]
 
-theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD default := by
-  simp only [get!_eq_getElem?, get?_eq_getElem?]
+set_option linter.deprecated false in
+@[deprecated get!_eq_getD_getElem? (since := "2025-02-12")] abbrev get!_eq_get? := @get!_eq_getD_getElem?
 
 theorem back!_eq_back? [Inhabited α] (a : Array α) : a.back! = a.back?.getD default := by
   simp [back!, back?, getElem!_def, Option.getD]; rfl
@@ -3939,8 +3954,6 @@ end Array
 
 namespace List
 
-@[deprecated back!_toArray (since := "2024-10-31")] abbrev back_toArray := @back!_toArray
-
 @[deprecated setIfInBounds_toArray (since := "2024-11-24")] abbrev setD_toArray := @setIfInBounds_toArray
 
 end List
@@ -3962,9 +3975,6 @@ abbrev getElem_fin_eq_toList_get := @getElem_fin_eq_getElem_toList
 @[deprecated "Use reverse direction of `getElem?_toList`" (since := "2024-10-17")]
 abbrev getElem?_eq_toList_getElem? := @getElem?_toList
 
-@[deprecated get?_eq_get?_toList (since := "2024-10-17")]
-abbrev get?_eq_toList_get? := @get?_eq_get?_toList
-
 @[deprecated getElem?_swap (since := "2024-10-17")] abbrev get?_swap := @getElem?_swap
 
 @[deprecated getElem_push (since := "2024-10-21")] abbrev get_push := @getElem_push
diff --git a/src/Init/Data/Array/MapIdx.lean b/src/Init/Data/Array/MapIdx.lean
index 9e4c002eb0..07eeb00e6f 100644
--- a/src/Init/Data/Array/MapIdx.lean
+++ b/src/Init/Data/Array/MapIdx.lean
@@ -418,6 +418,11 @@ theorem mapIdx_eq_mapIdx_iff {l : Array α} :
   rcases l with ⟨l⟩
   simp [List.getLast?_mapIdx]
 
+@[simp] theorem back_mapIdx {l : Array α} {f : Nat → α → β} (h) :
+    (l.mapIdx f).back h = f (l.size - 1) (l.back (by simpa using h)) := by
+  rcases l with ⟨l⟩
+  simp [List.getLast_mapIdx]
+
 @[simp] theorem mapIdx_mapIdx {l : Array α} {f : Nat → α → β} {g : Nat → β → γ} :
     (l.mapIdx f).mapIdx g = l.mapIdx (fun i => g i ∘ f i) := by
   simp [mapIdx_eq_iff]
diff --git a/src/Init/Data/ByteArray/Basic.lean b/src/Init/Data/ByteArray/Basic.lean
index 2807f4c804..19b44a5550 100644
--- a/src/Init/Data/ByteArray/Basic.lean
+++ b/src/Init/Data/ByteArray/Basic.lean
@@ -47,7 +47,7 @@ def uget : (a : @& ByteArray) → (i : USize) → (h : i.toNat < a.size := by ge
 
 @[extern "lean_byte_array_get"]
 def get! : (@& ByteArray) → (@& Nat) → UInt8
-  | ⟨bs⟩, i => bs.get! i
+  | ⟨bs⟩, i => bs[i]!
 
 @[extern "lean_byte_array_fget"]
 def get : (a : @& ByteArray) → (i : @& Nat) → (h : i < a.size := by get_elem_tactic) → UInt8
diff --git a/src/Init/Data/FloatArray/Basic.lean b/src/Init/Data/FloatArray/Basic.lean
index bf60a543a7..508ad86bf8 100644
--- a/src/Init/Data/FloatArray/Basic.lean
+++ b/src/Init/Data/FloatArray/Basic.lean
@@ -51,7 +51,7 @@ def get : (ds : @& FloatArray) → (i : @& Nat) → (h : i < ds.size := by get_e
 
 @[extern "lean_float_array_get"]
 def get! : (@& FloatArray) → (@& Nat) → Float
-  | ⟨ds⟩, i => ds.get! i
+  | ⟨ds⟩, i => ds[i]!
 
 def get? (ds : FloatArray) (i : Nat) : Option Float :=
   if h : i < ds.size then
diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean
index f57dfaa75e..e4d088e2b9 100644
--- a/src/Init/Data/List/Attach.lean
+++ b/src/Init/Data/List/Attach.lean
@@ -239,6 +239,8 @@ theorem getElem?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h
       · simp_all
       · simp_all
 
+set_option linter.deprecated false in
+@[deprecated List.getElem?_pmap (since := "2025-02-12")]
 theorem get?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) (n : Nat) :
     get? (pmap f l h) n = Option.pmap f (get? l n) fun x H => h x (mem_of_get? H) := by
   simp only [get?_eq_getElem?]
@@ -259,6 +261,7 @@ theorem getElem_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h
     · simp
     · simp [hl]
 
+@[deprecated getElem_pmap (since := "2025-02-13")]
 theorem get_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) {n : Nat}
     (hn : n < (pmap f l h).length) :
     get (pmap f l h) ⟨n, hn⟩ =
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index 5d54b6a265..ea002f2d3e 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -246,46 +246,6 @@ theorem lex_cons_cons [BEq α] {a b} {as bs : List α} :
 
 /-! ## Alternative getters -/
 
-/-! ### get? -/
-
-/--
-Returns the `i`-th element in the list (zero-based).
-
-If the index is out of bounds (`i ≥ as.length`), this function returns `none`.
-Also see `get`, `getD` and `get!`.
--/
-def get? : (as : List α) → (i : Nat) → Option α
-  | a::_,  0   => some a
-  | _::as, n+1 => get? as n
-  | _,     _   => none
-
-@[simp] theorem get?_nil : @get? α [] n = none := rfl
-@[simp] theorem get?_cons_zero : @get? α (a::l) 0 = some a := rfl
-@[simp] theorem get?_cons_succ : @get? α (a::l) (n+1) = get? l n := rfl
-
-theorem ext_get? : ∀ {l₁ l₂ : List α}, (∀ n, l₁.get? n = l₂.get? n) → l₁ = l₂
-  | [], [], _ => rfl
-  | _ :: _, [], h => nomatch h 0
-  | [], _ :: _, 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_get? fun n => h (n+1)]
-
-/-! ### getD -/
-
-/--
-Returns the `i`-th element in the list (zero-based).
-
-If the index is out of bounds (`i ≥ as.length`), this function returns `fallback`.
-See also `get?` and `get!`.
--/
-def getD (as : List α) (i : Nat) (fallback : α) : α :=
-  (as.get? i).getD fallback
-
-@[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
-
 /-! ### getLast -/
 
 /--
diff --git a/src/Init/Data/List/BasicAux.lean b/src/Init/Data/List/BasicAux.lean
index d2db35e9ae..d23327576f 100644
--- a/src/Init/Data/List/BasicAux.lean
+++ b/src/Init/Data/List/BasicAux.lean
@@ -14,6 +14,53 @@ namespace List
 
 /-! ## Alternative getters -/
 
+/-! ### get? -/
+
+/--
+Returns the `i`-th element in the list (zero-based).
+
+If the index is out of bounds (`i ≥ as.length`), this function returns `none`.
+Also see `get`, `getD` and `get!`.
+-/
+@[deprecated "Use `a[i]?` instead." (since := "2025-02-12")]
+def get? : (as : List α) → (i : Nat) → Option α
+  | a::_,  0   => some a
+  | _::as, n+1 => get? as n
+  | _,     _   => none
+
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]?` instead." (since := "2025-02-12"), simp]
+theorem get?_nil : @get? α [] n = none := rfl
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]?` instead." (since := "2025-02-12"), simp]
+theorem get?_cons_zero : @get? α (a::l) 0 = some a := rfl
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]?` instead." (since := "2025-02-12"), simp]
+theorem get?_cons_succ : @get? α (a::l) (n+1) = get? l n := rfl
+
+set_option linter.deprecated false in
+@[deprecated "Use `List.ext_getElem?`." (since := "2025-02-12")]
+theorem ext_get? : ∀ {l₁ l₂ : List α}, (∀ n, l₁.get? n = l₂.get? n) → l₁ = l₂
+  | [], [], _ => rfl
+  | _ :: _, [], h => nomatch h 0
+  | [], _ :: _, 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_get? fun n => h (n+1)]
+
+/-! ### getD -/
+
+/--
+Returns the `i`-th element in the list (zero-based).
+
+If the index is out of bounds (`i ≥ as.length`), this function returns `fallback`.
+See also `get?` and `get!`.
+-/
+def getD (as : List α) (i : Nat) (fallback : α) : α :=
+  as[i]?.getD fallback
+
+@[simp] theorem getD_nil : getD [] n d = d := rfl
+
 /-! ### get! -/
 
 /--
@@ -22,14 +69,21 @@ Returns the `i`-th element in the list (zero-based).
 If the index is out of bounds (`i ≥ as.length`), this function panics when executed, and returns
 `default`. See `get?` and `getD` for safer alternatives.
 -/
+@[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]
 def get! [Inhabited α] : (as : List α) → (i : Nat) → α
   | a::_,  0   => a
   | _::as, n+1 => get! as n
   | _,     _   => panic! "invalid index"
 
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]
 theorem get!_nil [Inhabited α] (n : Nat) : [].get! n = (default : α) := rfl
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]
 theorem get!_cons_succ [Inhabited α] (l : List α) (a : α) (n : Nat) :
     (a::l).get! (n+1) = get! l n := rfl
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]
 theorem get!_cons_zero [Inhabited α] (l : List α) (a : α) : (a::l).get! 0 = a := rfl
 
 /-! ### getLast! -/
@@ -170,9 +224,10 @@ theorem getElem_append_right {as bs : List α} {i : Nat} (h₁ : as.length ≤ i
   induction as generalizing i with
   | nil => trivial
   | cons a as ih =>
-    cases i with simp [get, Nat.succ_sub_succ] <;> simp [Nat.succ_sub_succ] at h₁
+    cases i with simp [Nat.succ_sub_succ] <;> simp [Nat.succ_sub_succ] at h₁
     | succ i => apply ih; simp [h₁]
 
+@[deprecated "Deprecated without replacement." (since := "2025-02-13")]
 theorem get_last {as : List α} {i : Fin (length (as ++ [a]))} (h : ¬ i.1 < as.length) : (as ++ [a] : List _).get i = a := by
   cases i; rename_i i h'
   induction as generalizing i with
diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean
index 050b9edb59..6fb74acea5 100644
--- a/src/Init/Data/List/Find.lean
+++ b/src/Init/Data/List/Find.lean
@@ -577,10 +577,6 @@ theorem findIdx_getElem {xs : List α} {w : xs.findIdx p < xs.length} :
     p xs[xs.findIdx p] :=
   xs.findIdx_of_getElem?_eq_some (getElem?_eq_getElem w)
 
-@[deprecated findIdx_of_getElem?_eq_some (since := "2024-08-12")]
-theorem findIdx_of_get?_eq_some {xs : List α} (w : xs.get? (xs.findIdx p) = some y) : p y :=
-  findIdx_of_getElem?_eq_some (by simpa using w)
-
 @[deprecated findIdx_getElem (since := "2024-08-12")]
 theorem findIdx_get {xs : List α} {w : xs.findIdx p < xs.length} :
     p (xs.get ⟨xs.findIdx p, w⟩) :=
@@ -603,11 +599,6 @@ theorem findIdx_getElem?_eq_getElem_of_exists {xs : List α} (h : ∃ x ∈ xs,
     xs[xs.findIdx p]? = some (xs[xs.findIdx p]'(xs.findIdx_lt_length_of_exists h)) :=
   getElem?_eq_getElem (findIdx_lt_length_of_exists h)
 
-@[deprecated findIdx_getElem?_eq_getElem_of_exists (since := "2024-08-12")]
-theorem findIdx_get?_eq_get_of_exists {xs : List α} (h : ∃ x ∈ xs, p x) :
-    xs.get? (xs.findIdx p) = some (xs.get ⟨xs.findIdx p, xs.findIdx_lt_length_of_exists h⟩) :=
-  get?_eq_get (findIdx_lt_length_of_exists h)
-
 @[simp]
 theorem findIdx_eq_length {p : α → Bool} {xs : List α} :
     xs.findIdx p = xs.length ↔ ∀ x ∈ xs, p x = false := by
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index ff3296e6a9..b9d3e6df98 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -167,51 +167,38 @@ We simplify `l.get i` to `l[i.1]'i.2` and `l.get? i` to `l[i]?`.
 
 @[simp] theorem get_eq_getElem (l : List α) (i : Fin l.length) : l.get i = l[i.1]'i.2 := rfl
 
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]?` instead." (since := "2025-02-12")]
 theorem get?_eq_none : ∀ {l : List α} {n}, length l ≤ n → l.get? n = none
   | [], _, _ => rfl
   | _ :: l, _+1, h => get?_eq_none (l := l) <| Nat.le_of_succ_le_succ h
 
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]?` instead." (since := "2025-02-12")]
 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) _
 
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]?` instead." (since := "2025-02-12")]
 theorem get?_eq_some_iff : 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?_eq_none hn ▸ e
     ⟨this, by rwa [get?_eq_get this, Option.some.injEq] at e⟩,
   fun ⟨_, e⟩ => e ▸ get?_eq_get _⟩
 
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]?` instead." (since := "2025-02-12")]
 theorem get?_eq_none_iff : l.get? n = none ↔ length l ≤ n :=
   ⟨fun e => Nat.ge_of_not_lt (fun h' => by cases e ▸ get?_eq_some_iff.2 ⟨h', rfl⟩), get?_eq_none⟩
 
-@[simp] theorem get?_eq_getElem? (l : List α) (i : Nat) : l.get? i = l[i]? := by
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]?` instead." (since := "2025-02-12"), simp]
+theorem get?_eq_getElem? (l : List α) (i : Nat) : l.get? i = l[i]? := by
   simp only [getElem?_def]; split
   · exact (get?_eq_get ‹_›)
   · exact (get?_eq_none_iff.2 <| Nat.not_lt.1 ‹_›)
 
-/-! ### getD
-
-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) (i) (a : α) : getD l i a = (l[i]?).getD a := by
-  simp [getD]
-
-/-! ### get!
-
-We simplify `l.get! i` to `l[i]!`.
--/
-
-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 α) (i) : l.get! i = l[i]! := by
-  simp [get!_eq_getD]
-  rfl
-
 /-! ### getElem!
 
 We simplify `l[i]!` to `(l[i]?).getD default`.
@@ -226,8 +213,26 @@ We simplify `l[i]!` to `(l[i]?).getD default`.
 
 /-! ### getElem? and getElem -/
 
-@[simp] theorem getElem?_eq_none_iff : l[i]? = none ↔ length l ≤ i := by
-  simp only [← get?_eq_getElem?, get?_eq_none_iff]
+@[simp] theorem getElem?_nil {i : Nat} : ([] : List α)[i]? = none := rfl
+
+theorem getElem_cons {l : List α} (w : i < (a :: l).length) :
+    (a :: l)[i] =
+      if h : i = 0 then a else l[i-1]'(match i, h with | i+1, _ => succ_lt_succ_iff.mp w) := by
+  cases i <;> simp
+
+theorem getElem?_cons_zero {l : List α} : (a::l)[0]? = some a := by
+  simp [getElem?]
+
+@[simp] theorem getElem?_cons_succ {l : List α} : (a::l)[i+1]? = l[i]? := by
+  simp [getElem?, decidableGetElem?, Nat.succ_lt_succ_iff]
+
+theorem getElem?_cons : (a :: l)[i]? = if i = 0 then some a else l[i-1]? := by
+  cases i <;> simp [getElem?_cons_zero]
+
+@[simp] theorem getElem?_eq_none_iff : l[i]? = none ↔ length l ≤ i :=
+  match l with
+  | [] => by simp
+  | _ :: l => by simp
 
 @[simp] theorem none_eq_getElem?_iff {l : List α} {i : Nat} : none = l[i]? ↔ length l ≤ i := by
   simp [eq_comm (a := none)]
@@ -237,8 +242,15 @@ theorem getElem?_eq_none (h : length l ≤ i) : l[i]? = none := getElem?_eq_none
 @[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[i]? = some a ↔ ∃ h : i < l.length, l[i] = a := by
-  simp only [← get?_eq_getElem?, get?_eq_some_iff, get_eq_getElem]
+theorem getElem?_eq_some_iff {l : List α} : l[i]? = some a ↔ ∃ h : i < l.length, l[i] = a :=
+  match l with
+  | [] => by simp
+  | _ :: l => by
+    simp only [getElem?_cons, length_cons]
+    split <;> rename_i h
+    · simp_all
+    · match i, h with
+      | i + 1, h => simp [getElem?_eq_some_iff, Nat.succ_lt_succ_iff]
 
 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]
@@ -267,22 +279,6 @@ 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 {i : Nat} : ([] : List α)[i]? = none := rfl
-
-theorem getElem_cons {l : List α} (w : i < (a :: l).length) :
-    (a :: l)[i] =
-      if h : i = 0 then a else l[i-1]'(match i, h with | i+1, _ => succ_lt_succ_iff.mp w) := by
-  cases i <;> simp
-
-theorem getElem?_cons_zero {l : List α} : (a::l)[0]? = some a := by simp
-
-@[simp] theorem getElem?_cons_succ {l : List α} : (a::l)[i+1]? = l[i]? := by
-  simp only [← get?_eq_getElem?]
-  rfl
-
-theorem getElem?_cons : (a :: l)[i]? = if i = 0 then some a else l[i-1]? := by
-  cases i <;> simp
-
 @[simp] theorem getElem_singleton (a : α) (h : i < 1) : [a][i] = a :=
   match i, h with
   | 0, _ => rfl
@@ -304,7 +300,13 @@ theorem getElem_zero {l : List α} (h : 0 < l.length) : l[0] = l.head (length_po
   | _ :: _, _ => rfl
 
 @[ext] theorem ext_getElem? {l₁ l₂ : List α} (h : ∀ i : Nat, l₁[i]? = l₂[i]?) : l₁ = l₂ :=
-  ext_get? fun n => by simp_all
+  match l₁, l₂, h with
+  | [], [], _ => rfl
+  | _ :: _, [], h => by simpa using h 0
+  | [], _ :: _, h => by simpa using h 0
+  | a :: l₁, a' :: l₂, h => by
+    have h0 : some a = some a' := by simpa using h 0
+    injection h0 with aa; simp only [aa, ext_getElem? fun n => by simpa using h (n+1)]
 
 theorem ext_getElem {l₁ l₂ : List α} (hl : length l₁ = length l₂)
     (h : ∀ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length), l₁[i]'h₁ = l₂[i]'h₂) : l₁ = l₂ :=
@@ -322,6 +324,35 @@ theorem ext_getElem {l₁ l₂ : List α} (hl : length l₁ = length l₂)
 theorem getElem?_concat_length (l : List α) (a : α) : (l ++ [a])[l.length]? = some a := by
   simp
 
+/-! ### getD
+
+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) (i) (a : α) : getD l i a = (l[i]?).getD a := by
+  simp [getD]
+
+theorem getD_cons_zero : getD (x :: xs) 0 d = x := by simp
+theorem getD_cons_succ : getD (x :: xs) (n + 1) d = getD xs n d := by simp
+
+/-! ### get!
+
+We simplify `l.get! i` to `l[i]!`.
+-/
+
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]
+theorem get!_eq_getD [Inhabited α] : ∀ (l : List α) i, l.get! i = l.getD i default
+  | [], _      => rfl
+  | _a::_, 0   => by simp [get!]
+  | _a::l, n+1 => by simpa using get!_eq_getD l n
+
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]!` instead." (since := "2025-02-12"), simp]
+theorem get!_eq_getElem! [Inhabited α] (l : List α) (i) : l.get! i = l[i]! := by
+  simp [get!_eq_getD]
+
 /-! ### mem -/
 
 @[simp] theorem not_mem_nil (a : α) : ¬ a ∈ [] := nofun
@@ -771,7 +802,7 @@ theorem getLast_eq_getElem : ∀ (l : List α) (h : l ≠ []),
       | a :: l => exact Nat.le_refl _)
   | [_], _ => rfl
   | _ :: _ :: _, _ => by
-    simp [getLast, get, Nat.succ_sub_succ, getLast_eq_getElem]
+    simp [getLast, Nat.succ_sub_succ, getLast_eq_getElem]
 
 theorem getElem_length_sub_one_eq_getLast (l : List α) (h : l.length - 1 < l.length) :
     l[l.length - 1] = getLast l (by cases l; simp at h; simp) := by
@@ -844,10 +875,6 @@ theorem getLast?_cons {a : α} : (a::l).getLast? = l.getLast?.getD a := by
 @[simp] theorem getLast?_cons_cons : (a :: b :: l).getLast? = (b :: l).getLast? := by
   simp [getLast?_cons]
 
-@[deprecated getLast?_eq_getElem? (since := "2024-07-07")]
-theorem getLast?_eq_get? (l : List α) : getLast? l = l.get? (l.length - 1) := by
-  simp [getLast?_eq_getElem?]
-
 theorem getLast?_concat (l : List α) : getLast? (l ++ [a]) = some a := by
   simp [getLast?_eq_getElem?, Nat.succ_sub_succ]
 
@@ -3399,6 +3426,8 @@ theorem get_cons_succ' {as : List α} {i : Fin as.length} :
 theorem get_mk_zero : ∀ {l : List α} (h : 0 < l.length), l.get ⟨0, h⟩ = l.head (length_pos.mp h)
   | _::_, _ => rfl
 
+set_option linter.deprecated false in
+@[deprecated "Use `a[0]?` instead." (since := "2025-02-12")]
 theorem get?_zero (l : List α) : l.get? 0 = l.head? := by cases l <;> rfl
 
 /--
@@ -3410,10 +3439,14 @@ 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
 
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]?` instead." (since := "2025-02-12")]
 theorem get!_of_get? [Inhabited α] : ∀ {l : List α} {n}, get? l n = some a → get! l n = a
   | _a::_, 0, rfl => rfl
   | _::l, _+1, e => get!_of_get? (l := l) e
 
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]
 theorem get!_len_le [Inhabited α] : ∀ {l : List α} {n}, length l ≤ n → l.get! n = (default : α)
   | [], _, _ => rfl
   | _ :: l, _+1, h => get!_len_le (l := l) <| Nat.le_of_succ_le_succ h
@@ -3443,6 +3476,8 @@ 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⟩
 
+set_option linter.deprecated false in
+@[deprecated getElem?_of_mem (since := "2025-02-12")]
 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 _⟩
 
@@ -3450,12 +3485,16 @@ theorem get_mem : ∀ (l : List α) n, get l n ∈ l
   | _ :: _, ⟨0, _⟩ => .head ..
   | _ :: l, ⟨_+1, _⟩ => .tail _ (get_mem l ..)
 
+set_option linter.deprecated false in
+@[deprecated mem_of_getElem? (since := "2025-02-12")]
 theorem mem_of_get? {l : List α} {n a} (e : l.get? n = some a) : a ∈ l :=
   let ⟨_, e⟩ := get?_eq_some_iff.1 e; e ▸ get_mem ..
 
 theorem mem_iff_get {a} {l : List α} : a ∈ l ↔ ∃ n, get l n = a :=
   ⟨get_of_mem, fun ⟨_, e⟩ => e ▸ get_mem ..⟩
 
+set_option linter.deprecated false in
+@[deprecated mem_iff_getElem? (since := "2025-02-12")]
 theorem mem_iff_get? {a} {l : List α} : a ∈ l ↔ ∃ n, l.get? n = some a := by
   simp [getElem?_eq_some_iff, Fin.exists_iff, mem_iff_get]
 
@@ -3477,7 +3516,6 @@ theorem join_map_filter (p : α → Bool) (l : List (List α)) :
 @[deprecated flatten_eq_cons_iff (since := "2024-09-05")] abbrev join_eq_cons := @flatten_eq_cons_iff
 @[deprecated flatten_eq_append_iff (since := "2024-09-05")] abbrev join_eq_append := @flatten_eq_append_iff
 @[deprecated mem_of_getElem? (since := "2024-09-06")] abbrev getElem?_mem := @mem_of_getElem?
-@[deprecated mem_of_get? (since := "2024-09-06")] abbrev get?_mem := @mem_of_get?
 @[deprecated getElem_set_self (since := "2024-09-04")] abbrev getElem_set_eq := @getElem_set_self
 @[deprecated getElem?_set_self (since := "2024-09-04")] abbrev getElem?_set_eq := @getElem?_set_self
 @[deprecated set_eq_nil_iff (since := "2024-09-05")] abbrev set_eq_nil := @set_eq_nil_iff
@@ -3538,11 +3576,11 @@ theorem join_map_filter (p : α → Bool) (l : List (List α)) :
 @[deprecated any_flatMap (since := "2024-10-16")] abbrev any_bind := @any_flatMap
 @[deprecated all_flatMap (since := "2024-10-16")] abbrev all_bind := @all_flatMap
 
-@[deprecated get?_eq_none (since := "2024-11-29")] abbrev get?_len_le := @get?_eq_none
+@[deprecated get?_eq_none (since := "2024-11-29")] abbrev get?_len_le := @getElem?_eq_none
 @[deprecated getElem?_eq_some_iff (since := "2024-11-29")]
 abbrev getElem?_eq_some := @getElem?_eq_some_iff
 @[deprecated get?_eq_some_iff (since := "2024-11-29")]
-abbrev get?_eq_some := @get?_eq_some_iff
+abbrev get?_eq_some := @getElem?_eq_some_iff
 @[deprecated LawfulGetElem.getElem?_def (since := "2024-11-29")]
 theorem getElem?_eq (l : List α) (i : Nat) :
     l[i]? = if h : i < l.length then some l[i] else none :=
diff --git a/src/Init/Data/List/Nat/InsertIdx.lean b/src/Init/Data/List/Nat/InsertIdx.lean
index 9d6672641e..131abdd3e1 100644
--- a/src/Init/Data/List/Nat/InsertIdx.lean
+++ b/src/Init/Data/List/Nat/InsertIdx.lean
@@ -132,7 +132,7 @@ theorem getElem_insertIdx_of_lt {l : List α} {x : α} {n k : Nat} (hn : k < n)
     | nil => simp
     | cons _ _=>
       cases k
-      · simp [get]
+      · simp
       · rw [Nat.succ_lt_succ_iff] at hn
         simpa using ih hn _
 
diff --git a/src/Init/Data/List/Nat/Range.lean b/src/Init/Data/List/Nat/Range.lean
index 68eb4040d3..be2f56e6a2 100644
--- a/src/Init/Data/List/Nat/Range.lean
+++ b/src/Init/Data/List/Nat/Range.lean
@@ -368,7 +368,7 @@ theorem mk_mem_zipIdx_iff_le_and_getElem?_sub {k i : Nat} {x : α} {l : List α}
     simp [mk_add_mem_zipIdx_iff_getElem?, Nat.add_sub_cancel_left]
   else
     have : ∀ m, k + m ≠ i := by rintro _ rfl; simp at h
-    simp [h, mem_iff_get?, this]
+    simp [h, mem_iff_getElem?, this]
 
 /-- Variant of `mk_mem_zipIdx_iff_le_and_getElem?_sub` specialized at `k = 0`,
 to avoid the inequality and the subtraction. -/
diff --git a/src/Init/Data/List/Pairwise.lean b/src/Init/Data/List/Pairwise.lean
index e1da955d68..f038b50eba 100644
--- a/src/Init/Data/List/Pairwise.lean
+++ b/src/Init/Data/List/Pairwise.lean
@@ -301,11 +301,10 @@ theorem getElem?_inj {xs : List α}
     | i+1, 0 => ?_
     | 0, j+1 => ?_
     all_goals
-      simp only [get?_eq_getElem?, getElem?_cons_zero, getElem?_cons_succ] at h₂
+      simp only [getElem?_cons_zero, getElem?_cons_succ] at h₂
       cases h₁; rename_i h' h
       have := h x ?_ rfl; cases this
-      rw [mem_iff_get?]
-      simp only [get?_eq_getElem?]
+      rw [mem_iff_getElem?]
     exact ⟨_, h₂⟩; exact ⟨_ , h₂.symm⟩
 
 @[simp] theorem nodup_replicate {n : Nat} {a : α} :
diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean
index 91f88518cf..c8c0c1e400 100644
--- a/src/Init/Data/List/ToArray.lean
+++ b/src/Init/Data/List/ToArray.lean
@@ -73,6 +73,10 @@ theorem toArray_cons (a : α) (l : List α) : (a :: l).toArray = #[a] ++ l.toArr
 @[simp] theorem back?_toArray (l : List α) : l.toArray.back? = l.getLast? := by
   simp [back?, List.getLast?_eq_getElem?]
 
+@[simp] theorem back_toArray (l : List α) (h) :
+    l.toArray.back = l.getLast (by simp at h; exact ne_nil_of_length_pos h) := by
+  simp [back, List.getLast_eq_getElem]
+
 @[simp] theorem set_toArray (l : List α) (i : Nat) (a : α) (h : i < l.length) :
     (l.toArray.set i a) = (l.set i a).toArray := rfl
 
diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean
index 2f505bed00..6fe85b72ba 100644
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -70,8 +70,8 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
     (Vector.mk a h).back? = a.back? := rfl
 
 @[simp] theorem back_mk [NeZero n] (a : Array α) (h : a.size = n) :
-    (Vector.mk a h).back =
-      a[n - 1]'(Nat.lt_of_lt_of_eq (Nat.sub_one_lt (NeZero.ne n)) h.symm) := rfl
+    (Vector.mk a h).back = a.back (by have : 0 ≠ n := NeZero.ne' n; omega) := by
+  simp [back, Array.back, h]
 
 @[simp] theorem foldlM_mk [Monad m] (f : β → α → m β) (b : β) (a : Array α) (h : a.size = n) :
     (Vector.mk a h).foldlM f b = a.foldlM f b := rfl
diff --git a/src/Init/GetElem.lean b/src/Init/GetElem.lean
index 817d99cb2a..00fc14ff43 100644
--- a/src/Init/GetElem.lean
+++ b/src/Init/GetElem.lean
@@ -251,6 +251,20 @@ namespace Array
 instance : GetElem (Array α) Nat α fun xs i => i < xs.size where
   getElem xs i h := xs.get i h
 
+-- We provide a `GetElem?` instance, rather than using the low priority instance,
+-- so that we use the `@[extern]` definition of `get!`.
+instance : GetElem? (Array α) Nat α fun xs i => i < xs.size where
+  getElem? xs i := decidableGetElem? xs i
+  getElem! xs i := xs.get! i
+
+instance : LawfulGetElem (Array α) Nat α fun xs i => i < xs.size where
+  getElem?_def xs i h := by
+    simp only [getElem?, decidableGetElem?]
+    split <;> rfl
+  getElem!_def xs i := by
+    simp only [getElem!, getElem?, decidableGetElem?, get!, getD, getElem]
+    split <;> rfl
+
 @[simp] theorem get_eq_getElem (a : Array α) (i : Nat) (h) : a.get i h = a[i] := rfl
 
 @[simp] theorem get!_eq_getElem! [Inhabited α] (a : Array α) (i : Nat) : a.get! i = a[i]! := by
diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index 69d0e79537..1a49f03c58 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -735,8 +735,8 @@ def decodeNatLitVal? (s : String) : Option Nat :=
 def isLit? (litKind : SyntaxNodeKind) (stx : Syntax) : Option String :=
   match stx with
   | Syntax.node _ k args =>
-    if k == litKind && args.size == 1 then
-      match args.get! 0 with
+    if h : k == litKind ∧ args.size = 1 then
+      match args[0]'(Nat.lt_of_sub_eq_succ h.2) with
       | (Syntax.atom _ val) => some val
       | _ => none
     else
diff --git a/src/Init/Omega/IntList.lean b/src/Init/Omega/IntList.lean
index 4501c6021b..d7471b0ead 100644
--- a/src/Init/Omega/IntList.lean
+++ b/src/Init/Omega/IntList.lean
@@ -21,18 +21,18 @@ abbrev IntList := List Int
 namespace IntList
 
 /-- Get the `i`-th element (interpreted as `0` if the list is not long enough). -/
-def get (xs : IntList) (i : Nat) : Int := (xs.get? i).getD 0
+def get (xs : IntList) (i : Nat) : Int := xs[i]?.getD 0
 
 @[simp] theorem get_nil : get ([] : IntList) i = 0 := rfl
-@[simp] theorem get_cons_zero : get (x :: xs) 0 = x := rfl
-@[simp] theorem get_cons_succ : get (x :: xs) (i+1) = get xs i := rfl
+@[simp] theorem get_cons_zero : get (x :: xs) 0 = x := by simp [get]
+@[simp] theorem get_cons_succ : get (x :: xs) (i+1) = get xs i := by simp [get]
 
 theorem get_map {xs : IntList} (h : f 0 = 0) : get (xs.map f) i = f (xs.get i) := by
-  simp only [get, List.get?_eq_getElem?, List.getElem?_map]
+  simp only [get, 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_iff.mpr h]
+  rw [get, List.getElem?_eq_none_iff.mpr h]
   rfl
 
 /-- Like `List.set`, but right-pad with zeroes as necessary first. -/
@@ -62,7 +62,7 @@ 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 [get, add_def, List.get?_eq_getElem?, List.getElem?_zipWithAll]
+  simp only [get, add_def, List.getElem?_zipWithAll]
   cases xs[i]? <;> cases ys[i]? <;> simp
 
 @[simp] theorem add_nil (xs : IntList) : xs + [] = xs := by simp [add_def]
@@ -79,7 +79,7 @@ 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 [get, mul_def, List.get?_eq_getElem?, List.getElem?_zipWith]
+  simp only [get, mul_def, List.getElem?_zipWith]
   cases xs[i]? <;> cases ys[i]? <;> simp
 
 @[simp] theorem mul_nil_left : ([] : IntList) * ys = [] := rfl
@@ -94,7 +94,7 @@ 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 [get, neg_def, List.get?_eq_getElem?, List.getElem?_map]
+  simp only [get, neg_def, List.getElem?_map]
   cases xs[i]? <;> simp
 
 @[simp] theorem neg_nil : (- ([] : IntList)) = [] := rfl
@@ -120,7 +120,7 @@ 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 [get, smul_def, List.get?_eq_getElem?, List.getElem?_map]
+  simp only [get, smul_def, List.getElem?_map]
   cases xs[i]? <;> simp
 
 @[simp] theorem smul_nil {i : Int} : i * ([] : IntList) = [] := rfl
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 2ddb0efa4b..f94d8057b8 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -2663,12 +2663,14 @@ def Array.size {α : Type u} (a : @& Array α) : Nat :=
  a.toList.length
 
 /--
+Use the indexing notation `a[i]` instead.
+
 Access an element from an array without needing a runtime bounds checks,
 using a `Nat` index and a proof that it is in bounds.
 
 This function does not use `get_elem_tactic` to automatically find the proof that
 the index is in bounds. This is because the tactic itself needs to look up values in
-arrays. Use the indexing notation `a[i]` instead.
+arrays.
 -/
 @[extern "lean_array_fget"]
 def Array.get {α : Type u} (a : @& Array α) (i : @& Nat) (h : LT.lt i a.size) : α :=
@@ -2678,7 +2680,11 @@ def Array.get {α : Type u} (a : @& Array α) (i : @& Nat) (h : LT.lt i a.size)
 @[inline] abbrev Array.getD (a : Array α) (i : Nat) (v₀ : α) : α :=
   dite (LT.lt i a.size) (fun h => a.get i h) (fun _ => v₀)
 
-/-- Access an element from an array, or panic if the index is out of bounds. -/
+/--
+Use the indexing notation `a[i]!` instead.
+
+Access an element from an array, or panic if the index is out of bounds.
+-/
 @[extern "lean_array_get"]
 def Array.get! {α : Type u} [Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
   Array.getD a i default
diff --git a/src/Lean/Compiler/IR/PushProj.lean b/src/Lean/Compiler/IR/PushProj.lean
index a7f2e9fdf5..2985b31302 100644
--- a/src/Lean/Compiler/IR/PushProj.lean
+++ b/src/Lean/Compiler/IR/PushProj.lean
@@ -20,7 +20,7 @@ partial def pushProjs (bs : Array FnBody) (alts : Array Alt) (altsF : Array Inde
     let push (x : VarId) :=
         if !ctxF.contains x.idx then
           let alts := alts.mapIdx fun i alt => alt.modifyBody fun b' =>
-             if (altsF.get! i).contains x.idx then b.setBody b'
+             if altsF[i]!.contains x.idx then b.setBody b'
              else b'
           let altsF  := altsF.map fun s => if s.contains x.idx then b.collectFreeIndices s else s
           pushProjs bs alts altsF ctx ctxF
diff --git a/src/Lean/Compiler/IR/SimpCase.lean b/src/Lean/Compiler/IR/SimpCase.lean
index fe73f7e8f7..e1519f8412 100644
--- a/src/Lean/Compiler/IR/SimpCase.lean
+++ b/src/Lean/Compiler/IR/SimpCase.lean
@@ -18,7 +18,7 @@ def ensureHasDefault (alts : Array Alt) : Array Alt :=
     alts.push (Alt.default last.body)
 
 private def getOccsOf (alts : Array Alt) (i : Nat) : Nat := Id.run do
-  let aBody := (alts.get! i).body
+  let aBody := alts[i]!.body
   let mut n := 1
   for h : j in [i+1:alts.size] do
     if alts[j].body == aBody then
@@ -52,8 +52,8 @@ private def mkSimpCase (tid : Name) (x : VarId) (xType : IRType) (alts : Array A
   let alts := addDefault alts;
   if alts.size == 0 then
     FnBody.unreachable
-  else if alts.size == 1 then
-    (alts.get! 0).body
+  else if _ : alts.size = 1 then
+    alts[0].body
   else
     FnBody.case tid x xType alts
 
diff --git a/src/Lean/Data/FuzzyMatching.lean b/src/Lean/Data/FuzzyMatching.lean
index 1ee2cd7ea9..d3ab316f6b 100644
--- a/src/Lean/Data/FuzzyMatching.lean
+++ b/src/Lean/Data/FuzzyMatching.lean
@@ -109,13 +109,13 @@ private def fuzzyMatchCore (pattern word : String) (patternRoles wordRoles : Arr
   let mut penaltyNs : Int := 0
   let mut penaltySkip : Int := 0
   for wordIdx in [:word.length] do
-    if (wordIdx != 0) && (wordRoles.get! wordIdx) matches .separator then
+    if (wordIdx != 0) && wordRoles[wordIdx]! matches .separator then
       -- reset skip penalty at namespace separator
       penaltySkip := 0
       -- add constant penalty for each namespace to prefer shorter namespace nestings
       penaltyNs := penaltyNs + 1
       lastSepIdx := wordIdx
-    penaltySkip := penaltySkip + skipPenalty (wordRoles.get! wordIdx) (wordIdx == 0)
+    penaltySkip := penaltySkip + skipPenalty wordRoles[wordIdx]! (wordIdx == 0)
     startPenalties := startPenalties.set! wordIdx $ penaltySkip + penaltyNs
 
   -- TODO: the following code is assuming all characters are ASCII
@@ -124,8 +124,8 @@ private def fuzzyMatchCore (pattern word : String) (patternRoles wordRoles : Arr
    `word.length - pattern.length` at each index (because at the very end, we can only consider fuzzy matches
     of `pattern` with a longer substring of `word`). -/
     for wordIdx in [patternIdx:word.length-(pattern.length - patternIdx - 1)] do
-      let missScore? := 
-        if wordIdx >= 1 then 
+      let missScore? :=
+        if wordIdx >= 1 then
           selectBest
             (getMiss result patternIdx (wordIdx - 1))
             (getMatch result patternIdx (wordIdx - 1))
@@ -133,29 +133,29 @@ private def fuzzyMatchCore (pattern word : String) (patternRoles wordRoles : Arr
 
       let mut matchScore? := none
 
-      if allowMatch (pattern.get ⟨patternIdx⟩) (word.get ⟨wordIdx⟩) (patternRoles.get! patternIdx) (wordRoles.get! wordIdx) then
-        if patternIdx >= 1 then 
-          let runLength := runLengths.get! (getIdx (patternIdx - 1) (wordIdx - 1)) + 1
+      if allowMatch (pattern.get ⟨patternIdx⟩) (word.get ⟨wordIdx⟩) patternRoles[patternIdx]! wordRoles[wordIdx]! then
+        if patternIdx >= 1 then
+          let runLength := runLengths[getIdx (patternIdx - 1) (wordIdx - 1)]! + 1
           runLengths := runLengths.set! (getIdx patternIdx wordIdx) runLength
 
           matchScore? := selectBest
             (getMiss result (patternIdx - 1) (wordIdx - 1) |>.map (· + matchResult
               patternIdx wordIdx
-              (patternRoles.get! patternIdx) (wordRoles.get! wordIdx)
+              patternRoles[patternIdx]! wordRoles[wordIdx]!
               none
-            - startPenalties.get! wordIdx))
+            - startPenalties[wordIdx]!))
             (getMatch result (patternIdx - 1) (wordIdx - 1) |>.map (· + matchResult
               patternIdx wordIdx
-              (patternRoles.get! patternIdx) (wordRoles.get! wordIdx)
+              patternRoles[patternIdx]! wordRoles[wordIdx]!
               (.some runLength)
             )) |>.map fun score => if wordIdx >= lastSepIdx then score + 1 else score -- main identifier bonus
         else
           runLengths := runLengths.set! (getIdx patternIdx wordIdx) 1
           matchScore? := .some $ matchResult
               patternIdx wordIdx
-              (patternRoles.get! patternIdx) (wordRoles.get! wordIdx)
+              patternRoles[patternIdx]! wordRoles[wordIdx]!
               none
-              - startPenalties.get! wordIdx
+              - startPenalties[wordIdx]!
 
       result := set result patternIdx wordIdx missScore? matchScore?
 
@@ -167,10 +167,10 @@ private def fuzzyMatchCore (pattern word : String) (patternRoles wordRoles : Arr
     getIdx (patternIdx wordIdx : Nat) := patternIdx * word.length + wordIdx
 
     getMiss (result : Array (Option Int)) (patternIdx wordIdx : Nat) : Option Int :=
-      result.get! $ getDoubleIdx patternIdx wordIdx
+      result[getDoubleIdx patternIdx wordIdx]!
 
     getMatch (result : Array (Option Int)) (patternIdx wordIdx : Nat) : Option Int :=
-      result.get! $ getDoubleIdx patternIdx wordIdx + 1
+      result[getDoubleIdx patternIdx wordIdx + 1]!
 
     set (result : Array (Option Int)) (patternIdx wordIdx : Nat) (missValue matchValue : Option Int) : Array (Option Int) :=
       let idx := getDoubleIdx patternIdx wordIdx
@@ -213,7 +213,7 @@ private def fuzzyMatchCore (pattern word : String) (patternRoles wordRoles : Arr
       /- Consecutive character match. -/
       if let some bonus := consecutive then
         /- consecutive run bonus -/
-        score := score + bonus 
+        score := score + bonus
       return score
 
 /-- Match the given pattern with the given word using a fuzzy matching
diff --git a/src/Lean/Data/Json/Basic.lean b/src/Lean/Data/Json/Basic.lean
index 8efce0000d..3d19a2ada0 100644
--- a/src/Lean/Data/Json/Basic.lean
+++ b/src/Lean/Data/Json/Basic.lean
@@ -275,7 +275,7 @@ def getObjVal? : Json → String → Except String Json
 
 def getArrVal? : Json → Nat → Except String Json
   | arr a, i =>
-    match a.get? i with
+    match a[i]? with
     | some v => return v
     | none => throw s!"index out of bounds: {i}"
   | _    , _ => throw "array expected"
diff --git a/src/Lean/Data/PersistentArray.lean b/src/Lean/Data/PersistentArray.lean
index 39877e000a..b4d0f40507 100644
--- a/src/Lean/Data/PersistentArray.lean
+++ b/src/Lean/Data/PersistentArray.lean
@@ -66,7 +66,7 @@ partial def getAux [Inhabited α] : PersistentArrayNode α → USize → USize 
 
 def get! [Inhabited α] (t : PersistentArray α) (i : Nat) : α :=
   if i >= t.tailOff then
-    t.tail.get! (i - t.tailOff)
+    t.tail[i - t.tailOff]!
   else
     getAux t.root (USize.ofNat i) t.shift
 
@@ -175,8 +175,8 @@ def pop (t : PersistentArray α) : PersistentArray α :=
       let last       := last.pop
       let newSize    := t.size - 1
       let newTailOff := newSize - last.size
-      if newRoots.size == 1 && (newRoots.get! 0).isNode then
-        { root    := newRoots.get! 0,
+      if h : ∃ _ : newRoots.size = 1, newRoots[0].isNode then
+        { root    := newRoots[0]'(have := h.1; by omega),
           shift   := t.shift - initShift,
           size    := newSize,
           tail    := last,
@@ -199,7 +199,7 @@ variable {β : Type v}
 @[specialize] private partial def foldlFromMAux (f : β → α → m β) : PersistentArrayNode α → USize → USize → β → m β
   | node cs, i, shift, b => do
     let j    := (div2Shift i shift).toNat
-    let b ← foldlFromMAux f (cs.get! j) (mod2Shift i shift) (shift - initShift) b
+    let b ← foldlFromMAux f cs[j]! (mod2Shift i shift) (shift - initShift) b
     cs.foldlM (init := b) (start := j+1) fun b c => foldlMAux f c b
   | leaf vs, i, _, b => vs.foldlM (init := b) (start := i.toNat) f
 
diff --git a/src/Lean/Data/PersistentHashMap.lean b/src/Lean/Data/PersistentHashMap.lean
index 8df0aa505c..c6b2380731 100644
--- a/src/Lean/Data/PersistentHashMap.lean
+++ b/src/Lean/Data/PersistentHashMap.lean
@@ -149,7 +149,7 @@ partial def findAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.s
 partial def findAux [BEq α] : Node α β → USize → α → Option β
   | Node.entries entries, h, k =>
     let j     := (mod2Shift h shift).toNat
-    match entries.get! j with
+    match entries[j]! with
     | Entry.null       => none
     | Entry.ref node   => findAux node (div2Shift h shift) k
     | Entry.entry k' v => if k == k' then some v else none
@@ -180,7 +180,7 @@ partial def findEntryAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : k
 partial def findEntryAux [BEq α] : Node α β → USize → α → Option (α × β)
   | Node.entries entries, h, k =>
     let j     := (mod2Shift h shift).toNat
-    match entries.get! j with
+    match entries[j]! with
     | Entry.null       => none
     | Entry.ref node   => findEntryAux node (div2Shift h shift) k
     | Entry.entry k' v => if k == k' then some (k', v) else none
@@ -199,7 +199,7 @@ partial def containsAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : ke
 partial def containsAux [BEq α] : Node α β → USize → α → Bool
   | Node.entries entries, h, k =>
     let j     := (mod2Shift h shift).toNat
-    match entries.get! j with
+    match entries[j]! with
     | Entry.null       => false
     | Entry.ref node   => containsAux node (div2Shift h shift) k
     | Entry.entry k' _ => k == k'
@@ -242,7 +242,7 @@ partial def eraseAux [BEq α] : Node α β → USize → α → Node α β
     | none     => n
   | n@(Node.entries entries), h, k =>
     let j       := (mod2Shift h shift).toNat
-    let entry   := entries.get! j
+    let entry   := entries[j]!
     match entry with
     | Entry.null       => n
     | Entry.entry k' _ =>
diff --git a/src/Lean/Data/Position.lean b/src/Lean/Data/Position.lean
index 0336684b62..de64636b8b 100644
--- a/src/Lean/Data/Position.lean
+++ b/src/Lean/Data/Position.lean
@@ -80,7 +80,7 @@ partial def toPosition (fmap : FileMap) (pos : String.Pos) : Position :=
         if e == b + 1 then { line := fmap.getLine b, column := toColumn posB 0 }
         else
           let m := (b + e) / 2;
-          let posM := ps.get! m;
+          let posM := ps[m]!
           if pos == posM then { line := fmap.getLine m, column := 0 }
           else if pos > posM then loop m e
           else loop b m
diff --git a/src/Lean/Data/Trie.lean b/src/Lean/Data/Trie.lean
index d545741199..bdb0163421 100644
--- a/src/Lean/Data/Trie.lean
+++ b/src/Lean/Data/Trie.lean
@@ -119,7 +119,7 @@ partial def find? (t : Trie α) (s : String) : Option α :=
         let c := s.getUtf8Byte i h
         match cs.findIdx? (· == c) with
         | none   => none
-        | some idx => loop (i + 1) (ts.get! idx)
+        | some idx => loop (i + 1) ts[idx]!
       else
         val
   loop 0 t
@@ -155,7 +155,7 @@ partial def findPrefix (t : Trie α) (pre : String) : Array α := go t 0
         | node _val cs ts =>
           match cs.findIdx? (· == c) with
           | none   => .empty
-          | some idx => go (ts.get! idx) (i + 1)
+          | some idx => go ts[idx]! (i + 1)
       else
         t.values
 
@@ -180,7 +180,7 @@ partial def matchPrefix (s : String) (t : Trie α) (i : String.Pos) : Option α
         let c := s.getUtf8Byte i h
         match cs.findIdx? (· == c) with
         | none => res
-        | some idx => loop (ts.get! idx) (i + 1) res
+        | some idx => loop ts[idx]! (i + 1) res
       else
         res
   loop t i.byteIdx none
diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index b9bf6a73a2..1e6b900bef 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -333,7 +333,7 @@ private def getFieldType (infos : Array StructFieldInfo) (parentType : Expr) (fi
           let Name.str _ subFieldName .. := subProjName
             | throwError "invalid projection name {subProjName}"
           let args := e.getAppArgs
-          if let some major := args.get? numParams then
+          if let some major := args[numParams]? then
             if (← getNestedProjectionArg major) == parent then
               if let some existingFieldInfo := findFieldInfo? infos (.mkSimple subFieldName) then
                 return TransformStep.done <| mkAppN existingFieldInfo.fvar args[numParams+1:args.size]
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean
index 27d01ac5a7..a5ad663832 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean
@@ -39,7 +39,7 @@ def reconstructCounterExample (var2Cnf : Std.HashMap BVBit Nat) (assignment : Ar
     Array (Expr × BVExpr.PackedBitVec) := Id.run do
   let mut sparseMap : Std.HashMap Nat (RBMap Nat Bool Ord.compare) := {}
   let filter bvBit _ :=
-    let (_, _, synthetic) := atomsAssignment.get! bvBit.var
+    let (_, _, synthetic) := atomsAssignment[bvBit.var]!
     !synthetic
   let var2Cnf := var2Cnf.filter filter
   for (bitVar, cnfVar) in var2Cnf.toArray do
@@ -74,7 +74,7 @@ def reconstructCounterExample (var2Cnf : Std.HashMap BVBit Nat) (assignment : Ar
       if bitValue then
         value := value ||| (1 <<< currentBit)
       currentBit := currentBit + 1
-    let (_, atomExpr, _) := atomsAssignment.get! bitVecVar
+    let (_, atomExpr, _) := atomsAssignment[bitVecVar]!
     finalMap := finalMap.push (atomExpr, ⟨BitVec.ofNat currentBit value⟩)
   return finalMap
 
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index eac29e0e8b..2a2f5b6bf8 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -241,7 +241,7 @@ where
                     new := promise
                     old? := do
                       let old ← old?
-                      return ⟨old.stx, (← old.next.get? 0)⟩
+                      return ⟨old.stx, (← old.next[0]?)⟩
                   } }) do
                     evalTactic stx'
                   return
diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index ffc66f0c4d..ff1ce8f7ad 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -73,7 +73,7 @@ where
         if let some state := oldParsed.finished.get.state? then
           reusableResult? := some ((), state)
           -- only allow `next` reuse in this case
-          oldNext? := oldParsed.next.get? 0 |>.map (⟨old.stx, ·⟩)
+          oldNext? := oldParsed.next[0]?.map (⟨old.stx, ·⟩)
 
       let next ← IO.Promise.new
       let finished ← IO.Promise.new
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 01afdc2ef4..033ef692dc 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -77,6 +77,13 @@ abbrev ModuleIdx.toNat (midx : ModuleIdx) : Nat := midx
 
 instance : Inhabited ModuleIdx where default := (0 : Nat)
 
+instance : GetElem (Array α) ModuleIdx α (fun a i => i.toNat < a.size) where
+  getElem a i h := a[i.toNat]
+
+instance : GetElem? (Array α) ModuleIdx α (fun a i => i.toNat < a.size) where
+  getElem? a i := a[i.toNat]?
+  getElem! a i := a[i.toNat]!
+
 abbrev ConstMap := SMap Name ConstantInfo
 
 structure Import where
@@ -1102,7 +1109,7 @@ namespace PersistentEnvExtension
 
 def getModuleEntries {α β σ : Type} [Inhabited σ] (ext : PersistentEnvExtension α β σ) (env : Environment) (m : ModuleIdx) : Array α :=
   -- `importedEntries` is identical on all environment branches, so `local` is always sufficient
-  (ext.toEnvExtension.getState (asyncMode := .local) env).importedEntries.get! m
+  (ext.toEnvExtension.getState (asyncMode := .local) env).importedEntries[m]!
 
 def addEntry {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : Environment) (b : β) : Environment :=
   ext.toEnvExtension.modifyState env fun s =>
diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index 57b3599e9b..6ccc44fb9f 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -751,7 +751,7 @@ def mkAppN (f : Expr) (args : Array Expr) : Expr :=
   args.foldl mkApp f
 
 private partial def mkAppRangeAux (n : Nat) (args : Array Expr) (i : Nat) (e : Expr) : Expr :=
-  if i < n then mkAppRangeAux n args (i+1) (mkApp e (args.get! i)) else e
+  if i < n then mkAppRangeAux n args (i+1) (mkApp e args[i]!) else e
 
 /-- `mkAppRange f i j #[a_1, ..., a_i, ..., a_j, ... ]` ==> the expression `f a_i ... a_{j-1}` -/
 def mkAppRange (f : Expr) (i j : Nat) (args : Array Expr) : Expr :=
@@ -1467,7 +1467,7 @@ private partial def mkAppRevRangeAux (revArgs : Array Expr) (start : Nat) (b : E
   if i == start then b
   else
     let i := i - 1
-    mkAppRevRangeAux revArgs start (mkApp b (revArgs.get! i)) i
+    mkAppRevRangeAux revArgs start (mkApp b revArgs[i]!) i
 
 /-- `mkAppRevRange f b e args == mkAppRev f (revArgs.extract b e)` -/
 def mkAppRevRange (f : Expr) (beginIdx endIdx : Nat) (revArgs : Array Expr) : Expr :=
diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean
index dd3be8a93b..6f3278e641 100644
--- a/src/Lean/Level.lean
+++ b/src/Lean/Level.lean
@@ -359,7 +359,7 @@ private partial def isExplicitSubsumedAux (lvls : Array Level) (maxExplicit : Na
 private def isExplicitSubsumed (lvls : Array Level) (firstNonExplicit : Nat) : Bool :=
   if firstNonExplicit == 0 then false
   else
-    let max := (lvls.get! (firstNonExplicit - 1)).getOffset;
+    let max := lvls[firstNonExplicit - 1]!.getOffset
     isExplicitSubsumedAux lvls max firstNonExplicit
 
 partial def normalize (l : Level) : Level :=
diff --git a/src/Lean/Linter/UnusedVariables.lean b/src/Lean/Linter/UnusedVariables.lean
index 7d7abe40bb..b733d8ec92 100644
--- a/src/Lean/Linter/UnusedVariables.lean
+++ b/src/Lean/Linter/UnusedVariables.lean
@@ -196,7 +196,7 @@ builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ =>
 /-- `inductive Foo where | unused : Foo` -/
 builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ =>
   stack.matches [`null, none, `null, none, ``Lean.Parser.Command.inductive] &&
-  (stack.get? 3 |>.any fun (stx, pos) =>
+  (stack[3]? |>.any fun (stx, pos) =>
     pos == 0 &&
     [``Lean.Parser.Command.optDeclSig, ``Lean.Parser.Command.declSig].any (stx.isOfKind ·)))
 
@@ -206,7 +206,7 @@ builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ =>
 -/
 builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ =>
   stack.matches [`null, none, `null, ``Lean.Parser.Command.optDeclSig, none] &&
-  (stack.get? 4 |>.any fun (stx, _) =>
+  (stack[4]? |>.any fun (stx, _) =>
     [``Lean.Parser.Command.ctor, ``Lean.Parser.Command.structSimpleBinder].any (stx.isOfKind ·)))
 
 /--
@@ -215,7 +215,7 @@ builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ =>
 -/
 builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ =>
   stack.matches [`null, none, `null, ``Lean.Parser.Command.declSig, none] &&
-  (stack.get? 4 |>.any fun (stx, _) =>
+  (stack[4]? |>.any fun (stx, _) =>
     [``Lean.Parser.Command.opaque, ``Lean.Parser.Command.axiom].any (stx.isOfKind ·)))
 
 /--
@@ -225,10 +225,10 @@ Definition with foreign definition
 -/
 builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ =>
   stack.matches [`null, none, `null, none, none, ``Lean.Parser.Command.declaration] &&
-  (stack.get? 3 |>.any fun (stx, _) =>
+  (stack[3]? |>.any fun (stx, _) =>
     stx.isOfKind ``Lean.Parser.Command.optDeclSig ||
     stx.isOfKind ``Lean.Parser.Command.declSig) &&
-  (stack.get? 5 |>.any fun (stx, _) => match stx[0] with
+  (stack[5]? |>.any fun (stx, _) => match stx[0] with
     | `(Lean.Parser.Command.declModifiersT| $[$_:docComment]? @[$[$attrs:attr],*] $[$vis]? $[noncomputable]?) =>
       attrs.any (fun attr => attr.raw.isOfKind ``Parser.Attr.extern || attr matches `(attr| implemented_by $_))
     | _ => false))
@@ -247,8 +247,8 @@ Function argument in let declaration (when `linter.unusedVariables.funArgs` is f
 builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack opts =>
   !getLinterUnusedVariablesFunArgs opts &&
   stack.matches [`null, none, `null, ``Lean.Parser.Term.letIdDecl, none] &&
-  (stack.get? 3 |>.any fun (_, pos) => pos == 1) &&
-  (stack.get? 5 |>.any fun (stx, _) => !stx.isOfKind ``Lean.Parser.Term.structInstField))
+  (stack[3]? |>.any fun (_, pos) => pos == 1) &&
+  (stack[5]? |>.any fun (stx, _) => !stx.isOfKind ``Lean.Parser.Term.structInstField))
 
 /--
 Function argument in declaration signature (when `linter.unusedVariables.funArgs` is false)
@@ -257,7 +257,7 @@ Function argument in declaration signature (when `linter.unusedVariables.funArgs
 builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack opts =>
   !getLinterUnusedVariablesFunArgs opts &&
   stack.matches [`null, none, `null, none] &&
-  (stack.get? 3 |>.any fun (stx, pos) =>
+  (stack[3]? |>.any fun (stx, pos) =>
     pos == 0 &&
     [``Lean.Parser.Command.optDeclSig, ``Lean.Parser.Command.declSig].any (stx.isOfKind ·)))
 
diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean
index 300d18c821..3ff45c2ffa 100644
--- a/src/Lean/LocalContext.lean
+++ b/src/Lean/LocalContext.lean
@@ -252,8 +252,8 @@ def getFVars (lctx : LocalContext) : Array Expr :=
   lctx.getFVarIds.map mkFVar
 
 private partial def popTailNoneAux (a : PArray (Option LocalDecl)) : PArray (Option LocalDecl) :=
-  if a.size == 0 then a
-  else match a.get! (a.size - 1) with
+  if h : a.size = 0 then a
+  else match a[a.size - 1] with
     | none   => popTailNoneAux a.pop
     | some _ => a
 
@@ -268,8 +268,8 @@ def erase (lctx : LocalContext) (fvarId : FVarId) : LocalContext :=
 def pop (lctx : LocalContext): LocalContext :=
   match lctx with
   | { fvarIdToDecl := map, decls := decls } =>
-    if decls.size == 0 then lctx
-    else match decls.get! (decls.size - 1) with
+    if _ : decls.size = 0 then lctx
+    else match decls[decls.size - 1] with
       | none      => lctx -- unreachable
       | some decl => { fvarIdToDecl := map.erase decl.fvarId, decls := popTailNoneAux decls.pop }
 
@@ -293,7 +293,7 @@ def getUnusedName (lctx : LocalContext) (suggestion : Name) : Name :=
   else suggestion
 
 def lastDecl (lctx : LocalContext) : Option LocalDecl :=
-  lctx.decls.get! (lctx.decls.size - 1)
+  lctx.decls[lctx.decls.size - 1]!
 
 def setUserName (lctx : LocalContext) (fvarId : FVarId) (userName : Name) : LocalContext :=
   let decl := lctx.get! fvarId
@@ -340,7 +340,7 @@ def numIndices (lctx : LocalContext) : Nat :=
   lctx.decls.size
 
 def getAt? (lctx : LocalContext) (i : Nat) : Option LocalDecl :=
-  lctx.decls.get! i
+  lctx.decls[i]!
 
 @[specialize] def foldlM [Monad m] (lctx : LocalContext) (f : β → LocalDecl → m β) (init : β) (start : Nat := 0) : m β :=
   lctx.decls.foldlM (init := init) (start := start) fun b decl => match decl with
diff --git a/src/Lean/Meta/LazyDiscrTree.lean b/src/Lean/Meta/LazyDiscrTree.lean
index 33c39f7801..aa56f01fe4 100644
--- a/src/Lean/Meta/LazyDiscrTree.lean
+++ b/src/Lean/Meta/LazyDiscrTree.lean
@@ -486,7 +486,7 @@ private partial def evalLazyEntries
 
 private def evalNode (c : TrieIndex) :
     MatchM α (Array α × TrieIndex × Std.HashMap Key TrieIndex) := do
-  let .node vs star cs pending := (←get).get! c
+  let .node vs star cs pending := (←get)[c]!
   if pending.size = 0 then
     return (vs, star, cs)
   else
diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index d8909221a4..8c0399d658 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -599,8 +599,8 @@ private def processArrayLit (p : Problem) : MetaM (Array Problem) := do
   let sizes := collectArraySizes p
   let subgoals ← caseArraySizes p.mvarId x.fvarId! sizes
   subgoals.mapIdxM fun i subgoal => do
-    if i < sizes.size then
-      let size     := sizes.get! i
+    if h : i < sizes.size then
+      let size     := sizes[i]
       let subst    := subgoal.subst
       let elems    := subgoal.elems.toList
       let newVars  := elems.map mkFVar ++ xs
diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index af203e1419..409685809b 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -547,7 +547,7 @@ def generate : SynthM Unit := do
   else
     let key  := gNode.key
     let idx  := gNode.currInstanceIdx - 1
-    let inst := gNode.instances.get! idx
+    let inst := gNode.instances[idx]!
     let mctx := gNode.mctx
     let mvar := gNode.mvar
     /- See comment at `typeHasMVars` -/
diff --git a/src/Lean/Meta/Tactic/Induction.lean b/src/Lean/Meta/Tactic/Induction.lean
index ff62ef476e..13631015b3 100644
--- a/src/Lean/Meta/Tactic/Induction.lean
+++ b/src/Lean/Meta/Tactic/Induction.lean
@@ -131,23 +131,25 @@ Remark: `mvarId` and `tacticName` are used to generate error messages.
 def getMajorTypeIndices (mvarId : MVarId) (tacticName : Name) (recursorInfo : RecursorInfo) (majorType : Expr) : MetaM (Array Expr) := do
   let majorTypeArgs := majorType.getAppArgs
   recursorInfo.indicesPos.toArray.mapM fun idxPos => do
-    if idxPos ≥ majorTypeArgs.size then throwTacticEx tacticName mvarId m!"major premise type is ill-formed{indentExpr majorType}"
-    let idx := majorTypeArgs.get! idxPos
-    unless idx.isFVar do throwTacticEx tacticName mvarId m!"major premise type index {idx} is not a variable{indentExpr majorType}"
-    majorTypeArgs.size.forM fun i _ => do
-      let arg := majorTypeArgs[i]
-      if i != idxPos && arg == idx then
-        throwTacticEx tacticName mvarId m!"'{idx}' is an index in major premise, but it occurs more than once{indentExpr majorType}"
-      if i < idxPos then
-        if (← exprDependsOn arg idx.fvarId!) then
-          throwTacticEx tacticName mvarId m!"'{idx}' is an index in major premise, but it occurs in previous arguments{indentExpr majorType}"
-      -- If arg is also and index and a variable occurring after `idx`, we need to make sure it doesn't depend on `idx`.
-      -- Note that if `arg` is not a variable, we will fail anyway when we visit it.
-      if i > idxPos && recursorInfo.indicesPos.contains i && arg.isFVar then
-        let idxDecl ← idx.fvarId!.getDecl
-        if (← localDeclDependsOn idxDecl arg.fvarId!) then
-          throwTacticEx tacticName mvarId m!"'{idx}' is an index in major premise, but it depends on index occurring at position #{i+1}"
-    return idx
+    if h : idxPos ≥ majorTypeArgs.size then
+      throwTacticEx tacticName mvarId m!"major premise type is ill-formed{indentExpr majorType}"
+    else
+      let idx := majorTypeArgs[idxPos]
+      unless idx.isFVar do throwTacticEx tacticName mvarId m!"major premise type index {idx} is not a variable{indentExpr majorType}"
+      majorTypeArgs.size.forM fun i _ => do
+        let arg := majorTypeArgs[i]
+        if i != idxPos && arg == idx then
+          throwTacticEx tacticName mvarId m!"'{idx}' is an index in major premise, but it occurs more than once{indentExpr majorType}"
+        if i < idxPos then
+          if (← exprDependsOn arg idx.fvarId!) then
+            throwTacticEx tacticName mvarId m!"'{idx}' is an index in major premise, but it occurs in previous arguments{indentExpr majorType}"
+        -- If arg is also and index and a variable occurring after `idx`, we need to make sure it doesn't depend on `idx`.
+        -- Note that if `arg` is not a variable, we will fail anyway when we visit it.
+        if i > idxPos && recursorInfo.indicesPos.contains i && arg.isFVar then
+          let idxDecl ← idx.fvarId!.getDecl
+          if (← localDeclDependsOn idxDecl arg.fvarId!) then
+            throwTacticEx tacticName mvarId m!"'{idx}' is an index in major premise, but it depends on index occurring at position #{i+1}"
+      return idx
 
 /--
 Auxiliary method for implementing `induction`-like tactics.
@@ -173,8 +175,10 @@ def mkRecursorAppPrefix (mvarId : MVarId) (tacticName : Name) (majorFVarId : FVa
             match univPos with
             | RecursorUnivLevelPos.motive => pure (recursorLevels.push targetLevel, true)
             | RecursorUnivLevelPos.majorType idx =>
-              if idx ≥ majorTypeFnLevels.size then throwTacticEx tacticName mvarId "ill-formed recursor"
-              pure (recursorLevels.push (majorTypeFnLevels.get! idx), foundTargetLevel)
+              if h : idx ≥ majorTypeFnLevels.size then
+                throwTacticEx tacticName mvarId "ill-formed recursor"
+              else
+                pure (recursorLevels.push majorTypeFnLevels[idx], foundTargetLevel)
       if !foundTargetLevel && !targetLevel.isZero then
         throwTacticEx tacticName mvarId m!"recursor '{recursorInfo.recursorName}' can only eliminate into Prop"
       let recursor := mkConst recursorInfo.recursorName recursorLevels.toList
diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index cfe55ffb18..2d65dc3062 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -332,7 +332,7 @@ mutual
           unless projInfo.fromClass do return none
           let args := e.getAppArgs
           -- First check whether `e`s instance is stuck.
-          if let some major := args.get? projInfo.numParams then
+          if let some major := args[projInfo.numParams]? then
             if let some mvarId ← getStuckMVar? major then
               return mvarId
           /-
diff --git a/src/Lean/Parser/Types.lean b/src/Lean/Parser/Types.lean
index a825bddf04..2f778c36a5 100644
--- a/src/Lean/Parser/Types.lean
+++ b/src/Lean/Parser/Types.lean
@@ -177,7 +177,7 @@ def back (stack : SyntaxStack) : Syntax :=
 
 def get! (stack : SyntaxStack) (i : Nat) : Syntax :=
   if i < stack.size then
-    stack.raw.get! (stack.drop + i)
+    stack.raw[stack.drop + i]!
   else
     panic! "SyntaxStack.get!: element is inaccessible"
 
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 2e7f912a42..eab8ac1b65 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -882,9 +882,9 @@ def delabLam : Delab :=
           -- as a term, i.e. a single `Syntax.ident` or an application thereof
           let stxCurNames ←
             if h : curNames.size > 1 then
-              `($(curNames.get! 0) $(curNames.eraseIdx 0)*)
+              `($(curNames[0]!) $(curNames.eraseIdx 0)*)
             else
-              pure $ curNames.get! 0;
+              pure $ curNames[0]!;
           `(funBinder| ($stxCurNames : $stxT))
         else
           pure curNames.back!  -- here `curNames.size == 1`
diff --git a/src/Lean/Server/Completion/CompletionResolution.lean b/src/Lean/Server/Completion/CompletionResolution.lean
index c071840192..0bca6ca38f 100644
--- a/src/Lean/Server/Completion/CompletionResolution.lean
+++ b/src/Lean/Server/Completion/CompletionResolution.lean
@@ -112,7 +112,7 @@ def resolveCompletionItem?
     (completionInfoPos : Nat)
     : IO CompletionItem := do
   let completionInfos := findCompletionInfosAt fileMap hoverPos cmdStx infoTree
-  let some i := completionInfos.get? completionInfoPos
+  let some i := completionInfos[completionInfoPos]?
     | return item
   i.ctx.runMetaM i.info.lctx (item.resolve id)
 
diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index aae83847d2..031f7ec6f0 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -199,7 +199,7 @@ def locationLinksOfInfo (kind : GoToKind) (ictx : InfoWithCtx)
             | .app fn arg => do pure $ (← extractInstances fn).append (← extractInstances arg)
             | .mdata _ e => extractInstances e
             | _ => pure #[]
-          if let some instArg := appArgs.get? instIdx then
+          if let some instArg := appArgs[instIdx]? then
             for inst in (← extractInstances instArg) do
               results := results.append (← ci.runMetaM i.lctx <| locationLinksFromDecl i inst)
             results := results.append elaborators -- put elaborators at the end of the results
diff --git a/src/Lean/Server/References.lean b/src/Lean/Server/References.lean
index 2fa0e7936b..06ece422fa 100644
--- a/src/Lean/Server/References.lean
+++ b/src/Lean/Server/References.lean
@@ -209,7 +209,7 @@ def getModuleContainingDecl? (env : Environment) (declName : Name) : Option Name
   if env.constants.map₂.contains declName then
     return env.header.mainModule
   let modIdx ← env.getModuleIdxFor? declName
-  env.allImportedModuleNames.get? modIdx
+  env.allImportedModuleNames[modIdx]?
 
 /--
 Determines the `RefIdent` for the `Info` `i` of an identifier in `module` and
diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean
index 020e7eaeef..2bacc95fdc 100644
--- a/src/Lean/Syntax.lean
+++ b/src/Lean/Syntax.lean
@@ -90,7 +90,7 @@ namespace SyntaxNode
   withArgs n fun args => args.size
 
 @[inline] def getArg (n : SyntaxNode) (i : Nat) : Syntax :=
-  withArgs n fun args => args.get! i
+  withArgs n fun args => args[i]!
 
 @[inline] def getArgs (n : SyntaxNode) : Array Syntax :=
   withArgs n fun args => args
diff --git a/src/Lean/Util/Profiler.lean b/src/Lean/Util/Profiler.lean
index fc5f6b4f05..ce21352d75 100644
--- a/src/Lean/Util/Profiler.lean
+++ b/src/Lean/Util/Profiler.lean
@@ -285,7 +285,7 @@ def Profile.export (name : String) (startTime : Float) (traceStates : Array Trac
     let traces := traceStates.map (·.traces.toArray)
     -- sort traces of thread by start time
     let traces := traces.qsort (fun tr1 tr2 =>
-      let f tr := tr.get? 0 |>.bind (getFirstStart? ·.msg) |>.getD 0
+      let f tr := tr[0]? |>.bind (getFirstStart? ·.msg) |>.getD 0
       f tr1 < f tr2)
     let mut traces := traces.flatMap id |>.map (·.msg)
     if tid = 0 then
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
index 41d343c3dd..4b7b97b38e 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
@@ -69,7 +69,7 @@ theorem limplies_of_assignmentsInvariant {n : Nat} (f : DefaultFormula n)
   · next h =>
     specialize f_AssignmentsInvariant h p pf
     by_cases hpi : p i <;> simp [hpi, Entails.eval] at f_AssignmentsInvariant
-  · next h => simp_all [getElem!, i.2.2, decidableGetElem?]
+  · next h => simp_all [getElem!_def, i.2.2, decidableGetElem?]
 
 /--
 performRupAdd adds to f.rupUnits and then clears f.rupUnits. If f begins with some units in f.rupUnits,
@@ -496,8 +496,8 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
               have idx_in_bounds2 : idx < f.clauses.size := by
                 conv => rhs; rw [Array.size_toArray]
                 exact hbound
-              simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, ↓reduceDIte,
-                Fin.eta, Array.get_eq_getElem, ← Array.getElem_toList, decidableGetElem?] at heq
+              simp only [id_eq_idx, getElem!_def, idx_in_bounds2, Array.getElem?_eq_getElem, ←
+                Array.getElem_toList] at heq
               rw [hidx, hl] at heq
               simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
               simp only [← heq] at l_ne_b
@@ -529,8 +529,8 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
               have idx_in_bounds2 : idx < f.clauses.size := by
                 conv => rhs; rw [Array.size_toArray]
                 exact hbound
-              simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, ↓reduceDIte,
-                Fin.eta, Array.get_eq_getElem, ← Array.getElem_toList, decidableGetElem?] at heq
+              simp only [id_eq_idx, getElem!_def, idx_in_bounds2, Array.getElem?_eq_getElem, ←
+                Array.getElem_toList] at heq
               rw [hidx, hl] at heq
               simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
               have i_eq_l : i = l.1 := by rw [← heq]
@@ -589,8 +589,8 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
               have idx_in_bounds2 : idx < f.clauses.size := by
                 conv => rhs; rw [Array.size_toArray]
                 exact hbound
-              simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, ↓reduceDIte,
-                Fin.eta, Array.get_eq_getElem, ← Array.getElem_toList, decidableGetElem?] at heq
+              simp only [id_eq_idx, getElem!_def, idx_in_bounds2, Array.getElem?_eq_getElem, ←
+                Array.getElem_toList] at heq
               rw [hidx] at heq
               simp only [Option.some.injEq] at heq
               rw [← heq] at hl
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
index 5143b81630..c421e8eb9a 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
@@ -398,7 +398,7 @@ theorem assignmentsInvariant_performRupCheck_of_assignmentsInvariant {n : Nat} (
       omega
     rw [Array.foldl_induction in_bounds_motive in_bounds_base in_bounds_inductive]
     exact i.2.2
-  simp only [getElem!, i_in_bounds, dite_true, Array.get_eq_getElem, decidableGetElem?] at h1
+  simp only [getElem!_def, i_in_bounds, Array.getElem?_eq_getElem] at h1
   simp only [( · ⊨ ·), Entails.eval.eq_1]
   by_cases hb : b
   · rw [hb]
@@ -462,8 +462,8 @@ theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n)
     · rw [← Array.mem_toList]
       apply Array.getElem_mem_toList
     · rw [Array.getElem_toList] at c'_in_f
-      simp only [getElem!, Array.getElem_range, i_lt_f_clauses_size, dite_true,
-        c'_in_f, DefaultClause.contains_iff, Array.get_eq_getElem, decidableGetElem?]
+      simp only [Array.getElem_range, getElem!_def, i_lt_f_clauses_size, Array.getElem?_eq_getElem,
+        c'_in_f, contains_iff]
       simpa [Clause.toList] using negPivot_in_c'
   rcases List.get_of_mem h with ⟨j, h'⟩
   have j_in_bounds : j < ratHints.size := by
@@ -475,7 +475,7 @@ theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n)
   rw [Array.getElem_toList] at h'
   rw [Array.getElem_toList] at c'_in_f
   exists ⟨j.1, j_in_bounds⟩
-  simp [getElem!, h', i_lt_f_clauses_size, dite_true, c'_in_f, decidableGetElem?]
+  simp [getElem!_def, h', i_lt_f_clauses_size, dite_true, c'_in_f]
 
 theorem performRatCheck_success_of_performRatCheck_fold_success {n : Nat} (f : DefaultFormula n)
     (hf : f.ratUnits = #[] ∧ f.assignments.size = n) (p : Literal (PosFin n))
@@ -511,12 +511,12 @@ theorem performRatCheck_success_of_performRatCheck_fold_success {n : Nat} (f : D
           omega
         rcases i_lt_or_eq_idx with i_lt_idx | i_eq_idx
         · exact ih.2 acc_eq_true ⟨i.1, i_lt_idx⟩
-        · simp only [getElem!, i_eq_idx, idx.2, Fin.getElem_fin, dite_true, decidableGetElem?]
+        · simp only [getElem!_def, Fin.getElem?_fin, i_eq_idx, idx.2, Array.getElem?_eq_getElem]
           simp only [Fin.getElem_fin, ih.1] at h
           exact h
       · simp at h
   have h := (Array.foldl_induction motive h_base h_inductive).2 performRatCheck_fold_success i
-  simpa [getElem!, i.2, dite_true, decidableGetElem?] using h
+  simpa [getElem!_def, i.2, dite_true] using h
 
 theorem safe_insert_of_performRatCheck_fold_success {n : Nat} (f : DefaultFormula n)
     (f_readyForRatAdd : ReadyForRatAdd f) (c : DefaultClause n) (pivot : Literal (PosFin n))
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
index ee001fdb78..7366c6f391 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
@@ -118,8 +118,8 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
           · rw [Array.getElem_modify_self]
             simp only [← i_eq_l, h1]
           · constructor
-            · simp only [getElem!, l_in_bounds, ↓reduceDIte, Array.get_eq_getElem,
-                Bool.not_eq_true, decidableGetElem?] at h3
+            · simp only [getElem!_def, l_in_bounds, Array.getElem?_eq_getElem,
+                Bool.not_eq_true] at h3
               simp only [← i_eq_l, ← h1]
               simp only [i_eq_l, h3]
             · intro k hk
@@ -183,7 +183,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
         | true, true =>
           exfalso
           have assignments_i_rw : assignments[i.1]! = assignments[i.1] := by
-            simp only [getElem!, i_in_bounds, ↓reduceDIte, Array.get_eq_getElem, decidableGetElem?]
+            simp only [getElem!_def, i_in_bounds, Array.getElem?_eq_getElem]
           rw [hl, ← i_eq_l, assignments_i_rw, h2] at h5
           exact h5 (has_add _ true)
         | true, false =>
@@ -206,7 +206,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                   | neg =>
                     simp only [addAssignment, addPosAssignment, h, ite_true] at h2
                     simp only [i_eq_l] at h2
-                    simp [hasAssignment, hl, getElem!, l_in_bounds, h2, hasNegAssignment, decidableGetElem?] at h5
+                    simp [hasAssignment, hl, getElem!_def, l_in_bounds, h2, hasNegAssignment] at h5
                   | both => simp +decide only [h] at h3
                 · intro k k_ne_j k_ne_l
                   rw [Array.getElem_push]
@@ -242,7 +242,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                   | pos =>
                     simp only [addAssignment, h, ite_false, addNegAssignment, reduceCtorEq] at h2
                     simp only [i_eq_l] at h2
-                    simp [hasAssignment, hl, getElem!, l_in_bounds, h2, hasPosAssignment, decidableGetElem?] at h5
+                    simp [hasAssignment, hl, getElem!_def, l_in_bounds, h2, hasPosAssignment] at h5
                   | neg  => simp +decide only [h] at h3
                   | both => simp +decide only [h] at h3
                 · intro k k_ne_l k_ne_j
@@ -263,7 +263,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
         | false, false =>
           exfalso
           have assignments_i_rw : assignments[i.1]! = assignments[i.1] := by
-            simp [getElem!, i_in_bounds, decidableGetElem?]
+            simp [getElem!_def, i_in_bounds]
           rw [hl, ← i_eq_l, assignments_i_rw, h2] at h5
           exact h5 (has_add _ false)
       · next i_ne_l =>
@@ -355,7 +355,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                   · exact k_eq_units_size
                 simp only [k_eq_units_size, Array.getElem_push_eq, ne_eq]
                 intro l_eq_i
-                simp [getElem!, l_eq_i, i_in_bounds, h3, has_both, decidableGetElem?] at h
+                simp [getElem!_def, l_eq_i, i_in_bounds, h3, has_both] at h
 
 theorem insertUnitInvariant_insertUnit_fold {n : Nat} (assignments0 : Array Assignment)
     (assignments0_size : assignments0.size = n) (rupUnits : Array (Literal (PosFin n)))
@@ -791,8 +791,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
         · simp only [l_eq_i, Array.getElem_modify_self, List.get, h1]
         · constructor
           · simp only [List.get, Bool.not_eq_true]
-            simp only [getElem!, l_in_bounds, ↓reduceDIte, Array.get_eq_getElem,
-              Bool.not_eq_true, decidableGetElem?] at h
+            simp only [getElem!_def, l_in_bounds, Array.getElem?_eq_getElem, Bool.not_eq_true] at h
             simp only [l_eq_i, h1] at h
             exact h
           · intro k k_ne_zero
@@ -840,7 +839,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
         intro l_eq_l'
         rw [l_eq_i] at h
         simp only [l'] at l_eq_l'
-        simp [getElem!, i_in_bounds, h1, l_eq_l', has_add, decidableGetElem?] at h
+        simp [getElem!_def, i_in_bounds, h1, l_eq_l', has_add] at h
       by_cases l.2
       · next l_eq_true =>
         rw [l_eq_true] at l_ne_l'
@@ -863,9 +862,9 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
             · constructor
               · simp only [l'] at l'_eq_false
                 simp only [l'_eq_false, hasAssignment, ite_false] at h2
-                simp only [hasAssignment, l_eq_true, getElem!, l_eq_i, i_in_bounds,
-                  Array.get_eq_getElem, ↓reduceIte, ↓reduceDIte, h1, addAssignment, l'_eq_false,
-                  hasPos_addNeg, decidableGetElem?, reduceCtorEq] at h
+                simp only [hasAssignment, l_eq_true, ↓reduceIte, l_eq_i, getElem!_def, i_in_bounds,
+                  Array.getElem?_eq_getElem, h1, addAssignment, l'_eq_false, reduceCtorEq,
+                  hasPos_addNeg, l'] at h
                 exact unassigned_of_has_neither _ h h2
               · intro k k_ne_zero k_ne_j_succ
                 have k_eq_succ : ∃ k' : Nat, ∃ k'_succ_in_bounds : k' + 1 < (l :: acc.2.1).length, k = ⟨k' + 1, k'_succ_in_bounds⟩ := by
@@ -912,8 +911,9 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
             · constructor
               · simp only [l'] at l'_eq_true
                 simp only [hasAssignment, l'_eq_true, ite_true] at h2
-                simp only [hasAssignment, l_eq_false, ↓reduceIte, ↓reduceDIte, getElem!, l_eq_i, i_in_bounds,
-                  Array.get_eq_getElem, h1, addAssignment, l'_eq_true, hasNeg_addPos, decidableGetElem?, reduceCtorEq] at h
+                simp only [hasAssignment, l_eq_false, reduceCtorEq, ↓reduceIte, l_eq_i,
+                  getElem!_def, i_in_bounds, Array.getElem?_eq_getElem, h1, addAssignment,
+                  l'_eq_true, hasNeg_addPos, l'] at h
                 exact unassigned_of_has_neither _ h2 h
               · intro k k_ne_j_succ k_ne_zero
                 have k_eq_succ : ∃ k' : Nat, ∃ k'_succ_in_bounds : k' + 1 < (l :: acc.2.1).length, k = ⟨k' + 1, k'_succ_in_bounds⟩ := by
@@ -992,7 +992,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
       simp only [hasAssignment, Bool.not_eq_true] at h
       split at h
       all_goals
-        simp +decide [getElem!, l_eq_i, i_in_bounds, h1, decidableGetElem?] at h
+        simp +decide [getElem!_def, l_eq_i, i_in_bounds, h1] at h
     constructor
     · rw [Array.getElem_modify_of_ne l_ne_i]
       exact h1
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
index 6e8fec9cdc..937d69b42f 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
@@ -49,17 +49,19 @@ theorem contradiction_of_insertUnit_success {n : Nat} (assignments : Array Assig
         exact h
     · apply Exists.intro l.1
       simp only [insertUnit, hl, ite_false, Array.getElem_modify_self, reduceCtorEq]
-      simp only [getElem!, l_in_bounds, dite_true, decidableGetElem?] at assignments_l_ne_unassigned
+      simp only [getElem!_def, l_in_bounds, Array.getElem?_eq_getElem,
+        insertUnit_res] at assignments_l_ne_unassigned
       by_cases l.2
       · next l_eq_true =>
         simp only [l_eq_true]
-        simp only [hasAssignment, l_eq_true, hasPosAssignment, getElem!, l_in_bounds, dite_true, ite_true,
-          Bool.not_eq_true, decidableGetElem?] at hl
+        simp only [hasAssignment, l_eq_true, getElem!_def, l_in_bounds, Array.getElem?_eq_getElem,
+          ite_true, hasPosAssignment, Bool.not_eq_true, insertUnit_res] at hl
         split at hl <;> simp_all +decide
       · next l_eq_false =>
         simp only [Bool.not_eq_true] at l_eq_false
         simp only [l_eq_false]
-        simp [hasAssignment, l_eq_false, hasNegAssignment, getElem!, l_in_bounds, decidableGetElem?] at hl
+        simp [hasAssignment, l_eq_false, hasNegAssignment, getElem!_def, l_in_bounds,
+          Array.getElem?_eq_getElem] at hl
         split at hl <;> simp_all +decide
 
 theorem contradiction_of_insertUnit_fold_success {n : Nat} (assignments : Array Assignment) (assignments_size : assignments.size = n)
@@ -679,16 +681,17 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin
           have i_in_bounds : i.1 < acc.1.size := by rw [hsize]; exact i.2.2
           by_cases l.1 = i.1
           · next l_eq_i =>
-            simp only [getElem!, Array.size_modify, i_in_bounds, ↓ reduceDIte,
-              Array.get_eq_getElem, l_eq_i, Array.getElem_modify_self (addAssignment b), decidableGetElem?]
-            simp only [getElem!, i_in_bounds, dite_true, Array.get_eq_getElem, decidableGetElem?] at pacc
+            simp only [l_eq_i, getElem!_def, Array.size_modify, i_in_bounds,
+              Array.getElem?_eq_getElem, Array.getElem_modify_self (addAssignment b)]
+            simp only [getElem!_def, i_in_bounds, Array.getElem?_eq_getElem] at pacc
             by_cases pi : p i
             · simp only [pi, decide_false]
               simp only [hasAssignment, pi, decide_false, ite_false] at pacc
               by_cases hb : b
               · simp only [hasAssignment, ↓reduceIte, addAssignment]
                 simp only [hb]
-                simp [hasAssignment, addAssignment, hb, ite_true, ite_false, hasNeg_addPos]
+                simp only [Bool.true_eq_false, decide_false, Bool.false_eq_true, ↓reduceIte,
+                  hasNeg_addPos]
                 exact pacc
               · exfalso -- hb, pi, l_eq_i, and plb are incompatible
                 simp only [Bool.not_eq_true] at hb
@@ -703,10 +706,9 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin
                 simp only [hasAssignment, ite_true] at pacc
                 exact pacc
           · next l_ne_i =>
-            simp only [getElem!, Array.size_modify, i_in_bounds,
-              Array.getElem_modify_of_ne l_ne_i, dite_true,
-              Array.get_eq_getElem, decidableGetElem?]
-            simp only [getElem!, i_in_bounds, dite_true, decidableGetElem?] at pacc
+            simp only [getElem!_def, Array.size_modify, i_in_bounds, Array.getElem?_eq_getElem,
+              Array.getElem_modify_of_ne l_ne_i]
+            simp only [getElem!_def, i_in_bounds, Array.getElem?_eq_getElem] at pacc
             exact pacc
       · apply And.intro hsize ∘ And.intro h1
         simp
diff --git a/src/Std/Time/Zoned/Database/Basic.lean b/src/Std/Time/Zoned/Database/Basic.lean
index 7b046d2ce7..b23224de3c 100644
--- a/src/Std/Time/Zoned/Database/Basic.lean
+++ b/src/Std/Time/Zoned/Database/Basic.lean
@@ -47,7 +47,7 @@ def convertUt : Bool → UTLocal
 Converts a given time index into a `LocalTimeType` by using a time zone (`tz`) and its identifier.
 -/
 def convertLocalTimeType (index : Nat) (tz : TZif.TZifV1) (identifier : String) : Option LocalTimeType := do
-  let localType ← tz.localTimeTypes.get? index
+  let localType ← tz.localTimeTypes[index]?
   let offset := Offset.ofSeconds <| .ofInt localType.gmtOffset
   let abbreviation ← tz.abbreviations.getD index (offset.toIsoString true)
   let wallflag := convertWall (tz.stdWallIndicators.getD index true)
@@ -66,10 +66,10 @@ def convertLocalTimeType (index : Nat) (tz : TZif.TZifV1) (identifier : String)
 Converts a transition.
 -/
 def convertTransition (times: Array LocalTimeType) (index : Nat) (tz : TZif.TZifV1) : Option Transition := do
-  let time := tz.transitionTimes.get! index
+  let time := tz.transitionTimes[index]!
   let time := Second.Offset.ofInt time
-  let indice := tz.transitionIndices.get! index
-  return { time, localTimeType := times.get! indice.toNat }
+  let indice := tz.transitionIndices[index]!
+  return { time, localTimeType := times[indice.toNat]! }
 
 /--
 Converts a `TZif.TZifV1` structure to a `ZoneRules` structure.
diff --git a/src/Std/Time/Zoned/Database/TZdb.lean b/src/Std/Time/Zoned/Database/TZdb.lean
index 4a5ebd2deb..7b280ab1dc 100644
--- a/src/Std/Time/Zoned/Database/TZdb.lean
+++ b/src/Std/Time/Zoned/Database/TZdb.lean
@@ -60,8 +60,8 @@ Extracts a timezone ID from a file path.
 -/
 def idFromPath (path : System.FilePath) : Option String := do
   let res := path.components.toArray
-  let last ← res.get? (res.size - 1)
-  let last₁ ← res.get? (res.size - 2)
+  let last ← res[res.size - 1]?
+  let last₁ ← res[res.size - 2]?
 
   if last₁ = some "zoneinfo"
     then last.trim
diff --git a/src/Std/Time/Zoned/Database/TzIf.lean b/src/Std/Time/Zoned/Database/TzIf.lean
index 3822d582f8..06df0acb12 100644
--- a/src/Std/Time/Zoned/Database/TzIf.lean
+++ b/src/Std/Time/Zoned/Database/TzIf.lean
@@ -243,7 +243,7 @@ private def parseAbbreviations (times : Array LocalTimeType) (n : UInt32) : Pars
 
   for time in times do
     for indx in [time.abbreviationIndex.toNat:n.toNat] do
-      let char := chars.get! indx
+      let char := chars[indx]!
       if char = 0 then
         strings := strings.push current
         current := ""
diff --git a/src/Std/Time/Zoned/ZoneRules.lean b/src/Std/Time/Zoned/ZoneRules.lean
index 27fc8b6558..d648786073 100644
--- a/src/Std/Time/Zoned/ZoneRules.lean
+++ b/src/Std/Time/Zoned/ZoneRules.lean
@@ -155,7 +155,7 @@ If the timestamp falls between two transitions, it returns the most recent trans
 -/
 def findTransitionForTimestamp (transitions : Array Transition) (timestamp : Timestamp) : Option Transition :=
   if let some idx := findTransitionIndexForTimestamp transitions timestamp
-    then transitions.get? (idx - 1)
+    then transitions[idx - 1]?
     else transitions.back?
 
 /--
diff --git a/tests/compiler/534.lean b/tests/compiler/534.lean
index 4dad681ac2..549a977c01 100644
--- a/tests/compiler/534.lean
+++ b/tests/compiler/534.lean
@@ -5,7 +5,7 @@ def foo (array : Array Nat) : Nat -> Nat
     if array.isEmpty then
       0
     else
-      let arrayOfLast := #[array.back]
+      let arrayOfLast := #[array.back!]
       foo arrayOfLast n
 
 def main : IO Unit :=
diff --git a/tests/lean/run/generalizeTelescope.lean b/tests/lean/run/generalizeTelescope.lean
index f750529cac..22ca23bba8 100644
--- a/tests/lean/run/generalizeTelescope.lean
+++ b/tests/lean/run/generalizeTelescope.lean
@@ -18,7 +18,7 @@ let n1    := mkApp succ n
 let vecN1 := mkApp2 (mkConst `Vec) nat n1
 withLocalDeclD `xs vecN1 fun xs => do
 generalizeTelescope #[n1, xs] fun ys => do
-let t ← mkLambdaFVars ys ys.back
+let t ← mkLambdaFVars ys ys.back!
 trace[Meta.debug] t
 pure ()
 
@@ -35,7 +35,7 @@ let vecN1 := mkApp2 (mkConst `Vec) nat n1
 withLocalDeclD `xs vecN1 $ fun xs => do
 let e ← mkEqRefl xs
 generalizeTelescope #[n1, xs, e] fun ys => do
-let t ← mkLambdaFVars ys ys.back
+let t ← mkLambdaFVars ys ys.back!
 trace[Meta.debug] t
 pure ()
 
@@ -56,7 +56,7 @@ withLocalDeclD `xs vecN1 $ fun xs => do
 let e ← mkEqRefl xs
 failIfSuccess do
   generalizeTelescope #[n1, e] fun ys => do
-  let t ← mkLambdaFVars ys ys.back
+  let t ← mkLambdaFVars ys ys.back!
   trace[Meta.debug] t
   pure ()
 trace[Meta.debug] "failed as expected"