-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
Y : Cᵒᵖ
X Y_1 : C
f : X ⟶ Y_1
g :
  Functor.obj (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) (Functor.obj (evaluation Cᵒᵖ (Type w)) Y)
    (Functor.obj shrinkYoneda.{w, v, u} X)
h :
  ∀ (g : unop Y ⟶ X),
    Eq (α := Functor.obj (Functor.obj coyoneda Y ⋙ uliftFunctor.{w, v}) Y_1)
      (TypeCat.Fun.toFun (X :=
        Functor.obj (shrinkYoneda.{w, v, u} ⋙ Functor.obj (evaluation Cᵒᵖ (Type w)) Y ⋙ uliftFunctor.{v, w}) X)
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Functor.map (shrinkYoneda.{w, v, u} ⋙ Functor.obj (evaluation Cᵒᵖ (Type w)) Y ⋙ uliftFunctor.{v, w}) f ≫
            Iso.hom
              ((fun (X : C) ↦
                  (Equiv.toIso
                      (Equiv.trans Equiv.ulift (Equiv.trans shrinkYonedaObjObjEquiv (Equiv.symm Equiv.ulift))) :
                    ULift.{v, w} (Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y) ≅
                      ULift.{w, v} (unop Y ⟶ X)))
                Y_1)))
        { down := (Equiv.symm shrinkYonedaObjObjEquiv : (a : unop Y ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj Y) g })
      (TypeCat.Fun.toFun (X :=
        Functor.obj (shrinkYoneda.{w, v, u} ⋙ Functor.obj (evaluation Cᵒᵖ (Type w)) Y ⋙ uliftFunctor.{v, w}) X)
        (ConcreteCategory.hom (FC := TypeCat.Fun)
            (Iso.hom
                ((fun (X : C) ↦
                    (Equiv.toIso
                        (Equiv.trans Equiv.ulift (Equiv.trans shrinkYonedaObjObjEquiv (Equiv.symm Equiv.ulift))) :
                      ULift.{v, w} (Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y) ≅
                        ULift.{w, v} (unop Y ⟶ X)))
                  X) ≫
              Functor.map (Functor.obj coyoneda Y ⋙ uliftFunctor.{w, v}) f) :
          TypeCat.Fun
            (Functor.obj (shrinkYoneda.{w, v, u} ⋙ Functor.obj (evaluation Cᵒᵖ (Type w)) Y ⋙ uliftFunctor.{v, w}) X)
            (Functor.obj (Functor.obj coyoneda Y ⋙ uliftFunctor.{w, v}) Y_1))
        ({ down := (Equiv.symm shrinkYonedaObjObjEquiv : (a : unop Y ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj Y) g } :
          ULift.{v, w}
            (Functor.obj (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) (Functor.obj (evaluation Cᵒᵖ (Type w)) Y)
              (Functor.obj shrinkYoneda.{w, v, u} X))))
⊢ Eq (α := Functor.obj (Functor.obj coyoneda Y ⋙ uliftFunctor.{w, v}) Y_1)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Functor.map (shrinkYoneda.{w, v, u} ⋙ Functor.obj (evaluation Cᵒᵖ (Type w)) Y ⋙ uliftFunctor.{v, w}) f ≫
          Iso.hom
            ((fun (X : C) ↦
                (Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.trans shrinkYonedaObjObjEquiv (Equiv.symm Equiv.ulift))) :
                  ULift.{v, w} (Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y) ≅
                    ULift.{w, v} (unop Y ⟶ X)))
              Y_1)))
      { down := g :
        ULift.{v, w}
          (Functor.obj (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) (Functor.obj (evaluation Cᵒᵖ (Type w)) Y)
            (Functor.obj shrinkYoneda.{w, v, u} X)) })
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (X : C) ↦
                (Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.trans shrinkYonedaObjObjEquiv (Equiv.symm Equiv.ulift))) :
                  ULift.{v, w} (Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y) ≅
                    ULift.{w, v} (unop Y ⟶ X)))
              X) ≫
          Functor.map (Functor.obj coyoneda Y ⋙ uliftFunctor.{w, v}) f))
      { down := g :
        ULift.{v, w}
          (Functor.obj (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) (Functor.obj (evaluation Cᵒᵖ (Type w)) Y)
            (Functor.obj shrinkYoneda.{w, v, u} X)) })

Tactic:
obtain ⟨g, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective g

Premises used: CategoryTheory.shrinkYonedaObjObjEquiv, Equiv.surjective, Equiv.symm, rfl