update expected output

Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>

src/Init/Data/Array/Basic.lean

@@ -166,13 +166,14 @@ count of 1 when called.
 -/
 @[extern "lean_array_fswap"]
 def swap (a : Array α) (i j : @& Fin a.size) : Array α :=
-  let v₁ := a.get i
+  let v₁ := a[i]
-  let v₂ := a.get j
+  let v₂ := a[j]
   let a'  := a.set i v₂
   a'.set j v₁ (Nat.lt_of_lt_of_eq j.isLt (size_set a i v₂ _).symm)
 
 @[simp] theorem size_swap (a : Array α) (i j : Fin a.size) : (a.swap i j).size = a.size := by
-  show ((a.set i (a.get j)).set j (a.get i) (Nat.lt_of_lt_of_eq j.isLt (size_set a i (a.get j) _).symm)).size = a.size
+  show ((a.set i a[j]).set j a[i]
+    (Nat.lt_of_lt_of_eq j.isLt (size_set a i a[j] _).symm)).size = a.size
   rw [size_set, size_set]
 
 /--
@@ -249,7 +250,7 @@ def back? (a : Array α) : Option α :=
   a.get? (a.size - 1)
 
 @[inline] def swapAt (a : Array α) (i : Fin a.size) (v : α) : α × Array α :=
-  let e := a.get i
+  let e := a[i]
   let a := a.set i v
   (e, a)
 
@@ -273,24 +274,22 @@ def take (a : Array α) (n : Nat) : Array α :=
 @[inline]
 unsafe def modifyMUnsafe [Monad m] (a : Array α) (i : Nat) (f : α → m α) : m (Array α) := do
   if h : i < a.size then
-    let idx : Fin a.size := ⟨i, h⟩
+    let v                := a[i]
-    let v                := a.get idx
     -- Replace a[i] by `box(0)`.  This ensures that `v` remains unshared if possible.
     -- Note: we assume that arrays have a uniform representation irrespective
     -- of the element type, and that it is valid to store `box(0)` in any array.
-    let a'               := a.set idx (unsafeCast ())
+    let a'               := a.set i (unsafeCast ())
     let v ← f v
-    pure <| a'.set idx v (Nat.lt_of_lt_of_eq h (size_set a ..).symm)
+    pure <| a'.set i v (Nat.lt_of_lt_of_eq h (size_set a ..).symm)
   else
     pure a
 
 @[implemented_by modifyMUnsafe]
 def modifyM [Monad m] (a : Array α) (i : Nat) (f : α → m α) : m (Array α) := do
   if h : i < a.size then
-    let idx := ⟨i, h⟩
+    let v   := a[i]
-    let v   := a.get idx
     let v ← f v
-    pure <| a.set idx v
+    pure <| a.set i v
   else
     pure a
 
@@ -455,7 +454,7 @@ def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
         rw [← inv, Nat.add_assoc, Nat.add_comm 1 j, Nat.add_comm]
         apply Nat.le_add_right
       have : i + (j + 1) = as.size := by rw [← inv, Nat.add_comm j 1, Nat.add_assoc]
-      map i (j+1) this (bs.push (← f ⟨j, j_lt⟩ (as.get ⟨j, j_lt⟩)))
+      map i (j+1) this (bs.push (← f ⟨j, j_lt⟩ (as.get j j_lt)))
   map as.size 0 rfl (mkEmpty as.size)
 
 @[inline]
@@ -618,8 +617,7 @@ def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
 @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size) :=
   if h : i < a.size then
-    let idx : Fin a.size := ⟨i, h⟩;
+    if a[i] == v then some ⟨i, h⟩
-    if a.get idx == v then some idx
     else indexOfAux a v (i+1)
   else none
 decreasing_by simp_wf; decreasing_trivial_pre_omega
@@ -744,7 +742,7 @@ where
 @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def popWhile (p : α → Bool) (as : Array α) : Array α :=
   if h : as.size > 0 then
