deprecations

src/Init/Core.lean

@@ -1598,9 +1598,13 @@ theorem true_imp_iff {α : Prop} : (True → α) ↔ α := imp_iff_right True.in
 
 @[simp] theorem imp_false : (a → False) ↔ ¬a := Iff.rfl
 
-theorem imp.swap : (a → b → c) ↔ (b → a → c) := Iff.intro flip flip
+theorem imp_swap : (a → b → c) ↔ (b → a → c) := Iff.intro flip flip
 
-theorem imp_not_comm : (a → ¬b) ↔ (b → ¬a) := imp.swap
+set_option linter.missingDocs false in
+@[deprecated imp_swap (since := "2025-03-18")]
+abbrev imp.swap := @imp_swap
+
+theorem imp_not_comm : (a → ¬b) ↔ (b → ¬a) := imp_swap
 
 theorem imp_congr_left (h : a ↔ b) : (a → c) ↔ (b → c) := Iff.intro (· ∘ h.mpr) (· ∘ h.mp)
 

src/Init/Data/Array/Lemmas.lean

@@ -1004,11 +1004,14 @@ theorem mem_or_eq_of_mem_setIfInBounds
   simpa using List.mem_or_eq_of_mem_set (by simpa using h)
 
 /-- Simplifies a normal form from `get!` -/
-@[simp] theorem getD_get?_setIfInBounds (xs : Array α) (i : Nat) (v d : α) :
+@[simp] theorem getD_getElem?_setIfInBounds (xs : Array α) (i : Nat) (v d : α) :
     (xs.setIfInBounds i v)[i]?.getD d = if i < xs.size then v else d := by
   by_cases h : i < xs.size <;>
     simp [setIfInBounds, Nat.not_lt_of_le, h,  getD_getElem?]
 
+@[deprecated getD_getElem?_setIfInBounds (since := "2025-03-18")]
+abbrev getD_get?_setIfInBounds := @getD_getElem?_setIfInBounds
+
 @[simp] theorem toList_setIfInBounds (xs : Array α) (i x) :
     (xs.setIfInBounds i x).toList = xs.toList.set i x := by
   simp only [setIfInBounds]
@@ -1018,14 +1021,20 @@ theorem mem_or_eq_of_mem_setIfInBounds
 
 /-! ### BEq -/
 
