-- 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)
            (NatTrans.app
              (G.map
                ((Equiv.symm uliftYonedaEquiv : (a : P.obj 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 y.fst)))) →
            (G.obj P).obj (op (F.obj (unop y.fst))))
        ((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) :
            (a : (G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x.1))).obj (op (F.obj (unop x.fst)))) →
              (G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x.1))).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 : ULift.{max v₁ w, v₂} (F.1 (unop x.fst) ⟶ F.obj (unop x.fst))) →
                (G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x.fst))).obj (op (F.1 (unop x.fst))))
            { down := 𝟙 (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) ((G.obj P).map (F.map (↑f : x.fst ⟶ y.fst).unop).op) :
          (a : (G.obj P).obj (op (F.obj (unop x.fst)))) → (G.obj P).obj (op (F.obj (unop y.fst))))
        ((hom (FC := TypeCat.Fun)
              (NatTrans.app
                (G.map
                  ((Equiv.symm uliftYonedaEquiv : (a : P.obj 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)))))) :
            (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 x.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 : ULift.{max v₁ w, v₂} (F.1 (unop x.fst) ⟶ F.obj (unop x.fst))) →
                (G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x.fst))).obj (op (F.1 (unop x.fst))))
            { down := 𝟙 (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 (α :=
    (G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (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)
            (NatTrans.app (φ.app (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))
              (op (F.1 (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) :
          (a : ULift.{max v₁ w, v₂} (F.1 (unop y.fst) ⟶ F.obj (unop x.fst))) →
            (G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x.fst))).obj (op (F.1 (unop y.fst))))
        { down := 𝟙 (F.1 (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))) ≫ F.map (↑f : x.fst ⟶ y.fst).unop } :
      (G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (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)
            (NatTrans.app (G.map (Functor.map uliftYoneda.{max w v₂, v₁, u₁} (↑f : x.fst ⟶ y.fst).unop))
              (op (F.1 (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) :
          (a : (G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop y.fst))).obj (op (F.1 (unop y.fst)))) →
            (G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x.fst))).obj (op (F.1 (unop y.fst))))
        ((hom (FC := TypeCat.Fun)
              (NatTrans.app (φ.app (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))
                (op (F.1 (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) :
            (a : ULift.{max v₁ w, v₂} (F.1 (unop y.fst) ⟶ F.obj (unop y.fst))) →
              (G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop y.fst))).obj (op (F.1 (unop y.fst))))
          { down := 𝟙 (F.1 (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))) }) :
      (G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))).obj
        (op (F.1 (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))))
eq₄ :
  ∀
    (x_1 :
      ToType (FC := TypeCat.Fun)
        (ULift.{max v₁ w, v₂}
          (F.obj (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ⟶ F.obj (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))),
    Eq (α :=
      (G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (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 (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) :
            (a : ULift.{max v₁ w, v₂} (F.obj (unop y.fst) ⟶ F.obj (unop x.fst))) →
              (G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x.fst))).obj (op (F.obj (unop y.fst))))
          { down := F.map (↑f : x.fst ⟶ y.fst).unop ≫ x_1.down } :
        (G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (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)
              ((G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))).map
                (F.map (↑f : x.fst ⟶ y.fst).unop).op) :
            (a : (G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x.fst))).obj (op (F.obj (unop x.fst)))) →
              (G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x.fst))).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.obj (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) :
              (a : ULift.{max v₁ w, v₂} (F.obj (unop x.fst) ⟶ F.obj (unop x.fst))) →
                (G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x.fst))).obj (op (F.obj (unop x.fst))))
            x_1) :
        (G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))).obj
          (op (F.obj (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))))
