From 6931e91bf05aaaa200ca40e05ec612eb817f4bfa Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 21 Mar 2025 15:23:03 +0100
Subject: [PATCH] fix: mark Nat.div and Nat.modCore irreducible (#7614)

This PR marks `Nat.div` and `Nat.modCore` as `irreducible`, to recover
the behavior from from before #7558.

Fixes #7612. H't to @tobiasgrosser for the good bug report.
---
 src/Init/Data/Nat/Div/Basic.lean | 4 ++--
 tests/lean/run/7612.lean         | 5 +++++
 2 files changed, 7 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/7612.lean

diff --git a/src/Init/Data/Nat/Div/Basic.lean b/src/Init/Data/Nat/Div/Basic.lean
index 2e24e47375..311039aac1 100644
--- a/src/Init/Data/Nat/Div/Basic.lean
+++ b/src/Init/Data/Nat/Div/Basic.lean
@@ -39,7 +39,7 @@ Examples:
  * `0 / 22 = 0`
  * `5 / 0 = 0`
 -/
-@[extern "lean_nat_div"]
+@[extern "lean_nat_div", irreducible]
 protected def div (x y : @& Nat) : Nat :=
   if hy : 0 < y then
     let rec
@@ -140,7 +140,7 @@ reductions](lean-manual://section/type-system) when the `Nat`s contain free vari
 This function is overridden at runtime with an efficient implementation. This definition is the
 logical model.
 -/
-@[extern "lean_nat_mod"]
+@[extern "lean_nat_mod", irreducible]
 protected noncomputable def modCore (x y : Nat) : Nat :=
   if hy : 0 < y then
     let rec
diff --git a/tests/lean/run/7612.lean b/tests/lean/run/7612.lean
new file mode 100644
index 0000000000..4cf4966315
--- /dev/null
+++ b/tests/lean/run/7612.lean
@@ -0,0 +1,5 @@
+
+theorem extracted_1 (x y : BitVec 9) :
+    (y - y.srem x).sdiv x = y.sdiv x := by
+  ac_nf
+  sorry