-- Mathlib/RingTheory/Spectrum/Prime/IsOpenComapC.lean
theorem imageOfDf_eq_comap_C_compl_zeroLocus :
    imageOfDf f = PrimeSpectrum.comap (C : R →+* R[X]) '' (zeroLocus {f})ᶜ

Proof state:
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 := ⋯ } ∈ (zeroLocus {f})ᶜ

Tactic:
rw [mem_compl_iff, mem_zeroLocus, singleton_subset_iff]

Result:
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 := ⋯ }.asIdeal

Proof state:
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 := ⋯ }).asIdeal
⊢ x ∈ x✝.asIdeal

Tactic:
rw [← @coeff_C_zero R x _]

Result:
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 := ⋯ }).asIdeal
⊢ (C x).coeff 0 ∈ x✝.asIdeal

Proof state:
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 := ⋯ } = x

Tactic:
ext x

Result:
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 := ⋯ }).asIdeal ↔ x ∈ x✝.asIdeal

Proof state:
case h.refine_1.intro
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
i : ℕ
hi : f.coeff i ∉ x.asIdeal
⊢ f ∉ ↑{ asIdeal := Ideal.map C x.asIdeal, isPrime := ⋯ }.asIdeal

Tactic:
exact fun a => hi (mem_map_C_iff.mp a i)

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
⊢ x ∈ imageOfDf f ↔ x ∈ ⇑(PrimeSpectrum.comap C) '' (zeroLocus {f})ᶜ

Tactic:
refine ⟨fun hx => ⟨⟨map C x.asIdeal, isPrime_map_C_of_isPrime x.isPrime⟩, ⟨?_, ?_⟩⟩, ?_⟩

Result:
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 := ⋯ } ∈ (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 := ⋯ } = 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

Proof state:
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 := ⋯ }.asIdeal

Tactic:
obtain ⟨i, hi⟩ := hx

Result:
case h.refine_1.intro
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
i : ℕ
hi : f.coeff i ∉ x.asIdeal
⊢ f ∉ ↑{ asIdeal := Ideal.map C x.asIdeal, isPrime := ⋯ }.asIdeal

Proof state:
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

Tactic:
rintro ⟨xli, complement, rfl⟩

Result:
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

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ imageOfDf f = ⇑(PrimeSpectrum.comap C) '' (zeroLocus {f})ᶜ

Tactic:
ext x

Result:
case h
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
⊢ x ∈ imageOfDf f ↔ x ∈ ⇑(PrimeSpectrum.comap C) '' (zeroLocus {f})ᶜ

Proof state:
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 := ⋯ }).asIdeal ↔ x ∈ x✝.asIdeal

Tactic:
refine ⟨fun h => ?_, fun h => subset_span (mem_image_of_mem C.1 h)⟩

Result:
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 := ⋯ }).asIdeal
⊢ x ∈ x✝.asIdeal

Proof state:
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 := ⋯ }).asIdeal
⊢ (C x).coeff 0 ∈ x✝.asIdeal

Tactic:
exact mem_map_C_iff.mp h 0

Result:
no goals

Proof state:
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

Tactic:
exact comap_C_mem_imageOfDf complement

Result:
no goals