awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Ulift
Goal:
J : Type w
inst : Category.{w', w} J
K : Functor.{w', u, w, u + 1} J (Type u)
c : Cone K
hc : IsLimit c
s : (j : J) → (K ⋙ uliftFunctor.{v, u}).obj j
hs : s ∈ (K ⋙ uliftFunctor.{v, u}).sections
x : c.pt
hx₁ :
  ∀ (j : J),
    Eq (α := (fun (X : Type u) ↦ X) (K.obj j))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.π.app j) :
            (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j)) → (fun (X : Type u) ↦ X) (K.obj j))
          x :
        (fun (X : Type u) ↦ X) (K.obj j))
      ((↑(((sectionsEquiv K).symm :
                  (a : (↑(K ⋙ uliftFunctor.{v, u}).sections : Type (max (max u w) v))) → (↑K.sections : Type (max u w)))
                (Subtype.mk (p := fun (x : (j : J) → (K ⋙ uliftFunctor.{v, u}).obj j) ↦
                  x ∈ (K ⋙ uliftFunctor.{v, u}).sections) s ⋯)) :
            (j : J) → K.obj j)
          j :
        K.obj j)
hx₂ :
  ∀ (y : c.pt),
    (fun (x : c.pt) ↦
          ∀ (j : J),
            Eq (α := (fun (X : Type u) ↦ X) (K.obj j))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.π.app j) :
                    (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j)) →
                      (fun (X : Type u) ↦ X) (K.obj j))
                  x :
                (fun (X : Type u) ↦ X) (K.obj j))
              ((↑(((sectionsEquiv K).symm :
                          (a : (↑(K ⋙ uliftFunctor.{v, u}).sections : Type (max (max u w) v))) →
                            (↑K.sections : Type (max u w)))
                        (Subtype.mk (p := fun (x : (j : J) → (K ⋙ uliftFunctor.{v, u}).obj j) ↦
                          x ∈ (K ⋙ uliftFunctor.{v, u}).sections) s ⋯)) :
                    (j : J) → K.obj j)
                  j :
                K.obj j))
        y →
      y = x
⊢ ∃! x : (uliftFunctor.{v, u}.mapCone c).pt,
    ∀ (j : J),
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((uliftFunctor.{v, u}.mapCone c).π.app j) :
            (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const J).obj (uliftFunctor.{v, u}.mapCone c).pt).obj j)) →
              (fun (X : Type (max u v)) ↦ X) ((K ⋙ uliftFunctor.{v, u}).obj j))
          x =
        s j

