-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
x y : P.Elements
f : x ⟶ y
eq₁ :
  Eq (α := Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ⟶ P)
    (Functor.map uliftYoneda.{max v₂ w, v₁, u₁} (↑f : x.fst ⟶ y.fst).unop ≫
      (Equiv.symm uliftYonedaEquiv :
          (a : P.obj (op (unop x.fst))) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x.fst) ⟶ P)
        (x.snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)))
    ((Equiv.symm uliftYonedaEquiv : (a : P.obj (op (unop y.1))) → uliftYoneda.{max w v₂, v₁, u₁}.obj (unop y.1) ⟶ P)
      (y.snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)))
eq₂ :
  Eq (α := (G.obj P).obj (op (F.obj (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))))
    ((hom (FC := TypeCat.Fun)
            ((G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop x.1))).map (F.map (↑f : x.fst ⟶ y.fst).unop).op ≫
              NatTrans.app
                (G.map
                  ((Equiv.symm uliftYonedaEquiv :
                      (a : P.obj (op (unop x.1))) → uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x.1) ⟶ P)
                    (x.snd (β := fun (c : Cᵒᵖ) ↦ P.obj c))))
                (op (F.obj (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) :
          (a : (G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x.1))).obj (op (F.obj (unop x.fst)))) →
            (G.obj P).obj (op (F.obj (unop y.fst))))
        ((hom (FC := TypeCat.Fun)
              (NatTrans.app (φ.app (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))
                (op (F.1 (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) :
            (a :
                (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                  (((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj (unop x.fst)).obj (op (F.1 (unop x.fst))))) →
              (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                (((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj (unop x.fst)).obj (op (F.1 (unop x.fst)))))
          { down := 𝟙 (unop (op (F.1 (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) }) :
      (G.obj P).obj (op (F.obj (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))))
    ((hom (FC := TypeCat.Fun)
            (NatTrans.app
                (G.map
                  ((Equiv.symm uliftYonedaEquiv :
                      (a : P.obj (op (unop x.1))) → uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x.1) ⟶ P)
                    (x.snd (β := fun (c : Cᵒᵖ) ↦ P.obj c))))
                (op (F.obj (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))) ≫
              (G.obj P).map (F.map (↑f : x.fst ⟶ y.fst).unop).op) :
          (a : (G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x.1))).obj (op (F.obj (unop x.fst)))) →
            (G.obj P).obj (op (F.obj (unop y.fst))))
        ((hom (FC := TypeCat.Fun)
              (NatTrans.app (φ.app (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))
                (op (F.1 (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) :
            (a :
                (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                  (((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj (unop x.fst)).obj (op (F.1 (unop x.fst))))) →
              (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                (((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj (unop x.fst)).obj (op (F.1 (unop x.fst)))))
          { down := 𝟙 (unop (op (F.1 (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) }) :
      (G.obj P).obj (op (F.obj (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))))
eq₃ :
  Eq (α :=
    ((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))).obj
      (op (F.1 (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))))
    ((hom (FC := TypeCat.Fun)
            (((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).map (↑f : x.fst ⟶ y.fst).unop ≫
                  φ.app (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))).app
              (op (F.1 (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) :
          (a : ((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj (unop y.fst)).obj (op (F.1 (unop y.fst)))) →
            ((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj (unop x.fst)).obj (op (F.1 (unop y.fst))))
        { down := 𝟙 (unop (op (F.1 (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) } :
      ((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))).obj
        (op (F.1 (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))))
    ((hom (FC := TypeCat.Fun)
            ((φ.app (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ≫
                  (uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).map (↑f : x.fst ⟶ y.fst).unop).app
              (op (F.1 (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) :
          (a : ((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj (unop y.fst)).obj (op (F.1 (unop y.fst)))) →
            ((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj (unop x.fst)).obj (op (F.1 (unop y.fst))))
        { down := 𝟙 (unop (op (F.1 (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) } :
      ((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))).obj
        (op (F.1 (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))))
⊢ ∀
    (x_1 :
      ToType (FC := TypeCat.Fun)
        (((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))).obj
          (op (F.obj (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))))),
    Eq (α :=
      ((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))).obj
        (op (F.obj (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))))
      ((hom (FC := TypeCat.Fun)
              (((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))).map
                  (F.map (↑f : x.fst ⟶ y.fst).unop).op ≫
                NatTrans.app (φ.app (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))
                  (op (F.obj (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) :
            (a : ((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj (unop x.fst)).obj (op (F.obj (unop x.fst)))) →
              ((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj (unop x.fst)).obj (op (F.obj (unop y.fst))))
          x_1 :
        ((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))).obj
          (op (F.obj (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))))
      ((hom (FC := TypeCat.Fun)
              (NatTrans.app (φ.app (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))
                  (op (F.obj (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))) ≫
                ((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))).map
                  (F.map (↑f : x.fst ⟶ y.fst).unop).op) :
            (a : ((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj (unop x.fst)).obj (op (F.obj (unop x.fst)))) →
              ((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj (unop x.fst)).obj (op (F.obj (unop y.fst))))
          x_1 :
        ((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))).obj
          (op (F.obj (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))))

Tactic:
have eq₄ := ConcreteCategory.congr_hom ((φ.app x.1.unop).naturality (F.map f.1.unop).op)