awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Functor.{u₂, u₂, u₁, u₂ + 1} Cᵒᵖ (Type u₂)
inst_2 : HasColimit (D.unop ⋙ yoneda)
inst_3 : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.unop ⋙ yoneda) ⟶ F
i : Iᵒᵖ
dsimp :
  Eq (α := ULift.{u₁, u₂} (F.obj (D.obj i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((↾fun (g : colimit (D.unop ⋙ yoneda) ⟶ F) ↦ colimit.ι (D.unop ⋙ yoneda) (unop i) ≫ g) ≫
              Iso.hom (Equiv.toIso (Equiv.trans yonedaEquiv (Equiv.symm Equiv.ulift)))) :
          (a : colimit (D.unop ⋙ yoneda) ⟶ F) → ULift.{u₁, u₂} (F.obj (D.obj i)))
        f :
      ULift.{u₁, u₂} (F.obj (D.obj i)))
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj i)) :
              (a : (colimit (D.unop ⋙ yoneda)).obj (D.obj i)) → F.obj (D.obj i))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D.unop ⋙ yoneda) (unop i)) (D.obj i)) :
                  (a : unop (D.obj i) ⟶ unop (D.obj i)) → (colimit (D.unop ⋙ yoneda)).obj (D.obj i))
                (𝟙 (unop (D.obj i))) :
              (colimit (D.unop ⋙ yoneda)).obj (D.obj i)) } :
      ULift.{u₁, u₂} (F.obj (D.obj i)))
⊢ Eq (α := (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
    (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (CategoryStruct.comp (Y := ((D.unop ⋙ yoneda).op ⋙ Functor.obj yoneda F).obj i)
                (Functor.map (Functor.obj yoneda F) (Quiver.Hom.op (colimit.ι (D.unop ⋙ yoneda) (unop i))))
                (NatTrans.app (Iso.hom (Functor.isoWhiskerLeft (D ⋙ Prod.sectL Cᵒᵖ F) (yonedaLemma C))) i)) :
            TypeCat.Fun (colimit (D.unop ⋙ yoneda) ⟶ F) ((D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)) :
          (a : colimit (D.unop ⋙ yoneda) ⟶ F) → (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
        f :
      (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj i)) :
              (a : (colimit (D.unop ⋙ yoneda)).obj (D.obj i)) → F.obj (D.obj i))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D.unop ⋙ yoneda) (unop i)) (D.obj i)) :
                  (a : unop (D.obj i) ⟶ unop (D.obj i)) → (colimit (D.unop ⋙ yoneda)).obj (D.obj i))
                (𝟙 (unop (D.obj i))) :
              (colimit (D.unop ⋙ yoneda)).obj (D.obj i)) } :
      ULift.{u₁, u₂} (F.obj (D.obj i)))

Tactic:
dsimp [yonedaLemma]

Premises used: CategoryTheory.yonedaLemma
-- 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 : Functor.{u₂, u₂, u₁, u₂ + 1} Cᵒᵖ (Type u₂)
inst_2 : HasColimit (D.unop ⋙ yoneda)
inst_3 : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.unop ⋙ yoneda) ⟶ F
i : Iᵒᵖ
⊢ Eq (α := ULift.{u₁, u₂} (F.obj (D.obj i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((↾fun (g : colimit (D.unop ⋙ yoneda) ⟶ F) ↦ colimit.ι (D.unop ⋙ yoneda) (unop i) ≫ g) ≫
              Iso.hom (Equiv.toIso (Equiv.trans yonedaEquiv (Equiv.symm Equiv.ulift)))) :
          (a : colimit (D.unop ⋙ yoneda) ⟶ F) → ULift.{u₁, u₂} (F.obj (D.obj i)))
        f :
      ULift.{u₁, u₂} (F.obj (D.obj i)))
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj i)) :
              (a : (colimit (D.unop ⋙ yoneda)).obj (D.obj i)) → F.obj (D.obj i))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D.unop ⋙ yoneda) (unop i)) (D.obj i)) :
                  (a : unop (D.obj i) ⟶ unop (D.obj i)) → (colimit (D.unop ⋙ yoneda)).obj (D.obj i))
                (𝟙 (unop (D.obj i))) :
              (colimit (D.unop ⋙ yoneda)).obj (D.obj i)) } :
      ULift.{u₁, u₂} (F.obj (D.obj i)))

