From 44938480c306f82a352332e9c32ec446ed7e0811 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Fri, 21 Aug 2026 19:05:22 +0200
Subject: [PATCH 1/7] Revert PR content for better git history

---
 Mathlib/Tactic/NormNum/DivMod.lean  | 60 ++++++++++++------------
 Mathlib/Tactic/NormNum/Ineq.lean    | 50 ++++++++++----------
 Mathlib/Tactic/NormNum/Prime.lean   | 71 ++++++++++++++---------------
 Mathlib/Tactic/ReduceModChar.lean   |  3 +-
 Mathlib/Tactic/Ring/Compare.lean    |  1 +
 Mathlib/Tactic/Simproc/Factors.lean |  5 +-
 6 files changed, 94 insertions(+), 96 deletions(-)

diff --git a/Mathlib/Tactic/NormNum/DivMod.lean b/Mathlib/Tactic/NormNum/DivMod.lean
index bd2589307b2d29..8548e62573090a 100644
--- a/Mathlib/Tactic/NormNum/DivMod.lean
+++ b/Mathlib/Tactic/NormNum/DivMod.lean
@@ -100,23 +100,37 @@ lemma isInt_emod {a b q m a' : ℤ} {b' r : ℕ}
 lemma isInt_emod_neg {a b : ℤ} {r : ℕ} (h : IsNat (a % -b) r) : IsNat (a % b) r :=
   ⟨by rw [← Int.emod_neg, h.out]⟩
 
-/-- Given a result for evaluating `a b` in `ℤ`, evaluate `a % b`. -/
-def evalIntMod.go (a na : Q(ℤ)) (za : ℤ) (pa : Q(IsInt $a $na))
-    (b : Q(ℤ)) : Result (u := .zero) b → Option (Result q($a % $b))
-  | .isNat _ nb pb => do
-    assumeInstancesCommute
-    if nb.natLit! == 0 then
-      have _ : $nb =Q nat_lit 0 := ⟨⟩
-      return .isInt q(Int.instRing) na za q(isInt_emod_zero $pa $pb)
-    else
-      let ⟨r, p⟩ := core a na za pa b nb pb
-      return .isNat q(instAddMonoidWithOne) r p
-  | .isNegNat _ nb pb => do
-    assumeInstancesCommute
-    let ⟨r, p⟩ := core a na za pa q(-$b) nb q(isNat_neg_of_isNegNat $pb)
-    return .isNat q(instAddMonoidWithOne) r q(isInt_emod_neg $p)
-  | _ => none
+attribute [local instance] monadLiftOptionMetaM in
+/-- The `norm_num` extension which identifies expressions of the form `Int.emod a b`,
+such that `norm_num` successfully recognises both `a` and `b`. -/
+@[norm_num (_ : ℤ) % _, Int.emod _ _]
+partial def evalIntMod : NormNumExt where eval {u α} e := do
+  let .app (.app f (a : Q(ℤ))) (b : Q(ℤ)) ← whnfR e | failure
+  -- We assert that the default instance for `HMod` is `Int.mod` when the first parameter is `ℤ`.
+  guard <|← withNewMCtxDepth <| isDefEq f q(HMod.hMod (α := ℤ))
+  haveI' : u =QL 0 := ⟨⟩; haveI' : $α =Q ℤ := ⟨⟩
+  haveI' : $e =Q ($a % $b) := ⟨⟩
+  let rℤ : Q(Ring ℤ) := q(Int.instRing)
+  let some ⟨za, na, pa⟩ := (← derive a).toInt rℤ | failure
+  go a na za pa b (← derive (u := .zero) b)
 where
+  /-- Given a result for evaluating `a b` in `ℤ`, evaluate `a % b`. -/
+  go (a na : Q(ℤ)) (za : ℤ) (pa : Q(IsInt $a $na))
+      (b : Q(ℤ)) : Result b → Option (Result q($a % $b))
+    | .isNat inst nb pb => do
+      assumeInstancesCommute
+      if nb.natLit! == 0 then
+        have _ : $nb =Q nat_lit 0 := ⟨⟩
+        return .isInt q(Int.instRing) na za q(isInt_emod_zero $pa $pb)
+      else
+        let ⟨r, p⟩ := core a na za pa b nb pb
+        return .isNat q(instAddMonoidWithOne) r p
+    | .isNegNat _ nb pb => do
+      assumeInstancesCommute
+      let ⟨r, p⟩ := core a na za pa q(-$b) nb q(isNat_neg_of_isNegNat $pb)
+      return .isNat q(instAddMonoidWithOne) r q(isInt_emod_neg $p)
+    | _ => none
+
   /-- Given a result for evaluating `a b` in `ℤ` where `b > 0`, evaluate `a % b`. -/
   core (a na : Q(ℤ)) (za : ℤ) (pa : Q(IsInt $a $na))
       (b : Q(ℤ)) (nb : Q(ℕ)) (pb : Q(IsNat $b $nb)) :
@@ -133,20 +147,6 @@ where
     have pf₃ : Q(Nat.blt $nr $nb = true) := (q(Eq.refl true) :)
     ⟨nr, q(isInt_emod $pa $pb $pf₁ $pf₂ $pf₃)⟩
 
-attribute [local instance] monadLiftOptionMetaM in
-/-- The `norm_num` extension which identifies expressions of the form `Int.emod a b`,
-such that `norm_num` successfully recognises both `a` and `b`. -/
-@[norm_num (_ : ℤ) % _, Int.emod _ _]
-partial def evalIntMod : NormNumExt where eval {u α} e := do
-  let .app (.app f (a : Q(ℤ))) (b : Q(ℤ)) ← whnfR e | failure
-  -- We assert that the default instance for `HMod` is `Int.mod` when the first parameter is `ℤ`.
-  guard <|← withNewMCtxDepth <| isDefEq f q(HMod.hMod (α := ℤ))
-  haveI' : u =QL 0 := ⟨⟩; haveI' : $α =Q ℤ := ⟨⟩
-  haveI' : $e =Q ($a % $b) := ⟨⟩
-  let rℤ : Q(Ring ℤ) := q(Int.instRing)
-  let some ⟨za, na, pa⟩ := (← derive a).toInt rℤ | failure
-  evalIntMod.go a na za pa b (← derive (u := .zero) b)
-
 theorem isInt_dvd_true : {a b : ℤ} → {a' b' c : ℤ} →
     IsInt a a' → IsInt b b' → Int.mul a' c = b' → a ∣ b
   | _, _, _, _, _, ⟨rfl⟩, ⟨rfl⟩, rfl => ⟨_, rfl⟩
diff --git a/Mathlib/Tactic/NormNum/Ineq.lean b/Mathlib/Tactic/NormNum/Ineq.lean
index 51d25f216fbb88..a70b42dde5a358 100644
--- a/Mathlib/Tactic/NormNum/Ineq.lean
+++ b/Mathlib/Tactic/NormNum/Ineq.lean
@@ -179,9 +179,21 @@ theorem isInt_lt_false [Ring α] [PartialOrder α] [IsOrderedRing α] {a b : α}
   not_lt_of_ge (isInt_le_true hb ha h)
 
 attribute [local instance] monadLiftOptionMetaM in
