help welcome: #9993 build failure in PrimeSpectrum/Basic

Stream: mathlib4

[Michael Rothgang]

In #9993 (re-using some variables in Topology/Basic), I'm getting a build failure in PrimeSpectrum/Basic which I'm stuck on. Help by an algebraic geometry expert is welcome. You can see the PR for typical fixes: often, it's switching argument order or removing an underscore which is no longer necessary.

[Ruben Van de Velde]

error: tactic 'rewrite' failed, failed to assign synthesized instance

[Michael Rothgang]

The PR builds except for this one error (tested locally).

[Sébastien Gouëzel]

fixed.

[Sébastien Gouëzel]

But to me it looks like an indication that the previous version worked better.

[Kevin Buzzard]

great to see Sebastien is now an algebraic geometry expert!

[Michael Rothgang]

Thanks for the quick fix. I have restored the one affected lemma, so the original proof works.