-- Mathlib.CategoryTheory.GradedObject.Trifunctor
/-- The action on graded objects of a trifunctor obtained by composition of two
bifunctors can be computed as a composition of the actions of these two bifunctors.  -/
CategoryTheory.GradedObject.mapBifunctorComp₂₃MapObjIso : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        {C₂₃ : Type u_6} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] →
                    (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) →
                      (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) →
                        {I₁ : Type u_7} →
                          {I₂ : Type u_8} →
                            {I₃ : Type u_9} →
                              {J : Type u_10} →
                                {r : I₁ × I₂ × I₃ → J} →
                                  (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) →
                                    (X₁ : CategoryTheory.GradedObject I₁ C₁) →
                                      (X₂ : CategoryTheory.GradedObject I₂ C₂) →
                                        (X₃ : CategoryTheory.GradedObject I₃ C₃) →
                                          [inst_5 :
                                              (((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj
                                                    X₃).HasMap
                                                ρ₂₃.p] →
                                            [inst_6 :
                                                (((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
                                                      (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂
                                                        X₃)).HasMap
                                                  ρ₂₃.q] →
                                              [H :
                                                  CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂
                                                    X₃] →
                                                [inst_7 :
                                                    ((((CategoryTheory.GradedObject.mapTrifunctor
                                                                      (CategoryTheory.bifunctorComp₂₃ F G₂₃) I₁ I₂
                                                                      I₃).obj
                                                                  X₁).obj
                                                              X₂).obj
                                                          X₃).HasMap
                                                      r] →
                                                  CategoryTheory.GradedObject.mapTrifunctorMapObj
                                                      (CategoryTheory.bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ ≅
                                                    CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁
                                                      (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)