-- 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 : Elements.{w, v₁, u₁} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X))
m :
  Sigma.fst (β := fun (c : C) ↦ obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c)
      (elementsMk (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) X
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op X))
          (𝟙 X))) ⟶
    u.fst (β := fun (c : C) ↦ obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c)
hm :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) m) :
        (a :
            (fun (X : Type w) ↦ X)
              ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).obj
                ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).elementsMk X
                    ((shrinkYonedaObjObjEquiv.symm :
                        (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op X))
                      (𝟙 X))).fst)) →
          (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).obj u.fst))
      (Sigma.snd (β := fun (c : C) ↦ obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c)
        (elementsMk (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) X
          ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op X))
            (𝟙 X)))) =
    u.snd (β := fun (c : C) ↦ obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c)
⊢ Eq (α :=
    elementsMk (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) X
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op X))
          (𝟙 X)) ⟶
      u)
    (Subtype.mk (p :=
      fun
        (f :
          Sigma.fst (β := fun (c : C) ↦ obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c)
              (elementsMk (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) X
                ((Equiv.symm shrinkYonedaObjObjEquiv :
                    (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op X))
                  (𝟙 X))) ⟶
            u.fst (β := fun (c : C) ↦ obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c)) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) f) :
            (a :
                (fun (X : Type w) ↦ X)
                  ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).obj
                    ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).elementsMk X
                        ((shrinkYonedaObjObjEquiv.symm :
                            (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op X))
                          (𝟙 X))).fst)) →
              (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).obj u.fst))
          (Sigma.snd (β := fun (c : C) ↦ obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c)
            (elementsMk (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) X
              ((Equiv.symm shrinkYonedaObjObjEquiv :
                  (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op X))
                (𝟙 X)))) =
        u.snd (β := fun (c : C) ↦ obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c))
      m hm)
    ((fun (u : Elements.{w, v₁, u₁} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X))) ↦
        (Subtype.mk (p :=
            fun
              (f :
                Sigma.fst (β := fun (c : C) ↦
                    obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c)
                    (elementsMk (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) X
                      ((Equiv.symm shrinkYonedaObjObjEquiv :
                          (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op X))
                        (𝟙 X))) ⟶
                  u.fst (β := fun (c : C) ↦
                    obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c)) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) f) :
                  (a :
                      (fun (X : Type w) ↦ X)
                        ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).obj
                          ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).elementsMk X
                              ((shrinkYonedaObjObjEquiv.symm :
                                  (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op X))
                                (𝟙 X))).fst)) →
                    (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).obj u.fst))
                (Sigma.snd (β := fun (c : C) ↦
                  obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c)
                  (elementsMk (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) X
                    ((Equiv.symm shrinkYonedaObjObjEquiv :
                        (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op X))
                      (𝟙 X)))) =
              u.snd (β := fun (c : C) ↦ obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c))
            ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj u.fst).obj (op X)) → unop (op X) ⟶ u.fst)
              (u.snd (β := fun (c : C) ↦
                obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c)))
            ⋯ :
          { f :
            Sigma.fst (β := fun (c : C) ↦ obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c)
                (elementsMk (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) X
                  ((Equiv.symm shrinkYonedaObjObjEquiv :
                      (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op X))
                    (𝟙 X))) ⟶
              u.fst (β := fun (c : C) ↦
                obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c) //
            (ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) f) :
                  (a :
                      (fun (X : Type w) ↦ X)
                        ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).obj
                          ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).elementsMk X
                              ((shrinkYonedaObjObjEquiv.symm :
                                  (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op X))
                                (𝟙 X))).fst)) →
                    (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).obj u.fst))
                (Sigma.snd (β := fun (c : C) ↦
                  obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c)
                  (elementsMk (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) X
                    ((Equiv.symm shrinkYonedaObjObjEquiv :
                        (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op X))
                      (𝟙 X)))) =
              u.snd (β := fun (c : C) ↦
                obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c) }))
      u)
have w : (↑(Subtype.mk (p :=
        fun
          (f :
            Sigma.fst (β := fun (c : C) ↦ obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c)
                (elementsMk (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) X
                  ((Equiv.symm shrinkYonedaObjObjEquiv :
                      (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op X))
                    (𝟙 X))) ⟶
              u.fst (β := fun (c : C) ↦
                obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c)) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) f) :
              (a :
                  (fun (X : Type w) ↦ X)
                    ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).obj
                      ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).elementsMk X
                          ((shrinkYonedaObjObjEquiv.symm :
                              (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op X))
                            (𝟙 X))).fst)) →
                (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).obj u.fst))
            (Sigma.snd (β := fun (c : C) ↦
              obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c)
              (elementsMk (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) X
                ((Equiv.symm shrinkYonedaObjObjEquiv :
                    (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op X))
                  (𝟙 X)))) =
          u.snd (β := fun (c : C) ↦ obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c))
        m hm) :
    ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).elementsMk X
          ((shrinkYonedaObjObjEquiv.symm : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op X))
            (𝟙 X))).fst ⟶
      u.fst) =
  (↑((fun (u : Elements.{w, v₁, u₁} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X))) ↦
          (Subtype.mk (p :=
              fun
                (f :
                  Sigma.fst (β := fun (c : C) ↦
                      obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c)
                      (elementsMk (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) X
                        ((Equiv.symm shrinkYonedaObjObjEquiv :
                            (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op X))
                          (𝟙 X))) ⟶
                    u.fst (β := fun (c : C) ↦
                      obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c)) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) f) :
                    (a :
                        (fun (X : Type w) ↦ X)
                          ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).obj
                            ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).elementsMk X
                                ((shrinkYonedaObjObjEquiv.symm :
                                    (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op X))
                                  (𝟙 X))).fst)) →
                      (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).obj u.fst))
                  (Sigma.snd (β := fun (c : C) ↦
                    obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c)
                    (elementsMk (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) X
                      ((Equiv.symm shrinkYonedaObjObjEquiv :
                          (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op X))
                        (𝟙 X)))) =
                u.snd (β := fun (c : C) ↦
                  obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c))
              ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj u.fst).obj (op X)) → unop (op X) ⟶ u.fst)
                (u.snd (β := fun (c : C) ↦
                  obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c)))
              sorry :
            { f :
              Sigma.fst (β := fun (c : C) ↦
                  obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c)
                  (elementsMk (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) X
                    ((Equiv.symm shrinkYonedaObjObjEquiv :
                        (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op X))
                      (𝟙 X))) ⟶
                u.fst (β := fun (c : C) ↦
                  obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c) //
              (ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) f) :
                    (a :
                        (fun (X : Type w) ↦ X)
                          ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).obj
                            ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).elementsMk X
                                ((shrinkYonedaObjObjEquiv.symm :
                                    (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op X))
                                  (𝟙 X))).fst)) →
                      (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).obj u.fst))
                  (Sigma.snd (β := fun (c : C) ↦
                    obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c)
                    (elementsMk (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) X
                      ((Equiv.symm shrinkYonedaObjObjEquiv :
                          (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op X))
                        (𝟙 X)))) =
                u.snd (β := fun (c : C) ↦
                  obj.{v₁, w, u₁, w + 1} (obj (Functor.flip shrinkYoneda.{w, v₁, u₁}) (op X)) c) }))
        u) :
    ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).elementsMk X
          ((shrinkYonedaObjObjEquiv.symm : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op X))
            (𝟙 X))).fst ⟶
      u.fst)
Tactic: ext