diff --git a/SampCert.lean b/SampCert.lean
index 5a7ac53e..11e4b65e 100644
--- a/SampCert.lean
+++ b/SampCert.lean
@@ -18,8 +18,17 @@ import Init.Data.UInt.Lemmas
 
 open SLang PMF
 
-def combineConcentrated := @privNoisedBoundedMean_DP zCDPSystem
-def combinePure := @privNoisedBoundedMean_DP PureDPSystem
+theorem combineConcentrated [dpn : DPNoise (zCDPSystem (T := ℕ))] (U ε₁ ε₂ : ℕ+) (ε : NNReal)
+    (h : dpn.noise_priv ε₁ (2 * ε₂) (ε / 2)) :
+    @DPSystem.prop ℕ (zCDPSystem (T := ℕ)) ℚ
+      (@privNoisedBoundedMean (zCDPSystem (T := ℕ)) dpn U ε₁ ε₂) ε :=
+  @privNoisedBoundedMean_DP (zCDPSystem (T := ℕ)) dpn U ε₁ ε₂ ε h
+
+theorem combinePure [dpn : DPNoise (PureDPSystem (T := ℕ))] (U ε₁ ε₂ : ℕ+) (ε : NNReal)
+    (h : dpn.noise_priv ε₁ (2 * ε₂) (ε / 2)) :
+    @DPSystem.prop ℕ (PureDPSystem (T := ℕ)) ℚ
+      (@privNoisedBoundedMean (PureDPSystem (T := ℕ)) dpn U ε₁ ε₂) ε :=
+  @privNoisedBoundedMean_DP (PureDPSystem (T := ℕ)) dpn U ε₁ ε₂ ε h
 
 /-
 ##  Example: execute the histogram mean on a list
diff --git a/SampCert/DifferentialPrivacy/Abstract.lean b/SampCert/DifferentialPrivacy/Abstract.lean
index 88c4c920..eae5b4db 100644
--- a/SampCert/DifferentialPrivacy/Abstract.lean
+++ b/SampCert/DifferentialPrivacy/Abstract.lean
@@ -102,11 +102,9 @@ end DPSystem
 
 lemma DPSystem_prop_ext [dps : DPSystem T] {ε₁ ε₂ : NNReal} (m : Mechanism T U) (Hε : ε₁ = ε₂) (H : dps.prop m ε₁) :
     dps.prop m ε₂ := by
-  rw [<- Hε]
-  assumption
+  rwa [← Hε]
 
 
-@[simp]
 lemma bind_bind_indep (p : Mechanism T U) (q : Mechanism T V) (h : U → V → PMF A) :
     (fun l => (p l) >>= (fun a : U => (q l) >>= fun b : V => h a b)) =
     fun l => (privCompose p q l) >>= (fun z => h z.1 z.2) := by
diff --git a/SampCert/DifferentialPrivacy/Neighbours.lean b/SampCert/DifferentialPrivacy/Neighbours.lean
index b8758b5b..7055f2e7 100644
--- a/SampCert/DifferentialPrivacy/Neighbours.lean
+++ b/SampCert/DifferentialPrivacy/Neighbours.lean
@@ -26,7 +26,7 @@ inductive Neighbour (l₁ l₂ : List T) : Prop where
 /--
 Neighbour relation is symmetric.
 -/
-def Neighbour_symm (l₁ l₂ : List T) (H : Neighbour l₁ l₂) : Neighbour l₂ l₁ := by
+theorem Neighbour_symm (l₁ l₂ : List T) (H : Neighbour l₁ l₂) : Neighbour l₂ l₁ := by
   cases H
   · rename_i _ _ _ Hl1 Hl2
     exact Neighbour.Deletion Hl2 Hl1
diff --git a/SampCert/DifferentialPrivacy/Pure/AdaptiveComposition.lean b/SampCert/DifferentialPrivacy/Pure/AdaptiveComposition.lean
index 4f164cee..def9d0c7 100644
--- a/SampCert/DifferentialPrivacy/Pure/AdaptiveComposition.lean
+++ b/SampCert/DifferentialPrivacy/Pure/AdaptiveComposition.lean
@@ -7,7 +7,7 @@ import SampCert.DifferentialPrivacy.Generic
 import SampCert.DifferentialPrivacy.Pure.DP
 import Mathlib.Data.Set.Defs
 import Mathlib.Data.Set.Prod
-import Mathlib.Logic.IsEmpty.Basic
+import Mathlib.Basic.IsEmpty.Basic
 
 noncomputable section
 
