From 0d79890a0ca0e3df041fe69dc3bb1f3cfbf9a56e Mon Sep 17 00:00:00 2001 From: AlvaroRBO Date: Thu, 26 Sep 2024 14:04:22 -0400 Subject: [PATCH 1/2] Update CodiscreteCat.lean Fix triangle identities on adj' --- .../ForMathlib/AlgebraicTopology/CodiscreteCat.lean | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/InfinityCosmos/ForMathlib/AlgebraicTopology/CodiscreteCat.lean b/InfinityCosmos/ForMathlib/AlgebraicTopology/CodiscreteCat.lean index 1d4673a..7a2f725 100644 --- a/InfinityCosmos/ForMathlib/AlgebraicTopology/CodiscreteCat.lean +++ b/InfinityCosmos/ForMathlib/AlgebraicTopology/CodiscreteCat.lean @@ -122,14 +122,8 @@ def adj' : Cat.objects ⊣ Cod 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 From 80eb40b3e68ae5d8a6dc2f328eae7cad1c5484df Mon Sep 17 00:00:00 2001 From: pitmonticone <38562595+pitmonticone@users.noreply.github.com> Date: Thu, 26 Sep 2024 18:51:42 +0000 Subject: [PATCH 2/2] [create-pull-request] automated change --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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,