-- 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₂
⊢ Eq (α :=
    ((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X).obj u₁ ⟶ obj (obj (const F.Elementsᵒᵖ) (F.obj X)) u₂)
    (((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)))
    ((↾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)
have h : ∀ (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)
Tactic: ext f