Tactic:
rfl
-- 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 : Functor.{u₂, u₂, u₁, u₂ + 1} Cᵒᵖ (Type u₂)
inst_2 : HasColimit (D ⋙ yoneda)
inst_3 : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D ⋙ yoneda) ⟶ F
i : Iᵒᵖ
⊢ Eq (α := ULift.{u₁, u₂} (F.obj (op (D.obj (unop i)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (D.op ⋙ F ⋙ uliftFunctor.{u₁, u₂}) i) :
          (a : limit (D.op ⋙ F ⋙ uliftFunctor.{u₁, u₂})) → ULift.{u₁, u₂} (F.obj (op (D.obj (unop i)))))
        (((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (colimitYonedaHomIsoLimitOp D F)) :
              TypeCat.Fun (colimit (D ⋙ yoneda) ⟶ F) (limit (D.op ⋙ F ⋙ uliftFunctor.{u₁, u₂}))) :
            (a : colimit (D ⋙ yoneda) ⟶ F) → limit (D.op ⋙ F ⋙ uliftFunctor.{u₁, u₂}))
          f) :
      ULift.{u₁, u₂} (F.obj (op (D.obj (unop i)))))
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (D.obj (unop i)))) :
              (a : (colimit (D ⋙ yoneda)).obj (op (D.obj (unop i)))) → F.obj (op (D.obj (unop i))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (NatTrans.app (colimit.ι (D ⋙ yoneda) (unop i)) (op (D.obj (unop i)))) :
                  (a : D.obj (unop i) ⟶ D.obj (unop i)) → (colimit (D ⋙ yoneda)).obj (op (D.obj (unop i))))
                (𝟙 (D.obj (unop i))) :
              (colimit (D ⋙ yoneda)).obj (op (D.obj (unop i)))) } :
      ULift.{u₁, u₂} (F.obj (op (D.obj (unop i)))))

Tactic:
haveI : HasColimit (D.op.unop ⋙ yoneda) :=
    inferInstanceAs <| HasColimit (D ⋙ yoneda)
  colimitYonedaHomIsoLimit_π_apply _ _ _ _

Premises used: CategoryTheory.Functor.op, Quiver.Hom.unop, CategoryTheory.Limits.colimitYonedaHomIsoLimit_π_apply, CategoryTheory.Functor.unop
-- 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.op ⋙ coyoneda)
inst_3 : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.op ⋙ coyoneda) ⟶ F
i : I
simp :
  Eq (α := (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Iso.hom (colimitHomIsoLimitYoneda' (D.op ⋙ coyoneda) F) ≫
              limit.π ((D.op ⋙ coyoneda).rightOp ⋙ Functor.obj yoneda F) i ≫
                NatTrans.app (Iso.hom (Functor.isoWhiskerLeft (D ⋙ Prod.sectL C F) (coyonedaLemma C))) i) :
          (a : colimit (D.op ⋙ coyoneda) ⟶ F) → (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
        f :
      (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj i)) :
              (a : (colimit (D.op ⋙ coyoneda)).obj (D.obj i)) → F.obj (D.obj i))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D.op ⋙ coyoneda) (op i)) (D.obj i)) :
                  (a : D.obj i ⟶ D.obj i) → (colimit (D.op ⋙ coyoneda)).obj (D.obj i))
                (𝟙 (D.obj i)) :
              (colimit (D.op ⋙ coyoneda)).obj (D.obj i)) } :
      ULift.{u₁, u₂} (F.obj (D.obj i)))
