-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u₁
inst_1 : Category.{v₁, u₁} J
K : Type u₂
inst_2 : Category.{v₂, u₂} K
D : Type u₃
inst_3 : Category.{v₃, u₃} D
inst_4 : HasLimitsOfShape.{v₁, u₁, v, u} J C
inst_5 : HasColimitsOfShape.{v₂, u₂, v, u} K C
inst_6 : PreservesLimitsOfShape (C := Functor.{v₂, v, u₂, u} K C) J colim
d : D
F G : K ⥤ Functor.{v₃, v, u₃, u} D C
η : F ⟶ G
j : K
⊢ Eq (α :=
    (F.obj j).obj d ⟶
      obj (colimit (Functor.flip (obj (whiskeringRight K (Functor.{v₃, v, u₃, u} D C) C) (obj (evaluation D C) d)))) G)
    (CategoryStruct.comp (Y := (colimit F).obj d) (NatTrans.app (colimit.ι F j) d)
      (map (colim ⋙ obj (evaluation D C) d) η ≫
        Iso.hom
          ((fun (X : K ⥤ Functor.{v₃, v, u₃, u} D C) ↦
              (Iso.trans (Y := colimit (X ⋙ obj (evaluation D C) d))
                  (colimitObjIsoColimitCompEvaluation X d : (colimit X).obj d ≅ colimit (X ⋙ obj (evaluation D C) d))
                  (Iso.trans (Y :=
                      colimit
                        (Functor.flip
                            (obj (whiskeringRight K (Functor.{v₃, v, u₃, u} D C) C) (obj (evaluation D C) d)) ⋙
                          obj (evaluation (K ⥤ Functor.{v₃, v, u₃, u} D C) C) X))
                      (HasColimit.isoOfNatIso (Iso.refl (X ⋙ obj (evaluation D C) d)))
                      (Iso.symm
                        (colimitObjIsoColimitCompEvaluation
                          (Functor.flip
                            (obj (whiskeringRight K (Functor.{v₃, v, u₃, u} D C) C) (obj (evaluation D C) d)))
                          X)) :
                    colimit (X ⋙ obj (evaluation D C) d) ≅
                      obj
                        (colimit
                          (Functor.flip
                            (obj (whiskeringRight K (Functor.{v₃, v, u₃, u} D C) C) (obj (evaluation D C) d))))
                        X) :
                obj (colim ⋙ obj (evaluation D C) d) X ≅
                  obj
                    (colimit
                      (Functor.flip (obj (whiskeringRight K (Functor.{v₃, v, u₃, u} D C) C) (obj (evaluation D C) d))))
                    X))
            G)))
    (CategoryStruct.comp (Y := (colimit F).obj d) (NatTrans.app (colimit.ι F j) d)
      (Iso.hom
          ((fun (X : K ⥤ Functor.{v₃, v, u₃, u} D C) ↦
              (Iso.trans (Y := colimit (X ⋙ obj (evaluation D C) d))
                  (colimitObjIsoColimitCompEvaluation X d : (colimit X).obj d ≅ colimit (X ⋙ obj (evaluation D C) d))
                  (Iso.trans (Y :=
                      colimit
                        (Functor.flip
                            (obj (whiskeringRight K (Functor.{v₃, v, u₃, u} D C) C) (obj (evaluation D C) d)) ⋙
                          obj (evaluation (K ⥤ Functor.{v₃, v, u₃, u} D C) C) X))
                      (HasColimit.isoOfNatIso (Iso.refl (X ⋙ obj (evaluation D C) d)))
                      (Iso.symm
                        (colimitObjIsoColimitCompEvaluation
                          (Functor.flip
                            (obj (whiskeringRight K (Functor.{v₃, v, u₃, u} D C) C) (obj (evaluation D C) d)))
                          X)) :
                    colimit (X ⋙ obj (evaluation D C) d) ≅
                      obj
                        (colimit
                          (Functor.flip
                            (obj (whiskeringRight K (Functor.{v₃, v, u₃, u} D C) C) (obj (evaluation D C) d))))
                        X) :
                obj (colim ⋙ obj (evaluation D C) d) X ≅
                  obj
                    (colimit
                      (Functor.flip (obj (whiskeringRight K (Functor.{v₃, v, u₃, u} D C) C) (obj (evaluation D C) d))))
                    X))
            F) ≫
        map (colimit (Functor.flip (obj (whiskeringRight K (Functor.{v₃, v, u₃, u} D C) C) (obj (evaluation D C) d))))
          η))

Tactic:
simp [← NatTrans.comp_app_assoc]

Premises used: CategoryTheory.NatTrans.comp_app_assoc