-/-- Identify (as `true` or `false`) expressions of the form `a ≤ b`, where `a` and `b` are numeric
-expressions whose evaluations to `NormNum.Result` have already been computed. -/
-def evalLE.core {u : Level} {α : Q(Type u)} (lα : Q(LE $α)) {a b : Q($α)}
+/-- The `norm_num` extension which identifies expressions of the form `a ≤ b`,
+such that `norm_num` successfully recognises both `a` and `b`. -/
+@[norm_num _ ≤ _] def evalLE : NormNumExt where eval {v β} e := do
+  haveI' : v =QL 0 := ⟨⟩; haveI' : $β =Q Prop := ⟨⟩
+  let .app (.app f a) b ← whnfR e | failure
+  let ⟨u, α, a⟩ ← inferTypeQ' a
+  have b : Q($α) := b
+  let ra ← derive a; let rb ← derive b
+  let lα ← synthInstanceQ q(LE $α)
+  guard <|← withNewMCtxDepth <| isDefEq f q(LE.le (α := $α))
+  core lα ra rb
+where
+  /-- Identify (as `true` or `false`) expressions of the form `a ≤ b`, where `a` and `b` are numeric
+  expressions whose evaluations to `NormNum.Result` have already been computed. -/
+  core {u : Level} {α : Q(Type u)} (lα : Q(LE $α)) {a b : Q($α)}
     (ra : NormNum.Result a) (rb : NormNum.Result b) : MetaM (NormNum.Result q($a ≤ $b)) := do
   let e := q($a ≤ $b)
   let rec intArm : MetaM (Result e) := do
@@ -231,22 +243,22 @@ def evalLE.core {u : Level} {α : Q(Type u)} (lα : Q(LE $α)) {a b : Q($α)}
     else -- Nats can appear in an ordered ring without `CharZero`.
       intArm
 
-/-- The `norm_num` extension which identifies expressions of the form `a ≤ b`,
+attribute [local instance] monadLiftOptionMetaM in
+/-- The `norm_num` extension which identifies expressions of the form `a < b`,
 such that `norm_num` successfully recognises both `a` and `b`. -/
-@[norm_num _ ≤ _] def evalLE : NormNumExt where eval {v β} e := do
+@[norm_num _ < _] def evalLT : NormNumExt where eval {v β} e := do
   haveI' : v =QL 0 := ⟨⟩; haveI' : $β =Q Prop := ⟨⟩
   let .app (.app f a) b ← whnfR e | failure
   let ⟨u, α, a⟩ ← inferTypeQ' a
   have b : Q($α) := b
   let ra ← derive a; let rb ← derive b
-  let lα ← synthInstanceQ q(LE $α)
-  guard <|← withNewMCtxDepth <| isDefEq f q(LE.le (α := $α))
-  evalLE.core lα ra rb
-
-attribute [local instance] monadLiftOptionMetaM in
-/-- Identify (as `true` or `false`) expressions of the form `a < b`, where `a` and `b` are numeric
-expressions whose evaluations to `NormNum.Result` have already been computed. -/
-def evalLT.core {u : Level} {α : Q(Type u)} (lα : Q(LT $α)) {a b : Q($α)}
+  let lα ← synthInstanceQ q(LT $α)
+  guard <|← withNewMCtxDepth <| isDefEq f q(LT.lt (α := $α))
+  core lα ra rb
+where
+  /-- Identify (as `true` or `false`) expressions of the form `a < b`, where `a` and `b` are numeric
+  expressions whose evaluations to `NormNum.Result` have already been computed. -/
+  core {u : Level} {α : Q(Type u)} (lα : Q(LT $α)) {a b : Q($α)}
     (ra : NormNum.Result a) (rb : NormNum.Result b) : MetaM (NormNum.Result q($a < $b)) := do
   let e := q($a < $b)
   let rec intArm : MetaM (Result e) := do
@@ -311,16 +323,4 @@ def evalLT.core {u : Level} {α : Q(Type u)} (lα : Q(LT $α)) {a b : Q($α)}
       let r : Q(Nat.ble $nb $na = true) := (q(Eq.refl true) : Expr)
       return .isFalse q(isNat_lt_false $pa $pb $r)
 
-/-- The `norm_num` extension which identifies expressions of the form `a < b`,
-such that `norm_num` successfully recognises both `a` and `b`. -/
-@[norm_num _ < _] def evalLT : NormNumExt where eval {v β} e := do
-  haveI' : v =QL 0 := ⟨⟩; haveI' : $β =Q Prop := ⟨⟩
-  let .app (.app f a) b ← whnfR e | failure
-  let ⟨u, α, a⟩ ← inferTypeQ' a
-  have b : Q($α) := b
-  let ra ← derive a; let rb ← derive b
-  let lα ← synthInstanceQ q(LT $α)
-  guard <|← withNewMCtxDepth <| isDefEq f q(LT.lt (α := $α))
-  evalLT.core lα ra rb
-
 end Mathlib.Meta.NormNum
