-- 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
X : C
Y Z : C ⥤ Type v₁
f : Y ⟶ Z
⊢ Eq (α :=
    obj (obj (Functor.rightOp coyoneda ⋙ coyoneda) X) Y ⟶
      obj
        (obj
          (evaluation C (Type v₁) ⋙
            obj (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))) uliftFunctor.{u₁, v₁})
          X)
        Z)
    (map (obj (Functor.rightOp coyoneda ⋙ coyoneda) X) f ≫
      Iso.hom
        ((fun (x : C ⥤ Type v₁) ↦
            (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
              obj (obj (Functor.rightOp coyoneda ⋙ coyoneda) X) x ≅
                obj
                  (obj
                    (evaluation C (Type v₁) ⋙
                      obj (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))) uliftFunctor.{u₁, v₁})
                    X)
                  x))
          Z))
    (Iso.hom
        ((fun (x : C ⥤ Type v₁) ↦
            (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
              obj (obj (Functor.rightOp coyoneda ⋙ coyoneda) X) x ≅
                obj
                  (obj
                    (evaluation C (Type v₁) ⋙
                      obj (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))) uliftFunctor.{u₁, v₁})
                    X)
                  x))
          Y) ≫
      map
        (obj
          (evaluation C (Type v₁) ⋙
            obj (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))) uliftFunctor.{u₁, v₁})
          X)
        f)
have h : ∀ (g : obj (obj (Functor.rightOp coyoneda ⋙ coyoneda) X) Y),
  Eq (α :=
    obj
      (obj
        (evaluation C (Type v₁) ⋙
          obj (whiskeringRight (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.rightOp coyoneda ⋙ coyoneda) X) f ≫
          Iso.hom
            ((fun (x : C ⥤ Type v₁) ↦
                (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
                  obj (obj (Functor.rightOp coyoneda ⋙ coyoneda) X) x ≅
                    obj
                      (obj
                        (evaluation C (Type v₁) ⋙
                          obj (whiskeringRight (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 : C ⥤ Type v₁) ↦
                (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
                  obj (obj (Functor.rightOp coyoneda ⋙ coyoneda) X) x ≅
                    obj
                      (obj
                        (evaluation C (Type v₁) ⋙
                          obj (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))) uliftFunctor.{u₁, v₁})
                        X)
                      x))
              Y) ≫
          map
            (obj
              (evaluation C (Type v₁) ⋙
                obj (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))) uliftFunctor.{u₁, v₁})
              X)
            f))
      g)
Tactic: ext g