Tactic:
exact ⟨⟨x⟩, fun i => ULift.ext _ _ (hx₁ i),
          fun y hy => ULift.ext _ _ (hx₂ y.down fun i ↦ ULift.ext_iff.mp (hy i))⟩
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Ulift
Goal:
J_1 : Type u_1
inst : Category.{v_1, u_1} J_1
K : Functor.{v_1, u, u_1, u + 1} J_1 (Type u)
c_1 : Cocone K
hc_1 : IsColimit c_1
lc : Cocone (K ⋙ uliftFunctor.{v, u})
J : Type w
x : Category.{w', w} J
F : Functor.{w', u, w, u + 1} J (Type u)
c : Cocone F
hc : IsColimit c
rw :
  Functor.CoconeTypes.IsColimit (J := J) (F := F ⋙ uliftFunctor.{v, u})
    (((F ⋙ uliftFunctor.{v, u}).coconeTypesEquiv.symm :
        (a : Cocone (F ⋙ uliftFunctor.{v, u})) → (F ⋙ uliftFunctor.{v, u}).CoconeTypes)
      (uliftFunctor.{v, u}.mapCocone c))
⊢ Nonempty (IsColimit (uliftFunctor.{v, u}.mapCocone c))

Tactic:
rw [isColimit_iff_coconeTypesIsColimit]

Premises used: CategoryTheory.Limits.Types.isColimit_iff_coconeTypesIsColimit
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Ulift
Goal:
J_1 : Type u_1
inst : Category.{v_1, u_1} J_1
K : Functor.{v_1, u, u_1, u + 1} J_1 (Type u)
c_1 : Cocone K
hc_1 : IsColimit c_1
lc : Cocone (K ⋙ uliftFunctor.{v, u})
J : Type w
x : Category.{w', w} J
F : Functor.{w', u, w, u + 1} J (Type u)
c : Cocone F
hc : IsColimit c
⊢ Functor.CoconeTypes.IsColimit (J := J) (F := F ⋙ uliftFunctor.{v, u})
    (((F ⋙ uliftFunctor.{v, u}).coconeTypesEquiv.symm :
        (a : Cocone (F ⋙ uliftFunctor.{v, u})) → (F ⋙ uliftFunctor.{v, u}).CoconeTypes)
      (uliftFunctor.{v, u}.mapCocone c))

Tactic:
(((isColimit_iff_coconeTypesIsColimit _).1 ⟨hc⟩).precompose
          (G := F ⋙ uliftFunctor.{v}) (fun _ ↦ Equiv.ulift)
          (fun _ ↦ rfl)).of_equiv Equiv.ulift.symm (fun _ _ ↦ rfl)

Premises used: CategoryTheory.Limits.Types.isColimit_iff_coconeTypesIsColimit, Equiv.ulift, CategoryTheory.Functor.CoconeTypes.IsColimit.precompose, Nonempty.intro, Iff.mp, CategoryTheory.Functor.CoconeTypes.IsColimit.of_equiv, Equiv.symm, rfl
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Ulift
Goal:
J_1 : Type u_1
inst : Category.{v_1, u_1} J_1
K : Functor.{v_1, u, u_1, u + 1} J_1 (Type u)
c_1 : Cocone K
hc_1 : IsColimit c_1
lc : Cocone (K ⋙ uliftFunctor.{v, u})
J : Type w
x : Category.{w', w} J
F : Functor.{w', u, w, u + 1} J (Type u)
c : Cocone F
hc : IsColimit c
⊢ Functor.CoconeTypes.IsColimit (J := J) (F := F ⋙ uliftFunctor.{v, u})
    (((F ⋙ uliftFunctor.{v, u}).coconeTypesEquiv.symm :
        (a : Cocone (F ⋙ uliftFunctor.{v, u})) → (F ⋙ uliftFunctor.{v, u}).CoconeTypes)
      (uliftFunctor.{v, u}.mapCocone c))

Tactic:
exact (((isColimit_iff_coconeTypesIsColimit _).1 ⟨hc⟩).precompose
          (G := F ⋙ uliftFunctor.{v}) (fun _ ↦ Equiv.ulift)
          (fun _ ↦ rfl)).of_equiv Equiv.ulift.symm (fun _ _ ↦ rfl)
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasColimitsOfShape.{v₂, u₂, v₁, v₁ + 1} J (Type v₁)
inst_3 : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
X : C
w :
  ∀ (j : J),
    CategoryStruct.comp (Y := colimit (F ⋙ obj coyoneda (op (obj yoneda X))))
        (colimit.ι (F ⋙ obj coyoneda (op (obj yoneda X))) j)
        (CategoryStruct.comp (Y := colimit (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}))
          (colimMap (F.whiskerLeft (NatTrans.app (Iso.hom largeCurriedYonedaLemma) (op X))) :
            colimit (F ⋙ obj coyoneda (op (obj yoneda X))) ⟶
              colimit (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X) ⋙ uliftFunctor.{u₁, v₁}))
          (CategoryStruct.comp (Y := ULift.{u₁, v₁} (colimit (F.flip.obj (op X))))
              (Iso.inv (preservesColimitIso uliftFunctor.{u₁, v₁} (F.flip.obj (op X))))
              ((↾fun (x : ULift.{u₁, v₁} (colimit (F.flip.obj (op X)))) ↦
                  {
                    down :=
                      ((ConcreteCategory.hom (FC := TypeCat.Fun)
                              (Iso.inv (colimitObjIsoColimitCompEvaluation F (op X))) :
                            TypeCat.Fun (colimit (F.flip.obj (op X))) ((colimit F).obj (op X))) :
                          (a : colimit (F.flip.obj (op X))) → (colimit F).obj (op X))
                        x.down }) ≫
                (yonedaOpCompYonedaObj (colimit F)).inv.app (op X)) :
            colimit (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}) ⟶ obj yoneda X ⟶ colimit F)) =
      CategoryStruct.comp (Y := colimit (F ⋙ obj coyoneda (op (obj yoneda X))))
        (colimit.ι (F ⋙ obj coyoneda (op (obj yoneda X))) j) (colimit.post F (obj coyoneda (op (obj yoneda X))))
⊢ Eq (α := colimit (F ⋙ obj coyoneda (op (obj yoneda X))) ⟶ obj yoneda X ⟶ colimit F)
    (CategoryStruct.comp (Y := colimit (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}))
      (colimMap (F.whiskerLeft (NatTrans.app (Iso.hom largeCurriedYonedaLemma) (op X))) :
        colimit (F ⋙ obj coyoneda (op (obj yoneda X))) ⟶
          colimit (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X) ⋙ uliftFunctor.{u₁, v₁}))
      (CategoryStruct.comp (Y := ULift.{u₁, v₁} (colimit (F.flip.obj (op X))))
          (Iso.inv (preservesColimitIso uliftFunctor.{u₁, v₁} (F.flip.obj (op X))))
          ((↾fun (x : ULift.{u₁, v₁} (colimit (F.flip.obj (op X)))) ↦
              {
                down :=
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (colimitObjIsoColimitCompEvaluation F (op X))) :
                        TypeCat.Fun (colimit (F.flip.obj (op X))) ((colimit F).obj (op X))) :
                      (a : colimit (F.flip.obj (op X))) → (colimit F).obj (op X))
                    x.down }) ≫
            (yonedaOpCompYonedaObj (colimit F)).inv.app (op X)) :
        colimit (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}) ⟶ obj yoneda X ⟶ colimit F))
    (colimit.post F (obj coyoneda (op (obj yoneda X))))

