diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml
index b13d4b0a..727b79ff 100644
--- a/.github/workflows/blueprint.yml
+++ b/.github/workflows/blueprint.yml
@@ -48,8 +48,8 @@ jobs:
         uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0
         with:
           build: true
-          lint: false
-          mk_all-check: false
+          lint: true
+          mk_all-check: true
 
       - name: Build Verso Documentation
         run: |
diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean b/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean
index 4ec80488..3f216d3e 100644
--- a/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean
+++ b/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean
@@ -513,7 +513,7 @@ lemma expectation_pullCount_le' [Nonempty (Fin K)]
     simp only [id_eq, Nat.cast_sum]
     rw [lintegral_add_left (by fun_prop), lintegral_add_left (by fun_prop)]
     simp only [lintegral_const, measure_univ, mul_one]
-    rw [lintegral_finset_sum _ (by fun_prop), lintegral_finset_sum _ (by fun_prop)]
+    rw [lintegral_finsetSum _ (by fun_prop), lintegral_finsetSum _ (by fun_prop)]
     gcongr with k hk k hk
     · rw [← lintegral_indicator_one]
       swap; · exact h_set_2 _
diff --git a/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean b/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean
index 466eb7f4..817e8bf6 100644
--- a/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean
+++ b/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean
@@ -628,7 +628,7 @@ lemma indepFun_fst_add_one_aux (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (n : ℕ
     simp only [X, Y, Set.preimage_inter, Set.preimage_preimage]
     by_cases h : ω₁ (n + 1) ∈ s
     · simp [h]
-      grind
+      congr
     · simp [h]
   simp_rw [hY_fst, hX_fst, hXY]
   -- Factor the integral using independence
@@ -1191,8 +1191,8 @@ lemma hasCondDistrib_reward' (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMa
     let e : ((𝓐 × ℕ) × (Iic n → 𝓐 × R)) ≃ᵐ ((𝓐 × (Iic n → 𝓐 × R)) × ℕ) :=
     { toFun := fun x ↦ ((x.1.1, x.2), x.1.2)
       invFun := fun x ↦ ((x.1.1, x.2), x.1.2)
-      measurable_toFun := by fun_prop
-      measurable_invFun := by fun_prop }
+      measurable_toFun := by simp only [Equiv.coe_fn_mk]; fun_prop
+      measurable_invFun := by simp only [Equiv.symm_mk, Equiv.coe_fn_mk]; fun_prop }
     exact this.comp_right e
   suffices HasCondDistrib R' (fun ω ↦ (A ω, P ω)) (ν.prodMkRight _) (arrayMeasure ν) by
     have h_indep : H ⟂ᵢ[(fun ω ↦ (A ω, P ω)), (by fun_prop); arrayMeasure ν] R' :=
diff --git a/LeanMachineLearning/Online/Bandit/Regret.lean b/LeanMachineLearning/Online/Bandit/Regret.lean
index 4f3c20bb..86f03527 100644
--- a/LeanMachineLearning/Online/Bandit/Regret.lean
+++ b/LeanMachineLearning/Online/Bandit/Regret.lean
@@ -75,7 +75,7 @@ lemma integral_regret_eq_sum_gap_mul_integral_pullCount
     (hA : ∀ n, Measurable (A n)) :
     P[regret ν A n] = ∑ a, gap ν a * P[fun ω ↦ (pullCount A a n ω : ℝ)] := by
   simp_rw [regret_eq_sum_pullCount_mul_gap]
-  rw [integral_finset_sum]
+  rw [integral_finsetSum]
   swap; · exact fun i _ ↦ (integrable_pullCount hA i n).mul_const _
   congr with a
   rw [integral_mul_const, mul_comm]
diff --git a/LeanMachineLearning/Online/Bandit/SumRewards.lean b/LeanMachineLearning/Online/Bandit/SumRewards.lean
index 140d762c..5fbec0ee 100644
--- a/LeanMachineLearning/Online/Bandit/SumRewards.lean
+++ b/LeanMachineLearning/Online/Bandit/SumRewards.lean
@@ -75,7 +75,8 @@ lemma prob_pullCount_mem_and_sumRewards_mem_le (a : 𝓐) (n : ℕ)
   classical
   rcases Set.eq_empty_or_nonempty B with h_empty | h_nonempty
   · simp [h_empty]
-  convert prob_pullCount_prod_sumRewards_mem_le a n (hs.prod hB) (ν := ν) (alg := alg) with _ _ k hk
+  convert prob_pullCount_prod_sumRewards_mem_le a n (hs.prod hB) (ν := ν) (alg := alg)
+    with _ _ _ k hk
   · ext n
     have : ∃ x, x ∈ B := h_nonempty
     simp [this]
@@ -274,7 +275,7 @@ lemma prob_pullCount_mem_and_sumRewards_mem_le [Countable 𝓐]
   classical
   rcases Set.eq_empty_or_nonempty B with h_empty | h_nonempty
   · simp [h_empty]
-  convert prob_pullCount_prod_sumRewards_mem_le h (hs.prod hB) (ν := ν) (alg := alg) with _ _ k hk
+  convert prob_pullCount_prod_sumRewards_mem_le h (hs.prod hB) (ν := ν) (alg := alg) with _ _ _ k hk
   · ext n
     have : ∃ x, x ∈ B := h_nonempty
     simp [this]
diff --git a/LeanMachineLearning/Probability/Independence/CondDistrib.lean b/LeanMachineLearning/Probability/Independence/CondDistrib.lean
index 98b6f974..78696b15 100644
--- a/LeanMachineLearning/Probability/Independence/CondDistrib.lean
+++ b/LeanMachineLearning/Probability/Independence/CondDistrib.lean
@@ -10,6 +10,11 @@ public import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
 public import Mathlib.Probability.Independence.Basic
 public import Mathlib.Probability.Independence.Conditional
 
+/-!
+# Lemmas about conditional distributions
+
+-/
+
 @[expose] public section
 
 open MeasureTheory ProbabilityTheory Finset
@@ -472,7 +477,7 @@ lemma condDistrib_prod_of_forall_condDistrib_cond [Countable Ω'] [IsFiniteMeasu
         · simp only [hZ, Set.setOf_true, Set.mem_setOf_eq, Set.indicator_of_mem]
           exact κ.measure_le_bound _ _
         · simp [hZ]
-      refine le_antisymm (h_le.trans ?_) (zero_le _)
+      refine le_antisymm (h_le.trans ?_) zero_le
       rw [lintegral_indicator]
       swap; · exact (measurableSet_singleton _).preimage (by fun_prop)
       simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter,
diff --git a/LeanMachineLearning/Probability/Independence/CondIndepFun.lean b/LeanMachineLearning/Probability/Independence/CondIndepFun.lean
index fd6941de..420483c0 100644
--- a/LeanMachineLearning/Probability/Independence/CondIndepFun.lean
+++ b/LeanMachineLearning/Probability/Independence/CondIndepFun.lean
@@ -9,11 +9,11 @@ public import Mathlib.MeasureTheory.Function.FactorsThrough
 public import Mathlib.Probability.Independence.Basic
 public import Mathlib.Probability.Independence.Conditional
 
-@[expose] public section
-
 /-! # Laws of `stepsUntil` and `rewardByCount`
 -/
 
+@[expose] public section
+
 open MeasureTheory ProbabilityTheory Finset
 open scoped ENNReal NNReal
 
diff --git a/LeanMachineLearning/Probability/Independence/IndepFun.lean b/LeanMachineLearning/Probability/Independence/IndepFun.lean
index 82aa1a14..80df7dff 100644
--- a/LeanMachineLearning/Probability/Independence/IndepFun.lean
+++ b/LeanMachineLearning/Probability/Independence/IndepFun.lean
@@ -8,6 +8,9 @@ module
 public import Mathlib.Probability.IdentDistrib
 public import Mathlib.Probability.Independence.InfinitePi
 
+/-! # Lemmas about independence
+-/
+
 @[expose] public section
 
 open MeasureTheory Finset
diff --git a/LeanMachineLearning/Probability/Independence/IndepInfinitePi.lean b/LeanMachineLearning/Probability/Independence/IndepInfinitePi.lean
index fae48915..78ffa84a 100644
--- a/LeanMachineLearning/Probability/Independence/IndepInfinitePi.lean
+++ b/LeanMachineLearning/Probability/Independence/IndepInfinitePi.lean
@@ -7,6 +7,9 @@ module
 
 public import Mathlib.Probability.Independence.InfinitePi
 
+/-! # Lemmas about independence and infinite products
+-/
+
 @[expose] public section
 
 open MeasureTheory Measure ProbabilityTheory Set Function
diff --git a/LeanMachineLearning/Probability/Integrable.lean b/LeanMachineLearning/Probability/Integrable.lean
index 1e77f126..d899b999 100644
--- a/LeanMachineLearning/Probability/Integrable.lean
+++ b/LeanMachineLearning/Probability/Integrable.lean
@@ -7,6 +7,9 @@ module
 
 public import Mathlib.Probability.IdentDistrib
 
+/-! # Lemmas about integrable functions
+-/
+
 @[expose] public section
 
 open ProbabilityTheory
diff --git a/LeanMachineLearning/Probability/Kernel/Basic.lean b/LeanMachineLearning/Probability/Kernel/Basic.lean
index 723691fc..a8e69939 100644
--- a/LeanMachineLearning/Probability/Kernel/Basic.lean
+++ b/LeanMachineLearning/Probability/Kernel/Basic.lean
@@ -7,6 +7,9 @@ module
 
 public import Mathlib.Probability.Kernel.Basic
 
+/-! # Basic lemmas about Markov kernels
+-/
+
 @[expose] public section
 
 open MeasureTheory
diff --git a/LeanMachineLearning/Probability/Kernel/Composition/MapComap.lean b/LeanMachineLearning/Probability/Kernel/Composition/MapComap.lean
index 093e04dc..2a1b2efc 100644
--- a/LeanMachineLearning/Probability/Kernel/Composition/MapComap.lean
+++ b/LeanMachineLearning/Probability/Kernel/Composition/MapComap.lean
@@ -7,6 +7,9 @@ module
 
 public import Mathlib.Probability.Kernel.Composition.MapComap
 
+/-! # Lemmas about map and comap of Markov kernels
+-/
+
 @[expose] public section
 
 namespace ProbabilityTheory.Kernel
diff --git a/LeanMachineLearning/Probability/Kernel/Composition/MeasureCompProd.lean b/LeanMachineLearning/Probability/Kernel/Composition/MeasureCompProd.lean
index 7caf1a15..e2f2aec7 100644
--- a/LeanMachineLearning/Probability/Kernel/Composition/MeasureCompProd.lean
+++ b/LeanMachineLearning/Probability/Kernel/Composition/MeasureCompProd.lean
@@ -7,6 +7,9 @@ module
 
 public import Mathlib.Probability.Kernel.Composition.MeasureCompProd
 
+/-! # Lemmas about measure composition-product
+-/
+
 @[expose] public section
 
 open ProbabilityTheory
diff --git a/LeanMachineLearning/Probability/Kernel/IonescuTulcea/Traj.lean b/LeanMachineLearning/Probability/Kernel/IonescuTulcea/Traj.lean
index c2b1e190..098fb002 100644
--- a/LeanMachineLearning/Probability/Kernel/IonescuTulcea/Traj.lean
+++ b/LeanMachineLearning/Probability/Kernel/IonescuTulcea/Traj.lean
@@ -9,6 +9,9 @@ public import LeanMachineLearning.Probability.HasCondDistrib
 public import Mathlib.Probability.Kernel.IonescuTulcea.Traj
 public import Mathlib.Probability.Process.FiniteDimensionalLaws
 
+/-! # Lemmas about `traj` and `trajMeasure`
+-/
+
 @[expose] public section
 
 open Filter Finset Function MeasurableEquiv MeasurableSpace MeasureTheory Preorder ProbabilityTheory
diff --git a/LeanMachineLearning/Probability/Kernel/KernelSub.lean b/LeanMachineLearning/Probability/Kernel/KernelSub.lean
index 244af920..785aab28 100644
--- a/LeanMachineLearning/Probability/Kernel/KernelSub.lean
+++ b/LeanMachineLearning/Probability/Kernel/KernelSub.lean
@@ -9,7 +9,7 @@ public import Mathlib.MeasureTheory.Measure.SubFinite
 public import Mathlib.Probability.Kernel.RadonNikodym
 
 /-!
-# Kernels substraction
+# Kernel substraction
 
 -/
 
diff --git a/LeanMachineLearning/Probability/Moments/SubGaussian.lean b/LeanMachineLearning/Probability/Moments/SubGaussian.lean
index 68965f0e..c4d63dbc 100644
--- a/LeanMachineLearning/Probability/Moments/SubGaussian.lean
+++ b/LeanMachineLearning/Probability/Moments/SubGaussian.lean
@@ -7,6 +7,9 @@ module
 
 public import Mathlib.Probability.Moments.SubGaussian
 
+/-! # Lemmas about sub-Gaussian random variables
+-/
+
 @[expose] public section
 
 open MeasureTheory Real
@@ -114,18 +117,18 @@ lemma measure_sum_le_sum_le [IsFiniteMeasure μ]
     (cX := ∑ i ∈ s, cX i) (cY := ∑ j ∈ t, cY j) ?_ ?_ h_indep_sum ?_).trans_eq ?_
   · suffices HasSubgaussianMGF (fun ω ↦ ∑ i ∈ s, (X i ω - μ[X i])) (∑ i ∈ s, cX i) μ by
       convert this
-      rw [integral_finset_sum _ hX_int, Finset.sum_sub_distrib]
+      rw [integral_finsetSum _ hX_int, Finset.sum_sub_distrib]
     refine sum_of_iIndepFun ?_ hX_subG
     exact hX_indep.comp (g := fun i x ↦ x - μ[X i]) (by fun_prop)
   · suffices HasSubgaussianMGF (fun ω ↦ ∑ j ∈ t, (Y j ω - μ[Y j])) (∑ j ∈ t, cY j) μ by
       convert this
-      rw [integral_finset_sum _ hY_int, Finset.sum_sub_distrib]
+      rw [integral_finsetSum _ hY_int, Finset.sum_sub_distrib]
     refine sum_of_iIndepFun ?_ hY_subG
     exact hY_indep.comp (g := fun i x ↦ x - μ[Y i]) (by fun_prop)
-  · rwa [integral_finset_sum _ hX_int, integral_finset_sum _ hY_int]
+  · rwa [integral_finsetSum _ hX_int, integral_finsetSum _ hY_int]
   · congr
-    · rw [integral_finset_sum _ hY_int]
-    · rw [integral_finset_sum _ hX_int]
+    · rw [integral_finsetSum _ hY_int]
+    · rw [integral_finsetSum _ hX_int]
 
 lemma measure_sum_le_sum_le' [IsFiniteMeasure μ]
     (hX_indep : iIndepFun X μ) (hY_indep : iIndepFun Y μ)
diff --git a/LeanMachineLearning/Probability/WithDensity.lean b/LeanMachineLearning/Probability/WithDensity.lean
index bc378c8f..8471c6ff 100644
--- a/LeanMachineLearning/Probability/WithDensity.lean
+++ b/LeanMachineLearning/Probability/WithDensity.lean
@@ -8,6 +8,9 @@ module
 public import Mathlib.Probability.Kernel.CompProdEqIff
 public import Mathlib.Probability.Kernel.Composition.MeasureComp
 
+/-! # Lemmas about kernels and measures with density
+-/
+
 @[expose] public section
 
 open MeasureTheory ProbabilityTheory
diff --git a/LeanMachineLearning/SequentialLearning/Algorithm.lean b/LeanMachineLearning/SequentialLearning/Algorithm.lean
index f2d67863..9f5748d8 100644
--- a/LeanMachineLearning/SequentialLearning/Algorithm.lean
+++ b/LeanMachineLearning/SequentialLearning/Algorithm.lean
@@ -59,7 +59,7 @@ instance (alg : Algorithm 𝓐 𝓨) : IsProbabilityMeasure alg.p0 := alg.hp0
 
 /-- An algorithm with observations in `𝓧 × 𝓨` obtained from an algorithm with observations in `𝓨`
 by ignoring the `𝓧` component of each observation. -/
-def Algorithm.prod_left (𝓧 : Type*) [MeasurableSpace 𝓧] (alg : Algorithm 𝓐 𝓨) :
+def Algorithm.prodLeft (𝓧 : Type*) [MeasurableSpace 𝓧] (alg : Algorithm 𝓐 𝓨) :
     Algorithm 𝓐 (𝓧 × 𝓨) where
   policy n := (alg.policy n).comap (fun h i ↦ ((h i).1, (h i).2.2)) (by fun_prop)
   p0 := alg.p0
diff --git a/LeanMachineLearning/SequentialLearning/FiniteActions.lean b/LeanMachineLearning/SequentialLearning/FiniteActions.lean
index 9b9690a1..d11dfab4 100644
--- a/LeanMachineLearning/SequentialLearning/FiniteActions.lean
+++ b/LeanMachineLearning/SequentialLearning/FiniteActions.lean
@@ -233,11 +233,16 @@ lemma adapted_pullCount_add_one [MeasurableSingletonClass 𝓐]
   rw [← measurable_iff_comap_le]
   exact measurable_comp_comap _ (measurable_pullCount' n a)
 
+lemma stronglyAdapted_pullCount_add_one [MeasurableSingletonClass 𝓐]
+    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : 𝓐) :
+    StronglyAdapted (IsAlgEnvSeq.filtration hA hR') (fun n ↦ pullCount A a (n + 1)) :=
+  (adapted_pullCount_add_one hA hR' a).stronglyAdapted
+
 lemma isPredictable_pullCount [MeasurableSingletonClass 𝓐]
     (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : 𝓐) :
-    IsPredictable (IsAlgEnvSeq.filtration hA hR') (pullCount A a) := by
-  rw [isPredictable_iff_measurable_add_one]
-  refine ⟨?_, adapted_pullCount_add_one hA hR' a⟩
+    IsStronglyPredictable (IsAlgEnvSeq.filtration hA hR') (pullCount A a) := by
+  rw [IsStronglyPredictable.iff_measurable_add_one]
+  refine ⟨?_, stronglyAdapted_pullCount_add_one hA hR' a⟩
   simp only [pullCount_zero]
   fun_prop
 
@@ -385,7 +390,7 @@ lemma action_stepsUntil (hm : m ≠ 0) (h_exists : ∃ s, pullCount A a (s + 1)
   have h_spec := Nat.find_spec h_exists
   have h_spec' n := Nat.find_min h_exists (m := n)
   by_cases h_zero : Nat.find h_exists = 0
-  · simp only [h_zero, zero_add, not_lt_zero', IsEmpty.forall_iff, implies_true] at *
+  · simp only [h_zero, zero_add, not_lt_zero, IsEmpty.forall_iff, implies_true] at *
     by_contra h_ne
     rw [← zero_add 1, pullCount_eq_pullCount_of_action_ne h_ne] at h_spec
     simp only [pullCount_zero] at h_spec
@@ -592,7 +597,8 @@ lemma measurable_comap_indicator_stepsUntil_eq [MeasurableSingletonClass 𝓐]
     · simp only [hn, pullCount_zero]
       exact measurable_const
     have h_meas := adapted_pullCount_add_one hA hR' a (n - 1)
-    grind
+    have : 1 ≤ n := by grind
+    simpa [Nat.sub_add_cancel this] using h_meas
 
 lemma measurable_indicator_stepsUntil_eq [MeasurableSingletonClass 𝓐]
     (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : 𝓐) (m n : ℕ) :
@@ -938,13 +944,14 @@ lemma measurable_uncurry_empMean' [MeasurableEq 𝓐] (n : ℕ) :
 lemma IsAlgEnvSeq.isPredictable_sumRewards [StandardBorelSpace 𝓐] [Nonempty 𝓐] {R' : ℕ → Ω → ℝ}
     {alg : Algorithm 𝓐 ℝ} {env : Environment 𝓐 ℝ}
     (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
-    IsPredictable (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
+    IsStronglyPredictable (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
       (sumRewards A R' a) := by
-  rw [isPredictable_iff_measurable_add_one]
+  rw [IsStronglyPredictable.iff_measurable_add_one]
   constructor
   · simp only [sumRewards_zero]
     fun_prop
-  refine fun n ↦ measurable_fun_sum _ fun i hi ↦ Measurable.ite ?_ ?_ (by fun_prop)
+  refine fun n ↦ Measurable.stronglyMeasurable ?_
+  refine measurable_fun_sum _ fun i hi ↦ Measurable.ite ?_ ?_ (by fun_prop)
   · refine (measurableSet_singleton a).preimage ?_
     have h_meas_i := IsAlgEnvSeq.adapted_action h.measurable_action h.measurable_feedback i
     simp only [mem_range] at hi
@@ -955,15 +962,22 @@ lemma IsAlgEnvSeq.isPredictable_sumRewards [StandardBorelSpace 𝓐] [Nonempty 
     exact h_meas_i.mono ((IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback).mono
       (by lia)) le_rfl
 
-lemma IsAlgEnvSeq.adapted_sumRewards_add_one [StandardBorelSpace 𝓐] [Nonempty 𝓐] {R' : ℕ → Ω → ℝ}
-    {alg : Algorithm 𝓐 ℝ} {env : Environment 𝓐 ℝ}
+lemma IsAlgEnvSeq.stronglyAdapted_sumRewards_add_one [StandardBorelSpace 𝓐] [Nonempty 𝓐]
+    {R' : ℕ → Ω → ℝ} {alg : Algorithm 𝓐 ℝ} {env : Environment 𝓐 ℝ}
     (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
-    Adapted (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
+    StronglyAdapted (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
       (fun n ↦ sumRewards A R' a (n + 1)) := by
   have h_predictable := h.isPredictable_sumRewards a
-  rw [isPredictable_iff_measurable_add_one] at h_predictable
+  rw [IsStronglyPredictable.iff_measurable_add_one] at h_predictable
   exact h_predictable.2
 
+lemma IsAlgEnvSeq.adapted_sumRewards_add_one [StandardBorelSpace 𝓐] [Nonempty 𝓐] {R' : ℕ → Ω → ℝ}
+    {alg : Algorithm 𝓐 ℝ} {env : Environment 𝓐 ℝ}
+    (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
+    Adapted (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
+      (fun n ↦ sumRewards A R' a (n + 1)) :=
+  (h.stronglyAdapted_sumRewards_add_one a).adapted
+
 section CopiedFromPR
 
 open Set
@@ -990,7 +1004,7 @@ end CopiedFromPR
 lemma IsAlgEnvSeq.isPredictable_empMean [StandardBorelSpace 𝓐] [Nonempty 𝓐] {R' : ℕ → Ω → ℝ}
     {alg : Algorithm 𝓐 ℝ} {env : Environment 𝓐 ℝ}
     (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
-    IsPredictable (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
+    IsStronglyPredictable (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
       (empMean A R' a) := by
   unfold empMean
   refine StronglyMeasurable.div₀' ?_ ?_
@@ -998,15 +1012,22 @@ lemma IsAlgEnvSeq.isPredictable_empMean [StandardBorelSpace 𝓐] [Nonempty 𝓐
   · have h_meas := (isPredictable_pullCount h.measurable_action h.measurable_feedback a).measurable
     fun_prop
 
-lemma IsAlgEnvSeq.adapted_empMean_add_one [StandardBorelSpace 𝓐] [Nonempty 𝓐] {R' : ℕ → Ω → ℝ}
-    {alg : Algorithm 𝓐 ℝ} {env : Environment 𝓐 ℝ}
+lemma IsAlgEnvSeq.stronglyAdapted_empMean_add_one [StandardBorelSpace 𝓐] [Nonempty 𝓐]
+    {R' : ℕ → Ω → ℝ} {alg : Algorithm 𝓐 ℝ} {env : Environment 𝓐 ℝ}
     (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
-    Adapted (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
+    StronglyAdapted (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
       (fun n ↦ empMean A R' a (n + 1)) := by
   have h_predictable := h.isPredictable_empMean a
-  rw [isPredictable_iff_measurable_add_one] at h_predictable
+  rw [IsStronglyPredictable.iff_measurable_add_one] at h_predictable
   exact h_predictable.2
 
+lemma IsAlgEnvSeq.adapted_empMean_add_one [StandardBorelSpace 𝓐] [Nonempty 𝓐] {R' : ℕ → Ω → ℝ}
+    {alg : Algorithm 𝓐 ℝ} {env : Environment 𝓐 ℝ}
+    (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
+    Adapted (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
+      (fun n ↦ empMean A R' a (n + 1)) :=
+  (h.stronglyAdapted_empMean_add_one a).adapted
+
 end SumRewards
 
 end Learning
diff --git a/LeanMachineLearning/Tutorial/BasicProbability.lean b/LeanMachineLearning/Tutorial/BasicProbability.lean
index ea63ce24..cf08ae41 100644
--- a/LeanMachineLearning/Tutorial/BasicProbability.lean
+++ b/LeanMachineLearning/Tutorial/BasicProbability.lean
@@ -9,6 +9,9 @@ public import Mathlib.Probability.Distributions.Gaussian.Real
 public import Mathlib.Probability.Independence.Basic
 public import Mathlib.Probability.Moments.Basic
 
+/-! # Tutorial source file for basic probability
+-/
+
 @[expose] public section
 
 open MeasureTheory ProbabilityTheory
diff --git a/LeanMachineLearning/Tutorial/MarkovKernel.lean b/LeanMachineLearning/Tutorial/MarkovKernel.lean
index ad142b25..99161719 100644
--- a/LeanMachineLearning/Tutorial/MarkovKernel.lean
+++ b/LeanMachineLearning/Tutorial/MarkovKernel.lean
@@ -8,6 +8,9 @@ module
 public import Mathlib.Probability.Kernel.Composition.Lemmas
 public import Mathlib.Tactic.Recall
 
+/-! # Tutorial source file for Markov kernels
+-/
+
 @[expose] public section
 
 open MeasureTheory ProbabilityTheory
diff --git a/LeanMachineLearning/Tutorial/Martingales.lean b/LeanMachineLearning/Tutorial/Martingales.lean
index 2808aafa..dd4d4883 100644
--- a/LeanMachineLearning/Tutorial/Martingales.lean
+++ b/LeanMachineLearning/Tutorial/Martingales.lean
@@ -9,6 +9,8 @@ public import Mathlib.Probability.Martingale.Convergence
 public import Mathlib.Probability.Martingale.OptionalStopping
 public import Mathlib.Probability.Martingale.OptionalSampling
 
+/-! # Tutorial source file for martingales -/
+
 @[expose] public section
 
 open Filter
diff --git a/lake-manifest.json b/lake-manifest.json
index d9d0a85c..568c5ae9 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,11 +1,11 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover/subverso",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "52b9dfbd2658408e37ae6e8b72601ddeaaa25a0c",
+   "rev": "a86770a5eba721c8554d1d7fce741bc4dde3bb61",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -25,17 +25,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8a178386ffc0f5fef0b77738bb5449d50efeea95",
+   "rev": "c5ea00351c28e24afc9f0f84379aa41082b1188f",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.29.0",
+   "inputRev": "v4.30.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3",
+   "rev": "a456461b368b71d2accd95234832cd9c174b5437",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "48d5698bc464786347c1b0d859b18f938420f060",
+   "rev": "515cf9d0c00ece5e661f6de4326a53dedc1e8ea1",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,37 +65,37 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3c52dee17f0cd89c1ec14de78920d1bdaa3d26b3",
+   "rev": "a84b3e2475d5c5ab979567b1ad8aea21b764bcf8",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.95",
+   "inputRev": "v0.0.99",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7152850e7b216a0d409701617721b6e469d34bf6",
+   "rev": "558915ae105bfd8074e22d597613d1961822adc2",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.30.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "707efb56d0696634e9e965523a1bbe9ac6ce141d",
+   "rev": "a6e6c34c4ef182f83b219a3a5a385f51f44bdc4c",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.30.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "756e3321fd3b02a85ffda19fef789916223e578c",
+   "rev": "32dc18cde3684679f3c003de608743b57498c56f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,11 +105,12 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "7802da01beb530bf051ab657443f9cd9bc3e1a29",
+   "rev": "6b907cf12b2e445ccb7c24bc208ef04a1f39e84c",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.29.0",
+   "inputRev": "v4.30.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "LeanMachineLearning",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/lakefile.toml b/lakefile.toml
index 494f0aa9..82662275 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -6,14 +6,13 @@ lintDriver = "batteries/runLinter"
 pp.unicode.fun = true
 autoImplicit = false
 relaxedAutoImplicit = false
-weak.linter.flexible = true # no rigid tactic (e.g. `exact`) after a flexible tactic (e.g. `simp`)
 # Enable all mathlib linters: automatically matches what mathlib uses.
 weak.linter.mathlibStandardSet = true
 
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.29.0"
+rev = "v4.30.0"
 
 [[require]]
 name = "checkdecls"
diff --git a/lean-toolchain b/lean-toolchain
index 14791d72..af9e5d33 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.29.0
+leanprover/lean4:v4.30.0
diff --git a/scripts/nolints.json b/scripts/nolints.json
index fe51488c..a29c0e2e 100644
--- a/scripts/nolints.json
+++ b/scripts/nolints.json
@@ -1 +1,3 @@
-[]
+[["defsWithUnderscore", "ProbabilityTheory.instPartialOrderFiniteMeasure_leanMachineLearning"],
+["defsWithUnderscore", "ProbabilityTheory.instSubFiniteMeasure_leanMachineLearning"],
+["defsWithUnderscore", "ProbabilityTheory.Kernel.instSubOfDecidableIsSFiniteKernel_leanMachineLearning"]]
diff --git a/tutorial/lake-manifest.json b/tutorial/lake-manifest.json
index fb0e940c..b9bfd020 100644
--- a/tutorial/lake-manifest.json
+++ b/tutorial/lake-manifest.json
@@ -1,21 +1,31 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover/verso",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "286953ec42c78625798b734ded39e924468bfd41",
+   "rev": "14e7bf2c43076234c4f728d94f8b098dbb36e3cd",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
-   "inputRev": null,
+   "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/illuminate",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "c7a8de81e102ee2a42a7395f98d1ed12a861a43b",
+   "name": "illuminate",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3",
+   "rev": "744117af710b1c0400cd297c9ce91f8d0ad3a347",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,11 +45,12 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "52b9dfbd2658408e37ae6e8b72601ddeaaa25a0c",
+   "rev": "a86770a5eba721c8554d1d7fce741bc4dde3bb61",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"}],
  "name": "manual",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/tutorial/lakefile.toml b/tutorial/lakefile.toml
index 9e58485d..49a2fa3a 100644
--- a/tutorial/lakefile.toml
+++ b/tutorial/lakefile.toml
@@ -8,6 +8,7 @@ autoImplicit = true
 [[require]]
 name = "verso"
 git = "https://github.com/leanprover/verso"
+rev = "main"
 
 [[lean_lib]]
 name = "Manual"
diff --git a/tutorial/lean-toolchain b/tutorial/lean-toolchain
index 14791d72..6af09a89 100644
--- a/tutorial/lean-toolchain
+++ b/tutorial/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.29.0
+leanprover/lean4:v4.31.0-rc2
\ No newline at end of file