Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
I : Type v
inst✝⁴ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
J : Type v
inst✝³ : SmallCategory J
inst✝² : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
K : Type v
inst✝¹ : SmallCategory K
H : K ⥤ Over (colimit F)
inst✝ : IsFiltered K
t : limit ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙ yoneda.obj (colimit H))
t₂ : (fun X ↦ X)
  (limit
    (colimit
      (H ⋙
        yoneda ⋙
          (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj
            (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op)))) :=
  (ConcreteCategory.hom (limMap (compYonedaColimitIsoColimitCompYoneda F G H).hom)) t
t₃ : (fun X ↦ X)
  (colimit
    (limit
      (H ⋙
          yoneda ⋙
            (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj
              (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op)).flip)) :=
  (ConcreteCategory.hom
      (colimitLimitIso
          (H ⋙
              yoneda ⋙
                (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj
                  (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op)).flip).inv)
    t₂
k : K
y :
  (limit
        (H ⋙
            yoneda ⋙
              (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj
                (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op)).flip).obj
    k
z : (fun X ↦ X)
  (limit
    ((H ⋙
          yoneda ⋙
            (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj
              (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op)).flip ⋙
      (evaluation K (Type (max u v))).obj k)) :=
  (ConcreteCategory.hom
      (limitObjIsoLimitCompEvaluation
          (H ⋙
              yoneda ⋙
                (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj
                  (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op)).flip
          k).hom)
    y
⊢ limit ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙ yoneda.obj (H.obj k))

Tactic:
let y := flipCompEvaluation (H ⋙ yoneda ⋙ (whiskeringLeft _ _ _).obj 𝒢) k

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
I : Type v
inst✝⁴ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
J : Type v
inst✝³ : SmallCategory J
inst✝² : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
K : Type v
inst✝¹ : SmallCategory K
H : K ⥤ Over (colimit F)
inst✝ : IsFiltered K
t : limit ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙ yoneda.obj (colimit H))
t₂ : (fun X ↦ X)
  (limit
    (colimit
      (H ⋙
        yoneda ⋙
          (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj
            (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op)))) :=
  (ConcreteCategory.hom (limMap (compYonedaColimitIsoColimitCompYoneda F G H).hom)) t
t₃ : (fun X ↦ X)
  (colimit
    (limit
      (H ⋙
          yoneda ⋙
            (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj
              (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op)).flip)) :=
  (ConcreteCategory.hom
      (colimitLimitIso
          (H ⋙
              yoneda ⋙
                (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj
                  (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op)).flip).inv)
    t₂
k : K
y✝ :
  (limit
        (H ⋙
            yoneda ⋙
              (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj
                (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op)).flip).obj
    k
z : (fun X ↦ X)
  (limit
    ((H ⋙
          yoneda ⋙
            (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj
              (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op)).flip ⋙
      (evaluation K (Type (max u v))).obj k)) :=
  (ConcreteCategory.hom
      (limitObjIsoLimitCompEvaluation
          (H ⋙
              yoneda ⋙
                (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj
                  (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op)).flip
          k).hom)
    y✝
y : (H ⋙
        yoneda ⋙
          (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj
            (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op)).flip ⋙
    (evaluation K (Type (max u v))).obj k ≅
  (H ⋙
        yoneda ⋙
          (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj
            (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op)).obj
    k :=
  flipCompEvaluation
    (H ⋙
      yoneda ⋙
        (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj
          (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op))
    k
⊢ limit ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙ yoneda.obj (H.obj k))