Tactic:
apply colimit.hom_ext

Premises used: CategoryTheory.Limits.colimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasColimitsOfShape.{v₂, u₂, v₁, v₁ + 1} J (Type v₁)
inst_3 : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
X : C
j : J
w :
  Eq (α := (F ⋙ obj coyoneda (op (obj yoneda X))).obj j ⟶ obj yoneda X ⟶ colimit F)
    ((F.whiskerLeft (NatTrans.app (Iso.hom largeCurriedYonedaLemma) (op X))).app j ≫
      CategoryStruct.comp (Y := colimit (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}))
        (colimit.ι (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}) j :
          (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}).obj j ⟶ colimit (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}))
        (CategoryStruct.comp (Y := ULift.{u₁, v₁} (colimit (F.flip.obj (op X))))
            (Iso.inv (preservesColimitIso uliftFunctor.{u₁, v₁} (F.flip.obj (op X))))
            ((↾fun (x : ULift.{u₁, v₁} (colimit (F.flip.obj (op X)))) ↦
                {
                  down :=
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (colimitObjIsoColimitCompEvaluation F (op X))) :
                          TypeCat.Fun (colimit (F.flip.obj (op X))) ((colimit F).obj (op X))) :
                        (a : colimit (F.flip.obj (op X))) → (colimit F).obj (op X))
                      x.down }) ≫
              (yonedaOpCompYonedaObj (colimit F)).inv.app (op X)) :
          colimit (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}) ⟶ obj yoneda X ⟶ colimit F))
    (map (obj coyoneda (op (obj yoneda X))) (colimit.ι F j))
