awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A_1 A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
D : Type u₂
inst_3 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : Functor.LeftExtension uliftYoneda.{max w v₂, v₁, u₁} (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
X : C
w :
  CategoryStruct.comp (Y := Functor.obj F.op.lan (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X))
      (NatTrans.app (Iso.hom (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) X)
      (NatTrans.app (Iso.inv (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) X ≫
        (StructuredArrow.hom Φ).app X) =
    (StructuredArrow.hom Φ).app X
w₁ w₂ : (StructuredArrow.hom Φ).app X = (StructuredArrow.hom Φ).app X
⊢ NatTrans.app (Iso.hom (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) X ≫
      NatTrans.app (natTrans.{w, v₁, v₂, u₁, u₂} (StructuredArrow.hom Φ))
        (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X) =
    (StructuredArrow.hom Φ).app X

Tactic:
rw [natTrans_app_uliftYoneda_obj, Iso.hom_inv_id_app_assoc]

Premises used: CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.natTrans_app_uliftYoneda_obj, CategoryTheory.Iso.hom_inv_id_app_assoc
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : Functor.LeftExtension uliftYoneda.{max w v₂, v₁, u₁} (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
f g : Functor.LeftExtension.mk F.op.lan (Iso.hom (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) ⟶ Φ
h : ∀ (P : Cᵒᵖ ⥤ Type (max (max w v₁) v₂)), (StructuredArrow.Hom.right f).app P = (StructuredArrow.Hom.right g).app P
⊢ f = g

Tactic:
ext P : 3
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : Functor.LeftExtension uliftYoneda.{max w v₂, v₁, u₁} (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
f g : Functor.LeftExtension.mk F.op.lan (Iso.hom (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) ⟶ Φ
P : Cᵒᵖ ⥤ Type (max (max w v₁) v₂)
h :
  NatTrans.app F.op.lanUnit P ≫ F.op.whiskerLeft ((StructuredArrow.Hom.right f).app P) =
    NatTrans.app F.op.lanUnit P ≫ F.op.whiskerLeft ((StructuredArrow.Hom.right g).app P)
⊢ (StructuredArrow.Hom.right f).app P = (StructuredArrow.Hom.right g).app P

Tactic:
apply (F.op.lan.obj P).hom_ext_of_isLeftKanExtension (F.op.lanUnit.app P)

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.hom_ext_of_isLeftKanExtension, CategoryTheory.Functor.lan, CategoryTheory.Functor.lanUnit, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : Functor.LeftExtension uliftYoneda.{max w v₂, v₁, u₁} (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
f g : Functor.LeftExtension.mk F.op.lan (Iso.hom (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) ⟶ Φ
P : Cᵒᵖ ⥤ Type (max (max w v₁) v₂)
h :
  ∀ (j : P.Elementsᵒᵖ),
    (coconeOfRepresentable P).ι.app j ≫
        NatTrans.app F.op.lanUnit P ≫ F.op.whiskerLeft ((StructuredArrow.Hom.right f).app P) =
      (coconeOfRepresentable P).ι.app j ≫
        NatTrans.app F.op.lanUnit P ≫ F.op.whiskerLeft ((StructuredArrow.Hom.right g).app P)
⊢ NatTrans.app F.op.lanUnit P ≫ F.op.whiskerLeft ((StructuredArrow.Hom.right f).app P) =
    NatTrans.app F.op.lanUnit P ≫ F.op.whiskerLeft ((StructuredArrow.Hom.right g).app P)

Tactic:
apply (colimitOfRepresentable.{max w v₂} P).hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : Functor.LeftExtension uliftYoneda.{max w v₂, v₁, u₁} (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
f g : Functor.LeftExtension.mk F.op.lan (Iso.hom (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) ⟶ Φ
P : Cᵒᵖ ⥤ Type (max (max w v₁) v₂)
x : P.Elementsᵒᵖ
⊢ Eq (α :=
    Functor.obj (𝟭 (Cᵒᵖ ⥤ Type (max (max w v₂) v₁))) (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop (unop x).1)) ⟶
      Functor.obj (F.op.lan ⋙ Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max (max w v₂) v₁))) F.op) P)
    (Functor.map (𝟭 (Cᵒᵖ ⥤ Type (max (max w v₂) v₁)))
          ((Equiv.symm uliftYonedaEquiv :
              (a : P.obj (op (unop (unop x).1))) → uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).1) ⟶ P)
            ((unop x).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ≫
        NatTrans.app F.op.lanUnit P :
      Functor.obj (𝟭 (Cᵒᵖ ⥤ Type (max (max w v₂) v₁))) (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop (unop x).1)) ⟶
        Functor.obj (F.op.lan ⋙ Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max (max w v₂) v₁))) F.op) P)
    (NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop (unop x).1)) ≫
        Functor.map (F.op.lan ⋙ Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max (max w v₂) v₁))) F.op)
          ((Equiv.symm uliftYonedaEquiv :
              (a : P.obj (op (unop (unop x).1))) → uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).1) ⟶ P)
            ((unop x).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c))) :
      Functor.obj (𝟭 (Cᵒᵖ ⥤ Type (max (max w v₂) v₁))) (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop (unop x).1)) ⟶
        Functor.obj (F.op.lan ⋙ Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max (max w v₂) v₁))) F.op) P)

