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

Tactic:
ext f