-- Mathlib/RingTheory/Spectrum/Prime/RingHom.lean
theorem image_specComap_zeroLocus_eq_zeroLocus_comap (hf : Surjective f) (I : Ideal S) :
    f.specComap '' zeroLocus I = zeroLocus (I.comap f)

Proof state:
case refine_1
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
⊢ (∃ x, I ≤ x.asIdeal ∧ f.specComap x = p) → Ideal.comap f I ≤ p.asIdeal

Tactic:
rintro ⟨p, hp, rfl⟩ a ha

Result:
case refine_1.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum S
hp : I ≤ p.asIdeal
a : R
ha : a ∈ Ideal.comap f I
⊢ a ∈ (f.specComap p).asIdeal

Proof state:
case refine_2.refine_2.asIdeal.h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : R
⊢ (∃ x_1 ∈ p.asIdeal, f x_1 = f x) ↔ x ∈ p.asIdeal

Tactic:
refine ⟨?_, fun hx => ⟨x, hx, rfl⟩⟩

Result:
case refine_2.refine_2.asIdeal.h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : R
⊢ (∃ x_1 ∈ p.asIdeal, f x_1 = f x) → x ∈ p.asIdeal

Proof state:
case refine_1.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum S
hp : I ≤ p.asIdeal
a : R
ha : a ∈ Ideal.comap f I
⊢ a ∈ (f.specComap p).asIdeal

Tactic:
exact hp ha

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
⊢ f.specComap '' zeroLocus ↑I = zeroLocus ↑(Ideal.comap f I)

Tactic:
simp only [Set.ext_iff, Set.mem_image, mem_zeroLocus, SetLike.coe_subset_coe]

Result:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
⊢ ∀ (x : PrimeSpectrum R), (∃ x_1, I ≤ x_1.asIdeal ∧ f.specComap x_1 = x) ↔ Ideal.comap f I ≤ x.asIdeal

Proof state:
case refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
⊢ ∃ x, I ≤ x.asIdeal ∧ f.specComap x = p

Tactic:
have hp : ker f ≤ p.asIdeal := (Ideal.comap_mono bot_le).trans h_I_p

Result:
case refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
⊢ ∃ x, I ≤ x.asIdeal ∧ f.specComap x = p

Proof state:
case refine_2.refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
⊢ f.specComap { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ } = p

Tactic:
ext x

Result:
case refine_2.refine_2.asIdeal.h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : R
⊢ x ∈ (f.specComap { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ }).asIdeal ↔ x ∈ p.asIdeal

Proof state:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
⊢ ∀ (x : PrimeSpectrum R), (∃ x_1, I ≤ x_1.asIdeal ∧ f.specComap x_1 = x) ↔ Ideal.comap f I ≤ x.asIdeal

Tactic:
refine fun p => ⟨?_, fun h_I_p => ?_⟩

Result:
case refine_1
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
⊢ (∃ x, I ≤ x.asIdeal ∧ f.specComap x = p) → Ideal.comap f I ≤ p.asIdeal

case refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
⊢ ∃ x, I ≤ x.asIdeal ∧ f.specComap x = p

Proof state:
case refine_2.refine_2.asIdeal.h.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : f x' = f x
⊢ x' - (x' - x) ∈ p.asIdeal

Tactic:
refine p.asIdeal.sub_mem hx' (hp ?_)

Result:
case refine_2.refine_2.asIdeal.h.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : f x' = f x
⊢ x' - x ∈ ker f

Proof state:
case refine_2.refine_1
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : S
hx : x ∈ I
⊢ x ∈ { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ }.asIdeal

Tactic:
obtain ⟨x', rfl⟩ := hf x

Result:
case refine_2.refine_1.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x' : R
hx : f x' ∈ I
⊢ f x' ∈ { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ }.asIdeal

Proof state:
case refine_2.refine_1.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x' : R
hx : f x' ∈ I
⊢ f x' ∈ { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ }.asIdeal

Tactic:
exact Ideal.mem_map_of_mem f (h_I_p hx)

Result:
no goals

Proof state:
case refine_2.refine_2.asIdeal.h.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : f x' = f x
⊢ x' - x ∈ ker f

Tactic:
rwa [mem_ker, map_sub, sub_eq_zero]

Result:
no goals

Proof state:
case refine_2.refine_2.asIdeal.h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : R
⊢ x ∈ (f.specComap { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ }).asIdeal ↔ x ∈ p.asIdeal

Tactic:
rw [specComap_asIdeal, Ideal.mem_comap, Ideal.mem_map_iff_of_surjective f hf]

Result:
case refine_2.refine_2.asIdeal.h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : R
⊢ (∃ x_1 ∈ p.asIdeal, f x_1 = f x) ↔ x ∈ p.asIdeal

Proof state:
case refine_2.refine_2.asIdeal.h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : R
⊢ (∃ x_1 ∈ p.asIdeal, f x_1 = f x) → x ∈ p.asIdeal

Tactic:
rintro ⟨x', hx', heq⟩

Result:
case refine_2.refine_2.asIdeal.h.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : f x' = f x
⊢ x ∈ p.asIdeal

Proof state:
case refine_2.refine_2.asIdeal.h.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : f x' = f x
⊢ x ∈ p.asIdeal

Tactic:
rw [← sub_sub_cancel x' x]

Result:
case refine_2.refine_2.asIdeal.h.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : f x' = f x
⊢ x' - (x' - x) ∈ p.asIdeal