awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} C (Type w)
X : C
x :
  CoconeTypes.pt (J := F.Elementsᵒᵖ) (F := (CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X)
    ((((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X).coconeTypesEquiv.symm :
        (a : Cocone ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X)) →
          ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).CoconeTypes)
      (coconeπOpCompShrinkYonedaObj F X))
⊢ ∃ (a : ((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X).ColimitType),
    ((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X).descColimitType
        ((((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X).coconeTypesEquiv.symm :
            (a : Cocone ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X)) →
              ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).CoconeTypes)
          (coconeπOpCompShrinkYonedaObj F X))
        a =
      x

Tactic:
exact ⟨Functor.ιColimitType _ (op (elementsMk _ _ x))
      (shrinkYonedaObjObjEquiv.symm (𝟙 X)), by simp⟩
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} C (Type w)
X₁ X₂ : C
f : X₁ ⟶ X₂
u : F.Elements
h :
  ∀ (g : obj.{v₁, w, u₁, w + 1} (obj shrinkYoneda.{w, v₁, u₁} X₁) (op (u.fst (β := fun (c : C) ↦ F.obj c)))),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app (map shrinkYoneda.{w, v₁, u₁} f) (op (u.fst (β := fun (c : C) ↦ F.obj c))) ≫
            ↾fun
                (t :
                  obj.{v₁, w, u₁, w + 1} (obj shrinkYoneda.{w, v₁, u₁} X₂) (op (u.fst (β := fun (c : C) ↦ F.obj c)))) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun)
                    (F.map
                      ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X₂).obj (op u.fst)) → u.fst ⟶ X₂)
                        t)) :
                  (a : F.obj u.fst) → F.obj X₂)
                (u.snd (β := fun (c : C) ↦ F.obj c))))
        g =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((↾fun
                (t :
                  obj.{v₁, w, u₁, w + 1} (obj shrinkYoneda.{w, v₁, u₁} X₁) (op (u.fst (β := fun (c : C) ↦ F.obj c)))) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun)
                    (F.map
                      ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X₁).obj (op u.fst)) → u.fst ⟶ X₁)
                        t)) :
                  (a : F.obj u.fst) → F.obj X₁)
                (u.snd (β := fun (c : C) ↦ F.obj c))) ≫
            F.map f))
        g
⊢ Eq (α :=
    obj.{v₁, w, u₁, w + 1} (obj shrinkYoneda.{w, v₁, u₁} X₁) (op (u.fst (β := fun (c : C) ↦ F.obj c))) ⟶ F.obj X₂)
    (NatTrans.app (map shrinkYoneda.{w, v₁, u₁} f) (op (u.fst (β := fun (c : C) ↦ F.obj c))) ≫
      ↾fun (t : obj.{v₁, w, u₁, w + 1} (obj shrinkYoneda.{w, v₁, u₁} X₂) (op (u.fst (β := fun (c : C) ↦ F.obj c)))) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun)
              (F.map
                ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X₂).obj (op u.fst)) → u.fst ⟶ X₂) t)) :
            (a : F.obj u.fst) → F.obj X₂)
          (u.snd (β := fun (c : C) ↦ F.obj c)))
    ((↾fun (t : obj.{v₁, w, u₁, w + 1} (obj shrinkYoneda.{w, v₁, u₁} X₁) (op (u.fst (β := fun (c : C) ↦ F.obj c)))) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun)
              (F.map
                ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X₁).obj (op u.fst)) → u.fst ⟶ X₁) t)) :
            (a : F.obj u.fst) → F.obj X₁)
          (u.snd (β := fun (c : C) ↦ F.obj c))) ≫
      F.map f)

