-- 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
u₁ u₂ : F.Elementsᵒᵖ
g : u₁ ⟶ u₂
f : ((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X).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)
have 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₁)))
Tactic: obtain ⟨f, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective f
Cleared hypotheses: f