From 70db27b714dfe56ed8e22da6ad13ef1baacbcc70 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Fri, 27 Sep 2024 06:07:36 +0000
Subject: [PATCH] Bump mathlib

---
 LeanCamCombi.lean                              |  4 +++-
 LeanCamCombi/ConvexityRefactor/StdSimplex.lean |  1 -
 LeanCamCombi/Mathlib/Logic/Function/Defs.lean  |  3 ---
 lake-manifest.json                             | 12 ++++++------
 4 files changed, 9 insertions(+), 11 deletions(-)
 delete mode 100644 LeanCamCombi/Mathlib/Logic/Function/Defs.lean

diff --git a/LeanCamCombi.lean b/LeanCamCombi.lean
index 20c7774d63..2b95dbb015 100644
--- a/LeanCamCombi.lean
+++ b/LeanCamCombi.lean
@@ -23,6 +23,7 @@ import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Finset.Basic
 import LeanCamCombi.Mathlib.Algebra.Module.BigOperators
 import LeanCamCombi.Mathlib.Algebra.Order.BigOperators.LocallyFinite
 import LeanCamCombi.Mathlib.Algebra.Order.Group.Pi
+import LeanCamCombi.Mathlib.Analysis.Convex.Between
 import LeanCamCombi.Mathlib.Analysis.Convex.Exposed
 import LeanCamCombi.Mathlib.Analysis.Convex.Extreme
 import LeanCamCombi.Mathlib.Analysis.Convex.Independence
@@ -48,7 +49,6 @@ import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
 import LeanCamCombi.Mathlib.GroupTheory.QuotientGroup
 import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.AffineMap
 import LeanCamCombi.Mathlib.Logic.Basic
-import LeanCamCombi.Mathlib.Logic.Function.Defs
 import LeanCamCombi.Mathlib.Order.ConditionallyCompleteLattice.Basic
 import LeanCamCombi.Mathlib.Order.Partition.Finpartition
 import LeanCamCombi.Mathlib.Order.Sublattice
@@ -56,6 +56,8 @@ import LeanCamCombi.Mathlib.Probability.Independence.Basic
 import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
 import LeanCamCombi.MetricBetween
 import LeanCamCombi.MinkowskiCaratheodory
+import LeanCamCombi.OrderShatter
+import LeanCamCombi.PhD.VCDim.Basic
 import LeanCamCombi.Sight.Sight
 import LeanCamCombi.SimplicialComplex.Basic
 import LeanCamCombi.SimplicialComplex.Finite
diff --git a/LeanCamCombi/ConvexityRefactor/StdSimplex.lean b/LeanCamCombi/ConvexityRefactor/StdSimplex.lean
index 3c2494e1a8..391bf34329 100644
--- a/LeanCamCombi/ConvexityRefactor/StdSimplex.lean
+++ b/LeanCamCombi/ConvexityRefactor/StdSimplex.lean
@@ -7,7 +7,6 @@ import LeanCamCombi.Mathlib.Algebra.BigOperators.Finsupp
 import LeanCamCombi.Mathlib.Algebra.Module.BigOperators
 import LeanCamCombi.Mathlib.Data.Finsupp.Order
 import LeanCamCombi.Mathlib.Logic.Basic
-import LeanCamCombi.Mathlib.Logic.Function.Defs
 
 noncomputable section
 
diff --git a/LeanCamCombi/Mathlib/Logic/Function/Defs.lean b/LeanCamCombi/Mathlib/Logic/Function/Defs.lean
deleted file mode 100644
index 36887c3ad0..0000000000
--- a/LeanCamCombi/Mathlib/Logic/Function/Defs.lean
+++ /dev/null
@@ -1,3 +0,0 @@
-import Mathlib.Logic.Function.Defs
-
-alias Function.comp_assoc := Function.comp.assoc
diff --git a/lake-manifest.json b/lake-manifest.json
index 025d18b35d..c4a724477a 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "46fed98b5cac2b1ea64e363b420c382ed1af0d85",
+   "rev": "27c99fb6e7a1088b1746fe5a63ef1be077b9dd0b",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "662f986ad3c5ad6ab1a1726b3c04f5ec425aa9f7",
+   "rev": "a895713f7701e295a015b1087f3113fd3d615272",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -61,11 +61,11 @@
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/siddhartha-gadgil/LeanSearchClient.git",
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "c260ed920e2ebd23ef9fc8ca3fd24115e04c18b1",
+   "scope": "leanprover-community",
+   "rev": "2ba60fa2c384a94735454db11a2d523612eaabff",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "1ea941a98905b2166146b60739226f3953fd5290",
+   "rev": "28af5205699f7d1945d148ebb846cd60a08e74a6",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,