refactor(Tactic/NormNum): expose the derive API for known expressions directly (#28621)

eric-wieser · eric-wieser · commit 4cb1b3ce077a · 2025-08-20T15:48:11.000Z
We already exposed these through a janky `core` method, this now makes them more obviously part of the API, via dot notation. Most of the norm_num changes are just moves out to an auxiliary function. This should make it possible to write `← (← ra.mul rb).add (← rc.mul rd)` to derive a term of the form `a * b + c * d`. This deletes the `core` methods, but we could instead deprecate them. `:= by exact q(delta% inferInstance)` is from [#metaprogramming / tactics > A Qq gotcha @ 💬](https://leanprover.zulipchat.com/#narrow/channel/239415-metaprogramming-.2F-tactics/topic/A.20Qq.20gotcha/near/535030050).
diff --git a/Mathlib/Tactic/NormNum/Basic.lean b/Mathlib/Tactic/NormNum/Basic.lean
@@ -223,20 +223,19 @@ def _root_.Mathlib.Meta.monadLiftOptionMetaM : MonadLift Option MetaM where
   | some e => pure e
 
 attribute [local instance] monadLiftOptionMetaM in
-/-- Main part of `evalAdd`. -/
-def evalAdd.core {u : Level} {α : Q(Type u)} (e : Q(«$α»)) (f : Q(«$α» → «$α» → «$α»))
-    (a b : Q(«$α»)) (ra : Result a) (rb : Result b) : MetaM (Result e) := do
+/-- The result of adding two norm_num results. -/
+def Result.add {u : Level} {α : Q(Type u)} {a b : Q($α)} (ra : Result q($a)) (rb : Result q($b))
+    (inst : Q(Add $α) := by exact q(delta% inferInstance)) :
+    MetaM (Result q($a + $b)) := do
   let rec intArm (rα : Q(Ring $α)) := do
-    haveI' : $e =Q $a + $b := ⟨⟩
+    assumeInstancesCommute
     let ⟨za, na, pa⟩ ← ra.toInt _; let ⟨zb, nb, pb⟩ ← rb.toInt _
-    haveI' : $f =Q HAdd.hAdd := ⟨⟩
     let zc := za + zb
     have c := mkRawIntLit zc
     haveI' : Int.add $na $nb =Q $c := ⟨⟩
-    return .isInt rα c zc q(isInt_add (f := $f) (.refl $f) $pa $pb (.refl $c))
-  let rec nnratArm (dsα : Q(DivisionSemiring $α)) : Option (Result _) := do
-    haveI' : $e =Q $a + $b := ⟨⟩
-    haveI' : $f =Q HAdd.hAdd := ⟨⟩
+    return .isInt rα c zc q(isInt_add (.refl _) $pa $pb (.refl $c))
+  let rec nnratArm (dsα : Q(DivisionSemiring $α)) : MetaM (Result _) := do
+    assumeInstancesCommute
     let ⟨qa, na, da, pa⟩ ← ra.toNNRat' dsα; let ⟨qb, nb, db, pb⟩ ← rb.toNNRat' dsα
     let qc := qa + qb
     let dd := qa.den * qb.den
@@ -249,10 +248,9 @@ def evalAdd.core {u : Level} {α : Q(Type u)} (e : Q(«$α»)) (f : Q(«$α» 
     let r1 : Q(Nat.add (Nat.mul $na $db) (Nat.mul $nb $da) = Nat.mul $k $nc) :=
       (q(Eq.refl $t1) : Expr)
     let r2 : Q(Nat.mul $da $db = Nat.mul $k $dc) := (q(Eq.refl $t2) : Expr)
-    return .isNNRat' dsα qc nc dc q(isNNRat_add (f := $f) (.refl $f) $pa $pb $r1 $r2)
-  let rec ratArm (dα : Q(DivisionRing $α)) : Option (Result _) := do
-    haveI' : $e =Q $a + $b := ⟨⟩
-    haveI' : $f =Q HAdd.hAdd := ⟨⟩
+    return .isNNRat' dsα qc nc dc q(isNNRat_add (.refl _) $pa $pb $r1 $r2)
+  let rec ratArm (dα : Q(DivisionRing $α)) : MetaM (Result _) := do
+    assumeInstancesCommute
     let ⟨qa, na, da, pa⟩ ← ra.toRat' dα; let ⟨qb, nb, db, pb⟩ ← rb.toRat' dα
     let qc := qa + qb
     let dd := qa.den * qb.den
@@ -265,25 +263,26 @@ def evalAdd.core {u : Level} {α : Q(Type u)} (e : Q(«$α»)) (f : Q(«$α» 
     let r1 : Q(Int.add (Int.mul $na $db) (Int.mul $nb $da) = Int.mul $k $nc) :=
       (q(Eq.refl $t1) : Expr)
     let r2 : Q(Nat.mul $da $db = Nat.mul $k $dc) := (q(Eq.refl $t2) : Expr)
-    return .isRat dα qc nc dc q(isRat_add (f := $f) (.refl $f) $pa $pb $r1 $r2)
+    return .isRat dα qc nc dc q(isRat_add (.refl _) $pa $pb $r1 $r2)
   match ra, rb with
   | .isBool .., _ | _, .isBool .. => failure
   | .isNegNNRat dα .., _ | _, .isNegNNRat dα .. => ratArm dα
   -- mixing positive rationals and negative naturals means we need to use the full rat handler
   | .isNNRat _dsα .., .isNegNat _rα .. | .isNegNat _rα .., .isNNRat _dsα .. =>
     -- could alternatively try to combine `rα` and `dsα` here, but we'd have to do a defeq check
     -- so would still need to be in `MetaM`.
-    ratArm (←synthInstanceQ q(DivisionRing $α))
+    let dα ← synthInstanceQ q(DivisionRing $α)
+    assumeInstancesCommute
+    ratArm q($dα)
   | .isNNRat dsα .., _ | _, .isNNRat dsα .. => nnratArm dsα
   | .isNegNat rα .., _ | _, .isNegNat rα .. => intArm rα
   | .isNat _ na pa, .isNat sα nb pb =>
-    haveI' : $e =Q $a + $b := ⟨⟩
-    haveI' : $f =Q HAdd.hAdd := ⟨⟩
     assumeInstancesCommute
     have c : Q(ℕ) := mkRawNatLit (na.natLit! + nb.natLit!)
     haveI' : Nat.add $na $nb =Q $c := ⟨⟩
-    return .isNat sα c q(isNat_add (f := $f) (.refl $f) $pa $pb (.refl $c))
+    return .isNat sα c q(isNat_add (.refl _) $pa $pb (.refl $c))
 
+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 evalAdd : NormNumExt where eval {u α} e := do
@@ -300,7 +299,7 @@ such that `norm_num` successfully recognises both `a` and `b`. -/
   | .isNegNNRat _ .., .isNat _ .. | .isNegNNRat _ .., .isNegNat _ ..
     | .isNegNNRat _ .., .isNNRat _ .. | .isNegNNRat _ .., .isNegNNRat _ .. =>
     guard <|← withNewMCtxDepth <| isDefEq f q(HAdd.hAdd (α := $α))
-  evalAdd.core q($e) q($f) q($a) q($b) ra rb
+    ra.add rb
 
 -- see note [norm_num lemma function equality]
 theorem isInt_neg {α} [Ring α] : ∀ {f : α → α} {a : α} {a' b : ℤ},
@@ -313,40 +312,41 @@ theorem isRat_neg {α} [Ring α] : ∀ {f : α → α} {a : α} {n n' : ℤ} {d
   | _, _, _, _, _, rfl, ⟨h, rfl⟩, rfl => ⟨h, by rw [← neg_mul, ← Int.cast_neg]; rfl⟩
 
 attribute [local instance] monadLiftOptionMetaM in
-/-- Main part of `evalNeg`. -/
-def evalNeg.core {u : Level} {α : Q(Type u)} (e : Q(«$α»)) (f : Q(«$α» → «$α»)) (a : Q(«$α»))
-    (ra : Result a) (rα : Q(Ring «$α»)) : MetaM (Result e) := do
-  have : $f =Q Neg.neg := ⟨⟩
-  haveI' _e_eq : $e =Q -$a := ⟨⟩
+/-- The result of subtracting two norm_num results. -/
+def Result.neg {u : Level} {α : Q(Type u)} {a : Q($α)} (ra : Result q($a))
+    (rα : Q(Ring $α) := by exact q(delta% inferInstance)) :
+    MetaM (Result q(-$a)) := do
   let intArm (rα : Q(Ring $α)) := do
     assumeInstancesCommute
     let ⟨za, na, pa⟩ ← ra.toInt rα
     let zb := -za
     have b := mkRawIntLit zb
     haveI' : Int.neg $na =Q $b := ⟨⟩
-    return .isInt rα b zb q(isInt_neg (f := $f) (.refl $f) $pa (.refl $b))
+    return .isInt rα b zb q(isInt_neg (.refl _) $pa (.refl $b))
   let ratArm (dα : Q(DivisionRing $α)) : Option (Result _) := do
     assumeInstancesCommute
     let ⟨qa, na, da, pa⟩ ← ra.toRat' dα
     let qb := -qa
     have nb := mkRawIntLit qb.num
     haveI' : Int.neg $na =Q $nb := ⟨⟩
-    return .isRat dα qb nb da q(isRat_neg (f := $f) (.refl $f) $pa (.refl $nb))
+    return .isRat dα qb nb da q(isRat_neg (.refl _) $pa (.refl $nb))
   match ra with
   | .isBool _ .. => failure
   | .isNat _ .. => intArm rα
   | .isNegNat rα .. => intArm rα
   | .isNNRat _dsα .. => ratArm (← synthInstanceQ q(DivisionRing $α))
   | .isNegNNRat dα .. => ratArm dα
 
+attribute [local instance] monadLiftOptionMetaM in
 /-- The `norm_num` extension which identifies expressions of the form `-a`,
 such that `norm_num` successfully recognises `a`. -/
 @[norm_num -_] def evalNeg : NormNumExt where eval {u α} e := do
   let .app (f : Q($α → $α)) (a : Q($α)) ← whnfR e | failure
   let ra ← derive a
   let rα ← inferRing α
   let ⟨(_f_eq : $f =Q Neg.neg)⟩ ← withNewMCtxDepth <| assertDefEqQ _ _
-  evalNeg.core q($e) q($f) q($a) ra rα
+  haveI' _e_eq : $e =Q -$a := ⟨⟩
+  ra.neg
 
 -- see note [norm_num lemma function equality]
 theorem isInt_sub {α} [Ring α] : ∀ {f : α → α → α} {a b : α} {a' b' c : ℤ},
@@ -364,19 +364,18 @@ theorem isRat_sub {α} [Ring α] {f : α → α → α} {a b : α} {na nb nc : 
   rw [show Int.mul (-nb) _ = _ from neg_mul ..]; exact h₁
 
 attribute [local instance] monadLiftOptionMetaM in
-/-- Main part of `evalSub`. -/
-def evalSub.core {u : Level} {α : Q(Type u)} (e : Q(«$α»)) (f : Q(«$α» → «$α» → «$α»))
-    (a b : Q(«$α»)) (rα : Q(Ring «$α»)) (ra : Result a) (rb : Result b) : MetaM (Result e) := do
-  have : $f =Q HSub.hSub := ⟨⟩
-  haveI' _e_eq : $e =Q $a - $b := ⟨⟩
+/-- The result of subtracting two norm_num results. -/
+def Result.sub {u : Level} {α : Q(Type u)} {a b : Q($α)} (ra : Result q($a)) (rb : Result q($b))
+    (inst : Q(Ring $α) := by exact q(delta% inferInstance)) :
+    MetaM (Result q($a - $b)) := do
   let intArm (rα : Q(Ring $α)) := do
     assumeInstancesCommute
     let ⟨za, na, pa⟩ ← ra.toInt rα; let ⟨zb, nb, pb⟩ ← rb.toInt rα
     let zc := za - zb
     have c := mkRawIntLit zc
     haveI' : Int.sub $na $nb =Q $c := ⟨⟩
-    return Result.isInt rα c zc q(isInt_sub (f := $f) (.refl $f) $pa $pb (.refl $c))
-  let ratArm (dα : Q(DivisionRing $α)) : Option (Result _) := do
+    return Result.isInt rα c zc q(isInt_sub (.refl _) $pa $pb (.refl $c))
+  let ratArm (dα : Q(DivisionRing $α)) : MetaM (Result _) := do
     assumeInstancesCommute
     let ⟨qa, na, da, pa⟩ ← ra.toRat' dα; let ⟨qb, nb, db, pb⟩ ← rb.toRat' dα
     let qc := qa - qb
@@ -390,16 +389,18 @@ def evalSub.core {u : Level} {α : Q(Type u)} (e : Q(«$α»)) (f : Q(«$α» 
     let r1 : Q(Int.sub (Int.mul $na $db) (Int.mul $nb $da) = Int.mul $k $nc) :=
       (q(Eq.refl $t1) : Expr)
     let r2 : Q(Nat.mul $da $db = Nat.mul $k $dc) := (q(Eq.refl $t2) : Expr)
-    return .isRat dα qc nc dc q(isRat_sub (f := $f) (.refl $f) $pa $pb $r1 $r2)
+    return .isRat dα qc nc dc q(isRat_sub (.refl _) $pa $pb $r1 $r2)
   match ra, rb with
   | .isBool .., _ | _, .isBool .. => failure
   | .isNegNNRat dα .., _ | _, .isNegNNRat dα .. =>
     ratArm dα
   | _, .isNNRat _dsα .. | .isNNRat _dsα .., _ =>
     ratArm (← synthInstanceQ q(DivisionRing $α))
-  | .isNegNat rα .., _ | _, .isNegNat rα ..
-  | .isNat _ .., .isNat _ .. => intArm rα
+  | .isNegNat _rα .., _ | _, .isNegNat _rα ..
+  | .isNat _ .., .isNat _ .. =>
+    intArm inst
 
+attribute [local instance] monadLiftOptionMetaM in
 /-- The `norm_num` extension which identifies expressions of the form `a - b` in a ring,
 such that `norm_num` successfully recognises both `a` and `b`. -/
 @[norm_num _ - _] def evalSub : NormNumExt where eval {u α} e := do
@@ -408,7 +409,7 @@ such that `norm_num` successfully recognises both `a` and `b`. -/
   let ⟨(_f_eq : $f =Q HSub.hSub)⟩ ← withNewMCtxDepth <| assertDefEqQ _ _
   let ra ← derive a; let rb ← derive b
   haveI' _e_eq : $e =Q $a - $b := ⟨⟩
-  evalSub.core q($e) q($f) q($a) q($b) q($rα) ra rb
+  ra.sub rb
 
 -- see note [norm_num lemma function equality]
 theorem isNat_mul {α} [Semiring α] : ∀ {f : α → α → α} {a b : α} {a' b' c : ℕ},
@@ -461,19 +462,18 @@ theorem isRat_mul {α} [Ring α] {f : α → α → α} {a b : α} {na nb nc : 
     (Nat.cast_commute (α := α) db dc).invOf_left.invOf_right.right_comm]
 
 attribute [local instance] monadLiftOptionMetaM in
-/-- Main part of `evalMul`. -/
-def evalMul.core {u : Level} {α : Q(Type u)} (e : Q(«$α»)) (f : Q(«$α» → «$α» → «$α»))
-    (a b : Q(«$α»)) (sα : Q(Semiring «$α»)) (ra : Result a) (rb : Result b) : MetaM (Result e) := do
-  haveI' : $f =Q HMul.hMul := ⟨⟩
-  haveI' : $e =Q $a * $b := ⟨⟩
-  let rec intArm (rα : Q(Ring $α)) := do
+/-- The result of multiplying two norm_num results. -/
+def Result.mul {u : Level} {α : Q(Type u)} {a b : Q($α)} (ra : Result q($a)) (rb : Result q($b))
+    (inst : Q(Semiring $α) := by exact q(delta% inferInstance)) :
+    MetaM (Result q($a * $b)) := do
+  let intArm (rα : Q(Ring $α)) := do
     assumeInstancesCommute
     let ⟨za, na, pa⟩ ← ra.toInt rα; let ⟨zb, nb, pb⟩ ← rb.toInt rα
     let zc := za * zb
     have c := mkRawIntLit zc
     haveI' : Int.mul $na $nb =Q $c := ⟨⟩
-    return .isInt rα c zc q(isInt_mul (f := $f) (.refl $f) $pa $pb (.refl $c))
-  let rec nnratArm (dsα : Q(DivisionSemiring $α)) : Option (Result _) := do
+    return .isInt rα c zc q(isInt_mul (.refl _) $pa $pb (.refl $c))
+  let nnratArm (dsα : Q(DivisionSemiring $α)) : Option (Result _) := do
     assumeInstancesCommute
     let ⟨qa, na, da, pa⟩ ← ra.toNNRat' dsα; let ⟨qb, nb, db, pb⟩ ← rb.toNNRat' dsα
     let qc := qa * qb
@@ -486,7 +486,7 @@ def evalMul.core {u : Level} {α : Q(Type u)} (e : Q(«$α»)) (f : Q(«$α» 
       (q(Eq.refl (Nat.mul $na $nb)) : Expr)
     have t2 : Q(ℕ) := mkRawNatLit dd
     let r2 : Q(Nat.mul $da $db = Nat.mul $k $dc) := (q(Eq.refl $t2) : Expr)
-    return .isNNRat' dsα qc nc dc q(isNNRat_mul (f := $f) (.refl $f) $pa $pb $r1 $r2)
+    return .isNNRat' dsα qc nc dc q(isNNRat_mul (.refl _) $pa $pb $r1 $r2)
   let rec ratArm (dα : Q(DivisionRing $α)) : Option (Result _) := do
     assumeInstancesCommute
     let ⟨qa, na, da, pa⟩ ← ra.toRat' dα; let ⟨qb, nb, db, pb⟩ ← rb.toRat' dα
@@ -500,7 +500,7 @@ def evalMul.core {u : Level} {α : Q(Type u)} (e : Q(«$α»)) (f : Q(«$α» 
       (q(Eq.refl (Int.mul $na $nb)) : Expr)
     have t2 : Q(ℕ) := mkRawNatLit dd
     let r2 : Q(Nat.mul $da $db = Nat.mul $k $dc) := (q(Eq.refl $t2) : Expr)
-    return .isRat dα qc nc dc q(isRat_mul (f := $f) (.refl $f) $pa $pb $r1 $r2)
+    return .isRat dα qc nc dc q(isRat_mul (.refl _) $pa $pb $r1 $r2)
   match ra, rb with
   | .isBool .., _ | _, .isBool .. => failure
   | .isNegNNRat dα .., _ | _, .isNegNNRat dα .. =>
@@ -513,12 +513,12 @@ def evalMul.core {u : Level} {α : Q(Type u)} (e : Q(«$α»)) (f : Q(«$α» 
   | .isNNRat dsα .., _ | _, .isNNRat dsα .. =>
     nnratArm dsα
   | .isNegNat rα .., _ | _, .isNegNat rα .. => intArm rα
-  | .isNat mα' na pa, .isNat mα nb pb =>
+  | .isNat mα' na pa, .isNat mα nb pb => do
     haveI' : $mα =Q by clear! $mα $mα'; apply AddCommMonoidWithOne.toAddMonoidWithOne := ⟨⟩
     assumeInstancesCommute
     have c : Q(ℕ) := mkRawNatLit (na.natLit! * nb.natLit!)
     haveI' : Nat.mul $na $nb =Q $c := ⟨⟩
-    return .isNat mα c q(isNat_mul (f := $f) (.refl $f) $pa $pb (.refl $c))
+    return .isNat mα c q(isNat_mul (.refl _) $pa $pb (.refl $c))
 
 /-- The `norm_num` extension which identifies expressions of the form `a * b`,
 such that `norm_num` successfully recognises both `a` and `b`. -/
@@ -529,7 +529,7 @@ such that `norm_num` successfully recognises both `a` and `b`. -/
   guard <|← withNewMCtxDepth <| isDefEq f q(HMul.hMul (α := $α))
   haveI' : $f =Q HMul.hMul := ⟨⟩
   haveI' : $e =Q $a * $b := ⟨⟩
-  evalMul.core q($e) q($f) q($a) q($b) q($sα) ra rb
+  ra.mul rb
 
 theorem isNNRat_div {α : Type u} [DivisionSemiring α] : {a b : α} → {cn : ℕ} → {cd : ℕ} →
     IsNNRat (a * b⁻¹) cn cd → IsNNRat (a / b) cn cd
@@ -718,3 +718,5 @@ end NormNum
 end Meta
 
 end Mathlib
+
+open Mathlib.Meta.NormNum
diff --git a/Mathlib/Tactic/NormNum/BigOperators.lean b/Mathlib/Tactic/NormNum/BigOperators.lean
@@ -370,8 +370,7 @@ partial def evalFinsetProd : NormNumExt where eval {u β} e := do
 
   evalFinsetBigop q(Finset.prod) f res_empty (fun {a s' h} res_fa res_prod_s' ↦ do
       let fa : Q($β) := Expr.app f a
-      let res ← evalMul.core q($fa * Finset.prod $s' $f) q(HMul.hMul) _ _ instS res_fa
-        res_prod_s'
+      let res ← res_fa.mul res_prod_s'
       let eq : Q(Finset.prod (Finset.cons $a $s' $h) $f = $fa * Finset.prod $s' $f) :=
         q(Finset.prod_cons $h)
       pure <| res.eq_trans eq)
@@ -397,7 +396,7 @@ partial def evalFinsetSum : NormNumExt where eval {u β} e := do
 
   evalFinsetBigop q(Finset.sum) f res_empty (fun {a s' h} res_fa res_sum_s' ↦ do
       let fa : Q($β) := Expr.app f a
-      let res ← evalAdd.core q($fa + Finset.sum $s' $f) q(HAdd.hAdd) _ _ res_fa res_sum_s'
+      let res ← res_fa.add res_sum_s'
       let eq : Q(Finset.sum (Finset.cons $a $s' $h) $f = $fa + Finset.sum $s' $f) :=
         q(Finset.sum_cons $h)
       pure <| res.eq_trans eq)
diff --git a/Mathlib/Tactic/Ring/Basic.lean b/Mathlib/Tactic/Ring/Basic.lean
@@ -227,8 +227,6 @@ partial def ExSum.cast
 
 end
 
-variable {u : Lean.Level}
-
 /--
 The result of evaluating an (unnormalized) expression `e` into the type family `E`
 (one of `ExSum`, `ExProd`, `ExBase`) is a (normalized) element `e'`
@@ -246,7 +244,8 @@ instance {α : Q(Type u)} {E : Q($α) → Type} {e : Q($α)} [Inhabited (Σ e, E
     Inhabited (Result E e) :=
   let ⟨e', v⟩ : Σ e, E e := default; ⟨e', v, default⟩
 
-variable {α : Q(Type u)} (sα : Q(CommSemiring $α)) {R : Type*} [CommSemiring R]
+variable (sα)
+variable {R : Type*} [CommSemiring R]
 
 /--
 Constructs the expression corresponding to `.const n`.
@@ -337,7 +336,7 @@ def evalAddOverlap {a b : Q($α)} (va : ExProd sα a) (vb : ExProd sα b) :
   match va, vb with
   | .const za ha, .const zb hb => do
     let ra := Result.ofRawRat za a ha; let rb := Result.ofRawRat zb b hb
-    let res ← NormNum.evalAdd.core q($a + $b) q(HAdd.hAdd) a b ra rb
+    let res ← ra.add rb
     match res with
     | .isNat _ (.lit (.natVal 0)) p => pure <| .zero p
     | rc =>
@@ -436,7 +435,7 @@ partial def evalMulProd {a b : Q($α)} (va : ExProd sα a) (vb : ExProd sα b) :
       return ⟨a, .const za ha, (q(mul_one $a) : Expr)⟩
     else
       let ra := Result.ofRawRat za a ha; let rb := Result.ofRawRat zb b hb
-      let rc ← NormNum.evalMul.core q($a * $b) q(HMul.hMul) _ _ q(CommSemiring.toSemiring) ra rb
+      let rc ← ra.mul rb
       let ⟨zc, hc⟩ := rc.toRatNZ.get!
       let ⟨c, pc⟩ := rc.toRawEq
       return ⟨c, .const zc hc, pc⟩
@@ -597,13 +596,14 @@ def evalNegProd {a : Q($α)} (rα : Q(Ring $α)) (va : ExProd sα a) :
   match va with
   | .const za ha =>
     let ⟨m1, _⟩ := ExProd.mkNegNat sα rα 1
-    let rm := Result.isNegNat rα q(nat_lit 1) (q(IsInt.of_raw $α (.negOfNat (nat_lit 1))) : Expr)
+    let rm := Result.isNegNat rα q(nat_lit 1) q(IsInt.of_raw $α (.negOfNat (nat_lit 1)))
     let ra := Result.ofRawRat za a ha
-    let rb ← NormNum.evalMul.core q($m1 * $a) q(HMul.hMul) _ _
-      q(CommSemiring.toSemiring) rm ra
+    let rb ← rm.mul ra
     let ⟨zb, hb⟩ := rb.toRatNZ.get!
-    let ⟨b, (pb : Q((Int.negOfNat (nat_lit 1)).rawCast * $a = $b))⟩ := rb.toRawEq
-    return ⟨b, .const zb hb, (q(neg_one_mul (R := $α) $pb) : Expr)⟩
+    let ⟨b, pb⟩ := rb.toRawEq
+    -- Qq is probably unhappy about `Ring` and `CommSemiring` at the same time.
+    have pb : Q(((Int.negOfNat (nat_lit 1)).rawCast : $α) * $a = $b) := pb
+    return ⟨b, .const zb hb, q(neg_one_mul (R := $α) $pb)⟩
   | .mul (x := a₁) (e := a₂) va₁ va₂ va₃ =>
     let ⟨_, vb, pb⟩ ← evalNegProd rα va₃
     return ⟨_, .mul va₁ va₂ vb, (q(neg_mul $a₁ $a₂ $pb) : Expr)⟩
diff --git a/scripts/nolints.json b/scripts/nolints.json
@@ -314,14 +314,14 @@
  ["docBlame", "Mathlib.Tactic.GCongr.ForwardExt.eval"],
  ["docBlame", "Mathlib.Tactic.Monotonicity.mono.side"],
  ["docBlame", "Mathlib.Tactic.Sat.buildReify.mkPS"],
- ["docBlame", "Mathlib.Meta.NormNum.evalAdd.core.intArm"],
- ["docBlame", "Mathlib.Meta.NormNum.evalAdd.core.nnratArm"],
- ["docBlame", "Mathlib.Meta.NormNum.evalAdd.core.ratArm"],
+ ["docBlame", "Mathlib.Meta.NormNum.Result.add.intArm"],
+ ["docBlame", "Mathlib.Meta.NormNum.Result.add.nnratArm"],
+ ["docBlame", "Mathlib.Meta.NormNum.Result.add.ratArm"],
  ["docBlame", "Mathlib.Meta.NormNum.evalLE.core.intArm"],
  ["docBlame", "Mathlib.Meta.NormNum.evalLE.core.ratArm"],
  ["docBlame", "Mathlib.Meta.NormNum.evalLT.core.intArm"],
  ["docBlame", "Mathlib.Meta.NormNum.evalLT.core.nnratArm"],
  ["docBlame", "Mathlib.Meta.NormNum.evalLT.core.ratArm"],
- ["docBlame", "Mathlib.Meta.NormNum.evalMul.core.intArm"],
- ["docBlame", "Mathlib.Meta.NormNum.evalMul.core.nnratArm"],
- ["docBlame", "Mathlib.Meta.NormNum.evalMul.core.ratArm"]]
+ ["docBlame", "Mathlib.Meta.NormNum.Result.mul.intArm"],
+ ["docBlame", "Mathlib.Meta.NormNum.Result.mul.nnratArm"],
+ ["docBlame", "Mathlib.Meta.NormNum.Result.mul.ratArm"]]
