-- Module: Mathlib.CategoryTheory.Category.Cat.Adjunction
Goal:
X : Type u
C : Cat
F : typeToCat.obj X ⟶ C
x x_1 : (↑(of (Discrete ((fun (X : Type u) ↦ X) X))) : Type u)
as as_1 : X
f : { as := as : Discrete ((fun (X : Type u) ↦ X) X) } ⟶ { as := as_1 }
obtain :
  ∀ (f : { as := as : Discrete ((fun (X : Type u) ↦ X) X) } ⟶ { as := { as := as }.as }),
    Eq (α :=
      Quiver.Hom (V := (↑(of ((fun (X : Type u) ↦ X) (objects.obj C))) : Type u))
        (Functor.obj
          (Hom.toFunctor
            ((fun (f : X ⟶ objects.obj C) ↦
                (Functor.toCatHom
                    (Discrete.functor
                      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                        (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (objects.obj C))) :
                  of (Discrete ((fun (X : Type u) ↦ X) X)) ⟶ of ((fun (X : Type u) ↦ X) (objects.obj C))))
              ((fun (F : typeToCat.obj X ⟶ C) ↦ (↾fun (x : X) ↦ F.toFunctor.obj { as := x } : X ⟶ objects.obj C)) F)))
          { as := as : Discrete ((fun (X : Type u) ↦ X) X) })
        (Functor.obj
          (Hom.toFunctor
            ((fun (f : X ⟶ objects.obj C) ↦
                (Functor.toCatHom
                    (Discrete.functor
                      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                        (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (objects.obj C))) :
                  of (Discrete ((fun (X : Type u) ↦ X) X)) ⟶ of ((fun (X : Type u) ↦ X) (objects.obj C))))
              ((fun (F : typeToCat.obj X ⟶ C) ↦ (↾fun (x : X) ↦ F.toFunctor.obj { as := x } : X ⟶ objects.obj C)) F)))
          { as := { as := as : Discrete ((fun (X : Type u) ↦ X) X) }.as : Discrete ((fun (X : Type u) ↦ X) X) }))
      (Functor.map
        (Hom.toFunctor
          ((fun (f : X ⟶ objects.obj C) ↦
              (Functor.toCatHom
                  (Discrete.functor
                    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                      (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (objects.obj C))) :
                of (Discrete ((fun (X : Type u) ↦ X) X)) ⟶ of ((fun (X : Type u) ↦ X) (objects.obj C))))
            ((fun (F : typeToCat.obj X ⟶ C) ↦ (↾fun (x : X) ↦ F.toFunctor.obj { as := x } : X ⟶ objects.obj C)) F)))
        f)
      (eqToHom ⋯ ≫ F.toFunctor.map f ≫ eqToHom ⋯)
⊢ Eq (α :=
    Quiver.Hom (V := (↑(of ((fun (X : Type u) ↦ X) (objects.obj C))) : Type u))
      (Functor.obj
        (Hom.toFunctor
          ((fun (f : X ⟶ objects.obj C) ↦
              (Functor.toCatHom
                  (Discrete.functor
                    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                      (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (objects.obj C))) :
                of (Discrete ((fun (X : Type u) ↦ X) X)) ⟶ of ((fun (X : Type u) ↦ X) (objects.obj C))))
            ((fun (F : typeToCat.obj X ⟶ C) ↦ (↾fun (x : X) ↦ F.toFunctor.obj { as := x } : X ⟶ objects.obj C)) F)))
        { as := as : Discrete ((fun (X : Type u) ↦ X) X) })
      (Functor.obj
        (Hom.toFunctor
          ((fun (f : X ⟶ objects.obj C) ↦
              (Functor.toCatHom
                  (Discrete.functor
                    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                      (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (objects.obj C))) :
                of (Discrete ((fun (X : Type u) ↦ X) X)) ⟶ of ((fun (X : Type u) ↦ X) (objects.obj C))))
            ((fun (F : typeToCat.obj X ⟶ C) ↦ (↾fun (x : X) ↦ F.toFunctor.obj { as := x } : X ⟶ objects.obj C)) F)))
        { as := as_1 : Discrete ((fun (X : Type u) ↦ X) X) }))
    (Functor.map
      (Hom.toFunctor
        ((fun (f : X ⟶ objects.obj C) ↦
            (Functor.toCatHom
                (Discrete.functor
                  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                    (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (objects.obj C))) :
              of (Discrete ((fun (X : Type u) ↦ X) X)) ⟶ of ((fun (X : Type u) ↦ X) (objects.obj C))))
          ((fun (F : typeToCat.obj X ⟶ C) ↦ (↾fun (x : X) ↦ F.toFunctor.obj { as := x } : X ⟶ objects.obj C)) F)))
      f)
    (eqToHom ⋯ ≫ F.toFunctor.map f ≫ eqToHom ⋯)

Tactic:
obtain rfl := Discrete.eq_of_hom f

Premises used: CategoryTheory.Discrete.eq_of_hom, rfl