From ad30c8df673baa36a735e45f1b1254f9a9c3d4b6 Mon Sep 17 00:00:00 2001
From: dagurtomas <dagurtomas@gmail.com>
Date: Fri, 4 Oct 2024 11:08:07 +0000
Subject: [PATCH] fix the build

---
 .../CategoryTheory/Sites/DirectImage.lean     | 11 ++-------
 lake-manifest.json                            | 24 +++++++++++++------
 lean-toolchain                                |  2 +-
 3 files changed, 20 insertions(+), 17 deletions(-)

diff --git a/LeanCondensed/Mathlib/CategoryTheory/Sites/DirectImage.lean b/LeanCondensed/Mathlib/CategoryTheory/Sites/DirectImage.lean
index bf98552..559d4d1 100644
--- a/LeanCondensed/Mathlib/CategoryTheory/Sites/DirectImage.lean
+++ b/LeanCondensed/Mathlib/CategoryTheory/Sites/DirectImage.lean
@@ -33,12 +33,7 @@ lemma inverseDirectImageAdjunction_unit_app_val (X : Sheaf J A) :
     ((inverseDirectImageAdjunction J K A F).unit.app X).val =
     F.op.lanUnit.app X.val ≫ whiskerLeft F.op (toSheafify K (F.op.lan.obj X.val)) := by
   change ((sheafToPresheaf J A).map ((inverseDirectImageAdjunction J K A F).unit.app X)) = _
-  simp only [Functor.id_obj, sheafToPresheaf_obj, Functor.comp_obj, inverseDirectImageAdjunction,
-    Adjunction.comp, whiskeringLeft_obj_obj, Functor.lanAdjunction_unit,
-    Adjunction.map_restrictFullyFaithful_unit_app, NatTrans.comp_app, whiskerLeft_app,
-    whiskerRight_app, sheafificationAdjunction_unit_app, whiskeringLeft_obj_map,
-    Functor.associator_inv_app, Category.comp_id, Iso.refl_hom, NatTrans.id_app, Functor.comp_map,
-    Functor.map_id, whiskerLeft_id']
+  simp [inverseDirectImageAdjunction, -sheafToPresheaf_map]
 
 lemma inverseDirectImageAdjunction_unit_app_val_app (X : Sheaf J A) (Y : C) :
     ((inverseDirectImageAdjunction J K A F).unit.app X).val.app ⟨Y⟩ =
@@ -57,9 +52,7 @@ lemma inverseDirectImageAdjunction_counit_app (X : Sheaf K A) :
     Adjunction.map_restrictFullyFaithful_counit_app, Iso.refl_inv, NatTrans.id_app,
     whiskeringLeft_obj_obj, Functor.comp_map, Category.id_comp]
   erw [Functor.map_id, Functor.map_id]
-  simp only [Adjunction.comp, Functor.comp_obj, sheafToPresheaf_obj, whiskeringLeft_obj_obj,
-    Functor.lanAdjunction_unit, NatTrans.comp_app, Functor.id_obj, Functor.associator_hom_app,
-    whiskerLeft_app, whiskerRight_app, Category.id_comp]
+  simp
 
 def pointTopology : GrothendieckTopology PUnit := ⊥
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 2215d29..879a672 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "31fb27d6b89dc94cf7349df247fc44d2a1d130af",
+   "rev": "13f9b00769bdac2c0041406a6c2524a361e8d660",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222",
+   "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c792cfd1efe6e01cb176e158ddb195bedfb7ad33",
+   "rev": "b20a88676fd00affb90cbc9f1ff004ae588103b3",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,10 +35,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a96aee5245720f588876021b6a0aa73efee49c76",
+   "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.41",
+   "inputRev": "v0.0.42",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -55,17 +55,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6",
+   "rev": "63a7d4a353f48f6c5f1bc19d0f018b0513cb370a",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "781beceb959c68b36d3d96205b3531e341879d2c",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5d1d19d652d9d0f3effa4041727d4c3fca31d5da",
+   "rev": "b758def5262ecb106a626ec885176ed1ece2e4ba",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
diff --git a/lean-toolchain b/lean-toolchain
index e7a4f40..eff86fd 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.11.0-rc2
+leanprover/lean4:v4.13.0-rc3