fix test

src/Init/Data/Array/Attach.lean

@@ -149,24 +149,23 @@ theorem pmap_eq_attachWith {p q : α → Prop} (f : ∀ a, p a → q a) (l H) :
   cases l
   simp [List.pmap_eq_attachWith]
 
-theorem attach_map_coe (l : Array α) (f : α → β) :
+theorem attach_map_val (l : Array α) (f : α → β) :
     (l.attach.map fun (i : {i // i ∈ l}) => f i) = l.map f := by
   cases l
   simp
 
-theorem attach_map_val (l : Array α) (f : α → β) : (l.attach.map fun i => f i.val) = l.map f :=
-  attach_map_coe _ _
+@[deprecated attach_map_val (since := "2025-02-17")]
+abbrev attach_map_coe := @attach_map_val
 
 theorem attach_map_subtype_val (l : Array α) : l.attach.map Subtype.val = l := by
   cases l; simp
 
-theorem attachWith_map_coe {p : α → Prop} (f : α → β) (l : Array α) (H : ∀ a ∈ l, p a) :
+theorem attachWith_map_val {p : α → Prop} (f : α → β) (l : Array α) (H : ∀ a ∈ l, p a) :
     ((l.attachWith p H).map fun (i : { i // p i}) => f i) = l.map f := by
   cases l; simp
 
-theorem attachWith_map_val {p : α → Prop} (f : α → β) (l : Array α) (H : ∀ a ∈ l, p a) :
-    ((l.attachWith p H).map fun i => f i.val) = l.map f :=
-  attachWith_map_coe _ _ _
+@[deprecated attachWith_map_val (since := "2025-02-17")]
+abbrev attachWith_map_coe := @attachWith_map_val
 
 theorem attachWith_map_subtype_val {p : α → Prop} (l : Array α) (H : ∀ a ∈ l, p a) :
     (l.attachWith p H).map Subtype.val = l := by
@@ -318,7 +317,7 @@ See however `foldl_subtype` below.
 theorem foldl_attach (l : Array α) (f : β → α → β) (b : β) :
     l.attach.foldl (fun acc t => f acc t.1) b = l.foldl f b := by
   rcases l with ⟨l⟩
-  simp only [List.attach_toArray, List.attachWith_mem_toArray, size_toArray,
+  simp only [List.attach_toArray, List.attachWith_mem_toArray, List.size_toArray,
     List.length_pmap, List.foldl_toArray', mem_toArray, List.foldl_subtype]
   congr
   ext
@@ -337,7 +336,7 @@ See however `foldr_subtype` below.
 theorem foldr_attach (l : Array α) (f : α → β → β) (b : β) :
     l.attach.foldr (fun t acc => f t.1 acc) b = l.foldr f b := by
   rcases l with ⟨l⟩
-  simp only [List.attach_toArray, List.attachWith_mem_toArray, size_toArray,
+  simp only [List.attach_toArray, List.attachWith_mem_toArray, List.size_toArray,
     List.length_pmap, List.foldr_toArray', mem_toArray, List.foldr_subtype]
   congr
   ext
@@ -645,7 +644,7 @@ and simplifies these to the function directly taking the value.
     {f : { x // p x } → Option β} {g : α → Option β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     l.filterMap f = l.unattach.filterMap g := by
   cases l
-  simp only [size_toArray, List.filterMap_toArray', List.unattach_toArray, List.length_unattach,
+  simp only [List.size_toArray, List.filterMap_toArray', List.unattach_toArray, List.length_unattach,
     mk.injEq]
   rw [List.filterMap_subtype]
   simp [hf]
@@ -655,7 +654,7 @@ and simplifies these to the function directly taking the value.
     {f : { x // p x } → Array β} {g : α → Array β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     (l.flatMap f) = l.unattach.flatMap g := by
   cases l
-  simp only [size_toArray, List.flatMap_toArray, List.unattach_toArray, List.length_unattach,
+  simp only [List.size_toArray, List.flatMap_toArray, List.unattach_toArray, List.length_unattach,
     mk.injEq]
   rw [List.flatMap_subtype]
   simp [hf]

src/Init/Data/Array/Basic.lean

@@ -83,10 +83,7 @@ theorem ext' {as bs : Array α} (h : as.toList = bs.toList) : as = bs := by
 @[simp] theorem toArrayAux_eq (as : List α) (acc : Array α) : (as.toArrayAux acc).toList = acc.toList ++ as := by
   induction as generalizing acc <;> simp [*, List.toArrayAux, Array.push, List.append_assoc, List.concat_eq_append]
 
--- This does not need to be a simp lemma, as already after the `whnfR` the right hand side is `as`.
-theorem toList_toArray (as : List α) : as.toArray.toList = as := rfl
-
-@[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]
+@[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl
 
 @[simp] theorem getElem_toList {a : Array α} {i : Nat} (h : i < a.size) : a.toList[i] = a[i] := rfl
 
@@ -115,7 +112,19 @@ end Array
 
 namespace List
 
-@[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl
+@[deprecated Array.toArray_toList (since := "2025-02-17")]
+abbrev toArray_toList := @Array.toArray_toList
+
+-- This does not need to be a simp lemma, as already after the `whnfR` the right hand side is `as`.
+theorem toList_toArray (as : List α) : as.toArray.toList = as := rfl
+
+@[deprecated toList_toArray (since := "2025-02-17")]
+abbrev _root_.Array.toList_toArray := @List.toList_toArray
+
+@[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [Array.size]
+
+@[deprecated size_toArray (since := "2025-02-17")]
+abbrev _root_.Array.size_toArray := @List.size_toArray
 
 @[simp] theorem getElem_toArray {a : List α} {i : Nat} (h : i < a.toArray.size) :
     a.toArray[i] = a[i]'(by simpa using h) := rfl
@@ -130,7 +139,7 @@ end List
 
 namespace Array
 
-@[deprecated toList_toArray (since := "2024-09-09")] abbrev data_toArray := @toList_toArray
+@[deprecated toList_toArray (since := "2024-09-09")] abbrev data_toArray := @List.toList_toArray
 
 @[deprecated Array.toList (since := "2024-09-10")] abbrev Array.data := @Array.toList
 

src/Init/Data/Array/Bootstrap.lean

@@ -69,7 +69,10 @@ theorem foldrM_eq_reverse_foldlM_toList [Monad m] (f : α → β → m β) (init
 @[simp] theorem toListImpl_eq (arr : Array α) : arr.toListImpl = arr.toList := by
   simp [toListImpl, ← foldr_toList]
 
-@[simp] theorem pop_toList (arr : Array α) : arr.pop.toList = arr.toList.dropLast := rfl
+@[simp] theorem toList_pop (a : Array α) : a.pop.toList = a.toList.dropLast := rfl
+
+@[deprecated toList_pop (since := "2025-02-17")]
+abbrev pop_toList := @Array.toList_pop
 
 @[simp] theorem append_eq_append (arr arr' : Array α) : arr.append arr' = arr ++ arr' := rfl
 
@@ -153,7 +156,7 @@ abbrev push_data := @push_toList
 abbrev toList_eq := @toListImpl_eq
 
 @[deprecated pop_toList (since := "2024-09-09")]
-abbrev pop_data := @pop_toList
+abbrev pop_data := @toList_pop
 
 @[deprecated toList_append (since := "2024-09-09")]
 abbrev append_data := @toList_append

src/Init/Data/Array/Erase.lean

@@ -281,10 +281,10 @@ end erase
 
 theorem eraseIdx_eq_take_drop_succ (l : Array α) (i : Nat) (h) : l.eraseIdx i = l.take i ++ l.drop (i + 1) := by
   rcases l with ⟨l⟩
-  simp only [size_toArray] at h
+  simp only [List.size_toArray] at h
   simp only [List.eraseIdx_toArray, List.eraseIdx_eq_take_drop_succ, take_eq_extract,
     List.extract_toArray, List.extract_eq_drop_take, Nat.sub_zero, List.drop_zero, drop_eq_extract,
-    size_toArray, List.append_toArray, mk.injEq, List.append_cancel_left_eq]
+    List.size_toArray, List.append_toArray, mk.injEq, List.append_cancel_left_eq]
   rw [List.take_of_length_le]
   simp
 
@@ -316,7 +316,7 @@ theorem getElem_eraseIdx (l : Array α) (i : Nat) (h : i < l.size) (j : Nat) (h'
 
 @[simp] theorem eraseIdx_eq_empty_iff {l : Array α} {i : Nat} {h} : eraseIdx l i = #[] ↔ l.size = 1 ∧ i = 0 := by
   rcases l with ⟨l⟩
-  simp only [List.eraseIdx_toArray, mk.injEq, List.eraseIdx_eq_nil_iff, size_toArray,
+  simp only [List.eraseIdx_toArray, mk.injEq, List.eraseIdx_eq_nil_iff, List.size_toArray,
     or_iff_right_iff_imp]
   rintro rfl
   simp_all

src/Init/Data/Array/Extract.lean

@@ -351,7 +351,7 @@ theorem takeWhile_append {xs ys : Array α} :
       if (xs.takeWhile p).size = xs.size then xs ++ ys.takeWhile p else xs.takeWhile p := by
   rcases xs with ⟨xs⟩
   rcases ys with ⟨ys⟩
-  simp only [List.append_toArray, List.takeWhile_toArray, List.takeWhile_append, size_toArray]
+  simp only [List.append_toArray, List.takeWhile_toArray, List.takeWhile_append, List.size_toArray]
   split <;> rfl
 
 @[simp] theorem takeWhile_append_of_pos {p : α → Bool} {l₁ l₂ : Array α} (h : ∀ a ∈ l₁, p a) :
@@ -367,7 +367,7 @@ theorem popWhile_append {xs ys : Array α} :
   rcases xs with ⟨xs⟩
   rcases ys with ⟨ys⟩
   simp only [List.append_toArray, List.popWhile_toArray, List.reverse_append, List.dropWhile_append,
-    List.isEmpty_eq_true, List.isEmpty_toArray, List.isEmpty_reverse]
+    List.isEmpty_iff, List.isEmpty_toArray, List.isEmpty_reverse]
   -- Why do these not fire with `simp`?
   rw [List.popWhile_toArray, List.isEmpty_toArray, List.isEmpty_reverse]
   split

src/Init/Data/Array/Find.lean

@@ -86,7 +86,7 @@ theorem getElem_zero_flatten.proof {L : Array (Array α)} (h : 0 < L.flatten.siz
   cases L using array₂_induction
   simp only [List.findSome?_toArray, List.findSome?_map, Function.comp_def, List.getElem?_toArray,
     List.findSome?_isSome_iff, isSome_getElem?]
-  simp only [flatten_toArray_map_toArray, size_toArray, List.length_flatten,
+  simp only [flatten_toArray_map_toArray, List.size_toArray, List.length_flatten,
     Nat.sum_pos_iff_exists_pos, List.mem_map] at h
   obtain ⟨_, ⟨xs, m, rfl⟩, h⟩ := h
   exact ⟨xs, m, by simpa using h⟩

src/Init/Data/Array/GetLit.lean

@@ -31,7 +31,7 @@ def toArrayLit (a : Array α) (n : Nat) (hsz : a.size = n) : Array α :=
 
 theorem toArrayLit_eq (as : Array α) (n : Nat) (hsz : as.size = n) : as = toArrayLit as n hsz := by
   apply ext'
-  simp [toArrayLit, toList_toArray]
+  simp [toArrayLit, List.toList_toArray]
   have hle : n ≤ as.size := hsz ▸ Nat.le_refl _
   have hge : as.size ≤ n := hsz ▸ Nat.le_refl _
   have := go n hle

src/Init/Data/Array/Lemmas.lean

@@ -419,23 +419,26 @@ theorem forall_getElem {l : Array α} {p : α → Prop} :
 @[simp] theorem isEmpty_toList {l : Array α} : l.toList.isEmpty = l.isEmpty := by
   rcases l with ⟨_ | _⟩ <;> simp
 
-theorem isEmpty_iff {l : Array α} : l.isEmpty ↔ l = #[] := by
-  cases l <;> simp
-
 theorem isEmpty_eq_false_iff_exists_mem {xs : Array α} :
     xs.isEmpty = false ↔ ∃ x, x ∈ xs := by
   cases xs
   simpa using List.isEmpty_eq_false_iff_exists_mem
 
+@[simp] theorem isEmpty_iff {l : Array α} : l.isEmpty ↔ l = #[] := by
+  cases l <;> simp
+
+@[deprecated isEmpty_iff (since := "2025-02-17")]
+abbrev isEmpty_eq_true := @isEmpty_iff
+
+@[simp] theorem isEmpty_eq_false_iff {l : Array α} : l.isEmpty = false ↔ l ≠ #[] := by
+  cases l <;> simp
+
+@[deprecated isEmpty_eq_false_iff (since := "2025-02-17")]
+abbrev isEmpty_eq_false := @isEmpty_eq_false_iff
+
 theorem isEmpty_iff_size_eq_zero {l : Array α} : l.isEmpty ↔ l.size = 0 := by
   rw [isEmpty_iff, size_eq_zero]
 
-@[simp] theorem isEmpty_eq_true {l : Array α} : l.isEmpty ↔ l = #[] := by
-  cases l <;> simp
-
-@[simp] theorem isEmpty_eq_false {l : Array α} : l.isEmpty = false ↔ l ≠ #[] := by
-  cases l <;> simp
-
 /-! ### Decidability of bounded quantifiers -/
 
 instance {xs : Array α} {p : α → Prop} [DecidablePred p] :
@@ -480,7 +483,7 @@ theorem anyM_loop_cons [Monad m] (p : α → m Bool) (a : α) (as : List α) (st
   match as with
   | ⟨[]⟩  => rfl
   | ⟨a :: as⟩ => by
-    simp only [List.anyM, anyM, size_toArray, List.length_cons, Nat.le_refl, ↓reduceDIte]
+    simp only [List.anyM, anyM, List.size_toArray, List.length_cons, Nat.le_refl, ↓reduceDIte]
     rw [anyM.loop, dif_pos (by omega)]
     congr 1
     funext b
@@ -1340,7 +1343,7 @@ theorem map_filter_eq_foldl (f : α → β) (p : α → Bool) (l : Array α) :
     map f (filter p l) = foldl (fun y x => bif p x then y.push (f x) else y) #[] l := by
   rcases l with ⟨l⟩
   apply ext'
-  simp only [size_toArray, List.filter_toArray', List.map_toArray, List.foldl_toArray']
+  simp only [List.size_toArray, List.filter_toArray', List.map_toArray, List.foldl_toArray']
   rw [← List.reverse_reverse l]
   generalize l.reverse = l
   simp only [List.filter_reverse, List.map_reverse, List.foldl_reverse]
@@ -1362,7 +1365,7 @@ theorem filter_eq_append_iff {p : α → Bool} :
   rcases l with ⟨l⟩
   rcases L₁ with ⟨L₁⟩
   rcases L₂ with ⟨L₂⟩
-  simp only [size_toArray, List.filter_toArray', List.append_toArray, mk.injEq,
+  simp only [List.size_toArray, List.filter_toArray', List.append_toArray, mk.injEq,
     List.filter_eq_append_iff]
   constructor
   · rintro ⟨l₁, l₂, rfl, rfl, rfl⟩
@@ -1375,7 +1378,7 @@ theorem filter_eq_push_iff {p : α → Bool} {l l' : Array α} {a : α} :
       ∃ l₁ l₂, l = l₁.push a ++ l₂ ∧ filter p l₁ = l' ∧ p a ∧ (∀ x, x ∈ l₂ → ¬p x) := by
   rcases l with ⟨l⟩
   rcases l' with ⟨l'⟩
-  simp only [size_toArray, List.filter_toArray', List.push_toArray, mk.injEq, Bool.not_eq_true]
+  simp only [List.size_toArray, List.filter_toArray', List.push_toArray, mk.injEq, Bool.not_eq_true]
   rw [← List.reverse_inj]
   simp only [← List.filter_reverse]
   simp only [List.reverse_append, List.reverse_cons, List.reverse_nil, List.nil_append,
@@ -1544,7 +1547,7 @@ theorem filterMap_eq_push_iff {f : α → Option β} {l : Array α} {l' : Array
       l = l₁.push a ++ l₂ ∧ filterMap f l₁ = l' ∧ f a = some b ∧ (∀ x, x ∈ l₂ → f x = none) := by
   rcases l with ⟨l⟩
   rcases l' with ⟨l'⟩
-  simp only [size_toArray, List.filterMap_toArray', List.push_toArray, mk.injEq]
+  simp only [List.size_toArray, List.filterMap_toArray', List.push_toArray, mk.injEq]
   rw [← List.reverse_inj]
   simp only [← List.filterMap_reverse]
   simp only [List.reverse_append, List.reverse_cons, List.reverse_nil, List.nil_append,
@@ -1842,7 +1845,7 @@ theorem filterMap_eq_append_iff {f : α → Option β} :
   rcases l with ⟨l⟩
   rcases L₁ with ⟨L₁⟩
   rcases L₂ with ⟨L₂⟩
-  simp only [size_toArray, List.filterMap_toArray', List.append_toArray, mk.injEq,
+  simp only [List.size_toArray, List.filterMap_toArray', List.append_toArray, mk.injEq,
     List.filterMap_eq_append_iff, toArray_eq_append_iff]
   constructor
   · rintro ⟨l₁, l₂, rfl, rfl, rfl⟩
@@ -1951,7 +1954,7 @@ theorem flatten_eq_flatMap {L : Array (Array α)} : flatten L = L.flatMap id :=
     filterMap f (flatten L) 0 stop = flatten (map (filterMap f) L) := by
   subst w
   induction L using array₂_induction
-  simp only [flatten_toArray_map, size_toArray, List.length_flatten, List.filterMap_toArray',
+  simp only [flatten_toArray_map, List.size_toArray, List.length_flatten, List.filterMap_toArray',
     List.filterMap_flatten, List.map_toArray, List.map_map, Function.comp_def]
   rw [← Function.comp_def, ← List.map_map, flatten_toArray_map]
 
@@ -1959,7 +1962,7 @@ theorem flatten_eq_flatMap {L : Array (Array α)} : flatten L = L.flatMap id :=
     filter p (flatten L) 0 stop = flatten (map (filter p) L) := by
   subst w
   induction L using array₂_induction
-  simp only [flatten_toArray_map, size_toArray, List.length_flatten, List.filter_toArray',
+  simp only [flatten_toArray_map, List.size_toArray, List.length_flatten, List.filter_toArray',
     List.filter_flatten, List.map_toArray, List.map_map, Function.comp_def]
   rw [← Function.comp_def, ← List.map_map, flatten_toArray_map]
 
@@ -2151,7 +2154,7 @@ theorem filter_flatMap (l : Array α) (g : α → Array β) (f : β → Bool) :
 theorem flatMap_eq_foldl (f : α → Array β) (l : Array α) :
     l.flatMap f = l.foldl (fun acc a => acc ++ f a) #[] := by
   rcases l with ⟨l⟩
-  simp only [List.flatMap_toArray, List.flatMap_eq_foldl, size_toArray, List.foldl_toArray']
+  simp only [List.flatMap_toArray, List.flatMap_eq_foldl, List.size_toArray, List.foldl_toArray']
   suffices ∀ l', (List.foldl (fun acc a => acc ++ (f a).toList) l' l).toArray =
       List.foldl (fun acc a => acc ++ f a) l'.toArray l by
     simpa using this []
@@ -2731,9 +2734,9 @@ theorem foldrM_start_stop {m} [Monad m] (l : Array α) (f : α → β → m β)
   subst hstart hstop w
   rcases l with ⟨l⟩
   rw [foldlM_start_stop, List.extract_toArray]
-  simp only [size_toArray, List.length_take, List.length_drop, List.foldlM_toArray']
+  simp only [List.size_toArray, List.length_take, List.length_drop, List.foldlM_toArray']
   rw [foldlM_start_stop, List.extract_toArray]
-  simp only [size_toArray, List.length_take, List.length_drop, List.foldlM_toArray']
+  simp only [List.size_toArray, List.length_take, List.length_drop, List.foldlM_toArray']
   congr
   funext b a
   simp_all
@@ -2745,9 +2748,9 @@ theorem foldrM_start_stop {m} [Monad m] (l : Array α) (f : α → β → m β)
   subst hstart hstop w
   rcases l with ⟨l⟩
   rw [foldrM_start_stop, List.extract_toArray]
-  simp only [size_toArray, List.length_take, List.length_drop, List.foldrM_toArray']
+  simp only [List.size_toArray, List.length_take, List.length_drop, List.foldrM_toArray']
   rw [foldrM_start_stop, List.extract_toArray]
-  simp only [size_toArray, List.length_take, List.length_drop, List.foldrM_toArray']
+  simp only [List.size_toArray, List.length_take, List.length_drop, List.foldrM_toArray']
   congr
   funext b a
   simp_all
@@ -3185,11 +3188,6 @@ theorem sum_eq_sum_toList [Add α] [Zero α] (as : Array α) : as.toList.sum = a
   cases as
   simp [Array.sum, List.sum]
 
--- This is a duplicate of `List.toArray_toList`.
--- It's confusing to guess which namespace this theorem should live in,
--- so we provide both.
-@[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl
-
 @[deprecated size_toArray (since := "2024-12-11")]
 theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size]
 
@@ -3424,8 +3422,6 @@ theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
   · simp
   · rfl
 
-@[simp] theorem toList_pop (a : Array α) : a.pop.toList = a.toList.dropLast := by simp [pop]
-
 @[simp] theorem pop_empty : (#[] : Array α).pop = #[] := rfl
 
 @[simp] theorem pop_push (a : Array α) : (a.push x).pop = a := by simp [pop]

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

@@ -33,7 +33,7 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs
      (#[a] ++ xs).lex (#[b] ++ ys) lt =
        (lt a b || a == b && xs.lex ys lt) := by
   simp only [lex, Id.run]
-  simp only [Std.Range.forIn'_eq_forIn'_range', size_append, size_toArray, List.length_singleton,
+  simp only [Std.Range.forIn'_eq_forIn'_range', size_append, List.size_toArray, List.length_singleton,
     Nat.add_comm 1]
   simp [Nat.add_min_add_right, List.range'_succ, getElem_append_left, List.range'_succ_left,
     getElem_append_right]

src/Init/Data/Array/MapIdx.lean

@@ -388,7 +388,7 @@ theorem mapIdx_eq_append_iff {l : Array α} {f : Nat → α → β} {l₁ l₂ :
   · rintro ⟨l₁, l₂, rfl, rfl, rfl⟩
     exact ⟨l₁.toArray, l₂.toArray, by simp⟩
   · rintro ⟨⟨l₁⟩, ⟨l₂⟩, rfl, h₁, h₂⟩
-    simp only [List.mapIdx_toArray, mk.injEq, size_toArray] at h₁ h₂
+    simp only [List.mapIdx_toArray, mk.injEq, List.size_toArray] at h₁ h₂
     obtain rfl := h₁
     obtain rfl := h₂
     exact ⟨l₁, l₂, by simp⟩

src/Init/Data/Array/Monadic.lean

@@ -29,7 +29,7 @@ open Nat
 theorem mapM_eq_foldlM_push [Monad m] [LawfulMonad m] (f : α → m β) (l : Array α) :
     mapM f l = l.foldlM (fun acc a => return (acc.push (← f a))) #[] := by
   rcases l with ⟨l⟩
-  simp only [List.mapM_toArray, bind_pure_comp, size_toArray, List.foldlM_toArray']
+  simp only [List.mapM_toArray, bind_pure_comp, List.size_toArray, List.foldlM_toArray']
   rw [List.mapM_eq_reverse_foldlM_cons]
   simp only [bind_pure_comp, Functor.map_map]
   suffices ∀ (k), (fun a => a.reverse.toArray) <$> List.foldlM (fun acc a => (fun a => a :: acc) <$> f a) k l =
@@ -190,7 +190,7 @@ theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
         | .yield b => f a b
         | .done b => pure (.done b)) (ForInStep.yield init) := by
   cases l
-  simp only [List.forIn_toArray, List.forIn_eq_foldlM, size_toArray, List.foldlM_toArray']
+  simp only [List.forIn_toArray, List.forIn_eq_foldlM, List.size_toArray, List.foldlM_toArray']
   congr
 
 /-- We can express a for loop over an array which always yields as a fold. -/

src/Init/Data/Array/Range.lean

@@ -124,7 +124,7 @@ theorem range_succ_eq_map (n : Nat) : range (n + 1) = #[0] ++ map succ (range n)
   ext i h₁ h₂
   · simp
     omega
-  · simp only [getElem_range, getElem_append, size_toArray, List.length_cons, List.length_nil,
+  · simp only [getElem_range, getElem_append, List.size_toArray, List.length_cons, List.length_nil,
       Nat.zero_add, lt_one_iff, List.getElem_toArray, List.getElem_singleton, getElem_map,
       succ_eq_add_one, dite_eq_ite]
     split <;> omega
@@ -290,7 +290,7 @@ theorem zipIdx_eq_append_iff {l : Array α} {k : Nat} :
   · rintro ⟨l₁', l₂', rfl, rfl, rfl⟩
     exact ⟨⟨l₁'⟩, ⟨l₂'⟩, by simp⟩
   · rintro ⟨⟨l₁'⟩, ⟨l₂'⟩, rfl, h⟩
-    simp only [zipIdx_toArray, mk.injEq, size_toArray] at h
+    simp only [zipIdx_toArray, mk.injEq, List.size_toArray] at h
     obtain ⟨rfl, rfl⟩ := h
     exact ⟨l₁', l₂', by simp⟩
 

src/Init/Data/Array/Zip.lean

@@ -275,7 +275,7 @@ theorem zip_eq_zip_take_min (l₁ : Array α) (l₂ : Array β) :
     zip l₁ l₂ = zip (l₁.take (min l₁.size l₂.size)) (l₂.take (min l₁.size l₂.size)) := by
   cases l₁
   cases l₂
-  simp only [List.zip_toArray, size_toArray, List.take_toArray, mk.injEq]
+  simp only [List.zip_toArray, List.size_toArray, List.take_toArray, mk.injEq]
   rw [List.zip_eq_zip_take_min]
 
 
@@ -338,21 +338,21 @@ theorem unzip_zip_left {l₁ : Array α} {l₂ : Array β} (h : l₁.size ≤ l
     (unzip (zip l₁ l₂)).1 = l₁ := by
   cases l₁
   cases l₂
-  simp_all only [size_toArray, List.zip_toArray, List.unzip_toArray, Prod.map_fst,
+  simp_all only [List.size_toArray, List.zip_toArray, List.unzip_toArray, Prod.map_fst,
     List.unzip_zip_left]
 
 theorem unzip_zip_right {l₁ : Array α} {l₂ : Array β} (h : l₂.size ≤ l₁.size) :
     (unzip (zip l₁ l₂)).2 = l₂ := by
   cases l₁
   cases l₂
-  simp_all only [size_toArray, List.zip_toArray, List.unzip_toArray, Prod.map_snd,
+  simp_all only [List.size_toArray, List.zip_toArray, List.unzip_toArray, Prod.map_snd,
     List.unzip_zip_right]
 
 theorem unzip_zip {l₁ : Array α} {l₂ : Array β} (h : l₁.size = l₂.size) :
     unzip (zip l₁ l₂) = (l₁, l₂) := by
   cases l₁
   cases l₂
-  simp_all only [size_toArray, List.zip_toArray, List.unzip_toArray, List.unzip_zip, Prod.map_apply]
+  simp_all only [List.size_toArray, List.zip_toArray, List.unzip_toArray, List.unzip_zip, Prod.map_apply]
 
 theorem zip_of_prod {l : Array α} {l' : Array β} {lp : Array (α × β)} (hl : lp.map Prod.fst = l)
     (hr : lp.map Prod.snd = l') : lp = l.zip l' := by

src/Init/Data/BitVec/Basic.lean

@@ -395,7 +395,7 @@ and is a computational noop.
 def setWidth' {n w : Nat} (le : n ≤ w) (x : BitVec n) : BitVec w :=
   x.toNat#'(by
     apply Nat.lt_of_lt_of_le x.isLt
-    exact Nat.pow_le_pow_of_le_right (by trivial) le)
+    exact Nat.pow_le_pow_right (by trivial) le)
 
 @[deprecated setWidth' (since := "2024-09-18"), inherit_doc setWidth'] abbrev zeroExtend' := @setWidth'
 

src/Init/Data/BitVec/Bitblast.lean

@@ -144,7 +144,7 @@ private theorem testBit_limit {x i : Nat} (x_lt_succ : x < 2^(i+1)) :
         exfalso
         apply Nat.lt_irrefl
         calc x < 2^(i+1) := x_lt_succ
-             _ ≤ 2 ^ j := Nat.pow_le_pow_of_le_right Nat.zero_lt_two x_lt
+             _ ≤ 2 ^ j := Nat.pow_le_pow_right Nat.zero_lt_two x_lt
              _ ≤ x := testBit_implies_ge jp
 
 private theorem mod_two_pow_succ (x i : Nat) :

src/Init/Data/BitVec/Lemmas.lean

@@ -29,7 +29,7 @@ namespace BitVec
   let ⟨x, x_lt⟩ := x
   simp only [getLsbD_ofFin]
   apply Nat.testBit_lt_two_pow
-  have p : 2^w ≤ 2^i := Nat.pow_le_pow_of_le_right (by omega) ge
+  have p : 2^w ≤ 2^i := Nat.pow_le_pow_right (by omega) ge
   omega
 
 @[simp] theorem getMsbD_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getMsbD x i = false := by
@@ -52,12 +52,16 @@ theorem lt_of_getMsbD {x : BitVec w} {i : Nat} : getMsbD x i = true → i < w :=
 @[simp] theorem getElem?_eq_getElem {l : BitVec w} {n} (h : n < w) : l[n]? = some l[n] := by
   simp only [getElem?_def, h, ↓reduceDIte]
 
-theorem getElem?_eq_some {l : BitVec w} : l[n]? = some a ↔ ∃ h : n < w, l[n] = a := by
+theorem getElem?_eq_some_iff {l : BitVec w} : l[n]? = some a ↔ ∃ h : n < w, l[n] = a := by
   simp only [getElem?_def]
   split
   · simp_all
   · simp; omega
 
+set_option linter.missingDocs false in
+@[deprecated getElem?_eq_some_iff (since := "2025-02-17")]
+abbrev getElem?_eq_some := @getElem?_eq_some_iff
+
 @[simp] theorem getElem?_eq_none_iff {l : BitVec w} : l[n]? = none ↔ w ≤ n := by
   simp only [getElem?_def]
   split
@@ -79,7 +83,7 @@ theorem getElem?_eq (l : BitVec w) (i : Nat) :
   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]
+  simp only [getElem?_eq_some_iff]
   exact ⟨fun w => ⟨h, w⟩, fun h => h.2⟩
 
 theorem getElem_eq_getElem? (l : BitVec w) (i : Nat) (h : i < w) :
@@ -374,7 +378,7 @@ theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) :
     Int.sub_eq_add_neg]
 
 private theorem lt_two_pow_of_le {x m n : Nat} (lt : x < 2 ^ m) (le : m ≤ n) : x < 2 ^ n :=
-  Nat.lt_of_lt_of_le lt (Nat.pow_le_pow_of_le_right (by trivial : 0 < 2) le)
+  Nat.lt_of_lt_of_le lt (Nat.pow_le_pow_right (by trivial : 0 < 2) le)
 
 theorem getElem_zero_ofNat_zero (i : Nat) (h : i < w) : (BitVec.ofNat w 0)[i] = false := by
   simp
@@ -1344,7 +1348,7 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
         simp only [Bool.false_bne, Bool.false_and]
         rw [Nat.testBit_lt_two_pow]
         calc BitVec.toNat x < 2 ^ v := isLt _
-          _ ≤ 2 ^ i := Nat.pow_le_pow_of_le_right Nat.zero_lt_two w
+          _ ≤ 2 ^ i := Nat.pow_le_pow_right Nat.zero_lt_two w
       · simp
 
 @[simp] theorem toInt_not {x : BitVec w} :
@@ -2082,9 +2086,9 @@ If the msb is true, then we add a value of `(2^v - 2^w)`, which arises from the
 theorem toNat_signExtend (x : BitVec w) {v : Nat} :
     (x.signExtend v).toNat = (x.setWidth v).toNat + if x.msb then 2^v - 2^w else 0 := by
   by_cases h : v ≤ w
-  · have : 2^v ≤ 2^w := Nat.pow_le_pow_of_le_right Nat.two_pos h
+  · have : 2^v ≤ 2^w := Nat.pow_le_pow_right Nat.two_pos h
     simp [signExtend_eq_setWidth_of_lt x h, toNat_setWidth, Nat.sub_eq_zero_of_le this]
-  · have : 2^w ≤ 2^v := Nat.pow_le_pow_of_le_right Nat.two_pos (by omega)
+  · have : 2^w ≤ 2^v := Nat.pow_le_pow_right Nat.two_pos (by omega)
     rw [toNat_signExtend_of_le x (by omega), toNat_setWidth, Nat.mod_eq_of_lt (by omega)]
 
 /-
@@ -2097,7 +2101,7 @@ theorem toInt_signExtend_of_lt {x : BitVec w} (hv : w < v):
   have : (x.signExtend v).msb = x.msb := by
     rw [msb_eq_getLsbD_last, getLsbD_eq_getElem (Nat.sub_one_lt_of_lt hv)]
     simp [getElem_signExtend, Nat.le_sub_one_of_lt hv]
-  have H : 2^w ≤ 2^v := Nat.pow_le_pow_of_le_right (by omega) (by omega)
+  have H : 2^w ≤ 2^v := Nat.pow_le_pow_right (by omega) (by omega)
   simp only [this, toNat_setWidth, Int.natCast_add, Int.ofNat_emod, Int.natCast_mul]
   by_cases h : x.msb
   <;> norm_cast

src/Init/Data/Int/Pow.lean

@@ -17,24 +17,14 @@ protected theorem pow_succ (b : Int) (e : Nat) : b ^ (e+1) = (b ^ e) * b := rfl
 protected theorem pow_succ' (b : Int) (e : Nat) : b ^ (e+1) = b * (b ^ e) := by
   rw [Int.mul_comm, Int.pow_succ]
 
-theorem pow_le_pow_of_le_left {n m : Nat} (h : n ≤ m) : ∀ (i : Nat), n^i ≤ m^i
-  | 0      => Nat.le_refl _
-  | i + 1 => Nat.mul_le_mul (pow_le_pow_of_le_left h i) h
+@[deprecated Nat.pow_le_pow_left (since := "2025-02-17")]
+abbrev pow_le_pow_of_le_left := @Nat.pow_le_pow_left
 
-theorem pow_le_pow_of_le_right {n : Nat} (hx : n > 0) {i : Nat} : ∀ {j}, i ≤ j → n^i ≤ n^j
-  | 0,      h =>
-    have : i = 0 := Nat.eq_zero_of_le_zero h
-    this.symm ▸ Nat.le_refl _
-  | j + 1, h =>
-    match Nat.le_or_eq_of_le_succ h with
-    | Or.inl h => show n^i ≤ n^j * n from
-      have : n^i * 1 ≤ n^j * n := Nat.mul_le_mul (pow_le_pow_of_le_right hx h) hx
-      Nat.mul_one (n^i) ▸ this
-    | Or.inr h =>
-      h.symm ▸ Nat.le_refl _
+@[deprecated Nat.pow_le_pow_right (since := "2025-02-17")]
+abbrev pow_le_pow_of_le_right := @Nat.pow_le_pow_right
 
-theorem pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) : 0 < n^m :=
-  pow_le_pow_of_le_right h (Nat.zero_le _)
+@[deprecated Nat.pow_pos (since := "2025-02-17")]
+abbrev pos_pow_of_pos := @Nat.pow_pos
 
 @[norm_cast]
 theorem natCast_pow (b n : Nat) : ((b^n : Nat) : Int) = (b : Int) ^ n := by

src/Init/Data/List/Attach.lean

@@ -120,27 +120,26 @@ theorem pmap_eq_attachWith {p q : α → Prop} (f : ∀ a, p a → q a) (l H) :
   | cons a l ih =>
     simp [pmap, attachWith, ih]
 
-theorem attach_map_coe (l : List α) (f : α → β) :
+theorem attach_map_val (l : List α) (f : α → β) :
     (l.attach.map fun (i : {i // i ∈ l}) => f i) = l.map f := by
   rw [attach, attachWith, map_pmap]; exact pmap_eq_map _ _ _ _
 
-theorem attach_map_val (l : List α) (f : α → β) : (l.attach.map fun i => f i.val) = l.map f :=
-  attach_map_coe _ _
+@[deprecated attach_map_val (since := "2025-02-17")]
+abbrev attach_map_coe := @attach_map_val
 
 theorem attach_map_subtype_val (l : List α) : l.attach.map Subtype.val = l :=
-  (attach_map_coe _ _).trans (List.map_id _)
+  (attach_map_val _ _).trans (List.map_id _)
 
-theorem attachWith_map_coe {p : α → Prop} (f : α → β) (l : List α) (H : ∀ a ∈ l, p a) :
+theorem attachWith_map_val {p : α → Prop} (f : α → β) (l : List α) (H : ∀ a ∈ l, p a) :
     ((l.attachWith p H).map fun (i : { i // p i}) => f i) = l.map f := by
   rw [attachWith, map_pmap]; exact pmap_eq_map _ _ _ _
 
-theorem attachWith_map_val {p : α → Prop} (f : α → β) (l : List α) (H : ∀ a ∈ l, p a) :
-    ((l.attachWith p H).map fun i => f i.val) = l.map f :=
-  attachWith_map_coe _ _ _
+@[deprecated attachWith_map_val (since := "2025-02-17")]
+abbrev attachWith_map_coe := @attachWith_map_val
 
 theorem attachWith_map_subtype_val {p : α → Prop} (l : List α) (H : ∀ a ∈ l, p a) :
     (l.attachWith p H).map Subtype.val = l :=
-  (attachWith_map_coe _ _ _).trans (List.map_id _)
+  (attachWith_map_val _ _ _).trans (List.map_id _)
 
 @[simp]
 theorem mem_attach (l : List α) : ∀ x, x ∈ l.attach

src/Init/Data/List/Find.lean

@@ -117,7 +117,7 @@ theorem find?_eq_findSome?_guard (l : List α) : find? p l = findSome? (Option.g
 
 @[simp] theorem getLast_filterMap (f : α → Option β) (l : List α) (h) :
     (l.filterMap f).getLast h = (l.reverse.findSome? f).get (by simp_all [Option.isSome_iff_ne_none]) := by
-  simp [getLast_eq_iff_getLast_eq_some]
+  simp [getLast_eq_iff_getLast?_eq_some]
 
 @[simp] theorem map_findSome? (f : α → Option β) (g : β → γ) (l : List α) :
     (l.findSome? f).map g = l.findSome? (Option.map g ∘ f) := by
@@ -144,7 +144,7 @@ theorem head_flatten {L : List (List α)} (h : ∃ l, l ∈ L ∧ l ≠ []) :
 theorem getLast_flatten {L : List (List α)} (h : ∃ l, l ∈ L ∧ l ≠ []) :
     (flatten L).getLast (by simpa using h) =
       (L.reverse.findSome? fun l => l.getLast?).get (by simpa using h) := by
-  simp [getLast_eq_iff_getLast_eq_some, getLast?_flatten]
+  simp [getLast_eq_iff_getLast?_eq_some, getLast?_flatten]
 
 theorem findSome?_replicate : findSome? f (replicate n a) = if n = 0 then none else f a := by
   cases n with
@@ -309,7 +309,7 @@ theorem get_find?_mem (xs : List α) (p : α → Bool) (h) : (xs.find? p).get h
 
 @[simp] theorem getLast_filter (p : α → Bool) (l : List α) (h) :
     (l.filter p).getLast h = (l.reverse.find? p).get (by simp_all [Option.isSome_iff_ne_none]) := by
-  simp [getLast_eq_iff_getLast_eq_some]
+  simp [getLast_eq_iff_getLast?_eq_some]
 
 @[simp] theorem find?_filterMap (xs : List α) (f : α → Option β) (p : β → Bool) :
     (xs.filterMap f).find? p = (xs.find? (fun a => (f a).any p)).bind f := by

src/Init/Data/List/Impl.lean

@@ -91,7 +91,7 @@ The following operations are given `@[csimp]` replacements below:
 @[specialize] def foldrTR (f : α → β → β) (init : β) (l : List α) : β := l.toArray.foldr f init
 
 @[csimp] theorem foldr_eq_foldrTR : @foldr = @foldrTR := by
-  funext α β f init l; simp [foldrTR, ← Array.foldr_toList, -Array.size_toArray]
+  funext α β f init l; simp only [foldrTR, ← Array.foldr_toList]
 
 /-! ### flatMap  -/
 
@@ -324,7 +324,7 @@ def zipIdxTR (l : List α) (n : Nat := 0) : List (α × Nat) :=
   (arr.foldr (fun a (n, acc) => (n-1, (a, n-1) :: acc)) (n + arr.size, [])).2
 
 @[csimp] theorem zipIdx_eq_zipIdxTR : @zipIdx = @zipIdxTR := by
-  funext α l n; simp [zipIdxTR, -Array.size_toArray]
+  funext α l n; simp only [zipIdxTR, size_toArray]
   let f := fun (a : α) (n, acc) => (n-1, (a, n-1) :: acc)
   let rec go : ∀ l n, l.foldr f (n + l.length, []) = (n, zipIdx l n)
     | [], n => rfl
@@ -345,7 +345,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 [enumFromTR, -Array.size_toArray]
+  funext α n l; simp only [enumFromTR, size_toArray]
   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/Lemmas.lean

@@ -527,9 +527,18 @@ theorem elem_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
 
 /-! ### `isEmpty` -/
 
-theorem isEmpty_iff {l : List α} : l.isEmpty ↔ l = [] := by
+@[simp] theorem isEmpty_iff {l : List α} : l.isEmpty ↔ l = [] := by
   cases l <;> simp
 
+@[deprecated isEmpty_iff (since := "2025-02-17")]
+abbrev isEmpty_eq_true := @isEmpty_iff
+
+@[simp] theorem isEmpty_eq_false_iff {l : List α} : l.isEmpty = false ↔ l ≠ [] := by
+  cases l <;> simp
+
+@[deprecated isEmpty_eq_false_iff (since := "2025-02-17")]
+abbrev isEmpty_eq_false := @isEmpty_eq_false_iff
+
 theorem isEmpty_eq_false_iff_exists_mem {xs : List α} :
     xs.isEmpty = false ↔ ∃ x, x ∈ xs := by
   cases xs <;> simp
@@ -537,12 +546,6 @@ theorem isEmpty_eq_false_iff_exists_mem {xs : List α} :
 theorem isEmpty_iff_length_eq_zero {l : List α} : l.isEmpty ↔ l.length = 0 := by
   rw [isEmpty_iff, length_eq_zero]
 
-@[simp] theorem isEmpty_eq_true {l : List α} : l.isEmpty ↔ l = [] := by
-  cases l <;> simp
-
-@[simp] theorem isEmpty_eq_false {l : List α} : l.isEmpty = false ↔ l ≠ [] := by
-  cases l <;> simp
-
 /-! ### any / all -/
 
 theorem any_eq {l : List α} : l.any p = decide (∃ x, x ∈ l ∧ p x) := by induction l <;> simp [*]
@@ -2798,9 +2801,8 @@ theorem getLast_eq_head_reverse {l : List α} (h : l ≠ []) :
     l.getLast h = l.reverse.head (by simp_all) := by
   rw [← head_reverse]
 
-theorem getLast_eq_iff_getLast_eq_some {xs : List α} (h) : xs.getLast h = a ↔ xs.getLast? = some a := by
-  rw [getLast_eq_head_reverse, head_eq_iff_head?_eq_some]
-  simp
+@[deprecated getLast_eq_iff_getLast?_eq_some (since := "2025-02-17")]
+abbrev getLast_eq_iff_getLast_eq_some := @getLast_eq_iff_getLast?_eq_some
 
 @[simp] theorem getLast?_eq_none_iff {xs : List α} : xs.getLast? = none ↔ xs = [] := by
   rw [getLast?_eq_head?_reverse, head?_eq_none_iff, reverse_eq_nil_iff]

src/Init/Data/List/Nat/Range.lean

@@ -42,7 +42,7 @@ theorem getLast?_range' (n : Nat) : (range' s n).getLast? = if n = 0 then none e
 @[simp] theorem getLast_range' (n : Nat) (h) : (range' s n).getLast h = s + n - 1 := by
   cases n with
   | zero => simp at h
-  | succ n => simp [getLast?_range', getLast_eq_iff_getLast_eq_some]
+  | succ n => simp [getLast?_range', getLast_eq_iff_getLast?_eq_some]
 
 theorem pairwise_lt_range' s n (step := 1) (pos : 0 < step := by simp) :
     Pairwise (· < ·) (range' s n step) :=

src/Init/Data/List/Range.lean

@@ -209,7 +209,7 @@ theorem getLast?_range (n : Nat) : (range n).getLast? = if n = 0 then none else
 @[simp] theorem getLast_range (n : Nat) (h) : (range n).getLast h = n - 1 := by
   cases n with
   | zero => simp at h
-  | succ n => simp [getLast?_range, getLast_eq_iff_getLast_eq_some]
+  | succ n => simp [getLast?_range, getLast_eq_iff_getLast?_eq_some]
 
 /-! ### zipIdx -/
 

src/Init/Data/Nat/Basic.lean

@@ -726,34 +726,48 @@ protected theorem pow_add_one (n m : Nat) : n^(m + 1) = n^m * n :=
 
 protected theorem pow_zero (n : Nat) : n^0 = 1 := rfl
 
-theorem pow_le_pow_of_le_left {n m : Nat} (h : n ≤ m) : ∀ (i : Nat), n^i ≤ m^i
+theorem pow_le_pow_left {n m : Nat} (h : n ≤ m) : ∀ (i : Nat), n^i ≤ m^i
   | 0      => Nat.le_refl _
-  | succ i => Nat.mul_le_mul (pow_le_pow_of_le_left h i) h
+  | succ i => Nat.mul_le_mul (pow_le_pow_left h i) h
 
-theorem pow_le_pow_of_le_right {n : Nat} (hx : n > 0) {i : Nat} : ∀ {j}, i ≤ j → n^i ≤ n^j
+theorem pow_le_pow_right {n : Nat} (hx : n > 0) {i : Nat} : ∀ {j}, i ≤ j → n^i ≤ n^j
   | 0,      h =>
     have : i = 0 := eq_zero_of_le_zero h
     this.symm ▸ Nat.le_refl _
   | succ j, h =>
     match le_or_eq_of_le_succ h with
     | Or.inl h => show n^i ≤ n^j * n from
-      have : n^i * 1 ≤ n^j * n := Nat.mul_le_mul (pow_le_pow_of_le_right hx h) hx
+      have : n^i * 1 ≤ n^j * n := Nat.mul_le_mul (pow_le_pow_right hx h) hx
       Nat.mul_one (n^i) ▸ this
     | Or.inr h =>
       h.symm ▸ Nat.le_refl _
 
-theorem pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) : 0 < n^m :=
-  pow_le_pow_of_le_right h (Nat.zero_le _)
+set_option linter.missingDocs false in
+@[deprecated Nat.pow_le_pow_left (since := "2025-02-17")]
+abbrev pow_le_pow_of_le_left := @pow_le_pow_left
+
+set_option linter.missingDocs false in
+@[deprecated Nat.pow_le_pow_right (since := "2025-02-17")]
+abbrev pow_le_pow_of_le_right := @pow_le_pow_right
+
+protected theorem pow_pos (h : 0 < a) : 0 < a^n :=
+  match n with
+  | 0 => Nat.zero_lt_one
+  | _ + 1 => Nat.mul_pos (Nat.pow_pos h) h
+
+set_option linter.missingDocs false in
+@[deprecated Nat.pow_pos (since := "2025-02-17")]
+abbrev pos_pow_of_pos := @Nat.pow_pos
 
 @[simp] theorem zero_pow_of_pos (n : Nat) (h : 0 < n) : 0 ^ n = 0 := by
   cases n with
   | zero => cases h
   | succ n => simp [Nat.pow_succ]
 
-protected theorem two_pow_pos (w : Nat) : 0 < 2^w := Nat.pos_pow_of_pos _ (by decide)
+protected theorem two_pow_pos (w : Nat) : 0 < 2^w := Nat.pow_pos (by decide)
 
 instance {n m : Nat} [NeZero n] : NeZero (n^m) :=
-  ⟨Nat.ne_zero_iff_zero_lt.mpr (Nat.pos_pow_of_pos m (pos_of_neZero _))⟩
+  ⟨Nat.ne_zero_iff_zero_lt.mpr (Nat.pow_pos (pos_of_neZero _))⟩
 
 /-! # min/max -/
 

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -286,7 +286,7 @@ theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) :
       · simp [i_lt_j]
       · have x_lt : x < 2^i :=
             calc x < 2^j := x_lt_j
-                _ ≤ 2^i := Nat.pow_le_pow_of_le_right Nat.zero_lt_two i_ge_j
+                _ ≤ 2^i := Nat.pow_le_pow_right Nat.zero_lt_two i_ge_j
         simp [Nat.testBit_lt_two_pow x_lt]
     · generalize y_eq : x - 2^j = y
       have x_eq : x = y + 2^j := Nat.eq_add_of_sub_eq x_ge_j y_eq
@@ -490,7 +490,7 @@ theorem and_lt_two_pow (x : Nat) {y n : Nat} (right : y < 2^n) : (x &&& y) < 2^n
   have yf : testBit y i = false := by
           apply Nat.testBit_lt_two_pow
           apply Nat.lt_of_lt_of_le right
-          exact pow_le_pow_of_le_right Nat.zero_lt_two i_ge_n
+          exact pow_le_pow_right Nat.zero_lt_two i_ge_n
   simp [testBit_and, yf]
 
 @[simp] theorem and_pow_two_sub_one_eq_mod (x n : Nat) : x &&& 2^n - 1 = x % 2^n := by
@@ -695,7 +695,7 @@ theorem mul_add_lt_is_or {b : Nat} (b_lt : b < 2^i) (a : Nat) : 2^i * a + b = 2^
     have i_le : i ≤ j := Nat.le_of_not_lt j_lt
     have b_lt_j :=
             calc b < 2 ^ i := b_lt
-                 _ ≤ 2 ^ j := Nat.pow_le_pow_of_le_right Nat.zero_lt_two i_le
+                 _ ≤ 2 ^ j := Nat.pow_le_pow_right Nat.zero_lt_two i_le
     simp [i_le, j_lt, testBit_lt_two_pow, b_lt_j]
 
 /-! ### shiftLeft and shiftRight -/

src/Init/Data/Nat/Lemmas.lean

@@ -750,9 +750,6 @@ protected theorem mul_pow (a b n : Nat) : (a * b) ^ n = a ^ n * b ^ n := by
   | zero => rw [Nat.pow_zero, Nat.pow_zero, Nat.pow_zero, Nat.mul_one]
   | succ _ ih => rw [Nat.pow_succ, Nat.pow_succ, Nat.pow_succ, Nat.mul_mul_mul_comm, ih]
 
-protected abbrev pow_le_pow_left := @pow_le_pow_of_le_left
-protected abbrev pow_le_pow_right := @pow_le_pow_of_le_right
-
 protected theorem one_lt_two_pow (h : n ≠ 0) : 1 < 2 ^ n :=
   match n, h with
   | n+1, _ => by
@@ -778,11 +775,6 @@ protected theorem one_le_two_pow : 1 ≤ 2 ^ n :=
 @[simp] theorem one_mod_two_pow (h : 0 < n) : 1 % 2 ^ n = 1 :=
   one_mod_two_pow_eq_one.mpr h
 
-protected theorem pow_pos (h : 0 < a) : 0 < a^n :=
-  match n with
-  | 0 => Nat.zero_lt_one
-  | _ + 1 => Nat.mul_pos (Nat.pow_pos h) h
-
 protected theorem pow_lt_pow_succ (h : 1 < a) : a ^ n < a ^ (n + 1) := by
   rw [← Nat.mul_one (a^n), Nat.pow_succ]
   exact Nat.mul_lt_mul_of_le_of_lt (Nat.le_refl _) h (Nat.pow_pos (Nat.lt_trans Nat.zero_lt_one h))
@@ -898,7 +890,7 @@ theorem le_log2 (h : n ≠ 0) : k ≤ n.log2 ↔ 2 ^ k ≤ n := by
       exact Nat.le_div_iff_mul_le (by decide)
     · simp only [le_zero_eq, succ_ne_zero, false_iff]
       refine mt (Nat.le_trans ?_) ‹_›
-      exact Nat.pow_le_pow_of_le_right Nat.zero_lt_two (Nat.le_add_left 1 k)
+      exact Nat.pow_le_pow_right Nat.zero_lt_two (Nat.le_add_left 1 k)
 
 theorem log2_lt (h : n ≠ 0) : n.log2 < k ↔ n < 2 ^ k := by
   rw [← Nat.not_le, ← Nat.not_le, le_log2 h]

src/Init/Data/Nat/Power2.lean

@@ -36,7 +36,7 @@ theorem mul2_isPowerOfTwo_of_isPowerOfTwo (h : isPowerOfTwo n) : isPowerOfTwo (n
 theorem pos_of_isPowerOfTwo (h : isPowerOfTwo n) : n > 0 := by
   have ⟨k, h⟩ := h
   rw [h]
-  apply Nat.pos_pow_of_pos
+  apply Nat.pow_pos
   decide
 
 theorem isPowerOfTwo_nextPowerOfTwo (n : Nat) : n.nextPowerOfTwo.isPowerOfTwo := by

src/Init/Data/Option/Attach.lean

@@ -48,29 +48,27 @@ theorem attachWith_congr {o₁ o₂ : Option α} (w : o₁ = o₂) {P : α → P
   subst w
   simp
 
-theorem attach_map_coe (o : Option α) (f : α → β) :
+theorem attach_map_val (o : Option α) (f : α → β) :
     (o.attach.map fun (i : {i // i ∈ o}) => f i) = o.map f := by
   cases o <;> simp
 
-theorem attach_map_val (o : Option α) (f : α → β) :
-    (o.attach.map fun i => f i.val) = o.map f :=
-  attach_map_coe _ _
+@[deprecated attach_map_val (since := "2025-02-17")]
+abbrev attach_map_coe := @attach_map_val
 
 theorem attach_map_subtype_val (o : Option α) :
     o.attach.map Subtype.val = o :=
-  (attach_map_coe _ _).trans (congrFun Option.map_id _)
+  (attach_map_val _ _).trans (congrFun Option.map_id _)
 
-theorem attachWith_map_coe {p : α → Prop} (f : α → β) (o : Option α) (H : ∀ a ∈ o, p a) :
+theorem attachWith_map_val {p : α → Prop} (f : α → β) (o : Option α) (H : ∀ a ∈ o, p a) :
     ((o.attachWith p H).map fun (i : { i // p i}) => f i.val) = o.map f := by
   cases o <;> simp [H]
 
-theorem attachWith_map_val {p : α → Prop} (f : α → β) (o : Option α) (H : ∀ a ∈ o, p a) :
-    ((o.attachWith p H).map fun i => f i.val) = o.map f :=
-  attachWith_map_coe _ _ _
+@[deprecated attachWith_map_val (since := "2025-02-17")]
+abbrev attachWith_map_coe := @attachWith_map_val
 
 theorem attachWith_map_subtype_val {p : α → Prop} (o : Option α) (H : ∀ a ∈ o, p a) :
     (o.attachWith p H).map Subtype.val = o :=
-  (attachWith_map_coe _ _ _).trans (congrFun Option.map_id _)
+  (attachWith_map_val _ _ _).trans (congrFun Option.map_id _)
 
 theorem mem_attach : ∀ (o : Option α) (x : {x // x ∈ o}), x ∈ o.attach
   | none, ⟨x, h⟩ => by simp at h

src/Init/Data/Vector/Attach.lean

@@ -154,24 +154,23 @@ theorem pmap_eq_attachWith {p q : α → Prop} (f : ∀ a, p a → q a) (l : Vec
   cases l
   simp
 
-theorem attach_map_coe (l : Vector α n) (f : α → β) :
+theorem attach_map_val (l : Vector α n) (f : α → β) :
     (l.attach.map fun (i : {i // i ∈ l}) => f i) = l.map f := by
   cases l
   simp
 
-theorem attach_map_val (l : Vector α n) (f : α → β) : (l.attach.map fun i => f i.val) = l.map f :=
-  attach_map_coe _ _
+@[deprecated attach_map_val (since := "2025-02-17")]
+abbrev attach_map_coe := @attach_map_val
 
 theorem attach_map_subtype_val (l : Vector α n) : l.attach.map Subtype.val = l := by
   cases l; simp
 
-theorem attachWith_map_coe {p : α → Prop} (f : α → β) (l : Vector α n) (H : ∀ a ∈ l, p a) :
+theorem attachWith_map_val {p : α → Prop} (f : α → β) (l : Vector α n) (H : ∀ a ∈ l, p a) :
     ((l.attachWith p H).map fun (i : { i // p i}) => f i) = l.map f := by
   cases l; simp
 
-theorem attachWith_map_val {p : α → Prop} (f : α → β) (l : Vector α n) (H : ∀ a ∈ l, p a) :
-    ((l.attachWith p H).map fun i => f i.val) = l.map f :=
-  attachWith_map_coe _ _ _
+@[deprecated attachWith_map_val (since := "2025-02-17")]
+abbrev attachWith_map_coe := @attachWith_map_val
 
 theorem attachWith_map_subtype_val {p : α → Prop} (l : Vector α n) (H : ∀ a ∈ l, p a) :
     (l.attachWith p H).map Subtype.val = l := by

src/Init/GetElem.lean

@@ -181,13 +181,16 @@ theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem d
   simp only [getElem?_def] at h ⊢
   split <;> simp_all
 
-@[simp] theorem getElem?_eq_none [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+@[simp] theorem getElem?_eq_none_iff [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     (c : cont) (i : idx) [Decidable (dom c i)] : c[i]? = none ↔ ¬dom c i := by
   simp only [getElem?_def]
   split <;> simp_all
 
+@[deprecated getElem?_eq_none_iff (since := "2025-02-17")]
+abbrev getElem?_eq_none := @getElem?_eq_none_iff
+
 @[deprecated getElem?_eq_none (since := "2024-12-11")]
-abbrev isNone_getElem? := @getElem?_eq_none
+abbrev isNone_getElem? := @getElem?_eq_none_iff
 
 @[simp] theorem isSome_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     (c : cont) (i : idx) [Decidable (dom c i)] : c[i]?.isSome = dom c i := by

src/Init/Omega/Int.lean

@@ -27,7 +27,7 @@ theorem ofNat_pow (a b : Nat) : ((a ^ b : Nat) : Int) = (a : Int) ^ b := by
 
 theorem pos_pow_of_pos (a : Int) (b : Nat) (h : 0 < a) : 0 < a ^ b := by
   rw [Int.eq_natAbs_of_zero_le (Int.le_of_lt h), ← Int.ofNat_zero, ← Int.ofNat_pow, Int.ofNat_lt]
-  exact Nat.pos_pow_of_pos _ (Int.natAbs_pos.mpr (Int.ne_of_gt h))
+  exact Nat.pow_pos (Int.natAbs_pos.mpr (Int.ne_of_gt h))
 
 theorem ofNat_pos {a : Nat} : 0 < (a : Int) ↔ 0 < a := by
   rw [← Int.ofNat_zero, Int.ofNat_lt]

src/Std/Data/Internal/List/Associative.lean

@@ -29,7 +29,7 @@ open List (Perm Sublist pairwise_cons erase_sublist filter_sublist)
 
 namespace Std.Internal.List
 
-attribute [-simp] List.isEmpty_eq_false
+attribute [-simp] List.isEmpty_eq_false_iff
 
 @[elab_as_elim]
 theorem assoc_induction {motive : List ((a : α) × β a) → Prop} (nil : motive [])
@@ -3127,7 +3127,7 @@ theorem alterKey_cons_perm {k : α} {f : Option β → Option β} {k' : α} {v'
 theorem isEmpty_alterKey_eq_isEmpty_eraseKey {k : α} {f : Option β → Option β}
     {l : List ((_ : α) × β)} :
     (alterKey k f l).isEmpty = ((eraseKey k l).isEmpty && (f (getValue? k l)).isNone) := by
-  simp only [alterKey, List.isEmpty_eq_true]
+  simp only [alterKey, List.isEmpty_iff]
   split <;> { next heq => simp [heq] }
 
 theorem isEmpty_alterKey {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)} :

src/Std/Sat/AIG/Basic.lean

@@ -186,7 +186,7 @@ The empty array is a DAG.
 -/
 theorem IsDAG.empty {α : Type} : IsDAG α #[] := by
   intro i lhs rhs linv rinv h
-  simp only [Array.size_toArray, List.length_nil] at h
+  simp only [List.size_toArray, List.length_nil] at h
   omega
 
 end AIG

src/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean

@@ -112,7 +112,7 @@ theorem limplies_insert [Clause α β] [Entails α σ] [Formula α β σ] {c :
   simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq]
   intro h c' c'_in_f
   have c'_in_fc : c' ∈ toList (insert f c) := by
-    simp only [insert_iff, Array.toList_toArray, List.mem_singleton]
+    simp only [insert_iff, List.toList_toArray, List.mem_singleton]
     exact Or.inr c'_in_f
   exact h c' c'_in_fc
 

src/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean

@@ -61,7 +61,7 @@ theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈
   | nil => cases h1
   | cons hd tl ih =>
     unfold DefaultClause.ofArray at h2
-    rw [← Array.foldr_toList, List.toArray_toList] at h2
+    rw [← Array.foldr_toList, Array.toArray_toList] at h2
     dsimp only [List.foldr] at h2
     split at h2
     · cases h2
@@ -77,7 +77,7 @@ theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈
             · assumption
             · next heq _ _ =>
               unfold DefaultClause.ofArray
-              rw [← Array.foldr_toList, List.toArray_toList]
+              rw [← Array.foldr_toList, Array.toArray_toList]
               exact heq
         · cases h1
           · simp only [← Option.some.inj h2]
@@ -89,7 +89,7 @@ theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈
             apply ih
             assumption
             unfold DefaultClause.ofArray
-            rw [← Array.foldr_toList, List.toArray_toList]
+            rw [← Array.foldr_toList, Array.toArray_toList]
             exact heq
 
 theorem CNF.Clause.convertLRAT_sat_of_sat (clause : CNF.Clause (PosFin n))
@@ -155,7 +155,7 @@ theorem CNF.unsat_of_convertLRAT_unsat (cnf : CNF Nat) :
   simp only [Formula.formulaEntails_def, List.all_eq_true, decide_eq_true_eq]
   intro lratClause hlclause
   simp only [Formula.toList, DefaultFormula.toList, DefaultFormula.ofArray,
-    CNF.convertLRAT', Array.size_toArray, List.length_map, Array.toList_toArray,
+    CNF.convertLRAT', List.size_toArray, List.length_map, List.toList_toArray,
     List.map_nil, List.append_nil, List.mem_filterMap, List.mem_map, id_eq, exists_eq_right] at hlclause
   rcases hlclause with ⟨reflectClause, ⟨hrclause1, hrclause2⟩⟩
   simp only [CNF.eval, List.all_eq_true] at h2

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

@@ -246,7 +246,7 @@ theorem limplies_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) :
   simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq]
   intro h c' c'_in_f
   have c'_in_fc : c' ∈ toList (insert f c) := by
-    simp only [insert_iff, Array.toList_toArray, List.mem_singleton]
+    simp only [insert_iff, List.toList_toArray, List.mem_singleton]
     exact Or.inr c'_in_f
   exact h c' c'_in_fc
 
@@ -494,7 +494,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
             · next id_eq_idx =>
               exfalso
               have idx_in_bounds2 : idx < f.clauses.size := by
-                conv => rhs; rw [Array.size_toArray]
+                conv => rhs; rw [List.size_toArray]
                 exact hbound
               simp only [id_eq_idx, getElem!_def, idx_in_bounds2, Array.getElem?_eq_getElem, ←
                 Array.getElem_toList] at heq
@@ -527,7 +527,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
             · next id_eq_idx =>
               exfalso
               have idx_in_bounds2 : idx < f.clauses.size := by
-                conv => rhs; rw [Array.size_toArray]
+                conv => rhs; rw [List.size_toArray]
                 exact hbound
               simp only [id_eq_idx, getElem!_def, idx_in_bounds2, Array.getElem?_eq_getElem, ←
                 Array.getElem_toList] at heq
@@ -587,7 +587,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
             · next id_eq_idx =>
               exfalso
               have idx_in_bounds2 : idx < f.clauses.size := by
-                conv => rhs; rw [Array.size_toArray]
+                conv => rhs; rw [List.size_toArray]
                 exact hbound
               simp only [id_eq_idx, getElem!_def, idx_in_bounds2, Array.getElem?_eq_getElem, ←
                 Array.getElem_toList] at heq

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

@@ -42,7 +42,7 @@ theorem insertRatUnits_postcondition {n : Nat} (f : DefaultFormula n)
     apply Or.inl
     simp only [Fin.getElem_fin, ne_eq, true_and, Bool.not_eq_true, exists_and_right]
     intro j
-    simp only [hf.1, Array.size_toArray, List.length_nil] at j
+    simp only [hf.1, List.size_toArray, List.length_nil] at j
     exact Fin.elim0 j
   exact insertUnitInvariant_insertUnit_fold f.assignments hf.2 f.ratUnits f.assignments hsize false units h0
 

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

@@ -291,7 +291,7 @@ theorem sat_of_insertRat {n : Nat} (f : DefaultFormula n)
       apply List.get_mem
     have ib_in_insertUnit_fold := mem_insertUnit_fold_units f.ratUnits f.assignments false (negate c) (i, b) ib_in_insertUnit_fold
     simp only [negate, Literal.negate, List.mem_map, Prod.mk.injEq, Prod.exists, Bool.exists_bool,
-      Bool.not_false, Bool.not_true, hf.1, Array.toList_toArray, List.find?, List.not_mem_nil, or_false]
+      Bool.not_false, Bool.not_true, hf.1, List.toList_toArray, List.find?, List.not_mem_nil, or_false]
       at ib_in_insertUnit_fold
     rw [hboth] at h2
     rcases ib_in_insertUnit_fold with ⟨i', ⟨i_false_in_c, i'_eq_i, b_eq_true⟩ | ⟨i_true_in_c, i'_eq_i, b_eq_false⟩⟩
@@ -344,7 +344,7 @@ theorem sat_of_insertRat {n : Nat} (f : DefaultFormula n)
     have i_false_in_insertUnit_fold :=
       mem_insertUnit_fold_units #[] f.assignments false (c.clause.map Literal.negate) (i, false) i_false_in_insertUnit_fold
     simp only [Literal.negate, List.mem_map, Prod.mk.injEq, Bool.not_eq_true', Prod.exists,
-      exists_eq_right_right, exists_eq_right, Array.toList_toArray, List.find?, List.not_mem_nil, or_false,
+      exists_eq_right_right, exists_eq_right, List.toList_toArray, List.find?, List.not_mem_nil, or_false,
       Bool.not_eq_false'] at i_true_in_insertUnit_fold i_false_in_insertUnit_fold
     have c_not_tautology := Clause.not_tautology c (i, true)
     simp only [Clause.toList] at c_not_tautology
@@ -440,7 +440,7 @@ theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n)
     (ratHintsExhaustive_eq_true : ratHintsExhaustive f pivot ratHints = true) (c' : DefaultClause n)
     (c'_in_f : c' ∈ toList f) (negPivot_in_c' : Literal.negate pivot ∈ Clause.toList c') :
     ∃ i : Fin ratHints.size, f.clauses[ratHints[i].1]! = some c' := by
-  simp only [toList, f_readyForRatAdd.2.1, Array.toList_toArray, List.map, List.append_nil, f_readyForRatAdd.1,
+  simp only [toList, f_readyForRatAdd.2.1, List.toList_toArray, List.map, List.append_nil, f_readyForRatAdd.1,
     List.mem_filterMap, id_eq, exists_eq_right] at c'_in_f
   rw [List.mem_iff_getElem] at c'_in_f
   rcases c'_in_f with ⟨i, hi, c'_in_f⟩
@@ -559,7 +559,7 @@ theorem safe_insert_of_performRatCheck_fold_success {n : Nat} (f : DefaultFormul
       simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq, Classical.not_forall,
         not_imp] at fc_unsat
       rcases fc_unsat with ⟨c', c'_in_fc, p'_not_entails_c'⟩
-      simp only [insert_iff, Array.toList_toArray, List.mem_singleton] at c'_in_fc
+      simp only [insert_iff, List.toList_toArray, List.mem_singleton] at c'_in_fc
       rcases c'_in_fc with c'_eq_c | c'_in_f
       · rw [← c'_eq_c] at p'_entails_c
         exact p'_not_entails_c' p'_entails_c

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

@@ -392,7 +392,7 @@ theorem insertUnitInvariant_insertRupUnits {n : Nat} (f : DefaultFormula n) (f_r
     simp only [Fin.getElem_fin, ne_eq, true_and, Bool.not_eq_true, exists_and_right]
     apply Or.inl
     intro j
-    simp only [f_readyForRupAdd.1, Array.size_toArray, List.length_nil] at j
+    simp only [f_readyForRupAdd.1, List.size_toArray, List.length_nil] at j
     exact Fin.elim0 j
   exact insertUnitInvariant_insertUnit_fold f.assignments hsize f.rupUnits f.assignments hsize false units h0
 
@@ -1114,11 +1114,11 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
     simp [li, Array.getElem_mem]
   have i_in_bounds : i.1 < derivedLits.length := by
     have i_property := i.2
-    simp only [derivedLits_arr_def, Array.size_toArray] at i_property
+    simp only [derivedLits_arr_def, List.size_toArray] at i_property
     exact i_property
   have j_in_bounds : j.1 < derivedLits.length := by
     have j_property := j.2
-    simp only [derivedLits_arr_def, Array.size_toArray] at j_property
+    simp only [derivedLits_arr_def, List.size_toArray] at j_property
     exact j_property
   rcases derivedLits_satisfies_invariant ⟨li.1.1, li.1.2.2⟩ with ⟨_, h2⟩ | ⟨k, _, _, _, h3⟩ |
     ⟨k1, k2, _, _, k1_eq_true, k2_eq_false, _, _, h3⟩
@@ -1215,7 +1215,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
       exact h2 derivedLits_arr[j] idx_in_list
   · apply Or.inr ∘ Or.inl
     have j_lt_derivedLits_arr_size : j.1 < derivedLits_arr.size := by
-      simp only [derivedLits_arr_def, Array.size_toArray]
+      simp only [derivedLits_arr_def, List.size_toArray]
       exact j.2
     have i_gt_zero : i.1 > 0 := by rw [← j_eq_i]; exact (List.get derivedLits j).1.2.1
     refine ⟨⟨j.1, j_lt_derivedLits_arr_size⟩, List.get derivedLits j |>.2, i_gt_zero, ?_⟩
@@ -1228,7 +1228,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
         intro k _ k_ne_j
         have k_in_bounds : k < derivedLits.length := by
           have k_property := k.2
-          simp only [derivedLits_arr_def, Array.size_toArray] at k_property
+          simp only [derivedLits_arr_def, List.size_toArray] at k_property
           exact k_property
         have k_ne_j : ⟨k.1, k_in_bounds⟩ ≠ j := by
           apply Fin.ne_of_val_ne
@@ -1238,10 +1238,10 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
         exact h3 ⟨k.1, k_in_bounds⟩ k_ne_j
   · apply Or.inr ∘ Or.inr
     have j1_lt_derivedLits_arr_size : j1.1 < derivedLits_arr.size := by
-      simp only [derivedLits_arr_def, Array.size_toArray]
+      simp only [derivedLits_arr_def, List.size_toArray]
       exact j1.2
     have j2_lt_derivedLits_arr_size : j2.1 < derivedLits_arr.size := by
-      simp only [derivedLits_arr_def, Array.size_toArray]
+      simp only [derivedLits_arr_def, List.size_toArray]
       exact j2.2
     have i_gt_zero : i.1 > 0 := by rw [← j1_eq_i]; exact (List.get derivedLits j1).1.2.1
     refine ⟨⟨j1.1, j1_lt_derivedLits_arr_size⟩,
@@ -1259,7 +1259,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
         intro k _ k_ne_j1 k_ne_j2
         have k_in_bounds : k < derivedLits.length := by
           have k_property := k.2
-          simp only [derivedLits_arr_def, Array.size_toArray] at k_property
+          simp only [derivedLits_arr_def, List.size_toArray] at k_property
           exact k_property
         have k_ne_j1 : ⟨k.1, k_in_bounds⟩ ≠ j1 := by
           apply Fin.ne_of_val_ne

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

@@ -135,7 +135,7 @@ theorem sat_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : Re
     simp only [Fin.getElem_fin, ne_eq, true_and, Bool.not_eq_true, exists_and_right]
     apply Or.inl
     intro j
-    simp only [f_readyForRupAdd.1, Array.size_toArray, List.length_nil] at j
+    simp only [f_readyForRupAdd.1, List.size_toArray, List.length_nil] at j
     exact Fin.elim0 j
   have insertUnit_fold_satisfies_invariant := insertUnitInvariant_insertUnit_fold f.assignments f_readyForRupAdd.2.1 f.rupUnits
     f.assignments f_readyForRupAdd.2.1 false (negate c) h0
@@ -157,7 +157,7 @@ theorem sat_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : Re
       apply List.get_mem
     have ib_in_insertUnit_fold := mem_insertUnit_fold_units f.rupUnits f.assignments false (negate c) (i, b) ib_in_insertUnit_fold
     simp only [negate, Literal.negate, List.mem_map, Prod.mk.injEq, Prod.exists, Bool.exists_bool,
-      Bool.not_false, Bool.not_true, f_readyForRupAdd.1, Array.toList_toArray, List.find?, List.not_mem_nil, or_false]
+      Bool.not_false, Bool.not_true, f_readyForRupAdd.1, List.toList_toArray, List.find?, List.not_mem_nil, or_false]
       at ib_in_insertUnit_fold
     rw [hboth] at h2
     rcases ib_in_insertUnit_fold with ⟨i', ⟨i_false_in_c, i'_eq_i, b_eq_true⟩ | ⟨i_true_in_c, i'_eq_i, b_eq_false⟩⟩
@@ -211,7 +211,7 @@ theorem sat_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : Re
     have i_false_in_insertUnit_fold :=
       mem_insertUnit_fold_units #[] f.assignments false (c.clause.map Literal.negate) (i, false) i_false_in_insertUnit_fold
     simp only [Literal.negate, List.mem_map, Prod.mk.injEq, Bool.not_eq_true', Prod.exists,
-      exists_eq_right_right, exists_eq_right, Array.toList_toArray, List.find?, List.not_mem_nil, or_false,
+      exists_eq_right_right, exists_eq_right, List.toList_toArray, List.find?, List.not_mem_nil, or_false,
       Bool.not_eq_false'] at i_true_in_insertUnit_fold i_false_in_insertUnit_fold
     have c_not_tautology := Clause.not_tautology c (i, true)
     simp only [Clause.toList, (· ⊨ ·)] at c_not_tautology
@@ -252,7 +252,7 @@ theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f
     rcases cf with cf | cf | cf
     · specialize hp c (Or.inl cf)
       exact hp
-    · simp only [f_readyForRupAdd.1, Array.toList_toArray, List.find?, List.not_mem_nil, false_and, or_self, exists_false] at cf
+    · simp only [f_readyForRupAdd.1, List.toList_toArray, List.find?, List.not_mem_nil, false_and, or_self, exists_false] at cf
     · specialize hp c <| (Or.inr ∘ Or.inr) cf
       exact hp
   rcases h ⟨i.1, i.2.2⟩ with ⟨h1, h2⟩ | ⟨j, b', i_gt_zero, h1, h2, h3, h4⟩ | ⟨j1, j2, i_gt_zero, h1, h2, _, _, _⟩

tests/lean/run/2846.lean

@@ -17,13 +17,13 @@ The List argument is not named, it is not printed as a named argument.
 /-!
 All arguments are named, all are printed as named arguments.
 -/
-/-- info: Nat.pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) : 0 < n ^ m -/
-#guard_msgs in #check Nat.pos_pow_of_pos
+/-- info: Nat.pow_pos {a n : Nat} (h : 0 < a) : 0 < a ^ n -/
+#guard_msgs in #check Nat.pow_pos
 
 /-!
 The hypothesis is not a named argument, so it's not printed as a named argument.
 -/
-def Nat.pos_pow_of_pos' {n : Nat} (m : Nat) : 0 < n → 0 < n ^ m := Nat.pos_pow_of_pos m
+def Nat.pos_pow_of_pos' {n : Nat} (m : Nat) : 0 < n → 0 < n ^ m := @Nat.pow_pos _ m
 
 /-- info: Nat.pos_pow_of_pos' {n : Nat} (m : Nat) : 0 < n → 0 < n ^ m -/
 #guard_msgs in #check Nat.pos_pow_of_pos'