Tactic:
have eq := F.op.lanUnit.naturality (uliftYonedaEquiv.{max w v₂}.symm x.unop.2)
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A_1 A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
D : Type u₂
inst_3 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
⊢ Functor.IsLeftKanExtension F.op.lan (Iso.hom (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F))

Tactic:
⟨⟨Limits.IsInitial.ofUnique _⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.IsInitial.ofUnique, CategoryTheory.Functor.IsLeftKanExtension.mk
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type v₁
inst_1 : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
h : IsTerminal (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda))
⊢ (c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt).Final

Tactic:
apply Functor.final_of_isTerminal_colimit_comp_yoneda

Premises used: CategoryTheory.Functor.final_of_isTerminal_colimit_comp_yoneda
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type v₁
inst_1 : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
this :
  IsTerminal
    (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
l :
  IsTerminal
    ((overEquivPresheafCostructuredArrow c.pt).inverse.obj
      (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda)))
⊢ IsTerminal (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda))

Tactic:
apply IsTerminal.isTerminalOfObj (overEquivPresheafCostructuredArrow c.pt).inverse

Premises used: CategoryTheory.Limits.IsTerminal.isTerminalOfObj, CategoryTheory.overEquivPresheafCostructuredArrow, CategoryTheory.Limits.Cocone.pt, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type v₁
inst_1 : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
this :
  IsTerminal
    (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
l :
  colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt) ≅
    (overEquivPresheafCostructuredArrow c.pt).inverse.obj
      (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda))
⊢ IsTerminal
    ((overEquivPresheafCostructuredArrow c.pt).inverse.obj
      (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda)))

Tactic:
apply IsTerminal.ofIso this

Premises used: CategoryTheory.Limits.IsTerminal.ofIso
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type v₁
inst_1 : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
this :
  IsTerminal
    (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
l :
  colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt) ≅
    colimit
      (((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda) ⋙
        (overEquivPresheafCostructuredArrow c.pt).inverse)
⊢ colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt) ≅
    (overEquivPresheafCostructuredArrow c.pt).inverse.obj
      (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda))

Tactic:
refine ?_ ≪≫ (preservesColimitIso (overEquivPresheafCostructuredArrow c.pt).inverse _).symm

Premises used: CategoryTheory.overEquivPresheafCostructuredArrow, CategoryTheory.preservesColimitIso, CategoryTheory.Iso.symm, CategoryTheory.Limits.Cocone.pt, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type v₁
inst_1 : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
this :
  IsTerminal
    (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
l :
  (c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt ≅
    ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda) ⋙
      (overEquivPresheafCostructuredArrow c.pt).inverse
⊢ colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt) ≅
    colimit
      (((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda) ⋙
        (overEquivPresheafCostructuredArrow c.pt).inverse)

Tactic:
apply HasColimit.isoOfNatIso

Premises used: CategoryTheory.Limits.HasColimit.isoOfNatIso
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type v₁
inst_1 : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
this :
  IsTerminal
    (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
⊢ (c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt ≅
    ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda) ⋙
      (overEquivPresheafCostructuredArrow c.pt).inverse

Tactic:
exact Functor.isoWhiskerLeft _
      (CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow c.pt).isoCompInverse

Premises used: CategoryTheory.CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow, CategoryTheory.Iso.isoCompInverse, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Limits.Cocone.pt
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type v₁
inst_1 : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
h :
  IsTerminal
    (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
⊢ IsTerminal (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda))

Tactic:
suffices IsTerminal (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙
      CostructuredArrow.toOver yoneda c.pt)) by
    apply IsTerminal.isTerminalOfObj (overEquivPresheafCostructuredArrow c.pt).inverse
    apply IsTerminal.ofIso this
    refine ?_ ≪≫ (preservesColimitIso (overEquivPresheafCostructuredArrow c.pt).inverse _).symm
    apply HasColimit.isoOfNatIso
    exact Functor.isoWhiskerLeft _
      (CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow c.pt).isoCompInverse
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type v₁
inst_1 : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
h :
  Over.mk (𝟙 c.pt) ≅
    colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt)
