Bump mathlib to v4.21.0

Author: YaelDillies

LeanCamCombi/ExtrProbCombi/BollobasContainment.lean

@@ -37,3 +37,4 @@ lemma one_statement
   sorry
 
 end SimpleGraph
+  

LeanCamCombi/PlainCombi/KatonaCircle.lean

@@ -84,9 +84,9 @@ def prefixedEquiv (s : Finset α) : prefixed s ≃ Numbering s × Numbering ↑(
           simp [hx, this]
         · simp [hx, Equiv.symm_apply_eq]
       val.right_inv n := by
-        obtain hns | hsn := lt_or_le n.1 #s
+        obtain hns | hsn := lt_or_ge n.1 #s
         · simp [hns]
-        · simp [hsn.not_lt, hsn, dif_neg (mem_compl.1 <| Subtype.prop _), Fin.ext_iff,
+        · simp [hsn.not_gt, hsn, dif_neg (mem_compl.1 <| Subtype.prop _), Fin.ext_iff,
             Fintype.card_subtype_le]
       property := mem_prefixed.2 fun x ↦ by
         constructor

LeanCamCombi/PlainCombi/LittlewoodOfford.lean

@@ -40,7 +40,7 @@ lemma card_le_of_forall_dist_sum_le (hr : 0 < r) (h𝒜 : ∀ t ∈ 𝒜, t ⊆
   obtain ⟨P, hP, _hs, hr⟩ := exists_littlewood_offord_partition hr hf
   rw [← hP]
   refine card_le_card_of_forall_subsingleton (· ∈ ·) (fun t ht ↦ ?_) fun ℬ hℬ t ht u hu ↦
-    (hr _ hℬ).eq ht.2 hu.2 (h𝒜r _ ht.1 _ hu.1).not_le
+    (hr _ hℬ).eq ht.2 hu.2 (h𝒜r _ ht.1 _ hu.1).not_ge
   simpa only [exists_prop] using P.exists_mem (mem_powerset.2 <| h𝒜 _ ht)
 
 end Finset

lake-manifest.json

@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5c0c94b3f563ed756b48b9439788c53b0d56a897",
+   "rev": "308445d7985027f538e281e18df29ca16ede2ba3",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.20.1",
+   "inputRev": "v4.21.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2ac43674e92a695e96caac19f4002b25434636da",
+   "rev": "c4aa78186d388e50a436e8362b947bae125a2933",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a11bcb5238149ae5d8a0aa5e2f8eddf8a3a9b27d",
+   "rev": "d07bd64f1910f1cc5e4cc87b6b9c590080e7a457",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "21e6a0522cd2ae6cf88e9da99a1dd010408ab306",
+   "rev": "6980f6ca164de593cb77cd03d8eac549cc444156",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.60",
+   "inputRev": "v0.0.62",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ddfca7829bf8aa4083cdf9633935dddbb28b7b2a",
+   "rev": "8ff27701d003456fd59f13a9212431239d902aef",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2865ea099ab1dd8d6fc93381d77a4ac87a85527a",
+   "rev": "e9c65db4823976353cd0bb03199a172719efbeb7",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7a0d63fbf8fd350e891868a06d9927efa545ac1e",
+   "rev": "8d2067bf518731a70a255d4a61b5c103922c772e",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "f9e25dcbed001489c53bceeb1f1d50bbaf7451d4",
+   "rev": "7c6aef5f75a43ebbba763b44d535175a1b04c9e0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lakefile.toml

@@ -39,7 +39,7 @@ linter.style.setOption = true
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.20.1"
+rev = "v4.21.0"
 
 [[lean_lib]]
 name = "LeanCamCombi"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.20.1
+leanprover/lean4:v4.21.0