fix

src/Init/Data/BitVec/Lemmas.lean

@@ -4109,9 +4109,7 @@ theorem sub_le_sub_iff_le {x y z : BitVec w} (hxz : z ≤ x) (hyz : z ≤ y) :
 
 theorem msb_eq_toInt {x : BitVec w}:
     x.msb = decide (x.toInt < 0) := by
-  by_cases h : x.msb <;>
-  · simp [h, toInt_eq_msb_cond]
-    omega
+  by_cases h : x.msb <;> simp [h, toInt_eq_msb_cond] <;> omega
 
 theorem msb_eq_toNat {x : BitVec w}:
     x.msb = decide (x.toNat ≥ 2 ^ (w - 1)) := by

src/Init/Data/Int/Basic.lean

@@ -17,10 +17,12 @@ open Nat
 This file defines the `Int` type as well as
 
 * coercions, conversions, and compatibility with numeric literals,
-* basic arithmetic operations add/sub/mul/div/mod/pow,
+* basic arithmetic operations add/sub/mul/pow,
 * a few `Nat`-related operations such as `negOfNat` and `subNatNat`,
 * relations `<`/`≤`/`≥`/`>`, the `NonNeg` property and `min`/`max`,
 * decidability of equality, relations and `NonNeg`.
+
+Division and modulus operations are defined in `Init.Data.Int.DivMod.Basic`.
 -/
 
 /--

src/Init/Data/Int/DivMod/Basic.lean

