case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.109078
inst✝ : CommRing S'
f : R →+* S
s : Set R
x : PrimeSpectrum S
⊢ x ∈
      (fun y => { asIdeal := Ideal.comap f y.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.comap f y.asIdeal)) }) ⁻¹'
        zeroLocus s ↔
    x ∈ zeroLocus (↑f '' s)
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.109078
inst✝ : CommRing S'
f : R →+* S
s : Set R
⊢ (fun y => { asIdeal := Ideal.comap f y.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.comap f y.asIdeal)) }) ⁻¹'
      zeroLocus s =
    zeroLocus (↑f '' s)
ext x
case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.109078
inst✝ : CommRing S'
f : R →+* S
s : Set R
x : PrimeSpectrum S
⊢ x ∈
      (fun y => { asIdeal := Ideal.comap f y.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.comap f y.asIdeal)) }) ⁻¹'
        zeroLocus s ↔
    s ⊆ (fun a => ↑f a) ⁻¹' ↑x.asIdeal
case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.109078
inst✝ : CommRing S'
f : R →+* S
s : Set R
x : PrimeSpectrum S
⊢ x ∈
      (fun y => { asIdeal := Ideal.comap f y.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.comap f y.asIdeal)) }) ⁻¹'
        zeroLocus s ↔
    x ∈ zeroLocus (↑f '' s)
simp only [mem_zeroLocus, Set.image_subset_iff]
no goals
case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.109078
inst✝ : CommRing S'
f : R →+* S
s : Set R
x : PrimeSpectrum S
⊢ x ∈
      (fun y => { asIdeal := Ideal.comap f y.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.comap f y.asIdeal)) }) ⁻¹'
        zeroLocus s ↔
    s ⊆ (fun a => ↑f a) ⁻¹' ↑x.asIdeal
rfl