-- Mathlib/CategoryTheory/Limits/Preserves/Presheaf.lean
theorem iso_hom [IsFiltered (CostructuredArrow yoneda A)] : (iso A K).hom = limit.post K A

Proof state:
C : Type u
inst✝⁴ : SmallCategory C
inst✝³ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Cᵒᵖ
inst✝ : IsFiltered (CostructuredArrow yoneda A)
⊢ (((((((((((Presheaf.isColimitTautologicalCocone A).coconePointUniqueUpToIso
                              (colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda))).app
                          (limit K)).hom ≫
                      (colimitObjIsoColimitCompEvaluation (CostructuredArrow.proj yoneda A ⋙ yoneda) (limit K)).hom) ≫
                    (HasColimit.isoOfNatIso
                        ((CostructuredArrow.proj yoneda A).associator yoneda
                          ((evaluation Cᵒᵖ (Type u)).obj (limit K)))).hom) ≫
                  (HasColimit.isoOfNatIso (isoAux A K)).hom) ≫
                (HasColimit.isoOfNatIso
                    (preservesLimitIso
                      (coyoneda ⋙
                        (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A))
                      K)).hom) ≫
              (HasColimit.isoOfNatIso (HasLimit.isoOfNatIso (functorToInterchangeIso A K).symm)).hom) ≫
            (colimitLimitIso (functorToInterchange A K)).hom) ≫
          (HasLimit.isoOfNatIso (HasColimit.isoOfNatIso (flipFunctorToInterchange A K))).hom) ≫
        (HasLimit.isoOfNatIso
            (colimitCompWhiskeringLeftIsoCompColimit (CostructuredArrow.proj yoneda A ⋙ yoneda) K)).hom) ≫
      (HasLimit.isoOfNatIso
          (isoWhiskerLeft K
            ((colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda)).coconePointUniqueUpToIso
              (Presheaf.isColimitTautologicalCocone A)))).hom =
    limit.post K A

Tactic:
simp only [Category.assoc]

Result:
C : Type u
inst✝⁴ : SmallCategory C
inst✝³ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Cᵒᵖ
inst✝ : IsFiltered (CostructuredArrow yoneda A)
⊢ (((Presheaf.isColimitTautologicalCocone A).coconePointUniqueUpToIso
              (colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda))).app
          (limit K)).hom ≫
      (colimitObjIsoColimitCompEvaluation (CostructuredArrow.proj yoneda A ⋙ yoneda) (limit K)).hom ≫
        (HasColimit.isoOfNatIso
              ((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K)))).hom ≫
          (HasColimit.isoOfNatIso (isoAux A K)).hom ≫
            (HasColimit.isoOfNatIso
                  (preservesLimitIso
                    (coyoneda ⋙
                      (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A))
                    K)).hom ≫
              (HasColimit.isoOfNatIso (HasLimit.isoOfNatIso (functorToInterchangeIso A K).symm)).hom ≫
                (colimitLimitIso (functorToInterchange A K)).hom ≫
                  (HasLimit.isoOfNatIso (HasColimit.isoOfNatIso (flipFunctorToInterchange A K))).hom ≫
                    (HasLimit.isoOfNatIso
                          (colimitCompWhiskeringLeftIsoCompColimit (CostructuredArrow.proj yoneda A ⋙ yoneda) K)).hom ≫
                      (HasLimit.isoOfNatIso
                          (isoWhiskerLeft K
                            ((colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda)).coconePointUniqueUpToIso
                              (Presheaf.isColimitTautologicalCocone A)))).hom =
    limit.post K A

Proof state:
C : Type u
inst✝⁴ : SmallCategory C
inst✝³ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Cᵒᵖ
inst✝ : IsFiltered (CostructuredArrow yoneda A)
⊢ (((Presheaf.isColimitTautologicalCocone A).coconePointUniqueUpToIso
              (colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda))).app
          (limit K)).hom ≫
      (colimitObjIsoColimitCompEvaluation (CostructuredArrow.proj yoneda A ⋙ yoneda) (limit K)).hom ≫
        (HasColimit.isoOfNatIso
              ((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K)))).hom ≫
          (HasColimit.isoOfNatIso (isoAux A K)).hom ≫
            (HasColimit.isoOfNatIso
                  (preservesLimitIso
                    (coyoneda ⋙
                      (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A))
                    K)).hom ≫
              (HasColimit.isoOfNatIso (HasLimit.isoOfNatIso (functorToInterchangeIso A K).symm)).hom ≫
                (colimitLimitIso (functorToInterchange A K)).hom ≫
                  (HasLimit.isoOfNatIso (HasColimit.isoOfNatIso (flipFunctorToInterchange A K))).hom ≫
                    (HasLimit.isoOfNatIso
                          (colimitCompWhiskeringLeftIsoCompColimit (CostructuredArrow.proj yoneda A ⋙ yoneda) K)).hom ≫
                      (HasLimit.isoOfNatIso
                          (isoWhiskerLeft K
                            ((colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda)).coconePointUniqueUpToIso
                              (Presheaf.isColimitTautologicalCocone A)))).hom =
    limit.post K A

Tactic:
rw [Eq.comm, ← Iso.inv_comp_eq, ← Iso.inv_comp_eq]

Result:
C : Type u
inst✝⁴ : SmallCategory C
inst✝³ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Cᵒᵖ
inst✝ : IsFiltered (CostructuredArrow yoneda A)
⊢ (colimitObjIsoColimitCompEvaluation (CostructuredArrow.proj yoneda A ⋙ yoneda) (limit K)).inv ≫
      (((Presheaf.isColimitTautologicalCocone A).coconePointUniqueUpToIso
                (colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda))).app
            (limit K)).inv ≫
        limit.post K A =
    (HasColimit.isoOfNatIso
          ((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K)))).hom ≫
      (HasColimit.isoOfNatIso (isoAux A K)).hom ≫
        (HasColimit.isoOfNatIso
              (preservesLimitIso
                (coyoneda ⋙
                  (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A))
                K)).hom ≫
          (HasColimit.isoOfNatIso (HasLimit.isoOfNatIso (functorToInterchangeIso A K).symm)).hom ≫
            (colimitLimitIso (functorToInterchange A K)).hom ≫
              (HasLimit.isoOfNatIso (HasColimit.isoOfNatIso (flipFunctorToInterchange A K))).hom ≫
                (HasLimit.isoOfNatIso
                      (colimitCompWhiskeringLeftIsoCompColimit (CostructuredArrow.proj yoneda A ⋙ yoneda) K)).hom ≫
                  (HasLimit.isoOfNatIso
                      (isoWhiskerLeft K
                        ((colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda)).coconePointUniqueUpToIso
                          (Presheaf.isColimitTautologicalCocone A)))).hom