feat: force-mathlib-ci label

This PR prepares for #7141.

.github/workflows/pr-release.yml

@@ -155,6 +155,20 @@ jobs:
           fi
 
           if [[ -n "$MESSAGE" ]]; then
+            # Check if force-mathlib-ci label is present
+            LABELS="$(curl --retry 3 --location --silent \
+                          -H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
+                          -H "Accept: application/vnd.github.v3+json" \
+                          "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/labels" \
+                          | jq -r '.[].name')"
+            
+            if echo "$LABELS" | grep -q "^force-mathlib-ci$"; then
+              echo "force-mathlib-ci label detected, forcing CI despite issues"
+              MESSAGE="Forcing Mathlib CI because the \`force-mathlib-ci\` label is present, despite problem: $MESSAGE"
+              FORCE_CI=true
+            else
+              MESSAGE="$MESSAGE You can force Mathlib CI using the \`force-mathlib-ci\` label."
+            fi
 
             echo "Checking existing messages"
 
@@ -201,7 +215,12 @@ jobs:
             else
               echo "The message already exists in the comment body."
             fi
-            echo "mathlib_ready=false" >> "$GITHUB_OUTPUT"
+
+            if [[ "$FORCE_CI" == "true" ]]; then
+              echo "mathlib_ready=true" >> "$GITHUB_OUTPUT"
+            else
+              echo "mathlib_ready=false" >> "$GITHUB_OUTPUT"
+            fi
           else
             echo "mathlib_ready=true" >> "$GITHUB_OUTPUT"
           fi
@@ -252,7 +271,7 @@ jobs:
           if git ls-remote --heads --tags --exit-code origin "nightly-testing-${MOST_RECENT_NIGHTLY}" >/dev/null; then
             BASE="nightly-testing-${MOST_RECENT_NIGHTLY}"
           else
-            echo "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' tag at Batteries. Falling back to 'nightly-testing'."
+            echo "Couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' tag at Batteries. Falling back to 'nightly-testing'."
             BASE=nightly-testing
           fi
 
@@ -316,7 +335,7 @@ jobs:
           if git ls-remote --heads --tags --exit-code origin "nightly-testing-${MOST_RECENT_NIGHTLY}" >/dev/null; then
             BASE="nightly-testing-${MOST_RECENT_NIGHTLY}"
           else
-            echo "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' branch at Mathlib. Falling back to 'nightly-testing'."
+            echo "Couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' branch at Mathlib. Falling back to 'nightly-testing'."
             BASE=nightly-testing
           fi
 

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

@@ -158,10 +158,6 @@ theorem add_mul_ediv_right (a b : Int) {c : Int} (H : c ≠ 0) : (a + b * c) / c
       apply congrArg negSucc
       rw [Nat.mul_comm, Nat.sub_mul_div]; rwa [Nat.mul_comm]
 
-theorem add_mul_ediv_left (a : Int) {b : Int}
-    (c : Int) (H : b ≠ 0) : (a + b * c) / b = a / b + c :=
-  Int.mul_comm .. ▸ Int.add_mul_ediv_right _ _ H
-
 theorem add_ediv_of_dvd_right {a b c : Int} (H : c ∣ b) : (a + b) / c = a / c + b / c :=
   if h : c = 0 then by simp [h] else by
     let ⟨k, hk⟩ := H
@@ -200,6 +196,16 @@ theorem emod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : a % b < b :=
   | ofNat _, _, ⟨_, rfl⟩ => ofNat_lt.2 (Nat.mod_lt _ (Nat.succ_pos _))
   | -[_+1], _, ⟨_, rfl⟩ => Int.sub_lt_self _ (ofNat_lt.2 <| Nat.succ_pos _)
 
+theorem mul_ediv_self_le {x k : Int} (h : k ≠ 0) : k * (x / k) ≤ x :=
+  calc k * (x / k)
+    _ ≤ k * (x / k) + x % k := Int.le_add_of_nonneg_right (emod_nonneg x h)
+    _ = x                   := ediv_add_emod _ _
+
+theorem lt_mul_ediv_self_add {x k : Int} (h : 0 < k) : x < k * (x / k) + k :=
+  calc x
+    _ = k * (x / k) + x % k := (ediv_add_emod _ _).symm
+    _ < k * (x / k) + k     := Int.add_lt_add_left (emod_lt_of_pos x h) _
+
 @[simp] theorem add_mul_emod_self {a b c : Int} : (a + b * c) % c = a % c :=
   if cz : c = 0 then by
     rw [cz, Int.mul_zero, Int.add_zero]
@@ -307,18 +313,6 @@ theorem emod_pos_of_not_dvd {a b : Int} (h : ¬ a ∣ b) : a = 0 ∨ 0 < b % a :
   · simp_all
   · exact Or.inr (Int.lt_iff_le_and_ne.mpr ⟨emod_nonneg b w, Ne.symm h⟩)
 
-/-! ### `/` and ordering -/
-
-theorem mul_ediv_self_le {x k : Int} (h : k ≠ 0) : k * (x / k) ≤ x :=
-  calc k * (x / k)
-    _ ≤ k * (x / k) + x % k := Int.le_add_of_nonneg_right (emod_nonneg x h)
-    _ = x                   := ediv_add_emod _ _
-
-theorem lt_mul_ediv_self_add {x k : Int} (h : 0 < k) : x < k * (x / k) + k :=
-  calc x
-    _ = k * (x / k) + x % k := (ediv_add_emod _ _).symm
-    _ < k * (x / k) + k     := Int.add_lt_add_left (emod_lt_of_pos x h) _
-
 /-! ### bmod -/
 
 @[simp] theorem bmod_emod : bmod x m % m = x % m := by

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

@@ -40,17 +40,6 @@ protected theorem dvd_add_left {a b c : Int} (H : a ∣ c) : a ∣ b + c ↔ a
 protected theorem dvd_add_right {a b c : Int} (H : a ∣ b) : a ∣ b + c ↔ a ∣ c := by
   rw [Int.add_comm, Int.dvd_add_left H]
 
-@[simp] protected theorem dvd_add_mul_self {a b c : Int} : a ∣ b + c * a ↔ a ∣ b := by
-  rw [Int.dvd_add_left (Int.dvd_mul_left c a)]
-
-@[simp] protected theorem dvd_add_self_mul {a b c : Int} : a ∣ b + a * c ↔ a ∣ b := by
-  rw [Int.mul_comm, Int.dvd_add_mul_self]
-
-@[simp] protected theorem dvd_mul_self_add {a b c : Int} : a ∣ b * a + c ↔ a ∣ c := by
-  rw [Int.add_comm, Int.dvd_add_mul_self]
-
-@[simp] protected theorem dvd_self_mul_add {a b c : Int} : a ∣ a * b + c ↔ a ∣ c := by
-  rw [Int.mul_comm, Int.dvd_mul_self_add]
 protected theorem dvd_iff_dvd_of_dvd_sub {a b c : Int} (H : a ∣ b - c) : a ∣ b ↔ a ∣ c :=
   ⟨fun h => Int.sub_sub_self b c ▸ Int.dvd_sub h H,
    fun h => Int.sub_add_cancel b c ▸ Int.dvd_add H h⟩
@@ -401,13 +390,10 @@ theorem tmod_eq_fmod {a b : Int} :
 
 /-! ### `/` ediv -/
 
-theorem ediv_neg_of_neg_of_pos {a b : Int} (Ha : a < 0) (Hb : 0 < b) : a / b < 0 :=
+theorem ediv_neg' {a b : Int} (Ha : a < 0) (Hb : 0 < b) : a / b < 0 :=
   match a, b, eq_negSucc_of_lt_zero Ha, eq_succ_of_zero_lt Hb with
   | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => negSucc_lt_zero _
 
-@[deprecated ediv_neg_of_neg_of_pos (since := "2025-03-04")]
-abbrev ediv_neg' := @ediv_neg_of_neg_of_pos
-
 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