⊢ Eq (α := (F ⋙ obj coyoneda (op (obj yoneda X))).obj j ⟶ obj yoneda X ⟶ colimit F)
    ((F.whiskerLeft (NatTrans.app (Iso.hom largeCurriedYonedaLemma) (op X))).app j ≫
      CategoryStruct.comp (Y := colimit (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X) ⋙ uliftFunctor.{u₁, v₁}))
        (colimit.ι (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X) ⋙ uliftFunctor.{u₁, v₁}) j :
          (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X) ⋙ uliftFunctor.{u₁, v₁}).obj j ⟶
            colimit (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X) ⋙ uliftFunctor.{u₁, v₁}))
        (CategoryStruct.comp (Y := ULift.{u₁, v₁} (colimit (F.flip.obj (op X))))
            (Iso.inv (preservesColimitIso uliftFunctor.{u₁, v₁} (F.flip.obj (op X))))
            ((↾fun (x : ULift.{u₁, v₁} (colimit (F.flip.obj (op X)))) ↦
                {
                  down :=
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (colimitObjIsoColimitCompEvaluation F (op X))) :
                          TypeCat.Fun (colimit (F.flip.obj (op X))) ((colimit F).obj (op X))) :
                        (a : colimit (F.flip.obj (op X))) → (colimit F).obj (op X))
                      x.down }) ≫
              (yonedaOpCompYonedaObj (colimit F)).inv.app (op X)) :
          colimit (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}) ⟶ obj yoneda X ⟶ colimit F))
    (map (obj coyoneda (op (obj yoneda X))) (colimit.ι F j))

Tactic:
simp only [← CategoryTheory.Functor.assoc, comp_evaluation]

Premises used: CategoryTheory.comp_evaluation, CategoryTheory.Functor.assoc
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasColimitsOfShape.{v₂, u₂, v₁, v₁ + 1} J (Type v₁)
inst_3 : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
X : C
j : J
w :
  Eq (α := (F ⋙ obj coyoneda (op (obj yoneda X))).obj j ⟶ obj yoneda X ⟶ colimit F)
    ((F.whiskerLeft (NatTrans.app (Iso.hom largeCurriedYonedaLemma) (op X))).app j ≫
      CategoryStruct.comp (Y := uliftFunctor.{u₁, v₁}.obj (colimit (F.flip.obj (op X))))
        (uliftFunctor.{u₁, v₁}.map (colimit.ι (F.flip.obj (op X)) j))
        ((↾fun (x : ULift.{u₁, v₁} (colimit (F.flip.obj (op X)))) ↦
            {
              down :=
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (colimitObjIsoColimitCompEvaluation F (op X))) :
                      TypeCat.Fun (colimit (F.flip.obj (op X))) ((colimit F).obj (op X))) :
                    (a : colimit (F.flip.obj (op X))) → (colimit F).obj (op X))
                  x.down }) ≫
          (yonedaOpCompYonedaObj (colimit F)).inv.app (op X)))
    (map (obj coyoneda (op (obj yoneda X))) (colimit.ι F j))
⊢ Eq (α := (F ⋙ obj coyoneda (op (obj yoneda X))).obj j ⟶ obj yoneda X ⟶ colimit F)
    ((F.whiskerLeft (NatTrans.app (Iso.hom largeCurriedYonedaLemma) (op X))).app j ≫
      CategoryStruct.comp (Y := colimit (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}))
        (colimit.ι (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}) j :
          (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}).obj j ⟶ colimit (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}))
        (CategoryStruct.comp (Y := ULift.{u₁, v₁} (colimit (F.flip.obj (op X))))
            (Iso.inv (preservesColimitIso uliftFunctor.{u₁, v₁} (F.flip.obj (op X))))
            ((↾fun (x : ULift.{u₁, v₁} (colimit (F.flip.obj (op X)))) ↦
                {
                  down :=
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (colimitObjIsoColimitCompEvaluation F (op X))) :
                          TypeCat.Fun (colimit (F.flip.obj (op X))) ((colimit F).obj (op X))) :
                        (a : colimit (F.flip.obj (op X))) → (colimit F).obj (op X))
                      x.down }) ≫
              (yonedaOpCompYonedaObj (colimit F)).inv.app (op X)) :
          colimit (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}) ⟶ obj yoneda X ⟶ colimit F))
    (map (obj coyoneda (op (obj yoneda X))) (colimit.ι F j))

