From 75d7f7eb227bc54dc6ea3d8ead090ee4180debaf Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Thu, 5 Feb 2026 16:13:00 +1100
Subject: [PATCH] feat: add `Nat.ext_div_mod` and `Int.ext_ediv_emod` (#12258)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR adds theorems that directly state that div and mod form an
injective pair: if `a / n = b / n` and `a % n = b % n` then `a = b`.
These complement existing div/mod lemmas and are useful for extension
arguments.

Upstreaming from
https://github.com/leanprover-community/mathlib4/pull/34201

🤖 Prepared with Claude Code

Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
---
 src/Init/Data/Int/DivMod/Lemmas.lean | 6 ++++++
 src/Init/Data/Nat/Div/Lemmas.lean    | 6 ++++++
 2 files changed, 12 insertions(+)

diff --git a/src/Init/Data/Int/DivMod/Lemmas.lean b/src/Init/Data/Int/DivMod/Lemmas.lean
index 83d3cdca5a..c3bdfebc54 100644
--- a/src/Init/Data/Int/DivMod/Lemmas.lean
+++ b/src/Init/Data/Int/DivMod/Lemmas.lean
@@ -3000,4 +3000,10 @@ protected theorem dvd_eq_false_of_mod_ne_zero {a b : Int} (h : b % a != 0) : (a
   simp [eq_of_beq] at h
   simp [Int.dvd_iff_emod_eq_zero, h]
 
+theorem ext_ediv_emod {n a b : Int} (h0 : a / n = b / n) (h1 : a % n = b % n) : a = b :=
+  (mul_ediv_add_emod a n).symm.trans (h0 ▸ h1 ▸ mul_ediv_add_emod b n)
+
+theorem ext_ediv_emod_iff (n a b : Int) : a = b ↔ a / n = b / n ∧ a % n = b % n :=
+  ⟨fun h => ⟨h ▸ rfl, h ▸ rfl⟩, fun ⟨h0, h1⟩ => ext_ediv_emod h0 h1⟩
+
 end Int
diff --git a/src/Init/Data/Nat/Div/Lemmas.lean b/src/Init/Data/Nat/Div/Lemmas.lean
index 1f9473d8cd..95b7553b9d 100644
--- a/src/Init/Data/Nat/Div/Lemmas.lean
+++ b/src/Init/Data/Nat/Div/Lemmas.lean
@@ -241,4 +241,10 @@ theorem mod_eq_mod_iff {x y z : Nat} :
     replace h := congrArg (· % z) h
     simpa using h
 
+theorem ext_div_mod {n a b : Nat} (h0 : a / n = b / n) (h1 : a % n = b % n) : a = b :=
+  (div_add_mod a n).symm.trans (h0 ▸ h1 ▸ div_add_mod b n)
+
+theorem ext_div_mod_iff (n a b : Nat) : a = b ↔ a / n = b / n ∧ a % n = b % n :=
+  ⟨fun h => ⟨h ▸ rfl, h ▸ rfl⟩, fun ⟨h0, h1⟩ => ext_div_mod h0 h1⟩
+
 end Nat