diff --git a/src/Init/Data/Int/DivMod.lean b/src/Init/Data/Int/DivMod.lean
index 10c6ef4b3796..8e2ef7873f21 100644
--- a/src/Init/Data/Int/DivMod.lean
+++ b/src/Init/Data/Int/DivMod.lean
@@ -16,83 +16,99 @@ There are three main conventions for integer division,
 referred here as the E, F, T rounding conventions.
 All three pairs satisfy the identity `x % y + (x / y) * y = x` unconditionally,
 and satisfy `x / 0 = 0` and `x % 0 = x`.
+
+### Historical notes
+In early versions of Lean, the typeclasses provided by `/` and `%`
+were defined in terms of `tdiv` and `tmod`, and these were named simply as `div` and `mod`.
+
+However we decided it was better to use `ediv` and `emod`,
+as they are consistent with the conventions used in SMTLib, Mathlib,
+and often mathematical reasoning is easier with these conventions.
+
+At that time, we did not rename `div` and `mod` to `tdiv` and `tmod` (along with all their lemma).
+In September 2024, we decided to do this rename (with deprecations in place),
+and later we intend to rename `ediv` and `emod` to `div` and `mod`, as nearly all users will only
+ever need to use these functions and their associated lemmas.
 -/
 
 /-! ### T-rounding division -/
 
 /--
-`div` uses the [*"T-rounding"*][t-rounding]
+`tdiv` uses the [*"T-rounding"*][t-rounding]
 (**T**runcation-rounding) convention, meaning that it rounds toward
 zero. Also note that division by zero is defined to equal zero.
 
   The relation between integer division and modulo is found in
-  `Int.mod_add_div` which states that
-  `a % b + b * (a / b) = a`, unconditionally.
+  `Int.tmod_add_tdiv` which states that
+  `tmod a b + b * (tdiv a b) = a`, unconditionally.
 