Tactic:
rw [ι_preservesColimitIso_inv_assoc]

Premises used: CategoryTheory.ι_preservesColimitIso_inv_assoc
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasColimitsOfShape.{v₂, u₂, v₁, v₁ + 1} J (Type v₁)
inst_3 : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
X : C
j : J
w :
  Eq (α := (obj yoneda X ⟶ F.obj j) ⟶ obj yoneda X ⟶ colimit F)
    (NatTrans.app (NatTrans.app (Iso.hom largeCurriedYonedaLemma) (op X)) (F.obj j) ≫
      CategoryStruct.comp (Y := ULift.{u₁, v₁} (colimit (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X))))
        (↾fun (x : ULift.{u₁, v₁} ((F.obj j).obj (op X))) ↦
          {
            down :=
              (ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X)) j) :
                  (a : (F.obj j).obj (op X)) → colimit (F ⋙ (evaluation Cᵒᵖ (Type v₁)).obj (op X)))
                x.down })
        ((↾fun (x : ULift.{u₁, v₁} (colimit (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X)))) ↦
            {
              down :=
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (colimitObjIsoColimitCompEvaluation F (op X))) :
                      TypeCat.Fun (colimit (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X))) ((colimit F).obj (op X))) :
                    (a : colimit (F ⋙ (evaluation Cᵒᵖ (Type v₁)).obj (op X))) → (colimit F).obj (op X))
                  x.down }) ≫
          (yonedaOpCompYonedaObj (colimit F)).inv.app (op X)))
    (↾fun (g : obj yoneda X ⟶ F.obj j) ↦ g ≫ colimit.ι F j)
⊢ Eq (α := (F ⋙ obj coyoneda (op (obj yoneda X))).obj j ⟶ obj yoneda X ⟶ colimit F)
    ((F.whiskerLeft (NatTrans.app (Iso.hom largeCurriedYonedaLemma) (op X))).app j ≫
      CategoryStruct.comp (Y := uliftFunctor.{u₁, v₁}.obj (colimit (F.flip.obj (op X))))
        (uliftFunctor.{u₁, v₁}.map (colimit.ι (F.flip.obj (op X)) j))
        ((↾fun (x : ULift.{u₁, v₁} (colimit (F.flip.obj (op X)))) ↦
            {
              down :=
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (colimitObjIsoColimitCompEvaluation F (op X))) :
                      TypeCat.Fun (colimit (F.flip.obj (op X))) ((colimit F).obj (op X))) :
                    (a : colimit (F.flip.obj (op X))) → (colimit F).obj (op X))
                  x.down }) ≫
          (yonedaOpCompYonedaObj (colimit F)).inv.app (op X)))
    (map (obj coyoneda (op (obj yoneda X))) (colimit.ι F j))

Tactic:
simp only [← comp_evaluation, comp_obj, evaluation_obj_obj, yoneda_obj_obj, uliftFunctor_obj,
    whiskerLeft_app, uliftFunctor_map, Functor.comp_map, evaluation_obj_map, yoneda_map_app]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.yoneda_map_app, CategoryTheory.comp_evaluation, CategoryTheory.evaluation_obj_map, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.yoneda_obj_obj, CategoryTheory.evaluation_obj_obj, CategoryTheory.uliftFunctor_map, CategoryTheory.uliftFunctor_obj, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasColimitsOfShape.{v₂, u₂, v₁, v₁ + 1} J (Type v₁)
inst_3 : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
X : C
j : J
η : obj yoneda X ⟶ F.obj j
Y : Cᵒᵖ
f : obj (obj yoneda X) Y
w :
  Eq (α := (colimit F).obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((↾fun (g : X ⟶ X) ↦ f ≫ g) ≫ η.app Y ≫ NatTrans.app (colimit.ι F j) Y) :
          (a : X ⟶ X) → (colimit F).obj Y)
        (𝟙 X) :
      (colimit F).obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app Y ≫ NatTrans.app (colimit.ι F j) Y) :
          (a : unop Y ⟶ X) → (colimit F).obj Y)
        f :
      (colimit F).obj Y)
