perf(to_additive): hard code OfNat and OfNat.ofNat for numeral translation (leanprover-community#34696)

This PR removes the environment extension used by `to_additive` to determine which numerals to translate. The only two entries in this environment extension are `OfNat` and `OfNat.ofNat`, and I don't see why this would change.

See [#mathlib4 > Performance cost of environment extensions](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Performance.20cost.20of.20environment.20extensions/with/571319366)

Author: JovanGerb

Mathlib/Tactic/ToAdditive.lean

@@ -18,8 +18,6 @@ set_option linter.privateModule false
 attribute [to_additive_do_translate] Empty PEmpty Unit PUnit
 attribute [to_additive_ignore_args 2] Subtype
 
-attribute [translate_change_numeral 2] OfNat OfNat.ofNat
-
 attribute [to_additive] One
 attribute [to_additive existing Zero.toOfNat0] One.toOfNat1
 attribute [to_additive existing Zero.ofOfNat0] One.ofOfNat1

Mathlib/Tactic/Translate/Core.lean

@@ -108,21 +108,6 @@ syntax attrArgs :=
 -- We omit a doc-string on these syntaxes to instead show the `to_additive` or `to_dual` doc-string
 attribute [nolint docBlame] attrArgs bracketedOption
 
-/-- An attribute that stores all the declarations that deal with numeric literals on variable types.
-
-Numeral literals occur in expressions without type information, so in order to decide whether `1`
-needs to be changed to `0`, the context around the numeral is relevant.
-Most numerals will be in an `OfNat.ofNat` application, though tactics can add numeral literals
-inside arbitrary functions. By default we assume that we do not change numerals, unless it is
-in a function application with the `translate_change_numeral` attribute.
-
-`@[translate_change_numeral n₁ ...]` should be added to all functions that take one or more
-numerals as argument that should be changed if `shouldTranslate` succeeds on the first argument,
-i.e. when the numeral is only translated if the first argument is a variable
-(or consists of variables).
-The arguments `n₁ ...` are the positions of the numeral arguments (starting counting from 1). -/
-syntax (name := translate_change_numeral) "translate_change_numeral" (ppSpace num)* : attr
-
 initialize registerTraceClass `translate
 initialize registerTraceClass `translate_detail
 
@@ -164,17 +149,6 @@ register_option linter.translateRedundant : Bool := {
   defValue := true
   descr := "Linter used by translate attributes that checks if the attribute is redundant" }
 
-@[inherit_doc translate_change_numeral]
-initialize changeNumeralAttr : NameMapExtension (List Nat) ←
-  registerNameMapAttribute {
-    name := `translate_change_numeral
-    descr :=
-      "Auxiliary attribute for `to_additive` that stores functions that have numerals as argument."
-    add := fun
-    | _, `(attr| translate_change_numeral $[$arg]*) =>
-      pure <| arg.map (·.1.isNatLit?.get!.pred) |>.toList
-    | _, _ => throwUnsupportedSyntax }
-
 /-- `ArgInfo` stores information about how a constant should be translated. -/
 structure ArgInfo where
   /-- The arguments that should be reordered when translating, using cycle notation. -/
@@ -428,18 +402,17 @@ where
         mkAppN (.app (mkAppN (.const projName bf.constLevels!) bargs) b) args
     | .const n₀ ls₀ =>
       withTraceNode `translate_detail (fun res => return m!"{exceptEmoji res} replacing at {e}") do
-      -- Replace numeral `1` with `0` when required
-      if t.changeNumeral then
-        if let some numeralArgs := changeNumeralAttr.find? env n₀ then
-          if let some firstArg := args[0]? then
-            if shouldTranslate env t firstArg dontTranslate |>.isNone then
-              -- In this case, we still update all arguments of `g` that are not numerals,
-              -- since all other arguments can contain subexpressions like
-              -- `(fun x ↦ ℕ) (1 : G)`, and we have to update the `(1 : G)` to `(0 : G)`
-              trace[translate_detail] "applyReplacementFun: We change the numerals in this \
-                  expression. However, we will still recurse into all the non-numeral arguments."
-              let args := numeralArgs.foldl (·.modify · changeNumeral) args
-              return mkAppN f (← args.mapM visit)
+      -- Replace numeral `1` with `0` in applications of `OfNat` and `OfNat.ofNat`.
+      if t.changeNumeral && n₀ matches ``OfNat | ``OfNat.ofNat then
+        if let some firstArg := args[0]? then
+          if shouldTranslate env t firstArg dontTranslate |>.isNone then
+            -- In this case, we still update all arguments of `g` that are not numerals,
+            -- since all other arguments can contain subexpressions like
+            -- `(fun x ↦ ℕ) (1 : G)`, and we have to update the `(1 : G)` to `(0 : G)`
+            trace[translate_detail] "applyReplacementFun: We change the numerals in this \
+                expression. However, we will still recurse into all the non-numeral arguments."
+            let args := args.modify 1 changeNumeral
+            return mkAppN f (← args.mapM visit)
       let some n₁ := findTranslation? env t n₀ <|> do
         let n₁ := findPrefixTranslation env n₀ t
         guard (n₀ != n₁ && (isReservedName env n₁ || env.contains n₁)); some n₁