C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
⊢ (F.obj n).map ((MonoidalFunctor.εIso F).inv.app X ≫ F.ε.app X) =
    ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ M) n).app X ≫ (F.map (λ_ n).hom).app X) ≫
      (F.obj n).map (F.ε.app X)
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
⊢ (F.obj n).map ((MonoidalFunctor.εIso F).inv.app X) =
    (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ M) n).app X ≫ (F.map (λ_ n).hom).app X
rw [← cancel_mono ((F.obj n).map (F.ε.app X)), ← Functor.map_comp]
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
⊢ 𝟙 ((F.obj n).obj ((F.obj (𝟙_ M)).obj X)) = 𝟙 ((F.obj (𝟙_ M) ⊗ F.obj n).obj X)
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
⊢ (F.obj n).map ((MonoidalFunctor.εIso F).inv.app X ≫ F.ε.app X) =
    ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ M) n).app X ≫ (F.map (λ_ n).hom).app X) ≫
      (F.obj n).map (F.ε.app X)
simp
no goals
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
⊢ 𝟙 ((F.obj n).obj ((F.obj (𝟙_ M)).obj X)) = 𝟙 ((F.obj (𝟙_ M) ⊗ F.obj n).obj X)
rfl