a :
  Eq (α := (F.op ⋙ G.obj P).obj (op (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))
    ((hom (FC := TypeCat.Fun) ((F.op ⋙ G.obj P).map (↑f : x.fst ⟶ y.fst)) :
          (a : (fun (X : Type (max v₁ v₂ w)) ↦ X) ((F.op ⋙ G.obj P).obj x.fst)) →
            (fun (X : Type (max v₁ v₂ w)) ↦ X) ((F.op ⋙ G.obj P).obj y.fst))
        ((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))))
                (F.op.obj (op (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) :
            (a : (G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x.1))).obj (F.op.obj (op (unop x.fst)))) →
              (G.obj P).obj (F.op.obj (op (unop x.fst))))
          ((hom (FC := TypeCat.Fun)
                (NatTrans.app (φ.app (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))
                  (F.op.obj (op (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) :
              (a : ((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj (unop x.fst)).obj (F.op.obj (op (unop x.fst)))) →
                ((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj (unop x.fst)).obj (F.op.obj (op (unop x.fst))))
            { down := 𝟙 (unop (F.op.obj (op (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) })) :
      (fun (X : Type (max v₁ v₂ w)) ↦ X) ((F.op ⋙ G.obj P).obj (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))
    ((hom (FC := TypeCat.Fun)
            (NatTrans.app
              (G.map
                ((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))))
              (F.op.obj (op (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) :
          (a : (G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop y.1))).obj (F.op.obj (op (unop y.fst)))) →
            (G.obj P).obj (F.op.obj (op (unop y.fst))))
        ((hom (FC := TypeCat.Fun)
              (NatTrans.app (φ.app (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))
                (F.op.obj (op (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) :
            (a : ((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj (unop y.fst)).obj (F.op.obj (op (unop y.fst)))) →
              ((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj (unop y.fst)).obj (F.op.obj (op (unop y.fst))))
          { down := 𝟙 (unop (F.op.obj (op (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) }) :
      (G.obj P).obj (F.op.obj (op (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))))
⊢ Eq (α := (F.op ⋙ G.obj P).obj (op (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))
    ((uliftYonedaEquiv :
          (a : uliftYoneda.{max w v₂, v₁, u₁}.obj (unop y.fst) ⟶ F.op ⋙ G.obj P) →
            (F.op ⋙ G.obj P).obj (op (unop y.fst)))
        (Functor.map uliftYoneda.{max v₂ w, v₁, u₁} (↑f : x.fst ⟶ y.fst).unop ≫
          (Equiv.symm uliftYonedaEquiv :
              (a : (F.op ⋙ G.obj P).obj (op (unop x.fst))) →
                uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x.fst) ⟶ F.op ⋙ G.obj P)
            ((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))))
                    (F.op.obj (op (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) :
                (a : (G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x.1))).obj (F.op.obj (op (unop x.fst)))) →
                  (G.obj P).obj (F.op.obj (op (unop x.fst))))
              ((hom (FC := TypeCat.Fun)
                    (NatTrans.app (φ.app (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))
                      (F.op.obj (op (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) :
                  (a : ((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj (unop x.fst)).obj (F.op.obj (op (unop x.fst)))) →
                    ((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj (unop x.fst)).obj (F.op.obj (op (unop x.fst))))
                { down := 𝟙 (unop (F.op.obj (op (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) }))) :
      (F.op ⋙ G.obj P).obj (op (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))
    ((uliftYonedaEquiv :
          (a : uliftYoneda.{max w v₂, v₁, u₁}.obj (unop y.fst) ⟶ F.op ⋙ G.obj P) →
            (F.op ⋙ G.obj P).obj (op (unop y.fst)))
        ((Equiv.symm uliftYonedaEquiv :
            (a : (F.op ⋙ G.obj P).obj (op (unop y.fst))) →
              uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop y.fst) ⟶ F.op ⋙ G.obj P)
          ((hom (FC := TypeCat.Fun)
                (NatTrans.app
                  (G.map
                    ((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))))
                  (F.op.obj (op (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) :
              (a : (G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop y.1))).obj (F.op.obj (op (unop y.fst)))) →
                (G.obj P).obj (F.op.obj (op (unop y.fst))))
            ((hom (FC := TypeCat.Fun)
                  (NatTrans.app (φ.app (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))
                    (F.op.obj (op (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) :
                (a : ((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj (unop y.fst)).obj (F.op.obj (op (unop y.fst)))) →
                  ((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj (unop y.fst)).obj (F.op.obj (op (unop y.fst))))
              { down := 𝟙 (unop (F.op.obj (op (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) }))) :
      (F.op ⋙ G.obj P).obj (op (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))

Tactic:
rw [Equiv.apply_symm_apply, ← uliftYonedaEquiv_naturality, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, CategoryTheory.uliftYonedaEquiv_naturality