∀ {R : Type u_1} [inst : CommRing R] {A : Type u_1} [inst_1 : CommRing A] [inst_2 : Bialgebra R A],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CommAlgCat.ofHom (Bialgebra.comulAlgHom R A)).op
        (Opposite.op (CommAlgCat.of R A)))
      (CommAlgCat.ofHom (Bialgebra.comulAlgHom R A)).op =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (Opposite.op (CommAlgCat.of R A))
          (Opposite.op (CommAlgCat.of R A)) (Opposite.op (CommAlgCat.of R A))).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Opposite.op (CommAlgCat.of R A))
          (CommAlgCat.ofHom (Bialgebra.comulAlgHom R A)).op)
        (CommAlgCat.ofHom (Bialgebra.comulAlgHom R A)).op)