diff --git a/src/Init/Control/Basic.lean b/src/Init/Control/Basic.lean
index 18cb917817..37941387b5 100644
--- a/src/Init/Control/Basic.lean
+++ b/src/Init/Control/Basic.lean
@@ -36,11 +36,13 @@ instance (priority := 500) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α
   simp [h]
   rfl
 
-@[wf_preprocess] theorem forIn_eq_forin' [d : Membership α ρ] [ForIn' m ρ α d] {β} [Monad m]
+@[wf_preprocess] theorem forIn_eq_forIn' [d : Membership α ρ] [ForIn' m ρ α d] {β} [Monad m]
     (x : ρ) (b : β) (f : (a : α) → β → m (ForInStep β)) :
     forIn x b f = forIn' x b (fun x h => binderNameHint x f <| binderNameHint h () <| f x) := by
-  simp [binderNameHint]
-  rfl -- very strange why `simp` did not close it
+  rfl
+
+@[deprecated forIn_eq_forIn' (since := "2025-04-04")]
+abbrev forIn_eq_forin' := @forIn_eq_forIn'
 
 /--
 Extracts the value from a `ForInStep`, ignoring whether it is `ForInStep.done` or `ForInStep.yield`.
diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index f08cbf1b43..04f025115a 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -999,11 +999,19 @@ set_option linter.missingDocs false in
 theorem toBoolUsing_eq_true {p : Prop} (d : Decidable p) (h : p) : toBoolUsing d = true :=
   decide_eq_true (inst := d) h
 
-theorem ofBoolUsing_eq_true {p : Prop} {d : Decidable p} (h : toBoolUsing d = true) : p :=
-  of_decide_eq_true (inst := d) h
+theorem of_toBoolUsing_eq_true {p : Prop} {d : Decidable p} (h : toBoolUsing d = true) : p :=
+  of_decide_eq_true h
 
-theorem ofBoolUsing_eq_false {p : Prop} {d : Decidable p} (h : toBoolUsing d = false) : ¬ p :=
-  of_decide_eq_false (inst := d) h
+theorem of_toBoolUsing_eq_false {p : Prop} {d : Decidable p} (h : toBoolUsing d = false) : ¬p :=
+  of_decide_eq_false h
+
+set_option linter.missingDocs false in
+@[deprecated of_toBoolUsing_eq_true (since := "2025-04-04")]
+abbrev ofBoolUsing_eq_true := @of_toBoolUsing_eq_true
+
+set_option linter.missingDocs false in
+@[deprecated of_toBoolUsing_eq_false (since := "2025-04-04")]
+abbrev ofBoolUsing_eq_false := @of_toBoolUsing_eq_false
 
 instance : Decidable True :=
   isTrue trivial
@@ -1269,9 +1277,13 @@ theorem Relation.TransGen.trans {α : Sort u} {r : α → α → Prop} {a b c} :
 
 namespace Subtype
 
-theorem existsOfSubtype {α : Type u} {p : α → Prop} : { x // p x } → Exists (fun x => p x)
+theorem exists_of_subtype {α : Type u} {p : α → Prop} : { x // p x } → Exists (fun x => p x)
   | ⟨a, h⟩ => ⟨a, h⟩
 
+set_option linter.missingDocs false in
+@[deprecated exists_of_subtype (since := "2025-04-04")]
+abbrev existsOfSubtype := @exists_of_subtype
+
 variable {α : Type u} {p : α → Prop}
 
 protected theorem eq : ∀ {a1 a2 : {x // p x}}, val a1 = val a2 → a1 = a2
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index 0987c71822..d5941ee4c2 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -1026,7 +1026,7 @@ 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?]
@@ -1040,14 +1040,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
+@[simp] theorem empty_beq_eq [BEq α] {xs : Array α} : (#[] == xs) = xs.isEmpty := by
   cases xs
   simp
 
+@[deprecated beq_empty_eq (since := "2025-04-04")]
+abbrev beq_empty_iff := @beq_empty_eq
+
+@[deprecated empty_beq_eq (since := "2025-04-04")]
+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
@@ -1667,10 +1673,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-04-04")]
+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
@@ -3618,7 +3627,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-04-04")]
+abbrev elem_cons_self := @elem_push_self
 
 theorem contains_eq_any_beq [BEq α] {xs : Array α} {a : α} : xs.contains a = xs.any (a == ·) := by
   rcases xs with ⟨xs⟩
@@ -4587,7 +4599,8 @@ 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 := "2025-04-04")] abbrev getD_get?_setIfInBounds := @getD_getElem?_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")]
diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
index 7ae15cf92f..9591902d24 100644
--- a/src/Init/Data/BitVec/Bitblast.lean
+++ b/src/Init/Data/BitVec/Bitblast.lean
@@ -135,14 +135,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 [Nat.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_ge_and_testBit_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
@@ -151,7 +151,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
@@ -262,7 +262,7 @@ theorem getLsbD_add_add_bool {i : Nat} (i_lt : i < w) (x y : BitVec w) (c : Bool
       Nat.add_left_comm (_%_) (_ * _) _,
       testBit_limit (mod_two_pow_add_mod_two_pow_add_bool_lt_two_pow_succ x y i c)
     ]
-  simp [testBit_to_div_mod, carry, Nat.add_assoc]
+  simp [testBit_eq_decide_div_mod_eq, carry, Nat.add_assoc]
 
 theorem getLsbD_add {i : Nat} (i_lt : i < w) (x y : BitVec w) :
     getLsbD (x + y) i =
@@ -343,13 +343,13 @@ theorem add_eq_or_of_and_eq_zero {w : Nat} (x y : BitVec w)
 theorem getLsbD_sub {i : Nat} {i_lt : i < w} {x y : BitVec w} :
     (x - y).getLsbD i
       = (x.getLsbD i ^^ ((~~~y + 1#w).getLsbD i ^^ carry i x (~~~y + 1#w) false)) := by
-  rw [sub_toAdd, BitVec.neg_eq_not_add, getLsbD_add]
+  rw [sub_eq_add_neg, BitVec.neg_eq_not_add, getLsbD_add]
   omega
 
 theorem getMsbD_sub {i : Nat} {i_lt : i < w} {x y : BitVec w} :
     (x - y).getMsbD i =
       (x.getMsbD i ^^ ((~~~y + 1).getMsbD i ^^ carry (w - 1 - i) x (~~~y + 1) false)) := by
-  rw [sub_toAdd, neg_eq_not_add, getMsbD_add]
+  rw [sub_eq_add_neg, neg_eq_not_add, getMsbD_add]
   · rfl
   · omega
 
@@ -360,7 +360,7 @@ theorem getElem_sub {i : Nat} {x y : BitVec w} (h : i < w) :
 theorem msb_sub {x y: BitVec w} :
     (x - y).msb
       = (x.msb ^^ ((~~~y + 1#w).msb ^^ carry (w - 1 - 0) x (~~~y + 1#w) false)) := by
-  simp [sub_toAdd, BitVec.neg_eq_not_add, msb_add]
+  simp [sub_eq_add_neg, BitVec.neg_eq_not_add, msb_add]
 
 /-! ### Negation -/
 
@@ -375,17 +375,17 @@ theorem bit_not_add_self (x : BitVec w) :
   intro i; simp only [adcb, Fin.is_lt, getLsbD_eq_getElem, atLeastTwo_false_right, bne_false,
     ofNat_eq_ofNat, Fin.getElem_fin, Prod.mk.injEq, and_eq_false_imp]
   rw [iunfoldr_replace_snd (fun _ => ()) (((iunfoldr (fun i c => (c, !(x[i.val])))) ()).snd)]
-  <;> simp [bit_not_testBit, negOne_eq_allOnes, getElem_allOnes]
+  <;> simp [bit_not_testBit, neg_one_eq_allOnes, getElem_allOnes]
 
 theorem bit_not_eq_not (x : BitVec w) :
   ((iunfoldr (fun i c => (c, !(x[i])))) ()).snd = ~~~ x := by
-  simp [←allOnes_sub_eq_not, BitVec.eq_sub_iff_add_eq.mpr (bit_not_add_self x), ←negOne_eq_allOnes]
+  simp [←allOnes_sub_eq_not, BitVec.eq_sub_iff_add_eq.mpr (bit_not_add_self x), ←neg_one_eq_allOnes]
 
 theorem bit_neg_eq_neg (x : BitVec w) : -x = (adc (((iunfoldr (fun (i : Fin w) c => (c, !(x[i.val])))) ()).snd) (BitVec.ofNat w 1) false).snd:= by
   simp only [← add_eq_adc]
   rw [iunfoldr_replace_snd ((fun _ => ())) (((iunfoldr (fun (i : Fin w) c => (c, !(x[i.val])))) ()).snd) _ rfl]
-  · rw [BitVec.eq_sub_iff_add_eq.mpr (bit_not_add_self x), sub_toAdd, BitVec.add_comm _ (-x)]
-    simp [← sub_toAdd, BitVec.sub_add_cancel]
+  · rw [BitVec.eq_sub_iff_add_eq.mpr (bit_not_add_self x), sub_eq_add_neg, BitVec.add_comm _ (-x)]
+    simp [← sub_eq_add_neg, BitVec.sub_add_cancel]
   · simp [bit_not_testBit x _]
 
 /--
@@ -420,7 +420,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
@@ -1664,7 +1664,7 @@ theorem intMin_sdiv_neg_one : (intMin w).sdiv (-1#w) = intMin w := by
   refine (Nat.eq_zero_or_pos w).elim (by rintro rfl; exact Subsingleton.elim _ _) (fun hw => ?_)
   apply BitVec.eq_of_toNat_eq
   rw [sdiv]
-  simp [msb_intMin, hw, negOne_eq_allOnes, msb_allOnes]
+  simp [msb_intMin, hw, neg_one_eq_allOnes, msb_allOnes]
   have : 2 ≤ 2 ^ w := Nat.pow_one 2 ▸ (Nat.pow_le_pow_iff_right (by omega)).2 (by omega)
   rw [Nat.sub_sub_self (by omega), Nat.mod_eq_of_lt, Nat.div_one]
   omega
@@ -1674,7 +1674,7 @@ theorem toInt_sdiv (a b : BitVec w) : (a.sdiv b).toInt = (a.toInt.tdiv b.toInt).
   · rcases h with ⟨rfl, rfl⟩
     rw [BitVec.intMin_sdiv_neg_one]
     refine (Nat.eq_zero_or_pos w).elim (by rintro rfl; simp [toInt_of_zero_length]) (fun hw => ?_)
-    rw [toInt_intMin_of_pos hw, negOne_eq_allOnes, toInt_allOnes, if_pos hw, Int.tdiv_neg,
+    rw [toInt_intMin_of_pos hw, neg_one_eq_allOnes, toInt_allOnes, if_pos hw, Int.tdiv_neg,
       Int.tdiv_one, Int.neg_neg, Int.bmod_eq_neg (Int.pow_nonneg (by omega))]
     conv => lhs; rw [(by omega: w = (w - 1) + 1)]
     simp [Nat.pow_succ, Int.natCast_pow, Int.mul_comm]
@@ -1740,7 +1740,7 @@ theorem not_add_one {x : BitVec w} : ~~~ (x + 1#w) = ~~~ x - 1#w := by
 
 theorem not_add_eq_not_neg {x y : BitVec w} : ~~~ (x + y) = ~~~ x - y := by
   rw [not_eq_neg_add, not_eq_neg_add, neg_add]
-  simp only [sub_toAdd]
+  simp only [sub_eq_add_neg]
   rw [BitVec.add_assoc, @BitVec.add_comm _ (-y), ← BitVec.add_assoc]
 
 theorem not_sub_one_eq_not_add_one {x : BitVec w} : ~~~ (x - 1#w) = ~~~ x + 1#w := by
@@ -1748,7 +1748,7 @@ theorem not_sub_one_eq_not_add_one {x : BitVec w} : ~~~ (x - 1#w) = ~~~ x + 1#w
     BitVec.add_sub_cancel, BitVec.sub_add_cancel]
 
 theorem not_sub_eq_not_add {x y : BitVec w} : ~~~ (x - y) = ~~~ x + y := by
-  rw [BitVec.sub_toAdd, not_add_eq_not_neg, sub_neg]
+  rw [BitVec.sub_eq_add_neg, not_add_eq_not_neg, sub_neg]
 
 /-- The value of `(carry i x y false)` can be computed by truncating `x` and `y`
 to `len` bits where `len ≥ i`. -/
@@ -1785,7 +1785,7 @@ theorem append_add_append_eq_append {v w : Nat} {x : BitVec v} {y : BitVec w} :
 
 /-- Heuristically, `y <<< x` is much larger than `x`,
 and hence low bits of `y <<< x`. Thus, `x + (y <<< x) = x ||| (y <<< x).` -/
-theorem add_shifLeft_eq_or_shiftLeft {x y : BitVec w} :
+theorem add_shiftLeft_eq_or_shiftLeft {x y : BitVec w} :
     x + (y <<< x) =  x ||| (y <<< x) := by
   rw [add_eq_or_of_and_eq_zero]
   ext i hi
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 5e99971830..9a30ef4877 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/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
+@[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 getLsbD_of_ge (since := "2025-04-04")]
+abbrev getLsbD_ge := @getLsbD_of_ge
+
+set_option linter.missingDocs false in
+@[deprecated getMsbD_of_ge (since := "2025-04-04")]
+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]
@@ -138,7 +146,7 @@ theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i := rfl
 
 theorem two_pow_le_toNat_of_getElem_eq_true {i : Nat} {x : BitVec w}
     (hi : i < w) (hx : x[i] = true) : 2^i ≤ x.toNat := by
-  apply Nat.testBit_implies_ge
+  apply Nat.ge_two_pow_of_testBit
   rw [← getElem_eq_testBit_toNat x i hi]
   exact hx
 
@@ -161,16 +169,22 @@ 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
+@[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 getElem?_of_ge (since := "2025-04-04")] abbrev getLsb?_ge := @getElem?_of_ge
+
+set_option linter.missingDocs false in
+@[deprecated getMsb?_of_ge (since := "2025-04-04")] 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
@@ -181,17 +195,29 @@ theorem lt_of_getMsb?_eq_some (x : BitVec w) (i : Nat) : getMsb? x i = some b 
   else
     simp [Nat.ge_of_not_lt h]
 
-theorem lt_of_getLsb?_isSome (x : BitVec w) (i : Nat) : x[i]?.isSome → i < w := by
+theorem lt_of_isSome_getElem? (x : BitVec w) (i : Nat) : x[i]?.isSome → i < w := by
   cases h : x[i]? with
   | none => simp
   | some => by_cases i < w <;> simp_all
 
-theorem lt_of_getMsb?_isSome (x : BitVec w) (i : Nat) : (getMsb? x i).isSome → i < w := by
+theorem lt_of_isSome_getMsb? (x : BitVec w) (i : Nat) : (getMsb? x i).isSome → i < w := by
   if h : i < w then
     simp [h]
   else
     simp [Nat.ge_of_not_lt h]
 
+set_option linter.missingDocs false in
+@[deprecated lt_of_getElem?_eq_some (since := "2025-04-04")]
+abbrev lt_of_getLsb?_eq_some := @lt_of_getElem?_eq_some
+
+set_option linter.missingDocs false in
+@[deprecated lt_of_isSome_getElem? (since := "2025-04-04")]
+abbrev lt_of_getLsb?_isSome := @lt_of_isSome_getElem?
+
+set_option linter.missingDocs false in
+@[deprecated lt_of_isSome_getMsb? (since := "2025-04-04")]
+abbrev lt_of_getMsb?_isSome := @lt_of_isSome_getMsb?
+
 theorem getMsbD_eq_getMsb?_getD (x : BitVec w) (i : Nat) :
     x.getMsbD i = (x.getMsb? i).getD false := by
   rw [getMsbD_eq_getLsbD]
@@ -199,7 +225,7 @@ theorem getMsbD_eq_getMsb?_getD (x : BitVec w) (i : Nat) :
   · simp [getMsb?, h]
   · rw [getLsbD_eq_getElem?_getD, getMsb?_eq_getLsb?]
     split <;>
-    · simp only [getLsb?_eq_getElem?, Bool.and_iff_right_iff_imp, decide_eq_true_eq,
+    · simp only [getLsb?_eq_getElem?, Bool.and_eq_right_iff_imp, decide_eq_true_eq,
         Option.getD_none, Bool.and_eq_false_imp]
       intros
       omega
@@ -213,7 +239,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 :=
@@ -380,7 +406,7 @@ theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) :
 @[simp] theorem getLsbD_one : (1#w).getLsbD i = (decide (0 < w) && decide (i = 0)) := by
   simp only [getLsbD, toNat_ofNat, Nat.testBit_mod_two_pow]
   by_cases h : i = 0
-    <;> simp [h, Nat.testBit_to_div_mod, Nat.div_eq_of_lt]
+    <;> simp [h, Nat.testBit_eq_decide_div_mod_eq, Nat.div_eq_of_lt]
 
 @[simp] theorem getElem_one (h : i < w) : (1#w)[i] = decide (i = 0) := by
   simp [← getLsbD_eq_getElem, getLsbD_one, h, show 0 < w by omega]
@@ -501,7 +527,7 @@ theorem msb_eq_getLsbD_last (x : BitVec w) :
     x.getLsbD (w-1) = decide (2 ^ (w-1) ≤ x.toNat) := by
   rcases w with rfl | w
   · simp [toNat_of_zero_length]
-  · simp only [getLsbD, Nat.testBit_to_div_mod, Nat.succ_sub_succ_eq_sub, Nat.sub_zero]
+  · simp only [getLsbD, Nat.testBit_eq_decide_div_mod_eq, Nat.succ_sub_succ_eq_sub, Nat.sub_zero]
     rcases (Nat.lt_or_ge (BitVec.toNat x) (2 ^ w)) with h | h
     · simp [Nat.div_eq_of_lt h, h]
     · simp only [h]
@@ -908,8 +934,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) :
@@ -948,7 +974,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) :
@@ -990,7 +1016,7 @@ theorem setWidth_ofNat_one_eq_ofNat_one_of_lt {v w : Nat} (hv : 0 < v) :
     (BitVec.ofNat v 1).setWidth w = BitVec.ofNat w 1 := by
   ext i h
   simp only [getElem_setWidth, h, decide_true, getLsbD_ofNat, Bool.true_and,
-    Bool.and_iff_right_iff_imp, decide_eq_true_eq]
+    Bool.and_eq_right_iff_imp, decide_eq_true_eq]
   have hv := (@Nat.testBit_one_eq_true_iff_self_eq_zero i)
   by_cases h : Nat.testBit 1 i = true <;> simp_all
 
@@ -1021,7 +1047,7 @@ and the second `setWidth` is a non-trivial extension.
 
 @[simp] theorem msb_setWidth'_of_lt {m n : Nat} (p : m < n) {x : BitVec m} :
     (setWidth' (by omega : m ≤ n) x).msb = false := by
-  have h : x.getLsbD (n - 1) = false := getLsbD_ge _ _ (by omega)
+  have h : x.getLsbD (n - 1) = false := getLsbD_of_ge _ _ (by omega)
   simp [msb_setWidth', -setWidth'_eq, h]
 
 @[simp] theorem toInt_setWidth'_of_lt {m n : Nat} (p : m < n) {x : BitVec m} :
@@ -1693,8 +1719,8 @@ theorem not_eq_comm {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y := by
     rw [h]
     simp
 
-theorem getMsb_not {x : BitVec w} :
-    (~~~x).getMsbD i = (decide (i < w) && !(x.getMsbD i)) := by simp
+set_option linter.missingDocs false in
+@[deprecated getMsbD_not (since := "2025-04-04")] abbrev getMsb_not := @getMsbD_not
 
 @[simp] theorem msb_not {x : BitVec w} : (~~~x).msb = (decide (0 < w) && !x.msb) := by
   simp [BitVec.msb]
@@ -1836,7 +1862,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} :
@@ -1864,7 +1890,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
@@ -2036,7 +2062,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,
@@ -2058,7 +2084,7 @@ theorem msb_ushiftRight {x : BitVec w} {n : Nat} :
     (x >>> y).setWidth i = x.setWidth i >>> y := by
   refine eq_of_getElem_eq (fun j hj => ?_)
   simp only [getElem_setWidth, getLsbD_ushiftRight, getElem_ushiftRight, getLsbD_setWidth,
-    Bool.iff_and_self, decide_eq_true_eq]
+    Bool.eq_and_self, decide_eq_true_eq]
   intro ha
   have := lt_of_getLsbD ha
   omega
@@ -2125,9 +2151,9 @@ 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,
+    · simp only [hi, decide_false, Bool.not_false, Bool.true_and, Bool.eq_and_self,
         decide_eq_true_eq]
       intros hlsb
       apply BitVec.lt_of_getLsbD hlsb
@@ -2135,7 +2161,7 @@ theorem getLsbD_sshiftRight (x : BitVec w) (s i : Nat) :
     · simp [hi]
     · simp only [sshiftRight_eq_of_msb_true hmsb, getLsbD_not, getLsbD_ushiftRight, Bool.not_and,
         Bool.not_not, hi, decide_false, Bool.not_false, Bool.if_true_right, Bool.true_and,
-        Bool.and_iff_right_iff_imp, Bool.or_eq_true, Bool.not_eq_true', decide_eq_false_iff_not,
+        Bool.and_eq_right_iff_imp, Bool.or_eq_true, Bool.not_eq_true', decide_eq_false_iff_not,
         Nat.not_lt, decide_eq_true_eq]
       omega
 
@@ -2478,7 +2504,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.
@@ -2626,7 +2652,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
@@ -2741,7 +2767,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`.
@@ -2754,7 +2780,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
@@ -2764,7 +2790,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
@@ -2772,7 +2798,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
@@ -2816,7 +2842,7 @@ theorem signExtend_eq_append_extractLsb' {w v : Nat} {x : BitVec w} :
   cases hx : x.msb
   · simp only [hx, signExtend_eq_setWidth_of_msb_false, getElem_setWidth, Bool.false_eq_true,
       ↓reduceIte, getElem_append, getElem_extractLsb', Nat.zero_add, getElem_zero, dite_eq_ite,
-      Bool.if_false_right, Bool.iff_and_self, decide_eq_true_eq]
+      Bool.if_false_right, Bool.eq_and_self, decide_eq_true_eq]
     intros hi
     have hw : i < w := lt_of_getLsbD hi
     omega
@@ -2938,7 +2964,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
@@ -2953,7 +2979,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
@@ -3348,11 +3374,14 @@ theorem ofInt_neg {w : Nat} {n : Int} : BitVec.ofInt w (-n) = -BitVec.ofInt w n
     (-x).toFin = Fin.ofNat' (2^n) (2^n - x.toNat) :=
   rfl
 
-theorem sub_toAdd {n} (x y : BitVec n) : x - y = x + - y := by
+theorem sub_eq_add_neg {n} (x y : BitVec n) : x - y = x + - y := by
   apply eq_of_toNat_eq
   simp only [toNat_sub, toNat_add, toNat_neg, Nat.add_mod_mod]
   rw [Nat.add_comm]
 
+set_option linter.missingDocs false in
+@[deprecated sub_eq_add_neg (since := "2025-04-04")] abbrev sub_toAdd := @sub_eq_add_neg
+
 theorem add_left_neg (x : BitVec w) : -x + x = 0#w := by
   apply toInt_inj.mp
   simp [toInt_neg, Int.add_left_neg]
@@ -3361,7 +3390,7 @@ theorem add_right_neg (x : BitVec w) : x + -x = 0#w := by
   rw [BitVec.add_comm]
   exact add_left_neg x
 
-@[simp] theorem neg_zero (n:Nat) : -BitVec.ofNat n 0 = BitVec.ofNat n 0 := by apply eq_of_toNat_eq ; simp
+@[simp] theorem neg_zero (n : Nat) : -BitVec.ofNat n 0 = BitVec.ofNat n 0 := by apply eq_of_toNat_eq ; simp
 
 theorem add_sub_cancel (x y : BitVec w) : x + y - y = x := by
   apply eq_of_toNat_eq
@@ -3370,8 +3399,8 @@ theorem add_sub_cancel (x y : BitVec w) : x + y - y = x := by
       Nat.add_sub_cancel_left, Nat.add_mod_right, toNat_mod_cancel]
 
 theorem sub_add_cancel (x y : BitVec w) : x - y + y = x := by
-  rw [sub_toAdd, BitVec.add_assoc, BitVec.add_comm _ y,
-      ← BitVec.add_assoc, ← sub_toAdd, add_sub_cancel]
+  rw [sub_eq_add_neg, BitVec.add_assoc, BitVec.add_comm _ y,
+      ← BitVec.add_assoc, ← sub_eq_add_neg, add_sub_cancel]
 
 theorem eq_sub_iff_add_eq {x y z : BitVec w} : x = z - y ↔ x + y = z := by
   apply Iff.intro <;> intro h
@@ -3383,7 +3412,7 @@ theorem sub_eq_iff_eq_add {x y z : BitVec w} : x - y = z ↔ x = z + y := by
   · simp [← h, sub_add_cancel]
   · simp [h, add_sub_cancel]
 
-theorem negOne_eq_allOnes : -1#w = allOnes w := by
+theorem neg_one_eq_allOnes : -1#w = allOnes w := by
   apply eq_of_toNat_eq
   if g : w = 0 then
     simp [g]
@@ -3392,6 +3421,10 @@ theorem negOne_eq_allOnes : -1#w = allOnes w := by
     have r : (2^w - 1) < 2^w := by omega
     simp [Nat.mod_eq_of_lt q, Nat.mod_eq_of_lt r]
 
+set_option linter.missingDocs false in
+@[deprecated neg_one_eq_allOnes (since := "2025-04-04")]
+abbrev negOne_eq_allOnes := @neg_one_eq_allOnes
+
 theorem neg_eq_not_add (x : BitVec w) : -x = ~~~x + 1#w := by
   apply eq_of_toNat_eq
   simp only [toNat_neg, ofNat_eq_ofNat, toNat_add, toNat_not, toNat_ofNat, Nat.add_mod_mod]
@@ -3463,7 +3496,7 @@ theorem sub_neg {x y : BitVec w} : x - - y = x + y := by
   simp [toInt_neg, Int.bmod_neg]
 
 theorem neg_sub {x y : BitVec w} : - (x - y) = - x + y := by
- rw [sub_toAdd, neg_add, sub_neg]
+ rw [sub_eq_add_neg, neg_add, sub_neg]
 
 /- ### add/sub injectivity -/
 
@@ -3480,11 +3513,11 @@ protected theorem add_right_inj {x y : BitVec w} (z : BitVec w) : (z + x = z + y
 
 @[simp]
 protected theorem sub_left_inj {x y : BitVec w} (z : BitVec w) : (x - z = y - z) ↔ x = y := by
-  simp [sub_toAdd]
+  simp [sub_eq_add_neg]
 
 @[simp]
 protected theorem sub_right_inj {x y : BitVec w} (z : BitVec w) : (z - x = z - y) ↔ x = y := by
-  simp [sub_toAdd]
+  simp [sub_eq_add_neg]
 
 /-! ### add self -/
 
@@ -3514,19 +3547,19 @@ protected theorem self_eq_add_left {x y : BitVec w} : x = y + x ↔ y = 0#w := b
 theorem getLsbD_fill {w i : Nat} {v : Bool} :
     (fill w v).getLsbD i = (v && decide (i < w)) := by
   by_cases h : v
-  <;> simp [h, BitVec.fill, BitVec.negOne_eq_allOnes]
+  <;> simp [h, BitVec.fill, BitVec.neg_one_eq_allOnes]
 
 @[simp]
 theorem getMsbD_fill {w i : Nat} {v : Bool} :
     (fill w v).getMsbD i = (v && decide (i < w)) := by
   by_cases h : v
-  <;> simp [h, BitVec.fill, BitVec.negOne_eq_allOnes]
+  <;> simp [h, BitVec.fill, BitVec.neg_one_eq_allOnes]
 
 @[simp]
 theorem getElem_fill {w i : Nat} {v : Bool} (h : i < w) :
     (fill w v)[i] = v := by
   by_cases h : v
-  <;> simp [h, BitVec.fill, BitVec.negOne_eq_allOnes]
+  <;> simp [h, BitVec.fill, BitVec.neg_one_eq_allOnes]
 
 @[simp]
 theorem msb_fill {w : Nat} {v : Bool} :
@@ -3639,7 +3672,7 @@ theorem mul_sub {x y z : BitVec w} :
 
 theorem neg_add_mul_eq_mul_not {x y : BitVec w} :
     - (x + x * y) = x * ~~~ y := by
-  rw [neg_add, sub_toAdd, ← BitVec.mul_neg, neg_eq_not_add y, mul_add,
+  rw [neg_add, sub_eq_add_neg, ← BitVec.mul_neg, neg_eq_not_add y, mul_add,
     BitVec.mul_one, BitVec.add_comm, BitVec.add_assoc,
     BitVec.add_right_eq_self, add_neg_eq_sub, BitVec.sub_self]
 
@@ -4039,7 +4072,7 @@ theorem smtSDiv_eq (x y : BitVec w) : smtSDiv x y =
 
 @[simp]
 theorem smtSDiv_zero {x : BitVec n} : x.smtSDiv 0#n = if x.slt 0#n then 1#n else (allOnes n) := by
-  rcases hx : x.msb <;> simp [smtSDiv, slt_zero_iff_msb_cond, hx, ← negOne_eq_allOnes]
+  rcases hx : x.msb <;> simp [smtSDiv, slt_zero_iff_msb_cond, hx, ← neg_one_eq_allOnes]
 
 /-! ### srem -/
 
@@ -4125,9 +4158,12 @@ theorem zero_smod {x : BitVec w} : (0#w).smod x = 0#w := by
   rw [List.getElem?_eq_getElem (by omega)]
   simp
 
-@[simp] theorem getLsb_ofBoolListLE : (ofBoolListLE bs).getLsbD i = bs.getD i false := by
+@[simp] theorem getLsbD_ofBoolListLE : (ofBoolListLE bs).getLsbD i = bs.getD i false := by
   induction bs generalizing i <;> cases i <;> simp_all [ofBoolListLE]
 
+set_option linter.missingDocs false in
+@[deprecated getLsbD_ofBoolListLE (since := "2025-04-04")] abbrev getLsb_ofBoolListLE := @getLsbD_ofBoolListLE
+
 @[simp] theorem getMsbD_ofBoolListLE :
     (ofBoolListLE bs).getMsbD i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false) := by
   simp [getMsbD_eq_getLsbD]
@@ -4166,7 +4202,7 @@ 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
@@ -4187,7 +4223,7 @@ x.rotateLeft 2 = (<6 5 | 4 3 2 1 0>).rotateLeft 2 = <3 2 1 0 | 6 5>
 Intuitively, grab the full width (7), then move the marker `|` by `r` to the right `(-2)`
 Then, access the bit at `i` from the right `(+i)`.
  -/
-theorem getLsbD_rotateLeftAux_of_geq {x : BitVec w} {r : Nat} {i : Nat} (hi : i ≥ r) :
+theorem getLsbD_rotateLeftAux_of_ge {x : BitVec w} {r : Nat} {i : Nat} (hi : i ≥ r) :
     (x.rotateLeftAux r).getLsbD i = (decide (i < w) && x.getLsbD (i - r)) := by
   rw [rotateLeftAux, getLsbD_or]
   suffices (x >>> (w - r)).getLsbD i = false by
@@ -4195,9 +4231,17 @@ 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
 
+set_option linter.missingDocs false in
+@[deprecated getLsbD_rotateLeftAux_of_lt (since := "2025-04-04")]
+abbrev getLsbD_rotateLeftAux_of_le := @getLsbD_rotateLeftAux_of_lt
+
+set_option linter.missingDocs false in
+@[deprecated getLsbD_rotateLeftAux_of_ge (since := "2025-04-04")]
+abbrev getLsbD_rotateLeftAux_of_geq := @getLsbD_rotateLeftAux_of_ge
+
 /-- When `r < w`, we give a formula for `(x.rotateLeft r).getLsbD i`. -/
 theorem getLsbD_rotateLeft_of_le {x : BitVec w} {r i : Nat} (hr: r < w) :
     (x.rotateLeft r).getLsbD i =
@@ -4206,8 +4250,8 @@ 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_geq <| Nat.ge_of_not_lt h]
+    · simp [h, getLsbD_rotateLeftAux_of_lt h]
+    · simp [h, getLsbD_rotateLeftAux_of_ge <| Nat.ge_of_not_lt h]
 
 @[simp]
 theorem getLsbD_rotateLeft {x : BitVec w} {r i : Nat}  :
@@ -4318,7 +4362,7 @@ x.rotateRight 2 = (<6 5 4 3 2 | 1 0>).rotateRight 2 = <1 0 | 6 5 4 3 2>
 = <6 5 4 3 2>.getLsbD i
 = <6 5 4 3 2 | 1 0>[i + 2]
 -/
-theorem getLsbD_rotateRightAux_of_le {x : BitVec w} {r : Nat} {i : Nat} (hi : i < w - r) :
+theorem getLsbD_rotateRightAux_of_lt {x : BitVec w} {r : Nat} {i : Nat} (hi : i < w - r) :
     (x.rotateRightAux r).getLsbD i = x.getLsbD (r + i) := by
   rw [rotateRightAux, getLsbD_or, getLsbD_ushiftRight]
   suffices (x <<< (w - r)).getLsbD i = false by
@@ -4340,7 +4384,7 @@ x.rotateRight 2 = (<6 5 4 3 2 | 1 0>).rotateRight 2 = <1 0 | 6 5 4 3 2>
 = <1 0>.getLsbD (i - len(<6 5 4 3 2>)
 = <6 5 4 3 2 | 1 0> (i - len<6 4 4 3 2>)
  -/
-theorem getLsbD_rotateRightAux_of_geq {x : BitVec w} {r : Nat} {i : Nat} (hi : i ≥ w - r) :
+theorem getLsbD_rotateRightAux_of_ge {x : BitVec w} {r : Nat} {i : Nat} (hi : i ≥ w - r) :
     (x.rotateRightAux r).getLsbD i = (decide (i < w) && x.getLsbD (i - (w - r))) := by
   rw [rotateRightAux, getLsbD_or]
   suffices (x >>> r).getLsbD i = false by
@@ -4348,9 +4392,17 @@ 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
 
+set_option linter.missingDocs false in
+@[deprecated getLsbD_rotateRightAux_of_lt (since := "2025-04-04")]
+abbrev getLsbD_rotateRightAux_of_le := @getLsbD_rotateRightAux_of_lt
+
+set_option linter.missingDocs false in
+@[deprecated getLsbD_rotateRightAux_of_ge (since := "2025-04-04")]
+abbrev getLsbD_rotateRightAux_of_geq := @getLsbD_rotateRightAux_of_ge
+
 /-- `rotateRight` equals the bit fiddling definition of `rotateRightAux` when the rotation amount is
 smaller than the bitwidth. -/
 theorem rotateRight_eq_rotateRightAux_of_lt {x : BitVec w} {r : Nat} (hr : r < w) :
@@ -4371,8 +4423,8 @@ theorem getLsbD_rotateRight_of_lt {x : BitVec w} {r i : Nat} (hr: r < w) :
       (decide (i < w) && x.getLsbD (i - (w - r))) := by
   · rw [rotateRight_eq_rotateRightAux_of_lt hr]
     by_cases h : i < w - r
-    · simp [h, getLsbD_rotateRightAux_of_le h]
-    · simp [h, getLsbD_rotateRightAux_of_geq <| Nat.le_of_not_lt h]
+    · simp [h, getLsbD_rotateRightAux_of_lt h]
+    · simp [h, getLsbD_rotateRightAux_of_ge <| Nat.le_of_not_lt h]
 
 @[simp]
 theorem getLsbD_rotateRight {x : BitVec w} {r i : Nat} :
@@ -4503,7 +4555,7 @@ theorem getLsbD_twoPow (i j : Nat) : (twoPow w i).getLsbD j = ((i < w) && (i = j
 theorem msb_twoPow {i w: Nat} :
     (twoPow w i).msb = (decide (i < w) && decide (i = w - 1)) := by
   simp only [BitVec.msb, getMsbD_eq_getLsbD, Nat.sub_zero, getLsbD_twoPow,
-    Bool.and_iff_right_iff_imp, Bool.and_eq_true, decide_eq_true_eq, and_imp]
+    Bool.and_eq_right_iff_imp, Bool.and_eq_true, decide_eq_true_eq, and_imp]
   intros
   omega
 
@@ -4703,7 +4755,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) :
diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean
index fc4bb39bfd..ef76738b2a 100644
--- a/src/Init/Data/Bool.lean
+++ b/src/Init/Data/Bool.lean
@@ -103,15 +103,39 @@ Needed for confluence of term `(a && b) ↔ a` which reduces to `(a && b) = a` v
 `Bool.coe_iff_coe` and `a → b` via `Bool.and_eq_true` and
 `and_iff_left_iff_imp`.
 -/
-@[simp] theorem and_iff_left_iff_imp  : ∀ {a b : Bool}, ((a && b) = a) ↔ (a → b) := by decide
-@[simp] theorem and_iff_right_iff_imp : ∀ {a b : Bool}, ((a && b) = b) ↔ (b → a) := by decide
-@[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 and_eq_left_iff_imp  : ∀ {a b : Bool}, ((a && b) = a) ↔ (a → b) := by decide
+@[simp] theorem and_eq_right_iff_imp : ∀ {a b : Bool}, ((a && b) = b) ↔ (b → a) := by decide
+@[simp] theorem eq_self_and : ∀ {a b : Bool}, (a = (a && b)) ↔ (a → b) := by decide
+@[simp] theorem eq_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 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
+@[deprecated and_eq_left_iff_imp (since := "2025-04-04")]
+abbrev and_iff_left_iff_imp := @and_eq_left_iff_imp
+
+@[deprecated and_eq_right_iff_imp (since := "2025-04-04")]
+abbrev and_iff_right_iff_imp := @and_eq_right_iff_imp
+
+@[deprecated eq_self_and (since := "2025-04-04")]
+abbrev iff_self_and := @eq_self_and
+
+@[deprecated eq_and_self (since := "2025-04-04")]
+abbrev iff_and_self := @eq_and_self
+
+@[simp] theorem not_and_eq_left_iff_and  : ∀ {a b : Bool}, ((!a && b) = a) ↔ !a ∧ !b := by decide
+@[simp] theorem and_not_eq_right_iff_and : ∀ {a b : Bool}, ((a && !b) = b) ↔ !a ∧ !b := by decide
+@[simp] theorem eq_not_self_and : ∀ {a b : Bool}, (a = (!a && b)) ↔ !a ∧ !b := by decide
+@[simp] theorem eq_and_not_self : ∀ {a b : Bool}, (b = (a && !b)) ↔ !a ∧ !b := by decide
+
+@[deprecated not_and_eq_left_iff_and (since := "2025-04-04")]
+abbrev not_and_iff_left_iff_imp := @not_and_eq_left_iff_and
+
+@[deprecated and_not_eq_right_iff_and (since := "2025-04-04")]
+abbrev and_not_iff_right_iff_imp := @and_not_eq_right_iff_and
+
+@[deprecated eq_not_self_and (since := "2025-04-04")]
+abbrev iff_not_self_and := @eq_not_self_and
+
+@[deprecated eq_and_not_self (since := "2025-04-04")]
+abbrev iff_and_not_self := @eq_and_not_self
 
 /-! ### or -/
 
@@ -137,15 +161,39 @@ Needed for confluence of term `(a || b) ↔ a` which reduces to `(a || b) = a` v
 `Bool.coe_iff_coe` and `a → b` via `Bool.or_eq_true` and
 `and_iff_left_iff_imp`.
 -/
-@[simp] theorem or_iff_left_iff_imp  : ∀ {a b : Bool}, ((a || b) = a) ↔ (b → a) := by decide
-@[simp] theorem or_iff_right_iff_imp : ∀ {a b : Bool}, ((a || b) = b) ↔ (a → b) := by decide
-@[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 or_eq_left_iff_imp  : ∀ {a b : Bool}, ((a || b) = a) ↔ (b → a) := by decide
+@[simp] theorem or_eq_right_iff_imp : ∀ {a b : Bool}, ((a || b) = b) ↔ (a → b) := by decide
+@[simp] theorem eq_self_or : ∀ {a b : Bool}, (a = (a || b)) ↔ (b → a) := by decide
+@[simp] theorem eq_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 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
+@[deprecated or_eq_left_iff_imp (since := "2025-04-04")]
+abbrev or_iff_left_iff_imp := @or_eq_left_iff_imp
+
+@[deprecated or_eq_right_iff_imp (since := "2025-04-04")]
+abbrev or_iff_right_iff_imp := @or_eq_right_iff_imp
+
+@[deprecated eq_self_or (since := "2025-04-04")]
+abbrev iff_self_or := @eq_self_or
+
+@[deprecated eq_or_self (since := "2025-04-04")]
+abbrev iff_or_self := @eq_or_self
+
+@[simp] theorem not_or_eq_left_iff_and  : ∀ {a b : Bool}, ((!a || b) = a) ↔ a ∧ b := by decide
+@[simp] theorem or_not_eq_right_iff_and : ∀ {a b : Bool}, ((a || !b) = b) ↔ a ∧ b := by decide
+@[simp] theorem eq_not_self_or : ∀ {a b : Bool}, (a = (!a || b)) ↔ a ∧ b := by decide
+@[simp] theorem eq_or_not_self : ∀ {a b : Bool}, (b = (a || !b)) ↔ a ∧ b := by decide
+
+@[deprecated not_or_eq_left_iff_and (since := "2025-04-04")]
+abbrev not_or_iff_left_iff_imp := @not_or_eq_left_iff_and
+
+@[deprecated or_not_eq_right_iff_and (since := "2025-04-04")]
+abbrev or_not_iff_right_iff_imp := @or_not_eq_right_iff_and
+
+@[deprecated eq_not_self_or (since := "2025-04-04")]
+abbrev iff_not_self_or := @eq_not_self_or
+
+@[deprecated eq_or_not_self (since := "2025-04-04")]
+abbrev iff_or_not_self := @eq_or_not_self
 
 theorem or_comm : ∀ (x y : Bool), (x || y) = (y || x) := by decide
 instance : Std.Commutative (· || ·) := ⟨or_comm⟩
@@ -564,11 +612,16 @@ protected theorem cond_false {α : Sort u} {a b : α} : cond false a b = b := co
 @[simp] theorem cond_false_right : ∀(c t : Bool), cond c t false = ( c && t) := by decide
 
 -- These restore confluence between the above lemmas and `cond_not`.
-@[simp] theorem cond_true_not_same  : ∀ (c b : Bool), cond c (!c) b = (!c && b) := by decide
-@[simp] theorem cond_false_not_same : ∀ (c b : Bool), cond c b (!c) = (!c || b) := by decide
+@[simp] theorem cond_then_not_self  : ∀ (c b : Bool), cond c (!c) b = (!c && b) := by decide
+@[simp] theorem cond_else_not_self : ∀ (c b : Bool), cond c b (!c) = (!c || b) := by decide
 
-@[simp] theorem cond_true_same  : ∀(c b : Bool), cond c c b = (c || b) := by decide
-@[simp] theorem cond_false_same : ∀(c b : Bool), cond c b c = (c && b) := by decide
+@[simp] theorem cond_then_self  : ∀ (c b : Bool), cond c c b = (c || b) := by decide
+@[simp] theorem cond_else_self : ∀ (c b : Bool), cond c b c = (c && b) := by decide
+
+@[deprecated cond_then_not_self (since := "2025-04-04")] abbrev cond_true_not_same := @cond_then_not_self
+@[deprecated cond_else_not_self (since := "2025-04-04")] abbrev cond_false_not_same := @cond_else_not_self
+@[deprecated cond_then_self (since := "2025-04-04")] abbrev cond_true_same := @cond_then_self
+@[deprecated cond_else_self (since := "2025-04-04")] abbrev cond_false_same := @cond_else_self
 
 theorem cond_pos {b : Bool} {a a' : α} (h : b = true) : (bif b then a else a') = a := by
   rw [h, cond_true]
diff --git a/src/Init/Data/Int/DivMod/Lemmas.lean b/src/Init/Data/Int/DivMod/Lemmas.lean
index 576e9c7246..c62432f365 100644
--- a/src/Init/Data/Int/DivMod/Lemmas.lean
+++ b/src/Init/Data/Int/DivMod/Lemmas.lean
@@ -2307,7 +2307,7 @@ theorem bmod_le {x : Int} {m : Nat} (h : 0 < m) : bmod x m ≤ (m - 1) / 2 := by
       · trivial
 
 -- This could be strengthed by changing to `w : x ≠ -1` if needed.
-theorem bmod_natAbs_plus_one (x : Int) (w : 1 < x.natAbs) : bmod x (x.natAbs + 1) = - x.sign := by
+theorem bmod_natAbs_add_one (x : Int) (w : 1 < x.natAbs) : bmod x (x.natAbs + 1) = - x.sign := by
   have t₁ : ∀ (x : Nat), x % (x + 2) = x :=
     fun x => Nat.mod_eq_of_lt (Nat.lt_succ_of_lt (Nat.lt.base x))
   have t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x := fun x h => by
@@ -2349,6 +2349,9 @@ theorem bmod_natAbs_plus_one (x : Int) (w : 1 < x.natAbs) : bmod x (x.natAbs + 1
     · exact ofNat_nonneg x
     · exact succ_ofNat_pos (x + 1)
 
+@[deprecated bmod_natAbs_add_one (since := "2025-04-04")]
+abbrev bmod_natAbs_plus_one := @bmod_natAbs_add_one
+
 @[simp]
 theorem bmod_neg_bmod : bmod (-(bmod x n)) n = bmod (-x) n := by
   apply (bmod_add_cancel_right x).mp
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index 9ed808eab6..cc0ba2716c 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -723,12 +723,18 @@ theorem mem_or_eq_of_mem_set : ∀ {l : List α} {i : Nat} {a b : α}, a ∈ l.s
 
 /-! ### BEq -/
 
-@[simp] theorem beq_nil_iff [BEq α] {l : List α} : (l == []) = l.isEmpty := by
+@[simp] theorem beq_nil_eq [BEq α] {l : List α} : (l == []) = l.isEmpty := by
   cases l <;> rfl
 
-@[simp] theorem nil_beq_iff [BEq α] {l : List α} : ([] == l) = l.isEmpty := by
+@[simp] theorem nil_beq_eq [BEq α] {l : List α} : ([] == l) = l.isEmpty := by
   cases l <;> rfl
 
+@[deprecated beq_nil_eq (since := "2025-04-04")]
+abbrev beq_nil_iff := @beq_nil_eq
+
+@[deprecated nil_beq_eq (since := "2025-04-04")]
+abbrev nil_beq_iff := @nil_beq_eq
+
 @[simp] theorem cons_beq_cons [BEq α] {a b : α} {l₁ l₂ : List α} :
     (a :: l₁ == b :: l₂) = (a == b && l₁ == l₂) := rfl
 
@@ -744,8 +750,8 @@ theorem mem_or_eq_of_mem_set : ∀ {l : List α} {i : Nat} {a b : α}, a ∈ l.s
 theorem length_eq_of_beq [BEq α] {l₁ l₂ : List α} (h : l₁ == l₂) : l₁.length = l₂.length :=
   match l₁, l₂ with
   | [], [] => rfl
-  | [], _ :: _ => by simp [beq_nil_iff] at h
-  | _ :: _, [] => by simp [nil_beq_iff] at h
+  | [], _ :: _ => by simp at h
+  | _ :: _, [] => by simp at h
   | a :: l₁, b :: l₂ => by
     simp at h
     simpa [Nat.add_one_inj] using length_eq_of_beq h.2
@@ -1276,7 +1282,7 @@ theorem length_filter_eq_length_iff {l} : (filter p l).length = l.length ↔ ∀
     · have := Nat.ne_of_lt (Nat.lt_succ.mpr (length_filter_le p l))
       simp_all
 
-@[deprecated length_filter_eq_length_iff (since := "2024-09-05")]
+@[deprecated length_filter_eq_length_iff (since := "2025-04-04")]
 abbrev filter_length_eq_length := @length_filter_eq_length_iff
 
 @[simp] theorem mem_filter : x ∈ filter p as ↔ x ∈ as ∧ p x := by
diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index 81fb24eda4..5350c1e3a2 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -21,9 +21,6 @@ It is primarily intended to support the bitvector library.
 
 namespace Nat
 
-@[local simp]
-private theorem one_div_two : 1/2 = 0 := by trivial
-
 private theorem two_pow_succ_sub_succ_div_two : (2 ^ (n+1) - (x + 1)) / 2 = 2^n - (x/2 + 1) := by
   omega
 
@@ -79,7 +76,7 @@ noncomputable def div2Induction {motive : Nat → Sort u}
     simp only [HAnd.hAnd, AndOp.and, land]
     unfold bitwise
     cases mod_two_eq_zero_or_one x with | _ p =>
-      simp [xz, p, andz, one_div_two, mod_eq_of_lt]
+      simp [xz, p, andz, mod_eq_of_lt]
 
 /-! ### testBit -/
 
@@ -124,7 +121,7 @@ theorem testBit_div_two (x i : Nat) : testBit (x / 2) i = testBit x (i + 1) := b
 theorem testBit_div_two_pow (x i : Nat) : testBit (x / 2 ^ n) i = testBit x (i + n) :=
   testBit_add .. |>.symm
 
-theorem testBit_to_div_mod {x : Nat} : testBit x i = decide (x / 2^i % 2 = 1) := by
+theorem testBit_eq_decide_div_mod_eq {x : Nat} : testBit x i = decide (x / 2^i % 2 = 1) := by
   induction i generalizing x with
   | zero =>
     unfold testBit
@@ -132,12 +129,15 @@ theorem testBit_to_div_mod {x : Nat} : testBit x i = decide (x / 2^i % 2 = 1) :=
   | succ i hyp =>
     simp [hyp, Nat.div_div_eq_div_mul, Nat.pow_succ']
 
+@[deprecated testBit_eq_decide_div_mod_eq (since := "2025-04-04")]
+abbrev testBit_to_div_mod := @testBit_eq_decide_div_mod_eq
+
 theorem toNat_testBit (x i : Nat) :
     (x.testBit i).toNat = x / 2 ^ i % 2 := by
-  rw [Nat.testBit_to_div_mod]
+  rw [testBit_eq_decide_div_mod_eq]
   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
@@ -152,14 +152,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-04-04")]
+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 =>
@@ -178,6 +181,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-04-04")]
+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.
@@ -186,18 +192,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_ge_and_testBit_of_ge_two_pow {x : Nat} (p : x ≥ 2^n) : ∃ 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
@@ -210,25 +216,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
-  simp only [testBit_to_div_mod] at p
+@[deprecated exists_ge_and_testBit_of_ge_two_pow (since := "2025-04-04")]
+abbrev ge_two_pow_implies_high_bit_true := @exists_ge_and_testBit_of_ge_two_pow
+
+theorem ge_two_pow_of_testBit {x : Nat} (p : testBit x i = true) : x ≥ 2^i := by
+  simp only [Nat.testBit_eq_decide_div_mod_eq] 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-04-04")]
+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_ge_and_testBit_of_ge_two_pow x_ge_n
   have test_false := p _ i_ge_n
   simp [test_true] at test_false
 
@@ -242,12 +254,12 @@ private theorem succ_mod_two : succ x % 2 = 1 - x % 2 := by
     cases Nat.mod_two_eq_zero_or_one x with | _ p => simp [p]
 
 private theorem testBit_succ_zero : testBit (x + 1) 0 = !(testBit x 0) := by
-  simp [testBit_to_div_mod, succ_mod_two]
+  simp only [testBit_eq_decide_div_mod_eq, Nat.pow_zero, Nat.div_one, succ_mod_two]
   cases Nat.mod_two_eq_zero_or_one x with | _ p =>
     simp [p]
 
 theorem testBit_two_pow_add_eq (x i : Nat) : testBit (2^i + x) i = !(testBit x i) := by
-  simp [testBit_to_div_mod, add_div_left, Nat.two_pow_pos, succ_mod_two]
+  simp only [testBit_eq_decide_div_mod_eq, add_div_left, Nat.two_pow_pos, succ_mod_two]
   cases mod_two_eq_zero_or_one (x / 2 ^ i) with
   | _ p => simp [p]
 
@@ -267,7 +279,7 @@ theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) :
     testBit (2^i + x) j = testBit x j := by
   have i_def : i = j + (i-j) := (Nat.add_sub_cancel' (Nat.le_of_lt j_lt_i)).symm
   rw [i_def]
-  simp only [testBit_to_div_mod, Nat.pow_add,
+  simp only [testBit_eq_decide_div_mod_eq, Nat.pow_add,
         Nat.add_comm x, Nat.mul_add_div (Nat.two_pow_pos _)]
   match i_sub_j_eq : i - j with
   | 0 =>
@@ -336,9 +348,8 @@ theorem testBit_two_pow_sub_succ (h₂ : x < 2 ^ n) (i : Nat) :
 theorem testBit_bool_to_nat (b : Bool) (i : Nat) :
     testBit (Bool.toNat b) i = (decide (i = 0) && b) := by
   cases b <;> cases i <;>
-  simp [testBit_to_div_mod, Nat.pow_succ, Nat.mul_comm _ 2,
-        ←Nat.div_div_eq_div_mul _ 2, one_div_two,
-        Nat.mod_eq_of_lt]
+  simp [testBit_eq_decide_div_mod_eq, Nat.pow_succ, Nat.mul_comm _ 2,
+        ←Nat.div_div_eq_div_mul _ 2, Nat.mod_eq_of_lt]
 
 /-- `testBit 1 i` is true iff the index `i` equals 0. -/
 theorem testBit_one_eq_true_iff_self_eq_zero {i : Nat} :
@@ -403,7 +414,7 @@ theorem testBit_bitwise (of_false_false : f false false = false) (x y i : Nat) :
       | succ i =>
         have hyp_i := hyp i (Nat.le_refl (i+1))
         cases p : f (decide (x % 2 = 1)) (decide (y % 2 = 1)) <;>
-          simp [p, one_div_two, hyp_i, Nat.mul_add_div]
+          simp [p, hyp_i, Nat.mul_add_div]
 
 /-! ### bitwise -/
 
@@ -686,13 +697,13 @@ theorem testBit_two_pow_mul_add (a : Nat) {b i : Nat} (b_lt : b < 2^i) (j : Nat)
     have i_def : i = j + succ (pred (i-j)) := by
       rw [succ_pred_eq_of_pos] <;> omega
     rw [i_def]
-    simp only [testBit_to_div_mod, Nat.pow_add, Nat.mul_assoc]
+    simp only [testBit_eq_decide_div_mod_eq, Nat.pow_add, Nat.mul_assoc]
     simp only [Nat.mul_add_div (Nat.two_pow_pos _), Nat.mul_add_mod]
     simp [Nat.pow_succ, Nat.mul_comm _ 2, Nat.mul_assoc, Nat.mul_add_mod]
   | inr j_ge =>
     have j_def : j = i + (j-i) := (Nat.add_sub_cancel' j_ge).symm
     simp only [
-        testBit_to_div_mod,
+        testBit_eq_decide_div_mod_eq,
         Nat.not_lt_of_le,
         j_ge,
         ite_false]
diff --git a/src/Init/Data/Nat/Power2.lean b/src/Init/Data/Nat/Power2.lean
index bfdc58961a..c9b9f85839 100644
--- a/src/Init/Data/Nat/Power2.lean
+++ b/src/Init/Data/Nat/Power2.lean
@@ -43,12 +43,15 @@ theorem isPowerOfTwo_one : isPowerOfTwo 1 :=
   ⟨0, by decide⟩
 
 @[deprecated isPowerOfTwo_one (since := "2025-03-18")]
-abbrev one_isPowerOfTwo := @isPowerOfTwo_one
+abbrev one_isPowerOfTwo := isPowerOfTwo_one
 
-theorem mul2_isPowerOfTwo_of_isPowerOfTwo (h : isPowerOfTwo n) : isPowerOfTwo (n * 2) :=
+theorem isPowerOfTwo_mul_two_of_isPowerOfTwo (h : isPowerOfTwo n) : isPowerOfTwo (n * 2) :=
   have ⟨k, h⟩ := h
   ⟨k+1, by simp [h, Nat.pow_succ]⟩
 
+@[deprecated isPowerOfTwo_mul_two_of_isPowerOfTwo (since := "2025-04-04")]
+abbrev mul2_isPowerOfTwo_of_isPowerOfTwo := @isPowerOfTwo_mul_two_of_isPowerOfTwo
+
 theorem pos_of_isPowerOfTwo (h : isPowerOfTwo n) : n > 0 := by
   have ⟨k, h⟩ := h
   rw [h]
@@ -62,7 +65,7 @@ where
   isPowerOfTwo_go (power : Nat) (h₁ : power > 0) (h₂ : power.isPowerOfTwo) : (nextPowerOfTwo.go n power h₁).isPowerOfTwo := by
     unfold nextPowerOfTwo.go
     split
-    . exact isPowerOfTwo_go (power*2) (Nat.mul_pos h₁ (by decide)) (Nat.mul2_isPowerOfTwo_of_isPowerOfTwo h₂)
+    . exact isPowerOfTwo_go (power*2) (Nat.mul_pos h₁ (by decide)) (Nat.isPowerOfTwo_mul_two_of_isPowerOfTwo h₂)
     . assumption
   termination_by n - power
   decreasing_by simp_wf; apply nextPowerOfTwo_dec <;> assumption
diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean
index fbe07b74a8..a7351c3d0b 100644
--- a/src/Init/Data/Option/Lemmas.lean
+++ b/src/Init/Data/Option/Lemmas.lean
@@ -112,17 +112,24 @@ theorem ne_none_iff_exists : o ≠ none ↔ ∃ x, some x = o := by cases o <;>
 theorem ne_none_iff_exists' : o ≠ none ↔ ∃ x, o = some x :=
   ne_none_iff_exists.trans <| exists_congr fun _ => eq_comm
 
-theorem bex_ne_none {p : Option α → Prop} : (∃ x, ∃ (_ : x ≠ none), p x) ↔ ∃ x, p (some x) :=
+theorem exists_ne_none {p : Option α → Prop} : (∃ x, x ≠ none ∧ p x) ↔ ∃ x, p (some x) :=
   ⟨fun ⟨x, hx, hp⟩ => ⟨x.get <| ne_none_iff_isSome.1 hx, by rwa [some_get]⟩,
     fun ⟨x, hx⟩ => ⟨some x, some_ne_none x, hx⟩⟩
 
-theorem ball_ne_none {p : Option α → Prop} : (∀ x (_ : x ≠ none), p x) ↔ ∀ x, p (some x) :=
+@[deprecated exists_ne_none (since := "2025-04-04")]
+theorem bex_ne_none {p : Option α → Prop} : (∃ x, ∃ (_ : x ≠ none), p x) ↔ ∃ x, p (some x) := by
+  simp only [exists_prop, exists_ne_none]
+
+theorem forall_ne_none {p : Option α → Prop} : (∀ x (_ : x ≠ none), p x) ↔ ∀ x, p (some x) :=
   ⟨fun h x => h (some x) (some_ne_none x),
     fun h x hx => by
       have := h <| x.get <| ne_none_iff_isSome.1 hx
       simp [some_get] at this ⊢
       exact this⟩
 
+@[deprecated forall_ne_none (since := "2025-04-04")]
+abbrev ball_ne_none := @forall_ne_none
+
 @[simp] theorem pure_def : pure = @some α := rfl
 
 @[simp] theorem bind_eq_bind : bind = @Option.bind α β := rfl
diff --git a/src/Init/Data/SInt/Bitwise.lean b/src/Init/Data/SInt/Bitwise.lean
index 8f54a11589..63557edf59 100644
--- a/src/Init/Data/SInt/Bitwise.lean
+++ b/src/Init/Data/SInt/Bitwise.lean
@@ -313,19 +313,19 @@ instance : Std.LawfulCommIdentity (α := ISize) (· ||| ·) 0 where
 
 @[simp] theorem Int8.neg_one_or {a : Int8} : -1 ||| a = -1 := by
   rw [← Int8.toBitVec_inj, Int8.toBitVec_or, Int8.toBitVec_neg, Int8.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_or]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_or]
 @[simp] theorem Int16.neg_one_or {a : Int16} : -1 ||| a = -1 := by
   rw [← Int16.toBitVec_inj, Int16.toBitVec_or, Int16.toBitVec_neg, Int16.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_or]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_or]
 @[simp] theorem Int32.neg_one_or {a : Int32} : -1 ||| a = -1 := by
   rw [← Int32.toBitVec_inj, Int32.toBitVec_or, Int32.toBitVec_neg, Int32.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_or]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_or]
 @[simp] theorem Int64.neg_one_or {a : Int64} : -1 ||| a = -1 := by
   rw [← Int64.toBitVec_inj, Int64.toBitVec_or, Int64.toBitVec_neg, Int64.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_or]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_or]
 @[simp] theorem ISize.neg_one_or {a : ISize} : -1 ||| a = -1 := by
   rw [← ISize.toBitVec_inj, ISize.toBitVec_or, ISize.toBitVec_neg, ISize.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_or]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_or]
 
 @[simp] theorem Int8.or_neg_one {a : Int8} : a ||| -1 = -1 := by rw [Int8.or_comm, neg_one_or]
 @[simp] theorem Int16.or_neg_one {a : Int16} : a ||| -1 = -1 := by rw [Int16.or_comm, neg_one_or]
@@ -394,19 +394,19 @@ instance : Std.IdempotentOp (α := ISize) (· &&& ·) := ⟨fun _ => ISize.and_s
 
 @[simp] theorem Int8.neg_one_and {a : Int8} : -1 &&& a = a := by
   rw [← Int8.toBitVec_inj, Int8.toBitVec_and, Int8.toBitVec_neg, Int8.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_and]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_and]
 @[simp] theorem Int16.neg_one_and {a : Int16} : -1 &&& a = a := by
   rw [← Int16.toBitVec_inj, Int16.toBitVec_and, Int16.toBitVec_neg, Int16.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_and]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_and]
 @[simp] theorem Int32.neg_one_and {a : Int32} : -1 &&& a = a := by
   rw [← Int32.toBitVec_inj, Int32.toBitVec_and, Int32.toBitVec_neg, Int32.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_and]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_and]
 @[simp] theorem Int64.neg_one_and {a : Int64} : -1 &&& a = a := by
   rw [← Int64.toBitVec_inj, Int64.toBitVec_and, Int64.toBitVec_neg, Int64.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_and]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_and]
 @[simp] theorem ISize.neg_one_and {a : ISize} : -1 &&& a = a := by
   rw [← ISize.toBitVec_inj, ISize.toBitVec_and, ISize.toBitVec_neg, ISize.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_and]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_and]
 
 @[simp] theorem Int8.and_neg_one {a : Int8} : a &&& -1 = a := by rw [Int8.and_comm, neg_one_and]
 @[simp] theorem Int16.and_neg_one {a : Int16} : a &&& -1 = a := by rw [Int16.and_comm, neg_one_and]
@@ -427,19 +427,19 @@ instance : Std.LawfulCommIdentity (α := ISize) (· &&& ·) (-1) where
 
 @[simp] theorem Int8.and_eq_neg_one_iff {a b : Int8} : a &&& b = -1 ↔ a = -1 ∧ b = -1 := by
   simp only [← Int8.toBitVec_inj, Int8.toBitVec_and, Int8.toBitVec_neg, Int8.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.and_eq_allOnes_iff]
+    BitVec.neg_one_eq_allOnes, BitVec.and_eq_allOnes_iff]
 @[simp] theorem Int16.and_eq_neg_one_iff {a b : Int16} : a &&& b = -1 ↔ a = -1 ∧ b = -1 := by
   simp only [← Int16.toBitVec_inj, Int16.toBitVec_and, Int16.toBitVec_neg, Int16.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.and_eq_allOnes_iff]
+    BitVec.neg_one_eq_allOnes, BitVec.and_eq_allOnes_iff]
 @[simp] theorem Int32.and_eq_neg_one_iff {a b : Int32} : a &&& b = -1 ↔ a = -1 ∧ b = -1 := by
   simp only [← Int32.toBitVec_inj, Int32.toBitVec_and, Int32.toBitVec_neg, Int32.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.and_eq_allOnes_iff]
+    BitVec.neg_one_eq_allOnes, BitVec.and_eq_allOnes_iff]
 @[simp] theorem Int64.and_eq_neg_one_iff {a b : Int64} : a &&& b = -1 ↔ a = -1 ∧ b = -1 := by
   simp only [← Int64.toBitVec_inj, Int64.toBitVec_and, Int64.toBitVec_neg, Int64.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.and_eq_allOnes_iff]
+    BitVec.neg_one_eq_allOnes, BitVec.and_eq_allOnes_iff]
 @[simp] theorem ISize.and_eq_neg_one_iff {a b : ISize} : a &&& b = -1 ↔ a = -1 ∧ b = -1 := by
   simp only [← ISize.toBitVec_inj, ISize.toBitVec_and, ISize.toBitVec_neg, ISize.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.and_eq_allOnes_iff]
+    BitVec.neg_one_eq_allOnes, BitVec.and_eq_allOnes_iff]
 
 protected theorem Int8.xor_assoc (a b c : Int8) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := Int8.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
 protected theorem Int16.xor_assoc (a b c : Int16) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := Int16.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
@@ -485,19 +485,19 @@ instance : Std.Commutative (α := ISize) (· ^^^ ·) := ⟨ISize.xor_comm⟩
 
 @[simp] theorem Int8.neg_one_xor {a : Int8} : -1 ^^^ a = ~~~a := by
   rw [← Int8.toBitVec_inj, Int8.toBitVec_xor, Int8.toBitVec_neg, Int8.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_xor, Int8.toBitVec_not]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_xor, Int8.toBitVec_not]
 @[simp] theorem Int16.neg_one_xor {a : Int16} : -1 ^^^ a = ~~~a := by
   rw [← Int16.toBitVec_inj, Int16.toBitVec_xor, Int16.toBitVec_neg, Int16.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_xor, Int16.toBitVec_not]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_xor, Int16.toBitVec_not]
 @[simp] theorem Int32.neg_one_xor {a : Int32} : -1 ^^^ a = ~~~a := by
   rw [← Int32.toBitVec_inj, Int32.toBitVec_xor, Int32.toBitVec_neg, Int32.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_xor, Int32.toBitVec_not]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_xor, Int32.toBitVec_not]
 @[simp] theorem Int64.neg_one_xor {a : Int64} : -1 ^^^ a = ~~~a := by
   rw [← Int64.toBitVec_inj, Int64.toBitVec_xor, Int64.toBitVec_neg, Int64.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_xor, Int64.toBitVec_not]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_xor, Int64.toBitVec_not]
 @[simp] theorem ISize.neg_one_xor {a : ISize} : -1 ^^^ a = ~~~a := by
   rw [← ISize.toBitVec_inj, ISize.toBitVec_xor, ISize.toBitVec_neg, ISize.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_xor, ISize.toBitVec_not]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_xor, ISize.toBitVec_not]
 
 @[simp] theorem Int8.xor_neg_one {a : Int8} : a ^^^ -1 = ~~~a := by rw [Int8.xor_comm, neg_one_xor]
 @[simp] theorem Int16.xor_neg_one {a : Int16} : a ^^^ -1 = ~~~a := by rw [Int16.xor_comm, neg_one_xor]
@@ -582,19 +582,19 @@ instance : Std.LawfulCommIdentity (α := ISize) (· ^^^ ·) 0 where
 
 @[simp] theorem Int8.or_not_self {a : Int8} : a ||| ~~~a = -1 := by
   rw [← Int8.toBitVec_inj, Int8.toBitVec_or, Int8.toBitVec_not, BitVec.or_not_self,
-    Int8.toBitVec_neg, Int8.toBitVec_one, BitVec.negOne_eq_allOnes]
+    Int8.toBitVec_neg, Int8.toBitVec_one, BitVec.neg_one_eq_allOnes]
 @[simp] theorem Int16.or_not_self {a : Int16} : a ||| ~~~a = -1 := by
   rw [← Int16.toBitVec_inj, Int16.toBitVec_or, Int16.toBitVec_not, BitVec.or_not_self,
-    Int16.toBitVec_neg, Int16.toBitVec_one, BitVec.negOne_eq_allOnes]
+    Int16.toBitVec_neg, Int16.toBitVec_one, BitVec.neg_one_eq_allOnes]
 @[simp] theorem Int32.or_not_self {a : Int32} : a ||| ~~~a = -1 := by
   rw [← Int32.toBitVec_inj, Int32.toBitVec_or, Int32.toBitVec_not, BitVec.or_not_self,
-    Int32.toBitVec_neg, Int32.toBitVec_one, BitVec.negOne_eq_allOnes]
+    Int32.toBitVec_neg, Int32.toBitVec_one, BitVec.neg_one_eq_allOnes]
 @[simp] theorem Int64.or_not_self {a : Int64} : a ||| ~~~a = -1 := by
   rw [← Int64.toBitVec_inj, Int64.toBitVec_or, Int64.toBitVec_not, BitVec.or_not_self,
-    Int64.toBitVec_neg, Int64.toBitVec_one, BitVec.negOne_eq_allOnes]
+    Int64.toBitVec_neg, Int64.toBitVec_one, BitVec.neg_one_eq_allOnes]
 @[simp] theorem ISize.or_not_self {a : ISize} : a ||| ~~~a = -1 := by
   rw [← ISize.toBitVec_inj, ISize.toBitVec_or, ISize.toBitVec_not, BitVec.or_not_self,
-    ISize.toBitVec_neg, ISize.toBitVec_one, BitVec.negOne_eq_allOnes]
+    ISize.toBitVec_neg, ISize.toBitVec_one, BitVec.neg_one_eq_allOnes]
 
 @[simp] theorem Int8.not_or_self {a : Int8} : ~~~a ||| a = -1 := by simp [Int8.or_comm]
 @[simp] theorem Int16.not_or_self {a : Int16} : ~~~a ||| a = -1 := by simp [Int16.or_comm]
diff --git a/src/Init/Data/SInt/Lemmas.lean b/src/Init/Data/SInt/Lemmas.lean
index 62443b7b92..b639ec00a2 100644
--- a/src/Init/Data/SInt/Lemmas.lean
+++ b/src/Init/Data/SInt/Lemmas.lean
@@ -1812,11 +1812,11 @@ theorem ISize.toInt64_div_of_ne_right (a b : ISize) (hb : b ≠ -1) : (a / b).to
 @[simp] theorem Int64.toISize_mul (a b : Int64) : (a * b).toISize = a.toISize * b.toISize :=
   ISize.toBitVec_inj.1 (by simp [BitVec.signExtend_eq_setWidth_of_le, BitVec.setWidth_mul])
 
-protected theorem Int8.sub_eq_add_neg (a b : Int8) : a - b = a + -b := Int8.toBitVec.inj (by simp [BitVec.sub_toAdd])
-protected theorem Int16.sub_eq_add_neg (a b : Int16) : a - b = a + -b := Int16.toBitVec.inj (by simp [BitVec.sub_toAdd])
-protected theorem Int32.sub_eq_add_neg (a b : Int32) : a - b = a + -b := Int32.toBitVec.inj (by simp [BitVec.sub_toAdd])
-protected theorem Int64.sub_eq_add_neg (a b : Int64) : a - b = a + -b := Int64.toBitVec.inj (by simp [BitVec.sub_toAdd])
-protected theorem ISize.sub_eq_add_neg (a b : ISize) : a - b = a + -b := ISize.toBitVec.inj (by simp [BitVec.sub_toAdd])
+protected theorem Int8.sub_eq_add_neg (a b : Int8) : a - b = a + -b := Int8.toBitVec.inj (by simp [BitVec.sub_eq_add_neg])
+protected theorem Int16.sub_eq_add_neg (a b : Int16) : a - b = a + -b := Int16.toBitVec.inj (by simp [BitVec.sub_eq_add_neg])
+protected theorem Int32.sub_eq_add_neg (a b : Int32) : a - b = a + -b := Int32.toBitVec.inj (by simp [BitVec.sub_eq_add_neg])
+protected theorem Int64.sub_eq_add_neg (a b : Int64) : a - b = a + -b := Int64.toBitVec.inj (by simp [BitVec.sub_eq_add_neg])
+protected theorem ISize.sub_eq_add_neg (a b : ISize) : a - b = a + -b := ISize.toBitVec.inj (by simp [BitVec.sub_eq_add_neg])
 
 @[simp] theorem Int8.toInt_sub (a b : Int8) : (a - b).toInt = (a.toInt - b.toInt).bmod (2 ^ 8) := by
   simp [Int8.sub_eq_add_neg, Int.sub_eq_add_neg]
diff --git a/src/Init/Data/UInt/Bitwise.lean b/src/Init/Data/UInt/Bitwise.lean
index 6b9ebdc408..d287d3e68c 100644
--- a/src/Init/Data/UInt/Bitwise.lean
+++ b/src/Init/Data/UInt/Bitwise.lean
@@ -768,19 +768,19 @@ instance : Std.LawfulCommIdentity (α := USize) (· ||| ·) 0 where
 
 @[simp] theorem UInt8.neg_one_or {a : UInt8} : -1 ||| a = -1 := by
   rw [← UInt8.toBitVec_inj, UInt8.toBitVec_or, UInt8.toBitVec_neg, UInt8.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_or]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_or]
 @[simp] theorem UInt16.neg_one_or {a : UInt16} : -1 ||| a = -1 := by
   rw [← UInt16.toBitVec_inj, UInt16.toBitVec_or, UInt16.toBitVec_neg, UInt16.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_or]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_or]
 @[simp] theorem UInt32.neg_one_or {a : UInt32} : -1 ||| a = -1 := by
   rw [← UInt32.toBitVec_inj, UInt32.toBitVec_or, UInt32.toBitVec_neg, UInt32.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_or]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_or]
 @[simp] theorem UInt64.neg_one_or {a : UInt64} : -1 ||| a = -1 := by
   rw [← UInt64.toBitVec_inj, UInt64.toBitVec_or, UInt64.toBitVec_neg, UInt64.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_or]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_or]
 @[simp] theorem USize.neg_one_or {a : USize} : -1 ||| a = -1 := by
   rw [← USize.toBitVec_inj, USize.toBitVec_or, USize.toBitVec_neg, USize.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_or]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_or]
 
 @[simp] theorem UInt8.or_neg_one {a : UInt8} : a ||| -1 = -1 := by rw [UInt8.or_comm, neg_one_or]
 @[simp] theorem UInt16.or_neg_one {a : UInt16} : a ||| -1 = -1 := by rw [UInt16.or_comm, neg_one_or]
@@ -849,19 +849,19 @@ instance : Std.IdempotentOp (α := USize) (· &&& ·) := ⟨fun _ => USize.and_s
 
 @[simp] theorem UInt8.neg_one_and {a : UInt8} : -1 &&& a = a := by
   rw [← UInt8.toBitVec_inj, UInt8.toBitVec_and, UInt8.toBitVec_neg, UInt8.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_and]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_and]
 @[simp] theorem UInt16.neg_one_and {a : UInt16} : -1 &&& a = a := by
   rw [← UInt16.toBitVec_inj, UInt16.toBitVec_and, UInt16.toBitVec_neg, UInt16.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_and]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_and]
 @[simp] theorem UInt32.neg_one_and {a : UInt32} : -1 &&& a = a := by
   rw [← UInt32.toBitVec_inj, UInt32.toBitVec_and, UInt32.toBitVec_neg, UInt32.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_and]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_and]
 @[simp] theorem UInt64.neg_one_and {a : UInt64} : -1 &&& a = a := by
   rw [← UInt64.toBitVec_inj, UInt64.toBitVec_and, UInt64.toBitVec_neg, UInt64.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_and]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_and]
 @[simp] theorem USize.neg_one_and {a : USize} : -1 &&& a = a := by
   rw [← USize.toBitVec_inj, USize.toBitVec_and, USize.toBitVec_neg, USize.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_and]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_and]
 
 @[simp] theorem UInt8.and_neg_one {a : UInt8} : a &&& -1 = a := by rw [UInt8.and_comm, neg_one_and]
 @[simp] theorem UInt16.and_neg_one {a : UInt16} : a &&& -1 = a := by rw [UInt16.and_comm, neg_one_and]
@@ -882,19 +882,19 @@ instance : Std.LawfulCommIdentity (α := USize) (· &&& ·) (-1) where
 
 @[simp] theorem UInt8.and_eq_neg_one_iff {a b : UInt8} : a &&& b = -1 ↔ a = -1 ∧ b = -1 := by
   simp only [← UInt8.toBitVec_inj, UInt8.toBitVec_and, UInt8.toBitVec_neg, UInt8.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.and_eq_allOnes_iff]
+    BitVec.neg_one_eq_allOnes, BitVec.and_eq_allOnes_iff]
 @[simp] theorem UInt16.and_eq_neg_one_iff {a b : UInt16} : a &&& b = -1 ↔ a = -1 ∧ b = -1 := by
   simp only [← UInt16.toBitVec_inj, UInt16.toBitVec_and, UInt16.toBitVec_neg, UInt16.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.and_eq_allOnes_iff]
+    BitVec.neg_one_eq_allOnes, BitVec.and_eq_allOnes_iff]
 @[simp] theorem UInt32.and_eq_neg_one_iff {a b : UInt32} : a &&& b = -1 ↔ a = -1 ∧ b = -1 := by
   simp only [← UInt32.toBitVec_inj, UInt32.toBitVec_and, UInt32.toBitVec_neg, UInt32.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.and_eq_allOnes_iff]
+    BitVec.neg_one_eq_allOnes, BitVec.and_eq_allOnes_iff]
 @[simp] theorem UInt64.and_eq_neg_one_iff {a b : UInt64} : a &&& b = -1 ↔ a = -1 ∧ b = -1 := by
   simp only [← UInt64.toBitVec_inj, UInt64.toBitVec_and, UInt64.toBitVec_neg, UInt64.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.and_eq_allOnes_iff]
+    BitVec.neg_one_eq_allOnes, BitVec.and_eq_allOnes_iff]
 @[simp] theorem USize.and_eq_neg_one_iff {a b : USize} : a &&& b = -1 ↔ a = -1 ∧ b = -1 := by
   simp only [← USize.toBitVec_inj, USize.toBitVec_and, USize.toBitVec_neg, USize.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.and_eq_allOnes_iff]
+    BitVec.neg_one_eq_allOnes, BitVec.and_eq_allOnes_iff]
 
 protected theorem UInt8.xor_assoc (a b c : UInt8) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := UInt8.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
 protected theorem UInt16.xor_assoc (a b c : UInt16) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := UInt16.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
@@ -940,19 +940,19 @@ instance : Std.Commutative (α := USize) (· ^^^ ·) := ⟨USize.xor_comm⟩
 
 @[simp] theorem UInt8.neg_one_xor {a : UInt8} : -1 ^^^ a = ~~~a := by
   rw [← UInt8.toBitVec_inj, UInt8.toBitVec_xor, UInt8.toBitVec_neg, UInt8.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_xor, UInt8.toBitVec_not]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_xor, UInt8.toBitVec_not]
 @[simp] theorem UInt16.neg_one_xor {a : UInt16} : -1 ^^^ a = ~~~a := by
   rw [← UInt16.toBitVec_inj, UInt16.toBitVec_xor, UInt16.toBitVec_neg, UInt16.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_xor, UInt16.toBitVec_not]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_xor, UInt16.toBitVec_not]
 @[simp] theorem UInt32.neg_one_xor {a : UInt32} : -1 ^^^ a = ~~~a := by
   rw [← UInt32.toBitVec_inj, UInt32.toBitVec_xor, UInt32.toBitVec_neg, UInt32.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_xor, UInt32.toBitVec_not]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_xor, UInt32.toBitVec_not]
 @[simp] theorem UInt64.neg_one_xor {a : UInt64} : -1 ^^^ a = ~~~a := by
   rw [← UInt64.toBitVec_inj, UInt64.toBitVec_xor, UInt64.toBitVec_neg, UInt64.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_xor, UInt64.toBitVec_not]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_xor, UInt64.toBitVec_not]
 @[simp] theorem USize.neg_one_xor {a : USize} : -1 ^^^ a = ~~~a := by
   rw [← USize.toBitVec_inj, USize.toBitVec_xor, USize.toBitVec_neg, USize.toBitVec_one,
-    BitVec.negOne_eq_allOnes, BitVec.allOnes_xor, USize.toBitVec_not]
+    BitVec.neg_one_eq_allOnes, BitVec.allOnes_xor, USize.toBitVec_not]
 
 @[simp] theorem UInt8.xor_neg_one {a : UInt8} : a ^^^ -1 = ~~~a := by rw [UInt8.xor_comm, neg_one_xor]
 @[simp] theorem UInt16.xor_neg_one {a : UInt16} : a ^^^ -1 = ~~~a := by rw [UInt16.xor_comm, neg_one_xor]
@@ -1037,19 +1037,19 @@ instance : Std.LawfulCommIdentity (α := USize) (· ^^^ ·) 0 where
 
 @[simp] theorem UInt8.or_not_self {a : UInt8} : a ||| ~~~a = -1 := by
   rw [← UInt8.toBitVec_inj, UInt8.toBitVec_or, UInt8.toBitVec_not, BitVec.or_not_self,
-    UInt8.toBitVec_neg, UInt8.toBitVec_one, BitVec.negOne_eq_allOnes]
+    UInt8.toBitVec_neg, UInt8.toBitVec_one, BitVec.neg_one_eq_allOnes]
 @[simp] theorem UInt16.or_not_self {a : UInt16} : a ||| ~~~a = -1 := by
   rw [← UInt16.toBitVec_inj, UInt16.toBitVec_or, UInt16.toBitVec_not, BitVec.or_not_self,
-    UInt16.toBitVec_neg, UInt16.toBitVec_one, BitVec.negOne_eq_allOnes]
+    UInt16.toBitVec_neg, UInt16.toBitVec_one, BitVec.neg_one_eq_allOnes]
 @[simp] theorem UInt32.or_not_self {a : UInt32} : a ||| ~~~a = -1 := by
   rw [← UInt32.toBitVec_inj, UInt32.toBitVec_or, UInt32.toBitVec_not, BitVec.or_not_self,
-    UInt32.toBitVec_neg, UInt32.toBitVec_one, BitVec.negOne_eq_allOnes]
+    UInt32.toBitVec_neg, UInt32.toBitVec_one, BitVec.neg_one_eq_allOnes]
 @[simp] theorem UInt64.or_not_self {a : UInt64} : a ||| ~~~a = -1 := by
   rw [← UInt64.toBitVec_inj, UInt64.toBitVec_or, UInt64.toBitVec_not, BitVec.or_not_self,
-    UInt64.toBitVec_neg, UInt64.toBitVec_one, BitVec.negOne_eq_allOnes]
+    UInt64.toBitVec_neg, UInt64.toBitVec_one, BitVec.neg_one_eq_allOnes]
 @[simp] theorem USize.or_not_self {a : USize} : a ||| ~~~a = -1 := by
   rw [← USize.toBitVec_inj, USize.toBitVec_or, USize.toBitVec_not, BitVec.or_not_self,
-    USize.toBitVec_neg, USize.toBitVec_one, BitVec.negOne_eq_allOnes]
+    USize.toBitVec_neg, USize.toBitVec_one, BitVec.neg_one_eq_allOnes]
 
 @[simp] theorem UInt8.not_or_self {a : UInt8} : ~~~a ||| a = -1 := by simp [UInt8.or_comm]
 @[simp] theorem UInt16.not_or_self {a : UInt16} : ~~~a ||| a = -1 := by simp [UInt16.or_comm]
diff --git a/src/Init/Data/UInt/Lemmas.lean b/src/Init/Data/UInt/Lemmas.lean
index 546be10fd9..686c7bba70 100644
--- a/src/Init/Data/UInt/Lemmas.lean
+++ b/src/Init/Data/UInt/Lemmas.lean
@@ -1864,11 +1864,11 @@ theorem USize.le_iff_toFin_le {a b : USize} : a ≤ b ↔ a.toFin ≤ b.toFin :=
 @[simp] theorem UInt64.toNat_neg (a : UInt64) : (-a).toNat = (UInt64.size - a.toNat) % UInt64.size := rfl
 @[simp] theorem USize.toNat_neg (a : USize) : (-a).toNat = (USize.size - a.toNat) % USize.size := rfl
 
-protected theorem UInt8.sub_eq_add_neg (a b : UInt8) : a - b = a + (-b) := UInt8.toBitVec_inj.1 (BitVec.sub_toAdd _ _)
-protected theorem UInt16.sub_eq_add_neg (a b : UInt16) : a - b = a + (-b) := UInt16.toBitVec_inj.1 (BitVec.sub_toAdd _ _)
-protected theorem UInt32.sub_eq_add_neg (a b : UInt32) : a - b = a + (-b) := UInt32.toBitVec_inj.1 (BitVec.sub_toAdd _ _)
-protected theorem UInt64.sub_eq_add_neg (a b : UInt64) : a - b = a + (-b) := UInt64.toBitVec_inj.1 (BitVec.sub_toAdd _ _)
-protected theorem USize.sub_eq_add_neg (a b : USize) : a - b = a + (-b) := USize.toBitVec_inj.1 (BitVec.sub_toAdd _ _)
+protected theorem UInt8.sub_eq_add_neg (a b : UInt8) : a - b = a + (-b) := UInt8.toBitVec_inj.1 (BitVec.sub_eq_add_neg _ _)
+protected theorem UInt16.sub_eq_add_neg (a b : UInt16) : a - b = a + (-b) := UInt16.toBitVec_inj.1 (BitVec.sub_eq_add_neg _ _)
+protected theorem UInt32.sub_eq_add_neg (a b : UInt32) : a - b = a + (-b) := UInt32.toBitVec_inj.1 (BitVec.sub_eq_add_neg _ _)
+protected theorem UInt64.sub_eq_add_neg (a b : UInt64) : a - b = a + (-b) := UInt64.toBitVec_inj.1 (BitVec.sub_eq_add_neg _ _)
+protected theorem USize.sub_eq_add_neg (a b : USize) : a - b = a + (-b) := USize.toBitVec_inj.1 (BitVec.sub_eq_add_neg _ _)
 
 protected theorem UInt8.add_neg_eq_sub {a b : UInt8} : a + -b = a - b := UInt8.toBitVec_inj.1 BitVec.add_neg_eq_sub
 protected theorem UInt16.add_neg_eq_sub {a b : UInt16} : a + -b = a - b := UInt16.toBitVec_inj.1 BitVec.add_neg_eq_sub
diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean
index ae0771e734..3171a9aebf 100644
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -515,7 +515,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 = [] := rfl
 
 theorem toList_emptyWithCapacity {cap} :
     (Vector.emptyWithCapacity (α := α) cap).toList = [] := rfl
@@ -660,11 +660,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-04-04")]
+abbrev toList_eq_empty_iff {α n} (xs) := @toList_eq_nil_iff α n xs
+
 @[simp] theorem mem_toList_iff {a : α} {xs : Vector α n} : a ∈ xs.toList ↔ a ∈ xs := by
   simp
 
diff --git a/src/Init/Util.lean b/src/Init/Util.lean
index 5aa4b7bc2f..40f37b01d9 100644
--- a/src/Init/Util.lean
+++ b/src/Init/Util.lean
@@ -94,8 +94,8 @@ def withPtrEq {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () =
 @[inline] def withPtrEqDecEq {α : Type u} (a b : α) (k : Unit → Decidable (a = b)) : Decidable (a = b) :=
   let b := withPtrEq a b (fun _ => toBoolUsing (k ())) (toBoolUsing_eq_true (k ()));
   match h:b with
-  | true  => isTrue (ofBoolUsing_eq_true h)
-  | false => isFalse (ofBoolUsing_eq_false h)
+  | true  => isTrue (of_toBoolUsing_eq_true h)
+  | false => isFalse (of_toBoolUsing_eq_false h)
 
 @[implemented_by withPtrAddrUnsafe]
 def withPtrAddr {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β := k 0
diff --git a/src/Init/WF.lean b/src/Init/WF.lean
index 665d9c09b1..f2c71501eb 100644
--- a/src/Init/WF.lean
+++ b/src/Init/WF.lean
@@ -92,10 +92,13 @@ noncomputable def fixF (x : α) (a : Acc r x) : C x := by
   induction a with
   | intro x₁ _ ih => exact F x₁ ih
 
-theorem fixFEq (x : α) (acx : Acc r x) : fixF F x acx = F x (fun (y : α) (p : r y x) => fixF F y (Acc.inv acx p)) := by
+theorem fixF_eq (x : α) (acx : Acc r x) : fixF F x acx = F x (fun (y : α) (p : r y x) => fixF F y (Acc.inv acx p)) := by
   induction acx with
   | intro x r _ => exact rfl
 
+@[deprecated fixF_eq (since := "2025-04-04")]
+abbrev fixFEq := @fixF_eq
+
 end
 
 variable {α : Sort u} {C : α → Sort v} {r : α → α → Prop}
@@ -114,7 +117,7 @@ noncomputable def fix (hwf : WellFounded r) (F : ∀ x, (∀ y, r y x → C y) 
 -- Well-founded fixpoint satisfies fixpoint equation
 theorem fix_eq (hwf : WellFounded r) (F : ∀ x, (∀ y, r y x → C y) → C x) (x : α) :
     fix hwf F x = F x (fun y _ => fix hwf F y) :=
-  fixFEq F x (apply hwf x)
+  fixF_eq F x (apply hwf x)
 end WellFounded
 
 open WellFounded
diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
index 555993fe2e..8d833ddf84 100644
--- a/src/Std/Data/DHashMap/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Lemmas.lean
@@ -3061,13 +3061,13 @@ set_option linter.missingDocs false in
 @[deprecated equiv_empty_iff_isEmpty (since := "2025-03-11")]
 abbrev equiv_emptyc_iff_isEmpty := @equiv_empty_iff_isEmpty
 
-theorem empty_equivWithCapacity_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} :
+theorem empty_emptyWithCapacity_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} :
     emptyWithCapacity c ~m m ↔ m.isEmpty :=
   Equiv.comm.trans equiv_emptyWithCapacity_iff_isEmpty
 
 @[simp]
 theorem empty_equiv_iff_isEmpty [EquivBEq α] [LawfulHashable α] : ∅ ~m m ↔ m.isEmpty :=
-  empty_equivWithCapacity_iff_isEmpty
+  empty_emptyWithCapacity_iff_isEmpty
 
 set_option linter.missingDocs false in
 @[deprecated empty_equiv_iff_isEmpty (since := "2025-03-11")]
diff --git a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
index 8b58e4e1ca..14f8762c1f 100644
--- a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
@@ -331,7 +331,7 @@ theorem toListModel_eq_append [Ord α] [TransOrd α] (k : α → Ordering) [IsSt
       simp
   · simp
 
-theorem ordered_updateAtKey [Ord α] [TransOrd α] {k : α}
+theorem ordered_updateCell [Ord α] [TransOrd α] {k : α}
     {f : Cell α β (compare k) → Cell α β (compare k)}
     {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) : (l.updateCell k f hlb).impl.Ordered := by
   rw [Ordered, toListModel_updateCell _ hlo]
@@ -361,7 +361,7 @@ theorem ordered_updateAtKey [Ord α] [TransOrd α] {k : α}
 
 open Std.Internal.List
 
-theorem exists_cell_of_updateAtKey [BEq α] [Ord α] [TransOrd α] [LawfulBEqOrd α] (l : Impl α β) (hlb : l.Balanced)
+theorem exists_cell_of_updateCell [BEq α] [Ord α] [TransOrd α] [LawfulBEqOrd α] (l : Impl α β) (hlb : l.Balanced)
     (hlo : l.Ordered) (k : α)
     (f : Cell α β (compare k) → Cell α β (compare k)) : ∃ (l' : List ((a : α) × β a)),
     l.toListModel.Perm ((l.toListModel.find? (compare k ·.1 == .eq)).toList ++ l') ∧
@@ -386,7 +386,7 @@ theorem Ordered.distinctKeys [BEq α] [Ord α] [LawfulBEqOrd α] {l : Impl α β
     simp [← LawfulBEqOrd.not_compare_eq_iff_beq_eq_false, h])⟩
 
 /-- This is the general theorem to show that modification operations are correct. -/
-theorem toListModel_updateAtKey_perm [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+theorem toListModel_updateCell_perm [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
     {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) {k : α}
     {f : Cell α β (compare k) → Cell α β (compare k)}
     {g : List ((a : α) × β a) → List ((a : α) × β a)}
@@ -394,7 +394,7 @@ theorem toListModel_updateAtKey_perm [Ord α] [TransOrd α] [BEq α] [LawfulBEqO
     (hg₁ : ∀ {l l'}, DistinctKeys l → List.Perm l l' → List.Perm (g l) (g l'))
     (hg₂ : ∀ {l l'}, containsKey k l' = false → g (l ++ l') = g l ++ l') :
     List.Perm (l.updateCell k f hlb).impl.toListModel (g l.toListModel) := by
-  obtain ⟨l, h₁, h₂, h₃⟩ := exists_cell_of_updateAtKey l hlb hlo k f
+  obtain ⟨l, h₁, h₂, h₃⟩ := exists_cell_of_updateCell l hlb hlo k f
   refine h₂.trans (List.Perm.trans ?_ (hg₁ hlo.distinctKeys h₁).symm)
   rwa [hfg, hg₂, List.findCell_inner]
 
@@ -814,12 +814,12 @@ theorem ordered_empty [Ord α] : (.empty : Impl α β).Ordered := by
 
 theorem ordered_insertₘ [Ord α] [TransOrd α] {k : α} {v : β k} {l : Impl α β} (hlb : l.Balanced)
     (hlo : l.Ordered) : (l.insertₘ k v hlb).Ordered :=
-  ordered_updateAtKey _ hlo
+  ordered_updateCell _ hlo
 
 theorem toListModel_insertₘ [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k}
     {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) :
     (l.insertₘ k v hlb).toListModel.Perm (insertEntry k v l.toListModel) := by
-  refine toListModel_updateAtKey_perm _ hlo ?_ insertEntry_of_perm
+  refine toListModel_updateCell_perm _ hlo ?_ insertEntry_of_perm
     insertEntry_append_of_not_contains_right
   rintro ⟨(_|l), hl⟩
   · simp
@@ -861,12 +861,12 @@ theorem toListModel_insert! [instBEq : BEq α] [Ord α] [LawfulBEqOrd α] [Trans
 
 theorem ordered_eraseₘ [Ord α] [TransOrd α] {k : α} {t : Impl α β} (htb : t.Balanced)
     (hto : t.Ordered) : (t.eraseₘ k htb).Ordered :=
-  ordered_updateAtKey _ hto
+  ordered_updateCell _ hto
 
 theorem toListModel_eraseₘ [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β}
     (htb : t.Balanced) (hto : t.Ordered) :
     (t.eraseₘ k htb).toListModel.Perm (eraseKey k t.toListModel) := by
-  refine toListModel_updateAtKey_perm _ hto ?_ eraseKey_of_perm
+  refine toListModel_updateCell_perm _ hto ?_ eraseKey_of_perm
     eraseKey_append_of_containsKey_right_eq_false
   rintro ⟨(_|t), hl⟩
   · simp
@@ -1059,7 +1059,7 @@ theorem ordered_filter [Ord α] {t : Impl α β} {h} {f : (a : α) → β a →
 theorem toListModel_alterₘ [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α]
     {t : Impl α β} {a f} (htb : t.Balanced) (hto : t.Ordered) :
     List.Perm ((t.alterₘ a f htb).toListModel) (alterKey a f t.toListModel) := by
-  refine toListModel_updateAtKey_perm _ hto ?_ alterKey_of_perm
+  refine toListModel_updateCell_perm _ hto ?_ alterKey_of_perm
     alterKey_append_of_containsKey_right_eq_false
   rintro ⟨(_|l), hl⟩
   · simp [Cell.alter, Cell.ofOption]
@@ -1102,7 +1102,7 @@ theorem toListModel_alter [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [Lawf
 theorem ordered_alter [Ord α] [TransOrd α] [LawfulEqOrd α] {t : Impl α β} {a f}
     (htb : t.Balanced) (hto : t.Ordered) : (t.alter a f htb).impl.Ordered := by
   rw [alter_eq_alterₘ htb hto, alterₘ]
-  exact ordered_updateAtKey htb hto
+  exact ordered_updateCell htb hto
 
 /-!
 ### alter!
@@ -1313,7 +1313,7 @@ theorem WF.getThenInsertIfNew?! [Ord α] [TransOrd α] [LawfulEqOrd α] {k : α}
 theorem toListModel_alterₘ [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α β} {a f}
     (htb : t.Balanced) (hto : t.Ordered) :
     List.Perm ((alterₘ a f t htb).toListModel) (Const.alterKey a f t.toListModel) := by
-  refine toListModel_updateAtKey_perm _ hto ?_ Const.alterKey_of_perm
+  refine toListModel_updateCell_perm _ hto ?_ Const.alterKey_of_perm
     Const.alterKey_append_of_containsKey_right_eq_false
   rintro ⟨(_|l), hl⟩
   · simp [Cell.Const.alter, Cell.ofOption]
@@ -1356,7 +1356,7 @@ theorem toListModel_alter [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {t :
 theorem ordered_alter [Ord α] [TransOrd α] {t : Impl α β} {a f}
     (htb : t.Balanced) (hto : t.Ordered) : (alter a f t htb).impl.Ordered := by
   rw [alter_eq_alterₘ htb hto, alterₘ]
-  exact ordered_updateAtKey htb hto
+  exact ordered_updateCell htb hto
 
 /-!
 ### alter!
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
index cf2c4671b7..2359c6ac97 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
@@ -439,7 +439,7 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment)
     · rw [goCache_denote_eq]
       exact hinv
     · symm
-      apply BitVec.getLsbD_ge
+      apply BitVec.getLsbD_of_ge
       omega
   · rw [eval_shiftLeft, ← hres, denote_blastShiftLeft]
     · intro idx hidx
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsbD.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsbD.lean
index e456f1d347..fbd100faae 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsbD.lean
+++ b/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]
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean
index 40cfcd0522..d07e3967b7 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean
@@ -115,7 +115,7 @@ theorem go_denote_eq {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr + 1 ≤
     rw [hacc]
     rw [BitVec.mulRec_succ_eq]
     have : rexpr.getLsbD (curr + 1) = false := by
-      apply BitVec.getLsbD_ge
+      apply BitVec.getLsbD_of_ge
       omega
     simp [this]
 termination_by w - curr
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean
index dceb5be1a6..ef31e8289a 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean
@@ -206,11 +206,11 @@ 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,
-          decide_true, Bool.true_and, Bool.iff_and_self, Bool.not_eq_true', decide_eq_false_iff_not,
+          decide_true, Bool.true_and, Bool.eq_and_self, Bool.not_eq_true', decide_eq_false_iff_not,
           Nat.not_lt]
         omega
     · next hif1 =>
@@ -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,8 +294,8 @@ 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_shiftLeft, Nat.sub_zero, Bool.iff_and_self, Bool.and_eq_true, decide_eq_true_eq,
+      BitVec.getLsbD_of_ge, Bool.false_eq_true, ↓reduceIte, BitVec.reduceHShiftLeft',
+      BitVec.getLsbD_shiftLeft, Nat.sub_zero, Bool.eq_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
   · rw [← hg]
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean
index 8b6202681b..72f8947d77 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean
+++ b/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]
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Sub.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Sub.lean
index 244d238283..d53dca9317 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Sub.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Sub.lean
@@ -31,7 +31,7 @@ theorem denote_blastSub (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Boo
             =
           (lhs - rhs).getLsbD idx := by
   intro idx hidx
-  rw [BitVec.sub_toAdd]
+  rw [BitVec.sub_eq_add_neg]
   unfold blastSub
   rw [denote_blastAdd]
   · intros
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.lean
index 0e0117a07d..81511863dc 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.lean
@@ -109,7 +109,7 @@ theorem denote_bitblast (aig : AIG BVBit) (input : BVExpr.WithCache BVPred aig)
     · rw [BVExpr.denote_bitblast]
       exact hinv
     · symm
-      apply BitVec.getLsbD_ge
+      apply BitVec.getLsbD_of_ge
       omega
 
 end BVPred
diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
index fef0384ea8..b3b0d1a39a 100644
--- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
@@ -172,12 +172,12 @@ attribute [bv_normalize] BitVec.intMin
 -- Used in simproc because of - normalization
 theorem BitVec.ones_and (a : BitVec w) : (-1#w) &&& a = a := by
   ext
-  simp [BitVec.negOne_eq_allOnes]
+  simp [BitVec.neg_one_eq_allOnes]
 
 -- Used in simproc because of - normalization
 theorem BitVec.and_ones (a : BitVec w) : a &&& (-1#w) = a := by
   ext
-  simp [BitVec.negOne_eq_allOnes]
+  simp [BitVec.neg_one_eq_allOnes]
 
 -- Normalize (1#w + ~~~x) to (~~~x + 1#w) to limit the number of symmetries we need for theorems
 -- related to negative BitVecs.
@@ -200,7 +200,7 @@ theorem BitVec.and_contra' (a : BitVec w) : ~~~a &&& a = 0#w := by
 @[bv_normalize]
 theorem BitVec.add_not (a : BitVec w) : a + ~~~a = (-1#w) := by
   ext
-  simp [BitVec.negOne_eq_allOnes]
+  simp [BitVec.neg_one_eq_allOnes]
 
 @[bv_normalize]
 theorem BitVec.not_add (a : BitVec w) : ~~~a + a = (-1#w) := by
@@ -210,20 +210,20 @@ theorem BitVec.not_add (a : BitVec w) : ~~~a + a = (-1#w) := by
 @[bv_normalize]
 theorem BitVec.add_neg (a : BitVec w) : a + (~~~a + 1#w) = 0#w := by
   rw [← BitVec.neg_eq_not_add]
-  rw [← BitVec.sub_toAdd]
+  rw [← BitVec.sub_eq_add_neg]
   rw [BitVec.sub_self]
 
 @[bv_normalize]
 theorem BitVec.neg_add (a : BitVec w) : (~~~a + 1#w) + a = 0#w := by
   rw [← BitVec.neg_eq_not_add]
   rw [BitVec.add_comm]
-  rw [← BitVec.sub_toAdd]
+  rw [← BitVec.sub_eq_add_neg]
   rw [BitVec.sub_self]
 
 @[bv_normalize]
 theorem BitVec.not_neg (x : BitVec w) : ~~~(~~~x + 1#w) = x + -1#w := by
   rw [← BitVec.neg_eq_not_add x]
-  rw [_root_.BitVec.not_neg, _root_.BitVec.sub_toAdd]
+  rw [_root_.BitVec.not_neg, BitVec.sub_eq_add_neg]
 
 @[bv_normalize]
 theorem BitVec.not_neg' (x : BitVec w) : ~~~(x + 1#w) = ~~~x + -1#w := by
@@ -334,12 +334,12 @@ theorem BitVec.lt_one_iff (a : BitVec n) (h : 0 < n) : (BitVec.ult a 1#n) = (a =
 
 -- used in simproc because of -1#w normalisation
 theorem BitVec.max_ult' (a : BitVec w) : (BitVec.ult (-1#w) a) = false := by
-  rw [BitVec.negOne_eq_allOnes, ← Bool.not_eq_true, ← @lt_ult]
+  rw [BitVec.neg_one_eq_allOnes, ← Bool.not_eq_true, ← @lt_ult]
   exact BitVec.not_allOnes_lt
 
 theorem BitVec.ult_max' (a : BitVec w) : (BitVec.ult a (-1#w)) = (!(a == -1#w)) := by
   have := BitVec.lt_allOnes_iff (x := a)
-  rw [lt_ult, ← BitVec.negOne_eq_allOnes] at this
+  rw [lt_ult, ← BitVec.neg_one_eq_allOnes] at this
   by_cases (a.ult (-1#w)) <;> simp_all
 
 attribute [bv_normalize] BitVec.replicate_zero_eq
@@ -455,7 +455,7 @@ theorem BitVec.append_const_right {a : BitVec w1} :
 theorem BitVec.signExtend_elim {v : Nat} {x : BitVec v} {w : Nat} (h : v ≤ w) :
     BitVec.signExtend w x = ((bif x.msb then -1#(w - v) else 0#(w - v)) ++ x).cast (by omega) := by
   rw [BitVec.signExtend_eq_append_of_le]
-  simp [BitVec.negOne_eq_allOnes, cond_eq_if]
+  simp [BitVec.neg_one_eq_allOnes, cond_eq_if]
   assumption
 
 theorem BitVec.signExtend_elim' {v : Nat} {x : BitVec v} {w : Nat} (h : w ≤ v) :
@@ -488,13 +488,13 @@ theorem BitVec.norm_bv_add_mul' {x y : BitVec w} : ~~~(~~~y * x) + 1#w = x + (y
 
 theorem BitVec.mul_beq_mul_short_circuit_left {x₁ x₂ y : BitVec w} :
     (x₁ * y == x₂ * y) = !(!x₁ == x₂ && !x₁ * y == x₂ * y) := by
-  simp only [Bool.not_and, Bool.not_not, Bool.iff_or_self, beq_iff_eq]
+  simp only [Bool.not_and, Bool.not_not, Bool.eq_or_self, beq_iff_eq]
   intros
   congr
 
 theorem BitVec.mul_beq_mul_short_circuit_right {x y₁ y₂ : BitVec w} :
     (x * y₁ == x * y₂) = !(!y₁ == y₂ && !x * y₁ == x * y₂) := by
-  simp only [Bool.not_and, Bool.not_not, Bool.iff_or_self, beq_iff_eq]
+  simp only [Bool.not_and, Bool.not_not, Bool.eq_or_self, beq_iff_eq]
   intros
   congr
 
diff --git a/src/Std/Tactic/BVDecide/Normalize/Equal.lean b/src/Std/Tactic/BVDecide/Normalize/Equal.lean
index 455d4632f6..ee65768531 100644
--- a/src/Std/Tactic/BVDecide/Normalize/Equal.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/Equal.lean
@@ -39,11 +39,11 @@ theorem BitVec.zero_beq_xor_iff (a b : BitVec w) : (0#w == a ^^^ b) = (a == b) :
 
 -- used in bv_and_eq_allOnes simproc
 theorem BitVec.and_eq_allOnes (a b : BitVec w) : (a &&& b == -1#w) = (a == -1#w && b == -1#w) := by
-  rw [Bool.eq_iff_iff, beq_iff_eq, BitVec.negOne_eq_allOnes]
+  rw [Bool.eq_iff_iff, beq_iff_eq, BitVec.neg_one_eq_allOnes]
   simp
 
 theorem BitVec.allOnes_eq_and (a b : BitVec w) : (-1#w == a &&& b) = (a == -1#w && b == -1#w) := by
-  rw [Bool.eq_iff_iff, beq_iff_eq, Eq.comm, BitVec.negOne_eq_allOnes]
+  rw [Bool.eq_iff_iff, beq_iff_eq, Eq.comm, BitVec.neg_one_eq_allOnes]
   simp
 
 @[bv_normalize]
@@ -106,7 +106,7 @@ theorem BitVec.self_eq_add_left (a b : BitVec w) : (a == b + a) = (b == 0#w) :=
 
 @[bv_normalize]
 theorem BitVec.eq_sub_iff_add_eq (a b c : BitVec w) : (a == c + (~~~b + 1#w)) = (a + b == c) := by
-  rw [Bool.eq_iff_iff, beq_iff_eq, beq_iff_eq, ← BitVec.neg_eq_not_add, ← @BitVec.sub_toAdd]
+  rw [Bool.eq_iff_iff, beq_iff_eq, beq_iff_eq, ← BitVec.neg_eq_not_add, ← BitVec.sub_eq_add_neg]
   exact _root_.BitVec.eq_sub_iff_add_eq
 
 @[bv_normalize]
@@ -116,7 +116,7 @@ theorem BitVec.eq_neg_add_iff_add_eq (a b c : BitVec w) : (a == (~~~b + 1#w) + c
 
 @[bv_normalize]
 theorem BitVec.sub_eq_iff_eq_add (a b c : BitVec w) : (a + (~~~b + 1#w) == c) = (a == c + b) := by
-  rw [Bool.eq_iff_iff, beq_iff_eq, beq_iff_eq, ← BitVec.neg_eq_not_add, ← @BitVec.sub_toAdd]
+  rw [Bool.eq_iff_iff, beq_iff_eq, beq_iff_eq, ← BitVec.neg_eq_not_add, ← BitVec.sub_eq_add_neg]
   exact _root_.BitVec.sub_eq_iff_eq_add
 
 @[bv_normalize]