fix test

src/Init/Data/Array/Basic.lean

@@ -91,7 +91,8 @@ theorem ext' {xs ys : Array α} (h : xs.toList = ys.toList) : xs = ys := by
 @[simp, grind =] theorem getElem_toList {xs : Array α} {i : Nat} (h : i < xs.size) : xs.toList[i] = xs[i] := rfl
 
 @[simp, grind =] theorem getElem?_toList {xs : Array α} {i : Nat} : xs.toList[i]? = xs[i]? := by
-  simp [getElem?_def]
+  simp only [getElem?_def, getElem_toList]
+  simp only [Array.size]
 
 /-- `a ∈ as` is a predicate which asserts that `a` is in the array `as`. -/
 -- NB: This is defined as a structure rather than a plain def so that a lemma

src/Init/Data/Array/Bootstrap.lean

@@ -78,7 +78,8 @@ theorem foldrM_eq_reverse_foldlM_toList [Monad m] {f : α → β → m β} {init
   have : xs = #[] ∨ 0 < xs.size :=
     match xs with | ⟨[]⟩ => .inl rfl | ⟨a::l⟩ => .inr (Nat.zero_lt_succ _)
   match xs, this with | _, .inl rfl => simp [foldrM] | xs, .inr h => ?_
-  simp [foldrM, h, ← foldrM_eq_reverse_foldlM_toList.aux, List.take_length]
+  simp only [foldrM, h, ← foldrM_eq_reverse_foldlM_toList.aux]
+  simp [Array.size]
 
 @[simp, grind =] theorem foldrM_toList [Monad m]
     {f : α → β → m β} {init : β} {xs : Array α} :

src/Init/Data/Array/Count.lean

@@ -105,6 +105,7 @@ theorem boole_getElem_le_countP {xs : Array α} {i : Nat} (h : i < xs.size) :
 theorem countP_set {xs : Array α} {i : Nat} {a : α} (h : i < xs.size) :
     (xs.set i a).countP p = xs.countP p - (if p xs[i] then 1 else 0) + (if p a then 1 else 0) := by
   rcases xs with ⟨xs⟩
+  simp at h
   simp [List.countP_set, h]
 
 theorem countP_filter {xs : Array α} :

src/Init/Data/Array/DecidableEq.lean

@@ -69,7 +69,7 @@ theorem isEqv_eq_decide (xs ys : Array α) (r) :
     simpa [isEqv_iff_rel] using h'
 
 @[simp, grind =] theorem isEqv_toList [BEq α] (xs ys : Array α) : (xs.toList.isEqv ys.toList r) = (xs.isEqv ys r) := by
-  simp [isEqv_eq_decide, List.isEqv_eq_decide]
+  simp [isEqv_eq_decide, List.isEqv_eq_decide, Array.size]
 
 theorem eq_of_isEqv [DecidableEq α] (xs ys : Array α) (h : Array.isEqv xs ys (fun x y => x = y)) : xs = ys := by
   have ⟨h, h'⟩ := rel_of_isEqv h
@@ -100,7 +100,7 @@ theorem beq_eq_decide [BEq α] (xs ys : Array α) :
   simp [BEq.beq, isEqv_eq_decide]
 
 @[simp, grind =] theorem beq_toList [BEq α] (xs ys : Array α) : (xs.toList == ys.toList) = (xs == ys) := by
-  simp [beq_eq_decide, List.beq_eq_decide]
+  simp [beq_eq_decide, List.beq_eq_decide, Array.size]
 
 end Array
 

src/Init/Data/Array/Find.lean

@@ -655,13 +655,13 @@ theorem findFinIdx?_append {xs ys : Array α} {p : α → Bool} :
 theorem isSome_findFinIdx? {xs : Array α} {p : α → Bool} :
     (xs.findFinIdx? p).isSome = xs.any p := by
   rcases xs with ⟨xs⟩
-  simp
+  simp [Array.size]
 
 @[simp]
 theorem isNone_findFinIdx? {xs : Array α} {p : α → Bool} :
     (xs.findFinIdx? p).isNone = xs.all (fun x => ¬ p x) := by
   rcases xs with ⟨xs⟩
-  simp
+  simp [Array.size]
 
 @[simp] theorem findFinIdx?_subtype {p : α → Prop} {xs : Array { x // p x }}
     {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
@@ -669,7 +669,8 @@ theorem isNone_findFinIdx? {xs : Array α} {p : α → Bool} :
   cases xs
   simp only [List.findFinIdx?_toArray, hf, List.findFinIdx?_subtype]
   rw [findFinIdx?_congr List.unattach_toArray]
-  simp [Function.comp_def]
+  simp only [Option.map_map, Function.comp_def, Fin.cast_trans]
+  simp [Array.size]
 
 /-! ### idxOf
 
@@ -733,18 +734,19 @@ theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by sim
 @[simp] theorem finIdxOf?_eq_none_iff [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     xs.finIdxOf? a = none ↔ a ∉ xs := by
   rcases xs with ⟨xs⟩
-  simp [List.finIdxOf?_eq_none_iff]
+  simp [List.finIdxOf?_eq_none_iff, Array.size]
 
 @[simp] theorem finIdxOf?_eq_some_iff [BEq α] [LawfulBEq α] {xs : Array α} {a : α} {i : Fin xs.size} :
     xs.finIdxOf? a = some i ↔ xs[i] = a ∧ ∀ j (_ : j < i), ¬xs[j] = a := by
   rcases xs with ⟨xs⟩
+  unfold Array.size at i ⊢
   simp [List.finIdxOf?_eq_some_iff]
 
 @[simp]
 theorem isSome_finIdxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     (xs.finIdxOf? a).isSome ↔ a ∈ xs := by
   rcases xs with ⟨xs⟩
-  simp
+  simp [Array.size]
 
 theorem isNone_finIdxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     (xs.finIdxOf? a).isNone = ¬ a ∈ xs := by

src/Init/Data/Array/InsertIdx.lean

@@ -44,6 +44,7 @@ theorem insertIdx_zero {xs : Array α} {x : α} : xs.insertIdx 0 x = #[x] ++ xs
 
 @[simp] theorem size_insertIdx {xs : Array α} (h : i ≤ xs.size) : (xs.insertIdx i a).size = xs.size + 1 := by
   rcases xs with ⟨xs⟩
+  simp at h
   simp [List.length_insertIdx, h]
 
 theorem eraseIdx_insertIdx {i : Nat} {xs : Array α} (h : i ≤ xs.size) :

src/Init/Data/Array/Lemmas.lean

@@ -75,7 +75,7 @@ theorem ne_empty_of_size_pos (h : 0 < xs.size) : xs ≠ #[] := by
   cases xs
   simpa using List.ne_nil_of_length_pos h
 
-theorem size_eq_zero_iff : xs.size = 0 ↔ xs = #[] :=
+@[simp] theorem size_eq_zero_iff : xs.size = 0 ↔ xs = #[] :=
   ⟨eq_empty_of_size_eq_zero, fun h => h ▸ rfl⟩
 
 @[deprecated size_eq_zero_iff (since := "2025-02-24")]
@@ -169,6 +169,7 @@ theorem getD_getElem? {xs : Array α} {i : Nat} {d : α} :
 theorem getElem_push_lt {xs : Array α} {x : α} {i : Nat} (h : i < xs.size) :
     have : i < (xs.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]
     (xs.push x)[i] = xs[i] := by
+  rw [Array.size] at h
   simp only [push, ← getElem_toList, List.concat_eq_append, List.getElem_append_left, h]
 
 @[simp] theorem getElem_push_eq {xs : Array α} {x : α} : (xs.push x)[xs.size] = x := by
@@ -1858,7 +1859,7 @@ theorem getElem_append_right {xs ys : Array α} {h : i < (xs ++ ys).size} (hle :
     (xs ++ ys)[i] = ys[i - xs.size]'(Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h)) := by
   simp only [← getElem_toList]
   have h' : i < (xs.toList ++ ys.toList).length := by rwa [← length_toList, toList_append] at h
-  conv => rhs; rw [← List.getElem_append_right (h₁ := hle) (h₂ := h')]
+  conv => rhs; unfold Array.size; rw [← List.getElem_append_right (h₁ := hle) (h₂ := h')]
   apply List.get_of_eq; rw [toList_append]
 
 theorem getElem?_append_left {xs ys : Array α} {i : Nat} (hn : i < xs.size) :
@@ -2025,7 +2026,7 @@ theorem append_eq_append_iff {ws xs ys zs : Array α} :
         xs ++ ys.set (i - xs.size) x (by simp at h; omega) := by
   rcases xs with ⟨s⟩
   rcases ys with ⟨t⟩
-  simp only [List.append_toArray, List.set_toArray, List.set_append]
+  simp only [List.append_toArray, List.set_toArray, List.set_append, Array.size]
   split <;> simp
 
 @[simp] theorem set_append_left {xs ys : Array α} {i : Nat} {x : α} (h : i < xs.size)  :
@@ -2045,7 +2046,7 @@ theorem append_eq_append_iff {ws xs ys zs : Array α} :
         xs ++ ys.setIfInBounds (i - xs.size) x := by
   rcases xs with ⟨s⟩
   rcases ys with ⟨t⟩
-  simp only [List.append_toArray, List.setIfInBounds_toArray, List.set_append]
+  simp only [List.append_toArray, List.setIfInBounds_toArray, List.set_append, Array.size]
   split <;> simp
 
 @[simp] theorem setIfInBounds_append_left {xs ys : Array α} {i : Nat} {x : α} (h : i < xs.size) :
@@ -4500,6 +4501,7 @@ abbrev contains_def [DecidableEq α] {a : α} {xs : Array α} : xs.contains a
 @[simp] theorem size_zipWith {xs : Array α} {ys : Array β} {f : α → β → γ} :
     (zipWith f xs ys).size = min xs.size ys.size := by
   rw [size_eq_length_toList, toList_zipWith, List.length_zipWith]
+  simp only [Array.size]
 
 @[simp] theorem size_zip {xs : Array α} {ys : Array β} :
     (zip xs ys).size = min xs.size ys.size :=
@@ -4572,7 +4574,7 @@ theorem toListRev_toArray {l : List α} : l.toArray.toListRev = l.reverse := by
   | nil => simp
   | cons a l ih =>
     simp only [foldlM_toArray] at ih
-    rw [size_toArray, mapM'_cons, foldlM_toArray]
+    rw [size_toArray, mapM'_cons]
     simp [ih]
 
 theorem uset_toArray {l : List α} {i : USize} {a : α} {h : i.toNat < l.toArray.size} :

src/Init/Data/Array/MapIdx.lean

@@ -192,7 +192,8 @@ theorem mapFinIdx_empty {f : (i : Nat) → α → (h : i < 0) → β} : mapFinId
 theorem mapFinIdx_eq_ofFn {xs : Array α} {f : (i : Nat) → α → (h : i < xs.size) → β} :
     xs.mapFinIdx f = Array.ofFn fun i : Fin xs.size => f i xs[i] i.2 := by
   cases xs
-  simp [List.mapFinIdx_eq_ofFn]
+  simp only [List.mapFinIdx_toArray, List.mapFinIdx_eq_ofFn, Fin.getElem_fin, List.getElem_toArray]
+  simp [Array.size]
 
 theorem mapFinIdx_append {xs ys : Array α} {f : (i : Nat) → α → (h : i < (xs ++ ys).size) → β} :
     (xs ++ ys).mapFinIdx f =
@@ -200,7 +201,7 @@ theorem mapFinIdx_append {xs ys : Array α} {f : (i : Nat) → α → (h : i < (
         ys.mapFinIdx (fun i a h => f (i + xs.size) a (by simp; omega)) := by
   cases xs
   cases ys
-  simp [List.mapFinIdx_append]
+  simp [List.mapFinIdx_append, Array.size]
 
 @[simp]
 theorem mapFinIdx_push {xs : Array α} {a : α} {f : (i : Nat) → α → (h : i < (xs.push a).size) → β} :
@@ -264,12 +265,12 @@ theorem mapFinIdx_eq_append_iff {xs : Array α} {f : (i : Nat) → α → (h : i
     toArray_eq_append_iff]
   constructor
   · rintro ⟨l₁, l₂, rfl, rfl, rfl⟩
-    refine ⟨l₁.toArray, l₂.toArray, by simp_all⟩
+    refine ⟨l₁.toArray, l₂.toArray, by simp_all [Array.size]⟩
   · rintro ⟨⟨l₁⟩, ⟨l₂⟩, rfl, h₁, h₂⟩
     simp [← toList_inj] at h₁ h₂
     obtain rfl := h₁
     obtain rfl := h₂
-    refine ⟨l₁, l₂, by simp_all⟩
+    refine ⟨l₁, l₂, by simp_all [Array.size]⟩
 
 theorem mapFinIdx_eq_push_iff {xs : Array α} {b : β} {f : (i : Nat) → α → (h : i < xs.size) → β} :
     xs.mapFinIdx f = ys.push b ↔
@@ -307,7 +308,7 @@ abbrev mapFinIdx_eq_mkArray_iff := @mapFinIdx_eq_replicate_iff
 @[simp] theorem mapFinIdx_reverse {xs : Array α} {f : (i : Nat) → α → (h : i < xs.reverse.size) → β} :
     xs.reverse.mapFinIdx f = (xs.mapFinIdx (fun i a h => f (xs.size - 1 - i) a (by simp; omega))).reverse := by
   rcases xs with ⟨l⟩
-  simp [List.mapFinIdx_reverse]
+  simp [List.mapFinIdx_reverse, Array.size]
 
 /-! ### mapIdx -/
 
@@ -486,7 +487,7 @@ namespace List
     | x :: xs => simp only [mapFinIdxM.go, mapIdxM.go, go]
   unfold Array.mapIdxM
   rw [mapFinIdxM_toArray]
-  simp only [mapFinIdxM, mapIdxM]
+  simp only [mapFinIdxM, mapIdxM, Array.size]
   rw [go]
 
 end List

src/Init/Data/Array/Monadic.lean

@@ -310,7 +310,7 @@ namespace List
 @[simp] theorem filterM_toArray' [Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool} (w : stop = l.length) :
     l.toArray.filterM p 0 stop = toArray <$> l.filterM p := by
   subst w
-  rw [filterM_toArray]
+  simp [← filterM_toArray]
 
 @[grind =] theorem filterRevM_toArray [Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool} :
     l.toArray.filterRevM p = toArray <$> l.filterRevM p := by
@@ -322,7 +322,7 @@ namespace List
 @[simp] theorem filterRevM_toArray' [Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool} (w : start = l.length) :
     l.toArray.filterRevM p start 0 = toArray <$> l.filterRevM p := by
   subst w
-  rw [filterRevM_toArray]
+  simp [← filterRevM_toArray]
 
 @[grind =] theorem filterMapM_toArray [Monad m] [LawfulMonad m] {l : List α} {f : α → m (Option β)} :
     l.toArray.filterMapM f = toArray <$> l.filterMapM f := by
@@ -340,7 +340,7 @@ namespace List
 @[simp] theorem filterMapM_toArray' [Monad m] [LawfulMonad m] {l : List α} {f : α → m (Option β)} (w : stop = l.length) :
     l.toArray.filterMapM f 0 stop = toArray <$> l.filterMapM f := by
   subst w
-  rw [filterMapM_toArray]
+  simp [← filterMapM_toArray]
 
 @[simp, grind =] theorem flatMapM_toArray [Monad m] [LawfulMonad m] {l : List α} {f : α → m (Array β)} :
     l.toArray.flatMapM f = toArray <$> l.flatMapM (fun a => Array.toList <$> f a) := by

src/Init/Data/List/Impl.lean

@@ -550,7 +550,7 @@ def zipIdxTR (l : List α) (n : Nat := 0) : List (α × Nat) :=
   (as.foldr (fun a (n, acc) => (n-1, (a, n-1) :: acc)) (n + as.size, [])).2
 
 @[csimp] theorem zipIdx_eq_zipIdxTR : @zipIdx = @zipIdxTR := by
-  funext α l n; simp only [zipIdxTR, size_toArray]
+  funext α l n; simp only [zipIdxTR]
   let f := fun (a : α) (n, acc) => (n-1, (a, n-1) :: acc)
   let rec go : ∀ l i, l.foldr f (i + l.length, []) = (i, zipIdx l i)
     | [], n => rfl
@@ -571,7 +571,7 @@ def enumFromTR (n : Nat) (l : List α) : List (Nat × α) :=
 set_option linter.deprecated false in
 @[deprecated zipIdx_eq_zipIdxTR (since := "2025-01-21"), csimp]
 theorem enumFrom_eq_enumFromTR : @enumFrom = @enumFromTR := by
-  funext α n l; simp only [enumFromTR, size_toArray]
+  funext α n l; simp only [enumFromTR]
   let f := fun (a : α) (n, acc) => (n-1, (n-1, a) :: acc)
   let rec go : ∀ l n, l.foldr f (n + l.length, []) = (n, enumFrom n l)
     | [], n => rfl

src/Init/Data/List/MapIdx.lean

@@ -320,7 +320,7 @@ theorem mapIdx_nil {f : Nat → α → β} : mapIdx f [] = [] :=
 theorem mapIdx_go_length {acc : Array β} :
     length (mapIdx.go f l acc) = length l + acc.size := by
   induction l generalizing acc with
-  | nil => simp only [mapIdx.go, length_nil, Nat.zero_add]
+  | nil => simp [mapIdx.go]
   | cons _ _ ih =>
     simp only [mapIdx.go, ih, Array.size_push, Nat.add_succ, length_cons, Nat.add_comm]
 

src/Init/Data/List/ToArray.lean

@@ -302,7 +302,7 @@ termination_by l.length - j
 @[simp, grind =] theorem findIdx?_toArray (p : α → Bool) (l : List α) :
     l.toArray.findIdx? p = l.findIdx? p := by
   rw [Array.findIdx?_eq_map_findFinIdx?_val, findIdx?_eq_map_findFinIdx?_val]
-  simp
+  simp [Array.size]
 
 private theorem idxAuxOf_toArray [BEq α] (a : α) (l : List α) (j : Nat) (w : l' = l.drop j) (h) :
     l.toArray.idxOfAux a j = findFinIdx?.go (fun x => x == a) l l' j h := by
@@ -339,11 +339,11 @@ termination_by l.length - j
 @[simp, grind =] theorem idxOf?_toArray [BEq α] (a : α) (l : List α) :
     l.toArray.idxOf? a = l.idxOf? a := by
   rw [Array.idxOf?, idxOf?]
-  simp [finIdxOf?, findIdx?_eq_map_findFinIdx?_val]
+  simp [finIdxOf?, findIdx?_eq_map_findFinIdx?_val, Array.size]
 
 @[simp, grind =] theorem findIdx_toArray {as : List α} {p : α → Bool} :
     as.toArray.findIdx p = as.findIdx p := by
-  rw [Array.findIdx, findIdx?_toArray, findIdx_eq_getD_findIdx?]
+  rw [Array.findIdx, findIdx?_toArray, findIdx_eq_getD_findIdx?, Array.size]
 
 @[simp, grind =] theorem idxOf_toArray [BEq α] {as : List α} {a : α} :
     as.toArray.idxOf a = as.idxOf a := by
@@ -670,9 +670,9 @@ theorem replace_toArray [BEq α] [LawfulBEq α] (l : List α) (a b : α) :
   split <;> rename_i i h
   · simp only [finIdxOf?_toArray, finIdxOf?_eq_none_iff] at h
     rw [replace_of_not_mem]
-    simpa
+    exact finIdxOf?_eq_none_iff.mp h
   · simp_all only [finIdxOf?_toArray, finIdxOf?_eq_some_iff, Fin.getElem_fin, set_toArray,
-      mk.injEq]
+      mk.injEq, Array.size]
     apply List.ext_getElem
     · simp
     · intro j h₁ h₂

src/Init/Data/Option/Array.lean

@@ -84,7 +84,7 @@ theorem toArray_eq_singleton_iff {o : Option α} : o.toArray = #[a] ↔ o = some
 
 theorem size_toArray_eq_zero_iff {o : Option α} :
     o.toArray.size = 0 ↔ o = none := by
-  simp
+  simp [Array.size]
 
 @[simp]
 theorem size_toArray_eq_one_iff {o : Option α} :

src/Init/Data/Vector/Count.lean

@@ -45,7 +45,7 @@ theorem countP_singleton {a : α} : countP p #v[a] = if p a then 1 else 0 := by
 
 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⟩
-  simp [List.length_eq_countP_add_countP (p := p)]
+  simp [Array.size_eq_countP_add_countP (p := p)]
 
 theorem countP_le_size {xs : Vector α n} : countP p xs ≤ n := by
   rcases xs with ⟨xs, rfl⟩

src/Init/Data/Vector/Lemmas.lean

@@ -698,7 +698,7 @@ protected theorem eq_empty {xs : Vector α 0} : xs = #v[] := by
 theorem eq_empty_of_size_eq_zero {xs : Vector α n} (h : n = 0) : xs = #v[].cast h.symm := by
   rcases xs with ⟨xs, rfl⟩
   apply toArray_inj.1
-  simp only [List.length_eq_zero_iff, Array.toList_eq_nil_iff] at h
+  simp only [Array.size_eq_zero_iff] at h
   simp [h]
 
 theorem size_eq_one {xs : Vector α 1} : ∃ a, xs = #v[a] := by

src/Init/Prelude.lean

@@ -3000,7 +3000,7 @@ This is a cached value, so it is `O(1)` to access. The space allocated for an ar
 its _capacity_, is at least as large as its size, but may be larger. The capacity of an array is an
 internal detail that's not observable by Lean code.
 -/
-@[reducible, extern "lean_array_get_size"]
+@[extern "lean_array_get_size"]
 def Array.size {α : Type u} (a : @& Array α) : Nat :=
  a.toList.length
 

tests/lean/run/grind_nested_proofs.lean

@@ -22,7 +22,7 @@ detect equalities between array access terms.
 -/
 
 /--
-trace: [Meta.debug] [‹i < a.toList.length›, ‹j < a.toList.length›, ‹j < b.toList.length›]
+trace: [Meta.debug] [‹i < a.size›, ‹j < a.size›, ‹j < b.size›]
 [Meta.debug] [a[i], b[j], a[j]]
 -/
 #guard_msgs (trace) in
@@ -30,7 +30,7 @@ example (i j : Nat) (a b : Array Nat) (h1 : j < a.size) (h : j < b.size) (h2 : i
   grind -mbtc on_failure fallback
 
 /--
-trace: [Meta.debug] [‹i < a.toList.length›, ‹j < a.toList.length›, ‹j < b.toList.length›]
+trace: [Meta.debug] [‹i < a.size›, ‹j < a.size›, ‹j < b.size›]
 [Meta.debug] [a[i], a[j]]
 -/
 #guard_msgs (trace) in