grind/grobner regression in 4.33.0-rc1

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The code below works on 4.32.0, but fails in 4.33.0-rc1.

variable {F : Type} [Lean.Grind.Field F] (a₂ a₄ a₆ ℓ m x₁ x₂ x₃ : F)

theorem test (hne : x₁ ≠ x₂)
    (hx₃ : x₃ = ℓ ^ 2 - a₂ - x₁ - x₂)
    (h₁ : (ℓ * x₁ + m) ^ 2 = x₁ ^ 3 + a₂ * x₁ ^ 2 + a₄ * x₁ + a₆)
    (h₂ : (ℓ * x₂ + m) ^ 2 = x₂ ^ 3 + a₂ * x₂ ^ 2 + a₄ * x₂ + a₆) :
    x₁ * x₂ + x₁ * x₃ + x₂ * x₃ = a₄ - 2 * ℓ * m ∧
        x₁ * x₂ * x₃ = m ^ 2 - a₆ := by
  grobner

Context

Occurred in a project downstream of mathlib.

Note that by increasing the number of ringSteps, grobner/grind succeeds. Perhaps this suggests the default should have been adjusted when some recent change was made?

Steps to Reproduce

1. Code as above

Expected behavior: grobner closes the goal.

Actual behavior: grobner fails to close the goal.

Versions

Tested on live.lean-lang.org, comparing Latest Release (v4.33.0-rc1 with mathlib, cslib) against Stable Release (v4.32.0 with mathlib, cslib)

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.ecent chan

Start by running the minimal theorem on Lean 4.33.0-rc1 and 4.32.0 to confirm the regression. Investigate the grobner/grind behavior around the default ringSteps setting; done means the supplied goal closes on 4.33.0-rc1 without manually increasing ringSteps.