V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
A B : Action V G
⊢ inv ((MonoidalFunctor.μIso (functorCategoryMonoidalEquivalence V G) A B).app PUnit.unit).hom =
    𝟙 (((functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor.obj (A ⊗ B)).obj PUnit.unit)
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
A B : Action V G
⊢ (MonoidalFunctor.μIso (functorCategoryMonoidalEquivalence V G) A B).inv.app PUnit.unit =
    𝟙 (((functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor.obj (A ⊗ B)).obj PUnit.unit)
rw [← NatIso.app_inv, ← IsIso.Iso.inv_hom]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
A B : Action V G
⊢ ((MonoidalFunctor.μIso (functorCategoryMonoidalEquivalence V G) A B).app PUnit.unit).hom ≫
      𝟙 (((functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor.obj (A ⊗ B)).obj PUnit.unit) =
    𝟙
      (((functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor.obj A ⊗
            (functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor.obj B).obj
        PUnit.unit)
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
A B : Action V G
⊢ inv ((MonoidalFunctor.μIso (functorCategoryMonoidalEquivalence V G) A B).app PUnit.unit).hom =
    𝟙 (((functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor.obj (A ⊗ B)).obj PUnit.unit)
refine' IsIso.inv_eq_of_hom_inv_id _
no goals
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
A B : Action V G
⊢ ((MonoidalFunctor.μIso (functorCategoryMonoidalEquivalence V G) A B).app PUnit.unit).hom ≫
      𝟙 (((functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor.obj (A ⊗ B)).obj PUnit.unit) =
    𝟙
      (((functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor.obj A ⊗
            (functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor.obj B).obj
        PUnit.unit)
rw [Category.comp_id, NatIso.app_hom, MonoidalFunctor.μIso_hom,
  functorCategoryMonoidalEquivalence.μ_app]