∀ {R : Type u_1} [inst : CommRing R] (x x_1 x_2 : AlgCat R),
  (CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)).map
      (CategoryTheory.MonoidalCategoryStruct.associator x x_1 x_2).hom =
    (((CategoryTheory.Iso.refl
              (CategoryTheory.MonoidalCategoryStruct.tensorObj
                ((CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)).obj
                  (CategoryTheory.MonoidalCategoryStruct.tensorObj x x_1))
                ((CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)).obj x_2))).symm ≪≫
          CategoryTheory.MonoidalCategory.tensorIso
            (CategoryTheory.Iso.refl
                (CategoryTheory.MonoidalCategoryStruct.tensorObj
                  ((CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)).obj x)
                  ((CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)).obj x_1))).symm
            (CategoryTheory.Iso.refl ((CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)).obj x_2))) ≪≫
        CategoryTheory.MonoidalCategoryStruct.associator ((CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)).obj x)
            ((CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)).obj x_1)
            ((CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)).obj x_2) ≪≫
          CategoryTheory.MonoidalCategory.tensorIso
              (CategoryTheory.Iso.refl ((CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)).obj x))
              (CategoryTheory.Iso.refl
                (CategoryTheory.MonoidalCategoryStruct.tensorObj
                  ((CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)).obj x_1)
                  ((CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)).obj x_2))) ≪≫
            CategoryTheory.Iso.refl
              (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)).obj x)
                ((CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)).obj
                  (CategoryTheory.MonoidalCategoryStruct.tensorObj x_1 x_2)))).hom