C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m n m' : M
f : m ⟶ m'
X : C
⊢ (F.obj n).map ((F.map f).app X) ≫ inv ((MonoidalFunctor.μIso F m' n).inv.app X) =
    inv ((MonoidalFunctor.μIso F m n).inv.app X) ≫ (F.map (f ⊗ 𝟙 n)).app X
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m n m' : M
f : m ⟶ m'
X : C
⊢ (MonoidalFunctor.μIso F m n).inv.app X ≫ (F.obj n).map ((F.map f).app X) =
    (F.map (f ⊗ 𝟙 n)).app X ≫ (MonoidalFunctor.μIso F m' n).inv.app X
rw [← IsIso.comp_inv_eq, Category.assoc, ← IsIso.eq_inv_comp]
no goals
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m n m' : M
f : m ⟶ m'
X : C
⊢ (F.obj n).map ((F.map f).app X) ≫ inv ((MonoidalFunctor.μIso F m' n).inv.app X) =
    inv ((MonoidalFunctor.μIso F m n).inv.app X) ≫ (F.map (f ⊗ 𝟙 n)).app X
simp