Tactic:
ext g
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} C (Type w)
X₁ X₂ : C
f : X₁ ⟶ X₂
u : F.Elements
g : unop (op (u.fst (β := fun (c : C) ↦ F.obj c))) ⟶ X₁
⊢ TypeCat.Fun.toFun (X :=
      obj.{v₁, w, u₁, w + 1} (obj shrinkYoneda.{w, v₁, u₁} X₁) (op (u.fst (β := fun (c : C) ↦ F.obj c))))
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app (map shrinkYoneda.{w, v₁, u₁} f) (op (u.fst (β := fun (c : C) ↦ F.obj c))) ≫
          ↾fun
              (t : obj.{v₁, w, u₁, w + 1} (obj shrinkYoneda.{w, v₁, u₁} X₂) (op (u.fst (β := fun (c : C) ↦ F.obj c)))) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (F.map
                    ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X₂).obj (op u.fst)) → u.fst ⟶ X₂)
                      t)) :
                (a : F.obj u.fst) → F.obj X₂)
              (u.snd (β := fun (c : C) ↦ F.obj c))))
      ((Equiv.symm shrinkYonedaObjObjEquiv :
          (a : unop (op u.fst) ⟶ X₁) → (shrinkYoneda.{w, v₁, u₁}.obj X₁).obj (op u.fst))
        g) =
    TypeCat.Fun.toFun (X :=
      obj.{v₁, w, u₁, w + 1} (obj shrinkYoneda.{w, v₁, u₁} X₁) (op (u.fst (β := fun (c : C) ↦ F.obj c))))
      (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((↾fun
                (t :
                  obj.{v₁, w, u₁, w + 1} (obj shrinkYoneda.{w, v₁, u₁} X₁) (op (u.fst (β := fun (c : C) ↦ F.obj c)))) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun)
                    (F.map
                      ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X₁).obj (op u.fst)) → u.fst ⟶ X₁)
                        t)) :
                  (a : F.obj u.fst) → F.obj X₁)
                (u.snd (β := fun (c : C) ↦ F.obj c))) ≫
            F.map f) :
        TypeCat.Fun (obj.{v₁, w, u₁, w + 1} (obj shrinkYoneda.{w, v₁, u₁} X₁) (op (u.fst (β := fun (c : C) ↦ F.obj c))))
          (F.obj X₂))
      ((Equiv.symm shrinkYonedaObjObjEquiv :
            (a : unop (op u.fst) ⟶ X₁) → (shrinkYoneda.{w, v₁, u₁}.obj X₁).obj (op u.fst))
          g :
        obj.{v₁, w, u₁, w + 1} (obj shrinkYoneda.{w, v₁, u₁} X₁) (op (u.fst (β := fun (c : C) ↦ F.obj c))))

Tactic:
simp [shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm.{w}]
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} C (Type w)
u : F.Elementsᵒᵖ
X Y : C
f : X ⟶ Y
h :
  ∀ (x : (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).obj X),
    Eq (α := (obj (obj (const F.Elementsᵒᵖ) F) u).obj Y)
      (TypeCat.Fun.toFun
          (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            ((((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).map f ≫
              NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F Y)) u))
          x :
        (obj (obj (const F.Elementsᵒᵖ) F) u).obj Y)
      (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F X)) u ≫ (obj (obj (const F.Elementsᵒᵖ) F) u).map f))
          x :
        (obj (obj (const F.Elementsᵒᵖ) F) u).obj Y)
⊢ Eq (α :=
    (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).obj X ⟶
      (obj (obj (const F.Elementsᵒᵖ) F) u).obj Y)
    ((((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).map f ≫
        NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F Y)) u :
      (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).obj X ⟶
        (obj (obj (const F.Elementsᵒᵖ) F) u).obj Y)
    (NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F X)) u ≫ (obj (obj (const F.Elementsᵒᵖ) F) u).map f :
      (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).obj X ⟶
        (obj (obj (const F.Elementsᵒᵖ) F) u).obj Y)

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} C (Type w)
u : F.Elementsᵒᵖ
X Y : C
f : X ⟶ Y
x : (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).obj X
h :
  ∀ (x : unop ((CategoryOfElements.π F).op.obj u) ⟶ X),
    Eq (α := (obj (obj (const F.Elementsᵒᵖ) F) u).obj Y)
      (TypeCat.Fun.toFun (X := (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).obj X)
          (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              ((((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).map f ≫
                NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F Y)) u) :
            TypeCat.Fun ((((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).obj X)
              ((obj (obj (const F.Elementsᵒᵖ) F) u).obj Y))
          ((Equiv.symm shrinkYonedaObjObjEquiv :
                (a : unop ((CategoryOfElements.π F).op.obj u) ⟶ X) →
                  (shrinkYoneda.{w, v₁, u₁}.obj X).obj ((CategoryOfElements.π F).op.obj u))
              x :
            obj.{v₁, w, u₁, w + 1} (obj shrinkYoneda.{w, v₁, u₁} X) ((CategoryOfElements.π F).op.obj u)) :
        (obj (obj (const F.Elementsᵒᵖ) F) u).obj Y)
      (TypeCat.Fun.toFun (X := (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).obj X)
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F X)) u ≫ (obj (obj (const F.Elementsᵒᵖ) F) u).map f))
          ((Equiv.symm shrinkYonedaObjObjEquiv :
              (a : unop ((CategoryOfElements.π F).op.obj u) ⟶ X) →
                (shrinkYoneda.{w, v₁, u₁}.obj X).obj ((CategoryOfElements.π F).op.obj u))
            x) :
        (obj (obj (const F.Elementsᵒᵖ) F) u).obj Y)