-  [t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862 [theo
-  mod_add_div]:
-  https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.mod_add_div#doc
+  [t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862
+  [theo tmod_add_tdiv]: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.tmod_add_tdiv#doc
 
   Examples:
 
   ```
-  #eval (7 : Int).div (0 : Int) -- 0
-  #eval (0 : Int).div (7 : Int) -- 0
-
-  #eval (12 : Int).div (6 : Int) -- 2
-  #eval (12 : Int).div (-6 : Int) -- -2
-  #eval (-12 : Int).div (6 : Int) -- -2
-  #eval (-12 : Int).div (-6 : Int) -- 2
-
-  #eval (12 : Int).div (7 : Int) -- 1
-  #eval (12 : Int).div (-7 : Int) -- -1
-  #eval (-12 : Int).div (7 : Int) -- -1
-  #eval (-12 : Int).div (-7 : Int) -- 1
+  #eval (7 : Int).tdiv (0 : Int) -- 0
+  #eval (0 : Int).tdiv (7 : Int) -- 0
+
+  #eval (12 : Int).tdiv (6 : Int) -- 2
+  #eval (12 : Int).tdiv (-6 : Int) -- -2
+  #eval (-12 : Int).tdiv (6 : Int) -- -2
+  #eval (-12 : Int).tdiv (-6 : Int) -- 2
+
+  #eval (12 : Int).tdiv (7 : Int) -- 1
+  #eval (12 : Int).tdiv (-7 : Int) -- -1
+  #eval (-12 : Int).tdiv (7 : Int) -- -1
+  #eval (-12 : Int).tdiv (-7 : Int) -- 1
   ```
 
   Implemented by efficient native code.
 -/
 @[extern "lean_int_div"]
-def div : (@& Int) → (@& Int) → Int
+def tdiv : (@& Int) → (@& Int) → Int
   | ofNat m, ofNat n =>  ofNat (m / n)
   | ofNat m, -[n +1] => -ofNat (m / succ n)
   | -[m +1], ofNat n => -ofNat (succ m / n)
   | -[m +1], -[n +1] =>  ofNat (succ m / succ n)
 
+@[deprecated tdiv (since := "2024-09-11")] abbrev div := tdiv
+
 /-- Integer modulo. This function uses the
   [*"T-rounding"*][t-rounding] (**T**runcation-rounding) convention
-  to pair with `Int.div`, meaning that `a % b + b * (a / b) = a`
-  unconditionally (see [`Int.mod_add_div`][theo mod_add_div]). In
+  to pair with `Int.tdiv`, meaning that `tmod a b + b * (tdiv a b) = a`
+  unconditionally (see [`Int.tmod_add_tdiv`][theo tmod_add_tdiv]). In
   particular, `a % 0 = a`.
 
   [t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862
-  [theo mod_add_div]: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.mod_add_div#doc
+  [theo tmod_add_tdiv]: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.tmod_add_tdiv#doc
 
   Examples:
 
   ```
-  #eval (7 : Int).mod (0 : Int) -- 7
-  #eval (0 : Int).mod (7 : Int) -- 0
-
-  #eval (12 : Int).mod (6 : Int) -- 0
-  #eval (12 : Int).mod (-6 : Int) -- 0
-  #eval (-12 : Int).mod (6 : Int) -- 0
-  #eval (-12 : Int).mod (-6 : Int) -- 0
-
-  #eval (12 : Int).mod (7 : Int) -- 5
-  #eval (12 : Int).mod (-7 : Int) -- 5
-  #eval (-12 : Int).mod (7 : Int) -- -5
-  #eval (-12 : Int).mod (-7 : Int) -- -5
+  #eval (7 : Int).tmod (0 : Int) -- 7
+  #eval (0 : Int).tmod (7 : Int) -- 0
+
+  #eval (12 : Int).tmod (6 : Int) -- 0
+  #eval (12 : Int).tmod (-6 : Int) -- 0
+  #eval (-12 : Int).tmod (6 : Int) -- 0
+  #eval (-12 : Int).tmod (-6 : Int) -- 0
+
+  #eval (12 : Int).tmod (7 : Int) -- 5
+  #eval (12 : Int).tmod (-7 : Int) -- 5
+  #eval (-12 : Int).tmod (7 : Int) -- -5
+  #eval (-12 : Int).tmod (-7 : Int) -- -5
   ```
 
   Implemented by efficient native code. -/
 @[extern "lean_int_mod"]
-def mod : (@& Int) → (@& Int) → Int
+def tmod : (@& Int) → (@& Int) → Int
   | ofNat m, ofNat n =>  ofNat (m % n)
   | ofNat m, -[n +1] =>  ofNat (m % succ n)
   | -[m +1], ofNat n => -ofNat (succ m % n)
   | -[m +1], -[n +1] => -ofNat (succ m % succ n)
 
+@[deprecated tmod (since := "2024-09-11")] abbrev mod := tmod
+
 /-! ### F-rounding division
 This pair satisfies `fdiv x y = floor (x / y)`.
 -/
@@ -233,7 +249,9 @@ instance : Mod Int where
 
 @[simp, norm_cast] theorem ofNat_ediv (m n : Nat) : (↑(m / n) : Int) = ↑m / ↑n := rfl
 
-theorem ofNat_div (m n : Nat) : ↑(m / n) = div ↑m ↑n := rfl
+theorem ofNat_tdiv (m n : Nat) : ↑(m / n) = tdiv ↑m ↑n := rfl
+
+@[deprecated ofNat_tdiv (since := "2024-09-11")] abbrev ofNat_div := ofNat_tdiv
 
 theorem ofNat_fdiv : ∀ m n : Nat, ↑(m / n) = fdiv ↑m ↑n
   | 0, _ => by simp [fdiv]
diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean
index a99d0b66a870..cfab5e8a832b 100644
--- a/src/Init/Data/Int/DivModLemmas.lean
+++ b/src/Init/Data/Int/DivModLemmas.lean
@@ -137,12 +137,12 @@ theorem eq_one_of_mul_eq_one_left {a b : Int} (H : 0 ≤ b) (H' : a * b = 1) : b
   | ofNat _ => show ofNat _ = _ by simp
   | -[_+1] => rfl
 
-@[simp] protected theorem zero_div : ∀ b : Int, div 0 b = 0
+@[simp] protected theorem zero_tdiv : ∀ b : Int, tdiv 0 b = 0
   | ofNat _ => show ofNat _ = _ by simp
   | -[_+1] => show -ofNat _ = _ by simp
 
 unseal Nat.div in
-@[simp] protected theorem div_zero : ∀ a : Int, div a 0 = 0
+@[simp] protected theorem tdiv_zero : ∀ a : Int, tdiv a 0 = 0
   | ofNat _ => show ofNat _ = _ by simp
   | -[_+1] => rfl
 
@@ -156,16 +156,17 @@ unseal Nat.div in
 
 /-! ### div equivalences  -/
 
-theorem div_eq_ediv : ∀ {a b : Int}, 0 ≤ a → 0 ≤ b → a.div b = a / b
+theorem tdiv_eq_ediv : ∀ {a b : Int}, 0 ≤ a → 0 ≤ b → a.tdiv b = a / b
   | 0, _, _, _ | _, 0, _, _ => by simp
   | succ _, succ _, _, _ => rfl
 
+
 theorem fdiv_eq_ediv : ∀ (a : Int) {b : Int}, 0 ≤ b → fdiv a b = a / b
   | 0, _, _ | -[_+1], 0, _ => by simp
   | succ _, ofNat _, _ | -[_+1], succ _, _ => rfl
 
-theorem fdiv_eq_div {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : fdiv a b = div a b :=
-  div_eq_ediv Ha Hb ▸ fdiv_eq_ediv _ Hb
+theorem fdiv_eq_tdiv {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : fdiv a b = tdiv a b :=
+  tdiv_eq_ediv Ha Hb ▸ fdiv_eq_ediv _ Hb
 
 /-! ### mod zero -/
 
@@ -175,9 +176,9 @@ theorem fdiv_eq_div {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : fdiv a b = div a
   | ofNat _ => congrArg ofNat <| Nat.mod_zero _
   | -[_+1]  => congrArg negSucc <| Nat.mod_zero _
 
-@[simp] theorem zero_mod (b : Int) : mod 0 b = 0 := by cases b <;> simp [mod]
+@[simp] theorem zero_tmod (b : Int) : tmod 0 b = 0 := by cases b <;> simp [tmod]
 
-@[simp] theorem mod_zero : ∀ a : Int, mod a 0 = a
+@[simp] theorem tmod_zero : ∀ a : Int, tmod a 0 = a
   | ofNat _ => congrArg ofNat <| Nat.mod_zero _
   | -[_+1] => congrArg (fun n => -ofNat n) <| Nat.mod_zero _
 
@@ -221,7 +222,7 @@ theorem ediv_add_emod' (a b : Int) : a / b * b + a % b = a := by
 theorem emod_def (a b : Int) : a % b = a - b * (a / b) := by
   rw [← Int.add_sub_cancel (a % b), emod_add_ediv]
 
-theorem mod_add_div : ∀ a b : Int, mod a b + b * (a.div b) = a
+theorem tmod_add_tdiv : ∀ a b : Int, tmod a b + b * (a.tdiv b) = a
   | ofNat _, ofNat _ => congrArg ofNat (Nat.mod_add_div ..)
   | ofNat m, -[n+1] => by
     show (m % succ n + -↑(succ n) * -↑(m / succ n) : Int) = m
@@ -238,17 +239,17 @@ theorem mod_add_div : ∀ a b : Int, mod a b + b * (a.div b) = a
     rw [Int.neg_mul, ← Int.neg_add]
     exact congrArg (-ofNat ·) (Nat.mod_add_div ..)
 
-theorem div_add_mod (a b : Int) : b * a.div b + mod a b = a := by
-  rw [Int.add_comm]; apply mod_add_div ..
+theorem tdiv_add_tmod (a b : Int) : b * a.tdiv b + tmod a b = a := by
+  rw [Int.add_comm]; apply tmod_add_tdiv ..
 
-theorem mod_add_div' (m k : Int) : mod m k + m.div k * k = m := by
-  rw [Int.mul_comm]; apply mod_add_div
+theorem tmod_add_tdiv' (m k : Int) : tmod m k + m.tdiv k * k = m := by
+  rw [Int.mul_comm]; apply tmod_add_tdiv
 
-theorem div_add_mod' (m k : Int) : m.div k * k + mod m k = m := by
-  rw [Int.mul_comm]; apply div_add_mod
+theorem tdiv_add_tmod' (m k : Int) : m.tdiv k * k + tmod m k = m := by
+  rw [Int.mul_comm]; apply tdiv_add_tmod
 
-theorem mod_def (a b : Int) : mod a b = a - b * a.div b := by
-  rw [← Int.add_sub_cancel (mod a b), mod_add_div]
+theorem tmod_def (a b : Int) : tmod a b = a - b * a.tdiv b := by
+  rw [← Int.add_sub_cancel (tmod a b), tmod_add_tdiv]
 
 theorem fmod_add_fdiv : ∀ a b : Int, a.fmod b + b * a.fdiv b = a
   | 0, ofNat _ | 0, -[_+1] => congrArg ofNat <| by simp
@@ -278,11 +279,11 @@ theorem fmod_def (a b : Int) : a.fmod b = a - b * a.fdiv b := by
 theorem fmod_eq_emod (a : Int) {b : Int} (hb : 0 ≤ b) : fmod a b = a % b := by
   simp [fmod_def, emod_def, fdiv_eq_ediv _ hb]
 
-theorem mod_eq_emod {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : mod a b = a % b := by
-  simp [emod_def, mod_def, div_eq_ediv ha hb]
+theorem tmod_eq_emod {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : tmod a b = a % b := by
+  simp [emod_def, tmod_def, tdiv_eq_ediv ha hb]
 
-theorem fmod_eq_mod {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : fmod a b = mod a b :=
-  mod_eq_emod Ha Hb ▸ fmod_eq_emod _ Hb
+theorem fmod_eq_tmod {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : fmod a b = tmod a b :=
+  tmod_eq_emod Ha Hb ▸ fmod_eq_emod _ Hb
 
 /-! ### `/` ediv -/
 
@@ -297,7 +298,7 @@ theorem ediv_neg' {a b : Int} (Ha : a < 0) (Hb : 0 < b) : a / b < 0 :=
 
 protected theorem div_def (a b : Int) : a / b = Int.ediv a b := rfl
 
-theorem negSucc_ediv (m : Nat) {b : Int} (H : 0 < b) : -[m+1] / b = -(div m b + 1) :=
+theorem negSucc_ediv (m : Nat) {b : Int} (H : 0 < b) : -[m+1] / b = -(ediv m b + 1) :=
   match b, eq_succ_of_zero_lt H with
   | _, ⟨_, rfl⟩ => rfl
 
@@ -796,191 +797,191 @@ theorem ediv_eq_ediv_of_mul_eq_mul {a b c d : Int}
   Int.ediv_eq_of_eq_mul_right H3 <| by
     rw [← Int.mul_ediv_assoc _ H2]; exact (Int.ediv_eq_of_eq_mul_left H4 H5.symm).symm
 
-/-! ### div -/
+/-! ### tdiv -/
 
-@[simp] protected theorem div_one : ∀ a : Int, a.div 1 = a
+@[simp] protected theorem tdiv_one : ∀ a : Int, a.tdiv 1 = a
   | (n:Nat) => congrArg ofNat (Nat.div_one _)
-  | -[n+1] => by simp [Int.div, neg_ofNat_succ]; rfl
+  | -[n+1] => by simp [Int.tdiv, neg_ofNat_succ]; rfl
 
 unseal Nat.div in
-@[simp] protected theorem div_neg : ∀ a b : Int, a.div (-b) = -(a.div b)
+@[simp] protected theorem tdiv_neg : ∀ a b : Int, a.tdiv (-b) = -(a.tdiv b)
   | ofNat m, 0 => show ofNat (m / 0) = -↑(m / 0) by rw [Nat.div_zero]; rfl
   | ofNat m, -[n+1] | -[m+1], succ n => (Int.neg_neg _).symm
   | ofNat m, succ n | -[m+1], 0 | -[m+1], -[n+1] => rfl
 
 unseal Nat.div in
-@[simp] protected theorem neg_div : ∀ a b : Int, (-a).div b = -(a.div b)
+@[simp] protected theorem neg_tdiv : ∀ a b : Int, (-a).tdiv b = -(a.tdiv b)
   | 0, n => by simp [Int.neg_zero]
   | succ m, (n:Nat) | -[m+1], 0 | -[m+1], -[n+1] => rfl
   | succ m, -[n+1] | -[m+1], succ n => (Int.neg_neg _).symm
 
-protected theorem neg_div_neg (a b : Int) : (-a).div (-b) = a.div b := by
-  simp [Int.div_neg, Int.neg_div, Int.neg_neg]
+protected theorem neg_tdiv_neg (a b : Int) : (-a).tdiv (-b) = a.tdiv b := by
+  simp [Int.tdiv_neg, Int.neg_tdiv, Int.neg_neg]
 
-protected theorem div_nonneg {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a.div b :=
+protected theorem tdiv_nonneg {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a.tdiv b :=
   match a, b, eq_ofNat_of_zero_le Ha, eq_ofNat_of_zero_le Hb with
   | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => ofNat_zero_le _
 
-protected theorem div_nonpos {a b : Int} (Ha : 0 ≤ a) (Hb : b ≤ 0) : a.div b ≤ 0 :=
-  Int.nonpos_of_neg_nonneg <| Int.div_neg .. ▸ Int.div_nonneg Ha (Int.neg_nonneg_of_nonpos Hb)
+protected theorem tdiv_nonpos {a b : Int} (Ha : 0 ≤ a) (Hb : b ≤ 0) : a.tdiv b ≤ 0 :=
+  Int.nonpos_of_neg_nonneg <| Int.tdiv_neg .. ▸ Int.tdiv_nonneg Ha (Int.neg_nonneg_of_nonpos Hb)
 
-theorem div_eq_zero_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : a.div b = 0 :=
+theorem tdiv_eq_zero_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : a.tdiv b = 0 :=
   match a, b, eq_ofNat_of_zero_le H1, eq_succ_of_zero_lt (Int.lt_of_le_of_lt H1 H2) with
   | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => congrArg Nat.cast <| Nat.div_eq_of_lt <| ofNat_lt.1 H2
 
-@[simp] protected theorem mul_div_cancel (a : Int) {b : Int} (H : b ≠ 0) : (a * b).div b = a :=
-  have : ∀ {a b : Nat}, (b : Int) ≠ 0 → (div (a * b) b : Int) = a := fun H => by
-    rw [← ofNat_mul, ← ofNat_div,
+@[simp] protected theorem mul_tdiv_cancel (a : Int) {b : Int} (H : b ≠ 0) : (a * b).tdiv b = a :=
+  have : ∀ {a b : Nat}, (b : Int) ≠ 0 → (tdiv (a * b) b : Int) = a := fun H => by
+    rw [← ofNat_mul, ← ofNat_tdiv,
       Nat.mul_div_cancel _ <| Nat.pos_of_ne_zero <| Int.ofNat_ne_zero.1 H]
   match a, b, a.eq_nat_or_neg, b.eq_nat_or_neg with
   | _, _, ⟨a, .inl rfl⟩, ⟨b, .inl rfl⟩ => this H
   | _, _, ⟨a, .inl rfl⟩, ⟨b, .inr rfl⟩ => by
-    rw [Int.mul_neg, Int.neg_div, Int.div_neg, Int.neg_neg,
+    rw [Int.mul_neg, Int.neg_tdiv, Int.tdiv_neg, Int.neg_neg,
       this (Int.neg_ne_zero.1 H)]
-  | _, _, ⟨a, .inr rfl⟩, ⟨b, .inl rfl⟩ => by rw [Int.neg_mul, Int.neg_div, this H]
+  | _, _, ⟨a, .inr rfl⟩, ⟨b, .inl rfl⟩ => by rw [Int.neg_mul, Int.neg_tdiv, this H]
   | _, _, ⟨a, .inr rfl⟩, ⟨b, .inr rfl⟩ => by
-    rw [Int.neg_mul_neg, Int.div_neg, this (Int.neg_ne_zero.1 H)]
+    rw [Int.neg_mul_neg, Int.tdiv_neg, this (Int.neg_ne_zero.1 H)]
 
-@[simp] protected theorem mul_div_cancel_left (b : Int) (H : a ≠ 0) : (a * b).div a = b :=
-  Int.mul_comm .. ▸ Int.mul_div_cancel _ H
+@[simp] protected theorem mul_tdiv_cancel_left (b : Int) (H : a ≠ 0) : (a * b).tdiv a = b :=
+  Int.mul_comm .. ▸ Int.mul_tdiv_cancel _ H
 
-@[simp] protected theorem div_self {a : Int} (H : a ≠ 0) : a.div a = 1 := by
-  have := Int.mul_div_cancel 1 H; rwa [Int.one_mul] at this
+@[simp] protected theorem tdiv_self {a : Int} (H : a ≠ 0) : a.tdiv a = 1 := by
+  have := Int.mul_tdiv_cancel 1 H; rwa [Int.one_mul] at this
 
-theorem mul_div_cancel_of_mod_eq_zero {a b : Int} (H : a.mod b = 0) : b * (a.div b) = a := by
-  have := mod_add_div a b; rwa [H, Int.zero_add] at this
+theorem mul_tdiv_cancel_of_tmod_eq_zero {a b : Int} (H : a.tmod b = 0) : b * (a.tdiv b) = a := by
+  have := tmod_add_tdiv a b; rwa [H, Int.zero_add] at this
 
-theorem div_mul_cancel_of_mod_eq_zero {a b : Int} (H : a.mod b = 0) : a.div b * b = a := by
-  rw [Int.mul_comm, mul_div_cancel_of_mod_eq_zero H]
+theorem tdiv_mul_cancel_of_tmod_eq_zero {a b : Int} (H : a.tmod b = 0) : a.tdiv b * b = a := by
+  rw [Int.mul_comm, mul_tdiv_cancel_of_tmod_eq_zero H]
 
-theorem dvd_of_mod_eq_zero {a b : Int} (H : mod b a = 0) : a ∣ b :=
-  ⟨b.div a, (mul_div_cancel_of_mod_eq_zero H).symm⟩
+theorem dvd_of_tmod_eq_zero {a b : Int} (H : tmod b a = 0) : a ∣ b :=
+  ⟨b.tdiv a, (mul_tdiv_cancel_of_tmod_eq_zero H).symm⟩
 
-protected theorem mul_div_assoc (a : Int) : ∀ {b c : Int}, c ∣ b → (a * b).div c = a * (b.div c)
+protected theorem mul_tdiv_assoc (a : Int) : ∀ {b c : Int}, c ∣ b → (a * b).tdiv c = a * (b.tdiv c)
   | _, c, ⟨d, rfl⟩ =>
     if cz : c = 0 then by simp [cz, Int.mul_zero] else by
-      rw [Int.mul_left_comm, Int.mul_div_cancel_left _ cz, Int.mul_div_cancel_left _ cz]
+      rw [Int.mul_left_comm, Int.mul_tdiv_cancel_left _ cz, Int.mul_tdiv_cancel_left _ cz]
 
-protected theorem mul_div_assoc' (b : Int) {a c : Int} (h : c ∣ a) :
-    (a * b).div c = a.div c * b := by
-  rw [Int.mul_comm, Int.mul_div_assoc _ h, Int.mul_comm]
+protected theorem mul_tdiv_assoc' (b : Int) {a c : Int} (h : c ∣ a) :
+    (a * b).tdiv c = a.tdiv c * b := by
+  rw [Int.mul_comm, Int.mul_tdiv_assoc _ h, Int.mul_comm]
 
-theorem div_dvd_div : ∀ {a b c : Int}, a ∣ b → b ∣ c → b.div a ∣ c.div a
+theorem tdiv_dvd_tdiv : ∀ {a b c : Int}, a ∣ b → b ∣ c → b.tdiv a ∣ c.tdiv a
   | a, _, _, ⟨b, rfl⟩, ⟨c, rfl⟩ => by
     by_cases az : a = 0
     · simp [az]
-    · rw [Int.mul_div_cancel_left _ az, Int.mul_assoc, Int.mul_div_cancel_left _ az]
+    · rw [Int.mul_tdiv_cancel_left _ az, Int.mul_assoc, Int.mul_tdiv_cancel_left _ az]
       apply Int.dvd_mul_right
 
-@[simp] theorem natAbs_div (a b : Int) : natAbs (a.div b) = (natAbs a).div (natAbs b) :=
+@[simp] theorem natAbs_tdiv (a b : Int) : natAbs (a.tdiv b) = (natAbs a).div (natAbs b) :=
   match a, b, eq_nat_or_neg a, eq_nat_or_neg b with
   | _, _, ⟨_, .inl rfl⟩, ⟨_, .inl rfl⟩ => rfl
-  | _, _, ⟨_, .inl rfl⟩, ⟨_, .inr rfl⟩ => by rw [Int.div_neg, natAbs_neg, natAbs_neg]; rfl
-  | _, _, ⟨_, .inr rfl⟩, ⟨_, .inl rfl⟩ => by rw [Int.neg_div, natAbs_neg, natAbs_neg]; rfl
-  | _, _, ⟨_, .inr rfl⟩, ⟨_, .inr rfl⟩ => by rw [Int.neg_div_neg, natAbs_neg, natAbs_neg]; rfl
+  | _, _, ⟨_, .inl rfl⟩, ⟨_, .inr rfl⟩ => by rw [Int.tdiv_neg, natAbs_neg, natAbs_neg]; rfl
+  | _, _, ⟨_, .inr rfl⟩, ⟨_, .inl rfl⟩ => by rw [Int.neg_tdiv, natAbs_neg, natAbs_neg]; rfl
+  | _, _, ⟨_, .inr rfl⟩, ⟨_, .inr rfl⟩ => by rw [Int.neg_tdiv_neg, natAbs_neg, natAbs_neg]; rfl
 
-protected theorem div_eq_of_eq_mul_right {a b c : Int}
-    (H1 : b ≠ 0) (H2 : a = b * c) : a.div b = c := by rw [H2, Int.mul_div_cancel_left _ H1]
+protected theorem tdiv_eq_of_eq_mul_right {a b c : Int}
+    (H1 : b ≠ 0) (H2 : a = b * c) : a.tdiv b = c := by rw [H2, Int.mul_tdiv_cancel_left _ H1]
 
-protected theorem eq_div_of_mul_eq_right {a b c : Int}
-    (H1 : a ≠ 0) (H2 : a * b = c) : b = c.div a :=
-  (Int.div_eq_of_eq_mul_right H1 H2.symm).symm
+protected theorem eq_tdiv_of_mul_eq_right {a b c : Int}
+    (H1 : a ≠ 0) (H2 : a * b = c) : b = c.tdiv a :=
+  (Int.tdiv_eq_of_eq_mul_right H1 H2.symm).symm
 
 /-! ### (t-)mod -/
 
-theorem ofNat_mod (m n : Nat) : (↑(m % n) : Int) = mod m n := rfl
+theorem ofNat_tmod (m n : Nat) : (↑(m % n) : Int) = tmod m n := rfl
 
-@[simp] theorem mod_one (a : Int) : mod a 1 = 0 := by
-  simp [mod_def, Int.div_one, Int.one_mul, Int.sub_self]
+@[simp] theorem tmod_one (a : Int) : tmod a 1 = 0 := by
+  simp [tmod_def, Int.tdiv_one, Int.one_mul, Int.sub_self]
 
-theorem mod_eq_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : mod a b = a := by
-  rw [mod_eq_emod H1 (Int.le_trans H1 (Int.le_of_lt H2)), emod_eq_of_lt H1 H2]
+theorem tmod_eq_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : tmod a b = a := by
+  rw [tmod_eq_emod H1 (Int.le_trans H1 (Int.le_of_lt H2)), emod_eq_of_lt H1 H2]
 
-theorem mod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : mod a b < b :=
+theorem tmod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : tmod a b < b :=
   match a, b, eq_succ_of_zero_lt H with
   | ofNat _, _, ⟨n, rfl⟩ => ofNat_lt.2 <| Nat.mod_lt _ n.succ_pos
   | -[_+1], _, ⟨n, rfl⟩ => Int.lt_of_le_of_lt
     (Int.neg_nonpos_of_nonneg <| Int.ofNat_nonneg _) (ofNat_pos.2 n.succ_pos)
 
-theorem mod_nonneg : ∀ {a : Int} (b : Int), 0 ≤ a → 0 ≤ mod a b
+theorem tmod_nonneg : ∀ {a : Int} (b : Int), 0 ≤ a → 0 ≤ tmod a b
   | ofNat _, -[_+1], _ | ofNat _, ofNat _, _ => ofNat_nonneg _
 
-@[simp] theorem mod_neg (a b : Int) : mod a (-b) = mod a b := by
-  rw [mod_def, mod_def, Int.div_neg, Int.neg_mul_neg]
+@[simp] theorem tmod_neg (a b : Int) : tmod a (-b) = tmod a b := by
+  rw [tmod_def, tmod_def, Int.tdiv_neg, Int.neg_mul_neg]
 
-@[simp] theorem mul_mod_left (a b : Int) : (a * b).mod b = 0 :=
+@[simp] theorem mul_tmod_left (a b : Int) : (a * b).tmod b = 0 :=
   if h : b = 0 then by simp [h, Int.mul_zero] else by
-    rw [Int.mod_def, Int.mul_div_cancel _ h, Int.mul_comm, Int.sub_self]
+    rw [Int.tmod_def, Int.mul_tdiv_cancel _ h, Int.mul_comm, Int.sub_self]
 
-@[simp] theorem mul_mod_right (a b : Int) : (a * b).mod a = 0 := by
-  rw [Int.mul_comm, mul_mod_left]
+@[simp] theorem mul_tmod_right (a b : Int) : (a * b).tmod a = 0 := by
+  rw [Int.mul_comm, mul_tmod_left]
 
-theorem mod_eq_zero_of_dvd : ∀ {a b : Int}, a ∣ b → mod b a = 0
-  | _, _, ⟨_, rfl⟩ => mul_mod_right ..
+theorem tmod_eq_zero_of_dvd : ∀ {a b : Int}, a ∣ b → tmod b a = 0
+  | _, _, ⟨_, rfl⟩ => mul_tmod_right ..
 
-theorem dvd_iff_mod_eq_zero {a b : Int} : a ∣ b ↔ mod b a = 0 :=
-  ⟨mod_eq_zero_of_dvd, dvd_of_mod_eq_zero⟩
+theorem dvd_iff_tmod_eq_zero {a b : Int} : a ∣ b ↔ tmod b a = 0 :=
+  ⟨tmod_eq_zero_of_dvd, dvd_of_tmod_eq_zero⟩
 
-@[simp] theorem neg_mul_mod_right (a b : Int) : (-(a * b)).mod a = 0 := by
-  rw [← dvd_iff_mod_eq_zero, Int.dvd_neg]
+@[simp] theorem neg_mul_tmod_right (a b : Int) : (-(a * b)).tmod a = 0 := by
+  rw [← dvd_iff_tmod_eq_zero, Int.dvd_neg]
   exact Int.dvd_mul_right a b
 
-@[simp] theorem neg_mul_mod_left (a b : Int) : (-(a * b)).mod b = 0 := by
-  rw [← dvd_iff_mod_eq_zero, Int.dvd_neg]
+@[simp] theorem neg_mul_tmod_left (a b : Int) : (-(a * b)).tmod b = 0 := by
+  rw [← dvd_iff_tmod_eq_zero, Int.dvd_neg]
   exact Int.dvd_mul_left a b
 
-protected theorem div_mul_cancel {a b : Int} (H : b ∣ a) : a.div b * b = a :=
-  div_mul_cancel_of_mod_eq_zero (mod_eq_zero_of_dvd H)
+protected theorem tdiv_mul_cancel {a b : Int} (H : b ∣ a) : a.tdiv b * b = a :=
+  tdiv_mul_cancel_of_tmod_eq_zero (tmod_eq_zero_of_dvd H)
 
-protected theorem mul_div_cancel' {a b : Int} (H : a ∣ b) : a * b.div a = b := by
-  rw [Int.mul_comm, Int.div_mul_cancel H]
+protected theorem mul_tdiv_cancel' {a b : Int} (H : a ∣ b) : a * b.tdiv a = b := by
+  rw [Int.mul_comm, Int.tdiv_mul_cancel H]
 
-protected theorem eq_mul_of_div_eq_right {a b c : Int}
-    (H1 : b ∣ a) (H2 : a.div b = c) : a = b * c := by rw [← H2, Int.mul_div_cancel' H1]
+protected theorem eq_mul_of_tdiv_eq_right {a b c : Int}
+    (H1 : b ∣ a) (H2 : a.tdiv b = c) : a = b * c := by rw [← H2, Int.mul_tdiv_cancel' H1]
 
-@[simp] theorem mod_self {a : Int} : a.mod a = 0 := by
-  have := mul_mod_left 1 a; rwa [Int.one_mul] at this
+@[simp] theorem tmod_self {a : Int} : a.tmod a = 0 := by
+  have := mul_tmod_left 1 a; rwa [Int.one_mul] at this
 
-@[simp] theorem neg_mod_self (a : Int) : (-a).mod a = 0 := by
-  rw [← dvd_iff_mod_eq_zero, Int.dvd_neg]
+@[simp] theorem neg_tmod_self (a : Int) : (-a).tmod a = 0 := by
+  rw [← dvd_iff_tmod_eq_zero, Int.dvd_neg]
   exact Int.dvd_refl a
 
-theorem lt_div_add_one_mul_self (a : Int) {b : Int} (H : 0 < b) : a < (a.div b + 1) * b := by
+theorem lt_tdiv_add_one_mul_self (a : Int) {b : Int} (H : 0 < b) : a < (a.tdiv b + 1) * b := by
   rw [Int.add_mul, Int.one_mul, Int.mul_comm]
-  exact Int.lt_add_of_sub_left_lt <| Int.mod_def .. ▸ mod_lt_of_pos _ H
+  exact Int.lt_add_of_sub_left_lt <| Int.tmod_def .. ▸ tmod_lt_of_pos _ H
 
-protected theorem div_eq_iff_eq_mul_right {a b c : Int}
-    (H : b ≠ 0) (H' : b ∣ a) : a.div b = c ↔ a = b * c :=
-  ⟨Int.eq_mul_of_div_eq_right H', Int.div_eq_of_eq_mul_right H⟩
+protected theorem tdiv_eq_iff_eq_mul_right {a b c : Int}
+    (H : b ≠ 0) (H' : b ∣ a) : a.tdiv b = c ↔ a = b * c :=
+  ⟨Int.eq_mul_of_tdiv_eq_right H', Int.tdiv_eq_of_eq_mul_right H⟩
 
-protected theorem div_eq_iff_eq_mul_left {a b c : Int}
-    (H : b ≠ 0) (H' : b ∣ a) : a.div b = c ↔ a = c * b := by
-  rw [Int.mul_comm]; exact Int.div_eq_iff_eq_mul_right H H'
+protected theorem tdiv_eq_iff_eq_mul_left {a b c : Int}
+    (H : b ≠ 0) (H' : b ∣ a) : a.tdiv b = c ↔ a = c * b := by
+  rw [Int.mul_comm]; exact Int.tdiv_eq_iff_eq_mul_right H H'
 
-protected theorem eq_mul_of_div_eq_left {a b c : Int}
-    (H1 : b ∣ a) (H2 : a.div b = c) : a = c * b := by
-  rw [Int.mul_comm, Int.eq_mul_of_div_eq_right H1 H2]
+protected theorem eq_mul_of_tdiv_eq_left {a b c : Int}
+    (H1 : b ∣ a) (H2 : a.tdiv b = c) : a = c * b := by
+  rw [Int.mul_comm, Int.eq_mul_of_tdiv_eq_right H1 H2]
 
-protected theorem div_eq_of_eq_mul_left {a b c : Int}
-    (H1 : b ≠ 0) (H2 : a = c * b) : a.div b = c :=
-  Int.div_eq_of_eq_mul_right H1 (by rw [Int.mul_comm, H2])
+protected theorem tdiv_eq_of_eq_mul_left {a b c : Int}
+    (H1 : b ≠ 0) (H2 : a = c * b) : a.tdiv b = c :=
+  Int.tdiv_eq_of_eq_mul_right H1 (by rw [Int.mul_comm, H2])
 
-protected theorem eq_zero_of_div_eq_zero {d n : Int} (h : d ∣ n) (H : n.div d = 0) : n = 0 := by
-  rw [← Int.mul_div_cancel' h, H, Int.mul_zero]
+protected theorem eq_zero_of_tdiv_eq_zero {d n : Int} (h : d ∣ n) (H : n.tdiv d = 0) : n = 0 := by
+  rw [← Int.mul_tdiv_cancel' h, H, Int.mul_zero]
 
-@[simp] protected theorem div_left_inj {a b d : Int}
-    (hda : d ∣ a) (hdb : d ∣ b) : a.div d = b.div d ↔ a = b := by
-  refine ⟨fun h => ?_, congrArg (div · d)⟩
-  rw [← Int.mul_div_cancel' hda, ← Int.mul_div_cancel' hdb, h]
+@[simp] protected theorem tdiv_left_inj {a b d : Int}
+    (hda : d ∣ a) (hdb : d ∣ b) : a.tdiv d = b.tdiv d ↔ a = b := by
+  refine ⟨fun h => ?_, congrArg (tdiv · d)⟩
+  rw [← Int.mul_tdiv_cancel' hda, ← Int.mul_tdiv_cancel' hdb, h]
 
-theorem div_sign : ∀ a b, a.div (sign b) = a * sign b
+theorem tdiv_sign : ∀ a b, a.tdiv (sign b) = a * sign b
   | _, succ _ => by simp [sign, Int.mul_one]
   | _, 0 => by simp [sign, Int.mul_zero]
   | _, -[_+1] => by simp [sign, Int.mul_neg, Int.mul_one]
 
-protected theorem sign_eq_div_abs (a : Int) : sign a = a.div (natAbs a) :=
+protected theorem sign_eq_tdiv_abs (a : Int) : sign a = a.tdiv (natAbs a) :=
   if az : a = 0 then by simp [az] else
-    (Int.div_eq_of_eq_mul_left (ofNat_ne_zero.2 <| natAbs_ne_zero.2 az)
+    (Int.tdiv_eq_of_eq_mul_left (ofNat_ne_zero.2 <| natAbs_ne_zero.2 az)
       (sign_mul_natAbs _).symm).symm
 
 /-! ### fdiv -/
@@ -1033,7 +1034,7 @@ theorem fmod_eq_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : a.fmod b = a :=
   rw [fmod_eq_emod _ (Int.le_trans H1 (Int.le_of_lt H2)), emod_eq_of_lt H1 H2]
 
 theorem fmod_nonneg {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a.fmod b :=
-  fmod_eq_mod ha hb ▸ mod_nonneg _ ha
+  fmod_eq_tmod ha hb ▸ tmod_nonneg _ ha
 
 theorem fmod_nonneg' (a : Int) {b : Int} (hb : 0 < b) : 0 ≤ a.fmod b :=
   fmod_eq_emod _ (Int.le_of_lt hb) ▸ emod_nonneg _ (Int.ne_of_lt hb).symm
@@ -1053,10 +1054,10 @@ theorem fmod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : a.fmod b < b :=
 
 /-! ### Theorems crossing div/mod versions -/
 
-theorem div_eq_ediv_of_dvd {a b : Int} (h : b ∣ a) : a.div b = a / b := by
+theorem tdiv_eq_ediv_of_dvd {a b : Int} (h : b ∣ a) : a.tdiv b = a / b := by
   by_cases b0 : b = 0
   · simp [b0]
-  · rw [Int.div_eq_iff_eq_mul_left b0 h, ← Int.ediv_eq_iff_eq_mul_left b0 h]
+  · rw [Int.tdiv_eq_iff_eq_mul_left b0 h, ← Int.ediv_eq_iff_eq_mul_left b0 h]
 
 theorem fdiv_eq_ediv_of_dvd : ∀ {a b : Int}, b ∣ a → a.fdiv b = a / b
   | _, b, ⟨c, rfl⟩ => by
@@ -1268,3 +1269,65 @@ theorem bmod_natAbs_plus_one (x : Int) (w : 1 < x.natAbs) : bmod x (x.natAbs + 1
           all_goals decide
     · exact ofNat_nonneg x
     · exact succ_ofNat_pos (x + 1)
+
+/-! ### Deprecations -/
+
+@[deprecated Int.zero_tdiv (since := "2024-09-11")] abbrev zero_div := @Int.zero_tdiv
+@[deprecated Int.tdiv_zero (since := "2024-09-11")] abbrev div_zero := @Int.tdiv_zero
+@[deprecated tdiv_eq_ediv (since := "2024-09-11")] abbrev div_eq_ediv := @tdiv_eq_ediv
+@[deprecated fdiv_eq_tdiv (since := "2024-09-11")] abbrev fdiv_eq_div := @fdiv_eq_tdiv
+@[deprecated zero_tmod (since := "2024-09-11")] abbrev zero_mod := @zero_tmod
+@[deprecated tmod_zero (since := "2024-09-11")] abbrev mod_zero := @tmod_zero
+@[deprecated tmod_add_tdiv (since := "2024-09-11")] abbrev mod_add_div := @tmod_add_tdiv
+@[deprecated tdiv_add_tmod (since := "2024-09-11")] abbrev div_add_mod := @tdiv_add_tmod
+@[deprecated tmod_add_tdiv' (since := "2024-09-11")] abbrev mod_add_div' := @tmod_add_tdiv'
+@[deprecated tdiv_add_tmod' (since := "2024-09-11")] abbrev div_add_mod' := @tdiv_add_tmod'
+@[deprecated tmod_def (since := "2024-09-11")] abbrev mod_def := @tmod_def
+@[deprecated tmod_eq_emod (since := "2024-09-11")] abbrev mod_eq_emod := @tmod_eq_emod
+@[deprecated fmod_eq_tmod (since := "2024-09-11")] abbrev fmod_eq_mod := @fmod_eq_tmod
+@[deprecated Int.tdiv_one (since := "2024-09-11")] abbrev div_one := @Int.tdiv_one
+@[deprecated Int.tdiv_neg (since := "2024-09-11")] abbrev div_neg := @Int.tdiv_neg
+@[deprecated Int.neg_tdiv (since := "2024-09-11")] abbrev neg_div := @Int.neg_tdiv
+@[deprecated Int.neg_tdiv_neg (since := "2024-09-11")] abbrev neg_div_neg := @Int.neg_tdiv_neg
+@[deprecated Int.tdiv_nonneg (since := "2024-09-11")] abbrev div_nonneg := @Int.tdiv_nonneg
+@[deprecated Int.tdiv_nonpos (since := "2024-09-11")] abbrev div_nonpos := @Int.tdiv_nonpos
+@[deprecated Int.tdiv_eq_zero_of_lt (since := "2024-09-11")] abbrev div_eq_zero_of_lt := @Int.tdiv_eq_zero_of_lt
+@[deprecated Int.mul_tdiv_cancel (since := "2024-09-11")] abbrev mul_div_cancel := @Int.mul_tdiv_cancel
+@[deprecated Int.mul_tdiv_cancel_left (since := "2024-09-11")] abbrev mul_div_cancel_left := @Int.mul_tdiv_cancel_left
+@[deprecated Int.tdiv_self (since := "2024-09-11")] abbrev div_self := @Int.tdiv_self
+@[deprecated Int.mul_tdiv_cancel_of_tmod_eq_zero (since := "2024-09-11")] abbrev mul_div_cancel_of_mod_eq_zero := @Int.mul_tdiv_cancel_of_tmod_eq_zero
+@[deprecated Int.tdiv_mul_cancel_of_tmod_eq_zero (since := "2024-09-11")] abbrev div_mul_cancel_of_mod_eq_zero := @Int.tdiv_mul_cancel_of_tmod_eq_zero
+@[deprecated Int.dvd_of_tmod_eq_zero (since := "2024-09-11")] abbrev dvd_of_mod_eq_zero := @Int.dvd_of_tmod_eq_zero
+@[deprecated Int.mul_tdiv_assoc (since := "2024-09-11")] abbrev mul_div_assoc := @Int.mul_tdiv_assoc
+@[deprecated Int.mul_tdiv_assoc' (since := "2024-09-11")] abbrev mul_div_assoc' := @Int.mul_tdiv_assoc'
+@[deprecated Int.tdiv_dvd_tdiv (since := "2024-09-11")] abbrev div_dvd_div := @Int.tdiv_dvd_tdiv
+@[deprecated Int.natAbs_tdiv (since := "2024-09-11")] abbrev natAbs_div := @Int.natAbs_tdiv
+@[deprecated Int.tdiv_eq_of_eq_mul_right (since := "2024-09-11")] abbrev div_eq_of_eq_mul_right := @Int.tdiv_eq_of_eq_mul_right
+@[deprecated Int.eq_tdiv_of_mul_eq_right (since := "2024-09-11")] abbrev eq_div_of_mul_eq_right := @Int.eq_tdiv_of_mul_eq_right
+@[deprecated Int.ofNat_tmod (since := "2024-09-11")] abbrev ofNat_mod := @Int.ofNat_tmod
+@[deprecated Int.tmod_one (since := "2024-09-11")] abbrev mod_one := @Int.tmod_one
+@[deprecated Int.tmod_eq_of_lt (since := "2024-09-11")] abbrev mod_eq_of_lt := @Int.tmod_eq_of_lt
+@[deprecated Int.tmod_lt_of_pos (since := "2024-09-11")] abbrev mod_lt_of_pos := @Int.tmod_lt_of_pos
+@[deprecated Int.tmod_nonneg (since := "2024-09-11")] abbrev mod_nonneg := @Int.tmod_nonneg
+@[deprecated Int.tmod_neg (since := "2024-09-11")] abbrev mod_neg := @Int.tmod_neg
+@[deprecated Int.mul_tmod_left (since := "2024-09-11")] abbrev mul_mod_left := @Int.mul_tmod_left
+@[deprecated Int.mul_tmod_right (since := "2024-09-11")] abbrev mul_mod_right := @Int.mul_tmod_right
+@[deprecated Int.tmod_eq_zero_of_dvd (since := "2024-09-11")] abbrev mod_eq_zero_of_dvd := @Int.tmod_eq_zero_of_dvd
+@[deprecated Int.dvd_iff_tmod_eq_zero (since := "2024-09-11")] abbrev dvd_iff_mod_eq_zero := @Int.dvd_iff_tmod_eq_zero
+@[deprecated Int.neg_mul_tmod_right (since := "2024-09-11")] abbrev neg_mul_mod_right := @Int.neg_mul_tmod_right
+@[deprecated Int.neg_mul_tmod_left (since := "2024-09-11")] abbrev neg_mul_mod_left := @Int.neg_mul_tmod_left
+@[deprecated Int.tdiv_mul_cancel (since := "2024-09-11")] abbrev div_mul_cancel := @Int.tdiv_mul_cancel
+@[deprecated Int.mul_tdiv_cancel' (since := "2024-09-11")] abbrev mul_div_cancel' := @Int.mul_tdiv_cancel'
+@[deprecated Int.eq_mul_of_tdiv_eq_right (since := "2024-09-11")] abbrev eq_mul_of_div_eq_right := @Int.eq_mul_of_tdiv_eq_right
+@[deprecated Int.tmod_self (since := "2024-09-11")] abbrev mod_self := @Int.tmod_self
+@[deprecated Int.neg_tmod_self (since := "2024-09-11")] abbrev neg_mod_self := @Int.neg_tmod_self
+@[deprecated Int.lt_tdiv_add_one_mul_self (since := "2024-09-11")] abbrev lt_div_add_one_mul_self := @Int.lt_tdiv_add_one_mul_self
+@[deprecated Int.tdiv_eq_iff_eq_mul_right (since := "2024-09-11")] abbrev div_eq_iff_eq_mul_right := @Int.tdiv_eq_iff_eq_mul_right
+@[deprecated Int.tdiv_eq_iff_eq_mul_left (since := "2024-09-11")] abbrev div_eq_iff_eq_mul_left := @Int.tdiv_eq_iff_eq_mul_left
+@[deprecated Int.eq_mul_of_tdiv_eq_left (since := "2024-09-11")] abbrev eq_mul_of_div_eq_left := @Int.eq_mul_of_tdiv_eq_left
+@[deprecated Int.tdiv_eq_of_eq_mul_left (since := "2024-09-11")] abbrev div_eq_of_eq_mul_left := @Int.tdiv_eq_of_eq_mul_left
+@[deprecated Int.eq_zero_of_tdiv_eq_zero (since := "2024-09-11")] abbrev eq_zero_of_div_eq_zero := @Int.eq_zero_of_tdiv_eq_zero
+@[deprecated Int.tdiv_left_inj (since := "2024-09-11")] abbrev div_left_inj := @Int.tdiv_left_inj
+@[deprecated Int.tdiv_sign (since := "2024-09-11")] abbrev div_sign := @Int.tdiv_sign
+@[deprecated Int.sign_eq_tdiv_abs (since := "2024-09-11")] abbrev sign_eq_div_abs := @Int.sign_eq_tdiv_abs
+@[deprecated Int.tdiv_eq_ediv_of_dvd (since := "2024-09-11")] abbrev div_eq_ediv_of_dvd := @Int.tdiv_eq_ediv_of_dvd
diff --git a/src/Lean/Data/Rat.lean b/src/Lean/Data/Rat.lean
index 03fe31ddee87..127d9eb707d7 100644
--- a/src/Lean/Data/Rat.lean
+++ b/src/Lean/Data/Rat.lean
@@ -29,7 +29,7 @@ instance : Repr Rat where
 
 @[inline] def Rat.normalize (a : Rat) : Rat :=
   let n := Nat.gcd a.num.natAbs a.den
-  if n == 1 then a else { num := a.num.div n, den := a.den / n }
+  if n == 1 then a else { num := a.num.tdiv n, den := a.den / n }
 
 def mkRat (num : Int) (den : Nat) : Rat :=
   if den == 0 then { num := 0 } else Rat.normalize { num, den }
@@ -53,7 +53,7 @@ protected def lt (a b : Rat) : Bool :=
 protected def mul (a b : Rat) : Rat :=
   let g1 := Nat.gcd a.den b.num.natAbs
   let g2 := Nat.gcd a.num.natAbs b.den
-  { num := (a.num.div g2)*(b.num.div g1)
+  { num := (a.num.tdiv g2)*(b.num.tdiv g1)
     den := (b.den / g2)*(a.den / g1) }
 
 protected def inv (a : Rat) : Rat :=
@@ -78,7 +78,7 @@ protected def add (a b : Rat) : Rat :=
     if g1 == 1 then
       { num, den }
     else
-      { num := num.div g1, den := den / g1 }
+      { num := num.tdiv g1, den := den / g1 }
 
 protected def sub (a b : Rat) : Rat :=
   let g := Nat.gcd a.den b.den
@@ -91,7 +91,7 @@ protected def sub (a b : Rat) : Rat :=
     if g1 == 1 then
       { num, den }
     else
-      { num := num.div g1, den := den / g1 }
+      { num := num.tdiv g1, den := den / g1 }
 
 protected def neg (a : Rat) : Rat :=
   { a with num := - a.num }
@@ -100,14 +100,14 @@ protected def floor (a : Rat) : Int :=
   if a.den == 1 then
     a.num
   else
-    let r := a.num.mod a.den
+    let r := a.num.tmod a.den
     if a.num < 0 then r - 1 else r
 
 protected def ceil (a : Rat) : Int :=
   if a.den == 1 then
     a.num
   else
-    let r := a.num.mod a.den
+    let r := a.num.tmod a.den
     if a.num > 0 then r + 1 else r
 
 instance : LT Rat where
diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean
index 930ca1e4a605..3643d63f3d49 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean
@@ -71,8 +71,8 @@ builtin_dsimproc [simp, seval] reduceMul ((_ * _ : Int)) := reduceBin ``HMul.hMu
 builtin_dsimproc [simp, seval] reduceSub ((_ - _ : Int)) := reduceBin ``HSub.hSub 6 (· - ·)
 builtin_dsimproc [simp, seval] reduceDiv ((_ / _ : Int)) := reduceBin ``HDiv.hDiv 6 (· / ·)
 builtin_dsimproc [simp, seval] reduceMod ((_ % _ : Int)) := reduceBin ``HMod.hMod 6 (· % ·)
-builtin_dsimproc [simp, seval] reduceTDiv (div  _ _) := reduceBin ``Int.div 2 Int.div
-builtin_dsimproc [simp, seval] reduceTMod (mod  _ _) := reduceBin ``Int.mod 2 Int.mod
+builtin_dsimproc [simp, seval] reduceTDiv (tdiv  _ _) := reduceBin ``Int.div 2 Int.tdiv
+builtin_dsimproc [simp, seval] reduceTMod (tmod  _ _) := reduceBin ``Int.mod 2 Int.tmod
 builtin_dsimproc [simp, seval] reduceFDiv (fdiv _ _) := reduceBin ``Int.fdiv 2 Int.fdiv
 builtin_dsimproc [simp, seval] reduceFMod (fmod _ _) := reduceBin ``Int.fmod 2 Int.fmod
 builtin_dsimproc [simp, seval] reduceBdiv (bdiv _ _) := reduceBinIntNatOp ``bdiv bdiv