From a605b1a6a0c0cd4e6dfd04df92247d020441d7c1 Mon Sep 17 00:00:00 2001
From: thorimur <68410468+thorimur@users.noreply.github.com>
Date: Tue, 4 Aug 2026 18:26:51 -0400
Subject: [PATCH 1/7] chore: remove `import all` by making `norm_num` component
 public

---
 Mathlib/Tactic/NormNum/Prime.lean   | 71 +++++++++++++++--------------
 Mathlib/Tactic/Simproc/Factors.lean |  6 +--
 2 files changed, 40 insertions(+), 37 deletions(-)

diff --git a/Mathlib/Tactic/NormNum/Prime.lean b/Mathlib/Tactic/NormNum/Prime.lean
index adf338a09b55aa..d314f80c55b9eb 100644
--- a/Mathlib/Tactic/NormNum/Prime.lean
+++ b/Mathlib/Tactic/NormNum/Prime.lean
@@ -120,39 +120,37 @@ 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
-  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)) :
+/-- 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(«$n».minFac)) := do
+    let sℕ : Q(AddMonoidWithOne ℕ) := q(Nat.instAddMonoidWithOne)
+    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)⟩
-    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'⟩
+      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 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
+        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)
     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)
@@ -163,7 +161,12 @@ theorem isNat_minFac_4 : {n n' k : ℕ} →
     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
+
+/-- 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!
 
 theorem isNat_prime_0 : {n : ℕ} → IsNat n (nat_lit 0) → ¬ n.Prime
   | _, ⟨rfl⟩ => not_prime_zero
@@ -180,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
@@ -195,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 _) nn.natLit! | failure
       return .isTrue q(isNat_prime_2 $pn $r $p2n)
   core
 
diff --git a/Mathlib/Tactic/Simproc/Factors.lean b/Mathlib/Tactic/Simproc/Factors.lean
index c0a6e985dacc2c..d37b064650830b 100644
--- a/Mathlib/Tactic/Simproc/Factors.lean
+++ b/Mathlib/Tactic/Simproc/Factors.lean
@@ -5,7 +5,7 @@ Authors: Mario Carneiro, Eric Wieser
 -/
 module
 
-import all Mathlib.Tactic.NormNum.Prime  -- for accessing `evalMinFac.core`
+import Mathlib.Tactic.NormNum.Prime
 public import Mathlib.Data.Nat.Factors
 public import Mathlib.Tactic.NormNum.Prime
 
@@ -112,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(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 +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(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)⟩

From 1b404e9eba7f2ddba179f1d36b0763c67a592723 Mon Sep 17 00:00:00 2001
From: thorimur <68410468+thorimur@users.noreply.github.com>
Date: Tue, 4 Aug 2026 18:29:20 -0400
Subject: [PATCH 2/7] chore: oops, redundant import

---
 Mathlib/Tactic/Simproc/Factors.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Tactic/Simproc/Factors.lean b/Mathlib/Tactic/Simproc/Factors.lean
index d37b064650830b..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 Mathlib.Tactic.NormNum.Prime
 public import Mathlib.Data.Nat.Factors
 public import Mathlib.Tactic.NormNum.Prime
 

From 2ff555a783746cdbd76cc8e2562777a99254cbc8 Mon Sep 17 00:00:00 2001
From: "Thomas R. Murrills" <68410468+thorimur@users.noreply.github.com>
Date: Tue, 4 Aug 2026 19:21:43 -0400
Subject: [PATCH 3/7] chore: fix copied type signature

---
 Mathlib/Tactic/NormNum/Prime.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Tactic/NormNum/Prime.lean b/Mathlib/Tactic/NormNum/Prime.lean
index d314f80c55b9eb..7f820165f0300a 100644
--- a/Mathlib/Tactic/NormNum/Prime.lean
+++ b/Mathlib/Tactic/NormNum/Prime.lean
@@ -122,8 +122,8 @@ theorem isNat_minFac_4 : {n n' k : ℕ} →
 
 /-- 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(«$n».minFac)) := 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 rec aux (ek : Q(ℕ)) (prf : Q(MinFacHelper $nn $ek)) :
       (c : Q(ℕ)) × Q(IsNat (Nat.minFac $n) $c) :=

From 47e62a3e0e0e29cd12e59373b5ee8ac689067695 Mon Sep 17 00:00:00 2001
From: thorimur <68410468+thorimur@users.noreply.github.com>
Date: Tue, 4 Aug 2026 19:40:20 -0400
Subject: [PATCH 4/7] chore: more public norm_num components

---
 Mathlib/Tactic/NormNum/DivMod.lean | 60 +++++++++++++++---------------
 Mathlib/Tactic/NormNum/Ineq.lean   | 50 ++++++++++++-------------
 Mathlib/Tactic/ReduceModChar.lean  |  3 +-
 Mathlib/Tactic/Ring/Compare.lean   |  1 -
 4 files changed, 57 insertions(+), 57 deletions(-)

diff --git a/Mathlib/Tactic/NormNum/DivMod.lean b/Mathlib/Tactic/NormNum/DivMod.lean
index 8548e62573090a..bd2589307b2d29 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 (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
 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
+  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 a70b42dde5a358..51d25f216fbb88 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
-  expressions whose evaluations to `NormNum.Result` have already been computed. -/
-  core {u : Level} {α : Q(Type u)} (lα : Q(LE $α)) {a b : Q($α)}
+/-- 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($α)}
     (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 (α := $α))
-  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($α)}
+  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($α)}
     (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 (α := $α))
