diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml
index e6f955b5..d7846650 100644
--- a/.github/workflows/blueprint.yml
+++ b/.github/workflows/blueprint.yml
@@ -25,24 +25,35 @@ jobs:
     runs-on: ubuntu-latest
     name: Build project
     steps:
+      - name: Cleanup to free disk space
+        uses: jlumbroso/free-disk-space@main
+        with:
+          # this might remove tools that are actually needed,
+          # if set to "true" but frees about 6 GB
+          tool-cache: false
+          # all of these default to true, but feel free to set to
+          # "false" if necessary for your workflow
+          android: true
+          dotnet: false
+          haskell: false
+          large-packages: false
+          docker-images: false
+          swap-storage: false
+
       - name: Checkout project
         uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
         with:
           fetch-depth: 0 # Fetch all history for all branches and tags
 
-      - name: Build the project
-        uses: leanprover/lean-action@434f25c2f80ded67bba02502ad3a86f25db50709 # v1.3.0
+      - name: Build and lint project
+        uses: leanprover/lean-action@434f25c2f80ded67bba02502ad3a86f25db50709 # 2025-07-02
         with:
-          use-github-cache: false
-
-      - name: check that LeanBandits.lean is up to date
-        run: ~/.elan/bin/lake exe mk_all --check
-
-      - name: Lint project
-        run: env LEAN_ABORT_ON_PANIC=1 ~/.elan/bin/lake exe runLinter LeanBandits
+          build: true
+          lint: true
+          mk_all-check: true
 
       - name: Compile blueprint and documentation
-        uses: leanprover-community/docgen-action@1417dc7f90338c875da5e5870c03a287d8348896 # docgen-action#11
+        uses: leanprover-community/docgen-action@deed0cdc44dd8e5de07a300773eb751d33e32fc8 # 2025-10-26
         with:
           blueprint: true
           homepage: home_page
diff --git a/LeanBandits/ForMathlib/CondDistrib.lean b/LeanBandits/ForMathlib/CondDistrib.lean
index ffc4ae1c..9aa67375 100644
--- a/LeanBandits/ForMathlib/CondDistrib.lean
+++ b/LeanBandits/ForMathlib/CondDistrib.lean
@@ -87,7 +87,8 @@ lemma CondIndepFun.of_prod_left {ε : Type*} {mε : MeasurableSpace ε}
     X ⟂ᵢ[Z, hZ; μ] Y :=
   Kernel.IndepFun.of_prod_left h
 