@@ -437,16 +423,17 @@ theorem ediv_pos_of_neg_of_neg {a b : Int} (ha : a < 0) (hb : b < 0) : 0 < a / b
   match a, b, ha, hb with
   | .negSucc a, .negSucc b, _, _ => apply ofNat_succ_pos
 
-theorem ediv_nonpos_of_nonneg_of_nonpos {a b : Int} (Ha : 0 ≤ a) (Hb : b ≤ 0) : a / b ≤ 0 :=
+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)
 
-@[deprecated ediv_nonpos_of_nonneg_of_nonpos (since := "2025-03-04")]
-abbrev ediv_nonpos := @ediv_nonpos_of_nonneg_of_nonpos
-
 theorem ediv_eq_zero_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : a / 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
 
+theorem add_mul_ediv_left (a : Int) {b : Int}
+    (c : Int) (H : b ≠ 0) : (a + b * c) / b = a / b + c :=
+  Int.mul_comm .. ▸ Int.add_mul_ediv_right _ _ H
+
 @[simp] theorem mul_ediv_mul_of_pos {a : Int}
     (b c : Int) (H : 0 < a) : (a * b) / (a * c) = b / c :=
   suffices ∀ (m k : Nat) (b : Int), (m.succ * b) / (m.succ * k) = b / k from
@@ -490,15 +477,6 @@ 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
 
-@[simp] protected theorem ediv_self {a : Int} (H : a ≠ 0) : a / a = 1 := by
-  have := Int.mul_ediv_cancel 1 H; rwa [Int.one_mul] at this
-
-@[simp] protected theorem neg_ediv_self (a : Int) (h : a ≠ 0) : (-a) / a = -1 := by
-  rw [neg_ediv_of_dvd (Int.dvd_refl a), Int.ediv_self h]
-
--- There are no theorems `neg_ediv : ∀ {a b : Int}, (-a) / b = - (a / b)` or
--- `neg_ediv_neg: ∀ {a b : Int},  (-a) / (-b) = a / b` because these are false.
-
 /-! ### emod -/
 
 theorem mod_def' (m n : Int) : m % n = emod m n := rfl
@@ -629,6 +607,12 @@ theorem dvd_emod_sub_self {x : Int} {m : Nat} : (m : Int) ∣ x % m - x := by
 @[simp] theorem emod_one (a : Int) : a % 1 = 0 := by
   simp [emod_def, Int.one_mul, Int.sub_self]
 
+@[simp] protected theorem ediv_self {a : Int} (H : a ≠ 0) : a / a = 1 := by
+  have := Int.mul_ediv_cancel 1 H; rwa [Int.one_mul] at this
+
+@[simp] protected theorem neg_ediv_self (a : Int) (h : a ≠ 0) : (-a) / a = -1 := by
+  rw [neg_ediv_of_dvd (Int.dvd_refl a), Int.ediv_self h]
+
 @[simp]
 theorem emod_sub_cancel (x y : Int): (x - y) % y = x % y := by
   by_cases h : y = 0
@@ -762,8 +746,6 @@ theorem ediv_eq_ediv_of_mul_eq_mul {a b c d : Int}
 
 /-! ### tdiv -/
 
--- `tdiv` analogues of `ediv` lemmas from `Bootstrap.lean`
-
 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
@@ -771,12 +753,12 @@ unseal Nat.div in
   | ofNat _, succ _ | -[_+1], 0 | -[_+1], -[_+1] => rfl
 
 /-!
-There are no lemmas
-* `add_mul_tdiv_right : c ≠ 0 → (a + b * c).tdiv c = a.tdiv c + b`
-* `add_mul_tdiv_left : b ≠ 0 → (a + b * c).tdiv b = a.tdiv b + c`
-* `add_tdiv_of_dvd_right : c ∣ b → (a + b).tdiv c = a.tdiv c + b.tdiv c`
-* `add_tdiv_of_dvd_left : c ∣ a → (a + b).tdiv c = a.tdiv c + b.tdiv c`
-because these statements are all incorrect, and require awkward conditional off-by-one corrections.
+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
@@ -785,10 +767,8 @@ because these statements are all incorrect, and require awkward conditional off-
 @[simp] theorem mul_tdiv_cancel_left (b : Int) (H : a ≠ 0) : (a * b).tdiv a = b :=
   Int.mul_comm .. ▸ Int.mul_tdiv_cancel _ H
 
--- `tdiv` analogues of `ediv` lemmas given above
-
--- There are no lemmas `tdiv_nonneg_iff_of_pos`, `tdiv_neg_of_neg_of_pos`, or `negSucc_tdiv`
--- corresponding to `ediv_nonneg_iff_of_pos`, `ediv_neg_of_neg_of_pos`, or `negSucc_ediv` as they require awkward corrections.
+-- 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
@@ -812,12 +792,9 @@ theorem tdiv_nonneg_of_nonpos_of_nonpos {a b : Int} (Ha : a ≤ 0) (Hb : b ≤ 0
           exact ediv_pos_of_neg_of_neg h'' h'
       omega
 
-protected theorem tdiv_nonpos_of_nonneg_of_nonpos {a b : Int} (Ha : 0 ≤ a) (Hb : b ≤ 0) : a.tdiv b ≤ 0 :=
+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)
 
-@[deprecated Int.tdiv_nonpos_of_nonneg_of_nonpos (since := "2025-03-04")]
-abbrev tdiv_nonpos := @Int.tdiv_nonpos_of_nonneg_of_nonpos
-
 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
@@ -863,9 +840,6 @@ 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
 
-@[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
-
 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]
@@ -875,6 +849,34 @@ 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]
 