⊢ Eq (α := (obj (obj (const F.Elementsᵒᵖ) F) u).obj Y)
    (TypeCat.Fun.toFun
        (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          ((((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).map f ≫
            NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F Y)) u))
        x :
      (obj (obj (const F.Elementsᵒᵖ) F) u).obj Y)
    (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F X)) u ≫ (obj (obj (const F.Elementsᵒᵖ) F) u).map f))
        x :
      (obj (obj (const F.Elementsᵒᵖ) F) u).obj Y)

Tactic:
obtain ⟨x, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective x

Premises used: CategoryTheory.shrinkYonedaObjObjEquiv, Equiv.surjective, Equiv.symm, rfl
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} C (Type w)
u : F.Elementsᵒᵖ
X Y : C
f : X ⟶ Y
x : unop ((CategoryOfElements.π F).op.obj u) ⟶ X
⊢ Eq (α := (obj (obj (const F.Elementsᵒᵖ) F) u).obj Y)
    (TypeCat.Fun.toFun (X := (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).obj X)
        (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            ((((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).map f ≫
              NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F Y)) u) :
          TypeCat.Fun ((((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).obj X)
            ((obj (obj (const F.Elementsᵒᵖ) F) u).obj Y))
        ((Equiv.symm shrinkYonedaObjObjEquiv :
              (a : unop ((CategoryOfElements.π F).op.obj u) ⟶ X) →
                (shrinkYoneda.{w, v₁, u₁}.obj X).obj ((CategoryOfElements.π F).op.obj u))
            x :
          obj.{v₁, w, u₁, w + 1} (obj shrinkYoneda.{w, v₁, u₁} X) ((CategoryOfElements.π F).op.obj u)) :
      (obj (obj (const F.Elementsᵒᵖ) F) u).obj Y)
    (TypeCat.Fun.toFun (X := (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).obj X)
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F X)) u ≫ (obj (obj (const F.Elementsᵒᵖ) F) u).map f))
        ((Equiv.symm shrinkYonedaObjObjEquiv :
            (a : unop ((CategoryOfElements.π F).op.obj u) ⟶ X) →
              (shrinkYoneda.{w, v₁, u₁}.obj X).obj ((CategoryOfElements.π F).op.obj u))
          x) :
      (obj (obj (const F.Elementsᵒᵖ) F) u).obj Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} C (Type w)
u v : F.Elementsᵒᵖ
g : u ⟶ v
w :
  ∀ (X : C) (x : (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).obj X),
    Eq (α := (obj (obj (const F.Elementsᵒᵖ) F) v).obj X)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).map g ≫
              { app := fun (X : C) ↦ NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F X)) v, naturality := ⋯ :
                NatTrans (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj v)
                  (obj (obj (const F.Elementsᵒᵖ) F) v) })
            X))
        x)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            ({ app := fun (X : C) ↦ NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F X)) u, naturality := ⋯ :
                NatTrans (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u)
                  (obj (obj (const F.Elementsᵒᵖ) F) u) } ≫
              map (obj (const F.Elementsᵒᵖ) F) g)
            X))
        x)
⊢ Eq (α :=
    ((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u ⟶ obj (obj (const F.Elementsᵒᵖ) F) v)
    (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).map g ≫
      { app := fun (X : C) ↦ NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F X)) v, naturality := ⋯ })
    ({ app := fun (X : C) ↦ NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F X)) u, naturality := ⋯ } ≫
      map (obj (const F.Elementsᵒᵖ) F) g)

