-- 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)
refine :
  ∀ (j : J) (i : CostructuredArrow yoneda A),
    CategoryStruct.comp (Y :=
        colimit (J := CostructuredArrow yoneda A)
          ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙ obj (evaluation Cᵒᵖ (Type u)) (limit K)))
        (colimit.ι ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙ obj (evaluation Cᵒᵖ (Type u)) (limit K)) i :
          obj ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙ obj (evaluation Cᵒᵖ (Type u)) (limit K)) i ⟶
            colimit (J := CostructuredArrow yoneda A)
              ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙ obj (evaluation Cᵒᵖ (Type u)) (limit K)))
        (CategoryStruct.comp (Y := limit (K ⋙ A))
            (CategoryStruct.comp (Y :=
              (colimit (J := CostructuredArrow yoneda A) (CostructuredArrow.proj yoneda A ⋙ yoneda)).obj (limit K))
              (Iso.inv (colimitObjIsoColimitCompEvaluation (CostructuredArrow.proj yoneda A ⋙ yoneda) (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 (limit K))
              (Iso.inv
                    (Iso.app
                      ((Presheaf.isColimitTautologicalCocone A).coconePointUniqueUpToIso
                        (colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda)))
                      (limit K)) ≫
                  limit.post K A :
                (colimit (J := CostructuredArrow yoneda A) (CostructuredArrow.proj yoneda A ⋙ yoneda)).obj (limit K) ⟶
                  limit (K ⋙ A)))
            (limit.π (K ⋙ A) j) :
          colimit (J := CostructuredArrow yoneda A)
              ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙ obj (evaluation Cᵒᵖ (Type u)) (limit K)) ⟶
            (K ⋙ A).obj j) =
      CategoryStruct.comp (Y :=
        colimit (J := CostructuredArrow yoneda A)
          ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙ obj (evaluation Cᵒᵖ (Type u)) (limit K)))
        (colimit.ι ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙ obj (evaluation Cᵒᵖ (Type u)) (limit K)) i)
        (CategoryStruct.comp (Y := limit (K ⋙ A))
          (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))))
          (limit.π (K ⋙ A) j))
⊢ Eq (α :=
    colimit (J := CostructuredArrow yoneda A)
        ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙ obj (evaluation Cᵒᵖ (Type u)) (limit K)) ⟶
      limit (K ⋙ A))
    (CategoryStruct.comp (Y :=
        (colimit (J := CostructuredArrow yoneda A) (CostructuredArrow.proj yoneda A ⋙ yoneda)).obj (limit K))
        (Iso.inv (colimitObjIsoColimitCompEvaluation (CostructuredArrow.proj yoneda A ⋙ yoneda) (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 (limit K))
        (Iso.inv
              (Iso.app
                ((Presheaf.isColimitTautologicalCocone A).coconePointUniqueUpToIso
                  (colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda)))
                (limit K)) ≫
            limit.post K A :
          (colimit (J := CostructuredArrow yoneda A) (CostructuredArrow.proj yoneda A ⋙ yoneda)).obj (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))
    (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))

Tactic:
refine limit.hom_ext (fun j => colimit.hom_ext (fun i => ?_))

Premises used: CategoryTheory.Limits.limit.hom_ext, CategoryTheory.Limits.colimit.hom_ext