C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
this :
  ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂ ⊗ 𝟙 (F.obj m₃)) ≫
          LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃ ≫ F.map (α_ m₁ m₂ m₃).hom).app
      X =
    ((α_ (F.obj m₁) (F.obj m₂) (F.obj m₃)).hom ≫
          (𝟙 (F.obj m₁) ⊗ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₂ m₃) ≫
            LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (m₂ ⊗ m₃)).app
      X
⊢ (F.obj m₃).map ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂).app X) ≫
      (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃).app X ≫ (F.map (α_ m₁ m₂ m₃).hom).app X =
    (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₂ m₃).app ((F.obj m₁).obj X) ≫
      (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (m₂ ⊗ m₃)).app X
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ (F.obj m₃).map ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂).app X) ≫
      (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃).app X ≫ (F.map (α_ m₁ m₂ m₃).hom).app X =
    (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₂ m₃).app ((F.obj m₁).obj X) ≫
      (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (m₂ ⊗ m₃)).app X
have := congr_app (F.toLaxMonoidalFunctor.associativity m₁ m₂ m₃) X
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
this :
  (𝟙 ((F.obj m₃).obj ((F.obj m₂).obj ((F.obj m₁).obj X))) ≫
        (F.obj m₃).map ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂).app X)) ≫
      (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃).app X ≫ (F.map (α_ m₁ m₂ m₃).hom).app X =
    𝟙 ((F.obj m₃).obj ((F.obj m₂).obj ((F.obj m₁).obj X))) ≫
      ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₂ m₃).app ((F.obj m₁).obj X) ≫
          (F.obj (m₂ ⊗ m₃)).map (𝟙 ((F.obj m₁).obj X))) ≫
        (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (m₂ ⊗ m₃)).app X
⊢ (F.obj m₃).map ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂).app X) ≫
      (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃).app X ≫ (F.map (α_ m₁ m₂ m₃).hom).app X =
    (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₂ m₃).app ((F.obj m₁).obj X) ≫
      (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (m₂ ⊗ m₃)).app X
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
this :
  ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂ ⊗ 𝟙 (F.obj m₃)) ≫
          LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃ ≫ F.map (α_ m₁ m₂ m₃).hom).app
      X =
    ((α_ (F.obj m₁) (F.obj m₂) (F.obj m₃)).hom ≫
          (𝟙 (F.obj m₁) ⊗ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₂ m₃) ≫
            LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (m₂ ⊗ m₃)).app
      X
⊢ (F.obj m₃).map ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂).app X) ≫
      (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃).app X ≫ (F.map (α_ m₁ m₂ m₃).hom).app X =
    (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₂ m₃).app ((F.obj m₁).obj X) ≫
      (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (m₂ ⊗ m₃)).app X
dsimp [endofunctorMonoidalCategory] at this
no goals
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
this :
  (𝟙 ((F.obj m₃).obj ((F.obj m₂).obj ((F.obj m₁).obj X))) ≫
        (F.obj m₃).map ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂).app X)) ≫
      (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃).app X ≫ (F.map (α_ m₁ m₂ m₃).hom).app X =
    𝟙 ((F.obj m₃).obj ((F.obj m₂).obj ((F.obj m₁).obj X))) ≫
      ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₂ m₃).app ((F.obj m₁).obj X) ≫
          (F.obj (m₂ ⊗ m₃)).map (𝟙 ((F.obj m₁).obj X))) ≫
        (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (m₂ ⊗ m₃)).app X
⊢ (F.obj m₃).map ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂).app X) ≫
      (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃).app X ≫ (F.map (α_ m₁ m₂ m₃).hom).app X =
    (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₂ m₃).app ((F.obj m₁).obj X) ≫
      (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (m₂ ⊗ m₃)).app X
simpa using this