-- 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)
inst_2 : HasColimitsOfShape F.Elementsᵒᵖ (Type w)
u : F.Elements
⊢ Eq (α :=
    (fun (X : Type w) ↦ X)
      ((shrinkYoneda.{w, v₁, u₁} ⋙
            obj (whiskeringLeft F.Elementsᵒᵖ Cᵒᵖ (Type w)) (CategoryOfElements.π F).op ⋙ colim).obj
        (u.fst (β := fun (c : C) ↦ F.obj c))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Iso.inv (shrinkYonedaCompWhiskeringLeftObjπCompColimIso F))
              (u.fst (β := fun (c : C) ↦ F.obj c))) :
          (a : (fun (X : Type w) ↦ X) (F.obj u.fst)) →
            (fun (X : Type w) ↦ X)
              ((shrinkYoneda.{w, v₁, u₁} ⋙
                    (whiskeringLeft F.Elementsᵒᵖ Cᵒᵖ (Type w)).obj (CategoryOfElements.π F).op ⋙ colim).obj
                u.fst))
        (u.snd (β := fun (c : C) ↦ F.obj c)) :
      (fun (X : Type w) ↦ X)
        ((shrinkYoneda.{w, v₁, u₁} ⋙
              obj (whiskeringLeft F.Elementsᵒᵖ Cᵒᵖ (Type w)) (CategoryOfElements.π F).op ⋙ colim).obj
          (u.fst (β := fun (c : C) ↦ F.obj c))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (colimit.ι ((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} (u.fst (β := fun (c : C) ↦ F.obj c)))
              (op u)) :
          (a : (fun (X : Type w) ↦ X) (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj u.fst).obj (op u))) →
            (fun (X : Type w) ↦ X) (colimit ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj u.fst)))
        ((Equiv.symm shrinkYonedaObjObjEquiv :
              (a : unop ((CategoryOfElements.π F).op.obj (op u)) ⟶ u.fst) →
                (shrinkYoneda.{w, v₁, u₁}.obj u.fst).obj ((CategoryOfElements.π F).op.obj (op u)))
            (𝟙 (unop ((CategoryOfElements.π F).op.obj (op u)))) :
          obj.{v₁, w, u₁, w + 1} (obj shrinkYoneda.{w, v₁, u₁} (u.fst (β := fun (c : C) ↦ F.obj c)))
            ((CategoryOfElements.π F).op.obj (op u))) :
      (fun (X : Type w) ↦ X)
        (colimit ((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} (u.fst (β := fun (c : C) ↦ F.obj c)))))
have this : 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)