-- Lean 4 proof step from Mathlib.CategoryTheory.ShrinkYoneda (goal)
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)
⊢ 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)) })
have 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))))
Tactic: obtain ⟨g, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective g
Cleared hypotheses: g