-- 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
w :
  ∀ (F : Cᵒᵖ ⥤ Type (max w v₁)) (g : obj (obj (Functor.op uliftYoneda.{w, v₁, u₁} ⋙ coyoneda) Y) F),
    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.op uliftYoneda.{w, v₁, u₁} ⋙ coyoneda) f ≫
              Iso.hom
                ((fun (X : Cᵒᵖ) ↦
                    (NatIso.ofComponents
                        (fun (x : Cᵒᵖ ⥤ Type (max w v₁)) ↦
                          Equiv.toIso (Equiv.trans uliftYonedaEquiv (Equiv.symm Equiv.ulift)))
                        ⋯ :
                      Iso (C := (Cᵒᵖ ⥤ Type (max w v₁)) ⥤ Type (max (max w u₁) v₁))
                        (obj (Functor.op uliftYoneda.{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 uliftYonedaEquiv (Equiv.symm Equiv.ulift)))
                        ⋯ :
                      Iso (C := (Cᵒᵖ ⥤ Type (max w v₁)) ⥤ Type (max (max w u₁) v₁))
                        (obj (Functor.op uliftYoneda.{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 (α :=
    Quiver.Hom (V := (Cᵒᵖ ⥤ Type (max w v₁)) ⥤ Type (max (max w u₁) v₁))
      (obj (Functor.op uliftYoneda.{w, v₁, u₁} ⋙ coyoneda) Y)
      (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))
    (map (Functor.op uliftYoneda.{w, v₁, u₁} ⋙ coyoneda) f ≫
      Iso.hom
        ((fun (X : Cᵒᵖ) ↦
            (NatIso.ofComponents
                (fun (x : Cᵒᵖ ⥤ Type (max w v₁)) ↦ Equiv.toIso (Equiv.trans uliftYonedaEquiv (Equiv.symm Equiv.ulift)))
                ⋯ :
              Iso (C := (Cᵒᵖ ⥤ Type (max w v₁)) ⥤ Type (max (max w u₁) v₁))
                (obj (Functor.op uliftYoneda.{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))
    (Iso.hom
        ((fun (X : Cᵒᵖ) ↦
            (NatIso.ofComponents
                (fun (x : Cᵒᵖ ⥤ Type (max w v₁)) ↦ Equiv.toIso (Equiv.trans uliftYonedaEquiv (Equiv.symm Equiv.ulift)))
                ⋯ :
              Iso (C := (Cᵒᵖ ⥤ Type (max w v₁)) ⥤ Type (max (max w u₁) v₁))
                (obj (Functor.op uliftYoneda.{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)

Tactic:
ext F g