-- 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_4} →
        {D₁ : Type u_6} →
          {D₂ : Type u_7} →
            {D₃ : Type u_8} →
              {D₁₂ : Type u_9} →
                {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_7, u_4} C₁₂] →
                                  [inst_7 : CategoryTheory.Category.{v_9, u_9} 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')