Update to v4.33.0

LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean

@@ -35,19 +35,19 @@ end Function
 
 section Argmax
 
-@[to_dual exists_argmin]
+@[to_dual]
 lemma exists_argmax : ∃ i, f i = f.max := by
   obtain ⟨i, -, hi⟩ := Finset.exists_mem_eq_sup' (by simp : Finset.univ.Nonempty) f
   exact ⟨i, hi.symm⟩
 
 /-- The index of the maximum value of a tuple. -/
-@[to_dual argmin /-- The index of the minimum value of a tuple. -/]
+@[to_dual /-- The index of the minimum value of a tuple. -/]
 noncomputable def argmax := (exists_argmax f).choose
 
-@[to_dual argmin_spec]
+@[to_dual]
 lemma argmax_spec : f (argmax f) = f.max := (exists_argmax f).choose_spec
 
-@[to_dual isMinOn_argmin]
+@[to_dual]
 lemma isMaxOn_argmax (x : ι) : f x ≤ f (argmax f) := by
   rw [argmax_spec f]
   exact f.le_max x
@@ -62,7 +62,7 @@ lemma measurable_max [MeasurableSup₂ α] : Measurable (fun (t : ι → α) =>
   ext
   simp [Function.max]
 
-@[to_dual (attr := fun_prop) measurable_argmin]
+@[to_dual (attr := fun_prop)]
 lemma measurable_argmax [MeasurableSpace ι] [MeasurableEq α] [MeasurableSup₂ α] :
     Measurable fun f : ι → α ↦ argmax f := by
   refine measurable_to_countable' fun i ↦ ?_

lake-manifest.json

@@ -5,27 +5,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "51e6992efd06126df61a496bebf8f49482a4e129",
+   "rev": "db584cd6d46c92f209a44c0f1c829460d327499d",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.33.0-rc2",
+   "inputRev": "v4.33.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/verso",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "755ccbe968ad1b0255bee8b46d9cb2306486d6d8",
+   "rev": "3bdedf29bada13d8103e6c979001c51dcee210c8",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.33.0-rc2",
+   "inputRev": "v4.33.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "123d15766ba49356c02ebad2a4462dfe12d79899",
+   "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f5c090429dff3cf66cb65562526c9ea6e8edfbcb",
+   "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "bb3469a87774349fe01898d8bf2fc6a1ce6411ca",
+   "rev": "16f02aa7642864af59f1ff0e384a015994db9118",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "222c58dad7706a6e7cae46c0edd65ea881d3ee27",
+   "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7db8190085343afde2f5d2cdcc9bac719b6ec02c",
+   "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ef42f8944eaf5b6cbfbe75d1917d824c7dd6cf33",
+   "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "76e1c118b0700b4ceafe99532e887d6431625e1a",
+   "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "006dc1d1db18c5dc73d637c926cf132e88df05b5",
+   "rev": "6bc815869cba1f19515715dc6b47795acd521f1c",
    "name": "illuminate",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -115,7 +115,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "4343da18d95390b09fde98efb18125677c4b500c",
+   "rev": "3a75ede05278806fd3249bb0c97a6fb5777a4f7d",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -125,10 +125,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "1319485273bf87833fa472afbcefdedecb16b45f",
+   "rev": "6130a47896ce867c6a4a55373441e59e565bad0f",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.33.0-rc2",
+   "inputRev": "v4.33.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "LeanMachineLearning",

lakefile.toml

@@ -12,12 +12,12 @@ weak.linter.mathlibStandardSet = true
 [[require]]
 name = "verso"
 git = "https://github.com/leanprover/verso"
-rev = "v4.33.0-rc2"
+rev = "v4.33.0"
 
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "v4.33.0-rc2"
+rev = "v4.33.0"
 
 [[lean_lib]]
 name = "LeanMachineLearning"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.33.0-rc2
+leanprover/lean4:v4.33.0