CategoryTheory.μ_hom_inv_app

theorem CategoryTheory.μ_hom_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{u_2, u_1} M] [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)) (i j : M) (X : C), CategoryTheory.CategoryStruct.comp ((F.μ i j).app X) ((F.μIso i j).inv.app X) = CategoryTheory.CategoryStruct.id ((CategoryTheory.MonoidalCategory.tensorObj (F.obj i) (F.obj j)).obj X)

The theorem `CategoryTheory.μ_hom_inv_app` states that for any type `C` forming a category, another type `M` also forming a category and being a Monoidal category, and a Monoidal functor `F` mapping from `M` to the endomorphisms on `C`, then for all `i`, `j` in `M` and `X` in `C`, the composition of the application of the morphism `F.μ i j` to `X` and the application of the inverse of the morphism `CategoryTheory.MonoidalFunctor.μIso F i j` to `X` is equivalent to the identity morphism on the object resulting from the tensor product of `F.obj i` and `F.obj j` applied to `X`. Here, `F.μ i j` and `CategoryTheory.MonoidalFunctor.μIso F i j` refer to specific morphisms related to the monoidal structure of `F`.

More concisely: For any monoidal functor F from a monoidal category M to the endomorphisms on a category C, the application of F.μ i j, followed by the inverse of F.μIso i j, is equivalent to the identity morphism on the tensor product of F.obj i and F.obj j in C.