Bump mathlib

LeanCamCombi.lean

@@ -29,7 +29,6 @@ import LeanCamCombi.Mathlib.Analysis.Convex.Independence
 import LeanCamCombi.Mathlib.Analysis.Convex.Normed
 import LeanCamCombi.Mathlib.Analysis.Convex.Segment
 import LeanCamCombi.Mathlib.Analysis.Convex.SimplicialComplex.Basic
-import LeanCamCombi.Mathlib.Combinatorics.Colex
 import LeanCamCombi.Mathlib.Combinatorics.Schnirelmann
 import LeanCamCombi.Mathlib.Combinatorics.SetFamily.Shatter
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Basic
@@ -50,8 +49,8 @@ import LeanCamCombi.Mathlib.Data.Nat.Defs
 import LeanCamCombi.Mathlib.Data.Set.Finite
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
 import LeanCamCombi.Mathlib.GroupTheory.QuotientGroup
-import LeanCamCombi.Mathlib.Init.Function
 import LeanCamCombi.Mathlib.Logic.Basic
+import LeanCamCombi.Mathlib.Logic.Function.Defs
 import LeanCamCombi.Mathlib.Order.ConditionallyCompleteLattice.Basic
 import LeanCamCombi.Mathlib.Order.Interval.Finset.Basic
 import LeanCamCombi.Mathlib.Order.Partition.Finpartition

LeanCamCombi/ConvexityRefactor/StdSimplex.lean

@@ -6,8 +6,8 @@ import Mathlib.GroupTheory.GroupAction.BigOperators
 import LeanCamCombi.Mathlib.Algebra.BigOperators.Finsupp
 import LeanCamCombi.Mathlib.Algebra.Module.BigOperators
 import LeanCamCombi.Mathlib.Data.Finsupp.Order
-import LeanCamCombi.Mathlib.Init.Function
 import LeanCamCombi.Mathlib.Logic.Basic
+import LeanCamCombi.Mathlib.Logic.Function.Defs
 
 noncomputable section
 

LeanCamCombi/KruskalKatona.lean

@@ -3,13 +3,13 @@ Copyright (c) 2020 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta, Yaël Dillies
 -/
+import Mathlib.Combinatorics.Colex
 import Mathlib.Combinatorics.SetFamily.Compression.UV
 import Mathlib.Combinatorics.SetFamily.Intersecting
 import Mathlib.Combinatorics.SetFamily.Shadow
 import Mathlib.Data.Finset.Fin
 import Mathlib.Data.Finset.Sort
 import Mathlib.Data.Finset.Sups
-import LeanCamCombi.Mathlib.Combinatorics.Colex
 
 /-!
 # Kruskal-Katona theorem
@@ -95,7 +95,7 @@ lemma shadow_initSeg [Fintype α] (hs : s.Nonempty) :
     · simpa [ha] using erase_le_erase_min' hts hst.ge (mem_insert_self _ _)
   -- Now show that if t ≤ s - min s, there is j such that t ∪ j ≤ s
   -- We choose j as the smallest thing not in t
-  simp_rw [le_iff_eq_or_lt, lt_iff_exists_forall_lt_mem_iff_mem]
+  simp_rw [le_iff_eq_or_lt, lt_iff_exists_filter_lt, mem_sdiff, filter_inj, and_assoc]
   simp only [toColex_inj, ofColex_toColex, ne_eq, and_imp]
   rintro cards' (rfl | ⟨k, hks, hkt, z⟩)
   -- If t = s - min s, then use j = min s so t ∪ j = s
@@ -158,7 +158,8 @@ the set is being "shifted 'down" as `max U < max V`. -/
 lemma toColex_compress_lt_toColex {hU : U.Nonempty} {hV : V.Nonempty} (h : max' U hU < max' V hV)
     (hA : compress U V s ≠ s) : toColex (compress U V s) < toColex s := by
   rw [compress, ite_ne_right_iff] at hA
-  rw [compress, if_pos hA.1, lt_iff_exists_forall_lt_mem_iff_mem]
+  rw [compress, if_pos hA.1, lt_iff_exists_filter_lt]
+  simp_rw [mem_sdiff (s := s), filter_inj, and_assoc]
   refine ⟨_, hA.1.2 $ max'_mem _ hV, not_mem_sdiff_of_mem_right $ max'_mem _ _, fun a ha ↦ ?_⟩
   have : a ∉ V := fun H ↦ ha.not_le (le_max' _ _ H)
   have : a ∉ U := fun H ↦ ha.not_lt ((le_max' _ _ H).trans_lt h)

LeanCamCombi/Mathlib/Init/Function.lean → LeanCamCombi/Mathlib/Logic/Function/Defs.lean

@@ -1,3 +1,3 @@
-import Mathlib.Init.Function
+import Mathlib.Logic.Function.Defs
 
 alias Function.comp_assoc := Function.comp.assoc

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c0efc1fd2a0bec51bd55c5b17348af13d7419239",
+   "rev": "f27beb10b53350d6c1257ba3a8899df369135cc3",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "27990300a94dd6789254c2ffef4023896d3717c6",
+   "rev": "622d52c803db99ff4ea4fb442c1db9e91aed944c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8a1d23abc6b006c32a3707c8ceec4a51e950f241",
+   "rev": "23c87df3dc33f21c40279c894022a37b71ffa918",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -85,17 +85,27 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c74a052aebee847780e165611099854de050adf7",
+   "rev": "f93115d0209de6db335725dee900d379f40c0317",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/dupuisf/BibtexQuery",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "bd8747df9ee72fca365efa5bd3bd0d8dcd083b9f",
+   "name": "BibtexQuery",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/doc-gen4",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "194403be8599ce1d95afa15113960045f8483c7c",
+   "rev": "b941c425f6f0f1dc45fe13b850ffa7db1bb20d04",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",