C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m n n' : M
g : n ⟶ n'
X : C
⊢ (F.map g).app ((F.obj m).obj X) ≫ inv ((MonoidalFunctor.μIso F m n').inv.app X) =
    inv ((MonoidalFunctor.μIso F m n).inv.app X) ≫ (F.map (𝟙 m ⊗ g)).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 n' : M
g : n ⟶ n'
X : C
⊢ (MonoidalFunctor.μIso F m n).inv.app X ≫ (F.map g).app ((F.obj m).obj X) =
    (F.map (𝟙 m ⊗ g)).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 n' : M
g : n ⟶ n'
X : C
⊢ (F.map g).app ((F.obj m).obj X) ≫ inv ((MonoidalFunctor.μIso F m n').inv.app X) =
    inv ((MonoidalFunctor.μIso F m n).inv.app X) ≫ (F.map (𝟙 m ⊗ g)).app X
simp