-- Mathlib/CategoryTheory/Limits/Presheaf.lean
lemma yonedaEquiv_ι_presheafHom (P : Cᵒᵖ ⥤ Type v₁) {X : C} (f : yoneda.obj X ⟶ P) :
    yonedaEquiv (f ≫ presheafHom φ P) =
      (G.map f).app (Opposite.op (F.obj X)) ((φ.app X).app _ (𝟙 _))

Proof state:
case intro
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 : C
x : P.obj (Opposite.op X)
⊢ yonedaEquiv
      ({
              pt :=
                { obj := fun X => (G.obj P).obj (F.op.obj X), map := fun {X Y} f => (G.obj P).map (F.op.map f),
                  map_id := ⋯, map_comp := ⋯ },
              ι := { app := fun x => coconeApp φ (Opposite.unop x), naturality := ⋯ } }.ι.app
        (Opposite.op (P.elementsMk (Opposite.op X) x))) =
    (G.map (yonedaEquiv.symm x)).app (Opposite.op (F.obj X))
      ((φ.app X).app (Opposite.op (F.obj X)) (𝟙 (Opposite.unop (Opposite.op (F.obj X)))))

Tactic:
dsimp only [coconeApp]

Result:
case intro
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 : C
x : P.obj (Opposite.op X)
⊢ yonedaEquiv
      (yonedaEquiv.symm
        ((G.map (yonedaEquiv.symm x)).app (F.op.obj (Opposite.op X))
          ((φ.app X).app (F.op.obj (Opposite.op X)) (𝟙 (Opposite.unop (F.op.obj (Opposite.op X))))))) =
    (G.map (yonedaEquiv.symm x)).app (Opposite.op (F.obj X)) ((φ.app X).app (Opposite.op (F.obj X)) (𝟙 (F.obj X)))

Proof state:
case intro
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 : C
x : P.obj (Opposite.op X)
⊢ yonedaEquiv
      (yonedaEquiv.symm
        ((G.map (yonedaEquiv.symm x)).app (F.op.obj (Opposite.op X))
          ((φ.app X).app (F.op.obj (Opposite.op X)) (𝟙 (Opposite.unop (F.op.obj (Opposite.op X))))))) =
    (G.map (yonedaEquiv.symm x)).app (Opposite.op (F.obj X)) ((φ.app X).app (Opposite.op (F.obj X)) (𝟙 (F.obj X)))

Tactic:
apply Equiv.apply_symm_apply

Result:
no goals

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 : C
f : yoneda.obj X ⟶ P
⊢ yonedaEquiv (f ≫ presheafHom φ P) =
    (G.map f).app (Opposite.op (F.obj X))
      ((φ.app X).app (Opposite.op (F.obj X)) (𝟙 (Opposite.unop (Opposite.op (F.obj X)))))

Tactic:
obtain ⟨x, rfl⟩ := yonedaEquiv.symm.surjective f

Result:
case intro
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 : C
x : P.obj (Opposite.op X)
⊢ yonedaEquiv (yonedaEquiv.symm x ≫ presheafHom φ P) =
    (G.map (yonedaEquiv.symm x)).app (Opposite.op (F.obj X))
      ((φ.app X).app (Opposite.op (F.obj X)) (𝟙 (Opposite.unop (Opposite.op (F.obj X)))))

Proof state:
case intro
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 : C
x : P.obj (Opposite.op X)
⊢ yonedaEquiv (yonedaEquiv.symm x ≫ presheafHom φ P) =
    (G.map (yonedaEquiv.symm x)).app (Opposite.op (F.obj X))
      ((φ.app X).app (Opposite.op (F.obj X)) (𝟙 (Opposite.unop (Opposite.op (F.obj X)))))

Tactic:
erw [(colimitOfRepresentable P).fac _ (Opposite.op (P.elementsMk _ x))]

Result:
case intro
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 : C
x : P.obj (Opposite.op X)
⊢ yonedaEquiv
      ({
              pt :=
                { obj := fun X => (G.obj P).obj (F.op.obj X), map := fun {X Y} f => (G.obj P).map (F.op.map f),
                  map_id := ⋯, map_comp := ⋯ },
              ι := { app := fun x => coconeApp φ (Opposite.unop x), naturality := ⋯ } }.ι.app
        (Opposite.op (P.elementsMk (Opposite.op X) x))) =
    (G.map (yonedaEquiv.symm x)).app (Opposite.op (F.obj X))
      ((φ.app X).app (Opposite.op (F.obj X)) (𝟙 (Opposite.unop (Opposite.op (F.obj X)))))