-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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 : ℰ
g : P ⟶ (restrictedULiftYoneda A).obj E
y y' : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
f : y ⟶ y'
rw :
  Eq (α := A.obj y.left ⟶ E)
    (A.map f.left ≫
      ULift.down
        ((uliftYonedaEquiv :
            (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y'.left ⟶ (restrictedULiftYoneda A).obj E) →
              ((restrictedULiftYoneda A).obj E).obj (op y'.left))
          (y'.hom ≫ g)))
    (ULift.down
      ((uliftYonedaEquiv :
          (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y.left ⟶ (restrictedULiftYoneda A).obj E) →
            ((restrictedULiftYoneda A).obj E).obj (op y.left))
        (y.hom ≫ g)))
rw₁ :
  Eq (α := A.obj y.left ⟶ E)
    (A.map f.left ≫
      ULift.down
        ((uliftYonedaEquiv :
            (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y'.left ⟶ (restrictedULiftYoneda A).obj E) →
              ((restrictedULiftYoneda A).obj E).obj (op y'.left))
          (y'.hom ≫ g)))
    (ULift.down
      ((uliftYonedaEquiv :
          (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y.left ⟶ (restrictedULiftYoneda A).obj E) →
            ((restrictedULiftYoneda A).obj E).obj (op y.left))
        ((Functor.map uliftYoneda.{max w v₂, v₁, u₁} f.left ≫ y'.hom) ≫ g)))
rw₂ :
  Eq (α := A.obj y.left ⟶ E)
    (A.map f.left ≫
      ULift.down
        ((uliftYonedaEquiv :
            (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y'.left ⟶ (restrictedULiftYoneda A).obj E) →
              ((restrictedULiftYoneda A).obj E).obj (op y'.left))
          (y'.hom ≫ g)))
    (ULift.down
      ((uliftYonedaEquiv :
          (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y.left ⟶ (restrictedULiftYoneda A).obj E) →
            ((restrictedULiftYoneda A).obj E).obj (op y.left))
        (Functor.map uliftYoneda.{max w v₂, v₁, u₁} f.left ≫ y'.hom ≫ g)))
rw₃ rw₄ :
  Eq.{v₂ + 1} (α := A.obj y.left ⟶ E)
    (ULift.down
      ((uliftYonedaEquiv :
          (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj y.left ⟶ (restrictedULiftYoneda A).obj E) →
            ((restrictedULiftYoneda A).obj E).obj (op y.left))
        (Functor.map uliftYoneda.{max v₂ w, v₁, u₁} f.left ≫ y'.hom ≫ g)))
    (ULift.down
      ((uliftYonedaEquiv :
          (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y.left ⟶ (restrictedULiftYoneda A).obj E) →
            ((restrictedULiftYoneda A).obj E).obj (op y.left))
        (Functor.map uliftYoneda.{max w v₂, v₁, u₁} f.left ≫ y'.hom ≫ g)))
⊢ A.map f.left ≫
      ULift.down
        ((uliftYonedaEquiv :
            (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y'.left ⟶ (restrictedULiftYoneda A).obj E) →
              ((restrictedULiftYoneda A).obj E).obj (op y'.left))
          (y'.hom ≫ g)) =
    ULift.down
        ((uliftYonedaEquiv :
            (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y.left ⟶ (restrictedULiftYoneda A).obj E) →
              ((restrictedULiftYoneda A).obj E).obj (op y.left))
          (y.hom ≫ g)) ≫
      𝟙 E

Tactic:
rw [comp_id, ← CostructuredArrow.w f, assoc, map_comp_uliftYonedaEquiv_down]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.CostructuredArrow.w, CategoryTheory.Presheaf.map_comp_uliftYonedaEquiv_down