-- Module: Mathlib.CategoryTheory.Limits.Preserves.Presheaf
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst_2 : SmallCategory J
inst_3 : FinCategory J
K : J ⥤ Cᵒᵖ
inst_4 : IsFiltered.{u, u} (CostructuredArrow yoneda A)
simp :
  Eq (α := A.obj (limit K) ⟶ limit (K ⋙ A))
    (CategoryStruct.comp (Y :=
      (colimit (J := CostructuredArrow yoneda A) (CostructuredArrow.proj yoneda A ⋙ yoneda)).obj (limit K))
      (Iso.hom
          (Iso.app
            ((Presheaf.isColimitTautologicalCocone A).coconePointUniqueUpToIso
              (colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda)))
            (limit K)) :
        A.obj (limit K) ⟶
          (colimit (J := CostructuredArrow yoneda A) (CostructuredArrow.proj yoneda A ⋙ yoneda)).obj (limit K))
      (CategoryStruct.comp (Y :=
          colimit (J := CostructuredArrow yoneda A)
            ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙ obj (evaluation Cᵒᵖ (Type u)) (limit K)))
          (Iso.hom (colimitObjIsoColimitCompEvaluation (CostructuredArrow.proj yoneda A ⋙ yoneda) (limit K)) :
            (colimit (J := CostructuredArrow yoneda A) (CostructuredArrow.proj yoneda A ⋙ yoneda)).obj (limit K) ⟶
              colimit (J := CostructuredArrow yoneda A)
                ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙ obj (evaluation Cᵒᵖ (Type u)) (limit K)))
          (CategoryStruct.comp (Y :=
              colimit (J := CostructuredArrow yoneda A)
                (CostructuredArrow.proj yoneda A ⋙ yoneda ⋙ obj (evaluation Cᵒᵖ (Type u)) (limit K)))
              (Iso.hom
                (HasColimit.isoOfNatIso
                  (associator (CostructuredArrow.proj yoneda A) yoneda (obj (evaluation Cᵒᵖ (Type u)) (limit K)))))
              (CategoryStruct.comp (Y :=
                colimit (J := CostructuredArrow yoneda A) (CostructuredArrow.proj yoneda A ⋙ obj coyoneda (limit K)))
                (Iso.hom (HasColimit.isoOfNatIso (isoAux A K)) :
                  colimit (J := CostructuredArrow yoneda A)
                      (CostructuredArrow.proj yoneda A ⋙ yoneda ⋙ obj (evaluation Cᵒᵖ (Type u)) (limit K)) ⟶
                    colimit (J := CostructuredArrow yoneda A)
                      (CostructuredArrow.proj yoneda A ⋙ obj coyoneda (limit K)))
                (CategoryStruct.comp (Y :=
                    colimit (J := CostructuredArrow yoneda A)
                      (limit
                        (K ⋙
                          coyoneda ⋙
                            obj (whiskeringLeft (CostructuredArrow yoneda A) C (Type u))
                              (CostructuredArrow.proj yoneda A))))
                    (Iso.hom
                      (HasColimit.isoOfNatIso
                        (preservesLimitIso
                          (coyoneda ⋙
                            obj (whiskeringLeft (CostructuredArrow yoneda A) C (Type u))
                              (CostructuredArrow.proj yoneda A))
                          K)))
                    (CategoryStruct.comp (Y := colimit (limit (functorToInterchange A K)))
                      (Iso.hom (HasColimit.isoOfNatIso (HasLimit.isoOfNatIso (functorToInterchangeIso A K).symm)) :
                        colimit (J := CostructuredArrow yoneda A)
                            (limit
                              (K ⋙
                                coyoneda ⋙
                                  obj (whiskeringLeft (CostructuredArrow yoneda A) C (Type u))
                                    (CostructuredArrow.proj yoneda A))) ⟶
                          colimit (limit (functorToInterchange A K)))
                      (CategoryStruct.comp (Y := limit (colimit (functorToInterchange A K).flip))
                          (Iso.hom (colimitLimitIso (functorToInterchange A K)) :
                            colimit (limit (functorToInterchange A K)) ⟶
                              limit (colimit (functorToInterchange A K).flip))
                          (CategoryStruct.comp (Y :=
                              limit
                                (colimit (J := CostructuredArrow yoneda A)
                                  ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙ obj (whiskeringLeft J Cᵒᵖ (Type u)) K)))
                              (Iso.hom (HasLimit.isoOfNatIso (HasColimit.isoOfNatIso (flipFunctorToInterchange A K))) :
                                limit (colimit (functorToInterchange A K).flip) ⟶
                                  limit
                                    (colimit (J := CostructuredArrow yoneda A)
                                      ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙
                                        obj (whiskeringLeft J Cᵒᵖ (Type u)) K)))
                              (CategoryStruct.comp (Y :=
                                  limit
                                    (K ⋙
                                      colimit (J := CostructuredArrow yoneda A)
                                        (CostructuredArrow.proj yoneda A ⋙ yoneda)))
                                  (Iso.hom
                                      (HasLimit.isoOfNatIso
                                        (colimitCompWhiskeringLeftIsoCompColimit
                                          (CostructuredArrow.proj yoneda A ⋙ yoneda) K)) :
                                    limit
                                        (colimit (J := CostructuredArrow yoneda A)
                                          ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙
                                            obj (whiskeringLeft J Cᵒᵖ (Type u)) K)) ⟶
                                      limit
                                        (K ⋙
                                          colimit (J := CostructuredArrow yoneda A)
                                            (CostructuredArrow.proj yoneda A ⋙ yoneda)))
                                  (Iso.hom
                                      (HasLimit.isoOfNatIso
                                        (K.isoWhiskerLeft
                                          (IsColimit.coconePointUniqueUpToIso
                                            (colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda))
                                            (Presheaf.isColimitTautologicalCocone A)))) :
                                    limit
                                        (K ⋙
                                          colimit (J := CostructuredArrow yoneda A)
                                            (CostructuredArrow.proj yoneda A ⋙ yoneda)) ⟶
                                      limit (K ⋙ A)) :
                                limit
                                    (colimit (J := CostructuredArrow yoneda A)
                                      ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙
                                        obj (whiskeringLeft J Cᵒᵖ (Type u)) K)) ⟶
                                  limit (K ⋙ A)) :
                            limit (colimit (functorToInterchange A K).flip) ⟶ limit (K ⋙ A)) :
                        colimit (limit (functorToInterchange A K)) ⟶ limit (K ⋙ A))) :
                  colimit (J := CostructuredArrow yoneda A) (CostructuredArrow.proj yoneda A ⋙ obj coyoneda (limit K)) ⟶
                    limit (K ⋙ A))) :
            colimit (J := CostructuredArrow yoneda A)
                ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙ obj (evaluation Cᵒᵖ (Type u)) (limit K)) ⟶
              limit (K ⋙ A)) :
        (colimit (J := CostructuredArrow yoneda A) (CostructuredArrow.proj yoneda A ⋙ yoneda)).obj (limit K) ⟶
          limit (K ⋙ A)))
    (limit.post K A)
