case h.asIdeal.h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.132631
inst✝ : CommRing S'
f : R →+* S
a✝ : PrimeSpectrum R
x✝ : R
⊢ x✝ ∈ (↑(comap (RingHom.id R)) a✝).asIdeal ↔ x✝ ∈ (↑(ContinuousMap.id (PrimeSpectrum R)) a✝).asIdeal
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.132631
inst✝ : CommRing S'
f : R →+* S
⊢ comap (RingHom.id R) = ContinuousMap.id (PrimeSpectrum R)
ext
no goals
case h.asIdeal.h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.132631
inst✝ : CommRing S'
f : R →+* S
a✝ : PrimeSpectrum R
x✝ : R
⊢ x✝ ∈ (↑(comap (RingHom.id R)) a✝).asIdeal ↔ x✝ ∈ (↑(ContinuousMap.id (PrimeSpectrum R)) a✝).asIdeal
rfl