-- 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 : HasColimitsOfShape.{v₁, u₁, v, u} J C
inst_5 : HasLimitsOfShape.{v₂, u₂, v, u} K C
inst_6 : PreservesColimitsOfShape (C := Functor.{v₂, v, u₂, u} K C) J lim
d : D
F G : K ⥤ Functor.{v₃, v, u₃, u} D C
η : F ⟶ G
j : K
⊢ Eq (α :=
    obj (lim ⋙ obj (evaluation D C) d) F ⟶
      obj (obj (Functor.flip (obj (whiskeringRight K (Functor.{v₃, v, u₃, u} D C) C) (obj (evaluation D C) d))) j) G)
    (CategoryStruct.comp (Y :=
      obj (limit (Functor.flip (obj (whiskeringRight K (Functor.{v₃, v, u₃, u} D C) C) (obj (evaluation D C) d)))) G)
      (map (lim ⋙ obj (evaluation D C) d) η ≫
        Iso.hom
          ((fun (X : K ⥤ Functor.{v₃, v, u₃, u} D C) ↦
              (Iso.trans (Y := limit (X ⋙ obj (evaluation D C) d))
                  (limitObjIsoLimitCompEvaluation X d : (limit X).obj d ≅ limit (X ⋙ obj (evaluation D C) d))
                  (Iso.trans (Y :=
                      limit
                        (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))
                      (HasLimit.isoOfNatIso (Iso.refl (X ⋙ obj (evaluation D C) d)))
                      (Iso.symm
                        (limitObjIsoLimitCompEvaluation
                          (Functor.flip
                            (obj (whiskeringRight K (Functor.{v₃, v, u₃, u} D C) C) (obj (evaluation D C) d)))
                          X)) :
                    limit (X ⋙ obj (evaluation D C) d) ≅
                      obj
                        (limit
                          (Functor.flip
                            (obj (whiskeringRight K (Functor.{v₃, v, u₃, u} D C) C) (obj (evaluation D C) d))))
                        X) :
                obj (lim ⋙ obj (evaluation D C) d) X ≅
                  obj
                    (limit
                      (Functor.flip (obj (whiskeringRight K (Functor.{v₃, v, u₃, u} D C) C) (obj (evaluation D C) d))))
                    X))
            G))
      (NatTrans.app
        (limit.π (Functor.flip (obj (whiskeringRight K (Functor.{v₃, v, u₃, u} D C) C) (obj (evaluation D C) d))) j) G))
    (CategoryStruct.comp (Y :=
      obj (limit (Functor.flip (obj (whiskeringRight K (Functor.{v₃, v, u₃, u} D C) C) (obj (evaluation D C) d)))) G)
      (Iso.hom
          ((fun (X : K ⥤ Functor.{v₃, v, u₃, u} D C) ↦
              (Iso.trans (Y := limit (X ⋙ obj (evaluation D C) d))
                  (limitObjIsoLimitCompEvaluation X d : (limit X).obj d ≅ limit (X ⋙ obj (evaluation D C) d))
                  (Iso.trans (Y :=
                      limit
                        (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))
                      (HasLimit.isoOfNatIso (Iso.refl (X ⋙ obj (evaluation D C) d)))
                      (Iso.symm
                        (limitObjIsoLimitCompEvaluation
                          (Functor.flip
                            (obj (whiskeringRight K (Functor.{v₃, v, u₃, u} D C) C) (obj (evaluation D C) d)))
                          X)) :
                    limit (X ⋙ obj (evaluation D C) d) ≅
                      obj
                        (limit
                          (Functor.flip
                            (obj (whiskeringRight K (Functor.{v₃, v, u₃, u} D C) C) (obj (evaluation D C) d))))
                        X) :
                obj (lim ⋙ obj (evaluation D C) d) X ≅
                  obj
                    (limit
                      (Functor.flip (obj (whiskeringRight K (Functor.{v₃, v, u₃, u} D C) C) (obj (evaluation D C) d))))
                    X))
            F) ≫
        map (limit (Functor.flip (obj (whiskeringRight K (Functor.{v₃, v, u₃, u} D C) C) (obj (evaluation D C) d)))) η)
      (NatTrans.app
        (limit.π (Functor.flip (obj (whiskeringRight K (Functor.{v₃, v, u₃, u} D C) C) (obj (evaluation D C) d))) j) G))

Tactic:
simp [← NatTrans.comp_app]

Premises used: CategoryTheory.NatTrans.comp_app