-- 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 : 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)
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)))
                ⋯ :
              { 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)
⊢ 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)

Tactic:
ext