-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Presheaf (goal)
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)
⊢ Eq (α := A.obj (limit K) ⟶ limit (K ⋙ A)) (Iso.hom (iso A K) : A.obj (limit K) ⟶ limit (K ⋙ A))
    (limit.post K A : A.obj (limit K) ⟶ limit (K ⋙ A))
have dsimp : 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: dsimp [iso, -Iso.app_hom]