R : Type u
inst✝ : CommRing R
x : ↑(PrimeSpectrum.Top R)
f : { x_1 // x_1 ∈ Ideal.primeCompl x.asIdeal }
⊢ IsUnit
    (↑(germ (Sheaf.presheaf (structureSheaf R)) { val := x, property := (_ : ↑f ∈ Ideal.primeCompl x.asIdeal) })
      (↑(toOpen R (PrimeSpectrum.basicOpen ↑f)) ↑f))
R : Type u
inst✝ : CommRing R
x : ↑(PrimeSpectrum.Top R)
f : { x_1 // x_1 ∈ Ideal.primeCompl x.asIdeal }
⊢ IsUnit (↑(toStalk R x) ↑f)
erw [← germ_toOpen R (PrimeSpectrum.basicOpen (f : R)) ⟨x, f.2⟩ (f : R)]
no goals
R : Type u
inst✝ : CommRing R
x : ↑(PrimeSpectrum.Top R)
f : { x_1 // x_1 ∈ Ideal.primeCompl x.asIdeal }
⊢ IsUnit
    (↑(germ (Sheaf.presheaf (structureSheaf R)) { val := x, property := (_ : ↑f ∈ Ideal.primeCompl x.asIdeal) })
      (↑(toOpen R (PrimeSpectrum.basicOpen ↑f)) ↑f))
exact RingHom.isUnit_map _ (isUnit_to_basicOpen_self R f)