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) =
    (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.map (α_ m₁ m₂ m₃).inv).app X ≫ (MonoidalFunctor.μIso F (m₁ ⊗ m₂) m₃).inv.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₃).app ((F.obj m₁).obj X) ≫
      (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (m₂ ⊗ m₃)).app X ≫
        (F.map (α_ m₁ m₂ m₃).inv).app X ≫ (MonoidalFunctor.μIso F (m₁ ⊗ m₂) m₃).inv.app X
rw [← associativity_app_assoc]
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) =
    (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.map (α_ m₁ m₂ m₃).inv).app X ≫ (MonoidalFunctor.μIso F (m₁ ⊗ m₂) m₃).inv.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) =
    (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.map (α_ m₁ m₂ m₃).inv).app X ≫ (MonoidalFunctor.μIso F (m₁ ⊗ m₂) m₃).inv.app X
dsimp [endofunctorMonoidalCategory]
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) =
    (F.obj m₃).map ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂).app X) ≫ 𝟙 ((F.obj (m₁ ⊗ m₂) ⊗ F.obj m₃).obj 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) =
    (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.map (α_ m₁ m₂ m₃).inv).app X ≫ (MonoidalFunctor.μIso F (m₁ ⊗ m₂) m₃).inv.app X
simp
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) =
    (F.obj m₃).map ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂).app X) ≫
      𝟙 ((F.obj m₃).obj ((F.obj (m₁ ⊗ m₂)).obj 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) =
    (F.obj m₃).map ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂).app X) ≫ 𝟙 ((F.obj (m₁ ⊗ m₂) ⊗ F.obj m₃).obj X)
dsimp [endofunctorMonoidalCategory]
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
⊢ (F.obj m₃).map ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂).app X) =
    (F.obj m₃).map ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂).app X) ≫
      𝟙 ((F.obj m₃).obj ((F.obj (m₁ ⊗ m₂)).obj X))
simp