Nsatz-like tactic

Stream: Is there code for X?

[Bolton Bailey]

In the course of my project I have reached a point where I have a goal and a collection of equations that take the form of equations of polynomials over an integral domain. After searching a bit I found Nsatz, a Coq tactic that seems to do this sort of thing. I am not too familiar with the Nullstellensatz, but I see there is a file on it in mathlib. Does something like the Nsatz tactic exist for Lean? Does anyone have thoughts on how easily this algorithm could be implemented based on what already does exist?

[Adam Topaz]

Looking briefly at the link you sent, it seems this tactic does a Gröbner basis calculation. Unfortunately we don't have such a tactic as far as I know.

[Kevin Buzzard]

MS have got their eye on adding this in Lean 4 but we're unlikely to get it in Lean 3