chore: add TODO for offset equalities

src/Init/Data/Array/Attach.lean

@@ -69,11 +69,11 @@ well-founded recursion mechanism to prove that the function terminates.
   simp [pmap]
 
 @[simp] theorem toList_attachWith {xs : Array α} {P : α → Prop} {H : ∀ x ∈ xs, P x} :
-   (xs.attachWith P H).toList = xs.toList.attachWith P (by simpa [mem_toList_iff] using H) := by
+   (xs.attachWith P H).toList = xs.toList.attachWith P (by simpa [mem_toList] using H) := by
   simp [attachWith]
 
 @[simp] theorem toList_attach {xs : Array α} :
-    xs.attach.toList = xs.toList.attachWith (· ∈ xs) (by simp [mem_toList_iff]) := by
+    xs.attach.toList = xs.toList.attachWith (· ∈ xs) (by simp [mem_toList]) := by
   simp [attach]
 
 @[simp] theorem toList_pmap {xs : Array α} {P : α → Prop} {f : ∀ a, P a → β} {H : ∀ a ∈ xs, P a} :
@@ -574,12 +574,9 @@ state, the right approach is usually the tactic `simp [Array.unattach, -Array.ma
 -/
 def unattach {α : Type _} {p : α → Prop} (xs : Array { x // p x }) : Array α := xs.map (·.val)
 
-@[simp] theorem unattach_empty {p : α → Prop} : (#[] : Array { x // p x }).unattach = #[] := by
+@[simp] theorem unattach_nil {p : α → Prop} : (#[] : Array { x // p x }).unattach = #[] := by
   simp [unattach]
 
-@[deprecated unattach_empty (since := "2025-05-26")]
-abbrev unattach_nil := @unattach_empty
-
 @[simp] theorem unattach_push {p : α → Prop} {a : { x // p x }} {xs : Array { x // p x }} :
     (xs.push a).unattach = xs.unattach.push a.1 := by
   simp only [unattach, Array.map_push]

src/Init/Data/Array/Basic.lean

@@ -331,14 +331,12 @@ Examples:
  * `Array.ofFn (n := 3) toString = #["0", "1", "2"]`
  * `Array.ofFn (fun i => #["red", "green", "blue"].get i.val i.isLt) = #["red", "green", "blue"]`
 -/
-def ofFn {n} (f : Fin n → α) : Array α := go (emptyWithCapacity n) n (Nat.le_refl n) where
-  /-- Auxiliary for `ofFn`. `ofFn.go f acc i h = acc ++ #[f (n - i), ..., f(n - 1)]` -/
-  go (acc : Array α) : (i : Nat) → i ≤ n → Array α
-  | i + 1, h =>
-     have w : n - i - 1 < n :=
-       Nat.lt_of_lt_of_le (Nat.sub_one_lt (Nat.sub_ne_zero_iff_lt.mpr h)) (Nat.sub_le n i)
-     go (acc.push (f ⟨n - i - 1, w⟩)) i (Nat.le_of_succ_le h)
-  | 0, _ => acc
+def ofFn {n} (f : Fin n → α) : Array α := go 0 (emptyWithCapacity n) where
+  /-- Auxiliary for `ofFn`. `ofFn.go f i acc = acc ++ #[f i, ..., f(n - 1)]` -/
+  @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+  go (i : Nat) (acc : Array α) : Array α :=
+    if h : i < n then go (i+1) (acc.push (f ⟨i, h⟩)) else acc
+  decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 -- See also `Array.ofFnM` defined in `Init.Data.Array.OfFn`.
 

src/Init/Data/Array/Bootstrap.lean

