-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
η : F ⟶ A
X : C
x : F.obj (op X)
⊢ Eq (α :=
    (fun (X : Type v) ↦ X)
      (A.obj
        (op
          (CostructuredArrow.left (D := Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)) (S :=
            (yoneda : C ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v))) (T := A)
            (unop
                (op
                  (CostructuredArrow.mk (Y := X)
                    ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A)
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app (op X)) :
                          (a : (fun (X : Type v) ↦ X) (F.obj (op X))) → (fun (X : Type v) ↦ X) (A.obj (op X)))
                        x)))) :
              CostructuredArrow yoneda A)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (η.app
              (op
                (CostructuredArrow.left (D := Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)) (S :=
                  (yoneda : C ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v))) (T := A)
                  (unop
                      (op
                        (CostructuredArrow.mk (Y := X)
                          ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A)
                            ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app (op X)) :
                                (a : (fun (X : Type v) ↦ X) (F.obj (op X))) → (fun (X : Type v) ↦ X) (A.obj (op X)))
                              x)))) :
                    CostructuredArrow yoneda A)))) :
          (a :
              (fun (X : Type v) ↦ X)
                (F.obj
                  (op
                    (unop
                        (op
                          (CostructuredArrow.mk
                            ((yonedaEquiv.symm : (a : A.obj (op X)) → yoneda.obj X ⟶ A)
                              ((ConcreteCategory.hom (η.app (op X)) :
                                  (a : (fun (X : Type v) ↦ X) (F.obj (op X))) → (fun (X : Type v) ↦ X) (A.obj (op X)))
                                x))))).left))) →
            (fun (X : Type v) ↦ X)
              (A.obj
                (op
                  (unop
                      (op
                        (CostructuredArrow.mk
                          ((yonedaEquiv.symm : (a : A.obj (op X)) → yoneda.obj X ⟶ A)
                            ((ConcreteCategory.hom (η.app (op X)) :
                                (a : (fun (X : Type v) ↦ X) (F.obj (op X))) → (fun (X : Type v) ↦ X) (A.obj (op X)))
                              x))))).left)))
        x :
      (fun (X : Type v) ↦ X)
        (A.obj
          (op
            (CostructuredArrow.left (D := Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)) (S :=
              (yoneda : C ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v))) (T := A)
              (unop
                  (op
                    (CostructuredArrow.mk (Y := X)
                      ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A)
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app (op X)) :
                            (a : (fun (X : Type v) ↦ X) (F.obj (op X))) → (fun (X : Type v) ↦ X) (A.obj (op X)))
                          x)))) :
                CostructuredArrow yoneda A)))))
    ((yonedaEquiv :
          (a :
              yoneda.obj
                  (unop
                      (op
                        (CostructuredArrow.mk
                          ((yonedaEquiv.symm : (a : A.obj (op X)) → yoneda.obj X ⟶ A)
                            ((ConcreteCategory.hom (η.app (op X)) :
                                (a : (fun (X : Type v) ↦ X) (F.obj (op X))) → (fun (X : Type v) ↦ X) (A.obj (op X)))
                              x))))).left ⟶
                A) →
            A.obj
              (op
                (unop
                    (op
                      (CostructuredArrow.mk
                        ((yonedaEquiv.symm : (a : A.obj (op X)) → yoneda.obj X ⟶ A)
                          ((ConcreteCategory.hom (η.app (op X)) :
                              (a : (fun (X : Type v) ↦ X) (F.obj (op X))) → (fun (X : Type v) ↦ X) (A.obj (op X)))
                            x))))).left))
        (CostructuredArrow.hom
          (unop
            (op
              (CostructuredArrow.mk (Y := X)
                ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app (op X)) :
                      (a : (fun (X : Type v) ↦ X) (F.obj (op X))) → (fun (X : Type v) ↦ X) (A.obj (op X)))
                    x)))))) :
      A.obj
        (op
          (CostructuredArrow.left (D := Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)) (S :=
            (yoneda : C ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v))) (T := A)
            (unop
                (op
                  (CostructuredArrow.mk (Y := X)
                    ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A)
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app (op X)) :
                          (a : (fun (X : Type v) ↦ X) (F.obj (op X))) → (fun (X : Type v) ↦ X) (A.obj (op X)))
                        x)))) :
              CostructuredArrow yoneda A))))

Tactic:
simp