[Merged by Bors] - feat(algebraic_geometry/prime_spectrum): add lemma zero_locus_bUnion

[adomani]

Add a simple extension of a lemma, to be able to work with bUnion, instead of only Union.

---

[jcommelin]

bors merge

[eric-wieser]

Turns out this can actually just be proved with

def zero_locus_bUnion (s : set (set R)) :
  zero_locus (⋃ s' ∈ s, s' : set R) = ⋂ s' ∈ s, zero_locus s' :=
by simp only [zero_locus_Union]

since bUnion is just two nested Unions

[jcommelin]

bors r-

[bors]

Canceled.

[jcommelin]

bors r+

[adomani]

I do not entirely understand how the proof works, but I am happy that this is going through!

Thank you very much, @eric-wieser and @jcommelin !

[eric-wieser]

I do not entirely understand how the proof works,

Try using simp_rw [zero_locus_Union, zero_locus_Union] so you can see the intermediate goal state. It's just rewriting the two binders (s' : set R) (hs : s' ∈ s) separately.

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests