-- Mathlib/CategoryTheory/Limits/Presheaf.lean
@[reassoc (attr := simp)]
lemma coconeApp_naturality {P : Cᵒᵖ ⥤ Type v₁} {x y : P.Elements} (f : x ⟶ y) :
    yoneda.map f.1.unop ≫ coconeApp φ x = coconeApp φ y

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₁, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁
φ : F ⋙ yoneda ⟶ yoneda ⋙ G
P : Cᵒᵖ ⥤ Type v₁
x y : P.Elements
f : x ⟶ y
eq₁ : yoneda.map (↑f).unop ≫ yonedaEquiv.symm x.snd = yonedaEquiv.symm y.snd
eq₂ :
  ((G.obj (yoneda.obj (Opposite.unop x.1))).map (F.map (↑f).unop).op ≫
        (G.map (yonedaEquiv.symm x.snd)).app (Opposite.op (F.obj (Opposite.unop y.fst))))
      ((φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop x.fst)))
        (𝟙 (Opposite.unop (Opposite.op (F.obj (Opposite.unop x.fst)))))) =
    ((G.map (yonedaEquiv.symm x.snd)).app (Opposite.op (F.obj (Opposite.unop x.fst))) ≫
        (G.obj P).map (F.map (↑f).unop).op)
      ((φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop x.fst)))
        (𝟙 (Opposite.unop (Opposite.op (F.obj (Opposite.unop x.fst))))))
eq₃ :
  ((F ⋙ yoneda).map (↑f).unop ≫ φ.app (Opposite.unop x.fst)).app (Opposite.op (F.toPrefunctor.1 (Opposite.unop y.fst)))
      (𝟙 (Opposite.unop (Opposite.op (F.toPrefunctor.1 (Opposite.unop y.fst))))) =
    (φ.app (Opposite.unop y.fst) ≫ (yoneda ⋙ G).map (↑f).unop).app
      (Opposite.op (F.toPrefunctor.1 (Opposite.unop y.fst)))
      (𝟙 (Opposite.unop (Opposite.op (F.toPrefunctor.1 (Opposite.unop y.fst)))))
⊢ yoneda.map (↑f).unop ≫ coconeApp φ x = coconeApp φ y

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

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₁, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁
φ : F ⋙ yoneda ⟶ yoneda ⋙ G
P : Cᵒᵖ ⥤ Type v₁
x y : P.Elements
f : x ⟶ y
eq₁ : yoneda.map (↑f).unop ≫ yonedaEquiv.symm x.snd = yonedaEquiv.symm y.snd
eq₂ :
  ((G.obj (yoneda.obj (Opposite.unop x.1))).map (F.map (↑f).unop).op ≫
        (G.map (yonedaEquiv.symm x.snd)).app (Opposite.op (F.obj (Opposite.unop y.fst))))
      ((φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop x.fst)))
        (𝟙 (Opposite.unop (Opposite.op (F.obj (Opposite.unop x.fst)))))) =
    ((G.map (yonedaEquiv.symm x.snd)).app (Opposite.op (F.obj (Opposite.unop x.fst))) ≫
        (G.obj P).map (F.map (↑f).unop).op)
      ((φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop x.fst)))
        (𝟙 (Opposite.unop (Opposite.op (F.obj (Opposite.unop x.fst))))))
eq₃ :
  ((F ⋙ yoneda).map (↑f).unop ≫ φ.app (Opposite.unop x.fst)).app (Opposite.op (F.toPrefunctor.1 (Opposite.unop y.fst)))
      (𝟙 (Opposite.unop (Opposite.op (F.toPrefunctor.1 (Opposite.unop y.fst))))) =
    (φ.app (Opposite.unop y.fst) ≫ (yoneda ⋙ G).map (↑f).unop).app
      (Opposite.op (F.toPrefunctor.1 (Opposite.unop y.fst)))
      (𝟙 (Opposite.unop (Opposite.op (F.toPrefunctor.1 (Opposite.unop y.fst)))))
eq₄ :
  ∀ (a : ((F ⋙ yoneda).obj (Opposite.unop x.fst)).obj (Opposite.op (F.obj (Opposite.unop x.fst)))),
    (((F ⋙ yoneda).obj (Opposite.unop x.fst)).map (F.map (↑f).unop).op ≫
          (φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop y.fst))))
        a =
      ((φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop x.fst))) ≫
          ((yoneda ⋙ G).obj (Opposite.unop x.fst)).map (F.map (↑f).unop).op)
        a
⊢ yoneda.map (↑f).unop ≫ coconeApp φ x = coconeApp φ y