⊢ Eq (α := (colimit F).obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((colimit F).map (Quiver.Hom.op f)) :
          (a : (colimit F).obj (op X)) → (colimit F).obj Y)
        (((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (colimitObjIsoColimitCompEvaluation F (op X))) :
                TypeCat.Fun (colimit (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X))) ((colimit F).obj (op X))) :
              (a : colimit (F ⋙ (evaluation Cᵒᵖ (Type v₁)).obj (op X))) → (colimit F).obj (op X))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X)) j) :
                  (a : (F.obj j).obj (op X)) → colimit (F ⋙ (evaluation Cᵒᵖ (Type v₁)).obj (op X)))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app (op X)) : (a : X ⟶ X) → (F.obj j).obj (op X)) (𝟙 X) :
                  (F.obj j).obj (op X)) :
              colimit (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X))) :
          (colimit F).obj (op X)) :
      (colimit F).obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι F j) Y) :
          (a : (F.obj j).obj Y) → (colimit F).obj Y)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app Y) : (a : unop Y ⟶ X) → (F.obj j).obj Y) f :
          (F.obj j).obj Y) :
      (colimit F).obj Y)

Tactic:
simp only [← comp_apply, Category.assoc, colimitObjIsoColimitCompEvaluation_ι_inv,
    ← NatTrans.naturality, ← NatTrans.naturality_assoc, yoneda_obj_obj, yoneda_obj_map,
    Quiver.Hom.unop_op]

Premises used: CategoryTheory.Category.assoc, Quiver.Hom.unop_op, CategoryTheory.yoneda_obj_obj, CategoryTheory.yoneda_obj_map, CategoryTheory.comp_apply, CategoryTheory.NatTrans.naturality, CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation_ι_inv, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasColimitsOfShape.{v₂, u₂, v₁, v₁ + 1} J (Type v₁)
inst_3 : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
X : C
j : J
η : obj yoneda X ⟶ F.obj j
Y : Cᵒᵖ
f : obj (obj yoneda X) Y
⊢ Eq (α := (colimit F).obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((↾fun (g : X ⟶ X) ↦ f ≫ g) ≫ η.app Y ≫ NatTrans.app (colimit.ι F j) Y) :
          (a : X ⟶ X) → (colimit F).obj Y)
        (𝟙 X) :
      (colimit F).obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app Y ≫ NatTrans.app (colimit.ι F j) Y) :
          (a : unop Y ⟶ X) → (colimit F).obj Y)
        f :
      (colimit F).obj Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasColimitsOfShape.{v₂, u₂, v₁, v₁ + 1} J (Type v₁)
inst_3 : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
X : C
suffices :
  IsIso (X := colimit (F ⋙ obj coyoneda (op (obj yoneda X)))) (Y := obj (obj coyoneda (op (obj yoneda X))) (colimit F))
    (colimit.post F (obj coyoneda (op (obj yoneda X))))
⊢ PreservesColimit F (obj coyoneda (op (obj yoneda X)))

