∀ {R : Type u_2} [inst : CommRing R] {J : Type u_4} [inst_1 : CategoryTheory.Category.{u_3, u_4} J]
  (F : CategoryTheory.Functor J (AlgCat R))
  [inst_2 : Small.{u_1, max u_4 u_1} ↑(F.comp (CategoryTheory.forget (AlgCat R))).sections]
  (s : CategoryTheory.Limits.Cone F) (x y : ↑s.1),
  EquivLike.coe (equivShrink ↑(F.comp (CategoryTheory.forget (AlgCat R))).sections)
      ⟨fun j => ((CategoryTheory.forget (AlgCat R)).mapCone s).π.app j (x * y), ⋯⟩ =
    EquivLike.coe (equivShrink ↑(F.comp (CategoryTheory.forget (AlgCat R))).sections)
        ⟨fun j => ((CategoryTheory.forget (AlgCat R)).mapCone s).π.app j x, ⋯⟩ *
      EquivLike.coe (equivShrink ↑(F.comp (CategoryTheory.forget (AlgCat R))).sections)
        ⟨fun j => ((CategoryTheory.forget (AlgCat R)).mapCone s).π.app j y, ⋯⟩