no goals
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
X Y : C
f : X ⟶ Y
⊢ (MonoidalFunctor.εIso F).inv.app X ≫ (𝟙_ (C ⥤ C)).map f = (MonoidalFunctor.εIso F).inv.app X ≫ f
aesop_cat