-- 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 : ((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X).obj u₁
h :
  ∀ (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₁)))
⊢ 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))))
      f)
    (TypeCat.Fun.toFun
      (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))
      f)

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

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