∀ (K : Type u_1) [inst : Field K] (X : AlgebraicGeometry.Scheme)
  (f : (x : ↥X) × (X.residueField x ⟶ { carrier := K, commRing := Field.toEuclideanDomain.toCommRing })),
  ⟨(CategoryTheory.ConcreteCategory.hom
            (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map f.snd) (X.fromSpecResidueField f.fst)).base)
          (IsLocalRing.closedPoint ↑{ carrier := K, commRing := Field.toEuclideanDomain.toCommRing }),
        AlgebraicGeometry.Scheme.descResidueField
          (AlgebraicGeometry.Scheme.stalkClosedPointTo
            (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map f.snd)
              (X.fromSpecResidueField f.fst)))⟩.fst =
    f.fst