Merge branch 'main' of https://github.com/emilyriehl/infinity-cosmos

emilyriehl · Sep 26, 2024 · 27cccc3 · 27cccc3
2 parents 1580bf1 + cca4a87
commit 27cccc3
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 9 deletions.
diff --git 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
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9a3cd8cd317d9d5bebb3368c74507801e82dac33",
+   "rev": "aaff5ad5b038e792f9225de7fe6a37c9689b6ec8",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,