-@[simp] theorem beq_empty_iff [BEq α] {xs : Array α} : (xs == #[]) = xs.isEmpty := by
+@[simp] theorem beq_empty_eq [BEq α] {xs : Array α} : (xs == #[]) = xs.isEmpty := by
   cases xs
   simp
 
-@[simp] theorem empty_beq_iff [BEq α] {xs : Array α} : (#[] == xs) = xs.isEmpty := by
+@[deprecated beq_empty_eq (since := "2025-03-18")]
+abbrev beq_empty_iff := @beq_empty_eq
+
+@[simp] theorem empty_beq_eq [BEq α] {xs : Array α} : (#[] == xs) = xs.isEmpty := by
   cases xs
   simp
 
+@[deprecated empty_beq_eq (since := "2025-03-18")]
+abbrev empty_beq_iff := @empty_beq_eq
+
 @[simp] theorem push_beq_push [BEq α] {a b : α} {xs ys : Array α} :
     (xs.push a == ys.push b) = (xs == ys && a == b) := by
   cases xs
@@ -1636,10 +1645,13 @@ theorem forall_none_of_filterMap_eq_empty (h : filterMap f xs = #[]) : ∀ x ∈
   cases xs
   simpa using h
 
-@[simp] theorem filterMap_eq_nil_iff {xs : Array α} : filterMap f xs = #[] ↔ ∀ a, a ∈ xs → f a = none := by
+@[simp] theorem filterMap_eq_empty_iff {xs : Array α} : filterMap f xs = #[] ↔ ∀ a, a ∈ xs → f a = none := by
   cases xs
   simp
 
+@[deprecated filterMap_eq_empty_iff (since := "2025-03-18")]
+abbrev filterMap_eq_nil_iff := @filterMap_eq_empty_iff
+
 theorem filterMap_eq_push_iff {f : α → Option β} {xs : Array α} {ys : Array β} {b : β} :
     filterMap f xs = ys.push b ↔ ∃ as a bs,
       xs = as.push a ++ bs ∧ filterMap f as = ys ∧ f a = some b ∧ (∀ x, x ∈ bs → f x = none) := by
@@ -3487,7 +3499,10 @@ theorem size_rightpad (n : Nat) (a : α) (xs : Array α) :
 
 /-! ### contains -/
 
-theorem elem_cons_self [BEq α] [LawfulBEq α] {xs : Array α} {a : α} : (xs.push a).elem a = true := by simp
+theorem elem_push_self [BEq α] [LawfulBEq α] {xs : Array α} {a : α} : (xs.push a).elem a = true := by simp
+
+@[deprecated elem_push_self (since := "2025-03-18")]
+abbrev elem_cons_push := @elem_push_self
 
 theorem contains_eq_any_beq [BEq α] (xs : Array α) (a : α) : xs.contains a = xs.any (a == ·) := by
   rcases xs with ⟨xs⟩
@@ -4062,7 +4077,8 @@ theorem getElem!_eq_getD [Inhabited α] (xs : Array α) : xs[i]! = xs.getD i def
 
 @[simp] theorem mem_toList {a : α} {xs : Array α} : a ∈ xs.toList ↔ a ∈ xs := mem_def.symm
 
-theorem not_mem_nil (a : α) : ¬ a ∈ #[] := nofun
+@[deprecated not_mem_empty (since := "2025-03-18")]
+abbrev not_mem_nil := @not_mem_empty
 
 /-! # get lemmas -/
 
@@ -4440,7 +4456,7 @@ abbrev eq_push_pop_back_of_size_ne_zero := @eq_push_pop_back!_of_size_ne_zero
 @[deprecated size_setIfInBounds (since := "2024-11-24")] abbrev size_setD := @size_setIfInBounds
 @[deprecated getElem_setIfInBounds_eq (since := "2024-11-24")] abbrev getElem_setD_eq := @getElem_setIfInBounds_self
 @[deprecated getElem?_setIfInBounds_eq (since := "2024-11-24")] abbrev get?_setD_eq := @getElem?_setIfInBounds_self
-@[deprecated getD_get?_setIfInBounds (since := "2024-11-24")] abbrev getD_setD := @getD_get?_setIfInBounds
+@[deprecated getD_getElem?_setIfInBounds (since := "2024-11-24")] abbrev getD_setD := @getD_getElem?_setIfInBounds
 @[deprecated getElem_setIfInBounds (since := "2024-11-24")] abbrev getElem_setD := @getElem_setIfInBounds
 
 @[deprecated List.getElem_toArray (since := "2024-11-29")]

src/Init/Data/BitVec/Bitblast.lean

@@ -134,14 +134,14 @@ private theorem testBit_limit {x i : Nat} (x_lt_succ : x < 2^(i+1)) :
     testBit x i = decide (x ≥ 2^i) := by
   cases xi : testBit x i with
   | true =>
-    simp [testBit_implies_ge xi]
+    simp [ge_two_pow_of_testBit xi]
   | false =>
     simp
     cases Nat.lt_or_ge x (2^i) with
     | inl x_lt =>
       exact x_lt
     | inr x_ge =>
-      have ⟨j, ⟨j_ge, jp⟩⟩  := ge_two_pow_implies_high_bit_true x_ge
+      have ⟨j, ⟨j_ge, jp⟩⟩ := exists_testBit_ge_of_ge_two_pow x_ge
       cases Nat.lt_or_eq_of_le j_ge with
       | inr x_eq =>
         simp [x_eq, jp] at xi
@@ -150,7 +150,7 @@ private theorem testBit_limit {x i : Nat} (x_lt_succ : x < 2^(i+1)) :
         apply Nat.lt_irrefl
         calc x < 2^(i+1) := x_lt_succ
              _ ≤ 2 ^ j := Nat.pow_le_pow_right Nat.zero_lt_two x_lt
-             _ ≤ x := testBit_implies_ge jp
+             _ ≤ x := ge_two_pow_of_testBit jp
 
 private theorem mod_two_pow_succ (x i : Nat) :
     x % 2^(i+1) = 2^i*(x.testBit i).toNat + x % (2 ^ i):= by
@@ -419,7 +419,7 @@ theorem getLsbD_neg {i : Nat} {x : BitVec w} :
       · rintro h j hj; exact And.right <| h j (by omega)
       · rintro h j hj; exact ⟨by omega, h j (by omega)⟩
   · have h_ge : w ≤ i := by omega
-    simp [getLsbD_ge _ _ h_ge, h_ge, hi]
+    simp [getLsbD_of_ge _ _ h_ge, h_ge, hi]
 
 theorem getElem_neg {i : Nat} {x : BitVec w} (h : i < w) :
     (-x)[i] = (x[i] ^^ decide (∃ j < i, x.getLsbD j = true)) := by

src/Init/Data/BitVec/Lemmas.lean

@@ -27,18 +27,26 @@ namespace BitVec
 @[simp] theorem getElem_ofFin (x : Fin (2^n)) (i : Nat) (h : i < n) :
     (BitVec.ofFin x)[i] = x.val.testBit i := rfl
 
-@[simp] theorem getLsbD_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false := by
+@[simp] theorem getLsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false := by
   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_right (by omega) ge
   omega
 
-@[simp] theorem getMsbD_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getMsbD x i = false := by
+set_option linter.missingDocs false in
+@[deprecated getLsbD_of_ge (since := "2025-03-18")]
+abbrev getLsbD_ge := @getLsbD_of_ge
+
+@[simp] theorem getMsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getMsbD x i = false := by
   rw [getMsbD]
   simp only [Bool.and_eq_false_imp, decide_eq_true_eq]
   omega
 
+set_option linter.missingDocs false in
+@[deprecated getMsbD_of_ge (since := "2025-03-18")]
+abbrev getMsbD_ge := @getMsbD_of_ge
+
 theorem lt_of_getLsbD {x : BitVec w} {i : Nat} : getLsbD x i = true → i < w := by
   if h : i < w then
     simp [h]
@@ -149,20 +157,32 @@ theorem getLsbD_eq_getMsbD (x : BitVec w) (i : Nat) : x.getLsbD i = (decide (i <
   · congr
     omega
   all_goals
-    apply getLsbD_ge
+    apply getLsbD_of_ge
     omega
 
-@[simp] theorem getLsb?_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : x[i]? = none := by
+@[simp] theorem getElem?_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : x[i]? = none := by
   simp [ge]
 
-@[simp] theorem getMsb?_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getMsb? x i = none := by
+set_option linter.missingDocs false in
+@[deprecated getElem?_of_ge (since := "2025-03-18")]
+abbrev getLsb?_ge := @getElem?_of_ge
+
+@[simp] theorem getMsb?_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getMsb? x i = none := by
   simp [getMsb?_eq_getLsb?]; omega
 
-theorem lt_of_getLsb?_eq_some (x : BitVec w) (i : Nat) : x[i]? = some b → i < w := by
+set_option linter.missingDocs false in
+@[deprecated getMsb?_of_ge (since := "2025-03-18")]
+abbrev getMsb?_ge := @getMsb?_of_ge
+
+theorem lt_of_getElem?_eq_some (x : BitVec w) (i : Nat) : x[i]? = some b → i < w := by
   cases h : x[i]? with
   | none => simp
   | some => by_cases i < w <;> simp_all
 
+set_option linter.missingDocs false in
+@[deprecated lt_of_getElem?_eq_some (since := "2025-03-18")]
+abbrev lt_of_getLsb?_eq_some := @lt_of_getElem?_eq_some
+
 theorem lt_of_getMsb?_eq_some (x : BitVec w) (i : Nat) : getMsb? x i = some b → i < w := by
   if h : i < w then
     simp [h]
@@ -201,7 +221,7 @@ theorem eq_of_getLsbD_eq {x y : BitVec w}
     exact pred i i_lt
   else
     have p : i ≥ w := Nat.le_of_not_gt i_lt
-    simp [testBit_toNat, getLsbD_ge _ _ p]
+    simp [testBit_toNat, getLsbD_of_ge _ _ p]
 
 @[ext] theorem eq_of_getElem_eq {x y : BitVec n} :
         (∀ i (hi : i < n), x[i] = y[i]) → x = y :=
@@ -810,8 +830,8 @@ theorem getElem?_setWidth (m : Nat) (x : BitVec n) (i : Nat) :
     simp only [h₁, h₂, h₃, h₄]
     simp_all only [ge_iff_le, decide_eq_true_eq, Nat.not_le, Nat.not_lt, Bool.true_and,
       Bool.false_and, Bool.and_self] <;>
-    (try apply getLsbD_ge) <;>
-    (try apply (getLsbD_ge _ _ _).symm) <;>
+    (try apply getLsbD_of_ge) <;>
+    (try apply (getLsbD_of_ge _ _ _).symm) <;>
     omega
 
 @[simp] theorem getLsbD_setWidth (m : Nat) (x : BitVec n) (i : Nat) :
@@ -850,7 +870,7 @@ theorem setWidth'_eq {x : BitVec w} (h : w ≤ v) : x.setWidth' h = x.setWidth v
     <;> simp [h₁, h₂, h₃]
   · congr 1
     omega
-  all_goals (first | apply getLsbD_ge | apply Eq.symm; apply getLsbD_ge)
+  all_goals (first | apply getLsbD_of_ge | apply Eq.symm; apply getLsbD_of_ge)
     <;> omega
 
 @[simp] theorem cast_setWidth (h : v = v') (x : BitVec w) :
@@ -1648,7 +1668,7 @@ theorem shiftLeft_or_distrib (x y : BitVec w) (n : Nat) :
   by_cases h₁ : k < w <;> by_cases h₂ : w - (1 + k) < i <;> by_cases h₃ : k + i < w
     <;> simp only [h₁, h₂, h₃, decide_false, h₂, decide_true, Bool.not_true, Bool.false_and, Bool.and_self,
       Bool.true_and, Bool.false_eq, Bool.false_and, Bool.not_false]
-    <;> (first | apply getLsbD_ge | apply Eq.symm; apply getLsbD_ge)
+    <;> (first | apply getLsbD_of_ge | apply Eq.symm; apply getLsbD_of_ge)
     <;> omega
 
 theorem shiftLeftZeroExtend_eq {x : BitVec w} :
@@ -1676,7 +1696,7 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
   simp only [getLsbD_shiftLeft, getLsbD_setWidth]
   cases h₁ : decide (i < n) <;> cases h₂ : decide (i - n < m + n) <;> cases h₃ : decide (i < m + n)
     <;> simp_all
-    <;> (rw [getLsbD_ge]; omega)
+    <;> (rw [getLsbD_of_ge]; omega)
 
 @[simp] theorem getMsbD_shiftLeftZeroExtend (x : BitVec m) (n : Nat) :
     getMsbD (shiftLeftZeroExtend x n) i = getMsbD x i := by
@@ -1844,7 +1864,7 @@ theorem getMsbD_ushiftRight {x : BitVec w} {i n : Nat} :
     (x >>> n).getMsbD i = (decide (i < w) && (!decide (i < n) && x.getMsbD (i - n))) := by
   simp only [getMsbD, getLsbD_ushiftRight]
   by_cases h : i < n
-  · simp [getLsbD_ge, show w ≤ (n + (w - 1 - i)) by omega]
+  · simp [getLsbD_of_ge, show w ≤ (n + (w - 1 - i)) by omega]
     omega
   · by_cases h₁ : i < w
     · simp only [h, decide_false, Bool.not_false, show i - n < w by omega, decide_true,
@@ -1924,7 +1944,7 @@ theorem getLsbD_sshiftRight (x : BitVec w) (s i : Nat) :
   · simp only [sshiftRight_eq_of_msb_false hmsb, getLsbD_ushiftRight, Bool.if_false_right]
     by_cases hi : i ≥ w
     · simp only [hi, decide_true, Bool.not_true, Bool.false_and]
-      apply getLsbD_ge
+      apply getLsbD_of_ge
       omega
     · simp only [hi, decide_false, Bool.not_false, Bool.true_and, Bool.iff_and_self,
         decide_eq_true_eq]
@@ -2277,7 +2297,7 @@ private theorem toNat_signExtend_of_le (x : BitVec w) {v : Nat} (hv : w ≤ v) :
     rcases hi with hi | hi | hi
     · simp [hi]; omega
     · simp [hi]
-    · simp [hi, show ¬ (i < w + k) by omega, show ¬ (i < w) by omega, getLsbD_ge x i (by omega)]
+    · simp [hi, show ¬ (i < w + k) by omega, show ¬ (i < w) by omega, getLsbD_of_ge x i (by omega)]
 
 /-- Sign extending to a larger bitwidth depends on the msb.
 If the msb is false, then the result equals the original value.
@@ -2385,7 +2405,7 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
   · subst h
     simp [BitVec.msb, getMsbD]
   · have q : 0 < w + v := by omega
-    have t : y.getLsbD (w + v - 1) = false := getLsbD_ge _ _ (by omega)
+    have t : y.getLsbD (w + v - 1) = false := getLsbD_of_ge _ _ (by omega)
     simp [h, q, t, BitVec.msb, getMsbD]
 
 @[simp] theorem append_zero_width (x : BitVec w) (y : BitVec 0) : x ++ y = x := by
@@ -2500,7 +2520,7 @@ theorem setWidth_eq_append_extractLsb' {v : Nat} {x : BitVec v} {w : Nat} :
   by_cases hiv : i < v
   · simp [hi]
     omega
-  · simp [getLsbD_ge x i (by omega)]
+  · simp [getLsbD_of_ge x i (by omega)]
 
 /--
 A `(x : BitVec v)` set to a width `w ≥ v` equals `(w - v)` zeros, followed by `x`.
@@ -2513,7 +2533,7 @@ theorem setWidth_eq_append {v : Nat} {x : BitVec v} {w : Nat} (h : v ≤ w) :
   by_cases hiv : i < v
   · simp [hiv]
     omega
-  · simp [hiv, getLsbD_ge x i (by omega)]
+  · simp [hiv, getLsbD_of_ge x i (by omega)]
 
 theorem setWidth_eq_extractLsb' {v : Nat} {x : BitVec v} {w : Nat} (h : w ≤ v) :
     x.setWidth w = x.extractLsb' 0 w := by
@@ -2523,7 +2543,7 @@ theorem setWidth_eq_extractLsb' {v : Nat} {x : BitVec v} {w : Nat} (h : w ≤ v)
   by_cases hiv : i < v
   · simp [hi]
     omega
-  · simp [getLsbD_ge x i (by omega)]
+  · simp [getLsbD_of_ge x i (by omega)]
 
 theorem ushiftRight_eq_extractLsb'_of_lt {x : BitVec w} {n : Nat} (hn : n < w) :
     x >>> n = ((0#n) ++ (x.extractLsb' n (w - n))).cast (by omega) := by
@@ -2531,7 +2551,7 @@ theorem ushiftRight_eq_extractLsb'_of_lt {x : BitVec w} {n : Nat} (hn : n < w) :
   simp only [getElem_cast, getElem_append, getElem_zero, getElem_ushiftRight, getElem_extractLsb']
   split
   · simp
-  · exact getLsbD_ge x (n+i) (by omega)
+  · exact getLsbD_of_ge x (n+i) (by omega)
 
 theorem shiftLeft_eq_concat_of_lt {x : BitVec w} {n : Nat} (hn : n < w) :
     x <<< n = (x.extractLsb' 0 (w - n) ++ 0#n).cast (by omega) := by
@@ -2636,7 +2656,7 @@ theorem extractLsb'_append_eq_ite {v w} {xhi : BitVec v} {xlo : BitVec w} {start
   · simp only [hstart, ↓reduceDIte]
     ext i hi
     simp [getElem_extractLsb', getLsbD_append,
-      show ¬start + i < w by omega, ↓reduceIte, 
+      show ¬start + i < w by omega, ↓reduceIte,
       show start + i - w = start - w + i by omega]
 
 /-- Extracting bits `[start..start+len)` from `(xhi ++ xlo)` equals extracting
@@ -2697,7 +2717,7 @@ theorem getLsbD_cons (b : Bool) {n} (x : BitVec n) (i : Nat) :
     have p2 : i ≠ n := by omega
     simp [p1, p2]
   · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_true, Nat.sub_self, Nat.testBit_zero,
-    Bool.true_and, testBit_toNat, getLsbD_ge, Bool.or_false, ↓reduceIte]
+    Bool.true_and, testBit_toNat, getLsbD_of_ge, Bool.or_false, ↓reduceIte]
     cases b <;> trivial
   · have p1 : i ≠ n := by omega
     have p2 : i - n ≠ 0 := by omega
@@ -2712,7 +2732,7 @@ theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
     have p2 : i ≠ n := by omega
     simp [p1, p2]
   · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_true, Nat.sub_self, Nat.testBit_zero,
-    Bool.true_and, testBit_toNat, getLsbD_ge, Bool.or_false, ↓reduceIte]
+    Bool.true_and, testBit_toNat, getLsbD_of_ge, Bool.or_false, ↓reduceIte]
     cases b <;> trivial
   · have p1 : i ≠ n := by omega
     have p2 : i - n ≠ 0 := by omega
@@ -3850,11 +3870,15 @@ x.rotateLeft 2 = (<6 5 | 4 3 2 1 0>).rotateLeft 2 = <3 2 1 0 | 6 5>
 = <6 5 | 4 3 2 1 0>[i + len(<4 3 2 1 0>)]
 = <6 5 | 4 3 2 1 0>[i + 7 - 2]
 -/
-theorem getLsbD_rotateLeftAux_of_le {x : BitVec w} {r : Nat} {i : Nat} (hi : i < r) :
+theorem getLsbD_rotateLeftAux_of_lt {x : BitVec w} {r : Nat} {i : Nat} (hi : i < r) :
     (x.rotateLeftAux r).getLsbD i = x.getLsbD (w - r + i) := by
   rw [rotateLeftAux, getLsbD_or, getLsbD_ushiftRight]
   simp; omega
 
+set_option linter.missingDocs false in
+@[deprecated getLsbD_rotateLeftAux_of_lt (since := "2025-03-18")]
+abbrev getLsbD_rotateLeftAux_of_le := @getLsbD_rotateLeftAux_of_lt
+
 /--
 Accessing bits in `x.rotateLeft r` the range `[r, w)` is equal to
 accessing bits `x` in the range `[0, w - r)`.
@@ -3879,7 +3903,7 @@ theorem getLsbD_rotateLeftAux_of_geq {x : BitVec w} {r : Nat} {i : Nat} (hi : i
       simp [hi]
     simp [getLsbD_shiftLeft, Bool.or_false, hi, hiltr, this]
   simp only [getLsbD_ushiftRight]
-  apply getLsbD_ge
+  apply getLsbD_of_ge
   omega
 
 /-- When `r < w`, we give a formula for `(x.rotateLeft r).getLsbD i`. -/
@@ -3890,7 +3914,7 @@ theorem getLsbD_rotateLeft_of_le {x : BitVec w} {r i : Nat} (hr: r < w) :
       (decide (i < w) && x.getLsbD (i - r)) := by
   · rw [rotateLeft_eq_rotateLeftAux_of_lt hr]
     by_cases h : i < r
-    · simp [h, getLsbD_rotateLeftAux_of_le h]
+    · simp [h, getLsbD_rotateLeftAux_of_lt h]
     · simp [h, getLsbD_rotateLeftAux_of_geq <| Nat.ge_of_not_lt h]
 
 @[simp]
@@ -4022,7 +4046,7 @@ theorem getLsbD_rotateRightAux_of_geq {x : BitVec w} {r : Nat} {i : Nat} (hi : i
     by_cases hiw : i < w
     <;> simp [hiw, hi]
   simp only [getLsbD_ushiftRight]
-  apply getLsbD_ge
+  apply getLsbD_of_ge
   omega
 
 /-- `rotateRight` equals the bit fiddling definition of `rotateRightAux` when the rotation amount is
@@ -4174,7 +4198,7 @@ theorem msb_twoPow {i w: Nat} :
   omega
 
 theorem toInt_twoPow {w i : Nat} :
-    (BitVec.twoPow w i).toInt = if w ≤ i then 0 
+    (BitVec.twoPow w i).toInt = if w ≤ i then 0
       else if i + 1 = w then (-(2^i : Nat) : Int) else 2^i := by
   simp only [BitVec.toInt_eq_msb_cond, toNat_twoPow_eq_ite]
   rcases w with _ | w
@@ -4345,7 +4369,7 @@ theorem getLsbD_replicate {n w : Nat} {x : BitVec w} :
         rw [Nat.sub_mul_eq_mod_of_lt_of_le (by omega) (by omega)]
     · rw [Nat.mul_succ] at hi ⊢
       simp only [show ¬i < w * n by omega, decide_false, cond_false, hi, Bool.false_and]
-      apply BitVec.getLsbD_ge (x := x) (i := i - w * n) (ge := by omega)
+      apply BitVec.getLsbD_of_ge (x := x) (i := i - w * n) (ge := by omega)
 
 @[simp]
 theorem getElem_replicate {n w : Nat} {x : BitVec w} (h : i < w * n) :

src/Init/Data/Bool.lean

@@ -108,8 +108,14 @@ Needed for confluence of term `(a && b) ↔ a` which reduces to `(a && b) = a` v
 @[simp] theorem iff_self_and : ∀ {a b : Bool}, (a = (a && b)) ↔ (a → b) := by decide
 @[simp] theorem iff_and_self : ∀ {a b : Bool}, (b = (a && b)) ↔ (b → a) := by decide
 
-@[simp] theorem not_and_iff_left_iff_imp  : ∀ {a b : Bool}, ((!a && b) = a) ↔ !a ∧ !b := by decide
-@[simp] theorem and_not_iff_right_iff_imp : ∀ {a b : Bool}, ((a && !b) = b) ↔ !a ∧ !b := by decide
+@[simp] theorem not_and_eq_left_iff_not_and_not : ∀ {a b : Bool}, ((!a && b) = a) ↔ !a ∧ !b := by decide
+@[deprecated not_and_eq_left_iff_not_and_not (since := "2025-03-18")]
+abbrev not_and_iff_left_iff_imp := @not_and_eq_left_iff_not_and_not
+
+@[simp] theorem and_not_eq_right_iff_not_and_not : ∀ {a b : Bool}, ((a && !b) = b) ↔ !a ∧ !b := by decide
+@[deprecated and_not_eq_right_iff_not_and_not (since := "2025-03-18")]
+abbrev and_not_iff_right_iff_imp := @and_not_eq_right_iff_not_and_not
+
 @[simp] theorem iff_not_self_and : ∀ {a b : Bool}, (a = (!a && b)) ↔ !a ∧ !b := by decide
 @[simp] theorem iff_and_not_self : ∀ {a b : Bool}, (b = (a && !b)) ↔ !a ∧ !b := by decide
 
@@ -142,8 +148,14 @@ Needed for confluence of term `(a || b) ↔ a` which reduces to `(a || b) = a` v
 @[simp] theorem iff_self_or : ∀ {a b : Bool}, (a = (a || b)) ↔ (b → a) := by decide
 @[simp] theorem iff_or_self : ∀ {a b : Bool}, (b = (a || b)) ↔ (a → b) := by decide
 
-@[simp] theorem not_or_iff_left_iff_imp  : ∀ {a b : Bool}, ((!a || b) = a) ↔ a ∧ b := by decide
-@[simp] theorem or_not_iff_right_iff_imp : ∀ {a b : Bool}, ((a || !b) = b) ↔ a ∧ b := by decide
+@[simp] theorem not_or_eq_left_iff_and  : ∀ {a b : Bool}, ((!a || b) = a) ↔ a ∧ b := by decide
+@[deprecated not_or_eq_left_iff_and (since := "2025-03-18")]
+abbrev not_or_iff_left_iff_imp := @not_or_eq_left_iff_and
+
+@[simp] theorem or_not_eq_right_iff_and : ∀ {a b : Bool}, ((a || !b) = b) ↔ a ∧ b := by decide
+@[deprecated or_not_eq_right_iff_and (since := "2025-03-18")]
+abbrev or_not_iff_right_iff_imp := @or_not_eq_right_iff_and
+
 @[simp] theorem iff_not_self_or : ∀ {a b : Bool}, (a = (!a || b)) ↔ a ∧ b := by decide
 @[simp] theorem iff_or_not_self : ∀ {a b : Bool}, (b = (a || !b)) ↔ a ∧ b := by decide
 

src/Init/Data/List/Lemmas.lean

@@ -428,7 +428,10 @@ theorem forall_mem_ne {a : α} {l : List α} : (∀ a' : α, a' ∈ l → ¬a =
 theorem forall_mem_ne' {a : α} {l : List α} : (∀ a' : α, a' ∈ l → ¬a' = a) ↔ a ∉ l :=
   ⟨fun h m => h _ m rfl, fun h _ m e => h (e.symm ▸ m)⟩
 
-theorem exists_mem_nil (p : α → Prop) : ¬ (∃ x, ∃ _ : x ∈ @nil α, p x) := nofun
+theorem not_exists_mem_nil (p : α → Prop) : ¬ (∃ x, ∃ _ : x ∈ @nil α, p x) := nofun
+
+@[deprecated not_exists_mem_nil (since := "2025-03-18")]
+abbrev exists_mem_nil := @not_exists_mem_nil
 
 theorem forall_mem_nil (p : α → Prop) : ∀ (x) (_ : x ∈ @nil α), p x := nofun
 

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

@@ -134,7 +134,7 @@ theorem toNat_testBit (x i : Nat) :
   rw [Nat.testBit_to_div_mod]
   rcases Nat.mod_two_eq_zero_or_one (x / 2^i) <;> simp_all
 
-theorem ne_zero_implies_bit_true {x : Nat} (xnz : x ≠ 0) : ∃ i, testBit x i := by
+theorem exists_testBit_of_ne_zero {x : Nat} (xnz : x ≠ 0) : ∃ i, testBit x i := by
   induction x using div2Induction with
   | ind x hyp =>
     have x_pos : x > 0 := Nat.pos_of_ne_zero xnz
@@ -149,14 +149,17 @@ theorem ne_zero_implies_bit_true {x : Nat} (xnz : x ≠ 0) : ∃ i, testBit x i
       apply Exists.intro 0
       simp_all
 
-theorem ne_implies_bit_diff {x y : Nat} (p : x ≠ y) : ∃ i, testBit x i ≠ testBit y i := by
+@[deprecated exists_testBit_of_ne_zero (since := "2025-03-18")]
+abbrev ne_zero_implies_bit_true := @exists_testBit_of_ne_zero
+
+theorem exists_testBit_ne_of_ne {x y : Nat} (p : x ≠ y) : ∃ i, testBit x i ≠ testBit y i := by
   induction y using Nat.div2Induction generalizing x with
   | ind y hyp =>
     cases Nat.eq_zero_or_pos y with
     | inl yz =>
       simp only [yz, Nat.zero_testBit, Bool.eq_false_iff]
       simp only [yz] at p
-      have ⟨i,ip⟩  := ne_zero_implies_bit_true p
+      have ⟨i,ip⟩  := exists_testBit_of_ne_zero p
       apply Exists.intro i
       simp [ip]
     | inr ypos =>
@@ -175,6 +178,9 @@ theorem ne_implies_bit_diff {x y : Nat} (p : x ≠ y) : ∃ i, testBit x i ≠ t
           cases mod_two_eq_zero_or_one y with | _ q =>
             simp [p,q]
 
+@[deprecated exists_testBit_ne_of_ne (since := "2025-03-18")]
+abbrev ne_implies_bit_diff := @exists_testBit_ne_of_ne
+
 /--
 `eq_of_testBit_eq` allows proving two natural numbers are equal
 if their bits are all equal.
@@ -183,18 +189,18 @@ theorem eq_of_testBit_eq {x y : Nat} (pred : ∀i, testBit x i = testBit y i) :
   if h : x = y then
     exact h
   else
-    let ⟨i,eq⟩ := ne_implies_bit_diff h
+    let ⟨i,eq⟩ := exists_testBit_ne_of_ne h
     have p := pred i
     contradiction
 
-theorem ge_two_pow_implies_high_bit_true {x : Nat} (p : x ≥ 2^n) : ∃ i, i ≥ n ∧ testBit x i := by
+theorem exists_testBit_ge_of_ge_two_pow {x : Nat} (p : x ≥ 2^n) : ∃ i, i ≥ n ∧ testBit x i := by
   induction x using div2Induction generalizing n with
   | ind x hyp =>
     have x_pos : x > 0 := Nat.lt_of_lt_of_le (Nat.two_pow_pos n) p
     have x_ne_zero : x ≠ 0 := Nat.ne_of_gt x_pos
     match n with
     | zero =>
-      let ⟨j, jp⟩ := ne_zero_implies_bit_true x_ne_zero
+      let ⟨j, jp⟩ := exists_testBit_of_ne_zero x_ne_zero
       exact Exists.intro j (And.intro (Nat.zero_le _) jp)
     | succ n =>
       have x_ge_n : x / 2 ≥ 2 ^ n := by
@@ -207,25 +213,31 @@ theorem ge_two_pow_implies_high_bit_true {x : Nat} (p : x ≥ 2^n) : ∃ i, i
       case right =>
         simpa using jp.right
 
-theorem testBit_implies_ge {x : Nat} (p : testBit x i = true) : x ≥ 2^i := by
+@[deprecated exists_testBit_ge_of_ge_two_pow (since := "2025-03-18")]
+abbrev ge_two_pow_implies_high_bit_true := @exists_testBit_ge_of_ge_two_pow
+
+theorem ge_two_pow_of_testBit {x : Nat} (p : testBit x i = true) : x ≥ 2^i := by
   simp only [testBit_to_div_mod] at p
   apply Decidable.by_contra
   intro not_ge
   have x_lt : x < 2^i := Nat.lt_of_not_le not_ge
   simp [div_eq_of_lt x_lt] at p
 
+@[deprecated ge_two_pow_of_testBit (since := "2025-03-18")]
+abbrev testBit_implies_ge := @ge_two_pow_of_testBit
+
 theorem testBit_lt_two_pow {x i : Nat} (lt : x < 2^i) : x.testBit i = false := by
   match p : x.testBit i with
   | false => trivial
   | true =>
     exfalso
-    exact Nat.not_le_of_gt lt (testBit_implies_ge p)
+    exact Nat.not_le_of_gt lt (ge_two_pow_of_testBit p)
 
 theorem lt_pow_two_of_testBit (x : Nat) (p : ∀i, i ≥ n → testBit x i = false) : x < 2^n := by
   apply Decidable.by_contra
   intro not_lt
   have x_ge_n := Nat.ge_of_not_lt not_lt
-  have ⟨i, ⟨i_ge_n, test_true⟩⟩ := ge_two_pow_implies_high_bit_true x_ge_n
+  have ⟨i, ⟨i_ge_n, test_true⟩⟩ := exists_testBit_ge_of_ge_two_pow x_ge_n
   have test_false := p _ i_ge_n
   simp [test_true] at test_false
 

src/Init/Data/Vector/Lemmas.lean

@@ -510,7 +510,7 @@ theorem toList_append (xs : Vector α m) (ys : Vector α n) :
     (xs.drop i).toList = xs.toList.drop i := by
   simp [List.take_of_length_le]
 
-theorem toList_empty : (#v[] : Vector α 0).toArray = #[] := by simp
+theorem toList_empty : (#v[] : Vector α 0).toList = [] := by simp
 
 theorem toList_emptyWithCapacity (cap) :
     (Vector.emptyWithCapacity (α := α) cap).toList = [] := rfl
@@ -579,8 +579,8 @@ theorem toList_swap (xs : Vector α n) (i j) (hi hj) :
 @[simp] theorem toList_take (xs : Vector α n) (i) : (xs.take i).toList = xs.toList.take i := by
   simp [List.take_of_length_le]
 
-@[simp] theorem toList_zipWith (f : α → β → γ) (as : Vector α n) (bs : Vector β n) :
-    (Vector.zipWith f as bs).toArray = Array.zipWith f as.toArray bs.toArray := rfl
+theorem toList_zipWith (f : α → β → γ) (as : Vector α n) (bs : Vector β n) :
+    (Vector.zipWith f as bs).toList = List.zipWith f as.toList bs.toList := by simp
 
 @[simp] theorem anyM_toList [Monad m] (p : α → m Bool) (xs : Vector α n) :
     xs.toList.anyM p = xs.anyM p := by
@@ -649,11 +649,14 @@ theorem toList_inj {xs ys : Vector α n} : xs.toList = ys.toList ↔ xs = ys :=
   cases ys
   simp [Array.toList_inj]
 
-@[simp] theorem toList_eq_empty_iff (xs : Vector α n) : xs.toList = [] ↔ n = 0 := by
+@[simp] theorem toList_eq_nil_iff (xs : Vector α n) : xs.toList = [] ↔ n = 0 := by
   rcases xs with ⟨xs, h⟩
   simp only [Array.toList_eq_nil_iff]
   exact ⟨by rintro rfl; simp_all, by rintro rfl; simpa using h⟩
 
+@[deprecated toList_eq_nil_iff (since := "2025-03-18")]
+abbrev toList_eq_empty_iff := @toList_eq_nil_iff
+
 @[simp] theorem mem_toList_iff (a : α) (xs : Vector α n) : a ∈ xs.toList ↔ a ∈ xs := by
   simp
 

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsbD.lean

@@ -31,7 +31,7 @@ theorem denote_getD_eq_getLsbD (aig : AIG α) (assign : α → Bool) (x : BitVec
   · rw [hx]
   · rw [hfalse]
     symm
-    apply BitVec.getLsbD_ge
+    apply BitVec.getLsbD_of_ge
     omega
 
 @[simp]

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean

@@ -206,7 +206,7 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs :
         Bool.false_eq, Bool.and_eq_false_imp, Bool.and_eq_true, decide_eq_true_eq,
         Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_lt, and_imp]
         intros
-        apply BitVec.getLsbD_ge
+        apply BitVec.getLsbD_of_ge
         omega
       · rw [hleft]
         simp only [BitVec.shiftLeft_eq', BitVec.toNat_twoPow, hmod, BitVec.getLsbD_shiftLeft, hidx,
@@ -225,7 +225,7 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs :
       rw [hleft]
       simp
   · have : rhs.getLsbD pow = false := by
-      apply BitVec.getLsbD_ge
+      apply BitVec.getLsbD_of_ge
       dsimp only
       omega
     simp only [this, Bool.false_eq_true, ↓reduceIte]
@@ -294,7 +294,7 @@ theorem denote_blastShiftLeft (aig : AIG α) (target : ArbitraryShiftTarget aig
     subst hzero
     rw [← hg]
     simp only [hleft, Nat.zero_sub, BitVec.shiftLeftRec_zero, BitVec.and_twoPow, Nat.le_refl,
-      BitVec.getLsbD_ge, Bool.false_eq_true, ↓reduceIte, BitVec.reduceHShiftLeft',
+      BitVec.getLsbD_of_ge, Bool.false_eq_true, ↓reduceIte, BitVec.reduceHShiftLeft',
       BitVec.getLsbD_shiftLeft, Nat.sub_zero, Bool.iff_and_self, Bool.and_eq_true, decide_eq_true_eq,
       Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_lt, Nat.zero_le, and_true]
     apply BitVec.lt_of_getLsbD

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean

@@ -295,7 +295,7 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs :
         simp [hmod]
       · simp only [BitVec.ushiftRight_eq', BitVec.toNat_twoPow, BitVec.getLsbD_ushiftRight,
         Bool.false_eq]
-        apply BitVec.getLsbD_ge
+        apply BitVec.getLsbD_of_ge
         omega
     · next hif1 =>
       simp only [Bool.not_eq_true] at hif1
@@ -309,7 +309,7 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs :
       rw [hleft]
       simp
   · have : rhs.getLsbD pow = false := by
-      apply BitVec.getLsbD_ge
+      apply BitVec.getLsbD_of_ge
       dsimp only
       omega
     simp only [this, Bool.false_eq_true, ↓reduceIte]
@@ -442,7 +442,7 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs :
       rw [hleft]
       simp
   · have : rhs.getLsbD pow = false := by
-      apply BitVec.getLsbD_ge
+      apply BitVec.getLsbD_of_ge
       dsimp only
       omega
     simp only [this, Bool.false_eq_true, ↓reduceIte]