-- Mathlib/CategoryTheory/Localization/Trifunctor.lean
lemma associator_hom_app_app_app (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) :
    (((associator L₁ L₂ L₃ L₁₂ L₂₃ L W₁ W₂ W₃ W₁₂ W₂₃ iso F₁₂' G' F' G₂₃').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 _ _ _).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 _ _ _).obj L₂₃) G₂₃').inv.app X₂).app X₃)

Proof state:
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.{u_19, u_1} C₁
inst✝²⁰ : Category.{u_20, u_2} C₂
inst✝¹⁹ : Category.{u_21, u_3} C₃
inst✝¹⁸ : Category.{u_17, u_6} D₁
inst✝¹⁷ : Category.{u_16, u_7} D₂
inst✝¹⁶ : Category.{u_15, u_8} D₃
inst✝¹⁵ : Category.{u_23, u_4} C₁₂
inst✝¹⁴ : Category.{u_24, u_5} C₂₃
inst✝¹³ : Category.{u_18, u_9} D₁₂
inst✝¹² : Category.{u_22, u_10} D₂₃
inst✝¹¹ : Category.{u_25, u_11} C
inst✝¹⁰ : Category.{u_14, 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₃ ((Functor.postcompose₃.obj L).obj (bifunctorComp₁₂ F₁₂ G))
                      (bifunctorComp₁₂ F₁₂' G')).hom.app
                X₁).app
            X₂).app
        X₃ ≫
      ((((Functor.postcompose₃.obj L).map iso.hom).app X₁).app X₂).app X₃ ≫
        (((Lifting₃.iso L₁ L₂ L₃ W₁ W₂ W₃ ((Functor.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₃)

Tactic:
dsimp [Lifting₃.iso, Lifting₃.bifunctorComp₁₂, Lifting₃.bifunctorComp₂₃]

Result:
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.{u_19, u_1} C₁
inst✝²⁰ : Category.{u_20, u_2} C₂
inst✝¹⁹ : Category.{u_21, u_3} C₃
inst✝¹⁸ : Category.{u_17, u_6} D₁
inst✝¹⁷ : Category.{u_16, u_7} D₂
inst✝¹⁶ : Category.{u_15, u_8} D₃
inst✝¹⁵ : Category.{u_23, u_4} C₁₂
inst✝¹⁴ : Category.{u_24, u_5} C₂₃
inst✝¹³ : Category.{u_18, u_9} D₁₂
inst✝¹² : Category.{u_22, u_10} D₂₃
inst✝¹¹ : Category.{u_25, u_11} C
inst✝¹⁰ : Category.{u_14, 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₃
⊢ ((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₃) =
    (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₃)