no goals
V : Type (u + 1)
inst✝³ : LargeCategory V
W : Type (u + 1)
inst✝² : LargeCategory W
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalCategory W
F : MonoidalFunctor V W
G : MonCat
X Y : Action V G
⊢ (inv (LaxMonoidalFunctor.μ (mapAction F G).toLaxMonoidalFunctor X Y)).hom =
    inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V)
rw [← cancel_mono (F.μ X.V Y.V), IsIso.inv_hom_id, ← F.mapAction_toLaxMonoidalFunctor_μ_hom G,
  ← Action.comp_hom, IsIso.inv_hom_id, Action.id_hom]