⊢ IsTerminal
    (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))

Tactic:
apply IsTerminal.ofIso Over.mkIdTerminal

Premises used: CategoryTheory.Over.mkIdTerminal, CategoryTheory.Limits.IsTerminal.ofIso
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type v₁
inst_1 : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
isc : IsColimit (F :=
  ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt) ⋙
    Over.forget c.pt)
  (Functor.mapCocone (Over.forget c.pt)
    (colimit.cocone
      ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))) :=
  isColimitOfPreserves (Over.forget c.pt)
    (colimit.isColimit
      ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
i : I
⊢ c.ι.app i ≫
      (hc.coconePointUniqueUpToIso isc).hom ≫
        (colimit
            ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙
              CostructuredArrow.toOver yoneda c.pt)).hom =
    c.ι.app i ≫ (Over.mk (𝟙 c.pt)).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type v₁
inst_1 : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
isc : IsColimit (F :=
  ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt) ⋙
    Over.forget c.pt)
  (Functor.mapCocone (Over.forget c.pt)
    (colimit.cocone
      ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))) :=
  isColimitOfPreserves (Over.forget c.pt)
    (colimit.isColimit
      ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
⊢ Over.mk (𝟙 c.pt) ≅
    colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt)

Tactic:
exact Over.isoMk (hc.coconePointUniqueUpToIso isc) (hc.hom_ext fun i => by simp)

Premises used: CategoryTheory.Over.isoMk
-- 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₁ u₂ : F.Elementsᵒᵖ
g : u₁ ⟶ u₂
f : unop ((CategoryOfElements.π F).op.obj u₁) ⟶ X
⊢ Eq (α := obj (obj (const F.Elementsᵒᵖ) (F.obj X)) u₂)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X).map g ≫
          ↾fun (t : ((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X).obj u₂) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (F.map
                    ((shrinkYonedaObjObjEquiv :
                        (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj ((CategoryOfElements.π F).op.obj u₂)) →
                          unop ((CategoryOfElements.π F).op.obj u₂) ⟶ X)
                      t)) :
                (a : (fun (X : Type w) ↦ X) (F.obj (unop ((CategoryOfElements.π F).op.obj u₂)))) →
                  (fun (X : Type w) ↦ X) (F.obj X))
              ((unop u₂).snd (β := fun (c : C) ↦ F.obj c))))
      ((Equiv.symm shrinkYonedaObjObjEquiv :
          (a : unop ((CategoryOfElements.π F).op.obj u₁) ⟶ X) →
            (shrinkYoneda.{w, v₁, u₁}.obj X).obj ((CategoryOfElements.π F).op.obj u₁))
        f))
    (TypeCat.Fun.toFun (X := ((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X).obj u₁)
      (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((↾fun (t : ((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X).obj u₁) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun)
                    (F.map
                      ((shrinkYonedaObjObjEquiv :
                          (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj ((CategoryOfElements.π F).op.obj u₁)) →
                            unop ((CategoryOfElements.π F).op.obj u₁) ⟶ X)
                        t)) :
                  (a : (fun (X : Type w) ↦ X) (F.obj (unop ((CategoryOfElements.π F).op.obj u₁)))) →
                    (fun (X : Type w) ↦ X) (F.obj X))
                ((unop u₁).snd (β := fun (c : C) ↦ F.obj c))) ≫
            map (obj (const F.Elementsᵒᵖ) (F.obj X)) g) :
        TypeCat.Fun (((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X).obj u₁)
          (obj (obj (const F.Elementsᵒᵖ) (F.obj X)) u₂))
      ((Equiv.symm shrinkYonedaObjObjEquiv :
            (a : unop ((CategoryOfElements.π F).op.obj u₁) ⟶ X) →
              (shrinkYoneda.{w, v₁, u₁}.obj X).obj ((CategoryOfElements.π F).op.obj u₁))
          f :
        obj.{v₁, w, u₁, w + 1} (obj shrinkYoneda.{w, v₁, u₁} X) ((CategoryOfElements.π F).op.obj u₁)))

Tactic:
simp [shrinkYoneda_obj_map_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
refine_1 :
  Function.Injective (β :=
    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)))
    (((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)))