+  evalLT.core lα ra rb
+
 end Mathlib.Meta.NormNum
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
 

From bcb6f994802f8dd3ebda725da2c1417ac2509e8b Mon Sep 17 00:00:00 2001
From: "Thomas R. Murrills" <68410468+thorimur@users.noreply.github.com>
Date: Mon, 31 Aug 2026 19:24:51 -0400
Subject: [PATCH 5/7] Update Mathlib/Tactic/NormNum/Prime.lean

Co-authored-by: Jon Eugster <eugster.jon@gmail.com>
---
 Mathlib/Tactic/NormNum/Prime.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Tactic/NormNum/Prime.lean b/Mathlib/Tactic/NormNum/Prime.lean
index 7f820165f0300a..5f9b13436c2841 100644
--- a/Mathlib/Tactic/NormNum/Prime.lean
+++ b/Mathlib/Tactic/NormNum/Prime.lean
@@ -123,9 +123,9 @@ theorem isNat_minFac_4 : {n n' k : ℕ} →
 /-- 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)) :
+    (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)) :
       (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.

From 03b921d63102e1c8cf897db06e01d6a0ce50df10 Mon Sep 17 00:00:00 2001
From: "Thomas R. Murrills" <68410468+thorimur@users.noreply.github.com>
Date: Mon, 31 Aug 2026 19:25:42 -0400
Subject: [PATCH 6/7] Apply suggestion from @joneugster

Co-authored-by: Jon Eugster <eugster.jon@gmail.com>
---
 Mathlib/Tactic/NormNum/Prime.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Tactic/NormNum/Prime.lean b/Mathlib/Tactic/NormNum/Prime.lean
index 5f9b13436c2841..14c037f0496820 100644
--- a/Mathlib/Tactic/NormNum/Prime.lean
+++ b/Mathlib/Tactic/NormNum/Prime.lean
@@ -198,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 71a605ef33451c0873a25e5b30f0379c33c6d1b8 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Fri, 4 Sep 2026 12:12:12 +0200
Subject: [PATCH 7/7] fix indentation

---
 Mathlib/Tactic/NormNum/Prime.lean | 66 +++++++++++++++----------------
 1 file changed, 33 insertions(+), 33 deletions(-)

diff --git a/Mathlib/Tactic/NormNum/Prime.lean b/Mathlib/Tactic/NormNum/Prime.lean
index 14c037f0496820..f7bc6ba91c95cd 100644
--- a/Mathlib/Tactic/NormNum/Prime.lean
+++ b/Mathlib/Tactic/NormNum/Prime.lean
@@ -127,40 +127,40 @@ partial def evalMinFac.core (n : Q(ℕ)) (nn : Q(ℕ)) (pn : Q(IsNat $n $nn))
   let sℕ : Q(AddMonoidWithOne ℕ) := q(Nat.instAddMonoidWithOne)
   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)
-    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
+        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)
+  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