case intro
R : Type u_1
inst✝ : CommRing R
f : R[X]
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (↑(PrimeSpectrum.comap C) '' U)
R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ IsOpenMap ↑(PrimeSpectrum.comap C)
rintro U ⟨s, z⟩
case intro
R : Type u_1
inst✝ : CommRing R
f : R[X]
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (⋃ (i : ↑s), ↑(PrimeSpectrum.comap C) '' zeroLocus {↑i}ᶜ)
case intro
R : Type u_1
inst✝ : CommRing R
f : R[X]
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (↑(PrimeSpectrum.comap C) '' U)
rw [← compl_compl U, ← z, ← iUnion_of_singleton_coe s, zeroLocus_iUnion, compl_iInter,
  image_iUnion]
case intro
R : Type u_1
inst✝ : CommRing R
f : R[X]
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (⋃ (i : ↑s), imageOfDf ↑i)
case intro
R : Type u_1
inst✝ : CommRing R
f : R[X]
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (⋃ (i : ↑s), ↑(PrimeSpectrum.comap C) '' zeroLocus {↑i}ᶜ)
simp_rw [← imageOfDf_eq_comap_C_compl_zeroLocus]
no goals
case intro
R : Type u_1
inst✝ : CommRing R
f : R[X]
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (⋃ (i : ↑s), imageOfDf ↑i)
exact isOpen_iUnion fun f => isOpen_imageOfDf