From 705084d9ba258dec704af428d7ce2444525f9ffb Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Thu, 30 Oct 2025 16:58:29 +1100
Subject: [PATCH] chore: deprecate more duplications (#11004)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR deprecates various duplicated definitions, detected in
[#mathlib4 > duplicate declarations @
💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/duplicate.20declarations/near/547434277)
---
 src/Init/ByCases.lean                         |  7 +++
 src/Init/Core.lean                            |  6 ---
 src/Init/Data/Array/Lemmas.lean               |  4 +-
 src/Init/Data/BitVec/Bitblast.lean            |  5 +-
 src/Init/Data/BitVec/Lemmas.lean              | 35 +++++++------
 src/Init/Data/Bool.lean                       |  3 +-
 src/Init/Data/Dyadic/Basic.lean               |  6 +--
 src/Init/Data/Dyadic/Round.lean               |  2 +-
 src/Init/Data/Fin/Lemmas.lean                 | 12 +++--
 src/Init/Data/Int/Basic.lean                  |  5 +-
 src/Init/Data/Int/Bitwise/Lemmas.lean         | 12 ++---
 src/Init/Data/Int/DivMod/Lemmas.lean          | 41 ++++++++--------
 src/Init/Data/Int/Lemmas.lean                 |  4 +-
 src/Init/Data/Int/LemmasAux.lean              |  4 +-
 src/Init/Data/Int/Linear.lean                 |  2 +-
 src/Init/Data/List/Erase.lean                 |  2 +-
 src/Init/Data/List/Find.lean                  | 14 +++---
 src/Init/Data/List/Nat/TakeDrop.lean          |  8 +--
 src/Init/Data/List/ToArray.lean               |  3 +-
 src/Init/Data/Option/Lemmas.lean              |  2 +-
 src/Init/Data/Rat/Lemmas.lean                 | 21 ++++----
 src/Init/Grind/Module/NatModuleNorm.lean      |  2 +-
 src/Init/Grind/Ring/CommSemiringAdapter.lean  | 20 ++++----
 src/Init/Grind/Ring/CommSolver.lean           | 40 +++++++--------
 src/Init/Omega/Int.lean                       |  2 +-
 .../DHashMap/Internal/AssocList/Lemmas.lean   |  4 +-
 src/Std/Data/DHashMap/Internal/WF.lean        |  2 +-
 src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean |  5 +-
 src/Std/Data/Internal/List/Associative.lean   | 49 ++++++++++---------
 src/Std/Sat/AIG/CNF.lean                      | 23 ++++-----
 src/Std/Sat/AIG/RefVecOperator/Map.lean       |  1 +
 src/Std/Sat/AIG/RefVecOperator/Zip.lean       |  1 +
 src/Std/Tactic/BVDecide/Normalize/BitVec.lean |  2 +-
 src/Std/Tactic/BVDecide/Normalize/Bool.lean   |  2 +-
 tests/lean/grind/experiments/bitvec.lean      |  4 +-
 tests/lean/run/grind_bitvec2.lean             |  2 +-
 36 files changed, 188 insertions(+), 169 deletions(-)

diff --git a/src/Init/ByCases.lean b/src/Init/ByCases.lean
index 20d9e42583..5f1222c17e 100644
--- a/src/Init/ByCases.lean
+++ b/src/Init/ByCases.lean
@@ -44,3 +44,10 @@ theorem apply_ite (f : α → β) (P : Prop) [Decidable P] (x y : α) :
 /-- A `dite` whose results do not actually depend on the condition may be reduced to an `ite`. -/
 @[simp] theorem dite_eq_ite [Decidable P] :
   (dite P (fun _ => a) (fun _ => b)) = ite P a b := rfl
+
+-- Remark: dite and ite are "defally equal" when we ignore the proofs.
+@[deprecated dite_eq_ite (since := "2025-10-29")]
+theorem dif_eq_if (c : Prop) {h : Decidable c} {α : Sort u} (t : α) (e : α) : dite c (fun _ => t) (fun _ => e) = ite c t e :=
+  match h with
+  | isTrue _    => rfl
+  | isFalse _   => rfl
diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index a98bccc7f0..8e4959e959 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -1188,12 +1188,6 @@ theorem dif_neg {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort u} {t : c 
   | isTrue hc   => absurd hc hnc
   | isFalse _   => rfl
 
--- Remark: dite and ite are "defally equal" when we ignore the proofs.
-theorem dif_eq_if (c : Prop) {h : Decidable c} {α : Sort u} (t : α) (e : α) : dite c (fun _ => t) (fun _ => e) = ite c t e :=
-  match h with
-  | isTrue _    => rfl
-  | isFalse _   => rfl
-
 @[macro_inline]
 instance {c t e : Prop} [dC : Decidable c] [dT : Decidable t] [dE : Decidable e] : Decidable (if c then t else e) :=
   match dC with
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index 78e8efefc8..09e2c8807e 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -2252,8 +2252,6 @@ theorem flatMap_def {xs : Array α} {f : α → Array β} : xs.flatMap f = flatt
   rcases xs with ⟨l⟩
   simp [flatten_toArray, Function.comp_def, List.flatMap_def]
 
-@[simp, grind =] theorem flatMap_empty {β} {f : α → Array β} : (#[] : Array α).flatMap f = #[] := rfl
-
 theorem flatMap_toList {xs : Array α} {f : α → List β} :
     xs.toList.flatMap f = (xs.flatMap (fun a => (f a).toArray)).toList := by
   rcases xs with ⟨l⟩
@@ -2264,6 +2262,7 @@ theorem flatMap_toList {xs : Array α} {f : α → List β} :
   rcases xs with ⟨l⟩
   simp
 
+@[deprecated List.flatMap_toArray_cons (since := "2025-10-29")]
 theorem flatMap_toArray_cons {β} {f : α → Array β} {a : α} {as : List α} :
     (a :: as).toArray.flatMap f = f a ++ as.toArray.flatMap f := by
   simp [flatMap]
@@ -2274,6 +2273,7 @@ theorem flatMap_toArray_cons {β} {f : α → Array β} {a : α} {as : List α}
   intro cs
   induction as generalizing cs <;> simp_all
 
+@[deprecated List.flatMap_toArray (since := "2025-10-29")]
 theorem flatMap_toArray {β} {f : α → Array β} {as : List α} :
     as.toArray.flatMap f = (as.flatMap (fun a => (f a).toList)).toArray := by
   simp
diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
index 41c7497c7a..2465eb8c3b 100644
--- a/src/Init/Data/BitVec/Bitblast.lean
+++ b/src/Init/Data/BitVec/Bitblast.lean
@@ -635,12 +635,11 @@ theorem mulRec_eq_mul_signExtend_setWidth (x y : BitVec w) (s : Nat) :
     simp only [mulRec_zero_eq, ofNat_eq_ofNat, Nat.reduceAdd]
     by_cases y.getLsbD 0
     case pos hy =>
-      simp only [hy, ↓reduceIte, setWidth_one_eq_ofBool_getLsb_zero,
-        ofBool_true, ofNat_eq_ofNat]
+      simp only [hy, ↓reduceIte, setWidth_one, ofBool_true, ofNat_eq_ofNat]
       rw [setWidth_ofNat_one_eq_ofNat_one_of_lt (by omega)]
       simp
     case neg hy =>
-      simp [hy, setWidth_one_eq_ofBool_getLsb_zero]
+      simp [hy, setWidth_one]
   case succ s' hs =>
     rw [mulRec_succ_eq, hs]
     have heq :
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index d396903c1e..f54cb55926 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -64,6 +64,7 @@ theorem getElem?_eq_none_iff {l : BitVec w} : l[n]? = none ↔ w ≤ n := by
 theorem none_eq_getElem?_iff {l : BitVec w} : none = l[n]? ↔ w ≤ n := by
   simp
 
+@[simp]
 theorem getElem?_eq_none {l : BitVec w} (h : w ≤ n) : l[n]? = none := getElem?_eq_none_iff.mpr h
 
 theorem getElem?_eq (l : BitVec w) (i : Nat) :
@@ -158,7 +159,8 @@ theorem getLsbD_eq_getMsbD (x : BitVec w) (i : Nat) : x.getLsbD i = (decide (i <
     apply getLsbD_of_ge
     omega
 
-@[simp] theorem getElem?_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : x[i]? = none := by
+@[deprecated getElem?_eq_none (since := "2025-10-29")]
+theorem getElem?_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : x[i]? = none := by
   simp [ge]
 
 @[simp] theorem getMsb?_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getMsb? x i = none := by
@@ -415,12 +417,18 @@ theorem getElem?_zero_ofNat_one : (BitVec.ofNat (w+1) 1)[0]? = some true := by
 
 -- This does not need to be a `@[simp]` theorem as it is already handled by `getElem?_eq_getElem`.
 theorem getElem?_zero_ofBool (b : Bool) : (ofBool b)[0]? = some b := by
-  simp only [ofBool, ofNat_eq_ofNat, cond_eq_if]
+  simp only [ofBool, ofNat_eq_ofNat, cond_eq_ite]
   split <;> simp_all
 
-@[simp, grind =] theorem getElem_zero_ofBool (b : Bool) : (ofBool b)[0] = b := by
+@[simp, grind =]
+theorem getElem_ofBool_zero {b : Bool} : (ofBool b)[0] = b := by
   rw [getElem_eq_iff, getElem?_zero_ofBool]
 
+
+@[deprecated getElem_ofBool_zero (since := "2025-10-29")]
+theorem getElem_zero_ofBool (b : Bool) : (ofBool b)[0] = b := by
+  simp
+
 theorem getElem?_succ_ofBool (b : Bool) (i : Nat) : (ofBool b)[i + 1]? = none := by
   simp
 
@@ -431,8 +439,6 @@ theorem getLsbD_ofBool (b : Bool) (i : Nat) : (ofBool b).getLsbD i = ((i = 0) &&
   · simp only [ofBool, ofNat_eq_ofNat, cond_true, getLsbD_ofNat, Bool.and_true]
     by_cases hi : i = 0 <;> simp [hi] <;> omega
 
-theorem getElem_ofBool_zero {b : Bool} : (ofBool b)[0] = b := by simp
-
 @[simp]
 theorem getElem_ofBool {b : Bool} {h : i < 1}: (ofBool b)[i] = b := by
   simp [← getLsbD_eq_getElem]
@@ -580,7 +586,7 @@ theorem toInt_eq_toNat_bmod (x : BitVec n) : x.toInt = Int.bmod x.toNat (2^n) :=
   simp only [toInt_eq_toNat_cond]
   split
   next g =>
-    rw [Int.bmod_pos] <;> simp only [←Int.natCast_emod, toNat_mod_cancel]
+    rw [Int.bmod_eq_emod_of_lt] <;> simp only [←Int.natCast_emod, toNat_mod_cancel]
     omega
   next g =>
     rw [Int.bmod_neg] <;> simp only [←Int.natCast_emod, toNat_mod_cancel]
@@ -988,7 +994,14 @@ theorem msb_setWidth' (x : BitVec w) (h : w ≤ v) : (x.setWidth' h).msb = (deci
 theorem msb_setWidth'' (x : BitVec w) : (x.setWidth (k + 1)).msb = x.getLsbD k := by
   simp [BitVec.msb, getMsbD]
 
+/-- Truncating to width 1 produces a bitvector equal to the least significant bit. -/
+theorem setWidth_one {x : BitVec w} :
+    x.setWidth 1 = ofBool (x.getLsbD 0) := by
+  ext i
+  simp [show i = 0 by omega]
+
 /-- zero extending a bitvector to width 1 equals the boolean of the lsb. -/
+@[deprecated setWidth_one (since := "2025-10-29")]
 theorem setWidth_one_eq_ofBool_getLsb_zero (x : BitVec w) :
     x.setWidth 1 = BitVec.ofBool (x.getLsbD 0) := by
   ext i h
@@ -1004,12 +1017,6 @@ theorem setWidth_ofNat_one_eq_ofNat_one_of_lt {v w : Nat} (hv : 0 < v) :
   have hv := (@Nat.testBit_one_eq_true_iff_self_eq_zero i)
   by_cases h : Nat.testBit 1 i = true <;> simp_all
 
-/-- Truncating to width 1 produces a bitvector equal to the least significant bit. -/
-theorem setWidth_one {x : BitVec w} :
-    x.setWidth 1 = ofBool (x.getLsbD 0) := by
-  ext i
-  simp [show i = 0 by omega]
-
 @[simp, grind =] theorem setWidth_ofNat_of_le (h : v ≤ w) (x : Nat) : setWidth v (BitVec.ofNat w x) = BitVec.ofNat v x := by
   apply BitVec.eq_of_toNat_eq
   simp only [toNat_setWidth, toNat_ofNat]
@@ -1639,11 +1646,11 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
 
 @[simp] theorem ofInt_negSucc_eq_not_ofNat {w n : Nat} :
     BitVec.ofInt w (Int.negSucc n) = ~~~.ofNat w n := by
-  simp only [BitVec.ofInt, Int.toNat, Int.ofNat_eq_coe, toNat_eq, toNat_ofNatLT, toNat_not,
+  simp only [BitVec.ofInt, Int.toNat, Int.ofNat_eq_natCast, toNat_eq, toNat_ofNatLT, toNat_not,
     toNat_ofNat]
   cases h : Int.negSucc n % ((2 ^ w : Nat) : Int)
   case ofNat =>
-    rw [Int.ofNat_eq_coe, Int.negSucc_emod] at h
+    rw [Int.ofNat_eq_natCast, Int.negSucc_emod] at h
     · dsimp only
       omega
     · omega
diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean
index 37da5a0b42..862d65879f 100644
--- a/src/Init/Data/Bool.lean
+++ b/src/Init/Data/Bool.lean
@@ -514,6 +514,7 @@ theorem exists_bool {p : Bool → Prop} : (∃ b, p b) ↔ p false ∨ p true :=
 theorem cond_eq_ite {α} (b : Bool) (t e : α) : cond b t e = if b then t else e := by
   cases b <;> simp
 
+@[deprecated cond_eq_ite (since := "2025-10-29")]
 theorem cond_eq_if : (bif b then x else y) = (if b then x else y) := cond_eq_ite b x y
 
 @[simp] theorem cond_not (b : Bool) (t e : α) : cond (!b) t e = cond b e t := by
@@ -612,7 +613,7 @@ theorem decide_beq_decide (p q : Prop) [dpq : Decidable (p ↔ q)] [dp : Decidab
 
 end Bool
 
-export Bool (cond_eq_if xor and or not)
+export Bool (cond_eq_if cond_eq_ite xor and or not)
 
 /-! ### decide -/
 
diff --git a/src/Init/Data/Dyadic/Basic.lean b/src/Init/Data/Dyadic/Basic.lean
index 88778941b6..22a1283cdf 100644
--- a/src/Init/Data/Dyadic/Basic.lean
+++ b/src/Init/Data/Dyadic/Basic.lean
@@ -287,7 +287,7 @@ theorem toRat_add (x y : Dyadic) : toRat (x + y) = toRat x + toRat y := by
     · rename_i h
       cases Int.sub_eq_iff_eq_add.mp h
       rw [toRat_ofOdd_eq_mkRat, Rat.mkRat_eq_iff (NeZero.ne _) (NeZero.ne _)]
-      simp only [succ_eq_add_one, Int.ofNat_eq_coe, Int.add_shiftLeft, ← Int.shiftLeft_add,
+      simp only [succ_eq_add_one, Int.ofNat_eq_natCast, Int.add_shiftLeft, ← Int.shiftLeft_add,
         Int.natCast_mul, Int.natCast_shiftLeft, Int.shiftLeft_mul_shiftLeft, Int.add_mul]
       congr 2 <;> omega
     · rename_i h
@@ -438,7 +438,7 @@ theorem toDyadic_mkRat (a : Int) (b : Nat) (prec : Int) :
   rcases h : mkRat a b with ⟨n, d, hnz, hr⟩
   obtain ⟨m, hm, rfl, rfl⟩ := Rat.mkRat_num_den hb h
   cases prec
-  · simp only [Rat.toDyadic, Int.ofNat_eq_coe, Int.toNat_natCast, Int.toNat_neg_natCast,
+  · simp only [Rat.toDyadic, Int.ofNat_eq_natCast, Int.toNat_natCast, Int.toNat_neg_natCast,
       shiftLeft_zero, Int.natCast_mul]
     rw [Int.mul_comm d, ← Int.ediv_ediv (by simp), ← Int.shiftLeft_mul,
       Int.mul_ediv_cancel _ (by simpa using hm)]
@@ -463,7 +463,7 @@ theorem toRat_toDyadic (x : Rat) (prec : Int) :
   rw [Rat.floor_def, Int.shiftLeft_eq, Nat.shiftLeft_eq]
   match prec with
   | .ofNat prec =>
-    simp only [Int.ofNat_eq_coe, Int.toNat_natCast, Int.toNat_neg_natCast, Nat.pow_zero,
+    simp only [Int.ofNat_eq_natCast, Int.toNat_natCast, Int.toNat_neg_natCast, Nat.pow_zero,
       Nat.mul_one]
     have : (2 ^ prec : Rat) = ((2 ^ prec : Nat) : Rat) := by simp
     rw [Rat.zpow_natCast, this, Rat.mul_def']
diff --git a/src/Init/Data/Dyadic/Round.lean b/src/Init/Data/Dyadic/Round.lean
index 2a7422dfae..13ff921616 100644
--- a/src/Init/Data/Dyadic/Round.lean
+++ b/src/Init/Data/Dyadic/Round.lean
@@ -36,7 +36,7 @@ theorem roundDown_le {x : Dyadic} {prec : Int} : roundDown x prec ≤ x :=
       refine Lean.Grind.OrderedRing.mul_le_mul_of_nonneg_right ?_ (Rat.zpow_nonneg (by decide))
       rw [Int.shiftRight_eq_div_pow]
       rw [← Lean.Grind.Field.IsOrdered.mul_le_mul_iff_of_pos_right (c := 2^(Int.ofNat l)) (Rat.zpow_pos (by decide))]
-      simp only [Int.natCast_pow, Int.cast_ofNat_Int, Int.ofNat_eq_coe]
+      simp only [Int.natCast_pow, Int.cast_ofNat_Int, Int.ofNat_eq_natCast]
       rw [Rat.mul_assoc, ← Rat.zpow_add (by decide), Int.add_left_neg, Rat.zpow_zero, Rat.mul_one]
       have : (2 : Rat) ^ (l : Int) = (2 ^ l : Int) := by
         rw [Rat.zpow_natCast, Rat.intCast_pow, Rat.intCast_ofNat]
diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean
index d53fca52e8..fb9effeb8c 100644
--- a/src/Init/Data/Fin/Lemmas.lean
+++ b/src/Init/Data/Fin/Lemmas.lean
@@ -547,7 +547,7 @@ theorem succ_cast_eq {n' : Nat} (i : Fin n) (h : n = n') :
 @[simp] theorem cast_castSucc {n' : Nat} {h : n + 1 = n' + 1} {i : Fin n} :
     i.castSucc.cast h = (i.cast (Nat.succ.inj h)).castSucc := rfl
 
-theorem castSucc_lt_succ (i : Fin n) : i.castSucc < i.succ :=
+theorem castSucc_lt_succ {i : Fin n} : i.castSucc < i.succ :=
   lt_def.2 <| by simp only [coe_castSucc, val_succ, Nat.lt_succ_self]
 
 theorem le_castSucc_iff {i : Fin (n + 1)} {j : Fin n} : i ≤ j.castSucc ↔ i < j.succ := by
@@ -587,8 +587,12 @@ theorem castSucc_pos [NeZero n] {i : Fin n} (h : 0 < i) : 0 < i.castSucc := by
 theorem castSucc_ne_zero_iff [NeZero n] {a : Fin n} : a.castSucc ≠ 0 ↔ a ≠ 0 :=
   not_congr <| castSucc_eq_zero_iff
 
+@[simp, grind _=_]
+theorem castSucc_succ (i : Fin n) : i.succ.castSucc = i.castSucc.succ := rfl
+
+@[deprecated castSucc_succ (since := "2025-10-29")]
 theorem castSucc_fin_succ (n : Nat) (j : Fin n) :
-    j.succ.castSucc = (j.castSucc).succ := by simp [Fin.ext_iff]
+    j.succ.castSucc = (j.castSucc).succ := by simp
 
 @[simp]
 theorem coeSucc_eq_succ {a : Fin n} : a.castSucc + 1 = a.succ := by
@@ -596,6 +600,7 @@ theorem coeSucc_eq_succ {a : Fin n} : a.castSucc + 1 = a.succ := by
   · exact a.elim0
   · simp [Fin.ext_iff, add_def, Nat.mod_eq_of_lt (Nat.succ_lt_succ a.is_lt)]
 
+@[deprecated castSucc_lt_succ (since := "2025-10-29")]
 theorem lt_succ {a : Fin n} : a.castSucc < a.succ := by
   rw [castSucc, lt_def, coe_castAdd, val_succ]; exact Nat.lt_succ_self a.val
 
@@ -699,9 +704,6 @@ theorem rev_castSucc (k : Fin n) : rev (castSucc k) = succ (rev k) := k.rev_cast
 
 theorem rev_succ (k : Fin n) : rev (succ k) = castSucc (rev k) := k.rev_addNat 1
 
-@[simp, grind _=_]
-theorem castSucc_succ (i : Fin n) : i.succ.castSucc = i.castSucc.succ := rfl
-
 @[simp, grind =]
 theorem castLE_refl (h : n ≤ n) (i : Fin n) : i.castLE h = i := rfl
 
diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean
index 06a590e951..6a7adcdbfe 100644
--- a/src/Init/Data/Int/Basic.lean
+++ b/src/Init/Data/Int/Basic.lean
@@ -80,7 +80,10 @@ protected theorem zero_ne_one : (0 : Int) ≠ 1 := nofun
 
 /-! ## Coercions -/
 
-@[simp] theorem ofNat_eq_coe : Int.ofNat n = Nat.cast n := rfl
+@[simp] theorem ofNat_eq_natCast (n : Nat) : Int.ofNat n = n := rfl
+
+@[deprecated ofNat_eq_natCast (since := "2025-10-29")]
+theorem ofNat_eq_coe : Int.ofNat n = Nat.cast n := rfl
 
 @[simp] theorem ofNat_zero : ((0 : Nat) : Int) = 0 := rfl
 
diff --git a/src/Init/Data/Int/Bitwise/Lemmas.lean b/src/Init/Data/Int/Bitwise/Lemmas.lean
index 256e751a0d..f745117166 100644
--- a/src/Init/Data/Int/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Int/Bitwise/Lemmas.lean
@@ -47,10 +47,10 @@ theorem shiftRight_zero (n : Int) : n >>> 0 = n := by
   simp [Int.shiftRight_eq_div_pow]
 
 theorem le_shiftRight_of_nonpos {n : Int} {s : Nat} (h : n ≤ 0) : n ≤ n >>> s := by
-  simp only [Int.shiftRight_eq, Int.shiftRight, Int.ofNat_eq_coe]
+  simp only [Int.shiftRight_eq, Int.shiftRight, Int.ofNat_eq_natCast]
   split
   case _ _ _ m =>
-    simp only [ofNat_eq_coe] at h
+    simp only [ofNat_eq_natCast] at h
     by_cases hm : m = 0
     · simp [hm]
     · omega
@@ -61,14 +61,14 @@ theorem le_shiftRight_of_nonpos {n : Int} {s : Nat} (h : n ≤ 0) : n ≤ n >>>
       omega
 
 theorem shiftRight_le_of_nonneg {n : Int} {s : Nat} (h : 0 ≤ n) : n >>> s ≤ n := by
-  simp only [Int.shiftRight_eq, Int.shiftRight, Int.ofNat_eq_coe]
+  simp only [Int.shiftRight_eq, Int.shiftRight, Int.ofNat_eq_natCast]
   split
   case _ _ _ m =>
-    simp only [Int.ofNat_eq_coe] at h
+    simp only [Int.ofNat_eq_natCast] at h
     by_cases hm : m = 0
     · simp [hm]
     · have := Nat.shiftRight_le m s
-      rw [ofNat_eq_coe]
+      rw [ofNat_eq_natCast]
       omega
   case _ _ _ m =>
     omega
@@ -108,7 +108,7 @@ theorem shiftLeft_succ (m : Int) (n : Nat) : m <<< (n + 1) = (m <<< n) * 2 := by
   change Int.shiftLeft _ _ = Int.shiftLeft _ _ * 2
   match m with
   | (m : Nat) =>
-    dsimp only [Int.shiftLeft, Int.ofNat_eq_coe]
+    dsimp only [Int.shiftLeft, Int.ofNat_eq_natCast]
     rw [Nat.shiftLeft_succ, Nat.mul_comm, natCast_mul, ofNat_two]
   | Int.negSucc m =>
     dsimp only [Int.shiftLeft]
diff --git a/src/Init/Data/Int/DivMod/Lemmas.lean b/src/Init/Data/Int/DivMod/Lemmas.lean
index 5b8e35ba47..5dd06102b3 100644
--- a/src/Init/Data/Int/DivMod/Lemmas.lean
+++ b/src/Init/Data/Int/DivMod/Lemmas.lean
@@ -214,7 +214,7 @@ theorem tdiv_eq_ediv {a b : Int} :
   | ofNat a, -[b+1] => simp [tdiv_eq_ediv_of_nonneg]
   | -[a+1], 0 => simp
   | -[a+1], ofNat (succ b) =>
-    simp only [tdiv, Nat.succ_eq_add_one, ofNat_eq_coe, Int.natCast_add, cast_ofNat_Int,
+    simp only [tdiv, Nat.succ_eq_add_one, ofNat_eq_natCast, Int.natCast_add, cast_ofNat_Int,
       negSucc_not_nonneg, sign_natCast_add_one]
     simp only [negSucc_emod_ofNat_succ_eq_zero_iff]
     norm_cast
@@ -225,7 +225,7 @@ theorem tdiv_eq_ediv {a b : Int} :
     · rw [neg_ofNat_eq_negSucc_add_one_iff]
       exact Nat.succ_div_of_mod_ne_zero h
   | -[a+1], -[b+1] =>
-    simp only [tdiv, ofNat_eq_coe, negSucc_not_nonneg, false_or, sign_negSucc]
+    simp only [tdiv, ofNat_eq_natCast, negSucc_not_nonneg, false_or, sign_negSucc]
     norm_cast
     simp only [negSucc_ediv_negSucc]
     rw [Int.natCast_add, Int.natCast_one]
@@ -256,7 +256,7 @@ theorem fdiv_eq_ediv {a b : Int} :
   | 0, -[b+1] => simp
   | ofNat (a + 1), -[b+1] =>
     simp only [fdiv, ofNat_ediv_negSucc, negSucc_not_nonneg, negSucc_dvd, false_or]
-    simp only [ofNat_eq_coe, ofNat_dvd]
+    simp only [ofNat_eq_natCast, ofNat_dvd]
     norm_cast
     rw [Nat.succ_div, negSucc_eq]
     split <;> rename_i h
@@ -264,7 +264,7 @@ theorem fdiv_eq_ediv {a b : Int} :
     · simp [Int.neg_add]
       norm_cast
   | -[a+1], -[b+1] =>
-    simp only [fdiv, ofNat_eq_coe, negSucc_ediv_negSucc, negSucc_not_nonneg, dvd_negSucc, negSucc_dvd,
+    simp only [fdiv, ofNat_eq_natCast, negSucc_ediv_negSucc, negSucc_not_nonneg, dvd_negSucc, negSucc_dvd,
       false_or]
     norm_cast
     rw [Int.natCast_add, Int.natCast_one, Nat.succ_div]
@@ -559,7 +559,7 @@ theorem ediv_eq_one_of_neg_of_le {a b : Int} (H1 : a < 0) (H2 : b ≤ a) : a / b
   match a, b, H1, H2 with
   | negSucc a', ofNat n', H1, H2 => simp [Int.negSucc_eq] at H2; omega
   | negSucc a', negSucc b', H1, H2 =>
-    rw [Int.div_def, ediv, ofNat_eq_coe]
+    rw [Int.div_def, ediv, ofNat_eq_natCast]
     norm_cast
     rw [Nat.succ_eq_add_one, Nat.add_eq_right, Nat.div_eq_zero_iff_lt (by omega)]
     simp [Int.negSucc_eq] at H2
@@ -579,7 +579,7 @@ theorem neg_one_ediv (b : Int) : -1 / b = -b.sign :=
   match b with
   | ofNat 0 => by simp
   | ofNat (b + 1) =>
-    ediv_eq_neg_one_of_neg_of_le (by decide) (by simp [ofNat_eq_coe]; omega)
+    ediv_eq_neg_one_of_neg_of_le (by decide) (by simp [ofNat_eq_natCast]; omega)
   | negSucc b =>
     ediv_eq_one_of_neg_of_le (by decide) (by omega)
 
@@ -1389,7 +1389,7 @@ theorem tmod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : tmod a b < b :=
 
 theorem lt_tmod_of_pos (a : Int) {b : Int} (H : 0 < b) : -b < tmod a b :=
   match a, b, eq_succ_of_zero_lt H with
-  | ofNat _, _, ⟨n, rfl⟩ => by rw [ofNat_eq_coe, ← Int.natCast_succ, ← ofNat_tmod]; omega
+  | ofNat _, _, ⟨n, rfl⟩ => by rw [ofNat_eq_natCast, ← Int.natCast_succ, ← ofNat_tmod]; omega
   | -[a+1], _, ⟨n, rfl⟩ => by
     rw [negSucc_eq, neg_tmod, ← Int.natCast_add_one, ← Int.natCast_add_one, ← ofNat_tmod]
     have : (a + 1) % (n + 1) < n + 1 := Nat.mod_lt _ (Nat.zero_lt_succ n)
@@ -1836,7 +1836,7 @@ theorem le_emod_self_add_one_iff {a b : Int} (h : 0 < b) : b ≤ a % b + 1 ↔ b
   match b, h with
   | .ofNat 1, h => simp
   | .ofNat (b + 2), h =>
-    simp only [ofNat_eq_coe, Int.natCast_add, cast_ofNat_Int] at *
+    simp only [ofNat_eq_natCast, Int.natCast_add, cast_ofNat_Int] at *
     constructor
     · rw [dvd_iff_emod_eq_zero]
       intro w
@@ -1857,7 +1857,7 @@ theorem add_one_tdiv_of_pos {a b : Int} (h : 0 < b) :
   match b, h with
   | .ofNat 1, h => simp; omega
   | .ofNat (b + 2), h =>
-    simp only [ofNat_eq_coe]
+    simp only [ofNat_eq_natCast]
     rw [tdiv_eq_ediv, add_ediv (by omega), tdiv_eq_ediv]
     simp only [Int.natCast_add, cast_ofNat_Int]
     have : 1 / (b + 2 : Int) = 0 := by rw [one_ediv]; omega
@@ -2059,20 +2059,20 @@ theorem neg_fdiv {a b : Int} : (-a).fdiv b = -(a.fdiv b) - if b = 0 ∨ b ∣ a
   | ofNat (a + 1), 0 => simp
   | ofNat (a + 1), ofNat (b + 1) =>
     unfold fdiv
-    simp only [ofNat_eq_coe, Int.natCast_add, cast_ofNat_Int, Nat.succ_eq_add_one]
+    simp only [ofNat_eq_natCast, Int.natCast_add, cast_ofNat_Int, Nat.succ_eq_add_one]
     rw [← negSucc_eq, ← negSucc_eq]
   | ofNat (a + 1), -[b+1] =>
     unfold fdiv
-    simp only [ofNat_eq_coe, Int.natCast_add, cast_ofNat_Int, Nat.succ_eq_add_one]
+    simp only [ofNat_eq_natCast, Int.natCast_add, cast_ofNat_Int, Nat.succ_eq_add_one]
     rw [← negSucc_eq, neg_negSucc]
   | -[a+1], 0 => simp
   | -[a+1], ofNat (b + 1) =>
     unfold fdiv
-    simp only [ofNat_eq_coe, Int.natCast_add, cast_ofNat_Int, Nat.succ_eq_add_one]
+    simp only [ofNat_eq_natCast, Int.natCast_add, cast_ofNat_Int, Nat.succ_eq_add_one]
     rw [neg_negSucc, ← negSucc_eq]
   | -[a+1], -[b+1] =>
     unfold fdiv
-    simp only [ofNat_eq_coe, natCast_ediv, Nat.succ_eq_add_one, Int.natCast_add, cast_ofNat_Int]
+    simp only [ofNat_eq_natCast, natCast_ediv, Nat.succ_eq_add_one, Int.natCast_add, cast_ofNat_Int]
     rw [neg_negSucc, neg_negSucc]
     simp
 
@@ -2361,7 +2361,7 @@ theorem natAbs_fdiv_le_natAbs (a b : Int) : natAbs (a.fdiv b) ≤ natAbs a := by
     | 0, .negSucc b, h => simp at h
     | .ofNat (a + 1), .negSucc 0, h => simp at h
     | .ofNat (a + 1), .negSucc (b + 1), h =>
-      rw [negSucc_eq, ofNat_eq_coe]
+      rw [negSucc_eq, ofNat_eq_natCast]
       norm_cast
       rw [Int.ediv_neg, Int.sub_eq_add_neg, ← Int.neg_add, natAbs_neg]
       norm_cast
@@ -2477,6 +2477,10 @@ theorem bmod_eq_self_sub_mul_bdiv (x : Int) (m : Nat) : bmod x m = x - m * bdiv
 theorem bmod_eq_self_sub_bdiv_mul (x : Int) (m : Nat) : bmod x m = x - bdiv x m * m := by
   rw [← Int.add_sub_cancel (bmod x m), bmod_add_bdiv']
 
+theorem bmod_eq_emod_of_lt {x : Int} {m : Nat} (hx : x % m < (m + 1) / 2) : bmod x m = x % m := by
+  simp [bmod, hx]
+
+@[deprecated Int.bmod_eq_emod_of_lt (since := "2025-10-29")]
 theorem bmod_pos (x : Int) (m : Nat) (p : x % m < (m + 1) / 2) : bmod x m = x % m := by
   simp [bmod_def, p]
 
@@ -2486,7 +2490,7 @@ theorem bmod_neg (x : Int) (m : Nat) (p : x % m ≥ (m + 1) / 2) : bmod x m = (x
 theorem bmod_eq_emod (x : Int) (m : Nat) : bmod x m = x % m - if x % m ≥ (m + 1) / 2 then m else 0 := by
   split
   · rwa [bmod_neg]
-  · rw [bmod_pos] <;> simp_all
+  · rw [bmod_eq_emod_of_lt] <;> simp_all
 
 @[simp]
 theorem bmod_one (x : Int) : Int.bmod x 1 = 0 := by
@@ -2723,9 +2727,6 @@ theorem bmod_eq_iff {a : Int} {b : Nat} {c : Int} (hb : 0 < b) :
     have := bmod_lt (x := a) (m := b) hb
     omega
 
-theorem bmod_eq_emod_of_lt {x : Int} {m : Nat} (hx : x % m < (m + 1) / 2) : bmod x m = x % m := by
-  simp [bmod, hx]
-
 theorem bmod_eq_neg {n : Nat} {m : Int} (hm : 0 ≤ m) (hn : n = 2 * m) : m.bmod n = -m := by
   by_cases h : m = 0
   · subst h; simp
@@ -2766,7 +2767,7 @@ theorem one_bmod_two : Int.bmod 1 2 = -1 := by simp
 
 theorem one_bmod {b : Nat} (h : 3 ≤ b) : Int.bmod 1 b = 1 := by
   have hb : 1 % (b : Int) = 1 := by rw [one_emod]; omega
-  rw [bmod_pos _ _ (by omega), hb]
+  rw [bmod_eq_emod_of_lt (by omega), hb]
 
 theorem bmod_two_eq (x : Int) : x.bmod 2 = -1 ∨ x.bmod 2 = 0 := by
   have := le_bmod (x := x) (m := 2) (by omega)
@@ -2941,7 +2942,7 @@ theorem neg_self_le_ediv_of_nonneg_of_nonpos (x y : Int) (hx : 0 ≤ x) (hy : y
   · obtain ⟨xn, rfl⟩ := Int.eq_ofNat_of_zero_le (a := x) (by omega)
     obtain ⟨yn, rfl⟩ := Int.eq_negSucc_of_lt_zero (a := y) (by omega)
     rw [show xn = ofNat xn by norm_cast, Int.ofNat_ediv_negSucc (a := xn)]
-    simp only [ofNat_eq_coe, natCast_ediv, Int.natCast_add, cast_ofNat_Int, Int.neg_le_neg_iff]
+    simp only [ofNat_eq_natCast, natCast_ediv, Int.natCast_add, cast_ofNat_Int, Int.neg_le_neg_iff]
     norm_cast
     apply Nat.le_trans (m := xn) (by exact Nat.div_le_self xn (yn + 1)) (by omega)
 
diff --git a/src/Init/Data/Int/Lemmas.lean b/src/Init/Data/Int/Lemmas.lean
index eb4b79b5af..242bdf2990 100644
--- a/src/Init/Data/Int/Lemmas.lean
+++ b/src/Init/Data/Int/Lemmas.lean
@@ -17,7 +17,7 @@ open Nat
 /-! ## Definitions of basic functions -/
 
 theorem subNatNat_of_sub_eq_zero {m n : Nat} (h : n - m = 0) : subNatNat m n = ↑(m - n) := by
-  rw [subNatNat, h, ofNat_eq_coe]
+  rw [subNatNat, h, ofNat_eq_natCast]
 
 theorem subNatNat_of_sub_eq_succ {m n k : Nat} (h : n - m = succ k) : subNatNat m n = -[k+1] := by
   rw [subNatNat, h]
@@ -129,7 +129,7 @@ theorem subNatNat_elim (m n : Nat) (motive : Nat → Nat → Int → Prop)
 
 theorem subNatNat_add_left : subNatNat (m + n) m = n := by
   unfold subNatNat
-  rw [Nat.sub_eq_zero_of_le (Nat.le_add_right ..), Nat.add_sub_cancel_left, ofNat_eq_coe]
+  rw [Nat.sub_eq_zero_of_le (Nat.le_add_right ..), Nat.add_sub_cancel_left, ofNat_eq_natCast]
 
 theorem subNatNat_add_right : subNatNat m (m + n + 1) = negSucc n := by
   simp [subNatNat, Nat.add_assoc, Nat.add_sub_cancel_left]
diff --git a/src/Init/Data/Int/LemmasAux.lean b/src/Init/Data/Int/LemmasAux.lean
index 2417bc3c65..73f7359e61 100644
--- a/src/Init/Data/Int/LemmasAux.lean
+++ b/src/Init/Data/Int/LemmasAux.lean
@@ -49,8 +49,6 @@ protected theorem ofNat_mul_out (m n : Nat) : ↑m * ↑n = (↑(m * n) : Int) :
 
 protected theorem ofNat_add_one_out (n : Nat) : ↑n + (1 : Int) = ↑(Nat.succ n) := rfl
 
-@[simp] theorem ofNat_eq_natCast (n : Nat) : Int.ofNat n = n := rfl
-
 @[norm_cast] theorem natCast_inj {m n : Nat} : (m : Int) = (n : Int) ↔ m = n := ofNat_inj
 
 @[norm_cast]
@@ -84,7 +82,7 @@ theorem natCast_succ_pos (n : Nat) : 0 < (n.succ : Int) := natCast_pos.2 n.succ_
   symm
   simp only [Int.toNat]
   split <;> rename_i x a
-  · simp only [Int.ofNat_eq_coe]
+  · simp only [Int.ofNat_eq_natCast]
     split <;> rename_i y b h
     · simp at h
       omega
diff --git a/src/Init/Data/Int/Linear.lean b/src/Init/Data/Int/Linear.lean
index 3acac32964..b6f50bc775 100644
--- a/src/Init/Data/Int/Linear.lean
+++ b/src/Init/Data/Int/Linear.lean
@@ -1091,7 +1091,7 @@ theorem eq_unsat_coeff (ctx : Context) (p : Poly) (k : Int) : eq_unsat_coeff_cer
   induction p
   next => rfl
   next a y p ih =>
-    simp [coeff_k, coeff, cond_eq_if]; split
+    simp [coeff_k, coeff, cond_eq_ite]; split
     next h => simp [h]
     next h => rw [← Nat.beq_eq, Bool.not_eq_true] at h; simp [h, ← ih]; rfl
 
diff --git a/src/Init/Data/List/Erase.lean b/src/Init/Data/List/Erase.lean
index 83b9a3b977..ff453badd5 100644
--- a/src/Init/Data/List/Erase.lean
+++ b/src/Init/Data/List/Erase.lean
@@ -44,7 +44,7 @@ theorem eraseP_of_forall_not {l : List α} (h : ∀ a, a ∈ l → ¬p a) : l.er
   induction xs with
   | nil => simp
   | cons x xs ih =>
-    simp only [eraseP_cons, cond_eq_if]
+    simp only [eraseP_cons, cond_eq_ite]
     split <;> rename_i h
     · simp only [reduceCtorEq, cons.injEq, false_or]
       constructor
diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean
index ac247ae708..99f40dfdbe 100644
--- a/src/Init/Data/List/Find.lean
+++ b/src/Init/Data/List/Find.lean
@@ -579,7 +579,7 @@ theorem findIdx_eq_length {p : α → Bool} {xs : List α} :
   | nil => simp_all
   | cons x xs ih =>
     rw [findIdx_cons, length_cons]
-    simp only [cond_eq_if]
+    simp only [cond_eq_ite]
     split <;> simp_all
 
 theorem findIdx_eq_length_of_false {p : α → Bool} {xs : List α} (h : ∀ x ∈ xs, p x = false) :
@@ -669,7 +669,7 @@ theorem findIdx_append {p : α → Bool} {l₁ l₂ : List α} :
     simp only [findIdx_cons, length_cons, cons_append]
     by_cases h : p x
     · simp [h]
-    · simp only [h, ih, cond_eq_if, Bool.false_eq_true, ↓reduceIte, add_one_lt_add_one_iff]
+    · simp only [h, ih, cond_eq_ite, Bool.false_eq_true, ↓reduceIte, add_one_lt_add_one_iff]
       split <;> simp [Nat.add_assoc]
 
 theorem IsPrefix.findIdx_le {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂) :
@@ -699,7 +699,7 @@ theorem findIdx_le_findIdx {l : List α} {p q : α → Bool} (h : ∀ x ∈ l, p
   induction l with
   | nil => simp
   | cons x xs ih =>
-    simp only [findIdx_cons, cond_eq_if]
+    simp only [findIdx_cons, cond_eq_ite]
     split
     · simp
     · split
@@ -752,10 +752,10 @@ theorem findIdx?_eq_some_iff_findIdx_eq {xs : List α} {p : α → Bool} {i : Na
   | cons x xs ih =>
     simp only [findIdx?_cons, findIdx_cons]
     split
-    · simp_all [cond_eq_if]
+    · simp_all [cond_eq_ite]
       rintro rfl
       exact zero_lt_succ xs.length
-    · simp_all [cond_eq_if, and_assoc]
+    · simp_all [cond_eq_ite, and_assoc]
       constructor
       · rintro ⟨a, lt, rfl, rfl⟩
         simp_all [Nat.succ_lt_succ_iff]
@@ -1098,7 +1098,7 @@ theorem idxOf_eq_length [BEq α] [LawfulBEq α] {l : List α} (h : a ∉ l) : l.
   | nil => rfl
   | cons x xs ih =>
     simp only [mem_cons, not_or] at h
-    simp only [idxOf_cons, cond_eq_if, beq_iff_eq]
+    simp only [idxOf_cons, cond_eq_ite, beq_iff_eq]
     split <;> simp_all
 
 
@@ -1110,7 +1110,7 @@ theorem idxOf_lt_length_of_mem [BEq α] [EquivBEq α] {l : List α} (h : a ∈ l
     simp only [mem_cons] at h
     obtain rfl | h := h
     · simp
-    · simp only [idxOf_cons, cond_eq_if, length_cons]
+    · simp only [idxOf_cons, cond_eq_ite, length_cons]
       specialize ih h
       split
       · exact zero_lt_succ xs.length
diff --git a/src/Init/Data/List/Nat/TakeDrop.lean b/src/Init/Data/List/Nat/TakeDrop.lean
index 987d90bdc8..9ca767fd73 100644
--- a/src/Init/Data/List/Nat/TakeDrop.lean
+++ b/src/Init/Data/List/Nat/TakeDrop.lean
@@ -467,7 +467,7 @@ theorem false_of_mem_take_findIdx {xs : List α} {p : α → Bool} (h : x ∈ xs
   | cons x xs ih =>
     cases i
     · simp
-    · simp only [take_succ_cons, findIdx_cons, ih, cond_eq_if]
+    · simp only [take_succ_cons, findIdx_cons, ih, cond_eq_ite]
       split
       · simp
       · rw [Nat.add_min_add_right]
@@ -477,7 +477,7 @@ theorem false_of_mem_take_findIdx {xs : List α} {p : α → Bool} (h : x ∈ xs
   induction xs with
   | nil => simp
   | cons x xs ih =>
-    simp [findIdx_cons, cond_eq_if]
+    simp [findIdx_cons, cond_eq_ite]
     split <;> split <;> simp_all [Nat.add_min_add_right]
 
 /-! ### findIdx? -/
@@ -501,7 +501,7 @@ theorem takeWhile_eq_take_findIdx_not {xs : List α} {p : α → Bool} :
   induction xs with
   | nil => simp
   | cons x xs ih =>
-    simp only [takeWhile_cons, ih, findIdx_cons, cond_eq_if, Bool.not_eq_eq_eq_not, Bool.not_true]
+    simp only [takeWhile_cons, ih, findIdx_cons, cond_eq_ite, Bool.not_eq_eq_eq_not, Bool.not_true]
     split <;> simp_all
 
 theorem dropWhile_eq_drop_findIdx_not {xs : List α} {p : α → Bool} :
@@ -509,7 +509,7 @@ theorem dropWhile_eq_drop_findIdx_not {xs : List α} {p : α → Bool} :
   induction xs with
   | nil => simp
   | cons x xs ih =>
-    simp only [dropWhile_cons, ih, findIdx_cons, cond_eq_if, Bool.not_eq_eq_eq_not, Bool.not_true]
+    simp only [dropWhile_cons, ih, findIdx_cons, cond_eq_ite, Bool.not_eq_eq_eq_not, Bool.not_true]
     split <;> simp_all
 
 /-! ### rotateLeft -/
diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean
index 4eaa5a80cd..ccf17cd8ed 100644
--- a/src/Init/Data/List/ToArray.lean
+++ b/src/Init/Data/List/ToArray.lean
@@ -548,7 +548,8 @@ theorem _root_.Array.replicate_eq_toArray_replicate :
     Array.replicate n v = (List.replicate n v).toArray := by
   simp
 
-@[simp, grind =] theorem flatMap_empty {β} (f : α → Array β) : (#[] : Array α).flatMap f = #[] := rfl
+@[simp, grind =] theorem _root_.Array.flatMap_empty {β} (f : α → Array β) :
+    (#[] : Array α).flatMap f = #[] := rfl
 
 theorem flatMap_toArray_cons {β} (f : α → Array β) (a : α) (as : List α) :
     (a :: as).toArray.flatMap f = f a ++ as.toArray.flatMap f := by
diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean
index 5bae6e0ba0..de615d6484 100644
--- a/src/Init/Data/Option/Lemmas.lean
+++ b/src/Init/Data/Option/Lemmas.lean
@@ -1319,7 +1319,7 @@ theorem pfilter_congr {α : Type u} {o o' : Option α} (ho : o = o')
 
 @[simp, grind =] theorem pfilter_some {α : Type _} {x : α} {p : (a : α) → some x = some a → Bool} :
     (some x).pfilter p = if p x rfl then some x else none := by
-  simp only [pfilter, cond_eq_if]
+  simp only [pfilter, cond_eq_ite]
 
 theorem isSome_pfilter_iff {α : Type _} {o : Option α} {p : (a : α) → o = some a → Bool} :
     (o.pfilter p).isSome ↔ ∃ (a : α) (ha : o = some a), p a ha := by
diff --git a/src/Init/Data/Rat/Lemmas.lean b/src/Init/Data/Rat/Lemmas.lean
index 2cf5d5f112..16a4c5f7b6 100644
--- a/src/Init/Data/Rat/Lemmas.lean
+++ b/src/Init/Data/Rat/Lemmas.lean
@@ -160,11 +160,12 @@ theorem mkRat_eq_iff (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) :
 @[simp] theorem divInt_ofNat (num den) : num /. (den : Nat) = mkRat num den := by
   simp [divInt]
 
-theorem mk_eq_divInt (num den nz c) : ⟨num, den, nz, c⟩ = num /. (den : Nat) := by
+theorem mk_eq_divInt {num den nz c} : ⟨num, den, nz, c⟩ = num /. (den : Nat) := by
   simp [mk_eq_mkRat]
 
 theorem num_divInt_den (a : Rat) : a.num /. a.den = a := by rw [divInt_ofNat, mkRat_self]
 
+@[deprecated mk_eq_divInt (since := "2025-10-29")]
 theorem mk'_eq_divInt {n d h c} : (⟨n, d, h, c⟩ : Rat) = n /. d := (num_divInt_den _).symm
 
 @[deprecated num_divInt_den (since := "2025-08-22")]
@@ -220,7 +221,7 @@ theorem num_divInt (a b : Int) : (a /. b).num = b.sign * a / b.gcd a := by
   rw [divInt.eq_def]
   simp only [inline, Nat.succ_eq_add_one]
   split <;> rename_i d
-  · simp only [num_mkRat, Int.ofNat_eq_coe]
+  · simp only [num_mkRat, Int.ofNat_eq_natCast]
     split <;> rename_i h
     · simp_all
     · rw [Int.sign_natCast_of_ne_zero h, Int.one_mul, Int.gcd]
@@ -231,7 +232,7 @@ theorem den_divInt (a b : Int) : (a /. b).den = if b = 0 then 1 else b.natAbs /
   rw [divInt.eq_def]
   simp only [inline, Nat.succ_eq_add_one]
   split <;> rename_i d
-  · simp only [den_mkRat, Int.ofNat_eq_coe, Int.natAbs_natCast]
+  · simp only [den_mkRat, Int.ofNat_eq_natCast, Int.natAbs_natCast]
     split <;> rename_i h
     · simp_all
     · simp [if_neg (by omega), Int.gcd]
@@ -242,7 +243,7 @@ numbers of the form `n /. d` with `0 < d` and coprime `n`, `d`. -/
 @[elab_as_elim]
 def numDenCasesOn.{u} {C : Rat → Sort u} :
     ∀ (a : Rat) (_ : ∀ n d, 0 < d → (Int.natAbs n).Coprime d → C (n /. d)), C a
-  | ⟨n, d, h, c⟩, H => by rw [mk'_eq_divInt]; exact H n d (Nat.pos_of_ne_zero h) c
+  | ⟨n, d, h, c⟩, H => by rw [mk_eq_divInt]; exact H n d (Nat.pos_of_ne_zero h) c
 
 /-- Define a (dependent) function or prove `∀ r : Rat, p r` by dealing with rational
 numbers of the form `n /. d` with `d ≠ 0`. -/
@@ -256,7 +257,9 @@ numbers of the form `mk' n d` with `d ≠ 0`. -/
 @[elab_as_elim]
 def numDenCasesOn''.{u} {C : Rat → Sort u} (a : Rat)
     (H : ∀ (n : Int) (d : Nat) (nz red), C (mk' n d nz red)) : C a :=
-  numDenCasesOn a fun n d h h' ↦ by rw [← mk_eq_divInt _ _ (Nat.ne_of_gt h) h']; exact H n d (Nat.ne_of_gt h) _
+  numDenCasesOn a fun n d h h' ↦ by
+    rw [← mk_eq_divInt (c := h')]
+    exact H n d (Nat.ne_of_gt h) _
 
 @[simp] protected theorem ofInt_ofNat : ofInt (OfNat.ofNat n) = OfNat.ofNat n := rfl
 
@@ -529,7 +532,7 @@ protected theorem mul_eq_zero {a b : Rat} : a * b = 0 ↔ a = 0 ∨ b = 0 := by
 theorem div_def (a b : Rat) : a / b = a * b⁻¹ := rfl
 
 theorem divInt_eq_div (a b : Int) : a /. b = a / b := by
-  rw [← Rat.mk_den_one, ← Rat.mk_den_one, Rat.mk'_eq_divInt, Rat.mk'_eq_divInt, div_def,
+  rw [← Rat.mk_den_one, ← Rat.mk_den_one, Rat.mk_eq_divInt, Rat.mk_eq_divInt, div_def,
     inv_divInt, divInt_mul_divInt, Int.cast_ofNat_Int, Int.mul_one, Int.one_mul]
 
 theorem mkRat_eq_div (a : Int) (b : Nat) : mkRat a b = a / b := by
@@ -553,7 +556,7 @@ theorem pow_def (q : Rat) (n : Nat) :
 protected theorem pow_succ (q : Rat) (n : Nat) : q ^ (n + 1) = q ^ n * q := by
   rcases q with ⟨n, d, hn, r⟩
   simp only [pow_def, Int.pow_succ, Nat.pow_succ]
-  simp only [mk'_eq_divInt, Int.natCast_mul, divInt_mul_divInt]
+  simp only [mk_eq_divInt, Int.natCast_mul, divInt_mul_divInt]
 
 @[simp] protected theorem pow_one (q : Rat) : q ^ 1 = q := by simp [Rat.pow_succ]
 
@@ -621,7 +624,7 @@ theorem num_eq_zero {q : Rat} : q.num = 0 ↔ q = 0 := by
   induction q
   constructor
   · rintro rfl
-    rw [mk'_eq_divInt, zero_divInt]
+    rw [mk_eq_divInt, zero_divInt]
   · exact congrArg Rat.num
 
 protected theorem nonneg_antisymm {q : Rat} : 0 ≤ q → 0 ≤ -q → q = 0 := by
@@ -634,7 +637,7 @@ protected theorem nonneg_total (a : Rat) : 0 ≤ a ∨ 0 ≤ -a := by
 @[simp] theorem divInt_nonneg_iff_of_pos_right {a b : Int} (hb : 0 < b) :
     0 ≤ a /. b ↔ 0 ≤ a := by
   rcases hab : a /. b with ⟨n, d, hd, hnd⟩
-  rw [mk'_eq_divInt, divInt_eq_divInt_iff (Int.ne_of_gt hb) (mod_cast hd)] at hab
+  rw [mk_eq_divInt, divInt_eq_divInt_iff (Int.ne_of_gt hb) (mod_cast hd)] at hab
   rw [← num_nonneg, ← Int.mul_nonneg_iff_of_pos_right hb, ← hab,
     Int.mul_nonneg_iff_of_pos_right (mod_cast Nat.pos_of_ne_zero hd)]
 
diff --git a/src/Init/Grind/Module/NatModuleNorm.lean b/src/Init/Grind/Module/NatModuleNorm.lean
index ec8a6a8dcb..c7fbdd4585 100644
--- a/src/Init/Grind/Module/NatModuleNorm.lean
+++ b/src/Init/Grind/Module/NatModuleNorm.lean
@@ -35,7 +35,7 @@ def Poly.denoteN_nil {α} [NatModule α] (ctx : Context α) : Poly.denoteN ctx .
 
 def Poly.denoteN_add {α} [NatModule α] (ctx : Context α) (k : Int) (x : Var) (p : Poly)
     : k ≥ 0 → Poly.denoteN ctx (.add k x p) = k.toNat • x.denote ctx + p.denoteN ctx := by
-  intro h; simp [denoteN, cond_eq_if]; split
+  intro h; simp [denoteN, cond_eq_ite]; split
   next => omega
   next =>
     have : (k.natAbs : Int) = k.toNat := by
diff --git a/src/Init/Grind/Ring/CommSemiringAdapter.lean b/src/Init/Grind/Ring/CommSemiringAdapter.lean
index 009915fc0a..1d958a08e8 100644
--- a/src/Init/Grind/Ring/CommSemiringAdapter.lean
+++ b/src/Init/Grind/Ring/CommSemiringAdapter.lean
@@ -79,7 +79,7 @@ def denoteSInt {α} [Semiring α] (k : Int) : α :=
     OfNat.ofNat (α := α) k.natAbs
 
 theorem denoteSInt_eq {α} [Semiring α] (k : Int) : denoteSInt (α := α) k = k.toNat := by
-  simp [denoteSInt, cond_eq_if] <;> split
+  simp [denoteSInt, cond_eq_ite] <;> split
   next h => rw [ofNat_eq_natCast, Int.toNat_of_nonpos (Int.le_of_lt h)]
   next h =>
     have : (k.natAbs : Int) = k.toNat := by
@@ -103,7 +103,7 @@ theorem Poly.denoteS_ofVar {α} [Semiring α] (ctx : Context α) (x : Var)
 
 theorem Poly.denoteS_addConst {α} [Semiring α] (ctx : Context α) (p : Poly) (k : Int)
     : k ≥ 0 → p.NonnegCoeffs → (addConst p k).denoteS ctx = p.denoteS ctx + k.toNat := by
-  simp [addConst, cond_eq_if]; split
+  simp [addConst, cond_eq_ite]; split
   next => subst k; simp
   next =>
     fun_induction addConst.go <;> simp [denoteS, *]
@@ -116,7 +116,7 @@ theorem Poly.denoteS_addConst {α} [Semiring α] (ctx : Context α) (p : Poly) (
 
 theorem Poly.denoteS_insert {α} [Semiring α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly)
     : k ≥ 0 → p.NonnegCoeffs → (insert k m p).denoteS ctx = k.toNat * m.denote ctx + p.denoteS ctx := by
-  simp [insert, cond_eq_if] <;> split
+  simp [insert, cond_eq_ite] <;> split
   next => simp [*]
   next =>
     split
@@ -149,7 +149,7 @@ theorem Poly.denoteS_concat {α} [Semiring α] (ctx : Context α) (p₁ p₂ : P
 
 theorem Poly.denoteS_mulConst {α} [Semiring α] (ctx : Context α) (k : Int) (p : Poly)
     : k ≥ 0 → p.NonnegCoeffs → (mulConst k p).denoteS ctx = k.toNat * p.denoteS ctx := by
-  simp [mulConst, cond_eq_if] <;> split
+  simp [mulConst, cond_eq_ite] <;> split
   next => simp [denoteS, *, zero_mul]
   next =>
     split <;> try simp [*]
@@ -196,7 +196,7 @@ theorem Poly.denoteS_combine {α} [Semiring α] (ctx : Context α) (p₁ p₂ :
 
 theorem Poly.denoteS_mulMon {α} [CommSemiring α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly)
     : k ≥ 0 → p.NonnegCoeffs → (mulMon k m p).denoteS ctx = k.toNat * m.denote ctx * p.denoteS ctx := by
-  simp [mulMon, cond_eq_if] <;> split
+  simp [mulMon, cond_eq_ite] <;> split
   next => simp [denoteS, *]
   next =>
     split
@@ -218,7 +218,7 @@ theorem Poly.denoteS_mulMon {α} [CommSemiring α] (ctx : Context α) (k : Int)
         assumption; assumption
 
 theorem Poly.addConst_NonnegCoeffs {p : Poly} {k : Int} : k ≥ 0 → p.NonnegCoeffs → (p.addConst k).NonnegCoeffs := by
-  simp [addConst, cond_eq_if]; split
+  simp [addConst, cond_eq_ite]; split
   next => intros; assumption
   fun_induction addConst.go
   next h _ => intro _ h; cases h; constructor; apply Int.add_nonneg <;> assumption
@@ -269,7 +269,7 @@ theorem Poly.num_zero_NonnegCoeffs : (num 0).NonnegCoeffs := by
 
 theorem Poly.denoteS_mulMon_nc {α} [Semiring α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly)
     : k ≥ 0 → p.NonnegCoeffs → (mulMon_nc k m p).denoteS ctx = k.toNat * m.denote ctx * p.denoteS ctx := by
-  simp [mulMon_nc, cond_eq_if] <;> split
+  simp [mulMon_nc, cond_eq_ite] <;> split
   next => simp [denoteS, *]
   next =>
     split
@@ -282,7 +282,7 @@ theorem Poly.denoteS_mulMon_nc {α} [Semiring α] (ctx : Context α) (k : Int) (
       simp [this, denoteS]
 
 theorem Poly.mulConst_NonnegCoeffs {p : Poly} {k : Int} : k ≥ 0 → p.NonnegCoeffs → (p.mulConst k).NonnegCoeffs := by
-  simp [mulConst, cond_eq_if]; split
+  simp [mulConst, cond_eq_ite]; split
   next => intros; constructor; decide
   split; intros; assumption
   fun_induction mulConst.go
@@ -295,7 +295,7 @@ theorem Poly.mulConst_NonnegCoeffs {p : Poly} {k : Int} : k ≥ 0 → p.NonnegCo
     next ih _ h => exact ih h₁ h
 
 theorem Poly.mulMon_NonnegCoeffs {p : Poly} {k : Int} (m : Mon) : k ≥ 0 → p.NonnegCoeffs → (p.mulMon k m).NonnegCoeffs := by
-  simp [mulMon, cond_eq_if]; split
+  simp [mulMon, cond_eq_ite]; split
   next => intros; constructor; decide
   split
   next => intros; apply mulConst_NonnegCoeffs <;> assumption
@@ -323,7 +323,7 @@ theorem Poly.mulMon_nc_go_NonnegCoeffs {p : Poly} {k : Int} (m : Mon) {acc : Pol
     next => assumption
 
 theorem Poly.mulMon_nc_NonnegCoeffs {p : Poly} {k : Int} (m : Mon) : k ≥ 0 → p.NonnegCoeffs → (p.mulMon_nc k m).NonnegCoeffs := by
-  simp [mulMon_nc, cond_eq_if]; split
+  simp [mulMon_nc, cond_eq_ite]; split
   next => intros; constructor; decide
   split
   next => intros; apply mulConst_NonnegCoeffs <;> assumption
diff --git a/src/Init/Grind/Ring/CommSolver.lean b/src/Init/Grind/Ring/CommSolver.lean
index 92976e37af..d1c98e2d31 100644
--- a/src/Init/Grind/Ring/CommSolver.lean
+++ b/src/Init/Grind/Ring/CommSolver.lean
@@ -272,7 +272,7 @@ theorem Mon.revlex_k_eq_revlex (m₁ m₂ : Mon) : m₁.revlex_k m₂ = m₁.rev
   next =>
     simp [revlexFuel]; split <;> try rfl
     next ih _ _ pw₁ m₁ pw₂ m₂ =>
-      simp only [cond_eq_if, beq_iff_eq]
+      simp only [cond_eq_ite, beq_iff_eq]
       split
       next h =>
         replace h : Nat.beq pw₁.x pw₂.x = true := by rw [Nat.beq_eq, h]
@@ -378,7 +378,7 @@ noncomputable def Poly.addConst_k (p : Poly) (k : Int) : Poly :=
     (Int.beq' k 0)
 
 theorem Poly.addConst_k_eq_addConst (p : Poly) (k : Int) : addConst_k p k = addConst p k := by
-  unfold addConst_k addConst; rw [cond_eq_if]
+  unfold addConst_k addConst; rw [cond_eq_ite]
   split
   next h => rw [← Int.beq'_eq_beq] at h; rw [h]
   next h =>
@@ -433,7 +433,7 @@ noncomputable def Poly.mulConst_k (k : Int) (p : Poly) : Poly :=
     (Int.beq' k 0)
 
 @[simp] theorem Poly.mulConst_k_eq_mulConst (k : Int) (p : Poly) : p.mulConst_k k = p.mulConst k := by
-  simp [mulConst_k, mulConst, cond_eq_if]; split
+  simp [mulConst_k, mulConst, cond_eq_ite]; split
   next =>
     have h : Int.beq' k 0 = true := by simp [*]
     simp [h]
@@ -479,7 +479,7 @@ noncomputable def Poly.mulMon_k (k : Int) (m : Mon) (p : Poly) : Poly :=
     (Int.beq' k 0)
 
 @[simp] theorem Poly.mulMon_k_eq_mulMon (k : Int) (m : Mon) (p : Poly) : p.mulMon_k k m = p.mulMon k m := by
-  simp [mulMon_k, mulMon, cond_eq_if]; split
+  simp [mulMon_k, mulMon, cond_eq_ite]; split
   next =>
     have h : Int.beq' k 0 = true := by simp [*]
     simp [h]
@@ -492,7 +492,7 @@ noncomputable def Poly.mulMon_k (k : Int) (m : Mon) (p : Poly) : Poly :=
     next h =>
       have h₂ : m.beq' .unit = false := by rw [← Bool.not_eq_true, Mon.beq'_eq]; simp at h; assumption
       simp [h₂]
-      induction p <;> simp [mulMon.go, cond_eq_if]
+      induction p <;> simp [mulMon.go, cond_eq_ite]
       next k =>
         split
         next =>
@@ -653,7 +653,7 @@ noncomputable def Expr.toPoly_k (e : Expr) : Poly :=
   case sub => rw [← Poly.combine_k_eq_combine, ← Poly.mulConst_k_eq_mulConst]; congr
   case mul => congr
   case pow a k ih =>
-    rw [cond_eq_if]; split
+    rw [cond_eq_ite]; split
     next h => rw [Nat.beq_eq_true_eq, ← Nat.beq_eq] at h; rw [h]
     next h =>
       rw [Nat.beq_eq_true_eq, ← Nat.beq_eq, Bool.not_eq_true] at h; rw [h]; dsimp only
@@ -951,11 +951,11 @@ theorem Mon.denote_mul_nc {α} [Semiring α] (ctx : Context α) (m₁ m₂ : Mon
   fun_induction mul_nc <;> simp [denote, Semiring.one_mul, Semiring.mul_one, denote_mulPow_nc, Semiring.mul_assoc, *]
 
 theorem Var.eq_of_revlex {x₁ x₂ : Var} : x₁.revlex x₂ = .eq → x₁ = x₂ := by
-  simp [revlex, cond_eq_if] <;> split <;> simp
+  simp [revlex, cond_eq_ite] <;> split <;> simp
   next h₁ => intro h₂; exact Nat.le_antisymm h₂ (Nat.ge_of_not_lt h₁)
 
 theorem eq_of_powerRevlex {k₁ k₂ : Nat} : powerRevlex k₁ k₂ = .eq → k₁ = k₂ := by
-  simp [powerRevlex, cond_eq_if] <;> split <;> simp
+  simp [powerRevlex, cond_eq_ite] <;> split <;> simp
   next h₁ => intro h₂; exact Nat.le_antisymm h₂ (Nat.ge_of_not_lt h₁)
 
 theorem Power.eq_of_revlex (p₁ p₂ : Power) : p₁.revlex p₂ = .eq → p₁ = p₂ := by
@@ -996,7 +996,7 @@ theorem Mon.eq_of_grevlex {m₁ m₂ : Mon} : grevlex m₁ m₂ = .eq → m₁ =
   simp [grevlex]; intro; apply eq_of_revlex
 
 theorem Poly.denoteTerm_eq  {α} [Ring α] (ctx : Context α) (k : Int) (m : Mon) : denote'.denoteTerm ctx k m = k * m.denote ctx := by
-  simp [denote'.denoteTerm, Mon.denote'_eq_denote, cond_eq_if, zsmul_eq_intCast_mul]; intro; subst k; rw [Ring.intCast_one, Semiring.one_mul]
+  simp [denote'.denoteTerm, Mon.denote'_eq_denote, cond_eq_ite, zsmul_eq_intCast_mul]; intro; subst k; rw [Ring.intCast_one, Semiring.one_mul]
 
 theorem Poly.denote'_eq_denote {α} [Ring α] (ctx : Context α) (p : Poly) : p.denote' ctx = p.denote ctx := by
   cases p <;> simp [denote', denote, denoteTerm_eq, zsmul_eq_intCast_mul]
@@ -1014,7 +1014,7 @@ theorem Poly.denote_ofVar {α} [Ring α] (ctx : Context α) (x : Var)
   simp [ofVar, denote_ofMon, Mon.denote_ofVar]
 
 theorem Poly.denote_addConst {α} [Ring α] (ctx : Context α) (p : Poly) (k : Int) : (addConst p k).denote ctx = p.denote ctx + k := by
-  simp [addConst, cond_eq_if]; split
+  simp [addConst, cond_eq_ite]; split
   next => simp [*, intCast_zero, add_zero]
   next =>
     fun_induction addConst.go <;> simp [denote, *]
@@ -1023,7 +1023,7 @@ theorem Poly.denote_addConst {α} [Ring α] (ctx : Context α) (p : Poly) (k : I
 
 theorem Poly.denote_insert {α} [Ring α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly)
     : (insert k m p).denote ctx = k * m.denote ctx + p.denote ctx := by
-  simp [insert, cond_eq_if] <;> split
+  simp [insert, cond_eq_ite] <;> split
   next => simp [*, intCast_zero, zero_mul, zero_add]
   next =>
     split
@@ -1046,7 +1046,7 @@ theorem Poly.denote_concat {α} [Ring α] (ctx : Context α) (p₁ p₂ : Poly)
 
 theorem Poly.denote_mulConst {α} [Ring α] (ctx : Context α) (k : Int) (p : Poly)
     : (mulConst k p).denote ctx = k * p.denote ctx := by
-  simp [mulConst, cond_eq_if] <;> split
+  simp [mulConst, cond_eq_ite] <;> split
   next => simp [denote, *, intCast_zero, zero_mul]
   next =>
     split <;> try simp [*, intCast_one, one_mul]
@@ -1056,7 +1056,7 @@ theorem Poly.denote_mulConst {α} [Ring α] (ctx : Context α) (k : Int) (p : Po
 
 theorem Poly.denote_mulMon {α} [CommRing α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly)
     : (mulMon k m p).denote ctx = k * m.denote ctx * p.denote ctx := by
-  simp [mulMon, cond_eq_if] <;> split
+  simp [mulMon, cond_eq_ite] <;> split
   next => simp [denote, *, intCast_zero, zero_mul]
   next =>
     split
@@ -1080,7 +1080,7 @@ theorem Poly.denote_mulMon_nc_go {α} [Ring α] (ctx : Context α) (k : Int) (m
 
 theorem Poly.denote_mulMon_nc {α} [Ring α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly)
     : (mulMon_nc k m p).denote ctx = k * m.denote ctx * p.denote ctx := by
-  simp [mulMon_nc, cond_eq_if] <;> split
+  simp [mulMon_nc, cond_eq_ite] <;> split
   next => simp [denote, *, intCast_zero, zero_mul]
   next =>
     split
@@ -1176,7 +1176,7 @@ theorem Poly.denote_addConstC {α c} [Ring α] [IsCharP α c] (ctx : Context α)
 
 theorem Poly.denote_insertC {α c} [Ring α] [IsCharP α c] (ctx : Context α) (k : Int) (m : Mon) (p : Poly)
     : (insertC k m p c).denote ctx = k * m.denote ctx + p.denote ctx := by
-  simp [insertC, cond_eq_if] <;> split
+  simp [insertC, cond_eq_ite] <;> split
   next =>
     rw [← IsCharP.intCast_emod (p := c)]
     simp +zetaDelta [*, intCast_zero, zero_mul, zero_add]
@@ -1193,7 +1193,7 @@ theorem Poly.denote_insertC {α c} [Ring α] [IsCharP α c] (ctx : Context α) (
 
 theorem Poly.denote_mulConstC {α c} [Ring α] [IsCharP α c] (ctx : Context α) (k : Int) (p : Poly)
     : (mulConstC k p c).denote ctx = k * p.denote ctx := by
-  simp [mulConstC, cond_eq_if] <;> split
+  simp [mulConstC, cond_eq_ite] <;> split
   next =>
     rw [← IsCharP.intCast_emod (p := c)]
     simp [denote, *, intCast_zero, zero_mul]
@@ -1214,7 +1214,7 @@ theorem Poly.denote_mulConstC {α c} [Ring α] [IsCharP α c] (ctx : Context α)
 
 theorem Poly.denote_mulMonC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (k : Int) (m : Mon) (p : Poly)
     : (mulMonC k m p c).denote ctx = k * m.denote ctx * p.denote ctx := by
-  simp [mulMonC, cond_eq_if] <;> split
+  simp [mulMonC, cond_eq_ite] <;> split
   next =>
     rw [← IsCharP.intCast_emod (p := c)]
     simp [denote, *, intCast_zero, zero_mul]
@@ -1253,7 +1253,7 @@ theorem Poly.denote_mulMonC_nc_go {α c} [Ring α] [IsCharP α c] (ctx : Context
 
 theorem Poly.denote_mulMonC_nc {α c} [Ring α] [IsCharP α c] (ctx : Context α) (k : Int) (m : Mon) (p : Poly)
     : (mulMonC_nc k m p c).denote ctx = k * m.denote ctx * p.denote ctx := by
-  simp [mulMonC_nc, cond_eq_if] <;> split
+  simp [mulMonC_nc, cond_eq_ite] <;> split
   next =>
     rw [← IsCharP.intCast_emod (p := c)]
     simp [denote, *, intCast_zero, zero_mul]
@@ -1679,10 +1679,10 @@ private theorem of_mod_eq_0 {α} [CommRing α] {a : Int} {c : Nat} : Int.cast c
 theorem Poly.normEq0_eq {α} [CommRing α] (ctx : Context α) (p : Poly) (c : Nat) (h : Int.cast c = (0 : α)) : (p.normEq0 c).denote ctx = p.denote ctx := by
   induction p
   next a =>
-    simp [denote, normEq0, cond_eq_if]; split <;> simp [denote]
+    simp [denote, normEq0, cond_eq_ite]; split <;> simp [denote]
     next h' => rw [of_mod_eq_0 h h', Ring.intCast_zero]
   next a m p ih =>
-    simp [denote, normEq0, cond_eq_if]; split <;> simp [denote, zsmul_eq_intCast_mul, *]
+    simp [denote, normEq0, cond_eq_ite]; split <;> simp [denote, zsmul_eq_intCast_mul, *]
     next h' => rw [of_mod_eq_0 h h', Semiring.zero_mul, zero_add]
 
 noncomputable def eq_normEq0_cert (c : Nat) (p₁ p₂ p : Poly) : Bool :=
diff --git a/src/Init/Omega/Int.lean b/src/Init/Omega/Int.lean
index db10c43480..baa7b4b38a 100644
--- a/src/Init/Omega/Int.lean
+++ b/src/Init/Omega/Int.lean
@@ -121,7 +121,7 @@ theorem ofNat_max (a b : Nat) : ((max a b : Nat) : Int) = max (a : Int) (b : Int
 theorem ofNat_natAbs (a : Int) : (a.natAbs : Int) = if 0 ≤ a then a else -a := by
   rw [Int.natAbs.eq_def]
   split <;> rename_i n
-  · simp only [Int.ofNat_eq_coe]
+  · simp only [Int.ofNat_eq_natCast]
     rw [if_pos (Int.natCast_nonneg n)]
   · simp
 
diff --git a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
index 6a62e63cd4..ec5a160fb1 100644
--- a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
@@ -200,7 +200,7 @@ theorem toList_filter {f : (a : α) → β a → Bool} {l : AssocList α β} :
   induction l' generalizing l
   · simp [filter.go]
   next k v t ih =>
-    simp only [filter.go, toList_cons, List.filter_cons, cond_eq_if]
+    simp only [filter.go, toList_cons, List.filter_cons, cond_eq_ite]
     split
     · exact (ih _).trans (by simpa using perm_middle.symm)
     · exact ih _
@@ -220,7 +220,7 @@ theorem filterMap_eq_filter {f : (a : α) → β a → Bool} {l : AssocList α 
   induction l generalizing l' with
   | nil => rfl
   | cons k v t ih =>
-    simp only [filterMap.go, filter.go, ih, Option.guard, cond_eq_if]
+    simp only [filterMap.go, filter.go, ih, Option.guard, cond_eq_ite]
     symm; split <;> rfl
 
 theorem toList_alter [BEq α] [LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)}
diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean
index bdfbe5407c..eefc861de9 100644
--- a/src/Std/Data/DHashMap/Internal/WF.lean
+++ b/src/Std/Data/DHashMap/Internal/WF.lean
@@ -849,7 +849,7 @@ theorem toListModel_insertIfNewₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulH
     (h : Raw.WFImp m.1) {a : α} {b : β a} :
     Perm (toListModel (m.insertIfNewₘ a b).1.buckets)
       (insertEntryIfNew a b (toListModel m.1.buckets)) := by
-  rw [insertIfNewₘ, insertEntryIfNew, containsₘ_eq_containsKey h, cond_eq_if]
+  rw [insertIfNewₘ, insertEntryIfNew, containsₘ_eq_containsKey h, cond_eq_ite]
   split
   next h' => exact Perm.refl _
   next h' => exact (toListModel_expandIfNecessary _).trans (toListModel_consₘ m h a b)
diff --git a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
index 8549fda13c..19b5b43a83 100644
--- a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
@@ -959,7 +959,7 @@ theorem ordered_insertIfNew [Ord α] [TransOrd α] {k : α} {v : β k} {l : Impl
 theorem toListModel_insertIfNew [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k}
     {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) :
     (l.insertIfNew k v hlb).impl.toListModel.Perm (insertEntryIfNew k v l.toListModel) := by
-  simp only [Impl.insertIfNew, insertEntryIfNew, cond_eq_if, contains_eq_containsKey hlo]
+  simp only [Impl.insertIfNew, insertEntryIfNew, cond_eq_ite, contains_eq_containsKey hlo]
   split
   · rfl
   · refine (toListModel_insert hlb hlo).trans ?_
@@ -1350,8 +1350,7 @@ theorem toListModel_alterₘ [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {
     cases f none <;> rfl
   · simp only [Cell.Const.alter, Cell.ofOption, Const.alterKey, Option.toList_some]
     have := OrientedCmp.eq_symm <| hl l rfl
-    simp only [getValue?, compare_eq_iff_beq.mp this, cond_eq_if,
-      reduceIte]
+    simp only [getValue?, compare_eq_iff_beq.mp this, cond_eq_ite, reduceIte]
     cases f _
     · simp [eraseKey, compare_eq_iff_beq.mp this]
     · simp [insertEntry, containsKey, replaceEntry, compare_eq_iff_beq.mp this]
diff --git a/src/Std/Data/Internal/List/Associative.lean b/src/Std/Data/Internal/List/Associative.lean
index f57645efa6..f59ff7dd62 100644
--- a/src/Std/Data/Internal/List/Associative.lean
+++ b/src/Std/Data/Internal/List/Associative.lean
@@ -107,7 +107,7 @@ theorem getEntry?_eq_some_iff [BEq α] [EquivBEq α] {l : List ((a : α) × β a
   induction l using assoc_induction with
   | nil => simp
   | cons lk lv tail ih =>
-    simp only [getEntry?_cons, cond_eq_if, List.mem_cons]
+    simp only [getEntry?_cons, cond_eq_ite, List.mem_cons]
     split
     · rename_i hlkk
       simp only [Option.some.injEq]
@@ -506,7 +506,7 @@ theorem getEntry_mem [BEq α] {l : List ((a : α) × β a)} {k : α} {h} :
   induction l using assoc_induction with
   | nil => contradiction
   | cons k v l ih =>
-    simp only [getEntry?_cons, cond_eq_if]
+    simp only [getEntry?_cons, cond_eq_ite]
     split
     · exact List.mem_cons_self
     · simp only [List.mem_cons]
@@ -565,7 +565,7 @@ theorem getValue_cons [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} {
     getValue a (⟨k, v⟩ :: l) h = if h' : k == a then v
       else getValue a l (containsKey_of_containsKey_cons (k := k) h (Bool.eq_false_iff.2 h')) := by
   rw [← Option.some_inj, ← getValue?_eq_some_getValue, getValue?_cons, apply_dite Option.some,
-    cond_eq_if]
+    cond_eq_ite]
   split
   · rfl
   · exact getValue?_eq_some_getValue _
@@ -839,7 +839,7 @@ theorem getKey?_beq [BEq α] {l : List ((a : α) × β a)} {a : α} :
   induction l using assoc_induction with
   | nil => rfl
   | cons k v l ih =>
-    rw [getKey?_cons, cond_eq_if]
+    rw [getKey?_cons, cond_eq_ite]
     split <;> assumption
 
 theorem getKey?_congr [BEq α] [EquivBEq α] {l : List ((a : α) × β a)}
@@ -859,7 +859,7 @@ theorem getEntry?_eq_some_iff_getKey?_eq_some_getValue?_eq_some [BEq α] {β : T
   induction l with
   | nil => simp
   | cons hd tl ih =>
-    simp [getEntry?, getKey?, getValue?, cond_eq_if]
+    simp [getEntry?, getKey?, getValue?, cond_eq_ite]
     split
     · rename_i h
       simp [Sigma.ext_iff]
@@ -885,7 +885,7 @@ theorem getKey_cons [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
     getKey a (⟨k, v⟩ :: l) h = if h' : k == a then k
       else getKey a l (containsKey_of_containsKey_cons (k := k) h (Bool.eq_false_iff.2 h')) := by
   rw [← Option.some_inj, ← getKey?_eq_some_getKey, getKey?_cons, apply_dite Option.some,
-    cond_eq_if]
+    cond_eq_ite]
   split
   · rfl
   · exact getKey?_eq_some_getKey _
@@ -1068,7 +1068,7 @@ theorem getEntry?_eq_getValueCast? [BEq α] [LawfulBEq α] {l : List ((a : α) 
   induction l using assoc_induction with
   | nil => rfl
   | cons k v l ih =>
-    simp only [getEntry?_cons, getValueCast?_cons, cond_eq_if]
+    simp only [getEntry?_cons, getValueCast?_cons, cond_eq_ite]
     split
     · rename_i h
       simp only [beq_iff_eq] at h
@@ -1121,7 +1121,7 @@ theorem isEmpty_replaceEntry [BEq α] {l : List ((a : α) × β a)} {k : α} {v
     (replaceEntry k v l).isEmpty = l.isEmpty := by
   induction l using assoc_induction
   · simp
-  · simp only [replaceEntry_cons, cond_eq_if, List.isEmpty_cons]
+  · simp only [replaceEntry_cons, cond_eq_ite, List.isEmpty_cons]
     split <;> simp
 
 theorem mem_replaceEntry_of_beq_eq_false [BEq α] [EquivBEq α] {a : α} {b : β a}
@@ -1130,7 +1130,7 @@ theorem mem_replaceEntry_of_beq_eq_false [BEq α] [EquivBEq α] {a : α} {b : β
   induction l
   · simp only [replaceEntry_nil]
   next ih =>
-    simp only [replaceEntry, cond_eq_if]
+    simp only [replaceEntry, cond_eq_ite]
     split
     next h =>
       simp only [List.mem_cons, Sigma.ext_iff]
@@ -1200,12 +1200,13 @@ theorem getEntry_replaceEntry_of_true [BEq α] [PartialEquivBEq α] {l : List ((
   simp only [getEntry, getEntry?_replaceEntry]
   simp_all [containsKey_congr h]
 
+@[deprecated getEntry_mem (since := "2025-10-29")]
 theorem mem_getEntry [BEq α] {l : List ((a : α) × β a)} {k : α} (hl : containsKey k l) :
     getEntry k l hl ∈ l := by
   induction l using assoc_induction
   · simp at hl
   next k' v' l ih =>
-    simp [getEntry, getEntry?_cons, cond_eq_if]
+    simp [getEntry, getEntry?_cons, cond_eq_ite]
     split
     · simp
     · simp only [containsKey_cons, Bool.or_eq_true] at hl
@@ -1310,7 +1311,7 @@ theorem mem_eraseKey_of_key_beq_eq_false [BEq α] {a : α}
   · simp only [eraseKey_nil]
   next ih =>
     simp only [eraseKey, List.mem_cons]
-    rw [cond_eq_if]
+    rw [cond_eq_ite]
     split
     next h =>
       rw [iff_or_self, Sigma.ext_iff]
@@ -1405,7 +1406,7 @@ theorem insertEntry_nil [BEq α] {k : α} {v : β k} :
 theorem insertEntry_cons_of_false [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k}
     {v' : β k'} (h : (k' == k) = false) :
     Perm (insertEntry k v (⟨k', v'⟩ :: l)) (⟨k', v'⟩ :: insertEntry k v l) := by
-  simp only [insertEntry, containsKey_cons, h, Bool.false_or, cond_eq_if]
+  simp only [insertEntry, containsKey_cons, h, Bool.false_or, cond_eq_ite]
   split
   · rw [replaceEntry_cons_of_false h]
   · apply Perm.swap
@@ -1430,7 +1431,7 @@ theorem insertEntry_of_containsKey_eq_false [BEq α] {l : List ((a : α) × β a
 theorem mem_insertEntry_of_key_beq_eq_false [BEq α] [EquivBEq α] {a : α} {b : β a}
     {l : List ((a : α) × β a)} (p : (a : α) × β a)
     (hne : (p.1 == a) = false) : p ∈ insertEntry a b l ↔ p ∈ l := by
-  simp only [insertEntry, cond_eq_if]
+  simp only [insertEntry, cond_eq_ite]
   split
   · exact mem_replaceEntry_of_beq_eq_false p hne
   · simp only [List.mem_cons, or_iff_right_iff_imp, Sigma.ext_iff]
@@ -1507,7 +1508,7 @@ theorem getEntry?_insertEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α)
     {v : β k} :
     getEntry? a (insertEntry k v l) = if k == a then some ⟨k, v⟩ else getEntry? a l := by
   cases hl : containsKey k l
-  · rw [insertEntry_of_containsKey_eq_false hl, getEntry?_cons, cond_eq_if]
+  · rw [insertEntry_of_containsKey_eq_false hl, getEntry?_cons, cond_eq_ite]
   · simp [insertEntry_of_containsKey hl, getEntry?_replaceEntry, hl]
 
 theorem getValueCast?_insertEntry [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
@@ -1662,7 +1663,7 @@ theorem insertEntryIfNew_of_containsKey_eq_false [BEq α] {l : List ((a : α) ×
 theorem DistinctKeys.insertEntryIfNew [BEq α] [PartialEquivBEq α] {k : α} {v : β k}
     {l : List ((a : α) × β a)} (h : DistinctKeys l) :
     DistinctKeys (insertEntryIfNew k v l) := by
-  simp only [Std.Internal.List.insertEntryIfNew, cond_eq_if]
+  simp only [Std.Internal.List.insertEntryIfNew, cond_eq_ite]
   split
   · exact h
   · rw [distinctKeys_cons_iff]
@@ -2508,7 +2509,7 @@ theorem find?_map_toProd_eq_some_iff_getKey?_eq_some_and_getValue?_eq_some [BEq
   | nil => simp
   | cons hd tl ih =>
     simp only [List.map_cons, List.find?_cons_eq_some, Prod.mk.injEq, Bool.not_eq_eq_eq_not,
-      Bool.not_true, getKey?, cond_eq_if, getValue?]
+      Bool.not_true, getKey?, cond_eq_ite, getValue?]
     by_cases hdfst_k: hd.fst == k
     · simp only [hdfst_k, true_and, Bool.true_eq_false, false_and, or_false, ↓reduceIte,
       Option.some.injEq]
@@ -3773,7 +3774,7 @@ theorem insertListIfNewUnit_perm_of_perm_first [BEq α] [EquivBEq α] {l1 l2 : L
   | cons hd tl ih =>
     simp only [insertListIfNewUnit]
     apply ih
-    · simp only [insertEntryIfNew, cond_eq_if]
+    · simp only [insertEntryIfNew, cond_eq_ite]
       have contains_eq : containsKey hd l1 = containsKey hd l2 := containsKey_of_perm h
       rw [contains_eq]
       by_cases contains_hd: containsKey hd l2 = true
@@ -4621,7 +4622,7 @@ theorem isEmpty_modifyKey [BEq α] [LawfulBEq α] (k : α) (f : β k → β k) (
   match l with
   | [] => simp [modifyKey]
   | a :: as =>
-    simp only [modifyKey, replaceEntry, cond_eq_if]
+    simp only [modifyKey, replaceEntry, cond_eq_ite]
     repeat' split <;> simp
 
 theorem length_modifyKey [BEq α] [LawfulBEq α] (k : α) (f : β k → β k) (l : List ((a : α) × β a)) :
@@ -4799,7 +4800,7 @@ theorem isEmpty_modifyKey (k : α) (f : β → β) (l : List ((_ : α) × β)) :
   match l with
   | [] => simp [modifyKey]
   | a :: as =>
-    simp only [modifyKey, replaceEntry, cond_eq_if]
+    simp only [modifyKey, replaceEntry, cond_eq_ite]
     repeat' split <;> simp
 
 theorem modifyKey_eq_alterKey (k : α) (f : β → β) (l : List ((_ : α) × β)) :
@@ -5041,7 +5042,7 @@ theorem getEntry?_filterMap' [BEq α] [EquivBEq α]
   induction l using assoc_induction with
   | nil => rfl
   | cons k' v l ih =>
-    simp only [getEntry?, cond_eq_if]
+    simp only [getEntry?, cond_eq_ite]
     simp only [distinctKeys_cons_iff] at hl
     specialize ih hl.1
     specialize hf ⟨k', v⟩
@@ -5440,10 +5441,10 @@ theorem getKey?_filter_key [BEq α] [EquivBEq α]
     specialize ih hl.tail
     simp only [getKey?_cons, List.filter_cons]
     split
-    · simp only [getKey?_cons, ih, cond_eq_if, apply_ite (Option.filter f), Option.filter_some,
+    · simp only [getKey?_cons, ih, cond_eq_ite, apply_ite (Option.filter f), Option.filter_some,
         ‹f k'›, ↓reduceIte]
     · replace hl := hl.containsKey_eq_false
-      simp only [ih, cond_eq_if]
+      simp only [ih, cond_eq_ite]
       split
       · rw [containsKey_congr ‹_›] at hl
         simp only [getKey?_eq_none hl, Option.filter_none, Option.filter_some, eq_false ‹_›,
@@ -6154,7 +6155,7 @@ theorem minKey?_eq_some_iff_mem_and_forall [Ord α] [LawfulEqOrd α] [TransOrd 
     exact ⟨containsKey_of_mem hm, hcmp⟩
   · rintro ⟨hc, hle⟩
     have heq := beq_iff_eq.mp <| getKey_eq_getEntry_fst (α := α) ▸ getKey_beq hc
-    refine ⟨getEntry k l hc, ⟨mem_getEntry hc, ?_⟩, heq⟩
+    refine ⟨getEntry k l hc, ⟨getEntry_mem, ?_⟩, heq⟩
     intro k' hk'
     rw [heq]
     exact hle _ hk'
@@ -6233,7 +6234,7 @@ theorem replaceEntry_eq_map [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k
   induction l with
   | nil => rfl
   | cons e es ih =>
-    simp only [replaceEntry, cond_eq_if, List.map_cons]
+    simp only [replaceEntry, cond_eq_ite, List.map_cons]
     split
     · rename_i heq
       simp only [List.cons.injEq, true_and]
diff --git a/src/Std/Sat/AIG/CNF.lean b/src/Std/Sat/AIG/CNF.lean
index 178824c9cc..b2187b84ca 100644
--- a/src/Std/Sat/AIG/CNF.lean
+++ b/src/Std/Sat/AIG/CNF.lean
@@ -527,24 +527,25 @@ The CNF within the state is unsat.
 def State.Unsat (state : State aig) : Prop :=
   state.cnf.Unsat
 
-theorem State.sat_def (assign : CNFVar aig → Bool) (state : State aig) :
-    state.Sat assign ↔ state.cnf.Sat assign := by
-  rfl
-
-theorem State.unsat_def (state : State aig) :
-    state.Unsat ↔ state.cnf.Unsat := by
-  rfl
-
 @[simp]
 theorem State.eval_eq : State.eval assign state = state.cnf.eval assign := by
   simp [State.eval]
 
 @[simp]
-theorem State.sat_iff : State.Sat assign state ↔ state.cnf.Sat assign := by
-  simp [State.sat_def]
+theorem State.sat_iff : State.Sat assign state ↔ state.cnf.Sat assign := by rfl
 
 @[simp]
-theorem State.unsat_iff : State.Unsat state ↔ state.cnf.Unsat := by simp [State.unsat_def]
+theorem State.unsat_iff : State.Unsat state ↔ state.cnf.Unsat := by rfl
+
+@[deprecated State.sat_iff (since := "2025-10-29")]
+theorem State.sat_def (assign : CNFVar aig → Bool) (state : State aig) :
+    state.Sat assign ↔ state.cnf.Sat assign := by
+  rfl
+
+@[deprecated State.unsat_iff (since := "2025-10-29")]
+theorem State.unsat_def (state : State aig) :
+    state.Unsat ↔ state.cnf.Unsat := by
+  rfl
 
 end toCNF
 
diff --git a/src/Std/Sat/AIG/RefVecOperator/Map.lean b/src/Std/Sat/AIG/RefVecOperator/Map.lean
index eb5a921521..c8c219e82f 100644
--- a/src/Std/Sat/AIG/RefVecOperator/Map.lean
+++ b/src/Std/Sat/AIG/RefVecOperator/Map.lean
@@ -28,6 +28,7 @@ class LawfulMapOperator (α : Type) [Hashable α] [DecidableEq α]
 
 namespace LawfulMapOperator
 
+@[deprecated chainable (since := "2025-10-29")]
 theorem denote_prefix_cast_ref {aig : AIG α} {input1 input2 : Ref aig}
     {f : (aig : AIG α) → Ref aig → Entrypoint α} [LawfulOperator α Ref f] [LawfulMapOperator α f]
     {h} :
diff --git a/src/Std/Sat/AIG/RefVecOperator/Zip.lean b/src/Std/Sat/AIG/RefVecOperator/Zip.lean
index 46daccb75a..87d8e1916f 100644
--- a/src/Std/Sat/AIG/RefVecOperator/Zip.lean
+++ b/src/Std/Sat/AIG/RefVecOperator/Zip.lean
@@ -28,6 +28,7 @@ class LawfulZipOperator (α : Type) [Hashable α] [DecidableEq α]
 
 namespace LawfulZipOperator
 
+@[deprecated chainable (since := "2025-10-29")]
 theorem denote_prefix_cast_ref {aig : AIG α} {input1 input2 : BinaryInput aig}
     {f : (aig : AIG α) → BinaryInput aig → Entrypoint α} [LawfulOperator α BinaryInput f]
     [LawfulZipOperator α f] {h} :
diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
index 066473a639..b5ef91c6e7 100644
--- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
@@ -454,7 +454,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.neg_one_eq_allOnes, cond_eq_if]
+  simp [BitVec.neg_one_eq_allOnes, cond_eq_ite]
   assumption
 
 theorem BitVec.signExtend_elim' {v : Nat} {x : BitVec v} {w : Nat} (h : w ≤ v) :
diff --git a/src/Std/Tactic/BVDecide/Normalize/Bool.lean b/src/Std/Tactic/BVDecide/Normalize/Bool.lean
index 3c87687458..6c3a994c56 100644
--- a/src/Std/Tactic/BVDecide/Normalize/Bool.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/Bool.lean
@@ -42,7 +42,7 @@ attribute [bv_normalize] Bool.cond_not
 
 @[bv_normalize]
 theorem if_eq_cond {b : Bool} {x y : α} : (if b = true then x else y) = (bif b then x else y) := by
-  rw [cond_eq_if]
+  rw [cond_eq_ite]
 
 @[bv_normalize]
 theorem Bool.not_xor : ∀ (a b : Bool), (!(a ^^ b)) = (a == b) := by decide
diff --git a/tests/lean/grind/experiments/bitvec.lean b/tests/lean/grind/experiments/bitvec.lean
index 2b7d1f3094..0c36441602 100644
--- a/tests/lean/grind/experiments/bitvec.lean
+++ b/tests/lean/grind/experiments/bitvec.lean
@@ -396,7 +396,7 @@ theorem getElem?_zero_ofNat_one : (BitVec.ofNat (w+1) 1)[0]? = some true := by
 
 -- This does not need to be a `@[simp]` theorem as it is already handled by `getElem?_eq_getElem`.
 theorem getElem?_zero_ofBool (b : Bool) : (ofBool b)[0]? = some b := by
-  simp only [ofBool, ofNat_eq_ofNat, cond_eq_if]
+  simp only [ofBool, ofNat_eq_ofNat, cond_eq_ite]
   split <;> simp_all
 
 @[simp] theorem getElem_zero_ofBool (b : Bool) : (ofBool b)[0] = b := by
@@ -2687,7 +2687,7 @@ theorem setWidth_append {x : BitVec w} {y : BitVec v} :
 
 @[simp] theorem not_append {x : BitVec w} {y : BitVec v} : ~~~ (x ++ y) = (~~~ x) ++ (~~~ y) := by
   ext i
-  simp only [getElem_not, getElem_append, cond_eq_if]
+  simp only [getElem_not, getElem_append, cond_eq_ite]
   split
   · simp_all
   · simp_all
diff --git a/tests/lean/run/grind_bitvec2.lean b/tests/lean/run/grind_bitvec2.lean
index fc518c4747..c1bccd0c62 100644
--- a/tests/lean/run/grind_bitvec2.lean
+++ b/tests/lean/run/grind_bitvec2.lean
@@ -312,7 +312,7 @@ theorem getElem?_zero_ofNat_one : (BitVec.ofNat (w+1) 1)[0]? = some true := by g
 -- This does not need to be a `@[simp]` or `@[grind]` theorem as it is already handled by
 -- `getElem_zero_ofBool` and `getElem?_eq_getElem`.
 theorem getElem?_zero_ofBool (b : Bool) : (ofBool b)[0]? = some b := by
-  simp only [ofBool, ofNat_eq_ofNat, cond_eq_if]
+  simp only [ofBool, ofNat_eq_ofNat, cond_eq_ite]
   split <;>
     -- FIXME: `grind` gives a kernel type mismatch here:
     -- (kernel) application type mismatch