-- 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
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))
⊢ 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)))))

Tactic:
simpa using ConcreteCategory.congr_hom this (shrinkYonedaObjObjEquiv.symm (𝟙 _))

Premises used: CategoryTheory.ConcreteCategory.congr_hom