diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean
index 3dbb4310..0aa85f51 100644
--- a/LeanMachineLearning.lean
+++ b/LeanMachineLearning.lean
@@ -1,4 +1,4 @@
-module  -- shake: keep-all
+module  -- shake: keep-all --deprecated_module: ignore
 
 public import LeanMachineLearning.MeasureTheory.Constructions.BorelSpace.MeasurableArgMax
 public import LeanMachineLearning.MeasureTheory.Constructions.Polish.StandardBorel
diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean b/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean
index 054ff2d1..b9d4c829 100644
--- a/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean
+++ b/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean
@@ -82,7 +82,7 @@ section AlgorithmBehavior
 lemma arm_zero [Nonempty (Fin K)]
     (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P) :
     A 0 =ᵐ[P] fun _ ↦ ⟨0, hK⟩ :=
-  RoundRobin.action_zero ((isAlgEnvSeqUntil_roundRobinAlgorithm h).mono zero_le')
+  RoundRobin.action_zero ((isAlgEnvSeqUntil_roundRobinAlgorithm h).mono zero_le)
 
 lemma arm_ae_eq_etcNextArm [Nonempty (Fin K)]
     (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P) (n : ℕ) :
diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean b/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean
index 3f216d3e..8d4985c0 100644
--- a/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean
+++ b/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean
@@ -102,7 +102,7 @@ lemma ucbWidth_eq_ucbWidth' (c : ℝ) (a : Fin K) (n : ℕ) (ω : Ω) (hn : n 
 lemma arm_zero [Nonempty (Fin K)]
     (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) :
     A 0 =ᵐ[P] fun _ ↦ ⟨0, hK⟩ :=
-  RoundRobin.action_zero ((isAlgEnvSeqUntil_roundRobinAlgorithm h).mono zero_le')
+  RoundRobin.action_zero ((isAlgEnvSeqUntil_roundRobinAlgorithm h).mono zero_le)
 
 lemma arm_ae_eq_ucbNextArm [Nonempty (Fin K)]
     (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) (n : ℕ) :
@@ -415,7 +415,7 @@ lemma some_sum_eq_zero [Nonempty (Fin K)]
     grind
   · rwa [h_arm]
   · rw [h_arm]
-    exact zero_le'.trans_lt hC_lt
+    exact zero_le.trans_lt hC_lt
   refine lt_irrefl (8 * c * σ2 * log (n + 1) / gap ν a ^ 2) ?_
   refine hC'.trans_lt (lt_of_lt_of_le ?_ (h.trans ?_))
   · rw [h_arm]
diff --git a/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean b/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean
index 817e8bf6..b8467ae4 100644
--- a/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean
+++ b/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean
@@ -608,6 +608,8 @@ lemma indepFun_fst_add_one_aux (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (n : ℕ
     have h := h_indep.indepFun_finset₀ {n + 1} (Iic n) (by simp)
       (fun i ↦ (measurable_pi_apply i).aemeasurable)
     convert h.comp (measurable_pi_apply ⟨n + 1, by simp⟩) measurable_id using 1
+    · rfl
+    · rfl
   rw [indepFun_iff_measure_inter_preimage_eq_mul]
   intro s t hs ht
   let X : (ℕ → I) × (ℕ → 𝓐 → R) → I := fun ω ↦ ω.1 (n + 1)
@@ -910,6 +912,9 @@ lemma indepFun_snd_hist_cond [Countable 𝓐] (alg : Algorithm 𝓐 R)
       fun ω ↦ (ω.1, fun k b ↦ if b = a then if m ≠ 0 then ω.2 (min k (m - 1)) b
         else Nonempty.some inferInstance else ω.2 k b) by
     convert this using 1
+    · rfl
+    · rfl
+    · rfl
     congr with ω
     simp only [Set.mem_preimage, Set.mem_singleton_iff, Prod.mk.injEq, Set.indicator_apply,
       Set.mem_setOf_eq, ite_eq_left_iff, not_and, zero_ne_one, imp_false,
@@ -1230,6 +1235,7 @@ lemma hasCondDistrib_reward (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMar
     rw [hist_eq _ _ n]
   · simp only [reward]
     rw [hist_eq _ _ n]
+  · rfl
 
 lemma isAlgEnvSeq_arrayMeasure (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMarkovKernel ν] :
     IsAlgEnvSeq (action alg) (reward alg) alg (stationaryEnv ν) (arrayMeasure ν) where
diff --git a/LeanMachineLearning/Online/Bandit/SumRewards.lean b/LeanMachineLearning/Online/Bandit/SumRewards.lean
index 5fbec0ee..48b7e0ba 100644
--- a/LeanMachineLearning/Online/Bandit/SumRewards.lean
+++ b/LeanMachineLearning/Online/Bandit/SumRewards.lean
@@ -77,6 +77,7 @@ lemma prob_pullCount_mem_and_sumRewards_mem_le (a : 𝓐) (n : ℕ)
   · simp [h_empty]
   convert prob_pullCount_prod_sumRewards_mem_le a n (hs.prod hB) (ν := ν) (alg := alg)
     with _ _ _ k hk
+  · rfl
   · ext n
     have : ∃ x, x ∈ B := h_nonempty
     simp [this]
@@ -276,6 +277,7 @@ lemma prob_pullCount_mem_and_sumRewards_mem_le [Countable 𝓐]
   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
+  · rfl
   · ext n
     have : ∃ x, x ∈ B := h_nonempty
     simp [this]
@@ -290,7 +292,9 @@ lemma prob_sumRewards_mem_le [Countable 𝓐] (h : IsAlgEnvSeq A R alg (stationa
       ∑ k ∈ range (n + 1), streamMeasure ν {ω | ∑ i ∈ range k, ω i a ∈ B} := by
   classical
   have h_le := prob_pullCount_mem_and_sumRewards_mem_le h .univ hB (a := a) (n := n)
-  simpa using h_le
+  simp only [Set.mem_univ, true_and, filter_true] at h_le
+  convert h_le
+  rfl
 
 lemma prob_pullCount_eq_and_sumRewards_mem_le [Countable 𝓐]
     (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P)
diff --git a/LeanMachineLearning/SequentialLearning/Algorithm.lean b/LeanMachineLearning/SequentialLearning/Algorithm.lean
index 9f5748d8..bdb3c405 100644
--- a/LeanMachineLearning/SequentialLearning/Algorithm.lean
+++ b/LeanMachineLearning/SequentialLearning/Algorithm.lean
@@ -294,7 +294,7 @@ def IsAlgEnvSeq.filtrationAction
         refine le_sup_of_le_left ?_
         rw [← measurable_iff_comap_le]
         suffices Measurable[IsAlgEnvSeq.filtration hA hY 0] (A 0) from
-          this.mono ((IsAlgEnvSeq.filtration hA hY).mono zero_le') le_rfl
+          this.mono ((IsAlgEnvSeq.filtration hA hY).mono zero_le) le_rfl
         exact adapted_action hA hY 0
     have hm : m ≠ 0 := by grind
     simp only [hn, hm, ↓reduceIte]
diff --git a/LeanMachineLearning/SequentialLearning/FiniteActions.lean b/LeanMachineLearning/SequentialLearning/FiniteActions.lean
index d11dfab4..03cb9db6 100644
--- a/LeanMachineLearning/SequentialLearning/FiniteActions.lean
+++ b/LeanMachineLearning/SequentialLearning/FiniteActions.lean
@@ -598,7 +598,9 @@ lemma measurable_comap_indicator_stepsUntil_eq [MeasurableSingletonClass 𝓐]
       exact measurable_const
     have h_meas := adapted_pullCount_add_one hA hR' a (n - 1)
     have : 1 ≤ n := by grind
-    simpa [Nat.sub_add_cancel this] using h_meas
+    convert h_meas using 1
+    · rfl
+    · simp [Nat.sub_add_cancel this]
 
 lemma measurable_indicator_stepsUntil_eq [MeasurableSingletonClass 𝓐]
     (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : 𝓐) (m n : ℕ) :
diff --git a/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean b/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean
index 6c9290cb..e8dd506b 100644
--- a/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean
+++ b/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean
@@ -59,8 +59,7 @@ theorem eq_trajMeasure_of_isAlgEnvSeq (h : IsAlgEnvSeq A₁ R₁ alg env P) :
   · have hA := h.measurable_action n
     have hR := h.measurable_feedback n
     fun_prop
-  · simp only
-    exact h.hasLaw_step_zero
+  · exact h.hasLaw_step_zero
   · exact h.hasCondDistrib_step n
 
 lemma eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil
@@ -207,7 +206,7 @@ def filtrationAction (𝓐 𝓨 : Type*) [MeasurableSpace 𝓐] [MeasurableSpace
         refine le_sup_of_le_left ?_
         rw [← measurable_iff_comap_le]
         suffices Measurable[IT.filtration 𝓐 𝓨 0] (action 0) from
-          this.mono ((IT.filtration 𝓐 𝓨).mono zero_le') le_rfl
+          this.mono ((IT.filtration 𝓐 𝓨).mono zero_le) le_rfl
         exact adapted_action 0
     have hm : m ≠ 0 := by grind
     simp only [hn, hm, ↓reduceIte]
diff --git a/LeanMachineLearning/SequentialLearning/StationaryEnv.lean b/LeanMachineLearning/SequentialLearning/StationaryEnv.lean
index 6a658c93..c33fb2f7 100644
--- a/LeanMachineLearning/SequentialLearning/StationaryEnv.lean
+++ b/LeanMachineLearning/SequentialLearning/StationaryEnv.lean
@@ -137,11 +137,9 @@ def obliviousEnv (ν : ℕ → Kernel 𝓐 𝓨) [∀ n, IsMarkovKernel (ν n)]
   ν0 := ν 0
 -- ANCHOR_END: obliviousEnv
 
-@[simp]
 lemma feedback_obliviousEnv (ν : ℕ → Kernel 𝓐 𝓨) [∀ n, IsMarkovKernel (ν n)] (n : ℕ) :
     (obliviousEnv ν).feedback n = (ν (n + 1)).prodMkLeft _ := by simp [obliviousEnv]
 
-@[simp]
 lemma ν0_obliviousEnv (ν : ℕ → Kernel 𝓐 𝓨) [∀ n, IsMarkovKernel (ν n)] :
     (obliviousEnv ν).ν0 = ν 0 := by simp [obliviousEnv]
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 568c5ae9..304e065a 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -8,7 +8,7 @@
    "rev": "a86770a5eba721c8554d1d7fce741bc4dde3bb61",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
-   "inputRev": null,
+   "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/PatrickMassot/checkdecls.git",
@@ -25,17 +25,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c5ea00351c28e24afc9f0f84379aa41082b1188f",
+   "rev": "e912d6b313529e5ceb784745057de4e1dcc964b0",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0",
+   "inputRev": null,
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a456461b368b71d2accd95234832cd9c174b5437",
+   "rev": "744117af710b1c0400cd297c9ce91f8d0ad3a347",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "515cf9d0c00ece5e661f6de4326a53dedc1e8ea1",
+   "rev": "99c763c8a96d3d44fb4994e96eaa51ca4568449d",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,37 +65,37 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a84b3e2475d5c5ab979567b1ad8aea21b764bcf8",
+   "rev": "1537e3fc7e680d64e06fe5fb95c4c9edee7941c2",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.99",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "558915ae105bfd8074e22d597613d1961822adc2",
+   "rev": "7897ea6e5cfc6522d355083bdfa798377ab35e11",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a6e6c34c4ef182f83b219a3a5a385f51f44bdc4c",
+   "rev": "94346b7b49c36ae871639d1434232f057c193d60",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "32dc18cde3684679f3c003de608743b57498c56f",
+   "rev": "0bbac0a875ac0fd9366cb5bd4211da92d960ac84",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,10 +105,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "6b907cf12b2e445ccb7c24bc208ef04a1f39e84c",
+   "rev": "baf3e62fbb3502305076ca077e004aea78157c63",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0",
+   "inputRev": "v4.31.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "LeanMachineLearning",
diff --git a/lakefile.toml b/lakefile.toml
index 82662275..3efe4e38 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -12,7 +12,6 @@ weak.linter.mathlibStandardSet = true
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.30.0"
 
 [[require]]
 name = "checkdecls"
@@ -21,6 +20,7 @@ git = "https://github.com/PatrickMassot/checkdecls.git"
 [[require]]
 name = "subverso"
 git = "https://github.com/leanprover/subverso"
+rev = "main"
 
 [[lean_lib]]
 name = "LeanMachineLearning"
diff --git a/lean-toolchain b/lean-toolchain
index af9e5d33..6af09a89 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.30.0
+leanprover/lean4:v4.31.0-rc2
\ No newline at end of file