-- 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
q : YonedaCollection F X
p : A.obj (op X)
p' : 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') =
    q.fst
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 q.fst)))) →
            (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk (fst ⟨p, p'⟩)))))
        q.snd :
      (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')))))
rcases :
  ∀ (q : A.obj (op X))
    (q' :
      F.obj (op (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) q))))
    (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))))
            q 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 ⟨q, 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))))
                q 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')))))),
    Eq (α := YonedaCollection F X)
      (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.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))))
        q q')
⊢ 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' =
    q

Tactic:
rcases q with ⟨q, q'⟩