-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Trifunctor (goal)
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₃
⊢ 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₃
have 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₃
Tactic: dsimp [lift₃NatTrans, fullyFaithfulUncurry₃, Equivalence.fullyFaithfulFunctor]