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
⊢ (inv (mapAction F G).toLaxMonoidalFunctor.ε).hom = inv F.ε
rw [← cancel_mono F.ε, IsIso.inv_hom_id, ← F.mapAction_toLaxMonoidalFunctor_ε_hom G,
  ← Action.comp_hom, IsIso.inv_hom_id, Action.id_hom]