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.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x.1))).map (F.map (↑f).unop).op ≫
          (G.map (uliftYonedaEquiv.symm x.snd)).app (op (F.obj (unop y.fst)))))
      ((hom ((φ.app (unop x.fst)).app (op (F.1 (unop x.fst))))) { down := 𝟙 (unop (op (F.1 (unop x.fst)))) }) =
    (hom ((G.map (uliftYonedaEquiv.symm x.snd)).app (op (F.obj (unop x.fst))) ≫ (G.obj P).map (F.map (↑f).unop).op))
      ((hom ((φ.app (unop x.fst)).app (op (F.1 (unop x.fst))))) { down := 𝟙 (unop (op (F.1 (unop x.fst)))) })
eq₃ :
  (hom (((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).map (↑f).unop ≫ φ.app (unop x.fst)).app (op (F.1 (unop y.fst)))))
      { down := 𝟙 (unop (op (F.1 (unop y.fst)))) } =
    (hom ((φ.app (unop y.fst) ≫ (uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).map (↑f).unop).app (op (F.1 (unop y.fst)))))
      { down := 𝟙 (unop (op (F.1 (unop y.fst)))) }
⊢ uliftYoneda.{max v₂ w, v₁, u₁}.map (↑f).unop ≫ coconeApp φ x = coconeApp φ y

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

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