⊢ Eq (α := (fun (X : Type (max u₁ u₂)) ↦ X) ((D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := limit (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}))
              (Iso.hom (colimitCoyonedaHomIsoLimit' D F) :
                (colimit (D.op ⋙ coyoneda) ⟶ F) ⟶ limit (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}))
              (limit.π (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) i :
                limit (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) ⟶ (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)) :
          (a : (fun (X : Type (max u₁ u₂)) ↦ X) (colimit (D.op ⋙ coyoneda) ⟶ F)) →
            (fun (X : Type (max u₁ u₂)) ↦ X) ((D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i))
        f :
      (fun (X : Type (max u₁ u₂)) ↦ X) ((D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i))
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj i)) :
              (a : (colimit (D.op ⋙ coyoneda)).obj (D.obj i)) → F.obj (D.obj i))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D.op ⋙ coyoneda) (op i)) (D.obj i)) :
                  (a : D.obj i ⟶ D.obj i) → (colimit (D.op ⋙ coyoneda)).obj (D.obj i))
                (𝟙 (D.obj i)) :
              (colimit (D.op ⋙ coyoneda)).obj (D.obj i)) } :
      ULift.{u₁, u₂} (F.obj (D.obj 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_π
-- 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.op ⋙ coyoneda)
inst_3 : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.op ⋙ coyoneda) ⟶ F
i : I
rw :
  Eq (α := (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
    (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (CategoryStruct.comp (Y := ((D.op ⋙ coyoneda).rightOp ⋙ Functor.obj yoneda F).obj i)
                (Functor.map (Functor.obj yoneda F) (Quiver.Hom.op (colimit.ι (D.op ⋙ coyoneda) (op i))))
                (NatTrans.app (Iso.hom (Functor.isoWhiskerLeft (D ⋙ Prod.sectL C F) (coyonedaLemma C))) i)) :
            TypeCat.Fun (colimit (D.op ⋙ coyoneda) ⟶ F) ((D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)) :
          (a : colimit (D.op ⋙ coyoneda) ⟶ F) → (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
        f :
      (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj i)) :
              (a : (colimit (D.op ⋙ coyoneda)).obj (D.obj i)) → F.obj (D.obj i))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D.op ⋙ coyoneda) (op i)) (D.obj i)) :
                  (a : D.obj i ⟶ D.obj i) → (colimit (D.op ⋙ coyoneda)).obj (D.obj i))
                (𝟙 (D.obj i)) :
              (colimit (D.op ⋙ coyoneda)).obj (D.obj i)) } :
      ULift.{u₁, u₂} (F.obj (D.obj i)))
⊢ Eq (α := (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Iso.hom (colimitHomIsoLimitYoneda' (D.op ⋙ coyoneda) F) ≫
              limit.π ((D.op ⋙ coyoneda).rightOp ⋙ Functor.obj yoneda F) i ≫
                NatTrans.app (Iso.hom (Functor.isoWhiskerLeft (D ⋙ Prod.sectL C F) (coyonedaLemma C))) i) :
          (a : colimit (D.op ⋙ coyoneda) ⟶ F) → (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
        f :
      (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj i)) :
              (a : (colimit (D.op ⋙ coyoneda)).obj (D.obj i)) → F.obj (D.obj i))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D.op ⋙ coyoneda) (op i)) (D.obj i)) :
                  (a : D.obj i ⟶ D.obj i) → (colimit (D.op ⋙ coyoneda)).obj (D.obj i))
                (𝟙 (D.obj i)) :
              (colimit (D.op ⋙ coyoneda)).obj (D.obj i)) } :
      ULift.{u₁, u₂} (F.obj (D.obj i)))

Tactic:
rw [← Category.assoc, colimitHomIsoLimitYoneda'_hom_comp_π]

Premises used: CategoryTheory.Limits.colimitHomIsoLimitYoneda'_hom_comp_π, CategoryTheory.Category.assoc
-- 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.op ⋙ coyoneda)
inst_3 : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.op ⋙ coyoneda) ⟶ F
i : I
dsimp :
  Eq (α := ULift.{u₁, u₂} (F.obj (D.obj i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((↾fun (g : colimit (D.op ⋙ coyoneda) ⟶ F) ↦ colimit.ι (D.op ⋙ coyoneda) (op i) ≫ g) ≫
              Iso.hom (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)))) :
          (a : colimit (D.op ⋙ coyoneda) ⟶ F) → ULift.{u₁, u₂} (F.obj (D.obj i)))
        f :
      ULift.{u₁, u₂} (F.obj (D.obj i)))
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj i)) :
              (a : (colimit (D.op ⋙ coyoneda)).obj (D.obj i)) → F.obj (D.obj i))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D.op ⋙ coyoneda) (op i)) (D.obj i)) :
                  (a : D.obj i ⟶ D.obj i) → (colimit (D.op ⋙ coyoneda)).obj (D.obj i))
                (𝟙 (D.obj i)) :
              (colimit (D.op ⋙ coyoneda)).obj (D.obj i)) } :
      ULift.{u₁, u₂} (F.obj (D.obj i)))
⊢ Eq (α := (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
    (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (CategoryStruct.comp (Y := ((D.op ⋙ coyoneda).rightOp ⋙ Functor.obj yoneda F).obj i)
                (Functor.map (Functor.obj yoneda F) (Quiver.Hom.op (colimit.ι (D.op ⋙ coyoneda) (op i))))
                (NatTrans.app (Iso.hom (Functor.isoWhiskerLeft (D ⋙ Prod.sectL C F) (coyonedaLemma C))) i)) :
            TypeCat.Fun (colimit (D.op ⋙ coyoneda) ⟶ F) ((D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)) :
          (a : colimit (D.op ⋙ coyoneda) ⟶ F) → (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
        f :
      (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj i)) :
              (a : (colimit (D.op ⋙ coyoneda)).obj (D.obj i)) → F.obj (D.obj i))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D.op ⋙ coyoneda) (op i)) (D.obj i)) :
                  (a : D.obj i ⟶ D.obj i) → (colimit (D.op ⋙ coyoneda)).obj (D.obj i))
                (𝟙 (D.obj i)) :
              (colimit (D.op ⋙ coyoneda)).obj (D.obj i)) } :
      ULift.{u₁, u₂} (F.obj (D.obj i)))

