Bump mathlib to v4.23.0

Author: YaelDillies

LeanCamCombi/Mathlib/Probability/ProbabilityMassFunction/Constructions.lean

@@ -38,9 +38,7 @@ lemma mem_support_bernoulli'_iff : b ∈ (bernoulli' p hp).support ↔ if b then
     ext q
     by_cases p <;> by_cases q <;> simp [*]
   refine (map_ofFintype _ _ _).trans ?_
-  simp only [this, bernoulli', Finset.mem_filter, Finset.mem_univ, true_and,
-    Finset.mem_disjiUnion, tsub_le_self, eq_iff_iff, Finset.sum_singleton, WithTop.coe_sub,
-    ENNReal.coe_one]
+  simp only [eq_iff_iff, this, Finset.sum_singleton, bernoulli']
   congr 1 with q
   split_ifs <;> simp [ENNReal.sub_sub_cancel WithTop.one_ne_top (ENNReal.coe_le_coe.2 hp)]
 

LeanCamCombi/PlainCombi/KatonaCircle.lean

@@ -82,12 +82,11 @@ def prefixedEquiv (s : Finset α) : prefixed s ≃ Numbering s × Numbering ↑(
         by_cases hx : x ∈ s
         · have : g ⟨x, hx⟩ < #s := by simpa using (g ⟨x, hx⟩).2
           simp [hx, this]
-        · simp [hx, Equiv.symm_apply_eq]
+        · simp [hx]
       val.right_inv n := by
         obtain hns | hsn := lt_or_ge n.1 #s
         · simp [hns]
-        · simp [hsn.not_gt, hsn, dif_neg (mem_compl.1 <| Subtype.prop _), Fin.ext_iff,
-            Fintype.card_subtype_le]
+        · simp [hsn.not_gt, hsn, dif_neg (mem_compl.1 <| Subtype.prop _)]
       property := mem_prefixed.2 fun x ↦ by
         constructor
         · intro hx

LeanCamCombi/PlainCombi/LittlewoodOfford.lean

@@ -22,8 +22,9 @@ lemma exists_littlewood_offord_partition [DecidableEq ι] (hr : 0 < r) (hf : ∀
       #P.parts = (#s).choose (#s / 2) ∧ (∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ s) ∧ ∀ 𝒜 ∈ P.parts,
         (𝒜 : Set (Finset ι)).Pairwise fun u v ↦ r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i) := by
   classical
-  induction' s using Finset.induction with i s hi ih
-  · exact ⟨Finpartition.indiscrete <| singleton_ne_empty _, by simp⟩
+  induction s using Finset.induction with
+  | empty => exact ⟨Finpartition.indiscrete <| singleton_ne_empty _, by simp⟩
+  | insert i s hi ih =>
   obtain ⟨P, hP, hs, hPr⟩ := ih fun j hj ↦ hf _ <| mem_insert_of_mem hj
   clear ih
   obtain ⟨g, hg, hgf⟩ :=

lake-manifest.json

@@ -5,20 +5,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "79e94a093aff4a60fb1b1f92d9681e407124c2ca",
+   "rev": "37df177aaa770670452312393d4e84aaad56e7b6",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": "v4.23.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b100ad4c5d74a464f497aaa8e7c74d86bf39a56f",
+   "rev": "a22e7c1fa7707fb7ea75f2f9fd6b14de2b7b87a9",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
@@ -35,57 +35,57 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "eb164a46de87078f27640ee71e6c3841defc2484",
+   "rev": "7fca1d4a190761bac0028848f73dc9a59fcb4957",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1253a071e6939b0faf5c09d2b30b0bfc79dae407",
+   "rev": "6e47cc88cfbf1601ab364e9a4de5f33f13401ff8",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.68",
+   "inputRev": "v0.0.71",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1256a18522728c2eeed6109b02dd2b8f207a2a3c",
+   "rev": "247ff80701c76760523b5d7c180b27b7708faf38",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "917bfa5064b812b7fbd7112d018ea0b4def25ab3",
+   "rev": "9b703a545097978aef0e7e243ab8b71c32a9ff65",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "240676e9568c254a69be94801889d4b13f3b249f",
+   "rev": "d117e2c28cba42e974bc22568ac999492a34e812",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "c682c91d2d4dd59a7187e2ab977ac25bd1f87329",
+   "rev": "41c5d0b8814dec559e2e1441171db434fe2281cc",
    "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.22.0"
+rev = "v4.23.0"
 
 [[lean_lib]]
 name = "LeanCamCombi"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.22.0
+leanprover/lean4:v4.23.0