diff --git a/InfinityCosmos/ForMathlib/CategoryTheory/CodiscreteCat.lean b/InfinityCosmos/ForMathlib/CategoryTheory/CodiscreteCat.lean
index 6ccf6bf..da657dc 100644
--- a/InfinityCosmos/ForMathlib/CategoryTheory/CodiscreteCat.lean
+++ b/InfinityCosmos/ForMathlib/CategoryTheory/CodiscreteCat.lean
@@ -111,14 +111,8 @@ def adj' : objects ⊣ functor where
   counit := {
     app := fun _ => id
   }
-  left_triangle_components := by
-    intro _
-    simp only [Functor.id_obj, Functor.comp_obj, id_eq]
-    rfl
-  right_triangle_components := by
-    intro _
-    simp only [Functor.id_obj, Functor.comp_obj, id_eq]
-    rfl
+  left_triangle_components := by aesop
+  right_triangle_components := by aesop
 
 end Codiscrete
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 21a1e48..c9d4a51 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9a3cd8cd317d9d5bebb3368c74507801e82dac33",
+   "rev": "aaff5ad5b038e792f9225de7fe6a37c9689b6ec8",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,