Commit 2026-03-29 15:39 5ee50502

fix(Tactic/NormNum): do not re-enter simp from the very outside (#36841) This fixes a recursion error in

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:

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