∀ {R : Type u_1} [inst : CommRing R] (X Y : AlgCat R),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)) X Y)
      ((CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)).map (β_ X Y).hom) =
    CategoryTheory.CategoryStruct.comp
      (β_ ((CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)).obj X)
          ((CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)).obj Y)).hom
      (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)) Y X)