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 (𝟙_ M)).obj ((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)
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
⊢ (MonoidalFunctor.εIso F).inv.app ((F.obj n).obj X) =
    (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor n (𝟙_ M)).app X ≫ (F.map (ρ_ n).hom).app X
rw [← cancel_mono (F.ε.app ((F.obj n).obj X)), ε_inv_hom_app]
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 (𝟙_ M)).obj ((F.obj n).obj X)) = 𝟙 ((F.obj n ⊗ 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)
n : M
X : C
⊢ 𝟙 ((F.obj (𝟙_ M)).obj ((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)
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 (𝟙_ M)).obj ((F.obj n).obj X)) = 𝟙 ((F.obj n ⊗ F.obj (𝟙_ M)).obj X)
rfl