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
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 : u.fst (β := fun (c : C) ↦ F.obj c) ⟶ X
h :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (F.map
            ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op u.fst)) → u.fst ⟶ X)
              (((Equiv.symm shrinkYonedaObjObjEquiv :
                    Equiv.{v₁ + 1, w + 1} (u.fst (β := fun (c : C) ↦ F.obj c) ⟶ X)
                      (obj.{v₁, w, u₁, w + 1} (obj shrinkYoneda.{w, v₁, u₁} X)
                        (op (u.fst (β := fun (c : C) ↦ F.obj c))))) :
                  (a : u.fst ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op u.fst))
                v))) :
        (a : F.obj u.fst) → F.obj X)
      (u.snd (β := fun (c : C) ↦ F.obj c)) =
    x
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map v) : (a : F.obj u.fst) → F.obj X)
      (u.snd (β := fun (c : C) ↦ F.obj c)) =
    x

Tactic:
simp only [Equiv.apply_symm_apply] at h

Premises used: Equiv.apply_symm_apply
-- 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 : u.fst (β := fun (c : C) ↦ F.obj c) ⟶ X
h :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map v) : (a : F.obj u.fst) → F.obj X)
      (u.snd (β := fun (c : C) ↦ F.obj c)) =
    x
rw :
  G.ιColimitType (op u)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (G.map
              (Quiver.Hom.op
                (have this : u ⟶ F.elementsMk X x :=
                  Subtype.mk (p :=
                    fun (f : u.fst (β := fun (c : C) ↦ F.obj c) ⟶ (F.elementsMk X x).fst (β := fun (c : C) ↦ F.obj c)) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                          (a : (fun (X : Type w) ↦ X) (F.obj u.fst)) →
                            (fun (X : Type w) ↦ X) (F.obj (F.elementsMk X x).fst))
                        (u.snd (β := fun (c : C) ↦ F.obj c)) =
                      (F.elementsMk X x).snd (β := fun (c : C) ↦ F.obj c))
                    v h;
                this))) :
          (a : (fun (X : Type w) ↦ X) (G.obj (op (F.elementsMk X x)))) → (fun (X : Type w) ↦ X) (G.obj (op u)))
        ((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) :
          obj.{v₁, w, u₁, w + 1} (obj shrinkYoneda.{w, v₁, u₁} X)
            ((CategoryOfElements.π F).op.obj (op (F.elementsMk 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)
      ((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)

Tactic:
rw [← G.ιColimitType_map (show u ⟶ F.elementsMk _ x from ⟨v, h⟩).op]

Premises used: CategoryTheory.Functor.ιColimitType_map, Quiver.Hom.op, Subtype.mk
-- 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 : u.fst (β := fun (c : C) ↦ F.obj c) ⟶ X
h :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map v) : (a : F.obj u.fst) → F.obj X)
      (u.snd (β := fun (c : C) ↦ F.obj c)) =
    x
⊢ G.ιColimitType (op u)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (G.map
              (Quiver.Hom.op
                (have this : u ⟶ F.elementsMk X x :=
                  Subtype.mk (p :=
                    fun (f : u.fst (β := fun (c : C) ↦ F.obj c) ⟶ (F.elementsMk X x).fst (β := fun (c : C) ↦ F.obj c)) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                          (a : (fun (X : Type w) ↦ X) (F.obj u.fst)) →
                            (fun (X : Type w) ↦ X) (F.obj (F.elementsMk X x).fst))
                        (u.snd (β := fun (c : C) ↦ F.obj c)) =
                      (F.elementsMk X x).snd (β := fun (c : C) ↦ F.obj c))
                    v h;
                this))) :
          (a : (fun (X : Type w) ↦ X) (G.obj (op (F.elementsMk X x)))) → (fun (X : Type w) ↦ X) (G.obj (op u)))
        ((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) :
          obj.{v₁, w, u₁, w + 1} (obj shrinkYoneda.{w, v₁, u₁} X)
            ((CategoryOfElements.π F).op.obj (op (F.elementsMk 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)

Tactic:
simp [G, 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
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),
    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:
have (u : G.ColimitType) (x : F.obj X) (h : G.descColimitType c u = x) :
        G.ιColimitType (op (elementsMk _ _ x))
          (shrinkYonedaObjObjEquiv.symm (𝟙 X)) = u := by
      obtain ⟨⟨u⟩, v, rfl⟩ := Functor.ιColimitType_jointly_surjective _ u
      obtain ⟨v, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective v
      dsimp [c] at v h
      simp only [Equiv.apply_symm_apply] at h
      rw [← G.ιColimitType_map (show u ⟶ F.elementsMk _ x from ⟨v, h⟩).op]
      simp [G, 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
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)
this :
  ∀ (u : G.ColimitType) (x : F.obj X) (h : G.descColimitType c u = 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)) =
      u
u₁ u₂ : ((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X).ColimitType
hu :
  Eq (α :=
    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))
      u₁)
    (((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))
      u₂)
refine_1 : ∀ (x : c.pt) (hx₁ : G.descColimitType c u₁ = x), u₁ = u₂
⊢ u₁ = u₂

Tactic:
generalize hx₁ : G.descColimitType c u₁ = x

Premises used: CategoryTheory.Functor.descColimitType
-- 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)
this :
  ∀ (u : G.ColimitType) (x : F.obj X) (h : G.descColimitType c u = 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)) =
      u
