chore(Data/Int/GCD): review API (#31140)

This PR makes a few changes, but they are very linked so a single PR seems easiest:

- Rename `Nat.exists_mul_emod_eq_gcd` to `Nat.exists_mul_mod_eq_gcd`, and `Nat.exists_mul_emod_eq_one_of_coprime` to `Nat.exists_mul_mod_eq_one_of_coprime`. This is since the `%` operator on naturals is only ever named `mod`, whereas `emod` is reserved for the `%` operator on integers.
- Strengthen the statements of those two to additionally deduce that `m < k`.
- Add `exists_mul_mod_eq_of_coprime`, which is the non-one generalisation of `exists_mul_mod_eq_one_of_coprime`.

Author: b-mehta

Archive/Imo/Imo1985Q2.lean

@@ -75,7 +75,7 @@ lemma C_mul_mod {n j : ℕ} (hn : 3 ≤ n) (hj : j ∈ Set.Ico 1 n) (cpj : Nat.C
 theorem result {n j : ℕ} (hn : 3 ≤ n) (hj : j ∈ Set.Ico 1 n) (cpj : Coprime n j)
     {C : ℕ → Fin 2} (hC : Condition n j C) {i : ℕ} (hi : i ∈ Set.Ico 1 n) :
     C i = C j := by
-  obtain ⟨v, hv⟩ := exists_mul_emod_eq_one_of_coprime cpj.symm (by omega)
+  obtain ⟨v, -, hv⟩ := exists_mul_mod_eq_one_of_coprime cpj.symm (by omega)
   have hvi : i = (v * i % n) * j % n := by
     rw [mod_mul_mod, ← mul_rotate, ← mod_mul_mod, hv, one_mul, mod_eq_of_lt hi.2]
   have vib : v * i % n ∈ Set.Ico 1 n := by

Mathlib/Data/Int/GCD.lean

@@ -133,20 +133,32 @@ theorem gcd_eq_gcd_ab : (gcd x y : ℤ) = x * gcdA x y + y * gcdB x y := by
 
 end
 
-theorem exists_mul_emod_eq_gcd {k n : ℕ} (hk : gcd n k < k) : ∃ m, n * m % k = gcd n k := by
-  have hk' := Int.ofNat_ne_zero.2 (ne_of_gt (lt_of_le_of_lt (zero_le (gcd n k)) hk))
-  have key := congr_arg (fun (m : ℤ) => (m % k).toNat) (gcd_eq_gcd_ab n k)
-  simp only at key
+theorem exists_mul_mod_eq_gcd {k n : ℕ} (hk : gcd n k < k) : ∃ m < k, n * m % k = gcd n k := by
+  have hk' := Int.ofNat_ne_zero.2 (Nat.zero_lt_of_lt hk).ne'
+  have key := congr(($(gcd_eq_gcd_ab n k) % k).toNat)
   rw [Int.add_mul_emod_self_left, ← Int.natCast_mod, Int.toNat_natCast, mod_eq_of_lt hk] at key
-  refine ⟨(n.gcdA k % k).toNat, Eq.trans (Int.ofNat.inj ?_) key.symm⟩
-  rw [Int.ofNat_eq_natCast, Int.natCast_mod, Int.natCast_mul,
-    Int.toNat_of_nonneg (Int.emod_nonneg _ hk'), Int.ofNat_eq_natCast,
+  refine ⟨(n.gcdA k % k).toNat, ?_, (Int.ofNat_inj.1 ?_).trans key.symm⟩
+  · rw [Int.toNat_lt (Int.emod_nonneg _ hk')]
+    exact Int.emod_lt _ hk'
+  rw [Int.natCast_mod, Int.natCast_mul, Int.toNat_of_nonneg (Int.emod_nonneg _ hk'),
     Int.toNat_of_nonneg (Int.emod_nonneg _ hk'), Int.mul_emod, Int.emod_emod, ← Int.mul_emod]
 
-theorem exists_mul_emod_eq_one_of_coprime {k n : ℕ} (hkn : Coprime n k) (hk : 1 < k) :
-    ∃ m, n * m % k = 1 :=
-  Exists.recOn (exists_mul_emod_eq_gcd (lt_of_le_of_lt (le_of_eq hkn) hk)) fun m hm ↦
-    ⟨m, hm.trans hkn⟩
+@[deprecated (since := "2025-11-01")] alias exists_mul_emod_eq_gcd := exists_mul_mod_eq_gcd
+
+theorem exists_mul_mod_eq_one_of_coprime {k n : ℕ} (hkn : Coprime n k) (hk : 1 < k) :
+    ∃ m < k, n * m % k = 1 := by
+  simpa [hkn, hk] using exists_mul_mod_eq_gcd (k := k) (n := n)
+
+@[deprecated (since := "2025-11-01")] alias exists_mul_emod_eq_one_of_coprime :=
+  exists_mul_mod_eq_one_of_coprime
+
+theorem exists_mul_mod_eq_of_coprime {k n : ℕ} (r : ℕ) (hkn : Coprime n k) (hk : k ≠ 0) :
+    ∃ m < k, n * m % k = r % k := by
+  obtain rfl | hk : k = 1 ∨ 1 < k := by omega
+  next => simp [mod_one]
+  obtain ⟨m, -, hm⟩ := exists_mul_mod_eq_one_of_coprime hkn hk
+  use (m * r) % k, mod_lt _ (by omega)
+  rw [mul_mod, mod_mod, ← mul_mod, ← mul_assoc, mul_mod, hm, one_mul, mod_mod]
 
 end Nat
 

Mathlib/GroupTheory/OrderOfElement.lean

@@ -302,7 +302,7 @@ theorem exists_pow_eq_self_of_coprime (h : n.Coprime (orderOf x)) : ∃ m : ℕ,
     exact ⟨1, by rw [h, pow_one, pow_one]⟩
   by_cases h1 : orderOf x = 1
   · exact ⟨0, by rw [orderOf_eq_one_iff.mp h1, one_pow, one_pow]⟩
-  obtain ⟨m, h⟩ := exists_mul_emod_eq_one_of_coprime h (one_lt_iff_ne_zero_and_ne_one.mpr ⟨h0, h1⟩)
+  obtain ⟨m, -, h⟩ := exists_mul_mod_eq_one_of_coprime h (by omega)
   exact ⟨m, by rw [← pow_mul, ← pow_mod_orderOf, h, pow_one]⟩
 
 /-- If `x^n = 1`, but `x^(n/p) ≠ 1` for all prime factors `p` of `n`,

Mathlib/RingTheory/RootsOfUnity/CyclotomicUnits.lean

@@ -51,7 +51,7 @@ theorem associated_sub_one_pow_sub_one_of_coprime (hζ : IsPrimitiveRoot ζ n) (
   | 0 => simp_all
   | 1 => simp_all
   | n + 2 =>
-      obtain ⟨m, hm⟩ := exists_mul_emod_eq_one_of_coprime hj (by omega)
+      obtain ⟨m, -, hm⟩ := exists_mul_mod_eq_one_of_coprime hj (by omega)
       use ∑ i ∈ range m, (ζ ^ j) ^ i
       rw [mul_geom_sum, ← pow_mul, ← pow_mod_orderOf, ← hζ.eq_orderOf, hm, pow_one]