refine_2 :
  ∀
    (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
⊢ IsColimit (F := (CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X) (coconeπOpCompShrinkYonedaObj F X)

Tactic:
refine Nonempty.some ((Types.isColimit_iff_coconeTypesIsColimit _).2
    ⟨?_, fun x ↦ ?_⟩)

Premises used: Iff.mpr, CategoryTheory.Limits.Types.isColimit_iff_coconeTypesIsColimit, CategoryTheory.Functor.CoconeTypes.IsColimit.mk, Nonempty.some, And.intro
-- 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
G : F.Elementsᵒᵖ ⥤ Type w := (CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X
c : G.CoconeTypes := (G.coconeTypesEquiv.symm : (a : Cocone G) → G.CoconeTypes) (coconeπOpCompShrinkYonedaObj F X)
u : G.ColimitType
x : F.obj X
h : G.descColimitType c u = x
obtain :
  ∀ (u : F.Elements) (v : G.obj (op u)) (h : G.descColimitType c (G.ιColimitType (op u) v) = x),
    G.ιColimitType (op (F.elementsMk X x))
        ((Equiv.symm shrinkYonedaObjObjEquiv :
            (a : unop ((CategoryOfElements.π F).op.obj (op (F.elementsMk X x))) ⟶ X) →
              (shrinkYoneda.{w, v₁, u₁}.obj X).obj ((CategoryOfElements.π F).op.obj (op (F.elementsMk X x))))
          (𝟙 X)) =
      G.ιColimitType (op u) v
⊢ G.ιColimitType (op (F.elementsMk X x))
      ((Equiv.symm shrinkYonedaObjObjEquiv :
          (a : unop ((CategoryOfElements.π F).op.obj (op (F.elementsMk X x))) ⟶ X) →
            (shrinkYoneda.{w, v₁, u₁}.obj X).obj ((CategoryOfElements.π F).op.obj (op (F.elementsMk X x))))
        (𝟙 X)) =
    u

Tactic:
obtain ⟨⟨u⟩, v, rfl⟩ := Functor.ιColimitType_jointly_surjective _ u

Premises used: CategoryTheory.Functor.ιColimitType_jointly_surjective, 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)
X : C
G : F.Elementsᵒᵖ ⥤ Type w := (CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X
c : G.CoconeTypes := (G.coconeTypesEquiv.symm : (a : Cocone G) → G.CoconeTypes) (coconeπOpCompShrinkYonedaObj F X)
x : F.obj X
u : F.Elements
v : G.obj (op u)
h : G.descColimitType c (G.ιColimitType (op u) v) = x
obtain :
  ∀ (v : unop ((CategoryOfElements.π F).op.obj (op u)) ⟶ X)
    (h :
      G.descColimitType c
          (G.ιColimitType (op u)
            ((Equiv.symm shrinkYonedaObjObjEquiv :
                (a : unop ((CategoryOfElements.π F).op.obj (op u)) ⟶ X) →
                  (shrinkYoneda.{w, v₁, u₁}.obj X).obj ((CategoryOfElements.π F).op.obj (op u)))
              v)) =
        x),
    G.ιColimitType (op (F.elementsMk X x))
        ((Equiv.symm shrinkYonedaObjObjEquiv :
            (a : unop ((CategoryOfElements.π F).op.obj (op (F.elementsMk X x))) ⟶ X) →
              (shrinkYoneda.{w, v₁, u₁}.obj X).obj ((CategoryOfElements.π F).op.obj (op (F.elementsMk X x))))
          (𝟙 X)) =
      G.ιColimitType (op u)
        ((Equiv.symm shrinkYonedaObjObjEquiv :
            (a : unop ((CategoryOfElements.π F).op.obj (op u)) ⟶ X) →
              (shrinkYoneda.{w, v₁, u₁}.obj X).obj ((CategoryOfElements.π F).op.obj (op u)))
          v)
⊢ G.ιColimitType (op (F.elementsMk X x))
      ((Equiv.symm shrinkYonedaObjObjEquiv :
          (a : unop ((CategoryOfElements.π F).op.obj (op (F.elementsMk X x))) ⟶ X) →
            (shrinkYoneda.{w, v₁, u₁}.obj X).obj ((CategoryOfElements.π F).op.obj (op (F.elementsMk X x))))
        (𝟙 X)) =
    G.ιColimitType (op u) v

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

Premises used: CategoryTheory.shrinkYonedaObjObjEquiv, Equiv.surjective, Equiv.symm, rfl