diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index 343ab74bd8..37f5509f2d 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -8,6 +8,7 @@ import Init.Data.Nat.Lemmas
 import Init.Data.List.Impl
 import Init.Data.List.Monadic
 import Init.Data.List.Range
+import Init.Data.List.Nat.TakeDrop
 import Init.Data.Array.Mem
 import Init.TacticsExtra
 
@@ -43,21 +44,32 @@ theorem getElem?_eq_getElem?_toList (a : Array α) (i : Nat) : a[i]? = a.toList[
   rw [getElem?_eq]
   split <;> simp_all
 
-theorem get_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
+theorem getElem_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
     have : i < (a.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]
     (a.push x)[i] = a[i] := by
   simp only [push, getElem_eq_getElem_toList, List.concat_eq_append, List.getElem_append_left, h]
 
-@[simp] theorem get_push_eq (a : Array α) (x : α) : (a.push x)[a.size] = x := by
+@[simp] theorem getElem_push_eq (a : Array α) (x : α) : (a.push x)[a.size] = x := by
   simp only [push, getElem_eq_getElem_toList, List.concat_eq_append]
   rw [List.getElem_append_right] <;> simp [getElem_eq_getElem_toList, Nat.zero_lt_one]
 
-theorem get_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) :
+theorem getElem_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) :
     (a.push x)[i] = if h : i < a.size then a[i] else x := by
   by_cases h' : i < a.size
