∀ (K : Type u_1) [inst : Field K] (X : AlgebraicGeometry.Scheme)
  (f : (x : ↥X) × (X.residueField x ⟶ { carrier := K, commRing := Field.toEuclideanDomain.toCommRing })),
  IsLocalHom
    (CommRingCat.Hom.hom
      (AlgebraicGeometry.Scheme.stalkClosedPointTo
        (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map f.snd) (X.fromSpecResidueField f.fst))))