-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Cat.Adjunction (goal)
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 }
⊢ 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 ⋯)
have 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 sorry ≫ F.toFunctor.map f ≫ eqToHom sorry)
Tactic: obtain rfl := Discrete.eq_of_hom f
Cleared hypotheses: as_1, f