chore: update mathlib

DynamicalSystems/Basic/Autonomous.lean

@@ -91,7 +91,7 @@ theorem IsSemigroupOn.comm [AddCommMagma ι] [Zero ι] (hΦ : IsSemigroupOn Φ s
   rw [← hΦ.add t₀ t₁ x hx, ← hΦ.add t₁ t₀ x hx, add_comm]
 
 variable [TopologicalSpace E] [AddCommMonoid ι] [Preorder ι] [IsDirectedOrder ι] [AddLeftMono ι]
-  [TopologicalSpace ι] [ContinuousAdd ι]
+  [TopologicalSpace ι]
 
 
 open Filter

DynamicalSystems/Engineering/RLCCircuit.lean

@@ -39,7 +39,7 @@ theorem integral_differentiableAt (hf : Continuous f) (a) :
 variable {μ : MeasureTheory.Measure ℝ} {a b : ℝ}
 
 -- should be in mathlib
-theorem integral_nonneg_of_Ioo [MeasureTheory.NoAtoms μ] (hab : a ≤ b)
+theorem integral_nonneg_of_Ioo [MeasureTheory.NullSingletonClass μ] (hab : a ≤ b)
     (hf : IntervalIntegrable f μ a b) (h : ∀ x ∈ Set.Ioo a b, 0 ≤ f x) :
     0 ≤ ∫ u in a..b, f u ∂μ := by
   convert intervalIntegral.integral_mono_on_of_le_Ioo hab _ hf h

lake-manifest.json

@@ -5,27 +5,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f",
+   "rev": "3ee3f85eb48438ad4f8ce98b79a198f6573d5f70",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.31.0",
+   "inputRev": "master-2026-06-22",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/verso",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "891a59f2318e507d7df274c92a8f827dcc6823ea",
+   "rev": "8cb04559a9b9feb8efab43e135f662514561f668",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.31.0-rc1",
+   "inputRev": "v4.32.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc",
+   "rev": "f3f26cc72646205ca167117487c008ee1dafe816",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5c7542ed018c78194f1e2b903eaf6a792b74c03d",
+   "rev": "41f407a8e85b0fdc00910633a8f14754139b63f4",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "24b0d9dc081c5423f8eec7e866c441e5184f29d9",
+   "rev": "e6518a674e62de322b8f79eebeda7bcae2a36bc3",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e3cb2f741431ce31bf73549fb52316a57368b06f",
+   "rev": "b5b9e2bb45ce91e4bc44eaa738c3a8910404ab82",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2",
+   "rev": "7a62bd13860cd39ac98da16ffc8c24d601353f69",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fa08db58b30eb033edcdab331bba000827f9f785",
+   "rev": "7d1b02eb63b526dff04cb990cf05b06b38ccbd3f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "08da3f6f41c075e0c18d37eb0fd417c10ed77b6e",
+   "rev": "ae95e7e7d01c072421732d0b84cf63ff903f4f0e",
    "name": "illuminate",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -115,7 +115,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "ce893b9042128037e2d3c0158b9567fab9fae268",
+   "rev": "0bd508e8362f56d4a05cbf63614d4c97db954041",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -125,10 +125,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "92564e5770e4d09f2d86dfbf8ada1e9c715b384c",
+   "rev": "406ebb8c8e2f7e852a1b47764b42494022ce652c",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.31.0",
+   "inputRev": "v4.32.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "DynamicalSystems",

lakefile.toml

@@ -14,12 +14,12 @@ warn.sorry = false
 [[require]]
 name = "verso"
 scope = "leanprover"
-rev = "v4.31.0"
+rev = "v4.32.0-rc1"
 
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "v4.31.0"
+rev = "master-2026-06-22"
 
 [[lean_lib]]
 name = "DynamicalSystems"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.31.0
+leanprover/lean4:v4.32.0-rc1