∀ {R : Type u_1} (A : Type u_1) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)),
  1 ∈ (AlgebraicGeometry.StructureSheaf.sectionsSubmodule A U).carrier