awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
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
⊢ 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
have 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)
Tactic: obtain ⟨v, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective v
Cleared hypotheses: v, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (hypothesis)
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
⊢ 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)
have 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
Tactic: simp only [Equiv.apply_symm_apply] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
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 (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)
have 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)
Tactic: rw [← G.ιColimitType_map (show u ⟶ F.elementsMk _ x from ⟨v, h⟩).op]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (hypothesis)
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)
⊢ 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)))
have 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
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}]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
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₂)
⊢ u₁ = u₂
have refine_1 : ∀ (x : c.pt) (hx₁ : G.descColimitType c u₁ = x), u₁ = u₂
Tactic: generalize hx₁ : G.descColimitType c u₁ = x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
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
have rw : G.descColimitType c u₂ = G.descColimitType c u₁
Tactic: rw [← hx₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (hypothesis)
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
⊢ u₁ = u₂
have hx₂ : G.descColimitType c u₂ = x
Tactic: have hx₂ : G.descColimitType c u₂ = x := by rw [← hx₁]; exact hu.symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
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
⊢ u₁ = u₂
have 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₂
Tactic: rw [← this _ _ hx₁, ← this _ _ hx₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
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₂
⊢ u₁ = u₂
have 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))
Tactic: rw [← this _ _ hx₁, ← this _ _ hx₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
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
⊢ 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)
have 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
Tactic: ext g