u₁ u₂ : ((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X).ColimitType
hu :
  Eq (α :=
    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))
      u₁)
    (((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))
      u₂)
x : c.pt
hx₁ : G.descColimitType c u₁ = x
rw : G.descColimitType c u₂ = G.descColimitType c u₁
⊢ G.descColimitType c u₂ = x

Tactic:
rw [← hx₁]
-- 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)
this :
  ∀ (u : G.ColimitType) (x : F.obj X) (h : G.descColimitType c u = 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)) =
      u
u₁ u₂ : ((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X).ColimitType
hu :
  Eq (α :=
    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))
      u₁)
    (((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))
      u₂)
x : c.pt
hx₁ : G.descColimitType c u₁ = x
⊢ G.descColimitType c u₂ = G.descColimitType c u₁

Tactic:
hu.symm

Premises used: Eq.symm
-- 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)
this :
  ∀ (u : G.ColimitType) (x : F.obj X) (h : G.descColimitType c u = 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)) =
      u
u₁ u₂ : ((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X).ColimitType
hu :
  Eq (α :=
    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))
      u₁)
    (((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))
      u₂)
x : c.pt
hx₁ : G.descColimitType c u₁ = x
⊢ G.descColimitType c u₂ = G.descColimitType c u₁

Tactic:
exact hu.symm

Premises used: Eq.symm
-- 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)
this :
  ∀ (u : G.ColimitType) (x : F.obj X) (h : G.descColimitType c u = 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)) =
      u
u₁ u₂ : ((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X).ColimitType
hu :
  Eq (α :=
    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))
      u₁)
    (((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))
      u₂)
x : c.pt
hx₁ : G.descColimitType c u₁ = x
⊢ G.descColimitType c u₂ = x

Tactic:
have hx₂ : G.descColimitType c u₂ = x := by rw [← hx₁]; exact hu.symm
-- 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)
this :
  ∀ (u : G.ColimitType) (x : F.obj X) (h : G.descColimitType c u = 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)) =
      u
u₁ u₂ : ((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X).ColimitType
hu :
  Eq (α :=
    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))
      u₁)
    (((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))
      u₂)
x : c.pt
hx₁ : G.descColimitType c u₁ = x
hx₂ : G.descColimitType c u₂ = x
refine_1 :
  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₂
refine_1₁ refine_1₂ :
  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 (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₁ = u₂

Tactic:
rw [← this _ _ hx₁, ← this _ _ hx₂]
-- 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))
⊢ ((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))
      (((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X).ι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))) =
    x

Tactic:
simp