-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
p : A.obj (op X)
p' q' : F.obj (op (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) p)))
h :
  fst (F := F)
      (Sigma.mk (β := fun (s : A.obj (op X)) ↦
        F.obj (op (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
        p p') =
    fst (F := F)
      (Sigma.mk (β := fun (s : A.obj (op X)) ↦
        F.obj (op (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
        p q')
h' :
  Eq (α :=
    (fun (X : Type v) ↦ X)
      (F.obj
        (op
          (CostructuredArrow.mk
            (fst (F := F)
              (Sigma.mk (β := fun (s : A.obj (op X)) ↦
                F.obj
                  (op
                    (CostructuredArrow.mk (Y := X)
                      ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
                p p'))))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom ⋯)) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk (fst ⟨p, q'⟩))))) →
            (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk (fst ⟨p, p'⟩)))))
        (snd
          (Sigma.mk (β := fun (s : A.obj (op X)) ↦
            F.obj
              (op (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
            p q')) :
      (fun (X : Type v) ↦ X)
        (F.obj
          (op
            (CostructuredArrow.mk
              (fst (F := F)
                (Sigma.mk (β := fun (s : A.obj (op X)) ↦
                  F.obj
                    (op
                      (CostructuredArrow.mk (Y := X)
                        ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
                  p p'))))))
    (snd
        (Sigma.mk (β := fun (s : A.obj (op X)) ↦
          F.obj
            (op (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
          p p') :
      F.obj
        (op
          (CostructuredArrow.mk
            (fst (F := F)
              (Sigma.mk (β := fun (s : A.obj (op X)) ↦
                F.obj
                  (op
                    (CostructuredArrow.mk (Y := X)
                      ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
                p p')))))
⊢ HEq (α :=
    F.obj
      (op
        (CostructuredArrow.mk (Y := X)
          ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A)
            (Sigma.fst (β := fun (s : A.obj (op X)) ↦
              F.obj
                (op
                  (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
              (Sigma.mk (β := fun (s : A.obj (op X)) ↦
                F.obj
                  (op
                    (CostructuredArrow.mk (Y := X)
                      ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
                p p'))))))
    (Sigma.snd (β := fun (s : A.obj (op X)) ↦
        F.obj (op (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
        (Sigma.mk (β := fun (s : A.obj (op X)) ↦
          F.obj
            (op (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
          p p') :
      F.obj
        (op
          (CostructuredArrow.mk (Y := X)
            ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A)
              (Sigma.fst (β := fun (s : A.obj (op X)) ↦
                F.obj
                  (op
                    (CostructuredArrow.mk (Y := X)
                      ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
                (Sigma.mk (β := fun (s : A.obj (op X)) ↦
                  F.obj
                    (op
                      (CostructuredArrow.mk (Y := X)
                        ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
                  p p'))))))
    (β :=
    F.obj
      (op
        (CostructuredArrow.mk (Y := X)
          ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A)
            (Sigma.fst (β := fun (s : A.obj (op X)) ↦
              F.obj
                (op
                  (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
              (Sigma.mk (β := fun (s : A.obj (op X)) ↦
                F.obj
                  (op
                    (CostructuredArrow.mk (Y := X)
                      ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
                p q'))))))
    (Sigma.snd (β := fun (s : A.obj (op X)) ↦
        F.obj (op (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
        (Sigma.mk (β := fun (s : A.obj (op X)) ↦
          F.obj
            (op (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
          p q') :
      F.obj
        (op
          (CostructuredArrow.mk (Y := X)
            ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A)
              (Sigma.fst (β := fun (s : A.obj (op X)) ↦
                F.obj
                  (op
                    (CostructuredArrow.mk (Y := X)
                      ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
                (Sigma.mk (β := fun (s : A.obj (op X)) ↦
                  F.obj
                    (op
                      (CostructuredArrow.mk (Y := X)
                        ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
                  p q'))))))

Tactic:
simpa [snd] using h'.symm

Premises used: Eq.symm, CategoryTheory.OverPresheafAux.YonedaCollection.snd