@@ -89,13 +89,9 @@ theorem foldrM_eq_reverse_foldlM_toList [Monad m] {f : α → β → m β} {init
     xs.toList.foldr f init = xs.foldr f init :=
   List.foldr_eq_foldrM .. ▸ foldrM_toList ..
 
-@[simp, grind =] theorem toList_push {xs : Array α} {x : α} : (xs.push x).toList = xs.toList ++ [x] := by
-  rcases xs with ⟨xs⟩
+@[simp, grind =] theorem push_toList {xs : Array α} {a : α} : (xs.push a).toList = xs.toList ++ [a] := by
   simp [push, List.concat_eq_append]
 
-@[deprecated toList_push (since := "2025-05-26")]
-abbrev push_toList := @toList_push
-
 @[simp, grind =] theorem toListAppend_eq {xs : Array α} {l : List α} : xs.toListAppend l = xs.toList ++ l := by
   simp [toListAppend, ← foldr_toList]
 

src/Init/Data/Array/Count.lean

@@ -52,8 +52,8 @@ theorem countP_push {a : α} {xs : Array α} : countP p (xs.push a) = countP p x
   rcases xs with ⟨xs⟩
   simp_all
 
-theorem countP_singleton {a : α} : countP p #[a] = if p a then 1 else 0 := by
-  simp
+@[simp] theorem countP_singleton {a : α} : countP p #[a] = if p a then 1 else 0 := by
+  simp [countP_push]
 
 theorem size_eq_countP_add_countP {xs : Array α} : xs.size = countP p xs + countP (fun a => ¬p a) xs := by
   rcases xs with ⟨xs⟩

src/Init/Data/Array/Erase.lean

@@ -24,7 +24,7 @@ open Nat
 
 /-! ### eraseP -/
 
-theorem eraseP_empty : #[].eraseP p = #[] := by simp
+@[simp] theorem eraseP_empty : #[].eraseP p = #[] := by simp
 
 theorem eraseP_of_forall_mem_not {xs : Array α} (h : ∀ a, a ∈ xs → ¬p a) : xs.eraseP p = xs := by
   rcases xs with ⟨xs⟩

src/Init/Data/Array/Extract.lean

@@ -238,9 +238,11 @@ theorem extract_append_left {as bs : Array α} :
     (as ++ bs).extract 0 as.size = as.extract 0 as.size := by
   simp
 
-theorem extract_append_right {as bs : Array α} :
+@[simp] theorem extract_append_right {as bs : Array α} :
     (as ++ bs).extract as.size (as.size + i) = bs.extract 0 i := by
-  simp
+  simp only [extract_append, extract_size_left, Nat.sub_self, empty_append]
+  congr 1
+  omega
 
 @[simp] theorem map_extract {as : Array α} {i j : Nat} :
     (as.extract i j).map f = (as.map f).extract i j := by

src/Init/Data/Array/Find.lean

@@ -142,9 +142,9 @@ abbrev findSome?_mkArray_of_isNone := @findSome?_replicate_of_isNone
 
 @[simp] theorem find?_empty : find? p #[] = none := rfl
 
-theorem find?_singleton {a : α} {p : α → Bool} :
+@[simp] theorem find?_singleton {a : α} {p : α → Bool} :
     #[a].find? p = if p a then some a else none := by
-  simp
+  simp [singleton_eq_toArray_singleton]
 
 @[simp] theorem findRev?_push_of_pos {xs : Array α} (h : p a) :
     findRev? p (xs.push a) = some a := by
@@ -347,8 +347,7 @@ theorem find?_eq_some_iff_getElem {xs : Array α} {p : α → Bool} {b : α} :
 
 /-! ### findIdx -/
 
-theorem findIdx_empty : findIdx p #[] = 0 := rfl
-
+@[simp] theorem findIdx_empty : findIdx p #[] = 0 := rfl
 theorem findIdx_singleton {a : α} {p : α → Bool} :
     #[a].findIdx p = if p a then 0 else 1 := by
   simp
@@ -601,8 +600,7 @@ theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : Array α} {p q : α → Bo
 
 /-! ### findFinIdx? -/
 
-theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := by simp
-
+@[simp] theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := by simp
 theorem findFinIdx?_singleton {a : α} {p : α → Bool} :
     #[a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by
   simp
@@ -701,7 +699,7 @@ The verification API for `idxOf?` is still incomplete.
 The lemmas below should be made consistent with those for `findIdx?` (and proved using them).
 -/
 
-theorem idxOf?_empty [BEq α] : (#[] : Array α).idxOf? a = none := by simp
+@[simp] theorem idxOf?_empty [BEq α] : (#[] : Array α).idxOf? a = none := by simp
 
 @[simp] theorem idxOf?_eq_none_iff [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     xs.idxOf? a = none ↔ a ∉ xs := by
@@ -714,10 +712,14 @@ theorem isSome_idxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
   rcases xs with ⟨xs⟩
   simp
 
+@[simp]
 theorem isNone_idxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     (xs.idxOf? a).isNone = ¬ a ∈ xs := by
+  rcases xs with ⟨xs⟩
   simp
 
+
+
 /-! ### finIdxOf?
 
 The verification API for `finIdxOf?` is still incomplete.
@@ -728,7 +730,7 @@ theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : Array α} {a : α} :
     xs.idxOf? a = (xs.finIdxOf? a).map (·.val) := by
   simp [idxOf?, finIdxOf?, findIdx?_eq_map_findFinIdx?_val]
 
-theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by simp
+@[simp] theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by simp
 
 @[simp] theorem finIdxOf?_eq_none_iff [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     xs.finIdxOf? a = none ↔ a ∉ xs := by
@@ -746,8 +748,10 @@ theorem isSome_finIdxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
   rcases xs with ⟨xs⟩
   simp
 
+@[simp]
 theorem isNone_finIdxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     (xs.finIdxOf? a).isNone = ¬ a ∈ xs := by
+  rcases xs with ⟨xs⟩
   simp
 
 end Array

src/Init/Data/Array/Lemmas.lean

@@ -140,13 +140,13 @@ theorem getElem_of_getElem? {xs : Array α} : xs[i]? = some a → ∃ h : i < xs
 theorem some_eq_getElem?_iff {xs : Array α} : some b = xs[i]? ↔ ∃ h : i < xs.size, xs[i] = b := by
   rw [eq_comm, getElem?_eq_some_iff]
 
-theorem some_getElem_eq_getElem?_iff (xs : Array α) (i : Nat) (h : i < xs.size) :
+@[simp] theorem some_getElem_eq_getElem?_iff (xs : Array α) (i : Nat) (h : i < xs.size) :
     (some xs[i] = xs[i]?) ↔ True := by
-  simp
+  simp [h]
 
-theorem getElem?_eq_some_getElem_iff (xs : Array α) (i : Nat) (h : i < xs.size) :
+@[simp] theorem getElem?_eq_some_getElem_iff (xs : Array α) (i : Nat) (h : i < xs.size) :
     (xs[i]? = some xs[i]) ↔ True := by
-  simp
+  simp [h]
 
 theorem getElem_eq_iff {xs : Array α} {i : Nat} {h : i < xs.size} : xs[i] = x ↔ xs[i]? = some x := by
   simp only [getElem?_eq_some_iff]
@@ -186,11 +186,12 @@ theorem getElem?_push {xs : Array α} {x} : (xs.push x)[i]? = if i = xs.size the
   simp [getElem?_def, getElem_push]
   (repeat' split) <;> first | rfl | omega
 
-theorem getElem?_push_size {xs : Array α} {x} : (xs.push x)[xs.size]? = some x := by
-  simp
+@[simp] theorem getElem?_push_size {xs : Array α} {x} : (xs.push x)[xs.size]? = some x := by
+  simp [getElem?_push]
 
-theorem getElem_singleton {a : α} {i : Nat} (h : i < 1) : #[a][i] = a := by
-  simp
+@[simp] theorem getElem_singleton {a : α} {i : Nat} (h : i < 1) : #[a][i] = a :=
+  match i, h with
+  | 0, _ => rfl
 
 @[grind]
 theorem getElem?_singleton {a : α} {i : Nat} : #[a][i]? = if i = 0 then some a else none := by
@@ -239,6 +240,10 @@ theorem back?_pop {xs : Array α} :
 
 @[simp] theorem push_empty : #[].push x = #[x] := rfl
 
+@[simp] theorem toList_push {xs : Array α} {x : α} : (xs.push x).toList = xs.toList ++ [x] := by
+  rcases xs with ⟨xs⟩
+  simp
+
 @[simp] theorem push_ne_empty {a : α} {xs : Array α} : xs.push a ≠ #[] := by
   cases xs
   simp
@@ -418,7 +423,8 @@ theorem eq_empty_iff_forall_not_mem {xs : Array α} : xs = #[] ↔ ∀ a, a ∉
 theorem eq_of_mem_singleton (h : a ∈ #[b]) : a = b := by
   simpa using h
 
-theorem mem_singleton {a b : α} : a ∈ #[b] ↔ a = b := by simp
+@[simp] theorem mem_singleton {a b : α} : a ∈ #[b] ↔ a = b :=
+  ⟨eq_of_mem_singleton, (by simp [·])⟩
 
 theorem forall_mem_push {p : α → Prop} {xs : Array α} {a : α} :
     (∀ x, x ∈ xs.push a → p x) ↔ p a ∧ ∀ x, x ∈ xs → p x := by
@@ -862,8 +868,8 @@ theorem elem_eq_mem [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
 @[simp, grind] theorem contains_eq_mem [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
     xs.contains a = decide (a ∈ xs) := by rw [← elem_eq_contains, elem_eq_mem]
 
-@[grind] theorem any_empty [BEq α] {p : α → Bool} : (#[] : Array α).any p = false := by simp
-@[grind] theorem all_empty [BEq α] {p : α → Bool} : (#[] : Array α).all p = true := by simp
+@[simp, grind] theorem any_empty [BEq α] {p : α → Bool} : (#[] : Array α).any p = false := by simp
+@[simp, grind] theorem all_empty [BEq α] {p : α → Bool} : (#[] : Array α).all p = true := by simp
 
 /-- Variant of `any_push` with a side condition on `stop`. -/
 @[simp, grind] theorem any_push' [BEq α] {xs : Array α} {a : α} {p : α → Bool} (h : stop = xs.size + 1) :
@@ -1222,7 +1228,7 @@ where
 @[simp] theorem mapM_empty [Monad m] (f : α → m β) : mapM f #[] = pure #[] := by
   rw [mapM, mapM.map]; rfl
 
-@[grind] theorem map_empty {f : α → β} : map f #[] = #[] := by simp
+@[simp, grind] theorem map_empty {f : α → β} : map f #[] = #[] := mapM_empty f
 
 @[simp, grind] theorem map_push {f : α → β} {as : Array α} {x : α} :
     (as.push x).map f = (as.map f).push (f x) := by
@@ -1807,8 +1813,7 @@ theorem toArray_append {xs : List α} {ys : Array α} :
 
 theorem singleton_eq_toArray_singleton {a : α} : #[a] = [a].toArray := rfl
 
-@[deprecated empty_append (since := "2025-05-26")]
-theorem empty_append_fun : ((#[] : Array α) ++ ·) = id := by
+@[simp] theorem empty_append_fun : ((#[] : Array α) ++ ·) = id := by
   funext ⟨l⟩
   simp
 
@@ -1959,8 +1964,8 @@ theorem append_left_inj {xs₁ xs₂ : Array α} (ys) : xs₁ ++ ys = xs₂ ++ y
 theorem eq_empty_of_append_eq_empty {xs ys : Array α} (h : xs ++ ys = #[]) : xs = #[] ∧ ys = #[] :=
   append_eq_empty_iff.mp h
 
-theorem empty_eq_append_iff {xs ys : Array α} : #[] = xs ++ ys ↔ xs = #[] ∧ ys = #[] := by
-  simp
+@[simp] theorem empty_eq_append_iff {xs ys : Array α} : #[] = xs ++ ys ↔ xs = #[] ∧ ys = #[] := by
+  rw [eq_comm, append_eq_empty_iff]
 
 theorem append_ne_empty_of_left_ne_empty {xs ys : Array α} (h : xs ≠ #[]) : xs ++ ys ≠ #[] := by
   simp_all
@@ -2028,7 +2033,7 @@ theorem append_eq_append_iff {ws xs ys zs : Array α} :
   simp only [List.append_toArray, List.set_toArray, List.set_append]
   split <;> simp
 
-@[simp] theorem set_append_left {xs ys : Array α} {i : Nat} {x : α} (h : i < xs.size)  :
+@[simp] theorem set_append_left {xs ys : Array α} {i : Nat} {x : α} (h : i < xs.size) :
     (xs ++ ys).set i x (by simp; omega) = xs.set i x ++ ys := by
   simp [set_append, h]
 
@@ -2103,13 +2108,14 @@ theorem append_eq_map_iff {f : α → β} :
   | nil => simp
   | cons as => induction as.toList <;> simp [*]
 
-@[simp] theorem flatten_toArray_map {L : List (List α)} :
-    (L.map List.toArray).toArray.flatten = L.flatten.toArray := by
+@[simp] theorem flatten_map_toArray {L : List (List α)} :
+    (L.toArray.map List.toArray).flatten = L.flatten.toArray := by
   apply ext'
   simp [Function.comp_def]
 
-theorem flatten_map_toArray {L : List (List α)} :
-    (L.toArray.map List.toArray).flatten = L.flatten.toArray := by
+@[simp] theorem flatten_toArray_map {L : List (List α)} :
+    (L.map List.toArray).toArray.flatten = L.flatten.toArray := by
+  rw [← flatten_map_toArray]
   simp
 
 -- We set this to lower priority so that `flatten_toArray_map` is applied first when relevant.
@@ -2137,8 +2143,8 @@ theorem mem_flatten : ∀ {xss : Array (Array α)}, a ∈ xss.flatten ↔ ∃ xs
   induction xss using array₂_induction
   simp
 
-theorem empty_eq_flatten_iff {xss : Array (Array α)} : #[] = xss.flatten ↔ ∀ xs ∈ xss, xs = #[] := by
-  simp
+@[simp] theorem empty_eq_flatten_iff {xss : Array (Array α)} : #[] = xss.flatten ↔ ∀ xs ∈ xss, xs = #[] := by
+  rw [eq_comm, flatten_eq_empty_iff]
 
 theorem flatten_ne_empty_iff {xss : Array (Array α)} : xss.flatten ≠ #[] ↔ ∃ xs, xs ∈ xss ∧ xs ≠ #[] := by
   simp
@@ -2278,9 +2284,15 @@ theorem eq_iff_flatten_eq {xss₁ xss₂ : Array (Array α)} :
       rw [List.map_inj_right]
       simp +contextual
 
-theorem flatten_toArray_map_toArray {xss : List (List α)} :
+@[simp] theorem flatten_toArray_map_toArray {xss : List (List α)} :
     (xss.map List.toArray).toArray.flatten = xss.flatten.toArray := by
-  simp
+  simp [flatten]
+  suffices ∀ as, List.foldl (fun acc bs => acc ++ bs) as (List.map List.toArray xss) = as ++ xss.flatten.toArray by
+    simpa using this #[]
+  intro as
+  induction xss generalizing as with
+  | nil => simp
+  | cons xs xss ih => simp [ih]
 
 /-! ### flatMap -/
 
@@ -2310,9 +2322,13 @@ theorem flatMap_toArray_cons {β} {f : α → Array β} {a : α} {as : List α}
   intro cs
   induction as generalizing cs <;> simp_all
 
-theorem flatMap_toArray {β} {f : α → Array β} {as : List α} :
+@[simp, grind =] theorem flatMap_toArray {β} {f : α → Array β} {as : List α} :
     as.toArray.flatMap f = (as.flatMap (fun a => (f a).toList)).toArray := by
-  simp
+  induction as with
+  | nil => simp
+  | cons a as ih =>
+    apply ext'
+    simp [ih, flatMap_toArray_cons]
 
 @[simp] theorem flatMap_id {xss : Array (Array α)} : xss.flatMap id = xss.flatten := by simp [flatMap_def]
 
@@ -3014,21 +3030,19 @@ theorem take_size {xs : Array α} : xs.take xs.size = xs := by
   | succ n ih =>
     simp [shrink.loop, ih]
 
--- This doesn't need to be a simp lemma, as shortly we will simplify `shrink` to `take`.
-theorem size_shrink {xs : Array α} {i : Nat} : (xs.shrink i).size = min i xs.size := by
+@[simp] theorem size_shrink {xs : Array α} {i : Nat} : (xs.shrink i).size = min i xs.size := by
   simp [shrink]
   omega
 
--- This doesn't need to be a simp lemma, as shortly we will simplify `shrink` to `take`.
-theorem getElem_shrink {xs : Array α} {i j : Nat} (h : j < (xs.shrink i).size) :
-    (xs.shrink i)[j] = xs[j]'(by simp [size_shrink] at h; omega) := by
+@[simp] theorem getElem_shrink {xs : Array α} {i j : Nat} (h : j < (xs.shrink i).size) :
+    (xs.shrink i)[j] = xs[j]'(by simp at h; omega) := by
   simp [shrink]
 
-@[simp] theorem shrink_eq_take {xs : Array α} {i : Nat} : xs.shrink i = xs.take i := by
-  ext <;> simp [size_shrink, getElem_shrink]
+@[simp] theorem toList_shrink {xs : Array α} {i : Nat} : (xs.shrink i).toList = xs.toList.take i := by
+  apply List.ext_getElem <;> simp
 
-theorem toList_shrink {xs : Array α} {i : Nat} : (xs.shrink i).toList = xs.toList.take i := by
-  simp
+@[simp] theorem shrink_eq_take {xs : Array α} {i : Nat} : xs.shrink i = xs.take i := by
+  ext <;> simp
 
 /-! ### foldlM and foldrM -/
 
@@ -3235,7 +3249,7 @@ theorem foldrM_reverse [Monad m] {xs : Array α} {f : α → β → m β} {b} :
 
 theorem foldrM_push [Monad m] {f : α → β → m β} {init : β} {xs : Array α} {a : α} :
     (xs.push a).foldrM f init = f a init >>= xs.foldrM f := by
-  simp only [foldrM_eq_reverse_foldlM_toList, toList_push, List.reverse_append, List.reverse_cons,
+  simp only [foldrM_eq_reverse_foldlM_toList, push_toList, List.reverse_append, List.reverse_cons,
     List.reverse_nil, List.nil_append, List.singleton_append, List.foldlM_cons, List.foldlM_reverse]
 
 /--
@@ -3640,7 +3654,7 @@ theorem foldr_rel {xs : Array α} {f g : α → β → β} {a b : β} {r : β
 theorem back?_eq_some_iff {xs : Array α} {a : α} :
     xs.back? = some a ↔ ∃ ys : Array α, xs = ys.push a := by
   rcases xs with ⟨xs⟩
-  simp only [List.back?_toArray, List.getLast?_eq_some_iff, toArray_eq, toList_push]
+  simp only [List.back?_toArray, List.getLast?_eq_some_iff, toArray_eq, push_toList]
   constructor
   · rintro ⟨ys, rfl⟩
     exact ⟨ys.toArray, by simp⟩
@@ -4285,44 +4299,42 @@ Examples:
 
 /-! ### Preliminaries about `ofFn` -/
 
-@[simp] theorem size_ofFn_go {n} {f : Fin n → α} {i acc h} :
-    (ofFn.go f acc i h).size = acc.size + i := by
-  induction i generalizing acc with
-  | zero => simp [ofFn.go]
-  | succ i ih =>
-    simpa [ofFn.go, ih] using Nat.succ_add_eq_add_succ acc.size i
+@[simp] theorem size_ofFn_go {n} {f : Fin n → α} {i acc} :
+    (ofFn.go f i acc).size = acc.size + (n - i) := by
+  if hin : i < n then
+    unfold ofFn.go
+    have : 1 + (n - (i + 1)) = n - i :=
+      Nat.sub_sub .. ▸ Nat.add_sub_cancel' (Nat.le_sub_of_add_le (Nat.add_comm .. ▸ hin))
+    rw [dif_pos hin, size_ofFn_go, size_push, Nat.add_assoc, this]
+  else
+    have : n - i = 0 := Nat.sub_eq_zero_of_le (Nat.le_of_not_lt hin)
+    unfold ofFn.go
+    simp [hin, this]
+termination_by n - i
 
 @[simp] theorem size_ofFn {n : Nat} {f : Fin n → α} : (ofFn f).size = n := by simp [ofFn]
 
--- Recall `ofFn.go f acc i h = acc ++ #[f (n - i), ..., f(n - 1)]`
-theorem getElem_ofFn_go {f : Fin n → α} {acc i k} (h : i ≤ n) (w₁ : k < acc.size + i) :
-    (ofFn.go f acc i h)[k]'(by simpa using w₁) =
-      if w₂ : k < acc.size then acc[k] else f ⟨n - i + k - acc.size, by omega⟩ := by
-  induction i generalizing acc k with
-  | zero =>
-    simp at w₁
-    simp_all [ofFn.go]
-  | succ i ih =>
-    unfold ofFn.go
-    rw [ih]
-    · simp only [size_push]
-      split <;> rename_i h'
-      · rw [Array.getElem_push]
-        split
-        · rfl
-        · congr 2
-          omega
-      · split
-        · omega
-        · congr 2
-          omega
-    · simp
-      omega
+theorem getElem_ofFn_go {f : Fin n → α} {i} {acc k}
+    (hki : k < n) (hin : i ≤ n) (hi : i = acc.size)
+    (hacc : ∀ j, ∀ hj : j < acc.size, acc[j] = f ⟨j, Nat.lt_of_lt_of_le hj (hi ▸ hin)⟩) :
+    haveI : acc.size + (n - acc.size) = n := Nat.add_sub_cancel' (hi ▸ hin)
+    (ofFn.go f i acc)[k]'(by simp [*]) = f ⟨k, hki⟩ := by
+  unfold ofFn.go
+  if hin : i < n then
+    have : 1 + (n - (i + 1)) = n - i :=
+      Nat.sub_sub .. ▸ Nat.add_sub_cancel' (Nat.le_sub_of_add_le (Nat.add_comm .. ▸ hin))
+    simp only [dif_pos hin]
+    rw [getElem_ofFn_go _ 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 [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
 
 @[simp] theorem getElem_ofFn {f : Fin n → α} {i : Nat} (h : i < (ofFn f).size) :
-    (ofFn f)[i] = f ⟨i, size_ofFn (f := f) ▸ h⟩ := by
-  unfold ofFn
-  rw [getElem_ofFn_go] <;> simp_all
+    (ofFn f)[i] = f ⟨i, size_ofFn (f := f) ▸ h⟩ :=
+  getElem_ofFn_go _ (by simp) (by simp) nofun
 
 theorem getElem?_ofFn {f : Fin n → α} {i : Nat} :
     (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none := by
@@ -4413,8 +4425,7 @@ theorem getElem!_eq_getD [Inhabited α] {xs : Array α} {i} : xs[i]! = xs.getD i
 
 /-! # mem -/
 
-@[deprecated mem_toList_iff (since := "2025-05-26")]
-theorem mem_toList {a : α} {xs : Array α} : a ∈ xs.toList ↔ a ∈ xs := mem_def.symm
+@[simp, grind =] theorem mem_toList {a : α} {xs : Array α} : a ∈ xs.toList ↔ a ∈ xs := mem_def.symm
 
 @[deprecated not_mem_empty (since := "2025-03-25")]
 theorem not_mem_nil (a : α) : ¬ a ∈ #[] := nofun
@@ -4463,7 +4474,7 @@ theorem getElem?_push_eq {xs : Array α} {x : α} : (xs.push x)[xs.size]? = some
   simp
 
 @[simp, grind =] theorem forIn'_toList [Monad m] {xs : Array α} {b : β} {f : (a : α) → a ∈ xs.toList → β → m (ForInStep β)} :
-    forIn' xs.toList b f = forIn' xs b (fun a m b => f a (mem_toList_iff.mpr m) b) := by
+    forIn' xs.toList b f = forIn' xs b (fun a m b => f a (mem_toList.mpr m) b) := by
   cases xs
   simp
 
@@ -4560,8 +4571,8 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
 
 theorem toListRev_toArray {l : List α} : l.toArray.toListRev = l.reverse := by simp
 
-@[grind =] theorem take_toArray {l : List α} {i : Nat} : l.toArray.take i = (l.take i).toArray := by
-  simp
+@[simp, grind =] theorem take_toArray {l : List α} {i : Nat} : l.toArray.take i = (l.take i).toArray := by
+  apply Array.ext <;> simp
 
 @[simp, grind =] theorem mapM_toArray [Monad m] [LawfulMonad m] {f : α → m β} {l : List α} :
     l.toArray.mapM f = List.toArray <$> l.mapM f := by

src/Init/Data/Array/Lex/Lemmas.lean

@@ -31,6 +31,10 @@ protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {xs ys
 @[simp] theorem lex_empty [BEq α] {lt : α → α → Bool} {xs : Array α} : xs.lex #[] lt = false := by
   simp [lex]
 
+@[simp] theorem singleton_lex_singleton [BEq α] {lt : α → α → Bool} : #[a].lex #[b] lt = lt a b := by
+  simp only [lex, List.getElem_toArray, List.getElem_singleton]
+  cases lt a b <;> cases a != b <;> simp
+
 private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs ys : Array α} :
      (#[a] ++ xs).lex (#[b] ++ ys) lt =
        (lt a b || a == b && xs.lex ys lt) := by
@@ -54,9 +58,6 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs
     | cons y l₂ =>
       rw [List.toArray_cons, List.toArray_cons y, cons_lex_cons, List.lex, ih]
 
-theorem singleton_lex_singleton [BEq α] {lt : α → α → Bool} : #[a].lex #[b] lt = lt a b := by
-  simp
-
 @[simp, grind =] theorem lex_toList [BEq α] {lt : α → α → Bool} {xs ys : Array α} :
     xs.toList.lex ys.toList lt = xs.lex ys lt := by
   cases xs <;> cases ys <;> simp

src/Init/Data/Array/Monadic.lean

@@ -25,10 +25,10 @@ open Nat
 
 /-! ## Monadic operations -/
 
-theorem map_toList_inj [Monad m] [LawfulMonad m]
+@[simp] theorem map_toList_inj [Monad m] [LawfulMonad m]
     {xs : m (Array α)} {ys : m (Array α)} :
-   toList <$> xs = toList <$> ys ↔ xs = ys := by
-  simp
+   toList <$> xs = toList <$> ys ↔ xs = ys :=
+  _root_.map_inj_right (by simp)
 
 /-! ### mapM -/
 
@@ -195,11 +195,11 @@ theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
   rcases xs with ⟨xs⟩
   simp [List.forIn'_pure_yield_eq_foldl, List.foldl_map]
 
-theorem idRun_forIn'_yield_eq_foldl
+@[simp] theorem idRun_forIn'_yield_eq_foldl
     {xs : Array α} (f : (a : α) → a ∈ xs → β → Id β) (init : β) :
     (forIn' xs init (fun a m b => .yield <$> f a m b)).run =
-      xs.attach.foldl (fun b ⟨a, h⟩ => f a h b |>.run) init := by
-  simp
+      xs.attach.foldl (fun b ⟨a, h⟩ => f a h b |>.run) init :=
+  forIn'_pure_yield_eq_foldl _ _
 
 @[deprecated idRun_forIn'_yield_eq_foldl (since := "2025-05-21")]
 theorem forIn'_yield_eq_foldl
@@ -243,11 +243,11 @@ theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
   rcases xs with ⟨xs⟩
   simp [List.forIn_pure_yield_eq_foldl, List.foldl_map]
 
-theorem idRun_forIn_yield_eq_foldl
+@[simp] theorem idRun_forIn_yield_eq_foldl
     {xs : Array α} (f : α → β → Id β) (init : β) :
     (forIn xs init (fun a b => .yield <$> f a b)).run =
-      xs.foldl (fun b a => f a b |>.run) init := by
-  simp
+      xs.foldl (fun b a => f a b |>.run) init :=
+  forIn_pure_yield_eq_foldl _ _
 
 @[deprecated idRun_forIn_yield_eq_foldl (since := "2025-05-21")]
 theorem forIn_yield_eq_foldl

src/Init/Data/Array/Zip.lean

@@ -334,13 +334,11 @@ abbrev zipWithAll_mkArray := @zipWithAll_replicate
 
 /-! ### unzip -/
 
-@[deprecated fst_unzip (since := "2025-05-26")]
-theorem unzip_fst : (unzip l).fst = l.map Prod.fst := by
-  simp
+@[simp] theorem unzip_fst : (unzip l).fst = l.map Prod.fst := by
+  induction l <;> simp_all
 
-@[deprecated snd_unzip (since := "2025-05-26")]
-theorem unzip_snd : (unzip l).snd = l.map Prod.snd := by
-  simp
+@[simp] theorem unzip_snd : (unzip l).snd = l.map Prod.snd := by
+  induction l <;> simp_all
 
 theorem unzip_eq_map {xs : Array (α × β)} : unzip xs = (xs.map Prod.fst, xs.map Prod.snd) := by
   cases xs
@@ -373,7 +371,7 @@ theorem unzip_zip {as : Array α} {bs : Array β} (h : as.size = bs.size) :
 
 theorem zip_of_prod {as : Array α} {bs : Array β} {xs : Array (α × β)} (hl : xs.map Prod.fst = as)
     (hr : xs.map Prod.snd = bs) : xs = as.zip bs := by
-  rw [← hl, ← hr, ← zip_unzip xs, ← fst_unzip, ← snd_unzip, zip_unzip, zip_unzip]
+  rw [← hl, ← hr, ← zip_unzip xs, ← unzip_fst, ← unzip_snd, zip_unzip, zip_unzip]
 
 @[simp] theorem unzip_replicate {n : Nat} {a : α} {b : β} :
     unzip (replicate n (a, b)) = (replicate n a, replicate n b) := by

src/Init/Data/BitVec/Lemmas.lean

@@ -93,13 +93,13 @@ theorem getElem?_eq (l : BitVec w) (i : Nat) :
     l[i]? = if h : i < w then some l[i] else none := by
   split <;> simp_all
 
-theorem some_getElem_eq_getElem? (l : BitVec w) (i : Nat) (h : i < w) :
+@[simp] theorem some_getElem_eq_getElem? (l : BitVec w) (i : Nat) (h : i < w) :
     (some l[i] = l[i]?) ↔ True := by
-  simp
+  simp [h]
 
-theorem getElem?_eq_some_getElem (l : BitVec w) (i : Nat) (h : i < w) :
+@[simp] theorem getElem?_eq_some_getElem (l : BitVec w) (i : Nat) (h : i < w) :
     (l[i]? = some l[i]) ↔ True := by
-  simp
+  simp [h]
 
 theorem getElem_eq_iff {l : BitVec w} {n : Nat} {h : n < w} : l[n] = x ↔ l[n]? = some x := by
   simp only [getElem?_eq_some_iff]
@@ -505,7 +505,7 @@ theorem getLsbD_ofBool (b : Bool) (i : Nat) : (ofBool b).getLsbD i = ((i = 0) &&
   · simp only [ofBool, ofNat_eq_ofNat, cond_true, getLsbD_ofNat, Bool.and_true]
     by_cases hi : i = 0 <;> simp [hi] <;> omega
 
-theorem getElem_ofBool_zero {b : Bool} : (ofBool b)[0] = b := by simp
+@[simp] theorem getElem_ofBool_zero {b : Bool} : (ofBool b)[0] = b := by simp
 
 @[simp]
 theorem getElem_ofBool {b : Bool} {h : i < 1}: (ofBool b)[i] = b := by
@@ -3179,11 +3179,11 @@ theorem getElem_concat (x : BitVec w) (b : Bool) (i : Nat) (h : i < w + 1) :
   · simp [Nat.mod_eq_of_lt b.toNat_lt]
   · simp [Nat.div_eq_of_lt b.toNat_lt, Nat.testBit_add_one]
 
-@[simp] theorem getElem_concat_zero : (concat x b)[0] = b := by
+@[simp] theorem getLsbD_concat_zero : (concat x b).getLsbD 0 = b := by
   simp [getElem_concat]
 
-theorem getLsbD_concat_zero : (concat x b).getLsbD 0 = b := by
-  simp
+@[simp] theorem getElem_concat_zero : (concat x b)[0] = b := by
+  simp [getElem_concat]
 
 @[simp] theorem getLsbD_concat_succ : (concat x b).getLsbD (i + 1) = x.getLsbD i := by
   simp [getLsbD_concat]

src/Init/Data/Int/DivMod/Bootstrap.lean

@@ -264,8 +264,8 @@ theorem mul_emod (a b n : Int) : (a * b) % n = (a % n) * (b % n) % n := by
   match k, h with
   | _, ⟨t, rfl⟩ => rw [Int.mul_assoc, add_mul_emod_self_left]
 
-theorem emod_emod (a b : Int) : (a % b) % b = a % b := by
-  simp
+@[simp] theorem emod_emod (a b : Int) : (a % b) % b = a % b := by
+  conv => rhs; rw [← emod_add_ediv a b, add_mul_emod_self_left]
 
 theorem sub_emod (a b n : Int) : (a - b) % n = (a % n - b % n) % n := by
   apply (emod_add_cancel_right b).mp

src/Init/Data/Int/DivMod/Lemmas.lean

@@ -1410,7 +1410,8 @@ theorem mul_tmod (a b n : Int) : (a * b).tmod n = (a.tmod n * b.tmod n).tmod n :
   norm_cast at h
   rw [Nat.mod_mod_of_dvd _ h]
 
-theorem tmod_tmod (a b : Int) : (a.tmod b).tmod b = a.tmod b := by simp
+@[simp] theorem tmod_tmod (a b : Int) : (a.tmod b).tmod b = a.tmod b :=
+  tmod_tmod_of_dvd a (Int.dvd_refl b)
 
 theorem tmod_eq_zero_of_dvd : ∀ {a b : Int}, a ∣ b → tmod b a = 0
   | _, _, ⟨_, rfl⟩ => mul_tmod_right ..
@@ -1468,8 +1469,9 @@ protected theorem tdiv_mul_cancel {a b : Int} (H : b ∣ a) : a.tdiv b * b = a :
 protected theorem mul_tdiv_cancel' {a b : Int} (H : a ∣ b) : a * b.tdiv a = b := by
   rw [Int.mul_comm, Int.tdiv_mul_cancel H]
 
-theorem neg_tmod_self (a : Int) : (-a).tmod a = 0 := by
-  simp
+@[simp] theorem neg_tmod_self (a : Int) : (-a).tmod a = 0 := by
+  rw [← dvd_iff_tmod_eq_zero, Int.dvd_neg]
+  exact Int.dvd_refl a
 
 theorem lt_tdiv_add_one_mul_self (a : Int) {b : Int} (H : 0 < b) : a < (a.tdiv b + 1) * b := by
   rw [Int.add_mul, Int.one_mul, Int.mul_comm]
@@ -1566,11 +1568,13 @@ theorem dvd_tmod_sub_self {x m : Int} : m ∣ x.tmod m - x := by
 theorem dvd_self_sub_tmod {x m : Int} : m ∣ x - x.tmod m :=
   Int.dvd_neg.1 (by simpa only [Int.neg_sub] using dvd_tmod_sub_self)
 
-theorem neg_mul_tmod_right (a b : Int) : (-(a * b)).tmod a = 0 := by
-  simp
+@[simp] theorem neg_mul_tmod_right (a b : Int) : (-(a * b)).tmod a = 0 := by
+  rw [← dvd_iff_tmod_eq_zero, Int.dvd_neg]
+  exact Int.dvd_mul_right a b
 
-theorem neg_mul_tmod_left (a b : Int) : (-(a * b)).tmod b = 0 := by
-  simp
+@[simp] theorem neg_mul_tmod_left (a b : Int) : (-(a * b)).tmod b = 0 := by
+  rw [← dvd_iff_tmod_eq_zero, Int.dvd_neg]
+  exact Int.dvd_mul_left a b
 
 @[simp] protected theorem tdiv_one : ∀ a : Int, a.tdiv 1 = a
   | (n:Nat) => congrArg ofNat (Nat.div_one _)
@@ -2189,8 +2193,8 @@ theorem mul_fmod (a b n : Int) : (a * b).fmod n = (a.fmod n * b.fmod n).fmod n :
   match k, h with
   | _, ⟨t, rfl⟩ => rw [Int.mul_assoc, add_mul_fmod_self_left]
 
-theorem fmod_fmod (a b : Int) : (a.fmod b).fmod b = a.fmod b := by
-  simp
+@[simp] theorem fmod_fmod (a b : Int) : (a.fmod b).fmod b = a.fmod b :=
+  fmod_fmod_of_dvd _ (Int.dvd_refl b)
 
 theorem sub_fmod (a b n : Int) : (a - b).fmod n = (a.fmod n - b.fmod n).fmod n := by
   apply (fmod_add_cancel_right b).mp

src/Init/Data/List/Find.lean

@@ -1108,9 +1108,14 @@ theorem isSome_finIdxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} :
     simp only [finIdxOf?_cons]
     split <;> simp_all [@eq_comm _ x a]
 
+@[simp]
 theorem isNone_finIdxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} :
     (l.finIdxOf? a).isNone = ¬ a ∈ l := by
-  simp
+  induction l with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [finIdxOf?_cons]
+    split <;> simp_all [@eq_comm _ x a]
 
 /-! ### idxOf?
 
@@ -1149,9 +1154,15 @@ theorem isSome_idxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} :
     simp only [idxOf?_cons]
     split <;> simp_all [@eq_comm _ x a]
 
+@[simp]
 theorem isNone_idxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} :
     (l.idxOf? a).isNone = ¬ a ∈ l := by
-  simp
+  induction l with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [idxOf?_cons]
+    split <;> simp_all [@eq_comm _ x a]
+
 
 /-! ### lookup -/
 

src/Init/Data/List/Impl.lean

@@ -109,7 +109,7 @@ Example:
   let rec go : ∀ as acc, filterMapTR.go f as acc = acc.toList ++ as.filterMap f
     | [], acc => by simp [filterMapTR.go, filterMap]
     | a::as, acc => by
-      simp only [filterMapTR.go, go as, Array.toList_push, append_assoc, singleton_append,
+      simp only [filterMapTR.go, go as, Array.push_toList, append_assoc, singleton_append,
         filterMap]
       split <;> simp [*]
   exact (go l #[]).symm

src/Init/Data/List/Lemmas.lean

@@ -272,13 +272,13 @@ theorem getElem_of_getElem? {l : List α} : l[i]? = some a → ∃ h : i < l.len
 theorem some_eq_getElem?_iff {l : List α} : some a = l[i]? ↔ ∃ h : i < l.length, l[i] = a := by
   rw [eq_comm, getElem?_eq_some_iff]
 
-theorem some_getElem_eq_getElem?_iff {xs : List α} {i : Nat} (h : i < xs.length) :
+@[simp] theorem some_getElem_eq_getElem?_iff {xs : List α} {i : Nat} (h : i < xs.length) :
     (some xs[i] = xs[i]?) ↔ True := by
-  simp
+  simp [h]
 
-theorem getElem?_eq_some_getElem_iff {xs : List α} {i : Nat} (h : i < xs.length) :
+@[simp] theorem getElem?_eq_some_getElem_iff {xs : List α} {i : Nat} (h : i < xs.length) :
     (xs[i]? = some xs[i]) ↔ True := by
-  simp
+  simp [h]
 
 theorem getElem_eq_iff {l : List α} {i : Nat} (h : i < l.length) : l[i] = x ↔ l[i]? = some x := by
   simp only [getElem?_eq_some_iff]
@@ -296,7 +296,7 @@ theorem getD_getElem? {l : List α} {i : Nat} {d : α} :
     have p : i ≥ l.length := Nat.le_of_not_gt h
     simp [getElem?_eq_none p, h]
 
-@[simp] theorem getElem_singleton {a : α} {i : Nat} (h : i < 1) : [a][i] = a := by
+@[simp] theorem getElem_singleton {a : α} {i : Nat} (h : i < 1) : [a][i] = a :=
   match i, h with
   | 0, _ => rfl
 
@@ -434,8 +434,8 @@ theorem eq_nil_iff_forall_not_mem {l : List α} : l = [] ↔ ∀ a, a ∉ l := b
 theorem eq_of_mem_singleton : a ∈ [b] → a = b
   | .head .. => rfl
 
-theorem mem_singleton {a b : α} : a ∈ [b] ↔ a = b := by
-  simp
+@[simp] theorem mem_singleton {a b : α} : a ∈ [b] ↔ a = b :=
+  ⟨eq_of_mem_singleton, (by simp [·])⟩
 
 theorem forall_mem_cons {p : α → Prop} {a : α} {l : List α} :
     (∀ x, x ∈ a :: l → p x) ↔ p a ∧ ∀ x, x ∈ l → p x :=
@@ -1685,8 +1685,8 @@ theorem getLast_concat {a : α} : ∀ {l : List α}, getLast (l ++ [a]) (by simp
 
 @[deprecated append_eq_nil_iff (since := "2025-01-13")] abbrev append_eq_nil := @append_eq_nil_iff
 
-theorem nil_eq_append_iff : [] = a ++ b ↔ a = [] ∧ b = [] := by
-  simp
+@[simp] theorem nil_eq_append_iff : [] = a ++ b ↔ a = [] ∧ b = [] := by
+  rw [eq_comm, append_eq_nil_iff]
 
 @[grind →]
 theorem eq_nil_of_append_eq_nil {l₁ l₂ : List α} (h : l₁ ++ l₂ = []) : l₁ = [] ∧ l₂ = [] :=
@@ -1897,8 +1897,8 @@ theorem eq_nil_or_concat : ∀ l : List α, l = [] ∨ ∃ l' b, l = concat l' b
 @[simp] theorem flatten_eq_nil_iff {L : List (List α)} : L.flatten = [] ↔ ∀ l ∈ L, l = [] := by
   induction L <;> simp_all
 
-theorem nil_eq_flatten_iff {L : List (List α)} : [] = L.flatten ↔ ∀ l ∈ L, l = [] := by
-  simp
+@[simp] theorem nil_eq_flatten_iff {L : List (List α)} : [] = L.flatten ↔ ∀ l ∈ L, l = [] := by
+  rw [eq_comm, flatten_eq_nil_iff]
 
 theorem flatten_ne_nil_iff {xss : List (List α)} : xss.flatten ≠ [] ↔ ∃ xs, xs ∈ xss ∧ xs ≠ [] := by
   simp
@@ -2585,9 +2585,9 @@ theorem id_run_foldrM {f : α → β → Id β} {b : β} {l : List α} :
   induction l generalizing l' <;> simp [*]
 
 /-- Variant of `foldl_flip_cons_eq_append` specalized to `f = id`. -/
-@[grind] theorem foldl_flip_cons_eq_append' {l l' : List α} :
+@[simp, grind] theorem foldl_flip_cons_eq_append' {l l' : List α} :
     l.foldl (fun xs y => y :: xs) l' = l.reverse ++ l' := by
-  simp
+  induction l generalizing l' <;> simp [*]
 
 @[simp, grind] theorem foldr_append_eq_append {l : List α} {f : α → List β} {l' : List β} :
     l.foldr (f · ++ ·) l' = (l.map f).flatten ++ l' := by
@@ -3427,8 +3427,8 @@ variable [LawfulBEq α]
     | Or.inr h' => exact h'
   else rw [insert_of_not_mem h, mem_cons]
 
-theorem mem_insert_self {a : α} {l : List α} : a ∈ l.insert a := by
-  simp
+@[simp] theorem mem_insert_self {a : α} {l : List α} : a ∈ l.insert a :=
+  mem_insert_iff.2 (Or.inl rfl)
 
 theorem mem_insert_of_mem {l : List α} (h : a ∈ l) : a ∈ l.insert b :=
   mem_insert_iff.2 (Or.inr h)

src/Init/Data/List/MapIdx.lean

@@ -348,7 +348,7 @@ theorem getElem?_mapIdx_go : ∀ {l : List α} {acc : Array β} {i : Nat},
     split <;> split
     · simp only [Option.some.injEq]
       rw [← Array.getElem_toList]
-      simp only [Array.toList_push]
+      simp only [Array.push_toList]
       rw [getElem_append_left, ← Array.getElem_toList]
     · have : i = acc.size := by omega
       simp_all

src/Init/Data/List/Pairwise.lean

@@ -24,7 +24,7 @@ open Nat
 
 /-! ### Pairwise -/
 
-@[grind →] theorem Pairwise.sublist : l₁ <+ l₂ → l₂.Pairwise R → l₁.Pairwise R
+theorem Pairwise.sublist : l₁ <+ l₂ → l₂.Pairwise R → l₁.Pairwise R
   | .slnil, h => h
   | .cons _ s, .cons _ h₂ => h₂.sublist s
   | .cons₂ _ s, .cons h₁ h₂ => (h₂.sublist s).cons fun _ h => h₁ _ (s.subset h)
@@ -37,11 +37,11 @@ theorem Pairwise.imp {α R S} (H : ∀ {a b}, R a b → S a b) :
 theorem rel_of_pairwise_cons (p : (a :: l).Pairwise R) : ∀ {a'}, a' ∈ l → R a a' :=
   (pairwise_cons.1 p).1 _
 
-@[grind →] theorem Pairwise.of_cons (p : (a :: l).Pairwise R) : Pairwise R l :=
+theorem Pairwise.of_cons (p : (a :: l).Pairwise R) : Pairwise R l :=
   (pairwise_cons.1 p).2
 
 set_option linter.unusedVariables false in
-@[grind] theorem Pairwise.tail : ∀ {l : List α} (h : Pairwise R l), Pairwise R l.tail
+theorem Pairwise.tail : ∀ {l : List α} (h : Pairwise R l), Pairwise R l.tail
   | [], h => h
   | _ :: _, h => h.of_cons
 
@@ -101,11 +101,11 @@ theorem Pairwise.forall_of_forall_of_flip (h₁ : ∀ x ∈ l, R x x) (h₂ : Pa
     · exact h₃.1 _ hx
     · exact ih (fun x hx => h₁ _ <| mem_cons_of_mem _ hx) h₂.2 h₃.2 hx hy
 
-@[grind] theorem pairwise_singleton (R) (a : α) : Pairwise R [a] := by simp
+theorem pairwise_singleton (R) (a : α) : Pairwise R [a] := by simp
 
-@[grind =] theorem pairwise_pair {a b : α} : Pairwise R [a, b] ↔ R a b := by simp
+theorem pairwise_pair {a b : α} : Pairwise R [a, b] ↔ R a b := by simp
 
-@[grind =] theorem pairwise_map {l : List α} :
+theorem pairwise_map {l : List α} :
     (l.map f).Pairwise R ↔ l.Pairwise fun a b => R (f a) (f b) := by
   induction l
   · simp
@@ -115,11 +115,11 @@ theorem Pairwise.of_map {S : β → β → Prop} (f : α → β) (H : ∀ a b :
     (p : Pairwise S (map f l)) : Pairwise R l :=
   (pairwise_map.1 p).imp (H _ _)
 
-@[grind] theorem Pairwise.map {S : β → β → Prop} (f : α → β) (H : ∀ a b : α, R a b → S (f a) (f b))
+theorem Pairwise.map {S : β → β → Prop} (f : α → β) (H : ∀ a b : α, R a b → S (f a) (f b))
     (p : Pairwise R l) : Pairwise S (map f l) :=
   pairwise_map.2 <| p.imp (H _ _)
 
-@[grind =] theorem pairwise_filterMap {f : β → Option α} {l : List β} :
+theorem pairwise_filterMap {f : β → Option α} {l : List β} :
     Pairwise R (filterMap f l) ↔ Pairwise (fun a a' : β => ∀ b, f a = some b → ∀ b', f a' = some b' → R b b') l := by
   let _S (a a' : β) := ∀ b, f a = some b → ∀ b', f a' = some b' → R b b'
   induction l with
@@ -134,20 +134,20 @@ theorem Pairwise.of_map {S : β → β → Prop} (f : α → β) (H : ∀ a b :
     simpa [IH, e] using fun _ =>
       ⟨fun h a ha b hab => h _ _ ha hab, fun h a b ha hab => h _ ha _ hab⟩
 
-@[grind] theorem Pairwise.filterMap {S : β → β → Prop} (f : α → Option β)
+theorem Pairwise.filterMap {S : β → β → Prop} (f : α → Option β)
     (H : ∀ a a' : α, R a a' → ∀ b, f a = some b → ∀ b', f a' = some b' → S b b') {l : List α} (p : Pairwise R l) :
     Pairwise S (filterMap f l) :=
   pairwise_filterMap.2 <| p.imp (H _ _)
 
-@[grind =] theorem pairwise_filter {p : α → Bool} {l : List α} :
+theorem pairwise_filter {p : α → Prop} [DecidablePred p] {l : List α} :
     Pairwise R (filter p l) ↔ Pairwise (fun x y => p x → p y → R x y) l := by
   rw [← filterMap_eq_filter, pairwise_filterMap]
   simp
 
-@[grind] theorem Pairwise.filter (p : α → Bool) : Pairwise R l → Pairwise R (filter p l) :=
+theorem Pairwise.filter (p : α → Bool) : Pairwise R l → Pairwise R (filter p l) :=
   Pairwise.sublist filter_sublist
 
-@[grind =] theorem pairwise_append {l₁ l₂ : List α} :
+theorem pairwise_append {l₁ l₂ : List α} :
     (l₁ ++ l₂).Pairwise R ↔ l₁.Pairwise R ∧ l₂.Pairwise R ∧ ∀ a ∈ l₁, ∀ b ∈ l₂, R a b := by
   induction l₁ <;> simp [*, or_imp, forall_and, and_assoc, and_left_comm]
 
@@ -157,13 +157,13 @@ theorem pairwise_append_comm {R : α → α → Prop} (s : ∀ {x y}, R x y →
     (x : α) (xm : x ∈ l₂) (y : α) (ym : y ∈ l₁) : R x y := s (H y ym x xm)
   simp only [pairwise_append, and_left_comm]; rw [Iff.intro (this l₁ l₂) (this l₂ l₁)]
 
-@[grind =] theorem pairwise_middle {R : α → α → Prop} (s : ∀ {x y}, R x y → R y x) {a : α} {l₁ l₂ : List α} :
+theorem pairwise_middle {R : α → α → Prop} (s : ∀ {x y}, R x y → R y x) {a : α} {l₁ l₂ : List α} :
     Pairwise R (l₁ ++ a :: l₂) ↔ Pairwise R (a :: (l₁ ++ l₂)) := by
   show Pairwise R (l₁ ++ ([a] ++ l₂)) ↔ Pairwise R ([a] ++ l₁ ++ l₂)
   rw [← append_assoc, pairwise_append, @pairwise_append _ _ ([a] ++ l₁), pairwise_append_comm s]
   simp only [mem_append, or_comm]
 
-@[grind =] theorem pairwise_flatten {L : List (List α)} :
+theorem pairwise_flatten {L : List (List α)} :
     Pairwise R (flatten L) ↔
       (∀ l ∈ L, Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ x ∈ l₁, ∀ y ∈ l₂, R x y) L := by
   induction L with
@@ -174,16 +174,16 @@ theorem pairwise_append_comm {R : α → α → Prop} (s : ∀ {x y}, R x y →
     rw [and_comm, and_congr_left_iff]
     intros; exact ⟨fun h l' b c d e => h c d e l' b, fun h c d e l' b => h l' b c d e⟩
 
-@[grind =] theorem pairwise_flatMap {R : β → β → Prop} {l : List α} {f : α → List β} :
+theorem pairwise_flatMap {R : β → β → Prop} {l : List α} {f : α → List β} :
     List.Pairwise R (l.flatMap f) ↔
       (∀ a ∈ l, Pairwise R (f a)) ∧ Pairwise (fun a₁ a₂ => ∀ x ∈ f a₁, ∀ y ∈ f a₂, R x y) l := by
   simp [List.flatMap, pairwise_flatten, pairwise_map]
 
-@[grind =] theorem pairwise_reverse {l : List α} :
+theorem pairwise_reverse {l : List α} :
     l.reverse.Pairwise R ↔ l.Pairwise (fun a b => R b a) := by
   induction l <;> simp [*, pairwise_append, and_comm]
 
-@[simp, grind =] theorem pairwise_replicate {n : Nat} {a : α} :
+@[simp] theorem pairwise_replicate {n : Nat} {a : α} :
     (replicate n a).Pairwise R ↔ n ≤ 1 ∨ R a a := by
   induction n with
   | zero => simp
@@ -205,10 +205,10 @@ theorem pairwise_append_comm {R : α → α → Prop} (s : ∀ {x y}, R x y →
         simp
       · exact ⟨fun _ => h, Or.inr h⟩
 
-@[grind] theorem Pairwise.drop {l : List α} {i : Nat} (h : List.Pairwise R l) : List.Pairwise R (l.drop i) :=
+theorem Pairwise.drop {l : List α} {i : Nat} (h : List.Pairwise R l) : List.Pairwise R (l.drop i) :=
   h.sublist (drop_sublist _ _)
 
-@[grind] theorem Pairwise.take {l : List α} {i : Nat} (h : List.Pairwise R l) : List.Pairwise R (l.take i) :=
+theorem Pairwise.take {l : List α} {i : Nat} (h : List.Pairwise R l) : List.Pairwise R (l.take i) :=
   h.sublist (take_sublist _ _)
 
 theorem pairwise_iff_forall_sublist : l.Pairwise R ↔ (∀ {a b}, [a,b] <+ l → R a b) := by
@@ -247,7 +247,7 @@ theorem pairwise_of_forall_mem_list {l : List α} {r : α → α → Prop} (h :
   intro a b hab
   apply h <;> (apply hab.subset; simp)
 
-@[grind =] theorem pairwise_pmap {p : β → Prop} {f : ∀ b, p b → α} {l : List β} (h : ∀ x ∈ l, p x) :
+theorem pairwise_pmap {p : β → Prop} {f : ∀ b, p b → α} {l : List β} (h : ∀ x ∈ l, p x) :
     Pairwise R (l.pmap f h) ↔
       Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l := by
   induction l with
@@ -259,7 +259,7 @@ theorem pairwise_of_forall_mem_list {l : List α} {r : α → α → Prop} (h :
     rintro H _ b hb rfl
     exact H b hb _ _
 
-@[grind] theorem Pairwise.pmap {l : List α} (hl : Pairwise R l) {p : α → Prop} {f : ∀ a, p a → β}
+theorem Pairwise.pmap {l : List α} (hl : Pairwise R l) {p : α → Prop} {f : ∀ a, p a → β}
     (h : ∀ x ∈ l, p x) {S : β → β → Prop}
     (hS : ∀ ⦃x⦄ (hx : p x) ⦃y⦄ (hy : p y), R x y → S (f x hx) (f y hy)) :
     Pairwise S (l.pmap f h) := by
@@ -268,15 +268,15 @@ theorem pairwise_of_forall_mem_list {l : List α} {r : α → α → Prop} (h :
 
 /-! ### Nodup -/
 
-@[simp, grind]
+@[simp]
 theorem nodup_nil : @Nodup α [] :=
   Pairwise.nil
 
-@[simp, grind =]
+@[simp]
 theorem nodup_cons {a : α} {l : List α} : Nodup (a :: l) ↔ a ∉ l ∧ Nodup l := by
   simp only [Nodup, pairwise_cons, forall_mem_ne]
 
-@[grind →] theorem Nodup.sublist : l₁ <+ l₂ → Nodup l₂ → Nodup l₁ :=
+theorem Nodup.sublist : l₁ <+ l₂ → Nodup l₂ → Nodup l₁ :=
   Pairwise.sublist
 
 theorem Sublist.nodup : l₁ <+ l₂ → Nodup l₂ → Nodup l₁ :=
@@ -303,7 +303,7 @@ theorem getElem?_inj {xs : List α}
       rw [mem_iff_getElem?]
     exact ⟨_, h₂⟩; exact ⟨_ , h₂.symm⟩
 
-@[simp, grind =] theorem nodup_replicate {n : Nat} {a : α} :
+@[simp] theorem nodup_replicate {n : Nat} {a : α} :
     (replicate n a).Nodup ↔ n ≤ 1 := by simp [Nodup]
 
 end List

src/Init/Data/Nat/Basic.lean

@@ -150,7 +150,7 @@ theorem add_one (n : Nat) : n + 1 = succ n :=
 @[simp] theorem succ_eq_add_one (n : Nat) : succ n = n + 1 :=
   rfl
 
-theorem add_one_ne_zero (n : Nat) : n + 1 ≠ 0 := nofun
+@[simp] theorem add_one_ne_zero (n : Nat) : n + 1 ≠ 0 := nofun
 theorem zero_ne_add_one (n : Nat) : 0 ≠ n + 1 := by simp
 
 protected theorem add_comm : ∀ (n m : Nat), n + m = m + n
@@ -731,12 +731,13 @@ theorem exists_eq_add_one_of_ne_zero : ∀ {n}, n ≠ 0 → Exists fun k => n =
 theorem ctor_eq_zero : Nat.zero = 0 :=
   rfl
 
-protected theorem one_ne_zero : 1 ≠ (0 : Nat) := by simp
+@[simp] protected theorem one_ne_zero : 1 ≠ (0 : Nat) :=
+  fun h => Nat.noConfusion h
 
 @[simp] protected theorem zero_ne_one : 0 ≠ (1 : Nat) :=
   fun h => Nat.noConfusion h
 
-theorem succ_ne_zero (n : Nat) : succ n ≠ 0 := by simp
+@[simp] theorem succ_ne_zero (n : Nat) : succ n ≠ 0 := by simp
 
 instance instNeZeroSucc {n : Nat} : NeZero (n + 1) := ⟨succ_ne_zero n⟩
 

src/Init/Data/Nat/Lemmas.lean

@@ -415,7 +415,7 @@ theorem succ_min_succ (x y) : min (succ x) (succ y) = succ (min x y) := by
   | inl h => rw [Nat.min_eq_left h, Nat.min_eq_left (Nat.succ_le_succ h)]
   | inr h => rw [Nat.min_eq_right h, Nat.min_eq_right (Nat.succ_le_succ h)]
 
-protected theorem min_self (a : Nat) : min a a = a := by simp
+@[simp] protected theorem min_self (a : Nat) : min a a = a := Nat.min_eq_left (Nat.le_refl _)
 instance : Std.IdempotentOp (α := Nat) min := ⟨Nat.min_self⟩
 
 @[simp] protected theorem min_assoc : ∀ (a b c : Nat), min (min a b) c = min a (min b c)
@@ -431,14 +431,16 @@ instance : Std.Associative (α := Nat) min := ⟨Nat.min_assoc⟩
 @[simp] protected theorem min_self_assoc' {m n : Nat} : min n (min m n) = min n m := by
   rw [Nat.min_comm m n, ← Nat.min_assoc, Nat.min_self]
 
-theorem min_add_left_self {a b : Nat} : min a (b + a) = a := by
+@[simp] theorem min_add_left_self {a b : Nat} : min a (b + a) = a := by
+  rw [Nat.min_def]
   simp
-theorem min_add_right_self {a b : Nat} : min a (a + b) = a := by
-  simp
-theorem add_left_min_self {a b : Nat} : min (b + a) a = a := by
-  simp
-theorem add_right_min_self {a b : Nat} : min (a + b) a = a := by
+@[simp] theorem min_add_right_self {a b : Nat} : min a (a + b) = a := by
+  rw [Nat.min_def]
   simp
+@[simp] theorem add_left_min_self {a b : Nat} : min (b + a) a = a := by
+  rw [Nat.min_comm, min_add_left_self]
+@[simp] theorem add_right_min_self {a b : Nat} : min (a + b) a = a := by
+  rw [Nat.min_comm, min_add_right_self]
 
 protected theorem sub_sub_eq_min : ∀ (a b : Nat), a - (a - b) = min a b
   | 0, _ => by rw [Nat.zero_sub, Nat.zero_min]
@@ -460,7 +462,7 @@ protected theorem succ_max_succ (x y) : max (succ x) (succ y) = succ (max x y) :
   | inl h => rw [Nat.max_eq_right h, Nat.max_eq_right (Nat.succ_le_succ h)]
   | inr h => rw [Nat.max_eq_left h, Nat.max_eq_left (Nat.succ_le_succ h)]
 
-protected theorem max_self (a : Nat) : max a a = a := by simp
+@[simp] protected theorem max_self (a : Nat) : max a a = a := Nat.max_eq_right (Nat.le_refl _)
 instance : Std.IdempotentOp (α := Nat) max := ⟨Nat.max_self⟩
 
 instance : Std.LawfulIdentity (α := Nat) max 0 where
@@ -474,14 +476,16 @@ instance : Std.LawfulIdentity (α := Nat) max 0 where
   | _+1, _+1, _+1 => by simp only [Nat.succ_max_succ]; exact congrArg succ <| Nat.max_assoc ..
 instance : Std.Associative (α := Nat) max := ⟨Nat.max_assoc⟩
 
-theorem max_add_left_self {a b : Nat} : max a (b + a) = b + a := by
+@[simp] theorem max_add_left_self {a b : Nat} : max a (b + a) = b + a := by
+  rw [Nat.max_def]
   simp
-theorem max_add_right_self {a b : Nat} : max a (a + b) = a + b := by
-  simp
-theorem add_left_max_self {a b : Nat} : max (b + a) a = b + a := by
-  simp
-theorem add_right_max_self {a b : Nat} : max (a + b) a = a + b := by
+@[simp] theorem max_add_right_self {a b : Nat} : max a (a + b) = a + b := by
+  rw [Nat.max_def]
   simp
+@[simp] theorem add_left_max_self {a b : Nat} : max (b + a) a = b + a := by
+  rw [Nat.max_comm, max_add_left_self]
+@[simp] theorem add_right_max_self {a b : Nat} : max (a + b) a = a + b := by
+  rw [Nat.max_comm, max_add_right_self]
 
 protected theorem sub_add_eq_max (a b : Nat) : a - b + b = max a b := by
   match Nat.le_total a b with
@@ -810,8 +814,10 @@ theorem sub_mul_mod {x k n : Nat} (h₁ : n*k ≤ x) : (x - n*k) % n = x % n :=
       simp [mul_succ, Nat.add_comm] at h₁; simp [h₁]
     rw [mul_succ, ← Nat.sub_sub, ← mod_eq_sub_mod h₄, sub_mul_mod h₂]
 
-theorem mod_mod (a n : Nat) : (a % n) % n = a % n := by
-  simp
+@[simp] theorem mod_mod (a n : Nat) : (a % n) % n = a % n :=
+  match eq_zero_or_pos n with
+  | .inl n0 => by simp [n0, mod_zero]
+  | .inr npos => Nat.mod_eq_of_lt (mod_lt _ npos)
 
 theorem mul_mod (a b n : Nat) : a * b % n = (a % n) * (b % n) % n := by
   rw (occs := [1]) [← mod_add_div a n]

src/Init/Data/Option/Array.lean

@@ -82,9 +82,10 @@ theorem toArray_eq_empty_iff {o : Option α} : o.toArray = #[] ↔ o = none := b
 theorem toArray_eq_singleton_iff {o : Option α} : o.toArray = #[a] ↔ o = some a := by
   cases o <;> simp
 
+@[simp]
 theorem size_toArray_eq_zero_iff {o : Option α} :
     o.toArray.size = 0 ↔ o = none := by
-  simp
+  cases o <;> simp
 
 @[simp]
 theorem size_toArray_eq_one_iff {o : Option α} :

src/Init/Data/Option/Lemmas.lean

@@ -1522,13 +1522,13 @@ theorem pfilter_guard {a : α} {p : α → Bool} {q : (a' : α) → guard p a =
 /-! ### LT and LE -/
 
 @[simp, grind] theorem not_lt_none [LT α] {a : Option α} : ¬ a < none := by cases a <;> simp [LT.lt, Option.lt]
-@[grind] theorem none_lt_some [LT α] {a : α} : none < some a := by simp [LT.lt, Option.lt]
-@[simp] theorem none_lt [LT α] {a : Option α} : none < a ↔ a.isSome := by cases a <;> simp [none_lt_some]
+@[simp, grind] theorem none_lt_some [LT α] {a : α} : none < some a := by simp [LT.lt, Option.lt]
+@[simp] theorem none_lt [LT α] {a : Option α} : none < a ↔ a.isSome := by cases a <;> simp
 @[simp, grind] theorem some_lt_some [LT α] {a b : α} : some a < some b ↔ a < b := by simp [LT.lt, Option.lt]
 
 @[simp, grind] theorem none_le [LE α] {a : Option α} : none ≤ a := by cases a <;> simp [LE.le, Option.le]
-@[grind] theorem not_some_le_none [LE α] {a : α} : ¬ some a ≤ none := by simp [LE.le, Option.le]
-@[simp] theorem le_none [LE α] {a : Option α} : a ≤ none ↔ a = none := by cases a <;> simp [not_some_le_none]
+@[simp, grind] theorem not_some_le_none [LE α] {a : α} : ¬ some a ≤ none := by simp [LE.le, Option.le]
+@[simp] theorem le_none [LE α] {a : Option α} : a ≤ none ↔ a = none := by cases a <;> simp
 @[simp, grind] theorem some_le_some [LE α] {a b : α} : some a ≤ some b ↔ a ≤ b := by simp [LE.le, Option.le]
 
 @[simp]

src/Init/Data/Option/List.lean

@@ -86,9 +86,10 @@ theorem toList_eq_nil_iff {o : Option α} : o.toList = [] ↔ o = none := by
 theorem toList_eq_singleton_iff {o : Option α} : o.toList = [a] ↔ o = some a := by
   cases o <;> simp
 
+@[simp]
 theorem length_toList_eq_zero_iff {o : Option α} :
     o.toList.length = 0 ↔ o = none := by
-  simp
+  cases o <;> simp
 
 @[simp]
 theorem length_toList_eq_one_iff {o : Option α} :

src/Init/Data/Vector/Attach.lean

@@ -474,10 +474,7 @@ If not, usually the right approach is `simp [Vector.unattach, -Vector.map_subtyp
 -/
 def unattach {α : Type _} {p : α → Prop} (xs : Vector { x // p x } n) : Vector α n := xs.map (·.val)
 
-theorem unattach_empty {p : α → Prop} : (#v[] : Vector { x // p x } 0).unattach = #v[] := by simp
-
-@[deprecated unattach_empty (since := "2025-05-26")]
-abbrev unattach_nil := @unattach_empty
+@[simp] theorem unattach_nil {p : α → Prop} : (#v[] : Vector { x // p x } 0).unattach = #v[] := by simp
 
 @[simp] theorem unattach_push {p : α → Prop} {a : { x // p x }} {xs : Vector { x // p x } n} :
     (xs.push a).unattach = xs.unattach.push a.1 := by

src/Init/Data/Vector/Count.lean

@@ -40,8 +40,8 @@ theorem countP_push {a : α} {xs : Vector α n} : countP p (xs.push a) = countP
   rcases xs with ⟨xs, rfl⟩
   simp [Array.countP_push]
 
-theorem countP_singleton {a : α} : countP p #v[a] = if p a then 1 else 0 := by
-  simp
+@[simp] theorem countP_singleton {a : α} : countP p #v[a] = if p a then 1 else 0 := by
+  simp [countP_push]
 
 theorem size_eq_countP_add_countP {xs : Vector α n} : n = countP p xs + countP (fun a => ¬p a) xs := by
   rcases xs with ⟨xs, rfl⟩

src/Init/Data/Vector/DecidableEq.lean

@@ -48,18 +48,15 @@ theorem beq_eq_decide [BEq α] (xs ys : Vector α n) :
     (xs == ys) = decide (∀ (i : Nat) (h' : i < n), xs[i] == ys[i]) := by
   simp [BEq.beq, isEqv_eq_decide]
 
-@[deprecated mk_beq_mk (since := "2025-05-26")]
-theorem beq_mk [BEq α] (xs ys : Array α) (ha : xs.size = n) (hb : ys.size = n) :
+@[simp] theorem beq_mk [BEq α] (xs ys : Array α) (ha : xs.size = n) (hb : ys.size = n) :
     (mk xs ha == mk ys hb) = (xs == ys) := by
-  simp
+  simp [BEq.beq]
 
-@[deprecated toArray_beq_toArray (since := "2025-05-26")]
-theorem beq_toArray [BEq α] (xs ys : Vector α n) : (xs.toArray == ys.toArray) = (xs == ys) := by
-  simp
+@[simp, grind =] theorem beq_toArray [BEq α] (xs ys : Vector α n) : (xs.toArray == ys.toArray) = (xs == ys) := by
+  simp [beq_eq_decide, Array.beq_eq_decide]
 
-@[deprecated toList_beq_toList (since := "2025-05-26")]
-theorem beq_toList [BEq α] (xs ys : Vector α n) : (xs.toList == ys.toList) = (xs == ys) := by
-  simp
+@[simp] theorem beq_toList [BEq α] (xs ys : Vector α n) : (xs.toList == ys.toList) = (xs == ys) := by
+  simp [beq_eq_decide, List.beq_eq_decide]
 
 instance [BEq α] [ReflBEq α] : ReflBEq (Vector α n) where
   rfl := by simp [BEq.beq, isEqv_self_beq]

src/Init/Data/Vector/Find.lean

@@ -144,7 +144,7 @@ abbrev findSome?_mkVector_of_isNone := @findSome?_replicate_of_isNone
 
 @[simp] theorem find?_empty : find? p #v[] = none := rfl
 
-theorem find?_singleton {a : α} {p : α → Bool} :
+@[simp] theorem find?_singleton {a : α} {p : α → Bool} :
     #v[a].find? p = if p a then some a else none := by
   simp
 
@@ -291,8 +291,7 @@ theorem find?_eq_some_iff_getElem {xs : Vector α n} {p : α → Bool} {b : α}
 
 /-! ### findFinIdx? -/
 
-theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p (#v[] : Vector α 0) = none := by simp
-
+@[simp] theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p (#v[] : Vector α 0) = none := by simp
 theorem findFinIdx?_singleton {a : α} {p : α → Bool} :
     #[a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by
   simp

src/Init/Data/Vector/Lemmas.lean

@@ -684,7 +684,8 @@ abbrev toList_eq_empty_iff {α n} (xs) := @toList_eq_nil_iff α n xs
 
 /-! ### empty -/
 
-theorem empty_eq {xs : Vector α 0} : #v[] = xs ↔ xs = #v[] := by
+@[simp] theorem empty_eq {xs : Vector α 0} : #v[] = xs ↔ xs = #v[] := by
+  cases xs
   simp
 
 /-- A vector of length `0` is the empty vector. -/
@@ -841,13 +842,13 @@ theorem getElem_of_getElem? {xs : Vector α n} : xs[i]? = some a → ∃ h : i <
 theorem some_eq_getElem?_iff {xs : Vector α n} : some b = xs[i]? ↔ ∃ h : i < n, xs[i] = b :=
   _root_.some_eq_getElem?_iff
 
-theorem some_getElem_eq_getElem?_iff {xs : Vector α n} {i : Nat} (h : i < n) :
+@[simp] theorem some_getElem_eq_getElem?_iff {xs : Vector α n} {i : Nat} (h : i < n) :
     (some xs[i] = xs[i]?) ↔ True := by
-  simp
+  simp [h]
 
-theorem getElem?_eq_some_getElem_iff {xs : Vector α n} {i : Nat} (h : i < n) :
+@[simp] theorem getElem?_eq_some_getElem_iff {xs : Vector α n} {i : Nat} (h : i < n) :
     (xs[i]? = some xs[i]) ↔ True := by
-  simp
+  simp [h]
 
 theorem getElem_eq_iff {xs : Vector α n} {i : Nat} {h : i < n} : xs[i] = x ↔ xs[i]? = some x := by
   simp only [getElem?_eq_some_iff]
@@ -887,11 +888,12 @@ theorem getElem?_push {xs : Vector α n} {x : α} {i : Nat} : (xs.push x)[i]? =
   (repeat' split) <;> first | rfl | omega
 
 set_option linter.indexVariables false in
-theorem getElem?_push_size {xs : Vector α n} {x : α} : (xs.push x)[n]? = some x := by
-  simp
+@[simp] theorem getElem?_push_size {xs : Vector α n} {x : α} : (xs.push x)[n]? = some x := by
+  simp [getElem?_push]
 
-theorem getElem_singleton {a : α} (h : i < 1) : #v[a][i] = a := by
-  simp
+@[simp] theorem getElem_singleton {a : α} (h : i < 1) : #v[a][i] = a :=
+  match i, h with
+  | 0, _ => rfl
 
 @[grind]
 theorem getElem?_singleton {a : α} {i : Nat} : #v[a][i]? = if i = 0 then some a else none := by
@@ -903,7 +905,7 @@ theorem getElem?_singleton {a : α} {i : Nat} : #v[a][i]? = if i = 0 then some a
   rcases xs with ⟨xs, rfl⟩
   simp
 
-theorem not_mem_empty (a : α) : ¬ a ∈ #v[] := nofun
+@[simp] theorem not_mem_empty (a : α) : ¬ a ∈ #v[] := nofun
 
 @[simp] theorem mem_push {xs : Vector α n} {x y : α} : x ∈ xs.push y ↔ x ∈ xs ∨ x = y := by
   rcases xs with ⟨xs, rfl⟩
@@ -952,7 +954,8 @@ theorem size_zero_iff_forall_not_mem {xs : Vector α n} : n = 0 ↔ ∀ a, a ∉
 theorem eq_of_mem_singleton (h : a ∈ #v[b]) : a = b := by
   simpa using h
 
-theorem mem_singleton {a b : α} : a ∈ #v[b] ↔ a = b := by simp
+@[simp] theorem mem_singleton {a b : α} : a ∈ #v[b] ↔ a = b :=
+  ⟨eq_of_mem_singleton, (by simp [·])⟩
 
 theorem forall_mem_push {p : α → Prop} {xs : Vector α n} {a : α} :
     (∀ x, x ∈ xs.push a → p x) ↔ p a ∧ ∀ x, x ∈ xs → p x := by
@@ -1438,9 +1441,10 @@ theorem back_eq_getElem [NeZero n] {xs : Vector α n} : xs.back = xs[n - 1]'(by
   simp
 
 /-- The empty vector maps to the empty vector. -/
-@[grind]
+@[simp, grind]
 theorem map_empty {f : α → β} : map f #v[] = #v[] := by
-  simp
+  rw [map, mk.injEq]
+  exact Array.map_empty
 
 @[simp, grind] theorem map_push {f : α → β} {as : Vector α n} {x : α} :
     (as.push x).map f = (as.map f).push (f x) := by
@@ -1517,8 +1521,9 @@ theorem map_eq_push_iff {f : α → β} {xs : Vector α (n + 1)} {ys : Vector β
   · rintro ⟨xs', a, h₁, h₂, rfl⟩
     refine ⟨xs'.toArray, a, by simp_all⟩
 
-theorem map_eq_singleton_iff {f : α → β} {xs : Vector α 1} {b : β} :
+@[simp] theorem map_eq_singleton_iff {f : α → β} {xs : Vector α 1} {b : β} :
     map f xs = #v[b] ↔ ∃ a, xs = #v[a] ∧ f a = b := by
+  cases xs
   simp
 
 theorem map_eq_map_iff {f g : α → β} {xs : Vector α n} :
@@ -2353,13 +2358,13 @@ set_option linter.indexVariables false in
   rcases ys with ⟨ys, rfl⟩
   simp
 
-theorem foldlM_empty [Monad m] {f : β → α → m β} {init : β} :
+@[simp] theorem foldlM_empty [Monad m] {f : β → α → m β} {init : β} :
     foldlM f init #v[] = return init := by
-  simp
+  simp [foldlM]
 
-@[grind] theorem foldrM_empty [Monad m] {f : α → β → m β} {init : β} :
+@[simp, grind] theorem foldrM_empty [Monad m] {f : α → β → m β} {init : β} :
     foldrM f init #v[] = return init := by
-  simp
+  simp [foldrM]
 
 @[simp, grind] theorem foldlM_push [Monad m] [LawfulMonad m] {xs : Vector α n} {a : α} {f : β → α → m β} {b} :
     (xs.push a).foldlM f b = xs.foldlM f b >>= fun b => f b a := by
@@ -3050,7 +3055,8 @@ end replace
 /-! Content below this point has not yet been aligned with `List` and `Array`. -/
 
 set_option linter.indexVariables false in
-theorem getElem_push_last {xs : Vector α n} {x : α} : (xs.push x)[n] = x := by
+@[simp] theorem getElem_push_last {xs : Vector α n} {x : α} : (xs.push x)[n] = x := by
+  rcases xs with ⟨xs, rfl⟩
   simp
 
 @[simp] theorem push_pop_back (xs : Vector α (n + 1)) : xs.pop.push xs.back = xs := by
@@ -3082,7 +3088,8 @@ theorem getElem_push_last {xs : Vector α n} {x : α} : (xs.push x)[n] = x := by
 /-! ### take -/
 
 set_option linter.indexVariables false in
-theorem take_size {as : Vector α n} : as.take n = as.cast (by simp) := by
+@[simp] theorem take_size {as : Vector α n} : as.take n = as.cast (by simp) := by
+  rcases as with ⟨as, rfl⟩
   simp
 
 /-! ### swap -/
@@ -3131,8 +3138,9 @@ theorem swap_comm {xs : Vector α n} {i j : Nat} (hi hj) :
 
 /-! ### drop -/
 
-@[grind =] theorem getElem_drop {xs : Vector α n} {j : Nat} (hi : i < n - j) :
+@[simp, grind =] theorem getElem_drop {xs : Vector α n} {j : Nat} (hi : i < n - j) :
     (xs.drop j)[i] = xs[j + i] := by
+  cases xs
   simp
 
 /-! ### Decidable quantifiers. -/

src/Init/Data/Vector/Lex.lean

@@ -58,8 +58,9 @@ protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {xs ys
   cases xs
   simp_all
 
-theorem singleton_lex_singleton [BEq α] {lt : α → α → Bool} : #v[a].lex #v[b] lt = lt a b := by
-  simp
+@[simp] theorem singleton_lex_singleton [BEq α] {lt : α → α → Bool} : #v[a].lex #v[b] lt = lt a b := by
+  simp only [lex, getElem_mk, List.getElem_toArray, List.getElem_singleton]
+  cases lt a b <;> cases a != b <;> simp
 
 protected theorem lt_irrefl [LT α] [Std.Irrefl (· < · : α → α → Prop)] (xs : Vector α n) : ¬ xs < xs :=
   Array.lt_irrefl xs.toArray

src/Init/Data/Vector/MapIdx.lean

@@ -295,8 +295,9 @@ theorem mapIdx_eq_push_iff {xs : Vector α (n + 1)} {b : β} :
   · rintro ⟨a, zs, rfl, rfl, rfl⟩
     exact ⟨zs, a, rfl, by simp⟩
 
-theorem mapIdx_eq_singleton_iff {xs : Vector α 1} {f : Nat → α → β} {b : β} :
+@[simp] theorem mapIdx_eq_singleton_iff {xs : Vector α 1} {f : Nat → α → β} {b : β} :
     mapIdx f xs = #v[b] ↔ ∃ (a : α), xs = #v[a] ∧ f 0 a = b := by
+  rcases xs with ⟨xs⟩
   simp
 
 theorem mapIdx_eq_append_iff {xs : Vector α (n + m)} {f : Nat → α → β} {ys : Vector β n} {zs : Vector β m} :

src/Init/Data/Vector/Monadic.lean

@@ -25,10 +25,10 @@ open Nat
 
 /-! ## Monadic operations -/
 
-theorem map_toArray_inj [Monad m] [LawfulMonad m]
+@[simp] theorem map_toArray_inj [Monad m] [LawfulMonad m]
     {xs : m (Vector α n)} {ys : m (Vector α n)} :
-   toArray <$> xs = toArray <$> ys ↔ xs = ys := by
-  simp
+   toArray <$> xs = toArray <$> ys ↔ xs = ys :=
+  _root_.map_inj_right (by simp)
 
 /-! ### mapM -/
 
@@ -148,11 +148,11 @@ theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
   rcases xs with ⟨xs, rfl⟩
   simp [Array.forIn'_pure_yield_eq_foldl, Array.foldl_map]
 
-theorem idRun_forIn'_yield_eq_foldl
+@[simp] theorem idRun_forIn'_yield_eq_foldl
     {xs : Vector α n} (f : (a : α) → a ∈ xs → β → Id β) (init : β) :
     (forIn' xs init (fun a m b => .yield <$> f a m b)).run =
-      xs.attach.foldl (fun b ⟨a, h⟩ => f a h b |>.run) init := by
-  simp
+      xs.attach.foldl (fun b ⟨a, h⟩ => f a h b |>.run) init :=
+  forIn'_pure_yield_eq_foldl _ _
 
 @[deprecated forIn'_yield_eq_foldl (since := "2025-05-21")]
 theorem forIn'_yield_eq_foldl
@@ -196,11 +196,11 @@ theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
   rcases xs with ⟨xs, rfl⟩
   simp [Array.forIn_pure_yield_eq_foldl, Array.foldl_map]
 
-theorem idRun_forIn_yield_eq_foldl
+@[simp] theorem idRun_forIn_yield_eq_foldl
     {xs : Vector α n} (f : α → β → Id β) (init : β) :
     (forIn xs init (fun a b => .yield <$> f a b)).run =
-      xs.foldl (fun b a => f a b |>.run) init := by
-  simp
+      xs.foldl (fun b a => f a b |>.run) init :=
+  forIn_pure_yield_eq_foldl _ _
 
 @[deprecated idRun_forIn_yield_eq_foldl (since := "2025-05-21")]
 theorem forIn_yield_eq_foldl

src/Init/GetElem.lean

@@ -348,8 +348,7 @@ instance : GetElem? (List α) Nat α fun as i => i < as.length where
     | zero => rfl
     | succ i => exact ih ..
 
--- This is only needed locally; after the `LawfulGetElem` instance the general `getElem?_eq_none_iff` lemma applies.
-@[local simp] theorem getElem?_eq_none_iff : l[i]? = none ↔ length l ≤ i :=
+@[simp] theorem getElem?_eq_none_iff : l[i]? = none ↔ length l ≤ i :=
   match l with
   | [] => by simp; rfl
   | _ :: l => by
@@ -359,7 +358,7 @@ instance : GetElem? (List α) Nat α fun as i => i < as.length where
       simp only [length_cons, Nat.add_le_add_iff_right]
       exact getElem?_eq_none_iff (l := l) (i := i)
 
-theorem none_eq_getElem?_iff {l : List α} {i : Nat} : none = l[i]? ↔ length l ≤ i := by
+@[simp] theorem none_eq_getElem?_iff {l : List α} {i : Nat} : none = l[i]? ↔ length l ≤ i := by
   simp [eq_comm (a := none)]
 
 theorem getElem?_eq_none (h : length l ≤ i) : l[i]? = none := getElem?_eq_none_iff.mpr h

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean

@@ -218,7 +218,7 @@ theorem insert_iff {n : Nat} (f : DefaultFormula n) (c1 : DefaultClause n) (c2 :
         simp only [insert] at h
         split at h
         all_goals
-          simp only [Array.toList_push, List.mem_append, List.mem_singleton, Option.some.injEq] at h
+          simp only [Array.push_toList, List.mem_append, List.mem_singleton, Option.some.injEq] at h
           rcases h with h | h
           · exact h
           · exact False.elim <| c2_ne_c1 h
@@ -233,7 +233,7 @@ theorem insert_iff {n : Nat} (f : DefaultFormula n) (c1 : DefaultClause n) (c2 :
         simp only [insert]
         split
         all_goals
-          simp only [Array.toList_push, List.mem_append, List.mem_singleton, Option.some.injEq]
+          simp only [Array.push_toList, List.mem_append, List.mem_singleton, Option.some.injEq]
           exact Or.inl h
       · rw [rupUnits_insert]
         exact Or.inr <| Or.inl h
@@ -265,7 +265,7 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
     have hf := f_readyForRupAdd.2.2 i b hb
     simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right,
       List.mem_map, Prod.exists, Bool.exists_bool] at hf
-    simp only [toList, Array.toList_push, List.append_assoc, List.mem_append, List.mem_filterMap,
+    simp only [toList, Array.push_toList, List.append_assoc, List.mem_append, List.mem_filterMap,
       List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool]
     rcases hf with hf | hf
     · exact (Or.inl ∘ Or.inl) hf
@@ -280,7 +280,7 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
     simp only at hb
     by_cases (i, b) = (l, true)
     · next ib_eq_c =>
-      simp only [toList, Array.toList_push, List.append_assoc, List.mem_append, List.mem_filterMap,
+      simp only [toList, Array.push_toList, List.append_assoc, List.mem_append, List.mem_filterMap,
         List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool]
       apply Or.inl ∘ Or.inr
       rw [isUnit_iff, DefaultClause.toList, ← ib_eq_c] at hc
@@ -305,7 +305,7 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
       specialize hf hb'
       simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
         exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
-      simp only [toList, Array.toList_push, List.append_assoc, List.mem_append, List.mem_filterMap,
+      simp only [toList, Array.push_toList, List.append_assoc, List.mem_append, List.mem_filterMap,
         List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool]
       rcases hf with hf | hf
       · exact Or.inl <| Or.inl hf
@@ -320,7 +320,7 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
     simp only at hb
     by_cases (i, b) = (l, false)
     · next ib_eq_c =>
-      simp only [toList, Array.toList_push, List.append_assoc, List.mem_append, List.mem_filterMap,
+      simp only [toList, Array.push_toList, List.append_assoc, List.mem_append, List.mem_filterMap,
         List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool]
       apply Or.inl ∘ Or.inr
       rw [isUnit_iff, DefaultClause.toList, ← ib_eq_c] at hc
@@ -343,7 +343,7 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
       specialize hf hb'
       simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
         exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
-      simp only [toList, Array.toList_push, List.append_assoc, List.mem_append, List.mem_filterMap,
+      simp only [toList, Array.push_toList, List.append_assoc, List.mem_append, List.mem_filterMap,
         List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool]
       rcases hf with hf | hf
       · exact Or.inl <| Or.inl hf
@@ -374,7 +374,7 @@ theorem mem_of_insertRupUnits {n : Nat} (f : DefaultFormula n) (units : CNF.Clau
     dsimp at hl
     split at hl
     · exact ih l hl
-    · simp only [Array.toList_push, List.mem_append, List.mem_singleton] at hl
+    · simp only [Array.push_toList, List.mem_append, List.mem_singleton] at hl
       rcases hl with l_in_acc | l_eq_unit
       · exact ih l l_in_acc
       · rw [l_eq_unit]
@@ -411,7 +411,7 @@ theorem mem_of_insertRatUnits {n : Nat} (f : DefaultFormula n) (units : CNF.Clau
     dsimp at hl
     split at hl
     · exact ih l hl
-    · simp only [Array.toList_push, List.mem_append, List.mem_singleton] at hl
+    · simp only [Array.push_toList, List.mem_append, List.mem_singleton] at hl
       rcases hl with l_in_acc | l_eq_unit
       · exact ih l l_in_acc
       · rw [l_eq_unit]

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean

@@ -453,10 +453,10 @@ theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n)
     have i_eq_range_i : i = (Array.range f.clauses.size)[i]'i_in_bounds := by
       rw [Array.getElem_range]
     rw [i_eq_range_i]
-    rw [Array.mem_toList_iff]
+    rw [Array.mem_toList]
     rw [Array.mem_filter]
     constructor
-    · rw [← Array.mem_toList_iff]
+    · rw [← Array.mem_toList]
       apply Array.getElem_mem_toList
     · rw [Array.getElem_toList] at c'_in_f
       simp only [Array.getElem_range, getElem!_def, i_lt_f_clauses_size, Array.getElem?_eq_getElem,

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean

@@ -1109,7 +1109,7 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
   intro li_eq_lj
   let li := derivedLits_arr[i]
   have li_in_derivedLits : li ∈ derivedLits := by
-    rw [Array.mem_toList_iff, ← derivedLits_arr_def]
+    rw [Array.mem_toList, ← derivedLits_arr_def]
     simp [li, Array.getElem_mem]
   have i_in_bounds : i.1 < derivedLits.length := by
     have i_property := i.2

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean

@@ -100,7 +100,7 @@ theorem mem_insertUnit_units {n : Nat} (units : Array (Literal (PosFin n))) (ass
   simp only [insertUnit] at l'_in_insertUnit_res
   split at l'_in_insertUnit_res
   · exact Or.inr l'_in_insertUnit_res
-  · simp only [Array.toList_push, List.mem_append, List.mem_singleton] at l'_in_insertUnit_res
+  · simp only [Array.push_toList, List.mem_append, List.mem_singleton] at l'_in_insertUnit_res
     exact Or.symm l'_in_insertUnit_res
 
 theorem mem_insertUnit_fold_units {n : Nat} (units : Array (Literal (PosFin n))) (assignments : Array Assignment)

tests/lean/grind/experiments/bitvec.lean

@@ -64,9 +64,9 @@ theorem getElem?_eq (l : BitVec w) (i : Nat) :
     l[i]? = if h : i < w then some l[i] else none := by
   split <;> simp_all
 
-theorem some_getElem_eq_getElem? (l : BitVec w) (i : Nat) (h : i < w) :
+@[simp] theorem some_getElem_eq_getElem? (l : BitVec w) (i : Nat) (h : i < w) :
     (some l[i] = l[i]?) ↔ True := by
-  simp
+  simp [h]
 
 @[simp] theorem getElem?_eq_some_getElem (l : BitVec w) (i : Nat) (h : i < w) :
     (l[i]? = some l[i]) ↔ True := by
@@ -4882,9 +4882,10 @@ theorem and_one_eq_setWidth_ofBool_getLsbD {x : BitVec w} :
 theorem replicate_zero {x : BitVec w} : x.replicate 0 = 0#0 := by
   simp [replicate]
 
+@[simp]
 theorem replicate_one {w : Nat} {x : BitVec w} :
     (x.replicate 1) = x.cast (by rw [Nat.mul_one]) := by
-  simp
+  simp [replicate]
 
 @[simp]
 theorem replicate_succ {x : BitVec w} :

tests/lean/grind/experiments/list.lean

@@ -71,11 +71,11 @@ theorem some_eq_getElem?_iff {l : List α} : some a = l[i]? ↔ ∃ h : i < l.le
 
 theorem some_getElem_eq_getElem?_iff {xs : List α} {i : Nat} (h : i < xs.length) :
     (some xs[i] = xs[i]?) ↔ True := by
-  simp
+  simp [h]
 
 theorem getElem?_eq_some_getElem_iff {xs : List α} {i : Nat} (h : i < xs.length) :
     (xs[i]? = some xs[i]) ↔ True := by
-  simp
+  simp [h]
 
 theorem getElem_eq_iff {l : List α} {i : Nat} (h : i < l.length) : l[i] = x ↔ l[i]? = some x := by
   simp only [getElem?_eq_some_iff]