-- 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)
j : J
i : CostructuredArrow yoneda A
⊢ i.hom.app (limit K) ≫ A.map (limit.π K j) =
    ((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K))).hom.app i ≫
      (fun X => 𝟙 (Opposite.unop (limit K) ⟶ X.left)) i ≫
        ((coyoneda ⋙ (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A)).map
                (limit.π K j)).app
            i ≫
          ((functorToInterchangeIso A K).inv.app j).app i ≫
            ((flipFunctorToInterchange A K).hom.app i).app j ≫
              (whiskerLeft K ((Presheaf.tautologicalCocone A).ι.app i)).app j

Tactic:
have := i.hom.naturality (limit.π K j)

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)
j : J
i : CostructuredArrow yoneda A
this :
  (yoneda.obj i.left).map (limit.π K j) ≫ i.hom.app (K.obj j) =
    i.hom.app (limit K) ≫ ((Functor.fromPUnit A).obj i.right).map (limit.π K j)
⊢ i.hom.app (limit K) ≫ A.map (limit.π K j) =
    ((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K))).hom.app i ≫
      (fun X => 𝟙 (Opposite.unop (limit K) ⟶ X.left)) i ≫
        ((coyoneda ⋙ (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A)).map
                (limit.π K j)).app
            i ≫
          ((functorToInterchangeIso A K).inv.app j).app i ≫
            ((flipFunctorToInterchange A K).hom.app i).app j ≫
              (whiskerLeft K ((Presheaf.tautologicalCocone A).ι.app i)).app j

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)
j : J
i : CostructuredArrow yoneda A
this : (yoneda.obj i.left).map (limit.π K j) ≫ i.hom.app (K.obj j) = i.hom.app (limit K) ≫ A.map (limit.π K j)
⊢ (yoneda.obj i.left).map (limit.π K j) ≫ i.hom.app (K.obj j) =
    ((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K))).hom.app i ≫
      (fun X => 𝟙 (Opposite.unop (limit K) ⟶ X.left)) i ≫
        ((coyoneda ⋙ (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A)).map
                (limit.π K j)).app
            i ≫
          ((functorToInterchangeIso A K).inv.app j).app i ≫
            ((flipFunctorToInterchange A K).hom.app i).app j ≫
              (whiskerLeft K ((Presheaf.tautologicalCocone A).ι.app i)).app j

Tactic:
ext

Result:
case h
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)
j : J
i : CostructuredArrow yoneda A
this : (yoneda.obj i.left).map (limit.π K j) ≫ i.hom.app (K.obj j) = i.hom.app (limit K) ≫ A.map (limit.π K j)
a✝ : Opposite.unop (limit K) ⟶ i.left
⊢ ((yoneda.obj i.left).map (limit.π K j) ≫ i.hom.app (K.obj j)) a✝ =
    (((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K))).hom.app i ≫
        (fun X => 𝟙 (Opposite.unop (limit K) ⟶ X.left)) i ≫
          ((coyoneda ⋙
                      (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj
                        (CostructuredArrow.proj yoneda A)).map
                  (limit.π K j)).app
              i ≫
            ((functorToInterchangeIso A K).inv.app j).app i ≫
              ((flipFunctorToInterchange A K).hom.app i).app j ≫
                (whiskerLeft K ((Presheaf.tautologicalCocone A).ι.app i)).app j)
      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)
⊢ (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

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

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)
j : J
i : CostructuredArrow yoneda A
⊢ colimit.ι ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙ (evaluation Cᵒᵖ (Type u)).obj (limit K)) i ≫
      ((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) ≫
        limit.π (K ⋙ A) j =
    colimit.ι ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙ (evaluation Cᵒᵖ (Type u)).obj (limit K)) i ≫
      ((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.π (K ⋙ A) j