-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
X : Cᵒᵖ
Y Z : Cᵒᵖ ⥤ Type (max w v₁)
f : Y ⟶ Z
g : obj (obj (Functor.op uliftYoneda.{w, v₁, u₁} ⋙ coyoneda) X) Y
h :
  Eq (α := obj (obj (evaluation Cᵒᵖ (Type (max v₁ w))) X) Z)
    (ULift.down
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (map (obj (Functor.op uliftYoneda.{w, v₁, u₁} ⋙ coyoneda) X) f ≫
            Iso.hom
              ((fun (x : Cᵒᵖ ⥤ Type (max w v₁)) ↦
                  (Equiv.toIso (Equiv.trans uliftYonedaEquiv (Equiv.symm Equiv.ulift)) :
                    obj (obj (Functor.op uliftYoneda.{w, v₁, u₁} ⋙ coyoneda) X) x ≅
                      obj
                        (obj
                          (evaluation Cᵒᵖ (Type (max v₁ w)) ⋙
                            obj (whiskeringRight (Cᵒᵖ ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁)))
                              uliftFunctor.{u₁, max v₁ w})
                          X)
                        x))
                Z)))
        g))
    (ULift.down
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom
              ((fun (x : Cᵒᵖ ⥤ Type (max w v₁)) ↦
                  (Equiv.toIso (Equiv.trans uliftYonedaEquiv (Equiv.symm Equiv.ulift)) :
                    obj (obj (Functor.op uliftYoneda.{w, v₁, u₁} ⋙ coyoneda) X) x ≅
                      obj
                        (obj
                          (evaluation Cᵒᵖ (Type (max v₁ w)) ⋙
                            obj (whiskeringRight (Cᵒᵖ ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁)))
                              uliftFunctor.{u₁, max v₁ w})
                          X)
                        x))
                Y) ≫
            map
              (obj
                (evaluation Cᵒᵖ (Type (max v₁ w)) ⋙
                  obj (whiskeringRight (Cᵒᵖ ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁)))
                    uliftFunctor.{u₁, max v₁ w})
                X)
              f))
        g))
⊢ Eq (α :=
    obj
      (obj
        (evaluation Cᵒᵖ (Type (max v₁ w)) ⋙
          obj (whiskeringRight (Cᵒᵖ ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁)))
            uliftFunctor.{u₁, max v₁ w})
        X)
      Z)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (map (obj (Functor.op uliftYoneda.{w, v₁, u₁} ⋙ coyoneda) X) f ≫
          Iso.hom
            ((fun (x : Cᵒᵖ ⥤ Type (max w v₁)) ↦
                (Equiv.toIso (Equiv.trans uliftYonedaEquiv (Equiv.symm Equiv.ulift)) :
                  obj (obj (Functor.op uliftYoneda.{w, v₁, u₁} ⋙ coyoneda) X) x ≅
                    obj
                      (obj
                        (evaluation Cᵒᵖ (Type (max v₁ w)) ⋙
                          obj (whiskeringRight (Cᵒᵖ ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁)))
                            uliftFunctor.{u₁, max v₁ w})
                        X)
                      x))
              Z)))
      g)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (x : Cᵒᵖ ⥤ Type (max w v₁)) ↦
                (Equiv.toIso (Equiv.trans uliftYonedaEquiv (Equiv.symm Equiv.ulift)) :
                  obj (obj (Functor.op uliftYoneda.{w, v₁, u₁} ⋙ coyoneda) X) x ≅
                    obj
                      (obj
                        (evaluation Cᵒᵖ (Type (max v₁ w)) ⋙
                          obj (whiskeringRight (Cᵒᵖ ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁)))
                            uliftFunctor.{u₁, max v₁ w})
                        X)
                      x))
              Y) ≫
          map
            (obj
              (evaluation Cᵒᵖ (Type (max v₁ w)) ⋙
                obj (whiskeringRight (Cᵒᵖ ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁)))
                  uliftFunctor.{u₁, max v₁ w})
              X)
            f))
      g)

Tactic:
rw [← ULift.down_inj]

Premises used: ULift.down_inj