-- Module: Mathlib.CategoryTheory.Localization.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₁₂ : Type u_4
C₂₃ : Type u_5
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
D₁₂ : Type u_9
D₂₃ : Type u_10
C : Type u_11
D : Type u_12
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_6} D₁
inst_4 : Category.{v_5, u_7} D₂
inst_5 : Category.{v_6, u_8} D₃
inst_6 : Category.{v_7, u_4} C₁₂
inst_7 : Category.{v_8, u_5} C₂₃
inst_8 : Category.{v_9, u_9} D₁₂
inst_9 : Category.{v_10, u_10} D₂₃
inst_10 : Category.{v_11, u_11} C
inst_11 : Category.{v_12, u_12} D
L₁ : Functor.{v_1, v_4, u_1, u_6} C₁ D₁
L₂ : Functor.{v_2, v_5, u_2, u_7} C₂ D₂
L₃ : Functor.{v_3, v_6, u_3, u_8} C₃ D₃
L₁₂ : Functor.{v_7, v_9, u_4, u_9} C₁₂ D₁₂
L₂₃ : Functor.{v_8, v_10, u_5, u_10} C₂₃ D₂₃
L : Functor.{v_11, v_12, u_11, u_12} C D
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₃ : MorphismProperty.{v_3, u_3} C₃
W₁₂ : MorphismProperty.{v_7, u_4} C₁₂
W₂₃ : MorphismProperty.{v_8, u_5} C₂₃
inst_12 : W₁.ContainsIdentities
inst_13 : W₂.ContainsIdentities
inst_14 : W₃.ContainsIdentities
inst_15 : L₁.IsLocalization W₁
inst_16 : L₂.IsLocalization W₂
inst_17 : L₃.IsLocalization W₃
F₁₂ : C₁ ⥤ Functor.{v_2, v_7, u_2, u_4} C₂ C₁₂
G : C₁₂ ⥤ Functor.{v_3, v_11, u_3, u_11} C₃ C
F : C₁ ⥤ Functor.{v_8, v_11, u_5, u_11} C₂₃ C
G₂₃ : C₂ ⥤ Functor.{v_3, v_8, u_3, u_5} C₃ C₂₃
iso : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
F₁₂' : D₁ ⥤ Functor.{v_5, v_9, u_7, u_9} D₂ D₁₂
G' : D₁₂ ⥤ Functor.{v_6, v_12, u_8, u_12} D₃ D
F' : D₁ ⥤ Functor.{v_10, v_12, u_10, u_12} D₂₃ D
G₂₃' : D₂ ⥤ Functor.{v_6, v_10, u_8, u_10} D₃ D₂₃
inst_18 : Lifting₂ L₁ L₂ W₁ W₂ (F₁₂ ⋙ obj (whiskeringRight C₂ C₁₂ D₁₂) L₁₂) F₁₂'
inst_19 : Lifting₂ L₁₂ L₃ W₁₂ W₃ (G ⋙ obj (whiskeringRight C₃ C D) L) G'
inst_20 : Lifting₂ L₁ L₂₃ W₁ W₂₃ (F ⋙ obj (whiskeringRight C₂₃ C D) L) F'
inst_21 : Lifting₂ L₂ L₃ W₂ W₃ (G₂₃ ⋙ obj (whiskeringRight C₃ C₂₃ D₂₃) L₂₃) G₂₃'
X₁ : C₁
X₂ : C₂
X₃ : C₃
rw :
  Eq (α :=
    (G'.obj ((F₁₂'.obj (L₁.obj X₁)).obj (L₂.obj X₂))).obj (L₃.obj X₃) ⟶
      (F'.obj (L₁.obj X₁)).obj ((G₂₃'.obj (L₂.obj X₂)).obj (L₃.obj X₃)))
    (NatTrans.app
          (NatTrans.app
            (NatTrans.app
              (Iso.hom
                (Lifting₃.iso L₁ L₂ L₃ W₁ W₂ W₃ (obj (obj postcompose₃ L) (bifunctorComp₁₂ F₁₂ G))
                  (bifunctorComp₁₂ F₁₂' G')))
              X₁)
            X₂)
          X₃ ≫
        NatTrans.app (NatTrans.app (NatTrans.app (map (obj postcompose₃ L) iso.hom) X₁) X₂) X₃ ≫
          NatTrans.app
            (NatTrans.app
              (NatTrans.app
                (Iso.inv
                  (Lifting₃.iso L₁ L₂ L₃ W₁ W₂ W₃ (obj (obj postcompose₃ L) (bifunctorComp₂₃ F G₂₃))
                    (bifunctorComp₂₃ F' G₂₃')))
                X₁)
              X₂)
            X₃ :
      (((obj (obj (obj (obj (whiskeringLeft₃ D) L₁) L₂) L₃) (bifunctorComp₁₂ F₁₂' G')).obj X₁).obj X₂).obj X₃ ⟶
        (((obj (obj (obj (obj (whiskeringLeft₃ D) L₁) L₂) L₃) (bifunctorComp₂₃ F' G₂₃')).obj X₁).obj X₂).obj X₃)
    ((G'.map (((Lifting₂.iso L₁ L₂ W₁ W₂ (F₁₂ ⋙ obj (whiskeringRight C₂ C₁₂ D₁₂) L₁₂) F₁₂').hom.app X₁).app X₂)).app
        (L₃.obj X₃) ≫
      NatTrans.app ((Lifting₂.iso L₁₂ L₃ W₁₂ W₃ (G ⋙ obj (whiskeringRight C₃ C D) L) G').hom.app ((F₁₂.obj X₁).obj X₂))
          X₃ ≫
        L.map (((iso.hom.app X₁).app X₂).app X₃) ≫
          ((Lifting₂.iso L₁ L₂₃ W₁ W₂₃ (F ⋙ obj (whiskeringRight C₂₃ C D) L) F').inv.app X₁).app ((G₂₃.obj X₂).obj X₃) ≫
            (F'.obj (L₁.obj X₁)).map
              (((Lifting₂.iso L₂ L₃ W₂ W₃ (G₂₃ ⋙ obj (whiskeringRight C₃ C₂₃ D₂₃) L₂₃) G₂₃').inv.app X₂).app X₃))
⊢ Eq (α :=
    (G'.obj ((F₁₂'.obj (L₁.obj X₁)).obj (L₂.obj X₂))).obj (L₃.obj X₃) ⟶
      (F'.obj (L₁.obj X₁)).obj ((G₂₃'.obj (L₂.obj X₂)).obj (L₃.obj X₃)))
    (NatTrans.app
        (NatTrans.app
          (NatTrans.app
            (lift₃NatTrans L₁ L₂ L₃ W₁ W₂ W₃ (obj (obj postcompose₃ L) (bifunctorComp₁₂ F₁₂ G))
              (obj (obj postcompose₃ L) (bifunctorComp₂₃ F G₂₃)) (bifunctorComp₁₂ F₁₂' G') (bifunctorComp₂₃ F' G₂₃')
              (map (obj postcompose₃ L) iso.hom))
            (L₁.obj X₁))
          (L₂.obj X₂))
        (L₃.obj X₃) :
      ((bifunctorComp₁₂Obj F₁₂' G' (L₁.obj X₁)).obj (L₂.obj X₂)).obj (L₃.obj X₃) ⟶
        ((bifunctorComp₂₃Obj F' G₂₃' (L₁.obj X₁)).obj (L₂.obj X₂)).obj (L₃.obj X₃))
    ((G'.map (((Lifting₂.iso L₁ L₂ W₁ W₂ (F₁₂ ⋙ obj (whiskeringRight C₂ C₁₂ D₁₂) L₁₂) F₁₂').hom.app X₁).app X₂)).app
        (L₃.obj X₃) ≫
      NatTrans.app ((Lifting₂.iso L₁₂ L₃ W₁₂ W₃ (G ⋙ obj (whiskeringRight C₃ C D) L) G').hom.app ((F₁₂.obj X₁).obj X₂))
          X₃ ≫
        L.map (((iso.hom.app X₁).app X₂).app X₃) ≫
          ((Lifting₂.iso L₁ L₂₃ W₁ W₂₃ (F ⋙ obj (whiskeringRight C₂₃ C D) L) F').inv.app X₁).app ((G₂₃.obj X₂).obj X₃) ≫
            (F'.obj (L₁.obj X₁)).map
              (((Lifting₂.iso L₂ L₃ W₂ W₃ (G₂₃ ⋙ obj (whiskeringRight C₃ C₂₃ D₂₃) L₂₃) G₂₃').inv.app X₂).app X₃))

Tactic:
rw [lift₃NatTrans_app_app_app]

Premises used: CategoryTheory.Localization.lift₃NatTrans_app_app_app