-  · simp [get_push_lt, h']
+  · simp [getElem_push_lt, h']
   · simp at h
-    simp [get_push_lt, Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.ge_of_not_lt h')]
+    simp [getElem_push_lt, Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.ge_of_not_lt h')]
+
+@[deprecated getElem_push (since := "2024-10-21")] abbrev get_push := @getElem_push
+@[deprecated getElem_push_lt (since := "2024-10-21")] abbrev get_push_lt := @getElem_push_lt
+@[deprecated getElem_push_eq (since := "2024-10-21")] abbrev get_push_eq := @getElem_push_eq
+
+@[simp] theorem get!_eq_getElem! [Inhabited α] (a : Array α) (i : Nat) : a.get! i = a[i]! := by
+  simp [getElem!_def, get!, getD]
+  split <;> rename_i h
+  · simp [getElem?_eq_getElem h]
+    rfl
+  · simp [getElem?_eq_none_iff.2 (by simpa using h)]
 
 end Array
 
@@ -81,6 +93,9 @@ We prefer to pull `List.toArray` outwards.
 
 @[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
+
 @[simp] theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray := by
   apply ext'
   simp
@@ -90,6 +105,14 @@ We prefer to pull `List.toArray` outwards.
   funext a
   simp
 
+@[simp] theorem isEmpty_toArray (l : List α) : l.toArray.isEmpty = l.isEmpty := by
+  cases l <;> simp
+
+@[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = singleton a := rfl
+
+@[simp] theorem back_toArray [Inhabited α] (l : List α) : l.toArray.back = l.getLast! := by
+  simp only [back, size_toArray, Array.get!_eq_getElem!, getElem!_toArray, getLast!_eq_getElem!]
+
 theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List α) :
     l.toArray.foldrM f init = l.foldrM f init := by
   rw [foldrM_eq_reverse_foldlM_toList]
@@ -248,7 +271,7 @@ theorem size_uset (a : Array α) (v i h) : (uset a i v h).size = a.size := by si
 @[simp] theorem get_eq_getElem (a : Array α) (i : Fin _) : a.get i = a[i.1] := rfl
 
 theorem getElem?_lt
-    (a : Array α) {i : Nat} (h : i < a.size) : a[i]? = some (a[i]) := dif_pos h
+    (a : Array α) {i : Nat} (h : i < a.size) : a[i]? = some a[i] := dif_pos h
 
 theorem getElem?_ge
     (a : Array α) {i : Nat} (h : i ≥ a.size) : a[i]? = none := dif_neg (Nat.not_lt_of_le h)
@@ -271,8 +294,10 @@ theorem getD_get? (a : Array α) (i : Nat) (d : α) :
 
 theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default := rfl
 
-@[simp] theorem get!_eq_getElem? [Inhabited α] (a : Array α) (i : Nat) : a.get! i = (a.get? i).getD default := by
-  by_cases p : i < a.size <;> simp [getD_get?, get!_eq_getD, p]
+@[simp] theorem get!_eq_getElem? [Inhabited α] (a : Array α) (i : Nat) :
+    a.get! i = (a.get? i).getD default := by
+  by_cases p : i < a.size <;>
+  simp only [get!_eq_getD, getD_eq_get?, getD_get?, p, get?_eq_getElem?]
 
 /-! # set -/
 
@@ -352,8 +377,8 @@ theorem getElem_ofFn_go (f : Fin n → α) (i) {acc k}
     simp only [dif_pos hin]
     rw [getElem_ofFn_go f (i+1) _ hin (by simp [*]) (fun j hj => ?hacc)]
     cases (Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ (by simpa using hj)) with
-    | inl hj => simp [get_push, hj, hacc j hj]
-    | inr hj => simp [get_push, *]
+    | inl hj => simp [getElem_push, hj, hacc j hj]
+    | inr hj => simp [getElem_push, *]
   else
     simp [hin, hacc k (Nat.lt_of_lt_of_le hki (Nat.le_of_not_lt (hi ▸ hin)))]
 termination_by n - i
@@ -421,7 +446,7 @@ theorem lt_of_getElem {x : α} {a : Array α} {idx : Nat} {hidx : idx < a.size}
     idx < a.size :=
   hidx
 
-theorem getElem_mem {l : Array α} {i : Nat} (h : i < l.size) : l[i] ∈ l := by
+@[simp] theorem getElem_mem {l : Array α} {i : Nat} (h : i < l.size) : l[i] ∈ l := by
   erw [Array.mem_def, getElem_eq_getElem_toList]
   apply List.get_mem
 
@@ -430,9 +455,11 @@ theorem getElem_fin_eq_getElem_toList (a : Array α) (i : Fin a.size) : a[i] = a
 @[simp] theorem ugetElem_eq_getElem (a : Array α) {i : USize} (h : i.toNat < a.size) :
   a[i] = a[i.toNat] := rfl
 
-theorem get?_len_le (a : Array α) (i : Nat) (h : a.size ≤ i) : a[i]? = none := by
+theorem getElem?_size_le (a : Array α) (i : Nat) (h : a.size ≤ i) : a[i]? = none := by
   simp [getElem?_neg, h]
 
+@[deprecated getElem?_size_le (since := "2024-10-21")] abbrev get?_len_le := @getElem?_size_le
+
 theorem getElem_mem_toList (a : Array α) (h : i < a.size) : a[i] ∈ a.toList := by
   simp only [getElem_eq_getElem_toList, List.getElem_mem]
 
@@ -440,35 +467,39 @@ theorem get?_eq_get?_toList (a : Array α) (i : Nat) : a.get? i = a.toList.get?
   simp [getElem?_eq_getElem?_toList]
 
 theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD default := by
-  simp [get!_eq_getD]
+  simp only [get!_eq_getElem?, get?_eq_getElem?]
 
 theorem getElem?_eq_some_iff {as : Array α} : as[n]? = some a ↔ ∃ h : n < as.size, as[n] = a := by
   cases as
   simp [List.getElem?_eq_some_iff]
 
 @[simp] theorem back_eq_back? [Inhabited α] (a : Array α) : a.back = a.back?.getD default := by
-  simp [back, back?]
+  simp only [back, get!_eq_getElem?, get?_eq_getElem?, back?]
 
 @[simp] theorem back?_push (a : Array α) : (a.push x).back? = some x := by
   simp [back?, getElem?_eq_getElem?_toList]
 
 theorem back_push [Inhabited α] (a : Array α) : (a.push x).back = x := by simp
 
-theorem get?_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
+theorem getElem?_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
     (a.push x)[i]? = some a[i] := by
-  rw [getElem?_pos, get_push_lt]
+  rw [getElem?_pos, getElem_push_lt]
 
-theorem get?_push_eq (a : Array α) (x : α) : (a.push x)[a.size]? = some x := by
-  rw [getElem?_pos, get_push_eq]
+@[deprecated getElem?_push_lt (since := "2024-10-21")] abbrev get?_push_lt := @getElem?_push_lt
 
-theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x else a[i]? := by
+theorem getElem?_push_eq (a : Array α) (x : α) : (a.push x)[a.size]? = some x := by
+  rw [getElem?_pos, getElem_push_eq]
+
+@[deprecated getElem?_push_eq (since := "2024-10-21")] abbrev get?_push_eq := @getElem?_push_eq
+
+theorem getElem?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x else a[i]? := by
   match Nat.lt_trichotomy i a.size with
   | Or.inl g =>
     have h1 : i < a.size + 1 := by omega
     have h2 : i ≠ a.size := by omega
-    simp [getElem?_def, size_push, g, h1, h2, get_push_lt]
+    simp [getElem?_def, size_push, g, h1, h2, getElem_push_lt]
   | Or.inr (Or.inl heq) =>
-    simp [heq, getElem?_pos, get_push_eq]
+    simp [heq, getElem?_pos, getElem_push_eq]
   | Or.inr (Or.inr g) =>
     simp only [getElem?_def, size_push]
     have h1 : ¬ (i < a.size) := by omega
@@ -476,9 +507,13 @@ theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x el
     have h3 : i ≠ a.size := by omega
     simp [h1, h2, h3]
 
-@[simp] theorem get?_size {a : Array α} : a[a.size]? = none := by
+@[deprecated getElem?_push (since := "2024-10-21")] abbrev get?_push := @getElem?_push
+
+@[simp] theorem getElem?_size {a : Array α} : a[a.size]? = none := by
   simp only [getElem?_def, Nat.lt_irrefl, dite_false]
 
+@[deprecated getElem?_size (since := "2024-10-21")] abbrev get?_size := @getElem?_size
+
 @[simp] theorem toList_set (a : Array α) (i v) : (a.set i v).toList = a.toList.set i.1 v := rfl
 
 theorem get_set_eq (a : Array α) (i : Fin a.size) (v : α) :
@@ -528,6 +563,9 @@ theorem getElem?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)
 @[simp] theorem swapAt_def (a : Array α) (i : Fin a.size) (v : α) :
     a.swapAt i v = (a[i.1], a.set i v) := rfl
 
+@[simp] theorem size_swapAt (a : Array α) (i : Fin a.size) (v : α) :
+    (a.swapAt i v).2.size = a.size := by simp [swapAt_def]
+
 @[simp]
 theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
     a.swapAt! i v = (a[i], a.set ⟨i, h⟩ v) := by simp [swapAt!, h]
@@ -560,11 +598,11 @@ theorem eq_push_pop_back_of_size_ne_zero [Inhabited α] {as : Array α} (h : as.
   · simp [Nat.sub_add_cancel (Nat.zero_lt_of_ne_zero h)]
   · intros i h h'
     if hlt : i < as.pop.size then
-      rw [get_push_lt (h:=hlt), getElem_pop]
+      rw [getElem_push_lt (h:=hlt), getElem_pop]
     else
       have heq : i = as.pop.size :=
         Nat.le_antisymm (size_pop .. ▸ Nat.le_pred_of_lt h) (Nat.le_of_not_gt hlt)
-      cases heq; rw [get_push_eq, back, ←size_pop, get!_eq_getD, getD, dif_pos h]; rfl
+      cases heq; rw [getElem_push_eq, back, ←size_pop, get!_eq_getD, getD, dif_pos h]; rfl
 
 theorem eq_push_of_size_ne_zero {as : Array α} (h : as.size ≠ 0) :
     ∃ (bs : Array α) (c : α), as = bs.push c :=
@@ -773,9 +811,9 @@ theorem map_induction (as : Array α) (f : α → β) (motive : Nat → Prop) (h
     · intro j h
       simp at h ⊢
       by_cases h' : j < size b
-      · rw [get_push]
+      · rw [getElem_push]
         simp_all
-      · rw [get_push, dif_neg h']
+      · rw [getElem_push, dif_neg h']
         simp only [show j = i by omega]
         exact (hs _ m).1
 
@@ -800,7 +838,7 @@ theorem map_spec (as : Array α) (f : α → β) (p : Fin as.size → β → Pro
     (as.push x).map f = (as.map f).push (f x) := by
   ext
   · simp
-  · simp only [getElem_map, get_push, size_map]
+  · simp only [getElem_map, getElem_push, size_map]
     split <;> rfl
 
 @[simp] theorem map_pop {f : α → β} {as : Array α} :
@@ -831,6 +869,11 @@ theorem getElem_modify_of_ne {as : Array α} {i : Nat} (h : i ≠ j)
     (as.modify i f)[j] = as[j]'(by simpa using hj) := by
   simp [getElem_modify hj, h]
 
+theorem getElem?_modify {as : Array α} {i : Nat} {f : α → α} {j : Nat} :
+    (as.modify i f)[j]? = if i = j then as[j]?.map f else as[j]? := by
+  simp only [getElem?_def, size_modify, getElem_modify, Option.map_dif]
+  split <;> split <;> rfl
+
 /-! ### filter -/
 
 @[simp] theorem toList_filter (p : α → Bool) (l : Array α) :
@@ -892,7 +935,7 @@ theorem filterMap_congr {as bs : Array α} (h : as = bs)
 
 theorem size_empty : (#[] : Array α).size = 0 := rfl
 
-theorem toList_empty : (#[] : Array α).toList = [] := rfl
+@[simp] theorem toList_empty : (#[] : Array α).toList = [] := rfl
 
 /-! ### append -/
 
@@ -1050,7 +1093,7 @@ theorem getElem_extract_loop_ge (as bs : Array α) (size start : Nat) (hge : i 
       have h₂ : bs.size < (extract.loop as size (start+1) (bs.push as[start])).size := by
         rw [size_extract_loop]; apply Nat.lt_of_lt_of_le h₁; exact Nat.le_add_right ..
       have h : (extract.loop as size (start + 1) (push bs as[start]))[bs.size] = as[start] := by
-        rw [getElem_extract_loop_lt as (bs.push as[start]) size (start+1) h₁ h₂, get_push_eq]
+        rw [getElem_extract_loop_lt as (bs.push as[start]) size (start+1) h₁ h₂, getElem_push_eq]
       rw [h]; congr; rw [Nat.add_sub_cancel]
     else
       have hge : bs.size + 1 ≤ i := Nat.lt_of_le_of_ne hge hi
@@ -1077,6 +1120,14 @@ theorem getElem?_extract {as : Array α} {start stop : Nat} :
     · omega
   · rfl
 
+@[simp] theorem toList_extract (as : Array α) (start stop : Nat) :
+    (as.extract start stop).toList = (as.toList.drop start).take (stop - start) := by
+  apply List.ext_getElem
+  · simp only [length_toList, size_extract, List.length_take, List.length_drop]
+    omega
+  · intros n h₁ h₂
+    simp
+
 @[simp] theorem extract_all (as : Array α) : as.extract 0 as.size = as := by
   apply ext
   · rw [size_extract, Nat.min_self, Nat.sub_zero]
@@ -1246,7 +1297,7 @@ open Fin
       · assumption
 
 theorem getElem_swap' (a : Array α) (i j : Fin a.size) (k : Nat) (hk : k < a.size) :
-    (a.swap i j)[k]'(by simp_all) = if k = i then a[j] else if k = j then a[i]  else a[k] := by
+    (a.swap i j)[k]'(by simp_all) = if k = i then a[j] else if k = j then a[i] else a[k] := by
   split
   · simp_all only [getElem_swap_left]
   · split <;> simp_all
@@ -1256,7 +1307,7 @@ theorem getElem_swap (a : Array α) (i j : Fin a.size) (k : Nat) (hk : k < (a.sw
   apply getElem_swap'
 
 @[simp] theorem swap_swap (a : Array α) {i j : Fin a.size} :
-    (a.swap i j).swap ⟨i.1, (a.size_swap ..).symm ▸i.2⟩ ⟨j.1, (a.size_swap ..).symm ▸j.2⟩ = a := by
+    (a.swap i j).swap ⟨i.1, (a.size_swap ..).symm ▸ i.2⟩ ⟨j.1, (a.size_swap ..).symm ▸ j.2⟩ = a := by
   apply ext
   · simp only [size_swap]
   · intros
@@ -1419,6 +1470,11 @@ theorem filterMap_toArray (f : α → Option β) (l : List α) :
   apply ext'
   simp
 
+@[simp] theorem toArray_extract (l : List α) (start stop : Nat) :
+    l.toArray.extract start stop = ((l.drop start).take (stop - start)).toArray := by
+  apply ext'
+  simp
+
 end List
 
 /-! ### Deprecations -/
diff --git a/src/Init/Data/Array/MapIdx.lean b/src/Init/Data/Array/MapIdx.lean
index 8c90ae8d25..763d76eae0 100644
--- a/src/Init/Data/Array/MapIdx.lean
+++ b/src/Init/Data/Array/MapIdx.lean
@@ -28,7 +28,7 @@ theorem mapFinIdx_induction (as : Array α) (f : Fin as.size → α → β)
     | succ i ih =>
       apply @ih (bs.push (f ⟨j, by omega⟩ as[j])) (j + 1) (by omega) (by simp; omega)
       · intro i i_lt h'
-        rw [get_push]
+        rw [getElem_push]
         split
         · apply h₂
         · simp only [size_push] at h'
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index bb28f4d00e..b89341f4cc 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -1047,9 +1047,6 @@ theorem get_cons_length (x : α) (xs : List α) (n : Nat) (h : n = xs.length) :
 
 @[simp] theorem getLast?_singleton (a : α) : getLast? [a] = a := rfl
 
-theorem getLast!_of_getLast? [Inhabited α] : ∀ {l : List α}, getLast? l = some a → getLast! l = a
-  | _ :: _, rfl => rfl
-
 theorem getLast?_eq_getLast : ∀ l h, @getLast? α l = some (getLast l h)
   | [], h => nomatch h rfl
   | _ :: _, _ => rfl
@@ -1083,6 +1080,21 @@ theorem getLast?_concat (l : List α) : getLast? (l ++ [a]) = some a := by
 theorem getLastD_concat (a b l) : @getLastD α (l ++ [b]) a = b := by
   rw [getLastD_eq_getLast?, getLast?_concat]; rfl
 
+/-! ### getLast! -/
+
+@[simp] theorem getLast!_nil [Inhabited α] : ([] : List α).getLast! = default := rfl
+
+theorem getLast!_of_getLast? [Inhabited α] : ∀ {l : List α}, getLast? l = some a → getLast! l = a
+  | _ :: _, rfl => rfl
+
+theorem getLast!_eq_getElem! [Inhabited α] {l : List α} : l.getLast! = l[l.length - 1]! := by
+  cases l with
+  | nil => simp
+  | cons _ _ =>
+    apply getLast!_of_getLast?
+    rw [getElem!_pos, getElem_cons_length (h := by simp)]
+    rfl
+
 /-! ## Head and tail -/
 
 /-! ### head -/
diff --git a/src/Std/Sat/AIG/Basic.lean b/src/Std/Sat/AIG/Basic.lean
index 86c06caebf..cf12873255 100644
--- a/src/Std/Sat/AIG/Basic.lean
+++ b/src/Std/Sat/AIG/Basic.lean
@@ -128,7 +128,7 @@ theorem Cache.get?_property {decls : Array (Decl α)} {idx : Nat} (c : Cache α
   induction hcache generalizing decl with
   | empty => simp at hfound
   | push_id wf ih =>
-    rw [Array.get_push]
+    rw [Array.getElem_push]
     split
     · apply ih
       simp [hfound]
@@ -140,7 +140,7 @@ theorem Cache.get?_property {decls : Array (Decl α)} {idx : Nat} (c : Cache α
       assumption
   | push_cache wf ih =>
     rename_i decl'
-    rw [Array.get_push]
+    rw [Array.getElem_push]
     split
     · simp only [HashMap.getElem?_insert] at hfound
       match heq : decl == decl' with
@@ -464,7 +464,7 @@ def mkGate (aig : AIG α) (input : GateInput aig) : Entrypoint α :=
   let cache := aig.cache.noUpdate
   have invariant := by
     intro i lhs' rhs' linv' rinv' h1 h2
-    simp only [Array.get_push] at h2
+    simp only [Array.getElem_push] at h2
     split at h2
     · apply aig.invariant <;> assumption
     · injections
@@ -483,7 +483,7 @@ def mkAtom (aig : AIG α) (n : α) : Entrypoint α :=
   let cache := aig.cache.noUpdate
   have invariant := by
     intro i lhs rhs linv rinv h1 h2
-    simp only [Array.get_push] at h2
+    simp only [Array.getElem_push] at h2
     split at h2
     · apply aig.invariant <;> assumption
     · contradiction
@@ -499,7 +499,7 @@ def mkConst (aig : AIG α) (val : Bool) : Entrypoint α :=
   let cache := aig.cache.noUpdate
   have invariant := by
     intro i lhs rhs linv rinv h1 h2
-    simp only [Array.get_push] at h2
+    simp only [Array.getElem_push] at h2
     split at h2
     · apply aig.invariant <;> assumption
     · contradiction
diff --git a/src/Std/Sat/AIG/Cached.lean b/src/Std/Sat/AIG/Cached.lean
index 18b9d30e56..8537c6f07c 100644
--- a/src/Std/Sat/AIG/Cached.lean
+++ b/src/Std/Sat/AIG/Cached.lean
@@ -36,7 +36,7 @@ def mkAtomCached (aig : AIG α) (n : α) : Entrypoint α :=
     let decls := decls.push decl
     have inv := by
       intro i lhs rhs linv rinv h1 h2
-      simp only [Array.get_push] at h2
+      simp only [Array.getElem_push] at h2
       split at h2
       · apply inv <;> assumption
       · contradiction
@@ -58,7 +58,7 @@ def mkConstCached (aig : AIG α) (val : Bool) : Entrypoint α :=
     let decls := decls.push decl
     have inv := by
       intro i lhs rhs linv rinv h1 h2
-      simp only [Array.get_push] at h2
+      simp only [Array.getElem_push] at h2
       split at h2
       · apply inv <;> assumption
       · contradiction
@@ -121,7 +121,7 @@ where
           have inv := by
             intro i lhs rhs linv rinv h1 h2
             simp only [decls] at *
-            simp only [Array.get_push] at h2
+            simp only [Array.getElem_push] at h2
             split at h2
             · apply inv <;> assumption
             · injections; omega
diff --git a/src/Std/Sat/AIG/CachedLemmas.lean b/src/Std/Sat/AIG/CachedLemmas.lean
index 29d5184048..e213960d47 100644
--- a/src/Std/Sat/AIG/CachedLemmas.lean
+++ b/src/Std/Sat/AIG/CachedLemmas.lean
@@ -60,7 +60,7 @@ theorem mkAtomCached_decl_eq (aig : AIG α) (var : α) (idx : Nat) {h : idx < ai
     simp [this]
   | none =>
     have := mkAtomCached_miss_aig aig hcache
-    simp only [this, Array.get_push]
+    simp only [this, Array.getElem_push]
     split
     · rfl
     · contradiction
@@ -134,7 +134,7 @@ theorem mkConstCached_decl_eq (aig : AIG α) (val : Bool) (idx : Nat) {h : idx <
     simp [this]
   | none =>
     have := mkConstCached_miss_aig aig hcache
-    simp only [this, Array.get_push]
+    simp only [this, Array.getElem_push]
     split
     · rfl
     · contradiction
@@ -257,7 +257,7 @@ theorem mkGateCached.go_decl_eq (aig : AIG α) (input : GateInput aig) :
           · rw [← hres]
             dsimp only
             intro idx h1 h2
-            rw [Array.get_push]
+            rw [Array.getElem_push]
             simp [h2]
 
 /--
diff --git a/src/Std/Sat/AIG/Lemmas.lean b/src/Std/Sat/AIG/Lemmas.lean
index afde41c6da..c8c1f5f53c 100644
--- a/src/Std/Sat/AIG/Lemmas.lean
+++ b/src/Std/Sat/AIG/Lemmas.lean
@@ -78,7 +78,7 @@ The AIG produced by `AIG.mkGate` agrees with the input AIG on all indices that a
 theorem mkGate_decl_eq idx (aig : AIG α) (input : GateInput aig) {h : idx < aig.decls.size} :
     have := mkGate_le_size aig input
     (aig.mkGate input).aig.decls[idx]'(by omega) = aig.decls[idx] := by
-  simp only [mkGate, Array.get_push]
+  simp only [mkGate, Array.getElem_push]
   split
   · rfl
   · contradiction
@@ -99,13 +99,13 @@ theorem denote_mkGate {aig : AIG α} {input : GateInput aig} :
     unfold denote denote.go
   split
   · next heq =>
-    rw [mkGate, Array.get_push_eq] at heq
+    rw [mkGate, Array.getElem_push_eq] at heq
     contradiction
   · next heq =>
-    rw [mkGate, Array.get_push_eq] at heq
+    rw [mkGate, Array.getElem_push_eq] at heq
     contradiction
   · next heq =>
-    rw [mkGate, Array.get_push_eq] at heq
+    rw [mkGate, Array.getElem_push_eq] at heq
     injection heq with heq1 heq2 heq3 heq4
     dsimp only
     congr 2
@@ -132,7 +132,7 @@ The AIG produced by `AIG.mkAtom` agrees with the input AIG on all indices that a
 -/
 theorem mkAtom_decl_eq (aig : AIG α) (var : α) (idx : Nat) {h : idx < aig.decls.size} {hbound} :
     (aig.mkAtom var).aig.decls[idx]'hbound = aig.decls[idx] := by
-  simp only [mkAtom, Array.get_push]
+  simp only [mkAtom, Array.getElem_push]
   split
   · rfl
   · contradiction
@@ -149,14 +149,14 @@ theorem denote_mkAtom {aig : AIG α} :
   unfold denote denote.go
   split
   · next heq =>
-    rw [mkAtom, Array.get_push_eq] at heq
+    rw [mkAtom, Array.getElem_push_eq] at heq
     contradiction
   · next heq =>
-    rw [mkAtom, Array.get_push_eq] at heq
+    rw [mkAtom, Array.getElem_push_eq] at heq
     injection heq with heq
     rw [heq]
   · next heq =>
-    rw [mkAtom, Array.get_push_eq] at heq
+    rw [mkAtom, Array.getElem_push_eq] at heq
     contradiction
 
 /--
@@ -172,7 +172,7 @@ The AIG produced by `AIG.mkConst` agrees with the input AIG on all indices that
 theorem mkConst_decl_eq (aig : AIG α) (val : Bool) (idx : Nat) {h : idx < aig.decls.size} :
     have := mkConst_le_size aig val
     (aig.mkConst val).aig.decls[idx]'(by omega) = aig.decls[idx] := by
-  simp only [mkConst, Array.get_push]
+  simp only [mkConst, Array.getElem_push]
   split
   · rfl
   · contradiction
@@ -188,14 +188,14 @@ theorem denote_mkConst {aig : AIG α} : ⟦(aig.mkConst val), assign⟧ = val :=
   unfold denote denote.go
   split
   · next heq =>
-    rw [mkConst, Array.get_push_eq] at heq
+    rw [mkConst, Array.getElem_push_eq] at heq
     injection heq with heq
     rw [heq]
   · next heq =>
-    rw [mkConst, Array.get_push_eq] at heq
+    rw [mkConst, Array.getElem_push_eq] at heq
     contradiction
   · next heq =>
-    rw [mkConst, Array.get_push_eq] at heq
+    rw [mkConst, Array.getElem_push_eq] at heq
     contradiction
 
 /--
diff --git a/src/Std/Sat/AIG/RefVec.lean b/src/Std/Sat/AIG/RefVec.lean
index 4f02242dde..fe7d2146b2 100644
--- a/src/Std/Sat/AIG/RefVec.lean
+++ b/src/Std/Sat/AIG/RefVec.lean
@@ -59,7 +59,7 @@ def push (s : RefVec aig len) (ref : AIG.Ref aig) : RefVec aig (len + 1) :=
     by simp [hlen],
     by
       intro i hi
-      simp only [Array.get_push]
+      simp only [Array.getElem_push]
       split
       · apply hrefs
         omega
@@ -85,7 +85,7 @@ theorem get_push_ref_lt (s : RefVec aig len) (ref : AIG.Ref aig) (idx : Nat)
   simp only [get, push, Ref.mk.injEq]
   cases ref
   simp only [Ref.mk.injEq]
-  rw [Array.get_push_lt]
+  rw [Array.getElem_push_lt]
 
 @[simp]
 theorem get_cast {aig1 aig2 : AIG α} (s : RefVec aig1 len) (idx : Nat) (hidx : idx < len)
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
index 9f8b50a9c1..3903da25e3 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
@@ -111,7 +111,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
           ⟨units.size, units_size_lt_updatedUnits_size⟩
         have i_gt_zero : i.1 > 0 := by rw [i_eq_l]; exact l.1.2.1
         refine ⟨mostRecentUnitIdx, l.2, i_gt_zero, ?_⟩
-        simp only [insertUnit, h3, ite_false, Array.get_push_eq, i_eq_l, reduceCtorEq]
+        simp only [insertUnit, h3, ite_false, Array.getElem_push_eq, i_eq_l, reduceCtorEq]
         constructor
         · rfl
         · constructor
@@ -132,7 +132,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                 · intro h
                   simp only [← h, not_true, mostRecentUnitIdx] at hk
                   exact hk rfl
-              rw [Array.get_push_lt _ _ _ k_in_bounds]
+              rw [Array.getElem_push_lt _ _ _ k_in_bounds]
               rw [i_eq_l] at h2
               exact h2 ⟨k.1, k_in_bounds⟩
       · next i_ne_l =>
@@ -142,7 +142,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
         constructor
         · exact h1
         · intro j
-          rw [Array.get_push]
+          rw [Array.getElem_push]
           by_cases h : j.val < Array.size units
           · simp only [h, dite_true]
             exact h2 ⟨j.1, h⟩
@@ -189,9 +189,9 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
           exact h5 (has_add _ true)
         | true, false =>
           refine ⟨⟨j.1, j_lt_updatedUnits_size⟩, mostRecentUnitIdx, i_gt_zero, ?_⟩
-          simp only [insertUnit, h5, ite_false, Array.get_push_eq, ne_eq, reduceCtorEq]
+          simp only [insertUnit, h5, ite_false, Array.getElem_push_eq, ne_eq, reduceCtorEq]
           constructor
-          · rw [Array.get_push_lt units l j.1 j.2, h1]
+          · rw [Array.getElem_push_lt units l j.1 j.2, h1]
           · constructor
             · simp [i_eq_l, ← hl]
               rfl
@@ -210,7 +210,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                     simp [hasAssignment, hl, getElem!, l_in_bounds, h2, hasNegAssignment, decidableGetElem?] at h5
                   | both => simp (config := {decide := true}) only [h] at h3
                 · intro k k_ne_j k_ne_l
-                  rw [Array.get_push]
+                  rw [Array.getElem_push]
                   by_cases h : k.1 < units.size
                   · simp only [h, dite_true]
                     have k_ne_j : ⟨k.1, h⟩ ≠ j := by
@@ -226,12 +226,12 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                       exact k_ne_l rfl
         | false, true =>
           refine ⟨mostRecentUnitIdx, ⟨j.1, j_lt_updatedUnits_size⟩, i_gt_zero, ?_⟩
-          simp [insertUnit, h5, ite_false, Array.get_push_eq, ne_eq]
+          simp [insertUnit, h5, ite_false, Array.getElem_push_eq, ne_eq]
           constructor
           · simp [i_eq_l, ← hl]
             rfl
           · constructor
-            · rw [Array.get_push_lt units l j.1 j.2, h1]
+            · rw [Array.getElem_push_lt units l j.1 j.2, h1]
             · constructor
               · simp only [i_eq_l]
                 rw [Array.getElem_modify_self]
@@ -247,7 +247,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                   | neg  => simp (config := {decide := true}) only [h] at h3
                   | both => simp (config := {decide := true}) only [h] at h3
                 · intro k k_ne_l k_ne_j
-                  rw [Array.get_push]
+                  rw [Array.getElem_push]
                   by_cases h : k.1 < units.size
                   · simp only [h, dite_true]
                     have k_ne_j : ⟨k.1, h⟩ ≠ j := by
@@ -275,13 +275,13 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
         refine ⟨⟨j.1, j_lt_updatedUnits_size⟩, b,i_gt_zero, ?_⟩
         simp only [insertUnit, h5, ite_false, reduceCtorEq]
         constructor
-        · rw [Array.get_push_lt units l j.1 j.2, h1]
+        · rw [Array.getElem_push_lt units l j.1 j.2, h1]
         · constructor
           · rw [Array.getElem_modify_of_ne (Ne.symm i_ne_l), h2]
           · constructor
             · exact h3
             · intro k k_ne_j
-              rw [Array.get_push]
+              rw [Array.getElem_push]
               by_cases h : k.val < units.size
               · simp only [h, dite_true]
                 have k_ne_j : ⟨k.1, h⟩ ≠ j := by
@@ -307,11 +307,11 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
     constructor
     · split
       · exact h1
-      · simp only [Array.get_push_lt units l j1.1 j1.2, h1]
+      · simp only [Array.getElem_push_lt units l j1.1 j1.2, h1]
     · constructor
       · split
         · exact h2
-        · simp only [Array.get_push_lt units l j2.1 j2.2, h2]
+        · simp only [Array.getElem_push_lt units l j2.1 j2.2, h2]
       · constructor
         · split
           · exact h3
@@ -336,7 +336,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
               split
               · exact h5 ⟨k.1, k_in_bounds⟩ k_ne_j1 k_ne_j2
               · simp only [ne_eq]
-                rw [Array.get_push]
+                rw [Array.getElem_push]
                 simp only [k_in_bounds, dite_true]
                 exact h5 ⟨k.1, k_in_bounds⟩ k_ne_j1 k_ne_j2
             · next k_not_lt_units_size =>
@@ -354,7 +354,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                   rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ k_property with k_lt_units_size | k_eq_units_size
                   · exfalso; exact k_not_lt_units_size k_lt_units_size
                   · exact k_eq_units_size
-                simp only [k_eq_units_size, Array.get_push_eq, ne_eq]
+                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
 
diff --git a/tests/lean/simpArrayIdx.lean b/tests/lean/simpArrayIdx.lean
index abcd0d5a41..b31b3e642f 100644
--- a/tests/lean/simpArrayIdx.lean
+++ b/tests/lean/simpArrayIdx.lean
@@ -10,7 +10,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 ~> if i < a.size then v else default
+#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