-- 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)
j : J
i : CostructuredArrow yoneda A
rw :
  Eq (α := obj ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙ obj (evaluation Cᵒᵖ (Type u)) (limit K)) i ⟶ (K ⋙ A).obj j)
    (i.hom.app (limit K) ≫ A.map (limit.π K j))
    (NatTrans.app
        (Iso.hom (associator (CostructuredArrow.proj yoneda A) yoneda (obj (evaluation Cᵒᵖ (Type u)) (limit K)))) i ≫
      CategoryStruct.comp (Y := obj (CostructuredArrow.proj yoneda A ⋙ obj coyoneda (limit K)) i)
        ((fun (X : CostructuredArrow yoneda A) ↦
            (𝟙 (Opposite.unop (limit K) ⟶ X.left) :
              (Opposite.unop (limit K) ⟶ X.left) ⟶ Opposite.unop (limit K) ⟶ X.left))
          i)
        (NatTrans.app
            (Functor.map
              (coyoneda ⋙
                obj (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)) (CostructuredArrow.proj yoneda A))
              (limit.π K j))
            i ≫
          ((functorToInterchangeIso A K).inv.app j).app i ≫
            ((flipFunctorToInterchange A K).hom.app i).app j ≫
              (K.whiskerLeft ((Presheaf.tautologicalCocone A).ι.app i)).app 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 :
        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 :=
          (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)) ≫
              CategoryStruct.comp (Y := limit (K ⋙ A)) (limit.post K A) (limit.π (K ⋙ A) j) :
            (colimit (J := CostructuredArrow yoneda A) (CostructuredArrow.proj yoneda A ⋙ yoneda)).obj (limit K) ⟶
              (K ⋙ A).obj 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 :=
        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)))
                            (CategoryStruct.comp (Y := limit (K ⋙ A))
                                (Iso.hom
                                  (HasLimit.isoOfNatIso
                                    (K.isoWhiskerLeft
                                      (IsColimit.coconePointUniqueUpToIso
                                        (colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda))
                                        (Presheaf.isColimitTautologicalCocone A)))))
                                (limit.π (K ⋙ A) j) :
                              limit
                                  (K ⋙
                                    colimit (J := CostructuredArrow yoneda A)
                                      (CostructuredArrow.proj yoneda A ⋙ yoneda)) ⟶
                                (K ⋙ A).obj j) :
                          limit
                              (colimit (J := CostructuredArrow yoneda A)
                                ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙ obj (whiskeringLeft J Cᵒᵖ (Type u)) K)) ⟶
                            (K ⋙ A).obj j) :
                      limit (colimit (functorToInterchange A K).flip) ⟶ (K ⋙ A).obj j) :
                  colimit (limit (functorToInterchange A K)) ⟶ (K ⋙ A).obj j)) :
            colimit (J := CostructuredArrow yoneda A) (CostructuredArrow.proj yoneda A ⋙ obj coyoneda (limit K)) ⟶
              (K ⋙ A).obj j)))

Tactic:
rw [HasLimit.isoOfNatIso_hom_π, HasLimit.isoOfNatIso_hom_π_assoc, limit.post_π,
    colimitObjIsoColimitCompEvaluation_ι_inv_assoc (CostructuredArrow.proj yoneda A ⋙ yoneda),
    Iso.app_inv, ← NatTrans.comp_app_assoc, colimit.comp_coconePointUniqueUpToIso_inv,
    Presheaf.tautologicalCocone_ι_app, HasColimit.isoOfNatIso_ι_hom_assoc,
    HasLimit.isoOfNatIso_hom_π_assoc, HasColimit.isoOfNatIso_ι_hom_assoc,
    HasColimit.isoOfNatIso_ι_hom_assoc, HasColimit.isoOfNatIso_ι_hom_assoc,
    ι_colimitLimitIso_limit_π_assoc, isoAux_hom_app, ← NatTrans.comp_app_assoc,
    ← NatTrans.comp_app_assoc, Category.assoc, HasLimit.isoOfNatIso_hom_π,
    preservesLimitIso_hom_π_assoc, Iso.symm_hom,
    ← NatTrans.comp_app_assoc, HasColimit.isoOfNatIso_ι_hom,
    ← NatTrans.comp_app_assoc, Category.assoc,
    ι_colimitCompWhiskeringLeftIsoCompColimit_hom,
    NatTrans.comp_app, Category.assoc, isoWhiskerLeft_hom, NatTrans.comp_app, Category.assoc,
    ← NatTrans.comp_app, ← whiskerLeft_comp, colimit.comp_coconePointUniqueUpToIso_hom]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.app_inv, CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation_ι_inv_assoc, CategoryTheory.NatTrans.comp_app_assoc, CategoryTheory.Limits.limit.post_π, CategoryTheory.Functor.comp, CategoryTheory.Iso.symm_hom, CategoryTheory.yoneda, CategoryTheory.Limits.ι_colimitCompWhiskeringLeftIsoCompColimit_hom, CategoryTheory.Functor.whiskerLeft_comp, CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isoAux_hom_app, CategoryTheory.Limits.ι_colimitLimitIso_limit_π_assoc, CategoryTheory.Limits.HasLimit.isoOfNatIso_hom_π_assoc, CategoryTheory.preservesLimitIso_hom_π_assoc, CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_hom_assoc, CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_hom, CategoryTheory.Presheaf.tautologicalCocone_ι_app, CategoryTheory.NatTrans.comp_app, CategoryTheory.Limits.HasLimit.isoOfNatIso_hom_π, CategoryTheory.Functor.isoWhiskerLeft_hom, CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv, CategoryTheory.CostructuredArrow.proj