∀ (R S : Type u_1) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : PrimeSpectrum R),
  CategoryTheory.IsIso
    (CategoryTheory.Limits.pullback.map
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Spec.map
          (AlgebraicGeometry.Scheme.Spec.residueFieldIso { carrier := R, commRing := inst } p).inv)
        (AlgebraicGeometry.Spec.map
          (CommRingCat.ofHom (algebraMap (↑{ carrier := R, commRing := inst }) p.asIdeal.ResidueField))))
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R p.asIdeal.ResidueField)))
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))
      (AlgebraicGeometry.Spec.map
        (AlgebraicGeometry.Scheme.Spec.residueFieldIso { carrier := R, commRing := inst } p).inv)
      (CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec { carrier := S, commRing := inst_1 }))
      (CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec { carrier := R, commRing := inst })) ⋯ ⋯)