Module: Mathlib.CategoryTheory.Limits.Preserves.Presheaf

Goal state before:
pp: 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 ≫
      colimit.ι (CostructuredArrow.proj yoneda A ⋙ yoneda ⋙ (evaluation Cᵒᵖ (Type u)).obj (limit K)) i ≫
        (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 ≫
                  limit.π (colimit ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙ (whiskeringLeft J Cᵒᵖ (Type u)).obj K))
                      j ≫
                    (colimitCompWhiskeringLeftIsoCompColimit (CostructuredArrow.proj yoneda A ⋙ yoneda) K).hom.app j ≫
                      (K.isoWhiskerLeft
                              ((colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda)).coconePointUniqueUpToIso
                                (Presheaf.isColimitTautologicalCocone A))).hom.app
                        j

Tactic:
HasLimit.isoOfNatIso_hom_π_assoc,

Goal state after:
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 ≫
      colimit.ι (CostructuredArrow.proj yoneda A ⋙ yoneda ⋙ (evaluation Cᵒᵖ (Type u)).obj (limit K)) i ≫
        (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 ≫
                limit.π (colimit (functorToInterchange A K).flip) j ≫
                  (HasColimit.isoOfNatIso (flipFunctorToInterchange A K)).hom.app j ≫
                    (colimitCompWhiskeringLeftIsoCompColimit (CostructuredArrow.proj yoneda A ⋙ yoneda) K).hom.app j ≫
                      (K.isoWhiskerLeft
                              ((colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda)).coconePointUniqueUpToIso
                                (Presheaf.isColimitTautologicalCocone A))).hom.app
                        j