chore: rename Nat.div_eq to Nat.div_eq_ite (#14462)

This PR renames `Nat.div_eq` to `Nat.div_eq_ite` and `Nat.mod_eq` to
`Nat.mod_eq_ite`.

This will free up `Nat.div_eq` for a lemma analogous to `Nat.add_eq`.

Author: TwoFX

src/Init/Data/Fin/Lemmas.lean

@@ -1122,7 +1122,7 @@ theorem sub_ofNat [NeZero n] (x : Fin n) (y : Nat) :
 
 private theorem _root_.Nat.mod_eq_sub_of_lt_two_mul {x n} (h₁ : n ≤ x) (h₂ : x < 2 * n) :
     x % n = x - n := by
-  rw [Nat.mod_eq, if_pos (by omega), Nat.mod_eq_of_lt (by omega)]
+  rw [Nat.mod_eq_ite, if_pos (by omega), Nat.mod_eq_of_lt (by omega)]
 
 theorem coe_sub_iff_le {a b : Fin n} : (↑(a - b) : Nat) = a - b ↔ b ≤ a := by
   rw [sub_def, le_def]

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -261,7 +261,7 @@ private theorem succ_mod_two : succ x % 2 = 1 - x % 2 := by
     trivial
   | succ x hyp =>
     have p : 2 ≤ x + 2 := Nat.le_add_left _ _
-    simp [Nat.mod_eq (x+2) 2, p, hyp]
+    simp [Nat.mod_eq_ite (x+2) 2, p, hyp]
     cases Nat.mod_two_eq_zero_or_one x with | _ p => simp [p]
 
 private theorem testBit_succ_zero : testBit (x + 1) 0 = !(testBit x 0) := by
@@ -302,7 +302,7 @@ theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) :
     testBit (x % 2^j) i = (decide (i < j) && testBit x i) := by
   induction x using Nat.strongRecOn generalizing j i with
   | ind x hyp =>
-    rw [mod_eq]
+    rw [mod_eq_ite]
     rcases Nat.lt_or_ge x (2^j) with x_lt_j | x_ge_j
     · have not_j_le_x := Nat.not_le_of_gt x_lt_j
       simp [not_j_le_x]

src/Init/Data/Nat/Div/Basic.lean

