chore: cleanup simp lemmas, following the simpNF linter

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] using H) := by
+   (xs.attachWith P H).toList = xs.toList.attachWith P (by simpa [mem_toList_iff] using H) := by
   simp [attachWith]
 
 @[simp] theorem toList_attach {xs : Array α} :
-    xs.attach.toList = xs.toList.attachWith (· ∈ xs) (by simp [mem_toList]) := by
+    xs.attach.toList = xs.toList.attachWith (· ∈ xs) (by simp [mem_toList_iff]) := by
   simp [attach]
 
 @[simp] theorem toList_pmap {xs : Array α} {P : α → Prop} {f : ∀ a, P a → β} {H : ∀ a ∈ xs, P a} :
@@ -574,9 +574,12 @@ 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_nil {p : α → Prop} : (#[] : Array { x // p x }).unattach = #[] := by
+@[simp] theorem unattach_empty {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/Bootstrap.lean

@@ -89,9 +89,13 @@ 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 push_toList {xs : Array α} {a : α} : (xs.push a).toList = xs.toList ++ [a] := by
+@[simp, grind =] theorem toList_push {xs : Array α} {x : α} : (xs.push x).toList = xs.toList ++ [x] := by
+  rcases xs with ⟨xs⟩
   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
 
-@[simp] theorem countP_singleton {a : α} : countP p #[a] = if p a then 1 else 0 := by
-  simp [countP_push]
+theorem countP_singleton {a : α} : countP p #[a] = if p a then 1 else 0 := by
+  simp
 
 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 -/
 
-@[simp] theorem eraseP_empty : #[].eraseP p = #[] := by 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,11 +238,9 @@ theorem extract_append_left {as bs : Array α} :
     (as ++ bs).extract 0 as.size = as.extract 0 as.size := by
   simp
 
-@[simp] theorem extract_append_right {as bs : Array α} :
+theorem extract_append_right {as bs : Array α} :
     (as ++ bs).extract as.size (as.size + i) = bs.extract 0 i := by
-  simp only [extract_append, extract_size_left, Nat.sub_self, empty_append]
-  congr 1
-  omega
+  simp
 
 @[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
 
-@[simp] theorem find?_singleton {a : α} {p : α → Bool} :
+theorem find?_singleton {a : α} {p : α → Bool} :
     #[a].find? p = if p a then some a else none := by
-  simp [singleton_eq_toArray_singleton]
+  simp
 
 @[simp] theorem findRev?_push_of_pos {xs : Array α} (h : p a) :
     findRev? p (xs.push a) = some a := by
@@ -347,7 +347,8 @@ theorem find?_eq_some_iff_getElem {xs : Array α} {p : α → Bool} {b : α} :
 
 /-! ### findIdx -/
 
-@[simp] theorem findIdx_empty : findIdx p #[] = 0 := rfl
+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
@@ -600,7 +601,8 @@ theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : Array α} {p q : α → Bo
 
 /-! ### findFinIdx? -/
 
-@[simp] theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := by 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
@@ -699,7 +701,7 @@ The verification API for `idxOf?` is still incomplete.
 The lemmas below should be made consistent with those for `findIdx?` (and proved using them).
 -/
 
-@[simp] theorem idxOf?_empty [BEq α] : (#[] : Array α).idxOf? a = none := by 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
@@ -712,14 +714,10 @@ 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.
@@ -730,7 +728,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]
 
-@[simp] theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by 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
@@ -748,10 +746,8 @@ 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]
 
-@[simp] theorem some_getElem_eq_getElem?_iff (xs : Array α) (i : Nat) (h : i < xs.size) :
+theorem some_getElem_eq_getElem?_iff (xs : Array α) (i : Nat) (h : i < xs.size) :
     (some xs[i] = xs[i]?) ↔ True := by
-  simp [h]
+  simp
 
-@[simp] theorem getElem?_eq_some_getElem_iff (xs : Array α) (i : Nat) (h : i < xs.size) :
+theorem getElem?_eq_some_getElem_iff (xs : Array α) (i : Nat) (h : i < xs.size) :
     (xs[i]? = some xs[i]) ↔ True := by
-  simp [h]
+  simp
 
 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,12 +186,11 @@ 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
 
-@[simp] theorem getElem?_push_size {xs : Array α} {x} : (xs.push x)[xs.size]? = some x := by
-  simp [getElem?_push]
+theorem getElem?_push_size {xs : Array α} {x} : (xs.push x)[xs.size]? = some x := by
+  simp
 
-@[simp] theorem getElem_singleton {a : α} {i : Nat} (h : i < 1) : #[a][i] = a :=
-  match i, h with
-  | 0, _ => rfl
+theorem getElem_singleton {a : α} {i : Nat} (h : i < 1) : #[a][i] = a := by
+  simp
 
 @[grind]
 theorem getElem?_singleton {a : α} {i : Nat} : #[a][i]? = if i = 0 then some a else none := by
@@ -240,10 +239,6 @@ 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
@@ -423,8 +418,7 @@ 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
 
-@[simp] theorem mem_singleton {a b : α} : a ∈ #[b] ↔ a = b :=
-  ⟨eq_of_mem_singleton, (by simp [·])⟩
+theorem mem_singleton {a b : α} : a ∈ #[b] ↔ a = b := 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
@@ -868,8 +862,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]
 
-@[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
+@[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
 
 /-- 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) :
@@ -1228,7 +1222,7 @@ where
 @[simp] theorem mapM_empty [Monad m] (f : α → m β) : mapM f #[] = pure #[] := by
   rw [mapM, mapM.map]; rfl
 
-@[simp, grind] theorem map_empty {f : α → β} : map f #[] = #[] := mapM_empty f
+@[grind] theorem map_empty {f : α → β} : map f #[] = #[] := by simp
 
 @[simp, grind] theorem map_push {f : α → β} {as : Array α} {x : α} :
     (as.push x).map f = (as.map f).push (f x) := by
@@ -1813,7 +1807,8 @@ theorem toArray_append {xs : List α} {ys : Array α} :
 
 theorem singleton_eq_toArray_singleton {a : α} : #[a] = [a].toArray := rfl
 
-@[simp] theorem empty_append_fun : ((#[] : Array α) ++ ·) = id := by
+@[deprecated empty_append (since := "2025-05-26")]
+theorem empty_append_fun : ((#[] : Array α) ++ ·) = id := by
   funext ⟨l⟩
   simp
 
@@ -1964,8 +1959,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
 
-@[simp] theorem empty_eq_append_iff {xs ys : Array α} : #[] = xs ++ ys ↔ xs = #[] ∧ ys = #[] := by
-  rw [eq_comm, append_eq_empty_iff]
+theorem empty_eq_append_iff {xs ys : Array α} : #[] = xs ++ ys ↔ xs = #[] ∧ ys = #[] := by
+  simp
 
 theorem append_ne_empty_of_left_ne_empty {xs ys : Array α} (h : xs ≠ #[]) : xs ++ ys ≠ #[] := by
   simp_all
@@ -2033,7 +2028,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]
 
@@ -2108,14 +2103,13 @@ theorem append_eq_map_iff {f : α → β} :
   | nil => simp
   | cons as => induction as.toList <;> simp [*]
 
-@[simp] 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
   apply ext'
   simp [Function.comp_def]
 
-@[simp] theorem flatten_toArray_map {L : List (List α)} :
-    (L.map List.toArray).toArray.flatten = L.flatten.toArray := by
-  rw [← flatten_map_toArray]
+theorem flatten_map_toArray {L : List (List α)} :
+    (L.toArray.map List.toArray).flatten = L.flatten.toArray := by
   simp
 
 -- We set this to lower priority so that `flatten_toArray_map` is applied first when relevant.
@@ -2143,8 +2137,8 @@ theorem mem_flatten : ∀ {xss : Array (Array α)}, a ∈ xss.flatten ↔ ∃ xs
   induction xss using array₂_induction
   simp
 
-@[simp] theorem empty_eq_flatten_iff {xss : Array (Array α)} : #[] = xss.flatten ↔ ∀ xs ∈ xss, xs = #[] := by
-  rw [eq_comm, flatten_eq_empty_iff]
+theorem empty_eq_flatten_iff {xss : Array (Array α)} : #[] = xss.flatten ↔ ∀ xs ∈ xss, xs = #[] := by
+  simp
 
 theorem flatten_ne_empty_iff {xss : Array (Array α)} : xss.flatten ≠ #[] ↔ ∃ xs, xs ∈ xss ∧ xs ≠ #[] := by
   simp
@@ -2284,15 +2278,9 @@ theorem eq_iff_flatten_eq {xss₁ xss₂ : Array (Array α)} :
       rw [List.map_inj_right]
       simp +contextual
 
-@[simp] theorem flatten_toArray_map_toArray {xss : List (List α)} :
+theorem flatten_toArray_map_toArray {xss : List (List α)} :
     (xss.map List.toArray).toArray.flatten = xss.flatten.toArray := by
-  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]
+  simp
 
 /-! ### flatMap -/
 
@@ -2322,13 +2310,9 @@ theorem flatMap_toArray_cons {β} {f : α → Array β} {a : α} {as : List α}
   intro cs
   induction as generalizing cs <;> simp_all
 
-@[simp, grind =] theorem flatMap_toArray {β} {f : α → Array β} {as : List α} :
+theorem flatMap_toArray {β} {f : α → Array β} {as : List α} :
     as.toArray.flatMap f = (as.flatMap (fun a => (f a).toList)).toArray := by
-  induction as with
-  | nil => simp
-  | cons a as ih =>
-    apply ext'
-    simp [ih, flatMap_toArray_cons]
+  simp
 
 @[simp] theorem flatMap_id {xss : Array (Array α)} : xss.flatMap id = xss.flatten := by simp [flatMap_def]
 
@@ -3030,19 +3014,21 @@ theorem take_size {xs : Array α} : xs.take xs.size = xs := by
   | succ n ih =>
     simp [shrink.loop, ih]
 
-@[simp] theorem size_shrink {xs : Array α} {i : Nat} : (xs.shrink i).size = min i xs.size := by
+-- 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 [shrink]
   omega
 
-@[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
+-- 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 [shrink]
 
-@[simp] theorem toList_shrink {xs : Array α} {i : Nat} : (xs.shrink i).toList = xs.toList.take i := by
-  apply List.ext_getElem <;> simp
-
 @[simp] theorem shrink_eq_take {xs : Array α} {i : Nat} : xs.shrink i = xs.take i := by
-  ext <;> simp
+  ext <;> simp [size_shrink, getElem_shrink]
+
+theorem toList_shrink {xs : Array α} {i : Nat} : (xs.shrink i).toList = xs.toList.take i := by
+  simp
 
 /-! ### foldlM and foldrM -/
 
@@ -3249,7 +3235,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, push_toList, List.reverse_append, List.reverse_cons,
+  simp only [foldrM_eq_reverse_foldlM_toList, toList_push, List.reverse_append, List.reverse_cons,
     List.reverse_nil, List.nil_append, List.singleton_append, List.foldlM_cons, List.foldlM_reverse]
 
 /--
@@ -3654,7 +3640,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, push_toList]
+  simp only [List.back?_toArray, List.getLast?_eq_some_iff, toArray_eq, toList_push]
   constructor
   · rintro ⟨ys, rfl⟩
     exact ⟨ys.toArray, by simp⟩
@@ -4425,7 +4411,8 @@ theorem getElem!_eq_getD [Inhabited α] {xs : Array α} {i} : xs[i]! = xs.getD i
 
 /-! # mem -/
 
-@[simp, grind =] theorem mem_toList {a : α} {xs : Array α} : a ∈ xs.toList ↔ a ∈ xs := mem_def.symm
+@[deprecated mem_toList_iff (since := "2025-05-26")]
+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
@@ -4474,7 +4461,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.mpr m) b) := by
+    forIn' xs.toList b f = forIn' xs b (fun a m b => f a (mem_toList_iff.mpr m) b) := by
   cases xs
   simp
 
@@ -4571,8 +4558,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
 
-@[simp, grind =] theorem take_toArray {l : List α} {i : Nat} : l.toArray.take i = (l.take i).toArray := by
-  apply Array.ext <;> simp
+@[grind =] theorem take_toArray {l : List α} {i : Nat} : l.toArray.take i = (l.take i).toArray := by
+  simp
 
 @[simp, grind =] theorem mapM_toArray [Monad m] [LawfulMonad m] {f : α → m β} {l : List α} :
     l.toArray.mapM f = List.toArray <$> l.mapM f := by