Module: Mathlib.CategoryTheory.Localization.Trifunctor

Goal state before:
pp: 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✝²⁰ : Category.{v_2, u_2} C₂
inst✝¹⁹ : Category.{v_3, u_3} C₃
inst✝¹⁸ : Category.{v_4, u_6} D₁
inst✝¹⁷ : Category.{v_5, u_7} D₂
inst✝¹⁶ : Category.{v_6, u_8} D₃
inst✝¹⁵ : Category.{v_7, u_4} C₁₂
inst✝¹⁴ : Category.{v_8, u_5} C₂₃
inst✝¹³ : Category.{v_9, u_9} D₁₂
inst✝¹² : Category.{v_10, u_10} D₂₃
inst✝¹¹ : Category.{v_11, u_11} C
inst✝¹⁰ : Category.{v_12, u_12} D
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
L₃ : C₃ ⥤ D₃
L₁₂ : C₁₂ ⥤ D₁₂
L₂₃ : C₂₃ ⥤ D₂₃
L : C ⥤ D
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
W₁₂ : MorphismProperty C₁₂
W₂₃ : MorphismProperty C₂₃
inst✝⁹ : W₁.ContainsIdentities
inst✝⁸ : W₂.ContainsIdentities
inst✝⁷ : W₃.ContainsIdentities
inst✝⁶ : L₁.IsLocalization W₁
inst✝⁵ : L₂.IsLocalization W₂
inst✝⁴ : L₃.IsLocalization W₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C
F : C₁ ⥤ C₂₃ ⥤ C
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
iso : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
F₁₂' : D₁ ⥤ D₂ ⥤ D₁₂
G' : D₁₂ ⥤ D₃ ⥤ D
F' : D₁ ⥤ D₂₃ ⥤ D
G₂₃' : D₂ ⥤ D₃ ⥤ D₂₃
inst✝³ : Lifting₂ L₁ L₂ W₁ W₂ (F₁₂ ⋙ (whiskeringRight C₂ C₁₂ D₁₂).obj L₁₂) F₁₂'
inst✝² : Lifting₂ L₁₂ L₃ W₁₂ W₃ (G ⋙ (whiskeringRight C₃ C D).obj L) G'
inst✝¹ : Lifting₂ L₁ L₂₃ W₁ W₂₃ (F ⋙ (whiskeringRight C₂₃ C D).obj L) F'
inst✝ : Lifting₂ L₂ L₃ W₂ W₃ (G₂₃ ⋙ (whiskeringRight C₃ C₂₃ D₂₃).obj L₂₃) G₂₃'
X₁ : C₁
X₂ : C₂
X₃ : C₃
⊢ (((lift₃NatTrans L₁ L₂ L₃ W₁ W₂ W₃ ((postcompose₃.obj L).obj (bifunctorComp₁₂ F₁₂ G))
                  ((postcompose₃.obj L).obj (bifunctorComp₂₃ F G₂₃)) (bifunctorComp₁₂ F₁₂' G') (bifunctorComp₂₃ F' G₂₃')
                  ((postcompose₃.obj L).map iso.hom)).app
              (L₁.obj X₁)).app
          (L₂.obj X₂)).app
      (L₃.obj X₃) =
    (G'.map (((Lifting₂.iso L₁ L₂ W₁ W₂ (F₁₂ ⋙ (whiskeringRight C₂ C₁₂ D₁₂).obj L₁₂) F₁₂').hom.app X₁).app X₂)).app
        (L₃.obj X₃) ≫
      ((Lifting₂.iso L₁₂ L₃ W₁₂ W₃ (G ⋙ (whiskeringRight C₃ C D).obj L) G').hom.app ((F₁₂.obj X₁).obj X₂)).app X₃ ≫
        L.map (((iso.hom.app X₁).app X₂).app X₃) ≫
          ((Lifting₂.iso L₁ L₂₃ W₁ W₂₃ (F ⋙ (whiskeringRight C₂₃ C D).obj L) F').inv.app X₁).app ((G₂₃.obj X₂).obj X₃) ≫
            (F'.obj (L₁.obj X₁)).map
              (((Lifting₂.iso L₂ L₃ W₂ W₃ (G₂₃ ⋙ (whiskeringRight C₃ C₂₃ D₂₃).obj L₂₃) G₂₃').inv.app X₂).app X₃)

Tactic:
rw [lift₃NatTrans_app_app_app]

Goal state after:
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✝²⁰ : Category.{v_2, u_2} C₂
inst✝¹⁹ : Category.{v_3, u_3} C₃
inst✝¹⁸ : Category.{v_4, u_6} D₁
inst✝¹⁷ : Category.{v_5, u_7} D₂
inst✝¹⁶ : Category.{v_6, u_8} D₃
inst✝¹⁵ : Category.{v_7, u_4} C₁₂
inst✝¹⁴ : Category.{v_8, u_5} C₂₃
inst✝¹³ : Category.{v_9, u_9} D₁₂
inst✝¹² : Category.{v_10, u_10} D₂₃
inst✝¹¹ : Category.{v_11, u_11} C
inst✝¹⁰ : Category.{v_12, u_12} D
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
L₃ : C₃ ⥤ D₃
L₁₂ : C₁₂ ⥤ D₁₂
L₂₃ : C₂₃ ⥤ D₂₃
L : C ⥤ D
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
W₁₂ : MorphismProperty C₁₂
W₂₃ : MorphismProperty C₂₃
inst✝⁹ : W₁.ContainsIdentities
inst✝⁸ : W₂.ContainsIdentities
inst✝⁷ : W₃.ContainsIdentities
inst✝⁶ : L₁.IsLocalization W₁
inst✝⁵ : L₂.IsLocalization W₂
inst✝⁴ : L₃.IsLocalization W₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C
F : C₁ ⥤ C₂₃ ⥤ C
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
iso : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
F₁₂' : D₁ ⥤ D₂ ⥤ D₁₂
G' : D₁₂ ⥤ D₃ ⥤ D
F' : D₁ ⥤ D₂₃ ⥤ D
G₂₃' : D₂ ⥤ D₃ ⥤ D₂₃
inst✝³ : Lifting₂ L₁ L₂ W₁ W₂ (F₁₂ ⋙ (whiskeringRight C₂ C₁₂ D₁₂).obj L₁₂) F₁₂'
inst✝² : Lifting₂ L₁₂ L₃ W₁₂ W₃ (G ⋙ (whiskeringRight C₃ C D).obj L) G'
inst✝¹ : Lifting₂ L₁ L₂₃ W₁ W₂₃ (F ⋙ (whiskeringRight C₂₃ C D).obj L) F'
inst✝ : Lifting₂ L₂ L₃ W₂ W₃ (G₂₃ ⋙ (whiskeringRight C₃ C₂₃ D₂₃).obj L₂₃) G₂₃'
X₁ : C₁
X₂ : C₂
X₃ : C₃
⊢ (((Lifting₃.iso L₁ L₂ L₃ W₁ W₂ W₃ ((postcompose₃.obj L).obj (bifunctorComp₁₂ F₁₂ G))
                      (bifunctorComp₁₂ F₁₂' G')).hom.app
                X₁).app
            X₂).app
        X₃ ≫
      ((((postcompose₃.obj L).map iso.hom).app X₁).app X₂).app X₃ ≫
        (((Lifting₃.iso L₁ L₂ L₃ W₁ W₂ W₃ ((postcompose₃.obj L).obj (bifunctorComp₂₃ F G₂₃))
                        (bifunctorComp₂₃ F' G₂₃')).inv.app
                  X₁).app
              X₂).app
          X₃ =
    (G'.map (((Lifting₂.iso L₁ L₂ W₁ W₂ (F₁₂ ⋙ (whiskeringRight C₂ C₁₂ D₁₂).obj L₁₂) F₁₂').hom.app X₁).app X₂)).app
        (L₃.obj X₃) ≫
      ((Lifting₂.iso L₁₂ L₃ W₁₂ W₃ (G ⋙ (whiskeringRight C₃ C D).obj L) G').hom.app ((F₁₂.obj X₁).obj X₂)).app X₃ ≫
        L.map (((iso.hom.app X₁).app X₂).app X₃) ≫
          ((Lifting₂.iso L₁ L₂₃ W₁ W₂₃ (F ⋙ (whiskeringRight C₂₃ C D).obj L) F').inv.app X₁).app ((G₂₃.obj X₂).obj X₃) ≫
            (F'.obj (L₁.obj X₁)).map
              (((Lifting₂.iso L₂ L₃ W₂ W₃ (G₂₃ ⋙ (whiskeringRight C₃ C₂₃ D₂₃).obj L₂₃) G₂₃').inv.app X₂).app X₃)