-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
Y Z : C
f : Y ⟶ Z
F : C ⥤ Type (max w v₁)
g : obj (obj (Functor.rightOp uliftCoyoneda.{w, v₁, u₁} ⋙ coyoneda) Y) F
w :
  Eq (α := obj (obj (evaluation C (Type (max v₁ w))) Z) F)
    (ULift.down
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (map (Functor.rightOp uliftCoyoneda.{w, v₁, u₁} ⋙ coyoneda) f ≫
              Iso.hom
                ((fun (X : C) ↦
                    (NatIso.ofComponents
                        (fun (x : C ⥤ Type (max w v₁)) ↦
                          Equiv.toIso (Equiv.trans uliftCoyonedaEquiv (Equiv.symm Equiv.ulift)))
                        ⋯ :
                      Iso (C := (C ⥤ Type (max w v₁)) ⥤ Type (max (max w u₁) v₁))
                        (obj (Functor.rightOp uliftCoyoneda.{w, v₁, u₁} ⋙ coyoneda) X)
                        (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))
            F))
        g))
    (ULift.down
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (Iso.hom
                ((fun (X : C) ↦
                    (NatIso.ofComponents
                        (fun (x : C ⥤ Type (max w v₁)) ↦
                          Equiv.toIso (Equiv.trans uliftCoyonedaEquiv (Equiv.symm Equiv.ulift)))
                        ⋯ :
                      Iso (C := (C ⥤ Type (max w v₁)) ⥤ Type (max (max w u₁) v₁))
                        (obj (Functor.rightOp uliftCoyoneda.{w, v₁, u₁} ⋙ coyoneda) X)
                        (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)))
                  Y) ≫
              map
                (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})
                f)
            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})
        Z)
      F)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (map (Functor.rightOp uliftCoyoneda.{w, v₁, u₁} ⋙ coyoneda) f ≫
            Iso.hom
              ((fun (X : C) ↦
                  (NatIso.ofComponents
                      (fun (x : C ⥤ Type (max w v₁)) ↦
                        Equiv.toIso (Equiv.trans uliftCoyonedaEquiv (Equiv.symm Equiv.ulift)))
                      ⋯ :
                    Iso (C := (C ⥤ Type (max w v₁)) ⥤ Type (max (max w u₁) v₁))
                      (obj (Functor.rightOp uliftCoyoneda.{w, v₁, u₁} ⋙ coyoneda) X)
                      (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))
          F))
      g)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Iso.hom
              ((fun (X : C) ↦
                  (NatIso.ofComponents
                      (fun (x : C ⥤ Type (max w v₁)) ↦
                        Equiv.toIso (Equiv.trans uliftCoyonedaEquiv (Equiv.symm Equiv.ulift)))
                      ⋯ :
                    Iso (C := (C ⥤ Type (max w v₁)) ⥤ Type (max (max w u₁) v₁))
                      (obj (Functor.rightOp uliftCoyoneda.{w, v₁, u₁} ⋙ coyoneda) X)
                      (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)))
                Y) ≫
            map
              (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})
              f)
          F))
      g)

Tactic:
rw [← ULift.down_inj]

Premises used: ULift.down_inj