Tactic:
dsimp [coyonedaLemma]

Premises used: CategoryTheory.coyonedaLemma
-- 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.op ⋙ coyoneda)
inst_3 : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.op ⋙ coyoneda) ⟶ F
i : I
⊢ Eq (α := ULift.{u₁, u₂} (F.obj (D.obj i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((↾fun (g : colimit (D.op ⋙ coyoneda) ⟶ F) ↦ colimit.ι (D.op ⋙ coyoneda) (op i) ≫ g) ≫
              Iso.hom (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)))) :
          (a : colimit (D.op ⋙ coyoneda) ⟶ F) → ULift.{u₁, u₂} (F.obj (D.obj i)))
        f :
      ULift.{u₁, u₂} (F.obj (D.obj i)))
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj i)) :
              (a : (colimit (D.op ⋙ coyoneda)).obj (D.obj i)) → F.obj (D.obj i))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D.op ⋙ coyoneda) (op i)) (D.obj i)) :
                  (a : D.obj i ⟶ D.obj i) → (colimit (D.op ⋙ coyoneda)).obj (D.obj i))
                (𝟙 (D.obj i)) :
              (colimit (D.op ⋙ coyoneda)).obj (D.obj i)) } :
      ULift.{u₁, u₂} (F.obj (D.obj i)))

Tactic:
rfl
-- 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 ⋙ coyoneda)
inst_3 : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D ⋙ coyoneda) ⟶ F
i : I
⊢ Eq (α := ULift.{u₁, u₂} (F.obj (unop (D.obj (op i)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (D.unop ⋙ F ⋙ uliftFunctor.{u₁, u₂}) i) :
          (a : limit (D.unop ⋙ F ⋙ uliftFunctor.{u₁, u₂})) → ULift.{u₁, u₂} (F.obj (unop (D.obj (op i)))))
        (((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (colimitCoyonedaHomIsoLimitUnop D F)) :
              TypeCat.Fun (colimit (D ⋙ coyoneda) ⟶ F) (limit (D.unop ⋙ F ⋙ uliftFunctor.{u₁, u₂}))) :
            (a : colimit (D ⋙ coyoneda) ⟶ F) → limit (D.unop ⋙ F ⋙ uliftFunctor.{u₁, u₂}))
          f) :
      ULift.{u₁, u₂} (F.obj (unop (D.obj (op i)))))
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (unop (D.obj (op i)))) :
              (a : (colimit (D ⋙ coyoneda)).obj (unop (D.obj (op i)))) → F.obj (unop (D.obj (op i))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (NatTrans.app (colimit.ι (D ⋙ coyoneda) (op i)) (unop (D.obj (op i)))) :
                  (a : unop (D.obj (op i)) ⟶ unop (D.obj (op i))) → (colimit (D ⋙ coyoneda)).obj (unop (D.obj (op i))))
                (𝟙 (unop (D.obj (op i)))) :
              (colimit (D ⋙ coyoneda)).obj (unop (D.obj (op i)))) } :
      ULift.{u₁, u₂} (F.obj (unop (D.obj (op i)))))

Tactic:
haveI : HasColimit (D.unop.op ⋙ coyoneda) :=
    inferInstanceAs <| HasColimit (D ⋙ coyoneda)
  colimitCoyonedaHomIsoLimit'_π_apply _ _ _ _