+@[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_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 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_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_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_tdiv_cancel_left _ cz, Int.mul_tdiv_cancel_left _ cz]
+
+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 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_tdiv_cancel_left _ az, Int.mul_assoc, Int.mul_tdiv_cancel_left _ az]
+      apply Int.dvd_mul_right
+
 @[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
@@ -884,15 +886,13 @@ protected theorem neg_tdiv_neg (a b : Int) : (-a).tdiv (-b) = a.tdiv b := by
 
 /-! ### tmod -/
 
--- `tmod` analogues of `emod` lemmas from `Bootstrap.lean`
-
 theorem ofNat_tmod (m n : Nat) : (↑(m % n) : Int) = tmod m n := rfl
 
 @[simp] theorem tmod_one (a : Int) : tmod a 1 = 0 := by
   simp [tmod_def, Int.tdiv_one, Int.one_mul, Int.sub_self]
 
-theorem tmod_nonneg : ∀ {a : Int} (b : Int), 0 ≤ a → 0 ≤ tmod a b
-  | ofNat _, -[_+1], _ | ofNat _, ofNat _, _ => ofNat_nonneg _
+theorem tmod_eq_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : tmod a b = a := by
+  rw [tmod_eq_emod_of_nonneg H1, emod_eq_of_lt H1 H2]
 
 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
@@ -900,23 +900,12 @@ theorem tmod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : tmod a b < b :=
   | -[_+1], _, ⟨n, rfl⟩ => Int.lt_of_le_of_lt
     (Int.neg_nonpos_of_nonneg <| Int.ofNat_nonneg _) (ofNat_pos.2 n.succ_pos)
 
+theorem tmod_nonneg : ∀ {a : Int} (b : Int), 0 ≤ a → 0 ≤ tmod a b
+  | ofNat _, -[_+1], _ | ofNat _, ofNat _, _ => ofNat_nonneg _
+
 @[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 neg_tmod (a b : Int) : tmod (-a) b = -tmod a b := by
-  rw [tmod_def, Int.neg_tdiv, Int.mul_neg, tmod_def]
-  omega
-
--- The following statements for `tmod` are false:
--- `add_mul_tmod_self {a b c : Int} : (a + b * c).tmod c = a.tmod c`
--- `add_mul_tmod_self_left (a b c : Int) : (a + b * c).tmod b = a.tmod b`
--- `tmod_add_tmod (m n k : Int) : (m.tmod n + k).tmod n = (m + k).tmod n`
--- `add_tmod_tmod (m n k : Int) : (m + n.tmod k).tmod k = (m + n).tmod k`
--- `add_tmod (a b n : Int) : (a + b).tmod n = (a.tmod n + b.tmod n).tmod n`
--- `add_tmod_eq_add_tmod_right {m n k : Int} (i : Int) : (m.tmod n = k.tmod n) → (m + i).tmod n = (k + i).tmod n`
--- `tmod_add_cancel_right {m n k : Int} (i) : (m + i).tmod n = (k + i).tmod n ↔ m.tmod n = k.tmod n`
--- `sub_tmod (a b n : Int) : (a - b).tmod n = (a.tmod n - b.tmod n).tmod n`
-
 @[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.tmod_def, Int.mul_tdiv_cancel _ h, Int.mul_comm, Int.sub_self]
@@ -924,78 +913,9 @@ theorem tmod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : tmod a b < b :=
 @[simp] theorem mul_tmod_right (a b : Int) : (a * b).tmod a = 0 := by
   rw [Int.mul_comm, mul_tmod_left]
 
-/--
-If a predicate on the integers is invariant under negation,
-then it is sufficient to prove it for the nonnegative integers.
--/
-theorem wlog_sign {P : Int → Prop} (inv : ∀ a, P a ↔ P (-a)) (w : ∀ n : Nat, P n) (a : Int) : P a := by
-  cases a with
-  | ofNat n => exact w n
-  | negSucc n =>
-    rw [negSucc_eq, ← inv, ← ofNat_succ]
-    apply w
-
-attribute [local simp] Int.neg_inj
-
-theorem mul_tmod (a b n : Int) : (a * b).tmod n = (a.tmod n * b.tmod n).tmod n := by
-  induction a using wlog_sign
-  case inv => simp
-  induction b using wlog_sign
-  case inv => simp
-  induction n using wlog_sign
-  case inv => simp
-  simp only [← Int.natCast_mul, ← ofNat_tmod]
-  rw [Nat.mul_mod]
-
-@[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 tmod_tmod_of_dvd (n : Int) {m k : Int}
-    (h : m ∣ k) : (n.tmod k).tmod m = n.tmod m := by
-  induction n using wlog_sign
-  case inv => simp
-  induction k using wlog_sign
-  case inv => simp [Int.dvd_neg]
-  induction m using wlog_sign
-  case inv => simp
-  simp only [← Int.natCast_mul, ← ofNat_tmod]
-  norm_cast at h
-  rw [Nat.mod_mod_of_dvd _ h]
-
-@[simp] theorem tmod_tmod (a b : Int) : (a.tmod b).tmod b = a.tmod b :=
-  tmod_tmod_of_dvd a (Int.dvd_refl b)
-
 theorem tmod_eq_zero_of_dvd : ∀ {a b : Int}, a ∣ b → tmod b a = 0
   | _, _, ⟨_, rfl⟩ => mul_tmod_right ..
 
--- `tmod` analogues of `emod` lemmas from above
-
-theorem tmod_eq_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : tmod a b = a := by
-  rw [tmod_eq_emod_of_nonneg H1, emod_eq_of_lt H1 H2]
-
--- lemmas about `tmod` without `emod` analogues
-
-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_tdiv_abs (a : Int) : sign a = a.tdiv (natAbs a) :=
-  if az : a = 0 then by simp [az] else
-    (Int.tdiv_eq_of_eq_mul_left (ofNat_ne_zero.2 <| natAbs_ne_zero.2 az)
-      (sign_mul_natAbs _).symm).symm
-
-/-! properties of `tdiv` and `tmod` -/
-
-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 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_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⟩
-
 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⟩
 
@@ -1016,6 +936,9 @@ protected theorem mul_tdiv_cancel' {a b : Int} (H : a ∣ b) : a * b.tdiv a = b
 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 tmod_self {a : Int} : a.tmod a = 0 := by
+  have := mul_tmod_left 1 a; rwa [Int.one_mul] at this
+
 @[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
@@ -1036,6 +959,7 @@ 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 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]
 
@@ -1044,50 +968,33 @@ protected theorem eq_zero_of_tdiv_eq_zero {d n : Int} (h : d ∣ n) (H : n.tdiv
   refine ⟨fun h => ?_, congrArg (tdiv · d)⟩
   rw [← Int.mul_tdiv_cancel' hda, ← Int.mul_tdiv_cancel' hdb, h]
 
-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_tdiv_cancel_left _ cz, Int.mul_tdiv_cancel_left _ cz]
+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 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 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_tdiv_cancel_left _ az, Int.mul_assoc, Int.mul_tdiv_cancel_left _ az]
-      apply Int.dvd_mul_right
-
-/-! ### `tdiv` and ordering -/
-
--- Theorems about `tdiv` and ordering, whose `ediv` analogues are in `Bootstrap.lean`.
-
-theorem mul_tdiv_self_le {x k : Int} (h : 0 ≤ x) : k * (x.tdiv k) ≤ x := by
-  by_cases w : k = 0
-  · simp [w, h]
-  · rw [tdiv_eq_ediv_of_nonneg h]
-    apply mul_ediv_self_le w
-
-theorem lt_mul_tdiv_self_add {x k : Int} (h : 0 < k) : x < k * (x.tdiv k) + k := by
-  rw [tdiv_eq_ediv, sign_eq_one_of_pos h]
-  have := lt_mul_ediv_self_add (x := x) h
-  split <;> simp [Int.mul_add] <;> omega
+protected theorem sign_eq_tdiv_abs (a : Int) : sign a = a.tdiv (natAbs a) :=
+  if az : a = 0 then by simp [az] else
+    (Int.tdiv_eq_of_eq_mul_left (ofNat_ne_zero.2 <| natAbs_ne_zero.2 az)
+      (sign_mul_natAbs _).symm).symm
 
 /-! ### fdiv -/
 
--- There is no theorem `fdiv_neg : ∀ a b : Int, a.fdiv (-b) = -(a.fdiv b)`
--- because this is false, for example at `a = 2`, `b = 3`, as `-1 ≠ 0`.
+theorem fdiv_nonneg {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a.fdiv b :=
+  match a, b, eq_ofNat_of_zero_le Ha, eq_ofNat_of_zero_le Hb with
+  | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => ofNat_fdiv .. ▸ ofNat_zero_le _
 
-theorem add_mul_fdiv_right (a b : Int) {c : Int} (H : c ≠ 0) : (a + b * c).fdiv c = a.fdiv c + b := by
-  rw [fdiv_eq_ediv, add_mul_ediv_right _ _ H, fdiv_eq_ediv]
-  simp only [Int.dvd_add_left (Int.dvd_mul_left _ _)]
-  split <;> omega
+unseal Nat.div in
+theorem fdiv_nonpos : ∀ {a b : Int}, 0 ≤ a → b ≤ 0 → a.fdiv b ≤ 0
+  | 0, 0, _, _ | 0, -[_+1], _, _ | succ _, 0, _, _ | succ _, -[_+1], _, _ => ⟨_⟩
 
-theorem add_mul_fdiv_left (a : Int) {b : Int}
-    (c : Int) (H : b ≠ 0) : (a + b * c).fdiv b = a.fdiv b + c := by
-  rw [Int.mul_comm, Int.add_mul_fdiv_right _ _ H]
+theorem fdiv_neg' : ∀ {a b : Int}, a < 0 → 0 < b → a.fdiv b < 0
+  | -[_+1], succ _, _, _ => negSucc_lt_zero _
+
+@[simp] theorem fdiv_one : ∀ a : Int, a.fdiv 1 = a
+  | 0 => rfl
+  | succ _ => congrArg Nat.cast (Nat.div_one _)
+  | -[_+1] => congrArg negSucc (Nat.div_one _)
 
 @[simp] theorem mul_fdiv_cancel (a : Int) {b : Int} (H : b ≠ 0) : fdiv (a * b) b = a :=
   if b0 : 0 ≤ b then by
@@ -1103,174 +1010,32 @@ theorem add_mul_fdiv_left (a : Int) {b : Int}
 @[simp] theorem mul_fdiv_cancel_left (b : Int) (H : a ≠ 0) : fdiv (a * b) a = b :=
   Int.mul_comm .. ▸ Int.mul_fdiv_cancel _ H
 
-theorem add_fdiv_of_dvd_right {a b c : Int} (H : c ∣ b) : (a + b).fdiv c = a.fdiv c + b.fdiv c := by
-  by_cases h : c = 0
-  · simp [h]
-  · obtain ⟨d, rfl⟩ := H
-    rw [add_mul_fdiv_left _ _ h]
-    simp [h]
-
-theorem add_fdiv_of_dvd_left {a b c : Int} (H : c ∣ a) : (a + b).fdiv c = a.fdiv c + b.fdiv c := by
-  rw [Int.add_comm, Int.add_fdiv_of_dvd_right H, Int.add_comm]
-
-theorem fdiv_nonneg {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a.fdiv b :=
-  match a, b, eq_ofNat_of_zero_le Ha, eq_ofNat_of_zero_le Hb with
-  | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => ofNat_fdiv .. ▸ ofNat_zero_le _
-
-theorem fdiv_nonneg_of_nonpos_of_nonpos {a b : Int} (Ha : a ≤ 0) (Hb : b ≤ 0) : 0 ≤ a.fdiv b := by
-  rw [fdiv_eq_ediv]
-  by_cases ha : a = 0
-  · simp [ha]
-  · by_cases hb : b = 0
-    · simp [hb]
-    · have : 0 < a / b := ediv_pos_of_neg_of_neg (by omega) (by omega)
-      split <;> omega
-
-unseal Nat.div in
-theorem fdiv_nonpos_of_nonneg_of_nonpos : ∀ {a b : Int}, 0 ≤ a → b ≤ 0 → a.fdiv b ≤ 0
-  | 0, 0, _, _ | 0, -[_+1], _, _ | succ _, 0, _, _ | succ _, -[_+1], _, _ => ⟨_⟩
-
-@[deprecated fdiv_nonpos_of_nonneg_of_nonpos (since := "2025-03-04")]
-abbrev fdiv_nonpos := @fdiv_nonpos_of_nonneg_of_nonpos
-
-theorem fdiv_neg_of_neg_of_pos : ∀ {a b : Int}, a < 0 → 0 < b → a.fdiv b < 0
-  | -[_+1], succ _, _, _ => negSucc_lt_zero _
-
-@[deprecated fdiv_neg_of_neg_of_pos (since := "2025-03-04")]
-abbrev fdiv_neg := @fdiv_neg_of_neg_of_pos
-
-theorem fdiv_eq_zero_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : a.fdiv b = 0 := by
-  rw [fdiv_eq_ediv, if_pos, Int.sub_zero]
-  · apply ediv_eq_zero_of_lt (by omega) (by omega)
-  · left; omega
-
-@[simp] theorem mul_fdiv_mul_of_pos {a : Int}
-    (b c : Int) (H : 0 < a) : (a * b).fdiv (a * c) = b.fdiv c := by
-  rw [fdiv_eq_ediv, mul_ediv_mul_of_pos _ _ H, fdiv_eq_ediv]
-  congr 2
-  simp [Int.mul_dvd_mul_iff_left (Int.ne_of_gt H)]
-  constructor
-  · rintro (h | h)
-    · exact .inl (Int.nonneg_of_mul_nonneg_right h H)
-    · exact .inr h
-  · rintro (h | h)
-    · exact .inl (Int.mul_nonneg (by omega) h)
-    · exact .inr h
-
-@[simp] theorem mul_fdiv_mul_of_pos_left
-    (a : Int) {b : Int} (c : Int) (H : 0 < b) : (a * b).fdiv (c * b) = a.fdiv c := by
-  rw [Int.mul_comm a b, Int.mul_comm c b, Int.mul_fdiv_mul_of_pos _ _ H]
-
-@[simp] theorem fdiv_one : ∀ a : Int, a.fdiv 1 = a
-  | 0 => rfl
-  | succ _ => congrArg Nat.cast (Nat.div_one _)
-  | -[_+1] => congrArg negSucc (Nat.div_one _)
-
-protected theorem fdiv_eq_of_eq_mul_right {a b c : Int}
-    (H1 : b ≠ 0) (H2 : a = b * c) : a.fdiv b = c := by rw [H2, Int.mul_fdiv_cancel_left _ H1]
-
-protected theorem eq_fdiv_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 fdiv_eq_of_eq_mul_left {a b c : Int}
-    (H1 : b ≠ 0) (H2 : a = c * b) : a.fdiv b = c :=
-  Int.fdiv_eq_of_eq_mul_right H1 (by rw [Int.mul_comm, H2])
-
-protected theorem eq_fdiv_of_mul_eq_left {a b c : Int}
-    (H1 : b ≠ 0) (H2 : a * b = c) : a = c.fdiv b :=
-  (Int.fdiv_eq_of_eq_mul_left H1 H2.symm).symm
-
 @[simp] protected theorem fdiv_self {a : Int} (H : a ≠ 0) : a.fdiv a = 1 := by
   have := Int.mul_fdiv_cancel 1 H; rwa [Int.one_mul] at this
 
--- `neg_fdiv : ∀ a b : Int, (-a).fdiv b = -(a.fdiv b)` is untrue.
-
-protected theorem neg_fdiv_neg (a b : Int) : (-a).fdiv (-b) = a.fdiv b := by
-  match a, b with
-  | 0, 0 => rfl
-  | 0, ofNat b => simp
-  | 0, -[b+1] => simp
-  | ofNat (a + 1), 0 => simp
-  | ofNat (a + 1), ofNat (b + 1) =>
-    unfold fdiv
-    simp only [ofNat_eq_coe, natCast_add, Nat.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, natCast_add, Nat.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, natCast_add, Nat.cast_ofNat_Int, Nat.succ_eq_add_one]
-    rw [neg_negSucc, ← negSucc_eq]
-  | -[a+1], -[b+1] =>
-    unfold fdiv
-    simp only [ofNat_eq_coe, ofNat_ediv, Nat.succ_eq_add_one, natCast_add, Nat.cast_ofNat_Int]
-    rw [neg_negSucc, neg_negSucc]
-    simp
-
--- `natAbs_fdiv (a b : Int) : natAbs (a.fdiv b) = (natAbs a).div (natAbs b)` is untrue.
+theorem lt_fdiv_add_one_mul_self (a : Int) {b : Int} (H : 0 < b) : a < (a.fdiv b + 1) * b :=
+  Int.fdiv_eq_ediv_of_nonneg _ (Int.le_of_lt H) ▸ lt_ediv_add_one_mul_self a H
 
 /-! ### fmod -/
 
--- `fmod` analogues of `emod` lemmas from `Bootstrap.lean`
-
 theorem ofNat_fmod (m n : Nat) : ↑(m % n) = fmod m n := by
   cases m <;> simp [fmod, Nat.succ_eq_add_one]
 
 @[simp] theorem fmod_one (a : Int) : a.fmod 1 = 0 := by
   simp [fmod_def, Int.one_mul, Int.sub_self]
 
+theorem fmod_eq_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : a.fmod b = a := by
+  rw [fmod_eq_emod_of_nonneg _ (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_tmod_of_nonneg ha hb ▸ tmod_nonneg _ ha
 
-theorem fmod_nonneg_of_pos (a : Int) {b : Int} (hb : 0 < b) : 0 ≤ a.fmod b :=
+theorem fmod_nonneg' (a : Int) {b : Int} (hb : 0 < b) : 0 ≤ a.fmod b :=
   fmod_eq_emod_of_nonneg _ (Int.le_of_lt hb) ▸ emod_nonneg _ (Int.ne_of_lt hb).symm
 
-@[deprecated fmod_nonneg_of_pos (since := "2025-03-04")]
-abbrev fmod_nonneg' := @fmod_nonneg_of_pos
-
 theorem fmod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : a.fmod b < b :=
   fmod_eq_emod_of_nonneg _ (Int.le_of_lt H) ▸ emod_lt_of_pos a H
 
--- There is no `fmod_neg : ∀ {a b : Int}, a.fmod (-b) = -a.fmod b` as this is false.
-
-@[simp] theorem add_mul_fmod_self {a b c : Int} : (a + b * c).fmod c = a.fmod c := by
-  rw [fmod_eq_emod, add_mul_emod_self, fmod_eq_emod]
-  simp
-
-@[simp] theorem add_mul_fmod_self_left (a b c : Int) : (a + b * c).fmod b = a.fmod b := by
-  rw [Int.mul_comm, Int.add_mul_fmod_self]
-
-@[simp] theorem fmod_add_fmod (m n k : Int) : (m.fmod n + k).fmod n = (m + k).fmod n := by
-  by_cases h : n = 0
-  · simp [h]
-  rw [fmod_def, fmod_def]
-  conv => rhs; rw [fmod_def]
-  have : m - n * m.fdiv n + k = m + k + n * (- m.fdiv n) := by simp [Int.mul_neg]; omega
-  rw [this, add_fdiv_of_dvd_right (Int.dvd_mul_right ..), Int.mul_add, mul_fdiv_cancel_left _ h]
-  omega
-
-@[simp] theorem add_fmod_fmod (m n k : Int) : (m + n.fmod k).fmod k = (m + n).fmod k := by
-  rw [Int.add_comm, Int.fmod_add_fmod, Int.add_comm]
-
-theorem add_fmod (a b n : Int) : (a + b).fmod n = (a.fmod n + b.fmod n).fmod n := by
-  simp
-
-theorem add_fmod_eq_add_fmod_right {m n k : Int} (i : Int)
-    (H : m.fmod n = k.fmod n) : (m + i).fmod n = (k + i).fmod n := by
-  rw [add_fmod]
-  conv => rhs; rw [add_fmod]
-  rw [H]
-
-theorem fmod_add_cancel_right {m n k : Int} (i) : (m + i).fmod n = (k + i).fmod n ↔ m.fmod n = k.fmod n :=
-  ⟨fun H => by
-    have := add_fmod_eq_add_fmod_right (-i) H
-    rwa [Int.add_neg_cancel_right, Int.add_neg_cancel_right] at this,
-  add_fmod_eq_add_fmod_right _⟩
-
 @[simp] theorem mul_fmod_left (a b : Int) : (a * b).fmod b = 0 :=
   if h : b = 0 then by simp [h, Int.mul_zero] else by
     rw [Int.fmod_def, Int.mul_fdiv_cancel _ h, Int.mul_comm, Int.sub_self]
@@ -1278,56 +1043,9 @@ theorem fmod_add_cancel_right {m n k : Int} (i) : (m + i).fmod n = (k + i).fmod
 @[simp] theorem mul_fmod_right (a b : Int) : (a * b).fmod a = 0 := by
   rw [Int.mul_comm, mul_fmod_left]
 
-theorem mul_fmod (a b n : Int) : (a * b).fmod n = (a.fmod n * b.fmod n).fmod n := by
-  conv => lhs; rw [
-    ← fmod_add_fdiv a n, ← fmod_add_fdiv' b n, Int.add_mul, Int.mul_add, Int.mul_add,
-    Int.mul_assoc, Int.mul_assoc, ← Int.mul_add n _ _, add_mul_fmod_self_left,
-    ← Int.mul_assoc, add_mul_fmod_self]
-
 @[simp] theorem fmod_self {a : Int} : a.fmod a = 0 := by
   have := mul_fmod_left 1 a; rwa [Int.one_mul] at this
 
-@[simp] theorem fmod_fmod_of_dvd (n : Int) {m k : Int}
-    (h : m ∣ k) : (n.fmod k).fmod m = n.fmod m := by
-  conv => rhs; rw [← fmod_add_fdiv n k]
-  match k, h with
-  | _, ⟨t, rfl⟩ => rw [Int.mul_assoc, add_mul_fmod_self_left]
-
-@[simp] theorem fmod_fmod (a b : Int) : (a.fmod b).fmod b = a.fmod b :=
-  fmod_fmod_of_dvd _ (Int.dvd_refl b)
-
-theorem sub_fmod (a b n : Int) : (a - b).fmod n = (a.fmod n - b.fmod n).fmod n := by
-  apply (fmod_add_cancel_right b).mp
-  rw [Int.sub_add_cancel, ← Int.add_fmod_fmod, Int.sub_add_cancel, fmod_fmod]
-
-theorem fmod_eq_zero_of_dvd : ∀ {a b : Int}, a ∣ b → b.fmod a = 0
-  | _, _, ⟨_, rfl⟩ => mul_fmod_right ..
-
--- `fmod` analogues of `emod` lemmas from above
-
-theorem fmod_eq_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : a.fmod b = a := by
-  rw [fmod_eq_emod_of_nonneg _ (Int.le_trans H1 (Int.le_of_lt H2)), emod_eq_of_lt H1 H2]
-
--- lemmas about `fmod` without `emod` analogues
-
-theorem fdiv_sign {a b : Int} : a.fdiv (sign b) = a * sign b := by
-  rw [fdiv_eq_ediv]
-  rcases sign_trichotomy b with h | h | h <;> simp [h]
-
-protected theorem sign_eq_fdiv_abs (a : Int) : sign a = a.fdiv (natAbs a) :=
-  if az : a = 0 then by simp [az] else
-    (Int.fdiv_eq_of_eq_mul_left (ofNat_ne_zero.2 <| natAbs_ne_zero.2 az)
-      (sign_mul_natAbs _).symm).symm
-
-/-! ### properties of `fdiv` and `fmod` -/
-
-/-! ### `fdiv` and ordering -/
-
--- Theorems about `fdiv` and ordering, whose `ediv` analogues are in `Bootstrap.lean`.
-
-theorem lt_fdiv_add_one_mul_self (a : Int) {b : Int} (H : 0 < b) : a < (a.fdiv b + 1) * b :=
-  Int.fdiv_eq_ediv_of_nonneg _ (Int.le_of_lt H) ▸ lt_ediv_add_one_mul_self a H
-
 /-! ### bmod -/
 
 @[simp]

src/Init/Data/Int/Order.lean

@@ -139,9 +139,6 @@ protected theorem not_le_of_gt {a b : Int} (h : b < a) : ¬a ≤ b :=
 @[simp] protected theorem not_lt {a b : Int} : ¬a < b ↔ b ≤ a :=
   by rw [← Int.not_le, Decidable.not_not]
 
-protected theorem le_of_not_gt {a b : Int} (h : ¬ a > b) : a ≤ b :=
-  Int.not_lt.mp h
-
 protected theorem lt_trichotomy (a b : Int) : a < b ∨ a = b ∨ b < a :=
   if eq : a = b then .inr <| .inl eq else
   if le : a ≤ b then .inl <| Int.lt_iff_le_and_ne.2 ⟨le, eq⟩ else
@@ -941,22 +938,6 @@ protected theorem mul_self_le_mul_self {a b : Int} (h1 : 0 ≤ a) (h2 : a ≤ b)
 protected theorem mul_self_lt_mul_self {a b : Int} (h1 : 0 ≤ a) (h2 : a < b) : a * a < b * b :=
   Int.mul_lt_mul' (Int.le_of_lt h2) h2 h1 (Int.lt_of_le_of_lt h1 h2)
 
-protected theorem nonneg_of_mul_nonneg_left {a b : Int}
-    (h : 0 ≤ a * b) (hb : 0 < b) : 0 ≤ a :=
-  Int.le_of_not_gt fun ha => Int.not_le_of_gt (Int.mul_neg_of_neg_of_pos ha hb) h
-
-protected theorem nonneg_of_mul_nonneg_right {a b : Int}
-    (h : 0 ≤ a * b) (ha : 0 < a) : 0 ≤ b :=
-  Int.le_of_not_gt fun hb => Int.not_le_of_gt (Int.mul_neg_of_pos_of_neg ha hb) h
-
-protected theorem nonpos_of_mul_nonpos_left {a b : Int}
-    (h : a * b ≤ 0) (hb : 0 < b) : a ≤ 0 :=
-  Int.le_of_not_gt fun ha : a > 0 => Int.not_le_of_gt (Int.mul_pos ha hb) h
-
-protected theorem nonpos_of_mul_nonpos_right {a b : Int}
-    (h : a * b ≤ 0) (ha : 0 < a) : b ≤ 0 :=
-  Int.le_of_not_gt fun hb : b > 0 => Int.not_le_of_gt (Int.mul_pos ha hb) h
-
 /- ## sign -/
 
 @[simp] theorem sign_zero : sign 0 = 0 := rfl
@@ -1040,12 +1021,6 @@ theorem sign_eq_neg_one_iff_neg {a : Int} : sign a = -1 ↔ a < 0 :=
 @[simp] theorem sign_mul_self : sign i * i = natAbs i := by
   rw [Int.mul_comm, mul_sign_self]
 
-theorem sign_trichotomy (a : Int) : sign a = 1 ∨ sign a = 0 ∨ sign a = -1 := by
-  match a with
-  | 0 => simp
-  | .ofNat (_ + 1) => simp
-  | .negSucc _ => simp
-
 /- ## natAbs -/
 
 theorem natAbs_ne_zero {a : Int} : a.natAbs ≠ 0 ↔ a ≠ 0 := not_congr Int.natAbs_eq_zero

src/Lean/Elab/Deriving/DecEq.lean

@@ -134,7 +134,9 @@ partial def mkEnumOfNat (declName : Name) : MetaM Unit := do
   let enumType := mkConst declName
   let ctors := indVal.ctors.toArray
   withLocalDeclD `n (mkConst ``Nat) fun n => do
-    let cond := mkConst ``cond [levelZero]
+    -- After the next stage0 update, this can be reverted to
+    -- let cond := mkConst ``cond [1]
+    let cond := (← mkAppOptM ``cond #[enumType]).appFn!
     let rec mkDecTree (low high : Nat) : Expr :=
       if low + 1 == high then
         mkConst ctors[low]!

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Enums.lean

@@ -105,7 +105,7 @@ def getEqIffEnumToBitVecEqFor (declName : Name) : MetaM Name := do
     let inverseValue ←
       withLocalDeclD `x bvType fun x => do
         let instBeq ← synthInstance (mkApp (mkConst ``BEq [0]) bvType)
-        let inv := mkInverse x declType instBeq ctors (BitVec.ofNat bvSize 0) (mkConst ctors.head!)
+        let inv ← mkInverse x declType instBeq ctors (BitVec.ofNat bvSize 0) (mkConst ctors.head!)
         mkLambdaFVars #[x] inv
 
     let value ←
@@ -144,9 +144,9 @@ def getEqIffEnumToBitVecEqFor (declName : Name) : MetaM Name := do
 where
   mkInverse {w : Nat} (input : Expr) (retType : Expr) (instBEq : Expr) (ctors : List Name)
       (counter : BitVec w) (acc : Expr) :
-      Expr :=
+      MetaM Expr := do
     match ctors with
-    | [] => acc
+    | [] => pure acc
     | ctor :: ctors =>
       let eq :=
         mkApp4
@@ -155,7 +155,10 @@ where
           instBEq
           input
           (toExpr counter)
-      let acc := mkApp4 (mkConst ``cond [0]) retType eq (mkConst ctor) acc
+      -- After the next stage0 update, this can be reverted to
+      -- let acc := mkApp4 (mkConst ``cond [1]) retType eq (mkConst ctor) acc
+      -- and mkInverse can be pure again
+      let acc ← mkAppOptM ``cond #[retType, eq, mkConst ctor, acc]
       mkInverse input retType instBEq ctors (counter + 1) acc
 
 /--

src/Lean/Elab/Tactic/Grind.lean

@@ -167,7 +167,7 @@ def evalGrindCore
   let only := only.isSome
   let params := if let some params := params then params.getElems else #[]
   if Grind.grind.warning.get (← getOptions) then
-    logWarningAt ref "The `grind` tactic is experimental and still under development. Avoid using it in production projects"
+    logWarningAt ref "The `grind` tactic is experimental and still under development. Avoid using it in production projects."
   let declName := (← Term.getDeclName?).getD `_grind
   withMainContext do
     let result ← grind (← getMainGoal) config only params declName fallback

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Cooper.lean

@@ -1,24 +0,0 @@
-/-
-Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
-
-namespace Lean.Meta.Grind.Arith.Cutsat
-
-def CooperSplit.numCases (s : CooperSplit) : Nat :=
-  let a  := s.c₁.p.leadCoeff
-  let b  := s.c₂.p.leadCoeff
-  match s.c₃? with
-  | none => if s.left then a.natAbs else b.natAbs
-  | some c₃ =>
-    let c  := c₃.p.leadCoeff
-    let d  := c₃.d
-    if s.left then
-      Int.lcm a (a * d / Int.gcd (a * d) c)
-    else
-      Int.lcm b (b * d / Int.gcd (b * d) c)
-
-end Lean.Meta.Grind.Arith.Cutsat

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
-import Lean.Meta.Tactic.Grind.Arith.Cutsat.Cooper
 
 namespace Lean.Meta.Grind.Arith.Cutsat
 
@@ -66,25 +65,27 @@ partial def DvdCnstr.toExprProof (c' : DvdCnstr) : ProofM Expr := c'.caching do
     return mkApp10 (mkConst ``Int.Linear.eq_dvd_subst)
       (← getContext) (toExpr x) (toExpr c₁.p) (toExpr c₂.d) (toExpr c₂.p) (toExpr c'.d) (toExpr c'.p)
       reflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
-  | .cooper₁ c =>
-    let p₁ := c.c₁.p
-    let p₂ := c.c₂.p
-    match c.c₃? with
+  | .cooper₁ s =>
+    let { c₁, c₂, c₃?, left } := s.pred
+    let p₁ := c₁.p
+    let p₂ := c₂.p
+    match c₃? with
     | none =>
-      let thmName := if c.left then ``Int.Linear.cooper_left_split_dvd else ``Int.Linear.cooper_right_split_dvd
+      let thmName := if left then ``Int.Linear.cooper_left_split_dvd else ``Int.Linear.cooper_right_split_dvd
       return mkApp8 (mkConst thmName)
-        (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c.k) (toExpr c'.d) (toExpr c'.p) (← c.toExprProof) reflBoolTrue
+        (← getContext) (toExpr p₁) (toExpr p₂) (toExpr s.k) (toExpr c'.d) (toExpr c'.p) (← s.toExprProof) reflBoolTrue
     | some c₃ =>
-      let thmName := if c.left then ``Int.Linear.cooper_dvd_left_split_dvd1 else ``Int.Linear.cooper_dvd_right_split_dvd1
+      let thmName := if left then ``Int.Linear.cooper_dvd_left_split_dvd1 else ``Int.Linear.cooper_dvd_right_split_dvd1
       return mkApp10 (mkConst thmName)
-        (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c₃.p) (toExpr c₃.d) (toExpr c.k) (toExpr c'.d) (toExpr c'.p) (← c.toExprProof) reflBoolTrue
-  | .cooper₂ c =>
-    let p₁ := c.c₁.p
-    let p₂ := c.c₂.p
-    let some c₃ := c.c₃? | throwError "`grind` internal error, unexpected `cooper₂` proof"
-    let thmName := if c.left then ``Int.Linear.cooper_dvd_left_split_dvd2 else ``Int.Linear.cooper_dvd_right_split_dvd2
+        (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c₃.p) (toExpr c₃.d) (toExpr s.k) (toExpr c'.d) (toExpr c'.p) (← s.toExprProof) reflBoolTrue
+  | .cooper₂ s =>
+    let { c₁, c₂, c₃?, left } := s.pred
+    let p₁ := c₁.p
+    let p₂ := c₂.p
+    let some c₃ := c₃? | throwError "`grind` internal error, unexpected `cooper₂` proof"
+    let thmName := if left then ``Int.Linear.cooper_dvd_left_split_dvd2 else ``Int.Linear.cooper_dvd_right_split_dvd2
     return mkApp10 (mkConst thmName)
-      (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c₃.p) (toExpr c₃.d) (toExpr c.k) (toExpr c'.d) (toExpr c'.p) (← c.toExprProof) reflBoolTrue
+      (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c₃.p) (toExpr c₃.d) (toExpr s.k) (toExpr c'.d) (toExpr c'.p) (← s.toExprProof) reflBoolTrue
 
 partial def LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr := c'.caching do
   match c'.h with
@@ -122,19 +123,20 @@ partial def LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr := c'.caching do
     let hNot := mkLambda `h .default (mkIntLE (← p₂.denoteExpr') (mkIntLit 0)) (hFalse.abstract #[mkFVar fvarId])
     return mkApp7 (mkConst ``Int.Linear.diseq_split_resolve)
       (← getContext) (toExpr c₁.p) (toExpr p₂) (toExpr c'.p) reflBoolTrue (← c₁.toExprProof) hNot
-  | .cooper c =>
-    let p₁ := c.c₁.p
-    let p₂ := c.c₂.p
-    let coeff := if c.left then p₁.leadCoeff else p₂.leadCoeff
-    match c.c₃? with
+  | .cooper s =>
+    let { c₁, c₂, c₃?, left } := s.pred
+    let p₁ := c₁.p
+    let p₂ := c₂.p
+    let coeff := if left then p₁.leadCoeff else p₂.leadCoeff
+    match c₃? with
     | none =>
-      let thmName := if c.left then ``Int.Linear.cooper_left_split_ineq else ``Int.Linear.cooper_right_split_ineq
+      let thmName := if left then ``Int.Linear.cooper_left_split_ineq else ``Int.Linear.cooper_right_split_ineq
       return mkApp8 (mkConst thmName)
-        (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c.k) (toExpr coeff) (toExpr c'.p) (← c.toExprProof) reflBoolTrue
+        (← getContext) (toExpr p₁) (toExpr p₂) (toExpr s.k) (toExpr coeff) (toExpr c'.p) (← s.toExprProof) reflBoolTrue
     | some c₃ =>
-      let thmName := if c.left then ``Int.Linear.cooper_dvd_left_split_ineq else ``Int.Linear.cooper_dvd_right_split_ineq
+      let thmName := if left then ``Int.Linear.cooper_dvd_left_split_ineq else ``Int.Linear.cooper_dvd_right_split_ineq
       return mkApp10 (mkConst thmName)
-        (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c₃.p) (toExpr c₃.d) (toExpr c.k) (toExpr coeff) (toExpr c'.p) (← c.toExprProof) reflBoolTrue
+        (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c₃.p) (toExpr c₃.d) (toExpr s.k) (toExpr coeff) (toExpr c'.p) (← s.toExprProof) reflBoolTrue
 
 partial def DiseqCnstr.toExprProof (c' : DiseqCnstr) : ProofM Expr := c'.caching do
   match c'.h with
@@ -158,24 +160,25 @@ partial def CooperSplit.toExprProof (s : CooperSplit) : ProofM Expr := caching s
   match s.h with
   | .dec h => return mkFVar h
   | .last hs _ =>
-    let p₁ := s.c₁.p
-    let p₂ := s.c₂.p
-    let n := s.numCases
+    let { c₁, c₂, c₃?, left } := s.pred
+    let p₁ := c₁.p
+    let p₂ := c₂.p
+    let n := s.pred.numCases
     unless hs.size + 1 == n do
       throwError "`grind` internal error, unexpected number of cases at `CopperSplit`"
-    let (base, pred) ← match s.c₃? with
+    let (base, pred) ← match c₃? with
       | none =>
-        let thmName := if s.left then ``Int.Linear.cooper_left else ``Int.Linear.cooper_right
-        let predName := if s.left then ``Int.Linear.cooper_left_split else ``Int.Linear.cooper_right_split
+        let thmName := if left then ``Int.Linear.cooper_left else ``Int.Linear.cooper_right
+        let predName := if left then ``Int.Linear.cooper_left_split else ``Int.Linear.cooper_right_split
         let base := mkApp7 (mkConst thmName) (← getContext) (toExpr p₁) (toExpr p₂) (toExpr n)
-          reflBoolTrue (← s.c₁.toExprProof) (← s.c₂.toExprProof)
+          reflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
         let pred := mkApp3 (mkConst predName) (← getContext) (toExpr p₁) (toExpr p₂)
         pure (base, pred)
       | some c₃ =>
-        let thmName := if s.left then ``Int.Linear.cooper_dvd_left else ``Int.Linear.cooper_dvd_right
-        let predName := if s.left then ``Int.Linear.cooper_dvd_left_split else ``Int.Linear.cooper_dvd_right_split
+        let thmName := if left then ``Int.Linear.cooper_dvd_left else ``Int.Linear.cooper_dvd_right
+        let predName := if left then ``Int.Linear.cooper_dvd_left_split else ``Int.Linear.cooper_dvd_right_split
         let base := mkApp10 (mkConst thmName) (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c₃.p) (toExpr c₃.d) (toExpr n)
-          reflBoolTrue (← s.c₁.toExprProof) (← s.c₂.toExprProof) (← c₃.toExprProof)
+          reflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof) (← c₃.toExprProof)
         let pred := mkApp5 (mkConst predName) (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c₃.p) (toExpr c₃.d)
         pure (base, pred)
     -- `pred` is an expressions of the form `cooper_*_split ...` with type `Nat → Prop`
@@ -256,8 +259,8 @@ partial def EqCnstr.collectDecVars (c' : EqCnstr) : CollectDecVarsM Unit := do u
   | .norm c | .divCoeffs c => c.collectDecVars
   | .subst _ c₁ c₂ | .ofLeGe c₁ c₂ => c₁.collectDecVars; c₂.collectDecVars
 
-partial def CooperSplit.collectDecVars (c' : CooperSplit) : CollectDecVarsM Unit := do unless (← alreadyVisited c'.id) do
-  match c'.h with
+partial def CooperSplit.collectDecVars (s : CooperSplit) : CollectDecVarsM Unit := do unless (← alreadyVisited s.id) do
+  match s.h with
   | .dec h => markAsFound h
   | .last (decVars := decVars) .. => decVars.forM markAsFound
 

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean

@@ -14,6 +14,39 @@ import Lean.Meta.Tactic.Grind.Arith.Cutsat.Model
 
 namespace Lean.Meta.Grind.Arith.Cutsat
 
+/-- Asserts constraints implied by a `CooperSplit`. -/
+def CooperSplit.assert (cs : CooperSplit) : GoalM Unit := do
+  let { c₁, c₂, c₃?, left, .. } := cs.pred
+  let k   := cs.k
+  let p₁  := c₁.p
+  let p₂  := c₂.p
+  let p   := p₁.tail
+  let q   := p₂.tail
+  let a   := p₁.leadCoeff
+  let b   := p₂.leadCoeff
+  let p₁' := p.mul b |>.combine (q.mul (-a))
+  let p₁' := p₁'.addConst <| if left then b*k else (-a)*k
+  let c₁' ← mkLeCnstr p₁' (.cooper cs)
+  c₁'.assert
+  let p₂' := if left then p else q
+  let p₂' := p₂'.addConst k
+  let c₂' ← mkDvdCnstr (if left then a else b) p₂' (.cooper₁ cs)
+  c₂'.assert
+  let some c₃ := c₃? | return ()
+  let p₃  := c₃.p
+  let d   := c₃.d
+  let s   := p₃.tail
+  let c   := p₃.leadCoeff
+  let c₃' ← if left then
+    let p₃' := p.mul c |>.combine (s.mul (-a))
+    let p₃' := p₃'.addConst (c*k)
+    mkDvdCnstr (a*d) p₃' (.cooper₂ cs)
+  else
+    let p₃' := q.mul (-c) |>.combine (s.mul b)
+    let p₃' := p₃'.addConst (-c*k)
+    mkDvdCnstr (b*d) p₃' (.cooper₂ cs)
+  c₃'.assert
+
 private def checkIsNextVar (x : Var) : GoalM Unit := do
   if x != (← get').assignment.size then
     throwError "`grind` internal error, assigning variable out of order"
@@ -239,29 +272,19 @@ def resolveRealLowerUpperConflict (c₁ c₂ : LeCnstr) : GoalM Bool := do
     c.assert
     return true
 
-def resolveCooperLeft (c₁ c₂ : LeCnstr) : GoalM Unit := do
-  throwError "Cooper-left NIY {← c₁.pp}, {← c₂.pp}"
+def resolveCooperPred (pred : CooperSplitPred) : SearchM Unit := do
+  let n := pred.numCases
+  let fvarId ← mkCase (.cooper pred #[])
+  let s : CooperSplit := { pred, k := n - 1, id := (← mkCnstrId), h := .dec fvarId }
+  s.assert
 
-def resolveCooperRight (c₁ c₂ : LeCnstr) : GoalM Unit := do
-  throwError "Cooper-right NIY {← c₁.pp}, {← c₂.pp}"
+def resolveCooper (c₁ c₂ : LeCnstr) : SearchM Unit := do
+  let left : Bool := c₁.p.leadCoeff.natAbs < c₂.p.leadCoeff.natAbs
+  resolveCooperPred { c₁, c₂, left, c₃? := none }
 
-def resolveCooper (c₁ c₂ : LeCnstr) : GoalM Unit := do
-  if c₁.p.leadCoeff.natAbs < c₂.p.leadCoeff.natAbs then
-    resolveCooperLeft c₁ c₂
-  else
-    resolveCooperRight c₁ c₂
-
-def resolveCooperDvdLeft (c₁ c₂ : LeCnstr) (c : DvdCnstr) : GoalM Unit := do
-  throwError "Cooper-dvd-left NIY {← c₁.pp}, {← c₂.pp}, {← c.pp}"
-
-def resolveCooperDvdRight (c₁ c₂ : LeCnstr) (c : DvdCnstr) : GoalM Unit := do
-  throwError "Cooper-dvd-right NIY {← c₁.pp}, {← c₂.pp}, {← c.pp}"
-
-def resolveCooperDvd (c₁ c₂ : LeCnstr) (c : DvdCnstr) : GoalM Unit := do
-  if c₁.p.leadCoeff.natAbs < c₂.p.leadCoeff.natAbs then
-    resolveCooperDvdLeft c₁ c₂ c
-  else
-    resolveCooperDvdRight c₁ c₂ c
+def resolveCooperDvd (c₁ c₂ : LeCnstr) (c₃ : DvdCnstr) : SearchM Unit := do
+  let left : Bool := c₁.p.leadCoeff.natAbs < c₂.p.leadCoeff.natAbs
+  resolveCooperPred { c₁, c₂, left, c₃? := some c₃ }
 
 def resolveCooperDiseq (c₁ : DiseqCnstr) (c₂ : LeCnstr) (_c? : Option DvdCnstr) : GoalM Unit := do
   throwError "Cooper-diseq NIY {← c₁.pp}, {← c₂.pp}"

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/SearchM.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
--- import Lean.Meta.Tactic.Grind.Arith.Cutsat.Cooper
 
 namespace Lean.Meta.Grind.Arith.Cutsat
 /--
@@ -15,10 +14,7 @@ In principle, we only need to support two kinds of case split.
 -/
 inductive CaseKind where
   | diseq (d : DiseqCnstr)
-  | copperLeft
-  | copperDvdLeft
-  | cooperRight
-  | cooperDvdRight
+  | cooper (s : CooperSplitPred) (hs : Array (FVarId × UnsatProof))
   deriving Inhabited
 
 structure Case where

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean

@@ -103,16 +103,22 @@ The specific predicate used is determined as follows:
 - `cooper_dvd_left_split` (if `left` is `true` and `c₃?` is `some`)
 - `cooper_dvd_right_split` (if `left` is `false` and `c₃?` is `some`)
 
-See `CooperSplitProof` for additional explanations.
+See `CooperSplit`
 -/
-structure CooperSplit where
+structure CooperSplitPred where
   left     : Bool
   c₁       : LeCnstr
   c₂       : LeCnstr
   c₃?      : Option DvdCnstr
-  k        : Nat
-  h        : CooperSplitProof
-  id       : Nat
+
+/--
+An instance of the `CooperSplitPred` at `k`.
+-/
+structure CooperSplit where
+  pred  : CooperSplitPred
+  k     : Nat
+  h     : CooperSplitProof
+  id    : Nat
 
 /--
 The `cooper_left`, `cooper_right`, `cooper_dvd_left`, and `cooper_dvd_right` theorems have a resulting type
@@ -191,6 +197,12 @@ instance : Inhabited LeCnstr where
 instance : Inhabited DvdCnstr where
   default := { d := 0, p := .num 0, h := .expr default, id := 0 }
 
+instance : Inhabited CooperSplitPred where
+  default := { left := false, c₁ := default, c₂ := default, c₃? := none }
+
+instance : Inhabited CooperSplit where
+  default := { pred := default, k := 0, h := .dec default, id := 0 }
+
 abbrev VarSet := RBTree Var compare
 
 /-- State of the cutsat procedure. -/

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean

@@ -278,4 +278,17 @@ def _root_.Int.Linear.Poly.findVarToSubst (p : Poly) : GoalM (Option (Int × Var
     else
       findVarToSubst p
 
+def CooperSplitPred.numCases (pred : CooperSplitPred) : Nat :=
+  let a  := pred.c₁.p.leadCoeff
+  let b  := pred.c₂.p.leadCoeff
+  match pred.c₃? with
+  | none => if pred.left then a.natAbs else b.natAbs
+  | some c₃ =>
+    let c  := c₃.p.leadCoeff
+    let d  := c₃.d
+    if pred.left then
+      Int.lcm a (a * d / Int.gcd (a * d) c)
+    else
+      Int.lcm b (b * d / Int.gcd (b * d) c)
+
 end Lean.Meta.Grind.Arith.Cutsat

stage0/src/stdlib_flags.h

@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// please update stage0
+
 namespace lean {
 options get_default_options() {
     options opts;

tests/lean/run/simp_int_arith.lean

@@ -310,18 +310,14 @@ info: theorem ex4 : ∀ (a b : Int), 6 ∣ a + (11 - a) + 3 * (a + 2 * b) - 11
 fun a b =>
   of_eq_true
     (Eq.trans
-      (congr
-        (congrArg Iff
-          (Eq.trans
-            (id
-              (norm_dvd_gcd (RArray.branch 1 (RArray.leaf b) (RArray.leaf a)) 6
-                ((((Expr.var 1).add ((Expr.num 11).sub (Expr.var 1))).add
-                      (Expr.mulL 3 ((Expr.var 1).add (Expr.mulL 2 (Expr.var 0))))).sub
-                  (Expr.num 11))
-                2 (Poly.add 1 1 (Poly.add 2 0 (Poly.num 0))) 3 (Eq.refl true)))
-            Init.Data.Int.DivMod.Lemmas._auxLemma.2))
-        Init.Data.Int.DivMod.Lemmas._auxLemma.2)
-      (iff_self (2 ∣ a)))
+      (congrArg (fun x => x ↔ 2 ∣ a + 2 * b)
+        (id
+          (norm_dvd_gcd (RArray.branch 1 (RArray.leaf b) (RArray.leaf a)) 6
+            ((((Expr.var 1).add ((Expr.num 11).sub (Expr.var 1))).add
+                  (Expr.mulL 3 ((Expr.var 1).add (Expr.mulL 2 (Expr.var 0))))).sub
+              (Expr.num 11))
+            2 (Poly.add 1 1 (Poly.add 2 0 (Poly.num 0))) 3 (Eq.refl true))))
+      (iff_self (2 ∣ a + 2 * b)))
 -/
 #guard_msgs (info) in
 open Lean in open Int.Linear in