-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
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 v₁
g : obj (obj (Functor.rightOp coyoneda ⋙ coyoneda) Y) F
⊢ Eq (α :=
    obj
      (obj
        (evaluation C (Type v₁) ⋙
          obj (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))) uliftFunctor.{u₁, v₁})
        Z)
      F)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (map (Functor.rightOp coyoneda ⋙ coyoneda) f ≫
            Iso.hom
              ((fun (X : C) ↦
                  (NatIso.ofComponents
                      (fun (x : C ⥤ Type v₁) ↦ Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift))) ⋯ :
                    Iso (C := (C ⥤ Type v₁) ⥤ Type (max u₁ v₁)) (obj (Functor.rightOp coyoneda ⋙ coyoneda) X)
                      (obj
                        (evaluation C (Type v₁) ⋙
                          obj (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))) uliftFunctor.{u₁, v₁})
                        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 v₁) ↦ Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift))) ⋯ :
                    Iso (C := (C ⥤ Type v₁) ⥤ Type (max u₁ v₁)) (obj (Functor.rightOp coyoneda ⋙ coyoneda) X)
                      (obj
                        (evaluation C (Type v₁) ⋙
                          obj (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))) uliftFunctor.{u₁, v₁})
                        X)))
                Y) ≫
            map
              (evaluation C (Type v₁) ⋙
                obj (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))) uliftFunctor.{u₁, v₁})
              f)
          F))
      g)
have w : Eq.{v₁ + 1} (α := obj (obj (evaluation C (Type v₁)) Z) F)
  (ULift.down.{u₁, v₁}
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (map (Functor.rightOp coyoneda ⋙ coyoneda) f ≫
            Iso.hom
              ((fun (X : C) ↦
                  (NatIso.ofComponents
                      (fun (x : C ⥤ Type v₁) ↦ Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift))) sorry :
                    Iso (C := (C ⥤ Type v₁) ⥤ Type (max u₁ v₁)) (obj (Functor.rightOp coyoneda ⋙ coyoneda) X)
                      (obj
                        (evaluation C (Type v₁) ⋙
                          obj (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))) uliftFunctor.{u₁, v₁})
                        X)))
                Z))
          F))
      g))
  (ULift.down.{u₁, v₁}
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Iso.hom
              ((fun (X : C) ↦
                  (NatIso.ofComponents
                      (fun (x : C ⥤ Type v₁) ↦ Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift))) sorry :
                    Iso (C := (C ⥤ Type v₁) ⥤ Type (max u₁ v₁)) (obj (Functor.rightOp coyoneda ⋙ coyoneda) X)
                      (obj
                        (evaluation C (Type v₁) ⋙
                          obj (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))) uliftFunctor.{u₁, v₁})
                        X)))
                Y) ≫
            map
              (evaluation C (Type v₁) ⋙
                obj (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))) uliftFunctor.{u₁, v₁})
              f)
          F))
      g))
Tactic: rw [← ULift.down_inj]