Premises used: CategoryTheory.Functor.op, CategoryTheory.Limits.colimitCoyonedaHomIsoLimit'_π_apply, Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.Functor.unop
-- 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 : Functor.{u₂, u₂, u₁, u₂ + 1} Cᵒᵖ (Type u₂)
inst_2 : HasColimit (D.leftOp ⋙ yoneda)
inst_3 : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.leftOp ⋙ yoneda) ⟶ F
i : I
simp :
  Eq (α := (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Iso.hom (colimitHomIsoLimitYoneda' (D.leftOp ⋙ yoneda) F) ≫
              limit.π ((D.leftOp ⋙ yoneda).rightOp ⋙ Functor.obj yoneda F) i ≫
                NatTrans.app (Iso.hom (Functor.isoWhiskerLeft (D ⋙ Prod.sectL Cᵒᵖ F) (yonedaLemma C))) i) :
          (a : colimit (D.leftOp ⋙ yoneda) ⟶ F) → (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
        f :
      (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj i)) :
              (a : (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i)) → F.obj (D.obj i))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D.leftOp ⋙ yoneda) (op i)) (D.obj i)) :
                  (a : unop (D.obj i) ⟶ unop (D.obj i)) → (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i))
                (𝟙 (unop (D.obj i))) :
              (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i)) } :
      ULift.{u₁, u₂} (F.obj (D.obj i)))
⊢ Eq (α := (fun (X : Type (max u₁ u₂)) ↦ X) ((D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := limit (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}))
              (Iso.hom (colimitYonedaHomIsoLimit' D F) :
                (colimit (D.leftOp ⋙ yoneda) ⟶ F) ⟶ limit (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}))
              (limit.π (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) i :
                limit (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) ⟶ (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)) :
          (a : (fun (X : Type (max u₁ u₂)) ↦ X) (colimit (D.leftOp ⋙ yoneda) ⟶ F)) →
            (fun (X : Type (max u₁ u₂)) ↦ X) ((D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i))
        f :
      (fun (X : Type (max u₁ u₂)) ↦ X) ((D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i))
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj i)) :
              (a : (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i)) → F.obj (D.obj i))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D.leftOp ⋙ yoneda) (op i)) (D.obj i)) :
                  (a : unop (D.obj i) ⟶ unop (D.obj i)) → (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i))
                (𝟙 (unop (D.obj i))) :
              (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i)) } :
      ULift.{u₁, u₂} (F.obj (D.obj i)))

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.colimitYonedaHomIsoLimit', CategoryTheory.Iso.trans_hom, CategoryTheory.Limits.HasLimit.isoOfNatIso_hom_π
-- 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 : Functor.{u₂, u₂, u₁, u₂ + 1} Cᵒᵖ (Type u₂)
inst_2 : HasColimit (D.leftOp ⋙ yoneda)
inst_3 : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.leftOp ⋙ yoneda) ⟶ F
i : I
rw :
  Eq (α := (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
    (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (CategoryStruct.comp (Y := ((D.leftOp ⋙ yoneda).rightOp ⋙ Functor.obj yoneda F).obj i)
                (Functor.map (Functor.obj yoneda F) (Quiver.Hom.op (colimit.ι (D.leftOp ⋙ yoneda) (op i))))
                (NatTrans.app (Iso.hom (Functor.isoWhiskerLeft (D ⋙ Prod.sectL Cᵒᵖ F) (yonedaLemma C))) i)) :
            TypeCat.Fun (colimit (D.leftOp ⋙ yoneda) ⟶ F) ((D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)) :
          (a : colimit (D.leftOp ⋙ yoneda) ⟶ F) → (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
        f :
      (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj i)) :
              (a : (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i)) → F.obj (D.obj i))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D.leftOp ⋙ yoneda) (op i)) (D.obj i)) :
                  (a : unop (D.obj i) ⟶ unop (D.obj i)) → (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i))
                (𝟙 (unop (D.obj i))) :
              (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i)) } :
      ULift.{u₁, u₂} (F.obj (D.obj i)))
⊢ Eq (α := (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Iso.hom (colimitHomIsoLimitYoneda' (D.leftOp ⋙ yoneda) F) ≫
              limit.π ((D.leftOp ⋙ yoneda).rightOp ⋙ Functor.obj yoneda F) i ≫
                NatTrans.app (Iso.hom (Functor.isoWhiskerLeft (D ⋙ Prod.sectL Cᵒᵖ F) (yonedaLemma C))) i) :
          (a : colimit (D.leftOp ⋙ yoneda) ⟶ F) → (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
        f :
      (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj i)) :
              (a : (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i)) → F.obj (D.obj i))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D.leftOp ⋙ yoneda) (op i)) (D.obj i)) :
                  (a : unop (D.obj i) ⟶ unop (D.obj i)) → (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i))
                (𝟙 (unop (D.obj i))) :
              (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i)) } :
      ULift.{u₁, u₂} (F.obj (D.obj i)))

Tactic:
rw [← Category.assoc, colimitHomIsoLimitYoneda'_hom_comp_π]

Premises used: CategoryTheory.Limits.colimitHomIsoLimitYoneda'_hom_comp_π, CategoryTheory.Category.assoc