diff --git a/Mathlib/Tactic/NormNum/Prime.lean b/Mathlib/Tactic/NormNum/Prime.lean
index 7f820165f0300a..adf338a09b55aa 100644
--- a/Mathlib/Tactic/NormNum/Prime.lean
+++ b/Mathlib/Tactic/NormNum/Prime.lean
@@ -120,37 +120,39 @@ theorem isNat_minFac_4 : {n n' k : ℕ} →
       _ ≤ n.minFac := h1.2.2
       _ ≤ m        := Nat.minFac_le_of_dvd hm h2mn
 
-/-- The core of the `norm_num` extension which normalizes expressions of the form `minFac n`.
-This is public for use in the `Nat.primeFactorsList_ofNat` simproc. -/
-partial def evalMinFac.core (n : Q(ℕ)) (nn : Q(ℕ)) (pn : Q(IsNat $n $nn))
-  (n' : ℕ) : MetaM (Result q(Nat.minFac $n)) := do
-    let sℕ : Q(AddMonoidWithOne ℕ) := q(Nat.instAddMonoidWithOne)
-    let rec aux (ek : Q(ℕ)) (prf : Q(MinFacHelper $nn $ek)) :
+/-- The `norm_num` extension which identifies expressions of the form `minFac n`. -/
+@[norm_num Nat.minFac _] partial def evalMinFac : NormNumExt where eval {_ _} e := do
+  let .app (.const ``Nat.minFac _) (n : Q(ℕ)) ← whnfR e | failure
+  let sℕ : Q(AddMonoidWithOne ℕ) := q(Nat.instAddMonoidWithOne)
+  let ⟨nn, pn⟩ ← deriveNat n sℕ
+  let n' := nn.natLit!
+  let rec aux (ek : Q(ℕ)) (prf : Q(MinFacHelper $nn $ek)) :
       (c : Q(ℕ)) × Q(IsNat (Nat.minFac $n) $c) :=
-      let k := ek.natLit!
-      -- remark: `deriveBool q($nn < $ek * $ek)` is 2x slower than the following test.
-      if n' < k * k then
-        let r : Q(Nat.ble ($ek * $ek) $nn = false) := (q(Eq.refl false) : Expr)
-        ⟨nn, q(isNat_minFac_4 $pn $prf $r)⟩
+    let k := ek.natLit!
+    -- remark: `deriveBool q($nn < $ek * $ek)` is 2x slower than the following test.
+    if n' < k * k then
+      let r : Q(Nat.ble ($ek * $ek) $nn = false) := (q(Eq.refl false) : Expr)
+      ⟨nn, q(isNat_minFac_4 $pn $prf $r)⟩
+    else
+      let d : ℕ := k.minFac
+      -- the following branch is not necessary for the correctness,
+      -- but makes the algorithm 2x faster
+      if d < k then
+        have ek' : Q(ℕ) := mkRawNatLit <| k + 2
+        let pk' : Q($ek + 2 = $ek') := (q(Eq.refl $ek') : Expr)
+        let pd := deriveNotPrime k d ek
+        aux ek' q(minFacHelper_2 $pk' $pd $prf)
+      -- remark: `deriveBool q($nn % $ek = 0)` is 5x slower than the following test
+      else if n' % k = 0 then
+        let r : Q(nat_lit 0 = $nn % $ek) := (q(Eq.refl 0) : Expr)
+        let r' : Q(IsNat (minFac $n) $ek) := q(isNat_minFac_3 _ $pn $prf $r)
+        ⟨ek, r'⟩
       else
-        let d : ℕ := k.minFac
-        -- the following branch is not necessary for the correctness,
-        -- but makes the algorithm 2x faster
-        if d < k then
-          have ek' : Q(ℕ) := mkRawNatLit <| k + 2
-          let pk' : Q($ek + 2 = $ek') := (q(Eq.refl $ek') : Expr)
-          let pd := deriveNotPrime k d ek
-          aux ek' q(minFacHelper_2 $pk' $pd $prf)
-        -- remark: `deriveBool q($nn % $ek = 0)` is 5x slower than the following test
-        else if n' % k = 0 then
-          let r : Q(nat_lit 0 = $nn % $ek) := (q(Eq.refl 0) : Expr)
-          let r' : Q(IsNat (minFac $n) $ek) := q(isNat_minFac_3 _ $pn $prf $r)
-          ⟨ek, r'⟩
-        else
-          let r : Q(Nat.beq ($nn % $ek) 0 = false) := (q(Eq.refl false) : Expr)
-          have ek' : Q(ℕ) := mkRawNatLit <| k + 2
-          let pk' : Q($ek + 2 = $ek') := (q(Eq.refl $ek') : Expr)
-          aux ek' q(minFacHelper_3 $pk' $r $prf)
+        let r : Q(Nat.beq ($nn % $ek) 0 = false) := (q(Eq.refl false) : Expr)
+        have ek' : Q(ℕ) := mkRawNatLit <| k + 2
+        let pk' : Q($ek + 2 = $ek') := (q(Eq.refl $ek') : Expr)
+        aux ek' q(minFacHelper_3 $pk' $r $prf)
+  let rec core : MetaM <| Result q(Nat.minFac $n) := do
     if n' = 1 then
       let pn : Q(IsNat $n (nat_lit 1)) := pn
       return .isNat sℕ q(nat_lit 1) q(isNat_minFac_1 $pn)
@@ -161,12 +163,7 @@ partial def evalMinFac.core (n : Q(ℕ)) (nn : Q(ℕ)) (pn : Q(IsNat $n $nn))
     let pq : Q(1 = $nn % 2) := (q(Eq.refl (nat_lit 1)) : Expr)
     let ⟨c, pc⟩ := aux q(nat_lit 3) q(minFacHelper_0 $nn $pp $pq)
     return .isNat sℕ c pc
-
-/-- The `norm_num` extension which identifies expressions of the form `minFac n`. -/
-@[norm_num Nat.minFac _] partial def evalMinFac : NormNumExt where eval {_ _} e := do
-  let .app (.const ``Nat.minFac _) (n : Q(ℕ)) ← whnfR e | failure
-  let ⟨nn, pn⟩ ← deriveNat n q(Nat.instAddMonoidWithOne)
-  evalMinFac.core n nn pn nn.natLit!
+  core
 
 theorem isNat_prime_0 : {n : ℕ} → IsNat n (nat_lit 0) → ¬ n.Prime
   | _, ⟨rfl⟩ => not_prime_zero
@@ -183,7 +180,7 @@ theorem isNat_not_prime {n n' : ℕ} (h : IsNat n n') : ¬n'.Prime → ¬n.Prime
 /-- The `norm_num` extension which identifies expressions of the form `Nat.Prime n`. -/
 @[norm_num Nat.Prime _] def evalNatPrime : NormNumExt where eval {_ _} e := do
   let .app (.const `Nat.Prime _) (n : Q(ℕ)) ← whnfR e | failure
-  let ⟨nn, pn⟩ ← deriveNat n q(Nat.instAddMonoidWithOne)
+  let ⟨nn, pn⟩ ← deriveNat n _
   let n' := nn.natLit!
   -- note: if `n` is not prime, we don't have to verify the calculation of `n.minFac`, we just have
   -- to compute it, which is a lot quicker
@@ -198,7 +195,7 @@ theorem isNat_not_prime {n n' : ℕ} (h : IsNat n n') : ¬n'.Prime → ¬n.Prime
         return .isFalse q(isNat_not_prime $pn $prf)
       let r : Q(Nat.ble 2 $nn = true) := (q(Eq.refl true) : Expr)
       let .isNat _ _lit (p2n : Q(IsNat (minFac $nn) $nn)) ←
-        evalMinFac.core nn nn q(.raw_refl _) nn.natLit! | failure
+        evalMinFac.core nn _ nn q(.raw_refl _) nn.natLit! | failure
       return .isTrue q(isNat_prime_2 $pn $r $p2n)
   core
 
diff --git a/Mathlib/Tactic/ReduceModChar.lean b/Mathlib/Tactic/ReduceModChar.lean
index 94bbc328731b37..115eed60892f84 100644
--- a/Mathlib/Tactic/ReduceModChar.lean
+++ b/Mathlib/Tactic/ReduceModChar.lean
@@ -8,11 +8,10 @@ module
 public meta import Mathlib.Util.AtLocation
 public import Mathlib.Data.ZMod.Basic  -- shake: keep (Qq dependency)
 public import Mathlib.RingTheory.Polynomial.Basic  -- shake: keep (Qq dependency)
+import all Mathlib.Tactic.NormNum.DivMod  -- for accessing `evalIntMod.go`
 public import Mathlib.Tactic.NormNum.PowMod
 public import Mathlib.Tactic.ReduceModChar.Ext
 
-import Mathlib.Tactic.NormNum.DivMod
-
 /-!
 # `reduce_mod_char` tactic
 
diff --git a/Mathlib/Tactic/Ring/Compare.lean b/Mathlib/Tactic/Ring/Compare.lean
index 072207e46a1d24..7d3f9da5a05e6a 100644
--- a/Mathlib/Tactic/Ring/Compare.lean
+++ b/Mathlib/Tactic/Ring/Compare.lean
@@ -5,6 +5,7 @@ Authors: Heather Macbeth
 -/
 module
 
+import all Mathlib.Tactic.NormNum.Ineq
 public import Mathlib.Tactic.NormNum.Ineq
 public import Mathlib.Tactic.Ring.Basic
 
diff --git a/Mathlib/Tactic/Simproc/Factors.lean b/Mathlib/Tactic/Simproc/Factors.lean
index 43225e44366a1b..c0a6e985dacc2c 100644
--- a/Mathlib/Tactic/Simproc/Factors.lean
+++ b/Mathlib/Tactic/Simproc/Factors.lean
@@ -5,6 +5,7 @@ Authors: Mario Carneiro, Eric Wieser
 -/
 module
 
+import all Mathlib.Tactic.NormNum.Prime  -- for accessing `evalMinFac.core`
 public import Mathlib.Data.Nat.Factors
 public import Mathlib.Tactic.NormNum.Prime
 
@@ -111,7 +112,7 @@ private partial def evalPrimeFactorsListAux
       have ehp₂ : Q(Nat.blt $ea $eb = true) :=
         have : a < b := lt_of_le_of_ne' hab h_ba_eq
         (q(Eq.refl (true)) : Expr)
-      let .isNat _ lit ehp₃ ← evalMinFac.core q($eb) q($eb) ehb b | failure
+      let .isNat _ lit ehp₃ ← evalMinFac.core q($eb) q(inferInstance) q($eb) ehb b | failure
       assertInstancesCommute
       have : $lit =Q $eb := ⟨⟩
       let ⟨l, p₄⟩ ← evalPrimeFactorsListAux ehm ehb
@@ -128,7 +129,7 @@ private partial def evalPrimeFactorsListAux
       let eh_a_lt_n : Q(Nat.blt $ea $en = true) :=
         have : a < n := by lia
         (q(Eq.refl true) : Expr)
-      let .isNat _ lit ehn_minFac ← evalMinFac.core q($en) q($enl) ehn n | failure
+      let .isNat _ lit ehn_minFac ← evalMinFac.core q($en) q(inferInstance) q($enl) ehn n | failure
       have : $lit =Q $en := ⟨⟩
       assertInstancesCommute
       pure ⟨q([$en]), q(FactorsHelper.singleton $en $eh_a_lt_n $ehn_minFac)⟩

From cfee7a589ee67bef6fec499aece81500a65f01ac Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Fri, 21 Aug 2026 18:31:11 +0200
Subject: [PATCH 2/7] step 1: extract evalIntMod.go

---
 Mathlib/Tactic/NormNum/DivMod.lean | 60 +++++++++++++++---------------
 1 file changed, 30 insertions(+), 30 deletions(-)

diff --git a/Mathlib/Tactic/NormNum/DivMod.lean b/Mathlib/Tactic/NormNum/DivMod.lean
index 8548e62573090a..62734ea9b8e61a 100644
--- a/Mathlib/Tactic/NormNum/DivMod.lean
+++ b/Mathlib/Tactic/NormNum/DivMod.lean
@@ -100,37 +100,23 @@ lemma isInt_emod {a b q m a' : ℤ} {b' r : ℕ}
 lemma isInt_emod_neg {a b : ℤ} {r : ℕ} (h : IsNat (a % -b) r) : IsNat (a % b) r :=
   ⟨by rw [← Int.emod_neg, h.out]⟩
 
-attribute [local instance] monadLiftOptionMetaM in
-/-- The `norm_num` extension which identifies expressions of the form `Int.emod a b`,
-such that `norm_num` successfully recognises both `a` and `b`. -/
-@[norm_num (_ : ℤ) % _, Int.emod _ _]
-partial def evalIntMod : NormNumExt where eval {u α} e := do
-  let .app (.app f (a : Q(ℤ))) (b : Q(ℤ)) ← whnfR e | failure
-  -- We assert that the default instance for `HMod` is `Int.mod` when the first parameter is `ℤ`.
-  guard <|← withNewMCtxDepth <| isDefEq f q(HMod.hMod (α := ℤ))
-  haveI' : u =QL 0 := ⟨⟩; haveI' : $α =Q ℤ := ⟨⟩
-  haveI' : $e =Q ($a % $b) := ⟨⟩
-  let rℤ : Q(Ring ℤ) := q(Int.instRing)
-  let some ⟨za, na, pa⟩ := (← derive a).toInt rℤ | failure
-  go a na za pa b (← derive (u := .zero) b)
+/-- Given a result for evaluating `a b` in `ℤ`, evaluate `a % b`. -/
+def evalIntMod.go (a na : Q(ℤ)) (za : ℤ) (pa : Q(IsInt $a $na))
+    (b : Q(ℤ)) : Result b → Option (Result q($a % $b))
+  | .isNat inst nb pb => do
+    assumeInstancesCommute
+    if nb.natLit! == 0 then
+      have _ : $nb =Q nat_lit 0 := ⟨⟩
+      return .isInt q(Int.instRing) na za q(isInt_emod_zero $pa $pb)
+    else
+      let ⟨r, p⟩ := core a na za pa b nb pb
+      return .isNat q(instAddMonoidWithOne) r p
+  | .isNegNat _ nb pb => do
+    assumeInstancesCommute
+    let ⟨r, p⟩ := core a na za pa q(-$b) nb q(isNat_neg_of_isNegNat $pb)
+    return .isNat q(instAddMonoidWithOne) r q(isInt_emod_neg $p)
+  | _ => none
 where
-  /-- Given a result for evaluating `a b` in `ℤ`, evaluate `a % b`. -/
-  go (a na : Q(ℤ)) (za : ℤ) (pa : Q(IsInt $a $na))
-      (b : Q(ℤ)) : Result b → Option (Result q($a % $b))
-    | .isNat inst nb pb => do
-      assumeInstancesCommute
-      if nb.natLit! == 0 then
-        have _ : $nb =Q nat_lit 0 := ⟨⟩
-        return .isInt q(Int.instRing) na za q(isInt_emod_zero $pa $pb)
-      else
-        let ⟨r, p⟩ := core a na za pa b nb pb
-        return .isNat q(instAddMonoidWithOne) r p
-    | .isNegNat _ nb pb => do
-      assumeInstancesCommute
-      let ⟨r, p⟩ := core a na za pa q(-$b) nb q(isNat_neg_of_isNegNat $pb)
-      return .isNat q(instAddMonoidWithOne) r q(isInt_emod_neg $p)
-    | _ => none
-
   /-- Given a result for evaluating `a b` in `ℤ` where `b > 0`, evaluate `a % b`. -/
   core (a na : Q(ℤ)) (za : ℤ) (pa : Q(IsInt $a $na))
       (b : Q(ℤ)) (nb : Q(ℕ)) (pb : Q(IsNat $b $nb)) :
@@ -147,6 +133,20 @@ where
     have pf₃ : Q(Nat.blt $nr $nb = true) := (q(Eq.refl true) :)
     ⟨nr, q(isInt_emod $pa $pb $pf₁ $pf₂ $pf₃)⟩
 
+attribute [local instance] monadLiftOptionMetaM in
+/-- The `norm_num` extension which identifies expressions of the form `Int.emod a b`,
+such that `norm_num` successfully recognises both `a` and `b`. -/
+@[norm_num (_ : ℤ) % _, Int.emod _ _]
+partial def evalIntMod : NormNumExt where eval {u α} e := do
+  let .app (.app f (a : Q(ℤ))) (b : Q(ℤ)) ← whnfR e | failure
+  -- We assert that the default instance for `HMod` is `Int.mod` when the first parameter is `ℤ`.
+  guard <|← withNewMCtxDepth <| isDefEq f q(HMod.hMod (α := ℤ))
+  haveI' : u =QL 0 := ⟨⟩; haveI' : $α =Q ℤ := ⟨⟩
+  haveI' : $e =Q ($a % $b) := ⟨⟩
+  let rℤ : Q(Ring ℤ) := q(Int.instRing)
+  let some ⟨za, na, pa⟩ := (← derive a).toInt rℤ | failure
+  go a na za pa b (← derive (u := .zero) b)
+
 theorem isInt_dvd_true : {a b : ℤ} → {a' b' c : ℤ} →
     IsInt a a' → IsInt b b' → Int.mul a' c = b' → a ∣ b
   | _, _, _, _, _, ⟨rfl⟩, ⟨rfl⟩, rfl => ⟨_, rfl⟩

From 9c522156d4ed72cc0fafb13cf7ea11884134c718 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Fri, 21 Aug 2026 19:12:49 +0200
Subject: [PATCH 3/7] step 2: extract evalLE.core and evalLT.core

---
 Mathlib/Tactic/NormNum/Ineq.lean | 44 ++++++++++++++++----------------
 1 file changed, 22 insertions(+), 22 deletions(-)

diff --git a/Mathlib/Tactic/NormNum/Ineq.lean b/Mathlib/Tactic/NormNum/Ineq.lean
index a70b42dde5a358..06ad3b26ea9aa9 100644
--- a/Mathlib/Tactic/NormNum/Ineq.lean
+++ b/Mathlib/Tactic/NormNum/Ineq.lean
@@ -179,21 +179,9 @@ theorem isInt_lt_false [Ring α] [PartialOrder α] [IsOrderedRing α] {a b : α}
   not_lt_of_ge (isInt_le_true hb ha h)
 
 attribute [local instance] monadLiftOptionMetaM in
-/-- The `norm_num` extension which identifies expressions of the form `a ≤ b`,
-such that `norm_num` successfully recognises both `a` and `b`. -/
-@[norm_num _ ≤ _] def evalLE : NormNumExt where eval {v β} e := do
-  haveI' : v =QL 0 := ⟨⟩; haveI' : $β =Q Prop := ⟨⟩
-  let .app (.app f a) b ← whnfR e | failure
-  let ⟨u, α, a⟩ ← inferTypeQ' a
-  have b : Q($α) := b
-  let ra ← derive a; let rb ← derive b
-  let lα ← synthInstanceQ q(LE $α)
-  guard <|← withNewMCtxDepth <| isDefEq f q(LE.le (α := $α))
-  core lα ra rb
-where
-  /-- Identify (as `true` or `false`) expressions of the form `a ≤ b`, where `a` and `b` are numeric
+/-- Identify (as `true` or `false`) expressions of the form `a ≤ b`, where `a` and `b` are numeric
   expressions whose evaluations to `NormNum.Result` have already been computed. -/
-  core {u : Level} {α : Q(Type u)} (lα : Q(LE $α)) {a b : Q($α)}
+def evalLE.core {u : Level} {α : Q(Type u)} (lα : Q(LE $α)) {a b : Q($α)}
     (ra : NormNum.Result a) (rb : NormNum.Result b) : MetaM (NormNum.Result q($a ≤ $b)) := do
   let e := q($a ≤ $b)
   let rec intArm : MetaM (Result e) := do
@@ -243,22 +231,22 @@ where
     else -- Nats can appear in an ordered ring without `CharZero`.
       intArm
 
-attribute [local instance] monadLiftOptionMetaM in
-/-- The `norm_num` extension which identifies expressions of the form `a < b`,
+/-- The `norm_num` extension which identifies expressions of the form `a ≤ b`,
 such that `norm_num` successfully recognises both `a` and `b`. -/
-@[norm_num _ < _] def evalLT : NormNumExt where eval {v β} e := do
+@[norm_num _ ≤ _] def evalLE : NormNumExt where eval {v β} e := do
   haveI' : v =QL 0 := ⟨⟩; haveI' : $β =Q Prop := ⟨⟩
   let .app (.app f a) b ← whnfR e | failure
   let ⟨u, α, a⟩ ← inferTypeQ' a
   have b : Q($α) := b
   let ra ← derive a; let rb ← derive b
-  let lα ← synthInstanceQ q(LT $α)
-  guard <|← withNewMCtxDepth <| isDefEq f q(LT.lt (α := $α))
+  let lα ← synthInstanceQ q(LE $α)
+  guard <|← withNewMCtxDepth <| isDefEq f q(LE.le (α := $α))
   core lα ra rb
-where
-  /-- Identify (as `true` or `false`) expressions of the form `a < b`, where `a` and `b` are numeric
+
+attribute [local instance] monadLiftOptionMetaM in
+/-- Identify (as `true` or `false`) expressions of the form `a < b`, where `a` and `b` are numeric
   expressions whose evaluations to `NormNum.Result` have already been computed. -/
-  core {u : Level} {α : Q(Type u)} (lα : Q(LT $α)) {a b : Q($α)}
+def evalLT.core {u : Level} {α : Q(Type u)} (lα : Q(LT $α)) {a b : Q($α)}
     (ra : NormNum.Result a) (rb : NormNum.Result b) : MetaM (NormNum.Result q($a < $b)) := do
   let e := q($a < $b)
   let rec intArm : MetaM (Result e) := do
@@ -323,4 +311,16 @@ where
       let r : Q(Nat.ble $nb $na = true) := (q(Eq.refl true) : Expr)
       return .isFalse q(isNat_lt_false $pa $pb $r)
 
+/-- The `norm_num` extension which identifies expressions of the form `a < b`,
+such that `norm_num` successfully recognises both `a` and `b`. -/
+@[norm_num _ < _] def evalLT : NormNumExt where eval {v β} e := do
+  haveI' : v =QL 0 := ⟨⟩; haveI' : $β =Q Prop := ⟨⟩
+  let .app (.app f a) b ← whnfR e | failure
+  let ⟨u, α, a⟩ ← inferTypeQ' a
+  have b : Q($α) := b
+  let ra ← derive a; let rb ← derive b
+  let lα ← synthInstanceQ q(LT $α)
+  guard <|← withNewMCtxDepth <| isDefEq f q(LT.lt (α := $α))
+  core lα ra rb
+
 end Mathlib.Meta.NormNum

From c2182aa63de7e2df8768683061b579e80ff33c07 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Fri, 21 Aug 2026 19:28:46 +0200
Subject: [PATCH 4/7] step 3: extract evalMinFac.core

---
 Mathlib/Tactic/NormNum/Prime.lean | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Tactic/NormNum/Prime.lean b/Mathlib/Tactic/NormNum/Prime.lean
index adf338a09b55aa..e4cd52998b5a72 100644
--- a/Mathlib/Tactic/NormNum/Prime.lean
+++ b/Mathlib/Tactic/NormNum/Prime.lean
@@ -120,9 +120,7 @@ theorem isNat_minFac_4 : {n n' k : ℕ} →
       _ ≤ n.minFac := h1.2.2
       _ ≤ m        := Nat.minFac_le_of_dvd hm h2mn
 
-/-- The `norm_num` extension which identifies expressions of the form `minFac n`. -/
-@[norm_num Nat.minFac _] partial def evalMinFac : NormNumExt where eval {_ _} e := do
-  let .app (.const ``Nat.minFac _) (n : Q(ℕ)) ← whnfR e | failure
+partial def evalMinFac.core (n : Q(ℕ)) := do
   let sℕ : Q(AddMonoidWithOne ℕ) := q(Nat.instAddMonoidWithOne)
   let ⟨nn, pn⟩ ← deriveNat n sℕ
   let n' := nn.natLit!
@@ -165,6 +163,11 @@ theorem isNat_minFac_4 : {n n' k : ℕ} →
     return .isNat sℕ c pc
   core
 
+/-- The `norm_num` extension which identifies expressions of the form `minFac n`. -/
+@[norm_num Nat.minFac _] partial def evalMinFac : NormNumExt where eval {_ _} e := do
+  let .app (.const ``Nat.minFac _) (n : Q(ℕ)) ← whnfR e | failure
+  evalMinFac.core n
+
 theorem isNat_prime_0 : {n : ℕ} → IsNat n (nat_lit 0) → ¬ n.Prime
   | _, ⟨rfl⟩ => not_prime_zero
 

From 9aacbc51a4bda1482f68881c095e8093b12034d1 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Fri, 21 Aug 2026 19:21:24 +0200
Subject: [PATCH 5/7] fix stuff that broke

---
 Mathlib/Tactic/NormNum/DivMod.lean |  6 +++---
 Mathlib/Tactic/NormNum/Ineq.lean   |  4 ++--
 Mathlib/Tactic/NormNum/Prime.lean  | 11 ++++++-----
 3 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/Mathlib/Tactic/NormNum/DivMod.lean b/Mathlib/Tactic/NormNum/DivMod.lean
index 62734ea9b8e61a..bd2589307b2d29 100644
--- a/Mathlib/Tactic/NormNum/DivMod.lean
+++ b/Mathlib/Tactic/NormNum/DivMod.lean
@@ -102,8 +102,8 @@ lemma isInt_emod_neg {a b : ℤ} {r : ℕ} (h : IsNat (a % -b) r) : IsNat (a % b
 
 /-- Given a result for evaluating `a b` in `ℤ`, evaluate `a % b`. -/
 def evalIntMod.go (a na : Q(ℤ)) (za : ℤ) (pa : Q(IsInt $a $na))
-    (b : Q(ℤ)) : Result b → Option (Result q($a % $b))
-  | .isNat inst nb pb => do
+    (b : Q(ℤ)) : Result (u := .zero) b → Option (Result q($a % $b))
+  | .isNat _ nb pb => do
     assumeInstancesCommute
     if nb.natLit! == 0 then
       have _ : $nb =Q nat_lit 0 := ⟨⟩
@@ -145,7 +145,7 @@ partial def evalIntMod : NormNumExt where eval {u α} e := do
   haveI' : $e =Q ($a % $b) := ⟨⟩
   let rℤ : Q(Ring ℤ) := q(Int.instRing)
   let some ⟨za, na, pa⟩ := (← derive a).toInt rℤ | failure
-  go a na za pa b (← derive (u := .zero) b)
+  evalIntMod.go a na za pa b (← derive (u := .zero) b)
 
 theorem isInt_dvd_true : {a b : ℤ} → {a' b' c : ℤ} →
     IsInt a a' → IsInt b b' → Int.mul a' c = b' → a ∣ b
diff --git a/Mathlib/Tactic/NormNum/Ineq.lean b/Mathlib/Tactic/NormNum/Ineq.lean
index 06ad3b26ea9aa9..033dbf8b9f864d 100644
--- a/Mathlib/Tactic/NormNum/Ineq.lean
+++ b/Mathlib/Tactic/NormNum/Ineq.lean
@@ -241,7 +241,7 @@ such that `norm_num` successfully recognises both `a` and `b`. -/
   let ra ← derive a; let rb ← derive b
   let lα ← synthInstanceQ q(LE $α)
   guard <|← withNewMCtxDepth <| isDefEq f q(LE.le (α := $α))
-  core lα ra rb
+  evalLE.core lα ra rb
 
 attribute [local instance] monadLiftOptionMetaM in
 /-- Identify (as `true` or `false`) expressions of the form `a < b`, where `a` and `b` are numeric
@@ -321,6 +321,6 @@ such that `norm_num` successfully recognises both `a` and `b`. -/
   let ra ← derive a; let rb ← derive b
   let lα ← synthInstanceQ q(LT $α)
   guard <|← withNewMCtxDepth <| isDefEq f q(LT.lt (α := $α))
-  core lα ra rb
+  evalLT.core lα ra rb
 
 end Mathlib.Meta.NormNum
diff --git a/Mathlib/Tactic/NormNum/Prime.lean b/Mathlib/Tactic/NormNum/Prime.lean
index e4cd52998b5a72..ca644629083118 100644
--- a/Mathlib/Tactic/NormNum/Prime.lean
+++ b/Mathlib/Tactic/NormNum/Prime.lean
@@ -120,10 +120,9 @@ theorem isNat_minFac_4 : {n n' k : ℕ} →
       _ ≤ n.minFac := h1.2.2
       _ ≤ m        := Nat.minFac_le_of_dvd hm h2mn
 
-partial def evalMinFac.core (n : Q(ℕ)) := do
+partial def evalMinFac.core (n : Q(ℕ)) (nn : Q(ℕ)) (pn : Q(IsNat $n $nn))
+    (n' : ℕ) : MetaM (Result q(Nat.minFac $n)) := do
   let sℕ : Q(AddMonoidWithOne ℕ) := q(Nat.instAddMonoidWithOne)
-  let ⟨nn, pn⟩ ← deriveNat n sℕ
-  let n' := nn.natLit!
   let rec aux (ek : Q(ℕ)) (prf : Q(MinFacHelper $nn $ek)) :
       (c : Q(ℕ)) × Q(IsNat (Nat.minFac $n) $c) :=
     let k := ek.natLit!
@@ -166,7 +165,9 @@ partial def evalMinFac.core (n : Q(ℕ)) := do
 /-- The `norm_num` extension which identifies expressions of the form `minFac n`. -/
 @[norm_num Nat.minFac _] partial def evalMinFac : NormNumExt where eval {_ _} e := do
   let .app (.const ``Nat.minFac _) (n : Q(ℕ)) ← whnfR e | failure
-  evalMinFac.core n
+  let ⟨nn, pn⟩ ← deriveNat n q(Nat.instAddMonoidWithOne)
+  let n' := nn.natLit!
+  evalMinFac.core n nn pn n'
 
 theorem isNat_prime_0 : {n : ℕ} → IsNat n (nat_lit 0) → ¬ n.Prime
   | _, ⟨rfl⟩ => not_prime_zero
@@ -198,7 +199,7 @@ theorem isNat_not_prime {n n' : ℕ} (h : IsNat n n') : ¬n'.Prime → ¬n.Prime
         return .isFalse q(isNat_not_prime $pn $prf)
       let r : Q(Nat.ble 2 $nn = true) := (q(Eq.refl true) : Expr)
       let .isNat _ _lit (p2n : Q(IsNat (minFac $nn) $nn)) ←
-        evalMinFac.core nn _ nn q(.raw_refl _) nn.natLit! | failure
+        evalMinFac.core nn nn q(.raw_refl _) nn.natLit! | failure
       return .isTrue q(isNat_prime_2 $pn $r $p2n)
   core
 

From 5be25e05445c1393fe55fb07947707494637a412 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Fri, 21 Aug 2026 19:38:51 +0200
Subject: [PATCH 6/7] optional changes

---
 Mathlib/Tactic/NormNum/Ineq.lean  |  4 ++--
 Mathlib/Tactic/NormNum/Prime.lean | 31 +++++++++++++++----------------
 2 files changed, 17 insertions(+), 18 deletions(-)

diff --git a/Mathlib/Tactic/NormNum/Ineq.lean b/Mathlib/Tactic/NormNum/Ineq.lean
index 033dbf8b9f864d..51d25f216fbb88 100644
--- a/Mathlib/Tactic/NormNum/Ineq.lean
+++ b/Mathlib/Tactic/NormNum/Ineq.lean
@@ -180,7 +180,7 @@ theorem isInt_lt_false [Ring α] [PartialOrder α] [IsOrderedRing α] {a b : α}
 
 attribute [local instance] monadLiftOptionMetaM in
 /-- Identify (as `true` or `false`) expressions of the form `a ≤ b`, where `a` and `b` are numeric
-  expressions whose evaluations to `NormNum.Result` have already been computed. -/
+expressions whose evaluations to `NormNum.Result` have already been computed. -/
 def evalLE.core {u : Level} {α : Q(Type u)} (lα : Q(LE $α)) {a b : Q($α)}
     (ra : NormNum.Result a) (rb : NormNum.Result b) : MetaM (NormNum.Result q($a ≤ $b)) := do
   let e := q($a ≤ $b)
@@ -245,7 +245,7 @@ such that `norm_num` successfully recognises both `a` and `b`. -/
 
 attribute [local instance] monadLiftOptionMetaM in
 /-- Identify (as `true` or `false`) expressions of the form `a < b`, where `a` and `b` are numeric
-  expressions whose evaluations to `NormNum.Result` have already been computed. -/
+expressions whose evaluations to `NormNum.Result` have already been computed. -/
 def evalLT.core {u : Level} {α : Q(Type u)} (lα : Q(LT $α)) {a b : Q($α)}
     (ra : NormNum.Result a) (rb : NormNum.Result b) : MetaM (NormNum.Result q($a < $b)) := do
   let e := q($a < $b)
diff --git a/Mathlib/Tactic/NormNum/Prime.lean b/Mathlib/Tactic/NormNum/Prime.lean
index ca644629083118..f7bc6ba91c95cd 100644
--- a/Mathlib/Tactic/NormNum/Prime.lean
+++ b/Mathlib/Tactic/NormNum/Prime.lean
@@ -120,6 +120,8 @@ theorem isNat_minFac_4 : {n n' k : ℕ} →
       _ ≤ n.minFac := h1.2.2
       _ ≤ m        := Nat.minFac_le_of_dvd hm h2mn
 
+/-- The core of the `norm_num` extension which normalizes expressions of the form `minFac n`.
+This is public for use in the `Nat.primeFactorsList_ofNat` simproc. -/
 partial def evalMinFac.core (n : Q(ℕ)) (nn : Q(ℕ)) (pn : Q(IsNat $n $nn))
     (n' : ℕ) : MetaM (Result q(Nat.minFac $n)) := do
   let sℕ : Q(AddMonoidWithOne ℕ) := q(Nat.instAddMonoidWithOne)
@@ -149,25 +151,22 @@ partial def evalMinFac.core (n : Q(ℕ)) (nn : Q(ℕ)) (pn : Q(IsNat $n $nn))
         have ek' : Q(ℕ) := mkRawNatLit <| k + 2
         let pk' : Q($ek + 2 = $ek') := (q(Eq.refl $ek') : Expr)
         aux ek' q(minFacHelper_3 $pk' $r $prf)
-  let rec core : MetaM <| Result q(Nat.minFac $n) := do
-    if n' = 1 then
-      let pn : Q(IsNat $n (nat_lit 1)) := pn
-      return .isNat sℕ q(nat_lit 1) q(isNat_minFac_1 $pn)
-    if n' % 2 = 0 then
-      let pq : Q($nn % 2 = 0) := (q(Eq.refl 0) : Expr)
-      return .isNat sℕ q(nat_lit 2) q(isNat_minFac_2 $pn $pq)
-    let pp : Q(Nat.ble 2 $nn = true) := (q(Eq.refl true) : Expr)
-    let pq : Q(1 = $nn % 2) := (q(Eq.refl (nat_lit 1)) : Expr)
-    let ⟨c, pc⟩ := aux q(nat_lit 3) q(minFacHelper_0 $nn $pp $pq)
-    return .isNat sℕ c pc
-  core
+  if n' = 1 then
+    let pn : Q(IsNat $n (nat_lit 1)) := pn
+    return .isNat sℕ q(nat_lit 1) q(isNat_minFac_1 $pn)
+  if n' % 2 = 0 then
+    let pq : Q($nn % 2 = 0) := (q(Eq.refl 0) : Expr)
+    return .isNat sℕ q(nat_lit 2) q(isNat_minFac_2 $pn $pq)
+  let pp : Q(Nat.ble 2 $nn = true) := (q(Eq.refl true) : Expr)
+  let pq : Q(1 = $nn % 2) := (q(Eq.refl (nat_lit 1)) : Expr)
+  let ⟨c, pc⟩ := aux q(nat_lit 3) q(minFacHelper_0 $nn $pp $pq)
+  return .isNat sℕ c pc
 
 /-- The `norm_num` extension which identifies expressions of the form `minFac n`. -/
 @[norm_num Nat.minFac _] partial def evalMinFac : NormNumExt where eval {_ _} e := do
   let .app (.const ``Nat.minFac _) (n : Q(ℕ)) ← whnfR e | failure
   let ⟨nn, pn⟩ ← deriveNat n q(Nat.instAddMonoidWithOne)
-  let n' := nn.natLit!
-  evalMinFac.core n nn pn n'
+  evalMinFac.core n nn pn nn.natLit!
 
 theorem isNat_prime_0 : {n : ℕ} → IsNat n (nat_lit 0) → ¬ n.Prime
   | _, ⟨rfl⟩ => not_prime_zero
@@ -184,7 +183,7 @@ theorem isNat_not_prime {n n' : ℕ} (h : IsNat n n') : ¬n'.Prime → ¬n.Prime
 /-- The `norm_num` extension which identifies expressions of the form `Nat.Prime n`. -/
 @[norm_num Nat.Prime _] def evalNatPrime : NormNumExt where eval {_ _} e := do
   let .app (.const `Nat.Prime _) (n : Q(ℕ)) ← whnfR e | failure
-  let ⟨nn, pn⟩ ← deriveNat n _
+  let ⟨nn, pn⟩ ← deriveNat n q(Nat.instAddMonoidWithOne)
   let n' := nn.natLit!
   -- note: if `n` is not prime, we don't have to verify the calculation of `n.minFac`, we just have
   -- to compute it, which is a lot quicker
@@ -199,7 +198,7 @@ theorem isNat_not_prime {n n' : ℕ} (h : IsNat n n') : ¬n'.Prime → ¬n.Prime
         return .isFalse q(isNat_not_prime $pn $prf)
       let r : Q(Nat.ble 2 $nn = true) := (q(Eq.refl true) : Expr)
       let .isNat _ _lit (p2n : Q(IsNat (minFac $nn) $nn)) ←
-        evalMinFac.core nn nn q(.raw_refl _) nn.natLit! | failure
+        evalMinFac.core nn nn q(.raw_refl _) n' | failure
       return .isTrue q(isNat_prime_2 $pn $r $p2n)
   core
 

From e02b8ed111208e59e93ad4fbf7bd133ab31ca284 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Fri, 21 Aug 2026 19:43:47 +0200
Subject: [PATCH 7/7] remove public imports

---
 Mathlib/Tactic/ReduceModChar.lean   | 3 ++-
 Mathlib/Tactic/Ring/Compare.lean    | 1 -
 Mathlib/Tactic/Simproc/Factors.lean | 5 ++---
 3 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Tactic/ReduceModChar.lean b/Mathlib/Tactic/ReduceModChar.lean
index 115eed60892f84..94bbc328731b37 100644
--- a/Mathlib/Tactic/ReduceModChar.lean
+++ b/Mathlib/Tactic/ReduceModChar.lean
@@ -8,10 +8,11 @@ module
 public meta import Mathlib.Util.AtLocation
 public import Mathlib.Data.ZMod.Basic  -- shake: keep (Qq dependency)
 public import Mathlib.RingTheory.Polynomial.Basic  -- shake: keep (Qq dependency)
-import all Mathlib.Tactic.NormNum.DivMod  -- for accessing `evalIntMod.go`
 public import Mathlib.Tactic.NormNum.PowMod
 public import Mathlib.Tactic.ReduceModChar.Ext
 
+import Mathlib.Tactic.NormNum.DivMod
+
 /-!
 # `reduce_mod_char` tactic
 
diff --git a/Mathlib/Tactic/Ring/Compare.lean b/Mathlib/Tactic/Ring/Compare.lean
index 7d3f9da5a05e6a..072207e46a1d24 100644
--- a/Mathlib/Tactic/Ring/Compare.lean
+++ b/Mathlib/Tactic/Ring/Compare.lean
@@ -5,7 +5,6 @@ Authors: Heather Macbeth
 -/
 module
 
-import all Mathlib.Tactic.NormNum.Ineq
 public import Mathlib.Tactic.NormNum.Ineq
 public import Mathlib.Tactic.Ring.Basic
 
diff --git a/Mathlib/Tactic/Simproc/Factors.lean b/Mathlib/Tactic/Simproc/Factors.lean
index c0a6e985dacc2c..43225e44366a1b 100644
--- a/Mathlib/Tactic/Simproc/Factors.lean
+++ b/Mathlib/Tactic/Simproc/Factors.lean
@@ -5,7 +5,6 @@ Authors: Mario Carneiro, Eric Wieser
 -/
 module
 
-import all Mathlib.Tactic.NormNum.Prime  -- for accessing `evalMinFac.core`
 public import Mathlib.Data.Nat.Factors
 public import Mathlib.Tactic.NormNum.Prime
 
@@ -112,7 +111,7 @@ private partial def evalPrimeFactorsListAux
       have ehp₂ : Q(Nat.blt $ea $eb = true) :=
         have : a < b := lt_of_le_of_ne' hab h_ba_eq
         (q(Eq.refl (true)) : Expr)
-      let .isNat _ lit ehp₃ ← evalMinFac.core q($eb) q(inferInstance) q($eb) ehb b | failure
+      let .isNat _ lit ehp₃ ← evalMinFac.core q($eb) q($eb) ehb b | failure
       assertInstancesCommute
       have : $lit =Q $eb := ⟨⟩
       let ⟨l, p₄⟩ ← evalPrimeFactorsListAux ehm ehb
@@ -129,7 +128,7 @@ private partial def evalPrimeFactorsListAux
       let eh_a_lt_n : Q(Nat.blt $ea $en = true) :=
         have : a < n := by lia
         (q(Eq.refl true) : Expr)
-      let .isNat _ lit ehn_minFac ← evalMinFac.core q($en) q(inferInstance) q($enl) ehn n | failure
+      let .isNat _ lit ehn_minFac ← evalMinFac.core q($en) q($enl) ehn n | failure
       have : $lit =Q $en := ⟨⟩
       assertInstancesCommute
       pure ⟨q([$en]), q(FactorsHelper.singleton $en $eh_a_lt_n $ehn_minFac)⟩