@@ -36,7 +36,7 @@ private theorem div.go.fuel_congr (x y fuel1 fuel2 : Nat) (hy : 0 < y) (h1 : x <
     next => rfl
 termination_by structural fuel1
 
-theorem div_eq (x y : Nat) : x / y = if 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0 := by
+theorem div_eq_ite (x y : Nat) : x / y = if 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0 := by
   change Nat.div _ _ = ite _ (Nat.div _ _ + 1) _
   unfold Nat.div
   split
@@ -52,6 +52,10 @@ theorem div_eq (x y : Nat) : x / y = if 0 < y ∧ y ≤ x then (x - y) / y + 1 e
   next =>
     simp only [false_and, ↓reduceIte, *]
 
+@[deprecated div_eq_ite (since := "2026-07-20")]
+theorem div_eq (x y : Nat) : x / y = if 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0 :=
+  Nat.div_eq_ite x y
+
 /--
 An induction principle customized for reasoning about the recursion pattern of natural number
 division by iterated subtraction.
@@ -71,7 +75,7 @@ decreasing_by apply div_rec_lemma; assumption
 theorem div_le_self (n k : Nat) : n / k ≤ n := by
   induction n using Nat.strongRecOn with
   | ind n ih =>
-    rw [div_eq]
+    rw [div_eq_ite]
     -- Note: manual split to avoid Classical.em which is not yet defined
     cases (inferInstance : Decidable (0 < k ∧ k ≤ n)) with
     | isFalse h => simp [h]
@@ -83,7 +87,7 @@ theorem div_le_self (n k : Nat) : n / k ≤ n := by
       exact succ_le_of_lt (Nat.lt_of_le_of_lt this hSub)
 
 theorem div_lt_self {n k : Nat} (hLtN : 0 < n) (hLtK : 1 < k) : n / k < n := by
-  rw [div_eq]
+  rw [div_eq_ite]
   cases (inferInstance : Decidable (0 < k ∧ k ≤ n)) with
   | isFalse h => simp [hLtN, h]
   | isTrue h =>
@@ -155,9 +159,13 @@ protected theorem modCore_eq_mod (n m : Nat) : Nat.modCore n m = n % m := by
     rw [Nat.modCore_eq]
     exact if_neg fun ⟨_hlt, hle⟩ => h hle
 
-theorem mod_eq (x y : Nat) : x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x := by
+theorem mod_eq_ite (x y : Nat) : x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x := by
   rw [←Nat.modCore_eq_mod, ←Nat.modCore_eq_mod, Nat.modCore_eq]
 
+@[deprecated mod_eq_ite (since := "2026-07-20")]
+theorem mod_eq (x y : Nat) : x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x :=
+  Nat.mod_eq_ite x y
+
 /--
 An induction principle customized for reasoning about the recursion pattern of `Nat.mod`.
 -/
@@ -173,13 +181,13 @@ def mod.inductionOn.{u}
   have : (if 0 < 0 ∧ 0 ≤ a then (a - 0) % 0 else a) = a :=
     have h : ¬ (0 < 0 ∧ 0 ≤ a) := fun ⟨h₁, _⟩ => absurd h₁ (Nat.lt_irrefl _)
     if_neg h
-  (mod_eq a 0).symm ▸ this
+  (mod_eq_ite a 0).symm ▸ this
 
 theorem mod_eq_of_lt {a b : Nat} (h : a < b) : a % b = a :=
   have : (if 0 < b ∧ b ≤ a then (a - b) % b else a) = a :=
     have h' : ¬(0 < b ∧ b ≤ a) := fun ⟨_, h₁⟩ => absurd h₁ (Nat.not_le_of_gt h)
     if_neg h'
-  (mod_eq a b).symm ▸ this
+  (mod_eq_ite a b).symm ▸ this
 
 @[simp] theorem one_mod_eq_zero_iff {n : Nat} : 1 % n = 0 ↔ n = 1 := by
   match n with
@@ -197,7 +205,7 @@ theorem mod_eq_of_lt {a b : Nat} (h : a < b) : a % b = a :=
 theorem mod_eq_sub_mod {a b : Nat} (h : a ≥ b) : a % b = (a - b) % b :=
   match eq_zero_or_pos b with
   | Or.inl h₁ => h₁.symm ▸ (Nat.sub_zero a).symm ▸ rfl
-  | Or.inr h₁ => (mod_eq a b).symm ▸ if_pos ⟨h₁, h⟩
+  | Or.inr h₁ => (mod_eq_ite a b).symm ▸ if_pos ⟨h₁, h⟩
 
 @[simp] protected theorem sub_mod_add_mod_cancel (a b : Nat) [NeZero a] : a - b % a + b % a = a := by
   rw [Nat.sub_add_cancel]
@@ -231,7 +239,7 @@ theorem mod_one (x : Nat) : x % 1 = 0 := by
   exact this _ h
 
 theorem div_add_mod (m n : Nat) : n * (m / n) + m % n = m := by
-  rw [div_eq, mod_eq]
+  rw [div_eq_ite, mod_eq_ite]
   have h : Decidable (0 < n ∧ n ≤ m) := inferInstance
   cases h with
   | isFalse h => simp [h]
@@ -242,10 +250,10 @@ theorem div_add_mod (m n : Nat) : n * (m / n) + m % n = m := by
 decreasing_by apply div_rec_lemma; assumption
 
 theorem div_eq_sub_div (h₁ : 0 < b) (h₂ : b ≤ a) : a / b = (a - b) / b + 1 := by
- rw [div_eq a, if_pos]; constructor <;> assumption
+ rw [div_eq_ite a, if_pos]; constructor <;> assumption
 
 theorem mod_add_div (m k : Nat) : m % k + k * (m / k) = m := by
-  induction m, k using mod.inductionOn with rw [div_eq, mod_eq]
+  induction m, k using mod.inductionOn with rw [div_eq_ite, mod_eq_ite]
   | base x y h => simp [h]
   | ind x y h IH => simp [h]; rw [Nat.mul_succ, ← Nat.add_assoc, IH, Nat.sub_add_cancel h.2]
 
@@ -263,14 +271,14 @@ theorem mod_eq_sub_div_mul {x k : Nat} : x % k = x - (x / k) * k := by
   rwa [mod_one, Nat.zero_add, Nat.one_mul] at this
 
 @[simp] protected theorem div_zero (n : Nat) : n / 0 = 0 := by
-  rw [div_eq]; simp [Nat.lt_irrefl]
+  rw [div_eq_ite]; simp [Nat.lt_irrefl]
 
 @[simp] protected theorem zero_div (b : Nat) : 0 / b = 0 :=
-  (div_eq 0 b).trans <| if_neg <| And.rec Nat.not_le_of_gt
+  (div_eq_ite 0 b).trans <| if_neg <| And.rec Nat.not_le_of_gt
 
 theorem le_div_iff_mul_le (k0 : 0 < k) : x ≤ y / k ↔ x * k ≤ y := by
   induction y, k using mod.inductionOn generalizing x with
-    (rw [div_eq]; simp [h]; cases x with | zero => simp [zero_le] | succ x => ?_)
+    (rw [div_eq_ite]; simp [h]; cases x with | zero => simp [zero_le] | succ x => ?_)
   | base y k h =>
     simp only [add_one, succ_mul, false_iff, Nat.not_le, Nat.succ_ne_zero]
     refine Nat.lt_of_lt_of_le ?_ (Nat.le_add_left ..)
@@ -412,7 +420,7 @@ theorem mul_mod_mul_left (z x y : Nat) : (z * x) % (z * y) = z * (x % y) :=
         exact IH _ (sub_lt (Nat.lt_of_lt_of_le y0 yn) y0)
 
 theorem div_eq_of_lt (h₀ : a < b) : a / b = 0 := by
-  rw [div_eq a, if_neg]
+  rw [div_eq_ite a, if_neg]
   intro h₁
   apply Nat.not_le_of_gt h₀ h₁.right
 

src/Init/Data/Nat/Div/Lemmas.lean

@@ -123,7 +123,7 @@ theorem succ_div_of_dvd {a b : Nat} (h : b ∣ a + 1) :
   | zero => simp at h
   | succ b =>
     by_cases h' : b ≤ a
-    · rw [Nat.div_eq]
+    · rw [Nat.div_eq_ite]
       simp only [zero_lt_succ, Nat.add_le_add_iff_right, h', and_self, ↓reduceIte,
         Nat.reduceSubDiff, Nat.add_right_cancel_iff]
       obtain ⟨_|k, h⟩ := Nat.dvd_of_mod_eq_zero h

src/Init/Data/Nat/Lemmas.lean

@@ -1564,7 +1564,7 @@ theorem mul_add_div {m : Nat} (m_pos : m > 0) (x y : Nat) : (m * x + y) / m = x
   match x with
   | 0 => simp
   | x + 1 =>
-    rw [Nat.mul_succ, Nat.add_assoc _ m, mul_add_div m_pos x (m+y), div_eq]
+    rw [Nat.mul_succ, Nat.add_assoc _ m, mul_add_div m_pos x (m+y), div_eq_ite]
     simp +arith [m_pos]
 
 theorem mul_add_mod (m x y : Nat) : (m * x + y) % m = y % m := by

src/Init/Data/Nat/Log2.lean

@@ -19,7 +19,7 @@ theorem log2_terminates : ∀ n, n ≥ 2 → n / 2 < n
   | 2, _ => by decide
   | 3, _ => by decide
   | n+4, _ => by
-    rw [div_eq, if_pos]
+    rw [div_eq_ite, if_pos]
     refine succ_lt_succ (Nat.lt_trans ?_ (lt_succ_self _))
     exact log2_terminates (n+2) (by simp)
     simp

tests/elab/860.lean

@@ -4,7 +4,7 @@ private theorem pack_loop_terminates : (n : Nat) → n / 2 < n.succ
   | 0   => by decide
   | 1   => by decide
   | n+2 => by
-    rw [Nat.div_eq]
+    rw [Nat.div_eq_ite]
     split
     · rw [Nat.add_sub_self_right]
       have := pack_loop_terminates n

tests/elab/binrec.lean

@@ -27,7 +27,7 @@ theorem Nat.div2_lt (h : n ≠ 0) : n / 2 < n := by
   | 2   => decide
   | 3   => decide
   | n+4 =>
-    rw [div_eq, if_pos]
+    rw [div_eq_ite, if_pos]
     refine succ_lt_succ (Nat.lt_trans ?_ (lt_succ_self _))
     exact @div2_lt (n+2) (by simp +arith)
     simp +arith