Bump mathlib

LeanCamCombi/KruskalKatona.lean

@@ -317,7 +317,7 @@ lemma kruskal_katona (h₁ : (𝒜 : Set (Finset (Fin n))).Sized r) (h₂ : 𝒜
 This shows that the minimum possible shadow size is attained by initial segments. -/
 lemma strengthened_kk (h₁ : (𝒜 : Set (Finset (Fin n))).Sized r) (h₂ : 𝒞.card ≤ 𝒜.card)
     (h₃ : IsInitSeg 𝒞 r) : (∂ 𝒞).card ≤ (∂ 𝒜).card := by
-  rcases exists_smaller_set 𝒜 𝒞.card h₂ with ⟨𝒜', prop, size⟩
+  obtain ⟨𝒜', prop, size⟩ := exists_subset_card_eq h₂
   refine' (kruskal_katona (fun A hA ↦ h₁ (prop hA)) size h₃).trans (card_le_card _)
   rw [shadow, shadow]
   apply shadow_monotone prop
@@ -374,7 +374,7 @@ lemma lovasz_form (hir : i ≤ r) (hrk : r ≤ k) (hkn : k ≤ n)
     rw [Nat.sub_eq_iff_eq_add hir, ← Ah.2, ← card_sdiff_i, ← card_union_of_disjoint disjoint_sdiff,
       union_sdiff_of_subset BsubA]
   rintro ⟨hBk, hB⟩
-  have := exists_intermediate_set i ?_ hBk
+  have := exists_subsuperset_card_eq hBk (Nat.le_add_left _ i) ?_
   obtain ⟨C, BsubC, hCrange, hcard⟩ := this
   rw [hB, ← Nat.add_sub_assoc hir, Nat.add_sub_cancel_left] at hcard
   refine' ⟨C, _, BsubC, _⟩; rw [mem_powersetCard]; exact ⟨hCrange, hcard⟩

LeanCamCombi/Mathlib/Combinatorics/Schnirelmann.lean

@@ -156,8 +156,7 @@ theorem le_schnirelmannDensity_add (A B : Set ℕ) (hA : 0 ∈ A) (hB : 0 ∈ B)
       rw [next_elm] at hx3
       simp only [mem_Ioc, and_imp, ne_eq, ite_not] at hx3
       split_ifs at hx3 with h
-      · norm_cast at hx3
-        exact hx3.trans (mem_Ioc.1 (mem_filter.1 $ min'_mem _ _).1).2
+      · exact hx3.trans (mem_Ioc.1 (mem_filter.1 $ min'_mem _ _).1).2
       · simpa using hx3
     have aux : countelements (⋃ a : A, {c ∈ A + B | 0 < c - a ∧ (c : ℕ) ≤ (next_elm A a n)}) n ≤
       countelements (A + B) n := by

LeanCamCombi/Mathlib/Data/Finsupp/Order.lean

@@ -1,3 +1,4 @@
+import Mathlib.Algebra.Order.BigOperators.Group.Finset
 import Mathlib.Data.Finsupp.Order
 import LeanCamCombi.Mathlib.Algebra.Order.Group.Pi
 

LeanCamCombi/Mathlib/Data/List/DropRight.lean

@@ -10,14 +10,14 @@ lemma rtake_suffix (n : ℕ) (l : List α) : l.rtake n <:+ l := drop_suffix _ _
 lemma length_rtake (n : ℕ) (l : List α) : (l.rtake n).length = min n l.length :=
   (length_drop _ _).trans $ by rw [Nat.sub_sub_eq_min, min_comm]
 
-@[simp] lemma take_reverse (n : ℕ) (l : List α) : l.reverse.take n = (l.rtake n).reverse := by
+@[simp] lemma take_reverse' (n : ℕ) (l : List α) : l.reverse.take n = (l.rtake n).reverse := by
   rw [rtake_eq_reverse_take_reverse, reverse_reverse]
 
 @[simp] lemma rtake_reverse (n : ℕ) (l : List α) : l.reverse.rtake n = (l.take n).reverse := by
   rw [rtake_eq_reverse_take_reverse, reverse_reverse]
 
 @[simp] lemma rtake_rtake (n m) (l : List α) : (l.rtake m).rtake n = l.rtake (min n m) := by
-  rw [rtake_eq_reverse_take_reverse, ← take_reverse, take_take, rtake_eq_reverse_take_reverse]
+  rw [rtake_eq_reverse_take_reverse, ← take_reverse', take_take, rtake_eq_reverse_take_reverse]
 
 @[simp] lemma rdrop_append_rtake (n : ℕ) (l : List α) : l.rdrop n ++ l.rtake n = l :=
   take_append_drop _ _

lake-manifest.json

@@ -1,10 +1,11 @@
-{"version": "1.0.0",
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "47e4cc5c5800c07d9bf232173c9941fa5bf68589",
+   "scope": "leanprover-community",
+   "rev": "7391b9f9b06eca6fcc36d211db143ba7f84dbe29",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,6 +14,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
+   "scope": "leanprover-community",
    "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
@@ -22,7 +24,8 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "882561b77bd2aaa98bd8665a56821062bdb3034c",
+   "scope": "leanprover-community",
+   "rev": "deb5bd446a108da8aa8c1a1b62dd50722b961b73",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,25 +34,28 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5",
+   "scope": "leanprover-community",
+   "rev": "d1b33202c3a29a079f292de65ea438648123b635",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.36",
+   "inputRev": "v0.0.39",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
+   "scope": "",
    "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/import-graph.git",
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
-   "rev": "1588be870b9c76fe62286e8f42f0b4dafa154c96",
+   "scope": "leanprover-community",
+   "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +64,8 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "cd7c51790cac1a32c321373d45700290b3e8496c",
+   "scope": "",
+   "rev": "69ea8a215c47879fa0a4bd79a7be43c8e85afbe3",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -67,6 +74,7 @@
   {"url": "https://github.com/acmepjz/md4lean",
    "type": "git",
    "subDir": null,
+   "scope": "",
    "rev": "9148a0a7506099963925cf239c491fcda5ed0044",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
@@ -76,7 +84,8 @@
   {"url": "https://github.com/fgdorais/lean4-unicode-basic",
    "type": "git",
    "subDir": null,
-   "rev": "87791b59c53be80a9a000eb2bcbf61f60a27b334",
+   "scope": "",
+   "rev": "c74a052aebee847780e165611099854de050adf7",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +94,8 @@
   {"url": "https://github.com/leanprover/doc-gen4",
    "type": "git",
    "subDir": null,
-   "rev": "1f51169609a3a7c448558c3d3eb353fb355c7025",
+   "scope": "",
+   "rev": "194403be8599ce1d95afa15113960045f8483c7c",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.9.0-rc3
+leanprover/lean4:v4.10.0-rc1