-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Presheaf.Basic (goal)
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' : F.obj (op (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) p)))
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')
have obtain : ∀ (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 sorry)) :
            (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')))))),
  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)))) p
      q')
Tactic: obtain rfl : p = q := yonedaEquiv.symm.injective h
Cleared hypotheses: q, q', h, h'