Update Aesop

Fixes a bug in GradedObject.Bifunctor.
leanprover-community · Oct 30, 2024 · d1ce297 · d1ce297
1 parent 20f0817
commit d1ce297
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 5 deletions.
diff --git 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
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "67336380bce17cbb7cf9875ce4552d52d4f30f44",
+   "rev": "4d689f40f352d3e57f7aaac6cac49ec0b9cb4a9d",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "forward-code",