∀ {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ { carrier := ↥X, str := X.instTopologicalSpaceCarrierCarrier }}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f))
  (x : ↥(AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme X (X.ofRestrict h))),
  IsLocalRing ↑((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme X (X.ofRestrict h)).presheaf.stalk x)