Tactic:
ext X x
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} C (Type w)
u v : F.Elementsᵒᵖ
g : u ⟶ v
X : C
x : (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).obj X
w :
  ∀ (x : unop ((CategoryOfElements.π F).op.obj u) ⟶ X),
    Eq (α := (obj (obj (const F.Elementsᵒᵖ) F) v).obj X)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).map g ≫
              { app := fun (X : C) ↦ NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F X)) v, naturality := ⋯ :
                NatTrans (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj v)
                  (obj (obj (const F.Elementsᵒᵖ) F) v) })
            X))
        ((Equiv.symm shrinkYonedaObjObjEquiv :
            (a : unop ((CategoryOfElements.π F).op.obj u) ⟶ X) →
              (shrinkYoneda.{w, v₁, u₁}.obj X).obj ((CategoryOfElements.π F).op.obj u))
          x))
      (TypeCat.Fun.toFun (X := (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).obj X)
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            ({ app := fun (X : C) ↦ NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F X)) u, naturality := ⋯ :
                NatTrans (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u)
                  (obj (obj (const F.Elementsᵒᵖ) F) u) } ≫
              map (obj (const F.Elementsᵒᵖ) F) g)
            X))
        ((Equiv.symm shrinkYonedaObjObjEquiv :
            (a : unop ((CategoryOfElements.π F).op.obj u) ⟶ X) →
              (shrinkYoneda.{w, v₁, u₁}.obj X).obj ((CategoryOfElements.π F).op.obj u))
          x))
⊢ Eq (α := (obj (obj (const F.Elementsᵒᵖ) F) v).obj X)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).map g ≫
            { app := fun (X : C) ↦ NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F X)) v, naturality := ⋯ :
              NatTrans (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj v)
                (obj (obj (const F.Elementsᵒᵖ) F) v) })
          X))
      x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ({ app := fun (X : C) ↦ NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F X)) u, naturality := ⋯ :
              NatTrans (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u)
                (obj (obj (const F.Elementsᵒᵖ) F) u) } ≫
            map (obj (const F.Elementsᵒᵖ) F) g)
          X))
      x)

Tactic:
obtain ⟨x, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective x

Premises used: CategoryTheory.shrinkYonedaObjObjEquiv, Equiv.surjective, Equiv.symm, rfl
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} C (Type w)
u v : F.Elementsᵒᵖ
g : u ⟶ v
X : C
x : unop ((CategoryOfElements.π F).op.obj u) ⟶ X
⊢ Eq (α := (obj (obj (const F.Elementsᵒᵖ) F) v).obj X)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).map g ≫
            { app := fun (X : C) ↦ NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F X)) v, naturality := ⋯ :
              NatTrans (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj v)
                (obj (obj (const F.Elementsᵒᵖ) F) v) })
          X))
      ((Equiv.symm shrinkYonedaObjObjEquiv :
          (a : unop ((CategoryOfElements.π F).op.obj u) ⟶ X) →
            (shrinkYoneda.{w, v₁, u₁}.obj X).obj ((CategoryOfElements.π F).op.obj u))
        x))
    (TypeCat.Fun.toFun (X := (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u).obj X)
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ({ app := fun (X : C) ↦ NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F X)) u, naturality := ⋯ :
              NatTrans (((CategoryOfElements.π F).op ⋙ Functor.flip shrinkYoneda.{w, v₁, u₁}).obj u)
                (obj (obj (const F.Elementsᵒᵖ) F) u) } ≫
            map (obj (const F.Elementsᵒᵖ) F) g)
          X))
      ((Equiv.symm shrinkYonedaObjObjEquiv :
          (a : unop ((CategoryOfElements.π F).op.obj u) ⟶ X) →
            (shrinkYoneda.{w, v₁, u₁}.obj X).obj ((CategoryOfElements.π F).op.obj u))
        x))