-lemma CondIndepFun.prod_right [StandardBorelSpace α] [IsFiniteMeasure μ]
+lemma CondIndepFun.prod_right [StandardBorelSpace α] [StandardBorelSpace β] [Nonempty β]
+    [StandardBorelSpace γ] [Nonempty γ] [StandardBorelSpace δ] [Nonempty δ] [IsFiniteMeasure μ]
     {X : α → β} {Y : α → γ} {Z : α → δ}
     (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
     (h : X ⟂ᵢ[Z, hZ; μ] Y) :
diff --git a/LeanBandits/RewardByCountMeasure.lean b/LeanBandits/RewardByCountMeasure.lean
index 612d5937..cc8ded25 100644
--- a/LeanBandits/RewardByCountMeasure.lean
+++ b/LeanBandits/RewardByCountMeasure.lean
@@ -117,34 +117,34 @@ notation "𝓛[" Y " | " X " in " s "; " μ "]" => Measure.map Y (μ[|X ⁻¹' s
 /-- Law of `Y` conditioned on the event that `X` equals `x`. -/
 notation "𝓛[" Y " | " X " ← " x "; " μ "]" => Measure.map Y (μ[|X ⁻¹' {x}])
 
+local notation "𝔓t" => Bandit.trajMeasure alg ν
+local notation "𝔓" => Bandit.measure alg ν
+
 omit [DecidableEq α] [MeasurableSingletonClass α] in
 lemma condDistrib_reward'' [StandardBorelSpace α] [Nonempty α] (n : ℕ) :
-    𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1; Bandit.measure alg ν]
-      =ᵐ[(Bandit.measure alg ν).map (fun ω ↦ arm n ω.1)] ν := by
-  let μ := Bandit.measure alg ν
-  have h_ra' : 𝓛[reward n | arm n; Bandit.trajMeasure alg ν]
-      =ᵐ[(Bandit.trajMeasure alg ν).map (arm n)] ν := condDistrib_reward alg ν n
-  have h_law : μ.map (fun ω ↦ arm n ω.1) = (Bandit.trajMeasure alg ν).map (arm n) := by
-    calc μ.map (fun ω ↦ arm n ω.1)
-    _ = (μ.map (fun ω ↦ ω.1)).map (fun ω ↦ arm n ω) := by
+    𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1; 𝔓]
+      =ᵐ[(𝔓).map (fun ω ↦ arm n ω.1)] ν := by
+  have h_ra' : 𝓛[reward n | arm n; 𝔓t] =ᵐ[(𝔓t).map (arm n)] ν := condDistrib_reward alg ν n
+  have h_law : (𝔓).map (fun ω ↦ arm n ω.1) = (𝔓t).map (arm n) := by
+    calc (𝔓).map (fun ω ↦ arm n ω.1)
+    _ = ((𝔓).map (fun ω ↦ ω.1)).map (fun ω ↦ arm n ω) := by
       rw [Measure.map_map (by fun_prop) (by fun_prop)]
       rfl
-    _ = _ := by unfold μ Bandit.measure; simp [Measure.map_fst_prod]
+    _ = _ := by unfold Bandit.measure; simp [Measure.map_fst_prod]
   rw [h_law]
-  have h_prod : 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1; μ]
-      =ᵐ[(Bandit.trajMeasure alg ν).map (arm n)] 𝓛[reward n | arm n; Bandit.trajMeasure alg ν] :=
+  have h_prod : 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1; 𝔓]
+      =ᵐ[(𝔓t).map (arm n)] 𝓛[reward n | arm n; 𝔓t] :=
     condDistrib_fst_prod _ (by fun_prop) _
   filter_upwards [h_ra', h_prod] with ω h_eq h_prod
   rw [h_prod, h_eq]
 
 omit [DecidableEq α] in
 lemma reward_cond_arm [StandardBorelSpace α] [Nonempty α] [Countable α] (a : α) (n : ℕ)
-    (hμa : (Bandit.measure alg ν).map (fun ω ↦ arm n ω.1) {a} ≠ 0) :
-    𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1 ← a; Bandit.measure alg ν] = ν a := by
-  let μ := Bandit.measure alg ν
-  have h_ra : 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1; μ] =ᵐ[μ.map (fun ω ↦ arm n ω.1)] ν :=
+    (hμa : (𝔓).map (fun ω ↦ arm n ω.1) {a} ≠ 0) :
+    𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1 ← a; 𝔓] = ν a := by
+  have h_ra : 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1; 𝔓] =ᵐ[(𝔓).map (fun ω ↦ arm n ω.1)] ν :=
     condDistrib_reward'' n
-  have h_eq := condDistrib_ae_eq_cond (μ := μ)
+  have h_eq := condDistrib_ae_eq_cond (μ := 𝔓)
     (X := fun ω ↦ arm n ω.1) (Y := fun ω ↦ reward n ω.1) (by fun_prop) (by fun_prop)
   rw [Filter.EventuallyEq, ae_iff_of_countable] at h_ra h_eq
   specialize h_ra a hμa
@@ -194,9 +194,7 @@ lemma measurableSet_stepsUntil_eq (a : α) (m n : ℕ) :
 
 lemma condIndepFun_reward_stepsUntil_arm' [StandardBorelSpace α] [Countable α] [Nonempty α]
     (a : α) (m n : ℕ) (hm : m ≠ 0) :
-    CondIndepFun (mα.comap (arm n)) (measurable_arm n).comap_le
-      (reward n) ({ω | stepsUntil a m ω = ↑n}.indicator (fun _ ↦ 1))
-      (Bandit.trajMeasure alg ν) := by
+    reward n ⟂ᵢ[arm n, measurable_arm n; 𝔓t] {ω | stepsUntil a m ω = ↑n}.indicator (fun _ ↦ 1) := by
   -- the indicator of `stepsUntil ... = n` is a function of
   -- `hist (n-1)` and `arm n`.
   -- It thus suffices to prove the independence of `reward n` and `hist (n-1)` conditionally
