-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
f :
  Quiver.Hom (V := CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P ⥤ ℰ)
    (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A)
    (Functor.obj (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) E)
X : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
Y : Cᵒᵖ
x :
  Functor.obj
    (Functor.obj uliftYoneda.{max w v₂, v₁, u₁}
      (CostructuredArrow.left (D := Cᵒᵖ ⥤ Type (max (max w v₂) v₁)) (S :=
        (uliftYoneda.{max w v₂, v₁, u₁} : C ⥤ Cᵒᵖ ⥤ Type (max (max w v₂) v₁))) (T := P)
        (CostructuredArrow.mk (Y := X.left)
            ((Equiv.symm uliftYonedaEquiv : (a : P.obj (op X.left)) → uliftYoneda.{max w v₂, v₁, u₁}.obj X.left ⟶ P)
              ((hom (FC := TypeCat.Fun) (X.hom.app (op X.left)) :
                  (a :
                      (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                        ((uliftYoneda.{max w v₂, v₁, u₁}.obj X.left).obj (op X.left))) →
                    (fun (X : Type (max (max v₁ v₂) w)) ↦ X) (P.obj (op X.left)))
                { down := 𝟙 X.left })) :
          CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)))
    Y
⊢ (hom (FC := TypeCat.Fun)
          ((Functor.map uliftYoneda.{max w v₂, v₁, u₁}
                  (Iso.hom
                    (Iso.refl
                      (CostructuredArrow.left (D := Cᵒᵖ ⥤ Type (max (max w v₂) v₁)) (S :=
                        (uliftYoneda.{max w v₂, v₁, u₁} : C ⥤ Cᵒᵖ ⥤ Type (max (max w v₂) v₁))) (T := P)
                        (CostructuredArrow.mk (Y := X.left)
                            ((Equiv.symm uliftYonedaEquiv :
                                (a : P.obj (op X.left)) → uliftYoneda.{max w v₂, v₁, u₁}.obj X.left ⟶ P)
                              ((hom (FC := TypeCat.Fun) (X.hom.app (op X.left)) :
                                  (a :
                                      (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                                        ((uliftYoneda.{max w v₂, v₁, u₁}.obj X.left).obj (op X.left))) →
                                    (fun (X : Type (max (max v₁ v₂) w)) ↦ X) (P.obj (op X.left)))
                                { down := 𝟙 X.left :
                                  ULift.{max v₂ w, v₁} (Functor.obj (Functor.obj yoneda X.left) (op X.left)) })) :
                          CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)))) ≫
                X.hom).app
            Y)).toFun
      x =
    TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (NatTrans.app
          (CostructuredArrow.hom
            (CostructuredArrow.mk (Y := X.left)
              ((Equiv.symm uliftYonedaEquiv : (a : P.obj (op X.left)) → uliftYoneda.{max w v₂, v₁, u₁}.obj X.left ⟶ P)
                ((hom (FC := TypeCat.Fun) (X.hom.app (op X.left)) :
                    (a :
                        (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                          ((uliftYoneda.{max w v₂, v₁, u₁}.obj X.left).obj (op X.left))) →
                      (fun (X : Type (max (max v₁ v₂) w)) ↦ X) (P.obj (op X.left)))
                  { down := 𝟙 X.left : ULift.{max v₂ w, v₁} (Functor.obj (Functor.obj yoneda X.left) (op X.left)) }))))
          Y))
      x
have w : Eq (α := P.obj Y)
  ((hom (FC := TypeCat.Fun) (X.hom.app Y) : (a : ULift.{max v₂ w, v₁} (unop Y ⟶ X.left)) → P.obj Y)
      { down := x.down ≫ 𝟙 X.left } :
    P.obj Y)
  ((hom (FC := TypeCat.Fun) (P.map x.down.op) : (a : P.obj (op X.left)) → P.obj Y)
      (((@hom _ types TypeCat.Fun _ _ _ _ _ (X.hom.app (op X.left)) :
            TypeCat.Fun (ULift.{max v₂ w, v₁} (X.left ⟶ X.left)) (P.obj (op X.left))) :
          (a : ULift.{max v₂ w, v₁} (X.left ⟶ X.left)) → P.obj (op X.left))
        { down := 𝟙 X.left }) :
    P.obj Y)
Tactic: dsimp