feat: upstream helper functions for Name

src/Lean/Data/Name.lean

@@ -96,6 +96,12 @@ def quickCmp (n₁ n₂ : Name) : Ordering :=
 def quickLt (n₁ n₂ : Name) : Bool :=
   quickCmp n₁ n₂ == Ordering.lt
 
+/-- Returns true if the name has any numeric components. -/
+def hasNum : Name → Bool
+  | .anonymous => false
+  | .str p _ => p.hasNum
+  | .num _ _ => true
+
 /-- The frontend does not allow user declarations to start with `_` in any of its parts.
    We use name parts starting with `_` internally to create auxiliary names (e.g., `_private`). -/
 def isInternal : Name → Bool
@@ -103,6 +109,17 @@ def isInternal : Name → Bool
   | num p _ => isInternal p
   | _       => false
 
+/--
+The frontend does not allow user declarations to start with `_` in any of its parts.
+We use name parts starting with `_` internally to create auxiliary names (e.g., `_private`).
+
+This function checks if any component of the name starts with `_`, or is numeric.
+-/
+def isInternalOrNum : Name → Bool
+  | .str p s => s.get 0 == '_' || isInternalOrNum p
+  | .num _ _ => true
+  | _       => false
+
 /--
 Checks whether the name is an implementation-detail hypothesis name.