-- 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 : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : Y ⟶ Z
h :
  ∀ (g : obj (obj (Functor.op yoneda ⋙ coyoneda) X) Y),
    Eq (α :=
      obj
        (obj
          (evaluation Cᵒᵖ (Type v₁) ⋙
            obj (whiskeringRight (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (Type v₁) (Type (max u₁ v₁)))
              uliftFunctor.{u₁, v₁})
          X)
        Z)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (map (obj (Functor.op yoneda ⋙ coyoneda) X) f ≫
            Iso.hom
              ((fun (x : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) ↦
                  (Equiv.toIso (Equiv.trans yonedaEquiv (Equiv.symm Equiv.ulift)) :
                    obj (obj (Functor.op yoneda ⋙ coyoneda) X) x ≅
                      obj
                        (obj
                          (evaluation Cᵒᵖ (Type v₁) ⋙
                            obj
                              (whiskeringRight (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (Type v₁)
                                (Type (max u₁ v₁)))
                              uliftFunctor.{u₁, v₁})
                          X)
                        x))
                Z)))
        g)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom
              ((fun (x : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) ↦
                  (Equiv.toIso (Equiv.trans yonedaEquiv (Equiv.symm Equiv.ulift)) :
                    obj (obj (Functor.op yoneda ⋙ coyoneda) X) x ≅
                      obj
                        (obj
                          (evaluation Cᵒᵖ (Type v₁) ⋙
                            obj
                              (whiskeringRight (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (Type v₁)
                                (Type (max u₁ v₁)))
                              uliftFunctor.{u₁, v₁})
                          X)
                        x))
                Y) ≫
            map
              (obj
                (evaluation Cᵒᵖ (Type v₁) ⋙
                  obj (whiskeringRight (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (Type v₁) (Type (max u₁ v₁)))
                    uliftFunctor.{u₁, v₁})
                X)
              f))
        g)
⊢ Eq (α :=
    obj (obj (Functor.op yoneda ⋙ coyoneda) X) Y ⟶
      obj
        (obj
          (evaluation Cᵒᵖ (Type v₁) ⋙
            obj (whiskeringRight (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (Type v₁) (Type (max u₁ v₁)))
              uliftFunctor.{u₁, v₁})
          X)
        Z)
    (map (obj (Functor.op yoneda ⋙ coyoneda) X) f ≫
      Iso.hom
        ((fun (x : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) ↦
            (Equiv.toIso (Equiv.trans yonedaEquiv (Equiv.symm Equiv.ulift)) :
              obj (obj (Functor.op yoneda ⋙ coyoneda) X) x ≅
                obj
                  (obj
                    (evaluation Cᵒᵖ (Type v₁) ⋙
                      obj (whiskeringRight (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (Type v₁) (Type (max u₁ v₁)))
                        uliftFunctor.{u₁, v₁})
                    X)
                  x))
          Z))
    (Iso.hom
        ((fun (x : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) ↦
            (Equiv.toIso (Equiv.trans yonedaEquiv (Equiv.symm Equiv.ulift)) :
              obj (obj (Functor.op yoneda ⋙ coyoneda) X) x ≅
                obj
                  (obj
                    (evaluation Cᵒᵖ (Type v₁) ⋙
                      obj (whiskeringRight (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (Type v₁) (Type (max u₁ v₁)))
                        uliftFunctor.{u₁, v₁})
                    X)
                  x))
          Y) ≫
      map
        (obj
          (evaluation Cᵒᵖ (Type v₁) ⋙
            obj (whiskeringRight (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (Type v₁) (Type (max u₁ v₁)))
              uliftFunctor.{u₁, v₁})
          X)
        f)

Tactic:
ext g