Tactic:
simp [← shrinkYonedaObjObjEquiv_symm_comp.{w}]
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} C (Type w)
inst_2 : HasColimitsOfShape F.Elementsᵒᵖ (Type w)
u : F.Elements
⊢ Eq (α :=
    ((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} (u.fst (β := fun (c : C) ↦ F.obj c))).obj (op u) ⟶
      (shrinkYoneda.{w, v₁, u₁} ⋙
            obj (whiskeringLeft F.Elementsᵒᵖ Cᵒᵖ (Type w)) (CategoryOfElements.π F).op ⋙ colim).obj
        (u.fst (β := fun (c : C) ↦ F.obj c)))
    (CategoryStruct.comp (Y :=
      obj
        (obj (const F.Elementsᵒᵖ)
          (Cocone.pt (F :=
            (CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} (u.fst (β := fun (c : C) ↦ F.obj c)))
            (coconeπOpCompShrinkYonedaObj F (u.fst (β := fun (c : C) ↦ F.obj c)))))
        (op u))
      (NatTrans.app (Cocone.ι (coconeπOpCompShrinkYonedaObj F (u.fst (β := fun (c : C) ↦ F.obj c)))) (op u))
      (NatTrans.app (Iso.inv (shrinkYonedaCompWhiskeringLeftObjπCompColimIso F)) (u.fst (β := fun (c : C) ↦ F.obj c))))
    (colimit.ι ((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} (u.fst (β := fun (c : C) ↦ F.obj c))) (op u))

Tactic:
have :
      (coconeπOpCompShrinkYonedaObj F u.fst).ι.app (op u) ≫
        (shrinkYonedaCompWhiskeringLeftObjπCompColimIso F).inv.app u.fst =
      colimit.ι ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w}.obj u.fst) (op u) :=
    IsColimit.comp_coconePointUniqueUpToIso_inv (colimit.isColimit _) _ (op u)
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} C (Type w)
X : C
u : Elements.{w, v₁, u₁} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (map (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X))
            ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj u.fst).obj (op X)) → unop (op X) ⟶ u.fst)
              (u.snd (β := fun (c : C) ↦
                obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c)))) :
        (a :
            (fun (X : Type w) ↦ X)
              ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).obj
                ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).elementsMk X
                    ((shrinkYonedaObjObjEquiv.symm :
                        (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op X))
                      (𝟙 X))).fst)) →
          (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).obj u.fst))
      (Sigma.snd (β := fun (c : C) ↦ obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c)
        (elementsMk (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) X
          ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op X))
            (𝟙 X)))) =
    u.snd (β := fun (c : C) ↦ obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c)

Tactic:
simp [shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm.{w}]
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} C (Type w)
X : C
⊢ HasInitial (Elements.{w, v₁, u₁} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)))

Tactic:
(isInitialElementsMkShrinkYonedaObjObjEquivId X).hasInitial

Premises used: CategoryTheory.Functor.Elements.isInitialElementsMkShrinkYonedaObjObjEquivId, CategoryTheory.Limits.IsInitial.hasInitial
-- Module: Mathlib.CategoryTheory.Limits.Set
Goal:
J : Type w
inst : Category.{w', w} J
X : Type u
inst_1 : IsFilteredOrEmpty.{w', w} J
F : CategoryTheory.Functor.{w', u, w, u} J (Set X)
apply : IsColimit (F := F ⋙ functorToTypes) (Functor.mapCocone functorToTypes (colimitCocone F).cocone)
⊢ PreservesColimit F functorToTypes

Tactic:
apply preservesColimit_of_preserves_colimit_cocone (colimitCocone F).isColimit

Premises used: CategoryTheory.Limits.CompleteLattice.colimitCocone, CategoryTheory.Limits.ColimitCocone.isColimit, CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone
-- Module: Mathlib.CategoryTheory.Limits.Set
Goal:
J : Type w
inst : Category.{w', w} J
X : Type u
inst_1 : IsFilteredOrEmpty.{w', w} J
F : CategoryTheory.Functor.{w', u, w, u} J (Set X)
x : X
hx : x ∈ (colimitCocone F).cocone.pt
⊢ ∃ (i : J), x ∈ F.obj i

Tactic:
simp only [colimitCocone_cocone_pt, iSup_eq_iUnion, mem_iUnion] at hx

Premises used: Set.mem_iUnion, CategoryTheory.Limits.CompleteLattice.colimitCocone_cocone_pt, Set.iSup_eq_iUnion