Merge remote-tracking branch 'origin/master' into back_get

cleanup
fix tests
2026-03-19 03:14:08 +00:00 · 2025-02-17 12:12:48 +11:00 · 2025-02-17 12:08:14 +11:00 · 2025-02-14 14:48:36 +11:00 · 2025-02-14 14:13:14 +11:00 · 2025-02-13 10:58:20 +11:00
59 changed files with 405 additions and 286 deletions
--- 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
--- 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
--- 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
--- 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]
--- 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
--- 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
--- 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⟩ =
--- 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 -/

 /--
--- 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
--- 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
--- 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 :=
--- 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 _

--- 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. -/
--- 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 : α} :
--- 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

--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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

--- 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
--- 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"
--- 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

--- 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' _ =>
--- 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
--- 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
--- 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]
--- 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

--- 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
--- 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
--- 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 =>
--- 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 :=
--- 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 :=
--- 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 ·)))

--- 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
--- 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
--- 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
--- 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` -/
--- 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
--- 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
          /-
--- 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"

--- 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`
--- 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)

--- 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
--- 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
--- 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
--- 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
--- 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
--- 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))
--- 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
--- 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
--- 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.
--- 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
--- 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 := ""
--- 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?

 /--
--- 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 :=
--- 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"
Author	SHA1	Message	Date
Kim Morrison	f1d1b28d12	Merge remote-tracking branch 'origin/master' into back_get	2025-02-17 12:12:48 +11:00
Kim Morrison	37e851d82e	cleanup	2025-02-17 12:08:14 +11:00
Kim Morrison	5699f29ba1	fix tests	2025-02-14 14:48:36 +11:00
Kim Morrison	bd98715f0c	fix tests	2025-02-14 14:13:14 +11:00
Kim Morrison	24feb34190	.	2025-02-13 10:58:20 +11:00
Kim Morrison	45a3bb6af1	.	2025-02-13 10:58:19 +11:00
Kim Morrison	d4cf3ec0ff	.	2025-02-13 10:58:19 +11:00
Kim Morrison	6501af8a16	.	2025-02-13 10:58:19 +11:00
Kim Morrison	a9891d7173	.	2025-02-13 10:58:19 +11:00
Kim Morrison	5ce7ce1605	deprecating List.get? too	2025-02-13 10:58:19 +11:00
Kim Morrison	1151636139	chore: deprecate Array.get?, add Array.back	2025-02-13 10:58:19 +11:00