∀ {R : Type u} [inst : CommRing R] (f : R) (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (hu : U ≤ PrimeSpectrum.basicOpen f), AlgebraicGeometry.StructureSheaf.const f f U hu = 1