chore: cleanup some Yoneda lemma proofs (#10092)

kim-em · kim-em · commit cea4f7aabfdb · 2024-01-29T10:59:18.000Z
While thinking about simp lemmas for opposite categories (for the sake of comonoid objects, for the sake of group objects, for the sake of reductive groups), noticed some of the Yoneda lemma proofs can be golfed.



Co-authored-by: Scott Morrison &lt;scott.morrison@gmail.com&gt;
diff --git a/Mathlib/CategoryTheory/Opposites.lean b/Mathlib/CategoryTheory/Opposites.lean
@@ -498,8 +498,6 @@ between the opposite functors `F.op ≅ G.op`. -/
 protected def removeOp (α : F.op ≅ G.op) : G ≅ F where
   hom := NatTrans.removeOp α.hom
   inv := NatTrans.removeOp α.inv
-  hom_inv_id := by ext; dsimp; rw [← unop_comp]; rw [α.inv_hom_id_app]; rfl
-  inv_hom_id := by ext; dsimp; rw [← unop_comp]; rw [α.hom_inv_id_app]; rfl
 #align category_theory.nat_iso.remove_op CategoryTheory.NatIso.removeOp
 
 /-- The natural isomorphism between functors `G.unop ≅ F.unop` induced by a natural isomorphism
@@ -508,8 +506,6 @@ between the original functors `F ≅ G`. -/
 protected def unop {F G : Cᵒᵖ ⥤ Dᵒᵖ} (α : F ≅ G) : G.unop ≅ F.unop where
   hom := NatTrans.unop α.hom
   inv := NatTrans.unop α.inv
-  hom_inv_id := by ext; dsimp; rw [← unop_comp]; rw [α.inv_hom_id_app]; rfl
-  inv_hom_id := by ext; dsimp; rw [← unop_comp]; rw [α.hom_inv_id_app]; rfl
 #align category_theory.nat_iso.unop CategoryTheory.NatIso.unop
 
 end NatIso
diff --git a/Mathlib/CategoryTheory/Yoneda.lean b/Mathlib/CategoryTheory/Yoneda.lean
@@ -365,35 +365,21 @@ def yonedaLemma : yonedaPairing C ≅ yonedaEvaluation C where
     { app := fun F x => ULift.up ((x.app F.1) (𝟙 (unop F.1)))
       naturality := by
         intro X Y f
-        simp only [yonedaEvaluation]
         ext
-        dsimp
-        erw [Category.id_comp, ← FunctorToTypes.naturality]
-        simp only [Category.comp_id, yoneda_obj_map] }
+        simp [yonedaEvaluation, ← FunctorToTypes.naturality] }
   inv :=
     { app := fun F x =>
-        { app := fun X a => (F.2.map a.op) x.down
-          naturality := by
-            intro X Y f
-            ext
-            dsimp
-            rw [FunctorToTypes.map_comp_apply] }
+        { app := fun X a => (F.2.map a.op) x.down }
       naturality := by
         intro X Y f
-        simp only [yoneda]
         ext
-        dsimp
-        rw [← FunctorToTypes.naturality X.snd Y.snd f.snd, FunctorToTypes.map_comp_apply] }
+        simp [yoneda, ← FunctorToTypes.naturality] }
   hom_inv_id := by
     ext
-    dsimp
-    erw [← FunctorToTypes.naturality, obj_map_id]
-    simp only [yoneda_map_app, Quiver.Hom.unop_op]
-    erw [Category.id_comp]
+    simp [← FunctorToTypes.naturality]
   inv_hom_id := by
     ext
-    dsimp
-    rw [FunctorToTypes.map_id_apply, ULift.up_down]
+    simp [ULift.up_down]
 #align category_theory.yoneda_lemma CategoryTheory.yonedaLemma
 
 variable {C}
