fix: beta reduction in grind must respect generation threshold

[leodemoura]

This PR fixes a bug in propagateBetaEqs (in Lean.Meta.Tactic.Grind.Beta)
where new equalities/terms introduced by beta reduction were added to the goal
without checking the generation threshold. The generation of the new fact
is the maximum generation of the lambda, the function f, and its
arguments, plus one. Without the threshold check, beta reduction can
cascade indefinitely on self-similar lambdas such as
(fun b => f (b + 1)) = fun b => f b, which kept producing
f n = f (n + 1) for every n. The fix aggregates argument generations
before the threshold check and bails out when the resulting generation
reaches maxGeneration.

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-04-24 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-04-28 22:29:35)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-13560 has successfully built against this PR. (2026-04-28 23:25:54) View Log