-- Module: Mathlib.CategoryTheory.Limits.IndYoneda
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
I : Type v₁
inst_1 : Category.{v₂, v₁} I
D : Functor.{v₂, u₂, v₁, u₁} Iᵒᵖ C
F : C ⥤ Type u₂
inst_2 : HasColimit (D.rightOp ⋙ coyoneda)
inst_3 : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.rightOp ⋙ coyoneda) ⟶ F
i : I
simp :
  Eq (α := (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj (op i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Iso.hom (colimitHomIsoLimitYoneda (D.rightOp ⋙ coyoneda) F) ≫
              CategoryStruct.comp (Y := ((D.rightOp ⋙ coyoneda).op ⋙ Functor.obj yoneda F).obj (op i))
                (limit.π ((D.rightOp ⋙ coyoneda).op ⋙ Functor.obj yoneda F) (op i))
                (NatTrans.app (Iso.hom (Functor.isoWhiskerLeft (D ⋙ Prod.sectL C F) (coyonedaLemma C))) (op i))) :
          (a : colimit (D.rightOp ⋙ coyoneda) ⟶ F) → (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj (op i))
        f :
      (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj (op i))
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj (op i))) :
              (a : (colimit (D.rightOp ⋙ coyoneda)).obj (D.obj (op i))) → F.obj (D.obj (op i)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (NatTrans.app (colimit.ι (D.rightOp ⋙ coyoneda) i) (D.obj (op i))) :
                  (a : D.obj (op i) ⟶ D.obj (op i)) → (colimit (D.rightOp ⋙ coyoneda)).obj (D.obj (op i)))
                (𝟙 (D.obj (op i))) :
              (colimit (D.rightOp ⋙ coyoneda)).obj (D.obj (op i))) } :
      ULift.{u₁, u₂} (F.obj (D.obj (op i))))
⊢ Eq (α := (fun (X : Type (max u₁ u₂)) ↦ X) ((D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj (op i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := limit (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}))
              (Iso.hom (colimitCoyonedaHomIsoLimit D F) :
                (colimit (D.rightOp ⋙ coyoneda) ⟶ F) ⟶ limit (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}))
              (limit.π (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) (op i) :
                limit (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) ⟶ (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj (op i))) :
          (a : (fun (X : Type (max u₁ u₂)) ↦ X) (colimit (D.rightOp ⋙ coyoneda) ⟶ F)) →
            (fun (X : Type (max u₁ u₂)) ↦ X) ((D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj (op i)))
        f :
      (fun (X : Type (max u₁ u₂)) ↦ X) ((D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj (op i)))
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj (op i))) :
              (a : (colimit (D.rightOp ⋙ coyoneda)).obj (D.obj (op i))) → F.obj (D.obj (op i)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (NatTrans.app (colimit.ι (D.rightOp ⋙ coyoneda) i) (D.obj (op i))) :
                  (a : D.obj (op i) ⟶ D.obj (op i)) → (colimit (D.rightOp ⋙ coyoneda)).obj (D.obj (op i)))
                (𝟙 (D.obj (op i))) :
              (colimit (D.rightOp ⋙ coyoneda)).obj (D.obj (op i))) } :
      ULift.{u₁, u₂} (F.obj (D.obj (op i))))

Tactic:
simp only [colimitCoyonedaHomIsoLimit, Iso.trans_hom, Category.assoc,
    HasLimit.isoOfNatIso_hom_π]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.colimitCoyonedaHomIsoLimit, CategoryTheory.Iso.trans_hom, CategoryTheory.Limits.HasLimit.isoOfNatIso_hom_π