no goals
C : Type u₁
inst✝³ : Category C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X Y X' Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ F.map (f ⊗ g) =
    inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X X') ≫
      (F.map f ⊗ F.map g) ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y Y'
simp