∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  CategoryTheory.Limits.pullback.diagonal (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S))) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom))
      (AlgebraicGeometry.pullbackSpecIso R S S).inv