@@ -207,7 +205,7 @@ lemma condIndepFun_reward_stepsUntil_arm' [StandardBorelSpace α] [Countable α]
     by_cases hm1 : m = 1
     · simp only [hm1, true_and]
       have h_indep := condIndepFun_self_right (X := reward 0) (Z := arm 0)
-        (mβ := inferInstance) (mβ' := inferInstance) (μ := Bandit.trajMeasure alg ν)
+        (mβ := inferInstance) (mβ' := inferInstance) (μ := 𝔓t)
         (by fun_prop) (by fun_prop)
       have : {ω : ℕ → α × ℝ | arm 0 ω = a}.indicator (fun x ↦ 1)
           = {b | b = a}.indicator (fun _ ↦ 1) ∘ arm 0 := by ext; simp [Set.indicator]
@@ -215,12 +213,10 @@ lemma condIndepFun_reward_stepsUntil_arm' [StandardBorelSpace α] [Countable α]
       exact h_indep.comp measurable_id (by fun_prop)
     · simp only [hm1, false_and, Set.setOf_false, Set.indicator_empty]
       exact condIndepFun_const_right (reward 0) 0
-  have h_indep : CondIndepFun (mα.comap (arm n)) (measurable_arm n).comap_le (reward n)
-      (hist (n - 1)) (Bandit.trajMeasure alg ν) := by
+  have h_indep : reward n ⟂ᵢ[arm n, measurable_arm n; 𝔓t] hist (n - 1) := by
     convert condIndepFun_reward_hist_arm (alg := alg) (ν := ν) (n - 1)
       <;> rw [Nat.sub_add_cancel (by grind)]
-  have h_indep' : CondIndepFun (mα.comap (arm n)) (measurable_arm n).comap_le (reward n)
-      (fun ω ↦ (hist (n - 1) ω, arm n ω)) (Bandit.trajMeasure alg ν) :=
+  have h_indep' : reward n ⟂ᵢ[arm n, measurable_arm n; 𝔓t] fun ω ↦ (hist (n - 1) ω, arm n ω) :=
     h_indep.prod_right (by fun_prop) (by fun_prop) (by fun_prop)
   obtain ⟨φ, hφ_meas, h_eq⟩ : ∃ φ : ((Iic (n - 1) → α × ℝ) × α) → ℕ, Measurable φ ∧
       {ω | stepsUntil a m ω = ↑n}.indicator (fun _ ↦ 1) = φ ∘ (fun ω ↦ (hist (n - 1) ω, arm n ω)) :=
@@ -231,44 +227,41 @@ lemma condIndepFun_reward_stepsUntil_arm' [StandardBorelSpace α] [Countable α]
 lemma condIndepFun_reward_stepsUntil_arm [StandardBorelSpace α] [Countable α] [Nonempty α]
     (a : α) (m n : ℕ) (hm : m ≠ 0) :
     CondIndepFun (mα.comap (fun ω ↦ arm n ω.1)) ((measurable_arm n).comp measurable_fst).comap_le
-      (fun ω ↦ reward n ω.1) ({ω | stepsUntil a m ω.1 = ↑n}.indicator (fun _ ↦ 1))
-      (Bandit.measure alg ν) :=
+      (fun ω ↦ reward n ω.1) ({ω | stepsUntil a m ω.1 = ↑n}.indicator (fun _ ↦ 1)) 𝔓 :=
   condIndepFun_fst_prod (ν := Bandit.streamMeasure ν)
     (measurable_indicator_stepsUntil_eq a m n) (by fun_prop) (by fun_prop)
     (condIndepFun_reward_stepsUntil_arm' a m n hm)
 
 lemma reward_cond_stepsUntil [StandardBorelSpace α] [Countable α] [Nonempty α] (a : α) (m n : ℕ)
-    (hm : m ≠ 0)
-    (hμn : (Bandit.measure alg ν) ((fun ω ↦ stepsUntil a m ω.1) ⁻¹' {↑n}) ≠ 0) :
-    𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ stepsUntil a m ω.1 ← ↑n; Bandit.measure alg ν] = ν a := by
-  let μ := Bandit.measure alg ν
+    (hm : m ≠ 0) (hμn : 𝔓 ((fun ω ↦ stepsUntil a m ω.1) ⁻¹' {↑n}) ≠ 0) :
+    𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ stepsUntil a m ω.1 ← ↑n; 𝔓] = ν a := by
   have hμna :
-      μ ((fun ω ↦ stepsUntil a m ω.1) ⁻¹' {↑n} ∩ (fun ω ↦ arm n ω.1) ⁻¹' {a}) ≠ 0 := by
+      𝔓 ((fun ω ↦ stepsUntil a m ω.1) ⁻¹' {↑n} ∩ (fun ω ↦ arm n ω.1) ⁻¹' {a}) ≠ 0 := by
     suffices ((fun ω : (ℕ → α × ℝ) × (ℕ → α → ℝ) ↦
           stepsUntil a m ω.1) ⁻¹' {↑n} ∩ (fun ω ↦ arm n ω.1) ⁻¹' {a})
         = (fun ω ↦ stepsUntil a m ω.1) ⁻¹' {↑n} by simpa [this] using hμn
     ext ω
     simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_singleton_iff, and_iff_left_iff_imp]
     exact arm_eq_of_stepsUntil_eq_coe hm
-  have hμa : μ.map (fun ω ↦ arm n ω.1) {a} ≠ 0 := by
+  have hμa : (𝔓).map (fun ω ↦ arm n ω.1) {a} ≠ 0 := by
     rw [Measure.map_apply (by fun_prop) (measurableSet_singleton _)]
     refine fun h_zero ↦ hμn (measure_mono_null (fun ω ↦ ?_) h_zero)
     simp only [Set.mem_preimage, Set.mem_singleton_iff]
     exact arm_eq_of_stepsUntil_eq_coe hm
-  calc 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ stepsUntil a m ω.1 ← (n : ℕ∞); μ]
-  _ = (μ[|(fun ω ↦ stepsUntil a m ω.1) ⁻¹' {↑n} ∩ (fun ω ↦ arm n ω.1) ⁻¹' {a}]).map
+  calc 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ stepsUntil a m ω.1 ← (n : ℕ∞); 𝔓]
+  _ = (𝔓[|(fun ω ↦ stepsUntil a m ω.1) ⁻¹' {↑n} ∩ (fun ω ↦ arm n ω.1) ⁻¹' {a}]).map
       (fun ω ↦ reward n ω.1) := by
     congr with ω
     simp only [Set.mem_preimage, Set.mem_singleton_iff, Set.mem_inter_iff, iff_self_and]
     exact arm_eq_of_stepsUntil_eq_coe hm
-  _ = (μ[|(fun ω ↦ arm n ω.1) ⁻¹' {a}
+  _ = (𝔓[|(fun ω ↦ arm n ω.1) ⁻¹' {a}
       ∩ {ω : (ℕ → α × ℝ) × (ℕ → α → ℝ) | stepsUntil a m ω.1 = ↑n}.indicator 1 ⁻¹' {1} ]).map
       (fun ω ↦ reward n ω.1) := by
     congr 2 with ω
     simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_singleton_iff, Set.indicator_apply,
       Set.mem_setOf_eq, Pi.one_apply, ite_eq_left_iff, zero_ne_one, imp_false, Decidable.not_not]
     rw [and_comm]
-  _ = 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1 ← a; μ] := by
+  _ = 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1 ← a; 𝔓] := by
     rw [cond_of_condIndepFun (by fun_prop)]
     · exact condIndepFun_reward_stepsUntil_arm a m n hm
     · refine measurable_one.indicator ?_
@@ -282,11 +275,9 @@ lemma reward_cond_stepsUntil [StandardBorelSpace α] [Countable α] [Nonempty α
 
 lemma condDistrib_rewardByCount_stepsUntil [Countable α] [StandardBorelSpace α] [Nonempty α]
     (a : α) (m : ℕ) (hm : m ≠ 0) :
-    condDistrib (rewardByCount a m) (fun ω ↦ stepsUntil a m ω.1)
-        (Bandit.measure alg ν)
-      =ᵐ[(Bandit.measure alg ν).map (fun ω ↦ stepsUntil a m ω.1)] Kernel.const _ (ν a) := by
-  let μ := Bandit.measure alg ν
-  refine (condDistrib_ae_eq_cond (μ := μ)
+    condDistrib (rewardByCount a m) (fun ω ↦ stepsUntil a m ω.1) 𝔓
+      =ᵐ[(𝔓).map (fun ω ↦ stepsUntil a m ω.1)] Kernel.const _ (ν a) := by
+  refine (condDistrib_ae_eq_cond (μ := 𝔓)
     (X := fun ω ↦ stepsUntil a m ω.1) (by fun_prop) (by fun_prop)).trans ?_
   rw [Filter.EventuallyEq, ae_iff_of_countable]
   intro n hn
@@ -315,51 +306,45 @@ lemma condDistrib_rewardByCount_stepsUntil [Countable α] [StandardBorelSpace α
 /-- The reward received at the `m`-th pull of arm `a` has law `ν a`. -/
 lemma hasLaw_rewardByCount [Countable α] [StandardBorelSpace α] [Nonempty α]
     (a : α) (m : ℕ) (hm : m ≠ 0) :
-    HasLaw (rewardByCount a m) (ν a) (Bandit.measure alg ν) where
+    HasLaw (rewardByCount a m) (ν a) 𝔓 where
   map_eq := by
     have h_condDistrib :
-        condDistrib (rewardByCount a m) (fun ω ↦ stepsUntil a m ω.1)
-          (Bandit.measure alg ν)
-        =ᵐ[(Bandit.measure alg ν).map (fun ω ↦ stepsUntil a m ω.1)]
+        condDistrib (rewardByCount a m) (fun ω ↦ stepsUntil a m ω.1) 𝔓
+        =ᵐ[(𝔓).map (fun ω ↦ stepsUntil a m ω.1)]
           Kernel.const _ (ν a) := condDistrib_rewardByCount_stepsUntil a m hm
-    calc (Bandit.measure alg ν).map (rewardByCount a m)
-    _ = (condDistrib (rewardByCount a m) (fun ω ↦ stepsUntil a m ω.1)
-          (Bandit.measure alg ν))
-        ∘ₘ ((Bandit.measure alg ν).map (fun ω ↦ stepsUntil a m ω.1)) := by
+    calc (𝔓).map (rewardByCount a m)
+    _ = (condDistrib (rewardByCount a m) (fun ω ↦ stepsUntil a m ω.1) 𝔓)
+        ∘ₘ ((𝔓).map (fun ω ↦ stepsUntil a m ω.1)) := by
       rw [condDistrib_comp_map (by fun_prop) (by fun_prop)]
-    _ = (Kernel.const _ (ν a))
-        ∘ₘ ((Bandit.measure alg ν).map (fun ω ↦ stepsUntil a m ω.1)) :=
+    _ = (Kernel.const _ (ν a)) ∘ₘ ((𝔓).map (fun ω ↦ stepsUntil a m ω.1)) :=
       Measure.comp_congr h_condDistrib
     _ = ν a := by
-      have : IsProbabilityMeasure
-          ((Bandit.measure alg ν).map (fun ω ↦ stepsUntil a m ω.1)) :=
+      have : IsProbabilityMeasure ((𝔓).map (fun ω ↦ stepsUntil a m ω.1)) :=
         Measure.isProbabilityMeasure_map (by fun_prop)
       simp
 
 lemma identDistrib_rewardByCount [Countable α] [StandardBorelSpace α] [Nonempty α] (a : α) (n m : ℕ)
     (hn : n ≠ 0) (hm : m ≠ 0) :
-    IdentDistrib (rewardByCount a n) (rewardByCount a m)
-      (Bandit.measure alg ν) (Bandit.measure alg ν) where
+    IdentDistrib (rewardByCount a n) (rewardByCount a m) 𝔓 𝔓 where
   aemeasurable_fst := by fun_prop
   aemeasurable_snd := by fun_prop
   map_eq := by rw [(hasLaw_rewardByCount a n hn).map_eq, (hasLaw_rewardByCount a m hm).map_eq]
 
 lemma identDistrib_rewardByCount_id [Countable α] [StandardBorelSpace α] [Nonempty α]
     (a : α) (n : ℕ) (hn : n ≠ 0) :
-    IdentDistrib (rewardByCount a n) id (Bandit.measure alg ν) (ν a) where
+    IdentDistrib (rewardByCount a n) id 𝔓 (ν a) where
   aemeasurable_fst := by fun_prop
   aemeasurable_snd := Measurable.aemeasurable <| by fun_prop
   map_eq := by rw [(hasLaw_rewardByCount a n hn).map_eq, Measure.map_id]
 
 lemma identDistrib_rewardByCount_eval [Countable α] [StandardBorelSpace α] [Nonempty α]
     (a : α) (n m : ℕ) (hn : n ≠ 0) :
-    IdentDistrib (rewardByCount a n) (fun ω ↦ ω m a)
-      (Bandit.measure alg ν) (Bandit.streamMeasure ν) :=
+    IdentDistrib (rewardByCount a n) (fun ω ↦ ω m a) 𝔓 (Bandit.streamMeasure ν) :=
   (identDistrib_rewardByCount_id a n hn).trans (identDistrib_eval_eval_id_streamMeasure ν m a).symm
 
 lemma indepFun_rewardByCount_Iic (alg : Algorithm α ℝ) (ν : Kernel α ℝ) [IsMarkovKernel ν] (a : α)
     (n : ℕ) :
-    (rewardByCount a (n + 1)) ⟂ᵢ[Bandit.measure alg ν] fun ω (i : Iic n) ↦ rewardByCount a i ω := by
+    (rewardByCount a (n + 1)) ⟂ᵢ[𝔓] fun ω (i : Iic n) ↦ rewardByCount a i ω := by
   sorry
 
 lemma iIndepFun_rewardByCount' (alg : Algorithm α ℝ) (ν : Kernel α ℝ) [IsMarkovKernel ν] (a : α) :
@@ -368,13 +353,13 @@ lemma iIndepFun_rewardByCount' (alg : Algorithm α ℝ) (ν : Kernel α ℝ) [Is
   exact indepFun_rewardByCount_Iic alg ν a
 
 lemma iIndepFun_rewardByCount (alg : Algorithm α ℝ) (ν : Kernel α ℝ) [IsMarkovKernel ν] :
-    iIndepFun (fun (p : α × ℕ) ↦ rewardByCount p.1 p.2) (Bandit.measure alg ν) := by
+    iIndepFun (fun (p : α × ℕ) ↦ rewardByCount p.1 p.2) 𝔓 := by
   sorry
 
 lemma identDistrib_rewardByCount_stream' [Countable α] [StandardBorelSpace α] [Nonempty α]
     (a : α) :
     IdentDistrib (fun ω n ↦ rewardByCount a (n + 1) ω) (fun ω n ↦ ω n a)
-      (Bandit.measure alg ν) (Bandit.streamMeasure ν) := by
+      𝔓 (Bandit.streamMeasure ν) := by
   refine IdentDistrib.pi (fun n ↦ ?_) ?_ ?_
   · refine identDistrib_rewardByCount_eval a (n + 1) n (by simp) (ν := ν)
   · have h_indep := iIndepFun_rewardByCount' alg ν a
@@ -384,35 +369,32 @@ lemma identDistrib_rewardByCount_stream' [Countable α] [StandardBorelSpace α]
 omit [DecidableEq α] [MeasurableSingletonClass α] in
 lemma identDistrib_eval_streamMeasure_measure (a : α) :
     IdentDistrib (fun ω n ↦ ω n a) (fun ω n ↦ ω.2 n a)
-      (Bandit.streamMeasure ν) (Bandit.measure alg ν) := by
+      (Bandit.streamMeasure ν) 𝔓 := by
   refine IdentDistrib.pi (fun n ↦ ?_) ?_ ?_
   · rw [← Bandit.snd_measure alg ν, Measure.snd,
       identDistrib_map_left_iff (by fun_prop) (by fun_prop)
         (Measurable.aemeasurable <| by fun_prop)]
     exact IdentDistrib.refl (by fun_prop)
   · exact iIndepFun_eval_streamMeasure'' ν a
-  · change iIndepFun (fun n ↦ ((fun ω ↦ ω n a) ∘ Prod.snd)) (Bandit.measure alg ν)
+  · change iIndepFun (fun n ↦ ((fun ω ↦ ω n a) ∘ Prod.snd)) 𝔓
     rw [← iIndepFun_map_iff (by fun_prop) (fun _ ↦ Measurable.aemeasurable (by fun_prop))]
     rw [← Measure.snd, Bandit.snd_measure]
     exact iIndepFun_eval_streamMeasure'' ν a
 
 lemma identDistrib_rewardByCount_stream [Countable α] [StandardBorelSpace α] [Nonempty α]
     (a : α) :
-    IdentDistrib (fun ω n ↦ rewardByCount a (n + 1) ω) (fun ω n ↦ ω.2 n a)
-      (Bandit.measure alg ν) (Bandit.measure alg ν) :=
+    IdentDistrib (fun ω n ↦ rewardByCount a (n + 1) ω) (fun ω n ↦ ω.2 n a) 𝔓 𝔓 :=
   (identDistrib_rewardByCount_stream' a).trans (identDistrib_eval_streamMeasure_measure a)
 
 lemma indepFun_rewardByCount_of_ne {a b : α} (hab : a ≠ b) :
-    IndepFun (fun ω s ↦ rewardByCount a s ω) (fun ω s ↦ rewardByCount b s ω)
-      (Bandit.measure alg ν) := by
+    IndepFun (fun ω s ↦ rewardByCount a s ω) (fun ω s ↦ rewardByCount b s ω) 𝔓 := by
   sorry
 
 lemma identDistrib_sum_Icc_rewardByCount [Nonempty α] [Countable α] (m : ℕ) (a : α) :
     IdentDistrib (fun ω ↦ ∑ s ∈ Icc 1 m, rewardByCount a s ω)
-      (fun ω ↦ ∑ s ∈ range m, ω.2 s a) (Bandit.measure alg ν) (Bandit.measure alg ν) := by
+      (fun ω ↦ ∑ s ∈ range m, ω.2 s a) 𝔓 𝔓 := by
   have h1 (a : α) :
-      IdentDistrib (fun ω s ↦ rewardByCount a (s + 1) ω) (fun ω s ↦ ω.2 s a)
-        (Bandit.measure alg ν) (Bandit.measure alg ν) :=
+      IdentDistrib (fun ω s ↦ rewardByCount a (s + 1) ω) (fun ω s ↦ ω.2 s a) 𝔓 𝔓 :=
     identDistrib_rewardByCount_stream a
   have h_eq (ω : (ℕ → α × ℝ) × (ℕ → α → ℝ)) : ∑ s ∈ Icc 1 m, rewardByCount a s ω
       = ∑ s ∈ range m, rewardByCount a (s + 1) ω := by
diff --git a/lake-manifest.json b/lake-manifest.json
index fd41da25..d01e8787 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a06e2b664ad658aa0e96140ac942641ee8f5cd66",
+   "rev": "725c803ee924f55342e93f2c75976051ab902b54",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e2a2ee109182182dd0e347e8149d312d72bfbfb2",
+   "rev": "b3dd6c3ebc0a71685e86bea9223be39ea4c299fb",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "78129e1913fe4988ac238156ec5f223ec02d286c",
+   "rev": "2e16f91af2a97975e5d2fac906494cd6c17ba255",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lakefile.toml b/lakefile.toml
index e00690bf..253e7156 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -1,5 +1,6 @@
 name = "LeanBandits"
 defaultTargets = ["LeanBandits"]
+lintDriver = "batteries/runLinter"
 
 [leanOptions]
 pp.unicode.fun = true