-- Module: Mathlib.CategoryTheory.Localization.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_13
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_13, u_13} E
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₃
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₃ : MorphismProperty.{v_3, u_3} C₃
inst_7 : L₁.IsLocalization W₁
inst_8 : L₂.IsLocalization W₂
inst_9 : L₃.IsLocalization W₃
inst_10 : W₁.ContainsIdentities
inst_11 : W₂.ContainsIdentities
inst_12 : W₃.ContainsIdentities
F₁ F₂ : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_13, u_3, u_13} C₃ E
F₁' F₂' : D₁ ⥤ D₂ ⥤ Functor.{v_6, v_13, u_8, u_13} D₃ E
inst_13 : Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁'
inst_14 : Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂'
τ : F₁ ⟶ F₂
X₁ : C₁
X₂ : C₂
X₃ : C₃
dsimp :
  CategoryStruct.comp (Y :=
      (((obj (Equivalence.inverse currying₃) (obj (Equivalence.functor currying₃) F₁')).obj (L₁.obj X₁)).obj
            (L₂.obj X₂)).obj
        (L₃.obj X₃))
      (NatTrans.app
          (NatTrans.app (NatTrans.app (NatTrans.app (Iso.hom (Equivalence.unitIso currying₃)) F₁') (L₁.obj X₁))
            (L₂.obj X₂))
          (L₃.obj X₃) :
        ((F₁'.obj (L₁.obj X₁)).obj (L₂.obj X₂)).obj (L₃.obj X₃) ⟶
          (((obj (Equivalence.inverse currying₃) (obj (Equivalence.functor currying₃) F₁')).obj (L₁.obj X₁)).obj
                (L₂.obj X₂)).obj
            (L₃.obj X₃))
      (CategoryStruct.comp (Y :=
          (((obj (Equivalence.inverse currying₃) (obj (Equivalence.functor currying₃) F₂')).obj (L₁.obj X₁)).obj
                (L₂.obj X₂)).obj
            (L₃.obj X₃))
          (NatTrans.app
              (liftNatTrans (L₁.prod (L₂.prod L₃)) (W₁.prod (W₂.prod W₃)) (obj uncurry₃ F₁) (obj uncurry₃ F₂)
                (obj uncurry₃ F₁') (obj uncurry₃ F₂') (map uncurry₃ τ))
              (L₁.obj X₁, L₂.obj X₂, L₃.obj X₃) :
            (obj (Equivalence.functor currying₃) F₁').obj (L₁.obj X₁, L₂.obj X₂, L₃.obj X₃) ⟶
              (obj (Equivalence.functor currying₃) F₂').obj (L₁.obj X₁, L₂.obj X₂, L₃.obj X₃))
          (NatTrans.app
              (NatTrans.app (NatTrans.app (NatTrans.app (Iso.inv (Equivalence.unitIso currying₃)) F₂') (L₁.obj X₁))
                (L₂.obj X₂))
              (L₃.obj X₃) :
            (((obj (Equivalence.inverse currying₃) (obj (Equivalence.functor currying₃) F₂')).obj (L₁.obj X₁)).obj
                    (L₂.obj X₂)).obj
                (L₃.obj X₃) ⟶
              ((F₂'.obj (L₁.obj X₁)).obj (L₂.obj X₂)).obj (L₃.obj X₃)) :
        (((obj (Equivalence.inverse currying₃) (obj (Equivalence.functor currying₃) F₁')).obj (L₁.obj X₁)).obj
                (L₂.obj X₂)).obj
            (L₃.obj X₃) ⟶
          ((F₂'.obj (L₁.obj X₁)).obj (L₂.obj X₂)).obj (L₃.obj X₃)) =
    (((Lifting₃.iso L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁').hom.app X₁).app X₂).app X₃ ≫
      ((τ.app X₁).app X₂).app X₃ ≫ (((Lifting₃.iso L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂').inv.app X₁).app X₂).app X₃
⊢ NatTrans.app (NatTrans.app ((lift₃NatTrans L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₂ F₁' F₂' τ).app (L₁.obj X₁)) (L₂.obj X₂))
      (L₃.obj X₃) =
    (((Lifting₃.iso L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁').hom.app X₁).app X₂).app X₃ ≫
      ((τ.app X₁).app X₂).app X₃ ≫ (((Lifting₃.iso L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂').inv.app X₁).app X₂).app X₃

Tactic:
dsimp [lift₃NatTrans, fullyFaithfulUncurry₃, Equivalence.fullyFaithfulFunctor]

Premises used: CategoryTheory.Equivalence.fullyFaithfulFunctor, CategoryTheory.Localization.lift₃NatTrans, CategoryTheory.Functor.fullyFaithfulUncurry₃