chore: update mathlib

DynamicalSystems/Basic/LpLoc.lean

@@ -67,7 +67,7 @@ attribute [fun_prop] MemLp MemLp.add MemLp.sub MemLp.neg MemLp.aestronglyMeasura
 
 variable [TopologicalSpace ε] [TopologicalSpace.PseudoMetrizableSpace ε] [ENorm ε]
 
-theorem add_measure {f : α → ε} (hμ : MemLp f p μ) (hν : MemLp f p ν) : MemLp f p (μ + ν) := by
+theorem add_measure' {f : α → ε} (hμ : MemLp f p μ) (hν : MemLp f p ν) : MemLp f p (μ + ν) := by
   rw [memLp_iff]
   grw [eLpNorm_add_measure hμ.aestronglyMeasurable hν.aestronglyMeasurable]
   rw [ENNReal.mul_lt_top_iff, ENNReal.add_lt_top]
@@ -115,7 +115,7 @@ theorem MemLpLoc.indicator [TopologicalSpace ε'] [ESeminormedAddMonoid ε'] (hs
     MemLpLoc (s.indicator f) p μ := by
   intro x
   filter_upwards [hf x] with s' hf
-  exact hf.indicator hs
+  exact hf.indicator hs.nullMeasurableSet
 
 end ENorm
 
@@ -148,7 +148,7 @@ theorem MemLpLoc.memLp_restrict_isCompact (hf : MemLpLoc f p μ) (hs : IsCompact
   · intro s t hst h
     exact h.mono_measure (μ.restrict_mono_set hst)
   · intro s t hs ht
-    apply (hs.add_measure ht).mono_measure
+    apply (hs.add_measure' ht).mono_measure
     exact Measure.restrict_union_le s t
   · intro x hx
     rw [memLpLoc_iff] at hf
@@ -173,13 +173,13 @@ theorem memLpLoc_iff_memLp_indicator [WeaklyLocallyCompactSpace α] [Topological
     MemLpLoc f p μ ↔ ∀ s (_hs : IsCompact s), MemLp (s.indicator f) p μ := by
   rw [memLpLoc_iff_memLp_isCompact]
   congrm (∀ s hs, ?_)
-  exact (memLp_indicator_iff_restrict hs.measurableSet).symm
+  exact (memLp_indicator_iff_restrict hs.nullMeasurableSet).symm
 
 theorem MemLpLoc.memLp_indicator [OpensMeasurableSpace α] [T2Space α]
     [TopologicalSpace ε'] [TopologicalSpace.PseudoMetrizableSpace ε'] [ESeminormedAddMonoid ε']
     {f : α → ε'} (hf : MemLpLoc f p μ) (hs : IsCompact s) :
     MemLp (s.indicator f) p μ := by
-  rw [memLp_indicator_iff_restrict hs.measurableSet]
+  rw [memLp_indicator_iff_restrict hs.nullMeasurableSet]
   exact hf.memLp_restrict_isCompact hs
 
 @[fun_prop]

DynamicalSystems/InputOutput/Stability.lean

@@ -206,7 +206,7 @@ theorem isLpStable (hf : IsFiniteGainStableWith f k β s p μ)
     filter_upwards with t
     calc
       _ = eLpNorm (f u)  p (μ.restrict (s t)) :=
-        eLpNorm_indicator_eq_eLpNorm_restrict (hs.measurableSet t)
+        eLpNorm_indicator_eq_eLpNorm_restrict (hs.measurableSet t).nullMeasurableSet
       _ ≤ k * eLpNorm u p (μ.restrict <| s t) + β := hf.stableWith t u hu.memLpLoc
       _ ≤ _ := by gcongr; exact Measure.restrict_le_self
   calc
@@ -236,17 +236,17 @@ theorem IsCausal.isFiniteGainStableWith (hf : IsCausal f s p μ) (hs : ∀ t, Is
   · intro t u hu
     calc
       _ = eLpNorm ((s t).indicator (f u)) p μ :=
-        (eLpNorm_indicator_eq_eLpNorm_restrict (hs t).measurableSet).symm
+        (eLpNorm_indicator_eq_eLpNorm_restrict (hs t).nullMeasurableSet).symm
       _ = eLpNorm ((s t).indicator (f <| (s t).indicator u)) p μ := by
         rw [← hf.causal t u hu]
       _ ≤ eLpNorm (f <| (s t).indicator u) p μ := by
         apply eLpNorm_indicator_le
-        exact (hs t).measurableSet
+        exact (hs t).nullMeasurableSet
       _ ≤ ↑k * eLpNorm ((s t).indicator u) p μ + β := by
         apply h
         exact hu.memLp_indicator (hs t)
       _ = _ := by
-        rw [eLpNorm_indicator_eq_eLpNorm_restrict (hs t).measurableSet]
+        rw [eLpNorm_indicator_eq_eLpNorm_restrict (hs t).nullMeasurableSet]
 
 end Function
 

DynamicalSystems/Stability/Example.lean

@@ -61,7 +61,7 @@ theorem expFlow_apply (t : 𝕜) (x : E) : A.expFlow t x = NormedSpace.exp (t 
 
 @[fun_prop]
 theorem differentiable_expFlow (x : E) : Differentiable 𝕜 (A.expFlow · x) := by
-  fun_prop
+  fun_prop [ContinuousLinearMap.expFlow]
 
 theorem deriv_expFlow (x : E) : deriv (A.expFlow · x) 0 = A x := by
   simp only [expFlow_apply]
@@ -97,7 +97,7 @@ variable [ProperSpace E]
 /-- The origin is stable under the forward flow of `d/dt x = r x` -/
 theorem isStableOn_expFlow (hA : A.IsPositive) : (𝓝 0).IsStableOn (-A).expFlow (Set.Ici 0) := by
   apply (isLyapunov_inner_expFlow hA).isStableOn_nhds (by simp) (by simp) zero_lt_one
-  convert isCompact_closedBall (0 : E) 1
+  convert isCompact_closedBall (0 : E) 1 using 1
   ext; simp
 
 end InnerProductSpace

DynamicalSystems/Stability/Linearization.lean

@@ -63,7 +63,7 @@ theorem isStableOn_of_isCoercive_inner_comp_neg_fderiv (hf : DifferentiableAt 
     (𝓝 x₀).IsStableOn Φ (Set.Ici 0) := by
   obtain ⟨δ₀, hδ₀, h_lya⟩ := exists_isLyapunovOnIn hf hx₀ h hΦ
   apply h_lya.isStableOn_nhds (δ₀ := δ₀) ?_ (by simp [sub_eq_zero]) (by simp) hδ₀ (by simp)
-  convert isCompact_closedBall x₀ (δ₀ ^ ((1 : ℝ) / 2))
+  convert isCompact_closedBall x₀ (δ₀ ^ ((1 : ℝ) / 2)) using 1
   ext x
   simp only [Set.mem_ofPred_eq, one_div, Metric.mem_closedBall]
   rw [Real.le_rpow_inv_iff_of_pos (by positivity) hδ₀.le (by norm_num), dist_eq_norm]

DynamicalSystems/Stability/Lyapunov.lean

@@ -365,7 +365,7 @@ theorem IsLyapunovOn.isInvariantOn {δ : ℝ} (h_lya : IsLyapunovOn v Φ s) (hs
   have ht₀ : v (Φ t₀ x) ≤ δ := by rwa [h_id]
   have ht₀' : Φ t₀ x ∈ s := by rwa [h_id]
   have h_closed : IsClosed (s ∩ {x | v x ≤ δ}) := by
-    convert hv
+    convert hv using 1
     ext; simp [and_comm]
   refine continuity_method hs (hΦ' x) ht₀ ht₀' h_closed ?_ ht
   intro t (ht : t₀ ≤ t) h

lake-manifest.json

@@ -15,27 +15,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c55e6e786f49471c72fbddbec5415808896aec1e",
+   "rev": "9d581dfff2e41de989072ea63abf3daf69311520",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "c55e6e786f49471c72fbddbec5415808896aec1e",
+   "inputRev": "v4.36.0-rc2",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/verso",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "9f8096e40b31715b1d8d5997f15a0bd832f7e37d",
+   "rev": "71a2035b44e7f54a797ce799fd1b03cdd3a44684",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.35.0-rc2",
+   "inputRev": "v4.36.0-rc2",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fb13df72ecefd8ddbf9291021d7f33a8673eb57b",
+   "rev": "129d1ba9a16bc0660f46c79e9fb041ef5d5d80de",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "29ff470276c725ae01505d55b17148c18fc7dfd3",
+   "rev": "c61286b7b63cbfd563b28e11e81d0a18233a044a",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7e81a29bda33a6b257bd37557a6aa6aebe175d96",
+   "rev": "b8cc5dd0a36233b88a6ed5a7dbf1207d09338c60",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c643bbb3c24f8a25f9c14e3a6b1ceb13d01f3de1",
+   "rev": "16259c0d07d61ee37d999d05b5cf96338b8daa11",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a90fbf7b02ff06a0deebf74088dff9e5fe02c9ea",
+   "rev": "7d11bfa88558f8d3d90afdf6bd877ed70001498d",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "37b0ba0b26109cf9f9c541f0f9557e50cfa1a3b9",
+   "rev": "b0256621cb88178e9ad932a53633077b3029e621",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3b7c8101932390d60e92a3f3d917901d5b5a773b",
+   "rev": "d4c39b228d4a06f3b00748c2c445a7b9f056a6e3",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,17 +105,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "843844fa601dd56767b1eb22b7ada5b64d5e567a",
+   "rev": "c09cb1e4f1e6e1c231a1175a12b681b075054a1b",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.35.0-rc3",
+   "inputRev": "v4.36.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/illuminate",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "68a463c484e24708627b8761e8730e76b295d1e2",
+   "rev": "758bff3509b8e90ca82e37aa5de81de3c9e70fc0",
    "name": "illuminate",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -135,7 +135,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d047cb484b2f3598187450935dbcc84d078cb581",
+   "rev": "892d6dc520270b5fb8c1291dd1b131e8c16255ed",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lakefile.toml

@@ -14,12 +14,12 @@ warn.sorry = true
 [[require]]
 name = "verso"
 scope = "leanprover"
-rev = "v4.35.0-rc2"
+rev = "v4.36.0-rc2"
 
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "c55e6e786f49471c72fbddbec5415808896aec1e"
+rev = "v4.36.0-rc2"
 
 [[require]]
 name = "axiom-audit"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.35.0-rc3
+leanprover/lean4:v4.36.0-rc2