Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : 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₁ : uliftYoneda.{max v₂ w, v₁, u₁}.map (↑f).unop ≫ uliftYonedaEquiv.symm x.snd = uliftYonedaEquiv.symm y.snd
eq₂ :
  (hom ((G.map (uliftYonedaEquiv.symm x.snd)).app (op (F.obj (unop y.fst)))))
      ((hom ((G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x.1))).map (F.map (↑f).unop).op))
        ((hom ((φ.app (unop x.fst)).app (op (F.1 (unop x.fst))))) { down := 𝟙 (F.1 (unop x.fst)) })) =
    (hom ((G.obj P).map (F.map (↑f).unop).op))
      ((hom ((G.map (uliftYonedaEquiv.symm x.snd)).app (op (F.obj (unop x.fst)))))
        ((hom ((φ.app (unop x.fst)).app (op (F.1 (unop x.fst))))) { down := 𝟙 (F.1 (unop x.fst)) }))
eq₃ :
  (hom ((φ.app (unop x.fst)).app (op (F.1 (unop y.fst))))) { down := 𝟙 (F.1 (unop y.fst)) ≫ F.map (↑f).unop } =
    (hom ((G.map (uliftYoneda.{max w v₂, v₁, u₁}.map (↑f).unop)).app (op (F.1 (unop y.fst)))))
      ((hom ((φ.app (unop y.fst)).app (op (F.1 (unop y.fst))))) { down := 𝟙 (F.1 (unop y.fst)) })
eq₄ :
  ∀ (x_1 : ToType (ULift.{max v₁ w, v₂} (F.obj (unop x.fst) ⟶ F.obj (unop x.fst)))),
    (hom ((φ.app (unop x.fst)).app (op (F.obj (unop y.fst))))) { down := F.map (↑f).unop ≫ x_1.down } =
      (hom ((G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x.fst))).map (F.map (↑f).unop).op))
        ((hom ((φ.app (unop x.fst)).app (op (F.obj (unop x.fst))))) x_1)
⊢ uliftYonedaEquiv
      (uliftYoneda.{max v₂ w, v₁, u₁}.map (↑f).unop ≫
        uliftYonedaEquiv.symm
          ((hom ((G.map (uliftYonedaEquiv.symm x.snd)).app (F.op.obj (op (unop x.fst)))))
            ((hom ((φ.app (unop x.fst)).app (F.op.obj (op (unop x.fst)))))
              { down := 𝟙 (unop (F.op.obj (op (unop x.fst)))) }))) =
    uliftYonedaEquiv
      (uliftYonedaEquiv.symm
        ((hom ((G.map (uliftYonedaEquiv.symm y.snd)).app (F.op.obj (op (unop y.fst)))))
          ((hom ((φ.app (unop y.fst)).app (F.op.obj (op (unop y.fst)))))
            { down := 𝟙 (unop (F.op.obj (op (unop y.fst)))) })))

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

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : 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₁ : uliftYoneda.{max v₂ w, v₁, u₁}.map (↑f).unop ≫ uliftYonedaEquiv.symm x.snd = uliftYonedaEquiv.symm y.snd
eq₂ :
  (hom ((G.map (uliftYonedaEquiv.symm x.snd)).app (op (F.obj (unop y.fst)))))
      ((hom ((G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x.1))).map (F.map (↑f).unop).op))
        ((hom ((φ.app (unop x.fst)).app (op (F.1 (unop x.fst))))) { down := 𝟙 (F.1 (unop x.fst)) })) =
    (hom ((G.obj P).map (F.map (↑f).unop).op))
      ((hom ((G.map (uliftYonedaEquiv.symm x.snd)).app (op (F.obj (unop x.fst)))))
        ((hom ((φ.app (unop x.fst)).app (op (F.1 (unop x.fst))))) { down := 𝟙 (F.1 (unop x.fst)) }))
eq₃ :
  (hom ((φ.app (unop x.fst)).app (op (F.1 (unop y.fst))))) { down := 𝟙 (F.1 (unop y.fst)) ≫ F.map (↑f).unop } =
    (hom ((G.map (uliftYoneda.{max w v₂, v₁, u₁}.map (↑f).unop)).app (op (F.1 (unop y.fst)))))
      ((hom ((φ.app (unop y.fst)).app (op (F.1 (unop y.fst))))) { down := 𝟙 (F.1 (unop y.fst)) })
eq₄ :
  ∀ (x_1 : ToType (ULift.{max v₁ w, v₂} (F.obj (unop x.fst) ⟶ F.obj (unop x.fst)))),
    (hom ((φ.app (unop x.fst)).app (op (F.obj (unop y.fst))))) { down := F.map (↑f).unop ≫ x_1.down } =
      (hom ((G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x.fst))).map (F.map (↑f).unop).op))
        ((hom ((φ.app (unop x.fst)).app (op (F.obj (unop x.fst))))) x_1)
⊢ (hom ((F.op ⋙ G.obj P).map ↑f))
      ((hom ((G.map (uliftYonedaEquiv.symm x.snd)).app (F.op.obj (op (unop x.fst)))))
        ((hom ((φ.app (unop x.fst)).app (F.op.obj (op (unop x.fst)))))
          { down := 𝟙 (unop (F.op.obj (op (unop x.fst)))) })) =
    (hom ((G.map (uliftYonedaEquiv.symm y.snd)).app (F.op.obj (op (unop y.fst)))))
      ((hom ((φ.app (unop y.fst)).app (F.op.obj (op (unop y.fst))))) { down := 𝟙 (unop (F.op.obj (op (unop y.fst)))) })