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

Proof state:
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✝

Tactic:
simp

Result:
no goals

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)
⊢ (iso A K).hom = limit.post K A

Tactic:
dsimp [iso, -Iso.app_hom]

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)
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)
⊢ 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:
rw [← this]

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) ≫ 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