-    if p (as.get ⟨as.size - 1, Nat.sub_lt h (by decide)⟩) then
+    if p (as[as.size - 1]'(Nat.sub_lt h (by decide))) then
       popWhile p as.pop
     else
       as
@@ -756,7 +754,7 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
   let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
   go (i : Nat) (r : Array α) : Array α :=
     if h : i < as.size then
-      let a := as.get ⟨i, h⟩
+      let a := as[i]
       if p a then
         go (i+1) (r.push a)
       else

src/Init/Data/Array/Lemmas.lean

@@ -450,7 +450,7 @@ theorem size_uset (a : Array α) (v i h) : (uset a i v h).size = a.size := by si
 
 /-! # get -/
 
-@[simp] theorem get_eq_getElem (a : Array α) (i : Fin _) : a.get i = a[i.1] := rfl
+@[simp] theorem get_eq_getElem (a : Array α) (i : Nat) (h) : a.get i h = a[i] := rfl
 
 theorem getElem?_lt
     (a : Array α) {i : Nat} (h : i < a.size) : a[i]? = some a[i] := dif_pos h
@@ -730,11 +730,11 @@ theorem set_set (a : Array α) (i : Nat) (h) (v v' : α) :
 private theorem fin_cast_val (e : n = n') (i : Fin n) : e ▸ i = ⟨i.1, e ▸ i.2⟩ := by cases e; rfl
 
 theorem swap_def (a : Array α) (i j : Fin a.size) :
-    a.swap i j = (a.set i (a.get j)).set j (a.get i) := by
+    a.swap i j = (a.set i a[j]).set j a[i] := by
   simp [swap, fin_cast_val]
 
 @[simp] theorem toList_swap (a : Array α) (i j : Fin a.size) :
-    (a.swap i j).toList = (a.toList.set i (a.get j)).set j (a.get i) := by simp [swap_def]
+    (a.swap i j).toList = (a.toList.set i a[j]).set j a[i] := by simp [swap_def]
 
 theorem getElem?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)[k]? =
     if j = k then some a[i.1] else if i = k then some a[j.1] else a[k]? := by
@@ -2037,8 +2037,8 @@ abbrev mapM_eq_mapM_data := @mapM_eq_mapM_toList
 
 @[deprecated getElem_modify (since := "2024-08-08")]
 theorem get_modify {arr : Array α} {x i} (h : i < (arr.modify x f).size) :
-    (arr.modify x f).get ⟨i, h⟩ =
+    (arr.modify x f).get i h =
-    if x = i then f (arr.get ⟨i, by simpa using h⟩) else arr.get ⟨i, by simpa using h⟩ := by
+    if x = i then f (arr.get i (by simpa using h)) else arr.get i (by simpa using h) := by
   simp [getElem_modify h]
 
 @[deprecated toList_filter (since := "2024-09-09")]

src/Init/Data/Array/Mem.lean

@@ -14,12 +14,12 @@ theorem sizeOf_lt_of_mem [SizeOf α] {as : Array α} (h : a ∈ as) : sizeOf a <
   cases as with | _ as =>
   exact Nat.lt_trans (List.sizeOf_lt_of_mem h.val) (by simp_arith)
 
-theorem sizeOf_get [SizeOf α] (as : Array α) (i : Fin as.size) : sizeOf (as.get i) < sizeOf as := by
+theorem sizeOf_get [SizeOf α] (as : Array α) (i : Nat) (h : i < as.size) : sizeOf (as.get i h) < sizeOf as := by
   cases as with | _ as =>
-  exact Nat.lt_trans (List.sizeOf_get ..) (by simp_arith)
+  simpa using Nat.lt_trans (List.sizeOf_get _ ⟨i, h⟩) (by simp_arith)
 
 @[simp] theorem sizeOf_getElem [SizeOf α] (as : Array α) (i : Nat) (h : i < as.size) :
-  sizeOf (as[i]'h) < sizeOf as := sizeOf_get _ _
+  sizeOf (as[i]'h) < sizeOf as := sizeOf_get _ _ h
 
 /-- This tactic, added to the `decreasing_trivial` toolbox, proves that
 `sizeOf arr[i] < sizeOf arr`, which is useful for well founded recursions

src/Init/Data/Array/Subarray.lean

@@ -48,7 +48,7 @@ instance : GetElem (Subarray α) Nat α fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
 @[inline] def getD (s : Subarray α) (i : Nat) (v₀ : α) : α :=
-  if h : i < s.size then s.get ⟨i, h⟩ else v₀
+  if h : i < s.size then s[i] else v₀
 
 abbrev get! [Inhabited α] (s : Subarray α) (i : Nat) : α :=
   getD s i default

src/Init/Data/BitVec/Bitblast.lean

@@ -76,7 +76,7 @@ to prove the correctness of the circuit that is built by `bv_decide`.
 def blastMul (aig : AIG BVBit) (input : AIG.BinaryRefVec aig w) : AIG.RefVecEntry BVBit w
 theorem denote_blastMul (aig : AIG BVBit) (lhs rhs : BitVec w) (assign : Assignment) :
    ...
-   ⟦(blastMul aig input).aig, (blastMul aig input).vec.get idx hidx, assign.toAIGAssignment⟧
+   ⟦(blastMul aig input).aig, (blastMul aig input).vec[idx], assign.toAIGAssignment⟧
      =
    (lhs * rhs).getLsbD idx
 ```

src/Init/Data/ByteArray/Basic.lean

@@ -42,7 +42,7 @@ def usize (a : @& ByteArray) : USize :=
   a.size.toUSize
 
 @[extern "lean_byte_array_uget"]
-def uget : (a : @& ByteArray) → (i : USize) → i.toNat < a.size → UInt8
+def uget : (a : @& ByteArray) → (i : USize) → (h : i.toNat < a.size := by get_elem_tactic) → UInt8
   | ⟨bs⟩, i, h => bs[i]
 
 @[extern "lean_byte_array_get"]
@@ -50,11 +50,11 @@ def get! : (@& ByteArray) → (@& Nat) → UInt8
   | ⟨bs⟩, i => bs.get! i
 
 @[extern "lean_byte_array_fget"]
-def get : (a : @& ByteArray) → (@& Fin a.size) → UInt8
+def get : (a : @& ByteArray) → (i : @& Nat) → (h : i < a.size := by get_elem_tactic) → UInt8
-  | ⟨bs⟩, i => bs.get i
+  | ⟨bs⟩, i, _ => bs[i]
 
 instance : GetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
-  getElem xs i h := xs.get ⟨i, h⟩
+  getElem xs i h := xs.get i
 
 instance : GetElem ByteArray USize UInt8 fun xs i => i.val < xs.size where
   getElem xs i h := xs.uget i h
@@ -64,11 +64,11 @@ def set! : ByteArray → (@& Nat) → UInt8 → ByteArray
   | ⟨bs⟩, i, b => ⟨bs.set! i b⟩
 
 @[extern "lean_byte_array_fset"]
-def set : (a : ByteArray) → (@& Fin a.size) → UInt8 → ByteArray
+def set : (a : ByteArray) → (i : @& Nat) → UInt8 → (h : i < a.size := by get_elem_tactic) → ByteArray
-  | ⟨bs⟩, i, b => ⟨bs.set i.1 b i.2⟩
+  | ⟨bs⟩, i, b, h => ⟨bs.set i b h⟩
 
 @[extern "lean_byte_array_uset"]
-def uset : (a : ByteArray) → (i : USize) → UInt8 → i.toNat < a.size → ByteArray
+def uset : (a : ByteArray) → (i : USize) → UInt8 → (h : i.toNat < a.size := by get_elem_tactic) → ByteArray
   | ⟨bs⟩, i, v, h => ⟨bs.uset i v h⟩
 
 @[extern "lean_byte_array_hash"]
@@ -144,7 +144,7 @@ protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteAr
       have h' : i < as.size            := Nat.lt_of_lt_of_le (Nat.lt_succ_self i) h
       have : as.size - 1 < as.size     := Nat.sub_lt (Nat.zero_lt_of_lt h') (by decide)
       have : as.size - 1 - i < as.size := Nat.lt_of_le_of_lt (Nat.sub_le (as.size - 1) i) this
-      match (← f (as.get ⟨as.size - 1 - i, this⟩) b) with
+      match (← f as[as.size - 1 - i] b) with
       | ForInStep.done b  => pure b
       | ForInStep.yield b => loop i (Nat.le_of_lt h') b
   loop as.size (Nat.le_refl _) b
@@ -178,7 +178,7 @@ def foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 →
         match i with
         | 0    => pure b
         | i'+1 =>
-          loop i' (j+1) (← f b (as.get ⟨j, Nat.lt_of_lt_of_le hlt h⟩))
+          loop i' (j+1) (← f b as[j])
       else
         pure b
     loop (stop - start) start init

src/Init/Data/FloatArray/Basic.lean

@@ -46,8 +46,8 @@ def uget : (a : @& FloatArray) → (i : USize) → i.toNat < a.size → Float
   | ⟨ds⟩, i, h => ds[i]
 
 @[extern "lean_float_array_fget"]
-def get : (ds : @& FloatArray) → (@& Fin ds.size) → Float
+def get : (ds : @& FloatArray) → (i : @& Nat) → (h : i < ds.size := by get_elem_tactic) → Float
-  | ⟨ds⟩, i => ds.get i
+  | ⟨ds⟩, i, h => ds.get i h
 
 @[extern "lean_float_array_get"]
 def get! : (@& FloatArray) → (@& Nat) → Float
@@ -55,23 +55,23 @@ def get! : (@& FloatArray) → (@& Nat) → Float
 
 def get? (ds : FloatArray) (i : Nat) : Option Float :=
   if h : i < ds.size then
-    ds.get ⟨i, h⟩
+    some (ds.get i h)
   else
     none
 
 instance : GetElem FloatArray Nat Float fun xs i => i < xs.size where
-  getElem xs i h := xs.get ⟨i, h⟩
+  getElem xs i h := xs.get i h
 
 instance : GetElem FloatArray USize Float fun xs i => i.val < xs.size where
   getElem xs i h := xs.uget i h
 
 @[extern "lean_float_array_uset"]
-def uset : (a : FloatArray) → (i : USize) → Float → i.toNat < a.size → FloatArray
+def uset : (a : FloatArray) → (i : USize) → Float → (h : i.toNat < a.size := by get_elem_tactic) → FloatArray
   | ⟨ds⟩, i, v, h => ⟨ds.uset i v h⟩
 
 @[extern "lean_float_array_fset"]
-def set : (ds : FloatArray) → (@& Fin ds.size) → Float → FloatArray
+def set : (ds : FloatArray) → (i : @& Nat) → Float → (h : i < ds.size := by get_elem_tactic) → FloatArray
-  | ⟨ds⟩, i, d => ⟨ds.set i.1 d i.2⟩
+  | ⟨ds⟩, i, d, h => ⟨ds.set i d h⟩
 
 @[extern "lean_float_array_set"]
 def set! : FloatArray → (@& Nat) → Float → FloatArray
@@ -83,7 +83,7 @@ def isEmpty (s : FloatArray) : Bool :=
 partial def toList (ds : FloatArray) : List Float :=
   let rec loop (i r) :=
     if h : i < ds.size then
-      loop (i+1) (ds.get ⟨i, h⟩ :: r)
+      loop (i+1) (ds[i] :: r)
     else
       r.reverse
   loop 0 []
@@ -115,7 +115,7 @@ protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : FloatA
       have h' : i < as.size            := Nat.lt_of_lt_of_le (Nat.lt_succ_self i) h
       have : as.size - 1 < as.size     := Nat.sub_lt (Nat.zero_lt_of_lt h') (by decide)
       have : as.size - 1 - i < as.size := Nat.lt_of_le_of_lt (Nat.sub_le (as.size - 1) i) this
-      match (← f (as.get ⟨as.size - 1 - i, this⟩) b) with
+      match (← f as[as.size - 1 - i] b) with
       | ForInStep.done b  => pure b
       | ForInStep.yield b => loop i (Nat.le_of_lt h') b
   loop as.size (Nat.le_refl _) b
@@ -149,7 +149,7 @@ def foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → Float →
         match i with
         | 0    => pure b
         | i'+1 =>
-          loop i' (j+1) (← f b (as.get ⟨j, Nat.lt_of_lt_of_le hlt h⟩))
+          loop i' (j+1) (← f b (as[j]'(Nat.lt_of_lt_of_le hlt h)))
       else
         pure b
     loop (stop - start) start init

src/Init/Data/Repr.lean

@@ -162,7 +162,7 @@ private def reprArray : Array String := Id.run do
   List.range 128 |>.map (·.toUSize.repr) |> Array.mk
 
 private def reprFast (n : Nat) : String :=
-  if h : n < 128 then Nat.reprArray.get ⟨n, h⟩ else
+  if h : n < 128 then Nat.reprArray.get n h else
   if h : n < USize.size then (USize.ofNatCore n h).repr
   else (toDigits 10 n).asString
 

src/Init/Data/Stream.lean

@@ -94,7 +94,7 @@ instance : Stream (Subarray α) α where
   next? s :=
     if h : s.start < s.stop then
       have : s.start + 1 ≤ s.stop := Nat.succ_le_of_lt h
-      some (s.array.get ⟨s.start, Nat.lt_of_lt_of_le h s.stop_le_array_size⟩,
+      some (s.array[s.start]'(Nat.lt_of_lt_of_le h s.stop_le_array_size),
         { s with start := s.start + 1, start_le_stop := this })
     else
       none

src/Init/Data/String/Extra.lean

@@ -134,7 +134,7 @@ def toUTF8 (a : @& String) : ByteArray :=
 /-- Accesses a byte in the UTF-8 encoding of the `String`. O(1) -/
 @[extern "lean_string_get_byte_fast"]
 def getUtf8Byte (s : @& String) (n : Nat) (h : n < s.utf8ByteSize) : UInt8 :=
-  (toUTF8 s).get ⟨n, size_toUTF8 _ ▸ h⟩
+  (toUTF8 s)[n]'(size_toUTF8 _ ▸ h)
 
 theorem Iterator.sizeOf_next_lt_of_hasNext (i : String.Iterator) (h : i.hasNext) : sizeOf i.next < sizeOf i := by
   cases i; rename_i s pos; simp [Iterator.next, Iterator.sizeOf_eq]; simp [Iterator.hasNext] at h

src/Init/GetElem.lean

@@ -224,7 +224,7 @@ end List
 namespace Array
 
 instance : GetElem (Array α) Nat α fun xs i => i < xs.size where
-  getElem xs i h := xs.get ⟨i, h⟩
+  getElem xs i h := xs.get i h
 
 end Array
 

src/Init/Prelude.lean

@@ -938,8 +938,8 @@ and `e` can depend on `h : ¬c`. (Both branches use the same name for the hypoth
 even though it has different types in the two cases.)
 
 We use this to be able to communicate the if-then-else condition to the branches.
-For example, `Array.get arr ⟨i, h⟩` expects a proof `h : i < arr.size` in order to
+For example, `Array.get arr i h` expects a proof `h : i < arr.size` in order to
-avoid a bounds check, so you can write `if h : i < arr.size then arr.get ⟨i, h⟩ else ...`
+avoid a bounds check, so you can write `if h : i < arr.size then arr.get i h else ...`
 to avoid the bounds check inside the if branch. (Of course in this case we have only
 lifted the check into an explicit `if`, but we could also use this proof multiple times
 or derive `i < arr.size` from some other proposition that we are checking in the `if`.)
@@ -2630,14 +2630,21 @@ def Array.empty {α : Type u} : Array α := mkEmpty 0
 def Array.size {α : Type u} (a : @& Array α) : Nat :=
  a.toList.length
 
-/-- Access an element from an array without bounds checks, using a `Fin` index. -/
+/--
+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.
+-/
 @[extern "lean_array_fget"]
-def Array.get {α : Type u} (a : @& Array α) (i : @& Fin a.size) : α :=
+def Array.get {α : Type u} (a : @& Array α) (i : @& Nat) (h : LT.lt i a.size) : α :=
-  a.toList.get i
+  a.toList.get ⟨i, h⟩
 
 /-- Access an element from an array, or return `v₀` if the index is out of bounds. -/
 @[inline] abbrev Array.getD (a : Array α) (i : Nat) (v₀ : α) : α :=
-  dite (LT.lt i a.size) (fun h => a.get ⟨i, h⟩) (fun _ => 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. -/
 @[extern "lean_array_get"]
@@ -2695,7 +2702,7 @@ protected def Array.appendCore {α : Type u}  (as : Array α) (bs : Array α) :
       (fun hlt =>
         match i with
         | 0           => as
-        | Nat.succ i' => loop i' (hAdd j 1) (as.push (bs.get ⟨j, hlt⟩)))
+        | Nat.succ i' => loop i' (hAdd j 1) (as.push (bs.get j hlt)))
       (fun _ => as)
   loop bs.size 0 as
 
@@ -2710,7 +2717,7 @@ def Array.extract (as : Array α) (start stop : Nat) : Array α :=
       (fun hlt =>
         match i with
         | 0           => bs
-        | Nat.succ i' => loop i' (hAdd j 1) (bs.push (as.get ⟨j, hlt⟩)))
+        | Nat.succ i' => loop i' (hAdd j 1) (bs.push (as.get j hlt)))
       (fun _ => bs)
   let sz' := Nat.sub (min stop as.size) start
   loop sz' start (mkEmpty sz')
@@ -2829,7 +2836,7 @@ def Array.sequenceMap {α : Type u} {β : Type v} {m : Type v → Type w} [Monad
       (fun hlt =>
         match i with
         | 0           => pure bs
-        | Nat.succ i' => Bind.bind (f (as.get ⟨j, hlt⟩)) fun b => loop i' (hAdd j 1) (bs.push b))
+        | Nat.succ i' => Bind.bind (f (as.get j hlt)) fun b => loop i' (hAdd j 1) (bs.push b))
       (fun _ => pure bs)
   loop as.size 0 (Array.mkEmpty as.size)
 

src/Lean/Compiler/IR/Checker.lean

@@ -135,8 +135,8 @@ def checkExpr (ty : IRType) : Expr → M Unit
     match xType with
     | IRType.object       => checkObjType ty
     | IRType.tobject      => checkObjType ty
-    | IRType.struct _ tys => if h : i < tys.size then checkEqTypes (tys.get ⟨i,h⟩) ty else throw "invalid proj index"
+    | IRType.struct _ tys => if h : i < tys.size then checkEqTypes (tys[i]) ty else throw "invalid proj index"
-    | IRType.union _ tys  => if h : i < tys.size then checkEqTypes (tys.get ⟨i,h⟩) ty else throw "invalid proj index"
+    | IRType.union _ tys  => if h : i < tys.size then checkEqTypes (tys[i]) ty else throw "invalid proj index"
     | _                   => throw s!"unexpected IR type '{xType}'"
   | Expr.uproj _ x          => checkObjVar x *> checkType ty (fun t => t == IRType.usize)
   | Expr.sproj _ _ x        => checkObjVar x *> checkScalarType ty

src/Lean/Data/HashMap.lean

@@ -90,10 +90,9 @@ def contains [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Bool :=
 
 def moveEntries [Hashable α] (i : Nat) (source : Array (AssocList α β)) (target : HashMapBucket α β) : HashMapBucket α β :=
   if h : i < source.size then
-     let idx : Fin source.size := ⟨i, h⟩
+     let es  : AssocList α β   := source[i]
-     let es  : AssocList α β   := source.get idx
      -- We remove `es` from `source` to make sure we can reuse its memory cells when performing es.foldl
-     let source                := source.set idx AssocList.nil
+     let source                := source.set i AssocList.nil
      let target                := es.foldl (reinsertAux hash) target
      moveEntries (i+1) source target
   else target

src/Lean/Data/HashSet.lean

@@ -80,10 +80,9 @@ def contains [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : Bool :=
 
 def moveEntries [Hashable α] (i : Nat) (source : Array (List α)) (target : HashSetBucket α) : HashSetBucket α :=
   if h : i < source.size then
-     let idx : Fin source.size := ⟨i, h⟩
+     let es  : List α   := source[i]
-     let es  : List α   := source.get idx
      -- We remove `es` from `source` to make sure we can reuse its memory cells when performing es.foldl
-     let source                := source.set idx []
+     let source                := source.set i []
      let target                := es.foldl (reinsertAux hash) target
      moveEntries (i+1) source target
   else

src/Lean/Data/Lsp/Utf16.lean

@@ -66,7 +66,7 @@ namespace FileMap
 
 private def lineStartPos (text : FileMap) (line : Nat) : String.Pos :=
   if h : line < text.positions.size then
-    text.positions.get ⟨line, h⟩
+    text.positions[line]
   else if text.positions.isEmpty then
     0
   else

src/Lean/Data/PersistentArray.lean

@@ -149,8 +149,8 @@ private def emptyArray {α : Type u} : Array (PersistentArrayNode α) :=
 partial def popLeaf : PersistentArrayNode α → Option (Array α) × Array (PersistentArrayNode α)
   | node cs =>
     if h : cs.size ≠ 0 then
-      let idx : Fin cs.size := ⟨cs.size - 1, by exact Nat.pred_lt h⟩
+      let idx := cs.size - 1
-      let last := cs.get idx
+      let last := cs[idx]
       let cs'  := cs.set idx default
       match popLeaf last with
       | (none,   _)       => (none, emptyArray)

src/Lean/Data/PersistentHashMap.lean

@@ -84,11 +84,10 @@ private theorem size_push {ks : Array α} {vs : Array β} (h : ks.size = vs.size
 partial def insertAtCollisionNodeAux [BEq α] : CollisionNode α β → Nat → α → β → CollisionNode α β
   | n@⟨Node.collision keys vals heq, _⟩, i, k, v =>
     if h : i < keys.size then
-      let idx : Fin keys.size := ⟨i, h⟩;
+      let k' := keys[i];
-      let k' := keys.get idx;
       if k == k' then
          let j : Fin vals.size := ⟨i, by rw [←heq]; assumption⟩
-         ⟨Node.collision (keys.set idx k) (vals.set j v) (size_set heq idx j k v), IsCollisionNode.mk _ _ _⟩
+         ⟨Node.collision (keys.set i k) (vals.set j v) (size_set heq ⟨i, h⟩ j k v), IsCollisionNode.mk _ _ _⟩
       else insertAtCollisionNodeAux n (i+1) k v
     else
       ⟨Node.collision (keys.push k) (vals.push v) (size_push heq k v), IsCollisionNode.mk _ _ _⟩

src/Lean/Data/Position.lean

@@ -97,7 +97,7 @@ partial def toPosition (fmap : FileMap) (pos : String.Pos) : Position :=
 def ofPosition (text : FileMap) (pos : Position) : String.Pos :=
   let colPos :=
     if h : pos.line - 1 < text.positions.size then
-      text.positions.get ⟨pos.line - 1, h⟩
+      text.positions[pos.line - 1]
     else if text.positions.isEmpty then
       0
     else
@@ -110,7 +110,7 @@ This gives the same result as `map.ofPosition ⟨line, 0⟩`, but is more effici
 -/
 def lineStart (map : FileMap) (line : Nat) : String.Pos :=
   if h : line - 1 < map.positions.size then
-    map.positions.get ⟨line - 1, h⟩
+    map.positions[line - 1]
   else map.positions.back?.getD 0
 
 end FileMap

src/Lean/Elab/App.lean

@@ -506,8 +506,7 @@ where
     if h : i < args.size then
       match (← whnf cType) with
       | .forallE _ d b _ =>
-        let arg := args.get ⟨i, h⟩
+        if args[i] == x && d.isOutParam then
-        if arg == x && d.isOutParam then
           return true
         isOutParamOf x (i+1) args b
       | _ => return false

src/Lean/Elab/BuiltinCommand.lean

@@ -111,9 +111,8 @@ private def checkEndHeader : Name → List Scope → Option Name
 
 private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM Unit :=
   if h : i < cmds.size then
-    let cmd := cmds.get ⟨i, h⟩;
     catchInternalId unsupportedSyntaxExceptionId
-      (elabCommand cmd)
+      (elabCommand cmds[i])
       (fun _ => elabChoiceAux cmds (i+1))
   else
     throwUnsupportedSyntax

src/Lean/Elab/Declaration.lean

@@ -192,8 +192,7 @@ private def isMutualPreambleCommand (stx : Syntax) : Bool :=
 private partial def splitMutualPreamble (elems : Array Syntax) : Option (Array Syntax × Array Syntax) :=
   let rec loop (i : Nat) : Option (Array Syntax × Array Syntax) :=
     if h : i < elems.size then
-      let elem := elems.get ⟨i, h⟩
+      if isMutualPreambleCommand elems[i] then
-      if isMutualPreambleCommand elem then
         loop (i+1)
       else if i == 0 then
         none -- `mutual` block does not contain any preamble commands

src/Lean/Elab/Inductive.lean

@@ -133,7 +133,7 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Term
 private partial def elabHeaderAux (views : Array InductiveView) (i : Nat) (acc : Array ElabHeaderResult) : TermElabM (Array ElabHeaderResult) :=
   Term.withAutoBoundImplicitForbiddenPred (fun n => views.any (·.shortDeclName == n)) do
     if h : i < views.size then
-      let view := views.get ⟨i, h⟩
+      let view := views[i]
       let acc ← Term.withAutoBoundImplicit <| Term.elabBinders view.binders.getArgs fun params => do
         match view.type? with
         | none         =>
@@ -250,7 +250,7 @@ private partial def withInductiveLocalDecls (rs : Array ElabHeaderResult) (x : A
   withLCtx r0.lctx r0.localInsts <| withRef r0.view.ref do
     let rec loop (i : Nat) (indFVars : Array Expr) := do
       if h : i < namesAndTypes.size then
-        let (declName, shortDeclName, type) := namesAndTypes.get ⟨i, h⟩
+        let (declName, shortDeclName, type) := namesAndTypes[i]
         Term.withAuxDecl shortDeclName type declName fun indFVar => loop (i+1) (indFVars.push indFVar)
       else
         x params indFVars

src/Lean/Elab/LetRec.lean

@@ -77,7 +77,7 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
 private partial def withAuxLocalDecls {α} (views : Array LetRecDeclView) (k : Array Expr → TermElabM α) : TermElabM α :=
   let rec loop (i : Nat) (fvars : Array Expr) : TermElabM α :=
     if h : i < views.size then
-      let view := views.get ⟨i, h⟩
+      let view := views[i]
       withAuxDecl view.shortDeclName view.type view.declName fun fvar => loop (i+1) (fvars.push fvar)
     else
       k fvars

src/Lean/Elab/Match.lean

@@ -108,7 +108,7 @@ where
   /-- Elaborate discriminants inferring the match-type -/
   elabDiscrs (i : Nat) (discrs : Array Discr) : TermElabM ElabMatchTypeAndDiscrsResult := do
     if h : i < discrStxs.size then
-      let discrStx := discrStxs.get ⟨i, h⟩
+      let discrStx := discrStxs[i]
       let discr     ← elabAtomicDiscr discrStx
       let discr     ← instantiateMVars discr
       let userName ← mkUserNameFor discr
@@ -176,9 +176,8 @@ structure PatternVarDecl where
 private partial def withPatternVars {α} (pVars : Array PatternVar) (k : Array PatternVarDecl → TermElabM α) : TermElabM α :=
   let rec loop (i : Nat) (decls : Array PatternVarDecl) (userNames : Array Name) := do
     if h : i < pVars.size then
-      let var := pVars.get ⟨i, h⟩
       let type ← mkFreshTypeMVar
-      withLocalDecl var.getId BinderInfo.default type fun x =>
+      withLocalDecl pVars[i].getId BinderInfo.default type fun x =>
         loop (i+1) (decls.push { fvarId := x.fvarId! }) (userNames.push Name.anonymous)
     else
       k decls
@@ -760,7 +759,7 @@ where
     | [] => k eqs
     | p::ps =>
       if h : i < discrs.size then
-        let discr := discrs.get ⟨i, h⟩
+        let discr := discrs[i]
         if let some h := discr.h? then
           withLocalDeclD h.getId (← mkEqHEq discr.expr (← p.toExpr)) fun eq => do
             addTermInfo' h eq (isBinder := true)

src/Lean/Elab/MutualDef.lean

@@ -77,7 +77,7 @@ private def check (prevHeaders : Array DefViewElabHeader) (newHeader : DefViewEl
   if newHeader.modifiers.isPartial && newHeader.modifiers.isUnsafe then
     throwError "'unsafe' subsumes 'partial'"
   if h : 0 < prevHeaders.size then
-    let firstHeader := prevHeaders.get ⟨0, h⟩
+    let firstHeader := prevHeaders[0]
     try
       unless newHeader.levelNames == firstHeader.levelNames do
         throwError "universe parameters mismatch"
@@ -273,7 +273,7 @@ where
 private partial def withFunLocalDecls {α} (headers : Array DefViewElabHeader) (k : Array Expr → TermElabM α) : TermElabM α :=
   let rec loop (i : Nat) (fvars : Array Expr) := do
     if h : i < headers.size then
-      let header := headers.get ⟨i, h⟩
+      let header := headers[i]
       if header.modifiers.isNonrec then
         loop (i+1) fvars
       else
@@ -936,7 +936,7 @@ end MutualClosure
 private def getAllUserLevelNames (headers : Array DefViewElabHeader) : List Name :=
   if h : 0 < headers.size then
     -- Recall that all top-level functions must have the same levels. See `check` method above
-    (headers.get ⟨0, h⟩).levelNames
+    headers[0].levelNames
   else
     []
 

src/Lean/Elab/PatternVar.lean

@@ -135,7 +135,7 @@ private def isNextArgAccessible (ctx : Context) : Bool :=
   | none =>
     if h : i < ctx.paramDecls.size then
       -- For `[match_pattern]` applications, only explicit parameters are accessible.
-      let d := ctx.paramDecls.get ⟨i, h⟩
+      let d := ctx.paramDecls[i]
       d.2.isExplicit
     else
       false

src/Lean/Elab/StructInst.lean

@@ -885,7 +885,7 @@ partial def tryToSynthesizeDefault (structs : Array Struct) (allStructNames : Ar
     if dist > maxDistance then
       return false
     else if h : i < structs.size then
-      let struct := structs.get ⟨i, h⟩
+      let struct := structs[i]
       match getDefaultFnForField? (← getEnv) struct.structName fieldName with
       | some defFn =>
         let cinfo ← getConstInfo defFn

src/Lean/Elab/Structure.lean

@@ -321,7 +321,7 @@ private partial def processSubfields (structDeclName : Name) (parentFVar : Expr)
 where
   go (i : Nat) (infos : Array StructFieldInfo) := do
     if h : i < subfieldNames.size then
-      let subfieldName := subfieldNames.get ⟨i, h⟩
+      let subfieldName := subfieldNames[i]
       if containsFieldName infos subfieldName then
         throwError "field '{subfieldName}' from '{.ofConstName parentStructName}' has already been declared"
       let val  ← mkProjection parentFVar subfieldName
@@ -463,7 +463,7 @@ where
     let fieldNames := getStructureFields (← getEnv) parentStructName
     let rec copy (i : Nat) (infos : Array StructFieldInfo) (fieldMap : FieldMap) (expandedStructNames : NameSet) : TermElabM α := do
       if h : i < fieldNames.size then
-        let fieldName := fieldNames.get ⟨i, h⟩
+        let fieldName := fieldNames[i]
         let fieldType ← getFieldType infos parentType fieldName
         match findFieldInfo? infos fieldName with
         | some existingFieldInfo =>

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -308,7 +308,7 @@ def evalTacticSeq : Tactic :=
 
 partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit :=
   if h : i < tactics.size then
-    let tactic := tactics.get ⟨i, h⟩
+    let tactic := tactics[i]
     catchInternalId unsupportedSyntaxExceptionId
       (evalTactic tactic)
       (fun _ => evalChoiceAux tactics (i+1))

src/Lean/Elab/Tactic/RCases.lean

@@ -526,7 +526,7 @@ where
   /-- Runs `rintroContinue` on `pats[i:]` -/
   loop i g fs clears a := do
     if h : i < pats.size then
-      rintroCore g fs clears a ref (pats.get ⟨i, h⟩) ty? (loop (i+1))
+      rintroCore g fs clears a ref pats[i] ty? (loop (i+1))
     else cont g fs clears a
 
 end

src/Lean/Environment.lean

@@ -345,7 +345,7 @@ unsafe def setState {σ} (ext : Ext σ) (exts : Array EnvExtensionState) (s : σ
 
 unsafe def getState {σ} [Inhabited σ] (ext : Ext σ) (exts : Array EnvExtensionState) : σ :=
   if h : ext.idx < exts.size then
-    let s : EnvExtensionState := exts.get ⟨ext.idx, h⟩
+    let s : EnvExtensionState := exts[ext.idx]
     unsafeCast s
   else
     panic! invalidExtMsg

src/Lean/InternalExceptionId.lean

@@ -37,7 +37,7 @@ def InternalExceptionId.getName (id : InternalExceptionId) : IO Name :=  do
   let exs ← internalExceptionsRef.get
   let i := id.idx;
   if h : i < exs.size then
-    return exs.get ⟨i, h⟩
+    return exs[i]
   else
     throw <| IO.userError "invalid internal exception id"
 

src/Lean/Level.lean

@@ -320,7 +320,7 @@ private def accMax (result : Level) (prev : Level) (offset : Nat) : Level :=
  -/
 private partial def mkMaxAux (lvls : Array Level) (extraK : Nat) (i : Nat) (prev : Level) (prevK : Nat) (result : Level) : Level :=
   if h : i < lvls.size then
-    let lvl   := lvls.get ⟨i, h⟩
+    let lvl   := lvls[i]
     let curr  := lvl.getLevelOffset
     let currK := lvl.getOffset
     if curr == prev then
@@ -335,7 +335,7 @@ private partial def mkMaxAux (lvls : Array Level) (extraK : Nat) (i : Nat) (prev
   It finds the first position that is not an explicit universe. -/
 private partial def skipExplicit (lvls : Array Level) (i : Nat) : Nat :=
   if h : i < lvls.size then
-    let lvl := lvls.get ⟨i, h⟩
+    let lvl := lvls[i]
     if lvl.getLevelOffset.isZero then skipExplicit lvls (i+1) else i
   else
     i
@@ -349,7 +349,7 @@ It assumes `lvls` has been sorted using `normLt`.
 -/
 private partial def isExplicitSubsumedAux (lvls : Array Level) (maxExplicit : Nat) (i : Nat) : Bool :=
   if h : i < lvls.size then
-    let lvl := lvls.get ⟨i, h⟩
+    let lvl := lvls[i]
     if lvl.getOffset ≥ maxExplicit then true
     else isExplicitSubsumedAux lvls maxExplicit (i+1)
   else

src/Lean/Message.lean

@@ -250,7 +250,7 @@ instance : Coe (Option Expr) MessageData := ⟨fun o => match o with | none => "
 
 partial def arrayExpr.toMessageData (es : Array Expr) (i : Nat) (acc : MessageData) : MessageData :=
   if h : i < es.size then
-    let e   := es.get ⟨i, h⟩;
+    let e   := es[i];
     let acc := if i == 0 then acc ++ ofExpr e else acc ++ ", " ++ ofExpr e;
     toMessageData es (i+1) acc
   else

src/Lean/Meta/AppBuilder.lean

@@ -352,7 +352,7 @@ private partial def mkAppOptMAux (f : Expr) (xs : Array (Option Expr)) : Nat →
   | i, args, j, instMVars, Expr.forallE n d b bi => do
     let d  := d.instantiateRevRange j args.size args
     if h : i < xs.size then
-      match xs.get ⟨i, h⟩ with
+      match xs[i] with
       | none =>
         match bi with
         | BinderInfo.instImplicit => do

src/Lean/Meta/Basic.lean

@@ -1081,7 +1081,7 @@ mutual
   private partial def withNewLocalInstancesImp
       (fvars : Array Expr) (i : Nat) (k : MetaM α) : MetaM α := do
     if h : i < fvars.size then
-      let fvar := fvars.get ⟨i, h⟩
+      let fvar := fvars[i]
       let decl ← getFVarLocalDecl fvar
       match (← isClassQuick? decl.type) with
       | .none   => withNewLocalInstancesImp fvars (i+1) k
@@ -1650,7 +1650,7 @@ def setInlineAttribute (declName : Name) (kind := Compiler.InlineAttributeKind.i
 
 private partial def instantiateForallAux (ps : Array Expr) (i : Nat) (e : Expr) : MetaM Expr := do
   if h : i < ps.size then
-    let p := ps.get ⟨i, h⟩
+    let p := ps[i]
     match (← whnf e) with
     | .forallE _ _ b _ => instantiateForallAux ps (i+1) (b.instantiate1 p)
     | _                => throwError "invalid instantiateForall, too many parameters"
@@ -1663,7 +1663,7 @@ def instantiateForall (e : Expr) (ps : Array Expr) : MetaM Expr :=
 
 private partial def instantiateLambdaAux (ps : Array Expr) (i : Nat) (e : Expr) : MetaM Expr := do
   if h : i < ps.size then
-    let p := ps.get ⟨i, h⟩
+    let p := ps[i]
     match (← whnf e) with
     | .lam _ _ b _ => instantiateLambdaAux ps (i+1) (b.instantiate1 p)
     | _            => throwError "invalid instantiateLambda, too many parameters"

src/Lean/Meta/Closure.lean

@@ -224,7 +224,7 @@ def collectExpr (e : Expr) : ClosureM Expr := do
 partial def pickNextToProcessAux (lctx : LocalContext) (i : Nat) (toProcess : Array ToProcessElement) (elem : ToProcessElement)
     : ToProcessElement × Array ToProcessElement :=
   if h : i < toProcess.size then
-    let elem' := toProcess.get ⟨i, h⟩
+    let elem' := toProcess[i]
     if (lctx.get! elem.fvarId).index < (lctx.get! elem'.fvarId).index then
       pickNextToProcessAux lctx (i+1) (toProcess.set i elem) elem'
     else

src/Lean/Meta/CollectFVars.lean

@@ -29,7 +29,7 @@ where
     let s ← getThe CollectFVars.State
     let i ← get
     if h : i < s.fvarIds.size then
-      let r := s.fvarIds.get ⟨i, h⟩
+      let r := s.fvarIds[i]
       modify (· + 1)
       return some r
     else

src/Lean/Meta/DiscrTree.lean

@@ -202,7 +202,7 @@ instance : Inhabited (DiscrTree α) where
 -/
 private def ignoreArg (a : Expr) (i : Nat) (infos : Array ParamInfo) : MetaM Bool := do
   if h : i < infos.size then
-    let info := infos.get ⟨i, h⟩
+    let info := infos[i]
     if info.isInstImplicit then
       return true
     else if info.isImplicit || info.isStrictImplicit then
@@ -442,7 +442,7 @@ def mkPath (e : Expr) (config : WhnfCoreConfig) (noIndexAtArgs := false) : MetaM
 
 private partial def createNodes (keys : Array Key) (v : α) (i : Nat) : Trie α :=
   if h : i < keys.size then
-    let k := keys.get ⟨i, h⟩
+    let k := keys[i]
     let c := createNodes keys v (i+1)
     .node #[] #[(k, c)]
   else
@@ -470,7 +470,7 @@ where
 private partial def insertAux [BEq α] (keys : Array Key) (v : α) : Nat → Trie α → Trie α
   | i, .node vs cs =>
     if h : i < keys.size then
-      let k := keys.get ⟨i, h⟩
+      let k := keys[i]
       let c := Id.run $ cs.binInsertM
           (fun a b => a.1 < b.1)
           (fun ⟨_, s⟩ => let c := insertAux keys v (i+1) s; (k, c)) -- merge with existing

src/Lean/Meta/ExprDefEq.lean

@@ -332,7 +332,7 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta
 @[specialize] partial def isDefEqBindingDomain (fvars : Array Expr) (ds₂ : Array Expr) (k : MetaM Bool) : MetaM Bool :=
   let rec loop (i : Nat) := do
     if h : i < fvars.size then do
-      let fvar := fvars.get ⟨i, h⟩
+      let fvar := fvars[i]
       let fvarDecl ← getFVarLocalDecl fvar
       let fvarType := fvarDecl.type
       let d₂       := ds₂[i]!
@@ -1203,7 +1203,7 @@ private partial def processAssignment (mvarApp : Expr) (v : Expr) : MetaM Bool :
       let useFOApprox (args : Array Expr) : MetaM Bool :=
         processAssignmentFOApprox mvar args v <||> processConstApprox mvar args i v
       if h : i < args.size then
-        let arg := args.get ⟨i, h⟩
+        let arg := args[i]
         let arg ← simpAssignmentArg arg
         let args := args.set i arg
         match arg with

src/Lean/Meta/GeneralizeTelescope.lean

@@ -17,7 +17,7 @@ structure Entry where
 
 partial def updateTypes (e eNew : Expr) (entries : Array Entry) (i : Nat) : MetaM (Array Entry) :=
   if h : i < entries.size then
-    let entry := entries.get ⟨i, h⟩
+    let entry := entries[i]
     match entry with
     | ⟨_, type, _⟩ => do
       let typeAbst ← kabstract type e
@@ -38,7 +38,7 @@ partial def generalizeTelescopeAux {α} (k : Array Expr → MetaM α)
       withLocalDeclD userName type fun x => do
         let entries ← updateTypes e x entries (i+1)
         generalizeTelescopeAux k entries (i+1) (fvars.push x)
-    match entries.get ⟨i, h⟩ with
+    match entries[i] with
     | ⟨e@(.fvar fvarId), type, false⟩ =>
       let localDecl ← fvarId.getDecl
       match localDecl with

src/Lean/Meta/Injective.lean

@@ -86,7 +86,7 @@ private partial def mkInjectiveTheoremTypeCore? (ctorVal : ConstructorVal) (useE
       if h : i < args1.size then
         match (← whnf type) with
         | Expr.forallE n d b _ =>
-          let arg1 := args1.get ⟨i, h⟩
+          let arg1 := args1[i]
           if occursOrInType (← getLCtx) arg1 resultType then
             mkArgs2 (i + 1) (b.instantiate1 arg1) (args2.push arg1) args2New
           else

src/Lean/Meta/LazyDiscrTree.lean

@@ -73,7 +73,7 @@ private def tmpStar := mkMVar tmpMVarId
 -/
 private def ignoreArg (a : Expr) (i : Nat) (infos : Array ParamInfo) : MetaM Bool := do
   if h : i < infos.size then
-    let info := infos.get ⟨i, h⟩
+    let info := infos[i]
     if info.isInstImplicit then
       return true
     else if info.isImplicit || info.isStrictImplicit then

src/Lean/Meta/Match/CaseArraySizes.lean

@@ -71,7 +71,7 @@ def caseArraySizes (mvarId : MVarId) (fvarId : FVarId) (sizes : Array Nat) (xNam
       let mvarId := subgoal.mvarId
       let hEqSz  := (subst.get hEq).fvarId!
       if h : i < sizes.size then
-         let n := sizes.get ⟨i, h⟩
+         let n := sizes[i]
          let mvarId ← mvarId.clear subgoal.newHs[0]!
          let mvarId ← mvarId.clear (subst.get aSizeFVarId).fvarId!
          mvarId.withContext do

src/Lean/Meta/Match/Match.lean

@@ -546,7 +546,7 @@ private def processValue (p : Problem) : MetaM (Array Problem) := do
   subgoals.mapIdxM fun i subgoal => do
     trace[Meta.Match.match] "processValue subgoal\n{MessageData.ofGoal subgoal.mvarId}"
     if h : i < values.size then
-      let value := values.get ⟨i, h⟩
+      let value := values[i]
       -- (x = value) branch
       let subst := subgoal.subst
       trace[Meta.Match.match] "processValue subst: {subst.map.toList.map fun p => mkFVar p.1}, {subst.map.toList.map fun p => p.2}"

src/Lean/Meta/Match/MatchEqs.lean

@@ -366,7 +366,7 @@ private partial def withSplitterAlts (altTypes : Array Expr) (f : Array Expr →
   let rec go (i : Nat) (xs : Array Expr) : MetaM α := do
     if h : i < altTypes.size then
       let hName := (`h).appendIndexAfter (i+1)
-      withLocalDeclD hName (altTypes.get ⟨i, h⟩) fun x =>
+      withLocalDeclD hName altTypes[i] fun x =>
         go (i+1) (xs.push x)
     else
       f xs
@@ -525,7 +525,7 @@ where
           let rec go (i : Nat) (motiveTypeArgsNew : Array Expr) : ConvertM Expr := do
             assert! motiveTypeArgsNew.size == i
             if h : i < motiveTypeArgs.size then
-              let motiveTypeArg := motiveTypeArgs.get ⟨i, h⟩
+              let motiveTypeArg := motiveTypeArgs[i]
               if i < isAlt.size && isAlt[i]! then
                 let altNew := argsNew[6+i]! -- Recall that `Eq.ndrec` has 6 arguments
                 let altTypeNew ← inferType altNew
@@ -636,8 +636,7 @@ private partial def withNewAlts (numDiscrEqs : Nat) (discrs : Array Expr) (patte
 where
   go (i : Nat) (altsNew : Array Expr) : MetaM α := do
    if h : i < alts.size then
-     let alt := alts.get ⟨i, h⟩
+     let altLocalDecl ← getFVarLocalDecl alts[i]
-     let altLocalDecl ← getFVarLocalDecl alt
      let typeNew := altLocalDecl.type.replaceFVars discrs patterns
      withLocalDecl altLocalDecl.userName altLocalDecl.binderInfo typeNew fun altNew =>
        go (i+1) (altsNew.push altNew)

src/Lean/Meta/Match/MatcherApp/Transform.lean

@@ -15,7 +15,7 @@ namespace Lean.Meta.MatcherApp
 /-- Auxiliary function for MatcherApp.addArg -/
 private partial def updateAlts (unrefinedArgType : Expr) (typeNew : Expr) (altNumParams : Array Nat) (alts : Array Expr) (refined : Bool) (i : Nat) : MetaM (Array Nat × Array Expr) := do
   if h : i < alts.size then
-    let alt       := alts.get ⟨i, h⟩
+    let alt       := alts[i]
     let numParams := altNumParams[i]!
     let typeNew ← whnfD typeNew
     match typeNew with

src/Lean/Meta/RecursorInfo.lean

@@ -89,8 +89,7 @@ private def checkMotive (declName : Name) (motive : Expr) (motiveArgs : Array Ex
    We assume a parameter is anything that occurs before the motive -/
 private partial def getNumParams (xs : Array Expr) (motive : Expr) (i : Nat) : Nat :=
   if h : i < xs.size then
-    let x := xs.get ⟨i, h⟩
+    if motive == xs[i] then i
-    if motive == x then i
     else getNumParams xs motive (i+1)
   else
     i
@@ -100,7 +99,7 @@ private def getMajorPosDepElim (declName : Name) (majorPos? : Option Nat) (xs :
   match majorPos? with
   | some majorPos =>
     if h : majorPos < xs.size then
-      let major   := xs.get ⟨majorPos, h⟩
+      let major   := xs[majorPos]
       let depElim := motiveArgs.contains major
       pure (major, majorPos, depElim)
     else throwError "invalid major premise position for user defined recursor, recursor has only {xs.size} arguments"

src/Lean/Meta/SynthInstance.lean

@@ -665,7 +665,7 @@ private partial def preprocessArgs (type : Expr) (i : Nat) (args : Array Expr) (
     let type ← whnf type
     match type with
     | .forallE _ d b _ => do
-      let arg := args.get ⟨i, h⟩
+      let arg := args[i]
       /-
       We should not simply check `d.isOutParam`. See `checkOutParam` and issue #1852.
       If an instance implicit argument depends on an `outParam`, it is treated as an `outParam` too.

src/Lean/Meta/Tactic/Induction.lean

@@ -23,7 +23,7 @@ private def addRecParams (mvarId : MVarId) (majorTypeArgs : Array Expr) : List (
   | [], recursor => pure recursor
   | some pos :: rest, recursor =>
     if h : pos < majorTypeArgs.size then
-      addRecParams mvarId majorTypeArgs rest (mkApp recursor (majorTypeArgs.get ⟨pos, h⟩))
+      addRecParams mvarId majorTypeArgs rest (mkApp recursor (majorTypeArgs[pos]))
     else
       throwTacticEx `induction mvarId "ill-formed recursor"
   | none :: rest, recursor => do
@@ -97,7 +97,7 @@ private partial def finalize
             if arity < initialArity then throwTacticEx `induction mvarId "ill-formed recursor"
             let nparams := arity - initialArity -- number of fields due to minor premise
             let nextra  := reverted.size - indices.size - 1 -- extra dependencies that have been reverted
-            let minorGivenNames := if h : minorIdx < givenNames.size then givenNames.get ⟨minorIdx, h⟩ else {}
+            let minorGivenNames := if h : minorIdx < givenNames.size then givenNames[minorIdx] else {}
             let mvar ← mkFreshExprSyntheticOpaqueMVar d (tag ++ n)
             let recursor := mkApp recursor mvar
             let recursorType ← getTypeBody mvarId recursorType mvar

src/Lean/Meta/Tactic/LinearArith/Solver.lean

@@ -29,7 +29,7 @@ abbrev Assignment.size (a : Assignment) : Nat :=
 
 abbrev Assignment.get? (a : Assignment) (x : Var) : Option Rat :=
   if h : x.id < a.size then
-    some (a.val.get ⟨x.id, h⟩)
+    some (a.val[x.id])
   else
     none
 
@@ -53,7 +53,7 @@ abbrev Poly.getMaxVar (e : Poly) : Var :=
   e.val.back!.2
 
 abbrev Poly.get (e : Poly) (i : Fin e.size) : Int × Var :=
-  e.val.get i
+  e.val[i]
 
 def Poly.scale (d : Int) (e : Poly) : Poly :=
   { e with val := e.val.map fun (c, x) => (c*d, x) }
@@ -169,7 +169,7 @@ def getBestBound? (cs : Array Cnstr) (a : Assignment) (isLower isInt : Bool) : O
   let adjust (v : Rat) :=
     if isInt then if isLower then (v.ceil : Rat) else v.floor else v
   if h : 0 < cs.size then
-    let c0 := cs.get ⟨0, h⟩
+    let c0 := cs[0]
     let b  := adjust <| c0.getBound a
     some <| cs[1:].foldl (init := (b, c0)) fun r c =>
       let b' := adjust <| c.getBound a

src/Lean/Meta/WHNF.lean

@@ -184,7 +184,7 @@ private def cleanupNatOffsetMajor (e : Expr) : MetaM Expr := do
 private def reduceRec (recVal : RecursorVal) (recLvls : List Level) (recArgs : Array Expr) (failK : Unit → MetaM α) (successK : Expr → MetaM α) : MetaM α :=
   let majorIdx := recVal.getMajorIdx
   if h : majorIdx < recArgs.size then do
-    let major := recArgs.get ⟨majorIdx, h⟩
+    let major := recArgs[majorIdx]
     let mut major ← if isWFRec recVal.name && (← getTransparency) == .default then
       -- If recursor is `Acc.rec` or `WellFounded.rec` and transparency is default,
       -- then we bump transparency to .all to make sure we can unfold defs defined by WellFounded recursion.
@@ -226,7 +226,7 @@ private def reduceRec (recVal : RecursorVal) (recLvls : List Level) (recArgs : A
 private def reduceQuotRec (recVal  : QuotVal) (recArgs : Array Expr) (failK : Unit → MetaM α) (successK : Expr → MetaM α) : MetaM α :=
   let process (majorPos argPos : Nat) : MetaM α :=
     if h : majorPos < recArgs.size then do
-      let major := recArgs.get ⟨majorPos, h⟩
+      let major := recArgs[majorPos]
       let major ← whnf major
       match major with
       | Expr.app (Expr.app (Expr.app (Expr.const majorFn _) _) _) majorArg => do
@@ -255,7 +255,7 @@ mutual
     else do
       let majorIdx := recVal.getMajorIdx
       if h : majorIdx < recArgs.size then do
-        let major := recArgs.get ⟨majorIdx, h⟩
+        let major := recArgs[majorIdx]
         let major ← whnf major
         getStuckMVar? major
       else
@@ -264,7 +264,7 @@ mutual
   private partial def isQuotRecStuck? (recVal : QuotVal) (recArgs : Array Expr) : MetaM (Option MVarId) :=
     let process? (majorPos : Nat) : MetaM (Option MVarId) :=
       if h : majorPos < recArgs.size then do
-        let major := recArgs.get ⟨majorPos, h⟩
+        let major := recArgs[majorPos]
         let major ← whnf major
         getStuckMVar? major
       else

src/Lean/Structure.lean

@@ -70,7 +70,7 @@ def StructureInfo.lt (i₁ i₂ : StructureInfo) : Bool :=
 
 def StructureInfo.getProjFn? (info : StructureInfo) (i : Nat) : Option Name :=
   if h : i < info.fieldNames.size then
-    let fieldName := info.fieldNames.get ⟨i, h⟩
+    let fieldName := info.fieldNames[i]
     info.fieldInfo.binSearch { fieldName := fieldName, projFn := default, subobject? := none, binderInfo := default } StructureFieldInfo.lt |>.map (·.projFn)
   else
     none

src/Lean/Util/InstantiateLevelParams.lean

@@ -43,9 +43,9 @@ def instantiateLevelParamsNoCache (e : Expr) (paramNames : List Name) (lvls : Li
 
 private partial def getParamSubstArray (ps : Array Name) (us : Array Level) (p' : Name) (i : Nat) : Option Level :=
   if h : i < ps.size then
-    let p := ps.get ⟨i, h⟩
+    let p := ps[i]
     if h : i < us.size then
-      let u := us.get ⟨i, h⟩
+      let u := us[i]
       if p == p' then some u else getParamSubstArray ps us p' (i+1)
     else none
   else none

src/Std/Data/DHashMap/Internal/Defs.lean

@@ -195,11 +195,10 @@ where
       (target : { d : Array (AssocList α β) // 0 < d.size }) :
       { d : Array (AssocList α β) // 0 < d.size } :=
     if h : i < source.size then
-      let idx : Fin source.size := ⟨i, h⟩
+      let es := source[i]
-      let es := source.get idx
       -- We erase `es` from `source` to make sure we can reuse its memory cells
       -- when performing es.foldl
-      let source := source.set idx .nil
+      let source := source.set i .nil
       let target := es.foldl (reinsertAux hash) target
       go (i+1) source target
     else target

src/Std/Data/DHashMap/Internal/WF.lean

@@ -167,7 +167,7 @@ theorem toListModel_foldl_reinsertAux [BEq α] [Hashable α] [PartialEquivBEq α
 theorem expand.go_pos [Hashable α] {i : Nat} {source : Array (AssocList α β)}
     {target : { d : Array (AssocList α β) // 0 < d.size }} (h : i < source.size) :
     expand.go i source target = go (i + 1)
-      (source.set i .nil) ((source.get ⟨i, h⟩).foldl (reinsertAux hash) target) := by
+      (source.set i .nil) ((source[i]).foldl (reinsertAux hash) target) := by
   rw [expand.go]
   simp only [h, dite_true]
 
@@ -186,7 +186,7 @@ theorem expand.go_eq [BEq α] [Hashable α] [PartialEquivBEq α] (source : Array
     simpa using this 0
   intro i
   induction i, source, target using expand.go.induct
-  · next i source target hi _ es newSource newTarget ih =>
+  · next i source target _ hi es newSource newTarget ih =>
     simp only [newSource, newTarget, es] at *
     rw [expand.go_pos hi]
     refine ih.trans ?_

tests/bench/unionfind.lean

@@ -47,7 +47,7 @@ def findEntryAux : Nat → Node → M nodeData
 | i+1, n =>
   do let s ← read;
      if h : n < s.size then
-       do { let e := s.get ⟨n, h⟩;
+       do { let e := s[n];
             if e.find = n then pure e
             else do let e₁ ← findEntryAux i e.find;
                     updt (fun s => s.set! n e₁);

tests/lean/arrayGetU.lean

@@ -1,5 +1,5 @@
 def f (a : Array Nat) (i : Nat) (v : Nat) (h : i < a.size) : Array Nat :=
-  a.set i (a.get ⟨i, h⟩ + v)
+  a.set i (a.get i h + v)
 
 set_option pp.proofs true
 

tests/lean/funind_errors.lean

@@ -8,7 +8,7 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
 where
   foo (i : Nat) (r : Array α) : Array α :=
     if h : i < as.size then
-      let a := as.get ⟨i, h⟩
+      let a := as.get i h
       if p a then
         foo (i+1) (r.push a)
       else

tests/lean/funind_errors.lean.expected.out

@@ -6,11 +6,11 @@ has type
 takeWhile.foo.induct.{u_1} {α : Type u_1} (p : α → Bool) (as : Array α) (motive : Nat → Array α → Prop)
   (case1 :
     ∀ (i : Nat) (r : Array α) (h : i < as.size),
-      let a := as.get ⟨i, h⟩;
+      let a := as.get i h;
       p a = true → motive (i + 1) (r.push a) → motive i r)
   (case2 :
     ∀ (i : Nat) (r : Array α) (h : i < as.size),
-      let a := as.get ⟨i, h⟩;
+      let a := as.get i h;
       ¬p a = true → motive i r)
   (case3 : ∀ (i : Nat) (r : Array α), ¬i < as.size → motive i r) (i : Nat) (r : Array α) : motive i r
 funind_errors.lean:38:7-38:20: error: invalid field notation, type is not of the form (C ...) where C is a constant

tests/lean/run/988.lean

@@ -9,20 +9,20 @@ theorem append_empty (x : Fin i → Nat) : x ++ empty = x :=
 opaque f : (Fin 0 → Nat) → Prop
 example : f (empty ++ empty) = f empty := by simp only [append_empty] -- should work
 
-@[congr] theorem Array.get_congr (as bs : Array α) (h : as = bs) (i : Fin as.size) (j : Nat) (hi : i = j) :
+@[congr] theorem Array.get_congr (as bs : Array α) (w : as = bs) (i : Nat) (h : i < as.size) (j : Nat) (hi : i = j) :
-    as.get i = bs.get ⟨j, h ▸ hi ▸ i.2⟩ := by
+    as[i] = (bs[j]'(w ▸ hi ▸ h)) := by
   subst bs; subst j; rfl
 
 example (as : Array Nat) (h : 0 + x < as.size) :
-    as.get ⟨0 + x, h⟩ = as.get ⟨x, Nat.zero_add x ▸ h⟩ := by
+    as[0 + x] = as[x] := by
   simp -- should work
 
 example (as : Array (Nat → Nat)) (h : 0 + x < as.size) :
-    as.get ⟨0 + x, h⟩ i = as.get ⟨x, Nat.zero_add x ▸ h⟩ i := by
+    as[0 + x] = as[x]'(Nat.zero_add x ▸ h) := by
   simp -- should also work
 
 example (as : Array (Nat → Nat)) (h : 0 + x < as.size) :
-    as.get ⟨0 + x, h⟩ i = as.get ⟨x, Nat.zero_add x ▸ h⟩ (0+i) := by
+    as[0 + x] i = as[x] (0+i) := by
   simp -- should also work
 
 example [Decidable p] : decide (p ∧ True) = decide p := by simp -- should work

tests/lean/run/appFinalizeIssue.lean

@@ -9,7 +9,7 @@ instance : GetElem Lean.Syntax Nat Lean.Syntax where
   getElem' xs i := xs.getArg i
 
 instance : GetElem (Array α) Nat α where
-  getElem' xs i := xs.get ⟨i, sorry⟩
+  getElem' xs i := xs.get i sorry
 
 open Lean
 

tests/lean/run/array1.lean

@@ -8,7 +8,7 @@ def w : Array Nat :=
 #check @Array.casesOn
 
 def f : Fin w.size → Nat :=
-  w.get
+  fun i => w.get i i.isLt
 
 def arraySum (a : Array Nat) : Nat :=
 a.foldl Nat.add 0

tests/lean/run/coeOutParamIssue2.lean

@@ -5,7 +5,7 @@ class GetElem (Cont : Type u) (Idx : Type v) (Elem : outParam (Type w)) where
 export GetElem (getElem)
 
 instance : GetElem (Array α) Nat α where
-  getElem xs i := xs.get ⟨i, sorry⟩
+  getElem xs i := xs.get i sorry
 
 opaque f : Option Bool → Bool
 opaque g : Bool → Bool

tests/lean/run/doNotation3.lean

@@ -11,7 +11,7 @@ let rec loop : (i : Nat) → i ≤ as.size → β → m β
     have h' : i < as.size          := Nat.lt_of_lt_of_le (Nat.lt_succ_self i) h
     have : as.size - 1 < as.size     := Nat.sub_lt (zero_lt_of_lt h') (by decide)
     have : as.size - 1 - i < as.size := Nat.lt_of_le_of_lt (Nat.sub_le (as.size - 1) i) this
-    let b ← f (as.get ⟨as.size - 1 - i, this⟩) b
+    let b ← f as[as.size - 1 - i] b
     loop i (Nat.le_of_lt h') b
 loop as.size (Nat.le_refl _) b
 
@@ -28,7 +28,7 @@ let rec loop (i : Nat) (h : i ≤ as.size) (b : β) : m β := do
     have h' : i < as.size          := Nat.lt_of_lt_of_le (Nat.lt_succ_self i) h
     have : as.size - 1 < as.size     := Nat.sub_lt (zero_lt_of_lt h') (by decide)
     have : as.size - 1 - i < as.size := Nat.lt_of_le_of_lt (Nat.sub_le (as.size - 1) i) this
-    let b ← f (as.get ⟨as.size - 1 - i, this⟩) b
+    let b ← f as[as.size - 1 - i] b
     loop i (Nat.le_of_lt h') b
 loop as.size (Nat.le_refl _) b
 

tests/lean/run/forInRangeWF.lean

@@ -6,7 +6,7 @@ def Expr.size (e : Expr) : Nat := Id.run do
   | app f args =>
     let mut sz := 1
     for h : i in [: args.size] do
-      sz := sz + size (args.get ⟨i, h.upper⟩)
+      sz := sz + size args[i]
     return sz
 
 namespace Ex2

tests/lean/run/forOutParamIssue.lean

@@ -5,7 +5,7 @@ class GetElem (Cont : Type u) (Idx : Type v) (Elem : outParam (Type w)) where
 export GetElem (getElem)
 
 instance : GetElem (Array α) Nat α where
-  getElem xs i := xs.get ⟨i, sorry⟩
+  getElem xs i := xs.get i sorry
 
 opaque f : Option Bool → Id Unit
 

tests/lean/run/heapSort.lean

@@ -22,9 +22,9 @@ def heapifyDown (lt : α → α → Bool) (a : Array α) (i : Fin a.size) :
   have right_le : i ≤ right := Nat.le_trans left_le (Nat.le_add_right ..)
   have i_le : i ≤ i := Nat.le_refl _
   have j : {j : Fin a.size // i ≤ j} := if h : left < a.size then
-    if lt (a.get i) (a.get ⟨left, h⟩) then ⟨⟨left, h⟩, left_le⟩ else ⟨i, i_le⟩ else ⟨i, i_le⟩
+    if lt a[i] a[left] then ⟨⟨left, h⟩, left_le⟩ else ⟨i, i_le⟩ else ⟨i, i_le⟩
   have j := if h : right < a.size then
-    if lt (a.get j) (a.get ⟨right, h⟩) then ⟨⟨right, h⟩, right_le⟩ else j else j
+    if lt a[j.1] a[right] then ⟨⟨right, h⟩, right_le⟩ else j else j
   if h : i.1 = j then ⟨a, rfl⟩ else
     let a' := a.swap i j
     let j' := ⟨j, by rw [a.size_swap i j]; exact j.1.2⟩
@@ -59,8 +59,8 @@ def heapifyUp (lt : α → α → Bool) (a : Array α) (i : Fin a.size) :
   {a' : Array α // a'.size = a.size} :=
 if i0 : i.1 = 0 then ⟨a, rfl⟩ else
   have : (i.1 - 1) / 2 < i := sorry
-  let j := ⟨(i.1 - 1) / 2, Nat.lt_trans this i.2⟩
+  let j : Fin a.size := ⟨(i.1 - 1) / 2, Nat.lt_trans this i.2⟩
-  if lt (a.get j) (a.get i) then
+  if lt a[j] a[i] then
     let a' := a.swap i j
     let ⟨a₂, h₂⟩ := heapifyUp lt a' ⟨j.1, by rw [a.size_swap i j]; exact j.2⟩
     ⟨a₂, h₂.trans (a.size_swap i j)⟩
@@ -84,7 +84,7 @@ def singleton (lt) (x : α) : BinaryHeap α lt := ⟨#[x]⟩
 def size {lt} (self : BinaryHeap α lt) : Nat := self.1.size
 
 /-- `O(1)`. Get an element in the heap by index. -/
-def get {lt} (self : BinaryHeap α lt) (i : Fin self.size) : α := self.1.get i
+def get {lt} (self : BinaryHeap α lt) (i : Fin self.size) : α := self.1.get i i.2
 
 /-- `O(log n)`. Insert an element into a `BinaryHeap`, preserving the max-heap property. -/
 def insert {lt} (self : BinaryHeap α lt) (x : α) : BinaryHeap α lt where

tests/lean/run/issue5061.lean

@@ -8,7 +8,7 @@ def test (a: Array Nat) : Nat := @fin_max _ fun i =>
     with_reducible apply Fin.val_lt_of_le
     fail_if_success with_reducible apply Fin.val_lt_of_le;
     exact Nat.le_refl _
-  a.get ⟨i, h⟩
+  a[i]
 
 set_option pp.mvars false
 
@@ -30,4 +30,4 @@ set_option maxRecDepth 40 in
 def test2 (a: Array Nat) : Nat := @fin_max _ fun i =>
   let h : i < a.size := by
     get_elem_tactic
-  a.get ⟨i, h⟩
+  a[i]

tests/lean/run/lcnfInferProjTypeIssue.lean

@@ -15,14 +15,14 @@ instance {n} : Add (NFloatArray n) :=
  ⟨λ x y => Id.run do
    let mut x := x.1
    for i in [0:n] do
-     x := x.set ⟨i,sorry⟩ (x[i]'sorry+y.1[i]'sorry)
+     x := x.set i (x[i]'sorry+y.1[i]'sorry) sorry
    ⟨x,sorry⟩⟩
 
 instance {n} : HMul Float (NFloatArray n) (NFloatArray n) :=
  ⟨λ s x => Id.run do
    let mut x := x.1
    for i in [0:n] do
-     x := x.set ⟨i,sorry⟩ (s*x[i]'sorry)
+     x := x.set i (s*x[i]'sorry) sorry
    ⟨x,sorry⟩⟩
 
 def FloatVector : Nat → Type

tests/lean/run/missingSizeOfArrayGetThm.lean

@@ -5,7 +5,7 @@ inductive Node (Data : Type) : Type where
 
 def Node.FixedBranching (n : Nat) : Node Data → Prop
   | empty => True
-  | node children => children.size = n ∧ ∀ i, (children.get i).FixedBranching n
+  | node children => children.size = n ∧ ∀ (i : Nat) h, (children[i]'h).FixedBranching n
   | leaf _ => True
 
 structure MNode (Data : Type) (m : Nat) where

tests/lean/run/newfrontend3.lean

@@ -16,8 +16,8 @@ by {
 }
 
 def g (i j k : Nat) (a : Array Nat) (h₁ : i < k) (h₂ : k < j) (h₃ : j < a.size) : Nat :=
-  let vj := a.get ⟨j, h₃⟩;
+  let vj := a[j];
-  let vi := a.get ⟨i, Nat.lt_trans h₁ (Nat.lt_trans h₂ h₃)⟩;
+  let vi := a[i];
   vi + vj
 
 set_option pp.all true in

tests/lean/run/overAndPartialAppsAtWF.lean

@@ -8,7 +8,7 @@ def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) (
 termination_by a.size - i
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
-theorem eq_of_isEqvAux [DecidableEq α] (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size) (heqv : isEqvAux a b hsz (fun x y => x = y) i) : ∀ (j : Nat) (hl : i ≤ j) (hj : j < a.size), a.get ⟨j, hj⟩ = b.get ⟨j, hsz ▸ hj⟩ := by
+theorem eq_of_isEqvAux [DecidableEq α] (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size) (heqv : isEqvAux a b hsz (fun x y => x = y) i) : ∀ (j : Nat) (hl : i ≤ j) (hj : j < a.size), a[j] = b[j] := by
   intro j low high
   by_cases h : i < a.size
   · unfold isEqvAux at heqv

tests/lean/run/simproc_panic.lean

@@ -15,11 +15,11 @@ structure UnionFind (α) where
 -- set_option simprocs false
 
 def rankMaxAux (self : UnionFind α) : ∀ (i : Nat),
-    {k : Nat // ∀ j, j < i → ∀ h, (self.arr.get ⟨j, h⟩).rank ≤ k}
+    {k : Nat // ∀ j, j < i → ∀ h, self.arr[j].rank ≤ k}
   | 0 => ⟨0, fun j hj => nomatch hj⟩
   | i+1 => by
     let ⟨k, H⟩ := rankMaxAux self i
-    refine ⟨max k (if h : _ then (self.arr.get ⟨i, h⟩).rank else 0), fun j hj h ↦ ?_⟩
+    refine ⟨max k (if h : _ then self.arr[i].rank else 0), fun j hj h ↦ ?_⟩
     match j, Nat.lt_or_eq_of_le (Nat.le_of_lt_succ hj) with
     | j, Or.inl hj => exact Nat.le_trans (H _ hj h) (Nat.le_max_left _ _)
     | _, Or.inr rfl => simp [h, Nat.le_max_right]

tests/lean/run/subst.lean

@@ -43,7 +43,7 @@ theorem ex10 (a b : Nat) (h : a = b) : b = a :=
 h ▸ rfl
 
 def ex11  {α : Type u} {n : Nat} (a : Array α) (i : Nat) (h₁ : a.size = n) (h₂ : i < n) : α :=
-  a.get ⟨i, h₁ ▸ h₂⟩
+  a[i]
 
 theorem ex12 {α : Type u} {n : Nat}
   (a b : Array α)
@@ -58,7 +58,7 @@ partial def isEqvAux {α} (a b : Array α) (hsz : a.size = b.size) (p : α →
   if h : i < a.size then
      let aidx : Fin a.size := ⟨i, h⟩
      let bidx : Fin b.size := ⟨i, hsz ▸ h⟩
-     match p (a.get aidx) (b.get bidx) with
+     match p a[aidx] b[bidx] with
      | true  => isEqvAux a b hsz p (i+1)
      | false => false
   else

tests/lean/run/wfSum.lean

@@ -3,7 +3,7 @@ def sum (as : Array Nat) : Nat :=
 where
   go (i : Nat) (s : Nat) : Nat :=
     if h : i < as.size then
-      go (i+1) (s + as.get ⟨i, h⟩)
+      go (i+1) (s + as[i])
     else
       s
   termination_by as.size - i

tests/lean/simpArrayIdx.lean

@@ -9,7 +9,7 @@ variable (j_lt : j < (a.set! i v).size)
 
 #check_simp (i + 0) ~> i
 
-#check_simp (a.set! i v).get ⟨i, g⟩ ~> v
+#check_simp (a.set! i v).get i g ~> v
 #check_simp (a.set! i v).get! i ~> (a.setD i v)[i]!
 #check_simp (a.set! i v).getD i d ~> if i < a.size then v else d
 #check_simp (a.set! i v)[i] ~> v

tests/lean/substBadMotive.lean

@@ -25,9 +25,9 @@ def heapifyDown (lt : α → α → Bool) (a : Array α) (i : Fin a.size) : Arra
   have right_le : i ≤ right := sorry
   have i_le : i ≤ i := Nat.le_refl _
   have j : {j : Fin a.size // i ≤ j} := if h : left < a.size then
-    if lt (a.get i) (a.get ⟨left, h⟩) then ⟨⟨left, h⟩, left_le⟩ else ⟨i, i_le⟩ else ⟨i, i_le⟩
+    if lt a[i] a[left] then ⟨⟨left, h⟩, left_le⟩ else ⟨i, i_le⟩ else ⟨i, i_le⟩
   have j := if h : right < a.size then
-    if lt (a.get j) (a.get ⟨right, h⟩) then ⟨⟨right, h⟩, right_le⟩ else j else j
+    if lt a[j.1.1] a[right] then ⟨⟨right, h⟩, right_le⟩ else j else j
   if h : i ≠ j then
     let a' := a.swap i j
     have : a'.size - j < a.size - i := sorry