⊢ Eq (α := A.obj (limit K) ⟶ limit (K ⋙ A))
    (CategoryStruct.comp (Y :=
      limit (K ⋙ colimit (J := CostructuredArrow yoneda A) (CostructuredArrow.proj yoneda A ⋙ yoneda)))
      (CategoryStruct.comp (Y :=
          limit
            (colimit (J := CostructuredArrow yoneda A)
              ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙ obj (whiskeringLeft J Cᵒᵖ (Type u)) K)))
          (CategoryStruct.comp (Y := limit (colimit (functorToInterchange A K).flip))
              (CategoryStruct.comp (Y := colimit (limit (functorToInterchange A K)))
                  (CategoryStruct.comp (Y :=
                      colimit (J := CostructuredArrow yoneda A)
                        (limit
                          (K ⋙
                            coyoneda ⋙
                              obj (whiskeringLeft (CostructuredArrow yoneda A) C (Type u))
                                (CostructuredArrow.proj yoneda A))))
                      (CategoryStruct.comp (Y :=
                          colimit (J := CostructuredArrow yoneda A)
                            (CostructuredArrow.proj yoneda A ⋙ obj coyoneda (limit K)))
                          (CategoryStruct.comp (Y :=
                              colimit (J := CostructuredArrow yoneda A)
                                (CostructuredArrow.proj yoneda A ⋙ yoneda ⋙ obj (evaluation Cᵒᵖ (Type u)) (limit K)))
                              (CategoryStruct.comp (Y :=
                                colimit (J := CostructuredArrow yoneda A)
                                  ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙
                                    obj (evaluation Cᵒᵖ (Type u)) (limit K)))
                                (CategoryStruct.comp (Y :=
                                    (colimit (J := CostructuredArrow yoneda A)
                                          (CostructuredArrow.proj yoneda A ⋙ yoneda)).obj
                                      (limit K))
                                    (Iso.hom
                                        (Iso.app
                                          ((Presheaf.isColimitTautologicalCocone A).coconePointUniqueUpToIso
                                            (colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda)))
                                          (limit K)) :
                                      A.obj (limit K) ⟶
                                        (colimit (J := CostructuredArrow yoneda A)
                                              (CostructuredArrow.proj yoneda A ⋙ yoneda)).obj
                                          (limit K))
                                    (Iso.hom
                                        (colimitObjIsoColimitCompEvaluation (CostructuredArrow.proj yoneda A ⋙ yoneda)
                                          (limit K)) :
                                      (colimit (J := CostructuredArrow yoneda A)
                                              (CostructuredArrow.proj yoneda A ⋙ yoneda)).obj
                                          (limit K) ⟶
                                        colimit (J := CostructuredArrow yoneda A)
                                          ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙
                                            obj (evaluation Cᵒᵖ (Type u)) (limit K))) :
                                  A.obj (limit K) ⟶
                                    colimit (J := CostructuredArrow yoneda A)
                                      ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙
                                        obj (evaluation Cᵒᵖ (Type u)) (limit K)))
                                (Iso.hom
                                    (HasColimit.isoOfNatIso
                                      (associator (CostructuredArrow.proj yoneda A) yoneda
                                        (obj (evaluation Cᵒᵖ (Type u)) (limit K)))) :
                                  colimit (J := CostructuredArrow yoneda A)
                                      ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙
                                        obj (evaluation Cᵒᵖ (Type u)) (limit K)) ⟶
                                    colimit (J := CostructuredArrow yoneda A)
                                      (CostructuredArrow.proj yoneda A ⋙
                                        yoneda ⋙ obj (evaluation Cᵒᵖ (Type u)) (limit K))))
                              (Iso.hom (HasColimit.isoOfNatIso (isoAux A K))) :
                            A.obj (limit K) ⟶
                              colimit (J := CostructuredArrow yoneda A)
                                (CostructuredArrow.proj yoneda A ⋙ obj coyoneda (limit K)))
                          (Iso.hom
                              (HasColimit.isoOfNatIso
                                (preservesLimitIso
                                  (coyoneda ⋙
                                    obj (whiskeringLeft (CostructuredArrow yoneda A) C (Type u))
                                      (CostructuredArrow.proj yoneda A))
                                  K)) :
                            colimit (J := CostructuredArrow yoneda A)
                                (CostructuredArrow.proj yoneda A ⋙ obj coyoneda (limit K)) ⟶
                              colimit (J := CostructuredArrow yoneda A)
                                (limit
                                  (K ⋙
                                    coyoneda ⋙
                                      obj (whiskeringLeft (CostructuredArrow yoneda A) C (Type u))
                                        (CostructuredArrow.proj yoneda A)))) :
                        A.obj (limit K) ⟶
                          colimit (J := CostructuredArrow yoneda A)
                            (limit
                              (K ⋙
                                coyoneda ⋙
                                  obj (whiskeringLeft (CostructuredArrow yoneda A) C (Type u))
                                    (CostructuredArrow.proj yoneda A))))
                      (Iso.hom (HasColimit.isoOfNatIso (HasLimit.isoOfNatIso (functorToInterchangeIso A K).symm)) :
                        colimit (J := CostructuredArrow yoneda A)
                            (limit
                              (K ⋙
                                coyoneda ⋙
                                  obj (whiskeringLeft (CostructuredArrow yoneda A) C (Type u))
                                    (CostructuredArrow.proj yoneda A))) ⟶
                          colimit (limit (functorToInterchange A K))) :
                    A.obj (limit K) ⟶ colimit (limit (functorToInterchange A K)))
                  (Iso.hom (colimitLimitIso (functorToInterchange A K)) :
                    colimit (limit (functorToInterchange A K)) ⟶ limit (colimit (functorToInterchange A K).flip)) :
                A.obj (limit K) ⟶ limit (colimit (functorToInterchange A K).flip))
              (Iso.hom (HasLimit.isoOfNatIso (HasColimit.isoOfNatIso (flipFunctorToInterchange A K))) :
                limit (colimit (functorToInterchange A K).flip) ⟶
                  limit
                    (colimit (J := CostructuredArrow yoneda A)
                      ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙ obj (whiskeringLeft J Cᵒᵖ (Type u)) K))) :
            A.obj (limit K) ⟶
              limit
                (colimit (J := CostructuredArrow yoneda A)
                  ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙ obj (whiskeringLeft J Cᵒᵖ (Type u)) K)))
          (Iso.hom
              (HasLimit.isoOfNatIso
                (colimitCompWhiskeringLeftIsoCompColimit (CostructuredArrow.proj yoneda A ⋙ yoneda) K)) :
            limit
                (colimit (J := CostructuredArrow yoneda A)
                  ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙ obj (whiskeringLeft J Cᵒᵖ (Type u)) K)) ⟶
              limit (K ⋙ colimit (J := CostructuredArrow yoneda A) (CostructuredArrow.proj yoneda A ⋙ yoneda))) :
        A.obj (limit K) ⟶
          limit (K ⋙ colimit (J := CostructuredArrow yoneda A) (CostructuredArrow.proj yoneda A ⋙ yoneda)))
      (Iso.hom
          (HasLimit.isoOfNatIso
            (K.isoWhiskerLeft
              (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda))
                (Presheaf.isColimitTautologicalCocone A)))) :
        limit (K ⋙ colimit (J := CostructuredArrow yoneda A) (CostructuredArrow.proj yoneda A ⋙ yoneda)) ⟶
          limit (K ⋙ A)))
    (limit.post K A)

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc