∀ (R : Type u_1) [inst : CommRing R] (x x_1 x_2 : HopfAlgCat R),
  (TensorProduct.mk R x.carrier x_1.carrier).compr₂ₛₗ
      ((TensorProduct.mk R (CategoryTheory.MonoidalCategoryStruct.tensorObj x x_1).carrier x_2.carrier).compr₂ₛₗ
        ((fun x_3 => ↑x_3)
          ((CategoryTheory.forget₂ (HopfAlgCat R) (BialgCat R)).map
              (CategoryTheory.MonoidalCategoryStruct.associator x x_1 x_2).hom).toBialgHom')) =
    (TensorProduct.mk R x.carrier x_1.carrier).compr₂ₛₗ
      ((TensorProduct.mk R (CategoryTheory.MonoidalCategoryStruct.tensorObj x x_1).carrier x_2.carrier).compr₂ₛₗ
        ((fun x_3 => ↑x_3)
          (((CategoryTheory.Iso.refl
                      (CategoryTheory.MonoidalCategoryStruct.tensorObj
                        ((CategoryTheory.forget₂ (HopfAlgCat R) (BialgCat R)).obj
                          (CategoryTheory.MonoidalCategoryStruct.tensorObj x x_1))
                        ((CategoryTheory.forget₂ (HopfAlgCat R) (BialgCat R)).obj x_2))).symm ≪≫
                  CategoryTheory.MonoidalCategory.tensorIso
                    (CategoryTheory.Iso.refl
                        (CategoryTheory.MonoidalCategoryStruct.tensorObj
                          ((CategoryTheory.forget₂ (HopfAlgCat R) (BialgCat R)).obj x)
                          ((CategoryTheory.forget₂ (HopfAlgCat R) (BialgCat R)).obj x_1))).symm
                    (CategoryTheory.Iso.refl ((CategoryTheory.forget₂ (HopfAlgCat R) (BialgCat R)).obj x_2))) ≪≫
                CategoryTheory.MonoidalCategoryStruct.associator
                    ((CategoryTheory.forget₂ (HopfAlgCat R) (BialgCat R)).obj x)
                    ((CategoryTheory.forget₂ (HopfAlgCat R) (BialgCat R)).obj x_1)
                    ((CategoryTheory.forget₂ (HopfAlgCat R) (BialgCat R)).obj x_2) ≪≫
                  CategoryTheory.MonoidalCategory.tensorIso
                      (CategoryTheory.Iso.refl ((CategoryTheory.forget₂ (HopfAlgCat R) (BialgCat R)).obj x))
                      (CategoryTheory.Iso.refl
                        (CategoryTheory.MonoidalCategoryStruct.tensorObj
                          ((CategoryTheory.forget₂ (HopfAlgCat R) (BialgCat R)).obj x_1)
                          ((CategoryTheory.forget₂ (HopfAlgCat R) (BialgCat R)).obj x_2))) ≪≫
                    CategoryTheory.Iso.refl
                      (CategoryTheory.MonoidalCategoryStruct.tensorObj
                        ((CategoryTheory.forget₂ (HopfAlgCat R) (BialgCat R)).obj x)
                        ((CategoryTheory.forget₂ (HopfAlgCat R) (BialgCat R)).obj
                          (CategoryTheory.MonoidalCategoryStruct.tensorObj x_1 x_2)))).hom.toBialgHom'))