diff --git a/SampCert/DifferentialPrivacy/Queries/AboveThresh/Properties.lean b/SampCert/DifferentialPrivacy/Queries/AboveThresh/Properties.lean
index d8ea6f6c..ad7e6dae 100644
--- a/SampCert/DifferentialPrivacy/Queries/AboveThresh/Properties.lean
+++ b/SampCert/DifferentialPrivacy/Queries/AboveThresh/Properties.lean
@@ -333,7 +333,6 @@ lemma sv1_loop_ub (qs : sv_query sv_T) (T τ : ℤ) (ε₁ ε₂ : ℕ+) (l : Li
         conv =>
           enter [1, a]
           rw [← ENNReal.tsum_mul_right]
-          simp
         rw [ENNReal.tsum_comm]
         enter [1, b]
 
@@ -761,13 +760,15 @@ def sv4_loop (qs : sv_query sv_T) (T : ℤ) (ε₁ ε₂ : ℕ+) (τ : ℤ) (l :
   let v <- probWhileCut (sv4_aboveThreshC qs T τ l) sv4_aboveThreshF (point + 1) (init, presamples)
   return v.1
 
+omit dps dpn in
 /-- Total mass of a point distribution restricted to the states with a given
 first component. -/
 lemma tsum_indicator_pure (X : sv4_state) (fs : sv1_state) (h : fs = X.1) :
     (∑' (a : sv4_state), if fs = a.1 then probPure X a else 0) = 1 := by
-  rw [tsum_eq_single X (fun b hb => by simp [SLang.pure_apply_of_ne _ _ hb, hb])]
-  simp [h, SLang.pure_apply_self]
+  rw [tsum_eq_single X (fun b hb => by simp [hb])]
+  simp [h]
 
+omit dps dpn in
 /-- When `sv4`'s loop condition fails the loop halts immediately. -/
 lemma sv4_probWhileCut_succ_false (qs : sv_query sv_T) (T τ : ℤ) (l : List sv_T) (n : ℕ)
     (s : sv1_state) (ps : List ℤ) (h : ¬ sv1_aboveThreshC qs T τ l s = true) :
@@ -775,9 +776,10 @@ lemma sv4_probWhileCut_succ_false (qs : sv_query sv_T) (T τ : ℤ) (l : List sv
     probPure (s, ps) := by
   have hC : ¬ sv4_aboveThreshC qs T τ l (s, ps) = true := h
   simp only [probWhileCut, probWhileFunctional]
-  rw [if_neg hC]
+  rw [ite_eq_right hC]
   rfl
 
+omit dps dpn in
 /-- One step of `sv4`'s loop: when the condition holds, the head presample is
 consumed and the state advances. -/
 lemma sv4_probWhileCut_succ (qs : sv_query sv_T) (T τ : ℤ) (l : List sv_T) (n : ℕ)
@@ -785,7 +787,7 @@ lemma sv4_probWhileCut_succ (qs : sv_query sv_T) (T τ : ℤ) (l : List sv_T) (n
     probWhileCut (sv4_aboveThreshC qs T τ l) sv4_aboveThreshF (n + 1) (s, p :: ps) =
     probWhileCut (sv4_aboveThreshC qs T τ l) sv4_aboveThreshF n ((s.1 ++ [s.2], p), ps) := by
   have hC : sv4_aboveThreshC qs T τ l (s, p :: ps) = true := h
-  simp only [probWhileCut, probWhileFunctional, hC, if_true, sv4_aboveThreshF,
+  simp only [probWhileCut, probWhileFunctional, hC, ite_true, sv4_aboveThreshF,
     Bind.bind, Pure.pure]
   exact SLang.pure_bind _ _
 
@@ -856,7 +858,7 @@ lemma sv4_presample_eval (ε₁ ε₂ : ℕ+) (n : ℕ) (s : { l : List ℤ // L
       rw [← HF]
       rw [← this]
       rw [mul_comm]
-    haveI : RightCommutative F := by
+    have : RightCommutative F := by
       subst HF
       exact ⟨fun b a₁ a₂ => mul_right_comm _ _ _⟩
     rw [← List.foldl_cons]
@@ -920,6 +922,7 @@ lemma sv4_presample_split' (ε₁ ε₂ : ℕ+) (point : ℕ) (z : ℤ) (p : { l
       trivial
 
 
+omit dps dpn in
 lemma foldl_mul_left (g : ℤ → ENNReal) (a : ENNReal) (l : List ℤ) :
     List.foldl (fun acc b => acc * g b) a l = a * List.foldl (fun acc b => acc * g b) 1 l := by
   induction l generalizing a with
@@ -934,7 +937,7 @@ lemma sv4_presample_split'' (ε₁ ε₂ : ℕ+) (point : ℕ) (z : ℤ) (p : {
     sv4_presample ε₁ ε₂ (point + 1) ⟨ (p.1 ++ [z]), HP ⟩ := by rw [sv4_presample_split']
 
 -- Splits and rearranges the functions
-def sv4_presample_split (ε₁ ε₂ : ℕ+) (point : ℕ) :
+theorem sv4_presample_split (ε₁ ε₂ : ℕ+) (point : ℕ) :
     sv4_presample ε₁ ε₂ (point + 1) =
     (do
       let presample_1 <- sv4_presample ε₁ ε₂ 1
@@ -965,7 +968,7 @@ def sv4_presample_split (ε₁ ε₂ : ℕ+) (point : ℕ) :
   simp_all [len_list_append_rev]
 
   -- Join the sv4_presamples
-  simp only [mul_ite, mul_zero, sv4_presample_split']
+  simp only [sv4_presample_split']
   rw [vector_sum_merge]
   rw [vector_sum_merge]
 
@@ -983,14 +986,14 @@ def sv4_presample_split (ε₁ ε₂ : ℕ+) (point : ℕ) :
   · simp
     intro A B C
     right
-    apply if_neg
+    apply ite_eq_right
     intro K
     apply C
     subst K
     apply Subtype.ext
     exact (cons_headI_tail (by intro K'; subst K'; simp at B)).symm
 
-  rw [ENNReal.tsum_eq_add_tsum_ite ⟨[vsm_last final_state] ++ (vsm_init final_state), by simp [(vsm_init final_state).2, Nat.add_comm] ⟩ ]
+  rw [ENNReal.tsum_eq_add_tsum_ite ⟨[vsm_last final_state] ++ (vsm_init final_state), by simp [(vsm_init final_state).2] ⟩ ]
   refine Eq.trans (zero_add _).symm ?_
   conv =>
     rhs
@@ -999,7 +1002,7 @@ def sv4_presample_split (ε₁ ε₂ : ℕ+) (point : ℕ) :
   · symm
     simp
     intro A B C
-    apply if_neg
+    apply ite_eq_right
     intro K
     apply C
     subst K
@@ -1208,7 +1211,7 @@ lemma sv3_sv4_loop_eq_zero (qs : sv_query sv_T) (T τ : ℤ) (ε₁ ε₂ : ℕ+
       show (if sv1_aboveThreshC qs T τ l init = true then
               ((sv4_aboveThreshF (init, ([] : List ℤ))).probBind fun _ => probZero)
             else probPure (init, ([] : List ℤ))) i = 0
-      rw [if_neg hcond]
+      rw [ite_eq_right hcond]
       apply pure_apply_of_ne
       intro HK
       apply hk2
@@ -1258,8 +1261,6 @@ theorem sv3_sv4_loop_eq (qs : sv_query sv_T) (T : ℤ) (ε₁ ε₂ : ℕ+) (τ
     unfold sv4_loop
     conv =>
       enter [2]
-      unfold probWhileCut
-      unfold probWhileFunctional
       unfold sv4_aboveThreshC
 
     split
@@ -1290,10 +1291,6 @@ theorem sv3_sv4_loop_eq (qs : sv_query sv_T) (T : ℤ) (ε₁ ε₂ : ℕ+) (τ
       match vs1, Hvs1 with
       | [], Hvs1 => exact absurd Hvs1 (by simp)
       | vs1 :: vs_emp, Hvs1 =>
-      conv =>
-        enter [2, 1, a, 1]
-        unfold sv4_aboveThreshF
-        simp [len_list_append_rev]
       have Hemp : vs_emp = [] := by cases vs_emp <;> simp_all
       subst Hemp
       show probWhileCut (sv4_aboveThreshC qs T τ l) sv4_aboveThreshF (point + 1)
@@ -1434,7 +1431,7 @@ lemma sv5_sv6_loop_base_case (qs :  sv_query sv_T) (T : ℤ) (τ : ℤ) (l : Lis
   unfold probWhileFunctional
   split
   · next h =>
-    simp [probWhileCut, sv6_loop]
+    simp [sv6_loop]
     rw [h]
     simp
   · next h =>
@@ -1448,7 +1445,7 @@ lemma sv5_sv6_loop_base_case (qs :  sv_query sv_T) (T : ℤ) (τ : ℤ) (l : Lis
     have Hpt : point = sv1_threshold (past, pres) := by
       simp [sv1_threshold]
       omega
-    rw [if_pos Hpt]
+    rw [ite_eq_left Hpt]
     conv =>
       lhs; rw [← add_zero (1 : ENNReal)]
     congr 1
@@ -1827,9 +1824,9 @@ lemma sv1_lb_advance (τ : ℤ) (ε₁ ε₂ : ℕ+) (l : List sv_T) (cut : ℕ)
   rw [Hunroll]
   unfold probWhileFunctional
   by_cases hcond : sv1_aboveThreshC qs T τ l (H, v) = true
-  · rw [if_pos hcond]
+  · rw [ite_eq_left hcond]
     simp
-  · rw [if_neg hcond]
+  · rw [ite_eq_right hcond]
     simp
     apply ENNReal.tsum_lb_single (List.length H)
     apply ENNReal.tsum_lb_single (H, v)
@@ -1863,7 +1860,7 @@ lemma sv1_lb_advance (τ : ℤ) (ε₁ ε₂ : ℕ+) (l : List sv_T) (cut : ℕ)
       enter [1, b]
       rw [X b]
     clear X
-    simp [sv1_aboveThreshF, probBind]
+    simp [sv1_aboveThreshF]
     apply le_trans
     · apply ENNReal.tsum_le_tsum
       intro a
@@ -2155,7 +2152,7 @@ lemma sv1_lb (lucky_guess : has_lucky qs T) ε₁ ε₂ l :
       show (∑' (a : { t // PLucky t }), (privNoiseGuess ε₁ ε₂) ↑a) = _
       congr 1
       ext a
-      rw [if_pos (by simp [sv1_threshold])]
+      rw [ite_eq_left (by simp [sv1_threshold])]
       rcases a with ⟨a, Ha⟩
       have hcond : sv1_aboveThreshC qs T τ l (H ++ [v], a) = false := by
         simp [sv1_aboveThreshC, sv1_noise, sv1_threshold]
diff --git a/SampCert/DifferentialPrivacy/Queries/Histogram/Code.lean b/SampCert/DifferentialPrivacy/Queries/Histogram/Code.lean
index 256bba7a..07ac5d2b 100644
--- a/SampCert/DifferentialPrivacy/Queries/Histogram/Code.lean
+++ b/SampCert/DifferentialPrivacy/Queries/Histogram/Code.lean
@@ -28,7 +28,7 @@ variable (numBins : ℕ+)
 
 def predBins : ℕ := numBins.natPred
 
-def predBins_lt_numBins : predBins numBins < numBins := by
+theorem predBins_lt_numBins : predBins numBins < numBins := by
   rw [predBins]
   cases numBins
   rename_i v Hv
diff --git a/SampCert/DifferentialPrivacy/RenyiDivergence.lean b/SampCert/DifferentialPrivacy/RenyiDivergence.lean
index 33db834f..e35d0519 100644
--- a/SampCert/DifferentialPrivacy/RenyiDivergence.lean
+++ b/SampCert/DifferentialPrivacy/RenyiDivergence.lean
@@ -278,7 +278,7 @@ theorem Renyi_Jensen_strict_real [t2 : MeasurableSingletonClass T] [tcount : Cou
   have A := strictConvexOn_rpow h
   have B := continuousOn_rpow_Ici_of_one_lt h
   have C : IsClosed (Set.Ici (0 : ℝ)) := isClosed_Ici
-  haveI : IsProbabilityMeasure (PMF.toMeasure q) := PMF.toMeasure.isProbabilityMeasure q
+  have : IsProbabilityMeasure (PMF.toMeasure q) := PMF.toMeasure.isProbabilityMeasure q
   have D := @StrictConvexOn.ae_eq_const_or_map_average_lt T ℝ t1 _ _ _ (PMF.toMeasure q)
     (Set.Ici 0) f (fun (x : ℝ) => x ^ α) inferInstance A B C
     (MeasureTheory.ae_of_all (PMF.toMeasure q) h2)
@@ -306,7 +306,7 @@ theorem Renyi_Jensen_strict_real [t2 : MeasurableSingletonClass T] [tcount : Cou
         show f x = ∑' y : T, (q y).toReal * f y
         simpa using Heqx
       · -- `q x` is nonzero but the indicator forces it to vanish — contradiction.
-        simp only [Set.mem_setOf_eq, Set.indicator_apply, if_pos Heqx] at Hx
+        simp only [Set.mem_ofPred_eq, Set.indicator_apply, ite_eq_left Heqx] at Hx
         exact absurd Hx (HT_nz x)
     · -- Case: strict Jensen gave `(∫ f)^α < ∫ f^α`.
       left
@@ -355,34 +355,34 @@ lemma Renyi_Jensen_f_MemLp [MeasurableSpace T] [MeasurableSingletonClass T] [Cou
     (Hspecial : ∀ x : T, ¬(p x = ⊤ ∧ q x ≠ 0 ∧ q x ≠ ⊤))
     (Hnts : ∑' (a : T), (p a / q a) ^ α * q a ≠ ⊤) :
     MemLp (Renyi_Jensen_f p q) (ENNReal.ofReal α) (PMF.toMeasure q) := by
-  haveI : DiscreteMeasurableSpace T := MeasurableSingletonClass.toDiscreteMeasurableSpace
+  have : DiscreteMeasurableSpace T := MeasurableSingletonClass.toDiscreteMeasurableSpace
   have HRJf_nonneg (a : T) : 0 ≤ Renyi_Jensen_f p q a := toReal_nonneg
   have HRJf_nt := Renyi_Jensen_div_ne_top p q H Hspecial
-  refine ⟨?_, ?_⟩
+  have hp_ne_zero : ENNReal.ofReal α ≠ 0 := by simp; linarith
+  have hp_ne_top : ENNReal.ofReal α ≠ ⊤ := by simp
+  rw [memLp_iff]
+  rw [eLpNorm_eq_lintegral_rpow_enorm_toReal hp_ne_zero hp_ne_top]
+  rw [toReal_ofReal (le_of_lt (lt_trans zero_lt_one h))]
+  apply ENNReal.rpow_lt_top_of_nonneg (by positivity)
+  rw [MeasureTheory.lintegral_countable']
+  have Hsummand_eq : ∀ a : T,
+      ‖Renyi_Jensen_f p q a‖ₑ ^ α * (PMF.toMeasure q) {a} = (p a / q a) ^ α * q a := by
+    intro a
+    congr 1
+    · show (‖Renyi_Jensen_f p q a‖₊ : ENNReal) ^ α = (p a / q a) ^ α
+      rw [← Real.toNNReal_eq_nnnorm_of_nonneg (HRJf_nonneg a)]
+      show (ENNReal.ofReal (Renyi_Jensen_f p q a)) ^ α = (p a / q a) ^ α
+      rw [show Renyi_Jensen_f p q a = (p a / q a).toReal from rfl,
+          ENNReal.ofReal_toReal (HRJf_nt a)]
+    · exact PMF.toMeasure_apply_singleton _ _ (measurableSet_singleton _)
+  simp_rw [Hsummand_eq]
+  exact Hnts
   · apply MeasureTheory.StronglyMeasurable.aestronglyMeasurable
     apply Measurable.stronglyMeasurable
     apply Measurable.ennreal_toReal
     show Measurable (fun x => p x / q x)
     simp_rw [division_def]
     exact (Measurable.of_discrete).mul ((Measurable.of_discrete).inv)
-  · have hp_ne_zero : ENNReal.ofReal α ≠ 0 := by simp; linarith
-    have hp_ne_top : ENNReal.ofReal α ≠ ⊤ := by simp
-    rw [eLpNorm_eq_lintegral_rpow_enorm_toReal hp_ne_zero hp_ne_top]
-    rw [toReal_ofReal (le_of_lt (lt_trans zero_lt_one h))]
-    apply ENNReal.rpow_lt_top_of_nonneg (by positivity)
-    rw [MeasureTheory.lintegral_countable']
-    have Hsummand_eq : ∀ a : T,
-        ‖Renyi_Jensen_f p q a‖ₑ ^ α * (PMF.toMeasure q) {a} = (p a / q a) ^ α * q a := by
-      intro a
-      congr 1
-      · show (‖Renyi_Jensen_f p q a‖₊ : ENNReal) ^ α = (p a / q a) ^ α
-        rw [← Real.toNNReal_eq_nnnorm_of_nonneg (HRJf_nonneg a)]
-        show (ENNReal.ofReal (Renyi_Jensen_f p q a)) ^ α = (p a / q a) ^ α
-        rw [show Renyi_Jensen_f p q a = (p a / q a).toReal from rfl,
-            ENNReal.ofReal_toReal (HRJf_nt a)]
-      · exact PMF.toMeasure_apply_singleton _ _ (measurableSet_singleton _)
-    simp_rw [Hsummand_eq]
-    exact Hnts
 
 /--
 Jensen's inequality applied to ENNReals, in the case that q is nonzero.
@@ -390,7 +390,7 @@ Jensen's inequality applied to ENNReals, in the case that q is nonzero.
 lemma Renyi_Jensen_ENNReal_reduct [MeasurableSpace T] [MeasurableSingletonClass T] [Countable T]
   (p q : PMF T) {α : ℝ} (h : 1 < α) (H : AbsCts p q) :
   (∑' x : T, (p x / q x) * q x) ^ α ≤ (∑' x : T, (p x / q x) ^ α * q x) := by
-  haveI : DiscreteMeasurableSpace T := MeasurableSingletonClass.toDiscreteMeasurableSpace
+  have : DiscreteMeasurableSpace T := MeasurableSingletonClass.toDiscreteMeasurableSpace
   by_cases Hnts : ∑' (a : T), (p a / q a) ^ α * q a = ⊤
   · rw [Hnts]; exact OrderTop.le_top _
   by_cases Hspecial : ∀ x : T, ¬(p x = ⊤ ∧ q x ≠ 0 ∧ q x ≠ ⊤)
@@ -452,7 +452,7 @@ lemma Renyi_Jensen_ENNReal_converse_reduct [MeasurableSpace T] [MeasurableSingle
   (p q : PMF T) {α : ℝ} (h : 1 < α) (H : AbsCts p q) (Hq : ∀ t, q t ≠ 0)
   (Hsumeq : (∑' x : T, (p x / q x) * q x) ^ α = (∑' x : T, (p x / q x) ^ α * q x)) :
   (p = q) := by
-  haveI : DiscreteMeasurableSpace T := MeasurableSingletonClass.toDiscreteMeasurableSpace
+  have : DiscreteMeasurableSpace T := MeasurableSingletonClass.toDiscreteMeasurableSpace
   by_cases Hnts : ∑' (a : T), (p a / q a) ^ α * q a = ⊤
   · -- One of the series is Top, so the other series is too
     rw [Hnts] at Hsumeq
diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/AdaptiveComposition.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/AdaptiveComposition.lean
index b88a4e2f..af81647b 100644
--- a/SampCert/DifferentialPrivacy/ZeroConcentrated/AdaptiveComposition.lean
+++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/AdaptiveComposition.lean
@@ -151,10 +151,11 @@ theorem privComposeAdaptive_zCDPBound {nq1 : List T → PMF U} {nq2 : U -> List
     exact _root_.add_le_add (h1 α Hα l₁ l₂ Hneighbours) conditional_ub
   exact privComposeAdaptive_renyi_bound Hα Hneighbours HAC1 HAC2
 
+omit HU HU_meas HU_discr HU_count [MeasurableSpace V] [MeasurableSingletonClass V] [Countable V] in
 /--
 Adaptive composition preserves absolute continuity
 -/
-def privComposeAdaptive_AC (nq1 : Mechanism T U) (nq2 : U -> Mechanism T V) (Hac1 : ACNeighbour nq1) (Hac2 : ∀ u, ACNeighbour (nq2 u)) :
+theorem privComposeAdaptive_AC (nq1 : Mechanism T U) (nq2 : U -> Mechanism T V) (Hac1 : ACNeighbour nq1) (Hac2 : ∀ u, ACNeighbour (nq2 u)) :
     ACNeighbour (privComposeAdaptive nq1 nq2) := by
   simp only [ACNeighbour]
   simp [privComposeAdaptive]
diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/Const.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/Const.lean
index d87b8fd1..7c13f0ef 100644
--- a/SampCert/DifferentialPrivacy/ZeroConcentrated/Const.lean
+++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/Const.lean
@@ -33,10 +33,11 @@ theorem privConst_zCDPBound {u : U} : zCDPBound (privConst u : Mechanism T U) 0
   refine (RenyiDivergence_aux_zero (PMF.pure u) (PMF.pure u) ?G1 fun x a => a).mp rfl
   linarith
 
+omit [MeasurableSpace U] [MeasurableSingletonClass U] [Countable U] in
 /--
 Constant query satisfies absolute continuity
 -/
-def privConst_AC {u : U} : ACNeighbour (privConst u : Mechanism T U) := by
+theorem privConst_AC {u : U} : ACNeighbour (privConst u : Mechanism T U) := by
   simp [ACNeighbour, AbsCts, privConst]
 
 /--
diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean
index ad9cec45..4e6e14bf 100644
--- a/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean
+++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean
@@ -467,9 +467,9 @@ lemma ApproximateDP_of_zCDP_pos_lt_one [Countable U] (m : Mechanism T U)
   have HK (x : U) : (1 : ENNReal) = (if (z x < ENNReal.ofReal ε') then 1 else 0) + (if (z x ≥ ENNReal.ofReal ε') then 1 else 0) := by
     by_cases h : z x < ENNReal.ofReal ε'
     · have h2 : ¬ (z x ≥ ENNReal.ofReal ε') := not_le.mpr h
-      rw [if_pos h, if_neg h2]; simp
+      rw [ite_eq_left h, ite_eq_right h2]; simp
     · have h2 : z x ≥ ENNReal.ofReal ε' := le_of_not_gt h
-      rw [if_neg h, if_pos h2]; simp
+      rw [ite_eq_right h, ite_eq_left h2]; simp
   conv =>
     enter [1, 1, a]
     rw [<- mul_one (_ * _)]
@@ -1156,7 +1156,7 @@ lemma B_eval_false (Hε : 0 < ε) (Hqp : ∀ x, ENNReal.ofReal (Real.exp (-ε))
   · simp [Function.Injective]
   · intro x Hx
     simp [Function.support] at Hx
-    simp_all only [Subtype.range_coe_subtype, Function.mem_support, ne_eq, Set.mem_setOf_eq, not_false_eq_true]
+    simp_all only [Subtype.range_coe_subtype, Function.mem_support, ne_eq, Set.mem_ofPred_eq, not_false_eq_true]
   · simp [Function.support]
     intros x _
     rw [PMF_mul_mul_inv_eq_mul_cancel p q Hac x]
diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean
index 7d1d6e4d..1f1c5834 100644
--- a/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean
+++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean
@@ -108,7 +108,7 @@ lemma discrete_gaussian_shift {σ : ℝ} (h : σ ≠ 0) (μ : ℝ) (τ x : ℤ)
 /--
 privNoisedQuery preserves absolute continuity between neighbours
 -/
-def privNoisedQuery_AC (query : List T -> ℤ) (Δ ε₁ ε₂ : ℕ+) : ACNeighbour (privNoisedQuery query Δ ε₁ ε₂) := by
+theorem privNoisedQuery_AC (query : List T -> ℤ) (Δ ε₁ ε₂ : ℕ+) : ACNeighbour (privNoisedQuery query Δ ε₁ ε₂) := by
   simp only [ACNeighbour]
   intro l₁ l₂ _
   rw [AbsCts]
diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/Postprocessing.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/Postprocessing.lean
index 5e7549b3..64402ee3 100644
--- a/SampCert/DifferentialPrivacy/ZeroConcentrated/Postprocessing.lean
+++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/Postprocessing.lean
@@ -264,8 +264,6 @@ theorem privPostPocess_DP_pre_reduct {U : Type} [m2 : MeasurableSpace U] [count
     rw [δF₂_Eq]
     simp [δpmf]
     unfold δ
-    repeat rw [DFunLike.coe]
-    repeat rw [PMF.instFunLike]
     simp
     rw [<- N_def]
     rw [<- N_def]
@@ -447,7 +445,7 @@ theorem privPostPocess_DP_pre {nq : List T → PMF U} (HNorm : ∀ l, HasSum (nq
     simp [Function.support]
     exact fun a _ a_2 a_3 => a_2 (Habs' a a_3)
   have HSup3 : Function.support (fun (a : U) => nq l₁ a ^ α * nq l₂ a ^ (1 - α)) ⊆ { u : U | nq l₁ u ≠ 0 } := by
-    simp only [Function.support, Set.setOf_subset_setOf]
+    simp only [Function.support, Set.ofPred_subset_ofPred]
     intro a Hnz
     apply mul_ne_zero_iff.mp at Hnz
     rcases Hnz with ⟨ H1 , _ ⟩
@@ -507,7 +505,7 @@ theorem privPostPocess_DP_pre {nq : List T → PMF U} (HNorm : ∀ l, HasSum (nq
     apply HR
   · rename_i x_empty
     simp at *
-    haveI Hempty : IsEmpty ↑{u : U | ¬(nq l₁) u = 0} := by
+    have Hempty : IsEmpty ↑{u : U | ¬(nq l₁) u = 0} := by
       exact Subtype.isEmpty_of_false fun a a_1 => a_1 (x_empty a)
     simp only [tsum_empty]
     simp
@@ -530,13 +528,8 @@ theorem privPostProcess_zCDPBound {nq : Mechanism T U} {ε : ℝ}
   rw [DFunLike.coe]
   rw [PMF.instFunLike]
   simp
-  conv =>
-    enter [1, 1, 2, 1, 1, x]
-    repeat rw [SLang.toPMF]
-    simp
   conv =>
     enter [2, 1, 2, 1, 1, x]
-    repeat rw [SLang.toPMF]
     repeat rw [DFunLike.coe]
     repeat rw [PMF.instFunLike]
     simp
@@ -555,10 +548,11 @@ theorem privPostProcess_zCDPBound {nq : Mechanism T U} {ε : ℝ}
   · apply Hac l₂ l₁
     exact Neighbour_symm l₁ l₂ h2
 
+omit [MeasurableSpace U] [Countable U] [DiscreteMeasurableSpace U] in
 /--
 privPostProcess preserves absolute continuity between neighbours
 -/
-def privPostProcess_AC {f : U → V} (nq : Mechanism T U) (Hac : ACNeighbour nq) : ACNeighbour (privPostProcess nq f) := by
+theorem privPostProcess_AC {f : U → V} (nq : Mechanism T U) (Hac : ACNeighbour nq) : ACNeighbour (privPostProcess nq f) := by
   simp only [ACNeighbour] at *
   unfold AbsCts at *
   intro l₁ l₂ Hn v
diff --git a/SampCert/Foundations/Monad.lean b/SampCert/Foundations/Monad.lean
index d9adb887..576b5578 100644
--- a/SampCert/Foundations/Monad.lean
+++ b/SampCert/Foundations/Monad.lean
@@ -40,10 +40,10 @@ variable (a a' : α)
 theorem pure_apply : probPure a a' = if a' = a then 1 else 0 := rfl
 
 theorem pure_apply_self : probPure a a = 1 :=
-  if_pos rfl
+  ite_eq_left rfl
 
 theorem pure_apply_of_ne (h : a' ≠ a) : probPure a a' = 0 :=
-  if_neg h
+  ite_eq_right h
 
 variable (p : SLang α) (f : α → SLang β) (g : β → SLang γ)
 
diff --git a/SampCert/Foundations/UniformByte.lean b/SampCert/Foundations/UniformByte.lean
index 4bb79fbf..4a21dd86 100644
--- a/SampCert/Foundations/UniformByte.lean
+++ b/SampCert/Foundations/UniformByte.lean
@@ -39,7 +39,7 @@ local instance : Finite UInt8 := by
 /--
 ProbUniformByte is a proper distribution
 -/
-def probUniformByte_normalizes : HasSum probUniformByte 1 := by
+theorem probUniformByte_normalizes : HasSum probUniformByte 1 := by
   rw [Summable.hasSum_iff ENNReal.summable]
   unfold SLang.probUniformByte
   rw [division_def]
@@ -62,7 +62,7 @@ def probUniformByte_PMF : PMF UInt8 := ⟨ probUniformByte, probUniformByte_norm
 /--
 Evaluation of ``probUniformByteUpperBits`` for inside the support
 -/
-def probUniformByteUpperBits_eval_support {i x : ℕ} (Hx : x < 2 ^ (min 8 i)) :
+theorem probUniformByteUpperBits_eval_support {i x : ℕ} (Hx : x < 2 ^ (min 8 i)) :
     probUniformByteUpperBits i x = 2^(8 - i) / UInt8.size := by
   simp [probUniformByteUpperBits]
   rw [Nat.sub_eq_max_sub]
@@ -96,7 +96,7 @@ def probUniformByteUpperBits_eval_support {i x : ℕ} (Hx : x < 2 ^ (min 8 i)) :
       rename_i h val property
       subst HT
       simp_all only
-      simp_all only [Set.mem_setOf_eq]
+      simp_all only [Set.mem_ofPred_eq]
     conv =>
       enter [1, 1, a]
       rw [H a]
@@ -217,7 +217,7 @@ def probUniformByteUpperBits_eval_support {i x : ℕ} (Hx : x < 2 ^ (min 8 i)) :
 /--
 Evaluation of ``probUniformByteUpperBits`` for zero-shifts outside of the support
 -/
-def probUniformByteUpperBits_eval_zero {i x : ℕ} (Hx : x ≥ 2 ^ (min 8 i)) :
+theorem probUniformByteUpperBits_eval_zero {i x : ℕ} (Hx : x ≥ 2 ^ (min 8 i)) :
     probUniformByteUpperBits i x = 0 := by
   simp [probUniformByteUpperBits]
   rw [Nat.sub_eq_max_sub]
@@ -259,7 +259,7 @@ lemma UIint8_cast_lt_size (a : UInt8) : a.toNat < UInt8.size := by
 /--
 Evaluation of ``probUniformP2`` for inside the support
 -/
-def probUniformP2_eval_support {i x : ℕ} (Hx : x < 2 ^ i):
+theorem probUniformP2_eval_support {i x : ℕ} (Hx : x < 2 ^ i):
     probUniformP2 i x = (1 / 2 ^ i) := by
   revert x
   induction i using Nat.strong_induction_on with | _ i ih => ?_
@@ -408,7 +408,7 @@ def probUniformP2_eval_support {i x : ℕ} (Hx : x < 2 ^ i):
 /--
 Evaluation of ``probUniformP2`` for zero-shifts outside of the support
 -/
-def probUniformP2_eval_zero {i x : ℕ} (Hx : x ≥ 2 ^ i):
+theorem probUniformP2_eval_zero {i x : ℕ} (Hx : x ≥ 2 ^ i):
     probUniformP2 i x = 0 := by
   revert x
   induction i using Nat.strong_induction_on with | _ i ih => ?_
diff --git a/SampCert/Samplers/BernoulliNegativeExponential/Properties.lean b/SampCert/Samplers/BernoulliNegativeExponential/Properties.lean
index 682c5efa..9ce0c5c1 100644
--- a/SampCert/Samplers/BernoulliNegativeExponential/Properties.lean
+++ b/SampCert/Samplers/BernoulliNegativeExponential/Properties.lean
@@ -74,7 +74,7 @@ theorem BernoulliExpNegSampleUnitAux_succ_true (num : ℕ) (den : ℕ+) (fuel :
   cases st
   rename_i b' r'
   simp only [probWhileCut, probWhileFunctional, ite_apply, BernoulliExpNegSampleUnitLoop,
-    Bind.bind, Pure.pure, SLang.bind_apply, SLang.pure_apply, if_true]
+    Bind.bind, Pure.pure, SLang.bind_apply, SLang.pure_apply, ite_true]
   rw [ENNReal.tsum_prod']
   simp only [tsum_bool]
   rw [tsum_eq_single (r + 1) (by intro b hb; simp [hb])]
diff --git a/SampCert/Samplers/Gaussian/Properties.lean b/SampCert/Samplers/Gaussian/Properties.lean
index 67b28625..54721087 100644
--- a/SampCert/Samplers/Gaussian/Properties.lean
+++ b/SampCert/Samplers/Gaussian/Properties.lean
@@ -253,7 +253,7 @@ theorem DiscreteGaussianSample_apply (num : PNat) (den : PNat) (mix : ℕ) (x :
   clear A
 
   simp only [ENNReal.tsum_prod', tsum_bool, ↓reduceIte, DiscreteGaussianSampleLoop_apply_true,
-    Nat.succPNat_coe, Nat.succ_eq_add_one, PNat.mk_coe, cast_add, cast_one, PNat.pow_coe, cast_pow, zero_add, ite_mul,
+    Nat.succPNat_coe, Nat.succ_eq_add_one, cast_add, cast_one, PNat.pow_coe, cast_pow, zero_add, ite_mul,
     zero_mul, SLang.pure_apply, div_pow, Bool.false_eq_true]
   rw [ENNReal.tsum_eq_add_tsum_ite x]
   conv =>
diff --git a/SampCert/Samplers/Geometric/Properties.lean b/SampCert/Samplers/Geometric/Properties.lean
index a0a6fe88..cb8effe2 100644
--- a/SampCert/Samplers/Geometric/Properties.lean
+++ b/SampCert/Samplers/Geometric/Properties.lean
@@ -101,7 +101,7 @@ theorem geometric_succ_true (fuel n : ℕ) (st : Bool × ℕ) :
   rename_i b m
   simp only [probWhileCut, probWhileFunctional, geoLoopBody, ite_apply,
     Bind.bind, Pure.pure, SLang.bind_apply, SLang.pure_apply]
-  rw [if_pos (show geoLoopCond (true, n) = true by rfl)]
+  rw [ite_eq_left (show geoLoopCond (true, n) = true by rfl)]
   rw [ENNReal.tsum_prod']
   simp only [tsum_bool, Prod.mk.injEq, true_and]
   rw [tsum_eq_single (n + 1) (by intro b hb; simp [hb])]
@@ -325,7 +325,7 @@ theorem geometric_returns_false (n fuel k : ℕ) (b : Bool) :
   · rename_i fuel IH
     intro n k b
     cases b
-    · simp [probWhileCut, probWhileFunctional, geoLoopBody, geoLoopCond, probBind, probPure]
+    · simp [probWhileCut, probWhileFunctional, geoLoopCond, probPure]
     · simp [probWhileCut, probWhileFunctional, geoLoopBody, geoLoopCond, probBind, probPure, IH]
 
 lemma if_simpl_geo (x n : ℕ) :
diff --git a/SampCert/Samplers/Laplace/Properties.lean b/SampCert/Samplers/Laplace/Properties.lean
index 3b201013..e4111896 100644
--- a/SampCert/Samplers/Laplace/Properties.lean
+++ b/SampCert/Samplers/Laplace/Properties.lean
@@ -9,7 +9,7 @@ import SampCert.Samplers.Uniform.Basic
 import SampCert.Samplers.Bernoulli.Basic
 import SampCert.Samplers.BernoulliNegativeExponential.Basic
 import SampCert.Samplers.Geometric.Basic
-import Mathlib.Data.ENNReal.Inv
+import Mathlib.Basic.ENNReal.Inv
 import SampCert.Samplers.Laplace.Code
 
 /-!
@@ -119,7 +119,7 @@ theorem DiscreteLaplaceSampleLoopIn1_apply (t : PNat) (n : ℕ) (support : n < t
       (if (i + (t : ℕ) < (t : ℕ))
         then ENNReal.ofReal (rexp (-((↑(i + ↑t) : ℝ) / ↑↑t))) / ↑↑t else (0 : ENNReal)) = 0 := by
     intro i
-    rw [if_neg (by omega)]
+    rw [ite_eq_right (by omega)]
   simp_rw [hzero, tsum_zero, add_zero]
   rw [sum_ite]
   simp only [mem_range, imp_self, forall_const, filter_true_of_mem, not_lt, not_le,
@@ -815,7 +815,7 @@ theorem DiscreteLaplaceSampleLoop_equiv (num : PNat) (den : PNat) :
         · erw [BernoulliSample_apply_true]
           norm_num
       split <;> try simp [HB]
-      all_goals (try (cases b <;> simp [HB]))
+      all_goals (try (cases b <;> simp))
   rw [H]
   clear H
   congr
diff --git a/SampCert/Samplers/Uniform/Properties.lean b/SampCert/Samplers/Uniform/Properties.lean
index f3c2aaac..a1ea14e6 100644
--- a/SampCert/Samplers/Uniform/Properties.lean
+++ b/SampCert/Samplers/Uniform/Properties.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jean-Baptiste Tristan
 -/
 import SampCert.Foundations.Basic
-import Mathlib.Data.ENNReal.Basic
+import Mathlib.Basic.ENNReal.Basic
 import SampCert.Samplers.Uniform.Code
 
 /-!
@@ -132,10 +132,10 @@ Evaluation of the ``UniformSample`` distribution inside its support.
 @[simp]
 theorem UniformSample_apply (n : PNat) (x : Nat) (support : x < n) :
   UniformSample n x = 1 / n := by
-  simp only [UniformSample, Bind.bind, Pure.pure, SLang.bind_apply, probUntil_apply,
-    decide_eq_true_eq, rw_ite, one_div, ite_mul, zero_mul, SLang.pure_apply]
+  simp only [UniformSample, probUntil_apply,
+    decide_eq_true_eq, rw_ite, one_div, ite_mul, zero_mul]
   rw [ENNReal.tsum_eq_add_tsum_ite x]
-  simp only [support, ↓reduceIte, mul_one]
+  simp only [support, ↓reduceIte]
   have A : ∀ x_1 : ℕ, (@ite ℝ≥0∞ (x_1 = x) (propDecidable (x_1 = x)) 0
           (@ite ℝ≥0∞ (x_1 < ↑n) (decLt x_1 ↑n) 0 (UniformPowerOfTwoSample (2 * n) x_1)))
           = (@ite ℝ≥0∞ (↑n ≤ x_1) (decLe ↑n x_1) (UniformPowerOfTwoSample (2 * n) x_1) 0) := by
diff --git a/SampCert/Util/Gaussian/DiscreteGaussian.lean b/SampCert/Util/Gaussian/DiscreteGaussian.lean
index e36e29ed..3716be94 100644
--- a/SampCert/Util/Gaussian/DiscreteGaussian.lean
+++ b/SampCert/Util/Gaussian/DiscreteGaussian.lean
@@ -340,7 +340,7 @@ theorem discrete_gaussian_normalizes {σ : ℝ} (h : σ ≠ 0) (μ : ℝ) :
 /--
 Discrete Gaussian cast to ENNReal has sum 1
 -/
-def discrete_gaussian_normal {σ : ℝ} (h : σ ≠ 0) (μ : ℝ) : HasSum (fun z : ℤ => ENNReal.ofReal (discrete_gaussian σ μ z)) 1 := by
+theorem discrete_gaussian_normal {σ : ℝ} (h : σ ≠ 0) (μ : ℝ) : HasSum (fun z : ℤ => ENNReal.ofReal (discrete_gaussian σ μ z)) 1 := by
   rw [Summable.hasSum_iff ENNReal.summable]
   rw [<- ENNReal.ofReal_tsum_of_nonneg]
   case hf_nonneg =>
diff --git a/SampCert/Util/Gaussian/GaussBound.lean b/SampCert/Util/Gaussian/GaussBound.lean
index cb7f17e6..8aa9f84c 100644
--- a/SampCert/Util/Gaussian/GaussBound.lean
+++ b/SampCert/Util/Gaussian/GaussBound.lean
@@ -113,16 +113,7 @@ theorem sum_gauss_term_bound {σ : ℝ} (h : σ ≠ 0) (μ : ℝ) :
             simp
             rw [← Real.sqrt_zero]
             congr 1
-            have P1 : |π| = π := by
-              rw [_root_.abs_of_nonneg]
-              rw [le_iff_lt_or_eq]
-              left
-              apply pi_pos
-            rw [P1]
-            rw [← mul_add]
-            simp
-            right
-            ring_nf
+            ring
           · simp
       rw [← X]
       rw [H]
diff --git a/SampCert/Util/Log.lean b/SampCert/Util/Log.lean
index b0c64cc7..42990a2a 100644
--- a/SampCert/Util/Log.lean
+++ b/SampCert/Util/Log.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jean-Baptiste Tristan, Markus de Medeiros
 -/
 
-import Mathlib.Data.ENNReal.Basic
+import Mathlib.Basic.ENNReal.Basic
 import Mathlib.Data.EReal.Basic
 import Mathlib.Analysis.SpecialFunctions.Log.Basic
 import Mathlib.Analysis.SpecialFunctions.Pow.NNReal
diff --git a/lake-manifest.json b/lake-manifest.json
index f5f2901e..7177a67f 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,27 +5,27 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "0df444a360eaa60ab8c11dca51a86af692955474",
+   "rev": "d13f23b723b8a846827a245b89c10fc7d3f11612",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.33.1",
+   "inputRev": "v4.34.1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/doc-gen4",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e2af49a7b7e5e1a9224008c1f15e7aa4f58a4015",
+   "rev": "953c8992d174b4e56955e01e101d46668c68f2bb",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.33.1",
+   "inputRev": "v4.34.1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb",
+   "rev": "118aa17ee84656b8bd727fef7c458ee8c833385c",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404",
+   "rev": "ddf04cf3949fa556442341e87d47f9f6e6074707",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "16f02aa7642864af59f1ff0e384a015994db9118",
+   "rev": "e928b72544873815af278d38681b31c0293588e3",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957",
+   "rev": "106ff4fafc74ef4ac99d81dbf3ab399118f497a5",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e",
+   "rev": "355695d523e41d0554926416cba2a2b3544fbbc9",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81",
+   "rev": "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d",
+   "rev": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6168b7549738a19bc837a1625c60c5d1e5dd8aeb",
+   "rev": "f9cdb9eacb5c8b8ecc02ee9fd9e568d7d28c1416",
    "name": "leansqlite",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,17 +105,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "6130a47896ce867c6a4a55373441e59e565bad0f",
+   "rev": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.33.0",
+   "inputRev": "v4.34.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/fgdorais/lean4-unicode-basic",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "37e7d8cb7316a88cd3e91208385c9ec6ae780019",
+   "rev": "0e569d08b6443ce0908d356884c765397253e2f0",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -125,7 +125,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "852edafa268eb038a7158551fd580ee8433847b0",
+   "rev": "4d8616fd4870d0a3453d845770833eac7951fe1c",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
diff --git a/lakefile.lean b/lakefile.lean
index ad3d6c94..a92b7f13 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -5,10 +5,10 @@ package «sampcert» where
   testDriver := "test"
 
 require «doc-gen4» from git
-  "https://github.com/leanprover/doc-gen4" @ "v4.33.1"
+  "https://github.com/leanprover/doc-gen4" @ "v4.34.1"
 
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git" @ "v4.33.1"
+  "https://github.com/leanprover-community/mathlib4.git" @ "v4.34.1"
 
 target ffi.o (pkg : NPackage __name__) : FilePath := do
   let oFile := pkg.buildDir / "ffi.o"
diff --git a/lean-toolchain b/lean-toolchain
index a8afa7d1..ba8ebf2d 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.33.1
+leanprover/lean4:v4.34.1