C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ : M
X : C
⊢ (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 =
    (F.obj m₂).map ((MonoidalFunctor.εIso F).inv.app ((F.obj m₁).obj X) ≫ (F.map (ρ_ 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
X : C
⊢ (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 =
    (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ M) m₂).app ((F.obj m₁).obj X) ≫
      (F.map (λ_ m₂).hom).app ((F.obj m₁).obj X) ≫ (F.obj m₂).map ((F.map (ρ_ m₁).inv).app X)
rw [← obj_ε_inv_app_assoc, ← Functor.map_comp]
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ : M
X : C
⊢ (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 =
    (F.obj m₂).map ((MonoidalFunctor.εIso F).inv.app ((F.obj m₁).obj X) ≫ (F.map (ρ_ 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
X : C
⊢ (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 =
    (F.obj m₂).map ((MonoidalFunctor.εIso F).inv.app ((F.obj m₁).obj X) ≫ (F.map (ρ_ m₁).inv).app X)
congr
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
X : C
⊢ (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 =
    (F.obj m₂).map ((MonoidalFunctor.εIso F).inv.app ((F.obj m₁).obj X) ≫ (F.map (ρ_ m₁).inv).app X)
simp