From e7484e60aeacc624a2ae169d88d24c5ca58a5567 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@himmel-villmar.de>
Date: Mon, 7 Oct 2024 04:38:10 +0000
Subject: [PATCH] feat(CategoryTheory): `map_yonedaEquiv` (#17438)

---
 Mathlib/CategoryTheory/Yoneda.lean | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/Mathlib/CategoryTheory/Yoneda.lean b/Mathlib/CategoryTheory/Yoneda.lean
index 5fbeccb9b2ec8..f06afc7170c1c 100644
--- a/Mathlib/CategoryTheory/Yoneda.lean
+++ b/Mathlib/CategoryTheory/Yoneda.lean
@@ -417,6 +417,7 @@ theorem yonedaEquiv_symm_app_apply {X : C} {F : Cᵒᵖ ⥤ Type v₁} (x : F.ob
     (f : Y.unop ⟶ X) : (yonedaEquiv.symm x).app Y f = F.map f.op x :=
   rfl
 
+/-- See also `yonedaEquiv_naturality'` for a more general version. -/
 lemma yonedaEquiv_naturality {X Y : C} {F : Cᵒᵖ ⥤ Type v₁} (f : yoneda.obj X ⟶ F)
     (g : Y ⟶ X) : F.map g.op (yonedaEquiv f) = yonedaEquiv (yoneda.map g ≫ f) := by
   change (f.app (op X) ≫ F.map g.op) (𝟙 X) = f.app (op Y) (𝟙 Y ≫ g)
@@ -424,6 +425,9 @@ lemma yonedaEquiv_naturality {X Y : C} {F : Cᵒᵖ ⥤ Type v₁} (f : yoneda.o
   dsimp
   simp
 
+/-- Variant of `yonedaEquiv_naturality` with general `g`. This is technically strictly more general
+    than `yonedaEquiv_naturality`, but `yonedaEquiv_naturality` is sometimes preferable because it
+    can avoid the "motive is not type correct" error. -/
 lemma yonedaEquiv_naturality' {X Y : Cᵒᵖ} {F : Cᵒᵖ ⥤ Type v₁} (f : yoneda.obj (unop X) ⟶ F)
     (g : X ⟶ Y) : F.map g (yonedaEquiv f) = yonedaEquiv (yoneda.map g.unop ≫ f) :=
   yonedaEquiv_naturality _ _
@@ -436,6 +440,18 @@ lemma yonedaEquiv_yoneda_map {X Y : C} (f : X ⟶ Y) : yonedaEquiv (yoneda.map f
   rw [yonedaEquiv_apply]
   simp
 
+/-- See also `map_yonedaEquiv'` for a more general version. -/
+lemma map_yonedaEquiv {X Y : C} {F : Cᵒᵖ ⥤ Type v₁} (f : yoneda.obj X ⟶ F)
+    (g : Y ⟶ X) : F.map g.op (yonedaEquiv f) = f.app (op Y) g := by
+  rw [yonedaEquiv_naturality, yonedaEquiv_comp, yonedaEquiv_yoneda_map]
+
+/-- Variant of `map_yonedaEquiv` with general `g`. This is technically strictly more general
+    than `map_yonedaEquiv`, but `map_yonedaEquiv` is sometimes preferable because it
+    can avoid the "motive is not type correct" error. -/
+lemma map_yonedaEquiv' {X Y : Cᵒᵖ} {F : Cᵒᵖ ⥤ Type v₁} (f : yoneda.obj (unop X) ⟶ F)
+    (g : X ⟶ Y) : F.map g (yonedaEquiv f) = f.app Y g.unop := by
+  rw [yonedaEquiv_naturality', yonedaEquiv_comp, yonedaEquiv_yoneda_map]
+
 lemma yonedaEquiv_symm_map {X Y : Cᵒᵖ} (f : X ⟶ Y) {F : Cᵒᵖ ⥤ Type v₁} (t : F.obj X) :
     yonedaEquiv.symm (F.map f t) = yoneda.map f.unop ≫ yonedaEquiv.symm t := by
   obtain ⟨u, rfl⟩ := yonedaEquiv.surjective t
@@ -612,6 +628,10 @@ lemma coyonedaEquiv_coyoneda_map {X Y : C} (f : X ⟶ Y) :
   rw [coyonedaEquiv_apply]
   simp
 
+lemma map_coyonedaEquiv {X Y : C} {F : C ⥤ Type v₁} (f : coyoneda.obj (op X) ⟶ F)
+    (g : X ⟶ Y) : F.map g (coyonedaEquiv f) = f.app Y g := by
+  rw [coyonedaEquiv_naturality, coyonedaEquiv_comp, coyonedaEquiv_coyoneda_map]
+
 lemma coyonedaEquiv_symm_map {X Y : C} (f : X ⟶ Y) {F : C ⥤ Type v₁} (t : F.obj X) :
     coyonedaEquiv.symm (F.map f t) = coyoneda.map f.op ≫ coyonedaEquiv.symm t := by
   obtain ⟨u, rfl⟩ := coyonedaEquiv.surjective t