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
this :
  (ρ_ (F.obj n)).hom.app X =
    ((𝟙 (F.obj n) ⊗ F.ε) ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor n (𝟙_ M) ≫ F.map (ρ_ n).hom).app X
⊢ F.ε.app ((F.obj n).obj X) ≫ (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor n (𝟙_ M)).app X ≫ (F.map (ρ_ n).hom).app X =
    𝟙 ((𝟙_ (C ⥤ C)).obj ((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.ε.app ((F.obj n).obj X) ≫ (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor n (𝟙_ M)).app X ≫ (F.map (ρ_ n).hom).app X =
    𝟙 ((𝟙_ (C ⥤ C)).obj ((F.obj n).obj X))
have := congr_app (F.toLaxMonoidalFunctor.right_unitality n) 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
this :
  𝟙 ((F.obj n).obj X) =
    (F.ε.app ((F.obj n).obj X) ≫ (F.obj (𝟙_ M)).map (𝟙 ((F.obj n).obj X))) ≫
      (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor n (𝟙_ M)).app X ≫ (F.map (ρ_ n).hom).app X
⊢ F.ε.app ((F.obj n).obj X) ≫ (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor n (𝟙_ M)).app X ≫ (F.map (ρ_ n).hom).app X =
    𝟙 ((𝟙_ (C ⥤ C)).obj ((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
this :
  (ρ_ (F.obj n)).hom.app X =
    ((𝟙 (F.obj n) ⊗ F.ε) ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor n (𝟙_ M) ≫ F.map (ρ_ n).hom).app X
⊢ F.ε.app ((F.obj n).obj X) ≫ (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor n (𝟙_ M)).app X ≫ (F.map (ρ_ n).hom).app X =
    𝟙 ((𝟙_ (C ⥤ C)).obj ((F.obj n).obj 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)
n : M
X : C
this :
  𝟙 ((F.obj n).obj X) =
    (F.ε.app ((F.obj n).obj X) ≫ (F.obj (𝟙_ M)).map (𝟙 ((F.obj n).obj X))) ≫
      (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor n (𝟙_ M)).app X ≫ (F.map (ρ_ n).hom).app X
⊢ F.ε.app ((F.obj n).obj X) ≫ (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor n (𝟙_ M)).app X ≫ (F.map (ρ_ n).hom).app X =
    𝟙 ((𝟙_ (C ⥤ C)).obj ((F.obj n).obj X))
simpa using this.symm