-- 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)
⊢ (↑(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)

Tactic:
simp [← hm, shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm.{w}]