Tactic:
suffices IsIso (colimit.post F (coyoneda.obj (op (yoneda.obj X)))) from
    preservesColimit_of_isIso_post _ _
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
E : ℰ
X Y : C
f : X ⟶ Y
g : Functor.obj uliftYoneda.{max w v₂, v₁, u₁} Y ⟶ (restrictedULiftYoneda A).obj E
⊢ Eq (α := ((restrictedULiftYoneda A).obj E).obj (op X))
    ((hom (FC := TypeCat.Fun) (g.app (op X)) :
          (a : (uliftYoneda.{max w v₂, v₁, u₁}.obj Y).obj (op X)) → ((restrictedULiftYoneda A).obj E).obj (op X))
        ((hom (FC := TypeCat.Fun) (Functor.map (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} Y) f.op) :
            (a : (uliftYoneda.{max w v₂, v₁, u₁}.obj Y).obj (op Y)) → (uliftYoneda.{max w v₂, v₁, u₁}.obj Y).obj (op X))
          { down := 𝟙 Y }) :
      ((restrictedULiftYoneda A).obj E).obj (op X))
    ((hom (FC := TypeCat.Fun) (((restrictedULiftYoneda A).obj E).map f.op) :
          (a : ((restrictedULiftYoneda A).obj E).obj (op Y)) → ((restrictedULiftYoneda A).obj E).obj (op X))
        ((hom (FC := TypeCat.Fun) (g.app (op Y)) :
            (a : (uliftYoneda.{max w v₂, v₁, u₁}.obj Y).obj (op Y)) → ((restrictedULiftYoneda A).obj E).obj (op Y))
          { down := 𝟙 Y }) :
      ((restrictedULiftYoneda A).obj E).obj (op X))

Tactic:
have this := (g.naturality_apply f.op) (ULift.up (𝟙 Y))
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
E : ℰ
X Y : C
f : X ⟶ Y
g : Functor.obj uliftYoneda.{max w v₂, v₁, u₁} Y ⟶ (restrictedULiftYoneda A).obj E
this :
  Eq (α := ((restrictedULiftYoneda A).obj E).obj (op X))
    ((hom (FC := TypeCat.Fun) (g.app (op X)) :
          (a : (uliftYoneda.{max w v₂, v₁, u₁}.obj Y).obj (op X)) → ((restrictedULiftYoneda A).obj E).obj (op X))
        ((hom (FC := TypeCat.Fun) (Functor.map (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} Y) f.op) :
            (a : (uliftYoneda.{max w v₂, v₁, u₁}.obj Y).obj (op Y)) → (uliftYoneda.{max w v₂, v₁, u₁}.obj Y).obj (op X))
          { down := 𝟙 Y }) :
      ((restrictedULiftYoneda A).obj E).obj (op X))
    ((hom (FC := TypeCat.Fun) (((restrictedULiftYoneda A).obj E).map f.op) :
          (a : ((restrictedULiftYoneda A).obj E).obj (op Y)) → ((restrictedULiftYoneda A).obj E).obj (op X))
        ((hom (FC := TypeCat.Fun) (g.app (op Y)) :
            (a : (uliftYoneda.{max w v₂, v₁, u₁}.obj Y).obj (op Y)) → ((restrictedULiftYoneda A).obj E).obj (op Y))
          { down := 𝟙 Y }) :
      ((restrictedULiftYoneda A).obj E).obj (op X))
dsimp :
  Eq (α := A.obj X ⟶ E)
    (A.map f ≫
      ULift.down
        ((hom (FC := TypeCat.Fun) (g.app (op Y)) :
            (a : ULift.{max v₂ w, v₁} (Y ⟶ Y)) → ((restrictedULiftYoneda A).obj E).obj (op Y))
          { down := 𝟙 Y }))
    (ULift.down
      ((hom (FC := TypeCat.Fun) (g.app (op X)) :
          (a : ULift.{max v₂ w, v₁} (X ⟶ Y)) → ((restrictedULiftYoneda A).obj E).obj (op X))
        { down := 𝟙 X ≫ f }))
⊢ Eq (α := A.obj X ⟶ E)
    (A.map f ≫
      ULift.down
        ((uliftYonedaEquiv :
            (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj Y ⟶ (restrictedULiftYoneda A).obj E) →
              ((restrictedULiftYoneda A).obj E).obj (op Y))
          g))
    (ULift.down
      ((uliftYonedaEquiv :
          (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ (restrictedULiftYoneda A).obj E) →
            ((restrictedULiftYoneda A).obj E).obj (op X))
        (Functor.map uliftYoneda.{max v₂ w, v₁, u₁} f ≫ g)))

Tactic:
dsimp [uliftYonedaEquiv, uliftYoneda] at this ⊢

Premises used: CategoryTheory.uliftYoneda, CategoryTheory.uliftYonedaEquiv