∀ {R S : CommRingCat} [inst : Algebra ↑R ↑S] (A : CategoryTheory.Under R) {Z : CommRingCat}
  (h : (S.mkUnder (TensorProduct ↑R ↑S ↑A.right)).right ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl A.hom (CommRingCat.ofHom (algebraMap ↑R ↑S)))
      (CategoryTheory.CategoryStruct.comp (CommRingCat.tensorProdObjIsoPushoutObj S A).inv.right h) =
    CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom Algebra.TensorProduct.includeRight.toRingHom) h