∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {W X Y Z : CategoryTheory.Monad C} (x : W ⟶ X)
  (x_1 : X ⟶ Y) (x_2 : Y ⟶ Z) (X_1 : C),
  CategoryTheory.CategoryStruct.comp (W.μ.app X_1)
      (CategoryTheory.CategoryStruct.comp
        ({ app := fun X_2 => CategoryTheory.CategoryStruct.comp (x.app X_2) (x_1.app X_2), naturality := ⋯, app_η := ⋯,
              app_μ := ⋯ }.app
          X_1)
        (x_2.app X_1)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        (W.map
          (CategoryTheory.CategoryStruct.comp
            ({ app := fun X_2 => CategoryTheory.CategoryStruct.comp (x.app X_2) (x_1.app X_2), naturality := ⋯,
                  app_η := ⋯, app_μ := ⋯ }.app
              X_1)
            (x_2.app X_1)))
        (CategoryTheory.CategoryStruct.comp
          ({ app := fun X_2 => CategoryTheory.CategoryStruct.comp (x.app X_2) (x_1.app X_2), naturality := ⋯,
                app_η := ⋯, app_μ := ⋯ }.app
            (Z.obj X_1))
          (x_2.app (Z.obj X_1))))
      (Z.μ.app X_1)