fix(Tactic/NormNum): do not re-enter simp from the very outside (#36841)

This fixes a recursion error in
```lean4
import Mathlib.SetTheory.Cardinal.Basic
import Mathlib.Tactic.NormNum.Core

theorem foos.{u} (α β : Type u) : Cardinal.mk α = Cardinal.mk β → α = β := by
  norm_num [Cardinal.mk_eq_aleph0]
```
which is quite willing to be promoted to a stack overflow with a moderate recursion depth limit.

It's not entirely clear to me if `dischargeGround` is the right discharger to use here, but no tests fail because of that choice.

Note this change breaks the following proof:
```lean4
import Mathlib.Tactic.NormNum

theorem foo (x y : ℚ)
    (h₀ : x > 0 ∧ y > 0)
    (h₁ : x < 1 ∧ y < 1) :
    0 ≤ x / (1 - x) + y / (1 - y) := by
  norm_num [*, div_pos, add_pos, le_of_lt]
```

The reason is that previously `norm_num` was `simp` plus _two_ things:
* Numeral normalization.
* Hackily overriding `maxDischargeDepth` to exceed maxRecDepth

Author: eric-wieser

Mathlib/Tactic/NormNum/Core.lean

@@ -215,27 +215,25 @@ def tryNormNum (post := false) (e : Expr) : SimpM Simp.Step := do
   catch _ =>
     return .continue
 
-variable (ctx : Simp.Context) (useSimp := true) in
-mutual
-  /-- A discharger which calls `norm_num`. -/
-  partial def discharge (e : Expr) : SimpM (Option Expr) := do (← deriveSimp e).ofTrue
-
-  /-- A `Methods` implementation which calls `norm_num`. -/
-  partial def methods : Simp.Methods :=
-    if useSimp then {
-      pre := Simp.preDefault #[] >> tryNormNum
-      post := Simp.postDefault #[] >> tryNormNum (post := true)
-      discharge? := discharge
-    } else {
-      pre := tryNormNum
-      post := tryNormNum (post := true)
-      discharge? := discharge
-    }
-
-  /-- Traverses the given expression using simp and normalises any numbers it finds. -/
-  partial def deriveSimp (e : Expr) : MetaM Simp.Result :=
-    (·.1) <$> Simp.main e ctx (methods := methods)
-end
+/-- A `Methods` implementation which calls `norm_num`. -/
+def methods (useSimp := true) : Simp.Methods :=
+  if useSimp then {
+    pre := Simp.preDefault #[] >> tryNormNum
+    post := Simp.postDefault #[] >> tryNormNum (post := true)
+    discharge? := Simp.dischargeGround
+  } else {
+    pre := tryNormNum
+    post := tryNormNum (post := true)
+    discharge? := Simp.dischargeGround
+  }
+
+/-- Traverses the given expression using simp and normalises any numbers it finds. -/
+def deriveSimp (ctx : Simp.Context) (useSimp := true) (e : Expr) : MetaM Simp.Result :=
+  (·.1) <$> Simp.main e ctx (methods := methods useSimp)
+
+/-- A discharger which calls `norm_num`, for use in downstream tactics populating `Simp.Methods`. -/
+def discharge (useSimp := true) (e : Expr) : SimpM (Option Expr) := do
+  (← deriveSimp (← readThe Simp.Context) useSimp e).ofTrue
 
 open Tactic in
 /-- Constructs a simp context from the simp argument syntax. -/

Mathlib/Tactic/ReduceModChar.lean

@@ -256,7 +256,7 @@ partial def derive (expensive := false) (e : Expr) : MetaM Simp.Result := do
   | none => throwError "internal error: reduce_mod_char not registered as simp extension"
   let ctx ← Simp.mkContext config (congrTheorems := congrTheorems)
     (simpTheorems := #[← ext.getTheorems])
-  let discharge := Mathlib.Meta.NormNum.discharge ctx
+  let discharge := Mathlib.Meta.NormNum.discharge
   let r : Simp.Result := {expr := e}
   let pre := Simp.preDefault #[] >> fun e =>
       try return (Simp.Step.done (← matchAndNorm (expensive := expensive) e))