@@ -21,25 +21,25 @@ and satisfy `x / 0 = 0` and `x % 0 = x`.
 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`,
+However we decided it was better to use `ediv` and `emod` for the default typeclass instances,
 as they are consistent with the conventions used in SMTLib, and 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.
 
-In December 2024, we removed `tdiv` and `tmod`, but have not yet renamed `ediv` and `emod`.
+In December 2024, we removed `div` and `mod`, but have not yet renamed `ediv` and `emod`.
 -/
 
 /-! ### E-rounding division
-This pair satisfies `0 ≤ mod x y < natAbs y` for `y ≠ 0`.
+This pair satisfies `0 ≤ emod x y < natAbs y` for `y ≠ 0`.
 -/
 
 /--
-Integer division. This version of `Int.div` uses the E-rounding convention
-(euclidean division), in which `Int.emod x y` satisfies `0 ≤ mod x y < natAbs y` for `y ≠ 0`
+Integer division. This version of integer division uses the E-rounding convention
+(euclidean division), in which `Int.emod x y` satisfies `0 ≤ emod x y < natAbs y` for `y ≠ 0`
 and `Int.ediv` is the unique function satisfying `emod x y + (ediv x y) * y = x`.
 
 This is the function powering the `/` notation on integers.
@@ -71,7 +71,7 @@ def ediv : (@& Int) → (@& Int) → Int
   | -[m+1],  -[n+1]  => ofNat (succ (m / succ n))
 
 /--
-Integer modulus. This version of `Int.mod` uses the E-rounding convention
+Integer modulus. This version of integer modulus uses the E-rounding convention
 (euclidean division), in which `Int.emod x y` satisfies `0 ≤ emod x y < natAbs y` for `y ≠ 0`
 and `Int.ediv` is the unique function satisfying `emod x y + (ediv x y) * y = x`.
 
@@ -229,7 +229,7 @@ def fdiv : Int → Int → Int
   | -[m+1],  -[n+1]  => ofNat (succ m / succ n)
 
 /--
-Integer modulus. This version of `Int.mod` uses the F-rounding convention
+Integer modulus. This version of integer modulus uses the F-rounding convention
 (flooring division), in which `Int.fdiv x y` satisfies `fdiv x y = floor (x / y)`
 and `Int.fmod` is the unique function satisfying `fmod x y + (fdiv x y) * y = x`.
 
@@ -268,11 +268,14 @@ Balanced mod (and balanced div) are a division and modulus pair such
 that `b * (Int.bdiv a b) + Int.bmod a b = a` and
 `-b/2 ≤ Int.bmod a b < b/2` for all `a : Int` and `b > 0`.
 
-This is used in Omega as well as signed bitvectors.
+Note that unlike `emod`, `fmod`, and `tmod`,
+`bmod` takes a natural number as the second argument, rather than an integer.
+
+This function is used in `omega` as well as signed bitvectors.
 -/
 
 /--
-Balanced modulus.  This version of Integer modulus uses the
+Balanced modulus.  This version of integer modulus uses the
 balanced rounding convention, which guarantees that
 `-m/2 ≤ bmod x m < m/2` for `m ≠ 0` and `bmod x m` is congruent
 to `x` modulo `m`.

src/Init/Data/Int/DivMod/Bootstrap.lean

@@ -18,7 +18,7 @@ open Nat (succ)
 
 namespace Int
 
--- /-! ### dvd  -/
+/-! ### dvd  -/
 
 protected theorem dvd_def (a b : Int) : (a ∣ b) = Exists (fun c => b = a * c) := rfl
 
@@ -67,7 +67,7 @@ protected theorem dvd_neg {a b : Int} : a ∣ -b ↔ a ∣ b := by
 theorem ofNat_dvd_left {n : Nat} {z : Int} : (↑n : Int) ∣ z ↔ n ∣ z.natAbs := by
   rw [← natAbs_dvd_natAbs, natAbs_ofNat]
 
-/-! ### *div zero  -/
+/-! ### ediv zero  -/
 
 @[simp] theorem zero_ediv : ∀ b : Int, 0 / b = 0
   | ofNat _ => show ofNat _ = _ by simp
@@ -77,7 +77,7 @@ theorem ofNat_dvd_left {n : Nat} {z : Int} : (↑n : Int) ∣ z ↔ n ∣ z.natA
   | ofNat _ => show ofNat _ = _ by simp
   | -[_+1] => rfl
 
-/-! ### mod zero -/
+/-! ### emod zero -/
 
 @[simp] theorem zero_emod (b : Int) : 0 % b = 0 := rfl
 
@@ -89,7 +89,6 @@ theorem ofNat_dvd_left {n : Nat} {z : Int} : (↑n : Int) ∣ z ↔ n ∣ z.natA
 
 @[simp, norm_cast] theorem ofNat_emod (m n : Nat) : (↑(m % n) : Int) = m % n := rfl
 
-
 /-! ### mod definitions -/
 
 theorem emod_add_ediv : ∀ a b : Int, a % b + b * (a / b) = a
@@ -106,12 +105,17 @@ where
       ← Int.neg_neg (_-_), Int.neg_sub, Int.sub_sub_self, Int.add_right_comm]
     exact congrArg (fun x => -(ofNat x + 1)) (Nat.mod_add_div ..)
 
+/-- Variant of `emod_add_ediv` with the multiplication written the other way around. -/
 theorem emod_add_ediv' (a b : Int) : a % b + a / b * b = a := by
   rw [Int.mul_comm]; exact emod_add_ediv ..
 
 theorem ediv_add_emod (a b : Int) : b * (a / b) + a % b = a := by
   rw [Int.add_comm]; exact emod_add_ediv ..
 
+/-- Variant of `ediv_add_emod` with the multiplication written the other way around. -/
+theorem ediv_add_emod' (a b : Int) : a / b * b + a % b = a := by
+  rw [Int.mul_comm]; exact ediv_add_emod ..
+
 theorem emod_def (a b : Int) : a % b = a - b * (a / b) := by
   rw [← Int.add_sub_cancel (a % b), emod_add_ediv]
 
@@ -170,7 +174,7 @@ theorem add_ediv_of_dvd_left {a b c : Int} (H : c ∣ a) : (a + b) / c = a / c +
 @[simp] theorem mul_ediv_cancel_left (b : Int) (H : a ≠ 0) : (a * b) / a = b :=
   Int.mul_comm .. ▸ Int.mul_ediv_cancel _ H
 
-theorem div_nonneg_iff_of_pos {a b : Int} (h : 0 < b) : a / b ≥ 0 ↔ a ≥ 0 := by
+theorem ediv_nonneg_iff_of_pos {a b : Int} (h : 0 < b) : 0 ≤ a / b ↔ 0 ≤ a := by
   rw [Int.div_def]
   match b, h with
   | Int.ofNat (b+1), _ =>
@@ -178,6 +182,9 @@ theorem div_nonneg_iff_of_pos {a b : Int} (h : 0 < b) : a / b ≥ 0 ↔ a ≥ 0
     norm_cast
     simp
 
+@[deprecated ediv_nonneg_iff_of_pos (since := "2025-02-28")]
+abbrev div_nonneg_iff_of_pos := @ediv_nonneg_iff_of_pos
+
 /-! ### emod -/
 
 theorem emod_nonneg : ∀ (a : Int) {b : Int}, b ≠ 0 → 0 ≤ a % b

src/Init/Data/Int/DivMod/Lemmas.lean

@@ -94,6 +94,14 @@ theorem eq_one_of_mul_eq_one_left {a b : Int} (H : 0 ≤ b) (H' : a * b = 1) : b
 instance decidableDvd : DecidableRel (α := Int) (· ∣ ·) := fun _ _ =>
   decidable_of_decidable_of_iff (dvd_iff_emod_eq_zero ..).symm
 
+protected theorem mul_dvd_mul_iff_left {a b c : Int} (h : a ≠ 0) : (a * b) ∣ (a * c) ↔ b ∣ c :=
+  ⟨by rintro ⟨d, h'⟩; exact ⟨d, by rw [Int.mul_assoc] at h'; exact (mul_eq_mul_left_iff h).mp h'⟩,
+    by rintro ⟨d, rfl⟩; exact ⟨d, by simp [Int.mul_assoc]⟩⟩
+
+protected theorem mul_dvd_mul_iff_right {a b c : Int} (h : a ≠ 0) : (b * a) ∣ (c * a) ↔ b ∣ c := by
+  rw [Int.mul_comm b a, Int.mul_comm c a]
+  exact Int.mul_dvd_mul_iff_left h
+
 /-! ### *div zero  -/
 
 @[simp] protected theorem zero_tdiv : ∀ b : Int, tdiv 0 b = 0
@@ -234,6 +242,13 @@ theorem tdiv_eq_fdiv {a b : Int} :
   rw [fdiv_eq_tdiv]
   omega
 
+
+theorem tdiv_eq_ediv_of_dvd {a b : Int} (h : b ∣ a) : a.tdiv b = a / b := by
+  simp [tdiv_eq_ediv, h]
+
+theorem fdiv_eq_ediv_of_dvd {a b : Int} (h : b ∣ a) : a.fdiv b = a / b := by
+  simp [fdiv_eq_ediv, h]
+
 /-! ### mod zero -/
 
 @[simp] theorem zero_tmod (b : Int) : tmod 0 b = 0 := by cases b <;> simp [tmod]
@@ -251,9 +266,6 @@ theorem tdiv_eq_fdiv {a b : Int} :
 
 /-! ### mod definitions -/
 
-theorem ediv_add_emod' (a b : Int) : a / b * b + a % b = a := by
-  rw [Int.mul_comm]; exact ediv_add_emod ..
-
 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
@@ -274,9 +286,11 @@ theorem tmod_add_tdiv : ∀ a b : Int, tmod a b + b * (a.tdiv b) = a
 theorem tdiv_add_tmod (a b : Int) : b * a.tdiv b + tmod a b = a := by
   rw [Int.add_comm]; apply tmod_add_tdiv ..
 
+/-- Variant of `tmod_add_tdiv` with the multiplication written the other way around. -/
 theorem tmod_add_tdiv' (m k : Int) : tmod m k + m.tdiv k * k = m := by
   rw [Int.mul_comm]; apply tmod_add_tdiv
 
+/-- Variant of `tdiv_add_tmod` with the multiplication written the other way around. -/
 theorem tdiv_add_tmod' (m k : Int) : m.tdiv k * k + tmod m k = m := by
   rw [Int.mul_comm]; apply tdiv_add_tmod
 
@@ -300,9 +314,17 @@ theorem fmod_add_fdiv : ∀ a b : Int, a.fmod b + b * a.fdiv b = a
     show -(↑(succ m % succ n) : Int) + -↑(succ n * (succ m / succ n)) = -↑(succ m)
     rw [← Int.neg_add]; exact congrArg (-ofNat ·) <| Nat.mod_add_div ..
 
+/-- Variant of `fmod_add_fdiv` with the multiplication written the other way around. -/
+theorem fmod_add_fdiv' (a b : Int) : a.fmod b + (a.fdiv b) * b = a := by
+  rw [Int.mul_comm]; exact fmod_add_fdiv ..
+
 theorem fdiv_add_fmod (a b : Int) : b * a.fdiv b + a.fmod b = a := by
   rw [Int.add_comm]; exact fmod_add_fdiv ..
 
+/-- Variant of `fdiv_add_fmod` with the multiplication written the other way around. -/
+theorem fdiv_add_fmod' (a b : Int) : (a.fdiv b) * b + a.fmod b = a := by
+  rw [Int.mul_comm]; exact fdiv_add_fmod ..
+
 theorem fmod_def (a b : Int) : a.fmod b = a - b * a.fdiv b := by
   rw [← Int.add_sub_cancel (a.fmod b), fmod_add_fdiv]
 
@@ -396,6 +418,11 @@ theorem ediv_nonneg_of_nonpos_of_nonpos {a b : Int} (Ha : a ≤ 0) (Hb : b ≤ 0
     rw [Int.div_def, ediv]
     exact le_add_one (ediv_nonneg (ofNat_zero_le a) (Int.le_trans (ofNat_zero_le b) (le.intro 1 rfl)))
 
+theorem ediv_pos_of_neg_of_neg {a b : Int} (ha : a < 0) (hb : b < 0) : 0 < a / b := by
+  rw [Int.div_def]
+  match a, b, ha, hb with
+  | .negSucc a, .negSucc b, _, _ => apply ofNat_succ_pos
+
 theorem ediv_nonpos {a b : Int} (Ha : 0 ≤ a) (Hb : b ≤ 0) : a / b ≤ 0 :=
   Int.nonpos_of_neg_nonneg <| Int.ediv_neg .. ▸ Int.ediv_nonneg Ha (Int.neg_nonneg_of_nonpos Hb)
 
@@ -446,6 +473,10 @@ protected theorem ediv_eq_of_eq_mul_left {a b c : Int}
     (H1 : b ≠ 0) (H2 : a = c * b) : a / b = c :=
   Int.ediv_eq_of_eq_mul_right H1 (by rw [Int.mul_comm, H2])
 
+protected theorem eq_ediv_of_mul_eq_left {a b c : Int}
+    (H1 : b ≠ 0) (H2 : a * b = c) : a = c / b :=
+  (Int.ediv_eq_of_eq_mul_left H1 H2.symm).symm
+
 /-! ### emod -/
 
 theorem mod_def' (m n : Int) : m % n = emod m n := rfl
@@ -715,16 +746,100 @@ theorem ediv_eq_ediv_of_mul_eq_mul {a b c d : Int}
 
 /-! ### tdiv -/
 
-@[simp] protected theorem tdiv_one : ∀ a : Int, a.tdiv 1 = a
-  | (n:Nat) => congrArg ofNat (Nat.div_one _)
-  | -[n+1] => by simp [Int.tdiv, neg_ofNat_succ]; rfl
-
 unseal Nat.div in
 @[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 _, -[_+1] | -[_+1], succ _ => (Int.neg_neg _).symm
   | ofNat _, succ _ | -[_+1], 0 | -[_+1], -[_+1] => rfl
 
+/-!
+We don't give `tdiv` versions of
+* `add_mul_ediv_right : c ≠ 0 → (a + b * c) / c = a / c + b`
+* `add_mul_ediv_left : b ≠ 0 → (a + b * c) / b = a / b + c`
+* `add_ediv_of_dvd_right : c ∣ b → (a + b) / c = a / c + b / c`
+* `add_ediv_of_dvd_left : c ∣ a → (a + b) / c = a / c + b / c`
+because they all involve awkward off-by-one corrections.
+-/
+
+@[simp] theorem mul_tdiv_cancel (a : Int) {b : Int} (H : b ≠ 0) : (a * b).tdiv b = a := by
+  rw [tdiv_eq_ediv_of_dvd (Int.dvd_mul_left a b), mul_ediv_cancel _ H]
+
+@[simp] theorem mul_tdiv_cancel_left (b : Int) (H : a ≠ 0) : (a * b).tdiv a = b :=
+  Int.mul_comm .. ▸ Int.mul_tdiv_cancel _ H
+
+-- There's no good analogues of `ediv_nonneg_iff_of_pos`, `ediv_neg'`, or `negSucc_ediv`
+-- for `tdiv`.
+
+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 _
+
+theorem tdiv_nonneg_of_nonpos_of_nonpos {a b : Int} (Ha : a ≤ 0) (Hb : b ≤ 0) : 0 ≤ a.tdiv b := by
+  rw [tdiv_eq_ediv]
+  split <;> rename_i h
+  · simpa using ediv_nonneg_of_nonpos_of_nonpos Ha Hb
+  · simp at h
+    by_cases h' : b = 0
+    · subst h'
+      simp
+    · replace h' : b < 0 := by omega
+      rw [sign_eq_neg_one_of_neg h']
+      have : 0 < a / b := by
+        by_cases h'' : a = 0
+        · subst h''
+          simp at h
+        · replace h'' : a < 0 := by omega
+          exact ediv_pos_of_neg_of_neg h'' h'
+      omega
+
+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 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] theorem mul_tdiv_mul_of_pos {a : Int}
+    (b c : Int) (H : 0 < a) : (a * b).tdiv (a * c) = b.tdiv c := by
+  rw [tdiv_eq_ediv, mul_ediv_mul_of_pos _ _ H, tdiv_eq_ediv]
+  simp only [sign_mul]
+  by_cases h : 0 ≤ b
+  · rw [if_pos, if_pos (.inl h)]
+    left
+    exact Int.mul_nonneg (Int.le_of_lt H) h
+  · have H' : a ≠ 0 := by omega
+    simp only [Int.mul_dvd_mul_iff_left H']
+    by_cases h' : c ∣ b
+    · simp [h']
+    · rw [if_neg, if_neg]
+      · simp [sign_eq_one_of_pos H]
+      · simp [h']; omega
+      · simp_all only [Int.not_le, ne_eq, or_false]
+        exact Int.mul_neg_of_pos_of_neg H h
+
+@[simp] theorem mul_tdiv_mul_of_pos_left
+    (a : Int) {b : Int} (c : Int) (H : 0 < b) : (a * b).tdiv (c * b) = a.tdiv c := by
+  rw [Int.mul_comm, Int.mul_comm c, mul_tdiv_mul_of_pos _ _ H]
+
+@[simp] protected theorem tdiv_one : ∀ a : Int, a.tdiv 1 = a
+  | (n:Nat) => congrArg ofNat (Nat.div_one _)
+  | -[n+1] => by simp [Int.tdiv, neg_ofNat_succ]; rfl
+
+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_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
+
+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_tdiv_of_mul_eq_left {a b c : Int}
+    (H1 : b ≠ 0) (H2 : a * b = c) : a = c.tdiv b :=
+  (Int.tdiv_eq_of_eq_mul_left H1 H2.symm).symm
+
 unseal Nat.div in
 @[simp] protected theorem neg_tdiv : ∀ a b : Int, (-a).tdiv b = -(a.tdiv b)
   | 0, n => by simp [Int.neg_zero]
@@ -734,33 +849,6 @@ unseal Nat.div in
 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 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 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 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_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_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_tdiv, this H]
-  | _, _, ⟨a, .inr rfl⟩, ⟨b, .inr rfl⟩ => by
-    rw [Int.neg_mul_neg, Int.tdiv_neg, this (Int.neg_ne_zero.1 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 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
 
@@ -796,14 +884,7 @@ theorem tdiv_dvd_tdiv : ∀ {a b c : Int}, a ∣ b → b ∣ c → b.tdiv a ∣
   | _, _, ⟨_, .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 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_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 -/
+/-! ### tmod -/
 
 theorem ofNat_tmod (m n : Nat) : (↑(m % n) : Int) = tmod m n := rfl
 
@@ -878,9 +959,6 @@ 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 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_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]
@@ -968,19 +1046,6 @@ theorem fmod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : a.fmod b < b :=
 @[simp] theorem fmod_self {a : Int} : a.fmod a = 0 := by
   have := mul_fmod_left 1 a; rwa [Int.one_mul] at this
 
-/-! ### Theorems crossing div/mod versions -/
-
-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.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
-    by_cases bz : b = 0
-    · simp [bz]
-    · rw [mul_fdiv_cancel_left _ bz, mul_ediv_cancel_left _ bz]
-
 /-! ### bmod -/
 
 @[simp]

src/Init/Data/Int/Linear.lean

@@ -531,8 +531,9 @@ def Poly.isValidLe (p : Poly) : Bool :=
   | .num k => k ≤ 0
   | _ => false
 
+attribute [-simp] Int.not_le in
 theorem le_eq_false (ctx : Context) (lhs rhs : Expr) : (lhs.sub rhs).norm.isUnsatLe → (lhs.denote ctx ≤ rhs.denote ctx) = False := by
-  simp [Poly.isUnsatLe] <;> split <;> simp
+  simp only [Poly.isUnsatLe] <;> split <;> simp
   next p k h =>
     intro h'
     replace h := congrArg (Poly.denote ctx) h
@@ -820,7 +821,7 @@ def le_neg_cert (p₁ p₂ : Poly) : Bool :=
 theorem le_neg (ctx : Context) (p₁ p₂ : Poly) : le_neg_cert p₁ p₂ → ¬ p₁.denote' ctx ≤ 0 → p₂.denote' ctx ≤ 0 := by
   simp [le_neg_cert]
   intro; subst p₂; simp; intro h
-  replace h : _ + 1 ≤ -0 := Int.neg_lt_neg <| Int.lt_of_not_ge h
+  replace h : _ + 1 ≤ -0 := Int.neg_lt_neg h
   simp at h
   exact h
 
@@ -846,9 +847,6 @@ theorem le_combine (ctx : Context) (p₁ p₂ p₃ : Poly)
 
 theorem le_unsat (ctx : Context) (p : Poly) : p.isUnsatLe → p.denote' ctx ≤ 0 → False := by
   simp [Poly.isUnsatLe]; split <;> simp
-  intro h₁ h₂
-  have := Int.lt_of_le_of_lt h₂ h₁
-  simp at this
 
 theorem eq_norm (ctx : Context) (p₁ p₂ : Poly) (h : p₁.norm == p₂) : p₁.denote' ctx = 0 → p₂.denote' ctx = 0 := by
   simp at h

src/Init/Data/Int/Order.lean

@@ -133,10 +133,10 @@ protected theorem lt_of_not_ge {a b : Int} (h : ¬a ≤ b) : b < a :=
 protected theorem not_le_of_gt {a b : Int} (h : b < a) : ¬a ≤ b :=
   (Int.lt_iff_le_not_le.mp h).right
 
-protected theorem not_le {a b : Int} : ¬a ≤ b ↔ b < a :=
+@[simp] protected theorem not_le {a b : Int} : ¬a ≤ b ↔ b < a :=
   Iff.intro Int.lt_of_not_ge Int.not_le_of_gt
 
-protected theorem not_lt {a b : Int} : ¬a < b ↔ b ≤ a :=
+@[simp] protected theorem not_lt {a b : Int} : ¬a < b ↔ b ≤ a :=
   by rw [← Int.not_le, Decidable.not_not]
 
 protected theorem lt_trichotomy (a b : Int) : a < b ∨ a = b ∨ b < a :=

src/Init/Omega/Constraint.lean

@@ -111,9 +111,7 @@ def isExact : Constraint → Bool
 
 theorem not_sat_of_isImpossible (h : isImpossible c) {t} : ¬ c.sat t := by
   rcases c with ⟨_ | l, _ | u⟩ <;> simp [isImpossible, sat] at h ⊢
-  intro w
-  rw [Int.not_le]
-  exact Int.lt_of_lt_of_le h w
+  exact Int.lt_of_lt_of_le h
 
 /--
 Scale a constraint by multiplying by an integer.
@@ -139,17 +137,14 @@ theorem scale_sat {c : Constraint} (k) (w : c.sat t) : (scale k c).sat (k * t) :
   · rcases c with ⟨_ | l, _ | u⟩ <;> split <;> rename_i h <;> simp_all [sat, flip, map]
     · replace h := Int.le_of_lt h
       exact Int.mul_le_mul_of_nonneg_left w h
-    · rw [Int.not_lt] at h
-      exact Int.mul_le_mul_of_nonpos_left h w
+    · exact Int.mul_le_mul_of_nonpos_left h w
     · replace h := Int.le_of_lt h
       exact Int.mul_le_mul_of_nonneg_left w h
-    · rw [Int.not_lt] at h
-      exact Int.mul_le_mul_of_nonpos_left h w
+    · exact Int.mul_le_mul_of_nonpos_left h w
     · constructor
       · exact Int.mul_le_mul_of_nonneg_left w.1 (Int.le_of_lt h)
       · exact Int.mul_le_mul_of_nonneg_left w.2 (Int.le_of_lt h)
-    · replace h := Int.not_lt.mp h
-      constructor
+    · constructor
       · exact Int.mul_le_mul_of_nonpos_left h w.2
       · exact Int.mul_le_mul_of_nonpos_left h w.1
 
@@ -210,21 +205,19 @@ theorem div_sat (c : Constraint) (t : Int) (k : Nat) (n : k ≠ 0) (h : (k : Int
   · simp_all [sat, div]
   · simp [sat, div] at w ⊢
     apply Int.le_of_sub_nonneg
-    rw [← Int.sub_ediv_of_dvd _ h, ← ge_iff_le, Int.div_nonneg_iff_of_pos n]
+    rw [← Int.sub_ediv_of_dvd _ h, Int.ediv_nonneg_iff_of_pos n]
     exact Int.sub_nonneg_of_le w
   · simp [sat, div] at w ⊢
     apply Int.le_of_sub_nonneg
-    rw [Int.sub_neg, ← Int.add_ediv_of_dvd_left h, ← ge_iff_le,
-      Int.div_nonneg_iff_of_pos n]
+    rw [Int.sub_neg, ← Int.add_ediv_of_dvd_left h, Int.ediv_nonneg_iff_of_pos n]
     exact Int.sub_nonneg_of_le w
   · simp [sat, div] at w ⊢
     constructor
     · apply Int.le_of_sub_nonneg
-      rw [Int.sub_neg, ← Int.add_ediv_of_dvd_left h, ← ge_iff_le,
-        Int.div_nonneg_iff_of_pos n]
+      rw [Int.sub_neg, ← Int.add_ediv_of_dvd_left h, Int.ediv_nonneg_iff_of_pos n]
       exact Int.sub_nonneg_of_le w.1
     · apply Int.le_of_sub_nonneg
-      rw [← Int.sub_ediv_of_dvd _ h, ← ge_iff_le, Int.div_nonneg_iff_of_pos n]
+      rw [← Int.sub_ediv_of_dvd _ h, Int.ediv_nonneg_iff_of_pos n]
       exact Int.sub_nonneg_of_le w.2
 
 /--