Merge pull request #15 from emilyriehl/coherent-iso

Update CodiscreteCat.lean
emilyriehl · Sep 26, 2024 · 0fc736c · 0fc736c
2 parents 41ee2a1 + 55452c9
commit 0fc736c
Showing 1 changed file with 2 additions and 8 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