diff --git a/LeanMachineLearning/ForMathlib/Probability/Independence/CondDistrib.lean b/LeanMachineLearning/ForMathlib/Probability/Independence/CondDistrib.lean
index b4de6ce5..193345a7 100644
--- a/LeanMachineLearning/ForMathlib/Probability/Independence/CondDistrib.lean
+++ b/LeanMachineLearning/ForMathlib/Probability/Independence/CondDistrib.lean
@@ -10,6 +10,8 @@ public import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
 public import Mathlib.Probability.Independence.Basic
 public import Mathlib.Probability.Independence.Conditional
 
+import Mathlib.Probability.Kernel.CompProdEqIff
+
 /-!
 # Lemmas about conditional distributions
 
diff --git a/LeanMachineLearning/SequentialLearning/FeedbackMartingale.lean b/LeanMachineLearning/SequentialLearning/FeedbackMartingale.lean
index df1f7815..28e3be86 100644
--- a/LeanMachineLearning/SequentialLearning/FeedbackMartingale.lean
+++ b/LeanMachineLearning/SequentialLearning/FeedbackMartingale.lean
@@ -119,7 +119,7 @@ lemma IsAlgEnvSeq.memLp_noiseSum_increment [BorelSpace 𝓨]
     {m : ℕ} (k : 𝓐) (h : IsAlgEnvSeq O A Y alg env P) {p : ℝ≥0∞} (hp1 : 1 ≤ p) (hp_top : p ≠ ∞)
     (hY : MemLp (Y m) p P) :
     MemLp ({ω | A m ω = k}.indicator (fun ω ↦ Y m ω - env.means O A Y (A m ω) m ω)) p P := by
-  refine (hY.sub ?_).indicator (h.measurable_action _ (measurableSet_singleton k))
+  refine (hY.sub ?_).indicator (h.measurable_action _ (measurableSet_singleton k)).nullMeasurableSet
   exact h.memLp_means_action hp1 hp_top hY
 
 lemma IsAlgEnvSeq.memLp_meanSum_increment [BorelSpace 𝓨]
@@ -127,7 +127,7 @@ lemma IsAlgEnvSeq.memLp_meanSum_increment [BorelSpace 𝓨]
     (hY : MemLp (Y m) p P) :
     MemLp ({ω | A m ω = k}.indicator (fun ω ↦ env.means O A Y (A m ω) m ω)) p P := by
   exact (h.memLp_means_action hp1 hp_top hY).indicator
-    (h.measurable_action _ (measurableSet_singleton k))
+    (h.measurable_action _ (measurableSet_singleton k)).nullMeasurableSet
 
 lemma IsAlgEnvSeq.memLp_noiseSum [BorelSpace 𝓨]
     (h : IsAlgEnvSeq O A Y alg env P) {p : ℝ≥0∞} (hp1 : 1 ≤ p) (hp_top : p ≠ ∞)
diff --git a/lake-manifest.json b/lake-manifest.json
index 7043a584..f186ca80 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,27 +5,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f35c415953ee34a1ad5b022fe2ed97c3c77c4093",
+   "rev": "dd56d02cb7a58fa066c4a2c7fddec3cbb59ae8df",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "f35c415953ee34a1ad5b022fe2ed97c3c77c4093",
+   "inputRev": "master",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/verso",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9f8096e40b31715b1d8d5997f15a0bd832f7e37d",
+   "rev": "8fc7a297f14d5adc1a551b5b4ecf283c08bd691f",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.35.0-rc2",
+   "inputRev": "v4.35.0-rc3",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fb13df72ecefd8ddbf9291021d7f33a8673eb57b",
+   "rev": "afc2695efcb6855264d85a45632db1ddc56c8774",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "29ff470276c725ae01505d55b17148c18fc7dfd3",
+   "rev": "50cd21bc62f2c8357c4f269d1185921cbfcdfc90",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a6d31147557d4b044a3ce226768572919acc1def",
+   "rev": "7ad9f2e325aa6cec3dacaa97c2653a98032750eb",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c643bbb3c24f8a25f9c14e3a6b1ceb13d01f3de1",
+   "rev": "87dfe779d5dfd03142ee4fe158911b8eb553ec98",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a90fbf7b02ff06a0deebf74088dff9e5fe02c9ea",
+   "rev": "36cb0105a76ff3de70add8ae91afb6cfc57fafe3",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "37b0ba0b26109cf9f9c541f0f9557e50cfa1a3b9",
+   "rev": "d93a8a0622807953d1e424f0fe2a5f5b5520c12e",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "33131f4fb10067cb3009bf4db615d9680c1ccd6b",
+   "rev": "914928598160c128affd7a42640b4237b7e4d912",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "68a463c484e24708627b8761e8730e76b295d1e2",
+   "rev": "af451aaa73d8f8025189f228642b6e4fe047ce4f",
    "name": "illuminate",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lakefile.toml b/lakefile.toml
index dfe84c20..ec9d572a 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -12,12 +12,12 @@ weak.linter.mathlibStandardSet = true
 [[require]]
 name = "verso"
 git = "https://github.com/leanprover/verso"
-rev = "v4.35.0-rc2"
+rev = "v4.35.0-rc3"
 
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "f35c415953ee34a1ad5b022fe2ed97c3c77c4093"
+rev = "dd56d02cb7a58fa066c4a2c7fddec3cbb59ae8df"
 
 [[lean_lib]]
 name = "LeanMachineLearning"