case h
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
⊢ x ∈ imageOfDf f ↔ x ∈ ↑(PrimeSpectrum.comap C) '' zeroLocus {f}ᶜ
R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ imageOfDf f = ↑(PrimeSpectrum.comap C) '' zeroLocus {f}ᶜ
ext x
case h.refine'_1
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
hx : x ∈ imageOfDf f
⊢ { asIdeal := Ideal.map C x.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map C x.asIdeal)) } ∈ zeroLocus {f}ᶜ

case h.refine'_2
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
hx : x ∈ imageOfDf f
⊢ ↑(PrimeSpectrum.comap C)
      { asIdeal := Ideal.map C x.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map C x.asIdeal)) } =
    x

case h.refine'_3
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
⊢ x ∈ ↑(PrimeSpectrum.comap C) '' zeroLocus {f}ᶜ → x ∈ imageOfDf f
case h
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
⊢ x ∈ imageOfDf f ↔ x ∈ ↑(PrimeSpectrum.comap C) '' zeroLocus {f}ᶜ
refine' ⟨fun hx => ⟨⟨map C x.asIdeal, isPrime_map_C_of_isPrime x.IsPrime⟩, ⟨_, _⟩⟩, _⟩
case h.refine'_1
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
hx : x ∈ imageOfDf f
⊢ ¬f ∈ ↑{ asIdeal := Ideal.map C x.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map C x.asIdeal)) }.asIdeal
case h.refine'_1
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
hx : x ∈ imageOfDf f
⊢ { asIdeal := Ideal.map C x.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map C x.asIdeal)) } ∈ zeroLocus {f}ᶜ
rw [mem_compl_iff, mem_zeroLocus, singleton_subset_iff]
case h.refine'_1.intro
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
i : ℕ
hi : ¬coeff f i ∈ x.asIdeal
⊢ ¬f ∈ ↑{ asIdeal := Ideal.map C x.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map C x.asIdeal)) }.asIdeal
case h.refine'_1
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
hx : x ∈ imageOfDf f
⊢ ¬f ∈ ↑{ asIdeal := Ideal.map C x.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map C x.asIdeal)) }.asIdeal
cases' hx with i hi
no goals
case h.refine'_1.intro
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
i : ℕ
hi : ¬coeff f i ∈ x.asIdeal
⊢ ¬f ∈ ↑{ asIdeal := Ideal.map C x.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map C x.asIdeal)) }.asIdeal
exact fun a => hi (mem_map_C_iff.mp a i)
case h.refine'_2.asIdeal.h
R : Type u_1
inst✝ : CommRing R
f : R[X]
x✝ : PrimeSpectrum R
hx : x✝ ∈ imageOfDf f
x : R
⊢ x ∈
      (↑(PrimeSpectrum.comap C)
          { asIdeal := Ideal.map C x✝.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map C x✝.asIdeal)) }).asIdeal ↔
    x ∈ x✝.asIdeal
case h.refine'_2
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
hx : x ∈ imageOfDf f
⊢ ↑(PrimeSpectrum.comap C)
      { asIdeal := Ideal.map C x.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map C x.asIdeal)) } =
    x
ext x
case h.refine'_2.asIdeal.h
R : Type u_1
inst✝ : CommRing R
f : R[X]
x✝ : PrimeSpectrum R
hx : x✝ ∈ imageOfDf f
x : R
h :
  x ∈
    (↑(PrimeSpectrum.comap C)
        { asIdeal := Ideal.map C x✝.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map C x✝.asIdeal)) }).asIdeal
⊢ x ∈ x✝.asIdeal
case h.refine'_2.asIdeal.h
R : Type u_1
inst✝ : CommRing R
f : R[X]
x✝ : PrimeSpectrum R
hx : x✝ ∈ imageOfDf f
x : R
⊢ x ∈
      (↑(PrimeSpectrum.comap C)
          { asIdeal := Ideal.map C x✝.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map C x✝.asIdeal)) }).asIdeal ↔
    x ∈ x✝.asIdeal
refine' ⟨fun h => _, fun h => subset_span (mem_image_of_mem C.1 h)⟩
case h.refine'_2.asIdeal.h
R : Type u_1
inst✝ : CommRing R
f : R[X]
x✝ : PrimeSpectrum R
hx : x✝ ∈ imageOfDf f
x : R
h :
  x ∈
    (↑(PrimeSpectrum.comap C)
        { asIdeal := Ideal.map C x✝.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map C x✝.asIdeal)) }).asIdeal
⊢ coeff (↑C x) 0 ∈ x✝.asIdeal
case h.refine'_2.asIdeal.h
R : Type u_1
inst✝ : CommRing R
f : R[X]
x✝ : PrimeSpectrum R
hx : x✝ ∈ imageOfDf f
x : R
h :
  x ∈
    (↑(PrimeSpectrum.comap C)
        { asIdeal := Ideal.map C x✝.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map C x✝.asIdeal)) }).asIdeal
⊢ x ∈ x✝.asIdeal
rw [← @coeff_C_zero R x _]
no goals
case h.refine'_2.asIdeal.h
R : Type u_1
inst✝ : CommRing R
f : R[X]
x✝ : PrimeSpectrum R
hx : x✝ ∈ imageOfDf f
x : R
h :
  x ∈
    (↑(PrimeSpectrum.comap C)
        { asIdeal := Ideal.map C x✝.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map C x✝.asIdeal)) }).asIdeal
⊢ coeff (↑C x) 0 ∈ x✝.asIdeal
exact mem_map_C_iff.mp h 0
case h.refine'_3.intro.intro
R : Type u_1
inst✝ : CommRing R
f : R[X]
xli : PrimeSpectrum R[X]
complement : xli ∈ zeroLocus {f}ᶜ
⊢ ↑(PrimeSpectrum.comap C) xli ∈ imageOfDf f
case h.refine'_3
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
⊢ x ∈ ↑(PrimeSpectrum.comap C) '' zeroLocus {f}ᶜ → x ∈ imageOfDf f
rintro ⟨xli, complement, rfl⟩
no goals
case h.refine'_3.intro.intro
R : Type u_1
inst✝ : CommRing R
f : R[X]
xli : PrimeSpectrum R[X]
complement : xli ∈ zeroLocus {f}ᶜ
⊢ ↑(PrimeSpectrum.comap C) xli ∈ imageOfDf f
exact comap_C_mem_imageOfDf complement