no goals
R : Type u
inst✝² : CommRing R
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
U : Opens ↑(PrimeSpectrum.Top R)
p : ↑(PrimeSpectrum.Top R)
hpU : p ∈ U.carrier
⊢ p ∈ ↑(PrimeSpectrum.comap (RingHom.id R)) ⁻¹' U.carrier
rwa [PrimeSpectrum.comap_id]
R : Type u
inst✝² : CommRing R
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
U : Opens ↑(PrimeSpectrum.Top R)
⊢ eqToHom (_ : (structureSheaf R).val.obj U.op = (structureSheaf R).val.obj U.op) =
    RingHom.id ↑((structureSheaf R).val.obj U.op)
R : Type u
inst✝² : CommRing R
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
U : Opens ↑(PrimeSpectrum.Top R)
⊢ comap (RingHom.id R) U U
      (_ : ∀ (p : ↑(PrimeSpectrum.Top R)), p ∈ U.carrier → p ∈ ↑(PrimeSpectrum.comap (RingHom.id R)) ⁻¹' U.carrier) =
    RingHom.id ↑((structureSheaf R).val.obj U.op)
rw [comap_id U U rfl]
no goals
R : Type u
inst✝² : CommRing R
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
U : Opens ↑(PrimeSpectrum.Top R)
⊢ eqToHom (_ : (structureSheaf R).val.obj U.op = (structureSheaf R).val.obj U.op) =
    RingHom.id ↑((structureSheaf R).val.obj U.op)
rfl