-- Mathlib.CategoryTheory.Localization.Trifunctor
/-- The construction `bifunctorComp₂₃` of a trifunctor by composition of bifunctors
is compatible with localization.  -/
CategoryTheory.Localization.Lifting₃.bifunctorComp₂₃ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₂₃ : Type u_5} →
        {D₁ : Type u_6} →
          {D₂ : Type u_7} →
            {D₃ : Type u_8} →
              {D₂₃ : Type u_10} →
                {C : Type u_11} →
                  {D : Type u_12} →
                    [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_6} D₁] →
                            [inst_4 : CategoryTheory.Category.{v_5, u_7} D₂] →
                              [inst_5 : CategoryTheory.Category.{v_6, u_8} D₃] →
                                [inst_6 : CategoryTheory.Category.{v_8, u_5} C₂₃] →
                                  [inst_7 : CategoryTheory.Category.{v_10, u_10} D₂₃] →
                                    [inst_8 : CategoryTheory.Category.{v_11, u_11} C] →
                                      [inst_9 : CategoryTheory.Category.{v_12, u_12} D] →
                                        (L₁ : CategoryTheory.Functor C₁ D₁) →
                                          (L₂ : CategoryTheory.Functor C₂ D₂) →
                                            (L₃ : CategoryTheory.Functor C₃ D₃) →
                                              (L₂₃ : CategoryTheory.Functor C₂₃ D₂₃) →
                                                (L : CategoryTheory.Functor C D) →
                                                  (W₁ : CategoryTheory.MorphismProperty C₁) →
                                                    (W₂ : CategoryTheory.MorphismProperty C₂) →
                                                      (W₃ : CategoryTheory.MorphismProperty C₃) →
                                                        (W₂₃ : CategoryTheory.MorphismProperty C₂₃) →
                                                          (F :
                                                              CategoryTheory.Functor C₁
                                                                (CategoryTheory.Functor C₂₃ C)) →
                                                            (G₂₃ :
                                                                CategoryTheory.Functor C₂
                                                                  (CategoryTheory.Functor C₃ C₂₃)) →
                                                              (F' :
                                                                  CategoryTheory.Functor D₁
                                                                    (CategoryTheory.Functor D₂₃ D)) →
                                                                (G₂₃' :
                                                                    CategoryTheory.Functor D₂
                                                                      (CategoryTheory.Functor D₃ D₂₃)) →
                                                                  [CategoryTheory.Localization.Lifting₂ L₁ L₂₃ W₁ W₂₃
                                                                        (F.comp
                                                                          ((CategoryTheory.Functor.whiskeringRight C₂₃ C
                                                                                D).obj
                                                                            L))
                                                                        F'] →
                                                                    [CategoryTheory.Localization.Lifting₂ L₂ L₃ W₂ W₃
                                                                          (G₂₃.comp
                                                                            ((CategoryTheory.Functor.whiskeringRight C₃
                                                                                  C₂₃ D₂₃).obj
                                                                              L₂₃))
                                                                          G₂₃'] →
                                                                      CategoryTheory.Localization.Lifting₃ L₁ L₂ L₃ W₁
                                                                        W₂ W₃
                                                                        ((CategoryTheory.Functor.postcompose₃.obj L).obj
                                                                          (CategoryTheory.bifunctorComp₂₃ F G₂₃))
                                                                        (CategoryTheory.bifunctorComp₂₃ F' G₂₃')