From d1ce297610adde3b6a44461c1bf049a2e4d72071 Mon Sep 17 00:00:00 2001 From: Jannis Limperg Date: Thu, 31 Oct 2024 00:19:36 +0100 Subject: [PATCH] Update Aesop Fixes a bug in GradedObject.Bifunctor. --- Mathlib/CategoryTheory/GradedObject/Bifunctor.lean | 7 +++---- lake-manifest.json | 2 +- 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/Mathlib/CategoryTheory/GradedObject/Bifunctor.lean b/Mathlib/CategoryTheory/GradedObject/Bifunctor.lean index 0f044cf378c54..1cb425a581231 100644 --- a/Mathlib/CategoryTheory/GradedObject/Bifunctor.lean +++ b/Mathlib/CategoryTheory/GradedObject/Bifunctor.lean @@ -91,10 +91,9 @@ example {X₁ X₂ : GradedObject I C₁} (f : X₁ ⟶ X₂) [HasMap (((mapBifunctor F I J).obj X₁).obj Y₁) p] [HasMap (((mapBifunctor F I J).obj X₂).obj Y₂) p] (i : I) (j : J) (k : K) (h : p ⟨i, j⟩ = k) : True := by - -- FIXME bug - -- saturate [ιMapBifunctorMapObj, mapBifunctorMapMap, ι_mapMap, mapBifunctor_obj_obj, - -- categoryOfGradedObjects_comp, mapBifunctor_map_app, mapBifunctor_obj_map, - -- @assoc] + saturate [ιMapBifunctorMapObj, mapBifunctorMapMap, ι_mapMap, mapBifunctor_obj_obj, + categoryOfGradedObjects_comp, mapBifunctor_map_app, mapBifunctor_obj_map, + @assoc] trivial set_option aesop.dev.statefulForward true in diff --git a/lake-manifest.json b/lake-manifest.json index 4d1d217ea200d..ced3ea1f0eee5 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "67336380bce17cbb7cf9875ce4552d52d4f30f44", + "rev": "4d689f40f352d3e57f7aaac6cac49ec0b9cb4a9d", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "forward-code",